From 48d6f83c36f55471ba66281e6d9b272fb4b336f2 Mon Sep 17 00:00:00 2001 From: tomsmeding Date: Sun, 10 Mar 2019 18:26:30 +0100 Subject: Enough to prove functoriality of Parser --- src/Main.hs | 196 +++++++++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 176 insertions(+), 20 deletions(-) (limited to 'src/Main.hs') diff --git a/src/Main.hs b/src/Main.hs index fa4416f..3ed39f9 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,7 +1,9 @@ module Main where import Control.Monad +import Haskell.AST import Haskell.Env +import Haskell.Rewrite import Haskell.SimpleParser import System.Environment import System.Exit @@ -24,6 +26,179 @@ while val f = f val >>= \case whenM :: Monad m => m Bool -> m a -> m () whenM b a = b >>= \b' -> if b' then void a else return () +ifM :: Monad m => m Bool -> m a -> m a -> m a +ifM b t e = b >>= \b' -> if b' then t else e + +splitOn :: Eq a => a -> [a] -> [[a]] +splitOn _ [] = [[]] +splitOn spl (x:xs) + | x == spl = [] : splitOn spl xs + | otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs + + +data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name } + deriving (Show) + +data Context = Context { cStack :: [(Action, Env)], cBaseEnv :: Env } + deriving (Show) + +data Action = Action Cmd Name + deriving (Show) + +data Cmd = CForget + | CRewrite Name + | CBeta + | CEta + | CCase + | CCaseForce + | CEtaCase + | CCaseCase + deriving (Show) + +data UserCmd = UCCmd Cmd + | CAction Action + | CExit + | CUndo + | CShowEnv + | CUnFocus + | CFocus Name + | CLog + deriving (Show) + +instance Pretty Action where + pretty (Action cmd target) = "action " ++ target ++ " " ++ pretty cmd + +instance Pretty Cmd where + pretty CForget = "forget" + pretty (CRewrite name) = "rew " ++ name + pretty CBeta = "beta" + pretty CEta = "eta" + pretty CCase = "case" + pretty CCaseForce = "case!" + pretty CEtaCase = "etacase" + pretty CCaseCase = "casecase" + +topEnv :: Context -> Env +topEnv (Context [] env) = env +topEnv (Context ((_, env):_) _) = env + +pushCtx :: (Action, Env) -> Context -> Context +pushCtx pair ctx = ctx { cStack = pair : cStack ctx } + +apply :: Context -> Action -> Either String Context +apply ctx act@(Action cmd target) = case cmd of + CForget -> do + env' <- forget (topEnv ctx) target + return $ pushCtx (act, env') ctx + CRewrite name -> genTransform (\env -> liftM2 (,) (get env name) (get env target)) + (\(repl, expr) -> rewrite name repl expr) + CBeta -> transform betared + CEta -> transform etared + CCase -> transform (casered False) + CCaseForce -> transform (casered True) + CEtaCase -> transform etacase + CCaseCase -> transform casecase + where + transform :: (Expr -> Expr) -> Either String Context + transform = genTransform (\env -> get env target) + + genTransform :: (Env -> Either String a) -> (a -> Expr) -> Either String Context + genTransform getter f = do + expr <- normalise . f <$> getter (topEnv ctx) + env' <- reAdd (topEnv ctx) (Def target expr) + return $ pushCtx (act, env') ctx + +applyUserCmd :: AppState -> UserCmd -> IO (Either String (Maybe AppState)) +applyUserCmd appstate = \case + UCCmd cmd -> + case asFocus appstate of + Nothing -> return (Left "No focus set") + Just focus -> + case apply (asCtx appstate) (Action cmd focus) of + Left err -> return (Left err) + Right ctx -> return (Right (Just appstate { asCtx = ctx })) + CAction act -> case apply (asCtx appstate) act of + Left err -> return (Left err) + Right ctx -> return (Right (Just appstate { asCtx = ctx })) + CExit -> return (Right Nothing) + CUndo -> + let ctx = asCtx appstate + in case cStack ctx of + [] -> return (Left "Empty environment stack") + (_:stk) -> return (Right (Just appstate { asCtx = ctx { cStack = stk } })) + CShowEnv -> putStrLn (pretty (topEnv (asCtx appstate))) >> return (Right (Just appstate)) + CUnFocus -> return (Right (Just appstate { asFocus = Nothing })) + CFocus name -> if envContains (topEnv (asCtx appstate)) name + then return (Right (Just appstate { asFocus = Just name })) + else return (Left "Name doesn't exist") + CLog -> do + mapM_ (putStrLn . pretty) $ map fst (reverse $ cStack (asCtx appstate)) + return (Right (Just appstate)) + +applyUserCmds :: AppState -> [UserCmd] -> IO (Either String (Maybe AppState)) +applyUserCmds appstate [] = return (Right (Just appstate)) +applyUserCmds appstate (ucmd : ucmds) = + applyUserCmd appstate ucmd >>= \case + Left err -> return (Left err) + Right Nothing -> return (Right Nothing) + Right (Just as) -> applyUserCmds as ucmds + +interface :: AppState -> IO (Maybe AppState) +interface appstate = do + putStrLn "" + + let appstate' = case asFocus appstate of + Nothing -> appstate + Just focus -> + if envContains (topEnv (asCtx appstate)) focus + then appstate + else appstate { asFocus = Nothing } + + case asFocus appstate' of + Nothing -> return () + Just n -> + case get (topEnv (asCtx appstate')) n of + Left _ -> return () + Right expr -> putStrLn $ pretty (Def n expr) + + putStr "> " >> hFlush stdout + + ifM isEOF (return Nothing) + (getLine >>= handleInputLine appstate') + +handleInputLine :: AppState -> String -> IO (Maybe AppState) +handleInputLine appstate line = do + let phrases = map words $ splitOn ';' line + + ucmds <- case mapM parseCmd $ filter (not . null) phrases of + Left err -> putStrLn err >> return [] + Right ucmds -> return ucmds + + applyUserCmds appstate ucmds >>= \case + Left err -> putStrLn err >> return (Just appstate) + Right Nothing -> return Nothing + Right (Just as) -> return (Just as) + +parseCmd :: [String] -> Either String UserCmd +parseCmd ("action" : target : rest) = parseCmd rest >>= \case + UCCmd cmd -> Right (CAction (Action cmd target)) + _ -> Left "Invalid command within 'action'" +parseCmd ["exit"] = Right CExit +parseCmd ["undo"] = Right CUndo +parseCmd ["env"] = Right CShowEnv +parseCmd ["focus"] = Right CUnFocus +parseCmd ["focus", name] = Right (CFocus name) +parseCmd ["log"] = Right CLog +parseCmd ["forget"] = Right (UCCmd CForget) +parseCmd ["rew", func] = Right (UCCmd (CRewrite func)) +parseCmd ["beta"] = Right (UCCmd CBeta) +parseCmd ["eta"] = Right (UCCmd CEta) +parseCmd ["case"] = Right (UCCmd CCase) +parseCmd ["case!"] = Right (UCCmd CCaseForce) +parseCmd ["etacase"] = Right (UCCmd CEtaCase) +parseCmd ["casecase"] = Right (UCCmd CCaseCase) +parseCmd cmd = Left $ "Unrecognised command: " ++ show cmd + main :: IO () main = do fname <- getArgs >>= \case @@ -36,23 +211,4 @@ main = do env0 <- tryEither (envFromAST ast) print env0 - while env0 $ \env -> do - putStrLn "" - putStr "> " >> hFlush stdout - - eof <- isEOF - if eof - then return Nothing - else words <$> getLine >>= \case - [] -> return (Just env) - - ["forget", name] -> - case forget name env of - Left err -> putStrLn err >> return (Just env) - Right env' -> return (Just env') - - ["show"] -> print env >> return (Just env) - - cmd -> do - putStrLn $ "Unrecognised command: " ++ show cmd - return (Just env) + while (AppState (Context [] env0) Nothing) interface -- cgit v1.2.3-54-g00ecf