Simon Génier pushed to branch impl-args-in-datacons at Stefan / Typer

Commits: 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case

A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.

This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.

Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.

- - - - - 115d8b01 by Simon Génier at 2020-09-09T12:06:50-04:00 Make eval tests throw on a compilation failure.

- - - - - e8257259 by Simon Génier at 2020-09-09T12:06:59-04:00 Remove commented eval test.

- - - - - 940ade63 by Simon Génier at 2020-09-09T12:06:59-04:00 Do not print callstack of test handler.

This line always print the same callstack, that of the handler, which gives no information about why the test failed.

- - - - - 53c514f5 by Simon Génier at 2020-09-09T12:06:59-04:00 Actually record the backtrace of exceptions while testing.

- - - - - e0d4964e by Simon Génier at 2020-09-09T12:06:59-04:00 Print compiler log on a compilation error in tests.

- - - - - e290b701 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix implicit arguments test.

- - - - - 5f740bf1 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix case test with generic types.

- - - - - b6466a2b by Simon Génier at 2020-09-09T12:07:23-04:00 Fix the rest of the eval tests.

- - - - - 2041b4dd by Simon Génier at 2020-09-09T12:07:34-04:00 Remove = at the end of the flags to the test driver.

I think the intention was to have GNU style flags like --verbose=3, but that does not even work.

- - - - - 56e4fbed by Simon Génier at 2020-09-09T13:24:41-04:00 Easier elaboration tests.

I extracted these changes from another branch since I will need them for yet another. Ther should make elaboration tests easier to write. * New assertions reduce the amount of code to check the results. * Correctly restore state to be able to compare metavariables in two different code fragments.

- - - - - 9d41029c by Simon Génier at 2020-09-09T13:24:48-04:00 Rework add_test to avoid warnings.

- - - - - 10c27014 by Simon Génier at 2020-09-09T13:24:48-04:00 Make success and failure values.

- - - - - 18f49df0 by Simon Génier at 2020-09-09T13:31:55-04:00 Make expected an optional argument in elaboration tests.

- - - - - b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test.

- - - - - a8e2af1a by Simon Génier at 2020-09-10T09:38:07-04:00 Oops: add back running tests in the order they were inserted.

- - - - - a4540d14 by Simon Génier at 2020-09-10T15:47:53-04:00 Merge changes to elaboration and evaluation tests.

- - - - - 4eac6264 by Simon Génier at 2020-09-10T16:05:31-04:00 Get rid of warning by using String.uppercase_ascii.

This function is available since 4.03, and 4.05 is now on Debian stable so it is safe to use.

- - - - - a5a05e7b by Simon Génier at 2020-09-11T17:22:08-04:00 Merge branch 'string-uppercase' into master.

- - - - - c34d6d0c by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Fix an issue in the unification of metavariables

The issue was that unification was not idempotent in certain cases. In particular, when unifying a metavar that has a non-identity substitution (let's say lxp1) with a term (let's say lxp2) that refers to some metavariables, the corresponding metavariable references in the associated term (thus in lxp1 after association) could have different substitutions from the same references in lxp2. See the added comment for a more detailed example.

- - - - - 023ea461 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - b4d53239 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make Eq.refl available to the ocaml code

* src/debruijn.ml : Add a definition of the lexp for Eq.refl

* src/builtin.ml : Register the constant Eq.refl

* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl instead of registering the builtin with the `Built-in` form. This ensures that we have the right variable and type, and might help to keep things in sync between the ocaml and typer code.

- - - - - efe2032d by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make the case elaboration code more consistent

This commit doesn't substantially change the behavior of the case elaboration, but makes the code a bit more consistent and might save some unnecessary metavariables in some cases.

- - - - - 4c632a1f by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Add dependent elimination

This commit changes elaboration, conversion, typechecking, erasure, and the computation of free variables and WHNFs for case expressions, to account for the fact that the context of all the branches of case expressions is extended with a proof of equality between the branch's head and the case's target. Careful elimination of this equality proof with Eq_cast makes dependent elimination possible.

- - - - - b082a329 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Conversion for metavariables

- - - - - fd990da1 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Case conversion

- - - - - eb1741eb by Simon Génier at 2020-09-16T09:21:42-04:00 Update the requirements for building typer.

* Add tools and libraries. * Bump OCaml version to the latest one on Debian stable.

- - - - - bcb53b2c by Simon Génier at 2020-09-16T09:21:42-04:00 Use Map.S.find_opt.

- - - - - b36d30ac by Simon Génier at 2020-09-16T09:21:42-04:00 Oops: fix broken tests on OCaml 4.05.0.

- - - - - 1fb4ed6c by Simon Génier at 2020-09-16T09:23:33-04:00 Merge branch 'update-requirements' into HEAD

- - - - - d3a9e581 by Jean-Alexandre Barszcz at 2020-09-25T22:26:59-04:00 * src/eval.ml: Add overflow checking to the Int builtin operators

* tests/eval_test.ml: Test that overflows cause runtime errors

- - - - - 7e07d97d by Jean-Alexandre Barszcz at 2020-09-25T22:33:21-04:00 * src/sexp.ml (sexp): Use Zarith's big integers in sexps.

* btl/builtins.typer: Add the builtin `Integer->Int`. * src/eval.ml: Implement it. (sexp_dispatch): Fix the value passed to the integer handler.

- - - - - 043275cd by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * btl/pervasive.typer (quote1): Fix quoting for literals

- - - - - 8a7b7910 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Add a macro for dependent elimination

* btl/depelim.typer: New file, implements the macro. * btl/pervasive.typer: Load the new macro. * tests/elab_test.ml: Test it.

- - - - - c722732e by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/unification.ml: Clarify the order of the handlers

Try and impose some logic on the order in which the various unification cases are handled.

(unify'): Shuffle. (unify_*): Simplify accordingly. (unify_call): Handle calls of different length.

* tests/unify_test.ml: Rewrite and enable the tests.

- - - - - ad090c1f by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/elab.ml (sform_lambda): Use unify instead of conv_p.

(unify_or_error): New function, extracted from check_inferred. (check_inferred): Use it.

- - - - - bc81cad7 by Jean-Alexandre Barszcz at 2020-11-05T14:13:57-05:00 * src/opslexp.ml (clean_map): Fix the erasure of Case expressions.

Substitute the erased variables in the branch bodies.

* tests/eval_test.ml: Test the fix.

- - - - - 9111345b by Jean-Alexandre Barszcz at 2020-11-05T14:15:56-05:00 * src/opslexp.ml: Name the substitute dummy used for erasure.

(erasure_dummy): The new dummy.

(erase_type, clean_default, clean_map): Use it.

- - - - - e04cd437 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * tests/utest_main.ml (main): Quote arguments to system commands.

This make it possible to focus on tests that have spaces in their title.

- - - - - 44b54d2a by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/opslexp.ml (erase_type): Fail for all (even erased) metavars.

* btl/builtins.typer (Eq_comm): Correct the FIXME.

- - - - - 98183f18 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (sform_load): Raise error when file is not found.

- - - - - eab5fa77 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (move_typelevel_to_front -> sort_generalized_metavars)

Replace `move_typelevel_to_front` with the new function `sort_generalized_metavars`, which, in addition to bringing the typelevel parameters to the front, sorts the remaining generalized metavariables topologically so that later variables can depend on ealier ones, and ignores metavariables that are in lower scope levels.

(generalize): Call the new function.

- - - - - 7bcbc61e by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/lexp.ml (hc_eq, eq): Catch exception from `List.for_all2`.

- - - - - bb33116e by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/elab.ml (sform_identifier): Add error in elab of metavars.

Add a FIXME and an internal error instead of using a wrong substitution in the elaboration of a repeated metavariable.

- - - - - 0b414a46 by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/opslexp.ml (eq_cast_whnf): New, adds WHNF for `Eq.cast`.

(lexp_whnf_aux): Add the reduction of calls to builtins, for registered builtins.

* tests/elab_test.ml: Test the WHNF of `Eq.cast`.

- - - - - 6666e7a2 by Simon Génier at 2020-11-29T11:41:01-05:00 Instantiate implicit arguments in datacons.

The datacons special form is datacons T C, where T is an (inductive) type and C is a symbol for one of its constructor. Before this commit, T has to syntactically be an inductive. This causes problems for types like Decidable, which is in fact not a Type, but a TypeLevel ≡> Type! Now, Typer tries to instanciate implicit arguments before deciding if something is a type or not. This currently only works for datacons, which is the only place I think it is a problem, but the same technique will work in other similar situations.

- - - - -

30 changed files:

- GNUmakefile - README.md - btl/builtins.typer - + btl/depelim.typer - btl/pervasive.typer - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/eval.ml - + src/float.ml - + src/int.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - + src/option.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml - tests/inverse_test.ml - tests/macro_test.ml - tests/sexp_test.ml - tests/unify_test.ml - tests/utest_lib.ml - tests/utest_main.ml

Changes:

===================================== GNUmakefile ===================================== @@ -69,7 +69,7 @@ tests-build: $(BUILDDIR)/tests/utests

tests-run: - @./$(BUILDDIR)/tests/utests --verbose= 3 + @./$(BUILDDIR)/tests/utests --verbose 3

test-file: $(OCAMLBUILD) src/test.$(COMPILE_MODE) -I src $(OBFLAGS) @@ -105,7 +105,7 @@ run/typer: @./$(BUILDDIR)/typer

run/tests: - @./$(BUILDDIR)/tests/utests --verbose= 1 + @./$(BUILDDIR)/tests/utests --verbose 1

run/typer-file: @./$(BUILDDIR)/typer ./samples/test__.typer

===================================== README.md ===================================== @@ -8,7 +8,11 @@ Status []

## Requirement

-* Ocaml 4.01 +* Ocaml 4.05 +* Ocamlfind +* Ocamlbuild +* Findlib +* Zarith

## Build

@@ -29,4 +33,3 @@ By default ocamlbuild creates a '_build' folder which holds all the compiled fil # Emacs files

/typer-mode.el -

===================================== btl/builtins.typer ===================================== @@ -48,7 +48,7 @@ Void = typecons Void; %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l Eq_refl : ((x : ?t) ≡> Eq x x); -Eq_refl = Built-in "Eq.refl"; +Eq_refl = ##Eq.refl;

Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) @@ -63,10 +63,11 @@ Eq_cast = Built-in "Eq.cast"; %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: The code is incorrectly accepted even without - %% this `(p := p)` because we just get a metavar which - %% remains uninstantiated and undetected (and then gets - %% throw away by erasure)! + %% FIXME: The code is incorrectly accepted even + %% without this `(p := p)` because we just get a + %% metavar which remains uninstantiated and then + %% the definition gets ignored in the runtime + %% environment (see Eval.from_lctx). (p := p) Eq_refl;

@@ -133,7 +134,15 @@ Int_>= = Built-in "Int.>=" : Int -> Int -> Bool; %% bitwise negation Int_not = Built-in "Int.not" : Int -> Int;

+%% `Int` and `Integer` are conceptually isomorphic in that they both +%% represent unbounded integers, but in reality, both are bounded. +%% `Int` is implemented with `int` type in ocaml (31 or 63 bits), and +%% `Integer` is implemented with big integers (ultimately limited by +%% available memory). Both cause runtime errors at their limits, so no +%% overflows are allowed. Here are the functions that witness the +%% isomorphism: Int->Integer = Built-in "Int->Integer" : Int -> Integer; +Integer->Int = Built-in "Integer->Int" : Integer -> Int;

Int->String = Built-in "Int->String" : Int -> String;

===================================== btl/depelim.typer ===================================== @@ -0,0 +1,110 @@ +%%% depelim --- A macro for dependent elimination + +%% Copyright (C) 2020 Free Software Foundation, Inc. +%% +%% Author: Jean-Alexandre Barszcz jean-alexandre.barszcz@umontreal.ca +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see http://www.gnu.org/licenses/. + +%%% Description +%% +%% In Typer, the branch bodies of a `case` expression must all have +%% the same type. In order to write proofs that depend the +%% constructor, Typer adds a proof in the environment of each branch: +%% the equality between the branch's head and the case target. This +%% equality can be eliminated in each branch using `Eq_cast` to go +%% from a branch-dependent type to a target-dependent type. The +%% following macro eases this process by eliminating the boilerplate. +%% +%% The macro extends the builtin `case` syntax to +%% `case_as_return_`. The `as` and `return` clauses are used to build +%% Eq_cast's `f` argument (a lambda). The `as` clause should contain a +%% symbol (the variable binding the case target or branch head), and +%% is optional if the target is itself a symbol. The `return` clause +%% is `f`'s body, i.e. the return type of the case, using the variable +%% from the `as` clause to refer to the target or branch head. + +%%% Example usage +%% +%% type Nat +%% | Z +%% | S Nat; +%% +%% Nat_induction : +%% (P : Nat -> Type_ ?l) ≡> +%% P Z -> +%% ((n : Nat) -> P n -> P (S n)) -> +%% ((n : Nat) -> P n); +%% Nat_induction base step n = +%% case n return (P n) %% <-- `as` clause omitted: the target is a var. +%% | Z => base +%% | S n' => (step n' (Nat_induction (P := P) base step n')); + +%%% Grammar +%% +%% This macro was written for the following operators (the precedence +%% level 42 is chosen to match that of the builtin case): +%% +%% define-operator "as" 42 42; +%% define-operator "return" 42 42; + +case_as_return_impl args = + let impl target_sexp var_sexp ret_and_branches_sexp = + case Sexp_wrap ret_and_branches_sexp + | node hd (cons ret_sexp branches) => + %% TODO Check that var_sexp is a variable. + %% TODO Check that hd is the symbol `_|_`. + let + on_branch branch_sexp = + case Sexp_wrap branch_sexp + | node arrow_sexp (cons head_sexp (cons body_sexp nil)) => + %% TODO Check that arrow_sexp is `=>`. + Sexp_node + arrow_sexp + (cons head_sexp + (cons (quote (##Eq.cast + (x := uquote head_sexp) + (y := uquote target_sexp) + (p := ##DeBruijn 0) + (f := lambda (uquote var_sexp) -> + uquote ret_sexp) + (uquote body_sexp))) + nil)) + | _ => Sexp_error; %% FIXME Improve error reporting. + new_branches = List_map on_branch branches; + in %% We extend the builtin case, so nested patterns don't work. + quote (##case_ + (uquote (Sexp_node (Sexp_symbol "_|_") + (cons target_sexp new_branches)))) + | _ => Sexp_error; + in IO_return + case args + | cons target_sexp + (cons var_sexp + (cons ret_and_branches_sexp nil)) + => impl target_sexp var_sexp ret_and_branches_sexp + | cons target_sexp + (cons ret_and_branches_sexp nil) + => %% If the `as` clause is omitted, and the target is a + %% symbol, use it for `var_sexp` as well. + (case Sexp_wrap target_sexp + | symbol _ => impl target_sexp target_sexp ret_and_branches_sexp + | _ => Sexp_error) + | _ => Sexp_error; + +case_as_return_ = macro case_as_return_impl; +case_return_ = macro case_as_return_impl;

===================================== btl/pervasive.typer ===================================== @@ -203,21 +203,31 @@ K x y = x; %% which will construct an Sexp equivalent to `x` at run-time. %% This is basically *cross stage persistence* for Sexp. quote1 : Sexp -> Sexp; -quote1 x = let k = K x; +quote1 x = let qlist : List Sexp -> Sexp; qlist xs = case xs | nil => Sexp_symbol "nil" | cons x xs => Sexp_node (Sexp_symbol "cons") (cons (quote1 x) (cons (qlist xs) nil)); + make_app str sexp = + Sexp_node (Sexp_symbol str) (cons sexp nil); + node op y = case (Sexp_eq op (Sexp_symbol "uquote")) | true => List_head Sexp_error y | false => Sexp_node (Sexp_symbol "##Sexp.node") (cons (quote1 op) (cons (qlist y) nil)); - symbol s = Sexp_node (Sexp_symbol "##Sexp.symbol") - (cons (Sexp_string s) nil) - in Sexp_dispatch x node symbol k k k k; + symbol s = make_app "##Sexp.symbol" (Sexp_string s); + string s = make_app "##Sexp.string" (Sexp_string s); + integer i = make_app "##Sexp.integer" + (make_app "##Int->Integer" (Sexp_integer i)); + float f = make_app "##Sexp.float" (Sexp_float f); + block sxp = + %% FIXME ##Sexp.block takes a string (and prelexes + %% it) but we have a sexp, what should we do? + Sexp_symbol "<error FIXME block quoting>"; + in Sexp_dispatch x node symbol string integer float block;

%% quote definition quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); @@ -634,6 +644,17 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;

+%% +%% case_as_return_, case_return_ +%% A `case` for dependent elimination +%% + +define-operator "as" 42 42; +define-operator "return" 42 42; +depelim = load "btl/depelim.typer"; +case_as_return_ = depelim.case_as_return_; +case_return_ = depelim.case_return_; + %%%% Unit tests function for doing file

%% It's hard to do a primitive which execute test file

===================================== src/builtin.ml ===================================== @@ -99,19 +99,6 @@ let dloc = DB.dloc let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, mkArrow (Anormal, (dloc, None), t, dloc, t))

-let type_eq = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - DB.type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) - let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

(* Typer list as seen during runtime. *) @@ -161,7 +148,9 @@ let register_builtin_csts () = add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string; - add_builtin_cst "Elab_Context" DB.type_elabctx + add_builtin_cst "Elab_Context" DB.type_elabctx; + add_builtin_cst "Eq" DB.type_eq; + add_builtin_cst "Eq.refl" DB.eq_refl

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in @@ -175,7 +164,6 @@ let register_builtin_types () = "Array" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in - let _ = new_builtin_type "Eq" type_eq in ()

let _ = register_builtin_csts ();

===================================== src/debruijn.ml ===================================== @@ -96,6 +96,37 @@ let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_eq_type = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 0), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 1), dloc, + mkSort (dloc, Stype (mkVar (lv, 3))))))) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let eq_refl = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + let xv = (dloc, Some "x") in + mkBuiltin ((dloc, "Eq.refl"), + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Aerasable, xv, + mkVar (tv, 0), dloc, + mkCall (type_eq, + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkVar (xv, 0); + Anormal, mkVar (xv, 0)])))), + None) +

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype)

===================================== src/debug.ml ===================================== @@ -90,7 +90,7 @@ let rec debug_sexp_print sexp = print_string """; print_string str; print_string """

| Integer(loc, n) - -> print_info "Integer: " loc; print_int n + -> print_info "Integer: " loc; Z.print n

| Float(loc, x) -> print_info "Float: " loc; print_float x

===================================== src/elab.ml ===================================== @@ -92,6 +92,9 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value)

+let whnf (lexp : lexp) (ectx : DB.elab_context) = + OL.lexp_whnf lexp (ectx_to_lctx ectx) + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -278,7 +281,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | [String (_, name); l; r] -> let level s = match s with | Symbol (_, "") -> None - | Integer (_, n) -> Some n + | Integer (_, n) -> Some (Z.to_int n) | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in let (grm, a, b, c) = ctx in (SMap.add name (level l, level r) grm, a, b, c) @@ -467,11 +470,11 @@ let rec meta_to_var ids (e : lexp) = -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, loop (o + List.length fields) e)) + -> (l, fields, loop (o + List.length fields + 1) e)) cases in mkCase (l, loop o e, loop o t, ncases, match default with None -> None - | Some (v, e) -> Some (v, loop (1 + o) e)) + | Some (v, e) -> Some (v, loop (2 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then mkVar (name, o + count - IMap.find id ids) @@ -480,16 +483,37 @@ let rec meta_to_var ids (e : lexp) = | _ -> mkMetavar (id, adjust_subst o s, name) in loop 0 e

-let move_typelevel_to_front ctx mfvs = - (* TypeLevel arguments have to come first, so move them accordingly. *) - List.sort - (fun (id1, vname1, mt1) (id2, vname2, mt2) - -> let tl1 = OL.conv_p ctx mt1 type_level in - let tl2 = OL.conv_p ctx mt2 type_level in - if tl1 - then if tl2 then 0 else -1 - else if tl2 then 1 else 0) - mfvs +let sort_generalized_metavars sl cl ctx mfvs = + (* TypeLevel parameters have to come first, and the metavariables + must be sorted topologically, so that the type of a parameter can + only refer to earlier parameters. + + We do a DFS through the metavariable types to sort them and we + store any TypeLevel argument in a separate list. *) + let rec handle_metavar id (sl', mt, cl', vname) (* The metavar *) + ((typelevels, (* The front of the list (in reverse) *) + params, (* The rest of the list (in reverse) *) + seen) (* The set of indices already added to the lists *) + as acc) = + if sl' < sl || (* This metavar appears in the context, so we can't + generalize over it. *) + (IMap.mem id seen) (* We've already handled this metavar, skip it. *) + then acc else + (assert (cl' >= cl); + let mt = if cl' > cl then + Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) + else mt in + let mv = (id, vname, mt) in + if (OL.conv_p ctx mt type_level) then + ((mv :: typelevels), params, (IMap.add id () seen)) + else + let (_, (mt_mfvs, _)) = OL.fv mt in + let (typelevels, params, seen) = handle_metavars mt_mfvs acc in + (typelevels, mv :: params, (IMap.add id () seen)) + ) + and handle_metavars ids acc = IMap.fold handle_metavar ids acc in + let (typelevels, params, _) = handle_metavars mfvs ([], [], IMap.empty) in + List.append (List.rev typelevels) (List.rev params)

(* Generalize expression `e` with respect to its uninstantiated metavars.. * `wrap` is the function that adds the relevant quantification, typically @@ -502,24 +526,9 @@ let generalize (nctx : elab_context) e = if mfvs = IMap.empty then (fun wrap e -> e) (* Nothing to generalize, yay! *) else - let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs - -> if sl' < sl then - (* This metavar appears in the context, - * so we can't generalize over it. *) - fvs - else ( - assert (cl' >= cl); - (idx, vname, - if cl' > cl then - Inverse_subst.apply_inv_subst - mt (S.shift (cl' - cl)) - else - mt) - :: fvs)) - mfvs [] in - (* FIXME: Sort `mvfs' topologically! *) + (* Sort `mvfs' topologically, and bring typelevel args to the front *) + let mfvs = sort_generalized_metavars sl cl (ectx_to_lctx nctx) mfvs in let len = List.length mfvs in - let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> let rec loop ids n mfvs = assert (n = IMap.cardinal ids); @@ -622,7 +631,9 @@ and get_implicit_arg ctx loc oname t = | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (loc, oname) t

-(* Build the list of implicit arguments to instantiate. *) +(** Given a value [e] of type [t], wrap [e] in applications of its implicit + arguments. Returns a pair of the wrapped [e] and the [t] stripped of its + implicit arguments *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with @@ -632,6 +643,18 @@ and instantiate_implicit e t ctx = | _ -> (mkCall (e, List.rev args), t) in instantiate t []

+(** Like {!instanciate_implicit}, but works on a value directly. Wraps an + implicit (or erasable implicit) λ with an application to its instanciated + argument *) +and instantiate_implicit_of_value value ctx = + let rec instantiate e = + match whnf e ctx with + | Lambda ((Aerasable | Aimplicit), (_, arg_name), arg_ty, body), _ + -> let arg = get_implicit_arg ctx (lexp_location e) arg_name arg_ty in + instantiate (mkSusp body (S.substitute arg)) + | _ -> whnf e ctx + in instantiate value + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -694,6 +717,22 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = | _ -> OL.get_type (ectx_to_lctx ctx) e in check_inferred ctx e inferred_t t

+and unify_or_error lctx lxp ?lxp_name expect actual = + match Unif.unify expect actual lctx with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lxp) lxp + ("Type mismatch" + ^ (match ck with | Unif.CKimpossible -> "" + | Unif.CKresidual -> " (residue)") + ^ "! Context expected:\n " ^ lexp_string expect ^ "\nbut " + ^ (U.option_default "expression" lxp_name) ^ " has type:\n " + ^ lexp_string actual ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p lctx expect actual)) + | [] -> () + (* This is a crucial function: take an expression `e` of type `inferred_t` * and convert it into something of type `t`. Currently the only conversion * we use is to instantiate implicit arguments when needed, but we could/should @@ -704,20 +743,7 @@ and check_inferred ctx e inferred_t t = | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in - (match Unif.unify inferred_t t (ectx_to_lctx ctx) with - | ((ck, _ctx, t1, t2)::_) - -> lexp_error (lexp_location e) e - ("Type mismatch(" - ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") - ^ ")! Context expected:\n " - ^ lexp_string t ^ "\nbut expression has type:\n " - ^ lexp_string inferred_t ^ "\ncan't unify:\n " - ^ lexp_string t1 - ^ "\nwith:\n " - ^ lexp_string t2); - assert (not (OL.conv_p (ectx_to_lctx ctx) inferred_t t)) - | [] -> ()); + unify_or_error (ectx_to_lctx ctx) e t inferred_t; e

(* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -736,20 +762,24 @@ and check_case rtype (loc, target, ppatterns) ctx =

(* get target and its type *) let tlxp, tltp = infer target ctx in + let tknd = OL.get_type (ectx_to_lctx ctx) tltp in + let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with + | Sort (_, Stype l) -> l + | _ -> fatal "Target lexp's kind is not a sort" in let it_cs_as = ref None in let ltarget = ref tlxp in

let get_cs_as it' lctor = + let unify_ind expected actual = + match Unif.unify actual expected (ectx_to_lctx ctx) with + | (_::_) + -> lexp_error loc lctor + ("Expected pattern of type `" ^ lexp_string expected + ^ "` but got `" ^ lexp_string actual ^ "`") + | [] -> () in match !it_cs_as with | Some (it, cs, args) - -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with - | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" - ^ lexp_string it ^ "` but got `" - ^ lexp_string it' ^ "`") - | [] -> () in - (cs, args) + -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) @@ -771,8 +801,9 @@ and check_case rtype (loc, target, ppatterns) ctx = | Call (f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in + unify_ind it it'; let constructors = - match OL.lexp'_whnf it (ectx_to_lctx ctx) with + match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -780,16 +811,36 @@ and check_case rtype (loc, target, ppatterns) ctx = ("Can't `case` on objects of this type: " ^ lexp_string tltp); SMap.empty in + it_cs_as := Some (it, constructors, targs); (constructors, targs) in

(* Read patterns one by one *) let fold_fun (lbranches, dflt) (pat, pexp) =

+ let shift_to_extended_ctx nctx lexp = + mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + + let ctx_extend_with_eq nctx head_lexp = + (* Add a proof of equality between the target and the branch + head to the context *) + let tlxp' = shift_to_extended_ctx nctx tlxp in + let tltp' = shift_to_extended_ctx nctx tltp in + let tlvl' = shift_to_extended_ctx nctx tlvl in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl'); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) + (Anormal, head_lexp); (* Lexp of the branch head *) + (Anormal, tlxp')]) (* Target lexp *) + in ctx_extend nctx (loc, None) Variable eqty + in + let add_default v = (if dflt != None then uniqueness_warn pat); let nctx = ctx_extend ctx v Variable tltp in - let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + let head_lexp = mkVar (v, 0) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in lbranches, Some (v, lexp) in

@@ -870,9 +921,15 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in - let rtype' = mkSusp rtype - (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + let head_lexp_ctor = + shift_to_extended_ctx nctx + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + let head_lexp_args = + List.mapi (fun i (ak, vname) -> + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt @@ -1467,12 +1524,14 @@ let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] -> let idt, _ = infer t ctx in - (mkCons (idt, sym), Lazy) - - | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; - sform_dummy_ret ctx loc - | _ -> sexp_error loc "##constr requires two arguments"; - sform_dummy_ret ctx loc + let idt = instantiate_implicit_of_value idt ctx in + mkCons (idt, sym), Lazy + | [_;_] + -> sexp_error loc "Second arg of ##datacons should be a symbol"; + sform_dummy_ret ctx loc + | _ + -> sexp_error loc "##datacons requires two arguments"; + sform_dummy_ret ctx loc

let elab_colon_to_ak k = match k with | "_:::_" -> Aerasable @@ -1609,7 +1668,22 @@ let sform_identifier ctx loc sargs ot = let subst = S.shift ctx_shift in let (_, _, rmmap) = ectx_get_scope ctx in if not (name = "") && SMap.mem name (!rmmap) then - (mkMetavar (SMap.find name (!rmmap), subst, (loc, Some name)), Lazy) + let idx = SMap.find name (!rmmap) in + match (metavar_lookup idx) with + | MVar (sl',_,_) + -> if sl = sl' then + (mkMetavar (idx, subst, (loc, Some name)), Lazy) + else + (* FIXME: The variable is from another scope_level! It + means that `subst` is not the right substitution for + the metavar! *) + fatal ~loc ("Bug in the elaboration of a metavar" + ^ " repeated at a different scope level!") + | MVal _ + -> (* FIXME: We face the same problem as above, but here, + the situation is worse, we don't even know the scope + level! *) + fatal ~loc "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1680,10 +1754,8 @@ let rec sform_lambda kind ctx loc sargs ot = -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); + -> unify_or_error (ectx_to_lctx ctx) lt1' + ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2)

| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal @@ -1772,7 +1844,7 @@ let sform_type ctx loc sargs ot = let sform_debruijn ctx loc sargs ot = match sargs with | [Integer (l,i)] - -> if i < 0 || i > get_size ctx then + -> let i = Z.to_int i in if i < 0 || i > get_size ctx then (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else @@ -1809,7 +1881,11 @@ let in_pervasive = ref true let sform_load usr_elctx loc sargs ot =

let read_file file_name elctx = - let pres = prelex_file file_name in + let pres = + try prelex_file file_name with + | Sys_error _ + -> error ~loc + ("Could not load `" ^ file_name ^ "`: file not found."); [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx in elctx in @@ -1945,21 +2021,19 @@ let default_rctx = EV.from_ectx default_ectx * --------------------------------------------------------- *)

let lexp_expr_str str ctx = - try let tenv = default_stt in - let grm = ectx_get_grammar ctx in - let limit = Some ";" in - let pxps = sexp_parse_str str tenv grm limit in - let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) - lexps; - lexps - with Log.Stop_Compilation s -> [] + let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let pxps = sexp_parse_str str tenv grm limit in + let lexps = lexp_parse_all pxps ctx in + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + lexps; + lexps

let lexp_decl_str str ctx = - try let tenv = default_stt in - let tokens = lex_str str tenv in - lexp_p_decls [] tokens ctx - with Log.Stop_Compilation s -> ([],ctx) + let tenv = default_stt in + let tokens = lex_str str tenv in + lexp_p_decls [] tokens ctx

(* Eval String @@ -1967,15 +2041,11 @@ let lexp_decl_str str ctx = (* Because we cant include Elab in eval.ml *)

let eval_expr_str str lctx rctx = - try let lxps = lexp_expr_str str lctx in - let elxps = List.map OL.erase_type lxps in - EV.eval_all elxps rctx false - with Log.Stop_Compilation s -> [] + let lxps = lexp_expr_str str lctx in + let elxps = List.map OL.erase_type lxps in + EV.eval_all elxps rctx false

let eval_decl_str str lctx rctx = - let prev_lctx, prev_rctx = lctx, rctx in - try - let lxps, lctx = lexp_decl_str str lctx in - let elxps = (List.map OL.clean_decls lxps) in - (EV.eval_decls_toplevel elxps rctx), lctx - with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) + let lxps, lctx = lexp_decl_str str lctx in + let elxps = List.map OL.clean_decls lxps in + (EV.eval_decls_toplevel elxps rctx), lctx

===================================== src/eval.ml ===================================== @@ -151,17 +151,68 @@ let add_binary_iop name f = | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in add_builtin_function name f 2

-let _ = add_binary_iop "+" (+); - add_binary_iop "-" (-); - add_binary_iop "*" ( * ); - add_binary_iop "/" (/); +let add_binary_iop_with_loc name f = + let name = "Int." ^ name in + let f loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint (v); Vint (w)] -> Vint (f loc v w) + | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in + add_builtin_function name f 2 + +let add_with_overflow loc a b = + let c = a + b in + (* Check that signs of both args are diff. OR sign of result is the + same as the sign of the args. *) + if (a lxor b) lor (a lxor (lnot c)) < 0 + then c + else error loc "Overflow in `Int.+`" + +let sub_with_overflow loc a b = + let c = a - b in + (* Check that signs of both args are the same OR sign of result is + the same as the sign of the first arg. *) + if (a lxor (lnot b)) lor (a lxor (lnot c)) < 0 + then c + else error loc "Overflow in `Int.-`" + +let mul_with_overflow loc a b = + let c = a * b in + if b = 0 || not (c = min_int && b = -1) && a = c / b (* Simple but slow *) + then c + else error loc "Overflow in `Int.*`" + +let div_with_overflow loc a b = + if not (a = min_int && b = -1) + then a / b + else error loc "Overflow in `Int./`" + +let lsl_with_shift_check loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsl`") + else a lsl b + +let lsr_with_shift_check loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsr`") + else a lsr b + +let asr_with_shift_check loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.asr`") + else a asr b + +let _ = add_binary_iop_with_loc "+" add_with_overflow; + add_binary_iop_with_loc "-" sub_with_overflow; + add_binary_iop_with_loc "*" mul_with_overflow; + add_binary_iop_with_loc "/" div_with_overflow; + + add_binary_iop_with_loc "lsl" lsl_with_shift_check; + add_binary_iop_with_loc "lsr" lsr_with_shift_check; + add_binary_iop_with_loc "asr" asr_with_shift_check;

add_binary_iop "mod" (mod); add_binary_iop "and" (land); - add_binary_iop "or" (lor); - add_binary_iop "lsl" (lsl); - add_binary_iop "lsr" (lsr); - add_binary_iop "asr"(asr); + add_binary_iop "or" (lor); add_binary_iop "xor" (lxor)

let add_binary_bool_iop name f = @@ -221,6 +272,16 @@ let _ = add_binary_bool_biop "<" BI.lt; -> match args_val with | [Vint v] -> Vinteger (BI.of_int v) | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) + 1; + let name = "Integer->Int" in + add_builtin_function + name + (fun loc (depth : eval_debug_info) (args_val: value_type list) + -> match args_val with + | [Vinteger v] -> + (try Vint (BI.to_int v) with + | Z.Overflow -> error loc ("Overflow in `" ^ name ^ "`")) + | _ -> error loc ("`" ^ name ^ "` expects 1 Integer argument")) 1

(* Floating point numers. *) @@ -283,7 +344,7 @@ let make_string loc depth args_val = match args_val with | _ -> error loc "Sexp.string expects one string as argument"

let make_integer loc depth args_val = match args_val with - | [Vinteger n] -> Vsexp (Integer (loc, BI.to_int n)) + | [Vinteger n] -> Vsexp (Integer (loc, n)) | _ -> error loc "Sexp.integer expects one integer as argument"

let make_float loc depth args_val = match args_val with @@ -373,7 +434,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) match lxp with (* Leafs *) (* ---------------- *) - | Imm(Integer (_, i)) -> Vint i + | Imm(Integer (_, i)) -> Vint (Z.to_int i) | Imm(String (_, s)) -> Vstring s | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp @@ -567,7 +628,7 @@ and sexp_dispatch loc depth args = | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] | Symbol (_ , s) -> eval_call sym [Vstring s] | String (_ , s) -> eval_call str [Vstring s] - | Integer (_ , i) -> eval_call it [Vint i] + | Integer (_ , i) -> eval_call it [Vinteger i] | Float (_ , f) -> eval_call flt [Vfloat f] | Block (_ , _, _) as b -> (* I think this code breaks what Blocks are. *) @@ -744,7 +805,7 @@ let constructor_p name ectx = with Senv_Lookup_Fail _ -> false

let erasable_p name nth ectx = - let is_erasable ctors = match (smap_find_opt name ctors) with + let is_erasable ctors = match (SMap.find_opt name ctors) with | (Some args) -> if (nth < (List.length args) && nth >= 0) then ( match (List.nth args nth) with @@ -763,7 +824,7 @@ let erasable_p name nth ectx =

let erasable_p2 t name ectx = let is_erasable ctors = - match (smap_find_opt t ctors) with + match (SMap.find_opt t ctors) with | Some args -> (List.exists (fun (k, oname, _) @@ -783,7 +844,7 @@ let erasable_p2 t name ectx = with Senv_Lookup_Fail _ -> false

let nth_ctor_arg name nth ectx = - let find_nth ctors = match (smap_find_opt name ctors) with + let find_nth ctors = match (SMap.find_opt name ctors) with | Some args -> (match (List.nth args nth) with | (_, (_, Some n), _) -> n @@ -805,7 +866,7 @@ let ctor_arg_pos name arg ectx = | [] -> None | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) | _::xs -> find_opt xs (n + 1) in - let find_arg ctors = match (smap_find_opt name ctors) with + let find_arg ctors = match (SMap.find_opt name ctors) with | (Some args) -> ( match (find_opt args 0) with | None -> (-1)

===================================== src/float.ml ===================================== @@ -0,0 +1,25 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +type t = float + +let equal (l : t) (r : t) : bool = l = r + +let compare (l : t) (r : t) : int = compare l r

===================================== src/int.ml ===================================== @@ -0,0 +1,25 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +type t = int + +let equal (l : t) (r : t) : bool = l = r + +let compare (l : t) (r : t) : int = compare l r

===================================== src/inverse_subst.ml ===================================== @@ -304,11 +304,12 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, apply_inv_subst e s')) + let s'' = ssink (l, None) s' in + (l, cargs, apply_inv_subst e s'')) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s))) + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) | Metavar (id, s', name) -> match metavar_lookup id with | MVal e -> apply_inv_subst (push_susp e s') s

===================================== src/lexer.ml ===================================== @@ -58,7 +58,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos if bp >= String.length name then ((if np == NPint then Integer ({file;line;column=column+cpos;docstr=docstr}, - int_of_string (string_sub name bpos bp)) + Z.of_string (string_sub name bpos bp)) else Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), @@ -75,7 +75,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | _ -> ((if np == NPint then Integer ({file;line;column=column+cpos;docstr=docstr}, - int_of_string (string_sub name bpos bp)) + Z.of_string (string_sub name bpos bp)) else Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))),

===================================== src/lexp.ml ===================================== @@ -252,7 +252,7 @@ let lexp'_hash (lp : lexp') = (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) let hc_eq e1 e2 = - match (lexp_lexp' e1, lexp_lexp' e2) with + try match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 @@ -294,6 +294,8 @@ let hc_eq e1 e2 = | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> i1 = i2 && compare s1 s2 = 0 | _ -> false + with + | Invalid_argument _ -> false (* Different lengths in List.for_all2. *)

module WHC = Weak.Make (struct type t = lexp let equal x y = hc_eq x y @@ -574,11 +576,11 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e s')) + (l, cargs, mkSusp e (ssink (l, None) s'))) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink v s))) + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -641,11 +643,12 @@ let clean e = -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, clean s' e)) + let s'' = ssink (l, None) s' in + (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink v s) e)) + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) @@ -961,7 +964,7 @@ and lexp_str ctx (exp : lexp) : string = match lexp_lexp' exp with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) - | Integer(_, s) -> tval (string_of_int s) + | Integer(_, s) -> tval (Z.to_string s) | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e)

@@ -1118,7 +1121,7 @@ and lexp_str_decls ctx decls = (** Syntactic equality (i.e. without β). *******)

let rec eq e1 e2 = - e1 == e2 || + try e1 == e2 || match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm s1, Imm s2) -> sexp_equal s1 s2 | (SortLevel SLz, SortLevel SLz) -> true @@ -1170,6 +1173,8 @@ let rec eq e1 e2 = | MVal l -> eq e1 (push_susp l s2) | _ -> false) | _ -> false + with + | Invalid_argument _ -> false (* Different lengths in List.for_all2. *)

and subst_eq s1 s2 = s1 == s2 ||

===================================== src/log.ml ===================================== @@ -47,7 +47,7 @@ let string_of_level lvl = | Debug -> "Debug"

let level_of_string str = - match Util.string_uppercase str with + match String.uppercase_ascii str with | "NOTHING" -> Nothing | "FATAL" -> Fatal | "ERROR" -> Error

===================================== src/opslexp.ml ===================================== @@ -38,10 +38,33 @@ module S = Subst (* module L = List *) module DB = Debruijn

+type set_plexp = (lexp * lexp) list +type sort_compose_result + = SortResult of ltype + | SortInvalid + | SortK1NotType + | SortK2NotType +type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t + (* Metavars that appear in non-erasable positions. *) + * unit IMap.t + +module LMap + (* Memoization table. FIXME: Ideally the keys should be "weak", but + * I haven't found any such functionality in OCaml's libs. *) + = Hashtbl.Make + (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) + +let reducible_builtins + = ref (SMap.empty : (DB.lexp_context + -> (P.arg_kind * lexp) list (* The builtin's args *) + -> lexp option) SMap.t) + let error_tc = Log.log_error ~section:"TC" let warning_tc = Log.log_warning ~section:"TC"

-(* `conv_erase` is supposed to be safe according to the ICC papers. *) +(* `conv_erase` is supposed to be safe according to the ICC papers. + It might be incompatible with the reduction of `Eq.cast`, though. See : + https://mailman.iro.umontreal.ca/pipermail/typer/2020-October/000870.html *) let conv_erase = true (* Makes conv ignore erased terms. *)

(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer @@ -133,8 +156,13 @@ let lexp_close lctx e = * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *)

-let lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +(* FIXME This large letrec closes the loop between lexp_whnf_aux and + get_type so that we can use get_type in the WHNF of a case to get + the inductive type of the target (and it's typelevel). A better + solution would be to add these values as annotations in the lexp + datatype. *) let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e @@ -154,33 +182,52 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Builtin ((_, name), _, _) + -> (match SMap.find_opt name (!reducible_builtins) with + | Some f -> U.option_default e (f ctx args) + | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf_aux e ctx in - let reduce name aargs = + let get_refl e = + let etype = get_type ctx e in (* FIXME we should not need get_type here *) + let elevel = match lexp'_whnf (get_type ctx etype) ctx with + | Sort (_, Stype l) -> l + | _ -> Log.internal_error "" in + mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + let reduce it name aargs = + let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive (_,_,fargs,_) -> fargs + | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left - (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf_aux arg ctx) (S.shift d)) s, - d + 1)) - (S.identity, 0) + (fun (s, targs) (_, arg) -> + match targs with + | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) + | _targ::targs -> + (* Ignore the type arguments *) + (s, targs)) + (S.identity, targs) aargs in + (* Substitute case Eq variable by the proof (Eq.refl l t e') *) + let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf_aux (push_susp default (S.substitute e')) ctx + -> let subst = S.cons (get_refl e') (S.substitute e') in + lexp_whnf_aux (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with - | Cons (_, (_, name)) -> reduce name [] + | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> (match lexp_lexp' (lexp_whnf_aux f ctx) with - | Cons (_, (_, name)) -> reduce name aargs + | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) @@ -197,29 +244,44 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =

in lexp_whnf_aux e ctx

-let lexp'_whnf e (ctx : DB.lexp_context) : lexp' = +and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = lexp_lexp' (lexp_whnf_aux e ctx)

-let lexp_whnf e (ctx : DB.lexp_context) : lexp = +and lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf_aux e ctx

+and eq_cast_whnf ctx args = + match args with + | [_l; _t; _x; _y; (_, p); _f; (_, fx)] + -> (match lexp'_whnf p ctx with + | Call (refl, _) when conv_p ctx refl DB.eq_refl + -> Some (lexp_whnf fx ctx) + | _ -> None) + | _ -> None + +and register_reducible_builtins () = + reducible_builtins := + List.fold_right + (fun (n, f) m -> SMap.add n f m) [ + ("Eq.cast", eq_cast_whnf) + ] !reducible_builtins + (** A very naive implementation of sets of pairs of lexps. *) -type set_plexp = (lexp * lexp) list -let set_empty : set_plexp = [] -let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool +and set_empty : set_plexp = [] +and set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool = try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s in true with Not_found -> false -let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp +and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp = (* assert (not (set_member_p s e1 e2)); *) ((e1, e2) :: s) -let set_shift_n (s : set_plexp) (n : U.db_offset) +and set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) s -let set_shift s : set_plexp = set_shift_n s 1 +and set_shift s : set_plexp = set_shift_n s 1

(********* Testing if two types are "convertible" aka "equivalent" *********)

@@ -229,7 +291,7 @@ let set_shift s : set_plexp = set_shift_n s 1 * `c` is the maximum "constant" level that occurs in `e` * and `m` maps variable indices to the maxmimum depth at which they were * found. *) -let level_canon e = +and level_canon e = let add_var_depth v d ((c,m) as acc) = let o = try IMap.find v m with Not_found -> -1 in if o < d then (c, IMap.add v d m) else acc in @@ -249,14 +311,14 @@ let level_canon e = | _ -> (max_int, m) in canon e 0 (0,IMap.empty)

-let level_leq (c1, m1) (c2, m2) = +and level_leq (c1, m1) (c2, m2) = c1 <= c2 && c1 != max_int && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) m1

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = +and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in e1' == e2' || @@ -324,19 +386,109 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 - (* I'm not sure to understand how to compare two Metavar * - * Should I do a `lookup`? Or is it that simple: *) - (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*) - (* FIXME: Various missing cases, such as Case. *) + | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) + -> (* FIXME The termination of this case conversion is very + fragile. Indeed, we recurse in all branches, bypassing any + termination condition. Checking syntactic equality as a + base case seems to be sufficient in simple cases, but it + is probably not enough in general. *) + eq e1' e2' || ( + conv_p target1 target2 && + conv_p r1 r2 && ( + (* Compare the branches *) + (* We can arbitrarily use target1 since target1 and target2 + are convertible *) + let target = target1 in + let etype = lexp_whnf (get_type ctx target) ctx in + let ekind = get_type ctx etype in + let elvl = match lexp'_whnf ekind ctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_fatal ~loc:(lexp_location ekind) + "Target lexp's kind is not a sort"; in + (* 1. Get the inductive for the field types *) + let it, aargs = match lexp_lexp' etype with + | Call (f, args) -> (f, args) + | _ -> (etype, []) in + (* 2. Build the substitution for the inductive arguments *) + let fargs, ctors = + (match lexp'_whnf it ctx with + | Inductive (_, _, fargs, constructors) + -> fargs, constructors + | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in + let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) + S.identity fargs aargs in + (* 3. Compare the branches *) + let ctx_extend_with_eq ctx subst hlxp = + let tlxp = mkSusp target subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, hlxp); (* Lexp of the branch head *) + (Anormal, tlxp)]) in (* Target lexp *) + DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + (* The map module doesn't have a function to compare two + maps with the key (which is needed to get the field types + from the inductive. Instead, we work with the lists of + associations. *) + (try + List.for_all2 (fun (l1, (_, fields1, e1)) (l2, (_, fields2, e2)) -> + l1 = l2 && + let fieldtypes = SMap.find l1 ctors in + let rec mkctx ctx args s i vdefs1 vdefs2 fieldtypes = + match vdefs1, vdefs2, fieldtypes with + | [], [], [] -> Some (ctx, List.rev args, s) + | (ak1, vdef1)::vdefs1, (ak2, vdef2)::vdefs2, + (ak', vdef', ftype)::fieldtypes + -> if ak1 = ak2 && ak2 = ak' then + mkctx + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) + ((ak1, (mkVar (vdef1, i)))::args) + (ssink vdef1 s) + (i - 1) + vdefs1 vdefs2 fieldtypes + else None + | _,_,_ -> None in + match mkctx ctx [] fargs_subst (List.length fields1) + fields1 fields2 fieldtypes with + | None -> false + | Some (nctx, args, _subst) -> + let offset = (List.length fields1) in + let subst = S.shift offset in + let eaargs = + List.map (fun (_, a) -> (P.Aerasable, a)) aargs in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), + eaargs)) subst in + let hlxp = mkCall (ctor, args) in + let nctx = ctx_extend_with_eq nctx subst hlxp in + conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 + ) (SMap.bindings cases1) (SMap.bindings cases2) + with + | Invalid_argument _ -> false (* If the lists have different length *) + ) + && (match (def1, def2) with + | (Some (v1, e1), Some (v2, e2)) -> + let nctx = DB.lctx_extend ctx v1 Variable etype in + let subst = S.shift 1 in + let hlxp = mkVar ((DB.dloc, None), 0) in + let nctx = ctx_extend_with_eq nctx subst hlxp in + conv_p' nctx (set_shift_n vs' 2) e1 e2 + | None, None -> true + | _, _ -> false))) + | (Metavar (id1,s1,_), Metavar (id2,s2,_)) when id1 == id2 -> + (* FIXME Should we use conversion on the terms of the + substitution instead of syntactic equality? *) + subst_eq s1 s2 | (_, _) -> false

-let conv_p (ctx : DB.lexp_context) e1 e2 +and conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2

(********* Testing if a lexp is properly typed *********)

-let rec mkSLlub ctx e1 e2 = +and mkSLlub ctx e1 e2 = let lwhnf1 = lexp_whnf e1 ctx in let lwhnf2 = lexp_whnf e2 ctx in match (lexp_lexp' lwhnf1, lexp_lexp' lwhnf2) with @@ -351,13 +503,7 @@ let rec mkSLlub ctx e1 e2 = else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

-type sort_compose_result - = SortResult of ltype - | SortInvalid - | SortK1NotType - | SortK2NotType - -let sort_compose ctx1 ctx2 l ak k1 k2 = +and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) let lwhnf1 = lexp'_whnf k1 ctx1 in @@ -397,11 +543,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType

-let dbset_push ak erased = +and dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased

-let nerased_let defs erased = +and nerased_let defs erased = (* Let bindings are not erasable, with the important exception of * let-bindings of the form `x = y` where `y` is an erasable var. * This exception is designed so that macros like `case` which need to @@ -427,7 +573,7 @@ let nerased_let defs erased = erased es

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check'' erased ctx e = +and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () @@ -602,7 +748,14 @@ let rec check'' erased ctx e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e) ctx in + let etype = lexp_whnf (check erased ctx e) ctx in + (* FIXME save the type in the case lexp instead of recomputing + it over and over again *) + let ekind = get_type ctx etype in + let elvl = match lexp'_whnf ekind ctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_error ~loc:(lexp_location ekind) + "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> @@ -616,27 +769,46 @@ let rec check'' erased ctx e = | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in + let ctx_extend_with_eq ctx subst hlxp nerased = + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, hlxp); (* Lexp of the branch head *) + (Anormal, tlxp)]) in (* Target lexp *) + (* The eq proof is erasable. *) + let nerased = dbset_push Aerasable nerased in + let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in + (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s vdefs fieldtypes = + let rec mkctx erased ctx s hlxp vdefs fieldtypes = match vdefs, fieldtypes with - | [], [] -> (erased, ctx) + | [], [] -> (erased, ctx, hlxp) (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (mkVar (vdef, 0)) - (S.mkShift s 1)) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; - (erased, ctx)) in - let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in + (erased, ctx, hlxp)) in + let hctor = + mkCall (mkCons (it, (l, name)), + List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in + let (nerased, nctx, hlxp) = + mkctx erased ctx s hctor vdefs fieldtypes in + let subst = S.shift (List.length vdefs) in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch (check nerased nctx branch) - (mkSusp ret (S.shift (List.length fieldtypes)))) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -644,8 +816,13 @@ let rec check'' erased ctx e = -> if diff <= 0 then warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - assert_type nctx d (check (DB.set_sink 1 erased) nctx d) - (mkSusp ret (S.shift 1)) + let nerased = DB.set_sink 1 erased in + let subst = S.shift 1 in + let hlxp = mkVar ((l, None), 0) in + let (nerased, nctx) = + ctx_extend_with_eq nctx subst hlxp nerased in + assert_type nctx d (check nerased nctx d) + (mkSusp ret (S.shift 2)) | None -> if diff > 0 then error_tc ~loc:l ("Non-exhaustive match: " @@ -691,24 +868,21 @@ let rec check'' erased ctx e = check erased ctx e | MVar (_, t, _) -> push_susp t s)

-let check' ctx e = +and check' ctx e = let res = check'' DB.set_empty ctx e in (Log.stop_on_error (); res)

-let check = check' +and check ctx e = check' ctx e

(** Compute the set of free (meta)variables. **)

-let rec list_union l1 l2 = match l1 with +and list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

-type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t - (* Metavars that appear in non-erasable positions. *) - * unit IMap.t -let mv_set_empty : mv_set = (IMap.empty, IMap.empty) -let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) -let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set +and mv_set_empty : mv_set = (IMap.empty, IMap.empty) +and mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) +and mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set = (IMap.merge (fun _m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 @@ -724,25 +898,19 @@ let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set Some ss1) ms1 ms2, IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2) -let mv_set_erase (ms, _nes) = (ms, IMap.empty) +and mv_set_erase (ms, _nes) = (ms, IMap.empty)

-module LMap - (* Memoization table. FIXME: Ideally the keys should be "weak", but - * I haven't found any such functionality in OCaml's libs. *) - = Hashtbl.Make - (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) -let fv_memo = LMap.create 1000 +and fv_memo = LMap.create 1000

-let fv_empty = (DB.set_empty, mv_set_empty) -let fv_union (fv1, mv1) (fv2, mv2) +and fv_empty = (DB.set_empty, mv_set_empty) +and fv_union (fv1, mv1) (fv2, mv2) = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) -let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) -let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) -let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs) +and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) +and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) +and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

-let rec fv (e : lexp) : (DB.set * mv_set) = - let fv' e = - match lexp_lexp' e with +and fv (e : lexp) : (DB.set * mv_set) = + let fv' e = match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty | SortLevel (SLsucc e) -> fv e @@ -794,9 +962,9 @@ let rec fv (e : lexp) : (DB.set * mv_set) = -> let s = fv_union (fv e) (fv_erase (fv t)) in let s = match def with | None -> s - | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in + | Some (_, e) -> fv_union s (fv_hoist 2 (fv e)) in SMap.fold (fun _ (_, fields, e) s - -> fv_union s (fv_hoist (List.length fields) (fv e))) + -> fv_union s (fv_hoist (List.length fields + 1) (fv e))) cases s | Metavar (id, s, name) -> (match metavar_lookup id with @@ -816,7 +984,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (** Finding the type of a expression. **) (* This should never signal any warning/error. *)

-let rec get_type ctx e = +and get_type ctx e = match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -919,8 +1087,18 @@ let rec get_type ctx e = | MVal e -> get_type ctx (push_susp e s) | MVar (_, t, _) -> push_susp t s)

+(* FIXME: Remove the mutual recursion between `lexp_whnf` and + `get_type`, and move this closer to the `lexp_whnf`. *) +let _ = register_reducible_builtins () + (*********** Type erasure, before evaluation. *****************)

+(* References to erasable bindings shouldn't appear in the bodies of + lexps that are being erased, but we need to adjust the debruijn + indices of other vars, hence we substitute erasable variables with + a dummy. *) +let erasure_dummy = DB.type0 + let rec erase_type (lxp: lexp): E.elexp = match lexp_lexp' lxp with | L.Imm(s) -> E.Imm(s) @@ -928,9 +1106,7 @@ let rec erase_type (lxp: lexp): E.elexp = | L.Var(v) -> E.Var(v) | L.Cons(_, s) -> E.Cons(s) | L.Lambda (P.Aerasable, _, _, body) -> - (* The var shouldn't appear in body, basically, but we need - * to adjust the debruijn indices of other vars, hence the subst. *) - erase_type (L.push_susp body (S.substitute DB.type0)) + erase_type (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, _, body) -> E.Lambda (vdef, erase_type body)

@@ -942,7 +1118,7 @@ let rec erase_type (lxp: lexp): E.elexp =

| L.Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), - (clean_maybe default)) + (clean_default default))

| L.Susp(l, s) -> erase_type (L.push_susp l s)

@@ -971,25 +1147,43 @@ and filter_arg_list lst = and clean_decls decls = List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls

-and clean_maybe lxp = - match lxp with - | Some (v, lxp) -> Some (v, erase_type lxp) - | None -> None +and clean_default lxp = + match lxp with + | Some (v, lxp) -> + Some (v, + erase_type (L.push_susp lxp (S.substitute erasure_dummy))) + | None -> None

and clean_map cases = - let clean_arg_list lst = - let rec clean_arg_list lst acc = - match lst with - | (kind, var)::tl -> - let acc = if kind != P.Aerasable then - var::acc else acc in - clean_arg_list tl acc - | [] -> List.rev acc in - clean_arg_list lst [] in - - SMap.map (fun (l, args, expr) - -> (l, (clean_arg_list args), (erase_type expr))) - cases + let clean_branch (l, args, expr) = + let rec clean_arg_list args acc subst = + match args with + | (P.Aerasable, _)::tl -> + (* Drop the variable and substitute it in the body. *) + clean_arg_list tl acc (S.cons erasure_dummy subst) + | (kind, var)::tl -> + (* Keep the variable and sink the substitution. *) + clean_arg_list tl (var::acc) (ssink var subst) + | [] -> + (List.rev acc, subst) in + let args, subst = clean_arg_list args [] S.identity in + let subst = (S.cons erasure_dummy subst) in (* Substitute the equality. *) + (l, args, erase_type (L.push_susp expr subst)) in + SMap.map clean_branch cases + +let erase_type lxp = + let _, (mvs, _) = fv lxp in + if not (IMap.is_empty mvs) then + Log.log_fatal + ~print_action:(fun () -> + IMap.iter (fun i (_, t, _, (l, n)) -> + print_endline ("\t" ^ (Log.string_of_location l) + ^ " ?" ^ (U.option_default "" n) + ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) + ) mvs) + ("Metavariables in erase_type :"); + erase_type lxp +

(** Turning a set of declarations into an object. **)

===================================== src/option.ml ===================================== @@ -0,0 +1,27 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +type 'a t = 'a option + +let equal (inner_equal : 'a -> 'a -> bool) (l : 'a t) (r : 'a t) : bool = + match l, r with + | Some l, Some r -> inner_equal l r + | None, None -> true + | _ -> false

===================================== src/sexp.ml ===================================== @@ -27,16 +27,13 @@ open Grammar let sexp_error ?print_action loc msg = Log.log_error ~section:"SEXP" ?print_action ~loc msg

-type integer = (* Num.num *) int +type integer = Z.t type symbol = location * string

type sexp = (* Syntactic expression, kind of like Lisp. *) | Block of location * pretoken list * location | Symbol of symbol | String of location * string - (* FIXME: It would make a lof of sense to use a bigint here, but `compare` - * burps on Big_int objects, and `compare` is used for hash-consing of lexp - * objects which contain sexp objects as well. *) | Integer of location * integer | Float of location * float | Node of sexp * sexp list @@ -76,7 +73,7 @@ let rec sexp_string sexp = | Symbol(_, "") -> "()" (* Epsilon *) | Symbol(_, name) -> name | String(_, str) -> """ ^ str ^ """ - | Integer(_, n) -> string_of_int n + | Integer(_, n) -> Z.to_string n | Float(_, x) -> string_of_float x | Node(f, args) -> let str = "(" ^ (sexp_string f) in

===================================== src/unification.ml ===================================== @@ -171,10 +171,27 @@ let rec s_offset s = match s with

(** Dispatch to the right unifier.

- If (<code>unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) - - The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) -*) + Unification has the side-effect of associating the metavariables + in a way that makes the Lexp arguments convertible, if possible. In + case of success, it returns the empty list. Otherwise, it returns + the cause of failure as a list of constraints of the following + kinds: + + 1. `CKimpossible` constraints: constraints that cannot be + satisfied, even if other metavars are associated, redexes are + reduced, and subtitutions are done. For example, an arrow could + never be unified with a lambda. + + 2. `CKresidual` constraints: pairs of subterms that cannot be + unified in the current context, but might eventually be sucessfully + unifiable. For instance, a pair of different variables cannot be + unified, unless another reduction eventually substitutes one for + the other. As another example, a metavariable could be used in the + head position of a call, blocking its reduction, but a later + instanciation might turn this metavariable into a lambda, thus + yielding a redex, possibly reducing the call to a term unifiable + with the other argument. + *) let rec unify (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = @@ -191,28 +208,45 @@ and unify' (e1: lexp) (e2: lexp) if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (lexp_lexp' e1', lexp_lexp' e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + (* Both expressions are in WHNF: we don't have `Let`s nor `Susp`s. *) + + (* First, we handle the simple cases with no substructure. *) + | ((Imm _ | Builtin _), (Imm _ | Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] + + (* Then, we handle metavariables (aka. flexible-flexible and + Flexible-Rigid Equations). Reminder: WHNF implies that the + metavariables are not already instanciated. *) | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' - | (_, Call _) -> unify_call e2' e1' ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ , _) -> unify_arrow e1' e2' ctx vs' - | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' - | (Call _, _) -> unify_call e1' e2' ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _, _) -> unify_sort e1' e2' ctx vs' - | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> (* print_string ("Unifying inductives " - * ^ snd label1 - * ^ " and " - * ^ snd label2 - * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + + (* Otherwise, the equation is rigid-rigid. Let's start with the + cases that can leave residuals: 1. Variables, since they could + be substituted with further reduction; 2. Calls, because they + might become redexes; 3. Case expressions, for the same + reason. *) + | (_, Var _) -> unify_var e2' e1' ctx vs' + | (Var _, _) -> unify_var e1' e2' ctx vs' + | (_, Call _) -> unify_call e2' e1' ctx vs' + | (Call _, _) -> unify_call e1' e2' ctx vs' + (* FIXME: Handle `Case` expressions. *) + + (* We are left with the cases that are not affected by + substitutions, thus should not immediately lead to residual + constraints. *) + | (_, Arrow _) -> unify_arrow e2' e1' ctx vs' + | (Arrow _, _) -> unify_arrow e1' e2' ctx vs' + | (_, Lambda _) -> unify_lambda e2' e1' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (_, Sort _) -> unify_sort e2' e1' ctx vs' + | (Sort _, _) -> unify_sort e1' e2' ctx vs' + | (_, SortLevel _) -> unify_sortlvl e2' e1' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' + | (_, Inductive _) -> unify_inductive e2' e1' ctx vs' + | (Inductive _, _) -> unify_inductive e1' e2' ctx vs' + | (_, Cons _) -> unify_cons e2' e1' ctx vs' + | (Cons _, _) -> unify_cons e1' e2' ctx vs' + | _ -> (if OL.conv_p ctx e1' e2' then [] else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) @@ -223,7 +257,6 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - - (Arrow, Var) -> Constraint - (_, _) -> None *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @@ -236,19 +269,13 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) - else [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs + else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

(** Unify a Lambda and a lexp if possible - - Lamda , Lambda -> if var_kind = var_kind + - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , Var -> CONSTRAINT - - Lambda , Call -> Constraint - - Lambda , Let -> Constraint - - Lambda , lexp -> unify lexp lambda subst + - Lambda , _ -> Impossible *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' lambda, lexp_lexp' lxp) with @@ -260,19 +287,12 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, lambda, lxp)] - | ((Lambda _, Var _) - | (Lambda _, Let _) - | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] - | (Lambda _, Arrow _) - | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] - | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible - - lexp , {metavar <-> none} -> UNIFY - - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - - metavar , metavar -> if Metavar = Metavar then OK else ERROR - - metavar , lexp -> OK + - metavar , metavar -> if Metavar = Metavar then intersect + - metavar , metavar -> inverse subst (try both sides) + - metavar , lexp -> inverse subst *) and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = @@ -291,16 +311,35 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' -> metavar_table := associate idx lxp' (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)] in + let type_unif_residue = + match unify t (OL.get_type ctx lxp) ctx with + | [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)] in + (* FIXME Here, we unify lxp1 with lxp2 again, because that + the metavariables occuring in the associated term might + have different substitutions from the corresponding + metavariables on the other side (due to subst inversion + not being a perfect inverse of subtitution application). + + For example, when unifying `?τ↑1[114]` with `(List[56] + ?ℓ↑0[117] ?a↑0[118])`, we associate the metavar ?τ[114] + with the lexp `(List[55] ?ℓ() · ↑0[117] ?a() · ↑0[118])` + (after applying the inverse substitution of ↑1), and the + lexp (?τ↑1[114]) becomes `(List[56] ?ℓ(↑1 () · ↑0)[117] + ?a(↑1 () · ↑0)[118])`, which is not exactly the same as + the right-hand side. My solution/kludge to this problem is + to do a second unification to fix the metavar + substitutions on the right-hand side, but there is + probably a cleaner way to solve this. *) + let second_unif_residue = unify lxp1 lxp2 ctx in + List.append type_unif_residue second_unif_residue in match lexp_lexp' lxp2 with | Metavar (idx2, s2, name) -> if idx = idx2 then @@ -365,6 +404,16 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> unif idx2 s2 lxp1) | _ -> unif idx s1 lxp2

+(** Unify a Var (var) and a lexp (lxp) + - Var , Var -> IF same var THEN ok ELSE constraint + - Var , lexp -> Constraint +*) +and unify_var (var: lexp) (lxp: lexp) ctx vs + : return_type = + match (lexp_lexp' var, lexp_lexp' lxp) with + | (Var _, Var _) when OL.conv_p ctx var lxp -> [] + | (_, _) -> [(CKresidual, ctx, var, lxp)] + (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT @@ -374,13 +423,15 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs match (lexp_lexp' call, lexp_lexp' lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right - -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) + -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then (unify' e1 e2 ctx vs)@op else [(CKimpossible, ctx, call, lxp)]) [] (List.combine lxp_list1 lxp_list2) - | (_, _) -> [(CKresidual, ctx, call, lxp)] + with Invalid_argument _ (* Lists of diff. length in combine. *) + -> [(CKresidual, ctx, call, lxp)]) + | (_, _) -> [(CKresidual, ctx, call, lxp)]

(** Unify a Case with a lexp - Case, Case -> try to unify @@ -449,11 +500,10 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) - | _, _ -> [(CKresidual, ctx, sortlvl, lxp)] + | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]

(** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR - - Sort, Var -> Constraint - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = @@ -463,8 +513,7 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) - | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] - | _, _ -> [(CKimpossible, ctx, sort_, lxp)] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)]

(************************ Helper function ************************************)

@@ -514,7 +563,14 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive lxp1 lxp2 ctx vs = + match lexp_lexp' lxp1, lexp_lexp' lxp2 with + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)] + +and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -559,3 +615,8 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = * | _, _ -> None * in test l1 l2 subst *)

+and unify_cons lxp1 lxp2 ctx vs = + match lexp_lexp' lxp1, lexp_lexp' lxp2 with + | (Cons (it1, (_, l1)), Cons (it2, (_, l2))) when l1 = l2 + -> unify' it1 it2 ctx vs + | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]

===================================== src/util.ml ===================================== @@ -1,6 +1,6 @@ (* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -20,12 +20,21 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-module SMap = Map.Make (String) -(* Apparently OCaml-4.02 doesn't have find_opt and Debian stable still - * uses 4.02. *) -let smap_find_opt s m = try Some (SMap.find s m) with Not_found -> None +(** Adds the update function to maps. This can be removed when we upgrade to + OCaml >= 4.06 *) +module UPDATABLE(Base : Map.S) = struct + include Base

-module IMap = Map.Make (struct type t = int let compare = compare end) + let update key f map = + let before = find_opt key map in + match before, f before with + | _, Some after -> add key after map + | Some before, None -> remove key map + | None, None -> map +end + +module SMap = UPDATABLE(Map.Make(String)) +module IMap = UPDATABLE(Map.Make(Int))

type charpos = int type bytepos = int @@ -63,10 +72,6 @@ let loc_print loc = print_string (loc_string loc) let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b)

-(* `String.uppercase` is deprecated since OCaml-4.03, but the replacement - * `String.uppercase_ascii` is not yet available in Debian stable's `ocaml`. *) -let string_uppercase s = String.uppercase s - let opt_map f x = match x with None -> None | Some x -> Some (f x)

let str_split str sep =

===================================== tests/elab_test.ml ===================================== @@ -1,4 +1,4 @@ -(* elab_test.ml --- +(* elab_test.ml --- * * Copyright (C) 2016-2017 Free Software Foundation, Inc. * @@ -21,120 +21,205 @@ * * -------------------------------------------------------------------------- *)

- open Utest_lib

-open Pexp -open Lexp - -open Builtin - -let test - (input_gen: (unit -> 'a list)) - (fmt: 'b list -> string list) - (tester: 'a -> ('b * bool)): (string * bool) list = - let input = List.map tester (input_gen ()) - in let str = List.map (fun (s, _) -> s ) input - in let b = List.map (fun (_, b) -> b) input - in List.combine (fmt str) b - -let generate_tests (name: string) - (input_gen: (unit -> 'a list)) - (fmt: 'b list -> string list) - (tester: 'a -> ('b * bool)) = - let idx = (ref 0) - in List.map (fun (sub, res) -> - idx := !idx + 1; - add_test name - ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) - (fun () -> if res then success () else failure ())) - (test input_gen fmt tester) - -(* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3;" - -let generate_lexp_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, lxp, _) -> lxp)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let _ = generate_tests - "TYPECHECK" - (fun () -> [generate_lexp_from_str input]) - (fun x -> List.map lexp_string x) - (fun x -> (x, true)) - -let lctx = Elab.default_ectx -(* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () -> - * - * let dcode = " - * sqr = lambda (x) -> x * x; - * cube = lambda (x) -> x * (sqr x); - * - * mult = lambda (x) -> lambda (y) -> x * y; - * - * twice = (mult 2); - * - * let_fun = lambda (x) -> - * let a = (twice x); b = (mult 2 x); in - * a + b;" in - * - * let ret1, _ = lexp_decl_str dcode lctx in - * - * let to_str decls = - * let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in - * List.fold_left (fun str lxp -> str ^ lxp) "" str in - * - * (* Cast to string *) - * let str1 = to_str ret1 in - * - * print_string str1; - * - * (* read code again *) - * let ret2, _ = lexp_decl_str str1 lctx in - * - * (* Cast to string *) - * let str2 = to_str ret2 in - * - * if str1 = str2 then success () else failure () - * )) *) - -(* -let set_to_list s = - StringSet.fold (fun g a -> g::a) s [] - -let _ = (add_test "LEXP" "Free Variable" (fun () -> - - let dcode = " - a = 2; - b = 3; - f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b are fv - " in - - let ret = pexp_decl_str dcode in - let g = match List.rev ret with - | (_, g, _)::_ -> g - | _ -> raise (Unexpected_result "Unexpected empty list") in - - let (bound, free) = free_variable g in - - let bound = set_to_list bound in - let (free, _) = free in - - match bound with - | ["x"] ->( - match free with - | ["_+_"; "f"; "b"; "a"] -> success () - | _ -> failure ()) - | _ -> failure () - -)) *) - -(* run all tests *) -let _ = run_all () +let add_elab_test elab test name ?(setup="") ?(expected="") input = + let run_elab_test () = + let ectx = Elab.default_ectx in + let _, ectx = Elab.lexp_decl_str setup ectx in + let last_metavar = !Unification.global_last_metavar in + let actual, _ = elab input ectx in + if String.equal expected "" + then success + else + (Unification.global_last_metavar := last_metavar; + let expected, _ = elab expected ectx in + test actual expected) + in + add_test "ELAB" name run_elab_test + +(** Run setup, then elaborate [input]. Succeeds if there are no compilation + errors and [expected] elaborates to the same lexp, if provided. *) +let add_elab_test_expr = + add_elab_test (fun s ctx -> Elab.lexp_expr_str s ctx, ctx) expect_equal_lexps + +(** Like {!add_elab_test_expr}, but elaborates [input] and [expected] as top + level declarations instead of expressions. *) +let add_elab_test_decl = + add_elab_test Elab.lexp_decl_str expect_equal_decls + +let _ = add_elab_test_expr + "Instanciate implicit arguments" + ~setup:{| +f : (i : Int) -> Eq i i -> Int; +f = lambda i -> lambda eq -> i; + |} + ~expected:"f 4 (Eq_refl (x := 4));" + "f 4 Eq_refl;" + +let _ = add_elab_test_decl + "Whnf of case" + {| +Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); +box = (datacons Box box); +unbox b = ##case_ (b | box inside => inside); +alwaysbool b = ##case_ (b | box _ => Bool); + +example1 : unbox (box (lambda x -> Bool)) 1; +example1 = true; + +example2 : alwaysbool (box Int); +example2 = true; + |} + +let _ = add_elab_test_decl + "depelim with Nats" + {| +type Nat + | Z + | S Nat; + +Nat_induction : + (P : Nat -> Type_ ?l) ≡> + P Z -> + ((n : Nat) -> P n -> P (S n)) -> + ((n : Nat) -> P n); +Nat_induction base step n = + ##case_ (n + | Z => Eq_cast (p := ##DeBruijn 0) (f := P) base + | S n' => Eq_cast (p := ##DeBruijn 0) (f := P) (step n' (Nat_induction (P := P) base step n'))); + +plus : Nat -> Nat -> Nat; +plus x y = + case x + | Z => y + | S x' => S (plus x' y); + ++0_identity : (n : Nat) -> Eq (plus n Z) n; ++0_identity = + Nat_induction + (P := (lambda n -> Eq (plus n Z) n)) + Eq_refl + (lambda n-1 n-1+0=n-1 -> + Eq_cast + (p := n-1+0=n-1) + (f := lambda n-1_n -> Eq (S (plus n-1 Z)) (S n-1_n)) + Eq_refl); + |} + +let _ = add_elab_test_decl + "depelim macro" + {| +type Nat + | Z + | S Nat; + +Nat_induction : + (P : Nat -> Type_ ?l) ≡> + P Z -> + ((n : Nat) -> P n -> P (S n)) -> + ((n : Nat) -> P n); +Nat_induction base step n = + case n return (P n) + | Z => base + | S n' => (step n' (Nat_induction (P := P) base step n')); + |} + +let _ = add_elab_test_decl + "case conversion" + {| +unify = + macro ( + lambda sxps -> + do {vname <- gensym (); + IO_return + (quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "##Eq") sxps)); + (uquote vname) = Eq_refl; + )); + }); + +case_ = ##case_; + +type Nat + | S Nat + | Z; + +plus : ?; +plus x y = + case x + | Z => y + | S n => S (plus n y); + +f x y b = + case b + | true => plus x y + | false => Z; + +unify (f Z (S Z)) (f (S Z) Z); + |} + +let _ = add_elab_test_decl + "WHNF of Eq.cast" + {| +x = (4 : Int); +y = x; + +p : Eq x y; +p = Eq_refl; + +test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); +test = Eq_refl; + |} + +let _ = add_elab_test_decl + "Decidable at the type level" + {| +Decidable = + typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) + (yes (p :: prop)) (no (p :: Not prop)); +yes = datacons Decidable yes; +no = datacons Decidable no; + +true≠false (p : Eq true false) = + Eq_cast (p := p) + (f := lambda tf -> case tf + | true => True + | false => False) + (); % This is unit, an inhabitant of `True`. + +false≠true (p : Eq false true) = true≠false (Eq_comm p); + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case a return (Decidable (Eq a b)) + | true => + (case b return (Decidable (Eq true b)) + | true => yes (p := Eq_refl) + | false => no (p := true≠false)) + | false => + (case b return (Decidable (Eq false b)) + | true => no (p := false≠true) + | false => yes (p := Eq_refl)); + +getProof : + (l : TypeLevel) ≡> + (prop : Type_ l) ≡> + (d : Decidable prop) -> + case d | yes => prop | no => Not prop; +getProof d = + case d return (case d | yes => prop | no => Not prop) + | yes (p := p) => p + | no (p := p) => p; + +test = + (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true); + |} + +let _ = add_elab_test_expr + "Instanciate implicit arguments in datacons" + ~setup:"A = typecons (A (prop : Type_ ?ℓ)) (c (p ::: prop));" + ~expected:"datacons (A (ℓ := ?ℓ)) c" + "datacons A c"

let _ = run_all ()

===================================== tests/env_test.ml ===================================== @@ -67,14 +67,8 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> (ctx, idx - 1)) (rctx, n) var in

- print_rte_ctx rctx; - - success () - ) - else - success () - -)) + print_rte_ctx rctx); + success))

(* run all tests *)

===================================== tests/eval_test.ml ===================================== @@ -52,15 +52,7 @@ let test_eval_eqv_named name decl run res = let erun = Elab.eval_expr_str run ectx rctx in (* evaluated run expr *) let eres = Elab.eval_expr_str res ectx rctx in (* evaluated res expr *)

- if value_eq_list erun eres - then success () - else ( - (* List.hd was throwing when run or res failed to compile *) - (match erun with x::_ -> value_print x - | _ -> print_string ("no run expression\n")); - (match eres with x::_ -> value_print x - | _ -> print_string ("no result expression\n")); - failure ())) + expect_equal_values erun eres)

let test_eval_eqv decl run res = test_eval_eqv_named run decl run res

@@ -276,21 +268,6 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv "w = 2" "decltype w" "Int" let _ = test_eval_eqv "w = 2" "declexpr w" "2"

-(* let attr_decl = " - * w = 2; - * greater-than = new-attribute (Int -> Int); - * greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" - * - * let _ = test_eval_eqv_named - * "has-attribute" - * - * attr_decl - * - * "has-attribute greater-than w; - * (get-attribute greater-than w) 3;" - * - * "true; 3" *) - let _ = (add_test "EVAL" "Monads" (fun () ->

let dcode = " @@ -304,10 +281,9 @@ let _ = (add_test "EVAL" "Monads" (fun () ->

(* Eval defined lambda *) let ret = Elab.eval_expr_str rcode ectx rctx in - match ret with - | [v] -> success () - | _ -> failure () -)) + match ret with + | [v] -> success + | _ -> failure))

let _ = test_eval_eqv_named "Argument Reordering" @@ -350,21 +326,20 @@ let _ = test_eval_eqv_named

""hello"; 5.0; "hello"; 5.0; "hello"; 7"

-(* let _ = test_eval_eqv_named - * "Implicit Arguments" - * - * "default = new-attribute Macro; - * default = add-attribute default Int (macro (lambda (lst : List Sexp) -> - * (IO_return (Sexp_integer (Int->Integer 1))))); - * - * fun = lambda (x : Int) => - * lambda (y : Int) -> - * lambda (z : Int) -> x * y + z;" - * - * "fun 2 1; - * fun 2 1" - * - * "3; 3" *) +let _ = test_eval_eqv_named + "Implicit Arguments" + + {| + fun = lambda (x : Int) => + lambda (p : Eq x x) -> + x; + |} + + {| + fun (Eq_refl (x := 2)) + |} + + "2"

let _ = test_eval_eqv_named "Equalities" @@ -382,8 +357,8 @@ let _ = test_eval_eqv_named "P = (a : Type) ≡> a -> Not (Not a); p : P; p = lambda a ≡> lambda x notx -> notx x; - tP : Decidable P; - tP = (datacons Decidable true) (prop := P) (p := p); + tP : Decidable (ℓ := ?ℓ₀) P; + tP = (datacons (Decidable (ℓ := ?ℓ₀)) true) (prop := P) (p := p);

PairTest = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));

@@ -404,40 +379,119 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Y"

- "length_y = lambda t ≡> - %% FIXME: The `a` argument should be inferred! - Y (a := List t) (witness := (lambda l -> 0)) - (lambda length l - -> case l - | nil => 0 - | cons _ l => 1 + length l);" + {| + length_y = + Y (witness := (lambda l -> 0)) + (lambda length l + -> case l + | nil => 0 + | cons _ l => 1 + length l); + |}

"length_y (cons 1 (cons 5 nil));"

"2;"

let _ = test_eval_eqv_named - "Block" + "Block"

- "a = 2" + "a = 2"

- "a + 1;" - "{a + 1};" + "a + 1;" + "{a + 1};"

let _ = test_eval_eqv_named - "define-operator" + "define-operator"

- "define-operator "IF" () 2; - define-operator "THEN" 2 1; - define-operator "ELSE" 1 66; - IF_THEN_ELSE_ = if_then_else_;" + {| + define-operator "IF" () 2; + define-operator "THEN" 2 1; + define-operator "ELSE" 1 66; + IF_THEN_ELSE_ = if_then_else_; + |}

- "IF true THEN 2 ELSE 3;" - "if true then 2 else 3;" + "IF true THEN 2 ELSE 3;" + "if true then 2 else 3;"

let _ = test_eval_eqv_named - "Type Alias" "ListInt = List Int;" "" (* == *) "" + "Type Alias" "ListInt = List Int;" "" ""

-(* run all tests *) -let _ = run_all () +let _ = test_eval_eqv_named + "Equality in case : safe head" + + {| +unvoid (void : Void) = ##case_ void; + +Not prop = (contra : prop) ≡> False; + +head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; +head ls p = + ##case_ (ls + | nil => unvoid (p (contra := (##DeBruijn 0))) + | cons x xs => x); + +l = (cons 0 nil); + +nil≠l : Not (Eq nil l); +nil≠l = + lambda (if_it_were : Eq nil l) ≡> + Eq_cast (x := nil) (y := l) + (p := if_it_were) + (f := lambda nill -> + case nill + | nil => True + | cons _ _ => False) + (); + |} + "head l nil≠l" "0" + +let _ = test_eval_eqv_named + "Erasable cons args" + {| +P = (a : Type) ≡> a -> Not (Not a); +p : P; +p = lambda a ≡> lambda x notx -> notx x; + +tP : Decidable (ℓ := ?ℓ₀) P; +tP = (datacons (Decidable (ℓ := ?ℓ₀)) true) (prop := P) (p := p); + +res = + case tP + | (datacons ? true) (p := _) => tP % A ref to the ctx + | (datacons ? false) (p := _) => tP; + |} + "res" "tP" + +let _ = + add_test "EVAL" "int overflows" (fun () -> + let check_op op biop a b = + let a' = Z.of_int a in + let b' = Z.of_int b in + let expect' = biop a' b' in + let str = "(Int_" ^ op ^ " " ^ (string_of_int a) + ^ " " ^ (string_of_int b) ^ ")" in + let lxp = List.hd (Elab.lexp_expr_str str ectx) in + let elxp = OL.erase_type lxp in + assert (Log.error_count () == 0); + + if Z.fits_int expect' then + let actual = eval elxp rctx in + expect_equal_values [actual] [Vint (Z.to_int expect')] + else + (* The result should overflow *) + try let result = (eval elxp rctx) in + ut_string2 ("EXPECTED overflow for `" ^ str ^ "`\n"); + ut_string2 ("GOT: " ^ (value_string result) ^ "\n"); + failure + with + | Log.Internal_error _ -> Log.clear_log (); success in + let arith_ops = [("+", Z.add); ("-", Z.sub); ("*", Z.mul); ("/", Z.div)] in + let vals = [min_int; -1; 0; 1; max_int] in + let sum_for ls fn = List.fold_left (+) 0 (List.map fn ls) in + sum_for arith_ops (fun (op, biop) -> + sum_for vals (fun a -> + sum_for vals (fun b -> + if op = "/" && b = 0 then success else + check_op op biop a b))))

+let _ = run_all ()

===================================== tests/inverse_test.ml ===================================== @@ -94,7 +94,7 @@ let inv_add_test name inputs = then b else not b) | None -> (not b)) true inputs - then success () else failure ()) + then success else failure)

let _ = inv_add_test "Manual" input

===================================== tests/macro_test.ml ===================================== @@ -60,11 +60,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let ecode = "(lambda (x : Int) -> sqr 3) 5;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint(r)] -> expect_equal_int r (3 * 3) - | _ -> failure ()) -) + expect_equal_values ret [Vint(3 * 3)]))

let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " @@ -89,14 +85,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let ecode = "a; b;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint(a); Vint(b)] -> - if (a = 1 && b = 2) then success () else failure () - - | _ -> failure ()) -) - + expect_equal_values ret [Vint(1); Vint(2)]))

(* run all tests *) let _ = run_all ()

===================================== tests/sexp_test.ml ===================================== @@ -4,7 +4,7 @@ open Utest_lib

let sexp_parse_str dcode = sexp_parse_str dcode Grammar.default_stt Grammar.default_grammar (Some ";") - + let test_sexp_add dcode testfun = add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode)) @@ -14,8 +14,8 @@ let _ = test_sexp_add "lambda x -> x + x" (fun ret -> | [Node(Symbol(_, "lambda_->_"), [Symbol(_, "x"); Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])] - -> success () - | _ -> failure () + -> success + | _ -> failure )

let _ = test_sexp_add "x * x * x" (fun ret -> @@ -23,8 +23,8 @@ let _ = test_sexp_add "x * x * x" (fun ret -> | [Node(Symbol(_, "_*_"), [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")])] - -> success () - | _ -> failure () + -> success + | _ -> failure )

let test_sexp_eqv dcode1 dcode2 = @@ -33,10 +33,10 @@ let test_sexp_eqv dcode1 dcode2 = let s1 = sexp_parse_str dcode1 in let s2 = sexp_parse_str dcode2 in if sexp_eq_list s1 s2 - then success () + then success else (sexp_print (List.hd s1); sexp_print (List.hd s2); - failure ())) + failure))

let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y"

===================================== tests/unify_test.ml ===================================== @@ -21,21 +21,18 @@ * * -------------------------------------------------------------------------- *)

-open Sexp -open Pexp + open Lexp open Unification

-open Utest_lib - open Fmt +open Utest_lib

-open Builtin -open Env - -open Str +module U = Util

-open Debug +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx

type result = | Constraint @@ -43,10 +40,6 @@ type result = | Equivalent | Nothing

-type unif_res = (result * (constraints) * lexp * lexp) - -type triplet = string * string * string - let string_of_result r = match r with | Constraint -> "Constraint" @@ -54,179 +47,97 @@ let string_of_result r = | Equivalent -> "Equivalent" | Nothing -> "Nothing"

-let max_dim (lst: (string * string * string * string) list): (int * int * int *int) = - let max i l = max i (String.length l) - in List.fold_left - (fun (la, ca1, ca2, ra) (l, c1, c2, r) -> ((max la l), (max ca1 c1), (max ca2 c2), (max ra r))) - (0, 0, 0, 0) - lst - -let fmt (lst: (lexp * lexp * result * result) list): string list = - let str_lst = List.map - (fun (l1, l2, r1, r2) -> ((lexp_string l1), (lexp_string l2), (string_of_result r1), (string_of_result r2))) - lst - in let l, c1, c2, r = max_dim str_lst - in List.map (fun (l1, l2, r1, r2) -> (U.padding_right l1 l ' ') - ^ ", " - ^ (U.padding_right l2 c1 ' ') - ^ " -> got: " - ^ (U.padding_right r2 r ' ') - ^ " expected: " - ^ (U.padding_right r1 c2 ' ') - ) str_lst - -(* Inputs for the test *) -let str_induct = "Nat : Type; Nat = typecons (dNat) (zero) (succ Nat)" -let str_int_3 = "i = 3" -let str_int_4 = "i = 4" -let str_case = "i = case true -| true => 2 -| false => 42" -let str_case2 = "i = case nil(a := Int) -| nil => 12 -| _ => 24" -let str_let = "i = let a = 5 in a + 1" -let str_let2 = "j = let b = 5 in b" -let str_lambda = "sqr = lambda (x : Int) -> x * x;" -let str_lambda2 = "sqr = lambda (x : Int) -> x * x;" -let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;" -let str_type = "i = let j = decltype(Type) in decltype(j);" -let str_type2 = "j = let i = Int -> Int in decltype(i);" - -let generate_ltype_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, _, ltype) -> ltype)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let generate_lexp_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, lxp, _) -> lxp)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let input_induct = generate_lexp_from_str str_induct -let input_int_4 = generate_lexp_from_str str_int_4 -let input_int_3 = generate_lexp_from_str str_int_3 -let input_case = generate_lexp_from_str str_case -let input_case2 = generate_lexp_from_str str_case2 -let input_let = generate_lexp_from_str str_let -let input_let2 = generate_lexp_from_str str_let -let input_lambda = generate_lexp_from_str str_lambda -let input_lambda2 = generate_lexp_from_str str_lambda2 -let input_lambda3 = generate_lexp_from_str str_lambda3 -let input_arrow = generate_ltype_from_str str_lambda -let input_arrow2 = generate_ltype_from_str str_lambda2 -let input_arrow3 = generate_ltype_from_str str_lambda3 -let input_type = generate_ltype_from_str str_type -let input_type_t = generate_ltype_from_str str_type2 - -let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = - - ( mkLambda ((Anormal), - (Util.dummy_location, Some "L1"), - mkVar((Util.dummy_location, Some "z"), 3), - mkImm (Integer (Util.dummy_location, 3))), - mkLambda ((Anormal), - (Util.dummy_location, Some "L2"), - mkVar((Util.dummy_location, Some "z"), 4), - mkImm (Integer (Util.dummy_location, 3))), Nothing ) - - ::(input_induct , input_induct , Equivalent) (* 2 *) - ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) - ::(input_int_3 , input_int_4 , Nothing) (* 4 *) - ::(input_case , input_int_4 , Constraint) (* 5 *) - ::(input_case , input_induct , Constraint) (* 6 *) - ::(input_case , input_case , Equivalent) (* 7 *) - ::(input_case , input_case2 , Nothing) (* 8 *) - - ::(input_let , input_induct , Constraint) (* 9 *) - ::(input_let , input_int_4 , Constraint) (* 10 *) - ::(input_let , input_case , Constraint) (* 11 *) - ::(input_let , input_let , Equivalent) (* 12 *) - ::(input_let2 , input_let , Equivalent) (* 13 *) - ::(input_let2 , input_let2 , Equivalent) (* 14 *) - - ::(input_lambda , input_int_4 , Nothing) (* 15 *) - ::(input_lambda , input_induct , Nothing) (* 16 *) - ::(input_lambda , input_case , Constraint) (* 17 *) - ::(input_lambda , input_case2 , Constraint) (* 18 *) - ::(input_lambda , input_let , Constraint) (* 19 *) - ::(input_lambda , input_induct , Nothing) (* 20 *) - ::(input_lambda , input_lambda , Equivalent) (* 21 *) - - ::(input_lambda2 , input_int_4 , Nothing) (* 22 *) - ::(input_lambda2 , input_induct , Nothing) (* 23 *) - ::(input_lambda2 , input_case , Constraint) (* 24 *) - ::(input_lambda2 , input_case2 , Constraint) (* 25 *) - ::(input_lambda2 , input_let , Constraint) (* 26 *) - ::(input_lambda2 , input_induct , Nothing) (* 27 *) - ::(input_lambda2 , input_lambda , Equivalent) (* 28 *) - ::(input_lambda2 , input_lambda2 , Equivalent) (* 29 *) - ::(input_lambda2 , input_lambda3 , Constraint) (* 30 *) - ::(input_lambda3 , input_lambda3 , Equivalent) (* 31 *) - - ::(input_arrow2 , input_int_4 , Unification) (* 32 *) - ::(input_arrow2 , input_induct , Unification) (* 33 *) - ::(input_arrow2 , input_case , Constraint) (* 34 *) - ::(input_arrow2 , input_case2 , Constraint) (* 35 *) - ::(input_arrow2 , input_let , Constraint) (* 36 *) - ::(input_arrow2 , input_induct , Unification) (* 37 *) - ::(input_arrow2 , input_lambda , Unification) (* 38 *) - ::(input_arrow2 , input_lambda2 , Unification) (* 39 *) - ::(input_arrow2 , input_arrow3 , Unification) (* 40 *) - ::(input_arrow3 , input_arrow , Unification) (* 41 *) - ::(input_arrow2 , input_arrow , Unification) (* 42 *) - ::(input_arrow3 , input_arrow3 , Equivalent) (* 43 *) - - ::(input_type , input_type_t , Equivalent) (* 44 *) - - ::(mkMetavar (0, S.identity, (Util.dummy_location, Some "M")), - mkVar ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *) - - ::[] - -let test_input (lxp1: lexp) (lxp2: lexp): unif_res = +let unif_output (lxp1: lexp) (lxp2: lexp) ctx = let orig_subst = !metavar_table in - let res = unify lxp1 lxp2 Myers.nil in - match res with + let constraints = unify lxp1 lxp2 ctx in + match constraints with | [] -> let new_subst = !metavar_table in if orig_subst == new_subst - then (Equivalent, res, lxp1, lxp2) - else (Unification, res, lxp1, lxp2) - | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) - | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) - -let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = - let r, _, _, _ = test_input lxp1 lxp2 - in if r = res then true else false - -let test_if (input: lexp list) sample_generator checker : bool = - let rec test_if_ samples checker = - match samples with - | (l1, l2, res)::t -> if checker l1 l2 res then test_if_ t checker else false - | [] -> true - in test_if_ (sample_generator input) checker - -let unifications = List.map - (fun (l1, l2, res) -> - let r, _, _, _ = test_input l1 l2 - in (l1, l2, res, r)) - (* FIXME: Skip failure for now. *) - [] (* (generate_testable []) *) - -let idx = ref 0 -let _ = List.map - (fun (str, (l1, l2, expected, res)) -> - idx := !idx + 1; - add_test "UNIFICATION" - ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str ) - (fun () -> if expected = res then success () else failure ())) - (List.combine (fmt unifications) unifications ) + then (Equivalent, constraints) + else (Unification, constraints) + | (CKresidual, _, _, _)::_ -> (Constraint, constraints) + | (CKimpossible, _, _, _)::_ -> (Nothing, constraints) + +let add_unif_test name ?(ectx=ectx) lxp_a lxp_b expected = + add_test "UNIFICATION" name (fun () -> + let (r, cstrts) = unif_output lxp_a lxp_b (DB.ectx_to_lctx ectx) in + + if r = expected then + success + else ( + ut_string2 (red ^ "EXPECTED: " ^ reset ^ (string_of_result expected) ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ (string_of_result r ) ^ "\n"); + ut_string2 ("During the unification of:\n\t" ^ (lexp_string lxp_a) + ^ "\nand\n\t" ^ (lexp_string lxp_b) ^ "\n"); + failure + )) + +let add_unif_test_s name ?(setup="") ?(ectx=ectx) input_a input_b expected = + let _, ectx = Elab.lexp_decl_str setup ectx in + + let lxp_a = List.hd (Elab.lexp_expr_str input_a ectx) in + let lxp_b = List.hd (Elab.lexp_expr_str input_b ectx) in + + add_unif_test name ~ectx lxp_a lxp_b expected + +let _ = + (* Let's have some variables in context to block the reduction of + elimination forms. The variables are manually added to the + context (and not given a value) to make sure that they cannot be + reduced. *) + let _, ectx = Elab.lexp_decl_str + {| type Nat + | Z + | S (Nat); |} ectx in + let dloc = U.dummy_location in + let nat = mkVar ((dloc, Some "Nat"), 2) in + let shift l i = mkSusp l (S.shift i) in + let ectx, _ = + List.fold_left + (fun (ectx, i) (name, lexp) -> + Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + (ectx, 0) + [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, + mkArrow (Anormal, (dloc, Some "y"), shift nat 1, + dloc, shift nat 2)))); + ("a", nat); + ("b", nat)] in + + add_unif_test_s "same integer" "4" "4" Equivalent; + add_unif_test_s "diff. integers" "3" "4" Nothing; + add_unif_test_s "int and builtin" "3" "##Int" Nothing; + add_unif_test_s "same var" ~ectx "a" "a" Equivalent; + add_unif_test_s "diff. var" ~ectx "a" "b" Constraint; + add_unif_test_s "var and integer" ~ectx "a" "1" Constraint; + add_unif_test_s "same call" ~ectx "f a" "f a" Equivalent; + add_unif_test_s "calls with inconvertible heads" ~ectx "f a" "g a" Constraint; + add_unif_test_s "calls with diff. num. of args" ~ectx "h a" "h a b" Constraint; + add_unif_test_s "calls with residue in args" ~ectx "f a" "f b" Constraint; + add_unif_test_s "same case" ~ectx + "case a | Z => false | S n => true" + "case a | Z => false | S n => true" + Equivalent; + add_unif_test_s "diff. case" ~ectx + "case a | Z => false | S n => true" + "case a | Z => true | S n => false" + (* 'Nothing' would be a more accurate result here. This would + require implementing unification for case exprs. *) + Constraint; + + add_unif_test_s "datacons/inductive" ~ectx + "Z" + "(datacons (typecons Nat Z (S Nat)) Z)" + (* Not recursive! Refers to the previous def of Nat. *) + Equivalent; + + (* Metavariables *) + add_unif_test_s "same metavar" "?m" "?m" Equivalent; + add_unif_test_s "diff. metavar" "?m1" "?m2" Unification; + add_unif_test_s "metavar and int" "?m" "5" Unification; + + ()

let _ = run_all () - -

===================================== tests/utest_lib.ml ===================================== @@ -30,20 +30,14 @@ * * --------------------------------------------------------------------------- *)

- -module U = Util open Fmt +open Util

-module StringMap = - Map.Make (struct type t = string let compare = String.compare end) - - -type test_fun = (unit -> int) -type tests = (test_fun) StringMap.t -type sections = ((tests) StringMap.t) * string list +type test_fun = unit -> int +type section = test_fun SMap.t * string list

-let success () = 0 -let failure () = (-1) +let success = 0 +let failure = -1

(* * SECTION NAME - TEST NAME - FUNCTION (() -> int) @@ -52,7 +46,7 @@ let failure () = (-1) * "Lambda" - "Base Case" * "Lambda" - "Nested" *) -let global_sections = ref StringMap.empty +let global_sections = ref SMap.empty let insertion_order = ref [] let ret_code = ref 0 let number_test = ref 0 @@ -79,26 +73,26 @@ let set_verbose lvl = Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing)

let arg_defs = [ - ("--verbose=", + ("--verbose", Arg.Int set_verbose, " Set verbose level"); - ("--samples=", + ("--samples", Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); (* Allow users to select which test to run *) - ("--fsection=", - Arg.String (fun g -> global_fsection := U.string_uppercase g), + ("--fsection", + Arg.String (fun g -> global_fsection := String.uppercase_ascii g), " Set test filter"); - ("--ftitle=", - Arg.String (fun g -> global_ftitle := U.string_uppercase g), + ("--ftitle", + Arg.String (fun g -> global_ftitle := String.uppercase_ascii g), " Set test filter"); ]

let must_run_section str = !global_fsection = "" - || U.string_uppercase str = !global_fsection + || String.uppercase_ascii str = !global_fsection

let must_run_title str = !global_ftitle = "" - || U.string_uppercase str = !global_ftitle + || String.uppercase_ascii str = !global_ftitle

let parse_args () = Arg.parse arg_defs (fun s -> ()) ""

@@ -115,94 +109,142 @@ let ut_string2 = ut_string 2 let unexpected_throw sk tk e = ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); ut_string2 "[ ] UNEXPECTED THROW:\n"; - ut_string2 "[ ] ----------------------------- Callstack (20): -----------------------------------------\n"; - ut_string2 ("[ ] " ^ (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20))); - ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] ----------------------------- Backtrace: ----------------------------------------------\n"; ut_string2 ("[ ] " ^ (Printexc.get_backtrace ()) ^ "\n"); ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] "; ut_string2 ((Printexc.to_string e) ^ "\n" ^ reset)

-let _expect_equal_t to_string value expect = - if value = expect then - success () - else( - ut_string2 (red ^ "[ ] EXPECTED: " ^ (to_string expect)^ "\n"); - ut_string2 ( "[ ] GOT: " ^ (to_string value) ^ "\n" ^ reset); - failure ()) - -let expect_equal_int = _expect_equal_t string_of_int -let expect_equal_float = _expect_equal_t string_of_float -let expect_equal_str = _expect_equal_t (fun g -> g) - - -let add_section sname = - try - StringMap.find sname (!global_sections) - with - Not_found -> - insertion_order := sname::(!insertion_order); - (StringMap.empty, ref []) - -(* USAGE *) -(* +let _expect_equal_t equality_test to_string value expect = + if equality_test value expect then + success + else ( + ut_string2 (red ^ "EXPECTED: " ^ reset ^ "\n" ^ (to_string expect) ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n"); + failure) + +let print_value_list values = + List.fold_left (fun s v -> s ^ "\n" ^ Env.value_string v) "" values + +let expect_equal_int = _expect_equal_t Int.equal string_of_int +let expect_equal_float = _expect_equal_t Float.equal string_of_float +let expect_equal_str = _expect_equal_t String.equal (fun g -> g) +let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list + +let expect_equal_lexps = + let rec lexp_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when Lexp.eq l_head r_head + -> lexp_list_eq l_tail r_tail + | _ -> false + in + let string_of_lexp_list lexps = + List.fold_left (fun s lexp -> s ^ "\n" ^ Lexp.lexp_string lexp) "" lexps + in + _expect_equal_t lexp_list_eq string_of_lexp_list + +let expect_equal_decls = + let rec decl_eq l r = + let (_, l_vname), l_lexp, l_ltype = l in + let (_, r_vname), r_lexp, r_ltype = r in + Option.equal String.equal l_vname r_vname + && Lexp.eq l_lexp r_lexp + && Lexp.eq l_ltype r_ltype + in + let rec mutual_decl_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when decl_eq l_head r_head + -> mutual_decl_list_eq l_tail r_tail + | _ -> false + in + let rec decl_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when mutual_decl_list_eq l_head r_head + -> decl_list_eq l_tail r_tail + | _ -> false + in + let string_of_decl_list ds = + let buffer = Buffer.create 1024 in + let string_of_mutual_decl_list ds = + let source = Lexp.lexp_str_decls Lexp.pretty_ppctx ds in + let add_decl d = + Buffer.add_string buffer d; + Buffer.add_char buffer '\n' + in + List.iter add_decl source + in + List.iter string_of_mutual_decl_list ds; + Buffer.contents buffer + in + _expect_equal_t decl_list_eq string_of_decl_list + +(* USAGE + * * (add_test "LET" "Base Case" (fun () -> * let r = eval_string "let a = 2; b = 3; in a + b;" in * let v = (get_int r) in * if v = 5 then success () else failure ())) - * - * sname: Section Name - * tname: Test Name - * tfun : test function (unit -> int) *) -let add_test sname tname tfun = - - (* Does Section Exist ? *) - let (tmap, lst) = add_section sname in - - try let _ = StringMap.find tname tmap in - ut_string2 "TEST ALREADY EXISTS" - with - Not_found -> - - lst := tname::(!lst); - - (* add test *) - let ntmap = StringMap.add tname tfun tmap in - global_sections := StringMap.add sname (ntmap, lst) (!global_sections); - - number_test := (!number_test + 1) +let add_test section_name test_name test_fun = + let update_tests = function + | Some _ as entry + -> (ut_string2 (red ^ {|Test "|} ^ test_name ^ {|" alread exists.|} ^ reset); + entry) + | None + -> (number_test := !number_test + 1; + Some test_fun) + in + let update_sections section = + let updated_entry = match section with + | Some (tests, order) + -> SMap.update test_name update_tests tests, test_name :: order + | None + -> (insertion_order := section_name :: !insertion_order; + SMap.singleton test_name test_fun, [test_name]) + in + Some updated_entry + in + global_sections := SMap.update section_name update_sections !global_sections

(* sk : Section Key * tmap: test_name -> tmap * tk : Test Key *) let for_all_tests sk tmap tk = if (must_run_title tk) then ( - let tv = StringMap.find tk tmap in + let tv = SMap.find tk tmap in flush stdout; + Log.clear_log (); try let r = tv () in if r = 0 then( ut_string2 (green ^ "[ OK] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset)) else( ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset); - ret_code := failure ()) - with e -> - ret_code := failure (); - unexpected_throw sk tk e) else () + ret_code := failure) + with + | Log.Stop_Compilation message -> + ret_code := failure; + ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); + ut_string2 ("[ ] " ^ message ^ "\n" ^ reset); + Log.print_log (); + | e -> + ret_code := failure; + unexpected_throw sk tk e) else ()

let for_all_sections sk = - let tmap, tst = StringMap.find sk (!global_sections) in - - if (must_run_section sk) then( - ut_string2 ("[RUN ] " ^ sk ^ " \n"); - tst := List.rev (!tst); - List.iter (for_all_tests sk tmap) (!tst)) - - else () + let tmap, tst = SMap.find sk (!global_sections) in + let tst = List.rev tst in + if must_run_section sk + then ( + ut_string2 ("[RUN ] " ^ sk ^ " \n"); + List.iter (for_all_tests sk tmap) tst)

(* Run all *) let run_all () = + Printexc.record_backtrace true; + parse_args ();

insertion_order := List.rev (!insertion_order);

===================================== tests/utest_main.ml ===================================== @@ -29,8 +29,8 @@ * Basic utest program run all tests * * --------------------------------------------------------------------------- *) + open Fmt -module U = Util

let cut_name str = String.sub str 0 (String.length str - 12) @@ -43,18 +43,18 @@ let global_ftitle = ref "" let global_filter = ref false

let arg_defs = [ - ("--verbose=", + ("--verbose", Arg.Int (fun g -> global_verbose_lvl := g), " Set verbose level"); - ("--samples=", + ("--samples", Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); - ("--tests=", + ("--tests", Arg.String (fun g -> global_tests_dir := g), " Set tests directory"); (* Allow users to select which test to run *) - ("--fsection=", - Arg.String (fun g -> global_fsection := U.string_uppercase g; + ("--fsection", + Arg.String (fun g -> global_fsection := String.uppercase_ascii g; global_filter := true), " Set test filter"); - ("--ftitle=", - Arg.String (fun g -> global_ftitle := U.string_uppercase g; + ("--ftitle", + Arg.String (fun g -> global_ftitle := String.uppercase_ascii g; global_filter := true), " Set test filter"); ]

@@ -88,7 +88,7 @@ let print_file_name i n name pass =

let must_run str = not (!global_filter) - || U.string_uppercase (cut_name str) = !global_fsection + || String.uppercase_ascii (cut_name str) = !global_fsection

(* search *_test.byte executable en run them Usage: @@ -130,17 +130,20 @@ let main () = let exit_code = ref 0 in let failed_test = ref 0 in let tests_n = ref 0 in - let test_args = " --samples= " ^ root_folder ^ - " --verbose= " ^ (string_of_int !global_verbose_lvl) ^ - (if not (!global_ftitle = "") then - (" --ftitle= " ^ !global_ftitle) else "") in + let test_args = + ["--samples"; root_folder; + "--verbose"; (string_of_int !global_verbose_lvl)] @ + (if not (!global_ftitle = "") then + ["--ftitle"; !global_ftitle] else []) in

List.iter (fun file -> flush stdout;

if must_run file then ( tests_n := !tests_n + 1; - exit_code := Sys.command (folder ^ file ^ test_args); + let command = String.concat " " (List.map Filename.quote + ((folder ^ file)::test_args)) in + exit_code := Sys.command command;

(if !exit_code != 0 then( (if verbose 1 then print_file_name (!tests_n) files_n file false);

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