Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer

Commits: 4421b8e7 by Stefan Monnier at 2023-03-21T23:25:52-04:00 Fix an inf-loop during elaboration

When `typer-identifier` is redefined as something else than a special form or a macro, we got into an inf-loop when elaborating X because we would rewrite to (typer_identifier X), which would then be taken as a function call, which recursively elaborates its arg X, ...

* src/elab.ml (sform_immediate, sform_identifier): Move before `elaborate`. (elab_via): New function. (elaborate): Use it.

- - - - - 22282068 by Simon Génier at 2023-03-22T18:03:27-04:00 Merge branch 'simon--source-container'

- - - - - e13d2142 by Simon Génier at 2023-03-22T18:05:48-04:00 Use format to print pretokens.

- - - - - e350b2d7 by Simon Génier at 2023-03-22T18:10:14-04:00 Use Format to print sexps.

- - - - - 08503fe0 by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print lexps.

- - - - - 9f89fdce by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print elexps.

- - - - - 2c710bed by Simon Génier at 2023-03-24T16:23:32-04:00 Merge remote-tracking branch 'origin/simon--pp-print'

- - - - - 52c8fa7e by Simon Génier at 2023-03-24T16:26:13-04:00 Move the index set to its own module.

I want to separate the lexp context to its own module, but it depends on the index set in Debruijn. Debruijn will depend on this new Lctx module so splitting the index set is necessary to avoid circular dependencies.

- - - - - 7751fa1f by Simon Génier at 2023-03-24T16:26:14-04:00 Implement IdxSet in terms of Set instead of Map.

It probably ends up also using a map internally, but it makes the code more concise by not having all these () to ignore.

- - - - - 399b98e3 by Simon Génier at 2023-03-24T16:26:14-04:00 Add a fold for IdxSet.

- - - - - 734e0278 by Simon Génier at 2023-03-24T16:26:14-04:00 Move the lexp context to its own module.

- - - - - 53e2324b by Simon Génier at 2023-03-24T16:26:14-04:00 Merge the try and the match in Lctx.lookup.

- - - - - 54bdd38a by Simon Génier at 2023-03-24T16:26:14-04:00 Print the lexp context with the format module.

This patch introduces two important changes to the way lexp contexts are printed.

- The lexp context is now formatted as a list of definitions instead of a table. This leaves more horizontal room to print the expressions themselves. For example,

% index = 1, offset = 0 case_return_ : Macro; case_return_ = (__.__ (depelim) case_return_);

- We leverage the recent changes to the printing of lexps to limit the size of the expressions we print. We get this for free by setting a "box" limit on the formatter. Note that this limit only applies when dumping the context: the full expression is printed when inspecting single value.

Elab_arg-pos = (lambda (a : ##String) -> (lambda (b : ##String) -> (lambda … -> …)));

- - - - -

18 changed files:

- − .idea/workspace.xml - debug_util.ml - + src/IdxSet.ml - src/REPL.ml - src/debruijn.ml - − src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - src/inverse_subst.ml - + src/lctx.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml

The diff was not included because it is too large.

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