From 3aa9c531db4e9cde25a4a149a64e3ff730ed798b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 15:47:42 +0100
Subject: Fix a minor issue with the extraction

---
 compiler/ExtractTypes.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 66418410..3657627b 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -192,12 +192,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
       F.pp_print_space fmt ();
       extract_expr false arg1
   | _ ->
+      let binop_is_shift = match binop with Shl | Shr -> true | _ -> false in
       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 (
+      (* In the case of F*, for shift operations, 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 binop_is_shift && !backend = FStar && is_const arg1 then (
         F.pp_print_space fmt ();
         let ty = ty_as_integer arg1.ty in
         F.pp_print_string fmt
-- 
cgit v1.2.3