module Research where import Control.Monad.State import Data.List (intercalate) import Data.Map (Map) import qualified Data.Map as Map data T = Leaf | Stem T | Fork T T deriving (Show, Eq, Ord) apply :: T -> T -> T apply Leaf b = Stem b apply (Stem a) b = Fork a b apply (Fork Leaf a) _ = a apply (Fork (Stem a1) a2) b = apply (apply a1 b) (apply a2 b) apply (Fork (Fork a1 a2) a3) Leaf = a1 apply (Fork (Fork a1 a2) a3) (Stem u) = apply a2 u apply (Fork (Fork a1 a2) a3) (Fork u v) = apply (apply a3 u) v reduce :: T -> T reduce expr = let next = step expr in if next == expr then expr else reduce next step :: T -> T step (Fork left right) = reduce (apply (reduce left) (reduce right)) step (Stem inner) = Stem (reduce inner) step t = t -- SKI Combinators _S :: T _S = Fork (Stem (Fork Leaf Leaf)) Leaf _K :: T _K = Stem Leaf -- Identity -- We use the "point-free" style which drops a redundant node -- Full I form (SKK): Fork (Stem (Stem Leaf)) (Stem Leaf) _I :: T _I = Fork (Stem (Stem Leaf)) Leaf -- Booleans _false :: T _false = Leaf _true :: T _true = Stem Leaf _not :: T _not = Fork (Fork _true (Fork Leaf _false)) Leaf -- Marshalling ofString :: String -> T ofString str = ofList (map ofNumber (map fromEnum str)) ofNumber :: Int -> T ofNumber 0 = Leaf ofNumber n = Fork (if odd n then Stem Leaf else Leaf) (ofNumber (n `div` 2)) ofList :: [T] -> T ofList [] = Leaf ofList (x:xs) = Fork x (ofList xs) toNumber :: T -> Either String Int toNumber Leaf = Right 0 toNumber (Fork Leaf rest) = case toNumber rest of Right n -> Right (2 * n) Left err -> Left err toNumber (Fork (Stem Leaf) rest) = case toNumber rest of Right n -> Right (1 + 2 * n) Left err -> Left err toNumber _ = Left "Invalid Tree Calculus number" toString :: T -> Either String String toString tc = case toList tc of Right list -> traverse (fmap toEnum . toNumber) list Left err -> Left "Invalid Tree Calculus string" toList :: T -> Either String [T] toList Leaf = Right [] toList (Fork x rest) = case toList rest of Right xs -> Right (x : xs) Left err -> Left err toList _ = Left "Invalid Tree Calculus list" -- Utility toAscii :: T -> String toAscii tree = go tree "" True where go :: T -> String -> Bool -> String go Leaf prefix isLast = prefix ++ (if isLast then "`-- " else "|-- ") ++ "Leaf\n" go (Stem t) prefix isLast = prefix ++ (if isLast then "`-- " else "|-- ") ++ "Stem\n" ++ go t (prefix ++ (if isLast then " " else "| ")) True go (Fork left right) prefix isLast = prefix ++ (if isLast then "`-- " else "|-- ") ++ "Fork\n" ++ go left (prefix ++ (if isLast then " " else "| ")) False ++ go right (prefix ++ (if isLast then " " else "| ")) True rules :: IO () rules = putStr $ header ++ (unlines $ tcRules) ++ (unlines $ haskellRules) ++ footer where tcRules :: [String] tcRules = [ "| |" , "| ┌--------- | Tree Calculus | ---------┐ |" , "| | 1. t t a b -> a | |" , "| | 2. t (t a) b c -> a c (b c)| |" , "| | 3a. t (t a b) c t -> a | |" , "| | 3b. t (t a b) c (t u) -> b u | |" , "| | 3c. t (t a b) c (t u v) -> c u v | |" , "| └-------------------------------------┘ |" , "| |" ] haskellRules :: [String] haskellRules = [ "| ┌------------------------------ | Haskell | --------------------------------┐ |" , "| | | |" , "| | data T = Leaf | Stem T | Fork TT | |" , "| | | |" , "| | apply :: T -> T -> T | |" , "| | apply Leaf b = Stem b | |" , "| | apply (Stem a) b = Fork a b | |" , "| | apply (Fork Leaf a) _ = a | |" , "| | apply (Fork (Stem a1) a2) b = apply (apply a1 b) (apply a2 b) | |" , "| | apply (Fork (Fork a1 a2) a3) Leaf = a1 | |" , "| | apply (Fork (Fork a1 a2) a3) (Stem u) = apply a2 u | |" , "| | apply (Fork (Fork a1 a2) a3) (Fork u v) = apply (apply a3 u) v | |" , "| └---------------------------------------------------------------------------┘ |" ] header :: String header = "┌-------------------- | Rules for evaluating Tree Calculus | -------------------┐\n" footer :: String footer = "└-------------------- | Rules for evaluating Tree Calculus | -------------------┘\n"