1 files changed, 167 insertions, 0 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 := []