%
/*
 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).

% BDT classification of subterm

sbdt(true,true):-!.
sbdt(false,false):-!.
sbdt(P,F) :- atomic(P),!,F= ?(P,true,false).
sbdt(?(C,T,F),?(C,T,F)) :- !.
sbdt(not(P),F) :- !,sbdt(P,F0),sbdt_not(F0,F),!.
   sbdt_not(true,false).
   sbdt_not(false,true).
   sbdt_not(F,?(H,A1,B1)):-
   	arg(1,F,H),arg(2,F,A),arg(3,F,B),
   	sbdt_not(A,A1),sbdt_not(B,B1).
sbdt((P,Q),F) :- !,
	sbdt(P,P0),sbdt(Q,Q0),
	sbdt_and(P0,Q0,F),!.
   sbdt_and(false,_,false):-!.
   sbdt_and(_,false,false):-!.
   sbdt_and(true,T,T):-!.
   sbdt_and(T,true,T):-!.
   sbdt_and(P,Q,R) :-!,
   	arg(1,P,PF),arg(1,Q,QF),
   	sbdt_and(PF,QF,P,Q,R).
   sbdt_and(PF,QF,P,Q,R):-PF @< QF,!,
   	sbdt_and(QF,PF,Q,P,R).
   sbdt_and(PF,QF,P,Q,?(QF,R0,R1)):-PF @> QF,!,
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_and(Q0,P,R0),
   	sbdt_and(Q1,P,R1).
   sbdt_and(PF,PF,P,Q,?(PF,R0,R1)):-
   	arg(2,P,P0),arg(3,P,P1),
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_and(P0,Q0,R0),
   	sbdt_and(P1,Q1,R1).
sbdt((P;Q),F) :- !,
	sbdt(P,P0),sbdt(Q,Q0),
	sbdt_or(P0,Q0,F),!.
   sbdt_or(true,_,true):-!.
   sbdt_or(_,true,true):-!.
   sbdt_or(false,T,T):-!.
   sbdt_or(T,false,T):-!.
   sbdt_or(P,Q,R) :-!,
   	arg(1,P,PF),arg(1,Q,QF),
   	sbdt_or(PF,QF,P,Q,R).
   sbdt_or(PF,QF,P,Q,R):-PF @< QF,!,
   	sbdt_or(QF,PF,Q,P,R).
   sbdt_or(PF,QF,P,Q,?(QF,R0,R1)):-PF @> QF,!,
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_or(Q0,P,R0),
   	sbdt_or(Q1,P,R1).
   sbdt_or(PF,PF,P,Q,?(PF,R0,R1)):-
   	arg(2,P,P0),arg(3,P,P1),
   	arg(2,Q,Q0),arg(3,Q,Q1),
   	sbdt_or(P0,Q0,R0),
   	sbdt_or(P1,Q1,R1).
sbdt((P&Q), ?(N,true,false)) :-!,
	sbdt(P,P1),sbdt(Q,Q1), % projection touch later part of chop
	std_check((P1&Q1),N).
%sbdt(@(Q), ?(N,true,false)) :-!,   % Don't check next part now
%	std_check(@(Q),N).          %   this makes everything very slow
%sbdt(*(Q), ?(N,true,false)) :-!,   % Don't check next part now
%	std_check(*(Q),N).          %   this makes everything very slow
%sbdt(free_fin(Q), ?(N,true,false)) :-!,
%	std_check(free_fin(Q),N).
% bottom up development is effective for quantifier
sbdt(exists(P,Q), ?(N,true,false)) :-!,
	sbdt(Q,QF),
	std_check(exists(P,QF),N).
sbdt(proj(P,Q), ?(N,true,false)) :-!,
	sbdt(Q,QF),     % P part is fixed
	std_check(proj(P,QF),N).
sbdt(prefix(P), ?(N,true,false)) :-!,
	sbdt(P,PF),     % P part is fixed
	std_check(prefix(PF),N).
% Simple Functor including Regular variable and state
sbdt(Func,F) :- functor(Func,_,1),!,F= ?(N,true,false),
	std_check(Func,N).
sbdt(Func,F) :- functor(Func,_,2),!,F= ?(N,true,false),
	std_check(Func,N).
sbdt(Def,true) :-
    write('bdtstd error: '),write(Def),nl.

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


bdt2itl(B,F) :- number(B),!,sb(F0,B),
	bdt2itl(F0,F).
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 %