diff options
| -rw-r--r-- | Untyped.hs | 56 |
1 files 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' |