Stefan pushed to branch main at Stefan / Typer

Commits: 4919a2ab by Maxim Bernard at 2024-05-18T16:48:18-04:00 Move internal representations to a separate module, named Ir.

Import Ir in all relevant modules, and remove unneeded imports.

Move all datatypes representing context (lexp_context, elab_context, typeclass_context, runtime_env) and code (sexp, lexp, elexp, value) and their related types to the same mutually-recursive block.

Rename `set` to `db_set` for clarity.

Rename `value_type` to simply `value` for consistency with the naming convention used in the rest of the project.

Rename all `elexp` constructors by prefixing them with an "E", to avoid clashes with `lexp`.

Change `Imm` constructor so it contains a `sinfo * value` pair instead of an `sexp`. Similar change to `Eimm`.

* src/sexp.ml : Replace `Sym.t` with `symbol` for clarity, and remove `t` for the same reason. Replace certain `sexp`s in function types to `token` when appropriate. Replace certain `sexp`s in function types to `token` when appropriate.

* src/lexp.ml : `lexp_head` can't return the exact Imm name for now; can be fixed later (needs further refactoring). Remove unsued `pred_imm`.

* src/inverse_subst.ml: Improve code clarity.

* src/elab.ml (elab_macro_call) : Replace `token` with `sexp` in argument type for clarity.

- - - - - 7fc20e58 by Maxim Bernard at 2024-05-21T01:57:01-04:00 Move all pretty-printing functions to the same module.

* src/fmt.ml: Move printing functions from all over the project to here. Define them all in the same mutually recursive block (required to print `Imm` values). Polymorphic functions in that block require explicit type variables, otherwise OCaml attempts to assign them a non polymorphic type. Fix bug in `pp_print_lexp` (formerly `Lexp.pp_print`) in `Inductive` branch where a formatting block was opened without being closed.

* src/ir.ml: Move `pretoken` from Prelexer to here. Re-arrange type definitions to minimise recursive definitions. Replace uses of `Source.Location.t` with `location` for clarity.

* src/pexp.ml: Remove obsolete ArgKind module, since functions have been moved to Fmt.

* src/util.ml: Move `maybename` from Lexp to here (required by Fmt).

- - - - - 7b0ff399 by Maxim Bernard at 2024-05-22T01:54:10-04:00 Improve message formatting thoughout the project.

Print log messages using pretty-printing functions when available and the Format module instead of string conversions, which allow for appropriate indentation to be generated.

Perform a `clean` on all lexps prior to printing them, for performance reasons (otherwise, all memory would be consumed).

* src/fmt.ml: Reactivate printing lexps in substitutions (since they can now be printed safely, see above).

* src/lexp.ml: Define functions to be used elsewhere in the project when printing lexps.

* src/log.ml: Change type of `log_msg` to allow for `%a` conversion specifications in format strings.

* src/opslexp.ml: Cleanup dead code and re-organize module imports for cleanness.

- - - - - 2e478c82 by Maxim Bernard at 2024-05-22T17:24:07-04:00 Rearrange definitions in Ir.

* src/ir.ml: Reduce size of mutually recursive `type` block to a minimum, by extracting types that don't need to be there. Transfer a couple of definitions from Util for consistency.

* src/util.ml: Transfer several definitions from here to Ir.

- - - - -

30 changed files:

- src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - 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/ir.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/eval_test.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/macro_test.ml - tests/positivity_test.ml

The diff was not included because it is too large.

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