aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ExtrOCamlFloats.v61
-rw-r--r--plugins/extraction/extraction.ml15
-rw-r--r--plugins/extraction/g_extraction.mlg4
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/json.ml9
-rw-r--r--plugins/extraction/miniml.ml3
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/mlutil.ml28
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml29
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml2
12 files changed, 114 insertions, 44 deletions
diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v
new file mode 100644
index 0000000000..1891772cc2
--- /dev/null
+++ b/plugins/extraction/ExtrOCamlFloats.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(* * 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.
+
+Note: the extraction of primitive floats relies on Coq's internal file
+kernel/float64.ml, so make sure the corresponding binary is available
+when linking the extracted OCaml code.
+
+For example, if you build a (_CoqProject + coq_makefile)-based project
+and if you created an empty subfolder "extracted" and a file "test.v"
+containing [Cd "extracted". Separate Extraction function_to_extract.],
+you will just need to add in the _CoqProject: [test.v], [-I extracted]
+and the list of [extracted/*.ml] and [extracted/*.mli] files, then add
+[CAMLFLAGS += -w -33] in the Makefile.local file. *)
+
+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 78c6255c1e..04f5b66241 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
| (Info, TypeScheme) ->
extract_type_app env sg db (r, type_sign env sg ty) args
| (Info, Default) -> Tunknown))
- | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
+ | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -690,6 +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 f -> assert (args = []); MLfloat f
| Ind _ | Prod _ | Sort _ -> assert false
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
@@ -754,18 +755,6 @@ and extract_cst_app env sg mle mlt kn args =
let la = List.length args in
(* The ml arguments, already expunged from known logical ones *)
let mla = make_mlargs env sg mle s args metas in
- let mla =
- if magic1 || lang () != Ocaml then mla
- else
- try
- (* for better optimisations later, we discard dependent args
- of projections and replace them by fake args that will be
- removed during final pretty-print. *)
- let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in
- if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
- else mla
- with e when CErrors.noncritical e -> mla
- in
(* For strict languages, purely logical signatures lead to a dummy lam
(except when [Kill Ktype] everywhere). So a [MLdummy] is left
accordingly. *)
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index e222fbc808..4f077b08b6 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -128,7 +128,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> {Feedback. msg_info (print_extraction_inline ()) }
+ -> {Feedback.msg_notice (print_extraction_inline ()) }
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -150,7 +150,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> { Feedback.msg_info (print_extraction_blacklist ()) }
+ -> { Feedback.msg_notice (print_extraction_blacklist ()) }
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
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 fba6b7c780..81b3e1bcdc 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -16,7 +16,10 @@ let json_bool b =
if b then str "true" else str "false"
let json_global typ ref =
- json_str (Common.pp_global typ ref)
+ if is_custom ref then
+ json_str (find_custom ref)
+ else
+ json_str (Common.pp_global typ ref)
let json_id id =
json_str (Id.to_string id)
@@ -158,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 2d5872718f..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
@@ -779,7 +783,7 @@ let eta_red e =
else e
| _ -> e
-(* Performs an eta-reduction when the core is atomic,
+(* Performs an eta-reduction when the core is atomic and value,
or otherwise returns None *)
let atomic_eta_red e =
@@ -789,7 +793,7 @@ let atomic_eta_red e =
| MLapp (f,a) when test_eta_args_lift 0 n a ->
(match f with
| MLrel k when k>n -> Some (MLrel (k-n))
- | MLglob _ | MLexn _ | MLdummy _ -> Some f
+ | MLglob _ | MLdummy _ -> Some f
| _ -> None)
| _ -> None
@@ -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
@@ -1547,6 +1552,7 @@ let inline r t =
not (to_keep r) (* The user DOES want to keep it *)
&& not (is_inline_custom r)
&& (to_inline r (* The user DOES want to inline it *)
- || (lang () != Haskell && not (is_projection r) &&
- (is_recursor r || manual_inline r || inline_test r t)))
+ || (lang () != Haskell &&
+ (is_projection r || is_recursor r ||
+ manual_inline r || inline_test r t)))
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 75fb35192b..34ddf57b40 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -229,12 +229,7 @@ let rec pp_expr par env args =
and pp_a1 = pp_expr false env [] a1
and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
- | MLglob r ->
- (try
- let args = List.skipn (projection_arity r) args in
- let record = List.hd args in
- pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
- with e when CErrors.noncritical e -> apply (pp_global Term r))
+ | MLglob r -> apply (pp_global Term r)
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -312,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 =
@@ -324,10 +322,14 @@ and pp_record_proj par env typ t pv args =
let n = List.length ids in
let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
let rel_i,a = match body with
- | MLrel i when i <= n -> i,[]
- | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a
+ | MLrel i | MLmagic(MLrel i) when i <= n -> i,[]
+ | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a))
+ | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a
| _ -> raise Impossible
in
+ let magic =
+ match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false
+ in
let rec lookup_rel i idx = function
| Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
| Pwild :: l -> lookup_rel i (idx+1) l
@@ -343,7 +345,10 @@ and pp_record_proj par env typ t pv args =
let pp_args = (List.map (pp_expr true env' []) a) @ args in
let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx
in
- pp_apply pp_head par pp_args
+ if magic then
+ pp_apply (str "Obj.magic") par (pp_head :: pp_args)
+ else
+ pp_apply pp_head par pp_args
and pp_record_pat (fields, args) =
str "{ " ++
@@ -579,14 +584,10 @@ let pp_decl = function
| Dterm (r, a, t) ->
let def =
if is_custom r then str (" = " ^ find_custom r)
- else if is_projection r then
- (prvect str (Array.make (projection_arity r) " _")) ++
- str " x = x."
else pp_function (empty_env ()) a
in
let name = pp_global Term r in
- let postdef = if is_projection r then name else mt () in
- pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
+ pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
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 ->
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 96a3d00dc2..be9259861a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -380,7 +380,7 @@ let check_inside_module () =
warn_extraction_inside_module ()
let check_inside_section () =
- if Lib.sections_are_opened () then
+ if Global.sections_are_opened () then
err (str "You can't do that within a section." ++ fnl () ++
str "Close it and try again.")
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:29:01 +0000