From a682b32e323d08ca91119858559beb98aabe56ce Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Wed, 12 Jul 2023 16:35:09 +0300
Subject: i think done

---
 Untyped.hs | 56 ++++++++++++++++++++++++++++++++++++++------------------
 1 file changed, 38 insertions(+), 18 deletions(-)

diff --git a/Untyped.hs b/Untyped.hs
index 523776f..0e3bd6d 100644
--- a/Untyped.hs
+++ b/Untyped.hs
@@ -7,6 +7,7 @@ import qualified Data.Set as Set
 import Data.Map (Map, (!?), insert, fromList, alter)
 import Control.Monad (forever, void)
 import System.IO (hFlush, stdout)
+import Debug.Trace (traceShowId)
 import Control.Monad.State
 
 data Term = Var String | App Term Term | Lam String Term | Let String Term | Lit Int deriving (Eq)
@@ -17,7 +18,7 @@ instance Show Term where
     show (Lam x y) = "(λ"++x++". "++show y++")"
 
 parens p = char '(' *> spaces *> p <* spaces <* char ')'
-var = Var <$> many1 letter
+var = Var <$> many1 (letter <|> oneOf "_")
 lam = do
   void $ char '\\'
   spaces
@@ -45,32 +46,52 @@ term = elet <|> lam <|> app <|> lit <|> var
 
 newtype Env = Env (Map String Term) deriving (Show)
 
+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)
+fv (Lit _) = Set.empty
+
+pickFresh :: Set.Set String -> String -> String
+pickFresh s = pickFresh'
+  where
+    pickFresh' n | n `Set.notMember` s = n
+    pickFresh' n = pickFresh' $ n ++ "'"
+
+subst n x v@(Var e) 
+  | x == e = n
+  | otherwise = v
+subst n x (App m n') = App (subst n x m) (subst n x n')
+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
+subst _ _ t = t
+
 normalstep :: Term -> State Env (Maybe Term)
 normalstep (App m n) = do
   (Env env) <- get
   case m of
-    Lam x m -> do
-      m' <- return $ evalState (normalstep m) (Env $ alter (const $ Just $ n) x env)
-      case m' of
-        Nothing -> return $ Just $ m
-	Just m' -> return $ Just $ m'
+    Lam x m -> return $ Just $ subst n x m
     _ -> do 
          m' <- normalstep m
-	 case m' of
+         case m' of
            Nothing -> do
-	     n' <- normalstep n
-	     return $ App m <$> n'
-	   Just m' -> return $ Just $ App m' n
+             n' <- normalstep n
+             return $ App m <$> n'
+           Just m' -> return $ Just $ App m' n
 
-normalstep l@(Lam x m) = do
+normalstep (Lam x m) = do
   (Env env) <- get
   --case env !? x of
   --  Nothing -> return $ Lam x <$> evalState (normalstep m) (Env $ alter (const $ Just $ Var x) x env)
   --  Just n -> return $ evalState (normalstep m) e 
   --m' <- return $ evalState (normalstep m) (Env $ alter (const $ Just $ Var x) x env)
-  m' <- return $ evalState (normalstep m) (Env $ alter (const $ Just $ Var x) x env) 
-  return $ Lam x <$> m'
-  --return Nothing
+  --m' <- return $ evalState (normalstep m) (Env $ alter (const $ Just $ Shadow x) x env) 
+  --return $ Lam x <$> m'
+  return Nothing
 
 normalstep (Let s n) = do
   (Env env) <- get
@@ -81,7 +102,6 @@ normalstep (Var s) = do
   (Env env) <- get
   case env !? s of
     Nothing -> error $ "unbound variable: " ++ s
-    Just v@(Var s') | s == s' -> return Nothing 
     Just term -> return $ Just $ term 
 
 normalstep (Lit _) = return Nothing
@@ -104,9 +124,9 @@ repl = forever $ do
   case parse term "<stdin>" contents of
     Left x -> liftIO $ print x
     Right term -> do
-        let (term', env') = runState (eval term) env
-        put env'
-	case term' of
+        let (term', Env env') = runState (eval term) env
+        put $ Env $ alter (const $ Just term') "_" $ env'
+        case term' of
           (Let _ _) -> pure ()
           _ -> liftIO $ print term'
 
-- 
cgit 1.4.1