Re: [isabelle] Non-exhaustive pattern-matching in generated code for Set.image



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

On 25/10/17 02:57, Brandon Bohrer wrote:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.