diff options
| author | gareuselesinge | 2013-10-31 14:24:46 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:46 +0000 |
| commit | a46165247a22d9f1015dea81a17ee2f5c2ee6099 (patch) | |
| tree | 61fe946caf460e8d888c53914a6b6ab3dabb119c /toplevel | |
| parent | 6637d0b8cc876e91ced18cb0ea481463bddfe2eb (diff) | |
Future: better doc + restore ~pure optimization
This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored. This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 8 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 5 |
2 files changed, 8 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 04a2661d72..e63ff19915 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -68,9 +68,11 @@ let red_constant_entry n ce = function | None -> ce | Some red -> let proof_out = ce.const_entry_body in - { ce with const_entry_body = Future.chain proof_out (fun (body,eff) -> - under_binders (Global.env()) - (fst (reduction_of_red_expr (Global.env()) red)) n body,eff) } + let env = Global.env () in + { ce with const_entry_body = Future.chain ~pure:true proof_out + (fun (body,eff) -> + under_binders env + (fst (reduction_of_red_expr env red)) n body,eff) } let interp_definition bl red_option c ctypopt = let env = Global.env() in diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 519112dfdb..d6b868b004 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -48,8 +48,9 @@ let adjust_guardness_conditions const = function | [] -> const (* Not a recursive statement *) | possible_indexes -> (* Try all combinations... not optimal *) + let env = Global.env() in { const with const_entry_body = - Future.chain const.const_entry_body + Future.chain ~pure:true const.const_entry_body (fun (body, eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -59,7 +60,7 @@ let adjust_guardness_conditions const = function lemma_guard (Array.to_list fixdefs) in *) let indexes = - search_guard Loc.ghost (Global.env()) + search_guard Loc.ghost env possible_indexes fixdecls in mkFix ((indexes,0),fixdecls), eff | _ -> body, eff) } |