%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% 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