nnf変換とdnf変換を同時に行う

dnf.pl

% nnf変換とdnf変換を一発で計算する単純なプログラム
:- op(1200,xfx,::=),op(650,xfx,∈),op(250,yf,*),op(600,xfy,[&,$]).
G∈{G}. G∈(G|_). G∈(_|G1):-G∈G1. G∈G.
syntax(G,E):-G=..[O|Gs],E=..[O|Es],maplist(syntax,Gs,Es),!.
syntax(G,E):-(G::=Gs),!,G1∈Gs,syntax(G1,E),!.
syntax(x,X):-atom(X),!.
syntax(E*,Ls):-maplist(syntax(E),Ls).
t ::= x | t* | -t | (t | t) | t& t.
dod(D1|D2,D3,D1|D4):-!,dod(D2,D3,D4).
dod(-[],D2,D2):-!.
dod(D2,-[],D2):-!.
dod(D1,D2,D1|D2):-!.
dad(D1,D2|D3,D):-!,dad(D1,D2,D4),dad(D1,D3,D5),dod(D4,D5,D).
dad(D1|D2,D3,D):-!,dad(D1,D3,D4),dad(D2,D3,D5),dod(D4,D5,D).
dad(D1&D2,D3,D1&D4):-!,dad(D2,D3,D4).
dad([],D2,D2):-!.
dad(D2,[],D2):-!.
dad(D1,D2,D1&D2):-!.
dcons(N1&N3,N2,N):-!,dcons(N1,N2,N4),dcons(N3,N2,N5),dad(N4,N5,N).
dcons(N1|N3,N2,N):-!,dcons(N1,N2,N4),dcons(N3,N2,N5),dod(N4,N5,N).
dcons(N1,N2&N3,N):-!,dcons(N1,N2,N4),dcons(N1,N3,N5),dad(N4,N5,N).
dcons(N1,N2|N3,N):-!,dcons(N1,N2,N4),dcons(N1,N3,N5),dod(N4,N5,N).
dcons(B1,B2,[B1|B2]):-!.
t2d(T1&T2,D):-!,t2d(T1,D1),t2d(T2,D2),dad(D1,D2,D).
t2d(T1|T2,D):-!,t2d(T1,D1),t2d(T2,D2),dod(D1,D2,D).
t2d(-T,D):-!,nt2d(T,D).
t2d(Ts,D):-is_list(Ts),!,ts2d(Ts,D).
t2d(X,X):-!.
nt2d(-T,D):-!,t2d(T,D).
nt2d(T1&T2,D):-!,nt2d(T1,D1),nt2d(T2,D2),dod(D1,D2,D).
nt2d(T1|T2,D):-!,nt2d(T1,D1),nt2d(T2,D2),dad(D1,D2,D).
nt2d(Ts,Ds):-is_list(Ts),!,nts2d(Ts,Ds).
nt2d(X,-X):-!.
ts2d(Ts,D):-ts2d1(Ts,T),t2d2(T,D).
ts2d1([],[]):-!.
ts2d1([T|Ts],Ds2):-!,t2d(T,D),ts2d1(Ts,Ds),dcons(D,Ds,Ds2).
t2d2(T1&T2,D):-!,t2d2(T1,D1),t2d2(T2,D2),dad(D1,D2,D).
t2d2(T1|T2,D):-!,t2d2(T1,D1),t2d2(T2,D2),dod(D1,D2,D).
t2d2(Ts,D):- member(-_,Ts),!,maplist(t2a,Ts,A),findall(R,t2m(Ts,R),Ls),foldl(dad,Ls,[],M),dad(A,M,D).
t2d2(T,T):-!.
t2m(L,-R1):- select(-T,L,T,R),maplist(t2a,R,R1).
t2a(-_,[]):-!.
t2a(T,T):-!.
nts2d(Ts,D):-ts2d1(Ts,T),nt2d2(T,D).
nt2d2(T1&T2,D):-!,nt2d2(T1,D1),nt2d2(T2,D2),dad(D1,D2,D).
nt2d2(T1|T2,D):-!,nt2d2(T1,D1),nt2d2(T2,D2),dod(D1,D2,D).
nt2d2(Ts,D):- member(-_,Ts),!,maplist(t2a,Ts,A),findall(R,nt2m(Ts,R),Ls),foldl(dod,Ls,-[],M),dod(-A,M,D).
nt2d2(T,-T):-!.
nt2m(L,R1):- select(-T,L,T,R),maplist(t2a,R,R1).
nts2d1([],[]):-!.
nts2d1([T|Ts],D):-!,nt2d(T,D1),nts2d1(Ts,D2),dcons(D1,D2,D).

:- begin_tests(t2d).
test(a):-t2d(a&a,a&a).
test(a):-t2d(a&b&(c|d),a&b&c|a&b&d).
test(a):-t2d((a|b)&(c|d&e),a&c|b&c|a&d&e|b&d&e).
test(a):-t2d(-(a|b),-a& -b).
test(a):-t2d(-((a|b)&(c|d&e)),-a& -b| -c& -d| -c& -e).
test(a):-t2d(((a|b)|(c|d)|d)|(((a|b)|(c|d)|d)),a|b|c|d|d|a|b|c|d|d).
test(a):-t2d(((-a&c)&b)&((-a&b)&c),-a&c&b& -a&b&c).
test(a):-t2d([a],[a]).
test(a):-t2d([(a|b)],[a]|[b]).
test(a):-t2d([(a|b),c],[a,c]|[b,c]).
test(a):-t2d([a,(a&b),d],[a,a,d]&[a,b,d]).
test(a):-t2d([-a],[[]]& -[a]).
test(a):-t2d([a,-b,-c],[a,[],[]]& -[a,[],c]& -[a,b,[]]).
test(a):-t2d([(a|b),-c],[a,[]]& -[a,c]|[b,[]]& -[b,c]).
test(a):-t2d([-(a|b),d],[[],d]& -[a,d]&[[],d]& -[b,d]).
test(a):-t2d([-(a&b)],[[]]& -[a]|[[]]& -[b]).
test(a):-t2d([- -[- - -a&b],a],[[[]],a]&[[],a]& -[[a],a]&[[b],a]).
test(a):-t2d(- -[-a,- -c],[[],c]& -[a,c]).
test(a):-t2d([a,-c],[a,[]]& -[a,c]).
test(a):-t2d(-[a,-c],-[a,[]]|[a,c]).
test(a):-t2d(-[a,b],-[a,b]).
:- end_tests(t2d).

:-run_tests.
:-halt.