|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %typed combinator reduction for full-types (no S) |
|
4 |
|
5 clause( |
|
6 forall([A, B, P, Q], |
|
7 or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A)))), |
|
8 a1 ). |
|
9 |
|
10 clause( |
|
11 forall([P, T], |
|
12 or( equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T)))), |
|
13 a3 ). |
|
14 |
|
15 clause( |
|
16 forall([A, B, C, P, Q, R], |
|
17 or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B)))), |
|
18 a4 ). |
|
19 |
|
20 clause( |
|
21 forall([A, B, C, P, Q, R], |
|
22 or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C)))), |
|
23 a5 ). |
|
24 |
|
25 clause( |
|
26 forall([A, B, T], |
|
27 or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))))), |
|
28 a6 ). |
|
29 |
|
30 clause( |
|
31 forall([A, B, C, T], |
|
32 or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))))), |
|
33 a8 ). |
|
34 |
|
35 clause( |
|
36 forall([A, B, C, T], |
|
37 or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))))), |
|
38 a9 ). |
|
39 |
|
40 clause( |
|
41 forall([A, A1, B, B1, C1], |
|
42 or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))), |
|
43 a11 ). |
|
44 |
|
45 clause( |
|
46 forall([A, A2, B, B2, C2], |
|
47 or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), |
|
48 a12 ). |
|
49 |
|
50 clause( |
|
51 forall([A1, A2, B1, B2, C1, C2], |
|
52 or( not(equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), |
|
53 a15 ). |
|
54 |
|
55 clause( |
|
56 forall([A, X, Y], |
|
57 or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))), |
|
58 equal(typeinfo(X,A),typeinfo(Y,A)))), |
|
59 a16 ). |
|
60 |
|
61 clause( |
|
62 forall([A, X, Y], |
|
63 or( not(equal(typeinfo(X,A),typeinfo(Y,A))), |
|
64 hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))), |
|
65 a17 ). |
|
66 |