diff options
Diffstat (limited to 'src/Main.hs')
| -rw-r--r-- | src/Main.hs | 29 |
1 files changed, 24 insertions, 5 deletions
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) |