Stefan pushed to branch master at Stefan / Typer

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

- - - - -

5 changed files:

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

Changes:

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

@@ -102,7 +99,7 @@ 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 *) @@ -118,23 +115,26 @@ 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 ectx_extend_anon (ectx: elab_context) (t: lexp) : elab_context = - let ((n, map), lctx, f) = ectx in - ((n + 1, map), lexp_ctx_cons lctx 0 None Variable t, f) - 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 @@ -145,20 +145,12 @@ 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 ((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 @@ -170,15 +162,14 @@ let print_lexp_ctx (ctx : lexp_context) = 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 @@ -196,8 +187,7 @@ let print_lexp_ctx (ctx : lexp_context) = | [] -> () | hd::tl ->(

- 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 *) @@ -205,7 +195,8 @@ let print_lexp_ctx (ctx : lexp_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 *) @@ -234,13 +225,6 @@ let print_lexp_ctx (ctx : lexp_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 lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ((loc, ename), dbi) = v in @@ -248,13 +232,20 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = 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!")

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -298,7 +298,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 @@ -308,7 +308,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) @@ -694,7 +694,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 @@ -779,16 +780,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"; "-- --" + | 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 @@ -75,22 +75,39 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list

-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 * @@ -162,7 +179,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)) @@ -176,9 +193,7 @@ 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 = match ovar with - | None -> ectx_extend_anon ctx ltp - | Some var -> env_extend ctx var Variable ltp in + let nctx = ectx_extend ctx ovar Variable ltp in

let lxp, _ = lexp_infer expr nctx in

@@ -199,8 +214,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 @@ -240,12 +259,30 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = | _ -> lexp_error loc "Not an Inductive Type"; [], [] 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

@@ -405,7 +442,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) | _ -> lexp_fatal (sexp_location sarg) - "Explicit arg to non-function") + ("Explicit arg `" ^ aname ^ "` to non-function (type = " ^ lexp_to_str ltp ^ ")")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with @@ -422,7 +459,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = lexp_print t; print_string "\n"; 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 @@ -498,7 +536,10 @@ 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)) + macro_type) -> ( match macro with | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in @@ -624,11 +665,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

@@ -656,7 +694,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

@@ -673,6 +711,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 *)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -50,6 +50,10 @@ 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) -> @@ -78,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 @@ -181,7 +184,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) @@ -189,8 +192,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 = @@ -235,8 +238,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) @@ -265,7 +271,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 with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -274,33 +280,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 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/commit/40b62b36050d93cc6405803eaae82d457f3b...