CTree.hascasl.output revision ad187062b0009820118c1b773a232e29b879a2fa
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedervars a, b : Type
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedergenerated type Set a ::= empty | add a (Set a)
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maedergenerated type Sys b ::= node b (Set (Sys b))
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedergenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederfree type L ::= abs (L -> L)
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederfree type Tree a b ::= leaf b | branch (a -> Tree a b)
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederfree type List a ::= nil | cons (a; List a)
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederfree type Tree a b ::= leaf a | branch (b -> List (Tree a b))
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedervars f : a -> c; g : (b -> List c) -> c; x : a;
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder s : b -> List (Tree a b)
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder. fold f g (leaf x) = f x
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder. def fold f g (branch s);
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder%% Type Constructors -----------------------------------------------------
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder: Type -> Type
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder %[generated type CTree(a : Type) ::=
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder leaf (a) | branch (Nat ->? CTree a)]%
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian MaederL : Type %[free type L ::= abs (L -> L)]%
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder: Type -> Type
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder %[free type List(a : Type) ::= nil | cons (a; List a)]%
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder: Type -> Type
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder %[generated type Set(a : Type) ::= empty | add (a) (Set a)]%
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder: Type -> Type
62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder %[generated type Sys(b : Type) ::= node (b) (Set (Sys b))]%
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder: Type -> Type -> Type
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder %[free type Tree(a : Type)(b : Type) ::=
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder leaf (a) | branch (b -> List (Tree a b))]%
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder%% Type Variables --------------------------------------------------------
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maedera : Type %(var_5)%
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederb : Type %(var_2)%
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederc : Type %(var_12)%
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder%% Assumptions -----------------------------------------------------------
975642b989852fc24119c59cf40bc1af653608ffChristian Maederabs : (L -> L) -> L %(constructor)%
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederadd : forall a : Type . a -> Set a -> Set a %(constructor)%
975642b989852fc24119c59cf40bc1af653608ffChristian Maederbranch : forall a : Type . (Nat ->? CTree a) -> CTree a
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder %(constructor)%
975642b989852fc24119c59cf40bc1af653608ffChristian Maederbranch : forall a : Type; b : Type
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . (b -> List (Tree a b)) -> Tree a b
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder %(constructor)%
975642b989852fc24119c59cf40bc1af653608ffChristian Maederbranch : forall a : Type; b : Type . (a -> Tree a b) -> Tree a b
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder %(constructor)%
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedercons : forall a : Type . a * List a -> List a %(constructor)%
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederempty : forall a : Type . Set a %(constructor)%
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederfold : forall b : Type; a : Type; c : Type
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederleaf : forall a : Type . a -> CTree a %(constructor)%
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederleaf : forall a : Type; b : Type . a -> Tree a b %(constructor)%
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedernil : forall a : Type . List a %(constructor)%
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedernode : forall b : Type . b -> Set (Sys b) -> Sys b %(constructor)%
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder%% Variables -------------------------------------------------------------
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederg : (b -> List c) -> c
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeders : b -> List (Tree a b)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder%% Sentences -------------------------------------------------------------
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedergenerated type Set(a : Type) ::= empty | add (a) (Set a) %(ga_Set)%
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maedergenerated type Sys(b : Type) ::= node (b) (Set (Sys b)) %(ga_Sys)%
fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maedergenerated type CTree(a : Type) ::=
25612a7b3ce708909298d5426406592473880a20Christian Maeder leaf (a) | branch (Nat ->? CTree a) %(ga_CTree)%
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederfree type L ::= abs (L -> L) %(ga_L)%
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederfree type Tree(a : Type)(b : Type) ::=
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder leaf (b) | branch (a -> Tree a b) %(ga_Tree)%
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maederfree type List(a : Type) ::= nil | cons (a; List a) %(ga_List)%
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederfree type Tree(a : Type)(b : Type) ::=
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder leaf (a) | branch (b -> List (Tree a b)) %(ga_Tree)%
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederfold f g ((leaf : a -> Tree a b) x) = f x
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederdef fold f g ((branch : (b -> List (Tree a b)) -> Tree a b) s)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder%% Diagnostics -----------------------------------------------------------
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder### Hint 1.6, is type variable 'a'
18b709ce961d68328da768318dcc70067f066d86Christian Maeder### Hint 1.8, is type variable 'b'
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder### Hint 6.5, is type variable 'a'
18b709ce961d68328da768318dcc70067f066d86Christian Maeder### Hint 6.5, rebound type variable 'a'
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder### Warning 15.24, overlapping declaration of 'leaf'
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder### Hint 15.11, redeclared type 'Tree'
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder### Hint 17.5, is type variable 'c'
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder### Hint 20.8, not a class 'a'
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder### Hint 20.8, not a class 'c'
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder### Hint 20.20, not a kind '(b -> List c) -> c'
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder### Hint 20.44, not a class 'a'
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder### Hint 20.51, not a kind 'b -> List (Tree a b)'
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder### Hint 21.13, in type of '(op leaf : forall a : Type . a -> CTree a)'
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder typename 'CTree' (7.16)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder is not unifiable with type 'Tree _v23_a' (18.47)
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder### Hint 22.18, in type of '(op branch : forall a : Type . (Nat ->? CTree a) -> CTree a)'
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder typename 'CTree' (7.16)
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder is not unifiable with type 'Tree _v55_a' (18.47)
18b709ce961d68328da768318dcc70067f066d86Christian Maeder### Hint, in type of '(var s : b -> List (Tree a b))'
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski typename 'List' (20.58)
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder is not unifiable with type 'Tree b' (20.53)
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder### Hint 22.25, untypable term (with type: _v55_a -> Tree _v55_a _v57_b)