aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml56
-rw-r--r--library/declare.mli22
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/global.ml2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml148
-rw-r--r--library/goptions.mli15
-rw-r--r--library/heads.ml2
-rw-r--r--library/impargs.ml39
-rw-r--r--library/impargs.mli12
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml51
-rw-r--r--library/lib.mli14
-rw-r--r--library/libnames.ml2
-rw-r--r--library/libobject.ml45
-rw-r--r--library/libobject.mli1
-rw-r--r--library/library.ml40
-rw-r--r--library/loadpath.ml18
-rw-r--r--library/nametab.ml19
-rw-r--r--library/states.ml2
-rw-r--r--library/summary.ml35
-rw-r--r--library/summary.mli11
-rw-r--r--library/universes.ml158
-rw-r--r--library/universes.mli34
24 files changed, 399 insertions, 337 deletions
diff --git a/library/declare.ml b/library/declare.ml
index f809e97423..c9992fff3b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,7 +9,7 @@
(** This module is about the low-level declaration of logical objects *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Libnames
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
obj.cst_was_seff <- false;
if Global.exists_objlabel (Label.of_id (basename sp))
then constant_of_kn kn
- else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+ else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
end else
let () = check_exists sp in
let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -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 8dd24d2780..f70d594d7e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name
type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
-(** [declare_constant id cd] declares a global declaration
- (constant/parameter) with name [id] in the current section; it returns
- the full path of the declaration
-
- internal specify if the constant has been created by the kernel or by the
- user, and in the former case, if its errors should be silent
-
- *)
type internal_flag =
| UserAutomaticRequest
| InternalTacticRequest
@@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
?poly:polymorphic -> ?univs:Univ.universe_context ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
+(** [declare_constant id cd] declares a global declaration
+ (constant/parameter) with name [id] in the current section; it returns
+ the full path of the declaration
+
+ internal specify if the constant has been created by the kernel or by the
+ user, and in the former case, if its errors should be silent *)
val declare_constant :
?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
@@ -89,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/declaremods.ml b/library/declaremods.ml
index dcd63c7691..b2806a1ac3 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Declarations
@@ -822,7 +822,7 @@ let protect_summaries f =
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = Summary.unfreeze_summaries fs in
iraise reraise
diff --git a/library/global.ml b/library/global.ml
index c536119314..e748434d24 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -42,7 +42,7 @@ let () =
let assert_not_parsing () =
if !Flags.we_are_parsing then
- Errors.anomaly (
+ CErrors.anomaly (
Pp.strbrk"The global environment cannot be accessed during parsing")
let safe_env () = assert_not_parsing(); !global_env
diff --git a/library/globnames.ml b/library/globnames.ml
index bec463ecf2..a78f5f13a9 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Names
open Term
open Mod_subst
diff --git a/library/goptions.ml b/library/goptions.ml
index 4aa3a2a21d..9dc0f40588 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -9,7 +9,7 @@
(* This module manages customization parameters at the vernacular level *)
open Pp
-open Errors
+open CErrors
open Util
open Libobject
open Libnames
@@ -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
@@ -233,52 +237,57 @@ with Not_found ->
open Libobject
open Lib
-let declare_option cast uncast
+let warn_deprecated_option =
+ CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
+ (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
+ strbrk " is deprecated")
+
+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
- in
- let warn () =
- if depr then
- Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+ 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
@@ -287,36 +296,38 @@ 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 *)
(* Setting values of options *)
+let warn_unknown_option =
+ CWarnings.create ~name:"unknown-option" ~category:"option"
+ (fun key -> strbrk "There is no option " ++
+ str (nickname key) ++ str ".")
+
let set_option_value locality check_and_cast key v =
- let (name, depr, (_,read,write,lwrite,gwrite)) =
- try get_option key
- with Not_found ->
- errorlabstrm "Goptions.set_option_value"
- (str "There is no option " ++ str (nickname key) ++ str ".")
- in
- let write = match locality with
- | None -> write
- | Some true -> lwrite
- | Some false -> gwrite
- in
- write (check_and_cast v (read ()))
+ 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)) ->
+ write (get_locality locality) (check_and_cast v (read ()))
let bad_type_error () = error "Bad type of value for this option."
@@ -346,13 +357,18 @@ let check_unset_value v = function
let set_int_option_value_gen locality =
set_option_value locality check_int_value
let set_bool_option_value_gen locality key v =
- try set_option_value locality check_bool_value key v
- with UserError (_,s) -> Feedback.msg_warning s
+ set_option_value locality check_bool_value key v
let set_string_option_value_gen locality =
set_option_value locality check_string_value
let unset_option_value_gen locality key =
- try set_option_value locality check_unset_value key ()
- with UserError (_,s) -> Feedback.msg_warning s
+ 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
@@ -362,17 +378,17 @@ let set_string_option_value = set_string_option_value_gen None
let msg_option_value (name,v) =
match v with
- | BoolValue true -> str "true"
- | BoolValue false -> str "false"
+ | BoolValue true -> str "on"
+ | 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 ->
@@ -382,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;
@@ -401,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/heads.ml b/library/heads.ml
index 4c9b789769..02465f22fc 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -70,7 +70,7 @@ let kind_of_head env t =
| Const (cst,_) ->
(try on_subterm k l b (constant_head cst)
with Not_found ->
- Errors.anomaly
+ CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
str (Names.Constant.to_string cst)))
| Construct _ | CoFix _ ->
diff --git a/library/impargs.ml b/library/impargs.ml
index 4e344a9543..828d652c83 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Globnames
@@ -68,15 +68,14 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
let is_contextual_implicit_args () = !implicit_args.contextual
let is_maximal_implicit_args () = !implicit_args.maximal
-let with_implicits flags f x =
+let with_implicit_protection f x =
let oflags = !implicit_args in
try
- implicit_args := flags;
let rslt = f x in
implicit_args := oflags;
rslt
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = implicit_args := oflags in
iraise reraise
@@ -188,7 +187,7 @@ let is_reversible_pattern bound depth f l =
(* Precondition: rels in env are for inductive types only *)
let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
let rec frec rig (env,depth as ed) c =
- let hd = if strict then whd_betadeltaiota env c else c in
+ let hd = if strict then whd_all env c else c in
let c = if strongly_strict then hd else c in
match kind_of_term hd with
| Rel n when (n < bound+depth) && (n >= depth) ->
@@ -236,7 +235,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
let open Context.Rel.Declaration in
let rec aux env avoid n names t =
- let t = whd_betadeltaiota env t in
+ let t = whd_all env t in
match kind_of_term t with
| Prod (na,a,b) ->
let na',avoid' = find_displayed_name_in all avoid na (names,b) in
@@ -250,7 +249,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
add_free_rels_until strict strongly_strict revpat n env t Conclusion v
else v
in
- match kind_of_term (whd_betadeltaiota env t) with
+ match kind_of_term (whd_all env t) with
| Prod (na,a,b) ->
let na',avoid = find_displayed_name_in all [] na ([],b) in
let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
@@ -492,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) =
@@ -526,12 +527,6 @@ let impls_of_context ctx =
in
List.rev_map map (List.filter is_set ctx)
-let section_segment_of_reference = function
- | ConstRef con -> pi1 (section_segment_of_constant con)
- | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- pi1 (section_segment_of_mutual_inductive kn)
- | _ -> []
-
let adjust_side_condition p = function
| LessArgsThan n -> LessArgsThan (n+p)
| DefaultImpArgs -> DefaultImpArgs
@@ -545,7 +540,7 @@ let discharge_implicits (_,(req,l)) =
| ImplLocal -> None
| ImplInteractive (ref,flags,exp) ->
(try
- let vars = section_segment_of_reference ref in
+ let vars = variable_section_segment_of_reference ref in
let ref' = if isVarRef ref then ref else pop_global_reference ref in
let extra_impls = impls_of_context vars in
let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
@@ -563,7 +558,7 @@ let discharge_implicits (_,(req,l)) =
| ImplMutualInductive (kn,flags) ->
(try
let l' = List.map (fun (gr, l) ->
- let vars = section_segment_of_reference gr in
+ let vars = variable_section_segment_of_reference gr in
let extra_impls = impls_of_context vars in
((if isVarRef gr then gr else pop_global_reference gr),
List.map (add_section_impls vars extra_impls) l)) l
@@ -664,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/impargs.mli b/library/impargs.mli
index 34e529ca2c..3919a519c9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
-type implicits_flags
-val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
+val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments
@@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
val select_stronger_impargs : implicits_list list -> implicit_status list
-type implicit_interactive_request
-
-type implicit_discharge_request =
- | ImplLocal
- | ImplConstant of constant * implicits_flags
- | ImplMutualInductive of mutual_inductive * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
- implicit_interactive_request
-
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
(** Equality on [explicitation]. *)
diff --git a/library/kindops.ml b/library/kindops.ml
index c634193da8..21b1bec33c 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
let string_of_definition_kind def =
let (locality, poly, kind) = def in
- let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+ let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
match kind with
| Definition ->
begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
| Global -> "Global Instance"
end
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- Errors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind")
diff --git a/library/lib.ml b/library/lib.ml
index f8bb6bac59..f680ecee3c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Libnames
open Globnames
@@ -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
@@ -417,7 +422,7 @@ let add_section_variable id impl poly ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
- check_same_poly poly vars;
+ List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
let add_section_context ctx =
@@ -483,6 +488,12 @@ let section_segment_of_constant con =
let section_segment_of_mutual_inductive kn =
Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
+let variable_section_segment_of_reference = function
+ | ConstRef con -> pi1 (section_segment_of_constant con)
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ pi1 (section_segment_of_mutual_inductive kn)
+ | _ -> []
+
let section_instance = function
| VarRef id ->
let eq = function
@@ -500,13 +511,6 @@ let section_instance = function
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
- List.map (fun (vars,_,(x,_)) -> fun hyps ->
- named_of_variable_context
- (try pi1 (Names.Cmap.find con x)
- with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
(*************)
(* Sections. *)
@@ -607,15 +611,6 @@ let rec dp_of_mp = function
|Names.MPbound _ -> library_dp ()
|Names.MPdot (mp,_) -> dp_of_mp mp
-let rec split_mp = function
- |Names.MPfile dp -> dp, Names.DirPath.empty
- |Names.MPdot (prfx, lbl) ->
- let mprec, dprec = split_mp prfx in
- mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
- |Names.MPbound mbid ->
- let (_,id,dp) = Names.MBId.repr mbid in
- library_dp (), Names.DirPath.make [id]
-
let rec split_modpath = function
|Names.MPfile dp -> dp, []
|Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -627,20 +622,6 @@ let library_part = function
|VarRef id -> library_dp ()
|ref -> dp_of_mp (mp_of_global ref)
-let remove_section_part ref =
- let sp = Nametab.path_of_global ref in
- let dir,_ = repr_path sp in
- match ref with
- | VarRef id ->
- anomaly (Pp.str "remove_section_part not supported on local variables")
- | _ ->
- if is_dirpath_prefix_of dir (cwd ()) then
- (* Not yet (fully) discharged *)
- pop_dirpath_n (sections_depth ()) (cwd ())
- else
- (* Theorem/Lemma outside its outer section of definition *)
- dir
-
(************************)
(* Discharging names *)
diff --git a/library/lib.mli b/library/lib.mli
index e2e71ac90f..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]
@@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t
(** Extract the library part of a name even if in a section *)
val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t
val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
val library_part : Globnames.global_reference -> Names.DirPath.t
-val remove_section_part : Globnames.global_reference -> Names.DirPath.t
(** {6 Sections } *)
@@ -172,7 +170,8 @@ val named_of_variable_context : variable_context -> Context.Named.t
val section_segment_of_constant : Names.constant -> abstr_info
val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
-
+val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
+
val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
val is_in_section : Globnames.global_reference -> bool
@@ -190,10 +189,3 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive
val discharge_con : Names.constant -> Names.constant
val discharge_global : Globnames.global_reference -> Globnames.global_reference
val discharge_inductive : Names.inductive -> Names.inductive
-
-(* discharging a constant in one go *)
-val full_replacement_context : unit -> Opaqueproof.work_list list
-val full_section_segment_of_constant :
- Names.constant -> (Context.Named.t -> Context.Named.t) list
-
-
diff --git a/library/libnames.ml b/library/libnames.ml
index 99ff2f2fb4..dd74e192ff 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
diff --git a/library/libobject.ml b/library/libobject.ml
index b12d2038ae..caa03c85be 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -12,18 +12,6 @@ open Util
module Dyn = Dyn.Make(struct end)
-(* The relax flag is used to make it possible to load files while ignoring
- failures to incorporate some objects. This can be useful when one
- wants to work with restricted Coq programs that have only parts of
- the full capabilities, but may still be able to work correctly for
- limited purposes. One example is for the graphical interface, that uses
- such a limited Coq process to do only parsing. It loads .vo files, but
- is only interested in loading the grammar rule definitions. *)
-
-let relax_flag = ref false;;
-
-let relax b = relax_flag := b;;
-
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
@@ -43,7 +31,7 @@ let default_object s = {
load_function = (fun _ _ -> ());
open_function = (fun _ _ -> ());
subst_function = (fun _ ->
- Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
+ CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
classify_function = (fun obj -> Keep obj);
discharge_function = (fun _ -> None);
rebuild_function = (fun x -> x)}
@@ -109,36 +97,21 @@ let declare_object_full odecl =
let declare_object odecl =
try fst (declare_object_full odecl)
- with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+ with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
let declare_object_full odecl =
try declare_object_full odecl
- with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
-
-let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
+ with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
(* this function describes how the cache, load, open, and export functions
- are triggered. In relaxed mode, this function just return a meaningless
- value instead of raising an exception when they fail. *)
+ are triggered. *)
let apply_dyn_fun deflt f lobj =
let tag = object_tag lobj in
- try
- let dodecl =
- try
- Hashtbl.find cache_tab tag
- with Not_found ->
- failwith "local to_apply_dyn_fun" in
- f dodecl
- with
- Failure "local to_apply_dyn_fun" ->
- if not (!relax_flag || Hashtbl.mem missing_tab tag) then
- begin
- Feedback.msg_warning
- (Pp.str ("Cannot find library functions for an object with tag "
- ^ tag ^ " (a plugin may be missing)"));
- Hashtbl.add missing_tab tag ()
- end;
- deflt
+ let dodecl =
+ try Hashtbl.find cache_tab tag
+ with Not_found -> assert false
+ in
+ f dodecl
let cache_object ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index dbe0de8f8a..51b9af059f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -107,7 +107,6 @@ val subst_object : substitution * obj -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
val rebuild_object : obj -> obj
-val relax : bool -> unit
(** {6 Debug} *)
diff --git a/library/library.ml b/library/library.ml
index bc7723f481..d44f796a7a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
@@ -64,7 +64,7 @@ let fetch_delayed del =
let () = close_in ch in
if not (String.equal digest digest') then raise (Faulty f);
obj
- with e when Errors.noncritical e -> raise (Faulty f)
+ with e when CErrors.noncritical e -> raise (Faulty f)
end
@@ -271,6 +271,12 @@ exception LibUnmappedDir
exception LibNotFound
type library_location = LibLoaded | LibInPath
+let warn_several_object_files =
+ CWarnings.create ~name:"several-object-files" ~category:"require"
+ (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
+ strbrk " instead of " ++ str vo ++
+ strbrk " because it is more recent")
+
let locate_absolute_library dir =
(* Search in loadpath *)
let pref, base = split_dirpath dir in
@@ -287,9 +293,8 @@ let locate_absolute_library dir =
| [] -> raise LibNotFound
| [file] -> file
| [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
- str vo ++ str " because it is more recent");
- vi
+ warn_several_object_files (vi, vo);
+ vi
| [vo;vi] -> vo
| _ -> assert false
@@ -311,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
| [lpath, file] -> lpath, file
| [lpath_vo, vo; lpath_vi, vi]
when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
- str vo ++ str " because it is more recent");
+ warn_several_object_files (vi, vo);
lpath_vi, vi
| [lpath_vo, vo; _ ] -> lpath_vo, vo
| _ -> assert false
@@ -448,13 +452,13 @@ let intern_from_file f =
module DPMap = Map.Make(DirPath)
let rec intern_library (needed, contents) (dir, f) from =
- Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
(* Look if already listed and consequently its dependencies too *)
try (DPMap.find dir contents).library_digests, (needed, contents)
with Not_found ->
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in
@@ -464,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from =
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
- m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
+ m.library_digests, intern_library_deps (needed, contents) dir m f
and intern_library_deps libs dir m from =
let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
(dir :: needed, DPMap.add dir m contents )
and intern_mandatory_library caller from libs (dir,d) =
- let digest, libs = intern_library libs (dir, None) from in
+ let digest, libs = intern_library libs (dir, None) (Some from) in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
+ errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
+ over library " ++ pr_dirpath dir);
libs
let rec_intern_library libs (dir, f) =
@@ -547,12 +553,20 @@ let in_require : require_obj -> obj =
let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
+let warn_require_in_module =
+ CWarnings.create ~name:"require-in-module" ~category:"deprecated"
+ (fun () -> strbrk "Require inside a module is" ++
+ strbrk " deprecated and strongly discouraged. " ++
+ strbrk "You can Require a module at toplevel " ++
+ strbrk "and optionally Import it inside another one.")
+
let require_library_from_dirpath modrefl export =
let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
let modrefl = List.map fst modrefl in
if Lib.is_module_or_modtype () then
begin
+ warn_require_in_module ();
add_anonymous_leaf (in_require (needed,modrefl,None));
Option.iter (fun exp ->
add_anonymous_leaf (in_import_library (modrefl,exp)))
@@ -720,7 +734,7 @@ let save_library_to ?todo dir f otab =
except Int.Set.empty in
let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
Array.iteri (fun i x ->
- if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
+ if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
opaque_table;
let sd = {
@@ -752,7 +766,7 @@ let save_library_to ?todo dir f otab =
if not (Nativelib.compile_library dir ast fn) then
error "Could not compile the library to native code."
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = Feedback.msg_warning (str "Removed file " ++ str f') in
let () = close_out ch in
let () = Sys.remove f' in
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 33c0f41e17..d03c6c5553 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -8,7 +8,7 @@
open Pp
open Util
-open Errors
+open CErrors
open Names
open Libnames
@@ -50,6 +50,13 @@ let remove_load_path dir =
let filter p = not (String.equal p.path_physical dir) in
load_paths := List.filter filter !load_paths
+let warn_overriding_logical_loadpath =
+ CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
+ (fun (phys_path, old_path, coq_path) ->
+ str phys_path ++ strbrk " was previously bound to " ++
+ pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+ pr_dirpath coq_path)
+
let add_load_path phys_path coq_path ~implicit =
let phys_path = CUnix.canonical_path_name phys_path in
let filter p = String.equal p.path_physical phys_path in
@@ -65,17 +72,12 @@ let add_load_path phys_path coq_path ~implicit =
let replace =
if DirPath.equal coq_path old_path then
implicit <> old_implicit
- else if DirPath.equal coq_path (Nameops.default_root_prefix)
- && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
- false (* This is the default "-I ." path, don't override the old path *)
else
let () =
(* Do not warn when overriding the default "-I ." path *)
if not (DirPath.equal old_path Nameops.default_root_prefix) then
- Feedback.msg_warning
- (str phys_path ++ strbrk " was previously bound to " ++
- pr_dirpath old_path ++ strbrk "; it is remapped to " ++
- pr_dirpath coq_path) in
+ warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
+ in
true in
if replace then
begin
diff --git a/library/nametab.ml b/library/nametab.ml
index db902d625b..fa5db37ed5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -82,6 +82,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE
struct
type elt = E.t
+ (* A name became inaccessible, even with absolute qualification.
+ Example:
+ Module F (X : S). Module X.
+ The argument X of the functor F is masked by the inner module X.
+ *)
+ let masking_absolute n =
+ Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"))
+
type user_name = U.t
type path_status =
@@ -119,9 +127,7 @@ struct
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- Feedback.msg_warning (str ("Trying to mask the absolute name \""
- ^ U.to_string n ^ "\"!"));
- tree.path
+ masking_absolute n; tree.path
| Nothing
| Relative _ -> Relative (uname,o)
else tree.path
@@ -144,7 +150,6 @@ struct
| Nothing
| Relative _ -> mktree (Absolute (uname,o)) tree.map
-
let rec push_exactly uname o level tree = function
| [] ->
anomaly (Pp.str "Prefix longer than path! Impossible!")
@@ -155,9 +160,7 @@ let rec push_exactly uname o level tree = function
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- Feedback.msg_warning (str ("Trying to mask the absolute name \""
- ^ U.to_string n ^ "\"!"));
- tree.path
+ masking_absolute n; tree.path
| Nothing
| Relative _ -> Relative (uname,o)
in
diff --git a/library/states.ml b/library/states.ml
index 2e1be764ab..95bd819d66 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -35,7 +35,7 @@ let with_state_protection f x =
try
let a = f x in unfreeze st; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
(unfreeze st; iraise reraise)
let with_state_protection_on_exception = Future.transactify
diff --git a/library/summary.ml b/library/summary.ml
index edea7dbe50..6efa07f388 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
module Dyn = Dyn.Make(struct end)
@@ -105,10 +105,10 @@ let unfreeze_summaries fs =
in
let fold id decl state =
try fold id decl state
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
- (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e));
+ (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
iraise e
in
(** We rely on the order of the frozen list, and the order of folding *)
@@ -149,7 +149,7 @@ let unfreeze_summary datas =
let (name, summary) = Int.Map.find id !summaries in
try summary.unfreeze_function data
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
prerr_endline ("Exception unfreezing " ^ name);
iraise e)
datas
@@ -186,4 +186,29 @@ let ref ?(freeze=fun _ r -> r) ~name x =
init_function = (fun () -> r := x) };
r
+module Local = struct
+
+type 'a local_ref = ('a CEphemeron.key * string) ref
+
+let (:=) r v = r := (CEphemeron.create v, snd !r)
+
+let (!) r =
+ let key, name = !r in
+ try CEphemeron.get key
+ with CEphemeron.InvalidKey ->
+ let _, { init_function } =
+ Int.Map.find (String.hash (mangle name)) !summaries in
+ init_function ();
+ CEphemeron.get (fst !r)
+
+let ref ?(freeze=fun x -> x) ~name init =
+ let r = Pervasives.ref (CEphemeron.create init, name) in
+ declare_summary name
+ { freeze_function = (fun _ -> freeze !r);
+ unfreeze_function = ((:=) r);
+ init_function = (fun () -> r := init) };
+ r
+
+end
+
let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index 27889cab27..1b57613cb7 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit
val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
+ * workers. It is useful to implement a local cache for example. *)
+module Local : sig
+
+ type 'a local_ref
+ val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+ val (:=) : 'a local_ref -> 'a -> unit
+ val (!) : 'a local_ref -> 'a
+
+end
+
(** Special name for the summary of ML modules. This summary entry is
special because its unfreeze may load ML code and hence add summary
entries. Thus is has to be recognizable, and handled appropriately *)
diff --git a/library/universes.ml b/library/universes.ml
index 75cbd5604b..112b20a4c4 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -112,7 +112,7 @@ let enforce_eq_instances_univs strict x y c =
let d = if strict then ULub else UEq in
let ax = Instance.to_array x and ay = Instance.to_array y in
if Array.length ax != Array.length ay then
- Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
+ CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
Pp.str " instances of different lengths");
CArray.fold_right2
(fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
@@ -337,7 +337,7 @@ let existing_instance ctx inst =
and a2 = Instance.to_array (UContext.instance ctx) in
let len1 = Array.length a1 and len2 = Array.length a2 in
if not (len1 == len2) then
- Errors.errorlabstrm "Universes"
+ CErrors.errorlabstrm "Universes"
(str "Polymorphic constant expected " ++ int len2 ++
str" levels but was given " ++ int len1)
else ()
@@ -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
@@ -926,9 +995,7 @@ let normalize_context_set ctx us algs =
mentionning other variables remain in noneqs. *)
let noneqs, ucstrsl, ucstrsr =
Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
- let lus = LMap.mem l us
- and rus = LMap.mem r us
- in
+ let lus = LMap.mem l us and rus = LMap.mem r us in
let ucstrsl' =
if lus then add_list_map l (d, r) ucstrsl
else ucstrsl
@@ -1090,13 +1157,6 @@ let solve_constraints_system levels level_bounds level_min =
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 when not (Univ.Level.is_small u) -> *)
- (* v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
- (* | _ -> () *)
- (* done *)
done;
v
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-02 22:22:27 +0000