Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
it is not clear to me what you mean by generating code from a proof like
CoreC++. A proof of a theorem is not executable in ML or Haskell, only Isabelle
can check the proof. However, you can generate ML and Haskell code from
definitions in a formalisation, if they satisfy the restrictions of Isabelle's
code generator. The generated code then executes the definitions, not the
proofs. By the correctness of the code generator (unless someone messed with the
setup), the output of the generated code then is correct in the sense that you
could prove in Isabelle that the result is the denotation of the definitions for
the given input.
For CoreC++ in particular, the big-step semantics and the type system are
executable. This means that you can run CoreC++ programs in the semantics and
that you can infer the type of a statement or expression. Only two weeks ago, I
have spent a few days on reactivating the setup which got broken due to changes
in Isabelle's code generator. So, if you want to execute CoreC++, you need to
use the development version of the AFP. Most probably, this version will not
work with Isabelle2012, so you also have to use the development version, e.g.,
Now, back to your question. The export_code keyword generates such code. For
CoreC++, you might put these five lines into a file in the same folder as
CoreC++ and load it in jedit:
theory Code_Generation imports Execute begin
export_code big_step WT WT_i_i_i_o
in SML module_name CoreCpp
Once this file is processed, the code for the big step semantics, type checks
and type inference is in the file, along with the abstract syntax definition for
the CoreC++ language.
You can export to other language by replacing the "in SML ..." line as needed,
see the code generator tutorial for that.
If you prefer the command line, there's also Isabelle codegen tool with hardly
Once you have managed to get so far, you are now ready to execute CoreC++
programs. However, the type system and semantics expect the input to be in
CoreC++ abstract syntax, so you cannot feed in C++ programs directly. Daniel
Wasserrab once had a converter from C to CoreC++, but this has never been
adapted to the changes in Isabelle's code generator. So it probably won't work
out of the box. It should still work with the old generated ML files which
Daniel probably has somewhere, so you might ask him.
If you just want to try one small program in CoreC++, the easiest way is to
follow the examples in Execute.thy: Manually convert the program into CoreC++
syntax and define it inside Isabelle as a constant. Then, you can use the values
command to execute it.
Hope this helps,
Am 07.12.2012 01:04, schrieb Aaron Gray:
I am new to Isabelle/HOL and Isar in general although I know the principles
and am familiar with languages like Z. And with Haskell and ML.
I am trying to work out how to use the jEdit IDE, but would prefer to work
from command line as well.
How do I generate Haskell and ML and friends from a proof like CoreC++ for
Many thanks in advance,
Karlsruher Institut für Technologie
Dr. Andreas Lochbihler
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and