diff options
| author | letouzey | 2002-03-20 08:50:14 +0000 |
|---|---|---|
| committer | letouzey | 2002-03-20 08:50:14 +0000 |
| commit | 83a3896d3a9829f65f8cf19dd34890a1ea4913a9 (patch) | |
| tree | 0143b16411731315fd849fb3759661d4c345e14a | |
| parent | b360a6d7c86a5b79d995b642b7208353bae42ae1 (diff) | |
reorganisation des simplifications: letin eta-expansé apres le kill-dummy
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2550 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/mlutil.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index c9e2adaa24..59606dd65d 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -419,8 +419,6 @@ let rec simpl o = function | MLletin(id,c,e) when (id = dummy_name) || (is_atomic c) || (nb_occur e <= 1) -> simpl o (ml_subst c e) - | MLletin(_,c,e) when (is_atomic (eta_red c)) -> - simpl o (ml_subst (eta_red c) e) | MLfix(i,ids,c) as t when o -> let n = Array.length ids in if occurs_itvl 1 n c.(i) then @@ -474,6 +472,11 @@ and simpl_case o br e = if n = 0 then MLcase (e, br) else named_lams ids (MLcase (ml_lift n e, br)) +let rec post_simpl = function + | MLletin(_,c,e) when (is_atomic (eta_red c)) -> + post_simpl (ml_subst (eta_red c) e) + | a -> ast_map post_simpl a + (*S Local prop elimination. *) (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *) @@ -584,7 +587,7 @@ and kill_dummy_fix i fi c = (*s Putting things together. *) let normalize a = - if (optim()) then kill_dummy (simpl true a) else simpl false a + if (optim()) then post_simpl (kill_dummy (simpl true a)) else simpl false a (*S Special treatment of fixpoint for pretty-printing purpose. *) |