Stefan pushed to branch unification at Stefan / Typer

Commits: a707155b by Stefan Monnier at 2016-10-28T14:55:10-04:00 Infer implicit args; Give type to metavars

* src/lexp.ml (lexp): Add type to `Metavar`. (lexp_unparse): (somewhat) Handle Metavar and Sort.

* src/lparse.ml (global_substitution): Move, so elab_check_sort can use it. (mkMetavar): Add type arg. (mkMetalevel, mkMetatype): New functions. (elab_check_sort._lexp_p_infer): Use them. (_lexp_p_check.unify_with_arrow): Use the explicit arg type if present. (elab_check_sort.lexp_call.handle_fun_args): Infer missing implicit arg.

* src/opslexp.ml (lexp_whnf): Rewrite to reduce diff w.r.t `trunk`. (check): Add case of `Metavar`.

* src/unification.ml (mkMetavar): Remove.

* tests/eval_test.ml ("Lists"): Remove explicit-implicit args.

* tests/unify_test.ml: Remove unsupported `case` on integers.

* tests/utest_lib.ml (for_all_tests): Remove try/with which hides the better backtrace one gets with OCAMLRUNPARAM=b.

- - - - -

7 changed files:

- src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml - tests/eval_test.ml - tests/unify_test.ml - tests/utest_lib.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -76,7 +76,9 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) - | Metavar of int * subst * vdef + (* The substitution `s` only applies to the lexp associated + * with the metavar's index (i.e. its "value"), not to the ltype. *) + | Metavar of int * subst * vdef * ltype (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -136,7 +138,7 @@ let rec mkSusp e s = match e with | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v - | Metavar (vn, s', vd) -> Metavar (vn, scompose s' s, vd) + | Metavar (vn, s', vd, t) -> Metavar (vn, scompose s' s, vd, mkSusp t s) | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -289,7 +291,7 @@ let rec lexp_location e = | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> l + | Metavar (_,_,(l,_), _) -> l

(********* Normalizing a term *********) @@ -585,11 +587,19 @@ let rec lexp_unparse lxp = | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch)

- (* - | SortLevel of sort_level - | Sort of U.location * sort *) + (* | _ as e -> Pimm (Symbol(lexp_location e, "<")) *) + + (* FIXME: The cases below are all broken! *) + | Metavar (idx, subst, (loc, name), _) + -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ ">"))

- | _ as e -> Pimm (Symbol(lexp_location e, "Type")) + | SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) + | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), + [pexp_unparse (lexp_unparse sl)]) + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<SortOmega>")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<SortLevel>")) + | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), + [pexp_unparse (lexp_unparse sl)])

let rec subst_string s = match s with | S.Identity -> "Id" @@ -701,7 +711,8 @@ and _lexp_to_str ctx exp =

| Var ((loc, name), idx) -> name ^ (index idx) ;

- | Metavar (idx, subst, (loc, name)) -> "?" ^ name ^ (index idx) (*TODO : print subst*) + | Metavar (idx, subst, (loc, name), _) + -> "?" ^ name ^ (index idx) (*TODO : print subst*)

| Let (_, decls, body) -> (* Print first decls without indent *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -92,12 +92,16 @@ let pexp_fatal = debug_message fatal pexp_name pexp_string let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string

+(* :-( *) +let global_substitution = ref (empty_subst, []) + let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = - match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ltp + | k -> lexp_error l ltp ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ^ lexp_string ltp ^ " : " ^ lexp_string lsort);

let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp @@ -191,17 +195,18 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx)

-(* FIXME: We need to keep track of the type of metavars. We could keep it - * in the `Metavar` constructor of the `lexp` type, but that's risky (it could - * be difficult to make sure it's the same for all occurrences of that - * metavar). *) +let mkMetavar t = + let meta = Unif.create_metavar () in + let name = "__metavar" (* ^ (string_of_int meta) *) in + Metavar (meta, S.Identity, (Util.dummy_location, name), t)

-(* :-( *) -let global_substitution = ref (empty_subst, []) +let mkMetalevel () = + let meta = Unif.create_metavar () in + let name = "__metalevel" (* ^ (string_of_int meta) *) in + Metavar (meta, S.Identity, (Util.dummy_location, name), + Sort (dummy_location, StypeLevel))

-let mkMetavar () = let meta = Unif.create_metavar () - in let name = "__Metavar_" ^ (string_of_int meta) - in Metavar (meta, S.Identity, (Util.dummy_location, name)) +let mkMetatype () = mkMetavar (mkMetalevel ())

let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Debug_fun.do_debug (fun () -> @@ -342,19 +347,18 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Cons(idt, sym), cons_type

| Pmetavar _ - -> let meta = mkMetavar () in (*TODO *) - let type_ = mkMetavar () in - lexp_warning dloc meta "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned"; - (meta, type_) (* FIXME return the right type *) + -> let t = mkMetatype () in + let e = mkMetavar t in + (e, t)

| Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx trace), ltp

| (Plambda _ | Pcase _) - -> let meta = mkMetavar () in - let lxp = _lexp_p_check p meta ctx trace in - (lxp, meta) + -> let t = mkMetatype () in + let lxp = _lexp_p_check p t ctx trace in + (lxp, t)

and lexp_let_decls decls (body: lexp) ctx i = @@ -385,11 +389,17 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = _global_lexp_ctx := ctx; _global_lexp_trace := trace;

- let unify_with_arrow lxp kind subst = - let arg, body = mkMetavar (), mkMetavar () - in let arrow = Arrow (kind, None, arg, Util.dummy_location, body) - in match Unif.unify arrow lxp subst with - | Some(subst) -> global_substitution := subst; arg, body + let unify_with_arrow lxp kind var aty subst = + let body = mkMetatype () in + let arg = match aty with + | None -> mkMetatype () + | Some paty + -> let laty, lasort = lexp_infer paty ctx in + elab_check_sort ctx lasort var laty; + laty in + let arrow = Arrow (kind, None, arg, Util.dummy_location, body) in + match Unif.unify arrow lxp subst with + | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow @@ -401,15 +411,10 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* Read var type from the provided type *) let meta_ctx, _ = !global_substitution in let ltp, lbtp = match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | lxp -> unify_with_arrow lxp kind subst in - - let _ = match aty with - | Some paty - -> let laty, lasort = lexp_infer paty ctx in - elab_check_sort ctx lasort var laty; - () (* FIXME: Check `conv_p aty ltp`! *) - | _ -> () in + | Arrow(kind, _, ltp, _, lbtp) + (* FIXME: Check `conv_p aty ltp`! *) + -> ltp, lbtp + | lxp -> unify_with_arrow lxp kind var aty subst in

let nctx = env_extend ctx var Variable ltp in let lbody = lexp_check body lbtp nctx in @@ -629,10 +634,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((Aexplicit, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | Arrow _ as t -> - debug_messages fatal (sexp_location sarg) "Expected non-explicit arg" [ - "ltype : " ^ (lexp_string t); - "s-exp arg: " ^ (sexp_string sarg);] + | Arrow (kind, _, arg_type, _, ret_type) + -> let larg = mkMetavar arg_type in + handle_fun_args ((kind, larg) :: largs) (sarg::sargs) + (L.mkSusp ret_type (S.substitute larg))

| t -> print_lexp_ctx (ectx_to_lctx ctx);

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -130,7 +130,8 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = +let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = + let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); @@ -146,38 +147,37 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf e' ctx meta_ctx) - | Susp (e, s) -> lexp_whnf (push_susp e s) ctx meta_ctx - | Call (e, []) -> lexp_whnf e ctx meta_ctx + | Some e' -> lexp_whnf e' ctx) + | Susp (e, s) -> lexp_whnf (push_susp e s) ctx + | Call (e, []) -> lexp_whnf e ctx | Call (e, (((_, arg)::args) as xs)) -> - (match lexp_whnf e ctx meta_ctx with + (match lexp_whnf e ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx meta_ctx)), + lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx)), args)) - ctx meta_ctx + ctx | Call (e', xs1) -> Call (e', List.append xs1 xs) | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf e ctx meta_ctx in + let e' = lexp_whnf e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.Cons (L.mkSusp (lexp_whnf arg ctx meta_ctx) (S.shift d), s), + (S.Cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d), s), d + 1)) (S.identity, 0) aargs in - lexp_whnf (push_susp branch subst) ctx meta_ctx + lexp_whnf (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) - ctx meta_ctx + -> lexp_whnf (push_susp default (S.substitute e')) ctx | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); @@ -186,9 +186,13 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> Case (l, e', rt, branches, default)) - | Metavar (idx, _, _) -> lexp_whnf (L.VMap.find idx meta_ctx) ctx meta_ctx + | Metavar (idx, s, _, _) + -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + with Not_found -> e) | e -> e

+ in lexp_whnf e ctx +

(********* Testing if a lexp is properly typed *********)

@@ -408,6 +412,9 @@ let rec check ctx e = | _ -> (U.msg_error "TC" (lexp_location e) "Cons of a non-inductive type!"; B.type_int)) + | Metavar (idx, s, _, t) + -> try check ctx (push_susp (L.VMap.find idx meta_ctx) s) + with Not_found -> t

(*********** Type erasure, before evaluation. *****************)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -9,8 +9,8 @@ open Inverse_subst (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*)

-let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar -let mkMetavar subst vdef = Metavar (create_metavar (), subst, vdef) +let create_metavar () = global_last_metavar := !global_last_metavar + 1; + !global_last_metavar

(* For convenience *) type return_type = (substitution * constraints) option @@ -25,9 +25,10 @@ let associate (meta: int) (lxp: lexp) (subst: substitution) *) let find_or_none (value: lexp) (map: substitution) : lexp option = match value with - | Metavar (idx, _, _) -> (if VMap.mem idx map - then Some (VMap.find idx map) - else None) + | Metavar (idx, _, _, _) + -> if VMap.mem idx map + then Some (VMap.find idx map) + else None | _ -> None

(** Zip while applying a function, returns <code>None</code> list if l1 & l2 have different size*) @@ -215,15 +216,15 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type match find_or_none metavar s with | Some (lxp_) -> unify lxp_ lxp s | None -> (match metavar with - | Metavar (_, subst_, _) -> (match inverse subst_ with + | Metavar (_, subst_, _, _) -> (match inverse subst_ with | Some s' -> Some (associate value (mkSusp lxp s') s, []) | None -> None) | _ -> None) in match (meta, lxp) with - | (Metavar (val1, s1, _), Metavar (val2, s2, _)) when val1 = val2 -> + | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 -> Some ((subst, [])) - | (Metavar (v, s1, _), _) -> find_or_unify meta v lxp subst + | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst | (_, _) -> None

(** Unify a Call (call) and a lexp (lxp)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -226,14 +226,16 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lists"

- "my_list = cons (a := Int) 1 - (cons (a := Int) 2 - (cons (a := Int) 3 - (cons (a := Int) 4 (nil (a := Int)))))" - - "length (a := Int) my_list; - head (a := Int) my_list; - head (a := Int) (tail (a := Int) my_list)" + (* FIXME: This doesn't signal an error, even we don't yet have the code + * to handle the `nil` below! *) + "my_list = cons 1 + (cons 2 + (cons 3 + (cons 4 nil)))" + + "length my_list; + head my_list; + head (tail my_list)"

"4; 1; 2"

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -61,13 +61,12 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" -let str_case = "i = case 0 -| 1 => 2 -| 0 => 42 -| _ => 5" -let str_case2 = "i = case 0 -| 0 => 12 -| _ => 12" +let str_case = "i = case True +| True => 2 +| False => 42" +let str_case2 = "i = case nil(a := Int) +| 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;" @@ -166,7 +165,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::(input_type , input_type_t , Equivalent) (* 44 *)

- ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) + ::(Metavar (0, S.Identity, (Util.dummy_location, "M"), type0), + Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *)

::[]

@@ -179,7 +179,7 @@ let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = | None -> (Nothing, res, lxp1, lxp2) in tmp

-let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = +let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: substitution): bool = let r, _, _, _ = test_input lxp1 lxp2 subst in if r = res then true else false

===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -182,16 +182,16 @@ let for_all_tests sk tmap tk = if (must_run_title tk) then ( let tv = StringMap.find tk tmap in flush stdout; - try + (* try *) let r = tv () in if r = 0 then( ut_string2 (green ^ "[ OK] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset)) else( ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset); _ret_code := failure ()) - with e -> - _ret_code := failure (); - unexpected_throw sk tk e) else () + (* with e -> + * _ret_code := failure (); + * unexpected_throw sk tk e *)) else ()

let for_all_sections sk = let tmap, tst = StringMap.find sk (!_global_sections) in

View it on GitLab: https://gitlab.com/monnier/typer/commit/a707155bbc7c5eeb6bdd6e70adcd07f2dede...