| /* CHANGELOG by M.Banbara |
| - name/2 --> atom_codes/2 or number_codes/2 |
| - comment out write/1 |
| */ |
| |
| % preprocessing phase to eliminate disjunctions from the code |
| |
| % takes a list of clauses of the form source(Name,Clause) |
| % returns these clauses with disjunctions replaced by dummy calls |
| % and a list of NewClauses corresponding to those dummy calls |
| % Link is the uninstantiated last cdr of this list |
| |
| main :- |
| eliminate_disjunctions([(a(A,B,C):-(b(A);c(C)))],X,Y,[]), |
| inst_vars((X,Y)). |
| %write((X,Y)), nl, |
| % (X,Y) == ([(a:-'_dummy_0')],[('_dummy_0':-b),('_dummy_0':-c)]), |
| %write(ok), nl. |
| main. |
| %main :- write(wrong), nl. |
| |
| eliminate_disjunctions(OneProc,NewProc,NewClauses,Link) :- |
| gather_disj(OneProc,NewProc,Disj,[]), |
| treat_disj(Disj,NewClauses,Link). |
| |
| gather_disj([],[],Link,Link). |
| gather_disj([C|Cs],NewProc,Disj,Link) :- |
| extract_disj(C, NewC, Disj, Rest), |
| NewProc = [NewC|NewCs], |
| gather_disj(Cs,NewCs,Rest,Link). |
| |
| % given a clause, find in Disj the list of disj((A;B),N,X,C) |
| % where N is a unique ID, X is a var that takes the place of |
| % (A;B) in the code, NewC is the clause modified in such a way that |
| % the disjunctions are replaced by the corresponding vars |
| % Link is the last (uninstantiated) cdr of the list Disj. |
| % do the work of pretrans for nots, -> etc... |
| % put all those guys inside disjunctions |
| extract_disj(C, (Head:-NewBody), Disj, Link) :- |
| C = (Head:-Body), !, |
| CtrIn = 0, |
| extract_disj(Body, NewBody, Disj, Link, C, CtrIn, CtrOut). |
| extract_disj(Head, Head, Link, Link). |
| |
| extract_disj((C1,C2), (NewC1,NewC2), Disj, Link, C, CtrIn, CtrOut) :- |
| extract_disj(C1, NewC1, Disj, Link1, C, CtrIn, Ctr), |
| extract_disj(C2, NewC2, Link1, Link, C, Ctr, CtrOut). |
| |
| extract_disj(Goal, X, Disj, Link, C, CtrIn, CtrOut) :- |
| is_disj(Goal,NewGoal), !, |
| Disj = [disj(NewGoal,CtrIn,X,C)|Link], |
| CtrOut is CtrIn + 1. |
| extract_disj(Goal, Goal, Link, Link, _, CtrIn, CtrIn). |
| |
| is_disj(((C1 -> C2); C3),((C1, !, C2); C3)) :- !. |
| is_disj((C1;C2),(C1;C2)). |
| is_disj(not(C),((C,!,fail);true)). |
| is_disj(\+(C),((C,!,fail);true)). |
| is_disj('\='(C1,C2),((C1 = C2,!,fail);true)). |
| |
| % given a list of disj((A;B),N,X,C), for each, do the following: |
| % 1) find vars in (A;B) |
| % 2) find the vars in C |
| % 3) intersect the two sets of vars into one list |
| % 4) make a predicate name using N as a part of it ('dummy_disjN') |
| % 5) put a structure with that name and those vars as args |
| % 6) binds X to this call |
| % 7) add new clauses [(dummy:-A)),(dummy:-B))] |
| treat_disj([], Link, Link). |
| treat_disj([disj((A;B),N,X,C)|Disjs], DummyClauses, Link) :- |
| find_vars((A;B),Vars), |
| find_vars(C,CVars), |
| intersect_vars(Vars,CVars,Args), |
| make_dummy_name(N,Name), |
| X =.. [Name|Args], |
| make_dummy_clauses((A;B),X,DummyClauses,Rest), |
| treat_disj(Disjs, Rest, Link). |
| |
| make_dummy_clauses((A;B),X,[NewC|Cs],Link) :- |
| !, |
| copy((X:-A), NewC), |
| make_dummy_clauses(B,X,Cs,Link). |
| make_dummy_clauses(A,X,[NewC|Link],Link) :- copy((X:-A),NewC). |
| |
| find_vars(X,Y) :- find_vars(X,Y,Link), Link = []. |
| |
| find_vars(Var,[Var|Link],Link) :- var(Var), !. |
| find_vars(Cst,Link,Link) :- atomic(Cst), !. |
| find_vars([T|Ts],Vars,NewLink) :- !, |
| find_vars(T,Vars,Link), |
| find_vars(Ts,Link,NewLink). |
| find_vars(Term,Vars,Link) :- |
| Term =.. [_|Args], |
| find_vars(Args,Vars,Link). |
| |
| intersect_vars(V1,V2,Out) :- |
| sort_vars(V1,Sorted1), |
| sort_vars(V2,Sorted2), |
| intersect_sorted_vars(Sorted1,Sorted2,Out). |
| |
| sort_vars(V,Out) :- sort_vars(V,Out,[]). |
| sort_vars([],Link,Link). |
| sort_vars([V|Vs],Result,Link) :- |
| split_vars(Vs,V,Smaller,Bigger), |
| sort_vars(Smaller,Result,[V|SLink]), |
| sort_vars(Bigger,SLink,Link). |
| |
| split_vars([],_,[],[]). |
| split_vars([V|Vs],A,[V|Ss],Bs) :- |
| V @< A, !, |
| split_vars(Vs,A,Ss,Bs). |
| split_vars([V|Vs],A,Ss,Bs) :- |
| V == A, !, |
| split_vars(Vs,A,Ss,Bs). |
| split_vars([V|Vs],A,Ss,[V|Bs]) :- |
| V @> A, !, |
| split_vars(Vs,A,Ss,Bs). |
| |
| intersect_sorted_vars([],_,[]) :- !. |
| intersect_sorted_vars(_,[],[]). |
| intersect_sorted_vars([X|Xs],[Y|Ys],[X|Rs]) :- |
| X == Y, !, |
| intersect_sorted_vars(Xs,Ys,Rs). |
| intersect_sorted_vars([X|Xs],[Y|Ys],Rs) :- |
| X @< Y, !, |
| intersect_sorted_vars(Xs,[Y|Ys],Rs). |
| intersect_sorted_vars([X|Xs],[Y|Ys],Rs) :- |
| X @> Y, !, |
| intersect_sorted_vars([X|Xs],Ys,Rs). |
| |
| make_dummy_name(N,Name) :- |
| %name('_dummy_',L1), |
| atom_codes('_dummy_',L1), |
| %name(N,L2), |
| number_codes(N,L2), |
| append(L1,L2,L), |
| %name(Name,L). |
| atom_codes(Name,L). |
| |
| append([], L, L). |
| append([H|L1], L2, [H|Res]) :- append(L1, L2, Res). |
| |
| % copy_term using a symbol table. |
| copy(Term1, Term2) :- |
| varset(Term1, Set), make_sym(Set, Sym), |
| copy2(Term1, Term2, Sym), !. |
| |
| copy2(V1, V2, Sym) :- var(V1), !, retrieve_sym(V1, Sym, V2). |
| copy2(X1, X2, Sym) :- nonvar(X1), !, |
| functor(X1,Name,Arity), |
| functor(X2,Name,Arity), |
| copy2(X1, X2, Sym, 1, Arity). |
| |
| copy2(_X1,_X2,_Sym, N, Arity) :- N>Arity, !. |
| copy2(X1, X2, Sym, N, Arity) :- N=<Arity, !, |
| arg(N, X1, Arg1), |
| arg(N, X2, Arg2), |
| copy2(Arg1, Arg2, Sym), |
| N1 is N+1, |
| copy2(X1, X2, Sym, N1, Arity). |
| |
| retrieve_sym(V, [p(W,X)|_Sym], X) :- V==W, !. |
| retrieve_sym(V, [_|Sym], X) :- retrieve_sym(V, Sym, X). |
| |
| make_sym([], []). |
| make_sym([V|L], [p(V,_)|S]) :- make_sym(L, S). |
| |
| % *** Gather all variables used in a term: (in a set or a bag) |
| varset(Term, VarSet) :- varbag(Term, VB), sort(VB, VarSet). |
| varbag(Term, VarBag) :- varbag(Term, VarBag, []). |
| |
| varbag(Var) --> {var(Var)}, !, [Var]. |
| varbag(Str) --> {nonvar(Str), !, functor(Str,_,Arity)}, varbag(Str, 1, Arity). |
| |
| varbag(_Str, N, Arity) --> {N>Arity}, !. |
| varbag(Str, N, Arity) --> {N=<Arity}, !, |
| {arg(N, Str, Arg)}, varbag(Arg), |
| {N1 is N+1}, |
| varbag(Str, N1, Arity). |
| |
| inst_vars(Term) :- |
| varset(Term, Vars), |
| A is "A", |
| inst_vars_list(Vars, A). |
| |
| inst_vars_list([], _). |
| inst_vars_list([T|L], N) :- |
| %name(T, [N]), |
| atom_codes(T, [N]), |
| N1 is N+1, |
| inst_vars_list(L, N1). |