summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap_on_disk
diff options
context:
space:
mode:
authorSon HO2023-12-14 16:49:34 +0100
committerGitHub2023-12-14 16:49:34 +0100
commitc3e0b90e422cbd902ee6d2b47073940c0017b7fb (patch)
tree92da14273eb068bcf418a2bdf9fbb6d27ba86102 /tests/coq/hashmap_on_disk
parentc6247e0c103cc1dc95c2a63ae01602c4a1208dc4 (diff)
parentb32fd66b71ad8fe28449d87a2e0334fdd36e286a (diff)
Merge pull request #53 from AeneasVerif/son/casts
Add support for casts between integers and booleans
Diffstat (limited to 'tests/coq/hashmap_on_disk')
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 99ffe070..84280b96 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -266,6 +266,10 @@ Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty
Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) :=
mk_scalar tgt_ty (to_Z x).
+(* This can't fail, but for now we make all casts faillible (easier for the translation) *)
+Definition scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) :=
+ mk_scalar tgt_ty (if x then 1 else 0).
+
(** Comparisons *)
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .