diff options
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/ExtrOcamlNatInt.v | 14 | ||||
-rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 32 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 36 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 60 |
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); |