coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Re: Pushing constants out of functions at extraction time
- Date: Thu, 14 Apr 2011 14:12:58 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:content-type :content-transfer-encoding; b=IlE/PVObCp71OGmkvGQ7IFavWJBvA4tPinB9iMmX59gHAD1BbYTTM4J9wr+lXmeZoZ scQNULO/u47mdmbOkblOGQTSMvBYXdNimEuAHcWL1QHR3fBF6NxPGhvuZo0cCiJUl3qg KjsEcSG3hXeyhWzwYlCKdlbyAHl/If3BDTVzo=
My mistake, OCaml is already clever enough to solve this !
Sorry about the noise, and thanks to Arthur for pointing this
Alexandre
2011/4/14 Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>:
> Dear list
>
> I was wondering if it was currently possible (and if not, how hard it
> would be to add this possibility) to push constant out of function
> definitions at extraction time, so that they are not rebuild at each
> call.
>
> For example, say I have a function like
>
> Definition foo n :=
> if eq_nat_dec n 32 then ... else ...
>
> The 32 is extracted as S (S (.....)) *inside* the function, triggering
> 32 allocations at each call of foo
>
> I was wondering if it was possible to obtain automatically something like
>
> Let __const51 = S (S (...))
>
> let foo n =
> match eq_nat_dec n __const51 with
> ...
>
> to avoid those useless allocations
>
> Thanks
>
> Alexandre Pilkiewicz
>
- [Coq-Club] Pushing constants out of functions at extraction time, Alexandre Pilkiewicz
- [Coq-Club] Re: Pushing constants out of functions at extraction time, Alexandre Pilkiewicz
Archive powered by MhonArc 2.6.16.