%
/*
 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
                                  The University, Newcastle upton Tyne

 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@csl.sony.co.jp
 $Id$
*/
% ITL subterm standarization with BDT
%
% Fri Jun 21 10:32:58 BST 1991
%
% a standard form of ITL, based on subterm classification
%
%
subterm_init :- 
	abolish(sb,2),
	asserta((sb([],-1))),
	abolish(sbn,1),
	asserta(sbn(0)).

std_check(I,J) :-
	sb(I,J),!.
std_check(I,N1) :-
	retract(sbn(N)),N1 is N+1,asserta(sbn(N1)),
	assertz(sb(I,N1)),!.

itlstd(P,List) :- 
	sbdt(P,List,(0,[]),_).
itlstd(P,List,S) :- 
	sbdt(P,List,(0,S),_).

% BDT classification of subterm

sbdt(true,true,L,L):-!.
sbdt(false,false,L,L):-!.
sbdt(P,F,L,L) :- atomic(P),!,F= ?(P,true,false).
sbdt(?(C,T,F),?(C,T,F),L,L) :- !.
sbdt(not(P),F,L,L1) :- !,sbdt(P,F0,L,L0),sbdt_not(F0,F,L0,L1),!.
   sbdt_not(true,false,L,L).
   sbdt_not(false,true,L,L).
   sbdt_not(F,?(H,A1,B1),L,L1):-
   	arg(1,F,H),arg(2,F,A),arg(3,F,B),
   	sbdt_not(A,A1,L,L0),sbdt_not(B,B1,L0,L1).
sbdt((P,Q),F,L,L2) :- !,
	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
	sbdt_and(P0,Q0,F,L1,L2),!.
   sbdt_and(false,_,false,L,L):-!.
   sbdt_and(_,false,false,L,L):-!.
   sbdt_and(true,T,T,L,L):-!.
   sbdt_and(T,true,T,L,L):-!.
   sbdt_and(P,Q,R,L,L1) :-!,
   	arg(1,P,PF),arg(1,Q,QF),
   	sbdt_and(PF,QF,P,Q,R,L,L1).
   sbdt_and(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
   	sbdt_and(QF,PF,Q,P,R,L,L1).
   sbdt_and(PF,QF,P,Q,?(QF,R0,R1),L,L1):-PF @> QF,!,
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_and(Q0,P,R0,L,L0),
   	sbdt_and(Q1,P,R1,L0,L1).
   sbdt_and(PF,PF,P,Q,?(PF,R0,R1),L,L1):-
   	arg(2,P,P0),arg(3,P,P1),
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_and(P0,Q0,R0,L,L0),
   	sbdt_and(P1,Q1,R1,L0,L1).
sbdt((P;Q),F,L,L2) :- !,
	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
	sbdt_or(P0,Q0,F,L1,L2),!.
   sbdt_or(true,_,true,L,L):-!.
   sbdt_or(_,true,true,L,L):-!.
   sbdt_or(false,T,T,L,L):-!.
   sbdt_or(T,false,T,L,L):-!.
   sbdt_or(P,Q,R,L,L1) :-!,
   	arg(1,P,PF),arg(1,Q,QF),
   	sbdt_or(PF,QF,P,Q,R,L,L1).
   sbdt_or(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
   	sbdt_or(QF,PF,Q,P,R,L,L1).
   sbdt_or(PF,QF,P,Q,?(QF,R0,R1),L,L1):-PF @> QF,!,
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_or(Q0,P,R0,L,L0),
   	sbdt_or(Q1,P,R1,L0,L1).
   sbdt_or(PF,PF,P,Q,?(PF,R0,R1),L,L1):-
   	arg(2,P,P0),arg(3,P,P1),
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_or(P0,Q0,R0,L,L0),
   	sbdt_or(P1,Q1,R1,L0,L1).
sbdt((P&Q), ?(N,true,false),L,L1) :-!,
	sbdt(P,P1,L,L0),sbdt(Q,Q1,L0,L1), 
	% projection touch later part of chop
	std_check((P1&Q1),N).
% bottom up development is effective for quantifier
sbdt(exists(P,Q), ?(N,true,false),L,L1) :-!,
	sbdt(Q,QF,L,L1),
	std_check(exists(P,QF),N).
sbdt(proj(P,Q), ?(N,true,false),L,L1) :-!,
	sbdt(Q,QF,L,L1),     % P part is fixed
	std_check(proj(P,QF),N).
sbdt(prefix(P), ?(N,true,false),L,L1) :-!,
	sbdt(P,PF,L,L1),     % P part is fixed
	std_check(prefix(PF),N).
%sbdt(^(R), ?(N,true,false),(I,L),(I1,L1)) :-!,
%	recorded(current,S,_),!,
%	regular_check(L,L1,S,R,I,I1,N).
sbdt(^(R), ?(N,true,false),(I,L),(I,L)) :-!,
	std_check(^(R),N).
% remove singleton regular variable
sbdt(^(R,S), F,(I,L),(I,L)) :-
	member((^(R,S),F),L),!.
sbdt(^(R,S), ?(N,true,false),(I,L),(I,L)) :-!,
	std_check(^(R,S),N).
% Simple Functor
sbdt(Func,F,L,L) :- functor(Func,_,1),!,F= ?(N,true,false),
	std_check(Func,N).
sbdt(Func,F,L,L) :- functor(Func,_,2),!,F= ?(N,true,false),
	std_check(Func,N).
sbdt(Def,true,L,L) :-
    write('bdtstd error: '),write(Def),nl.

% renumbering (not used now)
regular_check([],[S,I1],S,R,I,I1,N) :- !,
	I1 is I+1,
	std_check(^(R,I1),N).
regular_check([S,J|L],L,S,R,I,I1,N) :- !,
	I1=I,
	std_check(^(R,J),N).
regular_check([_,_|L1],L,S,R,I,I1,N) :- !,
	regular_check(L1,L,S,R,I,I1,N).

sbterm :-
	listing(sb/2),listing(itl_state/2).


bdt2itl(B,F) :- number(B),!,sb(F0,B),
	bdt2itl(F0,F).
bdt2itl(^(R,N),^(R,N)) :-!.
bdt2itl(st(R),st(R)) :-!.
bdt2itl(?(IF,THEN,ELSE),F) :-
	bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0),
	bdt2itl_opt(IF0,THEN0,ELSE0,F).
% little more readable representation
    bdt2itl_opt(IF,true,false,IF) :- !.
    bdt2itl_opt(IF,false,true,not(IF)) :- !.
    bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
    bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
    bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
    bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
    bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
bdt2itl(B,F) :- atom(B),!,F=B.
bdt2itl(B,F) :- 
	functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F).
    bdt2itl_subterm(0,_,_,_) :- !.
    bdt2itl_subterm(N,N1,F,F0) :-
	N0 is N-1,
	arg(N,F,A),arg(N,F0,A0),
	bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0).

% BDT end %