From a26d059aecabb05d9edce10e939b3b518e37cc82 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Sat, 8 Jul 2023 02:50:40 +0300
Subject: finish untyped

---
 Main.hs    | 73 --------------------------------------------------------------
 Untyped.hs | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 73 deletions(-)
 delete mode 100644 Main.hs
 create mode 100644 Untyped.hs

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
diff --git a/Untyped.hs b/Untyped.hs
new file mode 100644
index 0000000..5e48ba3
--- /dev/null
+++ b/Untyped.hs
@@ -0,0 +1,63 @@
+module Main where
+import Text.ParserCombinators.Parsec (many1, sepBy1, string, noneOf, char, digit, spaces, sepEndBy, Parser, (<|>), parse, letter, oneOf)
+--import Relude hiding ((<|>))
+import Prelude
+import Data.Foldable (foldl1) 
+import qualified Data.Set as Set
+import Control.Monad (forever, void)
+import System.IO (hFlush, stdout)
+
+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 p = char '(' *> spaces *> p <* spaces <* char ')'
+var = Var <$> many1 letter
+lam = do
+  void $ char '\\'
+  spaces
+  vars <- many1 $ (many1 letter) <* spaces
+  void $ string "."
+  spaces
+  body <- term
+  return (foldr Lam body vars)
+app = foldl1 App <$> sepBy1 (var <|> parens term) spaces
+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 n | n `Set.notMember` s = n
+pickFresh s n = pickFresh s $ n <> "'"
+
+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 l@(Lam y m)
+    | x == y = l
+    | 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 (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 f x = maybe x (repeatedly f) (f x)
+eval = (repeatedly normalstep <$>) . parse term "<stdin>" 
+
+main = forever $ do 
+  putStr "Untyped> "
+  hFlush stdout
+  contents <- getLine 
+  putStrLn $ (either show show . eval) contents
-- 
cgit 1.4.1