ListEx.hascasl.output revision 9292a012760925eeb69ee23666f70592be6031b6
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskitype List(a : +Type)
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskifree type List a ::= Nil | Cons (head : a; tail : List a)
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederfree type List a ::= Nil | Cons (head : a; tail : List b)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederfree type List a ::= Nil | Cons (head : a; tail : List a b)
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederfree type List a ::= Nil | Cons (head : a; tail : List (List a))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederfree type Tree a ::= Leaf | Branch (head : Tree a; tail : Tree a)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder{type Tree1(a : +Type)
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski ::= Leaf | Branch (head : Tree a; tail : Tree1 a)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype Tree2(a : +Type)
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski ::= Leaf | Branch (head : Tree a; tail : Tree2 a)
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskieven a ::= rek (odd a);
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiodd a ::= rek (even a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedereven2 a ::= rek (odd2 (odd2 a));
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederodd2 a ::= rek (even2 a)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder%% Type Constructors -----------------------------------------------------
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder: +Type -> Type
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder %[free type List(a : +Type) ::=
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Cons : a * List a -> List a(head : a; tail : List a)]%
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder: +Type -> Type
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski %[free type Tree(a : +Type) ::=
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Leaf : Tree a
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder Branch : Tree a * Tree a -> Tree a(head : Tree a; tail : Tree a)]%
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder: +Type -> Type
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder %[generated type Tree1(a : +Type) ::=
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Leaf : Tree1 a
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Branch : Tree a * Tree1 a -> Tree1 a
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (head : Tree a; tail : Tree1 a)]%
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder: +Type -> Type
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski %[type Tree2(a : +Type) ::=
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Leaf : Tree2 a
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Branch : Tree a * Tree2 a -> Tree2 a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (head : Tree a; tail : Tree2 a)]%
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder: +Type -> Type
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich %[free type even(a : +Type) ::= rek : odd a -> even a(odd a)]%
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luetticheven2 : +Type -> Type %(data type)%
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich: +Type -> Type
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder %[free type odd(a : +Type) ::= rek : even a -> odd a(even a)]%
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski: +Type -> Type
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder %[free type odd2(a : +Type) ::= rek : even2 a -> odd2 a(even2 a)]%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder%% Type Variables --------------------------------------------------------
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedera : +Type %(var_2)%
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescub : Type %(var_1)%
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder%% Assumptions -----------------------------------------------------------
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder: forall a : +Type . Tree a * Tree2 a -> Tree2 a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder%(construct Tree2)%
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder: forall a : +Type . Tree a * Tree1 a -> Tree1 a
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder%(construct Tree1)%
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder: forall a : +Type . Tree a * Tree a -> Tree a %(construct Tree)%
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederCons : forall a : +Type . a * List a -> List a %(construct List)%
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder: forall a : +Type . Tree2 a %(construct Tree2)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder: forall a : +Type . Tree1 a %(construct Tree1)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder: forall a : +Type . Tree a %(construct Tree)%
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederNil : forall a : +Type . List a %(construct List)%
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder: forall a : +Type . Tree2 a -> Tree a
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder%(select from Tree2 constructed by
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederBranch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)%
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder: forall a : +Type . Tree1 a -> Tree a
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder%(select from Tree1 constructed by
d79e02625778d20a5458078f979ff74aac67db61Christian MaederBranch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)%
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder: forall a : +Type . Tree a -> Tree a
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder%(select from Tree constructed by
d79e02625778d20a5458078f979ff74aac67db61Christian MaederBranch : forall a : +Type . Tree a * Tree a -> Tree a)%
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder: forall a : +Type . List a -> a
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder%(select from List constructed by
d79e02625778d20a5458078f979ff74aac67db61Christian MaederCons : forall a : +Type . a * List a -> List a)%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder: forall a : +Type . even2 a -> odd2 a %(construct odd2)%
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder: forall a : +Type . even a -> odd a %(construct odd)%
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder: forall a : +Type . odd a -> even a %(construct even)%
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder: forall a : +Type . Tree2 a -> Tree2 a
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder%(select from Tree2 constructed by
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederBranch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder: forall a : +Type . Tree1 a -> Tree1 a
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder%(select from Tree1 constructed by
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiBranch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)%
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski: forall a : +Type . Tree a -> Tree a
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski%(select from Tree constructed by
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederBranch : forall a : +Type . Tree a * Tree a -> Tree a)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder: forall a : +Type . List a -> List a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder%(select from List constructed by
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederCons : forall a : +Type . a * List a -> List a)%
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder%% Sentences -------------------------------------------------------------
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederforall a : +Type; x_1_1 : a; x_1_2 : List a .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder(op head : forall a : +Type . List a -> a) (Cons (x_1_1, x_1_2)) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederx_1_1 %(ga_select_head)%
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederforall a : +Type; x_1_1 : a; x_1_2 : List a .
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder(op tail : forall a : +Type . List a -> List a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski(Cons (x_1_1, x_1_2))
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder= x_1_2 %(ga_select_tail)%
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskifree type List(a : +Type) ::=
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Cons : a * List a -> List a(head : a; tail : List a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederfree type List(a : +Type) ::=
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Cons : a * List a -> List a(head : a; tail : List a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederfree type List(a : +Type) ::=
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Cons : a * List a -> List a(head : a; tail : List a)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maederfree type List(a : +Type) ::=
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Cons : a * List a -> List a(head : a; tail : List a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree a .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder(op head : forall a : +Type . Tree a -> Tree a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder((op Branch : forall a : +Type . Tree a * Tree a -> Tree a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (x_1_1, x_1_2))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder= x_1_1 %(ga_select_head)%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree a .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder(op tail : forall a : +Type . Tree a -> Tree a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder((op Branch : forall a : +Type . Tree a * Tree a -> Tree a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (x_1_1, x_1_2))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder= x_1_2 %(ga_select_tail)%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederfree type Tree(a : +Type) ::=
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Leaf : Tree a
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Branch : Tree a * Tree a -> Tree a(head : Tree a; tail : Tree a)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree1 a .
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder(op head : forall a : +Type . Tree1 a -> Tree a)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder((op Branch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (x_1_1, x_1_2))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder= x_1_1 %(ga_select_head)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree1 a .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder(op tail : forall a : +Type . Tree1 a -> Tree1 a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder((op Branch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (x_1_1, x_1_2))
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder= x_1_2 %(ga_select_tail)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedergenerated type Tree1(a : +Type) ::=
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Leaf : Tree1 a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Branch : Tree a * Tree1 a -> Tree1 a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (head : Tree a; tail : Tree1 a) %(ga_Tree1)%
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree2 a .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder(op head : forall a : +Type . Tree2 a -> Tree a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder((op Branch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (x_1_1, x_1_2))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder= x_1_1 %(ga_select_head)%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree2 a .
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski(op tail : forall a : +Type . Tree2 a -> Tree2 a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski((op Branch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (x_1_1, x_1_2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski= x_1_2 %(ga_select_tail)%
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype Tree2(a : +Type) ::=
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Leaf : Tree2 a
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Branch : Tree a * Tree2 a -> Tree2 a(head : Tree a; tail : Tree2 a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskifree type even(a : +Type) ::= rek : odd a -> even a(odd a)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskifree type odd(a : +Type) ::= rek : even a -> odd a(even a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder %(ga_even_odd)%
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederfree type odd2(a : +Type) ::= rek : even2 a -> odd2 a(even2 a)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder %(ga_even2_odd2)%
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski%% Diagnostics -----------------------------------------------------------
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 1.5, is type variable 'b'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 2.5, is type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 3.11, rebound type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 4.16, rebound type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 4.11, redeclared type 'List'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 5.16, rebound type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Error 5.50-5.55, unbound type variable(s)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder b in 'List b'
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder### Hint 6.16, rebound type variable 'a'
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder*** Error 6.50-6.57, unexpected type argument 'b'
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder### Hint 7.16, rebound type variable 'a'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski*** Error 7.50-7.61, illegal polymorphic recursion
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski expected: List a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder found: List (List a)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 9.16, rebound type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 10.22, rebound type variable 'a'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder### Hint 11.12, rebound type variable 'a'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski### Hint 13.16, rebound type variable 'a'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder### Hint 13.39, rebound type variable 'a'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder### Hint 14.17, rebound type variable 'a'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder### Hint 14.49, rebound type variable 'a'
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder*** Error 14.27-14.38, illegal polymorphic recursion
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder expected: odd2 a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder found: odd2 (odd2 a)