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

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

- - - - - fd0d1b71 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-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?

- - - - - d50f4b33 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Improve quoting

- - - - - c21079e7 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Add a macro for dependent elimination

- - - - -

19 changed files:

- btl/builtins.typer - btl/case.typer - + btl/depelim.typer - btl/list.typer - btl/pervasive.typer - btl/polyfun.typer - btl/tuple.typer - src/debug.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/sexp.ml - tests/elab_test.ml - tests/eval_test.ml - tests/macro_test.ml - tests/unify_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -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/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,6 +736,10 @@ 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

@@ -787,11 +791,30 @@ and check_case rtype (loc, target, ppatterns) ctx = (* 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

@@ -872,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 @@ -1567,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 @@ -1774,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

===================================== 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/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

===================================== tests/elab_test.ml ===================================== @@ -51,7 +51,7 @@ let add_elab_test_decl = let _ = add_elab_test_expr "Instanciate implicit arguments" ~setup:{| -f : (i : Int) -> Eq i i -> Int; +f : (i : Integer) -> Eq i i -> Integer; f = lambda i -> lambda eq -> i; |} ~expected:"f 4 (Eq_refl (x := 4));" @@ -72,4 +72,90 @@ 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 _ = run_all ()

===================================== tests/eval_test.ml ===================================== @@ -112,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" @@ -120,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" @@ -148,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 @@ -166,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;" @@ -210,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 @@ -229,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; @@ -265,7 +265,7 @@ 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 _ = (add_test "EVAL" "Monads" (fun () -> @@ -288,9 +288,9 @@ let _ = (add_test "EVAL" "Monads" (fun () -> 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; @@ -312,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");"

@@ -330,7 +330,7 @@ let _ = test_eval_eqv_named "Implicit Arguments"

{| - fun = lambda (x : Int) => + fun = lambda (x : Integer) => lambda (p : Eq x x) -> x; |} @@ -344,7 +344,7 @@ let _ = test_eval_eqv_named 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"

@@ -364,7 +364,7 @@ let _ = test_eval_eqv_named

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; @@ -427,7 +427,7 @@ Not prop = (contra : prop) ≡> False; head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; head ls p = ##case_ (ls - | nil => unvoid (##DeBruijn 0) + | nil => unvoid (p (contra := (##DeBruijn 0))) | cons x xs => x);

l = (cons 0 nil);

===================================== tests/macro_test.ml ===================================== @@ -57,10 +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 - expect_equal_values ret [Vint(3 * 3)])) + expect_equal_values ret [Vinteger (Z.of_int (3 * 3))]))

let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " @@ -68,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 @@ -85,7 +85,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let ecode = "a; b;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - expect_equal_values ret [Vint(1); Vint(2)])) + expect_equal_values ret [Vinteger(Z.of_int 1); Vinteger(Z.of_int 2)]))

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

===================================== 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 *)

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