From f6cad578be588004b0f643083b0ea1274c389462 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 22:49:24 +0100
Subject: Rename Assumed.fst to Primitives.fst and make progress on that

---
 src/ExtractToFStar.ml | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'src')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 3a5d2c7a..3ca003a4 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -92,34 +92,40 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (binop : E.binop)
     (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
   if inside then F.pp_print_string fmt "(";
+  (* Some binary operations have a special treatment *)
   (match binop with
-  | Eq ->
+  | Eq | Lt | Le | Ne | Ge | Gt ->
+      let binop =
+        match binop with
+        | Eq -> "="
+        | Lt -> "<"
+        | Le -> "<="
+        | Ne -> "<>"
+        | Ge -> ">="
+        | Gt -> ">"
+        | _ -> failwith "Unreachable"
+      in
       extract_expr false arg0;
       F.pp_print_space fmt ();
-      F.pp_print_string fmt "=";
+      F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg1
-  | _ ->
+  | Div | Rem | Add | Sub | Mul ->
       let binop =
         match binop with
-        | Eq -> failwith "Unreachable"
-        | Lt -> "lt"
-        | Le -> "le"
-        | Ne -> "ne"
-        | Ge -> "ge"
-        | Gt -> "gt"
         | Div -> "div"
         | Rem -> "rem"
         | Add -> "add"
         | Sub -> "sub"
         | Mul -> "mul"
-        | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented
+        | _ -> failwith "Unreachable"
       in
       F.pp_print_string fmt (fstar_int_name int_ty ^ "_" ^ binop);
       F.pp_print_space fmt ();
       extract_expr false arg0;
       F.pp_print_space fmt ();
-      extract_expr false arg1);
+      extract_expr false arg1
+  | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented);
   if inside then F.pp_print_string fmt ")"
 
 (**
-- 
cgit v1.2.3