Stefan pushed to branch unification at Stefan / Typer

Commits: e314669e by Pierre Delaunay at 2016-09-25T13:39:35-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - f83ee0b4 by Pierre Delaunay at 2016-09-26T12:05:47-04:00 Merge branch 'master' of github.com:Delaunay/typer

- - - - - 12a677ab by Pierre Delaunay at 2016-09-26T19:27:11-04:00 Try to fix our Macro_ index problem. Nevertheless, it does not work as a lot of index are not computed correctly anymore

* Moved (print_lexp_ctx) from lparse.ml to debruijn.ml to help debugging * src/lparse.ml: types and expression are processed in a different context

- - - - - db617a20 by Pierre Delaunay at 2016-09-26T19:54:32-04:00 Merge with master. Indices seem to be correct. Nevertheles, Macro are still not recognized as such (back to the original issue)

- - - - - e938c998 by Stefan Monnier at 2016-09-26T20:29:14-04:00 Make type levels more canonical

* src/lexp.ml (sort_level): Replace SLn with SLz. (lexp_location, _lexp_to_str): Adjust accordingly.

* src/opslexp.ml (sort_level_max): New function. (sort_compose): Use it. (impredicative_erase): New var. (check): Adjust for new SLz. Obey impredicative_erase. Fix level calculation for inductive types.

* src/builtin.ml (type0, type1, type2): Adjust.

- - - - - 5949b172 by Stefan Monnier at 2016-09-26T20:29:53-04:00 Missing changes in last commit

- - - - - 6d7b4793 by Stefan Monnier at 2016-09-26T20:34:16-04:00 Merge branch 'trunk' into unification

- - - - -

10 changed files:

- btl/types.typer - samples/nat.typer - src/builtin.ml - src/debruijn.ml - src/fmt_lexp.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml - tests/eval_test.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -66,7 +66,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); % -----------------------------------------------------

List : Type -> Type; -List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); +List = inductive_ (List (a : Type)) (nil) (cons a (List a));

nil = inductive-cons List nil; cons = inductive-cons List cons; @@ -76,7 +76,7 @@ length = lambda a ≡> lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + (length(a := a) tl)); + | cons hd tl => (1 + (length (a := a) tl));

head : (a : Type) ≡> List a -> a; head = lambda a ≡> @@ -92,6 +92,7 @@ tail = lambda a ≡> | nil => nil | cons hd tl => tl;

+ % ----------------------------------------------------- % Macro % ----------------------------------------------------- @@ -103,8 +104,8 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp);

-% Macro : Type; -Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp)); +Macro : Type; +Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;

expand_macro_ : Macro -> List Sexp -> Sexp; @@ -187,3 +188,6 @@ declexpr = Built-in "declexpr" Macro;

+ + +

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -5,39 +5,31 @@ zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;

to-num : Nat -> Int; -to-num = lambda (x : Nat) -> - case x - | (succ y) => (1 + (to-num y)) - | zero => 0; - -one = (succ zero); -two = (succ one); -three = (succ two); +to-num = lambda (x : Nat) -> case x + | (succ y) => (1 + (to-num y)) + | zero => 0;

plus : Nat -> Nat -> Nat; -plus = lambda (x : Nat) -> - lambda (y : Nat) -> - case x - | zero => y - | succ z => succ (plus z y); +plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => y + | succ z => succ (plus z y);

+one = succ zero; +two = succ one; +three = succ two;

-odd : Nat -> Int; even : Nat -> Int; +odd : Nat -> Int; odd = lambda (n : Nat) -> case n - | zero => 0 - | succ y => (even y); + | zero => 0 + | succ y => (even y);

even = lambda (n : Nat) -> case n - | zero => 1 - | succ y => (odd y); - -%n1 = (to-num zero); -%n2 = (to-num one); -%n3 = (to-num two); + | zero => 1 + | succ y => (odd y);

-%m1 = (to-num (plus zero two)); % 2 -%m2 = (to-num (plus two zero)); % 2 -%m3 = (to-num (plus two one)); % 3

-o1 = (even two); \ No newline at end of file +a = odd one; +b = even one; +c = odd two; +d = even two; \ No newline at end of file

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -75,7 +75,7 @@ let get_predef_raw (name: string) : lexp = | None -> builtin_error dloc ("""^ name ^ "" was not predefined")

let get_predef_option (name: string) ctx = - let r = (get_size ctx) - !builtin_size - 1 in + let r = (get_size ctx) - !builtin_size - 0 in match !(SMap.find name (!predef_map)) with | Some exp -> Some (mkSusp exp (S.shift r)) | None -> None @@ -98,9 +98,12 @@ let dump_predef () =

(* Builtin types *) let dloc = dummy_location -let type0 = Sort (dloc, Stype (SortLevel (SLn 0))) -let type1 = Sort (dloc, Stype (SortLevel (SLn 1))) -let type2 = Sort (dloc, Stype (SortLevel (SLn 2))) +let level0 = SortLevel SLz +let level1 = SortLevel (SLsucc level0) +let level2 = SortLevel (SLsucc level1) +let type0 = Sort (dloc, Stype level0) +let type1 = Sort (dloc, Stype level1) +let type2 = Sort (dloc, Stype level2) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel)

@@ -343,7 +346,7 @@ let declexpr_impl loc largs ctx ftype = let lxp = match env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> lxp | None -> builtin_error loc "no expr available" in - let ltp = env_lookup_type ctx ((loc, vn), vi) in + let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *) lxp, ftype

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -46,6 +46,9 @@ let debruijn_warning = msg_warning "DEBRUIJN" (* Type definitions * ---------------------------------- *)

+let dloc = dummy_location +let type0 = Sort (dloc, Stype (SortLevel SLz)) +let dltype = type0

type property_key = (int * string) (* rev_dbi * Var name *) module PropertyMap @@ -116,7 +119,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = lexp_ctx_cons ctx 0 (Some def) v t

-let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = + +let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in (try let _ = senv_lookup name ctx in @@ -124,9 +128,11 @@ let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = with Not_found -> ()); let nmap = StringMap.add name n map in ((n + 1, nmap), - lexp_ctx_cons env 0 (Some def) v t, + lexp_ctx_cons env r (Some def) v t, f)

+let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t + let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = let (ctx, _) = List.fold_left @@ -152,10 +158,88 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = recursion_offset - 1) (ctx, List.length defs) defs

-let _name_error loc estr str = - if estr = str then () else +let env_lookup_by_index index (ctx: elab_context): env_elem = + (Myers.nth index (_get_env ctx)) + +(* Print context *) +let print_lexp_ctx (ctx : elab_context) = + let ((n, map), env, f) = ctx in + + print_string (make_title " LEXP CONTEXT "); + + make_rheader [ + (Some ('l', 10), "NAME"); + (Some ('l', 7), "INDEX"); + (Some ('l', 10), "NAME"); + (Some ('l', 4), "OFF"); + (Some ('l', 29), "VALUE:TYPE")]; + + print_string (make_sep '-'); + + (* it is annoying to print according to StringMap order *) + (* let's use myers list order *) + let rec extract_names (lst: lexp_context) acc = + match lst with + | M.Mnil -> acc + | M.Mcons (hd, tl, _, _) -> + let name = match hd with + | (_, Some (_, name), _, _) -> name + | _ -> "" in + extract_names tl (name::acc) in + + let ord = extract_names env [] in + + let rec _print idx ord = + match ord with + | [] -> () + | hd::tl ->( + let idx2 = StringMap.find hd map in + + (if idx2 != idx then ()); + + print_string " | "; lalign_print_string hd 10; + print_string " | "; lalign_print_int (n - idx - 1) 7; + print_string " | "; + + let ptr_str = "" in (*" | | | | " in *) + + try let r, name, exp, tp = + match env_lookup_by_index (n - idx - 1) ctx with + | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp + | _ -> 0, "", None, dltype in + + (* Print env Info *) + lalign_print_string name 10; (* name must match *) + print_string " | "; + lalign_print_int r 4; + print_string " | "; + + let _ = (match exp with + | None -> print_string "<var>" + | Some exp -> lexp_print exp) + (* let str = _lexp_to_str (!debug_ppctx) exp in + let str = (match str_split str '\n' with + | hd::tl -> print_string (hd ^ "\n"); tl + | _ -> []) in + + List.iter (fun elem -> + print_string (ptr_str ^ elem ^ "\n")) str) *)in + + print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n"; + + _print (idx + 1) tl + + with Not_found -> + (print_string "Not_found |\n"; _print (idx + 1) tl)) in + + _print 0 ord; print_string (make_sep '=') + + +let _name_error loc estr str ctx = + if estr = str then () else ( + print_lexp_ctx ctx; debruijn_error loc ("DeBruijn index refers to wrong name. " ^ - "Expected: "" ^ estr ^ "" got "" ^ str ^ """) + "Expected: "" ^ estr ^ "" got "" ^ str ^ """))

(* generic lookup *) @@ -167,7 +251,7 @@ let _env_lookup ctx (v: vref): env_elem = let _ = match ret with | (_, Some (_, name), _, _) -> (* Check if names match *) - _name_error loc ename name; + _name_error loc ename name ctx; | _ -> () in

ret) @@ -187,9 +271,6 @@ let env_lookup_expr ctx (v : vref): lexp option = | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) | _ -> None

-let env_lookup_by_index index (ctx: elab_context): env_elem = - (Myers.nth index (_get_env ctx)) - (* replace an expression by another *) (* Most of the time it should be O(1) but it can be O(n) *) let replace_by ctx name by =

===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -63,8 +63,8 @@ and string_of_kind = function

and string_of_sort_level lvl = match lvl with - | L.SLn i -> "SLn(" ^ string_of_int i ^ ")" - | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l^ ")" + | L.SLz -> "SLz" + | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l ^ ")"

and string_of_sort sort = match sort with

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -81,13 +81,24 @@ type ltype = lexp * * unification. *) * | MetaFoF * and subst = lexp VMap.t *) + (* + * The PTS I'm imagining looks like: + * + * S = { TypeLevel, TypeOmega, Type ℓ } + * A = { Level : TypeLevel, Z : Level, S : Level → Level, + * Type : (ℓ : Level) → Type (S ℓ) } + * R = { (TypeLevel, Type ℓ, TypeOmega), + * (TypeLevel, TypeOmega, TypeOmega), + * (Type ℓ, TypeOmega, TypeOmega), + * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } + *) and sort = | Stype of lexp | StypeOmega | StypeLevel and sort_level = - | SLn of int - | SLsucc of lexp + | SLz + | SLsucc of lexp

type varbind = @@ -253,7 +264,7 @@ let rec lexp_location e = match e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e - | SortLevel (SLn _) -> U.dummy_location + | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l | Builtin ((l, _), _) -> l @@ -778,7 +789,7 @@ and _lexp_to_str ctx exp = | Builtin ((_, name), _) -> name

| Sort (_, Stype lvl) -> (match lvl with - | SortLevel (SLn v) -> "Type_" ^ (string_of_int v) + | SortLevel SLz -> "Type_0" | _ -> "Type_?")

| _ -> print_string "Printing Not Implemented\n"; "-- --"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -176,14 +176,15 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

(* Symbol i.e identifier *) | Pvar (loc, name) ->( - try let idx = (senv_lookup name ctx) in + try + let idx = (senv_lookup name ctx) in let lxp = (make_var name idx loc) in

(* search type *) let ltp = env_lookup_type ctx ((loc, name), idx) in lxp, ltp

- with Not_found -> + with e -> (lexp_error loc ("The variable: "" ^ name ^ "" was not declared"); (* Error recovery. The -1 index will raise an error later on *) (make_var name (-1) loc), dltype)) @@ -441,7 +442,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = * Constructor : a constructor is returned * Anonymous : lambda *)

- (* retrieve function's body *) + (* retrieve function's body (sqr 3) sqr is a Pvar() *) let body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in

@@ -481,12 +482,11 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = sexp_print sarg; print_string "\n"; lexp_fatal (sexp_location sarg) "Expected non-explicit arg" - | e -> Debug_fun.do_debug (fun () -> - print_endline ("<>explicit arg : " ^ Fmt_lexp.string_of_lxp ltp); - print_endline ("<>explicit res : " ^ Fmt_lexp.string_of_lxp e); - ()); - lexp_fatal (sexp_location sarg) - "Explicit arg to non-function") in + | t -> + lexp_print t; print_string "\n"; + print_lexp_ctx ctx; + lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") in

let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -551,32 +551,32 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = _lexp_p_infer pxp ctx (i + 1) in

(* This is the builtin Macro type *) - let macro_type = match get_predef_option "Macro" ctx with - | Some lxp -> lxp - (* When type.typer is being parsed and the predef is not yet - * available *) - | None -> dltype in + let macro_type, macro_disp = match get_predef_option "Macro" ctx with + | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true + (* When type.typer is being parsed and the predef is not yet available *) + | None -> dltype, false in + + (*print_string "\nmacro_type="; lexp_print macro_type; + print_string "\nltp="; lexp_print ltp; + print_string " (= "; lexp_print (OL.lexp_whnf ltp (ectx_to_lctx ctx)); print_string ")\n"; *)

(* determine function type *) match func, ltp with - (* This is a work around for the bug described below *) | Pvar(l, name), _ when is_builtin_macro name -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - (get_macro_impl loc name) loc largs ctx ltp + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + (get_macro_impl loc name) loc largs ctx ltp

- (* FIXME: the branch 'builtin macro' is never used because of missing shift somewhere *) - (* while special forms have a type macro this does not recognize them as such *) - | macro, _ when OL.conv_p ltp macro_type -> ( + | macro, _ when (macro_disp && (OL.conv_p ltp macro_type))-> ( match macro with | Pvar(l, name) when is_builtin_macro name -> - print_string name; let pargs = List.map pexp_parse sargs in let largs = _lexp_parse_all pargs ctx i in (get_macro_impl loc name) loc largs ctx ltp

(* true macro *) - | _ -> handle_macro_call ()) + | _ -> + handle_macro_call ())

(* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall () @@ -628,17 +628,21 @@ and lexp_read_pattern pattern exp target ctx: ^ "` is not an inductive type!") in

(* Remove non explicit argument. *) - let rec remove_nexplicit args acc = - match args with - | [] -> List.rev acc - | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) - | hd::tl -> remove_nexplicit tl acc in - - let cons_args = remove_nexplicit cons_args [] in - - (* read pattern args *) - let args, nctx = lexp_read_pattern_args args cons_args ctx in - (cons_name, loc, args), nctx + let rec remove_nexplicit args acc = + match args with + | [] -> List.rev acc + | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) + | hd::tl -> remove_nexplicit tl acc in + + let cons_args = remove_nexplicit cons_args [] in + + (* read pattern args *) + let args, nctx = lexp_read_pattern_args args cons_args ctx in + (cons_name, loc, args), nctx + | _ -> lexp_warning (pexp_location ctor) + ("Invalid constructor `" + ^ (pexp_to_string ctor) ^ "`"); + ("_", pexp_location ctor, []), ctx

(* Read patterns inside a constructor *) and lexp_read_pattern_args args (args_type : lexp list) ctx: @@ -873,8 +877,9 @@ and _lexp_rec_decl decls ctx i = * i.e let decl parsing *)

(* to compute recursive offset *) - let n = (List.length decls) + 1 in + let n = (List.length decls) in let lst = ref [] in + (* print_int n; print_string "\n"; *)

(* add all elements to the environment *) let tctx = List.fold_left (fun vctx decl -> @@ -883,29 +888,30 @@ and _lexp_rec_decl decls ctx i = env_extend vctx (l, s) ForwardRef dltype

| Ldecl((l, s), _, Some ptp) -> - let lxp, _ = lexp_p_infer ptp vctx in - env_extend vctx (l, s) ForwardRef lxp + let ltp, _ = lexp_p_infer ptp vctx in + env_extend vctx (l, s) ForwardRef ltp

| Lmcall _ -> lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in

+ (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *) let i = ref 0 in let ctx = List.fold_left (fun vctx decl -> i := !i + 1; match decl with + (* +1 because we allow each definition to be recursive *) (* lexp infer *) | Ldecl ((l, s), Some pxp, None) -> - let lxp, ltp = lexp_p_infer pxp vctx in + let lxp, ltp = lexp_p_infer pxp tctx in lst := ((l, s), lxp, ltp)::!lst; - (* replace forward ref by its true value *) - replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)

(* lexp check *) | Ldecl ((l, s), Some pxp, Some ptp) -> let ltp, _ = lexp_p_infer ptp vctx in - let lxp = lexp_p_check pxp ltp vctx in + let lxp = lexp_p_check pxp ltp tctx in lst := ((l, s), lxp, ltp)::!lst; - replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp)

(* macros *) | Lmcall (a, sargs) -> @@ -914,7 +920,7 @@ and _lexp_rec_decl decls ctx i = (* unused arg *) | Ldecl ((l, s), None, _) -> lexp_error l ("Variable "" ^ s ^ "" is unused!"); - vctx) tctx decls in + vctx) ctx decls in

(List.rev !lst), ctx

@@ -931,80 +937,6 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =

(loop p ctx [])

-(* Print context *) -and print_lexp_ctx (ctx : elab_context) = - let ((n, map), env, f) = ctx in - - print_string (make_title " LEXP CONTEXT "); - - make_rheader [ - (Some ('l', 10), "NAME"); - (Some ('l', 7), "INDEX"); - (Some ('l', 10), "NAME"); - (Some ('l', 4), "OFF"); - (Some ('l', 29), "VALUE:TYPE")]; - - print_string (make_sep '-'); - - (* it is annoying to print according to StringMap order *) - (* let's use myers list order *) - let rec extract_names (lst: lexp_context) acc = - match lst with - | Mnil-> acc - | Mcons (hd, tl, _, _) -> - let name = match hd with - | (_, Some (_, name), _, _) -> name - | _ -> "" in - extract_names tl (name::acc) in - - let ord = extract_names env [] in - - let rec _print idx ord = - match ord with - | [] -> () - | hd::tl ->( - let idx2 = StringMap.find hd map in - - (if idx2 != idx then ()); - - print_string " | "; lalign_print_string hd 10; - print_string " | "; lalign_print_int (n - idx - 1) 7; - print_string " | "; - - let ptr_str = "" in (*" | | | | " in *) - - try let r, name, exp, tp = - match env_lookup_by_index (n - idx - 1) ctx with - | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp - | _ -> 0, "", None, dltype in - - (* Print env Info *) - lalign_print_string name 10; (* name must match *) - print_string " | "; - lalign_print_int r 4; - print_string " | "; - - let _ = (match exp with - | None -> print_string "<var>" - | Some exp -> lexp_print exp) - (* let str = _lexp_to_str (!debug_ppctx) exp in - let str = (match str_split str '\n' with - | hd::tl -> print_string (hd ^ "\n"); tl - | _ -> []) in - - List.iter (fun elem -> - print_string (ptr_str ^ elem ^ "\n")) str) *)in - - print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n"; - - _print (idx + 1) tl - - with Not_found -> - (print_string "Not_found |\n"; _print (idx + 1) tl)) in - - _print 0 ord; - - print_string (make_sep '=')

and print_lexp_trace () = print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -37,7 +37,11 @@ module S = Subst module B = Builtin module DB = Debruijn

-let conv_erase = true (* If true, conv ignores erased terms. *) +(* `conv_erase` is supposed to be safe according to the ICC papers. *) +let conv_erase = true (* Makes conv ignore erased terms. *) + +(* The safety of `impredicative_erase` is unknown. But I like the idea. *) +let impredicative_erase = true (* Allows erasable args to be impredicative. *)

(* Lexp context *)

@@ -195,14 +199,24 @@ let assert_type e t t' = if conv_p t t' then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()

+let rec sort_level_max l1 l2 = match l1, l2 with + | SortLevel SLz, l2 -> l2 + | l1, SortLevel SLz -> l1 + | SortLevel (SLsucc l1), SortLevel (SLsucc l2) + -> SortLevel (SLsucc (sort_level_max l1 l2)) + | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) + -> U.msg_error "TC" (lexp_location l1) + ("Can't compute the max of levels `" + ^ lexp_to_string l1 ^ "` and `" + ^ lexp_to_string l2 ^ "`"); + SortLevel SLz + let sort_compose l s1 s2 = match s1, s2 with - | (Stype (SortLevel (SLn n1)), Stype (SortLevel (SLn n2))) - (* Basic predicativity rule. *) - -> Stype (SortLevel (SLn (max n1 n2))) - | ( (StypeLevel, Stype (SortLevel (SLn _))) + | (Stype l1, Stype l2) -> Stype (sort_level_max l1 l2) + | ( (StypeLevel, Stype _) | (StypeLevel, StypeOmega) - (* | (Sort (_, Stype (SortLevel (SLn _))), Sort (_, StypeOmega)) *)) + | (Stype _, StypeOmega)) -> StypeOmega | _,_ -> (U.msg_error "TC" l "Mismatch sorts for arg and result"; @@ -218,8 +232,8 @@ let rec check ctx e = -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; B.type_int) | SortLevel (_) -> B.type_level - | Sort (l, Stype (SortLevel (SLn n))) - -> Sort (l, Stype (SortLevel (SLn (1 + n)))) + | Sort (l, Stype (SortLevel l1 as sl1)) + -> Sort (l, Stype (SortLevel (SLsucc sl1))) | Sort (_, (StypeOmega|StypeLevel)) -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!"; B.type_omega) @@ -248,7 +262,8 @@ let rec check ctx e = let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in match k1, k2 with | (Sort (_, s1), Sort (_, s2)) - -> Sort (l, sort_compose l s1 s2) + -> if ak == P.Aerasable && impredicative_erase then k2 + else Sort (l, sort_compose l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; Sort (l, StypeOmega)) @@ -280,20 +295,29 @@ let rec check ctx e = "Calling a non function!"; ft)) ft args | Inductive (l, label, args, cases) - -> let rec arg_loop args s ctx = + -> let level = SMap.fold + (fun _ case level -> + List.fold_left + (fun level (ak, _, t) -> + if ak == P.Aerasable && impredicative_erase + then level + else match check ctx t with + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | _ -> U.msg_error "TC" (lexp_location t) + "Field type is not a Type!"; + SortLevel SLz) + level + case) + cases (SortLevel SLz) in + let rec arg_loop args ctx = match args with - | [] -> Sort (l, s) + | [] -> Sort (l, Stype level) | (ak, v, t)::args - -> let s' = match check ctx t with - | Sort (_, s') -> s' - | _ -> (U.msg_error "TC" (lexp_location t) - "Field type is not a Type!"; - Stype (SortLevel (SLn 0))) in - Arrow (ak, Some v, t, lexp_location t, - (* FIXME: `sort_compose` doesn't do what we want! *) - arg_loop args (sort_compose l s s') - (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in + -> Arrow (ak, Some v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx v Variable t)) in + let tct = arg_loop args ctx in (* FIXME: Check cases! *) tct | Case (l, e, it, ret, branches, default)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -301,7 +301,7 @@ and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with - | SLn i, SLn j when i = j -> Some (subst, []) + | SLz, SLz -> Some (subst, []) | SLsucc l1, SLsucc l2 -> unify l1 l2 subst | _, _ -> None) | _, _ -> None

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -70,7 +70,7 @@ let _ = test_eval_eqv_named

"a = 10; b = a; c = b; d = c;"

- "d" (* == *) "10" + "d" (* == *) "10"

(* Let * ------------------------ *) @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "sqr : Int -> Int; sqr = lambda x -> x * x;"

- "(sqr 4);" (* == *) "16" + "sqr 4;" (* == *) "16"

let _ = test_eval_eqv_named "Nested Lambda" @@ -103,7 +103,7 @@ let _ = test_eval_eqv_named cube : Int -> Int; cube = lambda x -> x * (sqr x);"

- "(cube 4)" (* == *) "64" + "cube 4" (* == *) "64"

(* Cases + Inductive types @@ -130,7 +130,7 @@ let _ = test_eval_eqv_named | ctr2 l => 2 | _ => 3;"

- "(test_fun a); (test_fun b); (test_fun c)" + "test_fun a; test_fun b; test_fun c"

"1; 2; 3"

@@ -156,11 +156,11 @@ let _ = test_eval_eqv_named "Inductive::Recursive Call"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two);") + one = succ zero; + two = succ one; + three = succ two;")

- "(to-num zero); (to-num one); (to-num two);" + "to-num zero; to-num one; to-num two;"

"0; 1; 2"

@@ -168,9 +168,9 @@ let _ = test_eval_eqv_named "Inductive::Nat Plus"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + one = succ zero; + two = succ one; + three = succ two;

plus : Nat -> Nat -> Nat; plus = lambda (x : Nat) -> lambda (y : Nat) -> case x @@ -187,11 +187,13 @@ let _ = test_eval_eqv_named "Mutually Recursive Definition"

(nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + one = succ zero; + two = succ one; + three = succ two;

even : Nat -> Int; + odd : Nat -> Int; + odd = lambda (n : Nat) -> case n | zero => 0 | succ y => (even y); @@ -200,7 +202,7 @@ let _ = test_eval_eqv_named | zero => 1 | succ y => (odd y);")

- "(odd one); (even one); (odd two); (even two);" + "odd one; even one; odd two; even two;"

"1; 0; 0; 1"

@@ -212,9 +214,9 @@ let _ = test_eval_eqv_named add = lambda x y -> (x + y);

inc : Int -> Int; - inc = (add 1);" + inc = add 1;"

- "(inc 1); (inc 2); (inc 3);" + "inc 1; inc 2; inc 3;"

"2; 3; 4"

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