From eacfe73f33bb4468e160266b18c4f67071f4a255 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Sat, 8 Jul 2023 07:24:56 +0300
Subject: some bugs to iron out with new normalstep

---
 Untyped.hs | 120 +++++++++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 81 insertions(+), 39 deletions(-)

diff --git a/Untyped.hs b/Untyped.hs
index 5e48ba3..ab92bdf 100644
--- a/Untyped.hs
+++ b/Untyped.hs
@@ -4,60 +4,102 @@ import Text.ParserCombinators.Parsec (many1, sepBy1, string, noneOf, char, digit
 import Prelude
 import Data.Foldable (foldl1) 
 import qualified Data.Set as Set
+import Data.Map (Map, (!?), insert, fromList, alter)
 import Control.Monad (forever, void)
 import System.IO (hFlush, stdout)
+import Control.Monad.State
 
-data Term = Var String | App Term Term | Lam String Term deriving (Eq)
+data Term = Var String | App Term Term | Lam String Term | Let String Term | Lit Int deriving (Eq)
 instance Show Term where
+    show (Lit n) = show n
     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 "."
+  void $ char '.'
   spaces
   body <- term
   return (foldr Lam body vars)
+
+elet = do
+  void $ string "let"
+  spaces
+  name <- many1 letter
+  spaces
+  void $ char '='
+  spaces
+  body <- term
+  return $ Let name body 
+
+lit = Lit <$> read <$> many1 digit
 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
+
+term :: Parser Term
+term = elet <|> lam <|> app <|> lit <|> var 
+
+newtype Env = Env (Map String Term) deriving (Show)
+
+normalstep :: Term -> State Env (Maybe Term)
+normalstep (App m n) = do
+  (Env env) <- get
+  case m of
+    Lam x m -> return $ evalState (normalstep n) (Env $ insert x m env) 
+    _ -> do 
+         m' <- normalstep m
+	 case m' of
+           Nothing -> do 
+	     n' <- normalstep n
+	     return $ App m <$> n'
+	   Just m' -> return $ Just $ App m' n
+
+normalstep (Lam x m) = do
+  (Env env) <- get
+  m' <- return $ evalState (normalstep m) (Env $ alter (const $ Just $ Var x) x env)
+  return $ Lam x <$> m'
+
+normalstep (Let s n) = do
+  (Env env) <- get
+  modify (\(Env ls) -> (Env $ alter (const $ Just n) s ls)) 
+  return Nothing
+
+normalstep (Var s) = do
+  (Env env) <- get
+  case env !? s of
+    Nothing -> error $ "unbound variable: " ++ s
+    --Nothing -> return Nothing
+    Just v@(Var s') | s == s' -> return Nothing 
+    Just term -> return $ Just $ term 
+
+normalstep n@(Lit _) = return Nothing
+
+
+eval term = do
+  env <- get
+  let (term', env') = runState (normalstep term) env
+  put env'
+  case term' of
+    Nothing -> return term
+    Just term'' -> eval term'' 
+  
+repl :: StateT Env IO ()
+repl = forever $ do
+  liftIO $ putStr "Untyped> "
+  liftIO $ hFlush stdout
+  contents <- liftIO $ getLine
+  env <- get
+  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 _ _) -> pure ()
+          _ -> liftIO $ print term'
+
+main = runStateT (repl) $ Env $ fromList []
-- 
cgit 1.4.1