Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- To: Aaron Gray <aaronngray.lists at gmail.com>
- Subject: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- From: andreas.lochbihler at kit.edu
- Date: Fri, 04 Jan 2013 12:44:01 +0100
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <CANkmNDfqhwhZYQ=Az+2W9ek5DiQGX1v_imhgW7BSdnu-Jx-6uA@mail.gmail.com>
- References: <CANkmNDdVzsLAQZPQtpcKrXGuiRBP_dAnA=f6dWE4Bretmpqnig@mail.gmail.com> <50C1D8C1.email@example.com> <CANkmNDfqhwhZYQ=Az+2W9ek5DiQGX1v_imhgW7BSdnu-Jx-6uA@mail.gmail.com>
- User-agent: Internet Messaging Program (IMP) H3 (4.0.4)
Sorry for the late response, I have been out of office for 3 weeks.
This looks like you are using the Isabelle2012 version of CoreC++ from
http://afp.sourceforge.net/entries/CoreC++.shtml and not the
development version of the AFP from
http://afp.sourceforge.net/devel-entries/CoreC++.shtml. The above code
works fine for me with the latter.
theory Code_Generation imports Execute begin
export_code big_step WT WT_i_i_i_o
in SML module_name CoreCpp
I have the development version built on Ubuntu and checking CoreC++ okay,
but cannot seem to get your above example working. I have tried looking at
the code and managed to get an instance/constant code generated but not the
type system or semantics.
There is no constant 'big_step' or WT_i_i_i_o and it says "No code
equations for WT"
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and