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

1 files changed, 39 insertions, 0 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d19857ee1..2f8ab3813 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -8,6 +8,8 @@
 
 open Loc
 open Pp
+open Util
+open Stateid
 open Names
 open Tacexpr
 open Misctypes
@@ -214,6 +216,13 @@ type bullet =
     | Star
     | Plus
 
+(** {6 Types concerning Stm} *)
+type 'a stm_vernac =
+  | JoinDocument
+  | Finish
+  | Observe of Stateid.state_id
+  | Command of 'a (* An out of flow command not to be recorded by Stm *)
+
 (** {6 Types concerning the module layer} *)
 
 (** Rigid / flexible module signature *)
@@ -372,6 +381,9 @@ type vernac_expr =
   | VernacComments of comment list
   | VernacNop
 
+  (* Stm backdoor *)
+  | VernacStm of vernac_expr stm_vernac
+
   (* Proof management *)
   | VernacGoal of constr_expr
   | VernacAbort of lident option
@@ -401,3 +413,30 @@ type vernac_expr =
   | VernacLocal of bool * vernac_expr
 
 and located_vernac_expr = Loc.t * vernac_expr
+
+(* A vernac classifier has to tell if a command:
+   vernac_when: has to be executed now (alters the parser) or later
+   vernac_type: if it is starts, ends, continues a proof or
+     alters the global state or is a control command like BackTo or is
+     a query like Check *)
+type vernac_type =
+  | VtStartProof of vernac_start
+  | VtSideff
+  | VtQed of vernac_qed_type
+  | VtProofStep
+  | VtQuery of vernac_part_of_script
+  | VtStm of vernac_control * vernac_part_of_script
+  | VtUnknown
+and vernac_qed_type = KeepProof | DropProof (* Qed, Admitted/Abort *)
+and vernac_start = string * Id.t list
+and vernac_is_alias = bool
+and vernac_part_of_script = bool
+and vernac_control =
+  | VtFinish
+  | VtJoinDocument
+  | VtObserve of state_id
+  | VtBack of state_id
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when