summaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ExtrOcamlNatInt.v14
-rw-r--r--plugins/extraction/ExtrOcamlZInt.v32
-rw-r--r--plugins/extraction/extraction.ml36
-rw-r--r--plugins/extraction/modutil.ml60
4 files changed, 84 insertions, 58 deletions
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index fd134899..956ece79 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -14,6 +14,10 @@ Require Import ExtrOcamlBasic.
(** Disclaimer: trying to obtain efficient certified programs
by extracting [nat] into [int] is definitively *not* a good idea:
+ - This is just a syntactic adaptation, many things can go wrong,
+ such as name captures (e.g. if you have a constant named "int"
+ in your development, or a module named "Pervasives"). See bug #2878.
+
- Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
@@ -34,17 +38,17 @@ Require Import ExtrOcamlBasic.
(** Mapping of [nat] into [int]. The last string corresponds to
a [nat_case], see documentation of [Extract Inductive]. *)
-Extract Inductive nat => int [ "0" "succ" ]
+Extract Inductive nat => int [ "0" "Pervasives.succ" ]
"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
(** Efficient (but uncertified) versions for usual [nat] functions *)
Extract Constant plus => "(+)".
-Extract Constant pred => "fun n -> max 0 (n-1)".
-Extract Constant minus => "fun n m -> max 0 (n-m)".
+Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)".
Extract Constant mult => "( * )".
-Extract Inlined Constant max => max.
-Extract Inlined Constant min => min.
+Extract Inlined Constant max => "Pervasives.max".
+Extract Inlined Constant min => "Pervasives.min".
(*Extract Inlined Constant nat_beq => "(=)".*)
Extract Inlined Constant EqNat.beq_nat => "(=)".
Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index c8c40e73..ab634329 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -34,12 +34,12 @@ Extract Inductive N => int [ "0" "" ]
(** Efficient (but uncertified) versions for usual functions *)
Extract Constant Pos.add => "(+)".
-Extract Constant Pos.succ => "succ".
-Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
-Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.succ => "Pervasives.succ".
+Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)".
Extract Constant Pos.mul => "( * )".
-Extract Constant Pos.min => "min".
-Extract Constant Pos.max => "max".
+Extract Constant Pos.min => "Pervasives.min".
+Extract Constant Pos.max => "Pervasives.max".
Extract Constant Pos.compare =>
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
Extract Constant Pos.compare_cont =>
@@ -47,12 +47,12 @@ Extract Constant Pos.compare_cont =>
Extract Constant N.add => "(+)".
-Extract Constant N.succ => "succ".
-Extract Constant N.pred => "fun n -> max 0 (n-1)".
-Extract Constant N.sub => "fun n m -> max 0 (n-m)".
+Extract Constant N.succ => "Pervasives.succ".
+Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)".
Extract Constant N.mul => "( * )".
-Extract Constant N.min => "min".
-Extract Constant N.max => "max".
+Extract Constant N.min => "Pervasives.min".
+Extract Constant N.max => "Pervasives.max".
Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
Extract Constant N.compare =>
@@ -60,19 +60,19 @@ Extract Constant N.compare =>
Extract Constant Z.add => "(+)".
-Extract Constant Z.succ => "succ".
-Extract Constant Z.pred => "pred".
+Extract Constant Z.succ => "Pervasives.succ".
+Extract Constant Z.pred => "Pervasives.pred".
Extract Constant Z.sub => "(-)".
Extract Constant Z.mul => "( * )".
Extract Constant Z.opp => "(~-)".
-Extract Constant Z.abs => "abs".
-Extract Constant Z.min => "min".
-Extract Constant Z.max => "max".
+Extract Constant Z.abs => "Pervasives.abs".
+Extract Constant Z.min => "Pervasives.min".
+Extract Constant Z.max => "Pervasives.max".
Extract Constant Z.compare =>
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
Extract Constant Z.of_N => "fun p -> p".
-Extract Constant Z.abs_N => "abs".
+Extract Constant Z.abs_N => "Pervasives.abs".
(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
For the moment we don't even try *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e76c6919..0a17453c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -130,7 +130,7 @@ let rec nb_default_params env c =
(* Enriching a signature with implicit information *)
-let sign_with_implicits r s =
+let sign_with_implicits r s nb_params =
let implicits = implicits_of_global r in
let rec add_impl i = function
| [] -> []
@@ -139,7 +139,7 @@ let sign_with_implicits r s =
if sign = Keep && List.mem i implicits then Kill Kother else sign
in sign' :: add_impl (succ i) s
in
- add_impl 1 s
+ add_impl (1+nb_params) s
(* Enriching a exception message *)
@@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args =
let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
(* Now, the extraction of the arguments. *)
let s_full = type2signature env (snd schema) in
- let s_full = sign_with_implicits (ConstRef kn) s_full in
+ let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
let s = sign_no_final_keeps s_full in
let ls = List.length s in
let la = List.length args in
(* The ml arguments, already expunged from known logical ones *)
let mla = make_mlargs env mle s args metas in
let mla =
- if not magic1 then
+ 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 (ConstRef kn)) mla in
if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
else mla
with _ -> mla
- else mla
in
(* For strict languages, purely logical signatures with at least
one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
@@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
let s = List.map (type2sign env) types in
- let s = sign_with_implicits (ConstructRef cp) s in
+ let s = sign_with_implicits (ConstructRef cp) s params_nb in
let ls = List.length s in
let la = List.length args in
assert (la <= ls + params_nb);
@@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
let l = List.map f oi.ip_types.(i) in
(* the corresponding signature *)
let s = List.map (type2sign env) oi.ip_types.(i) in
- let s = sign_with_implicits r s in
+ let s = sign_with_implicits r s mi.ind_nparams in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
@@ -876,7 +879,7 @@ let extract_std_constant env kn body typ =
let l,t' = type_decomp (expand env (var2var' t)) in
let s = List.map (type2sign env) l in
(* Check for user-declared implicit information *)
- let s = sign_with_implicits (ConstRef kn) s in
+ let s = sign_with_implicits (ConstRef kn) s 0 in
(* Decomposing the top level lambdas of [body].
If there isn't enough, it's ok, as long as remaining args
aren't to be pruned (and initial lambdas aren't to be all
@@ -923,6 +926,19 @@ let extract_std_constant env kn body typ =
in
trm, type_expunge_from_sign env s t
+(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
+let extract_axiom env kn typ =
+ reset_meta_count ();
+ (* The short type [t] (i.e. possibly with abbreviations). *)
+ let t = snd (record_constant_type env kn (Some typ)) in
+ (* The real type [t']: without head products, expanded, *)
+ (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+ let l,_ = type_decomp (expand env (var2var' t)) in
+ let s = List.map (type2sign env) l in
+ (* Check for user-declared implicit information *)
+ let s = sign_with_implicits (ConstRef kn) s 0 in
+ type_expunge_from_sign env s t
+
let extract_fixpoint env vkn (fi,ti,ci) =
let n = Array.length vkn in
let types = Array.make n (Tdummy Kother)
@@ -959,8 +975,8 @@ let extract_constant env kn cb =
in Dtype (r, vl, t)
in
let mk_ax () =
- let t = snd (record_constant_type env kn (Some typ)) in
- Dterm (r, MLaxiom, type_expunge env t)
+ let t = extract_axiom env kn typ in
+ Dterm (r, MLaxiom, t)
in
let mk_def c =
let e,t = extract_std_constant env kn c typ in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 257e1c1c..bd997d2d 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -26,9 +26,9 @@ let rec msid_of_mt = function
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
-let se_iter do_decl do_spec =
+let se_iter do_decl do_spec do_mp =
let rec mt_iter = function
- | MTident _ -> ()
+ | MTident mp -> do_mp mp
| MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
| MTwith (mt,ML_With_type(idl,l,t))->
let mp_mt = msid_of_mt mt in
@@ -38,7 +38,12 @@ let se_iter do_decl do_spec =
in
let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
mt_iter mt; do_decl (Dtype(r,l,t))
- | MTwith (mt,_)->mt_iter mt
+ | MTwith (mt,ML_With_module(idl,mp))->
+ let mp_mt = msid_of_mt mt in
+ let mp_w =
+ List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
+ in
+ mt_iter mt; do_mp mp_w; do_mp mp
| MTsig (_, sign) -> List.iter spec_iter sign
and spec_iter = function
| (_,Spec s) -> do_spec s
@@ -51,15 +56,16 @@ let se_iter do_decl do_spec =
me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
| (_,SEmodtype m) -> mt_iter m
and me_iter = function
- | MEident _ -> ()
+ | MEident mp -> do_mp mp
| MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
| MEapply (me,me') -> me_iter me; me_iter me'
| MEstruct (msid, sel) -> List.iter se_iter sel
in
se_iter
-let struct_iter do_decl do_spec s =
- List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
+let struct_iter do_decl do_spec do_mp s =
+ List.iter
+ (function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s
(*s Apply some fonctions upon all references in [ml_type], [ml_ast],
[ml_decl], [ml_spec] and [ml_structure]. *)
@@ -141,7 +147,7 @@ let decl_ast_search f = function
| _ -> ()
let struct_ast_search f s =
- try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
+ try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false
with Found -> true
let rec type_search f = function
@@ -165,7 +171,9 @@ let spec_type_search f = function
| Sval (_,u) -> type_search f u
let struct_type_search f s =
- try struct_iter (decl_type_search f) (spec_type_search f) s; false
+ try
+ struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s;
+ false
with Found -> true
@@ -247,34 +255,32 @@ let dfix_to_mlfix rv av i =
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
+(* [optim_se] applies the [normalize] function everywhere and does the
+ inlining of code. The inlined functions are kept for the moment in
+ order to preserve the global interface, later [depcheck_se] will get
+ rid of them if possible *)
+
let rec optim_se top to_appear s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
if i then s := Refmap'.add r a !s;
- if top && i && not (library ()) && not (List.mem r to_appear)
- then optim_se top to_appear s lse
- else
- let d = match optimize_fix a with
- | MLfix (0, _, [|c|]) ->
- Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
- | a -> Dterm (r, a, t)
- in (l,SEdecl d) :: (optim_se top to_appear s lse)
+ let d = match optimize_fix a with
+ | MLfix (0, _, [|c|]) ->
+ Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
+ | a -> Dterm (r, a, t)
+ in
+ (l,SEdecl d) :: (optim_se top to_appear s lse)
| (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
- let all = ref true in
(* This fake body ensures that no fixpoint will be auto-inlined. *)
let fake_body = MLfix (0,[||],[||]) in
for i = 0 to Array.length rv - 1 do
if inline rv.(i) fake_body
then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
- else all := false
done;
- if !all && top && not (library ())
- && (array_for_all (fun r -> not (List.mem r to_appear)) rv)
- then optim_se top to_appear s lse
- else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+ (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
| (l,SEmodule m) :: lse ->
let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
in (l,SEmodule m) :: (optim_se top to_appear s lse)
@@ -289,7 +295,7 @@ and optim_me to_appear s = function
(* After these optimisations, some dependencies may not be needed anymore.
For non-library extraction, we recompute a minimal set of dependencies
- for first-level objects *)
+ for first-level definitions (no module pruning yet). *)
exception NoDepCheck
@@ -362,7 +368,7 @@ let rec depcheck_se = function
end
| t :: se ->
let se' = depcheck_se se in
- se_iter compute_deps_decl compute_deps_spec t;
+ se_iter compute_deps_decl compute_deps_spec add_needed_mp t;
t :: se'
let rec depcheck_struct = function
@@ -370,7 +376,7 @@ let rec depcheck_struct = function
| (mp,lse)::struc ->
let struc' = depcheck_struct struc in
let lse' = depcheck_se lse in
- (mp,lse')::struc'
+ if lse' = [] then struc' else (mp,lse')::struc'
let check_implicits = function
| MLexn s ->
@@ -389,9 +395,9 @@ let optimize_struct to_appear struc =
List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
struc
in
- let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
ignore (struct_ast_search check_implicits opt_struc);
- if library () then opt_struc
+ if library () then
+ List.filter (fun (_,lse) -> lse<>[]) opt_struc
else begin
reset_needed ();
List.iter add_needed (fst to_appear);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 21:29:38 +0000