aboutsummaryrefslogtreecommitdiff
path: root/src/Main.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Main.hs')
-rw-r--r--src/Main.hs196
1 files changed, 176 insertions, 20 deletions
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
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-18 11:42:24 +0200