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é
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
