Importing a set of sentences from a module

[dwightguth]

We want to improve the module signatures feature by allowing the type of "import foo from BAR` syntax present in most other import systems. Here are three possible syntaxes for consideration:

1. Sentence label

module FOO
  syntax [foo]: Foo ::= foo(Foo) 
  syntax [bar]: Foo ::= foo(Bar)
endmodule

module BAR
  imports FOO.foo
  imports FOO.foo as bar(_)
endmodule

Potential problems: you can't import something without help from someone who can modify the module being imported from. You also have trouble with sentence labels and pipes mixing.

2. Sentence tag

module FOO
  syntax Foo ::= foo(Foo) [tag(foo)]
  syntax Foo ::= foo(Bar) [tag(bar)]
endmodule

module BAR
  imports FOO.foo
  imports FOO.foo as bar(_)
endmodule

Basically the same but uses the tag attribute instead of the sentence label. Allows multiple sentences to be given the same tag, which could introduce complexity when it comes to renaming.

3. Explicit syntax

module FOO
  syntax Foo ::= foo(Foo)
  syntax Foo ::= foo(Bar)
endmodule

module BAR
  imports 
    syntax Foo ::= foo(Foo)
    syntax Bar ::= foo(Bar) => bar(_)
  from FOO
endmodule

Requires you to basically redeclare what you import, but is the most flexible.

[nishantjr]

Use cases

Allow mixing program syntax with semantics code

K definitions are routinely split into modules for program syntax and semantics.
For readability, it may be nicer program grammar close to the semantic rules that define them.
While For simpler semantics this may be achieved through the public and private attributes,
this does not work with module hierarchies with more than two levels (such as any semantics that uses proofs).

module IMP-SYNTAX
  imports IMP.program
endmodule

module IMP
  syntax [program] AExp  ::= Int | Id | "(" AExp ")" [bracket]

  syntax [program] AExp ::= AExp "/" AExp [left, strict]
  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0

  syntax AExp ::= "#undefined"
  rule I1 / I2 => #undefined   // #undefined may not be used in program syntax
                               // but may be used in proofs etc.

  syntax [program] AExp ::= AExp "+" AExp [left, strict]
  rule I1 + I2 => I1 +Int I2

  syntax [program] AExp ::=  "-" Int [format(%1%2)]
  rule - I1 => 0 -Int I1
endmodule

Alternate parsing rules for programs vs semantic rules.

Some productions, such as the empty production and tokens are needed in the program syntax
but cause trouble in the main semantic modules.

This can be worked around my defining a module heirarch that separates program
syntax from rule syntax.
However, this becomes quite complex and hard to read when a non-trivial module heirarchy is needed.
For example, a snipet from the BOogie semantics looks like this:

module NOTHING-COMMON-SYNTAX
    syntax Nothing
endmodule

module NOTHING-PROGRAM-SYNTAX
    imports NOTHING-COMMON-SYNTAX
    syntax Nothing ::= "" [klabel(Nothing), symbol]
endmodule

module NOTHING-RULE-SYNTAX
    imports NOTHING-COMMON-SYNTAX
    syntax Nothing ::= ".Nothing" [klabel(Nothing), symbol]
endmodule

module BOOGIE-COMMON-SYNTAX
    syntax Id
    syntax Ids ::= List{Id, ","}
    syntax ConstantDecl ::= "const" OptionalUnique Ids ";"
    syntax OptionalUnique ::= Nothing | "unique"
endmodule

module BOOGIE-PROGRAM-SYNTAX // --syntax-module
    imports NOTHING-PROGRAM-SYNTAX
    imports BOOGIE-COMMON-SYNTAX
    syntax Id ::= r"(?<![A-Za-z0-9\\_])[A-Za-z\\_]['A-Za-z0-9\\_#]*" [prec(1), token]  
endmodule

module BOOGIE-RULE-SYNTAX
    imports NOTHING-RULE-SYNTAX
    imports BOOGIE-COMMON-SYNTAX
endmodule

This could be replaced with:

module NOTHING
    syntax Nothing
    syntax [rules]   Nothing ::= ".Nothing" [klabel(Nothing), symbol]
    syntax [program] Nothing ::= "" [klabel(Nothing)]
endmodule

module BOOGIE-SYNTAX
    syntax [program] Id ::= r"(?<![A-Za-z0-9\\_])[A-Za-z\\_]['A-Za-z0-9\\_#]*" [prec(1), token]  
    syntax Ids ::= List{Id, ","}
    syntax ConstantDecl ::= "const" OptionalUnique Ids ";"
    syntax OptionalUnique ::= Nothing | "unique"
endmodule

module BOOGIE-PROGRAM-SYNTAX // --syntax-module
    imports BOOGIE-SYNTAX.program
endmodule

module BOOGIE-RULE-SYNTAX
    imports BOOGIE-SYNTAX.rules
endmodule

Note that in theory, this could be achieved by renaming.
However, that means that we need to repeat the rename each time the module is imported.
In this case, where only one production is hidden it may not be a big deal.
In extreme cases, such as in k-in-k things got quite gnarly.
In addition, I feel that this way is more readable because the intension of the programmer is explicit.
Another case where this feature may have been helpful is defining the Micheline syntax
although, in that case we would also have needed the ability to hide/collapse subsorts.

[ehildenb]

Discussion:

• Most people like suggestion 2 or 3.
• Problem with suggestion 2 -> requires upstream projects (eg. K -> KEVM -> ERC20) to tag any productions we want to rename. This could maybe be fixed by allowing either the tag or the klabel to refer to it. This would also make it harder to import a single overload within a set of overloads.
• Problem with suggestion 3 -> requires repeating yourself to list the production.

We should also allow mis-fix syntax (but can't change sorts or order of non-terminals):

module FOO
  syntax Foo ::= foo(Foo)
  syntax Foo ::= foo(Bar, Foo)
endmodule

module BAR
  imports 
    syntax Foo ::= foo(Foo)
    syntax Bar ::= foo(Bar, Foo) => _ "barOp" _
  from FOO
endmodule

[nishantjr]

module BAR                                                                                                              
    imports FOO hiding FOO_foo                                                                                          
    syntax Foo ::= foo(Foo) [overloading(Foo_foo)]                                                                      
endmodule

[ehildenb]

We'll use approach 2, but allow klabel-mentioning for referring to productions (to avoid the upstreaming issue).

Something like:

  imports MODULE.(TAG|KLABEL) [as PRODUCTION_ITEM*]
  imports MODULE [with (TAG|KLABEL) [as PRODUCTION_ITEM*]]*

But where PRODUCTION_ITEM is limited to terminals and underbar non-terminals. If the TAG|KLABEL does not refer to a unique production, it's an error (if you use an as PRODUCTION_ITEM* clause).

The as PRODUCTION_ITEM* clause is optional, only if you want to rename. Otherwise you're just importing only some specific syntax from the MODULE.

The with ... clause allows you to import the entire module, but rename just a small list of things. The one without the with ... clause defaults to not importing things.

[nishantjr]

We should also be clear both in the documentation, both for this feature and for private syntax, that this only affects the parsing and not rules.