Last active
May 7, 2020 18:36
-
-
Save hsk/29544ca4aef28c51ef817263a72123ec to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
https://letexpr.hatenablog.com/entry/2018/11/15/222959 | |
%ast | |
term ::= string | |
| bool(qual,bool) | |
| if(term, term , term) | |
| (qual, term, term) | |
| let((string, string)=term, term) | |
| λ(qual, string: ltype, term) | |
| app(term, term). | |
toplevel ::= list(string= term) . | |
%type | |
qual ::= lin | un. | |
ltype ::= bool(qual) | (qual,ltype,ltype) | (qual,ltype->ltype). | |
ctx ::= list(string:ltype). | |
*/ | |
getQual(bool(Q),Q). | |
getQual((Q,_,_),Q). | |
getQual((Q,_->_),Q). | |
containT_(un,lin):-!,fail. | |
containT_(_,_). | |
containT(Q,bool(Q_)):- containT_(Q,Q_),!. | |
containT(Q,(Q_,T1,T2)):- containT(Q_,T1),containT(Q_,T2),containT_(Q,Q_),!. | |
containT(Q,(Q_,T1->T2)):- containT(Q_,T1),containT(Q_,T2),containT_(Q,Q_),!. | |
%typecheck | |
eq(T,T):- !. | |
eq(T1,T2):- throw(typeError(T1,T2)). | |
eq_(T1,T2):- replaceUnQual(T1,T1_),replaceUnQual(T2,T2_),eq(T1_,T2_). | |
replaceUnQual(bool(_),bool). | |
replaceUnQual((_,T1_,T2_),(T1_,T2_)). | |
replaceUnQual((_,T1_->T2_),(T1_->T2_)). | |
eqConst(bool(_),bool(_)). | |
eqConst((_,_,_),(_,_,_)). | |
eqConst((_,_->_),(_,_->_)). | |
eqConst(T1,T2):- throw(typeError(T1,T2)). | |
eqCtx(Γ1,Γ2):- (length(Γ1,L),length(Γ2,L)->!;throw(ctxError)), | |
(existsCtx(Γ1,Γ2),existsCtx(Γ2,Γ1)->!;throw(ctxError)). | |
existsCtx(C1,C2):- forall(member(N:_,C2),member(N:_,C1)). | |
t(X,Γ,(VarT,Γ)):-atom(X),member(X:VarT,Γ),getQual(VarT,un),!. | |
t(X,Γ,(VarT,Γ_)):-atom(X),member(X:VarT,Γ),getQual(VarT,lin),del(X:_,Γ,Γ_),!. | |
t(X,_,_):-atom(X), throw(error(variable(X))). | |
t(bool(Qual,_),Γ,(bool(Qual),Γ)). | |
t(if(TermCond,Term1,Term2),Γ,(Term1T,Γ3)):- | |
t(TermCond,Γ,(CondT,Γ2)),t(Term1,Γ2,(Term1T,Γ3)),t(Term2,Γ2,(Term2T,Γ3_)), | |
eq_(CondT, bool(un)),eq(Term1T,Term2T),eqCtx(Γ3,Γ3_). | |
t((Qual,Term1,Term2),Γ,((Qual,Term1T,Term2T),Γ3)):- | |
t(Term1,Γ,(Term1T,Γ2)),t(Term2,Γ2,(Term2T,Γ3)), | |
(containT(Qual,Term1T),containT(Qual,Term2T)->!;throw(qualError)). | |
t(let((X,Y)=Term1,TermBody),Γ,(TermBodyT,Γ5)):- | |
t(Term1,Γ,(Term1T,Γ2)),eqConst(Term1T, (un,bool(un),bool(un))), | |
(_,XT,YT) = Term1T,t(TermBody,[(X:XT),(Y:YT)|Γ2],(TermBodyT,Γ3)),!, | |
(getQual(XT,lin),member(X:_,Γ3)->throw(unUsedError(X));!), | |
(getQual(YT,lin),member(Y:_,Γ3)->throw(unUsedError(Y));!), | |
del(X:_,Γ3,Γ4),del(Y:_,Γ4,Γ5). | |
t(app(Term1,Term2),Γ,(T12,Γ3)):- | |
t(Term1,Γ,(Term1T,Γ2)),eqConst(Term1T, (un,bool(un)->bool(un))), | |
t(Term2,Γ2,(Term2T,Γ3)),(_,T11->T12) = Term1T,eq(T11,Term2T). | |
t(λ(Qual,Name:Vtype,TermBody),Γ,((Qual,Vtype->TermBodyT),Γ3)):- | |
getQual(Vtype,Vqual),(containT(Vqual,Vtype)->!;throw(qualError)), | |
t(TermBody,[(Name:Vtype)|Γ],(TermBodyT,Γ2)), | |
(containT(Qual,TermBodyT)->!;throw(qualError)), | |
(\+((getQual(Vtype,lin),member(Name:_,Γ2)))->!;throw(unUsedError(Name))), | |
del(Name:_,Γ2,Γ3),(Qual=un->eqCtx(Γ,Γ3);!). | |
del(V,C,C_):- select(V,C,C_),!. | |
del(_,C,C). | |
% main | |
exec([],Ctx,Ctx,[]). | |
exec([N=T|Xs],Ctx,Ctx2,[(T : [(N:T_) | C])|Rs]):- | |
t(T,Ctx,(T_,C)),exec(Xs,[(N:T_) | C],L,Rs), | |
(member(N:_,C)->append(L,Ctx,Ctx2);del(N:_,L,L2),append(Ctx,L2,Ctx2)). | |
run(Top,Rs):- catch(( | |
exec(Top,[],Γ,Rs_),Rs=Rs_/Γ, | |
findall((S,X),(member(S:X,Γ),getQual(X,lin),S\=main),Unused), | |
(Unused=[]->!;Unused=[(Fst,_)|_],throw(unUsedError(Fst))) | |
),Rs,!). | |
run(Top):- run(Top,R),writeln(R). | |
:- begin_tests(lambda). | |
test(test):-run([ | |
main=λ(lin,x:bool(lin),x) | |
],[λ(lin,x:bool(lin),x):[main:(lin,bool(lin)->bool(lin))]]/[]). | |
test(app):- run([ | |
rtfn=λ(lin,x:bool(lin),λ(lin,y:(lin,bool(lin)->bool(lin)),app(y,x))), | |
main=app(app(rtfn,bool(lin,true)),λ(lin,x:bool(lin),x)) | |
],[ | |
λ(lin,x:bool(lin),λ(lin,y:(lin,bool(lin)->bool(lin)),app(y,x))): | |
[rtfn:(lin,bool(lin)->(lin,(lin,bool(lin)->bool(lin))->bool(lin)))], | |
app(app(rtfn,bool(lin,true)),λ(lin,x:bool(lin),x)): | |
[main:bool(lin)] | |
]/[]). | |
test(id):- run([ | |
id=λ(lin,x:bool(lin),x), | |
main=app(id,bool(lin,true)) | |
],[ | |
λ(lin,x:bool(lin),x):[id:(lin,bool(lin)->bool(lin))], | |
app(id,bool(lin,true)):[main:bool(lin)] | |
]/[]). | |
test(unuse):- run([ | |
f=λ(lin,x:bool(lin),bool(lin,true)), | |
main=app(f,bool(lin,true)) | |
],unUsedError(x)). | |
test(unrestricted):- run([ | |
f=λ(un,x:bool(un),x), | |
main=(lin,app(f,bool(un,true)),app(f,bool(un,true))) | |
],[ | |
λ(un,x:bool(un),x): | |
[f:(un,bool(un)->bool(un))], | |
(lin,app(f,bool(un,true)),app(f,bool(un,true))): | |
[main:(lin,bool(un),bool(un)),f:(un,bool(un)->bool(un))] | |
]/[f:(un,bool(un)->bool(un))]). | |
test(let):- run([ | |
fst=λ(lin,x:(lin,bool(un),bool(un)),let((p,q)=x,p)), | |
main=app(fst,(lin,bool(un,true),bool(un,true)))], | |
[λ(lin,x:(lin,bool(un),bool(un)),let((p,q)=x,p)):[fst:(lin,(lin,bool(un),bool(un))->bool(un))], | |
app(fst,(lin,bool(un,true),bool(un,true))):[main:bool(un)] | |
]/[]). | |
test(error_case):- run([ | |
discard= | |
λ(lin,x:bool(lin), | |
app( | |
λ(lin,f:(un,bool(un)->bool(lin)),bool(lin,true)), | |
λ(un,y:bool(un),x))), | |
main=discard], | |
qualError). | |
:- end_tests(lambda). | |
:- run_tests. | |
:- halt. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment