Simon Génier pushed to branch compiler-phase-simpl at Stefan / Typer

Commits: d3daf0a3 by Soilih BEN SOILIH at 2022-02-16T10:07:07-05:00 Add a `Proj` constructor to the `lexp` type

We add a projection constructor to the Lexp type in order to be able to offer the completion in a satisfactory manner for the LSP server. When we write MODULE.FIELD, if FIELD doesn't exist, we could not offer the completion because the AST could not be generated at all. So we add this case to be able to have an AST and be able to find the functions of a module, and also select specific functions thanks to the label of a projection.

* src/lexp.ml (lexp): Add `Proj` constructor. (lexp'_hash, lexp_head, lexp_location, push_susp, clean, lexp_unparse) (lexp_str): Adjust accordingly. (mkProj): new function. * src/elab.ml (adjust_subst.loop): Add `Proj` case for the loop substitution. (sform_proj): new special form. (register_special_forms): Register it. * src/opslexp.ml (pos_of_label): new function. (check'', get_type, fv, erase_type): * src/positivity.ml (positive'): Add new case for `Proj`. * src/eval.ml (eval): * src/apply_inv_subst.ml (apply_inv_subst): * src/elexp.ml (elexp, elexp_location, elexp_name, elexp_string): Add new case for `Proj`. * btl/pervasive.typer (__/.__): Delete macro.

- - - - - 29c8aded by Simon Génier at 2022-02-16T19:17:56-05:00 Add a flag to show macros, their arguments and the expanded code.

- - - - - a072f995 by Jean-Alexandre Barszcz at 2022-03-12T13:34:42-05:00 * shell.nix : Set the Ocaml version to 4.11

- - - - - ffd27741 by Jean-Alexandre Barszcz at 2022-03-17T15:34:57-04:00 * tests/samples_test.ml : Check that the samples can be evaluated.

- - - - - 60431a62 by Stefan Monnier at 2022-04-15T19:30:26-04:00 Improve support for typelevels in inductive types

* src/opslexp.ml (check''): Allow (erasable) typelevel fields. (get_type): Adjust accordingly.

* src/log.ml (handle_error): Don't catch internal errors.

* src/lexp.ml (mkSLsucc): Add some info in the error.

- - - - - 76398acd by Jean-Alexandre Barszcz at 2022-04-18T15:33:06-04:00 * src/opslexp.ml (lexp_whnf_aux): Add WHNF of Proj.

- - - - - 5adbad56 by Jean-Alexandre Barszcz at 2022-04-30T22:39:36-04:00 * src/opslexp.ml (lexp_whnf): Cleanup/simplify the recursive calls.

- - - - - 807227bd by Jean-Alexandre Barszcz at 2022-05-02T03:16:58-04:00 * src/unification.ml (unify): Provide a `matching` mode.

This new mode is for instance argument resolution, where unification is limited to a subset of the metavariables. We will characterize this subset with an increased scope level.

(associate): Make `associate` mutate the global metavar table to provide a cleaner interface.

- - - - - d9fc38a5 by Jean-Alexandre Barszcz at 2022-05-02T03:17:00-04:00 * src/elab.ml: Handle sdforms in a common way.

- - - - - 8306886e by Jean-Alexandre Barszcz at 2022-05-02T03:44:50-04:00 * src/debruijn.ml: Add a type class context to the elab context.

Use getters and setters for the elab_context. With 5 components in the elaboration context, tuple matching and construction has become impractical.

* src/elab.ml: Add the `typeclass` sdform that adds a type to the set of typeclasses in the typeclass context.

Add the `instance` and `not-instance` sdforms that set the instance flag for given variables in the typeclass context.

Add the `bind-instances` and `dont-bind-instances` sdforms that set the default instance flag for new variables.

* src/instargs.ml: New source file for things related to instance arguments.

- - - - - 0781fd2f by Jean-Alexandre Barszcz at 2022-05-02T03:45:02-04:00 * tests/instargs_test.ml: New file, test the type class context.

- - - - - e18bf31b by Jean-Alexandre Barszcz at 2022-05-02T03:45:02-04:00 * src/elab.ml: Save metavars' elaboration contexts for resolution.

* src/instargs.ml: Keep a table of resolution contexts for instance metavariables.

- - - - - 65341b0d by Jean-Alexandre Barszcz at 2022-05-02T03:48:51-04:00 * src/instargs: Implement instance resolution.

* src/elab.ml: Resolve instances before every generalization.

(lexp_check_decls): Resolve instances for recursive definitions.

(lexp_expr_str): Resolve instances when elaborating from a string.

* src/REPL.ml: Resolve and generalize expressions in the REPL.

- - - - - 35309dd9 by Jean-Alexandre Barszcz at 2022-05-02T03:48:53-04:00 * src/unification.ml (unify_call) : Return CKImpossible when we can.

- - - - - 699f644d by Jean-Alexandre Barszcz at 2022-05-02T03:48:53-04:00 Make integer literals polymorphic using type classes

* btl/poly-lits.typer: New file implementing polymorphic integer literals through the "typer-immediate" hook and type classes.

* btl/pervasive.typer: Use the new definition of "typer-immediate".

- - - - - 944fc4ac by Jean-Alexandre Barszcz at 2022-05-02T03:48:53-04:00 Change integer literals to have type Integer by default

- - - - - 2df52873 by Jean-Alexandre Barszcz at 2022-05-02T03:48:53-04:00 Make `do` polymorphic with a `Monad` class.

- - - - - a2bc3d5c by Stefan Monnier at 2022-05-10T14:50:33-04:00 * src/debruijn.ml (senv_lookup): Fix ordering of tests

- - - - - c422f432 by “falismai@iro.umontreal.ca” at 2022-05-26T18:51:50+00:00 [OK] Compilateur

- - - - - cbd1e53a by “falismai@iro.umontreal.ca” at 2022-05-31T20:45:09+00:00 Ajout du type sinfo

- - - - - 471c1ff6 by “falismai@iro.umontreal.ca” at 2022-05-31T20:52:07+00:00 Ajout du type sinfo pour Sexp-info

- - - - - 7d6ba1f2 by Simon Génier at 2022-09-02T14:03:27-04:00 Introduce an Op record to track operators during parsing.

This makes explicit the presence or not of rhs and lhs arguments instead of implicitely tracking them via empty symbols.

- - - - - 135e4ba1 by Simon Génier at 2022-09-02T14:03:27-04:00 Adds a simplification phase.

It β-reduces let bindings when the value bound is a variable or built-in, i.e. when there is - no-side effect - the value is as fast to evaluate as a variable.

The hope is that it will help the readability of the code after macro expantion, without have to rewrite every macro to be smart about expanding to let-expressions.

Since I'm a coward, I'm leaving it disabled by default. Use `-O` to enable it.

- - - - -

24 changed files:

- + .idea/workspace.xml - btl/case.typer - btl/do.typer - + btl/monads.typer - btl/pervasive.typer - + btl/poly-lits.typer - debug_util.ml - samples/decltype.typer - + samples/dune - + samples/nats.typer - + samples/unerase.typer - shell.nix - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/eval.ml - + src/instargs.ml - src/inverse_subst.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/da35c28dd8f332d62ba810596261e6c70...