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/mod_typing.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/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f7f3c2b77..67db4e806 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -97,16 +97,17 @@ and check_with_def env sign (idl,c) mp equiv = let (j,cst1) = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in let cst2 = Reduction.conv_leq env' j.uj_type typ in - let cst = - union_constraints - (union_constraints cb.const_constraints cst1) + let cst = union_constraints + (union_constraints + (Future.force cb.const_constraints) cst1) cst2 in let def = Def (Lazyconstr.from_val j.uj_val) in def,cst | Def cs -> let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in - let cst = union_constraints cb.const_constraints cst1 in + let cst = union_constraints + (Future.force cb.const_constraints) cst1 in let def = Def (Lazyconstr.from_val c) in def,cst in @@ -115,7 +116,7 @@ and check_with_def env sign (idl,c) mp equiv = const_body = def; const_body_code = Cemitcodes.from_val (compile_constant_body env' def); - const_constraints = cst } + const_constraints = Future.from_val cst } in SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst | _ -> @@ -373,13 +374,14 @@ let rec add_struct_expr_constraints env = function (add_struct_expr_constraints env meb1) meb2) | SEBwith(meb,With_definition_body(_,cb))-> - Environ.add_constraints cb.const_constraints + Environ.add_constraints (Future.force cb.const_constraints) (add_struct_expr_constraints env meb) | SEBwith(meb,With_module_body(_,_))-> add_struct_expr_constraints env meb and add_struct_elem_constraints env = function - | SFBconst cb -> Environ.add_constraints cb.const_constraints env + | SFBconst cb -> + Environ.add_constraints (Future.force cb.const_constraints) env | SFBmind mib -> Environ.add_constraints mib.mind_constraints env | SFBmodule mb -> add_module_constraints env mb | SFBmodtype mtb -> add_modtype_constraints env mtb @@ -418,7 +420,7 @@ let rec struct_expr_constraints cst = function meb2 | SEBwith(meb,With_definition_body(_,cb))-> struct_expr_constraints - (Univ.union_constraints cb.const_constraints cst) meb + (Univ.union_constraints (Future.force cb.const_constraints) cst) meb | SEBwith(meb,With_module_body(_,_))-> struct_expr_constraints cst meb |