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

More refactor

parent b7094923
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
.gitignore
+ 1
− 1
View file @ b2c30d92
......@@ -27,5 +27,5 @@ cabal.project.local~
result
a.out
rtree-c
/rtree-c
test.c
bin/rtree-c/Main.hs
+ 15
− 189
View file @ b2c30d92
......@@ -6,28 +6,24 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
import Control.Monad.Reduce
import Control.RTree
import ReduceC
import Colog
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Data.Foldable
import Data.Functor
import Data.Maybe
import Data.Map.Strict qualified as Map
import Data.Text qualified as Text
import GHC.Stack
import Language.C qualified as C
import Options.Applicative
import System.Directory
import System.Exit
import System.FilePath
import Data.Text qualified as Text
import Data.Map.Strict qualified as Map
import GHC.Stack
import Language.C (CInitializer (CInitExpr))
import System.IO
import System.Process.Typed
import Text.Pretty.Simple
......@@ -63,6 +59,13 @@ run = do
, help "check for validity, throw error if command fails"
]
expmode <-
flag False True
$ fold
[ long "exp"
, help "run in exponential mode"
]
pure
$ usingLoggerT (cmap fmtMessage logTextStdout)
$ do
......@@ -76,7 +79,7 @@ run = do
let x = P.render (C.pretty (c $> C.undefNode))
liftIO $ writeFile f x
check' f _ c = do
check' f c = do
when validity do
liftIO $ copyFile file (file <.> "last")
output f c
......@@ -119,10 +122,10 @@ run = do
liftIO exitFailure
l <-
reduceI
(if expmode then ireduceExp else ireduce)
(check' file)
(Map.singleton (C.internalIdent "main") True)
(reduceC c)
(ReduceC.reduceC c)
output file l
where
......@@ -133,180 +136,3 @@ run = do
Left err -> do
logError (Text.pack (show err))
liftIO exitFailure
type Lab = C.Ident
reduceC :: (MonadReduce Lab m) => C.CTranslUnit -> m C.CTranslUnit
reduceC (C.CTranslUnit es ni) = do
es' <- collect mrCExternalDeclaration es
pure $ C.CTranslUnit es' ni
mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo)
mrCExternalDeclaration = \case
C.CFDefExt fun -> do
givenWith (funName fun)
C.CFDefExt <$> rCFunctionDef fun
C.CDeclExt decl ->
C.CDeclExt <$> mrCDeclaration decl
a -> error (show a)
where
funName (C.CFunDef _ (C.CDeclr x _ _ _ _) _ _ _) =
x
mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo)
mrCDeclarationItem = \case
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)
mrCInitializer = \case
C.CInitExpr e ni -> mrCExpression e <&> \e' -> CInitExpr e' ni
C.CInitList (C.CInitializerList items) ni -> do
collectNonEmpty' rmCInitializerListItem items <&> \items' ->
C.CInitList (C.CInitializerList items') ni
where
rmCInitializerListItem (pds, is) = do
pds' <- lift $ collect rmCPartDesignator pds
is' <- mrCInitializer is
pure (pds', is')
rmCPartDesignator :: (MonadReduce Lab m) => C.CPartDesignator C.NodeInfo -> m (C.CPartDesignator C.NodeInfo)
rmCPartDesignator = \case
a -> error (show a)
mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo)
mrCDeclaration = \case
C.CDecl spc decl ni -> do
decl' <- lift $ collect mrCDeclarationItem decl
case decl' of
[] -> empty
decl'' -> pure $ C.CDecl spc decl'' ni
a -> error (show a)
rCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> m (C.CFunctionDef C.NodeInfo)
rCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
smt' <- rCStatement smt
pure $ C.CFunDef spc dec cdecls smt' ni
rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
rCStatement = \case
C.CCompound is cbi ni -> do
cbi' <- collect mrCCompoundBlockItem cbi
pure $ C.CCompound is cbi' ni
C.CExpr e ni -> do
e' <- runMaybeT $ munder e mrCExpression
pure $ C.CExpr e' ni
C.CIf e s els ni -> do
e' <- runMaybeT $ mrCExpression e
s' <- rCStatement s
els' <- case els of
Just els' -> do
pure Nothing <| Just <$> rCStatement els'
Nothing -> pure Nothing
case (e', els') of
(Nothing, Nothing) -> pure s'
(Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
(Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
(Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
C.CFor e1 e2 e3 s ni -> do
rCStatement s <| do
e1' <- rCForInit e1
e2' <- runMaybeT $ munder e2 mrCExpression
e3' <- runMaybeT $ munder e3 mrCExpression
s' <- rCStatement s
pure $ C.CFor e1' e2' e3' s' ni
C.CReturn e ni -> do
e' <- case e of
Nothing -> pure Nothing
Just e' -> Just <$> zrCExpression e'
pure $ C.CReturn e' ni
C.CBreak ni -> pure (C.CBreak ni)
C.CCont ni -> pure (C.CCont ni)
C.CLabel i s [] ni ->
-- todo fix attrs
splitOn i (rCStatement s) do
s' <- rCStatement s
pure $ C.CLabel i s' [] ni
C.CGoto i ni ->
-- todo fix attrs
splitOn i (pure $ C.CExpr Nothing ni) do
pure $ C.CGoto i ni
a -> error (show a)
where
rCForInit = \case
C.CForDecl decl -> do
m <- runMaybeT $ mrCDeclaration decl
pure $ case m of
Nothing -> C.CForInitializing Nothing
Just d' -> C.CForDecl d'
C.CForInitializing n -> do
C.CForInitializing <$> runMaybeT (munder n mrCExpression)
orZero :: Maybe (C.CExpression C.NodeInfo) -> C.CExpression C.NodeInfo
orZero = fromMaybe zeroExp
zeroExp :: C.CExpression C.NodeInfo
zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
zrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> m (C.CExpression C.NodeInfo)
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 -> do
givenThat i
pure $ C.CVar i ni
C.CCall e es ni -> do
e' <- mrCExpression e
es' <- lift $ traverse zrCExpression es
pure $ C.CCall e' es' ni
C.CCond ec et ef ni -> do
ec' <- mrCExpression ec
ef' <- mrCExpression ef
et' <- mtry $ munder et mrCExpression
pure $ C.CCond ec' et' ef' ni
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
pure $ C.CUnary o lhs ni
C.CConst c -> do
-- TODO fix
pure $ C.CConst c
C.CCast cd e ni -> do
-- TODO fix
cd' <- mrCDeclaration cd
e' <- mrCExpression e
pure $ C.CCast cd' e' ni
C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
pure $ C.CAssign op e1' e2' ni
C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
pure $ C.CIndex e1' e2' ni
C.CMember e i b ni -> do
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
onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs)
mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
mtry (MaybeT mt) = MaybeT (Just <$> mt)
mlift :: (Applicative m) => Maybe a -> MaybeT m a
mlift a = MaybeT (pure a)
munder :: (Monad m) => Maybe a -> (a -> MaybeT m b) -> MaybeT m b
munder a mf = mlift a >>= mf
mrCCompoundBlockItem :: (MonadReduce Lab m) => C.CCompoundBlockItem C.NodeInfo -> MaybeT m (C.CCompoundBlockItem C.NodeInfo)
mrCCompoundBlockItem = \case
C.CBlockStmt s -> empty <| lift (C.CBlockStmt <$> rCStatement s)
C.CBlockDecl d -> C.CBlockDecl <$> mrCDeclaration d
a -> error (show a)
bin/rtree-c/ReduceC.hs 0 → 100644
+ 197
− 0
View file @ b2c30d92
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module ReduceC where
import Control.Monad.Reduce
import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Data.Functor
import Data.Maybe
import qualified Language.C as C
type Lab = C.Ident
reduceC :: (MonadReduce Lab m) => C.CTranslUnit -> m C.CTranslUnit
reduceC (C.CTranslUnit es ni) = do
es' <- collect mrCExternalDeclaration es
pure $ C.CTranslUnit es' ni
mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo)
mrCExternalDeclaration = \case
C.CFDefExt fun -> do
givenWith (funName fun)
C.CFDefExt <$> rCFunctionDef fun
C.CDeclExt decl ->
C.CDeclExt <$> mrCDeclaration decl
a -> error (show a)
where
funName (C.CFunDef _ (C.CDeclr x _ _ _ _) _ _ _) =
x
mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo)
mrCDeclarationItem = \case
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)
mrCInitializer = \case
C.CInitExpr e ni -> mrCExpression e <&> \e' -> C.CInitExpr e' ni
C.CInitList (C.CInitializerList items) ni -> do
collectNonEmpty' rmCInitializerListItem items <&> \items' ->
C.CInitList (C.CInitializerList items') ni
where
rmCInitializerListItem (pds, is) = do
pds' <- lift $ collect rmCPartDesignator pds
is' <- mrCInitializer is
pure (pds', is')
rmCPartDesignator :: (MonadReduce Lab m) => C.CPartDesignator C.NodeInfo -> m (C.CPartDesignator C.NodeInfo)
rmCPartDesignator = \case
a -> error (show a)
mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo)
mrCDeclaration = \case
C.CDecl spc decl ni -> do
decl' <- lift $ collect mrCDeclarationItem decl
case decl' of
[] -> empty
decl'' -> pure $ C.CDecl spc decl'' ni
a -> error (show a)
rCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> m (C.CFunctionDef C.NodeInfo)
rCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
smt' <- rCStatement smt
pure $ C.CFunDef spc dec cdecls smt' ni
rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
rCStatement = \case
C.CCompound is cbi ni -> do
cbi' <- collect mrCCompoundBlockItem cbi
pure $ C.CCompound is cbi' ni
C.CExpr e ni -> do
e' <- runMaybeT $ munder e mrCExpression
pure $ C.CExpr e' ni
C.CIf e s els ni -> do
e' <- runMaybeT $ mrCExpression e
s' <- rCStatement s
els' <- case els of
Just els' -> do
pure Nothing <| Just <$> rCStatement els'
Nothing -> pure Nothing
case (e', els') of
(Nothing, Nothing) -> pure s'
(Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
(Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
(Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
C.CFor e1 e2 e3 s ni -> do
rCStatement s <| do
e1' <- rCForInit e1
e2' <- runMaybeT $ munder e2 mrCExpression
e3' <- runMaybeT $ munder e3 mrCExpression
s' <- rCStatement s
pure $ C.CFor e1' e2' e3' s' ni
C.CReturn e ni -> do
e' <- case e of
Nothing -> pure Nothing
Just e' -> Just <$> zrCExpression e'
pure $ C.CReturn e' ni
C.CBreak ni -> pure (C.CBreak ni)
C.CCont ni -> pure (C.CCont ni)
C.CLabel i s [] ni ->
-- todo fix attrs
splitOn i (rCStatement s) do
s' <- rCStatement s
pure $ C.CLabel i s' [] ni
C.CGoto i ni ->
-- todo fix attrs
splitOn i (pure $ C.CExpr Nothing ni) do
pure $ C.CGoto i ni
a -> error (show a)
where
rCForInit = \case
C.CForDecl decl -> do
m <- runMaybeT $ mrCDeclaration decl
pure $ case m of
Nothing -> C.CForInitializing Nothing
Just d' -> C.CForDecl d'
C.CForInitializing n -> do
C.CForInitializing <$> runMaybeT (munder n mrCExpression)
orZero :: Maybe (C.CExpression C.NodeInfo) -> C.CExpression C.NodeInfo
orZero = fromMaybe zeroExp
zeroExp :: C.CExpression C.NodeInfo
zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
zrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> m (C.CExpression C.NodeInfo)
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 -> do
givenThat i
pure $ C.CVar i ni
C.CCall e es ni -> do
e' <- mrCExpression e
es' <- lift $ traverse zrCExpression es
pure $ C.CCall e' es' ni
C.CCond ec et ef ni -> do
ec' <- mrCExpression ec
ef' <- mrCExpression ef
et' <- mtry $ munder et mrCExpression
pure $ C.CCond ec' et' ef' ni
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
pure $ C.CUnary o lhs ni
C.CConst c -> do
-- TODO fix
pure $ C.CConst c
C.CCast cd e ni -> do
-- TODO fix
cd' <- mrCDeclaration cd
e' <- mrCExpression e
pure $ C.CCast cd' e' ni
C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
pure $ C.CAssign op e1' e2' ni
C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
pure $ C.CIndex e1' e2' ni
C.CMember e i b ni -> do
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
onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs)
mrCCompoundBlockItem
:: (MonadReduce Lab m)
=> C.CCompoundBlockItem C.NodeInfo
-> MaybeT m (C.CCompoundBlockItem C.NodeInfo)
mrCCompoundBlockItem = \case
C.CBlockStmt s -> empty <| lift (C.CBlockStmt <$> rCStatement s)
C.CBlockDecl d -> C.CBlockDecl <$> mrCDeclaration d
a -> error (show a)
mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
mtry (MaybeT mt) = MaybeT (Just <$> mt)
mlift :: (Applicative m) => Maybe a -> MaybeT m a
mlift a = MaybeT (pure a)
munder :: (Monad m) => Maybe a -> (a -> MaybeT m b) -> MaybeT m b
munder a mf = mlift a >>= mf
rtree.cabal
+ 1
− 0
View file @ b2c30d92
......@@ -32,6 +32,7 @@ library
executable rtree-c
main-is: Main.hs
other-modules:
ReduceC
Paths_rtree
hs-source-dirs:
bin/rtree-c
......
src/Control/Monad/Reduce.hs
+ 34
− 20
View file @ b2c30d92
......@@ -15,7 +15,8 @@ Module: Control.Monad.Reduce
-}
module Control.Monad.Reduce (
MonadReduce (..),
-- # Constructors
-- * Constructors
(<|),
(|>),
splitOn,
......@@ -24,17 +25,20 @@ module Control.Monad.Reduce (
givenWith,
check,
checkThat,
-- # Combinators
-- * Combinators
collect,
collectNonEmpty,
collectNonEmpty',
-- # Algorithms
-- * Algorithms
ddmin,
linearSearch,
linearSearch',
binarySearch,
exponentialSearch,
-- # Helpers
-- * Helpers
onBoth,
) where
......@@ -53,33 +57,43 @@ import Data.Maybe
-- | 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
{-# MINIMAL splitWith | checkWith #-}
-- | Split the world into the a reduced world (left) without an element 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
False -> r1
True -> r2
{-# INLINE splitWith #-}
-- | Check with returns a boolean, that can be used to split the input into a world where
-- an optional label is true and where it is false.
checkWith :: Maybe l -> m Bool
checkWith l = splitWith l (pure False) (pure True)
{-# INLINE checkWith #-}
-- | Split with no label.
split :: (MonadReduce l m) => m i -> m i -> m i
split = splitWith Nothing
{-# INLINE split #-}
-- | Infix split.
(<|) :: (MonadReduce l m) => m i -> m i -> m i
(<|) = split
{-# INLINE (<|) #-}
infixr 3 <|
-- | Infix split, to the right.
(|>) :: (MonadReduce l m) => m i -> m i -> m i
r1 |> r2 = r2 <| r1
{-# INLINE (|>) #-}
infixl 3 |>
-- | Split on a label.
splitOn :: (MonadReduce l m) => l -> m i -> m i -> m i
splitOn l = splitWith (Just l)
{-# INLINE splitOn #-}
......@@ -94,9 +108,6 @@ 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
......@@ -130,6 +141,19 @@ collectNonEmpty fn as = do
MaybeT . pure $ NE.nonEmpty as'
{-# INLINE collectNonEmpty #-}
instance (MonadReduce l m) => MonadReduce l (MaybeT m) where
splitWith m (MaybeT lhs) (MaybeT rhs) = MaybeT (splitWith m lhs rhs)
-- | 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)
{- | Given a list of ordered options, choose the first that statisfy the constraints,
returning the last element if nothing else matches.
-}
......@@ -189,13 +213,3 @@ exponentialSearch = go 1
| 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)
src/Control/RTree.hs
+ 135
− 74
View file @ b2c30d92
......@@ -14,30 +14,46 @@
{- |
Module: Control.RTree
-}
module Control.RTree where
module Control.RTree (
-- # RTree
RTree (..),
extract,
reduce,
-- # IRTree
IRTree,
iextract,
ireduce,
ireduceExp,
IRTreeT (..),
iextractT,
ireduceT,
ireduceExpT,
ReState (..),
-- # Valuation
Valuation,
) where
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.Trans.Maybe
import Data.Functor.Identity
import qualified Data.Map.Strict as Map
import Data.Maybe
import GHC.IORef
import Control.Monad.Reduce
import Control.Monad.State.Strict
data RTree l i
= Split (RTree l i) !(RTree l i)
| SplitOn !l (RTree l i) !(RTree l i)
= SplitWith (Maybe l) (RTree l i) !(RTree l i)
| Done i
deriving (Functor)
extract :: RTree l i -> i
extract = \case
Split _ rhs -> extract rhs
SplitOn _ _ rhs -> extract rhs
Done v -> v
type Valuation l = Map.Map l Bool
extract :: (Ord l) => Valuation l -> RTree l i -> i
extract v = \case
SplitWith ml lhs rhs -> case ml >>= (`Map.lookup` v) of
Just False -> extract v lhs
_ -> extract v rhs
Done i -> i
instance Applicative (RTree l) where
pure = Done
......@@ -46,89 +62,134 @@ instance Applicative (RTree l) where
instance Monad (RTree l) where
ma >>= f = case ma of
Done i -> f i
Split lhs rhs ->
Split (lhs >>= f) (rhs >>= f)
SplitOn l lhs rhs ->
SplitOn l (lhs >>= f) (rhs >>= f)
SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
instance MonadReduce l (RTree l) where
splitWith = \case
Just n -> SplitOn n
Nothing -> Split
splitWith = SplitWith
reduce
:: forall m l i
. (Alternative m)
. (Alternative m, Ord l)
=> (i -> m ())
-> Valuation l
-> RTree l i
-> m i
reduce p = checkgo
where
go = \case
(Done i) -> pure i
(Split lhs rhs) -> (checkgo lhs <|> go rhs)
(SplitOn _ lhs rhs) -> (checkgo lhs <|> go rhs)
checkgo rt = p (extract rt) *> go rt
{-# SPECIALIZE reduce :: (i -> MaybeT IO ()) -> RTree l i -> MaybeT IO i #-}
checkgo v r = p (extract v r) *> go v r
go v = \case
Done i -> pure i
SplitWith (Just l) lhs rhs -> case Map.lookup l v of
Just True -> checkgo v rhs
Just False -> checkgo v lhs
Nothing -> checkgo (Map.insert l False v) lhs <|> go (Map.insert l True v) rhs
SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
{-# INLINE reduce #-}
data ReState l = ReState
{ choices :: [Bool]
, valuation :: !(Valuation l)
}
type IRTree l = IRTreeT l Identity
newtype IRTreeT l m i = IRTreeT {runIRTreeT :: StateT (ReState l) m i}
deriving (Functor, Applicative, Monad) via (StateT (ReState l) m)
deriving (MonadTrans) via (StateT (ReState l))
instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
checkWith =
IRTreeT . StateT . \case
Nothing -> \case
ReState (uncons -> (a, as)) v ->
pure (a, ReState as v)
Just l -> \case
ReState as v@(Map.lookup l -> Just x) ->
pure (x, ReState as v)
ReState (uncons -> (a, as)) v ->
pure (a, ReState as (Map.insert l a v))
where
uncons [] = (True, [])
uncons (a : as) = (a, as)
{-# INLINE checkWith #-}
type Valuation l = Map.Map l Bool
iextract :: (Ord l) => Valuation l -> IRTree l a -> a
iextract v t = runIdentity $ iextractT v t
{-# INLINE iextract #-}
extractL :: (Ord l) => Valuation l -> RTree l i -> i
extractL v = \case
Split _ rhs -> extractL v rhs
SplitOn l lhs rhs -> case Map.lookup l v of
Just False -> extractL v lhs
_ -> extractL v rhs
Done i -> i
iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m i
iextractT v (IRTreeT m) = evalStateT m (ReState [] v)
{-# INLINE iextractT #-}
reduceL
ireduce
:: forall m l i
. (Alternative m, Ord l)
=> (Valuation l -> i -> m ())
. (Monad m, Ord l)
=> (i -> m Bool)
-> Valuation l
-> RTree l i
-> IRTree l i
-> m i
reduceL p = checkgo
ireduce = ireduceT (pure . runIdentity)
{-# INLINE ireduce #-}
-- | Interpreted reduction with an m base monad
ireduceT
:: forall t m l i
. (Monad m, Monad t, Ord l)
=> (forall a. m a -> t a)
-- ^ a lift of monad m into t (normally @id@ or @lift@)
-> (i -> t Bool)
-> Valuation l
-> IRTreeT l m i
-> t i
ireduceT lift_ p v (IRTreeT m) = go []
where
checkgo v r = p v (extractL v r) *> go v r
go v = \case
Done i -> pure i
SplitOn l lhs rhs -> case Map.lookup l v of
Just True -> checkgo v rhs
Just False -> checkgo v lhs
Nothing -> checkgo (Map.insert l False v) lhs <|> go (Map.insert l True v) rhs
Split lhs rhs -> (checkgo v lhs <|> go v rhs)
{-# INLINE reduceL #-}
data ReState l = ReState ![Bool] !(Valuation l)
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
go pth =
lift_ (runStateT m (ReState pth v)) >>= \case
(i, ReState [] _) -> do
t <- p i
-- if the predicate is true, we can reduce to the false branch.
go (pth <> [not t])
(i, _) -> pure i
{-# INLINE ireduceT #-}
ireduceExp
:: forall m l i
. (Monad m, Ord l)
=> (Valuation l -> i -> m Bool)
=> (i -> m Bool)
-> Valuation l
-> IRTree l i
-> m i
reduceI p v (IRTree m) = go []
ireduceExp = ireduceExpT (pure . runIdentity)
{-# INLINE ireduceExp #-}
-- | Interpreted reduction with an m base monad, and running in expoential mode.
ireduceExpT
:: forall t m l i
. (Monad m, Monad t, Ord l)
=> (forall a. m a -> t a)
-- ^ a lift of monad m into t (normally @id@ or @lift@)
-> (i -> t Bool)
-> Valuation l
-> IRTreeT l m i
-> t i
ireduceExpT lift_ p v (IRTreeT (StateT m)) = go 0 []
where
go pth =
case m (ReState pth v) of
(i, ReState [] v') -> do
t <- p v' i
go (pth <> [t])
-- here n is the number of explorative elements
go n pth =
lift_ (m $ ReState pth v) >>= \case
(i, ReState [] _) -> do
p i >>= \case
True -> do
let n' = next n
go n' (pth <> replicate n' False)
False -> do
case n of
0 -> go 0 (pth <> [True])
n' -> go n' $ take (length pth - prev n') pth
(i, _) -> pure i
{-# INLINE reduceI #-}
next 0 = 1
next n = n * 2
prev 1 = 0
prev n = n `quot` 2
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment