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, 10 insertions, 11 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 06c52e4b26..d764894fad 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -55,6 +55,8 @@ let xml_export = ref false
 
 let ide_slave = ref false
 
+let time = ref false
+
 type load_proofs = Force | Lazy | Dont
 
 let load_proofs = ref Lazy
diff --git a/lib/flags.mli b/lib/flags.mli
index 14b9f26bcc..388b33c125 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -22,6 +22,8 @@ val xml_export : bool ref
 
 val ide_slave : bool ref
 
+val time : bool ref
+
 type load_proofs = Force | Lazy | Dont
 val load_proofs : load_proofs ref
 
diff --git a/lib/vcs.ml b/lib/vcs.ml
index 2202ddeb0c..dda0384f06 100644
--- a/lib/vcs.ml
+++ b/lib/vcs.ml
@@ -28,7 +28,7 @@ module type S = sig
   
   type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
   
-  val empty : default_info:'info -> id -> ('kind,'diff,'info) t
+  val empty : id -> ('kind,'diff,'info) t
   
   val current_branch : ('k,'e,'i) t -> branch_name
   val branches : ('k,'e,'i) t -> branch_name list
@@ -45,7 +45,7 @@ module type S = sig
   val checkout : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
   
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
-  val get_info : ('k,'e,'info) t -> id -> 'info
+  val get_info : ('k,'e,'info) t -> id -> 'info option
 
   val create_cluster : ('k,'e,'i) t -> id list -> ('k,'e,'i) t
 
@@ -78,14 +78,12 @@ type ('kind,'edge,'info) t = {
   cur_branch   : branch_name;
   heads        : (branch_name * 'kind branch_info) list;
   dag          : ('edge,'info) Dag.t;
-  default_info : 'info;
 }
 
-let empty ~default_info root = {
+let empty root = {
   cur_branch = master; 
   heads = [ master, { root = root; pos = root; kind = `Master } ];
   dag = Dag.empty;
-  default_info;
 }
 
 let add_node vcs id edges =
@@ -113,12 +111,10 @@ let delete_branch vcs name = { vcs with
 
 let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
   assert (name <> into);
-  let local = into = vcs.cur_branch in
   let br_id = (get_branch vcs name).pos in
   let cur_id = (get_branch vcs into).pos in
   let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
   let vcs = reset_branch vcs into id in
-  let vcs = if  local then reset_branch vcs name id else vcs in
   vcs
 
 let commit vcs id tr =
@@ -129,8 +125,7 @@ let commit vcs id tr =
 let checkout vcs name = { vcs with cur_branch = name }
 
 let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
-let get_info vcs id =
-  match Dag.get_info vcs.dag id with Some x -> x | None -> vcs.default_info
+let get_info vcs id = Dag.get_info vcs.dag id
 
 let create_cluster vcs l = { vcs with dag = Dag.create_cluster vcs.dag l }
 
diff --git a/lib/vcs.mli b/lib/vcs.mli
index 7c82352aef..7ac568c127 100644
--- a/lib/vcs.mli
+++ b/lib/vcs.mli
@@ -43,7 +43,7 @@ module type S = sig
   
   type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
   
-  val empty : default_info:'info -> id -> ('kind,'diff,'info) t
+  val empty : id -> ('kind,'diff,'info) t
   
   val current_branch : ('k,'e,'i) t -> branch_name
   val branches : ('k,'e,'i) t -> branch_name list
@@ -60,7 +60,7 @@ module type S = sig
   val checkout : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
   
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
-  val get_info : ('k,'e,'info) t -> id -> 'info
+  val get_info : ('k,'e,'info) t -> id -> 'info option
 
   val create_cluster : ('k,'e,'i) t -> id list -> ('k,'e,'i) t