linier.pl

/*
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.