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



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.