From c48859717d847f4492a0c3cc76e8f8b0b38fcc10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 16:54:10 +0100
Subject: Update the extraction to handle casts between integers/bools

---
 backends/fstar/Primitives.fst | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backends/fstar')

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index dd340c00..a3ffbde4 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -273,6 +273,10 @@ let scalar_shr (#ty0 #ty1 : scalar_ty)
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
+// This can't fail, but for now we make all casts faillible (easier for the translation)
+let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty (if x then 1 else 0)
+
 /// The scalar types
 type isize : eqtype = scalar Isize
 type i8    : eqtype = scalar I8
-- 
cgit v1.2.3