Discussion:
[isabelle] pairs and friends
(too old to reply)
Thomas Sternagel
2016-09-30 10:20:15 UTC
Permalink
Dear mailing list,

In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
below I get the following error message:

Cannot have type variable "'a" in the argument types when it does not
occur in the result type

Now "'a" clearly appears in the result type, so I don't see what is
going wrong.

theory Foo
imports
"~~/src/HOL/Library/Stream"
"~~/src/HOL/Library/BNF_Corec"
begin
primcorec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

friend_of_corec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

end

Cheers,
Tom
Jasmin Blanchette
2016-09-30 10:49:15 UTC
Permalink
Dear Thomas,
Post by Thomas Sternagel
In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
Cannot have type variable "'a" in the argument types when it does not
occur in the result type
I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.

Cheers,

Jasmin
Thomas Sternagel
2016-09-30 13:05:37 UTC
Permalink
I see. Have a nice vacation. I will try to figure something out.
Thanks,
Tom
Post by Jasmin Blanchette
Dear Thomas,
Post by Thomas Sternagel
In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
Cannot have type variable "'a" in the argument types when it does not
occur in the result type
I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.
Cheers,
Jasmin
Dmitriy Traytel
2016-09-30 14:24:18 UTC
Permalink
Hi Tom,

an admittedly ugly temporary workaround is to use a separate codatatype for streams of pairs:

codatatype 'a pairstream = SCons (shd: "'a × 'a") (stl: "'a pairstream”)

corecursive (friend) foo :: "'a list ⇒ 'a pairstream ⇒ 'a pairstream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"
unfolding relator_eq[symmetric] by transfer_prover

Cheers,
Dmitriy
Post by Jasmin Blanchette
Dear Thomas,
Post by Thomas Sternagel
In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
Cannot have type variable "'a" in the argument types when it does not
occur in the result type
I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.
Cheers,
Jasmin
Thomas Sternagel
2016-10-03 07:30:22 UTC
Permalink
Thanks for the tip, Dmitriy. I will try it.

Cheers,
Tom
Post by Dmitriy Traytel
Hi Tom,
codatatype 'a pairstream = SCons (shd: "'a × 'a") (stl: "'a pairstream”)
corecursive (friend) foo :: "'a list ⇒ 'a pairstream ⇒ 'a pairstream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"
unfolding relator_eq[symmetric] by transfer_prover
Cheers,
Dmitriy
Post by Jasmin Blanchette
Dear Thomas,
Post by Thomas Sternagel
In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
Cannot have type variable "'a" in the argument types when it does not
occur in the result type
I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.
Cheers,
Jasmin
Loading...