module Declare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 179 insertions, 21 deletions

diff --git a/library/declare.ml b/library/declare.ml
new file mode 100644
index 000000000..1af5ad6a8
--- /dev/null
+++ b/library/declare.ml
@@ -0,0 +1,133 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Inductive
+open Libobject
+open Lib
+open Impargs
+
+(* Variables. *)
+
+let cache_variable (_,obj) = 
+  Global.push_var obj
+
+let load_variable _ = 
+  anomaly "we shouldn't load a variable"
+
+let open_variable _ = 
+  anomaly "we shouldn't open a variable"
+
+let specification_variable _ = 
+  anomaly "we shouldn't extract the specification of a variable"
+
+let (in_variable, out_variable) =
+  let od = {
+    cache_function = cache_variable;
+    load_function = load_variable;
+    open_function = open_variable;
+    specification_function = specification_variable } in
+  declare_object ("Variable", od)
+
+let declare_variable id c =
+  let obj = (id,c) in
+  Global.push_var obj;
+  let _ = add_leaf id CCI (in_variable obj) in
+  ()
+
+(* Parameters. *)
+
+let cache_parameter (sp,c) =
+  Global.add_parameter sp c;
+  Nametab.push (basename sp) sp
+
+let load_parameter _ = ()
+  
+let open_parameter (sp,_) =
+  Nametab.push (basename sp) sp
+
+let specification_parameter obj = obj
+
+let (in_parameter, out_parameter) =
+  let od = {
+    cache_function = cache_parameter;
+    load_function = load_parameter;
+    open_function = open_parameter;
+    specification_function = specification_parameter } in
+  declare_object ("Parameter", od)
+
+let declare_parameter id c =
+  let sp = add_leaf id CCI (in_parameter c) in
+  Global.add_parameter sp c;
+  Nametab.push (basename sp) sp
+ 
+(* Constants. *)
+
+let cache_constant (sp,ce) =
+  Global.add_constant sp ce;
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
+
+let load_constant _ = ()
+  
+let open_constant (sp,_) =
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
+
+let specification_constant obj = obj
+
+let (in_constant, out_constant) =
+  let od = {
+    cache_function = cache_constant;
+    load_function = load_constant;
+    open_function = open_constant;
+    specification_function = specification_constant } in
+  declare_object ("Parameter", od)
+
+let declare_constant id ce =
+  let sp = add_leaf id CCI (in_constant ce) in
+  Global.add_constant sp ce;
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
+ 
+(* Inductives. *)
+
+let push_inductive_names sp mie =
+  List.iter
+    (fun (id,_,cnames,_) ->
+       Nametab.push id sp;
+       List.iter (fun x -> Nametab.push x sp) cnames)
+    mie.mind_entry_inds
+
+let cache_inductive (sp,mie) =
+  Global.add_mind sp mie;
+  push_inductive_names sp mie;
+  declare_inductive_implicits sp
+
+let load_inductive _ = ()
+  
+let open_inductive (sp,mie) =
+  push_inductive_names sp mie;
+  declare_inductive_implicits sp
+
+let specification_inductive obj = obj
+
+let (in_inductive, out_inductive) =
+  let od = {
+    cache_function = cache_inductive;
+    load_function = load_inductive;
+    open_function = open_inductive;
+    specification_function = specification_inductive } in
+  declare_object ("Parameter", od)
+
+let declare_mind mie =
+  let id = match mie.mind_entry_inds with
+    | (id,_,_,_)::_ -> id
+    | [] -> anomaly "cannot declare an empty list of inductives"
+  in
+  let sp = add_leaf id CCI (in_inductive mie) in
+  Global.add_mind sp mie;
+  push_inductive_names sp mie;
+  declare_inductive_implicits sp
+
diff --git a/library/declare.mli b/library/declare.mli
new file mode 100644
index 000000000..21486c250
--- /dev/null
+++ b/library/declare.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Constant
+open Inductive
+(*i*)
+
+(* This module provides the official functions to declare new variables, 
+   parameters, constants and inductive types. Using the following functions
+   will add the entries in the global environment (module [Global]), will
+   register the declarations in the library (module [Lib]) --- so that the
+   reset works properly --- and will fill some global tables as [Nametab] and
+   [Impargs]. *)
+
+val declare_variable : identifier -> constr -> unit
+
+val declare_parameter : identifier -> constr -> unit
+
+val declare_constant : identifier -> constant_entry -> unit
+
+val declare_mind : mutual_inductive_entry -> unit
+
diff --git a/library/lib.ml b/library/lib.ml
index 9c434fdf1..254134710 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -80,8 +80,8 @@ let add_anonymous_entry node =
   let sp = make_path (anonymous_id()) OBJ in
   add_entry sp node
 
-let add_leaf id obj =
-  let sp = make_path id OBJ in
+let add_leaf id kind obj =
+  let sp = make_path id kind in
   add_entry sp (Leaf obj);
   sp
 
diff --git a/library/lib.mli b/library/lib.mli
index a38fb4cef..92c2937b4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -27,7 +27,7 @@ type library_entry = section_path * node
 (*s Adding operations, and getting the current list of operations (most 
   recent ones coming first). *)
 
-val add_leaf : identifier -> obj -> section_path
+val add_leaf : identifier -> path_kind -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
 
 val contents_after : section_path option -> library_segment
diff --git a/library/libobject.ml b/library/libobject.ml
index 1096ac43a..31fb81c57 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,16 +6,16 @@ open Names
 
 type 'a object_declaration = {
   cache_function : section_path * 'a -> unit;
-  load_function : 'a -> unit;
-  open_function : 'a -> unit;
+  load_function : section_path * 'a -> unit;
+  open_function : section_path * 'a -> unit;
   specification_function : 'a -> 'a }
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
 type dynamic_object_declaration = {
   dyn_cache_function : section_path * obj -> unit;
-  dyn_load_function : obj -> unit;
-  dyn_open_function : obj -> unit;
+  dyn_load_function : section_path * obj -> unit;
+  dyn_open_function : section_path * obj -> unit;
   dyn_specification_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
@@ -28,11 +28,11 @@ let declare_object (na,odecl) =
   let cacher (spopt,lobj) =
     if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the cachefun"
-  and loader lobj =
-    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
+  and loader (spopt,lobj) =
+    if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the loadfun"
-  and opener lobj =
-    if Dyn.tag lobj = na then odecl.open_function (outfun lobj)
+  and opener (spopt,lobj) =
+    if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the openfun"
   and spec_extractor lobj = 
     infun(odecl.specification_function (outfun lobj))
@@ -53,11 +53,11 @@ let apply_dyn_fun f lobj =
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
 
-let load_object lobj = 
-  apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj
+let load_object ((_,lobj) as node) = 
+  apply_dyn_fun (fun d -> d.dyn_load_function node) lobj
 
-let open_object lobj = 
-  apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj
+let open_object ((_,lobj) as node) = 
+  apply_dyn_fun (fun d -> d.dyn_open_function node) lobj
 
 let extract_object_specification lobj =
   apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index ff076ee39..d855059fa 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -17,8 +17,8 @@ open Names
 
 type 'a object_declaration = {
   cache_function : section_path * 'a -> unit;
-  load_function : 'a -> unit;
-  open_function : 'a -> unit;
+  load_function : section_path * 'a -> unit;
+  open_function : section_path * 'a -> unit;
   specification_function : 'a -> 'a }
 
 (*s Given an object name and a declaration, the function [declare_object]
@@ -32,7 +32,7 @@ val declare_object :
 
 val object_tag : obj -> string
 
-val cache_object : (section_path * obj) -> unit
-val load_object : obj -> unit
-val open_object : obj -> unit
+val cache_object : section_path * obj -> unit
+val load_object : section_path * obj -> unit
+val open_object : section_path * obj -> unit
 val extract_object_specification : obj -> obj
diff --git a/library/library.ml b/library/library.ml
index 0bd0b895c..b48d7cfee 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -50,7 +50,7 @@ let (raw_extern_module, raw_intern_module) =
 
 let segment_iter f =
   let rec apply = function
-    | _,Leaf obj -> f obj
+    | sp,Leaf obj -> f (sp,obj)
     | _,ClosedSection (_,_,mseg) -> iter mseg
     | _,OpenedSection _ -> assert false
     | _,FrozenState _ -> ()