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



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

Attachment: Codegen_Exploder.thy
Description: Binary data

Attachment: Exploder.sml
Description: application/smil

Attachment: Exploder_Hack.sml
Description: application/smil



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