summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-11-29 15:45:27 +0100
committerSon Ho2023-11-29 15:45:27 +0100
commitdc4b11689131bdb41a43e5aca76538556a3a120c (patch)
tree513cd1909faa9b0316a0e6f6be2fa88b7a1e90a7 /compiler
parent0273fee7f6b74da1d3b66c3c6a2158c012d04197 (diff)
Add support for more bitwise operations and update the extraction
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBase.ml12
-rw-r--r--compiler/ExtractTypes.ml14
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 ();