coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
- To: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Ascii module
- Date: Wed, 2 Mar 2011 16:01:19 +0100
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
- [Coq-Club] Ascii module, AUGER Cedric
- Re: [Coq-Club] Ascii module, Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
AUGER Cedric
- Re: [Coq-Club] Ascii module,
Frederic Blanqui
- Re: [Coq-Club] Ascii module,
Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
Frederic Blanqui
- Re: [Coq-Club] Ascii module, Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
Frederic Blanqui
- Re: [Coq-Club] Ascii module,
Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
Frederic Blanqui
- Re: [Coq-Club] Ascii module, Brandon Moore
- Message not available
- Re: [Coq-Club] Ascii module,
Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
AUGER Cedric
- Re: [Coq-Club] Ascii module,
Pierre Letouzey
- Re: [Coq-Club] Ascii module, Adam Koprowski
- Re: [Coq-Club] Ascii module,
Pierre Letouzey
- Re: [Coq-Club] Ascii module,
AUGER Cedric
- Re: [Coq-Club] Ascii module,
Stéphane Lescuyer
- Re: [Coq-Club] Ascii module,
AUGER Cedric
- Re: [Coq-Club] Ascii module, Stéphane Lescuyer
Archive powered by MhonArc 2.6.16.