/*----------------------------------------------------------------
	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);

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

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

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

show_ideal():=expand(gideal);

/* Generate a point with coords [xi,yi] */
genpoint():=block([i:gindex],gindex:gindex+1,[concat('x,i),concat('y,i)]);
genangle():=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);

/*------------------------------- Lisp Output --------------------------------*/ 

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

/* Output a list as Lisp */
lispl(l):=apply(concat,append(["("],makelist(concat(" ",e," "),e,l),[")"]));

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

consider_angles([L]):=map(lambda([A],
	A::genangle(),gangles:append(gangles,eval(A),L);

arbitrary_points([L]):=map(lambda([P],gparams:append(gparams,eval(P))),L);
arbitrary_angles([L]):=map(lambda([P],gparams:endcons(gparams,eval(P))),L);
/*--------------- Geometric Declarations -----------------------------------*/
/* X, Y, Z on the plane are colinear */
are_collinear(X,Y,Z):=
	(geqns:endcons(det(matrix(cons(1,X),cons(1,Y),cons(1,Z))),geqns));

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

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

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

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

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

/* Angles ABC and DEF are equal */
/* equal_angles(A,B,C,D,E,F):=(geqns:endcons(geqns,*/