From 57ac7ed93d048397b36e53d50db6d328e31bd2cc Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 8 Apr 2019 22:25:40 +0200 Subject: Add auto command --- src/Haskell/Rewrite.hs | 15 ++++++++- src/Main.hs | 89 ++++++++++++++++++++++++++++++++++---------------- 2 files changed, 74 insertions(+), 30 deletions(-) diff --git a/src/Haskell/Rewrite.hs b/src/Haskell/Rewrite.hs index d53eb6f..c33f62e 100644 --- a/src/Haskell/Rewrite.hs +++ b/src/Haskell/Rewrite.hs @@ -2,7 +2,9 @@ module Haskell.Rewrite (rewrite ,betared, etared, casered ,etacase, casecase - ,normalise) where + ,autoSimp + ,normalise + ,fixpoint) where import Control.Monad import Data.List @@ -61,6 +63,11 @@ casecase (Case (Case subj arms1) arms2) = Case subj [(p, Case e arms2) | (p, e) <- arms1] casecase e = recurse id casecase e +autoSimp :: Expr -> Expr +autoSimp expr = + let steps = [betared, casered False, etared, etacase, casecase] + in fixpoint (normalise . foldl1 (.) (intersperse normalise steps)) expr + eqPE :: Pat -> Expr -> Bool eqPE pat expr = case unify pat expr of Nothing -> False @@ -98,3 +105,9 @@ recurse _ _ (Num k) = Num k recurse _ f (Tup es) = Tup (map f es) recurse _ f (Lam ns e) = Lam ns (f e) recurse fp f (Case e as) = Case (f e) (map (\(p, e') -> (fp p, f e')) as) + +fixpoint :: Eq a => (a -> a) -> a -> a +fixpoint f initVal = + let values = iterate f initVal + pairs = zip values (tail values) + in fst . head $ dropWhile (uncurry (/=)) pairs diff --git a/src/Main.hs b/src/Main.hs index faf21f7..460e2ab 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,6 +1,7 @@ module Main where import Control.Monad +import Data.List import Data.Maybe import Haskell.AST import Haskell.Env @@ -20,6 +21,10 @@ tryEither' :: Show e => Either e a -> IO a tryEither' (Left err) = die (show err) tryEither' (Right x) = return x +fromRight :: Either a b -> b +fromRight (Right x) = x +fromRight _ = error "fromRight on Left" + while :: Monad m => a -> (a -> m (Maybe a)) -> m () while val f = f val >>= \case Nothing -> return () @@ -48,6 +53,7 @@ usageString = \ focus -- Unfocus currently focused variable\n\ \ log -- Print list of commands that reproduces current environment\n\ \ help -- Show this help\n\ + \ auto -- Try to simplify the currently focused expression as far as possible\n\ \\n\ \\x1B[1mExpression rewrite commands\x1B[0m\n\ \These commands operate on the currently-focused expression.\n\ @@ -86,6 +92,7 @@ data Cmd = CRewrite Name data UserCmd = UCCmd Cmd | CAction Action + | CAuto | CExit | CUndo | CShowEnv @@ -124,29 +131,34 @@ exprTransformer CEtaCase = Just etacase exprTransformer CCaseCase = Just casecase exprTransformer _ = Nothing -repeatTrans :: (Expr -> Expr) -> Expr -> Expr -repeatTrans f expr = - let values = iterate f expr - pairs = zip values (tail values) - in fst . head $ dropWhile (uncurry (/=)) pairs +ctxTransform :: Context -> Action -> (Expr -> Expr) -> Either String Context +ctxTransform ctx act@(Action _ target) = generalCtxTransform ctx act (\env -> get env target) + +generalCtxTransform :: Context -> Action -> (Env -> Either String a) -> (a -> Expr) -> Either String Context +generalCtxTransform ctx act@(Action _ target) getter f = do + expr <- f <$> getter (topEnv ctx) + env' <- reAdd (topEnv ctx) (Def target expr) + return $ pushCtx (act, env') ctx apply :: Context -> Action -> Either String Context apply ctx act@(Action cmd target) = case cmd of - CRewrite name -> genTransform (\env -> liftM2 (,) (get env name) (get env target)) - (\(repl, expr) -> normalise $ rewrite name repl expr) - CRepeat subcmd -> case exprTransformer subcmd of - Nothing -> Left $ "Cannot repeat '" ++ pprint 80 subcmd ++ "'" - Just trans -> transform (repeatTrans (normalise . trans)) - _ -> transform (normalise . fromJust (exprTransformer cmd)) - 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 <- f <$> getter (topEnv ctx) - env' <- reAdd (topEnv ctx) (Def target expr) - return $ pushCtx (act, env') ctx + CRewrite name -> + generalCtxTransform + ctx act + (\env -> liftM2 (,) (get env name) (get env target)) + (\(repl, expr) -> normalise $ rewrite name repl expr) + CRepeat subcmd -> + case exprTransformer subcmd of + Nothing -> Left $ "Cannot repeat '" ++ pprint 80 subcmd ++ "'" + Just trans -> ctxTransform ctx act (fixpoint (normalise . trans)) + _ -> + ctxTransform ctx act (normalise . fromJust (exprTransformer cmd)) + +findChangingTransformer :: Expr -> Maybe Cmd +findChangingTransformer expr = + let opts = [CBeta, CEta, CCase, CEtaCase, CCaseCase] + results = [(cmd, normalise $ fromJust (exprTransformer cmd) expr) | cmd <- opts] + in fst <$> find (\(_, res) -> res /= expr) results applyUserCmd :: AppState -> UserCmd -> IO (Either String (Maybe AppState)) applyUserCmd appstate = \case @@ -157,24 +169,42 @@ applyUserCmd appstate = \case 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) + CAction act -> + case apply (asCtx appstate) act of + Left err -> return (Left err) + Right ctx -> return (Right (Just appstate { asCtx = ctx })) + CAuto -> + case asFocus appstate of + Nothing -> return (Left "No focus set") + Just focus -> + let nextStep ctx = case findChangingTransformer (fromRight (get (topEnv ctx) focus)) of + Nothing -> Right ctx + Just cmd -> case ctxTransform ctx (Action cmd focus) (normalise . fromJust (exprTransformer cmd)) of + Left err -> Left err + Right ctx' -> nextStep ctx' + in case nextStep (asCtx appstate) of + Left err -> return (Left err) Right ctx -> return (Right (Just appstate { asCtx = ctx })) - CExit -> return (Right Nothing) + 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 (pprint 80 (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") + CShowEnv -> + putStrLn (pprint 80 (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 . pprint 80) $ map fst (reverse $ cStack (asCtx appstate)) return (Right (Just appstate)) - CHelp -> putStrLn usageString >> return (Right (Just appstate)) + CHelp -> + putStrLn usageString >> return (Right (Just appstate)) applyUserCmds :: AppState -> [UserCmd] -> IO (Either String (Maybe AppState)) applyUserCmds appstate [] = return (Right (Just appstate)) @@ -231,6 +261,7 @@ parseCmd ["focus"] = Right CUnFocus parseCmd ["focus", name] = Right (CFocus name) parseCmd ["log"] = Right CLog parseCmd ["help"] = Right CHelp +parseCmd ["auto"] = Right CAuto parseCmd ["rew", func] = Right (UCCmd (CRewrite func)) parseCmd ["beta"] = Right (UCCmd CBeta) parseCmd ["eta"] = Right (UCCmd CEta) -- cgit v1.2.3