From b70949232fa8049edb017e09e25e1ff6ed4a69c5 Mon Sep 17 00:00:00 2001 From: Christian Gram Kalhauge <chrg@dtu.dk> Date: Wed, 10 Jan 2024 16:17:42 +0100 Subject: [PATCH] Clean-up code slightly --- .ghci | 4 + bin/rtree-c/Main.hs | 84 +++++++------- hie.yaml | 6 + rtree.cabal | 1 + src/Control/Monad/Reduce.hs | 201 +++++++++++++++++++++++++++++++++ src/Control/RTree.hs | 215 ++++++------------------------------ 6 files changed, 281 insertions(+), 230 deletions(-) create mode 100644 .ghci create mode 100644 hie.yaml create mode 100644 src/Control/Monad/Reduce.hs diff --git a/.ghci b/.ghci new file mode 100644 index 0000000..bb358d0 --- /dev/null +++ b/.ghci @@ -0,0 +1,4 @@ +:set -fwarn-unused-binds -fwarn-unused-imports +:set -isrc -ibin/rtree-c +:load Main + diff --git a/bin/rtree-c/Main.hs b/bin/rtree-c/Main.hs index e6f95de..19314eb 100644 --- a/bin/rtree-c/Main.hs +++ b/bin/rtree-c/Main.hs @@ -6,6 +6,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +import Control.Monad.Reduce import Control.RTree import Colog @@ -24,8 +25,6 @@ import System.FilePath import Data.Text qualified as Text --- import System.Process.Typed - import Data.Map.Strict qualified as Map import GHC.Stack import Language.C (CInitializer (CInitExpr)) @@ -39,7 +38,7 @@ main :: IO () main = join . execParser - $ info run + $ info (run <**> helper) . fold $ [] @@ -57,14 +56,19 @@ run :: (HasCallStack) => Parser (IO ()) run = do file <- strArgument $ fold [metavar "FILE"] - validity <- flag False True $ fold [long "validity"] + validity <- + flag False True + $ fold + [ long "validity" + , help "check for validity, throw error if command fails" + ] pure $ usingLoggerT (cmap fmtMessage logTextStdout) $ do let test f = process D ("test " <> Text.pack f) do - err <- liftIO $ runProcess (proc "clang" ["-O0", "test.c"]) + err <- liftIO $ runProcess (proc "clang" ["-O0", file]) log D (Text.pack $ show err) pure (err == ExitSuccess) @@ -72,19 +76,19 @@ run = do let x = P.render (C.pretty (c $> C.undefNode)) liftIO $ writeFile f x - check f _ c = MaybeT do + check' f _ c = do when validity do liftIO $ copyFile file (file <.> "last") output f c t <- test f if t - then pure (Just ()) + then pure True else do liftIO $ when validity do copyFile file (file <.> "fail") copyFile (file <.> "last") file exitFailure - pure Nothing + pure False let bak = file <.> "bak" @@ -114,15 +118,13 @@ run = do unless t do liftIO exitFailure - l <- runMaybeT (reduceIO (check file) (Map.singleton (C.internalIdent "main") True) (reduceC c)) + l <- + reduceI + (check' file) + (Map.singleton (C.internalIdent "main") True) + (reduceC c) - case l of - Just l' -> do - output file l' - logInfo "Success" - Nothing -> do - logError "Unable to produce results" - liftIO exitFailure + output file l where parseCFile file = do res <- liftIO $ C.parseCFilePre file @@ -141,11 +143,9 @@ reduceC (C.CTranslUnit es ni) = do mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo) mrCExternalDeclaration = \case - C.CFDefExt fun -> - split - (funName fun) - empty - (C.CFDefExt <$> rCFunctionDef fun) + C.CFDefExt fun -> do + givenWith (funName fun) + C.CFDefExt <$> rCFunctionDef fun C.CDeclExt decl -> C.CDeclExt <$> mrCDeclaration decl a -> error (show a) @@ -155,11 +155,11 @@ mrCExternalDeclaration = \case mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo) mrCDeclarationItem = \case - C.CDeclarationItem d@(C.CDeclr x _ _ _ _) i e -> - split x empty do - i' <- mtry $ munder i mrCInitializer - e' <- mtry $ munder e mrCExpression - pure (C.CDeclarationItem d i' e') + C.CDeclarationItem d@(C.CDeclr x _ _ _ _) i e -> do + givenWith x + i' <- mtry $ munder i mrCInitializer + e' <- mtry $ munder e mrCExpression + pure (C.CDeclarationItem d i' e') a -> error (show a) mrCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m (C.CInitializer C.NodeInfo) @@ -198,7 +198,7 @@ rCStatement = \case cbi' <- collect mrCCompoundBlockItem cbi pure $ C.CCompound is cbi' ni C.CExpr e ni -> do - e' <- runMaybeT $ mlift e >>= mrCExpression + e' <- runMaybeT $ munder e mrCExpression pure $ C.CExpr e' ni C.CIf e s els ni -> do e' <- runMaybeT $ mrCExpression e @@ -257,8 +257,9 @@ zrCExpression e = orZero <$> runMaybeT (mrCExpression e) mrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m (C.CExpression C.NodeInfo) mrCExpression = \case - C.CVar i ni -> - splitOn i empty (pure $ C.CVar i ni) + C.CVar i ni -> do + givenThat i + pure $ C.CVar i ni C.CCall e es ni -> do e' <- mrCExpression e es' <- lift $ traverse zrCExpression es @@ -268,7 +269,7 @@ mrCExpression = \case ef' <- mrCExpression ef et' <- mtry $ munder et mrCExpression pure $ C.CCond ec' et' ef' ni - C.CBinary o elhs erhs ni -> ejoin elhs erhs \lhs rhs -> + C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs -> pure $ C.CBinary o lhs rhs ni C.CUnary o elhs ni -> do lhs <- mrCExpression elhs @@ -281,30 +282,19 @@ mrCExpression = \case cd' <- mrCDeclaration cd e' <- mrCExpression e pure $ C.CCast cd' e' ni - C.CAssign op e1 e2 ni -> ejoin e1 e2 \e1' e2' -> + C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' -> pure $ C.CAssign op e1' e2' ni - C.CIndex e1 e2 ni -> ejoin e1 e2 \e1' e2' -> + C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' -> pure $ C.CIndex e1' e2' ni C.CMember e i b ni -> do - splitOn i empty do - e' <- mrCExpression e - pure $ C.CMember e' i b ni + givenThat i + e' <- mrCExpression e + pure $ C.CMember e' i b ni C.CComma items ni -> do C.CComma <$> collectNonEmpty' mrCExpression items <*> pure ni e -> error (show e) where - ejoin elhs erhs = mjoin (mrCExpression elhs) (mrCExpression erhs) - -mjoin :: (Monad m) => MaybeT m a -> MaybeT m a -> (a -> a -> MaybeT m a) -> MaybeT m a -mjoin mlhs mrhs fn = MaybeT do - lhs <- runMaybeT mlhs - case lhs of - Nothing -> runMaybeT mrhs - Just l -> do - rhs <- runMaybeT mrhs - case rhs of - Nothing -> pure (Just l) - Just r -> runMaybeT (fn l r) + onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs) mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a) mtry (MaybeT mt) = MaybeT (Just <$> mt) diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 0000000..78dbf93 --- /dev/null +++ b/hie.yaml @@ -0,0 +1,6 @@ +cradle: + cabal: + - path: "./src" + component: "lib:rtree" + - path: "./bin" + component: "exe:rtree-c" diff --git a/rtree.cabal b/rtree.cabal index 2a020e9..3e72b73 100644 --- a/rtree.cabal +++ b/rtree.cabal @@ -10,6 +10,7 @@ build-type: Simple library exposed-modules: + Control.Monad.Reduce Control.RTree other-modules: Paths_rtree diff --git a/src/Control/Monad/Reduce.hs b/src/Control/Monad/Reduce.hs new file mode 100644 index 0000000..de30966 --- /dev/null +++ b/src/Control/Monad/Reduce.hs @@ -0,0 +1,201 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +{- | +Module: Control.Monad.Reduce +-} +module Control.Monad.Reduce ( + MonadReduce (..), + -- # Constructors + (<|), + (|>), + splitOn, + given, + givenThat, + givenWith, + check, + checkThat, + -- # Combinators + collect, + collectNonEmpty, + collectNonEmpty', + -- # Algorithms + ddmin, + linearSearch, + linearSearch', + binarySearch, + exponentialSearch, + -- # Helpers + onBoth, +) where + +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import qualified Data.List.NonEmpty as NE +import Data.Maybe + +-- {- | A reducer should extract itself +-- @ +-- extract . red = id +-- @ +-- -} +-- lawReduceId :: (MonadReduce l m, Eq i) => (i -> m i) -> i -> Bool +-- lawReduceId red i = extract (red i) == i + +-- | The Monad Reduce class. +class (Monad m) => MonadReduce l m | m -> l where + -- | Split the world into the a reduced world (left) without an ellement and a world + -- with that element (right). Optionally, labeled with l. + splitWith :: Maybe l -> m i -> m i -> m i + splitWith l r1 r2 = + checkWith l >>= \case + True -> r1 + False -> r2 + {-# INLINE splitWith #-} + + checkWith :: Maybe l -> m Bool + checkWith l = splitWith l (pure False) (pure True) + {-# INLINE checkWith #-} + +split :: (MonadReduce l m) => m i -> m i -> m i +split = splitWith Nothing +{-# INLINE split #-} + +(<|) :: (MonadReduce l m) => m i -> m i -> m i +(<|) = split +{-# INLINE (<|) #-} +infixr 3 <| + +(|>) :: (MonadReduce l m) => m i -> m i -> m i +r1 |> r2 = r2 <| r1 +{-# INLINE (|>) #-} +infixl 3 |> + +splitOn :: (MonadReduce l m) => l -> m i -> m i -> m i +splitOn l = splitWith (Just l) +{-# INLINE splitOn #-} + +-- | Split the world on a fact. False it does not happen, and True it does happen. +check :: (MonadReduce l m) => m Bool +check = checkWith Nothing +{-# INLINE check #-} + +-- | Split the world on a labeled fact. False it does not happen, and True it does happen. +checkThat :: (MonadReduce l m) => l -> m Bool +checkThat l = checkWith (Just l) +{-# INLINE checkThat #-} + +instance (MonadReduce l m) => MonadReduce l (MaybeT m) where + splitWith m (MaybeT lhs) (MaybeT rhs) = MaybeT (splitWith m lhs rhs) + +-- | Continues if the fact is true. +given :: (MonadReduce l m) => MaybeT m () +given = givenWith Nothing +{-# INLINE given #-} + +-- | Continues if the labeled fact is true. +givenWith :: (MonadReduce l m) => Maybe l -> MaybeT m () +givenWith l = MaybeT $ splitWith l (pure Nothing) (pure (Just ())) +{-# INLINE givenWith #-} + +-- | Continues if the labeled fact is true. +givenThat :: (MonadReduce l m) => l -> MaybeT m () +givenThat l = givenWith (Just l) +{-# INLINE givenThat #-} + +-- | Given a list of item try to remove each of them from the list. +collect :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> m [b] +collect fn = fmap catMaybes . traverse (runMaybeT . fn) +{-# INLINE collect #-} + +-- | Given a list of item try to remove each of them, but keep atleast one. +collectNonEmpty' :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m [b] +collectNonEmpty' fn as = + NE.toList <$> collectNonEmpty fn as +{-# INLINE collectNonEmpty' #-} + +-- | Given a list of item try to remove each of them, but keep atleast one. +collectNonEmpty :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m (NE.NonEmpty b) +collectNonEmpty fn as = do + as' <- lift . fmap catMaybes . traverse (runMaybeT . fn) $ as + MaybeT . pure $ NE.nonEmpty as' +{-# INLINE collectNonEmpty #-} + +{- | Given a list of ordered options, choose the first that statisfy the constraints, +returning the last element if nothing else matches. +-} +linearSearch :: (MonadReduce l m) => NE.NonEmpty i -> m i +linearSearch = foldr1 (<|) . fmap pure + +{- | Given a list of ordered options, choose the first that statisfy the +constraints, potentially returning nothing. +-} +linearSearch' :: (MonadReduce l m) => [i] -> MaybeT m i +linearSearch' is = MaybeT $ linearSearch (NE.fromList (fmap Just is ++ [Nothing])) + +-- | Given +ddmin :: (MonadReduce l m) => [i] -> m [i] +ddmin = \case + [] -> pure [] + [a] -> pure [a] + as -> go 2 as + where + go n lst + | n' <= 0 = pure lst + | otherwise = do + r <- runMaybeT $ linearSearch' (partitions n' lst ++ composites n' lst) + case r of + Nothing -> go (n * 2) lst <| pure lst -- (for efficiency :D) + Just lst' -> ddmin lst' + where + n' = length lst `div` n + partitions n lst = + case lst of + [] -> [] + _ -> let (h, r) = splitAt n lst in h : partitions n r + composites n lst = + case lst of + [] -> [] + _ -> let (h, r) = splitAt n lst in r : fmap (h ++) (composites n r) + +{- | Given a progression of inputs that are progressively larger, pick the smallest using +binary search. +-} +binarySearch :: (MonadReduce l m) => NE.NonEmpty i -> m i +binarySearch = \case + a NE.:| [] -> pure a + d -> binarySearch l <| binarySearch f + where + (NE.fromList -> f, NE.fromList -> l) = NE.splitAt (NE.length d `div` 2) d + +{- | Given a progression of inputs that are progressively larger, pick the smallest using +binary search. +-} +exponentialSearch :: (MonadReduce l m) => NE.NonEmpty i -> m i +exponentialSearch = go 1 + where + go n = \case + d + | n >= NE.length d -> binarySearch d + | otherwise -> go (n * 2) l <| binarySearch f + where + (NE.fromList -> f, NE.fromList -> l) = NE.splitAt n d + +-- | Returns either of the maybes or combines them if both have values. +onBoth :: (Monad m) => MaybeT m a -> MaybeT m a -> (a -> a -> MaybeT m a) -> MaybeT m a +onBoth mlhs mrhs fn = MaybeT do + runMaybeT mlhs >>= \case + Nothing -> runMaybeT mrhs + Just l -> + runMaybeT mrhs >>= \case + Nothing -> pure (Just l) + Just r -> runMaybeT (fn l r) diff --git a/src/Control/RTree.hs b/src/Control/RTree.hs index 4d3f76b..165b2fb 100644 --- a/src/Control/RTree.hs +++ b/src/Control/RTree.hs @@ -3,9 +3,9 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} @@ -19,29 +19,13 @@ module Control.RTree where import Control.Applicative import Control.Monad.Reader import Control.Monad.Trans.Maybe -import qualified Data.List.NonEmpty as NE +import Data.Functor.Identity import qualified Data.Map.Strict as Map import Data.Maybe -import Data.Void import GHC.IORef -class (Monad m) => MonadReduce l m | m -> l where - split :: Maybe l -> m i -> m i -> m i - -infixr 3 <| -infixl 3 |> - -{-# INLINE (<|) #-} -(<|) :: (MonadReduce l r) => r i -> r i -> r i -r1 <| r2 = split Nothing r1 r2 - -{-# INLINE splitOn #-} -splitOn :: (MonadReduce l r) => l -> r i -> r i -> r i -splitOn l = split (Just l) - -{-# INLINE (|>) #-} -(|>) :: (MonadReduce l r) => r i -> r i -> r i -r1 |> r2 = r2 <| r1 +import Control.Monad.Reduce +import Control.Monad.State.Strict data RTree l i = Split (RTree l i) !(RTree l i) @@ -68,7 +52,7 @@ instance Monad (RTree l) where SplitOn l (lhs >>= f) (rhs >>= f) instance MonadReduce l (RTree l) where - split = \case + splitWith = \case Just n -> SplitOn n Nothing -> Split @@ -118,168 +102,33 @@ reduceL p = checkgo data ReState l = ReState ![Bool] !(Valuation l) -{- | A faster version of the RTree which simply reruns the reducer program instead -of building a tree. --} -newtype IORTree l i = IORTree {runIORTree :: IORef (ReState l) -> IO i} - deriving (Functor, Applicative, Monad) via (ReaderT (IORef (ReState l)) IO) - -instance (Ord l) => MonadReduce l (IORTree l) where - split ml r1 r2 = IORTree \ref -> do - test <- case ml of - Nothing -> do - atomicModifyIORef' - ref - ( \case - ReState (a : as) v -> (ReState as v, a) - ReState [] v -> (ReState [] v, False) - ) - Just l -> do - atomicModifyIORef' - ref - ( \case - ReState as v@(Map.lookup l -> Just x) -> (ReState as v, not x) - ReState (a : as) v -> (ReState as (Map.insert l (not a) v), a) - ReState [] v -> (ReState [] (Map.insert l True v), False) - ) - if test - then runIORTree r1 ref - else runIORTree r2 ref - -reduceIO +newtype IRTree l i = IRTree {runIRTree :: ReState l -> (i, ReState l)} + deriving (Functor, Applicative, Monad) via (State (ReState l)) + +instance (Ord l) => MonadReduce l (IRTree l) where + checkWith = \case + Nothing -> + IRTree \case + ReState (a : as) v -> (a, ReState as v) + ReState [] v -> (False, ReState [] v) + Just l -> IRTree \case + ReState as v@(Map.lookup l -> Just x) -> (not x, ReState as v) + ReState (a : as) v -> (a, ReState as (Map.insert l (not a) v)) + ReState [] v -> (False, ReState [] (Map.insert l True v)) + +reduceI :: forall m l i - . (MonadIO m, Ord l) - => (Valuation l -> i -> MaybeT m ()) + . (Monad m, Ord l) + => (Valuation l -> i -> m Bool) -> Valuation l - -> IORTree l i - -> MaybeT m i -reduceIO p v (IORTree ext) = MaybeT $ go [] - where - go pth = do - ref <- liftIO $ newIORef (ReState pth v) - i <- liftIO $ ext ref - ReState r v' <- liftIO $ readIORef ref - case r of - [] -> do - t <- isJust <$> runMaybeT (p v' i) - if t - then go (pth <> [True]) - else go (pth <> [False]) - _ - | null pth -> - pure Nothing - | otherwise -> - pure (Just i) -{-# INLINE reduceIO #-} - --- Combinators - -type MRTree l = MaybeT (RTree l) - -instance (MonadReduce l m) => MonadReduce l (MaybeT m) where - split m (MaybeT lhs) (MaybeT rhs) = MaybeT (split m lhs rhs) - --- | Given a list of item try to remove each of them the list. -collect :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> m [b] -collect fn = fmap catMaybes . traverse (runMaybeT . fn) -{-# INLINE collect #-} - -collectNonEmpty' :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m [b] -collectNonEmpty' fn as = - NE.toList <$> collectNonEmpty fn as -{-# INLINE collectNonEmpty' #-} - -collectNonEmpty :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m (NE.NonEmpty b) -collectNonEmpty fn as = do - as' <- lift . fmap catMaybes . traverse (runMaybeT . fn) $ as - MaybeT . pure $ NE.nonEmpty as' -{-# INLINE collectNonEmpty #-} - --- | Split the world on a fact. False it does not happen, and True it does happen. -given :: RTree Void Bool -given = pure False <| pure True - -{- | A reducer should extract itself -@ - extract . red = id -@ --} -lawReduceId :: (Eq i) => (i -> RTree l i) -> i -> Bool -lawReduceId red i = extract (red i) == i - --- | Reducing a list one element at a time. -rList :: [a] -> RTree l [a] -rList = \case - [] -> pure [] - a : as -> rList as <| (a :) <$> rList as - -{- | Binary reduction on the list assumming suffixes all contain eachother: -@[] < [c] < [b, c] < [a,b,c]@ --} -rSuffixList :: [a] -> RTree l [a] -rSuffixList as = do - res <- exponentialSearch (NE.tails as) - case res of - [] -> pure [] - a : as' -> (a :) <$> rSuffixList as' - -{- | Given a progression of inputs that are progressively larger, pick the smallest using -binary search. --} -binarySearch :: NE.NonEmpty i -> RTree l i -binarySearch = \case - a NE.:| [] -> pure a - d -> binarySearch l <| binarySearch f - where - (NE.fromList -> f, NE.fromList -> l) = NE.splitAt (NE.length d `div` 2) d - -{- | Given a progression of inputs that are progressively larger, pick the smallest using -binary search. --} -exponentialSearch :: NE.NonEmpty i -> RTree l i -exponentialSearch = go 1 - where - go n = \case - d - | n >= NE.length d -> binarySearch d - | otherwise -> go (n * 2) l <| binarySearch f - where - (NE.fromList -> f, NE.fromList -> l) = NE.splitAt n d - -nonEmptyOr :: String -> [a] -> NE.NonEmpty a -nonEmptyOr msg ls = case NE.nonEmpty ls of - Just a -> a - Nothing -> error msg - --- | Given a list of orderd options, the -linearSearch :: NE.NonEmpty i -> RTree l i -linearSearch = foldr1 (<|) . fmap pure - --- | Given a list of orderd options, the -linearSearch' :: [i] -> RTree l (Maybe i) -linearSearch' is = linearSearch (NE.fromList $ fmap Just is ++ [Nothing]) - --- | Given -ddmin :: [i] -> RTree l [i] -ddmin = \case - [] -> pure [] - [a] -> pure [a] - as -> go 2 as + -> IRTree l i + -> m i +reduceI p v (IRTree m) = go [] where - go n lst - | n' <= 0 = pure lst - | otherwise = do - r <- linearSearch' (partitions n' lst ++ composites n' lst) - case r of - Nothing -> go (n * 2) lst <| pure lst -- (for efficiency :D) - Just lst' -> ddmin lst' - where - n' = length lst `div` n - partitions n lst = - case lst of - [] -> [] - _ -> let (h, r) = splitAt n lst in h : partitions n r - composites n lst = - case lst of - [] -> [] - _ -> let (h, r) = splitAt n lst in r : fmap (h ++) (composites n r) + go pth = + case m (ReState pth v) of + (i, ReState [] v') -> do + t <- p v' i + go (pth <> [t]) + (i, _) -> pure i +{-# INLINE reduceI #-} -- GitLab