add_leaf -> application methode cache

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

5 files changed, 49 insertions, 52 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1a1d46d3f0..31749152c0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -52,11 +52,9 @@ let cache_variable (sp,(id,(ty,_,_) as vd)) =
   declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
 
-let load_variable _ = 
-  anomaly "we shouldn't load a variable"
+let load_variable _ = anomaly "we shouldn't load a variable"
 
-let open_variable _ = 
-  anomaly "we shouldn't open 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"
@@ -70,10 +68,8 @@ let (in_variable, out_variable) =
   declare_object ("VARIABLE", od)
 
 let declare_variable id ((ty,_,_) as obj) =
-  Global.push_var (id,ty);
-  let sp = add_leaf id CCI (in_variable (id,obj)) in
-  Nametab.push id sp;
-  declare_var_implicits id
+  let _ = add_leaf id CCI (in_variable (id,obj)) in
+  ()
 
 (* Parameters. *)
 
@@ -93,14 +89,12 @@ let (in_parameter, out_parameter) =
     cache_function = cache_parameter;
     load_function = (fun _ -> ());
     open_function = open_parameter;
-    specification_function = specification_parameter } in
+    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;
-  declare_constant_implicits sp
+  let _ = add_leaf id CCI (in_parameter c) in ()
  
 (* Constants. *)
 
@@ -113,30 +107,33 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_constant (sp,ce) =
+let cache_constant (sp,((ce,_,_) as cd)) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  declare_constant_implicits sp;
+  csttab := Spmap.add sp cd !csttab
+
+let load_constant (sp,((ce,_,_) as cd)) =
+  declare_constant_implicits sp;
+  csttab := Spmap.add sp cd !csttab
 
 let open_constant (sp,_) =
-  Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  Nametab.push (basename sp) sp
 
 let specification_constant obj = obj
 
 let (in_constant, out_constant) =
   let od = {
     cache_function = cache_constant;
-    load_function = (fun _ -> ());
+    load_function = load_constant;
     open_function = open_constant;
-    specification_function = specification_constant } in
+    specification_function = specification_constant } 
+  in
   declare_object ("CONSTANT", od)
 
-let declare_constant id ((ce,_,_) as cd) =
-  let sp = add_leaf id CCI (in_constant ce) in
-  Global.add_constant sp ce;
-  Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+let declare_constant id cd =
+  let _ = add_leaf id CCI (in_constant cd) in ()
+
  
 (* Inductives. *)
 
@@ -152,10 +149,12 @@ let cache_inductive (sp,mie) =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
-let open_inductive (sp,mie) =
-  push_inductive_names sp mie;
+let load_inductive (sp,_) =
   declare_inductive_implicits sp
 
+let open_inductive (sp,mie) =
+  push_inductive_names sp mie
+
 let specification_inductive obj = obj
 
 let (in_inductive, out_inductive) =
@@ -163,7 +162,8 @@ let (in_inductive, out_inductive) =
     cache_function = cache_inductive;
     load_function = (fun _ -> ());
     open_function = open_inductive;
-    specification_function = specification_inductive } in
+    specification_function = specification_inductive } 
+  in
   declare_object ("INDUCTIVE", od)
 
 let declare_mind mie =
@@ -171,17 +171,16 @@ let declare_mind mie =
     | (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
+  let _ = add_leaf id CCI (in_inductive mie) in ()
+
 
 (* Test and access functions. *)
 
 let is_constant sp = 
   try let _ = Global.lookup_constant sp in true with Not_found -> false
 
-let constant_strength sp = failwith "TODO"
+let constant_strength sp = 
+  let (_,stre,_) = Spmap.find sp !csttab in stre
 
 let is_variable id = 
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
@@ -291,7 +290,7 @@ let declare_eliminations sp =
   let declare na c =
     declare_constant (id_of_string na)
       ({ const_entry_body = c; const_entry_type = None },
-       false, NeverDischarge)
+       NeverDischarge,false)
   in
   let mispec = Global.lookup_mind_specif redmind in 
   let elim_scheme = 
diff --git a/library/global.ml b/library/global.ml
index 5cefe53f6d..af9dbe1d5b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -48,7 +48,7 @@ let import cenv = global_env := import cenv !global_env
 
 (* Some instanciations of functions from [Environ]. *)
 
-let id_of_global = Environ.id_of_global (env_of_safe_env !global_env)
+let id_of_global id = Environ.id_of_global (env_of_safe_env !global_env) id
 
 (* Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index a54d0870c8..a8b553f328 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -81,8 +81,8 @@ module MakeTable =
 		Libobject.open_function = open_options;
 		Libobject.cache_function = cache_options;
 		Libobject.specification_function = specification_options}) in
-        ((fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOadd, c)) in ()),
-         (fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOrmv, c)) in ()))
+        ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
+         (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
       else
         ((fun c -> t := MySet.add c !t),
          (fun c -> t := MySet.remove c !t))
@@ -244,8 +244,8 @@ let set_option_value check_and_cast key v =
   in
   match info with
     | Sync  current  ->
-      	let _ = Lib.add_anonymous_leaf
-		  (inOptVal (key,(name,check_and_cast v current))) in ()
+      	Lib.add_anonymous_leaf
+	  (inOptVal (key,(name,check_and_cast v current)))
     | Async (read,write) -> write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option"
diff --git a/library/lib.ml b/library/lib.ml
index 075e0e12af..b9964a87f9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,8 +26,6 @@ type library_entry = section_path * node
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-let lib_tab = Hashtbl.create 353
-
 let module_name = ref None
 let path_prefix = ref ([] : string list)
 
@@ -71,8 +69,7 @@ let split_lib sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk;
-  Hashtbl.add lib_tab sp node
+  lib_stk := (sp,node) :: !lib_stk
 
 let anonymous_id = 
   let n = ref 0 in
@@ -86,10 +83,12 @@ let add_anonymous_entry node =
 let add_leaf id kind obj =
   let sp = make_path id kind in
   add_entry sp (Leaf obj);
+  cache_object (sp,obj);
   sp
 
 let add_anonymous_leaf obj =
-  add_anonymous_entry (Leaf obj)
+  let sp = add_anonymous_entry (Leaf obj) in
+  cache_object (sp,obj)
 
 let add_frozen_state () =
   let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
@@ -98,11 +97,6 @@ let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
-let map_leaf sp = 
-  match Hashtbl.find lib_tab sp with
-    | Leaf obj -> obj
-    | _ -> anomaly "Lib.map_leaf: not a leaf"
-
 (* Sections. *)
 
 let open_section s =
@@ -178,6 +172,10 @@ let reset_to sp =
   let (after,_,_) = split_lib spf in
   recache_context (List.rev after)
 
+let reset_name id =
+  let (sp,_) = find_entry_p (fun (sp,_) -> id = basename sp) in
+  reset_to sp
+
 let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
 
 (* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index 826cc12e76..56bbcd59cf 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -22,15 +22,14 @@ and library_segment = (section_path * node) list
 type library_entry = section_path * node
 
 
-(*s Adding operations, and getting the current list of operations (most 
-  recent ones coming first). *)
+(*s Adding operations (which calls the [cache] method, and getting the
+  current list of operations (most recent ones coming first). *)
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
-val add_anonymous_leaf : obj -> section_path
+val add_anonymous_leaf : obj -> unit
 
 val contents_after : section_path option -> library_segment
 
-val map_leaf : section_path -> obj
 
 (*s Opening and closing a section. *)
 
@@ -48,6 +47,7 @@ val export_module : unit -> library_segment
 (*s Backtracking (undo). *)
 
 val reset_to : section_path -> unit
+val reset_name : identifier -> unit
 
 
 (*s We can get and set the state of the operations (used in [States]). *)