aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml12
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comInductive.ml70
-rw-r--r--vernac/comInductive.mli4
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declareDef.mli4
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernacentries.ml2
15 files changed, 97 insertions, 31 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5e602289b..2a41a50dd 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -59,15 +59,15 @@ exception NonSingletonProp of inductive
exception DecidabilityMutualNotSupported
exception NoDecidabilityCoInductive
-let constr_of_global g = lazy (Universes.constr_of_global g)
+let constr_of_global g = lazy (UnivGen.constr_of_global g)
(* Some pre declaration of constant we are going to use *)
let bb = constr_of_global Coqlib.glob_bool
-let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
let andb_true_intro = fun _ ->
- Universes.constr_of_global
+ UnivGen.constr_of_global
(Coqlib.build_bool_type()).Coqlib.andb_true_intro
let tt = constr_of_global Coqlib.glob_true
@@ -76,9 +76,9 @@ let ff = constr_of_global Coqlib.glob_false
let eq = constr_of_global Coqlib.glob_eq
-let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ())
+let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ())
-let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
let induct_on c = induction false None c None None
@@ -863,7 +863,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
create_input (
mkNamedProd n (mkFullInd ind (2*nparrec)) (
mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
- mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
+ mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
)
)
)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1ac597695..61ce5d6c4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -423,13 +423,13 @@ let context poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus = match b with
| None ->
- pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
+ pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
- let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
+ let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 26a46a752..722f21171 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -174,7 +174,7 @@ let do_assumptions kind nl l =
let t = replace_vars subst t in
let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
- (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+ (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
idl refs
in
subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2f2c7c4e2..56932360a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
nor in a module type and meant to be instantiated. *)
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
- Universes.universe_binders -> Impargs.manual_implicits ->
+ UnivNames.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b2532485a..629fcce5a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -177,6 +177,72 @@ let is_flexible_sort evd u =
| Some l -> Evd.is_flexible_level evd l
| None -> false
+(**********************************************************************)
+(* Tools for template polymorphic inductive types *)
+
+(* Miscellaneous functions to remove or test local univ assumed to
+ occur only in the le constraints *)
+
+(*
+ Solve a system of universe constraint of the form
+
+ u_s11, ..., u_s1p1, w1 <= u1
+ ...
+ u_sn1, ..., u_snpn, wn <= un
+
+where
+
+ - the ui (1 <= i <= n) are universe variables,
+ - the sjk select subsets of the ui for each equations,
+ - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let is_direct_sort_constraint s v = match s with
+ | Some u -> Univ.univ_level_mem u v
+ | None -> false
+
+let solve_constraints_system levels level_bounds =
+ let open Univ in
+ let levels =
+ Array.mapi (fun i o ->
+ match o with
+ | Some u ->
+ (match Universe.level u with
+ | Some u -> Some u
+ | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+ | None -> None)
+ levels in
+ let v = Array.copy level_bounds in
+ let nind = Array.length v in
+ let clos = Array.map (fun _ -> Int.Set.empty) levels in
+ (* First compute the transitive closure of the levels dependencies *)
+ for i=0 to nind-1 do
+ for j=0 to nind-1 do
+ if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+ clos.(i) <- Int.Set.add j clos.(i);
+ done;
+ done;
+ let rec closure () =
+ let continue = ref false in
+ Array.iteri (fun i deps ->
+ let deps' =
+ Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
+ in
+ if Int.Set.equal deps deps' then ()
+ else (clos.(i) <- deps'; continue := true))
+ clos;
+ if !continue then closure ()
+ else ()
+ in
+ closure ();
+ for i=0 to nind-1 do
+ for j=0 to nind-1 do
+ if not (Int.equal i j) && Int.Set.mem j clos.(i) then
+ (v.(i) <- Universe.sup v.(i) level_bounds.(j));
+ done;
+ done;
+ v
+
let inductive_levels env evd poly arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
@@ -205,8 +271,8 @@ let inductive_levels env evd poly arities inds =
in
(* Take the transitive closure of the system of constructors *)
(* level constraints and remove the recursive dependencies *)
- let levels' = Universes.solve_constraints_system (Array.of_list levels)
- (Array.of_list cstrs_levels) (Array.of_list min_levels)
+ let levels' = solve_constraints_system (Array.of_list levels)
+ (Array.of_list cstrs_levels)
in
let evd, arities =
CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 833935724..7ae8e8f71 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -37,7 +37,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val declare_mutual_inductive_with_eliminations :
- mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
+ mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
(** Exported for Funind *)
@@ -64,4 +64,4 @@ val extract_mutual_inductive_declaration_components :
val interp_mutual_inductive :
structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> Declarations.recursivity_kind ->
- mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+ mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 349fc562b..f41e0fc44 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
- let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
+ let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 12973f51b..c5e704a5e 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,11 +14,11 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition : Id.t -> definition_kind ->
- Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+ Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
GlobRef.t Lemmas.declaration_hook -> GlobRef.t
val declare_fix : ?opaque:bool -> definition_kind ->
- Universes.universe_binders -> Entries.constant_universes_entry ->
+ UnivNames.universe_binders -> Entries.constant_universes_entry ->
Id.t -> Safe_typing.private_constants Entries.proof_output ->
Constr.types -> Impargs.manual_implicits ->
GlobRef.t
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f9167f969..f68dcae26 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -55,7 +55,7 @@ let process_vernac_interp_error exn = match fst exn with
let msg =
if !Constrextern.print_universes then
str "." ++ spc() ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
else
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index acb461cac..3c4fcf714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -197,7 +197,7 @@ let rec pr_disjunction pr = function
let pr_puniverses f env (c,u) =
f env c ++
(if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
- str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
else mt())
let explain_elim_arity env sigma ind sorts c pj okinds =
@@ -314,7 +314,7 @@ let explain_unification_error env sigma p1 p2 = function
| UnifUnivInconsistency p ->
if !Constrextern.print_universes then
[str "universe inconsistency: " ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes p]
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
@@ -886,7 +886,7 @@ let explain_not_match_error = function
str"polymorphic universe instances do not match"
| IncompatibleUniverses incon ->
str"the universe constraints are inconsistent: " ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
| IncompatiblePolymorphism (env, t1, t2) ->
str "conversion of polymorphic values generates additional constraints: " ++
quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 32885ab88..2deca1e06 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort =
match inst with
| None ->
let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
- let u, ctx = Universes.fresh_instance_from ctx None in
+ let u, ctx = UnivGen.fresh_instance_from ctx None in
let evd = Evd.from_ctx (UState.of_context_set ctx) in
evd, (ind,u), Some u
| Some ui -> evd, (ind, ui), inst
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ae1065ef5..1e7721f8f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty =
let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
Coqlib.check_required_library ("Coq"::md);
- Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
+ UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
let hide_obligation = safe_init_constant tactics_module "obligation"
let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
@@ -472,7 +472,7 @@ let subst_body expand prg =
let declare_definition prg =
let body, typ = subst_body true prg in
- let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+ let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
(UState.subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in
@@ -555,7 +555,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.const_univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
diff --git a/vernac/record.ml b/vernac/record.ml
index b0f229294..bf6affd5f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -316,7 +316,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
let kn = destConstRef gr in
Declare.definition_message fid;
- Universes.register_universe_binders gr ubinders;
+ UnivNames.register_universe_binders gr ubinders;
kn, mkProj (Projection.make kn false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
@@ -352,7 +352,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
- Universes.register_universe_binders (ConstRef kn) ubinders;
+ UnivNames.register_universe_binders (ConstRef kn) ubinders;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
@@ -465,9 +465,9 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref [paramimpls];
- Universes.register_universe_binders cref ubinders;
+ UnivNames.register_universe_binders cref ubinders;
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
- Universes.register_universe_binders (ConstRef proj_cst) ubinders;
+ UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
diff --git a/vernac/record.mli b/vernac/record.mli
index 308c9e9b9..b2c039f0b 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,7 @@ val declare_projections :
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
bool list ->
- Universes.universe_binders ->
+ UnivNames.universe_binders ->
Impargs.manual_implicits list ->
Context.Rel.t ->
(Name.t * bool) list * Constant.t option list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 938e9718a..eae8167c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1741,7 +1741,7 @@ let vernac_print ~atts env sigma =
else str"There may remain asynchronous universe constraints"
in
begin match dst with
- | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining
+ | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
| Some s -> dump_universes_gen univ s
end
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 14:27:04 +0000