Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation



Dear René,

Thanks for the info and tips. Hopefully I will get somewhere tomorrow.

Regards,

Aaron



On 7 December 2012 11:52, René Thiemann <rene.thiemann at uibk.ac.at> wrote:

> Dear Aaron,
>
> > How do I generate Haskell and ML and friends from a proof like CoreC++
> for
> > example ?
>
> As far as I know, you cannot generate Haskell code from a "proof", but
> just from
> definitions and functions, and in certain cases also from inductive
> definitions
> by using the predicate compiler.
>
> In principle, everything that can be written as an equality "lhs = rhs"
> can be fed
> to the code-generator.
>
> lemma [code]: "lhs = rhs"
> proof ...
>
> declare my_theorem[code]
>
> then getting the code is as easy as writing
>
> export_code some_function in Haskell file ...
>
> however, it might fail whenever there are non-executable involved.
>
> For example, defining
>
> definition fermat where "fermat n = (?x y z. x > 0 /\ y > 0 /\ x^n + y^n =
> z^n)"
>
> then
>
> export_code fermat in Haskell file -
>
> will fail, but if you first prove a code-equation
>
> lemma fermat_code[code]: "fermat n = (n <= 2)"
> proof ...
>
> then of course it will become executable.
>
> Further information on the code-generator can be found by
>
> isabelle doc codegen
>
> Hope this helps,
> René
> --
> René Thiemann                    mailto:rene.thiemann at uibk.ac.at
> Computational Logic Group
> http://cl-informatik.uibk.ac.at/~thiemann/
> Institute of Computer Science    phone: +43 512 507-6434
> University of Innsbruck
>
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.