[isabelle-dev] Problems with Code-Generator

[Andreas Lochbihler]

Hi René,

I now pushed this the repository (1774d569b604), but I reuse the existing constant 
nat_of_integer instead of a new one.

Andreas

On 12/08/13 13:47, René Thiemann wrote:
> Hi Andreas,
>
>> Code_Target_Nat implements the type nat as an abstract type (code abstype) with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not appear in any equation of the code generator. Unfortunately, this declaration also sets up the term_of function for type nat to produce terms with this constructor. In the second example, your import_proof method uses the term_of function to get a term for the given proof (and the number contained in the proof) and introduces along with this number into the goal state.
>> As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then apply eval, the code generator complains that the abstract constructor is part of the goal state.
>
> I now see the problem.
>
>> The simplest solution is to introduce a new constructor for which you can prove a code equation. For example, the following defines a constructor Nat2 and redefines term_of for naturals to use Nat2. When you add it to your theory before declaring the parser structure, the second example works, too (tested with Isabelle 2b68f4109075). You then also have to reflect both nat and int as datatypes.
>
> I integrated this solution also in our larger development, and it works like a charm.
> Thanks!
>
>> If nobody has a better solution, we should think of including this setup in Code_Target_Nat.
>
> At least from my side, I can confirm that the solution works nicely.
>
> Cheers,
> René
>