define syntax on prolog

arith.pl

:- op(1200, xfx, ['--', where, ::=]).
:- op(920, xfx, ['==>', '==>>']).

term_expansion((A where B), (A :- B)).

% 構文

zip([], [], []).
zip([L|Ls], [R|Rs], [(L,R)|Ps]) :- zip(Ls, Rs, Ps).

% 再帰的チェックのおまじない
call2([],[]) :- !.
call2([F|Fs],[M|Ms]) :- !,call2(F,M),call2(Fs,Ms).
call2(X,M) :- atom(X),call(X,M).
call2(F,M) :- F=..[O|Fs],M=..[O|Ms], call2(Fs,Ms).

% 述語作成
addm(A,M,L) :- var(A), L =.. [call2,A|M].
addm(A,M,L) :- atom(A), L =.. [A|M].
addm(A,M,L) :- A=..[B|Bs],var(B),append([match,B|Bs],M,R), L =.. R.
addm(A,M,L) :- A=..B,append(B,M,R), L =.. R.

syntax_expansion(A::=B,A_ :- B_) :-
  addm(A,[M],A_), syntax_expansion2(M,B,B_) .

% (a|b) -> (a;b)にする
syntax_expansion2(M,(B|Bs),(B_;Bs_)) :-
  syntax_expansion2(M,B,B_),
  syntax_expansion2(M,Bs,Bs_).

% 個別のデータが複合項の場合
syntax_expansion2(M,A,B_) :-
  A =..[A_|Ps], % パラメータを取り出し
  maplist([B1,(K,BB)]>>addm(B1,[K],BB), Ps,Ps_), % パラメータごとに追加する変数を作成
  zip(L,R,Ps_), % 引数入りのものと、そうでないものを分離
  addm(A_,L,B),
  R2=[M=B|R],
  reverse(R2,[RA|R3]),
  foldl([AA,BB,(AA,BB)]>>!,R3,RA,B_).
% 個別のデータが複合項ではない場合
syntax_expansion2(M,A,M=A).

term_expansion((A::=B),R) :- syntax_expansion((A::=B),R)/*,writeln(R)*/.

list(A) ::= [] | [A|list(A)].
option(A) ::= none | some(A).

m ::=
    true
  | false
  | if(m,m,m)
  | 0
  | succ(m)
  | pred(m)
  | iszero(m)
  | op(option(m))
  | record(list(atom))
  | record2(list(m))
  | record3(list(atom:m))
  | record4(list(atom=m))
  | atom->m
  | (fn(atom)->m)
  .

:- m(op(some(true))).
:- m(record([a,b,c])).
:- m(record2([true,false])).
:- m(record3([a:true,b:false])).
:- m(record3([a:true,b=false])).
:- m(record4([a=true,b=false])).
:- m(x->true).
:- m(fn(x)->true).
/*
m(M) :-                                           % 項:
        M = true                                  % 定数真
      ; M = false                                 % 定数偽
      ; M = if(M1, M2, M3), m(M1), m(M2), m(M3)   % 条件式
      ; M = 0                                     % 定数ゼロ
      ; M = succ(M1), m(M1)                       % 後者値
      ; M = pred(M1), m(M1)                       % 前者値
      ; M = iszero(M1), m(M1)                     % ゼロ判定
      .
*/
n(N) :-                                           % 数値:
        N = 0                                     % ゼロ
      ; N = succ(N1), n(N1)                       % 後者値
      .
v(V) :-                                           % 値:
        V = true                                  % 定数真
      ; V = false                                 % 定数偽
      ; V = NV, n(NV)                             % 数値
      .

% 評価 M ==> M_

if(true, M2, _)  ==> M2.
if(false, _, M3) ==> M3.
if(M1, M2, M3)   ==> if(M1_, M2, M3) where M1 ==> M1_.
succ(M1)         ==> succ(M1_)       where M1 ==> M1_.
pred(0)          ==> 0.
pred(succ(N1))   ==> N1              where n(N1).
pred(M1)         ==> pred(M1_)       where M1 ==> M1_.
iszero(0)        ==> true.
iszero(succ(N1)) ==> false           where n(N1).
iszero(M1)       ==> iszero(M1_)     where M1 ==> M1_.

M               ==>> M_              where M  ==> M1, M1 ==>> M_.
M               ==>> M.

run(eval(M), Γ, Γ) :- !, m(M), !, M ==>> M_, !, writeln(M_).
run(Ls)            :- foldl(run, Ls, [], _).

:- run([eval(true)]).
:- run([eval(if(false, true, false))]).
:- run([eval(0)]).
:- run([eval(succ(pred(0)))]).
:- run([eval(iszero(pred(succ(succ(0)))))]).
:- run([eval(iszero(pred(pred(succ(succ(0))))))]).
:- run([eval(iszero(0))]).
:- run([eval(if(0, succ(pred(0)), 0))]).
:- run([eval(if(0, succ(succ(0)), 0))]).
:- run([eval(if(0, succ(pred(succ(0))), 0))]).
:- run([eval(hoge)]).
:- halt.