diff options
| author | letouzey | 2001-11-03 16:00:52 +0000 |
|---|---|---|
| committer | letouzey | 2001-11-03 16:00:52 +0000 |
| commit | eb698d2b16206a057a29779204e3817f2f4da093 (patch) | |
| tree | 55dbd376fe51f6239f9f771e9e3630bd496e0782 | |
| parent | d2805f1efbf19799229532ffd25ec2856fe11412 (diff) | |
retablissement de l'optim case constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2154 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/mlutil.ml | 17 | ||||
| -rw-r--r-- | contrib/extraction/test/Makefile | 6 |
2 files changed, 22 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 27c971c65c..2f3a67b6e6 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -239,6 +239,19 @@ let check_case br = if check_and_generalize br.(i) <> f then raise Impossible done; f +let check_constant_case br = + if br = [||] then raise Impossible; + let (r,l,t) = br.(0) in + let n = List.length l in + if occurs_itvl 1 n t then raise Impossible; + let cst = ml_lift (-n) t in + for i = 1 to Array.length br - 1 do + let (r,l,t) = br.(i) in + let n = List.length l in + if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) + then raise Impossible + done; cst + (*s Some Beta-iota reductions + simplifications*) let constructor_index = function @@ -320,7 +333,9 @@ let normalize a = try let f = check_case br' in simplify (MLapp (MLlam (anonymous,f),[e'])) - with Impossible -> MLcase (e', br') + with Impossible -> + try check_constant_case br' + with Impossible -> MLcase (e', br') else MLcase (e', br')) | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> (* expansion of a letin in special cases *) diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 787abb32ac..01875a6d26 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -75,6 +75,12 @@ $(REALSML): realsml # Utilities # +open: + find theories -name "*".ml -exec qualify2open \{\} \; + +undo_open: + find theories -name "*".ml -exec mv \{\}.orig \{\} \; + ml2v: ml2v.ml ocamlc -o $@ $< |