aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml383
-rw-r--r--library/coqlib.mli211
-rw-r--r--library/declare.ml43
-rw-r--r--library/declaremods.ml14
-rw-r--r--library/decls.ml10
-rw-r--r--library/global.ml14
-rw-r--r--library/global.mli7
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml76
-rw-r--r--library/goptions.mli11
-rw-r--r--library/heads.ml3
-rw-r--r--library/impargs.ml47
-rw-r--r--library/keys.ml4
-rw-r--r--library/keys.mli2
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml153
-rw-r--r--library/lib.mli3
-rw-r--r--library/libnames.ml4
-rw-r--r--library/libnames.mli2
-rw-r--r--library/libobject.ml13
-rw-r--r--library/library.ml40
-rw-r--r--library/library.mllib2
-rw-r--r--library/loadpath.ml4
-rw-r--r--library/nameops.ml135
-rw-r--r--library/nameops.mli92
-rw-r--r--library/nametab.ml24
-rw-r--r--library/nametab.mli38
-rw-r--r--library/summary.ml12
-rw-r--r--library/universes.ml1162
-rw-r--r--library/universes.mli238
30 files changed, 1042 insertions, 1711 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
new file mode 100644
index 0000000000..0cb8c7afcf
--- /dev/null
+++ b/library/coqlib.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open Names
+open Libnames
+open Globnames
+open Nametab
+
+let coq = Nameops.coq_string (* "Coq" *)
+
+(************************************************************************)
+(* Generic functions to find Coq objects *)
+
+type message = string
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+
+let find_reference locstr dir s =
+ let dp = make_dir dir in
+ let sp = Libnames.make_path dp (Id.of_string s) in
+ try Nametab.global_of_path sp
+ with Not_found ->
+ (* Following bug 5066 we are more permissive with the handling
+ of not found errors here *)
+ user_err ~hdr:locstr
+ Pp.(str "cannot find " ++ Libnames.pr_path sp ++
+ str "; maybe library " ++ Libnames.pr_dirpath dp ++
+ str " has to be required first.")
+
+let coq_reference locstr dir s = find_reference locstr (coq::dir) s
+
+let has_suffix_in_dirs dirs ref =
+ let dir = dirpath (path_of_global ref) in
+ List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
+let gen_reference_in_modules locstr dirs s =
+ let dirs = List.map make_dir dirs in
+ let qualid = qualid_of_string s in
+ let all = Nametab.locate_all qualid in
+ let all = List.sort_uniquize RefOrdered_env.compare all in
+ let these = List.filter (has_suffix_in_dirs dirs) all in
+ match these with
+ | [x] -> x
+ | [] ->
+ anomaly ~label:locstr (str "cannot find " ++ str s ++
+ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
+ | l ->
+ anomaly ~label:locstr
+ (str "ambiguous name " ++ str s ++ str " can represent " ++
+ prlist_with_sep pr_comma
+ (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
+ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
+
+(* For tactics/commands requiring vernacular libraries *)
+
+let check_required_library d =
+ let dir = make_dir d in
+ if Library.library_is_loaded dir then ()
+ else
+ let in_current_dir = match Lib.current_mp () with
+ | MPfile dp -> DirPath.equal dir dp
+ | _ -> false
+ in
+ if not in_current_dir then
+(* Loading silently ...
+ let m, prefix = List.sep_last d' in
+ read_library
+ (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
+*)
+(* or failing ...*)
+ user_err ~hdr:"Coqlib.check_required_library"
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
+
+(************************************************************************)
+(* Specific Coq objects *)
+
+let init_reference dir s =
+ let d = coq::"Init"::dir in
+ check_required_library d; find_reference "Coqlib" d s
+
+let logic_reference dir s =
+ let d = coq::"Logic"::dir in
+ check_required_library d; find_reference "Coqlib" d s
+
+let arith_dir = [coq;"Arith"]
+let arith_modules = [arith_dir]
+
+let numbers_dir = [coq;"Numbers"]
+let parith_dir = [coq;"PArith"]
+let narith_dir = [coq;"NArith"]
+let zarith_dir = [coq;"ZArith"]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
+
+let init_dir = [coq;"Init"]
+let init_modules = [
+ init_dir@["Datatypes"];
+ init_dir@["Logic"];
+ init_dir@["Specif"];
+ init_dir@["Logic_Type"];
+ init_dir@["Nat"];
+ init_dir@["Peano"];
+ init_dir@["Wf"]
+]
+
+let prelude_module_name = init_dir@["Prelude"]
+let prelude_module = make_dir prelude_module_name
+
+let logic_module_name = init_dir@["Logic"]
+let logic_module = make_dir logic_module_name
+
+let logic_type_module_name = init_dir@["Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = init_dir@["Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let jmeq_module_name = [coq;"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
+
+(* TODO: temporary hack. Works only if the module isn't an alias *)
+let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
+let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+
+(** Identity *)
+
+let id = make_con datatypes_module "idProp"
+let type_of_id = make_con datatypes_module "IDProp"
+
+(** Natural numbers *)
+let nat_kn = make_ind datatypes_module "nat"
+let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+
+let glob_nat = IndRef (nat_kn,0)
+
+let path_of_O = ((nat_kn,0),1)
+let path_of_S = ((nat_kn,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+(** Booleans *)
+let bool_kn = make_ind datatypes_module "bool"
+
+let glob_bool = IndRef (bool_kn,0)
+
+let path_of_true = ((bool_kn,0),1)
+let path_of_false = ((bool_kn,0),2)
+let glob_true = ConstructRef path_of_true
+let glob_false = ConstructRef path_of_false
+
+(** Equality *)
+let eq_kn = make_ind logic_module "eq"
+let glob_eq = IndRef (eq_kn,0)
+
+let identity_kn = make_ind datatypes_module "identity"
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_ind jmeq_module "JMeq"
+let glob_jmeq = IndRef (jmeq_kn,0)
+
+type coq_sigma_data = {
+ proj1 : global_reference;
+ proj2 : global_reference;
+ elim : global_reference;
+ intro : global_reference;
+ typ : global_reference }
+
+type coq_bool_data = {
+ andb : global_reference;
+ andb_prop : global_reference;
+ andb_true_intro : global_reference}
+
+let build_bool_type () =
+ { andb = init_reference ["Datatypes"] "andb";
+ andb_prop = init_reference ["Datatypes"] "andb_prop";
+ andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" }
+
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.")
+
+let build_sigma_type () =
+ { proj1 = init_reference ["Specif"] "projT1";
+ proj2 = init_reference ["Specif"] "projT2";
+ elim = init_reference ["Specif"] "sigT_rect";
+ intro = init_reference ["Specif"] "existT";
+ typ = init_reference ["Specif"] "sigT" }
+
+let build_sigma () =
+ { proj1 = init_reference ["Specif"] "proj1_sig";
+ proj2 = init_reference ["Specif"] "proj2_sig";
+ elim = init_reference ["Specif"] "sig_rect";
+ intro = init_reference ["Specif"] "exist";
+ typ = init_reference ["Specif"] "sig" }
+
+
+let build_prod () =
+ { proj1 = init_reference ["Datatypes"] "fst";
+ proj2 = init_reference ["Datatypes"] "snd";
+ elim = init_reference ["Datatypes"] "prod_rec";
+ intro = init_reference ["Datatypes"] "pair";
+ typ = init_reference ["Datatypes"] "prod" }
+
+(* Equalities *)
+type coq_eq_data = {
+ eq : global_reference;
+ ind : global_reference;
+ refl : global_reference;
+ sym : global_reference;
+ trans: global_reference;
+ congr: global_reference }
+
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+ inv_eq : global_reference; (* : forall params, t -> Prop *)
+ inv_ind : global_reference; (* : forall params P y, eq params y -> P y *)
+ inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
+
+let lazy_init_reference dir id = lazy (init_reference dir id)
+let lazy_logic_reference dir id = lazy (logic_reference dir id)
+
+(* Leibniz equality on Type *)
+
+let coq_eq_eq = lazy_init_reference ["Logic"] "eq"
+let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl"
+let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind"
+let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal"
+let coq_eq_sym = lazy_init_reference ["Logic"] "eq_sym"
+let coq_eq_trans = lazy_init_reference ["Logic"] "eq_trans"
+let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+ lazy_init_reference ["Logic"] "f_equal_canonical_form"
+
+let build_coq_eq_data () =
+ let _ = check_required_library logic_module_name in {
+ eq = Lazy.force coq_eq_eq;
+ ind = Lazy.force coq_eq_ind;
+ refl = Lazy.force coq_eq_refl;
+ sym = Lazy.force coq_eq_sym;
+ trans = Lazy.force coq_eq_trans;
+ congr = Lazy.force coq_eq_congr }
+
+let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
+let build_coq_eq_sym () = Lazy.force coq_eq_sym
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+let build_coq_inversion_eq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_eq;
+ inv_ind = Lazy.force coq_eq_ind;
+ inv_congr = Lazy.force coq_eq_congr_canonical }
+
+(* Heterogenous equality on Type *)
+
+let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq"
+let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom"
+let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl"
+let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind"
+let coq_jmeq_sym = lazy_logic_reference ["JMeq"] "JMeq_sym"
+let coq_jmeq_congr = lazy_logic_reference ["JMeq"] "JMeq_congr"
+let coq_jmeq_trans = lazy_logic_reference ["JMeq"] "JMeq_trans"
+let coq_jmeq_congr_canonical =
+ lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form"
+
+let build_coq_jmeq_data () =
+ let _ = check_required_library jmeq_module_name in {
+ eq = Lazy.force coq_jmeq_eq;
+ ind = Lazy.force coq_jmeq_ind;
+ refl = Lazy.force coq_jmeq_refl;
+ sym = Lazy.force coq_jmeq_sym;
+ trans = Lazy.force coq_jmeq_trans;
+ congr = Lazy.force coq_jmeq_congr }
+
+let build_coq_inversion_jmeq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_jmeq_hom;
+ inv_ind = Lazy.force coq_jmeq_ind;
+ inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
+(* Specif *)
+let coq_sumbool = lazy_init_reference ["Specif"] "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type as a Type *)
+let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity"
+let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl"
+let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind"
+let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr"
+let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym"
+let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans"
+let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form"
+
+let build_coq_identity_data () =
+ let _ = check_required_library datatypes_module_name in {
+ eq = Lazy.force coq_identity_eq;
+ ind = Lazy.force coq_identity_ind;
+ refl = Lazy.force coq_identity_refl;
+ sym = Lazy.force coq_identity_sym;
+ trans = Lazy.force coq_identity_trans;
+ congr = Lazy.force coq_identity_congr }
+
+let build_coq_inversion_identity_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_type_module_name in {
+ inv_eq = Lazy.force coq_identity_eq;
+ inv_ind = Lazy.force coq_identity_ind;
+ inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_true_eq;
+ inv_ind = Lazy.force coq_eq_true_ind;
+ inv_congr = Lazy.force coq_eq_true_congr }
+
+(* The False proposition *)
+let coq_False = lazy_init_reference ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True = lazy_init_reference ["Logic"] "True"
+let coq_I = lazy_init_reference ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_reference ["Logic"] "not"
+let coq_and = lazy_init_reference ["Logic"] "and"
+let coq_conj = lazy_init_reference ["Logic"] "conj"
+let coq_or = lazy_init_reference ["Logic"] "or"
+let coq_ex = lazy_init_reference ["Logic"] "ex"
+let coq_iff = lazy_init_reference ["Logic"] "iff"
+
+let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
+
+(* Runtime part *)
+let build_coq_True () = Lazy.force coq_True
+let build_coq_I () = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not () = Lazy.force coq_not
+let build_coq_and () = Lazy.force coq_and
+let build_coq_conj () = Lazy.force coq_conj
+let build_coq_or () = Lazy.force coq_or
+let build_coq_ex () = Lazy.force coq_ex
+let build_coq_iff () = Lazy.force coq_iff
+
+let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj
+let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
+let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref."))
+let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
+let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
+let coq_not_ref = lazy (init_reference ["Logic"] "not")
+let coq_False_ref = lazy (init_reference ["Logic"] "False")
+let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
+let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
+let coq_or_ref = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref = lazy (init_reference ["Logic"] "iff")
+
+(* Deprecated *)
+let gen_reference = coq_reference
+
diff --git a/library/coqlib.mli b/library/coqlib.mli
new file mode 100644
index 0000000000..716d97c9d0
--- /dev/null
+++ b/library/coqlib.mli
@@ -0,0 +1,211 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Libnames
+open Globnames
+open Util
+
+(** This module collects the global references, constructions and
+ patterns of the standard library used in ocaml files *)
+
+(** The idea is to migrate to rebindable name-based approach, thus the
+ only function this FILE will provide will be:
+
+ [find_reference : string -> global_reference]
+
+ such that [find_reference "core.eq.type"] returns the proper [global_reference]
+
+ [bind_reference : string -> global_reference -> unit]
+
+ will bind a reference.
+
+ A feature based approach would be possible too.
+
+ Contrary to the old approach of raising an anomaly, we expect
+ tactics to gracefully fail in the absence of some primitive.
+
+ This is work in progress, see below.
+*)
+
+(** {6 ... } *)
+(** [find_reference caller_message [dir;subdir;...] s] returns a global
+ reference to the name dir.subdir.(...).s; the corresponding module
+ must have been required or in the process of being compiled so that
+ it must be used lazily; it raises an anomaly with the given message
+ if not found *)
+
+type message = string
+
+val find_reference : message -> string list -> string -> global_reference
+val coq_reference : message -> string list -> string -> global_reference
+
+(** For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
+
+(** Search in several modules (not prefixed by "Coq") *)
+val gen_reference_in_modules : string->string list list-> string -> global_reference
+
+val arith_modules : string list list
+val zarith_base_modules : string list list
+val init_modules : string list list
+
+(** {6 Global references } *)
+
+(** Modules *)
+val prelude_module : DirPath.t
+
+val logic_module : DirPath.t
+val logic_module_name : string list
+
+val logic_type_module : DirPath.t
+
+val jmeq_module : DirPath.t
+val jmeq_module_name : string list
+
+val datatypes_module_name : string list
+
+(** Identity *)
+val id : constant
+val type_of_id : constant
+
+(** Natural numbers *)
+val nat_path : full_path
+val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
+val glob_O : global_reference
+val glob_S : global_reference
+
+(** Booleans *)
+val glob_bool : global_reference
+val path_of_true : constructor
+val path_of_false : constructor
+val glob_true : global_reference
+val glob_false : global_reference
+
+
+(** Equality *)
+val glob_eq : global_reference
+val glob_identity : global_reference
+val glob_jmeq : global_reference
+
+(** {6 ... } *)
+(** Constructions and patterns related to Coq initial state are unknown
+ at compile time. Therefore, we can only provide methods to build
+ them at runtime. This is the purpose of the [constr delayed] and
+ [constr_pattern delayed] types. Objects of this time needs to be
+ forced with [delayed_force] to get the actual constr or pattern
+ at runtime. *)
+
+type coq_bool_data = {
+ andb : global_reference;
+ andb_prop : global_reference;
+ andb_true_intro : global_reference}
+val build_bool_type : coq_bool_data delayed
+
+(** {6 For Equality tactics } *)
+type coq_sigma_data = {
+ proj1 : global_reference;
+ proj2 : global_reference;
+ elim : global_reference;
+ intro : global_reference;
+ typ : global_reference }
+
+val build_sigma_set : coq_sigma_data delayed
+val build_sigma_type : coq_sigma_data delayed
+val build_sigma : coq_sigma_data delayed
+
+(* val build_sigma_type_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_sigma_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_prod_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
+(* val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set *)
+
+(** Non-dependent pairs in Set from Datatypes *)
+val build_prod : coq_sigma_data delayed
+
+type coq_eq_data = {
+ eq : global_reference;
+ ind : global_reference;
+ refl : global_reference;
+ sym : global_reference;
+ trans: global_reference;
+ congr: global_reference }
+
+val build_coq_eq_data : coq_eq_data delayed
+
+val build_coq_identity_data : coq_eq_data delayed
+val build_coq_jmeq_data : coq_eq_data delayed
+
+val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *)
+val build_coq_f_equal2 : global_reference delayed
+
+(** Data needed for discriminate and injection *)
+
+type coq_inversion_data = {
+ inv_eq : global_reference; (** : forall params, args -> Prop *)
+ inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args
+ -> P args *)
+ inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args ->
+ f params = f args *)
+}
+
+val build_coq_inversion_eq_data : coq_inversion_data delayed
+val build_coq_inversion_identity_data : coq_inversion_data delayed
+val build_coq_inversion_jmeq_data : coq_inversion_data delayed
+val build_coq_inversion_eq_true_data : coq_inversion_data delayed
+
+(** Specif *)
+val build_coq_sumbool : global_reference delayed
+
+(** {6 ... } *)
+(** Connectives
+ The False proposition *)
+val build_coq_False : global_reference delayed
+
+(** The True proposition and its unique proof *)
+val build_coq_True : global_reference delayed
+val build_coq_I : global_reference delayed
+
+(** Negation *)
+val build_coq_not : global_reference delayed
+
+(** Conjunction *)
+val build_coq_and : global_reference delayed
+val build_coq_conj : global_reference delayed
+val build_coq_iff : global_reference delayed
+
+val build_coq_iff_left_proj : global_reference delayed
+val build_coq_iff_right_proj : global_reference delayed
+
+(** Disjunction *)
+val build_coq_or : global_reference delayed
+
+(** Existential quantifier *)
+val build_coq_ex : global_reference delayed
+
+val coq_eq_ref : global_reference lazy_t
+val coq_identity_ref : global_reference lazy_t
+val coq_jmeq_ref : global_reference lazy_t
+val coq_eq_true_ref : global_reference lazy_t
+val coq_existS_ref : global_reference lazy_t
+val coq_existT_ref : global_reference lazy_t
+val coq_exist_ref : global_reference lazy_t
+val coq_not_ref : global_reference lazy_t
+val coq_False_ref : global_reference lazy_t
+val coq_sumbool_ref : global_reference lazy_t
+val coq_sig_ref : global_reference lazy_t
+
+val coq_or_ref : global_reference lazy_t
+val coq_iff_ref : global_reference lazy_t
+
+(* Deprecated functions *)
+val gen_reference : message -> string list -> string -> global_reference
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
diff --git a/library/declare.ml b/library/declare.ml
index c9992fff3b..7d0edbc8b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -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 CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+ else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
end else
let () = check_exists sp in
let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -385,7 +385,7 @@ let declare_projections mind =
let declare_mind mie =
let id = match mie.mind_entry_inds with
| ind::_ -> ind.mind_entry_typename
- | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
+ | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
let isrecord,isprim = declare_projections mind in
@@ -400,7 +400,7 @@ let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
Flags.if_verbose Feedback.msg_info (match l with
- | [] -> anomaly (Pp.str "no recursive definition")
+ | [] -> anomaly (Pp.str "no recursive definition.")
| [id] -> pr_id id ++ str " is recursively defined" ++
(match indexes with
| Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
@@ -455,7 +455,7 @@ let declare_universe_context poly ctx =
type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
let cache_universes (p, l) =
- let glob = Universes.global_universe_names () in
+ let glob = Global.global_universe_names () in
let glob', ctx =
List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
((Idmap.add id (p, lev) idl,
@@ -464,7 +464,7 @@ let cache_universes (p, l) =
(glob, Univ.ContextSet.empty) l
in
cache_universe_context (p, ctx);
- Universes.set_global_universe_names glob'
+ Global.set_global_universe_names glob'
let input_universes : universe_decl -> Libobject.obj =
declare_object
@@ -478,8 +478,8 @@ let do_universe poly l =
let in_section = Lib.sections_are_opened () in
let () =
if poly && not in_section then
- user_err_loc (Loc.ghost, "Constraint",
- str"Cannot declare polymorphic universes outside sections")
+ user_err ~hdr:"Constraint"
+ (str"Cannot declare polymorphic universes outside sections")
in
let l =
List.map (fun (l, id) ->
@@ -512,36 +512,35 @@ let do_constraint poly l =
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
+ | GProp -> Loc.tag (false, Univ.Level.prop)
+ | GSet -> Loc.tag (false, Univ.Level.set)
+ | GType None | GType (Some (_, Anonymous)) ->
+ user_err ~hdr:"Constraint"
+ (str "Cannot declare constraints on anonymous universes")
+ | GType (Some (loc, Name id)) ->
+ let names, _ = Global.global_universe_names () in
try loc, Idmap.find id names
with Not_found ->
- user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
in
let in_section = Lib.sections_are_opened () in
let () =
if poly && not in_section then
- user_err_loc (Loc.ghost, "Constraint",
- str"Cannot declare polymorphic constraints outside sections")
+ user_err ~hdr:"Constraint"
+ (str"Cannot declare polymorphic constraints outside sections")
in
- let check_poly loc p loc' p' =
+ let check_poly ?loc p loc' p' =
if poly then ()
else if p || p' then
let loc = if p then loc else loc' in
- user_err_loc (loc, "Constraint",
- str "Cannot declare a global constraint on " ++
+ user_err ?loc ~hdr:"Constraint"
+ (str "Cannot declare a global constraint on " ++
str "a polymorphic universe, use "
++ str "Polymorphic Constraint instead")
in
let constraints = List.fold_left (fun acc (l, d, r) ->
let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
- check_poly ploc p rloc p';
+ check_poly ?loc:ploc p rloc p';
Univ.Constraint.add (lu, d, ru) acc)
Univ.Constraint.empty l
in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b2806a1ac3..c98d4a7f31 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -166,13 +166,13 @@ let consistency_checks exists dir dirinfo =
let globref =
try Nametab.locate_dir (qualid_of_dirpath dir)
with Not_found ->
- errorlabstrm "consistency_checks"
+ user_err ~hdr:"consistency_checks"
(pr_dirpath dir ++ str " should already exist!")
in
assert (eq_global_dir_reference globref dirinfo)
else
if Nametab.exists_dir dir then
- errorlabstrm "consistency_checks"
+ user_err ~hdr:"consistency_checks"
(pr_dirpath dir ++ str " already exists")
let compute_visibility exists i =
@@ -252,7 +252,7 @@ let in_modkeep : Lib.lib_objects -> obj =
let do_modtype i sp mp sobjs =
if Nametab.exists_modtype sp then
- anomaly (pr_path sp ++ str " already exists");
+ anomaly (pr_path sp ++ str " already exists.");
Nametab.push_modtype (Nametab.Until i) sp mp;
ModSubstObjs.set mp sobjs
@@ -345,7 +345,7 @@ let get_applications mexpr =
let rec get params = function
| MEident mp -> mp, params
| MEapply (fexpr, mp) -> get (mp::params) fexpr
- | MEwith _ -> error "Non-atomic functor application."
+ | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
in get [] mexpr
(** Create the substitution corresponding to some functor applications *)
@@ -353,7 +353,7 @@ let get_applications mexpr =
let rec compute_subst env mbids sign mp_l inl =
match mbids,mp_l with
| _,[] -> mbids,empty_subst
- | [],r -> error "Application of a functor with too few arguments."
+ | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
| mbid::mbids,mp::mp_l ->
let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
let mb = Environ.lookup_module mp env in
@@ -777,7 +777,7 @@ let rec decompose_functor mpl typ =
match mpl, typ with
| [], _ -> typ
| _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
- | _ -> error "Application of a functor with too much arguments."
+ | _ -> user_err Pp.(str "Application of a functor with too much arguments.")
exception NoIncludeSelf
@@ -883,7 +883,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
(* If not, let's do it now ... *)
let mp' = Global.import cenv univ digest in
if not (ModPath.equal mp mp') then
- anomaly (Pp.str "Unexpected disk module name");
+ anomaly (Pp.str "Unexpected disk module name.");
in
let sobjs,keepobjs = objs in
do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
diff --git a/library/decls.ml b/library/decls.ml
index 6e21880f1f..2952c258a5 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -14,6 +14,8 @@ open Names
open Decl_kinds
open Libnames
+module NamedDecl = Context.Named.Declaration
+
(** Datas associated to section variables and local definitions *)
type variable_data =
@@ -46,20 +48,18 @@ let constant_kind kn = Cmap.find kn !csttab
(** Miscellaneous functions. *)
-open Context.Named.Declaration
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
(fun d signv ->
- let id = get_id d in
- let d = if variable_opacity id then LocalAssum (id, get_type d) else d in
+ let id = NamedDecl.get_id d in
+ let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
let last_section_hyps dir =
Context.Named.fold_outside
(fun d sec_ids ->
- let id = get_id d in
+ let id = NamedDecl.get_id d in
try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
with Not_found -> sec_ids)
(Environ.named_context (Global.env()))
diff --git a/library/global.ml b/library/global.ml
index e748434d24..1ba86699d3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -8,6 +8,7 @@
open Names
open Environ
+open Decl_kinds
(** We introduce here the global environment of the system,
and we declare it as a synchronized table. *)
@@ -43,7 +44,7 @@ let () =
let assert_not_parsing () =
if !Flags.we_are_parsing then
CErrors.anomaly (
- Pp.strbrk"The global environment cannot be accessed during parsing")
+ Pp.strbrk"The global environment cannot be accessed during parsing.")
let safe_env () = assert_not_parsing(); !global_env
@@ -229,6 +230,17 @@ let universes_of_global env r =
let universes_of_global gr =
universes_of_global (env ()) gr
+(** Global universe names *)
+type universe_names =
+ (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+
+let global_universes =
+ Summary.ref ~name:"Global universe names"
+ ((Idmap.empty, Univ.LMap.empty) : universe_names)
+
+let global_universe_names () = !global_universes
+let set_global_universe_names s = global_universes := s
+
let is_polymorphic r =
let env = env() in
match r with
diff --git a/library/global.mli b/library/global.mli
index 247ca20b47..a4a38ce846 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -96,6 +96,13 @@ val constraints_of_constant_body :
val universes_of_constant_body :
Declarations.constant_body -> Univ.universe_context
+(** Global universe name <-> level mapping *)
+type universe_names =
+ (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+
+val global_universe_names : unit -> universe_names
+val set_global_universe_names : universe_names -> unit
+
(** {6 Compiled libraries } *)
val start_library : DirPath.t -> module_path
diff --git a/library/globnames.ml b/library/globnames.ml
index a78f5f13a9..9aeb379737 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -242,4 +242,4 @@ let pop_global_reference = function
| ConstRef con -> ConstRef (pop_con con)
| IndRef (kn,i) -> IndRef (pop_kn kn,i)
| ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
- | VarRef id -> anomaly (Pp.str "VarRef not poppable")
+ | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
diff --git a/library/goptions.ml b/library/goptions.ml
index 9dc0f40588..a305214e82 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -24,7 +24,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
- opt_sync : bool;
opt_depr : bool;
opt_name : string;
opt_value : option_value;
@@ -36,7 +35,7 @@ type option_state = {
let nickname table = String.concat " " table
let error_undeclared_key key =
- errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
+ user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type")
(****************************************************************************)
(* 1- Tables *)
@@ -62,7 +61,6 @@ module MakeTable =
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end) ->
struct
type option_mark =
@@ -73,17 +71,13 @@ module MakeTable =
let _ =
if String.List.mem_assoc nick !A.table then
- error "Sorry, this table name is already used."
+ user_err Pp.(str "Sorry, this table name is already used.")
module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
- let t =
- if A.synchronous
- then Summary.ref MySet.empty ~name:nick
- else ref MySet.empty
+ let t = Summary.ref MySet.empty ~name:nick
let (add_option,remove_option) =
- if A.synchronous then
let cache_options (_,(f,p)) = match f with
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
@@ -103,9 +97,6 @@ module MakeTable =
in
((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
(fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
- else
- ((fun c -> t := MySet.add c !t),
- (fun c -> t := MySet.remove c !t))
let print_table table_name printer table =
Feedback.msg_notice
@@ -141,7 +132,6 @@ sig
val key : option_name
val title : string
val member_message : string -> bool -> std_ppcmds
- val synchronous : bool
end
module StringConvert = functor (A : StringConvertArg) ->
@@ -156,7 +146,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeStringTable =
@@ -176,7 +165,6 @@ sig
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end
module RefConvert = functor (A : RefConvertArg) ->
@@ -191,7 +179,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeRefTable =
@@ -201,7 +188,6 @@ module MakeRefTable =
(* 2- Flags. *)
type 'a option_sig = {
- optsync : bool;
optdepr : bool;
optname : string;
optkey : option_name;
@@ -228,14 +214,13 @@ let get_option key = OptionMap.find key !value_tab
let check_key key = try
let _ = get_option key in
- error "Sorry, this option name is already used."
+ user_err Pp.(str "Sorry, this option name is already used.")
with Not_found ->
if String.List.mem_assoc (nickname key) !string_table
|| String.List.mem_assoc (nickname key) !ref_table
- then error "Sorry, this option name is already used."
+ then user_err Pp.(str "Sorry, this option name is already used.")
open Libobject
-open Lib
let warn_deprecated_option =
CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
@@ -248,11 +233,10 @@ let get_locality = function
| None -> OptDefault
let declare_option cast uncast append ?(preprocess = fun x -> x)
- { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+ { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
- if sync then
let _ = Summary.declare_summary (nickname key)
{ Summary.freeze_function = (fun _ -> read ());
Summary.unfreeze_function = write;
@@ -276,18 +260,12 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
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 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;
+ value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab;
write
type 'a write_function = 'a -> unit
@@ -295,23 +273,23 @@ type 'a write_function = 'a -> unit
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"))
+ (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"))
+ (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"))
+ (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"))
+ (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
(* 3- User accessible commands *)
@@ -326,10 +304,10 @@ 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,append)) ->
+ | 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."
+let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
let check_int_value v = function
| IntValue _ -> IntValue v
@@ -367,7 +345,7 @@ 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)) ->
+ | 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
@@ -382,13 +360,13 @@ let msg_option_value (name,v) =
| BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
- | StringValue s -> str "\"" ++ str s ++ str "\""
+ | StringValue s -> quote (str s)
| StringOptValue None -> str"undefined"
- | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\""
+ | StringOptValue (Some s) -> quote (str s)
(* | 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 ->
@@ -398,9 +376,8 @@ 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, (read,_,_)) accu =
let state = {
- opt_sync = sync;
opt_name = name;
opt_depr = depr;
opt_value = read ();
@@ -417,15 +394,8 @@ let print_tables () =
in
str "Synchronous options:" ++ fnl () ++
OptionMap.fold
- (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 ->
- if sync then p
- else p ++ print_option key name (read ()) depr)
+ (fun key (name, depr, (read,_,_)) p ->
+ p ++ print_option key name (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 3b3651f393..f612c4e369 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -40,8 +40,8 @@
Unset Tata Tutu Titi.
Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)
- The created table/option may be declared synchronous or not
- (synchronous = consistent with the resetting commands) *)
+ All options are synchronized with the document.
+*)
open Pp
open Libnames
@@ -65,7 +65,6 @@ module MakeStringTable :
val key : option_name
val title : string
val member_message : string -> bool -> std_ppcmds
- val synchronous : bool
end) ->
sig
val active : string -> bool
@@ -93,7 +92,6 @@ module MakeRefTable :
val key : option_name
val title : string
val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
end) ->
sig
val active : A.t -> bool
@@ -108,8 +106,6 @@ module MakeRefTable :
used when printing the option value (command "Print Toto Titi." *)
type 'a option_sig = {
- optsync : bool;
- (** whether the option is synchronous w.r.t to the section/module system. *)
optdepr : bool;
(** whether the option is DEPRECATED *)
optname : string;
@@ -120,8 +116,6 @@ type 'a option_sig = {
optwrite : 'a -> unit
}
-(** 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. *)
@@ -177,7 +171,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
- opt_sync : bool;
opt_depr : bool;
opt_name : string;
opt_value : option_value;
diff --git a/library/heads.ml b/library/heads.ml
index 02465f22fc..6aee63c744 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -72,7 +72,8 @@ let kind_of_head env t =
with Not_found ->
CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
- str (Names.Constant.to_string cst)))
+ Names.Constant.print cst ++
+ str "."))
| Construct _ | CoFix _ ->
if b then NotImmediatelyComputableHead else ConstructorHead
| Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/impargs.ml b/library/impargs.ml
index 828d652c83..8f3bfc17e4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -22,6 +22,9 @@ open Constrexpr
open Termops
open Namegen
open Decl_kinds
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(*s Flags governing the computation of implicit arguments *)
@@ -164,7 +167,6 @@ let update pos rig (na,st) =
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env bound depth f =
- let open Context.Named.Declaration in
match kind_of_term f with
| Rel n when n >= bound+depth -> (* inductive type *) false
| Rel n when n >= depth -> (* previous argument *) true
@@ -173,7 +175,7 @@ let is_flexible_reference env bound depth f =
let cb = Environ.lookup_constant kn env in
(match cb.const_body with Def _ -> true | _ -> false)
| Var id ->
- Environ.lookup_named id env |> is_local_def
+ env |> Environ.lookup_named id |> is_local_def
| Ind _ | Construct _ -> false
| _ -> true
@@ -226,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
(* calcule la liste des arguments implicites *)
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+ let b = EConstr.of_constr b in
+ let envnames_b = (env, b) in
let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in flag avoid na b
- else compute_displayed_name_in flag avoid na b
+ if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+ else compute_displayed_name_in Evd.empty flag avoid na b
let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
@@ -287,16 +291,16 @@ let is_status_implicit = function
| _ -> true
let name_of_implicit = function
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
| Some (id,_,_) -> id
let maximal_insertion_of = function
| Some (_,_,(b,_)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
let force_inference_of = function
| Some (_, _, (_, b)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
let is_inferable_implicit in_ctx n = function
@@ -320,7 +324,7 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit")
+ | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
let imps' = prepare_implicits f imps in
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
@@ -338,14 +342,14 @@ let check_correct_manual_implicits autoimps l =
List.iter (function
| ExplByName id,(b,fi,forced) ->
if not forced then
- errorlabstrm ""
+ user_err
(str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
| ExplByPos (i,_id),_t ->
if i<1 || i>List.length autoimps then
- errorlabstrm ""
+ user_err
(str "Bad implicit argument number: " ++ int i ++ str ".")
else
- errorlabstrm ""
+ user_err
(str "Cannot set implicit argument number " ++ int i ++
str ": it has no name.")) l
@@ -360,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l =
with Not_found -> l, None
in
if not (List.distinct l) then
- error ("Some parameters are referred more than once.");
+ user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k l = function
| (Name id,imp)::imps ->
@@ -449,8 +453,7 @@ let compute_all_mib_implicits flags manual kn =
let compute_var_implicits flags manual id =
let env = Global.env () in
- let open Context.Named.Declaration in
- compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
+ compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env))
(* Implicits of a global reference. *)
@@ -517,15 +520,11 @@ let subst_implicits (subst,(req,l)) =
(ImplLocal,List.smartmap (subst_implicits_decl subst) l)
let impls_of_context ctx =
- let map (id, impl, _, _) = match impl with
- | Implicit -> Some (id, Manual, (true, true))
+ let map (decl, impl) = match impl with
+ | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
| _ -> None
in
- let is_set (_, _, b, _) = match b with
- | None -> true
- | Some _ -> false
- in
- List.rev_map map (List.filter is_set ctx)
+ List.rev_map map (List.filter (fst %> is_local_assum) ctx)
let adjust_side_condition p = function
| LessArgsThan n -> LessArgsThan (n+p)
@@ -659,14 +658,14 @@ 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.";
+ user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
aux nl
| _ -> () in
aux (List.map (fun (imps,_) -> List.length imps) l)
let check_rigidity isrigid =
if not isrigid then
- errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
+ user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
let projection_implicits env p impls =
let pb = Environ.lookup_projection p env in
diff --git a/library/keys.ml b/library/keys.ml
index 057dc3b65d..c9e325ee57 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -114,11 +114,11 @@ let inKeys : key_obj -> obj =
let declare_equiv_keys ref ref' =
Lib.add_anonymous_leaf (inKeys (ref,ref'))
-let constr_key c =
+let constr_key kind c =
let open Globnames in
try
let rec aux k =
- match kind_of_term k with
+ match kind k with
| Const (c, _) -> KGlob (ConstRef c)
| Ind (i, u) -> KGlob (IndRef i)
| Construct (c,u) -> KGlob (ConstructRef c)
diff --git a/library/keys.mli b/library/keys.mli
index 69668590d6..6abac4de44 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -16,7 +16,7 @@ val declare_equiv_keys : key -> key -> unit
val equiv_keys : key -> key -> bool
(** Check equivalence of keys. *)
-val constr_key : Term.constr -> key option
+val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
(** Compute the head key of a term. *)
val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
diff --git a/library/kindops.ml b/library/kindops.ml
index 21b1bec33c..623d2537aa 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 () = CErrors.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) ->
- CErrors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/lib.ml b/library/lib.ml
index f680ecee3c..9d71a854f0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,6 +13,9 @@ open Libnames
open Globnames
open Nameops
open Libobject
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
type is_type = bool (* Module Type or just Module *)
type export = bool option (* None for a Module Type *)
@@ -73,9 +76,9 @@ let classify_segment seg =
(* LEM; TODO: Understand what this does and see if what I do is the
correct thing for ClosedMod(ule|type) *)
| (_,ClosedModule _) :: stk -> clean acc stk
- | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+ | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
| (_,OpenedModule (ty,_,_,_)) :: _ ->
- errorlabstrm "Lib.classify_segment"
+ user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
| (_,FrozenState _) :: stk -> clean acc stk
in
@@ -94,21 +97,30 @@ let segment_of_objects prefix =
let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
-let lib_stk = ref ([] : library_segment)
+type lib_state = {
+ comp_name : Names.DirPath.t option;
+ lib_stk : library_segment;
+ path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+}
+
+let initial_lib_state = {
+ comp_name = None;
+ lib_stk = [];
+ path_prefix = initial_prefix;
+}
-let comp_name = ref None
+let lib_state = ref initial_lib_state
let library_dp () =
- match !comp_name with Some m -> m | None -> default_library
+ match !lib_state.comp_name with Some m -> m | None -> default_library
(* [path_prefix] is a pair of absolute dirpath and a pair of current
module path and relative section path *)
-let path_prefix = ref initial_prefix
-let cwd () = fst !path_prefix
-let current_prefix () = snd !path_prefix
-let current_mp () = fst (snd !path_prefix)
-let current_sections () = snd (snd !path_prefix)
+let cwd () = fst !lib_state.path_prefix
+let current_prefix () = snd !lib_state.path_prefix
+let current_mp () = fst (snd !lib_state.path_prefix)
+let current_sections () = snd (snd !lib_state.path_prefix)
let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -129,7 +141,7 @@ let make_kn id =
let mp,dir = current_prefix () in
Names.make_kn mp dir (Names.Label.of_id id)
-let make_oname id = Libnames.make_oname !path_prefix id
+let make_oname id = Libnames.make_oname !lib_state.path_prefix id
let recalc_path_prefix () =
let rec recalc = function
@@ -139,18 +151,18 @@ let recalc_path_prefix () =
| _::l -> recalc l
| [] -> initial_prefix
in
- path_prefix := recalc !lib_stk
+ lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
let pop_path_prefix () =
- let dir,(mp,sec) = !path_prefix in
- path_prefix := pop_dirpath dir, (mp, pop_dirpath sec)
+ let dir,(mp,sec) = !lib_state.path_prefix in
+ lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
let find_entry_p p =
let rec find = function
| [] -> raise Not_found
| ent::l -> if p ent then ent else find l
in
- find !lib_stk
+ find !lib_state.lib_stk
let split_lib_gen test =
let rec collect after equal = function
@@ -171,8 +183,8 @@ let split_lib_gen test =
| _ -> findeq (hd::after) before)
| [] -> None
in
- match findeq [] !lib_stk with
- | None -> error "no such entry"
+ match findeq [] !lib_state.lib_stk with
+ | None -> user_err Pp.(str "no such entry")
| Some r -> r
let eq_object_name (fp1, kn1) (fp2, kn2) =
@@ -196,10 +208,10 @@ let split_lib_at_opening sp =
(* Adding operations. *)
let add_entry sp node =
- lib_stk := (sp,node) :: !lib_stk
+ lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
let pull_to_head oname =
- lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+ lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
let anonymous_id =
let n = ref 0 in
@@ -210,7 +222,7 @@ let add_anonymous_entry node =
let add_leaf id obj =
if Names.ModPath.equal (current_mp ()) Names.initial_path then
- error ("No session module started (use -top dir)");
+ user_err Pp.(str "No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
add_entry oname (Leaf obj);
@@ -260,8 +272,8 @@ let current_mod_id () =
try match find_entry_p is_opening_node_or_lib with
| oname,OpenedModule (_,_,_,fs) -> basename (fst oname)
| oname,CompilingLibrary _ -> basename (fst oname)
- | _ -> error "you are not in a module"
- with Not_found -> error "no opened modules"
+ | _ -> user_err Pp.(str "you are not in a module")
+ with Not_found -> user_err Pp.(str "no opened modules")
let start_mod is_type export id mp fs =
@@ -272,9 +284,9 @@ let start_mod is_type export id mp fs =
else Nametab.exists_module dir
in
if exists then
- errorlabstrm "open_module" (pr_id id ++ str " already exists");
+ user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix} ;
prefix
let start_module = start_mod false
@@ -282,7 +294,7 @@ let start_modtype = start_mod true None
let error_still_opened string oname =
let id = basename (fst oname) in
- errorlabstrm ""
+ user_err
(str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
let end_mod is_type =
@@ -293,19 +305,19 @@ let end_mod is_type =
else error_still_opened (module_kind ty) oname
| oname,OpenedSection _ -> error_still_opened "section" oname
| _ -> assert false
- with Not_found -> error "No opened modules."
+ with Not_found -> user_err (Pp.str "No opened modules.")
in
let (after,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
+ lib_state := { !lib_state with lib_stk = before };
add_entry oname (ClosedModule (List.rev (mark::after)));
- let prefix = !path_prefix in
+ let prefix = !lib_state.path_prefix in
recalc_path_prefix ();
(oname, prefix, fs, after)
let end_module () = end_mod false
let end_modtype () = end_mod true
-let contents () = !lib_stk
+let contents () = !lib_state.lib_stk
let contents_after sp = let (after,_,_) = split_lib sp in after
@@ -313,21 +325,21 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
(* TODO: use check_for_module ? *)
let start_compilation s mp =
- if !comp_name != None then
- error "compilation unit is already started";
+ if !lib_state.comp_name != None then
+ user_err Pp.(str "compilation unit is already started");
if not (Names.DirPath.is_empty (current_sections ())) then
- error "some sections are already opened";
+ user_err Pp.(str "some sections are already opened");
let prefix = s, (mp, Names.DirPath.empty) in
let () = add_anonymous_entry (CompilingLibrary prefix) in
- comp_name := Some s;
- path_prefix := prefix
+ lib_state := { !lib_state with comp_name = Some s;
+ path_prefix = prefix }
let end_compilation_checks dir =
let _ =
try match snd (find_entry_p is_opening_node) with
- | OpenedSection _ -> error "There are some open sections."
+ | OpenedSection _ -> user_err Pp.(str "There are some open sections.")
| OpenedModule (ty,_,_,_) ->
- errorlabstrm "Lib.end_compilation_checks"
+ user_err ~hdr:"Lib.end_compilation_checks"
(str "There are some open " ++ str (module_kind ty) ++ str "s.")
| _ -> assert false
with Not_found -> ()
@@ -338,22 +350,22 @@ let end_compilation_checks dir =
try match find_entry_p is_opening_lib with
| (oname, CompilingLibrary prefix) -> oname
| _ -> assert false
- with Not_found -> anomaly (Pp.str "No module declared")
+ with Not_found -> anomaly (Pp.str "No module declared.")
in
let _ =
- match !comp_name with
+ match !lib_state.comp_name with
| None -> anomaly (Pp.str "There should be a module name...")
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
(str "The current open module has name" ++ spc () ++ pr_dirpath m ++
- spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
+ spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
in
oname
let end_compilation oname =
let (after,mark,before) = split_lib_at_opening oname in
- comp_name := None;
- !path_prefix,after
+ lib_state := { !lib_state with comp_name = None };
+ !lib_state.path_prefix,after
(* Returns true if we are inside an opened module or module type *)
@@ -379,10 +391,10 @@ let find_opening_node id =
let oname,entry = find_entry_p is_opening_node in
let id' = basename (fst oname) in
if not (Names.Id.equal id id') then
- errorlabstrm "Lib.find_opening_node"
+ user_err ~hdr:"Lib.find_opening_node"
(str "Last block to end has name " ++ pr_id id' ++ str ".");
entry
- with Not_found -> error "There is nothing to end."
+ with Not_found -> user_err Pp.(str "There is nothing to end.")
(* Discharge tables *)
@@ -393,7 +405,7 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -416,7 +428,7 @@ let add_section () =
let check_same_poly p vars =
let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
if List.exists pred vars then
- error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+ user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
let add_section_variable id impl poly ctx =
match !sectab with
@@ -433,12 +445,10 @@ let add_section_context ctx =
sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
- let open Context.Named.Declaration in
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
- let (id',b,t) = to_tuple decl in
+ | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
+ (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
| (Variable (_,_,poly,ctx)::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, if poly then Univ.ContextSet.union r ctx else r
@@ -448,17 +458,11 @@ let extract_hyps (secs,ohyps) =
| [], _ -> [],Univ.ContextSet.empty
in aux (secs,ohyps)
-let instance_from_variable_context sign =
- let rec inst_rec = function
- | (id,b,None,_) :: sign -> id :: inst_rec sign
- | _ :: sign -> inst_rec sign
- | [] -> [] in
- Array.of_list (inst_rec sign)
-
-let named_of_variable_context ctx = let open Context.Named.Declaration in
- List.map (function id,_,None,t -> LocalAssum (id,t)
- | id,_,Some b,t -> LocalDef (id,b,t))
- ctx
+let instance_from_variable_context =
+ List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let named_of_variable_context =
+ List.map fst
let add_section_replacement f g poly hyps =
match !sectab with
@@ -519,16 +523,16 @@ let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
let open_section id =
- let olddir,(mp,oldsec) = !path_prefix in
+ let olddir,(mp,oldsec) = !lib_state.path_prefix in
let dir = add_dirpath_suffix olddir id in
let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
if Nametab.exists_section dir then
- errorlabstrm "open_section" (pr_id id ++ str " already exists.");
+ user_err ~hdr:"open_section" (pr_id id ++ str " already exists.");
let fs = Summary.freeze_summaries ~marshallable:`No in
add_entry (make_oname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix };
if !Flags.xml_export then Hook.get f_xml_open_section id;
add_section ()
@@ -543,7 +547,7 @@ let discharge_item ((sp,_ as oname),e) =
| FrozenState _ -> None
| ClosedSection _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
- anomaly (Pp.str "discharge_item")
+ anomaly (Pp.str "discharge_item.")
let close_section () =
let oname,fs =
@@ -551,11 +555,11 @@ let close_section () =
| oname,OpenedSection (_,fs) -> oname,fs
| _ -> assert false
with Not_found ->
- error "No opened section."
+ user_err Pp.(str "No opened section.")
in
let (secdecls,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
- let full_olddir = fst !path_prefix in
+ lib_state := { !lib_state with lib_stk = before };
+ let full_olddir = fst !lib_state.path_prefix in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
@@ -566,7 +570,7 @@ let close_section () =
(* State and initialization. *)
-type frozen = Names.DirPath.t option * library_segment
+type frozen = lib_state
let freeze ~marshallable =
match marshallable with
@@ -583,18 +587,15 @@ let freeze ~marshallable =
Some(n,OpenedSection(op,Summary.empty_frozen))
| n, ClosedSection _ -> Some (n,ClosedSection [])
| _, FrozenState _ -> None)
- !lib_stk in
- !comp_name, lib_stk
+ !lib_state.lib_stk in
+ { !lib_state with lib_stk }
| _ ->
- !comp_name, !lib_stk
+ !lib_state
-let unfreeze (mn,stk) =
- comp_name := mn;
- lib_stk := stk;
- recalc_path_prefix ()
+let unfreeze st = lib_state := st
let init () =
- unfreeze (None,[]);
+ unfreeze initial_lib_state;
Summary.init_summaries ();
add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
diff --git a/library/lib.mli b/library/lib.mli
index a8e110c67a..9f9d8c7e5f 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -160,8 +160,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t
val xml_close_section : (Names.Id.t -> unit) Hook.t
(** {6 Section management for discharge } *)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind *
- Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
diff --git a/library/libnames.ml b/library/libnames.ml
index dd74e192ff..50f28b0205 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
+ if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path.");
if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
- if Int.equal pos n then error (s ^ " is an invalid path.");
+ if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
in
diff --git a/library/libnames.mli b/library/libnames.mli
index 58d1da9d64..57013ef82e 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -125,7 +125,7 @@ val eq_reference : reference -> reference -> bool
val qualid_of_reference : reference -> qualid located
val string_of_reference : reference -> string
val pr_reference : reference -> std_ppcmds
-val loc_of_reference : reference -> Loc.t
+val loc_of_reference : reference -> Loc.t option
val join_reference : reference -> reference -> reference
(** Deprecated synonyms *)
diff --git a/library/libobject.ml b/library/libobject.ml
index caa03c85be..897591762c 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,7 +8,6 @@
open Libnames
open Pp
-open Util
module Dyn = Dyn.Make(struct end)
@@ -91,16 +90,8 @@ let declare_object_full odecl =
dyn_rebuild_function = rebuild };
(infun,outfun)
-(* The "try .. with .. " allows for correct printing when calling
- declare_object a loading time.
-*)
-
-let declare_object odecl =
- try fst (declare_object_full odecl)
- with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
-let declare_object_full odecl =
- try declare_object_full odecl
- with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
+let declare_object odecl = fst (declare_object_full odecl)
+let declare_object_full odecl = declare_object_full odecl
(* this function describes how the cache, load, open, and export functions
are triggered. *)
diff --git a/library/library.ml b/library/library.ml
index d44f796a7a..5a5f99cc51 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -131,7 +131,7 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- errorlabstrm "Library.find_library"
+ user_err ~hdr:"Library.find_library"
(str "Unknown library " ++ pr_dirpath dir)
let register_library_filename dir f =
@@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid =
let error_unmapped_dir qid =
let prefix, _ = repr_qualid qid in
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
let error_lib_not_found qid =
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
let try_locate_absolute_library dir =
@@ -378,7 +378,7 @@ let access_table what tables dp i =
let t =
try fetch_delayed f
with Faulty f ->
- errorlabstrm "Library.access_table"
+ user_err ~hdr:"Library.access_table"
(str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
str ") is inaccessible or corrupted,\ncannot load some " ++
str what ++ str " in it.\n")
@@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
- errorlabstrm "load_physical_library"
+ user_err ~hdr:"load_physical_library"
(str "The file " ++ str f ++ str " contains library" ++ spc () ++
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
@@ -477,7 +477,7 @@ and intern_library_deps libs dir m from =
and intern_mandatory_library caller from libs (dir,d) =
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 ++
+ user_err (str "Compiled library " ++ pr_dirpath caller ++
str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
over library " ++ pr_dirpath dir);
libs
@@ -582,8 +582,8 @@ let require_library_from_dirpath modrefl export =
let safe_locate_module (loc,qid) =
try Nametab.locate_module qid
with Not_found ->
- user_err_loc
- (loc,"import_library", pr_qualid qid ++ str " is not a module")
+ user_err ?loc ~hdr:"import_library"
+ (pr_qualid qid ++ str " is not a module")
let import_module export modl =
(* Optimization: libraries in a raw in the list are imported
@@ -597,7 +597,7 @@ let import_module export modl =
| [] -> ()
| modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
let rec aux acc = function
- | (loc,dir as m) :: l ->
+ | (loc, dir as m) :: l ->
let m,acc =
try Nametab.locate_module dir, acc
with Not_found-> flush acc; safe_locate_module m, [] in
@@ -607,8 +607,8 @@ let import_module export modl =
flush acc;
try Declaremods.import_module export mp; aux [] l
with Not_found ->
- user_err_loc (loc,"import_library",
- pr_qualid dir ++ str " is not a module"))
+ user_err ?loc ~hdr:"import_library"
+ (pr_qualid dir ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
@@ -619,7 +619,7 @@ let check_coq_overwriting p id =
let l = DirPath.repr p in
let is_empty = match l with [] -> true | _ -> false in
if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
- errorlabstrm ""
+ user_err
(str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
@@ -632,7 +632,7 @@ let check_module_name s =
(if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
strbrk " is not allowed in module names\n"
in
- let err c = errorlabstrm "" (msg c) in
+ let err c = user_err (msg c) in
match String.get s 0 with
| 'a' .. 'z' | 'A' .. 'Z' ->
for i = 1 to (String.length s)-1 do
@@ -668,10 +668,10 @@ let load_library_todo f =
let tasks, _, _ = System.marshal_in_segment f ch in
let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
close_in ch;
- if tasks = None then errorlabstrm "restart" (str"not a .vio file");
- if s2 = None then errorlabstrm "restart" (str"not a .vio file");
- if s3 = None then errorlabstrm "restart" (str"not a .vio file");
- if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
+ if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
(************************************************************************)
@@ -687,7 +687,7 @@ let current_deps () =
let current_reexports () = !libraries_exports_list
let error_recursively_dependent_library dir =
- errorlabstrm ""
+ user_err
(strbrk "Unable to use logical name " ++ pr_dirpath dir ++
strbrk " to save current library because" ++
strbrk " it already depends on a library of this name.")
@@ -734,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 CErrors.errorlabstrm "library"
+ if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
opaque_table;
let sd = {
@@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab =
if !Flags.native_compiler then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
- error "Could not compile the library to native code."
+ user_err Pp.(str "Could not compile the library to native code.")
with reraise ->
let reraise = CErrors.push reraise in
let () = Feedback.msg_warning (str "Removed file " ++ str f') in
diff --git a/library/library.mllib b/library/library.mllib
index 9206573658..6f433b77d1 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -5,7 +5,6 @@ Libobject
Summary
Nametab
Global
-Universes
Lib
Declaremods
Loadpath
@@ -17,3 +16,4 @@ Goptions
Decls
Heads
Keys
+Coqlib
diff --git a/library/loadpath.ml b/library/loadpath.ml
index d03c6c5553..ad429ea840 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -29,7 +29,7 @@ let physical p = p.path_physical
let get_load_paths () = !load_paths
let anomaly_too_many_paths path =
- anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
+ anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
let find_load_path phys_dir =
let phys_dir = CUnix.canonical_path_name phys_dir in
@@ -113,5 +113,5 @@ let expand_path ?root dir =
let locate_file fname =
let paths = List.map physical !load_paths in
let _,longfname =
- System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+ System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in
longfname
diff --git a/library/nameops.ml b/library/nameops.ml
index 71405d0240..0b5dfd8d0e 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Util
open Names
@@ -14,10 +13,6 @@ open Names
let pr_id id = Id.print id
-let pr_name = function
- | Anonymous -> str "_"
- | Name id -> pr_id id
-
(* Utilities *)
let code_of_0 = Char.code '0'
@@ -61,15 +56,27 @@ let make_ident sa = function
if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
else sa ^ "_" ^ (string_of_int n) in
Id.of_string s
- | None -> Id.of_string (String.copy sa)
+ | None -> Id.of_string sa
let root_of_id id =
let suffixstart = cut_ident true id in
Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
-(* Rem: semantics is a bit different, if an ident starts with toto00 then
- after successive renamings it comes to toto09, then it goes on with toto10 *)
-let lift_subscript id =
+(* Return the same identifier as the original one but whose {i subscript} is incremented.
+ If the original identifier does not have a suffix, [0] is appended to it.
+
+ Example mappings:
+
+ [bar] ↦ [bar0]
+ [bar0] ↦ [bar1]
+ [bar00] ↦ [bar01]
+ [bar1] ↦ [bar2]
+ [bar01] ↦ [bar01]
+ [bar9] ↦ [bar10]
+ [bar09] ↦ [bar10]
+ [bar99] ↦ [bar100]
+*)
+let increment_subscript id =
let id = Id.to_string id in
let len = String.length id in
let rec add carrypos =
@@ -80,20 +87,20 @@ let lift_subscript id =
add (carrypos-1)
end
else begin
- let newid = String.copy id in
- String.fill newid (carrypos+1) (len-1-carrypos) '0';
- newid.[carrypos] <- Char.chr (Char.code c + 1);
+ let newid = Bytes.of_string id in
+ Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+ Bytes.set newid carrypos (Char.chr (Char.code c + 1));
newid
end
else begin
- let newid = id^"0" in
+ let newid = Bytes.of_string (id^"0") in
if carrypos < len-1 then begin
- String.fill newid (carrypos+1) (len-1-carrypos) '0';
- newid.[carrypos+1] <- '1'
+ Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+ Bytes.set newid (carrypos+1) '1'
end;
newid
end
- in Id.of_string (add (len-1))
+ in Id.of_bytes (add (len-1))
let has_subscript id =
let id = Id.to_string id in
@@ -101,9 +108,9 @@ let has_subscript id =
let forget_subscript id =
let numstart = cut_ident false id in
- let newid = String.make (numstart+1) '0' in
+ let newid = Bytes.make (numstart+1) '0' in
String.blit (Id.to_string id) 0 newid 0 numstart;
- (Id.of_string newid)
+ (Id.of_bytes newid)
let add_suffix id s = Id.of_string (Id.to_string id ^ s)
let add_prefix s id = Id.of_string (s ^ Id.to_string id)
@@ -112,34 +119,82 @@ let atompart_of_id id = fst (repr_ident id)
(* Names *)
-let out_name = function
- | Name id -> id
- | Anonymous -> failwith "Nameops.out_name"
+module type ExtName =
+sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
+ val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
+ val iter : (Id.t -> unit) -> t -> unit
+ val map : (Id.t -> Id.t) -> t -> t
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+ val get_id : t -> Id.t
+ val pick : t -> t -> t
+ val cons : t -> Id.t list -> Id.t list
+ val to_option : Name.t -> Id.t option
+
+end
+
+module Name : ExtName =
+struct
+
+ include Names.Name
+
+ exception IsAnonymous
+
+ let fold_left f a = function
+ | Name id -> f a id
+ | Anonymous -> a
+
+ let fold_right f na a =
+ match na with
+ | Name id -> f id a
+ | Anonymous -> a
+
+ let iter f na = fold_right (fun x () -> f x) na ()
+
+ let map f = function
+ | Name id -> Name (f id)
+ | Anonymous -> Anonymous
+
+ let fold_map f a = function
+ | Name id -> let (a, id) = f a id in (a, Name id)
+ | Anonymous -> a, Anonymous
+
+ let get_id = function
+ | Name id -> id
+ | Anonymous -> raise IsAnonymous
-let name_fold f na a =
- match na with
- | Name id -> f id a
- | Anonymous -> a
+ let pick na1 na2 =
+ match na1 with
+ | Name _ -> na1
+ | Anonymous -> na2
-let name_iter f na = name_fold (fun x () -> f x) na ()
+ let cons na l =
+ match na with
+ | Anonymous -> l
+ | Name id -> id::l
-let name_cons na l =
- match na with
- | Anonymous -> l
- | Name id -> id::l
+ let to_option = function
+ | Anonymous -> None
+ | Name id -> Some id
-let name_app f = function
- | Name id -> Name (f id)
- | Anonymous -> Anonymous
+end
-let name_fold_map f e = function
- | Name id -> let (e,id) = f e id in (e,Name id)
- | Anonymous -> e,Anonymous
+open Name
-let name_max na1 na2 =
- match na1 with
- | Name _ -> na1
- | Anonymous -> na2
+(* Compatibility *)
+let out_name = get_id
+let name_fold = fold_right
+let name_iter = iter
+let name_app = map
+let name_fold_map = fold_map
+let name_cons = cons
+let name_max = pick
+let pr_name = print
let pr_lab l = Label.print l
diff --git a/library/nameops.mli b/library/nameops.mli
index 39ce409bcf..abfc09db8d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,8 +9,6 @@
open Names
(** Identifiers and names *)
-val pr_id : Id.t -> Pp.std_ppcmds
-val pr_name : Name.t -> Pp.std_ppcmds
val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
@@ -21,20 +19,98 @@ val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
val add_suffix : Id.t -> string -> Id.t
val add_prefix : string -> Id.t -> Id.t
-val has_subscript : Id.t -> bool
-val lift_subscript : Id.t -> Id.t
-val forget_subscript : Id.t -> Id.t
+(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)
+
+val has_subscript : Id.t -> bool
+
+val increment_subscript : Id.t -> Id.t
+(** Return the same identifier as the original one but whose {i subscript} is incremented.
+ If the original identifier does not have a suffix, [0] is appended to it.
+
+ Example mappings:
+
+ [bar] ↦ [bar0]
+
+ [bar0] ↦ [bar1]
+
+ [bar00] ↦ [bar01]
+
+ [bar1] ↦ [bar2]
+
+ [bar01] ↦ [bar01]
+
+ [bar9] ↦ [bar10]
+
+ [bar09] ↦ [bar10]
+
+ [bar99] ↦ [bar100]
+*)
+
+val forget_subscript : Id.t -> Id.t
+
+module Name : sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
+ (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)
+
+ val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+ (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)
+
+ val iter : (Id.t -> unit) -> Name.t -> unit
+ (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)
+
+ val map : (Id.t -> Id.t) -> Name.t -> t
+ (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
+
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+ (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
+ It is [a,Anonymous] otherwise. *)
+
+ val get_id : Name.t -> Id.t
+ (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
+
+ val pick : Name.t -> Name.t -> Name.t
+ (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
+ Pick one of [na] or [na'] otherwise. *)
+
+ val cons : Name.t -> Id.t list -> Id.t list
+ (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
+
+ val to_option : Name.t -> Id.t option
+ (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)
+
+end
val out_name : Name.t -> Id.t
-(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
- otherwise. *)
+(** @deprecated Same as [Name.get_id] *)
val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+(** @deprecated Same as [Name.fold_right] *)
+
val name_iter : (Id.t -> unit) -> Name.t -> unit
-val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.iter] *)
+
val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
+(** @deprecated Same as [Name.map] *)
+
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+(** @deprecated Same as [Name.fold_map] *)
+
val name_max : Name.t -> Name.t -> Name.t
+(** @deprecated Same as [Name.pick] *)
+
+val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.cons] *)
+
+val pr_name : Name.t -> Pp.std_ppcmds
+(** @deprecated Same as [Name.print] *)
+
+val pr_id : Id.t -> Pp.std_ppcmds
+(** @deprecated Same as [Names.Id.print] *)
val pr_lab : Label.t -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index fa5db37ed5..93e9c03cee 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -16,10 +16,8 @@ open Globnames
exception GlobalizationError of qualid
-let error_global_not_found_loc loc q =
- Loc.raise loc (GlobalizationError q)
-
-let error_global_not_found q = raise (GlobalizationError q)
+let error_global_not_found ?loc q =
+ Loc.raise ?loc (GlobalizationError q)
(* Kinds of global names *)
@@ -145,8 +143,8 @@ struct
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
- error ("Cannot mask the absolute name \""
- ^ U.to_string uname' ^ "\"!")
+ user_err Pp.(str @@ "Cannot mask the absolute name \""
+ ^ U.to_string uname' ^ "\"!")
| Nothing
| Relative _ -> mktree (Absolute (uname,o)) tree.map
@@ -296,7 +294,7 @@ module DirPath' =
struct
include DirPath
let repr dir = match DirPath.repr dir with
- | [] -> anomaly (Pp.str "Empty dirpath")
+ | [] -> anomaly (Pp.str "Empty dirpath.")
| id :: l -> (id, l)
end
@@ -455,11 +453,11 @@ let global r =
try match locate_extended qid with
| TrueGlobal ref -> ref
| SynDef _ ->
- user_err_loc (loc,"global",
- str "Unexpected reference to a notation: " ++
- pr_qualid qid)
+ user_err ?loc ~hdr:"global"
+ (str "Unexpected reference to a notation: " ++
+ pr_qualid qid)
with Not_found ->
- error_global_not_found_loc loc qid
+ error_global_not_found ?loc qid
(* Exists functions ********************************************************)
@@ -534,8 +532,8 @@ let global_inductive r =
match global r with
| IndRef ind -> ind
| ref ->
- user_err_loc (loc_of_reference r,"global_inductive",
- pr_reference r ++ spc () ++ str "is not an inductive type")
+ user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive"
+ (pr_reference r ++ spc () ++ str "is not an inductive type")
(********************************************************************)
diff --git a/library/nametab.mli b/library/nametab.mli
index a8a0572b33..095ac4f9df 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -60,8 +60,7 @@ open Globnames
exception GlobalizationError of qualid
(** Raises a globalization error *)
-val error_global_not_found_loc : Loc.t -> qualid -> 'a
-val error_global_not_found : qualid -> 'a
+val error_global_not_found : ?loc:Loc.t -> qualid -> 'a
(** {6 Register visibility of things } *)
@@ -174,3 +173,38 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
val absolute_reference : full_path -> global_reference (** = global_of_path *)
+
+(** {5 Generic name handling} *)
+
+(** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
+
+module type UserName = sig
+ type t
+ val equal : t -> t -> bool
+ val to_string : t -> string
+ val repr : t -> Id.t * module_ident list
+end
+
+module type EqualityType =
+sig
+ type t
+ val equal : t -> t -> bool
+end
+
+module type NAMETREE = sig
+ type elt
+ type t
+ type user_name
+
+ val empty : t
+ val push : visibility -> user_name -> elt -> t -> t
+ val locate : qualid -> t -> elt
+ val find : user_name -> t -> elt
+ val exists : user_name -> t -> bool
+ val user_name : qualid -> t -> user_name
+ val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+ val find_prefixes : qualid -> t -> elt list
+end
+
+module Make (U : UserName) (E : EqualityType) :
+ NAMETREE with type user_name = U.t and type elt = E.t
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f388..c7bf95fd41 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -46,7 +46,7 @@ let declare_summary sumname decl =
let () = if Int.Map.mem hash !summaries then
let (name, _) = Int.Map.find hash !summaries in
anomaly ~label:"Summary.declare_summary"
- (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name)
+ (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
in
all_declared_summaries := Int.Set.add hash !all_declared_summaries;
summary_names := (hash, sumname) :: !summary_names;
@@ -85,10 +85,10 @@ let unfreeze_summaries fs =
* may modify the content of [summaries] ny loading new ML modules *)
let (_, decl) =
try Int.Map.find ml_modules_summary !summaries
- with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
in
let () = match fs.ml_module with
- | None -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
| Some state -> decl.unfreeze_function state
in
let fold id (_, decl) states =
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
try fold id decl state
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 (CErrors.iprint e));
+ Feedback.msg_error
+ Pp.(seq [str "Error unfreezing summary %s\n%s\n%!";
+ str (name_of_summary id);
+ CErrors.iprint e]);
iraise e
in
(** We rely on the order of the frozen list, and the order of folding *)
diff --git a/library/universes.ml b/library/universes.ml
deleted file mode 100644
index 112b20a4c4..0000000000
--- a/library/universes.ml
+++ /dev/null
@@ -1,1162 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Pp
-open Names
-open Term
-open Environ
-open Univ
-open Globnames
-open Decl_kinds
-
-(** Global universe names *)
-type universe_names =
- (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
-
-let global_universes =
- Summary.ref ~name:"Global universe names"
- ((Idmap.empty, Univ.LMap.empty) : universe_names)
-
-let global_universe_names () = !global_universes
-let set_global_universe_names s = global_universes := s
-
-let pr_with_global_universes l =
- try Nameops.pr_id (LMap.find l (snd !global_universes))
- with Not_found -> Level.pr l
-
-(** Local universe names of polymorphic references *)
-
-type universe_binders = (Id.t * Univ.universe_level) list
-
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-
-let universe_binders_of_global ref =
- try
- let l = Refmap.find ref !universe_binders_table in l
- with Not_found -> []
-
-let register_universe_binders ref l =
- universe_binders_table := Refmap.add ref l !universe_binders_table
-
-(* To disallow minimization to Set *)
-
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = universe * universe_constraint_type * universe
-
-module Constraints = struct
- module S = Set.Make(
- struct
- type t = universe_constraint
-
- let compare_type c c' =
- match c, c' with
- | ULe, ULe -> 0
- | ULe, _ -> -1
- | _, ULe -> 1
- | UEq, UEq -> 0
- | UEq, _ -> -1
- | ULub, ULub -> 0
- | ULub, _ -> 1
-
- let compare (u,c,v) (u',c',v') =
- let i = compare_type c c' in
- if Int.equal i 0 then
- let i' = Universe.compare u u' in
- if Int.equal i' 0 then Universe.compare v v'
- else
- if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0
- else i'
- else i
- end)
-
- include S
-
- let add (l,d,r as cst) s =
- if Universe.equal l r then s
- else add cst s
-
- let tr_dir = function
- | ULe -> Le
- | UEq -> Eq
- | ULub -> Eq
-
- let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ "
-
- let pr c =
- fold (fun (u1,op,u2) pp_std ->
- pp_std ++ Universe.pr u1 ++ str (op_str op) ++
- Universe.pr u2 ++ fnl ()) c (str "")
-
- let equal x y =
- x == y || equal x y
-
-end
-
-type universe_constraints = Constraints.t
-type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
-type 'a universe_constrained = 'a * universe_constraints
-
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-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
- 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))
- ax ay c
-
-let subst_univs_universe_constraint fn (u,d,v) =
- let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
- if Universe.equal u' v' then None
- else Some (u',d,v')
-
-let subst_univs_universe_constraints subst csts =
- Constraints.fold
- (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c))
- csts Constraints.empty
-
-
-let to_constraints g s =
- let tr (x,d,y) acc =
- let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in
- match Universe.level x, d, Universe.level y with
- | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc
- | _, ULe, Some l' -> enforce_leq x y acc
- | _, ULub, _ -> acc
- | _, d, _ ->
- let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
- if f g x y then acc else
- raise (Invalid_argument
- "to_constraints: non-trivial algebraic constraint between universes")
- in Constraints.fold tr s Constraint.empty
-
-let eq_constr_univs_infer univs fold m n accu =
- if m == n then Some accu
- else
- let cstrs = ref accu in
- let eq_universes strict = UGraph.check_eq_instances univs in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
- if res then Some !cstrs else None
-
-(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
- to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
- (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
- haven't find a way to factor the code without destroying
- pointer-equality optimisations in [eq_constr_univs_infer].
- Pointer equality is not sufficient to ensure equality up to
- [kind1,kind2], because [kind1] and [kind2] may be different,
- typically evaluating [m] and [n] in different evar maps. *)
- let cstrs = ref accu in
- let eq_universes strict = UGraph.check_eq_instances univs in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let rec eq_constr' m n =
- Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
- in
- let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
- if res then Some !cstrs else None
-
-let leq_constr_univs_infer univs fold m n accu =
- if m == n then Some accu
- else
- let cstrs = ref accu in
- let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let leq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
- | None -> false
- | Some accu -> cstrs := accu; true
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts
- eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- let res = compare_leq m n in
- if res then Some !cstrs else None
-
-let eq_constr_universes m n =
- if m == n then true, Constraints.empty
- else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' =
- cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- (cstrs := Constraints.add
- (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
-
-let leq_constr_universes m n =
- if m == n then true, Constraints.empty
- else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' =
- cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let leq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let rec eq_constr' m n =
- m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- let res = compare_leq m n in
- res, !cstrs
-
-let compare_head_gen_proj env equ eqs eqc' m n =
- match kind_of_term m, kind_of_term n with
- | Proj (p, c), App (f, args)
- | App (f, args), Proj (p, c) ->
- (match kind_of_term f with
- | Const (p', u) when eq_constant (Projection.constant p) p' ->
- let pb = Environ.lookup_projection p env in
- let npars = pb.Declarations.proj_npars in
- if Array.length args == npars + 1 then
- eqc' c args.(npars)
- else false
- | _ -> false)
- | _ -> Constr.compare_head_gen equ eqs eqc' m n
-
-let eq_constr_universes_proj env m n =
- if m == n then true, Constraints.empty
- else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' =
- cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- (cstrs := Constraints.add
- (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let rec eq_constr' m n =
- m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
- in
- let res = eq_constr' m n in
- res, !cstrs
-
-(* Generator of levels *)
-let new_univ_level, set_remote_new_univ_level =
- RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
- ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n)
-
-let new_univ_level _ = new_univ_level ()
- (* Univ.Level.make db (new_univ_level ()) *)
-
-let fresh_level () = new_univ_level (Global.current_dirpath ())
-
-(* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
-
-let fresh_universe_instance ctx =
- Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ()))
- (UContext.instance ctx)
-
-let fresh_instance_from_context ctx =
- let inst = fresh_universe_instance ctx in
- let constraints = instantiate_univ_constraints inst ctx in
- inst, constraints
-
-let fresh_instance ctx =
- let ctx' = ref LSet.empty in
- let inst =
- Instance.subst_fn (fun v ->
- let u = new_univ_level (Global.current_dirpath ()) in
- ctx' := LSet.add u !ctx'; u)
- (UContext.instance ctx)
- in !ctx', inst
-
-let existing_instance ctx inst =
- let () =
- let a1 = Instance.to_array 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
- CErrors.errorlabstrm "Universes"
- (str "Polymorphic constant expected " ++ int len2 ++
- str" levels but was given " ++ int len1)
- else ()
- in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
- let ctx', inst =
- match inst with
- | Some inst -> existing_instance ctx inst
- | None -> fresh_instance ctx
- in
- let constraints = instantiate_univ_constraints inst ctx in
- inst, (ctx', constraints)
-
-let unsafe_instance_from ctx =
- (Univ.UContext.instance ctx, ctx)
-
-(** Fresh universe polymorphic construction *)
-
-let fresh_constant_instance env c inst =
- let cb = lookup_constant c env in
- if cb.Declarations.const_polymorphic then
- let inst, ctx =
- fresh_instance_from
- (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst
- in
- ((c, inst), ctx)
- else ((c,Instance.empty), ContextSet.empty)
-
-let fresh_inductive_instance env ind inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- if mib.Declarations.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
- ((ind,inst), ctx)
- else ((ind,Instance.empty), ContextSet.empty)
-
-let fresh_constructor_instance env (ind,i) inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- if mib.Declarations.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
- (((ind,i),inst), ctx)
- else (((ind,i),Instance.empty), ContextSet.empty)
-
-let unsafe_constant_instance env c =
- let cb = lookup_constant c env in
- if cb.Declarations.const_polymorphic then
- let inst, ctx = unsafe_instance_from
- (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in
- ((c, inst), ctx)
- else ((c,Instance.empty), UContext.empty)
-
-let unsafe_inductive_instance env ind =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- if mib.Declarations.mind_polymorphic then
- let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
- ((ind,inst), ctx)
- else ((ind,Instance.empty), UContext.empty)
-
-let unsafe_constructor_instance env (ind,i) =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- if mib.Declarations.mind_polymorphic then
- let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
- (((ind,i),inst), ctx)
- else (((ind,i),Instance.empty), UContext.empty)
-
-open Globnames
-
-let fresh_global_instance ?names env gr =
- match gr with
- | VarRef id -> mkVar id, ContextSet.empty
- | ConstRef sp ->
- let c, ctx = fresh_constant_instance env sp names in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = fresh_constructor_instance env sp names in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = fresh_inductive_instance env sp names in
- mkIndU c, ctx
-
-let fresh_constant_instance env sp =
- fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp =
- fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp =
- fresh_constructor_instance env sp None
-
-let unsafe_global_instance env gr =
- match gr with
- | VarRef id -> mkVar id, UContext.empty
- | ConstRef sp ->
- let c, ctx = unsafe_constant_instance env sp in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = unsafe_constructor_instance env sp in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = unsafe_inductive_instance env sp in
- mkIndU c, ctx
-
-let constr_of_global gr =
- let c, ctx = fresh_global_instance (Global.env ()) gr in
- if not (Univ.ContextSet.is_empty ctx) then
- if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
- (* Should be an error as we might forget constraints, allow for now
- to make firstorder work with "using" clauses *)
- c
- else raise (Invalid_argument
- ("constr_of_global: globalization of polymorphic reference " ^
- Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^
- " would forget universes."))
- else c
-
-let constr_of_reference = constr_of_global
-
-let unsafe_constr_of_global gr =
- unsafe_global_instance (Global.env ()) gr
-
-let constr_of_global_univ (gr,u) =
- match gr with
- | VarRef id -> mkVar id
- | ConstRef sp -> mkConstU (sp,u)
- | ConstructRef sp -> mkConstructU (sp,u)
- | IndRef sp -> mkIndU (sp,u)
-
-let fresh_global_or_constr_instance env = function
- | IsConstr c -> c, ContextSet.empty
- | IsGlobal gr -> fresh_global_instance env gr
-
-let global_of_constr c =
- match kind_of_term c with
- | Const (c, u) -> ConstRef c, u
- | Ind (i, u) -> IndRef i, u
- | Construct (c, u) -> ConstructRef c, u
- | Var id -> VarRef id, Instance.empty
- | _ -> raise Not_found
-
-let global_app_of_constr c =
- match kind_of_term c with
- | Const (c, u) -> (ConstRef c, u), None
- | Ind (i, u) -> (IndRef i, u), None
- | Construct (c, u) -> (ConstructRef c, u), None
- | Var id -> (VarRef id, Instance.empty), None
- | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
- | _ -> raise Not_found
-
-open Declarations
-
-let type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env, ContextSet.empty
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- let ty = Typeops.type_of_constant_type env cb.const_type in
- if cb.const_polymorphic then
- let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in
- Vars.subst_instance_constr inst ty, ctx
- else ty, ContextSet.empty
-
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- if mib.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.mind_universes None in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- else
- let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
- ty, ContextSet.empty
- | ConstructRef cstr ->
- let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- if mib.mind_polymorphic then
- let inst, ctx = fresh_instance_from mib.mind_universes None in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
-let unsafe_type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- Typeops.type_of_constant_type env cb.const_type
-
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_inductive env (specif, inst)
-
- | ConstructRef (ind, _ as cstr) ->
- let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_constructor (cstr,inst) specif
-
-let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
-
-let fresh_sort_in_family env = function
- | InProp -> prop_sort, ContextSet.empty
- | InSet -> set_sort, ContextSet.empty
- | InType ->
- let u = fresh_level () in
- Type (Univ.Universe.make u), ContextSet.singleton u
-
-let new_sort_in_family sf =
- fst (fresh_sort_in_family (Global.env ()) sf)
-
-let extend_context (a, ctx) (ctx') =
- (a, ContextSet.union ctx ctx')
-
-let new_global_univ () =
- let u = fresh_level () in
- (Univ.Universe.make u, ContextSet.singleton u)
-
-(** Simplification *)
-
-module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
-
-let add_list_map u t map =
- try
- let l = LMap.find u map in
- LMap.update u (t :: l) map
- with Not_found ->
- LMap.add u [t] map
-
-module UF = LevelUnionFind
-
-(** Precondition: flexible <= ctx *)
-let choose_canonical ctx flexible algs s =
- let global = LSet.diff s ctx in
- let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
- (** If there is a global universe in the set, choose it *)
- if not (LSet.is_empty global) then
- let canon = LSet.choose global in
- canon, (LSet.remove canon global, rigid, flexible)
- else (** No global in the equivalence class, choose a rigid one *)
- if not (LSet.is_empty rigid) then
- let canon = LSet.choose rigid in
- canon, (global, LSet.remove canon rigid, flexible)
- else (** There are only flexible universes in the equivalence
- class, choose a non-algebraic. *)
- let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
- if not (LSet.is_empty nonalgs) then
- let canon = LSet.choose nonalgs in
- canon, (global, rigid, LSet.remove canon flexible)
- else
- let canon = LSet.choose algs in
- canon, (global, rigid, LSet.remove canon flexible)
-
-let subst_univs_fn_puniverses lsubst (c, u as cu) =
- let u' = Instance.subst_fn lsubst u in
- if u' == u then cu else (c, u')
-
-let nf_evars_and_universes_opt_subst f subst =
- let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
- let lsubst = Univ.level_subst_of subst in
- let rec aux c =
- match kind_of_term c with
- | Evar (evk, args) ->
- let args = Array.map aux args in
- (match try f (evk, args) with Not_found -> None with
- | None -> c
- | Some c -> aux c)
- | Const pu ->
- let pu' = subst_univs_fn_puniverses lsubst pu in
- if pu' == pu then c else mkConstU pu'
- | Ind pu ->
- let pu' = subst_univs_fn_puniverses lsubst pu in
- if pu' == pu then c else mkIndU pu'
- | Construct pu ->
- let pu' = subst_univs_fn_puniverses lsubst pu in
- if pu' == pu then c else mkConstructU pu'
- | Sort (Type u) ->
- let u' = Univ.subst_univs_universe subst u in
- if u' == u then c else mkSort (sort_of_univ u')
- | _ -> map_constr aux c
- in aux
-
-let fresh_universe_context_set_instance ctx =
- if ContextSet.is_empty ctx then LMap.empty, ctx
- else
- let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
- let univs',subst = LSet.fold
- (fun u (univs',subst) ->
- let u' = fresh_level () in
- (LSet.add u' univs', LMap.add u u' subst))
- univs (LSet.empty, LMap.empty)
- in
- let cst' = subst_univs_level_constraints subst cst in
- subst, (univs', cst')
-
-let normalize_univ_variable ~find ~update =
- let rec aux cur =
- let b = find cur in
- let b' = subst_univs_universe aux b in
- if Universe.equal b' b then b
- else update cur b'
- in aux
-
-let normalize_univ_variable_opt_subst ectx =
- let find l =
- match Univ.LMap.find l !ectx with
- | Some b -> b
- | None -> raise Not_found
- in
- let update l b =
- assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
- in normalize_univ_variable ~find ~update
-
-let normalize_univ_variable_subst subst =
- let find l = Univ.LMap.find l !subst in
- let update l b =
- assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
- try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in
- normalize_univ_variable ~find ~update
-
-let normalize_universe_opt_subst subst =
- let normlevel = normalize_univ_variable_opt_subst subst in
- subst_univs_universe normlevel
-
-let normalize_universe_subst subst =
- let normlevel = normalize_univ_variable_subst subst in
- subst_univs_universe normlevel
-
-let normalize_opt_subst ctx =
- let ectx = ref ctx in
- let normalize = normalize_univ_variable_opt_subst ectx in
- let () =
- Univ.LMap.iter (fun u v ->
- if Option.is_empty v then ()
- else try ignore(normalize u) with Not_found -> assert(false)) ctx
- in !ectx
-
-type universe_opt_subst = universe option universe_map
-
-let make_opt_subst s =
- fun x ->
- (match Univ.LMap.find x s with
- | Some u -> u
- | None -> raise Not_found)
-
-let subst_opt_univs_constr s =
- let f = make_opt_subst s in
- Vars.subst_univs_fn_constr f
-
-
-let normalize_univ_variables ctx =
- let ctx = normalize_opt_subst ctx in
- let undef, def, subst =
- Univ.LMap.fold (fun u v (undef, def, subst) ->
- match v with
- | None -> (Univ.LSet.add u undef, def, subst)
- | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
- ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
- in ctx, undef, def, subst
-
-let pr_universe_body = function
- | None -> mt ()
- | Some v -> str" := " ++ Univ.Universe.pr v
-
-let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
-
-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',lower) ->
- if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
- insts; raise Not_found
- with Found (f,l) -> (f,l)
-
-let compute_lbound left =
- (** The universe variable was not fixed yet.
- Compute its level using its lower bound. *)
- let sup l lbound =
- match lbound with
- | None -> Some l
- | Some l' -> Some (Universe.sup l l')
- in
- List.fold_left (fun lbound (d, l) ->
- if d == Le (* l <= ?u *) then sup l lbound
- else (* l < ?u *)
- (assert (d == Lt);
- if not (Universe.level l == None) then
- sup (Universe.super l) lbound
- else None))
- None left
-
-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,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,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)
- 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 =
- Univ.LMap.fold (fun r lower (left, lbounds as acc) ->
- if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
- else (* Fixed universe, just compute its glb for sharing *)
- 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, 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, 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
- in
- let instantiate_lbound lbound =
- let alg = LSet.mem u algs in
- if alg then
- (* u is algebraic: we instantiate it with its lower bound, if any,
- or enforce the constraints if it is bounded from the top. *)
- 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 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 lower false true acc
- in
- let acc' acc =
- match right with
- | None -> acc
- | Some 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,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
- else
- try let lev = Option.get (Universe.level inst) in
- Constraint.add (lev, d, r) cstrs
- with Option.IsNone -> failwith "")
- cstrs dangling
- in
- (ctx', us, algs, insts, cstrs'), b
- in
- 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, lower))
- | Some lbound ->
- try acc' (instantiate_lbound lbound)
- 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
- in
- LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) ->
- if v == None then fst (aux acc u)
- else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
- us (ctx, us, algs, lbounds, cstrs)
-
-let normalize_context_set ctx us algs =
- let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
- let uf = UF.create () in
- (** Keep the Prop/Set <= i constraints separate for minimization *)
- let smallles, csts =
- Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
- if d == Le then
- if Univ.Level.is_small l then
- if is_set_minimization () && LSet.mem r ctx then
- (Constraint.add cstr smallles, noneqs)
- else (smallles, noneqs)
- else if Level.is_small r then
- if Level.is_prop r then
- raise (Univ.UniverseInconsistency
- (Le,Universe.make l,Universe.make r,None))
- else (smallles, Constraint.add (l,Eq,r) noneqs)
- else (smallles, Constraint.add cstr noneqs)
- else (smallles, Constraint.add cstr noneqs))
- csts (Constraint.empty, Constraint.empty)
- in
- let csts =
- (* We first put constraints in a normal-form: all self-loops are collapsed
- to equalities. *)
- let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
- ctx UGraph.empty_universes
- in
- let g =
- Univ.Constraint.fold
- (fun (l, d, r) g ->
- let g =
- if not (Level.is_small l || LSet.mem l ctx) then
- try UGraph.add_universe l false g
- with UGraph.AlreadyDeclared -> g
- else g
- in
- let g =
- if not (Level.is_small r || LSet.mem r ctx) then
- try UGraph.add_universe r false g
- with UGraph.AlreadyDeclared -> g
- else g
- in g) csts g
- in
- let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
- UGraph.constraints_of_universes g
- in
- let noneqs =
- Constraint.fold (fun (l,d,r as cstr) noneqs ->
- if d == Eq then (UF.union l r uf; noneqs)
- else (* We ignore the trivial Prop/Set <= i constraints. *)
- if d == Le && Univ.Level.is_small l then noneqs
- else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
- then noneqs
- else Constraint.add cstr noneqs)
- csts Constraint.empty
- in
- let noneqs = Constraint.union noneqs smallles in
- let partition = UF.partition uf in
- let flex x = LMap.mem x us in
- let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s ->
- let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
- (* Add equalities for globals which can't be merged anymore. *)
- let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) global
- cstrs
- in
- (* Also add equalities for rigid variables *)
- let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) rigid
- cstrs
- in
- let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in
- let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in
- let canonu = Some (Universe.make canon) in
- let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
- (LSet.diff ctx flexible, subst, us, cstrs))
- (ctx, LMap.empty, us, Constraint.empty) partition
- in
- (* Noneqs is now in canonical form w.r.t. equality constraints,
- and contains only inequality constraints. *)
- let noneqs = subst_univs_level_constraints subst noneqs in
- (* Compute the left and right set of flexible variables, constraints
- 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 ucstrsl' =
- if lus then add_list_map l (d, r) ucstrsl
- else ucstrsl
- and ucstrsr' =
- add_list_map r (d, l) ucstrsr
- in
- let noneqs =
- if lus || rus then noneq
- else Constraint.add cstr noneq
- in (noneqs, ucstrsl', ucstrsr'))
- noneqs (Constraint.empty, LMap.empty, LMap.empty)
- in
- (* Now we construct the instantiation of each variable. *)
- let ctx', us, algs, inst, noneqs =
- minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
- in
- let us = normalize_opt_subst us in
- (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
-
-let universes_of_constr c =
- let rec aux s c =
- match kind_of_term c with
- | Const (_, u) | Ind (_, u) | Construct (_, u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Sort u when not (Sorts.is_small u) ->
- let u = univ_of_sort u in
- LSet.fold LSet.add (Universe.levels u) s
- | _ -> fold_constr aux s c
- in aux LSet.empty c
-
-let restrict_universe_context (univs,csts) s =
- (* Universes that are not necessary to typecheck the term.
- E.g. univs introduced by tactics and not used in the proof term. *)
- let diff = LSet.diff univs s in
- let rec aux diff candid univs ness =
- let (diff', candid', univs', ness') =
- Constraint.fold
- (fun (l, d, r as c) (diff, candid, univs, csts) ->
- if not (LSet.mem l diff) then
- (LSet.remove r diff, candid, univs, Constraint.add c csts)
- else if not (LSet.mem r diff) then
- (LSet.remove l diff, candid, univs, Constraint.add c csts)
- else (diff, Constraint.add c candid, univs, csts))
- candid (diff, Constraint.empty, univs, ness)
- in
- if ness' == ness then (LSet.diff univs diff', ness)
- else aux diff' candid' univs' ness'
- in aux diff csts univs Constraint.empty
-
-let simplify_universe_context (univs,csts) =
- let uf = UF.create () in
- let noneqs =
- Constraint.fold (fun (l,d,r) noneqs ->
- if d == Eq && (LSet.mem l univs || LSet.mem r univs) then
- (UF.union l r uf; noneqs)
- else Constraint.add (l,d,r) noneqs)
- csts Constraint.empty
- in
- let partition = UF.partition uf in
- let flex x = LSet.mem x univs in
- let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s ->
- let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in
- (* Add equalities for globals which can't be merged anymore. *)
- let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid)
- cstrs
- in
- let subst = LSet.fold (fun f -> LMap.add f canon)
- flexible subst
- in (subst, LSet.diff univs flexible, cstrs))
- (LMap.empty, univs, noneqs) partition
- in
- (* Noneqs is now in canonical form w.r.t. equality constraints,
- and contains only inequality constraints. *)
- let csts' = subst_univs_level_constraints subst csts' in
- (univs', csts'), subst
-
-let is_trivial_leq (l,d,r) =
- Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
-
-(* Prop < i <-> Set+1 <= i <-> Set < i *)
-let translate_cstr (l,d,r as cstr) =
- if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
- (Level.set, d, r)
- else cstr
-
-let refresh_constraints univs (ctx, cstrs) =
- let cstrs', univs' =
- Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
- let c = translate_cstr c in
- if is_trivial_leq c then acc
- else (Univ.Constraint.add c cstrs', UGraph.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.mapi (fun i o ->
- match o with
- | Some u ->
- (match Universe.level u with
- | Some u -> Some u
- | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
- | None -> None)
- levels in
- let v = Array.copy level_bounds in
- let nind = Array.length v in
- let clos = Array.map (fun _ -> Int.Set.empty) levels in
- (* First compute the transitive closure of the levels dependencies *)
- for i=0 to nind-1 do
- for j=0 to nind-1 do
- if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
- clos.(i) <- Int.Set.add j clos.(i);
- done;
- done;
- let rec closure () =
- let continue = ref false in
- Array.iteri (fun i deps ->
- let deps' =
- Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
- in
- if Int.Set.equal deps deps' then ()
- else (clos.(i) <- deps'; continue := true))
- clos;
- if !continue then closure ()
- else ()
- in
- closure ();
- for i=0 to nind-1 do
- for j=0 to nind-1 do
- if not (Int.equal i j) && Int.Set.mem j clos.(i) then
- (v.(i) <- Universe.sup v.(i) level_bounds.(j));
- done;
- done;
- v
diff --git a/library/universes.mli b/library/universes.mli
deleted file mode 100644
index d3a271b8d0..0000000000
--- a/library/universes.mli
+++ /dev/null
@@ -1,238 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Environ
-open Univ
-
-val set_minimization : bool ref
-val is_set_minimization : unit -> bool
-
-(** Universes *)
-
-(** Global universe name <-> level mapping *)
-type universe_names =
- (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
-
-val global_universe_names : unit -> universe_names
-val set_global_universe_names : universe_names -> unit
-
-val pr_with_global_universes : Level.t -> Pp.std_ppcmds
-
-(** Local universe name <-> level mapping *)
-
-type universe_binders = (Id.t * Univ.universe_level) list
-
-val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
-val universe_binders_of_global : Globnames.global_reference -> universe_binders
-
-(** The global universe counter *)
-val set_remote_new_univ_level : universe_level RemoteCounter.installer
-
-(** Side-effecting functions creating new universe levels. *)
-
-val new_univ_level : Names.dir_path -> universe_level
-val new_univ : Names.dir_path -> universe
-val new_Type : Names.dir_path -> types
-val new_Type_sort : Names.dir_path -> sorts
-
-val new_global_univ : unit -> universe in_universe_context_set
-val new_sort_in_family : sorts_family -> sorts
-
-(** {6 Constraints for type inference}
-
- When doing conversion of universes, not only do we have =/<= constraints but
- also Lub constraints which correspond to unification of two levels which might
- not be necessary if unfolding is performed.
-*)
-
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = universe * universe_constraint_type * universe
-module Constraints : sig
- include Set.S with type elt = universe_constraint
-
- val pr : t -> Pp.std_ppcmds
-end
-
-type universe_constraints = Constraints.t
-type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
-type 'a universe_constrained = 'a * universe_constraints
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-val subst_univs_universe_constraints : universe_subst_fn ->
- universe_constraints -> universe_constraints
-
-val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
-
-val to_constraints : UGraph.t -> universe_constraints -> constraints
-
-(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
- application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
- constr -> constr -> 'a -> 'a option
-
-(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
- {!eq_constr_univs_infer} taking kind-of-term functions, to expose
- subterms of [m] and [n], arguments. *)
-val eq_constr_univs_infer_with :
- (constr -> (constr,types) kind_of_term) ->
- (constr -> (constr,types) kind_of_term) ->
- UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
-
-(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
- modulo alpha, casts, application grouping, the universe constraints
- in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
- constr -> constr -> 'a -> 'a option
-
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
- application grouping and the universe constraints in [c]. *)
-val eq_constr_universes : constr -> constr -> bool universe_constrained
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
- alpha, casts, application grouping and the universe constraints in [c]. *)
-val leq_constr_universes : constr -> constr -> bool universe_constrained
-
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
- application grouping and the universe constraints in [c]. *)
-val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
-
-(** Build a fresh instance for a given context, its associated substitution and
- the instantiated constraints. *)
-
-val fresh_instance_from_context : universe_context ->
- universe_instance constrained
-
-val fresh_instance_from : universe_context -> universe_instance option ->
- universe_instance in_universe_context_set
-
-val fresh_sort_in_family : env -> sorts_family ->
- sorts in_universe_context_set
-val fresh_constant_instance : env -> constant ->
- pconstant in_universe_context_set
-val fresh_inductive_instance : env -> inductive ->
- pinductive in_universe_context_set
-val fresh_constructor_instance : env -> constructor ->
- pconstructor in_universe_context_set
-
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
- constr in_universe_context_set
-
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
- constr in_universe_context_set
-
-(** Get fresh variables for the universe context.
- Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set ->
- universe_level_subst * universe_context_set
-
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> Globnames.global_reference puniverses
-
-val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
-
-val constr_of_global_univ : Globnames.global_reference puniverses -> constr
-
-val extend_context : 'a in_universe_context_set -> universe_context_set ->
- 'a in_universe_context_set
-
-(** Simplification and pruning of constraints:
- [normalize_context_set ctx us]
-
- - Instantiate the variables in [us] with their most precise
- universe levels respecting the constraints.
-
- - Normalizes the context [ctx] w.r.t. equality constraints,
- choosing a canonical universe in each equivalence class
- (a global one if there is one) and transitively saturate
- the constraints w.r.t to the equalities. *)
-
-module UF : Unionfind.PartitionSig with type elt = universe_level
-
-type universe_opt_subst = universe option universe_map
-
-val make_opt_subst : universe_opt_subst -> universe_subst_fn
-
-val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
-
-val normalize_context_set : universe_context_set ->
- universe_opt_subst (* The defined and undefined variables *) ->
- universe_set (* univ variables that can be substituted by algebraics *) ->
- (universe_opt_subst * universe_set) in_universe_context_set
-
-val normalize_univ_variables : universe_opt_subst ->
- universe_opt_subst * universe_set * universe_set * universe_subst
-
-val normalize_univ_variable :
- find:(universe_level -> universe) ->
- update:(universe_level -> universe -> universe) ->
- universe_level -> universe
-
-val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
- (universe_level -> universe)
-
-val normalize_univ_variable_subst : universe_subst ref ->
- (universe_level -> universe)
-
-val normalize_universe_opt_subst : universe_opt_subst ref ->
- (universe -> universe)
-
-val normalize_universe_subst : universe_subst ref ->
- (universe -> universe)
-
-(** Create a fresh global in the global environment, without side effects.
- BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
- the constraints should be properly added to an evd.
- See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
- the proper way to get a fresh copy of a global reference. *)
-val constr_of_global : Globnames.global_reference -> constr
-
-(** ** DEPRECATED ** synonym of [constr_of_global] *)
-val constr_of_reference : Globnames.global_reference -> constr
-
-(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
- references and computing their instantiated universe context. (side-effect on the
- universe counter, use with care). *)
-val type_of_global : Globnames.global_reference -> types in_universe_context_set
-
-(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well.
- USE with care. *)
-val unsafe_type_of_global : Globnames.global_reference -> types
-
-(** Full universes substitutions into terms *)
-
-val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
- universe_opt_subst -> constr -> constr
-
-(** Shrink a universe context to a restricted set of variables *)
-
-val universes_of_constr : constr -> universe_set
-val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
-val simplify_universe_context : universe_context_set ->
- universe_context_set * universe_level_subst
-
-val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
-
-(** Pretty-printing *)
-
-val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
-
-(** {6 Support for old-style sort-polymorphism } *)
-
-val solve_constraints_system : universe option array -> universe array -> universe array ->
- universe array
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 20:57:35 +0000