抽象

abstraction.hs

{-# LANGUAGE FlexibleInstances #-}
import Control.Arrow

data Atom = S | K | I | V Char deriving Eq
infixl 5 :$
data Tree a = Leaf a | Tree a :$ Tree a

instance Show (Tree Atom) where
    showsPrec _ (Leaf S) = ("S" ++)
    showsPrec _ (Leaf K) = ("K" ++)
    showsPrec _ (Leaf I) = ("I" ++)
    showsPrec _ (Leaf (V c)) = (c :)
    showsPrec n (l :$ r)
        | n <= 10 = s
        | n >  10 = ('(' :) . s . (')' :)
        where s = showsPrec 10 l . showsPrec 11 r

foldTree :: (b -> a) -> (a -> a -> a) -> Tree b -> a
foldTree c f = go
    where
        go (Leaf a) = c a
        go (l :$ r) = go l `f` go r

prim :: (b -> a) -> (a -> a -> Tree b -> Tree b -> a) -> Tree b -> a
prim c f = go
    where
        go (Leaf a) = c a
        go (l :$ r) = f (go l) (go r) l r

elemTree :: Eq c => c -> Tree c -> Bool
elemTree v = foldTree (v ==) (||)

abstr :: Char -> Tree Atom -> Tree Atom
abstr v = prim c f
    where
        c (V x) | v == x = i
        c e = k :$ Leaf e
        f l r el er
            | elemTree (V v) (el :$ er) = s :$ l :$ r
            | otherwise = k :$ (el :$ er)

abstr' :: Char -> Tree Atom -> Tree Atom
abstr' v = fst . snd . foldTree (c &&& p d) (\a b -> (f a b, q g a b))
    where
        p h x = (h x, Leaf x)
        q h x@(_,(_,l)) y@(_,(_,r)) = (h x y, l :$ r)
        c :: Atom -> Bool
        c = (V v ==)
        d :: Atom -> Tree Atom
        d (V x) | v == x = i
        d e = k :$ Leaf e
        f :: (Bool, (Tree Atom, Tree Atom)) -> (Bool, (Tree Atom, Tree Atom)) -> Bool
        f (b1,_) (b2,_) = b1 || b2
        g :: (Bool, (Tree Atom, Tree Atom)) -> (Bool, (Tree Atom, Tree Atom)) -> Tree Atom
        g (b1,(x,l)) (b2,(y,r))
            | b1 || b2 = s :$ x :$ y
            | otherwise = k :$ (l :$ r)

eta :: Char -> Tree Atom -> Tree Atom
eta v = prim c f
    where
        c (V x) | v == x = i
        c x = k :$ Leaf x
        f _ _ l (Leaf x@(V y))
            | v == y && not (elemTree x l) = l
        f l r el er
            | elemTree (V v) (el :$ er) = s :$ l :$ r
            | otherwise = k :$ (el :$ er)

eta' :: Char -> Tree Atom -> Tree Atom
eta' v = fst . snd . foldTree (c &&& p d) (\a b -> (f a b, q g a b))
    where
        p h x = (h x, Leaf x)
        q h x@(_,(_,l)) y@(_,(_,r)) = (h x y, l :$ r)
        c :: Atom -> Bool
        c = (V v ==)
        d :: Atom -> Tree Atom
        d (V x) | v == x = i
        d e = k :$ Leaf e
        f :: (Bool, (Tree Atom, Tree Atom)) -> (Bool, (Tree Atom, Tree Atom)) -> Bool
        f (b1,_) (b2,_) = b1 || b2
        g :: (Bool, (Tree Atom, Tree Atom)) -> (Bool, (Tree Atom, Tree Atom)) -> Tree Atom
        g (b1,(x,l)) (b2,(y, Leaf (V a)))
            | v == a && not b1 = l
        g (b1,(x,l)) (b2,(y,r))
            | b1 || b2 = s :$ x :$ y
            | otherwise = k :$ (l :$ r)

s = Leaf S
k = Leaf K
i = Leaf I
v = Leaf . V