From 2653421a0487c6ca2a008e3addae5c1369f18dfb Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 2 Jul 2019 11:44:00 +0530 Subject: [PATCH 01/11] build: Fix dependency on k-light --- Jenkinsfile | 2 +- build | 8 ++++---- ext/kninja | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) 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/kninja b/ext/kninja index a657727..96e4092 160000 --- a/ext/kninja +++ b/ext/kninja @@ -1 +1 @@ -Subproject commit a6577278bf7e9659a8ca66567276c5601167a412 +Subproject commit 96e4092d582dbc3577252baa5866d51fe5df668a From c3f619b13596cb482324019bed8536cc7dd4216e Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 3 Jul 2019 13:32:32 +0530 Subject: [PATCH 02/11] Update K --- ext/k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 12e8f7b0ab2f7226f12016491d68cd064415fa42 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 2 Jul 2019 12:12:26 +0530 Subject: [PATCH 03/11] imp-simple: Use DOTVAR instead of dotk as second argument of kseq --- t/imp-simple/expected.ekore | 4 ++-- t/imp-simple/imp-simple.ekore | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index 1a05192..043cb34 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -34,8 +34,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..2521bcc 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/imp-simple/imp-simple.ekore @@ -46,8 +46,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 From a3c69c35b85310acbefae1affe974ab1550c7b95 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 2 Jul 2019 17:22:46 +0530 Subject: [PATCH 04/11] Remove unused cell originally intended for import statments --- src/kink.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/kink.md b/src/kink.md index 7f5ed9f..b74ecc5 100644 --- a/src/kink.md +++ b/src/kink.md @@ -37,11 +37,10 @@ module KINK-CONFIGURATION .Patterns - #token("UNNAMED", "ModuleName"):ModuleName .Patterns - .Declarations nullDecl From 0af8cc06af947abc69ee51d60fa342caabcb15b1 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 2 Jul 2019 17:24:04 +0530 Subject: [PATCH 05/11] Extend #getImportedModules to recurse through modules --- src/kink.md | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/src/kink.md b/src/kink.md index b74ecc5..95cb47d 100644 --- a/src/kink.md +++ b/src/kink.md @@ -97,6 +97,19 @@ module META-ACCESSORS imports BOOL imports SET + 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 ::= #isSortDeclared(ModuleName, SortName) [function, withConfig] rule [[ #isSortDeclared(MNAME:ModuleName, SORT:SortName) => true ]] MNAME @@ -105,11 +118,19 @@ module META-ACCESSORS ``` ```k - syntax Bool ::= #isSymbolDeclared(ModuleName, SymbolName) [function, withConfig] - rule [[ #isSymbolDeclared(MNAME, SYMBOL) => true ]] + syntax Bool ::= #isSymbolDeclaredSingleModule(ModuleName, SymbolName) [function] + rule [[ #isSymbolDeclaredSingleModule(MNAME, SYMBOL) => true ]] MNAME (symbol SYMBOL { _ } ( _ ) : _ ATTRS) - rule #isSymbolDeclared(_, _) => false [owise] + rule #isSymbolDeclaredSingleModule(_, _) => 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) + => #isSymbolDeclaredSingleModule(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME) + rule #isSymbolDeclaredSet(.Set, SNAME) => false ``` ```k From 2b07276e0f7d2d9985b7c28eb4a4f3e1d58535fb Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 3 Jul 2019 16:38:43 +0530 Subject: [PATCH 06/11] #isSortDeclared: Recurse over modules --- src/kink.md | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/kink.md b/src/kink.md index 95cb47d..8852c7d 100644 --- a/src/kink.md +++ b/src/kink.md @@ -110,26 +110,34 @@ module META-ACCESSORS ``` ```k - syntax Bool ::= #isSortDeclared(ModuleName, SortName) [function, withConfig] - rule [[ #isSortDeclared(MNAME:ModuleName, SORT:SortName) => true ]] + 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 ::= #isSymbolDeclaredSingleModule(ModuleName, SymbolName) [function] - rule [[ #isSymbolDeclaredSingleModule(MNAME, SYMBOL) => true ]] + syntax Bool ::= #isSymbolDeclaredMod(ModuleName, SymbolName) [function] + rule [[ #isSymbolDeclaredMod(MNAME, SYMBOL) => true ]] MNAME (symbol SYMBOL { _ } ( _ ) : _ ATTRS) - rule #isSymbolDeclaredSingleModule(_, _) => 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) - => #isSymbolDeclaredSingleModule(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME) + => #isSymbolDeclaredMod(M, SNAME) orBool #isSymbolDeclaredSet(Ms, SNAME) rule #isSymbolDeclaredSet(.Set, SNAME) => false ``` From 854375ec6446dff45520c4219c8bbb7e10c79610 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 3 Jul 2019 17:11:06 +0530 Subject: [PATCH 07/11] t/*: Generate kseq and kdot from syntax declarations This fixes missing constructor and functional attributes --- t/foobar/expected.ekore | 6 ++++-- t/foobar/foobar.ekore | 5 +++-- t/imp-simple/expected.ekore | 6 ++++-- t/imp-simple/imp-simple.ekore | 5 +++-- t/peano/expected.ekore | 6 ++++-- t/peano/peano.ekore | 20 ++++++++++++++++---- 6 files changed, 34 insertions(+), 14 deletions(-) diff --git a/t/foobar/expected.ekore b/t/foobar/expected.ekore index 14b3961..8d00b54 100644 --- a/t/foobar/expected.ekore +++ b/t/foobar/expected.ekore @@ -10,8 +10,10 @@ 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 diff --git a/t/foobar/foobar.ekore b/t/foobar/foobar.ekore index 7b4f4af..96ab0b9 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}( diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index 043cb34..b2bf86c 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -13,8 +13,10 @@ 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 [ ] diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore index 2521bcc..6934cc3 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}( diff --git a/t/peano/expected.ekore b/t/peano/expected.ekore index c3e3c25..1c55d6c 100644 --- a/t/peano/expected.ekore +++ b/t/peano/expected.ekore @@ -10,8 +10,10 @@ 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 diff --git a/t/peano/peano.ekore b/t/peano/peano.ekore index c93618e..e729e64 100644 --- a/t/peano/peano.ekore +++ b/t/peano/peano.ekore @@ -5,11 +5,23 @@ 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 From 8931da01a06cc8a85f5a38d0d01c59423584a304 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 3 Jul 2019 17:12:39 +0530 Subject: [PATCH 08/11] t/*: Add `sortInjection{}` attr needed by newer versions of kore-exec --- t/foobar/expected.ekore | 2 +- t/foobar/foobar.ekore | 2 +- t/imp-simple/expected.ekore | 2 +- t/imp-simple/imp-simple.ekore | 2 +- t/peano/expected.ekore | 2 +- t/peano/peano.ekore | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/t/foobar/expected.ekore b/t/foobar/expected.ekore index 8d00b54..0975bc5 100644 --- a/t/foobar/expected.ekore +++ b/t/foobar/expected.ekore @@ -18,7 +18,7 @@ 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 96ab0b9..3964139 100644 --- a/t/foobar/foobar.ekore +++ b/t/foobar/foobar.ekore @@ -25,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 b2bf86c..47ebf53 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -23,7 +23,7 @@ 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 [ ] diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore index 6934cc3..2b1e81f 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/imp-simple/imp-simple.ekore @@ -25,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/peano/expected.ekore b/t/peano/expected.ekore index 1c55d6c..b635bdc 100644 --- a/t/peano/expected.ekore +++ b/t/peano/expected.ekore @@ -18,7 +18,7 @@ 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 e729e64..5bb32a1 100644 --- a/t/peano/peano.ekore +++ b/t/peano/peano.ekore @@ -25,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}( inj{S2,S3}(inj{S1,S2}(T:S1)), inj{S1,S3}(T:S1)) [] endmodule [ ] From 386c510f4ba64a38e98c81926c064ea2bb81bf43 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 5 Jul 2019 16:24:47 +0530 Subject: [PATCH 09/11] Update KNinja --- ext/kninja | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ext/kninja b/ext/kninja index 96e4092..c546284 160000 --- a/ext/kninja +++ b/ext/kninja @@ -1 +1 @@ -Subproject commit 96e4092d582dbc3577252baa5866d51fe5df668a +Subproject commit c546284c88df8209fed90921416aedb9ed2ab0f1 From d9c94713a00c30c9af3c291af8f3374f5184e0ae Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 5 Jul 2019 16:25:30 +0530 Subject: [PATCH 10/11] Set exit code on pipeline completion --- src/command-line.md | 9 +++++++++ src/kink.md | 1 + 2 files changed, 10 insertions(+) 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 8852c7d..7750fb1 100644 --- a/src/kink.md +++ b/src/kink.md @@ -48,6 +48,7 @@ module KINK-CONFIGURATION + 1 $STRATEGY:K token2String($KINKDEPLOYEDDIR:Path) endmodule From 3dd25e26958b6ee0f0658dab45b62271f9c09523 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 18 Jul 2019 12:46:33 +0530 Subject: [PATCH 11/11] Fix cell initialization --- src/kink.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kink.md b/src/kink.md index 7750fb1..6607f88 100644 --- a/src/kink.md +++ b/src/kink.md @@ -49,7 +49,7 @@ module KINK-CONFIGURATION 1 - $STRATEGY:K + initSCell(.Map) token2String($KINKDEPLOYEDDIR:Path) endmodule ```