Merge pull request #5 from kframework/fix-klight-dep

build: Fix dependency on k-light & Update K

Jenkinsfile

@@ -20,7 +20,7 @@ pipeline {
       steps {
         ansiColor('xterm') {
           sh '''#!/bin/bash
-            (cd ext/k-light/ && mvn package -DskipTests) && ./build kink .build/kbackend-haskell
+            ./build kink .build/kbackend-haskell
           '''
         }
       }

build

@@ -40,10 +40,10 @@ def kore_exec(kore, ext = 'kore-exec'):
 
 def build_k_light():
     return proj.rule( 'build-k-light'
-                    , description = 'Building K'
-                    , command = 'cd ext/k-light && mvn package -q -DskipTests'
+                    , description = 'Building K-light'
+                    , command = '(cd ext/k-light && mvn package -q -DskipTests) && touch $out'
                     ) \
-                    .output('ext/k-light/bin/kompile')
+                    .output(proj.builddir('k-light.timestamp'))
 k_light = proj.dotTarget().then(build_k_light())
 
 # Kore to K Pipeline
@@ -56,7 +56,7 @@ file   = 'src/file-util.md'
 
 kink = proj.definition( backend   = 'ocaml'
                       , main      = 'src/kink.md'
-                      , other     = [kore, ekore, parser, file, 'src/command-line.md']
+                      , other     = [kore, ekore, parser, file, 'src/command-line.md', k_light]
                       , directory = proj.builddir('kink')
                       , flags     = '--syntax-module KINK-SYNTAX'
                       , alias     = 'kink'

src/command-line.md

@@ -62,7 +62,14 @@ the kore definition are kept.
         => PGM ~> #ekorePipeline
            ...
        </k>
+```
 
+```k
+  syntax KItem ::= "#success"
+  rule <k> P:Pattern ~> (#success => .K) ... </k>
+       <exit-code> _ => 0 </exit-code>
+  rule <k> #success => .K ... </k>
+       <exit-code> _ => 0 </exit-code>
 ```
 
 High-level pipeline steps
@@ -76,6 +83,7 @@ High-level pipeline steps
     ~> #flattenProductions
     ~> #collectGrammar
     ~> #parseProgramPath(PATH)
+    ~> #success
 
   syntax K ::= "#ekorePipeline" [function]
   rule #ekorePipeline
@@ -86,6 +94,7 @@ High-level pipeline steps
     ~> #productionsToSortDeclarations
     ~> #productionsToSymbolDeclarations
     ~> #translateRules
+    ~> #success
 ```
 
 ```k

src/kink.md

@@ -37,19 +37,19 @@ module KINK-CONFIGURATION
                 <definition>
                    <defnAttrs format="[ %2 ]%n"> .Patterns </defnAttrs>
                    <modules format="%2%n">
-                     <mod format="module %2%i%n%4%n%5%n%6%d%n %i%dendmodule %3%n%n"
+                     <mod format="module %2%i%n%4%n%5%n%d%n %i%dendmodule %3%n%n"
                           multiplicity="*" type="Set">
                        <name format="%2"> #token("UNNAMED", "ModuleName"):ModuleName </name>
                        <attributes format="[ %2 ]"> .Patterns </attributes>
-                       <imp format="%2"> .Declarations </imp>
                        <declarations format="%2">
                          <decl format="%2%n" multiplicity="*" type="Set"> nullDecl </decl>
                        </declarations>
                        <grammar> .Set </grammar>
                      </mod>
                    </modules>
                 </definition>
-                <s> $STRATEGY:K </s>
+                <exit-code exit=""> 1 </exit-code>
+                initSCell(.Map)
                 <kinkDeployedDir> token2String($KINKDEPLOYEDDIR:Path) </kinkDeployedDir>
 endmodule
 ```
@@ -98,19 +98,48 @@ module META-ACCESSORS
   imports BOOL
   imports SET
 
-  syntax Bool ::= #isSortDeclared(ModuleName, SortName) [function, withConfig]
-  rule [[ #isSortDeclared(MNAME:ModuleName, SORT:SortName) => true ]]
+  syntax Set ::= #getImportedModules(ModuleName)      [function]
+  syntax Set ::= #getImportedModulesSet(ModuleName, Set) [function]
+  rule #getImportedModules(MNAME) => #getImportedModulesSet(MNAME, SetItem(MNAME))
+  rule [[ #getImportedModulesSet(MNAME, MODS)
+       => #getImportedModulesSet(MNAME, MODS SetItem(IMPORTED) #getImportedModules(IMPORTED))
+       ]]
+       <name> MNAME </name>
+       <decl> koreImport(IMPORTED, _) </decl>
+    requires notBool IMPORTED in MODS
+  rule #getImportedModulesSet(MNAME, MODS) => MODS [owise]
+```
+
+```k
+  syntax Bool ::= #isSortDeclaredMod(ModuleName, SortName) [function]
+  rule [[ #isSortDeclaredMod(MNAME:ModuleName, SORT:SortName) => true ]]
        <name> MNAME </name>
        <decl> sort SORT { PARAMS } ATTRS </decl>
-  rule #isSortDeclared(_, _) => false [owise]
+  rule #isSortDeclaredMod(_, _) => false [owise]
+
+  syntax Bool ::= #isSortDeclared(ModuleName, SortName) [function]
+  syntax Bool ::= #isSortDeclaredSet(Set, SortName)     [function]
+  rule #isSortDeclared(MNAME, SNAME)
+    => #isSortDeclaredSet(#getImportedModules(MNAME), SNAME)
+  rule #isSortDeclaredSet(SetItem(M) Ms, SNAME)
+    => #isSortDeclaredMod(M, SNAME) orBool #isSortDeclaredSet(Ms, SNAME)
+  rule #isSortDeclaredSet(.Set, SNAME) => false
 ```
 
 ```k
-  syntax Bool ::= #isSymbolDeclared(ModuleName, SymbolName) [function, withConfig]
-  rule [[ #isSymbolDeclared(MNAME, SYMBOL) => true ]]
+  syntax Bool ::= #isSymbolDeclaredMod(ModuleName, SymbolName) [function]
+  rule [[ #isSymbolDeclaredMod(MNAME, SYMBOL) => true ]]
        <name> MNAME </name>
        <decl> (symbol SYMBOL { _ } ( _ ) : _ ATTRS) </decl>
-  rule #isSymbolDeclared(_, _) => false [owise]
+  rule #isSymbolDeclaredMod(_, _) => false [owise]
+
+  syntax Bool ::= #isSymbolDeclared(ModuleName, SymbolName) [function]
+  syntax Bool ::= #isSymbolDeclaredSet(Set, SymbolName)     [function]
+  rule #isSymbolDeclared(MNAME, SNAME)
+    => #isSymbolDeclaredSet(#getImportedModules(MNAME), SNAME)
+  rule #isSymbolDeclaredSet(SetItem(M) Ms, SNAME)
+    => #isSymbolDeclaredMod(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME)
+  rule #isSymbolDeclaredSet(.Set, SNAME) => false
 ```
 
 ```k

t/foobar/expected.ekore

@@ -10,13 +10,15 @@ module B-KSEQ
   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 {  } [ functional { } ( ), constructor { } ( ), injective { } ( ) ]
-  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional { } ( ), constructor { } ( ), injective { } ( )  ]
+  symbol dotk {  } (  ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  syntax K ::= ".K" [ functional , constructor , injective , klabel ( dotk ) ]
+  syntax K ::= KItem "~>" K [ functional , constructor , injective , klabel ( kseq ) ]
 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 [  ]
+  symbol inj { From , To } ( From ) : To [ sortInjection{}() ]
 endmodule [  ]
 
 module D-K

t/foobar/foobar.ekore

@@ -6,9 +6,10 @@ endmodule [ ]
 module B-KSEQ
   import A-BASIC-K []
 
-  symbol kseq{}(KItem{}, K{}) : K{} [functional{}(), constructor{}(), injective{}()]
+  syntax K ::= KItem "~>" K [klabel(kseq)]
+  syntax K ::= ".K" [klabel(dotk)]
+
   symbol append{}(K{}, K{}) : K{} [function{}()]
-  symbol dotk{}() : K{} [functional{}(), constructor{}(), injective{}()]
 
   axiom{ R }
     \equals{K{},R}(
@@ -24,7 +25,7 @@ module B-KSEQ
 endmodule [ ]
 
 module C-INJ
-  symbol inj{From,To}(From) : To []
+  symbol inj{From,To}(From) : To [ sortInjection{}() ]
 
   axiom{S1,S2,S3,R}
     \equals{S3,R}(

t/imp-simple/expected.ekore

@@ -13,15 +13,17 @@ module B-KSEQ
   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 {  } [  ]
+  symbol dotk {  } (  ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  syntax K ::= ".K" [ functional , constructor , injective , klabel ( dotk ) ]
+  syntax K ::= KItem "~>" K [ functional , constructor , injective , klabel ( kseq ) ]
 
 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 [  ]
+  symbol inj { From , To } ( From ) : To [ sortInjection{}() ]
 
 endmodule [  ]
 
@@ -34,8 +36,8 @@ endmodule [  ]
 
 module IMP-SIMPLE
 
-  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( False {  } (  ) , VarB : BExp {  } ) ) , dotk {  } (  ) ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( False {  } (  ) ) , dotk {  } (  ) ) ) ) ) [  ]
-  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( True {  } (  ) , VarB : BExp {  } ) ) , dotk {  } (  ) ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( VarB : BExp {  } ) , dotk {  } (  ) ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( False {  } (  ) , VarB : BExp {  } ) ) , DOTVAR : K { } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( False {  } (  ) ) , DOTVAR : K { } ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( True {  } (  ) , VarB : BExp {  } ) ) , DOTVAR : K { } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( VarB : BExp {  } ) , DOTVAR : K { } ) ) ) ) [  ]
   import D-K [  ]
   sort BExp {  } [  ]
   sort KCell {  } [  ]

t/imp-simple/imp-simple.ekore

@@ -6,9 +6,10 @@ endmodule [ ]
 module B-KSEQ
   import A-BASIC-K []
 
-  symbol kseq{}(KItem{}, K{}) : K{} []
+  syntax K ::= KItem "~>" K [klabel(kseq)]
+  syntax K ::= ".K" [klabel(dotk)]
+
   symbol append{}(K{}, K{}) : K{} [function{}()]
-  symbol dotk{}() : K{} []
 
   axiom{ R }
     \equals{K{},R}(
@@ -24,7 +25,7 @@ module B-KSEQ
 endmodule [ ]
 
 module C-INJ
-  symbol inj{From,To}(From) : To []
+  symbol inj{From,To}(From) : To [ sortInjection{}() ]
 
   axiom{S1,S2,S3,R}
     \equals{S3,R}(
@@ -46,8 +47,8 @@ module IMP-SIMPLE
                 | BExp "&&" BExp     [klabel(And)]
   syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)]
 
-  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),dotk{}()))
-    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),dotk{}()))
-  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),dotk{}()))
-    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),dotk{}()))
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),DOTVAR:K{}))
+    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{}))
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),DOTVAR:K{}))
+    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),DOTVAR:K{}))
 endmodule

t/peano/expected.ekore

@@ -10,13 +10,15 @@ module B-KSEQ
   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 {  } [ functional { } ( ), constructor { } ( ), injective { } ( )  ]
-  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional { } ( ), constructor { } ( ), injective { } ( )  ]
+  symbol dotk {  } (  ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional {  } (  ) , constructor {  } (  ) , injective { } ( ) ]
+  syntax K ::= ".K" [ functional , constructor , injective , klabel ( dotk ) ]
+  syntax K ::= KItem "~>" K [ functional , constructor , injective , klabel ( kseq ) ]
 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 [  ]
+  symbol inj { From , To } ( From ) : To [ sortInjection{}() ]
 endmodule [  ]
 
 module D-K

t/peano/peano.ekore

@@ -5,15 +5,27 @@ endmodule [ ]
 
 module B-KSEQ
   import A-BASIC-K []
+
+  syntax K ::= KItem "~>" K [klabel(kseq)]
+  syntax K ::= ".K" [klabel(dotk)]
+
   symbol append{}(K{}, K{}) : K{} [function{}()]
-  symbol dotk {  } (  ) : K {  } [ functional { } ( ), constructor { } ( ), injective { } ( )  ]
-  symbol kseq {  } ( KItem {  } , K {  } ) : K {  } [ functional { } ( ), constructor { } ( ), injective { } ( )  ]
-  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 { } ) ) ) [ ]
+
+  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{})))
+  []
 endmodule [ ]
 
 module C-INJ
-  symbol inj{From,To}(From) : To []
+  symbol inj{From,To}(From) : To [ sortInjection{}() ]
   axiom{S1,S2,S3,R} \equals{S3,R}( inj{S2,S3}(inj{S1,S2}(T:S1)), inj{S1,S3}(T:S1)) []
 endmodule [ ]