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/build b/build index e77e786..80094e3 100755 --- a/build +++ b/build @@ -52,11 +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] + , other = [kore, ekore, parser, file, pgen, 'src/command-line.md', k_light, inner] , directory = proj.builddir('kink') , flags = '--syntax-module KINK-SYNTAX' , alias = 'kink' @@ -68,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) \ @@ -78,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) @@ -135,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/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/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 f20ee51..3994c68 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -1,4 +1,7 @@ ```k +require "file-util.k" +require "parser-gen.k" + module COMMAND-LINE-SYNTAX imports STRING-SYNTAX syntax KItem ::= "#parseCommandLine" "(" CommandLine "," Pgm ")" @@ -8,6 +11,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 ``` @@ -18,6 +22,8 @@ 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 @@ -28,6 +34,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 +60,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. @@ -76,16 +98,16 @@ High-level pipeline steps ========================= ```k - syntax K ::= "#kastPipeline" "(" String ")" [function] - rule #kastPipeline(PATH) - => #parseOuter + syntax K ::= "#kastPipeline" "(" String ")" + rule PGM:Any ~> #kastPipeline(PATH:String) + => parseOuter(tokenToString(PGM)) ~> #defnToConfig ~> #flattenProductions - ~> #collectGrammar + ~> #collectPgmGrammar ~> #parseProgramPath(PATH) ~> #success - syntax K ::= "#ekorePipeline" [function] + syntax K ::= "#ekorePipeline" rule #ekorePipeline => #parseToEKore ~> #defnToConfig @@ -95,6 +117,25 @@ High-level pipeline steps ~> #productionsToSymbolDeclarations ~> #translateRules ~> #success + + syntax K ::= "#frontendPipeline" + rule PGM:Any ~> #frontendPipeline + => parseOuter( + {readFile(DEPLOY_DIR +String "/src/inner.k")}:>String + +String + tokenToString(PGM) + ) // collect required files - hardcoded for now + ~> #defnToConfig + ~> #flattenProductions + // parse bubbles + ~> #createConfigGrammar + ~> #parseConfigBubbles + ~> #extractConfigInfo + ~> #createRuleGrammar + ~> #parseRuleBubbles + ~> #success + + DEPLOY_DIR ``` ```k diff --git a/src/ekore.md b/src/ekore.md index 0992a02..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 @@ -239,7 +245,7 @@ module ATTRIBUTES-COMMON syntax TagContent ::= UpperName | LowerName | Numbers | EKoreKString syntax TagContents - syntax KEY ::= LowerName + syntax KEY ::= LowerName //[token] // TODO: this token attribute causes a lot of weird ambiguities endmodule @@ -350,9 +356,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..410e9a7 --- /dev/null +++ b/src/inner.md @@ -0,0 +1,190 @@ +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 +``` + +```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 + +module DEFAULT-CONFIGURATION + imports BASIC-K + + configuration $PGM:K +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 6607f88..7e7e6e2 100644 --- a/src/kink.md +++ b/src/kink.md @@ -33,6 +33,7 @@ module KINK-CONFIGURATION syntax Declaration ::= "nullDecl" syntax DeclCellSet syntax DeclarationsCellFragment + configuration #parseCommandLine($COMMANDLINE:CommandLine, $PGM:Any) .Patterns @@ -44,13 +45,22 @@ 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 + + + .Map + .Set + 1 initSCell(.Map) token2String($KINKDEPLOYEDDIR:Path) + endmodule ``` @@ -67,6 +77,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) @@ -86,6 +97,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 ``` @@ -108,6 +122,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 @@ -199,67 +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 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 ------------------------------------ @@ -391,7 +361,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/kore.md b/src/kore.md index 17002ba..33f057e 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)] @@ -114,7 +115,8 @@ 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)] diff --git a/src/parser-gen.md b/src/parser-gen.md new file mode 100644 index 0000000..0574044 --- /dev/null +++ b/src/parser-gen.md @@ -0,0 +1,271 @@ +```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" + // 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) + 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 + imports META-ACCESSORS + + syntax KItem ::= "#parseProgramPath" "(" String ")" // Program Filename + | "#parseProgram" "(" IOString ")" // Program content + | "#collectPgmGrammar" + rule #parseProgramPath(PGM_FILENAME) => #parseProgram(readFile(PGM_FILENAME)) ... + + rule #parseProgram(PGM) + => parseWithProductions(GRAMMAR, "Pgm", PGM) + ... + + GRAMMAR + requires GRAMMAR =/=K .Set + + rule #collectPgmGrammar ... + MName + .Set => #getAllProds(MName) + requires findString(tokenToString(MName), "-SYNTAX", 0) =/=Int -1 + rule #collectPgmGrammar => .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 ::= "#parseConfigBubbles" + | "#createConfigGrammar" + + // 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 #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 #parseConfigBubbles => .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, .Patterns) ~> #extractConfigInfo ... + kConfiguration(noAttrs(P)) + Configs => Configs SetItem(P) + requires notBool P in Configs + + 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 ), .Patterns) => .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 ::= "#parseRuleBubbles" + | "#createRuleGrammar" + + rule #createRuleGrammar ... // create rule grammar + MName + kRule(noAttrs(_:Bubble)) + .Set => #addRuleCells(#addSubsorts(#addCasts(#getAllProds(MName) #getAllProds(#token("RULE-INNER", "UpperName"))))) + 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 #parseRuleBubbles ... + kRule(attrs(C:Bubble, At)) => kRule(attrs({parseWithProductions(GRAMMAR, "RuleContent", tokenToString(C))}:>Pattern, At)) + GRAMMAR + requires GRAMMAR =/=K .Set + + rule #parseRuleBubbles => .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 +``` 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/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/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 new file mode 100644 index 0000000..7735dc1 --- /dev/null +++ b/t/imp/expected.ekore @@ -0,0 +1,35 @@ +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 } } ( "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" ) , ( 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 + \ 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.k b/t/imp/imp.k new file mode 100644 index 0000000..009093e --- /dev/null +++ b/t/imp/imp.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 + imports IMP-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/inner-parsing/inner-parsing.k b/t/inner-parsing/inner-parsing.k new file mode 100644 index 0000000..8de3c52 --- /dev/null +++ b/t/inner-parsing/inner-parsing.k @@ -0,0 +1,10 @@ +module INNER-PARSING + syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] + + syntax Pgm ::= Foo + syntax Foo ::= "bar" [klabel(bar), function] + | "buzz" [klabel(buzz)] + configuration $PGM:Pgm .K + + rule A:Foo => .K +endmodule diff --git a/t/inner-parsing/parsed.ekore b/t/inner-parsing/parsed.ekore new file mode 100644 index 0000000..140b9bc --- /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" ) ) ) + + + + */ 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