Email Gateway (Aug 22 2022 at 16:18): Email Gateway (Aug 22 2022 at 16:18):From: Brandon Bohrer <bbohrer@cs.cmu.edu>
Hi All,
I'm currently generating code from Isabelle definitions that use " 'a set"
(where 'a::{finite,enum}).
When I run it I get exceptions because the generated code for Set.image
(i.e. f ` set) has a non-exhaustive pattern-match, which is difficult to
avoid for infinite types but in principle should be avoidable for
enumeration types (since the coset constructor is redundant with the set
constructor).
Does anyone know of a way to code-generate an exhaustive implementation for
Set.image for finite/enumeration types, without implementing my own
finite/cofinite-set data structure from scratch?
If I code-generate to Scala, I can hack the resulting code to be exhaustive
by matching on types at runtime, but (a) I'd rather avoid hacks and (b) I
may want to generate SML instead, where such hacks do not work as well.
I've attached a trivial example that reproduces the exception. The SML file
generated from the Isabelle theory raises Match on start. For good measure,
I've also included an SML file demonstrating the hacky solution.
Thanks!
-Brandon
Codegen_Exploder.thy
Exploder.sml
Exploder_Hack.sml
Email Gateway (Aug 22 2022 at 16:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Brandon,
To implement set image for an arbitrary function, I don't see any way other than first
converting the complement representation into an explicit list of the elements. You can
use the type class enum for that. For example:
lemma set_fold_remove1:
"distinct ys ⟹ set (fold remove1 xs ys) = set ys - set xs"
by(induction xs arbitrary: ys) auto
lemma coset_enum:
"List.coset xs = set (fold remove1 xs Enum.enum)"
by(auto simp add: set_fold_remove1 enum_distinct UNIV_enum[symmetric])
lemma image_coset [code]:
"f ` List.coset xs = set (map f (fold remove1 xs Enum.enum))"
by(simp only: coset_enum set_map)
Now image has two code equations, one for set and one for coset. However, you can no
longer use image on sets whose element types are not enumerable, i.e., an instance of the
enum type class.
If you want to have both, then you have to do a bit more work. Basically you must
implement in HOL the type tests that you do manually in Scala. The theory Collection_Enum
in my AFP entry Containers does this and uses it for set comprehensions. There's currently
no setup for set complement, but it would not be hard to do so.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 16:19):From: Brandon Bohrer <bbohrer@cs.cmu.edu>
I'm currently using sets only for enumeration types, so your code worked
perfectly. Many thanks!
Last updated: Apr 26 2024 at 08:19 UTC