
tancs_to_prolog(O,WFF):-
    name(O,P),!,
    tokeniseTANCS(P,Q),
    lookParse(Q,WFF).

lookParse(['(','('|L],WFF):-
    matchParen(['('|L],0,LR,R),!,
    lookParse(LR,WFFLeft),!,
    lookParseRH(R,WFFRight),!,
    WFFRight =.. [Reln,B],
    WFF =.. [Reln,WFFLeft,B].

lookParse(['(',box,R,':',A,')'],box(R,A)):-!.
lookParse(['(',box,R,':'|L],box(R,WFF)):-
    matchParen(L,0,LR,[')']),!,
    lookParse(LR,WFF).
lookParse(['(',pos,R,':',A,')'],pos(R,A)):-!.
lookParse(['(',pos,R,':'|L],pos(R,WFF)):-
    matchParen(L,0,LR,[')']),!,
    lookParse(LR,WFF).
lookParse(L,WFF):-
    phrase(wff(WFF),L),!.

lookParseRH(L,WFF):-
    phrase(rhwff(WFF),L),!.

matchParen([')'|L],1,[')'],L):-!.
matchParen([')'|L],X,[')'|LL],R):-
    Y is X - 1,
     matchParen(L,Y,LL,R).
matchParen(['('|L],X,['('|LL],R):-
    Y is X + 1,
     matchParen(L,Y,LL,R).
matchParen([I|L],X,[I|LL],R):-
     matchParen(L,X,LL,R).



wff(A)  --> [A], {not(reserved(A))}.
wff(box(R,A)) --> oparen,box_sym,reln(R),colon_sym,wff(A),cparen.
wff(pos(R,A)) --> oparen,pos_sym,reln(R),colon_sym,wff(A),cparen.
wff(not(A)) --> not_sym, wff(A).
wff(or(A,B)) --> oparen,wff(A), or_sym, wff(B),cparen.
wff(and(A,B)) --> oparen,wff(A), and_sym, wff(B),cparen.


rhwff(or(B)) --> or_sym, wff(B),cparen.
rhwff(or(or(B,C))) --> or_sym, wff(B),or_sym, wff(C),cparen.
rhwff(and(B)) --> and_sym, wff(B),cparen.
rhwff(and(and(B,C))) --> and_sym, wff(B),and_sym, wff(C),cparen.

%wff(implies(A,B)) --> oparen,wff(A), implies_sym, wff(B),cparen.
%wff(and(implies(A,B),implies(B,A))) --> oparen,wff(A), equiv_sym, wff(B),cparen.


reln(R) --> [R], {not(reserved(R))}.
not_sym -->['~'].
and_sym -->['&'].
or_sym  -->['|'].
implies_sym --> ['=','>'].
equiv_sym --> ['<','=','>'].
box_sym --> ['box'].
pos_sym --> ['pos'].
colon_sym --> [':'].
oparen --> ['('].
cparen --> [')'].

reserved('~').
reserved('&').
reserved('|').
reserved('=').
reserved('>').
reserved('<').
reserved('box').
reserved('pos').
reserved(':').
reserved('(').
reserved(')').


tokeniseTANCS(I,J):-
	tokeniseTANCS(I,[],J),!.

tokeniseTANCS([],[],[]):-!.

tokeniseTANCS([],In,[InN]):-
	reverse_lower(In,InR),
	name(InN,InR).
tokeniseTANCS([X|L],In,Out):-
	blankSymTANCS(X),
	tokeniseTANCS(L,In,Out).
tokeniseTANCS([32|L],[],Out):-
	tokeniseTANCS(L,[],Out).
tokeniseTANCS([32|L],In,[InN|Out]):-
	reverse_lower(In,InR),
	name(InN,InR),
	tokeniseTANCS(L,[],Out).
tokeniseTANCS([X|L],[],[SY|Out]):-
	endSymTANCS(X,SY),
	tokeniseTANCS(L,[],Out).
tokeniseTANCS([X|L],In,[InN,SY|Out]):-
	endSymTANCS(X,SY),
	reverse_lower(In,InR),
	name(InN,InR),
	tokeniseTANCS(L,[],Out).
tokeniseTANCS([I|L],In,Out):-
	tokeniseTANCS(L,[I|In],Out).

blankSymTANCS(13).
blankSymTANCS(35).
blankSymTANCS(36).
blankSymTANCS(39).
endSymTANCS(38,'&').
endSymTANCS(40,'(').
endSymTANCS(41,')').
endSymTANCS(58,':').
endSymTANCS(60,'<').
endSymTANCS(61,'=').
endSymTANCS(62,'>').
endSymTANCS(124,'|').
endSymTANCS(126,'~').
endSymTANCS(42,'*').
endSymTANCS(45,'-').
endSymTANCS(35,'#').
