From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- library/decl_kinds.ml | 29 +- library/decl_kinds.mli | 84 +++++ library/declare.ml | 191 ++--------- library/declare.mli | 24 +- library/declaremods.ml | 734 +++++++++++++++++++++++++++++++++---------- library/declaremods.mli | 29 +- library/decls.ml | 76 +++++ library/decls.mli | 47 +++ library/dischargedhypsmap.ml | 2 +- library/global.ml | 12 +- library/global.mli | 18 +- library/goptions.ml | 6 +- library/goptions.mli | 3 +- library/heads.ml | 190 +++++++++++ library/heads.mli | 28 ++ library/impargs.ml | 375 ++++++++++++++-------- library/impargs.mli | 33 +- library/lib.ml | 233 ++++++++++---- library/lib.mli | 22 +- library/libnames.ml | 3 +- library/libnames.mli | 2 +- library/libobject.ml | 21 +- library/libobject.mli | 16 +- library/library.ml | 88 +++--- library/nameops.ml | 2 +- library/nameops.mli | 2 +- library/nametab.ml | 31 +- library/nametab.mli | 12 +- 28 files changed, 1667 insertions(+), 646 deletions(-) create mode 100644 library/decl_kinds.mli create mode 100644 library/decls.ml create mode 100644 library/decls.mli create mode 100644 library/heads.ml create mode 100644 library/heads.mli (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index af54df2f..8f2525b8 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *) +(* $Id: decl_kinds.ml 11024 2008-05-30 12:41:39Z msozeau $ *) open Util +open Libnames (* Informal mathematical status of declarations *) -type locality_flag = (*bool (* local = true; global = false *)*) +type locality = | Local | Global @@ -38,8 +39,8 @@ type definition_object_kind = | Scheme | StructureComponent | IdentityCoercion - -type strength = locality_flag (* For compatibility *) + | Instance + | Method type assumption_object_kind = Definitional | Logical | Conjectural @@ -51,9 +52,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality_flag * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality_flag * boxed_flag * definition_object_kind +type definition_kind = locality * boxed_flag * definition_object_kind (* Kinds used in proofs *) @@ -61,7 +62,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality_flag * goal_object_kind +type goal_kind = locality * goal_object_kind (* Kinds used in library *) @@ -97,5 +98,17 @@ let string_of_definition_kind (l,boxed,d) = | Global, Example -> "Example" | Local, (CanonicalStructure|Example) -> anomaly "Unsupported local definition kind" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion) + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> anomaly "Internal definition kind" + +(* Strength *) + +let strength_of_global = function + | VarRef _ -> Local + | IndRef _ | ConstructRef _ | ConstRef _ -> Global + +let string_of_strength = function + | Local -> "Local" + | Global -> "Global" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli new file mode 100644 index 00000000..9358c4b5 --- /dev/null +++ b/library/decl_kinds.mli @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* logical_kind +val string_of_theorem_kind : theorem_kind -> string +val string_of_definition_kind : + locality * boxed_flag * definition_object_kind -> string + +(* About locality *) + +val strength_of_global : global_reference -> locality +val string_of_strength : locality -> string diff --git a/library/declare.ml b/library/declare.ml index 02bdb1cf..07810e3c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 9488 2007-01-17 11:11:58Z herbelin $ *) +(* $Id: declare.ml 10840 2008-04-23 21:29:34Z herbelin $ *) + +(** This module is about the low-level declaration of logical objects *) open Pp open Util @@ -17,97 +19,58 @@ open Term open Sign open Declarations open Entries -open Inductive -open Indtypes -open Reduction -open Type_errors -open Typeops open Libobject open Lib open Impargs -open Nametab open Safe_typing +open Cooking +open Decls open Decl_kinds -(**********************************************) - -(* Strength *) - -open Nametab +(** XML output hooks *) -let strength_min (stre1,stre2) = - if stre1 = Local or stre2 = Local then Local else Global - -let string_of_strength = function - | Local -> "(local)" - | Global -> "(global)" - -(* XML output hooks *) let xml_declare_variable = ref (fun (sp:object_name) -> ()) let xml_declare_constant = ref (fun (sp:bool * constant)-> ()) let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ()) -let if_xml f x = if !Options.xml_export then f x else () +let if_xml f x = if !Flags.xml_export then f x else () let set_xml_declare_variable f = xml_declare_variable := if_xml f let set_xml_declare_constant f = xml_declare_constant := if_xml f let set_xml_declare_inductive f = xml_declare_inductive := if_xml f -(* Section variables. *) +(** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types + | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind -type checked_section_variable = - | CheckedSectionLocalDef of constr * types * Univ.constraints * bool - | CheckedSectionLocalAssum of types * Univ.constraints - -type checked_variable_declaration = - dir_path * checked_section_variable * logical_kind - -let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) - -let _ = Summary.declare_summary "VARIABLE" - { Summary.freeze_function = (fun () -> !vartab); - Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } - let cache_variable ((sp,_),o) = match o with | Inl cst -> Global.add_constraints cst | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) - if Idmap.mem id !vartab then + if variable_exists id then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); - let vd = match d with (* Fails if not well-typed *) - | SectionLocalAssum ty -> + let impl,opaq,cst,keep = match d with (* Fails if not well-typed *) + | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in - let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalAssum (ty,cst) + impl, true, cst, (if keep then Some ty else None) | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in - let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in + false, opaq, cst, None in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id; + add_section_variable id impl keep; Dischargedhypsmap.set_discharged_hyps sp []; - vartab := Idmap.add id (p,vd,mk) !vartab - -let get_variable_constraints id = - match pi2 (Idmap.find id !vartab) with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst - | CheckedSectionLocalAssum (ty,cst) -> cst + add_variable_data id (p,opaq,cst,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> Some (Inl (get_variable_constraints id)) + | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (in_variable, out_variable) = +let (inVariable, outVariable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -115,25 +78,17 @@ let (in_variable, out_variable) = (* for initial declaration *) let declare_variable id obj = - let oname = add_leaf id (in_variable (Inr (id,obj))) in + let oname = add_leaf id (inVariable (Inr (id,obj))) in declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); + Heads.declare_head (EvalVarRef id); !xml_declare_variable oname; oname -(* Globals: constants and parameters *) +(** Declaration of constants and parameters *) type constant_declaration = constant_entry * logical_kind -let csttab = ref (Spmap.empty : logical_kind Spmap.t) - -let _ = Summary.declare_summary "CONSTANT" - { Summary.freeze_function = (fun () -> !csttab); - Summary.unfreeze_function = (fun ft -> csttab := ft); - Summary.init_function = (fun () -> csttab := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } - (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn),(_,_,kind)) = @@ -141,7 +96,7 @@ let load_constant i ((sp,kn),(_,_,kind)) = errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists"); Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)); - csttab := Spmap.add sp kind !csttab + add_constant_kind (constant_of_kn kn) kind (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = @@ -150,18 +105,14 @@ let open_constant i ((sp,kn),_) = let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in - if Idmap.mem id !vartab or Nametab.exists_cci sp then + if variable_exists id or Nametab.exists_cci sp then errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); 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)); add_section_constant kn' (Global.lookup_constant kn').const_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - csttab := Spmap.add sp kind !csttab - -(*s Registration as global tables and rollback. *) - -open Cooking + add_constant_kind (constant_of_kn kn) kind let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in @@ -177,7 +128,7 @@ 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) +let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk @@ -185,7 +136,7 @@ let export_constant cst = Some (dummy_constant cst) let classify_constant (_,cst) = Substitute (dummy_constant cst) -let (in_constant, out_constant) = +let (inConstant, outConstant) = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -196,19 +147,20 @@ let (in_constant, out_constant) = export_function = export_constant } let hcons_constant_declaration = function - | DefinitionEntry ce when !Options.hash_cons_proofs -> + | 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_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 (in_constant (cd,dhyps,kind)) in + let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in let kn = constant_of_kn kn in declare_constant_implicits kn; + Heads.declare_head (EvalConstRef kn); Notation.declare_ref_arguments_scope (ConstRef kn); kn @@ -221,7 +173,7 @@ let declare_constant_gen internal id (cd,kind) = let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false -(* Inductives. *) +(** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = list_iter_i (fun i {mind_entry_consnames=lc} -> @@ -251,7 +203,7 @@ let inductive_names sp kn mie = in names let check_exists_inductive (sp,_) = - (if Idmap.mem (basename sp) !vartab then + (if variable_exists (basename sp) then errorlabstrm "" (pr_id (basename sp) ++ str " already exists")); if Nametab.exists_cci sp then @@ -301,7 +253,7 @@ let dummy_inductive_entry (_,m) = ([],{ let export_inductive x = Some (dummy_inductive_entry x) -let (in_inductive, out_inductive) = +let (inInductive, outInductive) = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -316,84 +268,9 @@ let declare_mind isrecord mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in - let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in + let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in declare_mib_implicits kn; declare_inductive_argument_scopes kn mie; !xml_declare_inductive (isrecord,oname); oname -(*s Test and access functions. *) - -let is_constant sp = - try let _ = Spmap.find sp !csttab in true with Not_found -> false - -let constant_strength sp = Global -let constant_kind sp = Spmap.find sp !csttab - -let get_variable id = - let (p,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty) - | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) - -let variable_strength _ = Local - -let find_section_variable id = - let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id - -let variable_opacity id = - let (_,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq - | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *) - -let variable_kind id = - pi3 (Idmap.find id !vartab) - -let clear_proofs sign = - List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in - Environ.push_named_context_val d signv) sign Environ.empty_named_context_val - -(* Global references. *) - -let first f v = - let n = Array.length v in - let rec look_for i = - if i = n then raise Not_found; - try f i v.(i) with Not_found -> look_for (succ i) - in - look_for 0 - -let mind_oper_of_id sp id mib = - first - (fun tyi mip -> - if id = mip.mind_typename then - IndRef (sp,tyi) - else - first - (fun cj cid -> - if id = cid then - ConstructRef ((sp,tyi),succ cj) - else raise Not_found) - mip.mind_consnames) - mib.mind_packets - -let last_section_hyps dir = - fold_named_context - (fun (id,_,_) sec_ids -> - try - let (p,_,_) = Idmap.find id !vartab in - if dir=p then id::sec_ids else sec_ids - with Not_found -> sec_ids) - (Environ.named_context (Global.env())) - ~init:[] - -let is_section_variable = function - | VarRef _ -> true - | _ -> false - -let strength_of_global = function - | VarRef _ -> Local - | IndRef _ | ConstructRef _ | ConstRef _ -> Global diff --git a/library/declare.mli b/library/declare.mli index 938bfd06..78d3f027 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 7941 2006-01-28 23:07:59Z herbelin $ i*) +(*i $Id: declare.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) (*i*) open Names @@ -34,7 +34,7 @@ open Nametab type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types + | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -59,26 +59,6 @@ val declare_internal_constant : the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -val strength_min : strength * strength -> strength -val string_of_strength : strength -> string - -(*s Corresponding test and access functions. *) - -val is_constant : section_path -> bool -val constant_strength : section_path -> strength -val constant_kind : section_path -> logical_kind - -val get_variable : variable -> named_declaration -val variable_strength : variable -> strength -val variable_kind : variable -> logical_kind -val find_section_variable : variable -> section_path -val last_section_hyps : dir_path -> identifier list -val clear_proofs : named_context -> Environ.named_context_val - -(*s Global references *) - -val strength_of_global : global_reference -> strength - (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (bool * constant -> unit) -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index aac2b599..123417a6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) - +(*i $Id: declaremods.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) open Pp open Util open Names @@ -78,22 +77,29 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = - ref (([],None,None) : mod_bound_id list * module_type_entry option - * module_type_body option) + ref (([],None,None) : mod_bound_id list * module_struct_entry option + * struct_expr_body option) + +(* The library_cache here is needed to avoid recalculations of + substituted modules object during "reloading" of libraries *) +let library_cache = ref Dirmap.empty let _ = Summary.declare_summary "MODULE-INFO" { Summary.freeze_function = (fun () -> !modtab_substobjs, !modtab_objects, - !openmod_info); - Summary.unfreeze_function = (fun (sobjs,objs,info) -> + !openmod_info, + !library_cache); + Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> modtab_substobjs := sobjs; modtab_objects := objs; - openmod_info := info); + openmod_info := info; + library_cache := libcache); Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ([],None,None)); + openmod_info := ([],None,None); + library_cache := Dirmap.empty); Summary.survive_module = false; Summary.survive_section = false } @@ -107,6 +113,11 @@ let mp_of_kn kn = else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) +let is_bound mp = + match mp with + | MPbound _ -> true + | _ -> false + let dir_of_sp sp = let dir,id = repr_path sp in extend_dirpath dir id @@ -122,29 +133,32 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) -(* Check that a module type is not functorial *) - -let rec check_sig env = function - | MTBident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTBsig _ -> () - | MTBfunsig _ -> Modops.error_result_must_be_signature () - -let rec check_sig_entry env = function - | MTEident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTEsig _ -> () - | MTEfunsig _ -> Modops.error_result_must_be_signature () - | MTEwith (mte,_) -> check_sig_entry env mte +let scrape_alias mp = + Environ.scrape_alias mp (Global.env()) + (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) let check_subtypes mp sub_mtb = let env = Global.env () in - let mtb = (Environ.lookup_module mp env).mod_type in + let mtb = Environ.lookup_modtype mp env in + let sub_mtb = + {typ_expr = sub_mtb; + typ_strength = None; + typ_alias = empty_subst} in let _ = Environ.add_constraints (Subtyping.check_subtypes env mtb sub_mtb) in () (* The constraints are checked and forgot immediately! *) +let subst_substobjs dir mp (subst,mbids,msid,objs) = + match mbids with + | [] -> + let prefix = dir,(mp,empty_dirpath) in + let subst' = join_alias (map_msid msid mp) subst in + let subst = join subst' subst in + Some (subst_objects prefix (join (map_msid msid mp) subst) objs) + | _ -> None (* This function registers the visibility of the module and iterates through its components. It is called by plenty module functions *) @@ -176,7 +190,6 @@ let do_module exists what iter_objects i dir mp substobjs objects = iter_objects (i+1) prefix seg | None -> () - let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted = let dir,mp = dir_of_sp sp, mp_of_kn kn in @@ -194,21 +207,25 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = | Some (me,sub_mte_o) -> let sub_mtb_o = match sub_mte_o with None -> None - | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte) + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) in - + let mp = Global.add_module (basename sp) me in - if mp <> mp_of_kn kn then - anomaly "Kernel and Library names do not match"; + if mp <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; - match sub_mtb_o with - None -> () - | Some sub_mtb -> check_subtypes mp sub_mtb + match sub_mtb_o with + None -> () + | Some (sub_mtb,sub) -> + check_subtypes mp sub_mtb in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted + + (* TODO: This check is not essential *) let check_empty s = function | None -> () @@ -231,18 +248,16 @@ let open_module i (oname,(entry,substobjs,substituted)) = conv_names_do_module true "open" open_objects i oname substobjs substituted -let subst_substobjs dir mp (subst,mbids,msid,objs) = - match mbids with - | [] -> - let prefix = dir,(mp,empty_dirpath) in - Some (subst_objects prefix (add_msid msid mp subst) objs) - | _ -> None - let subst_module ((sp,kn),subst,(entry,substobjs,_)) = check_empty "subst_module" entry; let dir,mp = dir_of_sp sp, mp_of_kn kn in let (sub,mbids,msid,objs) = substobjs in + let sub = subst_key subst sub in + let sub' = update_subst_alias subst sub in + let sub' = update_subst_alias sub' (map_msid msid mp) in + (* let sub = join_alias sub sub' in*) + let sub = join sub' sub in let subst' = join sub subst in (* substitutive_objects get the new substitution *) let substobjs = (subst',mbids,msid,objs) in @@ -256,6 +271,8 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = let classify_module (_,(_,substobjs,_)) = Substitute (None,substobjs,None) + + let (in_module,out_module) = declare_object {(default_object "MODULE") with cache_function = cache_module; @@ -266,6 +283,182 @@ let (in_module,out_module) = export_function = (fun _ -> anomaly "No modules in sections!") } +let rec replace_alias modalias_obj obj = + let rec put_alias (id_alias,obj_alias) l = + match l with + [] -> [] + | (id,o)::r + when ( object_tag o = "MODULE") -> + if id = id_alias then +(* let (entry,subst_o,substed_o) = out_module_alias obj_alias in + let (entry',subst_o',substed_o') = out_module o in + begin + match substed_o,substed_o' with + Some a,Some b -> + (id,in_module_alias + (entry,subst_o',Some (dump_alias_object a b)))::r*) + (id_alias,obj_alias)::r + (* | _,_ -> (id,o)::r + end*) + else (id,o)::(put_alias (id_alias,obj_alias) r) + | e::r -> e::(put_alias (id_alias,obj_alias) r) in + let rec choose_obj_alias list_alias list_obj = + match list_alias with + | [] -> list_obj + | o::r ->choose_obj_alias r (put_alias o list_obj) in + choose_obj_alias modalias_obj obj + +and dump_alias_object alias_obj obj = + let rec alias_in_obj seg = + match seg with + | [] -> [] + | (id,o)::r when (object_tag o = "MODULE ALIAS") -> + (id,o)::(alias_in_obj r) + | e::r -> (alias_in_obj r) in + let modalias_obj = alias_in_obj alias_obj in + replace_alias modalias_obj obj + +and do_module_alias exists what iter_objects i dir mp alias substobjs objects = + let prefix = (dir,(alias,empty_dirpath)) in + let alias_objects = + try Some (MPmap.find alias !modtab_objects) with + Not_found -> None in + let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let vis = + if exists then + if + try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo + with Not_found -> false + then + Nametab.Exactly i + else + errorlabstrm (what^"_module") + (pr_dirpath dir ++ str " should already exist!") + else + if Nametab.exists_dir dir then + errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") + else + Nametab.Until i + in + Nametab.push_dir vis dir dirinfo; + modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; + match alias_objects,objects with + Some (_,seg), Some seg' -> + let new_seg = dump_alias_object seg seg' in + modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects; + iter_objects (i+1) prefix new_seg + | _,_-> () + +and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias = match entry with + | None -> + anomaly "You must not recache interactive modules!" + | Some (me,sub_mte_o) -> + let sub_mtb_o = match sub_mte_o with + None -> None + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) + in + + let mp' = match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + Global.add_alias (basename sp) mp + | _ -> anomaly "cache module alias" + in + if mp' <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; + + let _ = match sub_mtb_o with + None -> () + | Some (sub_mtb,sub) -> + check_subtypes mp' sub_mtb in + match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "cache module alias" + in + do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted + +and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + in + do_module_alias false "load" load_objects i dir mp alias substobjs substituted + +and open_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + in + do_module_alias true "open" open_objects i dir mp alias substobjs substituted + +and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = + let dir,mp = dir_of_sp sp, mp_of_kn kn in + let (sub,mbids,msid,objs) = substobjs in + let sub' = update_subst_alias subst (map_msid msid mp) in + let subst' = join sub' subst in + let subst' = join sub subst' in + (* substitutive_objects get the new substitution *) + let substobjs = (subst',mbids,msid,objs) in + (* if we are not a functor - calculate substitued. + We add "msid |-> mp" to the substitution *) + match entry with + | Some (me,sub)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp')} -> + let mp' = subst_mp subst' mp' in + let mp' = scrape_alias mp' in + (Some ({mod_entry_type = None; + mod_entry_expr = + Some (MSEident mp')},sub), + substobjs, match mbids with + | [] -> + Some (subst_objects (dir,(mp',empty_dirpath)) + (join subst' (join (map_msid msid mp') + (map_mp mp mp'))) objs) + | _ -> None) + + | _ -> anomaly "Modops: Not an alias" + end + | None -> anomaly "Modops: Empty info" + +and classify_module_alias (_,(entry,substobjs,_)) = + Substitute (entry,substobjs,None) + +let (in_module_alias,out_module_alias) = + declare_object {(default_object "MODULE ALIAS") with + cache_function = cache_module_alias; + open_function = open_module_alias; + classify_function = classify_module_alias; + subst_function = subst_module_alias; + load_function = load_module_alias; + export_function = (fun _ -> anomaly "No modules in sections!") } + + + + + let cache_keep _ = anomaly "This module should not be cached!" let load_keep i ((sp,kn),seg) = @@ -298,7 +491,7 @@ let (in_modkeep,out_modkeep) = The module M gets its objects from SIG *) let modtypetab = - ref (KNmap.empty : substitutive_objects KNmap.t) + ref (MPmap.empty : substitutive_objects MPmap.t) (* currently started interactive module type. We remember its arguments if it is a functor type *) @@ -312,22 +505,20 @@ let _ = Summary.declare_summary "MODTYPE-INFO" modtypetab := fst ft; openmodtype_info := snd ft); Summary.init_function = (fun () -> - modtypetab := KNmap.empty; + modtypetab := MPmap.empty; openmodtype_info := []); Summary.survive_module = false; Summary.survive_section = true } - - let cache_modtype ((sp,kn),(entry,modtypeobjs)) = let _ = match entry with | None -> anomaly "You must not recache interactive module types!" | Some mte -> - let kn' = Global.add_modtype (basename sp) mte in - if kn' <> kn then + let mp = Global.add_modtype (basename sp) mte in + if mp <>mp_of_kn kn then anomaly "Kernel and Library names do not match" in @@ -335,9 +526,9 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until 1) sp kn; + Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let load_modtype i ((sp,kn),(entry,modtypeobjs)) = @@ -347,23 +538,22 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until i) sp kn; + Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let open_modtype i ((sp,kn),(entry,_)) = check_empty "open_modtype" entry; if - try Nametab.locate_modtype (qualid_of_sp sp) <> kn + try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) with Not_found -> true then errorlabstrm ("open_modtype") (pr_sp sp ++ str " should already exist!"); - Nametab.push_modtype (Nametab.Exactly i) sp kn - + Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = check_empty "subst_modtype" entry; @@ -381,77 +571,106 @@ let (in_modtype,out_modtype) = load_function = load_modtype; subst_function = subst_modtype; classify_function = classify_modtype; - export_function = in_some } + export_function = Option.make } -let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = - if mbids<>[] then +let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = + let rec mp_rec = function + | [] -> MPself msid + | i::r -> MPdot(mp_rec r,label_of_id i) + in + 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,modobjs,None))::tail - | _ -> - let (_,substobjs,_) = out_module obj in - let substobjs' = replace_module_object idl substobjs modobjs in - (id, in_module (None,substobjs',None))::tail - ) - else error "MODULE expected!" - | idl,lobj::tail -> lobj::replace_idl (idl,tail) - in - (subst, mbids, msid, replace_idl (idl,lib_stack)) - + 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_alias (Some + ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)},None) + ,modobjs,None))::tail + | _ -> + let (_,substobjs,_) = out_module obj in + let substobjs' = replace_module_object idl substobjs modobjs mp in + (id, in_module (None,substobjs',None))::tail + ) + else error "MODULE expected!" + | idl,lobj::tail -> lobj::replace_idl (idl,tail) + in + (join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) + let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) - -let rec get_modtype_substobjs = function - MTEident ln -> KNmap.find ln !modtypetab - | MTEfunsig (mbid,_,mte) -> - let (subst, mbids, msid, objs) = get_modtype_substobjs mte in +let rec get_modtype_substobjs env = function + MSEident ln -> MPmap.find ln !modtypetab + | MSEfunctor (mbid,_,mte) -> + let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in (subst, mbid::mbids, msid, objs) - | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty - | MTEwith (mty, With_Module (idl,mp)) -> - let substobjs = get_modtype_substobjs mty in + | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_modtype_substobjs env mty in let modobjs = MPmap.find mp !modtab_substobjs in - replace_module_object idl substobjs modobjs - | MTEsig (msid,_) -> - todo "Anonymous module types"; (empty_subst, [], msid, []) + replace_module_object idl substobjs modobjs mp + | MSEapply (mexpr, MSEident mp) -> + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in + let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + (match mbids with + | mbid::mbids -> + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst (map_mbid mbid mp (Some resolve))) + sub3) + , mbids, msid, objs) + | [] -> match mexpr with + | MSEident _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") + | MSEapply (_,mexpr) -> + Modops.error_application_to_not_path mexpr + (* 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) = let dir = make_dirpath [id] in let mp = MPbound mbid in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in let substituted = subst_substobjs dir mp substobjs in do_module false "start" load_objects 1 dir mp substobjs substituted in List.iter2 process_arg argids args - -let replace_module mtb id mb = todo "replace module after with"; mtb - -let rec get_some_body mty env = match mty with - MTEident kn -> Environ.lookup_modtype kn env - | MTEfunsig _ - | MTEsig _ -> anomaly "anonymous module types not supported" - | MTEwith (mty,With_Definition _) -> get_some_body mty env - | MTEwith (mty,With_Module (id,mp)) -> - replace_module (get_some_body mty env) id (Environ.lookup_module mp env) - - let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in List.map2 (fun dir mbid -> Global.add_module_parameter mbid mty; @@ -472,39 +691,35 @@ let start_module interp_modtype export id args res_o = | Some (res, restricted) -> (* we translate the module here to catch errors as early as possible *) let mte = interp_modtype (Global.env()) res in - check_sig_entry (Global.env()) mte; if restricted then Some mte, None else - let mtb = Mod_typing.translate_modtype (Global.env()) mte in + let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in let sub_mtb = List.fold_right (fun (arg_id,arg_t) mte -> - let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t - in MTBfunsig(arg_id,arg_t,mte)) + let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t + in + let arg_t = {typ_expr = arg_t; + typ_strength = None; + typ_alias = sub} in + SEBfunctor(arg_id,arg_t,mte)) arg_entries mtb in None, Some sub_mtb in let mbids = List.map fst arg_entries in - openmod_info:=(mbids,res_entry_o,sub_body_o); + openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_module id = let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in let mbids, res_o, sub_o = !openmod_info in - let mp = Global.end_module id res_o in - - begin match sub_o with - None -> () - | Some sub_mtb -> check_subtypes mp sub_mtb - end; - let substitute, keep, special = Lib.classify_segment lib_stack in let dir = fst oldprefix in @@ -514,21 +729,27 @@ let end_module id = match res_o with | None -> (empty_subst, mbids, msid, substitute), keep, special - | Some (MTEident ln) -> - abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], [] - | Some (MTEsig (msid,_)) -> - todo "Anonymous signatures not supported"; - (empty_subst, mbids, msid, []), keep, special - | Some (MTEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs mty), [], [] - | Some (MTEfunsig _) -> + | Some (MSEident ln) -> + abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], [] + | Some (MSEwith _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + | Some (MSEfunctor _) -> anomaly "Funsig cannot be here..." - with + | Some (MSEapply _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + with Not_found -> anomaly "Module objects not found..." in - - (* must be called after get_modtype_substobjs, because of possible + (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) + + let mp = Global.end_module id res_o in + + begin match sub_o with + None -> () + | Some sub_mtb -> check_subtypes mp sub_mtb + end; + Summary.module_unfreeze_summaries fs; let substituted = subst_substobjs dir mp substobjs in @@ -546,7 +767,8 @@ let end_module id = if mp_of_kn (snd newoname) <> mp then anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state () (* to prevent recaching *) + Lib.add_frozen_state () (* to prevent recaching *); + mp @@ -566,18 +788,13 @@ type library_objects = mod_self_id * lib_objects * lib_objects -(* The library_cache here is needed to avoid recalculations of - substituted modules object during "reloading" of libraries *) -let library_cache = Hashtbl.create 17 - - let register_library dir cenv objs digest = let mp = MPfile dir in let substobjs, objects = try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) - Hashtbl.find library_cache dir + Dirmap.find dir !library_cache with Not_found -> if mp <> Global.import cenv digest then @@ -585,9 +802,9 @@ let register_library dir cenv objs digest = let msid,substitute,keep = objs in let substobjs = empty_subst, [], msid, substitute in let substituted = subst_substobjs dir mp substobjs in - let objects = option_map (fun seg -> seg@keep) substituted in + let objects = Option.map (fun seg -> seg@keep) substituted in let modobjs = substobjs, objects in - Hashtbl.add library_cache dir modobjs; + library_cache := Dirmap.add dir modobjs !library_cache; modobjs in do_module false "register_library" load_objects 1 dir mp substobjs objects @@ -625,16 +842,17 @@ let classify_import (_,(export,_ as obj)) = if export then Substitute obj else Dispose let subst_import (_,subst,(export,mp as obj)) = - let mp' = subst_mp subst mp in + let subst' = remove_alias subst in + let mp' = subst_mp subst' mp in if mp'==mp then obj else (export,mp') - + let (in_import,out_import) = declare_object {(default_object "IMPORT MODULE") with - cache_function = cache_import; - open_function = (fun i o -> if i=1 then cache_import o); - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import; + open_function = (fun i o -> if i=1 then cache_import o); + subst_function = subst_import; + classify_function = classify_import } let import_module export mp = @@ -642,7 +860,6 @@ let import_module export mp = (************************************************************************) (* module types *) - let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in @@ -653,7 +870,7 @@ let start_modtype interp_modtype id args = openmodtype_info := mbids; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_modtype id = @@ -673,76 +890,202 @@ let end_modtype id = if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; - if snd oname <> ln then + if (mp_of_kn (snd oname)) <> ln then anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state ()(* to prevent recaching *) + Lib.add_frozen_state ()(* to prevent recaching *); + ln let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in - let _ = Global.start_modtype id in + try + let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let base_mty = interp_modtype (Global.env()) mty in let entry = List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries base_mty in - let substobjs = get_modtype_substobjs entry in + let substobjs = get_modtype_substobjs (Global.env()) entry in + (* Undo the simulated interactive building of the module type *) + (* and declare the module type as a whole *) Summary.unfreeze_summaries fs; - ignore (add_leaf id (in_modtype (Some entry, substobjs))) + ignore (add_leaf id (in_modtype (Some entry, substobjs))); + mmp + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e let rec get_module_substobjs env = function - | MEident mp -> MPmap.find mp !modtab_substobjs - | MEfunctor (mbid,mty,mexpr) -> + | MSEident mp -> MPmap.find mp !modtab_substobjs + | MSEfunctor (mbid,mty,mexpr) -> let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) - | MEstruct (msid,_) -> - (empty_subst, [], msid, []) - | MEapply (mexpr, MEident mp) -> - let feb,ftb = Mod_typing.translate_mexpr env mexpr in - let ftb = Modops.scrape_modtype env ftb in - let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in + | MSEapply (mexpr, MSEident mp) -> + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in + + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp env in - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst (map_mbid mbid mp (Some resolve))) + sub3) + , mbids, msid, objs) | [] -> match mexpr with - | MEident _ | MEstruct _ -> error "Application of a non-functor" + | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") - | MEapply (_,mexpr) -> + | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr + | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_module_substobjs env mty in + let modobjs = MPmap.find mp !modtab_substobjs in + replace_module_object idl substobjs modobjs mp + + +(* Include *) + +let rec subst_inc_expr subst me = + match me with + | MSEident mp -> MSEident (subst_mp subst mp) + | MSEwith (me,With_Module(idl,mp)) -> + MSEwith (subst_inc_expr subst me, + With_Module(idl,subst_mp subst mp)) + | MSEwith (me,With_Definition(idl,const))-> + let const1 = Mod_subst.from_val const in + let force = Mod_subst.force subst_mps in + MSEwith (subst_inc_expr subst me, + With_Definition(idl,force (subst_substituted + subst const1))) + | MSEapply (me1,me2) -> + MSEapply (subst_inc_expr subst me1, + subst_inc_expr subst me2) + | _ -> anomaly "You cannot Include a high-order structure" + +let lift_oname (sp,kn) = + let mp,_,_ = Names.repr_kn kn in + let dir,_ = Libnames.repr_path sp in + (dir,mp) + +let cache_include (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + Global.add_include me; + match substituted with + Some seg -> + load_objects 1 prefix seg; + open_objects 1 prefix seg; + | None -> () + +let load_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + load_objects i prefix seg + | None -> () +let open_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + if is_mod then + open_objects i prefix seg + else + if i = 1 then + open_objects i prefix seg + | None -> () +let subst_include (oname,subst,((me,is_mod),substobj,_)) = + let dir,mp1 = lift_oname oname in + let (sub,mbids,msid,objs) = substobj in + let subst' = join sub subst in + let substobjs = (subst',mbids,msid,objs) in + let substituted = subst_substobjs dir mp1 substobjs in + ((subst_inc_expr subst' me,is_mod),substobjs,substituted) + +let classify_include (_,((me,is_mod),substobjs,_)) = + Substitute ((me,is_mod),substobjs,None) + +let (in_include,out_include) = + declare_object {(default_object "INCLUDE") with + cache_function = cache_include; + load_function = load_include; + open_function = open_include; + subst_function = subst_include; + classify_function = classify_include; + export_function = (fun _ -> anomaly "No modules in section!") } + +let rec update_include (sub,mbids,msid,objs) = + let rec replace_include = function + | [] -> [] + | (id,obj)::tail -> + if object_tag obj = "INCLUDE" then + let ((me,is_mod),substobjs,substituted) = out_include obj in + if not (is_mod) then + let substobjs' = update_include substobjs in + (id, in_include ((me,true),substobjs',substituted)):: + (replace_include tail) + else + (id,obj)::(replace_include tail) + else + (id,obj)::(replace_include tail) + in + (sub,mbids,msid,replace_include objs) + + + let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = + let fs = Summary.freeze_summaries () in - let _ = Global.start_module id in + try + let mmp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let mty_entry_o, mty_sub_o = match mty_o with None -> None, None | (Some (mty, true)) -> Some (List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries (interp_modtype (Global.env()) mty)), None | (Some (mty, false)) -> None, Some (List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries (interp_modtype (Global.env()) mty)) in @@ -750,7 +1093,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = None -> None | Some mexpr -> Some (List.fold_right - (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) + (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) arg_entries (interp_modexpr (Global.env()) mexpr)) in @@ -761,22 +1104,75 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let env = Global.env() in let substobjs = match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs mte + | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr | _ -> anomaly "declare_module: No type, no body ..." in + let substobjs = update_include substobjs in + (* Undo the simulated interactive building of the module *) + (* and declare the module as a whole *) Summary.unfreeze_summaries fs; + match entry with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp) } -> + let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let (sub,mbids,msid,objs) = substobjs in + let mp1 = Environ.scrape_alias mp env in + let prefix = dir,(mp1,empty_dirpath) in + let substituted = + match mbids with + | [] -> + Some (subst_objects prefix + (join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs) + | _ -> None in + ignore (add_leaf + id + (in_module_alias (Some ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), + substobjs, substituted))); + mmp + | _ -> + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let (sub,mbids,msid,objs) = substobjs in + let sub' = subst_key (map_msid msid mp) sub in + let substobjs = (join sub sub',mbids,msid,objs) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs, substituted))); + mmp + + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + +let declare_include interp_struct me_ast is_mod = - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let substituted = subst_substobjs dir mp substobjs in - - ignore (add_leaf - id - (in_module (Some (entry, mty_sub_o), substobjs, substituted))) - + let fs = Summary.freeze_summaries () in + try + let env = Global.env() in + let me = interp_struct env me_ast in + let substobjs = + if is_mod then + get_module_substobjs env me + else + get_modtype_substobjs env me in + let mp1,_ = current_prefix () in + let dir = dir_of_sp (Lib.path_of_include()) in + let substituted = subst_substobjs dir mp1 substobjs in + let id = current_mod_id() in + + ignore (add_leaf id + (in_include ((me,is_mod), substobjs, substituted))) + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + (*s Iterators. *) - + let iter_all_segments f = let _ = MPmap.iter diff --git a/library/declaremods.mli b/library/declaremods.mli index 481809fc..9c295451 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.mli 6758 2005-02-20 18:13:28Z herbelin $ i*) +(*i $Id: declaremods.mli 11065 2008-06-06 22:39:43Z msozeau $ i*) (*i*) open Util @@ -37,28 +37,28 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> - 'modexpr option -> unit + 'modexpr option -> module_path -val start_module : (env -> 'modtype -> module_type_entry) -> +val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> - ('modtype * bool) option -> unit + ('modtype * bool) option -> module_path -val end_module : identifier -> unit +val end_module : identifier -> module_path (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_type_entry) -> - identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit +val declare_modtype : (env -> 'modtype -> module_struct_entry) -> + identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path -val start_modtype : (env -> 'modtype -> module_type_entry) -> - identifier -> (identifier located list * 'modtype) list -> unit +val start_modtype : (env -> 'modtype -> module_struct_entry) -> + identifier -> (identifier located list * 'modtype) list -> module_path -val end_modtype : identifier -> unit +val end_modtype : identifier -> module_path (*s Objects of a module. They come in two lists: the substitutive ones @@ -95,6 +95,10 @@ val really_import_module : module_path -> unit val import_module : bool -> module_path -> unit +(* Include *) + +val declare_include : (env -> 'struct_expr -> module_struct_entry) -> + 'struct_expr -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented @@ -110,4 +114,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (* For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * module_type_entry) list -> unit + (mod_bound_id * module_struct_entry) list -> unit + diff --git a/library/decls.ml b/library/decls.ml new file mode 100644 index 00000000..12808310 --- /dev/null +++ b/library/decls.ml @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !vartab); + Summary.unfreeze_function = (fun ft -> vartab := ft); + Summary.init_function = (fun () -> vartab := Idmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_variable_data id o = vartab := Idmap.add id o !vartab + +let variable_path id = let (p,_,_,_) = Idmap.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq +let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k +let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst + +let variable_exists id = Idmap.mem id !vartab + +(** Datas associated to global parameters and constants *) + +let csttab = ref (Cmap.empty : logical_kind Cmap.t) + +let _ = Summary.declare_summary "CONSTANT" + { Summary.freeze_function = (fun () -> !csttab); + Summary.unfreeze_function = (fun ft -> csttab := ft); + Summary.init_function = (fun () -> csttab := Cmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_constant_kind kn k = csttab := Cmap.add kn k !csttab + +let constant_kind kn = Cmap.find kn !csttab + +(** Miscellaneous functions. *) + +let clear_proofs sign = + List.fold_right + (fun (id,c,t as d) signv -> + let d = if variable_opacity id then (id,None,t) else d in + Environ.push_named_context_val d signv) sign Environ.empty_named_context_val + +let last_section_hyps dir = + fold_named_context + (fun (id,_,_) sec_ids -> + try if dir=variable_path id then id::sec_ids else sec_ids + with Not_found -> sec_ids) + (Environ.named_context (Global.env())) + ~init:[] + +let is_section_variable = function + | VarRef _ -> true + | _ -> false diff --git a/library/decls.mli b/library/decls.mli new file mode 100644 index 00000000..39d258b3 --- /dev/null +++ b/library/decls.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* variable_data -> unit +val variable_kind : variable -> logical_kind +val variable_opacity : variable -> bool +val variable_constraints : variable -> Univ.constraints +val variable_exists : variable -> bool + +(** Registration and access to the table of constants *) + +val add_constant_kind : constant -> logical_kind -> unit +val constant_kind : constant -> logical_kind + +(** 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 f515dcb0..c7ccb3ae 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dischargedhypsmap.ml 9903 2007-06-21 17:02:07Z herbelin $ *) +(* $Id: dischargedhypsmap.ml 9902 2007-06-21 17:01:21Z herbelin $ *) open Util open Libnames diff --git a/library/global.ml b/library/global.ml index ab5d8956..b2f9e127 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: global.ml 10664 2008-03-14 11:27:37Z soubiran $ *) open Util open Names @@ -68,11 +68,14 @@ let add_constant = add_thing add_constant let add_mind = add_thing add_mind let add_modtype = add_thing (fun _ -> add_modtype) () let add_module = add_thing (fun _ -> add_module) () +let add_alias = add_thing (fun _ -> add_alias) () let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env +let add_include me = global_env := add_include me !global_env + let start_module id = let l = label_of_id id in let mp,newenv = start_module l !global_env in @@ -151,3 +154,10 @@ let type_of_reference env = function Inductive.type_of_constructor cstr specif let type_of_global t = type_of_reference (env ()) t + + +(* spiwack: register/unregister functions for retroknowledge *) +let register field value by_clause = + let entry = kind_of_term value in + let senv = Safe_typing.register !global_env field entry by_clause in + global_env := senv diff --git a/library/global.mli b/library/global.mli index 96965465..cb717cdf 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli 8723 2006-04-16 15:51:02Z herbelin $ i*) +(*i $Id: global.mli 10664 2008-03-14 11:27:37Z soubiran $ i*) (*i*) open Names @@ -50,7 +50,9 @@ val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name val add_module : identifier -> module_entry -> module_path -val add_modtype : identifier -> module_type_entry -> kernel_name +val add_modtype : identifier -> module_struct_entry -> module_path +val add_include : module_struct_entry -> unit +val add_alias : identifier -> module_path -> module_path val add_constraints : constraints -> unit @@ -64,12 +66,13 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : identifier -> module_path -val end_module : identifier -> module_type_entry option -> module_path +val end_module : identifier -> module_struct_entry option -> module_path -val add_module_parameter : mod_bound_id -> module_type_entry -> unit +val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path -val end_modtype : identifier -> kernel_name +val end_modtype : identifier -> module_path + (* Queries *) @@ -78,7 +81,7 @@ 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 : kernel_name -> module_type_body +val lookup_modtype : module_path -> module_type_body (* Compiled modules *) val start_library : dir_path -> module_path @@ -91,3 +94,6 @@ val import : compiled_library -> Digest.t -> module_path val type_of_global : Libnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env + +(* spiwack: register/unregister function for retroknowledge *) +val register : Retroknowledge.field -> constr -> constr -> unit diff --git a/library/goptions.ml b/library/goptions.ml index 4d36e1c5..a9b33235 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 9060 2006-07-27 15:30:35Z notin $ *) +(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *) (* This module manages customization parameters at the vernacular level *) @@ -25,10 +25,12 @@ open Mod_subst type option_name = | PrimaryTable of string | SecondaryTable of string * string + | TertiaryTable of string * string * string let nickname = function | PrimaryTable s -> s | SecondaryTable (s1,s2) -> s1^" "^s2 + | TertiaryTable (s1,s2,s3) -> s1^" "^s2^" "^s3 let error_undeclared_key key = error ((nickname key)^": no table or option of this type") @@ -206,7 +208,7 @@ module MakeRefTable = functor (A : RefConvertArg) -> MakeTable (RefConvert(A)) (****************************************************************************) -(* 2- Options *) +(* 2- Flags. *) type 'a option_sig = { optsync : bool; diff --git a/library/goptions.mli b/library/goptions.mli index 16744ec4..e076a396 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: goptions.mli 6304 2004-11-16 15:49:08Z sacerdot $ i*) +(*i $Id: goptions.mli 9810 2007-04-29 09:44:58Z herbelin $ i*) (* This module manages customization parameters at the vernacular level *) @@ -68,6 +68,7 @@ open Mod_subst type option_name = | PrimaryTable of string | SecondaryTable of string * string + | TertiaryTable of string * string * string val error_undeclared_key : option_name -> 'a diff --git a/library/heads.ml b/library/heads.ml new file mode 100644 index 00000000..626f1795 --- /dev/null +++ b/library/heads.ml @@ -0,0 +1,190 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* phi(x))] where [g] is [fun f => g O] does not launch + the evaluation of [phi(0)] and the head of [h] is declared unknown). *) + +type rigid_head_kind = +| RigidParameter of constant (* a Const without body *) +| RigidVar of variable (* a Var without body *) +| RigidType (* an inductive, a product or a sort *) + +type head_approximation = +| RigidHead of rigid_head_kind +| ConstructorHead +| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) +| NotImmediatelyComputableHead + +(** Registration as global tables and rollback. *) + +module Evalreford = struct + type t = evaluable_global_reference + let compare = Pervasives.compare +end + +module Evalrefmap = Map.Make(Evalreford) + +let head_map = ref Evalrefmap.empty + +let init () = head_map := Evalrefmap.empty + +let freeze () = !head_map + +let unfreeze hm = head_map := hm + +let _ = + Summary.declare_summary "Head_decl" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = true; + Summary.survive_section = false } + +let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map +let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map + +let kind_of_head env t = + let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with + | Rel n when n > k -> NotImmediatelyComputableHead + | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) + | Var id -> + (try on_subterm k l b (variable_head id) + with Not_found -> + (* a goal variable *) + match pi2 (lookup_named id env) with + | Some c -> aux k l c b + | None -> NotImmediatelyComputableHead) + | Const cst -> on_subterm k l b (constant_head cst) + | Construct _ | CoFix _ -> + if b then NotImmediatelyComputableHead else ConstructorHead + | Sort _ | Ind _ | Prod _ -> RigidHead RigidType + | Cast (c,_,_) -> aux k l c b + | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b + | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b + | LetIn _ -> assert false + | Meta _ | Evar _ -> NotImmediatelyComputableHead + | App (c,al) -> aux k (Array.to_list al @ l) c b + | Case (_,_,c,_) -> aux k [] c true + | Fix ((i,j),_) -> + let n = i.(j) in + try aux k [] (List.nth l n) true + with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true) + and on_subterm k l with_case = function + | FlexibleHead (n,i,q,with_subcase) -> + let m = List.length l in + let k',rest,a = + if n > m then + (* eta-expansion *) + let a = + if i <= m then + (* we pick the head in the existing arguments *) + lift (n-m) (List.nth l (i-1)) + else + (* we pick the head in the added arguments *) + mkRel (n-i+1) in + k+n-m,[],a + else + (* enough arguments to [cst] *) + k,list_skipn n l,List.nth l (i-1) in + let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in + aux k' l' a (with_subcase or with_case) + | ConstructorHead when with_case -> NotImmediatelyComputableHead + | x -> x + in aux 0 [] t false + +let compute_head = function +| EvalConstRef cst -> + (match constant_opt_value (Global.env()) cst with + | None -> RigidHead (RigidParameter cst) + | Some c -> kind_of_head (Global.env()) c) +| EvalVarRef id -> + (match pi2 (Global.lookup_named id) with + | Some c when not (Decls.variable_opacity id) -> + kind_of_head (Global.env()) c + | _ -> + RigidHead (RigidVar id)) + +let is_rigid env t = + match kind_of_head env t with + | RigidHead _ | ConstructorHead -> true + | _ -> false + +(** Registration of heads as an object *) + +let load_head _ (_,(ref,(k:head_approximation))) = + head_map := Evalrefmap.add ref k !head_map + +let cache_head o = + load_head 1 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 + (* A change of the prefix of the constant *) + k + else + (* A substitution of the constant by a functor argument *) + kind_of_head (Global.env()) c + | x -> x + +let subst_head (_,subst,(ref,k)) = + (subst_evaluable_reference subst ref, subst_head_approximation subst k) + +let discharge_head (_,(ref,k)) = + match ref with + | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k) + | EvalVarRef id -> None + +let rebuild_head (info,(ref,k)) = + (ref, compute_head ref) + +let export_head o = Some o + +let (inHead, _) = + declare_object {(default_object "HEAD") with + cache_function = cache_head; + load_function = load_head; + subst_function = subst_head; + classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_head; + rebuild_function = rebuild_head; + export_function = export_head } + +let declare_head c = + let hd = compute_head c in + add_anonymous_leaf (inHead (c,hd)) + +(** Printing *) + +let pr_head = function +| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst +| RigidHead (RigidType) -> str "rigid type" +| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id +| ConstructorHead -> str "constructor" +| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt()) +| NotImmediatelyComputableHead -> str "unknown" + + diff --git a/library/heads.mli b/library/heads.mli new file mode 100644 index 00000000..52270b49 --- /dev/null +++ b/library/heads.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(* [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 8cea4737..cae1986e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 9488 2007-01-17 11:11:58Z herbelin $ *) +(* $Id: impargs.ml 10796 2008-04-15 12:00:50Z herbelin $ *) open Util open Names @@ -25,49 +25,67 @@ open Topconstr (*s Flags governing the computation of implicit arguments *) +type implicits_flags = { + main : bool; + strict : bool; (* true = strict *) + strongly_strict : bool; (* true = strongly strict *) + reversible_pattern : bool; + contextual : bool; (* true = contextual *) + maximal : bool +} + (* les implicites sont stricts par défaut en v8 *) -let implicit_args = ref false -let strict_implicit_args = ref true -let contextual_implicit_args = ref false + +let implicit_args = ref { + main = false; + strict = true; + strongly_strict = false; + reversible_pattern = false; + contextual = false; + maximal = false; +} let make_implicit_args flag = - implicit_args := flag + implicit_args := { !implicit_args with main = flag } let make_strict_implicit_args flag = - strict_implicit_args := flag + implicit_args := { !implicit_args with strict = flag } -let make_contextual_implicit_args flag = - contextual_implicit_args := flag +let make_strongly_strict_implicit_args flag = + implicit_args := { !implicit_args with strongly_strict = flag } + +let make_reversible_pattern_implicit_args flag = + implicit_args := { !implicit_args with reversible_pattern = flag } -let is_implicit_args () = !implicit_args -let is_strict_implicit_args () = !strict_implicit_args -let is_contextual_implicit_args () = !contextual_implicit_args +let make_contextual_implicit_args flag = + implicit_args := { !implicit_args with contextual = flag } -type implicits_flags = bool * bool * bool +let make_maximal_implicit_args flag = + implicit_args := { !implicit_args with maximal = flag } -let implicit_flags () = - (!implicit_args, !strict_implicit_args, !contextual_implicit_args) +let is_implicit_args () = !implicit_args.main +let is_strict_implicit_args () = !implicit_args.strict +let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict +let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern +let is_contextual_implicit_args () = !implicit_args.contextual +let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits (a,b,c) f x = - let oa = !implicit_args in - let ob = !strict_implicit_args in - let oc = !contextual_implicit_args in +let with_implicits flags f x = + let oflags = !implicit_args in try - implicit_args := a; - strict_implicit_args := b; - contextual_implicit_args := c; - let rslt = f x in - implicit_args := oa; - strict_implicit_args := ob; - contextual_implicit_args := oc; + implicit_args := flags; + let rslt = f x in + implicit_args := oflags; rslt with e -> begin - implicit_args := oa; - strict_implicit_args := ob; - contextual_implicit_args := oc; + implicit_args := oflags; raise e end +let set_maximality imps b = + (* Force maximal insertion on ending implicits (compatibility) *) + b || List.for_all ((<>) None) imps + (*s Computation of implicit arguments *) (* We remember various information about why an argument is (automatically) @@ -99,7 +117,7 @@ type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position - | Manual + | Manual of bool let argument_less = function | Hyp n, Hyp n' -> n if argument_less (pos,fpos) or pos=fpos then DepRigid pos else DepFlexAndRigid (fpos,pos) - | Some Manual -> assert false + | Some (Manual _) -> assert false else match st with | None -> DepFlex pos @@ -129,7 +147,7 @@ let update pos rig (na,st) = if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x | Some (DepFlex fpos as x) -> if argument_less (pos,fpos) then DepFlex pos else x - | Some Manual -> assert false + | Some (Manual _) -> assert false in na, Some e (* modified is_rigid_reference with a truncated env *) @@ -148,18 +166,30 @@ let is_flexible_reference env bound depth f = let push_lift d (e,n) = (push_rel d e,n+1) +let is_reversible_pattern bound depth f l = + isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & + array_for_all (fun c -> isRel c & destRel c < depth) l & + array_distinct l + (* Precondition: rels in env are for inductive types only *) -let add_free_rels_until strict bound env m pos acc = +let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let rec frec rig (env,depth as ed) c = - match kind_of_term (whd_betadeltaiota env c) with + let hd = if strict then whd_betadeltaiota env c else c in + let c = if strongly_strict then hd else c in + match kind_of_term hd with | Rel n when (n < bound+depth) & (n >= depth) -> - acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1)) + let i = bound + depth - n - 1 in + acc.(i) <- update pos rig acc.(i) + | App (f,l) when revpat & is_reversible_pattern bound depth f l -> + let i = bound + depth - destRel f - 1 in + acc.(i) <- update pos rig acc.(i) | App (f,_) when rig & is_flexible_reference env bound depth f -> if strict then () else iter_constr_with_full_binders push_lift (frec false) ed c | Case _ when rig -> if strict then () else iter_constr_with_full_binders push_lift (frec false) ed c + | Evar _ -> () | _ -> iter_constr_with_full_binders push_lift (frec rig) ed c in @@ -167,74 +197,127 @@ let add_free_rels_until strict bound env m pos acc = (* calcule la liste des arguments implicites *) -let compute_implicits_gen strict contextual env t = +let concrete_name avoid_flags l env_names n all c = + if n = Anonymous & noccurn 1 c then + (Anonymous,l) + else + let fresh_id = next_name_not_occuring avoid_flags n l env_names c in + let idopt = if not all && noccurn 1 c then Anonymous else Name fresh_id in + (idopt, fresh_id::l) + +let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> - let na',avoid' = Termops.concrete_name false avoid names na b in - add_free_rels_until strict n env a (Hyp (n+1)) + let na',avoid' = concrete_name None avoid names na all b in + add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) | _ -> let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in - if contextual then add_free_rels_until strict n env t Conclusion v + if contextual then + add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v in match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> - let na',avoid = Termops.concrete_name false [] [] na b in + let na',avoid = concrete_name None [] [] na all b in let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in Array.to_list v | _ -> [] -let compute_implicits_auto env (_,strict,contextual) t = - let l = compute_implicits_gen strict contextual env t in - List.map (function - | (Name id, Some imp) -> Some (id,imp) - | (Anonymous, Some _) -> anomaly "Unnamed implicit" - | _ -> None) l - -let compute_implicits env t = compute_implicits_auto env (implicit_flags()) t - -let set_implicit id imp = - Some (id,match imp with None -> Manual | Some imp -> imp) - -let compute_manual_implicits flags ref l = - let t = Global.type_of_global ref in - let autoimps = compute_implicits_gen false true (Global.env()) t in +let rec prepare_implicits f = function + | [] -> [] + | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit" + | (Name id, Some imp)::imps -> + let imps' = prepare_implicits f imps in + Some (id,imp,set_maximality imps' f.maximal) :: imps' + | _::imps -> None :: prepare_implicits f imps + +let compute_implicits_flags env f all t = + compute_implicits_gen + (f.strict or f.strongly_strict) f.strongly_strict + f.reversible_pattern f.contextual all env t + +let set_implicit id imp insmax = + (id,(match imp with None -> Manual false | Some imp -> imp),insmax) + +let merge_imps f = function + None -> Some (Manual f) + | x -> x + +let rec assoc_by_pos k = function + (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl + | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl + | [] -> raise Not_found + +let compute_manual_implicits env flags t enriching l = + let autoimps = + if enriching then compute_implicits_flags env flags true t + else compute_implicits_gen false false false true true env t in let n = List.length autoimps in + let try_forced k l = + try + let (id, (b, f)), l' = assoc_by_pos k l in + if f then + let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in + l', Some (id,Manual f,b) + else l, None + with Not_found -> l, None + in if not (list_distinct l) then error ("Some parameters are referred more than once"); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp = - try list_remove_first (ExplByPos k) l, set_implicit id imp - with Not_found -> - try list_remove_first (ExplByName id) l, set_implicit id imp - with Not_found -> - l, None in - imp :: merge (k+1) l' imps - | (Anonymous,imp)::imps -> - None :: merge (k+1) l imps - | [] when l = [] -> [] - | _ -> - match List.hd l with - | ExplByName id -> - error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) - | ExplByPos i -> + | (Name id,imp)::imps -> + let l',imp,m = + try + let (b, f) = List.assoc (ExplByName id) l in + List.remove_assoc (ExplByName id) l, merge_imps f imp,Some b + with Not_found -> + try + let (id, (b, f)), l' = assoc_by_pos k l in + l', merge_imps f imp,Some b + with Not_found -> + l,imp, if enriching && imp <> None then Some flags.maximal else None + in + let imps' = merge (k+1) l' imps in + let m = Option.map (set_maximality imps') m in + Option.map (set_implicit id imp) m :: imps' + | (Anonymous,imp)::imps -> + let l', forced = try_forced k l in + forced :: merge (k+1) l' imps + | [] when l = [] -> [] + | [] -> + List.iter (function + | ExplByName id,(b,forced) -> + if not forced then + error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) + | ExplByPos (i,_id),_t -> if i<1 or i>n then error ("Bad implicit argument number: "^(string_of_int i)) else errorlabstrm "" (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name") in + str ": it has no name")) + l; [] + in merge 1 l autoimps +let compute_implicits_auto env f manual t = + match manual with + [] -> let l = compute_implicits_flags env f false t in + prepare_implicits f l + | _ -> compute_manual_implicits env f t true manual + +let compute_implicits env t = compute_implicits_auto env !implicit_args [] t + +type maximal_insertion = bool (* true = maximal contextual insertion *) + type implicit_status = (* None = Not implicit *) - (identifier * implicit_explanation) option + (identifier * implicit_explanation * maximal_insertion) option type implicits_list = implicit_status list @@ -244,18 +327,26 @@ let is_status_implicit = function let name_of_implicit = function | None -> anomaly "Not an implicit argument" - | Some (id,_) -> id + | Some (id,_,_) -> id -(* [in_ctx] means we now the expected type, [n] is the index of the argument *) +let maximal_insertion_of = function + | Some (_,_,b) -> b + | None -> anomaly "Not an implicit argument" + +let forced_implicit = function + | Some (_,Manual b,_) -> b + | _ -> false + +(* [in_ctx] means we know the expected type, [n] is the index of the argument *) let is_inferable_implicit in_ctx n = function | None -> false - | Some (_,DepRigid (Hyp p)) -> n >= p - | Some (_,DepFlex (Hyp p)) -> false - | Some (_,DepFlexAndRigid (_,Hyp q)) -> n >= q - | Some (_,DepRigid Conclusion) -> in_ctx - | Some (_,DepFlex Conclusion) -> false - | Some (_,DepFlexAndRigid (_,Conclusion)) -> false - | Some (_,Manual) -> true + | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p + | Some (_,DepFlex (Hyp p),_) -> false + | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q + | Some (_,DepRigid Conclusion,_) -> in_ctx + | Some (_,DepFlex Conclusion,_) -> false + | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx + | Some (_,Manual _,_) -> true let positions_of_implicits = let rec aux n = function @@ -264,21 +355,18 @@ let positions_of_implicits = | None :: l -> aux (n+1) l in aux 1 -type strict_flag = bool (* true = strict *) -type contextual_flag = bool (* true = contextual *) - (*s Constants. *) -let compute_constant_implicits flags cst = +let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_implicits_auto env flags (Typeops.type_of_constant env cst) + compute_implicits_auto env flags manual (Typeops.type_of_constant env cst) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let compute_mib_implicits flags kn = +let compute_mib_implicits flags manual kn = let env = Global.env () in let mib = lookup_mind kn env in let ar = @@ -291,41 +379,56 @@ let compute_mib_implicits flags kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,compute_implicits_auto env flags ar), + ((IndRef ind,compute_implicits_auto env flags manual ar), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c)) + (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets -let compute_all_mib_implicits flags kn = - let imps = compute_mib_implicits flags kn in +let compute_all_mib_implicits flags manual kn = + let imps = compute_mib_implicits flags manual kn in List.flatten (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let compute_var_implicits flags id = +let compute_var_implicits flags manual id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - compute_implicits_auto env flags ty + compute_implicits_auto env flags manual ty (* Implicits of a global reference. *) -let compute_global_implicits flags = function - | VarRef id -> compute_var_implicits flags id - | ConstRef kn -> compute_constant_implicits flags kn +let compute_global_implicits flags manual = function + | VarRef id -> compute_var_implicits flags manual id + | ConstRef kn -> compute_constant_implicits flags manual kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) + +(* Merge a manual explicitation with an implicit_status list *) + +let list_split_at index l = + let rec aux i acc = function + tl when i = index -> (List.rev acc), tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_at: Invalid argument" + in aux 0 [] l + +let merge_impls oimpls impls = + let oimpls, _ = list_split_at (List.length oimpls - List.length impls) oimpls in + oimpls @ impls (* Caching implicits *) -type implicit_interactive_request = ImplAuto | ImplManual of explicitation list +type implicit_interactive_request = + | ImplAuto + | ImplManual of implicit_status list type implicit_discharge_request = - | ImplNoDischarge + | ImplLocal | ImplConstant of constant * implicits_flags | ImplMutualInductive of kernel_name * implicits_flags | ImplInteractive of global_reference * implicits_flags * @@ -348,11 +451,11 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (_,subst,(req,l)) = - (ImplNoDischarge,list_smartmap (subst_implicits_decl subst) l) + (ImplLocal,list_smartmap (subst_implicits_decl subst) l) let discharge_implicits (_,(req,l)) = match req with - | ImplNoDischarge -> None + | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> Some (ImplInteractive (pop_global_reference ref,flags,exp),l) | ImplConstant (con,flags) -> @@ -360,20 +463,28 @@ let discharge_implicits (_,(req,l)) = | ImplMutualInductive (kn,flags) -> Some (ImplMutualInductive (pop_kn kn,flags),l) -let rebuild_implicits (req,l) = +let rebuild_implicits (info,(req,l)) = + let manual = List.fold_left (fun acc (id, impl, keep) -> + if impl then (ExplByName id, (true, true)) :: acc else acc) + [] info + in let l' = match req with - | ImplNoDischarge -> assert false + | ImplLocal -> assert false | ImplConstant (con,flags) -> - [ConstRef con,compute_constant_implicits flags con] + [ConstRef con, compute_constant_implicits flags manual con] | ImplMutualInductive (kn,flags) -> - compute_all_mib_implicits flags kn + compute_all_mib_implicits flags manual kn | ImplInteractive (ref,flags,o) -> match o with - | ImplAuto -> [ref,compute_global_implicits flags ref] - | ImplManual l -> - error "Discharge of global manually given implicit arguments not implemented" in - (req,l') + | ImplAuto -> [ref,compute_global_implicits flags manual ref] + | ImplManual l -> + let auto = compute_global_implicits flags manual ref in +(* let auto = if flags.main then auto else List.map (fun _ -> None) auto in *) + let l' = merge_impls auto l in [ref,l'] + in (req,l') +let export_implicits (req,_ as x) = + if req = ImplLocal then None else Some x let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with @@ -383,46 +494,56 @@ let (inImplicits, _) = classify_function = (fun (_,x) -> Substitute x); discharge_function = discharge_implicits; rebuild_function = rebuild_implicits; - export_function = (fun x -> Some x) } + export_function = export_implicits } let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags ref in + let imps = compute_global_implicits flags [] ref in add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = - let flags = (true,!strict_implicit_args,!contextual_implicit_args) in + let flags = { !implicit_args with main = true } in let req = - if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in + if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in declare_implicits_gen req flags ref let declare_var_implicits id = - if !implicit_args then - declare_implicits_gen ImplNoDischarge (implicit_flags ()) (VarRef id) + if !implicit_args.main then + declare_implicits_gen ImplLocal !implicit_args (VarRef id) let declare_constant_implicits con = - if !implicit_args then - let flags = implicit_flags () in + if !implicit_args.main then + let flags = !implicit_args in declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) let declare_mib_implicits kn = - if !implicit_args then - let flags = implicit_flags () in + if !implicit_args.main then + let flags = !implicit_args in let imps = array_map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags kn) in + (compute_mib_implicits flags [] kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) +type manual_explicitation = Topconstr.explicitation * (bool * bool) + +let compute_implicits_with_manual env typ enriching l = + compute_manual_implicits env !implicit_args typ enriching l -let declare_manual_implicits local ref l = - let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in - let l' = compute_manual_implicits flags ref l in +let declare_manual_implicits local ref enriching l = + let flags = !implicit_args in + let env = Global.env () in + let t = Global.type_of_global ref in + let l' = compute_manual_implicits env flags t enriching l in let req = - if local or isVarRef ref then ImplNoDischarge - else ImplInteractive(ref,flags,ImplManual l) + if local or isVarRef ref then ImplLocal + else ImplInteractive(ref,flags,ImplManual l') in - add_anonymous_leaf (inImplicits (req,[ref,l'])) + add_anonymous_leaf (inImplicits (req,[ref,l'])) + +let maybe_declare_manual_implicits local ref enriching l = + if l = [] then () + else declare_manual_implicits local ref enriching l (*s Registration as global tables *) diff --git a/library/impargs.mli b/library/impargs.mli index 64ce0360..5b55af82 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) +(*i $Id: impargs.mli 10741 2008-04-02 15:47:07Z msozeau $ i*) (*i*) open Names @@ -21,11 +21,17 @@ open Nametab val make_implicit_args : bool -> unit val make_strict_implicit_args : bool -> unit +val make_strongly_strict_implicit_args : bool -> unit +val make_reversible_pattern_implicit_args : bool -> unit val make_contextual_implicit_args : bool -> unit +val make_maximal_implicit_args : bool -> unit val is_implicit_args : unit -> bool val is_strict_implicit_args : unit -> bool +val is_strongly_strict_implicit_args : unit -> bool +val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool +val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b @@ -35,9 +41,13 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b type implicit_status type implicits_list = implicit_status list +type implicit_explanation + val is_status_implicit : implicit_status -> bool val is_inferable_implicit : bool -> int -> implicit_status -> bool val name_of_implicit : implicit_status -> identifier +val maximal_insertion_of : implicit_status -> bool +val forced_implicit : implicit_status -> bool val positions_of_implicits : implicits_list -> int list @@ -45,6 +55,13 @@ val positions_of_implicits : implicits_list -> int list for an object of the given type in the given env *) val compute_implicits : env -> types -> implicits_list +(* A [manual_explicitation] is a tuple of a positional or named explicitation with + maximal insertion and forcing flags. *) +type manual_explicitation = Topconstr.explicitation * (bool * bool) + +val compute_implicits_with_manual : env -> types -> bool -> + manual_explicitation list -> implicits_list + (*s Computation of implicits (done using the global environment). *) val declare_var_implicits : variable -> unit @@ -53,8 +70,16 @@ val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : bool -> global_reference -> unit -(* Manual declaration of which arguments are expected implicit *) -val declare_manual_implicits : bool -> global_reference -> - Topconstr.explicitation list -> unit +(* [declare_manual_implicits local ref enriching l] + Manual declaration of which arguments are expected implicit. + Unsets implicits if [l] is empty. *) + +val declare_manual_implicits : bool -> global_reference -> bool -> + manual_explicitation list -> unit + +(* If the list is empty, do nothing, otherwise declare the implicits. *) + +val maybe_declare_manual_implicits : bool -> global_reference -> bool -> + manual_explicitation list -> unit val implicits_of_global : global_reference -> implicits_list diff --git a/library/lib.ml b/library/lib.ml index 4a4e90c1..ce3d2520 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 10269 2007-10-29 11:09:43Z notin $ *) +(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *) open Pp open Util @@ -22,9 +22,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of bool option * 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 + | ClosedSection of library_segment | FrozenState of Summary.frozen and library_entry = object_name * node @@ -60,7 +62,11 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (oname,ClosedSection) :: stk -> clean acc stk + | (_,ClosedSection _) :: stk -> clean acc stk + (* 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" @@ -92,11 +98,15 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix - let cwd () = fst !path_prefix let make_path id = Libnames.make_path (cwd ()) id +let path_of_include () = + let dir = Names.repr_dirpath (cwd ()) in + let new_dir = List.tl dir in + let id = List.hd dir in + Libnames.make_path (Names.make_dirpath new_dir) id let current_prefix () = snd !path_prefix @@ -150,18 +160,32 @@ let find_split_p p = in find !lib_stk -let split_lib sp = +let split_lib_gen test = let rec collect after equal = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after (hd::equal) before else after,equal,hd::before - | [] -> after,equal,[] + | hd::strict_before as before -> + if test hd then collect after (hd::equal) strict_before else after,equal,before + | [] as before -> after,equal,before in let rec findeq after = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after [hd] before else findeq (hd::after) before - | [] -> error "no such entry" - in - findeq [] !lib_stk + | hd :: before -> + if test hd + 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 + | Some (sub_after,sub_equal,sub_before) -> + Some (sub_after, sub_equal, (List.append sub_before before))) + | _ -> findeq (hd::after) before) + | [] -> None + in + match findeq [] !lib_stk with + | None -> error "no such entry" + | Some r -> r + +let split_lib sp = split_lib_gen (fun x -> (fst x) = sp) (* Adding operations. *) @@ -190,9 +214,9 @@ let add_leaf id obj = add_entry oname (Leaf obj); oname -let add_discharged_leaf id obj = +let add_discharged_leaf id varinfo obj = let oname = make_oname id in - let newobj = rebuild_object obj in + let newobj = rebuild_object (varinfo, obj) in cache_object (oname,newobj); add_entry oname (Leaf newobj) @@ -216,12 +240,25 @@ let add_frozen_state () = (* Modules. *) + let is_something_opened = function (_,OpenedSection _) -> true | (_,OpenedModule _) -> true | (_,OpenedModtype _) -> true | _ -> false + +let current_mod_id () = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,_,nametab) -> + basename (fst oname) + | oname,OpenedModtype (_,nametab) -> + basename (fst oname) + | _ -> error "you are not in a module" + with Not_found -> + error "no opened modules" + + let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in let prefix = dir,(mp,empty_dirpath) in @@ -253,9 +290,15 @@ let end_module id = with Not_found -> error "no opened modules" in - let (after,_,before) = split_lib oname in + let (after,modopening,before) = split_lib oname in lib_stk := before; + add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening))); 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 *) @@ -292,8 +335,9 @@ let end_modtype id = with Not_found -> error "no opened module types" in - let (after,_,before) = split_lib sp in + let (after,modtypeopening,before) = split_lib sp in lib_stk := before; + add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening))); let dir = !path_prefix in recalc_path_prefix (); (* add_frozen_state must be called after processing the module type. @@ -396,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t let sectab = - ref ([] : (identifier list * Cooking.work_list * abstr_list) list) + ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab -let add_section_variable id = +let add_section_variable id impl keep = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl + | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl let rec extract_hyps = function - | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps) | (id::idl,hyps) -> extract_hyps (idl,hyps) | [], _ -> [] @@ -429,6 +474,8 @@ 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 = Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -442,15 +489,15 @@ let section_instance = function | IndRef (kn,_) | ConstructRef ((kn,_),_) -> KNmap.find kn (snd (pi2 (List.hd !sectab))) -let init () = sectab := [] -let freeze () = !sectab -let unfreeze s = sectab := s +let init_sectab () = sectab := [] +let freeze_sectab () = !sectab +let unfreeze_sectab s = sectab := s let _ = Summary.declare_summary "section-context" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; + { Summary.freeze_function = freeze_sectab; + Summary.unfreeze_function = unfreeze_sectab; + Summary.init_function = init_sectab; Summary.survive_module = false; Summary.survive_section = false } @@ -476,7 +523,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; - if !Options.xml_export then !xml_open_section id; + if !Flags.xml_export then !xml_open_section id; add_section () @@ -486,9 +533,9 @@ let open_section id = let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> - option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None - | ClosedSection -> None + | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" @@ -504,21 +551,29 @@ let close_section id = with Not_found -> error "no opened section" in - let (secdecls,_,before) = split_lib oname in + let var_info = List.map + (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false)) + (variables_context ()) + in + let (secdecls,secopening,before) = split_lib oname in lib_stk := before; let full_olddir = fst !path_prefix in pop_path_prefix (); - add_entry (make_oname id) ClosedSection; - if !Options.xml_export then !xml_close_section id; + add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening))); + if !Flags.xml_export then !xml_close_section id; let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; - List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) +let (inLabel,outLabel) = + declare_object {(default_object "DOT") with + classify_function = (fun _ -> Dispose)} + let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) | (_,OpenedSection _) -> add_section () @@ -529,16 +584,58 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let reset_to sp = - let (_,_,before) = split_lib sp in - lib_stk := before; +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 (); let spf = match find_entry_p is_frozen_state with | (sp, FrozenState f) -> unfreeze_summaries f; sp | _ -> assert false in let (after,_,_) = split_lib spf in - recache_context after + try + recache_context after + with + | Not_found -> error "Tried to set environment to an incoherent state." + +let reset_to_gen test = + let (_,_,before) = split_lib_gen test in + set_lib_stk before + +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; 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) + *) +let delete_gen test = + let (after,equal,before) = split_lib_gen test in + let rec chop_at_dot = function + | [] as l -> l + | (_, Leaf o)::t when object_tag o = "DOT" -> t + | _::t -> chop_at_dot t + and chop_before_dot = function + | [] as l -> l + | (_, Leaf o)::t as l when object_tag o = "DOT" -> l + | _::t -> chop_before_dot t + in + set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before)) + +let delete sp = delete_gen (fun x -> (fst x) = sp) let reset_name (loc,id) = let (sp,_) = @@ -549,10 +646,20 @@ let reset_name (loc,id) = in reset_to sp +let remove_name (loc,id) = + let (sp,_) = + try + find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) + with Not_found -> + user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry") + in + delete sp + let is_mod_node = function | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedSection -> true - | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true + | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + || t = "MODULE ALIAS" | _ -> false (* Reset on a module or section name in order to bypass constants with @@ -567,19 +674,7 @@ let reset_mod (loc,id) = with Not_found -> user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry") in - lib_stk := before; - recalc_path_prefix (); - let spf = match find_entry_p is_frozen_state with - | (sp, FrozenState f) -> unfreeze_summaries f; sp - | _ -> assert false - in - let (after,_,_) = split_lib spf in - recache_context after - - -let (inLabel,outLabel) = - declare_object {(default_object "DOT") with - classify_function = (fun _ -> Dispose)} + set_lib_stk before let mark_end_of_command, current_command_label, set_command_label = let n = ref 0 in @@ -590,17 +685,23 @@ let mark_end_of_command, current_command_label, set_command_label = (fun () -> !n), (fun x -> n:=x) -let rec reset_label_stk n stk = - match stk with - (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp - | _::tail -> reset_label_stk n tail - | [] -> error "Unknown state number" +let is_label_n n x = + match x with + | (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. *) let reset_label n = - let res = reset_label_stk n !lib_stk in - set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) - reset_to res - + 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)) + let rec back_stk n stk = match stk with (sp,Leaf o)::tail when object_tag o = "DOT" -> @@ -688,6 +789,14 @@ let remove_section_part ref = (************************) (* Discharging names *) +let pop_kn kn = + let (mp,dir,l) = Names.repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_con con = + let (mp,dir,l) = Names.repr_con con in + Names.make_con mp (dirpath_prefix dir) l + let con_defined_in_sec kn = let _,dir,_ = repr_con kn in dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) diff --git a/library/lib.mli b/library/lib.mli index ec896de5..64074cfd 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) +(*i $Id: lib.mli 11046 2008-06-03 22:48:06Z msozeau $ i*) (*i*) open Util @@ -25,9 +25,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of bool option * 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 + | ClosedSection of library_segment | FrozenState of Summary.frozen and library_segment = (object_name * node) list @@ -65,8 +67,14 @@ val add_anonymous_leaf : obj -> unit val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit + +(* 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 *) 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. *) val reset_label : int -> unit (*s The function [contents_after] returns the current library segment, @@ -80,6 +88,7 @@ val contents_after : object_name option -> library_segment (* User-side names *) val cwd : unit -> dir_path val make_path : identifier -> section_path +val path_of_include : unit -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path @@ -93,7 +102,7 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool - +val current_mod_id : unit -> module_ident (* Returns the most recent OpenedThing node *) val what_is_opened : unit -> object_name * node @@ -122,6 +131,7 @@ val end_compilation : dir_path -> object_prefix * library_segment val library_dp : unit -> dir_path (* Extract the library part of a name even if in a section *) +val dp_of_mp : module_path -> dir_path val library_part : global_reference -> dir_path val remove_section_part : global_reference -> dir_path @@ -134,7 +144,11 @@ val close_section : identifier -> unit val reset_to : object_name -> unit val reset_name : identifier located -> unit +val remove_name : identifier located -> unit val reset_mod : identifier located -> unit +val reset_to_state : object_name -> unit + +val has_top_frozen_state : unit -> object_name option (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) @@ -165,7 +179,7 @@ val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context val section_instance : global_reference -> identifier array -val add_section_variable : identifier -> unit +val add_section_variable : identifier -> bool -> Term.types option -> unit val add_section_constant : constant -> Sign.named_context -> unit val add_section_kn : kernel_name -> Sign.named_context -> unit val replacement_context : unit -> diff --git a/library/libnames.ml b/library/libnames.ml index 07c9ad23..31822da4 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 9488 2007-01-17 11:11:58Z herbelin $ i*) +(*i $Id: libnames.ml 10580 2008-02-22 13:39:13Z lmamane $ i*) open Pp open Util @@ -15,6 +15,7 @@ open Nameops open Term open Mod_subst +(*s Global reference is a kernel side type for all references together *) type global_reference = | VarRef of variable | ConstRef of constant diff --git a/library/libnames.mli b/library/libnames.mli index 9bf6918e..d4942061 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) +(*i $Id: libnames.mli 10308 2007-11-09 09:40:21Z herbelin $ i*) (*i*) open Pp diff --git a/library/libobject.ml b/library/libobject.ml index eaaa1be1..ff78f527 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 9488 2007-01-17 11:11:58Z herbelin $ *) +(* $Id: libobject.ml 10741 2008-04-02 15:47:07Z msozeau $ *) open Util open Names @@ -28,6 +28,7 @@ let relax b = relax_flag := b;; type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +type discharge_info = (identifier * bool * bool) list type 'a object_declaration = { object_name : string; @@ -37,7 +38,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : 'a -> 'a; + rebuild_function : discharge_info * 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -51,7 +52,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); discharge_function = (fun _ -> None); - rebuild_function = (fun x -> x); + rebuild_function = (fun (_,x) -> x); export_function = (fun _ -> None)} @@ -77,7 +78,7 @@ type dynamic_object_declaration = { dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; - dyn_rebuild_function : obj -> obj; + dyn_rebuild_function : discharge_info * obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -112,15 +113,15 @@ let declare_object odecl = anomaly "somehow we got the wrong dynamic object in the classifyfun" and discharge (oname,lobj) = if Dyn.tag lobj = na then - option_map infun (odecl.discharge_function (oname,outfun lobj)) + Option.map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" - and rebuild lobj = - if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) + and rebuild (varinfo,lobj) = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then - option_map infun (odecl.export_function (outfun lobj)) + Option.map infun (odecl.export_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the exportfun" @@ -173,8 +174,8 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj -let rebuild_object lobj = - apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj +let rebuild_object ((_,lobj) as node) = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 376da1f5..5f6cf13b 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) +(*i $Id: libobject.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) (*i*) open Names @@ -51,6 +51,14 @@ open Mod_subst this function should be declared for substitutive objects only (see obove) + * a discharge function, that is applied at section closing time to + collect the data necessary to rebuild the discharged form of the + non volatile objects + + * a rebuild function, that is applied after section closing to + rebuild the non volatile content of a section from the data + collected by the discharge function + * an export function, to enable optional writing of its contents to disk (.vo). This function is also the oportunity to remove redundant information in order to keep .vo size small @@ -63,6 +71,8 @@ open Mod_subst type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +type discharge_info = (identifier * bool * bool) list + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; @@ -71,7 +81,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : 'a -> 'a; + rebuild_function : discharge_info * 'a -> 'a; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -106,5 +116,5 @@ val subst_object : object_name * substitution * obj -> obj val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option val discharge_object : object_name * obj -> obj option -val rebuild_object : obj -> obj +val rebuild_object : discharge_info * obj -> obj val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index 3a3328ad..2904edc2 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 9525 2007-01-24 08:43:01Z herbelin $ *) +(* $Id: library.ml 11181 2008-06-27 07:35:45Z notin $ *) open Pp open Util @@ -86,10 +86,10 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then - (Options.if_verbose warning (phys_path^" was previously bound to " - ^(string_of_dirpath dir) - ^("\nIt is remapped to "^(string_of_dirpath coq_path))); - flush_all ()); + Flags.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); remove_load_path phys_path; load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end @@ -122,7 +122,6 @@ type library_disk = { type library_t = { library_name : compilation_unit_name; - library_filename : System.physical_path; library_compiled : compiled_library; library_objects : library_objects; library_deps : (compilation_unit_name * Digest.t) list; @@ -138,10 +137,15 @@ module LibraryOrdered = end module LibraryMap = Map.Make(LibraryOrdered) +module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) let libraries_table = ref LibraryMap.empty +(* This is the map of loaded libraries filename *) +(* (not synchronized so as not to be caught in the states on disk) *) +let libraries_filename_table = ref LibraryFilenameMap.empty + (* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = ref [] let libraries_imports_list = ref [] @@ -183,7 +187,15 @@ let try_find_library dir = with Not_found -> error ("Unknown library " ^ (string_of_dirpath dir)) -let library_full_filename dir = (find_library dir).library_filename +let register_library_filename dir f = + (* Not synchronized: overwrite the previous binding if one existed *) + (* from a previous play of the session *) + libraries_filename_table := + LibraryFilenameMap.add dir f !libraries_filename_table + +let library_full_filename dir = + try LibraryFilenameMap.find dir !libraries_filename_table + with Not_found -> "" let library_is_loaded dir = try let _ = find_library dir in true @@ -300,7 +312,7 @@ let (in_import, out_import) = (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number = 080992 (* V8.1 beta2 *) +let vo_magic_number = 08193 (* v8.2beta3 *) let (raw_extern_library, raw_intern_library) = System.raw_extern_intern vo_magic_number ".vo" @@ -309,7 +321,7 @@ let with_magic_number_check f a = try f a with System.Bad_magic_number fname -> errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ + (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++ spc () ++ str"It is corrupted" ++ spc () ++ str"or was compiled with another version of Coq.") @@ -331,9 +343,9 @@ let locate_absolute_library dir = (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) - try + if library_is_loaded dir then (dir, library_full_filename dir) - with Not_found -> + else raise LibNotFound let locate_qualified_library qid = @@ -351,10 +363,9 @@ let locate_qualified_library qid = let path, file = System.where_in_path loadpath name in let dir = extend_dirpath (find_logical_path path) base in (* Look if loaded *) - try - (LibLoaded, dir, library_full_filename dir) - with Not_found -> - (LibInPath, dir, file) + if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) + (* Otherwise, look for it in the file system *) + else (LibInPath, dir, file) with Not_found -> raise LibNotFound let explain_locate_library_error qid = function @@ -386,11 +397,10 @@ let try_locate_qualified_library (loc,qid) = (* Internalise libraries *) let lighten_library m = - if !Options.dont_load_proofs then lighten_library m else m + if !Flags.dont_load_proofs then lighten_library m else m -let mk_library md f digest = { +let mk_library md digest = { library_name = md.md_name; - library_filename = f; library_compiled = lighten_library md.md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; @@ -402,7 +412,8 @@ let intern_from_file f = let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; - mk_library md f digest + register_library_filename md.md_name f; + mk_library md digest let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -426,9 +437,9 @@ and intern_library_deps needed dir m = and intern_mandatory_library caller needed (dir,d) = let m,needed = intern_library needed (try_locate_absolute_library dir) in if d <> m.library_digest then - error ("compiled library "^(string_of_dirpath caller)^ - " makes inconsistent assumptions over library " - ^(string_of_dirpath dir)); + errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^ + ".vo makes inconsistent assumptions over library " + ^(string_of_dirpath dir))); needed let rec_intern_library needed mref = @@ -443,17 +454,18 @@ let check_library_short_name f dir = function | _ -> () let rec_intern_by_filename_only id f = - let m = intern_from_file f in + let m = try intern_from_file f with Sys_error s -> error s in (* Only the base name is expected to match *) check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) - try - let m' = find_library m.library_name in - Options.if_verbose warning - ((string_of_dirpath m.library_name)^" is already loaded from file "^ - m'.library_filename); - m.library_name, [] - with Not_found -> + 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); + m.library_name, [] + end + else let needed = intern_library_deps [] m.library_name m in m.library_name, needed @@ -496,7 +508,7 @@ let register_library (dir,m) = (* [needed] is the ordered list of libraries not already loaded *) let cache_require (_,(needed,modl,export)) = List.iter register_library needed; - option_iter (fun exp -> open_libraries exp (List.map find_library modl)) + Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) export let load_require _ (_,(needed,modl,_)) = @@ -530,13 +542,17 @@ let require_library qidl export = let modrefl = List.map fst modrefl in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); - option_iter (fun exp -> + Option.iter (fun exp -> List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) export end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Options.xml_export then List.iter !xml_require modrefl; + if !Flags.dump then List.iter2 (fun (loc, _) dp -> + Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (unloc loc)) (string_of_dirpath dp) "lib")) + qidl modrefl; + if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () let require_library_from_file idopt file export = @@ -544,12 +560,12 @@ let require_library_from_file idopt file export = let needed = List.rev needed in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) export end else add_anonymous_leaf (in_require (needed,[modref],export)); - if !Options.xml_export then !xml_require modref; + if !Flags.xml_export then !xml_require modref; add_frozen_state () (* the function called by Vernacentries.vernac_import *) @@ -614,7 +630,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) + with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e (************************************************************************) (*s Display the memory use of a library. *) diff --git a/library/nameops.ml b/library/nameops.ml index 6d0ad8ef..df9aa95d 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 9429 2006-12-12 08:01:03Z herbelin $ *) +(* $Id: nameops.ml 9433 2006-12-12 09:38:53Z herbelin $ *) open Pp open Util diff --git a/library/nameops.mli b/library/nameops.mli index 25c4ea56..b6a39c20 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nameops.mli 9429 2006-12-12 08:01:03Z herbelin $ i*) +(*i $Id: nameops.mli 9433 2006-12-12 09:38:53Z herbelin $ i*) open Names diff --git a/library/nametab.ml b/library/nametab.ml index 4e4e9b91..2c794fae 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml 10270 2007-10-29 14:48:33Z notin $ *) +(* $Id: nametab.ml 10664 2008-03-14 11:27:37Z soubiran $ *) open Util open Pp @@ -107,7 +107,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Options.if_verbose + Flags.if_verbose warning ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"); current @@ -147,7 +147,7 @@ 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 *) - Options.if_verbose + Flags.if_verbose warning ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"); current @@ -263,9 +263,11 @@ type ccitab = extended_global_reference SpTab.t let the_ccitab = ref (SpTab.empty : ccitab) type kntab = kernel_name SpTab.t -let the_modtypetab = ref (SpTab.empty : kntab) let the_tactictab = ref (SpTab.empty : kntab) +type mptab = module_path SpTab.t +let the_modtypetab = ref (SpTab.empty : mptab) + type objtab = unit SpTab.t let the_objtab = ref (SpTab.empty : objtab) @@ -299,8 +301,10 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab) type mprevtab = dir_path MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) +type mptrevtab = section_path MPmap.t +let the_modtyperevtab = ref (MPmap.empty : mptrevtab) + type knrevtab = section_path KNmap.t -let the_modtyperevtab = ref (KNmap.empty : knrevtab) let the_tacticrevtab = ref (KNmap.empty : knrevtab) @@ -314,7 +318,10 @@ let push_xref visibility sp xref = the_ccitab := SpTab.push visibility sp xref !the_ccitab; match visibility with | Until _ -> - the_globrevtab := Globrevtab.add xref sp !the_globrevtab + if Globrevtab.mem xref !the_globrevtab then + () + else + the_globrevtab := Globrevtab.add xref sp !the_globrevtab | _ -> () let push_cci visibility sp ref = @@ -328,7 +335,7 @@ let push = push_cci let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; - the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab + the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab (* This is for tactic definition names *) @@ -427,7 +434,7 @@ let global r = | TrueGlobal ref -> ref | SyntacticDef _ -> user_err_loc (loc,"global", - str "Unexpected reference to a syntactic definition: " ++ + str "Unexpected reference to a notation: " ++ pr_qualid qid) with Not_found -> error_global_not_found_loc loc qid @@ -483,7 +490,7 @@ let shortest_qualid_of_module mp = DirTab.shortest_qualid Idset.empty dir !the_dirtab let shortest_qualid_of_modtype kn = - let sp = KNmap.find kn !the_modtyperevtab in + let sp = MPmap.find kn !the_modtyperevtab in SpTab.shortest_qualid Idset.empty sp !the_modtypetab let shortest_qualid_of_tactic kn = @@ -497,13 +504,14 @@ let pr_global_env env ref = let s = string_of_qualid (shortest_qualid_of_global env ref) in (str s) -let global_inductive r = +let inductive_of_reference r = match global r with | IndRef ind -> ind | ref -> user_err_loc (loc_of_reference r,"global_inductive", pr_reference r ++ spc () ++ str "is not an inductive type") + (********************************************************************) (********************************************************************) @@ -520,10 +528,11 @@ let init () = the_tactictab := SpTab.empty; the_globrevtab := Globrevtab.empty; the_modrevtab := MPmap.empty; - the_modtyperevtab := KNmap.empty; + the_modtyperevtab := MPmap.empty; the_tacticrevtab := KNmap.empty + let freeze () = !the_ccitab, !the_dirtab, diff --git a/library/nametab.mli b/library/nametab.mli index a05b7415..71ea0aa5 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli 7596 2005-11-21 09:17:07Z herbelin $ i*) +(*i $Id: nametab.mli 10497 2008-02-01 12:18:37Z soubiran $ i*) (*i*) open Util @@ -73,7 +73,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> section_path -> global_reference -> unit val push_syntactic_definition : visibility -> section_path -> kernel_name -> unit -val push_modtype : visibility -> section_path -> kernel_name -> unit +val push_modtype : visibility -> section_path -> module_path -> unit val push_dir : visibility -> dir_path -> global_dir_reference -> unit val push_object : visibility -> section_path -> unit val push_tactic : visibility -> section_path -> kernel_name -> unit @@ -89,9 +89,9 @@ val locate : qualid -> global_reference val global : reference -> global_reference (* The same for inductive types *) -val global_inductive : reference -> inductive +val inductive_of_reference : reference -> inductive -(* This locates also syntactic definitions *) +(* This locates also syntactic definitions; raise [Not_found] if not found *) val extended_locate : qualid -> extended_global_reference (* This locates all names with a given suffix, if qualid is valid as @@ -106,7 +106,7 @@ val locate_obj : qualid -> section_path val locate_constant : qualid -> constant val locate_mind : qualid -> mutual_inductive val locate_section : qualid -> dir_path -val locate_modtype : qualid -> kernel_name +val locate_modtype : qualid -> module_path val locate_syntactic_definition : qualid -> kernel_name type ltac_constant = kernel_name @@ -161,7 +161,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds Coq.A.B.x that denotes the same object. *) val shortest_qualid_of_module : module_path -> qualid -val shortest_qualid_of_modtype : kernel_name -> qualid +val shortest_qualid_of_modtype : module_path -> qualid (* -- cgit v1.2.3