From dc4b11689131bdb41a43e5aca76538556a3a120c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 15:45:27 +0100
Subject: Add support for more bitwise operations and update the extraction

---
 compiler/ExtractBase.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'compiler/ExtractBase.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 85ab1112..73ccac44 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -786,7 +786,7 @@ let unop_name (unop : unop) : string =
     like [<]).
  *)
 let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
-  let binop =
+  let binop_s =
     match binop with
     | Div -> "div"
     | Rem -> "rem"
@@ -800,16 +800,14 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | BitXor -> "xor"
     | BitAnd -> "and"
     | BitOr -> "or"
-    | Shl -> "lsl"
-    | Shr ->
-        "asr"
-        (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
+    | Shl -> "shl"
+    | Shr -> "shr"
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
   match !backend with
-  | Lean -> int_name int_ty ^ "." ^ binop
-  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
+  | Lean -> int_name int_ty ^ "." ^ binop_s
+  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
 
 (** A list of keywords/identifiers used by the backend and with which we
     want to check collision.
-- 
cgit v1.2.3