Add extraction for primitive floats

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

10 files changed, 78 insertions, 10 deletions

diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v
new file mode 100644
index 0000000000..1b07215c63
--- /dev/null
+++ b/plugins/extraction/ExtrOCamlFloats.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Extraction to OCaml of native binary64 floating-point numbers. *)
+
+From Coq Require Floats Extraction.
+
+(** Basic data types used by some primitive operators. *)
+
+Extract Inductive bool => bool [ true false ].
+Extract Inductive prod => "( * )" [ "" ].
+
+Extract Inductive FloatClass.float_class =>
+  "Float64.float_class"
+  [ "PNormal" "NNormal" "PSubn" "NSubn" "PZero" "NZero" "PInf" "NInf" "NaN" ].
+Extract Inductive PrimFloat.float_comparison =>
+  "Float64.float_comparison"
+  [ "FEq" "FLt" "FGt" "FNotComparable" ].
+
+(** Primitive types and operators. *)
+
+Extract Constant PrimFloat.float => "Float64.t".
+Extraction Inline PrimFloat.float.
+(* Otherwise, the name conflicts with the primitive OCaml type [float] *)
+
+Extract Constant PrimFloat.classify => "Float64.classify".
+Extract Constant PrimFloat.abs => "Float64.abs".
+Extract Constant PrimFloat.sqrt => "Float64.sqrt".
+Extract Constant PrimFloat.opp => "Float64.opp".
+Extract Constant PrimFloat.eqb => "Float64.eq".
+Extract Constant PrimFloat.ltb => "Float64.lt".
+Extract Constant PrimFloat.leb => "Float64.le".
+Extract Constant PrimFloat.compare => "Float64.compare".
+Extract Constant PrimFloat.mul => "Float64.mul".
+Extract Constant PrimFloat.add => "Float64.add".
+Extract Constant PrimFloat.sub => "Float64.sub".
+Extract Constant PrimFloat.div => "Float64.div".
+Extract Constant PrimFloat.of_int63 => "Float64.of_int63".
+Extract Constant PrimFloat.normfr_mantissa => "Float64.normfr_mantissa".
+Extract Constant PrimFloat.frshiftexp => "Float64.frshiftexp".
+Extract Constant PrimFloat.ldshiftexp => "Float64.ldshiftexp".
+Extract Constant PrimFloat.next_up => "Float64.next_up".
+Extract Constant PrimFloat.next_down => "Float64.next_down".
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 872f30135f..04f5b66241 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -690,7 +690,7 @@ let rec extract_term env sg mle mlt c args =
        let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in
        extract_app env sg mle mlt extract_var args
     | Int i -> assert (args = []); MLuint i
-    | Float _ -> assert false (* TODO: Implement primitive float for extraction *)
+    | Float f -> assert (args = []); MLfloat f
     | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e4efbcff0c..4769bef475 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -215,6 +215,8 @@ let rec pp_expr par env args =
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
+    | MLfloat _ ->
+      pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
 
 and pp_cons_pat par r ppl =
   pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 912a20f389..81b3e1bcdc 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -161,6 +161,10 @@ let rec json_expr env = function
       ("what", json_str "expr:int");
       ("int", json_str (Uint63.to_string i))
     ]
+  | MLfloat f -> json_dict [
+      ("what", json_str "expr:float");
+      ("float", json_str (Float64.to_string f))
+    ]
 
 and json_one_pat env (ids,p,t) =
   let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index 8b69edbe4c..32e0d3c05d 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -126,7 +126,8 @@ and ml_ast =
   | MLdummy  of kill_reason
   | MLaxiom
   | MLmagic  of ml_ast
-  | MLuint of Uint63.t
+  | MLuint   of Uint63.t
+  | MLfloat  of Float64.t
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index e3c9635c55..32e0d3c05d 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -127,6 +127,7 @@ and ml_ast =
   | MLaxiom
   | MLmagic  of ml_ast
   | MLuint   of Uint63.t
+  | MLfloat  of Float64.t
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
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
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 6b1eef7abb..fe49bfc1ec 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a =
 	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index e7004fe9af..34ddf57b40 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -307,6 +307,9 @@ let rec pp_expr par env args =
     | MLuint i ->
         assert (args=[]);
         str "(" ++ str (Uint63.compile i) ++ str ")"
+    | MLfloat f ->
+        assert (args=[]);
+        str "(" ++ str (Float64.compile f) ++ str ")"
 
 
 and pp_record_proj par env typ t pv args =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index dd840cd929..c341ec8d57 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -131,6 +131,8 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
+    | MLfloat _ ->
+      paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->