Open malturki opened 2 years ago
This is probably because the exhaustiveness check is not interacting correctly with the overloaded syntax, so it thinks that the rule won't match a TList. This is actually a bug in the llvm backend, but we can look into it.
Thanks for the feedback. Obviously this is not high priority, but I thought I should have it confirmed and documented.
@Baltoli whenever you have time, this could help you get familiar with the llvm backend. @dwightguth can provide assistance.
Possibly needs replication; will most likely still occur though.
@dwightguth suggests that the trick here is to modify the exhaustiveness algorithm somehow but that the fix might not be obvious.
Here is one more example, extracted from the wasm semantics:
a.k
module A
syntax A ::= "a" | B
syntax B ::= "b"
syntax Bs ::= List{B, ""}
syntax As ::= List{A, ""}
syntax As ::= Bs
syntax K ::= f(As) [function, total]
rule f(.As) => .K
rule f(A AA) => A ~> f(AA)
endmodule
Command line:
$ kompile a.k --backend llvm
[Warning] Compiler: Non exhaustive match detected:
`f(_)_A_K_As`(`.List{"___A_As_A_As"}_As`(.KList))
Source(/mnt/data/runtime-verification/elrond-wasm-real-elrond/kmxwasm/tmp/a.k)
Location(9,16,9,40)
9 | syntax K ::= f(As) [function, total]
. ^~~~~~~~~~~~~~~~~~~~~~~~
The same warning shows up if the two list productions have the [klabel(stuff)]
attribute (the original rules in the WASM semantics have it) and if one adds rule f(B:Bs) => B
to the semantics.
K Version
Description
kompile emits a "Non exhaustive match detected" warning seemingly unnecessarily in some cases (see the minimal example below). The function for which it gives the warning is declared
functional
and is sufficiently completely specified as far as I can tell.Note: when uncommenting the
owise
line in the example below, the warning is not shown. But it shouldn't be needed, I think.Input Files
The
owise.k
file below:Reproduction Steps
Expected Behavior
No "Non exhaustive match detected" warning is emitted.