diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 36 |
1 files changed, 26 insertions, 10 deletions
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 |