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/coq/Primitives.v                 | 4 ++++
 backends/fstar/Primitives.fst             | 4 ++++
 backends/lean/Base/Primitives/Scalar.lean | 4 ++++
 3 files changed, 12 insertions(+)

(limited to 'backends')

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 99ffe070..84280b96 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/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) .
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
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index db522df2..a8eda6d5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -411,6 +411,10 @@ def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
 def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) :=
   Scalar.tryMk tgt_ty x.val
 
+-- This can't fail, but for now we make all casts faillible (easier for the translation)
+def Scalar.cast_bool (tgt_ty : ScalarTy) (x : Bool) : Result (Scalar tgt_ty) :=
+  Scalar.tryMk tgt_ty (if x then 1 else 0)
+
 -- The scalar types
 -- We declare the definitions as reducible so that Lean can unfold them (useful
 -- for type class resolution for instance).
-- 
cgit v1.2.3