summary refs log tree commit diff
path: root/Main.hs
diff options
context:
space:
mode:
authortzlil <tzlils@protonmail.com>2023-07-08 02:50:40 +0300
committertzlil <tzlils@protonmail.com>2023-07-08 02:50:40 +0300
commita26d059aecabb05d9edce10e939b3b518e37cc82 (patch)
treed6cefc390aa644008134c5ec7640a6b4b9940668 /Main.hs
parent6c9359519f54d580821e04d8e416861e8bfde83a (diff)
finish untyped
Diffstat (limited to 'Main.hs')
-rw-r--r--Main.hs73
1 files changed, 0 insertions, 73 deletions
diff --git a/Main.hs b/Main.hs
deleted file mode 100644
index eccb702..0000000
--- a/Main.hs
+++ /dev/null
@@ -1,73 +0,0 @@
-{-# 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