t/*: Generate kseq and kdot from syntax declarations

This fixes missing constructor and functional attributes
kframework · Jul 3, 2019 · e23bf99 · e23bf99
1 parent f553a22
commit e23bf99
Show file tree

Hide file tree

Showing 6 changed files with 34 additions and 14 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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