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

4 files changed, 39 insertions, 30 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 8c5aec38bf..0cbd263168 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -99,11 +99,13 @@ let proof_cond = Proof.no_cond proof_focus
 
 let focus p =
   let inf = get_stack p in
-  Proof.focus proof_cond inf 1 p
+  Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
-let unfocus = Proof.unfocus proof_focus
+let unfocus () =
+  Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus = Proof_global.maximal_unfocus proof_focus
+let maximal_unfocus () = 
+  Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
 
 let get_top_stack pts =
   try
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index c54dcdc281..8e691f508f 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -75,6 +75,6 @@ val get_last:  Environ.env -> Id.t
 
 val focus : Proof.proof -> unit
 
-val unfocus : Proof.proof -> unit
+val unfocus : unit -> unit
 
-val maximal_unfocus : Proof.proof -> unit
+val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a06b44083d..e3ef0671c0 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -51,12 +51,13 @@ let _ =
 
 let tcl_change_info_gen info_gen =
   (fun gls ->
+     let it, eff = sig_it gls, sig_eff gls in
      let concl = pf_concl gls in
-     let hyps = Goal.V82.hyps (project gls) (sig_it gls) in
-     let extra = Goal.V82.extra (project gls) (sig_it gls) in
+     let hyps = Goal.V82.hyps (project gls) it in
+     let extra = Goal.V82.extra (project gls) it in
      let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
-     let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in
-     { it = [gl] ; sigma= sigma } )
+     let sigma = Goal.V82.partial_solution sigma it ev in
+     { it = [gl] ; sigma= sigma; eff = eff } )
 
 let tcl_change_info info gls =
   let info_gen s = Store.set s Decl_mode.info info in
@@ -128,34 +129,34 @@ let go_to_proof_mode () =
 
 let daimon_tac gls =
   set_daimon_flag ();
-  {it=[];sigma=sig_sig gls}
+  {it=[];sigma=sig_sig gls;eff=gls.eff}
 
 (* post-instruction focus management *)
 
 (* spiwack: This used to fail if there was no focusing command
    above, but I don't think it ever happened. I hope it doesn't mess
    things up*)
-let goto_current_focus pts = 
-  Decl_mode.maximal_unfocus pts
+let goto_current_focus () = 
+  Decl_mode.maximal_unfocus ()
 
-let goto_current_focus_or_top pts =
-  goto_current_focus pts
+let goto_current_focus_or_top () =
+  goto_current_focus ()
 
 (* return *)
 
-let close_tactic_mode pts =
-  try goto_current_focus pts
+let close_tactic_mode () =
+  try goto_current_focus ()
   with Not_found ->
     error "\"return\" cannot be used outside of Declarative Proof Mode."
 
 let return_from_tactic_mode () =
-  close_tactic_mode (Proof_global.give_me_the_proof ())
+  close_tactic_mode ()
 
 (* end proof/claim *)
 
 let close_block bt pts =
     if Proof.no_focused_goal pts then
-      goto_current_focus pts
+      goto_current_focus ()
     else
       let stack =
 	if Proof.is_done pts then
@@ -165,7 +166,7 @@ let close_block bt pts =
       in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
-	  (goto_current_focus pts)
+	  (goto_current_focus ())
       | _, Claim::_ ->
 	  error "\"end claim\" expected."
       | _, Focus_claim::_ ->
@@ -190,13 +191,13 @@ let close_previous_case pts =
     match get_top_stack pts with
 	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus (pts)
+	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
   else
     match get_stack pts with
 	Per (et,_,_,_) :: _ -> ()
       | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus ((pts))
+	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
 
 (* Proof instructions *)
@@ -1443,21 +1444,21 @@ let rec postprocess pts instr =
 	  in
 	    try
 	      Inductiveops.control_only_guard env pfterm;
-	      goto_current_focus_or_top pts
+	      goto_current_focus_or_top ()
  	    with
 		Type_errors.TypeError(env,
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
     | Pend _ ->
-	goto_current_focus_or_top (pts)
+	goto_current_focus_or_top ()
 
 let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
   begin
     if has_tactic then
-      let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
-      let gl = { it=List.hd gls ; sigma=sigma } in
+            let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
+      let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in
       let env=  pf_env gl in
       let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
 		 gsigma = sigma; genv = env} in
@@ -1469,7 +1470,7 @@ let do_instr raw_instr pts =
   postprocess pts raw_instr.instr;
   (* spiwack: this should restore a compatible semantics with
      v8.3 where we never stayed focused on 0 goal. *)
-  Decl_mode.maximal_unfocus pts
+  Decl_mode.maximal_unfocus ()
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 8f570af7e2..072737dab2 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -65,7 +65,7 @@ let vernac_decl_proof () =
   if Proof.is_done pf then 
     Errors.error "Nothing left to prove here."
   else
-    Proof.transaction pf begin fun () ->
+    begin
       Decl_proof_instr.go_to_proof_mode () ;
       Proof_global.set_proof_mode "Declarative" ;
       Vernacentries.print_subgoals ()
@@ -73,14 +73,14 @@ let vernac_decl_proof () =
 
 (* spiwack: some bureaucracy is not performed here *)
 let vernac_return () =
-  Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () ->
+  begin
     Decl_proof_instr.return_from_tactic_mode () ;
     Proof_global.set_proof_mode "Declarative" ;
     Vernacentries.print_subgoals ()
   end
 
 let vernac_proof_instr instr =
-  Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () ->
+  begin
     Decl_proof_instr.proof_instr instr;
     Vernacentries.print_subgoals ()
   end
@@ -397,4 +397,10 @@ GLOBAL: proof_instr;
   ;
 END;;
 
- 
+open Vernacexpr
+
+let () =
+  Vernac_classifier.declare_vernac_classifier "decl_mode" (function
+    | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow
+    | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater
+    | _ -> VtUnknown, VtNow)