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



Dear Andreas,

Thank you for the information and a path forwards. I will try running Linux
in a VM tomorrow. I have Linux servers but they are headless. And I have
Windows/Cygwin/Java 1.7 problems using the development branch.

Then will look into using Java native on Windows with MinGW for Bash rather
than via Cygwin. It would also be nice to have an environment that is not
dependent upon Bash though.

Has/is Isabelle/HOL been/being migrated to Scala from ML ? If so do you
know what the status is here ?

Regards,

Aaron





On 7 December 2012 11:53, Andreas Lochbihler <andreas.lochbihler at kit.edu>wrote:

> 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/<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 <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.