/*
%	FILE: ot.pro
%	SYNOPSIS: Construct Ordinal Trees from Equations,
%	AUTHOR: Mohsin Ahmed,	22-sept-91
%	GPL(C) Mohsin Ahmed, http://www.cs.albany.edu/~mosh
%
% Notes:
%	Variables are i(in),o(out), io(in and out ).
%	Syntax of terms used below:
%		ot_eqn		::= ot_eqn(ot_name,node_name,node_value).
%		ot_eqn_list	::= [ node_name = node_value , .. ]
%		node_list	::= [ node_name , .. , node_name ]
%		node_value	::= proposition |
%				::= split( node_value, node_value )
%		node_name	::= n( term )
%		string		::= interval
%		interval	::= [ interval , .. , interval ]
%				::= [ interval ^ omega ^ integer ]
%				::= [ interval ^ omega ]
%				::= proposition
%		propostion	::= p( term )
%		omega		::= w
*/

/*----------------------------------------------------------------
%	exponent operator ^ is right associative.
----------------------------------------------------------------*/
?- op(10, xfy, ^).
/*----------------------------------------------------------------
%	ot( VA:i, FN:i, CN:i, NV:i, OTN:i, SN:o, LN:o, STR:o ).
%	ot(	Visitable_Ancestors	: node_list,
%		Forbidden_Nodes		: node_list,
%		Current_Node		: node_name,
%		Current_Node_Value	: node_value,
%		Ot_Name			: term,
%		Sub_Nodes		: node_list,
%		Loop_Node		: node_list,
%		String			: string     ).
%	Traverses an ordinal tree, given by equations,
%	and succeeds if the tree is legal
%	and also returns the string representation of the tree.
----------------------------------------------------------------*/
/*	top call to examine ot equations			*/
ot( Root, Ot_name, Sub_nodes, String ):-
	ot_equation( Ot_name, Root, Value ),
	ot( [], [], Root, Value, Ot_name, Sub_nodes, [], String ).

/*	node pointing to forbidden ancestor/sibling		*/
ot( _, FN, n(X), _, _, _, _, _ ) :-
	member( n(X), FN ),
	write('Invalid arc, to node : '), write( n(X) ), nl, !, fail.

/*	loop node pointing back					*/
ot( VA, _, n(X), _, _, [], [n(X)], [] ):- member( n(X), VA ), !.

/*	leaf node						*/
ot( _, _, n(X), p(P), _, [], [], [p(P)] ):- !.

/*	find ot of Y and Z, and return the combined result	*/
ot( VA_X, FN_X, n(X), split(n(Y),n(Z)), OTN,
	[n(Y),n(Z)|SN_YZ] , LN_X, ST_X ) :-
	!,
	/*	ot of Y */
	union( FN_X, VA_X, FN_Y ),
	ot_equation( OTN, n(Y), V_Y ),
	ot( [] , [n(X)|FN_Y] , n(Y), V_Y, OTN, SN_Y, [] , ST_Y ),
	/*	ot of Z */
	union( FN_X, SN_Y, FN_Z ),
	ot_equation( OTN, n(Z), V_Z ),
	ot( [n(X)|VA_X], FN_Z, n(Z), V_Z, OTN, SN_Z, LN_Z, ST_Z ),
	union( ST_Y, ST_Z, ST_YZ ),
	omega_check( n(X), LN_Z, LN_X, ST_YZ, ST_X ),
	union( SN_Y, SN_Z, SN_YZ ), ! .

ot( _, _, CN, NV, OTN, _, _, _ ):-
	write('ot:error in '), write( OTN ), write(' : '),
	write( CN ), write(' = '), write( NV ), nl, fail.
/*----------------------------------------------------------------
%	omega_check(	CN:i, LNi:i, LNo:o, STi:i, STo:o )
%	omega_check(	Current_node	: node_name,
%			Loop_node_in	: node_list,
%			Loop_node_out	: node_list,
%			String_in	: string,
%			String_out	: string 	)
%	check if a lower node is pointing to current node
%	if yes, raise the string to the power of omega.
----------------------------------------------------------------*/
omega_check( n(X), [n(X)], [], [ST^w], [ST^w^2] ):- !.
omega_check( n(X), [n(X)], [], [ST^w^N], [ST^w^M] ):- M is N + 1, !.
omega_check( n(X), [n(X)], [], ST, [ST^w] ):- !.
omega_check( _, LN, LN, ST, ST ).
/*----------------------------------------------------------------
%	ot_equation( Ot_name:i, Node:i, Node_Value:o ) :-
%	Just returns the value of Node in any given tree,
%	gives error message if node is undefined.
----------------------------------------------------------------*/
ot_equation( Ot_name, Node, Value ) :- ot_eqn( Ot_name, Node, Value ), !.
ot_equation( Ot_name, Node, p(Node) ):-
	write('ot_equation:error, OTN: '), write( Ot_name ),
	write(',using node: '), write( Node ), write(' = '),
	write( p(N) ), nl.
/*----------------------------------------------------------------
%	make_ot_eqn( OtName:i, OtEqnList:i )
%	make_ot_eqn(	OtName		: OrdinalTreeName,
%			OtEqnList	: [ node = node_value , .. ] )
%	Given a OtName, and OtEqnList, it asserts the ot_eqns.
----------------------------------------------------------------*/
make_ot_eqn( OtName, [] ).
make_ot_eqn( OtName, [ Node = NodeValue | OtEqnList_T ] ):-
	assertz( ot_eqn( OtName, Node, NodeValue ) ),
	make_ot_eqn( OtName, OtEqnList_T ).
/*--------------------------------------------------------------*/

/*----------------------------------------------------------------
	Test equations
ot_eqn describing ordinal trees, used for testing ot().
ot_eqn(	TreeName, NodeName, NodeValue )
ot_eqn( t#, n(#), split(n(#),n(#)) ).
ot_eqn( t#, n(#), p(#) ).
----------------------------------------------------------------*/
ot_eqn( t0, n(x), split(n(y),n(x)) ).
ot_eqn( t0, n(y), p(a)).
ot_eqn( t1, n(x), split(n(y),n(z)) ).
ot_eqn( t1, n(y), split(n(p),n(q)) ).
ot_eqn( t1, n(p), p(1) ).
ot_eqn( t1, n(q), p(2) ).
ot_eqn( t1, n(z), p(3) ).
ot_eqn( t2, n(x), split(n(x),n(z)) ).
ot_eqn( t2, n(z), p(a) ).
ot_eqn( t3, n(x), split(n(y),n(z)) ).
ot_eqn( t3, n(y), split(n(u),n(v)) ).
ot_eqn( t3, n(z), split(n(v),n(r)) ).
ot_eqn( t3, n(u), p(a) ).
ot_eqn( t3, n(v), p(b) ).
ot_eqn( t3, n(r), p(c) ).
ot_eqn( t4, n(x), split(n(w),n(y)) ).
ot_eqn( t4, n(y), split(n(u),n(z)) ).
ot_eqn( t4, n(z), split(n(v),n(x)) ).
ot_eqn( t4, n(w), p(a) ).
ot_eqn( t4, n(u), p(b) ).
ot_eqn( t4, n(v), p(c) ).
ot_eqn( t5, n(x), split(n(v),n(y)) ).
ot_eqn( t5, n(y), split(n(w),n(z)) ).
ot_eqn( t5, n(z), split(n(r),n(u)) ).
ot_eqn( t5, n(u), split(n(s),n(y)) ).
ot_eqn( t5, n(v), p(a) ).
ot_eqn( t5, n(w), p(b) ).
ot_eqn( t5, n(r), p(c) ).
ot_eqn( t5, n(s), p(d) ).
ot_eqn( t6, n(x), split(n(y),n(x)) ).
ot_eqn( t6, n(y), split(n(z),n(y)) ).
ot_eqn( t6, n(z), split(n(u),n(z)) ).
ot_eqn( t6, n(u), split(n(v),n(u)) ).
ot_eqn( t6, n(v), p(a) ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	file: str.pro
%	string_ot( String:i, Root:i, OtEqnList:o )
%	string_ot(	String		: string,
%			Root		: node_name,
%			OtEqnList	: ot_eqn_list )
%
%	Obtain equations representing a given string
%	rooted at node n(Root),
%	To avoid duplicate answers, ! after new_node,
%	since new_node always suceeding on backtrack.
----------------------------------------------------------------*/
string_ot( p(P), n(A), [ n(A) = p(P) ] ):- !.
/*	process power of omega					*/
string_ot( [ST^w], n(A), [ n(A) = split( n(L), n(A) ) | OtEqnList ] ):-
	new_node( L ), !, string_ot( ST, n(L), OtEqnList ).

/*	process first and n_th power of omega			*/
string_ot( [ST^w^1], n(A), [ n(A) = split( n(L), n(A) ) | OtEqnList ] ):-
	new_node( L ), !, string_ot( ST, n(L), OtEqnList ).

string_ot( [ST^w^N], n(A), [ n(A) = split( n(L), n(A) ) | OtEqnList ] ):-
	integer( N ), M is N - 1, new_node( L ), !,
	string_ot( [ST^w^M], n(L), OtEqnList ).

/*	process lists, [] is invalid				*/

string_ot( [H], n(A), OtEqnList ):- !, string_ot( H, n(A), OtEqnList ).

string_ot( [H|T], n(A), [ n(A) = split( n(L), n(R) ) | OtEqnList_A ] ):-
	new_node( L ), new_node( R ), !,
	string_ot( H, n(L), OtEqnList_LA ),
	string_ot( T, n(R), OtEqnList_RA ),
	union( OtEqnList_LA, OtEqnList_RA, OtEqnList_A ).

/*	error check						*/
string_ot( String, Node, [ Node = String ] ):-
	write('string_ot:error, using: node: '), write( Node ),
	write( ' = string: '), write( String ), nl.
/*----------------------------------------------------------------
%	node_name( Count:io : global integer data variable )
%	new_node( Count:o : a new number to name new nodes )
----------------------------------------------------------------*/
node_name( 0 ).
new_node( Count ) :-
	retract( node_name( Count ) ),
	M is Count + 1,
	assert( node_name( M ) ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	File: lib.pro
%	member( x:i, list:i )
%	Tested	6-oct-91, 9am. see notebook
----------------------------------------------------------------*/
member( X, [X|_] ).
member( X, [_|Tail] ):- member( X, Tail ).
/*----------------------------------------------------------------
%	union( L1:i, L2:i, L1_union_L2:o )
%	Tested	6-oct-91, 9.10am. see notebook
%	Using append, no need to remove duplicates here.
%		union([],Y,Y).
%		union([X|R],Y,RuY) :-
%			member(X,Y), !, union(R,Y,RuY).
%			union([X|R],Y,[X|RuY]) :- union(R,Y,RuY).
----------------------------------------------------------------*/
union( A, B, C ):- append( A, B, C ).
/*----------------------------------------------------------------
%	append( L1:i, L2:i, L1_appended_to_L2:o )
%	Tested	6-oct-91, 9.10am. see notebook
%	The two rules have been split into 4, to take care of
%	two cases: L2 = [], L2 = [L2H|L2T], This accepts only lists.
----------------------------------------------------------------*/
append([],[],[]).
append([],[LH|LT],[LH|LT]).
append([X|L1],[],[X|L1]).
append([X|L1],[L2H|L2T],[X|L3]) :- append(L1,[L2H|L2T],L3).
/*----------------------------------------------------------------
%	printlist( List:i ): for testing
%	Tested	6-oct-91, 9am. see notebook
----------------------------------------------------------------*/
printlist( X ):- var( X ), !.
printlist([]).
printlist([Head|Tail]):- write(Head),nl,printlist(Tail).
/*----------------------------------------------------------------
%	frontlast( A:List:i, FrontOfA:List:o, LastElementOfA:o )
%		The converse of car/cdr, head/tail.
%	eg.	frontlast( [a,b,c], [a,b], [c] ).
%	Tested	6-oct-91, 9am. see notebook
----------------------------------------------------------------*/
frontlast( [H], [], H ).
frontlast( [H|T], [H|FT], LT ):-
	frontlast( T, FT, LT ).
/*----------------------------------------------------------------
%	islist( A:i )
%	Tested	6-oct-91, 3pm. see notebook
----------------------------------------------------------------*/
islist( [] ).
islist( [_|T] ) :- islist( T ).
/*----------------------------------------------------------------
%	length( List:i, LengthofList:integer:o )
%	Tested	7-oct-91, 11am. see notebook
----------------------------------------------------------------*/
length( [], 0 ).
length( [_|T], M ):- length( T, N ), M is N + 1.
/*----------------------------------------------------------------
%	reverse( List:i, ReversedList:o )
%	Tested	7-oct-91, 11:50pm. see notebook
----------------------------------------------------------------*/
reverse( A, B ) :-
	reverse( A, [], B ).
reverse( [], S, S ).
reverse( [A|B], S, C ) :-
	reverse( B, [A|S], C ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	File: nf.pro
%	normalform( St1:i, St2:o ) Top call
%	normalform( St1:i, St3:i, St2:o )
%		recurse until done.
%		repeat nf(St1,St2) until St1 == St2.
%	HalfTested	7-oct-91, 8:45pm. works very well.
----------------------------------------------------------------*/
normalform( S, V ):-
	standardform( S, T ),
	!,
	normalform( T, [] , V ).

normalform( A, A, A ) :- !.
normalform( A4, A3, D ) :-
	nf( A4, B ),
	sf( B, A5 ),
	normalform( A5, A4, D ).
/*----------------------------------------------------------------
%	nf( String1:i, String2:o )
%	nflist( List1:i, List2:o )
%		List2 is List1 with each element normalised.
%		String2 is normal form of String1
%	HalfTested	7-oct-91, 8:45pm. works.
----------------------------------------------------------------*/
nf( A, A ) :- alphabet( A ).

nf( A^w^N, D^w^N ):-
	nf( A, B),
	omegagobble( B, C ),
	callpack( C, D ).

nf( L, B ):-
	islist( L ),
	nflist( L, A ),
	listgobble( A, B ).

/*	nf every element of a list	*/
nflist( [], [] ).
nflist( [H|T], [A|B] ):-
	nf( H, A ),
	nflist( T, B ).
/*----------------------------------------------------------------
%	standardform( St1:i, St2:o )
%		for User convinience, a^w => [a]^w^1
%		standardform of St1 is St2.
%	HalfTested	7-oct-91, 8:45pm. works.
----------------------------------------------------------------*/
standardform( A, A ) :-
	alphabet( A ).
standardform( [], [] ).
standardform( [H|T], [SH|ST] ):-
	standardform( H, SH ),
	standardform( T, ST ).
standardform( A^w , B ) :-
	standardform( A^w^1, B ).
standardform( A^w^N, [A]^w^N ) :-
	alphabet( A ),
	!.
standardform( A^w^N, B^w^N ):-
	standardform( A, B ).
standardform( A, _ ):-
	write('error:standardform > '), write( A ), nl,
	fail.
/*----------------------------------------------------------------
%	sf( St1:i, St2:o )
%		standardform of St1 is St2.
%	HalfTested	7-oct-91, 8:45pm. works.
----------------------------------------------------------------*/
sf( A, A ) :-
	alphabet( A ).
sf( [], [] ).
sf( [H|T], [SH|ST] ):-
	sf( H, SH ),
	sf( T, ST ).
sf( [A^w^N]^w^M, B ):-
	integer( N ),
	integer( M ),
	K is N + M,
	sf( A^w^K, B ).
sf( A^w^N, B^w^N ):-
	sf( A, B ).
/*----------------------------------------------------------------
%	alphabet( Term:i ) 	succeeds if Term
%		is an alphabet of the string language.
%	ie. Term is a propostion/constant/term
%	HalfTested	7-oct-91, 8:45pm. works.
----------------------------------------------------------------*/
alphabet( p(X) ).
alphabet( X ):- atomic( X ).

/*----------------------------------------------------------------
%	File: gob.pro
%	listgobble( List:i, List:o )		Always succeeds
%	    apply the following to every adjacent elements:
%		headgobble(  HeadList , T^w^N )
%		unrollgobble( T^w^1, T^w^N )
%		rotagobble( T, T^w^1 )
%	HalfTested, seems ok,	7-oct-91, 7pm.
----------------------------------------------------------------*/
listgobble( A, D ):-
	applyhg( A, B ),
	applyug( B, C ),
	applyrg( C, D ).
/*----------------------------------------------------------------
%	applyhg( ListA:i, ListC:o )	Always succeeds
%	applyhg( ListA:i, DoneListB:i, AnswerListC:o ).
%	Goes right to left.
%	   for each ti of a List:in
%		it takes each sublist [t1..t(i-1)] in List:in,
%		and applies it to ti for ???? gobble.
%	see diagram in note book.
%	HalfTested, seems ok,	7-oct-91, 7pm.
----------------------------------------------------------------*/
applyhg( A, A ) :- length( A , N ), N < 2.
applyhg( A, B ) :-
	applyhg( A, [], B ).
applyhg( [], Done, Done ).

/*	apply last of A on front of A to get B,
	and be done with last of B.
*/
applyhg( A, Done, C ) :-
	frontlast( A, Fa, La ),
	callheadgobble( Fa, La, B ),
	frontlast( B, Fb, Lb ),
	applyhg( Fb, [Lb|Done], C ).
/*----------------------------------------------------------------
%	applyug( A:List:i, B:List:o ) 	Always succeeds
%	     apply unrollgobble on adjacent terms, right to left.
%	HalfTested, seems ok,	7-oct-91, 7pm.
----------------------------------------------------------------*/
applyug( A, A ) :- length( A , N ), N < 2.
applyug( [A,B], AB ) :-
	unrollgobble( A, B, AB ).
applyug( [H|T], Z ) :-
	applyug( T, [X|Y] ),
	unrollgobble( H, X, HX ),
	append( HX, Y, Z ).
/*----------------------------------------------------------------
%	applyrg( A:List:i, B:List:o ) Always succeeds
%	     apply rotagobble on adjacent terms, right to left.
%	HalfTested, seems ok,	7-oct-91, 7pm.
----------------------------------------------------------------*/
applyrg( A, A ) :- length( A , N ), N < 2.
applyrg( [A,B], AB ) :-
	rotagobble( A, B, AB ).
applyrg( [H|T], Z ) :-
	applyrg( T, [X|Y] ),
	rotagobble( H, X, HX ),
	append( HX, Y, Z ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	omegagobble( List:i, List:o )	Always succeeds
%	   omegahg( List:i, List:o )  Always succeeds
%	  	headgobble (for a list followed by a term)
%	   omegarg( List:i, List:o )  Always succeeds
%	  	unrollgobble (for w^1 term followed by w^N term)
%	   omegaug( List:i, List:o) Always succeeds
%	  	rotagobble (for a term followed by w^1 term)
%
%	for terms of form [[a]^w^1,..,a]^w^N,
%	the head can gobble the last term(s),
%	because of the outer ^w^N, not passed here (implicit).
%	eg.	[[a]^w^1,b,c,a]^w^N => [[a]^w,b,c]^w^N
%	HalfTested, seems ok,	7-oct-91, 7pm.
----------------------------------------------------------------*/
omegagobble( A, D ) :-
	omegahg( A, B ),
	omegaug( B, C ),
	omegarg( C, D ).
/*	you need two or more elements to start with		*/
omegahg( X, X ) :- length( X , N ), N < 2.
omegahg( [H|T], [L|F] ) :-
	callheadgobble( T, H, A ),
	frontlast( A, F, L ).

omegaug( X, X ) :- length( X , N ), N < 2.
omegaug( [H|T], [Y|G] ) :-
	frontlast( T, F, L ),
	unrollgobble( L, H, A ),
	frontlast( A, X, Y ),
	append( F, X, G ).

omegarg( X, X ) :- length( X , N ), N < 2.
omegarg( [H|T], [Y|G] ) :-
	frontlast( T, F, L ),
	rotagobble( L, H, A ),
	frontlast( A, X, Y ),
	append( F, X, G ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	callheadgobble( HeadList:i, Term^w^N:i, CombinedList:o )
%				Always succeeds once.
%	headgobble( HeadList:i, Term^w^N:i, LeftOverHeadList:o )
%		The Term may direct gobble part of head or
%		The Head of Term of omega power may gobble
%		a HeadList before it.
%		Double recursion: inside HeadList, and inside Term.
%	eg. 	[a, [a]^w^1 ] => [ [a]^w^1 ]
%		callheadgobble( a, [a]^w^1, [[a]^w^1] ).
%	eg.	[a, [[a^w^1,c],d]^w^1 ] => [[a^w^1,c],d]^w^1
%		callheadgobble( [a], [[a^w^1,c],d]^1, [[[a^w^1,c],d]^1] )
%	eg.	[x,a,b, [[[a,b]^w^1,c],d]^w^1] ]
%		=>	[x,[[[a,b]^w^1,c],d]^w^1]
%		callheadgobble( [x,a,b], [[a,b]^w^1,c],d]^w^1 ,
%				[x,[[a,b]^w^1,c],d]^w^1] )
%	eg.	[x,[[a]^w^1,b]^w^N] => no headgobble
%		callheadgobble( [x], [[a]^w^1,b]^w^4,
%				[x,[[a]^w^1,b]^w^4] )
%	Tested	6-oct-91, 3.30pm. see notebook
----------------------------------------------------------------*/
callheadgobble( A, B^w^N, C ):-
	headgobble( A, B^w^N ,LA),
	append( LA, [B^w^N], C ),
	!.
/*	catch all	*/
callheadgobble( A, B, C):-
	append( A, [B], C ).
/*	direct gobble	*/
headgobble( T, T^w^N, [] ).
headgobble( [T^w^M], T^w^N, [] ) :-
	integer(M), integer(N),
	M < N.
/*	Recurse inside Term	*/
headgobble( A, [T^w^N|_]^w^M, B ):-
	headgobble( A, T^w^N, B ).
/*	if nothing works, Recurse inside HeadList	*/
headgobble( [A|L], T^w^N, [A|B] ):-
	headgobble( L, T^w^N, B ).
headgobble( [], _, [] ).
/*----------------------------------------------------------------
%	unrollgobble( A^w^1:i, B^w^N:i, D:list:o )
%			Always succeeds only once.
%	unrollgobble( A^w^1:i, B^w^N:i, C:i, D:list:o )
%			Succeeds only gobbling.
%		A is to an explicit power of w^1, it unrolls
%			to release C and gets gobbled by B.
%		B is to an explicit power of w^N, N > 1.
%		C is unrolled part of A (so far).
%		D is result
%	eg.	[ [b,c,a]^w^1 , [a,b,c]^w^5 ] =>
%		=>	[[b,[c,a,b]^w^1] , [a,b,c]^w^5 ]
%		=>	[[b,c,[a,b,c]^w^1] , [a,b,c]^w^5 ]
%		=>	[b,c, [a,b,c]^w^5 ]
%	here:	A = [b,c,a]^w^1,
%		B = [a,b,c]^w^5,
%		D = [b,c, [a,b,c]^w^5 ]
%	eg.	unrollgobble( [a,b]^w^1, [b,a]^w^3, [a,[b,a]^w^3] )
%	Tested	6-oct-91, 10am. see notebook
----------------------------------------------------------------*/
unrollgobble( A^w^1, B^w^N, D ) :-
	integer( N ),
	N > 1,
	unrollgobble( A^w^1, B^w^N, [], D ),
	!.
/*	unrolled A equals B					*/
unrollgobble( A^w^1, A^w^N, _, [A^w^N] ).

/*	'A' was completely unrolled once without a match 	*/
unrollgobble( A^w^1, B^w^N, A, [A^w^1,B^w^N] ):- !, fail.

/*	A is Unrolled as [H,T] => [H,[T,H]],
	now B will try to gobble [T,H]
*/
unrollgobble( [H|T]^w^1, B^w^N, U, [H|G] ):-
	append( T, [H], R ),
	append( U, [H], V ),
	unrollgobble( R^w^1, B^w^N, V, G ).

/*	catch all, A/B not of correct w^power */
unrollgobble( A, B, [A,B] ).
/*----------------------------------------------------------------
%	rotagobble( A:term:i, B^w^1:i, List:o )
%	Always succeeds only once.
%		B^w^1 may gobble a single element 'A' before it
%		and the list_B itself rotates.
%		rotagobble may occur many times on the same List.
%	eg.	[x,a, [b,x,a]^w^1 ]
%		=> [ x, [a,b,x]^w^1 ]	rotagobble once
%		=> [ [x,a,b]^w^1 ]	rotagobble twice
%	rotagobble( a, [b,x,a]^w^1, [[a,b,x]^w^1] )
%	Tested	6-oct-91, 9.30am. see notebook
----------------------------------------------------------------*/
rotagobble( A, B^w^1, [[A|LB]^w^1] ):-
	frontlast( B, LB, A ), !.
rotagobble( A, B, [A,B] ).
/*--------------------------------------------------------------*/
/*----------------------------------------------------------------
%	File: pack.pro
%	callpack( String1:i, String2:o ) Always succeeds
%	Tested	6-oct-91, 9.15am. see notebook
----------------------------------------------------------------*/
callpack( A, B ) :- nonvar( A ), pack( A, B ), !.
callpack( A, A ).
/*----------------------------------------------------------------
%	pack( String1:i, String2:o ) Succeeds only on a packing
%	Tested: works well, 1-Oct-91.
%	since: [S,S,S]^w => [S]^w
%	pack [a,a,a] => [a]
%	pack [a,b,a,b] => [a,b] etc.
----------------------------------------------------------------*/
pack( [], [] ) :- !.
pack( A, PA ):-
	length( A, LA ),
	A = [F|T],
	packit( A, LA, [F], 1, T, PA ).
/*----------------------------------------------------------------
%	packit( A:i, LA:i, F:i, LF:i, T:i, PA:o ).
%	These hold: LA := |A|, LF := |F|, append( F, T, A )
%	-------- The Algo for packing is -----------
%	k := length( A )
%	A := [a1,..,ak ]
%	for i := 1 to k do
%		B :=  [ a1,..,ai ]
%		if A = B.B.B..B then
%			return B
%	Optimized: try only if |B| divides |A|.
%	packit(	List,
%		LengthOfList,
%		FrontOfList,
%		LengthOfFrontOfList,
%		TailOfList,
%		PackedList ).
----------------------------------------------------------------*/
/*	The sublist  F is longer than half of OriginalList A	*/
packit( A, LA, F, LF, _, A ):-
	LF2 is LF * 2 ,
	LF2 > LA ,
	! ,
	fail.
/*	if  |F| divides |A| then,  check if A == F,F,..,F	*/
packit( A, LA, F, LF, T, F ):-
	0 is LA mod LF,
	packpower( A, [], F ).
/*	else try with a larger F				*/
packit( A, LA, F, LF, [H|T], PA ):-
	append( F, [H], FH ),
	LFH is LF + 1,
	packit( A, LA, FH, LFH, T, PA ).
/*----------------------------------------------------------------
%	packpower( A:i, R:io, B:i )
%		if	 A = B,B,..,B,R,
%		and	 |R|<|B|.
%	eg. packpower( [a,b,c,a,b,c,x,x], [x,x], [a,b,c] ).
%	In some sense, R is the remainder on A divided by B.
%	See if A = B,B,..,B.
%	Repeatedly remove B from the front of A,
----------------------------------------------------------------*/
packpower( [], [], _ ).
packpower( A, [], B ):-
	packpower( A, B, B ).
packpower( [X|Y], [X|Z], B ) :-
	packpower( Y, Z, B ).
/*--------------------------------------------------------------*/
/*--------------------------------------------------------------*/
/*
%	File: help.pro
*/
help :-
write('F1: prolog86 [...]. ...'), nl,
write('F2: smartkey'), nl,
write('F4: listing(?) S.F4: spy(?)  C.F4: nospy(?) '), nl,
write('F7: match(?,?) '), nl,
write('F8: match( , ) '), nl,
nl.
/*--------------------------------------------------------------*/
/*--------------------------------------------------------------*/
/*
%	File: test.pro
%	Tests for normalform
*/
testnf( N ) :-
	testnf( N, N ).
/*	Test strings N to M	*/
testnf( N, M ):-
	N > M, !.
testnf( N, M ) :-
	nl,
	testnf( N, Str,  Title ),
	write( N ), write(') '), write( Str ), nl,
	normalform( Str, Y ),
	write('                '), write( Title ), nl,
	write('=> '), write( Y ), nl,
	K is N + 1,
	testnf( K, M ).
/*	strings to try out	*/
testnf(	0,
	[a,a^w],
	direct	).
testnf(	1,
	[a^w^2,a^w],
	none	).
testnf(	2,
	[a^w^2,a^w^5],
	direct	).
testnf(	3,
	[a,a,a,a,a,a^w],
	direct	).
testnf(	4,
	[a,b,a,a,a,a^w],
	direct	).
testnf(	5,
	[a,b,a,a,a,b^w],
	none	).
testnf(	6,
	[x,y,[a,a^w]^w^3],
	direct_pack 	).
testnf(	7,
	[a,x,a,a^w],
	direct	).
testnf(	8,
	[a,b,a,b,[a,b]^w],
	direct	).
testnf(	9,
	[a,x,a,b,[a,b]^w],
	direct	).
testnf(	10,
	[b,[a,b]^w],
	rotate	).
testnf(	11,
	[x,b,a,b,[a,b]^w],
	direct_rotate	).
testnf(	12,
	[a,[a^w,b]^w],
	head	).
testnf(	13,
	[a,b,[[a,b]^w,x]^w],
	head	).
testnf(	14,
	[a,b,[[[a,b]^w,x^w,y]^w^3,d]^w],
	head	).
testnf(	15,
	[a,b,[[[a,b]^w,x^w,y]^w^3,d]^w],
	head	).
testnf(	16,
	[a^w,x,a]^w^2,
	tail	).
testnf(	17,
	[[a,b,c]^w,x,a,b,c]^w^2,
	tail	).
testnf(	18,
	[a,a,a]^w,
	pack	).
testnf(	19,
	[x,[a,b,c]^w,[c,a,b]^w^2],
	unroll	).
testnf(	20,
	[a,[a^w,b]^w,b,b,[b,a,a^w]^w^2],
	head_direct_unroll	).
testnf(	21,
	[a,[a^w,b]^w,b,b,[b^w,a,a^w]^w^2],
	head_direct_unrollhead	).
testnf(	22,
	[a,b,c,d,e,[[a,b,c,d,e]^w,b,[b^w,c,d]]^w],
	head_direct_unrollhead	).
testnf(	23,
	[a,[a^w^10,b]^w^12,b,b^w^12,[b^w^15,a,b,[a,b]^w]^w^2],
	big_test	).
/*--------------------------------------------------------------*/