diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-20 14:54:01 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-20 14:54:01 +0000 |
commit | 4102fedccf34dc3f759685cda7018c605be1c22c (patch) | |
tree | e7f43604ce719ee8f5bc73d0b0d6b4223698b3ff /plugins/extraction | |
parent | 0c4a086210c6366c9ee1f091cc51ea5c92b5a903 (diff) |
Extraction: re-introduce some eta-expansions in rare situations leading to '_a types
If there's no lambdas at the top of a constant body
and its type is functional
and this type contains type variable
and we're extracting to Ocaml
then we perform one eta-expansion to please the ML type-checker
This might slow down things, if some computations are shared
thanks to the partial application. But it seems quite unlikely to
encounter both situations (clever partial application and
non-generalizable variable) at the same time. Compcert is ok,
for instance.
As a consequence, no need for manual eta-expansion in AVL code
(and by the way MSetAVL.element wasn't a problem, it is monomorphic)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/extraction.ml | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index eb039ba59..ba7fc272a 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -815,6 +815,18 @@ let rec decomp_lams_eta_n n m env c t = let eta_args = List.rev_map mkRel (interval 1 d) in rels, applist (lift d c,eta_args) +(* Let's try to identify some situation where extracted code + will allow generalisation of type variables *) + +let rec gentypvar_ok c = match kind_of_term c with + | Lambda _ | Const _ -> true + | App (c,v) -> + (* if all arguments are variables, these variables will + disappear after extraction (see [empty_s] below) *) + array_for_all isRel v && gentypvar_ok c + | Cast (c,_,_) -> gentypvar_ok c + | _ -> false + (*s From a constant to a ML declaration. *) let extract_std_constant env kn body typ = @@ -844,6 +856,17 @@ let extract_std_constant env kn body typ = then decompose_lam_n m body else decomp_lams_eta_n n m env body typ in + (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) + let rels, c = + let n = List.length rels in + let s,s' = list_chop n s in + let k = sign_kind s in + let empty_s = (k = EmptySig || k = SafeLogicalSig) in + if lang () = Ocaml && empty_s && not (gentypvar_ok c) + && s' <> [] && type_maxvar t <> 0 + then decomp_lams_eta_n (n+1) n env body typ + else rels,c + in let n = List.length rels in let s = list_firstn n s in let l,l' = list_chop n l in |