Skip to content

Commit c33cd1a

Browse files
nishantjrnishantjr
committed
!!! incomplete: Extend imp to do heating and cooling
1 parent d0909a4 commit c33cd1a

5 files changed

Lines changed: 36 additions & 22 deletions

File tree

‎t/imp-simple/expected.ekore‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -36,18 +36,22 @@ endmodule [ ]
3636

3737
module IMP-SIMPLE
3838

39-
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 { } ) ) ) ) [ ]
40-
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 { } ) ) ) ) [ ]
39+
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 { } ) ) ) ) [ ]
40+
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 { } ) ) ) ) [ ]
4141
import D-K [ ]
4242
sort BExp { } [ ]
43+
sort BExpResult { } [ ]
4344
sort KCell { } [ ]
44-
symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } (), constructor { } (), injective { } () ]
45-
symbol False { } ( ) : BExp { } [ functional { } (), constructor { } (), injective { } () ]
46-
symbol True { } ( ) : BExp { } [ functional { } (), constructor { } (), injective { } () ]
47-
symbol kCell { } ( K { } ) : KCell { } [ functional { } (), constructor { } (), injective { } () ]
48-
syntax BExp ::= "False" [ functional , constructor , injective , klabel ( False ) ]
49-
syntax BExp ::= "True" [ functional , constructor , injective , klabel ( True ) ]
45+
symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ]
46+
symbol False { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ]
47+
symbol HOLE { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ]
48+
symbol True { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ]
49+
symbol kCell { } ( K { } ) : KCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ]
5050
syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ]
51+
syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ]
52+
syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ]
53+
syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ]
54+
syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ]
5155
syntax KCell ::= "kCell" "(" K ")" [ functional , constructor , injective , klabel ( kCell ) ]
5256

5357
endmodule [ ]

‎t/imp-simple/imp-simple.ekore‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -42,13 +42,16 @@ endmodule
4242
module IMP-SIMPLE
4343
import D-K []
4444

45-
syntax BExp ::= "True" [klabel(True)]
46-
| "False" [klabel(False)]
47-
| BExp "&&" BExp [klabel(And)]
48-
syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)]
45+
syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)]
4946

50-
rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),DOTVAR:K{}))
47+
syntax BExpResult ::= "True" [klabel(True)]
48+
| "False" [klabel(False)]
49+
| "#hole" [klabel(HOLE)]
50+
syntax BExp ::= BExpResult [klabel(inj)]
51+
| BExp "&&" BExp [klabel(And)]
52+
53+
rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{}))
5154
=> kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{}))
52-
rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),DOTVAR:K{}))
53-
=> kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),DOTVAR:K{}))
55+
rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{}))
56+
=> kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{}))
5457
endmodule

‎t/imp-simple/imp-simple.k‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,16 @@ module IMP-SIMPLE
77
| ".K" [klabel(dotk)]
88
syntax KItem ::= BExp [klabel(inj)]
99

10-
syntax BExp ::= "True" [klabel(True)]
11-
| "False" [klabel(False)]
12-
| BExp "&&" BExp [klabel(And)]
13-
rule <k> True && B:BExp => B:BExp </k>
14-
rule <k> False && B:BExp => False </k>
10+
syntax BExpResult ::= "True" [klabel(True)]
11+
| "False" [klabel(False)]
12+
| "#hole" [klabel(HOLE)]
13+
syntax BExp ::= BExpResult [klabel(inj)]
14+
| BExp "&&" BExp [klabel(And)]
15+
16+
rule <k> True && B:BExp => B:BExp ... </k>
17+
rule <k> False && B:BExp => False ... </k>
18+
rule <k> B1 && B2
19+
=> B1 ~> HOLE && B2
20+
...
21+
</k>
1522
endmodule

‎t/imp-simple/programs/conjunction.imp.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
kCell { } ( kseq { }(inj{BExp{}, KItem{}}(False{}()), dotk{}()))
1+
kCell { } ( kseq { }(inj{BExpResult{}, KItem{}}(False{}()), dotk{}()))

‎t/imp-simple/programs/conjunction.imp.kast‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , False { } ( ) ) ) , dotk { } ( ) ) )
1+
kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , inj { BExpResult { } , BExp { } } ( False { } ( ) ) ) ) , dotk { } ( ) ) )

0 commit comments

Comments
 (0)