diff --git a/Jenkinsfile b/Jenkinsfile index 68c5620..6a98c39 100644 --- a/Jenkinsfile +++ b/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 ''' } } diff --git a/build b/build index 155fa41..e77e786 100755 --- a/build +++ b/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' diff --git a/ext/k b/ext/k index 573112b..bf16bc2 160000 --- a/ext/k +++ b/ext/k @@ -1 +1 @@ -Subproject commit 573112b971d07286ff0b5ed0474707e79d34f96c +Subproject commit bf16bc272c4563ad697731f6abcc472ed18cd224 diff --git a/ext/kninja b/ext/kninja index a657727..c546284 160000 --- a/ext/kninja +++ b/ext/kninja @@ -1 +1 @@ -Subproject commit a6577278bf7e9659a8ca66567276c5601167a412 +Subproject commit c546284c88df8209fed90921416aedb9ed2ab0f1 diff --git a/src/command-line.md b/src/command-line.md index 824f497..f20ee51 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -62,7 +62,14 @@ the kore definition are kept. => PGM ~> #ekorePipeline ... +``` +```k + syntax KItem ::= "#success" + rule P:Pattern ~> (#success => .K) ... + _ => 0 + rule #success => .K ... + _ => 0 ``` 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 diff --git a/src/kink.md b/src/kink.md index 7f5ed9f..6607f88 100644 --- a/src/kink.md +++ b/src/kink.md @@ -37,11 +37,10 @@ module KINK-CONFIGURATION .Patterns - #token("UNNAMED", "ModuleName"):ModuleName .Patterns - .Declarations nullDecl @@ -49,7 +48,8 @@ module KINK-CONFIGURATION - $STRATEGY:K + 1 + initSCell(.Map) token2String($KINKDEPLOYEDDIR:Path) 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)) + ]] + MNAME + koreImport(IMPORTED, _) + 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 ]] MNAME sort SORT { PARAMS } ATTRS - 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 ]] MNAME (symbol SYMBOL { _ } ( _ ) : _ ATTRS) - 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 diff --git a/t/foobar/expected.ekore b/t/foobar/expected.ekore index 14b3961..0975bc5 100644 --- a/t/foobar/expected.ekore +++ b/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 diff --git a/t/foobar/foobar.ekore b/t/foobar/foobar.ekore index 7b4f4af..3964139 100644 --- a/t/foobar/foobar.ekore +++ b/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}( diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index 1a05192..47ebf53 100644 --- a/t/imp-simple/expected.ekore +++ b/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 { } [ ] diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore index c1be661..2b1e81f 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/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 diff --git a/t/peano/expected.ekore b/t/peano/expected.ekore index c3e3c25..b635bdc 100644 --- a/t/peano/expected.ekore +++ b/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 diff --git a/t/peano/peano.ekore b/t/peano/peano.ekore index c93618e..5bb32a1 100644 --- a/t/peano/peano.ekore +++ b/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 [ ]