!!! incomplete: Extend imp to do heating and cooling

kframework · Jul 2, 2019 · 36d51ef · 36d51ef
1 parent d51a077
commit 36d51ef
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 22 deletions.
diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore
@@ -34,18 +34,22 @@ endmodule [  ]
 
 module IMP-SIMPLE
 
-  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 { } ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( inj { BExpResult { } , BExp { } } ( False {  } (  ) ) , VarB : BExp {  } ) ) , DOTVAR : K {  } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExpResult {  } , KItem {  } } ( False {  } (  ) ) , DOTVAR : K {  } ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( inj { BExpResult { } , BExp { } } ( True {  } (  ) ) , VarB : BExp {  } ) ) , DOTVAR : K {  } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( VarB : BExp {  } ) , DOTVAR : K {  } ) ) ) ) [  ]
   import D-K [  ]
   sort BExp {  } [  ]
+  sort BExpResult {  } [  ]
   sort KCell {  } [  ]
-  symbol And {  } ( BExp {  } , BExp {  } ) : BExp {  } [ functional { } (), constructor { } (), injective { } () ]
-  symbol False {  } (  ) : BExp {  }                    [ functional { } (), constructor { } (), injective { } () ]
-  symbol True {  } (  ) : BExp {  }                     [ functional { } (), constructor { } (), injective { } () ]
-  symbol kCell {  } ( K {  } ) : KCell {  }             [ functional { } (), constructor { } (), injective { } () ]
-  syntax BExp ::= "False" [ functional , constructor , injective , klabel ( False ) ]
-  syntax BExp ::= "True" [ functional , constructor , injective , klabel ( True ) ]
+  symbol And {  } ( BExp {  } , BExp {  } ) : BExp {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  symbol False {  } (  ) : BExpResult {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  symbol HOLE {  } (  ) : BExpResult {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  symbol True {  } (  ) : BExpResult {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  symbol kCell {  } ( K {  } ) : KCell {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
   syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ]
+  syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ]
+  syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ]
+  syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ]
+  syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ]
   syntax KCell ::= "kCell" "(" K ")" [ functional , constructor , injective , klabel ( kCell ) ]
 
 endmodule [  ]

diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore
@@ -41,13 +41,16 @@ endmodule
 module IMP-SIMPLE
   import D-K []
 
-  syntax BExp ::= "True"             [klabel(True)]
-                | "False"            [klabel(False)]
-                | BExp "&&" BExp     [klabel(And)]
-  syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)]
+  syntax KCell ::= "kCell" "(" K ")"  [klabel(kCell)]
 
-  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),DOTVAR:K{}))
+  syntax BExpResult ::= "True"        [klabel(True)]
+                      | "False"       [klabel(False)]
+                      | "#hole"       [klabel(HOLE)]
+  syntax BExp ::= BExpResult          [klabel(inj)]
+                | BExp "&&" BExp      [klabel(And)]
+
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(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{}))
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{}))
+    => kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{}))
 endmodule
diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k
@@ -7,9 +7,16 @@ module IMP-SIMPLE
                  | ".K"               [klabel(dotk)]
   syntax KItem ::= BExp               [klabel(inj)]
 
-  syntax BExp ::= "True"         [klabel(True)]
-                | "False"        [klabel(False)]
-                | BExp "&&" BExp [klabel(And)]
-  rule <k> True  && B:BExp  => B:BExp </k>
-  rule <k> False && B:BExp  => False  </k>
+  syntax BExpResult ::= "True"        [klabel(True)]
+                      | "False"       [klabel(False)]
+                      | "#hole"       [klabel(HOLE)]
+  syntax BExp ::= BExpResult          [klabel(inj)]
+                | BExp "&&" BExp      [klabel(And)]
+
+  rule <k> True  && B:BExp  => B:BExp ... </k>
+  rule <k> False && B:BExp  => False ... </k>
+  rule <k> B1 && B2
+        => B1 ~> HOLE && B2
+           ...
+       </k>
 endmodule
diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/imp-simple/programs/conjunction.imp.expected
@@ -1 +1 @@
-kCell { } ( kseq { }(inj{BExp{}, KItem{}}(False{}()), dotk{}()))
+kCell { } ( kseq { }(inj{BExpResult{}, KItem{}}(False{}()), dotk{}()))
diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/imp-simple/programs/conjunction.imp.kast
@@ -1 +1 @@
-kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( True {  } (  ) , False {  } (  ) ) ) , dotk {  } (  ) ) )
+kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( inj { BExpResult {  } , BExp {  } } ( True {  } (  ) ) , inj { BExpResult {  } , BExp {  } } ( False {  } (  ) ) ) ) , dotk {  } (  ) ) )