modules Libobject et Summary (partiel)

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

11 files changed, 211 insertions, 6 deletions

diff --git a/.depend b/.depend
index 080e11881..b674b479a 100644
--- a/.depend
+++ b/.depend
@@ -24,10 +24,12 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \
 kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
-kernel/univ.cmi: kernel/names.cmi 
+kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/coqast.cmi: lib/dyn.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 lib/util.cmi: lib/pp.cmi 
+library/libobject.cmi: kernel/names.cmi 
+library/summary.cmi: kernel/names.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
@@ -134,3 +136,9 @@ lib/pp_control.cmo: lib/pp_control.cmi
 lib/pp_control.cmx: lib/pp_control.cmi 
 lib/util.cmo: lib/pp.cmi lib/util.cmi 
 lib/util.cmx: lib/pp.cmx lib/util.cmi 
+library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
+    library/libobject.cmi 
+library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
+    library/libobject.cmi 
+library/summary.cmo: kernel/names.cmi library/summary.cmi 
+library/summary.cmx: kernel/names.cmx library/summary.cmi 
diff --git a/Makefile b/Makefile
index 775cdc3c7..e062d3997 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
 DEPFLAGS=$(INCLUDES)
 
-INCLUDES=-I config -I lib -I kernel
+INCLUDES=-I config -I lib -I kernel -I library
 
 # Objects files 
 
@@ -33,18 +33,22 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
        kernel/typing.cmo
 
-OBJS=$(CONFIG) $(LIB) $(KERNEL)
+LIBRARY=library/libobject.cmo library/summary.cmo
+
+OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY)
 
 # Targets
 
 world: $(OBJS)
-	$(OCAMLC) -o coqtop.byte $(OBJS)
+	#$(OCAMLC) -o coqtop.byte $(OBJS)
+	ocamlmktop -o coqtop $(OBJS)
 
 # Literate programming (with ocamlweb)
 
 LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
-LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL)
+LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
+LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY)
 lp: doc/coq.ps
 doc/coq.ps: doc/coq.tex
 	cd doc; make coq.ps
diff --git a/kernel/doc.tex b/kernel/doc.tex
index 78f1a267d..56debc102 100644
--- a/kernel/doc.tex
+++ b/kernel/doc.tex
@@ -1,7 +1,7 @@
 
 \section*{The Coq kernel}
 
-\ocwsection 
+\ocwsection \label{kernel}
 This section describes the \Coq\ kernel, which is a type checker for the \CCI.
 
 The modules of the kernel are organized as follows.
diff --git a/kernel/univ.mli b/kernel/univ.mli
index b262ad718..2104fa721 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -17,6 +17,8 @@ val prop_univ_univ_univ : universe
 
 val new_univ : section_path -> universe
 
+(*s Graphs of universes. *)
+
 type universes
 
 val initial_universes : universes
@@ -34,3 +36,6 @@ val enforce_gt : constraint_function
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
+(* pretty-printing. *)
+
+val pr_universes : universes -> Pp.std_ppcmds
diff --git a/lib/util.ml b/lib/util.ml
index 95a609378..698341097 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -61,6 +61,8 @@ let parse_section_path s =
     let id,k = decoupe_kind n in
     dirs,id,k
 
+module Stringmap = Map.Make(struct type t = string let compare = compare end)
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
diff --git a/lib/util.mli b/lib/util.mli
index 9517d8742..2d764d499 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -23,6 +23,8 @@ val implode : string list -> string
 
 val parse_section_path : string -> string list * string * string
 
+module Stringmap : Map.S with type key = string
+
 (*s Lists. *)
 
 val list_intersect : 'a list -> 'a list -> 'a list
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
+
+
+