From ba0918ffdacd6abc8457e70e96ffd10fcdf0060d Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Fri, 28 Jun 2019 11:31:02 +0300 Subject: [PATCH 01/20] Started to parse configurations Run into some errors and ambiguities. --- build | 5 +- src/command-line.md | 19 +++++++ src/config-inner.md | 23 ++++++++ src/ekore.md | 6 +- src/inner.md | 122 ++++++++++++++++++++++++++++++++++++++++ src/rule-inner.md | 45 +++++++++++++++ t/config/config.k | 8 +++ t/config/expected.ekore | 38 +++++++++++++ 8 files changed, 262 insertions(+), 4 deletions(-) create mode 100644 src/config-inner.md create mode 100644 src/inner.md create mode 100644 src/rule-inner.md create mode 100644 t/config/config.k create mode 100644 t/config/expected.ekore diff --git a/build b/build index e77e786..9b9954f 100755 --- a/build +++ b/build @@ -53,10 +53,13 @@ ekore = 'src/ekore.md' kore = 'src/kore.md' parser = 'src/parser-util.md' file = 'src/file-util.md' +inner = 'src/inner.md' +configinner = 'src/config-inner.md' +ruleinner = 'src/rule-inner.md' kink = proj.definition( backend = 'ocaml' , main = 'src/kink.md' - , other = [kore, ekore, parser, file, 'src/command-line.md', k_light] + , other = [kore, ekore, parser, file, 'src/command-line.md', k_light, inner, configinner, ruleinner] , directory = proj.builddir('kink') , flags = '--syntax-module KINK-SYNTAX' , alias = 'kink' diff --git a/src/command-line.md b/src/command-line.md index f20ee51..1a79e31 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -1,4 +1,6 @@ ```k +require "file-util.k" + module COMMAND-LINE-SYNTAX imports STRING-SYNTAX syntax KItem ::= "#parseCommandLine" "(" CommandLine "," Pgm ")" @@ -8,6 +10,7 @@ module COMMAND-LINE-SYNTAX syntax String ::= token2String(KItem) [function, functional, hook(STRING.token2string)] syntax CommandLine ::= "kompile" | "kast" Path + | "frontend-to-ekore" | "ekore-to-kore" endmodule ``` @@ -28,6 +31,7 @@ module COMMAND-LINE imports PRODUCTIONS-TO-SYMBOL-DECLARATIONS imports TRANSLATE-FUNCTION-RULES imports REMOVE-FRONTEND-DECLARATIONS + imports FILE-UTIL ``` Command line options @@ -53,6 +57,21 @@ the `PATH`: ``` +`frontend-to-ekore`: gets a full K definition and: + + - parses into bubbles + - sanity checks + - parse config + - parse rules + +```k + rule #parseCommandLine(frontend-to-ekore, PGM) + => PGM ~> #frontendPipeline + ... + + +``` + `ekore-to-kore`: Convert the EKore definition specified in `$PGM` to kore syntax. Frontend declarations that are not captured completely by the kore definition are kept. diff --git a/src/config-inner.md b/src/config-inner.md new file mode 100644 index 0000000..9e88377 --- /dev/null +++ b/src/config-inner.md @@ -0,0 +1,23 @@ +```k +//require "inner.k" + +module CONFIG-CELLS + imports KCELLS + imports RULE-LISTS + syntax CellName ::= r"[a-zA-Z][A-Za-z0-9'_]*" [token] + + syntax Cell ::= "<" CellName CellProperties ">" K "" [klabel(configCell)] + syntax Cell ::= "<" CellName "/>" [klabel(externalCell)] + + syntax CellProperties ::= CellProperty CellProperties [klabel(cellPropertyList)] + | "" [klabel(cellPropertyListTerminator)] + syntax CellProperty ::= CellName "=" KString [klabel(cellProperty)] + +endmodule + +module CONFIG-INNER // main parsing module for configuration, start symbol: K + imports K-TERM + imports CONFIG-CELLS + imports DEFAULT-LAYOUT +endmodule +``` diff --git a/src/ekore.md b/src/ekore.md index 0992a02..da8d0a0 100644 --- a/src/ekore.md +++ b/src/ekore.md @@ -239,7 +239,7 @@ module ATTRIBUTES-COMMON syntax TagContent ::= UpperName | LowerName | Numbers | EKoreKString syntax TagContents - syntax KEY ::= LowerName + syntax KEY ::= LowerName [token] endmodule @@ -350,9 +350,9 @@ module K-DEFINITION-ABSTRACT imports ATTRIBUTES-ABSTRACT syntax KImportList ::= ".KImportList" [klabel(emptyKImportList)] - | KImportList KImport [klabel(kImportList), format(%1%2%n%3)] + | KImportList KImport [klabel(kImportList), format(%1%2%n)] syntax KRequireList ::= ".KRequireList" [klabel(emptyKRequireList)] - | KRequireList KRequire [klabel(KRequireList), format(%1%2%n%3)] + | KRequireList KRequire [klabel(KRequireList), format(%1%2%n)] syntax KDefinition ::= kDefinition(KRequireList, Modules) [klabel(kDefinition), format(%3%n%n%5)] syntax Definition ::= KDefinition diff --git a/src/inner.md b/src/inner.md new file mode 100644 index 0000000..ac70efb --- /dev/null +++ b/src/inner.md @@ -0,0 +1,122 @@ +Predefined sorts and base K syntax + +```k +// Module defining only the sorts K and KString, useful for modularity +module SORT-K + syntax K +endmodule + +module BASIC-K + imports SORT-K + syntax KItem + syntax KConfigVar [token] +endmodule + +module KSTRING + syntax KString ::= r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token] + // optionally qualified strings, like in Scala "abc", i"abc", r"a*bc", etc. +endmodule + +module SORT-KBOTT + imports SORT-K + syntax KBott +endmodule + +module KAST + imports BASIC-K + imports SORT-KBOTT + imports KSTRING + + syntax KBott ::= "#token" "(" KString "," KString ")" [klabel(kToken)] + | "#klabel" "(" KLabel ")" [klabel(wrappedKLabel)] + | KLabel "(" KList ")" [klabel(kApply)] + + syntax KLabel ::= r"`(\\\\`|\\\\\\\\|[^`\\\\\n\r])+`" [token] + | r"(?" K [klabel(kSequence), left, assoc, unit(emptyK)] + | "(" K ")" [bracket] +endmodule + +// To be used when parsing/pretty-printing symbolic configurations +module KSEQ-SYMBOLIC + imports KSEQ + + syntax KVariable ::= r"(?Sort" + // this is part of the mechanism that allows concrete user syntax in K +endmodule + +module AUTO-FOLLOW + // if this module is imported, the parser automatically + // generates a follow restriction for every terminal which is a prefix + // of another terminal. This is useful to prevent ambiguities such as: + // syntax K ::= "a" + // syntax K ::= "b" + // syntax K ::= "ab" + // syntax K ::= K K + // #parse("ab", "K") + // In the above example, the terminal "a" is not allowed to be followed by a "b" + // because it would turn the terminal into the terminal "ab". +endmodule + +module RULE-LISTS + // if this module is imported, the parser automatically + // adds the subsort production to the parsing module only: + // Es ::= E [userList("*")] + +endmodule + +module DEFAULT-LAYOUT + syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] +endmodule + +// To be used to parse terms in full K +module K-TERM + imports KSEQ-SYMBOLIC + imports K-SORT-LATTICE + imports AUTO-CASTS + imports AUTO-FOLLOW +endmodule +``` diff --git a/src/rule-inner.md b/src/rule-inner.md new file mode 100644 index 0000000..fe8cb6e --- /dev/null +++ b/src/rule-inner.md @@ -0,0 +1,45 @@ + +```k +require "inner.k" + + +module RULE-CELLS + imports KCELLS + imports RULE-LISTS + // if this module is imported, the parser automatically + // generates, for all productions that have the attribute 'cell' or 'maincell', + // a production like below: + //syntax Cell ::= "" #OptionalDots K #OptionalDots "" [klabel()] + + syntax #OptionalDots ::= "..." [klabel(#dots)] + | "" [klabel(#noDots)] +endmodule + +module REQUIRES-ENSURES + imports BASIC-K + + syntax #RuleBody ::= K + + syntax #RuleContent ::= #RuleBody [klabel("#ruleNoConditions")] + | #RuleBody "requires" K [klabel("#ruleRequires")] + | #RuleBody "ensures" K [klabel("#ruleEnsures")] + | #RuleBody "requires" K "ensures" K [klabel("#ruleRequiresEnsures")] +endmodule + +// To be used to parse semantic rules +module K + imports KSEQ-SYMBOLIC + imports REQUIRES-ENSURES + imports K-SORT-LATTICE + imports AUTO-CASTS + imports AUTO-FOLLOW + + syntax KBott ::= K "=>" K [klabel(#KRewrite), poly(0, 1, 2), non-assoc] +endmodule + +module RULE-INNER // main parsing module for rules, start symbol: #RuleContent + imports K + imports RULE-CELLS + imports DEFAULT-LAYOUT +endmodule +``` diff --git a/t/config/config.k b/t/config/config.k new file mode 100644 index 0000000..f1fa2b0 --- /dev/null +++ b/t/config/config.k @@ -0,0 +1,8 @@ +module FOOBAR + syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] + + syntax Pgm ::= Foo + syntax Foo ::= "bar" [klabel(bar), function] + | "buzz" [klabel(buzz)] + configuration $PGM .K +endmodule diff --git a/t/config/expected.ekore b/t/config/expected.ekore new file mode 100644 index 0000000..594f19e --- /dev/null +++ b/t/config/expected.ekore @@ -0,0 +1,38 @@ +[ ] + +module A-BASIC-K + sort K { } [ ] + sort KItem { } [ ] +endmodule [ ] + +module B-KSEQ + axiom { R } \equals { K { } , R } ( append { } ( dotk { } ( ) , K2 : K { } ) , K2 : K { } ) [ ] + axiom { R } \equals { K { } , R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } ( K2 : K { } , K3 : K { } ) ) ) [ ] + import A-BASIC-K [ ] + symbol append { } ( K { } , K { } ) : K { } [ function { } ( ) ] + symbol dotk { } ( ) : K { } [ ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ ] +endmodule [ ] + +module C-INJ + axiom { S1 , S2 , S3 , R } \equals { S3 , R } ( inj { S2 , S3 } ( inj { S1 , S2 } ( T : S1 ) ) , inj { S1 , S3 } ( T : S1 ) ) [ ] + symbol inj { From , To } ( From ) : To [ ] +endmodule [ ] + +module D-K + import B-KSEQ [ ] + import C-INJ [ ] +endmodule [ ] + +module FOOBAR + axiom { R } \equals { Foo { } , R } ( bar { } ( ) , buzz2 { } ( ) ) [ ] + import D-K [ ] + sort Fizz { } [ ] + sort Foo { } [ ] + symbol bar { } ( ) : Foo { } [ function { } ( ) ] + symbol buzz2 { } ( ) : Foo { } [ ] + symbol foobar { } ( ) : Fizz { } [ ] + syntax Fizz ::= "foobar" [ klabel ( foobar ) ] + syntax Foo ::= "bar" [ klabel ( bar ) , function ] + syntax Foo ::= "buzz" [ klabel ( buzz2 ) ] +endmodule [ ] From ebb4e74468d2dd31bcc68ba649b0fe0cb97c9a4f Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 2 Jul 2019 19:03:23 +0300 Subject: [PATCH 02/20] Parsing the configuration --- src/command-line.md | 1 + src/kink.md | 37 +++++++++++++++++++++++++++++++++++++ src/kore.md | 5 +++-- 3 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 1a79e31..01939ee 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -21,6 +21,7 @@ module COMMAND-LINE imports PARSE-OUTER imports PARSE-PROGRAM + imports PARSE-CONFIG imports PARSE-TO-EKORE imports FRONTEND-MODULES-TO-KORE-MODULES diff --git a/src/kink.md b/src/kink.md index 6607f88..eabd6da 100644 --- a/src/kink.md +++ b/src/kink.md @@ -47,6 +47,7 @@ module KINK-CONFIGURATION .Set + .Set 1 initSCell(.Map) @@ -246,6 +247,42 @@ module PARSE-PROGRAM endmodule ``` +Parse Config +------------- + +```k +module PARSE-CONFIG + imports RULES-WITH-BUBBLES-COMMON + imports KINK-CONFIGURATION + imports K-PRODUCTION-ABSTRACT + imports EKORE-KSTRING-ABSTRACT + imports KORE-HELPERS + imports STRING + imports FILE-UTIL + imports PARSER-UTIL + + syntax KItem ::= "#parseConfigBubble" + | "#collectConfigGrammar" + + rule #parseConfigBubble ... + kConfiguration(C:Bubble) => kConfiguration(parseWithProductions(GRAMMAR, "K", tokenToString(C))) + GRAMMAR + + rule #parseConfigBubble => .K ... + #STUCK() => .K ... + + rule #collectConfigGrammar ... + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ( .Set => SetItem(SYNTAXDECL) ) REST + requires notBool(SYNTAXDECL in REST) + rule #collectConfigGrammar => .K ... + #STUCK() => .K ... + + rule collectCellNames(K) => + +endmodule +``` + Parse into EKore ---------------- diff --git a/src/kore.md b/src/kore.md index 17002ba..1774f89 100644 --- a/src/kore.md +++ b/src/kore.md @@ -6,6 +6,7 @@ module TOKENS syntax DollarName syntax Numbers syntax BacktickName + syntax KoreString // Abstract syntax KModuleName ::= UpperName @@ -28,6 +29,7 @@ module TOKENS-SYNTAX syntax Numbers ::= r"[\\+-]?[0-9]+" [token] syntax DollarName ::= r"(\\$)([A-Z][A-Za-z\\-0-9]*)" [token] syntax BacktickName ::= r"`(\\\\`|\\\\\\\\|[^`\\\\\\n\\r])+`" [token] + syntax KoreString ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token] endmodule module KORE-COMMON @@ -44,7 +46,6 @@ module KORE-COMMON syntax Variable ::= VariableName ":" Sort [klabel(varType)] syntax Pattern ::= Variable - // | String | Symbol "(" Patterns ")" [klabel(application)] | "\\and" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(and)] | "\\not" "{" Sort "}" "(" Pattern ")" [klabel(not)] @@ -61,7 +62,7 @@ module KORE-COMMON | "\\bottom" "{" Sort "}" "(" ")" [klabel(bottom)] | "\\next" "{" Sort "}" "(" Pattern ")" [klabel(next)] | "\\rewrites" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(rewrites)] - | "\\dv" "{" Sort "}" "(" Pattern ")" [klabel(dv)] + | "\\dv" "{" Sort "}" "(" KoreString ")" [klabel(dv)] syntax Patterns syntax Attribute ::= "[" Patterns "]" [klabel(koreAttributes)] From 95a59df54abc689e7a5316b440171e48a08c120a Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Wed, 17 Jul 2019 17:06:26 +0300 Subject: [PATCH 03/20] Auto generating casts and subsorts not working, strategy error --- src/ekore.md | 2 +- src/inner.md | 2 -- src/kink.md | 77 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 75 insertions(+), 6 deletions(-) diff --git a/src/ekore.md b/src/ekore.md index da8d0a0..f35706e 100644 --- a/src/ekore.md +++ b/src/ekore.md @@ -239,7 +239,7 @@ module ATTRIBUTES-COMMON syntax TagContent ::= UpperName | LowerName | Numbers | EKoreKString syntax TagContents - syntax KEY ::= LowerName [token] + syntax KEY ::= LowerName //[token] // TODO: this token attribute causes a lot of weird ambiguities endmodule diff --git a/src/inner.md b/src/inner.md index ac70efb..3d79684 100644 --- a/src/inner.md +++ b/src/inner.md @@ -68,8 +68,6 @@ module KCELLS | ".Bag" [klabel(cells)] | Cell syntax Bag ::= "(" Bag ")" [bracket] - syntax K ::= Bag - syntax Bag ::= KBott endmodule module K-SORT-LATTICE diff --git a/src/kink.md b/src/kink.md index eabd6da..d8dcbde 100644 --- a/src/kink.md +++ b/src/kink.md @@ -33,6 +33,8 @@ module KINK-CONFIGURATION syntax Declaration ::= "nullDecl" syntax DeclCellSet syntax DeclarationsCellFragment + syntax UpperName ::= String2UpperName (String) [function, functional, hook(STRING.string2token)] + configuration #parseCommandLine($COMMANDLINE:CommandLine, $PGM:Any) .Patterns @@ -47,11 +49,43 @@ module KINK-CONFIGURATION .Set - .Set + + noCastSortsInit // sorts excepted from casts + noLatticeSortsInit + .Set // place to collect the grammar used to parse configurations + 1 initSCell(.Map) token2String($KINKDEPLOYEDDIR:Path) + + syntax Set ::= "noCastSortsInit" [function] + rule noCastSortsInit => // sorts from this list do not receive productions for casting + SetItem(String2UpperName("Cell")) + SetItem(String2UpperName("CellName")) + SetItem(String2UpperName("CellProperties")) + SetItem(String2UpperName("CellProperty")) + SetItem(String2UpperName("KConfigVar")) + SetItem(String2UpperName("KLabel")) + SetItem(String2UpperName("KList")) + SetItem(String2UpperName("KString")) + SetItem(String2UpperName("KVariable")) + SetItem(String2UpperName("Layout")) + syntax Set ::= "noLatticeSortsInit" [function] + rule noLatticeSortsInit => // sorts from this list are not included in the automatic subsorts lattice + SetItem(String2UpperName("Cell")) + SetItem(String2UpperName("CellName")) + SetItem(String2UpperName("CellProperties")) + SetItem(String2UpperName("CellProperty")) + SetItem(String2UpperName("K")) + SetItem(String2UpperName("KBott")) + SetItem(String2UpperName("KConfigVar")) + SetItem(String2UpperName("KLabel")) + SetItem(String2UpperName("KList")) + SetItem(String2UpperName("KString")) + SetItem(String2UpperName("KVariable")) + SetItem(String2UpperName("Layout")) + endmodule ``` @@ -277,9 +311,46 @@ module PARSE-CONFIG requires notBool(SYNTAXDECL in REST) rule #collectConfigGrammar => .K ... #STUCK() => .K ... - - rule collectCellNames(K) => + syntax EKoreKString ::= String2EKoreKString (String) [function, functional, hook(STRING.string2token)] + syntax TagContents ::= String2TagContents (String) [function, functional, hook(STRING.string2token)] + // Add config parsing syntax + // casts: Sort ::= Sort ":Sort" + syntax KItem ::= "#addCasts" + rule #addCasts ... + kSyntaxProduction(SORT, PROD) + NOCASTSORTS (.Set => SetItem(SORT)) + .Set => SetItem( + kSyntaxProduction(SORT, + kProductionWAttr(kProduction(nonTerminal(SORT), + terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), + String2TagContents("#SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) + ... + + requires notBool(SORT in NOCASTSORTS) + + rule #addCasts => .K ... + #STUCK() => .K ... + + // subsorts: K ::= Sort, Sort ::= KBott + syntax KItem ::= "#addSubsorts" + rule #addSubsorts ... + kSyntaxProduction(SORT, PROD) + NOCASTSORTS (.Set => SetItem(SORT)) + .Set => + SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT)), noAtt)) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott"))), noAtt)) + ... + + requires notBool(SORT in NOCASTSORTS) + + rule #addSubsorts => .K ... + #STUCK() => .K ... + + + endmodule ``` From 88c64c8df9a444ff9199c2cb12f75e0f78b90676 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 18 Jul 2019 13:40:52 +0300 Subject: [PATCH 04/20] Call config parsing. --- src/command-line.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/command-line.md b/src/command-line.md index 01939ee..6cd0d5e 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -115,6 +115,30 @@ High-level pipeline steps ~> #productionsToSymbolDeclarations ~> #translateRules ~> #success + + syntax K ::= "#frontendPipeline" //[function] + rule PGM:Any ~> #frontendPipeline + => parseOuter( + {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String + +String + {readFile(DEPLOY_DIR +String "/src/config-inner.k")}:>String + +String + tokenToString(PGM) + ) // add config-inner.k + // create the common module + // create linkage and extras + // parse bubbles + // discard config parser + ~> #defnToConfig + ~> #flattenProductions + // import config parsing syntax + ~> #addCasts + ~> #addSubsorts + ~> #collectConfigGrammar + ~> #parseConfigBubble + // parse config bubbles + + DEPLOY_DIR ``` ```k From 3ba416fb09a8cf1ba4616c4a4123f54ee2308ba4 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 18 Jul 2019 15:40:46 +0300 Subject: [PATCH 05/20] FIx subsort production creation. --- .gitignore | 1 + src/kink.md | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index cf2ee14..f05fade 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ /.build/ /.stack-work/ +.krun* diff --git a/src/kink.md b/src/kink.md index d8dcbde..39c1125 100644 --- a/src/kink.md +++ b/src/kink.md @@ -340,8 +340,8 @@ module PARSE-CONFIG kSyntaxProduction(SORT, PROD) NOCASTSORTS (.Set => SetItem(SORT)) .Set => - SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT)), noAtt)) - SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott"))), noAtt)) + SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt))) ... requires notBool(SORT in NOCASTSORTS) From 58136fe0fc5ddc7b08d8e1b617dd25367deb73a3 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 18 Jul 2019 16:04:13 +0300 Subject: [PATCH 06/20] Parse the configuration only. No disambiguation. No config analysis. --- src/kink.md | 2 +- t/config/config.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kink.md b/src/kink.md index 39c1125..0cae380 100644 --- a/src/kink.md +++ b/src/kink.md @@ -326,7 +326,7 @@ module PARSE-CONFIG terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), kAttributesDeclaration(consAttrList( tagContent(#token("klabel","LowerName"), - String2TagContents("#SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) ... requires notBool(SORT in NOCASTSORTS) diff --git a/t/config/config.k b/t/config/config.k index f1fa2b0..32e76a7 100644 --- a/t/config/config.k +++ b/t/config/config.k @@ -4,5 +4,5 @@ module FOOBAR syntax Pgm ::= Foo syntax Foo ::= "bar" [klabel(bar), function] | "buzz" [klabel(buzz)] - configuration $PGM .K + configuration $PGM:Pgm .K endmodule From e78a9d2335251c8a6db40ccb522cea1894e069b8 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 18 Jul 2019 21:58:54 +0300 Subject: [PATCH 07/20] Extracting configurationInfo --- src/command-line.md | 5 ++++- src/kink.md | 32 ++++++++++++++++++++++++++++++++ src/kore.md | 6 ++++-- 3 files changed, 40 insertions(+), 3 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 6cd0d5e..e1c0bee 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -136,7 +136,10 @@ High-level pipeline steps ~> #addSubsorts ~> #collectConfigGrammar ~> #parseConfigBubble - // parse config bubbles + ~> #extractConfigInfo + // TODO: + // do another parseOuter with rule-inner.k + // parse rule bubbles DEPLOY_DIR ``` diff --git a/src/kink.md b/src/kink.md index 0cae380..9c97021 100644 --- a/src/kink.md +++ b/src/kink.md @@ -49,10 +49,12 @@ module KINK-CONFIGURATION .Set + .Map noCastSortsInit // sorts excepted from casts noLatticeSortsInit .Set // place to collect the grammar used to parse configurations + .Set // place to collect the grammar used to parse rules 1 @@ -294,6 +296,7 @@ module PARSE-CONFIG imports STRING imports FILE-UTIL imports PARSER-UTIL + imports KORE-ABSTRACT syntax KItem ::= "#parseConfigBubble" | "#collectConfigGrammar" @@ -329,6 +332,15 @@ module PARSE-CONFIG String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) ... + .Set => SetItem( + kSyntaxProduction(SORT, + kProductionWAttr(kProduction(nonTerminal(SORT), + terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) + ... + requires notBool(SORT in NOCASTSORTS) rule #addCasts => .K ... @@ -344,12 +356,32 @@ module PARSE-CONFIG SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt))) ... + .Set => + SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt))) + ... + requires notBool(SORT in NOCASTSORTS) rule #addSubsorts => .K ... #STUCK() => .K ... + // collect config info - destructure the configuration and populate + // with \dv key -> type (CellInfo or KConfigVar) + syntax KItem ::= "#extractConfigInfo" + syntax KItem ::= collectCellName(Patterns) + rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... + ( kConfiguration(P) => .Bag) + rule collectCellName( _ { _ } (A)) => collectCellName(A) ... + rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... + rule collectCellName( .Patterns ) => .K ... + + rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... + .Map => CellName |-> Srt ... + + rule #extractConfigInfo => .K ... + #STUCK() => .K ... endmodule ``` diff --git a/src/kore.md b/src/kore.md index 1774f89..cad7016 100644 --- a/src/kore.md +++ b/src/kore.md @@ -115,10 +115,12 @@ endmodule module KORE-ABSTRACT imports KORE-COMMON - syntax Sorts ::= Sort "," Sorts [klabel(consSorts)] + syntax Sorts ::= Sort + | Sort "," Sorts [klabel(consSorts)] | ".Sorts" [klabel(dotSorts )] - syntax Patterns ::= Pattern "," Patterns [klabel(consPatterns)] + syntax Patterns ::= Pattern + | Pattern "," Patterns [klabel(consPatterns)] | ".Patterns" [klabel(dotPatterns )] syntax Declarations ::= Declaration Declarations [klabel(consDeclarations), format(%1%n%2)] From bfe3cdd86e8163f12579b3e8a7deab9034ecf8b9 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Fri, 19 Jul 2019 15:22:38 +0300 Subject: [PATCH 08/20] Started to parse rules. Very simple stuff and no disambiguation. --- src/command-line.md | 16 ++++++++++++- src/kink.md | 50 ++++++++++++++++++++++++++++++++++++++++- src/rule-inner.md | 22 +++++++++--------- t/config/config.k | 2 ++ t/config/expected.ekore | 44 ++++++------------------------------ 5 files changed, 83 insertions(+), 51 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index e1c0bee..bda366e 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -137,9 +137,23 @@ High-level pipeline steps ~> #collectConfigGrammar ~> #parseConfigBubble ~> #extractConfigInfo - // TODO: // do another parseOuter with rule-inner.k + ~> #clearModules + ~> parseOuter( + {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String + +String + {readFile(DEPLOY_DIR +String "/src/rule-inner.k")}:>String + +String + tokenToString(PGM) + ) // add config-inner.k + ~> #defnToConfig + ~> #flattenProductions + ~> #collectRuleGrammar + // TODO: add rule cells + ~> #addRuleCells + ~> #parseConfigBubble // again since I destroyed it when I built // parse rule bubbles + ~> #parseRuleBubble DEPLOY_DIR ``` diff --git a/src/kink.md b/src/kink.md index 9c97021..d2b68d7 100644 --- a/src/kink.md +++ b/src/kink.md @@ -378,11 +378,59 @@ module PARSE-CONFIG rule collectCellName( .Patterns ) => .K ... rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... - .Map => CellName |-> Srt ... + .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... rule #extractConfigInfo => .K ... #STUCK() => .K ... + // remove modules to prepare for second stage + // TODO: find a better way with better modularity + syntax KItem ::= "#clearModules" + rule #clearModules ... + ( _ => .Bag) ... + + rule #clearModules => .K ... + #STUCK() => .K ... + + // collect rule grammar - important to be after config so it doesn't taint the grammar + syntax KItem ::= "#collectRuleGrammar" + rule #collectRuleGrammar ... + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ( .Set => SetItem(SYNTAXDECL) ) REST + requires notBool(SYNTAXDECL in REST) + rule #collectRuleGrammar => .K ... + #STUCK() => .K ... + + // add rule cells + syntax KItem ::= "#addRuleCells" + rule #addRuleCells ... + CellName |-> "CellName" => .Map ... + .Set => SetItem( + kSyntaxProduction(#token("Cell","UpperName"), + kProductionWAttr(kProduction( + terminal(String2EKoreKString("\"<" +String CellName +String ">\"")), kProduction( + nonTerminal(#token("OptionalDots","UpperName")), kProduction( + nonTerminal(#token("K","UpperName")), kProduction( + nonTerminal(#token("OptionalDots","UpperName")), + terminal(String2EKoreKString("\"\"")))))), + kAttributesDeclaration(consAttrList( + tagContent(#token("cellName","LowerName"), String2TagContents(CellName)),consAttrList( + tagSimple(#token("cell","LowerName")), dotAttrList(.KList))))))) + ... + + rule #addRuleCells => .K ... + #STUCK() => .K ... + + // parse rule bubbles + syntax KItem ::= "#parseRuleBubble" + rule #parseRuleBubble ... + kRule(C:Bubble) => kRule(parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))) + GRAMMAR + + rule #parseRuleBubble => .K ... + #STUCK() => .K ... + + endmodule ``` diff --git a/src/rule-inner.md b/src/rule-inner.md index fe8cb6e..1fcf89c 100644 --- a/src/rule-inner.md +++ b/src/rule-inner.md @@ -1,7 +1,5 @@ ```k -require "inner.k" - module RULE-CELLS imports KCELLS @@ -9,21 +7,21 @@ module RULE-CELLS // if this module is imported, the parser automatically // generates, for all productions that have the attribute 'cell' or 'maincell', // a production like below: - //syntax Cell ::= "" #OptionalDots K #OptionalDots "" [klabel()] + //syntax Cell ::= "" OptionalDots K OptionalDots "" [klabel()] - syntax #OptionalDots ::= "..." [klabel(#dots)] - | "" [klabel(#noDots)] + syntax OptionalDots ::= "..." [klabel(dots)] + | "" [klabel(noDots)] endmodule module REQUIRES-ENSURES imports BASIC-K - syntax #RuleBody ::= K + syntax RuleBody ::= K - syntax #RuleContent ::= #RuleBody [klabel("#ruleNoConditions")] - | #RuleBody "requires" K [klabel("#ruleRequires")] - | #RuleBody "ensures" K [klabel("#ruleEnsures")] - | #RuleBody "requires" K "ensures" K [klabel("#ruleRequiresEnsures")] + syntax RuleContent ::= RuleBody [klabel("ruleNoConditions")] + | RuleBody "requires" K [klabel("ruleRequires")] + | RuleBody "ensures" K [klabel("ruleEnsures")] + | RuleBody "requires" K "ensures" K [klabel("ruleRequiresEnsures")] endmodule // To be used to parse semantic rules @@ -34,10 +32,10 @@ module K imports AUTO-CASTS imports AUTO-FOLLOW - syntax KBott ::= K "=>" K [klabel(#KRewrite), poly(0, 1, 2), non-assoc] + syntax KBott ::= K "=>" K [klabel(KRewrite)] endmodule -module RULE-INNER // main parsing module for rules, start symbol: #RuleContent +module RULE-INNER // main parsing module for rules, start symbol: RuleContent imports K imports RULE-CELLS imports DEFAULT-LAYOUT diff --git a/t/config/config.k b/t/config/config.k index 32e76a7..2f83a86 100644 --- a/t/config/config.k +++ b/t/config/config.k @@ -5,4 +5,6 @@ module FOOBAR syntax Foo ::= "bar" [klabel(bar), function] | "buzz" [klabel(buzz)] configuration $PGM:Pgm .K + + rule A:Foo => .K endmodule diff --git a/t/config/expected.ekore b/t/config/expected.ekore index 594f19e..3fee2de 100644 --- a/t/config/expected.ekore +++ b/t/config/expected.ekore @@ -1,38 +1,8 @@ -[ ] - -module A-BASIC-K - sort K { } [ ] - sort KItem { } [ ] -endmodule [ ] - -module B-KSEQ - axiom { R } \equals { K { } , R } ( append { } ( dotk { } ( ) , K2 : K { } ) , K2 : K { } ) [ ] - axiom { R } \equals { K { } , R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } ( K2 : K { } , K3 : K { } ) ) ) [ ] - import A-BASIC-K [ ] - symbol append { } ( K { } , K { } ) : K { } [ function { } ( ) ] - symbol dotk { } ( ) : K { } [ ] - symbol kseq { } ( KItem { } , K { } ) : K { } [ ] -endmodule [ ] - -module C-INJ - axiom { S1 , S2 , S3 , R } \equals { S3 , R } ( inj { S2 , S3 } ( inj { S1 , S2 } ( T : S1 ) ) , inj { S1 , S3 } ( T : S1 ) ) [ ] - symbol inj { From , To } ( From ) : To [ ] -endmodule [ ] - -module D-K - import B-KSEQ [ ] - import C-INJ [ ] -endmodule [ ] - module FOOBAR - axiom { R } \equals { Foo { } , R } ( bar { } ( ) , buzz2 { } ( ) ) [ ] - import D-K [ ] - sort Fizz { } [ ] - sort Foo { } [ ] - symbol bar { } ( ) : Foo { } [ function { } ( ) ] - symbol buzz2 { } ( ) : Foo { } [ ] - symbol foobar { } ( ) : Fizz { } [ ] - syntax Fizz ::= "foobar" [ klabel ( foobar ) ] - syntax Foo ::= "bar" [ klabel ( bar ) , function ] - syntax Foo ::= "buzz" [ klabel ( buzz2 ) ] -endmodule [ ] + configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToFoo { .Sorts } ( \dv { KVariable { .Sorts } } ( "A" ) , .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) + syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] + syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] + syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] + syntax Pgm ::= Foo noAtt +endmodule [ .Patterns ] From ccb69bfd00ca90bf8593397e730fcf8d522d6b3a Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 1 Aug 2019 14:52:06 +0300 Subject: [PATCH 09/20] Managed to parse IMP with ambiguities --- src/command-line.md | 2 +- src/ekore.md | 10 ++++- src/inner.md | 2 +- src/kink.md | 14 ++++--- src/parser-util.md | 2 +- t/imp/expected.ekore | 27 +++++++++++++ t/imp/imp-typed.k | 90 ++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 137 insertions(+), 10 deletions(-) create mode 100644 t/imp/expected.ekore create mode 100644 t/imp/imp-typed.k diff --git a/src/command-line.md b/src/command-line.md index bda366e..0187b31 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -145,7 +145,7 @@ High-level pipeline steps {readFile(DEPLOY_DIR +String "/src/rule-inner.k")}:>String +String tokenToString(PGM) - ) // add config-inner.k + ) // add rule-inner.k ~> #defnToConfig ~> #flattenProductions ~> #collectRuleGrammar diff --git a/src/ekore.md b/src/ekore.md index f35706e..642cb49 100644 --- a/src/ekore.md +++ b/src/ekore.md @@ -70,7 +70,8 @@ module RULES-WITH-BUBBLES-COMMON imports CONFIG-RULE-CONTEXT-COMMON syntax BubbleItem syntax Bubble - syntax RuleContents ::= Bubble + syntax BubbleWithAttr + syntax RuleContents ::= BubbleWithAttr endmodule module RULES-WITH-BUBBLES-ABSTRACT @@ -81,6 +82,8 @@ endmodule module RULES-WITH-BUBBLES-SYNTAX imports RULES-WITH-BUBBLES-COMMON imports CONFIG-RULE-CONTEXT-SYNTAX + syntax BubbleWithAttr ::= Bubble [klabel(noAttrs)] + | Bubble KAttributesDeclaration [klabel(attrs), prefer] syntax BubbleItem ::= r"[^ \t\n\r]+" [token, reject2("rule|syntax|endmodule|configuration|context")] syntax Bubble ::= Bubble BubbleItem [token] | BubbleItem [token] @@ -187,9 +190,12 @@ endmodule module CONFIG-RULE-CONTEXT-ABSTRACT imports CONFIG-RULE-CONTEXT-COMMON + imports RULES-WITH-BUBBLES-COMMON imports KORE-ABSTRACT syntax RuleContents ::= noAttrs(Pattern) [klabel(noAttrs), format(%3)] - | attrs(Pattern, KAttributesDeclaration) [klabel(attrs), prefer] + | attrs(Pattern, KAttributesDeclaration) [klabel(attrs)] + | noAttrs(Bubble) [klabel(noAttrs), format(%3)] + | attrs(Bubble, KAttributesDeclaration) [klabel(attrs)] endmodule module CONFIG-RULE-CONTEXT-SYNTAX diff --git a/src/inner.md b/src/inner.md index 3d79684..892d260 100644 --- a/src/inner.md +++ b/src/inner.md @@ -13,7 +13,7 @@ module BASIC-K endmodule module KSTRING - syntax KString ::= r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token] + syntax KString ::= r"[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" [token] // optionally qualified strings, like in Scala "abc", i"abc", r"a*bc", etc. endmodule diff --git a/src/kink.md b/src/kink.md index d2b68d7..a611d37 100644 --- a/src/kink.md +++ b/src/kink.md @@ -302,7 +302,7 @@ module PARSE-CONFIG | "#collectConfigGrammar" rule #parseConfigBubble ... - kConfiguration(C:Bubble) => kConfiguration(parseWithProductions(GRAMMAR, "K", tokenToString(C))) + kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) GRAMMAR rule #parseConfigBubble => .K ... @@ -371,7 +371,7 @@ module PARSE-CONFIG syntax KItem ::= "#extractConfigInfo" syntax KItem ::= collectCellName(Patterns) rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... - ( kConfiguration(P) => .Bag) + ( kConfiguration(noAttrs(P)) => .Bag) rule collectCellName( _ { _ } (A)) => collectCellName(A) ... rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... @@ -414,8 +414,9 @@ module PARSE-CONFIG nonTerminal(#token("OptionalDots","UpperName")), terminal(String2EKoreKString("\"\"")))))), kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), String2TagContents(CellName +String "cell")),consAttrList( tagContent(#token("cellName","LowerName"), String2TagContents(CellName)),consAttrList( - tagSimple(#token("cell","LowerName")), dotAttrList(.KList))))))) + tagSimple(#token("cell","LowerName")), dotAttrList(.KList)))))))) ... rule #addRuleCells => .K ... @@ -424,7 +425,10 @@ module PARSE-CONFIG // parse rule bubbles syntax KItem ::= "#parseRuleBubble" rule #parseRuleBubble ... - kRule(C:Bubble) => kRule(parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))) + kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) + GRAMMAR + rule #parseRuleBubble ... + kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) GRAMMAR rule #parseRuleBubble => .K ... @@ -579,7 +583,7 @@ module FLATTEN-PRODUCTIONS rule #flattenProductions ... - kSyntaxProduction(SORT, P1 > P2) + kSyntaxProduction(SORT, P1 > _:AssocAttribute P2) => kSyntaxProduction(SORT, P1) kSyntaxProduction(SORT, P2) ... diff --git a/src/parser-util.md b/src/parser-util.md index ca13d4f..5068a87 100644 --- a/src/parser-util.md +++ b/src/parser-util.md @@ -116,7 +116,7 @@ module PARSER-UTIL rule KProductionToString(PI:KProductionItem) => KProductionItemToString(PI) rule KProductionToString(kProduction(PI, PIs)) - => KProductionItemToString(PI) +String "\n" +String KProductionToString(PIs) + => KProductionItemToString(PI) +String " " +String KProductionToString(PIs) rule KProductionToString(TAG:Tag(KSORTLIST:KSortList)) => tokenToString(TAG) +String "(" +String KSortListToString(KSORTLIST) +String ")" diff --git a/t/imp/expected.ekore b/t/imp/expected.ekore new file mode 100644 index 0000000..0828fc8 --- /dev/null +++ b/t/imp/expected.ekore @@ -0,0 +1,27 @@ +module IMP-TYPED + import IMP-TYPED-SYNTAX [ .Patterns ] + + configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"yellow\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"green\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "state" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"red\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , emptyMap { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "state" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( block { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( emptyBlock { .Sorts } ( .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( start { .Sorts } ( emptyIds { .Sorts } ( .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( start { .Sorts } ( emptyIds { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( kSequence { .Sorts } ( \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , .Patterns ) ) , \or { Stmt { .Sorts } } ( KRewrite { .Sorts } ( \or { Stmt { .Sorts } } ( SemanticCastToStmt { .Sorts } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) , \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \or { Stmt { .Sorts } } ( SemanticCastToStmt { .Sorts } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) , \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( kSequence { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) ) , \or { KBott { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \or { KBott { .Sorts } } ( kSequence { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( kSequence { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( \or { Stmt { .Sorts } } ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( if { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( block { .Sorts } ( stmts { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , emptyBlock { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) ) , \or { Stmt { .Sorts } } ( KRewrite { .Sorts } ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( if { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( block { .Sorts } ( stmts { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , emptyBlock { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule ruleNoConditions { .Sorts } ( \or { AExp { .Sorts } } ( uminus { .Sorts } ( \or { Int { .Sorts } } ( minusInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , \or { Int { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( minusInt { .Sorts } ( \dv { Int { .Sorts } } ( "0" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Int { .Sorts } } ( ) ) ) , .Patterns ) , \or { AExp { .Sorts } } ( minusInt { .Sorts } ( KRewrite { .Sorts } ( uminus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , \or { AExp { .Sorts } } ( KRewrite { .Sorts } ( uminus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) , ( minusInt { .Sorts } ( \dv { Int { .Sorts } } ( "0" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , .Patterns ) ) , \bottom { AExp { .Sorts } } ( ) ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , .Patterns ) ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , .Patterns ) ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( not { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , ( notBool { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , .Patterns ) ) , .Patterns ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( not { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , ( notBool { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { Bag { .Sorts } } ( cells { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( lteInt { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \or { Int { .Sorts } } ( lteInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Int { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( lteInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Int { .Sorts } } ( ) ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lteInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( mapConcat { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( stmts { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { Bag { .Sorts } } ( ) ) ) ) ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { Bag { .Sorts } } ( cells { .Sorts } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( plusInt { .Sorts } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( plusInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( mapConcat { .Sorts } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \or { Int { .Sorts } } ( plusInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Int { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( plusInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Int { .Sorts } } ( ) ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( stmts { .Sorts } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { Bag { .Sorts } } ( ) ) ) ) ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( SemanticCastToId { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( asgn { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( SemanticCastToInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) , .Patterns ) ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleRequires { .Sorts } ( \or { Bag { .Sorts } } ( cells { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( divInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { KBott { .Sorts } } ( divInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( divInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( mapConcat { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( divInt { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( stmts { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { Bag { .Sorts } } ( ) ) ) ) ) ) ) , ( neInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) + rule ruleRequires { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( start { .Sorts } ( \or { Ids { .Sorts } } ( consIds { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "Xs" ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , .Patterns ) ) , \or { Ids { .Sorts } } ( KRewrite { .Sorts } ( consIds { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , \bottom { Ids { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( mapConcat { .Sorts } ( SemanticCastToMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , ( \or { Map { .Sorts } } ( mapItem { .Sorts } ( KRewrite { .Sorts } ( emptyMap { .Sorts } ( .Patterns ) , ( \dv { KVariable { .Sorts } } ( "X" ) , .Patterns ) ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , \or { Map { .Sorts } } ( KRewrite { .Sorts } ( emptyMap { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Map { .Sorts } } ( ) ) ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , ( notBool { .Sorts } ( keyInSet { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( keysOfMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , .Patterns ) ) , .Patterns ) , .Patterns ) ) + + syntax Id ::= "n" [ token , .AttrList ] + syntax Id ::= "sum" [ token , .AttrList ] + syntax KResult ::= Bool noAtt + syntax KResult ::= Int noAtt +endmodule [ .Patterns ] diff --git a/t/imp/imp-typed.k b/t/imp/imp-typed.k new file mode 100644 index 0000000..84204e7 --- /dev/null +++ b/t/imp/imp-typed.k @@ -0,0 +1,90 @@ +// Copyright (c) 2014-2018 K Team. All Rights Reserved. + +module DOMAINS-SYNTAX + syntax Map ::= ".Map" [klabel(emptyMap)] + | K "|->" K [klabel(mapItem)] + | Map Map [klabel(mapConcat), left] + syntax Set ::= "keys" "(" Map ")" [klabel(keysOfMap)] + + syntax Int ::= r"[0-9]+" [prefer, token] + | Int "<=Int" Int [klabel(lteInt)] + | Int "+Int" Int [klabel(plusInt)] + | Int "-Int" Int [klabel(minusInt)] + | Int "/Int" Int [klabel(divInt)] + | Int "=/=Int" Int [klabel(neInt)] + syntax Id //::= r"(? AExp "+" AExp [klabel(plus), left, strict] + | "(" AExp ")" [bracket] + syntax BExp ::= Bool + | AExp "<=" AExp [klabel(lte), seqstrict] + | "!" BExp [klabel(not), strict] + > BExp "&&" BExp [klabel(and), left, strict(1)] + | "(" BExp ")" [bracket] + syntax Block ::= "{" "}" [klabel(emptyBlock)] + | "{" Stmt "}" [klabel(block)] + syntax Stmt ::= Block + | Id "=" AExp ";" [klabel(asgn), strict(2)] + | "if" "(" BExp ")" + Block "else" Block [klabel(if), strict(1)] + | "while" "(" BExp ")" Block [klabel(while)] + > Stmt Stmt [klabel(stmts), left] + syntax Pgm ::= "int" Ids ";" Stmt [klabel(start)] + syntax Ids ::= Id + | Id "," Ids [klabel(consIds)] + // | "" [klabel(emptyIds)] + | ".Ids" [klabel(emptyIds)] +endmodule + + +module IMP-TYPED + imports IMP-TYPED-SYNTAX + syntax KResult ::= Int | Bool + + configuration + $PGM:Pgm + .Map + + +// AExp + rule X:Id => I ... ... X |-> I ... + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 + rule I1 + I2 => I1 +Int I2 + rule - I1 => 0 -Int I1 +// BExp + rule I1 <= I2 => I1 <=Int I2 + rule ! T => notBool T + rule true && B => B + rule false && _ => false +// Block + rule {} => .K [structural] + rule {S} => S [structural] +// Stmt + rule X = I:Int; => .K ... ... X |-> (_ => I) ... + rule S1:Stmt S2:Stmt => S1 ~> S2 [structural] + rule if (true) S else _ => S + rule if (false) _ else S => S + rule while (B) S => if (B) {S while (B) S} else {} [structural] +// Pgm + rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0) + requires notBool (X in keys(Rho)) + rule int .Ids; S => S [structural] + +// verification ids + syntax Id ::= "n" [token] + | "sum" [token] +endmodule + From 80a1b8c51460e5faff100961c922b5169af426e2 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 6 Aug 2019 15:38:29 +0300 Subject: [PATCH 10/20] Parsing IMP non ambiguously with parens --- ext/k-light | 2 +- t/imp/expected-paren.ekore | 30 ++++++++++++ t/imp/expected.ekore | 24 ++++++---- t/imp/imp-paren.k | 90 ++++++++++++++++++++++++++++++++++++ t/imp/{imp-typed.k => imp.k} | 10 ++-- 5 files changed, 142 insertions(+), 14 deletions(-) create mode 100644 t/imp/expected-paren.ekore create mode 100644 t/imp/imp-paren.k rename t/imp/{imp-typed.k => imp.k} (96%) diff --git a/ext/k-light b/ext/k-light index bec541f..ffc8095 160000 --- a/ext/k-light +++ b/ext/k-light @@ -1 +1 @@ -Subproject commit bec541f5806c1db1e768218a998bb5962f7aac46 +Subproject commit ffc80955b658deca557bea87669432e9d82cf9c1 diff --git a/t/imp/expected-paren.ekore b/t/imp/expected-paren.ekore new file mode 100644 index 0000000..b6b5dd8 --- /dev/null +++ b/t/imp/expected-paren.ekore @@ -0,0 +1,30 @@ +module IMP-PAREN +configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"yellow\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"green\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "state" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"red\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , emptyMap { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "state" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) + import IMP-PAREN-SYNTAX [ .Patterns ] + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( block { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( emptyBlock { .Sorts } ( .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( start { .Sorts } ( emptyIds { .Sorts } ( .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , .Patterns ) ) , ( kSequence { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( if { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( block { .Sorts } ( stmts { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , emptyBlock { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) + + rule ruleNoConditions { .Sorts } ( + KRewrite { .Sorts } ( + and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , + ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lteInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( not { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , ( notBool { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( plus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( plusInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( uminus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) , ( minusInt { .Sorts } ( \dv { Int { .Sorts } } ( "0" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( SemanticCastToId { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( asgn { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( SemanticCastToInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) , .Patterns ) ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleRequires { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( divInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , ( neInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) + rule ruleRequires { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( start { .Sorts } ( KRewrite { .Sorts } ( consIds { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( mapConcat { .Sorts } ( SemanticCastToMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , ( KRewrite { .Sorts } ( emptyMap { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , ( notBool { .Sorts } ( keyInSet { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( keysOfMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , .Patterns ) ) , .Patterns ) , .Patterns ) ) + syntax Id ::= "n" [ token , .AttrList ] + syntax Id ::= "sum" [ token , .AttrList ] + syntax KResult ::= Bool noAtt + syntax KResult ::= Int noAtt + +endmodule diff --git a/t/imp/expected.ekore b/t/imp/expected.ekore index 0828fc8..7735dc1 100644 --- a/t/imp/expected.ekore +++ b/t/imp/expected.ekore @@ -1,14 +1,21 @@ -module IMP-TYPED - import IMP-TYPED-SYNTAX [ .Patterns ] - - configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"yellow\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"green\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "state" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"red\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , emptyMap { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "state" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) +module IMP +configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"yellow\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"green\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "state" ) , ( cellPropertyList { .Sorts } ( cellProperty { .Sorts } ( \dv { CellName { .Sorts } } ( "color" ) , ( \dv { KString { .Sorts } } ( "\"red\"" ) , .Patterns ) ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , .Patterns ) ) , emptyMap { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "state" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) + import IMP-SYNTAX [ .Patterns ] rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( block { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) rule attrs ( ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( emptyBlock { .Sorts } ( .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) , [ structural , .AttrList ] ) rule attrs ( ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( start { .Sorts } ( emptyIds { .Sorts } ( .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( start { .Sorts } ( emptyIds { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) , [ structural , .AttrList ] ) rule attrs ( ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( kSequence { .Sorts } ( \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , .Patterns ) ) , \or { Stmt { .Sorts } } ( KRewrite { .Sorts } ( \or { Stmt { .Sorts } } ( SemanticCastToStmt { .Sorts } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) , \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \or { Stmt { .Sorts } } ( SemanticCastToStmt { .Sorts } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) , \or { Stmt { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , ( kSequence { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) ) , \or { KBott { .Sorts } } ( stmts { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) , ( \or { KBott { .Sorts } } ( kSequence { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "S1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( SemanticCastToStmt { .Sorts } ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) , ( kSequence { .Sorts } ( \dv { KVariable { .Sorts } } ( "S1" ) , ( \dv { KVariable { .Sorts } } ( "S2" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) ) , .Patterns ) , [ structural , .AttrList ] ) rule attrs ( ruleNoConditions { .Sorts } ( \or { Stmt { .Sorts } } ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( if { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( block { .Sorts } ( stmts { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , emptyBlock { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) ) , \or { Stmt { .Sorts } } ( KRewrite { .Sorts } ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( if { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( block { .Sorts } ( stmts { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( while { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) , emptyBlock { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , \bottom { Stmt { .Sorts } } ( ) ) ) , .Patterns ) , [ structural , .AttrList ] ) rule ruleNoConditions { .Sorts } ( \or { AExp { .Sorts } } ( uminus { .Sorts } ( \or { Int { .Sorts } } ( minusInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , \or { Int { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( minusInt { .Sorts } ( \dv { Int { .Sorts } } ( "0" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Int { .Sorts } } ( ) ) ) , .Patterns ) , \or { AExp { .Sorts } } ( minusInt { .Sorts } ( KRewrite { .Sorts } ( uminus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , \or { AExp { .Sorts } } ( KRewrite { .Sorts } ( uminus { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) , ( minusInt { .Sorts } ( \dv { Int { .Sorts } } ( "0" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , .Patterns ) ) , \bottom { AExp { .Sorts } } ( ) ) ) ) , .Patterns ) - rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , .Patterns ) ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( + \or { BExp { .Sorts } } ( + and { .Sorts } ( + \dv { Bool { .Sorts } } ( "false" ) , + ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , .Patterns ) ) , + \or { BExp { .Sorts } } ( + KRewrite { .Sorts } ( + and { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , + ( \dv { Bool { .Sorts } } ( "false" ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "B" ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , .Patterns ) ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( and { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "B" ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) rule ruleNoConditions { .Sorts } ( \or { BExp { .Sorts } } ( not { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , ( notBool { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , .Patterns ) ) , .Patterns ) , \or { BExp { .Sorts } } ( KRewrite { .Sorts } ( not { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , ( notBool { .Sorts } ( \dv { KVariable { .Sorts } } ( "T" ) , .Patterns ) , .Patterns ) ) , \bottom { BExp { .Sorts } } ( ) ) ) , .Patterns ) rule ruleNoConditions { .Sorts } ( \or { Bag { .Sorts } } ( cells { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( lteInt { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \or { Int { .Sorts } } ( lteInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Int { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( lteInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Int { .Sorts } } ( ) ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lteInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( mapConcat { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( stmts { .Sorts } ( KRewrite { .Sorts } ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( lte { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { Bag { .Sorts } } ( ) ) ) ) ) ) ) , .Patterns ) @@ -16,12 +23,13 @@ module IMP-TYPED rule ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "false" ) , ( \dv { KVariable { .Sorts } } ( "_" ) , KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "S" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) rule ruleNoConditions { .Sorts } ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , \or { KBott { .Sorts } } ( if { .Sorts } ( \dv { Bool { .Sorts } } ( "true" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "S" ) , .Patterns ) ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( SemanticCastToId { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , .Patterns ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) - rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( asgn { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( SemanticCastToInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) , .Patterns ) ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) + rule ruleNoConditions { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( KRewrite { .Sorts } ( asgn { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( SemanticCastToInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) , .Patterns ) ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( dots { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "_" ) , ( \dv { KVariable { .Sorts } } ( "I" ) , .Patterns ) ) , .Patterns ) ) , dots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , .Patterns ) rule ruleRequires { .Sorts } ( \or { Bag { .Sorts } } ( cells { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \or { KBott { .Sorts } } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( divInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { KBott { .Sorts } } ( divInt { .Sorts } ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { KBott { .Sorts } } ( ) ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( divInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , .Patterns ) ) , \or { Bag { .Sorts } } ( mapConcat { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( divInt { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I1" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \or { Bag { .Sorts } } ( stmts { .Sorts } ( KRewrite { .Sorts } ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , ( div { .Sorts } ( \dv { KVariable { .Sorts } } ( "I1" ) , ( \dv { KVariable { .Sorts } } ( "Int" ) , .Patterns ) ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "I2" ) , .Patterns ) ) , \bottom { Bag { .Sorts } } ( ) ) ) ) ) ) ) , ( neInt { .Sorts } ( \dv { KVariable { .Sorts } } ( "I2" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) rule ruleRequires { .Sorts } ( cells { .Sorts } ( kcell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( start { .Sorts } ( \or { Ids { .Sorts } } ( consIds { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( KRewrite { .Sorts } ( \dv { KVariable { .Sorts } } ( "Xs" ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , .Patterns ) ) , \or { Ids { .Sorts } } ( KRewrite { .Sorts } ( consIds { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , ( \dv { KVariable { .Sorts } } ( "Xs" ) , .Patterns ) ) , \bottom { Ids { .Sorts } } ( ) ) ) , ( \dv { KVariable { .Sorts } } ( "_" ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , ( statecell { .Sorts } ( noDots { .Sorts } ( .Patterns ) , ( mapConcat { .Sorts } ( SemanticCastToMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , ( \or { Map { .Sorts } } ( mapItem { .Sorts } ( KRewrite { .Sorts } ( emptyMap { .Sorts } ( .Patterns ) , ( \dv { KVariable { .Sorts } } ( "X" ) , .Patterns ) ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , \or { Map { .Sorts } } ( KRewrite { .Sorts } ( emptyMap { .Sorts } ( .Patterns ) , ( mapItem { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( \dv { Int { .Sorts } } ( "0" ) , .Patterns ) ) , .Patterns ) ) , \bottom { Map { .Sorts } } ( ) ) ) , .Patterns ) ) , noDots { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) ) , ( notBool { .Sorts } ( keyInSet { .Sorts } ( \dv { KVariable { .Sorts } } ( "X" ) , ( keysOfMap { .Sorts } ( \dv { KVariable { .Sorts } } ( "Rho" ) , .Patterns ) , .Patterns ) ) , .Patterns ) , .Patterns ) ) - syntax Id ::= "n" [ token , .AttrList ] syntax Id ::= "sum" [ token , .AttrList ] syntax KResult ::= Bool noAtt syntax KResult ::= Int noAtt -endmodule [ .Patterns ] + +endmodule + \ No newline at end of file diff --git a/t/imp/imp-paren.k b/t/imp/imp-paren.k new file mode 100644 index 0000000..33b52b7 --- /dev/null +++ b/t/imp/imp-paren.k @@ -0,0 +1,90 @@ +// Copyright (c) 2014-2018 K Team. All Rights Reserved. + +module DOMAINS-SYNTAX + syntax Map ::= ".Map" [klabel(emptyMap)] + | K "|->" K [klabel(mapItem)] + | Map Map [klabel(mapConcat), left] + syntax Set ::= "keys" "(" Map ")" [klabel(keysOfMap)] + + syntax Int ::= r"[0-9]+" [prefer, token] + | Int "<=Int" Int [klabel(lteInt)] + | Int "+Int" Int [klabel(plusInt)] + | Int "-Int" Int [klabel(minusInt)] + | Int "/Int" Int [klabel(divInt)] + | Int "=/=Int" Int [klabel(neInt)] + syntax Id //::= r"(? AExp "+" AExp [klabel(plus), left, strict] + | "(" AExp ")" [bracket] + syntax BExp ::= Bool + | AExp "<=" AExp [klabel(lte), seqstrict] + | "!" BExp [klabel(not), strict] + > BExp "&&" BExp [klabel(and), left, strict(1)] + | "(" BExp ")" [bracket] + syntax Block ::= "{" "}" [klabel(emptyBlock)] + | "{" Stmt "}" [klabel(block)] + syntax Stmt ::= Block + | Id "=" AExp ";" [klabel(asgn), strict(2)] + | "if" "(" BExp ")" + Block "else" Block [klabel(if), strict(1)] + | "while" "(" BExp ")" Block [klabel(while)] + > Stmt Stmt [klabel(stmts), left] + syntax Pgm ::= "int" Ids ";" Stmt [klabel(start)] + syntax Ids ::= Id // List{Id,","} + | Id "," Ids [klabel(consIds)] + // | "" [klabel(emptyIds)] + | ".Ids" [klabel(emptyIds)] +endmodule + + +module IMP-PAREN + imports IMP-PAREN-SYNTAX + syntax KResult ::= Int | Bool + + configuration + $PGM:Pgm + .Map + + +// AExp + rule X:Id => I ... ... X |-> I ... + rule (I1 / I2) => (I1 /Int I2) requires I2 =/=Int 0 + rule (I1 + I2) => (I1 +Int I2) + rule (- I1) => (0 -Int I1) +// BExp + rule (I1 <= I2) => (I1 <=Int I2) + rule (! T) => notBool T + rule (true && B) => B + rule (false && _) => false +// Block + rule {} => .K [structural] + rule {S} => S [structural] +// Stmt + rule X = I:Int; => .K ... ... X |-> (_ => I) ... + rule (S1:Stmt (S2:Stmt)) => (S1 ~> S2) [structural] + rule (if (true) S else _) => S + rule (if (false) _ else S) => S + rule (while (B) S) => if (B) {S while (B) S} else {} [structural] +// Pgm + rule int ((X,Xs) => Xs);_ Rho:Map (.Map => (X|->0)) + requires notBool (X in keys(Rho)) + rule (int .Ids; S) => S [structural] + +// verification ids + syntax Id ::= "n" [token] + | "sum" [token] +endmodule + diff --git a/t/imp/imp-typed.k b/t/imp/imp.k similarity index 96% rename from t/imp/imp-typed.k rename to t/imp/imp.k index 84204e7..009093e 100644 --- a/t/imp/imp-typed.k +++ b/t/imp/imp.k @@ -21,7 +21,7 @@ module DOMAINS-SYNTAX syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" endmodule -module IMP-TYPED-SYNTAX +module IMP-SYNTAX imports DOMAINS-SYNTAX syntax AExp ::= Int | Id @@ -43,15 +43,15 @@ module IMP-TYPED-SYNTAX | "while" "(" BExp ")" Block [klabel(while)] > Stmt Stmt [klabel(stmts), left] syntax Pgm ::= "int" Ids ";" Stmt [klabel(start)] - syntax Ids ::= Id + syntax Ids ::= Id // List{Id,","} | Id "," Ids [klabel(consIds)] // | "" [klabel(emptyIds)] | ".Ids" [klabel(emptyIds)] endmodule -module IMP-TYPED - imports IMP-TYPED-SYNTAX +module IMP + imports IMP-SYNTAX syntax KResult ::= Int | Bool configuration @@ -70,7 +70,7 @@ module IMP-TYPED rule true && B => B rule false && _ => false // Block - rule {} => .K [structural] + rule {} => .K [structural] rule {S} => S [structural] // Stmt rule X = I:Int; => .K ... ... X |-> (_ => I) ... From 043995787ee80efa09bafb8150a844ce620149f6 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 8 Aug 2019 22:50:12 +0300 Subject: [PATCH 11/20] Parsing configs in a modular way --- build | 4 +- src/command-line.md | 11 ++---- src/config-inner.md | 23 ------------ src/inner.md | 64 ++++++++++++++++++++++++++++++++ src/kink.md | 89 +++++++++++++++++++++++++-------------------- src/rule-inner.md | 43 ---------------------- 6 files changed, 118 insertions(+), 116 deletions(-) delete mode 100644 src/config-inner.md delete mode 100644 src/rule-inner.md diff --git a/build b/build index 9b9954f..eb7f44e 100755 --- a/build +++ b/build @@ -54,12 +54,10 @@ kore = 'src/kore.md' parser = 'src/parser-util.md' file = 'src/file-util.md' inner = 'src/inner.md' -configinner = 'src/config-inner.md' -ruleinner = 'src/rule-inner.md' kink = proj.definition( backend = 'ocaml' , main = 'src/kink.md' - , other = [kore, ekore, parser, file, 'src/command-line.md', k_light, inner, configinner, ruleinner] + , other = [kore, ekore, parser, file, 'src/command-line.md', k_light, inner] , directory = proj.builddir('kink') , flags = '--syntax-module KINK-SYNTAX' , alias = 'kink' diff --git a/src/command-line.md b/src/command-line.md index 0187b31..87a2321 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -121,8 +121,6 @@ High-level pipeline steps => parseOuter( {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String +String - {readFile(DEPLOY_DIR +String "/src/config-inner.k")}:>String - +String tokenToString(PGM) ) // add config-inner.k // create the common module @@ -132,18 +130,15 @@ High-level pipeline steps ~> #defnToConfig ~> #flattenProductions // import config parsing syntax - ~> #addCasts - ~> #addSubsorts - ~> #collectConfigGrammar ~> #parseConfigBubble + /*~> #addCasts + ~> #addSubsorts ~> #extractConfigInfo // do another parseOuter with rule-inner.k ~> #clearModules ~> parseOuter( {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String +String - {readFile(DEPLOY_DIR +String "/src/rule-inner.k")}:>String - +String tokenToString(PGM) ) // add rule-inner.k ~> #defnToConfig @@ -153,7 +148,7 @@ High-level pipeline steps ~> #addRuleCells ~> #parseConfigBubble // again since I destroyed it when I built // parse rule bubbles - ~> #parseRuleBubble + ~> #parseRuleBubble*/ DEPLOY_DIR ``` diff --git a/src/config-inner.md b/src/config-inner.md deleted file mode 100644 index 9e88377..0000000 --- a/src/config-inner.md +++ /dev/null @@ -1,23 +0,0 @@ -```k -//require "inner.k" - -module CONFIG-CELLS - imports KCELLS - imports RULE-LISTS - syntax CellName ::= r"[a-zA-Z][A-Za-z0-9'_]*" [token] - - syntax Cell ::= "<" CellName CellProperties ">" K "" [klabel(configCell)] - syntax Cell ::= "<" CellName "/>" [klabel(externalCell)] - - syntax CellProperties ::= CellProperty CellProperties [klabel(cellPropertyList)] - | "" [klabel(cellPropertyListTerminator)] - syntax CellProperty ::= CellName "=" KString [klabel(cellProperty)] - -endmodule - -module CONFIG-INNER // main parsing module for configuration, start symbol: K - imports K-TERM - imports CONFIG-CELLS - imports DEFAULT-LAYOUT -endmodule -``` diff --git a/src/inner.md b/src/inner.md index 892d260..e70539a 100644 --- a/src/inner.md +++ b/src/inner.md @@ -118,3 +118,67 @@ module K-TERM imports AUTO-FOLLOW endmodule ``` + +```k +module CONFIG-CELLS + imports KCELLS + imports RULE-LISTS + syntax CellName ::= r"[a-zA-Z][A-Za-z0-9'_]*" [token] + + syntax Cell ::= "<" CellName CellProperties ">" K "" [klabel(configCell)] + syntax Cell ::= "<" CellName "/>" [klabel(externalCell)] + + syntax CellProperties ::= CellProperty CellProperties [klabel(cellPropertyList)] + | "" [klabel(cellPropertyListTerminator)] + syntax CellProperty ::= CellName "=" KString [klabel(cellProperty)] + +endmodule + +module CONFIG-INNER // main parsing module for configuration, start symbol: K + imports K-TERM + imports CONFIG-CELLS + imports DEFAULT-LAYOUT +endmodule +``` + +```k +module RULE-CELLS + imports KCELLS + imports RULE-LISTS + // if this module is imported, the parser automatically + // generates, for all productions that have the attribute 'cell' or 'maincell', + // a production like below: + //syntax Cell ::= "" OptionalDots K OptionalDots "" [klabel()] + + syntax OptionalDots ::= "..." [klabel(dots)] + | "" [klabel(noDots)] +endmodule + +module REQUIRES-ENSURES + imports BASIC-K + + syntax RuleBody ::= K + + syntax RuleContent ::= RuleBody [klabel("ruleNoConditions")] + | RuleBody "requires" K [klabel("ruleRequires")] + | RuleBody "ensures" K [klabel("ruleEnsures")] + | RuleBody "requires" K "ensures" K [klabel("ruleRequiresEnsures")] +endmodule + +// To be used to parse semantic rules +module K + imports KSEQ-SYMBOLIC + imports REQUIRES-ENSURES + imports K-SORT-LATTICE + imports AUTO-CASTS + imports AUTO-FOLLOW + + syntax KBott ::= K "=>" K [klabel(KRewrite)] +endmodule + +module RULE-INNER // main parsing module for rules, start symbol: RuleContent + imports K + imports RULE-CELLS + imports DEFAULT-LAYOUT +endmodule +``` diff --git a/src/kink.md b/src/kink.md index a611d37..baf36bd 100644 --- a/src/kink.md +++ b/src/kink.md @@ -39,7 +39,7 @@ module KINK-CONFIGURATION .Patterns - #token("UNNAMED", "ModuleName"):ModuleName .Patterns @@ -47,15 +47,15 @@ module KINK-CONFIGURATION nullDecl .Set + + noCastSortsInit // sorts excepted from casts + noLatticeSortsInit + .Set // place to collect the grammar used to parse configurations + .Set // place to collect the grammar used to parse rules + .Map - - noCastSortsInit // sorts excepted from casts - noLatticeSortsInit - .Set // place to collect the grammar used to parse configurations - .Set // place to collect the grammar used to parse rules - 1 initSCell(.Map) @@ -297,73 +297,84 @@ module PARSE-CONFIG imports FILE-UTIL imports PARSER-UTIL imports KORE-ABSTRACT + imports META-ACCESSORS syntax KItem ::= "#parseConfigBubble" - | "#collectConfigGrammar" + | "#collectConfigGrammar" "(" ModuleName "," Set ")" + + rule #parseConfigBubble + => #collectConfigGrammar(MName, #getImportedModules(MName) #getImportedModules(#token("CONFIG-INNER", "UpperName"))) + ~> #addConfigCasts + ~> #addConfigSubsorts + ~> #parseConfigBubble + ... + MName + kConfiguration(noAttrs(_:Bubble)) + .Set rule #parseConfigBubble ... kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) GRAMMAR + requires GRAMMAR =/=K .Set rule #parseConfigBubble => .K ... #STUCK() => .K ... - rule #collectConfigGrammar ... + rule #collectConfigGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... + + MName + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ... + + + MainMod + ( .Set => SetItem(SYNTAXDECL) ) REST + ... + + requires notBool(SYNTAXDECL in REST) + rule #collectConfigGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... // same as above but for the seed module kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + MainMod ( .Set => SetItem(SYNTAXDECL) ) REST requires notBool(SYNTAXDECL in REST) - rule #collectConfigGrammar => .K ... + rule #collectConfigGrammar(_, _) => .K ... #STUCK() => .K ... syntax EKoreKString ::= String2EKoreKString (String) [function, functional, hook(STRING.string2token)] syntax TagContents ::= String2TagContents (String) [function, functional, hook(STRING.string2token)] // Add config parsing syntax // casts: Sort ::= Sort ":Sort" - syntax KItem ::= "#addCasts" - rule #addCasts ... - kSyntaxProduction(SORT, PROD) - NOCASTSORTS (.Set => SetItem(SORT)) - .Set => SetItem( + syntax KItem ::= "#addConfigCasts" + rule #addConfigCasts ... + NOCASTSORTS (.Set => SetItem(SORT)) + SetItem(kSyntaxProduction(SORT, PROD)) + (.Set => SetItem( kSyntaxProduction(SORT, kProductionWAttr(kProduction(nonTerminal(SORT), terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), kAttributesDeclaration(consAttrList( tagContent(#token("klabel","LowerName"), - String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) ... - .Set => SetItem( - kSyntaxProduction(SORT, - kProductionWAttr(kProduction(nonTerminal(SORT), - terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), - kAttributesDeclaration(consAttrList( - tagContent(#token("klabel","LowerName"), - String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList)))))) - ... - requires notBool(SORT in NOCASTSORTS) - rule #addCasts => .K ... + rule #addConfigCasts => .K ... #STUCK() => .K ... // subsorts: K ::= Sort, Sort ::= KBott - syntax KItem ::= "#addSubsorts" - rule #addSubsorts ... - kSyntaxProduction(SORT, PROD) - NOCASTSORTS (.Set => SetItem(SORT)) - .Set => + syntax KItem ::= "#addConfigSubsorts" + rule #addConfigSubsorts ... + NOCASTSORTS (.Set => SetItem(SORT)) + SetItem(kSyntaxProduction(SORT, PROD)) + (.Set => SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) - SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt))) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) ... - .Set => - SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) - SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt))) - ... - requires notBool(SORT in NOCASTSORTS) - - rule #addSubsorts => .K ... + + rule #addConfigSubsorts => .K ... #STUCK() => .K ... // collect config info - destructure the configuration and populate diff --git a/src/rule-inner.md b/src/rule-inner.md deleted file mode 100644 index 1fcf89c..0000000 --- a/src/rule-inner.md +++ /dev/null @@ -1,43 +0,0 @@ - -```k - -module RULE-CELLS - imports KCELLS - imports RULE-LISTS - // if this module is imported, the parser automatically - // generates, for all productions that have the attribute 'cell' or 'maincell', - // a production like below: - //syntax Cell ::= "" OptionalDots K OptionalDots "" [klabel()] - - syntax OptionalDots ::= "..." [klabel(dots)] - | "" [klabel(noDots)] -endmodule - -module REQUIRES-ENSURES - imports BASIC-K - - syntax RuleBody ::= K - - syntax RuleContent ::= RuleBody [klabel("ruleNoConditions")] - | RuleBody "requires" K [klabel("ruleRequires")] - | RuleBody "ensures" K [klabel("ruleEnsures")] - | RuleBody "requires" K "ensures" K [klabel("ruleRequiresEnsures")] -endmodule - -// To be used to parse semantic rules -module K - imports KSEQ-SYMBOLIC - imports REQUIRES-ENSURES - imports K-SORT-LATTICE - imports AUTO-CASTS - imports AUTO-FOLLOW - - syntax KBott ::= K "=>" K [klabel(KRewrite)] -endmodule - -module RULE-INNER // main parsing module for rules, start symbol: RuleContent - imports K - imports RULE-CELLS - imports DEFAULT-LAYOUT -endmodule -``` From 321ca9e56fd6e63d3aabb427f3922cb2acaaa578 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Fri, 9 Aug 2019 14:38:50 +0300 Subject: [PATCH 12/20] Parsing rules module by module Tested on the simple config example. --- src/command-line.md | 23 +------ src/kink.md | 147 ++++++++++++++++++++++++++++++++++---------- 2 files changed, 116 insertions(+), 54 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 87a2321..5dbc6ff 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -22,6 +22,7 @@ module COMMAND-LINE imports PARSE-OUTER imports PARSE-PROGRAM imports PARSE-CONFIG + imports PARSE-RULE imports PARSE-TO-EKORE imports FRONTEND-MODULES-TO-KORE-MODULES @@ -123,32 +124,12 @@ High-level pipeline steps +String tokenToString(PGM) ) // add config-inner.k - // create the common module - // create linkage and extras // parse bubbles - // discard config parser ~> #defnToConfig ~> #flattenProductions - // import config parsing syntax ~> #parseConfigBubble - /*~> #addCasts - ~> #addSubsorts ~> #extractConfigInfo - // do another parseOuter with rule-inner.k - ~> #clearModules - ~> parseOuter( - {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String - +String - tokenToString(PGM) - ) // add rule-inner.k - ~> #defnToConfig - ~> #flattenProductions - ~> #collectRuleGrammar - // TODO: add rule cells - ~> #addRuleCells - ~> #parseConfigBubble // again since I destroyed it when I built - // parse rule bubbles - ~> #parseRuleBubble*/ + ~> #parseRuleBubble DEPLOY_DIR ``` diff --git a/src/kink.md b/src/kink.md index baf36bd..9108386 100644 --- a/src/kink.md +++ b/src/kink.md @@ -48,14 +48,20 @@ module KINK-CONFIGURATION .Set - noCastSortsInit // sorts excepted from casts - noLatticeSortsInit + noCastSortsInit // sorts excepted from casts + noLatticeSortsInit .Set // place to collect the grammar used to parse configurations + noCastSortsInit // sorts excepted from casts + noLatticeSortsInit + .Set // collector for already inserted cell productions .Set // place to collect the grammar used to parse rules - .Map + + .Map + .Set + 1 initSCell(.Map) @@ -73,6 +79,9 @@ module KINK-CONFIGURATION SetItem(String2UpperName("KString")) SetItem(String2UpperName("KVariable")) SetItem(String2UpperName("Layout")) + SetItem(String2UpperName("RuleBody")) + SetItem(String2UpperName("RuleContent")) + SetItem(String2UpperName("OptionalDots")) syntax Set ::= "noLatticeSortsInit" [function] rule noLatticeSortsInit => // sorts from this list are not included in the automatic subsorts lattice SetItem(String2UpperName("Cell")) @@ -87,6 +96,9 @@ module KINK-CONFIGURATION SetItem(String2UpperName("KString")) SetItem(String2UpperName("KVariable")) SetItem(String2UpperName("Layout")) + SetItem(String2UpperName("RuleBody")) + SetItem(String2UpperName("RuleContent")) + SetItem(String2UpperName("OptionalDots")) endmodule ``` @@ -104,6 +116,7 @@ Meta functions module KORE-HELPERS imports KORE-ABSTRACT imports K-EQUAL + imports STRING syntax Declarations ::= Declarations "++Declarations" Declarations [function] rule (D1 DS1) ++Declarations DS2 => D1 (DS1 ++Declarations DS2) @@ -123,6 +136,9 @@ module KORE-HELPERS rule (P inPatterns P1:Pattern , PS) => (P inPatterns PS) requires notBool P ==K P1 + + syntax EKoreKString ::= String2EKoreKString (String) [function, functional, hook(STRING.string2token)] + syntax TagContents ::= String2TagContents (String) [function, functional, hook(STRING.string2token)] endmodule ``` @@ -340,13 +356,11 @@ module PARSE-CONFIG rule #collectConfigGrammar(_, _) => .K ... #STUCK() => .K ... - syntax EKoreKString ::= String2EKoreKString (String) [function, functional, hook(STRING.string2token)] - syntax TagContents ::= String2TagContents (String) [function, functional, hook(STRING.string2token)] // Add config parsing syntax // casts: Sort ::= Sort ":Sort" syntax KItem ::= "#addConfigCasts" rule #addConfigCasts ... - NOCASTSORTS (.Set => SetItem(SORT)) + NOCASTSORTS (.Set => SetItem(SORT)) SetItem(kSyntaxProduction(SORT, PROD)) (.Set => SetItem( kSyntaxProduction(SORT, @@ -365,7 +379,7 @@ module PARSE-CONFIG // subsorts: K ::= Sort, Sort ::= KBott syntax KItem ::= "#addConfigSubsorts" rule #addConfigSubsorts ... - NOCASTSORTS (.Set => SetItem(SORT)) + NOCASTSORTS (.Set => SetItem(SORT)) SetItem(kSyntaxProduction(SORT, PROD)) (.Set => SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) @@ -382,40 +396,119 @@ module PARSE-CONFIG syntax KItem ::= "#extractConfigInfo" syntax KItem ::= collectCellName(Patterns) rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... - ( kConfiguration(noAttrs(P)) => .Bag) + kConfiguration(noAttrs(P)) + Configs => Configs SetItem(P) + requires notBool P in Configs rule collectCellName( _ { _ } (A)) => collectCellName(A) ... rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... rule collectCellName( .Patterns ) => .K ... rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... - .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... + .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... rule #extractConfigInfo => .K ... #STUCK() => .K ... - // remove modules to prepare for second stage - // TODO: find a better way with better modularity - syntax KItem ::= "#clearModules" - rule #clearModules ... - ( _ => .Bag) ... +endmodule + +module PARSE-RULE + imports RULES-WITH-BUBBLES-COMMON + imports KINK-CONFIGURATION + imports K-PRODUCTION-ABSTRACT + imports EKORE-KSTRING-ABSTRACT + imports KORE-HELPERS + imports STRING + imports FILE-UTIL + imports PARSER-UTIL + imports KORE-ABSTRACT + imports META-ACCESSORS + + // parse rule bubbles + syntax KItem ::= "#parseRuleBubble" + | "#collectRuleGrammar" "(" ModuleName "," Set ")" + rule #parseRuleBubble + => #collectRuleGrammar(MName, #getImportedModules(MName) #getImportedModules(#token("RULE-INNER", "UpperName"))) + ~> #addRuleCasts + ~> #addRuleSubsorts + ~> #addRuleCells + ~> #parseRuleBubble + ... + MName + kRule(noAttrs(_:Bubble)) + .Set + + rule #parseRuleBubble ... + kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) + GRAMMAR + requires GRAMMAR =/=K .Set + rule #parseRuleBubble ... + kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) + GRAMMAR + requires GRAMMAR =/=K .Set - rule #clearModules => .K ... + rule #parseRuleBubble => .K ... #STUCK() => .K ... - // collect rule grammar - important to be after config so it doesn't taint the grammar syntax KItem ::= "#collectRuleGrammar" - rule #collectRuleGrammar ... + rule #collectRuleGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... + + MName + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ... + + + MainMod + ( .Set => SetItem(SYNTAXDECL) ) REST + ... + + requires notBool(SYNTAXDECL in REST) + rule #collectRuleGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... // same as above but for the seed module kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + MainMod ( .Set => SetItem(SYNTAXDECL) ) REST requires notBool(SYNTAXDECL in REST) - rule #collectRuleGrammar => .K ... + rule #collectRuleGrammar(_, _) => .K ... + #STUCK() => .K ... + + syntax KItem ::= "#addRuleCasts" + rule #addRuleCasts ... + NOCASTSORTS (.Set => SetItem(SORT)) + SetItem(kSyntaxProduction(SORT, PROD)) + (.Set => SetItem( + kSyntaxProduction(SORT, + kProductionWAttr(kProduction(nonTerminal(SORT), + terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) + ... + + requires notBool(SORT in NOCASTSORTS) + + rule #addRuleCasts => .K ... + #STUCK() => .K ... + + // subsorts: K ::= Sort, Sort ::= KBott + syntax KItem ::= "#addRuleSubsorts" + rule #addRuleSubsorts ... + NOCASTSORTS (.Set => SetItem(SORT)) + SetItem(kSyntaxProduction(SORT, PROD)) + (.Set => + SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) + ... + + requires notBool(SORT in NOCASTSORTS) + + rule #addRuleSubsorts => .K ... #STUCK() => .K ... // add rule cells syntax KItem ::= "#addRuleCells" rule #addRuleCells ... - CellName |-> "CellName" => .Map ... + CellName |-> "CellName" ... + Cells => Cells SetItem(CellName) .Set => SetItem( kSyntaxProduction(#token("Cell","UpperName"), kProductionWAttr(kProduction( @@ -430,21 +523,9 @@ module PARSE-CONFIG tagSimple(#token("cell","LowerName")), dotAttrList(.KList)))))))) ... + requires notBool CellName in Cells rule #addRuleCells => .K ... - #STUCK() => .K ... - - // parse rule bubbles - syntax KItem ::= "#parseRuleBubble" - rule #parseRuleBubble ... - kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) - GRAMMAR - rule #parseRuleBubble ... - kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) - GRAMMAR - - rule #parseRuleBubble => .K ... - #STUCK() => .K ... - + #STUCK() => .K ... endmodule ``` From 0bd78f6df19ccf9cf804975d9351938a89252517 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 13 Aug 2019 21:55:57 +0300 Subject: [PATCH 13/20] Refactor collect prods --- src/kink.md | 70 ++++++++++++++++------------------------------------- 1 file changed, 21 insertions(+), 49 deletions(-) diff --git a/src/kink.md b/src/kink.md index 9108386..5ffcf3f 100644 --- a/src/kink.md +++ b/src/kink.md @@ -161,6 +161,23 @@ module META-ACCESSORS koreImport(IMPORTED, _) requires notBool IMPORTED in MODS rule #getImportedModulesSet(MNAME, MODS) => MODS [owise] + + syntax Set ::= #getLocalProds(ModuleName) [function] + syntax Set ::= #getLocalProdsSet(ModuleName, Set) [function] + rule #getLocalProds(MNAME) => #getLocalProdsSet(MNAME, .Set) + rule [[ #getLocalProdsSet(MNAME, PRODS) + => #getLocalProdsSet(MNAME, PRODS SetItem(PRD)) + ]] + MNAME + kSyntaxProduction(_, _) #as PRD + requires notBool PRD in PRODS + rule #getLocalProdsSet(MNAME, PRODS) => PRODS [owise] + + syntax Set ::= #getAllProds(ModuleName) [function] + syntax Set ::= #getAllProdsSet(Set) [function] + rule #getAllProds(MName) => #getAllProdsSet(#getImportedModules(MName)) + rule #getAllProdsSet(SetItem(MName) Rest) => #getLocalProds(MName) #getAllProdsSet(Rest) + rule #getAllProdsSet(.Set) => .Set ``` ```k @@ -316,17 +333,15 @@ module PARSE-CONFIG imports META-ACCESSORS syntax KItem ::= "#parseConfigBubble" - | "#collectConfigGrammar" "(" ModuleName "," Set ")" rule #parseConfigBubble - => #collectConfigGrammar(MName, #getImportedModules(MName) #getImportedModules(#token("CONFIG-INNER", "UpperName"))) - ~> #addConfigCasts + => #addConfigCasts ~> #addConfigSubsorts ~> #parseConfigBubble ... MName kConfiguration(noAttrs(_:Bubble)) - .Set + .Set => #getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")) rule #parseConfigBubble ... kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) @@ -336,26 +351,6 @@ module PARSE-CONFIG rule #parseConfigBubble => .K ... #STUCK() => .K ... - rule #collectConfigGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... - - MName - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - ... - - - MainMod - ( .Set => SetItem(SYNTAXDECL) ) REST - ... - - requires notBool(SYNTAXDECL in REST) - rule #collectConfigGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... // same as above but for the seed module - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - MainMod - ( .Set => SetItem(SYNTAXDECL) ) REST - requires notBool(SYNTAXDECL in REST) - rule #collectConfigGrammar(_, _) => .K ... - #STUCK() => .K ... - // Add config parsing syntax // casts: Sort ::= Sort ":Sort" syntax KItem ::= "#addConfigCasts" @@ -426,17 +421,15 @@ module PARSE-RULE // parse rule bubbles syntax KItem ::= "#parseRuleBubble" - | "#collectRuleGrammar" "(" ModuleName "," Set ")" rule #parseRuleBubble - => #collectRuleGrammar(MName, #getImportedModules(MName) #getImportedModules(#token("RULE-INNER", "UpperName"))) - ~> #addRuleCasts + => #addRuleCasts ~> #addRuleSubsorts ~> #addRuleCells ~> #parseRuleBubble ... MName kRule(noAttrs(_:Bubble)) - .Set + .Set => #getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName")) rule #parseRuleBubble ... kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) @@ -450,27 +443,6 @@ module PARSE-RULE rule #parseRuleBubble => .K ... #STUCK() => .K ... - syntax KItem ::= "#collectRuleGrammar" - rule #collectRuleGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... - - MName - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - ... - - - MainMod - ( .Set => SetItem(SYNTAXDECL) ) REST - ... - - requires notBool(SYNTAXDECL in REST) - rule #collectRuleGrammar(MainMod, SetItem(MName:ModuleName) _:Set) ... // same as above but for the seed module - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - MainMod - ( .Set => SetItem(SYNTAXDECL) ) REST - requires notBool(SYNTAXDECL in REST) - rule #collectRuleGrammar(_, _) => .K ... - #STUCK() => .K ... - syntax KItem ::= "#addRuleCasts" rule #addRuleCasts ... NOCASTSORTS (.Set => SetItem(SORT)) From 3c5ad35dc59ec377be520b014fa8aa6079b56faa Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 13 Aug 2019 22:59:51 +0300 Subject: [PATCH 14/20] Refactor prod generators --- src/kink.md | 133 +++++++++++++++++----------------------------------- 1 file changed, 43 insertions(+), 90 deletions(-) diff --git a/src/kink.md b/src/kink.md index 5ffcf3f..142a268 100644 --- a/src/kink.md +++ b/src/kink.md @@ -48,12 +48,7 @@ module KINK-CONFIGURATION .Set - noCastSortsInit // sorts excepted from casts - noLatticeSortsInit .Set // place to collect the grammar used to parse configurations - noCastSortsInit // sorts excepted from casts - noLatticeSortsInit - .Set // collector for already inserted cell productions .Set // place to collect the grammar used to parse rules @@ -334,14 +329,10 @@ module PARSE-CONFIG syntax KItem ::= "#parseConfigBubble" - rule #parseConfigBubble - => #addConfigCasts - ~> #addConfigSubsorts - ~> #parseConfigBubble - ... + rule #parseConfigBubble ... MName kConfiguration(noAttrs(_:Bubble)) - .Set => #getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")) + .Set => #addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")))) rule #parseConfigBubble ... kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) @@ -353,39 +344,37 @@ module PARSE-CONFIG // Add config parsing syntax // casts: Sort ::= Sort ":Sort" - syntax KItem ::= "#addConfigCasts" - rule #addConfigCasts ... - NOCASTSORTS (.Set => SetItem(SORT)) - SetItem(kSyntaxProduction(SORT, PROD)) - (.Set => SetItem( - kSyntaxProduction(SORT, - kProductionWAttr(kProduction(nonTerminal(SORT), - terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), - kAttributesDeclaration(consAttrList( - tagContent(#token("klabel","LowerName"), - String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) - ... - - requires notBool(SORT in NOCASTSORTS) - - rule #addConfigCasts => .K ... - #STUCK() => .K ... + syntax Set ::= "#addCasts" "(" Set ")" [function] + syntax Set ::= "#addCasts2" "(" Set "," Set ")" [function] + rule #addCasts(Prds) => #addCasts2(Prds, noCastSortsInit) + rule #addCasts2( + SetItem(kSyntaxProduction(SORT, PROD)) + _:Set + (.Set => SetItem( + kSyntaxProduction(SORT, + kProductionWAttr(kProduction(nonTerminal(SORT), + terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) + , SORTS (.Set => SetItem(SORT))) + requires notBool SORT in SORTS + rule #addCasts2(Prds, _) => Prds [owise] // subsorts: K ::= Sort, Sort ::= KBott - syntax KItem ::= "#addConfigSubsorts" - rule #addConfigSubsorts ... - NOCASTSORTS (.Set => SetItem(SORT)) - SetItem(kSyntaxProduction(SORT, PROD)) - (.Set => + syntax Set ::= "#addSubsorts" "(" Set ")" [function] + syntax Set ::= "#addSubsorts2" "(" Set "," Set ")" [function] + rule #addSubsorts(Prds) => #addSubsorts2(Prds, noLatticeSortsInit) + rule #addSubsorts2( + SetItem(kSyntaxProduction(SORT, PROD)) + _:Set + (.Set => SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) - ... - - requires notBool(SORT in NOCASTSORTS) - - rule #addConfigSubsorts => .K ... - #STUCK() => .K ... - + , SORTS (.Set => SetItem(SORT))) + requires notBool SORT in SORTS + rule #addSubsorts2(Prds, _) => Prds [owise] + // collect config info - destructure the configuration and populate // with \dv key -> type (CellInfo or KConfigVar) syntax KItem ::= "#extractConfigInfo" @@ -418,18 +407,14 @@ module PARSE-RULE imports PARSER-UTIL imports KORE-ABSTRACT imports META-ACCESSORS + imports PARSE-CONFIG // parse rule bubbles syntax KItem ::= "#parseRuleBubble" - rule #parseRuleBubble - => #addRuleCasts - ~> #addRuleSubsorts - ~> #addRuleCells - ~> #parseRuleBubble - ... + rule #parseRuleBubble ... MName kRule(noAttrs(_:Bubble)) - .Set => #getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName")) + .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) rule #parseRuleBubble ... kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) @@ -443,45 +428,13 @@ module PARSE-RULE rule #parseRuleBubble => .K ... #STUCK() => .K ... - syntax KItem ::= "#addRuleCasts" - rule #addRuleCasts ... - NOCASTSORTS (.Set => SetItem(SORT)) - SetItem(kSyntaxProduction(SORT, PROD)) - (.Set => SetItem( - kSyntaxProduction(SORT, - kProductionWAttr(kProduction(nonTerminal(SORT), - terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), - kAttributesDeclaration(consAttrList( - tagContent(#token("klabel","LowerName"), - String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) - ... - - requires notBool(SORT in NOCASTSORTS) - - rule #addRuleCasts => .K ... - #STUCK() => .K ... - - // subsorts: K ::= Sort, Sort ::= KBott - syntax KItem ::= "#addRuleSubsorts" - rule #addRuleSubsorts ... - NOCASTSORTS (.Set => SetItem(SORT)) - SetItem(kSyntaxProduction(SORT, PROD)) - (.Set => - SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) - SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) - ... - - requires notBool(SORT in NOCASTSORTS) - - rule #addRuleSubsorts => .K ... - #STUCK() => .K ... - // add rule cells - syntax KItem ::= "#addRuleCells" - rule #addRuleCells ... - CellName |-> "CellName" ... - Cells => Cells SetItem(CellName) - .Set => SetItem( + syntax Set ::= "#addRuleCells" "(" Set ")" [function] + syntax Set ::= "#addRuleCells2" "(" Set "," Set ")" [function] + rule #addRuleCells(Prds) => #addRuleCells2(Prds, .Set) + rule [[ #addRuleCells2( + Prds:Set + (.Set => SetItem( kSyntaxProduction(#token("Cell","UpperName"), kProductionWAttr(kProduction( terminal(String2EKoreKString("\"<" +String CellName +String ">\"")), kProduction( @@ -492,12 +445,12 @@ module PARSE-RULE kAttributesDeclaration(consAttrList( tagContent(#token("klabel","LowerName"), String2TagContents(CellName +String "cell")),consAttrList( tagContent(#token("cellName","LowerName"), String2TagContents(CellName)),consAttrList( - tagSimple(#token("cell","LowerName")), dotAttrList(.KList)))))))) - ... - + tagSimple(#token("cell","LowerName")), dotAttrList(.KList))))))))) + , Cells (.Set => SetItem(CellName))) + ]] + CellName |-> "CellName" ... requires notBool CellName in Cells - rule #addRuleCells => .K ... - #STUCK() => .K ... + rule #addRuleCells2(Prods, _) => Prods [owise] endmodule ``` From e11056b98bd1d5baa6c7b8fcced619281e406a33 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 13 Aug 2019 23:13:58 +0300 Subject: [PATCH 15/20] Move parsing to parser-gen.k --- build | 3 +- src/command-line.md | 1 + src/kink.md | 241 +----------------------------------------- src/parser-gen.md | 251 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 255 insertions(+), 241 deletions(-) create mode 100644 src/parser-gen.md diff --git a/build b/build index eb7f44e..a0790bd 100755 --- a/build +++ b/build @@ -52,12 +52,13 @@ k_light = proj.dotTarget().then(build_k_light()) ekore = 'src/ekore.md' kore = 'src/kore.md' parser = 'src/parser-util.md' +pgen = 'src/parser-gen.md' file = 'src/file-util.md' inner = 'src/inner.md' kink = proj.definition( backend = 'ocaml' , main = 'src/kink.md' - , other = [kore, ekore, parser, file, 'src/command-line.md', k_light, inner] + , other = [kore, ekore, parser, file, pgen, 'src/command-line.md', k_light, inner] , directory = proj.builddir('kink') , flags = '--syntax-module KINK-SYNTAX' , alias = 'kink' diff --git a/src/command-line.md b/src/command-line.md index 5dbc6ff..9445d3a 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -1,5 +1,6 @@ ```k require "file-util.k" +require "parser-gen.k" module COMMAND-LINE-SYNTAX imports STRING-SYNTAX diff --git a/src/kink.md b/src/kink.md index 142a268..0614c62 100644 --- a/src/kink.md +++ b/src/kink.md @@ -33,7 +33,6 @@ module KINK-CONFIGURATION syntax Declaration ::= "nullDecl" syntax DeclCellSet syntax DeclarationsCellFragment - syntax UpperName ::= String2UpperName (String) [function, functional, hook(STRING.string2token)] configuration #parseCommandLine($COMMANDLINE:CommandLine, $PGM:Any) @@ -61,40 +60,7 @@ module KINK-CONFIGURATION 1 initSCell(.Map) token2String($KINKDEPLOYEDDIR:Path) - - syntax Set ::= "noCastSortsInit" [function] - rule noCastSortsInit => // sorts from this list do not receive productions for casting - SetItem(String2UpperName("Cell")) - SetItem(String2UpperName("CellName")) - SetItem(String2UpperName("CellProperties")) - SetItem(String2UpperName("CellProperty")) - SetItem(String2UpperName("KConfigVar")) - SetItem(String2UpperName("KLabel")) - SetItem(String2UpperName("KList")) - SetItem(String2UpperName("KString")) - SetItem(String2UpperName("KVariable")) - SetItem(String2UpperName("Layout")) - SetItem(String2UpperName("RuleBody")) - SetItem(String2UpperName("RuleContent")) - SetItem(String2UpperName("OptionalDots")) - syntax Set ::= "noLatticeSortsInit" [function] - rule noLatticeSortsInit => // sorts from this list are not included in the automatic subsorts lattice - SetItem(String2UpperName("Cell")) - SetItem(String2UpperName("CellName")) - SetItem(String2UpperName("CellProperties")) - SetItem(String2UpperName("CellProperty")) - SetItem(String2UpperName("K")) - SetItem(String2UpperName("KBott")) - SetItem(String2UpperName("KConfigVar")) - SetItem(String2UpperName("KLabel")) - SetItem(String2UpperName("KList")) - SetItem(String2UpperName("KString")) - SetItem(String2UpperName("KVariable")) - SetItem(String2UpperName("Layout")) - SetItem(String2UpperName("RuleBody")) - SetItem(String2UpperName("RuleContent")) - SetItem(String2UpperName("OptionalDots")) - + endmodule ``` @@ -264,211 +230,6 @@ endmodule Transforms ========== -Parse Outer ------------ - -```k -module PARSE-OUTER - imports KINK-CONFIGURATION - imports PARSER-UTIL - - // TODO: remove: #writeStringToFile, #doSystem, #doSystemGetOutput, #doParseAST - syntax KItem ::= "#parseOuter" - rule PGM:Any ~> #parseOuter => parseOuter(tokenToString(PGM)) ... -endmodule -``` - -Parse Program -------------- - -```k -module PARSE-PROGRAM - imports KINK-CONFIGURATION - imports K-PRODUCTION-ABSTRACT - imports EKORE-KSTRING-ABSTRACT - imports KORE-HELPERS - imports STRING - imports FILE-UTIL - imports PARSER-UTIL - - syntax KItem ::= "#parseProgramPath" "(" String ")" // Program Filename - | "#parseProgram" "(" IOString ")" // Program content - | "#collectGrammar" - rule #parseProgramPath(PGM_FILENAME) => #parseProgram(readFile(PGM_FILENAME)) ... - - rule #parseProgram(PGM) - => parseWithProductions(GRAMMAR, "Pgm", PGM) - ... - - GRAMMAR - - rule #collectGrammar ... - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - ( .Set => SetItem(SYNTAXDECL) ) REST - requires notBool(SYNTAXDECL in REST) - rule #collectGrammar => .K ... - #STUCK() => .K ... -endmodule -``` - -Parse Config -------------- - -```k -module PARSE-CONFIG - imports RULES-WITH-BUBBLES-COMMON - imports KINK-CONFIGURATION - imports K-PRODUCTION-ABSTRACT - imports EKORE-KSTRING-ABSTRACT - imports KORE-HELPERS - imports STRING - imports FILE-UTIL - imports PARSER-UTIL - imports KORE-ABSTRACT - imports META-ACCESSORS - - syntax KItem ::= "#parseConfigBubble" - - rule #parseConfigBubble ... - MName - kConfiguration(noAttrs(_:Bubble)) - .Set => #addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")))) - - rule #parseConfigBubble ... - kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) - GRAMMAR - requires GRAMMAR =/=K .Set - - rule #parseConfigBubble => .K ... - #STUCK() => .K ... - - // Add config parsing syntax - // casts: Sort ::= Sort ":Sort" - syntax Set ::= "#addCasts" "(" Set ")" [function] - syntax Set ::= "#addCasts2" "(" Set "," Set ")" [function] - rule #addCasts(Prds) => #addCasts2(Prds, noCastSortsInit) - rule #addCasts2( - SetItem(kSyntaxProduction(SORT, PROD)) - _:Set - (.Set => SetItem( - kSyntaxProduction(SORT, - kProductionWAttr(kProduction(nonTerminal(SORT), - terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), - kAttributesDeclaration(consAttrList( - tagContent(#token("klabel","LowerName"), - String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) - , SORTS (.Set => SetItem(SORT))) - requires notBool SORT in SORTS - rule #addCasts2(Prds, _) => Prds [owise] - - // subsorts: K ::= Sort, Sort ::= KBott - syntax Set ::= "#addSubsorts" "(" Set ")" [function] - syntax Set ::= "#addSubsorts2" "(" Set "," Set ")" [function] - rule #addSubsorts(Prds) => #addSubsorts2(Prds, noLatticeSortsInit) - rule #addSubsorts2( - SetItem(kSyntaxProduction(SORT, PROD)) - _:Set - (.Set => - SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) - SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) - , SORTS (.Set => SetItem(SORT))) - requires notBool SORT in SORTS - rule #addSubsorts2(Prds, _) => Prds [owise] - - // collect config info - destructure the configuration and populate - // with \dv key -> type (CellInfo or KConfigVar) - syntax KItem ::= "#extractConfigInfo" - syntax KItem ::= collectCellName(Patterns) - rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... - kConfiguration(noAttrs(P)) - Configs => Configs SetItem(P) - requires notBool P in Configs - - rule collectCellName( _ { _ } (A)) => collectCellName(A) ... - rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... - rule collectCellName( .Patterns ) => .K ... - - rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... - .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... - - rule #extractConfigInfo => .K ... - #STUCK() => .K ... - -endmodule - -module PARSE-RULE - imports RULES-WITH-BUBBLES-COMMON - imports KINK-CONFIGURATION - imports K-PRODUCTION-ABSTRACT - imports EKORE-KSTRING-ABSTRACT - imports KORE-HELPERS - imports STRING - imports FILE-UTIL - imports PARSER-UTIL - imports KORE-ABSTRACT - imports META-ACCESSORS - imports PARSE-CONFIG - - // parse rule bubbles - syntax KItem ::= "#parseRuleBubble" - rule #parseRuleBubble ... - MName - kRule(noAttrs(_:Bubble)) - .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) - - rule #parseRuleBubble ... - kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) - GRAMMAR - requires GRAMMAR =/=K .Set - rule #parseRuleBubble ... - kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) - GRAMMAR - requires GRAMMAR =/=K .Set - - rule #parseRuleBubble => .K ... - #STUCK() => .K ... - - // add rule cells - syntax Set ::= "#addRuleCells" "(" Set ")" [function] - syntax Set ::= "#addRuleCells2" "(" Set "," Set ")" [function] - rule #addRuleCells(Prds) => #addRuleCells2(Prds, .Set) - rule [[ #addRuleCells2( - Prds:Set - (.Set => SetItem( - kSyntaxProduction(#token("Cell","UpperName"), - kProductionWAttr(kProduction( - terminal(String2EKoreKString("\"<" +String CellName +String ">\"")), kProduction( - nonTerminal(#token("OptionalDots","UpperName")), kProduction( - nonTerminal(#token("K","UpperName")), kProduction( - nonTerminal(#token("OptionalDots","UpperName")), - terminal(String2EKoreKString("\"\"")))))), - kAttributesDeclaration(consAttrList( - tagContent(#token("klabel","LowerName"), String2TagContents(CellName +String "cell")),consAttrList( - tagContent(#token("cellName","LowerName"), String2TagContents(CellName)),consAttrList( - tagSimple(#token("cell","LowerName")), dotAttrList(.KList))))))))) - , Cells (.Set => SetItem(CellName))) - ]] - CellName |-> "CellName" ... - requires notBool CellName in Cells - rule #addRuleCells2(Prods, _) => Prods [owise] - -endmodule -``` - -Parse into EKore ----------------- - -```k -module PARSE-TO-EKORE - imports EKORE-ABSTRACT - imports KINK-CONFIGURATION - imports PARSER-UTIL - - syntax KItem ::= "#parseToEKore" - rule PGM:Any ~> #parseToEKore => parseEKore(tokenToString(PGM)) ... -endmodule -``` - K (frontend) modules to Kore Modules ------------------------------------ diff --git a/src/parser-gen.md b/src/parser-gen.md new file mode 100644 index 0000000..03f523f --- /dev/null +++ b/src/parser-gen.md @@ -0,0 +1,251 @@ +```k +module PARSER-GEN-HELPERS + imports SET + imports STRING-SYNTAX + imports KINK-CONFIGURATION + imports KORE-HELPERS + imports META-ACCESSORS + + syntax UpperName ::= String2UpperName (String) [function, functional, hook(STRING.string2token)] + syntax Set ::= "noCastSortsInit" [function] + rule noCastSortsInit => // sorts from this list do not receive productions for casting + SetItem(String2UpperName("Cell")) + SetItem(String2UpperName("CellName")) + SetItem(String2UpperName("CellProperties")) + SetItem(String2UpperName("CellProperty")) + SetItem(String2UpperName("KConfigVar")) + SetItem(String2UpperName("KLabel")) + SetItem(String2UpperName("KList")) + SetItem(String2UpperName("KString")) + SetItem(String2UpperName("KVariable")) + SetItem(String2UpperName("Layout")) + SetItem(String2UpperName("RuleBody")) + SetItem(String2UpperName("RuleContent")) + SetItem(String2UpperName("OptionalDots")) + syntax Set ::= "noLatticeSortsInit" [function] + rule noLatticeSortsInit => // sorts from this list are not included in the automatic subsorts lattice + SetItem(String2UpperName("Cell")) + SetItem(String2UpperName("CellName")) + SetItem(String2UpperName("CellProperties")) + SetItem(String2UpperName("CellProperty")) + SetItem(String2UpperName("K")) + SetItem(String2UpperName("KBott")) + SetItem(String2UpperName("KConfigVar")) + SetItem(String2UpperName("KLabel")) + SetItem(String2UpperName("KList")) + SetItem(String2UpperName("KString")) + SetItem(String2UpperName("KVariable")) + SetItem(String2UpperName("Layout")) + SetItem(String2UpperName("RuleBody")) + SetItem(String2UpperName("RuleContent")) + SetItem(String2UpperName("OptionalDots")) + + // Add parsing syntax + // casts: Sort ::= Sort ":Sort" + syntax Set ::= "#addCasts" "(" Set ")" [function] + syntax Set ::= "#addCasts2" "(" Set "," Set ")" [function] + rule #addCasts(Prds) => #addCasts2(Prds, noCastSortsInit) + rule #addCasts2( + SetItem(kSyntaxProduction(SORT, PROD)) + _:Set + (.Set => SetItem( + kSyntaxProduction(SORT, + kProductionWAttr(kProduction(nonTerminal(SORT), + terminal(String2EKoreKString("\":" +String token2String(SORT) +String "\""))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), + String2TagContents("SemanticCastTo" +String token2String(SORT))),dotAttrList(.KList))))))) + , SORTS (.Set => SetItem(SORT))) + requires notBool SORT in SORTS + rule #addCasts2(Prds, _) => Prds [owise] + + // subsorts: K ::= Sort, Sort ::= KBott + syntax Set ::= "#addSubsorts" "(" Set ")" [function] + syntax Set ::= "#addSubsorts2" "(" Set "," Set ")" [function] + rule #addSubsorts(Prds) => #addSubsorts2(Prds, noLatticeSortsInit) + rule #addSubsorts2( + SetItem(kSyntaxProduction(SORT, PROD)) + _:Set + (.Set => + SetItem(kSyntaxProduction(String2UpperName("K"), kProductionWAttr(nonTerminal(SORT), noAtt))) + SetItem(kSyntaxProduction(SORT, kProductionWAttr(nonTerminal(String2UpperName("KBott")), noAtt)))) + , SORTS (.Set => SetItem(SORT))) + requires notBool SORT in SORTS + rule #addSubsorts2(Prds, _) => Prds [owise] + +endmodule +``` + +Parse Outer +----------- + +```k +module PARSE-OUTER + imports KINK-CONFIGURATION + imports PARSER-UTIL + + // TODO: remove: #writeStringToFile, #doSystem, #doSystemGetOutput, #doParseAST + syntax KItem ::= "#parseOuter" + rule PGM:Any ~> #parseOuter => parseOuter(tokenToString(PGM)) ... +endmodule +``` + +Parse Program +------------- + +```k +module PARSE-PROGRAM + imports KINK-CONFIGURATION + imports K-PRODUCTION-ABSTRACT + imports EKORE-KSTRING-ABSTRACT + imports KORE-HELPERS + imports STRING + imports FILE-UTIL + imports PARSER-UTIL + + syntax KItem ::= "#parseProgramPath" "(" String ")" // Program Filename + | "#parseProgram" "(" IOString ")" // Program content + | "#collectGrammar" + rule #parseProgramPath(PGM_FILENAME) => #parseProgram(readFile(PGM_FILENAME)) ... + + rule #parseProgram(PGM) + => parseWithProductions(GRAMMAR, "Pgm", PGM) + ... + + GRAMMAR + + rule #collectGrammar ... + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ( .Set => SetItem(SYNTAXDECL) ) REST + requires notBool(SYNTAXDECL in REST) + rule #collectGrammar => .K ... + #STUCK() => .K ... +endmodule +``` + +Parse Config +------------- + +```k +module PARSE-CONFIG + imports RULES-WITH-BUBBLES-COMMON + imports KINK-CONFIGURATION + imports K-PRODUCTION-ABSTRACT + imports EKORE-KSTRING-ABSTRACT + imports KORE-HELPERS + imports STRING + imports FILE-UTIL + imports PARSER-UTIL + imports KORE-ABSTRACT + imports META-ACCESSORS + imports PARSER-GEN-HELPERS + + syntax KItem ::= "#parseConfigBubble" + + rule #parseConfigBubble ... + MName + kConfiguration(noAttrs(_:Bubble)) + .Set => #addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")))) + + rule #parseConfigBubble ... + kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) + GRAMMAR + requires GRAMMAR =/=K .Set + + rule #parseConfigBubble => .K ... + #STUCK() => .K ... + + + // collect config info - destructure the configuration and populate + // with \dv key -> type (CellInfo or KConfigVar) + syntax KItem ::= "#extractConfigInfo" + syntax KItem ::= collectCellName(Patterns) + rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... + kConfiguration(noAttrs(P)) + Configs => Configs SetItem(P) + requires notBool P in Configs + + rule collectCellName( _ { _ } (A)) => collectCellName(A) ... + rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... + rule collectCellName( .Patterns ) => .K ... + + rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... + .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... + + rule #extractConfigInfo => .K ... + #STUCK() => .K ... + +endmodule + +module PARSE-RULE + imports RULES-WITH-BUBBLES-COMMON + imports KINK-CONFIGURATION + imports K-PRODUCTION-ABSTRACT + imports EKORE-KSTRING-ABSTRACT + imports KORE-HELPERS + imports STRING + imports FILE-UTIL + imports PARSER-UTIL + imports KORE-ABSTRACT + imports META-ACCESSORS + imports PARSER-GEN-HELPERS + + // parse rule bubbles + syntax KItem ::= "#parseRuleBubble" + rule #parseRuleBubble ... + MName + kRule(noAttrs(_:Bubble)) + .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) + + rule #parseRuleBubble ... + kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) + GRAMMAR + requires GRAMMAR =/=K .Set + rule #parseRuleBubble ... + kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) + GRAMMAR + requires GRAMMAR =/=K .Set + + rule #parseRuleBubble => .K ... + #STUCK() => .K ... + + // add rule cells + syntax Set ::= "#addRuleCells" "(" Set ")" [function] + syntax Set ::= "#addRuleCells2" "(" Set "," Set ")" [function] + rule #addRuleCells(Prds) => #addRuleCells2(Prds, .Set) + rule [[ #addRuleCells2( + Prds:Set + (.Set => SetItem( + kSyntaxProduction(#token("Cell","UpperName"), + kProductionWAttr(kProduction( + terminal(String2EKoreKString("\"<" +String CellName +String ">\"")), kProduction( + nonTerminal(#token("OptionalDots","UpperName")), kProduction( + nonTerminal(#token("K","UpperName")), kProduction( + nonTerminal(#token("OptionalDots","UpperName")), + terminal(String2EKoreKString("\"\"")))))), + kAttributesDeclaration(consAttrList( + tagContent(#token("klabel","LowerName"), String2TagContents(CellName +String "cell")),consAttrList( + tagContent(#token("cellName","LowerName"), String2TagContents(CellName)),consAttrList( + tagSimple(#token("cell","LowerName")), dotAttrList(.KList))))))))) + , Cells (.Set => SetItem(CellName))) + ]] + CellName |-> "CellName" ... + requires notBool CellName in Cells + rule #addRuleCells2(Prods, _) => Prods [owise] + +endmodule +``` + +Parse into EKore +---------------- + +```k +module PARSE-TO-EKORE + imports EKORE-ABSTRACT + imports KINK-CONFIGURATION + imports PARSER-UTIL + + syntax KItem ::= "#parseToEKore" + rule PGM:Any ~> #parseToEKore => parseEKore(tokenToString(PGM)) ... +endmodule +``` From ab7b3e53709d45e0fa3ecf57f851e3f18aa5a50a Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Wed, 21 Aug 2019 17:50:59 +0300 Subject: [PATCH 16/20] Small refactor and more comments --- src/command-line.md | 10 ++++++---- src/parser-gen.md | 43 ++++++++++++++++++++++++++++++------------- 2 files changed, 36 insertions(+), 17 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 9445d3a..01fdc1a 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -124,13 +124,15 @@ High-level pipeline steps {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String +String tokenToString(PGM) - ) // add config-inner.k - // parse bubbles + ) // collect required files - hardcoded for now ~> #defnToConfig ~> #flattenProductions - ~> #parseConfigBubble + // parse bubbles + ~> #createConfigGrammar + ~> #parseConfigBubbles ~> #extractConfigInfo - ~> #parseRuleBubble + ~> #createRuleGrammar + ~> #parseRuleBubbles DEPLOY_DIR ``` diff --git a/src/parser-gen.md b/src/parser-gen.md index 03f523f..5668002 100644 --- a/src/parser-gen.md +++ b/src/parser-gen.md @@ -5,7 +5,7 @@ module PARSER-GEN-HELPERS imports KINK-CONFIGURATION imports KORE-HELPERS imports META-ACCESSORS - + syntax UpperName ::= String2UpperName (String) [function, functional, hook(STRING.string2token)] syntax Set ::= "noCastSortsInit" [function] rule noCastSortsInit => // sorts from this list do not receive productions for casting @@ -39,9 +39,11 @@ module PARSER-GEN-HELPERS SetItem(String2UpperName("RuleBody")) SetItem(String2UpperName("RuleContent")) SetItem(String2UpperName("OptionalDots")) - + // Add parsing syntax // casts: Sort ::= Sort ":Sort" + // expecting a list of productions as argument and returns a new list with added cast for each sort found + // except for `noCastSortsInit` syntax Set ::= "#addCasts" "(" Set ")" [function] syntax Set ::= "#addCasts2" "(" Set "," Set ")" [function] rule #addCasts(Prds) => #addCasts2(Prds, noCastSortsInit) @@ -58,7 +60,7 @@ module PARSER-GEN-HELPERS , SORTS (.Set => SetItem(SORT))) requires notBool SORT in SORTS rule #addCasts2(Prds, _) => Prds [owise] - + // subsorts: K ::= Sort, Sort ::= KBott syntax Set ::= "#addSubsorts" "(" Set ")" [function] syntax Set ::= "#addSubsorts2" "(" Set "," Set ")" [function] @@ -140,19 +142,25 @@ module PARSE-CONFIG imports META-ACCESSORS imports PARSER-GEN-HELPERS - syntax KItem ::= "#parseConfigBubble" + syntax KItem ::= "#parseConfigBubbles" + | "#createConfigGrammar" - rule #parseConfigBubble ... + // create config grammar in modules where we find configs as bubbles + rule #createConfigGrammar ... MName kConfiguration(noAttrs(_:Bubble)) .Set => #addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("CONFIG-INNER", "UpperName")))) - rule #parseConfigBubble ... + rule #createConfigGrammar => .K ... + #STUCK() => .K ... + + // actually parsing the configuration once we have the grammar + rule #parseConfigBubbles ... kConfiguration(noAttrs(C:Bubble)) => kConfiguration(noAttrs({parseWithProductions(GRAMMAR, "K", tokenToString(C))}:>Pattern)) GRAMMAR requires GRAMMAR =/=K .Set - rule #parseConfigBubble => .K ... + rule #parseConfigBubbles => .K ... #STUCK() => .K ... @@ -191,22 +199,31 @@ module PARSE-RULE imports PARSER-GEN-HELPERS // parse rule bubbles - syntax KItem ::= "#parseRuleBubble" - rule #parseRuleBubble ... + syntax KItem ::= "#parseRuleBubbles" + | "#createRuleGrammar" + + rule #createRuleGrammar ... // create rule grammar MName kRule(noAttrs(_:Bubble)) .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) - - rule #parseRuleBubble ... + rule #createRuleGrammar ... // create rule grammar for rules with attributes + MName + kRule(attrs(_:Bubble, _)) + .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) + + rule #createRuleGrammar => .K ... + #STUCK() => .K ... + + rule #parseRuleBubbles ... kRule(noAttrs(C:Bubble)) => kRule(noAttrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern)) GRAMMAR requires GRAMMAR =/=K .Set - rule #parseRuleBubble ... + rule #parseRuleBubbles ... kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) GRAMMAR requires GRAMMAR =/=K .Set - rule #parseRuleBubble => .K ... + rule #parseRuleBubbles => .K ... #STUCK() => .K ... // add rule cells From a0f2b352498388d857721dfd478a8d3bc06de496 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 29 Aug 2019 15:17:46 +0300 Subject: [PATCH 17/20] Update parse program pipeline --- src/command-line.md | 8 ++++---- src/kink.md | 2 +- src/parser-gen.md | 16 +++++++++------- t/foobar/foobar.k | 6 +++++- t/peano/peano.k | 5 ++++- 5 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 01fdc1a..847d867 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -98,12 +98,12 @@ High-level pipeline steps ========================= ```k - syntax K ::= "#kastPipeline" "(" String ")" [function] - rule #kastPipeline(PATH) - => #parseOuter + syntax K ::= "#kastPipeline" "(" String ")" //[function] + rule PGM:Any ~> #kastPipeline(PATH:String) + => parseOuter(tokenToString(PGM)) ~> #defnToConfig ~> #flattenProductions - ~> #collectGrammar + ~> #collectPgmGrammar ~> #parseProgramPath(PATH) ~> #success diff --git a/src/kink.md b/src/kink.md index 0614c62..e3db025 100644 --- a/src/kink.md +++ b/src/kink.md @@ -45,8 +45,8 @@ module KINK-CONFIGURATION nullDecl - .Set + .Set // place to collect the grammar used to parse programs .Set // place to collect the grammar used to parse configurations .Set // place to collect the grammar used to parse rules diff --git a/src/parser-gen.md b/src/parser-gen.md index 5668002..c370291 100644 --- a/src/parser-gen.md +++ b/src/parser-gen.md @@ -104,23 +104,25 @@ module PARSE-PROGRAM imports STRING imports FILE-UTIL imports PARSER-UTIL + imports META-ACCESSORS syntax KItem ::= "#parseProgramPath" "(" String ")" // Program Filename | "#parseProgram" "(" IOString ")" // Program content - | "#collectGrammar" + | "#collectPgmGrammar" rule #parseProgramPath(PGM_FILENAME) => #parseProgram(readFile(PGM_FILENAME)) ... rule #parseProgram(PGM) => parseWithProductions(GRAMMAR, "Pgm", PGM) ... - GRAMMAR + GRAMMAR + requires GRAMMAR =/=K .Set - rule #collectGrammar ... - kSyntaxProduction(SORT, PROD) #as SYNTAXDECL - ( .Set => SetItem(SYNTAXDECL) ) REST - requires notBool(SYNTAXDECL in REST) - rule #collectGrammar => .K ... + rule #collectPgmGrammar ... + MName + .Set => #getAllProds(MName) + requires findString(tokenToString(MName), "-SYNTAX", 0) =/=Int -1 + rule #collectPgmGrammar => .K ... #STUCK() => .K ... endmodule ``` diff --git a/t/foobar/foobar.k b/t/foobar/foobar.k index 2c61693..1fc33df 100644 --- a/t/foobar/foobar.k +++ b/t/foobar/foobar.k @@ -1,8 +1,12 @@ -module FOOBAR +module FOOBAR-SYNTAX syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] syntax Pgm ::= Foo syntax Foo ::= "bar" [klabel(bar), function] | "buzz" [klabel(buzz)] +endmodule + +module FOOBAR + imports FOOBAR-SYNTAX rule bar => buzz endmodule diff --git a/t/peano/peano.k b/t/peano/peano.k index 3432070..5c5c8c0 100644 --- a/t/peano/peano.k +++ b/t/peano/peano.k @@ -1,11 +1,14 @@ -module PEANO +module PEANO-SYNTAX syntax Pgm ::= Nat syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] syntax Nat ::= "zero" [klabel(zero)] | succ(Nat) [klabel(succ)] | plus(Nat, Nat) [function, klabel(plus)] +endmodule +module PEANO + imports PEANO-SYNTAX rule plus(zero, Y:Nat) => Y rule plus(succ(X:Nat), Y:Nat) => succ(plus(X, Y)) endmodule From 571b806efa14fd0fc3fe822305c562a41d166589 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Sat, 31 Aug 2019 16:34:29 +0300 Subject: [PATCH 18/20] Renaming example --- src/inner.md | 6 + src/kink.md | 2 +- t/config/expected.ekore | 8 - t/inner-parsing/expected.ekore | 658 ++++++++++++++++++ .../inner-parsing.k} | 2 +- 5 files changed, 666 insertions(+), 10 deletions(-) delete mode 100644 t/config/expected.ekore create mode 100644 t/inner-parsing/expected.ekore rename t/{config/config.k => inner-parsing/inner-parsing.k} (93%) diff --git a/src/inner.md b/src/inner.md index e70539a..410e9a7 100644 --- a/src/inner.md +++ b/src/inner.md @@ -165,6 +165,12 @@ module REQUIRES-ENSURES | RuleBody "requires" K "ensures" K [klabel("ruleRequiresEnsures")] endmodule +module DEFAULT-CONFIGURATION + imports BASIC-K + + configuration $PGM:K +endmodule + // To be used to parse semantic rules module K imports KSEQ-SYMBOLIC diff --git a/src/kink.md b/src/kink.md index e3db025..a3b1d60 100644 --- a/src/kink.md +++ b/src/kink.md @@ -45,7 +45,7 @@ module KINK-CONFIGURATION nullDecl - + .Set // place to collect the grammar used to parse programs .Set // place to collect the grammar used to parse configurations .Set // place to collect the grammar used to parse rules diff --git a/t/config/expected.ekore b/t/config/expected.ekore deleted file mode 100644 index 3fee2de..0000000 --- a/t/config/expected.ekore +++ /dev/null @@ -1,8 +0,0 @@ -module FOOBAR - configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) - rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToFoo { .Sorts } ( \dv { KVariable { .Sorts } } ( "A" ) , .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) - syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] - syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] - syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] - syntax Pgm ::= Foo noAtt -endmodule [ .Patterns ] diff --git a/t/inner-parsing/expected.ekore b/t/inner-parsing/expected.ekore new file mode 100644 index 0000000..c39b919 --- /dev/null +++ b/t/inner-parsing/expected.ekore @@ -0,0 +1,658 @@ + + + . + + + [ .Patterns ] + + module AUTO-CASTS + .DeclCellSet + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module AUTO-FOLLOW + .DeclCellSet + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module BASIC-K + import SORT-K [ .Patterns ] + syntax KConfigVar [ token , .AttrList ] + syntax KItem noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module CONFIG-CELLS + import KCELLS [ .Patterns ] + import RULE-LISTS [ .Patterns ] + syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] + syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] + syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] + syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] + syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] + syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module CONFIG-INNER + import CONFIG-CELLS [ .Patterns ] + import DEFAULT-LAYOUT [ .Patterns ] + import K-TERM [ .Patterns ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module DEFAULT-CONFIGURATION + configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToK { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) + import BASIC-K [ .Patterns ] + + /* + + + .Set + + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] ) + SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] ) + SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] ) + SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] ) + SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] ) + SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + .Set + + + */ + + + endmodule [ .Patterns ] + + module DEFAULT-LAYOUT + syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module INNER-PARSING + configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) + rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToFoo { .Sorts } ( \dv { KVariable { .Sorts } } ( "A" ) , .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) + syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] + syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] + syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] + syntax Pgm ::= Foo noAtt + + /* + + + .Set + + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] ) + SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] ) + SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] ) + SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] ) + SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] ) + SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] ) + SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] ) + SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] ) + SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) , .AttrList ] ) + SetItem ( syntax Foo ::= KBott noAtt ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= Foo noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax K ::= Pgm noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( Tcell ) , cellName ( T ) , cell , .AttrList ] ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( envcell ) , cellName ( env ) , cell , .AttrList ] ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( kcell ) , cellName ( k ) , cell , .AttrList ] ) + SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] ) + SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] ) + SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) , .AttrList ] ) + SetItem ( syntax Foo ::= KBott noAtt ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= Foo noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax K ::= Pgm noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) + SetItem ( syntax KBott ::= K "=>" K [ klabel ( KRewrite ) , .AttrList ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + */ + + + endmodule [ .Patterns ] + + module K + import AUTO-CASTS [ .Patterns ] + import AUTO-FOLLOW [ .Patterns ] + import K-SORT-LATTICE [ .Patterns ] + import KSEQ-SYMBOLIC [ .Patterns ] + import REQUIRES-ENSURES [ .Patterns ] + syntax KBott ::= K "=>" K [ klabel ( KRewrite ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module K-SORT-LATTICE + import SORT-KBOTT [ .Patterns ] + syntax K ::= KItem noAtt + syntax KItem ::= KBott noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module K-TERM + import AUTO-CASTS [ .Patterns ] + import AUTO-FOLLOW [ .Patterns ] + import K-SORT-LATTICE [ .Patterns ] + import KSEQ-SYMBOLIC [ .Patterns ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module KAST + import BASIC-K [ .Patterns ] + import KSTRING [ .Patterns ] + import SORT-KBOTT [ .Patterns ] + syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] + syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] + syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] + syntax KLabel ::= regexTerminal ( "(? + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module KCELLS + import KAST [ .Patterns ] + syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] + syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] + syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] + syntax Bag ::= Cell noAtt + syntax Cell noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module KSEQ + import KAST [ .Patterns ] + syntax KBott ::= "(" K ")" [ bracket , .AttrList ] + syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] + syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module KSEQ-SYMBOLIC + import KSEQ [ .Patterns ] + syntax KBott ::= KConfigVar noAtt + syntax KBott ::= KVariable noAtt + syntax KConfigVar ::= regexTerminal ( "(? + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module KSTRING + syntax KString ::= regexTerminal ( "[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" ) [ token , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module REQUIRES-ENSURES + import BASIC-K [ .Patterns ] + syntax RuleBody ::= K noAtt + syntax RuleContent ::= RuleBody "ensures" K [ klabel ( "ruleEnsures" ) , .AttrList ] + syntax RuleContent ::= RuleBody "requires" K "ensures" K [ klabel ( "ruleRequiresEnsures" ) , .AttrList ] + syntax RuleContent ::= RuleBody "requires" K [ klabel ( "ruleRequires" ) , .AttrList ] + syntax RuleContent ::= RuleBody [ klabel ( "ruleNoConditions" ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module RULE-CELLS + import KCELLS [ .Patterns ] + import RULE-LISTS [ .Patterns ] + syntax OptionalDots ::= "" [ klabel ( noDots ) , .AttrList ] + syntax OptionalDots ::= "..." [ klabel ( dots ) , .AttrList ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module RULE-INNER + import DEFAULT-LAYOUT [ .Patterns ] + import K [ .Patterns ] + import RULE-CELLS [ .Patterns ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module RULE-LISTS + .DeclCellSet + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module SORT-K + syntax K noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + module SORT-KBOTT + import SORT-K [ .Patterns ] + syntax KBott noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + + endmodule [ .Patterns ] + + + + + + "$PGM" |-> "KConfigVar" + "T" |-> "CellName" + "env" |-> "CellName" + "k" |-> "CellName" + + + SetItem ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) ) + SetItem ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToK { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) ) + + + + + 1 + + + #STUCK ( ) ~> ^ regular + + + "/home/radu/work/k-in-k/.build/kink/" + + diff --git a/t/config/config.k b/t/inner-parsing/inner-parsing.k similarity index 93% rename from t/config/config.k rename to t/inner-parsing/inner-parsing.k index 2f83a86..8de3c52 100644 --- a/t/config/config.k +++ b/t/inner-parsing/inner-parsing.k @@ -1,4 +1,4 @@ -module FOOBAR +module INNER-PARSING syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] syntax Pgm ::= Foo From 23f32052bb8a3ec0a890046d096b9117dc22ffd1 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Mon, 2 Sep 2019 19:39:39 +0300 Subject: [PATCH 19/20] Fixing build system and adding inner-parsing test --- build | 12 +- lib/kore-from-config | 4 +- src/command-line.md | 7 +- src/kink.md | 4 +- t/inner-parsing/expected.ekore | 658 --------------------------------- t/inner-parsing/parsed.ekore | 623 +++++++++++++++++++++++++++++++ 6 files changed, 639 insertions(+), 669 deletions(-) delete mode 100644 t/inner-parsing/expected.ekore create mode 100644 t/inner-parsing/parsed.ekore diff --git a/build b/build index a0790bd..80094e3 100755 --- a/build +++ b/build @@ -70,9 +70,9 @@ def pipeline(commandline, extension): flags = "-cCOMMANDLINE='%s' -cKINKDEPLOYEDDIR=%s" % (commandline, kink.directory())) -def kink_test(base_dir, test_file, pipeline): +def kink_test(base_dir, test_file, expected_file, pipeline): input = path.join(base_dir, test_file) - expected = path.join(base_dir, 'expected.ekore') + expected = path.join(base_dir, expected_file) return proj.source(input) \ .then(pipeline) \ .then(kore_from_config) \ @@ -80,7 +80,8 @@ def kink_test(base_dir, test_file, pipeline): .variables(flags = '--ignore-all-space --ignore-blank-lines')) \ .default() -ekore_test = functools.partial(kink_test, pipeline = pipeline('ekore-to-kore' , 'ekorePipeline')) +ekore_test = functools.partial(kink_test, expected_file = 'expected.ekore', pipeline = pipeline('ekore-to-kore', 'ekorePipeline')) +frontend_test = functools.partial(kink_test, expected_file = 'parsed.ekore', pipeline = pipeline('frontend-to-ekore', 'frontendPipeline')) def parse_test(base_dir, def_file, input_program): def_path = path.join(base_dir, def_file) @@ -137,4 +138,9 @@ imp_tests += [ lang_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ] imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ] proj.build('t/imp', 'phony', inputs = Target.to_paths(imp_tests)) +# Inner parsing +inner_tests = [] +inner_tests += [ frontend_test('t/inner-parsing', 'inner-parsing.k') ] +proj.build('t/inner-parsing', 'phony', inputs = Target.to_paths(inner_tests)) + proj.main() diff --git a/lib/kore-from-config b/lib/kore-from-config index 5c5db85..8787c27 100755 --- a/lib/kore-from-config +++ b/lib/kore-from-config @@ -23,14 +23,12 @@ kore = input[begin.end():end.start()] # Remove unwanted units from Lists etc. commaSeparated = ['AttrList', 'KoreNames', 'Names', 'Patterns', 'Sorts'] -others = ['Modules', 'Declarations', 'KImportList', 'TagContents'] +others = ['Modules', 'Declarations', 'KImportList', 'TagContents', 'DeclCellSet' ] for listSort in commaSeparated: kore = kore.replace(' , .' + listSort, '') for listSort in commaSeparated + others: kore = kore.replace('.' + listSort, '') kore = re.sub(r' *\n *\.\n *\n', '', kore) -kore = re.sub(r' *.*\n', '', kore) -kore = re.sub(r' *\n.*\n *\n', '', kore) # '.' doesn't match new lines?! outfile = open(out_file, 'w') for line in kore.split("\n")[1:-1]: diff --git a/src/command-line.md b/src/command-line.md index 847d867..3994c68 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -98,7 +98,7 @@ High-level pipeline steps ========================= ```k - syntax K ::= "#kastPipeline" "(" String ")" //[function] + syntax K ::= "#kastPipeline" "(" String ")" rule PGM:Any ~> #kastPipeline(PATH:String) => parseOuter(tokenToString(PGM)) ~> #defnToConfig @@ -107,7 +107,7 @@ High-level pipeline steps ~> #parseProgramPath(PATH) ~> #success - syntax K ::= "#ekorePipeline" [function] + syntax K ::= "#ekorePipeline" rule #ekorePipeline => #parseToEKore ~> #defnToConfig @@ -118,7 +118,7 @@ High-level pipeline steps ~> #translateRules ~> #success - syntax K ::= "#frontendPipeline" //[function] + syntax K ::= "#frontendPipeline" rule PGM:Any ~> #frontendPipeline => parseOuter( {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String @@ -133,6 +133,7 @@ High-level pipeline steps ~> #extractConfigInfo ~> #createRuleGrammar ~> #parseRuleBubbles + ~> #success DEPLOY_DIR ``` diff --git a/src/kink.md b/src/kink.md index a3b1d60..7e7e6e2 100644 --- a/src/kink.md +++ b/src/kink.md @@ -38,7 +38,7 @@ module KINK-CONFIGURATION .Patterns - #token("UNNAMED", "ModuleName"):ModuleName .Patterns @@ -52,7 +52,7 @@ module KINK-CONFIGURATION - + .Map .Set diff --git a/t/inner-parsing/expected.ekore b/t/inner-parsing/expected.ekore deleted file mode 100644 index c39b919..0000000 --- a/t/inner-parsing/expected.ekore +++ /dev/null @@ -1,658 +0,0 @@ - - - . - - - [ .Patterns ] - - module AUTO-CASTS - .DeclCellSet - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module AUTO-FOLLOW - .DeclCellSet - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module BASIC-K - import SORT-K [ .Patterns ] - syntax KConfigVar [ token , .AttrList ] - syntax KItem noAtt - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module CONFIG-CELLS - import KCELLS [ .Patterns ] - import RULE-LISTS [ .Patterns ] - syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] - syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] - syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] - syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] - syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] - syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module CONFIG-INNER - import CONFIG-CELLS [ .Patterns ] - import DEFAULT-LAYOUT [ .Patterns ] - import K-TERM [ .Patterns ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module DEFAULT-CONFIGURATION - configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToK { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) - import BASIC-K [ .Patterns ] - - /* - - - .Set - - - SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) - SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Cell noAtt ) - SetItem ( syntax Bag ::= KBott noAtt ) - SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] ) - SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] ) - SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] ) - SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] ) - SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] ) - SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] ) - SetItem ( syntax K ::= Bag noAtt ) - SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) - SetItem ( syntax K ::= KItem noAtt ) - SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) - SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) - SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) - SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) - SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) - SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) - SetItem ( syntax KBott ::= KConfigVar noAtt ) - SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) - SetItem ( syntax KBott ::= KVariable noAtt ) - SetItem ( syntax KConfigVar ::= regexTerminal ( "(? - - .Set - - - */ - - - endmodule [ .Patterns ] - - module DEFAULT-LAYOUT - syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module INNER-PARSING - configuration configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) - rule ruleNoConditions { .Sorts } ( KRewrite { .Sorts } ( SemanticCastToFoo { .Sorts } ( \dv { KVariable { .Sorts } } ( "A" ) , .Patterns ) , ( emptyK { .Sorts } ( .Patterns ) , .Patterns ) ) , .Patterns ) - syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] - syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] - syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) , .AttrList ] - syntax Pgm ::= Foo noAtt - - /* - - - .Set - - - SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) - SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Cell noAtt ) - SetItem ( syntax Bag ::= KBott noAtt ) - SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) , .AttrList ] ) - SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) , .AttrList ] ) - SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token , .AttrList ] ) - SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) , .AttrList ] ) - SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) , .AttrList ] ) - SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) , .AttrList ] ) - SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] ) - SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] ) - SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) , .AttrList ] ) - SetItem ( syntax Foo ::= KBott noAtt ) - SetItem ( syntax K ::= Bag noAtt ) - SetItem ( syntax K ::= Foo noAtt ) - SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) - SetItem ( syntax K ::= KItem noAtt ) - SetItem ( syntax K ::= Pgm noAtt ) - SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) - SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) - SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) - SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) - SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) - SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) - SetItem ( syntax KBott ::= KConfigVar noAtt ) - SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) - SetItem ( syntax KBott ::= KVariable noAtt ) - SetItem ( syntax KConfigVar ::= regexTerminal ( "(? - - SetItem ( syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] ) - SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) , .AttrList ] ) - SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] ) - SetItem ( syntax Bag ::= Cell noAtt ) - SetItem ( syntax Bag ::= KBott noAtt ) - SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( Tcell ) , cellName ( T ) , cell , .AttrList ] ) - SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( envcell ) , cellName ( env ) , cell , .AttrList ] ) - SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( kcell ) , cellName ( k ) , cell , .AttrList ] ) - SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function , .AttrList ] ) - SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) , .AttrList ] ) - SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) , .AttrList ] ) - SetItem ( syntax Foo ::= KBott noAtt ) - SetItem ( syntax K ::= Bag noAtt ) - SetItem ( syntax K ::= Foo noAtt ) - SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) , .AttrList ] ) - SetItem ( syntax K ::= KItem noAtt ) - SetItem ( syntax K ::= Pgm noAtt ) - SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] ) - SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] ) - SetItem ( syntax KBott ::= "(" K ")" [ bracket , .AttrList ] ) - SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] ) - SetItem ( syntax KBott ::= K "=>" K [ klabel ( KRewrite ) , .AttrList ] ) - SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] ) - SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) , .AttrList ] ) - SetItem ( syntax KBott ::= KConfigVar noAtt ) - SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] ) - SetItem ( syntax KBott ::= KVariable noAtt ) - SetItem ( syntax KConfigVar ::= regexTerminal ( "(? - - */ - - - endmodule [ .Patterns ] - - module K - import AUTO-CASTS [ .Patterns ] - import AUTO-FOLLOW [ .Patterns ] - import K-SORT-LATTICE [ .Patterns ] - import KSEQ-SYMBOLIC [ .Patterns ] - import REQUIRES-ENSURES [ .Patterns ] - syntax KBott ::= K "=>" K [ klabel ( KRewrite ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module K-SORT-LATTICE - import SORT-KBOTT [ .Patterns ] - syntax K ::= KItem noAtt - syntax KItem ::= KBott noAtt - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module K-TERM - import AUTO-CASTS [ .Patterns ] - import AUTO-FOLLOW [ .Patterns ] - import K-SORT-LATTICE [ .Patterns ] - import KSEQ-SYMBOLIC [ .Patterns ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module KAST - import BASIC-K [ .Patterns ] - import KSTRING [ .Patterns ] - import SORT-KBOTT [ .Patterns ] - syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) , .AttrList ] - syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) , .AttrList ] - syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) , .AttrList ] - syntax KLabel ::= regexTerminal ( "(? - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module KCELLS - import KAST [ .Patterns ] - syntax Bag ::= "(" Bag ")" [ bracket , .AttrList ] - syntax Bag ::= ".Bag" [ klabel ( cells ) , .AttrList ] - syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) , .AttrList ] - syntax Bag ::= Cell noAtt - syntax Cell noAtt - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module KSEQ - import KAST [ .Patterns ] - syntax KBott ::= "(" K ")" [ bracket , .AttrList ] - syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid , .AttrList ] - syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module KSEQ-SYMBOLIC - import KSEQ [ .Patterns ] - syntax KBott ::= KConfigVar noAtt - syntax KBott ::= KVariable noAtt - syntax KConfigVar ::= regexTerminal ( "(? - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module KSTRING - syntax KString ::= regexTerminal ( "[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" ) [ token , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module REQUIRES-ENSURES - import BASIC-K [ .Patterns ] - syntax RuleBody ::= K noAtt - syntax RuleContent ::= RuleBody "ensures" K [ klabel ( "ruleEnsures" ) , .AttrList ] - syntax RuleContent ::= RuleBody "requires" K "ensures" K [ klabel ( "ruleRequiresEnsures" ) , .AttrList ] - syntax RuleContent ::= RuleBody "requires" K [ klabel ( "ruleRequires" ) , .AttrList ] - syntax RuleContent ::= RuleBody [ klabel ( "ruleNoConditions" ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module RULE-CELLS - import KCELLS [ .Patterns ] - import RULE-LISTS [ .Patterns ] - syntax OptionalDots ::= "" [ klabel ( noDots ) , .AttrList ] - syntax OptionalDots ::= "..." [ klabel ( dots ) , .AttrList ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module RULE-INNER - import DEFAULT-LAYOUT [ .Patterns ] - import K [ .Patterns ] - import RULE-CELLS [ .Patterns ] - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module RULE-LISTS - .DeclCellSet - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module SORT-K - syntax K noAtt - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - module SORT-KBOTT - import SORT-K [ .Patterns ] - syntax KBott noAtt - - /* - - - .Set - - - .Set - - - .Set - - - */ - - - endmodule [ .Patterns ] - - - - - - "$PGM" |-> "KConfigVar" - "T" |-> "CellName" - "env" |-> "CellName" - "k" |-> "CellName" - - - SetItem ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "T" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , cells { .Sorts } ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToPgm { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) , ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "env" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , emptyK { .Sorts } ( .Patterns ) , \dv { CellName { .Sorts } } ( "env" ) , .Patterns ) ) , .Patterns ) ) , \dv { CellName { .Sorts } } ( "T" ) , .Patterns ) ) ) - SetItem ( configCell { .Sorts } ( \dv { CellName { .Sorts } } ( "k" ) , ( cellPropertyListTerminator { .Sorts } ( .Patterns ) , SemanticCastToK { .Sorts } ( \dv { KConfigVar { .Sorts } } ( "$PGM" ) , .Patterns ) , \dv { CellName { .Sorts } } ( "k" ) , .Patterns ) ) ) - - - - - 1 - - - #STUCK ( ) ~> ^ regular - - - "/home/radu/work/k-in-k/.build/kink/" - - diff --git a/t/inner-parsing/parsed.ekore b/t/inner-parsing/parsed.ekore new file mode 100644 index 0000000..e9d79ad --- /dev/null +++ b/t/inner-parsing/parsed.ekore @@ -0,0 +1,623 @@ + [ ] + + module AUTO-CASTS + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module AUTO-FOLLOW + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module BASIC-K + import SORT-K [ ] + syntax KConfigVar [ token ] + syntax KItem noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module CONFIG-CELLS + import KCELLS [ ] + import RULE-LISTS [ ] + syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) ] + syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) ] + syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token ] + syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) ] + syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) ] + syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module CONFIG-INNER + import CONFIG-CELLS [ ] + import DEFAULT-LAYOUT [ ] + import K-TERM [ ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module DEFAULT-CONFIGURATION + configuration configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) + import BASIC-K [ ] + + /* + + + .Set + + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) ] ) + SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) ] ) + SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token ] ) + SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) ] ) + SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) ] ) + SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) ] ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + .Set + + + */ + + endmodule [ ] + + module DEFAULT-LAYOUT + syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module INNER-PARSING + configuration configCell { } ( \dv { CellName { } } ( "T" ) , ( cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) , ( configCell { } ( \dv { CellName { } } ( "env" ) , ( cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) ) ) , \dv { CellName { } } ( "T" ) ) ) + rule ruleNoConditions { } ( KRewrite { } ( SemanticCastToFoo { } ( \dv { KVariable { } } ( "A" ) ) , ( emptyK { } ( ) ) ) ) + syntax Foo ::= "bar" [ klabel ( bar ) , function ] + syntax Foo ::= "buzz" [ klabel ( buzz ) ] + syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) ] + syntax Pgm ::= Foo noAtt + + /* + + + .Set + + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "<" CellName "/>" [ klabel ( externalCell ) ] ) + SetItem ( syntax Cell ::= "<" CellName CellProperties ">" K "" [ klabel ( configCell ) ] ) + SetItem ( syntax CellName ::= regexTerminal ( "[a-zA-Z][A-Za-z0-9'_]*" ) [ token ] ) + SetItem ( syntax CellProperties ::= "" [ klabel ( cellPropertyListTerminator ) ] ) + SetItem ( syntax CellProperties ::= CellProperty CellProperties [ klabel ( cellPropertyList ) ] ) + SetItem ( syntax CellProperty ::= CellName "=" KString [ klabel ( cellProperty ) ] ) + SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function ] ) + SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) ] ) + SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) ] ) + SetItem ( syntax Foo ::= KBott noAtt ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= Foo noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax K ::= Pgm noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + SetItem ( syntax Bag ::= "(" Bag ")" [ bracket ] ) + SetItem ( syntax Bag ::= ".Bag" [ klabel ( cells ) ] ) + SetItem ( syntax Bag ::= Bag ":Bag" [ klabel ( SemanticCastToBag ) ] ) + SetItem ( syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) ] ) + SetItem ( syntax Bag ::= Cell noAtt ) + SetItem ( syntax Bag ::= KBott noAtt ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( Tcell ) , cellName ( T ) , cell ] ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( envcell ) , cellName ( env ) , cell ] ) + SetItem ( syntax Cell ::= "" OptionalDots K OptionalDots "" [ klabel ( kcell ) , cellName ( k ) , cell ] ) + SetItem ( syntax Foo ::= "bar" [ klabel ( bar ) , function ] ) + SetItem ( syntax Foo ::= "buzz" [ klabel ( buzz ) ] ) + SetItem ( syntax Foo ::= Foo ":Foo" [ klabel ( SemanticCastToFoo ) ] ) + SetItem ( syntax Foo ::= KBott noAtt ) + SetItem ( syntax K ::= Bag noAtt ) + SetItem ( syntax K ::= Foo noAtt ) + SetItem ( syntax K ::= K ":K" [ klabel ( SemanticCastToK ) ] ) + SetItem ( syntax K ::= KItem noAtt ) + SetItem ( syntax K ::= Pgm noAtt ) + SetItem ( syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) ] ) + SetItem ( syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) ] ) + SetItem ( syntax KBott ::= "(" K ")" [ bracket ] ) + SetItem ( syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid ] ) + SetItem ( syntax KBott ::= K "=>" K [ klabel ( KRewrite ) ] ) + SetItem ( syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) ] ) + SetItem ( syntax KBott ::= KBott ":KBott" [ klabel ( SemanticCastToKBott ) ] ) + SetItem ( syntax KBott ::= KConfigVar noAtt ) + SetItem ( syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) ] ) + SetItem ( syntax KBott ::= KVariable noAtt ) + SetItem ( syntax KConfigVar ::= regexTerminal ( "(? + + */ + + endmodule [ ] + + module K + import AUTO-CASTS [ ] + import AUTO-FOLLOW [ ] + import K-SORT-LATTICE [ ] + import KSEQ-SYMBOLIC [ ] + import REQUIRES-ENSURES [ ] + syntax KBott ::= K "=>" K [ klabel ( KRewrite ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module K-SORT-LATTICE + import SORT-KBOTT [ ] + syntax K ::= KItem noAtt + syntax KItem ::= KBott noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module K-TERM + import AUTO-CASTS [ ] + import AUTO-FOLLOW [ ] + import K-SORT-LATTICE [ ] + import KSEQ-SYMBOLIC [ ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module KAST + import BASIC-K [ ] + import KSTRING [ ] + import SORT-KBOTT [ ] + syntax KBott ::= "#klabel" "(" KLabel ")" [ klabel ( wrappedKLabel ) ] + syntax KBott ::= "#token" "(" KString "," KString ")" [ klabel ( kToken ) ] + syntax KBott ::= KLabel "(" KList ")" [ klabel ( kApply ) ] + syntax KLabel ::= regexTerminal ( "(? + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module KCELLS + import KAST [ ] + syntax Bag ::= "(" Bag ")" [ bracket ] + syntax Bag ::= ".Bag" [ klabel ( cells ) ] + syntax Bag ::= Bag Bag [ left , assoc , klabel ( cells ) , unit ( cells ) ] + syntax Bag ::= Cell noAtt + syntax Cell noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module KSEQ + import KAST [ ] + syntax KBott ::= "(" K ")" [ bracket ] + syntax KBott ::= ".K" [ klabel ( emptyK ) , unparseAvoid ] + syntax KBott ::= K "~>" K [ klabel ( kSequence ) , left , assoc , unit ( emptyK ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module KSEQ-SYMBOLIC + import KSEQ [ ] + syntax KBott ::= KConfigVar noAtt + syntax KBott ::= KVariable noAtt + syntax KConfigVar ::= regexTerminal ( "(? + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module KSTRING + syntax KString ::= regexTerminal ( "[\\\"](([^\\\"\n\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]" ) [ token ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module REQUIRES-ENSURES + import BASIC-K [ ] + syntax RuleBody ::= K noAtt + syntax RuleContent ::= RuleBody "ensures" K [ klabel ( "ruleEnsures" ) ] + syntax RuleContent ::= RuleBody "requires" K "ensures" K [ klabel ( "ruleRequiresEnsures" ) ] + syntax RuleContent ::= RuleBody "requires" K [ klabel ( "ruleRequires" ) ] + syntax RuleContent ::= RuleBody [ klabel ( "ruleNoConditions" ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module RULE-CELLS + import KCELLS [ ] + import RULE-LISTS [ ] + syntax OptionalDots ::= "" [ klabel ( noDots ) ] + syntax OptionalDots ::= "..." [ klabel ( dots ) ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module RULE-INNER + import DEFAULT-LAYOUT [ ] + import K [ ] + import RULE-CELLS [ ] + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module RULE-LISTS + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module SORT-K + syntax K noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + module SORT-KBOTT + import SORT-K [ ] + syntax KBott noAtt + + /* + + + .Set + + + .Set + + + .Set + + + */ + + endmodule [ ] + + + + /* + + + "$PGM" |-> "KConfigVar" + "T" |-> "CellName" + "env" |-> "CellName" + "k" |-> "CellName" + + + SetItem ( configCell { } ( \dv { CellName { } } ( "T" ) , ( cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) , ( configCell { } ( \dv { CellName { } } ( "env" ) , ( cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) ) ) , \dv { CellName { } } ( "T" ) ) ) ) + SetItem ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) ) + + + + */ From f5d2a5135b49197b5dc823287ae58c4f32a534f1 Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Thu, 5 Sep 2019 15:27:57 +0300 Subject: [PATCH 20/20] Work around pretty-printing issue --- src/kore.md | 3 +-- src/parser-gen.md | 9 +++++---- t/inner-parsing/parsed.ekore | 10 +++++----- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/kore.md b/src/kore.md index cad7016..33f057e 100644 --- a/src/kore.md +++ b/src/kore.md @@ -119,8 +119,7 @@ module KORE-ABSTRACT | Sort "," Sorts [klabel(consSorts)] | ".Sorts" [klabel(dotSorts )] - syntax Patterns ::= Pattern - | Pattern "," Patterns [klabel(consPatterns)] + syntax Patterns ::= Pattern "," Patterns [klabel(consPatterns)] | ".Patterns" [klabel(dotPatterns )] syntax Declarations ::= Declaration Declarations [klabel(consDeclarations), format(%1%n%2)] diff --git a/src/parser-gen.md b/src/parser-gen.md index c370291..0574044 100644 --- a/src/parser-gen.md +++ b/src/parser-gen.md @@ -170,16 +170,17 @@ module PARSE-CONFIG // with \dv key -> type (CellInfo or KConfigVar) syntax KItem ::= "#extractConfigInfo" syntax KItem ::= collectCellName(Patterns) - rule #extractConfigInfo => collectCellName(P) ~> #extractConfigInfo ... + rule #extractConfigInfo => collectCellName(P, .Patterns) ~> #extractConfigInfo ... kConfiguration(noAttrs(P)) Configs => Configs SetItem(P) requires notBool P in Configs - rule collectCellName( _ { _ } (A)) => collectCellName(A) ... - rule collectCellName(A, B) => collectCellName(A) ~> collectCellName(B) ... + rule collectCellName( _ { _ } (A), .Patterns) => collectCellName(A) ... + rule collectCellName(A, B) => collectCellName(A, .Patterns) ~> collectCellName(B) ... + requires B =/=K .Patterns rule collectCellName( .Patterns ) => .K ... - rule collectCellName(\dv { Srt { .Sorts } } ( CellName )) => .K ... + rule collectCellName(\dv { Srt { .Sorts } } ( CellName ), .Patterns) => .K ... .Map => substrString(token2String(CellName), 1, lengthString(token2String(CellName)) -Int 1) |-> token2String(Srt) ... rule #extractConfigInfo => .K ... diff --git a/t/inner-parsing/parsed.ekore b/t/inner-parsing/parsed.ekore index e9d79ad..140b9bc 100644 --- a/t/inner-parsing/parsed.ekore +++ b/t/inner-parsing/parsed.ekore @@ -105,7 +105,7 @@ endmodule [ ] module DEFAULT-CONFIGURATION - configuration configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) + configuration configCell { } ( \dv { CellName { } } ( "k" ) , cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) import BASIC-K [ ] /* @@ -179,8 +179,8 @@ endmodule [ ] module INNER-PARSING - configuration configCell { } ( \dv { CellName { } } ( "T" ) , ( cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) , ( configCell { } ( \dv { CellName { } } ( "env" ) , ( cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) ) ) , \dv { CellName { } } ( "T" ) ) ) - rule ruleNoConditions { } ( KRewrite { } ( SemanticCastToFoo { } ( \dv { KVariable { } } ( "A" ) ) , ( emptyK { } ( ) ) ) ) + configuration configCell { } ( \dv { CellName { } } ( "T" ) , cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) , configCell { } ( \dv { CellName { } } ( "env" ) , cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) , \dv { CellName { } } ( "T" ) ) + rule ruleNoConditions { } ( KRewrite { } ( SemanticCastToFoo { } ( \dv { KVariable { } } ( "A" ) ) , emptyK { } ( ) ) ) syntax Foo ::= "bar" [ klabel ( bar ) , function ] syntax Foo ::= "buzz" [ klabel ( buzz ) ] syntax Layout ::= regexTerminal ( "(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" ) [ klabel ( layout ) ] @@ -615,8 +615,8 @@ "k" |-> "CellName" - SetItem ( configCell { } ( \dv { CellName { } } ( "T" ) , ( cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) , ( configCell { } ( \dv { CellName { } } ( "env" ) , ( cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) ) ) , \dv { CellName { } } ( "T" ) ) ) ) - SetItem ( configCell { } ( \dv { CellName { } } ( "k" ) , ( cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) ) ) + SetItem ( configCell { } ( \dv { CellName { } } ( "T" ) , cellPropertyListTerminator { } ( ) , cells { } ( configCell { } ( \dv { CellName { } } ( "k" ) , cellPropertyListTerminator { } ( ) , SemanticCastToPgm { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) , configCell { } ( \dv { CellName { } } ( "env" ) , cellPropertyListTerminator { } ( ) , emptyK { } ( ) , \dv { CellName { } } ( "env" ) ) ) , \dv { CellName { } } ( "T" ) ) ) + SetItem ( configCell { } ( \dv { CellName { } } ( "k" ) , cellPropertyListTerminator { } ( ) , SemanticCastToK { } ( \dv { KConfigVar { } } ( "$PGM" ) ) , \dv { CellName { } } ( "k" ) ) )