[Bug] [kompile] - Implicit import of the module BOOL

[amelieled]

K Version

$ kompile --version

K version: 5.2.110
Build date: Mon Mar 21 00:10:55 CET 2022

Description

The command kompile lazy.k returns the error:

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(NoSuchElementException: key not found: _andBool_)

Input Files

The file lazy.k is:

module LAZY-SYNTAX
    // imports BOOL
    syntax MyBool ::= "mytrue" | "myfalse"
    syntax BExp ::= MyBool | BExp "myand" BExp [strict(1)]

    syntax KResult ::= MyBool

endmodule

module LAZY
    imports LAZY-SYNTAX

    rule mytrue  myand B2 => B2
    rule myfalse myand _  => myfalse

endmodule

Expected Behavior

The command kompile lazy.k should return nothing.

To fix the problem, you can uncomment the second line (imports BOOL).

[Baltoli]

The problem here is that the strictness attribute desugars to rules that look something like this:

rule `<generatedTop>`(`<k>`(``HOLE~>`#freezer_myand__LAZY-SYNTAX_BExp_BExp_BExp0_`(K1)=>`_myand__LAZY-SYNTAX_BExp_BExp_BExp`(HOLE,K1)``~>_DotVar1),_DotVar0) requires `_andBool_`(#token("true","Bool"),isKResult(HOLE)) ensures #token("true","Bool") [UNIQUE_ID(64c81fd8b81584b85277e600b482ee43e85fd098c829b691c067c2ce8d2842a1), cool, cool-like, org.kframework.attributes.Location(Location(4,30,4,59)), org.kframework.attributes.Source(Source(/home/bruce/code/k/lazy.k)), strict(1)]

We should either implicitly import BOOL into modules that use strictness annotations as @amelieled suggests, or issue an error to the user that they need to supply their own definition of _andBool_ etc.

[radumereuta]

K doesn't work if BOOL is not imported somewhere.
It works if it's imported in the main syntax module or the main semantics module.
One thing to avoid is to taint the program syntax module.