1:- module(formulae,
2 [ list_to_conj/3,
3 list_to_conj/2,
4 conj_to_list/2,
5 list_to_disj/2,
6 disj_to_list/2,
7 conj_to_llist/2,
8 llist_to_conj/2,
9 disj_to_llist/2,
10 llist_to_disj/2,
11 12 body2list/2,
13 asbody_to_conj/2
14 ]). 15
16list_to_conj([X|More],(X,Next),End):-
17 list_to_conj(More,Next,End).
18list_to_conj([],End,End).
19
20list_to_conj([], true) :- !.
21list_to_conj([A|B], (A,Br)) :- B \== [], !,
22 list_to_conj_(B, Br).
23list_to_conj([A], A) :- !.
24list_to_conj(A, _) :-
25 throw(error(domain_error(list, A), list_to_conj/2)).
26
27list_to_conj_(B, Br) :- var(B), var(Br), !,
28 [Br] = B.
29list_to_conj_(B, Br) :-
30 list_to_conj(B, Br).
31
32conj_to_list(A, B) :- list_to_conj(B, A). 33
34list_to_disj([], false) :- !.
35list_to_disj([A|B], (A;Br)) :- B \== [], !,
36 list_to_disj_(B, Br).
37list_to_disj([A], A) :- !.
38list_to_disj(A, _) :-
39 throw(error(domain_error(list, A), list_to_disj/2)).
40
41list_to_disj_(B, Br) :- var(B), var(Br), !,
42 [Br] = B.
43list_to_disj_(B, Br) :-
44 list_to_disj(B, Br).
45
46list_to_disj2([],false):- !.
47list_to_disj2([X],X):- !.
48list_to_disj2([X|Xs],(X;Ys)):-
49 list_to_disj2(Xs,Ys).
50
51disj_to_list(D, L) :-
52 list_to_disj(L, D). 53
54conj_to_llist(D,L):-
55 conj_to_llist_diff(D,L,[]).
56
57conj_to_llist_diff((A,B),LL,LT):- !,
58 conj_to_llist_diff(A,LL,LA),
59 conj_to_llist_diff(B,LA,LT).
60conj_to_llist_diff((A;B),[LL|LT],LT):- !,
61 disj_to_llist_diff(A,LL,LA),
62 disj_to_llist_diff(B,LA,[]).
63conj_to_llist_diff(A,[A|LT],LT).
64
65llist_to_conj([LL],C):- !,
66 llist_to_disj(LL,C).
67llist_to_conj([LL|LLs],(C,Cs)):- !,
68 llist_to_disj(LL,C),
69 llist_to_conj(LLs,Cs).
70llist_to_conj(C,C).
71
72disj_to_llist(D,L):-
73 disj_to_llist_diff(D,L,[]).
74
75disj_to_llist_diff((A;B),LL,LT):- !,
76 disj_to_llist_diff(A,LL,LA),
77 disj_to_llist_diff(B,LA,LT).
78disj_to_llist_diff((A,B),[LL|LT],LT):- !,
79 conj_to_llist_diff(A,LL,LA),
80 conj_to_llist_diff(B,LA,[]).
81disj_to_llist_diff(A,[A|LT],LT).
82
83llist_to_disj([LL],D):- !,
84 llist_to_conj(LL,D).
85llist_to_disj([LL|LLs],(D;Ds)):- !,
86 llist_to_conj(LL,D),
87 llist_to_disj(LLs,Ds).
88llist_to_disj(D,D).
89
90asbody_to_conj(A, B) :- var(A), !,
91 ( var(B) ->
92 A = B
93 ; conj_to_list_of_list(B, A, [])
94 ).
95asbody_to_conj(A, B) :-
96 list_of_list_to_conj(A, B).
97
98list_of_list_to_conj([(A;B)|C], Out) :- !,
99 list_to_conj(A, AC),
100 list_of_list_to_conj([B], BC),
101 list_of_list_to_conj(C, CC),
102 ( CC == true ->
103 Out = (AC;BC)
104 ; Out = ((AC;BC),CC)
105 ).
106list_of_list_to_conj([A|B], (AC,BC)) :- B \== [], !,
107 list_of_list_to_conj(A, AC),
108 list_of_list_to_conj(B, BC).
109list_of_list_to_conj([AL], A) :-
110 list_of_list_to_conj(AL, A),
111 !.
112list_of_list_to_conj(AL, A) :-
113 is_list(AL), 114 !,
115 list_to_conj(AL, A).
116list_of_list_to_conj(A, A).
117
118conj_to_list_of_list((A,B), Ac, TAc) :- !,
119 conj_to_list_of_list(A, Ac, T),
120 conj_to_list_of_list(B, T, TAc).
121conj_to_list_of_list((A;B), [(AC;BC)|T], T) :- !,
122 conj_to_list__(A, AC),
123 conj_to_list__(B, BC).
124conj_to_list_of_list(true, T, T) :- !.
125conj_to_list_of_list(A, [A|T], T).
126
127conj_to_list__((A,B), [A|Bs]) :- !,
128 conj_to_list(B, Bs).
129conj_to_list__((A;B), (As;Bs)) :- !,
130 conj_to_list(A, As),
131 conj_to_list__(B, Bs).
132conj_to_list__(A, [A]).
133
134body2list((First,Rest), [NewFirst|More]) :- !,
135 p_exp2list(First, NewFirst),
136 body2list(Rest, More).
137body2list(Last, [NewLast]) :-
138 p_exp2list(Last, NewLast).
139
140p_exp2list('&'(G,Goals), [G|More]) :- !,
141 p_exp2list__(Goals, More).
142p_exp2list(Goal, Goal).
143
144p_exp2list__('&'(G,Goals), [G|More]) :-
145 p_exp2list__(Goals, More).
146p_exp2list__(Goal, [Goal])