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, X, Y], |
|
27 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))), |
|
28 equal(typeinfo(X,A),typeinfo(Y,A)))), |
|
29 a6 ). |
|
30 |
|
31 clause( |
|
32 forall([A, X, Y], |
|
33 or( not(equal(typeinfo(X,A),typeinfo(Y,A))), |
|
34 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)))), |
|
35 a7 ). |
|
36 |
|