diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 23 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
3 files changed, 25 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index eb039ba59a..ba7fc272a6 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 diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 684291d7ce..f9dda51255 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements m := elements_aux nil m. +Definition elements := elements_aux nil. (** * Fold *) diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index fee3f5bcfc..349cdedf7b 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -328,7 +328,7 @@ Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements s := elements_aux nil s. +Definition elements := elements_aux nil. (** ** Filter *) |