Jean-Alexandre Barszcz pushed to branch type-macro-improvements at Stefan / Typer

Commits: 8e1be507 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 Fix nix shell and dune details

- - - - - dc07e915 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Accept implicit type params.

Also, allow type definitions at other type levels than 0, with an annotation.

- - - - - b8d1df5b by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00 * btl/pervasive.typer (type-impl): Keep the constructors in order.

- - - - -

5 changed files:

- GNUmakefile - README.md - btl/pervasive.typer - shell.nix - tests/elab_test.ml

Changes:

===================================== GNUmakefile ===================================== @@ -9,7 +9,7 @@ DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG)) DUNE_PROFILE = dev # DUNE_PROFILE = release

-# Set COMPILE_MODE to native to build ocaml code with ocamlopt. +# Set COMPILE_MODE to `exe` for native builds. COMPILE_MODE ?= bc

# DEBUG ?= 1 @@ -28,7 +28,7 @@ debug: debug_util.$(COMPILE_MODE)

# interactive typer typer.$(COMPILE_MODE): - $(DUNE) --profile $(DUNE_PROFILE) build ./typer.$(COMPILE_MODE) + $(DUNE) build ./typer.$(COMPILE_MODE) --profile $(DUNE_PROFILE)

debug_util.$(COMPILE_MODE): $(DUNE) build ./debug_util.$(COMPILE_MODE) @@ -37,7 +37,7 @@ debug_util.$(COMPILE_MODE): # be confusing if you don't know Dune, so we pass the --force flag to rerun all # the tests no matter what. tests: - $(DUNE) --force test + $(DUNE) test --force

# There is nothing here. I use this to test if opam integration works install: tests

===================================== README.md ===================================== @@ -17,7 +17,7 @@ Status [] By default, Dune creates a '_build' folder which holds all the compiled files.

* `make typer`: build Typer interpreter (`./typer_cli.bc`). -* `COMPILE_MODE=native make typer`: build Typer interpreter (`./typer_cli.exe`). +* `COMPILE_MODE=exe make typer`: build Typer interpreter (`./typer_cli.exe`). * `make debug`: build typer with debug info (`./debug_util.bc`). * `make tests`: run interpreter's tests.

===================================== btl/pervasive.typer ===================================== @@ -308,17 +308,34 @@ type-impl = lambda (x : List Sexp) -> (lambda _ -> (nil : List Sexp)) % Float (lambda _ -> (nil : List Sexp)); % List of Sexp

- get-type : Sexp -> Sexp; - get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); + %% Takes an arrow type and a parameter (possibly named using + %% `:`/`::`/`:::`), and prepends the corresponding arrow + %% (`->`/`=>`/`≡>`) to the arrow type given as argument. + add-arg-arrow : Sexp -> Sexp -> Sexp; + add-arg-arrow arrow-type arg = + let default_arr = + Sexp_node (Sexp_symbol "_->_") (cons arg (cons arrow-type nil)) in + Sexp_dispatch arg + (lambda s ss -> + let single-colon-arg = + (Sexp_node (Sexp_symbol "_:_") + (cons (List_head Sexp_error ss) + (cons (List_nth 1 ss Sexp_error) nil))); + arrow-args = (cons single-colon-arg (cons arrow-type nil)) in + case (Sexp_eq s (Sexp_symbol "_:_")) + | true => Sexp_node (Sexp_symbol "_->_") arrow-args + | false => + (case (Sexp_eq s (Sexp_symbol "_::_")) + | true => Sexp_node (Sexp_symbol "_=>_") arrow-args + | false => + (case (Sexp_eq s (Sexp_symbol "_:::_")) + | true => Sexp_node (Sexp_symbol "_≡>_") arrow-args + | false => default_arr))) + (lambda _ -> default_arr) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error);

get-head = List_head Sexp_error;

@@ -328,24 +345,30 @@ type-impl = lambda (x : List Sexp) -> %% Expression is Sexp_node (Sexp_symbol "|") (list) %% we only care about the list bit lst = get-list expr; - - %% head is (Sexp_node type-name (arg list)) - name = get-head lst; ctor = List_tail lst;

- type-name = get-name name; + %% head+ is (Sexp_node type-name (arg list)), optionally wrapped + %% with a type annotation (<head> : Type_ l) + head+ = get-head lst; + + %% head-pair is a 2-list, which adds a default type annotation to head+ + head-pair = case Sexp_eq (get-name head+) (Sexp_symbol "_:_") + | true => get-list head+ + | false => cons head+ (cons (Sexp_symbol "Type") nil); + + head = List_nth 0 head-pair Sexp_error; + type-type = List_nth 1 head-pair Sexp_error; + type-name = get-name head; + type-args = get-list head;

%% Create the inductive type definition. inductive = Sexp_node (Sexp_symbol "typecons") - (cons name ctor); + (cons head ctor);

%% Declare the inductive type as a function %% Useful for recursive type - type-decl = quote ((uquote (get-name name)) : (uquote ( - (List_foldl (lambda args arg -> - Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) - %% FIXME: Don't hardcode TypeLevel.z! - (Sexp_symbol "Type") (List_reverse (get-args name) nil)) + type-decl = quote ((uquote type-name) : (uquote ( + (List_foldl add-arg-arrow type-type (List_reverse type-args nil)) )));

decl = make-decl type-name inductive; @@ -354,9 +377,8 @@ type-impl = lambda (x : List Sexp) -> ctors = let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => - let acc2 = chain-decl (make-cons (get-name hd) - type-name) - acc + let acc2 = chain-decl acc (make-cons (get-name hd) + type-name) in for-each tl acc2 | nil => acc in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)

===================================== shell.nix ===================================== @@ -3,7 +3,7 @@ pkgs.mkShell { name = "typer"; buildInputs = with pkgs.ocamlPackages; [ - pkgs.gnumake ocaml ocamlbuild findlib utop # tooling + pkgs.gnumake ocaml dune_2 findlib utop # tooling zarith # ocaml libraries merlin # for emacs ];

===================================== tests/elab_test.ml ===================================== @@ -217,4 +217,18 @@ test = (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true); |}

+let _ = add_elab_test_decl + "Implicit type parameters" + {| +type Not (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ + | mkNot ((contra : prop) -> False); + +type Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ + | yes (p ::: prop) + | no (p ::: Not prop); + +type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t) + | mkLift; + |} + let _ = run_all ()

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