From c27c3052ec3f9a093b06a41f56b3a361cb65e950 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Sun, 22 Oct 2023 16:34:46 -0700
Subject: Add more support for numeric operations, xor, rotate

---
 compiler/Extract.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'compiler/Extract.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ac81d6f3..b842aea1 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -3,7 +3,6 @@
    the formatter everywhere...
 *)
 
-open Utils
 open Pure
 open PureUtils
 open TranslateCore
@@ -61,6 +60,11 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | Le -> "le"
     | Ge -> "ge"
     | Gt -> "gt"
+    | 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 *)
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
@@ -498,14 +502,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg1
-  | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) ->
+  | _ ->
       let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr true arg0;
       F.pp_print_space fmt ();
-      extract_expr true arg1
-  | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented);
+      extract_expr true arg1);
   if inside then F.pp_print_string fmt ")"
 
 let type_decl_kind_to_qualif (kind : decl_kind)
-- 
cgit v1.2.3