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

```Thanks Florian, that helps my understanding.

```
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:
```
theory Queue
imports Main
begin

datatype 'a queue = Queue "('a list)"

definition empty :: "'a queue" where ...

primrec enqueue :: "'a => 'a queue => 'a queue" where ...

fun dequeue :: "'a queue => 'a option * 'a queue" where ...

end

```
Then I have another theory file where I'm trying to generate code for the concrete instance of the queue type with two constructor arguments:
```
theory AQueue
imports Queue
begin

definition
AQueue :: "'a list => 'a list => 'a queue" where
"AQueue xs ys = Queue (ys @ rev xs)"

code_datatype AQueue

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)

export_code "eq_class.eq :: 'a queue => 'a queue => bool" in Haskell
module_name AQueue
file AQueueCode

end

```
I'm trying to use lemma eq_AQueue to tell the code generator to use my specialized (==) method definition on the AQueue constructors when generating Haskell code. But then Isabelle gives me this error when it tries to generate the Haskell program:
```
```
*** "Queue.queue.Queue" is not a constructor, on left hand side of equation *** eq_queue_inst.eq_queue (Queue ?list1) (Queue ?list'1) == eq_list_inst.eq_list ?list1 ?list'1
```  *** At command "export_code".

Should I be doing something differently here?

Thanks,
-john

On Jun 9, 2010, at 11:01 PM, Florian Haftmann wrote:

```
```Hi John,

```
I'm trying to understand how to safely generate Haskell code from HOL,
```where I want the Haskell code to be an instance of the Eq class, but
with my own definition of the (==) method. I want Isabelle to enforce
```
that my definition of (==) is sound, i.e. it implements logical equality.
```
```
the system is setup in a way that instantiation of the eq class happens
```in exectly that manner automatically on each datatype statements (c.f.
§2.6 of the code generation tutorial):

```
So I'm trying to make my datatype an instance of the eq class, but I'm
```running into an error when using the function package to make the
corresponding definition. Here's an example theory file:

theory Silly
imports Main
begin

datatype silly = Silly int
```
```
Try here,  e.g.

export_code "HOL.eq :: silly => _" in Haskell file -

```
```instantiation silly :: eq
begin

fun "eq_class.eq" where
"eq (Silly n) (Silly m) = (m - n = 0)"

instance ..

end
```
```
The conventions how to write down specifications in an instantiation
block are a little bit unconventional (c.f. class tutorial):

* In a binding (the name with optional type after fun, definition,
primrec, ...), you must write "f_typeconstructor" instead of "f" (in
your case, eq_silly -- the names can be inspected using the "show me
context" button in PG).

* In the specification terms, you may simply use "f" and have to make
sure that typing will it make refer to the particular type instance.

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.