Stefan pushed to branch unification at Stefan / Typer

Commits: 9bb74c93 by Stefan Monnier at 2016-09-29T00:10:31-04:00 * src/opslexp.ml (lookup_type, lookup_value): Move to debruijn.ml

* src/debruijn.ml (_get_env): Remove functions. (env_lookup_by_index, print_lexp_ctx): Change ctx type. (lctx_lookup): Rename from _env_lookup; change ctx type. (lctx_lookup_type, lctx_lookup_value): Move from opslexp.ml; use lctx_lookup. (env_lookup_type, env_lookup_expr): Use them.

- - - - - f49911fd by Stefan Monnier at 2016-09-29T00:41:49-04:00 * src/lparse.ml (_lexp_p_infer) <Parrow>: Also add anon vars to lctx

* src/debruijn.ml (ectx_extend_anon): New function.

* src/lparse.ml (_type_shift): Remove function. (_lexp_p_infer) <Parrow>: Also add anonymous vars to lctx.

- - - - - 8458627d by Stefan Monnier at 2016-09-29T10:51:32-04:00 * src/lparse.ml (_lexp_rec_decl): Call lexp_p_infer with complete context

This fixes an assertion failure in "EVAL - Mutually Recursive Definition".

- - - - - 40b62b36 by Stefan Monnier at 2016-10-01T22:56:56-04:00 Various fixes to type inference and checking

* src/debruijn.ml (StringMap): Delete. Use util.ml's SMap instead. (ectx_extend_anon): Remove. (ectx_extend): New function to replace it. (ectx_extend_rec): Rewrite, using lctx_extend_rec. (print_lexp_ctx): Drop redundant first column. Improve handling of non-let bindings. (_name_error): Remove function, folded into its sole user.

* src/lexp.ml (push_susp): Fix incorrect handling of Inductive's `args` and reversal of field order. (_lexp_to_str): Add parens around arrows. Add missing cases.

* src/lparse.ml (elab_check_def): New function, extracted from ctx_define. (ctx_define): Use it. (ctx_define_rec): New function. (_lexp_p_infer) <Pvar>: Don't blindly catch all exceptions. (_lexp_p_infer) <Parrow>: Use ectx_extend. (_lexp_p_infer) <Pinductive>: Fix ordering of args in the computed type. (_lexp_p_infer) <Pcons>: Fix ordering of return type. (lexp_call): Work around conv_p limitation. (lexp_parse_inductive.make_args.loop): Anonymous fields should also be added to the context.

* src/opslexp.ml (get_vardef): New function. (conv_p') <Arrow>: Use it to handle anonymous args. (sort_level_max): Handle Susp args. (check) [Let]: Bring each binding's type into the overall context. (check) [Call]: Reduce to whnf before checking if it's an Arrow. (check) [Inductive]: Check cases in the proper context.

- - - - - a84525ad by Stefan Monnier at 2016-10-01T23:11:33-04:00 Merge branch 'trunk' into unification

- - - - -

7 changed files:

- src/REPL.ml - src/debruijn.ml - src/debug_util.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -216,7 +216,7 @@ let rec repl i clxp rctx = | "%quit" | "%q" -> () | "%help" | "%h" -> (print_string _help_msg; repl clxp rctx) | "%who" | "%w" -> (print_rte_ctx rctx; repl clxp rctx) - | "%info" | "%i" -> (print_lexp_ctx clxp; repl clxp rctx) + | "%info" | "%i" -> (print_lexp_ctx (ectx_to_lctx clxp); repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace (); repl clxp rctx)

(* command with arguments *)

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -54,9 +54,6 @@ type property_key = (int * string) (* rev_dbi * Var name *) module PropertyMap = Map.Make (struct type t = property_key let compare = compare end)

-module StringMap - = Map.Make (struct type t = string let compare = String.compare end) - (* (* rev_dbi * Var name *) => (name * lexp) *) type property_elem = lexp PropertyMap.t type property_env = property_elem PropertyMap.t @@ -70,7 +67,7 @@ type db_idx = int (* DeBruijn index. *) type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)

(* Map matching variable name and its distance in the current scope *) -type scope = db_ridx StringMap.t (* Map<String, db_ridx>*) +type scope = db_ridx SMap.t (* Map<String, db_ridx>*)

type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope @@ -86,10 +83,9 @@ let ectx_to_lctx (ectx : elab_context) : lexp_context = (* internal definitions * ---------------------------------- *)

-let _make_scope = StringMap.empty +let _make_scope = SMap.empty let _make_senv_type = (0, _make_scope) let _make_myers = M.nil -let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev

(* Public methods: DO USE * ---------------------------------- *) @@ -103,36 +99,42 @@ let get_size ctx = let ((n, _), _, _) = ctx in n (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = let ((n, map), _, _) = ctx in - let raw_idx = n - (StringMap.find name map) - 1 in (* + let raw_idx = n - (SMap.find name map) - 1 in (* if raw_idx > (n - csize) then raw_idx - rof (* Shift if the variable is not bound *) else *) raw_idx

let lexp_ctx_cons (ctx : lexp_context) offset d v t = - assert (offset >= 0 && - (ctx = M.nil || - let (previous_offset, _, _, _) = M.car ctx in + assert (offset >= 0 + && (ctx = M.nil + || let (previous_offset, _, _, _) = M.car ctx in previous_offset >= 0 && previous_offset <= 1 + offset)); M.cons (offset, d, v, t) ctx

let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = lexp_ctx_cons ctx 0 (Some def) v t

- 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 debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); - let nmap = StringMap.add name n map in + let nmap = SMap.add name n map in ((n + 1, nmap), 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 ectx_extend (ectx: elab_context) (def: vdef option) (v: varbind) (t: lexp) + : elab_context = + match def with + | None -> let ((n, map), lctx, f) = ectx in + ((n + 1, map), lexp_ctx_cons lctx 0 None v t, f) + | Some def -> env_extend ectx def v t + let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = let (ctx, _) = List.fold_left @@ -143,40 +145,31 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = - (* FIXME: Use lctx_extend_rec! *) - List.fold_left - (fun (ctx, recursion_offset) (def, e, t) -> - let (loc, name) = def in - let ((n, map), env, f) = ctx in - (try let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); - with Not_found -> ()); - let nmap = StringMap.add name n map in - ((n + 1, nmap), - lexp_ctx_cons env recursion_offset (Some def) (LetDef e) t, - f), - recursion_offset - 1) - (ctx, List.length defs) defs - -let env_lookup_by_index index (ctx: elab_context): env_elem = - (Myers.nth index (_get_env ctx)) + let ((n, senv), lctx, f) = ctx in + let senv', _ = List.fold_left + (fun (senv, i) ((_, vname), _, _) -> + SMap.add vname i senv, i + 1) + (senv, n) defs in + ((n + List.length defs, senv'), lctx_extend_rec lctx defs, f) + +let env_lookup_by_index index (ctx: lexp_context): env_elem = + Myers.nth index ctx

(* Print context *) -let print_lexp_ctx (ctx : elab_context) = - let ((n, map), env, f) = ctx in +let print_lexp_ctx (ctx : lexp_context) = + let n = M.length 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")]; + (Some ('l', 40), "VALUE:TYPE")];

print_string (make_sep '-');

- (* it is annoying to print according to StringMap order *) + (* it is annoying to print according to SMap order *) (* let's use myers list order *) let rec extract_names (lst: lexp_context) acc = match lst with @@ -187,18 +180,14 @@ let print_lexp_ctx (ctx : elab_context) = | _ -> "" in extract_names tl (name::acc) in

- let ord = extract_names env [] in + let ord = extract_names ctx [] 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 " | "; lalign_print_int (n - idx - 1) 7; print_string " | ";

let ptr_str = "" in (*" | | | | " in *) @@ -206,7 +195,8 @@ let print_lexp_ctx (ctx : elab_context) = 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 + | (r, Some (_, name), _, tp) -> r, name, None, tp + | (r, _, _, tp) -> r, "", None, tp in

(* Print env Info *) lalign_print_string name 10; (* name must match *) @@ -235,41 +225,46 @@ let print_lexp_ctx (ctx : elab_context) = _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 ^ """)) - - (* generic lookup *) -let _env_lookup ctx (v: vref): env_elem = - let ((dv_size, _), info_env, _) = ctx in +let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ((loc, ename), dbi) = v in

- try(let ret = (Myers.nth dbi info_env) in + try(let ret = (Myers.nth dbi ctx) in let _ = match ret with | (_, Some (_, name), _, _) -> - (* Check if names match *) - _name_error loc ename name ctx; + (* Check if names match *) + if not (ename = name) then + (print_lexp_ctx ctx; + debruijn_error loc ("DeBruijn index " + ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`")) | _ -> () in

ret) with - Not_found -> debruijn_error loc "DeBruijn index out of bounds!" + Not_found -> debruijn_error loc ("DeBruijn index " + ^ string_of_int dbi ^ " out of bounds!") + +

+let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = + let (_, i) = vref in + let (_, _, _, t) = lctx_lookup ctx vref in + mkSusp t (S.shift (i + 1)) + +let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = + let (_, i) = vref in + match lctx_lookup ctx vref with + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) + | _ -> None

let env_lookup_type ctx (v : vref): lexp = - let (_, idx) = v in - let (_, _, _, ltp) = _env_lookup ctx v in - mkSusp ltp (S.shift (idx + 0)) + lctx_lookup_type (ectx_to_lctx ctx) v

let env_lookup_expr ctx (v : vref): lexp option = - let (_, idx) = v in - let (r, _, lxp, _) = _env_lookup ctx v in - match lxp with - | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) - | _ -> None + lctx_lookup_value (ectx_to_lctx ctx) v

(* replace an expression by another *) (* Most of the time it should be O(1) but it can be O(n) *)

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -345,7 +345,7 @@ let main () = debug_lexp_decls flexps; print_string "\n"));

(if (get_p_option "lctx") then( - print_lexp_ctx nctx; print_string "\n")); + print_lexp_ctx (ectx_to_lctx nctx); print_string "\n"));

let clean_lxp = List.map OL.clean_decls lexps in

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -305,7 +305,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Call (f, args) -> Call (mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) | Inductive (l, label, args, cases) - -> let (_, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) + -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) (s, []) args in let ncases = SMap.map (fun args @@ -315,7 +315,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) (ak, v, mkSusp t s) :: nargs)) (s, []) args in - ncase) + L.rev ncase) cases in Inductive (l, label, nargs, ncases) | Cons (it, name) -> Cons (mkSusp it s, name) @@ -703,7 +703,8 @@ and _lexp_to_str ctx exp = (kind_str k) ^ " " ^ (lexp_to_str expr)

| Arrow(k, None, tp, loc, expr) -> - (lexp_to_str tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_to_str expr) + "(" ^ (lexp_to_str tp) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_to_str expr) ^ ")"

| Lambda(k, (loc, name), ltype, lbody) -> let arg = "(" ^ name ^ " : " ^ (lexp_to_str ltype) ^ ")" in @@ -788,16 +789,17 @@ and _lexp_to_str ctx exp =

| Builtin ((_, name), _) -> name

- | Sort (_, Stype lvl) -> (match lvl with - | SortLevel SLz -> "Type_0" - | _ -> "Type_?") + | Sort (_, Stype (SortLevel SLz)) -> "Type_0" + | Sort (_, Stype _) -> "Type_?" + | Sort (_, StypeOmega) -> "Type_ω" + | Sort (_, StypeLevel) -> "Type_Level"

- | _ -> print_string "Printing Not Implemented\n"; "-- --" + | SortLevel (SLz) -> "<Level0>" + | SortLevel (SLsucc e) -> "<LevelS?>"

and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> let str = str ^ " (" ^ key in - let str = List.fold_left (fun str (k, _, arg) -> str ^ " " ^ (_lexp_to_str ctx arg)) str value in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -77,30 +77,39 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list

-(* This is used to make Type annotation and inferred type having the same index *) -(* since inferred type might need to parse a lambda var to infer the type *) - -let _type_shift tp i = - match tp with - | Var(v, idx) -> Var(v, idx) - | expr -> expr - -let ctx_define (ctx: elab_context) var lxp ltype = - let (_, cctx, _) = ctx in - if OL.conv_p ltype (OL.check cctx lxp) then - env_extend ctx var (LetDef lxp) ltype +let elab_check_def (ctx : lexp_context) var lxp ltype = + if OL.conv_p ltype (OL.check ctx lxp) then + () (* FIXME: Check ltype as well! *) else (print_string "¡¡ctx_define error!!\n"; lexp_print lxp; print_string " !: "; lexp_print ltype; print_string "\nbecause\n"; - lexp_print (OL.check cctx lxp); + lexp_print (OL.check ctx lxp); print_string " != "; lexp_print ltype; print_string "\n"; lexp_fatal (let (l,_) = var in l) "TC error")

+let ctx_define (ctx: elab_context) var lxp ltype = + elab_check_def (ectx_to_lctx ctx) var lxp ltype; + env_extend ctx var (LetDef lxp) ltype + +let ctx_define_rec (ctx: elab_context) decls = + let nctx = ectx_extend_rec ctx decls in + (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is + * convertible to `Type_0`, because it doesn't have access to lctx. + * + * let nlctx = ectx_to_lctx nctx in + * let _ = List.fold_left (fun n (var, lxp, ltp) + * -> elab_check_def nlctx var lxp + * (push_susp ltp (S.shift n)); + * n - 1) + * (List.length decls) + * decls in *) + nctx + (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * @@ -184,7 +193,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = let ltp = env_lookup_type ctx ((loc, name), idx) in lxp, ltp

- with e -> + with Not_found -> (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)) @@ -198,12 +207,9 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in - let nctx, sh = match ovar with - | None -> ctx, 0 - | Some var -> (env_extend ctx var Variable ltp), 1 in + let nctx = ectx_extend ctx ovar Variable ltp in

let lxp, _ = lexp_infer expr nctx in - let lxp = _type_shift lxp sh in

let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -222,8 +228,12 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = ) formal_args in

let nctx = !nctx in - let ltp = List.fold_left (fun tp (kind, _, _) -> - (Arrow(kind, None, type0, tloc, tp))) type0 formal in + let ltp = List.fold_left (fun tp (kind, v, ltp) + -> (Arrow (kind, Some v, ltp, tloc, tp))) + (* FIXME: See OL.check for how to + * compute the real target sort + * (not always type0). *) + type0 (List.rev formal) in

let map_ctor = lexp_parse_inductive ctors nctx i in let v = Inductive(tloc, label, formal, map_ctor) in @@ -255,12 +265,30 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = [], [] in

(* build Arrow type *) - let cons_type = List.fold_left (fun ltp (kind, v, tp) -> - Arrow(kind, v, tp, loc, ltp)) idt (List.rev args) in + let target = if formal = [] then + push_susp idt (S.shift (List.length args)) + else + let targs, _ = + List.fold_right + (fun (ak, v, _) (targs, i) + -> ((ak, Var (v, i)) :: targs, + i - 1)) + formal + ([], List.length formal + List.length args - 1) in + Call (push_susp idt (S.shift (List.length formal + + List.length args)), + targs) in + let cons_type + = List.fold_left (fun ltp (kind, v, tp) + -> Arrow (kind, v, tp, loc, ltp)) + target + (List.rev args) in

(* Add Aerasable argument *) - let cons_type = List.fold_left (fun ltp (kind, v, tp) -> - Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in + let cons_type = List.fold_left + (fun ltp (kind, v, tp) + -> Arrow (Aerasable, Some v, tp, loc, ltp)) + cons_type (List.rev formal) in

Cons(idt, sym), cons_type

@@ -389,18 +417,16 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =

(* make a list of all branches return type *) let texp = ref [] in - let ctx_len = get_size ctx in

(* Read patterns one by one *) let fold_fun (merged, dflt) (pat, exp) = (* Create pattern context *) let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in - let nctx_len = get_size nctx in

(* parse using pattern context *) let exp, ltp = lexp_infer exp nctx in (* we added len(arg) variable int the context *) - texp := (_type_shift ltp (nctx_len - ctx_len))::!texp; + texp := ltp::!texp;

(* Check ltp type. Must be similar to rtype *) (if type_check ltp then () @@ -449,7 +475,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let rec handle_fun_args largs sargs ltp = Debug_fun.do_debug (fun () -> print_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; - print_lexp_ctx ctx; + print_lexp_ctx (ectx_to_lctx ctx); flush stdout; prerr_endline "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<"; print_newline ();();); @@ -464,12 +490,16 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | 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-implicit arg " ^ aname ^ " to non-function")) + | 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-implicit arg `" ^ aname + ^ "` to non-function (type = " ^ lexp_to_str ltp ^ ")")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with @@ -484,9 +514,11 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Expected non-explicit arg" | t -> lexp_print t; print_string "\n"; - print_lexp_ctx ctx; + print_lexp_ctx (ectx_to_lctx ctx); lexp_fatal (sexp_location sarg) - "Explicit arg to non-function") in + ("Explicit arg `" ^ sexp_to_str sarg + ^ "` to non-function (type = " + ^ lexp_to_str ltp ^ ")")) in

let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -567,7 +599,11 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let largs = _lexp_parse_all pargs ctx i in (get_macro_impl loc name) loc largs ctx ltp

- | macro, _ when (macro_disp && (OL.conv_p ltp macro_type))-> ( + | macro, _ when (macro_disp + (* FIXME: This call to lexp_whnf shouldn't be needed! *) + && OL.conv_p (OL.lexp_whnf ltp (ectx_to_lctx ctx) + meta_ctx) + macro_type) -> ( match macro with | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in @@ -627,6 +663,8 @@ and lexp_read_pattern pattern exp target ctx: ("`" ^ lexp_to_str (it) ^ "` is not an inductive type!") in

+ (* FIXME: Don't remove them, add them without names! *) + (* FIXME: Add support for explicit-implicit fields! *) (* Remove non explicit argument. *) let rec remove_nexplicit args acc = match args with @@ -693,11 +731,8 @@ and lexp_parse_inductive ctors ctx i = match hd with | (kind, var, exp) -> let lxp, _ = lexp_parse exp ctx in - match var with - | None -> loop tl ((kind, None, lxp)::acc) ctx - | Some (var) -> - let nctx = env_extend ctx var Variable dltype in - loop tl ((kind, Some var, lxp)::acc) nctx + let nctx = ectx_extend ctx var Variable dltype in + loop tl ((kind, var, lxp)::acc) nctx end in loop args [] ctx in

@@ -725,7 +760,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct | None -> lexp_fatal loc "expression does not exist" | Some lxp -> print_string "\n"; - print_string (lexp_to_string lxp); print_string "\n"; + print_string (lexp_to_str lxp); print_string "\n"; lexp_print lxp; print_string "\n"; lexp_fatal loc "Macro is ill formed" in

@@ -742,6 +777,8 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) =

let ctx = add_property ctx var att fn in

+ (* FIXME: We need to have something in lexp to represent this + * add-attribute operation! *) [], ctx ) (* Standard Macro *) @@ -877,9 +914,7 @@ and _lexp_rec_decl decls ctx i = * i.e let decl parsing *)

(* to compute recursive offset *) - 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 -> @@ -895,23 +930,23 @@ and _lexp_rec_decl decls ctx i = 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 i = ref (1 + List.length decls) in let ctx = List.fold_left (fun vctx decl -> - i := !i + 1; + 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 tctx in lst := ((l, s), lxp, ltp)::!lst; - (env_extend_rec (n - !i + 1) vctx (l, s) (LetDef lxp) ltp) + (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp)

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

(* macros *) | Lmcall (a, sargs) ->

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -45,19 +45,15 @@ let impredicative_erase = true (* Allows erasable args to be impredicative. *)

(* Lexp context *)

-let lookup_type (ctx : DB.lexp_context) vref = - let (_, i) = vref in - let (_, _, _, t) = Myers.nth i ctx in - mkSusp t (S.shift (i + 1)) - -let lookup_value (ctx : DB.lexp_context) vref = - let (_, i) = vref in - match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) - | _ -> None +let lookup_type = DB.lctx_lookup_type +let lookup_value = DB.lctx_lookup_value

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

+let get_vardef lv = match lv with + | Some lv -> lv + | None -> (U.dummy_location, "<anon>") + let rec conv_arglist_p s1 s2 args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) -> @@ -86,8 +82,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = | (e1, Susp (e2, s2')) -> conv_p' s1 (scompose s2' s2) e1 e2 | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) -> ak1 == ak2 && conv_p t11 t21 - && conv_p' (match vd1 with None -> s1 | Some l -> ssink l s1) - (match vd2 with None -> s2 | Some l -> ssink l s2) + && conv_p' (ssink (get_vardef vd1) s1) (ssink (get_vardef vd2) s2) t12 t22 | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && conv_p t1 t2 && conv_p' (ssink l1 s1) (ssink l2 s2) e1 e2 @@ -199,7 +194,7 @@ 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 +let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with | SortLevel SLz, l2 -> l2 | l1, SortLevel SLz -> l1 | SortLevel (SLsucc l1), SortLevel (SLsucc l2) @@ -207,8 +202,8 @@ let rec sort_level_max l1 l2 = match l1, l2 with | _, _ (* 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 ^ "`"); + ^ lexp_to_str l1 ^ "` and `" + ^ lexp_to_str l2 ^ "`"); SortLevel SLz

let sort_compose l s1 s2 = @@ -253,8 +248,11 @@ let rec check ctx e = "Def type is not a type!"; ())); DB.lctx_extend ctx v ForwardRef t) ctx defs in - let _ = List.iter (fun (v, e, t) -> assert_type e t (check tmp_ctx e)) - defs in + let _ = List.fold_left (fun n (v, e, t) + -> assert_type e (push_susp t (S.shift n)) + (check tmp_ctx e); + n - 1) + (List.length defs) defs in let new_ctx = DB.lctx_extend_rec ctx defs in check new_ctx e | Arrow (ak, v, t1, l, t2) @@ -283,7 +281,7 @@ let rec check ctx e = -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) -> let at = check ctx arg in - match ft with + match lexp_whnf ft ctx VMap.empty with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -292,33 +290,40 @@ let rec check ctx e = assert_type arg t1 at; mkSusp t2 (S.substitute arg) | _ -> (U.msg_error "TC" (lexp_location arg) - "Calling a non function!"; ft)) + ("Calling a non function (type = " + ^ lexp_to_str ft ^ ")!"); + ft)) ft args | Inductive (l, label, args, cases) - -> 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 = + -> let rec arg_loop args ctx = match args with - | [] -> Sort (l, Stype level) + | [] + -> let level + = SMap.fold + (fun _ case level -> + List.fold_left + (fun level (ak, _, t) -> + if ak == P.Aerasable && impredicative_erase + then level + else match lexp_whnf (check ctx t) ctx VMap.empty with + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | tt -> U.msg_error "TC" (lexp_location t) + ("Field type " + ^ lexp_to_str t + ^ " is not a Type! (" + ^ lexp_to_str tt ^")"); + DB.print_lexp_ctx ctx; + SortLevel SLz) + level + case) + cases (SortLevel SLz) in + Sort (l, Stype level) | (ak, v, t)::args -> 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) -> let rec call_split e =

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -260,7 +260,7 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () ->

let code = " infinity : Int -> Int; - infinity = lambda (beyond : Int) -> (infinity beyond);" in + infinity = lambda beyond -> infinity beyond;" in

let rctx, lctx = eval_decl_str code lctx rctx in

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