From 8f742dc39085ebd15848ab32662239e8562a430c Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom.smeding@gmail.com>
Date: Mon, 8 Apr 2019 22:57:10 +0200
Subject: Add rewall command

---
 src/Haskell/AST.hs | 30 ++++++++++++++++++++++++++----
 src/Main.hs        | 29 ++++++++++++++++++++++++-----
 2 files changed, 50 insertions(+), 9 deletions(-)

diff --git a/src/Haskell/AST.hs b/src/Haskell/AST.hs
index 1e181e2..f8b5c72 100644
--- a/src/Haskell/AST.hs
+++ b/src/Haskell/AST.hs
@@ -105,7 +105,29 @@ instance Pretty Inst where
     pretty (Inst n t ds) = Node ("instance " ++ n ++ " " ++ pprintOneline t ++ " where") [Bracket "{" "}" ";" (map pretty ds)]
 
 
-mapInit :: (a -> a) -> [a] -> [a]
-mapInit _ [] = []
-mapInit _ [x] = [x]
-mapInit f (x:y:zs) = f x : mapInit f (y:zs)
+class AllRefs a where
+    allRefs :: a -> [Name]
+
+instance AllRefs AST where
+    allRefs (AST tops) = nub $ concatMap allRefs tops
+
+instance AllRefs Toplevel where
+    allRefs (TopDef def) = allRefs def
+    allRefs (TopDecl _) = []
+    allRefs (TopData _) = []
+    allRefs (TopClass _) = []
+    allRefs (TopInst inst) = allRefs inst
+
+instance AllRefs Def where
+    allRefs (Def _ e) = allRefs e
+
+instance AllRefs Expr where
+    allRefs (App e es) = nub $ concatMap allRefs (e : es)
+    allRefs (Ref n) = [n]
+    allRefs (Num _) = []
+    allRefs (Tup es) = nub $ concatMap allRefs es
+    allRefs (Lam ns e) = allRefs e \\ ns
+    allRefs (Case e pairs) = nub $ allRefs e ++ concatMap (allRefs . snd) pairs
+
+instance AllRefs Inst where
+    allRefs (Inst _ _ ds) = nub $ concatMap allRefs ds
diff --git a/src/Main.hs b/src/Main.hs
index 460e2ab..6dfbef5 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -23,7 +23,11 @@ tryEither' (Right x) = return x
 
 fromRight :: Either a b -> b
 fromRight (Right x) = x
-fromRight _ = error "fromRight on Left"
+fromRight (Left _) = error "fromRight on Left"
+
+isRight :: Either a b -> Bool
+isRight (Right _) = True
+isRight (Left _) = False
 
 while :: Monad m => a -> (a -> m (Maybe a)) -> m ()
 while val f = f val >>= \case
@@ -54,6 +58,7 @@ usageString =
     \  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\
+    \  rewall       -- Rewrite as much as possible, but each name at most once\n\
     \\n\
     \\x1B[1mExpression rewrite commands\x1B[0m\n\
     \These commands operate on the currently-focused expression.\n\
@@ -93,6 +98,7 @@ data Cmd = CRewrite Name
 data UserCmd = UCCmd Cmd
              | CAction Action
              | CAuto
+             | CRewriteAll
              | CExit
              | CUndo
              | CShowEnv
@@ -179,12 +185,24 @@ applyUserCmd appstate = \case
             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
+                        Just cmd -> case apply ctx (Action cmd focus) 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 }))
+                in return $ fmap (\ctx -> Just appstate { asCtx = ctx }) $ nextStep (asCtx appstate)
+    CRewriteAll ->
+        case asFocus appstate of
+            Nothing -> return (Left "No focus set")
+            Just focus ->
+                let nextStep ctx done =
+                        let orig = fromRight (get (topEnv ctx) focus)
+                        in case filter (isRight . get (topEnv ctx)) $ allRefs orig \\ done of
+                            [] -> Right ctx
+                            (name:_) -> case apply ctx (Action (CRewrite name) focus) of
+                                Left err   -> Left ("Error rewriting '" ++ name ++ "': " ++ err)
+                                Right ctx' ->
+                                    let newexpr = fromRight (get (topEnv ctx') focus)
+                                    in nextStep (if newexpr /= orig then ctx' else ctx) (name : done)
+                in return $ fmap (\ctx -> Just appstate { asCtx = ctx }) $ nextStep (asCtx appstate) []
     CExit ->
         return (Right Nothing)
     CUndo ->
@@ -262,6 +280,7 @@ parseCmd ["focus", name] = Right (CFocus name)
 parseCmd ["log"] = Right CLog
 parseCmd ["help"] = Right CHelp
 parseCmd ["auto"] = Right CAuto
+parseCmd ["rewall"] = Right CRewriteAll
 parseCmd ["rew", func] = Right (UCCmd (CRewrite func))
 parseCmd ["beta"] = Right (UCCmd CBeta)
 parseCmd ["eta"] = Right (UCCmd CEta)
-- 
cgit v1.2.3