Initialize Repo

Working (but likely buggy!) lexing, parsing, and evaluation of Tree Calculus terms

src/Research.hs

@@ -0,0 +1,142 @@
+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"