tapl on prolog

FeatherWeightJava.pl

/*
Featherweight Java on Prolog

Featherweight Javaは形式化されたJavaのシンプルなサブセットです。
Featherweight Java on PrologはProlog上のDSLとしてFeatherweight Javaを実装したものです。
Featherweight Java on Prologの構文はProlog上で実装しやすい形に書き換えてあります:

構文

CL ::=                             クラス宣言：
　class C <: C = { [F:C], K, [M] }

K ::=                              コンストラクタ宣言：
　def(this,[F:C] = { super([F]), [this..F=F] })

M ::=                              メソッド宣言：
　def(M, [F:C]:C = {T})

T ::=                              項：
　X                                変数
　T..F                             フィールドアクセス
　T..(M,[T])                       メソッド呼び出し
　new(C,[T])                       オブジェクト生成
　cast(C,T)                        キャスト

V ::=                              値：
　new(C,[V])                       オブジェクト生成
*/

:- initialization(main).
:- op(999, fx, class).
:- op(920, xfx, [ ==>, *==> ]).
:- op(910, xfx, [ ⊢ ]).
:- op(909, yfx, [ => ]).
:- op(501, xfx, <:).
:- op(11, yfx, ..).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).


/*
クラスの宣言(CL)にはクラス名(C)を継承したクラス名があります。
また、フィールド(F)が複数、コンストラクタ(K)が1つ、メソッド(M)が複数あります。
コンストラクタ(K)はメソッドの引数[F:C]がフィールド名とクラス名とのペアが複数で、
スーパークラスのコンストラクタを呼びそのあと、追加分のフィールド設定する必要があります。
メソッド(M)は複数の値を受け取り、式を１つだけかけます。
項(T)は変数や、フィールドアクセス、メソッド呼び出し、
オブジェクト生成、キャストがあるだけです。フィールドの更新はできません。
値(V)はオブジェクト生成時のコンストラクタが値となります。
オリジナルのFetherweight Javaの図では上にバーを振って繰り返しを表現していますが、
テキストに書く場合は[]で括ることにしました。
また、Prologで処理できるように演算子定義をおこない、若干Scalaに近い文法に修正しました。
文法要素は大文字にしました。
*/

% 部分型付け規則 C <: D

% 型のリストが両方とも空なら部分型です
[] <: [].

% リスト内の型の全部が部分型なら部分型です
C <: D, Cs <: Ds
--%----------------
[C|Cs] <: [D|Ds].

% C は C の部分型という式です。
C <: C.

% 全ての型はObjectの部分型です。
_ <: 'Object'.


% CがDの部分型かつDがEの部分型ならCはEの部分型です。
class C <: D ={_}, D <: E
--%----------------------
C <: E.


% フィールドの探索 fields(C, [f:C])

% Objectのフィールドはありません。
fields('Object',[]).

% Cのフィールドはクラステーブルの中身のクラスの中のスーパークラスのフィールドとクラスのフィールドを合わせたものです。

class C <: D = {FCs, _, _},
fields(D, GDs), append(GDs, FCs, FCs_) 
--%-----------------------------------
fields(C, FCs_).

% メソッドの型の探索 mtype(M,C,[C] -> C)

% 補助述語
split([], [], []).
split([X:Y|Ls],[X|Xs],[Y|Ys]) :- split(Ls,Xs,Ys).

% メソッドの型の探索はmtype(メソッド名,クラス名, 型)

% クラステーブルからクラスを取り出し、
% Ms内のメソッドを取得し、
% 引数の型からメソッドのリターンの型になります。

class C <: _ = {_, _, Ms},
member(def(M, Args:B={_}), Ms),
split(Args,_,Bs)
--%-------------------------------------
mtype(M,C,Bs -> B). 

% MがMsの中になかった場合は、スーパークラスを検索する
class C <: D = {_}, mtype(M,D,T)
--%-------------------------------------
mtype(M,C,T).


% メソッドの本体の探索 mbody(M,C,([X],T))

% 型の代わりにメソッドの本体の引数と式のペアを返す
class C <: _ = {_, _, Ms},
member(def(M, Args:_ = {T}), Ms),
split(Args,Xs,_)
--%-------------------------------------
mbody(M, C, (Xs,T)).

class C <: D = {_}, mbody(M,D,T)
--%-------------------------------------
mbody(M,C,T).


% メソッドの正当なオーバーライド override(M, D, [C]->C0)
% ただしく、オーバーライドされているかどうかはoverrideで判定できます。

\+ mtype(M, D, _)
--%-------------------------------------
override(M, D, _ -> _).

mtype(M,D,Ds->D0), Cs = Ds, C0 = D0
--%-------------------------------------
override(M, D, Cs -> C0).

% 項の型付け Γ ⊢ T : C

atom(X),
log('T-Var':X),
member(X : C, Γ),
log('T-Var End'),!
--%------------------------------------- (T-Var)
Γ ⊢ X : C.

log('T-Field'),
Γ ⊢ T0 : C0, fields(C0, FCs),
member(Fi:Ci,FCs),!
--%------------------------------------- (T-Field)
Γ ⊢ T0..Fi : Ci.

log('T-Invk'),
Γ ⊢ T0 : C0,
mtype(M, C0, Ds -> C),
Γ ⊢ Ts : Cs, Cs <: Ds,!
--%------------------------------------- (T-Invk)
Γ ⊢ T0..(M, Ts) : C.

log('T-New'),
fields(C, FDs),
Γ ⊢ Ts : Cs, split(FDs, _, Ds), log("check subtyping"=Cs <: Ds), Cs <: Ds,
log('T-New':C),!
--%------------------------------------- (T-New)
Γ ⊢ new(C, Ts) : C.

log('T-UCast'),
Γ ⊢ T0 : D, D <: C,!
--%------------------------------------- (T-UCast)
Γ ⊢ cast(C, T0) : C.

log('T-DCast'),
Γ ⊢ T0 : D, C <: D, C \= D,!
--%------------------------------------- (T-DCast)
Γ ⊢ cast(C, T0) : C.

log('T-SCast'),
Γ ⊢ T0 : D, \+ C <: D, \+ C <: D,
format('愚かさの警告 ~w と ~w はキャストできません\n',[C,D]),!
--%------------------------------------- (T-SCast)
Γ ⊢ cast(C, T0) : C.

!
--%------------------------------------- (T-List0)
_ ⊢ [] : [].

log('T-List1'=[T|Ts]),
Γ ⊢ T : C, Γ ⊢ Ts : Cs,
log('T-List1 End':[C|Cs]),!
--%------------------------------------- (T-List1)
Γ ⊢ [T|Ts] : [C|Cs].

% メソッドの型付け okas(C, M)

[this:C|Args] ⊢ T0:E0, E0 <: C0,
class C <: D = {_},
split(Args,_,Cs),override(M,D,Cs->C0)
--%-------------------------------------
okas(C, def(M, Args:C0 = {T0})).

% クラスの型付け ok(C)

thisffs(this..F = F).


K= def(this,Args = { super(Gs), ThisFFs }),
maplist(thisffs,ThisFFs),
fields(D,GDs),split(GDs,Gs,_),
append(GDs,FCs,Args),maplist(okas(C), Ms),!
--%-------------------------------------
ok(class C <: D = {FCs, K, Ms}).

ok1(Class) :- ok(Class),!; Class=(class C <: _ = _), format('error class ~W\n',[C,[]]),fail.

okall :-
	findall(class C,class C,Cs),!,maplist(ok1,Cs),!.

% 置き換え

subst(S->D,S->D) :- atom(S).
subst([]->[],T->T).
subst([S|Ss]->[D|Ds],T->T_) :- subst(S->D,T->T1), subst(Ss->Ds,T1->T_).
subst(_->_,X->X) :- atom(X).
subst(_->_,[]->[]).
subst(S->D,[X|Xs]->[X_|Xs_]) :- subst(S->D,X->X_), subst(S->D,Xs->Xs_).
subst(S->D,(T..(M,Ts))->(T_..(M,Ts_))) :- subst(S->D,T->T_),subst(S->D,Ts->Ts_).
subst(S->D,(T..F)->(T_..F)) :- subst(S->D,T->T_).
subst(S->D,new(C,Ts)->new(C,Ts_)) :- subst(S->D,Ts->Ts_).
subst(S->D,cast(C,T)->cast(C,T_)) :- subst(S->D,T->T_).
isVal(new(C,Vs)) :- atom(C),isVals(Vs).
isVals(Vs) :- maplist(isVal, Vs).

% 値と項を分離する
splitVals([],[],[]).
splitVals([V|Ts],[V|Vs],Ts_) :- isVal(V), splitVals(Ts,Vs,Ts_).
splitVals(Ts,[],Ts).

% 評価 T ==> T_

isVals(Vs),atom(Fi),fields(C,FCs),
nth0(I,FCs,(Fi:_)),nth0(I,Vs,Vi),!
--%------------------------------------- (E-ProjNew)
new(C, Vs)..Fi ==> Vi.

isVals(Vs),atom(M),mbody(M,C,(Xs, T0)),
subst([this|Xs]->[new(C,Vs)|Us], T0 -> T0_),!
--%------------------------------------- (E-InvkNew)
new(C,Vs)..(M,Us) ==> T0_.

isVals(Vs), C <: D,!
--%------------------------------------- (E-CastNew)
cast(D, new(C, Vs)) ==> new(C, Vs).

atom(F), T0 ==> T0_,!
--%------------------------------------- (E-Field)
T0..F ==> T0_..F.

atom(M), T0 ==> T0_,!
--%------------------------------------- (E-Invk-Recv)
T0..(M,Ts) ==> T0_..(M,Ts).

atom(M), splitVals(Args,Vs,[Ti|Ts]),
Ti ==> Ti_,
append(Vs,[Ti_|Ts],Args_),!
--%------------------------------------- (E-Invk-Arg)
V0..(M,Args) ==> V0..(M,Args_).

atom(C), splitVals(Args,Vs,[Ti|Ts]),
Ti ==> Ti_,
append(Vs,[Ti_|Ts],Args_),!
--%------------------------------------- (E-New-Arg)
new(C,Args) ==> new(C,Args_).

atom(C), T0 ==> T0_,!
--%------------------------------------- (E-Cast)
cast(C, T0) ==> cast(C, T0_).

E1 *==> E3 :- E1 ==> E2,!, E2 *==> E3.
E1 *==> E1.

% クラス定義

class 'B' <: 'Object' = {[],def(this,[]={super([]),[]}),[]}.
class 'C' <: 'Object' = {[],def(this,[]={super([]),[]}),[]}.
class 'A' <: 'B' = {[],def(this,[]={super([]),[]}),[]}.
class 'Pair' <: 'B' = {
	[fst:'B',snd:'B'],
	def(this,[fst:'B',snd:'B']={
		super([]),[this..fst=fst,this..snd=snd]
	}),
	[
		def(getFst,[]:'B' = {
			this..fst
		}),
		def(setFst,[fst:'B']:'Pair' = {
			new('Pair',[fst,this..snd])
		}),
		def(setSnd,[snd:'B']:'Pair' = {
			new('Pair',[this..fst,snd])
		})
	]
}.
class 'Triple' <: 'Pair' = {
	[thr:'B'],
	def(this,[fst:'B',snd:'B',thr:'B']={
		super([fst,snd]),[this..thr=thr]
	}),
	[
		def(setFst,[fst:'B']:'Pair' = {
			new('Triple',[fst,this..snd,this..thr])
		})
	]
}.

log(_).
%log(A) :- writeln(A).

test(E) :-
  
  ([] ⊢ E : T,!, format('~W : ~W = ',[E,[],T,[]]);format('~W : type error\n',[E,[]]),fail),
  (E *==> V, writeln(V),isVal(V); writeln('runtime error'));!.

main :- (okall,writeln('all classes valid.'); writeln('invalid classess.'),halt),
  test(new('Pair',[new('A',[]),new('B',[])])..fst),
  test(new('Pair',[new('Pair',[new('A',[]),new('B',[])])..snd,new('B',[])])..fst),
  test(new('Pair',[new('A',[]),new('B',[])])..(getFst,[])),
  test(new('Pair',[new('A',[]),new('B',[])])..(setFst,[new('B',[])])),
  test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])..(getFst,[])),
  test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])..(setFst,[new('B',[])])),
  test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])..(setSnd,[new('A',[])])),
  test(cast('Object',new('Object',[]))),
  test(cast('Pair',new('Object',[]))..fst),
  test(cast('C',new('C',[]))),
  test(cast('A',new('B',[]))),
  test(cast('B',new('A',[]))),
  test(cast('C',new('B',[]))), % warning
  test(new('Pair',[new('Pair',[new('A',[]),new('B',[])]),new('B',[])])..fst..fst),
  test(cast('Pair',new('Pair',[new('Pair',[new('A',[]),new('B',[])]),new('B',[])])..fst)..fst),

  halt.

fsimplebool.pl

/*
構文

t ::=                項：
　x                  変数
　λx:T.t            ラムダ抽象
　t t                関数適用
　true               定数真
　false              定数偽
　if t then t else t 条件式
　λX.t              型抽象 [new]
　t[T]               型適用 [new]

v ::=                値：
　λx:T.t            ラムダ抽象値
　true               定数真
　false              定数偽
　λX.t              型抽象値 [new]

T ::=                型：
　T->T               関数の型
　Bool               ブール値型
　X                  型変数 [new]
　∀X.T              全称型 [new]
Γ ::=               文脈：
　∅                  空の文脈
　Γ,x:T             項変数の束縛
　Γ,X               型変数の束縛 [new]
*/

:- initialization(main).
:- style_check(-singleton).
:- op(920, xfx, [ ==>, *==> ]).
:- op(910, xfx, [ ⊢ ]).
:- op(901, xfx, [∈]).
:- op(900, xfx, [ : ]).
:- op(892, xfy, [ then, else ]).
:- op(890, fx, [ letrec, let, if ]).
:- op(500, yfx, [$,$$]).
:- op(10, fx, [λ,∀]).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

isVal(λ _ : _ -> _).
isVal(λ _ -> _).
isVal(true). isVal(false).

subst(X1->V1,X1->V1).
subst(X1->V1,(T2$T3)->(T2_$T3_)) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 : T -> T2)->(λ X1 : T -> T2)).
subst(X1->V1,(λ X2 : T -> T2)->(λ X2 : T -> T2_)) :- subst(X1->V1, T2->T2_).
subst(X1->V1,(if T1 then T2 else T3)->(if T1_ then T2_ else T3_)) :- subst(X1->V1, T1->T1_),subst(X1->V1, T2->T2_),subst(X1->V1, T3->T3_).
subst(X1->V1,(T2$$[T3])->(T2_$$[T3_])) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 -> T2)->(λ X1 -> T2)).
subst(X1->V1,(λ X2 -> T2)->(λ X2 -> T2_)) :- subst(X1->V1, T2->T2_).
subst(_->_,T1->T1).

% 評価 E ==> E_

E1 ==> E1_
--%-------------------------------------- (E-App1)
E1 $ E2 ==> E1_ $ E2.

isVal(V1), E2 ==> E2_
--%-------------------------------------- (E-App2)
V1 $ E2 ==> V1 $ E2_.

isVal(V2), subst(X->V2,E12->E12_)
--%-------------------------------------- (E-AppAbs)
(λ X : T11 -> E12) $ V2 ==> E12_.

(if true then T2 else _) ==> T2.        % (E-IfTrue)

(if false then _ else T3) ==> T3.       % (E-IfFalse)

E1 ==> E1_
--%-------------------------------------- (E-TApp)[new]
E1 $$ [T2] ==> E1_ $$ [T2].

subst(TX->T2, E12->E12_)
--%-------------------------------------- (E-TAppTAbs)[new]
(λ TX -> E12) $$ [T2] ==> E12_.

% 型付け Γ ⊢ t : T

X : T ∈ (Γ,(X:T)).
X : T ∈ (Γ,(X1:_)) :- X : T ∈ Γ.

X : T ∈ Γ
--%-------------------------------------- (T-Var)
Γ ⊢ X : T.

(Γ , (X : T1)) ⊢ E2 : T2
--%-------------------------------------- (T-Abs)
Γ ⊢ (λ X : T1 -> E2) : (T1 -> T2).

Γ ⊢ E1 : (T11 -> T12), Γ ⊢ E2 : T11
--%-------------------------------------- (T-App)
Γ ⊢ E1 $ E2 : T12.

Γ ⊢ true : bool.                       % (T-True)

Γ ⊢ false : bool.                      % (T-False)

Γ ⊢ E1 : bool, Γ ⊢ E2 : T, Γ ⊢ E3 : T
--%-------------------------------------- (T-If)
Γ ⊢ if E1 then E2 else E3 : T.

(Γ,TX) ⊢ E2 : T2
--%-------------------------------------- (T-TAbs)
Γ ⊢ (λ TX -> E2) : (∀ TX -> T2).

Γ ⊢ E1 : (∀ X -> T12),
subst(X->T2,T12->T12_)
--%-------------------------------------- (T-TApp)
Γ ⊢ (E1 $$ [T2]) : T12_.


E1 *==> E3 :- E1 ==> E2, E2 *==> E3.
E1 *==> E1.

test(E:T=R) :-
  write(E),write(" : "),!,
  [] ⊢ E : T,
  write(T), write(" = "),!,
  T *==> R,
  writeln(R),!.

test_system_f :-
  writeln("test system f"),
  test((λ 'X' -> λ x:'X'-> x):(∀'X'->'X'->'X')=(∀'X'->'X'->'X')),
  test(((λ 'X'-> λ x:'X'-> x) $$ [∀ 'X'->'X'->'X']):('X'->'X')=('X'->'X')),
  !.

main :-
  (λ x : bool -> x) $ true *==> E1, write(E1), nl,!, 
  (λ x : bool -> ((λ z : bool -> z) $ x)) $ true *==> E2, write(E2), nl,!, 
  (λ x : bool -> x) *==> E3, write(E3), nl,E3=(λ x:bool -> x),!, 
  (if true then false else true) *==> E4, write(E4),nl, E4=false,!,
  (if false then false else true) *==> E5, write(E5),nl, E5=true,!,
  [] ⊢ true : T0, write(T0), nl,!, T0=bool,
  [] ⊢ (λ x : bool -> x) $ true : T1, write(T1), nl,!, T1=bool,
  [] ⊢ (λ x : bool -> ((λ z : bool -> z) $ x)) $ true : T2, write(T2), nl,!, T2=bool,
  [] ⊢ (λ x : bool -> x) : T3, write(T3), nl,!, T3=(bool->bool),
  [] ⊢ (if true then false else true) : T4, write(T4),nl, T4=bool,!,
  [] ⊢ (if false then false else true) : T5, write(T5),nl, T5=bool,!,
  test_system_f,
  halt.

fsimpleboolsub.pl

/*
構文

t ::=                項：
　x                  変数
　λx<:T.t           ラムダ抽象[up]
　t t                関数適用
　true               定数真
　false              定数偽
　if t then t else t 条件式
　λX.t              型抽象
　t[T]               型適用

v ::=                値：
　λx<:T.t           ラムダ抽象値[up]
　true               定数真
　false              定数偽
　λX.t              型抽象値

T ::=                型：
　T->T               関数の型
　Bool               ブール値型
　X                  型変数
　∀X<:.T            全称型[up]
Γ ::=               文脈：
　∅                  空の文脈
　Γ,x:T             項変数の束縛
　Γ,X<:T            型変数の束縛[up]
*/

:- initialization(main).
:- style_check(-singleton).
:- op(920, xfx, [ ==>, *==> ]).
:- op(910, xfx, [ ⊢ ]).
:- op(901, xfx, [∈]).
:- op(900, xfx, [ :, <: ]).
:- op(892, xfy, [ then, else ]).
:- op(890, fx, [ letrec, let, if ]).
:- op(500, yfx, [$,$$]).
:- op(10, fx, [λ,∀]).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

isVal(λ _ : _ -> _).
isVal(λ _ -> _).
isVal(true). isVal(false).

subst(X1->V1,X1->V1).
subst(X1->V1,(T2$T3)->(T2_$T3_)) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 : T -> T2)->(λ X1 : T -> T2)).
subst(X1->V1,(λ X2 : T -> T2)->(λ X2 : T -> T2_)) :- subst(X1->V1, T2->T2_).
subst(X1->V1,(if T1 then T2 else T3)->(if T1_ then T2_ else T3_)) :- subst(X1->V1, T1->T1_),subst(X1->V1, T2->T2_),subst(X1->V1, T3->T3_).
subst(X1->V1,(T2$$[T3])->(T2_$$[T3_])) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 <: T1 -> T2)->(λ X1 <: T1 -> T2)). %[up]
subst(X1->V1,(λ X2 <: T1 -> T2)->(λ X2 <: T1 -> T2_)) :- subst(X1->V1, T2->T2_). %[up]
subst(_->_,T1->T1).

% 評価 E ==> E_

E1 ==> E1_
--%-------------------------------------- (E-App1)
E1 $ E2 ==> E1_ $ E2.

isVal(V1), E2 ==> E2_
--%-------------------------------------- (E-App2)
V1 $ E2 ==> V1 $ E2_.

isVal(V2), subst(X->V2,E12->E12_)
--%-------------------------------------- (E-AppAbs)
(λ X : T11 -> E12) $ V2 ==> E12_.

(if true then T2 else _) ==> T2.        % (E-IfTrue)

(if false then _ else T3) ==> T3.       % (E-IfFalse)

E1 ==> E1_
--%-------------------------------------- (E-TApp)
E1 $$ [T2] ==> E1_ $$ [T2].

subst(TX->T2, E12->E12_)
--%-------------------------------------- (E-TAppTAbs)[up]
(λ TX<:T11 -> E12) $$ [T2] ==> E12_.


X : T ∈ (Γ,(X:T)).
X : T ∈ (Γ,(X1:_)) :- X : T ∈ Γ.
X <: T ∈ (Γ,(X:T1)) :- X <: T1. % [new]
X <: T ∈ (Γ,(X1:_)) :- X1 \= X, X <: T ∈ Γ. % [new]

% 部分型付け S <: T

Γ ⊢ S <: S.                 % (S-Refl) [up]
Γ ⊢ _ <: top.               % (S-Top) [up]

Γ ⊢ S <: U, Γ ⊢ U <: T
--%---------------------- (S-Trans) [up]
Γ ⊢ S <: T.

X <: T ∈ Γ
--%---------------------- (S-TVar) [new]
Γ ⊢ X <: T.

Γ ⊢ T1 <: S1, Γ ⊢ S2 <: T2
--%---------------------- (S-Arrow) [up]
Γ ⊢ (S1 -> S2) <: (T1 -> T2).

(Γ, X <: U1) ⊢ S2 <: T2
--%---------------------- (S-All) [new]
Γ ⊢ (∀ X<:U1->S2) <: (∀ X<:U1->T2).

% 型付け Γ ⊢ t : T

X : T ∈ Γ
--%-------------------------------------- (T-Var)
Γ ⊢ X : T.

(Γ , (X : T1)) ⊢ E2 : T2
--%-------------------------------------- (T-Abs)
Γ ⊢ (λ X : T1 -> E2) : (T1 -> T2).

Γ ⊢ E1 : (T11 -> T12), Γ ⊢ E2 : T11
--%-------------------------------------- (T-App)
Γ ⊢ E1 $ E2 : T12.

Γ ⊢ true : bool.                       % (T-True)

Γ ⊢ false : bool.                      % (T-False)

Γ ⊢ E1 : bool, Γ ⊢ E2 : T, Γ ⊢ E3 : T
--%-------------------------------------- (T-If)
Γ ⊢ if E1 then E2 else E3 : T.

(Γ,TX) ⊢ E2 : T2
--%-------------------------------------- (T-TAbs)[up]
Γ ⊢ (λ TX -> E2) : (∀ TX -> T2).

Γ ⊢ E1 : (∀ X -> T12),
subst(X->T2,T12->T12_)
--%-------------------------------------- (T-TApp)[up]
Γ ⊢ (E1 $$ [T2]) : T12_.

Γ ⊢ E : S, Γ ⊢ S <: T
--%-------------------------------------- (T-Sub)[up]
Γ ⊢ E : T.

E1 *==> E3 :- E1 ==> E2, E2 *==> E3.
E1 *==> E1.

test(E:T=R) :-
  write(E),write(" : "),!,
  [] ⊢ E : T,
  write(T), write(" = "),!,
  T *==> R,
  writeln(R),!.

test_system_f :-
  writeln("test system f"),
  test((λ 'X' -> λ x:'X'-> x):(∀'X'->'X'->'X')=(∀'X'->'X'->'X')),
  test(((λ 'X'-> λ x:'X'-> x) $$ [∀ 'X'->'X'->'X']):('X'->'X')=('X'->'X')),
  !.

main :-
  (λ x : bool -> x) $ true *==> E1, write(E1), nl,!, 
  (λ x : bool -> ((λ z : bool -> z) $ x)) $ true *==> E2, write(E2), nl,!, 
  (λ x : bool -> x) *==> E3, write(E3), nl,E3=(λ x:bool -> x),!, 
  (if true then false else true) *==> E4, write(E4),nl, E4=false,!,
  (if false then false else true) *==> E5, write(E5),nl, E5=true,!,
  [] ⊢ true : T0, write(T0), nl,!, T0=bool,
  [] ⊢ (λ x : bool -> x) $ true : T1, write(T1), nl,!, T1=bool,
  [] ⊢ (λ x : bool -> ((λ z : bool -> z) $ x)) $ true : T2, write(T2), nl,!, T2=bool,
  [] ⊢ (λ x : bool -> x) : T3, write(T3), nl,!, T3=(bool->bool),
  [] ⊢ (if true then false else true) : T4, write(T4),nl, T4=bool,!,
  [] ⊢ (if false then false else true) : T5, write(T5),nl, T5=bool,!,
  test_system_f,
  halt.

fulluntyped.pl

:- initialization(main).
:- op(920, xfx, [ ==>, *==> ]).
:- op(900, xfx, [ in ]).
:- op(500, yfx, $).
:- op(11, yfx, ..).
:- op(10, fx, λ).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

isVal(λ _ -> _).
isVal(X) :- isNumericValue(X).
% isVal({V1,V2}) :- isVal(V1), isVal(V2).
isVal(T) :- isTupleVal(T).
isVal(T) :- isRcdVal(T).

isTupleVal(T) :- T =.. ['{}', T2], isTupleVal2(T2).
isTupleVal2(T) :- isVal(T).
isTupleVal2((T1,T2)) :- isVal(T1),isTupleVal2(T2).

getTupleVal(T..N->Vn) :- T =.. ['{}', T2], getTupleVal2(T2..N->Vn).
getTupleVal2((T,_)..1->T).
getTupleVal2(T..1->T).
getTupleVal2((_,T)..N->Vn) :- N > 1, N_ is N - 1, getTupleVal2(T..N_->Vn).

substTuple(T->T_) :- T =.. ['{}', T2], substTuple2(T2->T2_), T_ =.. ['{}', T2_].
substTuple2(T->T_) :- \+ isVal(T), T ==> T_.
substTuple2((T,T2)->(T,T2_)) :- isVal(T), substTuple2(T2->T2_).
substTuple2((T,T2)->(T_,T2)) :- T ==> T_.

isRcdVal(T) :- T =.. ['{}', T2], isRcdVal2(T2).
isRcdVal2(L=T) :- atom(L),isVal(T).
isRcdVal2((L1=T1,T2)) :- atom(L1),isVal(T1),isRcdVal2(T2).

getRcdVal(T..L->Vn) :- T =.. ['{}', T2], getRcdVal2(T2..L->Vn).
getRcdVal2((L=T,_)..L->T).
getRcdVal2((L=T)..L->T).
getRcdVal2((_,T)..L->Vn) :- getRcdVal2(T..L->Vn).

substRcd(T->T_) :- T =.. ['{}', T2], substRcd2(T2->T2_), T_ =.. ['{}', T2_].
substRcd2((L=T)->(L=T_)) :- \+ isVal(T), T ==> T_.
substRcd2(((L=T),T2)->((L=T),T2_)) :- isVal(T), substRcd2(T2->T2_).
substRcd2(((L=T),T2)->((L=T_),T2)) :- T ==> T_.

matchRcd(X1->V1,T->T_) :- X1 =.. ['{}', X1_], matchRcd2(X1_->V1,T->T_).
matchRcd2((L=P)->T,T2->T2_) :- getRcdVal(T..L->T_), match(P->T_, T2->T2_).
matchRcd2(((L=P),T1)->T, T2->T2_) :- getRcdVal(T..L->T_), match(P->T_, T2->T21), matchRcd2(T1->T, T21->T2_).

subst(X1->V1,X1->V1).
subst(X1->V1,(T2$T3)->(T2_$T3_)) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 -> T2)->(λ X1 -> T2)).
subst(X1->V1,(λ X2 -> T2)->(λ X2 -> T2_)) :- subst(X1->V1, T2->T2_).
subst(X1->V1,succ(T1)->succ(T1_)) :- subst(X1->V1, T1->T1_).
subst(X1->V1,pred(T1)->pred(T1_)) :- subst(X1->V1, T1->T1_).
subst(X1->V1,iszero(T1)->iszero(T1_)) :- subst(X1->V1, T1->T1_).
subst(X1->V1,if(T1,T2,T3)->if(T1_,T2_,T3_)) :- subst(X1->V1, T1->T1_),subst(X1->V1, T2->T2_),subst(X1->V1, T3->T3_).
subst(_->_,T1->T1).

atom(X1), subst(X1->V1,T1->T1_)
--%-------------------------------- (M-Var)
match(X1->V1,T1->T1_).

isRcdVal(V1), matchRcd(X1->V1,T1->T1_)
--%-------------------------------- (M-Rcd)
match(X1->V1,T1->T1_).

isVal(V2), subst(X->V2, T12->T12_)
--%-------------------------------- (E-AppAbs)
(λ X -> T12) $ V2 ==> T12_.

T1 ==> T1_
--%-------------------------------- (E-App1)
T1 $ T2 ==> T1_ $ T2.

isVal(V1), T2 ==> T2_
--%-------------------------------- (E-App2)
V1 $ T2 ==> V1 $ T2_.

if(true, T2,_) ==> T2.            % (E-IfTrue)
if(false,_,T3) ==> T3.            % (E-IfFalse)

T1 ==> T1_
--%-------------------------------- (E-If)
if(T1,T2,T3) ==> if(T1_,T2,T3).

T1 ==> T1_
--%-------------------------------- (E-Succ)
succ(T1) ==> succ(T1_).

pred(0) ==> 0.                    % (E-PredZero)
pred(succ(NV1)) ==> NV1.          % (E-PredSucc)

T1 ==> T1_
--%-------------------------------- (E-Pred)
pred(T1) ==> pred(T1_).

iszero(0) ==> true.               % (E-IsZeroZero)

isNumericValue(NV1)
--%-------------------------------- (E-IsZeroSucc)
iszero(succ(NV1)) ==> false.

isVal(V1), match(X->V1, T2->T2_)
--%-------------------------------- (E-LetV)
let(X=V1 in T2) ==> T2_.

T1 ==> T1_
--%-------------------------------- (E-Let)
let(P=T1 in T2) ==> let(P=T1_ in T2).

T1 ==> T1_
--%-------------------------------- (E-Zero)
iszero(T1) ==> iszero(T1_).

/*
isVal(V1),isVal(V2)
--%-------------------------------- (E-PairBeta1)
{V1,V2} .. 1 ==> V1.

isVal(V1),isVal(V2)
--%-------------------------------- (E-PairBeta2)
{V1,V2} .. 2 ==> V2.

T1 ==> T1_
--%-------------------------------- (E-Proj1)
T1 .. 1 ==> T1_ .. 1.

T1 ==> T1_
--%-------------------------------- (E-Proj2)
T1 .. 2 ==> T1_ .. 2.

isVal(V1), T2 ==> T2_
--%-------------------------------- (E-Pair2)
{V1,T2} ==> {V1,T2_}.

T1 ==> T1_
--%-------------------------------- (E-Pair1)
{T1,T2} ==> {T1_,T2}.
*/

atom(L), isRcdVal(T), getRcdVal(T..L->V)
--%-------------------------------- (E-ProjRcd)
T .. L ==> V.

atom(L), T ==> T_
--%-------------------------------- (E-Proj)
T .. L ==> T_ .. L.

substRcd(T->T_)
--%-------------------------------- (E-Rcd)
T ==> T_.

I > 0, isTupleVal(T), getTupleVal(T..I->Vn) 
--%-------------------------------- (E-ProjTuple)
T .. I ==> Vn.

I > 0, T ==> T_
--%-------------------------------- (E-Proj)
T .. I ==> T_ .. I.

substTuple(T->T_)
--%-------------------------------- (E-Tuple)
T ==> T_.

isNumericValue(0).
isNumericValue(succ(NV1)) :- isNumericValue(NV1).

toInt(0,0).
toInt(succ(NV),I) :- toInt(NV, I1), I is I1 + 1.

writeValue(NV) :- toInt(NV, I), write(I).
writeValue(V) :- write(V).

T1 *==> T3 :- T1 ==> T2, T2 *==> T3.
T1 *==> T1.

main :-
  true *==> T1, write(T1),nl,!,
  false *==> T2, write(T2),nl,!,
  if(if(true,false,true),false,true) *==> T3, write(T3),nl,!,
  pred(0) *==> T4, write(T4),nl,!,
  succ(0) *==> T5, write(T5),nl,!,
  succ(0) *==> T6, writeValue(T6),nl,!,
  succ(succ(0)) *==> T7, writeValue(T7),nl,!,
  succ(succ(succ(0))) *==> T8, writeValue(T8),nl,!,
  (λ x -> x) $ (λ y -> y) *==> V1, write(V1), nl,V1=(λ y -> y),!,
  (λ x -> ((λ z -> z) $ x)) $ (λ k -> x) *==> V2, write(V2), nl,!,
  (λ x -> x) *==> V3, write(V3), nl,V3=(λ x -> x),!,
  (λ x -> succ(x)) $ 0 *==> V4, write(V4), nl,!,
  (λ x -> succ(succ(x))) $ 0 *==> V5, write(V5), nl,!,
  (λ x -> pred(succ(x))) $ 0 *==> V6, write(V6), nl,!,
  (λ x -> pred(x)) $ succ(succ(0)) *==> V7, write(V7), nl,!,
  let(x=succ(succ(0)) in pred(x)) *==> V8, write(V8), nl, !,
  {let(x=succ(succ(0)) in pred(x)),0} .. 1 *==> V9, write(V9),nl,!,
  {0,let(x=succ(succ(0)) in pred(x))} .. 2 *==> VA, write(VA),nl,!,
  (isVal({}),write(ok);write(ng)),nl,!,
  (isVal({0}),write(ok);write(ng)),nl,!,
  (isVal({0,succ(0)}),write(ok);write(ng)),nl,!,
  (isVal({0,succ(0),succ(succ(0))}),write(ok);write(ng)),nl,!,
  {0}..1 *==> VB, write(VB),nl,!,
  {0,succ(0)}..1 *==> VC, write(VC),nl,!,
  {0,succ(0)}..2 *==> VD, write(VD),nl,!,
  {0,succ(0),succ(succ(0))}..3 *==> VE, write(VE),nl,!,
  {pred(succ(0))}..1 *==> VF, write(VF),nl,!,
  {pred(succ(0)),pred(succ(0))}..1 *==> VG, write(VG),nl,!,
  {pred(succ(0)),pred(succ(succ(0)))}..2 *==> VH, write(VH),nl,!,
  {hoge=succ(0)}..hoge *==> VJ, write(VJ),nl,!,
  {hoge=succ(0),fuga=0}..hoge *==> VK, write(VK),nl,!,
  {hoge=succ(0),fuga=0}..fuga *==> VM, write(VM),nl,!,
  {hoge=pred(succ(0)),fuga=pred(succ(succ(0)))} *==> VN, write(VN),nl,!,
  let({x=p}={x=succ(succ(0))} in p) *==> VO, write(VO), nl, !,
  let({x=p}={y=0,x=succ(succ(0))} in p) *==> VO, write(VO), nl, !,
  let({y=p}={y=succ(succ(0)),x=0} in p) *==> VO, write(VO), nl, !,
  let({x=p,y=p2}={y=0,x=succ(succ(0))} in p) *==> VO, write(VO), nl, !,
  let({x=p,y=p2}={y=0,x=succ(succ(0))} in p2) *==> 0, write(0), nl, !,
  let({x={z=p}}={y=0,x={z=succ(succ(0))}} in p) *==> VO, write(VO), nl, !,
  halt.

rcdsubbot.pl

:- initialization(main).
:- op(11, yfx, ..).
:- op(910, xfx, [ ⊢ ]).
:- op(901, xfx, [∈]).
%:- op(900, xfx, [ : ]).
:- op(501, xfx, <:).
:- op(500, yfx, $).
:- op(11, yfx, ..).
:- op(10, fx, λ).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

maptpl(F,(A,B)) :- call(F,A), maptpl(F,B).
maptpl(F,A) :- call(F,A).
maprcd(F,R) :- R =..[_,T], maptpl(F,T).
maptpl(F,(A,B),(A_,B_)) :- call(F,A,A_), maptpl(F,B,B_).
maptpl(F,A,A_) :- call(F,A,A_).
maprcd(F,R,R_) :- R =..[Op,T], maptpl(F,T,T_), R_ =..[Op,T_].
membertpl(X,(X,_)).
membertpl(X,(_,B)) :- membertpl(X,B).
membertpl(X,X).
memberrcd(X,R) :- R =..[_,T],membertpl(X,T).

isVal(I) :- integer(I).
isVal(true). isVal(false).
isVal(V) :- isRcdVal(V).
isVal(λ _ -> _).
isRcdVal(T) :- maprcd(isRcdVal1, T).
isRcdVal1(L=T) :- atom(L), isVal(T).

T <: T.
_ <: top.
bot <: _.
(S1->S2) <: (T1->T2) :- S1 <: T1, S2 <: T2.
S <: T :- maprcd(subtypercd1(S), T).
subtypercd1(S, (L:T)) :- memberrcd(L:S1,S), S1 <: T.

X ∈ (_,X).
X ∈ (Γ,_) :- X ∈ Γ.

X : T ∈ Γ
--%-------------------------------------- (TA-Var)
Γ ⊢ (X : T).

(Γ , X : T1) ⊢ E2 : T2
--%-------------------------------------- (TA-Abs)
Γ ⊢ (λ (X : T1) -> E2) : (T1 -> T2).

Γ ⊢ E1 : bot, Γ ⊢ E2 : _
--%-------------------------------------- (TA-AppBot)
Γ ⊢ E1 $ E2 : bot.

Γ ⊢ E1 : (T11 -> T12),
Γ ⊢ E2 : T2, T2 <: T11
--%-------------------------------------- (TA-App)
Γ ⊢ E1 $ E2 : T12.

Γ ⊢ E1 : R1, memberrcd(Li:Ti,R1)
--%-------------------------------------- (TA-Proj)
Γ ⊢ E1..Li : Ti.

maprcd(taRcd1(Γ),E1,T1)
--%-------------------------------------- (TA-Rcd)
Γ ⊢ E1 : T1.

taRcd1(Γ,Li=Ei,Li:Ti) :- Γ ⊢ Ei : Ti.
typeof(E1:T1) :- [] ⊢ E1 : T1.

testSubtype :-
  {a:bool,b:int,c:int} <: {b:int,a:bool},!,
  {a:bool,b:int} <: {b:int,a:bool},!,
  \+ ({a:bool} <: {b:int,a:bool}),!,
  \+ ({a:bool,b:int} <: {b:int,a:bool,c:int}),!,
  !.

testMapRcd :-
  maprcd(writeln,{a=1,b=1,c=1}),!,
  !.

testIsValRcd :-
  \+ isRcdVal({}),writeln(ok),!,
  \+ isRcdVal(1),writeln(ok),!,
  isRcdVal({a=1,b=1}),writeln(ok),!,
  isRcdVal({a=1,b=1,c=1}),writeln(ok),!,
  !.

testTypeof :-
  typeof((λ(x:top)-> x):T),writeln(T),!,T=(top->top),
  typeof((λ(x:top)-> x)$(λ(x:top)-> x):T2),writeln(T2),!,
  typeof((λ(x:(top->top))-> x) $ (λ(x:top)-> x):T3),writeln(T3),!,
  typeof(((λ(r:{x:(top->top)})-> r..x $ r..x)):T4a),writeln(T4a),!,
  typeof({x=(λ(z:top)->z)}:TT),writeln(TT),!,
  typeof(((λ(r:{x:(top->top)})-> (r..x $ r..x)) $ {x=(λ(z:top)->z), y=(λ(z:top)->z)}):T4),writeln(T4),!,
  typeof((λ(x:bot)-> x):T5),writeln(T5),!,T5=(bot->bot),
  typeof((λ(x:bot)-> (x $ x)):T6),writeln(T6),!,T6=(bot->bot),
  !.

main :-
  testMapRcd,
  testIsValRcd,
  testSubtype,
  testTypeof,
  halt.

ScalaLikeFeatherWeightJava.pl

/*
Scala like featherweight Java on Prolog

Scala like featherweight Javaは形式化された Java のシンプルなサブセットでScalaに似せた文法にしたものです。
Scala like featherweight Java on PrologはProlog上のDSLとして実装したものです。
Scala like featherweight Java on Prologの構文はProlog上で実装しやすい形に書き換えてあります:

構文

CL ::=                             クラス宣言：
　class(C,[F:C]<:C,K, [M])

K ::=                              コンストラクタ宣言：
　[F]

M ::=                              メソッド宣言：
　def(M, [F:C]:C = T)

T ::=                              項：
　X                                変数
　T..F                             フィールドアクセス
　T..(M,[T])                       メソッド呼び出し
　new(C,[T])                       オブジェクト生成
　cast(C,T)                        キャスト

V ::=                              値：
　new(C,[V])                       オブジェクト生成
*/

:- initialization(main).
:- op(920, xfx, [ ==>, *==> ]).
:- op(910, xfx, [ ⊢ ]).
:- op(909, yfx, [ => ]).
:- op(501, xfx, <:).
:- op(11, yfx, ..).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).


/*
クラスの宣言(CL)にはクラス名(C)を継承したクラス名があります。
また、フィールド(F)が複数、コンストラクタ(K)が1つ、メソッド(M)が複数あります。
コンストラクタ(K)はメソッドの引数[F:C]がフィールド名とクラス名とのペアが複数で、
スーパークラスのコンストラクタを呼びそのあと、追加分のフィールド設定する必要があります。
メソッド(M)は複数の値を受け取り、式を１つだけかけます。
項(T)は変数や、フィールドアクセス、メソッド呼び出し、
オブジェクト生成、キャストがあるだけです。フィールドの更新はできません。
値(V)はオブジェクト生成時のコンストラクタが値となります。
オリジナルのFeatherweight Scalaの図では上にバーを振って繰り返しを表現していますが、
テキストに書く場合は[]で括ることにしました。
また、Prologで処理できるように演算子定義をおこない、若干Scalaに近い文法に修正しました。
文法要素は大文字にしました。
*/

% 部分型付け規則 C <: D

% 型のリストが両方とも空なら部分型です
[] <: [].

% リスト内の型の全部が部分型なら部分型です
C <: D, Cs <: Ds
--%----------------
[C|Cs] <: [D|Ds].

% C は C の部分型という式です。
C <: C.

% 全ての型はObjectの部分型です。
%_ <: 'Object'.

% CがDを継承していたらCはDの部分型です。
class(C,_ <: D,_, _)
--%----------------
C <: D.

% CがDの部分型かつDがEの部分型ならCはEの部分型です。
C <: D, D <: E
--%------------
C <: E.


% フィールドの探索 fields(C, [f:C])

% Objectのフィールドはありません。
fields('Object',[]).

% Cのフィールドはクラステーブルの中身のクラスの中のスーパークラスのフィールドとクラスのフィールドを合わせたものです。

class(C,FCs <: D,_, _),
fields(D, GDs), append(GDs, FCs, FCs_) 
--%-----------------------------------
fields(C, FCs_).

% メソッドの型の探索 mtype(M,C,[C] -> C)

% 補助述語
split([], [], []).
split([X:Y|Ls],[X|Xs],[Y|Ys]) :- split(Ls,Xs,Ys).

% メソッドの型の探索はmtype(メソッド名,クラス名, 型)

% クラステーブルからクラスを取り出し、
% Ms内のメソッドを取得し、
% 引数の型からメソッドのリターンの型になります。

class(C,_ <: _,_, Ms),
member(def(M, Args:B=_), Ms),
split(Args,_,Bs)
--%-------------------------------------
mtype(M,C,Bs -> B). 

% MがMsの中になかった場合は、スーパークラスを検索する
class(C,_ <: D,_, _), mtype(M,D,T)
--%-------------------------------------
mtype(M,C,T).


% メソッドの本体の探索 mbody(M,C,([X],T))

% 型の代わりにメソッドの本体の引数と式のペアを返す
class(C,_ <: _,_, Ms),
member(def(M, Args:_ = T), Ms),
split(Args,Xs,_)
--%-------------------------------------
mbody(M, C, (Xs,T)).

class(C,_ <: D,_, _), mbody(M,D,T)
--%-------------------------------------
mbody(M,C,T).


% メソッドの正当なオーバーライド override(M, D, [C]->C0)
% ただしく、オーバーライドされているかどうかはoverrideで判定できます。

\+ mtype(M, D, _)
--%-------------------------------------
override(M, D, _ -> _).

mtype(M,D,Ds->D0), Cs = Ds, C0 = D0
--%-------------------------------------
override(M, D, Cs -> C0).

% 項の型付け Γ ⊢ T : C

atom(X),
log('T-Var':X),
member(X : C, Γ),
log('T-Var End'),!
--%------------------------------------- (T-Var)
Γ ⊢ X : C.

log('T-Field'),
Γ ⊢ T0 : C0, fields(C0, FCs),
member(Fi:Ci,FCs),!
--%------------------------------------- (T-Field)
Γ ⊢ T0..Fi : Ci.

log('T-Invk'),
Γ ⊢ T0 : C0,
mtype(M, C0, Ds -> C),
Γ ⊢ Ts : Cs, Cs <: Ds,!
--%------------------------------------- (T-Invk)
Γ ⊢ T0..(M, Ts) : C.

log('T-New'),
fields(C, FDs),
Γ ⊢ Ts : Cs, split(FDs, _, Ds), log("check subtyping"=Cs <: Ds), Cs <: Ds,
log('T-New':C),!
--%------------------------------------- (T-New)
Γ ⊢ new(C, Ts) : C.

log('T-UCast'),
Γ ⊢ T0 : D, D <: C,!
--%------------------------------------- (T-UCast)
Γ ⊢ cast(C, T0) : C.

log('T-DCast'),
Γ ⊢ T0 : D, C <: D, C \= D,!
--%------------------------------------- (T-DCast)
Γ ⊢ cast(C, T0) : C.

log('T-SCast'),
Γ ⊢ T0 : D, \+ C <: D, \+ C <: D,
writeln('愚かさの警告'),!
--%------------------------------------- (T-SCast)
Γ ⊢ cast(C, T0) : C.

!
--%------------------------------------- (T-List0)
_ ⊢ [] : [].

log('T-List1'=[T|Ts]),
Γ ⊢ T : C, Γ ⊢ Ts : Cs,
log('T-List1 End':[C|Cs]),!
--%------------------------------------- (T-List1)
Γ ⊢ [T|Ts] : [C|Cs].

% メソッドの型付け okin(C, M)

[this:C|Args] ⊢ T0:E0, E0 <: C0,
class(C,_ <: D,_, _),
split(Args,_,Cs),override(M,D,Cs->C0)
--%-------------------------------------
okin(C, def(M, Args:C0 = T0)).

% クラスの型付け ok(C)

diff([],_).
diff([X|Xs],[X|Ys]) :- diff(Xs,Ys).

K= Gs,
log("C ":C; " D ":D),fields(D,GDs),
split(GDs,Gs,_),
log("GDs ":GDs;"FCs ":FCs),
diff(GDs,FCs),maplist(okin(C), Ms),writeln(C:" ok"),!
--%-------------------------------------
ok((C,FCs <: D,K,Ms)).

okall :-
	findall((C,FCs <: D,K,Ms),class(C,FCs <: D,K,Ms),Cs),!,
	writeln(Cs),
	maplist(ok,Cs),!.

% 置き換え

subst(_->_,X->X) :- atom(X).
subst(_->_,[]->[]).
subst(S->D,[X|Xs]->[X_|Xs_]) :- subst(S->D,X->X_), subst(S->D,Xs->Xs_).
subst(S->D,(T..(M,Ts))->(T_..(M,Ts_))) :- subst(S->D,T->T_),subst(S->D,Ts->Ts_).
subst(S->D,(T..F)->(T_..F)) :- subst(S->D,T->T_).
subst(S->D,new(C,Ts)->new(C,Ts_)) :- subst(S->D,Ts->Ts_).
subst(S->D,cast(C,T)->cast(C,T_)) :- subst(S->D,T->T_).
subst(Ls,Ls_) :- maplist(subst,Ls,Ls_).
isVal(new(C,Vs)) :- atom(C),isVals(Vs).
isVals(Vs) :- maplist(isVal, Vs).

% 値と項を分離する
splitVals([],[],[]).
splitVals([V|Ts],[V|Vs],Ts_) :- isVal(V), splitVals(Ts,Vs,Ts_).
splitVals(Ts,[],Ts).

% 評価 T ==> T_

isVals(Vs),atom(Fi),fields(C,FCs),
nth0(I,FCs,(Fi:_)),nth0(I,Vs,Vi),!
--%------------------------------------- (E-ProjNew)
new(C, Vs)..Fi ==> Vi.

isVals(Vs),atom(M),mbody(M,C,(Xs, T0)),
subst(Xs->Us, T0 -> T0_),
subst(this->new(C,Vs), T0_ -> T0__),!
--%------------------------------------- (E-InvkNew)
new(C,Vs)..(M,Us) ==> T0__.

isVals(Vs), C <: D,!
--%------------------------------------- (E-CastNew)
cast(D, new(C, Vs)) ==> new(C, Vs).

atom(F), T0 ==> T0_,!
--%------------------------------------- (E-Field)
T0..F ==> T0_..F.

atom(M), T0 ==> T0_,!
--%------------------------------------- (E-Invk-Recv)
T0..(M,Ts) ==> T0_..(M,Ts).

atom(M), splitVals(Args,Vs,[Ti|Ts]),
Ti ==> Ti_,
append(Vs,[Ti_|Ts],Args_),!
--%------------------------------------- (E-Invk-Arg)
V0..(M,Args) ==> V0..(M,Args_).

atom(C), splitVals(Args,Vs,[Ti|Ts]),
Ti ==> Ti_,
append(Vs,[Ti_|Ts],Args_),!
--%------------------------------------- (E-New-Arg)
new(C,Args) ==> new(C,Args_).

atom(C), T0 ==> T0_,!
--%------------------------------------- (E-Cast)
cast(C, T0) ==> cast(C, T0_).

E1 *==> E3 :- E1 ==> E2,!, E2 *==> E3.
E1 *==> E1.

% クラス定義

class('B',[] <: 'Object',[], []).
class('A',[] <: 'B',[], []).
class('Pair',[fst:'B',snd:'B'] <: 'B',[], [
	def(setFst,[fst:'B']:'Pair' = 
		new('Pair',[fst,this..snd])
	)
]).
class('Triple',[fst:'B',snd:'B',thr:'B'] <: 'Pair',[fst,snd], [
]).

%log(_).
log(A) :- writeln(A).

main :- okall,writeln('all classes valid.'),
  E = (new('Pair',[new('A',[]),new('B',[])])..fst),
  \+ isVal(E),!,writeln('not isval':E),
  [] ⊢ E : T,!, format('E : ~w\n',[T]),
  E *==> V, writeln(V),
  halt.

simplebool.pl

/*
構文

t ::=                項：
　x                  変数
　λx:T.t            ラムダ抽象
　t t                関数適用
　true               定数真
　false              定数偽
　if t then t else t 条件式

v ::=                値：
　λx:T.t            ラムダ抽象値
　true               定数真
　false              定数偽

T ::=                型：
　T->T               関数の型
　Bool               ブール値型

Γ ::=               文脈：
　∅                  空の文脈
　Γ,x:T             項変数の束縛
*/

:- initialization(main).
:- style_check(-singleton).
:- op(920, xfx, [ ==>, *==> ]).
:- op(910, xfx, [ ⊢ ]).
:- op(901, xfx, [∈]).
:- op(900, xfx, [ : ]).
:- op(892, xfy, [ then, else ]).
:- op(890, fx, [ letrec, let, if ]).
:- op(500, yfx, $).
:- op(10, fx, λ).
:- op(1200, xfx, [ -- ]).
term_expansion(A -- B, B :- A).

isVal(λ _ : _ -> _).
isVal(true). isVal(false).

subst(X1->V1,X1->V1).
subst(X1->V1,(T2$T3)->(T2_$T3_)) :- subst(X1->V1,T2->T2_), subst(X1->V1,T3->T3_).
subst(X1->_,(λ X1 : T -> T2)->(λ X1 : T -> T2)).
subst(X1->V1,(λ X2 : T -> T2)->(λ X2 : T -> T2_)) :- subst(X1->V1, T2->T2_).
subst(X1->V1,(if T1 then T2 else T3)->(if T1_ then T2_ else T3_)) :- subst(X1->V1, T1->T1_),subst(X1->V1, T2->T2_),subst(X1->V1, T3->T3_).
subst(_->_,T1->T1).

% 評価 E ==> E_

E1 ==> E1_
--%-------------------------------------- (E-App1)
E1 $ E2 ==> E1_ $ E2.

isVal(V1), E2 ==> E2_
--%-------------------------------------- (E-App2)
V1 $ E2 ==> V1 $ E2_.

isVal(V2), subst(X->V2,E12->E12_)
--%-------------------------------------- (E-AppAbs)
(λ X : T11 -> E12) $ V2 ==> E12_.

(if true then T2 else _) ==> T2.        % (E-IfTrue)

(if false then _ else T3) ==> T3.       % (E-IfFalse)

% 型付け Γ ⊢ t : T

X : T ∈ (Γ,(X:T)).
X : T ∈ (Γ,(X1:_)) :- X : T ∈ Γ.

X : T ∈ Γ
--%-------------------------------------- (T-Var)
Γ ⊢ X : T.

(Γ , (X : T1)) ⊢ E2 : T2
--%-------------------------------------- (T-Abs)
Γ ⊢ (λ X : T1 -> E2) : (T1 -> T2).

Γ ⊢ E1 : (T11 -> T12), Γ ⊢ E2 : T11
--%-------------------------------------- (T-App)
Γ ⊢ E1 $ E2 : T12.

Γ ⊢ true : bool.                       % (T-True)

Γ ⊢ false : bool.                      % (T-False)

Γ ⊢ E1 : bool, Γ ⊢ E2 : T, Γ ⊢ E3 : T
--%-------------------------------------- (T-If)
Γ ⊢ if E1 then E2 else E3 : T.


E1 *==> E3 :- E1 ==> E2, E2 *==> E3.
E1 *==> E1.

main :-
  (λ x : bool -> x) $ true *==> E1, write(E1), nl,!, 
  (λ x : bool -> ((λ z : bool -> z) $ x)) $ true *==> E2, write(E2), nl,!, 
  (λ x : bool -> x) *==> E3, write(E3), nl,E3=(λ x:bool -> x),!, 
  (if true then false else true) *==> E4, write(E4),nl, E4=false,!,
  (if false then false else true) *==> E5, write(E5),nl, E5=true,!,
  [] ⊢ true : T0, write(T0), nl,!, T0=bool,
  [] ⊢ (λ x : bool -> x) $ true : T1, write(T1), nl,!, T1=bool,
  [] ⊢ (λ x : bool -> ((λ z : bool -> z) $ x)) $ true : T2, write(T2), nl,!, T2=bool,
  [] ⊢ (λ x : bool -> x) : T3, write(T3), nl,!, T3=(bool->bool),
  halt.