diff options
| author | Son HO | 2023-11-29 16:02:42 +0100 |
|---|---|---|
| committer | GitHub | 2023-11-29 16:02:42 +0100 |
| commit | 789ba1473acd287814a0d659b5f5a0e480e4e9d7 (patch) | |
| tree | 983ad685eb6b3c60b0baa3e3920dedbc6eaa0e57 /compiler/ExtractBase.ml | |
| parent | 90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff) | |
| parent | e732f97d09179fae43fafcb244340f98e3ca9229 (diff) | |
Merge pull request #39 from AeneasVerif/afromher_shifts
Add support for bitshifts
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 12 |
1 files changed, 5 insertions, 7 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. |