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