From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/typeops.ml | 59 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 35 insertions(+), 24 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be4c0e1e..25c1cbff 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -69,7 +69,7 @@ let type_of_type u = mkType uu let type_of_sort = function - | Prop c -> type1 + | Prop | Set -> type1 | Type u -> type_of_type u (*s Type of a de Bruijn index. *) @@ -178,11 +178,11 @@ let type_of_apply env func funt argsv argstv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | ((Prop | Set), Set) -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | (Type u1, Set) -> if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -190,9 +190,9 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (Universe.sup u1 u2) @@ -221,7 +221,7 @@ let check_cast env c ct k expected_type = try match k with | VMcast -> - vm_conv CUMUL env ct expected_type + Vconv.vm_conv CUMUL env ct expected_type | DEFAULTcast -> default_conv ~l2r:false CUMUL env ct expected_type | REVERTcast -> @@ -296,13 +296,13 @@ let type_of_case env ci p pt c ct lf lft = rslty let type_of_projection env p c ct = - let pb = lookup_projection p env in + let pty = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(MutInd.equal pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + assert(eq_ind (Projection.inductive p) ind); + let ty = Vars.subst_instance_constr u pty in substl (c :: CList.rev args) ty @@ -431,7 +431,28 @@ and execute_recdef env (names,lar,vdef) i = and execute_array env = Array.map (execute env) (* Derived functions *) + +let universe_levels_of_constr env c = + let rec aux s c = + match kind c with + | Const (c, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Sorts.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c + +let check_wellformed_universes env c = + let univs = universe_levels_of_constr env c in + try UGraph.check_declared_universes (universes env) univs + with UGraph.UndeclaredLevel u -> + error_undeclared_universe env u + let infer env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in make_judge constr t @@ -449,11 +470,13 @@ let type_judgment env {uj_val=c; uj_type=t} = {utj_val = c; utj_type = s } let infer_type env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in let s = check_type env constr t in {utj_val = constr; utj_type = s} let infer_v env cv = + let () = Array.iter (check_wellformed_universes env) cv in let jv = execute_array env cv in make_judgev cv jv @@ -461,9 +484,11 @@ let infer_v env cv = let infer_local_decl env id = function | Entries.LocalDefEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalDef (Name id, c, t) | Entries.LocalAssumEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalAssum (Name id, check_assumption env c t) @@ -481,10 +506,6 @@ let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 let judge_of_type u = make_judge (mkType u) (type_of_type u) -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) @@ -528,13 +549,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") -- cgit v1.2.3