-
Notifications
You must be signed in to change notification settings - Fork 0
Kast and Kore
Design proposal for standardizing the basic representation of KIL for programs and definitions
#Introduction
The objective of this design proposal is to separate concerns even further in the design and implementation of the K tool.
This proposal is about the syntax of core K, which for simplicity I'm going to call Kore. Recall that K in its full generality requires a two-phase parser: one parsing the syntax declarations and generating a parser for the rules (or contexts, macros, etc.), and the other parsing the rules using the parser generated in phase one. Kore is a fragment of K meant to be very easy to parse, eliminating the need for a two-phase parser. From a user perspective, the difference between K and Kore is that instead of writing terms which need a concrete-syntax parser to parse, such as A + B, one writes terms using the KAST syntax, such as '_+_(A,B).
The idea is that Kore should be nothing but a textual reflection of the KIL of a K definition, the same way the KAST of a program is nothing but a textual reflection of the KIL of that program. We are going to have a trivial "loader" of a K definition in Kore format into KIL data-structures, which in principle is a parser, but a very simple one, infinitely simpler than the current K parser that Radu is working on.
There are LOTS of advantages for doing this. I'll only mention the beautiful separation of concerns that we will achieve, where the complex K parser is completely separated out from the kompile tool, so both of them can then be designed and improved in isolation. Further, I hope that the syntax of Kore will be simple enough that we will not need to change it as we change the support for parsing in K, so middle-end and back-end developers will not depend on other crazy syntactic tricks that we may apply to the front-end (e.g., sort inferencers, syntactic conventions for builtins like using X|->I in cells, etc.).
Whatever I say next can and will be obviously changed/improved, so feel free to comment or fight for your point. Actually, I really hope that this message will start you on to say all the things that you wanted to say about this topic. Keep in mind, though, that we want a fragment of K here, which should be trivial to parse.
#GeneriK
Let us start with the generic syntax of K, that is, the K syntax for defining language syntax and semantics which is independent upon the particular language that is being defined. For simplicity, we refer to this syntax as GeneriK. At this level there is only one generic sort for all syntax, K, which has no constructs. A parser for GeneriK would put all the K terms into "bubbles":
syntax String ::= usual double-quoted strings
syntax NAME ::= any sequences of characters; each context may further restrict them (e.g., variables and sorts start with capital letter, etc.)
syntax Comment ::= usual comments (/* multiline */ and // one line)
syntax K // GeneriK does not care about the concrete or abstract syntax; all syntactic terms are parsed as K "bubbles" at this stage
syntax Definition ::= List{Module | Comment}{""} // maybe this notation should be used for non-empty lists?
syntax Module ::= "module" NAME ModuleBody "endmodule"
syntax ModuleBody ::= List{Sentence | Comment}{""}{""}
syntax Sentence ::= Import | Configuration | Syntax | Context | Rule
syntax Import ::= "import" NAME
syntax Configuration ::= "configuration" K OptionalAttributes // cells and configurations are represented as K terms, too
syntax Syntax ::= "syntax" Sort OptionalAttributes // sort declarations, possibly with attributes
| "syntax" Sort "::=" List{Production}{"|"}
syntax Sort ::= NAME
syntax Production ::= List{String | Sort}{""} OptionalAttributes
syntax Context ::= "context" K OptionalAttributes
syntax Rule ::= "rule" K OptionalAttributes
syntax OptionalAttributes ::= "" | "[" Attributes "]"
syntax Attributes ::= List{Attribute}{","}{""}
syntax Attribute ::= NAME OptionalNAMES
syntax OptionalNAMES ::= "" | "(" NAMES ")"
syntax NAMES ::= List{NAME}{","}
The K terms marked as "bubbles" by the GeneriK parser need to be further parsed with specialized parsers (e.g., the Kore parser, or the parser for Full K, etc.; see next). Note that each such K term bubble above appears in a construct that also allows optional attributes. One of those attributes can, for example, state the specific parser to be used to parse the corresponding K term bubble (in case the default one, probably the one for Full K, generates ambiguities).
Important note: The GeneriK parser should be as simple and efficient as possible. It should not attempts to parse any K terms at all and it should give very nice error messages. Any other subsequent parsers for K will only be concerned with parsing the K term bubbles (possibly in parallel).
#Kore
Kore adds to GeneriK a more specific syntax for K terms, but one which is still very easy to parse (without requiring 2 phase parsing). Specifically, it adds to GeneriK the following: KAST syntax; support for variables, sort memberships and cells; and the rewrite relation => and the HOLE.
##KAST
KAST is meant to represent any ground K terms (including ones corresponding to programs in AST format, obtained by removing the ~> construct):
syntax K ::= List{KItem}{"~>"}{".K"} // generic
syntax KItem ::= KToken | KLabel "(" KList ")" // generic
syntax KList ::= List{K}{","}{".KList"} // generic
syntax KToken ::= "#" String // tokens start with # and are immediately (no space) followed by a string; e.g., #"abc", #"735", etc.
syntax KLabel ::= NAME // ones starting with single-quote are generated automatically from productions
##Variables and Sort Memberships
Adding support for sorting/casting and variables:
syntax Variable ::= NAME // possibly restricted to start with capital letter
syntax K ::= Variable
| K ":" Sort // sorting arbitrary K terms
| "(" K ")" [bracket]
syntax KItem ::= Variable ":" "KItem" // should have priority over the above
syntax KList ::= Variable ":" "KList"
syntax KToken ::= Variable ":" "KToken"
syntax KLabel ::= Variable ":" "KLabel"
##Cells and Configurations
In the long run we want cells and configurations to be embedded into K the same way we decided to embed the builtins (integers, maps, etc.). Probably <k> T </k> will become something of the form '<k>_</k>(T). However, for now we decided to make a notational exception and allow cells to be written in an XML-ish notation in Kore (this is orthogonal to how cells are represented in KIL):
syntax K ::= Cells
syntax Cells ::= List{Cell}{""}
syntax Cell ::= "<" NAME OptionalTags ">" K "</" NAME ">" // the two NAME should be the same
syntax OptionalTags ::= List{NAME "=" String}{""}{""}
##Rewriting and HOLE
syntax K ::= KList "=>" KList // should be greedy
syntax K ::= "HOLE" // further restricted to only appear in certain contexts
#Example: IMP in Kore
Below is IMP defined in the Kore language above, including all the builtins that it needs.
###IMP Syntax and Builtins
We can define the syntax either using sorts and productions, which are easier to read and hold more information that may be useful in some backends, or using only KLabels, which is more minimal but also loses sort information.
Here is the syntax using sorts and productions. This is almost identical to the IMP syntax in full K, except for purely parsing-related features, such as bracket productions, operation priorities, prefer and avoid attributes, etc.:
module BUILTINS
sort "Int" [builtin(Integer)]
sort "Bool" [builtin(Boolean)]
sort "Id" [builtin(Identifier)]
syntax Int ::= Int "/Int" Int [builtin(IntegerDivision)]
| Int "+Int" Int [builtin(IntegerAddition)]
syntax Bool ::= Int "<=Int" Int [builtin(IntegerLeq)]
| Int "=/=Int" Int [builtin(IntegerNeq)]
| "notBool" Bool [builtin(BoolNot)]
syntax Map ::= ".Map" [builtin(MapEmpty)]
| lookup(Map) [builtin(MapLookup)]
| update(Map,K,K) [builtin(MapUpdate)]
| addBinding(Map,K,K) [builtin(MapAddBinding)]
syntax Bool ::= K "in" Map [builtin(MapMembership)]
syntax K ::= keys(Map) [builtin(MapGetKeys)]
endmodule
module IMP-SYNTAX
imports BUILTINS
syntax AExp ::= Int | Id
| AExp "/" AExp [strict]
| AExp "+" AExp [strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| BExp "&&" BExp [strict(1)]
syntax Block ::= "{" "}"
| "{" Stmt "}"
syntax Stmt ::= Block
| Id "=" AExp ";" [strict(2)]
| "if" "(" BExp ")" Block "else" Block [strict(1)]
| "while" "(" BExp ")" Block
| Stmt Stmt
syntax Pgm ::= "int" Ids ";" Stmt
syntax Ids ::= List{Id}{","}{".Ids"}
endmodule
Here is the KLabel alternative of the syntax above, which may be prefered in some cases:
module BUILTINS
syntax KLabel ::= "Int" [builtin(Integer)] // can be added automatically, from 'sort "Int" [builtin(Integer)]'
syntax KLabel ::= "Bool" [builtin(Boolean)]
syntax KLabel ::= "Id" [builtin(Identifier)]
syntax KLabel ::= "'_/Int_" [builtin(IntegerDivision)]
| "'_+Int_" [builtin(IntegerAddition)]
| "'_<=Int_" [builtin(IntegerLeq)]
| "'_=/=Int_" [builtin(IntegerNeq)]
| "'notBool_" [builtin(BoolNot)]
| "'.Map" [builtin(MapEmpty)]
| "'lookup_" [builtin(MapLookup)]
| "'update_" [builtin(MapUpdate)]
| "'addBinding_" [builtin(MapAddBinding)]
| "'_in_" [builtin(MapMembership)]
| "'keys_" [builtin(MapGetKeys)]
endmodule
module IMP-SYNTAX
imports BUILTINS
syntax KLabel ::= "'_/_" [strict]
| "'_+_" [strict]
| "'_<=_" [seqstrict]
| "'!_" [strict]
| "'_&&_" [strict(1)]
| "'{}"
| "'{_}"
| "'_=_;" [strict(2)]
| "'if`(_`)then_" [strict(1)]
| "'while`(_`)_"
| "'__"
| "'int_;_"
| "'_,_"
| "'.Ids"
endmodule
###IMP Semantics
Below I'm allowing unsorted variables, with the simple and locally resolved semantics that they have the sort K.
module IMP
imports IMP-SYNTAX
rule isKResult(I:Int) => Bool(#"true")
rule isKResult(B:Bool) => Bool(#"true")
configuration <T>
<k> $PGM:K </k>
<state> '.Map(.KList) </state>
</T>
rule <k> X:Id => 'lookup(Sigma,X:Id) ...</k> <state> Sigma </state>
rule '_/_(I1:Int,I2:Int) => '_/Int_(I1:Int,I2:Int) when '_=/=Int_(I2:Int,Int(#"0"))
rule '_+_(I1:Int,I2:Int) => '_+_(I1:Int,I2:Int)
rule '_<=_(I1:Int,I2:Int) => '_<=_(I1:Int,I2:Int)
rule '!_(T:Bool) => 'notBool_(T:Bool)
rule '_&&_(Bool(#"true"),B) => B
rule '_&&_(Bool(#"false"),_) => Bool(#"false")
rule '{}(.KList) => .K [structural]
rule '{_}(S) => S [structural]
rule <k> '_=_;(X:Id,I:Int) => .K ...</k> <state> Sigma => 'update(Sigma,X:Id,I:Int) </state>
rule '__(S1,S2) => S1 ~> S2 [structural]
rule 'if`(_`)_else_(Bool(#"true"),S,_) => S
rule 'if`(_`)_else_(Bool(#"false"),Bool),_,S) => S
rule 'while`(_`)_(B,S) => 'if`(_`)_else_(B, '{_}('__(S, 'while`(_`)_(B,S))), '{}(.KList)) [structural]
rule <k> 'int_;_(('_,_(X:Id, Xs) => Xs), _) </k>
<state> Sigma => 'addBinding(Sigma, X:Id, Int(#"0")) </state>
when 'notBool('_in_(X:Id, 'keys(Sigma)))
rule 'int_;_('.Ids(.KList),S) => S [structural]
endmodule
##Kuestions
###Q1 Do we really need to keep strings in tokens? That is, why not just #token(735, Int) instead of #token("735", "Int")? Of course, the projections will still give us strings. For example, getSort(#token(735,Int)) will evaluate to "Int". So should we replace
syntax KToken ::= #token(String,String)
with
syntax KToken ::= #token(NAME,NAME)
?
Answer: Problem solved. I did what Dwight suggested, that is, added KTokenSort, which eliminates the quotes around the sort name only. But that is better actually that what i wanted. Besides, it also gives a nice way to associate builtins to tokens.
###Q2: Do we need a more elaborate syntax for declaring configurations and cells, or we can limit ourselves to KItems? How about modularity, where we want to name and reuse configuration fragments?
Answer: Partially solved. I only added support for monolithic configurations. We still have to discuss and design the modular configurations.
###Q3: Should we keep all the syntax declarations in Kore like in K, so that we can use the priority, prefer, bracket, etc., information for unparsing?
###Q4: How about rules between KLabels, for example:
syntax KLabel ::= "foo" | "bar" | "baz"
rule foo => bar
rule Context[(bar => baz)(kl)] // kl is some KList term, and Context some K holed context
Answer: Complete/cChange the rules to apply between K terms:
rule foo(KL:KList) => bar(KL)
rule Context[bar(kl) => baz(kl)]
###Q5: KORE should support anything we want to do in Full K, such as, for example, operations of the form
syntax KLabel ::= foo(KLabel)
rule Context[foo(L:KLabel)(KL:KList)] // Context is any context with hole of sort K
syntax KLabel ::= bar(KList)
rule Context[bar(KL1:KList)(KL2:KList)]
syntax KList ::= rev(KList)
rule rev(K,KL) => rev(KL),K
rule rev(.KList) => .KList
How can we encode these in KORE?
Answer: The same basic principle: we add the various operations as KLabels, and then we add corresponding rules between corresponding KList terms. For some of them we also need to get some special/additional labels involved. For the first two, see also the previous question.
syntax KLabel ::= "foo"
rule Context[foo(L:KLabel(KL:KList))]
syntax KLabel ::= "bar"
rule Context[bar($klist(KL1:KList),KL2:KList)]
syntax KLabel ::= "rev"
rule rev($klist(K,KL)) => $klist(KL',K) requires $klist(KL') =K rev(KL)
rule rev($klist(.KList)) => $klist(.KList)
where $klist is a special KLabel (Andrei A suggests that users should not even be allowed to match against it with L(KL) := $klist(KL')).
For the reverse example, note that we cannot simply make rev a KLabel and nothing else, because then we have strange situations like this one that Traian noticed: rev(rev(1,2)) => rev(1,2) => 2,1. The trick with $klist achieves the desired innermost evaluation strategy.