Add --pattern support to the llvm backend via haskell backend tool #2370
Conversation
| V ==K ( y ~> #freezer___LAMBDA1_ ( lambda x . lambda y . x ) ~> #freezer___LAMBDA0_ ( z ) ~> #freezer___LAMBDA1_ ( a ) ) | ||
| #Or | ||
| V ==K ( z ~> #freezer___LAMBDA1_ ( ( lambda x . lambda y . x ) y ) ~> #freezer___LAMBDA1_ ( a ) ) | ||
| #Or | ||
| V ==K ( z ~> #freezer___LAMBDA1_ ( closure ( .Map , x , lambda y . x ) y ) ~> #freezer___LAMBDA1_ ( a ) ) | ||
| { | ||
| V:K | ||
| #Equals | ||
| z ~> #freezer___LAMBDA_Exp_Exp_Exp1_ ( ( lambda x . lambda y . x ) y ~> . ) ~> #freezer___LAMBDA_Exp_Exp_Exp1_ ( a ~> . ) ~> . | ||
| } |
There was a problem hiding this comment.
We have less search results in the post-state than the pre. Is this intentional? (just want to make sure it's double-checked)
There was a problem hiding this comment.
This is intentional. The java backend implements some custom logic to ensure that heating and cooling rules can apply at any time while also preventing them from applying in an infinitely looping cycle. The Haskell and LLVM backends do not do this, and thus require that any heated term be fully evaluated before cooling. That is why you lose two behaviors in each instance of this particular program. I have previously spoken with @grosu and he has explicitly stated he is okay with making this change for the time being in order to be able to migrate the lessons in the pl-tutorial. We can revisit and readd these behaviors when we have an actual need to implement the full nondeterminism of heating/cooling in K.
There was a problem hiding this comment.
Ok, is this recorded in an issue somewhere? We don't want to forget.
There was a problem hiding this comment.
I will create an issue.
There was a problem hiding this comment.
* haskell-backend/src/main/native/haskell-backend: c4278195 - Keep table of term replacements in SideCondition, use in term simplifier (runtimeverification#2315) * haskell-backend/src/main/native/haskell-backend: 51607104 - Update dependency: deps/k_release * haskell-backend/src/main/native/haskell-backend: 44423faa - Remove build date from version info and add dirty flag (runtimeverification#2370) * haskell-backend/src/main/native/haskell-backend: d0412b76 - Update dependency: deps/k_release * haskell-backend/src/main/native/haskell-backend: e87dac75 - Fix uninterpreted functions in keys of Maps and Sets (runtimeverification#2323) * haskell-backend/src/main/native/haskell-backend: deaf0af1 - Keep set of defined terms in SideCondition (runtimeverification#2354) * haskell-backend/src/main/native/haskell-backend: 266597e9 - Revert runtimeverification#2315 (runtimeverification#2385) * haskell-backend/src/main/native/haskell-backend: d18be998 - kore-0.39.0.0 (runtimeverification#2388)
Basically, we add support for --pattern passed to krun when you use the llvm backend, by means of delegating the search pattern matching to the haskell backend.
Fixes #1742