base LC, now add types

1 files changed, 73 insertions, 0 deletions

diff --git a/Main.hs b/Main.hs
new file mode 100644
index 0000000..eccb702
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+
+module Main where
+import Text.ParserCombinators.Parsec (many1, sepBy1, string, noneOf, char, digit, spaces, sepEndBy, Parser, (<|>), parse, letter)
+import Control.Monad (void)
+import Prelude
+import qualified Data.Set as Set
+data Term = Var String | App Term Term | Lam String Term deriving (Eq)
+instance Show Term where
+    show (Var x) = x
+    show (App x y) = show x ++ show y
+    show (Lam x y) = "(λ"++x++". "++show y++")"
+
+parens :: Parser a -> Parser a
+parens p = char '(' *> spaces *> p <* spaces <* char ')'
+
+var :: Parser Term
+var = Var <$> many1 letter
+
+lam :: Parser Term
+lam = Lam <$> (char 'λ' *> spaces *> (many1 letter)) <*> (spaces *> string "." *> spaces *> term)
+
+app :: Parser Term
+app = foldl1 App <$> sepBy1 (var <|> parens term) spaces
+
+term :: Parser Term
+term = lam <|> app <|> var
+
+fv :: Term -> Set.Set String
+fv (Var x) = Set.singleton x
+fv (Lam x m) = x `Set.delete` (fv m)
+fv (App m1 m2) = (fv m1) `Set.union` (fv m2)
+
+pickFresh :: Set.Set String -> String -> String
+pickFresh s = pickFresh'
+  where
+    pickFresh' n | n `Set.notMember` s = n
+    pickFresh' n = pickFresh' $ n ++ "'"
+
+subst :: Term -> String -> Term -> Term
+subst n x (Var e)
+    | x == e = n
+    | otherwise = Var e
+subst n x (App m1 m2) = App (subst n x m1) (subst n x m2)
+subst n x (Lam y m)
+    | x == y = Lam y m
+    | y `Set.notMember` (fv n) = Lam y (subst n x m)
+    | otherwise = Lam y' (subst n x (subst (Var y') y m))
+  where
+    y' = pickFresh ((fv n) `Set.union` (fv m)) y
+
+normalstep :: Term -> Maybe Term
+normalstep (App (Lam x m) n) = Just (subst n x m)
+normalstep (Lam x m) = normalstep m >>= return . Lam x
+normalstep (App m n) | normalstep m == Nothing = normalstep n >>= return . App m
+normalstep (App m n) = normalstep m >>= return . (`App` n)
+normalstep _ = Nothing
+
+repeatedly :: (a -> Maybe a) -> a -> [a]
+repeatedly f = repeatedly'
+  where
+    repeatedly' x =
+        x : case f x of
+            Nothing -> []
+            Just y -> repeatedly' y
+
+eval s = last <$> repeatedly normalstep <$> parse term "" s 
+
+main = do 
+	contents <- getContents 
+	putStrLn $ show $ eval contents