/*----------------------------------------------------------------
	Basic function for construction of equations 
	in Geometric Theorem proving 
----------------------------------------------------------------*/
put('geometry,1,'version);

define_variable(geqns,[],any);
define_variable(hypotheses,[],any);
define_variable(conclusions,[],any);
define_variable(gvars,[],any);
define_variable(gparams,[],any);
define_variable(gindex,1,any);
define_variable(gparindex,1,any);
define_variable(gideal,FALSE,any);

ginit():=(geqns:hypotheses:conclusions:gvars:gparams:[],
	gindex:gparindex:1);
ghypot():=(hypotheses:geqns,geqns:[]);

gconcl():=(conclusions:geqns,geqns:[]);

gideal():= (gideal:append(hypotheses,
	makelist(1-genpar()*conclusions[i],i,1,length(conclusions))));

showideal():=expand(gideal);

gstringout(file):=block([val:ev(string(showideal()),grind=true)],
stringout(file,concat("(string-grobner-system \"",
val,"\" '",
lispl(gvars),
" '",lispl(gparams),")")));

lispl(l):=apply(concat,append(["("],makelist(concat(" ",e," "),e,l),[")"]));

gpoints([L]):=map(lambda([P],
	P::genpoint(),gvars:append(gvars,eval(P))),L);

garbitrary([L]):=map(lambda([P],gparams:append(gparams,eval(P))),L);

/* X, Y, Z on the plane are colinear */
collinear(X,Y,Z):=
	(geqns:endcons(det(matrix(cons(1,X),cons(1,Y),cons(1,Z))),geqns));

/* Vector AB and CD are perpendicular */
perp(A,B,C,D):= (geqns:endcons((B-A).(D-C),geqns));

/* AB and CD have equal length */
eqlen(A,B,C,D):=(geqns:endcons((B-A).(B-A)-(D-C).(D-C),geqns));

/* AB and CD are parallel */
parallel(A,B,C,D):=(geqns:endcons(geqns,det(matrix(B-A,D-C))));

/* M is the midpoint of AB; 2 equations */
midpoint(M,A,B):=(geqns:append(geqns,2*M-(A+B)));

/* Points A and B are identical */
identical(A,B):=(geqns:append(geqns,A-B));

/* Generate a point with coords [xi,yi] */
genpoint():=block([i:gindex],gindex:gindex+1,[concat('x,i),concat('y,i)]);

/* Generate a parameter ui */
genpar():=block([i:gparindex,sym:concat('u,i)],
	gvars:endcons(sym,gvars),gparindex:gparindex+1,sym);