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

  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 ...


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

    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


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?


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

datatype silly = Silly int

Try here,  e.g.

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

instantiation silly :: eq

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

instance ..


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,



PGP available:

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

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