State Transaction Machine

The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).

The observe id function runs the transactions necessary to reach to the
state id.  Transaction being on a merged branch are not executed but
stored into a future.

The finish function calls observe on the tip of the current branch.

Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.

This is the work described in the Coq Workshop 2012 paper.

Coq is compile with thread support from now on.

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

8 files changed, 23 insertions, 134 deletions

diff --git a/library/global.ml b/library/global.ml
index 28b691769..5425e5930 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -14,7 +14,17 @@ open Safe_typing
 (* We introduce here the global environment of the system, and we declare it
    as a synchronized table. *)
 
-let global_env = Summary.ref empty_environment ~name:"Global environment"
+let global_env = ref empty_environment
+
+let join_safe_environment () =
+  global_env := Safe_typing.join_safe_environment !global_env
+
+let () =
+  Summary.declare_summary "Global environment"
+    { Summary.freeze_function = (fun b ->
+        if b then join_safe_environment (); !global_env);
+      unfreeze_function = (fun fr -> global_env := fr);
+      init_function = (fun () -> global_env := empty_environment) }
 
 let safe_env () = !global_env
 
diff --git a/library/global.mli b/library/global.mli
index 3238294f2..a5ca92013 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -102,6 +102,8 @@ val import : compiled_library -> Digest.t ->
 val type_of_global : Globnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
+val join_safe_environment : unit -> unit
+
 (** spiwack: register/unregister function for retroknowledge *)
 val register : Retroknowledge.field -> constr -> constr -> unit
 
diff --git a/library/lib.ml b/library/lib.ml
index 47341e675..b4371812b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -523,85 +523,8 @@ let close_section () =
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
-(*****************)
-(* Backtracking. *)
-
-let (inLabel : int -> obj), (outLabel : obj -> int) =
-  declare_object_full {(default_object "DOT") with
-				classify_function = (fun _ -> Dispose)}
-
-let recache_decl = function
-  | (sp, Leaf o) -> cache_object (sp,o)
-  | (_,OpenedSection _) -> add_section ()
-  | _ -> ()
-
-let recache_context ctx =
-  List.iter recache_decl ctx
-
-let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
-
-let set_lib_stk new_lib_stk =
-  lib_stk := new_lib_stk;
-  recalc_path_prefix ();
-  (* Always at least one frozen state in the libstack *)
-  match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) ->
-      Summary.unfreeze_summaries f;
-      let (after,_,_) = split_lib sp in
-      recache_context after
-    | _ -> assert false
-
-let reset_to test =
-  let (_,_,before) = split_lib_gen test in
-  set_lib_stk before
-
-let first_command_label = 1
-
-let mark_end_of_command, current_command_label, reset_command_label =
-  let n = ref (first_command_label-1) in
-  (fun () ->
-    match !lib_stk with
-        (_,Leaf o)::_ when String.equal (object_tag o) "DOT" -> ()
-      | _ -> incr n;add_anonymous_leaf (inLabel !n)),
-  (fun () -> !n),
-  (fun x -> n:=x;add_anonymous_leaf (inLabel x))
-
-let is_label_n n x =
-  match x with
-    | (sp, Leaf o) when String.equal (object_tag o) "DOT" &&
-      Int.equal n (outLabel o) -> true
-    | _ -> false
-
-(** Reset the label registered by [mark_end_of_command()] with number n,
-    which should be strictly in the past. *)
-
-let reset_label n =
-  if n >= current_command_label () then
-    error "Cannot backtrack to the current label or a future one";
-  reset_to (is_label_n n);
-  (* forget state numbers after n only if reset succeeded *)
-  reset_command_label n
-
-let raw_reset_initial () = reset_label first_command_label
-
-(** Search the last label registered before defining [id] *)
-
-let label_before_name (loc,id) =
-  let found = ref false in
-  let search = function
-    | (_, Leaf o) when !found && String.equal (object_tag o) "DOT" -> true
-    | ((fp, _),_) ->
-      let (_, name) = repr_path fp in
-      let () = if Names.Id.equal id name then found := true in
-      false
-  in
-  match find_entry_p search with
-    | (_,Leaf o) -> outLabel o
-    | _ -> raise Not_found
-
 (* State and initialization. *)
 
 type frozen = Names.DirPath.t option * library_segment
@@ -616,8 +539,7 @@ let unfreeze (mn,stk) =
 let init () =
   unfreeze (None,[]);
   Summary.init_summaries ();
-  add_frozen_state (); (* Stores e.g. the keywords declared in g_*.ml4 *)
-  mark_end_of_command () (* For allowing Reset Initial in coqtop -l *)
+  add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
 
 (* Misc *)
 
diff --git a/library/lib.mli b/library/lib.mli
index a956ff5d0..04f8d0775 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,31 +147,6 @@ val remove_section_part : Globnames.global_reference -> Names.DirPath.t
 val open_section : Names.Id.t -> unit
 val close_section : unit -> unit
 
-(** {6 Backtracking } *)
-
-(** NB: The next commands are low-level ones, do not use them directly
-    otherwise the command history stack in [Backtrack] will be out-of-sync.
-    Also note that [reset_initial] is now [reset_label first_command_label] *)
-
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
-   [mark_end_of_command()]. It forgets anything registered after
-   this label. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
-(** [raw_reset_initial] is now [reset_label] to the first label.
-    This is meant to be used during initial Load's and compilations.
-    Otherwise, consider instead [Backtrack.reset_initial] *)
-val raw_reset_initial : unit -> unit
-
-(** search the label registered immediately before adding some definition *)
-val label_before_name : Names.Id.t Loc.located -> int
-
 (** {6 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 472b1fb1d..0766a62d7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -44,17 +44,20 @@ module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
+let join x = Safe_typing.join_compiled_library x.library_compiled
 (* This is a map from names to loaded libraries *)
-let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
+let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l
+let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
 let libraries_filename_table = ref LibraryFilenameMap.empty
 
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
-let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
-let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
-let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
+let freeze b l = if b then (List.iter join l; l) else l
+let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze
+let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze
+let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze
 
 (* various requests to the tables *)
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 9f2bede75..fd27ef264 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -522,8 +522,8 @@ let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
   paresseusement : il faut forcer l'évaluation pour capturer
   l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
-  let s = string_of_qualid (shortest_qualid_of_global env ref) in
-  (str s)
+  try str (string_of_qualid (shortest_qualid_of_global env ref))
+  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
 
 let global_inductive r =
   match global r with
diff --git a/library/states.ml b/library/states.ml
index 1fd3fa2e5..93b2c120e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -32,17 +32,6 @@ let (extern_state,intern_state) =
 
 (* Rollback. *)
 
-let with_heavy_rollback f h x =
-  let st = freeze ~marshallable:false in
-  try
-    f x
-  with reraise ->
-    let e = h reraise in (unfreeze st; raise e)
-
-let without_rollback f h x =
-  try f x
-  with reraise -> raise (h reraise)
-
 let with_state_protection f x =
   let st = freeze ~marshallable:false in
   try
diff --git a/library/states.mli b/library/states.mli
index d186bf1c8..da6f33d65 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -22,18 +22,6 @@ val unfreeze : state -> unit
 
 (** {6 Rollback } *)
 
-(** [with_heavy_rollback f h x] applies [f] to [x]. If this application
-    ends on an exception, the wrapper [h] is applied to it, then
-    the state of the whole system is restored as it was before applying [f],
-    and finally the exception produced by [h] is raised. *)
-
-val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
-
-(** [without_rollback] is just like [with_heavy_rollback], except that
-    no state is restored in case of exception. *)
-
-val without_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
-
 (** [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before applying [f] *)