Parametric rules

[ttuegel]

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.

[dwightguth]

The first step of implementing this is modifying the parser so that you can infer that the sort of a variable or production parameter is a sort variable instead of a concrete sort. I can't tell you precisely what this will require, but it may require changes to the grammar generator, parser, and/or sort inferencer. You will have to try and write such a sentence and see where things start to go wrong.

[ttuegel]

We would like to write parametric rules thus:

  rule {S} #if C:Bool #then B1:S #else _ #fi => B1 requires C
  rule {S} #if C:Bool #then _ #else B2:S #fi => B2 requires notBool C

The translation to Kore would not change, except that the corresponding axioms would have a sort parameter,

  axiom {S} ...

and that the sort variable would appear in place of the concrete sort.

[radumereuta]

I found a few bugs in kompile that are blocking me from solving this. This simple production makes kore-exec complain about missing parameters:
syntax {S} Exp ::= minus(S) [klabel(minus), symbol]
I managed to trace a few of the issues to:

• ModuleToKore: 'no junk' axiom generation doesn't take into consideration parameters - kore-exec complains
• ModuleToKore: 'no confusion different constructors' axiom generation same issue
• productionsForSort seem to be incorrect. I'm assuming that parameter names take priority over sort names in a production. At least that seems to be the behavior in kore-exec.

lazy val productionsForSort: Map[SortHead, Set[Production]] =
    productions
      .filter(prd => !prd.isSortVariable(prd.sort)) // line added
      .groupBy(_.sort.head)
      .map { case (l, ps) => (l, ps) }

This makes flex to crash. Need to investigate further, but I would like confirmation that this is the behavior we want.

Can someone also confirm that returning a parametric sort is not supported by the haskell-backend?

syntax {Exp} Exp ::= mul(Exp) [klabel(mul), symbol]
radu@radu:~/work/test$ kompile test.k --backend haskell
Error:
  module 'TEST':
  symbol 'Lblmul' declaration (definition.kore 151:10):
    Cannot define constructor Lblmul with variable result sort.
[Error] Critical: Haskell backend reported errors validating compiled
definition.
Examine output to see errors.

What should we do in kompile then? Is this not yet supported, but should be in the future? Is this available only for hooked symbols?
syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, functional, smt-hook(ite), hook(KEQUAL.ite)]

[ttuegel]

Can someone also confirm that returning a parametric sort is not supported by the haskell-backend?

The backend supports parametric symbols. I need to see what Kore sentences are generated to say what is wrong here.

[radumereuta]

Does this help?

radu@radu:~/work/test$ cat test.k
module TEST
  syntax {S} S ::= mul(S) [klabel(mul), symbol]
endmodule
radu@radu:~/work/test$ kompile test.k --backend haskell
Error:
  module 'TEST':
  symbol 'Lblmul' declaration (definition.kore 136:10):
    Cannot define constructor Lblmul with variable result sort.
[Error] Critical: Haskell backend reported errors validating compiled
definition.
Examine output to see errors.

definition.kore:136

  symbol Lblmul{SortS}(SortS) : SortS [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/test/./test.k)"), symbol'Kywd'{}(), priorities{}(), right{}(), terminals{}("1101"), klabel{}("mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2,20,2,47)"), left{}(), format{}("%cmul%r %c(%r %1 %c)%r"), injective{}()]

[ttuegel]

You can't define constructors in any sort. This would allow you to bypass the restriction against defining constructors in built-in sorts, for example. You need at least one sort constructor in any constructor declaration, e.g.

syntax {S} C{S} ::= mul(S)

[ttuegel]

I'm assuming that parameter names take priority over sort names in a production. At least that seems to be the behavior in kore-exec.

In Kore, parameter names and sort names are syntactically distinct.

[ehildenb]

We do not need to worry about parametric sorts or constructors yet. Let's just get parametric function symbols ironed out first.