fjv.pl

fjv.pl

:- module(fjv,[init/0,syntax/2,(<:)/2,fields/2,ftype/3,split/3,
               mtype/3,(/-)/2,okall/0,run/1]).
% ------------------------  SYNTAX  ------------------------
init :- op(920,xfx,[=>,=>*]),op(910,xfx,[/-]),
        op(501,xfx,<:),op(500,xfy,∨),op(511,yfx,#),op(510,xfx,!),
        op(1200,xfx,::=),op(650,xfx,∈),op(250,yf,*),op(999,fx,class).
:- init.
G∈{G}. G∈(G|_). G∈(_|G1):-G∈G1. G∈G.
syntax(G,E):-G=..[O|Gs],E=..[O|Es],maplist(syntax,Gs,Es),!.
syntax(G,E):-(G::=Gs),!,G1∈Gs,syntax(G1,E),!.
syntax(E*,Ls):- maplist(syntax(E),Ls).
syntax(atom,N):- atom(N).
syntax(i,I) :- integer(I).
c ::= atom. f ::= atom. x ::= atom.
l ::= class c!((f:t)*) <: c=(m*).
m ::= x!(x:t)* :t=e.
e ::= i | x | e#f | e#x!(e*) | c!(e*) | case(e)!((x:t=>e)*).
t ::= c | t∨t.
% ------------------------  SUBTYPING  ------------------------
% 構文主導部分型付け規則 S<:T 型付け規則と簡約規則で使用
  T <: T :- !.
  [T|Ts] <: [U|Us] :- !,T <: U, Ts<:Us.
  T <: U∨_ :- T <: U,!.
  T <: _∨U :- T <: U,!.
  U∨V <: T :- U <: T, V <: T,!.
  C <: E :- class C!_ <: D=_,!,D <: E.
% ------------------------  TYPING  ------------------------
% fields 型付け&簡約両方で使用
  fields(object,[]) :- !.
  fields(C,Fs_) :- class C!Fs<:D=_,!,fields(D,Us),append(Fs,Us,Fs_).
% ftype 型付け規則で使用
  ftype(Fi,C,Ti) :- fields(C,Fs),!,memberchk(Fi:Ti,Fs).
  ftype(F,T∨U, T_∨U_):- ftype(F,T,T_),ftype(F,U,U_).
% mtype 型付け規則で使用
  mtype(M,C,Us->U):- class C!_<:_=Ms,member(M!As:U=_,Ms),!,split(As,_,Us).
  mtype(M,C,Us->U):- class C!_<:D=_,!,mtype(M,D,Us->U).
  mtype(M,T_∨U_,Ts->T∨U):- mtype(M,T_,Ts->T),mtype(M,U_,Us->U),Ts<:Us,Us<:Ts.
  % フィールド内を分離
  split([],[],[]).
  split([X:Y|Ls],[X|Xs],[Y|Ys]) :- split(Ls,Xs,Ys).
% 型付け規則
  _/-[]:[] :- !.
  Γ/-[E|Es]:[T|Ts] :- Γ/-E:T,!,Γ/-Es:Ts,!.
  _/-X:string :- string(X),!.
  _/-X:int :- integer(X),!.
  _/-null:_ :- !.
  Γ/-X:T:- syntax(x,X),!,member(X:T,Γ).
  Γ/-E0#F:T:- syntax(f,F),!,Γ/-E0:T0,ftype(F,T0,T).
  Γ/-E0#M!Es:U0:- !,Γ/-E0:T0,mtype(M,T0,Us->U0),Γ/-Es:Ts,Ts<:Us.
  Γ/-case(E0)!Cs:T:- !,cnv(T,Ts),split2(Cs,Ts_),cnv(T_,Ts_),Γ/-E0:T0,T0<:T_,
                     maplist([X:T1_=>E1,T1]>>([X:T1_|Γ]/-E1:T1),Cs,Ts).
  Γ/-C!Es:C:- !,fields(C,Ufs),Γ/-Es:Ts,split(Ufs,_,Us),Ts<:Us.
  split2([],[]).
  split2([_:T=>_|Ls],[T|Ts]) :- split2(Ls,Ts).
  cnv(T,[T]) :- \+(T= _∨_),!.
  cnv(T∨S,[T|S_]) :- !,cnv(S,S_).

% メソッドの型付け
  ok_as(C,M!As:T=E) :- [this:C|As]/-E:V,V<:T,class C!_<:D=_,
                       (mtype(M,D,Us->U)->split(As,_,Ts),Us=Ts,U=T;!).
% クラスの型付け ok(C)
  ok(class C!_<:_=Ms):- maplist(ok_as(C),Ms),!.
  ok(class C!_<:_=_) :- format('error class ~w\n',[C]),fail.
  okall :- forall(class(C!Fs<:D=Ms),ok(class(C!Fs<:D=Ms))),!.
% ------------------------  EVALUATION  ------------------------
% mbody 簡約規則で使用
  mbody(M,C,Xs#E):- class C!_<:_=Ms,member(M!As:_=E,Ms),!,split(As,Xs,_).
  mbody(M,C,Xs#E):- class C!_<:D=_,!,mbody(M,D,Xs#E).
% 置換
  s([],T,T).
  s([S/D|DSs],T,T_) :- s(S/D,T,T1),s(DSs,T1,T_).
  s(S/D,D,S) :- atom(D).
  s(_/_,X,X) :- atom(X);integer(X);string(X).
  s(_/_,[],[]).
  s(S/D,[X|Xs],[X_|Xs_]) :- s(S/D,X,X_),s(S/D,Xs,Xs_).
  s(S/D,T#M!Ts,T_#M!Ts_) :- s(S/D,T,T_),s(S/D,Ts,Ts_).
  s(S/D,T#F,T_#F) :- s(S/D,T,T_).
  s(_/D,D:T=>E,D:T=>E).
  s(S/D,X:T=>E,X:T=>E_) :- s(S/D,E,E_).
  s(S/D,case(E)!Es,case(E_)!Es_) :- s(S/D,[E|Es],[E_|Es_]).
  s(S/D,C!Ts,C!Ts_) :- s(S/D,Ts,Ts_).
  s(S/D,E,_) :- writeln(error:s(S/D,E)),fail.
% 簡約規則
  case(C!Ds)![X:T=>E|_]=>E_:- C<:T,!,s([(C!Ds)/X],E,E_).
  case(C!Ds)![_|Cs]=>E:- case(C!Ds)!Cs=>E.
  case(E)!Cs=>case(E_)!Cs :- E=>E_,!.
  C!Es#Fi=>Ei:- fields(C,Fs),nth0(I,Fs,Fi:_),nth0(I,Es,Ei).
  C!Es#M!Ds=>E0_:- mbody(M,C,Xs#E0),s([Ds/Xs,(C!Es)/this],E0,E0_).
  E#F => E_#F :- E=>E_,!.
  E1 =>* E3 :- E1=>E2,!,E2 =>* E3.
  E1 =>* E1.
  run(E:T=>V) :- syntax(e,E),[]/-E:T,!,E=>*V1,!,V=V1.

fjv_test.pl

:- use_module(fjv).
:- init.
% 例
term_expansion(class A!B<:C=D,class A!B<:C=D).
term_expansion(class A!B=D,class A!B<:object=D).
term_expansion(class A!B<:C,class A!B<:C=[]).
term_expansion(class A!B,class A!B<:object=[]).
term_expansion(class A<:C=D,class A![]<:C=D).
term_expansion(class A=D,class A![]<:object=D).
term_expansion(class A<:C,class A![]<:C=[]).
term_expansion(class A,class A![]<:object=[]).

class integer![i:int].

class c.
class a <: c = [
  m![]:integer = integer![10]
].
class b <: c = [
  m![]:string = "foo"
].
class list![car:a∨b,cdr:list].
class ca <: a.
class cb <: b.
class l1![f:a].
class l2![a:a,f:l2].
class l3 = [
  m![i:int,s:string]:integer = integer![i]
].
l(list![a![],list![b![],null]]).

:- begin_tests(syntax).
  test(l1) :- syntax(l,class x![]<:x = []).
  test(l2) :- syntax(l,class x![a:int,b:int]<:x = []).
  test(m1) :- syntax(l,class x![]<:x = [m![]:int=1]).
  test(e1) :- syntax(e,1).
  test(e2) :- syntax(e,x).
  test(e3) :- syntax(e,x#f).
  test(e4) :- syntax(e,x#m![1,2]).
  test(e5) :- syntax(e,hoge![1,2]).
  test(t1) :- syntax(t,x).
  test(t1) :- syntax(t,a∨b).
  test(t1) :- syntax(t,a∨b∨c).
:- end_tests(syntax).
:-begin_tests(subtype).
  test(sub1) :- t <: t.
  test(sub1) :- c <: object.
  test(sub1) :- a <: object.
  test(sub1) :- b <: object.
  test(sub1) :- a <: c.
  test(sub1) :- b <: c.
  test(sub1) :- x <: x∨y.
  test(sub1) :- y <: x∨y.
  test(sub1) :- x <: x∨y∨z.
  test(sub1) :- y <: x∨y∨z.
  test(sub1) :- z <: x∨y∨z.
  test(sub1) :- x∨z <: x∨z.
  test(sub1) :- z∨x <: x∨z.
  test(sub1) :- x∨z <: x∨y∨z.
:-end_tests(subtype).
:- begin_tests(typing_subrutine).
  test(fields_object) :- fields(object,[]).
  test(fields_list) :- fields(list,[car:a∨b,cdr:list]).
  test(ftype) :- ftype(car,list, a∨b).
  test(ftype) :- ftype(car,list∨list, (a∨b)∨(a∨b)).
  test(ftype) :- ftype(cdr,list, list).
  test(ftype) :- ftype(cdr,list∨list, list∨list).
:- end_tests(typing_subrutine).
:- begin_tests(typing_mtype).
  test(split) :- split([],[],[]).
  test(split2) :- split([x:int,y:int],[x,y],[int,int]).
  test(mtype) :- mtype(m,a, []->integer).
  test(mtype) :- mtype(m,b, []->string).
  test(mtype) :- mtype(m,l3, [int,string]->integer).
  test(mtype_parent) :- mtype(m,ca, []->integer).
  test(mtype_parent) :- mtype(m,cb, []->string).
:- end_tests(typing_mtype).
:- begin_tests(typing_e).
  test(x) :- [x:int]/-x:int.
  test(a) :- []/-a![]:a.
  test(null) :- []/-null:list.
  test(integer) :- []/-integer![1]:integer.
  test(l) :- []/-l1![a![]]:l1.
  test(l) :- []/-l1![null]:l1.
  test(l2) :- []/-l2![null,null]:l2.
  test(l2) :- []/-l2![a![],null]:l2.
  test(l2) :- []/-l2![a![],l2![a![],null]]:l2.
  test(list) :- []/-list![a![],null]:list.
  test(list_car) :- []/-list![a![],null]#car:a∨b.
  test(a_m) :- []/-a![]#m![]:integer.
  test(b_m) :- []/-b![]#m![]:string.
  test(case) :- l(L),[]/-case(L#car)![x:a=>x#m![],y:b=>y#m![]]:integer∨string.
:- end_tests(typing_e).
:- begin_tests(typing_class).
  test(all) :- okall.
:- end_tests(typing_class).
:- begin_tests(eval).
  test(a):- run(a![]:a=>a![]).
  test(a):- run(a![]#m![]:integer=>integer![10]).
  test(l):- run(l1![a![]]:l1 => l1![a![]]).
  test(l):- run(l1![a![]]#f:a => a![]).
  test(l0):- l(L),run(L:list=> L).
  test(l1):- l(L),run(L#car:a∨b=>a![]).
  test(c0):- run(case(a![])![x:a=>x#m![],y:b=>y#m![]]:integer∨string=>integer![10]).
  test(c1):- l(L),run(case(L#car)![x:a=>x#m![],y:b=>y#m![]]:integer∨string=>integer![10]).
  test(c2):- l(L),run(case(L#cdr#car)![x:a=>x#m![],y:b=>y#m![]]:integer∨string=>"foo").
  test(c3):- l(L),run(L#car#m![]:integer∨string=>integer![10]).
:- end_tests(eval).
:- run_tests.
:- halt.