Stefan pushed to branch master at Stefan / Typer

Commits: ee53e868 by Stefan Monnier at 2017-09-25T02:21:00Z Generalize non-recursive let-definitions

* btl/pervasive.typer (List_head, List_tail, Sexp_to_list.singleton): Let Typer generalize the definition's type.

* src/elab.ml (newMetalevel): Add a `loc` argument. (generalize): New function, extracted from infer_and_generalize_type. (track_fv): Adjust to new output of `OL.fv`. (infer_and_generalize_type): Use `generalize`. (infer_and_generalize_def): New function. (lexp_decls_1): Use it for non-recursive definitions.

* src/eval.ml (closed_p): Adjust to new output of `OL.fv`.

* src/opslexp.ml (mv_set): Add info to keep track of erasability. (mv_set_erase, fv_erase): New functions. (fv): Use them.

* src/unification.ml (_unify_metavar.unif): Return None in case of failure of inversion.

- - - - -

5 changed files:

- btl/pervasive.typer - src/elab.ml - src/eval.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -55,13 +55,12 @@ List_head1 xs = case xs | nil => none | cons hd tl => some hd;

-List_head : ?a -> List ?a -> ?a; -List_head x = lambda xs -> case xs +List_head x = lambda xs -> case (xs : List ?a) + %% FIXME: We shouldn't need to annotate `xs` above! | cons x _ => x | nil => x;

-List_tail : List ?a -> List ?a; -List_tail xs = case xs +List_tail xs = case (xs : List ?a) % FIXME: Same here. | nil => nil | cons hd tl => tl;

@@ -71,8 +70,8 @@ List_map f = lambda xs -> case xs | cons x xs => cons (f x) (List_map f xs);

List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; -List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) - ≡> (b -> a -> a) -> List b -> a -> a; +%% List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) +%% ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i); @@ -95,9 +94,9 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs %% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>";

-Sexp_to_list : Sexp -> List Sexp -> List Sexp; +%% Sexp_to_list : Sexp -> List Sexp -> List Sexp; Sexp_to_list s = lambda exceptions -> - let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in + let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! Sexp_dispatch s (node := lambda head -> lambda tail

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -236,11 +236,11 @@ let newMetavar (ctx : lexp_context) sl l name t= let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.Identity, (l, name))

-let newMetalevel (ctx : lexp_context) sl = - newMetavar ctx sl Util.dummy_location "l" type_level +let newMetalevel (ctx : lexp_context) sl loc = + newMetavar ctx sl Util.dummy_location "ℓ" type_level

let newMetatype (ctx : lexp_context) sl loc - = newMetavar ctx sl loc "t" (mkSort (loc, Stype (newMetalevel ctx sl))) + = newMetavar ctx sl loc "τ" (mkSort (loc, Stype (newMetalevel ctx sl loc)))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -272,7 +272,7 @@ let elab_varref ctx ((loc, name) as id) (lxp, Inferred ltp)

(* Turn metavar into plain vars after generalization. *) -let rec meta_to_var idxs o (e : lexp) = +let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with | Imm _ -> e | SortLevel SLz -> e @@ -288,14 +288,14 @@ let rec meta_to_var idxs o (e : lexp) = let (_, ndefs) = List.fold_right (fun (l,e,t) (o', defs) -> let o' = o' - 1 in - (o', (l, meta_to_var idxs (len + o) e, - meta_to_var idxs (o' + o) t) :: defs)) + (o', (l, meta_to_var ids (len + o) e, + meta_to_var ids (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var idxs (len + o) e) + mkLet (l, ndefs, meta_to_var ids (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var idxs (1 + o) t2) + -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var idxs (1 + o) e) + -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) | Call (f, args) -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) | Inductive (l, label, args, cases) @@ -303,7 +303,7 @@ let rec meta_to_var idxs o (e : lexp) = let (_, nargs) = List.fold_right (fun (ak, v, t) (o', args) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var idxs (o' + o) t) + (o', (ak, v, meta_to_var ids (o' + o) t) :: args)) args (alen, []) in let ncases @@ -314,7 +314,7 @@ let rec meta_to_var idxs o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var idxs (o' + o) t) + (o', (ak, v, meta_to_var ids (o' + o) t) :: fields)) fields (flen, []) in nfields) @@ -325,18 +325,55 @@ let rec meta_to_var idxs o (e : lexp) = -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var idxs (o + List.length fields) e)) + -> (l, fields, meta_to_var ids (o + List.length fields) e)) cases in mkCase (l, loop e, loop t, ncases, match default with None -> None | Some (v, e) -> Some (v, loop e)) | Metavar (id, s, name) - -> if IMap.mem id idxs then - mkVar (name, o + IMap.find id idxs) + -> if IMap.mem id ids then + mkVar (name, o + IMap.find id ids) else match metavar_lookup id with | MVal e -> loop (push_susp e s) | _ -> e in loop e

+(* Generalize expression `e` with respect to its uninstantiated metavars. + * `wrap` is the function that adds the relevant quantification, typically + * either mkArrow or mkLambda. *) +let generalize wrap (nctx : elab_context) e = + let l = lexp_location e in + let sl = ectx_to_scope_level nctx in + let cl = Myers.length (ectx_to_lctx nctx) in + let (_, (mfvs, nes)) = OL.fv e in + if mfvs = IMap.empty then e else ( + let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs + -> if sl' < sl then + (* This metavar appears in the context, + * so we can't generalize over it. *) + fvs + else ( + assert (cl' >= cl); + (idx, vname, + if cl' > cl then + Inverse_subst.apply_inv_subst + mt (S.shift (cl' - cl)) + else + mt) + :: fvs)) + mfvs [] in + (* FIXME: Sort `mvfs' topologically! *) + let len = List.length mfvs in + let e = mkSusp e (S.shift len) in + let rec loop ids n mfvs = match mfvs with + | [] -> assert (n = 0); meta_to_var ids 0 e + | ((id, vname, mt) :: mfvs) + -> let mt' = mkSusp mt (S.shift (len - n)) in + let mt'' = meta_to_var ids (- n) mt' in + let n = n - 1 in + let e' = loop (IMap.add id n ids) n mfvs in + wrap (IMap.mem id nes) vname mt'' l e' in + loop (IMap.empty) len mfvs) + (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = match se with @@ -445,11 +482,12 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) + let l = lexp_location s in match - Unif.unify (mkSort (lexp_location s, - Stype (newMetalevel - (ectx_to_lctx ectx) - (ectx_to_scope_level ectx)))) + Unif.unify (mkSort (l, Stype (newMetalevel + (ectx_to_lctx ectx) + (ectx_to_scope_level ectx) + l))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -484,10 +522,10 @@ and unify_with_arrow ctx tloc lxp kind var aty ^ " does not match"); (mkDummy_type ctx l, mkDummy_type nctx l) | Some ((t1,t2)::_) - -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 - ^ " and " + -> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1 + ^ "\n and:\n " ^ lexp_string t2 - ^ " do not match"); + ^ "\n do not match!"); (mkDummy_type ctx l, mkDummy_type nctx l) | Some [] -> arg, body

@@ -785,7 +823,7 @@ and lexp_parse_inductive ctors ctx = SMap.empty ctors

and track_fv rctx lctx e = - let (fvs, mvs) = OL.fv e in + let (fvs, (mvs, _)) = OL.fv e in let nc = EV.not_closed rctx fvs in if nc = [] && not (IMap.is_empty mvs) then "metavars" @@ -883,48 +921,28 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) decls, ctx_define_rec ectx decls

and infer_and_generalize_type (ctx : elab_context) se oname = - let l = sexp_location se in let nctx = ectx_new_scope ctx in - let sl = ectx_to_scope_level nctx in - let cl = Myers.length (ectx_to_lctx nctx) in let t = infer_type se nctx oname in match OL.lexp_whnf t (ectx_to_lctx ctx) with (* There's no point generalizing a single metavar, and it's useful * to keep it ungeneralized so you can use `x : ?` to declare that * `x` will be defined later. *) | Metavar _ -> t - | _ - -> let (_, mfvs) = OL.fv t in - if mfvs = IMap.empty then t else ( - let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs - -> if sl' < sl then - (* This metavar appears in the context, - * so we can't generalize over it. *) - fvs - else ( - assert (cl' >= cl); - (idx, vname, - if cl' > cl then - Inverse_subst.apply_inv_subst - mt (S.shift (cl' - cl)) - else - mt) - :: fvs)) - mfvs [] in - (* FIXME: Sort `mvfs' topologically! *) - let len = List.length mfvs in - let t = mkSusp t (S.shift len) in - let rec loop idxs n mfvs = match mfvs with - | [] -> assert (n = 0); meta_to_var idxs 0 t - | ((idx, vname, mt) :: mfvs) - -> let mt' = mkSusp mt (S.shift (len - n)) in - let mt'' = meta_to_var idxs (- n) mt' in - let n = n - 1 in - let t' = loop (IMap.add idx n idxs) n mfvs in - mkArrow (Aerasable, Some vname, mt'', l, - t') in - loop (IMap.empty) len mfvs) + | _ -> generalize (fun _ne vname t l e + -> mkArrow (Aerasable, Some vname, t, l, e)) + nctx t

+and infer_and_generalize_def (ctx : elab_context) se = + let nctx = ectx_new_scope ctx in + let (e,t) = infer se nctx in + let e' = generalize (fun ne vname t l e + -> mkLambda ((if ne then Aimplicit else Aerasable), + vname, t, e)) + nctx e in + if e == e' + then (e, t) + (* FIXME: Compute type directly instead of going through `e'`. *) + else (e', OL.get_type (ectx_to_lctx ctx) e')

and lexp_decls_1 (sdecls : sexp list) @@ -989,7 +1007,7 @@ and lexp_decls_1 -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) - let (lexp, ltp) = infer sexp (ectx_new_scope nctx) in + let (lexp, ltp) = infer_and_generalize_def nctx sexp in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(v, mkSusp lexp (S.shift 1), ltp)], sdecls,

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -670,7 +670,7 @@ let not_closed rctx ((o, vm) : DB.set) = match !rc with Vundefined -> i::nc | _ -> nc) vm []

-let closed_p rctx (fvs, mvs) = +let closed_p rctx (fvs, (mvs, _)) = not_closed rctx fvs = [] (* FIXME: Handle metavars! *) && IMap.is_empty mvs

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -624,10 +624,12 @@ let rec list_union l1 l2 = match l1 with | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

type mv_set = (scope_level * ltype * scope_length * vname) IMap.t -let mv_set_empty = IMap.empty -let mv_set_add ms m x = IMap.add m x ms -let mv_set_union : mv_set -> mv_set -> mv_set - = IMap.merge (fun m oss1 oss2 + (* Metavars that appear in non-erasable positions. *) + * unit IMap.t +let mv_set_empty : mv_set = (IMap.empty, IMap.empty) +let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) +let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set + = (IMap.merge (fun _m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 | (_, None) -> oss1 @@ -640,6 +642,9 @@ let mv_set_union : mv_set -> mv_set -> mv_set assert (len1 = len2); assert (name2 = name1)); Some ss1) + ms1 ms2, + IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2) +let mv_set_erase (ms, _nes) = (ms, IMap.empty)

module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but @@ -653,6 +658,7 @@ let fv_union (fv1, mv1) (fv2, mv2) = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) +let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

let rec fv (e : lexp) : (DB.set * mv_set) = let fv' e = match e with @@ -667,18 +673,23 @@ let rec fv (e : lexp) : (DB.set * mv_set) = | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in - let (s, _) - = List.fold_left (fun (s, o) (_, e, t) - -> (fv_union s (fv_union (fv_sink o (fv t)) - (fv e)), + let (fvs, _) + = List.fold_left (fun (fvs, o) (_, e, t) + -> (fv_union fvs (fv_union (fv_erase + (fv_sink o (fv t))) + (fv e)), o - 1)) (fv e, len) defs in - fv_hoist len s + fv_hoist len fvs | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) - | Lambda (_, _, t, e) -> fv_union (fv t) (fv_hoist 1 (fv e)) + | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) | Call (f, args) - -> List.fold_left (fun s (_, arg) - -> fv_union s (fv arg)) + -> List.fold_left (fun fvs (ak, arg) + -> let afvs = fv arg in + fv_union fvs + (if ak = P.Aerasable + then fv_erase afvs + else afvs)) (fv f) args | Inductive (_, _, args, cases) -> let alen = List.length args in @@ -697,22 +708,24 @@ let rec fv (e : lexp) : (DB.set * mv_set) = fv_empty fields))) cases s in fv_hoist alen s - | Cons (t, _) -> fv t + | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) - -> let s = fv_union (fv e) (fv t) in + -> let s = fv_union (fv e) (fv_erase (fv t)) in let s = match def with | None -> s | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in SMap.fold (fun _ (_, fields, e) s -> fv_union s (fv_hoist (List.length fields) (fv e))) cases s - | Metavar (m, s, name) - -> (match metavar_lookup m with + | Metavar (id, s, name) + -> (match metavar_lookup id with | MVal e -> fv (push_susp e s) | MVar (sl, t, cl) - -> let (fvs, mvs) = fv (push_susp t s) in - (fvs, mv_set_add mvs m (sl, t, cl, name))) + -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in + (fvs, mv_set_add mvs id (sl, t, cl, name))) in + (* FIXME: Flush the memoization table whenever the metavar table + * is modified, since that can affect the output of `fv`. *) try LMap.find fv_memo e with Not_found -> let r = fv' e in

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -167,24 +167,25 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | MVal _ -> U.internal_error "`lexp_whnf` returned an instantiated metavar!!" | MVar (_, t, _) -> push_susp t s in - let lxp' = try Inverse_subst.apply_inv_subst lxp s with - | Inverse_subst.Not_invertible - -> print_string "Not_invertible:\n "; - lexp_print lxp; + match Inverse_subst.apply_inv_subst lxp s with + | exception Inverse_subst.Not_invertible + -> print_string "Unification of metavar failed:\n "; + print_string ("?[" ^ subst_string s ^ "]"); print_string "\nAgainst:\n "; - print_string (subst_string s); + lexp_print lxp; print_string "\n"; - lxp in - metavar_table := associate idx lxp' (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + None + | lxp' + -> metavar_table := associate idx lxp' (!metavar_table); + match unify t (OL.get_type ctx lxp) ctx with + | Some [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then

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

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/ee53e86819ca2da07ec4d91725276406c9c7... You're receiving this email because of your account on gitlab.com.