 23 Feb, 2017 3 commits


Mário Pereira authored
Better treatment of partial applied constructors

JeanChristophe Filliâtre authored
in preparation of commandline option mono

Mário Pereira authored
Support for recursive extraction and qualified names

 21 Feb, 2017 2 commits


Mário Pereira authored

Mário Pereira authored
Treatment of toplevel constants

 20 Feb, 2017 4 commits


Leon Gondelman authored
1. The equality symbol is now bidirectionally compatible with coercions. That is, in the module Binary below (see bench/typing/good/coercions.mlw), goal G is welltyped, with coercion [to_int] being applied to variable [x] both in [x=y] and in [y=x] : module Binary use import int.Int use import mach.int.Int63 goal G: forall x: int63, y: int. x = y /\ y = x end 2. Each coercion is still uniquely defined by type symbols [Ts, Ts'] [ ls: Ts1 ty_1,1 ... ty_1,n > Ts2 ty_2,1 ... ty_2,m ], but searching for a possible coercion is now taking into account types [ ty_1,1 ... ty_1,n ] and [ ty_2,1 ... ty_2,m ] in order to compare them with the actual type of a term [t] on which coercion may apply as well as the actual expected type. (That is, now the signature of find is [t > ty > ty > lsymbol list]) This is done to anticipate in a heurstic way a situation when a coercion can be technically applied but will eventually fail, because type mismatch between types in coercion signature and the types of a term on which coercion applies. For instance, given a coercion function to_list bool : list bool meta coercion function to_list the following goal is rejected by typing: goal G: forall x: list int, y: bool. x = y Indeed, [y] is expected to be of type [list int]. Since [y] is of type [bool], one may try to apply a coercion [to_list] in order to get a term [to_list y] of type [list bool]. However, this would not help, since a [list bool] mismatch with [list int]. The error message is now better: "This term (i.e. [y]) has type bool, but is expected to have type list int" compared to old version: "This term (i.e. [y]) has type list bool, but is expected to have type list int"

JeanChristophe Filliâtre authored

Mário Pereira authored
[Raise] expressions compiled and printed

Mário Pereira authored

 19 Feb, 2017 1 commit


Mário Pereira authored
Some examples from the gallery adapted for extraction purposes

 16 Feb, 2017 6 commits



Mário Pereira authored
For loops are now turned into a local recursive function. This allows big integers to be used as indexes of the loop

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Mário Pereira authored

 15 Feb, 2017 3 commits


JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

 14 Feb, 2017 7 commits


Mário Pereira authored
Inlining of variables binded to unit

Mário Pereira authored
Constructors without arguments are now inlined in extracted code

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

Mário Pereira authored

Mário Pereira authored

JeanChristophe Filliâtre authored

 13 Feb, 2017 2 commits


JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

 11 Feb, 2017 4 commits


Leon Gondelman authored
This commit fixes some bugs for coercions. 1. Applying coercion should work correctly w.r.t. unification (see modules TrickyPolymorphic(AlphaBeta) in bench/typing/good/coercions.mlw). 2. Union of two coercion maps now works correctly w.r.t. adding the same coercion twice even if it is transitive closure (see module SameTransitivityCheck in bench/typing/good/coercions.mlw). 3. Coercion error printing is now listing all components of conflicting coercion (see bench/typing/bad/coercion_cycle3.mlw for example). In this version, we still just lookup at head tysymbols to decide whether a coercion can be applied. This can be improved by taking into account also the types of arguments to decide earlier that a coercion cannot be applied. For instance, given type t 'a function f (t int) : int meta coercion function f goal G: forall x: t bool. x = 42 results now in an error message This term has type t bool, but is expected to have type t int We can do better, detecting that a coercion f cannot be applied to [x] at all. To be done.

Leon Gondelman authored

Leon Gondelman authored

Mário Pereira authored
Forgetting local variables identifiers

 10 Feb, 2017 3 commits


Mário Pereira authored

Leon Gondelman authored

Leon Gondelman authored

 09 Feb, 2017 5 commits


JeanChristophe Filliâtre authored
a slightly different representation of coercions (using trees instead of lists) bench files for coercions

JeanChristophe Filliâtre authored

Leon Gondelman authored
Now adding the very same coercion is accepted (useful for multiple/transitive use imports)

Leon Gondelman authored

Leon Gondelman authored
