 22 Nov, 2013 2 commits


Andrei Paskevich authored
This is a syntactic sugar for higherorder "any", for which I can't find reasonably unambiguous syntax. One can write val x : int <spec> in <expr> or val f (x : int) : int <spec> in <expr> or val f <spec> (x : int) : int <spec> in <expr> for a function which is created via some effectful computation. This is a generalized form of toplevel "val" which only admits latent effects (as in the second form above).

Andrei Paskevich authored

 20 Nov, 2013 2 commits


Andrei Paskevich authored

Andrei Paskevich authored

 19 Nov, 2013 12 commits


Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored
Needed when e1 is a recursive call whose effects are not yet known.

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored
and sort them out in typing. Actually, there is no reason not to have local lemmas. Also, accept "let ghost (x,y) = ... in ...", which is the same as "let x,y = ghost ... in ...", which is the same as "match ghost ... with x,y > ... end".

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored
Finally, it is simpler to treat "higherorder" applications in Dterm and Dexpr, since we can analyze the dtypes.

 18 Nov, 2013 1 commit


MARCHE Claude authored

 16 Nov, 2013 1 commit


MARCHE Claude authored

 12 Nov, 2013 2 commits


François Bobot authored
fix: recompute_all_shapes forgot to iter on metas

Andrei Paskevich authored
thanks to Johannes Kanig

 11 Nov, 2013 4 commits


Andrei Paskevich authored

Andrei Paskevich authored

Guillaume Melquiond authored

Andrei Paskevich authored
Instead, pass the optional vsymbol representing the result. Now formulasunderpatterns do not need to be typechecked separately, so the previous commit is partially reverted.

 10 Nov, 2013 6 commits


Andrei Paskevich authored
The (pattern > fmla) format is used in Dexpr for postconditions. Also, restructure the mutually recursive calls, with a massive change of indentation (use "git show w" to view this commit).

Andrei Paskevich authored

Andrei Paskevich authored
If the function is defined, the correct opacity for fresh type variables in the result will be computed automatically. If the function is abstract, then every fresh type variable is opaque by default, as no information leak is possible anyway.

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

 09 Nov, 2013 5 commits


Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored
Certain modifications in Why3 change tasks but not the propositional structure of the goal. In this case, it is sometimes easier to use "optimistic pairing": as long as the number of subgoals is the same as in the old session, match them in the existing order, without comparing shapes. This should be used only for repairing sessions after changes in Why3.

Andrei Paskevich authored

 08 Nov, 2013 5 commits


Andrei Paskevich authored

Andrei Paskevich authored
Submitted by Johannes Kanig

Andrei Paskevich authored
Submitted by Johannes Kanig

Andrei Paskevich authored
lskept: the old selection check required at least one nonvariable nonclosed type in the lsymbol's signature. This is too permissive, because (list_match : list 'a > 'b > 'b) is allowed and will produce an instance for every type in the "inst" set. The new check requires that all freely standing type variables occur under a type constructor elsewhere in the lsymbol's signature. lsinst: accept any monomorphic instance of any polymorphic symbol except equality. The old procedure applied the same restrictions as for the "lskept" set which serve no real purpose for "lsinst".

Andrei Paskevich authored
