modules System, Lib et States

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

6 files changed, 258 insertions, 4 deletions

diff --git a/library/lib.ml b/library/lib.ml
new file mode 100644
index 000000000..a8ab156c5
--- /dev/null
+++ b/library/lib.ml
@@ -0,0 +1,167 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Libobject
+open Summary
+
+type node = 
+  | Leaf of obj
+  | OpenedSection of string * module_p
+  | ClosedSection of string * module_p * library_segment
+  | FrozenState of Summary.frozen
+
+and library_segment = (section_path * node) list
+
+and module_p = bool
+
+type library_entry = section_path * node
+
+
+(* We keep trace of operations in a stack [lib_stk]. 
+   [path_prefix] is the current path of sections (in correct order). *)
+
+let lib_stk = ref ([] : (section_path * node) list)
+
+let path_prefix = ref ([] : string list)
+
+let recalc_path_prefix () =
+  let rec recalc = function
+    | (sp, OpenedSection _) :: _ ->
+	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
+    | _::l -> recalc l
+    | [] -> []
+  in
+  path_prefix := recalc !lib_stk
+
+let pop_path_prefix () =
+  let rec pop acc = function
+    | [] -> assert false
+    | [_] -> path_prefix := acc
+    | s::l -> pop (s::acc) l
+  in
+  pop [] !path_prefix
+
+let make_path id k = Names.make_path !path_prefix id k
+
+let cwd () = !path_prefix
+
+let find_entry_p p = 
+  let rec find = function
+    | [] -> raise Not_found
+    | ent::l -> if p ent then ent else find l
+  in
+  find !lib_stk
+
+let split_lib sp = 
+  let rec findrec acc = function
+    | ((sp',obj) as hd)::t ->
+      	if sp = sp' then (acc,hd,t) else findrec (hd::acc) t
+    | [] -> error "no such entry"
+  in 
+  findrec [] !lib_stk
+
+
+(* Adding operations. *)
+
+let add_entry sp node =
+  lib_stk := (sp,node) :: !lib_stk
+
+let anonymous_id = 
+  let n = ref 0 in
+  fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+
+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
+  add_entry sp (Leaf obj);
+  sp
+
+let add_anonymous_leaf obj =
+  add_anonymous_entry (Leaf obj)
+
+let add_frozen_state () =
+  add_anonymous_entry (FrozenState (freeze_summaries()))
+
+let contents_after = function
+  | None -> !lib_stk
+  | Some sp -> let (after,_,_) = split_lib sp in after
+
+
+(* Sections. *)
+
+let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
+
+let check_single_module () =
+  try
+    let _ = find_entry_p is_opened_section in
+    error "a module or a section is already opened"
+  with Not_found -> ()
+
+let open_section s modp =
+  if modp then check_single_module ();
+  let sp = make_path (id_of_string s) OBJ in
+  add_entry sp (OpenedSection (s,modp));
+  path_prefix := !path_prefix @ [s];
+  sp
+
+let close_section s =
+  let (sp,modp) = 
+    try
+      match find_entry_p is_opened_section with
+	| sp,OpenedSection (s',modp) -> 
+	    if s <> s' then error "this is not the last opened section"; 
+	    (sp,modp)
+	| _ -> assert false
+    with Not_found ->
+      error "no opened section"
+  in
+  let (after,_,before) = split_lib sp in
+  lib_stk := before;
+  add_entry sp (ClosedSection (s,modp,after));
+  add_frozen_state ();
+  pop_path_prefix ()
+
+
+(* Backtracking. *)
+
+let recache_decl = function
+  | (sp, Leaf o) -> cache_object (sp,o)
+  | _ -> ()
+
+let recache_context ctx =
+  List.iter recache_decl ctx
+
+let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
+
+let reset_to sp =
+  let (_,_,before) = split_lib sp in
+  lib_stk := before;
+  recalc_path_prefix ();
+  let (spf,frozen) = match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) -> sp,f
+    | _ -> assert false
+  in
+  unfreeze_summaries frozen;
+  let (after,_,_) = split_lib spf in
+  recache_context (List.rev after)
+
+
+(* State and initialization. *)
+
+type frozen = library_segment
+
+let freeze () = !lib_stk
+
+let unfreeze stk =
+  lib_stk := stk;
+  recalc_path_prefix ()
+
+let init () =
+  lib_stk := [];
+  add_frozen_state ();
+  path_prefix := []
diff --git a/library/lib.mli b/library/lib.mli
new file mode 100644
index 000000000..80f61ef40
--- /dev/null
+++ b/library/lib.mli
@@ -0,0 +1,57 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Libobject
+open Summary
+(*i*)
+
+(* This module provides a general mechanism to keep a trace of all operations
+   and to backtrack (undo) those operations. It provides also the section
+   mechanism (at a low level; discharge is not known at this step). *)
+
+type node = 
+  | Leaf of obj
+  | OpenedSection of string * module_p
+  | ClosedSection of string * module_p * library_segment
+  | FrozenState of Summary.frozen
+
+and library_segment = (section_path * node) list
+
+and module_p = bool
+
+type library_entry = section_path * node
+
+
+(*s Adding operations, and getting the current list of operations (most 
+  recent ones come first). *)
+
+val add_leaf : identifier -> obj -> section_path
+val add_anonymous_leaf : obj -> unit
+
+val contents_after : section_path option -> library_segment
+
+
+(*s Opening and closing a section. *)
+
+val open_section : string -> bool -> section_path
+val close_section : string -> unit
+
+val make_path : identifier -> path_kind -> section_path
+val cwd : unit -> string list
+
+
+(*s Backtracking (undo). *)
+
+val reset_to : section_path -> unit
+
+
+(*s We can get and set the state of the operations (used in [States]). *)
+
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+
+val init : unit -> unit
diff --git a/library/states.ml b/library/states.ml
new file mode 100644
index 000000000..2e198e36f
--- /dev/null
+++ b/library/states.ml
@@ -0,0 +1,22 @@
+
+(* $Id$ *)
+
+open System
+open Lib
+open Summary
+
+type state = Lib.frozen * Summary.frozen
+
+let get_state () =
+  (Lib.freeze(), freeze_summaries())
+
+let set_state (fl,fs) =
+  Lib.unfreeze fl;
+  unfreeze_summaries fs
+
+let state_magic_number = 19764
+
+let (extern_state,intern_state) =
+  let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
+  (fun s -> raw_extern s (get_state())),
+  (fun s -> set_state (raw_intern s))
diff --git a/library/states.mli b/library/states.mli
new file mode 100644
index 000000000..06a877802
--- /dev/null
+++ b/library/states.mli
@@ -0,0 +1,8 @@
+
+(* $Id$ *)
+
+type state
+
+val intern_state : string -> unit
+val extern_state : string -> unit
+
diff --git a/library/summary.ml b/library/summary.ml
index f58917202..0ba07a737 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -28,7 +28,7 @@ let declare_summary sumname sdecl =
       [< 'sTR "Cannot declare a summary twice: " ; 'sTR sumname >];
   Hashtbl.add summaries sumname ddecl
 
-type frozen_summaries = Dyn.t Stringmap.t
+type frozen = Dyn.t Stringmap.t
 
 let freeze_summaries () =
   let m = ref Stringmap.empty in
diff --git a/library/summary.mli b/library/summary.mli
index faa887f37..0d329a947 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -15,10 +15,10 @@ type 'a summary_declaration = {
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
-type frozen_summaries
+type frozen
 
-val freeze_summaries : unit -> frozen_summaries
-val unfreeze_summaries : frozen_summaries -> unit
+val freeze_summaries : unit -> frozen
+val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit