Jean-Alexandre Barszcz pushed to branch depelim at Stefan / Typer

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

- - - - - 2f295e56 by Jean-Alexandre Barszcz at 2020-09-13T17:59:43-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.

- - - - - caa7bf07 by Jean-Alexandre Barszcz at 2020-09-13T22:12:25-04:00 Conversion for metavariables

- - - - - 709128db by Jean-Alexandre Barszcz at 2020-09-13T22:36:27-04:00 Case conversion

- - - - - 7d4c6a80 by Jean-Alexandre Barszcz at 2020-09-13T22:36:27-04:00 [WIP] Big ints in sexps and for int literals

Issues to resolve:

- Should we refer to the big ints module as `Z` (as done here) or as `BI`, as is done elsewhere in the codebase?

- Review every use of the partial Z.to_int, to make sure that it makes sense. In particular, I am not sure about the decision to change the `Elab_*` functions to take `Integer`s instead of `Int`s. I have done this to avoid having to deal with the partiality on the Typer side, but it means that these functions could technically fail.

- Should type levels be big ints?

- - - - - 9e758d24 by Jean-Alexandre Barszcz at 2020-09-13T22:36:27-04:00 Improve quoting

- - - - - 6da5889f by Jean-Alexandre Barszcz at 2020-09-13T22:36:28-04:00 Add a macro for dependent elimination

- - - - -

30 changed files:

- GNUmakefile - btl/builtins.typer - btl/case.typer - + btl/depelim.typer - btl/list.typer - btl/pervasive.typer - btl/polyfun.typer - btl/tuple.typer - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.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

===================================== 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) @@ -108,11 +108,6 @@ Int_- = Built-in "Int.-" : Int -> Int -> Int; Int_* = Built-in "Int.*" : Int -> Int -> Int; Int_/ = Built-in "Int./" : Int -> Int -> Int;

-_+_ = Int_+; -_-_ = Int_-; -_*_ = Int_*; -_/_ = Int_/; - %% modulo Int_mod = Built-in "Int.mod" : Int -> Int -> Int;

@@ -142,6 +137,11 @@ Integer_- = Built-in "Integer.-" : Integer -> Integer -> Integer; Integer_* = Built-in "Integer.*" : Integer -> Integer -> Integer; Integer_/ = Built-in "Integer./" : Integer -> Integer -> Integer;

+_+_ = Integer_+; +_-_ = Integer_-; +_*_ = Integer_*; +_/_ = Integer_/; + Integer_< = Built-in "Integer.<" : Integer -> Integer -> Bool; Integer_> = Built-in "Integer.>" : Integer -> Integer -> Bool; Integer_eq = Built-in "Integer.=" : Integer -> Integer -> Bool; @@ -367,7 +367,7 @@ Elab_isconstructor = Built-in "Elab.isconstructor" %% Check if the n'th field of a constructor is erasable %% If the constructor isn't defined it will always return false %% -Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool; +Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Integer -> Elab_Context -> Bool;

%% %% Check if a field of a constructor is erasable @@ -380,14 +380,14 @@ Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Ela %% It return "_" in case the field isn't defined %% see pervasive.typer for a more convenient function %% -Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; +Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Integer -> Elab_Context -> String;

%% %% Get the position of a field in a constructor %% It return -1 in case the field isn't defined %% see pervasive.typer for a more convenient function %% -Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; +Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Integer;

%% %% Get the docstring associated with a symbol

===================================== btl/case.typer ===================================== @@ -156,7 +156,7 @@ get-branches vars sexps = let to-case sexp = let

tup-exprs : Sexp -> List Sexp; - tup-exprs sexp = if (Int_eq (List_length vars) 1) then + tup-exprs sexp = if (Integer_eq (List_length vars) 1) then (cons (expand-tuple-ctor sexp) nil) else (List_map expand-tuple-ctor (get-tup-exprs sexp)); @@ -229,7 +229,7 @@ kinds pat = let %% What I do not expect to work is a combinaison of %% arguments with name, other without name and all this in a random order %% - mf : Elab_Context -> Sexp -> Int -> Bool; + mf : Elab_Context -> Sexp -> Integer -> Bool; mf env arg i = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then ( if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then @@ -283,8 +283,8 @@ renamed-pat pat names = let %% %% Get the name of the n'th element of any tuple %% - tuple-nth : Int -> Sexp; - tuple-nth n = Sexp_symbol (String_concat "%" (Int->String n)); + tuple-nth : Integer -> Sexp; + tuple-nth n = Sexp_symbol (String_concat "%" (Integer->String n));

%% %% Get the constructor of the pattern as argument @@ -304,7 +304,7 @@ renamed-pat pat names = let %% Produce code according to argument kind %% and if it already use explicit field or not %% - mf : List Bool -> Sexp -> Int -> Sexp; + mf : List Bool -> Sexp -> Integer -> Sexp; mf kinds v i = Sexp_dispatch v (lambda sym ss -> if (Sexp_eq sym (Sexp_symbol "_:=_")) @@ -421,7 +421,7 @@ introduced-vars pat = let %% It is useful to know where is the variable in `ks` to get its kind %% (kind is actualy only erasable or not) %% - ff : IO (Pair Int (List Sexp)) -> Sexp -> IO (Pair Int (List Sexp)); + ff : IO (Pair Integer (List Sexp)) -> Sexp -> IO (Pair Integer (List Sexp)); ff p v = let

o = do { @@ -808,25 +808,25 @@ in case parts adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); adjust-len branches = let

- max-len : Int; + max-len : Integer; max-len = let

- ff : Int -> Pair Pats Code -> Int; + ff : Integer -> Pair Pats Code -> Integer; ff n branch = case branch | pair pats _ => - if (Int_< n (List_length pats)) then + if (Integer_< n (List_length pats)) then (List_length pats) else (n);

in List_foldl ff 0 branches;

- preppend-dflt : Int -> Pair Pats Code -> Pair Pats Code; + preppend-dflt : Integer -> Pair Pats Code -> Pair Pats Code; preppend-dflt n branch = let

- sup : Int -> Pats; + sup : Integer -> Pats; sup n = - if (Int_eq n 0) then + if (Integer_eq n 0) then (nil) else (cons dflt-var (sup (n - 1)));

===================================== btl/depelim.typer ===================================== @@ -0,0 +1,69 @@ +%% 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 the arrow_sexp? + 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 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 (lambda args -> IO_return (case_as_return_impl args)); +case_return_ = macro (lambda args -> IO_return (case_as_return_impl args)); + +%% 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 = +%% lambda l (P : Nat -> Type_ l) ≡> +%% lambda base step n -> +%% case n return (P n) %% <--- The as clause is omitted: the target is a var. +%% | Z => base +%% | S n' => (step n' (Nat_induction (P := P) base step n'));

===================================== btl/list.typer ===================================== @@ -25,14 +25,14 @@ %% Alternative (tail recursive): %% %% length xs = let -%% helper : (a : Type) ≡> Int -> List a -> Int; +%% helper : (a : Type) ≡> Integer -> List a -> Integer; %% helper len xs = case xs %% | nil => len %% | cons hd tl => helper (len + 1) tl; %% in helper 0 xs; %% %% -length : (a : Type) ≡> List a -> Int; +length : (a : Type) ≡> List a -> Integer; length xs = case xs | nil => 0 | cons hd tl => @@ -83,9 +83,9 @@ map f = lambda xs -> case xs %% %% As `map` but user's function also takes element index as last argument %% -mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +mapi : (a : Type) ≡> (b : Type) ≡> (a -> Integer -> b) -> List a -> List b; mapi = lambda f -> lambda xs -> let - helper : (a -> Int -> b) -> Int -> List a -> List b; + helper : (a -> Integer -> b) -> Integer -> List a -> List b; helper = lambda f -> lambda i -> lambda xs -> case xs | nil => nil | cons x xs => cons (f x i) (helper f (i + 1) xs); @@ -105,9 +105,9 @@ map2 = lambda f -> lambda xs -> lambda ys -> case xs %% %% As `foldl` but user's function also takes element index as last argument %% -foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> List b -> a; +foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Integer -> a) -> a -> List b -> a; foldli = lambda f -> lambda o -> lambda xs -> let - helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a; + helper : (a -> b -> Integer -> a) -> Integer -> a -> List b -> a; helper = lambda f -> lambda i -> lambda o -> lambda xs -> case xs | nil => o | cons x xs => helper f (i + 1) (f o x i) xs; @@ -144,11 +144,11 @@ find = lambda f -> lambda xs -> case xs %% %% Get the n'th element of a list or a default if the list is smaller than n %% -nth : (a : Type) ≡> Int -> List a -> a -> a; +nth : (a : Type) ≡> Integer -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs - => case Int_<= n 0 + => case Integer_<= n 0 | true => x | false => nth (n - 1) xs d;

@@ -223,7 +223,7 @@ in map mf xs; empty? : (a : Type) ≡> List a -> Bool; %% %% O(N): -%% empty? = lambda xs -> Int_eq (length xs) 0; +%% empty? = lambda xs -> Integer_eq (length xs) 0; %% %% O(1): empty? = lambda xs -> case xs

===================================== btl/pervasive.typer ===================================== @@ -38,7 +38,7 @@ none = datacons Option none;

%%%% List functions

-List_length : List ?a -> Int; % Recursive defs aren't generalized :-( +List_length : List ?a -> Integer; % Recursive defs aren't generalized :-( List_length xs = case xs | nil => 0 | cons hd tl => @@ -76,11 +76,11 @@ List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs;

-List_nth : Int -> List ?a -> ?a -> ?a; +List_nth : Integer -> List ?a -> ?a -> ?a; List_nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs - => case Int_<= n 0 + => case Integer_<= n 0 | true => x | false => List_nth (n - 1) xs d;

@@ -150,9 +150,9 @@ List_foldl f i xs = case xs | nil => i | cons x xs => List_foldl f (f i x) xs;

-List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Integer -> b) -> List a -> List b; List_mapi f xs = let - helper : (a -> Int -> b) -> Int -> List a -> List b; + helper : (a -> Integer -> b) -> Integer -> List a -> List b; helper f i xs = case xs | nil => nil | cons x xs => cons (f x i) (helper f (i + 1) xs); @@ -175,7 +175,7 @@ List_fold2 f o xs ys = case xs

%% Is argument List empty? List_empty : List ?a -> Bool; -List_empty xs = Int_eq (List_length xs) 0; +List_empty xs = Integer_eq (List_length xs) 0;

%%% Good 'ol combinators

@@ -203,21 +203,30 @@ 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" (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))); @@ -462,10 +471,10 @@ Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors. -LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! -type LList (a : Type) (n : Int) +LList : Type -> Integer -> Type; %FIXME: `LList : ?` should be sufficient! +type LList (a : Type) (n : Integer) | vnil (p ::: Eq n 0) - | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! + | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1));

%%%% If

@@ -543,7 +552,7 @@ in case (String_eq r "_") %% Elab_arg-pos a b c = let r = Elab_arg-pos' a b c; -in case (Int_eq r (-1)) +in case (Integer_eq r (-1)) | true => (none) | false => (some r);

@@ -634,6 +643,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

===================================== btl/polyfun.typer ===================================== @@ -84,7 +84,7 @@ cases-to-sexp vars cases = let (cons pat (cons body nil));

tup : Bool; - tup = Int_< 1 (List_length vars); + tup = Integer_< 1 (List_length vars);

in Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons

===================================== btl/tuple.typer ===================================== @@ -66,7 +66,7 @@ gen-vars vars = io-list (List_map %% gen-tuple-names : List Sexp -> List Sexp; gen-tuple-names vars = List_mapi - (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i))) + (lambda _ i -> Sexp_symbol (String_concat "%" (Integer->String i))) vars;

%% @@ -90,7 +90,7 @@ gen-deduce vars = List_map %% tuple-nth = macro (lambda args -> let

- nerr = lambda _ -> (Int->Integer (-1)); + nerr = lambda _ -> (-1);

%% argument `n` of this macro n : Integer; @@ -138,10 +138,10 @@ assign-tuple = macro (lambda args -> let

%% map every tuple's variable %% using `tuple-nth` to assign element to variable - mf : Sexp -> Sexp -> Int -> Sexp; + mf : Sexp -> Sexp -> Integer -> Sexp; mf t arg i = Sexp_node (Sexp_symbol "_=_") (cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth") - (cons t (cons (Sexp_integer (Int->Integer i)) nil))) nil)); + (cons t (cons (Sexp_integer i) nil))) nil));

in do { IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi

===================================== 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 ===================================== @@ -278,7 +278,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 +467,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) @@ -736,20 +736,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 +775,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 +785,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 +895,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 @@ -1565,7 +1596,7 @@ let sform_arrow kind ctx loc sargs ot = let sform_immediate ctx loc sargs ot = match sargs with | [(String _) as se] -> mkImm (se), Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_integer | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (sl, pts, el)] -> let grm = ectx_get_grammar ctx in @@ -1772,7 +1803,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 @@ -1945,21 +1976,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 +1996,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 ===================================== @@ -283,7 +283,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 +373,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)) -> Vinteger i | Imm(String (_, s)) -> Vstring s | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp @@ -567,7 +567,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. *) @@ -826,7 +826,7 @@ let is_constructor loc depth args_val = match args_val with | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"

let is_nth_erasable loc depth args_val = match args_val with - | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) + | [Vstring name; Vinteger nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name (Z.to_int nth_arg) ectx) | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments"

let is_arg_erasable loc depth args_val = match args_val with @@ -834,11 +834,11 @@ let is_arg_erasable loc depth args_val = match args_val with | _ -> error loc "Elab.is-arg-erasable takes two String and an Elab_Context as arguments"

let nth_arg loc depth args_val = match args_val with - | [Vstring t; Vint nth; Velabctx ectx] -> Vstring (nth_ctor_arg t nth ectx) + | [Vstring t; Vinteger nth; Velabctx ectx] -> Vstring (nth_ctor_arg t (Z.to_int nth) ectx) | _ -> error loc "Elab.nth-arg takes a String, an Int and an Elab_Context as arguments"

let arg_pos loc depth args_val = match args_val with - | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) + | [Vstring t; Vstring a; Velabctx ectx] -> Vinteger (Z.of_int (ctor_arg_pos t a ectx)) | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"

let array_append loc depth args_val = match args_val with

===================================== 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 ===================================== @@ -574,11 +574,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 +641,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 +962,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)

===================================== 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,6 +38,22 @@ 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 error_tc = Log.log_error ~section:"TC" let warning_tc = Log.log_warning ~section:"TC"

@@ -133,8 +149,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 @@ -157,6 +178,12 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf_aux e ctx in + 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 @@ -173,11 +200,14 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = (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"); @@ -203,29 +233,28 @@ 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

(** 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" *********)

@@ -235,7 +264,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 @@ -255,14 +284,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' || @@ -330,19 +359,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 @@ -357,13 +476,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 @@ -403,11 +516,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 @@ -433,7 +546,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 () @@ -453,7 +566,7 @@ let rec check'' erased ctx e = s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float - | Imm (Integer (_, _)) -> DB.type_int + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; @@ -608,7 +721,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 -> @@ -622,27 +742,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 @@ -650,8 +789,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: " @@ -697,24 +841,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 @@ -730,25 +871,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 @@ -800,9 +935,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 @@ -822,10 +957,10 @@ 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 + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t @@ -948,7 +1083,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)

@@ -977,10 +1112,12 @@ 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 DB.type0))) + | None -> None

and clean_map cases = let clean_arg_list lst = @@ -994,7 +1131,8 @@ and clean_map cases = clean_arg_list lst [] in

SMap.map (fun (l, args, expr) - -> (l, (clean_arg_list args), (erase_type expr))) + -> (l, (clean_arg_list args), + erase_type (L.push_susp expr (S.substitute DB.type0)))) cases

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

===================================== 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 ===================================== @@ -291,16 +291,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

===================================== src/util.ml ===================================== @@ -63,10 +63,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,42 +21,45 @@ * * -------------------------------------------------------------------------- *)

- 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 inputs = - [("identity", {| -id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3; - |}); - ("whnf of case", {| +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 : Integer) -> Eq i i -> Integer; +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); @@ -67,103 +70,96 @@ example1 = true;

example2 : alwaysbool (box Int); example2 = true; - |}); - ] - -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 () -> inputs) - (fun x -> x) - (fun (name, input) -> - let result = - try - let ectx = Elab.default_ectx in - let pres = Prelexer.prelex_string input in - let sxps = Lexer.lex Grammar.default_stt pres in - let _lxps, _ectx = Elab.lexp_p_decls [] sxps ectx in - Log.stop_on_error(); - true - with - | Log.Stop_Compilation _ -> (Log.print_and_clear_log (); false) - | Log.Internal_error _ -> (Log.print_and_clear_log (); false) in - (name, result) - ) - -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_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 = + lambda l (P : Nat -> Type_ l) ≡> + lambda 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 = + lambda l (P : Nat -> Type_ l) ≡> + lambda 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 _ = 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

@@ -120,7 +112,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lambda"

- "sqr : Int -> Int; + "sqr : Integer -> Integer; sqr = lambda x -> x * x;"

"sqr 4;" (* == *) "16" @@ -128,10 +120,10 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Nested Lambda"

- "sqr : Int -> Int; + "sqr : Integer -> Integer; sqr = lambda x -> x * x;

- cube : Int -> Int; + cube : Integer -> Integer; cube = lambda x -> x * (sqr x);"

"cube 4" (* == *) "64" @@ -156,7 +148,7 @@ let _ = test_eval_eqv_named b = (ctr2 (ctr2 ctr0)); z = 3; c = (ctr3 (ctr2 ctr0)); w = 4;

- test_fun : idt -> Int; + test_fun : idt -> Integer; test_fun = lambda k -> case k | ctr1 l => 1 | ctr2 l => 2 @@ -174,7 +166,7 @@ let nat_decl = " zero = datacons Nat zero; succ = datacons Nat succ;

- to-num : Nat -> Int; + to-num : Nat -> Integer; to-num = lambda (x : Nat) -> case x | (succ y) => (1 + (to-num y)) | zero => 0;" @@ -218,8 +210,8 @@ let _ = test_eval_eqv_named two = succ one; three = succ two;

- even : Nat -> Int; - odd : Nat -> Int; + even : Nat -> Integer; + odd : Nat -> Integer;

odd = lambda (n : Nat) -> case n | zero => 0 @@ -237,7 +229,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Partial Application"

- "add : Int -> Int -> Int; + "add : Integer -> Integer -> Integer; add = lambda x y -> (x + y);

inc1 = add 1; @@ -273,24 +265,9 @@ let _ = test_eval_eqv_named (* * Special forms *) -let _ = test_eval_eqv "w = 2" "decltype w" "Int" +let _ = test_eval_eqv "w = 2" "decltype w" "Integer" 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,17 +281,16 @@ 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"

- "fun = lambda (x : Int) => - lambda (y : Int) -> - lambda (z : Int) -> x * y + z;" + "fun = lambda (x : Integer) => + lambda (y : Integer) -> + lambda (z : Integer) -> x * y + z;"

"fun (x := 3) 2 1; fun (x := 3) (z := 1) 4; @@ -336,7 +312,7 @@ let _ = test_eval_eqv_named "Metavars" let _ = test_eval_eqv_named "Explicit field patterns" "Triplet = typecons Triplet - (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); + (triplet (a ::: Integer) (b :: Float) (c : String) (d :: Integer)); triplet = datacons Triplet triplet; t = triplet (b := 5.0) (a := 3) (d := 7) (c := "hello");"

@@ -350,26 +326,25 @@ 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 : Integer) => + lambda (p : Eq x x) -> + x; + |} + + {| + fun (Eq_refl (x := 2)) + |} + + "2"

let _ = test_eval_eqv_named "Equalities"

- "f : (α : Type) ≡> (p : Eq Int α) -> Int -> α; + "f : (α : Type) ≡> (p : Eq Integer α) -> Integer -> α; f = lambda α ≡> lambda p x -> Eq_cast (f := lambda v -> v) (p := p) x"

@@ -382,14 +357,14 @@ 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));

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

- ptest : Pair Int String; + ptest : Pair Integer String; ptest = (##datacons Pair cons) (x := 4) (y := "hello");

px = case ptest | (##datacons ? cons) (x := v) => v; @@ -404,40 +379,70 @@ 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 _ = 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 ===================================== @@ -57,14 +57,10 @@ let _ = (add_test "MACROS" "macros base" (fun () ->

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

- let ecode = "(lambda (x : Int) -> sqr 3) 5;" in + let ecode = "(lambda (x : Integer) -> 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 [Vinteger (Z.of_int (3 * 3))]))

let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " @@ -72,9 +68,9 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)) in

- let make-decl : String -> Int -> Sexp; + let make-decl : String -> Integer -> Sexp; make-decl name val = - (Sexp_node (Sexp_symbol "_=_") (cons (Sexp_symbol name) (cons (Sexp_integer (Int->Integer val)) nil))) in + (Sexp_node (Sexp_symbol "_=_") (cons (Sexp_symbol name) (cons (Sexp_integer val) nil))) in

let d1 = make-decl "a" 1 in let d2 = make-decl "b" 2 in @@ -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 [Vinteger(Z.of_int 1); Vinteger(Z.of_int 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 ===================================== @@ -82,14 +82,14 @@ let str_int_4 = "i = 4" let str_case = "i = case true | true => 2 | false => 42" -let str_case2 = "i = case nil(a := Int) +let str_case2 = "i = case nil(a := Integer) | 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_lambda = "sqr = lambda (x : Integer) -> x * x;" +let str_lambda2 = "sqr = lambda (x : Integer) -> x * x;" +let str_lambda3 = "sqr = lambda (x : Integer) -> lambda (y : Integer) -> x * y;" let str_type = "i = let j = decltype(Type) in decltype(j);" let str_type2 = "j = let i = Int -> Int in decltype(i);"

@@ -128,11 +128,11 @@ 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))), + mkImm (Integer (Util.dummy_location, Z.of_int 3))), mkLambda ((Anormal), (Util.dummy_location, Some "L2"), mkVar((Util.dummy_location, Some "z"), 4), - mkImm (Integer (Util.dummy_location, 3))), Nothing ) + mkImm (Integer (Util.dummy_location, Z.of_int 3))), Nothing )

::(input_induct , input_induct , Equivalent) (* 2 *) ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) @@ -224,7 +224,7 @@ let _ = List.map 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 ())) + (fun () -> if expected = res then success else failure)) (List.combine (fmt unifications) unifications )

let _ = run_all ()

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

- -module U = Util open Fmt

module StringMap = Map.Make (struct type t = string let compare = String.compare end)

+type test_fun = unit -> int +type section = test_fun StringMap.t * string list

-type test_fun = (unit -> int) -type tests = (test_fun) StringMap.t -type sections = ((tests) StringMap.t) * string list - -let success () = 0 -let failure () = (-1) +let success = 0 +let failure = -1

(* * SECTION NAME - TEST NAME - FUNCTION (() -> int) @@ -79,26 +75,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,63 +111,104 @@ 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) + -> StringMap.update test_name update_tests tests, test_name :: order + | None + -> (insertion_order := section_name :: !insertion_order; + StringMap.singleton test_name test_fun, [test_name]) + in + Some updated_entry + in + global_sections := StringMap.update section_name update_sections !global_sections

(* sk : Section Key * tmap: test_name -> tmap @@ -180,29 +217,36 @@ let for_all_tests sk tmap tk = if (must_run_title tk) then ( let tv = StringMap.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 = StringMap.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,10 +130,10 @@ 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) ^ + let test_args = " --samples " ^ root_folder ^ + " --verbose " ^ (string_of_int !global_verbose_lvl) ^ (if not (!global_ftitle = "") then - (" --ftitle= " ^ !global_ftitle) else "") in + (" --ftitle " ^ !global_ftitle) else "") in

List.iter (fun file -> flush stdout;

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