GitLab

* src/REPL.ml (main): Re-raise internal error, so OCAMLRUNPARAM=b gives
a proper backtrace.

* samples/nat.typer (even1): Make it trickier to catch the previous error.

This patch add a new primitive type, ##DataconsLabel, which uniquely identifies
a data constructor within a type. Its inhabitants will be consumed by Low Level
Typer to write the correct header for objects. The goal is to give an abstract
type that is as useful on Typer on OCaml where the labels are strings than on a
future backend which will be better for Low Level Typer and where labels will
likely be integers.

Values are created through the primitive ##datacons-label<-string and there is
also a macro datacons-label which allows us to write a symbol directly. I
choosed to use a right pointing arrow its name, against the Lisp convention. I
think it makes more sense in languages with an ML syntax because function
composition is made like this

    c<-b . b<-a

and it also goes in the same direction as the b_of_a convention in OCaml. I also
though it was OK because there where no other primitives with arrows in their
names so that convention does not clash with others.

Finally, I decided to go against the name ##Discriminent because it suggests it
only applies to sum types, but ##DataconsLabel is also needed for product types.

Some of these changes bring the style more in line with the GNU coding standard
that is used for Typer.
- Reindent file to 2 spaces.
- Break lines before a operator.
- Break lines before 80 columns.

Others are my attempts to improve readability.
- Use functions specialized on refs in Arg.
- Remove superfluous parenthesis.
- Extract large fun expressions to local let bindings.

  (lexp_whnf_aux): Add the reduction of calls to builtins, for
  registered builtins.

* tests/elab_test.ml: Test the WHNF of `Eq.cast`.

Add a FIXME and an internal error instead of using a wrong
substitution in the elaboration of a repeated metavariable.

  Replace `move_typelevel_to_front` with the new function
  `sort_generalized_metavars`, which, in addition to bringing the
  typelevel parameters to the front, sorts the remaining generalized
  metavariables topologically so that later variables can depend on
  ealier ones, and ignores metavariables that are in lower scope
  levels.

  (generalize): Call the new function.

* btl/builtins.typer (Eq_comm): Correct the FIXME.

This make it possible to focus on tests that have spaces in their title.

  (erasure_dummy): The new dummy.

  (erase_type, clean_default, clean_map): Use it.

Substitute the erased variables in the branch bodies.

* tests/eval_test.ml: Test the fix.

(unify_or_error): New function, extracted from check_inferred.
(check_inferred): Use it.

Try and impose some logic on the order in which the various
unification cases are handled.

(unify'): Shuffle.
(unify_*): Simplify accordingly.
(unify_call): Handle calls of different length.

* tests/unify_test.ml: Rewrite and enable the tests.

* btl/depelim.typer: New file, implements the macro.
* btl/pervasive.typer: Load the new macro.
* tests/elab_test.ml: Test it.

* btl/builtins.typer: Add the builtin `Integer->Int`.
* src/eval.ml: Implement it.
(sexp_dispatch): Fix the value passed to the integer handler.

* tests/eval_test.ml: Test that overflows cause runtime errors

* Add tools and libraries.
* Bump OCaml version to the latest one on Debian stable.

This commit changes elaboration, conversion, typechecking, erasure,
and the computation of free variables and WHNFs for case expressions,
to account for the fact that the context of all the branches of case
expressions is extended with a proof of equality between the branch's
head and the case's target. Careful elimination of this equality proof
with Eq_cast makes dependent elimination possible.

This commit doesn't substantially change the behavior of the case
elaboration, but makes the code a bit more consistent and might save
some unnecessary metavariables in some cases.

* src/debruijn.ml : Add a definition of the lexp for Eq.refl

* src/builtin.ml : Register the constant Eq.refl

* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl
instead of registering the builtin with the `Built-in` form. This
ensures that we have the right variable and type, and might help to
keep things in sync between the ocaml and typer code.