diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-07 18:59:02 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-07 18:59:02 +0000 |
commit | 6413ff1c4dd4b67d53fb15f82ca3dc0e129b7e38 (patch) | |
tree | dd6f3c5ed0eb2f9a220afa67fb4bbf0b358a7235 /test-suite/success/simpl.v | |
parent | 08adc88038688078c9b3e141620d8c320685e04a (diff) |
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
For instance, consider this inductive type:
Inductive Ind := A | B | C | D.
For detecting "match" on this type, one was forced earlier to write code
in Ltac using "match goal" and/or "context [...]" and long patterns such as:
match _ with A => _ | B => _ | C => _ | D => _ end
After this patch, this pattern can be shortened in many alternative ways:
match _ with A => _ | _ => _ end
match _ with B => _ | _ => _ end
match _ in Ind with _ => _ end
Indeed, if we want to detect a "match" of a given type, we can either
leave at least one branch where a constructor is explicit, or use a "in"
annotation.
Now, we can also detect any "match" regardless of its type:
match _ with _ => _ end
Note : this will even detect "match" over empty inductive types.
Compatibility should be preserved, since "match _ with end" will
continue to correspond only to empty inductive types.
Internally, the constr_pattern PCase has changed quite a lot, a few elements
are now grouped into a case_info_pattern record, while branches are now
lists of given sub-patterns.
NB: writing "match" with missing last branches in a constr pattern was actually
tolerated by Pattern.pattern_of_glob_constr earlier, since the number of
constructor per inductive is unknown there. And this was triggering an uncaught
exception in a array_fold_left_2 in Matching later. Oups. At least this patch
fixes this issue...
Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number
of branch in a match pattern. I doubt this was really a problem, but having now
linear code instead cannot harm ;-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/simpl.v')
0 files changed, 0 insertions, 0 deletions