 -*- Prolog -*-
%
% $Id: prolog_benchmarks,v 1.2 2000/10/29 01:29:11 peteg Exp $

%
%   nreverse
%
%   David H. D. Warren
%
%   "naive"-reverse a list of 30 integers

main :- nreverse([1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30],_).

nreverse([X|L0],L) :- nreverse(L0,L1), concatenate(L1,[X],L).
nreverse([],[]).

concatenate([X|L1],L2,[X|L3]) :- concatenate(L1,L2,L3).
concatenate([],L,L).

%
%   tak
%
%   Evan Tick (from Lisp version by R. P. Gabriel)
%
%   (almost) Takeuchi function (recursive arithmetic)

main :- tak(18,12,6,_).

tak(X,Y,Z,A) :-
	X =< Y,
	Z = A.
tak(X,Y,Z,A) :-
	X > Y,
	X1 is X - 1,
	tak(X1,Y,Z,A1),
	Y1 is Y - 1,
	tak(Y1,Z,X,A2),
	Z1 is Z - 1,
	tak(Z1,X,Y,A3),
	tak(A1,A2,A3,A).

%
%   qsort
%
%   David H. D. Warren
%
%   quicksort a list of 50 integers

main :- qsort([27,74,17,33,94,18,46,83,65, 2,32,53,28,85,99,47,28,82, 6,11,55,29,39,81,90,37,10, 0,66,
			51,7,21,85,27,31,63,75, 4,95,99,11,28,61,74,18,92,40,53,59, 8],_,[]).

qsort([X|L],R,R0) :-
	partition(L,X,L1,L2),
	qsort(L2,R1,R0),
	qsort(L1,R,[X|R1]).
qsort([],R,R).

partition([X|L],Y,[X|L1],L2) :-
	X =< Y, !,
	partition(L,Y,L1,L2).
partition([X|L],Y,L1,[X|L2]) :-
	partition(L,Y,L1,L2).
partition([],_,[],[]).

main :-
	primes(98, X).

primes(Limit, Ps) :-
	integers(2, Limit, Is),
	sift(Is, Ps).

integers(Low, High, [Low | Rest]) :- 
	Low =< High,
	!,
	M is Low+1,
	integers(M, High, Rest).
integers(_,_,[]).

sift([],[]).
sift([I | Is], [I | Ps]) :-
	remove(I,Is,New),
	sift(New, Ps).

remove(P,[],[]).
remove(P,[I | Is], [I | Nis]) :-
	0 =\= I mod P,
	!,
	remove(P,Is,Nis).
remove(P,[I | Is], Nis) :-
	0 =:= I mod P,
	!,
	remove(P,Is,Nis).

%
%   serialise
%
%   David H. D. Warren
%
%   itemize (pick a "serial number" for each 
%   unique integer in) a list of 25 integers

main :- serialise("ABLE WAS I ERE I SAW ELBA",_).

serialise(L,R) :-
	pairlists(L,R,A),
	arrange(A,T),
	numbered(T,1,_).

pairlists([X|L],[Y|R],[pair(X,Y)|A]) :- pairlists(L,R,A).
pairlists([],[],[]).

arrange([X|L],tree(T1,X,T2)) :-
	split(L,X,L1,L2),
	arrange(L1,T1),
	arrange(L2,T2).
arrange([],void).

split([X|L],X,L1,L2) :- !, split(L,X,L1,L2).
split([X|L],Y,[X|L1],L2) :- before(X,Y), !, split(L,Y,L1,L2).
split([X|L],Y,L1,[X|L2]) :- before(Y,X), !, split(L,Y,L1,L2).
split([],_,[],[]).

before(pair(X1,_),pair(X2,_)) :- X1 < X2.

numbered(tree(T1,pair(_,N1),T2),N0,N) :-
	numbered(T1,N0,N1),
	N2 is N1+1,
	numbered(T2,N2,N).
numbered(void,N,N).

% Queens

main :- queens(8,_), !.

queens(N,Qs) :-
	range(1,N,Ns),
	queens(Ns,[],Qs).

queens([],Qs,Qs).
queens(UnplacedQs,SafeQs,Qs) :-
	select(UnplacedQs,UnplacedQs1,Q),
	not_attack(SafeQs,Q),
	queens(UnplacedQs1,[Q|SafeQs],Qs).

not_attack(Xs,X) :-
	not_attack(Xs,X,1).

not_attack([],_,_) :- !.
not_attack([Y|Ys],X,N) :-
	X =\= Y+N, X =\= Y-N,
	N1 is N+1,
	not_attack(Ys,X,N1).

select([X|Xs],Xs,X).
select([Y|Ys],[Y|Zs],X) :- select(Ys,Zs,X).

range(N,N,[N]) :- !.
range(M,N,[M|Ns]) :-
	M < N,
	M1 is M+1,
	range(M1,N,Ns).

%
%   mu
%
%   derived from Douglas R. Hofstadter,
%   "Godel, Escher, Bach," pages 33-35.
%
%   prove "mu-math" theorem muiiu

main :- theorem([m,u,i,i,u], 5, _), !.

theorem([m,i], _, [[a|[m,i]]]).
theorem(R, Depth, [[N|R]|P]) :-
	Depth > 0,
	D is Depth-1,
	theorem(S, D, P),
	rule(N, S, R).

rule(1, S, R) :- rule1(S, R).
rule(2, S, R) :- rule2(S, R).
rule(3, S, R) :- rule3(S, R).
rule(4, S, R) :- rule4(S, R).

rule1([i], [i,u]).
rule1([H|X], [H|Y]) :-
	rule1(X, Y).

rule2([m|X], [m|Y]) :- 
	append(X, X, Y).

rule3([i,i,i|X], [u|X]).
rule3([H|X], [H|Y]) :-
	rule3(X, Y).

rule4([u,u|X], X).
rule4([H|X], [H|Y]) :-
	rule4(X, Y).

append([], X, X).
append([A|B], X, [A|B1]) :-
	append(B, X, B1).

%   deriv
%
%   David H. D. Warren
%

main :- ops8, divide10, log10, times10.

d(U+V,X,DU+DV) :- !, 
	d(U,X,DU),
	d(V,X,DV).
d(U-V,X,DU-DV) :- !,
	d(U,X,DU),
	d(V,X,DV).
d(U*V,X,DU*V+U*DV) :- !,
	d(U,X,DU),
	d(V,X,DV).
d(U/V,X,(DU*V-U*DV)/(^(V,2))) :- !,
	d(U,X,DU),
	d(V,X,DV).
d(^(U,N),X,DU*N*(^(U,N1))) :- !, 
	integer(N),
	N1 is N-1,
	d(U,X,DU).
d(-U,X,-DU) :- !,
	d(U,X,DU).
d(exp(U),X,exp(U)*DU) :- !,
	d(U,X,DU).
d(log(U),X,DU/U) :- !,
	d(U,X,DU).
d(X,X,1) :- !.
d(_,_,0).

ops8 :- d((x+1)*((^(x,2)+2)*(^(x,3)+3)),x,_).
divide10 :- d(((((((((x/x)/x)/x)/x)/x)/x)/x)/x)/x,x,_).
log10 :- d(log(log(log(log(log(log(log(log(log(log(x)))))))))),x,_).
times10 :- d(((((((((x*x)*x)*x)*x)*x)*x)*x)*x)*x,x,_).

%
% zebra
%
% Where does the zebra live?
% Puzzle solution written by Claude Sammut.
main :-
	houses(Houses),
	member(house(red, english, _, _, _), Houses),
	member(house(_, spanish, dog, _, _), Houses),
	member(house(green, _, _, coffee, _), Houses),
	member(house(_, ukrainian, _, tea, _), Houses),
	right_of(house(green,_,_,_,_), house(ivory,_,_,_,_), Houses),
	member(house(_, _, snails, _, winstons), Houses),
	member(house(yellow, _, _, _, kools), Houses),
	Houses = [_, _, house(_, _, _, milk, _), _,_],
	Houses = [house(_, norwegian, _, _, _)|_],
	next_to(house(_,_,_,_,chesterfields), house(_,_,fox,_,_), Houses),
	next_to(house(_,_,_,_,kools), house(_,_,horse,_,_), Houses),
	member(house(_, _, _, orange_juice, lucky_strikes), Houses),
	member(house(_, japanese, _, _, parliaments), Houses),
	next_to(house(_,norwegian,_,_,_), house(blue,_,_,_,_), Houses),
	member(house(_, _, zebra, _, _), Houses),
	member(house(_, _, _, water, _), Houses),
	print_houses(Houses).

houses([
	house(_, _, _, _, _),
	house(_, _, _, _, _),
	house(_, _, _, _, _),
	house(_, _, _, _, _),
	house(_, _, _, _, _)
]).

right_of(A, B, [B, A | _]).
right_of(A, B, [_ | Y]) :- right_of(A, B, Y).

next_to(A, B, [A, B | _]).
next_to(A, B, [B, A | _]).
next_to(A, B, [_ | Y]) :- next_to(A, B, Y).

member(X, [X|_]).
member(X, [_|Y]) :- member(X, Y).

print_houses([A|B]) :- !,
	write(A), nl,
	print_houses(B).
print_houses([]).

%
% crypt
%
% Cryptomultiplication:
% Find the unique answer to:
%	OEE
%	 EE
% 	---
%      EOEE
%      EOE
%      ----
%      OOEE
%
% where E=even, O=odd.
% This program generalizes easily
% to any such problem.
% Written by Peter Van Roy

main :-
	odd(A), even(B), even(C),
	even(E),
	mult([C,B,A], E, [I,H,G,F|X]),
	lefteven(F), odd(G), even(H),
	even(I), zero(X),
	lefteven(D),
	mult([C,B,A], D, [L,K,J|Y]),
	lefteven(J), odd(K), even(L), zero(Y),
	sum([I,H,G,F], [0,L,K,J], [P,O,N,M|Z]),
	odd(M), odd(N), even(O), even(P), zero(Z).
	% write(' '), write(A), write(B), write(C), nl,
	% write('  '), write(D), write(E), nl,
	% write(F), write(G), write(H), write(I), nl,
	% write(J), write(K), write(L), nl,
	% write(M), write(N), write(O), write(P), nl.

% Addition of two numbers
sum(AL, BL, CL) :- sum(AL, BL, 0, CL).

sum([A|AL], [B|BL], Carry, [C|CL]) :- !,
	X is (A+B+Carry),
	C is X mod 10,
	NewCarry is X // 10,
	sum(AL, BL, NewCarry, CL).
sum([], BL, 0, BL) :- !.
sum(AL, [], 0, AL) :- !.
sum([], [B|BL], Carry, [C|CL]) :- !,
	X is B+Carry,
	NewCarry is X // 10,
	C is X mod 10,
	sum([], BL, NewCarry, CL).
sum([A|AL], [], Carry, [C|CL]) :- !,
	X is A+Carry,
	NewCarry is X // 10,
	C is X mod 10,
	sum([], AL, NewCarry, CL).
sum([], [], Carry, [Carry]).

% Multiplication
mult(AL, D, BL) :- mult(AL, D, 0, BL).

mult([A|AL], D, Carry, [B|BL] ) :-
	X is A*D+Carry,
	B is X mod 10,
	NewCarry is X // 10,
	mult(AL, D, NewCarry, BL).
mult([], _, Carry, [C,Cend]) :-
	C is Carry mod 10,
	Cend is Carry // 10.

zero([]).
zero([0|L]) :- zero(L).

odd(1).
odd(3).
odd(5).
odd(7).
odd(9).

even(0).
even(2).
even(4).
even(6).
even(8).

lefteven(2).
lefteven(4).
lefteven(6).
lefteven(8).

%
%   query
%
%   David H. D. Warren
%
%   query population and area database to find coun-
%   tries of approximately equal population density

query :- query(_), fail.
query.

query([C1,D1,C2,D2]) :- 
	density(C1,D1), 
	density(C2,D2),
	D1 > D2,
	T1 is 20*D1,
	T2 is 21*D2,
	T1 < T2.

density(C,D) :- 
	pop(C,P),
	area(C,A),
	D is (P*100)//A.

% populations in 100000's % areas in 1000's of square miles
pop(china,	8250).		area(china,	3380).
pop(india,	5863).		area(india,	1139).
pop(ussr,	2521).		area(ussr,	8708).
pop(usa,	2119).		area(usa,	3609).
pop(indonesia,	1276).		area(indonesia,	  570).
pop(japan,	1097).		area(japan,	  148).
pop(brazil,	1042).		area(brazil,	3288).
pop(bangladesh,	  750).		area(bangladesh,	    55).
pop(pakistan,	  682).		area(pakistan,	  311).
pop(w_germany,	  620).		area(w_germany,   96).
pop(nigeria,	  613).		area(nigeria,	  373).
pop(mexico,	  581).		area(mexico,	  764).
pop(uk,	  559).		area(uk,		    86).
pop(italy,	  554).		area(italy,	  116).
pop(france,	  525).		area(france,	  213).
pop(philippines,	  415).		area(philippines,	    90).
pop(thailand,	  410).		area(thailand,	  200).
pop(turkey,	  383).		area(turkey,	  296).
pop(egypt,	  364).		area(egypt,	  386).
pop(spain,	  352).		area(spain,	  190).
pop(poland,	  337).		area(poland,	  121).
pop(s_korea,	  335).		area(s_korea,	    37).
pop(iran,	  320).		area(iran,	  628).
pop(ethiopia,	  272).		area(ethiopia,	  350).
pop(argentina,	  251).		area(argentina,	1080).

%
%   prover
%
%   Richard A. O'Keefe
%
%   Prolog theorem prover
%
%   from "Prolog Compared with Lisp?,"
%   SIGPLAN Notices, v. 18 #5, May 1983

% op/3 directives

:- op(950, xfy, #).	% disjunction
:- op(850, xfy, &).	% conjunction
:- op(500, fx, +).	% assertion
:- op(500, fx, -).	% denial

prover :- problem(_, P, C),
	  implies(P, C),
	  fail.
prover.

% problem set

problem( 1, -a, +a).

problem( 2, +a, -a & -a).

problem( 3, -a, +to_be # -to_be).

problem( 4, -a & -a, -a).

problem( 5, -a, +b # -a).

problem( 6, -a & -b, -b & -a).

problem( 7, -a, -b # (+b & -a)).

problem( 8, -a # (-b # +c), -b # (-a # +c)).

problem( 9, -a # +b, (+b & -c) # (-a # +c)).

problem( 10, (-a # +c) & (-b # +c), (-a & -b) # +c).

% Prolog theorem prover

implies(Premise, Conclusion) :-
	opposite(Conclusion, Denial),
	add_conjunction(Premise, Denial, fs([],[],[],[])).

opposite(F0 & G0, F1 # G1) :- !,
	opposite(F0, F1),
	opposite(G0, G1).
opposite(F1 # G1, F0 & G0) :- !,
	opposite(F1, F0),
	opposite(G1, G0).
opposite(+Atom, -Atom) :- !.
opposite(-Atom, +Atom).

add_conjunction(F, G, Set) :-
	expand(F, Set, Mid),
	expand(G, Mid, New),
	refute(New).

expand(_, refuted, refuted) :- !.
expand(F & G, fs(D,_,_,_), refuted) :-
	includes(D, F & G), !.
expand(F & G, fs(D,C,P,N), fs(D,C,P,N)) :-
	includes(C, F & G), !.
expand(F & G, fs(D,C,P,N), New) :- !,
	expand(F, fs(D,[F & G|C],P,N), Mid),
	expand(G, Mid, New).
expand(F # G, fs(D,C,P,N), Set) :- !,
	opposite(F # G, Conj),
	extend(Conj, D, C, D1, fs(D1,C,P,N), Set).
expand(+Atom, fs(D,C,P,N), Set) :- !,
	extend(Atom, P, N, P1, fs(D,C,P1,N), Set).
expand(-Atom, fs(D,C,P,N), Set) :-
	extend(Atom, N, P, N1, fs(D,C,P,N1), Set).

includes([Head|_], Head) :- !.
includes([_|Tail], This) :- includes(Tail, This).

extend(Exp, _, Neg, _, _, refuted) :-
	includes(Neg, Exp), !.
extend(Exp, Pos, _, Pos, Set, Set) :-
	includes(Pos, Exp), !.
extend(Exp, Pos, _, [Exp|Pos], Set, Set).

refute(refuted) :- !.
refute(fs([F1 & G1|D], C, P, N)) :-
	opposite(F1, F0),
	opposite(G1, G0),
	Set = fs(D, C, P, N),
	add_conjunction(F0, G1, Set),
	add_conjunction(F0, G0, Set),
	add_conjunction(F1, G0, Set).

%
%   poly_10
%
%   Ralph Haygood (based on Prolog version by Rick McGeer
%                  based on Lisp version by R. P. Gabriel)
%
%   raise a polynomial (1+x+y+z) to the 10th power (symbolically)

:-op(700,xfx,less_than).

poly_10 :- test_poly(P), poly_exp(10, P, _).

% test polynomial definition

test_poly(P) :-
	poly_add(poly(x,[term(0,1),term(1,1)]),poly(y,[term(1,1)]),Q),
	poly_add(poly(z,[term(1,1)]),Q,P).

% 'less_than'/2 for x, y, z

x less_than y.
y less_than z.
x less_than z.

% polynomial addition

poly_add(poly(Var,Terms1), poly(Var,Terms2), poly(Var,Terms)) :- !,
	term_add(Terms1, Terms2, Terms).
poly_add(poly(Var1,Terms1), poly(Var2,Terms2), poly(Var1,Terms)) :-
	Var1 less_than Var2, !,
	add_to_order_zero_term(Terms1, poly(Var2,Terms2), Terms).
poly_add(Poly, poly(Var,Terms2), poly(Var,Terms)) :- !,
	add_to_order_zero_term(Terms2, Poly, Terms).
poly_add(poly(Var,Terms1), C, poly(Var,Terms)) :- !,
	add_to_order_zero_term(Terms1, C, Terms).
poly_add(C1, C2, C) :-
	C is C1+C2.

% term addition

term_add([], X, X) :- !.
term_add(X, [], X) :- !.
term_add([term(E,C1)|Terms1], [term(E,C2)|Terms2], [term(E,C)|Terms]) :- !,
	poly_add(C1, C2, C),
	term_add(Terms1, Terms2, Terms).
term_add([term(E1,C1)|Terms1], [term(E2,C2)|Terms2], [term(E1,C1)|Terms]) :-
	E1 < E2, !,
	term_add(Terms1, [term(E2,C2)|Terms2], Terms).
term_add(Terms1, [term(E2,C2)|Terms2], [term(E2,C2)|Terms]) :-
	term_add(Terms1, Terms2, Terms).

add_to_order_zero_term([term(0,C1)|Terms], C2, [term(0,C)|Terms]) :- !,
	poly_add(C1, C2, C).
add_to_order_zero_term(Terms, C, [term(0,C)|Terms]).

% polynomial exponentiation

poly_exp(0, _, 1) :- !.
poly_exp(N, Poly, Result) :-
	M is N>>1,
	N is M<<1, !,
	poly_exp(M, Poly, Part),
	poly_mul(Part, Part, Result).
poly_exp(N, Poly, Result) :-
	M is N-1,
	poly_exp(M, Poly, Part),
	poly_mul(Poly, Part, Result).

% polynomial multiplication

poly_mul(poly(Var,Terms1), poly(Var,Terms2), poly(Var,Terms)) :- !,
	term_mul(Terms1, Terms2, Terms).
poly_mul(poly(Var1,Terms1), poly(Var2,Terms2), poly(Var1,Terms)) :-
	Var1 less_than Var2, !,
	mul_through(Terms1, poly(Var2,Terms2), Terms).
poly_mul(P, poly(Var,Terms2), poly(Var,Terms)) :- !,
	mul_through(Terms2, P, Terms).
poly_mul(poly(Var,Terms1), C, poly(Var,Terms)) :- !,
	mul_through(Terms1, C, Terms).
poly_mul(C1, C2, C) :-
	C is C1*C2.

term_mul([], _, []) :- !.
term_mul(_, [], []) :- !.
term_mul([Term|Terms1], Terms2, Terms) :-
	single_term_mul(Terms2, Term, PartA),
	term_mul(Terms1, Terms2, PartB),
	term_add(PartA, PartB, Terms).

single_term_mul([], _, []) :- !.
single_term_mul([term(E1,C1)|Terms1], term(E2,C2),
		[term(E,C)|Terms]) :-
	E is E1+E2,
	poly_mul(C1, C2, C),
	single_term_mul(Terms1, term(E2,C2), Terms).

mul_through([], _, []) :- !.
mul_through([term(E,Term)|Terms], Poly,
		[term(E,NewTerm)|NewTerms]) :-
	poly_mul(Term, Poly, NewTerm),
	mul_through(Terms, Poly, NewTerms).
%
%   browse
%
%   Tep Dobry
%   (from Lisp version by R. P. Gabriel)
%
%   (modified January 1987 by Herve' Touati)

main :- 
	init(100,10,4,
	 [[a,a,a,b,b,b,b,a,a,a,a,a,b,b,a,a,a],
	  [a,a,b,b,b,b,a,a,[a,a],[b,b]],
	  [a,a,a,b,[b,a],b,a,b,a]
	 ],
	 Symbols),
	randomize(Symbols,RSymbols,21),!,
	investigate(RSymbols,
		[[star(SA),B,star(SB),B,a,star(SA),
			a,star(SB),star(SA)],
		 [star(SA),star(SB),star(SB),star(SA),
			[star(SA)],[star(SB)]],
		 [_,_,star(_),[b,a],star(_),_,_]
		]).


init(N,M,Npats,Ipats,Result) :-
	init(N,M,M,Npats,Ipats,Result).

init(0,_,_,_,_,_) :- !.
init(N,I,M,Npats,Ipats,[Symb|Rest]) :- 
	fill(I,[],L),
	get_pats(Npats,Ipats,Ppats),
	J is M - I,
	fill(J,[pattern(Ppats)|L],Symb),
	N1 is N - 1,
	(I =:= 0 -> I1 is M; I1 is I - 1),
	init(N1,I1,M,Npats,Ipats,Rest).

fill(0,L,L) :- !.
fill(N,L,[dummy([])|Rest]) :- 
	N1 is N - 1,
	fill(N1,L,Rest).

randomize([],[],_) :- !.
randomize(In,[X|Out],Rand) :-
	length(In,Lin),
	Rand1 is (Rand * 17) mod 251,
	N is Rand1 mod Lin,
	split(N,In,X,In1),
	randomize(In1,Out,Rand1).

split(0,[X|Xs],X,Xs) :- !.
split(N,[X|Xs],RemovedElt,[X|Ys]) :-
	N1 is N - 1,
	split(N1,Xs,RemovedElt,Ys).

investigate([],_) :- !.
investigate([U|Units],Patterns) :-
	property(U,pattern,Data),
	p_investigate(Data,Patterns),
	investigate(Units,Patterns).

get_pats(Npats,Ipats,Result) :-
	get_pats(Npats,Ipats,Result,Ipats).

get_pats(0,_,[],_) :- !.
get_pats(N,[X|Xs],[X|Ys],Ipats) :-
	N1 is N - 1,
	get_pats(N1,Xs,Ys,Ipats).
get_pats(N,[],Ys,Ipats) :-
	get_pats(N,Ipats,Ys,Ipats).

property([],_,_) :- fail.	/* don't really need this */
property([Prop|_],P,Val) :-
	functor(Prop,P,_),!,
	arg(1,Prop,Val).
property([_|RProps],P,Val) :-
	property(RProps,P,Val).

p_investigate([],_).
p_investigate([D|Data],Patterns) :-
	p_match(Patterns,D),
	p_investigate(Data,Patterns).

p_match([],_).
p_match([P|Patterns],D) :-
	(match(D,P),fail; true),
	p_match(Patterns,D).

match([],[]) :- !.
match([X|PRest],[Y|SRest]) :-
	var(Y),!,X = Y,
	match(PRest,SRest).
match(List,[Y|Rest]) :- 
	nonvar(Y),Y = star(X),!,
	concat(X,SRest,List),
	match(SRest,Rest).
match([X|PRest],[Y|SRest]) :-
	(atom(X) -> X = Y; match(X,Y)),
	match(PRest,SRest).

concat([],L,L).
concat([X|L1],L2,[X|L3]) :- concat(L1,L2,L3).

%
% press1
%
% An adaption of part of the PRESS symbolic algebra system
% from The Art of Prolog by Sterling and Shapiro
%
main :- equation(_, E, U), solve_equation(E, U, Y),
	write(E), write(' -> '), write(Y), nl, fail.

equation(1, 3*x+1=0, x).
equation(2, x+2=0, x).
equation(3, cos(x)*(1-2*sin(x))=0, x).
equation(4, x^2-3*x+2=0, x).
equation(5, 2^(2*x)-5*2^(x+1)+16=0, x).

solve_equation(A*B=0,X,Solution) :-
	!,
	factorize(A*B, X, Factors/[]),
	remove_duplicates(Factors, Factors1),
	solve_factors(Factors1, X, Solution).
solve_equation(Equation, X, Solution) :-
	single_occurrence(X, Equation),
	!,
	position(X, Equation, [Side|Position]),
	maneuver_sides(Side, Equation, Equation1),
	isolate(Position, Equation1, Solution).
solve_equation(Lhs=Rhs, X, Solution) :-
	polynomial(Lhs, X),
	polynomial(Rhs, X),
	!,
	polynomial_normal_form(Lhs-Rhs, X, PolyForm),
	solve_polynomial_equation(PolyForm, X, Solution).
solve_equation(Equation, X, Solution) :-
	homogenize(Equation, X, Equation1, X1),
	!,
	solve_equation(Equation1, X1, Solution1),
	solve_equation(Solution1, X, Solution).

factorize(A*B, X, Factors/Rest) :-
	!, factorize(A, X, Factors/Factors1),
	factorize(B, X, Factors1/Rest).
factorize(C, X, [C|Factors]/Factors) :-
	subterm(X, C), !.
factorize(_, _, Factors/Factors).

solve_factors([Factor|_], X, Solution) :-
	solve_equation(Factor=0, X, Solution).
solve_factors([_|Factors], X, Solution) :-
	solve_factors(Factors, X, Solution).

maneuver_sides(1, Lhs = Rhs, Lhs = Rhs) :- !.
maneuver_sides(2, Lhs = Rhs, Rhs = Lhs) :- !.

isolate([N|Position], Equation, IsolatedEquation) :-
	isolax(N, Equation, Equation1),
	isolate(Position, Equation1, IsolatedEquation).
isolate([], Equation, Equation).

isolax(1, -Lhs = Rhs, Lhs = -Rhs).
isolax(1, Term1+Term2 = Rhs, Term1 = Rhs-Term2).
isolax(2, Term1+Term2 = Rhs, Term2 = Rhs-Term1).
isolax(1, Term1-Term2 = Rhs, Term1 = Rhs+Term2).
isolax(2, Term1-Term2 = Rhs, Term2 = Term1-Rhs).
isolax(1, Term1*Term2 = Rhs, Term1 = Rhs/Term2) :-
	Term2 =\= 0.
isolax(2, Term1*Term2 = Rhs, Term2 = Rhs/Term1) :-
	Term1 =\= 0.
isolax(1, Term1^Term2 = Rhs, Term1 = Rhs^(-Term2)).
isolax(2, Term1^Term2 = Rhs, Term2 = log(base(Term1), Rhs)).
isolax(1, sin(U) = V, U = arcsin(V)).
isolax(1, sin(U) = V, U = pi-arcsin(V)).
isolax(1, cos(U) = V, U = arccos(V)).
isolax(1, cos(U) = V, U = -arccos(V)).

polynomial(X, X) :- !.
polynomial(Term, _) :- atomic(Term), !.
polynomial(Term1+Term2, X) :-
	!, polynomial(Term1, X), polynomial(Term2, X).
polynomial(Term1-Term2, X) :-
	!, polynomial(Term1, X), polynomial(Term2, X).
polynomial(Term1*Term2, X) :-
	!, polynomial(Term1, X), polynomial(Term2, X).
polynomial(Term1/Term2, X) :-
	!, polynomial(Term1, X), polynomial(Term2, X).
polynomial(Term^N, X) :-
	!, integer(N), polynomial(Term, X).

polynomial_normal_form(Polynomial, X, NormalForm) :-
	polynomial_form(Polynomial, X, PolyForm),
	remove_zero_terms(PolyForm, NormalForm), !.

polynomial_form(X, X, [(1,1)]).
polynomial_form(X^N, X, [(1,N)]).
polynomial_form(Term1+Term2, X, PolyForm) :-
	polynomial_form(Term1, X, PolyForm1),
	polynomial_form(Term2, X, PolyForm2),
	add_polynomials(PolyForm1, PolyForm2, PolyForm).
polynomial_form(Term1-Term2, X, PolyForm) :-
	polynomial_form(Term1, X, PolyForm1),
	polynomial_form(Term2, X, PolyForm2),
	subtract_polynomials(PolyForm1, PolyForm2, PolyForm).
polynomial_form(Term1*Term2, X, PolyForm) :-
	polynomial_form(Term1, X, PolyForm1),
	polynomial_form(Term2, X, PolyForm2),
	multiply_polynomials(PolyForm1, PolyForm2, PolyForm).
polynomial_form(Term^N, X, PolyForm) :-
	polynomial_form(Term, X, PolyForm1),
	binomial(PolyForm1, N, PolyForm).
polynomial_form(Term, X, [(Term,0)]) :-
	free_of(X, Term).

remove_zero_terms([(0,_)|Poly], Poly1) :-
	!, remove_zero_terms(Poly, Poly1).
remove_zero_terms([(C,N)|Poly], [(C,N)|Poly1]) :-
	C =\= 0, !, remove_zero_terms(Poly, Poly1).
remove_zero_terms([], []).

add_polynomials([], Poly, Poly) :- !.
add_polynomials(Poly, [], Poly) :- !.
add_polynomials([(Ai,Ni)|Poly1],[(Aj,Nj)|Poly2],[(Ai,Ni)|Poly]) :-
	Ni > Nj, !, add_polynomials(Poly1, [(Aj, Nj)|Poly2], Poly).
add_polynomials([(Ai,Ni)|Poly1],[(Aj,Nj)|Poly2],[(A,Ni)|Poly]) :-
	Ni =:= Nj, !, A is Ai + Aj, add_polynomials(Poly1, Poly2, Poly).
add_polynomials([(Ai,Ni)|Poly1],[(Aj,Nj)|Poly2],[(Aj,Nj)|Poly]) :-
	Ni < Nj, !, add_polynomials([(Ai, Ni)|Poly1], Poly2, Poly).

subtract_polynomials(Poly1, Poly2, Poly) :-
	multiply_single(Poly2, (-1, 0), Poly3),
	add_polynomials(Poly1, Poly3, Poly), !.

multiply_single([(C1,N1)|Poly1], (C,N), [(C2,N2)|Poly]) :-
	C2 is C1*C, N2 is N1 + N, multiply_single(Poly1, (C, N), Poly).
multiply_single([], _, []).

multiply_polynomials([(C,N)|Poly1], Poly2, Poly) :-
	multiply_single(Poly2, (C,N), Poly3),
	multiply_polynomials(Poly1, Poly2, Poly4),
	add_polynomials(Poly3, Poly4, Poly).
multiply_polynomials([], _, []).

binomial(Poly, 1, Poly). /* ? */

solve_polynomial_equation(PolyEquation, X, X = - B/A) :-
	linear(PolyEquation), !,
	pad(PolyEquation, [(A,1),(B,0)]).
solve_polynomial_equation(PolyEquation, X, Solution) :-
	quadratic(PolyEquation), !,
	pad(PolyEquation, [(A,2),(B,1),(C,0)]),
	discriminant(A, B, C, Discriminant),
	root(X, A, B, C, Discriminant, Solution).

discriminant(A, B, C, D) :- D is B*B - 4*A*C.

root(X, A, B, _, 0, X = -B/(2*A)).
root(X, A, B, _, D, X = (-B+sqrt(D))/(2*A)).
root(X, A, B, _, D, X = (-B-sqrt(D))/(2*A)).

pad([(C,N)|Poly], [(C,N)|Poly1]) :-
	!, pad(Poly, Poly1).
pad(Poly, [(0,_)|Poly1]) :-
	!, pad(Poly, Poly1).
pad([], []).

linear([(_,1)|_]).

quadratic([(_, 2)|_]).

homogenize(Equation, X, Equation1, X1) :-
	offenders(Equation, X, Offenders),
	reduced_term(X, Offenders, Type, X1),
	rewrite(Offenders, Type, X1, Substitutions),
	substitute(Equation, Substitutions, Equation1).

offenders(Equation, X, Offenders) :-
	parse(Equation, X, Offenders1/[]),
	remove_duplicates(Offenders1, Offenders),
	multiple(Offenders).

reduced_term(X, Offenders, Type, X1) :-
	classify(Offenders, X, Type),
	candidate(Type, Offenders, X, X1).

classify(Offenders, X, exponential) :-
	exponential_offenders(Offenders, X).

exponential_offenders([A^B|Offs], X) :-
	free_of(X, A),
	subterm(X, B),
	exponential_offenders(Offs, X).
exponential_offenders([], _).

candidate(exponential, Offenders, X, A^X) :-
	base(Offenders, A), polynomial_exponents(Offenders, X).

base([A^_|Offs], A) :- base(Offs, A).
base([], _).

polynomial_exponents([_^B|Offs], X) :-
	polynomial(B, X), polynomial_exponents(Offs, X).
polynomial_exponents([], _).


parse(A+B, X, L1/L2) :-
	!, parse(A, X, L1/L3), parse(B, X, L3/L2).
parse(A*B, X, L1/L2) :-
	!, parse(A, X, L1/L3), parse(B, X, L3/L2).
parse(A-B, X, L1/L2) :-
	!, parse(A, X, L1/L3), parse(B, X, L3/L2).
parse(A=B, X, L1/L2) :-
	!, parse(A, X, L1/L3), parse(B, X, L3/L2). /* ? */
parse(A^B, X, L) :-
	integer(B), !, parse(A, X, L). /* ? */
parse(A, X, L/L) :- free_of(X, A), !.
parse(A, X, [A|L]/L) :- subterm(X, A), !.

substitute(A+B, Subs, NewA+NewB) :-
	!, substitute(A, Subs, NewA), substitute(B, Subs, NewB).
substitute(A*B, Subs, NewA*NewB) :-
	!, substitute(A, Subs, NewA), substitute(B, Subs, NewB).
substitute(A-B, Subs, NewA-NewB) :-
	!, substitute(A, Subs, NewA), substitute(B, Subs, NewB).
substitute(A=B, Subs, NewA=NewB) :-
	!, substitute(A, Subs, NewA), substitute(B, Subs, NewB).
substitute(A^B, Subs, NewA^B) :-
	integer(B), !, substitute(A, Subs, NewA).
substitute(A, Subs, B) :-
	member(A = B, Subs), !.
substitute(A, _, A).

rewrite([Off|Offs], Type, X1, [Off=Term|Rewrites]) :-
	homog_axiom(Type, Off, X1, Term),
	rewrite(Offs, Type, X1, Rewrites).
rewrite([], _, _, []).

homog_axiom(exponential, A^(N*X), A^X, (A^X)^N).
homog_axiom(exponential, A^(-X), A^X, 1/(A^X)).
homog_axiom(exponential, A^(X+B), A^X, A^B*A^X).

subterm(Term, Term).
subterm(Sub, Term) :-
	functor(Term, _, N), N > 0, subterm(N, Sub, Term).

subterm(N, Sub, Term) :-
	N > 1, N1 is N - 1, subterm(N1, Sub, Term).
subterm(N, Sub, Term) :-
	arg(N, Term, Arg), subterm(Sub, Arg).

position(Term, Term, []) :- !.
position(Sub, Term, Path) :-
	functor(Term, _, N), N > 0,
	position(N, Sub, Term, Path), !.

position(N, Sub, Term, [N|Path]) :-
	arg(N, Term, Arg), position(Sub, Arg, Path).
position(N, Sub, Term, Path) :-
	N > 1, N1 is N - 1, position(N1, Sub, Term, Path).

free_of(Subterm, Term) :-
	occurrence(Subterm, Term, N), !, N = 0.

single_occurrence(Subterm, Term) :-
	occurrence(Subterm, Term, N), !, N = 1.

occurrence(Term, Term, 1) :- !.
occurrence(Sub, Term, N) :-
	functor(Term, _, M), M > 0, !,
	occurrence(M, Sub, Term, 0, N).
occurrence(_, _, 0).

occurrence(M, Sub, Term, N1, N2) :-
	M > 0, !, arg(M, Term, Arg), occurrence(Sub, Arg, N),
	N3 is N + N1, M1 is M - 1,
	occurrence(M1, Sub, Term, N3, N2).
occurrence(0, _, _, N, N).

multiple([_,_|_]).

remove_duplicates(X, X).

member(H, [H|_]).
member(H, [_|T]) :- member(H, T).

%
%  reducer
%
% A Graph Reducer for T-Combinators:
% Reduces a T-combinator expression to a final answer.  Recognizes
% the combinators I,K,S,B,C,S',B',C', cond, apply, arithmetic, tests,
% basic list operations, and function definitions in the data base stored
% as facts of the form t_def(_func, _args, _expr).
% Written by Peter Van Roy

% Uses write/1, compare/3, functor/3, arg/3.
main :-
	try(fac(3), _ans1),
	write(_ans1), nl,
	try(quick([3,1,2]), _ans2),
	write(_ans2), nl.

try(_inpexpr, _anslist) :-
	listify(_inpexpr, _list),
	curry(_list, _curry),
	t_reduce(_curry, _ans), nl,
	make_list(_ans, _anslist).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Examples of applicative functions which can be compiled & executed.
% This test version compiles them just before each execution.

% Factorial function:
t_def(fac, [N], cond(N=0, 1, N*fac(N-1))).

% Quicksort:
t_def(quick, [_l], cond(_l=[], [],
		 cond(tl(_l)=[], _l,
		 quick2(split(hd(_l),tl(_l)))))).
t_def(quick2, [_l], append(quick(hd(_l)), quick(tl(_l)))).

t_def(split, [_e,_l], cond(_l=[], [[_e]|[]],
		    cond(hd(_l)=<_e, inserthead(hd(_l),split(_e,tl(_l))),
		    inserttail(hd(_l),split(_e,tl(_l)))))).
t_def(inserthead, [_e,_l], [[_e|hd(_l)]|tl(_l)]).
t_def(inserttail, [_e,_l], [hd(_l)|[_e|tl(_l)]]).

t_def(append, [_a,_b], cond(_a=[], _b, [hd(_a)|append(tl(_a),_b)])).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Full reduction:
% A dot '.' is printed for each reduction step.

t_reduce(_expr, _ans) :-
	atomic(_expr), !,
	 _ans=_expr.
% The reduction of '.' must be here to avoid an infinite loop
t_reduce([_y,_x|'.'], [_yr,_xr|'.']) :-
	t_reduce(_x, _xr),
	!,
	t_reduce(_y, _yr),
	!.
t_reduce(_expr, _ans) :-
	t_append(_next, _red, _form, _expr),
	write('.'),
	t_redex(_form, _red),
	!,
	t_reduce(_next, _ans), 
	!.

t_append(_link, _link, _l, _l).
t_append([_a|_l1], _link, _l2, [_a|_l3]) :- t_append(_l1, _link, _l2, _l3).

% One step of the reduction:

% Combinators:
t_redex([_x,_g,_f,_k|sp], [[_xr|_g],[_xr|_f]|_k]) :- t_reduce(_x, _xr).
t_redex([_x,_g,_f,_k|bp], [[_x|_g],_f|_k]).
t_redex([_x,_g,_f,_k|cp], [_g,[_x|_f]|_k]).
t_redex([_x,_g,_f|s], [[_xr|_g]|[_xr|_f]]) :- t_reduce(_x, _xr).
t_redex([_x,_g,_f|b], [[_x|_g]|_f]).
t_redex([_x,_g,_f|c], [_g,_x|_f]).
t_redex([_y,_x|k], _x).
t_redex([_x|i], _x).

% Conditional:
t_redex([_elsepart,_ifpart,_cond|cond], _ifpart) :-
	t_reduce(_cond, _bool), _bool=true, !.
	% Does NOT work if _bool is substituted in the call!
t_redex([_elsepart,_ifpart,_cond|cond], _elsepart).

% Apply:
t_redex([_f|apply], _fr) :- 
	t_reduce(_f, _fr).

% List operations:
t_redex([_arg|hd], _x) :- 
	t_reduce(_arg, [_y,_x|'.']).
t_redex([_arg|tl], _y) :- 
	t_reduce(_arg, [_y,_x|'.']).

% Arithmetic:
t_redex([_y,_x|_op], _res) :-
	atom(_op),
	member(_op, ['+', '-', '*', '//', 'mod']),
	t_reduce(_x, _xres),
	t_reduce(_y, _yres),
	number(_xres), number(_yres),
	eval(_op, _res, _xres, _yres).

% Tests:
t_redex([_y,_x|_test], _res) :-
	atom(_test),
	member(_test, ['<', '>', '=<', '>=', '=\=', '=:=']),
	t_reduce(_x, _xres),
	t_reduce(_y, _yres),
	number(_xres), number(_yres),
	(relop(_test, _xres, _yres)
	-> _res=true
	;  _res=false
	), !.

% Equality:
t_redex([_y,_x|=], _res) :-
	t_reduce(_x, _xres),
	t_reduce(_y, _yres),
	(_xres=_yres -> _res=true; _res=false), !.

% Arithmetic functions:
t_redex([_x|_op], _res) :-
	atom(_op),
	member(_op, ['-']),
	t_reduce(_x, _xres),
	number(_xres),
	eval1(_op, _t, _xres).

% Definitions:
% Assumes a fact t_def(_func,_def) in the database for every
% defined function.
t_redex(_in, _out) :-
	append(_par,_func,_in),
	atom(_func),
	t_def(_func, _args, _expr),
	t(_args, _expr, _def),
	append(_par,_def,_out).

% Basic arithmetic and relational operators:

eval(  '+', C, A, B) :- C is A + B.
eval(  '-', C, A, B) :- C is A - B.
eval(  '*', C, A, B) :- C is A * B.
eval( '//', C, A, B) :- C is A // B.
eval('mod', C, A, B) :- C is A mod B.

eval1('-', C, A) :- C is -A.

relop(  '<', A, B) :- A<B.
relop(  '>', A, B) :- A>B.
relop( '=<', A, B) :- A=<B.
relop( '>=', A, B) :- A>=B.
relop('=\=', A, B) :- A=\=B.
relop('=:=', A, B) :- A=:=B.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Scheme T:
% A Translation Scheme for T-Combinators

% Translate an expression to combinator form
% by abstracting out all variables in _argvars:
t(_argvars, _expr, _trans) :-
	listify(_expr, _list),
	curry(_list, _curry),
	t_argvars(_argvars, _curry, _trans), !.

t_argvars([], _trans, _trans).
t_argvars([_x|_argvars], _in, _trans) :-
	t_argvars(_argvars, _in, _mid),
	t_vars(_mid, _vars), % calculate variables in each subexpression
	t_trans(_x, _mid, _vars, _trans). % main translation routine

% Curry the original expression:
% This converts an applicative expression of any number
% of arguments and any depth of nesting into an expression
% where all functions are curried, i.e. all function
% applications are to one argument and have the form
% [_arg|_func] where _func & _arg are also of that form.
% Input is a nested function application in list form.
% Currying makes t_trans faster.
curry(_a, _a) :- (var(_a); atomic(_a)), !.
curry([_func|_args], _cargs) :-
	currylist(_args, _cargs, _func).

% Transform [_a1, ..., _aN] to [_cN, ..., _c1|_link]-_link
currylist([], _link, _link) :- !.
currylist([_a|_args], _cargs, _link) :-
	curry(_a, _c),
	currylist(_args, _cargs, [_c|_link]).

% Calculate variables in each subexpression:
% To any expression a list of the form
% [_vexpr, _astr, _fstr] is matched.
% If the expression is a variable or an atom
% then this list only has the first element.
% _vexpr = List of all variables in the expression.
% _astr, _fstr = Similar structures for argument & function.
t_vars(_v, [[_v]]) :- var(_v), !.
t_vars(_a, [[]]) :- atomic(_a), !.
t_vars([_func], [[]]) :- atomic(_func), !.
t_vars([_arg|_func], [_g,[_g1|_af1],[_g2|_af2]]) :-
	t_vars(_arg, [_g1|_af1]),
	t_vars(_func, [_g2|_af2]),
	unionv(_g1, _g2, _g).

% The main translation routine:
% trans(_var, _curriedexpr, _varexpr, _result)
% The translation scheme T in the article is followed literally.
% A good example of Prolog as a specification language.
t_trans(_x, _a, _, [_a|k]) :- (atomic(_a); var(_a), _a\==_x), !.
t_trans(_x, _y, _, i) :- _x==_y, !.
t_trans(_x, _e, [_ve|_], [_e|k]) :- notinv(_x, _ve).
t_trans(_x, [_f|_e], [_vef,_sf,_se], _res) :-
	_sf=[_vf|_],
	_se=[_ve|_other],
	(atom(_e); _other=[_,[_ve1|_]], _ve1\==[]),
	t_rule1(_x, _e, _ve, _se, _f, _vf, _sf, _res).
t_trans(_x, [_g|[_f|_e]], [_vefg,_sg,_sef], _res) :-
	_sg=[_vg|_],
	_sef=[_vef,_sf,_se],
	_se=[_ve|_],
	_sf=[_vf|_],
	t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, _res).

% First complex rule of translation scheme T:
t_rule1(_x, _e, _ve, _se, _f, _vf, _sf, _e) :-
	notinv(_x, _ve), _x==_f, !.
t_rule1(_x, _e, _ve, _se, _f, _vf, _sf, [_resf,_e|b]) :-
	notinv(_x, _ve), inv(_x, _vf), _x\==_f, !,
	t_trans(_x, _f, _sf, _resf).
t_rule1(_x, _e, _ve, _se, _f, _vf, _sf, [_f,_rese|c]) :-
	/* inv(_x, _ve), */ 
	notinv(_x, _vf), !,
	t_trans(_x, _e, _se, _rese).
t_rule1(_x, _e, _ve, _se, _f, _vf, _sf, [_resf,_rese|s]) :-
	/* inv(_x, _ve), inv(_x, _vf), */
	t_trans(_x, _e, _se, _rese),
	t_trans(_x, _f, _sf, _resf).

% Second complex rule of translation scheme T:
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_g,_e|c]) :-
	_x==_f, notinv(_x, _vg), !.
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_resg,_e|s]) :-
	_x==_f, /* inv(_x, _vg), */ !,
	t_trans(_x, _g, _sg, _resg).
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_g,_resf,_e|cp]) :-
	/* _x\==_f, */ inv(_x, _vf), notinv(_x, _vg), !,
	t_trans(_x, _f, _sf, _resf).
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_resg,_resf,_e|sp]) :-
	/* _x\==_f, */ inv(_x, _vf), /* inv(_x, _vg), */ !,
	t_trans(_x, _f, _sf, _resf),
	t_trans(_x, _g, _sg, _resg).
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_f|_e]) :-
	/* notinv(_x, _vf), */ _x==_g, !.
t_rule2(_x, _e, _f, _vf, _sf, _g, _vg, _sg, [_resg,_f,_e|bp]) :-
	/* notinv(_x, _vf), inv(_x, _vg), _x\==_g, */
	t_trans(_x, _g, _sg, _resg).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% List utilities:

% Convert curried list into a regular list:
make_list(_a, _a) :- atomic(_a).
make_list([_b,_a|'.'], [_a|_rb]) :- make_list(_b, _rb).

listify(_X, _X) :- 
	(var(_X); atomic(_X)), !.
listify(_Expr, [_Op|_LArgs]) :-
	functor(_Expr, _Op, N),
	listify_list(1, N, _Expr, _LArgs).

listify_list(I, N, _, []) :- I>N, !.
listify_list(I, N, _Expr, [_LA|_LArgs]) :- I=<N, !,
	arg(I, _Expr, _A),
	listify(_A, _LA),
	I1 is I+1,
	listify_list(I1, N, _Expr, _LArgs).

member(X, [X|_]).
member(X, [_|L]) :- member(X, L).

append([], L, L).
append([X|L1], L2, [X|L3]) :- append(L1, L2, L3).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Set utilities:
% Implementation inspired by R. O'Keefe, Practical Prolog.
% Sets are represented as sorted lists without duplicates.
% Predicates with 'v' suffix work with sets containing
% uninstantiated vars.

% *** Intersection
intersectv([], _, []).
intersectv([A|S1], S2, S) :- intersectv_2(S2, A, S1, S).

intersectv_2([], _, _, []).
intersectv_2([B|S2], A, S1, S) :-
	compare(Order, A, B),
	intersectv_3(Order, A, S1, B, S2, S).

intersectv_3(<, _, S1, B, S2,     S) :- intersectv_2(S1, B, S2, S).
intersectv_3(=, A, S1, _, S2, [A|S]) :- intersectv(S1, S2, S).
intersectv_3(>, A, S1, _, S2,     S) :- intersectv_2(S2, A, S1, S).

intersectv_list([], []).
intersectv_list([InS|Sets], OutS) :- intersectv_list(Sets, InS, OutS).

intersectv_list([]) --> [].
intersectv_list([S|Sets]) --> intersectv(S), intersectv_list(Sets).

% *** Difference
diffv([], _, []).
diffv([A|S1], S2, S) :- diffv_2(S2, A, S1, S).

diffv_2([], A, S1, [A|S1]).
diffv_2([B|S2], A, S1, S) :-
	compare(Order, A, B),
	diffv_3(Order, A, S1, B, S2, S).
 
diffv_3(<, A, S1, B, S2, [A|S]) :- diffv(S1, [B|S2], S).
diffv_3(=, A, S1, _, S2,     S) :- diffv(S1, S2, S).
diffv_3(>, A, S1, _, S2,     S) :- diffv_2(S2, A, S1, S).
 
% *** Union
unionv([], S2, S2).
unionv([A|S1], S2, S) :- unionv_2(S2, A, S1, S).
 
unionv_2([], A, S1, [A|S1]).
unionv_2([B|S2], A, S1, S) :-
	compare(Order, A, B),
	unionv_3(Order, A, S1, B, S2, S).
 
unionv_3(<, A, S1, B, S2, [A|S]) :- unionv_2(S1, B, S2, S).
unionv_3(=, A, S1, _, S2, [A|S]) :- unionv(S1, S2, S).
unionv_3(>, A, S1, B, S2, [B|S]) :- unionv_2(S2, A, S1, S).
 
% *** Subset
subsetv([], _).
subsetv([A|S1], [B|S2]) :-
	compare(Order, A, B),
	subsetv_2(Order, A, S1, S2).
 
subsetv_2(=, _, S1, S2) :- subsetv(S1, S2).
subsetv_2(>, A, S1, S2) :- subsetv([A|S1], S2).
 
% For unordered lists S1:
small_subsetv([], _).
small_subsetv([A|S1], S2) :- inv(A, S2), small_subsetv(S1, S2).
 
% *** Membership
inv(A, [B|S]) :-
	compare(Order, A, B),
	inv_2(Order, A, S).
 
inv_2(=, _, _).
inv_2(>, A, S) :- inv(A, S).

% *** Non-membership
notinv(A, S) :- notinv_2(S, A).

notinv_2([], _).
notinv_2([B|S], A) :-
	compare(Order, A, B),
	notinv_3(Order, A, S).
 
notinv_3(<, _, _).
notinv_3(>, A, S) :- notinv_2(S, A).

%
%   boyer
%
%   Evan Tick (from Lisp version by R. P. Gabriel)
%
%   November 1985
%
%   prove arithmetic theorem

main :- wff(Wff),
	rewrite(Wff,NewWff),
	tautology(NewWff,[],[]).

wff(implies(and(implies(X,Y),
		and(implies(Y,Z),
		    and(implies(Z,U),
			implies(U,W)))),
	    implies(X,W))) :-
	X = f(plus(plus(a,b),plus(c,zero))),
	Y = f(times(times(a,b),plus(c,d))),
	Z = f(reverse(append(append(a,b),[]))),
	U = equal(plus(a,b),difference(x,y)),
	W = lessp(remainder(a,b),member(a,length(b))).

tautology(Wff) :-
	write('rewriting...'),nl,
	rewrite(Wff,NewWff),
	write('proving...'),nl,
	tautology(NewWff,[],[]).

tautology(Wff,Tlist,Flist) :-
	(truep(Wff,Tlist) -> true
	;falsep(Wff,Flist) -> fail
	;Wff = if(If,Then,Else) ->
		(truep(If,Tlist) -> tautology(Then,Tlist,Flist)
		;falsep(If,Flist) -> tautology(Else,Tlist,Flist)
		;tautology(Then,[If|Tlist],Flist),	% both must hold
		 tautology(Else,Tlist,[If|Flist])
		)
	),!.

rewrite(Atom,Atom) :-
	atomic(Atom),!.
rewrite(Old,New) :-
	functor(Old,F,N),
	functor(Mid,F,N),
	rewrite_args(N,Old,Mid),
	( equal(Mid,Next),        % should be ->, but is compiler smart
	  rewrite(Next,New)       % enough to generate cut for -> ?
	; New=Mid
	),!.

rewrite_args(0,_,_) :- !.
rewrite_args(N,Old,Mid) :- 
	arg(N,Old,OldArg),
	arg(N,Mid,MidArg),
	rewrite(OldArg,MidArg),
	N1 is N-1,
	rewrite_args(N1,Old,Mid).

truep(t,_) :- !.
truep(Wff,Tlist) :- member(Wff,Tlist).

falsep(f,_) :- !.
falsep(Wff,Flist) :- member(Wff,Flist).

member(X,[X|_]) :- !.
member(X,[_|T]) :- member(X,T).


equal(  and(P,Q),
	if(P,if(Q,t,f),f)
	).
equal(  append(append(X,Y),Z),
	append(X,append(Y,Z))
	).
equal(  assignment(X,append(A,B)),
	if(assignedp(X,A),
	   assignment(X,A),
	   assignment(X,B))
	).
equal(  assume_false(Var,Alist),
	cons(cons(Var,f),Alist)
	).
equal(  assume_true(Var,Alist),
	cons(cons(Var,t),Alist)
	).
equal(  boolean(X),
	or(equal(X,t),equal(X,f))
	).
equal(  car(gopher(X)),
	if(listp(X),
	car(flatten(X)),
	zero)
	).
equal(  compile(Form),
	reverse(codegen(optimize(Form),[]))
	).
equal(  count_list(Z,sort_lp(X,Y)),
	plus(count_list(Z,X),
	     count_list(Z,Y))
	).
equal(  countps_(L,Pred),
	countps_loop(L,Pred,zero)
	).
equal(  difference(A,B),
	C
	) :- difference(A,B,C).
equal(  divides(X,Y),
	zerop(remainder(Y,X))
	).
equal(  dsort(X),
	sort2(X)
	).
equal(  eqp(X,Y),
	equal(fix(X),fix(Y))
	).
equal(  equal(A,B),
	C
	) :- eq(A,B,C).
equal(  even1(X),
	if(zerop(X),t,odd(decr(X)))
	).
equal(  exec(append(X,Y),Pds,Envrn),
	exec(Y,exec(X,Pds,Envrn),Envrn)
	).
equal(  exp(A,B),
	C
	) :- exp(A,B,C).
equal(  fact_(I),
	fact_loop(I,1)
	).
equal(  falsify(X),
	falsify1(normalize(X),[])
	).
equal(  fix(X),
	if(numberp(X),X,zero)
	).
equal(  flatten(cdr(gopher(X))),
	if(listp(X),
	   cdr(flatten(X)),
	   cons(zero,[]))
	).
equal(  gcd(A,B),
	C
	) :- gcd(A,B,C).
equal(  get(J,set(I,Val,Mem)),
	if(eqp(J,I),Val,get(J,Mem))
	).
equal(  greatereqp(X,Y),
	not(lessp(X,Y))
	).
equal(  greatereqpr(X,Y),
	not(lessp(X,Y))
	).
equal(  greaterp(X,Y),
	lessp(Y,X)
	).
equal(  if(if(A,B,C),D,E),
	if(A,if(B,D,E),if(C,D,E))
	).
equal(  iff(X,Y),
	and(implies(X,Y),implies(Y,X))
	).
equal(  implies(P,Q),
	if(P,if(Q,t,f),t)
	).
equal(  last(append(A,B)),
	if(listp(B),
	   last(B),
	   if(listp(A),
	      cons(car(last(A))),
	      B))
	).
equal(  length(A),
	B
	) :- mylength(A,B).
equal(        lesseqp(X,Y),
	not(lessp(Y,X))
	).
equal(  lessp(A,B),
	C
	) :- lessp(A,B,C).
equal(  listp(gopher(X)),
	listp(X)
	).
equal(  mc_flatten(X,Y),
	append(flatten(X),Y)
	).
equal(  meaning(A,B),
	C
	) :- meaning(A,B,C).
equal(  member(A,B),
	C
	) :- mymember(A,B,C).
equal(  not(P),
	if(P,f,t)
	).
equal(  nth(A,B),
	C
	) :- nth(A,B,C).
equal(  numberp(greatest_factor(X,Y)),
	not(and(or(zerop(Y),equal(Y,1)),
		not(numberp(X))))            
	).
equal(  or(P,Q),
	if(P,t,if(Q,t,f),f)
	).
equal(  plus(A,B),
	C
	) :- plus(A,B,C).
equal(  power_eval(A,B),
	C
	) :- power_eval(A,B,C).
equal(  prime(X),
	and(not(zerop(X)),
	    and(not(equal(X,add1(zero))),
		prime1(X,decr(X))))
	).
equal(  prime_list(append(X,Y)),
	and(prime_list(X),prime_list(Y))
	).
equal(  quotient(A,B),
	C
	) :- quotient(A,B,C).
equal(  remainder(A,B),
	C
	) :- remainder(A,B,C).
equal(  reverse_(X),
	reverse_loop(X,[])
	).
equal(  reverse(append(A,B)),
	append(reverse(B),reverse(A))
	).
equal(  reverse_loop(A,B),
	C
	) :- reverse_loop(A,B,C).
equal(  samefringe(X,Y),
	equal(flatten(X),flatten(Y))
	).
equal(  sigma(zero,I),
	quotient(times(I,add1(I)),2)
	).
equal(  sort2(delete(X,L)),
	delete(X,sort2(L))
	).
equal(  tautology_checker(X),
	tautologyp(normalize(X),[])
	).
equal(  times(A,B),
	C
	) :- times(A,B,C).
equal(  times_list(append(X,Y)),
	times(times_list(X),times_list(Y))
	).
equal(  value(normalize(X),A),
	value(X,A)
	).
equal(  zerop(X),
	or(equal(X,zero),not(numberp(X)))
	).

difference(X, X, zero) :- !.
difference(plus(X,Y), X, fix(Y)) :- !.
difference(plus(Y,X), X, fix(Y)) :- !.
difference(plus(X,Y), plus(X,Z), difference(Y,Z)) :- !.
difference(plus(B,plus(A,C)), A, plus(B,C)) :- !.
difference(add1(plus(Y,Z)), Z, add1(Y)) :- !.
difference(add1(add1(X)), 2, fix(X)).

eq(plus(A,B), zero, and(zerop(A),zerop(B))) :- !.
eq(plus(A,B), plus(A,C), equal(fix(B),fix(C))) :- !.
eq(zero, difference(X,Y),not(lessp(Y,X))) :- !.
eq(X, difference(X,Y),and(numberp(X),
			  and(or(equal(X,zero),
				 zerop(Y))))) :- !.
eq(times(X,Y), zero, or(zerop(X),zerop(Y))) :- !.
eq(append(A,B), append(A,C), equal(B,C)) :- !.
eq(flatten(X), cons(Y,[]), and(nlistp(X),equal(X,Y))) :- !.
eq(greatest_factor(X,Y),zero, and(or(zerop(Y),equal(Y,1)),
				     equal(X,zero))) :- !.
eq(greatest_factor(X,_),1, equal(X,1)) :- !.
eq(Z, times(W,Z), and(numberp(Z),
		      or(equal(Z,zero),
			 equal(W,1)))) :- !.
eq(X, times(X,Y), or(equal(X,zero),
		     and(numberp(X),equal(Y,1)))) :- !.
eq(times(A,B), 1, and(not(equal(A,zero)),
		      and(not(equal(B,zero)),
			  and(numberp(A),
			      and(numberp(B),
				  and(equal(decr(A),zero),
				      equal(decr(B),zero))))))) :- !.
eq(difference(X,Y), difference(Z,Y),if(lessp(X,Y),
				       not(lessp(Y,Z)),
				       if(lessp(Z,Y),
					  not(lessp(Y,X)),
					  equal(fix(X),fix(Z))))) :- !.
eq(lessp(X,Y), Z, if(lessp(X,Y),
		     equal(t,Z),
		     equal(f,Z))).

exp(I, plus(J,K), times(exp(I,J),exp(I,K))) :- !.
exp(I, times(J,K), exp(exp(I,J),K)).

gcd(X, Y, gcd(Y,X)) :- !.
gcd(times(X,Z), times(Y,Z), times(Z,gcd(X,Y))).

mylength(reverse(X),length(X)).
mylength(cons(_,cons(_,cons(_,cons(_,cons(_,cons(_,X7)))))),
	 plus(6,length(X7))).

lessp(remainder(_,Y), Y, not(zerop(Y))) :- !.
lessp(quotient(I,J), I, and(not(zerop(I)),
			    or(zerop(J),
			       not(equal(J,1))))) :- !.
lessp(remainder(X,Y), X, and(not(zerop(Y)),
			     and(not(zerop(X)),
				 not(lessp(X,Y))))) :- !.
lessp(plus(X,Y), plus(X,Z), lessp(Y,Z)) :- !.
lessp(times(X,Z), times(Y,Z), and(not(zerop(Z)),
				  lessp(X,Y))) :- !.
lessp(Y, plus(X,Y), not(zerop(X))) :- !.
lessp(length(delete(X,L)), length(L), member(X,L)).

meaning(plus_tree(append(X,Y)),A,
	plus(meaning(plus_tree(X),A),
	     meaning(plus_tree(Y),A))) :- !.
meaning(plus_tree(plus_fringe(X)),A,
	fix(meaning(X,A))) :- !.
meaning(plus_tree(delete(X,Y)),A,
	if(member(X,Y),
	   difference(meaning(plus_tree(Y),A),
		      meaning(X,A)),
	   meaning(plus_tree(Y),A))).

mymember(X,append(A,B),or(member(X,A),member(X,B))) :- !.
mymember(X,reverse(Y),member(X,Y)) :- !.
mymember(A,intersect(B,C),and(member(A,B),member(A,C))).

nth(zero,_,zero).
nth([],I,if(zerop(I),[],zero)).
nth(append(A,B),I,append(nth(A,I),nth(B,difference(I,length(A))))).

plus(plus(X,Y),Z,
	 plus(X,plus(Y,Z))) :- !.
plus(remainder(X,Y),
	 times(Y,quotient(X,Y)),
	 fix(X)) :- !.
plus(X,add1(Y),
	 if(numberp(Y),
	add1(plus(X,Y)),
	add1(X))).

power_eval(big_plus1(L,I,Base),Base,
	   plus(power_eval(L,Base),I)) :- !.
power_eval(power_rep(I,Base),Base,
	   fix(I)) :- !.
power_eval(big_plus(X,Y,I,Base),Base,
	   plus(I,plus(power_eval(X,Base),
		       power_eval(Y,Base)))) :- !.
power_eval(big_plus(power_rep(I,Base),
		    power_rep(J,Base),
		    zero,
		    Base),
	   Base,
	   plus(I,J)).

quotient(plus(X,plus(X,Y)),2,plus(X,quotient(Y,2))).
quotient(times(Y,X),Y,if(zerop(Y),zero,fix(X))).

remainder(_,         1,zero) :- !.
remainder(X,         X,zero) :- !.
remainder(times(_,Z),Z,zero) :- !.
remainder(times(Y,_),Y,zero).

reverse_loop(X,Y,  append(reverse(X),Y)) :- !.
reverse_loop(X,[], reverse(X)          ).

times(X, plus(Y,Z), plus(times(X,Y),times(X,Z)) ) :- !.
times(times(X,Y),Z, times(X,times(Y,Z)) ) :- !.
times(X,difference(C,W),difference(times(C,X),times(W,X))) :- !.
times(X,add1(Y),if(numberp(Y), plus(X,times(X,Y)), fix(X))).
%
%  nand
%
%  This is a rough approximation to the algorithm presented in:
%
%	"An Algorithm for NAND Decomposition Under Network Constraints,"
%	IEEE Trans. Comp., vol C-18, no. 12, Dec. 1969, p. 1098
%	by E. S. Davidson.
%
%  Written by Bruce Holmer
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  I have used the paper's terminology for names used in the program.
%
%  The data structure for representing functions and variables is
%		function(FunctionNumber, TrueSet, FalseSet,
%			ConceivableInputs,
%			ImmediatePredecessors, ImmediateSuccessors,
%			Predecessors, Successors)
%
%
%  Common names used in the program:
%
%	NumVars		number of variables (signal inputs)
%	NumGs		current number of variables and functions
%	Gs		list of variable and function data
%	Gi,Gj,Gk,Gl	individual variable or function--letter corresponds to
%			the subscript in the paper (most of the time)
%	Vector,V	vector from a function's true set
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

main :- main(0).

main(N) :-
	init_state(N, NumVars, NumGs, Gs),
	add_necessary_functions(NumVars, NumGs, Gs, NumGs2, Gs2),
	test_bounds(NumVars, NumGs2, Gs2),
	search(NumVars, NumGs2, Gs2).
main(_) :-
	write('Search completed'), nl.

%  Test input
%  init_state(circuit(NumInputs, NumOutputs, FunctionList))
init_state(0, 2, 3, [		% 2 input xor
		function(2, [1,2], [0,3], [], [], [], [], []),
		function(1, [2,3], [0,1], [], [], [], [], []),
		function(0, [1,3], [0,2], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(1, 3, 4, [		% carry circuit
		function(3, [3,5,6,7], [0,1,2,4], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(2, 3, 4, [		% example in paper
		function(3, [1,2,4,6,7], [0,3,5], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(3, 3, 4, [		% sum (3 input xor)
		function(3, [1,2,4,7], [0,3,5,6], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(4, 3, 5, [		% do sum and carry together
		function(4, [3,5,6,7], [0,1,2,4], [], [], [], [], []),
		function(3, [1,2,4,7], [0,3,5,6], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(5, 5, 8, [		% 2 bit full adder
		function(7,		% A2 (output)
			[1,3,4,6,9,11,12,14,16,18,21,23,24,26,29,31],
			[0,2,5,7,8,10,13,15,17,19,20,22,25,27,28,30],
			[], [], [], [], []),
		function(6,		% B2 (output)
			[2,3,5,6,8,9,12,15,17,18,20,21,24,27,30,31],
			[0,1,4,7,10,11,13,14,16,19,22,23,25,26,28,29],
			[], [], [], [], []),
		function(5,		% carry-out (output)
			[7,10,11,13,14,15,19,22,23,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,8,9,12,16,17,18,20,21,24],
			[], [], [], [], []),
		function(4,		% carry-in
			[16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15],
			[], [], [], [], []),
		function(3,		% B1 input
			[8,9,10,11,12,13,14,15,24,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,7,16,17,18,19,20,21,22,23],
			[], [], [], [], []),
		function(2,		% B0 input
			[4,5,6,7,12,13,14,15,20,21,22,23,28,29,30,31],
			[0,1,2,3,8,9,10,11,16,17,18,19,24,25,26,27],
			[], [], [], [], []),
		function(1, 		% A1 input
			[2,3,6,7,10,11,14,15,18,19,22,23,26,27,30,31],
			[0,1,4,5,8,9,12,13,16,17,20,21,24,25,28,29],
			[], [], [], [], []),
		function(0,		% A0 input
			[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31],
			[0,2,4,6,8,10,12,14,16,18,20,22,24,26,28,30],
			[], [], [], [], [])
		]) :-
	update_bounds(_, 21, _).


%  Iterate over all the TRUE vectors that need to be covered.
%  If no vectors remain to be covered (select_vector fails), then
%  the circuit is complete (printout results, update bounds, and
%  continue search for a lower cost circuit).
search(NumVars, NumGsIn, GsIn) :-
	select_vector(NumVars, NumGsIn, GsIn, Gj, Vector), !,
	cover_vector(NumVars, NumGsIn, GsIn, Gj, Vector, NumGs, Gs),
	add_necessary_functions(NumVars, NumGs, Gs, NumGsOut, GsOut),
	test_bounds(NumVars, NumGsOut, GsOut),
	search(NumVars, NumGsOut, GsOut).
search(NumVars, NumGs, Gs) :-
	output_results(NumVars, NumGs, Gs),
	update_bounds(NumVars, NumGs, Gs),
	fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Given the current solution, pick the best uncovered TRUE vector
%  for covering next.
%  The selected vector is specified by its vector number and function.
%  Select_vector fails if all TRUE vectors are covered.
%  Select_vector is determinant (gives only one solution).
select_vector(NumVars, NumGs, Gs, Gj, Vector) :-
	select_vector(Gs, NumVars, NumGs, Gs,
		dummy, 0, nf, 999, Gj, Vector, Type, _), !,
	\+ Type = cov,
	\+ Type = nf.

% loop over functions
select_vector([Gk|_], NumVars, _, _, Gj, V, Type, N, Gj, V, Type, N) :-
	function_number(Gk, K),
	K < NumVars.
select_vector([Gk|Gks], NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, GjOut, Vout, TypeOut, Nout) :-
	function_number(Gk, K),
	K >= NumVars,
	true_set(Gk, Tk),
	select_vector(Tk, Gk, NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, Gj, V, Type, N),
	select_vector(Gks, NumVars, NumGs, Gs,
		Gj, V, Type, N, GjOut, Vout, TypeOut, Nout).
	
% loop over vectors
select_vector([], _, _, _, _, Gj, V, Type, N, Gj, V, Type, N).
select_vector([V|Vs], Gk, NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, GjOut, Vout, TypeOut, Nout) :-
	vector_cover_type(NumVars, Gs, Gk, V, Type, N),
	best_vector(GjIn, Vin, TypeIn, Nin,
			Gk, V, Type, N,
			Gj2, V2, Type2, N2),
	select_vector(Vs, Gk, NumVars, NumGs, Gs,
		Gj2, V2, Type2, N2, GjOut, Vout, TypeOut, Nout).

vector_cover_type(NumVars, Gs, Gj, Vector, Type, NumCovers) :-
	immediate_predecessors(Gj, IPs),
	conceivable_inputs(Gj, CIs),
	false_set(Gj, Fj),
	cover_type1(IPs, Gs, Vector, nf, 0, T, N),
	cover_type2(CIs, Gs, NumVars, Fj, Vector, T, N, Type, NumCovers).

cover_type1([], _, _, T, N, T, N).
cover_type1([I|IPs], Gs, V, TypeIn, Nin, TypeOut, Nout) :-
	function(I, Gs, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti), !,
	false_set(Gi, Fi),
	(set_member(V, Fi) ->
		max_type(TypeIn, cov, Type);
		max_type(TypeIn, exp, Type)),
	N is Nin + 1,
	cover_type1(IPs, Gs, V, Type, N, TypeOut, Nout).
cover_type1([_|IPs], Gs, V, TypeIn, Nin, TypeOut, Nout) :-
	cover_type1(IPs, Gs, V, TypeIn, Nin, TypeOut, Nout).

cover_type2([], _, _, _, _, T, N, T, N).
cover_type2([I|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	I < NumVars,
	function(I, Gs, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi), !,
	max_type(TypeIn, var, Type),
	N is Nin + 1,
	cover_type2(CIs, Gs, NumVars, Fj, V, Type, N, TypeOut, Nout).
cover_type2([I|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	I >= NumVars,
	function(I, Gs, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti), !,
	false_set(Gi, Fi),
	(set_member(V, Fi) ->
		(set_subset(Fj, Ti) ->
			max_type(TypeIn, fcn, Type);
			max_type(TypeIn, mcf, Type));
		(set_subset(Fj, Ti) ->
			max_type(TypeIn, exf, Type);
			max_type(TypeIn, exmcf, Type))),
	N is Nin + 1,
	cover_type2(CIs, Gs, NumVars, Fj, V, Type, N, TypeOut, Nout).
cover_type2([_|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	cover_type2(CIs, Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout).

%  The best vector to cover is the one with worst type, or, if types
%  are equal, with the least number of possible covers.
best_vector(dummy, _, _, _, Gj2, V2, Type2, N2, Gj2, V2, Type2, N2) :- !.
best_vector(Gj1, V1, Type1, N1, dummy, _, _, _, Gj1, V1, Type1, N1) :- !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, N2, Gj1, V1, Type, N1) :-
	function_number(Gj1, J), function_number(Gj2, J),
	N1 < N2, !.
best_vector(Gj1, _, Type, N1, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	function_number(Gj1, J), function_number(Gj2, J),
	N1 >= N2, !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, _, Gj1, V1, Type, N1) :-
	(Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 > J2, !.
best_vector(Gj1, _, Type, _, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	(Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 < J2, !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, _, Gj1, V1, Type, N1) :-
	\+ (Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 < J2, !.
best_vector(Gj1, _, Type, _, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	\+ (Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 > J2, !.
best_vector(Gj1, V1, Type1, N1, _, _, Type2, _, Gj1, V1, Type1, N1) :-
	type_order(Type2, Type1), !.
best_vector(_, _, Type1, _, Gj2, V2, Type2, N2, Gj2, V2, Type2, N2) :-
	type_order(Type1, Type2), !.

max_type(T1, T2, T1) :- type_order(T1, T2), !.
max_type(T1, T2, T2) :- \+ type_order(T1, T2), !.

%  Order of types

type_order(cov, exp).
type_order(cov, var).
type_order(cov, fcn).
type_order(cov, mcf).
type_order(cov, exf).
type_order(cov, exmcf).
type_order(cov, nf).
type_order(exp, var).
type_order(exp, fcn).
type_order(exp, mcf).
type_order(exp, exf).
type_order(exp, exmcf).
type_order(exp, nf).
type_order(var, fcn).
type_order(var, mcf).
type_order(var, exf).
type_order(var, exmcf).
type_order(var, nf).
type_order(fcn, mcf).
type_order(fcn, exf).
type_order(fcn, exmcf).
type_order(fcn, nf).
type_order(mcf, exf).
type_order(mcf, exmcf).
type_order(mcf, nf).
type_order(exf, exmcf).
type_order(exf, nf).
type_order(exmcf, nf).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  Cover_vector will cover the specified vector and
%  generate new circuit information.
%  Using backtracking, all possible coverings are generated.
%  The ordering of the possible coverings is approximately that
%  given in Davidson's paper, but has been simplified.

cover_vector(NumVars, NumGsIn, GsIn, Gj, Vector, NumGsOut, GsOut) :-
	immediate_predecessors(Gj, IPs),
	conceivable_inputs(Gj, CIs),
	vector_types(Type),
	cover_vector(Type, IPs, CIs, Gj, Vector, NumVars, NumGsIn, GsIn,
		NumGsOut, GsOut).
	
vector_types(var).
vector_types(exp).
vector_types(fcn).
vector_types(mcf).
vector_types(exf).
vector_types(exmcf).
vector_types(nf).

cover_vector(exp, [I|_], _, Gj, V, _, NumGs, GsIn, NumGs, GsOut) :-
	function(I, GsIn, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exp, [_|IPs], _, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exp, IPs, _, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(var, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I < NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(var, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(var, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(fcn, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	true_set(Gi, Ti),
	false_set(Gj, Fj),
	set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(fcn, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(fcn, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(mcf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	true_set(Gi, Ti),
	false_set(Gj, Fj),
	\+ set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(mcf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(mcf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(exf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	\+ set_member(V, Fi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	false_set(Gj, Fj),
	set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(exmcf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	\+ set_member(V, Fi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	false_set(Gj, Fj),
	\+ set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exmcf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exmcf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(nf, _, _, Gj, V, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	NumGsOut is NumGsIn + 1,
	false_set(Gj, Fj),
	new_function_CIs(GsIn,
		function(NumGsIn,Fj,[V],[],[],[],[],[]),
		NumVars, Gs, Gi),
	update_circuit(Gs, Gi, Gj, V, Gs, GsOut).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

update_circuit([], _, _, _, _, []).
update_circuit([function(K,Tk,Fk,CIk,IPk,ISk,Pk,Sk)|GsIn],
		Gi, Gj, V, Gs,
		[function(K,Tko,Fko,CIko,IPko,ISko,Pko,Sko)|GsOut]) :-
	Gi = function(I,_,Fi,_,IPi,ISi,Pi,_),
	Gj = function(J,_,Fj,_,_,_,_,Sj),
	set_union([I], Pi, PiI),
	set_union([J], Sj, SjJ),
	(K = J ->
		set_union(Tk, Fi, Tk2);
		Tk2 = Tk),
	(K = I ->
		set_union(Tk2, Fj, Tk3);
		Tk3 = Tk2),
	((set_member(K, IPi); set_member(K, ISi)) ->
		set_union(Tk3, [V], Tko);
		Tko = Tk3),
	(K = I ->
		set_union(Fk, [V], Fko);
		Fko = Fk),
	((set_member(K, Pi); K = I) ->
		set_difference(CIk, SjJ, CIk2);
		CIk2 = CIk),
	((set_member(I, CIk), set_member(V, Fk)) ->
		set_difference(CIk2, [I], CIk3);
		CIk3 = CIk2),
	(K = I ->
		exclude_if_vector_in_false_set(CIk3, Gs, V, CIk4);
		CIk4 = CIk3),
	(K = J ->
		set_difference(CIk4, [I], CIko);
		CIko = CIk4),
	(K = J ->
		set_union(IPk, [I], IPko);
		IPko = IPk),
	(K = I ->
		set_union(ISk, [J], ISko);
		ISko = ISk),
	(set_member(K, SjJ) ->
		set_union(Pk, PiI, Pko);
		Pko = Pk),
	(set_member(K, PiI) ->
		set_union(Sk, SjJ, Sko);
		Sko = Sk),
	update_circuit(GsIn, Gi, Gj, V, Gs, GsOut).

exclude_if_vector_in_false_set([], _, _, []).
exclude_if_vector_in_false_set([K|CIsIn], Gs, V, CIsOut) :-
	function(K, Gs, Gk),
	false_set(Gk, Fk),
	set_member(V, Fk), !,
	exclude_if_vector_in_false_set(CIsIn, Gs, V, CIsOut).
exclude_if_vector_in_false_set([K|CIsIn], Gs, V, [K|CIsOut]) :-
	exclude_if_vector_in_false_set(CIsIn, Gs, V, CIsOut).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

add_necessary_functions(NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	add_necessary_functions(NumVars, NumVars, NumGsIn, GsIn,
					NumGsOut, GsOut).

add_necessary_functions(NumGs, _, NumGs, Gs, NumGs, Gs) :- !.
add_necessary_functions(K, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	function(K, GsIn, Gk),
	function_type(NumVars, NumGsIn, GsIn, Gk, nf, V), !,
	false_set(Gk, Fk),
	new_function_CIs(GsIn,
		function(NumGsIn,Fk,[V],[],[],[],[],[]),
		NumVars, Gs, Gl),
	function(K, Gs, Gk1),
	update_circuit(Gs, Gl, Gk1, V, Gs, Gs1),
	NumGs1 is NumGsIn + 1,
	K1 is K + 1,
	add_necessary_functions(K1, NumVars, NumGs1, Gs1, NumGsOut, GsOut).
add_necessary_functions(K, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	K1 is K + 1,
	add_necessary_functions(K1, NumVars, NumGsIn, GsIn, NumGsOut, GsOut).

new_function_CIs(GsIn, function(L,Tl,Fl,_,IPl,ISl,Pl,Sl), NumVars,
		[GlOut|GsOut], GlOut) :-
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, [], CIlo),
	GlOut = function(L,Tl,Fl,CIlo,IPl,ISl,Pl,Sl).
	
new_function_CIs([], _, _, _, [], CIl, CIl).
new_function_CIs([function(K,Tk,Fk,CIk,IPk,ISk,Pk,Sk)|GsIn], L, Fl, NumVars,
		[function(K,Tk,Fk,CIko,IPk,ISk,Pk,Sk)|GsOut], CIlIn, CIlOut) :-
	set_intersection(Fl, Fk, []), !,
	(K >= NumVars ->
		set_union(CIk, [L], CIko);
		CIko = CIk),
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, [K|CIlIn], CIlOut).
new_function_CIs([Gk|GsIn], L, Fl, NumVars, [Gk|GsOut], CIlIn, CIlOut) :-
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, CIlIn, CIlOut).

function_type(NumVars, NumGs, Gs, Gk, Type, Vector) :-
	true_set(Gk, Tk),
	select_vector(Tk, Gk, NumVars, NumGs, Gs,
		dummy, 0, nf, 999, _, Vector, Type, _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Cost and constraint predicates:

% very simple bound for now

test_bounds(_, NumGs, _) :-
	access(bound, Bound),
	NumGs < Bound.

update_bounds(_, NumGs, _) :-
	set(bound, NumGs).

% set and access for systems that don't support them
set(N, A) :-
	(recorded(N, _, Ref) -> erase(Ref) ; true),
	recorda(N, A, _).

access(N, A) :-
	recorded(N, A, _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Output predicates:

%  for now just dump everything

output_results(NumVars, NumGs, Gs) :-
	NumGates is NumGs - NumVars,
	write(NumGates), write(' gates'), nl,
	write_gates(Gs), nl,
	write('searching for a better solution...'), nl, nl.

write_gates([]).
write_gates([Gi|Gs]) :-
	function_number(Gi, I),
	write('gate #'), write(I), write(' inputs:   '),
	immediate_predecessors(Gi, IPi),
	write(IPi), nl,
	write_gates(Gs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  Retrieve the specified function from the function list.
%  function(FunctionNumber, FunctionList, Function).
function(I, [Gi|_], Gi) :- function_number(Gi, I), !.
function(I, [_|Gs], Gi) :- function(I, Gs, Gi).

function_number(        function(I,_,_,_,_,_,_,_), I).
true_set(               function(_,T,_,_,_,_,_,_), T).
false_set(              function(_,_,F,_,_,_,_,_), F).
conceivable_inputs(     function(_,_,_,CI,_,_,_,_), CI).
immediate_predecessors( function(_,_,_,_,IP,_,_,_), IP).
immediate_successors(   function(_,_,_,_,_,IS,_,_), IS).
predecessors(           function(_,_,_,_,_,_,P,_), P).
successors(             function(_,_,_,_,_,_,_,S), S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Set operations assume that the sets are represented by an ordered list
%  of integers.

set_union([],     [],     []).
set_union([],     [X|L2], [X|L2]).
set_union([X|L1], [],     [X|L1]).
set_union([X|L1], [X|L2], [X|L3]) :-        set_union(L1, L2,     L3).
set_union([X|L1], [Y|L2], [X|L3]) :- X < Y, set_union(L1, [Y|L2], L3).
set_union([X|L1], [Y|L2], [Y|L3]) :- X > Y, set_union([X|L1], L2, L3).

set_intersection([],     [],     []).
set_intersection([],     [_|_],  []).
set_intersection([_|_],  [],     []).
set_intersection([X|L1], [X|L2], [X|L3]) :-    set_intersection(L1, L2,     L3).
set_intersection([X|L1], [Y|L2], L3) :- X < Y, set_intersection(L1, [Y|L2], L3).
set_intersection([X|L1], [Y|L2], L3) :- X > Y, set_intersection([X|L1], L2, L3).

set_difference([],     [],     []).
set_difference([],     [_|_],  []).
set_difference([X|L1], [],     [X|L1]).
set_difference([X|L1], [X|L2], L3) :-            set_difference(L1, L2,     L3).
set_difference([X|L1], [Y|L2], [X|L3]) :- X < Y, set_difference(L1, [Y|L2], L3).
set_difference([X|L1], [Y|L2], L3) :-     X > Y, set_difference([X|L1], L2, L3).

set_subset([],     _).
set_subset([X|L1], [X|L2]) :-        set_subset(L1, L2).
set_subset([X|L1], [Y|L2]) :- X > Y, set_subset([X|L1], L2).

set_member(X, [X|_]).
set_member(X, [Y|T]) :- X > Y, set_member(X, T).

%
%  chat
%
%  chat_parser
%
%  Fernando C. N. Pereira and David H. D. Warren

main :- string(X),
	       determinate_say(X,_),
	       fail.
main.

%  query set

string([what,rivers,are,there,?]).
string([does,afghanistan,border,china,?]).
string([what,is,the,capital,of,upper_volta,?]).
string([where,is,the,largest,country,?]).
string([which,country,'`',s,capital,is,london,?]).
string([which,countries,are,european,?]).
string([how,large,is,the,smallest,american,country,?]).
string([what,is,the,ocean,that,borders,african,countries,
	and,that,borders,asian,countries,?]).
string([what,are,the,capitals,of,the,countries,bordering,the,baltic,?]).
string([which,countries,are,bordered,by,two,seas,?]).
string([how,many,countries,does,the,danube,flow,through,?]).
string([what,is,the,total,area,of,countries,south,of,the,equator,
	and,not,in,australasia,?]).
string([what,is,the,average,area,of,the,countries,in,each,continent,?]).
string([is,there,more,than,one,country,in,each,continent,?]).
string([is,there,some,ocean,that,does,not,border,any,country,?]).
string([what,are,the,countries,from,which,a,river,flows,
	into,the,black_sea,?]).

%  determinate_say

determinate_say(X,Y) :- 
   say(X,Y), !.

%-----------------------------------------------------------------------------
%
%  xgrun
%
%-----------------------------------------------------------------------------

terminal(T,S,S,x(_,terminal,T,X),X).
terminal(T,[T|S],S,X,X) :-
   gap(X).

gap(x(gap,_,_,_)).
gap([]).

virtual(NT,x(_,nonterminal,NT,X),X).

%----------------------------------------------------------------------------
%
%  clotab
%
%----------------------------------------------------------------------------

% normal form masks

is_pp(#(1,_,_,_)).

is_pred(#(_,1,_,_)).

is_trace(#(_,_,1,_)).

is_adv(#(_,_,_,1)).

trace(#(_,_,1,_),#(0,0,0,0)).

trace(#(0,0,1,0)).

adv(#(0,0,0,1)).

empty(#(0,0,0,0)).

np_all(#(1,1,1,0)).

s_all(#(1,0,1,1)).

np_no_trace(#(1,1,0,0)).

% mask operations

myplus(#(B1,B2,B3,B4),#(C1,C2,C3,C4),#(D1,D2,D3,D4)) :-
   or(B1,C1,D1),
   or(B2,C2,D2),
   or(B3,C3,D3),
   or(B4,C4,D4).

minus(#(B1,B2,B3,B4),#(C1,C2,C3,C4),#(D1,D2,D3,D4)) :-
   anot(B1,C1,D1),
   anot(B2,C2,D2),
   anot(B3,C3,D3),
   anot(B4,C4,D4).

or(1,_,1).
or(0,1,1).
or(0,0,0).

anot(X,0,X).
anot(X,1,0).

% noun phrase position features

role(subj,_,#(1,0,0)).
role(compl,_,#(0,_,_)).
role(undef,main,#(_,0,_)).
role(undef,aux,#(0,_,_)).
role(undef,decl,_).
role(nil,_,_).

subj_case(#(1,0,0)).
verb_case(#(0,1,0)).
prep_case(#(0,0,1)).
compl_case(#(0,_,_)).

%----------------------------------------------------------------------------
%
%  newg
%
%----------------------------------------------------------------------------

say(X,Y) :-
   sentence(Y,X,[],[],[]).

sentence(B,C,D,E,F) :-
   declarative(B,C,G,E,H),
   terminator(.,G,D,H,F).
sentence(B,C,D,E,F) :-
   wh_question(B,C,G,E,H),
   terminator(?,G,D,H,F).
sentence(B,C,D,E,F) :-
   topic(C,G,E,H),
   wh_question(B,G,I,H,J),
   terminator(?,I,D,J,F).
sentence(B,C,D,E,F) :-
   yn_question(B,C,G,E,H),
   terminator(?,G,D,H,F).
sentence(B,C,D,E,F) :-
   imperative(B,C,G,E,H),
   terminator(!,G,D,H,F).

pp(B,C,D,E,F,F,G,H) :-
   virtual(pp(B,C,D,E),G,H).
pp(pp(B,C),D,E,F,G,H,I,J) :-
   prep(B,G,K,I,L),
   prep_case(M),
   np(C,N,M,O,D,E,F,K,H,L,J).

topic(B,C,D,x(gap,nonterminal,pp(E,compl,F,G),H)) :-
   pp(E,compl,F,G,B,I,D,J),
   opt_comma(I,C,J,H).

opt_comma(B,C,D,E) :-
   `(',',B,C,D,E).
opt_comma(B,B,C,C).

declarative(decl(B),C,D,E,F) :-
   s(B,G,C,D,E,F).

wh_question(whq(B,C),D,E,F,G) :-
   variable_q(B,H,I,J,D,K,F,L),
   question(I,J,C,K,E,L,G).

np(B,C,D,E,F,G,H,I,I,J,K) :-
   virtual(np(B,C,D,E,F,G,H),J,K).
np(np(B,C,[]),B,D,def,E,F,G,H,I,J,K) :-
   is_pp(F),
   pers_pron(C,B,L,H,I,J,K),
   empty(G),
   role(L,decl,D).
np(np(B,C,D),B,E,F,G,H,I,J,K,L,M) :-
   is_pp(H),
   np_head(C,B,F+N,O,D,J,P,L,Q),
   np_all(R),
   np_compls(N,B,G,O,R,I,P,K,Q,M).
np(part(B,C),3+D,E,indef,F,G,H,I,J,K,L) :-
   is_pp(G),
   determiner(B,D,indef,I,M,K,N),
   `(of,M,O,N,P),
   s_all(Q),
   prep_case(R),
   np(C,3+plu,R,def,F,Q,H,O,J,P,L).

variable_q(B,C,D,E,F,G,H,x(gap,nonterminal,np(I,C,E,J,K,L,M),N)) :-
   whq(B,C,I,D,F,G,H,N),
   trace(L,M).
variable_q(B,C,compl,D,E,F,G,x(gap,nonterminal,pp(pp(H,I),compl,J,K),L)) :-
   prep(H,E,M,G,N),
   whq(B,C,I,O,M,F,N,L),
   trace(J,K),
   compl_case(D).
variable_q(B,C,compl,D,E,F,G,x(gap,nonterminal,
	   adv_phrase(pp(H,np(C,np_head(int_det(B),[],I),[])),J,K),L)) :-
   context_pron(H,I,E,F,G,L),
   trace(J,K),
   verb_case(D).
variable_q(B,C,compl,D,E,F,G,
	   x(gap,nonterminal,predicate(adj,value(H,wh(B)),I),J)) :-
   `(how,E,K,G,L),
   adj(quant,H,K,F,L,J),
   empty(I),
   verb_case(D).

adv_phrase(B,C,D,E,E,F,G) :-
   virtual(adv_phrase(B,C,D),F,G).
adv_phrase(pp(B,C),D,E,F,G,H,I) :-
   loc_pred(B,F,J,H,K),
   pp(pp(prep(of),C),compl,D,E,J,G,K,I).

predicate(B,C,D,E,E,F,G) :-
   virtual(predicate(B,C,D),F,G).
predicate(B,C,D,E,F,G,H) :-
   adj_phrase(C,D,E,F,G,H).
predicate(neg,B,C,D,E,F,G) :-
   s_all(H),
   pp(B,compl,H,C,D,E,F,G).
predicate(B,C,D,E,F,G,H) :-
   s_all(I),
   adv_phrase(C,I,D,E,F,G,H).

whq(B,C,D,undef,E,F,G,H) :-
   int_det(B,C,E,I,G,J),
   s_all(K),
   np(D,C,L,M,subj,K,N,I,F,J,H).
whq(B,3+C,np(3+C,wh(B),[]),D,E,F,G,H) :-
   int_pron(D,E,F,G,H).

int_det(B,3+C,D,E,F,G) :-
   whose(B,C,D,E,F,G).
int_det(B,3+C,D,E,F,G) :-
   int_art(B,C,D,E,F,G).

gen_marker(B,B,C,D) :-
   virtual(gen_marker,C,D).
gen_marker(B,C,D,E) :-
   `('`',B,F,D,G),
   an_s(F,C,G,E).

whose(B,C,D,E,F,x(nogap,nonterminal,np_head0(wh(B),C,proper),
	  x(nogap,nonterminal,gen_marker,G))) :-
   `(whose,D,E,F,G).

question(B,C,D,E,F,G,H) :-
   subj_question(B),
   role(subj,I,C),
   s(D,J,E,F,G,H).
question(B,C,D,E,F,G,H) :-
   fronted_verb(B,C,E,I,G,J),
   s(D,K,I,F,J,H).

det(B,C,D,E,E,F,G) :-
   virtual(det(B,C,D),F,G).
det(det(B),C,D,E,F,G,H) :-
   terminal(I,E,F,G,H),
   det(I,C,B,D).
det(generic,B,generic,C,C,D,D).

int_art(B,C,D,E,F,x(nogap,nonterminal,det(G,C,def),H)) :-
   int_art(B,C,G,D,E,F,H).

subj_question(subj).
subj_question(undef).

yn_question(q(B),C,D,E,F) :-
   fronted_verb(nil,G,C,H,E,I),
   s(B,J,H,D,I,F).

verb_form(B,C,D,E,F,F,G,H) :-
   virtual(verb_form(B,C,D,E),G,H).
verb_form(B,C,D,E,F,G,H,I) :-
   terminal(J,F,G,H,I),
   verb_form(J,B,C,D).

neg(B,C,D,D,E,F) :-
   virtual(neg(B,C),E,F).
neg(aux+B,neg,C,D,E,F) :-
   `(not,C,D,E,F).
neg(B,pos,C,C,D,D).

fronted_verb(B,C,D,E,F,x(gap,nonterminal,verb_form(G,H,I,J),
	     x(nogap,nonterminal,neg(K,L),M))) :-
   verb_form(G,H,I,N,D,O,F,P),
   verb_type(G,aux+Q),
   role(B,J,C),
   neg(R,L,O,E,P,M).

imperative(imp(B),C,D,E,F) :-
   imperative_verb(C,G,E,H),
   s(B,I,G,D,H,F).

imperative_verb(B,C,D,x(nogap,terminal,you,x(nogap,nonterminal,
		verb_form(E,imp+fin,2+sin,main),F))) :-
   verb_form(E,inf,G,H,B,C,D,F).

s(s(B,C,D,E),F,G,H,I,J) :-
   subj(B,K,L,G,M,I,N),
   verb(C,K,L,O,M,P,N,Q),
   empty(R),
   s_all(S),
   verb_args(L,O,D,R,T,P,U,Q,V),
   minus(S,T,W),
   myplus(S,T,X),
   verb_mods(E,W,X,F,U,H,V,J).

subj(there,B,C+be,D,E,F,G) :-
   `(there,D,E,F,G).
subj(B,C,D,E,F,G,H) :-
   s_all(I),
   subj_case(J),
   np(B,C,J,K,subj,I,L,E,F,G,H).

np_head(B,C,D,E,F,G,H,I,J) :-
   np_head0(K,L,M,G,N,I,O),
   possessive(K,L,M,P,P,B,C,D,E,F,N,H,O,J).

np_head0(B,C,D,E,E,F,G) :-
   virtual(np_head0(B,C,D),F,G).
np_head0(name(B),3+sin,def+proper,C,D,E,F) :-
   name(B,C,D,E,F).
np_head0(np_head(B,C,D),3+E,F+common,G,H,I,J) :-
   determiner(B,E,F,G,K,I,L),
   adjs(C,K,M,L,N),
   noun(D,E,M,H,N,J).
np_head0(B,C,def+proper,D,E,F,x(nogap,nonterminal,gen_marker,G)) :-
   poss_pron(B,C,D,E,F,G).
np_head0(np_head(B,[],C),3+sin,indef+common,D,E,F,G) :-
   quantifier_pron(B,C,D,E,F,G).

np_compls(proper,B,C,[],D,E,F,F,G,G) :-
   empty(E).
np_compls(common,B,C,D,E,F,G,H,I,J) :-
   np_all(K),
   np_mods(B,C,L,D,E,M,K,N,G,O,I,P),
   relative(B,L,M,N,F,O,H,P,J).

possessive(B,C,D,[],E,F,G,H,I,J,K,L,M,N) :-
   gen_case(K,O,M,P),
   np_head0(Q,R,S,O,T,P,U),
   possessive(Q,R,S,V,[pp(poss,np(C,B,E))|V],F,G,H,I,J,T,L,U,N).
possessive(B,C,D,E,F,B,C,D,E,F,G,G,H,H).

gen_case(B,C,D,x(nogap,terminal,the,E)) :-
   gen_marker(B,C,D,E).

an_s(B,C,D,E) :-
   `(s,B,C,D,E).
an_s(B,B,C,C).

determiner(B,C,D,E,F,G,H) :-
   det(B,C,D,E,F,G,H).
determiner(B,C,D,E,F,G,H) :-
   quant_phrase(B,C,D,E,F,G,H).

quant_phrase(quant(B,C),D,E,F,G,H,I) :-
   quant(B,E,F,J,H,K),
   number(C,D,J,G,K,I).

quant(B,indef,C,D,E,F) :-
   neg_adv(G,B,C,H,E,I),
   comp_adv(G,H,J,I,K),
   `(than,J,D,K,F).
quant(B,indef,C,D,E,F) :-
   `(at,C,G,E,H),
   sup_adv(I,G,D,H,F),
   sup_op(I,B).
quant(the,def,B,C,D,E) :-
   `(the,B,C,D,E).
quant(same,indef,B,B,C,C).

neg_adv(B,not+B,C,D,E,F) :-
   `(not,C,D,E,F).
neg_adv(B,B,C,C,D,D).

sup_op(least,not+less).
sup_op(most,not+more).

np_mods(B,C,D,[E|F],G,H,I,J,K,L,M,N) :-
   np_mod(B,C,E,G,O,K,P,M,Q),
   trace(R),
   myplus(R,O,S),
   minus(G,S,T),
   myplus(O,G,U),
   np_mods(B,C,D,F,T,H,U,J,P,L,Q,N).
np_mods(B,C,D,D,E,E,F,F,G,G,H,H).

np_mod(B,C,D,E,F,G,H,I,J) :-
   pp(D,C,E,F,G,H,I,J).
np_mod(B,C,D,E,F,G,H,I,J) :-
   reduced_relative(B,D,E,F,G,H,I,J).

verb_mods([B|C],D,E,F,G,H,I,J) :-
   verb_mod(B,D,K,G,L,I,M),
   trace(N),
   myplus(N,K,O),
   minus(D,O,P),
   myplus(K,D,Q),
   verb_mods(C,P,Q,F,L,H,M,J).
verb_mods([],B,C,C,D,D,E,E).

verb_mod(B,C,D,E,F,G,H) :-
   adv_phrase(B,C,D,E,F,G,H).
verb_mod(B,C,D,E,F,G,H) :-
   is_adv(C),
   adverb(B,E,F,G,H),
   empty(D).
verb_mod(B,C,D,E,F,G,H) :-
   pp(B,compl,C,D,E,F,G,H).

adjs([B|C],D,E,F,G) :-
   pre_adj(B,D,H,F,I),
   adjs(C,H,E,I,G).
adjs([],B,B,C,C).

pre_adj(B,C,D,E,F) :-
   adj(G,B,C,D,E,F).
pre_adj(B,C,D,E,F) :-
   sup_phrase(B,C,D,E,F).

sup_phrase(sup(most,B),C,D,E,F) :-
   sup_adj(B,C,D,E,F).
sup_phrase(sup(B,C),D,E,F,G) :-
   sup_adv(B,D,I,F,J),
   adj(quant,C,I,E,J,G).

comp_phrase(comp(B,C,D),E,F,G,H,I) :-
   comp(B,C,F,J,H,K),
   np_no_trace(L),
   prep_case(M),
   np(D,N,M,O,compl,L,E,J,G,K,I).

comp(B,C,D,E,F,G) :-
   comp_adv(B,D,H,F,I),
   adj(quant,C,H,J,I,K),
   `(than,J,E,K,G).
comp(more,B,C,D,E,F) :-
   rel_adj(B,C,G,E,H),
   `(than,G,D,H,F).
comp(same,B,C,D,E,F) :-
   `(as,C,G,E,H),
   adj(quant,B,G,I,H,J),
   `(as,I,D,J,F).

relative(B,[C],D,E,F,G,H,I,J) :-
   is_pred(D),
   rel_conj(B,K,C,F,G,H,I,J).
relative(B,[],C,D,D,E,E,F,F).

rel_conj(B,C,D,E,F,G,H,I) :-
   rel(B,J,K,F,L,H,M),
   rel_rest(B,C,J,D,K,E,L,G,M,I).

rel_rest(B,C,D,E,F,G,H,I,J,K) :-
   conj(C,L,D,M,E,H,N,J,O),
   rel_conj(B,L,M,G,N,I,O,K).
rel_rest(B,C,D,D,E,E,F,F,G,G).

rel(B,rel(C,D),E,F,G,H,I) :-
   open(F,J,H,K),
   variable(B,C,J,L,K,M),
   s(D,N,L,O,M,P),
   trace(Q),
   minus(N,Q,E),
   close(O,G,P,I).

variable(B,C,D,E,F,x(gap,nonterminal,np(np(B,wh(C),[]),B,G,H,I,J,K),L)) :-
   `(that,D,E,F,L),
   trace(J,K).
variable(B,C,D,E,F,x(gap,nonterminal,np(G,H,I,J,K,L,M),N)) :-
   wh(C,B,G,H,I,D,E,F,N),
   trace(L,M).
variable(B,C,D,E,F,x(gap,nonterminal,pp(pp(G,H),compl,I,J),K)) :-
   prep(G,D,L,F,M),
   wh(C,B,H,N,O,L,E,M,K),
   trace(I,J),
   compl_case(O).

wh(B,C,np(C,wh(B),[]),C,D,E,F,G,H) :-
   rel_pron(I,E,F,G,H),
   role(I,decl,D).
wh(B,C,np(D,E,[pp(F,G)]),D,H,I,J,K,L) :-
   np_head0(E,D,M+common,I,N,K,O),
   prep(F,N,P,O,Q),
   wh(B,C,G,R,S,P,J,Q,L).
wh(B,C,D,E,F,G,H,I,J) :-
   whose(B,C,G,K,I,L),
   s_all(M),
   np(D,E,F,def,subj,M,N,K,H,L,J).

reduced_relative(B,C,D,E,F,G,H,I) :-
   is_pred(D),
   reduced_rel_conj(B,J,C,E,F,G,H,I).

reduced_rel_conj(B,C,D,E,F,G,H,I) :-
   reduced_rel(B,J,K,F,L,H,M),
   reduced_rel_rest(B,C,J,D,K,E,L,G,M,I).

reduced_rel_rest(B,C,D,E,F,G,H,I,J,K) :-
   conj(C,L,D,M,E,H,N,J,O),
   reduced_rel_conj(B,L,M,G,N,I,O,K).
reduced_rel_rest(B,C,D,D,E,E,F,F,G,G).

reduced_rel(B,reduced_rel(C,D),E,F,G,H,I) :-
   open(F,J,H,K),
   reduced_wh(B,C,J,L,K,M),
   s(D,N,L,O,M,P),
   trace(Q),
   minus(N,Q,E),
   close(O,G,P,I).

reduced_wh(B,C,D,E,F,x(nogap,nonterminal,
	   np(np(B,wh(C),[]),B,G,H,I,J,K),x(nogap,nonterminal,
	   verb_form(be,pres+fin,B,main),x(nogap,nonterminal,
	   neg(L,M),x(nogap,nonterminal,predicate(M,N,O),P))))) :-
   neg(Q,M,D,R,F,S),
   predicate(M,N,O,R,E,S,P),
   trace(J,K),
   subj_case(G).
reduced_wh(B,C,D,E,F,x(nogap,nonterminal,
	   np(np(B,wh(C),[]),B,G,H,I,J,K),x(nogap,nonterminal,
	   verb(L,M,N,O),P))) :-
   participle(L,N,O,D,E,F,P),
   trace(J,K),
   subj_case(G).
reduced_wh(B,C,D,E,F,x(nogap,nonterminal,
	   np(G,H,I,J,K,L,M),x(gap,nonterminal,
	   np(np(B,wh(C),[]),B,N,O,P,Q,R),S))) :-
   s_all(T),
   subj_case(I),
   verb_case(N),
   np(G,H,U,J,subj,T,V,D,E,F,S),
   trace(L,M),
   trace(Q,R).

verb(B,C,D,E,F,F,G,H) :-
   virtual(verb(B,C,D,E),G,H).
verb(verb(B,C,D+fin,E,F),G,H,C,I,J,K,L) :-
   verb_form(M,D+fin,G,N,I,O,K,P),
   verb_type(M,Q),
   neg(Q,F,O,R,P,S),
   rest_verb(N,M,B,C,E,R,J,S,L),
   verb_type(B,H).

rest_verb(aux,have,B,C,[perf|D],E,F,G,H) :-
   verb_form(I,past+part,J,K,E,L,G,M),
   have(I,B,C,D,L,F,M,H).
rest_verb(aux,be,B,C,D,E,F,G,H) :-
   verb_form(I,J,K,L,E,M,G,N),
   be(J,I,B,C,D,M,F,N,H).
rest_verb(aux,do,B,active,[],C,D,E,F) :-
   verb_form(B,inf,G,H,C,D,E,F).
rest_verb(main,B,B,active,[],C,C,D,D).

have(be,B,C,D,E,F,G,H) :-
   verb_form(I,J,K,L,E,M,G,N),
   be(J,I,B,C,D,M,F,N,H).
have(B,B,active,[],C,C,D,D).

be(past+part,B,B,passive,[],C,C,D,D).
be(pres+part,B,C,D,[prog],E,F,G,H) :-
   passive(B,C,D,E,F,G,H).

passive(be,B,passive,C,D,E,F) :-
   verb_form(B,past+part,G,H,C,D,E,F),
   verb_type(B,I),
   passive(I).
passive(B,B,active,C,C,D,D).

participle(verb(B,C,inf,D,E),F,C,G,H,I,J) :-
   neg(K,E,G,L,I,M),
   verb_form(B,N,O,P,L,H,M,J),
   participle(N,C,D),
   verb_type(B,F).

passive(B+trans).
passive(B+ditrans).

participle(pres+part,active,[prog]).
participle(past+part,passive,[]).

close(B,B,C,D) :-
   virtual(close,C,D).

open(B,B,C,x(gap,nonterminal,close,C)).

verb_args(B+C,D,E,F,G,H,I,J,K) :-
   advs(E,L,M,H,N,J,O),
   verb_args(C,D,L,F,G,N,I,O,K).
verb_args(trans,active,[arg(dir,B)],C,D,E,F,G,H) :-
   verb_arg(np,B,D,E,F,G,H).
verb_args(ditrans,B,[arg(C,D)|E],F,G,H,I,J,K) :-
   verb_arg(np,D,L,H,M,J,N),
   object(C,E,L,G,M,I,N,K).
verb_args(be,B,[void],C,C,D,E,F,G) :-
   terminal(there,D,E,F,G).
verb_args(be,B,[arg(predicate,C)],D,E,F,G,H,I) :-
   pred_conj(J,C,E,F,G,H,I).
verb_args(be,B,[arg(dir,C)],D,E,F,G,H,I) :-
   verb_arg(np,C,E,F,G,H,I).
verb_args(have,active,[arg(dir,B)],C,D,E,F,G,H) :-
   verb_arg(np,B,D,E,F,G,H).
verb_args(B,C,[],D,D,E,E,F,F) :-
   no_args(B).

object(B,C,D,E,F,G,H,I) :-
   adv(J),
   minus(J,D,K),
   advs(C,L,K,F,M,H,N),
   obj(B,L,D,E,M,G,N,I).

obj(ind,[arg(dir,B)],C,D,E,F,G,H) :-
   verb_arg(np,B,D,E,F,G,H).
obj(dir,[],B,B,C,C,D,D).

pred_conj(B,C,D,E,F,G,H) :-
   predicate(I,J,K,E,L,G,M),
   pred_rest(B,J,C,K,D,L,F,M,H).

pred_rest(B,C,D,E,F,G,H,I,J) :-
   conj(B,K,C,L,D,G,M,I,N),
   pred_conj(K,L,F,M,H,N,J).
pred_rest(B,C,C,D,D,E,E,F,F).

verb_arg(np,B,C,D,E,F,G) :-
   s_all(H),
   verb_case(I),
   np(B,J,I,K,compl,H,C,D,E,F,G).

advs([B|C],D,E,F,G,H,I) :-
   is_adv(E),
   adverb(B,F,J,H,K),
   advs(C,D,E,J,G,K,I).
advs(B,B,C,D,D,E,E).

adj_phrase(B,C,D,E,F,G) :-
   adj(H,B,D,E,F,G),
   empty(C).
adj_phrase(B,C,D,E,F,G) :-
   comp_phrase(B,C,D,E,F,G).

no_args(trans).
no_args(ditrans).
no_args(intrans).

conj(conj(B,C),conj(B,D),E,F,conj(B,E,F),G,H,I,J) :-
   conj(B,C,D,G,H,I,J).

noun(B,C,D,E,F,G) :-
   terminal(H,D,E,F,G),
   noun_form(H,B,C).

adj(B,adj(C),D,E,F,G) :-
   terminal(C,D,E,F,G),
   adj(C,B).

prep(prep(B),C,D,E,F) :-
   terminal(B,C,D,E,F),
   prep(B).

rel_adj(adj(B),C,D,E,F) :-
   terminal(G,C,D,E,F),
   rel_adj(G,B).

sup_adj(adj(B),C,D,E,F) :-
   terminal(G,C,D,E,F),
   sup_adj(G,B).

comp_adv(less,B,C,D,E) :-
   `(less,B,C,D,E).
comp_adv(more,B,C,D,E) :-
   `(more,B,C,D,E).

sup_adv(least,B,C,D,E) :-
   `(least,B,C,D,E).
sup_adv(most,B,C,D,E) :-
   `(most,B,C,D,E).

rel_pron(B,C,D,E,F) :-
   terminal(G,C,D,E,F),
   rel_pron(G,B).

name(B,C,D,E,F) :-
   opt_the(C,G,E,H),
   terminal(B,G,D,H,F),
   name(B).

int_art(B,plu,quant(same,wh(B)),C,D,E,F) :-
   `(how,C,G,E,H),
   `(many,G,D,H,F).
int_art(B,C,D,E,F,G,H) :-
   terminal(I,E,F,G,H),
   int_art(I,B,C,D).

int_pron(B,C,D,E,F) :-
   terminal(G,C,D,E,F),
   int_pron(G,B).

adverb(adv(B),C,D,E,F) :-
   terminal(B,C,D,E,F),
   adverb(B).

poss_pron(pronoun(B),C+D,E,F,G,H) :-
   terminal(I,E,F,G,H),
   poss_pron(I,B,C,D).

pers_pron(pronoun(B),C+D,E,F,G,H,I) :-
   terminal(J,F,G,H,I),
   pers_pron(J,B,C,D,E).

quantifier_pron(B,C,D,E,F,G) :-
   terminal(H,D,E,F,G),
   quantifier_pron(H,B,C).

context_pron(prep(in),place,B,C,D,E) :-
   `(where,B,C,D,E).
context_pron(prep(at),time,B,C,D,E) :-
   `(when,B,C,D,E).

number(nb(B),C,D,E,F,G) :-
   terminal(H,D,E,F,G),
   number(H,B,C).

terminator(B,C,D,E,F) :-
   terminal(G,C,D,E,F),
   terminator(G,B).

opt_the(B,B,C,C).
opt_the(B,C,D,E) :-
   `(the,B,C,D,E).

conj(B,list,list,C,D,E,F) :-
   terminal(',',C,D,E,F).
conj(B,list,'end',C,D,E,F) :-
   terminal(B,C,D,E,F),
   conj(B).

loc_pred(B,C,D,E,F) :-
   terminal(G,C,D,E,F),
   loc_pred(G,B).

`(B,C,D,E,F) :-
   terminal(B,C,D,E,F),
   `(B).

%----------------------------------------------------------------------------
%
%  newdic
%
%----------------------------------------------------------------------------

word(Word) :- `(Word).
word(Word) :- conj(Word).
word(Word) :- adverb(Word).
word(Word) :- sup_adj(Word,_).
word(Word) :- rel_adj(Word,_).
word(Word) :- adj(Word,_).
word(Word) :- name(Word).
word(Word) :- terminator(Word,_).
word(Word) :- pers_pron(Word,_,_,_,_).
word(Word) :- poss_pron(Word,_,_,_).
word(Word) :- rel_pron(Word,_).
word(Word) :- verb_form(Word,_,_,_).
word(Word) :- noun_form(Word,_,_).
word(Word) :- prep(Word).
word(Word) :- quantifier_pron(Word,_,_).
word(Word) :- number(Word,_,_).
word(Word) :- det(Word,_,_,_).
word(Word) :- int_art(Word,_,_,_).
word(Word) :- int_pron(Word,_).
word(Word) :- loc_pred(Word,_).

`(how).
`(whose).
`(there).
`(of).
`('`').		% use ` instead of ' to help assembler
`(',').	
`(s).
`(than).
`(at).
`(the).
`(not).
`(as).
`(that).
`(less).
`(more).
`(least).
`(most).
`(many).
`(where).
`(when).

conj(and).
conj(or).

int_pron(what,undef).
int_pron(which,undef).
int_pron(who,subj).
int_pron(whom,compl).

int_art(what,X,_,int_det(X)).
int_art(which,X,_,int_det(X)).

det(the,No,the(No),def).
det(a,sin,a,indef).
det(an,sin,a,indef).
det(every,sin,every,indef).
det(some,_,some,indef).
det(any,_,any,indef).
det(all,plu,all,indef).
det(each,sin,each,indef).
det(no,_,no,indef).

number(W,I,Nb) :-
   tr_number(W,I),
   ag_number(I,Nb).

tr_number(nb(I),I).
tr_number(one,1).
tr_number(two,2).
tr_number(three,3).
tr_number(four,4).
tr_number(five,5).
tr_number(six,6).
tr_number(seven,7).
tr_number(eight,8).
tr_number(nine,9).
tr_number(ten,10).

ag_number(1,sin).
ag_number(N,plu) :- N>1.

quantifier_pron(everybody,every,person).
quantifier_pron(everyone,every,person).
quantifier_pron(everything,every,thing).
quantifier_pron(somebody,some,person).
quantifier_pron(someone,some,person).
quantifier_pron(something,some,thing).
quantifier_pron(anybody,any,person).
quantifier_pron(anyone,any,person).
quantifier_pron(anything,any,thing).
quantifier_pron(nobody,no,person).
quantifier_pron(nothing,no,thing).

prep(as).
prep(at).
prep(of).
prep(to).
prep(by).
prep(with).
prep(in).
prep(on).
prep(from).
prep(into).
prep(through).

noun_form(Plu,Sin,plu) :- noun_plu(Plu,Sin).
noun_form(Sin,Sin,sin) :- noun_sin(Sin).
noun_form(proportion,proportion,_).
noun_form(percentage,percentage,_).

root_form(1+sin).
root_form(2+_).
root_form(1+plu).
root_form(3+plu).

verb_root(be).
verb_root(have).
verb_root(do).
verb_root(border).
verb_root(contain).
verb_root(drain).
verb_root(exceed).
verb_root(flow).
verb_root(rise).

regular_pres(have).
regular_pres(do).
regular_pres(rise).
regular_pres(border).
regular_pres(contain).
regular_pres(drain).
regular_pres(exceed).
regular_pres(flow).

regular_past(had,have).
regular_past(bordered,border).
regular_past(contained,contain).
regular_past(drained,drain).
regular_past(exceeded,exceed).
regular_past(flowed,flow).

rel_pron(who,subj).
rel_pron(whom,compl).
rel_pron(which,undef).

poss_pron(my,_,1,sin).
poss_pron(your,_,2,_).
poss_pron(his,masc,3,sin).
poss_pron(her,fem,3,sin).
poss_pron(its,neut,3,sin).
poss_pron(our,_,1,plu).
poss_pron(their,_,3,plu).

pers_pron(i,_,1,sin,subj).
pers_pron(you,_,2,_,_).
pers_pron(he,masc,3,sin,subj).
pers_pron(she,fem,3,sin,subj).
pers_pron(it,neut,3,sin,_).
pers_pron(we,_,1,plu,subj).
pers_pron(them,_,3,plu,subj).
pers_pron(me,_,1,sin,compl(_)).
pers_pron(him,masc,3,sin,compl(_)).
pers_pron(her,fem,3,sin,compl(_)).
pers_pron(us,_,1,plu,compl(_)).
pers_pron(them,_,3,plu,compl(_)).

terminator(.,_).
terminator(?,?).
terminator(!,!).

name(_).

% ===============================

% specialised dictionary

loc_pred(east,prep(eastof)).
loc_pred(west,prep(westof)).
loc_pred(north,prep(northof)).
loc_pred(south,prep(southof)).

adj(minimum,restr).
adj(maximum,restr).
adj(average,restr).
adj(total,restr).
adj(african,restr).
adj(american,restr).
adj(asian,restr).
adj(european,restr).
adj(great,quant).
adj(big,quant).
adj(small,quant).
adj(large,quant).
adj(old,quant).
adj(new,quant).
adj(populous,quant).

rel_adj(greater,great).
rel_adj(less,small).
rel_adj(bigger,big).
rel_adj(smaller,small).
rel_adj(larger,large).
rel_adj(older,old).
rel_adj(newer,new).

sup_adj(biggest,big).
sup_adj(smallest,small).
sup_adj(largest,large).
sup_adj(oldest,old).
sup_adj(newest,new).

noun_sin(average).
noun_sin(total).
noun_sin(sum).
noun_sin(degree).
noun_sin(sqmile).
noun_sin(ksqmile).
noun_sin(thousand).
noun_sin(million).
noun_sin(time).
noun_sin(place).
noun_sin(area).
noun_sin(capital).
noun_sin(city).
noun_sin(continent).
noun_sin(country).
noun_sin(latitude).
noun_sin(longitude).
noun_sin(ocean).
noun_sin(person).
noun_sin(population).
noun_sin(region).
noun_sin(river).
noun_sin(sea).
noun_sin(seamass).
noun_sin(number).

noun_plu(averages,average).
noun_plu(totals,total).
noun_plu(sums,sum).
noun_plu(degrees,degree).
noun_plu(sqmiles,sqmile).
noun_plu(ksqmiles,ksqmile).
noun_plu(million,million).
noun_plu(thousand,thousand).
noun_plu(times,time).
noun_plu(places,place).
noun_plu(areas,area).
noun_plu(capitals,capital).
noun_plu(cities,city).
noun_plu(continents,continent).
noun_plu(countries,country).
noun_plu(latitudes,latitude).
noun_plu(longitudes,longitude).
noun_plu(oceans,ocean).
noun_plu(persons,person).  noun_plu(people,person).
noun_plu(populations,population).
noun_plu(regions,region).
noun_plu(rivers,river).
noun_plu(seas,sea).
noun_plu(seamasses,seamass).
noun_plu(numbers,number).

verb_form(V,V,inf,_) :- verb_root(V).
verb_form(V,V,pres+fin,Agmt) :-
   regular_pres(V),
   root_form(Agmt),
   verb_root(V).
verb_form(Past,Root,past+_,_) :-
   regular_past(Past,Root).

verb_form(am,be,pres+fin,1+sin).
verb_form(are,be,pres+fin,2+sin).
verb_form(is,be,pres+fin,3+sin).
verb_form(are,be,pres+fin,_+plu).
verb_form(was,be,past+fin,1+sin).
verb_form(were,be,past+fin,2+sin).
verb_form(was,be,past+fin,3+sin).
verb_form(were,be,past+fin,_+plu).
verb_form(been,be,past+part,_).
verb_form(being,be,pres+part,_).
verb_form(has,have,pres+fin,3+sin).
verb_form(having,have,pres+part,_).
verb_form(does,do,pres+fin,3+sin).
verb_form(did,do,past+fin,_).
verb_form(doing,do,pres+part,_).
verb_form(done,do,past+part,_).
verb_form(flows,flow,pres+fin,3+sin).
verb_form(flowing,flow,pres+part,_).
verb_form(rises,rise,pres+fin,3+sin).
verb_form(rose,rise,past+fin,_).
verb_form(risen,rise,past+part,_).
verb_form(borders,border,pres+fin,3+sin).
verb_form(bordering,border,pres+part,_).
verb_form(contains,contain,pres+fin,3+sin).
verb_form(containing,contain,pres+part,_).
verb_form(drains,drain,pres+fin,3+sin).
verb_form(draining,drain,pres+part,_).
verb_form(exceeds,exceed,pres+fin,3+sin).
verb_form(exceeding,exceed,pres+part,_).

verb_type(have,aux+have).
verb_type(be,aux+be).
verb_type(do,aux+ditrans).
verb_type(rise,main+intrans).
verb_type(border,main+trans).
verb_type(contain,main+trans).
verb_type(drain,main+intrans).
verb_type(exceed,main+trans).
verb_type(flow,main+intrans).

adverb(yesterday).
adverb(tomorrow).
