aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml52
-rw-r--r--library/declare.mli8
-rw-r--r--library/goptions.ml113
-rw-r--r--library/goptions.mli15
-rw-r--r--library/impargs.ml16
-rw-r--r--library/lib.ml11
-rw-r--r--library/lib.mli2
-rw-r--r--library/universes.ml143
-rw-r--r--library/universes.mli34
9 files changed, 243 insertions, 151 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f4..c9992fff3b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -434,6 +434,23 @@ let assumption_message id =
(** Global universe names, in a different summary *)
+type universe_context_decl = polymorphic * Univ.universe_context_set
+
+let cache_universe_context (p, ctx) =
+ Global.push_context_set p ctx;
+ if p then Lib.add_section_context ctx
+
+let input_universe_context : universe_context_decl -> Libobject.obj =
+ declare_object
+ { (default_object "Global universe context state") with
+ cache_function = (fun (na, pi) -> cache_universe_context pi);
+ load_function = (fun _ (_, pi) -> cache_universe_context pi);
+ discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+ classify_function = (fun a -> Keep a) }
+
+let declare_universe_context poly ctx =
+ Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
+
(* Discharged or not *)
type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
@@ -446,9 +463,8 @@ let cache_universes (p, l) =
Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
- Global.push_context_set p ctx;
- if p then Lib.add_section_context ctx;
- Universes.set_global_universe_names glob'
+ cache_universe_context (p, ctx);
+ Universes.set_global_universe_names glob'
let input_universes : universe_decl -> Libobject.obj =
declare_object
@@ -475,8 +491,10 @@ let do_universe poly l =
type constraint_decl = polymorphic * Univ.constraints
let cache_constraints (na, (p, c)) =
- Global.add_constraints c;
- if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+ let ctx =
+ Univ.ContextSet.add_constraints c
+ Univ.ContextSet.empty (* No declared universes here, just constraints *)
+ in cache_universe_context (p,ctx)
let discharge_constraints (_, (p, c as a)) =
if p then None else Some a
@@ -491,12 +509,20 @@ let input_constraints : constraint_decl -> Libobject.obj =
classify_function = (fun a -> Keep a) }
let do_constraint poly l =
- let u_of_id =
- let names, _ = Universes.global_universe_names () in
- fun (loc, id) ->
- try Idmap.find id names
- with Not_found ->
- user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ let open Misctypes in
+ let u_of_id x =
+ match x with
+ | GProp -> Loc.dummy_loc, (false, Univ.Level.prop)
+ | GSet -> Loc.dummy_loc, (false, Univ.Level.set)
+ | GType None ->
+ user_err_loc (Loc.dummy_loc, "Constraint",
+ str "Cannot declare constraints on anonymous universes")
+ | GType (Some (loc, id)) ->
+ let id = Id.of_string id in
+ let names, _ = Universes.global_universe_names () in
+ try loc, Idmap.find id names
+ with Not_found ->
+ user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
in
let in_section = Lib.sections_are_opened () in
let () =
@@ -514,8 +540,8 @@ let do_constraint poly l =
++ str "Polymorphic Constraint instead")
in
let constraints = List.fold_left (fun acc (l, d, r) ->
- let p, lu = u_of_id l and p', ru = u_of_id r in
- check_poly (fst l) p (fst r) p';
+ let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+ check_poly ploc p rloc p';
Univ.Constraint.add (lu, d, ru) acc)
Univ.Constraint.empty l
in
diff --git a/library/declare.mli b/library/declare.mli
index 7824506da0..f70d594d7e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -87,7 +87,11 @@ val exists_name : Id.t -> bool
-(** Global universe names and constraints *)
+(** Global universe contexts, names and constraints *)
+
+val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_constraint : polymorphic ->
+ (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+ unit
diff --git a/library/goptions.ml b/library/goptions.ml
index 1cf25987b1..9dc0f40588 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -208,6 +208,10 @@ type 'a option_sig = {
optread : unit -> 'a;
optwrite : 'a -> unit }
+type option_locality = OptLocal | OptDefault | OptGlobal
+
+type option_mod = OptSet | OptAppend
+
module OptionOrd =
struct
type t = option_name
@@ -238,49 +242,52 @@ let warn_deprecated_option =
(fun key -> str "Option" ++ spc () ++ str (nickname key) ++
strbrk " is deprecated")
-let declare_option cast uncast
+let get_locality = function
+ | Some true -> OptLocal
+ | Some false -> OptGlobal
+ | None -> OptDefault
+
+let declare_option cast uncast append ?(preprocess = fun x -> x)
{ optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
- (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
- That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
- lists of strings *without* spaces. *)
- let (write,lwrite,gwrite) = if sync then
- let ldecl_obj = (* "Local": doesn't survive section or modules. *)
- declare_object {(default_object ("L "^nickname key)) with
- cache_function = (fun (_,v) -> write v);
- classify_function = (fun _ -> Dispose)}
- in
- let decl_obj = (* default locality: survives sections but not modules. *)
- declare_object {(default_object (nickname key)) with
- cache_function = (fun (_,v) -> write v);
- classify_function = (fun _ -> Dispose);
- discharge_function = (fun (_,v) -> Some v)}
- in
- let gdecl_obj = (* "Global": survives section and modules. *)
- declare_object {(default_object ("G "^nickname key)) with
- cache_function = (fun (_,v) -> write v);
- classify_function = (fun v -> Substitute v);
- subst_function = (fun (_,v) -> v);
- discharge_function = (fun (_,v) -> Some v);
- load_function = (fun _ (_,v) -> write v)}
- in
- let _ = Summary.declare_summary (nickname key)
- { Summary.freeze_function = (fun _ -> read ());
- Summary.unfreeze_function = write;
- Summary.init_function = (fun () -> write default) }
- in
- begin fun v -> add_anonymous_leaf (decl_obj v) end ,
- begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
- begin fun v -> add_anonymous_leaf (gdecl_obj v) end
- else write,write,write
+ let change =
+ if sync then
+ let _ = Summary.declare_summary (nickname key)
+ { Summary.freeze_function = (fun _ -> read ());
+ Summary.unfreeze_function = write;
+ Summary.init_function = (fun () -> write default) } in
+ let cache_options (_,(l,m,v)) =
+ match m with
+ | OptSet -> write v
+ | OptAppend -> write (append (read ()) v) in
+ let load_options i o = cache_options o in
+ let subst_options (subst,obj) = obj in
+ let discharge_options (_,(l,_,_ as o)) =
+ match l with OptLocal -> None | _ -> Some o in
+ let classify_options (l,_,_ as o) =
+ match l with OptGlobal -> Substitute o | _ -> Dispose in
+ let options : option_locality * option_mod * _ -> obj =
+ declare_object
+ { (default_object (nickname key)) with
+ load_function = load_options;
+ cache_function = cache_options;
+ subst_function = subst_options;
+ discharge_function = discharge_options;
+ classify_function = classify_options } in
+ (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
+ else
+ (fun _ m v ->
+ let v = preprocess v in
+ match m with
+ | OptSet -> write v
+ | OptAppend -> write (append (read ()) v))
in
let warn () = if depr then warn_deprecated_option key in
let cread () = cast (read ()) in
- let cwrite v = warn (); write (uncast v) in
- let clwrite v = warn (); lwrite (uncast v) in
- let cgwrite v = warn (); gwrite (uncast v) in
- value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
+ let cwrite l v = warn (); change l OptSet (uncast v) in
+ let cappend l v = warn (); change l OptAppend (uncast v) in
+ value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab;
write
type 'a write_function = 'a -> unit
@@ -289,18 +296,22 @@ let declare_int_option =
declare_option
(fun v -> IntValue v)
(function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (fun _ _ -> anomaly (Pp.str "async_option"))
let declare_bool_option =
declare_option
(fun v -> BoolValue v)
(function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (fun _ _ -> anomaly (Pp.str "async_option"))
let declare_string_option =
declare_option
(fun v -> StringValue v)
(function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (fun x y -> x^","^y)
let declare_stringopt_option =
declare_option
(fun v -> StringOptValue v)
(function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (fun _ _ -> anomaly (Pp.str "async_option"))
(* 3- User accessible commands *)
@@ -315,13 +326,8 @@ let set_option_value locality check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (_,read,write,lwrite,gwrite)) ->
- let write = match locality with
- | None -> write
- | Some true -> lwrite
- | Some false -> gwrite
- in
- write (check_and_cast v (read ()))
+ | Some (name, depr, (_,read,write,append)) ->
+ write (get_locality locality) (check_and_cast v (read ()))
let bad_type_error () = error "Bad type of value for this option."
@@ -357,6 +363,13 @@ let set_string_option_value_gen locality =
let unset_option_value_gen locality key =
set_option_value locality check_unset_value key ()
+let set_string_option_append_value_gen locality key v =
+ let opt = try Some (get_option key) with Not_found -> None in
+ match opt with
+ | None -> warn_unknown_option key
+ | Some (name, depr, (_,read,write,append)) ->
+ append (get_locality locality) (check_string_value v (read ()))
+
let set_int_option_value = set_int_option_value_gen None
let set_bool_option_value = set_bool_option_value_gen None
let set_string_option_value = set_string_option_value_gen None
@@ -369,13 +382,13 @@ let msg_option_value (name,v) =
| BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
- | StringValue s -> str s
+ | StringValue s -> str "\"" ++ str s ++ str "\""
| StringOptValue None -> str"undefined"
- | StringOptValue (Some s) -> str s
+ | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\""
(* | IdentValue r -> pr_global_env Id.Set.empty r *)
let print_option_value key =
- let (name, depr, (_,read,_,_,_)) = get_option key in
+ let (name, depr, (_,read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
@@ -385,7 +398,7 @@ let print_option_value key =
let get_tables () =
let tables = !value_tab in
- let fold key (name, depr, (sync,read,_,_,_)) accu =
+ let fold key (name, depr, (sync,read,_,_)) accu =
let state = {
opt_sync = sync;
opt_name = name;
@@ -404,13 +417,13 @@ let print_tables () =
in
str "Synchronous options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (sync,read,_,_,_)) p ->
+ (fun key (name, depr, (sync,read,_,_)) p ->
if sync then p ++ print_option key name (read ()) depr
else p)
!value_tab (mt ()) ++
str "Asynchronous options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (sync,read,_,_,_)) p ->
+ (fun key (name, depr, (sync,read,_,_)) p ->
if sync then p
else p ++ print_option key name (read ()) depr)
!value_tab (mt ()) ++
diff --git a/library/goptions.mli b/library/goptions.mli
index 26864503b1..3b3651f393 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -122,13 +122,19 @@ type 'a option_sig = {
(** When an option is declared synchronous ([optsync] is [true]), the output is
a synchronous write function. Otherwise it is [optwrite] *)
+(** The [preprocess] function is triggered before setting the option. It can be
+ used to emit a warning on certain values, and clean-up the final value. *)
type 'a write_function = 'a -> unit
-val declare_int_option : int option option_sig -> int option write_function
-val declare_bool_option : bool option_sig -> bool write_function
-val declare_string_option: string option_sig -> string write_function
-val declare_stringopt_option: string option option_sig -> string option write_function
+val declare_int_option : ?preprocess:(int option -> int option) ->
+ int option option_sig -> int option write_function
+val declare_bool_option : ?preprocess:(bool -> bool) ->
+ bool option_sig -> bool write_function
+val declare_string_option: ?preprocess:(string -> string) ->
+ string option_sig -> string write_function
+val declare_stringopt_option: ?preprocess:(string option -> string option) ->
+ string option option_sig -> string option write_function
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -154,6 +160,7 @@ val get_ref_table :
val set_int_option_value_gen : bool option -> option_name -> int option -> unit
val set_bool_option_value_gen : bool option -> option_name -> bool -> unit
val set_string_option_value_gen : bool option -> option_name -> string -> unit
+val set_string_option_append_value_gen : bool option -> option_name -> string -> unit
val unset_option_value_gen : bool option -> option_name -> unit
val set_int_option_value : option_name -> int option -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index bce7a15cbe..828d652c83 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -491,13 +491,15 @@ let implicits_of_global ref =
let l = Refmap.find ref !implicits_table in
try
let rename_l = Arguments_renaming.arguments_names ref in
- let rename imp name = match imp, name with
- | Some (_, x,y), Name id -> Some (id, x,y)
- | _ -> imp in
- List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+ let rec rename implicits names = match implicits, names with
+ | [], _ -> []
+ | _, [] -> implicits
+ | Some (_, x,y) :: implicits, Name id :: names ->
+ Some (id, x,y) :: rename implicits names
+ | imp :: implicits, _ :: names -> imp :: rename implicits names
+ in
+ List.map (fun (t, il) -> t, rename il rename_l) l
with Not_found -> l
- | Invalid_argument _ ->
- anomaly (Pp.str "renamings list and implicits list have different lenghts")
with Not_found -> [DefaultImpArgs,[]]
let cache_implicits_decl (ref,imps) =
@@ -657,7 +659,7 @@ let check_inclusion l =
let rec aux = function
| n1::(n2::_ as nl) ->
if n1 <= n2 then
- error "Sequences of implicit arguments must be of different lengths";
+ error "Sequences of implicit arguments must be of different lengths.";
aux nl
| _ -> () in
aux (List.map (fun (imps,_) -> List.length imps) l)
diff --git a/library/lib.ml b/library/lib.ml
index 7218950da3..f680ecee3c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -231,11 +231,16 @@ let add_leaves id objs =
List.iter add_obj objs;
oname
-let add_anonymous_leaf obj =
+let add_anonymous_leaf ?(cache_first = true) obj =
let id = anonymous_id () in
let oname = make_oname id in
- cache_object (oname,obj);
- add_entry oname (Leaf obj)
+ if cache_first then begin
+ cache_object (oname,obj);
+ add_entry oname (Leaf obj)
+ end else begin
+ add_entry oname (Leaf obj);
+ cache_object (oname,obj)
+ end
let add_frozen_state () =
add_anonymous_entry
diff --git a/library/lib.mli b/library/lib.mli
index 0a70152efb..a8e110c67a 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -54,7 +54,7 @@ val segment_of_objects :
current list of operations (most recent ones coming first). *)
val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
-val add_anonymous_leaf : Libobject.obj -> unit
+val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
val pull_to_head : Libnames.object_name -> unit
(** this operation adds all objects with the same name and calls [load_object]
diff --git a/library/universes.ml b/library/universes.ml
index db95607f18..112b20a4c4 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -702,12 +702,45 @@ let pr_universe_body = function
let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
-exception Found of Level.t
+let compare_constraint_type d d' =
+ match d, d' with
+ | Eq, Eq -> 0
+ | Eq, _ -> -1
+ | _, Eq -> 1
+ | Le, Le -> 0
+ | Le, _ -> -1
+ | _, Le -> 1
+ | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+ let merge k a b =
+ match a, b with
+ | Some _, None -> a
+ | None, Some _ -> b
+ | None, None -> None
+ | Some l, Some r ->
+ if compare_constraint_type l r >= 0 then a
+ else b
+ in LMap.merge merge
+
+let lower_add l c m =
+ try let c' = LMap.find l m in
+ if compare_constraint_type c c' > 0 then
+ LMap.add l c m
+ else m
+ with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+ List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+exception Found of Level.t * lowermap
let find_inst insts v =
- try LMap.iter (fun k (enf,alg,v') ->
- if not alg && enf && Universe.equal v' v then raise (Found k))
+ try LMap.iter (fun k (enf,alg,v',lower) ->
+ if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
insts; raise Not_found
- with Found l -> l
+ with Found (f,l) -> (f,l)
let compute_lbound left =
(** The universe variable was not fixed yet.
@@ -726,27 +759,33 @@ let compute_lbound left =
else None))
None left
-let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
+let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
if enforce then
let inst = Universe.make u in
let cstrs' = enforce_leq lbound inst cstrs in
(ctx, us, LSet.remove u algs,
- LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst)
+ LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
+ (enforce, alg, inst, lower)
else (* Actually instantiate *)
(Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
- LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound)
+ LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
+ (enforce, alg, lbound, lower)
type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
let pr_constraints_map cmap =
LMap.fold (fun l cstrs acc ->
Level.pr l ++ str " => " ++
- prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
- ++ acc)
+ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
+ fnl () ++ acc)
cmap (mt ())
let remove_alg l (ctx, us, algs, insts, cstrs) =
(ctx, us, LSet.remove l algs, insts, cstrs)
+
+let remove_lower u lower =
+ let levels = Universe.levels u in
+ LSet.fold (fun l acc -> LMap.remove l acc) levels lower
let minimize_univ_variables ctx us algs left right cstrs =
let left, lbounds =
@@ -756,22 +795,50 @@ let minimize_univ_variables ctx us algs left right cstrs =
let lbounds' =
match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
| None -> lbounds
- | Some lbound -> LMap.add r (true, false, lbound) lbounds
+ | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
+ lbounds
in (Univ.LMap.remove r left, lbounds'))
left (left, Univ.LMap.empty)
in
let rec instance (ctx', us, algs, insts, cstrs as acc) u =
- let acc, left =
- try let l = LMap.find u left in
- List.fold_left
- (fun (acc, left') (d, l) ->
- let acc', (enf,alg,l') = aux acc l in
- let l' =
- if enf then Universe.make l
- else l'
- in acc', (d, l') :: left')
- (acc, []) l
- with Not_found -> acc, []
+ let acc, left, lower =
+ try
+ let l = LMap.find u left in
+ let acc, left, newlow, lower =
+ List.fold_left
+ (fun (acc, left', newlow, lower') (d, l) ->
+ let acc', (enf,alg,l',lower) = aux acc l in
+ let l' =
+ if enf then Universe.make l
+ else l'
+ in acc', (d, l') :: left',
+ lower_add l d newlow, lower_union lower lower')
+ (acc, [], LMap.empty, LMap.empty) l
+ in
+ let not_lower (d,l) =
+ (* We're checking if (d,l) is already implied by the lower
+ constraints on some level u. If it represents l < u (d is Lt
+ or d is Le and i > 0, the i < 0 case is impossible due to
+ invariants of Univ), and the lower constraints only have l <=
+ u then it is not implied. *)
+ Univ.Universe.exists
+ (fun (l,i) ->
+ let d =
+ if i == 0 then d
+ else match d with
+ | Le -> Lt
+ | d -> d
+ in
+ try let d' = LMap.find l lower in
+ (* If d is stronger than the already implied lower
+ * constraints we must keep it. *)
+ compare_constraint_type d d' > 0
+ with Not_found ->
+ (** No constraint existing on l *) true) l
+ in
+ let left = List.uniquize (List.filter not_lower left) in
+ (acc, left, LMap.union newlow lower)
+ with Not_found -> acc, [], LMap.empty
and right =
try Some (LMap.find u right)
with Not_found -> None
@@ -779,31 +846,33 @@ let minimize_univ_variables ctx us algs left right cstrs =
let instantiate_lbound lbound =
let alg = LSet.mem u algs in
if alg then
- (* u is algebraic: we instantiate it with it's lower bound, if any,
+ (* u is algebraic: we instantiate it with its lower bound, if any,
or enforce the constraints if it is bounded from the top. *)
- instantiate_with_lbound u lbound true false acc
+ let lower = remove_lower lbound lower in
+ instantiate_with_lbound u lbound lower true false acc
else (* u is non algebraic *)
match Universe.level lbound with
| Some l -> (* The lowerbound is directly a level *)
(* u is not algebraic but has no upper bounds,
we instantiate it with its lower bound if it is a
different level, otherwise we keep it. *)
+ let lower = LMap.remove l lower in
if not (Level.equal l u) then
(* Should check that u does not
have upper constraints that are not already in right *)
let acc' = remove_alg l acc in
- instantiate_with_lbound u lbound false false acc'
- else acc, (true, false, lbound)
- | None ->
- try
- (* if right <> None then raise Not_found; *)
- (* Another universe represents the same lower bound,
- we can share them with no harm. *)
- let can = find_inst insts lbound in
- instantiate_with_lbound u (Universe.make can) false false acc
+ instantiate_with_lbound u lbound lower false false acc'
+ else acc, (true, false, lbound, lower)
+ | None ->
+ try
+ (* Another universe represents the same lower bound,
+ we can share them with no harm. *)
+ let can, lower = find_inst insts lbound in
+ let lower = LMap.remove can lower in
+ instantiate_with_lbound u (Universe.make can) lower false false acc
with Not_found ->
(* We set u as the canonical universe representing lbound *)
- instantiate_with_lbound u lbound false true acc
+ instantiate_with_lbound u lbound lower false true acc
in
let acc' acc =
match right with
@@ -812,7 +881,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
if List.is_empty dangling then acc
else
- let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in
+ let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
let cstrs' = List.fold_left (fun cstrs (d, r) ->
if d == Univ.Le then
enforce_leq inst (Universe.make r) cstrs
@@ -824,15 +893,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
in
(ctx', us, algs, insts, cstrs'), b
in
- if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u))
+ if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
else
let lbound = compute_lbound left in
match lbound with
| None -> (* Nothing to do *)
- acc' (acc, (true, false, Universe.make u))
+ acc' (acc, (true, false, Universe.make u, lower))
| Some lbound ->
try acc' (instantiate_lbound lbound)
- with Failure _ -> acc' (acc, (true, false, Universe.make u))
+ with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
and aux (ctx', us, algs, seen, cstrs as acc) u =
try acc, LMap.find u seen
with Not_found -> instance acc u
diff --git a/library/universes.mli b/library/universes.mli
index a5740ec49f..d3a271b8d0 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -232,40 +232,6 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
-(* For tracing *)
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-val pr_constraints_map : constraints_map -> Pp.std_ppcmds
-
-val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set ->
- universe_level * (universe_set * universe_set * universe_set)
-
-val compute_lbound : (constraint_type * Univ.universe) list -> universe option
-
-val instantiate_with_lbound :
- Univ.LMap.key ->
- Univ.universe ->
- bool ->
- bool ->
- Univ.LSet.t * Univ.universe option Univ.LMap.t *
- Univ.LSet.t *
- (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
- (Univ.LSet.t * Univ.universe option Univ.LMap.t *
- Univ.LSet.t *
- (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
- (bool * bool * Univ.universe)
-
-val minimize_univ_variables :
- Univ.LSet.t ->
- Univ.universe option Univ.LMap.t ->
- Univ.LSet.t ->
- constraints_map -> constraints_map ->
- Univ.constraints ->
- 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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:08:59 +0000