diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
| commit | b2f2727670853183bfbcbafb9dc19f0f71494a7b (patch) | |
| tree | 8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /kernel/modops.ml | |
| parent | 1f48326c7edf7f6e7062633494d25b254a6db82c (diff) | |
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
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 3b789016b..39e5514c9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -588,3 +588,32 @@ let clean_bounded_mod_expr = function let str_clean = collect_mbid [] str in if str_clean == str then str else str_clean | str -> str + +let rec join_module_body mb = + Option.iter join_struct_expr_body mb.mod_expr; + Option.iter join_struct_expr_body mb.mod_type_alg; + join_struct_expr_body mb.mod_type +and join_structure_body struc = + let join_body (l,body) = match body with + | SFBconst sb -> join_constant_body sb + | SFBmind _ -> () + | SFBmodule m -> join_module_body m + | SFBmodtype m -> + join_struct_expr_body m.typ_expr; + Option.iter join_struct_expr_body m.typ_expr_alg in + List.iter join_body struc; +and join_struct_expr_body = function + | SEBfunctor (_,t,e) -> + join_struct_expr_body t.typ_expr; + Option.iter join_struct_expr_body t.typ_expr_alg; + join_struct_expr_body e + | SEBident mp -> () + | SEBstruct s -> join_structure_body s + | SEBapply (mexpr,marg,u) -> + join_struct_expr_body mexpr; + join_struct_expr_body marg + | SEBwith (seb,wdcl) -> + join_struct_expr_body seb; + match wdcl with + | With_module_body _ -> () + | With_definition_body (_, sb) -> join_constant_body sb |