modules Libobject et Summary (partiel)

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

5 files changed, 184 insertions, 0 deletions

diff --git a/library/doc.tex b/library/doc.tex
new file mode 100644
index 000000000..fd1a8bbf9
--- /dev/null
+++ b/library/doc.tex
@@ -0,0 +1,11 @@
+
+\section*{The Coq library}
+
+\ocwsection \label{library}
+This section describes the \Coq\ library, which is made of two parts:
+\begin{itemize}
+  \item a general mechanism to keep a trace of all operations and of
+    the state of the system, with backtrack possibilities;
+  \item a global environment for the CCI, with functions to export and 
+    import compiled modules.
+\end{itemize}
diff --git a/library/libobject.ml b/library/libobject.ml
new file mode 100644
index 000000000..f5e610704
--- /dev/null
+++ b/library/libobject.ml
@@ -0,0 +1,63 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+
+type 'a object_declaration = {
+  load_function : 'a -> unit;
+  cache_function : section_path * 'a -> unit;
+  specification_function : 'a -> 'a }
+
+type obj = Dyn.t (* persistent dynamic objects *)
+
+type dynamic_object_declaration = {
+  dyn_load_function : obj -> unit;
+  dyn_cache_function : section_path * obj -> unit;
+  dyn_specification_function : obj -> obj }
+
+let object_tag lobj = Dyn.tag lobj
+
+let cache_tab = 
+  (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
+
+let declare_object (na,odecl) =
+  let (infun,outfun) = Dyn.create na in
+  let loader lobj =
+    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+  and 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 spec_extractor lobj = 
+    infun(odecl.specification_function (outfun lobj))
+  in 
+  Hashtbl.add cache_tab na { dyn_load_function = loader;
+                             dyn_cache_function = cacher;
+                             dyn_specification_function = spec_extractor };
+  (infun,outfun)
+
+
+let load_object lobj =
+  let tag = object_tag lobj in
+  try 
+    let dodecl = Hashtbl.find cache_tab tag in 
+    dodecl.dyn_load_function lobj
+  with Not_found ->
+    anomaly ("Cannot find loadfun for an object with tag "^tag)
+
+let cache_object (spopt,lobj) =
+  let tag = object_tag lobj in
+  try 
+    let dodecl = Hashtbl.find cache_tab tag in 
+    dodecl.dyn_cache_function(spopt,lobj)
+  with Not_found ->
+    anomaly ("Cannot find cachefun for an object with tag "^tag)
+
+let extract_object_specification lobj =
+  let tag = object_tag lobj in
+  try 
+    let dodecl = Hashtbl.find cache_tab tag in
+    dodecl.dyn_specification_function lobj
+  with Not_found ->
+    anomaly ("Cannot find specification extractor for an object with tag "^tag)
diff --git a/library/libobject.mli b/library/libobject.mli
new file mode 100644
index 000000000..967e4c410
--- /dev/null
+++ b/library/libobject.mli
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* [Libobject] declares persistent objects given with three methods:
+   - a loading function, specifying what to do when the object is loaded
+     from the disk;
+   - a caching function specifying how to import the object in the current
+     scope of theory modules;
+   - a specification function, to extract its specification when writing
+     the specification of a module to the disk (.vi) *)
+
+type 'a object_declaration = {
+  load_function : 'a -> unit;
+  cache_function : section_path * 'a -> unit;
+  specification_function : 'a -> 'a }
+
+(*s given the object-name, the "loading" function, the "caching" function, 
+   and the "specification" function, the function [declare_object]
+   will hand back two functions, the "injection" and "projection"
+   functions for dynamically typed library-objects. *)
+
+type obj
+
+val declare_object : 
+  (string * 'a object_declaration) -> ('a -> obj) * (obj -> 'a)
+
+val object_tag : obj -> string
+
+val load_object : obj -> unit
+
+val cache_object : (section_path * obj) -> unit
+
+val extract_object_specification : obj -> obj
diff --git a/library/summary.ml b/library/summary.ml
new file mode 100644
index 000000000..f58917202
--- /dev/null
+++ b/library/summary.ml
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+
+type 'a summary_declaration = {
+  freeze_function : unit -> 'a;
+  unfreeze_function : 'a -> unit;
+  init_function : unit -> unit }
+
+let summaries = 
+  (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
+
+let declare_summary sumname sdecl =
+  let (infun,outfun) = Dyn.create (sumname^"-SUMMARY") in
+  let dyn_freeze () = infun (sdecl.freeze_function())
+  and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
+  and dyn_init = sdecl.init_function in
+  let ddecl = {
+    freeze_function = dyn_freeze;
+    unfreeze_function = dyn_unfreeze;
+    init_function = dyn_init} 
+  in
+  if Hashtbl.mem summaries sumname then
+    anomalylabstrm "Summary.declare_summary"
+      [< 'sTR "Cannot declare a summary twice: " ; 'sTR sumname >];
+  Hashtbl.add summaries sumname ddecl
+
+type frozen_summaries = Dyn.t Stringmap.t
+
+let freeze_summaries () =
+  let m = ref Stringmap.empty in
+  Hashtbl.iter 
+    (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m)
+    summaries;
+  !m
+
+let unfreeze_summaries fs =
+  Hashtbl.iter
+    (fun id decl -> 
+       try decl.unfreeze_function (Stringmap.find id fs)
+       with Not_found -> decl.init_function())
+    summaries
+
+let init_summaries () =
+  Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
new file mode 100644
index 000000000..faa887f37
--- /dev/null
+++ b/library/summary.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* This module registers the declaration of global tables, which will be kept
+   in synchronization during the various backtracks of the system. *)
+
+type 'a summary_declaration = {
+  freeze_function : unit -> 'a;
+  unfreeze_function : 'a -> unit;
+  init_function : unit -> unit }
+
+val declare_summary : string -> 'a summary_declaration -> unit
+
+type frozen_summaries
+
+val freeze_summaries : unit -> frozen_summaries
+val unfreeze_summaries : frozen_summaries -> unit
+val init_summaries : unit -> unit
+
+
+