Skip to content
Snippets Groups Projects
Commit b7094923 authored by chrg's avatar chrg
Browse files

Clean-up code slightly

parent e0cc21e2
No related branches found
No related tags found
No related merge requests found
.ghci 0 → 100644
:set -fwarn-unused-binds -fwarn-unused-imports
:set -isrc -ibin/rtree-c
:load Main
......@@ -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)
......
cradle:
cabal:
- path: "./src"
component: "lib:rtree"
- path: "./bin"
component: "exe:rtree-c"
......@@ -10,6 +10,7 @@ build-type: Simple
library
exposed-modules:
Control.Monad.Reduce
Control.RTree
other-modules:
Paths_rtree
......
{-# 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)
......@@ -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 #-}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment