juste l'interface de Discharge

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

7 files changed, 78 insertions, 39 deletions

diff --git a/library/discharge.mli b/library/discharge.mli
new file mode 100644
index 000000000..7b22e2ead
--- /dev/null
+++ b/library/discharge.mli
@@ -0,0 +1,4 @@
+
+(* $Id$ *)
+
+val close_section : string -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index 95b322e4e..0aa269213 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -77,7 +77,7 @@ let unfreeze ct =
   constants_table := ct
 
 let _ = 
-  Summary.declare_summary "names"
+  Summary.declare_summary "implicits"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init }
diff --git a/library/lib.ml b/library/lib.ml
index 254134710..470c85674 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,26 +8,25 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | OpenedSection of string * module_p
-  | ClosedSection of string * module_p * library_segment
+  | OpenedSection of string
+  | ClosedSection of string * 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. Sections are stored in 
+(* We keep trace of operations in the stack [lib_stk]. 
+   [path_prefix] is the current path of sections, where sections are stored in 
    ``correct'' order, the oldest coming first in the list. It may seems 
    costly, but in practice there is not so many openings and closings of
    sections, but on the contrary there are many constructions of section
-   paths. *) 
+   paths based on the library path. *) 
 
 let lib_stk = ref ([] : (section_path * node) list)
 
+let module_name = ref None
 let path_prefix = ref ([] : string list)
 
 let recalc_path_prefix () =
@@ -35,7 +34,7 @@ let recalc_path_prefix () =
     | (sp, OpenedSection _) :: _ ->
 	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
     | _::l -> recalc l
-    | [] -> []
+    | [] -> (match !module_name with Some m -> [m] | None -> [])
   in
   path_prefix := recalc !lib_stk
 
@@ -98,38 +97,55 @@ let contents_after = function
 
 (* Sections. *)
 
-let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
+let open_section s =
+  let sp = make_path (id_of_string s) OBJ in
+  add_entry sp (OpenedSection s);
+  path_prefix := !path_prefix @ [s];
+  sp
 
-let check_single_module () =
+let check_for_module () =
+  let is_decl = function (_,FrozenState _) -> false | _ -> true in
   try
-    let _ = find_entry_p is_opened_section in
-    error "a module or a section is already opened"
+    let _ = find_entry_p is_decl in
+    error "a module can not be opened after some declarations"
   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 open_module s =
+  if !module_name <> None then error "a module is already opened";
+  check_for_module ();
+  module_name := Some s
+
+let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
 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
+  let sp = 
+    try match find_entry_p is_opened_section with
+      | sp,OpenedSection s' -> 
+	  if s <> s' then error "this is not the last opened section"; sp
+      | _ -> 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_entry sp (ClosedSection (s,after));
   add_frozen_state ();
   pop_path_prefix ()
 
+(* The following function exports the whole library segment, that will be 
+   saved as a module. Objects are presented in chronological order, and
+   closed sections and frozen states are removed. *)
+
+let export_module () =
+  if !module_name = None then error "no module declared";
+  let rec export acc = function
+    | [] -> acc
+    | (_,Leaf _) as node :: stk -> export (node::acc) stk
+    | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+    | (_,(FrozenState _ | ClosedSection _)) :: stk -> export acc stk
+  in
+  export [] !lib_stk
+
 
 (* Backtracking. *)
 
@@ -169,3 +185,17 @@ let init () =
   lib_stk := [];
   add_frozen_state ();
   path_prefix := []
+
+
+(* Rollback. *)
+
+let with_heavy_rollback f x =
+  let sum = freeze_summaries ()
+  and flib = freeze() in
+  try 
+    f x
+  with reraise -> begin
+    unfreeze_summaries sum;
+    unfreeze flib;
+    raise reraise
+  end
diff --git a/library/lib.mli b/library/lib.mli
index 92c2937b4..33f6e9056 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,14 +13,12 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | OpenedSection of string * module_p
-  | ClosedSection of string * module_p * library_segment
+  | OpenedSection of string
+  | ClosedSection of string * library_segment
   | FrozenState of Summary.frozen
 
 and library_segment = (section_path * node) list
 
-and module_p = bool
-
 type library_entry = section_path * node
 
 
@@ -33,21 +31,30 @@ val add_anonymous_leaf : obj -> unit
 val contents_after : section_path option -> library_segment
 
 
-(*s Opening and closing a section. The boolean in [open_section] indicates
-  a module. *)
+(*s Opening and closing a section. *)
 
-val open_section : string -> bool -> section_path
+val open_section : string -> section_path
 val close_section : string -> unit
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
 
+val open_module : string -> unit
+val export_module : unit -> library_segment
+
 
 (*s Backtracking (undo). *)
 
 val reset_to : section_path -> unit
 
 
+(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
+  state of the whole system as it was before the evaluation if an exception 
+  is raised. *)
+
+val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+
+
 (*s We can get and set the state of the operations (used in [States]). *)
 
 type frozen
diff --git a/library/library.ml b/library/library.ml
index b48d7cfee..1f040984a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -51,7 +51,7 @@ let (raw_extern_module, raw_intern_module) =
 let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
-    | _,ClosedSection (_,_,mseg) -> iter mseg
+    | _,ClosedSection (_,mseg) -> iter mseg
     | _,OpenedSection _ -> assert false
     | _,FrozenState _ -> ()
   and iter seg =
@@ -135,7 +135,7 @@ let current_imports () =
   !l
 
 let save_module_to s f =
-  let seg = contents_after None in
+  let seg = export_module () in
   let md = { 
     md_name = s;
     md_compiled_env = Global.export s;
diff --git a/library/library.mli b/library/library.mli
index 2c54aec2e..dc34de8a0 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -26,3 +26,4 @@ val require_module : bool option -> string -> string option -> bool -> unit
   in the file [f]. *)
 
 val save_module_to : string -> string -> unit
+
diff --git a/library/nametab.mli b/library/nametab.mli
index 2d0cd62eb..463dc63de 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -12,6 +12,3 @@ val push : identifier -> section_path -> unit
 
 val sp_of_id : path_kind -> identifier -> section_path
 val fw_sp_of_id : identifier -> section_path
-
-val rollback : ('a -> 'b) -> 'a -> 'b
-