Stefan pushed to branch master at Stefan / Typer

Commits: 93cb1223 by Stefan Monnier at 2020-03-18T23:30:00-04:00 Fix up various issues with universe levels

* src/builtin.ml (type_eq): Use `mkVar`.

* src/elab.ml (elaborate): Use `mkVar`. (infer_level): Add suport for ∪ in type level expressions.

* src/lexp.ml (mkSLlub'): Add a crutch. (lexp_unparse, lexp_print): Clarify output of TypeLevel.

* src/opslexp.ml (level_canon, level_leq): Move earlier. (conv_p'): Use to fix handling of `SLlub`. (mkSLlub): Fix thinko. (check'', get_type): Use `mkVar`.

* src/unification.ml (unify): Improve unification of SLlub.

- - - - -

5 changed files:

- src/builtin.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2019 Free Software Foundation, Inc. + * Copyright (C) 2016-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -105,12 +105,12 @@ let type_eq = mkArrow (Aerasable, lv, DB.type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (Var (lv, 0))), dloc, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, mkArrow (Anormal, (dloc, None), - Var (tv, 0), dloc, + mkVar (tv, 0), dloc, mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, - mkSort (dloc, Stype (Var (lv, 3))))))) + mkSort (dloc, Stype (mkVar (lv, 3)))))))

let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2019 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -491,7 +491,7 @@ and get_implicit_arg ctx loc oname t = match try (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = Var ((dloc, Some pname), pidx) in + let default = mkVar ((dloc, Some pname), pidx) in get_attribute ctx loc [default; t] with e -> None with | Some attr @@ -1562,6 +1562,8 @@ let rec infer_level ctx se : lexp = | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) -> mkSortLevel (SLsucc (infer_level ctx se)) + | Node (Symbol (_, "_∪_"), [se1; se2]) + -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in (sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se); newMetavar (ectx_to_lctx ctx) dummy_scope_level (l, None) type_level)

===================================== src/lexp.ml ===================================== @@ -206,6 +206,8 @@ let mkCall (f, es) | _ -> hc (Call (f, es))

let mkSLlub' (e1, e2) = match (e1, e2) with + (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) + | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l | (SortLevel SLz, _) | (_, SortLevel SLz) -> Log.log_fatal ~section:"internal" "lub of SLz" | (SortLevel (SLsucc _), SortLevel (SLsucc _)) @@ -582,7 +584,7 @@ let rec lexp_unparse lxp = -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##Type_ℓ") + | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel") | Sort (l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -904,13 +906,13 @@ and lexp_str ctx (exp : lexp) : string = | Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" - | Sort (_, StypeLevel) -> "##Type_ℓ" + | Sort (_, StypeLevel) -> "##TypeLevel" | Sort (_, StypeOmega) -> "##Type_ω"

| SortLevel (SLz) -> "##TypeLevel.z" | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" | SortLevel (SLlub (e1, e2)) - -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e1 ^ ")" + -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"

and lexp_str_ctor ctx ctors =

===================================== src/opslexp.ml ===================================== @@ -216,6 +216,36 @@ let set_shift s : set_plexp = set_shift_n s 1

(********* Testing if two types are "convertible" aka "equivalent" *********)

+(* Turn e (presumably of type TypeLevel) into a canonical representation, + * which is basically the set of vars it references along with the number of + * `succ` applied to them. + * `c` is the maximum "constant" level that occurs in `e` + * and `m` maps variable indices to the maxmimum depth at which they were + * found. *) +let level_canon e = + let add_var_depth v d ((c,m) as acc) = + let o = try IMap.find v m with Not_found -> -1 in + if o < d then (c, IMap.add v d m) else acc in + + let rec canon e d ((c,m) as acc) = match e with + | SortLevel SLz -> if c < d then (d, m) else acc + | SortLevel (SLsucc e) -> canon e (d + 1) acc + | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + | Var (_, i) -> add_var_depth i d acc + | Metavar (i, s, _) + -> (match metavar_lookup i with + | MVal e -> canon (push_susp e s) d acc + | _ -> add_var_depth (- i) d acc) + | Susp (e, s) -> canon (push_susp e s) d acc + | _ -> (max_int, m) + in canon e 0 (0,IMap.empty) + +let level_leq (c1, m1) (c2, m2) = + c1 <= c2 + && c1 != max_int + && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) + m1 + (* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in @@ -233,13 +263,9 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> (match (sl1, sl2) with | (SLz, SLz) -> true | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 - | (SLlub (sl11, sl12), sl2) - (* FIXME: This should be "<=" rather than equality! *) - -> conv_p sl11 e2' && conv_p sl12 e2' - | (sl1, SLlub (sl21, sl22)) - (* FIXME: This should be "<=" rather than equality! *) - -> conv_p e1' sl21 && conv_p e1' sl22 - | _ -> false) + | _ -> let ce1 = level_canon (L.clean e1') in + let ce2 = level_canon (L.clean e2') in + level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 || (match (s1, s2) with @@ -301,47 +327,17 @@ let conv_p (ctx : DB.lexp_context) e1 e2

(********* Testing if a lexp is properly typed *********)

-(* Turn e (presumably of type TypeLevel) into its canonical representation, - * which is basically the set of vars it references along with the number of - * `succ` applied to them. - * `c` is the maximum "constant" level that occurs in `e` - * and `m` maps variable indices to the maxmimum depth at which they were - * found. *) -let level_canon e = - let add_var_depth v d ((c,m) as acc) = - let o = try IMap.find v m with Not_found -> -1 in - if o < d then (c, IMap.add v d m) else acc in - - let rec canon e d ((c,m) as acc) = match e with - | SortLevel SLz -> if c < d then (d, m) else acc - | SortLevel (SLsucc e) -> canon e (d + 1) acc - | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) - | Var (_, i) -> add_var_depth i d acc - | Metavar (i, s, _) - -> (match metavar_lookup i with - | MVal e -> canon (push_susp e s) d acc - | _ -> add_var_depth (- i) d acc) - | Susp (e, s) -> canon (push_susp e s) d acc - | _ -> (max_int, m) - in canon e 0 (0,IMap.empty) - -let level_leq (c1, m1) (c2, m2) = - c1 <= c2 - && c1 != max_int - && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) - m1 - let rec mkSLlub ctx e1 e2 = match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with - | (SortLevel SLz, e2) -> e2 - | (e1, SortLevel SLz) -> e1 + | (SortLevel SLz, _) -> e2 + | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') -> let ce1 = level_canon (L.clean e1') in let ce2 = level_canon (L.clean e2') in - if level_leq ce1 ce2 then e1 - else if level_leq ce2 ce1 then e2 + if level_leq ce1 ce2 then e2 + else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

type sort_compose_result @@ -360,6 +356,10 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = -> if ak == P.Aerasable && impredicative_erase then SortResult (mkSusp k2 (S.substitute impossible)) else let l2' = (mkSusp l2 (S.substitute impossible)) in + (* print_string ("Normal: " ^ lexp_string l1 ^ " -> " + * ^ lexp_string l2' ^ " ==> " + * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + * ^ "\n"); *) SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) | (StypeLevel, Stype l2) when ak == P.Aerasable && impredicative_universe_poly @@ -367,7 +367,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = * It's pretty powerful, e.g. allows tuples containing * level-polymorphic functions, and makes impredicative-encoding * of data types almost(just?) as flexible as inductive types. *) - -> SortResult (mkSusp k2 (S.substitute DB.level0)) + -> (* print_string ("ImpUniv: " ^ lexp_string k1 ^ " ≡> " + * ^ lexp_string k2 ^ " ==> " + * ^ lexp_string (mkSusp k2 (S.substitute DB.level0)) + * ^ "\n"); *) + SortResult (mkSusp k2 (S.substitute DB.level0)) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -608,7 +612,7 @@ let rec check'' erased ctx e = | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (Var (vdef, 0)) + (S.cons (mkVar (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes | _,_ -> (error_tc ~loc:l @@ -641,7 +645,7 @@ let rec check'' erased ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with @@ -875,7 +879,7 @@ let rec get_type ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with @@ -1007,7 +1011,7 @@ let ctx2tup ctx nctx = SMap.empty), cons_label), List.mapi (fun i (oname, t) - -> (P.Aimplicit, Var (oname, offset - i - 1))) + -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) -> Let (loc, [(name, mkSusp e (S.shift 1), t)],

===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -348,8 +348,13 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs - (* FIXME: Handle SLsub! *) - | _, _ -> None) + | SLlub (l11, l12), SLlub (l21, l22) + -> (* FIXME: This SLlub representation needs to be + * more "canonicalized" otherwise it's too restrictive! *) + (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with + | (Some cs1, Some cs2) -> Some (cs1 @ cs2) + | _ -> None) + | _, _ -> None) | _, _ -> None

(** Unify a Sort and a lexp

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93cb1223b53de871422205d2635b24a1e9...