%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% The {log} interpreter
%%
%% by Agostino Dovier Eugenio Omodeo
%% Enrico Pontelli Gianfranco Rossi
%%
%% VERSION 2.2.4 (for SICStus Prolog)
%%
%% (revised October 97 by Gianfranco Rossi)
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%% Syntactic conventions %%%%%%%%%%%
%% 1. Extensional set terms:
%% - {a,b,c} is a set containing three elements, a, b, c
%% (equivalent to '{}' with c with b with a)
%% - {a,b / R} is the set {a,b} U R
%% (equivalent to R with b with a)
%% - '{}' is the empty set
%% 2. Predefined set predicates (set constraints):
%% - t in s (membership)
%% - t nin s (non-membership)
%% - t = s (equality)
%% - t neq s (non-equality)
%% 3. RUQs:
%% - forall(X in t, G), X variable and G any {log} goal containing X
%% 4. Intensional set terms:
%% - {X : G}, X variable and G any {log} goal containing X
%% 5. Syntactic differences w.r.t. std Prolog:
%% - '&' is used in place of ',' in clause bodies
%% - 'or' is used in place of ';' to represent goal disjunction.
%%%%%%%%%%%%%%%% New operators %%%%%%%%%%%%%%%
:-op(1100,fx,(<-)).
:-op(1000,xfx,/).
:-op(980,xfx,:).
:-op(970,xfy,or).
:-op(950,xfy,&).
:-op(900,fy,non).
:-op(700,xfx,in).
:-op(700,xfx,neq).
:-op(700,xfx,nin).
:-op(650,yfx,with).
%:- dynamic(iclause). %MacPROLOG only
%:- dynamic(newpred_counter). %MacPROLOG only
:- dynamic iclause/1. %SICStus Prolog only
:- dynamic newpred_counter/1. %SICStus Prolog only
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Top-level meta-interpreter %%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%init_env :- %% {log} user interface - MacPROLOG only
% whide('{log}.impl'), init_env_cont.
%init_env_cont :- %% MacPROLOG only
% wsize('� Output Window',225,27,154,452),
% kill_menu('Fonts'),
% install_menu('{log}',['Query...','Help','Consult...','Listing','Halt','Abolish','Add...']),
% mdialog(120,110, 80, 280,
% [button( 50, 95, 20, 90, 'Let''s go...'),
% text( 10, 10, 40, 260, 'Welcome to {log}')], _),
% message('Prefix goals at the top level by <-').
%'{log}'('Help'):- %% {log} menu items - MacPROLOG only
% sys_special(help).
%'{log}'('Halt'):-
% sys_special(halt).
%'{log}'('Consult...'):-
% sys_special(consult), nl, write('yes'),nl.
%'{log}'('Abolish'):-
% sys_special(abolish), nl, write('yes'),nl.
%'{log}'('Listing'):-
% nl, sys_special(listing).
%'{log}'('Query...'):-
% 'Eval'('Query...').
%'{log}'('Add...'):-
% sys_special(assert), nl, write('yes'),nl.
setlog :- top_level.
top_level :- %% {log} top-level (for SICStus Prolog only)
nl, write('{log}=> '),
read_term(Goal,[variable_names(VarNames)]),
solve(Goal,Constr),
nl, write_subs_pp(VarNames),
write_constr(Constr),nl,
(VarNames=[],!,write(yes),nl
;
nl, write('Another solution? (y/n)'),
get(C), skip(10),
(C \== 121,! ; fail)),
top_level.
top_level :-
nl,write(no),nl,
top_level.
:- nl, write('loading {log}...please wait (10%)'), nl.
write_subs_pp(VarSubs) :- %% SICStus Prolog only
postproc(VarSubs,VarSubsExt),
write_subs_vv(VarSubsExt,VarSubsMin),
write_subs(VarSubsMin).
write_subs_vv([],[]). %% SICStus Prolog only
write_subs_vv([N1=V1|R],RR) :-
var(V1),!,V1 = N1,
write_subs_vv(R,RR).
write_subs_vv([N1=V1|R],[N1=V1|RR]) :-
write_subs_vv(R,RR).
write_subs([]). %% SICStus Prolog only
write_subs([N1=V1|R]) :-
write(N1), write(' = '), write(V1),
(R = [],!,true ; write(', ') ),
write_subs(R).
write_constr([]) :- !. %% SICStus Prolog only
write_constr(Constr) :-
nl, write('Constraint:'),
postproc(Constr,Constr_ext),
write(Constr_ext).
%<-Goal :- %% {log} top-level (for MacPROLOG only)
% chvar([],L1,Goal,[],L1_new,Goal_new),
% solve(Goal_new,Constr),
% make_res(L1,L1_new),
% write('Constraint:'),
% postproc(Constr,Constr_ext),
% write(Constr_ext),nl.
%
%make_res([],[]). %% MacPROLOG only
%make_res([A|R],[B|S]) :-
% postproc(B,Bset),
% A = Bset,
% make_res(R,S).
solve(Goal_int_ruq,Constr):- % {log} interpreter main predicate
sf_in_goal(Goal_int_ruq,Goal_ruq),
preproc(Goal_ruq,Goal),!,
ruq_in_goal(Goal,B),
constrlist(B,Clist,Alist),
solve_goal(Clist,Alist,Constr).
%%%%%%%%%% Extended SLD-Resolution algorithm %%%%%%%%%%
solve_goal(Clist,[],CListCan):-
can(Clist,CListCan),!.
solve_goal(Clist,[A|B],CListNew):-
ssolve(A,C,D),
append(Clist,C,C1),
can(C1,C2),
append(D,B,B1),
solve_goal(C2,B1,CListNew).
ssolve(true,[],[]):- !. %% unit goal
ssolve(non A,[],[]):- %% negation
selectvars(A,B),
constrlist(A,Clist,Alist),
solve_goal(Clist,Alist,Clist1),
( alldist(B), Clist == Clist1, !, fail
;
message('WARNING: unsafe use of negation'), fail).
ssolve(non _A,[],[]):-!.
ssolve( (G1 or G2),[],ClistNew):- %% goal disjunction
!,( constrlist(G1,G1Clist,G1Alist),
solve_goal(G1Clist,G1Alist,ClistNew)
;
constrlist(G2,G2Clist,G2Alist),
solve_goal(G2Clist,G2Alist,ClistNew) ).
ssolve(A,[],[]):- %% Prolog built-in predicates
nonvar(A),functor(A,F,_),
sys(F),!,A.
ssolve(A,[],[]):- %% {log} built-in predicates
sys_special(A),!.
ssolve(A = B,[],[]):- %% equality
!, sunify(A,B).
ssolve(A in B,[],[]):- %% membership
!,set_term(B),
set_member(A,B).
ssolve(setlog_RUQ(S,InName,VarList),Cout,[]) :- %% RUQs
!, solve_RUQ(S,InName,VarList,[],Cout).
solve_RUQ('{}',_,_,C,C).
solve_RUQ(S,InName,VarList,Cin,Cout) :-
nonvar(S),
sunify(S,R with X),
is_min(X,R),
InPred =.. [InName,X|VarList],
solve_goal([X nin R|Cin],[InPred],C2),
solve_RUQ(R,InName,VarList,C2,Cout).
solve_RUQ(S,InName,VarList,Cin,Cout) :-
var(S),
S = R with X,
InPred =.. [InName,X|VarList],
solve_goal([X nin R|Cin],[InPred],C2),
solve_RUQ(R,InName,VarList,C2,Cout),
set_ordered(S).
ssolve(A,C,D):- %% program defined goals
our_clause(A,B),
constrlist(B,C,D).
our_clause(A,B):-
functor(A,Pname,N),
functor(P,Pname,N),
iclause((P :- B)),
sunify(P,A).
%% Auxiliar predicates for Extended SLD-Resolution
constrlist(A & B,[A|B1],B2):-
constraint(A),!,
constrlist(B,B1,B2).
constrlist(A & B,B1,[A|B2]):-
!,constrlist(B,B1,B2).
constrlist(A,[A],[]):-
constraint(A),!.
constrlist(A,[],[A]).
set_term(X):- var(X),!.
set_term('{}').
set_term(Y with _):- set_term(Y).
set_member(A,B):-
var(B),!,
B = _N with A. %%N.B. no occur-check for 't[X] in X'
%use 'sunify(B,N with A)' instead of 'B = N with A' to enforce it
set_member(A,_ with X):-
sunify(A,X).
set_member(A,Y with _):-
set_member(A,Y).
set_ordered(S) :- var(S),!.
set_ordered('{}') :- !.
set_ordered(R with A) :-
in_order(A,R), set_ordered(R).
in_order(_A,S) :- var(S),!.
in_order(_A,'{}') :- !.
in_order(A,_R with _B) :- var(A), !.
in_order(A,R with B) :- var(B), in_order(A,R),!.
in_order(A,_R with B) :- A @=< B.
is_min(X,_) :- var(X), !.
is_min(_X,'{}') :- !.
is_min(_X,S) :- var(S),!.
is_min(_X,_R with Y) :- var(Y), !.
is_min(X,R with Y) :- X @=< Y,is_min(X,R).
%%%%%%%%%%%%%%% "built in" predicates %%%%%%%%%%%%%
sys(is).
sys(<).
sys(>).
sys(=:=).
sys(nl).
%sys(append). %% MacPROLOG only
%%********* list to be completed!!*********
sys_special(write(T)) :-
!,postproc(T,NewT),
write(NewT).
sys_special(read(T)) :-
!,read(Tout),
preproc(Tout,T).
sys_special(assert):-
!, read(Clause),
setassert(Clause).
%sys_special(consult):- %% MacPROLOG only
% !, old('TEXT',File,Volume),
% open(File,Volume),
% readall(File,1).
sys_special(consult):- %% SICSstus Prolog only
!, write('give file name: '), nl,
read(File),
open(File,read,FileStream),
readall(FileStream,1),
close(FileStream).
sys_special(listing):-
iclause((H :- B)), H \== true,
postproc(H,Hnew), write(Hnew), write((':-')), nl,
write(' '), postproc(B,Bnew), write(Bnew), write('.'), nl,nl,
fail.
sys_special(listing) :- !,write('no more clauses'),nl.
sys_special(abolish):- %% SICSstus Prolog only
!, abolish(iclause,1),
assert( iclause((true :- true)) ).
sys_special(help):- !, setlog_help.
sys_special(halt):- confirm, !, abort.
sys_special(halt).
confirm :-
nl, write('Are you sure you want to leave {log}? (y/n)'),
get(C), skip(10),
C == 121,
nl, write('Bye, bye. See you later').
:- write('loading {log}...please wait (30%)'), nl.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%% Unification Algorithm %%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sunify(X,Y) :- var(X),var(Y),!,X=Y. % 1
sunify(X,Y) :- nonvar(X),var(Y),!,sunify(Y,X). % 2
sunify(X,Y) :- % 5
var(X),tail(Y,T,_),var(T),
samevar(X,T),!,replace_tail(Y,_N,NewY),
sunify(X,NewY).
sunify(X,Y) :- % 6
var(X),!,
% occur_check(X,Y), % occur-check supressed for efficiency reasons
X=Y. % (drop % to reactivate it)
sunify(X,Y) :- % 8
X=..[F|Ax],Y=..[F|Ay],F \== with,
sunifylist(Ax,Ay).
%% 9(b) - same tail vars.
sunify(R with X,S with Y):-
tail(R with X, TS1, _),
tail(S with Y, TS2, _),
samevar(TS1,TS2),!,
sunify_samevar(R with X,S with Y,TS1).
sunify_samevar(A, V, _TS):-
var(A),!, sunify(A,V).
sunify_samevar(A, V, _TS):-
var(V),!, sunify(V,A).
sunify_samevar(R with X, S with Y, TS):-
select(Z, S with Y, Rest),
sunify(X,Z),
(sunify_samevar(R, Rest, TS); % 9(b).1
sunify_samevar(R with X, Rest, TS); % 9(b).2
sunify_samevar(R, S with Y, TS)). % 9(b).3
sunify_samevar(A,B,TS):- % 9(b).4
nonvar(A),nonvar(B),
A = R with X, B = S with Y,
replace_tail(R,N,T1),
replace_tail(S with Y,N, T2),
sunify(TS, N with X),
sunify_samevar(T1,T2,N).
sunify_samevar('{}','{}','{}').
%% distinct tail vars.
sunify(R with X,S with Y) :- % 9(a).1
sunify(R,S),
sunify(X,Y).
sunify(R with X,S with Y) :- % 9(a).2
sunify(R,S with Y),
sunify(X,Y).
sunify(R with X,S with Y) :- % 9(a).3
sunify(R with X,S),
sunify(X,Y).
sunify(R with X,S with Y) :- % 9(a).4
sunify(R, N with Y),sunify(S, N with X).
%% Auxiliar predicates for unification
select(_,S,_):-
var(S), !, fail.
select(Z, R with Z, R).
select(Z, R with Y, A with Y):-
select(Z, R, A).
sunifylist([],[]).
sunifylist([X|AX],[Y|AY]):-
sunify(X,Y),sunifylist(AX,AY).
samevar(X,Y) :- var(X), var(Y), X == Y.
tail(R,R,0) :- var(R),!.
tail('{}','{}',0) :- !.
tail(R with _,T,N) :-
tail(R,T,M), N is M + 1.
replace_tail(R,N,N) :- var(R),!.
replace_tail('{}',N,N) :- !.
replace_tail(R1 with X,N,R2 with X) :-
replace_tail(R1,N,R2).
occur_check(X,Y):-
var(Y),!,X \== Y.
occur_check(X,Y):-
Y =.. [_|R],
occur_check_list(X,R).
occur_check_list(_X,[]):-!.
occur_check_list(X,[A|R]):-
occur_check(X,A),
occur_check_list(X,R).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%% Set constraints %%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%constraint(_ in _). %% dealt with directly by the 'solve' predicate
%% for efficiency reasons
constraint(_ nin _).
constraint(_ neq _).
%%%%%%%%% Set constraint canonization algorithm %%%%%%%%%
can(X,Y):-
can_step(X,W,Z),
( Z == stop, norep_in_list(W,Y),!;
can(W,Y) ).
%% base
can_step([],[],stop).
%% non-membership
can_step([T1 nin Set|R1],[T1 neq T2,T1 nin S|R2],continue):- % 1
nonvar(Set),Set = S with T2,!,
can_step(R1,R2,_).
can_step([T1 nin V|R1], R2,continue):-
( var(V), occurs(V,T1); % 3
nonvar(V) ),!, % 2
can_step(R1,R2,_).
%% inequality
can_step([F neq G|R1],R2,continue):- % 4
nonvar(F),nonvar(G),
functor(F,Fname,Far),
functor(G,Gname,Gar),
(Fname \== Gname; Far \== Gar),!,
can_step(R1,R2,_).
can_step([F neq G|R1],[A neq B|R2],continue):- % 5, 6
nonvar(F),nonvar(G),
functor(F,Fname,Far),
functor(G,Gname,Gar),
Fname == Gname, Far == Gar, Fname \== with,
F =.. [_|Flist], G =.. [_|Glist],!,
memberall(A,B,Flist,Glist),
can_step(R1,R2,_).
can_step([T neq X|R1],[X neq T|R2],continue):- % 7
var(X),nonvar(T),! ,
can_step(R1,R2,_).
can_step([X neq Y|_],_,_):- % 6
var(X),var(Y),
samevar(X,Y),!,fail.
can_step([X neq T|R1], R2,continue):- % 8
var(X),nonvar(T),
functor(T,Tname,_),Tname \== with,
occurs(X,T),!,
can_step(R1,R2,_).
can_step([X neq Set|R1],[Ti nin X |R2],continue):- % 9
var(X), nonvar(Set), Set = _S with _T,
tail(Set, TS,_),
samevar(X,TS),!,
split(Set, _, L),
member(Ti,L) ,
can_step(R1,R2,_).
can_step([X neq Set|R1], R2,continue):- % 8
var(X), nonvar(Set), Set = _S with _T,
occurs(X,Set),!,
can_step(R1,R2,_).
can_step([T1 neq T2|R1],[Z in T1, Z nin T2 | R2],continue):- % 10
nonvar(T1),nonvar(T2), T1 = _A with _S, T2 = _B with _T,
can_step(R1,R2,_).
can_step([T1 neq T2|R1],[Z in T2, Z nin T1 | R2],continue):- % 10
nonvar(T1),nonvar(T2), T1 = _A with _S, T2 = _B with _T,
can_step(R1,R2,_),!.
%% membership
can_step([Z in Set|R1],[Z in S| R2],continue):- % 13.a
nonvar(Set), Set = S with _A,
can_step(R1,R2,_).
can_step([Z in Set |R1],R2,continue):- % 13.b
nonvar(Set), Set = _S with A,
sunify(A,Z),!,
can_step(R1,R2,_).
can_step([Z in X |R1],R2,continue):- %N.B. no occur-check for 't[X] in X'
( var(X), X = _N with Z,!; %use 'sunify(B,N with A)' instead of 'B = N with A' to enforce it
nonvar(X),!,fail ), % 11
can_step(R1,R2,_).
%% else
can_step([X|R1],[X|R2],Stop):-
can_step(R1,R2,Stop).
%%%%%% Auxiliary predicates for set constraint canonization %%%%%%
norep_in_list([],[]):-!.
norep_in_list([A|R],S):-
member_strong(A,R),!,
norep_in_list(R,S).
norep_in_list([A|R],[A|S]):-
norep_in_list(R,S).
member_strong(A,[B|_R]):-
A == B, !.
member_strong(A,[_|R]):-
member_strong(A,R).
memberall(A,B,[A|_R],[B|_S]).
memberall(A,B,[_|R],[_|S]):-
memberall(A,B,R,S).
occurs(X,Y):-
var(Y),samevar(X,Y),!.
occurs(X,Y):-
nonvar(Y),
Y =.. [_|R],
occur_list(X,R).
occur_list(_X,[]):-!,fail.
occur_list(X,[A|_R]):-
occurs(X,A),!.
occur_list(X,[_|R]):-
occur_list(X,R).
split(N,N,[]):-
var(N),!.
split(S with T, N, [T|R]):-
split(S,N,R).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%% Consulting and storing {log} clauses %%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- write('loading {log}...please wait (60%)'), nl.
readall(FileStream,N):-
write('Reading clause '), write(N),
read(FileStream,Clause),!,
( Clause \== end_of_file, write(' : OK'),nl,
setassert(Clause),
N1 is N + 1,
readall(FileStream,N1)
;
write(' = end_of_file'), nl ).
setassert(Clause):-
sf_in_clause(Clause,ExplClause),
preproc(ExplClause,ExtClause),
ruq_in_clause(ExtClause,BaseClause),
assert(iclause(BaseClause)).
iclause((true :- true)).
%%%%%%%% Set preprocessor: from {...} to 'with' notation %%%%%%%%
preproc(X,X):-
var(X),!.
preproc(X,Y1):-
nonvar(X), set(X), !,
set_preproc(X,Y),norep_in_set(Y,Y1).
preproc(X,X):-
atomic(X),!.
preproc((A & B), (A1 & B1)):-
!, preproc(A,A1), preproc(B,B1).
preproc((A ':-' B ), (A1 ':-' B1 )) :-
!, preproc(A,A1), preproc(B,B1).
preproc(X,Z):-
nonvar(X),
functor(X,F,_A), F \== /,
=..(X,[F|ListX]),
preproc_all(ListX,ListZ),
=..(Z,[F|ListZ]).
preproc_all([],[]).
preproc_all([A|L1],[B|L2]):-
preproc(A,B),
preproc_all(L1,L2).
set(X):- nonvar(X),functor(X,'{}',_).
set_preproc(A,A) :- var(A),!.
set_preproc('{}','{}'):- !.
set_preproc('{}'(A),B):-
preproc_list(A,B),!.
set_preproc(_,_):-
message(' wrong set term '),fail.
preproc_list( A, '{}' with A):-
var(A), !.
preproc_list((A1,B1),B2 with A2):- !,
preproc(A1,A2),preproc_list(B1,B2).
preproc_list((A / X),X with B):-
var(X),!, preproc(A,B).
preproc_list((A / X),Y with B):-
(set(X) ; X = _ with _),!, preproc(A,B), preproc(X,Y).
preproc_list(A1,'{}' with A2):-
preproc(A1,A2).
norep_in_set(X,X):- var(X),!.
norep_in_set('{}','{}').
norep_in_set(R with A,S):-
set_member_strong(A,R),!,
norep_in_set(R,S).
norep_in_set(R with A,S with A):-
norep_in_set(R,S).
set_member_strong(A,B):-
nonvar(B),
B = _ with X,
A == X,!.
set_member_strong(A,B):-
nonvar(B),
B = Y with _,
set_member_strong(A,Y).
%%%%%%% Set postprocessor: from 'with' to {...} notation %%%%%%%%%
postproc(X,X):-
var(X),!.
postproc(X,X):-
atomic(X),!.
postproc(X,Y):-
nonvar(X), set_term(X),!,
norep_in_set(X,X1),
with_postproc(X1,Y).
postproc(_ with _,_Y):-!,
message(' wrong set term '),fail.
postproc(X,Z):-
nonvar(X),
=..(X,[F|ListX]),
postproc_all(ListX,ListZ),
=..(Z,[F|ListZ]).
postproc_all([],[]).
postproc_all([A|L1],[B|L2]):-
postproc(A,B),
postproc_all(L1,L2).
with_postproc(A,A) :- var(A),!.
with_postproc('{}','{}'):- !.
with_postproc(A,'{}'(B)):-
postproc_list(A,B).
postproc_list(X with A1,(A2 / X)):-
var(X),!,postproc(A1,A2).
postproc_list( '{}' with A,A ):-
var(A), !.
postproc_list('{}' with A1,A2):- !,
postproc(A1,A2).
postproc_list(B1 with A1,(A2,B2)):-
postproc(A1,A2),postproc_list(B1,B2).
%%%%%%%%%%%% Intensional set preprocessing %%%%%%%%%%%%
sf_in_clause((H :- B),(H1 :- B1)):-
!,sf_in_literals(H,[H1],List1),
sf_in_literals(B,Btemp,List2),
append(List1,Btemp,L),
append(L,List2,List),
list_to_conj(B1,List).
sf_in_clause(A,(H :- B)):-
sf_in_literals(A,[H],List),
list_to_conj(B,List).
sf_in_goal(A,A1):-
sf_in_literals(A,A2,List),
append(List,A2,List1),
list_to_conj(A1,List1).
sf_in_literals(A & B, G2, L2):- % N.B. 'sf_in_literals(A or B, ...)' not supported at present
!, sf_in_literals(A,A1,L1),
sf_in_literals(B,B1,L2),
append(L1,A1,A2),
append(A2,B1,G2).
sf_in_literals(non A, [non A1], List):-
!,sf_in_literals(A,[A1],List).
sf_in_literals(A,[B],List):-
A =.. [Pname|Args],
sf_find(Args,Args1,List),
B =.. [Pname|Args1].
sf_find([],[],[]).
sf_find([Int|R],[Var|S],List):-
nonvar(Int), Int = {SExpr}, nonvar(SExpr), SExpr = (_:G),!,
selectvars(G,Vars),
sf_var(Int,X),
remove_var(X,Vars,Finalvars),
(Vars = Finalvars, message('ERROR - Formula of a set former must contain the set former control variable'), abort ; true),
sf_translate(Int,Var,L1,Finalvars),
sf_find(R,S,L2),
append(L1,L2,List).
sf_find([A|R],[B|S],List):-
nonvar(A),
A =.. [Fname|Rest],
Rest \== [],!,
sf_find(Rest,Newrest,List1),
B =.. [Fname|Newrest],
sf_find(R,S,List2),
append(List1,List2,List).
sf_find([A|R],[A|S],List):-
sf_find(R,S,List).
sf_var({X : _},X) :- var(X),!.
sf_var({X : _},X) :- message('ERROR - Control variable in a set former must be a variable term!'), abort.
sf_translate({X : P1},Y,[Pred],Vars):-
length([_|Vars],N),
newpred(Pred,N),
Pred =.. [_,Y|Vars],
newpred(Aux,N),
Aux =.. [_,Y|Vars],
setassert((Pred :- forall(X in Y,P1) & Y neq '{}' & non Aux)),
setassert((Aux :- X nin Y & P1)).
list_to_conj(A & B,[A|R]):-
!,list_to_conj(B,R).
list_to_conj(A,[A]):- !.
list_to_conj(true,[]).
%%%%%%%%%%%%%% R.U.Q. preprocessing %%%%%%%%%%%%%%%
ruq_in_clause((H :- B),(H :- B1)):-
ruq_in_goal(B,B1),!.
ruq_in_clause(H,H).
ruq_in_goal(forall(X in _S,_Y),_):-
nonvar(X), !,
message('ERROR - Control variable in a R.U.Q. must be a variable term!'), abort.
ruq_in_goal(forall(X in S,Y) & B,NewG):- %N.B. no check for 'forall(X in {...,t[X},...})'
nonvar(S), S = _ with _, !, %add 'occur_check(X,S)' to enforce it
ruq_in_goal(Z = S & forall(X in Z,Y) & B,NewG).
ruq_in_goal(A & B,A1 & B1):-
!, ruq_in_goal(A,A1), ruq_in_goal(B,B1).
ruq_in_goal(RUQ,NewG):-
RUQ = forall(X in S,G),
!, selectvars(G,V),
length(V,N),
newpred(Gpred,N),
remove_var(X,V,Vars),
( V = Vars, message('ERROR - Formula of a R.U.Q. must contain the R.U.Q.control variable'), abort ; true ),
bind(Gpred,[X|Vars]),
setassert( (Gpred :- G) ),
functor(Gpred,F,N),
NewG = setlog_RUQ(S,F,Vars).
ruq_in_goal(A,A).
%%%%%%%%%%%%% New predicate generation %%%%%%%%%%%%%%
newpred_counter(0).
newpred(P,A):-
retract(newpred_counter(Y)), !,
Z is Y + 1,
assert((newpred_counter(Z))),
name(Y,Ylist),
append("setlog_",Ylist,Plist),
name(Pred,Plist),
mklist(L,A),
P =.. [Pred|L].
mklist([],0):- !.
mklist([_|R],N):-
M is N-1,
mklist(R,M).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%% Auxiliary predicates %%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%% Variable extraction and checking %%%%%%%%%%%
selectvars(A,[A]):-
var(A),!.
selectvars(A & B,Vars):-
!, selectvars(A,L1),
selectvars(B,L2),
listunion(L1,L2,Vars).
selectvars(forall(X in Y,B),Vars):-
!, selectvars(Y,L1),
selectvars(B,L2),
listunion(L1,L2,L),
remove_var(X,L,Vars).
selectvars(P,Vars):-
functor(P,_,A),
!, findallvars(P,A,Vars).
findallvars(_P,0,[]):- !.
findallvars(P,A,Vars):-
arg(A,P,Arg),
selectvars(Arg,L1),
B is A-1,
findallvars(P,B,L2),
listunion(L1,L2,Vars).
bind(P,V):-
P =.. [_Pname|Arg],
(Arg = [],! ; Arg = V).
remove_var(_,[],[]).
remove_var(X,[Y|L],S):-
X == Y,!,remove_var(X,L,S).
remove_var(X,[Y|L],[Y|S]):-
remove_var(X,L,S).
alldist([]).
alldist([A|R]):-
var(A), not_in_vars(A,R),
alldist(R).
not_in_vars(_X,[]).
not_in_vars(X,[A|R]):-
X \== A, not_in_vars(X,R).
:- write('loading {log}...please wait (90%)'), nl.
%%%%%%%%%%%% Variable renaming %%%%%%%%%%%%%
chvar(L1,[X|L1],X,L2,[Y|L2],Y):-
var(X), notin(X,L1), !.
chvar(L1,L1,X,L2,L2,Y):-
var(X), find_corr(X,Y,L1,L2),!.
chvar(L1,L1new,(H :- B),L2,L2new,(H1 :- B1)):-
!, chvar(L1,L1a,H,L2,L2a,H1),
chvar(L1a,L1new,B,L2a,L2new,B1).
chvar(L1,L1new,(B1 & B2),L2,L2new,(B1a & B2a)):-
!, chvar(L1,L1a,B1,L2,L2a,B1a),
chvar(L1a,L1new,B2,L2a,L2new,B2a).
chvar(L1,L1,F,L2,L2,F):-
atomic(F),!.
chvar(L1,L1new,F,L2,L2new,F1):-
F =.. [Fname|Args],
chvar_all(L1,L1new,Args,L2,L2new,Brgs),
F1 =.. [Fname|Brgs].
chvar_all(L1,L1,[],L2,L2,[]).
chvar_all(L1,L1b,[A|R],L2,L2b,[B|S]):-
chvar(L1,L1a,A,L2,L2a,B),
chvar_all(L1a,L1b,R,L2a,L2b,S).
find_corr(X,Y,[A|_R],[Y|_S]):-
X == A,!.
find_corr(X,Y,[_|R],[_|S]):-
find_corr(X,Y,R,S).
%%%%%%%%%%%%%% List manipulation pred's %%%%%%%%%%%%%
member(X,[X|_R]).
member(X,[_|R]):-member(X,R).
listunion([],L,L).
listunion([A|R],X,[A|S]):-
notin(A,X),!,
listunion(R,X,S).
listunion([_A|R],X,S):-
listunion(R,X,S).
notin(_,[]).
notin(A,[B|R]):-
A \== B, notin(A,R).
append([],L,L). %% SICStus Prolog only
append([X|L1],L2,[X|L3]):-
append(L1,L2,L3).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%% Help information %%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
setlog_help :-
message('Sorry! No help available at present').
h :- setlog_help.
%welcome_message :- %% MACProlog only
% nl,
% write(' WELCOME TO {log} - version 2.2 '),
% nl,nl,
% write('To run {log}, select Query from the {log} menu. '),
% write('In the Q: field of the Query dialogue box '),
% write('type any {log} goal preceeded by <-. '),
% write('The interpreter will be run when you click on '),
% write('the First button (or hit the Return key). '),
%% nl,nl,
%% write('Give the goal <-help or select Help in the {log} menu '),
%% write('to have more information about the current {log} implementation.'),
% nl,nl.
welcome_message :- %% SICSstus Prolog only
nl, nl,
write(' WELCOME TO {log} - version 2.2 '),nl,
nl,
% nl,
% write('Give the goal <-help or select Help in the {log} menu '),
% write('to have more information about the current {log} implementation.'),nl,
nl.
message(M) :- %% SICStus Prolog only
write(M), nl.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:- welcome_message,init_env. %% MACProlog only
:- welcome_message,top_level. %% SICStus Prolog only