Inner Parser: Scanner Error: Numeric Argument to substrString

Question

I'm working on lesson 10 of the K introduction. Can't figure out an error I'm getting. I have the file lesson-10.k with the following contents (simplified for now to demonstrate the error):

module LESSON-10
  imports STRING

  syntax String ::= nonsentence(String) [function]
  rule nonsentence(S) => substrString(S, 0, 5)
  rule nonsentence(_) => " ." [owise]
endmodule

When I try to compile it as follows:

kompile lesson-10.k

I get this error - compiler seems to be flagging the argument 0 to substrString as unexpected:

[Error] Inner Parser: Scanner error: unexpected character sequence '0'.
        Source(/home/bhandalc/k/lesson-10/lesson-10.k)
        Location(5,42,5,43)
[Error] Compiler: Had 1 parsing errors.

I'm working on WSL with Ubuntu focal.

Answer 1

...Ah I got it. I wasn't importing INT so it didn't know what 0 was. Fixed code:

module LESSON-10
  imports INT
  imports STRING

  syntax String ::= nonsentence(String) [function]
  rule nonsentence(S) => substrString(S, 0, 5)
  rule nonsentence(_) => " ." [owise]
endmodule

---

I was initially still a little bit confused by this because I thought "Surely STRING needs INT to define the substring function in the first place?"

Then I saw this in the K User Manual:

Imports can be public or private. By default, they are public, which means that all the imported syntax can be used by any module that imports the module doing the import. However, you can explicitly override the visibility of the import with the public or private keyword immediately prior to the module name. A module imported privately does not export its syntax to modules that import the module doing the import.

And indeed, the INT import is private in STRING-COMMON:

module STRING-COMMON
  imports STRING-SYNTAX
  imports private INT
  imports private FLOAT-SYNTAX
  imports private K-EQUAL
  imports private BOOL

...And STRING itself is built atop STRING-COMMON:

module STRING
  imports STRING-COMMON

So importing STRING won't just bring in the INT module for you. You need to do it yourself.