BasicSpec.hascasl.output revision f8a1ab8012a1f36060d6ce9b63399fa4a8a2981c
10139N/Aclass Type < Type;
10139N/Avar t : Type
10139N/Aclass TYPE < Type;
10139N/Atype Unit : TYPE
10139N/Aclass a, b, c < Type;
10139N/Aclass a, b, c < Type;
10139N/A a < b;
11904N/Atype s : c
10139N/Apred tt : s
10139N/Avar x : s
10139N/Aprogram tt = \ x : s . ();
10139N/Aprogram
10139N/Afst (x : s, y : t) : s = x;
10139N/Asnd (x : s, y : t) : t = y;
11904N/Apred eq : s * s
10139N/Atype s < ? s
10139N/Aprogram
10139N/Aprogram
10139N/Aprogram
10139N/Aprogram
10139N/Aforall x : t; y : t
10139N/A
10139N/A%(..)%
10139N/A. x = y;
10139N/Asort s
11904N/Aop a : (? s)
11904N/Atype Data1 ::= a | b | c
11904N/Atype Data2
11904N/A ::= Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | type Data1
11904N/Atype Data3
11904N/A ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |
11904N/A Cons32 (sel2 :? Data2; sel1 :? Data1)
11904N/Atype Data4
11904N/A ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |
11904N/A Cons42 (sel2 :? Data2; sel1 :? Data1)?
11904N/A. true;
11904N/Aforall x : s
11904N/Aforall x : s
11904N/A%% Classes ---------------------------------------------------------------
11904N/ATYPE < Type
11904N/Aa < b
11904N/Ab < Type
11904N/Ac < Type
11904N/A%% Type Constructors -----------------------------------------------------
11904N/AData1
11904N/A: Type < Data2
11904N/A %[type Data1 ::=
11904N/A a : Data1
11904N/A b : Data1
11904N/A c : Data1]%
10139N/AData2
10139N/A: Type
10139N/A %[type Data2 ::=
10139N/A Cons21 : Data1 * Data2 -> Data2(Data1; Data2)
10139N/A Cons22 : Data2 * Data1 -> Data2(Data2; Data1)
10139N/A types Data1]%
10139N/AData3
10139N/A: Type
10139N/A %[type Data3 ::=
10139N/A Cons31 : Data1 * Data2 -> Data3(sel1 :? Data1; sel2 :? Data2)
11904N/A Cons32 : Data2 * Data1 -> Data3(sel2 :? Data2; sel1 :? Data1)]%
11904N/AData4
11904N/A: Type
10139N/A %[type Data4 ::=
11904N/A Cons41 : Data1 * Data2 ->? Data4(sel1 :? Data1; sel2 :? Data2)
11904N/A Cons42 : Data2 * Data1 ->? Data4(sel2 :? Data2; sel1 :? Data1)]%
11904N/As : (Type, c)
10139N/A%% Type Variables --------------------------------------------------------
11904N/At : Type %(var_1)%
11904N/A%% Assumptions -----------------------------------------------------------
11904N/ACons21 : Data1 * Data2 -> Data2 %(construct Data2)%
11904N/ACons22 : Data2 * Data1 -> Data2 %(construct Data2)%
11904N/ACons31 : Data1 * Data2 -> Data3 %(construct Data3)%
11904N/ACons32 : Data2 * Data1 -> Data3 %(construct Data3)%
10139N/ACons41 : Data1 * Data2 ->? Data4 %(construct Data4)%
10139N/ACons42 : Data2 * Data1 ->? Data4 %(construct Data4)%
11904N/Aa
11904N/A: Data1 %(construct Data1)%
10139N/A: ? s %(op)%
11904N/Ab : Data1 %(construct Data1)%
11904N/Ac : Data1 %(construct Data1)%
10139N/Aeq : s * s ->? Unit %(pred)%
11904N/Afst : s * t ->? s %(op)%
11904N/Asel1
10139N/A: Data4 ->? Data1
11904N/A%(select from Data4 constructed by
11904N/A(Cons42 : Data2 * Data1 ->? Data4,
11904N/A Cons41 : Data1 * Data2 ->? Data4))%
10139N/A: Data3 ->? Data1
10139N/A%(select from Data3 constructed by
11904N/A(Cons32 : Data2 * Data1 -> Data3,
11904N/A Cons31 : Data1 * Data2 -> Data3))%
11904N/Asel2
11904N/A: Data4 ->? Data2
11904N/A%(select from Data4 constructed by
11904N/A(Cons42 : Data2 * Data1 ->? Data4,
11904N/A Cons41 : Data1 * Data2 ->? Data4))%
11904N/A: Data3 ->? Data2
11904N/A%(select from Data3 constructed by
11904N/A(Cons32 : Data2 * Data1 -> Data3,
11904N/A Cons31 : Data1 * Data2 -> Data3))%
11904N/Asnd : s * t ->? t %(op)%
11904N/Att : s ->? Unit %(pred)%
10139N/A%% Variables -------------------------------------------------------------
11904N/Ax : s
11904N/Ay : t
11904N/A%% Sentences -------------------------------------------------------------
11904N/Aprogram tt = (\ x . ()) : s ->? Unit %(pe_tt)%
11904N/Aprogram (var fst : s * t ->? s) (x, y : t) : s = x %(pe_fst)%
10139N/Aprogram (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%
11904N/Ax = y
11904N/Atype Data1 ::=
11904N/A a : Data1
11904N/A b : Data1
11904N/A c : Data1 %(ga_Data1)%
11904N/Atype Data2 ::=
11904N/A Cons21 : Data1 * Data2 -> Data2(Data1; Data2)
10139N/A Cons22 : Data2 * Data1 -> Data2(Data2; Data1)
11904N/A types Data1 %(ga_Data2)%
11904N/Aforall x_1_1 : Data1; x_1_2 : Data2 .
11904N/A(op sel1 : Data3 ->? Data1) (Cons31 (x_1_1, x_1_2)) = x_1_1
10139N/A %(ga_select_sel1)%
11904N/Aforall x_1_1 : Data1; x_1_2 : Data2 .
11904N/A(op sel2 : Data3 ->? Data2) (Cons31 (x_1_1, x_1_2)) = x_1_2
11904N/A %(ga_select_sel2)%
11904N/Aforall x_1_1 : Data2; x_1_2 : Data1 .
11904N/A(op sel2 : Data3 ->? Data2) (Cons32 (x_1_1, x_1_2)) = x_1_1
11904N/A %(ga_select_sel2)%
11904N/Aforall x_1_1 : Data2; x_1_2 : Data1 .
11904N/A(op sel1 : Data3 ->? Data1) (Cons32 (x_1_1, x_1_2)) = x_1_2
11904N/A %(ga_select_sel1)%
10139N/Atype Data3 ::=
11904N/A Cons31 : Data1 * Data2 -> Data3(sel1 :? Data1; sel2 :? Data2)
11904N/A Cons32 : Data2 * Data1 -> Data3(sel2 :? Data2; sel1 :? Data1)
11904N/A %(ga_Data3)%
11904N/Aforall x_1_1 : Data1; x_1_2 : Data2 .
10139N/A(op sel1 : Data4 ->? Data1) (Cons41 (x_1_1, x_1_2)) = x_1_1
11904N/A %(ga_select_sel1)%
11904N/Aforall x_1_1 : Data1; x_1_2 : Data2 .
11904N/A(op sel2 : Data4 ->? Data2) (Cons41 (x_1_1, x_1_2)) = x_1_2
10139N/A %(ga_select_sel2)%
11904N/Aforall x_1_1 : Data2; x_1_2 : Data1 .
10139N/A(op sel2 : Data4 ->? Data2) (Cons42 (x_1_1, x_1_2)) = x_1_1
10139N/A %(ga_select_sel2)%
11904N/Aforall x_1_1 : Data2; x_1_2 : Data1 .
11904N/A(op sel1 : Data4 ->? Data1) (Cons42 (x_1_1, x_1_2)) = x_1_2
11904N/A %(ga_select_sel1)%
10139N/Atype Data4 ::=
10139N/A Cons41 : Data1 * Data2 ->? Data4(sel1 :? Data1; sel2 :? Data2)
10139N/A Cons42 : Data2 * Data1 ->? Data4(sel2 :? Data2; sel1 :? Data1)
10139N/A %(ga_Data4)%
10139N/Atrue
10139N/A%% Diagnostics -----------------------------------------------------------
10139N/A### Warning 1.7, void universe class declaration 'Type'
10139N/A### Hint 3.5, is type variable 't'
10139N/A*** Error 7.11, illegal type pattern argument '__'
10139N/A*** Error 11.16, not a class 'd'
10139N/A### Warning 11.7, unchanged class 'a'
10139N/A### Warning 11.10, unchanged class 'b'
10139N/A### Warning 11.13, unchanged class 'c'
10139N/A### Hint 11.19, refined class 'a'
10139N/A### Hint 16.7, not a class 's'
10139N/A### Hint 18.15, rebound variable 'x'
10139N/A*** Error 20.12, unexpected mixfix token: res
10139N/A### Hint 21.6, rebound variable 'x'
10139N/A### Hint 21.6, rebound variable 'x'
10139N/A### Warning 21.5-21.16, illegal lhs pattern '(var fst : s * t ->? s) ((var x : s), (var y : t))'
10139N/A### Hint 22.6, rebound variable 'x'
10139N/A### Hint 22.6, rebound variable 'x'
10139N/A### Warning 22.5-22.16, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'
10139N/A### Hint 28.41, in type of '(p, (pred tt : s))'
10139N/A typename 's' (24.15)
10139N/A is not unifiable with type 's ->? Unit' (15.11)
10139N/A
10139N/A### Hint 28.35-28.41, untypable application (with result type: ? Unit)
10139N/A 'eq (p, tt)'
10139N/A*** Error 28.33, no typing for 'program all (p : ? s) : ? Unit = eq (p, tt)'
10139N/A### Hint 30.14, rebound variable 'x'
10139N/A### Hint 30.40, no type match for: t1
10139N/A with (maximal) type: _v64 ->? _v63 ->? _v62 ->? _v61 ->? ? Unit
10139N/A known types:
10139N/A
10139N/A### Hint 30.40-30.42, untypable application (with result type: _v63 ->? _v62 ->? _v61 ->? ? Unit)
10139N/A 't1'
10139N/A### Hint 30.40-30.45, untypable application (with result type: _v62 ->? _v61 ->? ? Unit)
11904N/A 't1 res'
11904N/A### Hint 30.40-30.49, untypable application (with result type: _v61 ->? ? Unit)
11904N/A 't1 res t2'
11904N/A### Hint 30.40-30.52, untypable application (with result type: ? Unit)
10139N/A 't1 res t2 ()'
10139N/A*** Error 30.38, no typing for 'program And (x, y : ? Unit) : ? Unit = t1 res t2 ()'
11904N/A*** Error 32.12, unexpected mixfix token: impl
11904N/A*** Error 34.12, unexpected mixfix token: or
11904N/A### Hint 37.27, no type match for: all
11904N/A with (maximal) type: _v74 ->? ? Unit
11904N/A known types:
11904N/A
10139N/A### Hint 37.27-38.45, untypable application (with result type: ? Unit)
10139N/A 'all (\ r : ? Unit . all (\ x : s . p x impl r) impl r)'
10139N/A*** Error 37.25, no typing for 'program ex (p : ? s) : ? Unit =
10139N/A all (\ r : ? Unit . all (\ x : s . p x impl r) impl r)'
10139N/A### Hint 40.20, no type match for: all
10139N/A with (maximal) type: _v82 ->? ? Unit
10139N/A known types:
10139N/A
10139N/A### Hint 40.20-40.38, untypable application (with result type: ? Unit)
10139N/A 'all (\ r : ? Unit . r)'
10139N/A*** Error 40.18, no typing for 'program ff () : ? Unit = all (\ r : ? Unit . r)'
10139N/A### Hint 45.9, not a class 't'
10139N/A### Hint 45.8, rebound variable 'x'
10139N/A### Hint 45.16, not a class 't'
10139N/A### Hint 57.11, redeclared type 's'
10139N/A### Hint 66.22, not a class 's'
10139N/A### Hint 66.21, rebound variable 'x'
10139N/A### Hint 66.25, no type match for: e
10139N/A with (maximal) type: Unit
10139N/A known types:
10139N/A
10139N/A*** Error 66.25, no typing for 'e'
10139N/A### Hint 67.9, not a class 's'
10139N/A### Hint 67.8, rebound variable 'x'
10139N/A### Hint 67.12, no type match for: e
11904N/A with (maximal) type: Unit
11904N/A known types:
11904N/A
11904N/A*** Error 67.12, no typing for 'e'
11904N/A