I am assuming your are talking about the KAST classes here, which are only used by the kompiler.  That's because we do not want to spend any runtime overhead to read the first character in a string to see whether the variable is fresh or universally quantified.  The Java rewrite engine should encode the rules the possible way it can, so that it can quickly find this information without deciphering strings.  I'm sure that's the way it is, but I just re-iterate it to be safe.

Grigore


________________________________
From: dwightguth [notifications@github.com]
Sent: Friday, May 23, 2014 11:44 AM
To: kframework/k
Cc: Rosu, Grigore
Subject: Re: [k] Unified builtins fresh (#493)


In src/javasources/KTool/src/org/kframework/kil/Variable.java:

> @@ -16,7 +15,8 @@
>      private String name;
>      /** True if the variable was written with an explicit type annotation */
>      private boolean userTyped = false;
> -    private boolean fresh = false;
> +    private boolean freshVariable = false;


My concern here is something different than Grigore's, although I agree with Grigore.

The problem with this solution is it creates a fragmented authority for determining whether a variable in a rule is ! or ?. I look at the freshVariable flag and I don't know if it tells me the correct information, because I could be looking at a variable whose flag was set incorrectly by one of the other constructors.

In my opinion, the variable class, outside the frontend, should have the following fields only:

String name; //name of variable, including ? or !
String declaredSort; //EXPLICIT sort of variable. set only if the variable should be runtime checked to be that sort
String sort; //inherited from Term, set by type inferencer to concrete syntactic sort of variable.


—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/493/files#r13007790>.