Add extraction for primitive floats

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

1 files changed, 12 insertions, 7 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 000df26858..44b95ae4c1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -398,6 +398,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLaxiom, MLaxiom -> true
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2
+| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
 | _, _ -> false
 
 and eq_ml_pattern p1 p2 = match p1, p2 with
@@ -430,7 +431,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> ()
   in iter 0
 
 (*s Map over asts. *)
@@ -449,7 +450,8 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -467,7 +469,8 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ as a -> a
 
 (*s Iter over asts. *)
 
@@ -481,7 +484,8 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -517,7 +521,7 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0
   in nb 1
 
 (* Replace unused variables by _ *)
@@ -569,7 +573,7 @@ let dump_unused_vars a =
        let b' = ren env b in
        if b' == b then a else MLmagic b'
 
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a
 
     and ren_branch env ((ids,p,b) as tr) =
       let occs = List.map (fun _ -> ref false) ids in
@@ -1402,7 +1406,8 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l