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

---
 compiler/ExtractBase.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'compiler/ExtractBase.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 93204515..eb2a2ec9 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -498,7 +498,7 @@ let char_name () = if !backend = Lean then "Char" else "char"
 let str_name () = if !backend = Lean then "String" else "string"
 
 (** Small helper to compute the name of an int type *)
-let int_name (int_ty : integer_type) =
+let int_name (int_ty : integer_type) : string =
   let isize, usize, i_format, u_format =
     match !backend with
     | FStar | Coq | HOL4 ->
@@ -519,6 +519,14 @@ let int_name (int_ty : integer_type) =
   | U64 -> Printf.sprintf u_format 64
   | U128 -> Printf.sprintf u_format 128
 
+let scalar_name (ty : literal_type) : string =
+  match ty with
+  | TInteger ty -> int_name ty
+  | TBool -> (
+      match !backend with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+  | TChar -> (
+      match !backend with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+
 (** Extraction context.
 
     Note that the extraction context contains information coming from the
-- 
cgit v1.2.3