dnf+

dnf+.pl

% Sound and Complete Flow Typing with Unions,
% Intersections and Negation
% https://ecs.wgtn.ac.nz/foswiki/pub/Main/TechnicalReportSeries/ECSTR12-20.pdf

:- 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(i,I):-integer(I),!.
syntax(E*,Ls):-maplist(syntax(E),Ls).
x ::= int | x* .
y ::= any | int | y* .
t ::= y | -t | (t|t) | t&t.
b ::= x | -x.
n ::= b | (n|n) | n&n.
c ::= b* .
d ::= c* .
ns ::= (-x)* .
a ::= [x|ns] | ns.
o ::= a* .
comparison ::= (=) | (<:) | (:>).
comparison2 ::= comparison | none.

x2y([],any):-!.
x2y(int,int):-!.
x2y(-X,-Y):-!,x2y(X,Y).
x2y(Ls,Ls_):-!,maplist(x2y,Ls,Ls_).
t2n(-T,N):-!,t2nneg(T,N).
t2n(T1&T2,N1&N2):-!,t2n(T1,N1),t2n(T2,N2).
t2n(T1|T2,N1|N2):-!,t2n(T1,N1),t2n(T2,N2).
t2n(Y,X):-!,x2y(X,Y).
t2nneg(-T,N):-!,t2n(T,N).
t2nneg(T1&T2,N1|N2):-!,t2nneg(T1,N1),t2nneg(T2,N2).
t2nneg(T1|T2,N1&N2):-!,t2nneg(T1,N1),t2nneg(T2,N2).
t2nneg(Y,X_):-!,x2y(X,Y),(-X_ = X;X_ = -X).

cod(C1,[],[C1]):-!.
cod(C1,[C|D],[C|D_]):-!,cod(C1,D,D_).
bod(B1,D2,D):-cod([B1],D2,D).
dod([],_,[]):-!.
dod([C1|D1],D2,D):-dod(D1,D2,D3),cod(C1,D3,D).
bac(B1,C2,[B1|C2]).
cac([],C1,C1):-!.
cac([B|C0],C1,C):-cac(C0,C1,C2),bac(B,C2,C). 
cad(_,[],[]):-!.
cad(C,[C2|D2],D):-cac(C,C2,C3),cad(C,D2,D3),cod(C3,D3,D).
dad([],_,[]):-!.
dad([C1|D1],D2,D):-cad(C1,D2,D3),dad(D1,D2,D4),dod(D3,D4,D).
nod(A|B,D2,D):-!,nod(B,D2,D3),nod(A,D3,D).
nod(A&B,D2,D):-!,n2d(A,DA),n2d(B,DB),dad(DA,DB,DAB),dod(DAB,D2,D).
nod(B,D2,D):-!,bod(B,D2,D).
n2d(N,D):-nod(N,[],D).
t2d(T,D):-t2n(T,N),n2d(N,D).

xsub(_,[],1):-!.
xsub(int,int,1):-!.
xsub([],_,0):-!.
xsub([V1|X1],[V2|X2],R):-!,xsub(V1,V2,R1),xsub(X1,X2,R2),R is R1/\R2.
xsub(_,_,0):-!.
xsubcmp(X1,X2,R):- xsub(X1,X2,R1),xsub(X2,X1,R2),xsubcmp1(R1,R2,R).
xsubcmp1(1,1,=):-!.
xsubcmp1(1,0,:>):-!.
xsubcmp1(0,1,<:):-!.
xsubcmp1(0,0,none).
xcmp(int,int,=):-!.
xcmp([],[],=):-!.
xcmp(_,[],<:):-!.
xcmp([],_,:>):-!.
xcmp(_,int,<:):-!.
xcmp(int,_,:>):-!.
xcmp([V|X],[V2|X2],R):-xcmp(X,X2,R1),(R1=(=)->xcmp(V,V2,R);R=R1).
xax([],X,X):-!.
xax(X,[],X):-!.
xax(int,int,int):-!.
xax(Xs,Xs2,R):-xsaxs(Xs,Xs2,R).
xsaxs([],[],[]):-!.
xsaxs([X|Xs],[X2|Xs2],[R|Rs]):-xax(X,X2,R),xsaxs(Xs,Xs2,Rs).
cons(X,[],[X]):-!.
cons(-X,[-X2|Ns2],R):-xsubcmp(X,X2,R1),cons1(-X,R1,[-X2|Ns2],R).
cons1(B,<:,[_|Ns2],R):-!,cons(B,Ns2,R).
cons1(-X,none,[-X2|Ns2],R):-!,xcmp(X,X2,R1),cons2(-X,R1,[-X2|Ns2],R).
cons1(_,_,Ns1,Ns1).
cons2(B,:>,Ns1,[B|Ns1]):-!.
cons2(B,_,[B2|Ns2],[B2|R]):-cons(B,Ns2,R).
xans(X,-N,Ns,R):-xsubcmp(N,X,R1),xans1(X,N,Ns,R1,R).
xans1(_,N,Ns,:>,R):-!,cons(-N,Ns,R).
xans1(X,N,Ns,none,R):-xax(N,X,R1),cons(-R1,Ns,R),!.
xans1(_,_,Ns,none,Ns).
nsans(X,Ns1,Ns2,R):-foldl(xans(X),Ns1,Ns2,R).
aaa([X1|Ns1],[X2|Ns2],[X|R]):-xax(X1,X2,X),nsans(X,Ns2,[],R1),nsans(X,Ns1,R1,R).
b2a(-[],_):-!,fail.
b2a(-X,[[],-X]):-!.
b2a([],[[]]):-!.
b2a(X,[X]):-!.
baa(B1,A2,R):- b2a(B1,A1),aaa(A1,A2,R).
c2a([],[[]]):-!.
c2a([B|C],R):-c2a(C,R1),baa(B,R1,R).
d2o(D,O):-findall(A,(member(C,D),c2a(C,A)),O1),list_to_ord_set(O1,O).

ns2n(X,any,Y):-!,x2y(X,Y).
ns2n(X,T,T& Y):-!,x2y(X,Y).
a2n(Ns,-any,T_):-!,foldl(ns2n,Ns,any,T_).
a2n(Ns,T,T|T_):-!,foldl(ns2n,Ns,any,T_).
o2n(O,T):-foldl(a2n,O,-any,T).
t2o(T,O):- t2d(T,D),d2o(D,O).
t2o2(T,O,N):- t2d(T,D),d2o(D,O),o2n(O,N).
t2n2(T,N):- t2d(T,D),d2o(D,O),o2n(O,N).

tsub(T1,T2):- t2o(T1 & -T2,[]).
t(_,V,int):-integer(V),!. %(T-Int)
t(Γ,X,T):-member(X:T,Γ),!. %(T-Var)
t(Γ,Es,Ts):-is_list(Es),!,maplist(t(Γ),Es,Ts). %(T-Tup)
t(Γ,F$E1,T3):-member(F:(T2->T3),Γ),!,t(Γ,E1,T1),tsub(T1,T2). %(T-App)
t(Γ,def(F$(X:T1) = E2);E3,T3):-!,t([X:T1|Γ],E2,T2),t([F:(T1 -> T2)|Γ],E3,T3). %(T-Dec)
t(Γ,if(X is T1,E2,E3),T):-t(Γ,X,ΓX),!,t2n2(ΓX&T1,ΓXT1),t2n2(ΓX& -T1,ΓXM1),t([X:ΓXT1|Γ],E2,T2),t([X:ΓXM1|Γ],E3,T3),t2n2(T2|T3,T). %(T-If)

ist(V1,T):-t([],V1,T1),tsub(T,T1).
e(_,V,V):-integer(V),!. %(E-Int)
e(Δ,X,V):-member(X:V,Δ),!. %(E-Var)
e(Δ,Es,Vs):-is_list(Es),!,maplist(e(Δ),Es,Vs). %(E-Tup)
e(Δ,F$E1,V):-member(F:((X:_)=E2),Δ),!,e(Δ,E1,V1),e([X:V1],E2,V). %(E-App)
e(Δ,def(F$(X:T1) = E2);E3,T3):-!,e([F:((X:T1) = E2)|Δ],E3,T3). %(E-Dec)
e(Δ,if(E1 is T,E2,E3),V):- e(Δ,E1,V1),(ist(V1,T)->e(Δ,E2,V);e(Δ,E3,V)). %(E-If)

:-begin_tests(t_to_nnf).
  test(int):- t2n(int,int).
  test('-int'):- t2n(-int,-int).
  test('--int'):- t2n(- -int,int).
  test('-(int&int)'):- t2n(-(int&int),-int | -int).
  test('-(int|int)'):- t2n(-(int|int),-int & -int).
:-end_tests(t_to_nnf).
:-begin_tests(nnf_to_dnf).
  test(int):- t2d(int,[[int]]).
  test('-int'):- t2d(-int,[[-int]]).
  test('--int'):- t2d(- -int,[[int]]).
  test('-(int&int)'):- t2d(-(int&int),[[-int],[-int]]).
  test('-(int|int)'):- t2d(-(int|int),[[-int,-int]]).
:-end_tests(nnf_to_dnf).
:-begin_tests('dnf_to_dnf+').
test(xsub):-xsub([[],[]],[],1).
test(int_subcmp_int):-xsubcmp(int,int,=).
test(any_subcmp_int):-xsubcmp([],int,<:).
test(int_subcmp_any):-xsubcmp(int,[],:>).
test(int_cmp_int):-xcmp(int,int,=).
test(any_cmp_int):-xcmp([],int,:>).
test(int_cmp_any):-xcmp(int,[],<:).
test(intint_cmp_any):-xcmp([int,int],[],<:).
test(intint_cmp_int):-xcmp([int,int],int,<:).
test(intint_cmp_intint):-xcmp([int,int],[int,int],=).
test(int_cons_nil):-cons(-int,[],[-int]).
test(int_cons_int_nil):-cons(-int,[-int],[-int]).
test(int_cons_any_nil):-cons(-int,[-[]],[-[]]).
test(any_cons_int_nil):-cons(-[],[-int],[-[]]).
test(any_cons_any_nil):-cons(-[],[-[]],[-[]]).
test(int_cons_intint_nil):-cons(-int,[-[int,int]],[-int,-[int,int]]).
test(nsans1):-nsans([[],int],[],[-[int,int]],[-[int,int]]).
test(nsans2):-nsans([[],int],[-[int,[]]],[],[-[int,int]]).
test(nsans3):-nsans([],[-[[],[]]],[],[-[[],[]]]).
test(aaa):-aaa([[[],int]],[[],-[int,[]]],[[[],int],-[int,int]]).
test(aaa):- \+aaa([[int,int]],[[],-[[],[]]],_).
test(aaa):-aaa([[],-[[],[]]],[[]],[[],-[[],[]]]).
test(int_and_any_2_int):- c2a([int,[]],[int]).
test(intint_and_n_anyany_2_void):- \+c2a([[int,int],-[[],[]]],_).
test(intint_and_n_int_2_intint):- c2a([[int,int],-int],[[int,int]]).
test(anyint_and_n_intany_2_anyint_and_n_intint):-
  c2a([[[],int],-[int,[]]],[[[],int],-[int,int]]).
:-end_tests('dnf_to_dnf+').

:-begin_tests('t_to_dnf+').
  test(int):- t2o2(int,[[int]],int).
  test(any):- t2o2(any,[[[]]],any).
  test('-any'):- t2o2(-any,[],-any).
  test('any & -any'):- t2o2(any& -any,[],-any).
  test('any & -int'):- t2o2(any& -int,[[[],-int]],-int).
  test('-int'):- t2o2(-int,[[[],-int]],-int).
  test('--int'):- t2o2(- -int,[[int]],int).
  test('-(int&int)'):- t2o2(-(int&int),[[[],-int]],-int).
  test('-(int|int)'):- t2o2(-(int|int),[[[],-int]],-int).
:-end_tests('t_to_dnf+').
:-begin_tests(tsub).
  test('int<:int'):-tsub(int,int).
  test('int<:any'):-tsub(int,any).
  test('any<:int'):- \+tsub(any,int).
  test('int<:[int,int]'):- \+tsub(int,[int,int]).
  test('[int,int]<:int'):- \+tsub([int,int],int).
  test('any<:[int,int]'):- \+tsub(any,[int,int]).
  test('[int,int]<:any'):- tsub([int,int],any).
  test('[int,int]<:[int,int]'):- tsub([int,int],[int,int]).
  test('[int,int]<:[any,any]'):- tsub([int,int],[any,any]).
:-end_tests(tsub).
:-begin_tests(t).
  test('1'):- t([],1,int).
  test('1'):- t([x:int],x,int).
  test('1'):- t([f:(int->int)],f$1,int).
  test('1'):- t([],def(f$(x:int)=x);f$1,int).
  test('1'):- t([],def(f$(x:int)=[x,x]);f$1,[int,int]).
  test('1'):- t([],if(1 is int,3,4),int).
:-end_tests(t).
:-begin_tests(e).
  test('1'):- e([],1,1).
  test('1'):- e([x:10],x,10).
  test('1'):- e([f:((y:int)=y)],f$1,1).
  test('1'):- e([],def(f$(x:int)=x);f$1,1).
  test('1'):- e([],def(f$(x:int)=[x,x]);f$1,[1,1]).
  test('1'):- e([],if(1 is int,3,4),3).
:-end_tests(e).

:- run_tests.
:- halt.