Pure で CCS みたいなやつ

Pure で書いてみよう第二弾。new と replication のない(!) CCS 式を実行できます。型なし Haskell みたいな書き方をしたのでとても簡単だった。やっぱり Pure を使う利点が見つからない…。

using system;
using strings;
//----------------------------------------------------------------------
// utility rules
print = puts . str;
mynot x = x == false;
concat = foldl (+) [];
concatMap f = concat . map f;
remove 0 (_:xs) = xs;
remove n (x:xs) = x : remove (n-1) xs;
mapi f xs = map f $ zip (0..#xs) xs;

splitBy f list = subSplitBy list
with
  subSplitBy [] = ([],[]);
  subSplitBy (x:xs) = if f x then (x:a,b) else (a,x:b) when
    (a,b) = subSplitBy xs
  end;
end;	   
//----------------------------------------------------------------------
isNil p = p == ();
isSend (Send _ _) = true;
isSend _          = false;
isRecv (Recv _ _) = true;
isRecv _          = false;
isTau  (Tau _)    = true;
isTau  _          = false;
isPar  (Par _)    = true;
isPar  _          = false;
//----------------------------------------------------------------------
structualCongruence (Par [()]) = ();
structualCongruence (Par procs) = Par $ betterPars + notpars
when
  (pars, notpars) = splitBy isPar procs;
  betterPars = filter (mynot.isNil) $
                 concatMap (\ (Par ps) -> ps) $
                   map structualCongruence pars;
end;
structualCongruence p = p;
//----------------------------------------------------------------------
reduction (Par ps) = concatMap communicate $ pairs ps
with
  pairs ps = subpairs ps []
  with
    subpairs [] _      = [];
    subpairs (x:xs) ys = mapi (\ (i,p) -> ((x,p), ys + remove i xs)) xs
                           + subpairs xs (ys+[x]);
  end;
  // NOTE: "(a, (b, c))" is equals to "(a,b,c)"
  communicate (Send x p1, Recv y p2, rest) =
    if x == y then [Par $ p1:p2:rest] else [];
  communicate (Recv x p1, Send y p2, rest) =
    if x == y then [Par $ p1:p2:rest] else [];
  communicate _ = [];
end;
reduction p = p;
//----------------------------------------------------------------------
labelledTransition p = chooseOne p
with
  chooseOne (Par ps)   =
    mapi (\ (i,p) -> Par [chooseOne p,  Par (remove i ps)]) ps;
  chooseOne (Send _ p) = Par [p];
  chooseOne (Recv _ p) = Par [p];
  chooseOne (Tau p)    = Par [p];
  chooseOne _          = [];
end;
//----------------------------------------------------------------------
step p = map structualCongruence (reduction p) +
         map structualCongruence (labelledTransition p);
//----------------------------------------------------------------------
proc_a = Send 1 (Send 2 ());
proc_b = Recv 1 (Recv 2 ());
proc = Par [proc_a, proc_b];