Skip to content

Instantly share code, notes, and snippets.

@hsk

hsk/file0.pl

Last active January 9, 2018 09:18
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save hsk/c8ea6bab8586f7e934eaa74efc63b9c5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save hsk/c8ea6bab8586f7e934eaa74efc63b9c5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
file0.pl
:- tpp(
type Colour = 'MkColour'!(int,int,int);
type Point = 'MkPoint'!(float,float);
type CPoint = 'MkCPoint'!(float,float,Colour);
val 'MkColour' : (int->int->int->Colour);
val c1 : (Colour->int);
val c2 : (Colour->int);
val c3 : (Colour->int);
val 'MkPoint' : (float->float->Point);
val pt1 : (Point->float);
val pt2 : (Point->float);
val 'MkCPoint' : (float->float->Colour->CPoint);
val cpt1 : (CPoint->float);
val cpt2 : (CPoint->float);
val cpt3 : (CPoint->colour);
val add : (float->float->float);
val sqr : (float->float);
val sqrt : (float->float);
class P:XCoord where xcoord:(P->float);
class P2:YCoord where ycoord:(P2->float);
inst Point:XCoord where xcoord=λ(u,pt1$u);
inst Point:YCoord where ycoord=λ(u,pt2$u);
inst CPoint:XCoord where xcoord=λ(u,cpt1$u);
inst CPoint:YCoord where ycoord=λ(u,cpt2$u);
let distance=λ(p,sqrt$(add$(sqr$(xcoord$p))$(sqr$(ycoord$p))));
distance$('MkCPoint'$2.0$3.0$('MkColour'$0$0$0))
,R),!,R==float.
:- halt.
Raw
file0.txt
Type variables α
Type constructors κ
Class constructors c
Types τ ::= () | κ τ | α | τ1 * τ2 | τ1 -> τ2
Type schemes σ ::= ∀α::Γ.σ | τ
Type classes γ ::= c τ
Class sets Γ ::= {c1 τ1,..., cn τn} (n ≥ 0,ci pairwise disjoint)
Contexts C ::= {α1::Γ1, ..., αn::Γn} (n ≥ 0)
Expressions e ::= x | e e' | λx : e | let x = e' in e
Programs p ::= class α::γ where x : σ in p
| inst C ⇒ τ::γ where x = e in p
| e
Raw
file1.pl
:- module(param,
[foldr/4,fv/2,gfv/2,cfv/2,cdom/2,capp/3,creg/2,gfv/2, tpgen/5,put/2,get/2,tp1/2,tp3/3, tpp/2]).
:- expects_dialect(sicstus).
:- op(500,xfx,!).
:- op(600,yfx,[∈, ⊑ , ˄, $]).
:- op(700,xfy,[=>,where]).
:- op(900,xfx,ⱶo).
:- op(1200, xfx, --).
:- op(990,fy,[let,inst,val,class,type]).
:- set_prolog_flag(occurs_check, true).
term_expansion((A--B), (B:-A)).
member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).
union_eq([],Ys,Ys) :- !.
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!, union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).
subtract_eq([],_,[]) :- !.
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!,subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).
del_eq(C,A,C_) :- foldr(del_eq1(A),C,[],C_).
del_eq1(A,(B,_),F,F) :- B==A.
del_eq1(_,(B,V),F,[(B,V)|F]).
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す
walk(F,X,I,R) :- call(F,X,I,R).
walk(F,X,I,R) :- compound(X), X =.. [_|Xs],!,foldl(walk(F),Xs,I,R),!.
walk(_,_,I,I) :- !.
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
% 型の置換
sub(X1/T,X,T) :- X1==X,!.
sub(X1/T,∀(X,Πa,T), ∀(X,Πa,T)) :- X1==X,!.
sub(AB,X,R) :- compound(X),X=..Xs,!,maplist(sub(AB),Xs,R_),R=..R_,!.
sub(_,I,I) :- !.
gsub(S,Γ,Γ_) :- maplist(ysub(S),Γ,Γ_),!. % 型環境の置換
ysub(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.
csub(S,C,C_) :- maplist(csub1(S),C,C_),!.
csub1(S,(A,Γ),(A_,Γ_)) :- !,sub(S,A,A_),gsub(S,Γ,Γ_),!.
% 自由型変数取得
fv(X,R) :- walk(fv1,X,[],R),!. % 自由型変数取得
fv1(X,I,R) :- var(X), union_eq(I,[X],R).
fv1(∀(X,G,T),I,R) :- !,fv(T,Ts),gfv(G,Ts2), union_eq(Ts2,Ts,Ts3),
subtract_eq(Ts3,[X],R1), union_eq(I,R1,R).
gfv(Γ,Xs) :- foldr(gfv1, Γ, [], Xs).% 型環境置換
gfv1((_,T), Fv1,R) :- fv(T,T_),union_eq(Fv1,T_,R).%todo
cfv(C,R) :- maplist(cfv1,C,R1),foldr(union_eq,R1,[],R).
cfv1((_,G),R) :- gfv(G,R).
cdom(C,R) :- maplist(cdom1,C,R). % ドメイン
cdom1((A,_),A).
creg(C,R) :- cdom(C,R1), foldr(creg1(C),R1,[],R). % リージョン(領域)
creg1(C,A,R1,R) :- capp(C,A,G), gfv(G,R2), union_eq(R1,R2,R).
capp(C,A,R) :- (A1,R) ∈ C,A1==A,!. % 適用
capp(_,_,[]).
% 一般化 : 制約Cを一般化できたら環境から回収して清潔さを保つのがポイント
mem(F,A) :- call(F,As),!, A ∈ As. % 述語を実行してメンバ取り出し
memeq(F,A) :- call(F,As),!, member_eq(A,As). % 述語を実行してメンバ判定
tpgen(T,G,C,C_,R) :- mem(cdom(C),A), % CのドメインにあるAで
\+memeq(gfv(G),A), % 環境の自由変数になく
\+memeq(creg(C),A), % リージョン領域にもない
\+memeq(cdom(C_),A), % 元のドメインにもない
capp(C,A,Ca),!, % 制約をとりだし
%(memeq(gfv(Ca),A) ; memeq(fv(T),A)),!, % 追加条件
del_eq(C,A,C2),% 制約リストからAを除外
tpgen(∀(A, Ca, T), G, C2, C_,R).
tpgen(T,_,C,_,(T,C)).
% 具体化
inst(T,C,(T,C)) :- var(T),!;T\= ∀(_,_,_),!. % ∀でなければそのまま
inst(∀(A,G,T),C,R) :- sub(A/B,T,T_),inst(T_,[(B,G)|C],R).% 新しいBで置換、制約追加
% 単一化
mgu(_, T1,T2,C,C) :- T1==T2,!. % 同じ
mgu(G,A,T,C,R) :- var(A),!,mgu1(G,A,T,C,R).% 型変数なら単一化
mgu(G,T,A,C,R) :- var(A),!,mgu1(G,A,T,C,R).
mgu(G,K!T,K!T_,C,R) :- !,mgu(G,T,T_,C,R).% データ引数で単一化
mgu(G,(T1,T2),(T1_,T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%ペア
mgu(G,(T1->T2),(T1_->T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%関数
mgu(_,[],[],C,C) :- !.% ユニット
mgu(_,T1,T2,(_,_),_) :- failwith('mgu error ~w ~w', [T1,T2]).
mgu1(G,A,T,C,R) :- capp(C,A,G1), del_eq(C,A,C2),% 変数制約取得、制約の回収※1
A=T, mgn(G,(A,G1),C2,R),!.% 単一化、回収制約正規化
mgu1(_,A,T,_,_) :- failwith('mgu1 error ~w ~w',[A,T]).
% 正規化アルゴリズム
mgn(G,(A,G1),C,R) :- foldl(mgn1(G,A),G1,C,R). % 制約G1でループ
mgn1(G,A,(D,T),C,R) :- var(A),capp(C,A,G1),!,% 変数なら制約取得
((D_,T_)∈G1,D==D_,!,mgu(G,T,T_,C,R) % クラス有り、単一化
; R=[(A,[(D,T)|G1])|C]).% クラス無し、制約追加(※1戻す)
mgn1(G,K!KT,(D,T),C,R) :- !,(inst C_=>K_!KT_:D_!T_)∈G,K_==K,D_==D,% データ実装検索
!,sub(KT_/KT,T_,T2_),mgu(G,T,T2_,C,C2),% クラス引数単一化
csub(KT_/KT,C_,C2_),% 制約を置換して実体化
foldr(mgn(G),C2_,C2,R).% 実体化した制約で正規化ループ
mgn1(G,(T1,T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% ペア
mgn1(G,(T1->T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% 関数
mgn1(_,[],_,C, C). % ユニット
mgn1(G,T1,Y,C,_) :- failwith('error:~w',[mgn1(G,T1,Y,C)]).
% 型推論(式)
tp(I,_,C,(int,C)) :- integer(I),!.
tp(F,_,C,(float,C)) :- float(F),!.
tp([],_,C,([],C)). :- !. % unit
tp(λ(X,E),G,C,((A->T1),C1)) :- !,tp(E,[(X,A)|G],[(A,[])|C],(T1,C1)).
tp((let X=E1;E2),G,C,R) :- !,tp(E1,G,C,(T1,C1)),tpgen(T1,G,C1,C,(T,C2)),
tp(E2,[(X,T)|G],C2,R).
tp(X,G,C,R) :- atom(X),!,(X,T) ∈ G, inst(T,C,R).
tp((E1$E2),G,C,(A,C3)) :- !,tp(E1,G,C,(T1,C1)),!,tp(E2,G,C1,(T2,C2)),!,
mgu(G,T1,(T2->A),([(A,[])|C2]),C3),!.
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
Raw
file1.txt
C ⊦⊦ α :: γ (α::{...γ...} ∈ C)
C ⊦⊦ C'
--------- ("inst C' ⇒ τ::γ" ∈ Ds)
C ⊦⊦ τ::γ
C ⊦⊦ τ::γ1 ... C ⊦⊦ τ::γn
----------------------------- (n ≥ 0)
C ⊦⊦ τ:: {γ1 ,..., γn}
C ⊦⊦ τ1::Γ1 ... C ⊦⊦ τn::Γn
------------------------------------ (n ≥ 0)
C ⊦⊦ {τ1::Γ1, ... ,τn::Γn}
Raw
file10.pl
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
Raw
file11.pl
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す
Raw
file12.pl
walk(F,X,I,R) :- call(F,X,I,R).
walk(F,X,I,R) :- compound(X), X =.. [_|Xs],!,foldl(walk(F),Xs,I,R),!.
walk(_,_,I,I) :- !.
Raw
file13.pl
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
Raw
file14.pl
% 型の置換
sub(X1/T,X,T) :- X1==X,!.
sub(X1/T,∀(X,Πa,T), ∀(X,Πa,T)) :- X1==X,!.
sub(AB,X,R) :- compound(X),X=..Xs,!,maplist(sub(AB),Xs,R_),R=..R_,!.
sub(_,I,I) :- !.
gsub(S,Γ,Γ_) :- maplist(ysub(S),Γ,Γ_),!. % 型環境の置換
ysub(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.
csub(S,C,C_) :- maplist(csub1(S),C,C_),!.
csub1(S,(A,Γ),(A_,Γ_)) :- !,sub(S,A,A_),gsub(S,Γ,Γ_),!.
Raw
file15.pl
% 自由型変数取得
fv(X,R) :- walk(fv1,X,[],R),!. % 自由型変数取得
fv1(X,I,R) :- var(X), union_eq(I,[X],R).
fv1(∀(X,G,T),I,R) :- !,fv(T,Ts),gfv(G,Ts2), union_eq(Ts2,Ts,Ts3),
subtract_eq(Ts3,[X],R1), union_eq(I,R1,R).
gfv(Γ,Xs) :- foldr(gfv1, Γ, [], Xs).% 型環境置換
gfv1((_,T), Fv1,R) :- fv(T,T_),union_eq(Fv1,T_,R).%todo
cfv(C,R) :- maplist(cfv1,C,R1),foldr(union_eq,R1,[],R).
cfv1((_,G),R) :- gfv(G,R).
Raw
file16.pl
cdom(C,R) :- maplist(cdom1,C,R). % ドメイン
cdom1((A,_),A).
creg(C,R) :- cdom(C,R1), foldr(creg1(C),R1,[],R). % リージョン(領域)
creg1(C,A,R1,R) :- capp(C,A,G), gfv(G,R2), union_eq(R1,R2,R).
capp(C,A,R) :- (A1,R) ∈ C,A1==A,!. % 適用
capp(_,_,[]).
Raw
file17.pl
% 一般化 : 制約Cを一般化できたら環境から回収して清潔さを保つのがポイント
mem(F,A) :- call(F,As),!, A ∈ As. % 述語を実行してメンバ取り出し
memeq(F,A) :- call(F,As),!, member_eq(A,As). % 述語を実行してメンバ判定
tpgen(T,G,C,C_,R) :- mem(cdom(C),A), % CのドメインにあるAで
\+memeq(gfv(G),A), % 環境の自由変数になく
\+memeq(creg(C),A), % リージョン領域にもない
\+memeq(cdom(C_),A), % 元のドメインにもない
capp(C,A,Ca),!, % 制約をとりだし
%(memeq(gfv(Ca),A) ; memeq(fv(T),A)),!, % 追加条件
del_eq(C,A,C2),% 制約リストからAを除外
tpgen(∀(A, Ca, T), G, C2, C_,R).
tpgen(T,_,C,_,(T,C)).
Raw
file18.pl
% 具体化
inst(T,C,(T,C)) :- var(T),!;T\= ∀(_,_,_),!. % ∀でなければそのまま
inst(∀(A,G,T),C,R) :- sub(A/B,T,T_),inst(T_,[(B,G)|C],R).% 新しいBで置換、制約追加
Raw
file19.pl
% 単一化
mgu(_, T1,T2,C,C) :- T1==T2,!. % 同じ
mgu(G,A,T,C,R) :- var(A),!,mgu1(G,A,T,C,R).% 型変数なら単一化
mgu(G,T,A,C,R) :- var(A),!,mgu1(G,A,T,C,R).
mgu(G,K!T,K!T_,C,R) :- !,mgu(G,T,T_,C,R).% データ引数で単一化
mgu(G,(T1,T2),(T1_,T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%ペア
mgu(G,(T1->T2),(T1_->T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%関数
mgu(_,[],[],C,C) :- !.% ユニット
mgu(_,T1,T2,(_,_),_) :- failwith('mgu error ~w ~w', [T1,T2]).
mgu1(G,A,T,C,R) :- capp(C,A,G1), del_eq(C,A,C2),% 変数制約取得、制約の回収※1
A=T, mgn(G,(A,G1),C2,R),!.% 単一化、回収制約正規化
mgu1(_,A,T,_,_) :- failwith('mgu1 error ~w ~w',[A,T]).
% 正規化アルゴリズム
mgn(G,(A,G1),C,R) :- foldl(mgn1(G,A),G1,C,R). % 制約G1でループ
mgn1(G,A,(D,T),C,R) :- var(A),capp(C,A,G1),!,% 変数なら制約取得
((D_,T_)∈G1,D==D_,!,mgu(G,T,T_,C,R) % クラス有り、単一化
; R=[(A,[(D,T)|G1])|C]).% クラス無し、制約追加(※1戻す)
mgn1(G,K!KT,(D,T),C,R) :- !,(inst C_=>K_!KT_:D_!T_)∈G,K_==K,D_==D,% 実装検索
!,sub(KT_/KT,T_,T2_),mgu(G,T,T2_,C,C2),% クラス引数単一化
csub(KT_/KT,C_,C2_),% 制約を置換して実体化
foldr(mgn(G),C2_,C2,R).% 実体化した制約で正規化ループ
mgn1(G,(T1,T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% ペア
mgn1(G,(T1->T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% 関数
mgn1(_,[],_,C, C). % ユニット
mgn1(G,T1,Y,C,_) :- failwith('error:~w',[mgn1(G,T1,Y,C)]).
Raw
file2.pl
:- module(param,
[foldr/4,fv/2,gfv/2,cfv/2,cdom/2,capp/3,creg/2,gfv/2, tpgen/5,put/2,get/2,tp1/2,tp3/3, tpp/2]).
Raw
file2.txt
(var) A,C ⊢ x : σ (x : σ ∈ A)
A,C ⊢ e : ∀α::Γ.σ C ⊦⊦ τ::Γ
(∀-elim) --------------------------------
A,C ⊢ e : [α -> τ] σ
A,C.α::Γ ⊢ e : σ
(∀-intro) ------------------------ (α ∉ fv A ∪ reg C)
A,C ⊢ e : ∀α::Γ.σ
A,C ⊢ e :τ' -> τ A,C ⊢ e' : τ'
(λ-elim) --------------------------------
A,C ⊢ e e' : τ
A.x:τ',C ⊢ e : τ
(λ-intro) --------------------------------
A,C ⊢ λx.e :τ' -> τ
A,C ⊢ e' : σ A.x : σ,C ⊢ e : τ
(let) --------------------------------------
A,C ⊢ let x = e' in e : τ
Raw
file20.pl
% 型推論(式)
tp(I,_,C,(int,C)) :- integer(I),!.
tp(F,_,C,(float,C)) :- float(F),!.
tp([],_,C,([],C)). :- !. % unit
tp(λ(X,E),G,C,((A->T1),C1)) :- !,tp(E,[(X,A)|G],[(A,[])|C],(T1,C1)).
tp((let X=E1;E2),G,C,R) :- !,tp(E1,G,C,(T1,C1)),tpgen(T1,G,C1,C,(T,C2)),
tp(E2,[(X,T)|G],C2,R).
tp(X,G,C,R) :- atom(X),!,(X,T) ∈ G, inst(T,C,R).
tp((E1$E2),G,C,(A,C3)) :- !,tp(E1,G,C,(T1,C1)),!,tp(E2,G,C1,(T2,C2)),!,
mgu(G,T1,(T2->A),([(A,[])|C2]),C3),!.
Raw
file21.pl
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
Raw
file22.pl
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
Raw
file23.pl
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
Raw
file24.pl
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
Raw
file25.pl
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
Raw
file26.pl
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
Raw
file3.pl
:- expects_dialect(sicstus).
Raw
file3.txt
A.x : ∀_{fvγ} ∀α :: {γ}.σ, C ⊢ p : τ
(class) -------------------------------------------
A,C ⊢ class α :: γ　where x : σ in p : τ
A,C ⊢ x : ∀α :: {γ} :σ A,C ⊢ e :[α ->τ'] σ A,C ⊢ p : τ
(inst) --------------------------------------------------------------
A,C ⊢ inst C' ⇒ τ'::γ where x = e in p : τ
Raw
file4.pl
:- op(500,xfx,!).
:- op(600,yfx,[∈, ⊑ , ˄, $]).
:- op(700,xfy,[=>,where]).
:- op(900,xfx,ⱶo).
:- op(1200, xfx, --).
:- op(990,fy,[let,inst,val,class,type]).
:- set_prolog_flag(occurs_check, true).
Raw
file4.txt
(var') A,C ⊢' x : τ (x : σ ∈ A, τ ≼C σ)
A,C ⊢' e : τ' -> τ A,C ⊢' e' : τ'
(∀-elim') ------------------------------
A,C ⊢' e e' : τ
A.x : τ', C ⊢' e : τ
(∀-intro') -----------------------
A,C ⊢' λx.e : τ' -> τ
A,C ⊢' e' : τ' A.x : σ,C ⊢' e : τ
(let') ---------------------------------------- (σ, C'') = gen(τ',A,C'), C'' ≼ C
A,C ⊢' let x = e' in e : τ
Raw
file5.pl
term_expansion((A--B), (B:-A)).
Raw
file6.pl
member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).
Raw
file7.pl
union_eq([],Ys,Ys) :- !.
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!, union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).
Raw
file8.pl
subtract_eq([],_,[]) :- !.
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!,subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).
Raw
file9.pl
del_eq(C,A,C_) :- foldr(del_eq1(A),C,[],C_).
del_eq1(A,(B,_),F,F) :- B==A.
del_eq1(_,(B,V),F,[(B,V)|F]).
Raw
param3.pl
:- module(param,
[foldr/4,fv/2,gfv/2,cfv/2,cdom/2,capp/3,creg/2,gfv/2, tpgen/5,put/2,get/2,tp1/2,tp3/3, tpp/2]).
:- expects_dialect(sicstus).
:- op(500,xfx,!).
:- op(600,yfx,[∈, ⊑ , ˄, $]).
:- op(700,xfy,[=>,where]).
:- op(900,xfx,ⱶo).
:- op(1200, xfx, --).
:- op(990,fy,[let,inst,val,class,type]).
:- set_prolog_flag(occurs_check, true).
term_expansion((A--B), (B:-A)).
member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).
union_eq([],Ys,Ys) :- !.
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!, union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).
subtract_eq([],_,[]) :- !.
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!,subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).
del_eq(C,A,C_) :- foldr(del_eq1(A),C,[],C_).
del_eq1(A,(B,_),F,F) :- B==A.
del_eq1(_,(B,V),F,[(B,V)|F]).
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す
walk(F,X,I,R) :- call(F,X,I,R).
walk(F,X,I,R) :- compound(X), X =.. [_|Xs],!,foldl(walk(F),Xs,I,R),!.
walk(_,_,I,I) :- !.
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
% 型の置換
sub(X1/T,X,T) :- X1==X,!.
sub(X1/T,∀(X,Πa,T), ∀(X,Πa,T)) :- X1==X,!.
sub(AB,X,R) :- compound(X),X=..Xs,!,maplist(sub(AB),Xs,R_),R=..R_,!.
sub(_,I,I) :- !.
gsub(S,Γ,Γ_) :- maplist(ysub(S),Γ,Γ_),!. % 型環境の置換
ysub(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.
csub(S,C,C_) :- maplist(csub1(S),C,C_),!.
csub1(S,(A,Γ),(A_,Γ_)) :- !,sub(S,A,A_),gsub(S,Γ,Γ_),!.
% 自由型変数取得
fv(X,R) :- walk(fv1,X,[],R),!. % 自由型変数取得
fv1(X,I,R) :- var(X), union_eq(I,[X],R).
fv1(∀(X,G,T),I,R) :- !,fv(T,Ts),gfv(G,Ts2), union_eq(Ts2,Ts,Ts3),
subtract_eq(Ts3,[X],R1), union_eq(I,R1,R).
gfv(Γ,Xs) :- foldr(gfv1, Γ, [], Xs).% 型環境置換
gfv1((_,T), Fv1,R) :- fv(T,T_),union_eq(Fv1,T_,R).%todo
cfv(C,R) :- maplist(cfv1,C,R1),foldr(union_eq,R1,[],R).
cfv1((_,G),R) :- gfv(G,R).
cdom(C,R) :- maplist(cdom1,C,R). % ドメイン
cdom1((A,_),A).
creg(C,R) :- cdom(C,R1), foldr(creg1(C),R1,[],R). % リージョン(領域)
creg1(C,A,R1,R) :- capp(C,A,G), gfv(G,R2), union_eq(R1,R2,R).
capp(C,A,R) :- (A1,R) ∈ C,A1==A,!. % 適用
capp(_,_,[]).
% 一般化 : 制約Cを一般化できたら環境から回収して清潔さを保つのがポイント
mem(F,A) :- call(F,As),!, A ∈ As. % 述語を実行してメンバ取り出し
memeq(F,A) :- call(F,As),!, member_eq(A,As). % 述語を実行してメンバ判定
tpgen(T,G,C,C_,R) :- mem(cdom(C),A), % CのドメインにあるAで
\+memeq(gfv(G),A), % 環境の自由変数になく
\+memeq(creg(C),A), % リージョン領域にもない
\+memeq(cdom(C_),A), % 元のドメインにもない
capp(C,A,Ca),!, % 制約をとりだし
%(memeq(gfv(Ca),A) ; memeq(fv(T),A)),!, % 追加条件
del_eq(C,A,C2),% 制約リストからAを除外
tpgen(∀(A, Ca, T), G, C2, C_,R).
tpgen(T,_,C,_,(T,C)).
% 具体化
inst(T,C,(T,C)) :- var(T),!;T\= ∀(_,_,_),!. % ∀でなければそのまま
inst(∀(A,G,T),C,R) :- sub(A/B,T,T_),inst(T_,[(B,G)|C],R).% 新しいBで置換、制約追加
% 単一化
mgu(_, T1,T2,C,C) :- T1==T2,!. % 同じ
mgu(G,A,T,C,R) :- var(A),!,mgu1(G,A,T,C,R).% 型変数なら単一化
mgu(G,T,A,C,R) :- var(A),!,mgu1(G,A,T,C,R).
mgu(G,K!T,K!T_,C,R) :- !,mgu(G,T,T_,C,R).% データ引数で単一化
mgu(G,(T1,T2),(T1_,T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%ペア
mgu(G,(T1->T2),(T1_->T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%関数
mgu(_,[],[],C,C) :- !.% ユニット
mgu(_,T1,T2,(_,_),_) :- failwith('mgu error ~w ~w', [T1,T2]).
mgu1(G,A,T,C,R) :- capp(C,A,G1), del_eq(C,A,C2),% 変数制約取得、制約の回収※1
A=T, mgn(G,(A,G1),C2,R),!.% 単一化、回収制約正規化
mgu1(_,A,T,_,_) :- failwith('mgu1 error ~w ~w',[A,T]).
% 正規化アルゴリズム
mgn(G,(A,G1),C,R) :- foldl(mgn1(G,A),G1,C,R). % 制約G1でループ
mgn1(G,A,(D,T),C,R) :- var(A),capp(C,A,G1),!,% 変数なら制約取得
((D_,T_)∈G1,D==D_,!,mgu(G,T,T_,C,R) % クラス有り、単一化
; R=[(A,[(D,T)|G1])|C]).% クラス無し、制約追加(※1戻す)
mgn1(G,K!KT,(D,T),C,R) :- !,(inst C_=>K_!KT_:D_!T_)∈G,K_==K,D_==D,% 実装検索
!,sub(KT_/KT,T_,T2_),mgu(G,T,T2_,C,C2),% クラス引数単一化
csub(KT_/KT,C_,C2_),% 制約を置換して実体化
foldr(mgn(G),C2_,C2,R).% 実体化した制約で正規化ループ
mgn1(G,(T1,T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% ペア
mgn1(G,(T1->T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% 関数
mgn1(_,[],_,C, C). % ユニット
mgn1(G,T1,Y,C,_) :- failwith('error:~w',[mgn1(G,T1,Y,C)]).
% 型推論(式)
tp(I,_,C,(int,C)) :- integer(I),!.
tp(F,_,C,(float,C)) :- float(F),!.
tp([],_,C,([],C)). :- !. % unit
tp(λ(X,E),G,C,((A->T1),C1)) :- !,tp(E,[(X,A)|G],[(A,[])|C],(T1,C1)).
tp((let X=E1;E2),G,C,R) :- !,tp(E1,G,C,(T1,C1)),tpgen(T1,G,C1,C,(T,C2)),
tp(E2,[(X,T)|G],C2,R).
tp(X,G,C,R) :- atom(X),!,(X,T) ∈ G, inst(T,C,R).
tp((E1$E2),G,C,(A,C3)) :- !,tp(E1,G,C,(T1,C1)),!,tp(E2,G,C1,(T2,C2)),!,
mgu(G,T1,(T2->A),([(A,[])|C2]),C3),!.
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
Raw
param3test.pl
:- expects_dialect(sicstus).
:- current_prolog_flag(argv, [M]),!,format('use ~w\n',[M]),use_module(M) ;
use_module(param3).
:- begin_tests(foldr).
test(foldl0) :- foldl(concat,[a,b,c],'',cba).
test(foldr0) :- foldr(concat,[a,b,c],'',abc).
:- end_tests(foldr).
:- begin_tests(tvar).
test(tvar) :- var(_).
test(tvar) :- \+var(a).
test(val) :- atom(a).
test(val) :- \+atom(_).
:- end_tests(tvar).
permutation(0, Xs, Xs).
permutation(N, Xs, [X | Ys]) :-
N > 0, N1 is N - 1, select(X, Xs, Zs), permutation(N1, Zs, Ys).
pair(Xs,(A,B)) :- select(A,Xs,Ys),select(B,Ys,_).
dim(Xs) :- forall(member(C,Xs),var(C)),forall(pair(Xs,(A,B)),dif(A,B)).
:- begin_tests(fv).
test(tvx):-fv(X,[X]).
test(tvd):-fv(x!(Y,Z), R),R=[Y,Z],dim([Y,Z]).
test(arr):-fv(X->Y, [X,Y]),dim([X,Y]).
test(forall):-fv(∀(X,[],(D->X->Y)),[D,Y]),dim([D,Y]).
test(forall2):-fv(∀(Y,[],∀(X,[],(D->X->Y))),[D]),dim([X,Y,D]).
test(forall_pia):-fv(∀(X,[(x,(Y->Z)),(y,(B->C))],(D->X)),R),
/* A=a,B=b,C=c,Y=y,Z=z,D=d,X=x,writeln(R),*/R==[B,C,Y,Z,D],dim([B,C,Y,Z,D]). % todo
test(int):- fv(int, []).
:- end_tests(fv).
:- begin_tests(gfv).
test(gfv) :- gfv([],[]).
test(gfv) :- gfv([(X,Y)],[Y]),dim([X,Y]).
:- end_tests(gfv).
:- begin_tests(cfv).
test(cfv) :- cfv([],R),!,R=[].
test(cfv) :- cfv([(A,[(A,X),(B,Y)]),(B,[(A,Z)])],R),!,R=[Y,X,Z].
:- end_tests(cfv).
/*
:- begin_tests(sub).
test(sub_var_null) :- sub([], x,R),R=x.
test(sub_var1) :- sub([(x,y)], x,R),R=y.
test(sub_var2) :- sub([(a,b),(x,y)], x,R),R=y.
test(sub_var_none) :- sub([(a,b)], x,R),R=x.
test(sub_con_null) :- sub([], (a![]),R),R=(a![]).
test(sub_con1) :- sub([(x,y)], (a!x),R),R=(a!y).
test(sub_con2) :- sub([(x,y),(a,b)], a!(x->a),R),R=a!(y->b).
test(sub_arr_null) :- sub([], (x->y),R),R=(x->y).
test(sub_arr1) :- sub([(x,y)], (y->x),R),R=(y->y).
test(sub_arr2) :- sub([(x,y),(a,b)], (x->y),R),R=(y->y).
test(sub_pair_null) :- sub([(x,y),(y,z)], (x,y),R),R=(z,z).
test(sub_all1) :- sub([(x,y),(a,b)], ∀(x,[],(x->y)),R), R= ∀(x,[],(x->y)). %todo
test(sub_all2) :- sub([(x,y),(a,b)], ∀(z,[],(x->y)),R), R= ∀(z,[],(y->y)).
:- end_tests(sub).
:- begin_tests(gsub).
test(gsub_null) :- gsub([], [],R),R=[].
test(gsub_null) :- gsub([], [(x,y)],R),R=[(x,y)].
test(gsub_null) :- gsub([(x,y)], [(x,x)],R),R=[(x,y)].
test(gsub_null) :- gsub([(x,y),(y,z)], [(x,x)],R),R=[(x,z)].
:- end_tests(gsub).
g_c1([(o1,(a->int)),(o2,(a->int)),(o1,(b->int)),(o2,(b->int))]).
g_c2([(o1,(a->int)),(o2,(a->float)),(o1,(b->int)),(o2,(b->int))]).
g_c3([(xcoord,(x10->x9)),(xcoord,(x4->x3)),(xcoord,('MkPoint'![float,float]->float))]).
*/
:- begin_tests(cdom).
test(null) :- cdom([],R),R==[].
test(null) :- cdom([(Tv,[(C1,[]),(C2,[])])],R),R==[Tv],dim([Tv,C1,C2]).
test(null) :- cdom([(Tv,[(C1,[])]),(Tv2,[(C1,[])])],R),R==[Tv,Tv2],dim([Tv,Tv2,C1]).
:- end_tests(cdom).
:- begin_tests(capp).
test(null) :- capp([], A,R),R==[],dim([A]).
test(null) :- capp([(Tv,[(C1,[]),(C2,[])])],Tv,R),!, R==[(C1,[]),(C2,[])],dim([Tv,C1,C2]).
test(null) :- capp([(Tv,[(C1,[])]),(Tv2,[(C2,[])])],Tv,R),!, R==[(C1,[])],dim([Tv,Tv2,C1,C2]).
test(null) :- capp([(Tv2,[(C2,[])]),(Tv,[(C1,[])])],Tv,R),!, R==[(C1,[])],dim([Tv,Tv2,C1,C2]).
:- end_tests(capp).
:- begin_tests(creg).
test(null) :- creg([],[]).
test(null) :- creg([(Tv,[(C1,A),(C2,B)])],R),R==[B,A],dim([Tv,C1,C2,A,B]).
test(null) :- creg([(Tv,[(C1,A)]),(Tv2,[(C2,B)])],R),R==[B,A],dim([Tv,Tv2,C1,C2,A,B]).
:- end_tests(creg).
:- begin_tests(gen).
test(gfv) :- gfv([(A,A)],R),!,R==[A],dim([A]). % todo 他のアルゴリズムでもしらべる
test(gfv) :- gfv([(X,A)],R),!,R==[A],dim([X,A]). % todo 他のアルゴリズムでもしらべる
/*
test(gen1) :-
g_c2(C),
put(s,[]),
gen(((a->int),[],C),R),
R=(∀(a,[(o1,(a->int)),(o2,(a->float))],(a->int)),_),!.
test(gen3) :- g_c3(C),gen(((x10->x9),[(x0,'MkPoint'![float,float]),(x5,float),(Point,'MkPoint'![float,float])],C),(R,_)),
R= ∀(x9,[],∀(x10,[(xcoord,(x10->x9))],(x10->x9))),!.
test(gen4) :- g_c3(C),gen(((x6->x10->x9),[(x0,'MkPoint'![float,float]),(x5,float),(Point,'MkPoint'![float,float])],C),(R,_)),
R= ∀(x9,[],∀(x10,[(xcoord,(x10->x9))],∀(x6,[],(x6->x10->x9)))),!.
*/
:- end_tests(gen).
:- begin_tests('tp mono').
test(mono_int) :- tp1(1, int).
test(mono_float) :- tp1(1.0, float).
test(mono_let) :- tp1(let x=1;x, int).
test(mono_lambda) :- tp1(λ(x,x), R),!,R= ∀(X0,[],(X0->X0)),var(X0).
test(mono_lambda2) :- tp1(let id = λ(x,x); id, R), !,R= ∀(X1,[],(X1->X1)),var(X1).
test(mono_lambda3) :- tp1(let id = λ(x,x); id $ 1, R),!,R==int.
:- end_tests('tp mono').
:- begin_tests('tp poly').
test(poly1) :- tp1(let id=λ(x,x); id, R),!,R= ∀(x1,[],(x1->x1)).
test(poly_id_app) :- tp1(let id=λ(x,x); id$id, R),!,R= ∀(x2,[],(x2->x2)).
test(poly_id_app2) :- tp1(let id=λ(x,x); (id$id)$ 1, R),!,R==int.
:- end_tests('tp poly').
:- begin_tests('type constructor').
test(con1) :- tp3([(a, int)], a, int).
test(con2) :- tp3([(a, float)], a, float).
test(con3) :- tp3([('MkPoint', float)], 'MkPoint',float).
test(con4) :- tp3([('MkPoint', (float->float->point))], 'MkPoint',(float->float->point)).
test(con5) :- Point= 'MkPoint'!float,
tp3(
[('MkPoint', (float->Point))],
'MkPoint' $ 2.0,R),!,R=='MkPoint'!float.
test(con6) :- Point='MkPoint'!(float,float),tp3(
[('MkPoint', (float->float->Point))],
'MkPoint' $ 2.0 $ 3.0,R),!,R='MkPoint'!(float,float).
test(con7) :- Point='MkPoint'!(float,float),tp3(
[('MkPoint', (float->float->Point))],
let p= 'MkPoint' $ 2.0$ 3.0; p,
R),!,R='MkPoint'!(float,float).
test(con8) :- Point='MkPoint'!(float,float),tp3(
[('MkPoint', (float->float->Point)),
(pt1, (Point->float)),
(pt2, (Point->float)),
('+', (float->float->float))],
let p= 'MkPoint' $ 2.0$ 3.0; '+'$(pt1 $p)$(pt2 $p),
float).
:- end_tests('type constructor').
:- begin_tests('tp inst1').
test(inst0) :- tpp(
class P:T2 where inc:(P->P);
1
,R),!,R= int,dim([T2]).
test(inst1) :- tpp(
class P:T2 where inc:(P->P);
inst k!int:T2 where inc= λ(x,x);
1
,R),!,R= int.
% test(h) :- halt.
test(inst2_a) :- tpp(
val k: (int->(k!int));
class P:T2 where inc:(P->P);
inst k!int:T2 where inc = λ(x,x);
k $ 1
,R),!,R==k!int.
test(inst2) :- tpp(
val k: (int->(k!int));
class P:T2 where inc:(P->P);
inst k!int:T2 where inc = λ(x,x);
inc $ (k $ 1)
,R),!,R=(k!int).
test(instk2i) :- tpp(
val k: (int->(k!int));
val k2i: ((k!int)->int);
class P:T2 where inc:(P->int);
inst k!int:T2 where inc= λ(x,k2i$x);
1
,R),!,R= int.
test(inst3) :- tpp(
val f: (float -> (f!float));
class P:T2 where inc:(P->P);
inst f!float:T2 where inc = λ(x,x);
inc$(f $ 1.0)
,R),!,R==(f!float).
test(inst4) :- tpp(
val k: (int->(k!int));
val f: (float -> (f!float));
class P:T2 where inc:(P->P);
inst k!int:T2 where inc = λ(x,x);
inst f!float:T2 where inc = λ(x,x);
inc $ (f $ 1.0)
,R),!,R==(f!float).
test(inst5) :- tpp(
val k: (int->(k!int));
val k2i: ((k!int)->int);
val l: (int->(k!int));
val l2i: ((k!int)->int);
val (+): (int->int->int);
class P:ToInt where toint:(P->int);
inst k!int:ToInt where toint= λ(x,k2i$x);
inst l!int:ToInt where toint= λ(x,l2i$x);
(+)$(toint$(l$1))$(toint$(k$2))
,R),!,R== int.
:- end_tests('tp inst1').
:- begin_tests('tp dict').
test(tpp):-tpp(let a=λ(u,u);a,R),!,R= ∀(x1,[],(x1->x1)).
test(tpp):-tpp(
type Point='MkPoint'!(float,float);
val 'MkPoint' : (float->float->Point);
val ptx : (Point->float);
class P:X where xcoord:(P->float);
inst Point:X where xcoord=λ(u,ptx$u);
xcoord
,R),!,R= ∀(x3,[(x,[])],(x3->float)).
test(tpp):-tpp(
type Point = 'MkPoint'!(float,float);
val 'MkPoint' : (float->float->Point);
val ptx : (Point->float);
class P:X where xcoord:(P->float);
inst Point:X where xcoord=λ(u,ptx$u);
λ(p,xcoord)
,R),!, R= ∀(x3,[],∀(x4,[(X,[])],(x3->x4->float))).
test(tpp):-tpp(
type Point = 'MkPoint'!(float,float);
val 'MkPoint' : (float->float->Point);
val ptx : (Point->float);
class P:X where xcoord:(P->float);
inst Point:X where xcoord=λ(u,ptx$u);
let a=xcoord;
a
,R),!,R= ∀(x4,[(x,[])],(x4->float)).
test(tpp):-tpp(
type Point = 'MkPoint'!(float,float);
val 'MkPoint' : (float->float->Point);
val ptx : (Point->float);
class P:X where xcoord:(P->float);
inst Point:X where xcoord=λ(u,ptx$u);
let xx=λ(p,xcoord$p);
let p = 'MkPoint' $ 2.0 $ 3.0;
xx $ p
,R),R==float.
test(tpp):- tpp(
type Colour = 'MkColour'!(int,int,int);
type Point = 'MkPoint'!(float,float);
type CPoint = 'MkCPoint'!(float,float,Colour);
val 'MkColour' : (int->int->int->Colour);
val c1 : (Colour->int);
val c2 : (Colour->int);
val c3 : (Colour->int);
val 'MkPoint' : (float->float->Point);
val pt1 : (Point->float);
val pt2 : (Point->float);
val 'MkCPoint' : (float->float->Colour->CPoint);
val cpt1 : (CPoint->float);
val cpt2 : (CPoint->float);
val cpt3 : (CPoint->colour);
val add : (float->float->float);
val sqr : (float->float);
val sqrt : (float->float);
class P:XCoord where xcoord:(P->float);
class P2:YCoord where ycoord:(P2->float);
inst Point:XCoord where xcoord=λ(u,pt1$u);
inst Point:YCoord where ycoord=λ(u,pt2$u);
inst CPoint:XCoord where xcoord=λ(u,cpt1$u);
inst CPoint:YCoord where ycoord=λ(u,cpt2$u);
let distance=λ(p,sqrt$(add$(sqr$(xcoord$p))$(sqr$(ycoord$p))));
distance$('MkCPoint'$2.0$3.0$('MkColour'$0$0$0))
,R),!,R==float.
:- end_tests('tp dict').
:- begin_tests('tp param').
test(tpp):-tpp(
class P: Xcd!A where xcoord:(P->A);
xcoord
,R),!,
R= ∀(x0,[],∀(x1,[(Xcd,x0)],(x1->x0))).
test(tpp):-tpp(
type Point = 'MkPoint'!(float,float);
val p : Point;
val ptx : (Point->float);
class P: Xcd!A where xcoord:(P->A);
inst Point: Xcd!float where xcoord=λ(u,ptx$u);
xcoord $ p
,R),!,R==float.
test(tpp):-tpp(
type Point = 'MkPoint'!(float,float);
val p : Point;
val ptx : (Point->float);
class P: Xcd!A where xcoord:(P->A);
inst Point: Xcd!float where xcoord=λ(u,ptx$u);
let xx=λ(p,xcoord$p);
xx $ p
,R),!,R==float.
:- end_tests('tp param').
:- begin_tests('inst constrain').
test(feq) :- tpp(
type F = f!float;
val f : (float->F);
val feq : (F -> F -> int);
feq $ (f $ 1.0) $ (f $ 2.0)
,R),!,R==int.
test(class_Eq) :- tpp(
type F = f!float;
val f : (float->F);
val feq : (F -> F -> int);
class E: Eq where eq:(E->E->int);
eq
,R),!,eq=Eq,e=E, R = ∀(A,[(Eq,[])],(A->A->int)).
test(class_Member) :- tpp(
type F = f!float;
val f : (float->F);
val feq : (F -> F -> int);
class E: Eq where eq:(E->E->int);
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
eq $ (f $ 1.0) $ (f $ 2.0)
,R),!,R==(int).
test(class_Member) :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class E: Eq where eq:(E->E->int);
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
class E:Member!C where member : (E->C->int);
member
,R),!,Member=member,c=C,e=E,R= ∀(C,[],∀(E,[(member,C)],(E->C->int))).
test("Fのインスタンスがないけど、呼んでないのでセーフ?todo") :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
member
,_).
test("Fのインスタンスがないけど、1個目はセーフ") :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
member $ f1
,_).
test("Fのインスタンスがなく、順番の問題で1個目もアウト") :- \+tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (C->E->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
member $ f1
,_).
test("Fのインスタンスがないのでエラー") :- \+tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
member $ f1 $ f2
,_).
test("FのインスタンスがあるのでOK") :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
member $ f1 $ f1
,R),!,R==int.
test("Fのインスタンスは後付でも大丈夫") :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
member $ f1 $ f1
,R),!,R==int.
test("Fのeqの制約がないのでエラーになるx eqの制約を自動追加される") :- \+tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
% inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
class C:Member!E where member : (C->E->int);
inst F:Member!F where member = eq;
1
,_).
test("Fのeqの制約がないので、実装があってもエラーになるｘ自動追加でエラーにならない") :- \+tpp(
type F = f!float;
val f1 : f!float;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
class C:Member!E where member : (C->E->int);
inst F:Member!F where member = eq;
1
,_).%,R==int.
test("Fのeqの制約がないので、実装があってもエラーになるｘ自動追加でエラーにならない") :- \+tpp(
type F = f!float;
val f1 : f!float;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
class C:Member!E where member : (C->E->int);
inst F:Member!F where member = eq;
member $ f1 $ f1
,R).%,R==int.
test("Fのeqの制約を自動追加されてもされなくても実装無いからエラー") :- \+tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C:Member!E where member : (C->E->int);
inst F:Member!F where member = eq;
member $ f1 $ f1
,R),writeln(R).
test("余計にある制約") :- tpp(
type F = f!float;
val f1 : F;
val feq : (F -> F -> int);
class C: Eq where eq:(C->C->int);
class C: Eq2 where eq2:(C->C->int);
class C:Member!E where member : (E->C->int);
inst [(F,[(Eq,[]),(Eq2,[])])]=>F:Member!F where member = λ(a,λ(b,eq $ a $ b));
inst F: Eq where eq = λ(a,λ(b,feq $ a $ b));
inst F: Eq2 where eq2 = λ(a,λ(b,feq $ a $ b));
member $ f1 $ f1
,R),!,R==int.
:- end_tests('inst constrain').
% todo ペアのテスト
:- run_tests.
:- halt.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment