Jean-Alexandre Barszcz pushed to branch instance-args at Stefan / Typer

Commits: f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00 Rewrite the Lexer module in terms of source objects.

This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects.

I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators.

- - - - - 8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00 Merge branch 'lexer-with-source'

- - - - - 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects.

These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise.

- - - - - a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given.

Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored.

- - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods'

- - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column.

- - - - - 87882dea by Simon Génier at 2021-09-28T17:45:35-04:00 Compute location inside the source from the given point.

- - - - - fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00 Upgrade to OCaml 4.11.

* Update the README * Remove a few functions that are now part of the standard library.

- - - - - 01e6295a by Simon Génier at 2021-09-29T11:09:53-04:00 Remove doc strings from Typer.

Doc strings are a good idea, but the implementation that was in Typer was not. They should not be hardcoded in the syntax of the langague, but rather a good implementation would use the metaprogramming capabilities of Typer to make them part of the standard library.

- - - - - 8cfa2243 by Simon Génier at 2021-09-30T11:39:27-04:00 Locations now track their end points.

- - - - - db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00 Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk

- - - - - 8efdff37 by Stefan Monnier at 2021-10-06T10:01:02-04:00 Merge remote-tracking branch 'gitlab/purge-docstr' into trunk

- - - - - 89cc2432 by Stefan Monnier at 2021-10-06T10:01:55-04:00 Merge remote-tracking branch 'gitlab/source-spans-2' into trunk

- - - - - f832b339 by Simon Génier at 2021-10-28T10:43:05-04:00 Remove artisanal formatting functions in favour of printf.

- - - - - 7f6f32dd by Simon Génier at 2021-10-28T10:43:38-04:00 Printfify log functions.

- - - - - edf888bc by Simon Génier at 2021-10-28T11:00:18-04:00 Typer accepts subcommands (repl, compile, run) like git.

This will hopefully simplify option handling as I add more modes of operation with their own option for running Typer code in a Gambit subprocess.

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

- - - - - 537ab8c3 by Jean-Alexandre Barszcz at 2022-02-16T13:49:48-05:00 * shell.nix : Set the Ocaml version to 4.11

- - - - - f89ed276 by Jean-Alexandre Barszcz at 2022-02-24T16:01:43-05:00 * src/opslexp.ml (lexp_whnf_aux): Add WHNF of Proj.

- - - - - ee155042 by Jean-Alexandre Barszcz at 2022-02-24T16:05:35-05: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.

- - - - - 649c82f3 by Jean-Alexandre Barszcz at 2022-02-24T16:10:43-05:00 * src/elab.ml: Handle sdforms in a common way.

- - - - - cd1735cd by Jean-Alexandre Barszcz at 2022-02-24T16:19:18-05:00 * src/debruijn.ml: Add a type class context to the elab context.

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

- - - - - ef4cb013 by Jean-Alexandre Barszcz at 2022-02-24T16:20:04-05:00 * tests/instargs_test.ml: New file, test the type class context.

- - - - - 51e2c2f1 by Jean-Alexandre Barszcz at 2022-02-24T16:29:35-05:00 * src/elab.ml: Save metavars' elaboration contexts for resolution.

* src/instargs.ml: Keep a table of resolution contexts for instance metavariables.

- - - - - fbcb99f4 by Jean-Alexandre Barszcz at 2022-02-24T16:40:23-05: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.

- - - - - 811bb343 by Jean-Alexandre Barszcz at 2022-02-24T16:43:00-05:00 * src/unification.ml (unify_call) : Return CKImpossible when we can.

- - - - - 17cb9524 by Jean-Alexandre Barszcz at 2022-02-24T17:02:11-05: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".

- - - - - f76b9510 by Jean-Alexandre Barszcz at 2022-02-24T17:02:20-05:00 Change integer literals to have type Integer by default

- - - - - f2c2fcf1 by Jean-Alexandre Barszcz at 2022-02-24T17:48:16-05:00 Make `do` polymorphic with a `Monad` class.

- - - - -

30 changed files:

- README.md - btl/builtins.typer - btl/case.typer - btl/do.typer - + btl/monads.typer - btl/pervasive.typer - + btl/poly-lits.typer - debug_util.ml - + samples/nats.typer - shell.nix - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - − src/float.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - + src/instargs.ml - − src/int.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml - src/log.ml

The diff was not included because it is too large.

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