Email Gateway (Aug 22 2022 at 14:32): Email Gateway (Aug 22 2022 at 14:32):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I am still experiencing some problems with friend_of_corec: It
occasionally produces "UnequalLength" exceptions and I have no idea why.
For an example, see the end of the attached file.
Cheers,
Manuel
Foo.thy
Email Gateway (Aug 22 2022 at 14:52):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Manuel,
I am still experiencing some problems with friend_of_corec: It occasionally produces "UnequalLength" exceptions and I have no idea why. For an example, see the end of the attached file.
First, I am sorry for the delay in answering your email.
I minimized your example to
codatatype 'a tree =
Node "'a tree" "'a tree"
consts tms :: "int tree \<Rightarrow> int tree"
friend_of_corec tms :: "int tree \<Rightarrow> int tree" where
"tms ys = Node (map_tree id ys) (tms ys)"
The exception is not nice; I just pushed a change to the repository version to avoid this situation. But then you get the error
"map_tree" not polymorphic enough to be applied like this and no friend
The problem is the "map_tree" call (or "lmap" in your example) applied to the argument "ys". For a function to be a friend, it must inspect its arguments only in fixed (and not well documented) ways: E.g. it may destroy them using "case", discriminators, or selectors, and it may apply a constructor or friendly function. Or it must be parametric. Unfortunately, "map_tree" is not registered as friendly and, due to its type (for reasons which I don't fully understand on the spot), it isn't recognized as potentially parametric due to its type (cf. the first conjunct in the error message). Even though all map functions are always friendly (for arguments "'a ⇒ 'a"), they are not registered by default. In your example, adding
friend_of_corec lmap :: "('a ⇒ 'a) ⇒ 'a llist ⇒ 'a llist" where
"lmap f xs = (case xs of LNil ⇒ LNil | LCons x xs' ⇒ LCons (f x) (lmap f xs'))"
(and a proof, left as an exercise to the reader) solves the problem.
Let me know if you run into further problems. I should be more reactive next time. "corec" has many rough edges and is likely to keep some of them, but I am excited to see it used and will gladly help you get your work done.
Cheers,
Jasmin
Last updated: Apr 23 2024 at 16:19 UTC