# Re: [isabelle] Code generator "eq" instances

```Hi Florian,

```
I may have spoke too soon: trying your [code del] trick didn't work. Here's the exact lemma I used:
```
lemma [code del]:
"eq_class.eq (Queue xs) (Queue ys) \<longleftrightarrow> xs = ys"

```
But I still get the same error when trying to generate Haskell code. I've also attached the two theory files.
```
Thanks,
-john

```

Attachment: Queue.thy
Description: Binary data

Attachment: AQueue.thy
Description: Binary data

```

On Jun 12, 2010, at 7:49 AM, John Matthews wrote:

```
```Hi Florian,

That makes sense, thanks.

```
In Section 2.5 ("Datatypes") of the codegen tutorial, when you talk about the code_datatype command you might want to mention that the user has to explicitly [code del] any definitions that use the old versions of the constructors, including automatically generated definitions like eq_class.eq. You might even want to consider adding some text showing how to add the concrete equality method for the AQueue example, but that would be more work. :)
```
```
Also, in the isar_ref manual, the syntax diagram for code_datatype is incorrect: It should take a list of consts, not a single const.
```
Cheers,
-john

On Jun 11, 2010, at 11:29 PM, Florian Haftmann wrote:

```
```Hi John,

```
What I'm really trying to do is generate a specialized equality method for your amortized queue code generation example. So I've defined the
```abstract version of the queue type as a single linked list, with the
corresponding queue method definitions:

lemma eq_AQueue[code]:
```
"eq_class.eq (AQueue xs ys) (AQueue xs' ys') = (ys @ rev xs = ys' @
```rev xs')"
by (auto simp add: AQueue_def eq_class.eq)
```
```
```
the problem is that the old equation using Queue is still kept as code
```equations;  you can either delete it explicitly:

lemma [code del]:
"eq_class.eq (Queue xs) (Queue ys) <--> xs = ys"

Or, which is perhaps more elegant, define an explicit conversion from
queues to lists:

primrec list_of_queue :: "'a queue \<Rightarrow> 'a list" where
"list_of_queue (Queue xs) = xs"

lemma list_of_AQueue [code]:
"list_of_queue (AQueue xs ys) = ys @ rev xs"

lemma [code]:
"HOL.eq q1 q2 \<longleftrightarrow>
HOL.eq (list_of_queue q1) (list_of_queue q2)"
by (auto simp add: eq intro: queue_eqI)

```
Then the old code equation is dropped since it is syntactically subsumed.
```
Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```
```
```
```
```

Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.