From 9abd5986dae204ccdbc8a0dd06dec40ffd0ae842 Mon Sep 17 00:00:00 2001
From: Escherichia <162574063+EschericHya@users.noreply.github.com>
Date: Tue, 27 Aug 2024 16:33:57 +0200
Subject: [PATCH] Adds "support" for float (#321)

Co-authored-by: Escherichia <escherichia@charlotte>
---
 charon-pin                     |  2 +-
 compiler/ExtractBase.ml        | 16 +++++++++++++++-
 compiler/ExtractTypes.ml       |  1 +
 compiler/Pure.ml               |  1 +
 compiler/SynthesizeSymbolic.ml |  2 ++
 flake.lock                     | 12 ++++++------
 6 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/charon-pin b/charon-pin
index 4ec5a4ecc..cab9e427d 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-9e782beeb099f447661ce91da9ba1181a94642fe
+13502d2f3bd477ee86acafe5974016dc7707db83
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 197130b9a..b577f9aa0 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -530,9 +530,22 @@ let int_name (int_ty : integer_type) : string =
   | U64 -> Printf.sprintf u_format 64
   | U128 -> Printf.sprintf u_format 128
 
+let float_name (float_ty : float_type) : string =
+  let format =
+    match backend () with
+    | FStar | Coq | HOL4 -> format_of_string "f%d"
+    | Lean -> format_of_string "F%d"
+  in
+  match float_ty with
+  | F16 -> Printf.sprintf format 16
+  | F32 -> Printf.sprintf format 32
+  | F64 -> Printf.sprintf format 64
+  | F128 -> Printf.sprintf format 128
+
 let scalar_name (ty : literal_type) : string =
   match ty with
   | TInteger ty -> int_name ty
+  | TFloat ty -> float_name ty
   | TBool -> (
       match backend () with
       | FStar | Coq | HOL4 -> "bool"
@@ -1835,7 +1848,8 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
           match lty with
           | TBool -> "b"
           | TChar -> "c"
-          | TInteger _ -> "i")
+          | TInteger _ -> "i"
+          | TFloat _ -> "fl")
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
       | Error -> "x")
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 7a573d5a2..0315a1f68 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -438,6 +438,7 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
   | TBool -> F.pp_print_string fmt (bool_name ())
   | TChar -> F.pp_print_string fmt (char_name ())
   | TInteger int_ty -> F.pp_print_string fmt (int_name int_ty)
+  | TFloat float_ty -> F.pp_print_string fmt (float_name float_ty)
 
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ec81aedfa..aa7e1d9cc 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -37,6 +37,7 @@ module ConstGenericVarId = T.ConstGenericVarId
 
 type llbc_name = T.name [@@deriving show, ord]
 type integer_type = T.integer_type [@@deriving show, ord]
+type float_type = T.float_type [@@deriving show, ord]
 type const_generic_var = T.const_generic_var [@@deriving show, ord]
 type const_generic = T.const_generic [@@deriving show, ord]
 type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 69485ebc8..e6505b19f 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -60,6 +60,8 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
         sanity_check __FILE__ __LINE__ (otherwise_see = None) span;
         (* Return *)
         ExpandInt (int_ty, branches, otherwise)
+    | TLiteral (TFloat _) ->
+        craise __FILE__ __LINE__ span "Float are not supported in Aeneas yet"
     | TAdt (_, _) ->
         (* Branching: it is necessarily an enumeration expansion *)
         let get_variant (see : symbolic_expansion option) :
diff --git a/flake.lock b/flake.lock
index f51d42245..783e603f1 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1724239793,
-        "narHash": "sha256-aiR5BVfWpkzZWR1WZbMhqcuDAvznV5fq2nBDCqQEczc=",
+        "lastModified": 1724768110,
+        "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "9e782beeb099f447661ce91da9ba1181a94642fe",
+        "rev": "13502d2f3bd477ee86acafe5974016dc7707db83",
         "type": "github"
       },
       "original": {
@@ -272,11 +272,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1724206841,
-        "narHash": "sha256-L8dKaX4T3k+TR2fEHCfGbH4UXdspovz/pj87iai9qmc=",
+        "lastModified": 1724725307,
+        "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "45e98fbd62c32e5927e952d2833fa1ba4fb35a61",
+        "rev": "f56076b216c266cd855b0811ceb86802e834cdb9",
         "type": "github"
       },
       "original": {