1% preprocessing phase to eliminate disjunctions from the code
2
3% takes a list of clauses of the form source(Name,Clause)
4% returns these clauses with disjunctions replaced by dummy calls
5% and a list of NewClauses corresponding to those dummy calls
6% Link is the uninstantiated last cdr of this list
7
8top:-
9	eliminate_disjunctions([(a(A,B,C):-(b(A);c(C)))],X,Y,[]),
10    inst_vars((X,Y)).
11%	write((X,Y)), nl,
12	% (X,Y) == ([(a:-'_dummy_0')],[('_dummy_0':-b),('_dummy_0':-c)]),
13%	write(ok), nl.
14top :- true.
15%write(wrong), nl.
16
17eliminate_disjunctions(OneProc,NewProc,NewClauses,Link) :-
18	gather_disj(OneProc,NewProc,Disj,[]),
19    treat_disj(Disj,NewClauses,Link).
20
21gather_disj([],[],Link,Link).
22gather_disj([C|Cs],NewProc,Disj,Link) :-
23	extract_disj(C, NewC, Disj, Rest),
24	NewProc = [NewC|NewCs],
25	gather_disj(Cs,NewCs,Rest,Link).
26
27% given a clause, find in Disj the list of disj((A;B),N,X,C)
28% where N is a unique ID, X is a var that takes the place of
29% (A;B) in the code, NewC is the clause modified in such a way that
30% the disjunctions are replaced by the corresponding vars
31% Link is the last (uninstantiated) cdr of the list Disj.
32% do the work of pretrans for nots, -> etc...
33% put all those guys inside disjunctions
34extract_disj(C, (Head:-NewBody), Disj, Link) :-
35	C = (Head:-Body), !,
36	CtrIn = 0,
37	extract_disj(Body, NewBody, Disj, Link, C, CtrIn, CtrOut).
38extract_disj(Head, Head, Link, Link).
39
40extract_disj((C1,C2), (NewC1,NewC2), Disj, Link, C, CtrIn, CtrOut) :-
41	extract_disj(C1, NewC1, Disj, Link1, C, CtrIn, Ctr),
42	extract_disj(C2, NewC2, Link1, Link, C, Ctr, CtrOut).
43
44extract_disj(Goal, X, Disj, Link, C, CtrIn, CtrOut) :-
45	is_disj(Goal,NewGoal), !,
46	Disj = [disj(NewGoal,CtrIn,X,C)|Link],
47	CtrOut is CtrIn + 1.
48extract_disj(Goal, Goal, Link, Link, _, CtrIn, CtrIn).
49
50is_disj(((C1 -> C2); C3),((C1, !, C2); C3)) :- !.
51is_disj((C1;C2),(C1;C2)).
52is_disj(not(C),((C,!,fail);true)).
53is_disj(\+(C),((C,!,fail);true)).
54is_disj(\=(C1,C2),((C1 = C2,!,fail);true)).
55
56% given a list of disj((A;B),N,X,C), for each, do the following:
57% 1) find vars in (A;B)
58% 2) find the vars in C
59% 3) intersect the two sets of vars into one list
60% 4) make a predicate name using N as a part of it ('dummy_disjN')
61% 5) put a structure with that name and those vars as args
62% 6) binds X to this call
63% 7) add new clauses [(dummy:-A)),(dummy:-B))]
64treat_disj([], Link, Link).
65treat_disj([disj((A;B),N,X,C)|Disjs], DummyClauses, Link) :-
66	find_vars((A;B),Vars),
67	find_vars(C,CVars),
68	intersect_vars(Vars,CVars,Args),
69	make_dummy_name(N,Name),
70	X =.. [Name|Args],
71	make_dummy_clauses((A;B),X,DummyClauses,Rest),
72	treat_disj(Disjs, Rest, Link).
73
74make_dummy_clauses((A;B),X,[NewC|Cs],Link) :-
75	!,
76	copy((X:-A), NewC),
77	make_dummy_clauses(B,X,Cs,Link).
78make_dummy_clauses(A,X,[NewC|Link],Link) :- copy((X:-A),NewC).
79
80find_vars(X,Y) :- find_vars(X,Y,Link), Link = [].
81
82find_vars(Var,[Var|Link],Link) :- var(Var), !.
83find_vars(Cst,Link,Link) :- atomic(Cst), !.
84find_vars([T|Ts],Vars,NewLink) :- !,
85	find_vars(T,Vars,Link),
86	find_vars(Ts,Link,NewLink).
87find_vars(Term,Vars,Link) :-
88	Term =.. [_|Args],
89	find_vars(Args,Vars,Link).
90
91intersect_vars(V1,V2,Out) :-
92	sort_vars(V1,Sorted1),
93	sort_vars(V2,Sorted2),
94	intersect_sorted_vars(Sorted1,Sorted2,Out).
95
96make_dummy_name(N,Name) :-
97	name('_dummy_',L1),
98	name(N,L2),
99	my_append(L1,L2,L),
100	name(Name,L).
101
102my_append([], L, L).
103my_append([H|L1], L2, [H|Res]) :- my_append(L1, L2, Res).
104
105% copy_term using a symbol table.
106copy(Term1, Term2) :-
107        varset(Term1, Set), make_sym(Set, Sym),
108        copy2(Term1, Term2, Sym), !.
109
110copy2(V1, V2, Sym) :- var(V1), !, retrieve_sym(V1, Sym, V2).
111copy2(X1, X2, Sym) :- nonvar(X1), !,
112        functor(X1,Name,Arity),
113        functor(X2,Name,Arity),
114        copy2(X1, X2, Sym, 1, Arity).
115
116copy2(_X1,_X2,_Sym, N, Arity) :- N>Arity, !.
117copy2(X1, X2, Sym, N, Arity) :- N=<Arity, !,
118        arg(N, X1, Arg1),
119        arg(N, X2, Arg2),
120        copy2(Arg1, Arg2, Sym),
121        N1 is N+1,
122        copy2(X1, X2, Sym, N1, Arity).
123
124retrieve_sym(V, [p(W,X)|_Sym], X) :- V==W, !.
125retrieve_sym(V, [_|Sym], X) :- retrieve_sym(V, Sym, X).
126
127make_sym([], []).
128make_sym([V|L], [p(V,_)|S]) :- make_sym(L, S).
129
130% *** Gather all variables used in a term: (in a set or a bag)
131varset(Term, VarSet) :- varbag(Term, VB),
132    sort(VB, VarSet).
133varbag(Term, VarBag) :- varbag(Term, VarBag, []).
134
135varbag(Var) --> {var(Var)}, !, [Var].
136varbag(Str) --> {nonvar(Str), !, functor(Str,_,Arity)}, varbag(Str, 1, Arity).
137
138varbag(_Str, N, Arity) --> {N>Arity}, !.
139varbag(Str, N, Arity) --> {N=<Arity}, !,
140        {arg(N, Str, Arg)}, varbag(Arg),
141        {N1 is N+1},
142        varbag(Str, N1, Arity).
143
144inst_vars(Term) :-
145	varset(Term, Vars),
146	inst_vars_list(Vars, 0'A).
147
148inst_vars_list([], _).
149inst_vars_list([T|L], N) :-
150	name(T, [N]),
151	N1 is N+1,
152	inst_vars_list(L, N1).
153
154sort_vars(V,Out) :- sort_vars(V,Out,[]).
155sort_vars([],Link,Link).
156sort_vars([V|Vs],Result,Link) :-
157	split_vars(Vs,V,Smaller,Bigger),
158	sort_vars(Smaller,Result,[V|SLink]),
159	sort_vars(Bigger,SLink,Link).
160
161intersect_sorted_vars([],_,[]) :- !.
162intersect_sorted_vars(_,[],[]).
163intersect_sorted_vars([X|Xs],[Y|Ys],[X|Rs]) :-
164	X == Y, !,
165	intersect_sorted_vars(Xs,Ys,Rs).
166intersect_sorted_vars([X|Xs],[Y|Ys],Rs) :-
167	X @< Y, !,
168	intersect_sorted_vars(Xs,[Y|Ys],Rs).
169intersect_sorted_vars([X|Xs],[Y|Ys],Rs) :-
170	X @> Y, !,
171	intersect_sorted_vars([X|Xs],Ys,Rs).
172
173
174split_vars([],_,[],[]).
175split_vars([V|Vs],A,[V|Ss],Bs) :-
176	V @< A, !,
177	split_vars(Vs,A,Ss,Bs).
178split_vars([V|Vs],A,Ss,Bs) :-
179	V == A, !,
180	split_vars(Vs,A,Ss,Bs).
181split_vars([V|Vs],A,Ss,[V|Bs]) :-
182	V @> A, !,
183	split_vars(Vs,A,Ss,Bs).
184