Email Gateway (Aug 18 2022 at 15:27): Email Gateway (Aug 18 2022 at 15:27):From: John Matthews <matthews@galois.com>
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.
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
instantiation silly :: eq
begin
fun "eq_class.eq" where
"eq (Silly n) (Silly m) = (m - n = 0)"
instance ..
end
The "fun" command returns the error
*** Bad name binding "eq_class.eq"
*** At command "fun".
Am I, in fact, doing something silly here?
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 15:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
begindatatype silly = Silly int
Try here, e.g.
export_code "HOL.eq :: silly => _" in Haskell file -
instantiation silly :: eq
beginfun "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
signature.asc
Email Gateway (Aug 18 2022 at 15:28):From: John Matthews <matthews@galois.com>
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
smime.p7s
Email Gateway (Aug 18 2022 at 15:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
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
signature.asc
Email Gateway (Aug 18 2022 at 15:29):From: John Matthews <matthews@galois.com>
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
smime.p7s
Email Gateway (Aug 18 2022 at 15:29):From: John Matthews <matthews@galois.com>
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"
by (simp add: eq_equals)
But I still get the same error when trying to generate Haskell code.
I've also attached the two theory files.
Thanks,
-john
Queue.thy
AQueue.thy
smime.p7s
Email Gateway (Aug 18 2022 at 15:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
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.
thanks for pointing this out.
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"
by (simp add: eq_equals)But I still get the same error when trying to generate Haskell code. I've also attached the two theory files.
Unfortunately I did not give names to those theorems (but I have
convinced myself that it should be done) -- identifying theorems by
proposition only is brittle. In such situations use the following:
lemma [code, code del]:
"(eq_class.eq :: 'a queue => _) = eq_class.eq"
by (rule refl)
This inserts a code equations which will subsume all others
syntactically, and deletes it immediately afterwards, leaving no code
equations at all.
An alternative is the list_of_queue approach I described in an earlier
e-mail:
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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC