Add support for more bitwise operations and update the extraction

2 files changed, 17 insertions, 9 deletions

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.
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index f61c28e4..66418410 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -163,7 +163,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   (match (!backend, binop) with
   | HOL4, (Eq | Ne)
   | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
-  | Lean, (Div | Rem | Add | Sub | Mul) ->
+  | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
       let binop =
         match binop with
         | Eq -> "="
@@ -179,7 +179,9 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
         | Mul -> "*"
         | Shl -> "<<<"
         | Shr -> ">>>"
-        | BitXor | BitAnd | BitOr -> raise (Failure "Unimplemented")
+        | BitXor -> "^^^"
+        | BitOr -> "|||"
+        | BitAnd -> "&&&"
       in
       let binop =
         match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop
@@ -192,6 +194,14 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   | _ ->
       let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
+      (* In the case of F*, because machine integers are simply integers
+         with a refinement, if the second argument is a constant we
+         need to provide the second implicit type argument *)
+      if !backend = FStar && is_const arg1 then (
+        F.pp_print_space fmt ();
+        let ty = ty_as_integer arg1.ty in
+        F.pp_print_string fmt
+          ("#" ^ StringUtils.capitalize_first_letter (int_name ty)));
       F.pp_print_space fmt ();
       extract_expr true arg0;
       F.pp_print_space fmt ();