module Research where

import Data.List (intercalate)
import Control.Monad.State
import qualified Data.Map as Map
import Data.Map (Map)

data T
  = Leaf     -- t
  | Stem T   -- t t
  | Fork T T -- t a b
  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

_I :: T
_I = apply (apply _S _K) _K -- Fork (Stem (Stem Leaf)) (Stem Leaf)

-- Lambda
data Lambda
  = Var String
  | App Lambda Lambda
  | Lam String Lambda
  | TC T
  deriving (Show, Eq)

-- Booleans
_false :: T
_false = Leaf

_true :: T
_true = Stem Leaf

_not :: T
_not = Fork (Fork _true (Fork Leaf _false)) Leaf

-- Marshalling
toString :: String -> T
toString str = toList (map toNumber (map fromEnum str))

ofString :: T -> String
ofString tc = map (toEnum . ofNumber) (ofList tc)

toNumber :: Int -> T 
toNumber 0 = Leaf
toNumber n =
  Fork
    (if odd n then Stem Leaf else Leaf)
    (toNumber (n `div` 2)) 

ofNumber :: T -> Int
ofNumber Leaf = 0
ofNumber (Fork Leaf rest) = 2 * ofNumber rest
ofNumber (Fork (Stem Leaf) rest) = 1 + 2 * ofNumber rest
ofNumber _ = error "Invalid Tree Calculus number" 

toList :: [T] -> T 
toList [] = Leaf
toList (x:xs) = Fork x (toList xs)

ofList :: T -> [T]
ofList Leaf = []
ofList (Fork x rest) = x : ofList rest
ofList _ = error "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"