Parse configs and rules

.gitignore

@@ -4,3 +4,4 @@
 
 /.build/
 /.stack-work/
+.krun*

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,17 +70,18 @@ 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) \
                .then(proj.check(proj.source(expected))
                          .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()

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' *<k>\n *\.\n *</k>\n', '', kore)
-kore = re.sub(r' *<grammar>.*</grammar>\n', '', kore)
-kore = re.sub(r' *<grammar>\n.*\n *</grammar>\n', '', kore) # '.' doesn't match new lines?!
 
 outfile = open(out_file, 'w')
 for line in kore.split("\n")[1:-1]:

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`:
        </k>
 ```
 
+`frontend-to-ekore`: gets a full K definition and:
+
+ - parses into bubbles
+ - sanity checks
+ - parse config
+ - parse rules
+
+```k
+  rule <k> #parseCommandLine(frontend-to-ekore, PGM)
+        => PGM ~> #frontendPipeline
+           ...
+       </k>
+
+```
+
 `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 <k> 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
+    </k>
+    <kinkDeployedDir> DEPLOY_DIR </kinkDeployedDir>
 ```
 
 ```k

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