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



I'm currently using sets only for enumeration types, so your code worked
perfectly. Many thanks!

On Wed, Oct 25, 2017 at 2:53 AM, Andreas Lochbihler <
andreas.lochbihler at inf.ethz.ch> wrote:

> 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.