occ.pl

% Implementation on Prolog of The Design and Implementation of Typed Scheme 
:- op(1200,xfx,[::=]),op(600,xfx,[∈,<:,:>]).
:- op(990,xfx,[⊢]),op(990,fy,[⊢]).
:- op(250,yf,[*]).
:- op(920, xfx, ['→', '↠']).
:- op(600,yfx,[$]).
G∈(G|_). G∈(_|G2):-G∈G2. G∈G :- G\=(_|_).
bnf(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),bnf(S,A),bnf(S2,Es).
bnf(G,E):-G=..[O|Gs],E=..[O|Es],maplist(bnf,Gs,Es),!.
bnf(G,E):-(G::=Gs),!,G1∈Gs,bnf(G1,E),!.
bnf(n,I):- number(I),!.
bnf(x,I):- atom(I),\+bnf(keywords,I),!.
bnf(G*,Ls) :- maplist(bnf(G),Ls).
hn([G|_]/G,[E|Es]/E,[H|Es]/H).
hn([_|Gs]/G,[E|Es]/E1,[E|Es_]/H):-hn(Gs/G,Es/E1,Es_/H).
h([],E,E,H/H).
h(G,E,V,E_/H):-G=..[O|Gs],E=..[O|Es],hn(Gs/G1,Es/E1,Es_/H_),h(G1,E1,V,H_/H),E_=..[O|Es_].
h(G,E,V,E_/H):-(G::=Gs),G1∈Gs,h(G1,E,V,E_/H).
small(F,G,E,E_):- h(G,E,V,E_/H),call(F,V,H).
all(F)-->call(F),all(F).
all(_)-->!.
reset:- retractall(count(_)),assert(count(0)).
genid(V,A):- retract(count(C)),C1 is C+1,assert(count(C1)),format(atom(A),'~w~w',[V,C]).
mapsubst(_,S,X,V):- atom(X),member(X/V,S),!.
mapsubst(_,_,X,X) :- atom(X),!.
mapsubst(F,S,E,E_) :- call(F,S,E,E_),!.
mapsubst(F,S,E,E_):- E =.. [Op|Es],maplist(mapsubst(F,S),Es,Es_),E_ =.. [Op|Es_].
mapsubstf(F,FV,S,Y,Y2,E,E_) :- call(FV,E,Fs),member(Y,Fs),!,genid(Y,Y2),
                               \+member(Y2,Fs), mapsubst(F,[Y/Y2|S],E,E_).
mapsubstf(F,_,S,_,Y,Y,E,E_) :- mapsubst(F,S,E,E_).
mapfv(_,X,M,M) :- member(X,M),!.
mapfv(_,X,M,[X|M]) :- atom(X),!.
mapfv(F,E,M,M_) :- call(F,E,M,M_),!.
mapfv(F,E,M,M_):- E =.. [_|Es],foldl(mapfv(F),Es,M,M_).
mapfvf(F,X,E,M,M_):- mapfv(F,E,M,M1),subtract(M1,[X],M_).

% 図1. 構文
keywords ::= c | b.
b ::= true | false.
e ::= x | (e $ e) | if(e, e, e) | v.                 % 式
v ::= c | b | n | λ(x : τ,e).                        % 値
c ::= add1 | number | boolean | procedure | not.     % 原始演算
a ::= [] | (a $ e) | (v $ a) | if(a, e, e).          % 評価文脈
φ ::= τ | • .                                        % 潜在述語
ψ ::= (τ$x) | x | true | false | • .                 % 可視述語
τ ::= ⊤ | number | true | false | (τ-φ→τ) | u(τ*).   % 型

% 図7. 操作的意味
(C $ V) → V_          :- bnf(c,C),bnf(v,V),δ(C, V, V_). % E-DELTA
(λ(X : _,E) $ V) → E_ :- bnf(v,V),subst(E,[X/V],E_).    % E-BETA
if(false, _, E3) → E3 :- !.                             % E-IFFALSE
if(V, E2, _) → E2     :- bnf(v,V),V \= false.           % E-IFTRUE

δ(add1, N, N1) :- N1 is N + 1.
δ(not, false, true):- !.
δ(not, _, false).
δ(number, N, true):- number(N),!.
δ(number, _, false).
δ(boolean, B, true):- bnf(b,B),!.
δ(boolean, _, false).
δ(procedure, λ(_ : _, _), true):- !.
δ(procedure, C, true):- bnf(c,C),!.
δ(procedure, _,false).

% 自由変数
fv(E,M):- mapfv(fvf,E,[],M).
fvf(λ(X:_,E)) --> mapfvf(fvf,X,E).
% 代入、置換
substf(S,λ(X:T,E),λ(X_:T,E_)) :- mapsubstf(substf,fv,S,X,X_,E,E_).
subst(E,S,E_):- mapsubst(substf,S,E,E_).

test(E,R) :- reset,bnf(e,E),all(small(→,a),E,R1),!,R=R1.
test(E):- test(E,R),writeln(R).
:- begin_tests(eval).
test(number):- test(1, 1).
test(add1):- test(add1 $ 1, 2).
test(not):- test(not $ false, true).
test(not):- test(not $ true, false).
test(not):- test(not $ 1, false).
test(not):- test(if(not $ 1, 1, 2), 2).
test(if):- test(if(true, 1, 2), 1).
test(if):- test(if(false, 1, 2), 2).
test(number):- test(number $ 1, true).
test(number):- test(number $ true, false).
test(lambda):- test(λ(x:u([true,false]),x),λ(x:u([true,false]),x)).
test(lambda):- test(λ(x:u([true,false]),x)$true,true).
test(lambda):- test(λ(x:u([true,false]),x)$false,false).
test(lambda):- test(λ(x:u([true,false]),not$x)$false,true).
test(lambda):- test(λ(x:u([true,false]),not$x)$true,false).
test(lambda):- test(λ(x:false,λ(y:false,x$y))$λ(y:false,y),λ(y0:false,λ(y:false,y)$y0)).
test(lambda):- test(λ(x:false,λ(y:false,x$y))$λ(y:false,y)$false,false).
test(lambda):- test(λ(x:false,λ(y:false,not$(x$y)))$λ(y:false,y)$false,true).
test(procedure):- test(procedure$add1,true).
test(procedure):- test(procedure$number,true).
test(procedure):- test(procedure$boolean,true).
test(procedure):- test(procedure$procedure,true).
test(procedure):- test(procedure$not,true).
test(procedure):- test(procedure$1,false).
test(procedure):- test(procedure$(add1$1),false).
:- end_tests(eval).


Γ⊢X:T/X:- member(X:T,Γ),!.                                       % T-VAR
_⊢N:number/true:- number(N),!.                                   % T-NUM
_⊢C:T/true:- δτ(C,T),writeln(c:C:T/true),!.                      % T-CONST
_⊢true:u([true,false])/true:- !.                                 % T-TRUE
_⊢false:u([true,false])/false:- !.                               % T-FALSE
Γ⊢λ(X:S,E):(S- • →T)/true:- [X:S|Γ]⊢E:T/_.                       % T-ABS
Γ⊢λ(X:S,E):(S- S_→T)/true:- [X:S|Γ]⊢E:T/(S_$X).                  % T-ABSPRED
Γ⊢(E1$E2):T1/ • :- Γ⊢E1:T_/_, Γ⊢E2:T/_, T<:T0, T_<:(T0-_→T1).    % T-APP
Γ⊢(E1$E2):T1/(S$X):- Γ⊢E1:T_/_, Γ⊢E2:T/X, T<:T0, T_<:(T0-S→T1),  % T-APPPRED
                     bnf(x,X),bnf(τ,S),!.
Γ⊢if(E1,E2,E3):T/P:- Γ⊢E1:_/P1,!,writeln(+(Γ,P1)), +(Γ,P1,Γ2),writeln(b),Γ2⊢E2:T2/P2, -(Γ,P1,Γ3),Γ3⊢E3:T3/P3,
                     T2<:T, T3<:T, combpred(P1, P2, P3, P).       % T-IF

combpred(    _,    P,     P, P):- !.
combpred(  T$X, true,   S$X, T_$X):- u(T,S,T_).
combpred( true,    P,     _, P).
combpred(false,    _,     P, P).
combpred(    P, true, false, P).
combpred(    _,    _,     _, •).
u(T,T,T).
u(u(Ts),u(Ss),u(Ts_)):- union(Ts,Ss,Ts_),!.
u(u(Ts),S,u(Ts_)):- union(Ts,[S],Ts_),!.
u(T,u(Ss),u(Ts_)):- union([T],Ss,Ts_),!.
u(T,S,u(Ts_)):- union([T],[S],Ts_),!.

δτ(add1,      number - • →             number).
δτ(not,       ⊤      - • →             u([true,false])).
δτ(procedure, ⊤      -(⊥ - • → ⊤)→    u([true,false])).
δτ(number,    ⊤      -number→          u([true,false])).
δτ(boolean,   ⊤      -u([true,false])→ u([true,false])).

+(Γ, • , Γ).
+(Γ, T$X, [X:S|Γ]):- member(X:T1,Γ),restrict(T1, T, S).
+(Γ,X, [X:S|Γ]):- member(X:T1,Γ),remove(T1, false, S).
+(Γ, _ , Γ).
-(Γ, • , Γ).
-(Γ,T$X, [X : S|Γ]):- member(X:T1,Γ),remove(T1, T, S).
-(Γ, X , [X : false|Γ]).
-(Γ, _ , Γ).

restrict(S, T, S)       :- S <: T.
restrict(S, u(Ts), u(Ts_)) :- maplist(restrict(S),Ts,Ts_),!.
restrict(_, T, T).
remove(S, T,⊥)         :- S <: T ,!.
remove(S, u(Ts), u(Ts_)) :- maplist(remove(S), Ts, Ts_),!.
remove(S, _, S).

T <: T.                                              % S-REFL
(T1-P→T2)<:(S1-P_→S2) :- S1<:T1, T2<:S2,(P=P_;P_= •).% S-FUN
T <: u(Ss) :- maplist(<:(T),Ss).                     % S-UNIONSUPER
u(Ts) <: S :- maplist(:>(S),Ts).                     % S-UNIONSUB
T :> S :- S <: T.

typing(E,T/P):- []⊢E:T/P,!.
typing(E):- []⊢E:T/P,!,writeln(T/P).

:- begin_tests(typing).
test(number):- typing(1,number/true).
test(bool):- typing(false, u([true,false])/ false).
test(bool):- typing(true, u([true,false])/ true).
test(add1):- typing(add1,(number - • → number)/true).
test(add1):- typing(add1 $ 1,number/ •).
test(not):- typing(not,(⊤ - • → u([true,false]))/true).
test(not):- typing(not $ false, u([true,false])/ •).
test(not):- typing(not $ true, u([true,false])/ •).
test(not):- typing(not $ 1, u([true,false])/ •).
test(not):- typing(if(not $ 1, 1, 2), number/ •).
test(if):- typing(if(true, 1, 2), number/ •).
test(if):- typing(if(false, 1, 2), number/ •).
test(number):- typing(number $ 1, u([true,false])/ •).
test(number):- typing(number $ true, u([true,false])/ •).
test(lambda):- typing(λ(x:u([true,false]),x),(u([true,false]) - • → u([true,false]))/true).
test(lambda):- typing(λ(x:u([true,false]),x)$true,u([true,false])/ •).
test(lambda):- typing(λ(x:u([true,false]),x)$false,u([true,false])/ •).
test(lambda):- typing(λ(x:u([true,false]),not$x)$false,u([true,false])/ •).
test(lambda):- typing(λ(x:u([true,false]),not$x)$true,u([true,false])/ •).
/*
test(lambda):- typing(λ(x:false,λ(y:false,x$y))$λ(y:false,y),λ(y0:false,λ(y:false,y)$y0)).
test(lambda):- typing(λ(x:false,λ(y:false,x$y))$λ(y:false,y)$false,false).
test(lambda):- typing(λ(x:false,λ(y:false,not$(x$y)))$λ(y:false,y)$false,true).
*/
test(procedure):- typing(procedure,(⊤-(⊥- • →⊤)→u([true,false]))/true).
%test(procedure):- typing(procedure$add1,u([true,false])/ true).
/*
test(procedure):- typing(procedure$number,true).
test(procedure):- typing(procedure$boolean,true).
test(procedure):- typing(procedure$procedure,true).
test(procedure):- typing(procedure$not,true).
*/
test(procedure):- typing(procedure$1,u([true,false])/ •).
test(procedure):- typing(procedure$(add1$1),u([true,false])/ •).

:- end_tests(typing).

:- run_tests.
:- halt.