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

Done refactor, next rebuilding rtree-c

parent 17fc3d3c
No related branches found
No related tags found
No related merge requests found
Showing
with 330 additions and 250 deletions
...@@ -10,9 +10,11 @@ build-type: Simple ...@@ -10,9 +10,11 @@ build-type: Simple
library library
exposed-modules: exposed-modules:
Control.Monad.IRTree
Control.Monad.Reduce Control.Monad.Reduce
Control.Monad.RTree Control.Monad.RTree
Control.RTree Control.RTree
Data.RPath
Data.Valuation Data.Valuation
other-modules: other-modules:
Paths_rtree Paths_rtree
...@@ -33,7 +35,9 @@ test-suite rtree-test ...@@ -33,7 +35,9 @@ test-suite rtree-test
type: exitcode-stdio-1.0 type: exitcode-stdio-1.0
main-is: Main.hs main-is: Main.hs
other-modules: other-modules:
Control.Monad.IRTreeSpec
Control.Monad.RTreeSpec Control.Monad.RTreeSpec
Data.Expr
Spec Spec
Test.Hspec.GitGolden Test.Hspec.GitGolden
Paths_rtree Paths_rtree
......
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
module Control.Monad.IRTree (
-- * IRTree
IRTree,
extract,
reduce,
reduceExp,
-- * IRTreeT
IRTreeT,
extractT,
reduceT,
reduceExpT,
-- * Re-exports
module Control.Monad.Reader,
module Data.RPath,
) where
import Control.Monad.Reader
import Control.Monad.Reduce
import Control.Monad.State
import Data.Bits
import Data.Foldable
import Data.Functor.Identity
import Data.RPath
import qualified Data.Sequence as Seq
type IRTree = IRTreeT Identity
newtype IRTreeT m i = IRTreeT (RPath -> Int -> m (i, Int))
deriving
(Functor, Applicative, Monad)
via (ReaderT RPath (StateT Int m))
instance (Monad m) => MonadReduce (IRTreeT m) where
check = IRTreeT \rp i -> do
pure (indexChoice rp i, i + 1)
extract :: IRTree i -> i
extract t = runIdentity $ extractT t
{-# INLINE extract #-}
extractT :: (Functor m) => IRTreeT m i -> m i
extractT (IRTreeT m) = fmap fst (m "" 0)
{-# INLINE extractT #-}
reduce
:: (Monad m)
=> (i -> m Bool)
-> IRTree i
-> m (Maybe i)
reduce = reduceT (pure . runIdentity)
{-# INLINE reduce #-}
-- | Interpreted reduction with an m base monad
reduceT
:: (Monad m)
=> (forall a. t a -> m a)
-> (i -> m Bool)
-> IRTreeT t i
-> m (Maybe i)
reduceT lift_ p (IRTreeT m) = do
(i, _) <- lift_ (m "" 0)
t <- p i
if t
then Just <$> go Seq.empty
else pure Nothing
where
go pth = do
-- Try to run the true branch.
let pth' = fromChoiceList (toList (pth Seq.|> True))
(i, x) <- lift_ (m pth' 0)
t <- p i
if x >= numberOfChoices pth'
then go (pth Seq.|> t)
else pure i
{-# INLINE reduceT #-}
reduceExp
:: (Monad m)
=> (i -> m Bool)
-> IRTree i
-> m (Maybe i)
reduceExp = reduceExpT (pure . runIdentity)
{-# INLINE reduceExp #-}
-- | Interpreted reduction with an m base monad, and running in expoential mode.
reduceExpT
:: (Monad m)
=> (forall a. t a -> m a)
-- ^ a lift of monad m into t (normally @id@ or @lift@)
-> (i -> m Bool)
-> IRTreeT t i
-> m (Maybe i)
reduceExpT lift_ p (IRTreeT m) = do
(i, _) <- lift_ (m "" 0)
t <- p i
if t
then Just <$> go 0 Seq.empty
else pure Nothing
where
go n sq = do
let depth = shiftL 1 n
let sq' = sq <> Seq.replicate depth True
let pth' = fromChoiceList (toList sq')
(i, x) <- lift_ (m pth' 0)
t <- p i
if x >= numberOfChoices pth' - depth + 1
then
if t
then go (n + 1) sq'
else case n of
0 -> go 0 (sq Seq.|> False)
n' -> go (n' - 1) sq
else pure i
{-# INLINE reduceExpT #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{- |
Module: Control.RTree
-}
module Control.RTree (
-- -- # RTree
-- RTree (..),
-- extract,
-- reduce,
-- reduceMaybe,
-- -- # IRTree
-- IRTree,
-- iextract,
-- ireduce,
-- ireduceExp,
-- IRTreeT (..),
-- iextractT,
-- ireduceT,
-- ireduceExpT,
-- ReState (..),
-- -- # Valuation
-- Valuation,
) where
-- import Control.Applicative
-- import Control.Monad.Reader
-- import Control.Monad.State.Strict
-- import Data.Functor.Identity
--
-- import qualified Data.Vector as V
--
-- import Control.Monad.Reduce
-- import Control.Monad.Trans.Maybe
-- import Data.Bits
-- import Data.Maybe
-- import qualified Data.Valuation as Val
--
-- type Valuation = Val.Valuation
-- type Truth = Val.Truth
--
-- data RTree l i
-- = Bottom
-- | Done i
-- | SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
-- deriving (Functor)
--
-- extract :: (Ord l) => Valuation l -> RTree l i -> Maybe i
-- extract v = \case
-- Bottom -> Nothing
-- SplitWith ml lhs rhs -> case ml >>= Val.condition v of
-- Just v' -> extract v' rhs
-- _ -> extract v lhs
-- Done i -> Just i
--
-- instance Applicative (RTree l) where
-- pure = Done
-- (<*>) = ap
--
-- instance Monad (RTree l) where
-- ma >>= f = case ma of
-- Bottom -> Bottom
-- Done i -> f i
-- SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
--
-- instance MonadReduce l (RTree l) where
-- splitWith = SplitWith
-- bottom = Bottom
--
-- reduce
-- :: forall m l i
-- . (Alternative m, Ord l)
-- => (Valuation l -> i -> m ())
-- -> Valuation l
-- -> RTree l i
-- -> m i
-- reduce p = checkgo
-- where
-- checkgo v r =
-- case extract v r of
-- Nothing -> empty
-- Just e -> p v e *> go v r
-- go v = \case
-- Bottom -> empty
-- Done i -> pure i
-- SplitWith (Just l) lhs rhs -> case Val.truthValue v (Val.label l) of
-- Just t
-- | t == Val.truth l -> checkgo v rhs
-- | otherwise -> checkgo v lhs
-- Nothing -> checkgo (Val.withTruth v $ Val.not l) lhs <|> go (Val.withTruth v l) rhs
-- SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
-- {-# INLINE reduce #-}
--
-- reduceMaybe
-- :: forall m l i
-- . (Monad m, Ord l)
-- => (Valuation l -> i -> m Bool)
-- -> Valuation l
-- -> RTree l i
-- -> m (Maybe i)
-- reduceMaybe p v rt =
-- runMaybeT
-- $ reduce
-- ( \v' i -> do
-- t <- lift (p v' i)
-- unless t empty
-- )
-- v
-- rt
--
-- data ReState l = ReState
-- { choices :: V.Vector Bool
-- , progress :: Int
-- , valuation :: !(Valuation l)
-- }
--
-- type IRTree l = IRTreeT l Identity
--
-- newtype IRTreeT l m i = IRTreeT {runIRTreeT :: MaybeT (StateT (ReState l) m) i}
-- deriving (Functor, Applicative, Alternative, Monad, MonadPlus) via (MaybeT (StateT (ReState l) m))
--
-- instance MonadTrans (IRTreeT l) where
-- lift m = IRTreeT (lift (lift m))
--
-- instance (MonadState s m) => MonadState s (IRTreeT l m) where
-- state s = lift (state s)
--
-- instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
-- bottom = mzero
-- checkWith =
-- IRTreeT . MaybeT . StateT . \case
-- Nothing -> \case
-- ReState ch i v ->
-- pure (Just (fromMaybe True (ch V.!? i)), ReState ch (i + 1) v)
-- Just l -> \case
-- ReState ch i v@((`Val.truthValue` Val.label l) -> Just t) ->
-- pure (Just (t == Val.truth l), ReState ch i v)
-- ReState ch i v ->
-- let a = fromMaybe True (ch V.!? i)
-- in pure (Just a, ReState ch (i + 1) (Val.withTruth v (if a then l else Val.not l)))
-- {-# INLINE checkWith #-}
--
-- iextract :: (Ord l) => Valuation l -> IRTree l a -> Maybe a
-- iextract v t = runIdentity $ iextractT v t
-- {-# INLINE iextract #-}
--
-- iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m (Maybe i)
-- iextractT v (IRTreeT m) = evalStateT (runMaybeT m) (ReState V.empty 0 v)
-- {-# INLINE iextractT #-}
--
-- ireduce
-- :: forall m l i
-- . (Monad m, Ord l)
-- => (ReState l -> Maybe i -> m Bool)
-- -> Valuation l
-- -> IRTree l i
-- -> m (Maybe i)
-- 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@)
-- -> (ReState l -> Maybe i -> t Bool)
-- -> Valuation l
-- -> IRTreeT l m i
-- -> t (Maybe i)
-- ireduceT lift_ p v (IRTreeT m) = go V.empty
-- where
-- go pth = do
-- -- Try to run the false branch.
-- let pth' = pth <> V.singleton False
-- result <- lift_ (runStateT (runMaybeT m) (ReState pth' 0 v))
-- case result of
-- (mi, ReState _ i v') | i >= V.length pth' -> do
-- t <- p (ReState pth' i v') mi
-- -- if the predicate is true, we can reduce to the false branch.
-- go (pth <> V.singleton (not t))
--
-- -- if we no more choices are needed, stop.
-- (mi, _) -> pure mi
-- {-# INLINE ireduceT #-}
--
-- ireduceExp
-- :: forall m l i
-- . (Monad m, Ord l)
-- => (ReState l -> Maybe i -> m Bool)
-- -> Valuation l
-- -> IRTree l i
-- -> m (Maybe i)
-- 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@)
-- -> (ReState l -> Maybe i -> t Bool)
-- -> Valuation l
-- -> IRTreeT l m i
-- -> t (Maybe i)
-- ireduceExpT lift_ p v (IRTreeT m) = go 0 V.empty
-- where
-- -- here n is the number of explorative elements
-- go n pth = do
-- let depth = shiftL 1 n
-- let pth' = pth <> V.replicate depth False
-- result <- lift_ (runStateT (runMaybeT m) $ ReState pth' 0 v)
-- case result of
-- (mi, ReState _ i v') | i >= length pth' - depth + 1 -> do
-- t <- p (ReState pth' i v') mi
-- if t
-- then go (n + 1) pth'
-- else case n of
-- 0 -> go 0 (pth <> V.singleton True)
-- n' -> go (n' - 1) pth
-- (mi, _) -> pure mi
...@@ -3,10 +3,15 @@ module Data.RPath ( ...@@ -3,10 +3,15 @@ module Data.RPath (
RPath, RPath,
fromChoiceList, fromChoiceList,
toChoiceList, toChoiceList,
numberOfChoices,
indexChoice,
-- * As a predicate -- * As a predicate
toPredicate, toPredicate,
toPredicateDebug, toPredicateDebug,
-- * Helpers
debugShowWithDepth,
) where ) where
import Data.Bool import Data.Bool
...@@ -22,19 +27,32 @@ newtype RPath = RPath {rPathAsVector :: VU.Vector Bool} ...@@ -22,19 +27,32 @@ newtype RPath = RPath {rPathAsVector :: VU.Vector Bool}
deriving (Eq, Ord) deriving (Eq, Ord)
toPredicate :: RPath -> IO (i -> IO Bool) toPredicate :: RPath -> IO (i -> IO Bool)
toPredicate (RPath v) = do toPredicate rp = do
idx <- newIORef (-1) idx <- newIORef (-1)
pure . const $ do pure . const $ do
idx' <- atomicModifyIORef idx (\n -> (n + 1, n)) idx' <- atomicModifyIORef idx (\n -> (n + 1, n))
pure (fromMaybe True (v VU.!? idx')) pure $ indexChoice rp idx'
toPredicateDebug :: (Show i) => RPath -> IO (i -> IO Bool) toPredicateDebug :: (Show i) => RPath -> IO (i -> IO Bool)
toPredicateDebug rp@(RPath v) = do toPredicateDebug rp = do
idx <- newIORef (-1) idx <- newIORef (-1)
pure $ \i -> do pure $ \i -> do
idx' <- atomicModifyIORef idx (\n -> (n + 1, n)) idx' <- atomicModifyIORef idx (\n -> (n + 1, n))
print (rp, idx', i) putStr (debugShowWithDepth rp idx')
pure (fromMaybe True (v VU.!? idx')) putStr ": "
print i
pure $ indexChoice rp idx'
{- | Index the list of choices, if there are no choices left
default to false. Indexing with a negative number gives True.
-}
indexChoice :: RPath -> Int -> Bool
indexChoice (RPath v) idx
| idx < 0 = True
| otherwise = fromMaybe False (v VU.!? idx)
numberOfChoices :: RPath -> Int
numberOfChoices (RPath v) = VU.length v
-- | Create a reduction path from a list of choices -- | Create a reduction path from a list of choices
fromChoiceList :: [Bool] -> RPath fromChoiceList :: [Bool] -> RPath
...@@ -44,6 +62,11 @@ fromChoiceList = RPath . VU.fromList ...@@ -44,6 +62,11 @@ fromChoiceList = RPath . VU.fromList
toChoiceList :: RPath -> [Bool] toChoiceList :: RPath -> [Bool]
toChoiceList = VU.toList . rPathAsVector toChoiceList = VU.toList . rPathAsVector
debugShowWithDepth :: RPath -> Int -> String
debugShowWithDepth rp i =
(map (bool '0' '1') . take (i + 1) . toChoiceList $ rp)
<> replicate (numberOfChoices rp - i - 1) '*'
instance Show RPath where instance Show RPath where
show = show . map (bool '0' '1') . toChoiceList show = show . map (bool '0' '1') . toChoiceList
......
1: x := 1; y := 2; x + y
0: -
1: y := 2; 1 + y
0: -
1: 1 + 2
0: 2
0: 1
0: 3
1: 1 + 2
1: x := 1; y := 2; x + y
0: -
1: y := 2; 1 + y
0: -
0: -
1: 1 + 2
0: -
0: 2
0: 1
0: 3
1: 1 + 2
1: x := 1; x := 2; x + x
0: -
1: x := 2; x + x
0: -
1: 2 + 2
0: 2
0: 2
0: 4
1: 2 + 2
1: x := 1; x := 2; x + x
0: -
1: x := 2; x + x
0: -
0: -
1: 2 + 2
0: -
0: 2
0: 2
0: 4
1: 2 + 2
1: x := 1; 2 + x
0: -
1: 2 + 1
0: 1
0: 2
0: 3
1: 2 + 1
1: x := 1; 2 + x
0: -
1: 2 + 1
0: -
0: 1
0: 2
0: 3
1: 2 + 1
1: 1 + 2
0: 2
0: 1
0: 3
1: 1 + 2
1: 1 + 2
0: 2
0: 1
0: 3
1: 1 + 2
{-# LANGUAGE BlockArguments #-}
module Control.Monad.IRTreeSpec where
import Control.Monad.IRTree
import qualified Control.Monad.IRTree as IRTree
import qualified Control.Monad.RTree as RTree
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Data.Bool
import Data.Expr as Expr
import Data.IORef (modifyIORef', newIORef, readIORef)
import qualified Data.Map.Strict as Map
import Test.Hspec
import Test.Hspec.GitGolden
spec :: Spec
spec = describe "examples" do
handle "small-opr-expr" $
Opr (Cnt 1) (Cnt 2)
handle "small-let-expr" $
Let "x" (Cnt 1) (Opr (Cnt 2) (Var "x"))
handle "double-let-expr" $
Let "x" (Cnt 1) (Let "y" (Cnt 2) (Opr (Var "x") (Var "y")))
handle "double-overloading-let-expr" $
Let "x" (Cnt 1) (Let "x" (Cnt 2) (Opr (Var "x") (Var "x")))
where
handle str e = describe (str <> " (" <> prettyExprS 0 e ")") do
let me = evalStateT (runMaybeT $ Expr.rExpr e) Map.empty
it "should extract" do
IRTree.extract me `shouldBe` Just e
let re = evalStateT (runMaybeT $ Expr.rExpr e) Map.empty
let predicate = maybe False (contains isOpr)
rex <- RTree.reduce (pure . predicate) re
it "should find an opr" do
ref <- newIORef ""
let test i = do
let x = predicate i
modifyIORef' ref (\t -> t <> bool "0" "1" x <> ": " <> maybe "-" (flip (prettyExprS 0) "") i <> "\n")
pure x
mex <- IRTree.reduce test me
rex `shouldBe` mex
result <- readIORef ref
pure $ golden ("test/expected/" <> str <> "-red") result
it "should find an opr exponentially" do
ref <- newIORef ""
let test i = do
let x = predicate i
modifyIORef' ref (\t -> t <> bool "0" "1" x <> ": " <> maybe "-" (flip (prettyExprS 0) "") i <> "\n")
pure x
mex <- IRTree.reduceExp test me
rex `shouldBe` mex
result <- readIORef ref
pure $ golden ("test/expected/" <> str <> "-red-exp") result
it "should reduce like iinputs" do
forM_ (RTree.iinputs re) \(ii, e') -> do
p <- toPredicate ii
IRTree.reduce p me `shouldReturn` Just e'
...@@ -88,19 +88,18 @@ rtreeSpec = describe "RTree" do ...@@ -88,19 +88,18 @@ rtreeSpec = describe "RTree" do
(drawRTree show (rList [1, 2, 3 :: Int])) (drawRTree show (rList [1, 2, 3 :: Int]))
examplesSpec :: Spec examplesSpec :: Spec
examplesSpec = do examplesSpec = describe "example" do
describe "rExpr" do handle "small-opr-expr" $
handle "small-opr-expr" $ Opr (Cnt 1) (Cnt 2)
Opr (Cnt 1) (Cnt 2)
handle "small-let-expr" $ handle "small-let-expr" $
Let "x" (Cnt 1) (Opr (Cnt 2) (Var "x")) Let "x" (Cnt 1) (Opr (Cnt 2) (Var "x"))
handle "double-let-expr" $ handle "double-let-expr" $
Let "x" (Cnt 1) (Let "y" (Cnt 2) (Opr (Var "x") (Var "y"))) Let "x" (Cnt 1) (Let "y" (Cnt 2) (Opr (Var "x") (Var "y")))
handle "double-overloading-let-expr" $ handle "double-overloading-let-expr" $
Let "x" (Cnt 1) (Let "x" (Cnt 2) (Opr (Var "x") (Var "x"))) Let "x" (Cnt 1) (Let "x" (Cnt 2) (Opr (Var "x") (Var "x")))
where where
handle str e = describe (str <> " (" <> prettyExprS 0 e ")") do handle str e = describe (str <> " (" <> prettyExprS 0 e ")") do
let me = runMaybeT $ Expr.rExpr e let me = runMaybeT $ Expr.rExpr e
......
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-} {-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Expr where module Data.Expr where
import Control.Applicative import Control.Applicative
import Control.Monad.Reduce import Control.Monad.Reduce
import Control.Monad.State import Control.Monad.State
import Data.Data
import Data.Functor import Data.Functor
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import Test.Hspec
data Expr data Expr
= Var !String = Var !String
| Cnt !Int | Cnt !Int
| Opr !Expr !Expr | Opr !Expr !Expr
| Let !String !Expr !Expr | Let !String !Expr !Expr
deriving (Show, Eq) deriving (Show, Eq, Data)
isOpr :: Expr -> Bool
isOpr = \case
Opr _ _ -> True
_a -> False
spec :: Spec
spec = do
describe "contains" do
it "handles a small case" do
contains isOpr (Opr (Var "x") (Var "y")) `shouldBe` True
contains :: (Data a) => (Expr -> Bool) -> a -> Bool
contains fn e =
gmapQl (||) False (contains fn) e || case cast e of
Just (e' :: Expr) -> fn e'
Nothing -> False
rExpr rExpr
:: (MonadReducePlus m, MonadState (Map.Map String (Either String Expr)) m) :: (MonadReducePlus m, MonadState (Map.Map String (Either String Expr)) m)
......
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedRecordDot #-}
module Test.Hspec.GitGolden where module Test.Hspec.GitGolden where
...@@ -16,6 +17,11 @@ data GitGolden = GitGolden ...@@ -16,6 +17,11 @@ data GitGolden = GitGolden
, content :: !String , content :: !String
} }
instance Example (IO GitGolden) where
evaluateExample e p a c = do
e' <- e
evaluateExample e' p a c
instance Example GitGolden where instance Example GitGolden where
evaluateExample e _p _a _c = do evaluateExample e _p _a _c = do
createDirectoryIfMissing True (takeDirectory e.filename) createDirectoryIfMissing True (takeDirectory e.filename)
......
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