diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 057057d1..b615955f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*) (*i*) open Util @@ -817,6 +817,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 = @@ -846,6 +858,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_split_at 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_split_at n l in |