k-legacy
k-legacy copied to clipboard
Published
20 hours ago •
kframework
kframework
problem with `Bag`
I am trying to send part of the configuration to a function.
rule <k> @egress => (#if @egressDefined(Fls) #then egress (); #else . #fi) ~> @deparseNext(L) ... </k>
<dporder> L:List </dporder>
<controlFlows> Fls:Bag </controlFlows>
syntax Bool ::= "@egressDefined" "(" Bag ")" [function]
...
But kompile gives me error:
java.lang.AssertionError: While defining module CONFIGURATION: Could not find symbol Bag
at org.kframework.definition.SymbolResolver.$anonfun$apply$1(ResolvedSymbol.scala:71)
at scala.Option.getOrElse(Option.scala:121)
at org.kframework.definition.SymbolResolver.apply(ResolvedSymbol.scala:71)
at org.kframework.definition.Module.resolve(outer.scala:113)
at org.kframework.definition.Module.$anonfun$localSyntaxSentences$2(outer.scala:152)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.Iterator.foreach$(Iterator.scala:932)
at scala.collection.Iterator.foreach(Iterator.scala:932)
at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
at scala.collection.IterableLike.foreach(IterableLike.scala:70)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.TraversableLike.map(TraversableLike.scala:227)
at org.kframework.definition.Module.$anonfun$localSyntaxSentences$1(outer.scala:151)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.Module.<init>(outer.scala:150)
at org.kframework.definition.Constructors$.Module(Constructors.scala:24)
at org.kframework.definition.Constructors.Module(Constructors.scala)
at org.kframework.kore.convertors.KILtoKORE.apply(KILtoKORE.java:144)
at org.kframework.kore.convertors.KILtoKORE.apply(KILtoKORE.java:96)
at org.kframework.parser.concrete2kore.ParserUtils.lambda$loadModules$5(ParserUtils.java:221)
at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1374)
at java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:580)
at org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:221)
at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)
at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)
at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)
at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)
at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)
at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
at org.kframework.main.Main.runApplication(Main.java:414)
at org.kframework.main.Main.runApplication(Main.java:132)
at org.kframework.main.Main.main(Main.java:74)
java.lang.AssertionError: While defining module CONFIGURATION: Could not find symbol Bag
at org.kframework.definition.SymbolResolver.$anonfun$apply$1(ResolvedSymbol.scala:71)
at scala.Option.getOrElse(Option.scala:121)
at org.kframework.definition.SymbolResolver.apply(ResolvedSymbol.scala:71)
at org.kframework.definition.Module.resolve(outer.scala:113)
at org.kframework.definition.Module.$anonfun$localSyntaxSentences$2(outer.scala:152)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.Iterator.foreach$(Iterator.scala:932)
at scala.collection.Iterator.foreach(Iterator.scala:932)
at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
at scala.collection.IterableLike.foreach(IterableLike.scala:70)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.TraversableLike.map(TraversableLike.scala:227)
at org.kframework.definition.Module.$anonfun$localSyntaxSentences$1(outer.scala:151)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.Module.<init>(outer.scala:150)
at org.kframework.definition.Constructors$.Module(Constructors.scala:24)
at org.kframework.definition.Constructors.Module(Constructors.scala)
at org.kframework.kore.convertors.KILtoKORE.apply(KILtoKORE.java:144)
at org.kframework.kore.convertors.KILtoKORE.apply(KILtoKORE.java:96)
at org.kframework.parser.concrete2kore.ParserUtils.lambda$loadModules$5(ParserUtils.java:221)
at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1374)
at java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:580)
at org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:221)
at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)
at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)
at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)
at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)
at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)
at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
at org.kframework.main.Main.runApplication(Main.java:414)
at org.kframework.main.Main.runApplication(Main.java:132)
at org.kframework.main.Main.main(Main.java:74)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
Do not use Bag other than .Bag. You can say K for the function argument sort. For < controlFlows> cell, you should use the correct sort.
what is the correct sort for <controlFlows> ? My configuration is :
<controlFlows>
<control multiplicity="*">
<name> .K </name>
<body> .K </body>
</control>
</controlFlows>
I want to have a rule like:
rule @egressDefined(<control> <name> F:ControlFunctionName </name> ... </control> Rest) =>
#if F ==K egress #then true #else @egressDefined(Rest) #fi
rule @egressDefined(.Bag) => false
Um, then try without specifying the sort. Also try to pass the whole cell <controlFlows> Fls </controlFlows> into the function.
With this
rule <k> @egress => (#if @egressDefined(S) #then egress (); #else . #fi) ~> @deparseNext(L) ... </k>
<dporder> L:List </dporder>
<controlFlows> S </controlFlows>
syntax Bool ::= "@egressDefined" "(" K ")" [function]
rule @egressDefined(<control> <name> F:ControlFunctionName </name> ... </control> Rest) =>
#if F ==K egress #then true #else @egressDefined(Rest) #fi
or this
rule <k> @egress => (#if @egressDefined(<controlFlows> S </controlFlows>) #then egress (); #else . #fi) ~> @deparseNext(L) ... </k>
<dporder> L:List </dporder>
<controlFlows> S </controlFlows>
syntax Bool ::= "@egressDefined" "(" K ")" [function]
rule @egressDefined(<controlFlows> <control> <name> F:ControlFunctionName </name> ... </control> Rest </controlFlows>) =>
#if F ==K egress #then true #else @egressDefined(<controlFlows> Rest </controlFlows>) #fi
I get this error
expand macro rules : java.lang.AssertionError
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:69)
at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84)
at scala.collection.mutable.MapLike.getOrElseUpdate$(MapLike.scala:206)
at scala.collection.mutable.MapLike.getOrElseUpdate(MapLike.scala:203)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:76)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.Set$Set3.foreach(Set.scala:166)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84)
at scala.collection.mutable.MapLike.getOrElseUpdate$(MapLike.scala:206)
at scala.collection.mutable.MapLike.getOrElseUpdate(MapLike.scala:203)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:76)
at scala.Option.foreach(Option.scala:257)
at org.kframework.definition.SelectiveDefinitionTransformer.$anonfun$apply$5(transformers.scala:217)
at org.kframework.definition.SelectiveDefinitionTransformer.$anonfun$apply$5$adapted(transformers.scala:217)
at scala.collection.immutable.List.foreach(List.scala:376)
at org.kframework.definition.SelectiveDefinitionTransformer.apply(transformers.scala:217)
at org.kframework.backend.java.kore.compile.ExpandMacrosDefinitionTransformer.apply(ExpandMacrosDefinitionTransformer.java:37)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$0(JavaBackend.java:124)
at org.kframework.kompile.Kompile.compile(Kompile.java:131)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:56)
at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
at org.kframework.main.Main.runApplication(Main.java:414)
at org.kframework.main.Main.runApplication(Main.java:132)
at org.kframework.main.Main.main(Main.java:74)
Caused by: java.lang.AssertionError
at org.kframework.backend.java.kil.KCollection.upKind(KCollection.java:126)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:87)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291)
at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
at java.util.Iterator.forEachRemaining(Iterator.java:116)
at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:88)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:299)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:143)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:124)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:149)
at org.kframework.definition.ModuleTransformer$$anon$1.process(transformers.scala:18)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:137)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:135)
at org.kframework.definition.SentenceBasedModuleTransformer.$anonfun$process$1(transformers.scala:145)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:142)
at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
... 49 more
expand macro rules : java.lang.AssertionError
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:69)
at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84)
at scala.collection.mutable.MapLike.getOrElseUpdate$(MapLike.scala:206)
at scala.collection.mutable.MapLike.getOrElseUpdate(MapLike.scala:203)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:76)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.Set$Set3.foreach(Set.scala:166)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.BasicModuleTransformer.processModule(transformers.scala:124)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$3(transformers.scala:84)
at scala.collection.mutable.MapLike.getOrElseUpdate$(MapLike.scala:206)
at scala.collection.mutable.MapLike.getOrElseUpdate(MapLike.scala:203)
at org.kframework.definition.MemoizingModuleTransformer.$anonfun$apply$2(transformers.scala:84)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:84)
at org.kframework.definition.MemoizingModuleTransformer.apply(transformers.scala:76)
at scala.Option.foreach(Option.scala:257)
at org.kframework.definition.SelectiveDefinitionTransformer.$anonfun$apply$5(transformers.scala:217)
at org.kframework.definition.SelectiveDefinitionTransformer.$anonfun$apply$5$adapted(transformers.scala:217)
at scala.collection.immutable.List.foreach(List.scala:376)
at org.kframework.definition.SelectiveDefinitionTransformer.apply(transformers.scala:217)
at org.kframework.backend.java.kore.compile.ExpandMacrosDefinitionTransformer.apply(ExpandMacrosDefinitionTransformer.java:37)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at scala.Function1.$anonfun$andThen$1(Function1.scala:52)
at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$0(JavaBackend.java:124)
at org.kframework.kompile.Kompile.compile(Kompile.java:131)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:56)
at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
at org.kframework.main.Main.runApplication(Main.java:414)
at org.kframework.main.Main.runApplication(Main.java:132)
at org.kframework.main.Main.main(Main.java:74)
Caused by: java.lang.AssertionError
at org.kframework.backend.java.kil.KCollection.upKind(KCollection.java:126)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:87)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291)
at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
at java.util.Iterator.forEachRemaining(Iterator.java:116)
at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KList(KOREtoBackendKIL.java:88)
at org.kframework.backend.java.compile.KOREtoBackendKIL.KApply1(KOREtoBackendKIL.java:117)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:291)
at org.kframework.backend.java.compile.KOREtoBackendKIL.convert(KOREtoBackendKIL.java:299)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:143)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:124)
at org.kframework.backend.java.kore.compile.ExpandMacros.expand(ExpandMacros.java:149)
at org.kframework.definition.ModuleTransformer$$anon$1.process(transformers.scala:18)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:137)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:135)
at org.kframework.definition.SentenceBasedModuleTransformer.$anonfun$process$1(transformers.scala:145)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
at scala.collection.SetLike.map$(SetLike.scala:101)
at scala.collection.SetLike.map(SetLike.scala:101)
at org.kframework.definition.SentenceBasedModuleTransformer.process(transformers.scala:142)
at org.kframework.definition.BasicModuleTransformer.$anonfun$processModule$1(transformers.scala:124)
at org.kframework.definition.ModuleTransformer.wrapExceptions(transformers.scala:66)
... 49 more
[Error] Internal: Uncaught exception thrown of type ModuleTransformerException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
I looked at kool, I see something like this there
// the syntax declarations below are required because the sorts are
// referenced directly by a production and, because of the way KIL to KORE
// is implemented, the configuration syntax is not available yet
// should simply work once KIL is removed completely
// check other definitions for this hack as well
syntax EnvCell
syntax ControlCell
syntax EnvStackCell
syntax CrntObjCellFragment
But I don't know what it means and what I should do for my semantics
We discussed this at the time. The javacc parser generates KIL data structures which are converted directly into KORE modules, but with the bubbles not parsed yet. The configuration is still a bubble at this stage so its information, including the sorts generated according to the methodology here, is not available at this time. If there are productions (not rules, it works for rules because they are bubbles also) that reference something in the configuration, that information would not be available when the KIL module is first converted into KORE so the KORE module fails consistency checks. To make the consistency checks pass, we need to explicitly define the sorts we need.
As I see it, better way for this is to leave the KORE module at the meta-level until all the information for it to pass the consistency checks is available. The implementation based on the new parser, the one @lucaspena and @ehildenb are working on, should solve this by first parsing to the meta-level, then downing. But it can still be tricky as the non-configuration productions are required to parse the configuration. We could solve this by filtering out any productions for which we do not have the referenced sorts and hope for the best. It's a chicken and egg problem.
