--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bdtstd.pl	Thu Jan 18 23:27:24 2001 +0900
@@ -0,0 +1,142 @@
+%
+/*
+ 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 %