aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/univ.ml16
-rw-r--r--kernel/univ.mli9
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml7
-rw-r--r--pretyping/cases.ml9
-rw-r--r--pretyping/evarconv.ml49
-rw-r--r--pretyping/evarutil.ml42
-rw-r--r--pretyping/evarutil.mli7
-rw-r--r--pretyping/evd.ml91
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/pretyping.ml25
-rw-r--r--pretyping/termops.ml5
-rw-r--r--pretyping/termops.mli1
12 files changed, 167 insertions, 97 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e31e2be689..660e39e637 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -54,6 +54,11 @@ module UniverseLevel = struct
end
module UniverseLMap = Map.Make (UniverseLevel)
+module UniverseLSet = Set.Make (UniverseLevel)
+
+type universe_level = UniverseLevel.t
+
+let compare_levels = UniverseLevel.compare
(* An algebraic universe [universe] is either a universe variable
[UniverseLevel.t] or a formal universe known to be greater than some
@@ -71,7 +76,13 @@ type universe =
| Atom of UniverseLevel.t
| Max of UniverseLevel.t list * UniverseLevel.t list
-let make_univ (m,n) = Atom (UniverseLevel.Level (m,n))
+let make_universe_level (m,n) = UniverseLevel.Level (m,n)
+let make_universe l = Atom l
+let make_univ c = Atom (make_universe_level c)
+
+let universe_level = function
+ | Atom l -> Some l
+ | Max _ -> None
let pr_uni_level u = str (UniverseLevel.to_string u)
@@ -500,9 +511,6 @@ let merge_constraints c g =
(* Normalization *)
-module UniverseLSet =
- Set.Make (UniverseLevel)
-
let lookup_level u g =
try Some (UniverseLMap.find u g) with Not_found -> None
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e19a4c43a7..2f99e16ec7 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -8,8 +8,11 @@
(** Universes. *)
+type universe_level
type universe
+module UniverseLSet : Set.S with type elt = universe_level
+
(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
@@ -17,12 +20,17 @@ val type0m_univ : universe (** image of Prop in the universes hierarchy *)
val type0_univ : universe (** image of Set in the universes hierarchy *)
val type1_univ : universe (** the universe of the type of Prop/Set *)
+val make_universe_level : Names.dir_path * int -> universe_level
+val make_universe : universe_level -> universe
val make_univ : Names.dir_path * int -> universe
val is_type0_univ : universe -> bool
val is_type0m_univ : universe -> bool
val is_univ_variable : universe -> bool
+val universe_level : universe -> universe_level option
+val compare_levels : universe_level -> universe_level -> int
+
(** The type of a universe *)
val super : universe -> universe
@@ -82,6 +90,7 @@ val no_upper_constraints : universe -> constraints -> bool
(** {6 Pretty-printing of universes. } *)
+val pr_uni_level : universe_level -> Pp.std_ppcmds
val pr_uni : universe -> Pp.std_ppcmds
val pr_universes : universes -> Pp.std_ppcmds
val pr_constraints : constraints -> Pp.std_ppcmds
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 28bf6e64d0..509a4e9e5f 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -159,9 +159,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let c = constr_of_global ref in
make_judge c (Retyping.get_type_of env Evd.empty c)
- let pretype_sort = function
+ let pretype_sort evdref = function
| GProp c -> judge_of_prop_contents c
- | GType _ -> judge_of_new_Type ()
+ | GType _ -> evd_comb0 judge_of_new_Type evdref
let split_tycon_lam loc env evd tycon =
let rec real_split evd c =
@@ -307,7 +307,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref fixj tycon
| GSort (loc,s) ->
- inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+ let s' = pretype_sort evdref s in
+ inh_conv_coerce_to_tycon loc env evdref s' tycon
| GApp (loc,f,args) ->
let length = List.length args in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8e0d28fbfb..5e2c0729c8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -948,7 +948,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
let pred= abstract_predicate env !evdref indf current dep tms p in
(pred, whd_betaiota !evdref
- (applist (pred, realargs@[current])), new_Type ())
+ (applist (pred, realargs@[current])))
let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
match typ, oldtyp with
@@ -1164,7 +1164,7 @@ and match_current pb tomatch =
(* We build the (elementary) case analysis *)
let brvals = Array.map (fun (v,_) -> v) brs in
- let (pred,typ,s) =
+ let (pred,typ) =
find_predicate pb.caseloc pb.env pb.evdref
pb.pred current indt (names,dep) pb.tomatch in
let ci = make_case_info pb.env mind pb.casestyle in
@@ -1621,7 +1621,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
(* we use two strategies *)
let sigma,t = match tycon with
| Some (None, t) -> sigma,t
- | _ -> new_evar sigma env ~src:(loc, CasesType) (new_Type ()) in
+ | _ -> new_type_evar sigma env ~src:(loc, CasesType) in
(* First strategy: we build an "inversion" predicate *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
(* Second strategy: we directly use the evar as a non dependent pred *)
@@ -1631,8 +1631,9 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
| Some rtntyp, _ ->
(* We extract the signature of the arity *)
let env = List.fold_right push_rels arsign env in
+ let sigma, newt = new_sort_variable sigma in
let evdref = ref sigma in
- let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in
+ let predcclj = typing_fun (mk_tycon (mkSort newt)) env evdref rtntyp in
let sigma = Option.cata (fun tycon ->
let tycon = lift_tycon_type (List.length arsign) tycon in
Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3906f87288..c5bcb631e7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -26,28 +26,33 @@ type flex_kind_of_term =
| MaybeFlexible of constr (* approx'ed as reducible but not necessarily so *)
| Flexible of existential
-let flex_kind_of_term ts c l =
+let flex_kind_of_term c l =
match kind_of_term c with
- | Const n when is_transparent_constant ts n -> MaybeFlexible c
- | Rel n -> MaybeFlexible c
- | Var id when is_transparent_variable ts id -> MaybeFlexible c
+ | Rel _ | Const _ | Var _ -> MaybeFlexible c
| Lambda _ when l<>[] -> MaybeFlexible c
| LetIn _ -> MaybeFlexible c
| Evar ev -> Flexible ev
| Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid c
- | Meta _ | Case _ | Fix _ | Const _ | Var _ -> PseudoRigid c
+ | Meta _ | Case _ | Fix _ -> PseudoRigid c
| Cast _ | App _ -> assert false
let is_rigid = function Rigid _ -> true | _ -> false
-let eval_flexible_term env c =
+let eval_flexible_term ts env c =
match kind_of_term c with
- | Const c -> constant_opt_value env c
+ | Const c ->
+ if is_transparent_constant ts c
+ then constant_opt_value env c
+ else None
| Rel n ->
(try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
with Not_found -> None)
| Var id ->
- (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
+ (try
+ if is_transparent_variable ts id then
+ let (_,v,_) = lookup_named id env in v
+ else None
+ with Not_found -> None)
| LetIn (_,b,_,c) -> Some (subst1 b c)
| Lambda _ -> Some c
| _ -> assert false
@@ -194,7 +199,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Evar must be undefined since we have flushed evars *)
- match (flex_kind_of_term ts term1 l1, flex_kind_of_term ts term2 l2) with
+ match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =
@@ -249,7 +254,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
else (i,false)
and f2 i =
- match eval_flexible_term env flex2 with
+ match eval_flexible_term ts env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
@@ -281,7 +286,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
else (i,false)
and f2 i =
- match eval_flexible_term env flex1 with
+ match eval_flexible_term ts env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
@@ -324,20 +329,20 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
usable as a canonical projection *)
if isLambda flex1 or is_open_canonical_projection i appr2
then
- match eval_flexible_term env flex1 with
+ match eval_flexible_term ts env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None ->
- match eval_flexible_term env flex2 with
+ match eval_flexible_term ts env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
else
- match eval_flexible_term env flex2 with
+ match eval_flexible_term ts env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None ->
- match eval_flexible_term env flex1 with
+ match eval_flexible_term ts env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
@@ -411,7 +416,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(try conv_record ts env i (check_conv_record appr1 appr2)
with Not_found -> (i,false))
and f4 i =
- match eval_flexible_term env flex1 with
+ match eval_flexible_term ts env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
| None -> (i,false)
@@ -423,7 +428,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(try conv_record ts env i (check_conv_record appr2 appr1)
with Not_found -> (i,false))
and f4 i =
- match eval_flexible_term env flex2 with
+ match eval_flexible_term ts env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
| None -> (i,false)
@@ -434,7 +439,14 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
match kind_of_term c1, kind_of_term c2 with
| Sort s1, Sort s2 when l1=[] & l2=[] ->
- (evd, base_sort_cmp pbty s1 s2)
+ (try
+ let evd' =
+ if pbty = CONV
+ then Evd.set_eq_sort evd s1 s2
+ else Evd.set_leq_sort evd s1 s2
+ in (evd', true)
+ with Univ.UniverseInconsistency _ -> (evd, false)
+ | _ -> (evd, false))
| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
ise_and evd
@@ -508,7 +520,6 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| (Lambda _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
| _, (Lambda _ | Rel _ | Var _ | Const _ | Evar _) -> assert false
-
end
| PseudoRigid _, Rigid _ -> (evd,false)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 418f683319..b88ea03e19 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1297,7 +1297,7 @@ let status_changed lev (pbty,_,t1,t2) =
(* Util *)
-let check_instance_type conv_algo env evd ev1 t2 =
+let check_instance_type conv_algo pbty env evd ev1 t2 =
let t2 = nf_evar evd t2 in
if has_undefined_evars_or_sorts evd t2 then
(* May contain larger constraints than needed: don't want to
@@ -1309,9 +1309,9 @@ let check_instance_type conv_algo env evd ev1 t2 =
else
let typ1 = existential_type evd ev1 in
let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
- if b then evd else
- user_err_loc (fst (evar_source (fst ev1) evd),"",
- str "Unable to find a well-typed instantiation")
+ if b then evd else
+ user_err_loc (fst (evar_source (fst ev1) evd),"",
+ str "Unable to find a well-typed instantiation")
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
@@ -1334,11 +1334,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
else
add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
| _ ->
- let evd =
- if pbty = Some false then
- check_instance_type conv_algo env evd ev1 t2
- else
- evd in
+ let evd = check_instance_type conv_algo pbty env evd ev1 t2 in
let evd = evar_define ~choose env ev1 t2 evd in
let evi = Evd.find evd evk1 in
if occur_existential evd evi.evar_concl then
@@ -1480,31 +1476,25 @@ let empty_valcon = None
(* Builds a value constraint *)
let mk_valcon c = Some c
-(* Refining an evar to a product
-
- I.e., solve x1..xq |- ?e:T(x1..xq) with e:=Πy:?dom[x1..xq].?rng[x1..xq,y]
- where x1..xq |- ?dom:Type and x1..xq,y |- ?rng:Type
- Note: Declaring any type to be in the sort Type shouldn't be harmful
- since cumulativity now includes Prop and Set in Type...
- It is, but that's not too bad
-
- To do: should we check that T is Type and instantiate it by a sort
- if an evar?
-*)
+let new_type_evar ?src ?filter evd env =
+ let evd', s = new_sort_variable evd in
+ new_evar evd' env ?src ?filter (mkSort s)
let idx = id_of_string "x"
+(* Refining an evar to a product *)
+
let define_pure_evar_as_product evd evk =
let evi = Evd.find_undefined evd evk in
let evenv = evar_unfiltered_env evi in
let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
- let evd1,dom = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
+ let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in
let evd2,rng =
let newenv = push_named (id, None, dom) evenv in
let src = evar_source evk evd1 in
let filter = true::evar_filter evi in
- new_evar evd1 newenv ~src (new_Type()) ~filter in
+ new_type_evar evd1 newenv ~src ~filter in
let prod = mkProd (Name id, dom, subst_var id rng) in
let evd3 = Evd.define evk prod evd2 in
evd3,prod
@@ -1558,13 +1548,15 @@ let define_evar_as_lambda env evd (evk,args) =
(* Refining an evar to a sort *)
let define_evar_as_sort evd (ev,args) =
- let s = new_Type () in
- Evd.define ev s evd, destSort s
+ let evd, s = new_sort_variable evd in
+ Evd.define ev (mkSort s) evd, s
(* We don't try to guess in which sort the type should be defined, since
any type has type Type. May cause some trouble, but not so far... *)
-let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
+let judge_of_new_Type evd =
+ let evd', s = new_univ_variable evd in
+ evd', Typeops.judge_of_type s
(* Propagation of constraints through application and abstraction:
Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3127d87eda..4d28d66e71 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -34,6 +34,11 @@ val new_evar :
val e_new_evar :
evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
+(** Create a new Type existential variable, as we keep track of
+ them during type-checking and unification. *)
+val new_type_evar :
+ ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+
(** Create a fresh evar in a context different from its definition context:
[new_evar_instance sign evd ty inst] creates a new evar of context
[sign] and type [ty], [inst] is a mapping of the evar context to
@@ -114,7 +119,7 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
(** {6 Value/Type constraints} *)
-val judge_of_new_Type : unit -> unsafe_judgment
+val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
type type_constraint_type = (int * int) option * constr
type type_constraint = type_constraint_type option
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e5347b7f60..4e1795a978 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -210,8 +210,8 @@ module EvarInfoMap = struct
end
module EvarMap = struct
- type t = EvarInfoMap.t * Univ.universes
- let empty = EvarInfoMap.empty, Univ.initial_universes
+ type t = EvarInfoMap.t * (Univ.UniverseLSet.t * Univ.universes)
+ let empty = EvarInfoMap.empty, (Univ.UniverseLSet.empty, Univ.initial_universes)
let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm)
let find (sigma,_) = EvarInfoMap.find sigma
@@ -237,8 +237,8 @@ module EvarMap = struct
EvarInfoMap.is_defined sigma2 k))
let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
- let add_constraints (sigma, sm) cstrs =
- (sigma, Univ.merge_constraints cstrs sm)
+ let add_constraints (sigma, (us, sm)) cstrs =
+ (sigma, (us, Univ.merge_constraints cstrs sm))
end
(*******************************************************************)
@@ -391,7 +391,7 @@ let subst_evar_info s evi =
evar_body = subst_evb evi.evar_body }
let subst_evar_defs_light sub evd =
- assert (Univ.initial_universes = (snd evd.evars));
+ assert (Univ.initial_universes = (snd (snd evd.evars)));
assert (evd.conv_pbs = []);
{ evd with
metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
@@ -490,11 +490,16 @@ let evar_list evd c =
(**********************************************************)
(* Sort variables *)
-let new_sort_variable ({ evars = (sigma,sm) } as d)=
- let u = Termops.new_univ() in
- (Type u, d)
+let new_univ_variable ({ evars = (sigma,(us,sm)) } as d) =
+ let u = Termops.new_univ_level () in
+ let us' = Univ.UniverseLSet.add u us in
+ ({d with evars = (sigma, (us', sm))}, Univ.make_universe u)
+
+let new_sort_variable d =
+ let (d', u) = new_univ_variable d in
+ (d', Type u)
-let is_sort_variable {evars=(_,sm)} s = match s with Type _ -> true | _ -> false
+let is_sort_variable {evars=(_,(us,_))} s = match s with Type u -> true | _ -> false
let whd_sort_variable {evars=(_,sm)} t = t
let univ_of_sort = function
@@ -502,26 +507,56 @@ let univ_of_sort = function
| Prop Pos -> Univ.type0_univ
| Prop Null -> Univ.type0m_univ
-let set_leq_sort d s1 s2 =
- if s1 = s2 then d
+let is_eq_sort s1 s2 =
+ if s1 = s2 then None
else
let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in
+ if u1 = u2 then None
+ else Some (u1, u2)
+
+let is_univ_var_or_set u =
+ Univ.is_univ_variable u || u = Univ.type0_univ
+
+let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
+ match is_eq_sort s1 s2 with
+ | None -> d
+ | Some (u1, u2) ->
match s1, s2 with
| Prop c, Prop c' ->
if c = Null && c' = Pos then d
else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)))
- | _, _ ->
- add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
-
-let set_eq_sort d s1 s2 =
- if s1 = s2 then d
- else
- let u1, u2 = univ_of_sort s1, univ_of_sort s2 in
+ | Type u, Prop c ->
+ if c = Pos then
+ add_constraints d (Univ.enforce_geq Univ.type0_univ u Univ.empty_constraint)
+ else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+ | _, Type u ->
+ if is_univ_var_or_set u then
+ add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
+ else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+
+let is_univ_level_var us u =
+ match Univ.universe_level u with
+ | Some u -> Univ.UniverseLSet.mem u us
+ | None -> false
+
+let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
+ match is_eq_sort s1 s2 with
+ | None -> d
+ | Some (u1, u2) ->
match s1, s2 with
- | Prop c, Prop c' -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
- | _, _ ->
+ | Prop c, Type u when is_univ_level_var us u ->
add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
-
+ | Type u, Prop c when is_univ_level_var us u ->
+ add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+ | Type u, Type v when (is_univ_level_var us u) || (is_univ_level_var us v) ->
+ add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+ | Prop c, Type u when is_univ_var_or_set u &&
+ Univ.check_eq sm u1 u2 -> d
+ | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d
+ | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
+ add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+ | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
+
(**********************************************************)
(* Accessing metas *)
@@ -717,7 +752,7 @@ let pr_evar_info evi =
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
-let pr_evar_map_t (evars,univs as sigma) =
+let pr_evar_map_t (evars,(uvs,univs) as sigma) =
let evs =
if evars = EvarInfoMap.empty then mt ()
else
@@ -726,11 +761,16 @@ let pr_evar_map_t (evars,univs as sigma) =
(fun (ev,evi) ->
h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
(EvarMap.to_list sigma))++fnl()
- and cs =
+ and svs =
+ if Univ.UniverseLSet.is_empty uvs then mt ()
+ else str"UNIVERSE VARIABLES:"++brk(0,1)++
+ h 0 (prlist_with_sep pr_fnl
+ (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl()
+ and cs =
if univs = Univ.initial_universes then mt ()
else str"UNIVERSES:"++brk(0,1)++
h 0 (Univ.pr_universes univs)++fnl()
- in evs ++ cs
+ in evs ++ svs ++ cs
let pr_constraints pbs =
h 0
@@ -749,8 +789,7 @@ let pr_evar_map evd =
let pp_evm =
if evd.evars = EvarMap.empty then mt() else
pr_evar_map_t evd.evars++fnl() in
- let cstrs =
- if evd.conv_pbs = [] then mt() else
+ let cstrs = if evd.conv_pbs = [] then mt() else
str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
let pp_met =
if evd.metas = Metamap.empty then mt() else
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 29c505d92f..bb345580ee 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -247,7 +247,8 @@ val subst_defined_metas : metabinding list -> constr -> constr option
(*********************************************************
Sort variables *)
-val new_sort_variable : evar_map -> sorts * evar_map
+val new_univ_variable : evar_map -> evar_map * Univ.universe
+val new_sort_variable : evar_map -> evar_map * sorts
val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3b8dbc204..aefa7dfd43 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -292,12 +292,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let c = constr_of_global ref in
make_judge c (Retyping.get_type_of env Evd.empty c)
- let pretype_sort = function
+ let pretype_sort evdref = function
| GProp c -> judge_of_prop_contents c
- | GType _ -> judge_of_new_Type ()
+ | GType _ -> evd_comb0 judge_of_new_Type evdref
exception Found of fixpoint
+ let new_type_evar evdref env loc =
+ evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
+
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
@@ -327,8 +330,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ty =
match tycon with
| Some (None, ty) -> ty
- | None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+ | None | Some _ -> new_type_evar evdref env loc in
let k = MatchingVar (someta,n) in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
@@ -337,7 +339,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+ new_type_evar evdref env loc in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
| GRec (loc,fixkind,names,bl,lar,vdef) ->
@@ -404,7 +406,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref fixj tycon
| GSort (loc,s) ->
- inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+ let j = pretype_sort evdref s in
+ inh_conv_coerce_to_tycon loc env evdref j tycon
| GApp (loc,f,args) ->
let fj = pretype empty_tycon env evdref lvar f in
@@ -547,9 +550,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let v =
let mis,_ = dest_ind_family indf in
let ci = make_case_info env mis LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|] )
- in
- { uj_val = v; uj_type = ccl })
+ mkCase (ci, p, cj.uj_val,[|f|])
+ in { uj_val = v; uj_type = ccl })
| GIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
@@ -586,8 +588,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| None ->
let p = match tycon with
| Some (None, ty) -> ty
- | None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+ | None | Some _ -> new_type_evar evdref env loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
@@ -674,7 +675,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
{ utj_val = v;
utj_type = s }
| None ->
- let s = new_Type_sort () in
+ let s = evd_comb0 new_sort_variable evdref in
{ utj_val = e_new_evar evdref env ~src:loc (mkSort s);
utj_type = s})
| c ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9888821d14..cd848984d4 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -146,11 +146,12 @@ let print_env env =
let set_module m = current_module := m*)
-let new_univ =
+let new_univ_level =
let univ_gen = ref 0 in
(fun sp ->
incr univ_gen;
- Univ.make_univ (Lib.library_dp(),!univ_gen))
+ Univ.make_universe_level (Lib.library_dp(),!univ_gen))
+let new_univ () = Univ.make_universe (new_univ_level ())
let new_Type () = mkType (new_univ ())
let new_Type_sort () = Type (new_univ ())
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1350743d5d..71e781aeb8 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -14,6 +14,7 @@ open Sign
open Environ
(** Universes *)
+val new_univ_level : unit -> Univ.universe_level
val new_univ : unit -> Univ.universe
val new_sort_in_family : sorts_family -> sorts
val new_Type : unit -> types
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:00:18 +0000