From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- library/decl_kinds.ml | 75 ++++ library/declare.ml | 402 +++++++++++++++++++++ library/declare.mli | 102 ++++++ library/declaremods.ml | 820 ++++++++++++++++++++++++++++++++++++++++++ library/declaremods.mli | 116 ++++++ library/dischargedhypsmap.ml | 60 ++++ library/dischargedhypsmap.mli | 24 ++ library/doc.tex | 16 + library/global.ml | 145 ++++++++ library/global.mli | 95 +++++ library/goptions.ml | 359 ++++++++++++++++++ library/goptions.mli | 171 +++++++++ library/impargs.ml | 551 ++++++++++++++++++++++++++++ library/impargs.mli | 69 ++++ library/lib.ml | 566 +++++++++++++++++++++++++++++ library/lib.mli | 156 ++++++++ library/libnames.ml | 269 ++++++++++++++ library/libnames.mli | 140 ++++++++ library/libobject.ml | 157 ++++++++ library/libobject.mli | 105 ++++++ library/library.ml | 704 ++++++++++++++++++++++++++++++++++++ library/library.mli | 94 +++++ library/nameops.ml | 173 +++++++++ library/nameops.mli | 55 +++ library/nametab.ml | 553 ++++++++++++++++++++++++++++ library/nametab.mli | 171 +++++++++ library/states.ml | 39 ++ library/states.mli | 29 ++ library/summary.ml | 73 ++++ library/summary.mli | 32 ++ 30 files changed, 6321 insertions(+) create mode 100644 library/decl_kinds.ml create mode 100644 library/declare.ml create mode 100644 library/declare.mli create mode 100644 library/declaremods.ml create mode 100644 library/declaremods.mli create mode 100644 library/dischargedhypsmap.ml create mode 100644 library/dischargedhypsmap.mli create mode 100644 library/doc.tex create mode 100644 library/global.ml create mode 100644 library/global.mli create mode 100644 library/goptions.ml create mode 100644 library/goptions.mli create mode 100644 library/impargs.ml create mode 100644 library/impargs.mli create mode 100644 library/lib.ml create mode 100644 library/lib.mli create mode 100644 library/libnames.ml create mode 100644 library/libnames.mli create mode 100644 library/libobject.ml create mode 100644 library/libobject.mli create mode 100644 library/library.ml create mode 100644 library/library.mli create mode 100644 library/nameops.ml create mode 100644 library/nameops.mli create mode 100755 library/nametab.ml create mode 100755 library/nametab.mli create mode 100644 library/states.ml create mode 100644 library/states.mli create mode 100644 library/summary.ml create mode 100644 library/summary.mli (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml new file mode 100644 index 00000000..a030284c --- /dev/null +++ b/library/decl_kinds.ml @@ -0,0 +1,75 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* IsDefinition + | Proof s -> IsProof s + diff --git a/library/declare.ml b/library/declare.ml new file mode 100644 index 00000000..8b9dfeda --- /dev/null +++ b/library/declare.ml @@ -0,0 +1,402 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "(local)" + | Global -> "(global)" + +(* XML output hooks *) +let xml_declare_variable = ref (fun sp -> ()) +let xml_declare_constant = ref (fun sp -> ()) +let xml_declare_inductive = ref (fun sp -> ()) + +let if_xml f x = if !Options.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. *) + +type section_variable_entry = + | SectionLocalDef of constr * types option * bool (* opacity *) + | SectionLocalAssum of types + +type variable_declaration = dir_path * section_variable_entry * local_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 * local_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,_),(id,(p,d,mk))) = + (* Constr raisonne sur les noms courts *) + if Idmap.mem id !vartab then + errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); + let vd = match d with (* Fails if not well-typed *) + | SectionLocalAssum ty -> + let cst = Global.push_named_assum (id,ty) in + let (_,bd,ty) = Global.lookup_named id in + CheckedSectionLocalAssum (ty,cst) + | 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 + Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + vartab := Idmap.add id (p,vd,mk) !vartab + +let (in_variable, out_variable) = + declare_object { (default_object "VARIABLE") with + cache_function = cache_variable; + classify_function = (fun _ -> Dispose) } + +let declare_variable_common id obj = + let oname = add_leaf id (in_variable (id,obj)) in + declare_var_implicits id; + Symbols.declare_ref_arguments_scope (VarRef id); + oname + +(* for initial declaration *) +let declare_variable id obj = + let (sp,kn as oname) = declare_variable_common id obj in + !xml_declare_variable oname; + Dischargedhypsmap.set_discharged_hyps sp []; + oname + +(* when coming from discharge: no xml output *) +let redeclare_variable id discharged_hyps obj = + let oname = declare_variable_common id obj in + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps + +(* Globals: constants and parameters *) + +type constant_declaration = constant_entry * global_kind + +let csttab = ref (Spmap.empty : global_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 } + +let cache_constant ((sp,kn),(cdt,kind)) = + (if Idmap.mem (basename sp) !vartab then + errorlabstrm "cache_constant" + (pr_id (basename sp) ++ str " already exists")); + (if Nametab.exists_cci sp then + let (_,id) = repr_path sp in + errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); + let _,dir,_ = repr_kn kn in + let kn' = Global.add_constant dir (basename sp) cdt in + if kn' <> kn then + anomaly "Kernel and Library names do not match"; + Nametab.push (Nametab.Until 1) sp (ConstRef kn); + csttab := Spmap.add sp kind !csttab + +(* 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)) = + (if Nametab.exists_cci sp then + let (_,id) = repr_path sp in + errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); + csttab := Spmap.add sp kind !csttab; + Nametab.push (Nametab.Until i) sp (ConstRef kn) + +(* Opening means making the name without its module qualification available *) +let open_constant i ((sp,kn),_) = + Nametab.push (Nametab.Exactly i) sp (ConstRef kn) + +(* Hack to reduce the size of .vo: we keep only what load/open needs *) +let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) + +let dummy_constant (ce,mk) = dummy_constant_entry,mk + +let export_constant cst = Some (dummy_constant cst) + +let classify_constant (_,cst) = Substitute (dummy_constant cst) + +let (in_constant, out_constant) = + declare_object { (default_object "CONSTANT") with + cache_function = cache_constant; + load_function = load_constant; + open_function = open_constant; + classify_function = classify_constant; + subst_function = ident_subst_function; + export_function = export_constant } + +let hcons_constant_declaration = function + | DefinitionEntry ce -> + let (hcons1_constr,_) = hcons_constr (hcons_names()) in + DefinitionEntry + { const_entry_body = hcons1_constr ce.const_entry_body; + const_entry_type = option_app hcons1_constr ce.const_entry_type; + const_entry_opaque = ce.const_entry_opaque } + | cd -> cd + +let declare_constant_common id discharged_hyps (cd,kind) = + let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in + declare_constant_implicits kn; + Symbols.declare_ref_arguments_scope (ConstRef kn); + Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; + oname + +let declare_constant_gen internal id (cd,kind) = + let cd = hcons_constant_declaration cd in + let oname = declare_constant_common id [] (ConstantEntry cd,kind) in + !xml_declare_constant (internal,oname); + oname + +let declare_internal_constant = declare_constant_gen true +let declare_constant = declare_constant_gen false + +(* when coming from discharge *) +let redeclare_constant id discharged_hyps (cd,kind) = + let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in + () + +(* Inductives. *) + +let inductive_names sp kn mie = + let (dp,_) = repr_path sp in + let names, _ = + List.fold_left + (fun (names, n) ind -> + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) ind.mind_entry_consnames in + let sp = Libnames.make_path dp ind.mind_entry_typename + in + ((sp, IndRef ind_p) :: names, n+1)) + ([], 0) mie.mind_entry_inds + in names + + +let check_exists_inductive (sp,_) = + (if Idmap.mem (basename sp) !vartab then + errorlabstrm "cache_inductive" + (pr_id (basename sp) ++ str " already exists")); + if Nametab.exists_cci sp then + let (_,id) = repr_path sp in + errorlabstrm "cache_inductive" (pr_id id ++ str " already exists") + +let cache_inductive ((sp,kn),mie) = + let names = inductive_names sp kn mie in + List.iter check_exists_inductive names; + let _,dir,_ = repr_kn kn in + let kn' = Global.add_mind dir (basename sp) mie in + if kn' <> kn then + anomaly "Kernel and Library names do not match"; + + List.iter + (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) + names + +let load_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in + List.iter check_exists_inductive names; + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names + +let open_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in +(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*) + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + +let dummy_one_inductive_entry mie = { + mind_entry_params = []; + mind_entry_typename = mie.mind_entry_typename; + mind_entry_arity = mkProp; + mind_entry_consnames = mie.mind_entry_consnames; + mind_entry_lc = [] +} + +(* Hack to reduce the size of .vo: we keep only what load/open needs *) +let dummy_inductive_entry m = { + mind_entry_finite = true; + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds } + +let export_inductive x = Some (dummy_inductive_entry x) + +let (in_inductive, out_inductive) = + declare_object {(default_object "INDUCTIVE") with + cache_function = cache_inductive; + load_function = load_inductive; + open_function = open_inductive; + classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); + subst_function = ident_subst_function; + export_function = export_inductive } + +let declare_inductive_argument_scopes kn mie = + list_iter_i (fun i {mind_entry_consnames=lc} -> + Symbols.declare_ref_arguments_scope (IndRef (kn,i)); + for j=1 to List.length lc do + Symbols.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + +let declare_inductive_common mie = + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> anomaly "cannot declare an empty list of inductives" + in + let oname = add_leaf id (in_inductive mie) in + declare_mib_implicits (snd oname); + declare_inductive_argument_scopes (snd oname) mie; + oname + +(* for initial declaration *) +let declare_mind isrecord mie = + let (sp,kn as oname) = declare_inductive_common mie in + Dischargedhypsmap.set_discharged_hyps sp [] ; + !xml_declare_inductive (isrecord,oname); + oname + +(* when coming from discharge: no xml output *) +let redeclare_inductive discharged_hyps mie = + let oname = declare_inductive_common mie in + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ; + 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 get_variable_with_constraints id = + let (p,x,_) = Idmap.find id !vartab in + match x with + | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst) + | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst) + +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.map + (fun (id,c,t as d) -> if variable_opacity id then (id,None,t) else d) sign + +(* 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 context_of_global_reference = function + | VarRef id -> [] + | ConstRef sp -> (Global.lookup_constant sp).const_hyps + | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps + | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps + +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 new file mode 100644 index 00000000..968be059 --- /dev/null +++ b/library/declare.mli @@ -0,0 +1,102 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* variable_declaration -> object_name + +(* Declaration from Discharge *) +val redeclare_variable : + variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit + +(* Declaration of global constructions *) +(* i.e. Definition/Theorem/Axiom/Parameter/... *) + +type constant_declaration = constant_entry * global_kind + +(* [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration *) +val declare_constant : identifier -> constant_declaration -> object_name + +val declare_internal_constant : + identifier -> constant_declaration -> object_name + +val redeclare_constant : + identifier -> Dischargedhypsmap.discharged_hyps -> + Cooking.recipe * global_kind -> unit + +(* [declare_mind me] declares a block of inductive types with + their constructors in the current section; it returns the path of + the whole block (boolean must be true iff it is a record) *) +val declare_mind : bool -> mutual_inductive_entry -> object_name + +(* Declaration from Discharge *) +val redeclare_inductive : + Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name + +val out_inductive : Libobject.obj -> mutual_inductive_entry + +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 -> global_kind + +val out_variable : Libobject.obj -> identifier * variable_declaration +val get_variable : variable -> named_declaration +val get_variable_with_constraints : + variable -> named_declaration * Univ.constraints +val variable_strength : variable -> strength +val variable_kind : variable -> local_kind +val find_section_variable : variable -> section_path +val last_section_hyps : dir_path -> identifier list +val clear_proofs : named_context -> named_context + +(*s Global references *) + +val context_of_global_reference : global_reference -> section_context +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 * object_name -> unit) -> unit +val set_xml_declare_inductive : (bool * object_name -> unit) -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml new file mode 100644 index 00000000..b968a432 --- /dev/null +++ b/library/declaremods.ml @@ -0,0 +1,820 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + !modtab_substobjs, + !modtab_objects, + !openmod_info); + Summary.unfreeze_function = (fun (sobjs,objs,info) -> + modtab_substobjs := sobjs; + modtab_objects := objs; + openmod_info := info); + Summary.init_function = (fun () -> + modtab_substobjs := MPmap.empty; + modtab_objects := MPmap.empty; + openmod_info := ([],None,None)); + Summary.survive_module = false; + Summary.survive_section = false } + +(* auxiliary functions to transform section_path and kernel_name given + by Lib into module_path and dir_path needed for modules *) + +let mp_of_kn kn = + let mp,sec,l = repr_kn kn in + if sec=empty_dirpath then + MPdot (mp,l) + else + anomaly ("Non-empty section in module name!" ^ string_of_kn kn) + +let dir_of_sp sp = + let dir,id = repr_path sp in + extend_dirpath dir id + +let msid_of_mp = function + MPself msid -> msid + | _ -> anomaly "'Self' module path expected!" + +let msid_of_prefix (_,(mp,sec)) = + if sec=empty_dirpath then + msid_of_mp mp + else + anomaly ("Non-empty section in module name!" ^ + string_of_mp mp ^ "." ^ string_of_dirpath sec) + + +(* 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 _ = Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) + in + () (* The constraints are checked and forgot immediately! *) + + +(* This function registers the visibility of the module and iterates + through its components. It is called by plenty module functions *) + +let do_module exists what iter_objects i dir mp substobjs objects = + let prefix = (dir,(mp,empty_dirpath)) 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 objects with + Some seg -> + modtab_objects := MPmap.add mp (prefix,seg) !modtab_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 + do_module exists what iter_objects i dir mp substobjs substituted + +(* Interactive modules and module types cannot be recached! cache_mod* + functions can be called only once (and "end_mod*" set the flag to + false then) +*) + +let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = + let _ = 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_modtype (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"; + + match sub_mtb_o with + None -> () + | Some sub_mtb -> 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 -> () + | Some _ -> + anomaly ("We should never have full info in " ^ s^"!") + + +(* When this function is called the module itself is already in the + environment. This function loads its objects only *) + +let load_module i (oname,(entry,substobjs,substituted)) = + (* TODO: This check is not essential *) + check_empty "load_module" entry; + conv_names_do_module false "load" load_objects i oname substobjs substituted + + +let open_module i (oname,(entry,substobjs,substituted)) = + (* TODO: This check is not essential *) + check_empty "open_module" entry; + 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 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 *) + let substituted = subst_substobjs dir mp substobjs + in + (None,substobjs,substituted) + + +let classify_module (_,(_,substobjs,_)) = + Substitute (None,substobjs,None) + +let (in_module,out_module) = + declare_object {(default_object "MODULE") with + cache_function = cache_module; + load_function = load_module; + open_function = open_module; + subst_function = subst_module; + classify_function = classify_module; + 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) = + let mp = mp_of_kn kn in + let prefix = dir_of_sp sp, (mp,empty_dirpath) in + begin + try + let prefix',objects = MPmap.find mp !modtab_objects in + if prefix' <> prefix then + anomaly "Two different modules with the same path!"; + modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects; + with + Not_found -> anomaly "Keep objects before substitutive" + end; + load_objects i prefix seg + +let open_keep i ((sp,kn),seg) = + let dirpath,mp = dir_of_sp sp, mp_of_kn kn in + open_objects i (dirpath,(mp,empty_dirpath)) seg + +let (in_modkeep,out_modkeep) = + declare_object {(default_object "MODULE KEEP OBJECTS") with + cache_function = cache_keep; + load_function = load_keep; + open_function = open_keep; + export_function = (fun _ -> anomaly "No modules in sections!") } + +(* we remember objects for a module type. In case of a declaration: + Module M:SIG:=... + The module M gets its objects from SIG +*) +let modtypetab = + ref (KNmap.empty : substitutive_objects KNmap.t) + +(* currently started interactive module type. We remember its arguments + if it is a functor type *) +let openmodtype_info = + ref ([] : mod_bound_id list) + +let _ = Summary.declare_summary "MODTYPE-INFO" + { Summary.freeze_function = (fun () -> + !modtypetab,!openmodtype_info); + Summary.unfreeze_function = (fun ft -> + modtypetab := fst ft; + openmodtype_info := snd ft); + Summary.init_function = (fun () -> + modtypetab := KNmap.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 + anomaly "Kernel and Library names do not match" + in + + if Nametab.exists_modtype sp then + errorlabstrm "cache_modtype" + (pr_sp sp ++ str " already exists") ; + + Nametab.push_modtype (Nametab.Until 1) sp kn; + + modtypetab := KNmap.add kn modtypeobjs !modtypetab + + +let load_modtype i ((sp,kn),(entry,modtypeobjs)) = + check_empty "load_modtype" entry; + + if Nametab.exists_modtype sp then + errorlabstrm "cache_modtype" + (pr_sp sp ++ str " already exists") ; + + Nametab.push_modtype (Nametab.Until i) sp kn; + + modtypetab := KNmap.add 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 + with Not_found -> true + then + errorlabstrm ("open_modtype") + (pr_sp sp ++ str " should already exist!"); + + Nametab.push_modtype (Nametab.Exactly i) sp kn + + +let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = + check_empty "subst_modtype" entry; + (entry,(join subs subst,mbids,msid,objs)) + + +let classify_modtype (_,(_,substobjs)) = + Substitute (None,substobjs) + + +let (in_modtype,out_modtype) = + declare_object {(default_object "MODULE TYPE") with + cache_function = cache_modtype; + open_function = open_modtype; + load_function = load_modtype; + subst_function = subst_modtype; + classify_function = classify_modtype; + export_function = in_some } + + + +let replace_module_object id (subst, mbids, msid, lib_stack) modobjs = + if mbids<>[] then + error "Unexpected functor objects" + else + let rec replace_id = function + | [] -> [] + | (id',obj)::tail when id = id' -> + if object_tag obj = "MODULE" then + (id, in_module (None,modobjs,None))::tail + else error "MODULE expected!" + | lobj::tail -> lobj::replace_id tail + in + (subst, mbids, msid, replace_id 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 + (subst, mbid::mbids, msid, objs) + | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty + | MTEwith (mty, With_Module (id,mp)) -> + let substobjs = get_modtype_substobjs mty in + let modobjs = MPmap.find mp !modtab_substobjs in + replace_module_object id substobjs modobjs + | MTEsig (msid,_) -> + todo "Anonymous module types"; (empty_subst, [], msid, []) + +(* 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 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 (env,oldargs) (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 env arg in + let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in + let mps = List.map (fun mbid -> MPbound mbid) mbids in + let substobjs = get_modtype_substobjs mty in + let substituted's = + List.map2 + (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) + dirs mps + in + List.iter + (fun (dir, mp, substituted) -> + do_module false "interp" load_objects 1 dir mp substobjs substituted) + substituted's; + let body = Modops.module_body_of_type (get_some_body mty env) in + let env = + List.fold_left (fun env mp -> Modops.add_module mp body env) env mps + in + env, List.map (fun mbid -> mbid,mty) mbids :: oldargs + +let start_module interp_modtype id args res_o = + let fs = Summary.freeze_summaries () in + let env = Global.env () in + let env,arg_entries_revlist = + List.fold_left (intern_args interp_modtype) (env,[]) args + in + let arg_entries = List.concat (List.rev arg_entries_revlist) in + + let res_entry_o, sub_body_o = match res_o with + None -> None, None + | Some (res, true) -> + Some (interp_modtype env res), None + | Some (res, false) -> + (* If the module type is non-restricting, we must translate it + here to catch errors as early as possible. If it is + estricting, the kernel takes care of it. *) + let sub_mte = + List.fold_right + (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + arg_entries + (interp_modtype env res) + in + let sub_mtb = + Mod_typing.translate_modtype (Global.env()) sub_mte + in + None, Some sub_mtb + in + + let mp = Global.start_module id arg_entries res_entry_o in + + let mbids = List.map fst arg_entries in + openmod_info:=(mbids,res_entry_o,sub_body_o); + let prefix = Lib.start_module id mp fs in + Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); + Lib.add_frozen_state () + + +let end_module id = + + let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in + let mp = Global.end_module id in + let mbids, res_o, sub_o = !openmod_info 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 + let msid = msid_of_prefix oldprefix in + + let substobjs = try + match res_o with + | None -> + empty_subst, mbids, msid, substitute + | Some (MTEident ln) -> + abstract_substobjs mbids (KNmap.find ln (!modtypetab)) + | Some (MTEsig (msid,_)) -> + todo "Anonymous signatures not supported"; + empty_subst, mbids, msid, [] + | Some (MTEwith _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs mty) + | Some (MTEfunsig _) -> + anomaly "Funsig cannot be here..." + with + Not_found -> anomaly "Module objects not found..." + in + + (* must be called after get_modtype_substobjs, because of possible + dependencies on functor arguments *) + Summary.module_unfreeze_summaries fs; + + let substituted = subst_substobjs dir mp substobjs in + let node = in_module (None,substobjs,substituted) in + let objects = + if keep = [] || mbids <> [] then + special@[node] (* no keep objects or we are defining a functor *) + else + special@[node;in_modkeep keep] (* otherwise *) + in + let newoname = Lib.add_leaves id objects in + + if (fst newoname) <> (fst oldoname) then + anomaly "Names generated on start_ and end_module do not match"; + if mp_of_kn (snd newoname) <> mp then + anomaly "Kernel and Library names do not match"; + + Lib.add_frozen_state () (* to prevent recaching *) + + + +let module_objects mp = + let prefix,objects = MPmap.find mp !modtab_objects in + segment_of_objects prefix objects + + + +(************************************************************************) +(* libraries *) + +type library_name = dir_path + +(* The first two will form substitutive_objects, the last one is keep *) +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 prefix = dir, (mp, empty_dirpath) 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 + with + Not_found -> + if mp <> Global.import cenv digest then + anomaly "Unexpected disk module name"; + let msid,substitute,keep = objs in + let substobjs = empty_subst, [], msid, substitute in + let substituted = subst_substobjs dir mp substobjs in + let objects = option_app (fun seg -> seg@keep) substituted in + let modobjs = substobjs, objects in + Hashtbl.add library_cache dir modobjs; + modobjs + in + do_module false "register_library" load_objects 1 dir mp substobjs objects + + +let start_library dir = + let mp = Global.start_library dir in + openmod_info:=[],None,None; + Lib.start_compilation dir mp; + Lib.add_frozen_state () + + +let end_library dir = + let prefix, lib_stack = Lib.end_compilation dir in + let cenv = Global.export dir in + let msid = msid_of_prefix prefix in + let substitute, keep, _ = Lib.classify_segment lib_stack in + cenv,(msid,substitute,keep) + + +(* implementation of Export M and Import M *) + + +let really_import_module mp = + let prefix,objects = MPmap.find mp !modtab_objects in + open_objects 1 prefix objects + + +let cache_import (_,(_,mp)) = +(* for non-substitutive exports: + let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) + really_import_module mp + +let classify_import (_,(export,_ as obj)) = + if export then Substitute obj else Dispose + +let subst_import (_,subst,(export,mp as obj)) = + let mp' = subst_mp subst mp in + if mp'==mp then obj else + (export,mp') + +let (in_import,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 } + + +let import_module export mp = + Lib.add_anonymous_leaf (in_import (export,mp)) + +(************************************************************************) +(* module types *) + +let start_modtype interp_modtype id args = + let fs = Summary.freeze_summaries () in + let env = Global.env () in + let env,arg_entries_revlist = + List.fold_left (intern_args interp_modtype) (env,[]) args + in + let arg_entries = List.concat (List.rev arg_entries_revlist) in + + let mp = Global.start_modtype id arg_entries in + + let mbids = List.map fst arg_entries in + 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 () + + +let end_modtype id = + + let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in + let ln = Global.end_modtype id in + let substitute, _, special = Lib.classify_segment lib_stack in + + let msid = msid_of_prefix prefix in + let mbids = !openmodtype_info in + + Summary.module_unfreeze_summaries fs; + + let modtypeobjs = empty_subst, mbids, msid, substitute in + + let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in + if fst oname <> fst oldoname then + anomaly + "Section paths generated on start_ and end_modtype do not match"; + if snd oname <> ln then + anomaly + "Kernel and Library names do not match"; + + Lib.add_frozen_state ()(* to prevent recaching *) + + +let declare_modtype interp_modtype id args mty = + let fs = Summary.freeze_summaries () in + let env = Global.env () in + let env,arg_entries_revlist = + List.fold_left (intern_args interp_modtype) (env,[]) args + in + let arg_entries = List.concat (List.rev arg_entries_revlist) in + let base_mty = interp_modtype env mty in + let entry = + List.fold_right + (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + arg_entries + base_mty + in + let substobjs = get_modtype_substobjs entry in + Summary.unfreeze_summaries fs; + + ignore (add_leaf id (in_modtype (Some entry, substobjs))) + + + +let rec get_module_substobjs = function + | MEident mp -> MPmap.find mp !modtab_substobjs + | MEfunctor (mbid,mty,mexpr) -> + let (subst, mbids, msid, objs) = + get_module_substobjs mexpr + in + (subst, mbid::mbids, msid, objs) + | MEstruct (msid,_) -> + (empty_subst, [], msid, []) + | MEapply (mexpr, MEident mp) -> + let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + (match mbids with + | mbid::mbids -> + (add_mbid mbid mp subst, mbids, msid, objs) + | [] -> match mexpr with + | MEident _ | MEstruct _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") + | MEapply (_,mexpr) -> + Modops.error_application_to_not_path mexpr + + +let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = + + let fs = Summary.freeze_summaries () in + let env = Global.env () in + let env,arg_entries_revlist = + List.fold_left (intern_args interp_modtype) (env,[]) args + in + let arg_entries = List.concat (List.rev arg_entries_revlist) 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)) + arg_entries + (interp_modtype env mty)), + None + | (Some (mty, false)) -> + None, + Some (List.fold_right + (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + arg_entries + (interp_modtype env mty)) + in + let mexpr_entry_o = match mexpr_o with + None -> None + | Some mexpr -> + Some (List.fold_right + (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) + arg_entries + (interp_modexpr env mexpr)) + in + let entry = + {mod_entry_type = mty_entry_o; + mod_entry_expr = mexpr_entry_o } + in + let substobjs = + match entry with + | {mod_entry_type = Some mte} -> get_modtype_substobjs mte + | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr + | _ -> anomaly "declare_module: No type, no body ..." + in + Summary.unfreeze_summaries fs; + + 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))) + + +(*s Iterators. *) + +let fold_all_segments insec f x = + let acc' = + MPmap.fold + (fun _ (prefix,objects) acc -> + let apply_obj acc (id,obj) = f acc (make_oname prefix id) obj in + List.fold_left apply_obj acc objects) + !modtab_objects x + in + let rec apply_node acc = function + | sp, Leaf o -> f acc sp o + | _, ClosedSection (_,_,seg) -> + if insec then List.fold_left apply_node acc seg else acc + | _ -> acc + in + List.fold_left apply_node acc' (Lib.contents_after None) + +let iter_all_segments insec f = + let _ = + MPmap.iter + (fun _ (prefix,objects) -> + let apply_obj (id,obj) = f (make_oname prefix id) obj in + List.iter apply_obj objects) + !modtab_objects + in + let rec apply_node = function + | sp, Leaf o -> f sp o + | _, ClosedSection (_,_,seg) -> if insec then List.iter apply_node seg + | _ -> () + in + List.iter apply_node (Lib.contents_after None) + + + +let debug_print_modtab _ = + let pr_seg = function + | [] -> str "[]" + | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") + in + let pr_modinfo mp (prefix,objects) s = + s ++ str (string_of_mp mp) ++ (spc ()) + ++ (pr_seg (segment_of_objects prefix objects)) + in + let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in + hov 0 modules + + diff --git a/library/declaremods.mli b/library/declaremods.mli new file mode 100644 index 00000000..f229da1e --- /dev/null +++ b/library/declaremods.mli @@ -0,0 +1,116 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + identifier -> + (identifier located list * 'modtype) list -> ('modtype * bool) option -> + 'modexpr option -> unit + +val start_module : (env -> 'modtype -> module_type_entry) -> + identifier -> + (identifier located list * 'modtype) list -> ('modtype * bool) option -> + unit + +val end_module : identifier -> unit + + + +(*s Module types *) + +val declare_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit + +val start_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier located list * 'modtype) list -> unit + +val end_modtype : identifier -> unit + + +(*s Objects of a module. They come in two lists: the substitutive ones + and the other *) + +val module_objects : module_path -> library_segment + + +(*s Libraries i.e. modules on disk *) + +type library_name = dir_path + +type library_objects + +val register_library : + library_name -> + Safe_typing.compiled_library -> library_objects -> Digest.t -> unit + +val start_library : library_name -> unit + +val end_library : + library_name -> Safe_typing.compiled_library * library_objects + + +(* [really_import_module mp] opens the module [mp] (in a Caml sense). + It modifies Nametab and performs the "open_object" function for + every object of the module. *) + +val really_import_module : module_path -> unit + +(* [import_module export mp] is a synchronous version of + [really_import_module]. If [export] is [true], the module is also + opened every time the module containing it is. *) + +val import_module : bool -> module_path -> unit + + +(*s [fold_all_segments] and [iter_all_segments] iterate over all + segments, the modules' segments first and then the current + segment. Modules are presented in an arbitrary order. The given + function is applied to all leaves (together with their section + path). The boolean indicates if we must enter closed sections. *) + +val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a +val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit + + +val debug_print_modtab : unit -> Pp.std_ppcmds + +(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*) + +(* For translator *) +val process_module_bindings : module_ident list -> + (mod_bound_id * module_type_entry) list -> unit diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml new file mode 100644 index 00000000..59a01d81 --- /dev/null +++ b/library/dischargedhypsmap.ml @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* cache_discharged_hyps_map); + export_function = (fun x -> Some x) } + +let set_discharged_hyps sp hyps = + add_anonymous_leaf (in_discharged_hyps_map (sp,hyps)) + +let get_discharged_hyps sp = + try + Spmap.find sp !discharged_hyps_map + with Not_found -> + anomaly ("No discharged hypothesis for object " ^ string_of_path sp) + +(*s Registration as global tables and rollback. *) + +let init () = + discharged_hyps_map := Spmap.empty + +let freeze () = !discharged_hyps_map + +let unfreeze dhm = discharged_hyps_map := dhm + +let _ = + Summary.declare_summary "discharged_hypothesis" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = true } diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli new file mode 100644 index 00000000..8851e5a3 --- /dev/null +++ b/library/dischargedhypsmap.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* discharged_hyps -> unit +val get_discharged_hyps : section_path -> discharged_hyps diff --git a/library/doc.tex b/library/doc.tex new file mode 100644 index 00000000..33af5933 --- /dev/null +++ b/library/doc.tex @@ -0,0 +1,16 @@ + +\newpage +\section*{The Coq library} + +\ocwsection \label{library} +This chapter describes the \Coq\ library, which is made of two parts: +\begin{itemize} + \item a general mechanism to keep a trace of all operations and of + the state of the system, with backtrack capabilities; + \item a global environment for the CCI, with functions to export and + import compiled modules. +\end{itemize} +The modules of the library are organized as follows. + +\bigskip +\begin{center}\epsfig{file=library.dep.ps}\end{center} diff --git a/library/global.ml b/library/global.ml new file mode 100644 index 00000000..bfa9335c --- /dev/null +++ b/library/global.ml @@ -0,0 +1,145 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !global_env); + unfreeze_function = (fun fr -> global_env := fr); + init_function = (fun () -> global_env := empty_environment); + survive_module = true; + survive_section = false } + +(* Then we export the functions of [Typing] on that environment. *) + +let universes () = universes (env()) +let named_context () = named_context (env()) + +let push_named_assum a = + let (cst,env) = push_named_assum a !global_env in + global_env := env; + cst +let push_named_def d = + let (cst,env) = push_named_def d !global_env in + global_env := env; + cst + +(*let add_thing add kn thing = + let _,dir,l = repr_kn kn in + let kn',newenv = add dir l thing !global_env in + if kn = kn' then + global_env := newenv + else + anomaly "Kernel names do not match." +*) + +let add_thing add dir id thing = + let kn, newenv = add dir (label_of_id id) thing !global_env in + global_env := newenv; + kn + +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_constraints c = global_env := add_constraints c !global_env + +let set_engagement c = global_env := set_engagement c !global_env + +let start_module id params mtyo = + let l = label_of_id id in + let mp,newenv = start_module l params mtyo !global_env in + global_env := newenv; + mp + +let end_module id = + let l = label_of_id id in + let mp,newenv = end_module l !global_env in + global_env := newenv; + mp + + +let start_modtype id params = + let l = label_of_id id in + let mp,newenv = start_modtype l params !global_env in + global_env := newenv; + mp + +let end_modtype id = + let l = label_of_id id in + let kn,newenv = end_modtype l !global_env in + global_env := newenv; + kn + + + + +let lookup_named id = lookup_named id (env()) +let lookup_constant kn = lookup_constant kn (env()) +let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind +let lookup_mind kn = lookup_mind kn (env()) + +let lookup_module mp = lookup_module mp (env()) +let lookup_modtype kn = lookup_modtype kn (env()) + + + + +let start_library dir = + let mp,newenv = start_library dir !global_env in + global_env := newenv; + mp + +let export s = snd (export !global_env s) + +let import cenv digest = + let mp,newenv = import cenv digest !global_env in + global_env := newenv; + mp + + + +(*s Function to get an environment from the constants part of the global + environment and a given context. *) + +let env_of_context hyps = + reset_with_named_context hyps (env()) + +open Libnames + +let type_of_reference env = function + | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t + | ConstRef c -> Environ.constant_type env c + | IndRef ind -> Inductive.type_of_inductive env ind + | ConstructRef cstr -> Inductive.type_of_constructor env cstr + +let type_of_global t = type_of_reference (env ()) t + + +(*let get_kn dp l = + make_kn (current_modpath !global_env) dp l +*) diff --git a/library/global.mli b/library/global.mli new file mode 100644 index 00000000..1da5965c --- /dev/null +++ b/library/global.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* safe_environment +val env : unit -> Environ.env + +val universes : unit -> universes +val named_context : unit -> Sign.named_context + +(*s Extending env with variables and local definitions *) +val push_named_assum : (identifier * types) -> Univ.constraints +val push_named_def : (identifier * constr * types option) -> Univ.constraints + +(*s Adding constants, inductives, modules and module types. All these + functions verify that given names match those generated by kernel *) + +val add_constant : + dir_path -> identifier -> global_declaration -> kernel_name +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_constraints : constraints -> unit + +val set_engagement : Environ.engagement -> unit + +(*s Interactive modules and module types *) +(* Both [start_*] functions take the [dir_path] argument to create a + [mod_self_id]. This should be the name of the compilation unit. *) + +(* [start_*] functions return the [module_path] valid for components + of the started module / module type *) + +val start_module : + identifier -> (mod_bound_id * module_type_entry) list + -> module_type_entry option + -> module_path + +val end_module : + identifier -> module_path + +val start_modtype : + identifier -> (mod_bound_id * module_type_entry) list + -> module_path + +val end_modtype : + identifier -> kernel_name + + +(* Queries *) +val lookup_named : variable -> named_declaration +val lookup_constant : constant -> constant_body +val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body +val lookup_mind : mutual_inductive -> mutual_inductive_body +val lookup_module : module_path -> module_body +val lookup_modtype : kernel_name -> module_type_body + +(* Compiled modules *) +val start_library : dir_path -> module_path +val export : dir_path -> compiled_library +val import : compiled_library -> Digest.t -> module_path + +(*s Function to get an environment from the constants part of the global + * environment and a given context. *) + +val type_of_global : Libnames.global_reference -> types +val env_of_context : Sign.named_context -> Environ.env + diff --git a/library/goptions.ml b/library/goptions.ml new file mode 100644 index 00000000..bcb4fb79 --- /dev/null +++ b/library/goptions.ml @@ -0,0 +1,359 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* s + | SecondaryTable (s1,s2) -> s1^" "^s2 + +let error_undeclared_key key = + error ((nickname key)^": no table or option of this type") + +type value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | IdentValue of global_reference + +(****************************************************************************) +(* 1- Tables *) + +class type ['a] table_of_A = +object + method add : 'a -> unit + method remove : 'a -> unit + method mem : 'a -> unit + method print : unit +end + +module MakeTable = + functor + (A : sig + type t + type key + val table : (string * key table_of_A) list ref + val encode : key -> t + val subst : substitution -> t -> t + val printer : t -> std_ppcmds + val key : option_name + val title : string + val member_message : t -> bool -> std_ppcmds + val synchronous : bool + end) -> + struct + type option_mark = + | GOadd + | GOrmv + + let nick = nickname A.key + + let _ = + if List.mem_assoc nick !A.table then + error "Sorry, this table name is already used" + + module MyType = struct type t = A.t let compare = Pervasives.compare end + module MySet = Set.Make(MyType) + + let t = ref (MySet.empty : MySet.t) + + let _ = + if A.synchronous then + let freeze () = !t in + let unfreeze c = t := c in + let init () = t := MySet.empty in + Summary.declare_summary nick + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = true } + + let (add_option,remove_option) = + if A.synchronous then + let cache_options (_,(f,p)) = match f with + | GOadd -> t := MySet.add p !t + | GOrmv -> t := MySet.remove p !t in + let load_options i o = if i=1 then cache_options o in + let subst_options (_,subst,(f,p as obj)) = + let p' = A.subst subst p in + if p' == p then obj else + (f,p') + in + let export_options fp = Some fp in + let (inGo,outGo) = + Libobject.declare_object {(Libobject.default_object nick) with + Libobject.load_function = load_options; + Libobject.open_function = load_options; + Libobject.cache_function = cache_options; + Libobject.subst_function = subst_options; + Libobject.classify_function = (fun (_,x) -> Substitute x); + Libobject.export_function = export_options} + in + ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), + (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) + else + ((fun c -> t := MySet.add c !t), + (fun c -> t := MySet.remove c !t)) + + let print_table table_name printer table = + msg (str table_name ++ + (hov 0 + (if MySet.is_empty table then str "None" ++ fnl () + else MySet.fold + (fun a b -> printer a ++ spc () ++ b) + table (mt ()) ++ fnl ()))) + + class table_of_A () = + object + method add x = add_option (A.encode x) + method remove x = remove_option (A.encode x) + method mem x = + let y = A.encode x in + let answer = MySet.mem y !t in + msg (A.member_message y answer ++ fnl ()) + method print = print_table A.title A.printer !t + end + + let _ = A.table := (nick,new table_of_A ())::!A.table + let active c = MySet.mem c !t + let elements () = MySet.elements !t + end + +let string_table = ref [] + +let get_string_table k = List.assoc (nickname k) !string_table + +module type StringConvertArg = +sig + val key : option_name + val title : string + val member_message : string -> bool -> std_ppcmds + val synchronous : bool +end + +module StringConvert = functor (A : StringConvertArg) -> +struct + type t = string + type key = string + let table = string_table + let encode x = x + let subst _ x = x + let printer = str + let key = A.key + let title = A.title + let member_message = A.member_message + let synchronous = A.synchronous +end + +module MakeStringTable = + functor (A : StringConvertArg) -> MakeTable (StringConvert(A)) + +let ref_table = ref [] + +let get_ref_table k = List.assoc (nickname k) !ref_table + +module type RefConvertArg = +sig + type t + val encode : reference -> t + val subst : substitution -> t -> t + val printer : t -> std_ppcmds + val key : option_name + val title : string + val member_message : t -> bool -> std_ppcmds + val synchronous : bool +end + +module RefConvert = functor (A : RefConvertArg) -> +struct + type t = A.t + type key = reference + let table = ref_table + let encode = A.encode + let subst = A.subst + let printer = A.printer + let key = A.key + let title = A.title + let member_message = A.member_message + let synchronous = A.synchronous +end + +module MakeRefTable = + functor (A : RefConvertArg) -> MakeTable (RefConvert(A)) + +(****************************************************************************) +(* 2- Options *) + +type 'a option_sig = { + optsync : bool; + optname : string; + optkey : option_name; + optread : unit -> 'a; + optwrite : 'a -> unit } + +type option_type = bool * (unit -> value) -> (value -> unit) + +module Key = struct type t = option_name let compare = Pervasives.compare end +module OptionMap = Map.Make(Key) + +let value_tab = ref OptionMap.empty + +(* This raises Not_found if option of key [key] is unknown *) + +let get_option key = OptionMap.find key !value_tab + +let check_key key = try + let _ = get_option key in + error "Sorry, this option name is already used" +with Not_found -> + if List.mem_assoc (nickname key) !string_table + or List.mem_assoc (nickname key) !ref_table + then error "Sorry, this option name is already used" + +open Summary +open Libobject +open Lib + +let declare_option cast uncast + { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } = + check_key key; + let default = read() in + let write = if sync then + let (decl_obj,_) = + declare_object {(default_object (nickname key)) with + cache_function = (fun (_,v) -> write v); + classify_function = (fun _ -> Dispose)} + in + let _ = declare_summary (nickname key) + {freeze_function = read; + unfreeze_function = write; + init_function = (fun () -> write default); + survive_module = false; + survive_section = true} + in + fun v -> add_anonymous_leaf (decl_obj v) + else write + in + let cread () = cast (read ()) in + let cwrite v = write (uncast v) in + value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; + write + +type 'a write_function = 'a -> unit + +let declare_int_option = + declare_option + (fun v -> IntValue v) + (function IntValue v -> v | _ -> anomaly "async_option") +let declare_bool_option = + declare_option + (fun v -> BoolValue v) + (function BoolValue v -> v | _ -> anomaly "async_option") +let declare_string_option = + declare_option + (fun v -> StringValue v) + (function StringValue v -> v | _ -> anomaly "async_option") + +(* 3- User accessible commands *) + +(* Setting values of options *) + +let set_option_value check_and_cast key v = + let (name,(_,read,write)) = + try get_option key + with Not_found -> error ("There is no option "^(nickname key)^".") + in + write (check_and_cast v (read ())) + +let bad_type_error () = error "Bad type of value for this option" + +let set_int_option_value = set_option_value + (fun v -> function + | (IntValue _) -> IntValue v + | _ -> bad_type_error ()) +let set_bool_option_value = set_option_value + (fun v -> function + | (BoolValue _) -> BoolValue v + | _ -> bad_type_error ()) +let set_string_option_value = set_option_value + (fun v -> function + | (StringValue _) -> StringValue v + | _ -> bad_type_error ()) + +(* Printing options/tables *) + +let msg_option_value (name,v) = + match v with + | BoolValue true -> str "true" + | BoolValue false -> str "false" + | IntValue (Some n) -> int n + | IntValue None -> str "undefined" + | StringValue s -> str s + | IdentValue r -> pr_global_env Idset.empty r + +let print_option_value key = + let (name,(_,read,_)) = get_option key in + let s = read () in + match s with + | BoolValue b -> + msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ + fnl ()) + | _ -> + msg (str ("Current value of "^name^" is ") ++ + msg_option_value (name,s) ++ fnl ()) + + +let print_tables () = + msg + (str "Synchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name,(sync,read,write)) p -> + if sync then + p ++ str (" "^(nickname key)^": ") ++ + msg_option_value (name,read()) ++ fnl () + else + p) + !value_tab (mt ()) ++ + str "Asynchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name,(sync,read,write)) p -> + if sync then + p + else + p ++ str (" "^(nickname key)^": ") ++ + msg_option_value (name,read()) ++ fnl ()) + !value_tab (mt ()) ++ + str "Tables:" ++ fnl () ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !string_table (mt ()) ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !ref_table (mt ()) ++ + fnl () + ) + + diff --git a/library/goptions.mli b/library/goptions.mli new file mode 100644 index 00000000..bbf5357a --- /dev/null +++ b/library/goptions.mli @@ -0,0 +1,171 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a + +(*s Tables. *) + +(* The functor [MakeStringTable] declares a table containing objects + of type [string]; the function [member_message] say what to print + when invoking the "Test Toto Titi foo." command; at the end [title] + is the table name printed when invoking the "Print Toto Titi." + command; [active] is roughly the internal version of the vernacular + "Test ...": it tells if a given object is in the table; [elements] + returns the list of elements of the table *) + +module MakeStringTable : + functor + (A : sig + val key : option_name + val title : string + val member_message : string -> bool -> std_ppcmds + val synchronous : bool + end) -> +sig + val active : string -> bool + val elements : unit -> string list +end + +(* The functor [MakeRefTable] declares a new table of objects of type + [A.t] practically denoted by [reference]; the encoding function + [encode : reference -> A.t] is typically a globalization function, + possibly with some restriction checks; the function + [member_message] say what to print when invoking the "Test Toto + Titi foo." command; at the end [title] is the table name printed + when invoking the "Print Toto Titi." command; [active] is roughly + the internal version of the vernacular "Test ...": it tells if a + given object is in the table. *) + +module MakeRefTable : + functor + (A : sig + type t + val encode : reference -> t + val subst : substitution -> t -> t + val printer : t -> std_ppcmds + val key : option_name + val title : string + val member_message : t -> bool -> std_ppcmds + val synchronous : bool + end) -> + sig + val active : A.t -> bool + val elements : unit -> A.t list + end + + +(*s Options. *) + +(* These types and function are for declaring a new option of name [key] + and access functions [read] and [write]; the parameter [name] is the option name + used when printing the option value (command "Print Toto Titi." *) + +type 'a option_sig = { + optsync : bool; + optname : string; + optkey : option_name; + optread : unit -> 'a; + optwrite : 'a -> unit +} + +(* When an option is declared synchronous ([optsync] is [true]), the output is + a synchronous write function. Otherwise it is [optwrite] *) + +type 'a write_function = 'a -> unit + +val declare_int_option : int option option_sig -> int option write_function +val declare_bool_option : bool option_sig -> bool write_function +val declare_string_option: string option_sig -> string write_function + + +(*s Special functions supposed to be used only in vernacentries.ml *) + +val get_string_table : + option_name -> + < add : string -> unit; + remove : string -> unit; + mem : string -> unit; + print : unit > + +val get_ref_table : + option_name -> + < add : reference -> unit; + remove : reference -> unit; + mem : reference -> unit; + print : unit > + +val set_int_option_value : option_name -> int option -> unit +val set_bool_option_value : option_name -> bool -> unit +val set_string_option_value : option_name -> string -> unit + +val print_option_value : option_name -> unit + +val print_tables : unit -> unit + diff --git a/library/impargs.ml b/library/impargs.ml new file mode 100644 index 00000000..8a9429a4 --- /dev/null +++ b/library/impargs.ml @@ -0,0 +1,551 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* begin + implicit_args := oa; + strict_implicit_args := ob; + contextual_implicit_args := oc; + implicit_args_out := od; + strict_implicit_args_out := oe; + contextual_implicit_args_out := og; + raise e + end + +(*s Computation of implicit arguments *) + +(* We remember various information about why an argument is (automatically) + inferable as implicit + +- [DepRigid] means that the implicit argument can be found by + unification along a rigid path (we do not print the arguments of + this kind if there is enough arguments to infer them) + +- [DepFlex] means that the implicit argument can be found by unification + along a collapsable path only (e.g. as x in (P x) where P is another + argument) (we do (defensively) print the arguments of this kind) + +- [DepFlexAndRigid] means that the least argument from which the + implicit argument can be inferred is following a collapsable path + but there is a greater argument from where the implicit argument is + inferable following a rigid path (useful to know how to print a + partial application) + + We also consider arguments inferable from the conclusion but it is + operational only if [conclusion_matters] is true. +*) + +type argument_position = + | Conclusion + | Hyp of int + +type implicit_explanation = + | DepRigid of argument_position + | DepFlex of argument_position + | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position + | Manual + +let argument_less = function + | Hyp n, Hyp n' -> n true + | Conclusion, _ -> false + +let update pos rig (na,st) = + let e = + if rig then + match st with + | None -> DepRigid pos + | Some (DepRigid n as x) -> + if argument_less (pos,n) then DepRigid pos else x + | Some (DepFlexAndRigid (fpos,rpos) as x) -> + if argument_less (pos,fpos) or pos=fpos then DepRigid pos else + if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x + | Some (DepFlex fpos as x) -> + if argument_less (pos,fpos) or pos=fpos then DepRigid pos + else DepFlexAndRigid (fpos,pos) + | Some Manual -> assert false + else + match st with + | None -> DepFlex pos + | Some (DepRigid rpos as x) -> + if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x + | Some (DepFlexAndRigid (fpos,rpos) as x) -> + 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 + in na, Some e + +(* modified is_rigid_reference with a truncated env *) +let is_flexible_reference env bound depth f = + match kind_of_term f with + | Rel n when n >= bound+depth -> (* inductive type *) false + | Rel n when n >= depth -> (* previous argument *) true + | Rel n -> (* since local definitions have been expanded *) false + | Const kn -> + let cb = Environ.lookup_constant kn env in + cb.const_body <> None & not cb.const_opaque + | Var id -> + let (_,value,_) = Environ.lookup_named id env in value <> None + | Ind _ | Construct _ -> false + | _ -> true + +let push_lift d (e,n) = (push_rel d e,n+1) + +(* Precondition: rels in env are for inductive types only *) +let add_free_rels_until strict bound env m pos acc = + let rec frec rig (env,depth as ed) c = + match kind_of_term (whd_betadeltaiota env c) with + | Rel n when (n < bound+depth) & (n >= depth) -> + acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1)) + | 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 + | _ -> + iter_constr_with_full_binders push_lift (frec rig) ed c + in + frec true (env,1) m; acc + +(* calcule la liste des arguments implicites *) + +let my_concrete_name avoid names t = function + | Anonymous -> Anonymous, avoid, Anonymous::names + | na -> + let id = Termops.next_name_not_occuring false na avoid names t in + Name id, id::avoid, Name id::names + +let compute_implicits_gen strict contextual 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)) + (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 + 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 v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in + Array.to_list v + | _ -> [] + +let compute_implicits output env t = + let strict = + (not output & !strict_implicit_args) or + (output & !strict_implicit_args_out) in + let contextual = + (not output & !contextual_implicit_args) or + (output & !contextual_implicit_args_out) in + 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 + +type implicit_status = + (* None = Not implicit *) + (identifier * implicit_explanation) option + +type implicits_list = implicit_status list + +let is_status_implicit = function + | None -> false + | _ -> true + +let name_of_implicit = function + | None -> anomaly "Not an implicit argument" + | Some (id,_) -> id + +(* [in_ctx] means we now 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 + +let positions_of_implicits = + let rec aux n = function + [] -> [] + | Some _ :: l -> n :: aux (n+1) l + | None :: l -> aux (n+1) l + in aux 1 + +type strict_flag = bool (* true = strict *) +type contextual_flag = bool (* true = contextual *) + +type implicits = + | Impl_auto of strict_flag * contextual_flag * implicits_list + | Impl_manual of implicits_list + | No_impl + +let auto_implicits env ty = + let impl = + if !implicit_args then + let l = compute_implicits false env ty in + Impl_auto (!strict_implicit_args,!contextual_implicit_args,l) + else + No_impl in + if Options.do_translate () then + impl, + if !implicit_args_out then + (let l = compute_implicits true env ty in + Impl_auto (!strict_implicit_args_out,!contextual_implicit_args_out,l)) + else No_impl + else + impl, impl + +let list_of_implicits = function + | Impl_auto (_,_,l) -> l + | Impl_manual l -> l + | No_impl -> [] + +(*s Constants. *) + +let constants_table = ref KNmap.empty + +let compute_constant_implicits kn = + let env = Global.env () in + let cb = lookup_constant kn env in + auto_implicits env (body_of_type cb.const_type) + +let constant_implicits sp = + try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl + +(*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 inductives_table = ref Indmap.empty + +let constructors_table = ref Constrmap.empty + +let compute_mib_implicits kn = + let env = Global.env () in + let mib = lookup_mind kn env in + let ar = + Array.to_list + (Array.map (* No need to lift, arities contain no de Bruijn *) + (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity)) + mib.mind_packets) in + let env_ar = push_rel_context ar env in + let imps_one_inductive i mip = + let ind = (kn,i) in + ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)), + Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) + mip.mind_user_lc) + in + Array.mapi imps_one_inductive mib.mind_packets + +let inductive_implicits indp = + try Indmap.find indp !inductives_table with Not_found -> No_impl,No_impl + +let constructor_implicits consp = + try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl +(*s Variables. *) + +let var_table = ref Idmap.empty + +let compute_var_implicits id = + let env = Global.env () in + let (_,_,ty) = lookup_named id env in + auto_implicits env ty + +let var_implicits id = + try Idmap.find id !var_table with Not_found -> No_impl,No_impl + +(* Caching implicits *) + +let cache_implicits_decl (r,imps) = + match r with + | VarRef id -> + var_table := Idmap.add id imps !var_table + | ConstRef kn -> + constants_table := KNmap.add kn imps !constants_table + | IndRef indp -> + inductives_table := Indmap.add indp imps !inductives_table; + | ConstructRef consp -> + constructors_table := Constrmap.add consp imps !constructors_table + +let cache_implicits (_,l) = List.iter cache_implicits_decl l + +let subst_implicits_decl subst (r,imps as o) = + let r' = subst_global subst r in if r==r' then o else (r',imps) + +let subst_implicits (_,subst,l) = + list_smartmap (subst_implicits_decl subst) l + +let (in_implicits, _) = + declare_object {(default_object "IMPLICITS") with + cache_function = cache_implicits; + load_function = (fun _ -> cache_implicits); + subst_function = subst_implicits; + classify_function = (fun (_,x) -> Substitute x); + export_function = (fun x -> Some x) } + +(* Implicits of a global reference. *) + +let compute_global_implicits = function + | VarRef id -> compute_var_implicits id + | ConstRef kn -> compute_constant_implicits kn + | IndRef (kn,i) -> + let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + | ConstructRef ((kn,i),j) -> + let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) + +let declare_implicits_gen r = + add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) + +let declare_implicits r = + with_implicits + ((true,!strict_implicit_args,!contextual_implicit_args), + (true,!strict_implicit_args_out,!contextual_implicit_args_out)) + declare_implicits_gen r + +let declare_var_implicits id = + if !implicit_args or !implicit_args_out then + declare_implicits_gen (VarRef id) + +let declare_constant_implicits kn = + if !implicit_args or !implicit_args_out then + declare_implicits_gen (ConstRef kn) + +let declare_mib_implicits kn = + if !implicit_args or !implicit_args_out then + let imps = compute_mib_implicits kn in + let imps = array_map_to_list + (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in + add_anonymous_leaf (in_implicits (List.flatten imps)) + +let implicits_of_global_gen = function + | VarRef id -> var_implicits id + | ConstRef sp -> constant_implicits sp + | IndRef isp -> inductive_implicits isp + | ConstructRef csp -> constructor_implicits csp + +let implicits_of_global r = + let (imp_in,imp_out) = implicits_of_global_gen r in + list_of_implicits imp_in + +let implicits_of_global_out r = + let (imp_in,imp_out) = implicits_of_global_gen r in + list_of_implicits imp_out + +(* Declare manual implicits *) + +(* +let check_range n = function + | loc,ExplByPos i -> + if i<1 or i>n then error ("Bad argument number: "^(string_of_int i)) + | loc,ExplByName id -> +() +*) + +let rec list_remove a = function + | b::l when a = b -> l + | b::l -> b::list_remove a l + | [] -> raise Not_found + +let set_implicit id imp = + Some (id,match imp with None -> Manual | Some imp -> imp) + +let declare_manual_implicits r l = + let t = Global.type_of_global r in + let autoimps = compute_implicits_gen false true (Global.env()) t in + let n = List.length autoimps in + if not (list_distinct l) then + error ("Some parameters are referred more than once"); +(* List.iter (check_range n) l;*) +(* let l = List.sort (-) l in*) + (* 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 (ExplByPos k) l, set_implicit id imp + with Not_found -> + try list_remove (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 -> + 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 + let l = Impl_manual (merge 1 l autoimps) in + let (_,oimp_out) = implicits_of_global_gen r in + let l = l, if !Options.v7_only then oimp_out else l in + add_anonymous_leaf (in_implicits [r,l]) + +(* Tests if declared implicit *) + +let test = function + | No_impl | Impl_manual _ -> false,false,false + | Impl_auto (s,c,_) -> true,s,c + +let test_if_implicit find a = + try let b,c = find a in test b, test c + with Not_found -> (false,false,false),(false,false,false) + +let is_implicit_constant sp = + test_if_implicit (KNmap.find sp) !constants_table + +let is_implicit_inductive_definition indp = + test_if_implicit (Indmap.find (indp,0)) !inductives_table + +let is_implicit_var id = + test_if_implicit (Idmap.find id) !var_table + +(*s Registration as global tables *) + +let init () = + constants_table := KNmap.empty; + inductives_table := Indmap.empty; + constructors_table := Constrmap.empty; + var_table := Idmap.empty + +let freeze () = + (!constants_table, !inductives_table, + !constructors_table, !var_table) + +let unfreeze (ct,it,const,vt) = + constants_table := ct; + inductives_table := it; + constructors_table := const; + var_table := vt + +let _ = + Summary.declare_summary "implicits" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +(* Remark: flags implicit_args, contextual_implicit_args + are synchronized by the general options mechanism - see Vernacentries *) + +let init () = + (* strict_implicit_args_out must be not !Options.v7 + but init is done before parsing *) + strict_implicit_args:=not !Options.v7; + implicit_args_out:=false; + (* strict_implicit_args_out needs to be not !Options.v7 or + Options.do_translate() but init is done before parsing *) + strict_implicit_args_out:=true; + contextual_implicit_args_out:=false + +let freeze () = + (!strict_implicit_args, + !implicit_args_out,!strict_implicit_args_out,!contextual_implicit_args_out) + +let unfreeze (b,d,e,f) = + strict_implicit_args := b; + implicit_args_out := d; + strict_implicit_args_out := e; + contextual_implicit_args_out := f + +let _ = + Summary.declare_summary "implicits-out-options" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = true } diff --git a/library/impargs.mli b/library/impargs.mli new file mode 100644 index 00000000..8db04ee7 --- /dev/null +++ b/library/impargs.mli @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val make_strict_implicit_args : bool -> unit +val make_contextual_implicit_args : bool -> unit + +val is_implicit_args : unit -> bool +val is_strict_implicit_args : unit -> bool +val is_contextual_implicit_args : unit -> bool + +type implicits_flags +val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b + +(*s An [implicits_list] is a list of positions telling which arguments + of a reference can be automatically infered *) +type implicit_status +type implicits_list = implicit_status list + +val is_status_implicit : implicit_status -> bool +val is_inferable_implicit : bool -> int -> implicit_status -> bool +val name_of_implicit : implicit_status -> identifier + +val positions_of_implicits : implicits_list -> int list + +(* Computation of the positions of arguments automatically inferable + for an object of the given type in the given env *) +val compute_implicits : bool -> env -> types -> implicits_list + +(*s Computation of implicits (done using the global environment). *) + +val declare_var_implicits : variable -> unit +val declare_constant_implicits : constant -> unit +val declare_mib_implicits : mutual_inductive -> unit + +val declare_implicits : global_reference -> unit + +(* Manual declaration of which arguments are expected implicit *) +val declare_manual_implicits : global_reference -> + Topconstr.explicitation list -> unit + +(* Get implicit arguments *) +val is_implicit_constant : constant -> implicits_flags +val is_implicit_inductive_definition : mutual_inductive -> implicits_flags +val is_implicit_var : variable -> implicits_flags + +val implicits_of_global : global_reference -> implicits_list + +(* For translator *) +val implicits_of_global_out : global_reference -> implicits_list +val is_implicit_args_out : unit -> bool diff --git a/library/lib.ml b/library/lib.ml new file mode 100644 index 00000000..b9da6dea --- /dev/null +++ b/library/lib.ml @@ -0,0 +1,566 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* f i (make_oname prefix id, obj)) + +let load_objects = iter_objects load_object +let open_objects = iter_objects open_object + +let subst_objects prefix subst seg = + let subst_one = fun (id,obj as node) -> + let obj' = subst_object (make_oname prefix id, subst, obj) in + if obj' == obj then node else + (id, obj') + in + list_smartmap subst_one seg + +let classify_segment seg = + let rec clean ((substl,keepl,anticipl) as acc) = function + | (_,CompilingLibrary _) :: _ | [] -> acc + | ((sp,kn as oname),Leaf o) as node :: stk -> + let id = id_of_label (label kn) in + (match classify_object (oname,o) with + | Dispose -> clean acc stk + | Keep o' -> + clean (substl, (id,o')::keepl, anticipl) stk + | Substitute o' -> + clean ((id,o')::substl, keepl, anticipl) stk + | Anticipate o' -> + clean (substl, keepl, o'::anticipl) stk) + | (oname,ClosedSection _ as item) :: 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" + | (_,FrozenState _) :: stk -> clean acc stk + in + clean ([],[],[]) (List.rev seg) + + +let segment_of_objects prefix = + List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj)) + +(* We keep trace of operations in the stack [lib_stk]. + [path_prefix] is the current path of sections, where sections are stored in + ``correct'' order, the oldest coming first in the list. It may seems + costly, but in practice there is not so many openings and closings of + sections, but on the contrary there are many constructions of section + paths based on the library path. *) + +let initial_prefix = default_library,(initial_path,empty_dirpath) + +let lib_stk = ref ([] : library_segment) + +let comp_name = ref None + +let library_dp () = + match !comp_name with Some m -> m | None -> default_library + +(* [path_prefix] is a pair of absolute dirpath and a pair of current + module path and relative section path *) +let path_prefix = ref initial_prefix + + +let cwd () = fst !path_prefix + +let make_path id = Libnames.make_path (cwd ()) id + + +let current_prefix () = snd !path_prefix + +let make_kn id = + let mp,dir = current_prefix () in + Names.make_kn mp dir (label_of_id id) + + +let make_oname id = make_path id, make_kn id + + +let sections_depth () = + List.length (repr_dirpath (snd (snd !path_prefix))) + +let sections_are_opened () = + match repr_dirpath (snd (snd !path_prefix)) with + [] -> false + | _ -> true + + +let recalc_path_prefix () = + let rec recalc = function + | (sp, OpenedSection (dir,_)) :: _ -> dir + | (sp, OpenedModule (dir,_)) :: _ -> dir + | (sp, OpenedModtype (dir,_)) :: _ -> dir + | (sp, CompilingLibrary dir) :: _ -> dir + | _::l -> recalc l + | [] -> initial_prefix + in + path_prefix := recalc !lib_stk + +let pop_path_prefix () = + let dir,(mp,sec) = !path_prefix in + path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec)) + +let find_entry_p p = + let rec find = function + | [] -> raise Not_found + | ent::l -> if p ent then ent else find l + in + find !lib_stk + +let find_split_p p = + let rec find = function + | [] -> raise Not_found + | ent::l -> if p ent then ent,l else find l + in + find !lib_stk + +let split_lib sp = + 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,[] + 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 + +(* Adding operations. *) + +let add_entry sp node = + lib_stk := (sp,node) :: !lib_stk + +let anonymous_id = + let n = ref 0 in + fun () -> incr n; id_of_string ("_" ^ (string_of_int !n)) + +let add_anonymous_entry node = + let id = anonymous_id () in + let name = make_oname id in + add_entry name node; + name + +let add_absolutely_named_leaf sp obj = + cache_object (sp,obj); + add_entry sp (Leaf obj) + +let add_leaf id obj = + let oname = make_oname id in + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname + +let add_leaves id objs = + let oname = make_oname id in + let add_obj obj = + add_entry oname (Leaf obj); + load_object 1 (oname,obj) + in + List.iter add_obj objs; + oname + +let add_anonymous_leaf obj = + let id = anonymous_id () in + let oname = make_oname id in + cache_object (oname,obj); + add_entry oname (Leaf obj) + +let add_frozen_state () = + let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in () + +(* Modules. *) + +let is_something_opened = function + (_,OpenedSection _) -> true + | (_,OpenedModule _) -> true + | (_,OpenedModtype _) -> true + | _ -> false + +let export_segment seg = + let rec clean acc = function + | (_,CompilingLibrary _) :: _ | [] -> acc + | (oname,Leaf o) as node :: stk -> + (match export_object o with + | None -> clean acc stk + | Some o' -> clean ((oname,Leaf o') :: acc) stk) + | (oname,ClosedSection _ as item) :: stk -> clean (item :: acc) stk + | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedModule _) :: _ -> error "there are still opened modules" + | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,FrozenState _) :: stk -> clean acc stk + in + clean [] seg + + +let start_module id mp nametab = + let dir = extend_dirpath (fst !path_prefix) id in + let prefix = dir,(mp,empty_dirpath) in + let oname = make_path id, make_kn id in + if Nametab.exists_module dir then + errorlabstrm "open_module" (pr_id id ++ str " already exists") ; + add_entry oname (OpenedModule (prefix,nametab)); + path_prefix := prefix; + prefix +(* add_frozen_state () must be called in declaremods *) + +let end_module id = + let oname,nametab = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,nametab) -> + let sp = fst oname in + let id' = basename sp in + if id<>id' then error "this is not the last opened module"; + oname,nametab + | _,OpenedModtype _ -> + error "there are some open module types" + | _,OpenedSection _ -> + error "there are some open sections" + | _ -> assert false + with Not_found -> + error "no opened modules" + in + let (after,_,before) = split_lib oname in + lib_stk := before; + let prefix = !path_prefix in + recalc_path_prefix (); + (* add_frozen_state must be called after processing the module, + because we cannot recache interactive modules *) + (oname, prefix, nametab,after) + +let start_modtype id mp nametab = + let dir = extend_dirpath (fst !path_prefix) id in + let prefix = dir,(mp,empty_dirpath) in + let sp = make_path id in + let name = sp, make_kn id in + if Nametab.exists_cci sp then + errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ; + add_entry name (OpenedModtype (prefix,nametab)); + path_prefix := prefix; + prefix + +let end_modtype id = + let sp,nametab = + try match find_entry_p is_something_opened with + | sp,OpenedModtype (_,nametab) -> + let id' = basename (fst sp) in + if id<>id' then error "this is not the last opened module"; + sp,nametab + | _,OpenedModule _ -> + error "there are some open modules" + | _,OpenedSection _ -> + error "there are some open sections" + | _ -> assert false + with Not_found -> + error "no opened module types" + in + let (after,_,before) = split_lib sp in + lib_stk := before; + let dir = !path_prefix in + recalc_path_prefix (); + (* add_frozen_state must be called after processing the module type. + This is because we cannot recache interactive module types *) + (sp,dir,nametab,after) + + + +let contents_after = function + | None -> !lib_stk + | Some sp -> let (after,_,_) = split_lib sp in after + +(* Modules. *) + +let check_for_comp_unit () = + let is_decl = function (_,FrozenState _) -> false | _ -> true in + try + let _ = find_entry_p is_decl in + error "a module cannot be started after some declarations" + with Not_found -> () + +(* TODO: use check_for_module ? *) +let start_compilation s mp = + if !comp_name <> None then + error "compilation unit is already started"; + if snd (snd (!path_prefix)) <> empty_dirpath then + error "some sections are already opened"; + let prefix = s, (mp, empty_dirpath) in + let _ = add_anonymous_entry (CompilingLibrary prefix) in + comp_name := Some s; + path_prefix := prefix + +let end_compilation dir = + let _ = + try match find_entry_p is_something_opened with + | _, OpenedSection _ -> error "There are some open sections" + | _, OpenedModule _ -> error "There are some open modules" + | _, OpenedModtype _ -> error "There are some open module types" + | _ -> assert false + with + Not_found -> () + in + let module_p = + function (_,CompilingLibrary _) -> true | x -> is_something_opened x + in + let oname = + try match find_entry_p module_p with + (oname, CompilingLibrary prefix) -> oname + | _ -> assert false + with + Not_found -> anomaly "No module declared" + in + let _ = match !comp_name with + | None -> anomaly "There should be a module name..." + | Some m -> + if m <> dir then anomaly + ("The current open module has name "^ (string_of_dirpath m) ^ + " and not " ^ (string_of_dirpath m)); + in + let (after,_,before) = split_lib oname in + comp_name := None; + !path_prefix,after + +(* Returns true if we are inside an opened module type *) +let is_modtype () = + let opened_p = function + | _, OpenedModtype _ -> true + | _ -> false + in + try + let _ = find_entry_p opened_p in true + with + Not_found -> false + +(* Returns true if we are inside an opened module *) +let is_module () = + let opened_p = function + | _, OpenedModule _ -> true + | _ -> false + in + try + let _ = find_entry_p opened_p in true + with + Not_found -> false + + +(* Returns the most recent OpenedThing node *) +let what_is_opened () = find_entry_p is_something_opened + +(* XML output hooks *) +let xml_open_section = ref (fun id -> ()) +let xml_close_section = ref (fun id -> ()) + +let set_xml_open_section f = xml_open_section := f +let set_xml_close_section f = xml_close_section := f + +(* Sections. *) + +let open_section id = + let olddir,(mp,oldsec) = !path_prefix in + let dir = extend_dirpath olddir id in + let prefix = dir, (mp, extend_dirpath oldsec id) in + let name = make_path id, make_kn id (* this makes little sense however *) in + if Nametab.exists_section dir then + errorlabstrm "open_section" (pr_id id ++ str " already exists"); + let sum = freeze_summaries() in + add_entry name (OpenedSection (prefix, sum)); + (*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; + prefix + + +(* Restore lib_stk and summaries as before the section opening, and + add a ClosedSection object. *) +let close_section ~export id = + let oname,fs = + try match find_entry_p is_something_opened with + | oname,OpenedSection (_,fs) -> + if id <> basename (fst oname) then + error "this is not the last opened section"; + (oname,fs) + | _ -> assert false + with Not_found -> + error "no opened section" + in + let (after,_,before) = split_lib oname in + lib_stk := before; + let prefix = !path_prefix in + pop_path_prefix (); + let closed_sec = + ClosedSection (export, (fst prefix), export_segment after) + in + let name = make_path id, make_kn id in + add_entry name closed_sec; + if !Options.xml_export then !xml_close_section id; + (prefix, after, fs) + +(* Backtracking. *) + +let recache_decl = function + | (sp, Leaf o) -> cache_object (sp,o) + | _ -> () + + +let recache_context ctx = + List.iter recache_decl ctx + +let is_frozen_state = function (_,FrozenState _) -> true | _ -> false + +let reset_to sp = + let (_,_,before) = split_lib sp 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 reset_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,"reset_name",pr_id id ++ str ": no such entry") + in + reset_to sp + +let is_mod_node = function + | OpenedModule _ | OpenedModtype _ | OpenedSection _ + | ClosedSection _ -> true + | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + | _ -> false + +(* Reset on a module or section name in order to bypass constants with + the same name *) + +let reset_mod (loc,id) = + let (ent,before) = + try + find_split_p (fun (sp,node) -> + let (_,spi) = repr_path (fst sp) in id = spi + && is_mod_node node) + 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 point_obj = + let (f,_) = declare_object {(default_object "DOT") with + classify_function = (fun _ -> Dispose)} in + f() + +let mark_end_of_command () = + match !lib_stk with + (_,Leaf o)::_ when object_tag o = "DOT" -> () + | _ -> add_anonymous_leaf point_obj + +let rec back_stk n stk = + match stk with + (sp,Leaf o)::tail when object_tag o = "DOT" -> + if n=0 then sp else back_stk (n-1) tail + | _::tail -> back_stk n tail + | [] -> error "Reached begin of command history" + +let back n = reset_to (back_stk n !lib_stk) + +(* State and initialization. *) + +type frozen = dir_path option * library_segment + +let freeze () = (!comp_name, !lib_stk) + +let unfreeze (mn,stk) = + comp_name := mn; + lib_stk := stk; + recalc_path_prefix () + +let init () = + lib_stk := []; + add_frozen_state (); + comp_name := None; + path_prefix := initial_prefix; + init_summaries() + +(* Initial state. *) + +let initial_state = ref None + +let declare_initial_state () = + let name = add_anonymous_entry (FrozenState (freeze_summaries())) in + initial_state := Some name + +let reset_initial () = + match !initial_state with + | None -> + error "Resetting to the initial state is possible only interactively" + | Some sp -> + begin match split_lib sp with + | (_,[_,FrozenState fs as hd],before) -> + lib_stk := hd::before; + recalc_path_prefix (); + unfreeze_summaries fs + | _ -> assert false + end + + +(* Misc *) + +let library_part ref = + let sp = Nametab.sp_of_global ref in + let dir,_ = repr_path sp in + match ref with + | VarRef id -> + anomaly "TODO"; + extract_dirpath_prefix (sections_depth ()) (cwd ()) + | _ -> + if is_dirpath_prefix_of dir (cwd ()) then + (* Not yet (fully) discharged *) + extract_dirpath_prefix (sections_depth ()) (cwd ()) + else + (* Theorem/Lemma outside its outer section of definition *) + dir diff --git a/library/lib.mli b/library/lib.mli new file mode 100644 index 00000000..8981754e --- /dev/null +++ b/library/lib.mli @@ -0,0 +1,156 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* object_prefix -> lib_objects -> unit +val load_objects : int -> object_prefix -> lib_objects -> unit +val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects + +(* [classify_segment seg] verifies that there are no OpenedThings, + clears ClosedSections and FrozenStates and divides Leafs according + to their answers to the [classify_object] function in three groups: + [Substitute], [Keep], [Anticipate] respectively. The order of each + returned list is the same as in the input list. *) +val classify_segment : + library_segment -> lib_objects * lib_objects * obj list + +(* [segment_of_objects prefix objs] forms a list of Leafs *) +val segment_of_objects : + object_prefix -> lib_objects -> library_segment + + +(*s Adding operations (which call the [cache] method, and getting the + current list of operations (most recent ones coming first). *) + +val add_leaf : identifier -> obj -> object_name +val add_absolutely_named_leaf : object_name -> obj -> unit +val add_anonymous_leaf : obj -> unit + +(* this operation adds all objects with the same name and calls load_object + for each of them *) +val add_leaves : identifier -> obj list -> object_name + +val add_frozen_state : unit -> unit +val mark_end_of_command : unit -> unit + + +(*s The function [contents_after] returns the current library segment, + starting from a given section path. If not given, the entire segment + is returned. *) + +val contents_after : object_name option -> library_segment + +(*s Functions relative to current path *) + +(* User-side names *) +val cwd : unit -> dir_path +val make_path : identifier -> section_path + +(* Kernel-side names *) +val current_prefix : unit -> module_path * dir_path +val make_kn : identifier -> kernel_name + +(* Are we inside an opened section *) +val sections_are_opened : unit -> bool +val sections_depth : unit -> int + +(* Are we inside an opened module type *) +val is_modtype : unit -> bool +val is_module : unit -> bool + + +(* Returns the most recent OpenedThing node *) +val what_is_opened : unit -> object_name * node + + +(*s Modules and module types *) + +val start_module : + module_ident -> module_path -> Summary.frozen -> object_prefix +val end_module : module_ident + -> object_name * object_prefix * Summary.frozen * library_segment + +val start_modtype : + module_ident -> module_path -> Summary.frozen -> object_prefix +val end_modtype : module_ident + -> object_name * object_prefix * Summary.frozen * library_segment +(* Lib.add_frozen_state must be called after each of the above functions *) + +(*s Compilation units *) + +val start_compilation : dir_path -> module_path -> unit +val end_compilation : dir_path -> object_prefix * library_segment + +(* The function [library_dp] returns the [dir_path] of the current + compiling library (or [default_library]) *) +val library_dp : unit -> dir_path + +(* Extract the library part of a name even if in a section *) +val library_part : global_reference -> dir_path + +(*s Sections *) + +val open_section : identifier -> object_prefix + +val close_section : export:bool -> identifier -> + object_prefix * library_segment * Summary.frozen + +(*s Backtracking (undo). *) + +val reset_to : object_name -> unit +val reset_name : identifier located -> unit +val reset_mod : identifier located -> unit + +(* [back n] resets to the place corresponding to the $n$-th call of + [mark_end_of_command] (counting backwards) *) +val back : int -> unit + +(*s We can get and set the state of the operations (used in [States]). *) + +type frozen + +val freeze : unit -> frozen +val unfreeze : frozen -> unit + +val init : unit -> unit + +val declare_initial_state : unit -> unit +val reset_initial : unit -> unit + + +(* XML output hooks *) +val set_xml_open_section : (identifier -> unit) -> unit +val set_xml_close_section : (identifier -> unit) -> unit diff --git a/library/libnames.ml b/library/libnames.ml new file mode 100644 index 00000000..16f5a917 --- /dev/null +++ b/library/libnames.ml @@ -0,0 +1,269 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ref + | ConstRef kn -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstRef kn' + | IndRef (kn,i) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + IndRef(kn',i) + | ConstructRef ((kn,i),j) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstructRef ((kn',i),j) + +let reference_of_constr c = match kind_of_term c with + | Const sp -> ConstRef sp + | Ind ind_sp -> IndRef ind_sp + | Construct cstr_cp -> ConstructRef cstr_cp + | Var id -> VarRef id + | _ -> raise Not_found + +let constr_of_reference = function + | VarRef id -> mkVar id + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkConstruct sp + | IndRef sp -> mkInd sp + +module RefOrdered = + struct + type t = global_reference + let compare = Pervasives.compare + end + +module Refset = Set.Make(RefOrdered) +module Refmap = Map.Make(RefOrdered) + +module InductiveOrdered = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then compare spx spy else c +end + +module Indmap = Map.Make(InductiveOrdered) + +let inductives_table = ref Indmap.empty + +module ConstructorOrdered = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c +end + +module Constrmap = Map.Make(ConstructorOrdered) + +(**********************************************) + +let pr_dirpath sl = (str (string_of_dirpath sl)) + +(*s Operations on dirpaths *) + +(* Pop the last n module idents *) +let extract_dirpath_prefix n dir = + make_dirpath (list_skipn n (repr_dirpath dir)) + +let dirpath_prefix p = match repr_dirpath p with + | [] -> anomaly "dirpath_prefix: empty dirpath" + | _::l -> make_dirpath l + +let is_dirpath_prefix_of d1 d2 = + list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + +(* To know how qualified a name should be to be understood in the current env*) +let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) + +let split_dirpath d = + let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) + +let extend_dirpath p id = make_dirpath (id :: repr_dirpath p) + + +(* +let path_of_constructor env ((sp,tyi),ind) = + let mib = Environ.lookup_mind sp env in + let mip = mib.mind_packets.(tyi) in + let (pa,_) = repr_path sp in + Names.make_path pa (mip.mind_consnames.(ind-1)) + +let path_of_inductive env (sp,tyi) = + if tyi = 0 then sp + else + let mib = Environ.lookup_mind sp env in + let mip = mib.mind_packets.(tyi) in + let (pa,_) = repr_path sp in + Names.make_path pa (mip.mind_typename) +*) +(* parsing *) +let parse_dir s = + let len = String.length s in + let rec decoupe_dirs dirs n = + if n>=len then dirs else + let pos = + try + String.index_from s n '.' + with Not_found -> len + in + let dir = String.sub s n (pos-n) in + decoupe_dirs ((id_of_string dir)::dirs) (pos+1) + in + decoupe_dirs [] 0 + +let dirpath_of_string s = + match parse_dir s with + [] -> invalid_arg "dirpath_of_string" + | dir -> make_dirpath dir + +module Dirset = Set.Make(struct type t = dir_path let compare = compare end) +module Dirmap = Map.Make(struct type t = dir_path let compare = compare end) + +(*s Section paths are absolute names *) + +type section_path = { + dirpath : dir_path ; + basename : identifier } + +let make_path pa id = { dirpath = pa; basename = id } +let repr_path { dirpath = pa; basename = id } = (pa,id) + +(* parsing and printing of section paths *) +let string_of_path sp = + let (sl,id) = repr_path sp in + if repr_dirpath sl = [] then string_of_id id + else (string_of_dirpath sl) ^ "." ^ (string_of_id id) + +let sp_ord sp1 sp2 = + let (p1,id1) = repr_path sp1 + and (p2,id2) = repr_path sp2 in + let p_bit = compare p1 p2 in + if p_bit = 0 then id_ord id1 id2 else p_bit + +module SpOrdered = + struct + type t = section_path + let compare = sp_ord + end + +module Spset = Set.Make(SpOrdered) +module Sppred = Predicate.Make(SpOrdered) +module Spmap = Map.Make(SpOrdered) + +let dirpath sp = let (p,_) = repr_path sp in p +let basename sp = let (_,id) = repr_path sp in id + +let path_of_string s = + try + let dir, id = split_dirpath (dirpath_of_string s) in + make_path dir id + with + | Invalid_argument _ -> invalid_arg "path_of_string" + +let pr_sp sp = str (string_of_path sp) + +let restrict_path n sp = + let dir, s = repr_path sp in + let dir' = list_firstn n (repr_dirpath dir) in + make_path (make_dirpath dir') s + +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of kernel_name + +let subst_ext subst glref = match glref with + | TrueGlobal ref -> + let ref' = subst_global subst ref in + if ref' == ref then glref else + TrueGlobal ref' + | SyntacticDef kn -> + let kn' = subst_kn subst kn in + if kn' == kn then glref else + SyntacticDef kn' + +let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) + +let decode_kn kn = + let mp,sec_dir,l = repr_kn kn in + match mp,(repr_dirpath sec_dir) with + MPfile dir,[] -> (dir,id_of_label l) + | _ , [] -> anomaly "MPfile expected!" + | _ -> anomaly "Section part should be empty!" + +(*s qualified names *) +type qualid = section_path + +let make_qualid = make_path +let repr_qualid = repr_path + +let string_of_qualid = string_of_path +let pr_qualid = pr_sp + +let qualid_of_string = path_of_string + +let qualid_of_sp sp = sp +let make_short_qualid id = make_qualid empty_dirpath id +let qualid_of_dirpath dir = + let (l,a) = split_dirpath dir in + make_qualid l a + +type object_name = section_path * kernel_name + +type object_prefix = dir_path * (module_path * dir_path) + +let make_oname (dirpath,(mp,dir)) id = + make_path dirpath id, make_kn mp dir (label_of_id id) + +(* to this type are mapped dir_path's in the nametab *) +type global_dir_reference = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + | DirClosedSection of dir_path + (* this won't last long I hope! *) + +(* | ModRef mp -> + let mp' = subst_modpath subst mp in if mp==mp' then ref else + ModRef mp' + | ModTypeRef kn -> + let kn' = subst_kernel_name subst kn in if kn==kn' then ref else + ModTypeRef kn' +*) + +type reference = + | Qualid of qualid located + | Ident of identifier located + +let qualid_of_reference = function + | Qualid (loc,qid) -> loc, qid + | Ident (loc,id) -> loc, make_short_qualid id + +let string_of_reference = function + | Qualid (loc,qid) -> string_of_qualid qid + | Ident (loc,id) -> string_of_id id + +let pr_reference = function + | Qualid (_,qid) -> pr_qualid qid + | Ident (_,id) -> pr_id id + +let loc_of_reference = function + | Qualid (loc,qid) -> loc + | Ident (loc,id) -> loc diff --git a/library/libnames.mli b/library/libnames.mli new file mode 100644 index 00000000..6f05333c --- /dev/null +++ b/library/libnames.mli @@ -0,0 +1,140 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference -> global_reference + +(* Turn a global reference into a construction *) +val constr_of_reference : global_reference -> constr + +(* Turn a construction denoting a global into a reference; + raise [Not_found] if not a global *) +val reference_of_constr : constr -> global_reference + +module Refset : Set.S with type elt = global_reference +module Refmap : Map.S with type key = global_reference + +module Indmap : Map.S with type key = inductive +module Constrmap : Map.S with type key = constructor + +(*s Dirpaths *) +val pr_dirpath : dir_path -> Pp.std_ppcmds + +val dirpath_of_string : string -> dir_path + +(* Give the immediate prefix of a [dir_path] *) +val dirpath_prefix : dir_path -> dir_path + +(* Give the immediate prefix and basename of a [dir_path] *) +val split_dirpath : dir_path -> dir_path * identifier + +val extend_dirpath : dir_path -> module_ident -> dir_path +val add_dirpath_prefix : module_ident -> dir_path -> dir_path + +val extract_dirpath_prefix : int -> dir_path -> dir_path +val is_dirpath_prefix_of : dir_path -> dir_path -> bool + +module Dirset : Set.S with type elt = dir_path +module Dirmap : Map.S with type key = dir_path + +(*s Section paths are {\em absolute} names *) +type section_path + +(* Constructors of [section_path] *) +val make_path : dir_path -> identifier -> section_path + +(* Destructors of [section_path] *) +val repr_path : section_path -> dir_path * identifier +val dirpath : section_path -> dir_path +val basename : section_path -> identifier + +(* Parsing and printing of section path as ["coq_root.module.id"] *) +val path_of_string : string -> section_path +val string_of_path : section_path -> string +val pr_sp : section_path -> std_ppcmds + +module Sppred : Predicate.S with type elt = section_path +module Spmap : Map.S with type key = section_path + +val restrict_path : int -> section_path -> section_path + +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of kernel_name + +val subst_ext : + substitution -> extended_global_reference -> extended_global_reference + +(*s Temporary function to brutally form kernel names from section paths *) + +val encode_kn : dir_path -> identifier -> kernel_name +val decode_kn : kernel_name -> dir_path * identifier + + +(*s A [qualid] is a partially qualified ident; it includes fully + qualified names (= absolute names) and all intermediate partial + qualifications of absolute names, including single identifiers *) +type qualid + +val make_qualid : dir_path -> identifier -> qualid +val repr_qualid : qualid -> dir_path * identifier + +val string_of_qualid : qualid -> string +val pr_qualid : qualid -> std_ppcmds + +val qualid_of_string : string -> qualid + +(* Turns an absolute name into a qualified name denoting the same name *) +val qualid_of_sp : section_path -> qualid + +val qualid_of_dirpath : dir_path -> qualid + +val make_short_qualid : identifier -> qualid + +(* Both names are passed to objects: a "semantic" kernel_name, which + can be substituted and a "syntactic" section_path which can be printed +*) + +type object_name = section_path * kernel_name + +type object_prefix = dir_path * (module_path * dir_path) + +val make_oname : object_prefix -> identifier -> object_name + +(* to this type are mapped dir_path's in the nametab *) +type global_dir_reference = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + | DirClosedSection of dir_path + (* this won't last long I hope! *) + +type reference = + | Qualid of qualid located + | Ident of identifier located + +val qualid_of_reference : reference -> qualid located +val string_of_reference : reference -> string +val pr_reference : reference -> std_ppcmds +val loc_of_reference : reference -> loc diff --git a/library/libobject.ml b/library/libobject.ml new file mode 100644 index 00000000..2e531e05 --- /dev/null +++ b/library/libobject.ml @@ -0,0 +1,157 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : object_name * 'a -> 'a substitutivity; + subst_function : object_name * substitution * 'a -> 'a; + export_function : 'a -> 'a option } + +let yell s = anomaly s + +let default_object s = { + object_name = s; + cache_function = (fun _ -> ()); + load_function = (fun _ _ -> ()); + open_function = (fun _ _ -> ()); + subst_function = (fun _ -> + yell ("The object "^s^" does not know how to substitute!")); + classify_function = (fun (_,obj) -> Keep obj); + export_function = (fun _ -> None)} + + +(* The suggested object declaration is the following: + + declare_object { (default_object "MY OBJECT") with + cache_function = fun (sp,a) -> Mytbl.add sp a} + + and the listed functions are only those which definitions accually + differ from the default. + + This helps introducing new functions in objects. +*) + +let ident_subst_function (_,_,a) = a + +type obj = Dyn.t (* persistent dynamic objects *) + +type dynamic_object_declaration = { + dyn_cache_function : object_name * obj -> unit; + dyn_load_function : int -> object_name * obj -> unit; + dyn_open_function : int -> object_name * obj -> unit; + dyn_subst_function : object_name * substitution * obj -> obj; + dyn_classify_function : object_name * obj -> obj substitutivity; + dyn_export_function : obj -> obj option } + +let object_tag lobj = Dyn.tag lobj + +let cache_tab = + (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + +let declare_object odecl = + let na = odecl.object_name in + let (infun,outfun) = Dyn.create na in + let cacher (oname,lobj) = + if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the cachefun" + and loader i (oname,lobj) = + if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the loadfun" + and opener i (oname,lobj) = + if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the openfun" + and substituter (oname,sub,lobj) = + if Dyn.tag lobj = na then + infun (odecl.subst_function (oname,sub,outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the substfun" + and classifier (spopt,lobj) = + if Dyn.tag lobj = na then + match odecl.classify_function (spopt,outfun lobj) with + | Dispose -> Dispose + | Substitute obj -> Substitute (infun obj) + | Keep obj -> Keep (infun obj) + | Anticipate (obj) -> Anticipate (infun obj) + else + anomaly "somehow we got the wrong dynamic object in the classifyfun" + and exporter lobj = + if Dyn.tag lobj = na then + option_app infun (odecl.export_function (outfun lobj)) + else + anomaly "somehow we got the wrong dynamic object in the exportfun" + + in + Hashtbl.add cache_tab na { dyn_cache_function = cacher; + dyn_load_function = loader; + dyn_open_function = opener; + dyn_subst_function = substituter; + dyn_classify_function = classifier; + dyn_export_function = exporter }; + (infun,outfun) + +(* this function describes how the cache, load, open, and export functions + are triggered. In relaxed mode, this function just return a meaningless + value instead of raising an exception when they fail. *) + +let apply_dyn_fun deflt f lobj = + let tag = object_tag lobj in + try + let dodecl = + try + Hashtbl.find cache_tab tag + with Not_found -> + if !relax_flag then + failwith "local to_apply_dyn_fun" + else + anomaly + ("Cannot find library functions for an object with tag "^tag) in + f dodecl + with + Failure "local to_apply_dyn_fun" -> deflt;; + +let cache_object ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj + +let load_object i ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj + +let open_object i ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj + +let subst_object ((_,_,lobj) as node) = + apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj + +let classify_object ((_,lobj) as node) = + apply_dyn_fun Dispose (fun d -> d.dyn_classify_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 new file mode 100644 index 00000000..8a3811e1 --- /dev/null +++ b/library/libobject.mli @@ -0,0 +1,105 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : object_name * 'a -> 'a substitutivity; + subst_function : object_name * substitution * 'a -> 'a; + export_function : 'a -> 'a option } + +(* The default object is a "Keep" object with empty methods. + Object creators are advised to use the construction + [{(default_object "MY_OBJECT") with + cache_function = ... + }] + and specify only these functions which are not empty/meaningless + +*) + +val default_object : string -> 'a object_declaration + +(* the identity substitution function *) +val ident_subst_function : object_name * substitution * 'a -> 'a + +(*s Given an object declaration, the function [declare_object] + will hand back two functions, the "injection" and "projection" + functions for dynamically typed library-objects. *) + +type obj + +val declare_object : + 'a object_declaration -> ('a -> obj) * (obj -> 'a) + +val object_tag : obj -> string + +val cache_object : object_name * obj -> unit +val load_object : int -> object_name * obj -> unit +val open_object : int -> object_name * obj -> unit +val subst_object : object_name * substitution * obj -> obj +val classify_object : object_name * obj -> obj substitutivity +val export_object : obj -> obj option +val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml new file mode 100644 index 00000000..0477a8f3 --- /dev/null +++ b/library/library.ml @@ -0,0 +1,704 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + + +let find_logical_path phys_dir = + let phys_dir = canonical_path_name phys_dir in + match list_filter2 (fun p d -> p = phys_dir) !load_path with + | _,[dir] -> dir + | _,[] -> Nameops.default_root_prefix + | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + +let remove_path dir = + load_path := list_filter2 (fun p d -> p <> dir) !load_path + +let add_load_path_entry (phys_path,coq_path) = + let phys_path = canonical_path_name phys_path in + match list_filter2 (fun p d -> p = phys_path) !load_path with + | _,[dir] -> + if coq_path <> dir + (* If this is not the default -I . to coqtop *) + && not + (phys_path = canonical_path_name Filename.current_dir_name + && coq_path = Nameops.default_root_prefix) + then + 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 ()); + remove_path phys_path; + load_path := (phys_path::fst !load_path, coq_path::snd !load_path) + end + | _,[] -> + load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path) + | _ -> anomaly ("Two logical paths are associated to "^phys_path) + +let physical_paths (dp,lp) = dp + +let load_path_of_logical_path dir = + fst (list_filter2 (fun p d -> d = dir) !load_path) + +let get_full_load_path () = List.combine (fst !load_path) (snd !load_path) + +(************************************************************************) +(*s Modules on disk contain the following informations (after the magic + number, and before the digest). *) + +type compilation_unit_name = dir_path + +type library_disk = { + md_name : compilation_unit_name; + md_compiled : compiled_library; + md_objects : library_objects; + md_deps : (compilation_unit_name * Digest.t) list; + md_imports : compilation_unit_name list } + +(*s Modules loaded in memory contain the following informations. They are + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_filename : System.physical_path; + library_compiled : compiled_library; + library_objects : library_objects; + library_deps : (compilation_unit_name * Digest.t) list; + library_imports : compilation_unit_name list; + library_digest : Digest.t } + +module CompilingLibraryOrdered = + struct + type t = dir_path + let compare d1 d2 = + Pervasives.compare + (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + end + +module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered) + +(* This is a map from names to libraries *) +let libraries_table = ref CompilingLibraryMap.empty + +(* These are the _ordered_ lists of loaded, imported and exported libraries *) +let libraries_loaded_list = ref [] +let libraries_imports_list = ref [] +let libraries_exports_list = ref [] + +let freeze () = + !libraries_table, + !libraries_loaded_list, + !libraries_imports_list, + !libraries_exports_list + +let unfreeze (mt,mo,mi,me) = + libraries_table := mt; + libraries_loaded_list := mo; + libraries_imports_list := mi; + libraries_exports_list := me + +let init () = + libraries_table := CompilingLibraryMap.empty; + libraries_loaded_list := []; + libraries_imports_list := []; + libraries_exports_list := [] + +let _ = + Summary.declare_summary "MODULES" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +let find_library s = + try + CompilingLibraryMap.find s !libraries_table + with Not_found -> + error ("Unknown library " ^ (string_of_dirpath s)) + +let library_full_filename m = (find_library m).library_filename + +let library_is_loaded dir = + try let _ = CompilingLibraryMap.find dir !libraries_table in true + with Not_found -> false + +let library_is_opened dir = + List.exists (fun m -> m.library_name = dir) !libraries_imports_list + +let library_is_exported dir = + List.exists (fun m -> m.library_name = dir) !libraries_exports_list + +let loaded_libraries () = + List.map (fun m -> m.library_name) !libraries_loaded_list + +let opened_libraries () = + List.map (fun m -> m.library_name) !libraries_imports_list + + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) + +let register_loaded_library m = + let rec aux = function + | [] -> [m] + | m'::_ as l when m'.library_name = m.library_name -> l + | m'::l' -> m' :: aux l' in + libraries_loaded_list := aux !libraries_loaded_list; + libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table + + (* ... while if a library is imported/exported several time, then + only the last occurrence is really needed - though the imported + list may differ from the exported list (consider the sequence + Export A; Export B; Import A which results in A;B for exports but + in B;A for imports) *) + +let rec remember_last_of_each l m = + match l with + | [] -> [m] + | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m + | m'::l' -> m' :: remember_last_of_each l' m + +let register_open_library export m = + libraries_imports_list := remember_last_of_each !libraries_imports_list m; + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +(************************************************************************) +(*s Opening libraries *) + +(*s [open_library s] opens a library. The library [s] and all + libraries needed by [s] are assumed to be already loaded. When + opening [s] we recursively open all the libraries needed by [s] + and tagged [exported]. *) + +let eq_lib_name m1 m2 = m1.library_name = m2.library_name + +let open_library export explicit_libs m = + if + (* Only libraries indirectly to open are not reopen *) + (* Libraries explicitly mentionned by the user are always reopen *) + List.exists (eq_lib_name m) explicit_libs + or not (library_is_opened m.library_name) + then begin + register_open_library export m; + Declaremods.really_import_module (MPfile m.library_name) + end + else + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +let open_libraries export modl = + let to_open_list = + List.fold_left + (fun l m -> + let subimport = + List.fold_left + (fun l m -> remember_last_of_each l (find_library m)) + l m.library_imports + in remember_last_of_each subimport m) + [] modl in + List.iter (open_library export modl) to_open_list + + +(**********************************************************************) +(* import and export - synchronous operations*) + +let cache_import (_,(dir,export)) = + open_libraries export [find_library dir] + +let open_import i (_,(dir,_) as obj) = + if i=1 then + (* even if the library is already imported, we re-import it *) + (* if not (library_is_opened dir) then *) + cache_import obj + +let subst_import (_,_,o) = o + +let export_import o = Some o + +let classify_import (_,(_,export as obj)) = + if export then Substitute obj else Dispose + + +let (in_import, out_import) = + declare_object {(default_object "IMPORT LIBRARY") with + cache_function = cache_import; + open_function = open_import; + subst_function = subst_import; + classify_function = classify_import } + + +(************************************************************************) +(*s Loading from disk to cache (preparation phase) *) + +let vo_magic_number7 = 07992 (* V8.0 final old syntax *) +let vo_magic_number8 = 08002 (* V8.0 final new syntax *) + +let (raw_extern_library7, raw_intern_library7) = + System.raw_extern_intern vo_magic_number7 ".vo" + +let (raw_extern_library8, raw_intern_library8) = + System.raw_extern_intern vo_magic_number8 ".vo" + +let raw_intern_library a = + if !Options.v7 then + try raw_intern_library7 a + with System.Bad_magic_number fname -> + let _= raw_intern_library8 a in + error "Inconsistent compiled files: you probably want to use Coq in new syntax and remove the option -v7 or -translate" + else + try raw_intern_library8 a + with System.Bad_magic_number fname -> + let _= raw_intern_library7 a in + error "Inconsistent compiled files: you probably want to use Coq in old syntax by setting options -v7 or -translate" + +let raw_extern_library = + if !Options.v7 then raw_extern_library7 else raw_extern_library8 + +(* cache for loaded libraries *) +let compunit_cache = ref CompilingLibraryMap.empty + +let _ = + Summary.declare_summary "MODULES-CACHE" + { Summary.freeze_function = (fun () -> !compunit_cache); + Summary.unfreeze_function = (fun cu -> compunit_cache := cu); + Summary.init_function = + (fun () -> compunit_cache := CompilingLibraryMap.empty); + Summary.survive_module = true; + Summary.survive_section = true } + +(*s [load_library s] loads the library [s] from the disk, and [find_library s] + returns the library of name [s], loading it if necessary. + The boolean [doexp] specifies if we open the libraries which are declared + exported in the dependencies (it is [true] at the highest level; + then same value as for caller is reused in recursive loadings). *) + +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +let locate_absolute_library dir = + (* Look if loaded in current environment *) + try + let m = CompilingLibraryMap.find dir !libraries_table in + (dir, m.library_filename) + with Not_found -> + (* Look if in loadpath *) + try + let pref, base = split_dirpath dir in + let loadpath = load_path_of_logical_path pref in + if loadpath = [] then raise LibUnmappedDir; + let name = (string_of_id base)^".vo" in + let _, file = System.where_in_path loadpath name in + (dir, file) + with Not_found -> raise LibNotFound + +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." ++ + spc () ++ str"It is corrupted" ++ spc () ++ + str"or was compiled with another version of Coq.") + +let lighten_library m = + if !Options.dont_load_proofs then lighten_library m else m + +let mk_library md f 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; + library_imports = md.md_imports; + library_digest = digest } + +let intern_from_file f = + let ch = with_magic_number_check raw_intern_library f in + let md = System.marshal_in ch in + let digest = System.marshal_in ch in + close_in ch; + mk_library md f digest + +let rec intern_library (dir, f) = + try + (* Look if in the current logical environment *) + CompilingLibraryMap.find dir !libraries_table + with Not_found -> + try + (* Look if already loaded in cache and consequently its dependencies *) + CompilingLibraryMap.find dir !compunit_cache + with Not_found -> + (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let m = intern_from_file f in + if dir <> m.library_name then + errorlabstrm "load_physical_library" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ + spc() ++ pr_dirpath dir); + intern_and_cache_library dir m + +and intern_and_cache_library dir m = + compunit_cache := CompilingLibraryMap.add dir m !compunit_cache; + try + List.iter (intern_mandatory_library dir) m.library_deps; + m + with e -> + compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; + raise e + +and intern_mandatory_library caller (dir,d) = + let m = intern_absolute_library_from dir in + if d <> m.library_digest then + error ("compiled library "^(string_of_dirpath caller)^ + " makes inconsistent assumptions over library " + ^(string_of_dirpath dir)) + +and intern_absolute_library_from dir = + try + intern_library (locate_absolute_library dir) + with + | LibUnmappedDir -> + let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in + errorlabstrm "load_absolute_library_from" + (str ("Cannot load "^dir^":") ++ spc () ++ + str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) + | LibNotFound -> + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_dirpath dir ++ str" in loadpath") + | e -> raise e + +let rec_intern_library mref = let _ = intern_library mref in () + +let check_library_short_name f dir = function + | Some id when id <> snd (split_dirpath dir) -> + errorlabstrm "check_library_short_name" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ + pr_id id) + | _ -> () + +let rec_intern_by_filename_only id f = + let m = intern_from_file f 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' = CompilingLibraryMap.find m.library_name !libraries_table 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 -> + let m = intern_and_cache_library m.library_name m in + m.library_name + +let locate_qualified_library qid = + (* Look if loaded in current environment *) + try + let dir = Nametab.full_name_module qid in + (LibLoaded, dir, library_full_filename dir) + with Not_found -> + (* Look if in loadpath *) + try + let dir, base = repr_qualid qid in + let loadpath = + if repr_dirpath dir = [] then get_load_path () + else + (* we assume dir is an absolute dirpath *) + load_path_of_logical_path dir + in + if loadpath = [] then raise LibUnmappedDir; + let name = (string_of_id base)^".vo" in + let path, file = System.where_in_path loadpath name in + (LibInPath, extend_dirpath (find_logical_path path) base, file) + with Not_found -> raise LibNotFound + +let rec_intern_qualified_library (loc,qid) = + try + let (_,dir,f) = locate_qualified_library qid in + rec_intern_library (dir,f); + dir + with + | LibUnmappedDir -> + let prefix, id = repr_qualid qid in + user_err_loc (loc, "rec_intern_qualified_library", + str ("Cannot load "^(string_of_id id)^":") ++ spc () ++ + str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ + fnl ()) + | LibNotFound -> + user_err_loc (loc, "rec_intern_qualified_library", + str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") + +let rec_intern_library_from_file idopt f = + (* A name is specified, we have to check it contains library id *) + let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in + rec_intern_by_filename_only idopt f + +(**********************************************************************) +(*s [require_library] loads and opens a library. This is a synchronized + operation. It is performed as follows: + + preparation phase: (functions require_library* ) the library and its + dependencies are read from to disk to the compunit_cache + (using intern_* ) + + execution phase: (through add_leaf and cache_require) + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, + which recursively loads its dependencies) + + + The [read_library] operation is very similar, but does not "open" + the library +*) + +type library_reference = dir_path list * bool option + +let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) + +let rec load_library dir = + try + (* Look if loaded in current env (and consequently its dependencies) *) + CompilingLibraryMap.find dir !libraries_table + with Not_found -> + (* [dir] is an absolute name matching [f] which must be in loadpath *) + let m = + try CompilingLibraryMap.find dir !compunit_cache + with Not_found -> + anomaly ((string_of_dirpath dir)^" should be in cache") + in + List.iter (fun (dir,_) -> ignore (load_library dir)) m.library_deps; + Declaremods.register_library + m.library_name + m.library_compiled + m.library_objects + m.library_digest; + register_loaded_library m; + m + +let cache_require (_,(modl,export)) = + let ml = list_map_left load_library modl in + match export with + | None -> () + | Some export -> open_libraries export ml + +let load_require _ (_,(modl,_)) = + ignore(list_map_left load_library modl) + + (* keeps the require marker for closed section replay but removes + OS dependent fields from .vo files for cross-platform compatibility *) +let export_require (l,e) = Some (l,e) + +let (in_require, out_require) = + declare_object {(default_object "REQUIRE") with + cache_function = cache_require; + load_function = load_require; + export_function = export_require; + classify_function = (fun (_,o) -> Anticipate o) } + +let xml_require = ref (fun d -> ()) +let set_xml_require f = xml_require := f + +let require_library spec qidl export = +(* + if sections_are_opened () && Options.verbose () then + warning ("Objets of "^(string_of_library modref)^ + " not surviving sections (e.g. Grammar \nand Hints)\n"^ + "will be removed at the end of the section"); +*) + let modrefl = List.map rec_intern_qualified_library qidl in + if Lib.is_modtype () || Lib.is_module () then begin + add_anonymous_leaf (in_require (modrefl,None)); + List.iter + (fun dir -> + add_anonymous_leaf (in_import (dir, export))) + modrefl + end + else + add_anonymous_leaf (in_require (modrefl,Some export)); + if !Options.xml_export then List.iter !xml_require modrefl; + add_frozen_state () + +let require_library_from_file spec idopt file export = + let modref = rec_intern_library_from_file idopt file in + if Lib.is_modtype () || Lib.is_module () then begin + add_anonymous_leaf (in_require ([modref],None)); + add_anonymous_leaf (in_import (modref, export)) + end + else + add_anonymous_leaf (in_require ([modref],Some export)); + if !Options.xml_export then !xml_require modref; + add_frozen_state () + + +(* read = require without opening *) + +let read_library qid = + let modref = rec_intern_qualified_library qid in + add_anonymous_leaf (in_require ([modref],None)); + if !Options.xml_export then !xml_require modref; + add_frozen_state () + +let read_library_from_file f = + let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in + let modref = rec_intern_by_filename_only None f in + add_anonymous_leaf (in_require ([modref],None)); + if !Options.xml_export then !xml_require modref; + add_frozen_state () + + +(* called at end of section *) + +let reload_library modrefl = + add_anonymous_leaf (in_require modrefl); + add_frozen_state () + + + +(* the function called by Vernacentries.vernac_import *) + +let import_library export (loc,qid) = + try + match Nametab.locate_module qid with + MPfile dir -> + if Lib.is_modtype () || Lib.is_module () || not export then + add_anonymous_leaf (in_import (dir, export)) + else + add_anonymous_leaf (in_require ([dir], Some export)) + | mp -> + import_module export mp + with + Not_found -> + user_err_loc + (loc,"import_library", + str ((string_of_qualid qid)^" is not a module")) + +(************************************************************************) +(*s [save_library s] saves the library [m] to the disk. *) + +let start_library f = + let _,longf = + System.find_file_in_path (get_load_path ()) (f^".v") in + let ldir0 = find_logical_path (Filename.dirname longf) in + let id = id_of_string (Filename.basename f) in + let ldir = extend_dirpath ldir0 id in + Declaremods.start_library ldir; + ldir,longf + +let current_deps () = + List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list + +let current_reexports () = + List.map (fun m -> m.library_name) !libraries_exports_list + +let save_library_to s f = + let cenv, seg = Declaremods.end_library s in + let md = { + md_name = s; + md_compiled = cenv; + md_objects = seg; + md_deps = current_deps (); + md_imports = current_reexports () } in + let (f',ch) = raw_extern_library f in + try + System.marshal_out ch md; + flush ch; + 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) + +(*s Pretty-printing of libraries state. *) + +(* this function is not used... *) +let fmt_libraries_state () = + let opened = opened_libraries () + and loaded = loaded_libraries () in + (str "Imported (open) Modules: " ++ + prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++ + str "Loaded Modules: " ++ + prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ()) + + +(*s For tactics/commands requiring vernacular libraries *) + +let check_required_library d = + let d' = List.map id_of_string d in + let dir = make_dirpath (List.rev d') in + if not (library_is_loaded dir) then +(* Loading silently ... + let m, prefix = list_sep_last d' in + read_library + (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) +*) +(* or failing ...*) + error ("Library "^(list_last d)^" has to be required first") + + +(*s Display the memory use of a library. *) + +open Printf + +let mem s = + let m = find_library s in + h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" + (size_kb m) (size_kb m.library_compiled) + (size_kb m.library_objects))) diff --git a/library/library.mli b/library/library.mli new file mode 100644 index 00000000..18be1671 --- /dev/null +++ b/library/library.mli @@ -0,0 +1,94 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +val read_library_from_file : System.physical_path -> unit + +(* [import_library true qid] = [export qid] *) + +val import_library : bool -> qualid located -> unit + +val library_is_loaded : dir_path -> bool +val library_is_opened : dir_path -> bool + +val loaded_libraries : unit -> dir_path list +val opened_libraries : unit -> dir_path list + +val fmt_libraries_state : unit -> Pp.std_ppcmds + +(*s Require. The command [require_library spec m file export] loads and opens + a library [m]. [file] specifies the filename, if not [None]. [spec] + specifies to look for a specification ([true]) or for an implementation + ([false]), if not [None]. And [export] specifies if the library must be + exported. *) + +val require_library : + bool option -> qualid located list -> bool -> unit + +val require_library_from_file : + bool option -> identifier option -> System.physical_path -> bool -> unit + +val set_xml_require : (dir_path -> unit) -> unit + +(*s [save_library_to s f] saves the current environment as a library [s] + in the file [f]. *) + +val start_library : string -> dir_path * string +val save_library_to : dir_path -> string -> unit + +(* [library_full_filename] returns the full filename of a loaded library. *) + +val library_full_filename : dir_path -> string + + +(*s Global load path *) +type logical_path = dir_path + +val get_load_path : unit -> System.physical_path list +val get_full_load_path : unit -> (System.physical_path * logical_path) list +val add_load_path_entry : System.physical_path * logical_path -> unit +val remove_path : System.physical_path -> unit +val find_logical_path : System.physical_path -> logical_path +val load_path_of_logical_path : dir_path -> System.physical_path list + +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +val locate_qualified_library : + qualid -> library_location * dir_path * System.physical_path + + +val check_required_library : string list -> unit + +(*s Displays the memory use of a library. *) +val mem : dir_path -> Pp.std_ppcmds + +(* For discharge *) +type library_reference + +val out_require : Libobject.obj -> library_reference +val reload_library : library_reference -> unit diff --git a/library/nameops.ml b/library/nameops.ml new file mode 100644 index 00000000..ea40aae5 --- /dev/null +++ b/library/nameops.ml @@ -0,0 +1,173 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* slen then + numpart (n-1) n' + else if code_of_0 <= c && c <= code_of_9 then + numpart (n-1) (n-1) + else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then + numpart (n-1) (n-1) + else + n' + in + numpart slen slen + +let repr_ident s = + let numstart = cut_ident false s in + let s = string_of_id s in + let slen = String.length s in + if numstart = slen then + (s, None) + else + (String.sub s 0 numstart, + Some (int_of_string (String.sub s numstart (slen - numstart)))) + +let make_ident sa = function + | Some n -> + let c = Char.code (String.get sa (String.length sa -1)) in + let s = + if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n) + else sa ^ "_" ^ (string_of_int n) in + id_of_string s + | None -> id_of_string (String.copy sa) + +let root_of_id id = + let suffixstart = cut_ident true id in + id_of_string (String.sub (string_of_id id) 0 suffixstart) + +(* Rem: semantics is a bit different, if an ident starts with toto00 then + after successive renamings it comes to toto09, then it goes on with toto10 *) +let lift_subscript id = + let id = string_of_id id in + let len = String.length id in + let rec add carrypos = + let c = id.[carrypos] in + if is_digit c then + if c = '9' then begin + assert (carrypos>0); + add (carrypos-1) + end + else begin + let newid = String.copy id in + String.fill newid (carrypos+1) (len-1-carrypos) '0'; + newid.[carrypos] <- Char.chr (Char.code c + 1); + newid + end + else begin + let newid = id^"0" in + if carrypos < len-1 then begin + String.fill newid (carrypos+1) (len-1-carrypos) '0'; + newid.[carrypos+1] <- '1' + end; + newid + end + in id_of_string (add (len-1)) + +let has_subscript id = + let id = string_of_id id in + is_digit (id.[String.length id - 1]) + +let forget_subscript id = + let numstart = cut_ident false id in + let newid = String.make (numstart+1) '0' in + String.blit (string_of_id id) 0 newid 0 numstart; + (id_of_string newid) + +let add_suffix id s = id_of_string (string_of_id id ^ s) +let add_prefix s id = id_of_string (s ^ string_of_id id) + +let atompart_of_id id = fst (repr_ident id) + +(* Fresh names *) + +let lift_ident = lift_subscript + +let next_ident_away id avoid = + if List.mem id avoid then + let id0 = if not (has_subscript id) then id else + (* Ce serait sans doute mieux avec quelque chose inspiré de + *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) + forget_subscript id in + let rec name_rec id = + if List.mem id avoid then name_rec (lift_ident id) else id in + name_rec id0 + else id + +let next_ident_away_from id avoid = + let rec name_rec id = + if List.mem id avoid then name_rec (lift_ident id) else id in + name_rec id + +(* Names *) + +let out_name = function + | Name id -> id + | Anonymous -> anomaly "out_name: expects a defined name" + +let name_fold f na a = + match na with + | Name id -> f id a + | Anonymous -> a + +let name_cons na l = + match na with + | Anonymous -> l + | Name id -> id::l + +let name_app f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + +let next_name_away_with_default default name l = + match name with + | Name str -> next_ident_away str l + | Anonymous -> next_ident_away (id_of_string default) l + +let next_name_away name l = + match name with + | Name str -> next_ident_away str l + | Anonymous -> id_of_string "_" + +let pr_lab l = str (string_of_label l) + +let default_library = Names.initial_dir (* = ["Top"] *) + +(*s Roots of the space of absolute names *) +let coq_root = id_of_string "Coq" +let default_root_prefix = make_dirpath [] + +(* Metavariables *) +let pr_meta = Pp.int +let string_of_meta = string_of_int diff --git a/library/nameops.mli b/library/nameops.mli new file mode 100644 index 00000000..4b7cecda --- /dev/null +++ b/library/nameops.mli @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Pp.std_ppcmds +val wildcard : identifier + +val make_ident : string -> int option -> identifier +val repr_ident : identifier -> string * int option + +val atompart_of_id : identifier -> string (* remove trailing digits *) +val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *) + +val add_suffix : identifier -> string -> identifier +val add_prefix : string -> identifier -> identifier + +val lift_ident : identifier -> identifier +val next_ident_away : identifier -> identifier list -> identifier +val next_ident_away_from : identifier -> identifier list -> identifier + +val next_name_away : name -> identifier list -> identifier +val next_name_away_with_default : + string -> name -> identifier list -> identifier + +val out_name : name -> identifier + +val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a +val name_cons : name -> identifier list -> identifier list +val name_app : (identifier -> identifier) -> name -> name + +val pr_lab : label -> Pp.std_ppcmds + +(* some preset paths *) + +val default_library : dir_path + +(* This is the root of the standard library of Coq *) +val coq_root : module_ident + +(* This is the default root prefix for developments which doesn't + mention a root *) +val default_root_prefix : dir_path + +(* Metavariables *) +val pr_meta : Term.metavariable -> Pp.std_ppcmds +val string_of_meta : Term.metavariable -> string diff --git a/library/nametab.ml b/library/nametab.ml new file mode 100755 index 00000000..f009d867 --- /dev/null +++ b/library/nametab.ml @@ -0,0 +1,553 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string + val repr : t -> identifier * module_ident list +end + + +(* A ['a t] is a map from [user_name] to ['a], with possible lookup by + partially qualified names of type [qualid]. The mapping of + partially qualified names to ['a] is determined by the [visibility] + parameter of [push]. + + The [shortest_qualid] function given a user_name Coq.A.B.x, tries + to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes + the same object. +*) +module type NAMETREE = sig + type 'a t + type user_name + + val empty : 'a t + val push : visibility -> user_name -> 'a -> 'a t -> 'a t + val locate : qualid -> 'a t -> 'a + val find : user_name -> 'a t -> 'a + val exists : user_name -> 'a t -> bool + val user_name : qualid -> 'a t -> user_name + val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid + val find_prefixes : qualid -> 'a t -> 'a list +end + +module Make(U:UserName) : NAMETREE with type user_name = U.t + = +struct + + type user_name = U.t + + type 'a path_status = + Nothing + | Relative of user_name * 'a + | Absolute of user_name * 'a + + (* Dictionaries of short names *) + type 'a nametree = ('a path_status * 'a nametree ModIdmap.t) + + type 'a t = 'a nametree Idmap.t + + let empty = Idmap.empty + + (* [push_until] is used to register [Until vis] visibility and + [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*) + + let rec push_until uname o level (current,dirmap) = function + | modid :: path as dir -> + let mc = + try ModIdmap.find modid dirmap + with Not_found -> (Nothing, ModIdmap.empty) + in + let this = + if level <= 0 then + match current with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); + current + | Nothing + | Relative _ -> Relative (uname,o) + else current + in + let ptab' = push_until uname o (level-1) mc path in + (this, ModIdmap.add modid ptab' dirmap) + | [] -> + match current with + | Absolute (uname',o') -> + if o'=o then begin + assert (uname=uname'); + current, dirmap + (* we are putting the same thing for the second time :) *) + end + else + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + (* But ours is also absolute! This is an error! *) + error ("Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") + | Nothing + | Relative _ -> Absolute (uname,o), dirmap + + +let rec push_exactly uname o level (current,dirmap) = function + | modid :: path as dir -> + let mc = + try ModIdmap.find modid dirmap + with Not_found -> (Nothing, ModIdmap.empty) + in + if level = 0 then + let this = + match current with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); + current + | Nothing + | Relative _ -> Relative (uname,o) + in + (this, dirmap) + else (* not right level *) + let ptab' = push_exactly uname o (level-1) mc path in + (current, ModIdmap.add modid ptab' dirmap) + | [] -> + anomaly "Prefix longer than path! Impossible!" + + +let push visibility uname o tab = + let id,dir = U.repr uname in + let ptab = + try Idmap.find id tab + with Not_found -> (Nothing, ModIdmap.empty) + in + let ptab' = match visibility with + | Until i -> push_until uname o (i-1) ptab dir + | Exactly i -> push_exactly uname o (i-1) ptab dir + in + Idmap.add id ptab' tab + + +let rec search (current,modidtab) = function + | modid :: path -> search (ModIdmap.find modid modidtab) path + | [] -> current + +let find_node qid tab = + let (dir,id) = repr_qualid qid in + search (Idmap.find id tab) (repr_dirpath dir) + +let locate qid tab = + let o = match find_node qid tab with + | Absolute (uname,o) | Relative (uname,o) -> o + | Nothing -> raise Not_found + in + o + +let user_name qid tab = + let uname = match find_node qid tab with + | Absolute (uname,o) | Relative (uname,o) -> uname + | Nothing -> raise Not_found + in + uname + +let find uname tab = + let id,l = U.repr uname in + match search (Idmap.find id tab) l with + Absolute (_,o) -> o + | _ -> raise Not_found + +let exists uname tab = + try + let _ = find uname tab in + true + with + Not_found -> false + +let shortest_qualid ctx uname tab = + let id,dir = U.repr uname in + let hidden = Idset.mem id ctx in + let rec find_uname pos dir (path,tab) = match path with + | Absolute (u,_) | Relative (u,_) + when u=uname && not(pos=[] && hidden) -> List.rev pos + | _ -> + match dir with + [] -> raise Not_found + | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab) + in + let ptab = Idmap.find id tab in + let found_dir = find_uname [] dir ptab in + make_qualid (make_dirpath found_dir) id + +let push_node node l = + match node with + | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l + | _ -> l + +let rec flatten_idmap tab l = + ModIdmap.fold (fun _ (current,idtab) l -> + flatten_idmap idtab (push_node current l)) tab l + +let rec search_prefixes (current,modidtab) = function + | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path + | [] -> List.rev (flatten_idmap modidtab (push_node current [])) + +let find_prefixes qid tab = + try + let (dir,id) = repr_qualid qid in + search_prefixes (Idmap.find id tab) (repr_dirpath dir) + with Not_found -> [] + +end + + + +(* Global name tables *************************************************) + +module SpTab = Make (struct + type t = section_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (repr_dirpath dir) + end) + + +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 objtab = unit SpTab.t +let the_objtab = ref (SpTab.empty : objtab) + + +module DirTab = Make(struct + type t = dir_path + let to_string = string_of_dirpath + let repr dir = match repr_dirpath dir with + | [] -> anomaly "Empty dirpath" + | id::l -> (id,l) + end) + +(* If we have a (closed) module M having a submodule N, than N does not + have the entry in [the_dirtab]. *) +type dirtab = global_dir_reference DirTab.t +let the_dirtab = ref (DirTab.empty : dirtab) + + +(* Reversed name tables ***************************************************) + +(* This table translates extended_global_references back to section paths *) +module Globrevtab = Map.Make(struct + type t=extended_global_reference + let compare = compare + end) + +type globrevtab = section_path Globrevtab.t +let the_globrevtab = ref (Globrevtab.empty : globrevtab) + + +type mprevtab = dir_path MPmap.t +let the_modrevtab = ref (MPmap.empty : mprevtab) + +type knrevtab = section_path KNmap.t +let the_modtyperevtab = ref (KNmap.empty : knrevtab) +let the_tacticrevtab = ref (KNmap.empty : knrevtab) + + +(* Push functions *********************************************************) + +(* This is for permanent constructions (never discharged -- but with + possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom, + Parameter but also Remark and Fact) *) + +let push_xref visibility sp xref = + the_ccitab := SpTab.push visibility sp xref !the_ccitab; + match visibility with + | Until _ -> + the_globrevtab := Globrevtab.add xref sp !the_globrevtab + | _ -> () + +let push_cci visibility sp ref = + push_xref visibility sp (TrueGlobal ref) + +(* This is for Syntactic Definitions *) +let push_syntactic_definition visibility sp kn = + push_xref visibility sp (SyntacticDef kn) + +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 + +(* This is for tactic definition names *) + +let push_tactic vis sp kn = + the_tactictab := SpTab.push vis sp kn !the_tactictab; + the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab + + +(* This is for dischargeable non-cci objects (removed at the end of the + section -- i.e. Hints, Grammar ...) *) (* --> Unused *) + +let push_object visibility sp = + the_objtab := SpTab.push visibility sp () !the_objtab + +(* This is to remember absolute Section/Module names and to avoid redundancy *) +let push_dir vis dir dir_ref = + the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; + match dir_ref with + DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab + | _ -> () + + +(* Locate functions *******************************************************) + + +(* This should be used when syntactic definitions are allowed *) +let extended_locate qid = SpTab.locate qid !the_ccitab + +(* This should be used when no syntactic definitions is expected *) +let locate qid = match extended_locate qid with + | TrueGlobal ref -> ref + | SyntacticDef _ -> raise Not_found +let full_name_cci qid = SpTab.user_name qid !the_ccitab + +let locate_syntactic_definition qid = match extended_locate qid with + | TrueGlobal _ -> raise Not_found + | SyntacticDef kn -> kn + +let locate_modtype qid = SpTab.locate qid !the_modtypetab +let full_name_modtype qid = SpTab.user_name qid !the_modtypetab + +let locate_obj qid = SpTab.user_name qid !the_objtab + +type ltac_constant = kernel_name +let locate_tactic qid = SpTab.locate qid !the_tactictab +let full_name_tactic qid = SpTab.user_name qid !the_tactictab + +let locate_dir qid = DirTab.locate qid !the_dirtab + +let locate_module qid = + match locate_dir qid with + | DirModule (_,(mp,_)) -> mp + | _ -> raise Not_found + +let full_name_module qid = + match locate_dir qid with + | DirModule (dir,_) -> dir + | _ -> raise Not_found + +let locate_section qid = + match locate_dir qid with + | DirOpenSection (dir, _) + | DirClosedSection dir -> dir + | _ -> raise Not_found + +let locate_all qid = + List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) + (SpTab.find_prefixes qid !the_ccitab) [] + +let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab + +(* Derived functions *) + +let locate_constant qid = + match extended_locate qid with + | TrueGlobal (ConstRef kn) -> kn + | _ -> raise Not_found + +let locate_mind qid = + match extended_locate qid with + | TrueGlobal (IndRef (kn,0)) -> kn + | _ -> raise Not_found + + +let absolute_reference sp = + match SpTab.find sp !the_ccitab with + | TrueGlobal ref -> ref + | _ -> raise Not_found + +let locate_in_absolute_module dir id = + absolute_reference (make_path dir id) + +let global r = + let (loc,qid) = qualid_of_reference r in + try match extended_locate qid with + | TrueGlobal ref -> ref + | SyntacticDef _ -> + user_err_loc (loc,"global", + str "Unexpected reference to a syntactic definition: " ++ + pr_qualid qid) + with Not_found -> + error_global_not_found_loc loc qid + +(* Exists functions ********************************************************) + +let exists_cci sp = SpTab.exists sp !the_ccitab + +let exists_dir dir = DirTab.exists dir !the_dirtab + +let exists_section = exists_dir + +let exists_module = exists_dir + +let exists_modtype sp = SpTab.exists sp !the_modtypetab + +let exists_tactic sp = SpTab.exists sp !the_tactictab + +(* Reverse locate functions ***********************************************) + +let sp_of_global ref = + match ref with + | VarRef id -> make_path empty_dirpath id + | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab + + +let id_of_global ref = + let (_,id) = repr_path (sp_of_global ref) in + id + +let sp_of_syntactic_definition kn = + Globrevtab.find (SyntacticDef kn) !the_globrevtab + +let dir_of_mp mp = + MPmap.find mp !the_modrevtab + + +(* Shortest qualid functions **********************************************) + +let shortest_qualid_of_global ctx ref = + match ref with + | VarRef id -> make_qualid empty_dirpath id + | _ -> + let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in + SpTab.shortest_qualid ctx sp !the_ccitab + +let shortest_qualid_of_syndef kn = + let sp = sp_of_syntactic_definition kn in + SpTab.shortest_qualid Idset.empty sp !the_ccitab + +let shortest_qualid_of_module mp = + let dir = MPmap.find mp !the_modrevtab in + DirTab.shortest_qualid Idset.empty dir !the_dirtab + +let shortest_qualid_of_modtype kn = + let sp = KNmap.find kn !the_modtyperevtab in + SpTab.shortest_qualid Idset.empty sp !the_modtypetab + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn !the_tacticrevtab in + SpTab.shortest_qualid Idset.empty sp !the_tactictab + +let pr_global_env env ref = + (* Il est important de laisser le let-in, car les streams s'évaluent + paresseusement : il faut forcer l'évaluation pour capturer + l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) + let s = string_of_qualid (shortest_qualid_of_global env ref) in + (str s) + +let global_inductive r = + match global r with + | IndRef ind -> ind + | ref -> + user_err_loc (loc_of_reference r,"global_inductive", + pr_reference r ++ spc () ++ str "is not an inductive type") + +(********************************************************************) + +(********************************************************************) +(* Registration of tables as a global table and rollback *) + +type frozen = ccitab * dirtab * objtab * kntab * kntab + * globrevtab * mprevtab * knrevtab * knrevtab + +let init () = + the_ccitab := SpTab.empty; + the_dirtab := DirTab.empty; + the_objtab := SpTab.empty; + the_modtypetab := SpTab.empty; + the_tactictab := SpTab.empty; + the_globrevtab := Globrevtab.empty; + the_modrevtab := MPmap.empty; + the_modtyperevtab := KNmap.empty; + the_tacticrevtab := KNmap.empty + + +let freeze () = + !the_ccitab, + !the_dirtab, + !the_objtab, + !the_modtypetab, + !the_tactictab, + !the_globrevtab, + !the_modrevtab, + !the_modtyperevtab, + !the_tacticrevtab + +let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) = + the_ccitab := ccit; + the_dirtab := dirt; + the_objtab := objt; + the_modtypetab := mtyt; + the_tactictab := tact; + the_globrevtab := globr; + the_modrevtab := modr; + the_modtyperevtab := mtyr; + the_tacticrevtab := tacr + +let _ = + Summary.declare_summary "names" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } diff --git a/library/nametab.mli b/library/nametab.mli new file mode 100755 index 00000000..3a0bd670 --- /dev/null +++ b/library/nametab.mli @@ -0,0 +1,171 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* full_user_name -> object_reference -> unit] + + Registers the [object_reference] to be referred to by the + [full_user_name] (and its suffixes according to [visibility]). + [full_user_name] can either be a [section_path] or a [dir_path]. + + \item [exists : full_user_name -> bool] + + Is the [full_user_name] already atributed as an absolute user name + of some object? + + \item [locate : qualid -> object_reference] + + Finds the object referred to by [qualid] or raises Not_found + + \item [name_of] : object_reference -> user_name + + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [identifier]. Such a function can also have a + local context argument. +*) + + +exception GlobalizationError of qualid +exception GlobalizationConstantError of qualid + +(* Raises a globalization error *) +val error_global_not_found_loc : loc -> qualid -> 'a +val error_global_not_found : qualid -> 'a +val error_global_constant_not_found_loc : loc -> qualid -> 'a + + + + +(*s Register visibility of things *) + +(* The visibility can be registered either + \begin{itemize} + + \item for all suffixes not shorter then a given int -- when the + object is loaded inside a module -- or + + \item for a precise suffix, when the module containing (the module + containing ...) the object is opened (imported) + \end{itemize} +*) + +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_dir : visibility -> dir_path -> global_dir_reference -> unit +val push_object : visibility -> section_path -> unit +val push_tactic : visibility -> section_path -> kernel_name -> unit + + +(*s The following functions perform globalization of qualified names *) + +(* This returns the section path of a constant or fails with [Not_found] *) +val locate : qualid -> global_reference + +(* This function is used to transform a qualified identifier into a + global reference, with a nice error message in case of failure *) +val global : reference -> global_reference + +(* The same for inductive types *) +val global_inductive : reference -> inductive + +(* This locates also syntactic definitions *) +val extended_locate : qualid -> extended_global_reference + +(* This locates all names with a given suffix, if qualid is valid as + such, it comes first in the list *) +val extended_locate_all : qualid -> extended_global_reference list + +(* This locates all global references with a given suffixe *) +val locate_all : qualid -> global_reference list + +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_syntactic_definition : qualid -> kernel_name + +type ltac_constant = kernel_name +val locate_tactic : qualid -> ltac_constant +val locate_dir : qualid -> global_dir_reference +val locate_module : qualid -> module_path + +(* A variant looking up a [section_path] *) +val absolute_reference : section_path -> global_reference + + +(*s These function tell if the given absolute name is already taken *) + +val exists_cci : section_path -> bool +val exists_modtype : section_path -> bool + +(* Those three functions are the same *) +val exists_dir : dir_path -> bool +val exists_section : dir_path -> bool (* deprecated *) +val exists_module : dir_path -> bool (* deprecated *) + + +(*s These functions turn qualids into full user names: [section_path]s + or [dir_path]s *) + +val full_name_modtype : qualid -> section_path +val full_name_cci : qualid -> section_path + +(* As above but checks that the path found is indeed a module *) +val full_name_module : qualid -> dir_path + + +(*s Reverse lookup -- finding user names corresponding to the given + internal name *) + +val sp_of_syntactic_definition : kernel_name -> section_path +val shortest_qualid_of_global : Idset.t -> global_reference -> qualid +val shortest_qualid_of_syndef : kernel_name -> qualid +val shortest_qualid_of_tactic : ltac_constant -> qualid + +val dir_of_mp : module_path -> dir_path + +val sp_of_global : global_reference -> section_path +val id_of_global : global_reference -> identifier + +(* Printing of global references using names as short as possible *) +val pr_global_env : Idset.t -> global_reference -> std_ppcmds + + +(* The [shortest_qualid] functions given an object with user_name + Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and + Coq.A.B.x that denotes the same object. *) + +val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_modtype : kernel_name -> qualid + + +(* +type frozen + +val freeze : unit -> frozen +val unfreeze : frozen -> unit +*) diff --git a/library/states.ml b/library/states.ml new file mode 100644 index 00000000..7a7f1e06 --- /dev/null +++ b/library/states.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raw_extern s (get_state())), + (fun s -> set_state (raw_intern (Library.get_load_path ()) s)) + +(* Rollback. *) + +let freeze = get_state +let unfreeze = set_state + +let with_heavy_rollback f x = + let st = get_state () in + try + f x + with reraise -> + (set_state st; raise reraise) diff --git a/library/states.mli b/library/states.mli new file mode 100644 index 00000000..70018180 --- /dev/null +++ b/library/states.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val extern_state : string -> unit + +type state +val freeze : unit -> state +val unfreeze : state -> unit + +(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the + state of the whole system as it was before the evaluation if an exception + is raised. *) + +val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b + + diff --git a/library/summary.ml b/library/summary.ml new file mode 100644 index 00000000..fc88350a --- /dev/null +++ b/library/summary.ml @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a; + unfreeze_function : 'a -> unit; + init_function : unit -> unit; + survive_module : bool ; + survive_section : bool } + +let summaries = + (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) + +let internal_declare_summary sumname sdecl = + let (infun,outfun) = Dyn.create sumname in + let dyn_freeze () = infun (sdecl.freeze_function()) + and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) + and dyn_init = sdecl.init_function in + let ddecl = { + freeze_function = dyn_freeze; + unfreeze_function = dyn_unfreeze; + init_function = dyn_init; + survive_module = sdecl.survive_module; + survive_section = sdecl.survive_section } + in + if Hashtbl.mem summaries sumname then + anomalylabstrm "Summary.declare_summary" + (str "Cannot declare a summary twice: " ++ str sumname); + Hashtbl.add summaries sumname ddecl + +let declare_summary sumname decl = + internal_declare_summary (sumname^"-SUMMARY") decl + +type frozen = Dyn.t Stringmap.t + +let freeze_summaries () = + let m = ref Stringmap.empty in + Hashtbl.iter + (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m) + summaries; + !m + + +let unfreeze_some_summaries p fs = + Hashtbl.iter + (fun id decl -> + try + if p decl then + decl.unfreeze_function (Stringmap.find id fs) + with Not_found -> decl.init_function()) + summaries + +let unfreeze_summaries = + unfreeze_some_summaries (fun _ -> true) + +let section_unfreeze_summaries = + unfreeze_some_summaries (fun decl -> not decl.survive_section) + +let module_unfreeze_summaries = + unfreeze_some_summaries (fun decl -> not decl.survive_module) + +let init_summaries () = + Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli new file mode 100644 index 00000000..7e691f0b --- /dev/null +++ b/library/summary.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a; + unfreeze_function : 'a -> unit; + init_function : unit -> unit; + survive_module : bool; (* should be false is most cases *) + survive_section : bool } + +val declare_summary : string -> 'a summary_declaration -> unit + +type frozen + +val freeze_summaries : unit -> frozen +val unfreeze_summaries : frozen -> unit +val section_unfreeze_summaries : frozen -> unit +val module_unfreeze_summaries : frozen -> unit +val init_summaries : unit -> unit + + + -- cgit v1.2.3