Stefan pushed to branch master at Stefan / Typer

Commits: e938c998 by Stefan Monnier at 2016-09-26T20:29:14-04:00 Make type levels more canonical

* src/lexp.ml (sort_level): Replace SLn with SLz. (lexp_location, _lexp_to_str): Adjust accordingly.

* src/opslexp.ml (sort_level_max): New function. (sort_compose): Use it. (impredicative_erase): New var. (check): Adjust for new SLz. Obey impredicative_erase. Fix level calculation for inductive types.

* src/builtin.ml (type0, type1, type2): Adjust.

- - - - -

4 changed files:

- src/builtin.ml - src/debruijn.ml - src/lexp.ml - src/opslexp.ml

Changes:

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -98,9 +98,12 @@ let dump_predef () =

(* Builtin types *) let dloc = dummy_location -let type0 = Sort (dloc, Stype (SortLevel (SLn 0))) -let type1 = Sort (dloc, Stype (SortLevel (SLn 1))) -let type2 = Sort (dloc, Stype (SortLevel (SLn 2))) +let level0 = SortLevel SLz +let level1 = SortLevel (SLsucc level0) +let level2 = SortLevel (SLsucc level1) +let type0 = Sort (dloc, Stype level0) +let type1 = Sort (dloc, Stype level1) +let type2 = Sort (dloc, Stype level2) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel)

@@ -343,7 +346,7 @@ let declexpr_impl loc largs ctx ftype = let lxp = match env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> lxp | None -> builtin_error loc "no expr available" in - let ltp = env_lookup_type ctx ((loc, vn), vi) in + let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *) lxp, ftype

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -47,7 +47,7 @@ let debruijn_warning = msg_warning "DEBRUIJN" * ---------------------------------- *)

let dloc = dummy_location -let type0 = Sort (dloc, Stype (SortLevel (SLn 0))) +let type0 = Sort (dloc, Stype (SortLevel SLz)) let dltype = type0

type property_key = (int * string) (* rev_dbi * Var name *) @@ -180,8 +180,8 @@ let print_lexp_ctx (ctx : elab_context) = (* let's use myers list order *) let rec extract_names (lst: lexp_context) acc = match lst with - | Mnil-> acc - | Mcons (hd, tl, _, _) -> + | M.Mnil -> acc + | M.Mcons (hd, tl, _, _) -> let name = match hd with | (_, Some (_, name), _, _) -> name | _ -> "" in

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -80,13 +80,24 @@ type ltype = lexp * * unification. *) * | MetaFoF * and subst = lexp VMap.t *) + (* + * The PTS I'm imagining looks like: + * + * S = { TypeLevel, TypeOmega, Type ℓ } + * A = { Level : TypeLevel, Z : Level, S : Level → Level, + * Type : (ℓ : Level) → Type (S ℓ) } + * R = { (TypeLevel, Type ℓ, TypeOmega), + * (TypeLevel, TypeOmega, TypeOmega), + * (Type ℓ, TypeOmega, TypeOmega), + * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } + *) and sort = | Stype of lexp | StypeOmega | StypeLevel and sort_level = - | SLn of int - | SLsucc of lexp + | SLz + | SLsucc of lexp

type varbind = @@ -246,7 +257,7 @@ let rec lexp_location e = match e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e - | SortLevel (SLn _) -> U.dummy_location + | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l | Builtin ((l, _), _) -> l @@ -769,7 +780,7 @@ and _lexp_to_str ctx exp = | Builtin ((_, name), _) -> name

| Sort (_, Stype lvl) -> (match lvl with - | SortLevel (SLn v) -> "Type_" ^ (string_of_int v) + | SortLevel SLz -> "Type_0" | _ -> "Type_?")

| _ -> print_string "Printing Not Implemented"; "-- --"

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -37,7 +37,11 @@ module S = Subst module B = Builtin module DB = Debruijn

-let conv_erase = true (* If true, conv ignores erased terms. *) +(* `conv_erase` is supposed to be safe according to the ICC papers. *) +let conv_erase = true (* Makes conv ignore erased terms. *) + +(* The safety of `impredicative_erase` is unknown. But I like the idea. *) +let impredicative_erase = true (* Allows erasable args to be impredicative. *)

(* Lexp context *)

@@ -185,14 +189,24 @@ let assert_type e t t' = if conv_p t t' then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()

+let rec sort_level_max l1 l2 = match l1, l2 with + | SortLevel SLz, l2 -> l2 + | l1, SortLevel SLz -> l1 + | SortLevel (SLsucc l1), SortLevel (SLsucc l2) + -> SortLevel (SLsucc (sort_level_max l1 l2)) + | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) + -> U.msg_error "TC" (lexp_location l1) + ("Can't compute the max of levels `" + ^ lexp_to_string l1 ^ "` and `" + ^ lexp_to_string l2 ^ "`"); + SortLevel SLz + let sort_compose l s1 s2 = match s1, s2 with - | (Stype (SortLevel (SLn n1)), Stype (SortLevel (SLn n2))) - (* Basic predicativity rule. *) - -> Stype (SortLevel (SLn (max n1 n2))) - | ( (StypeLevel, Stype (SortLevel (SLn _))) + | (Stype l1, Stype l2) -> Stype (sort_level_max l1 l2) + | ( (StypeLevel, Stype _) | (StypeLevel, StypeOmega) - (* | (Sort (_, Stype (SortLevel (SLn _))), Sort (_, StypeOmega)) *)) + | (Stype _, StypeOmega)) -> StypeOmega | _,_ -> (U.msg_error "TC" l "Mismatch sorts for arg and result"; @@ -208,8 +222,8 @@ let rec check ctx e = -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; B.type_int) | SortLevel (_) -> B.type_level - | Sort (l, Stype (SortLevel (SLn n))) - -> Sort (l, Stype (SortLevel (SLn (1 + n)))) + | Sort (l, Stype (SortLevel l1 as sl1)) + -> Sort (l, Stype (SortLevel (SLsucc sl1))) | Sort (_, (StypeOmega|StypeLevel)) -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!"; B.type_omega) @@ -238,7 +252,8 @@ let rec check ctx e = let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in match k1, k2 with | (Sort (_, s1), Sort (_, s2)) - -> Sort (l, sort_compose l s1 s2) + -> if ak == P.Aerasable && impredicative_erase then k2 + else Sort (l, sort_compose l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; Sort (l, StypeOmega)) @@ -270,20 +285,29 @@ let rec check ctx e = "Calling a non function!"; ft)) ft args | Inductive (l, label, args, cases) - -> let rec arg_loop args s ctx = + -> let level = SMap.fold + (fun _ case level -> + List.fold_left + (fun level (ak, _, t) -> + if ak == P.Aerasable && impredicative_erase + then level + else match check ctx t with + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | _ -> U.msg_error "TC" (lexp_location t) + "Field type is not a Type!"; + SortLevel SLz) + level + case) + cases (SortLevel SLz) in + let rec arg_loop args ctx = match args with - | [] -> Sort (l, s) + | [] -> Sort (l, Stype level) | (ak, v, t)::args - -> let s' = match check ctx t with - | Sort (_, s') -> s' - | _ -> (U.msg_error "TC" (lexp_location t) - "Field type is not a Type!"; - Stype (SortLevel (SLn 0))) in - Arrow (ak, Some v, t, lexp_location t, - (* FIXME: `sort_compose` doesn't do what we want! *) - arg_loop args (sort_compose l s s') - (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in + -> Arrow (ak, Some v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx v Variable t)) in + let tct = arg_loop args ctx in (* FIXME: Check cases! *) tct | Case (l, e, it, ret, branches, default)

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