aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTom Smeding <tom.smeding@gmail.com>2019-04-08 22:25:40 +0200
committerTom Smeding <tom.smeding@gmail.com>2019-04-08 22:25:40 +0200
commit57ac7ed93d048397b36e53d50db6d328e31bd2cc (patch)
tree9d415443980da7efdda0f23d92c9d06138c1a603 /src
parent04cf7ed628e840839e08f0d3c7e624200ded81b3 (diff)
Add auto command
Diffstat (limited to 'src')
-rw-r--r--src/Haskell/Rewrite.hs15
-rw-r--r--src/Main.hs89
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)