ApplyEquations refactor #555
Conversation
|
|
||
| llvmEval :: MonadLoggerIO io => KoreDefinition -> LLVM.API -> Term -> EquationT io Term | ||
| llvmEval definition api = eval | ||
| let simp = cached LLVM $ evalLlvm config.definition api $ traverseTerm BottomUp simp pure |
There was a problem hiding this comment.
BottomUp or TopDown are equivalent if onEval is just pure:
| direction == BottomUp -> do
-- evaluate arguments first
args' <- mapM onRecurse args
-- then try to apply equations
pure $ SymbolApplication sym sorts args'
| otherwise {- direction == TopDown -} -> do
-- try to apply equations
t <- pure app
SymbolApplication sym sorts
<$> mapM onRecurse args
There was a problem hiding this comment.
Indeed they are... but somehow I don't see how the cut-off is implemented.
If we have nested concrete terms, e.g., +Int(2, +Int(3, 4)) ,Is the llvm backend going to be called twice, for 3 + 4 and then 2 + 7, or is it called just once as a top-down traversal with cut-off would?
EDIT: with the recursion in what is called cb , this is indeed cutting the traversal short.
I concur we should call cb a different name, and leave a comment for posterity.
|
No difference in performance in KEVM |
| when (cached /= t) setChanged >> pure cached | ||
|
|
||
| eval' t@(Term attributes _) | ||
| evalLlvm definition api cb t@(Term attributes _) |
There was a problem hiding this comment.
I think this function deserves to have:
- an explicit type signature
- a better name for the
cbparameter, together with the comment on what the callback does. How about we call ittraversalActionor something along these lines?
| -- Bottom-up evaluation traverses AST nodes in post-order but finds work top-down | ||
| -- Top-down evaluation traverses AST nodes in pre-order | ||
| apply config = \case | ||
| traverseTerm :: |
There was a problem hiding this comment.
I suggest we expand the documentation of this function to reference it's two current instantiations, llvmSimplify and iterateEquations.
| Just cachedTerm -> do | ||
| when (t /= cachedTerm) $ do | ||
| setChanged | ||
| emitEquationTrace t Nothing (Just "Cache") Nothing $ Success cachedTerm |
There was a problem hiding this comment.
We may want to specify which cache the equation application came from:
| emitEquationTrace t Nothing (Just "Cache") Nothing $ Success cachedTerm | |
| emitEquationTrace t Nothing (Just ("Cache" <> show cacheTag)) Nothing $ Success cachedTerm |
geo2a
dismissed
their stale review
Actually, we do want to have the Kontrol performance tests results as well.
|
Kontrol
|
Incremental change towards design discussed in runtimeverification/haskell-backend#3772
Refactor definitions of applyTerm and llvmSimplify