From 573967434a8b1cb14ee7de43ec11bd616cf568c6 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Tue, 9 Apr 2019 23:30:08 +0200 Subject: Organisation cleanup --- src/Haskell/Env/Cmd.hs | 48 +++++++++++++++++++++++ src/Haskell/Env/Context.hs | 15 ++++++++ src/Haskell/Rewrite.hs | 10 +---- src/Main.hs | 96 ++++------------------------------------------ src/Util.hs | 44 +++++++++++++++++++++ verify-hs.cabal | 3 ++ 6 files changed, 120 insertions(+), 96 deletions(-) create mode 100644 src/Haskell/Env/Cmd.hs create mode 100644 src/Haskell/Env/Context.hs create mode 100644 src/Util.hs diff --git a/src/Haskell/Env/Cmd.hs b/src/Haskell/Env/Cmd.hs new file mode 100644 index 0000000..35a6542 --- /dev/null +++ b/src/Haskell/Env/Cmd.hs @@ -0,0 +1,48 @@ +module Haskell.Env.Cmd where + +import Haskell.AST +import Haskell.Rewrite +import Pretty +import Util + + +data Action = Action RewCmd Name + deriving (Show) + +data RewCmd = CRewrite Name + | CBeta + | CEta + | CCase + | CCaseForce + | CEtaCase + | CCaseCase + | CRepeat RewCmd + deriving (Show) + +instance Pretty Action where + pretty (Action cmd target) = Node ("action " ++ target) [pretty cmd] + +instance Pretty RewCmd where + pretty (CRewrite name) = Leaf ("rew " ++ name) + pretty CBeta = Leaf "beta" + pretty CEta = Leaf "eta" + pretty CCase = Leaf "case" + pretty CCaseForce = Leaf "case!" + pretty CEtaCase = Leaf "etacase" + pretty CCaseCase = Leaf "casecase" + pretty (CRepeat cmd) = Node "repeat" [pretty cmd] + + +exprTransformer :: RewCmd -> Maybe (Expr -> Expr) +exprTransformer = fmap (normalise .) . exprTransformer' + +exprTransformer' :: RewCmd -> Maybe (Expr -> Expr) +exprTransformer' (CRewrite _) = Nothing +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' (CRepeat (CRepeat cmd)) = exprTransformer' (CRepeat cmd) +exprTransformer' (CRepeat cmd) = fixpoint <$> exprTransformer' cmd diff --git a/src/Haskell/Env/Context.hs b/src/Haskell/Env/Context.hs new file mode 100644 index 0000000..2e6b6cc --- /dev/null +++ b/src/Haskell/Env/Context.hs @@ -0,0 +1,15 @@ +module Haskell.Env.Context where + +import Haskell.Env +import Haskell.Env.Cmd + + +data Context = Context { cStack :: [(Action, Env)], cBaseEnv :: Env } + deriving (Show) + +topEnv :: Context -> Env +topEnv (Context [] env) = env +topEnv (Context ((_, env):_) _) = env + +pushCtx :: (Action, Env) -> Context -> Context +pushCtx pair ctx = ctx { cStack = pair : cStack ctx } diff --git a/src/Haskell/Rewrite.hs b/src/Haskell/Rewrite.hs index c33f62e..bcec6f7 100644 --- a/src/Haskell/Rewrite.hs +++ b/src/Haskell/Rewrite.hs @@ -3,14 +3,14 @@ module Haskell.Rewrite ,betared, etared, casered ,etacase, casecase ,autoSimp - ,normalise - ,fixpoint) where + ,normalise) where import Control.Monad import Data.List import Data.Maybe import qualified Data.Map.Strict as Map import Haskell.AST +import Util rewrite :: Name -> Expr -> Expr -> Expr @@ -105,9 +105,3 @@ 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 6dfbef5..a6d80b3 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -5,46 +5,15 @@ import Data.List import Data.Maybe import Haskell.AST import Haskell.Env +import Haskell.Env.Cmd +import Haskell.Env.Context import Haskell.Rewrite import Haskell.Parser import Pretty import System.Environment import System.Exit import System.IO - - -tryEither :: Either String a -> IO a -tryEither (Left err) = die err -tryEither (Right x) = return x - -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 (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 - Nothing -> return () - Just val' -> while val' f - -whenM :: Monad m => m Bool -> m a -> m () -whenM b a = b >>= \b' -> if b' then void a else return () - -ifM :: Monad m => m Bool -> m a -> m a -> m a -ifM b t e = b >>= \b' -> if b' then t else e - -splitOn :: Eq a => a -> [a] -> [[a]] -splitOn _ [] = [[]] -splitOn spl (x:xs) - | x == spl = [] : splitOn spl xs - | otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs +import Util usageString :: String @@ -79,23 +48,7 @@ usageString = data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name } deriving (Show) -data Context = Context { cStack :: [(Action, Env)], cBaseEnv :: Env } - deriving (Show) - -data Action = Action Cmd Name - deriving (Show) - -data Cmd = CRewrite Name - | CBeta - | CEta - | CCase - | CCaseForce - | CEtaCase - | CCaseCase - | CRepeat Cmd - deriving (Show) - -data UserCmd = UCCmd Cmd +data UserCmd = UCCmd RewCmd | CAction Action | CAuto | CRewriteAll @@ -108,35 +61,6 @@ data UserCmd = UCCmd Cmd | CHelp deriving (Show) -instance Pretty Action where - pretty (Action cmd target) = Node ("action " ++ target) [pretty cmd] - -instance Pretty Cmd where - pretty (CRewrite name) = Leaf ("rew " ++ name) - pretty CBeta = Leaf "beta" - pretty CEta = Leaf "eta" - pretty CCase = Leaf "case" - pretty CCaseForce = Leaf "case!" - pretty CEtaCase = Leaf "etacase" - pretty CCaseCase = Leaf "casecase" - pretty (CRepeat cmd) = Node "repeat" [pretty cmd] - -topEnv :: Context -> Env -topEnv (Context [] env) = env -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 - ctxTransform :: Context -> Action -> (Expr -> Expr) -> Either String Context ctxTransform ctx act@(Action _ target) = generalCtxTransform ctx act (\env -> get env target) @@ -153,14 +77,10 @@ apply ctx act@(Action cmd target) = case cmd of 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)) + ctxTransform ctx act (fromJust (exprTransformer cmd)) -findChangingTransformer :: Expr -> Maybe Cmd +findChangingTransformer :: Expr -> Maybe RewCmd findChangingTransformer expr = let opts = [CBeta, CEta, CCase, CEtaCase, CCaseCase] results = [(cmd, normalise $ fromJust (exprTransformer cmd) expr) | cmd <- opts] @@ -302,8 +222,8 @@ main = do source <- readFile fname ast <- tryEither' (parseAST fname source) - print ast + -- print ast env0 <- tryEither (envFromAST ast) - print env0 + -- print env0 while (AppState (Context [] env0) Nothing) interface diff --git a/src/Util.hs b/src/Util.hs new file mode 100644 index 0000000..98943f0 --- /dev/null +++ b/src/Util.hs @@ -0,0 +1,44 @@ +module Util where + +import Control.Monad +import System.Exit + + +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 + +tryEither :: Either String a -> IO a +tryEither (Left err) = die err +tryEither (Right x) = return x + +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 (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 + Nothing -> return () + Just val' -> while val' f + +whenM :: Monad m => m Bool -> m a -> m () +whenM b a = b >>= \b' -> if b' then void a else return () + +ifM :: Monad m => m Bool -> m a -> m a -> m a +ifM b t e = b >>= \b' -> if b' then t else e + +splitOn :: Eq a => a -> [a] -> [[a]] +splitOn _ [] = [[]] +splitOn spl (x:xs) + | x == spl = [] : splitOn spl xs + | otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs diff --git a/verify-hs.cabal b/verify-hs.cabal index 87e36dc..68dec3d 100644 --- a/verify-hs.cabal +++ b/verify-hs.cabal @@ -14,9 +14,12 @@ executable verify-hs other-modules: Haskell.AST Haskell.Env + Haskell.Env.Cmd + Haskell.Env.Context Haskell.Parser Haskell.Rewrite Pretty + Util build-depends: base >=4.12 && <4.13, containers >=0.6.0.1 && <0.7, -- cgit v1.2.3