Adds "support" for float (#321)

Co-authored-by: Escherichia <escherichia@charlotte>

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

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")

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).

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]

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) :