From b2f2727670853183bfbcbafb9dc19f0f71494a7b Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:51:35 +0000 Subject: 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 --- proofs/goal.mli | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'proofs/goal.mli') diff --git a/proofs/goal.mli b/proofs/goal.mli index bb1c0639e..345f46abf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -41,13 +41,15 @@ type subgoals = private { subgoals: goal list } type +'a sensitive (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *) -val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map +val eval : + 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> + 'a * Evd.evar_map * Declareops.side_effects (* monadic bind on sensitive expressions *) val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive (* monadic return on sensitive expressions *) -val return : 'a -> 'a sensitive +val return : 'a -> Declareops.side_effects -> 'a sensitive (* interpretation of "open" constr *) @@ -168,10 +170,10 @@ val here_list : goal list -> 'a -> 'a sensitive (* emulates List.map for functions of type [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating new evar_map to next definition *) -val list_map : (Evd.evar_map -> 'a -> 'b * Evd.evar_map) -> - 'a list -> - Evd.evar_map -> - 'b list *Evd.evar_map +val list_map : + (Evd.evar_map -> 'a -> 'b * Evd.evar_map * Declareops.side_effects) -> + 'a list -> Evd.evar_map -> + 'b list * Evd.evar_map * Declareops.side_effects list (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the -- cgit v1.2.3