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

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

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

- - - - - 29c3f091 by Simon Génier at 2022-09-02T14:36:31-04:00 Merge branch 'oops-fix-off-by-one-error-on-line-numbers'

- - - - - ef72535e by Jean-Alexandre Barszcz at 2022-09-28T22:20:38-04:00 [WIP] Don't close the types of builtins

`lexp_close` introduces redundant definitions with let-expressions. Instead of closing the built-in (with their type), we keep track of their context (length) and shift them appropriately where they are used.

- - - - - acf0b570 by Jean-Alexandre Barszcz at 2022-10-12T03:24:48-04:00 [WIP] Add an internal name ("id") to make typecons more nominal

Comparing all the constructors and parameters of typeconses for conversion is slow. This commit takes the easy and short approach, by minimally changing the `Inductive` constructor and only adding an internal name. Conversion is checked by comparing this internal name, which is faster. However, type safety relies on the proper use of this name.

Design constraints: I would like to

1. be able to escape the nominal paradigm and refer to a typecons by value if needed (if its internal name is known).

2. not influence the property that the pretty printed code can be re-elaborated. A challenge here is that typeconses can be substituted through the code, so they have to be "pure".

3. avoid larger changes to the context (if the formal parameter and constructor info is not present in the typecons, it has to be somewhere in the context).

Another option meeting these requirement would be to add an indirection (eg. `typeconsref`) to `lexp` that is not substituted like normal variables, but still points to the typecons in context. The elaboration of inductives would bind the typecons and return a reference to it.

This indirection would take care of the redundancy of the current representation and avoid inconsistencies, but require a bit more work to implement.

- - - - - 35c30984 by Jean-Alexandre Barszcz at 2022-11-09T01:20:59-05:00 [WIP] Fix predefs; Reflect lists and S-exps

- - - - - 53a58925 by Jean-Alexandre Barszcz at 2022-11-09T13:04:39-05:00 [WIP] Remove Vsexp from value_type

- - - - - 511daa3a by Jean-Alexandre Barszcz at 2022-11-09T13:05:47-05:00 [WIP] Replace the Sexp builtins by regular constructors

- - - - -

29 changed files:

- .gitignore - + .idea/workspace.xml - btl/builtins.typer - btl/pervasive.typer - debug_util.ml - opam - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/dune - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - + src/predefs.ml - + src/pretty-printer.scm - src/sexp.ml - src/source.ml - src/unification.ml - src/util.ml

The diff was not included because it is too large.

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