diff options
Diffstat (limited to 'library')
36 files changed, 7102 insertions, 0 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml new file mode 100644 index 0000000000..784360dc8a --- /dev/null +++ b/library/coqlib.ml @@ -0,0 +1,323 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CErrors +open Util +open Pp +open Names +open Libnames +open Globnames + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) + +(************************************************************************) +(* Coq reference API *) +(************************************************************************) +let coq = Libnames.coq_string (* "Coq" *) + +let init_dir = [ coq; "Init"] + +let jmeq_module_name = [coq;"Logic";"JMeq"] +let jmeq_library_path = make_dir jmeq_module_name +let jmeq_module = MPfile jmeq_library_path + +let find_reference locstr dir s = + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in + Nametab.global_of_path sp + +let coq_reference locstr dir s = find_reference locstr (coq::dir) s + +let table : GlobRef.t CString.Map.t ref = + let name = "coqlib_registered" in + Summary.ref ~name CString.Map.empty + +let get_lib_refs () = + CString.Map.bindings !table + +let has_ref s = CString.Map.mem s !table + +let check_ind_ref s ind = + match CString.Map.find s !table with + | IndRef r -> eq_ind r ind + | _ -> false + | exception Not_found -> false + +let lib_ref s = + try CString.Map.find s !table + with Not_found -> + user_err Pp.(str "not found in table: " ++ str s) + +let add_ref s c = + table := CString.Map.add s c !table + +let cache_ref (_,(s,c)) = + add_ref s c + +let (inCoqlibRef : string * GlobRef.t -> Libobject.obj) = + let open Libobject in + declare_object { (default_object "COQLIBREF") with + cache_function = cache_ref; + load_function = (fun _ x -> cache_ref x); + classify_function = (fun o -> Substitute o); + subst_function = ident_subst_function; + discharge_function = fun (_, sc) -> Some sc } + +(** Replaces a binding ! *) +let register_ref s c = + Lib.add_anonymous_leaf @@ inCoqlibRef (s,c) + +(************************************************************************) +(* Generic functions to find Coq objects *) + +let has_suffix_in_dirs dirs ref = + let dir = dirpath (Nametab.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 GlobRef.Ordered_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 DirPath.print 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 DirPath.print 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 + user_err ~hdr:"Coqlib.check_required_library" + (str "Library " ++ DirPath.print dir ++ str " has to be required first.") + +(************************************************************************) +(* Specific Coq objects *) +(************************************************************************) + +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_modules = [ + init_dir@["Datatypes"]; + init_dir@["Logic"]; + init_dir@["Specif"]; + init_dir@["Logic_Type"]; + init_dir@["Nat"]; + init_dir@["Peano"]; + init_dir@["Wf"] +] + +let logic_module_name = init_dir@["Logic"] +let logic_module = MPfile (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 = MPfile (make_dir datatypes_module_name) + +(** Identity *) + +let id = Constant.make2 datatypes_module @@ Label.make "idProp" +let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp" + +(** Natural numbers *) +let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat" +let nat_path = Libnames.make_path (make_dir datatypes_module_name) (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 = MutInd.make2 datatypes_module @@ Label.make "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 = MutInd.make2 logic_module @@ Label.make "eq" +let glob_eq = IndRef (eq_kn,0) + +let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity" +let glob_identity = IndRef (identity_kn,0) + +let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq" +let glob_jmeq = IndRef (jmeq_kn,0) + +(* Sigma data *) +type coq_sigma_data = { + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } + +let build_sigma_gen str = + { typ = lib_ref ("core." ^ str ^ ".type"); + elim = lib_ref ("core." ^ str ^ ".rect"); + intro = lib_ref ("core." ^ str ^ ".intro"); + proj1 = lib_ref ("core." ^ str ^ ".proj1"); + proj2 = lib_ref ("core." ^ str ^ ".proj2"); + } + +let build_prod () = build_sigma_gen "prod" +let build_sigma () = build_sigma_gen "sig" +let build_sigma_type () = build_sigma_gen "sigT" + +(* Booleans *) + +type coq_bool_data = { + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} + +let build_bool_type () = + { andb = lib_ref "core.bool.andb"; + andb_prop = lib_ref "core.bool.andb_prop"; + andb_true_intro = lib_ref "core.bool.andb_true_intro"; } + +(* Equalities *) +type coq_eq_data = { + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } + +(* Leibniz equality on Type *) + +let build_eqdata_gen str = { + eq = lib_ref ("core." ^ str ^ ".type"); + ind = lib_ref ("core." ^ str ^ ".ind"); + refl = lib_ref ("core." ^ str ^ ".refl"); + sym = lib_ref ("core." ^ str ^ ".sym"); + trans = lib_ref ("core." ^ str ^ ".trans"); + congr = lib_ref ("core." ^ str ^ ".congr"); + } + +let build_coq_eq_data () = build_eqdata_gen "eq" +let build_coq_jmeq_data () = build_eqdata_gen "JMeq" +let build_coq_identity_data () = build_eqdata_gen "identity" + +(* Inversion data... *) + +(* Data needed for discriminate and injection *) +type coq_inversion_data = { + inv_eq : GlobRef.t; (* : forall params, t -> Prop *) + inv_ind : GlobRef.t; (* : forall params P y, eq params y -> P y *) + inv_congr: GlobRef.t (* : forall params B (f:t->B) y, eq params y -> f c=f y *) +} + +let build_coq_inversion_gen l str = + List.iter check_required_library l; { + inv_eq = lib_ref ("core." ^ str ^ ".type"); + inv_ind = lib_ref ("core." ^ str ^ ".ind"); + inv_congr = lib_ref ("core." ^ str ^ ".congr_canonical"); + } + +let build_coq_inversion_eq_data () = + build_coq_inversion_gen [logic_module_name] "eq" + +let build_coq_inversion_eq_true_data () = + build_coq_inversion_gen [logic_module_name] "True" + +let build_coq_inversion_identity_data () = + build_coq_inversion_gen [logic_module_name] "identity" + +(* This needs a special case *) +let build_coq_inversion_jmeq_data () = { + inv_eq = lib_ref "core.JMeq.hom"; + inv_ind = lib_ref "core.JMeq.ind"; + inv_congr = lib_ref "core.JMeq.congr_canonical"; +} + +(* Specif *) +let build_coq_sumbool () = lib_ref "core.sumbool.type" + +let build_coq_eq () = lib_ref "core.eq.type" +let build_coq_eq_refl () = lib_ref "core.eq.refl" +let build_coq_eq_sym () = lib_ref "core.eq.sym" +let build_coq_f_equal2 () = lib_ref "core.eq.congr2" + +(* Runtime part *) +let build_coq_True () = lib_ref "core.True.type" +let build_coq_I () = lib_ref "core.True.I" +let build_coq_identity () = lib_ref "core.identity.type" + +let build_coq_eq_true () = lib_ref "core.eq_true.type" +let build_coq_jmeq () = lib_ref "core.JMeq.type" + +let build_coq_prod () = lib_ref "core.prod.type" +let build_coq_pair () = lib_ref "core.prod.intro" + +let build_coq_False () = lib_ref "core.False.type" +let build_coq_not () = lib_ref "core.not.type" +let build_coq_and () = lib_ref "core.and.type" +let build_coq_conj () = lib_ref "core.and.conj" +let build_coq_or () = lib_ref "core.or.type" +let build_coq_ex () = lib_ref "core.ex.type" +let build_coq_sig () = lib_ref "core.sig.type" +let build_coq_existT () = lib_ref "core.sigT.existT" +let build_coq_iff () = lib_ref "core.iff.type" + +let build_coq_iff_left_proj () = lib_ref "core.iff.proj1" +let build_coq_iff_right_proj () = lib_ref "core.iff.proj2" + +(* The following is less readable but does not depend on parsing *) +let coq_eq_ref = Lazy.from_fun build_coq_eq +let coq_identity_ref = Lazy.from_fun build_coq_identity +let coq_jmeq_ref = Lazy.from_fun build_coq_jmeq +let coq_eq_true_ref = Lazy.from_fun build_coq_eq_true +let coq_existS_ref = Lazy.from_fun build_coq_existT +let coq_existT_ref = Lazy.from_fun build_coq_existT +let coq_exist_ref = Lazy.from_fun build_coq_ex +let coq_not_ref = Lazy.from_fun build_coq_not +let coq_False_ref = Lazy.from_fun build_coq_False +let coq_sumbool_ref = Lazy.from_fun build_coq_sumbool +let coq_sig_ref = Lazy.from_fun build_coq_sig +let coq_or_ref = Lazy.from_fun build_coq_or +let coq_iff_ref = Lazy.from_fun build_coq_iff + +(** Deprecated functions that search by library name. *) +let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.") diff --git a/library/coqlib.mli b/library/coqlib.mli new file mode 100644 index 0000000000..f6779dbbde --- /dev/null +++ b/library/coqlib.mli @@ -0,0 +1,300 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Names + +(** Indirection between logical names and global references. + + This module provides a mechanism to bind “names” to constants and to look up + these constants using their names. + + The two main functions are [register_ref n r] which binds the name [n] to + the reference [r] and [lib_ref n] which returns the previously registered + reference under name [n]. + + The first function is meant to be available through the vernacular command + [Register r as n], so that plug-ins can refer to a constant without knowing + its user-facing name, the precise module path in which it is defined, etc. + + For instance, [lib_ref "core.eq.type"] returns the proper [GlobRef.t] for + the type of the core equality type. +*) + +(** Registers a global reference under the given name. *) +val register_ref : string -> GlobRef.t -> unit + +(** Retrieves the reference bound to the given name (by a previous call to {!register_ref}). + Raises an error if no reference is bound to this name. *) +val lib_ref : string -> GlobRef.t + +(** Checks whether a name refers to a registered constant. + For any name [n], if [has_ref n] returns [true], [lib_ref n] will succeed. *) +val has_ref : string -> bool + +(** Checks whether a name is bound to a known inductive. *) +val check_ind_ref : string -> inductive -> bool + +(** List of all currently bound names. *) +val get_lib_refs : unit -> (string * GlobRef.t) list + +(* Exceptions to deprecation *) + +(** {2 For Equality tactics} *) + +type coq_sigma_data = { + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } + +val build_sigma_set : coq_sigma_data delayed +val build_sigma_type : coq_sigma_data delayed +val build_sigma : coq_sigma_data delayed + +type coq_eq_data = { + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } + +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 + +(* XXX: Some tactics special case JMeq, they should instead check for + the constant, not the module *) +(** For tactics/commands requiring vernacular libraries *) +val check_required_library : string list -> unit + +(* Used by obligations *) +val datatypes_module_name : string list + +(* Used by ind_schemes *) +val logic_module_name : string list + +(* Used by tactics *) +val jmeq_module_name : string list + + +(*************************************************************************) +(** {2 DEPRECATED} *) +(*************************************************************************) + +(** All the functions below are deprecated and should go away in the + next coq version ... *) + +(** [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 *) +val find_reference : string -> string list -> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** This just prefixes find_reference with Coq... *) +val coq_reference : string -> string list -> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Search in several modules (not prefixed by "Coq") *) +val gen_reference_in_modules : string->string list list-> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val arith_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val zarith_base_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val init_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** {6 Global references } *) + +(** Modules *) +val logic_module : ModPath.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val logic_type_module : DirPath.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Identity *) +val id : Constant.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val type_of_id : Constant.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Natural numbers *) + +val nat_path : Libnames.full_path +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val glob_nat : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val path_of_O : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val path_of_S : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_O : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_S : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Booleans *) +val glob_bool : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val path_of_true : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val path_of_false : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_true : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_false : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Equality *) +val glob_eq : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_identity : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val glob_jmeq : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** {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 : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t +} + +val build_bool_type : coq_bool_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Non-dependent pairs in Set from Datatypes *) +val build_prod : coq_sigma_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val build_coq_eq : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +(** = [(build_coq_eq_data()).eq] *) + +val build_coq_eq_refl : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +(** = [(build_coq_eq_data()).refl] *) + +val build_coq_eq_sym : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +(** = [(build_coq_eq_data()).sym] *) + +val build_coq_f_equal2 : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Data needed for discriminate and injection *) + +type coq_inversion_data = { + inv_eq : GlobRef.t; (** : forall params, args -> Prop *) + inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args + -> P args *) + inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> + f params = f args *) +} + +val build_coq_inversion_eq_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_inversion_identity_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_inversion_jmeq_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_inversion_eq_true_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Specif *) +val build_coq_sumbool : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** {6 ... } + Connectives + The False proposition *) +val build_coq_False : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** The True proposition and its unique proof *) +val build_coq_True : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_I : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Negation *) +val build_coq_not : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Conjunction *) +val build_coq_and : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_conj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_iff : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val build_coq_iff_left_proj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_iff_right_proj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Pairs *) +val build_coq_prod : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val build_coq_pair : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Disjunction *) +val build_coq_or : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +(** Existential quantifier *) +val build_coq_ex : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val coq_eq_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_identity_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_jmeq_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_eq_true_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_existS_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_existT_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_exist_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_not_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_False_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_sumbool_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_sig_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + +val coq_or_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] +val coq_iff_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml new file mode 100644 index 0000000000..171d51800e --- /dev/null +++ b/library/decl_kinds.ml @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Informal mathematical status of declarations *) + +type discharge = DoDischarge | NoDischarge + +type locality = Discharge | Local | Global + +type binding_kind = Explicit | Implicit + +type polymorphic = bool + +type private_flag = bool + +type cumulative_inductive_flag = bool + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) +type assumption_kind = locality * polymorphic * assumption_object_kind +type definition_kind = locality * polymorphic * definition_object_kind + +(** Kinds used in proofs *) + +type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + +type goal_kind = locality * polymorphic * goal_object_kind + +(** Kinds used in library *) + +type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind diff --git a/library/declaremods.ml b/library/declaremods.ml new file mode 100644 index 0000000000..8699583cdf --- /dev/null +++ b/library/declaremods.ml @@ -0,0 +1,1015 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names +open Declarations +open Entries +open Libnames +open Libobject +open Mod_subst + +(** {6 Inlining levels} *) + +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + +type module_kind = Module | ModType | ModAny + +let default_inline () = Some (Flags.get_inline_level ()) + +let inl2intopt = function + | NoInline -> None + | InlineAt i -> Some i + | DefaultInline -> default_inline () + +(** {6 Substitutive objects} + + - The list of bound identifiers is nonempty only if the objects + are owned by a functor + + - Then comes either the object segment itself (for interactive + modules), or a compact way to store derived objects (path to + a earlier module + subtitution). +*) + +type algebraic_objects = + | Objs of Lib.lib_objects + | Ref of ModPath.t * substitution + +type substitutive_objects = MBId.t list * algebraic_objects + +(** ModSubstObjs : a cache of module substitutive objects + + This table is common to modules and module types. + - For a Module M:=N, the objects of N will be reloaded + with M after substitution. + - For a Module M:SIG:=..., the module M gets its objects from SIG + + Invariants: + - A alias (i.e. a module path inside a Ref constructor) should + never lead to another alias, but rather to a concrete Objs + constructor. + + We will plug later a handler dealing with missing entries in the + cache. Such missing entries may come from inner parts of module + types, which aren't registered by the standard libobject machinery. +*) + +module ModSubstObjs : + sig + val set : ModPath.t -> substitutive_objects -> unit + val get : ModPath.t -> substitutive_objects + val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit + end = + struct + let table = + Summary.ref (MPmap.empty : substitutive_objects MPmap.t) + ~name:"MODULE-SUBSTOBJS" + let missing_handler = ref (fun mp -> assert false) + let set_missing_handler f = (missing_handler := f) + let set mp objs = (table := MPmap.add mp objs !table) + let get mp = + try MPmap.find mp !table with Not_found -> !missing_handler mp + end + +(** Some utilities about substitutive objects : + substitution, expansion *) + +let sobjs_no_functor (mbids,_) = List.is_empty mbids + +let subst_aobjs sub = function + | Objs o -> Objs (Lib.subst_objects sub o) + | Ref (mp, sub0) -> Ref (mp, join sub0 sub) + +let subst_sobjs sub (mbids,aobjs) = (mbids, subst_aobjs sub aobjs) + +let expand_aobjs = function + | Objs o -> o + | Ref (mp, sub) -> + match ModSubstObjs.get mp with + | (_,Objs o) -> Lib.subst_objects sub o + | _ -> assert false (* Invariant : any alias points to concrete objs *) + +let expand_sobjs (_,aobjs) = expand_aobjs aobjs + + +(** {6 ModObjs : a cache of module objects} + + For each module, we also store a cache of + "prefix", "substituted objects", "keep objects". + This is used for instance to implement the "Import" command. + + substituted objects : + roughly the objects above after the substitution - we need to + keep them to call open_object when the module is opened (imported) + + keep objects : + The list of non-substitutive objects - as above, for each of + them we will call open_object when the module is opened + + (Some) Invariants: + * If the module is a functor, it won't appear in this cache. + + * Module objects in substitutive_objects part have empty substituted + objects. + + * Modules which where created with Module M:=mexpr or with + Module M:SIG. ... End M. have the keep list empty. +*) + +type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects + +module ModObjs : + sig + val set : ModPath.t -> module_objects -> unit + val get : ModPath.t -> module_objects (* may raise Not_found *) + val all : unit -> module_objects MPmap.t + end = + struct + let table = + Summary.ref (MPmap.empty : module_objects MPmap.t) + ~name:"MODULE-OBJS" + let set mp objs = (table := MPmap.add mp objs !table) + let get mp = MPmap.find mp !table + let all () = !table + end + + +(** {6 Name management} + + Auxiliary functions to transform full_path and kernel_name given + by Lib into ModPath.t and DirPath.t needed for modules +*) + +let mp_of_kn kn = + let mp,l = KerName.repr kn in + MPdot (mp,l) + +let dir_of_sp sp = + let dir,id = repr_path sp in + add_dirpath_suffix dir id + + +(** {6 Declaration of module substitutive objects} *) + +(** These functions register the visibility of the module and iterates + through its components. They are called by plenty of module functions *) + +let consistency_checks exists dir dirinfo = + if exists then + let globref = + try Nametab.locate_dir (qualid_of_dirpath dir) + with Not_found -> + user_err ~hdr:"consistency_checks" + (DirPath.print dir ++ str " should already exist!") + in + assert (Nametab.GlobDirRef.equal globref dirinfo) + else + if Nametab.exists_dir dir then + user_err ~hdr:"consistency_checks" + (DirPath.print dir ++ str " already exists") + +let compute_visibility exists i = + if exists then Nametab.Exactly i else Nametab.Until i + +(** Iterate some function [iter_objects] on all components of a module *) + +let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let dirinfo = Nametab.GlobDirRef.DirModule prefix in + consistency_checks exists obj_dir dirinfo; + Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; + ModSubstObjs.set obj_mp sobjs; + (* If we're not a functor, let's iter on the internal components *) + if sobjs_no_functor sobjs then begin + let objs = expand_sobjs sobjs in + ModObjs.set obj_mp (prefix,objs,kobjs); + iter_objects (i+1) prefix objs; + iter_objects (i+1) prefix kobjs + end + +let do_module' exists iter_objects i ((sp,kn),sobjs) = + do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs [] + +(** Nota: Interactive modules and module types cannot be recached! + This used to be checked here via a flag along the substobjs. *) + +let cache_module = do_module' false Lib.load_objects 1 +let load_module = do_module' false Lib.load_objects +let open_module = do_module' true Lib.open_objects +let subst_module (subst,sobjs) = subst_sobjs subst sobjs +let classify_module sobjs = Substitute sobjs + +let (in_module : substitutive_objects -> obj), + (out_module : obj -> substitutive_objects) = + declare_object_full {(default_object "MODULE") with + cache_function = cache_module; + load_function = load_module; + open_function = open_module; + subst_function = subst_module; + classify_function = classify_module } + + +(** {6 Declaration of module keep objects} *) + +let cache_keep _ = anomaly (Pp.str "This module should not be cached!") + +let load_keep i ((sp,kn),kobjs) = + (* Invariant : seg isn't empty *) + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix',sobjs,kobjs0 = + try ModObjs.get obj_mp + with Not_found -> assert false (* a substobjs should already be loaded *) + in + assert Nametab.(eq_op prefix' prefix); + assert (List.is_empty kobjs0); + ModObjs.set obj_mp (prefix,sobjs,kobjs); + Lib.load_objects i prefix kobjs + +let open_keep i ((sp,kn),kobjs) = + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + Lib.open_objects i prefix kobjs + +let in_modkeep : Lib.lib_objects -> obj = + declare_object {(default_object "MODULE KEEP") with + cache_function = cache_keep; + load_function = load_keep; + open_function = open_keep } + + +(** {6 Declaration of module type substitutive objects} *) + +(** Nota: Interactive modules and module types cannot be recached! + This used to be checked more properly here. *) + +let do_modtype i sp mp sobjs = + if Nametab.exists_modtype sp then + anomaly (pr_path sp ++ str " already exists."); + Nametab.push_modtype (Nametab.Until i) sp mp; + ModSubstObjs.set mp sobjs + +let cache_modtype ((sp,kn),sobjs) = do_modtype 1 sp (mp_of_kn kn) sobjs +let load_modtype i ((sp,kn),sobjs) = do_modtype i sp (mp_of_kn kn) sobjs +let subst_modtype (subst,sobjs) = subst_sobjs subst sobjs +let classify_modtype sobjs = Substitute sobjs + +let open_modtype i ((sp,kn),_) = + let mp = mp_of_kn kn in + let mp' = + try Nametab.locate_modtype (qualid_of_path sp) + with Not_found -> + anomaly (pr_path sp ++ str " should already exist!"); + in + assert (ModPath.equal mp mp'); + Nametab.push_modtype (Nametab.Exactly i) sp mp + +let (in_modtype : substitutive_objects -> obj), + (out_modtype : obj -> substitutive_objects) = + declare_object_full {(default_object "MODULE TYPE") with + cache_function = cache_modtype; + open_function = open_modtype; + load_function = load_modtype; + subst_function = subst_modtype; + classify_function = classify_modtype } + + +(** {6 Declaration of substitutive objects for Include} *) + +let do_include do_load do_open i ((sp,kn),aobjs) = + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let o = expand_aobjs aobjs in + if do_load then Lib.load_objects i prefix o; + if do_open then Lib.open_objects i prefix o + +let cache_include = do_include true true 1 +let load_include = do_include true false +let open_include = do_include false true +let subst_include (subst,aobjs) = subst_aobjs subst aobjs +let classify_include aobjs = Substitute aobjs + +let (in_include : algebraic_objects -> obj), + (out_include : obj -> algebraic_objects) = + declare_object_full {(default_object "INCLUDE") with + cache_function = cache_include; + load_function = load_include; + open_function = open_include; + subst_function = subst_include; + classify_function = classify_include } + + +(** {6 Handler for missing entries in ModSubstObjs} *) + +(** Since the inner of Module Types are not added by default to + the ModSubstObjs table, we compensate this by explicit traversal + of Module Types inner objects when needed. Quite a hack... *) + +let mp_id mp id = MPdot (mp, Label.of_id id) + +let rec register_mod_objs mp (id,obj) = match object_tag obj with + | "MODULE" -> ModSubstObjs.set (mp_id mp id) (out_module obj) + | "MODULE TYPE" -> ModSubstObjs.set (mp_id mp id) (out_modtype obj) + | "INCLUDE" -> + List.iter (register_mod_objs mp) (expand_aobjs (out_include obj)) + | _ -> () + +let handle_missing_substobjs mp = match mp with + | MPdot (mp',l) -> + let objs = expand_sobjs (ModSubstObjs.get mp') in + List.iter (register_mod_objs mp') objs; + ModSubstObjs.get mp + | _ -> + assert false (* Only inner parts of module types should be missing *) + +let () = ModSubstObjs.set_missing_handler handle_missing_substobjs + + + +(** {6 From module expression to substitutive objects} *) + +(** Turn a chain of [MSEapply] into the head ModPath.t and the + list of ModPath.t parameters (deepest param coming first). + The left part of a [MSEapply] must be either [MSEident] or + another [MSEapply]. *) + +let get_applications mexpr = + let rec get params = function + | MEident mp -> mp, params + | MEapply (fexpr, mp) -> get (mp::params) fexpr + | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") + in get [] mexpr + +(** Create the substitution corresponding to some functor applications *) + +let rec compute_subst env mbids sign mp_l inl = + match mbids,mp_l with + | _,[] -> mbids,empty_subst + | [],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 + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = + if Modops.is_functor mb.mod_type then empty_delta_resolver + else + Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta + in + mbid_left,join (map_mbid mbid mp resolver) subst + +(** Create the objects of a "with Module" structure. *) + +let rec replace_module_object idl mp0 objs0 mp1 objs1 = + match idl, objs0 with + | _,[] -> [] + | id::idl,(id',obj)::tail when Id.equal id id' -> + assert (String.equal (object_tag obj) "MODULE"); + let mp_id = MPdot(mp0, Label.of_id id) in + let objs = match idl with + | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 + | _ -> + let objs_id = expand_sobjs (out_module obj) in + replace_module_object idl mp_id objs_id mp1 objs1 + in + (id, in_module ([], Objs objs))::tail + | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1 + +let type_of_mod mp env = function + |true -> (Environ.lookup_module mp env).mod_type + |false -> (Environ.lookup_modtype mp env).mod_type + +let rec get_module_path = function + |MEident mp -> mp + |MEwith (me,_) -> get_module_path me + |MEapply (me,_) -> get_module_path me + +(** Substitutive objects of a module expression (or module type) *) + +let rec get_module_sobjs is_mod env inl = function + |MEident mp -> + begin match ModSubstObjs.get mp with + |(mbids,Objs _) when not (ModPath.is_bound mp) -> + (mbids,Ref (mp, empty_subst)) (* we create an alias *) + |sobjs -> sobjs + end + |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty + |MEwith (mty, WithMod (idl,mp1)) -> + assert (not is_mod); + let sobjs0 = get_module_sobjs is_mod env inl mty in + assert (sobjs_no_functor sobjs0); + (* For now, we expanse everything, to be safe *) + let mp0 = get_module_path mty in + let objs0 = expand_sobjs sobjs0 in + let objs1 = expand_sobjs (ModSubstObjs.get mp1) in + ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) + |MEapply _ as me -> + let mp1, mp_l = get_applications me in + let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in + let typ = type_of_mod mp1 env is_mod in + let mbids_left,subst = compute_subst env mbids typ mp_l inl in + (mbids_left, subst_aobjs subst aobjs) + +let get_functor_sobjs is_mod env inl (params,mexpr) = + let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in + (List.map fst params @ mbids, aobjs) + + +(** {6 Handling of module parameters} *) + +(** For printing modules, [process_module_binding] adds names of + bound module (and its components) to Nametab. It also loads + objects associated to it. *) + +let process_module_binding mbid me = + let dir = DirPath.make [MBId.to_id mbid] in + let mp = MPbound mbid in + let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in + let subst = map_mp (get_module_path me) mp empty_delta_resolver in + let sobjs = subst_sobjs subst sobjs in + do_module false Lib.load_objects 1 dir mp sobjs [] + +(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ) + i.e. possibly multiple names with the same module type. + Global environment is updated on the fly. + Objects in these parameters are also loaded. + Output is accumulated on top of [acc] (in reverse order). *) + +let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = + let inl = inl2intopt ann in + let lib_dir = Lib.library_dp() in + let env = Global.env() in + let (mty, _, cst') = interp_modast env ModType typ in + let () = Global.push_context_set true cst' in + let env = Global.env () in + let sobjs = get_module_sobjs false env inl mty in + let mp0 = get_module_path mty in + let fold acc {CAst.v=id} = + let dir = DirPath.make [id] in + let mbid = MBId.make lib_dir id in + let mp = MPbound mbid in + let resolver = Global.add_module_parameter mbid mty inl in + let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in + do_module false Lib.load_objects 1 dir mp sobjs []; + (mbid,mty,inl)::acc + in + let acc = List.fold_left fold acc idl in + (acc, Univ.ContextSet.union cst cst') + +(** Process a list of declarations of functor parameters + (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk) + Global environment is updated on the fly. + The calls to [interp_modast] should be interleaved with these + env updates, otherwise some "with Definition" could be rejected. + Returns a list of mbids and entries (in reversed order). + + This used to be a [List.concat (List.map ...)], but this should + be more efficient and independent of [List.map] eval order. +*) + +let intern_args interp_modast params = + List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params + + +(** {6 Auxiliary functions concerning subtyping checks} *) + +let check_sub mtb sub_mtb_l = + (* The constraints are checked and forgot immediately : *) + ignore (List.fold_right + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) + +(** This function checks if the type calculated for the module [mp] is + a subtype of all signatures in [sub_mtb_l]. Uses only the global + environment. *) + +let check_subtypes mp sub_mtb_l = + let mb = + try Global.lookup_module mp with Not_found -> assert false + in + let mtb = Modops.module_type_of_module mb in + check_sub mtb sub_mtb_l + +(** Same for module type [mp] *) + +let check_subtypes_mt mp sub_mtb_l = + let mtb = + try Global.lookup_modtype mp with Not_found -> assert false + in + check_sub mtb sub_mtb_l + +(** Create a params entry. + In [args], the youngest module param now comes first. *) + +let mk_params_entry args = + List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args + +(** Create a functor type struct. + In [args], the youngest module param now comes first. *) + +let mk_funct_type env args seb0 = + List.fold_left + (fun seb (arg_id,arg_t,arg_inl) -> + let mp = MPbound arg_id in + let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in + MoreFunctor(arg_id,arg_t,seb)) + seb0 args + +(** Prepare the module type list for check of subtypes *) + +let build_subtypes interp_modast env mp args mtys = + let (cst, ans) = List.fold_left_map + (fun cst (m,ann) -> + let inl = inl2intopt ann in + let mte, _, cst' = interp_modast env ModType m in + let env = Environ.push_context_set ~strict:true cst' env in + let cst = Univ.ContextSet.union cst cst' in + let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in + cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) + Univ.ContextSet.empty mtys + in + (ans, cst) + + +(** {6 Current module information} + + This information is stored by each [start_module] for use + in a later [end_module]. *) + +type current_module_info = { + cur_typ : (module_struct_entry * int option) option; (** type via ":" *) + cur_typs : module_type_body list (** types via "<:" *) +} + +let default_module_info = { cur_typ = None; cur_typs = [] } + +let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" + + +(** {6 Current module type information} + + This information is stored by each [start_modtype] for use + in a later [end_modtype]. *) + +let openmodtype_info = + Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" + + +(** {6 Modules : start, end, declare} *) + +module RawModOps = struct + +let start_module interp_modast export id args res fs = + let mp = Global.start_module id in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in + let env = Global.env () in + let res_entry_o, subtyps, cst = match res with + | Enforce (res,ann) -> + let inl = inl2intopt ann in + let (mte, _, cst) = interp_modast env ModType res in + let env = Environ.push_context_set ~strict:true cst env in + (* We check immediately that mte is well-formed *) + let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some (mte, inl), [], cst + | Check resl -> + let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + None, typs, cst + in + let () = Global.push_context_set true cst in + openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; + let prefix = Lib.start_module export id mp fs in + Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); + mp + +let end_module () = + let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in + let substitute, keep, special = Lib.classify_segment lib_stack in + let m_info = !openmod_info in + + (* For sealed modules, we use the substitutive objects of their signatures *) + let sobjs0, keep, special = match m_info.cur_typ with + | None -> ([], Objs substitute), keep, special + | Some (mty, inline) -> + get_module_sobjs false (Global.env()) inline mty, [], [] + in + let id = basename (fst oldoname) in + let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in + let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in + + check_subtypes mp m_info.cur_typs; + + (* We substitute objects if the module is sealed by a signature *) + let sobjs = + match m_info.cur_typ with + | None -> sobjs + | Some (mty, _) -> + subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs + in + let node = in_module sobjs in + (* We add the keep objects, if any, and if this isn't a functor *) + let objects = match keep, mbids with + | [], _ | _, _ :: _ -> special@[node] + | _ -> special@[node;in_modkeep keep] + in + let newoname = Lib.add_leaves id objects in + + (* Name consistency check : start_ vs. end_module, kernel vs. library *) + assert (eq_full_path (fst newoname) (fst oldoname)); + assert (ModPath.equal (mp_of_kn (snd newoname)) mp); + + mp + +let declare_module interp_modast id args res mexpr_o fs = + (* We simulate the beginning of an interactive module, + then we adds the module parameters to the global env. *) + let mp = Global.start_module id in + let arg_entries_r, cst = intern_args interp_modast args in + let params = mk_params_entry arg_entries_r in + let env = Global.env () in + let env = Environ.push_context_set ~strict:true cst env in + let mty_entry_o, subs, inl_res, cst' = match res with + | Enforce (mty,ann) -> + let inl = inl2intopt ann in + let (mte, _, cst) = interp_modast env ModType mty in + let env = Environ.push_context_set ~strict:true cst env in + (* We check immediately that mte is well-formed *) + let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in + let cst = Univ.ContextSet.union cst cst' in + Some mte, [], inl, cst + | Check mtys -> + let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + None, typs, default_inline (), cst + in + let env = Environ.push_context_set ~strict:true cst' env in + let cst = Univ.ContextSet.union cst cst' in + let mexpr_entry_o, inl_expr, cst' = match mexpr_o with + | None -> None, default_inline (), Univ.ContextSet.empty + | Some (mexpr,ann) -> + let (mte, _, cst) = interp_modast env Module mexpr in + Some mte, inl2intopt ann, cst + in + let env = Environ.push_context_set ~strict:true cst' env in + let cst = Univ.ContextSet.union cst cst' in + let entry = match mexpr_entry_o, mty_entry_o with + | None, None -> assert false (* No body, no type ... *) + | None, Some typ -> MType (params, typ) + | Some body, otyp -> MExpr (params, body, otyp) + in + let sobjs, mp0 = match entry with + | MType (_,mte) | MExpr (_,_,Some mte) -> + get_functor_sobjs false env inl_res (params,mte), get_module_path mte + | MExpr (_,me,None) -> + get_functor_sobjs true env inl_expr (params,me), get_module_path me + in + (* Undo the simulated interactive building of the module + and declare the module as a whole *) + Summary.unfreeze_summaries fs; + let inl = match inl_expr with + | None -> None + | _ -> inl_res + in + let () = Global.push_context_set true cst in + let mp_env,resolver = Global.add_module id entry inl in + + (* Name consistency check : kernel vs. library *) + assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id))); + assert (ModPath.equal mp mp_env); + + check_subtypes mp subs; + + let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in + ignore (Lib.add_leaf id (in_module sobjs)); + mp + +end + +(** {6 Module types : start, end, declare} *) + +module RawModTypeOps = struct + +let start_modtype interp_modast id args mtys fs = + let mp = Global.start_modtype id in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in + let env = Global.env () in + let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let () = Global.push_context_set true cst in + openmodtype_info := sub_mty_l; + let prefix = Lib.start_modtype id mp fs in + Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); + mp + +let end_modtype () = + let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in + let id = basename (fst oldoname) in + let substitute, _, special = Lib.classify_segment lib_stack in + let sub_mty_l = !openmodtype_info in + let mp, mbids = Global.end_modtype fs id in + let modtypeobjs = (mbids, Objs substitute) in + check_subtypes_mt mp sub_mty_l; + let oname = Lib.add_leaves id (special@[in_modtype modtypeobjs]) + in + (* Check name consistence : start_ vs. end_modtype, kernel vs. library *) + assert (eq_full_path (fst oname) (fst oldoname)); + assert (ModPath.equal (mp_of_kn (snd oname)) mp); + + mp + +let declare_modtype interp_modast id args mtys (mty,ann) fs = + let inl = inl2intopt ann in + (* We simulate the beginning of an interactive module, + then we adds the module parameters to the global env. *) + let mp = Global.start_modtype id in + let arg_entries_r, cst = intern_args interp_modast args in + let () = Global.push_context_set true cst in + let params = mk_params_entry arg_entries_r in + let env = Global.env () in + let mte, _, cst = interp_modast env ModType mty in + let () = Global.push_context_set true cst in + let env = Global.env () in + (* We check immediately that mte is well-formed *) + let _, _, _, cst = Mod_typing.translate_mse env None inl mte in + let () = Global.push_context_set true cst in + let env = Global.env () in + let entry = params, mte in + let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let () = Global.push_context_set true cst in + let env = Global.env () in + let sobjs = get_functor_sobjs false env inl entry in + let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in + let sobjs = subst_sobjs subst sobjs in + + (* Undo the simulated interactive building of the module type + and declare the module type as a whole *) + Summary.unfreeze_summaries fs; + + (* We enrich the global environment *) + let mp_env = Global.add_modtype id entry inl in + + (* Name consistency check : kernel vs. library *) + assert (ModPath.equal mp_env mp); + + (* Subtyping checks *) + check_subtypes_mt mp sub_mty_l; + + ignore (Lib.add_leaf id (in_modtype sobjs)); + mp + +end + +(** {6 Include} *) + +module RawIncludeOps = struct + +let rec include_subst env mp reso mbids sign inline = match mbids with + | [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let subst = include_subst env mp reso mbids fbody_b inline in + let mp_delta = + Modops.inline_delta_resolver env inline mp farg_id farg_b reso + in + join (map_mbid mbid mp mp_delta) subst + +let rec decompose_functor mpl typ = + match mpl, typ with + | [], _ -> typ + | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str + | _ -> user_err Pp.(str "Application of a functor with too much arguments.") + +exception NoIncludeSelf + +let type_of_incl env is_mod = function + |MEident mp -> type_of_mod mp env is_mod + |MEapply _ as me -> + let mp0, mp_l = get_applications me in + decompose_functor mp_l (type_of_mod mp0 env is_mod) + |MEwith _ -> raise NoIncludeSelf + +let declare_one_include interp_modast (me_ast,annot) = + let env = Global.env() in + let me, kind, cst = interp_modast env ModAny me_ast in + let () = Global.push_context_set true cst in + let env = Global.env () in + let is_mod = (kind == Module) in + let cur_mp = Lib.current_mp () in + let inl = inl2intopt annot in + let mbids,aobjs = get_module_sobjs is_mod env inl me in + let subst_self = + try + if List.is_empty mbids then raise NoIncludeSelf; + let typ = type_of_incl env is_mod me in + let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in + include_subst env cur_mp reso mbids typ inl + with NoIncludeSelf -> empty_subst + in + let base_mp = get_module_path me in + let resolver = Global.add_include me is_mod inl in + let subst = join subst_self (map_mp base_mp cur_mp resolver) in + let aobjs = subst_aobjs subst aobjs in + ignore (Lib.add_leaf (Lib.current_mod_id ()) (in_include aobjs)) + +let declare_include interp me_asts = + List.iter (declare_one_include interp) me_asts + +end + + +(** {6 Module operations handling summary freeze/unfreeze} *) + +let protect_summaries f = + let fs = Summary.freeze_summaries ~marshallable:false in + try f fs + with reraise -> + (* Something wrong: undo the whole process *) + let reraise = CErrors.push reraise in + let () = Summary.unfreeze_summaries fs in + iraise reraise + +let start_module interp export id args res = + protect_summaries (RawModOps.start_module interp export id args res) + +let end_module = RawModOps.end_module + +let declare_module interp id args mtys me_l = + let declare_me fs = match me_l with + | [] -> RawModOps.declare_module interp id args mtys None fs + | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | me_l -> + ignore (RawModOps.start_module interp None id args mtys fs); + RawIncludeOps.declare_include interp me_l; + RawModOps.end_module () + in + protect_summaries declare_me + +let start_modtype interp id args mtys = + protect_summaries (RawModTypeOps.start_modtype interp id args mtys) + +let end_modtype = RawModTypeOps.end_modtype + +let declare_modtype interp id args mtys mty_l = + let declare_mt fs = match mty_l with + | [] -> assert false + | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | mty_l -> + ignore (RawModTypeOps.start_modtype interp id args mtys fs); + RawIncludeOps.declare_include interp mty_l; + RawModTypeOps.end_modtype () + in + protect_summaries declare_mt + +let declare_include interp me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) + + +(** {6 Libraries} *) + +type library_name = DirPath.t + +(** A library object is made of some substitutive objects + and some "keep" objects. *) + +type library_objects = Lib.lib_objects * Lib.lib_objects + +(** For the native compiler, we cache the library values *) + +let register_library dir cenv (objs:library_objects) digest univ = + let mp = MPfile dir in + let () = + try + (* Is this library already loaded ? *) + ignore(Global.lookup_module mp); + with Not_found -> + (* 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."); + in + let sobjs,keepobjs = objs in + do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs + +let get_library_native_symbols dir = + Safe_typing.get_library_native_symbols (Global.safe_env ()) dir + +let start_library dir = + let mp = Global.start_library dir in + openmod_info := default_module_info; + Lib.start_compilation dir mp + +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + +let end_library ?except dir = + !end_library_hook(); + let oname = Lib.end_compilation_checks dir in + let mp,cenv,ast = Global.export ?except dir in + let prefix, lib_stack = Lib.end_compilation oname in + assert (ModPath.equal mp (MPfile dir)); + let substitute, keep, _ = Lib.classify_segment lib_stack in + cenv,(substitute,keep),ast + + + +(** {6 Implementation of Import and Export commands} *) + +let really_import_module mp = + (* May raise Not_found for unknown module and for functors *) + let prefix,sobjs,keepobjs = ModObjs.get mp in + Lib.open_objects 1 prefix sobjs; + Lib.open_objects 1 prefix keepobjs + +let cache_import (_,(_,mp)) = really_import_module mp + +let open_import i obj = + if Int.equal i 1 then cache_import obj + +let classify_import (export,_ as obj) = + if export then Substitute obj else Dispose + +let subst_import (subst,(export,mp as obj)) = + let mp' = subst_mp subst mp in + if mp'==mp then obj else (export,mp') + +let in_import : bool * ModPath.t -> obj = + declare_object {(default_object "IMPORT MODULE") with + cache_function = cache_import; + open_function = open_import; + subst_function = subst_import; + classify_function = classify_import } + +let import_module export mp = + Lib.add_anonymous_leaf (in_import (export,mp)) + + +(** {6 Iterators} *) + +let iter_all_segments f = + let rec apply_obj prefix (id,obj) = match object_tag obj with + | "INCLUDE" -> + let objs = expand_aobjs (out_include obj) in + List.iter (apply_obj prefix) objs + | _ -> f (Lib.make_oname prefix id) obj + in + let apply_mod_obj _ (prefix,substobjs,keepobjs) = + List.iter (apply_obj prefix) substobjs; + List.iter (apply_obj prefix) keepobjs + in + let apply_node = function + | sp, Lib.Leaf o -> f sp o + | _ -> () + in + MPmap.iter apply_mod_obj (ModObjs.all ()); + List.iter apply_node (Lib.contents ()) + + +(** {6 Some types used to shorten declaremods.mli} *) + +type 'modast module_interpretor = + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t + +type 'modast module_params = + (lident list * ('modast * inline)) list + +(** {6 Debug} *) + +let debug_print_modtab _ = + let pr_seg = function + | [] -> str "[]" + | l -> str "[." ++ int (List.length l) ++ str ".]" + in + let pr_modinfo mp (prefix,substobjs,keepobjs) s = + s ++ str (ModPath.to_string mp) ++ (spc ()) + ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs))) + in + let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in + hov 0 modules diff --git a/library/declaremods.mli b/library/declaremods.mli new file mode 100644 index 0000000000..7aa4bc30ce --- /dev/null +++ b/library/declaremods.mli @@ -0,0 +1,144 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** {6 Modules } *) + +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + +(** Kinds of modules *) + +type module_kind = Module | ModType | ModAny + +type 'modast module_interpretor = + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t + +type 'modast module_params = + (lident list * ('modast * inline)) list + +(** [declare_module interp_modast id fargs typ exprs] + declares module [id], with structure constructed by [interp_modast] + from functor arguments [fargs], with final type [typ]. + [exprs] is usually of length 1 (Module definition with a concrete + body), but it could also be empty ("Declare Module", with non-empty [typ]), + or multiple (body of the shape M <+ N <+ ...). *) + +val declare_module : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) module_signature -> + ('modast * inline) list -> ModPath.t + +val start_module : + 'modast module_interpretor -> + bool option -> Id.t -> + 'modast module_params -> + ('modast * inline) module_signature -> ModPath.t + +val end_module : unit -> ModPath.t + + + +(** {6 Module types } *) + +(** [declare_modtype interp_modast id fargs typs exprs] + Similar to [declare_module], except that the types could be multiple *) + +val declare_modtype : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) list -> + ('modast * inline) list -> + ModPath.t + +val start_modtype : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> + ('modast * inline) list -> ModPath.t + +val end_modtype : unit -> ModPath.t + +(** {6 Libraries i.e. modules on disk } *) + +type library_name = DirPath.t + +type library_objects + +val register_library : + library_name -> + Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> + Univ.ContextSet.t -> unit + +val get_library_native_symbols : library_name -> Nativecode.symbols + +val start_library : library_name -> unit + +val end_library : + ?except:Future.UUIDSet.t -> library_name -> + Safe_typing.compiled_library * library_objects * Safe_typing.native_library + +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + +(** [really_import_module mp] opens the module [mp] (in a Caml sense). + It modifies Nametab and performs the [open_object] function for + every object of the module. Raises [Not_found] when [mp] is unknown + or when [mp] corresponds to a functor. *) + +val really_import_module : ModPath.t -> unit + +(** [import_module export mp] is a synchronous version of + [really_import_module]. If [export] is [true], the module is also + opened every time the module containing it is. *) + +val import_module : bool -> ModPath.t -> unit + +(** Include *) + +val declare_include : + 'modast module_interpretor -> ('modast * inline) list -> unit + +(** {6 ... } *) +(** [iter_all_segments] iterate over all segments, the modules' + segments first and then the current segment. Modules are presented + in an arbitrary order. The given function is applied to all leaves + (together with their section path). *) + +val iter_all_segments : + (Libobject.object_name -> Libobject.obj -> unit) -> unit + + +val debug_print_modtab : unit -> Pp.t + +(** For printing modules, [process_module_binding] adds names of + bound module (and its components) to Nametab. It also loads + objects associated to it. It may raise a [Failure] when the + bound module hasn't an atomic type. *) + +val process_module_binding : + MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/decls.ml b/library/decls.ml new file mode 100644 index 0000000000..b766b6e2cb --- /dev/null +++ b/library/decls.ml @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module registers tables for some non-logical informations + associated declarations *) + +open Names +open Decl_kinds +open Libnames + +(** Datas associated to section variables and local definitions *) + +type variable_data = + DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind + +let vartab = + Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" + +let add_variable_data id o = vartab := Id.Map.add id o !vartab + +let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq +let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k +let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx +let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p + +let variable_secpath id = + let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in + make_qualid dir id + +let variable_exists id = Id.Map.mem id !vartab + +(** Datas associated to global parameters and constants *) + +let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" + +let add_constant_kind kn k = csttab := Cmap.add kn k !csttab + +let constant_kind kn = Cmap.find kn !csttab diff --git a/library/decls.mli b/library/decls.mli new file mode 100644 index 0000000000..c0db537427 --- /dev/null +++ b/library/decls.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames +open Decl_kinds + +(** This module manages non-kernel informations about declarations. It + is either non-logical informations or logical informations that + have no place to be (yet) in the kernel *) + +(** Registration and access to the table of variable *) + +type variable_data = + DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind + +val add_variable_data : variable -> variable_data -> unit +val variable_path : variable -> DirPath.t +val variable_secpath : variable -> qualid +val variable_kind : variable -> logical_kind +val variable_opacity : variable -> bool +val variable_context : variable -> Univ.ContextSet.t +val variable_polymorphic : variable -> polymorphic +val variable_exists : variable -> bool + +(** Registration and access to the table of constants *) + +val add_constant_kind : Constant.t -> logical_kind -> unit +val constant_kind : Constant.t -> logical_kind diff --git a/library/doc.tex b/library/doc.tex new file mode 100644 index 0000000000..33af59336c --- /dev/null +++ b/library/doc.tex @@ -0,0 +1,16 @@ + +\newpage +\section*{The Coq library} + +\ocwsection \label{library} +This chapter describes the \Coq\ library, which is made of two parts: +\begin{itemize} + \item a general mechanism to keep a trace of all operations and of + the state of the system, with backtrack capabilities; + \item a global environment for the CCI, with functions to export and + import compiled modules. +\end{itemize} +The modules of the library are organized as follows. + +\bigskip +\begin{center}\epsfig{file=library.dep.ps}\end{center} diff --git a/library/dune b/library/dune new file mode 100644 index 0000000000..344fad5a75 --- /dev/null +++ b/library/dune @@ -0,0 +1,9 @@ +(library + (name library) + (synopsis "Coq's Loadable Libraries (vo) Support") + (public_name coq.library) + (wrapped false) + (libraries kernel)) + +(documentation + (package coq)) diff --git a/library/global.ml b/library/global.ml new file mode 100644 index 0000000000..84d2a37170 --- /dev/null +++ b/library/global.ml @@ -0,0 +1,191 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Environ + +(** We introduce here the global environment of the system, + and we declare it as a synchronized table. *) + +let global_env_summary_name = "Global environment" + +module GlobalSafeEnv : sig + + val safe_env : unit -> Safe_typing.safe_environment + val set_safe_env : Safe_typing.safe_environment -> unit + val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit + val is_joined_environment : unit -> bool + val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag + +end = struct + +let global_env = ref Safe_typing.empty_environment + +let join_safe_environment ?except () = + global_env := Safe_typing.join_safe_environment ?except !global_env + +let is_joined_environment () = + Safe_typing.is_joined_environment !global_env + +let global_env_summary_tag = + Summary.declare_summary_tag global_env_summary_name + { Summary.freeze_function = (fun ~marshallable -> if marshallable then + (join_safe_environment (); !global_env) + else !global_env); + unfreeze_function = (fun fr -> global_env := fr); + init_function = (fun () -> global_env := Safe_typing.empty_environment) } + +let assert_not_parsing () = + if !Flags.we_are_parsing then + CErrors.anomaly ( + Pp.strbrk"The global environment cannot be accessed during parsing.") + +let safe_env () = assert_not_parsing(); !global_env + +let set_safe_env e = global_env := e + +end + +let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag + +let safe_env = GlobalSafeEnv.safe_env +let join_safe_environment ?except () = + GlobalSafeEnv.join_safe_environment ?except () +let is_joined_environment = GlobalSafeEnv.is_joined_environment + +let env () = Safe_typing.env_of_safe_env (safe_env ()) + +let env_is_initial () = Safe_typing.is_initial (safe_env ()) + +(** Turn ops over the safe_environment state monad to ops on the global env *) + +let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) + +let globalize f = + let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res + +let globalize_with_summary fs f = + let res,env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env; + res + +(** [Safe_typing] operations, now operating on the global environment *) + +let i2l = Label.of_id + +let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) + +let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) +let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let typing_flags () = Environ.typing_flags (env ()) +let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) +let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d) +let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) +let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) +let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) +let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) + +let start_module id = globalize (Safe_typing.start_module (i2l id)) +let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) + +let end_module fs id mtyo = + globalize_with_summary fs (Safe_typing.end_module (i2l id) mtyo) + +let end_modtype fs id = + globalize_with_summary fs (Safe_typing.end_modtype (i2l id)) + +let add_module_parameter mbid mte inl = + globalize (Safe_typing.add_module_parameter mbid mte inl) + +(** Queries on the global environment *) + +let universes () = universes (env()) +let named_context () = named_context (env()) +let named_context_val () = named_context_val (env()) + +let lookup_named id = lookup_named id (env()) +let lookup_constant kn = lookup_constant kn (env()) +let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind +let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind +let lookup_mind kn = lookup_mind kn (env()) + +let lookup_module mp = lookup_module mp (env()) +let lookup_modtype kn = lookup_modtype kn (env()) + +let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) + +let opaque_tables () = Environ.opaque_tables (env ()) + +let body_of_constant_body ce = body_of_constant_body (env ()) ce + +let body_of_constant cst = body_of_constant_body (lookup_constant cst) + +(** Operations on kernel names *) + +let constant_of_delta_kn kn = + Safe_typing.constant_of_delta_kn_senv (safe_env ()) kn + +let mind_of_delta_kn kn = + Safe_typing.mind_of_delta_kn_senv (safe_env ()) kn + +(** Operations on libraries *) + +let start_library dir = globalize (Safe_typing.start_library dir) +let export ?except s = Safe_typing.export ?except (safe_env ()) s +let import c u d = globalize (Safe_typing.import c u d) + + +(** Function to get an environment from the constants part of the global + environment and a given context. *) + +let env_of_context hyps = + reset_with_named_context hyps (env()) + +let constr_of_global_in_context = Typeops.constr_of_global_in_context +let type_of_global_in_context = Typeops.type_of_global_in_context + +let universes_of_global gr = + universes_of_global (env ()) gr + +let is_polymorphic r = Environ.is_polymorphic (env()) r + +let is_template_polymorphic r = is_template_polymorphic (env ()) r + +let is_type_in_type r = is_type_in_type (env ()) r + +let current_modpath () = + Safe_typing.current_modpath (safe_env ()) + +let current_dirpath () = + Safe_typing.current_dirpath (safe_env ()) + +let with_global f = + let (a, ctx) = f (env ()) (current_dirpath ()) in + push_context_set false ctx; a + +(* spiwack: register/unregister functions for retroknowledge *) +let register field value = + globalize0 (Safe_typing.register field value) + +let register_inline c = globalize0 (Safe_typing.register_inline c) + +let set_strategy k l = + globalize0 (Safe_typing.set_strategy k l) + +let set_share_reduction b = + globalize0 (Safe_typing.set_share_reduction b) + +let set_VM b = globalize0 (Safe_typing.set_VM b) +let set_native_compiler b = globalize0 (Safe_typing.set_native_compiler b) diff --git a/library/global.mli b/library/global.mli new file mode 100644 index 0000000000..40962e21af --- /dev/null +++ b/library/global.mli @@ -0,0 +1,169 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** This module defines the global environment of Coq. The functions + below are exactly the same as the ones in [Safe_typing], operating on + that global environment. [add_*] functions perform name verification, + i.e. check that the name given as argument match those provided by + [Safe_typing]. *) + +val safe_env : unit -> Safe_typing.safe_environment +val env : unit -> Environ.env + +val env_is_initial : unit -> bool + +val universes : unit -> UGraph.t +val named_context_val : unit -> Environ.named_context_val +val named_context : unit -> Constr.named_context + +(** {6 Enriching the global environment } *) + +(** Changing the (im)predicativity of the system *) +val set_engagement : Declarations.engagement -> unit +val set_indices_matter : bool -> unit +val set_typing_flags : Declarations.typing_flags -> unit +val typing_flags : unit -> Declarations.typing_flags + +(** Variables, Local definitions, constants, inductive types *) + +val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Entries.section_def_entry) -> unit + +val export_private_constants : in_section:bool -> + Safe_typing.private_constants Entries.definition_entry -> + unit Entries.definition_entry * Safe_typing.exported_private_constant list + +val add_constant : + in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t +val add_mind : + Id.t -> Entries.mutual_inductive_entry -> MutInd.t + +(** Extra universe constraints *) +val add_constraints : Univ.Constraint.t -> unit + +val push_context_set : bool -> Univ.ContextSet.t -> unit + +(** Non-interactive modules and module types *) + +val add_module : + Id.t -> Entries.module_entry -> Declarations.inline -> + ModPath.t * Mod_subst.delta_resolver +val add_modtype : + Id.t -> Entries.module_type_entry -> Declarations.inline -> ModPath.t +val add_include : + Entries.module_struct_entry -> bool -> Declarations.inline -> + Mod_subst.delta_resolver + +(** Interactive modules and module types *) + +val start_module : Id.t -> ModPath.t +val start_modtype : Id.t -> ModPath.t + +val end_module : Summary.frozen -> Id.t -> + (Entries.module_struct_entry * Declarations.inline) option -> + ModPath.t * MBId.t list * Mod_subst.delta_resolver + +val end_modtype : Summary.frozen -> Id.t -> ModPath.t * MBId.t list + +val add_module_parameter : + MBId.t -> Entries.module_struct_entry -> Declarations.inline -> + Mod_subst.delta_resolver + +(** {6 Queries in the global environment } *) + +val lookup_named : variable -> Constr.named_declaration +val lookup_constant : Constant.t -> Declarations.constant_body +val lookup_inductive : inductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_pinductive : Constr.pinductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_mind : MutInd.t -> Declarations.mutual_inductive_body +val lookup_module : ModPath.t -> Declarations.module_body +val lookup_modtype : ModPath.t -> Declarations.module_type_body +val exists_objlabel : Label.t -> bool + +val constant_of_delta_kn : KerName.t -> Constant.t +val mind_of_delta_kn : KerName.t -> MutInd.t + +val opaque_tables : unit -> Opaqueproof.opaquetab + +val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) + +val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) + +(** {6 Compiled libraries } *) + +val start_library : DirPath.t -> ModPath.t +val export : ?except:Future.UUIDSet.t -> DirPath.t -> + ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library +val import : + Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> + ModPath.t + +(** {6 Misc } *) + +(** Function to get an environment from the constants part of the global + * environment and a given context. *) + +val env_of_context : Environ.named_context_val -> Environ.env + +val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit +val is_joined_environment : unit -> bool + +val is_polymorphic : GlobRef.t -> bool +val is_template_polymorphic : GlobRef.t -> bool +val is_type_in_type : GlobRef.t -> bool + +val constr_of_global_in_context : Environ.env -> + GlobRef.t -> Constr.types * Univ.AUContext.t + [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"] + +val type_of_global_in_context : Environ.env -> + GlobRef.t -> Constr.types * Univ.AUContext.t + [@@ocaml.deprecated "alias of [Typeops.type_of_global]"] + +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) +val universes_of_global : GlobRef.t -> Univ.AUContext.t +[@@ocaml.deprecated "Use [Environ.universes_of_global]"] + +(** {6 Retroknowledge } *) + +val register : + Retroknowledge.field -> GlobRef.t -> unit + +val register_inline : Constant.t -> unit + +(** {6 Oracle } *) + +val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit + +(** {6 Conversion settings } *) + +val set_share_reduction : bool -> unit + +val set_VM : bool -> unit +val set_native_compiler : bool -> unit + +(* Modifies the global state, registering new universes *) + +val current_modpath : unit -> ModPath.t + +val current_dirpath : unit -> DirPath.t + +val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a + +val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag diff --git a/library/globnames.ml b/library/globnames.ml new file mode 100644 index 0000000000..db2e8bfaed --- /dev/null +++ b/library/globnames.ml @@ -0,0 +1,139 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Constr +open Mod_subst + +(*s Global reference is a kernel side type for all references together *) +type global_reference = GlobRef.t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + +let isVarRef = function VarRef _ -> true | _ -> false +let isConstRef = function ConstRef _ -> true | _ -> false +let isIndRef = function IndRef _ -> true | _ -> false +let isConstructRef = function ConstructRef _ -> true | _ -> false + +let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" +let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" +let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" +let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" + +let subst_constructor subst (ind,j as ref) = + let ind' = subst_ind subst ind in + if ind==ind' then ref + else (ind',j) + +let subst_global_reference subst ref = match ref with + | VarRef var -> ref + | ConstRef kn -> + let kn' = subst_constant subst kn in + if kn==kn' then ref else ConstRef kn' + | IndRef ind -> + let ind' = subst_ind subst ind in + if ind==ind' then ref else IndRef ind' + | ConstructRef ((kn,i),j as c) -> + let c' = subst_constructor subst c in + if c'==c then ref else ConstructRef c' + +let subst_global subst ref = match ref with + | VarRef var -> ref, None + | ConstRef kn -> + let kn',t = subst_con subst kn in + if kn==kn' then ref, None else ConstRef kn', t + | IndRef ind -> + let ind' = subst_ind subst ind in + if ind==ind' then ref, None else IndRef ind', None + | ConstructRef ((kn,i),j as c) -> + let c' = subst_constructor subst c in + if c'==c then ref,None else ConstructRef c', None + +let canonical_gr = function + | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con)) + | IndRef (kn,i) -> IndRef(MutInd.make1(MutInd.canonical kn),i) + | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j) + | VarRef id -> VarRef id + +let global_of_constr c = match kind c with + | Const (sp,u) -> ConstRef sp + | Ind (ind_sp,u) -> IndRef ind_sp + | Construct (cstr_cp,u) -> ConstructRef cstr_cp + | Var id -> VarRef id + | _ -> raise Not_found + +let is_global c t = + match c, kind t with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + +let printable_constr_of_global = function + | VarRef id -> mkVar id + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkConstruct sp + | IndRef sp -> mkInd sp + +module RefOrdered = Names.GlobRef.Ordered +module RefOrdered_env = Names.GlobRef.Ordered_env + +module Refmap = Names.GlobRef.Map +module Refset = Names.GlobRef.Set + +module Refmap_env = Names.GlobRef.Map_env +module Refset_env = Names.GlobRef.Set_env + +(* Extended global references *) + +type syndef_name = KerName.t + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + +(* We order [extended_global_reference] via their user part + (cf. pretty printer) *) + +module ExtRefOrdered = struct + type t = extended_global_reference + + let equal x y = + x == y || + match x, y with + | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry + | SynDef knx, SynDef kny -> KerName.equal knx kny + | (TrueGlobal _ | SynDef _), _ -> false + + let compare x y = + if x == y then 0 + else match x, y with + | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry + | SynDef knx, SynDef kny -> KerName.compare knx kny + | TrueGlobal _, SynDef _ -> -1 + | SynDef _, TrueGlobal _ -> 1 + + open Hashset.Combine + + let hash = function + | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr) + | SynDef kn -> combinesmall 2 (KerName.hash kn) + +end + +type global_reference_or_constr = + | IsGlobal of global_reference + | IsConstr of constr + +(* Deprecated *) +let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli new file mode 100644 index 0000000000..d49ed453f5 --- /dev/null +++ b/library/globnames.mli @@ -0,0 +1,84 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Constr +open Mod_subst + +(** {6 Global reference is a kernel side type for all references together } *) +type global_reference = GlobRef.t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) +[@@ocaml.deprecated "Use Names.GlobRef.t"] + +val isVarRef : GlobRef.t -> bool +val isConstRef : GlobRef.t -> bool +val isIndRef : GlobRef.t -> bool +val isConstructRef : GlobRef.t -> bool + +val eq_gr : GlobRef.t -> GlobRef.t -> bool +[@@ocaml.deprecated "Use Names.GlobRef.equal"] +val canonical_gr : GlobRef.t -> GlobRef.t + +val destVarRef : GlobRef.t -> variable +val destConstRef : GlobRef.t -> Constant.t +val destIndRef : GlobRef.t -> inductive +val destConstructRef : GlobRef.t -> constructor + +val is_global : GlobRef.t -> constr -> bool + +val subst_constructor : substitution -> constructor -> constructor +val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option +val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t + +(** This constr is not safe to be typechecked, universe polymorphism is not + handled here: just use for printing *) +val printable_constr_of_global : GlobRef.t -> constr + +(** Turn a construction denoting a global reference into a global reference; + raise [Not_found] if not a global reference *) +val global_of_constr : constr -> GlobRef.t + +module RefOrdered = Names.GlobRef.Ordered +[@@ocaml.deprecated "Use Names.GlobRef.Ordered"] + +module RefOrdered_env = Names.GlobRef.Ordered_env +[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"] + +module Refset = Names.GlobRef.Set +[@@ocaml.deprecated "Use Names.GlobRef.Set"] +module Refmap = Names.GlobRef.Map +[@@ocaml.deprecated "Use Names.GlobRef.Map"] + +module Refset_env = GlobRef.Set_env +[@@ocaml.deprecated "Use Names.GlobRef.Set_env"] +module Refmap_env = GlobRef.Map_env +[@@ocaml.deprecated "Use Names.GlobRef.Map_env"] + +(** {6 Extended global references } *) + +type syndef_name = KerName.t + +type extended_global_reference = + | TrueGlobal of GlobRef.t + | SynDef of syndef_name + +module ExtRefOrdered : sig + type t = extended_global_reference + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int +end + +type global_reference_or_constr = + | IsGlobal of GlobRef.t + | IsConstr of constr diff --git a/library/goptions.ml b/library/goptions.ml new file mode 100644 index 0000000000..1b907fd966 --- /dev/null +++ b/library/goptions.ml @@ -0,0 +1,436 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This module manages customization parameters at the vernacular level *) + +open Pp +open CErrors +open Util +open Libobject +open Libnames +open Mod_subst + +type option_name = string list +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | StringOptValue of string option + +(** Summary of an option status *) +type option_state = { + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + +(****************************************************************************) +(* 0- Common things *) + +let nickname table = String.concat " " table + +let error_undeclared_key key = + user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") + +(****************************************************************************) +(* 1- Tables *) + +class type ['a] table_of_A = +object + method add : 'a -> unit + method remove : 'a -> unit + method mem : 'a -> unit + method print : unit +end + +module MakeTable = + functor + (A : sig + type t + type key + val compare : t -> t -> int + val table : (string * key table_of_A) list ref + val encode : key -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> + struct + type option_mark = + | GOadd + | GOrmv + + let nick = nickname A.key + + let _ = + if String.List.mem_assoc nick !A.table then + user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") + + module MySet = Set.Make (struct type t = A.t let compare = A.compare end) + + let t = Summary.ref MySet.empty ~name:nick + + let (add_option,remove_option) = + let cache_options (_,(f,p)) = match f with + | GOadd -> t := MySet.add p !t + | GOrmv -> t := MySet.remove p !t in + let load_options i o = if Int.equal i 1 then cache_options o in + let subst_options (subst,(f,p as obj)) = + let p' = A.subst subst p in + if p' == p then obj else + (f,p') + in + let inGo : option_mark * A.t -> obj = + Libobject.declare_object {(Libobject.default_object nick) with + Libobject.load_function = load_options; + Libobject.open_function = load_options; + Libobject.cache_function = cache_options; + Libobject.subst_function = subst_options; + Libobject.classify_function = (fun x -> Substitute x)} + in + ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), + (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) + + let print_table table_name printer table = + Feedback.msg_notice + (str table_name ++ + (hov 0 + (if MySet.is_empty table then str " None" ++ fnl () + else MySet.fold + (fun a b -> spc () ++ printer a ++ b) + table (mt ()) ++ str "." ++ fnl ()))) + + class table_of_A () = + object + method add x = add_option (A.encode x) + method remove x = remove_option (A.encode x) + method mem x = + let y = A.encode x in + let answer = MySet.mem y !t in + Feedback.msg_info (A.member_message y answer) + method print = print_table A.title A.printer !t + end + + let _ = A.table := (nick,new table_of_A ())::!A.table + let active c = MySet.mem c !t + let elements () = MySet.elements !t + end + +let string_table = ref [] + +let get_string_table k = String.List.assoc (nickname k) !string_table + +module type StringConvertArg = +sig + val key : option_name + val title : string + val member_message : string -> bool -> Pp.t +end + +module StringConvert = functor (A : StringConvertArg) -> +struct + type t = string + type key = string + let compare = String.compare + let table = string_table + let encode x = x + let subst _ x = x + let printer = str + let key = A.key + let title = A.title + let member_message = A.member_message +end + +module MakeStringTable = + functor (A : StringConvertArg) -> MakeTable (StringConvert(A)) + +let ref_table = ref [] + +let get_ref_table k = String.List.assoc (nickname k) !ref_table + +module type RefConvertArg = +sig + type t + val compare : t -> t -> int + val encode : qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t +end + +module RefConvert = functor (A : RefConvertArg) -> +struct + type t = A.t + type key = qualid + let compare = A.compare + let table = ref_table + let encode = A.encode + let subst = A.subst + let printer = A.printer + let key = A.key + let title = A.title + let member_message = A.member_message +end + +module MakeRefTable = + functor (A : RefConvertArg) -> MakeTable (RefConvert(A)) + +(****************************************************************************) +(* 2- Flags. *) + +type 'a option_sig = { + optdepr : bool; + optname : string; + optkey : option_name; + optread : unit -> 'a; + optwrite : 'a -> unit } + +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal + +type option_mod = OptSet | OptAppend + +module OptionOrd = +struct + type t = option_name + let compare opt1 opt2 = List.compare String.compare opt1 opt2 +end + +module OptionMap = Map.Make(OptionOrd) + +let value_tab = ref OptionMap.empty + +(* This raises Not_found if option of key [key] is unknown *) + +let get_option key = OptionMap.find key !value_tab + +let check_key key = try + let _ = get_option key in + user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.") +with Not_found -> + if String.List.mem_assoc (nickname key) !string_table + || String.List.mem_assoc (nickname key) !ref_table + then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.") + +open Libobject + +let warn_deprecated_option = + CWarnings.create ~name:"deprecated-option" ~category:"deprecated" + (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ + strbrk " is deprecated") + +let declare_option cast uncast append ?(preprocess = fun x -> x) + { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + check_key key; + let default = read() in + let change = + let _ = Summary.declare_summary (nickname key) + { Summary.freeze_function = (fun ~marshallable -> read ()); + Summary.unfreeze_function = write; + Summary.init_function = (fun () -> write default) } in + let cache_options (_,(l,m,v)) = + match m with + | OptSet -> write v + | OptAppend -> write (append (read ()) v) in + let load_options i (_, (l, _, _) as o) = match l with + | OptGlobal -> cache_options o + | OptExport -> () + | OptLocal | OptDefault -> + (* Ruled out by classify_function *) + assert false + in + let open_options i (_, (l, _, _) as o) = match l with + | OptExport -> if Int.equal i 1 then cache_options o + | OptGlobal -> () + | OptLocal | OptDefault -> + (* Ruled out by classify_function *) + assert false + in + let subst_options (subst,obj) = obj in + let discharge_options (_,(l,_,_ as o)) = + match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in + let classify_options (l,_,_ as o) = + match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in + let options : option_locality * option_mod * _ -> obj = + declare_object + { (default_object (nickname key)) with + load_function = load_options; + open_function = open_options; + cache_function = cache_options; + subst_function = subst_options; + discharge_function = discharge_options; + classify_function = classify_options } in + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) + 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, (cread,cwrite,cappend)) !value_tab + +let declare_int_option = + declare_option + (fun v -> IntValue v) + (function IntValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option = + declare_option + (fun v -> BoolValue v) + (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_string_option = + declare_option + (fun v -> StringValue v) + (function StringValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun x y -> x^","^y) +let declare_stringopt_option = + declare_option + (fun v -> StringOptValue v) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) + (fun _ _ -> anomaly (Pp.str "async_option.")) + +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + +(* 3- User accessible commands *) + +(* Setting values of options *) + +let warn_unknown_option = + CWarnings.create ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no option " ++ + str (nickname key) ++ str ".") + +let set_option_value ?(locality = OptDefault) 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)) -> + write locality (check_and_cast v (read ())) + +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") + +let check_int_value v = function + | IntValue _ -> IntValue v + | optv -> bad_type_error optv "int" + +let check_bool_value v = function + | BoolValue _ -> BoolValue v + | optv -> bad_type_error optv "bool" + +let check_string_value v = function + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) + | optv -> bad_type_error optv "string" + +let check_unset_value v = function + | BoolValue _ -> BoolValue false + | IntValue _ -> IntValue None + | StringOptValue _ -> StringOptValue None + | optv -> bad_type_error optv "nothing" + +(* Nota: For compatibility reasons, some errors are treated as + warning. This allows a script to refer to an option that doesn't + exist anymore *) + +let set_int_option_value_gen ?locality = + set_option_value ?locality check_int_value +let set_bool_option_value_gen ?locality key v = + set_option_value ?locality check_bool_value key v +let set_string_option_value_gen ?locality = + set_option_value ?locality check_string_value +let unset_option_value_gen ?locality key = + set_option_value ?locality check_unset_value key () + +let set_string_option_append_value_gen ?(locality = OptDefault) key v = + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (read,write,append)) -> + append locality (check_string_value v (read ())) + +let set_int_option_value opt v = set_int_option_value_gen opt v +let set_bool_option_value opt v = set_bool_option_value_gen opt v +let set_string_option_value opt v = set_string_option_value_gen opt v + +(* Printing options/tables *) + +let msg_option_value (name,v) = + match v with + | BoolValue true -> str "on" + | BoolValue false -> str "off" + | IntValue (Some n) -> int n + | IntValue None -> str "undefined" + | StringValue s -> quote (str s) + | StringOptValue None -> str"undefined" + | 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 s = read () in + match s with + | BoolValue b -> + Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + | _ -> + Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + +let get_tables () = + let tables = !value_tab in + let fold key (name, depr, (read,_,_)) accu = + let state = { + opt_name = name; + opt_depr = depr; + opt_value = read (); + } in + OptionMap.add key state accu + in + OptionMap.fold fold tables OptionMap.empty + +let print_tables () = + let print_option key name value depr = + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in + if depr then msg ++ str " [DEPRECATED]" ++ fnl () + else msg ++ fnl () + in + str "Options:" ++ fnl () ++ + OptionMap.fold + (fun key (name, depr, (read,_,_)) p -> + p ++ print_option key name (read ()) depr) + !value_tab (mt ()) ++ + str "Tables:" ++ fnl () ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) + !string_table (mt ()) ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) + !ref_table (mt ()) ++ + fnl () diff --git a/library/goptions.mli b/library/goptions.mli new file mode 100644 index 0000000000..b91553bf3c --- /dev/null +++ b/library/goptions.mli @@ -0,0 +1,185 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module manages customization parameters at the vernacular level *) + +(** Two kinds of things are managed : tables and options value + - Tables are created by applying the [MakeTable] functor. + - Variables storing options value are created by applying one of the + [declare_int_option], [declare_bool_option], ... functions. + + Each table/option is uniquely identified by a key of type [option_name] + which consists in a list of strings. Note that for parsing constraints, + table names must not be made of more than 2 strings while option names + can be of arbitrary length. + + The declaration of a table, say of name [["Toto";"Titi"]] + automatically makes available the following vernacular commands: + + Add Toto Titi foo. + Remove Toto Titi foo. + Print Toto Titi. + Test Toto Titi. + + The declaration of a non boolean option value, say of name + [["Tata";"Tutu";"Titi"]], automatically makes available the + following vernacular commands: + + Set Tata Tutu Titi val. + Print Table Tata Tutu Titi. + + If it is the declaration of a boolean value, the following + vernacular commands are made available: + + Set Tata Tutu Titi. + Unset Tata Tutu Titi. + Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) + + All options are synchronized with the document. +*) + +open Libnames +open Mod_subst + +type option_name = string list + +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal + +(** {6 Tables. } *) + +(** The functor [MakeStringTable] declares a table containing objects + of type [string]; the function [member_message] say what to print + when invoking the "Test Toto Titi foo." command; at the end [title] + is the table name printed when invoking the "Print Toto Titi." + command; [active] is roughly the internal version of the vernacular + "Test ...": it tells if a given object is in the table; [elements] + returns the list of elements of the table *) + +module MakeStringTable : + functor + (A : sig + val key : option_name + val title : string + val member_message : string -> bool -> Pp.t + end) -> +sig + val active : string -> bool + val elements : unit -> string list +end + +(** The functor [MakeRefTable] declares a new table of objects of type + [A.t] practically denoted by [reference]; the encoding function + [encode : reference -> A.t] is typically a globalization function, + possibly with some restriction checks; the function + [member_message] say what to print when invoking the "Test Toto + Titi foo." command; at the end [title] is the table name printed + when invoking the "Print Toto Titi." command; [active] is roughly + the internal version of the vernacular "Test ...": it tells if a + given object is in the table. *) + +module MakeRefTable : + functor + (A : sig + type t + val compare : t -> t -> int + val encode : qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> + sig + val active : A.t -> bool + val elements : unit -> A.t list + end + + +(** {6 Options. } *) + +(** These types and function are for declaring a new option of name [key] + and access functions [read] and [write]; the parameter [name] is the option name + used when printing the option value (command "Print Toto Titi." *) + +type 'a option_sig = { + optdepr : bool; + (** whether the option is DEPRECATED *) + optname : string; + (** a short string describing the option *) + optkey : option_name; + (** the low-level name of this option *) + optread : unit -> 'a; + optwrite : 'a -> unit +} + +(** 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. *) + +val declare_int_option : ?preprocess:(int option -> int option) -> + int option option_sig -> unit +val declare_bool_option : ?preprocess:(bool -> bool) -> + bool option_sig -> unit +val declare_string_option: ?preprocess:(string -> string) -> + string option_sig -> unit +val declare_stringopt_option: ?preprocess:(string option -> string option) -> + string option option_sig -> unit + +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) + +(** {6 Special functions supposed to be used only in vernacentries.ml } *) + +module OptionMap : CSig.MapS with type key = option_name + +val get_string_table : + option_name -> + < add : string -> unit; + remove : string -> unit; + mem : string -> unit; + print : unit > + +val get_ref_table : + option_name -> + < add : qualid -> unit; + remove : qualid -> unit; + mem : qualid -> unit; + print : unit > + +(** The first argument is a locality flag. *) +val set_int_option_value_gen : ?locality:option_locality -> option_name -> int option -> unit +val set_bool_option_value_gen : ?locality:option_locality -> option_name -> bool -> unit +val set_string_option_value_gen : ?locality:option_locality -> option_name -> string -> unit +val set_string_option_append_value_gen : ?locality:option_locality -> option_name -> string -> unit +val unset_option_value_gen : ?locality:option_locality -> option_name -> unit + +val set_int_option_value : option_name -> int option -> unit +val set_bool_option_value : option_name -> bool -> unit +val set_string_option_value : option_name -> string -> unit + +val print_option_value : option_name -> unit + +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | StringOptValue of string option + +(** Summary of an option status *) +type option_state = { + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + +val get_tables : unit -> option_state OptionMap.t +val print_tables : unit -> Pp.t + +val error_undeclared_key : option_name -> 'a diff --git a/library/keys.ml b/library/keys.ml new file mode 100644 index 0000000000..58883ccc88 --- /dev/null +++ b/library/keys.ml @@ -0,0 +1,159 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Keys for unification and indexing *) + +open Names +open Constr +open Libobject +open Globnames + +type key = + | KGlob of GlobRef.t + | KLam + | KLet + | KProd + | KSort + | KCase + | KFix + | KCoFix + | KRel + +module KeyOrdered = struct + type t = key + + let hash gr = + match gr with + | KGlob gr -> 8 + GlobRef.Ordered.hash gr + | KLam -> 0 + | KLet -> 1 + | KProd -> 2 + | KSort -> 3 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 + + let compare gr1 gr2 = + match gr1, gr2 with + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 + | _, KGlob _ -> -1 + | KGlob _, _ -> 1 + | k, k' -> Int.compare (hash k) (hash k') + + let equal k1 k2 = + match k1, k2 with + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 + | _, KGlob _ -> false + | KGlob _, _ -> false + | k, k' -> k == k' +end + +module Keymap = HMap.Make(KeyOrdered) +module Keyset = Keymap.Set + +(* Mapping structure for references to be considered equivalent *) + +let keys = Summary.ref Keymap.empty ~name:"Keys_decl" + +let add_kv k v m = + try Keymap.modify k (fun k' vs -> Keyset.add v vs) m + with Not_found -> Keymap.add k (Keyset.singleton v) m + +let add_keys k v = + keys := add_kv k v (add_kv v k !keys) + +let equiv_keys k k' = + k == k' || KeyOrdered.equal k k' || + try Keyset.mem k' (Keymap.find k !keys) + with Not_found -> false + +(** Registration of keys as an object *) + +let load_keys _ (_,(ref,ref')) = + add_keys ref ref' + +let cache_keys o = + load_keys 1 o + +let subst_key subst k = + match k with + | KGlob gr -> KGlob (subst_global_reference subst gr) + | _ -> k + +let subst_keys (subst,(k,k')) = + (subst_key subst k, subst_key subst k') + +let discharge_key = function + | KGlob (VarRef _ as g) when Lib.is_in_section g -> None + | x -> Some x + +let discharge_keys (_,(k,k')) = + match discharge_key k, discharge_key k' with + | Some x, Some y -> Some (x, y) + | _ -> None + +type key_obj = key * key + +let inKeys : key_obj -> obj = + declare_object @@ superglobal_object "KEYS" + ~cache:cache_keys + ~subst:(Some subst_keys) + ~discharge:discharge_keys + +let declare_equiv_keys ref ref' = + Lib.add_anonymous_leaf (inKeys (ref,ref')) + +let constr_key kind c = + let open Globnames in + try + let rec aux k = + match kind k with + | Const (c, _) -> KGlob (ConstRef c) + | Ind (i, u) -> KGlob (IndRef i) + | Construct (c,u) -> KGlob (ConstructRef c) + | Var id -> KGlob (VarRef id) + | App (f, _) -> aux f + | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) + | Cast (p, _, _) -> aux p + | Lambda _ -> KLam + | Prod _ -> KProd + | Case _ -> KCase + | Fix _ -> KFix + | CoFix _ -> KCoFix + | Rel _ -> KRel + | Meta _ -> raise Not_found + | Evar _ -> raise Not_found + | Sort _ -> KSort + | LetIn _ -> KLet + in Some (aux c) + with Not_found -> None + +open Pp + +let pr_key pr_global = function + | KGlob gr -> pr_global gr + | KLam -> str"Lambda" + | KLet -> str"Let" + | KProd -> str"Product" + | KSort -> str"Sort" + | KCase -> str"Case" + | KFix -> str"Fix" + | KCoFix -> str"CoFix" + | KRel -> str"Rel" + +let pr_keyset pr_global v = + prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) + +let pr_mapping pr_global k v = + pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v + +let pr_keys pr_global = + Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/library/keys.mli b/library/keys.mli new file mode 100644 index 0000000000..198383650a --- /dev/null +++ b/library/keys.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type key + +val declare_equiv_keys : key -> key -> unit +(** Declare two keys as being equivalent. *) + +val equiv_keys : key -> key -> bool +(** Check equivalence of keys. *) + +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 : (Names.GlobRef.t -> Pp.t) -> Pp.t +(** Pretty-print the mapping *) diff --git a/library/kindops.ml b/library/kindops.ml new file mode 100644 index 0000000000..247319fa2f --- /dev/null +++ b/library/kindops.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Decl_kinds + +(** Operations about types defined in [Decl_kinds] *) + +let logical_kind_of_goal_kind = function + | DefinitionBody d -> IsDefinition d + | Proof s -> IsProof s + +let string_of_theorem_kind = function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + +let string_of_definition_object_kind = function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli new file mode 100644 index 0000000000..df39019da4 --- /dev/null +++ b/library/kindops.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Decl_kinds + +(** Operations about types defined in [Decl_kinds] *) + +val logical_kind_of_goal_kind : goal_object_kind -> logical_kind +val string_of_theorem_kind : theorem_kind -> string +val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/lib.ml b/library/lib.ml new file mode 100644 index 0000000000..d4381a6923 --- /dev/null +++ b/library/lib.ml @@ -0,0 +1,668 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names +open Libnames +open Globnames +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 *) + +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname Nametab.{ obj_dir; obj_mp } id = + Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) + +(* let make_oname (dirpath,(mp,dir)) id = *) +type node = + | Leaf of obj + | CompilingLibrary of Nametab.object_prefix + | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen + | OpenedSection of Nametab.object_prefix * Summary.frozen + +type library_entry = object_name * node + +type library_segment = library_entry list + +type lib_objects = (Names.Id.t * obj) list + +let module_kind is_type = + if is_type then "module type" else "module" + +let iter_objects f i prefix = + List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) + +let load_objects i pr = iter_objects load_object i pr +let open_objects i pr = iter_objects open_object i pr + +let subst_objects subst seg = + let subst_one = fun (id,obj as node) -> + let obj' = subst_object (subst,obj) in + if obj' == obj then node else + (id, obj') + in + List.Smart.map subst_one seg + +(*let load_and_subst_objects i prefix subst seg = + List.rev (List.fold_left (fun seg (id,obj as node) -> + let obj' = subst_object (make_oname prefix id, subst, obj) in + let node = if obj == obj' then node else (id, obj') in + load_object i (make_oname prefix id, obj'); + node :: seg) [] seg) +*) +let classify_segment seg = + let rec clean ((substl,keepl,anticipl) as acc) = function + | (_,CompilingLibrary _) :: _ | [] -> acc + | ((sp,kn),Leaf o) :: stk -> + let id = Names.Label.to_id (Names.KerName.label kn) in + (match classify_object o with + | Dispose -> clean acc stk + | Keep o' -> + clean (substl, (id,o')::keepl, anticipl) stk + | Substitute o' -> + clean ((id,o')::substl, keepl, anticipl) stk + | Anticipate o' -> + clean (substl, keepl, o'::anticipl) stk) + | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") + | (_,OpenedModule (ty,_,_,_)) :: _ -> + user_err ~hdr:"Lib.classify_segment" + (str "there are still opened " ++ str (module_kind ty) ++ str "s") + in + clean ([],[],[]) (List.rev seg) + + +let segment_of_objects prefix = + List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj)) + +(* We keep trace of operations in the stack [lib_stk]. + [path_prefix] is the current path of sections, where sections are stored in + ``correct'' order, the oldest coming first in the list. It may seems + costly, but in practice there is not so many openings and closings of + sections, but on the contrary there are many constructions of section + paths based on the library path. *) + +let initial_prefix = Nametab.{ + obj_dir = default_library; + obj_mp = ModPath.initial; + obj_sec = DirPath.empty; +} + +type lib_state = { + comp_name : DirPath.t option; + lib_stk : library_segment; + path_prefix : Nametab.object_prefix; +} + +let initial_lib_state = { + comp_name = None; + lib_stk = []; + path_prefix = initial_prefix; +} + +let lib_state = ref initial_lib_state + +let library_dp () = + 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 cwd () = !lib_state.path_prefix.Nametab.obj_dir +let current_mp () = !lib_state.path_prefix.Nametab.obj_mp +let current_sections () = !lib_state.path_prefix.Nametab.obj_sec + +let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) +let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) + +let cwd_except_section () = + Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) + +let current_dirpath sec = + Libnames.drop_dirpath_prefix (library_dp ()) + (if sec then cwd () else cwd_except_section ()) + +let make_path id = Libnames.make_path (cwd ()) id + +let make_path_except_section id = + Libnames.make_path (cwd_except_section ()) id + +let make_kn id = + let mp = current_mp () in + Names.KerName.make mp (Names.Label.of_id id) + +let make_foname id = make_oname !lib_state.path_prefix id + +let recalc_path_prefix () = + let rec recalc = function + | (sp, OpenedSection (dir,_)) :: _ -> dir + | (sp, OpenedModule (_,_,dir,_)) :: _ -> dir + | (sp, CompilingLibrary dir) :: _ -> dir + | _::l -> recalc l + | [] -> initial_prefix + in + lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk } + +let pop_path_prefix () = + let op = !lib_state.path_prefix in + lib_state := { !lib_state + with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir; + obj_sec = pop_dirpath op.obj_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_state.lib_stk + +let find_entries_p p = + let rec find = function + | [] -> [] + | ent::l -> if p ent then ent::find l else find l + in + find !lib_state.lib_stk + +let split_lib_gen test = + let rec collect after equal = function + | hd::before when test hd -> collect after (hd::equal) before + | before -> after,equal,before + in + let rec findeq after = function + | hd :: before when test hd -> collect after [hd] before + | hd :: before -> findeq (hd::after) before + | [] -> user_err Pp.(str "no such entry") + in + findeq [] !lib_state.lib_stk + +let eq_object_name (fp1, kn1) (fp2, kn2) = + eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2 + +let split_lib sp = + let is_sp (nsp, _) = eq_object_name sp nsp in + split_lib_gen is_sp + +let split_lib_at_opening sp = + let is_sp (nsp, obj) = match obj with + | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> + eq_object_name nsp sp + | _ -> false + in + let a, s, b = split_lib_gen is_sp in + match s with + | [obj] -> (a, obj, b) + | _ -> assert false + +(* Adding operations. *) + +let add_entry sp node = + lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } + +let pull_to_head oname = + 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 + fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) + +let add_anonymous_entry node = + add_entry (make_foname (anonymous_id ())) node + +let add_leaf id obj = + if ModPath.equal (current_mp ()) ModPath.initial then + user_err Pp.(str "No session module started (use -top dir)"); + let oname = make_foname id in + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname + +let add_discharged_leaf id obj = + let oname = make_foname id in + let newobj = rebuild_object obj in + cache_object (oname,newobj); + add_entry oname (Leaf newobj) + +let add_leaves id objs = + let oname = make_foname id in + let add_obj obj = + add_entry oname (Leaf obj); + load_object 1 (oname,obj) + in + List.iter add_obj objs; + oname + +let add_anonymous_leaf ?(cache_first = true) obj = + let id = anonymous_id () in + let oname = make_foname id in + if cache_first then begin + cache_object (oname,obj); + add_entry oname (Leaf obj) + end else begin + add_entry oname (Leaf obj); + cache_object (oname,obj) + end + +(* Modules. *) + +let is_opening_node = function + | _,(OpenedSection _ | OpenedModule _) -> true + | _ -> false + +let is_opening_node_or_lib = function + | _,(CompilingLibrary _ | OpenedSection _ | OpenedModule _) -> true + | _ -> false + +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) + | _ -> 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 = + let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in + let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in + let exists = + if is_type then Nametab.exists_cci (make_path id) + else Nametab.exists_module dir + in + if exists then + user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); + add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs)); + lib_state := { !lib_state with path_prefix = prefix} ; + prefix + +let start_module = start_mod false +let start_modtype = start_mod true None + +let error_still_opened string oname = + let id = basename (fst oname) in + user_err + (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.") + +let end_mod is_type = + let oname,fs = + try match find_entry_p is_opening_node with + | oname,OpenedModule (ty,_,_,fs) -> + if ty == is_type then oname, fs + else error_still_opened (module_kind ty) oname + | oname,OpenedSection _ -> error_still_opened "section" oname + | _ -> assert false + with Not_found -> user_err (Pp.str "No opened modules.") + in + let (after,mark,before) = split_lib_at_opening oname in + lib_state := { !lib_state with lib_stk = before }; + 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_state.lib_stk + +let contents_after sp = let (after,_,_) = split_lib sp in after + +(* Modules. *) + +(* TODO: use check_for_module ? *) +let start_compilation s mp = + if !lib_state.comp_name != None then + user_err Pp.(str "compilation unit is already started"); + if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then + user_err Pp.(str "some sections are already opened"); + let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + add_anonymous_entry (CompilingLibrary prefix); + lib_state := { !lib_state with comp_name = Some s; + path_prefix = prefix } + +let open_blocks_message es = + let open_block_name = function + | oname, OpenedSection _ -> str "section " ++ Id.print (basename (fst oname)) + | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ Id.print (basename (fst oname)) + | _ -> assert false in + str "The " ++ pr_enum open_block_name es ++ spc () ++ + str "need" ++ str (if List.length es == 1 then "s" else "") ++ str " to be closed." + +let end_compilation_checks dir = + let _ = match find_entries_p is_opening_node with + | [] -> () + | es -> user_err ~hdr:"Lib.end_compilation_checks" (open_blocks_message es) in + let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false + in + let oname = + try match find_entry_p is_opening_lib with + | (oname, CompilingLibrary prefix) -> oname + | _ -> assert false + with Not_found -> anomaly (Pp.str "No module declared.") + in + let _ = + 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 () ++ DirPath.print m ++ + spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); + in + oname + +let end_compilation oname = + let (after,mark,before) = split_lib_at_opening oname in + 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 *) + +let is_module_gen which check = + let test = function + | _, OpenedModule (ty,_,_,_) -> which ty + | _ -> false + in + try + match find_entry_p test with + | _, OpenedModule (ty,_,_,_) -> check ty + | _ -> assert false + with Not_found -> false + +let is_module_or_modtype () = is_module_gen (fun _ -> true) (fun _ -> true) +let is_modtype () = is_module_gen (fun b -> b) (fun _ -> true) +let is_modtype_strict () = is_module_gen (fun _ -> true) (fun b -> b) +let is_module () = is_module_gen (fun b -> not b) (fun _ -> true) + +(* Returns the opening node of a given name *) +let find_opening_node id = + try + let oname,entry = find_entry_p is_opening_node in + let id' = basename (fst oname) in + if not (Names.Id.equal id id') then + user_err ~hdr:"Lib.find_opening_node" + (str "Last block to end has name " ++ Id.print id' ++ str "."); + entry + with Not_found -> user_err Pp.(str "There is nothing to end.") + +(* Discharge tables *) + +(* At each level of section, we remember + - the list of variables in this section + - the list of variables on which each constant depends in this section + - the list of variables on which each inductive depends in this section + - the list of substitution to do at section closing +*) + +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind + +type variable_context = variable_info list +type abstr_info = { + abstr_ctx : variable_context; + abstr_subst : Univ.Instance.t; + abstr_uctx : Univ.AUContext.t; +} +type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t + +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.ContextSet.t) + | Context of Univ.ContextSet.t + +let sectab = + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) + ~name:"section-context" + +let add_section () = + sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), + (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab + +let check_same_poly p vars = + let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + if List.exists pred vars then + user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") + +let add_section_variable id impl poly ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + check_same_poly true vars; + sectab := (Context ctx :: vars,repl,abs)::sl + +exception PolyFound of bool (* make this a let exception once possible *) +let is_polymorphic_univ u = + try + let open Univ in + List.iter (fun (vars,_,_) -> + List.iter (function + | Variable (_,_,poly,(univs,_)) -> + if LSet.mem u univs then raise (PolyFound poly) + | Context (univs,_) -> + if LSet.mem u univs then raise (PolyFound true) + ) vars + ) !sectab; + false + with PolyFound b -> b + +let extract_hyps (secs,ohyps) = + let rec aux = function + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + let l, r = aux (idl,hyps) in + (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 + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx + | [], _ -> [],Univ.ContextSet.empty + in aux (secs,ohyps) + +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 name_instance inst = + (* FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (* Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map map (Univ.Instance.to_array inst) + +let add_section_replacement f g poly hyps = + match !sectab with + | [] -> () + | (vars,exps,abs)::sl -> + let () = check_same_poly poly vars in + let sechyps,ctx = extract_hyps (vars,hyps) in + let ctx = Univ.ContextSet.to_context ctx in + let inst = Univ.UContext.instance ctx in + let nas = name_instance inst in + let subst, ctx = Univ.abstract_universes nas ctx in + let args = instance_from_variable_context (List.rev sechyps) in + let info = { + abstr_ctx = sechyps; + abstr_subst = subst; + abstr_uctx = ctx; + } in + sectab := (vars,f (inst,args) exps, g info abs) :: sl + +let add_section_kn poly kn = + let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in + add_section_replacement f f poly + +let add_section_constant poly kn = + let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in + add_section_replacement f f poly + +let replacement_context () = pi2 (List.hd !sectab) + +let section_segment_of_constant con = + Names.Cmap.find con (fst (pi3 (List.hd !sectab))) + +let section_segment_of_mutual_inductive kn = + Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) + +let empty_segment = { + abstr_ctx = []; + abstr_subst = Univ.Instance.empty; + abstr_uctx = Univ.AUContext.empty; +} + +let section_segment_of_reference = function +| ConstRef c -> section_segment_of_constant c +| IndRef (kn,_) | ConstructRef ((kn,_),_) -> + section_segment_of_mutual_inductive kn +| VarRef _ -> empty_segment + +let variable_section_segment_of_reference gr = + (section_segment_of_reference gr).abstr_ctx + +let section_instance = function + | VarRef id -> + let eq = function + | Variable (id',_,_,_) -> Names.Id.equal id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found + | ConstRef con -> + Names.Cmap.find con (fst (pi2 (List.hd !sectab))) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + Names.Mindmap.find kn (snd (pi2 (List.hd !sectab))) + +let is_in_section ref = + try ignore (section_instance ref); true with Not_found -> false + +(*************) +(* Sections. *) +let open_section id = + let opp = !lib_state.path_prefix in + let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in + let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + if Nametab.exists_section obj_dir then + user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); + let fs = Summary.freeze_summaries ~marshallable:false in + add_entry (make_foname id) (OpenedSection (prefix, fs)); + (*Pushed for the lifetime of the section: removed by unfrozing the summary*) + Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); + lib_state := { !lib_state with path_prefix = prefix }; + add_section () + + +(* Restore lib_stk and summaries as before the section opening, and + add a ClosedSection object. *) + +let discharge_item ((sp,_ as oname),e) = + match e with + | Leaf lobj -> + Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> + anomaly (Pp.str "discharge_item.") + +let close_section () = + let oname,fs = + try match find_entry_p is_opening_node with + | oname,OpenedSection (_,fs) -> oname,fs + | _ -> assert false + with Not_found -> + user_err Pp.(str "No opened section.") + in + let (secdecls,mark,before) = split_lib_at_opening oname in + lib_state := { !lib_state with lib_stk = before }; + pop_path_prefix (); + let newdecls = List.map discharge_item secdecls in + Summary.unfreeze_summaries fs; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls + +(* State and initialization. *) + +type frozen = lib_state + +let freeze ~marshallable = !lib_state + +let unfreeze st = lib_state := st + +let drop_objects st = + let lib_stk = + CList.map_filter (function + | _, Leaf _ -> None + | n, (CompilingLibrary _ as x) -> Some (n,x) + | n, OpenedModule (it,e,op,_) -> + Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) + | n, OpenedSection (op, _) -> + Some(n,OpenedSection(op,Summary.empty_frozen))) + st.lib_stk in + { st with lib_stk } + +let init () = + unfreeze initial_lib_state; + Summary.init_summaries () + +(* Misc *) + +let mp_of_global = function + | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp + | ConstRef cst -> Names.Constant.modpath cst + | IndRef ind -> Names.ind_modpath ind + | ConstructRef constr -> Names.constr_modpath constr + +let rec dp_of_mp = function + |Names.MPfile dp -> dp + |Names.MPbound _ -> library_dp () + |Names.MPdot (mp,_) -> dp_of_mp mp + +let rec split_modpath = function + |Names.MPfile dp -> dp, [] + |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid] + |Names.MPdot (mp,l) -> + let (dp,ids) = split_modpath mp in + (dp, Names.Label.to_id l :: ids) + +let library_part = function + |VarRef id -> library_dp () + |ref -> dp_of_mp (mp_of_global ref) + +let discharge_proj_repr = + Projection.Repr.map_npars (fun mind npars -> + if not (is_in_section (IndRef (mind,0))) then mind, npars + else let modlist = replacement_context () in + let _, newpars = Mindmap.find mind (snd modlist) in + mind, npars + Array.length newpars) + +let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = + let open Univ in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let subst = make_instance_subst subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli new file mode 100644 index 0000000000..30569197bc --- /dev/null +++ b/library/lib.mli @@ -0,0 +1,199 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** Lib: record of operations, backtrack, low-level sections *) + +(** This module provides a general mechanism to keep a trace of all operations + and to backtrack (undo) those operations. It provides also the section + mechanism (at a low level; discharge is not known at this step). *) + +type is_type = bool (* Module Type or just Module *) +type export = bool option (* None for a Module Type *) + +val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name + +type node = + | Leaf of Libobject.obj + | CompilingLibrary of Nametab.object_prefix + | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen + | OpenedSection of Nametab.object_prefix * Summary.frozen + +type library_segment = (Libobject.object_name * node) list + +type lib_objects = (Id.t * Libobject.obj) list + +(** {6 Object iteration functions. } *) + +val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit +val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit +val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects +(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) + +(** [classify_segment seg] verifies that there are no OpenedThings, + clears ClosedSections and FrozenStates and divides Leafs according + to their answers to the [classify_object] function in three groups: + [Substitute], [Keep], [Anticipate] respectively. The order of each + returned list is the same as in the input list. *) +val classify_segment : + library_segment -> lib_objects * lib_objects * Libobject.obj list + +(** [segment_of_objects prefix objs] forms a list of Leafs *) +val segment_of_objects : + Nametab.object_prefix -> lib_objects -> library_segment + + +(** {6 ... } *) +(** Adding operations (which call the [cache] method, and getting the + current list of operations (most recent ones coming first). *) + +val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name +val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit +val pull_to_head : Libobject.object_name -> unit + +(** this operation adds all objects with the same name and calls [load_object] + for each of them *) +val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name + +(** {6 ... } *) + +(** The function [contents] gives access to the current entire segment *) + +val contents : unit -> library_segment + +(** The function [contents_after] returns the current library segment, + starting from a given section path. *) + +val contents_after : Libobject.object_name -> library_segment + +(** {6 Functions relative to current path } *) + +(** User-side names *) +val cwd : unit -> DirPath.t +val cwd_except_section : unit -> DirPath.t +val current_dirpath : bool -> DirPath.t (* false = except sections *) +val make_path : Id.t -> Libnames.full_path +val make_path_except_section : Id.t -> Libnames.full_path + +(** Kernel-side names *) +val current_mp : unit -> ModPath.t +val make_kn : Id.t -> KerName.t + +(** Are we inside an opened section *) +val sections_are_opened : unit -> bool +val sections_depth : unit -> int + +(** Are we inside an opened module type *) +val is_module_or_modtype : unit -> bool +val is_modtype : unit -> bool +(* [is_modtype_strict] checks not only if we are in a module type, but + if the latest module started is a module type. *) +val is_modtype_strict : unit -> bool +val is_module : unit -> bool +val current_mod_id : unit -> module_ident + +(** Returns the opening node of a given name *) +val find_opening_node : Id.t -> node + +(** {6 Modules and module types } *) + +val start_module : + export -> module_ident -> ModPath.t -> + Summary.frozen -> Nametab.object_prefix + +val start_modtype : + module_ident -> ModPath.t -> + Summary.frozen -> Nametab.object_prefix + +val end_module : + unit -> + Libobject.object_name * Nametab.object_prefix * + Summary.frozen * library_segment + +val end_modtype : + unit -> + Libobject.object_name * Nametab.object_prefix * + Summary.frozen * library_segment + +(** {6 Compilation units } *) + +val start_compilation : DirPath.t -> ModPath.t -> unit +val end_compilation_checks : DirPath.t -> Libobject.object_name +val end_compilation : + Libobject.object_name-> Nametab.object_prefix * library_segment + +(** The function [library_dp] returns the [DirPath.t] of the current + compiling library (or [default_library]) *) +val library_dp : unit -> DirPath.t + +(** Extract the library part of a name even if in a section *) +val dp_of_mp : ModPath.t -> DirPath.t +val split_modpath : ModPath.t -> DirPath.t * Id.t list +val library_part : GlobRef.t -> DirPath.t + +(** {6 Sections } *) + +val open_section : Id.t -> unit +val close_section : unit -> unit + +(** {6 We can get and set the state of the operations (used in [States]). } *) + +type frozen + +val freeze : marshallable:bool -> frozen +val unfreeze : frozen -> unit + +(** Keep only the libobject structure, not the objects themselves *) +val drop_objects : frozen -> frozen + +val init : unit -> unit + +(** {6 Section management for discharge } *) +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind +type variable_context = variable_info list +type abstr_info = private { + abstr_ctx : variable_context; + (** Section variables of this prefix *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} + +val instance_from_variable_context : variable_context -> Id.t array +val named_of_variable_context : variable_context -> Constr.named_context + +val section_segment_of_constant : Constant.t -> abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> abstr_info +val section_segment_of_reference : GlobRef.t -> abstr_info + +val variable_section_segment_of_reference : GlobRef.t -> variable_context + +val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array +val is_in_section : GlobRef.t -> bool + +val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_context : Univ.ContextSet.t -> unit +val add_section_constant : Decl_kinds.polymorphic -> + Constant.t -> Constr.named_context -> unit +val add_section_kn : Decl_kinds.polymorphic -> + MutInd.t -> Constr.named_context -> unit +val replacement_context : unit -> Opaqueproof.work_list + +val is_polymorphic_univ : Univ.Level.t -> bool + +(** {6 Discharge: decrease the section level if in the current section } *) + +(* XXX Why can't we use the kernel functions ? *) + +val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/libnames.ml b/library/libnames.ml new file mode 100644 index 0000000000..87c4de42e8 --- /dev/null +++ b/library/libnames.ml @@ -0,0 +1,171 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names + +(**********************************************) + +(*s Operations on dirpaths *) + +let split_dirpath d = match DirPath.repr d with + | id :: l -> DirPath.make l, id + | _ -> failwith "split_dirpath" + +let pop_dirpath p = match DirPath.repr p with + | _::l -> DirPath.make l + | [] -> failwith "pop_dirpath" + +(* Pop the last n module idents *) +let pop_dirpath_n n dir = DirPath.make (List.skipn n (DirPath.repr dir)) + +let is_dirpath_prefix_of d1 d2 = + List.prefix_of Id.equal + (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) + +let is_dirpath_suffix_of dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 + +let chop_dirpath n d = + let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in + DirPath.make (List.rev d1), DirPath.make (List.rev d2) + +let drop_dirpath_prefix d1 d2 = + let d = + List.drop_prefix Id.equal + (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) + in + DirPath.make (List.rev d) + +let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1) + +let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id]) + +let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) + +(* parsing *) +let parse_dir s = + let len = String.length s in + let rec decoupe_dirs dirs n = + 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 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 + decoupe_dirs [] 0 + +let dirpath_of_string s = + let path = match s with + | "" -> [] + | _ -> parse_dir s + in + DirPath.make path + +module Dirset = Set.Make(DirPath) +module Dirmap = Map.Make(DirPath) + +(*s Section paths are absolute names *) + +type full_path = { + dirpath : DirPath.t ; + basename : Id.t } + +let dirpath sp = sp.dirpath +let basename sp = sp.basename + +let make_path pa id = { dirpath = pa; basename = id } + +let repr_path { dirpath = pa; basename = id } = (pa,id) + +let eq_full_path p1 p2 = + Id.equal p1.basename p2.basename && + DirPath.equal p1.dirpath p2.dirpath + +(* parsing and printing of section paths *) +let string_of_path sp = + let (sl,id) = repr_path sp in + match DirPath.repr sl with + | [] -> Id.to_string id + | _ -> (DirPath.to_string sl) ^ "." ^ (Id.to_string id) + +let sp_ord sp1 sp2 = + let (p1,id1) = repr_path sp1 + and (p2,id2) = repr_path sp2 in + let p_bit = DirPath.compare p1 p2 in + if Int.equal p_bit 0 then Id.compare id1 id2 else p_bit + +module SpOrdered = + struct + type t = full_path + let compare = sp_ord + end + +module Spmap = Map.Make(SpOrdered) + +let path_of_string s = + try + let dir, id = split_dirpath (dirpath_of_string s) in + make_path dir id + with + | Invalid_argument _ -> invalid_arg "path_of_string" + +let pr_path sp = str (string_of_path sp) + +let restrict_path n sp = + let dir, s = repr_path sp in + let dir' = List.firstn n (DirPath.repr dir) in + make_path (DirPath.make dir') s + +(*s qualified names *) +type qualid_r = full_path +type qualid = qualid_r CAst.t + +let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id) +let repr_qualid {CAst.v=qid} = repr_path qid + +let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v + +let string_of_qualid qid = string_of_path qid.CAst.v +let pr_qualid qid = pr_path qid.CAst.v + +let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s + +let qualid_of_path ?loc sp = CAst.make ?loc sp +let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id +let qualid_of_dirpath ?loc dir = + let (l,a) = split_dirpath dir in + make_qualid ?loc l a + +let qualid_is_ident qid = + DirPath.is_empty qid.CAst.v.dirpath + +let qualid_basename qid = + qid.CAst.v.basename + +let qualid_path qid = + qid.CAst.v.dirpath + +(* Default paths *) +let default_library = Names.DirPath.initial (* = ["Top"] *) + +(*s Roots of the space of absolute names *) +let coq_string = "Coq" +let coq_root = Id.of_string coq_string +let default_root_prefix = DirPath.empty diff --git a/library/libnames.mli b/library/libnames.mli new file mode 100644 index 0000000000..bbb4d2a058 --- /dev/null +++ b/library/libnames.mli @@ -0,0 +1,102 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Names + +(** {6 Dirpaths } *) +val dirpath_of_string : string -> DirPath.t + +(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *) +val pop_dirpath : DirPath.t -> DirPath.t + +(** Pop the suffix n times *) +val pop_dirpath_n : int -> DirPath.t -> DirPath.t + +(** Immediate prefix and basename of a [DirPath.t]. May raise [Failure] *) +val split_dirpath : DirPath.t -> DirPath.t * Id.t + +val add_dirpath_suffix : DirPath.t -> module_ident -> DirPath.t +val add_dirpath_prefix : module_ident -> DirPath.t -> DirPath.t + +val chop_dirpath : int -> DirPath.t -> DirPath.t * DirPath.t +val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t + +val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t +val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool + +val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool + +module Dirset : Set.S with type elt = DirPath.t +module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset + +(** {6 Full paths are {e absolute} paths of declarations } *) +type full_path + +val eq_full_path : full_path -> full_path -> bool + +(** Constructors of [full_path] *) +val make_path : DirPath.t -> Id.t -> full_path + +(** Destructors of [full_path] *) +val repr_path : full_path -> DirPath.t * Id.t +val dirpath : full_path -> DirPath.t +val basename : full_path -> Id.t + +(** Parsing and printing of section path as ["coq_root.module.id"] *) +val path_of_string : string -> full_path +val string_of_path : full_path -> string +val pr_path : full_path -> Pp.t + +module Spmap : CSig.MapS with type key = full_path + +val restrict_path : int -> full_path -> full_path + +(** {6 ... } *) +(** A [qualid] is a partially qualified ident; it includes fully + qualified names (= absolute names) and all intermediate partial + qualifications of absolute names, including single identifiers. + The [qualid] are used to access the name table. *) + +type qualid_r +type qualid = qualid_r CAst.t + +val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid +val repr_qualid : qualid -> DirPath.t * Id.t + +val qualid_eq : qualid -> qualid -> bool + +val pr_qualid : qualid -> Pp.t +val string_of_qualid : qualid -> string +val qualid_of_string : ?loc:Loc.t -> string -> qualid + +(** Turns an absolute name, a dirpath, or an Id.t into a + qualified name denoting the same name *) + +val qualid_of_path : ?loc:Loc.t -> full_path -> qualid +val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid +val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid + +val qualid_is_ident : qualid -> bool +val qualid_path : qualid -> DirPath.t +val qualid_basename : qualid -> Id.t + +(** {6 ... } *) + +(** some preset paths *) +val default_library : DirPath.t + +(** This is the root of the standard library of Coq *) +val coq_root : module_ident (* "Coq" *) +val coq_string : string (* "Coq" *) + +(** This is the default root prefix for developments which doesn't + mention a root *) +val default_root_prefix : DirPath.t diff --git a/library/libobject.ml b/library/libobject.ml new file mode 100644 index 0000000000..3d17b4a605 --- /dev/null +++ b/library/libobject.ml @@ -0,0 +1,174 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp + +module Dyn = Dyn.Make () + +type 'a substitutivity = + Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a + +type object_name = Libnames.full_path * Names.KerName.t + +type 'a object_declaration = { + object_name : string; + cache_function : object_name * 'a -> unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : 'a -> 'a substitutivity; + subst_function : Mod_subst.substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a } + +let default_object s = { + object_name = s; + cache_function = (fun _ -> ()); + load_function = (fun _ _ -> ()); + open_function = (fun _ _ -> ()); + subst_function = (fun _ -> + CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); + classify_function = (fun obj -> Keep obj); + discharge_function = (fun _ -> None); + rebuild_function = (fun x -> x)} + + +(* The suggested object declaration is the following: + + declare_object { (default_object "MY OBJECT") with + cache_function = fun (sp,a) -> Mytbl.add sp a} + + and the listed functions are only those which definitions actually + differ from the default. + + This helps introducing new functions in objects. +*) + +let ident_subst_function (_,a) = a + +type obj = Dyn.t (* persistent dynamic objects *) + +type dynamic_object_declaration = { + dyn_cache_function : object_name * obj -> unit; + dyn_load_function : int -> object_name * obj -> unit; + dyn_open_function : int -> object_name * obj -> unit; + dyn_subst_function : Mod_subst.substitution * obj -> obj; + dyn_classify_function : obj -> obj substitutivity; + dyn_discharge_function : object_name * obj -> obj option; + dyn_rebuild_function : obj -> obj } + +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t + +let cache_tab = + (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t) + +let declare_object_full odecl = + let na = odecl.object_name in + let (infun, outfun) = Dyn.Easy.make_dyn na in + let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) + and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) + and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) + and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj)) + and classifier lobj = match odecl.classify_function (outfun lobj) with + | Dispose -> Dispose + | Substitute obj -> Substitute (infun obj) + | Keep obj -> Keep (infun obj) + | Anticipate (obj) -> Anticipate (infun obj) + and discharge (oname,lobj) = + Option.map infun (odecl.discharge_function (oname,outfun lobj)) + and rebuild lobj = infun (odecl.rebuild_function (outfun lobj)) + in + Hashtbl.add cache_tab na { dyn_cache_function = cacher; + dyn_load_function = loader; + dyn_open_function = opener; + dyn_subst_function = substituter; + dyn_classify_function = classifier; + dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild }; + (infun,outfun) + +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. *) + +let apply_dyn_fun f lobj = + let tag = object_tag lobj in + let dodecl = + try Hashtbl.find cache_tab tag + with Not_found -> assert false + in + f dodecl + +let cache_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj + +let load_object i ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj + +let open_object i ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj + +let subst_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj + +let classify_object lobj = + apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj + +let discharge_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj + +let rebuild_object lobj = + apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump + +let local_object_nodischarge s ~cache = + { (default_object s) with + cache_function = cache; + classify_function = (fun _ -> Dispose); + } + +let local_object s ~cache ~discharge = + { (local_object_nodischarge s ~cache) with + discharge_function = discharge } + +let global_object_nodischarge s ~cache ~subst = + let import i o = if Int.equal i 1 then cache o in + { (default_object s) with + cache_function = cache; + open_function = import; + subst_function = (match subst with + | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!") + | Some subst -> subst; + ); + classify_function = + if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o); + } + +let global_object s ~cache ~subst ~discharge = + { (global_object_nodischarge s ~cache ~subst) with + discharge_function = discharge } + +let superglobal_object_nodischarge s ~cache ~subst = + { (default_object s) with + load_function = (fun _ x -> cache x); + cache_function = cache; + subst_function = (match subst with + | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!") + | Some subst -> subst; + ); + classify_function = + if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o); + } + +let superglobal_object s ~cache ~subst ~discharge = + { (superglobal_object_nodischarge s ~cache ~subst) with + discharge_function = discharge } diff --git a/library/libobject.mli b/library/libobject.mli new file mode 100644 index 0000000000..00515bd273 --- /dev/null +++ b/library/libobject.mli @@ -0,0 +1,169 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Libnames +open Mod_subst + +(** [Libobject] declares persistent objects, given with methods: + + * a caching function specifying how to add the object in the current + scope; + If the object wishes to register its visibility in the Nametab, + it should do so for all possible suffixes. + + * a loading function, specifying what to do when the module + containing the object is loaded; + If the object wishes to register its visibility in the Nametab, + it should do so for all suffixes no shorter than the "int" argument + + * an opening function, specifying what to do when the module + containing the object is opened (imported); + If the object wishes to register its visibility in the Nametab, + it should do so for the suffix of the length the "int" argument + + * a classification function, specifying what to do with the object, + when the current module (containing the object) is ended; + The possibilities are: + Dispose - the object dies at the end of the module + Substitute - meaning the object is substitutive and + the module name must be updated + Keep - the object is not substitutive, but survives module + closing + Anticipate - this is for objects that have to be explicitly + managed by the [end_module] function (like Require + and Read markers) + + The classification function is also an occasion for a cleanup + (if this function returns Keep or Substitute of some object, the + cache method is never called for it) + + * a substitution function, performing the substitution; + this function should be declared for substitutive objects + only (see above). NB: the substitution might now be delayed + instead of happening at module creation, so this function + should _not_ depend on the current environment + + * a discharge function, that is applied at section closing time to + collect the data necessary to rebuild the discharged form of the + non volatile objects + + * a rebuild function, that is applied after section closing to + rebuild the non volatile content of a section from the data + collected by the discharge function + + Any type defined as a persistent object must be pure (e.g. no references) and + marshallable by the OCaml Marshal module (e.g. no closures). + +*) + +type 'a substitutivity = + Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a + +(** Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [full_path] which can be printed +*) + +type object_name = full_path * Names.KerName.t + +type 'a object_declaration = { + object_name : string; + cache_function : object_name * 'a -> unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : 'a -> 'a substitutivity; + subst_function : substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a } + +(** The default object is a "Keep" object with empty methods. + Object creators are advised to use the construction + [{(default_object "MY_OBJECT") with + cache_function = ... + }] + and specify only these functions which are not empty/meaningless + +*) + +val default_object : string -> 'a object_declaration + +(** the identity substitution function *) +val ident_subst_function : substitution * 'a -> 'a + +(** {6 ... } *) +(** Given an object declaration, the function [declare_object_full] + will hand back two functions, the "injection" and "projection" + functions for dynamically typed library-objects. *) + +type obj + +val declare_object_full : + 'a object_declaration -> ('a -> obj) * (obj -> 'a) + +val declare_object : + 'a object_declaration -> ('a -> obj) + +val object_tag : obj -> string + +val cache_object : object_name * obj -> unit +val load_object : int -> object_name * obj -> unit +val open_object : int -> object_name * obj -> unit +val subst_object : substitution * obj -> obj +val classify_object : obj -> obj substitutivity +val discharge_object : object_name * obj -> obj option +val rebuild_object : obj -> obj + +(** Higher-level API for objects with fixed scope. + +- Local means that the object cannot be imported from outside. +- Global means that it can be imported (by importing the module that contains the +object). +- Superglobal means that the object survives to closing a module, and is imported +when the file which contains it is Required (even without Import). +- With the nodischarge variants, the object does not survive section closing. + With the normal variants, it does. + +We recommend to avoid declaring superglobal objects and using the nodischarge +variants. +*) + +val local_object : string -> + cache:(object_name * 'a -> unit) -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val local_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + 'a object_declaration + +val global_object : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val global_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + 'a object_declaration + +val superglobal_object : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + discharge:(object_name * 'a -> 'a option) -> + 'a object_declaration + +val superglobal_object_nodischarge : string -> + cache:(object_name * 'a -> unit) -> + subst:(Mod_subst.substitution * 'a -> 'a) option -> + 'a object_declaration + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/library.ml b/library/library.ml new file mode 100644 index 0000000000..9b9bd07c93 --- /dev/null +++ b/library/library.ml @@ -0,0 +1,750 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util + +open Names +open Libnames +open Lib +open Libobject + +(************************************************************************) +(*s Low-level interning/externing of libraries to files *) + +let raw_extern_library f = + System.raw_extern_state Coq_config.vo_magic_number f + +let raw_intern_library f = + System.with_magic_number_check + (System.raw_intern_state Coq_config.vo_magic_number) f + +(************************************************************************) +(** Serialized objects loaded on-the-fly *) + +exception Faulty of string + +module Delayed : +sig + +type 'a delayed +val in_delayed : string -> in_channel -> 'a delayed * Digest.t +val fetch_delayed : 'a delayed -> 'a + +end = +struct + +type 'a delayed = { + del_file : string; + del_off : int; + del_digest : Digest.t; +} + +let in_delayed f ch = + let pos = pos_in ch in + let _, digest = System.skip_in_segment f ch in + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) + +let fetch_delayed del = + let { del_digest = digest; del_file = f; del_off = pos; } = del in + try + let ch = raw_intern_library f in + let () = seek_in ch pos in + let obj, _, digest' = System.marshal_in_segment f ch in + let () = close_in ch in + if not (String.equal digest digest') then raise (Faulty f); + obj + with e when CErrors.noncritical e -> raise (Faulty f) + +end + +open Delayed + + +(************************************************************************) +(*s Modules on disk contain the following informations (after the magic + number, and before the digest). *) + +type compilation_unit_name = DirPath.t + +type library_disk = { + md_compiled : Safe_typing.compiled_library; + md_objects : Declaremods.library_objects; +} + +type summary_disk = { + md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : (compilation_unit_name * Safe_typing.vodigest) array; +} + +(*s Modules loaded in memory contain the following informations. They are + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_data : library_disk delayed; + library_deps : (compilation_unit_name * Safe_typing.vodigest) array; + library_imports : compilation_unit_name array; + library_digests : Safe_typing.vodigest; + library_extra_univs : Univ.ContextSet.t; +} + +type library_summary = { + libsum_name : compilation_unit_name; + libsum_digests : Safe_typing.vodigest; + libsum_imports : compilation_unit_name array; +} + +module LibraryOrdered = DirPath +module LibraryMap = Map.Make(LibraryOrdered) +module LibraryFilenameMap = Map.Make(LibraryOrdered) + +(* This is a map from names to loaded libraries *) +let libraries_table : library_summary LibraryMap.t ref = + Summary.ref LibraryMap.empty ~name:"LIBRARY" + +(* This is the map of loaded libraries filename *) +(* (not synchronized so as not to be caught in the states on disk) *) +let libraries_filename_table = ref LibraryFilenameMap.empty + +(* These are the _ordered_ sets of loaded, imported and exported libraries *) +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" + +(* various requests to the tables *) + +let find_library dir = + LibraryMap.find dir !libraries_table + +let try_find_library dir = + try find_library dir + with Not_found -> + user_err ~hdr:"Library.find_library" + (str "Unknown library " ++ DirPath.print dir) + +let register_library_filename dir f = + (* Not synchronized: overwrite the previous binding if one existed *) + (* from a previous play of the session *) + libraries_filename_table := + LibraryFilenameMap.add dir f !libraries_filename_table + +let library_full_filename dir = + try LibraryFilenameMap.find dir !libraries_filename_table + with Not_found -> "<unavailable filename>" + +let overwrite_library_filenames f = + let f = + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in + LibraryMap.iter (fun dir _ -> register_library_filename dir f) + !libraries_table + +let library_is_loaded dir = + try let _ = find_library dir in true + with Not_found -> false + +let library_is_opened dir = + List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list + +let loaded_libraries () = !libraries_loaded_list + +let opened_libraries () = !libraries_imports_list + + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) + +let register_loaded_library m = + let libname = m.libsum_name in + let link () = + let dirname = Filename.dirname (library_full_filename libname) in + let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in + let f = prefix ^ "cmo" in + let f = Dynlink.adapt_filename f in + if Coq_config.native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f + in + let rec aux = function + | [] -> link (); [libname] + | m'::_ as l when DirPath.equal m' libname -> l + | m'::l' -> m' :: aux l' in + libraries_loaded_list := aux !libraries_loaded_list; + libraries_table := LibraryMap.add libname m !libraries_table + + (* ... while if a library is imported/exported several time, then + only the last occurrence is really needed - though the imported + list may differ from the exported list (consider the sequence + Export A; Export B; Import A which results in A;B for exports but + in B;A for imports) *) + +let rec remember_last_of_each l m = + match l with + | [] -> [m] + | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m + | m'::l' -> m' :: remember_last_of_each l' m + +let register_open_library export m = + libraries_imports_list := remember_last_of_each !libraries_imports_list m; + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +(************************************************************************) +(*s Opening libraries *) + +(* [open_library export explicit m] opens library [m] if not already + opened _or_ if explicitly asked to be (re)opened *) + +let open_library export explicit_libs m = + if + (* Only libraries indirectly to open are not reopen *) + (* Libraries explicitly mentionned by the user are always reopen *) + List.exists (fun m' -> DirPath.equal m m') explicit_libs + || not (library_is_opened m) + then begin + register_open_library export m; + Declaremods.really_import_module (MPfile m) + end + else + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +(* open_libraries recursively open a list of libraries but opens only once + a library that is re-exported many times *) + +let open_libraries export modl = + let to_open_list = + List.fold_left + (fun l m -> + let subimport = + Array.fold_left + (fun l m -> remember_last_of_each l m) + l m.libsum_imports + in remember_last_of_each subimport m.libsum_name) + [] modl in + let explicit = List.map (fun m -> m.libsum_name) modl in + List.iter (open_library export explicit) to_open_list + + +(**********************************************************************) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) + +let open_import_library i (_,(modl,export)) = + if Int.equal i 1 then + (* even if the library is already imported, we re-import it *) + (* if not (library_is_opened dir) then *) + open_libraries export (List.map try_find_library modl) + +let cache_import_library obj = + open_import_library 1 obj + +let subst_import_library (_,o) = o + +let classify_import_library (_,export as obj) = + if export then Substitute obj else Dispose + +let in_import_library : DirPath.t list * bool -> obj = + declare_object {(default_object "IMPORT LIBRARY") with + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } + + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ + strbrk " instead of " ++ str vo ++ + strbrk " because it is more recent") + +let locate_absolute_library dir = + (* Search in loadpath *) + let pref, base = split_dirpath dir in + let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let loadpath = List.map fst loadpath in + let find ext = + try + let name = Id.to_string base ^ ext in + let _, file = System.where_in_path ~warn:false loadpath name in + Some file + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some file, None | None, Some file -> file + | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + vi + | Some vo, Some _ -> vo + +let locate_qualified_library ?root ?(warn = true) qid = + (* Search library in loadpath *) + let dir, base = repr_qualid qid in + let loadpath = Loadpath.expand_path ?root dir in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let find ext = + try + let name = Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn (List.map fst loadpath) name in + Some (lpath, file) + with Not_found -> None in + let lpath, file = + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some res, None | None, Some res -> res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + resvi + | Some resvo, Some _ -> resvo + in + let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in + (* Look if loaded *) + if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir) + (* Otherwise, look for it in the file system *) + else (LibInPath, dir, file) + +let error_unmapped_dir qid = + let prefix, _ = repr_qualid qid in + user_err ~hdr:"load_absolute_library_from" + (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ + str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) + +let error_lib_not_found qid = + user_err ~hdr:"load_absolute_library_from" + (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") + +let try_locate_absolute_library dir = + try + locate_absolute_library dir + with + | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) + | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) + +(************************************************************************) +(** {6 Tables of opaque proof terms} *) + +(** We now store opaque proof terms apart from the rest of the environment. + See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + we can quickly load a first half of a .vo file without these opaque + terms, and access them only when a specific command (e.g. Print or + Print Assumptions) needs it. *) + +(** Delayed / available tables of opaque terms *) + +type 'a table_status = + | ToFetch of 'a Future.computation array delayed + | Fetched of 'a Future.computation array + +let opaque_tables = + ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) +let univ_tables = + ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t) + +let add_opaque_table dp st = + opaque_tables := LibraryMap.add dp st !opaque_tables +let add_univ_table dp st = + univ_tables := LibraryMap.add dp st !univ_tables + +let access_table what tables dp i = + let t = match LibraryMap.find dp !tables with + | Fetched t -> t + | ToFetch f -> + let dir_path = Names.DirPath.to_string dp in + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let t = + try fetch_delayed f + with Faulty f -> + 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") + in + tables := LibraryMap.add dp (Fetched t) !tables; + t + in + assert (i < Array.length t); t.(i) + +let access_opaque_table dp i = + let what = "opaque proofs" in + access_table what opaque_tables dp i + +let access_univ_table dp i = + try + let what = "universe contexts of opaque proofs" in + Some (access_table what univ_tables dp i) + with Not_found -> None + +let () = + Opaqueproof.set_indirect_opaque_accessor access_opaque_table; + Opaqueproof.set_indirect_univ_accessor access_univ_table + +(************************************************************************) +(* Internalise libraries *) + +type seg_sum = summary_disk +type seg_lib = library_disk +type seg_univ = (* true = vivo, false = vi *) + Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool +type seg_discharge = Opaqueproof.cooking_info list array +type seg_proofs = Constr.constr Future.computation array + +let mk_library sd md digests univs = + { + library_name = sd.md_name; + library_data = md; + library_deps = sd.md_deps; + library_imports = sd.md_imports; + library_digests = digests; + library_extra_univs = univs; + } + +let mk_summary m = { + libsum_name = m.library_name; + libsum_imports = m.library_imports; + libsum_digests = m.library_digests; +} + +let intern_from_file f = + let ch = raw_intern_library f in + let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in + let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in + let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in + let _ = System.skip_in_segment f ch in + let _ = System.skip_in_segment f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in + close_in ch; + register_library_filename lsd.md_name f; + add_opaque_table lsd.md_name (ToFetch del_opaque); + let open Safe_typing in + match univs with + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + | Some (utab,uall,true) -> + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall + | Some (utab,_,false) -> + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + +module DPMap = Map.Make(DirPath) + +let rec intern_library (needed, contents) (dir, f) from = + (* Look if in the current logical environment *) + try (find_library dir).libsum_digests, (needed, contents) + with Not_found -> + (* Look if already listed and consequently its dependencies too *) + try (DPMap.find dir contents).library_digests, (needed, contents) + with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); + (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let f = match f with Some f -> f | None -> try_locate_absolute_library dir in + let m = intern_from_file f in + if not (DirPath.equal dir m.library_name) then + user_err ~hdr:"load_physical_library" + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ + DirPath.print m.library_name ++ spc () ++ str "and not library" ++ + spc() ++ DirPath.print dir); + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); + m.library_digests, intern_library_deps (needed, contents) dir m f + +and intern_library_deps libs dir m from = + let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in + (dir :: needed, DPMap.add dir m contents ) + +and intern_mandatory_library caller from libs (dir,d) = + let digest, libs = intern_library libs (dir, None) (Some from) in + if not (Safe_typing.digest_match ~actual:digest ~required:d) then + user_err (str "Compiled library " ++ DirPath.print caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ DirPath.print dir); + libs + +let rec_intern_library libs (dir, f) = + let _, libs = intern_library libs (dir, Some f) None in + libs + +let native_name_from_filename f = + let ch = raw_intern_library f in + let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in + Nativecode.mod_uid_of_dirpath lmd.md_name + +(**********************************************************************) +(*s [require_library] loads and possibly opens a library. This is a + synchronized operation. It is performed as follows: + + preparation phase: (functions require_library* ) the library and its + dependencies are read from to disk (using intern_* ) + [they are read from disk to ensure that at section/module + discharging time, the physical library referred to outside the + section/module is the one that was used at type-checking time in + the section/module] + + execution phase: (through add_leaf and cache_require) + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, + which recursively loads its dependencies) +*) + +let register_library m = + let l = fetch_delayed m.library_data in + Declaremods.register_library + m.library_name + l.md_compiled + l.md_objects + m.library_digests + m.library_extra_univs; + register_loaded_library (mk_summary m) + +(* Follow the semantics of Anticipate object: + - called at module or module type closing when a Require occurs in + the module or module type + - not called from a library (i.e. a module identified with a file) *) +let load_require _ (_,(needed,modl,_)) = + List.iter register_library needed + +let open_require i (_,(_,modl,export)) = + Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) + export + + (* [needed] is the ordered list of libraries not already loaded *) +let cache_require o = + load_require 1 o; + open_require 1 o + +let discharge_require (_,o) = Some o + +(* open_function is never called from here because an Anticipate object *) + +type require_obj = library_t list * DirPath.t list * bool option + +let in_require : require_obj -> obj = + declare_object {(default_object "REQUIRE") with + cache_function = cache_require; + load_function = load_require; + open_function = (fun _ _ -> assert false); + discharge_function = discharge_require; + classify_function = (fun o -> Anticipate o) } + +(* Require libraries, import them if [export <> None], mark them for export + if [export = Some true] *) + +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + +let require_library_from_dirpath modrefl export = + let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in + let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in + let modrefl = List.map fst modrefl in + if Lib.is_module_or_modtype () then + begin + warn_require_in_module (); + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun exp -> + add_anonymous_leaf (in_import_library (modrefl,exp))) + export + end + else + add_anonymous_leaf (in_require (needed,modrefl,export)); + () + +(* the function called by Vernacentries.vernac_import *) + +let safe_locate_module qid = + try Nametab.locate_module qid + with Not_found -> + user_err ?loc:qid.CAst.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 + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | qid :: l -> + let m,acc = + try Nametab.locate_module qid, acc + with Not_found-> flush acc; safe_locate_module qid, [] in + (match m with + | MPfile dir -> aux (dir::acc) l + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err ?loc:qid.CAst.loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module")) + | [] -> flush acc + in aux [] modl + +(************************************************************************) +(*s Initializing the compilation of a library. *) + +let load_library_todo f = + let longf = Loadpath.locate_file (f^".v") in + let f = longf^"io" in + let ch = raw_intern_library f in + let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in + let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in + let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in + let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in + 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 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 + +(************************************************************************) +(*s [save_library dir] ends library [dir] and save it to the disk. *) + +let current_deps () = + let map name = + let m = try_find_library name in + (name, m.libsum_digests) + in + List.map map !libraries_loaded_list + +let current_reexports () = !libraries_exports_list + +let error_recursively_dependent_library dir = + user_err + (strbrk "Unable to use logical name " ++ DirPath.print dir ++ + strbrk " to save current library because" ++ + strbrk " it already depends on a library of this name.") + +(* We now use two different digests in a .vo file. The first one + only covers half of the file, without the opaque table. It is + used for identifying this version of this library : this digest + is the one leading to "inconsistent assumptions" messages. + The other digest comes at the very end, and covers everything + before it. This one is used for integrity check of the whole + file when loading the opaque table. *) + +(* Security weakness: file might have been changed on disk between + writing the content and computing the checksum... *) + +let save_library_to ?todo dir f otab = + let except = match todo with + | None -> + (* XXX *) + (* assert(!Flags.compilation_mode = Flags.BuildVo); *) + assert(Filename.check_suffix f ".vo"); + Future.UUIDSet.empty + | Some (l,_) -> + assert(Filename.check_suffix f ".vio"); + List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) + Future.UUIDSet.empty l in + let cenv, seg, ast = Declaremods.end_library ~except dir in + let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in + let tasks, utab, dtab = + match todo with + | None -> None, None, None + | Some (tasks, rcbackup) -> + let tasks = + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in + Some (tasks,rcbackup), + Some (univ_table,Univ.ContextSet.empty,false), + Some disch_table in + let except = + Future.UUIDSet.fold (fun uuid acc -> + try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc + with Not_found -> acc) + 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.user_err ~hdr:"library" + Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) + opaque_table; + let sd = { + md_name = dir; + md_deps = Array.of_list (current_deps ()); + md_imports = Array.of_list (current_reexports ()); + } in + let md = { + md_compiled = cenv; + md_objects = seg; + } in + if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then + error_recursively_dependent_library dir; + (* Open the vo file and write the magic number *) + let f' = f in + let ch = raw_extern_library f' in + try + (* Writing vo payload *) + System.marshal_out_segment f' ch (sd : seg_sum); + System.marshal_out_segment f' ch (md : seg_lib); + System.marshal_out_segment f' ch (utab : seg_univ option); + System.marshal_out_segment f' ch (dtab : seg_discharge option); + System.marshal_out_segment f' ch (tasks : 'tasks option); + System.marshal_out_segment f' ch (opaque_table : seg_proofs); + close_out ch; + (* Writing native code files *) + if !Flags.output_native_objects then + let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in + if not (Nativelib.compile_library dir ast fn) then + 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 + let () = close_out ch in + let () = Sys.remove f' in + iraise reraise + +let save_library_raw f sum lib univs proofs = + let f' = f^"o" in + let ch = raw_extern_library f' in + System.marshal_out_segment f' ch (sum : seg_sum); + System.marshal_out_segment f' ch (lib : seg_lib); + System.marshal_out_segment f' ch (Some univs : seg_univ option); + System.marshal_out_segment f' ch (None : seg_discharge option); + System.marshal_out_segment f' ch (None : 'tasks option); + System.marshal_out_segment f' ch (proofs : seg_proofs); + close_out ch + +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) + +let get_used_load_paths () = + StringSet.elements + (List.fold_left (fun acc m -> StringSet.add + (Filename.dirname (library_full_filename m)) acc) + StringSet.empty !libraries_loaded_list) + +let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/library.mli b/library/library.mli new file mode 100644 index 0000000000..c016352808 --- /dev/null +++ b/library/library.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames + +(** This module provides functions to load, open and save + libraries. Libraries correspond to the subclass of modules that + coincide with a file on disk (the ".vo" files). Libraries on the + disk comes with checksums (obtained with the [Digest] module), which + are checked at loading time to prevent inconsistencies between files + written at various dates. +*) + +(** {6 ... } + Require = load in the environment + open (if the optional boolean + is not [None]); mark also for export if the boolean is [Some true] *) +val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit + +(** {6 Start the compilation of a library } *) + +(** Segments of a library *) +type seg_sum +type seg_lib +type seg_univ = (* cst, all_cst, finished? *) + Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool +type seg_discharge = Opaqueproof.cooking_info list array +type seg_proofs = Constr.constr Future.computation array + +(** Open a module (or a library); if the boolean is true then it's also + an export otherwise just a simple import *) +val import_module : bool -> qualid list -> unit + +(** End the compilation of a library and save it to a ".vo" file *) +val save_library_to : + ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + DirPath.t -> string -> Opaqueproof.opaquetab -> unit + +val load_library_todo : + string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit + +(** {6 Interrogate the status of libraries } *) + + (** - Tell if a library is loaded or opened *) +val library_is_loaded : DirPath.t -> bool +val library_is_opened : DirPath.t -> bool + + (** - Tell which libraries are loaded or imported *) +val loaded_libraries : unit -> DirPath.t list +val opened_libraries : unit -> DirPath.t list + + (** - Return the full filename of a loaded library. *) +val library_full_filename : DirPath.t -> string + + (** - Overwrite the filename of all libraries (used when restoring a state) *) +val overwrite_library_filenames : string -> unit + +(** {6 Locate a library in the load paths } *) +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +val locate_qualified_library : + ?root:DirPath.t -> ?warn:bool -> qualid -> + library_location * DirPath.t * CUnix.physical_path +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) + +(** {6 Native compiler. } *) +val native_name_from_filename : string -> string diff --git a/library/library.mllib b/library/library.mllib new file mode 100644 index 0000000000..8f694f4a31 --- /dev/null +++ b/library/library.mllib @@ -0,0 +1,17 @@ +Libnames +Globnames +Libobject +Summary +Nametab +Global +Decl_kinds +Lib +Declaremods +Loadpath +Library +States +Kindops +Goptions +Decls +Keys +Coqlib diff --git a/library/loadpath.ml b/library/loadpath.ml new file mode 100644 index 0000000000..fc13c864d0 --- /dev/null +++ b/library/loadpath.ml @@ -0,0 +1,119 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open Util +open CErrors +open Names +open Libnames + +(** Load paths. Mapping from physical to logical paths. *) + +type t = { + path_physical : CUnix.physical_path; + path_logical : DirPath.t; + path_implicit : bool; +} + +let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" + +let logical p = p.path_logical + +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 ++ str ".") + +let find_load_path phys_dir = + let phys_dir = CUnix.canonical_path_name phys_dir in + let filter p = String.equal p.path_physical phys_dir in + let paths = List.filter filter !load_paths in + match paths with + | [] -> raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let is_in_load_paths phys_dir = + let dir = CUnix.canonical_path_name phys_dir in + let lp = get_load_paths () in + let check_p p = String.equal dir p.path_physical in + List.exists check_p lp + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + DirPath.print old_path ++ strbrk "; it is remapped to " ++ + DirPath.print coq_path) + +let add_load_path phys_path coq_path ~implicit = + let phys_path = CUnix.canonical_path_name phys_path in + let filter p = String.equal p.path_physical phys_path in + let binding = { + path_logical = coq_path; + path_physical = phys_path; + path_implicit = implicit; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Libnames.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then + begin + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let filter_path f = + let rec aux = function + | [] -> [] + | p :: l -> + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l + else aux l + in + aux !load_paths + +let expand_path ?root dir = + let rec aux = function + | [] -> [] + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then is_dirpath_suffix_of dir lg + else DirPath.equal dir lg + | Some root -> + is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + if success then (ph, lg) :: aux l else aux l in + aux !load_paths + +let locate_file fname = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in + longfname diff --git a/library/loadpath.mli b/library/loadpath.mli new file mode 100644 index 0000000000..4044ca1127 --- /dev/null +++ b/library/loadpath.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** * Load paths. + + A load path is a physical path in the file system; to each load path is + associated a Coq [DirPath.t] (the "logical" path of the physical path). + +*) + +type t +(** Type of loadpath bindings. *) + +val physical : t -> CUnix.physical_path +(** Get the physical path (filesystem location) of a loadpath. *) + +val logical : t -> DirPath.t +(** Get the logical path (Coq module hierarchy) of a loadpath. *) + +val get_load_paths : unit -> t list +(** Get the current loadpath association. *) + +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current + loadpaths. *) + +val remove_load_path : CUnix.physical_path -> unit +(** Remove the current logical path binding associated to a given physical path, + if any. *) + +val find_load_path : CUnix.physical_path -> t +(** Get the binding associated to a physical path. Raises [Not_found] if there + is none. *) + +val is_in_load_paths : CUnix.physical_path -> bool +(** Whether a physical path is currently bound. *) + +val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list +(** Given a relative logical path, associate the list of absolute physical and + logical paths which are possible matches of it. *) + +val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list +(** As {!expand_path} but uses a filter function instead, and ignores the + implicit status of loadpaths. *) + +val locate_file : string -> string +(** Locate a file among the registered paths. Do not use this function, as + it does not respect the visibility of paths. *) diff --git a/library/nametab.ml b/library/nametab.ml new file mode 100644 index 0000000000..95890b2edf --- /dev/null +++ b/library/nametab.ml @@ -0,0 +1,594 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CErrors +open Util +open Pp +open Names +open Libnames +open Globnames + +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} + +let eq_op op1 op2 = + DirPath.equal op1.obj_dir op2.obj_dir && + DirPath.equal op1.obj_sec op2.obj_sec && + ModPath.equal op1.obj_mp op2.obj_mp + +(* to this type are mapped DirPath.t's in the nametab *) +module GlobDirRef = struct + type t = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + + let equal r1 r2 = match r1, r2 with + | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 + | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 + | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 + | DirModule op1, DirModule op2 -> eq_op op1 op2 + | _ -> false + +end + +type global_dir_reference = GlobDirRef.t +[@@ocaml.deprecated "Use [GlobDirRef.t]"] + +let eq_global_dir_reference = GlobDirRef.equal +[@@ocaml.deprecated "Use [GlobDirRef.equal]"] + +exception GlobalizationError of qualid + +let error_global_not_found qid = + Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid) + +(* The visibility can be registered either + - for all suffixes not shorter then a given int - when the object + is loaded inside a module + or + - for a precise suffix, when the module containing (the module + containing ...) the object is open (imported) +*) +type visibility = Until of int | Exactly of int + +let map_visibility f = function + | Until i -> Until (f i) + | Exactly i -> Exactly (f i) + +(* Data structure for nametabs *******************************************) + + +(* This module type will be instantiated by [full_path] of [DirPath.t] *) +(* The [repr] function is assumed to return the reversed list of idents. *) +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 + +(* A ['a t] is a map from [user_name] to ['a], with possible lookup by + partially qualified names of type [qualid]. The mapping of + partially qualified names to ['a] is determined by the [visibility] + parameter of [push]. + + The [shortest_qualid] function given a user_name Coq.A.B.x, tries + to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes + the same object. +*) +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 : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid + val find_prefixes : qualid -> t -> elt list + + (** Matches a prefix of [qualid], useful for completion *) + val match_prefixes : qualid -> t -> elt list +end + +module Make (U : UserName) (E : EqualityType) : NAMETREE + with type user_name = U.t and type elt = E.t = +struct + type elt = E.t + + (* A name became inaccessible, even with absolute qualification. + Example: + Module F (X : S). Module X. + The argument X of the functor F is masked by the inner module X. + *) + let warn_masking_absolute = + CWarnings.create ~name:"masking-absolute-name" ~category:"deprecated" + (fun n -> str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + + type user_name = U.t + + type path_status = + Nothing + | Relative of user_name * elt + | Absolute of user_name * elt + + (* Dictionaries of short names *) + type nametree = + { path : path_status; + map : nametree ModIdmap.t } + + let mktree p m = { path=p; map=m } + let empty_tree = mktree Nothing ModIdmap.empty + + type t = nametree Id.Map.t + + let empty = Id.Map.empty + + (* [push_until] is used to register [Until vis] visibility and + [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*) + + let rec push_until uname o level tree = function + | modid :: path -> + let modify _ mc = push_until uname o (level-1) mc path in + let map = + try ModIdmap.modify modid modify tree.map + with Not_found -> + let ptab = modify () empty_tree in + ModIdmap.add modid ptab tree.map + in + let this = + if level <= 0 then + match tree.path with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) + warn_masking_absolute n; tree.path + | Nothing + | Relative _ -> Relative (uname,o) + else tree.path + in + mktree this map + | [] -> + match tree.path with + | Absolute (uname',o') -> + if E.equal o' o then begin + assert (U.equal uname uname'); + tree + (* we are putting the same thing for the second time :) *) + end + else + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + (* But ours is also absolute! This is an error! *) + user_err Pp.(str @@ "Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") + | Nothing + | Relative _ -> mktree (Absolute (uname,o)) tree.map + +let rec push_exactly uname o level tree = function +| [] -> + anomaly (Pp.str "Prefix longer than path! Impossible!") +| modid :: path -> + if Int.equal level 0 then + let this = + match tree.path with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) + warn_masking_absolute n; tree.path + | Nothing + | Relative _ -> Relative (uname,o) + in + mktree this tree.map + else (* not right level *) + let modify _ mc = push_exactly uname o (level-1) mc path in + let map = + try ModIdmap.modify modid modify tree.map + with Not_found -> + let ptab = modify () empty_tree in + ModIdmap.add modid ptab tree.map + in + mktree tree.path map + + +let push visibility uname o tab = + let id,dir = U.repr uname in + let modify _ ptab = match visibility with + | Until i -> push_until uname o (i-1) ptab dir + | Exactly i -> push_exactly uname o (i-1) ptab dir + in + try Id.Map.modify id modify tab + with Not_found -> + let ptab = modify () empty_tree in + Id.Map.add id ptab tab + + +let rec search tree = function + | modid :: path -> search (ModIdmap.find modid tree.map) path + | [] -> tree.path + +let find_node qid tab = + let (dir,id) = repr_qualid qid in + search (Id.Map.find id tab) (DirPath.repr dir) + +let locate qid tab = + let o = match find_node qid tab with + | Absolute (uname,o) | Relative (uname,o) -> o + | Nothing -> raise Not_found + in + o + +let user_name qid tab = + let uname = match find_node qid tab with + | Absolute (uname,o) | Relative (uname,o) -> uname + | Nothing -> raise Not_found + in + uname + +let find uname tab = + let id,l = U.repr uname in + match search (Id.Map.find id tab) l with + Absolute (_,o) -> o + | _ -> raise Not_found + +let exists uname tab = + try + let _ = find uname tab in + true + with + Not_found -> false + +let shortest_qualid ?loc ctx uname tab = + let id,dir = U.repr uname in + let hidden = Id.Set.mem id ctx in + let rec find_uname pos dir tree = + let is_empty = match pos with [] -> true | _ -> false in + match tree.path with + | Absolute (u,_) | Relative (u,_) + when U.equal u uname && not (is_empty && hidden) -> List.rev pos + | _ -> + match dir with + [] -> raise Not_found + | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map) + in + let ptab = Id.Map.find id tab in + let found_dir = find_uname [] dir ptab in + make_qualid ?loc (DirPath.make found_dir) id + +let push_node node l = + match node with + | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l + | _ -> l + +let rec flatten_idmap tab l = + let f _ tree l = flatten_idmap tree.map (push_node tree.path l) in + ModIdmap.fold f tab l + +let rec search_prefixes tree = function + | modid :: path -> search_prefixes (ModIdmap.find modid tree.map) path + | [] -> List.rev (flatten_idmap tree.map (push_node tree.path [])) + +let find_prefixes qid tab = + try + let (dir,id) = repr_qualid qid in + search_prefixes (Id.Map.find id tab) (DirPath.repr dir) + with Not_found -> [] + +let match_prefixes = + let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in + fun qid tab -> + try + let (dir,id) = repr_qualid qid in + let id_prefix = cprefix Id.(to_string id) in + let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in + let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in + (* Coq's flatten is "magical", so this is not so bad perf-wise *) + CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches []) + with Not_found -> [] + +end + +(* Global name tables *************************************************) + +module FullPath = +struct + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module ExtRefEqual = ExtRefOrdered +module MPEqual = Names.ModPath + +module ExtRefTab = Make(FullPath)(ExtRefEqual) +module MPTab = Make(FullPath)(MPEqual) + +type ccitab = ExtRefTab.t +let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab) + +type mptab = MPTab.t +let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab) + +module DirPath' = +struct + include DirPath + let repr dir = match DirPath.repr dir with + | [] -> anomaly (Pp.str "Empty dirpath.") + | id :: l -> (id, l) +end + +module DirTab = Make(DirPath')(GlobDirRef) + +(* If we have a (closed) module M having a submodule N, than N does not + have the entry in [the_dirtab]. *) +type dirtab = DirTab.t +let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab) + +module UnivIdEqual = +struct + type t = Univ.Level.UGlobal.t + let equal = Univ.Level.UGlobal.equal +end +module UnivTab = Make(FullPath)(UnivIdEqual) +type univtab = UnivTab.t +let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab) + +(* Reversed name tables ***************************************************) + +(* This table translates extended_global_references back to section paths *) +module Globrevtab = HMap.Make(ExtRefOrdered) + +type globrevtab = full_path Globrevtab.t +let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab) + + +type mprevtab = DirPath.t MPmap.t +let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab) + +type mptrevtab = full_path MPmap.t +let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab) + +module UnivIdOrdered = +struct + type t = Univ.Level.UGlobal.t + let hash = Univ.Level.UGlobal.hash + let compare = Univ.Level.UGlobal.compare +end + +module UnivIdMap = HMap.Make(UnivIdOrdered) + +type univrevtab = full_path UnivIdMap.t +let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab) + +(* Push functions *********************************************************) + +(* This is for permanent constructions (never discharged -- but with + possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom, + Parameter but also Remark and Fact) *) + +let push_xref visibility sp xref = + match visibility with + | Until _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + the_globrevtab := Globrevtab.add xref sp !the_globrevtab + | _ -> + begin + if ExtRefTab.exists sp !the_ccitab then + match ExtRefTab.find sp !the_ccitab with + | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | + TrueGlobal( ConstructRef _) as xref -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + | _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + else + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + end + +let push_cci visibility sp ref = + push_xref visibility sp (TrueGlobal ref) + +(* This is for Syntactic Definitions *) +let push_syndef visibility sp kn = + push_xref visibility sp (SynDef kn) + +let push = push_cci + +let push_modtype vis sp kn = + the_modtypetab := MPTab.push vis sp kn !the_modtypetab; + the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab + +(* This is to remember absolute Section/Module names and to avoid redundancy *) +let push_dir vis dir dir_ref = + the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; + match dir_ref with + | GlobDirRef.DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab + | _ -> () + +(* This is for global universe names *) + +let push_universe vis sp univ = + the_univtab := UnivTab.push vis sp univ !the_univtab; + the_univrevtab := UnivIdMap.add univ sp !the_univrevtab + +(* Locate functions *******************************************************) + + +(* This should be used when syntactic definitions are allowed *) +let locate_extended qid = ExtRefTab.locate qid !the_ccitab + +(* This should be used when no syntactic definitions is expected *) +let locate qid = match locate_extended qid with + | TrueGlobal ref -> ref + | SynDef _ -> raise Not_found +let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab + +let locate_syndef qid = match locate_extended qid with + | TrueGlobal _ -> raise Not_found + | SynDef kn -> kn + +let locate_modtype qid = MPTab.locate qid !the_modtypetab +let full_name_modtype qid = MPTab.user_name qid !the_modtypetab + +let locate_universe qid = UnivTab.locate qid !the_univtab + +let locate_dir qid = DirTab.locate qid !the_dirtab + +let locate_module qid = + match locate_dir qid with + | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp + | _ -> raise Not_found + +let full_name_module qid = + match locate_dir qid with + | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir + | _ -> raise Not_found + +let locate_section qid = + match locate_dir qid with + | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir + | _ -> raise Not_found + +let locate_all qid = + List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) + (ExtRefTab.find_prefixes qid !the_ccitab) [] + +let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab + +let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab + +let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab + +(* Completion *) +let completion_canditates qualid = + ExtRefTab.match_prefixes qualid !the_ccitab + +(* Derived functions *) + +let locate_constant qid = + match locate_extended qid with + | TrueGlobal (ConstRef kn) -> kn + | _ -> raise Not_found + +let global_of_path sp = + match ExtRefTab.find sp !the_ccitab with + | TrueGlobal ref -> ref + | _ -> raise Not_found + +let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab + +let global qid = + try match locate_extended qid with + | TrueGlobal ref -> ref + | SynDef _ -> + user_err ?loc:qid.CAst.loc ~hdr:"global" + (str "Unexpected reference to a notation: " ++ + pr_qualid qid) + with Not_found -> + error_global_not_found qid + +(* Exists functions ********************************************************) + +let exists_cci sp = ExtRefTab.exists sp !the_ccitab + +let exists_dir dir = DirTab.exists dir !the_dirtab + +let exists_section = exists_dir + +let exists_module = exists_dir + +let exists_modtype sp = MPTab.exists sp !the_modtypetab + +let exists_universe kn = UnivTab.exists kn !the_univtab + +(* Reverse locate functions ***********************************************) + +let path_of_global ref = + match ref with + | VarRef id -> make_path DirPath.empty id + | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab + +let dirpath_of_global ref = + fst (repr_path (path_of_global ref)) + +let basename_of_global ref = + snd (repr_path (path_of_global ref)) + +let path_of_syndef kn = + Globrevtab.find (SynDef kn) !the_globrevtab + +let dirpath_of_module mp = + MPmap.find mp !the_modrevtab + +let path_of_modtype mp = + MPmap.find mp !the_modtyperevtab + +let path_of_universe mp = + UnivIdMap.find mp !the_univrevtab + +(* Shortest qualid functions **********************************************) + +let shortest_qualid_of_global ?loc ctx ref = + match ref with + | VarRef id -> make_qualid ?loc DirPath.empty id + | _ -> + let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab + +let shortest_qualid_of_syndef ?loc ctx kn = + let sp = path_of_syndef kn in + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab + +let shortest_qualid_of_module ?loc mp = + let dir = MPmap.find mp !the_modrevtab in + DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab + +let shortest_qualid_of_modtype ?loc kn = + let sp = MPmap.find kn !the_modtyperevtab in + MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab + +let shortest_qualid_of_universe ?loc kn = + let sp = UnivIdMap.find kn !the_univrevtab in + UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + +let pr_global_env env ref = + try pr_qualid (shortest_qualid_of_global env ref) + with Not_found as e -> + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e + +let global_inductive qid = + match global qid with + | IndRef ind -> ind + | ref -> + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type") + +(********************************************************************) + +(* Deprecated synonyms *) + +let extended_locate = locate_extended +let absolute_reference = global_of_path diff --git a/library/nametab.mli b/library/nametab.mli new file mode 100644 index 0000000000..fccb8fd918 --- /dev/null +++ b/library/nametab.mli @@ -0,0 +1,262 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames +open Globnames + +(** This module contains the tables for globalization. *) + +(** These globalization tables associate internal object references to + qualified names (qualid). There are three classes of names: + + - 1a) internal kernel names: [kernel_name], [constant], [inductive], + [module_path], [DirPath.t] + + - 1b) other internal names: [global_reference], [syndef_name], + [extended_global_reference], [global_dir_reference], ... + + - 2) full, non ambiguous user names: [full_path] + + - 3) non necessarily full, possibly ambiguous user names: [reference] + and [qualid] +*) + +(** Most functions in this module fall into one of the following categories: +{ul {- [push : visibility -> full_user_name -> object_reference -> unit] + + Registers the [object_reference] to be referred to by the + [full_user_name] (and its suffixes according to [visibility]). + [full_user_name] can either be a [full_path] or a [DirPath.t]. + } + {- [exists : full_user_name -> bool] + + Is the [full_user_name] already atributed as an absolute user name + of some object? + } + {- [locate : qualid -> object_reference] + + Finds the object referred to by [qualid] or raises [Not_found] + } + {- [full_name : qualid -> full_user_name] + + Finds the full user name referred to by [qualid] or raises [Not_found] + } + {- [shortest_qualid_of : object_reference -> user_name] + + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [Id.t]. Such a function can also have a + local context argument.}} + +*) + +(** Object prefix morally contains the "prefix" naming of an object to + be stored by [library], where [obj_dir] is the "absolute" path, + [obj_mp] is the current "module" prefix and [obj_sec] is the + "section" prefix. + + Thus, for an object living inside [Module A. Section B.] the + prefix would be: + + [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ] + + Note that both [obj_dir] and [obj_sec] are "paths" that is to say, + as opposed to [obj_mp] which is a single module name. + + *) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} + +val eq_op : object_prefix -> object_prefix -> bool + +(** to this type are mapped [DirPath.t]'s in the nametab *) +module GlobDirRef : sig + type t = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + val equal : t -> t -> bool +end + +type global_dir_reference = GlobDirRef.t +[@@ocaml.deprecated "Use [GlobDirRef.t]"] + +val eq_global_dir_reference : + GlobDirRef.t -> GlobDirRef.t -> bool +[@@ocaml.deprecated "Use [GlobDirRef.equal]"] + +exception GlobalizationError of qualid + +(** Raises a globalization error *) +val error_global_not_found : qualid -> 'a + +(** {6 Register visibility of things } *) + +(** The visibility can be registered either + - for all suffixes not shorter then a given int -- when the + object is loaded inside a module -- or + - for a precise suffix, when the module containing (the module + containing ...) the object is opened (imported) + +*) + +type visibility = Until of int | Exactly of int + +val map_visibility : (int -> int) -> visibility -> visibility + +val push : visibility -> full_path -> GlobRef.t -> unit +val push_modtype : visibility -> full_path -> ModPath.t -> unit +val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit +val push_syndef : visibility -> full_path -> syndef_name -> unit + +module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t + +val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit + +(** {6 The following functions perform globalization of qualified names } *) + +(** These functions globalize a (partially) qualified name or fail with + [Not_found] *) + +val locate : qualid -> GlobRef.t +val locate_extended : qualid -> extended_global_reference +val locate_constant : qualid -> Constant.t +val locate_syndef : qualid -> syndef_name +val locate_modtype : qualid -> ModPath.t +val locate_dir : qualid -> GlobDirRef.t +val locate_module : qualid -> ModPath.t +val locate_section : qualid -> DirPath.t +val locate_universe : qualid -> Univ.Level.UGlobal.t + +(** These functions globalize user-level references into global + references, like [locate] and co, but raise a nice error message + in case of failure *) + +val global : qualid -> GlobRef.t +val global_inductive : qualid -> inductive + +(** These functions locate all global references with a given suffix; + if [qualid] is valid as such, it comes first in the list *) + +val locate_all : qualid -> GlobRef.t list +val locate_extended_all : qualid -> extended_global_reference list +val locate_extended_all_dir : qualid -> GlobDirRef.t list +val locate_extended_all_modtype : qualid -> ModPath.t list + +(** Experimental completion support, API is _unstable_ *) +val completion_canditates : qualid -> extended_global_reference list +(** [completion_canditates qualid] will return the list of global + references that have [qualid] as a prefix. UI usually will want to + compose this with [shortest_qualid_of_global] *) + +(** Mapping a full path to a global reference *) + +val global_of_path : full_path -> GlobRef.t +val extended_global_of_path : full_path -> extended_global_reference + +(** {6 These functions tell if the given absolute name is already taken } *) + +val exists_cci : full_path -> bool +val exists_modtype : full_path -> bool +val exists_dir : DirPath.t -> bool +val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) + +val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) + +val exists_universe : full_path -> bool + +(** {6 These functions locate qualids into full user names } *) + +val full_name_cci : qualid -> full_path +val full_name_modtype : qualid -> full_path +val full_name_module : qualid -> DirPath.t + +(** {6 Reverse lookup } + Finding user names corresponding to the given + internal name *) + +(** Returns the full path bound to a global reference or syntactic + definition, and the (full) dirpath associated to a module path *) + +val path_of_syndef : syndef_name -> full_path +val path_of_global : GlobRef.t -> full_path +val dirpath_of_module : ModPath.t -> DirPath.t +val path_of_modtype : ModPath.t -> full_path + +(** A universe_id might not be registered with a corresponding user name. + @raise Not_found if the universe was not introduced by the user. *) +val path_of_universe : Univ.Level.UGlobal.t -> full_path + +(** Returns in particular the dirpath or the basename of the full path + associated to global reference *) + +val dirpath_of_global : GlobRef.t -> DirPath.t +val basename_of_global : GlobRef.t -> Id.t + +(** Printing of global references using names as short as possible. + @raise Not_found when the reference is not in the global tables. *) +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t + + +(** The [shortest_qualid] functions given an object with [user_name] + Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and + Coq.A.B.x that denotes the same object. + @raise Not_found for unknown objects. *) + +val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid +val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid +val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid + +(** Deprecated synonyms *) + +val extended_locate : qualid -> extended_global_reference (*= locate_extended *) +val absolute_reference : full_path -> GlobRef.t (** = 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 : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid + val find_prefixes : qualid -> t -> elt list + val match_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/states.ml b/library/states.ml new file mode 100644 index 0000000000..92bdc410a3 --- /dev/null +++ b/library/states.ml @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open System + +type state = Lib.frozen * Summary.frozen + +let lib_of_state = fst +let summary_of_state = snd +let replace_summary (lib,_) st = lib, st +let replace_lib (_,st) lib = lib, st + +let freeze ~marshallable = + (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) + +let unfreeze (fl,fs) = + Lib.unfreeze fl; + Summary.unfreeze_summaries fs + +let extern_state s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) + +let intern_state s = + unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s + +(* Rollback. *) + +let with_state_protection f x = + let st = freeze ~marshallable:false in + try + let a = f x in unfreeze st; a + with reraise -> + let reraise = CErrors.push reraise in + (unfreeze st; iraise reraise) diff --git a/library/states.mli b/library/states.mli new file mode 100644 index 0000000000..52feb95222 --- /dev/null +++ b/library/states.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** {6 States of the system} *) + +(** In that module, we provide functions to get + and set the state of the whole system. Internally, it is done by + freezing the states of both [Lib] and [Summary]. We provide functions + to write and restore state to and from a given file. *) + +val intern_state : string -> unit +val extern_state : string -> unit + +type state +val freeze : marshallable:bool -> state +val unfreeze : state -> unit + +val summary_of_state : state -> Summary.frozen +val lib_of_state : state -> Lib.frozen +val replace_summary : state -> Summary.frozen -> state +val replace_lib : state -> Lib.frozen -> state + +(** {6 Rollback } *) + +(** [with_state_protection f x] applies [f] to [x] and restores the + state of the whole system as it was before applying [f] *) + +val with_state_protection : ('a -> 'b) -> 'a -> 'b + diff --git a/library/summary.ml b/library/summary.ml new file mode 100644 index 0000000000..8fbca44353 --- /dev/null +++ b/library/summary.ml @@ -0,0 +1,165 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util + +module Dyn = Dyn.Make () + +type 'a summary_declaration = { + freeze_function : marshallable:bool -> 'a; + unfreeze_function : 'a -> unit; + init_function : unit -> unit } + +let sum_mod = ref None +let sum_map = ref String.Map.empty + +let mangle id = id ^ "-SUMMARY" +let unmangle id = String.(sub id 0 (length id - 8)) + +let ml_modules = "ML-MODULES" + +let internal_declare_summary fadd sumname sdecl = + let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in + let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable) + and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) + and dyn_init = sdecl.init_function in + let ddecl = { + freeze_function = dyn_freeze; + unfreeze_function = dyn_unfreeze; + init_function = dyn_init } + in + fadd sumname ddecl; + tag + +let declare_ml_modules_summary decl = + let ml_add _ ddecl = sum_mod := Some ddecl in + internal_declare_summary ml_add ml_modules decl + +let declare_ml_modules_summary decl = + ignore(declare_ml_modules_summary decl) + +let declare_summary_tag sumname decl = + let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in + let () = if String.Map.mem sumname !sum_map then + anomaly ~label:"Summary.declare_summary" + (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".") + in + internal_declare_summary fadd sumname decl + +let declare_summary sumname decl = + ignore(declare_summary_tag sumname decl) + +type frozen = { + summaries : Dyn.t String.Map.t; + (** Ordered list w.r.t. the first component. *) + ml_module : Dyn.t option; + (** Special handling of the ml_module summary. *) +} + +let empty_frozen = { summaries = String.Map.empty; ml_module = None } + +let freeze_summaries ~marshallable : frozen = + let smap decl = decl.freeze_function ~marshallable in + { summaries = String.Map.map smap !sum_map; + ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod; + } + +let warn_summary_out_of_scope = + let name = "summary-out-of-scope" in + let category = "dev" in + let default = CWarnings.Disabled in + CWarnings.create ~name ~category ~default (fun name -> + Pp.str (Printf.sprintf + "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s" + name) + ) + +let unfreeze_summaries ?(partial=false) { summaries; ml_module } = + (* The unfreezing of [ml_modules_summary] has to be anticipated since it + * may modify the content of [summaries] by loading new ML modules *) + begin match !sum_mod with + | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") + | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module + end; + (* We must be independent on the order of the map! *) + let ufz name decl = + try decl.unfreeze_function String.Map.(find name summaries) + with Not_found -> + if not partial then begin + warn_summary_out_of_scope name; + decl.init_function () + end; + in + (* String.Map.iter unfreeze_single !sum_map *) + String.Map.iter ufz !sum_map + +let init_summaries () = + String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map + +(** For global tables registered statically before the end of coqtop + launch, the following empty [init_function] could be used. *) + +let nop () = () + +(** Summary projection *) +let project_from_summary { summaries } tag = + let id = unmangle (Dyn.repr tag) in + let state = String.Map.find id summaries in + Option.get (Dyn.Easy.prj state tag) + +let modify_summary st tag v = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in + {st with summaries} + +let remove_from_summary st tag = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.remove id st.summaries in + {st with summaries} + +(** All-in-one reference declaration + registration *) + +let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x = + let r = ref x in + let tag = declare_summary_tag name + { freeze_function = (fun ~marshallable -> freeze ~marshallable !r); + unfreeze_function = ((:=) r); + init_function = (fun () -> r := x) } in + r, tag + +let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x + +module Local = struct + +type 'a local_ref = ('a CEphemeron.key * string) ref + +let (:=) r v = r := (CEphemeron.create v, snd !r) + +let (!) r = + let key, name = !r in + try CEphemeron.get key + with CEphemeron.InvalidKey -> + let { init_function } = String.Map.find name !sum_map in + init_function (); + CEphemeron.get (fst !r) + +let ref ?(freeze=fun x -> x) ~name init = + let r = Pervasives.ref (CEphemeron.create init, name) in + declare_summary name + { freeze_function = (fun ~marshallable -> freeze !r); + unfreeze_function = ((:=) r); + init_function = (fun () -> r := init) }; + r + +end + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli new file mode 100644 index 0000000000..0d77d725ac --- /dev/null +++ b/library/summary.mli @@ -0,0 +1,90 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module registers the declaration of global tables, which will be kept + in synchronization during the various backtracks of the system. *) + +(** Types of global Coq states. The ['a] type should be pure and marshallable by + the standard OCaml marshalling function. *) +type 'a summary_declaration = { + freeze_function : marshallable:bool -> 'a; + (** freeze_function [true] is for marshalling to disk. + * e.g. lazy must be forced *) + unfreeze_function : 'a -> unit; + init_function : unit -> unit } + +(** For tables registered during the launch of coqtop, the [init_function] + will be run only once, during an [init_summaries] done at the end of + coqtop initialization. For tables registered later (for instance + during a plugin dynlink), [init_function] is used when unfreezing + an earlier frozen state that doesn't contain any value for this table. + + Beware: for tables registered dynamically after the initialization + of Coq, their init functions may not be run immediately. It is hence + the responsability of plugins to initialize themselves properly. +*) + +val declare_summary : string -> 'a summary_declaration -> unit + +(** We provide safe projection from the summary to the types stored in + it.*) +module Dyn : Dyn.S + +val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag + +(** All-in-one reference declaration + summary registration. + It behaves just as OCaml's standard [ref] function, except + that a [declare_summary] is done, with [name] as string. + The [init_function] restores the reference to its initial value. + The [freeze_function] can be overridden *) + +val ref : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag + +(* As [ref] but the value is local to a process, i.e. not sent to, say, proof + * workers. It is useful to implement a local cache for example. *) +module Local : sig + + type 'a local_ref + val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val (:=) : 'a local_ref -> 'a -> unit + val (!) : 'a local_ref -> 'a + +end + +(** Special summary for ML modules. This summary entry is special + because its unfreeze may load ML code and hence add summary + entries. Thus is has to be recognizable, and handled properly. + *) +val declare_ml_modules_summary : 'a summary_declaration -> unit + +(** For global tables registered statically before the end of coqtop + launch, the following empty [init_function] could be used. *) + +val nop : unit -> unit + +(** The type [frozen] is a snapshot of the states of all the registered + tables of the system. *) + +type frozen + +val empty_frozen : frozen +val freeze_summaries : marshallable:bool -> frozen +val unfreeze_summaries : ?partial:bool -> frozen -> unit +val init_summaries : unit -> unit + +(** Typed projection of the summary. Experimental API, use with CARE *) + +val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen +val project_from_summary : frozen -> 'a Dyn.tag -> 'a +val remove_from_summary : frozen -> 'a Dyn.tag -> frozen + +(** {6 Debug} *) +val dump : unit -> (int * string) list |