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 f7a59ef..5874687 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 5e168e6..e02b262 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