The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Indeed, you are right, so in a way the situation isn't too bad.
Another matching pattern which looks simple but would be quadratic is
the following:

match c1, c2 with
| TAB, _ => true
| _, CR => true
| _, _ => false
end

I guess that's up to people to avoid stuff like that, except for some
basic necessary functions (equality test and maybe comparison).

Even with 'only' 512 cases or so, what bothers me is that because
underscore patterns are only syntactic, the right-hand side expression
will end up being duplicated and typechecked 500+ times in the term.

S.

On Wed, Mar 2, 2011 at 11:55 PM, Brandon Moore
<brandon_m_moore AT yahoo.com>
 wrote:
>
>
>> From: Stéphane Lescuyer 
>>Â <stephane.lescuyer AT inria.fr>
>
>>
>> ...
>>
>> The other thing I would be worried about is '_' patterns,  where
>> writing something like:
>>
>> match c1, c2 with
>> | TAB, CR =>  true
>> | _, _ => false
>> end
>>
>> would look harmless while actually  expanding to a 256*256 matching tree.
>
> A minor point, but I think that expands to a 256+256 matching tree.
> I would expect all but the TAB branch of the outer match to not
> decompose the second argument. It seems that's how it actually
> works, at least with a smaller example. Perhaps something with dependent
> types might see the pathological case.
>
> Example:
>
> Inductive foo : Set := A | B | C | D | E .
>
> Definition bar : foo -> foo -> bool := fun x y =>
>  match x, y with
>  | A, B => true
>  | _, _ => false
>  end.
>
> Print bar.
>
> produces
>
> bar =
> fun x y : foo =>
> match x with
> | A =>
>    match y with
>    | A => false
>    | B => true
>    | C => false
>    | D => false
>    | E => false
>    end
> | B => false
> | C => false
> | D => false
> | E => false
> end
>     : foo -> foo -> bool
>
>
>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06