Desugar `#Or` in rules - Githubissues

runtimeverification / k

K Framework Tools 7.0

BSD 3-Clause "New" or "Revised" License

447 stars 147 forks source link

Desugar `#Or` in rules #4355

Open Baltoli opened 4 months ago

Baltoli commented 4 months ago

A recent change to the MX semantics (required to provide sensible compilation times on the LLVM backend: https://github.com/runtimeverification/mx-semantics/pull/265) introduces #Or patterns in a set of rules; these are not supported by the booster, which means we can't execute this code symbolically.

We need to add a feature to the frontend that hoists these symbols to the top of rewrite rules when we see them, then duplicates the rules to remove the #Ors.

ehildenb commented 4 months ago

Some thoughts:

#Or only allowed in LHS of rules.
Type-inference done before desugaring #Or.
Restrictions on the symbols under the #Or?

We should look at the examples we need and make it restrictive to only handling those cases.

Baltoli commented 4 months ago

Or only allowed in LHS of rules.

The Haskell backend will permit and happily rewrite rules with #Or on the RHS; the LLVM backend just crashes when you try to compile the definition. We should emit a better error message here.