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 ... endThen 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 endI'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 enforcethat my definition of (==) is sound, i.e. it implements logical equality.the system is setup in a way that instantiation of the eq class happensin 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'mrunning 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 intTry 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 .. endThe 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
Description: S/MIME cryptographic signature