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

3 files changed, 15 insertions, 25 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f70ce00924..efed9a8560 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -339,7 +339,8 @@ let generate_functional_principle
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
 	let ce =
-	  { const_entry_body = value;
+          { const_entry_body =
+              Future.from_val (value,Declareops.no_seff);
             const_entry_secctx = None;
 	    const_entry_type = None;
 	    const_entry_opaque = false;
@@ -556,7 +557,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
     let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
-    let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+    let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
       List.map (* we can now compute the other principles *)
@@ -598,7 +599,8 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
-	      Entries.const_entry_body = princ_body;
+	      Entries.const_entry_body = 
+                (Future.from_val (princ_body,Declareops.no_seff));
 	      Entries.const_entry_type = Some scheme_type
 	   }
       )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index fd074386ec..7d14d1408c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1013,10 +1013,9 @@ let do_save () = Lemmas.save_named false
 *)
 
 let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
-  let previous_state = States.freeze ~marshallable:false in
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let funs_constr = Array.map mkConst funs  in
-  try
+  States.with_state_protection (fun () ->
     let graphs_constr = Array.map mkInd graphs in
     let lemmas_types_infos =
       Util.Array.map2_i
@@ -1044,7 +1043,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
+		  (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
 	    )
@@ -1122,16 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
-      funs;
-  with reraise ->
-    (* In case of problem, we reset all the lemmas *)
-    Pfedit.delete_all_proofs ();
-    States.unfreeze previous_state;
-    raise reraise
-
-
-
-
+      funs)
+  ()
 
 (***********************************************)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4b9704c2c9..68b291ff96 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -57,7 +57,8 @@ let find_reference sl s =
 
 let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
-    let ce = {const_entry_body = value;
+    let ce = {const_entry_body = Future.from_val
+                (value, Declareops.no_seff);
               const_entry_secctx = None;
 	      const_entry_type = None;
           const_entry_opaque = false;
@@ -1261,7 +1262,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
-    ignore (Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None));
+    ignore (Flags.silently Vernacentries.interp (Loc.ghost,Vernacexpr.VernacAbort None));
     build_proof
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
@@ -1443,7 +1444,6 @@ let (com_eqn : int -> Id.t ->
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
-  let previous_label = Lib.current_command_label () in
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
@@ -1513,7 +1513,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 			   spc () ++ str"is defined" )
       )
   in
-  try 
+  States.with_state_protection (fun () ->
     com_terminate
       tcc_lemma_name
       tcc_lemma_constr
@@ -1523,9 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      hook 
-  with reraise ->
-    ignore (Backtrack.backto previous_label);
-    (*       anomaly (Pp.str "Cannot create termination Lemma") *)
-    raise reraise
+      hook)
+    ()