GitLab

Preparing for the GT demo

Empty extracted modules (all definitions are defined in the driver)
are printed no more, independently of the extraction mode

New command line nearly done

Preparing for the new command line.

Preparing for the new command line (flat recursive extraction of symbols
only works for definitions in the same file).

Preparing for the new command line (not working for now).

Preparing for the new command line.

Preparation for the new command line

Preparation for the new command line

Preparing for monolithic extraction.

Better treatment of partial applied constructors

in preparation of command-line option --mono

Support for recursive extraction and qualified names

Treatment of top-level constants

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 well-typed, 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"

[Raise] expressions compiled and printed

Some examples from the gallery adapted for extraction purposes

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

Inlining of variables binded to unit

Constructors without arguments are now inlined in extracted code