Equality defined using boolean theory

formalsec · Jun 11, 2024 · a459be4 · a459be4
1 parent d89904a
commit a459be4
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/lib/lexer.mll b/lib/lexer.mll
@@ -56,8 +56,8 @@ let keywords =
      ; ("int.mul", BINARY (Ty_int, Mul))
      ; ("int.rem", BINARY (Ty_int, Rem))
      ; ("int.pow", BINARY (Ty_int, Pow))
-     ; ("int.eq", RELOP (Ty_int, Eq))
-     ; ("int.ne", RELOP (Ty_int, Ne))
+     ; ("int.eq", RELOP (Ty_bool, Eq))
+     ; ("int.ne", RELOP (Ty_bool, Ne))
      ; ("int.lt", RELOP (Ty_int, Lt))
      ; ("int.le", RELOP (Ty_int, Le))
      ; ("int.gt", RELOP (Ty_int, Gt))
@@ -77,8 +77,8 @@ let keywords =
      ; ("real.rem", BINARY (Ty_real, Rem))
      ; ("real.min", BINARY (Ty_real, Min))
      ; ("real.max", BINARY (Ty_real, Max))
-     ; ("real.eq", RELOP (Ty_real, Eq))
-     ; ("real.ne", RELOP (Ty_real, Ne))
+     ; ("real.eq", RELOP (Ty_bool, Eq))
+     ; ("real.ne", RELOP (Ty_bool, Ne))
      ; ("real.lt", RELOP (Ty_real, Lt))
      ; ("real.le", RELOP (Ty_real, Le))
      ; ("real.gt", RELOP (Ty_real, Gt))
@@ -115,8 +115,8 @@ let keywords =
      ; ("i32.shr_u", BINARY (Ty_bitv 32, ShrL))
      ; ("i32.rem", BINARY (Ty_bitv 32, Rem))
      ; ("i32.rem_u", BINARY (Ty_bitv 32, RemU))
-     ; ("i32.eq", RELOP (Ty_bitv 32, Eq))
-     ; ("i32.ne", RELOP (Ty_bitv 32, Ne))
+     ; ("i32.eq", RELOP (Ty_bool, Eq))
+     ; ("i32.ne", RELOP (Ty_bool, Ne))
      ; ("i32.lt_u", RELOP (Ty_bitv 32, LtU))
      ; ("i32.lt", RELOP (Ty_bitv 32, Lt))
      ; ("i32.le_u", RELOP (Ty_bitv 32, LeU))
@@ -153,8 +153,8 @@ let keywords =
      ; ("i64.shr_u", BINARY (Ty_bitv 64, ShrL))
      ; ("i64.rem", BINARY (Ty_bitv 64, Rem))
      ; ("i64.rem_u", BINARY (Ty_bitv 64, RemU))
-     ; ("i64.eq", RELOP (Ty_bitv 64, Eq))
-     ; ("i64.ne", RELOP (Ty_bitv 64, Ne))
+     ; ("i64.eq", RELOP (Ty_bool, Eq))
+     ; ("i64.ne", RELOP (Ty_bool, Ne))
      ; ("i64.lt_u", RELOP (Ty_bitv 64, LtU))
      ; ("i64.lt", RELOP (Ty_bitv 64, Lt))
      ; ("i64.le_u", RELOP (Ty_bitv 64, LeU))