You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
module FORMAT
syntax Foo ::= r"foo" Bar [symbol(foo), format("%2")]
syntax Bar ::= "bar"
endmodule
The generated KORE symbol for foo is then the following:
symbol Lblfoo{}(SortBar{}) : SortFoo{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2,20,2,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/ttoth/git/pyk/format.k)"), symbol'Kywd'{}("foo")]
Notice how format is present in the input but not the output. This is because ModuleToKORE does not generate format for productions that have items other than terminals and non-terminals:
Does it make sense to have format only in KAST and not in KORE? If not, we should add a validation pass that emits an error if format is put on such a production.
The text was updated successfully, but these errors were encountered:
The KAST and KORE format attributes are different; the LLVM backend can't handle regex terminals in the same way as the frontend. The underlying issue is turning a regex expression into a string, but maybe we should allow the user to pass the attribute through so long as they don't mention the regex terminal.
Possibly related: there's already an error that enforces format on productions with regex terminals:
[Error] Compiler: Expected format attribute on production with regular
expression terminal.
Source(/home/ttoth/git/pyk/format.k)
Location(2,20,2,44)
2 | syntax Foo ::= r"foo" Bar [symbol(foo)]
. ^~~~~~~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 structural errors.
Consider the following definition:
The generated KORE symbol for
foo
is then the following:Notice how
format
is present in the input but not the output. This is becauseModuleToKORE
does not generateformat
for productions that have items other than terminals and non-terminals:k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
Line 1726 in 61bd789
Does it make sense to have format only in KAST and not in KORE? If not, we should add a validation pass that emits an error if
format
is put on such a production.The text was updated successfully, but these errors were encountered: