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



Dear Aaron,

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., from http://isabelle.in.tum.de/devel/.

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
  file "path_to_my_file.ML"
end

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 any documentation.

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,

Andreas


Am 07.12.2012 01:04, schrieb Aaron Gray:
Hi,

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
example ?

Many thanks in advance,

Aaron

--
Karlsruher Institut für Technologie
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.