# HG changeset patch # User kono # Date 811221645 -32400 # Node ID b35e4dc6ec2372e957169add6649c64ad591eacc Initial revision diff -r 000000000000 -r b35e4dc6ec23 dvcomp.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dvcomp.pl Sat Sep 16 12:20:45 1995 +0900 @@ -0,0 +1,388 @@ +/* + 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 decomposition for DST + +:- dynamic regular_limit/1. +% requires [chop] +% itl(Predicate,Next,Empty,ConditionLists) + +itl(P) :- expand(P,P0), + moref(Ev),itl(P0,Next,Ev,[],C), + write(([Ev|C]->Next)),nl,fail. +itl(_). +itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C). + +moref(empty). +moref(more). + +% :- table itl/5. + +itl(N,F,E,C,C1):-number(N),!, + sb(Subterm,N),!,itl(Subterm,F,E,C,C1). +itl(true,true,_,C,C):-!. +itl(false,false,_,C,C):-!. +itl(more,false,empty,C,C). +itl(more,true,E,C,C):-!,E = more. +% next two rule determines descrete time +itl(empty,true,empty,C,C). +itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval +itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1). + local(true,P,C,C1):- true(C,P,C,C1). + true([],P,C,[P|C]):-!. + true([P|_],P,C,C):-!. + true([not(P)|_],P,_,_):-!,fail. + true([_|T],P,C,C1):-true(T,P,C,C1). + local(false,P,C,C1):- false(C,P,C,C1). + false([],P,C,[not(P)|C]):-!. + false([P|_],P,_,_):-!,fail. + false([not(P)|_],P,C,C):-!. + false([_|T],P,C,C1):-false(T,P,C,C1). +itl(@(P),P,more,C,C). % strong next +itl(@(_),false,E,C,C):-!,E=empty. + +itl(?(Cond,T,F),N,E,C,C1):-!, + itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1). +itl_cond(true,T,_,N,E,C,C1) :-!, + itl(T,N,E,C,C1). +itl_cond(false,_,F,N,E,C,C1) :-!, + itl(F,N,E,C,C1). +itl_cond(CN,T,F,N,E,C,C1) :-!, + itl(T,TN,E,C,C0), + itl(F,FN,E,C0,C1), negate(CN,NCN), + and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N). +% Regular Variable +itl(^(R),F,empty,C,C1):- + local(F0,up(R),C,C0), + local(F1,down(R,0),C0,C1),and(F0,F1,F). +itl(^(R),F1,E,C,[^(R,0)|C1]):-!, E=more, + local(F,up(R),C,C1),and(F,^(R,0),F1). + +itl(^(R,S),F,empty,C,C1):- + local(F,down(R,S),C,C1). +itl(^(R,S),F,E,C,C1):- E = more, + regular_limit(X),S>=X,!, + local(F,over(R,S),C,C1). +itl(^(R,S),^(R,S1),E,C,[^(R,S1)|C]):-!, + % increment regular variable rength + % mark reference to detect singleton + E=more, S1 is S+1. + +% Quantifier +itl(exists(P,Q),F,E,C,C0) :-!, + itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0). + itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1). + itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1), + itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F). + itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1), + itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0), + or(QT,QF,TF),exists(TF,P,F). + % constant order optimzation for quantifier + exists(P,P,true):-!. + exists(P,_,P):-atomic(P),!. + exists(Q,P,exists(P,Q)). + remove_p([],_,[]):-!. + remove_p([not(P)|T],P,T):-!. + remove_p([P|T],P,T):-!. + remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1). +itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1). +itl(*(P),F,E,C,C1):-!,E=more, + itl(P,PX,more,C,C1), + closure(PX,P,F). + closure(false,_,false):-!. + closure(PX,P,(PX & *(P))). %% infinite clousre (strong) +%% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak) +%% external state diagram +itl(st(N),F,E,C,C1):-!, + setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1). + itl_transition([],false,_,C,C):-!. + itl_transition([(Cond=>empty)|T],F,E,C,C1):-!, + itl((empty,Cond),F0,E,C,C0), + itl_transition(T,F1,E,C0,C1),or(F0,F1,F). + itl_transition([(Cond=>X)|T],F,E,C,C1):- + itl((more,Cond),F0,E,C,C0), + itl_transition1(F0,X,T,F,E,C0,C1). + itl_transition1(false,_,T,F,E,C,C1):- + itl_transition(T,F,E,C,C1). + itl_transition1(true,X,T,(st(X);F),E,C,C1):- + itl_transition(T,F,E,C,C1). +%% ignore last state to check non stop predicate +itl(non_terminate(_),F,empty,C,C):-!,F=true. +itl(non_terminate(L),F,more,C,C1):-!, + itl(L,F,more,C,C1). +%% shared resources or state +itl(share(L),F,empty,C,C1):-!, + exclusive(L,C,C1,true,F). +itl(share(L),F,more,C,C1):-!, + exclusive(L,C,C1,share(L),F). + exclusive([],C,C,F,F):-!. + exclusive([A|L],C,C1,F,F1):- + true(C,A,C,C0),exclusive1(L,C0,C1,F,F1). + exclusive([N|L],C,C1,F,F1):- + false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1). +% exclusive(_,C,C,_,false). % eliminate this brach + exclusive1([],C,C,F,F):-!. + exclusive1([H|L],C,C1,F,F1):- + false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1). +% exclusive1(_,C,C,_,false). +%% +itl((P,Q),N,E,C,C1) :-!, + itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1). +itland(false,_,false,_,C0,C0):-!. +itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). +itland(PN,Q,N,E,C0,C1):- + itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl +itl((P;Q),N,E,C,C1) :-!, + itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1). +itlor(true,_,true,_,C0,C0):-!. +itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). +itlor(PN,Q,N,E,C0,C1):- + itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl +itl(not(P),NN,E,X,X1) :- !, + itl(P,N,E,X,X1), + negate(N,NN). %% negate/2 in chop.pl +% F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q) +itl((P&Q),F,empty,C,C1) :-!, + itl((P,Q),F,empty,C,C1). +itl((P&Q),F,more,C,C2) :-!, + itl(P,PE,empty,C,C0), + itl(P,PM,more,C0,C1), + chop(PM,PE,F,Q,C1,C2). + +chop(false,false,false,_,C,C):-!. +chop(PM,false,(PM & Q),Q,C,C):-!. +chop(PM,true,F,Q,C,C1):-!, + itl(Q,QF,more,C,C1), + chop1(PM,QF,Q,F). +chop(PM,PE,F,Q,C,C):-!, + write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!, + fail. + +chop1(false,QF,_,QF):-!. +chop1(false,false,_,false):-!. +chop1(PM,false,Q,(PM&Q)):-!. +chop1(_,true,_,true):-!. +chop1(PM,QF,Q,(QF;(PM&Q))):-!. + +itl(proj(_,Q),F,empty,C,C1) :-!, + itl(Q,F,empty,C,C1). +itl(proj(P,Q),F,more,C,C1) :-!, + itl(P,PM,more,C,C0), + itl(Q,QM,more,C0,C1), + prj(PM,QM,P,F). +prj(false,_,_,false):-!. +prj(_,false,_,false):-!. +prj(PM,QM,P,(PM&proj(P,QM))). + +itl(prefix(P),F,empty,C,C1) :-!, + itl(P,PE,empty,C,C0), + itl(P,PM,more,C0,C1), + prefix(PM,PE,F). +itl(prefix(P),F,more,C,C1) :-!, + itl(P,PM,more,C,C1), + prefix(PM,F). + +prefix(true,true):-!. +prefix(false,false):-!. +prefix(PM,prefix(PM)):-!. + +prefix(true,_,true):-!. +prefix(_,true,true):-!. +prefix(false,false,false):-!. +prefix(_,false,true):-!. + +itl(Def,_,_,_,_) :- + write('error: '),write(Def),nl,!,fail. + +% detect regular variable singleton +% we can do renumbering here +% what do we do for permutation? + +itl_singleton([empty|L],[empty|L],[]) :- !. +itl_singleton(Cond,Cond1,Singleton) :- singleton,!, + select_singleton(Cond,Cond0,V), + split_singleton_case(V,Cond0,Cond1,Singleton). +itl_singleton(Cond,Cond1,[]) :- + select_singleton(Cond,Cond1,_). + +select_singleton([],[],[]):-!. +select_singleton([^(R,S)|L],L1,V):-!, + check_singleton(L,^(R,S),L0,single,F), + (F==single -> V = [^(R,S)|V0],select_singleton(L0,L1,V0) + ; select_singleton(L0,L1,V)). +select_singleton([H|L],[H|L1],V):-!, + select_singleton(L,L1,V). + +check_singleton([],_,[],F,F):-!. +check_singleton([H|T],H,T1,_,multi):-!, + check_singleton(T,H,T1,_,_). +check_singleton([H|T],H1,[H|T1],F,F1):-!, + check_singleton(T,H1,T1,F,F1). + +% choose singleton's truth value +% split_singleton_case(_,Cond,Cond,[]) :- !. +split_singleton_case([],Cond,Cond,[]). +split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),true)|T1]):- + split_singleton_case(T,[ev(^(R,S))|Cond],Cond1,T1). +split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),false)|T1]):- + split_singleton_case(T,[not(ev(^(R,S)))|Cond],Cond1,T1). + +% develop Local ITL formula into state diagram +% +% Mon May 20 17:24:23 BST 1991 +% require([chop]). + +:-dynamic verbose/0,state/2,links/2. +:-dynamic stay/3,lazy/0,singleton/0. + +:-assert(verbose). +verbose(off) :- retract(verbose),fail;true. +verbose(on) :- asserta(verbose). + +lazy(off) :- retract(lazy),fail;true. +lazy(on) :- asserta(lazy). + +singleton(off) :- retract(singleton),fail;true. +singleton(on) :- asserta(singleton). + +set_limit(X) :- + set_var(regular_limit,X,_). + +deve(ITL) :- + init,!, + expand(ITL,ITL0), % chop standard form + itlstd(ITL0,StdNOW), % BDT + assert(itl_state(StdNOW,1)),!, % Initial State + deve0((1,StdNOW)). + +deve0((S,ITL)) :- + show_state(S,ITL), + bagof(Next,itldecomp(ITL,Next,S), + Nexts),!, + deve1(Nexts). +deve0(_). + +deve1([]). +deve1([H|T]) :- deve0(H),deve1(T). + +itldecomp(ITL,(NextS,StdNext),From) :- + init_var(current,From), + itl(ITL,Next,Cond), + itl_singleton(Cond,Cond1,Singleton), + %% showing + itlshow(Next,NextS,Cond1,From,StdNext,Singleton). + +itlshow(Next,S,Cond,From,StdNext,Singleton):- + itlstd(Next,StdNext,Singleton), + + itlstd(Next,StdNext1,[]), + bdt2itl(StdNext,ItlNext), + bdt2itl(StdNext1,ItlNext1), + (ItlNext \== ItlNext1 -> write('>>'), + write(ItlNext),nl,write(' '), + write(ItlNext1),nl; true), + + check_state(StdNext,Cond,New,S), + (lazy,!;assertz(state(From,Cond,S))), + (links(S,From),!;assertz(links(S,From))), + itlshow0(S,Cond,StdNext,New), + !. + +itlshow0(S,Cond,Next,New) :- verbose,!, + itlshow1(S,Cond,Next,New),nl,!,New=1. +itlshow0(0,_,_,0):- !,put(101),!,fail. % "e" +itlshow0(false,_,_,0):- !,put(102),!,fail. % "f" +itlshow0(true,_,_,0):- !,put(116),!,fail. % "t" +itlshow0(_,_,_,0):- !,put(46),!,fail. % "." +itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!. + +itlshow1(0,Cond,_,_):-!, + write(Cond),write('->'),write(empty). itlshow1(true,Cond,_,_):-!, + write(Cond),write('->'),write(true). +itlshow1(false,Cond,_,_):-!, + write(Cond),write('->'),write(false). +itlshow1(S,Cond,_,0):-!, + write(Cond),write('->'),write(S). +itlshow1(S,Cond,Org,1):- + write(Cond),write('->'),write(S), + put(9),bdt2itl(Org,Org0),write(Org0),!. + +lazy_state(From,Cond,S) :- + links(S,From), + itl_state(ITL,From), + itl(ITL,Next,Cond), + itlstd(Next,StdNext), + check_state(StdNext,Cond,_,S). + +init :- + subterm_init, + abolish(state,3), + asserta((state(true,[more],true):-!)), + asserta((state(true,[empty],0):-!)), + (lazy,assertz((state(A,B,C) :- lazy_state(A,B,C))),!;true), + abolish(itl_state,2), + abolish(stay,3),asserta(stay(0,0,0)), + asserta(itl_state(false,false)), + asserta(itl_state(empty,0)), + asserta(itl_state(true,true)), + abolish(links,2),asserta(links(true,true)), + init_var(current,0), + init_var(regular_limit,5), + init_var(itl_state_number,1),!. + +show_state(S,ITL) :- + bdt2itl(ITL,ITL0), + nl,write('state('),write(S), % ( + (verbose,write(' , '), write(ITL0),write(')'),nl;write(')')),!. + +check_state(true,[more |_],0,true):-!. +check_state(true,[empty|_],0,0):-!. +check_state(false,_,0,false):-!. +check_state(STD,_,0,S):- + itl_state(STD,S),!. +check_state(STD,_,1,S):- + inc_var(itl_state_number,S), + assert(itl_state(STD,S)),!. + +init_var(X,_) :- functor(F,X,1),assert(F),fail. +init_var(X,_) :- functor(F,X,1),retract(F),fail. +init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!. +inc_var(Name,X1) :- + functor(F,Name,1),retract(F),arg(1,F,X), + X1 is X+1,functor(F1,Name,1),arg(1,F1,X1), + asserta(F1),!. +set_var(Name,X,X1) :- + functor(F,Name,1),retract(F),!,arg(1,F,X), + functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!. +set_var(Name,X,_) :- init_var(Name,X). + +%init_var(X,_) :- recorded(X,_,Ref),erase(Ref),fail. +%init_var(X,V) :- recorda(X,V,_). +%inc_var(Name,X1) :- +% recorded(Name,X,Ref),X1 is X+1, +% erase(Ref),recorda(Name,X1,_). +%set_var(Name,X,X1) :- +% recorded(Name,X1,_),!,init_var(Name,X). +%set_var(Name,X,_) :- init_var(Name,X). + +itl_statistics :- nl, + itl_state_number(X),write(X),write(' states'),nl,fail. +itl_statistics :- + sbn(X),write(X),write(' subterms'),nl,fail. +itl_statistics :- + init_var(tmp,0), + ((links(_,_),inc_var(tmp,_),fail);true), + tmp(N), + write(N),write(' state transions'),nl,fail. +itl_statistics. + +%% end %% diff -r 000000000000 -r b35e4dc6ec23 rstd.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/rstd.pl Sat Sep 16 12:20:45 1995 +0900 @@ -0,0 +1,161 @@ +% +/* + 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 %