coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Haskell Extraction, Trevor Elliott
- Re: [Coq-Club] Haskell Extraction, Wouter Swierstra
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Pierre Letouzey
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Pierre Letouzey
- Re: [Coq-Club] Haskell Extraction, Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Pierre Letouzey
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction,
Pierre Letouzey
- Re: [Coq-Club] Haskell Extraction, Pierre Letouzey
- Re: [Coq-Club] Haskell Extraction,
Trevor Elliott
- Re: [Coq-Club] Haskell Extraction, Wouter Swierstra
Archive powered by MhonArc 2.6.16.