diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-17 15:51:25 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-17 17:08:30 +0200 |
commit | b5ed27b9b8043e3df3ee4cd918f93fbf7465285f (patch) | |
tree | 5facb7bad17b086bd0a29cbc219f2aac30865107 | |
parent | 4e0e3022ca9eefefb57632152725b4a4c249ce38 (diff) |
Tentative optimization not to nf_evar too often in the compatibility
layer. To this intent, we add a cache evar_map in goals that is the
latest known one where the goal is nf-evarized. If the current one
and the cache coincide, we leave the goal as-is.
-rw-r--r-- | proofs/goal.ml | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ac3e593da..c31375f9e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -21,7 +21,12 @@ type goal = { content : Evd.evar; (* Corresponding evar. Allows to retrieve logical information once put together with an evar_map. *) - tags : string list (* Heriditary? tags to be displayed *) + tags : string list; + (** Heriditary? tags to be displayed *) + cache : Evd.evar_map; + (** Invariant: for all sigma, if gl.cache == sigma and gl.content is actually + pertaining to sigma, then gl is nf-evarized in sigma. We use this not to + nf-evar goals too often. *) } (* spiwack: I don't deal with the tags, yet. It is a worthy discussion whether we do want some tags displayed besides the goal or not. *) @@ -37,7 +42,8 @@ let content evars { content = e } = Evd.find evars e (* Builds a new (empty) goal with evar [e] *) let build e = { content = e ; - tags = [] + tags = []; + cache = Evd.empty; } @@ -53,7 +59,7 @@ let get_by_uid u = (* Builds a new goal with content evar [e] and inheriting from goal [gl]*) let descendent gl e = - { gl with content = e} + { gl with content = e; cache = Evd.empty } (* [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] @@ -72,7 +78,7 @@ let rec advance sigma g = | Evd.Evar_defined v -> if Option.default false (Evd.Store.get evi.Evd.evar_extra Evarutil.cleared) then let (e,_) = Term.destEvar v in - let g' = { g with content = e } in + let g' = descendent g e in advance sigma g' else None @@ -567,10 +573,12 @@ module V82 = struct (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = - let evi = content sigma gl in - let evi = Evarutil.nf_evar_info sigma evi in - let sigma = Evd.add sigma gl.content evi in - (gl,sigma) + if sigma == gl.cache then (gl, sigma) + else + let evi = content sigma gl in + let evi = Evarutil.nf_evar_info sigma evi in + let sigma = Evd.add sigma gl.content evi in + ({ gl with cache = sigma }, sigma) (* Goal represented as a type, doesn't take into account section variables *) let abstract_type sigma gl = |