Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Haskell Extraction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Haskell Extraction


chronological Thread 
  • From: Wouter Swierstra <w.swierstra AT cs.ru.nl>
  • To: Trevor Elliott <awesomelyawesome AT gmail.com>
  • Cc: coq-club AT inria.fr, Pierre Letouzey <pierre.letouzey AT inria.fr>
  • Subject: Re: [Coq-Club] Haskell Extraction
  • Date: Tue, 12 Apr 2011 10:36:08 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=xIBQAdu46lwxjyfMA+084QgGDmdtKz40mhPp7dLrUTdXy2bTsD4fp+owV/I03lkSl/ +49BW7Z/D7XA1pc+jhKqC13CektSLpGoEntvzk+H4Vjix3aDsNeavZGBXRlHm6+1GkIQ qNmewKRTpanHojmX83xre/Rv7B/y97/jquUcU=

Hi Trevor, cc-Pierre,

> Is this a limitation of the extraction plugin, or am I missing
> something when extracting Haskell?

Using the following commands produces pretty much what I'd expect to see:

> Extraction Language Haskell.
> Extract Inductive Datatypes.nat => "Integer" ["0" "succ"]
>   "(\fO fS n -> if n==0 then fO () else fS (n-1))".
> Extract Inlined Constant plus => "(+)".
> Extract Inlined Constant mult => "(*)".
> Extraction fact_body.
> Extraction fact.

But using "Recursive Extraction fact" seems to generate too much code:
it also produces code for mult and plus, which is exactly what the
Extract Inlined Constant commands should avoid... Is that the same
behaviour you're seeing?

All the best,

  Wouter



Archive powered by MhonArc 2.6.16.

Top of Page