The Coq mailing list

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

Hi Cedric,

I like your idea, and at the same time, this makes me think that maybe
implementing Ascii characters as a 256-branch inductive wouldn't be so
bad after all, would it ? (Both representations could still use your
trick by sharing the CharType signature you defined) Maybe that would
stress some parts of Coq's implementation but that's actually a good
thing. 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.

Do people out there actually use inductives with zillions (or, say,
hundreds) of constructors ? I'm quite curious about it.

Just my crazy 2 cents :)

Stéphane


On Wed, Mar 2, 2011 at 3:27 PM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> Hi all, I would like to know if hiding the
> "match c with Ascii b0 b1 b2 b3 b4 b5 b6 b7 => … end"
> when you do some "compute." or "simpl." with a module type wouldn't be
> nicer (as I did in the joint file); the obvious disadvantage, is that
> we can compute values only by rewritings, where the current version can
> simply evaluate expressions; but we may gain the possibility to have
> more readable code.
>
> What do you do to keep types clean with ascii?
>



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