Re: [isabelle] primcorec complains about invalid map function



Hi Andreas,

> It would certainly have saved me some work it the BNF package did not omit the dead variables in the map function (I have also generalised the relator, so that would be the next thing). But I need them only for the lifting package, I have not yet used them in other cases. So, if there will be some integration of BNF and lifting, then that's definitely worth thinking about; otherwise, I suggest that we need more evidence of this being useful before someone starts to implement special cases for dead type variables.

It occurred to me that it might be cleaner if you define a map function that affects only the deads and then use function composition with the BNF-generated "map" to obtain the map function you need for Lifting. (Whether this actually improves things or makes your life more miserable is an open question, admittedly.)

Now to your actual problem:

> codatatype 'a foobar = AA 'a | BB "bool => 'a foobar"
> 
> primcorec fbind :: "'a foobar => ('a => 'b foobar) => 'b foobar"
> where "fbind f g = (if is_AA f then g (un_AA f) else BB (%b. fbind (un_BB f b) g))"
> 
> datatype_new ('a, 'c, 'e) foo = A 'a | B "'c => 'e"
> 
> codatatype ('a, 'c) bar = Bar "('a, 'c, ('a, 'c) bar) foo foobar"
> 
> [...] The following attempt raises an exception that says something about Inr () (but there are no unit types anywhere in my spec ???).
> 
> *** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
> *** mk_split: bad body type
> *** Inr ()
> *** At command "primcorec"
> 
> primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
> where
>  "un_Bar (bbind r f) =
>   map_foobar (map_foo id (case_sum id (split bbind)))
>     (fbind (un_Bar r)
>      (case_foo
>        (map_foobar (map_foo id Inl) o un_Bar o f)
>        (%c. AA (B (%i. Inr (c i, f))))))"

This is currently not supported, because "sum" is an old-style datatype and "primrec" can only deal with new-style "case"s. (It wouldn't be hard to hard-code something for sums and products on our side, though.)

With the repository version: If you make sure that changes 1401434a7e83, f09037306f25, 3d2c97392e25, and 5ebf832b58a1 are applied, and you define your own sum "datatype_new" (or "codatatype" if you are so inclined), both the above example and the example below will work. (In fact, the naming "case_sum" in your example suggests that you are using a new-style datatype, if it's not a typo.)

Considering that we have 340 working instances of "primcorec" in Isabelle, the AFP, and a semi-private repository [*], I'm amazed that you managed to produce an example that triggered so many bugs at once. The combination of "split" not followed by a lambda + a case inside a map function argument was simply toxic. I hope you feel slightly guilty for shaming us [**] publicly like that. ;)

All right: Thanks for your patience and for taking the time to file in the bug report!

Cheers,

Jasmin

[*] https://bitbucket.org/traytel/co-rec
[**] or rather: me. I can't even blame Lorenz or Dmitriy; all the bugs were clearly mine.





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