aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/indtypes.ml1
-rw-r--r--kernel/univ.ml100
-rw-r--r--kernel/univ.mli27
-rw-r--r--library/universes.ml70
-rw-r--r--library/universes.mli5
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--toplevel/command.ml2
7 files changed, 92 insertions, 119 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cc56428fa4..ee4a404a7c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -320,7 +320,6 @@ let typecheck_inductive env ctx mie =
in
match s with
| Type u when expltype (* Explicitly polymorphic *) ->
- (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *)
(* The polymorphic level is a function of the level of the *)
(* conclusions of the parameters *)
(* We enforce [u >= lev] in case [lev] has a strict upper *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6a11251b06..256ce5e92c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1657,110 +1657,18 @@ let sort_universes orig =
in
Array.fold_left_i fold sorted types
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types *)
-
(* Miscellaneous functions to remove or test local univ assumed to
- occur only in the le constraints *)
+ occur in a universe *)
-let remove_large_constraint u v min =
+let univ_level_mem u v = Huniv.mem (Expr.make u) v
+
+let univ_level_rem u v min =
match Universe.level v with
| Some u' -> if Level.equal u u' then min else v
| None -> Huniv.remove (Universe.Expr.make u) v
-(* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
-let is_direct_constraint u v =
- match Universe.level v with
- | Some u' -> Level.equal u u'
- | None ->
- let expr = Universe.Expr.make u in
- Universe.exists (Universe.Expr.equal expr) v
-
-(*
- 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 -> is_direct_constraint u v
- | None -> false
-
-let solve_constraints_system levels level_bounds level_min =
- let levels =
- Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> anomaly (Pp.str"expects Atom")))
- 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);
- level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
- done;
- for j=0 to nind-1 do
- match levels.(j) with
- | Some u -> v.(i) <- remove_large_constraint u v.(i) level_min.(i)
- | None -> ()
- done
- done;
- v
-
-let subst_large_constraint u u' v =
- match level u with
- | Some u ->
- (* if is_direct_constraint u v then *)
- Universe.sup u' (remove_large_constraint u v type0m_univ)
- (* else v *)
- | _ ->
- anomaly (Pp.str "expect a universe level")
-
-let subst_large_constraints =
- List.fold_right (fun (u,u') -> subst_large_constraint u u')
-
-let no_upper_constraints u cst =
- match level u with
- | Some u ->
- let test (u1, _, _) =
- not (Int.equal (Level.compare u1 u) 0) in
- Constraint.for_all test cst
- | _ -> anomaly (Pp.str "no_upper_constraints")
-
(* Is u mentionned in v (or equals to v) ? *)
-let univ_depends u v =
- match atom u with
- | Some u -> Huniv.mem u v
- | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg")
(**********************************************************************)
(** Universe polymorphism *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8166d75e62..9b68dbc8ce 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -129,6 +129,15 @@ val super : universe -> universe
val universe_level : universe -> universe_level option
+(** [univ_level_mem l u] Is l is mentionned in u ? *)
+
+val univ_level_mem : universe_level -> universe -> bool
+
+(** [univ_level_rem u v min] removes [u] from [v], resulting in [min]
+ if [v] was exactly [u]. *)
+
+val univ_level_rem : universe_level -> universe -> universe -> universe
+
(** {6 Graphs of universes. } *)
type universes
@@ -211,24 +220,6 @@ val constraints_of_universes : universes -> constraints
val check_constraint : universes -> univ_constraint -> bool
val check_constraints : constraints -> universes -> bool
-(** {6 Support for old-style sort-polymorphism } *)
-
-val solve_constraints_system : universe option array -> universe array -> universe array ->
- universe array
-
-val remove_large_constraint : universe_level -> universe -> universe -> universe
-
-val subst_large_constraint : universe -> universe -> universe -> universe
-
-val subst_large_constraints :
- (universe * universe) list -> universe -> universe
-
-val no_upper_constraints : universe -> constraints -> bool
-
-(** Is u mentionned in v (or equals to v) ? *)
-
-val univ_depends : universe -> universe -> bool
-
(** {6 Support for universe polymorphism } *)
(** Polymorphic maps from universe levels to 'a *)
diff --git a/library/universes.ml b/library/universes.ml
index e84f1f975c..1c704bc229 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -930,3 +930,73 @@ let refresh_constraints univs (ctx, cstrs) =
else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
cstrs (Univ.Constraint.empty, univs)
in ((ctx, cstrs'), univs')
+
+
+(**********************************************************************)
+(* Tools for sort-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_level_mem u v
+ | None -> false
+
+let solve_constraints_system levels level_bounds level_min =
+ let open Univ in
+ let levels =
+ Array.map (Option.map
+ (fun u -> match Universe.level u with
+ | Some u -> u
+ | _ -> Errors.anomaly (Pp.str"expects Atom")))
+ 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);
+ level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
+ done;
+ for j=0 to nind-1 do
+ match levels.(j) with
+ | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i)
+ | None -> ()
+ done
+ done;
+ v
diff --git a/library/universes.mli b/library/universes.mli
index 5b09519286..2fc476732c 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -243,3 +243,8 @@ val minimize_univ_variables :
Univ.LSet.t * Univ.universe option Univ.LMap.t *
Univ.LSet.t *
(bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
+
+(** {6 Support for old-style sort-polymorphism } *)
+
+val solve_constraints_system : universe option array -> universe array -> universe array ->
+ universe array
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07a3378363..313bf6110c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -480,13 +480,13 @@ let rec instantiate_universes env evdref scl is = function
d :: instantiate_universes env evdref scl is (sign, exp)
| d::sign, None::exp ->
d :: instantiate_universes env evdref scl is (sign, exp)
- | (na,None,ty)::sign, Some u::exp ->
+ | (na,None,ty)::sign, Some l::exp ->
let ctx,_ = Reduction.dest_arity env ty in
- let u = Univ.Universe.make u in
+ let u = Univ.Universe.make l in
let s =
(* Does the sort of parameter [u] appear in (or equal)
the sort of inductive [is] ? *)
- if univ_depends u is then
+ if univ_level_mem l is then
scl (* constrained sort: replace by scl *)
else
(* unconstrained sort: replace by fresh universe *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4fc574daf5..ff2e89351e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -413,7 +413,7 @@ let inductive_levels env evdref poly arities inds =
in
(* Take the transitive closure of the system of constructors *)
(* level constraints and remove the recursive dependencies *)
- let levels' = Univ.solve_constraints_system (Array.of_list levels)
+ let levels' = Universes.solve_constraints_system (Array.of_list levels)
(Array.of_list cstrs_levels) (Array.of_list min_levels)
in
let evd =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:08:56 +0000