Email Gateway (Aug 22 2022 at 15:32): Email Gateway (Aug 22 2022 at 15:32):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have a HOL function that branches on whether an element is within
the domain of a map, like so:
...
if name ∉ dom G then Some (Γ, G(name ↦ fdef)) else None
...
For testing and amusement purposes, I want to extract this code to
SML. However, trying to run export_code on this function produces a
well-sortedness error, as the type of name (a string) is not of sort
enum. Yet, it is easy to see that x ∉ dom G ⟷ G x = None:
lemma foo:
shows "x ∉ dom G ⟷ G x = None"
by auto
and replacing the test of the if-then-else with the following:
...
if G name = None then Some (Γ, G(name ↦ fdef)) else None
...
means I can now extract code to SML just fine, avoiding these
well-sortedness errors.
More generally, suppose we are working with a type of enum sort, so
that extraction of my original if-then-else succeeds. It seems in
this case that the code generator is creating very inefficient code
that tries to enumerate and test every possible value of the domain
type, rather than simply performing a single test using the fact
above, which would be much more computationally efficient.
By marking foo above as a [code_unfold], both of these problems go
away, and you get efficient code extracted no matter whether you're
working with types of sort enum, or not. Is there any reason not to
include this code_unfold lemma by default in the Isabelle library?
Thanks,
Dom
Email Gateway (Aug 22 2022 at 15:32):From: Tobias Nipkow <nipkow@in.tum.de>
The general lemma that should be used for code generation is
"a ∈ dom m ⟷ m a ≠ None"
This lemma is already in the library under the name domIff and I believe it
should indeed be used for code generation. I leave it to a code generation
expert to decide if [code_unfold] is the right attribuet (I believe it is) and
to make this change in the library.
Thanks for pointing this out.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/repos/isabelle/rev/2f7d39285a1a
Florian
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC