Problem with infix and val predicate in transformations
Hello,
In master, the specification of the following is not usable inside transformations with arguments (apply, rewrite, print).
(** equality is extensional *)
val predicate (==) (s1 s2: seq 'a)
ensures { result <-> length s1 = length s2 &&
forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] }
ensures { result -> s1 = s2 }
This can be reproduce with the following code by searching (==) then trying to print the spec:
module Test
use import int.Int
use import seq.Seq
goal f: create 32 (fun x -> x) == empty -> false
end
I think the reason is that the spec of this is named "infix ==_spec" in pdecl.ml. This is not recognized as a valid identifier by the parser (I think because of the space and "=="). One solution would be to sanitize the new name introduced in pdecl.ml: we would get "infix_eqeq_spec" and be able to use it in transformations. This is probably a bigger problem, the solution looks very ad hoc but I think it works.
copying @rrieuhel as you reported the bug, thanks.