diff options
| author | herbelin | 2011-12-04 20:48:32 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-04 20:48:32 +0000 |
| commit | 095eee7e2ae4a1715683e766af973c28500583f0 (patch) | |
| tree | 1e053216380517db302e1ace1b7265887ccc5a7e | |
| parent | e47cdbd232517adf6e6bf411b9f9715c43773fd5 (diff) | |
Fixed a small regression in pattern-matching compilation introduced in
r14737 (when to expand an alias). However, the heuristic remains
different as before r14737 since we stopped taking into account the
dependency in the predicate to take the decision of expanding or not.
Let's see if we can eventually fine-tuning this.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | pretyping/termops.ml | 19 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
3 files changed, 24 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c7b6612f6a..77007b0ba5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1319,8 +1319,10 @@ and compile_alias pb (na,orig,(expanded,expanded_typ)) rest = mat = List.map (push_alias_eqn alias) pb.mat } in let j = compile pb in { uj_val = - if isRel c or isVar c then subst1 c j.uj_val - else mkLetIn (na,c,t,j.uj_val); + if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then + subst1 c j.uj_val + else + mkLetIn (na,c,t,j.uj_val); uj_type = subst1 c j.uj_type } in if isRel orig or isVar orig then (* Try to compile first using non expanded alias *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index b28f8046fa..2662093487 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -576,6 +576,25 @@ let dependent_main noevar m t = let dependent = dependent_main false let dependent_no_evar = dependent_main true +let count_occurrences m t = + let n = ref 0 in + let rec countrec m t = + if eq_constr m t then + incr n + else + match kind_of_term m, kind_of_term t with + | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> + countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); + Array.iter (countrec m) + (Array.sub lt + (Array.length lm) ((Array.length lt) - (Array.length lm))) + | _, Cast (c,_,_) when isMeta c -> () + | _, Evar _ -> () + | _ -> iter_constr_with_binders (lift 1) countrec m t + in + countrec m t; + !n + (* Synonymous *) let occur_term = dependent diff --git a/pretyping/termops.mli b/pretyping/termops.mli index d101d7d4ff..1c3517d564 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -108,6 +108,7 @@ val occur_var_in_decl : val free_rels : constr -> Intset.t val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool +val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Idset.t (** for visible vars only *) val occur_term : constr -> constr -> bool (** Synonymous |