Stefan pushed to branch master at Stefan / Typer

Commits: 06c37fc5 by Stefan Monnier at 2017-09-29T00:53:28-04:00 Also apply generalization to inductive type constructors

* src/elab.ml (generalize): Change calling convention. (infer_and_generalize_type, infer_and_generalize_def): Adjust accordingly. (lexp_parse_inductive.make_args): Generalize constructors. (var_of_ovar): Move to lexp.ml.

* src/opslexp.ml (check', get_type): Fix scoping of `level` in Inductive.

* btl/builtins.typer (Eq_comm): Take advantage of improvements in gneralization and unification.

* btl/pervasive.typer (BoolMod): Avoid `typecons`'s generalizing. (LList): New type, to test typecons's generalization.

* src/lexp.ml (var_of_ovar): Move from elab.ml. (lexp_unparse): Simplify.

* src/pexp.ml (pexp_u_ind_arg): Remove.

- - - - -

6 changed files:

- btl/builtins.typer - btl/pervasive.typer - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -52,10 +52,12 @@ Eq_cast = Built-in "Eq.cast" ≡> f x -> f y);

%% Commutativity of equality! -Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) - ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; +%% FIXME: I'd like to just say: +%% Eq_comm : (p : Eq ?x ?y) -> Eq ?y ?x`; +Eq_comm : (x : ?t) ≡> (y : ?t) ≡> (p : Eq x y) -> Eq (t := ?t) y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) - (p := p) + %% FIXME: I can't figure out how `(p := p)` + %% gets inferred here, yet it seems to work!?! Eq_refl;

%% General recursion!!

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -70,8 +70,6 @@ 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 f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i); @@ -164,7 +162,9 @@ I x = x; %% Typer generalizes to %% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; %% Which is less general. -K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; +%% FIXME: Change the generalizer to insert the `(b : Type) ≡>` +%% more lazily (i.e. after the `a` argument). +K : ?a -> (b : Type) ≡> b -> ?a; K x y = x;

%%%% Quasi-Quote macro @@ -308,8 +308,22 @@ tail = List_tail; %%%% Tuples

%% Sample tuple: a module holding Bool and its constructors. -BoolMod = (##datacons (typecons _ (cons (t :: ?) (true :: ?) (false :: ?))) - cons) +BoolMod = (##datacons + %% We need the `?` metavars to be lexically outside of the + %% `typecons` expression, otherwise they end up generalized, so + %% we end up with a type constructor like + %% + %% typecons _ (cons (τ₁ : Type) (t : τ₁) + %% (τ₂ : Type) (true : τ₂) + %% (τ₃ : Type) (false : τ₃) + %% + %% And it's actually even worse because it tries to generalize + %% over the level of those `Type`s, so we end up with an invalid + %% inductive type. + ((lambda t1 t2 t3 + -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) + ? ? ?) + cons) (_ := Bool) (_ := true) (_ := false);

Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); @@ -350,9 +364,17 @@ Not : Type -> Type; Not prop = prop -> False;

%% Like Bool, except that it additionally carries the meaning of its value. +%% We don't use the `type` macro here because it would make these `true` +%% and `false` constructors ovrride `Bool`'s, and we currently don't +%% want that. Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop));

+%% Testing generalization in inductive type constructors. +LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient! +type LList (a : Type) n + | vnil (p ::: Eq n 0) + | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!

%%%% If

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -340,12 +340,14 @@ let rec meta_to_var ids o (e : lexp) = (* 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 generalize (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 ( + if mfvs = IMap.empty + then (fun wrap e -> e) (* Nothing to generalize, yay! *) + else let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs -> if sl' < sl then (* This metavar appears in the context, @@ -363,16 +365,18 @@ let generalize wrap (nctx : elab_context) e = mfvs [] in (* FIXME: Sort `mvfs' topologically! *) let len = List.length mfvs in - let e = mkSusp e (S.shift len) in + fun wrap e -> let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); meta_to_var ids 0 e + | [] -> assert (n = 0); + let e = mkSusp e (S.shift len) in + 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) + loop (IMap.empty) len mfvs

(* Infer or check, as the case may be. *) let rec elaborate ctx se ot = @@ -803,24 +807,45 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx =

- let make_args (args:(arg_kind * pvar option * sexp) list) ctx - : (arg_kind * vname option * ltype) list = - let rec loop args acc ctx = - match args with - | [] -> (List.rev acc) - | hd::tl -> begin - match hd with - | (kind, var, exp) -> - let lxp = infer_type exp ctx var in - let nctx = ectx_extend ctx var Variable lxp in - loop tl ((kind, var, lxp)::acc) nctx - end in - loop args [] ctx in - - List.fold_left - (fun lctors ((_, name), args) -> - SMap.add name (make_args args ctx) lctors) - SMap.empty ctors + let make_args (args:(arg_kind * pvar option * sexp) list) ctx + : (arg_kind * vname option * ltype) list = + let nctx = ectx_new_scope ctx in + let rec loop args acc ctx = + match args with + | [] -> let acc = List.rev acc in + (* Convert the list of fields into a Lexp expression. + * The actual expression doesn't matter, as long as its + * scoping is right: we only use it so we can pass it to + * things like `fv` and `meta_to_var`. *) + let altacc = List.fold_right + (fun (ak, n, t) aa + -> Arrow (ak, n, t, dummy_location, aa)) + acc impossible in + let g = generalize nctx altacc in + let altacc' = g (fun _ne vname t l e + -> Arrow (Aerasable, Some vname, t, l, e)) + altacc in + if altacc' == altacc + then acc (* No generalization! *) + else + (* Convert the Lexp back into a list of fields. *) + let rec loop e = match e with + | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | _ -> assert (e = impossible); [] in + loop altacc' + | hd::tl -> begin + match hd with + | (kind, var, exp) -> + let lxp = infer_type exp ctx var in + let nctx = ectx_extend ctx var Variable lxp in + loop tl ((kind, var, lxp)::acc) nctx + end in + loop args [] nctx in + + List.fold_left + (fun lctors ((_, name), args) -> + SMap.add name (make_args args ctx) lctors) + SMap.empty ctors

and track_fv rctx lctx e = let (fvs, (mvs, _)) = OL.fv e in @@ -925,24 +950,27 @@ and infer_and_generalize_type (ctx : elab_context) se oname = 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. *) + * to keep it ungeneralized so we can use `x : ?` to declare that + * `x` will be defined later without specifying its type yet. *) | Metavar _ -> t - | _ -> generalize (fun _ne vname t l e - -> mkArrow (Aerasable, Some vname, t, l, e)) - nctx t + | _ -> let g = generalize nctx t in + g (fun _ne vname t l e + -> mkArrow (Aerasable, Some vname, t, l, e)) + 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') + let g = generalize nctx e in + let e' = g (fun ne vname t l e + -> mkLambda ((if ne then Aimplicit else Aerasable), + vname, t, e)) + e in + let t' = g (fun ne vname t l e + -> mkArrow ((if ne then Aimplicit else Aerasable), + Some vname, t, sexp_location se, e)) + t in + (e', t')

and lexp_decls_1 (sdecls : sexp list) @@ -1332,10 +1360,6 @@ let sform_identifier ctx loc sargs ot = -> (sexp_error loc ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc)

-let var_of_ovar l ov = match ov with - | None -> (l, "<anon>") - | Some v -> v - let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody]

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -205,6 +205,10 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es))

+let var_of_ovar l ov = match ov with + | None -> (l, "<anon>") + | Some v -> v + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -435,21 +439,24 @@ let rec lexp_unparse lxp = let pfargs = List.map (fun (kind, vdef, ltp) -> (kind, vdef, Some (lexp_unparse ltp))) lfargs in

- (* ((arg_kind * vdef option * ltype) list) SMap.t *) - (* (symbol * (arg_kind * pvar option * pexp) list) list *) - let ctors = List.map (fun (str, largs) -> - let pargs = List.map (fun (kind, var, ltp) -> - match var with - | Some (loc, name) -> (kind, Some (loc, name), lexp_unparse ltp) - | None -> (kind, None, lexp_unparse ltp)) largs - in ((loc, str), pargs) - ) (SMap.bindings ctors) in Node (stypecons, Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors) + :: List.map + (fun (name, types) + -> Node (Symbol (loc, name), + List.map + (fun arg -> + match arg with + | (Aexplicit, None, t) -> lexp_unparse t + | (ak, s, t) + -> let (l,_) as id = pexp_u_id s in + Node (Symbol (l, match ak with + | Aexplicit -> "_:_" + | Aimplicit -> "_::_" + | Aerasable -> "_:::_"), + [Symbol id; lexp_unparse t])) + types)) + (SMap.bindings ctors))

| Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -484,18 +484,18 @@ let rec check' erased ctx e = -> let level = SMap.fold (fun _ case level -> - let level, _, _ = + let (level, _, _, _) = List.fold_left - (fun (level, ctx, erased) (ak, v, t) -> - (* FIXME: DB.set_empty seems wrong! *) + (fun (level, ctx, erased, n) (ak, v, t) -> ((match lexp_whnf (check_type erased ctx t) ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> mkSLlub ctx level level' + -> mkSLlub ctx level + (Inverse_subst.apply_inv_subst level' + (S.shift n)) | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -505,8 +505,9 @@ let rec check' erased ctx e = (* U.internal_error "Oops"; *) level), DB.lctx_extend ctx v Variable t, - DB.set_sink 1 erased)) - (level, ctx, erased) + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) case in level) cases (mkSortLevel SLz) in @@ -788,19 +789,22 @@ let rec get_type ctx e = -> let level = SMap.fold (fun _ case level -> - let level, _ = + let (level, _, _) = List.fold_left - (fun (level, ctx) (ak, v, t) -> - (match lexp_whnf (get_type ctx t) ctx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> mkSLlub ctx level level' - | tt -> level), - DB.lctx_extend ctx v Variable t) - (level, ctx) + (fun (level, ctx, n) (ak, v, t) -> + ((match lexp_whnf (get_type ctx t) ctx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (try Inverse_subst.apply_inv_subst level' + (S.shift n) + with _ -> level) + | tt -> level), + DB.lctx_extend ctx v Variable t, + n + 1)) + (level, ctx, 0) case in level) cases (mkSortLevel SLz) in

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -90,15 +90,6 @@ and pexp_p_ind_arg s = match s with -> (Aerasable, pexp_p_id s, t) | _ -> (Aexplicit, None, s)

-and pexp_u_ind_arg arg = match arg with - | (Aexplicit, None, t) -> t - | (k, s, t) - -> let (l,_) as id = pexp_u_id s in - Node (Symbol (l, match k with Aexplicit -> "_:_" - | Aimplicit -> "_::_" - | Aerasable -> "_:::_"), - [Symbol id; t]) - and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s])

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

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