The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 2 Mar 2011 16:01:19 +0100,
Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>
 a écrit :

> 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.
> 

I have already done an Ocaml-generated Coq file of an inductive for
char with a 256 branching cases (quite a long time ago), but never
really tried it, maybe should I try to retrieve it.

I also thought of some intermediate representation with
8 time 2 cases and 1 time 256 cases, such as 2 times 16 cases, which
would allow to have hexadecimal digits.
But as often the best solution is an extremist one, I didn't really
thought of it.

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

I don't think anybody does that, but if one day some people want to do
benchmarks on coq, it could be a thing to try!

But what worries me in what I proposed, is that we won't be able to use
just "simpl/compute/unfold/cbv/…" to progress but variants like
"char_simpl/char_compute/char_cbv/…" which will produce bigger proof
terms, as will have to do some rewrittings.

Maybe should I browse coq contributions on chars to see if the
performance are not too bad.

> 
> 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?
> >
> 
> 
>