Antileft for priority rules is not a predicate in the generated kore file

[virgil-serbanuta]

For these rules:

module PRIORITY
  imports INT
  imports BOOL

  syntax S ::= "one" | "two" | "three" | "four" | "five" | "six" | "seven" | start(Int) | middle(Int)

  rule start(X) => one       requires X <Int 0  [priority(1)]
  rule start(X) => middle(X) requires X <Int 10 [priority(2), label(first)]
  rule start(X) => one                          [priority(3)]
endmodule

The generated axiom for middle looks something like this:

  axiom{} \rewrites{SortGeneratedTopCell{}} (
    \and{SortGeneratedTopCell{}}(
      \not{SortGeneratedTopCell{}}(priorityLE1{}()),
      rule2LHS{}(VarDotVar0:SortGeneratedCounterCell{},VarDotVar1:SortK{},VarX:SortInt{})),
    \and{SortGeneratedTopCell{}} (...configuration...))
  [...]

the priorityLE1 alias looks like this:

alias priorityLE1{}() : SortGeneratedTopCell{}
where priorityLE1{}() :=
    \or{SortGeneratedTopCell{}}(
        \exists{SortGeneratedTopCell{}}(VarDotVar0:SortGeneratedCounterCell{},
            \exists{SortGeneratedTopCell{}}(VarDotVar1:SortK{},
                \exists{SortGeneratedTopCell{}}(VarX:SortInt{},
                    rule3LHS{}(VarDotVar0:SortGeneratedCounterCell{},VarDotVar1:SortK{},VarX:SortInt{})
                )
            )
        ),
        \bottom{SortGeneratedTopCell{}}()
    ) []

This looks fine so far, but rule3LHS looks like this

alias rule3LHS{}(SortGeneratedCounterCell{},SortK{},SortInt{}) : SortGeneratedTopCell{}
where rule3LHS{}(VarDotVar0:SortGeneratedCounterCell{},VarDotVar1:SortK{},VarX:SortInt{}) :=
\and{SortGeneratedTopCell{}} (
    \equals{SortBool{},SortGeneratedTopCell{}}(
        Lbl'Unds-LT-'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0")),
        \dv{SortBool{}}("true")
    ),
    Lbl'-LT-'generatedTop'-GT-'{}(...)
) []

Note that the Lbl'-LT-'generatedTop'-GT-'{}(...) part can't occur
in a predicate without having an equals, ceil or something similar above it.

[virgil-serbanuta]

Steps to reproduce:

1. Copy the module above in a file called priority.k
2. kompile priority.k
3. Check the generated definition.kore file and search for first to find the axiom mentioned above.

[dwightguth]

I'm not following this, but it looks like there is something you don't like about how this module is encoded into kore, and it has something to do with the encoding of the priority attribute. I didn't write that code and it's not my responsibility to maintain it; code ownership for that part of the ModuleToKORE file belongs to the haskell backend team, because the llvm backend completely ignores the "antileft", as you call it.

[virgil-serbanuta]

Oh, I asked around and I was told that you wrote the code which generates these axioms. Sorry about that, I probably misunderstood.

For reference, I think that the Haskell backend team expects that antileft thing to be a predicate in the ML sense of the term, and it actually seems to be and(functional term, predicate).

[dwightguth]

I wrote large parts of ModuleToKORE, but I don't claim to be an expert in matching logic. Even if I'm wrong and I did write it and I forgot, I guarantee I was merely writing it to someone else's specification. Whatever problem you are describing, I don't understand it, whereas the haskell backend team likely would, so I don't think I'm the right person to try to fix it.

[ehildenb]

@virgil-serbanuta is this still relevant? If not, please close.

[virgil-serbanuta]

The current behaviour is correct, the antileft part is not supposed to be a predicate. Also see
https://github.com/kframework/kore/blob/master/docs/2020-06-22-Rewrite-Rule-Priorities.md