runtimeverification / runtimeverification/haskell-backend
Invalid variable names created by internalized rules
@nwatson22 is already working on this.
Since Mar 26, 2024.
- Dominant language
- Haskell
- Stars
- 224
- Forks
- 43
- PR merge metrics
- No merged PRs in 30d
Description
I stumbled across a case where a Rule# prefix is seemingly being appended to the beginning of a variable name for the generatedCounter cell possibly caused by using a claim as a lemma (the last request/response in this bug report). Is this a genuine bug? See https://github.com/runtimeverification/pyk/pull/959
<generatedCounter> in the response looks like this:
{
"tag":"App",
"name":"Lbl'-LT-'generatedCounter'-GT-'",
"sorts":[
],
"args":[
{
"tag":"EVar",
"name":"Rule#Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b",
"sort":{
"tag":"SortApp",
"name":"SortInt",
"args":[
]
}
}
]
}
Executing with the legacy backend yields the same variable name Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b without the Rule# prefix.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.