diff options
| -rw-r--r-- | contrib/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 10 |
2 files changed, 7 insertions, 5 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index e60765b7e1..b3510e7c17 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -1066,7 +1066,7 @@ let is_not_strict t = Futhermore we don't expand fixpoints. *) let inline_test t = - not (is_fix t) && (ml_size t < 12 && is_not_strict t) + not (is_fix (eta_red t)) && (ml_size t < 12 && is_not_strict t) let manual_inline_list = let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index cd3134a7e1..0726cd2507 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -329,7 +329,7 @@ let rec subst_glob_ast s t = match t with | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t) | _ -> ast_map (subst_glob_ast s) t -let dfix_to_mlfix rv av i = +let dfix_to_mlfix rv av = let rec make_subst n s = if n < 0 then s else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s) @@ -343,7 +343,8 @@ let dfix_to_mlfix rv av i = in let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in let c = Array.map (subst 0) av - in MLfix(i, ids, c) + in + fun i -> MLfix(i, ids, c) let rec optim prm s = function | [] -> [] @@ -381,9 +382,10 @@ let rec optim_se top prm s = function | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> let av = Array.map (fun a -> normalize (subst_glob_ast !s a)) av in let all = ref true in + let mlfix = dfix_to_mlfix rv av in for i = 0 to Array.length rv - 1 do - if inline rv.(i) av.(i) - then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s + if inline rv.(i) (mlfix i) + then s := KNmap.add (kn_of_r rv.(i)) (mlfix i) !s else all := false done; if !all && top && not prm.modular |