The result of simplifying some expression e
.
- expr : Expr
The simplified version of
e
A proof that
$e = $expr
, where the simplified expression is on the RHS. Ifnone
, the proof is assumed to berefl
.- cache : Bool
If
cache := true
the result is cached. Warning: we will remove this field in the future. It is currently used byarith := true
, but we can now refactor the code to avoid the hack.
Instances For
- config : Config
- zetaDeltaSet : FVarIdSet
Local declarations to propagate to
Meta.Context
- initUsedZetaDelta : FVarIdSet
When processing
Simp
arguments,zetaDelta
may be performed ifzetaDeltaSet
is not empty. We save the local free variable ids ininitUsedZetaDelta
.initUsedZetaDelta
is a subset ofzetaDeltaSet
. - metaConfig : ConfigWithKey
- indexConfig : ConfigWithKey
- maxDischargeDepth : UInt32
maxDischargeDepth
fromconfig
as anUInt32
. - simpTheorems : SimpTheoremsArray
- congrTheorems : SimpCongrTheorems
Stores the "parent" term for the term being simplified. If a simplification procedure result depends on this value, then it is its reponsability to set
Result.cache := false
.Motivation for this field: Suppose we have a simplification procedure for normalizing arithmetic terms. Then, given a term such as
t_1 + ... + t_n
, we don't want to apply the procedure to every subtermt_1 + ... + t_i
fori < n
for performance issues. The procedure can accomplish this by checking whether the parent term is also an arithmetical expression and do nothing if it is. However, it should setResult.cache := false
to ensure we don't miss simplification opportunities. For example, consider the following:example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by simp +arith only ...
If we don't set
Result.cache := false
for the firstx + x
, then we get the resulting state:... |- id (2*x + y) = id (x + x)
instead of
... |- id (2*x + y) = id (2*x)
as expected.
Remark: given an application
f a b c
the "parent" term forf
,a
,b
, andc
isf a b c
.- dischargeDepth : UInt32
- lctxInitIndices : Nat
Number of indices in the local context when starting
simp
. We use this information to decide which assumptions we can use without invalidating the cache. - inDSimp : Bool
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Number of times each simp theorem has been used/applied.
Number of times each simp theorem has been tried.
Number of times each congr theorem has been tried.
- thmsWithBadKeys : PArray SimpTheorem
When using
Simp.Config.index := false
, andset_option diagnostics true
, for every theorem used bysimp
, we check whether the theorem would be also applied ifindex := true
, and we store it here if it would not have been tried.
Instances For
- cache : Cache
- congrCache : CongrCache
- dsimpCache : ExprStructMap Expr
- usedTheorems : UsedSimps
- numSteps : Nat
- diag : Diagnostics
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Executes x
using a MetaM
configuration for indexing terms.
It is inferred from Simp.Config
.
For example, if the user has set simp (config := { zeta := false })
,
isDefEq
and whnf
in MetaM
should not perform zeta
reduction.
Equations
Instances For
Executes x
using a MetaM
configuration for inferred from Simp.Config
.
Equations
Instances For
Equations
Instances For
Similar to Simproc
, but resulting expression should be definitionally equal to the input one.
Equations
Instances For
Simproc
entry. It is the .olean entry plus the actual function.
Recall that we cannot store
Simproc
into .olean files because it is a closure. GivenSimprocOLeanEntry.declName
, we convert it into aSimproc
by using the unsafe functionevalConstCheck
.
Instances For
- pre : SimprocTree
- post : SimprocTree
Instances For
- pre : Simproc
- post : Simproc
- dpre : DSimproc
- dpost : DSimproc
- wellBehavedDischarge : Bool
wellBehavedDischarge
must not be set totrue
IFdischarge?
access local declarations with index >=Context.lctxInitIndices
whencontextual := false
. Reason: it would prevent us from aggressively cachingsimp
results.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Save current cache, reset it, execute x
, and then restore original cache.
Equations
Instances For
Equations
Instances For
Similar to Result.getProof
, but adds a mkExpectedTypeHint
if proof?
is none
(i.e., result is definitionally equal to input), but we cannot establish that
source
and r.expr
are definitionally when using TransparencyMode.reducible
.
Equations
Instances For
Auxiliary method.
Given the current target
of mvarId
, apply r
which is a new target and proof that it is equal to the current one.