Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Pushing constants out of functions at extraction time

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Pushing constants out of functions at extraction time


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page