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];