BasicSpec.hascasl.output revision a39a820684c1974350f46593025e0bb279f41bc6
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksatype Unit : TYPE
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucclasses a, b, c;
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucprogram tt = \ x : s . ();
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucfst (x : s, y : t) : s = x;
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucsnd (x : s, y : t) : t = y;
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksapred eq : s * s
1da120eb84c9d3ed16f64d6defd9bc30569dc45bChristian Maederforall x : t; y : t
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucop a : (? s)
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luctype Data1 ::= a | b | c
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc ::= Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | type Data1
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |
1da120eb84c9d3ed16f64d6defd9bc30569dc45bChristian Maeder Cons32 (sel2 :? Data2; sel1 :? Data1)
40988f50f3e378a38ab97702f6cc69fc7f43be6fmcodescu ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |
c4e7779ca2224fd41d86c88dd9d4c5e383eec7d7Christian Maeder Cons42 (sel2 :? Data2; sel1 :? Data1)?
c4e7779ca2224fd41d86c88dd9d4c5e383eec7d7Christian Maeder%% Classes ---------------------------------------------------------------
1da120eb84c9d3ed16f64d6defd9bc30569dc45bChristian Maeder%% Type Constructors -----------------------------------------------------
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl LucData1 : Type < Data2 %[type Data1 ::= a | b | c]%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc %[type Data2 ::=
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc types Data1 | Cons21 (Data1; Data2) | Cons22 (Data2; Data1)]%
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc %[type Data3 ::=
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc Cons31 (sel1 :? Data1; sel2 :? Data2) |
2aa433939988fc34e3968ae0363fe628374fb3d2Karl Luc Cons32 (sel2 :? Data2; sel1 :? Data1)]%
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luc %[type Data4 ::=
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa Cons41 (sel1 :? Data1; sel2 :? Data2)? |
b9d9f251715a0786afc39a7a79e3ec3cc62a697fChristian Maeder Cons42 (sel2 :? Data2; sel1 :? Data1)?]%
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luc%% Type Variables --------------------------------------------------------
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksat : Type %(var_1)%
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa%% Assumptions -----------------------------------------------------------
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaCons21 : Data1 * Data2 -> Data2 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaCons22 : Data2 * Data1 -> Data2 %(constructor)%
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen KuksaCons31 : Data1 * Data2 -> Data3 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaCons32 : Data2 * Data1 -> Data3 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaCons41 : Data1 * Data2 ->? Data4 %(constructor)%
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen KuksaCons42 : Data2 * Data1 ->? Data4 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaa : Data1 %(constructor)%
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luca : ? s %(op)%
2aa433939988fc34e3968ae0363fe628374fb3d2Karl Lucb : Data1 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksac : Data1 %(constructor)%
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaeq : s * s ->? Unit %(pred)%
08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksafst : s * t ->? s %(op)%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucsel1 : Data3 ->? Data1
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa %(selector of constructor(s)
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc (Cons31 : Data1 * Data2 -> Data3,
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc Cons32 : Data2 * Data1 -> Data3))%
b9d9f251715a0786afc39a7a79e3ec3cc62a697fChristian Maedersel1 : Data4 ->? Data1
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa %(selector of constructor(s)
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa (Cons41 : Data1 * Data2 ->? Data4,
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc Cons42 : Data2 * Data1 ->? Data4))%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucsel2 : Data3 ->? Data2
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc %(selector of constructor(s)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (Cons31 : Data1 * Data2 -> Data3,
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc Cons32 : Data2 * Data1 -> Data3))%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucsel2 : Data4 ->? Data2
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc %(selector of constructor(s)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (Cons41 : Data1 * Data2 ->? Data4,
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa Cons42 : Data2 * Data1 ->? Data4))%
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksasnd : s * t ->? t %(op)%
b9d9f251715a0786afc39a7a79e3ec3cc62a697fChristian Maedertt : s ->? Unit %(pred)%
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa%% Variables -------------------------------------------------------------
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc%% Sentences -------------------------------------------------------------
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucprogram tt = (\ x . ()) : s ->? Unit %(pe_tt)%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucprogram (var fst : s * t ->? s) (x, y : t) : s = x %(pe_fst)%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucprogram (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luctype Data1 ::= a | b | c %(ga_Data1)%
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksatype Data2 ::=
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luc types Data1 | Cons21 (Data1; Data2) | Cons22 (Data2; Data1)
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc %(ga_Data2)%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucforall x_1_1 : Data1; x_1_2 : Data2
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc. (op sel1 : Data3 ->? Data1) (Cons31 (x_1_1, x_1_2)) = x_1_1
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc %(ga_select_sel1)%
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Lucforall x_1_1 : Data1; x_1_2 : Data2
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc. (op sel2 : Data3 ->? Data2) (Cons31 (x_1_1, x_1_2)) = x_1_2
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc %(ga_select_sel2)%
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Lucforall x_1_1 : Data2; x_1_2 : Data1
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc. (op sel2 : Data3 ->? Data2) (Cons32 (x_1_1, x_1_2)) = x_1_1
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc %(ga_select_sel2)%
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucforall x_1_1 : Data2; x_1_2 : Data1
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski. (op sel1 : Data3 ->? Data1) (Cons32 (x_1_1, x_1_2)) = x_1_2
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski %(ga_select_sel1)%
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowskitype Data3 ::=
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski Cons31 (sel1 :? Data1; sel2 :? Data2) |
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski Cons32 (sel2 :? Data2; sel1 :? Data1) %(ga_Data3)%
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowskiforall x_1_1 : Data1; x_1_2 : Data2
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski. (op sel1 : Data4 ->? Data1) (Cons41 (x_1_1, x_1_2)) = x_1_1
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski %(ga_select_sel1)%
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowskiforall x_1_1 : Data1; x_1_2 : Data2
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski. (op sel2 : Data4 ->? Data2) (Cons41 (x_1_1, x_1_2)) = x_1_2
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski %(ga_select_sel2)%
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowskiforall x_1_1 : Data2; x_1_2 : Data1
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski. (op sel2 : Data4 ->? Data2) (Cons42 (x_1_1, x_1_2)) = x_1_1
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski %(ga_select_sel2)%
2aa433939988fc34e3968ae0363fe628374fb3d2Karl Lucforall x_1_1 : Data2; x_1_2 : Data1
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa. (op sel1 : Data4 ->? Data1) (Cons42 (x_1_1, x_1_2)) = x_1_2
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa %(ga_select_sel1)%
b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksatype Data4 ::=
b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksa Cons41 (sel1 :? Data1; sel2 :? Data2)? |
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski Cons42 (sel2 :? Data2; sel1 :? Data1)? %(ga_Data4)%
8b7e9bd07700b2fef4312835be342250347ad849Eugen Kuksa%% Diagnostics -----------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Warning 1.7, void universe class declaration 'Type'
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski### Hint 3.5, is type variable 't'
b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksa*** Error 7.11, illegal type pattern argument '__'
b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksa*** Error 11.16, not a class 'd'
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Warning 11.7, unchanged class 'a'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Warning 11.10, unchanged class 'b'
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Warning 11.13, unchanged class 'c'
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski### Hint 11.19, refined class 'a'
676bcc74ba0d2d6f8acc734bb9679b3f8de0483fTill Mossakowski### Hint 16.7, not a class 's'
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc### Hint 18.15, rebound variable 'x'
b9d9f251715a0786afc39a7a79e3ec3cc62a697fChristian Maeder### Hint 15.9-15.11, repeated declaration of 'tt' with type 's ->? Unit'
b9d9f251715a0786afc39a7a79e3ec3cc62a697fChristian Maeder*** Error 20.12, unexpected mixfix token: res
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc### Hint 21.6, rebound variable 'x'
2aa433939988fc34e3968ae0363fe628374fb3d2Karl Luc### Hint 21.6, rebound variable 'x'
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa### Warning 21.1-21.16, illegal lhs pattern '(var fst : s * t ->? s) ((var x : s), (var y : t))'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 22.6, rebound variable 'x'
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa### Hint 22.6, rebound variable 'x'
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa### Warning 22.1-22.16, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa### Hint 26.6, redeclared type 's'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 28.38-28.41, in type of '((var p : s), (pred tt : s))'
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa typename 's' (24.15)
2aa433939988fc34e3968ae0363fe628374fb3d2Karl Luc is not unifiable with type 's ->? Unit' (15.11)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 28.38-28.41, untypable term (with type: s * s)
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa*** Error 28.33, no typing for 'program all (p : ? s) : ? Unit = eq (p, tt)'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.14, rebound variable 'x'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40, no type found for 't1'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40, no type found for 't1'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40, untypable term (with type: ? (_v50 ->? _v49 ->? Unit ->? ? Unit))
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 30.40-30.42, untypable term (with type: _v50 ->? _v49 ->? Unit ->? ? Unit)
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 30.40-30.45, untypable term (with type: _v49 ->? Unit ->? ? Unit)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40, no type found for 't1'
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 30.40, no type found for 't1'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40, untypable term (with type: ? (_v52 ->? _v51 ->? ? (? Unit)))
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 30.40-30.42, untypable term (with type: _v52 ->? _v51 ->? ? (? Unit))
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40-30.45, untypable term (with type: _v51 ->? ? (? Unit))
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 30.40-30.49, untypable term (with type: ? (? Unit))
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc 't1 () res t2'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa*** Error 30.38, no typing for 'program And (x, y : ? Unit) : ? Unit = t1 () res t2 ()'
3d8bc16514ab5f8205f614ed6e02f06599c8ea29Karl Luc*** Error 32.12, unexpected mixfix token: impl
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze*** Error 34.12, unexpected mixfix token: or
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze### Hint 37.27, no type found for 'all'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 37.27, untypable term (with type: _v62 ->? ? Unit)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa*** Error 37.25, no typing for 'program ex (p : ? s) : ? Unit
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze = all \ r : ? Unit . (all \ x : s . p x impl r) impl r'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 40.20, no type found for 'all'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 40.20, untypable term (with type: _v69 ->? ? Unit)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 40.3, rebound variable 'ff'
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 40.20, no type found for 'all'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 40.20, untypable term (with type: _v70 ->? ? Unit)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa*** Error 40.18, no typing for 'program ff () : ? Unit = all \ r : ? Unit . r ()'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 45.9, not a class 't'
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luc### Hint 45.8, rebound variable 'x'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 45.16, not a class 't'
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze### Hint 57.11, redeclared type 's'
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc### Hint 62.11-62.70, repeated declaration of 'sel2' with type 'Data3 ->? Data2'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 62.11-63.1, repeated declaration of 'sel1' with type 'Data3 ->? Data1'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 64.11-64.71, repeated declaration of 'sel2' with type 'Data4 ->? Data2'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 64.11-64.84, repeated declaration of 'sel1' with type 'Data4 ->? Data1'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 66.22, not a class 's'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 66.21, rebound variable 'x'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 66.25, no type found for 'e'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa*** Error 66.25, no typing for 'e'
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc### Hint 67.9, not a class 's'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 67.8, rebound variable 'x'
e9db5c6041ef8686a248ebd0cf013e99246ed109Karl Luc### Hint 67.12, no type found for 'e'
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa*** Error 67.12, no typing for 'e'