ListEx.hascasl.output revision a59f2017dfc311ece7afcea3e8a3ceceac77ba5a
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maedertype List(a : +Type);
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List a ::= Nil | Cons (head : a; tail : List a);
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederfree type List a ::= Nil | Cons (head : a; tail : List b);
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List a ::= Nil | Cons (head : a; tail : List a b);
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederfree type List a ::= Nil | Cons (head : a; tail : List (List a));
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maederfree type Tree a ::= Leaf | Branch (head : Tree a; tail : Tree a);
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski{type Tree1(a : +Type)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder ::= Leaf | Branch (head : Tree a; tail : Tree1 a);
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowskitype Tree2(a : +Type)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder ::= Leaf | Branch (head : Tree a; tail : Tree2 a);
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskieven a ::= rek (odd a);
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederodd a ::= rek (even a);
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedereven2 a ::= rek (odd2 (odd2 a));
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiodd2 a ::= rek (even2 a);
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%% Type Constructors -----------------------------------------------------
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: +Type -> Type
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %[free type List(a : +Type) ::=
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Cons : a * List a -> List a(head : a; tail : List a)]%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: +Type -> Type
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder %[free type Tree(a : +Type) ::=
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Leaf : Tree a
cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maeder Branch : Tree a * Tree a -> Tree a(head : Tree a; tail : Tree a)]%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder: +Type -> Type
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %[generated type Tree1(a : +Type) ::=
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Leaf : Tree1 a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Branch : Tree a * Tree1 a -> Tree1 a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (head : Tree a; tail : Tree1 a)]%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder: +Type -> Type
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %[type Tree2(a : +Type) ::=
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder Leaf : Tree2 a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Branch : Tree a * Tree2 a -> Tree2 a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (head : Tree a; tail : Tree2 a)]%
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder: +Type -> Type
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder %[free type even(a : +Type) ::= rek : odd a -> even a(odd a)]%
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedereven2 : +Type -> Type %(data type)%
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder: +Type -> Type
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder %[free type odd(a : +Type) ::= rek : even a -> odd a(even a)]%
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder: +Type -> Type
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %[free type odd2(a : +Type) ::= rek : even2 a -> odd2 a(even2 a)]%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%% Type Variables --------------------------------------------------------
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskia : +Type %(var_2)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskib : Type %(var_1)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%% Assumptions -----------------------------------------------------------
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree a * Tree2 a -> Tree2 a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%(construct Tree2)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree a * Tree1 a -> Tree1 a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%(construct Tree1)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder: forall a : +Type . Tree a * Tree a -> Tree a %(construct Tree)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederCons : forall a : +Type . a * List a -> List a %(construct List)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree2 a %(construct Tree2)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree1 a %(construct Tree1)%
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder: forall a : +Type . Tree a %(construct Tree)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiNil : forall a : +Type . List a %(construct List)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree2 a -> Tree a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%(select from Tree2 constructed by
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiBranch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree1 a -> Tree a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%(select from Tree1 constructed by
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiBranch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree a -> Tree a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%(select from Tree constructed by
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiBranch : forall a : +Type . Tree a * Tree a -> Tree a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . List a -> a
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder%(select from List constructed by
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederCons : forall a : +Type . a * List a -> List a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . even2 a -> odd2 a %(construct odd2)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . even a -> odd a %(construct odd)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . odd a -> even a %(construct even)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree2 a -> Tree2 a
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder%(select from Tree2 constructed by
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederBranch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)%
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder: forall a : +Type . Tree1 a -> Tree1 a
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder%(select from Tree1 constructed by
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiBranch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . Tree a -> Tree a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%(select from Tree constructed by
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederBranch : forall a : +Type . Tree a * Tree a -> Tree a)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski: forall a : +Type . List a -> List a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%(select from List constructed by
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCons : forall a : +Type . a * List a -> List a)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%% Sentences -------------------------------------------------------------
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiforall a : +Type; x_1_1 : a; x_1_2 : List a .
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(op head : forall a : +Type . List a -> a) (Cons (x_1_1, x_1_2)) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederx_1_1 %(ga_select_head)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiforall a : +Type; x_1_1 : a; x_1_2 : List a .
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(op tail : forall a : +Type . List a -> List a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(Cons (x_1_1, x_1_2))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski= x_1_2 %(ga_select_tail)%
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List(a : +Type) ::=
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu Cons : a * List a -> List a(head : a; tail : List a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List(a : +Type) ::=
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Cons : a * List a -> List a(head : a; tail : List a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List(a : +Type) ::=
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Cons : a * List a -> List a(head : a; tail : List a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskifree type List(a : +Type) ::=
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Cons : a * List a -> List a(head : a; tail : List a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree a .
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(op head : forall a : +Type . Tree a -> Tree a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski((op Branch : forall a : +Type . Tree a * Tree a -> Tree a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (x_1_1, x_1_2))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski= x_1_1 %(ga_select_head)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree a .
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(op tail : forall a : +Type . Tree a -> Tree a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski((op Branch : forall a : +Type . Tree a * Tree a -> Tree a)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (x_1_1, x_1_2))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski= x_1_2 %(ga_select_tail)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederfree type Tree(a : +Type) ::=
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Leaf : Tree a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Branch : Tree a * Tree a -> Tree a(head : Tree a; tail : Tree a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree1 a .
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder(op head : forall a : +Type . Tree1 a -> Tree a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder((op Branch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (x_1_1, x_1_2))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder= x_1_1 %(ga_select_head)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree1 a .
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder(op tail : forall a : +Type . Tree1 a -> Tree1 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder((op Branch : forall a : +Type . Tree a * Tree1 a -> Tree1 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (x_1_1, x_1_2))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder= x_1_2 %(ga_select_tail)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedergenerated type Tree1(a : +Type) ::=
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Leaf : Tree1 a
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Branch : Tree a * Tree1 a -> Tree1 a
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (head : Tree a; tail : Tree1 a) %(ga_Tree1)%
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree2 a .
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder(op head : forall a : +Type . Tree2 a -> Tree a)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu((op Branch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (x_1_1, x_1_2))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder= x_1_1 %(ga_select_head)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederforall a : +Type; x_1_1 : Tree a; x_1_2 : Tree2 a .
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder(op tail : forall a : +Type . Tree2 a -> Tree2 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder((op Branch : forall a : +Type . Tree a * Tree2 a -> Tree2 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (x_1_1, x_1_2))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder= x_1_2 %(ga_select_tail)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype Tree2(a : +Type) ::=
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Leaf : Tree2 a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Branch : Tree a * Tree2 a -> Tree2 a(head : Tree a; tail : Tree2 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederfree type even(a : +Type) ::= rek : odd a -> even a(odd a)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederfree type odd(a : +Type) ::= rek : even a -> odd a(even a)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder %(ga_even_odd)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederfree type odd2(a : +Type) ::= rek : even2 a -> odd2 a(even2 a)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %(ga_even2_odd2)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%% Diagnostics -----------------------------------------------------------
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 1.5, is type variable 'b'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 2.5, is type variable 'a'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 3.11, rebound type variable 'a'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 4.16, rebound type variable 'a'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 4.11, redeclared type 'List'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 5.16, rebound type variable 'a'
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder*** Error 5.50-5.55, unbound type variable(s)
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder b in 'List b'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 6.16, rebound type variable 'a'
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder*** Error 6.50-6.57, unexpected type argument 'b'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Hint 7.16, rebound type variable 'a'
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu*** Error 7.50-7.61, illegal polymorphic recursion
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu expected: List a
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu found: List (List a)
da955132262baab309a50fdffe228c9efe68251dCui Jian### Hint 9.16, rebound type variable 'a'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu### Hint 10.22, rebound type variable 'a'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu### Hint 11.12, rebound type variable 'a'
da955132262baab309a50fdffe228c9efe68251dCui Jian### Hint 13.16, rebound type variable 'a'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu### Hint 13.39, rebound type variable 'a'
da955132262baab309a50fdffe228c9efe68251dCui Jian### Hint 14.17, rebound type variable 'a'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu### Hint 14.49, rebound type variable 'a'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu*** Error 14.27-14.38, illegal polymorphic recursion
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder expected: odd2 a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder found: odd2 (odd2 a)