Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: 28d16874 by irradiee at 2020-08-14T05:59:20-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp

- - - - - 68f25184 by irradiee at 2020-08-24T13:11:01-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp

- - - - - 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case

A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.

This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.

Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.

- - - - - 115d8b01 by Simon Génier at 2020-09-09T12:06:50-04:00 Make eval tests throw on a compilation failure.

- - - - - e8257259 by Simon Génier at 2020-09-09T12:06:59-04:00 Remove commented eval test.

- - - - - 940ade63 by Simon Génier at 2020-09-09T12:06:59-04:00 Do not print callstack of test handler.

This line always print the same callstack, that of the handler, which gives no information about why the test failed.

- - - - - 53c514f5 by Simon Génier at 2020-09-09T12:06:59-04:00 Actually record the backtrace of exceptions while testing.

- - - - - e0d4964e by Simon Génier at 2020-09-09T12:06:59-04:00 Print compiler log on a compilation error in tests.

- - - - - e290b701 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix implicit arguments test.

- - - - - 5f740bf1 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix case test with generic types.

- - - - - b6466a2b by Simon Génier at 2020-09-09T12:07:23-04:00 Fix the rest of the eval tests.

- - - - - 2041b4dd by Simon Génier at 2020-09-09T12:07:34-04:00 Remove = at the end of the flags to the test driver.

I think the intention was to have GNU style flags like --verbose=3, but that does not even work.

- - - - - 56e4fbed by Simon Génier at 2020-09-09T13:24:41-04:00 Easier elaboration tests.

I extracted these changes from another branch since I will need them for yet another. Ther should make elaboration tests easier to write. * New assertions reduce the amount of code to check the results. * Correctly restore state to be able to compare metavariables in two different code fragments.

- - - - - 9d41029c by Simon Génier at 2020-09-09T13:24:48-04:00 Rework add_test to avoid warnings.

- - - - - 10c27014 by Simon Génier at 2020-09-09T13:24:48-04:00 Make success and failure values.

- - - - - 18f49df0 by Simon Génier at 2020-09-09T13:31:55-04:00 Make expected an optional argument in elaboration tests.

- - - - - b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test.

- - - - - a8e2af1a by Simon Génier at 2020-09-10T09:38:07-04:00 Oops: add back running tests in the order they were inserted.

- - - - - a4540d14 by Simon Génier at 2020-09-10T15:47:53-04:00 Merge changes to elaboration and evaluation tests.

- - - - - 4eac6264 by Simon Génier at 2020-09-10T16:05:31-04:00 Get rid of warning by using String.uppercase_ascii.

This function is available since 4.03, and 4.05 is now on Debian stable so it is safe to use.

- - - - - a5a05e7b by Simon Génier at 2020-09-11T17:22:08-04:00 Merge branch 'string-uppercase' into master.

- - - - - c34d6d0c by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Fix an issue in the unification of metavariables

The issue was that unification was not idempotent in certain cases. In particular, when unifying a metavar that has a non-identity substitution (let's say lxp1) with a term (let's say lxp2) that refers to some metavariables, the corresponding metavariable references in the associated term (thus in lxp1 after association) could have different substitutions from the same references in lxp2. See the added comment for a more detailed example.

- - - - - 023ea461 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - b4d53239 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make Eq.refl available to the ocaml code

* 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.

- - - - - efe2032d by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make the case elaboration code more consistent

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.

- - - - - 4c632a1f by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Add dependent elimination

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.

- - - - - b082a329 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Conversion for metavariables

- - - - - fd990da1 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Case conversion

- - - - - eb1741eb by Simon Génier at 2020-09-16T09:21:42-04:00 Update the requirements for building typer.

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

- - - - - bcb53b2c by Simon Génier at 2020-09-16T09:21:42-04:00 Use Map.S.find_opt.

- - - - - b36d30ac by Simon Génier at 2020-09-16T09:21:42-04:00 Oops: fix broken tests on OCaml 4.05.0.

- - - - - 1fb4ed6c by Simon Génier at 2020-09-16T09:23:33-04:00 Merge branch 'update-requirements' into HEAD

- - - - - 371c37d4 by Jean-Alexandre Barszcz at 2020-09-19T23:59:22-04:00 Big ints in sexps and for int literals

* Change the sexp datatype to have Zarith big integers instead of plain Ocaml `int`s. * Change the type of integer literals to `Integer` instead of `Int`. * Add the `Integer->Int` builtin. * Add overflow checking to the `Int` builtin operators.

- - - - - 12076610 by Jean-Alexandre Barszcz at 2020-09-20T00:01:57-04:00 Improve quoting

- - - - - 695d98c7 by Jean-Alexandre Barszcz at 2020-09-20T00:01:57-04:00 Add a macro for dependent elimination

- - - - - e4da0173 by Jean-Alexandre Barszcz at 2020-09-24T14:39:40-04:00 Clarify unification

* Clarify the order of the handlers for different cases of unification. * Enable and rewrite unification tests.

- - - - - b5106636 by Jean-Alexandre Barszcz at 2020-09-24T14:39:40-04:00 Unify instead of conv_p in sform_lambda

- - - - - 04ad364a by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 [WIP] experiments with Decidable and proofs

- - - - - 596ec34c by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 [WIP] First draft of an instance search algorithm

- - - - - 34b2175f by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 [WIP] Add a syntax for records

- - - - - c23a9b2f by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 [WIP] Extend the Decidable sample with conjunction (dep on records)

- - - - - f3b767f9 by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 Resolve instances in the REPL (since exprs. are not generalized)

- - - - - b34687eb by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 Resolve instances for recursive definitions

- - - - - 2064b112 by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 [WIP] Do the set_getenv

IIRC these were missing to correctly handle the elab context for macro expansion and Elab_... primitives. Perhaps it would be simpler to call set_getenv once before macro expansion rather than everywhere where the context can change. Needs some experimentation and tests.

- - - - - d6991cfe by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 Num class example

- - - - - 2900fa72 by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 Num class (with records)

- - - - - 5b458959 by Jean-Alexandre Barszcz at 2020-09-24T14:40:17-04:00 Algebra classes sample with proofs for the additive monoid for Nats

- - - - -

30 changed files:

- GNUmakefile - README.md - btl/builtins.typer - btl/case.typer - + btl/depelim.typer - btl/do.typer - btl/list.typer - btl/pervasive.typer - btl/plain-let.typer - btl/polyfun.typer - + btl/records.typer - btl/tuple.typer - + samples/alg_classes.typer - + samples/decidable.typer - + samples/num_class.typer - + samples/num_class_recs.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/eval.ml - + src/float.ml - + src/instances.ml - + src/int.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/myers.ml

The diff was not included because it is too large.

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/7619fb6c2e74f82e3d688e402e55174e1...