summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml70
-rw-r--r--library/declare.ml262
-rw-r--r--library/declare.mli37
-rw-r--r--library/declaremods.ml74
-rw-r--r--library/declaremods.mli19
-rw-r--r--library/dischargedhypsmap.ml9
-rw-r--r--library/dischargedhypsmap.mli2
-rw-r--r--library/global.ml19
-rw-r--r--library/global.mli11
-rw-r--r--library/goptions.ml3
-rw-r--r--library/goptions.mli3
-rw-r--r--library/impargs.ml190
-rw-r--r--library/impargs.mli8
-rw-r--r--library/lib.ml215
-rw-r--r--library/lib.mli43
-rw-r--r--library/libnames.ml61
-rw-r--r--library/libnames.mli23
-rw-r--r--library/libobject.ml15
-rw-r--r--library/libobject.mli5
-rw-r--r--library/library.ml514
-rw-r--r--library/library.mli94
-rw-r--r--library/nameops.ml6
-rw-r--r--library/nameops.mli4
-rw-r--r--[-rwxr-xr-x]library/nametab.ml6
-rwxr-xr-xlibrary/nametab.mli2
-rw-r--r--library/states.ml4
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.ml2
-rw-r--r--library/summary.mli2
29 files changed, 837 insertions, 868 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index a030284c..af54df2f 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_kinds.ml,v 1.6.2.1 2004/07/16 19:30:33 herbelin Exp $ *)
+(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *)
+
+open Util
(* Informal mathematical status of declarations *)
@@ -14,23 +16,32 @@ type locality_flag = (*bool (* local = true; global = false *)*)
| Local
| Global
-(* Kinds used at parsing time *)
+type boxed_flag = bool
type theorem_kind =
| Theorem
| Lemma
| Fact
| Remark
+ | Property
+ | Proposition
+ | Corollary
type definition_object_kind =
| Definition
| Coercion
| SubClass
| CanonicalStructure
+ | Example
+ | Fixpoint
+ | CoFixpoint
+ | Scheme
+ | StructureComponent
+ | IdentityCoercion
type strength = locality_flag (* For compatibility *)
-type type_as_formula_kind = Definitional | Logical | Conjectural
+type assumption_object_kind = Definitional | Logical | Conjectural
(* [assumption_kind]
@@ -40,36 +51,51 @@ type type_as_formula_kind = Definitional | Logical | Conjectural
Logical | Hypothesis | Axiom
*)
-type assumption_kind = locality_flag * type_as_formula_kind
+type assumption_kind = locality_flag * assumption_object_kind
-type definition_kind = locality_flag * definition_object_kind
+type definition_kind = locality_flag * boxed_flag * definition_object_kind
(* Kinds used in proofs *)
-type global_goal_kind =
- | DefinitionBody
+type goal_object_kind =
+ | DefinitionBody of definition_object_kind
| Proof of theorem_kind
-type goal_kind =
- | IsGlobal of global_goal_kind
- | IsLocal
+type goal_kind = locality_flag * goal_object_kind
(* Kinds used in library *)
-type local_theorem_kind = LocalStatement
-
-type 'a mathematical_kind =
- | IsAssumption of type_as_formula_kind
- | IsDefinition
- | IsConjecture
- | IsProof of 'a
-
-type global_kind = theorem_kind mathematical_kind
-type local_kind = local_theorem_kind mathematical_kind
+type logical_kind =
+ | IsAssumption of assumption_object_kind
+ | IsDefinition of definition_object_kind
+ | IsProof of theorem_kind
(* Utils *)
-let theorem_kind_of_goal_kind = function
- | DefinitionBody -> IsDefinition
+let logical_kind_of_goal_kind = function
+ | DefinitionBody d -> IsDefinition d
| Proof s -> IsProof s
+let string_of_theorem_kind = function
+ | Theorem -> "Theorem"
+ | Lemma -> "Lemma"
+ | Fact -> "Fact"
+ | Remark -> "Remark"
+ | Property -> "Property"
+ | Proposition -> "Proposition"
+ | Corollary -> "Corollary"
+
+let string_of_definition_kind (l,boxed,d) =
+ match (l,d) with
+ | Local, Coercion -> "Coercion Local"
+ | Global, Coercion -> "Coercion"
+ | Local, Definition -> "Let"
+ | Global, Definition -> if boxed then "Boxed Definition" else "Definition"
+ | Local, SubClass -> "Local SubClass"
+ | Global, SubClass -> "SubClass"
+ | Global, CanonicalStructure -> "Canonical Structure"
+ | Global, Example -> "Example"
+ | Local, (CanonicalStructure|Example) ->
+ anomaly "Unsupported local definition kind"
+ | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion)
+ -> anomaly "Internal definition kind"
diff --git a/library/declare.ml b/library/declare.ml
index cfa8890a..b1e55c20 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *)
+(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
open Pp
open Util
@@ -31,11 +31,7 @@ open Decl_kinds
(**********************************************)
-(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
- construction keeps in its name (if persistent), or the section name
- beyond which it is discharged (if volatile); the integer [n]
- (useful only for persistent constructions), is the length of the section
- part in [dir] *)
+(* Strength *)
open Nametab
@@ -47,9 +43,9 @@ let string_of_strength = function
| 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 xml_declare_variable = ref (fun (sp:object_name) -> ())
+let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
let if_xml f x = if !Options.xml_export then f x else ()
@@ -63,25 +59,28 @@ 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 variable_declaration = dir_path * section_variable_entry * logical_kind
type checked_section_variable =
| CheckedSectionLocalDef of constr * types * Univ.constraints * bool
| CheckedSectionLocalAssum of types * Univ.constraints
type checked_variable_declaration =
- dir_path * checked_section_variable * local_kind
+ dir_path * checked_section_variable * logical_kind
let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
let _ = Summary.declare_summary "VARIABLE"
- { Summary.freeze_function = (fun () -> !vartab);
- Summary.unfreeze_function = (fun ft -> vartab := ft);
- Summary.init_function = (fun () -> vartab := Idmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = false }
-
-let cache_variable ((sp,_),(id,(p,d,mk))) =
+ { Summary.freeze_function = (fun () -> !vartab);
+ Summary.unfreeze_function = (fun ft -> vartab := ft);
+ Summary.init_function = (fun () -> vartab := Idmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+let cache_variable ((sp,_),o) =
+ match o with
+ | Inl cst -> Global.add_constraints cst
+ | Inr (id,(p,d,mk)) ->
(* Constr raisonne sur les noms courts *)
if Idmap.mem id !vartab then
errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -95,36 +94,38 @@ let cache_variable ((sp,_),(id,(p,d,mk))) =
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);
+ add_section_variable id;
+ Dischargedhypsmap.set_discharged_hyps sp [];
vartab := Idmap.add id (p,vd,mk) !vartab
+let get_variable_constraints id =
+ match pi2 (Idmap.find id !vartab) with
+ | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst
+ | CheckedSectionLocalAssum (ty,cst) -> cst
+
+let discharge_variable (_,o) = match o with
+ | Inr (id,_) -> Some (Inl (get_variable_constraints id))
+ | Inl _ -> Some o
+
let (in_variable, out_variable) =
declare_object { (default_object "VARIABLE") with
cache_function = cache_variable;
+ discharge_function = discharge_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
+ let oname = add_leaf id (in_variable (Inr (id,obj))) in
+ declare_var_implicits id;
+ Notation.declare_ref_arguments_scope (VarRef id);
!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
+type constant_declaration = constant_entry * logical_kind
-let csttab = ref (Spmap.empty : global_kind Spmap.t)
+let csttab = ref (Spmap.empty : logical_kind Spmap.t)
let _ = Summary.declare_summary "CONSTANT"
{ Summary.freeze_function = (fun () -> !csttab);
@@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT"
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)
+let load_constant i ((sp,kn),(_,_,_,kind)) =
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_constant"
+ (pr_id (basename sp) ++ str " already exists");
+ Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
+ csttab := Spmap.add sp kind !csttab
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn),_) =
- Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
+ Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+ let id = basename sp in
+ let _,dir,_ = repr_kn kn in
+ if Idmap.mem id !vartab then
+ errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+ let kn' = Global.add_constant dir id cdt in
+ assert (kn' = constant_of_kn kn);
+ Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+ add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+ Dischargedhypsmap.set_discharged_hyps sp dhyps;
+ with_implicits imps declare_constant_implicits kn';
+ Notation.declare_ref_arguments_scope (ConstRef kn');
+ csttab := Spmap.add sp kind !csttab
+
+(*s Registration as global tables and rollback. *)
+
+open Cooking
+
+let discharged_hyps kn sechyps =
+ let (_,dir,_) = repr_kn kn in
+ let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+ List.rev (List.map (Libnames.make_path dir) args)
+
+let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+ let con = constant_of_kn kn in
+ let cb = Global.lookup_constant con in
+ let (repl1,_ as repl) = replacement_context () in
+ let sechyps = section_segment (ConstRef con) in
+ let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+ Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
-let dummy_constant (ce,mk) = dummy_constant_entry,mk
+let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk
let export_constant cst = Some (dummy_constant cst)
@@ -176,40 +196,43 @@ let (in_constant, out_constant) =
open_function = open_constant;
classify_function = classify_constant;
subst_function = ident_subst_function;
+ discharge_function = discharge_constant;
export_function = export_constant }
let hcons_constant_declaration = function
- | DefinitionEntry ce ->
+ | DefinitionEntry ce when !Options.hash_cons_proofs ->
let (hcons1_constr,_) = hcons_constr (hcons_names()) in
DefinitionEntry
{ const_entry_body = hcons1_constr ce.const_entry_body;
const_entry_type = option_app hcons1_constr ce.const_entry_type;
- const_entry_opaque = ce.const_entry_opaque }
+ const_entry_opaque = ce.const_entry_opaque;
+ const_entry_boxed = ce.const_entry_boxed }
| 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_common id dhyps (cd,kind) =
+ let imps = implicits_flags () in
+ let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
+ let kn = constant_of_kn kn in
+ kn
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 kn = declare_constant_common id [] (ConstantEntry cd,kind) in
+ !xml_declare_constant (internal,kn);
+ kn
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 declare_inductive_argument_scopes kn mie =
+ list_iter_i (fun i {mind_entry_consnames=lc} ->
+ Notation.declare_ref_arguments_scope (IndRef (kn,i));
+ for j=1 to List.length lc do
+ Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
+ done) mie.mind_entry_inds
+
let inductive_names sp kn mie =
let (dp,_) = repr_path sp in
let names, _ =
@@ -230,39 +253,44 @@ let inductive_names sp kn mie =
([], 0) mie.mind_entry_inds
in names
-
let check_exists_inductive (sp,_) =
(if Idmap.mem (basename sp) !vartab then
- errorlabstrm "cache_inductive"
+ errorlabstrm ""
(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")
+ errorlabstrm "" (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 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 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 cache_inductive ((sp,kn),(dhyps,imps,mie)) =
+ let names = inductive_names sp kn mie in
+ List.iter check_exists_inductive names;
+ let id = basename sp in
+ let _,dir,_ = repr_kn kn in
+ let kn' = Global.add_mind dir id mie in
+ assert (kn'=kn);
+ add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+ Dischargedhypsmap.set_discharged_hyps sp dhyps;
+ with_implicits imps declare_mib_implicits kn;
+ declare_inductive_argument_scopes kn mie;
+ List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
+ let mie = Global.lookup_mind kn in
+ let repl = replacement_context () in
+ let sechyps = section_segment (IndRef (kn,0)) in
+ Some (discharged_hyps kn sechyps,imps,
+ Discharge.process_inductive sechyps repl mie)
+
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;
@@ -270,10 +298,11 @@ let dummy_one_inductive_entry mie = {
}
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry m = {
+let dummy_inductive_entry (_,imps,m) = ([],imps,{
+ mind_entry_params = [];
mind_entry_record = false;
mind_entry_finite = true;
- mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
let export_inductive x = Some (dummy_inductive_entry x)
@@ -284,38 +313,19 @@ let (in_inductive, out_inductive) =
open_function = open_inductive;
classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
subst_function = ident_subst_function;
+ discharge_function = discharge_inductive;
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 [] ;
+ let imps = implicits_flags () in
+ 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 ([],imps,mie)) in
!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 =
@@ -330,12 +340,6 @@ let get_variable id =
| 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 =
@@ -351,8 +355,10 @@ 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
+ List.fold_right
+ (fun (id,c,t as d) signv ->
+ let d = if variable_opacity id then (id,None,t) else d in
+ Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
(* Global references. *)
@@ -378,12 +384,6 @@ let mind_oper_of_id sp id mib =
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 ->
diff --git a/library/declare.mli b/library/declare.mli
index 968be059..938bfd06 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declare.mli,v 1.74.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declare.mli 7941 2006-01-28 23:07:59Z herbelin $ i*)
(*i*)
open Names
@@ -36,42 +36,29 @@ 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 variable_declaration = dir_path * section_variable_entry * logical_kind
val declare_variable : variable -> 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
+type constant_declaration = constant_entry * logical_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_constant :
+ identifier -> constant_declaration -> constant
val declare_internal_constant :
- identifier -> constant_declaration -> object_name
-
-val redeclare_constant :
- identifier -> Dischargedhypsmap.discharged_hyps ->
- Cooking.recipe * global_kind -> unit
+ identifier -> constant_declaration -> constant
(* [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
@@ -79,24 +66,20 @@ val string_of_strength : strength -> string
val is_constant : section_path -> bool
val constant_strength : section_path -> strength
-val constant_kind : section_path -> global_kind
+val constant_kind : section_path -> logical_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 variable_kind : variable -> logical_kind
val find_section_variable : variable -> section_path
val last_section_hyps : dir_path -> identifier list
-val clear_proofs : named_context -> named_context
+val clear_proofs : named_context -> Environ.named_context_val
(*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_constant : (bool * constant -> unit) -> unit
val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 2e8fb0a7..3b2196a5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*)
+(*i $Id: declaremods.ml 7720 2005-12-24 00:25:55Z herbelin $ i*)
open Pp
open Util
@@ -17,6 +17,7 @@ open Libnames
open Libobject
open Lib
open Nametab
+open Mod_subst
(* modules and components *)
@@ -372,19 +373,25 @@ let (in_modtype,out_modtype) =
-let replace_module_object id (subst, mbids, msid, lib_stack) modobjs =
+let rec replace_module_object idl (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' ->
+ let rec replace_idl = function
+ | _,[] -> []
+ | id::idl,(id',obj)::tail when id = id' ->
if object_tag obj = "MODULE" then
- (id, in_module (None,modobjs,None))::tail
+ (match idl with
+ [] -> (id, in_module (None,modobjs,None))::tail
+ | _ ->
+ let (_,substobjs,_) = out_module obj in
+ let substobjs' = replace_module_object idl substobjs modobjs in
+ (id, in_module (None,substobjs',None))::tail
+ )
else error "MODULE expected!"
- | lobj::tail -> lobj::replace_id tail
+ | idl,lobj::tail -> lobj::replace_idl (idl,tail)
in
- (subst, mbids, msid, replace_id lib_stack)
+ (subst, mbids, msid, replace_idl (idl,lib_stack))
let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
(subst, mbids1@mbids2, msid, lib_stack)
@@ -396,10 +403,10 @@ let rec get_modtype_substobjs = function
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)) ->
+ | MTEwith (mty, With_Module (idl,mp)) ->
let substobjs = get_modtype_substobjs mty in
let modobjs = MPmap.find mp !modtab_substobjs in
- replace_module_object id substobjs modobjs
+ replace_module_object idl substobjs modobjs
| MTEsig (msid,_) ->
todo "Anonymous module types"; (empty_subst, [], msid, [])
@@ -449,7 +456,7 @@ let intern_args interp_modtype (env,oldargs) (idl,arg) =
in
env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
-let start_module interp_modtype id args res_o =
+let start_module interp_modtype export id args res_o =
let fs = Summary.freeze_summaries () in
let env = Global.env () in
let env,arg_entries_revlist =
@@ -481,7 +488,7 @@ let start_module interp_modtype id args res_o =
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
+ let prefix = Lib.start_module export id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
Lib.add_frozen_state ()
@@ -565,7 +572,6 @@ 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);
@@ -697,21 +703,25 @@ let declare_modtype interp_modtype id args mty =
ignore (add_leaf id (in_modtype (Some entry, substobjs)))
-
-let rec get_module_substobjs = function
+let rec get_module_substobjs env = function
| MEident mp -> MPmap.find mp !modtab_substobjs
| MEfunctor (mbid,mty,mexpr) ->
- let (subst, mbids, msid, objs) =
- get_module_substobjs mexpr
- in
+ let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
(subst, mbid::mbids, msid, objs)
| MEstruct (msid,_) ->
(empty_subst, [], msid, [])
| MEapply (mexpr, MEident mp) ->
- let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+ let feb,ftb = Mod_typing.translate_mexpr env mexpr in
+ let ftb = Modops.scrape_modtype env ftb in
+ let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in
+ let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
(match mbids with
| mbid::mbids ->
- (add_mbid mbid mp subst, mbids, msid, objs)
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp env in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
| [] -> match mexpr with
| MEident _ | MEstruct _ -> error "Application of a non-functor"
| _ -> error "Application of a functor with too few arguments")
@@ -757,7 +767,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
let substobjs =
match entry with
| {mod_entry_type = Some mte} -> get_modtype_substobjs mte
- | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
+ | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
| _ -> anomaly "declare_module: No type, no body ..."
in
Summary.unfreeze_summaries fs;
@@ -772,23 +782,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
(*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 iter_all_segments f =
let _ =
MPmap.iter
(fun _ (prefix,objects) ->
@@ -798,13 +792,11 @@ let iter_all_segments insec f =
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 "[]"
@@ -816,5 +808,3 @@ let debug_print_modtab _ =
in
let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in
hov 0 modules
-
-
diff --git a/library/declaremods.mli b/library/declaremods.mli
index f896310a..481809fc 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.mli,v 1.8.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: declaremods.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
(*i*)
open Util
@@ -43,9 +43,8 @@ val declare_module :
'modexpr option -> unit
val start_module : (env -> 'modtype -> module_type_entry) ->
- identifier ->
- (identifier located list * 'modtype) list -> ('modtype * bool) option ->
- unit
+ bool option -> identifier -> (identifier located list * 'modtype) list ->
+ ('modtype * bool) option -> unit
val end_module : identifier -> unit
@@ -97,14 +96,12 @@ val really_import_module : module_path -> unit
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. *)
+(*s [iter_all_segments] iterate over all segments, the modules'
+ segments first and then the current segment. Modules are presented
+ in an arbitrary order. The given function is applied to all leaves
+ (together with their section path). *)
-val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a
-val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
+val iter_all_segments : (object_name -> obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.std_ppcmds
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 59a01d81..2a3abda8 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dischargedhypsmap.ml,v 1.3.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: dischargedhypsmap.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
open Util
open Libnames
@@ -24,13 +24,16 @@ type discharged_hyps = section_path list
let discharged_hyps_map = ref Spmap.empty
-let cache_discharged_hyps_map (_,(sp,hyps)) =
+let load_discharged_hyps_map _ (_,(sp,hyps)) =
discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+let cache_discharged_hyps_map o =
+ load_discharged_hyps_map 1 o
+
let (in_discharged_hyps_map, _) =
declare_object { (default_object "DISCHARGED-HYPS-MAP") with
cache_function = cache_discharged_hyps_map;
- load_function = (fun _ -> cache_discharged_hyps_map);
+ load_function = load_discharged_hyps_map;
export_function = (fun x -> Some x) }
let set_discharged_hyps sp hyps =
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index 8851e5a3..9a3259ce 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: dischargedhypsmap.mli,v 1.2.8.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: dischargedhypsmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Libnames
diff --git a/library/global.ml b/library/global.ml
index 8694d7af..b4d3a7ff 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *)
+(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
open Util
open Names
@@ -39,6 +39,7 @@ let _ =
let universes () = universes (env())
let named_context () = named_context (env())
+let named_context_val () = named_context_val (env())
let push_named_assum a =
let (cst,env) = push_named_assum a !global_env in
@@ -134,14 +135,14 @@ let env_of_context hyps =
open Libnames
let type_of_reference env = function
- | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
+ | VarRef id -> Environ.named_type id env
| ConstRef c -> Environ.constant_type env c
- | IndRef ind -> Inductive.type_of_inductive env ind
- | ConstructRef cstr -> Inductive.type_of_constructor env cstr
+ | IndRef ind ->
+ let specif = Inductive.lookup_mind_specif env ind in
+ Inductive.type_of_inductive specif
+ | ConstructRef cstr ->
+ let specif =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+ Inductive.type_of_constructor cstr specif
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
index 007986d1..278b9e65 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: global.mli,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*)
+(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*)
(*i*)
open Names
@@ -29,7 +29,10 @@ open Safe_typing
val safe_env : unit -> safe_environment
val env : unit -> Environ.env
+val env_is_empty : unit -> bool
+
val universes : unit -> universes
+val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Sign.named_context
val env_is_empty : unit -> bool
@@ -42,7 +45,7 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints
functions verify that given names match those generated by kernel *)
val add_constant :
- dir_path -> identifier -> global_declaration -> kernel_name
+ dir_path -> identifier -> global_declaration -> constant
val add_mind :
dir_path -> identifier -> mutual_inductive_entry -> kernel_name
@@ -51,7 +54,7 @@ val add_modtype : identifier -> module_type_entry -> kernel_name
val add_constraints : constraints -> unit
-val set_engagement : Environ.engagement -> unit
+val set_engagement : engagement -> unit
(*s Interactive modules and module types *)
(* Both [start_*] functions take the [dir_path] argument to create a
@@ -93,5 +96,5 @@ val import : compiled_library -> Digest.t -> module_path
* environment and a given context. *)
val type_of_global : Libnames.global_reference -> types
-val env_of_context : Sign.named_context -> Environ.env
+val env_of_context : Environ.named_context_val -> Environ.env
diff --git a/library/goptions.ml b/library/goptions.ml
index bcb4fb79..c220544c 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: goptions.ml,v 1.22.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: goptions.ml 6304 2004-11-16 15:49:08Z sacerdot $ *)
(* This module manages customization parameters at the vernacular level *)
@@ -17,6 +17,7 @@ open Names
open Libnames
open Term
open Nametab
+open Mod_subst
(****************************************************************************)
(* 0- Common things *)
diff --git a/library/goptions.mli b/library/goptions.mli
index bbf5357a..16744ec4 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: goptions.mli,v 1.10.6.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: goptions.mli 6304 2004-11-16 15:49:08Z sacerdot $ i*)
(* This module manages customization parameters at the vernacular level *)
@@ -59,6 +59,7 @@ open Names
open Libnames
open Term
open Nametab
+open Mod_subst
(*i*)
(*s Things common to tables and options. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 8a9429a4..08ae2aa5 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: impargs.ml,v 1.59.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
open Util
open Names
@@ -27,63 +27,44 @@ open Topconstr
(* les implicites sont stricts par défaut en v8 *)
let implicit_args = ref false
-let strict_implicit_args = ref (not !Options.v7)
+let strict_implicit_args = ref true
let contextual_implicit_args = ref false
-let implicit_args_out = ref false
-let strict_implicit_args_out = ref true
-let contextual_implicit_args_out = ref false
-
let make_implicit_args flag =
- implicit_args := flag;
- if not !Options.v7_only then implicit_args_out := flag;
- if !Options.translate_strict_impargs then
- strict_implicit_args_out := not flag
+ implicit_args := flag
let make_strict_implicit_args flag =
- strict_implicit_args := flag;
- if not !Options.v7_only then strict_implicit_args_out := flag
+ strict_implicit_args := flag
let make_contextual_implicit_args flag =
- contextual_implicit_args := flag;
- if not !Options.v7_only then contextual_implicit_args_out := flag
+ contextual_implicit_args := flag
let is_implicit_args () = !implicit_args
-let is_implicit_args_out () = !implicit_args_out
let is_strict_implicit_args () = !strict_implicit_args
let is_contextual_implicit_args () = !contextual_implicit_args
-type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
+type implicits_flags = bool * bool * bool
+
+let implicits_flags () =
+ (!implicit_args, !strict_implicit_args, !contextual_implicit_args)
-let with_implicits ((a,b,c),(d,e,g)) f x =
+let with_implicits (a,b,c) f x =
let oa = !implicit_args in
let ob = !strict_implicit_args in
let oc = !contextual_implicit_args in
- let od = !implicit_args_out in
- let oe = !strict_implicit_args_out in
- let og = !contextual_implicit_args_out in
try
implicit_args := a;
strict_implicit_args := b;
contextual_implicit_args := c;
- implicit_args_out := d;
- strict_implicit_args_out := e;
- contextual_implicit_args_out := g;
let rslt = f x in
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;
rslt
with e -> 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
@@ -135,7 +116,7 @@ let update pos rig (na,st) =
| 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) ->
+ | Some (DepFlex fpos) ->
if argument_less (pos,fpos) or pos=fpos then DepRigid pos
else DepFlexAndRigid (fpos,pos)
| Some Manual -> assert false
@@ -213,13 +194,9 @@ let compute_implicits_gen strict contextual env t =
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 compute_implicits env t =
+ let strict = !strict_implicit_args in
+ let contextual = !contextual_implicit_args in
let l = compute_implicits_gen strict contextual env t in
List.map (function
| (Name id, Some imp) -> Some (id,imp)
@@ -267,20 +244,11 @@ type implicits =
| 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
+ if !implicit_args then
+ let l = compute_implicits env ty in
+ Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
+ else
+ No_impl
let list_of_implicits = function
| Impl_auto (_,_,l) -> l
@@ -289,7 +257,7 @@ let list_of_implicits = function
(*s Constants. *)
-let constants_table = ref KNmap.empty
+let constants_table = ref Cmap.empty
let compute_constant_implicits kn =
let env = Global.env () in
@@ -297,7 +265,7 @@ let compute_constant_implicits kn =
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
+ try Cmap.find sp !constants_table with Not_found -> No_impl
(*s Inductives and constructors. Their implicit arguments are stored
in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -326,10 +294,11 @@ let compute_mib_implicits kn =
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
+ try Indmap.find indp !inductives_table with Not_found -> No_impl
let constructor_implicits consp =
- try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl
+ try Constrmap.find consp !constructors_table with Not_found -> No_impl
+
(*s Variables. *)
let var_table = ref Idmap.empty
@@ -340,7 +309,17 @@ let compute_var_implicits id =
auto_implicits env ty
let var_implicits id =
- try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+ try Idmap.find id !var_table with Not_found -> No_impl
+
+(* 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)
(* Caching implicits *)
@@ -349,16 +328,19 @@ let cache_implicits_decl (r,imps) =
| VarRef id ->
var_table := Idmap.add id imps !var_table
| ConstRef kn ->
- constants_table := KNmap.add kn imps !constants_table
+ constants_table := Cmap.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 load_implicits _ (_,l) = List.iter cache_implicits_decl l
+
+let cache_implicits o =
+ load_implicits 1 o
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 r' = fst (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
@@ -366,40 +348,27 @@ let subst_implicits (_,subst,l) =
let (in_implicits, _) =
declare_object {(default_object "IMPLICITS") with
cache_function = cache_implicits;
- load_function = (fun _ -> cache_implicits);
+ load_function = load_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))
+ (true,!strict_implicit_args,!contextual_implicit_args)
declare_implicits_gen r
let declare_var_implicits id =
- if !implicit_args or !implicit_args_out then
- declare_implicits_gen (VarRef id)
+ if !implicit_args then declare_implicits_gen (VarRef id)
let declare_constant_implicits kn =
- if !implicit_args or !implicit_args_out then
- declare_implicits_gen (ConstRef kn)
+ if !implicit_args then declare_implicits_gen (ConstRef kn)
let declare_mib_implicits kn =
- if !implicit_args or !implicit_args_out then
+ if !implicit_args then
let imps = compute_mib_implicits kn in
let imps = array_map_to_list
(fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
@@ -412,28 +381,10 @@ let implicits_of_global_gen = function
| 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
+ list_of_implicits (implicits_of_global_gen r)
(* 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)
@@ -443,15 +394,13 @@ let declare_manual_implicits r l =
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
+ try list_remove_first (ExplByPos k) l, set_implicit id imp
with Not_found ->
- try list_remove (ExplByName id) l, set_implicit id imp
+ try list_remove_first (ExplByName id) l, set_implicit id imp
with Not_found ->
l, None in
imp :: merge (k+1) l' imps
@@ -470,8 +419,6 @@ let declare_manual_implicits r l =
(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 *)
@@ -481,11 +428,11 @@ let test = function
| 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)
+ try let b = find a in test b
+ with Not_found -> (false,false,false)
let is_implicit_constant sp =
- test_if_implicit (KNmap.find sp) !constants_table
+ test_if_implicit (Cmap.find sp) !constants_table
let is_implicit_inductive_definition indp =
test_if_implicit (Indmap.find (indp,0)) !inductives_table
@@ -496,7 +443,7 @@ let is_implicit_var id =
(*s Registration as global tables *)
let init () =
- constants_table := KNmap.empty;
+ constants_table := Cmap.empty;
inductives_table := Indmap.empty;
constructors_table := Constrmap.empty;
var_table := Idmap.empty
@@ -518,34 +465,3 @@ let _ =
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
index 8db04ee7..671d195c 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: impargs.mli,v 1.26.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: impargs.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
(*i*)
open Names
@@ -43,7 +43,7 @@ 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
+val compute_implicits : env -> types -> implicits_list
(*s Computation of implicits (done using the global environment). *)
@@ -64,6 +64,4 @@ 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
+val implicits_flags : unit -> implicits_flags
diff --git a/library/lib.ml b/library/lib.ml
index c46634f4..ee553cad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml,v 1.63.2.4 2005/11/04 09:02:38 herbelin Exp $ *)
+(* $Id: lib.ml 7710 2005-12-23 10:16:42Z herbelin $ *)
open Pp
open Util
@@ -21,11 +21,10 @@ open Summary
type node =
| Leaf of obj
| CompilingLibrary of object_prefix
- | OpenedModule of object_prefix * Summary.frozen
+ | OpenedModule of bool option * object_prefix * Summary.frozen
| OpenedModtype of object_prefix * Summary.frozen
| OpenedSection of object_prefix * Summary.frozen
- (* bool is to tell if the section must be opened automatically *)
- | ClosedSection of bool * dir_path * library_segment
+ | ClosedSection
| FrozenState of Summary.frozen
and library_entry = object_name * node
@@ -51,7 +50,7 @@ let subst_objects prefix subst 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 ->
+ | ((sp,kn as oname),Leaf o) :: stk ->
let id = id_of_label (label kn) in
(match classify_object (oname,o) with
| Dispose -> clean acc stk
@@ -61,7 +60,7 @@ let classify_segment seg =
clean ((id,o')::substl, keepl, anticipl) stk
| Anticipate o' ->
clean (substl, keepl, o'::anticipl) stk)
- | (oname,ClosedSection _ as item) :: stk -> clean acc stk
+ | (oname,ClosedSection) :: 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"
@@ -105,6 +104,10 @@ let make_kn id =
let mp,dir = current_prefix () in
Names.make_kn mp dir (label_of_id id)
+let make_con id =
+ let mp,dir = current_prefix () in
+ Names.make_con mp dir (label_of_id id)
+
let make_oname id = make_path id, make_kn id
@@ -121,7 +124,7 @@ let sections_are_opened () =
let recalc_path_prefix () =
let rec recalc = function
| (sp, OpenedSection (dir,_)) :: _ -> dir
- | (sp, OpenedModule (dir,_)) :: _ -> dir
+ | (sp, OpenedModule (_,dir,_)) :: _ -> dir
| (sp, OpenedModtype (dir,_)) :: _ -> dir
| (sp, CompilingLibrary dir) :: _ -> dir
| _::l -> recalc l
@@ -180,6 +183,8 @@ let add_absolutely_named_leaf sp obj =
add_entry sp (Leaf obj)
let add_leaf id obj =
+ if fst (current_prefix ()) = initial_path then
+ error ("No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
add_entry oname (Leaf obj);
@@ -211,29 +216,13 @@ let is_something_opened = function
| (_,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 start_module export 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));
+ add_entry oname (OpenedModule (export,prefix,nametab));
path_prefix := prefix;
prefix
(* add_frozen_state () must be called in declaremods *)
@@ -241,7 +230,7 @@ let start_module id mp nametab =
let end_module id =
let oname,nametab =
try match find_entry_p is_something_opened with
- | oname,OpenedModule (_,nametab) ->
+ | 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";
@@ -379,6 +368,70 @@ let is_module () =
(* Returns the most recent OpenedThing node *)
let what_is_opened () = find_entry_p is_something_opened
+(* Discharge tables *)
+
+let sectab =
+ ref ([] : (identifier list *
+ (identifier array Cmap.t * identifier array KNmap.t) *
+ (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list)
+
+let add_section () =
+ sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+
+let add_section_variable id =
+ match !sectab with
+ | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+ | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+
+let rec extract_hyps = function
+ | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | (id::idl,hyps) -> extract_hyps (idl,hyps)
+ | [], _ -> []
+
+let add_section_replacement f g hyps =
+ match !sectab with
+ | [] -> ()
+ | (vars,exps,abs)::sl ->
+ let sechyps = extract_hyps (vars,hyps) in
+ let args = Sign.instance_from_named_context (List.rev sechyps) in
+ sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+
+let add_section_kn kn =
+ let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+ add_section_replacement f f
+
+let add_section_constant kn =
+ let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+ add_section_replacement f f
+
+let replacement_context () = pi2 (List.hd !sectab)
+
+let section_segment = function
+ | VarRef id ->
+ []
+ | ConstRef con ->
+ Cmap.find con (fst (pi3 (List.hd !sectab)))
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ KNmap.find kn (snd (pi3 (List.hd !sectab)))
+
+let section_instance r =
+ Sign.instance_from_named_context (List.rev (section_segment r))
+
+let init () = sectab := []
+let freeze () = !sectab
+let unfreeze s = sectab := s
+
+let _ =
+ Summary.declare_summary "section-context"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+(*************)
+(* Sections. *)
+
(* XML output hooks *)
let xml_open_section = ref (fun id -> ())
let xml_close_section = ref (fun id -> ())
@@ -386,8 +439,6 @@ 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
@@ -401,12 +452,19 @@ let open_section id =
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
path_prefix := prefix;
if !Options.xml_export then !xml_open_section id;
- prefix
+ add_section ()
(* Restore lib_stk and summaries as before the section opening, and
add a ClosedSection object. *)
-let close_section ~export id =
+
+let discharge_item = function
+ | ((sp,_ as oname),Leaf lobj) ->
+ option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ | _ ->
+ None
+
+let close_section id =
let oname,fs =
try match find_entry_p is_something_opened with
| oname,OpenedSection (_,fs) ->
@@ -417,25 +475,26 @@ let close_section ~export id =
with Not_found ->
error "no opened section"
in
- let (after,_,before) = split_lib oname in
+ let (secdecls,_,before) = split_lib oname in
lib_stk := before;
- let prefix = !path_prefix in
+ let full_olddir = fst !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;
+ add_entry (make_oname id) ClosedSection;
if !Options.xml_export then !xml_close_section id;
- (prefix, after, fs)
+ let newdecls = List.map discharge_item secdecls in
+ Summary.section_unfreeze_summaries fs;
+ List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+ Cooking.clear_cooking_sharing ();
+ Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+(*****************)
(* Backtracking. *)
let recache_decl = function
| (sp, Leaf o) -> cache_object (sp,o)
+ | (_,OpenedSection _) -> add_section ()
| _ -> ()
-
let recache_context ctx =
List.iter recache_decl ctx
@@ -463,7 +522,7 @@ let reset_name (loc,id) =
let is_mod_node = function
| OpenedModule _ | OpenedModtype _ | OpenedSection _
- | ClosedSection _ -> true
+ | ClosedSection -> true
| Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
| _ -> false
@@ -471,7 +530,7 @@ let is_mod_node = function
the same name *)
let reset_mod (loc,id) =
- let (ent,before) =
+ let (_,before) =
try
find_split_p (fun (sp,node) ->
let (_,spi) = repr_path (fst sp) in id = spi
@@ -489,15 +548,29 @@ let reset_mod (loc,id) =
recache_context after
-let point_obj =
- let (f,_) = declare_object {(default_object "DOT") with
- classify_function = (fun _ -> Dispose)} in
- f()
+let (inLabel,outLabel) =
+ declare_object {(default_object "DOT") with
+ classify_function = (fun _ -> Dispose)}
-let mark_end_of_command () =
- match !lib_stk with
- (_,Leaf o)::_ when object_tag o = "DOT" -> ()
- | _ -> add_anonymous_leaf point_obj
+let mark_end_of_command, current_command_label, set_command_label =
+ let n = ref 0 in
+ (fun () ->
+ match !lib_stk with
+ (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+ | _ -> incr n;add_anonymous_leaf (inLabel !n)),
+ (fun () -> !n),
+ (fun x -> n:=x)
+
+let rec reset_label_stk n stk =
+ match stk with
+ (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp
+ | _::tail -> reset_label_stk n tail
+ | [] -> error "Unknown state number"
+
+let reset_label n =
+ let res = reset_label_stk n !lib_stk in
+ set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
+ reset_to res
let rec back_stk n stk =
match stk with
@@ -543,6 +616,7 @@ let reset_initial () =
| (_,[_,FrozenState fs as hd],before) ->
lib_stk := hd::before;
recalc_path_prefix ();
+ set_command_label 0;
unfreeze_summaries fs
| _ -> assert false
end
@@ -564,14 +638,39 @@ let library_part ref =
(* Theorem/Lemma outside its outer section of definition *)
dir
+(************************)
+(* Discharging names *)
+
+let pop_kn kn =
+ let (mp,dir,l) = Names.repr_kn kn in
+ Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con =
+ let (mp,dir,l) = Names.repr_con con in
+ Names.make_con mp (dirpath_prefix dir) l
+
+let con_defined_in_sec kn =
+ let _,dir,_ = repr_con kn in
+ dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let defined_in_sec kn =
+ let _,dir,_ = repr_kn kn in
+ dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let discharge_global = function
+ | ConstRef kn when con_defined_in_sec kn ->
+ ConstRef (pop_con kn)
+ | IndRef (kn,i) when defined_in_sec kn ->
+ IndRef (pop_kn kn,i)
+ | ConstructRef ((kn,i),j) when defined_in_sec kn ->
+ ConstructRef ((pop_kn kn,i),j)
+ | r -> r
+
+let discharge_kn kn =
+ if defined_in_sec kn then pop_kn kn else kn
-let rec file_of_mp = function
- | MPfile dir -> Some dir
- | MPself _ -> Some (library_dp ())
- | MPbound _ -> None
- | MPdot (mp,_) -> file_of_mp mp
+let discharge_con cst =
+ if con_defined_in_sec cst then pop_con cst else cst
-let file_part = function
- | VarRef id -> anomaly "TODO";
- | ConstRef kn | ConstructRef ((kn,_),_) | IndRef (kn,_) ->
- file_of_mp (modpath kn)
+let discharge_inductive (kn,i) =
+ (discharge_kn kn,i)
diff --git a/library/lib.mli b/library/lib.mli
index aa874470..22b6b6d8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lib.mli,v 1.41.2.3 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: lib.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
(*i*)
open Util
@@ -14,6 +14,7 @@ open Names
open Libnames
open Libobject
open Summary
+open Mod_subst
(*i*)
(*s This module provides a general mechanism to keep a trace of all operations
@@ -23,10 +24,10 @@ open Summary
type node =
| Leaf of obj
| CompilingLibrary of object_prefix
- | OpenedModule of object_prefix * Summary.frozen
+ | OpenedModule of bool option * object_prefix * Summary.frozen
| OpenedModtype of object_prefix * Summary.frozen
| OpenedSection of object_prefix * Summary.frozen
- | ClosedSection of bool * dir_path * library_segment
+ | ClosedSection
| FrozenState of Summary.frozen
and library_segment = (object_name * node) list
@@ -65,7 +66,8 @@ val add_leaves : identifier -> obj list -> object_name
val add_frozen_state : unit -> unit
val mark_end_of_command : unit -> unit
-
+val current_command_label : unit -> int
+val reset_label : int -> unit
(*s The function [contents_after] returns the current library segment,
starting from a given section path. If not given, the entire segment
@@ -82,6 +84,7 @@ val make_path : identifier -> section_path
(* Kernel-side names *)
val current_prefix : unit -> module_path * dir_path
val make_kn : identifier -> kernel_name
+val make_con : identifier -> constant
(* Are we inside an opened section *)
val sections_are_opened : unit -> bool
@@ -99,7 +102,7 @@ val what_is_opened : unit -> object_name * node
(*s Modules and module types *)
val start_module :
- module_ident -> module_path -> Summary.frozen -> object_prefix
+ bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
val end_module : module_ident
-> object_name * object_prefix * Summary.frozen * library_segment
@@ -121,15 +124,10 @@ 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
-(* Extract the library part of a name if not in a functor *)
-val file_part : global_reference -> dir_path option
-
(*s Sections *)
-val open_section : identifier -> object_prefix
-
-val close_section : export:bool -> identifier ->
- object_prefix * library_segment * Summary.frozen
+val open_section : identifier -> unit
+val close_section : identifier -> unit
(*s Backtracking (undo). *)
@@ -157,3 +155,24 @@ val reset_initial : unit -> unit
(* XML output hooks *)
val set_xml_open_section : (identifier -> unit) -> unit
val set_xml_close_section : (identifier -> unit) -> unit
+
+
+(*s Section management for discharge *)
+
+val section_segment : global_reference -> Sign.named_context
+val section_instance : global_reference -> Term.constr array
+
+val add_section_variable : identifier -> unit
+val add_section_constant : constant -> Sign.named_context -> unit
+val add_section_kn : kernel_name -> Sign.named_context -> unit
+val replacement_context : unit ->
+ (identifier array Cmap.t * identifier array KNmap.t)
+
+(*s Discharge: decrease the section level if in the current section *)
+
+val discharge_kn : kernel_name -> kernel_name
+val discharge_con : constant -> constant
+val discharge_global : global_reference -> global_reference
+val discharge_inductive : inductive -> inductive
+
+
diff --git a/library/libnames.ml b/library/libnames.ml
index 16f5a917..536a382d 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.ml,v 1.11.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: libnames.ml 7052 2005-05-20 15:54:50Z herbelin $ i*)
open Pp
open Util
open Names
open Nameops
open Term
+open Mod_subst
type global_reference =
| VarRef of variable
@@ -21,30 +22,34 @@ type global_reference =
| ConstructRef of constructor
let subst_global subst ref = match ref with
- | VarRef _ -> ref
+ | VarRef var -> ref, mkVar var
| ConstRef kn ->
- let kn' = subst_kn subst kn in if kn==kn' then ref else
- ConstRef kn'
+ let kn',t = subst_con subst kn in
+ if kn==kn' then ref, mkConst kn else ConstRef kn', t
| IndRef (kn,i) ->
- let kn' = subst_kn subst kn in if kn==kn' then ref else
- IndRef(kn',i)
+ let kn' = subst_kn subst kn in
+ if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
| ConstructRef ((kn,i),j) ->
- let kn' = subst_kn subst kn in if kn==kn' then ref else
- ConstructRef ((kn',i),j)
+ let kn' = subst_kn subst kn in
+ if kn==kn' then ref, mkConstruct ((kn,i),j)
+ else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
-let reference_of_constr c = match kind_of_term c with
+let global_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
+let constr_of_global = function
| VarRef id -> mkVar id
| ConstRef sp -> mkConst sp
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
+let constr_of_reference = constr_of_global
+let reference_of_constr = global_of_constr
+
module RefOrdered =
struct
type t = global_reference
@@ -54,24 +59,8 @@ module RefOrdered =
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))
@@ -188,18 +177,10 @@ 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 encode_con dir id = make_con (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
@@ -207,6 +188,13 @@ let decode_kn kn =
| _ , [] -> anomaly "MPfile expected!"
| _ -> anomaly "Section part should be empty!"
+let decode_con kn =
+ let mp,sec_dir,l = repr_con 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
@@ -267,3 +255,4 @@ let pr_reference = function
let loc_of_reference = function
| Qualid (loc,qid) -> loc
| Ident (loc,id) -> loc
+
diff --git a/library/libnames.mli b/library/libnames.mli
index a6055428..06595e81 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.mli,v 1.8.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: libnames.mli 7052 2005-05-20 15:54:50Z herbelin $ i*)
(*i*)
open Pp
open Util
open Names
open Term
+open Mod_subst
(*i*)
(*s Global reference is a kernel side type for all references together *)
@@ -22,21 +23,22 @@ type global_reference =
| IndRef of inductive
| ConstructRef of constructor
-val subst_global : substitution -> global_reference -> global_reference
+val subst_global : substitution -> global_reference -> global_reference * constr
(* Turn a global reference into a construction *)
-val constr_of_reference : global_reference -> constr
+val constr_of_global : global_reference -> constr
+
+(* Turn a construction denoting a global reference into a global reference;
+ raise [Not_found] if not a global reference *)
+val global_of_constr : constr -> global_reference
-(* Turn a construction denoting a global into a reference;
- raise [Not_found] if not a global *)
+(* Obsolete synonyms for constr_of_global and global_of_constr *)
+val constr_of_reference : global_reference -> constr
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
@@ -82,13 +84,12 @@ 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
+val encode_con : dir_path -> identifier -> constant
+val decode_con : constant -> dir_path * identifier
(*s A [qualid] is a partially qualified ident; it includes fully
diff --git a/library/libobject.ml b/library/libobject.ml
index 2e531e05..708c19b1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: libobject.ml,v 1.8.8.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: libobject.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
open Util
open Names
open Libnames
+open Mod_subst
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
@@ -35,6 +36,7 @@ type 'a object_declaration = {
open_function : int -> object_name * 'a -> unit;
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
+ discharge_function : object_name * 'a -> 'a option;
export_function : 'a -> 'a option }
let yell s = anomaly s
@@ -47,6 +49,7 @@ let default_object s = {
subst_function = (fun _ ->
yell ("The object "^s^" does not know how to substitute!"));
classify_function = (fun (_,obj) -> Keep obj);
+ discharge_function = (fun _ -> None);
export_function = (fun _ -> None)}
@@ -71,6 +74,7 @@ type dynamic_object_declaration = {
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_discharge_function : object_name * obj -> obj option;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
@@ -103,6 +107,11 @@ let declare_object odecl =
| Anticipate (obj) -> Anticipate (infun obj)
else
anomaly "somehow we got the wrong dynamic object in the classifyfun"
+ and discharge (oname,lobj) =
+ if Dyn.tag lobj = na then
+ option_app infun (odecl.discharge_function (oname,outfun lobj))
+ else
+ anomaly "somehow we got the wrong dynamic object in the dischargefun"
and exporter lobj =
if Dyn.tag lobj = na then
option_app infun (odecl.export_function (outfun lobj))
@@ -115,6 +124,7 @@ let declare_object odecl =
dyn_open_function = opener;
dyn_subst_function = substituter;
dyn_classify_function = classifier;
+ dyn_discharge_function = discharge;
dyn_export_function = exporter };
(infun,outfun)
@@ -153,5 +163,8 @@ let subst_object ((_,_,lobj) as node) =
let classify_object ((_,lobj) as node) =
apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
+let discharge_object ((_,lobj) as node) =
+ apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
+
let export_object lobj =
apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index b9070f5d..88a12db9 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libobject.mli,v 1.9.8.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: libobject.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
(*i*)
open Names
open Libnames
+open Mod_subst
(*i*)
(* [Libobject] declares persistent objects, given with methods:
@@ -69,6 +70,7 @@ type 'a object_declaration = {
open_function : int -> object_name * 'a -> unit;
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
+ discharge_function : object_name * 'a -> 'a option;
export_function : 'a -> 'a option }
(* The default object is a "Keep" object with empty methods.
@@ -102,4 +104,5 @@ 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 discharge_object : object_name * obj -> obj option
val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index aaed4545..760b6f07 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml,v 1.79.2.5 2006/01/10 17:06:23 barras Exp $ *)
+(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
open Pp
open Util
@@ -25,30 +25,57 @@ open Declaremods
type logical_path = dir_path
-let load_path = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : System.physical_path list * logical_path list)
-let get_load_path () = fst !load_path
+let get_load_paths () = fst !load_paths
+
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p =
+ let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+ let n = String.length curdir in
+ if String.length p > 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 = System.canonical_path_name phys_dir in
- match list_filter2 (fun p d -> p = phys_dir) !load_path with
+ let phys_dir = canonical_path_name phys_dir in
+ match list_filter2 (fun p d -> p = phys_dir) !load_paths with
| _,[dir] -> dir
| _,[] -> Nameops.default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
-let remove_path dir =
- let dir = System.canonical_path_name dir in
- load_path := list_filter2 (fun p d -> p <> dir) !load_path
+let remove_load_path dir =
+ load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
-let add_load_path_entry (phys_path,coq_path) =
- let phys_path = System.canonical_path_name phys_path in
- match list_filter2 (fun p d -> p = phys_path) !load_path with
+let add_load_path (phys_path,coq_path) =
+ let phys_path = canonical_path_name phys_path in
+ match list_filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
&& not
- (phys_path = System.canonical_path_name Filename.current_dir_name
+ (phys_path = canonical_path_name Filename.current_dir_name
&& coq_path = Nameops.default_root_prefix)
then
begin
@@ -58,19 +85,19 @@ let add_load_path_entry (phys_path,coq_path) =
^(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)
+ remove_load_path phys_path;
+ load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
end
| _,[] ->
- load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+ load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
| _ -> 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 load_paths_of_dir_path dir =
+ fst (list_filter2 (fun p d -> d = dir) !load_paths)
-let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
+let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
(************************************************************************)
(*s Modules on disk contain the following informations (after the magic
@@ -97,7 +124,7 @@ type library_t = {
library_imports : compilation_unit_name list;
library_digest : Digest.t }
-module CompilingLibraryOrdered =
+module LibraryOrdered =
struct
type t = dir_path
let compare d1 d2 =
@@ -105,12 +132,12 @@ module CompilingLibraryOrdered =
(List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
end
-module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered)
+module LibraryMap = Map.Make(LibraryOrdered)
-(* This is a map from names to libraries *)
-let libraries_table = ref CompilingLibraryMap.empty
+(* This is a map from names to loaded libraries *)
+let libraries_table = ref LibraryMap.empty
-(* These are the _ordered_ lists of loaded, imported and exported libraries *)
+(* These are the _ordered_ sets of loaded, imported and exported libraries *)
let libraries_loaded_list = ref []
let libraries_imports_list = ref []
let libraries_exports_list = ref []
@@ -128,7 +155,7 @@ let unfreeze (mt,mo,mi,me) =
libraries_exports_list := me
let init () =
- libraries_table := CompilingLibraryMap.empty;
+ libraries_table := LibraryMap.empty;
libraries_loaded_list := [];
libraries_imports_list := [];
libraries_exports_list := []
@@ -141,18 +168,20 @@ let _ =
Summary.survive_module = false;
Summary.survive_section = false }
-let find_library s =
- CompilingLibraryMap.find s !libraries_table
+(* various requests to the tables *)
-let try_find_library s =
- try find_library s
+let find_library dir =
+ LibraryMap.find dir !libraries_table
+
+let try_find_library dir =
+ try find_library dir
with Not_found ->
- error ("Unknown library " ^ (string_of_dirpath s))
+ error ("Unknown library " ^ (string_of_dirpath dir))
-let library_full_filename m = (find_library m).library_filename
+let library_full_filename dir = (find_library dir).library_filename
let library_is_loaded dir =
- try let _ = CompilingLibraryMap.find dir !libraries_table in true
+ try let _ = find_library dir in true
with Not_found -> false
let library_is_opened dir =
@@ -176,7 +205,7 @@ let register_loaded_library 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
+ libraries_table := LibraryMap.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
@@ -198,10 +227,8 @@ let register_open_library export 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]. *)
+(* [open_library export explicit m] opens library [m] if not already
+ opened _or_ if explicitly asked to be (re)opened *)
let eq_lib_name m1 m2 = m1.library_name = m2.library_name
@@ -219,7 +246,10 @@ let open_library export explicit_libs m =
if export then
libraries_exports_list := remember_last_of_each !libraries_exports_list m
-let open_libraries export modl =
+(* open_libraries recursively open a list of libraries but opens only once
+ a library that is re-exported many times *)
+
+let open_libraries export modl =
let to_open_list =
List.fold_left
(fun l m ->
@@ -261,77 +291,94 @@ let (in_import, out_import) =
(************************************************************************)
-(*s Loading from disk to cache (preparation phase) *)
-
-let vo_magic_number7 = 07993 (* V8.0pl3 final old syntax *)
-let vo_magic_number8 = 08003 (* V8.0pl3 final new syntax *)
+(*s Low-level interning/externing of libraries to files *)
-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"
+(*s Loading from disk to cache (preparation phase) *)
-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 vo_magic_number = 08003 (* V8.0 final new syntax + new params in ind *)
-let raw_extern_library =
- if !Options.v7 then raw_extern_library7 else raw_extern_library8
+let (raw_extern_library, raw_intern_library) =
+ System.raw_extern_intern vo_magic_number ".vo"
-(* cache for loaded libraries *)
-let compunit_cache = ref CompilingLibraryMap.empty
+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 _ =
- 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). *)
+(************************************************************************)
+(*s Locate absolute or partially qualified library names in the path *)
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 *)
+ (* Search in loadpath *)
+ let pref, base = split_dirpath dir in
+ let loadpath = load_paths_of_dir_path pref in
+ if loadpath = [] then raise LibUnmappedDir;
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
+ with Not_found ->
+ (* Last chance, removed from the file system but still in memory *)
+ try
+ (dir, library_full_filename dir)
+ 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 locate_qualified_library qid =
+ try
+ (* Search library in loadpath *)
+ let dir, base = repr_qualid qid in
+ let loadpath =
+ if repr_dirpath dir = [] then get_load_paths ()
+ else
+ (* we assume dir is an absolute dirpath *)
+ load_paths_of_dir_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
+ let dir = extend_dirpath (find_logical_path path) base in
+ (* Look if loaded *)
+ try
+ (LibLoaded, dir, library_full_filename dir)
+ with Not_found ->
+ (LibInPath, dir, file)
+ with Not_found -> raise LibNotFound
+
+let explain_locate_library_error qid = function
+ | LibUnmappedDir ->
+ let prefix, _ = repr_qualid qid in
+ errorlabstrm "load_absolute_library_from"
+ (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
+ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+ | LibNotFound ->
+ errorlabstrm "load_absolute_library_from"
+ (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
+ | e -> raise e
+
+let try_locate_absolute_library dir =
+ try
+ locate_absolute_library dir
+ with e ->
+ explain_locate_library_error (qualid_of_dirpath dir) e
+
+let try_locate_qualified_library (loc,qid) =
+ try
+ let (_,dir,f) = locate_qualified_library qid in
+ dir,f
+ with e ->
+ explain_locate_library_error qid e
+
+
+(************************************************************************)
+(* Internalise libraries *)
let lighten_library m =
if !Options.dont_load_proofs then lighten_library m else m
@@ -352,55 +399,35 @@ let intern_from_file f =
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
+let rec intern_library needed (dir, f) =
+ (* Look if in the current logical environment *)
+ try find_library dir, needed
with Not_found ->
- try
- (* Look if already loaded in cache and consequently its dependencies *)
- CompilingLibraryMap.find dir !compunit_cache
+ (* Look if already listed and consequently its dependencies too *)
+ try List.assoc dir needed, needed
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
+ (* [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);
+ m, intern_library_deps needed dir m
-and intern_mandatory_library caller (dir,d) =
- let m = intern_absolute_library_from dir in
+and intern_library_deps needed dir m =
+ (dir,m)::List.fold_left (intern_mandatory_library dir) needed m.library_deps
+
+and intern_mandatory_library caller needed (dir,d) =
+ let m,needed = intern_library needed (try_locate_absolute_library dir) in
if d <> m.library_digest then
error ("compiled library "^(string_of_dirpath caller)^
" makes inconsistent assumptions over library "
- ^(string_of_dirpath dir))
-
-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
+ ^(string_of_dirpath dir));
+ needed
-let rec_intern_library mref = let _ = intern_library mref in ()
+let rec_intern_library needed mref =
+ let _,needed = intern_library needed mref in needed
let check_library_short_name f dir = function
| Some id when id <> snd (split_dirpath dir) ->
@@ -416,55 +443,18 @@ let rec_intern_by_filename_only id f =
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
+ let m' = find_library m.library_name in
Options.if_verbose warning
((string_of_dirpath m.library_name)^" is already loaded from file "^
m'.library_filename);
- m.library_name
+ 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 =
- try
- (* Search library in loadpath *)
- 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
- let dir = extend_dirpath (find_logical_path path) base in
- (* Look if loaded *)
- try
- (LibLoaded, dir, library_full_filename dir)
- with Not_found ->
- (LibInPath, dir, file)
- 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 needed = intern_library_deps [] m.library_name m in
+ m.library_name, needed
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
+ let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
rec_intern_by_filename_only idopt f
(**********************************************************************)
@@ -472,8 +462,11 @@ let rec_intern_library_from_file idopt f =
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_* )
+ dependencies are read from to disk (using intern_* )
+ [they are read from disk to ensure that at section/module
+ discharging time, the physical library referred to outside the
+ section/module is the one that was used at type-checking time in
+ the section/module]
execution phase: (through add_leaf and cache_require)
the library is loaded in the environment and Nametab, the objects are
@@ -487,117 +480,83 @@ let rec_intern_library_from_file idopt f =
type library_reference = dir_path list * bool option
-let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
+let register_library (dir,m) =
+ Declaremods.register_library
+ m.library_name
+ m.library_compiled
+ m.library_objects
+ m.library_digest;
+ register_loaded_library m
-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)
+ (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require (_,(needed,modl,export)) =
+ List.iter register_library needed;
+ option_iter (fun exp -> open_libraries exp (List.map find_library modl))
+ export
+
+let load_require _ (_,(needed,modl,_)) =
+ List.iter register_library needed
(* 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 export_require (_,l,e) = Some ([],l,e)
+
+let discharge_require (_,o) = Some o
let (in_require, out_require) =
declare_object {(default_object "REQUIRE") with
cache_function = cache_require;
load_function = load_require;
export_function = export_require;
+ discharge_function = discharge_require;
classify_function = (fun (_,o) -> Anticipate o) }
+(* Require libraries, import them if [export <> None], mark them for export
+ if [export = Some true] *)
+
+(* read = require without opening *)
+
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
+let require_library qidl export =
+ let modrefl = List.map try_locate_qualified_library qidl in
+ let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
+ let modrefl = List.map fst modrefl 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
+ add_anonymous_leaf (in_require (needed,modrefl,None));
+ option_iter (fun exp ->
+ List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+ export
end
else
- add_anonymous_leaf (in_require (modrefl,Some export));
+ add_anonymous_leaf (in_require (needed,modrefl,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));
+let require_library_from_file idopt file export =
+ let modref,needed = rec_intern_library_from_file idopt file in
+ let needed = List.rev needed in
+ if Lib.is_modtype () || Lib.is_module () then begin
+ add_anonymous_leaf (in_require (needed,[modref],None));
+ option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+ export
+ end
+ else
+ add_anonymous_leaf (in_require (needed,[modref],export));
if !Options.xml_export then !xml_require modref;
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) =
+let import_module export (loc,qid) =
try
match Nametab.locate_module qid with
MPfile dir ->
if Lib.is_modtype () || Lib.is_module () || not export then
add_anonymous_leaf (in_import (dir, export))
else
- add_anonymous_leaf (in_require ([dir], Some export))
+ add_anonymous_leaf (in_require ([],[dir], Some export))
| mp ->
import_module export mp
with
@@ -607,27 +566,30 @@ let import_library export (loc,qid) =
str ((string_of_qualid qid)^" is not a module"))
(************************************************************************)
-(*s [save_library s] saves the library [m] to the disk. *)
+(*s Initializing the compilation of a library. *)
let start_library f =
let _,longf =
- System.find_file_in_path (get_load_path ()) (f^".v") in
+ System.find_file_in_path (get_load_paths ()) (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
+(************************************************************************)
+(*s [save_library dir] ends library [dir] and save it to the disk. *)
+
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 save_library_to dir f =
+ let cenv, seg = Declaremods.end_library dir in
let md = {
- md_name = s;
+ md_name = dir;
md_compiled = cenv;
md_objects = seg;
md_deps = current_deps ();
@@ -641,33 +603,7 @@ let save_library_to s f =
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
diff --git a/library/library.mli b/library/library.mli
index 18be1671..f7620682 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: library.mli,v 1.23.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: library.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
(*i*)
open Util
@@ -15,65 +15,58 @@ open Libnames
open Libobject
(*i*)
-(*s This module is the heart of the library. It provides low level
- functions to load, open and save libraries. Libraries are saved
- onto the disk with checksums (obtained with the [Digest] module),
- which are checked at loading time to prevent inconsistencies
- between files written at various dates. It also provides a high
- level function [require] which corresponds to the vernacular
- command [Require]. *)
+(*s This module provides functions to load, open and save
+ libraries. Libraries correspond to the subclass of modules that
+ coincide with a file on disk (the ".vo" files). Libraries on the
+ disk comes with checksums (obtained with the [Digest] module), which
+ are checked at loading time to prevent inconsistencies between files
+ written at various dates.
+*)
+
+(*s Require = load in the environment + open (if the optional boolean
+ is not [None]); mark also for export if the boolean is [Some true] *)
+val require_library : qualid located list -> bool option -> unit
+val require_library_from_file :
+ identifier option -> System.physical_path -> bool option -> unit
+
+(*s Open a module (or a library); if the boolean is true then it's also
+ an export otherwise just a simple import *)
+val import_module : bool -> qualid located -> unit
-val read_library : qualid located -> unit
+(*s Start the compilation of a library *)
+val start_library : string -> dir_path * string
-val read_library_from_file : System.physical_path -> unit
+(*s End the compilation of a library and save it to a ".vo" file *)
+val save_library_to : dir_path -> string -> unit
-(* [import_library true qid] = [export qid] *)
-
-val import_library : bool -> qualid located -> unit
+(*s Interrogate the status of libraries *)
+ (* - Tell if a library is loaded or opened *)
val library_is_loaded : dir_path -> bool
val library_is_opened : dir_path -> bool
+ (* - Tell which libraries are loaded or imported *)
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. *)
-
+ (* - Return the full filename of a loaded library. *)
val library_full_filename : dir_path -> string
+(*s Hook for the xml exportation of libraries *)
+val set_xml_require : (dir_path -> unit) -> unit
-(*s Global load path *)
-type logical_path = dir_path
+(*s Global load paths: a load path is a physical path in the file
+ system; to each load path is associated a Coq [dir_path] (the "logical"
+ path of the physical path) *)
-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
+val get_load_paths : unit -> System.physical_path list
+val get_full_load_paths : unit -> (System.physical_path * dir_path) list
+val add_load_path : System.physical_path * dir_path -> unit
+val remove_load_path : System.physical_path -> unit
+val find_logical_path : System.physical_path -> dir_path
+val load_paths_of_dir_path : dir_path -> System.physical_path list
+(*s Locate a library in the load paths *)
exception LibUnmappedDir
exception LibNotFound
type library_location = LibLoaded | LibInPath
@@ -81,14 +74,5 @@ 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. *)
+(*s Statistics: display 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
index 35b707a7..6db5f75d 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: nameops.ml,v 1.21.2.2 2004/10/12 10:12:31 herbelin Exp $ *)
+(* $Id: nameops.ml 6205 2004-10-12 10:13:15Z herbelin $ *)
open Pp
open Util
@@ -16,6 +16,10 @@ open Names
let pr_id id = str (string_of_id id)
+let pr_name = function
+ | Anonymous -> str "_"
+ | Name id -> pr_id id
+
let wildcard = id_of_string "_"
(* Utilities *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 71dbf040..9d1722d4 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,12 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: nameops.mli,v 1.12.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: nameops.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
open Names
(* Identifiers and names *)
val pr_id : identifier -> Pp.std_ppcmds
+val pr_name : name -> Pp.std_ppcmds
+
val wildcard : identifier
val make_ident : string -> int option -> identifier
diff --git a/library/nametab.ml b/library/nametab.ml
index 4bd0cb3f..96280e8b 100755..100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: nametab.ml,v 1.48.2.2 2005/11/21 09:16:27 herbelin Exp $ *)
+(* $Id: nametab.ml 8642 2006-03-17 10:09:02Z notin $ *)
open Util
open Pp
@@ -96,7 +96,7 @@ struct
[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 ->
+ | modid :: path ->
let mc =
try ModIdmap.find modid dirmap
with Not_found -> (Nothing, ModIdmap.empty)
@@ -135,7 +135,7 @@ struct
let rec push_exactly uname o level (current,dirmap) = function
- | modid :: path as dir ->
+ | modid :: path ->
let mc =
try ModIdmap.find modid dirmap
with Not_found -> (Nothing, ModIdmap.empty)
diff --git a/library/nametab.mli b/library/nametab.mli
index 4cea1d40..a05b7415 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: nametab.mli,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*)
+(*i $Id: nametab.mli 7596 2005-11-21 09:17:07Z herbelin $ i*)
(*i*)
open Util
diff --git a/library/states.ml b/library/states.ml
index 7a7f1e06..3bb37a4d 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: states.ml,v 1.8.14.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: states.ml 6692 2005-02-06 13:03:51Z herbelin $ *)
open System
@@ -24,7 +24,7 @@ let state_magic_number = 19764
let (extern_state,intern_state) =
let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
(fun s -> raw_extern s (get_state())),
- (fun s -> set_state (raw_intern (Library.get_load_path ()) s))
+ (fun s -> set_state (raw_intern (Library.get_load_paths ()) s))
(* Rollback. *)
diff --git a/library/states.mli b/library/states.mli
index 70018180..eff046ef 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: states.mli,v 1.6.16.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*s States of the system. In that module, we provide functions to get
and set the state of the whole system. Internally, it is done by
diff --git a/library/summary.ml b/library/summary.ml
index fc88350a..455ee264 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: summary.ml,v 1.7.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: summary.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
open Pp
open Util
diff --git a/library/summary.mli b/library/summary.mli
index 7e691f0b..ba527bdf 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: summary.mli,v 1.8.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: summary.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* This module registers the declaration of global tables, which will be kept
in synchronization during the various backtracks of the system. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 11:21:47 +0000