Simon Génier pushed to branch oops-fix-off-by-one-error-on-line-numbers 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.

- - - - - 50069ddc by Shon Feder at 2022-03-11T20:42:03-05:00 Add Zarith dependency to opam file

Also adds "synopsis" and "description" fields, with content taken from https://www.iro.umontreal.ca/~monnier/

- - - - - 12c08fbb by Shon Feder at 2022-03-11T20:42:03-05:00 Ignore the opam switch directory

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

- - - - - f0551384 by Stefan Monnier at 2022-08-27T14:07:24-04:00 Merge branch 'add-zarith-dependency' into 'main'

See merge request monnier/typer!2

- - - - - 525e358e by Simon Génier at 2022-08-28T22:37:40-04:00 Add a test for type ascription.

Also improve how discrepancies in sexp tests are reported.

- - - - - 2a824e2d by Simon Génier at 2022-08-28T22:39:23-04:00 Pretty-prints the code emitted by the Gambit backend.

It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL.

- - - - - cc46ac0a by Simon Génier at 2022-09-02T14:34:57-04:00 Fix off by one error on line numbers.

The source_file object start in a kind of null state, with an empty line, causing to read the first line lazily as the first char is peeked. This means we need to put the cursor before the first line and not on the first line!

- - - - -

29 changed files:

- .gitignore - + .idea/workspace.xml - btl/case.typer - btl/do.typer - + btl/monads.typer - btl/pervasive.typer - + btl/poly-lits.typer - debug_util.ml - opam - 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/dune - src/elab.ml - src/elexp.ml - src/eval.ml - src/fmt.ml - src/gambit.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/e0d8110c35cd9cdfd69f87233d03c25ac...