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] Pushing constants out of functions at extraction time
- Date: Thu, 14 Apr 2011 11:04:11 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=jDxx6J8cVkR6yE0v72N3mATfavt66SzlmN49EE7snPTELEuXtGGYhimUZlI0YgmNnF /Zow/44G0iqZBroTCyFcG/5BQNlMofY5Tys0/S+SDTu+Z3Mwc3+l4xxjoQpa/bzdo3EV OgUc/eNRhXj4vsvfoL5Iuq8Pdahkwoseizlm0=
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.