ColorAlpha.hs

{-# LANGUAGE BangPatterns #-}
import Data.Char
import Data.List
import qualified Data.Set as S
import qualified Data.Map.Strict as M
import System.Environment
import System.Exit

data L = Var !Int | Abs L | App L L

instance Show L where
    show (Var i) = showParen (i < 0 || i > 9) (shows i) ""
    show (Abs t) = "^" ++ show t
    show (App s t) = "`" ++ show s ++ show t

instance Read L where
    readsPrec _ s
        | '(':s <- s, [(n,s)] <- reads s, ')':s <- s = [(Var n,s)]
        | c:s <- s, isDigit c = [(Var (digitToInt c),s)]
        | '^':s <- s, [(t,s)] <- reads s = [(Abs t,s)]
        | '`':s <- s, [(t,s)] <- reads s, [(u,s)] <- reads s = [(App t u,s)]

-- T = label tracking provenance of subterms; M = additional dependencies
type T = [Int]
type M = [(T, T)]

data LC
    = VarC !Char T !Int
    | AbsC !Char T LC
    | AppC !Char T LC LC
    | AlphaC !Char T
    | BotC !Char T

label (VarC _ p _) = p
label (AbsC _ p _) = p
label (AppC _ p _ _) = p
label (AlphaC _ p) = p
label (BotC _ p) = p

instance Show LC where
    show (VarC c p i)   = c : show p ++ show i
    show (AbsC c p t)   = c : show p ++ "^" ++ show t
    show (AppC c p s t) = c : show p ++ "`" ++ show s ++ show t
    show (AlphaC c p)   = c : show p ++ "α"
    show (BotC c p)     = c : show p ++ "⊥"

step :: LC -> Maybe (LC, T, M)
step (VarC _ _ _)                = Nothing
step (AbsC c p t)
    | Just (t, q, m) <- step t   = Just (AbsC c p t, q, m)
    | otherwise                  = Nothing
step (AppC c p s t)
    | AbsC _ _ s <- s
    , (t, _, m) <- subst 0 0 t s = Just (t, p, ([],label t) : m)
    | Just (s, q, m) <- step s   = Just (AppC c p s t, q, m)
    | Just (t, q, m) <- step t   = Just (AppC c p s t, q, m)
    | otherwise                  = Nothing
step (AlphaC c p)                = Just (alphaC c p, p, [])

subst i n s t@(VarC c p j)
    | i == j    = (mark n s, n+1, [(n:label s, p)])
    | i < j     = (VarC c p (j-1), n, [])
    | otherwise = (t, n, [])
subst i n s (AbsC c p t)
    | (t, n, m) <- subst (i+1) n (shift i s) t
    = (AbsC c p t, n, m)
subst i n s (AppC c p t u)
    | (t, n, m1) <- subst i n s t
    , (u, n, m2) <- subst i n s u
    = (AppC c p t u, n, m1 ++ m2)
subst i n s t = (t, n, [])

mark n (VarC c p i)   = VarC c (n:p) i
mark n (AbsC c p t)   = AbsC c (n:p) (mark n t)
mark n (AppC c p t u) = AppC c (n:p) (mark n t) (mark n u)
mark n (AlphaC c p)   = AlphaC c (n:p)
mark n (BotC c p)     = BotC c (n:p)

shift i t@(VarC c p j)
    | j >= i           = VarC c p (j+1)
    | otherwise        = t
shift i (AbsC c p t)   = AbsC c p (shift (i+1) t)
shift i (AppC c p s t) = AppC c p (shift i s) (shift i t)
shift _ t              = t

alphaC c p = AbsC c (0:p) (AbsC c (1:p) (AbsC c (2:p) (AppC c (3:p) (AppC c (4:p) (VarC c (5:p) 2) (VarC c (6:p) 0)) (AppC c (7:p) (VarC c (8:p) 1) (AbsC c (9:p) (VarC c (10:p) 1))))))

mkT xs = (\(t, _, _) -> t) (go (read xs) ['a'..] 0) where
    go (App s t) xs n
        | (s, xs, n) <- go s xs n
        , (t, xs, n) <- go t xs n
        = (AppC 'z' [n] s t, xs, n+1)
    go (Var 0) (x:xs) n
        = (AlphaC x [n], xs, n+1)


combs = [("S",s), ("S1", s1), ("S2", s2), ("S3", s3), ("S4", s4), ("S5", s5),
         ("K",k), ("K1", k1), ("K2", k2), ("K3", k3), ("K4", k4),
         ("I",i), ("B", b), ("C", c), ("W", w)]
  where
    s = s1
    s1 = mkT "```0`0```00``00`00`0`0``00`0000"
    s2 = mkT "````0`````0`0`000`00`00000`0`00"
    s3 = mkT "````0```0`0``0`00`000`0000`0`00"
    s4 = mkT "````0```0``0`0`000`00`0000`0`00"
    s5 = mkT "````0````0`0`000`00``00000`0`00"

    k = k3
    k1 = mkT "````00````0`000000`00"
    k2 = mkT "```00`````0`000000`00"
    k3 = mkT "``0`00``````0`0000000"
    k4 = mkT "```0``00``0000``0`000"

    i = mkT "``0`0``0`000``0`000"
    b = mkT "``0```0`0``0`000`000`0`0`00"
    c = mkT "```0`````000``000`00`0000"
    w = mkT "``00`0``0`000"

usage = do
    putStr $ unlines
        ["Render reduction of given combinator in terms of α to normal form as HTML."
        ,""
        ,"Usage:"
        ,"    $0 [-f] S|K|I|B|C|W|S1..S5|K1..K4 > out.html"
        ,"    $0 [-f] NAME T > out.html"
        ,"where"
        ,"    -f: full reduction with unneeded subterms"
        ,"    S1..S5 are alternative encodings of S (S = S1)"
        ,"    K1..K4 are alternative encodings of K (K = S3)"
        ,"    T := 0 | `TT"]
    exitFailure

main = do
    args <- getArgs
    !(full, args) <- pure $ case args of
            "-f":args -> (True, args)
            args      -> (False, args)
    !(t, n) <- case args of
            [n] | Just t <- lookup n combs -> pure (t, take 1 n)
            [n, t] -> pure (mkT t, n)
            _ -> usage
    let clrs = ["f00","cb0","0d0","0bc","00f","c0c",
                "e50","6c0","0c6","05c","60e","e06",
                "900","660","080","066","009","606"]
    putStr $ unlines $
        ["<!doctype html>"
        ,"<html>"
        ,"<title>Reduction: " ++ n ++ " in terms of alpha</title>"
        ,"<style>"
        ,"p { margin: 0 0 0 0 }"
        ,"b { font-weight: normal }"
        ,"s, u { text-decoration: none }"
        ,"s { padding: 0 0.15em 0 0.15em }"
        ,"u + s { padding-left: 0 }"
        ,"u:hover, s:hover, u:hover ~ * { background-color: #cdf }"] ++
        ["." ++ [c] ++ " { color: #" ++ p ++ " }" | (c, p) <- zip ['a'..] clrs] ++
        [".z { color: #000 }"
        ,"</style>"]
    let post = if full then map (\(t, _, _) -> t) else clean
    putStr $ unlines $ map (\l -> "<p>" ++ render l) (post (trace (t, [], [])))

trace :: (LC,T,M) -> [(LC,T,M)]
trace c@(t, _, _) = c : case step t of Nothing -> []; Just c -> trace c

-- replace unneeded subterms in a reduction by BotC
clean :: [(LC,T,M)] -> [LC]
clean cs = map erase (map erase ts)
  where
    ts = map (\(t,_,_) -> t) cs

    deps = M.fromListWith (++) $
        [(a,[b]) | (_,_,m) <- cs, (a,b) <- m] ++ (ts >>= nest [])

    nest q (VarC c p _)   = [(p, [q])]
    nest q (AbsC c p t)   = [(p, [q])] ++ nest p t
    nest q (AppC c p t u) = [(p, [q])] ++ nest p t ++ nest p u
    nest q (AlphaC c p)   = [(p, [q])]
    nest q (BotC c p)     = [(p, [q])]

    needed = complete S.empty (S.fromList ((labels (last ts) ++ (cs >>= \(_,p,_) -> [p])) >>= tails))

    complete seen new
        | seen <- seen `S.union` new
        , next <- S.fromList (S.toList new >>= \k -> M.findWithDefault [] k deps >>= tails) `S.difference` seen
        = if S.null next then seen else complete seen next

    labels (VarC _ p _) = [p]
    labels (AbsC _ p t) = [p] ++ labels t
    labels (AppC _ p t u) = [p] ++ labels t ++ labels u
    labels (AlphaC _ p) = [p]
    labels (BotC _ p) = [p]

    erase t@(VarC c p _)
        | p `S.member` needed = t
        | otherwise           = BotC c p
    erase (AbsC c p t)
        | p `S.member` needed = AbsC c p (erase t)
        | otherwise           = BotC c p
    erase (AppC c p t u)
        | p `S.member` needed = AppC c p (erase t) (erase u)
        | otherwise           = BotC c p
    erase t@(AlphaC c p)
        | p `S.member` needed = t
        | otherwise           = BotC c p
    erase t@(BotC _ p)        = t

spanb xs = "<b>" ++ xs ++ "</b>"
spanu cs xs = "<u class=\"" ++ cs ++ "\">" ++ xs ++ "</u>"
spans cs xs = "<s class=\"" ++ cs ++ "\">" ++ xs ++ "</s>"

render (AbsC c p t) = spanb $ spanu [c] "^" ++ render t
render (AppC c p t u) = spanb $ spanu [c] "`" ++ render t ++ render u
render (VarC c p i) = spans [c] $ show i
render (AlphaC c p) = spans [c] "α"
render (BotC c p) = spans [c] "⊥"