Add auto command

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)