goodlyrottenapple
commented
1 year ago @jeanas The issue you are experiencing comes from the overloading of the ~> symbol when compiling your definition from the highl-level K language to the kore format used by the haskell/llvm execution engines. If you inspect the definition.kore file inside the lambda-kompiled/ folder, you will find that the
<bound-variables>
_S ~> BoundRest => BoundRest
</bound-variables>portion of the problematic rule has been translated into the kore language as:
Lbl'-LT-'bound-variables'-GT-'{}(
append{}(
Var'Unds'S:SortK{},
VarBoundRest:SortK{}
)
)In the above pattern, both variables have been given the most generic sort possible, namely K.
However, as per the error message, your <bound-variables> cell just before the failure looks like this:
Lbl'-LT-'bound-variables'-GT-'{}(
kseq{}(
inj{SortSet{}, SortKItem{}}(
LblSetItem{}(
inj{SortId{}, SortKItem{}}(
\dv{SortId{}}("x")
)
)
),
kseq{}(
inj{SortSet{}, SortKItem{}}(
Lbl'Stop'Set{}()
),
dotk{}()
)
)
)In the high-level K syntax, this corresponds to
<bound-variables>
SetItem ( x ) ~> .Set ~> .
</bound-variables>as you can see, in this instance the compiler has transformed ~> into a kseq{}. This is because it inferred the types of the arguments to be of a more specific sort than K, namely that of Set injected into the sort KItem. Because of this more specific type,we have a kseq instead of append. Thus, a fix for your rule would be to add a more specific type to _S, as you know it must be a Set:
rule [debugme]: <state> ListFreeVariables() </state>
<list-free-variables>
done(U) ~> AbstracFreezer(X) ~> Rest => done(/\\ X . U) ~> Rest
</list-free-variables>
<bound-variables>
_S:Set ~> BoundRest => BoundRest
</bound-variables>
Baltoli
radumereuta
What component is the issue in?
haskell-backend
Which command
What K Version?
v5.6.90 (Thu May 11 22:42:38 CEST 2023)
Operating System
Linux
K Definitions (If Possible)
This is minimized from a larger file that is supposed to reduce λ-terms (NB I am a beginner with K).
Steps to Reproduce
Save the above as
lambda.k. Save the following assimple.lambda:Then run:
This gives this huge error message:
Here is the file it created: kore-exec.tar.gz
If the LLVM backend is used, it doesn't crash, but it stops at a point where I would have thought that the rule marked
debugmewould apply. Not sure if I'm doing something silly.I tried debugging with GDB but it gives errors as well. Not sure if this is related. Excerpt from GDB session:
Expected Results
No crash.