Stefan pushed to branch master at Stefan / Typer

Commits: 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels

(generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us.

- - - - -

2 changed files:

- btl/builtins.typer - src/elab.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@

%%%% Base Types used in builtin functions

+%% Box : Type_ ?ℓ₁ -> Type_ ?ℓ₂; +%% Box = lambda (ℓ₃ : TypeLevel) ≡> typecons (Box (t : Type_ ℓ₃)) (box t); + %% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; %% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel;

===================================== src/elab.ml ===================================== @@ -311,39 +311,142 @@ let elab_varref ctx (loc, name) "` was not declared" ^ relateds); sform_dummy_ret ctx loc)

-(* Turn metavar into plain vars after generalization. *) -let rec meta_to_var ids o (e : lexp) = - let rec loop e = match e with +(* Turn metavar into plain vars after generalization. + * ids: an IMap that maps metavars to their position as argument + * (first arg gets position 0). *) +let rec meta_to_var ids (e : lexp) = + + let count = IMap.cardinal ids in + + (* Yuck! Yuck! Yuck! + * This is very messy. What we need to do starts as follows: + * We have a `Γ ⊢ e : τ` and this `e` contains some metavars `m₁…mₙ : τ₁…τₙ` + * that we want to change into formal arguments, i.e. we want to turn `e` + * into something like + * + * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ + * + * The above substitution is not the usual capture-avoiding substitution + * since it replaces metavars with vars rather than vars with terms. + * It's more like *instanciation* of those metavars. + * And indeed, ideally it should be a simple matter of instanciating + * those metavars with temrs that are variable references. + * + * An important aspect here is that the rest of `e` also needs to be + * changed because it will now live in a new context: + * + * Γ,x₁:τ₁,…,xₙ:τₙ ⊢ e[x₁…xₙ/m₁…mₙ] : τ + * + * So we need to adjust all the variable references in `e` to account for + * that, which we normally do with a simple `S.shift n`. + * + * The first problem comes here: `S.shift n` takes a term from + * `Γ` to `Γ,x₁:τ₁,…,xₙ:τₙ`, making sure it still references the same + * bindings as before, i.e. it makes sure the result *cannot* refer to + * any `x₁…xₙ`! + * I first thought "it's OK, I'll first do the `S.shift n` and I only + * instanciate the metavars afterwards", but that does not help, + * because every reference to a metavar is properly wrapped in a + * pending application of the relevant substitution, so the `S.shift n` + * still applies to it. + * + * For this reason, we have a `loop` below which does the substitution + * of variable references for the metavars (since just instanciating + * the metavars doesn't work). + * + * The second problem comes with the other metavars in `e`. + * There are 3 kinds of metavars in `e`: + * + * A. Those that we want to replace with variable references. + * B. Those that live in some higher enclosing scope. + * C. The "others". + * + * Presumably, we have (A) under control. + * For (B) the situation is easy enough: since they live in a higher + * enlosing scope they can only refer to those variables that exist in + * some prefix of `Γ`, so we just need to apply `S.shift n` to them. + * + * For (C), we'd like those metavars (which originally could refer to + * any var in `Γ`) to now be a able to also refer to any of the + * new vars `x₁…xₙ`. So `S.shift n` is definitely not right for them. + * Instead, I ended up writing `adjust_subst` which hacks up + * the substitution attached to each metavar reference so it can + * now refer to its original context *and* to `x₁…xₙ`. + * + * Arguably, now that we handle (C), we could handle (A) by + * first treating them as (C) and then using instantiation. + * But the code for (A) was already written, and it doesn't seem like + * it would make things any simpler currently. + * + * Note: in the original HM algorithm (and in Twelf), (C) cannot occur + * because every metavariable that's not in (B) is generalized + * (i.e. will be in A). But here we need (C) for cases like: + * + * List : Type ? -> Type ?; + * + * Since the second `?` should not be generalized but should + * be inferred from the definition. I.e. the above should be + * generalized to: + * + * List : (ℓ : TypeLevel) ≡> Type ℓ -> Type ?; + * + * where the remaining `?` will be inferred by unification + * when type-checking the definition of `Box` where ti be unified with `ℓ`, + * the newly introduced variable! + *) + + (* `o` is the binding offset until the root. *) + let rec adjust_subst o s = match s with + | S.Identity n + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Identity (n + count) + else + Identity n + | S.Cons (e, s', n) + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Cons (e, s', n + count) + else + S.Cons (loop o' e, adjust_subst o' s', n) + + (* `o` is the binding depth at which we are relative to the "root" + * of the expression (i.e. where the new vars will be inserted). *) + and loop o e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var _ -> e - | Susp (e, s) -> loop (push_susp e s) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in let (_, ndefs) = List.fold_right (fun (l,e,t) (o', defs) -> let o' = o' - 1 in - (o', (l, meta_to_var ids (len + o) e, - meta_to_var ids (o' + o) t) :: defs)) + (o', (l, loop (len + o) e, + loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var ids (len + o) e) + mkLet (l, ndefs, loop (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) + -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) - -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) = List.fold_right (fun (ak, v, t) (o', args) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: args)) args (alen, []) in let ncases @@ -354,31 +457,29 @@ let rec meta_to_var ids o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: fields)) fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases) - | Cons (t, l) -> mkCons (loop t, l) + | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var ids (o + List.length fields) e)) + -> (l, fields, loop (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)) + mkCase (l, loop o e, loop o t, ncases, + match default with None -> None + | Some (v, e) -> Some (v, loop (1 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + IMap.find id ids) + mkVar (name, o + count - IMap.find id ids) else match metavar_lookup id with - | MVal e -> loop (push_susp e s) - (* FIXME: The substitution applied before calling `meta_to_var` - * make it impossible for the metavar to refer to the newly - * introduced variables. *) - | _ -> e - in loop e + | MVal e -> loop o (push_susp e s) + | _ -> mkMetavar (id, adjust_subst o s, name) + in loop 0 e

let move_typelevel_to_front ctx mfvs = (* TypeLevel arguments have to come first, so move them accordingly. *) @@ -421,17 +522,17 @@ let generalize (nctx : elab_context) e = let len = List.length mfvs in let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> - let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); - let e = mkSusp e (S.shift len) in - meta_to_var ids 0 e + let rec loop ids n mfvs = + assert (n = IMap.cardinal ids); + match mfvs with + | [] -> assert (n = len); + meta_to_var ids 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 mt' = meta_to_var ids 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 + wrap (IMap.mem id nes) vname mt' l e' in + loop (IMap.empty) 0 mfvs

let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/63f7644b69db00b352c60e38bee5ec3908...