diff options
| -rw-r--r-- | functorproof.txt | 32 | ||||
| -rw-r--r-- | src/Main.hs | 36 |
2 files changed, 60 insertions, 8 deletions
diff --git a/functorproof.txt b/functorproof.txt new file mode 100644 index 0000000..735cbd9 --- /dev/null +++ b/functorproof.txt @@ -0,0 +1,32 @@ +action v rew fmap +action v rew id +action v rew runParser +action v rew fmapEither +action v rew fmap1st +action v repeat beta +action v case +action v rew . +action v repeat beta +action v repeat etacase +action v eta +action x rew fmap +action x rew . +action x rew runParser +action x repeat beta +action x case +action x rew fmapEither +action x repeat beta +action x rew fmap1st +action x repeat beta +action y rew fmap +action y rew . +action y rew runParser +action y rew fmapEither +action y rew fmap1st +action y repeat beta +action y repeat case +action y repeat beta +action y casecase +action y case +action y casecase +action y case diff --git a/src/Main.hs b/src/Main.hs index 3ed39f9..bdbd447 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,6 +1,7 @@ module Main where import Control.Monad +import Data.Maybe import Haskell.AST import Haskell.Env import Haskell.Rewrite @@ -53,6 +54,7 @@ data Cmd = CForget | CCaseForce | CEtaCase | CCaseCase + | CRepeat Cmd deriving (Show) data UserCmd = UCCmd Cmd @@ -77,6 +79,7 @@ instance Pretty Cmd where pretty CCaseForce = "case!" pretty CEtaCase = "etacase" pretty CCaseCase = "casecase" + pretty (CRepeat cmd) = "repeat " ++ pretty cmd topEnv :: Context -> Env topEnv (Context [] env) = env @@ -85,26 +88,39 @@ topEnv (Context ((_, env):_) _) = env pushCtx :: (Action, Env) -> Context -> Context pushCtx pair ctx = ctx { cStack = pair : cStack ctx } +exprTransformer :: Cmd -> Maybe (Expr -> Expr) +exprTransformer CBeta = Just betared +exprTransformer CEta = Just etared +exprTransformer CCase = Just (casered False) +exprTransformer CCaseForce = Just (casered True) +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 + apply :: Context -> Action -> Either String Context apply ctx act@(Action cmd target) = case cmd of CForget -> do env' <- forget (topEnv ctx) target return $ pushCtx (act, env') ctx CRewrite name -> genTransform (\env -> liftM2 (,) (get env name) (get env target)) - (\(repl, expr) -> rewrite name repl expr) - CBeta -> transform betared - CEta -> transform etared - CCase -> transform (casered False) - CCaseForce -> transform (casered True) - CEtaCase -> transform etacase - CCaseCase -> transform casecase + (\(repl, expr) -> normalise $ rewrite name repl expr) + CRepeat subcmd -> case exprTransformer subcmd of + Nothing -> Left $ "Cannot repeat '" ++ pretty 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 <- normalise . f <$> getter (topEnv ctx) + expr <- f <$> getter (topEnv ctx) env' <- reAdd (topEnv ctx) (Def target expr) return $ pushCtx (act, env') ctx @@ -197,6 +213,10 @@ parseCmd ["case"] = Right (UCCmd CCase) parseCmd ["case!"] = Right (UCCmd CCaseForce) parseCmd ["etacase"] = Right (UCCmd CEtaCase) parseCmd ["casecase"] = Right (UCCmd CCaseCase) +parseCmd ("repeat" : rest) = parseCmd rest >>= \case + UCCmd (CRepeat _) -> Left "Cannot repeat 'repeat'" + UCCmd cmd -> Right (UCCmd (CRepeat cmd)) + _ -> Left "Invalid command within 'repeat'" parseCmd cmd = Left $ "Unrecognised command: " ++ show cmd main :: IO () |