Jean-Alexandre Barszcz pushed to branch dev/characterization at Stefan / Typer

Commits: c25f821e by Stefan Monnier at 2019-07-24T01:56:09Z * src/subst.ml (subst): Fold a `Shift` into the `Identity`.

Generalize `Identity` with `Identity o` where the old `Identity` is now `Identity 0` and `Identity o` is like the old `Shift (Identity, o)`.

(mkShift): Use `Identity` when possible. (shift): Use `Identity`. (identity): Adjust to new `Identity`. (lookup, identity_p, compose): Generalize to the new `Identity o`. (substitute): Use `identity`.

* src/elab.ml (newMetavar): Use S.identity.

* src/inverse_subst.ml (is_identity): Take advantage of the new `Identity o`. (shift_inv_subst): Optimize the case when n is 0. (transfo, invertible, lookup_inv_subst, compose_inv_subst): Generalize to the new `Identity o`.

* src/lexp.ml (subst_string): Handle the new `Identity o`. (subst_eq): Generalize to the new `Identity o`.

* tests/inverse_test.ml (is_identity): Copy new def from inverse_subst.ml.

* tests/unify_test.ml (generate_testable): Use `identity`.

- - - - - 6c5475e1 by Stefan Monnier at 2019-07-24T04:40:25Z * src/subst.ml (subst): Fold the remaining Shift into Cons.

Fold `Shift` into the `Cons`, and hence remove `Shift` since it's not needed as a separate constructor any more.

(sink, substitute): Use `cons` (lookup, mkShift, cons, compose): * src/lexp.ml (subst_string, subst_eq): * src/inverse_subst.ml (transfo, is_identity, invertible) (lookup_inv_subst, compose_inv_subst): Adjust accordingly.

* tests/inverse_test.ml (is_identity): Update from src/inverse_subst.ml.

* src/opslexp.ml (lexp_whnf): Use `S.cons`.

- - - - - d75ab820 by Stefan Monnier at 2019-07-27T03:38:33Z Add comments from a Myers's subst experiment

* src/lexp.ml (lexp_unparse): Prefer S.cons to S.Cons.

* src/subst.ml (subst): Add Myers's optimization in a comment. It probably works, but it currently bumps into another performance problem. (lookup, compose): Add commented-out Myers's optimization.

* tests/inverse_test.ml (is_identity): Remove (lets the code use the version of Inverse_subst).

- - - - - ff16d3ba by Stefan Monnier at 2019-07-27T03:39:04Z * samples/defmacro.typer (define-macro): New package and macro

- - - - - e3a0fe68 by Stefan Monnier at 2019-09-13T18:31:03Z Avoid using Inverse_subst in core type checking

* src/lexp.ml (mkSLlub', mkSLsucc): New constructors with sanity checks. (sunshift): New function. * src/opslexp.ml (check'', get_type): Use it instead of Inverse_subst.

- - - - - cf67844d by Stefan Monnier at 2019-09-13T21:06:03Z First tweak to try and handle parameterized inductives

* src/elab.ml (check_case.add_branch): Try and handle parameterized constructors. (elab_check_def): Slightly improve message.

* src/unification.ml (unify_inductive): New function. (unify'): Use it.

- - - - - 25bb77ab by Stefan Monnier at 2019-09-26T20:51:26Z * lexp.ml (lexp): Typo

- - - - - 5c7f8365 by Stefan Monnier at 2019-09-26T20:52:00Z Merge remote-tracking branch 'refs/remotes/gitlab/master' into trunk

- - - - - 9455fa18 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Extract logging from util.ml

- - - - - c1458d9a by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Replace typer_unreachable exception with 'failwith'

- - - - - 82fa3593 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Refactor logging

- - - - - 51251f1f by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Add optional color to logging

- - - - - 2a2afc56 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print errors/warnings all at once, after compilation stops

- - - - - 09952ed7 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print the log in default context

- - - - - c02e28bc by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add an option to control the verbosity/logging level

- - - - - f41b8bb3 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Always print the log after evaluation

If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log.

- - - - - b948d4c9 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print test messages instead of logging them

- - - - - 8f676939 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add `run_repl` to start the REPL with a stream of lines

* src/REPL.ml (run_repl) : Add the `run_repl` function. `run_repl` takes a stream of lines as input, making it possible to call it from the tests.

* src/REPL.ml (guard_compilation) : Refactor out the exception guards into the `guard_compilation` function.

* src/typer.ml (main) : Move the entry point from REPL.ml to typer.ml, making it possible to use the functions from REPL.ml as a library for the test suite.

- - - - - 769e07cd by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Fix argument parsing for test executables

The option keywords for the `Arg` module do not need '=' (the equals sign) at the end, indeed, the syntax "keyword=arg" is explicitly supported by the library. This commit fixes the argument specifications as well as the command invocations in GNUmakefile.

- - - - - 9c0d043d by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add test case skipping

Test cases will need to be skipped sometimes. Indeed, with characterization tests, if a sample has no expected output yet, the output must be recorded (so the test case runs), but the result is neither OK or FAIL. The new third option SKIP covers this case.

- - - - - 544c86f1 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add characterization tests as a new section in the test suite

* GNUmakefile : Add a dependency on the `Unix` library.

* GNUmakefile : Add the target `characterize` to record and update the outputs of all the samples.

* src/util.ml : Add functions to handle files and line streams.

* tests/sample_test.ml : New file, does characterization testing.

- - - - - 3c5299b3 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add syntax error samples/characterization

- - - - - 15c84225 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z [WIP] There is an error with REPL input parsing

- - - - - 30685cb6 by Jean-Alexandre Barszcz at 2019-10-10T07:02:05Z [WIP] Add sample outputs

- - - - -

30 changed files:

- GNUmakefile - + samples/%.input - + samples/%.out - + samples/acc.out - + samples/array_test.out - + samples/autodiff.out - + samples/batch_test.out - + samples/bbst.out - + samples/bbst_test.out - + samples/bool.out - + samples/case_test.out - + samples/decltype.out - + samples/defmacro.out - + samples/defmacro.typer - + samples/dependent.out - + samples/do_test.out - + samples/elabctx_test.out - + samples/empty.out - + samples/error.out - + samples/hurkens.out - + samples/io.out - + samples/list_n.out - + samples/math.out - + samples/myers.out - + samples/myers_test.out - + samples/nat.out - + samples/pervasive.out - + samples/plain_let_test.out - + samples/polyfun_test.out - + samples/syntax_errors.input

The diff was not included because it is too large.

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