diff options
Diffstat (limited to 'library')
37 files changed, 991 insertions, 888 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 9ce22b09..adc7f8ed 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,6 +22,8 @@ open Term open Declarations open Mod_subst +let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2) + type context_object = | Variable of identifier (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) @@ -34,10 +36,8 @@ struct let compare x y = match x , y with | Variable i1 , Variable i2 -> id_ord i1 i2 - | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2 - (* spiwack: it would probably be cleaner - to provide a [kn_ord] function *) - | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2 + | Axiom k1 , Axiom k2 -> cst_ord k1 k2 + | Opaque k1 , Opaque k2 -> cst_ord k1 k2 | Variable _ , Axiom _ -> -1 | Axiom _ , Variable _ -> 1 | Opaque _ , _ -> -1 @@ -142,7 +142,7 @@ let lookup_constant_in_impl cst fallback = let lookup_constant cst = try let cb = Global.lookup_constant cst in - if cb.const_body <> None then cb + if constant_has_body cb then cb else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None @@ -211,20 +211,20 @@ let assumptions ?(add_opaque=false) st (* t *) = let cb = lookup_constant kn in let do_type cst = let ctype = - match cb.const_type with + match cb.Declarations.const_type with | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) | NonPolymorphicType t -> t in (s,ContextObjectMap.add cst ctype acc) in let (s,acc) = - if add_opaque && cb.const_body <> None - && (cb.const_opaque || not (Cpred.mem kn knst)) + if add_opaque && Declarations.constant_has_body cb + && (Declarations.is_opaque cb || not (Cpred.mem kn knst)) then do_type (Opaque kn) else (s,acc) in - match cb.const_body with + match Declarations.body_of_constant cb with | None -> do_type (Axiom kn) | Some body -> do_constr (Declarations.force body) s acc diff --git a/library/assumptions.mli b/library/assumptions.mli index d0c185d3..1e3e9ef8 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 20690fa8..ba40f98c 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Libnames @@ -17,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -54,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -86,12 +82,12 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (l,boxed,d) = - match (l,d) with +let string_of_definition_kind def = + match def with | Local, Coercion -> "Coercion Local" | Global, Coercion -> "Coercion" | Local, Definition -> "Let" - | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Global, Definition -> "Definition" | Local, SubClass -> "Local SubClass" | Global, SubClass -> "SubClass" | Global, CanonicalStructure -> "Canonical Structure" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 38e83b1e..88ef763c 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -1,24 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Libnames -(* Informal mathematical status of declarations *) +(** Informal mathematical status of declarations *) type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -44,7 +40,7 @@ type definition_object_kind = type assumption_object_kind = Definitional | Logical | Conjectural -(* [assumption_kind] +(** [assumption_kind] | Local | Global ------------------------------------ @@ -54,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind -(* Kinds used in proofs *) +(** Kinds used in proofs *) type goal_object_kind = | DefinitionBody of definition_object_kind @@ -64,31 +60,31 @@ type goal_object_kind = type goal_kind = locality * goal_object_kind -(* Kinds used in library *) +(** Kinds used in library *) type logical_kind = | IsAssumption of assumption_object_kind | IsDefinition of definition_object_kind | IsProof of theorem_kind -(* Utils *) +(** Utils *) val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : - locality * boxed_flag * definition_object_kind -> string + locality * definition_object_kind -> string -(* About locality *) +(** About locality *) val strength_of_global : global_reference -> locality val string_of_strength : locality -> string -(* About recursive power of type declarations *) +(** About recursive power of type declarations *) type recursivity_kind = - | Finite (* = inductive *) - | CoFinite (* = coinductive *) - | BiFinite (* = non-recursive, like in "Record" definitions *) + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) -(* helper, converts to "finiteness flag" booleans *) +(** helper, converts to "finiteness flag" booleans *) val recursivity_flag_of_kind : recursivity_kind -> bool diff --git a/library/declare.ml b/library/declare.ml index 14cddd6c..28858085 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (** This module is about the low-level declaration of logical objects *) open Pp @@ -80,7 +78,10 @@ let discharge_variable (_,o) = match o with | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (inVariable,_) = +type variable_obj = + (Univ.constraints, identifier * variable_declaration) union + +let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -105,20 +106,26 @@ type constant_declaration = constant_entry * logical_kind let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then alreadydeclared (pr_id (basename sp) ++ str " already exists"); - let con = Global.constant_of_delta (constant_of_kn kn) in + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); add_constant_kind con kind (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - let con = Global.constant_of_delta (constant_of_kn kn) in + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Exactly i) sp (ConstRef con) +let exists_name id = + variable_exists id or Global.exists_label (label_of_id id) + +let check_exists sp = + let id = basename sp in + if exists_name id then alreadydeclared (pr_id id ++ str " already exists") + let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in - if variable_exists id or Nametab.exists_cci sp then - alreadydeclared (pr_id id ++ str " already exists"); + check_exists sp; let kn' = Global.add_constant dir id cdt in assert (kn' = constant_of_kn kn); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); @@ -141,13 +148,16 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) +let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant,_) = +type constant_obj = + global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind + +let inConstant : constant_obj -> obj = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -156,35 +166,19 @@ let (inConstant,_) = subst_function = ident_subst_function; discharge_function = discharge_constant } -let hcons_constant_declaration = function - | DefinitionEntry ce when !Flags.hash_cons_proofs -> - let (hcons1_constr,_) = hcons_constr (hcons_names()) in - DefinitionEntry - { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; - const_entry_boxed = ce.const_entry_boxed } - | cd -> cd - let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in - let c = Global.constant_of_delta (constant_of_kn kn) in + let c = Global.constant_of_delta_kn kn in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); c -let declare_constant_gen internal id (cd,kind) = - let cd = hcons_constant_declaration cd in +let declare_constant ?(internal = UserVerbose) id (cd,kind) = let kn = declare_constant_common id [] (ConstantEntry cd,kind) in !xml_declare_constant (internal,kn); kn -(* TODO: add a third function to distinguish between KernelVerbose - * and user Verbose *) -let declare_internal_constant = declare_constant_gen KernelSilent -let declare_constant = declare_constant_gen UserVerbose - (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = @@ -196,7 +190,7 @@ let declare_inductive_argument_scopes kn mie = let inductive_names sp kn mie = let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta (mind_of_kn kn) in + let kn = Global.mind_of_delta_kn kn in let names, _ = List.fold_left (fun (names, n) ind -> @@ -215,16 +209,8 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names -let check_exists_inductive (sp,_) = - (if variable_exists (basename sp) then - alreadydeclared (pr_id (basename sp) ++ str " already exists")); - if Nametab.exists_cci sp then - let (_,id) = repr_path sp in - alreadydeclared (pr_id id ++ str " already exists") - let load_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in - List.iter check_exists_inductive names; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names let open_inductive i ((sp,kn),(_,mie)) = @@ -233,7 +219,7 @@ let open_inductive i ((sp,kn),(_,mie)) = let cache_inductive ((sp,kn),(dhyps,mie)) = let names = inductive_names sp kn mie in - List.iter check_exists_inductive names; + List.iter check_exists (List.map fst names); let id = basename sp in let _,dir,_ = repr_kn kn in let kn' = Global.add_mind dir id mie in @@ -245,7 +231,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let discharge_inductive ((sp,kn),(dhyps,mie)) = - let mind = (Global.mind_of_delta (mind_of_kn kn)) in + let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let sechyps = section_segment_of_mutual_inductive mind in @@ -266,7 +252,9 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let (inInductive,_) = +type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry + +let inInductive : inductive_obj -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -281,7 +269,7 @@ let declare_mind isrecord mie = | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in - let mind = (Global.mind_of_delta (mind_of_kn kn)) in + let mind = Global.mind_of_delta_kn kn in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; !xml_declare_inductive (isrecord,oname); diff --git a/library/declare.mli b/library/declare.mli index 1ada7cc9..61c19996 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Term @@ -19,9 +16,8 @@ open Indtypes open Safe_typing open Nametab open Decl_kinds -(*i*) -(* This module provides the official functions to declare new variables, +(** This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions will add the entries in the global environment (module [Global]), will register the declarations in the library (module [Lib]) --- so that the @@ -30,54 +26,57 @@ open Decl_kinds open Nametab -(* Declaration of local constructions (Variable/Hypothesis/Local) *) +(** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool (* Implicit status *) + | SectionLocalDef of constr * types option * bool (** opacity *) + | SectionLocalAssum of types * bool (** Implicit status *) type variable_declaration = dir_path * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name -(* Declaration of global constructions *) -(* i.e. Definition/Theorem/Axiom/Parameter/... *) +(** Declaration of global constructions + i.e. Definition/Theorem/Axiom/Parameter/... *) type constant_declaration = constant_entry * logical_kind -(* [declare_constant id cd] declares a global declaration +(** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration *) + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent + + *) type internal_flag = | KernelVerbose | KernelSilent | UserVerbose val declare_constant : - identifier -> constant_declaration -> constant - -val declare_internal_constant : - identifier -> constant_declaration -> constant + ?internal:internal_flag -> identifier -> constant_declaration -> constant -(* [declare_mind me] declares a block of inductive types with +(** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block (boolean must be true iff it is a record) *) val declare_mind : internal_flag -> mutual_inductive_entry -> object_name -(* Hooks for XML output *) +(** Hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit -(* Hook for the cache function of constants and inductives *) +(** Hook for the cache function of constants and inductives *) val add_cache_hook : (full_path -> unit) -> unit -(* Declaration messages *) +(** Declaration messages *) val definition_message : identifier -> unit val assumption_message : identifier -> unit val fixpoint_message : int array option -> identifier list -> unit val cofixpoint_message : identifier list -> unit -val recursive_message : bool (* true = fixpoint *) -> +val recursive_message : bool (** true = fixpoint *) -> int array option -> identifier list -> unit +val exists_name : identifier -> bool diff --git a/library/declaremods.ml b/library/declaremods.ml index 7d996a66..90d4245a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Util open Names @@ -19,8 +17,55 @@ open Lib open Nametab open Mod_subst -(* modules and components *) +(** Rigid / flexible signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Should we adapt a few scopes during functor application ? *) + +type scope_subst = (string * string) list + +let scope_subst = ref (Stringmap.empty : string Stringmap.t) + +let add_scope_subst sc sc' = + scope_subst := Stringmap.add sc sc' !scope_subst + +let register_scope_subst scl = + List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl + +let subst_scope sc = + try Stringmap.find sc !scope_subst with Not_found -> sc + +let reset_scope_subst () = + scope_subst := Stringmap.empty + +(** Which 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 + +let default_inline () = Some (Flags.get_inline_level ()) + +let inl2intopt = function + | NoInline -> None + | InlineAt i -> Some i + | DefaultInline -> default_inline () + +type funct_app_annot = + { ann_inline : inline; + ann_scope_subst : scope_subst } +let inline_annot a = inl2intopt a.ann_inline + +type 'a annotated = ('a * funct_app_annot) + + +(* modules and components *) (* OBSOLETE This type is a functional closure of substitutive lib_objects. @@ -80,7 +125,8 @@ let modtab_objects = let openmod_info = ref ((MPfile(initial_dir),[],None,[]) : module_path * mod_bound_id list * - (module_struct_entry * bool) option * module_type_body list) + (module_struct_entry * int option) option * + module_type_body list) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -133,15 +179,21 @@ let check_sub mtb sub_mtb_l = environment. *) let check_subtypes mp sub_mtb_l = - let env = Global.env () in - let mb = Environ.lookup_module mp env in - let mtb = Modops.module_type_of_module env None mb in + let mb = + try Global.lookup_module mp + with Not_found -> assert false + in + let mtb = Modops.module_type_of_module None mb in check_sub mtb sub_mtb_l (* Same for module type [mp] *) let check_subtypes_mt mp sub_mtb_l = - check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l + let mtb = + try Global.lookup_modtype mp + with Not_found -> assert false + in + check_sub mtb sub_mtb_l (* Create a functor type entry *) @@ -154,7 +206,8 @@ let funct_entry args m = let build_subtypes interp_modtype mp args mtys = List.map - (fun (m,inl) -> + (fun (m,ann) -> + let inl = inline_annot ann in let mte = interp_modtype (Global.env()) m in let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in let funct_mtb = @@ -228,43 +281,27 @@ let conv_names_do_module exists what iter_objects i functions can be called only once (and "end_mod*" set the flag to false then) *) -let cache_module ((sp,kn),(entry,substobjs)) = +let cache_module ((sp,kn),substobjs) = let dir,mp = dir_of_sp sp, mp_of_kn kn in do_module false "cache" load_objects 1 dir mp substobjs [] - -(* TODO: This check is not essential *) -let check_empty s = function - | None -> () - | Some _ -> - anomaly ("We should never have full info in " ^ s^"!") - (* When this function is called the module itself is already in the environment. This function loads its objects only *) -let load_module i (oname,(entry,substobjs)) = - (* TODO: This check is not essential *) - check_empty "load_module" entry; +let load_module i (oname,substobjs) = conv_names_do_module false "load" load_objects i oname substobjs - -let open_module i (oname,(entry,substobjs)) = - (* TODO: This check is not essential *) - check_empty "open_module" entry; +let open_module i (oname,substobjs) = conv_names_do_module true "open" open_objects i oname substobjs +let subst_module (subst,(mbids,mp,objs)) = + (mbids,subst_mp subst mp, subst_objects subst objs) +let classify_module substobjs = Substitute substobjs -let subst_module (subst,(entry,(mbids,mp,objs))) = - check_empty "subst_module" entry; - (None,(mbids,subst_mp subst mp, subst_objects subst objs)) - - -let classify_module (_,substobjs) = - Substitute (None,substobjs) - -let (in_module,out_module) = - declare_object {(default_object "MODULE") with +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; @@ -291,7 +328,7 @@ let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,empty_dirpath)) seg -let (in_modkeep,_) = +let in_modkeep : lib_objects -> obj = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; @@ -323,6 +360,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let mp = mp_of_kn kn in + (* We enrich the global environment *) let _ = match entry with | None -> @@ -346,7 +384,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = - check_empty "load_modtype" entry; + assert (entry = None); if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" @@ -358,7 +396,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = let open_modtype i ((sp,kn),(entry,_,_)) = - check_empty "open_modtype" entry; + assert (entry = None); if try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) @@ -370,15 +408,18 @@ let open_modtype i ((sp,kn),(entry,_,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = - check_empty "subst_modtype" entry; + assert (entry = None); (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) - let classify_modtype (_,substobjs,_) = Substitute (None,substobjs,[]) +type modtype_obj = + (module_struct_entry * Entries.inline) option (* will be None in vo *) + * substitutive_objects + * module_type_body list -let (in_modtype,_) = +let in_modtype : modtype_obj -> obj = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; open_function = open_modtype; @@ -386,36 +427,27 @@ let (in_modtype,_) = subst_function = subst_modtype; classify_function = classify_modtype } +let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 = + if mbids<>[] then anomaly "Unexpected functor objects"; + let rec replace_idl = function + | _,[] -> [] + | id::idl,(id',obj)::tail when id = id' -> + if object_tag obj <> "MODULE" then anomaly "MODULE expected!"; + let substobjs = + if idl = [] then + let mp' = MPdot(mp, label_of_id id) in + mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs + else + replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp + in + (id, in_module substobjs)::tail + | idl,lobj::tail -> lobj::replace_idl (idl,tail) + in + (mbids, mp, replace_idl (idl,lib_stack)) -let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1= - if mbids<>[] then - error "Unexpected functor objects" - else - let rec replace_idl = function - | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj = "MODULE" then - (match idl with - [] -> (id, in_module - (None,(mbids,(MPdot(mp,label_of_id id)),subst_objects - (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail - | _ -> - let (_,substobjs) = out_module obj in - let substobjs' = replace_module_object idl substobjs - (mbids2,mp2,objs) mp in - (id, in_module (None,substobjs'))::tail - ) - else error "MODULE expected!" - | idl,lobj::tail -> lobj::replace_idl (idl,tail) - in - (mbids, mp, replace_idl (idl,lib_stack)) - -let discr_resolver mb = - match mb.mod_type with - SEBstruct _ -> - Some mb.mod_delta - | _ -> (*case mp is a functor *) - None +let discr_resolver mb = match mb.mod_type with + | SEBstruct _ -> Some mb.mod_delta + | _ -> None (* when mp is a functor *) (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_modtype_application env = function @@ -428,24 +460,20 @@ let rec get_objs_modtype_application env = function Modops.error_application_to_not_path mexpr | _ -> error "Application of a non-functor." -let rec compute_subst env mbids sign mp_l inline = +let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst | [],r -> error "Application of a functor with too few arguments." | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in - match discr_resolver mb with - | None -> - mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = match discr_resolver mb with + | None -> empty_delta_resolver | Some mp_delta -> - let mp_delta = - if not inline then mp_delta else - Modops.complete_inline_delta_resolver env mp - farg_id farg_b mp_delta - in - mbid_left,join (map_mbid mbid mp mp_delta) subst + Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta + in + mbid_left,join (map_mbid mbid mp resolver) subst let rec get_modtype_substobjs env mp_from inline = function MSEident ln -> @@ -472,20 +500,39 @@ let rec get_modtype_substobjs env mp_from inline = function (* push names of bound modules (and their components) to Nametab *) (* add objects associated to them *) let process_module_bindings argids args = - let process_arg id (mbid,(mty,inl)) = + let process_arg id (mbid,(mty,ann)) = let dir = make_dirpath [id] in let mp = MPbound mbid in let (mbids,mp_from,objs) = - get_modtype_substobjs (Global.env()) mp inl mty in + get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in let substobjs = (mbids,mp,subst_objects (map_mp mp_from mp empty_delta_resolver) objs)in do_module false "start" load_objects 1 dir mp substobjs [] in List.iter2 process_arg argids args -let intern_args interp_modtype (idl,(arg,inl)) = +(* Same with module_type_body *) + +let rec seb2mse = function + | SEBident mp -> MSEident mp + | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s') + | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) + | SEBwith (s,With_definition_body(l,cb)) -> + (match cb.const_body with + | Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c)) + | _ -> assert false) + | _ -> failwith "seb2mse: received a non-atomic seb" + +let process_module_seb_binding mbid seb = + process_module_bindings [id_of_mbid mbid] + [mbid, + (seb2mse seb, + { ann_inline = DefaultInline; ann_scope_subst = [] })] + +let intern_args interp_modtype (idl,(arg,ann)) = + let inl = inline_annot ann in let lib_dir = Lib.library_dp() in - let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in + let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env()) @@ -504,11 +551,12 @@ let start_module_ interp_modtype export id args res fs = let mp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let res_entry_o, sub_body_l = match res with - | Topconstr.Enforce (res,inl) -> + | Enforce (res,ann) -> + let inl = inline_annot ann in let mte = interp_modtype (Global.env()) res in let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in Some (mte,inl), [] - | Topconstr.Check resl -> + | Check resl -> None, build_subtypes interp_modtype mp arg_entries resl in let mbids = List.map fst arg_entries in @@ -561,7 +609,7 @@ let end_module () = | Some mp_from,(mbids,_,objs) -> (mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) in - let node = in_module (None,substobjs) in + let node = in_module substobjs in let objects = if keep = [] || mbids <> [] then special@[node] (* no keep objects or we are defining a functor *) @@ -652,7 +700,7 @@ let subst_import (subst,(export,mp as obj)) = if mp'==mp then obj else (export,mp') -let (in_import,_) = +let in_import = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; open_function = (fun i o -> if i=1 then cache_import o); @@ -698,7 +746,8 @@ let end_modtype () = mp -let declare_modtype_ interp_modtype id args mtys (mty,inl) fs = +let declare_modtype_ interp_modtype id args mtys (mty,ann) fs = + let inl = inline_annot ann in let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in @@ -708,9 +757,11 @@ let declare_modtype_ interp_modtype id args mtys (mty,inl) fs = (* Undo the simulated interactive building of the module type *) (* and declare the module type as a whole *) + register_scope_subst ann.ann_scope_subst; let substobjs = (mbids,mmp, subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in + reset_scope_subst (); Summary.unfreeze_summaries fs; ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l))); mmp @@ -744,6 +795,60 @@ let rec get_module_substobjs env mp_from inl = function | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty | MSEwith (mty, With_Module (idl,mp)) -> assert false + +let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = + let mmp = Global.start_module id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + + let funct f m = funct_entry arg_entries (f (Global.env ()) m) in + let env = Global.env() in + let mty_entry_o, subs, inl_res = match res with + | Enforce (mty,ann) -> + Some (funct interp_modtype mty), [], inline_annot ann + | Check mtys -> + None, build_subtypes interp_modtype mmp arg_entries mtys, + default_inline () + in + + (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *) + let mexpr_entry_o, inl_expr, scl = match mexpr_o with + | None -> None, default_inline (), [] + | Some (mexpr,ann) -> + Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst + + in + let entry = + {mod_entry_type = mty_entry_o; + mod_entry_expr = mexpr_entry_o } + in + + let substobjs = + match entry with + | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte + | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr + | _ -> anomaly "declare_module: No type, no body ..." + in + let (mbids,mp_from,objs) = substobjs in + (* Undo the simulated interactive building of the module *) + (* and declare the module as a whole *) + Summary.unfreeze_summaries fs; + let mp = mp_of_kn (Lib.make_kn id) in + let inl = if inl_expr = None then None else inl_res in (*PLTODO *) + let mp_env,resolver = Global.add_module id entry inl in + + if mp_env <> mp then anomaly "Kernel and Library names do not match"; + + + check_subtypes mp subs; + register_scope_subst scl; + let substobjs = (mbids,mp_env, + subst_objects(map_mp mp_from mp_env resolver) objs) in + reset_scope_subst (); + ignore (add_leaf + id + (in_module substobjs)); + mmp + (* Include *) let rec subst_inc_expr subst me = @@ -769,95 +874,48 @@ let lift_oname (sp,kn) = let dir,_ = Libnames.repr_path sp in (dir,mp) -let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) = +let cache_include (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in load_objects 1 prefix objs; - open_objects 1 prefix objs - -let load_include i (oname,((me,is_mod),(mbis,mp1,objs))) = + open_objects 1 prefix objs + +let load_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in load_objects i prefix objs - - -let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) = + +let open_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in open_objects i prefix objs - -let subst_include (subst,((me,is_mod),substobj)) = + +let subst_include (subst,(me,substobj)) = let (mbids,mp,objs) = substobj in let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in - ((subst_inc_expr subst me,is_mod),substobjs) - -let classify_include ((me,is_mod),substobjs) = - Substitute ((me,is_mod),substobjs) + (subst_inc_expr subst me,substobjs) + +let classify_include (me,substobjs) = Substitute (me,substobjs) -let (in_include,out_include) = - declare_object {(default_object "INCLUDE") with +type include_obj = module_struct_entry * substitutive_objects + +let (in_include : include_obj -> obj), + (out_include : obj -> include_obj) = + 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 } - -let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = - let mmp = Global.start_module id in - let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - - let funct f m = funct_entry arg_entries (f (Global.env ()) m) in - let env = Global.env() in - let mty_entry_o, subs, inl_res = match res with - | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl - | Topconstr.Check mtys -> - None, build_subtypes interp_modtype mmp arg_entries mtys, true - in - - (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *) - let mexpr_entry_o, inl_expr = match mexpr_o with - | None -> None, true - | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl - in - let entry = - {mod_entry_type = mty_entry_o; - mod_entry_expr = mexpr_entry_o } - in - - let(mbids,mp_from,objs) = - match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr - | _ -> anomaly "declare_module: No type, no body ..." - in - (* Undo the simulated interactive building of the module *) - (* and declare the module as a whole *) - Summary.unfreeze_summaries fs; - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in - - if mp_env <> mp then anomaly "Kernel and Library names do not match"; - - - check_subtypes mp subs; - - let substobjs = (mbids,mp_env, - subst_objects(map_mp mp_from mp_env resolver) objs) in - ignore (add_leaf - id - (in_module (Some (entry), substobjs))); - mmp - - let rec include_subst env mb mbids sign inline = match mbids with | [] -> empty_subst | mbid::mbids -> let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in let subst = include_subst env mb mbids fbody_b inline in - let mp_delta = if not inline then mb.mod_delta else - Modops.complete_inline_delta_resolver env mb.mod_mp + let mp_delta = + Modops.inline_delta_resolver env inline mb.mod_mp farg_id farg_b mb.mod_delta in join (map_mbid mbid mb.mod_mp mp_delta) subst @@ -894,9 +952,13 @@ let get_includeself_substobjs env objs me is_mod inline = ([],mp_self,subst_objects subst objects) with NothingToDo -> objs -let declare_one_include_inner inl (me,is_mod) = + + + +let declare_one_include_inner annot (me,is_mod) = let env = Global.env() in let mp1,_ = current_prefix () in + let inl = inline_annot annot in let (mbids,mp,objs)= if is_mod then get_module_substobjs env mp1 inl me @@ -909,14 +971,15 @@ let declare_one_include_inner inl (me,is_mod) = (mbids,mp,objs) in let id = current_mod_id() in let resolver = Global.add_include me is_mod inl in + register_scope_subst annot.ann_scope_subst; let substobjs = (mbids,mp1, subst_objects (map_mp mp mp1 resolver) objs) in - ignore (add_leaf id - (in_include ((me,is_mod), substobjs))) + reset_scope_subst (); + ignore (add_leaf id (in_include (me, substobjs))) -let declare_one_include interp_struct me_ast = - declare_one_include_inner (snd me_ast) - (interp_struct (Global.env()) (fst me_ast)) +let declare_one_include interp_struct (me_ast,annot) = + declare_one_include_inner annot + (interp_struct (Global.env()) me_ast) let declare_include_ interp_struct me_asts = List.iter (declare_one_include interp_struct) me_asts diff --git a/library/declaremods.mli b/library/declaremods.mli index 46b7f411..9d44ba97 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Entries @@ -16,15 +13,41 @@ open Environ open Libnames open Libobject open Lib - (*i*) -(*s This modules provides official functions to declare modules and +(** This modules provides official functions to declare modules and module types *) +(** Rigid / flexible signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Should we adapt a few scopes during functor application ? *) + +type scope_subst = (string * string) list + +val subst_scope : string -> string + +(** Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) -(*s Modules *) +type inline = + | NoInline + | DefaultInline + | InlineAt of int -(* [declare_module interp_modtype interp_modexpr id fargs typ expr] +(** The type of annotations for functor applications *) + +type funct_app_annot = + { ann_inline : inline; + ann_scope_subst : scope_subst } + +type 'a annotated = ('a * funct_app_annot) + +(** {6 Modules } *) + +(** [declare_module interp_modtype interp_modexpr id fargs typ expr] declares module [id], with type constructed by [interp_modtype] from functor arguments [fargs] and [typ] and with module body constructed by [interp_modtype] from functor arguments [fargs] and @@ -41,39 +64,44 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> - ('modast * bool) list -> module_path + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> + ('modast annotated) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> module_path + bool option -> identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> module_path val end_module : unit -> module_path -(*s Module types *) +(** {6 Module types } *) val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> ('modast * bool) list -> module_path + identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> + ('modast annotated) list -> + module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> module_path val end_modtype : unit -> module_path -(*s Objects of a module. They come in two lists: the substitutive ones +(** {6 ... } *) +(** Objects of a module. They come in two lists: the substitutive ones and the other *) val module_objects : module_path -> library_segment -(*s Libraries i.e. modules on disk *) +(** {6 Libraries i.e. modules on disk } *) type library_name = dir_path @@ -88,27 +116,28 @@ val start_library : library_name -> unit val end_library : library_name -> Safe_typing.compiled_library * library_objects -(* set a function to be executed at end_library *) +(** set a function to be executed at end_library *) val set_end_library_hook : (unit -> unit) -> unit -(* [really_import_module mp] opens the module [mp] (in a Caml sense). +(** [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. *) val really_import_module : module_path -> unit -(* [import_module export mp] is a synchronous version of +(** [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 -> module_path -> unit -(* Include *) +(** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * bool) list -> unit + ('struct_expr annotated) list -> unit -(*s [iter_all_segments] iterate over all segments, the modules' +(** {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). *) @@ -120,7 +149,10 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*) -(* For translator *) +(** For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * (module_struct_entry * bool)) list -> unit + (mod_bound_id * (module_struct_entry annotated)) list -> unit +(** For Printer *) +val process_module_seb_binding : + mod_bound_id -> Declarations.struct_expr_body -> unit diff --git a/library/decls.ml b/library/decls.ml index 425fe798..74a5f7ef 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decls.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (** This module registers tables for some non-logical informations associated declarations *) @@ -57,7 +55,8 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) -let clear_proofs sign = +let initialize_named_context_for_proof () = + let sign = Global.named_context () in List.fold_right (fun (id,c,t as d) signv -> let d = if variable_opacity id then (id,None,t) else d in diff --git a/library/decls.mli b/library/decls.mli index 7a8e138b..73f1745b 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decls.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names open Sign open Libnames @@ -20,7 +18,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - dir_path * bool (* opacity *) * Univ.constraints * logical_kind + dir_path * bool (** opacity *) * Univ.constraints * logical_kind val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> dir_path @@ -35,7 +33,11 @@ val variable_exists : variable -> bool val add_constant_kind : constant -> logical_kind -> unit val constant_kind : constant -> logical_kind +(* Prepare global named context for proof session: remove proofs of + opaque section definitions and remove vm-compiled code *) + +val initialize_named_context_for_proof : unit -> Environ.named_context_val + (** Miscellaneous functions *) val last_section_hyps : dir_path -> identifier list -val clear_proofs : named_context -> Environ.named_context_val diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 2a4d5494..ec92f679 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dischargedhypsmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Libnames open Names diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 59dcdf24..fda071a7 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,24 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dischargedhypsmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Libnames open Term open Environ open Nametab -(*i*) type discharged_hyps = full_path list -(*s Discharged hypothesis. Here we store the discharged hypothesis of each *) -(* constant or inductive type declaration. *) +(** Discharged hypothesis. Here we store the discharged hypothesis of each + constant or inductive type declaration. *) val set_discharged_hyps : full_path -> discharged_hyps -> unit val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/global.ml b/library/global.ml index 72429c76..ab70bb7c 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Term @@ -121,16 +119,22 @@ 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 constant_of_delta con = +let constant_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO : are resolver and resolver_param orthogonal ? + the effect of resolver is lost if resolver_param isn't + trivial at that spot. *) Mod_subst.constant_of_delta resolver_param - (Mod_subst.constant_of_delta resolver con) + (Mod_subst.constant_of_delta_kn resolver kn) -let mind_of_delta mind = +let mind_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO idem *) Mod_subst.mind_of_delta resolver_param - (Mod_subst.mind_of_delta resolver mind) - + (Mod_subst.mind_of_delta_kn resolver kn) + +let exists_label id = exists_label id !global_env + let start_library dir = let mp,newenv = start_library dir !global_env in global_env := newenv; diff --git a/library/global.mli b/library/global.mli index cdcf5801..1a0fabdc 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Univ open Term @@ -17,9 +14,8 @@ open Entries open Indtypes open Mod_subst open Safe_typing - (*i*) -(* This module defines the global environment of Coq. The functions +(** 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 @@ -38,11 +34,12 @@ val named_context : unit -> Sign.named_context val env_is_empty : unit -> bool -(*s Extending env with variables and local definitions *) +(** {6 Extending env with variables and local definitions } *) val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints -(*s Adding constants, inductives, modules and module types. All these +(** {6 ... } *) +(** Adding constants, inductives, modules and module types. All these functions verify that given names match those generated by kernel *) val add_constant : @@ -51,57 +48,59 @@ val add_mind : dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive val add_module : - identifier -> module_entry -> bool -> module_path * delta_resolver + identifier -> module_entry -> inline -> module_path * delta_resolver val add_modtype : - identifier -> module_struct_entry -> bool -> module_path + identifier -> module_struct_entry -> inline -> module_path val add_include : - module_struct_entry -> bool -> bool -> delta_resolver + module_struct_entry -> bool -> inline -> delta_resolver val add_constraints : constraints -> unit val set_engagement : engagement -> unit -(*s Interactive modules and module types *) -(* Both [start_*] functions take the [dir_path] argument to create a +(** {6 Interactive modules and module types } + Both [start_*] functions take the [dir_path] argument to create a [mod_self_id]. This should be the name of the compilation unit. *) -(* [start_*] functions return the [module_path] valid for components +(** [start_*] functions return the [module_path] valid for components of the started module / module type *) val start_module : identifier -> module_path val end_module : Summary.frozen ->identifier -> - (module_struct_entry * bool) option -> module_path * delta_resolver + (module_struct_entry * inline) option -> module_path * delta_resolver val add_module_parameter : - mod_bound_id -> module_struct_entry -> bool -> delta_resolver + mod_bound_id -> module_struct_entry -> inline -> delta_resolver val start_modtype : identifier -> module_path val end_modtype : Summary.frozen -> identifier -> module_path val pack_module : unit -> module_body -(* Queries *) +(** Queries *) val lookup_named : variable -> named_declaration val lookup_constant : constant -> constant_body val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body val lookup_mind : mutual_inductive -> mutual_inductive_body val lookup_module : module_path -> module_body val lookup_modtype : module_path -> module_type_body -val constant_of_delta : constant -> constant -val mind_of_delta : mutual_inductive -> mutual_inductive +val constant_of_delta_kn : kernel_name -> constant +val mind_of_delta_kn : kernel_name -> mutual_inductive +val exists_label : label -> bool -(* Compiled modules *) +(** Compiled modules *) val start_library : dir_path -> module_path val export : dir_path -> module_path * compiled_library val import : compiled_library -> Digest.t -> module_path -(*s Function to get an environment from the constants part of the global +(** {6 ... } *) +(** Function to get an environment from the constants part of the global * environment and a given context. *) val type_of_global : Libnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env -(* spiwack: register/unregister function for retroknowledge *) +(** spiwack: register/unregister function for retroknowledge *) val register : Retroknowledge.field -> constr -> constr -> unit diff --git a/library/goptions.ml b/library/goptions.ml index 178c436d..90c8728c 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* This module manages customization parameters at the vernacular level *) open Pp @@ -19,22 +17,18 @@ open Term open Nametab open Mod_subst +open Goptionstyp + +type option_name = Goptionstyp.option_name + (****************************************************************************) (* 0- Common things *) -type option_name = string list - let nickname table = String.concat " " table let error_undeclared_key key = error ((nickname key)^": no table or option of this type") -type value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | IdentValue of global_reference - (****************************************************************************) (* 1- Tables *) @@ -96,7 +90,7 @@ module MakeTable = if p' == p then obj else (f,p') in - let (inGo,outGo) = + 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; @@ -201,12 +195,13 @@ module MakeRefTable = type 'a option_sig = { optsync : bool; + optdepr : bool; optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> value) -> (value -> unit) +type option_type = bool * (unit -> option_value) -> (option_value -> unit) module OptionMap = Map.Make (struct type t = option_name let compare = compare end) @@ -230,25 +225,25 @@ open Libobject open Lib let declare_option cast uncast - { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } = + { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in (* spiwack: I use two spaces in the nicknames of "local" and "global" objects. That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are lists of strings *without* spaces. *) let (write,lwrite,gwrite) = if sync then - let (ldecl_obj,_) = (* "Local": doesn't survive section or modules. *) + let ldecl_obj = (* "Local": doesn't survive section or modules. *) declare_object {(default_object ("L "^nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun _ -> Dispose)} in - let (decl_obj,_) = (* default locality: survives sections but not modules. *) + let decl_obj = (* default locality: survives sections but not modules. *) declare_object {(default_object (nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun _ -> Dispose); discharge_function = (fun (_,v) -> Some v)} in - let (gdecl_obj,_) = (* "Global": survives section and modules. *) + let gdecl_obj = (* "Global": survives section and modules. *) declare_object {(default_object ("G "^nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun v -> Substitute v); @@ -269,7 +264,7 @@ let declare_option cast uncast let cwrite v = write (uncast v) in let clwrite v = lwrite (uncast v) in let cgwrite v = gwrite (uncast v) in - value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab; + value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; write type 'a write_function = 'a -> unit @@ -292,7 +287,7 @@ let declare_string_option = (* Setting values of options *) let set_option_value locality check_and_cast key v = - let (name,(_,read,write,lwrite,gwrite)) = + let (name, depr, (_,read,write,lwrite,gwrite)) = try get_option key with Not_found -> error ("There is no option "^(nickname key)^".") in @@ -330,12 +325,12 @@ let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = try set_option_value locality check_bool_value key v - with UserError (_,s) -> Flags.if_verbose msg_warning s + with UserError (_,s) -> Flags.if_warn msg_warning s let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = try set_option_value locality check_unset_value key () - with UserError (_,s) -> Flags.if_verbose msg_warning s + with UserError (_,s) -> Flags.if_warn msg_warning s let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -350,10 +345,10 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s - | IdentValue r -> pr_global_env Idset.empty r +(* | IdentValue r -> pr_global_env Idset.empty r *) let print_option_value key = - let (name,(_,read,_,_,_)) = get_option key in + let (name, depr, (_,read,_,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -364,25 +359,37 @@ let print_option_value key = msg_option_value (name,s) ++ fnl ()) +let get_tables () = + let tables = !value_tab in + let fold key (name, depr, (sync,read,_,_,_)) accu = + let state = { + opt_sync = sync; + 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 (" "^(nickname key)^": ") ++ msg_option_value (name, value) in + if depr then msg ++ str " [DEPRECATED]" ++ fnl () + else msg ++ fnl () + in msg (str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name,(sync,read,_,_,_)) p -> - if sync then - p ++ str (" "^(nickname key)^": ") ++ - msg_option_value (name,read()) ++ fnl () - else - p) + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p ++ print_option key name (read ()) depr + else p) !value_tab (mt ()) ++ str "Asynchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name,(sync,read,_,_,_)) p -> - if sync then - p - else - p ++ str (" "^(nickname key)^": ") ++ - msg_option_value (name,read()) ++ fnl ()) + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p + else p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right diff --git a/library/goptions.mli b/library/goptions.mli index 78c4d8e6..d25c1202 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,16 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: goptions.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** This module manages customization parameters at the vernacular level *) -(* This module manages customization parameters at the vernacular level *) - -(* Two kinds of things are managed : tables and options value +(** 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. @@ -40,12 +38,11 @@ Set Tata Tutu Titi. Unset Tata Tutu Titi. - Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *) + Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) The created table/option may be declared synchronous or not (synchronous = consistent with the resetting commands) *) -(*i*) open Pp open Util open Names @@ -53,18 +50,12 @@ open Libnames open Term open Nametab open Mod_subst -(*i*) - -(*s Things common to tables and options. *) - -(* The type of table/option keys *) -type option_name = string list -val error_undeclared_key : option_name -> 'a +type option_name = Goptionstyp.option_name -(*s Tables. *) +(** {6 Tables. } *) -(* The functor [MakeStringTable] declares a table containing objects +(** 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." @@ -85,7 +76,7 @@ sig val elements : unit -> string list end -(* The functor [MakeRefTable] declares a new table of objects of type +(** 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 @@ -113,21 +104,26 @@ module MakeRefTable : end -(*s Options. *) +(** {6 Options. } *) -(* These types and function are for declaring a new option of name [key] +(** 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 = { optsync : bool; + (** whether the option is synchronous w.r.t to the section/module system. *) + 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 } -(* When an option is declared synchronous ([optsync] is [true]), the output is +(** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) type 'a write_function = 'a -> unit @@ -137,7 +133,9 @@ val declare_bool_option : bool option_sig -> bool write_function val declare_string_option: string option_sig -> string write_function -(*s Special functions supposed to be used only in vernacentries.ml *) +(** {6 Special functions supposed to be used only in vernacentries.ml } *) + +module OptionMap : Map.S with type key = option_name val get_string_table : option_name -> @@ -153,7 +151,8 @@ val get_ref_table : mem : reference -> unit; print : unit > -(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *) +(** The first argument is a locality flag. + [Some true] = "Local", [Some false]="Global". *) val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit @@ -165,5 +164,7 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit +val get_tables : unit -> Goptionstyp.option_state OptionMap.t val print_tables : unit -> unit +val error_undeclared_key : option_name -> 'a diff --git a/library/goptionstyp.mli b/library/goptionstyp.mli new file mode 100644 index 00000000..541a1470 --- /dev/null +++ b/library/goptionstyp.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Some types used in the generic option mechanism (Goption) *) + +(** Placing them here in a pure interface avoid some dependency issues + when compiling CoqIDE *) + +type option_name = string list + +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +type option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} diff --git a/library/heads.ml b/library/heads.ml index 8244761d..9f9f1ca2 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heads.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -150,7 +148,7 @@ let cache_head o = let subst_head_approximation subst = function | RigidHead (RigidParameter cst) as k -> let cst,c = subst_con subst cst in - if c = mkConst cst then + if isConst c && eq_constant (destConst c) cst then (* A change of the prefix of the constant *) k else @@ -169,7 +167,9 @@ let discharge_head (_,(ref,k)) = let rebuild_head (ref,k) = (ref, compute_head ref) -let (inHead, _) = +type head_obj = evaluable_global_reference * head_approximation + +let inHead : head_obj -> obj = declare_object {(default_object "HEAD") with cache_function = cache_head; load_function = load_head; diff --git a/library/heads.mli b/library/heads.mli index e13b171f..9e80c173 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heads.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - open Names open Term open Environ @@ -17,12 +15,12 @@ open Environ provides the function to compute the head symbols and a table to store the heads *) -(* [declared_head] computes and registers the head symbol of a +(** [declared_head] computes and registers the head symbol of a possibly evaluable constant or variable *) val declare_head : evaluable_global_reference -> unit -(* [is_rigid] tells if some term is known to ultimately reduce to a term +(** [is_rigid] tells if some term is known to ultimately reduce to a term with a rigid head symbol *) val is_rigid : env -> constr -> bool diff --git a/library/impargs.ml b/library/impargs.ml index 1c2b5afe..ef7f5921 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Libnames @@ -159,7 +157,7 @@ let is_flexible_reference env bound depth f = | Rel n -> (* since local definitions have been expanded *) false | Const kn -> let cb = Environ.lookup_constant kn env in - cb.const_body <> None & not cb.const_opaque + (match cb.const_body with Def _ -> true | _ -> false) | Var id -> let (_,value,_) = Environ.lookup_named id env in value <> None | Ind _ | Construct _ -> false @@ -248,6 +246,10 @@ let compute_auto_implicits env flags enriching t = if enriching then compute_implicits_flags env flags true t else compute_implicits_gen false false false true true env t +let compute_implicits_names env t = + let _, impls = compute_implicits_gen false false false false true env t in + List.map fst impls + (* Extra information about implicit arguments *) type maximal_insertion = bool (* true = maximal contextual insertion *) @@ -439,9 +441,6 @@ let merge_impls (cond,oldimpls) (_,newimpls) = | Some (_, Manual, _) -> orig | _ -> ni) oldimpls newimpls)@usersuffiximpls -let merge_impls_list oldimpls newimpls = - merge_impls oldimpls newimpls - (* Caching implicits *) type implicit_interactive_request = @@ -458,7 +457,18 @@ type implicit_discharge_request = let implicits_table = ref Refmap.empty let implicits_of_global ref = - try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]] + try + let l = Refmap.find ref !implicits_table in + try + let rename_l = Arguments_renaming.arguments_names ref in + let rename imp name = match imp, name with + | Some (_, x,y), Name id -> Some (id, x,y) + | _ -> imp in + List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l + with Not_found -> l + | Invalid_argument _ -> + anomaly "renamings list and implicits list have different lenghts" + with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = implicits_table := Refmap.add ref imps !implicits_table @@ -496,18 +506,23 @@ let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> + (try let vars = section_segment_of_reference ref in let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') + with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> + (try let con' = pop_con con in let vars = section_segment_of_constant con in let extra_impls = impls_of_context vars in let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplConstant (con',flags),l') + with Not_found -> (* con not defined in this section *) Some (req,l)) | ImplMutualInductive (kn,flags) -> + (try let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in let extra_impls = impls_of_context vars in @@ -515,6 +530,7 @@ let discharge_implicits (_,(req,l)) = List.map (add_section_impls vars extra_impls) l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') + with Not_found -> (* ref not defined in this section *) Some (req,l)) let rebuild_implicits (req,l) = match req with @@ -553,7 +569,11 @@ let rebuild_implicits (req,l) = let classify_implicits (req,_ as obj) = if req = ImplLocal then Dispose else Substitute obj -let (inImplicits, _) = +type implicits_obj = + implicit_discharge_request * + (global_reference * implicits_list list) list + +let inImplicits : implicits_obj -> obj = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; @@ -593,6 +613,8 @@ let declare_mib_implicits kn = (* Declare manual implicits *) type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) +type manual_implicits = manual_explicitation list + let compute_implicits_with_manual env typ enriching l = let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in set_manual_implicits env !implicit_args enriching autoimpls l diff --git a/library/impargs.mli b/library/impargs.mli index 7ec7767b..04251f33 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,22 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Term open Environ open Nametab -(*i*) -(*s Implicit arguments. Here we store the implicit arguments. Notice that we +(** {6 Implicit Arguments } *) +(** Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit @@ -36,7 +33,8 @@ val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b -(*s An [implicits_list] is a list of positions telling which arguments +(** {6 ... } *) +(** An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) @@ -44,13 +42,35 @@ type argument_position = | Conclusion | Hyp of int +(** We remember various information about why an argument is + inferable as implicit *) type implicit_explanation = | DepRigid of argument_position + (** means that the implicit argument can be found by + unification along a rigid path (we do not print the arguments of + this kind if there is enough arguments to infer them) *) | DepFlex of argument_position + (** means that the implicit argument can be found by unification + along a collapsable path only (e.g. as x in (P x) where P is another + argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position + (** means that the least argument from which the + implicit argument can be inferred is following a collapsable path + but there is a greater argument from where the implicit argument is + inferable following a rigid path (useful to know how to print a + partial application) *) | Manual + (** means the argument has been explicitely set as implicit. *) + +(** We also consider arguments inferable from the conclusion but it is + operational only if [conclusion_matters] is true. *) + +type maximal_insertion = bool (** true = maximal contextual insertion *) +type force_inference = bool (** true = always infer, never turn into evar/subgoal *) -type implicit_status = (identifier * implicit_explanation * (bool * bool)) option +type implicit_status = (identifier * implicit_explanation * + (maximal_insertion * force_inference)) option + (** [None] = Not implicit *) type implicit_side_condition @@ -64,19 +84,20 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(* Computation of the positions of arguments automatically inferable - for an object of the given type in the given env *) -val compute_implicits : env -> types -> implicits_list list - -(* A [manual_explicitation] is a tuple of a positional or named explicitation with +(** A [manual_explicitation] is a tuple of a positional or named explicitation with maximal insertion, force inference and force usage flags. Forcing usage makes the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) +type manual_explicitation = Topconstr.explicitation * + (maximal_insertion * force_inference * bool) + +type manual_implicits = manual_explicitation list val compute_implicits_with_manual : env -> types -> bool -> - manual_explicitation list -> implicit_status list + manual_implicits -> implicit_status list + +val compute_implicits_names : env -> types -> name list -(*s Computation of implicits (done using the global environment). *) +(** {6 Computation of implicits (done using the global environment). } *) val declare_var_implicits : variable -> unit val declare_constant_implicits : constant -> unit @@ -84,28 +105,26 @@ val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : bool -> global_reference -> unit -(* [declare_manual_implicits local ref enriching l] +(** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. If not set, we decide if it should enrich by automatically inferd implicits depending on the current state. Unsets implicits if [l] is empty. *) val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_explicitation list list -> unit + manual_implicits list -> unit -(* If the list is empty, do nothing, otherwise declare the implicits. *) +(** If the list is empty, do nothing, otherwise declare the implicits. *) val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_explicitation list -> unit + manual_implicits -> unit val implicits_of_global : global_reference -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -val lift_implicits : int -> manual_explicitation list -> manual_explicitation list - -val merge_impls : implicits_list -> implicits_list -> implicits_list +val lift_implicits : int -> manual_implicits -> manual_implicits val make_implicits_list : implicit_status list -> implicits_list list @@ -115,9 +134,7 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request = - | ImplAuto - | ImplManual of int +type implicit_interactive_request type implicit_discharge_request = | ImplLocal diff --git a/library/lib.ml b/library/lib.ml index 6f8655d3..7554fd0b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,26 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Libnames open Nameops open Libobject open Summary + +type is_type = bool (* Module Type or just Module *) +type export = bool option (* None for a Module Type *) + type node = | Leaf of obj | CompilingLibrary of object_prefix - | OpenedModule of bool option * object_prefix * Summary.frozen + | OpenedModule of is_type * export * object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of object_prefix * Summary.frozen - | ClosedModtype of library_segment | OpenedSection of object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen @@ -31,6 +31,9 @@ and library_segment = library_entry list type lib_objects = (Names.identifier * 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)) @@ -69,10 +72,9 @@ let classify_segment seg = (* LEM; TODO: Understand what this does and see if what I do is the correct thing for ClosedMod(ule|type) *) | (_,ClosedModule _) :: stk -> clean acc stk - | (_,ClosedModtype _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" - | (_,OpenedModule _) :: _ -> error "there are still opened modules" - | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,OpenedModule (ty,_,_,_)) :: _ -> + error ("there are still opened " ^ module_kind ty ^"s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -144,8 +146,7 @@ let make_oname id = make_path id, make_kn id let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir - | (sp, OpenedModule (_,dir,_)) :: _ -> dir - | (sp, OpenedModtype (dir,_)) :: _ -> dir + | (sp, OpenedModule (_,_,dir,_)) :: _ -> dir | (sp, CompilingLibrary dir) :: _ -> dir | _::l -> recalc l | [] -> initial_prefix @@ -181,7 +182,6 @@ let split_lib_gen test = then Some (collect after [hd] before) else (match hd with | (sp,ClosedModule seg) - | (sp,ClosedModtype seg) | (sp,ClosedSection seg) -> (match findeq after seg with | None -> findeq (hd::after) before @@ -197,11 +197,11 @@ let split_lib_gen test = let split_lib sp = split_lib_gen (fun x -> fst x = sp) let split_lib_at_opening sp = - let a,s,b = split_lib_gen (function - | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) -> - x = sp - | _ -> - false) in + let is_sp = function + | x,(OpenedSection _|OpenedModule _|CompilingLibrary _) -> x = sp + | _ -> false + in + let a,s,b = split_lib_gen is_sp in assert (List.tl s = []); (a,List.hd s,b) @@ -254,97 +254,66 @@ let add_frozen_state () = (* Modules. *) - -let is_opened id = function - oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when - basename (fst oname) = id -> true - | _ -> false - let is_opening_node = function - _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true + | _,(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 with - | oname,OpenedModule (_,_,fs) -> - basename (fst oname) - | oname,OpenedModtype (_,fs) -> - basename (fst oname) + try match find_entry_p is_opening_node_or_lib with + | oname,OpenedModule (_,_,_,fs) -> basename (fst oname) + | oname,CompilingLibrary _ -> basename (fst oname) | _ -> error "you are not in a module" - with Not_found -> - error "no opened modules" + with Not_found -> error "no opened modules" -let start_module export id mp fs = +let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.empty_dirpath) in - let oname = make_path id, make_kn id in - if Nametab.exists_module dir then - errorlabstrm "open_module" (pr_id id ++ str " already exists") ; - add_entry oname (OpenedModule (export,prefix,fs)); + let sp = make_path id in + let oname = sp, make_kn id in + let exists = + if is_type then Nametab.exists_cci sp else Nametab.exists_module dir + in + if exists then + errorlabstrm "open_module" (pr_id id ++ str " already exists"); + add_entry oname (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix (* add_frozen_state () must be called in declaremods *) +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 - errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.") + errorlabstrm "" + (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") -let end_module () = +let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with - | oname,OpenedModule (_,_,fs) -> oname,fs - | oname,OpenedModtype _ -> error_still_opened "Module Type" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname + | 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 -> - error "No opened modules." + with Not_found -> error "No opened modules." in let (after,mark,before) = split_lib_at_opening oname in lib_stk := before; add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !path_prefix in - (* LEM: This module business seems more complicated than sections; - shouldn't a backtrack into a closed module also do something - with global.ml, given that closing a module does? - TODO - *) recalc_path_prefix (); (* add_frozen_state must be called after processing the module, because we cannot recache interactive modules *) (oname, prefix, fs, after) -let start_modtype id mp fs = - let dir = add_dirpath_suffix (fst !path_prefix) id in - let prefix = dir,(mp,Names.empty_dirpath) in - let sp = make_path id in - let name = sp, make_kn id in - if Nametab.exists_cci sp then - errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ; - add_entry name (OpenedModtype (prefix,fs)); - path_prefix := prefix; - prefix - -let end_modtype () = - let oname,fs = - try match find_entry_p is_opening_node with - | oname,OpenedModtype (_,fs) -> oname,fs - | oname,OpenedModule _ -> error_still_opened "Module" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname - | _ -> assert false - with Not_found -> - error "no opened module types" - in - let (after,mark,before) = split_lib_at_opening oname in - lib_stk := before; - add_entry oname (ClosedModtype (List.rev (mark::after))); - let dir = !path_prefix in - recalc_path_prefix (); - (* add_frozen_state must be called after processing the module type. - This is because we cannot recache interactive module types *) - (oname,dir,fs,after) - +let end_module () = end_mod false +let end_modtype () = end_mod true let contents_after = function | None -> !lib_stk @@ -352,13 +321,6 @@ let contents_after = function (* Modules. *) -let check_for_comp_unit () = - let is_decl = function (_,FrozenState _) -> false | _ -> true in - try - let _ = find_entry_p is_decl in - error "a module cannot be started after some declarations" - with Not_found -> () - (* TODO: use check_for_module ? *) let start_compilation s mp = if !comp_name <> None then @@ -374,21 +336,18 @@ let end_compilation dir = let _ = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." - | OpenedModule _ -> error "There are some open modules." - | OpenedModtype _ -> error "There are some open module types." + | OpenedModule (ty,_,_,_) -> + error ("There are some open "^module_kind ty^"s.") | _ -> assert false - with - Not_found -> () + with Not_found -> () in - let module_p = - function (_,CompilingLibrary _) -> true | x -> is_opening_node x + let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false in let oname = - try match find_entry_p module_p with - (oname, CompilingLibrary prefix) -> oname + try match find_entry_p is_opening_lib with + | (oname, CompilingLibrary prefix) -> oname | _ -> assert false - with - Not_found -> anomaly "No module declared" + with Not_found -> anomaly "No module declared" in let _ = match !comp_name with @@ -399,31 +358,23 @@ let end_compilation dir = " and not " ^ (Names.string_of_dirpath m)); in let (after,mark,before) = split_lib_at_opening oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after -(* Returns true if we are inside an opened module type *) -let is_modtype () = - let opened_p = function - | _, OpenedModtype _ -> true - | _ -> false - in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false - -(* Returns true if we are inside an opened module *) -let is_module () = - let opened_p = function - | _, OpenedModule _ -> true +(* Returns true if we are inside an opened module or module type *) + +let is_module_gen which = + let test = function + | _, OpenedModule (ty,_,_,_) -> which ty | _ -> false in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false + try + let _ = find_entry_p test in true + with Not_found -> false +let is_module_or_modtype () = is_module_gen (fun _ -> true) +let is_modtype () = is_module_gen (fun b -> b) +let is_module () = is_module_gen (fun b -> not b) (* Returns the opening node of a given name *) let find_opening_node id = @@ -495,8 +446,6 @@ let add_section_constant kn = let replacement_context () = pi2 (List.hd !sectab) -let variables_context () = pi1 (List.hd !sectab) - let section_segment_of_constant con = Names.Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -563,8 +512,8 @@ let discharge_item ((sp,_ as oname),e) = | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None - | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None - | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> + | ClosedSection _ | ClosedModule _ -> None + | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" let close_section () = @@ -590,8 +539,8 @@ let close_section () = (*****************) (* Backtracking. *) -let (inLabel,outLabel) = - declare_object {(default_object "DOT") with +let (inLabel : int -> obj), (outLabel : obj -> int) = + declare_object_full {(default_object "DOT") with classify_function = (fun _ -> Dispose)} let recache_decl = function @@ -604,13 +553,6 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let has_top_frozen_state () = - let rec aux = function - | (sp, FrozenState _)::_ -> Some sp - | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t - | _ -> None - in aux !lib_stk - let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; recalc_path_prefix (); @@ -630,17 +572,9 @@ let reset_to_gen test = let reset_to sp = reset_to_gen (fun x -> fst x = sp) -let reset_to_state sp = - let (_,eq,before) = split_lib sp in - (* if eq a frozen state, we'll reset to it *) - match eq with - | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f - | _ -> error "Not a frozen state" - - (* LEM: TODO * We will need to muck with frozen states in after, too! - * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype) + * Not only FrozenState, but also those embedded in Opened(Section|Module) *) let delete_gen test = let (after,equal,before) = split_lib_gen test in @@ -676,8 +610,8 @@ let remove_name (loc,id) = delete sp let is_mod_node = function - | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true + | OpenedModule _ | OpenedSection _ + | ClosedModule _ | ClosedSection _ -> true | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" || t = "MODULE ALIAS" | _ -> false @@ -710,17 +644,16 @@ let is_label_n n x = | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true | _ -> false -(* Reset the label registered by [mark_end_of_command()] with number n. *) +(** Reset the label registered by [mark_end_of_command()] with number n, + which should be strictly in the past. *) + let reset_label n = - let current = current_command_label() in - if n < current then - let res = reset_to_gen (is_label_n n) in - set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) - res - else (* optimisation to avoid recaching when not necessary (why is it so long??) *) - match !lib_stk with - | [] -> () - | x :: ls -> (lib_stk := ls;set_command_label (n-1)) + if n >= current_command_label () then + error "Cannot backtrack to the current label or a future one"; + let res = reset_to_gen (is_label_n n) in + (* forget state numbers after n only if reset succeeded *) + set_command_label (n-1); + res let rec back_stk n stk = match stk with @@ -729,7 +662,9 @@ let rec back_stk n stk = | _::tail -> back_stk n tail | [] -> error "Reached begin of command history" -let back n = reset_to (back_stk n !lib_stk) +let back n = + reset_to (back_stk n !lib_stk); + set_command_label (current_command_label () - n - 1) (* State and initialization. *) @@ -793,7 +728,7 @@ let rec split_mp mp = | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id] + | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [id] let split_modpath mp = let rec aux = function diff --git a/library/lib.mli b/library/lib.mli index 7eb8b688..0d6eb34b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,25 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** Lib: record of operations, backtrack, low-level sections *) -(*s This module provides a general mechanism to keep a trace of all operations +(** 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 *) + type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix - | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen + | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of Libnames.object_prefix * Summary.frozen - | ClosedModtype of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen @@ -28,14 +29,14 @@ and library_segment = (Libnames.object_name * node) list type lib_objects = (Names.identifier * Libobject.obj) list -(*s Object iteratation functions. *) +(** {6 Object iteration functions. } *) val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects (*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) -(* [classify_segment seg] verifies that there are no OpenedThings, +(** [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 @@ -43,41 +44,45 @@ val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list -(* [segment_of_objects prefix objs] forms a list of Leafs *) +(** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : Libnames.object_prefix -> lib_objects -> library_segment -(*s Adding operations (which call the [cache] method, and getting the +(** {6 ... } *) +(** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit -(* this operation adds all objects with the same name and calls [load_object] +(** this operation adds all objects with the same name and calls [load_object] for each of them *) val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit -(* Adds a "dummy" entry in lib_stk with a unique new label number. *) +(** Adds a "dummy" entry in lib_stk with a unique new label number. *) val mark_end_of_command : unit -> unit -(* Returns the current label number *) + +(** Returns the current label number *) val current_command_label : unit -> int -(* [reset_label n ] resets [lib_stk] to the label n registered by - [mark_end_of_command()]. That is it forgets the label and anything - registered after it. *) + +(** [reset_label n] resets [lib_stk] to the label n registered by + [mark_end_of_command()]. It forgets the label and anything + registered after it. The label should be strictly in the past. *) val reset_label : int -> unit -(*s The function [contents_after] returns the current library segment, +(** {6 ... } *) +(** The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) val contents_after : Libnames.object_name option -> library_segment -(*s Functions relative to current path *) +(** {6 Functions relative to current path } *) -(* User-side names *) +(** User-side names *) val cwd : unit -> Names.dir_path val cwd_except_section : unit -> Names.dir_path val current_dirpath : bool -> Names.dir_path (* false = except sections *) @@ -85,72 +90,79 @@ val make_path : Names.identifier -> Libnames.full_path val make_path_except_section : Names.identifier -> Libnames.full_path val path_of_include : unit -> Libnames.full_path -(* Kernel-side names *) +(** Kernel-side names *) val current_prefix : unit -> Names.module_path * Names.dir_path val make_kn : Names.identifier -> Names.kernel_name val make_con : Names.identifier -> Names.constant -(* Are we inside an opened section *) +(** Are we inside an opened section *) val sections_are_opened : unit -> bool val sections_depth : unit -> int -(* Are we inside an opened module type *) +(** Are we inside an opened module type *) +val is_module_or_modtype : unit -> bool val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident -(* Returns the opening node of a given name *) +(** Returns the opening node of a given name *) val find_opening_node : Names.identifier -> node -(*s Modules and module types *) +(** {6 Modules and module types } *) val start_module : - bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_module : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment + export -> Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_modtype : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(* [Lib.add_frozen_state] must be called after each of the above functions *) + Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix + +val end_module : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment -(*s Compilation units *) +val end_modtype : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment + +(** [Lib.add_frozen_state] must be called after each of the above functions *) + +(** {6 Compilation units } *) val start_compilation : Names.dir_path -> Names.module_path -> unit val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment -(* The function [library_dp] returns the [dir_path] of the current +(** The function [library_dp] returns the [dir_path] of the current compiling library (or [default_library]) *) val library_dp : unit -> Names.dir_path -(* Extract the library part of a name even if in a section *) +(** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.dir_path val split_mp : Names.module_path -> Names.dir_path * Names.dir_path val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list val library_part : Libnames.global_reference -> Names.dir_path val remove_section_part : Libnames.global_reference -> Names.dir_path -(*s Sections *) +(** {6 Sections } *) val open_section : Names.identifier -> unit val close_section : unit -> unit -(*s Backtracking (undo). *) +(** {6 Backtracking (undo). } *) val reset_to : Libnames.object_name -> unit val reset_name : Names.identifier Util.located -> unit val remove_name : Names.identifier Util.located -> unit val reset_mod : Names.identifier Util.located -> unit -val reset_to_state : Libnames.object_name -> unit - -val has_top_frozen_state : unit -> Libnames.object_name option -(* [back n] resets to the place corresponding to the $n$-th call of +(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of [mark_end_of_command] (counting backwards) *) val back : int -> unit -(*s We can get and set the state of the operations (used in [States]). *) +(** {6 We can get and set the state of the operations (used in [States]). } *) type frozen @@ -163,13 +175,13 @@ val declare_initial_state : unit -> unit val reset_initial : unit -> unit -(* XML output hooks *) +(** XML output hooks *) val set_xml_open_section : (Names.identifier -> unit) -> unit val set_xml_close_section : (Names.identifier -> unit) -> unit type binding_kind = Explicit | Implicit -(*s Section management for discharge *) +(** {6 Section management for discharge } *) type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types type variable_context = variable_info list @@ -189,7 +201,7 @@ val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit val replacement_context : unit -> (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t) -(*s Discharge: decrease the section level if in the current section *) +(** {6 Discharge: decrease the section level if in the current section } *) val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant diff --git a/library/libnames.ml b/library/libnames.ml index 2986940d..b91d24bd 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Util open Names @@ -29,8 +27,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false let eq_gr gr1 gr2 = match gr1,gr2 with - ConstRef con1, ConstRef con2 -> - eq_constant con1 con2 + | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2 | _,_ -> gr1=gr2 @@ -58,13 +55,10 @@ let subst_global subst ref = match ref with if c'==c then ref,t else ConstructRef c', t let canonical_gr = function - | ConstRef con -> - ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> - IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> - ConstructRef((mind_of_kn(canonical_mind kn),i),j) - | VarRef id -> VarRef id + | ConstRef con -> ConstRef(constant_of_kn(canonical_con con)) + | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i) + | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | VarRef id -> VarRef id let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp @@ -82,25 +76,37 @@ let constr_of_global = function let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr -(* outside of the kernel, names are ordered on their canonical part *) +let global_ord_gen fc fmi x y = + let ind_ord (indx,ix) (indy,iy) = + let c = Pervasives.compare ix iy in + if c = 0 then kn_ord (fmi indx) (fmi indy) else c + in + match x, y with + | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy) + | IndRef indx, IndRef indy -> ind_ord indx indy + | ConstructRef (indx,jx), ConstructRef (indy,jy) -> + let c = Pervasives.compare jx jy in + if c = 0 then ind_ord indx indy else c + | _, _ -> Pervasives.compare x y + +let global_ord_can = global_ord_gen canonical_con canonical_mind +let global_ord_user = global_ord_gen user_con user_mind + +(* By default, [global_reference] are ordered on their canonical part *) + module RefOrdered = struct type t = global_reference - let compare x y = - let make_name = function - | ConstRef con -> - ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> - IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> - ConstructRef((mind_of_kn(canonical_mind kn),i),j) - | VarRef id -> VarRef id - in - Pervasives.compare (make_name x) (make_name y) + let compare = global_ord_can +end + +module RefOrdered_env = struct + type t = global_reference + let compare = global_ord_user end - + module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) - + (* Extended global references *) type syndef_name = kernel_name @@ -109,6 +115,18 @@ 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 compare x y = + match x, y with + | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry + | SynDef knx, SynDef kny -> kn_ord knx kny + | _, _ -> Pervasives.compare x y +end + (**********************************************) let pr_dirpath sl = (str (string_of_dirpath sl)) @@ -177,6 +195,7 @@ type full_path = { basename : identifier } let make_path pa id = { dirpath = pa; basename = id } + let repr_path { dirpath = pa; basename = id } = (pa,id) (* parsing and printing of section paths *) @@ -197,8 +216,6 @@ module SpOrdered = let compare = sp_ord end -module Spset = Set.Make(SpOrdered) -module Sppred = Predicate.Make(SpOrdered) module Spmap = Map.Make(SpOrdered) let dirpath sp = let (p,_) = repr_path sp in p diff --git a/library/libnames.mli b/library/libnames.mli index a7bc3b52..18b6ac49 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,22 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Pp open Util open Names open Term open Mod_subst -(*i*) -(*s Global reference is a kernel side type for all references together *) +(** {6 Global reference is a kernel side type for all references together } *) type global_reference = | VarRef of variable | ConstRef of constant @@ -40,14 +36,14 @@ val destConstructRef : global_reference -> constructor val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr -(* Turn a global reference into a construction *) +(** Turn a global reference into a construction *) val constr_of_global : global_reference -> constr -(* Turn a construction denoting a global reference into a global reference; +(** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) val global_of_constr : constr -> global_reference -(* Obsolete synonyms for constr_of_global and global_of_constr *) +(** Obsolete synonyms for constr_of_global and global_of_constr *) val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference @@ -55,12 +51,16 @@ module RefOrdered : sig type t = global_reference val compare : global_reference -> global_reference -> int end - + +module RefOrdered_env : sig + type t = global_reference + val compare : global_reference -> global_reference -> int +end module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference -(*s Extended global references *) +(** {6 Extended global references } *) type syndef_name = kernel_name @@ -68,19 +68,24 @@ type extended_global_reference = | TrueGlobal of global_reference | SynDef of syndef_name -(*s Dirpaths *) +module ExtRefOrdered : sig + type t = extended_global_reference + val compare : t -> t -> int +end + +(** {6 Dirpaths } *) val pr_dirpath : dir_path -> Pp.std_ppcmds val dirpath_of_string : string -> dir_path val string_of_dirpath : dir_path -> string -(* Pop the suffix of a [dir_path] *) +(** Pop the suffix of a [dir_path] *) val pop_dirpath : dir_path -> dir_path -(* Pop the suffix n times *) +(** Pop the suffix n times *) val pop_dirpath_n : int -> dir_path -> dir_path -(* Give the immediate prefix and basename of a [dir_path] *) +(** Give the immediate prefix and basename of a [dir_path] *) val split_dirpath : dir_path -> dir_path * identifier val add_dirpath_suffix : dir_path -> module_ident -> dir_path @@ -95,28 +100,27 @@ val is_dirpath_prefix_of : dir_path -> dir_path -> bool module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path -(*s Full paths are {\em absolute} paths of declarations *) +(** {6 Full paths are {e absolute} paths of declarations } *) type full_path -(* Constructors of [full_path] *) +(** Constructors of [full_path] *) val make_path : dir_path -> identifier -> full_path -(* Destructors of [full_path] *) +(** Destructors of [full_path] *) val repr_path : full_path -> dir_path * identifier val dirpath : full_path -> dir_path val basename : full_path -> identifier -(* Parsing and printing of section path as ["coq_root.module.id"] *) +(** 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 -> std_ppcmds -module Sppred : Predicate.S with type elt = full_path module Spmap : Map.S with type key = full_path val restrict_path : int -> full_path -> full_path -(*s Temporary function to brutally form kernel names from section paths *) +(** {6 Temporary function to brutally form kernel names from section paths } *) val encode_mind : dir_path -> identifier -> mutual_inductive val decode_mind : mutual_inductive -> dir_path * identifier @@ -124,7 +128,8 @@ val encode_con : dir_path -> identifier -> constant val decode_con : constant -> dir_path * identifier -(*s A [qualid] is a partially qualified ident; it includes fully +(** {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. *) @@ -138,14 +143,14 @@ val pr_qualid : qualid -> std_ppcmds val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid -(* Turns an absolute name, a dirpath, or an identifier into a +(** Turns an absolute name, a dirpath, or an identifier into a qualified name denoting the same name *) val qualid_of_path : full_path -> qualid val qualid_of_dirpath : dir_path -> qualid val qualid_of_ident : identifier -> qualid -(* Both names are passed to objects: a "semantic" [kernel_name], which +(** Both names are passed to objects: a "semantic" [kernel_name], which can be substituted and a "syntactic" [full_path] which can be printed *) @@ -155,16 +160,17 @@ type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name -(* to this type are mapped [dir_path]'s in the nametab *) +(** to this type are mapped [dir_path]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix | DirClosedSection of dir_path - (* this won't last long I hope! *) + (** this won't last long I hope! *) -(*s A [reference] is the user-level notion of name. It denotes either a +(** {6 ... } *) +(** A [reference] is the user-level notion of name. It denotes either a global name (referred either by a qualified name or by a single name) or a variable *) @@ -177,13 +183,13 @@ val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc -(*s Popping one level of section in global names *) +(** {6 Popping one level of section in global names } *) val pop_con : constant -> constant val pop_kn : mutual_inductive-> mutual_inductive val pop_global_reference : global_reference -> global_reference -(* Deprecated synonyms *) +(** Deprecated synonyms *) -val make_short_qualid : identifier -> qualid (* = qualid_of_ident *) -val qualid_of_sp : full_path -> qualid (* = qualid_of_path *) +val make_short_qualid : identifier -> qualid (** = qualid_of_ident *) +val qualid_of_sp : full_path -> qualid (** = qualid_of_path *) diff --git a/library/libobject.ml b/library/libobject.ml index 7b61a386..bc62913d 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Libnames @@ -18,7 +16,7 @@ open Mod_subst wants to work with restricted Coq programs that have only parts of the full capabilities, but may still be able to work correctly for limited purposes. One example is for the graphical interface, that uses - such a limite coq process to do only parsing. It loads .vo files, but + such a limited Coq process to do only parsing. It loads .vo files, but is only interested in loading the grammar rule definitions. *) let relax_flag = ref false;; @@ -57,7 +55,7 @@ let default_object s = { 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 accually + and the listed functions are only those which definitions actually differ from the default. This helps introducing new functions in objects. @@ -81,7 +79,7 @@ let object_tag lobj = Dyn.tag lobj let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) -let declare_object odecl = +let declare_object_full odecl = let na = odecl.object_name in let (infun,outfun) = Dyn.create na in let cacher (oname,lobj) = @@ -124,6 +122,8 @@ let declare_object odecl = dyn_rebuild_function = rebuild }; (infun,outfun) +let declare_object odecl = fst (declare_object_full odecl) + let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) (* this function describes how the cache, load, open, and export functions @@ -143,8 +143,9 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.warning ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)"); + Pp.msg_warning + (Pp.str ("Cannot find library functions for an object with tag " + ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () end; deflt diff --git a/library/libobject.mli b/library/libobject.mli index c0d89e4d..57c3debe 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,30 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Mod_subst -(*i*) -(* [Libobject] declares persistent objects, given with methods: +(** [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 sufixes. + 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 sufixes no shorter than the "int" argument + 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); @@ -39,7 +35,7 @@ open Mod_subst 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 explicitely + Anticipate - this is for objects that have to be explicitly managed by the [end_module] function (like Require and Read markers) @@ -74,7 +70,7 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -(* The default object is a "Keep" object with empty methods. +(** 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 = ... @@ -85,18 +81,22 @@ type 'a object_declaration = { val default_object : string -> 'a object_declaration -(* the identity substitution function *) +(** the identity substitution function *) val ident_subst_function : substitution * 'a -> 'a -(*s Given an object declaration, the function [declare_object] +(** {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 : +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 diff --git a/library/library.ml b/library/library.ml index 09f92e6a..37622874 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util @@ -68,8 +66,6 @@ let add_load_path isroot (phys_path,coq_path) = load_paths := (phys_path,coq_path,isroot) :: !load_paths; | _ -> anomaly ("Two logical paths are associated to "^phys_path) -let physical_paths (dp,lp) = dp - let extend_path_with_dirpath p dir = List.fold_left Filename.concat p (List.map string_of_id (List.rev (repr_dirpath dir))) @@ -119,7 +115,7 @@ type compilation_unit_name = dir_path type library_disk = { md_name : compilation_unit_name; - md_compiled : compiled_library; + md_compiled : LightenLibrary.lightened_compiled_library; md_objects : Declaremods.library_objects; md_deps : (compilation_unit_name * Digest.t) list; md_imports : compilation_unit_name list } @@ -215,9 +211,6 @@ let library_is_loaded dir = let library_is_opened dir = List.exists (fun m -> m.library_name = dir) !libraries_imports_list -let library_is_exported dir = - List.exists (fun m -> m.library_name = dir) !libraries_exports_list - let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list @@ -307,7 +300,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let (in_import, out_import) = +let in_import : dir_path * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -389,24 +382,41 @@ let try_locate_qualified_library (loc,qid) = (************************************************************************) (* Internalise libraries *) -let lighten_library m = - if !Flags.dont_load_proofs then lighten_library m else m - -let mk_library md digest = { - library_name = md.md_name; - library_compiled = lighten_library md.md_compiled; - library_objects = md.md_objects; - library_deps = md.md_deps; - library_imports = md.md_imports; - library_digest = digest } +let mk_library md table digest = + let md_compiled = + LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled + in { + library_name = md.md_name; + library_compiled = md_compiled; + library_objects = md.md_objects; + library_deps = md.md_deps; + library_imports = md.md_imports; + library_digest = digest + } + +let fetch_opaque_table (f,pos,digest) = + try + let ch = System.with_magic_number_check raw_intern_library f in + seek_in ch pos; + if System.marshal_in ch <> digest then failwith "File changed!"; + let table = (System.marshal_in ch : LightenLibrary.table) in + close_in ch; + table + with _ -> + error + ("The file "^f^" is inaccessible or has changed,\n" ^ + "cannot load some opaque constant bodies in it.\n") let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in - let md = System.marshal_in ch in + let lmd = System.marshal_in ch in + let pos = pos_in ch in let digest = System.marshal_in ch in + let table = lazy (fetch_opaque_table (f,pos,digest)) in + register_library_filename lmd.md_name f; + let library = mk_library lmd table digest in close_in ch; - register_library_filename md.md_name f; - mk_library md digest + library let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -453,9 +463,9 @@ let rec_intern_by_filename_only id f = (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin - Flags.if_verbose warning - ((string_of_dirpath m.library_name)^" is already loaded from file "^ - library_full_filename m.library_name); + Flags.if_warn msg_warning + (pr_dirpath m.library_name ++ str " is already loaded from file " ++ + str (library_full_filename m.library_name)); m.library_name, [] end else @@ -488,7 +498,7 @@ let rec_intern_library_from_file idopt f = type library_reference = dir_path list * bool option -let register_library (dir,m) = +let register_library m = Declaremods.register_library m.library_name m.library_compiled @@ -516,7 +526,9 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -let (in_require, out_require) = +type require_obj = library_t list * dir_path list * bool option + +let in_require : require_obj -> obj = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; @@ -531,9 +543,10 @@ let xml_require = ref (fun d -> ()) let set_xml_require f = xml_require := f let require_library_from_dirpath modrefl export = - let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in + let needed = List.fold_left rec_intern_library [] modrefl in + let needed = List.rev_map snd needed in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> @@ -551,8 +564,8 @@ let require_library qidl export = let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in - let needed = List.rev needed in - if Lib.is_modtype () || Lib.is_module () then begin + let needed = List.rev_map snd needed in + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) export @@ -568,7 +581,7 @@ let import_module export (loc,qid) = try match Nametab.locate_module qid with | MPfile dir -> - if Lib.is_modtype () || Lib.is_module () || not export then + if Lib.is_module_or_modtype () || not export then add_anonymous_leaf (in_import (dir, export)) else add_anonymous_leaf (in_import (dir, export)) @@ -620,6 +633,7 @@ let error_recursively_dependent_library dir = writing the content and computing the checksum... *) let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in + let cenv, table = LightenLibrary.save cenv in let md = { md_name = dir; md_compiled = cenv; @@ -632,8 +646,14 @@ let save_library_to dir f = try System.marshal_out ch md; flush ch; + (* The loading of the opaque definitions table is optional whereas + the digest is loaded all the time. As a consequence, the digest + must be serialized before the table (if we want to keep the + current simple layout of .vo files). This also entails that the + digest does not take opaque terms into account anymore. *) let di = Digest.file f' in System.marshal_out ch di; + System.marshal_out ch table; close_out ch with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e diff --git a/library/library.mli b/library/library.mli index bc939666..ed17ed15 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,21 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: library.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Libnames open Libobject -(*i*) -(*s This module provides functions to load, open and save +(** 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 @@ -23,43 +19,46 @@ open Libobject written at various dates. *) -(*s Require = load in the environment + open (if the optional boolean +(** {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 : qualid located list -> bool option -> unit val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit val require_library_from_file : identifier option -> System.physical_path -> bool option -> unit -(*s Open a module (or a library); if the boolean is true then it's also +(** {6 ... } *) +(** 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 located -> unit -(*s Start the compilation of a library *) +(** {6 Start the compilation of a library } *) val start_library : string -> dir_path * string -(*s End the compilation of a library and save it to a ".vo" file *) +(** {6 End the compilation of a library and save it to a ".vo" file } *) val save_library_to : dir_path -> string -> unit -(*s Interrogate the status of libraries *) +(** {6 Interrogate the status of libraries } *) - (* - Tell if a library is loaded or opened *) + (** - Tell if a library is loaded or opened *) val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool - (* - Tell which libraries are loaded or imported *) + (** - Tell which libraries are loaded or imported *) val loaded_libraries : unit -> dir_path list val opened_libraries : unit -> dir_path list - (* - Return the full filename of a loaded library. *) + (** - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string - (* - Overwrite the filename of all libraries (used when restoring a state) *) + (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(*s Hook for the xml exportation of libraries *) +(** {6 Hook for the xml exportation of libraries } *) val set_xml_require : (dir_path -> unit) -> unit -(*s Global load paths: a load path is a physical path in the file +(** {6 ... } *) +(** Global load paths: a load path is a physical path in the file system; to each load path is associated a Coq [dir_path] (the "logical" path of the physical path) *) @@ -70,7 +69,7 @@ val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path val is_in_load_paths : System.physical_path -> bool -(*s Locate a library in the load paths *) +(** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -79,5 +78,5 @@ val locate_qualified_library : bool -> qualid -> library_location * dir_path * System.physical_path val try_locate_qualified_library : qualid located -> dir_path * string -(*s Statistics: display the memory use of a library. *) +(** {6 Statistics: display the memory use of a library. } *) val mem : dir_path -> Pp.std_ppcmds diff --git a/library/nameops.ml b/library/nameops.ml index 6a4bec5a..799b8ebe 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -112,8 +110,6 @@ let add_prefix s id = id_of_string (s ^ string_of_id id) let atompart_of_id id = fst (repr_ident id) -let lift_ident = lift_subscript - (* Names *) let out_name = function diff --git a/library/nameops.mli b/library/nameops.mli index e549d506..f3f9f752 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,24 +1,22 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nameops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names -(* Identifiers and names *) +(** Identifiers and names *) val pr_id : identifier -> Pp.std_ppcmds val pr_name : name -> Pp.std_ppcmds val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option -val atompart_of_id : identifier -> string (* remove trailing digits *) -val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_$ *) +val atompart_of_id : identifier -> string (** remove trailing digits *) +val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier @@ -38,17 +36,17 @@ val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * val pr_lab : label -> Pp.std_ppcmds -(* some preset paths *) +(** some preset paths *) val default_library : dir_path -(* This is the root of the standard library of Coq *) +(** This is the root of the standard library of Coq *) val coq_root : module_ident -(* This is the default root prefix for developments which doesn't +(** This is the default root prefix for developments which doesn't mention a root *) val default_root_prefix : dir_path -(* Metavariables *) +(** Metavariables *) val pr_meta : Term.metavariable -> Pp.std_ppcmds val string_of_meta : Term.metavariable -> string diff --git a/library/nametab.ml b/library/nametab.ml index c4ea5953..6dbd927d 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,14 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util +open Compat open Pp open Names open Libnames @@ -20,10 +19,10 @@ exception GlobalizationError of qualid exception GlobalizationConstantError of qualid let error_global_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationError q) + Loc.raise loc (GlobalizationError q) let error_global_constant_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationConstantError q) + Loc.raise loc (GlobalizationConstantError q) let error_global_not_found q = raise (GlobalizationError q) @@ -109,9 +108,9 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Flags.if_verbose - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Flags.if_warn + msg_warning (str ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!")); current | Nothing | Relative _ -> Relative (uname,o) @@ -132,7 +131,7 @@ struct become unaccessible forever *) (* But ours is also absolute! This is an error! *) error ("Cannot mask the absolute name \"" - ^ U.to_string uname' ^ "\"!") + ^ U.to_string uname' ^ "\"!") | Nothing | Relative _ -> Absolute (uname,o), dirmap @@ -149,9 +148,9 @@ let rec push_exactly uname o level (current,dirmap) = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Flags.if_verbose - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Flags.if_warn + msg_warning (str ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!")); current | Nothing | Relative _ -> Relative (uname,o) @@ -288,10 +287,7 @@ let the_dirtab = ref (DirTab.empty : dirtab) (* Reversed name tables ***************************************************) (* This table translates extended_global_references back to section paths *) -module Globrevtab = Map.Make(struct - type t=extended_global_reference - let compare = compare - end) +module Globrevtab = Map.Make(ExtRefOrdered) type globrevtab = full_path Globrevtab.t let the_globrevtab = ref (Globrevtab.empty : globrevtab) @@ -379,7 +375,6 @@ let locate_modtype qid = SpTab.locate qid !the_modtypetab let full_name_modtype qid = SpTab.user_name qid !the_modtypetab let locate_tactic qid = SpTab.locate qid !the_tactictab -let full_name_tactic qid = SpTab.user_name qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab @@ -412,11 +407,6 @@ let locate_constant qid = | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found -let locate_mind qid = - match locate_extended qid with - | TrueGlobal (IndRef (kn,0)) -> kn - | _ -> raise Not_found - let global_of_path sp = match SpTab.find sp !the_ccitab with | TrueGlobal ref -> ref @@ -424,9 +414,6 @@ let global_of_path sp = let extended_global_of_path sp = SpTab.find sp !the_ccitab -let locate_in_absolute_module dir id = - global_of_path (make_path dir id) - let global r = let (loc,qid) = qualid_of_reference r in try match locate_extended qid with @@ -450,8 +437,6 @@ let exists_module = exists_dir let exists_modtype sp = SpTab.exists sp !the_modtypetab -let exists_tactic sp = SpTab.exists sp !the_tactictab - (* Reverse locate functions ***********************************************) let path_of_global ref = diff --git a/library/nametab.mli b/library/nametab.mli index d0c24bfa..c5b55f2c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,86 +1,78 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Pp open Names open Libnames -(*i*) -(*s This module contains the tables for globalization, which - associates internal object references to qualified names (qualid). +(** This module contains the tables for globalization. *) - There are three classes of names: +(** 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], [dir_path] + - 1a) internal kernel names: [kernel_name], [constant], [inductive], + [module_path], [dir_path] - 1b- other internal names: [global_reference], [syndef_name], + - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... - 2- full, non ambiguous user names: [full_path] + - 2) full, non ambiguous user names: [full_path] - 3- non necessarily full, possibly ambiguous user names: [reference] - and [qualid] + - 3) non necessarily full, possibly ambiguous user names: [reference] + and [qualid] *) -(* Most functions in this module fall into one of the following categories: - \begin{itemize} - \item [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 [dir_path]. - - \item [exists : full_user_name -> bool] +(** Most functions in this module fall into one of the following categories: +{ul {- [push : visibility -> full_user_name -> object_reference -> unit] - Is the [full_user_name] already atributed as an absolute user name - of some object? + 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 [dir_path]. + } + {- [exists : full_user_name -> bool] - \item [locate : qualid -> object_reference] + 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] + Finds the object referred to by [qualid] or raises [Not_found] + } + {- [full_name : qualid -> full_user_name] - \item [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] - Finds the full user name referred to by [qualid] or raises [Not_found] + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [identifier]. Such a function can also have a + local context argument.}} - \item [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 [identifier]. Such a function can also have a - local context argument. - \end{itemize} *) exception GlobalizationError of qualid exception GlobalizationConstantError of qualid -(* Raises a globalization error *) +(** Raises a globalization error *) val error_global_not_found_loc : loc -> qualid -> 'a val error_global_not_found : qualid -> 'a val error_global_constant_not_found_loc : loc -> qualid -> 'a -(*s Register visibility of things *) - -(* The visibility can be registered either - \begin{itemize} +(** {6 Register visibility of things } *) - \item for all suffixes not shorter then a given int -- when the +(** The visibility can be registered either + - for all suffixes not shorter then a given int -- when the object is loaded inside a module -- or - - \item for a precise suffix, when the module containing (the module + - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) - \end{itemize} + *) type visibility = Until of int | Exactly of int @@ -94,9 +86,9 @@ type ltac_constant = kernel_name val push_tactic : visibility -> full_path -> ltac_constant -> unit -(*s The following functions perform globalization of qualified names *) +(** {6 The following functions perform globalization of qualified names } *) -(* These functions globalize a (partially) qualified name or fail with +(** These functions globalize a (partially) qualified name or fail with [Not_found] *) val locate : qualid -> global_reference @@ -109,42 +101,43 @@ val locate_module : qualid -> module_path val locate_section : qualid -> dir_path val locate_tactic : qualid -> ltac_constant -(* These functions globalize user-level references into global +(** 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 : reference -> global_reference val global_inductive : reference -> inductive -(* These functions locate all global references with a given suffix; +(** 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 -> global_reference list val locate_extended_all : qualid -> extended_global_reference list -(* Mapping a full path to a global reference *) +(** Mapping a full path to a global reference *) val global_of_path : full_path -> global_reference val extended_global_of_path : full_path -> extended_global_reference -(*s These functions tell if the given absolute name is already taken *) +(** {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 : dir_path -> bool -val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *) -val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *) +val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *) -(*s These functions locate qualids into full user names *) +(** {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 -> dir_path -(*s Reverse lookup -- finding user names corresponding to the given +(** {6 Reverse lookup } + Finding user names corresponding to the given internal name *) -(* Returns the full path bound to a global reference or syntactic +(** 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 @@ -152,17 +145,17 @@ val path_of_global : global_reference -> full_path val dirpath_of_module : module_path -> dir_path val path_of_tactic : ltac_constant -> full_path -(* Returns in particular the dirpath or the basename of the full path +(** Returns in particular the dirpath or the basename of the full path associated to global reference *) val dirpath_of_global : global_reference -> dir_path val basename_of_global : global_reference -> identifier -(* Printing of global references using names as short as possible *) +(** Printing of global references using names as short as possible *) val pr_global_env : Idset.t -> global_reference -> std_ppcmds -(* The [shortest_qualid] functions given an object with [user_name] +(** 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. *) @@ -172,7 +165,7 @@ val shortest_qualid_of_modtype : module_path -> qualid val shortest_qualid_of_module : module_path -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid -(* Deprecated synonyms *) +(** Deprecated synonyms *) val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> global_reference (* = global_of_path *) +val absolute_reference : full_path -> global_reference (** = global_of_path *) diff --git a/library/states.ml b/library/states.ml index 679f9028..c88858f7 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open System type state = Lib.frozen * Summary.frozen @@ -22,7 +20,10 @@ let unfreeze (fl,fs) = let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number ".coq" in - (fun s -> raw_extern s (freeze())), + (fun s -> + if !Flags.load_proofs <> Flags.Force then + Util.error "Write State only works with option -force-load-proofs"; + raw_extern s (freeze())), (fun s -> unfreeze (with_magic_number_check (raw_intern (Library.get_load_paths ())) s); diff --git a/library/states.mli b/library/states.mli index fc6497b6..4f114d57 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,14 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: states.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** {6 States of the system} *) -(*s States of the system. In that module, we provide functions to get +(** 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. *) @@ -20,13 +20,14 @@ type state val freeze : unit -> state val unfreeze : state -> unit -(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the +(** {6 Rollback } *) + +(** [with_heavy_rollback f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation if an exception is raised. *) - val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b -(*s [with_state_protection f x] applies [f] to [x] and restores the +(** [with_state_protection f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation of f *) val with_state_protection : ('a -> 'b) -> 'a -> 'b diff --git a/library/summary.ml b/library/summary.ml index a40a9354..697f57e8 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: summary.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util diff --git a/library/summary.mli b/library/summary.mli index 5db9617b..5963b23b 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: summary.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(* This module registers the declaration of global tables, which will be kept +(** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) type 'a summary_declaration = { |