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 methodfor 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" by (simp add: AQueue_def) 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
Description: S/MIME cryptographic signature