GitLab

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.