1:- module(test_trs,[]). 2
3term_expansion --> pac:expand_pac.
4
5:- use_module(misc(misc)). 6:- use_module(pac('expand-pac')). 7
13
14boole --> trs([t * X = X,
15 f * X = f,
16 t + X = t,
17 f + X = X,
18 - t = f,
19 - f = t,
20 X * Y = X0 *Y :- X = X0,
21 X * Y = X * Y0 :- Y = Y0,
22 X + Y = X0 + Y :- X = X0,
23 X + Y = X + Y0 :- Y = Y0,
24 - X = - X0 :- X = X0
25 ]).
26
29:- betrs(calc_boole). 30 t * X = X.
31 f * _ = f.
32 t + _ = t.
33 f + X = X.
34 - t = f.
35 - f = t.
36 X * Y = X0 *Y :- X = X0.
37 X * Y = X * Y0 :- Y = Y0.
38 X + Y = X0 + Y :- X = X0.
39 X + Y = X + Y0 :- Y = Y0.
40 - X = - X0 :- X = X0.
41:- etrs. 42
45:- betrs(slim_goal_in_block). 46A = call(A) :- var(A).
47(A, B) = (A0, B) :- A = A0.
48(A, B) = (A, B0) :- B = B0.
49(A; B) = (A0; B) :- A = A0.
50(A; B) = (A; B0) :- B = B0.
51(A -> B) = (A0->B) :- A = A0.
52(A -> B) = (A->B0) :- B = B0.
53\+(A) = \+(A0) :- A = A0.
54M:A = M:B :- A = B.
55(true, A) = A.
56(A, true) = A.
57(false, _A) = false.
58(true;true) = true.
59(A; false) = A.
60(false; A) = A.
61(false -> _A) = false.
62(true -> A) = A.
63\+(false) = true.
64\+(true) = false.
65(X=Y) = true :- X == Y.
66((X=Y) = false :- X \== Y, ground((X,Y))).
67(X==Y) = true :- X == Y.
68((X==Y) = false :- X \== Y, ground((X,Y))).
69nonvar(X) = true :- nonvar(X).
70var(X) = false :- nonvar(X).
71fail = false.
72[]:A = A.
73_M:(M:A) = M:A.
74_M:E = E :- reduce:prefix_cancellable(E).
75M:E = ME :- reduce:propagate_prefix(M, E, ME).
76X = Y :- reduce:slim_call(X, Y).
77:- etrs. 78
82slim_goal_in_dcg --> trs([
83A = call(A) :- var(A),
84(A, B) = (A0, B) :- A = A0,
85(A, B) = (A, B0) :- B = B0,
86(A; B) = (A0; B) :- A = A0,
87(A; B) = (A; B0) :- B = B0,
88(A -> B) = (A0->B) :- A = A0,
89(A -> B) = (A->B0) :- B = B0,
90\+(A) = \+(A0) :- A = A0,
91M:A = M:B :- A = B,
92(true, A) = A,
93(A, true) = A,
94(false, _) = false,
95(true;true) = true,
96(A; false) = A,
97(false; A) = A,
98(false -> _) = false,
99(true -> A) = A,
100\+(false) = true,
101\+(true) = false,
102(X=Y) = true :- X == Y,
103((X=Y) = false :- X \== Y, ground((X,Y))),
104(X==Y) = true :- X == Y,
105((X==Y) = false :- X \== Y, ground((X,Y))),
106nonvar(X) = true :- nonvar(X),
107var(X) = false :- nonvar(X),
108fail = false,
109[]:A = A,
110_:(M:A) = M:A,
111_:E = E :- reduce:prefix_cancellable(E),
112( M:E = ME :- reduce:propagate_prefix(M, E, ME), ((M:E) \== ME)),
113(X = Y :- reduce:slim_goal(X, Y), X\==Y)
114]).
115
119