Stefan pushed to branch master at Stefan / Typer

Commits: 7562d475 by Stefan Monnier at 2017-12-04T22:59:32-05:00 Verify and try to arrange that TypeLevel args come first

* btl/builtins.typer (Eq_cast): Simplify the type annotation yet a bit more.

* src/elab.ml (move_typelevel_to_front): New function. (generalize): Use it.

* src/opslexp.ml (sort_compose): Make it do more work. Properly enforce that TypeLevel args need to come first. (check', get_type): Adjust and simplify accordingly.

- - - - -

3 changed files:

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

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -46,7 +46,7 @@ Eq_refl = Built-in "Eq.refl";

Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) - ≡> (l : TypeLevel) ≡> (f : ? -> Type_ l) + ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say: %% Eq_cast : (p : Eq ?x ?y) ≡> ?f ?x -> ?f ?y;

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -337,6 +337,17 @@ let rec meta_to_var ids o (e : lexp) = | _ -> e in loop e

+let move_typelevel_to_front ctx mfvs = + (* TypeLevel arguments have to come first, so move them accordingly. *) + List.sort + (fun (id1, vname1, mt1) (id2, vname2, mt2) + -> let tl1 = OL.conv_p ctx mt1 type_level in + let tl2 = OL.conv_p ctx mt2 type_level in + if tl1 + then if tl2 then 0 else -1 + else if tl2 then 1 else 0) + mfvs + (* Generalize expression `e` with respect to its uninstantiated metavars. * `wrap` is the function that adds the relevant quantification, typically * either mkArrow or mkLambda. *) @@ -365,6 +376,7 @@ let generalize (nctx : elab_context) e = mfvs [] in (* FIXME: Sort `mvfs' topologically! *) 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); @@ -1317,8 +1329,7 @@ let sform_identifier ctx loc sargs ot =

| [Symbol (loc, name)] when String.length name >= 1 && String.get name 0 = '?' - -> assert (String.length name >= 1 && String.get name 0 = '?'); - let name = if name = "?" then "" else + -> let name = if name = "?" then "" else string_sub name 1 (String.length name) in (* Shift the var so it can't refer to the local vars. * This is used so that in cases like "lambda t (y : ?) ... "

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -335,20 +335,37 @@ let rec mkSLlub ctx e1 e2 = else if level_leq ce2 ce1 then e2 else mkSortLevel (SLlub (e1, e2))

-let sort_compose ctx l s1 s2 = - match s1, s2 with - | (Stype l1, Stype l2) -> Stype (mkSLlub ctx l1 l2) - | ( (StypeLevel, Stype _) - | (StypeLevel, StypeOmega) - (* This is probably safe, but I don't think it adds much power nor - * flexibility, so let's not bother for now: it's easier to add it later - * than to remove it later. - * | (Stype _, StypeOmega) *)) - -> StypeOmega - | _,_ -> (U.msg_error "TC" l - "Mismatch sorts for arg and result"; - StypeOmega) - +type sort_compose_result + = SortResult of ltype + | SortInvalid + | SortK1NotType + | SortK2NotType + +let sort_compose ctx l ak k1 k2 = + (* BEWARE! Technically `k2` can refer to `v`, but this should only happen + * if `v` is a TypeLevel, and in that case sort_compose + * should ignore `k2` and return TypeOmega anyway. *) + let k2 = mkSusp k2 (S.substitute impossible) in + match (lexp_whnf k1 ctx, lexp_whnf k2 ctx) with + | (Sort (_, s1), Sort (_, s2)) + (* FIXME: fix scoping of `k2` and `s2`. *) + -> (match s1, s2 with + | (Stype l1, Stype l2) + -> if ak == P.Aerasable && impredicative_erase + then SortResult k2 + else SortResult (mkSort (l, Stype (mkSLlub ctx l1 l2))) + | (StypeLevel, Stype _) + | (StypeLevel, StypeOmega) + (* This might be safe, but I don't think it adds much power. + * It would add some flexibility, especially w.r.t generalized + * arguments, but let's not bother for now: it's easier to add it + * later than to remove it later. + * | (Stype _, StypeOmega) *) + -> SortResult (mkSort (l, StypeOmega)) + | _ -> SortInvalid) + | (Sort (_, _), _) -> SortK2NotType + | (_, _) -> SortK1NotType + let dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased @@ -435,23 +452,20 @@ let rec check' erased ctx e = | Arrow (ak, v, t1, l, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in - (* BEWARE! `k2` can refer to `v`, but this should only happen - * if `v` is a TypeLevel, and in that case sort_compose - * should ignore `k2` and return TypeOmega anyway. *) let k2 = check_type (DB.set_sink 1 erased) nctx t2 in - let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx, lexp_whnf k2 ctx with - | (Sort (_, s1), Sort (_, s2)) - (* FIXME: fix scoping of `k2` and `s2`. *) - -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel - then k2 - else mkSort (l, sort_compose ctx l s1 s2) - | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) - "Not a proper type"; - mkSort (l, StypeOmega)) - | (_, _) -> (U.msg_error "TC" (lexp_location t1) - "Not a proper type"; - mkSort (l, StypeOmega))) + match sort_compose ctx l ak k1 k2 with + | SortResult k -> k + | SortInvalid + -> U.msg_error "TC" l "Invalid arrow: inner TypelLevel argument"; + mkSort (l, StypeOmega) + | SortK1NotType + -> (U.msg_error "TC" (lexp_location t1) + "Not a proper type"; + mkSort (l, StypeOmega)) + | SortK2NotType + -> (U.msg_error "TC" (lexp_location t2) + "Not a proper type"; + mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, Some v, t, l, @@ -757,17 +771,10 @@ let rec get_type ctx e = (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in - (* BEWARE! `k2` can refer to `v`, but this should only happen - * if `v` is a TypeLevel, and in that case sort_compose - * should ignore `k2` and return TypeOmega anyway. *) let k2 = get_type nctx t2 in - let k2 = mkSusp k2 (S.substitute impossible) in - match lexp_whnf k1 ctx, lexp_whnf k2 ctx with - | (Sort (_, s1), Sort (_, s2)) - -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel - then k2 - else mkSort (l, sort_compose ctx l s1 s2) - | _ -> DB.type0) + match sort_compose ctx l ak k1 k2 with + | SortResult k -> k + | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, Some v, t, l, get_type (DB.lctx_extend ctx (Some v) Variable t)

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

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