Separate modules for parsing and semantics

This page is obsolete and should be removed soon. See Module System instead. Make sure we add a link to parsers.pptx somewhere on Module System.

mostly copied from Grigore's email -- will eventually become an in-depth description of using separate modules for parsing and semantics

As we move to more and more tricky and complex languages, if we want people to use the K parser to parse programs in their languages (instead of external parsers), then we have to give them full freedom in how they write their grammars for parsing, without constraints imposed by what can be nicely handled semantically. For example, it is common to parse comma-separated expression lists with a grammar as follows:

module LANG-COMMON-SYNTAX
   ...  // syntax common to both parsing and semantics
   syntax Exp ::= ...
endmodule

module LANG-SYNTAX-PARSING
   import LANG-COMMON-SYNTAX
   ...
   syntax Temp ::= Exp | Temp "," Exp
   syntax Exps ::= "" | Temp
   ...
endmodule

Unfortunately, that is a fact of life. More efficient parsers can be generated when people focus on defining the syntax with parsing, instead of semantics, in mind. For semantics, we obviously want something like this:

module LANG-SYNTAX-SEMANTICS
   import LANG-COMMON-SYNTAX
   ...
   syntax Exps ::= ".Exps" | Exp | Exps "," Exps  [assoc, id(".Exps")]
   ...
endmodule

Having #rewrite we can relatively nicely reconcile the two as follows (see also the message about tagging symbols with their defining modules):

module TRANSLATE
   import LANG-SYNTAX-PARSING
   import LANG-SYNTAX-SEMANTICS
   syntax LANG-SYNATX=SEMANTICS.Exps ::= translate(LANG-SYNTAX-PARSING.Exps)
   syntax LANG-SYNATX=SEMANTICS.Exps ::= translate(LANG-SYNTAX-PARSING.Temp)
   rule translate(``::LANG-SYNTAX-PARSING.Exps) => .Exps
   rule translate(T:Temp, E) => translate(T),E
endmodule

module LANG-SEMANTICS
   import LANGUAGE-SYNTAX-SEMANTICS
   configuration ... <k> #rewrite(TRANSLATE, `translate(#parse(LANG-SNTAX-PARSING, $PGM))`) </k>
   ...
endmodule

We can probably even avoid defining the "translate" operations and replace them with casts, but that is not the point here.

Added by Radu: Here is a power point presentation that Grigore wrote in September '14 about how to create bubbles and parse them after wards. It offers a high level overview of how the K tool should parse programs and rules inside a definition parsers.pptx