!A and ?A are the actual names of the variables.  So if you want to reuse the same variable several times in a rule, each of them should use the ! or the ?.

I agree with you that it is a good idea to report an error message if somebody tries to use both A and !A (or ?A) in the same rule.  However, we do not need to report an error if they use both !A and ?A, but no A.

Grigore


________________________________
From: Radu Mereuta [notifications@github.com]
Sent: Friday, May 23, 2014 11:15 AM
To: kframework/k
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;


What constructor are you referring to?
I've asked Andrei to strip the "?" and "!" from the beginning of the variable so I can still run the CheckVariablesFilter correctly. This means that "?" and "!" is a semantic modifier to the variable, and is not part of the name.

The result of this is that a rule like:
rule A => A +Int !A
will produce an error message. I think this is safer and less likely for users to make a mistake.
But if more people disagree with this, we could change it (I know that there are tools which consider the annotations as part of the name).

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/493/files#r13006576>.