Skip to content

Commit 20aba52

Browse files
committed
[spectec] Add missing EQ/NE reduction rules to IL semantics
1 parent 035fbe0 commit 20aba52

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

spectec/doc/semantics/il/5-reduction.spectec

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,10 +121,18 @@ rule Step_exp/CMP-EQ-true:
121121
S |- CMP EQ e_1 e_2 ~> BOOL true
122122
-- if e_1 = e_2
123123

124+
rule Step_exp/CMP-EQ-false:
125+
S |- CMP EQ val_1 val_2 ~> BOOL false
126+
-- if val_1 =/= val_2
127+
124128
rule Step_exp/CMP-NE-false:
125129
S |- CMP NE e_1 e_2 ~> BOOL false
126130
-- if e_1 = e_2
127131

132+
rule Step_exp/CMP-NE-true:
133+
S |- CMP NE val_1 val_2 ~> BOOL true
134+
-- if val_1 =/= val_2
135+
128136
rule Step_exp/CMP-NUM:
129137
S |- CMP numcmpop num_1 num_2 ~> BOOL $numcmp(numcmpop, num_1, num_2)
130138

0 commit comments

Comments
 (0)