aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli2
-rw-r--r--engine/evd.ml25
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/uState.ml92
-rw-r--r--engine/uState.mli8
-rw-r--r--kernel/univ.mli1
-rw-r--r--plugins/funind/functional_principles_types.ml15
-rw-r--r--plugins/funind/recdef.ml5
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--test-suite/output/UnivBinders.out6
-rw-r--r--test-suite/output/UnivBinders.v6
-rw-r--r--vernac/class.ml3
-rw-r--r--vernac/command.ml7
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/vernacentries.ml2
19 files changed, 111 insertions, 83 deletions
diff --git a/API/API.mli b/API/API.mli
index 83f4a3c50..bb644c388 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2308,7 +2308,7 @@ sig
val universe_context_set : evar_map -> Univ.ContextSet.t
val evar_ident : evar -> evar_map -> Names.Id.t option
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
- val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map ->
+ val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
(Names.Id.t * Univ.Level.t) list * Univ.UContext.t
val nf_constraints : evar_map -> evar_map
val from_ctx : UState.t -> evar_map
diff --git a/engine/evd.ml b/engine/evd.ml
index 06b257a9e..f1b5419de 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -748,27 +748,10 @@ let evar_universe_context d = d.universes
let universe_context_set d = UState.context_set d.universes
-let universe_context ?names evd = UState.universe_context ?names evd.universes
-
-open Misctypes
-type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let check_implication evd cstrs ctx =
- let uctx = evar_universe_context evd in
- let gr = UState.initial_graph uctx in
- let grext = UGraph.merge_constraints cstrs gr in
- let cstrs' = Univ.UContext.constraints ctx in
- if UGraph.check_constraints cstrs' grext then ()
- else CErrors.user_err ~hdr:"check_univ_decl"
- (str "Universe constraints are not implied by the ones declared.")
-
-let check_univ_decl evd decl =
- let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in
- let pl, ctx = universe_context ?names:pl evd in
- if not decl.univdecl_extensible_constraints then
- check_implication evd decl.univdecl_constraints ctx;
- pl, ctx
+let universe_context ~names ~extensible evd =
+ UState.universe_context ~names ~extensible evd.universes
+
+let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
let restrict_universe_context evd vars =
{ evd with universes = UState.restrict evd.universes vars }
diff --git a/engine/evd.mli b/engine/evd.mli
index 8c3771cd9..abcabe815 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -547,15 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
val evar_universe_context : evar_map -> evar_universe_context
val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : ?names:(Id.t located) list -> evar_map ->
+val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
(Id.t * Univ.Level.t) list * Univ.universe_context
val universe_subst : evar_map -> Universes.universe_opt_subst
val universes : evar_map -> UGraph.t
-type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context
+val check_univ_decl : evar_map -> UState.universe_decl ->
+ Universes.universe_binders * Univ.universe_context
val merge_universe_context : evar_map -> evar_universe_context -> evar_map
val set_universe_context : evar_map -> evar_universe_context -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 979a9b086..13a9bb373 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -257,41 +257,63 @@ let pr_uctx_level uctx =
with Not_found | Option.IsNone ->
Universes.pr_with_global_universes l
-let universe_context ?names ctx =
- match names with
- | None -> [], Univ.ContextSet.to_context ctx.uctx_local
- | Some pl ->
- let levels = Univ.ContextSet.levels ctx.uctx_local in
- let newinst, map, left =
- List.fold_right
- (fun (loc,id) (newinst, map, acc) ->
- let l =
- try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
- with Not_found ->
- user_err ?loc ~hdr:"universe_context"
- (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
- in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
- pl ([], [], levels)
- in
- if not (Univ.LSet.is_empty left) then
- let n = Univ.LSet.cardinal left in
- let loc =
- try
- let info =
- Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
- info.uloc
- with Not_found -> None
- in
- user_err ?loc ~hdr:"universe_context"
- ((str(CString.plural n "Universe") ++ spc () ++
- Univ.LSet.pr (pr_uctx_level ctx) left ++
- spc () ++ str (CString.conjugate_verb_to_be n) ++
- str" unbound."))
- else
- let inst = Univ.Instance.of_array (Array.of_list newinst) in
- let ctx = Univ.UContext.make (inst,
- Univ.ContextSet.constraints ctx.uctx_local)
- in map, ctx
+type universe_decl =
+ (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let universe_context ~names ~extensible ctx =
+ let levels = Univ.ContextSet.levels ctx.uctx_local in
+ let newinst, left =
+ List.fold_right
+ (fun (loc,id) (newinst, acc) ->
+ let l =
+ try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+ with Not_found ->
+ user_err ?loc ~hdr:"universe_context"
+ (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+ in (l :: newinst, Univ.LSet.remove l acc))
+ names ([], levels)
+ in
+ if not extensible && not (Univ.LSet.is_empty left) then
+ let n = Univ.LSet.cardinal left in
+ let loc =
+ try
+ let info =
+ Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+ info.uloc
+ with Not_found -> None
+ in
+ user_err ?loc ~hdr:"universe_context"
+ ((str(CString.plural n "Universe") ++ spc () ++
+ Univ.LSet.pr (pr_uctx_level ctx) left ++
+ spc () ++ str (CString.conjugate_verb_to_be n) ++
+ str" unbound."))
+ else
+ let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+ let inst = Array.append (Array.of_list newinst) left in
+ let inst = Univ.Instance.of_array inst in
+ let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in
+ let ctx = Univ.UContext.make (inst,
+ Univ.ContextSet.constraints ctx.uctx_local) in
+ map, ctx
+
+let check_implication uctx cstrs ctx =
+ let gr = initial_graph uctx in
+ let grext = UGraph.merge_constraints cstrs gr in
+ let cstrs' = Univ.UContext.constraints ctx in
+ if UGraph.check_constraints cstrs' grext then ()
+ else CErrors.user_err ~hdr:"check_univ_decl"
+ (str "Universe constraints are not implied by the ones declared.")
+
+let check_univ_decl uctx decl =
+ let open Misctypes in
+ let pl, ctx = universe_context
+ ~names:decl.univdecl_instance
+ ~extensible:decl.univdecl_extensible_instance
+ uctx
+ in
+ if not decl.univdecl_extensible_constraints then
+ check_implication uctx decl.univdecl_constraints ctx;
+ pl, ctx
let restrict ctx vars =
let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index 0b67bb71f..21145e7e6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -120,7 +120,13 @@ val normalize : t -> t
(** {5 TODO: Document me} *)
-val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
+ (Id.t * Univ.Level.t) list * Univ.universe_context
+
+type universe_decl =
+ (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
val update_sigma_env : t -> Environ.env -> t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index a4f2e26b6..94116e473 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -411,6 +411,7 @@ sig
val add_instance : Instance.t -> t -> t
(** Arbitrary choice of linear order of the variables *)
+ val sort_levels : Level.t array -> Level.t array
val to_context : t -> universe_context
val of_context : universe_context -> t
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ef1654fdf..409bb89ee 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -338,13 +338,14 @@ let generate_functional_principle (evd: Evd.evar_map ref)
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let evd' = Evd.from_env (Global.env ()) in
- let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
- let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
- let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
- let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
- (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
+ let evd' = Evd.from_env (Global.env ()) in
+ let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
+ let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+ let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+ let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
+ (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+ let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in
+ let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
ignore(
Declare.declare_constant
name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 41a10cba3..d43fd78f3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1543,7 +1543,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let equation_id = add_suffix function_name "_equation" in
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
- let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+ let functional_ref =
+ let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in
+ declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
+ in
(* Refresh the global universes, now including those of _F *)
let evm = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75b665aad..3d01cbe8d 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let pl, ctx = Evd.universe_context sigma in
+ let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d0fe1f957..b8fae2494 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
let nf c = nf (constr_of c) in
- Array.map nf !tactic_res, snd (Evd.universe_context evd)
+ Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd)
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 967ec2a71..7c488f524 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
let invProof = EConstr.Unsafe.to_constr invProof in
let p = Evarutil.nf_evars_universes sigma invProof in
- p, Evd.universe_context sigma
+ p, Evd.universe_context ~names:[] ~extensible:true sigma
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 128bc7767..904ff68aa 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,3 +4,9 @@ bar@{u} = nat
*)
bar is universe polymorphic
+foo@{u Top.8 v} =
+Type@{Top.8} -> Type@{v} -> Type@{u}
+ : Type@{max(u+1, Top.8+1, v+1)}
+(* u Top.8 v |= *)
+
+foo is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index d9e89e43c..8656ff1a3 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,7 +1,13 @@
Set Universe Polymorphism.
Set Printing Universes.
+Unset Strict Universe Declaration.
Class Wrap A := wrap : A.
Instance bar@{u} : Wrap@{u} Set. Proof nat.
Print bar.
+
+(* The universes in the binder come first, then the extra universes in
+ order of appearance. *)
+Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Print foo.
diff --git a/vernac/class.ml b/vernac/class.ml
index be682977e..3915148a0 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -222,9 +222,10 @@ let build_id_coercion idf_opt source poly =
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
+ let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
- (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma))
+ (definition_entry ~types:typ_f ~poly ~univs
~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/vernac/command.ml b/vernac/command.ml
index 15dacb776..59f59e530 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1019,15 +1019,16 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let binders_rel = nf_evar_context !evdref binders_rel in
let binders = nf_evar_context !evdref binders in
let top_arity = Evarutil.nf_evar !evdref top_arity in
- let pl = Option.map (fun d -> d.univdecl_instance) pl in
- let hook, recname, typ =
+ let pl, plext = Option.cata
+ (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
+ let hook, recname, typ =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr _ =
let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ty = EConstr.Unsafe.to_constr ty in
- let pl, univs = Evd.universe_context ?names:pl !evdref in
+ let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
(*FIXME poly? *)
let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
(** FIXME: include locality *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index facebd096..90168843a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -108,7 +108,7 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
- let _, univs = Evd.universe_context ctx in
+ let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
let univs =
if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
else Monomorphic_const_entry univs
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 793022377..391e78bcd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function
(NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- let (_, uctx) = UState.universe_context uctx in
+ let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in
let inst = Univ.UContext.instance uctx in
let map (c, ctx) = Vars.subst_instance_constr inst c in
(Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook =
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
let () =
if not decl.Misctypes.univdecl_extensible_instance then
- ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance)
+ ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
else ()
in
let evd =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c71feb52b..89b18d254 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -888,7 +888,7 @@ in
let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
Univ.Instance.empty, Evd.evar_universe_context ctx'
else
- let (_, uctx) = UState.universe_context ctx' in
+ let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fd08b42d..c90d038f6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1556,7 +1556,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
- let pl, uctx = Evd.universe_context sigma' in
+ let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
let c = nf c in
let j =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 14:26:44 +0000