Parametric rules
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 25/100
Research direction
Read the parametric productions section in pending-documentation.md and inspect the examples in k-distribution/include/kframework/builtin/domains.k. Then trace how the Haskell backend applies the existing equations and determine where parametric rule support belongs. Done means parametric rules work across sort parameters without requiring separate sort-specific rules.
Written by the indexing model from the issue text.
Description
K supports parametric productions such as this one from domains.k
syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, functional, smt-hook(ite), hook(KEQUAL.ite)]
There is no corresponding way to write parametric rules for parametric productions, so we have rules such as these:
rule #if C:Bool #then B1::K #else _ #fi => B1 requires C
rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C
which restrict the sort parameter to K. These equations can only be applied by the Haskell backend when the #then and #else expressions are explicitly of sort K.
As a workaround, we can add specific rules for any sort which needs support, for example:
rule #if C:Bool #then B1::Int #else _ #fi => B1 requires C
rule #if C:Bool #then _ #else B2::Int #fi => B2 requires notBool C
This workaround quickly becomes tedious, though.
- Dominant language
- Python
- Stars
- 591
- Forks
- 163
- PR merge metrics
- No merged PRs in 30d
Contributor guide
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.
More from runtimeverification/k
-
runtimeverification/k#4939 · 1 assignee ·
-
Concolic Explorer Open
Difficulty 5/5 Over a week Newbie friendliness 32/100
runtimeverification/k#4937 ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
runtimeverification/k#4936 ·
-
type:epic
runtimeverification/k#4934 · 4 comments · 1 assignee ·
-
runtimeverification/k#4924 · 1 assignee ·
All issues in runtimeverification/k
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
bancolombia/sentinel#23 ·
-
test md OpenCI
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
-
integration:quickjs org:external priority:backlog topic:code-interpreter topic:middleware type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
langchain-ai/deepagents#6450 ·
-
bug client
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100