creditmonad 1.0.0 → 1.1.0

raw patch · 25 files changed

+565/−574 lines, 25 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• app/Intro.hs +40/−8
• app/Main.hs +1/−1
• app/Stack.hs +0/−61
• creditmonad.cabal +3/−4
• src/Control/Monad/Credit.hs +4/−4
• src/Control/Monad/Credit/Base.hs +4/−2
• src/Control/Monad/Credit/CounterM.hs +3/−0
• src/Control/Monad/Credit/CreditM.hs +12/−3
• src/Test/Credit.hs +58/−34
• src/Test/Credit/Deque/Base.hs +41/−56
• src/Test/Credit/Deque/Catenable.hs +2/−10
• src/Test/Credit/Deque/ImplicitCat.hs +0/−1
• src/Test/Credit/Deque/SimpleCat.hs +2/−2
• src/Test/Credit/Finger.hs +179/−161
• src/Test/Credit/Heap/Base.hs +29/−48
• src/Test/Credit/Heap/Scheduled.hs +5/−5
• src/Test/Credit/Queue/Bankers.hs +57/−28
• src/Test/Credit/Queue/Base.hs +12/−16
• src/Test/Credit/Queue/Implicit.hs +1/−7
• src/Test/Credit/Queue/Realtime.hs +25/−18
• src/Test/Credit/Queue/Streams.hs +58/−67
• src/Test/Credit/RandomAccess/Base.hs +17/−21
• src/Test/Credit/RandomAccess/Binary.hs +1/−1
• src/Test/Credit/RandomAccess/Zeroless.hs +1/−1
• src/Test/Credit/Sortable/Base.hs +10/−15

@@ -4,31 +4,31 @@ module Intro where  import Control.Monad-import System.Environment (getArgs)-import Test.QuickCheck- import Control.Monad.Credit+import Test.Credit+import Test.QuickCheck+import Data.Tree -data Batched a = Batched [a] [a]+data Batched a m = Batched [a] [a]   deriving (Eq, Ord, Show)  rev :: MonadCount m => [a] -> [a] -> m [a] rev [] acc = pure acc rev (x : xs) acc = tick >> rev xs (x : acc) -batched :: MonadCount m => [a] -> [a] -> m (Batched a)+batched :: MonadCount m => [a] -> [a] -> m (Batched a m) batched [] rear = do   front <- rev rear []   pure $ Batched front [] batched front rear = pure $ Batched front rear -empty :: MonadCount m => m (Batched a)+empty :: MonadCount m => m (Batched a m) empty = pure $ Batched [] [] -snoc :: MonadCount m => Batched a -> a -> m (Batched a)+snoc :: MonadCount m => Batched a m -> a -> m (Batched a m) snoc   (Batched front rear) x = batched front (x : rear) -uncons :: MonadCount m => Batched a -> m (Maybe (a, Batched a))+uncons :: MonadCount m => Batched a m -> m (Maybe (a, Batched a m)) uncons (Batched [] []) = pure Nothing uncons (Batched (x:front) rear) = do   q' <- batched front rear@@ -45,3 +45,35 @@ testBatched =   runCounterM $ empty >>= flip (foldM snoc) [1..10]                       >>= unfoldM uncons++data QueueOp a = Snoc a | Uncons+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (QueueOp a) where+  arbitrary = frequency+    [ (7, Snoc <$> arbitrary), (3, pure Uncons) ]++instance (Arbitrary a, Show a)+      => DataStructure (Batched a) (QueueOp a) where+  create = pure $ Batched [] []++  perform sz q (Snoc x) = (sz + 1,) <$> snoc q x+  perform sz q Uncons = do+    m <- uncons q+    case m of+      Nothing -> pure (sz, Batched [] [])+      Just (_, q') -> pure (sz - 1, q')++  cost n (Snoc _) = 1+  cost n Uncons   = 0++testSeq :: IO ()+testSeq = quickCheck $ checkCredits @(Batched Int) Path++genTree :: Strategy -> IO ()+genTree s = +  putStrLn . drawTree . fmap show+    =<< generate (genExecutionTrace @(QueueOp Int) s)++testPar :: IO ()+testPar = quickCheck $ checkCredits @(Batched Int) Random

@@ -35,7 +35,7 @@ import Test.Credit.RandomAccess.Zeroless  run :: forall t op. (MemoryStructure t, DataStructure t op) => Args -> Strategy -> IO Result-run args strat = quickCheckWithResult args $ checkCreditsMemory @t strat+run args strat = quickCheckWithResult args $ checkCreditsTrace @t strat  newtype Alpha = Alpha Char   deriving (Eq, Ord)

@@ -1,61 +0,0 @@-module Stack where--fn :: Int -> (a -> a) -> a -> a-fn 0 f x = x-fn n f x = fn (n - 1) f (f x)--suc :: Int -> Int-suc n = n + 1--exp1 :: Int -> Int -> Int-exp1 m n = fn m (fn n) suc 0------data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)--call :: Fun b -> b -> b-call (Unit f) x = f x-call (Rec env f) x = f env x--fn' :: Int -> Fun b -> b -> b-fn' 0 f x = x-fn' n f x = fn' (n - 1) f (call f x)--fn1 :: Int -> Fun b -> Fun b-fn1 n f = Rec f (fn' n)--exp2 :: Int -> Int -> Int-exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0------data Closure b where-  Exists :: a -> (a -> b -> b) -> Closure b--callC :: Closure b -> b -> b-callC (Exists x f) y = f x y--fnC :: Int -> Closure b -> b -> b-fnC 0 c x = x-fnC n c x = fnC (n - 1) c (callC c x)--fnC1 :: Int -> Closure b -> Closure b-fnC1 n c = Exists c (fnC n)--fnC1' :: Int -> () -> Closure b -> Closure b-fnC1' n () c = fnC1 n c--sucC :: () -> Int -> Int-sucC () n = n + 1--exp3 :: Int -> Int -> Int-exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0-------- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...--- [[\x.^n e]] = (fn, env) where---   fn env x = [[e]]---   env = "free vars in [[e]]"-

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           creditmonad-version:        1.0.0+version:        1.1.0 synopsis:       Reasoning about amortized time complexity description:    Persistent data structures are ubiquitous in functional                 programming languages and their designers frequently have to@@ -72,7 +72,7 @@       Control.Monad.Credit.CounterM   hs-source-dirs:       src-  ghc-options: -Wall -Wno-name-shadowing+  ghc-options: -Wall -Wno-name-shadowing -Wno-unused-matches   build-depends:       QuickCheck >=2.14 && <3     , STMonadTrans ==0.4.*@@ -87,10 +87,9 @@   other-modules:       Implicit       Intro-      Stack   hs-source-dirs:       app-  ghc-options: -Wall -Wno-name-shadowing -O2 -fworker-wrapper-cbv -threaded -rtsopts+  ghc-options: -Wall -Wno-name-shadowing -Wno-unused-matches -O2 -fworker-wrapper-cbv -threaded -rtsopts   build-depends:       QuickCheck >=2.14 && <3     , STMonadTrans ==0.4.*

@@ -2,15 +2,15 @@  module Control.Monad.Credit    (-  -- * Computations with credits+  -- * Computations with Credits     Control.Monad.Credit.Base.MonadCount(..), Control.Monad.Credit.Base.MonadLazy (..), Control.Monad.Credit.Base.HasStep(..), Control.Monad.Credit.Base.Lazy(..)-  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)+  , Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)   -- * Counter Monad-  , Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT+  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT   -- * Credit Monad   , Control.Monad.Credit.CreditM.CreditM, Control.Monad.Credit.CreditM.runCreditM, Control.Monad.Credit.CreditM.CreditT, Control.Monad.Credit.CreditM.runCreditT   , Control.Monad.Credit.CreditM.Error(..), Control.Monad.Credit.Base.Cell-  -- * Pretty-printing memory cells+  -- * Pretty-Printing Memory Cells   , Control.Monad.Credit.Base.Memory, Control.Monad.Credit.Base.mkMCell, Control.Monad.Credit.Base.mkMList, linearize   , Control.Monad.Credit.Base.MemoryCell(..), Control.Monad.Credit.Base.MonadMemory(..), Control.Monad.Credit.Base.PrettyCell(..), Control.Monad.Credit.Base.MemoryStructure(..)   ) where

@@ -39,6 +39,8 @@   data Thunk m :: (Type -> Type) -> Type -> Type   delay :: t a -> m (Thunk m t a)   -- ^ delay creates a new cell with the given thunk+  value :: a -> m (Thunk m t a)+  -- ^ value creates a new cell with the given value   force :: HasStep t m => Thunk m t a -> m a   -- ^ force retrieves and evaluates the thunk of a cell   lazymatch :: Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b@@ -51,7 +53,7 @@  -- | A basic thunk that contains the computation to be evaluated. -- This type can be used to express any thunk but its disadvantage is that--- it will be printed merely as "<lazy>".+-- its content cannot be inspected. newtype Lazy m a = Lazy (m a)  instance HasStep (Lazy m) m where@@ -108,7 +110,7 @@ instance Monad m => MemoryCell m (Lazy m a) where   prettyCell (Lazy _) = pure $ mkMCell "<lazy>" [] -class Monad m => MonadMemory m where+class MonadLazy m => MonadMemory m where   prettyThunk :: (MemoryCell m a, MemoryCell m (t a)) => Thunk m t a -> m Memory  instance (MonadMemory m, MemoryCell m a, MemoryCell m (t a)) => MemoryCell m (Thunk m t a) where

@@ -66,6 +66,9 @@   delay a = do     s <- liftST $ newSTRef (Left a)     pure (Thunk s)+  value b = do+    s <- liftST $ newSTRef (Right b)+    pure (Thunk s)   force (Thunk t) = do     t' <- liftST $ readSTRef t     case t' of

@@ -3,10 +3,12 @@ module Control.Monad.Credit.CreditM (CreditM, Error(..), runCreditM, CreditT, runCreditT, resetCurrentThunk) where  import Prelude hiding (lookup)+import Control.Monad import Control.Monad.Except import Control.Monad.Identity import Control.Monad.State.Lazy import Control.Monad.ST.Trans+import Data.Either import Data.Map (Map) import qualified Data.Map as Map import Data.IntMap (IntMap)@@ -172,6 +174,11 @@     withCredits $ pure . open i     s <- liftST $ newSTRef (Left a)     pure (Thunk i s)+  value b = do+    i <- getNext+    withCredits $ pure . open i+    s <- liftST $ newSTRef (Right b)+    pure (Thunk i s)   force (Thunk i t) = do     t' <- liftST $ readSTRef t     case t' of@@ -212,8 +219,10 @@       me <- getMe       withCredits $ subCredit me n . addCredit i n     else pure ()-  hasAtLeast (Thunk i _) n =-    assertAtLeast i n+  hasAtLeast (Thunk i t) n = do+    t' <- liftST $ readSTRef t+    when (isLeft t') $ do+      assertAtLeast i n  instance Monad m => MonadInherit (CreditT s m) where   {-# SPECIALIZE instance MonadInherit (CreditT s Identity) #-}@@ -265,7 +274,7 @@   pretty (OutOfCredits i) = "Out of credits for" <+> pretty i   pretty (InvalidAccount i) = "Invalid account for" <+> pretty i   pretty (InvalidTick i) = "Invalid tick for" <+> pretty i-  pretty (ClosedCurrent (Cell 0)) = "Closed maint thread account. Never invoke creditAllTo on main thread."+  pretty (ClosedCurrent (Cell 0)) = "Closed main thread account. Never invoke creditAllTo on main thread."   pretty (ClosedCurrent i) = "Closed current account" <+> pretty i   pretty (UserError e) = "User error:" <+> pretty e   pretty (AssertionFailed i n m) = pretty i <+> "should have" <+> pretty n <+> "credits but only has" <+> pretty m

@@ -2,12 +2,14 @@  module Test.Credit   (-  -- * Common time-complexity functions+  -- * Common Time-Complexity Functions     Size, logstar, log2, linear-  -- * Tree shapes for testing-  , Strategy(..), genTree-  -- * Testing data structures on trees of operations-  , DataStructure(..), runTree, checkCredits, runTreeMemory, checkCreditsMemory+  -- * Execution Traces for Testing+  , Strategy(..), genExecutionTrace+  -- * Running Data Structures on Execution Traces+  , DataStructure(..), runTree, runTreeTrace+  -- * Testing Data Structures on Execution Traces+  , checkCredits, checkCreditsTrace   ) where  import Data.Either@@ -70,11 +72,11 @@ data Strategy = Path | Bloom | Pennant | Random   deriving (Eq, Ord, Show) -genTree :: Arbitrary op => Strategy -> Gen (Tree op)-genTree Path = fromSeqTree <$> arbitrary-genTree Bloom = fromBloomTree <$> arbitrary-genTree Pennant = fromPennantTree <$> arbitrary-genTree Random = fromPrsTree <$> arbitrary+genExecutionTrace :: Arbitrary op => Strategy -> Gen (Tree op)+genExecutionTrace Path = fromSeqTree <$> arbitrary+genExecutionTrace Bloom = fromBloomTree <$> arbitrary+genExecutionTrace Pennant = fromPennantTree <$> arbitrary+genExecutionTrace Random = fromPrsTree <$> arbitrary  newtype Size = Size Int   deriving (Eq, Ord, Show)@@ -102,27 +104,41 @@ linear (Size n) = fromInteger $ toInteger n  class (Arbitrary op, Show op) => DataStructure t op | t -> op where-  create :: forall m. MonadInherit m => t m-  action :: forall m. MonadInherit m => t m -> op -> (Credit, m (t m))+  cost :: Size -> op -> Credit+  -- ^ Given a size and an operation, return the cost of the operation.+  -- This function can not inspect the internal state of the data structure.+  create :: MonadLazy m => m (t m)+  -- ^ create a new instance of the data structure.+  -- We allow the computation to be lazy, since lazy data structures+  -- often contain thunks even if they contain no elements.+  -- The create data structure is assumed to have size zero.+  perform :: MonadInherit m => Size -> t m -> op -> m (Size, t m)+  -- ^ Given a data structure, its size, and an operation,+  -- return the updated size and data structure.+  -- We allow the size to depend on the internal state of the data structure,+  -- since some operations, like insertions into a binary search tree, might+  -- return different sizes depending on whether a new element is already present. +-- | Evaluate an execution trace of operations on the given data structure+-- using the credit monad. Returns either an error or unit if the evaluation succeeded. runTree :: forall t op. DataStructure t op => Tree op -> Either Error ()-runTree tree = runCreditM 0 (go (create @t) tree)+runTree tree = runCreditM 0 (create @t >>= flip (go 0) tree)   where-    go :: forall s t op. DataStructure t op => t (CreditM s) -> Tree op -> CreditM s ()-    go a (Node op ts) = do-      let (cr, f) = action a op+    go :: forall s t op. DataStructure t op => Size -> t (CreditM s) -> Tree op -> CreditM s ()+    go sz a (Node op ts) = do+      let cr = cost @t sz op       resetCurrentThunk cr-      a' <- f-      mapM_ (go a') ts+      (sz, a) <- perform sz a op+      mapM_ (go sz a) ts  isPersistent :: Tree a -> Bool isPersistent (Node _ ts) = length ts > 1 || any isPersistent ts --- | Evaluate the queue operations using the given strategy on the given queue--- Reports only if evaluation succeeded.+-- | Test the given data structure in the credit monad using the given strategy.+-- This property only reports if evaluation succeeded or not. checkCredits :: forall t op. DataStructure t op => Strategy -> Property checkCredits strat =-  forAllShrink (genTree strat) shrink $ \t ->+  forAllShrink (genExecutionTrace strat) shrink $ \t ->     classify (isPersistent t) "persistent" $       isRight $ runTree @t t @@ -141,6 +157,10 @@ extract (Branch x ls Root) = Node x (reverse ls) extract z = extract (up z) +-- | If each node has only a single child, flatten the tree+-- by making all elements children of the root.+-- This improves the readability of the tree when printed.+-- Otherwise, return the original tree. flattenTree :: Tree a -> Tree a flattenTree t = case go t of   Just (x:xs) -> Node x (map (\x -> Node x []) xs)@@ -156,25 +176,29 @@  type M s = CreditT s (State (RoseZipper String)) -runTreeMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String-runTreeMemory tree = showState $ runState (runCreditT 0 (go (create @t) tree)) Root+-- | Evaluate an execution trace of operations on the given data structure+-- using the credit monad. Returns a pretty-printed string of the execution trace+-- annotated with the internal state of the data structure at each step.+runTreeTrace :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String+runTreeTrace tree = showState $ runState (runCreditT 0 (create @t >>= flip (go 0) tree)) Root   where-    go :: forall s t op. (MemoryStructure t, DataStructure t op) => t (M s) -> Tree op -> M s ()-    go a (Node op ts) = do-      let (cr, f) = action a op+    go :: forall s t op. (MemoryStructure t, DataStructure t op) => Size -> t (M s) -> Tree op -> M s ()+    go sz a (Node op ts) = do+      let cr = cost @t sz op       resetCurrentThunk cr       lift $ modify' (Branch (show op ++ ": ") []) -      a' <- f-      mem <- prettyStructure a'+      (sz, a) <- perform sz a op+      mem <- prettyStructure a       let s = renderString $ layoutSmart (defaultLayoutOptions { layoutPageWidth = Unbounded }) $ nest 2 $ pretty $ mem       lift $ modify' (extend s)-      mapM_ (go a') ts+      mapM_ (go sz a) ts       lift $ modify' up --- | Evaluate the queue operations using the given strategy on the given queue--- Reports only if evaluation succeeded.-checkCreditsMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property-checkCreditsMemory strat =-  forAllShrinkShow (genTree strat) shrink (\t -> runTreeMemory @t t) $ \t ->+-- | Test the given data structure in the credit monad using the given strategy.+-- If evaluation fails, this property prints the execution trace+-- annotated with the internal state of the data structure at each step.+checkCreditsTrace :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property+checkCreditsTrace strat =+  forAllShrinkShow (genExecutionTrace strat) shrink (\t -> runTreeTrace @t t) $ \t ->     classify (isPersistent t) "persistent" $       isRight $ runTree @t t

@@ -20,7 +20,7 @@     ]  class Deque q where-  empty :: MonadInherit m => m (q a m)+  empty :: MonadLazy m => m (q a m)   cons :: MonadInherit m => a -> q a m -> m (q a m)   snoc :: MonadInherit m => q a m -> a -> m (q a m)   uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))@@ -30,39 +30,32 @@ class Deque q => BoundedDeque q where   qcost :: Size -> DequeOp a -> Credit -data D q a m = E | D Size (q (PrettyCell a) m)+data D q a m = D (q (PrettyCell a) m)  instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (D q a m) where-  prettyCell E = pure $ mkMCell "" []-  prettyCell (D _ q) = prettyCell q+  prettyCell (D q) = prettyCell q  instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (D q a) where-  prettyStructure E = pure $ mkMCell "" []-  prettyStructure (D _ q) = prettyStructure q+  prettyStructure (D q) = prettyStructure q -act :: (MonadInherit m, Deque q) => Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)-act sz q (Cons x) = D (sz + 1) <$> cons (PrettyCell x) q-act sz q (Snoc x) = D (sz + 1) <$> snoc q (PrettyCell x)-act sz q Uncons = do-  m <- uncons q-  case m of-    Nothing -> pure E-    Just (_, q') -> pure $ D (max 0 (sz - 1)) q'-act sz q Unsnoc = do-  m <- unsnoc q-  case m of-    Nothing -> pure E-    Just (q', _) -> pure $ D (max 0 (sz - 1)) q'-act sz q Concat = pure $ D sz q  instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (D q a) (DequeOp a) where-  create = E-  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)-  action (D sz q) op = (qcost @q sz op, act sz q op)--size :: D q a m -> Size-size E = 0-size (D sz _) = sz+  cost _ Concat = 0+  cost sz op = qcost @q sz op+  create = D <$> empty+  perform sz (D q) (Cons x) = (sz + 1,) <$> D <$> cons (PrettyCell x) q+  perform sz (D q) (Snoc x) = (sz + 1,) <$> D <$> snoc q (PrettyCell x)+  perform sz (D q) Uncons = do+    m <- uncons q+    case m of+      Nothing -> (sz,) <$> D <$> empty+      Just (_, q') -> pure (sz - 1, D q')+  perform sz (D q) Unsnoc = do+    m <- unsnoc q+    case m of+      Nothing -> (sz,) <$> D <$> empty+      Just (q', _) -> pure (sz - 1, D q')+  perform sz (D q) Concat = pure $ (sz, D q) -- no op  data BD q a m = BD (D q a m) (D q a m) @@ -78,33 +71,25 @@     q2' <- prettyStructure q2     pure $ mkMCell "Concat" [q1', q2'] -act1 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)-act1 op (BD q1 q2) = do-  q1' <- case q1 of-    E -> empty-    D _ q -> pure q-  q1'' <- act (size q1) q1' op -  pure $ BD q1'' q2--act2 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)-act2 op (BD q1 q2) = do-  let sz = size q2-  q2' <- case q2 of-    E -> empty-    D _ q -> pure q-  q2'' <- act (size q2) q2' op -  pure $ BD q1 q2''--concatenate :: (MonadInherit m, Deque q) => D q a m -> D q a m -> m (D q a m)-concatenate E E = pure E-concatenate (D sz1 q1) E = pure $ D sz1 q1-concatenate E (D sz2 q2) = pure $ D sz2 q2-concatenate (D sz1 q1) (D sz2 q2) = D (sz1 + sz2) <$> concat q1 q2- instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (BD q a) (DequeOp a) where-  create = BD E E-  action (BD q1 q2) (Cons x) = (qcost @q (size q1) (Cons x), act1 (Cons x) (BD q1 q2))-  action (BD q1 q2) (Snoc x) = (qcost @q (size q2) (Snoc x), act2 (Snoc x) (BD q1 q2))-  action (BD q1 q2) Uncons = (qcost @q (size q1) Uncons, act1 Uncons (BD q1 q2))-  action (BD q1 q2) Unsnoc = (qcost @q (size q2) Unsnoc, act2 Unsnoc (BD q1 q2))-  action (BD q1 q2) Concat = (qcost @q (size q1 + size q2) Concat, BD E <$> concatenate q1 q2)+  cost = qcost @q+  create = do+    q1 <- empty+    q2 <- empty+    pure $ BD (D q1) (D q2)+  perform sz (BD q1 q2) (Cons x) = do+    (sz, q1) <- perform sz q1 (Cons x)+    pure (sz, BD q1 q2)+  perform sz (BD q1 q2) (Snoc x) = do+    (sz, q2) <- perform sz q2 (Snoc x)+    pure (sz, BD q1 q2)+  perform sz (BD q1 q2) Uncons = do+    (sz, q1) <- perform sz q1 Uncons+    pure (sz, BD q1 q2)+  perform sz (BD q1 q2) Unsnoc = do+    (sz, q2) <- perform sz q2 Unsnoc+    pure (sz, BD q1 q2)+  perform sz (BD (D q1) (D q2)) Concat = do+    e <- empty+    q <- concat q1 q2+    pure (sz, BD (D e) (D q))

@@ -16,11 +16,9 @@       (Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m) -- ^ tail  data CLazyCon m a where-  Pure :: a -> CLazyCon m a   LinkAll :: Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> CLazyCon m (CatDeque a m)  instance MonadInherit m => HasStep (CLazyCon m) m where-  step (Pure xs) = pure xs   step (LinkAll q) = linkAll q  costSnoc :: Credit@@ -49,7 +47,7 @@ concat' E xs = pure xs concat' xs E = pure xs concat' xs ys = do-  ys <- delay $ Pure ys+  ys <- value ys   link xs ys  -- | Assign credits to the thunk and force it@@ -59,14 +57,12 @@ dischargeThunk s = do   let assign = creditWith s (costSnoc + costUncons) >> force s >> pure ()   lazymatch s (\_ -> assign) $ \case-    Pure _ -> assign     LinkAll q -> do       q' <- Q.lazyqueue q       case q' of         [] -> assign         t' : _ -> do           lazymatch t' (\_ -> assign) $ \case-            Pure _ -> assign             LinkAll _ -> dischargeThunk t'  findFirstThunk :: MonadInherit m => CatDeque a m -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))@@ -79,7 +75,6 @@ seekFirstThunk [] = pure Nothing seekFirstThunk (t : q) = do   mt <- lazymatch t findFirstThunk $ \case-    Pure q' -> findFirstThunk q'     LinkAll _ -> pure $ Just t   case mt of     Nothing -> seekFirstThunk q@@ -114,12 +109,9 @@   qcost _ (Snoc _) = costSnoc   qcost _ Uncons = 4 * costUncons + 3 * costSnoc   qcost _ Unsnoc = 0-  qcost _ Concat = 0+  qcost _ Concat = costSnoc  instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CLazyCon m a) where-  prettyCell (Pure x) = do-    x' <- prettyCell x-    pure $ mkMCell "Pure" [x']   prettyCell (LinkAll q) = do     q' <- prettyCell q     pure $ mkMCell "LinkAll" [q']

@@ -4,7 +4,6 @@ import Control.Monad (join, when) import Prettyprinter (Pretty) import Control.Monad.Credit-import Test.Credit import Test.Credit.Deque.Base import qualified Test.Credit.Deque.Base as D import qualified Test.Credit.Deque.Bankers as D

@@ -4,7 +4,7 @@ import Prettyprinter (Pretty) import Control.Monad import Control.Monad.Credit-import Test.Credit+import Test.Credit (log2) import Test.Credit.Deque.Base import qualified Test.Credit.Deque.Base as D import qualified Test.Credit.Deque.Bankers as D@@ -184,7 +184,7 @@   qcost n (Snoc x) = qcost @(D.BDeque) n (Snoc x)   qcost n Uncons = 1 + qcost @(D.BDeque) n Uncons + 2 * cost   qcost n Unsnoc = 1 + qcost @(D.BDeque) n Unsnoc + 2 * cost-  qcost n Concat = (1 + 6 * cost) * log2 n+  qcost n Concat = cost + (1 + 6 * cost) * log2 n  instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SimpleCat a m) where   prettyCell (Shallow d) = do

@@ -1,10 +1,8 @@-{-# LANGUAGE GADTs, OverloadedLists, LambdaCase #-}+{-# LANGUAGE GADTs, LambdaCase #-}  module Test.Credit.Finger where  import Prelude hiding (head, tail, last, init)-import Data.List.NonEmpty (NonEmpty(..), (<|))-import qualified Data.List.NonEmpty as NE import Control.Monad (when, unless) import Data.Foldable (foldlM, foldrM) import Prettyprinter (Pretty)@@ -25,17 +23,15 @@ data FingerTree v a m   = Empty   | Single a-  | Deep (Thunk m (Lazy m) v) (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)+  | Deep v (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)  data FLazyCon m a where-  FPure :: a -> FLazyCon m a   FCons :: Measured a v => a -> Thunk m (FLazyCon m) (FingerTree v a m) -> FLazyCon m (FingerTree v a m)   FSnoc :: Measured a v => Thunk m (FLazyCon m) (FingerTree v a m) -> a -> FLazyCon m (FingerTree v a m)   FTail :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)   FInit :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)  instance MonadCredit m => HasStep (FLazyCon m) m where-  step (FPure xs) = pure xs   step (FCons x m) = cons x =<< force m   step (FSnoc m x) = flip snoc x =<< force m   step (FTail q) = tail q@@ -49,39 +45,44 @@ --  - snoc and tail spend their second credit on either the old m to be able to force it, --    or on the new m to maintain the invariant. -class Monoid v => Measured a v where+class (Eq v, Monoid v) => Measured a v where   measure :: a -> v -instance Measured a v => Measured [a] v where-  measure = mconcat . map measure+instance (Eq v, Monoid v) => Measured (Tuple v a) v where+  measure (Pair v _ _) = v+  measure (Triple v _ _ _) = v  instance Measured a v => Measured (Digit a) v where   measure = measure . toList -instance Monoid v => Measured (Tuple v a) v where-  measure (Pair v _ _) = v-  measure (Triple v _ _ _) = v+instance Measured a v => Measured [a] v where+  measure = mconcat . map measure -measurement :: (MonadCredit m, Measured a v) => FingerTree v a m -> m v-measurement Empty = pure $ mempty-measurement (Single x) = pure $ measure x-measurement (Deep vm f m r) = do-  vm' <- force vm-  pure $ measure f <> vm' <> measure r+instance (Measured a v, Measured b v) => Measured (a, b) v where+  measure (x, y) = measure x <> measure y -forceAll :: (MonadCredit m, Measured a v) => FingerTree v a m -> m ()-forceAll Empty = pure ()-forceAll (Single _) = pure ()-forceAll (Deep _ _ m _) = do-  creditWith m 2-  forceAll =<< force m+instance (Measured a v, Measured b v, Measured c v) => Measured (a, b, c) v where+  measure (x, y, z) = measure x <> measure y <> measure z +instance (Measured a v, Measured b v) => Measured (Either a b) v where+  measure (Left x) = measure x+  measure (Right y) = measure y++instance Measured a v => Measured (Maybe a) v where+  measure Nothing = mempty+  measure (Just a) = measure a++instance Measured a v => Measured (FingerTree v a m) v where+  measure Empty = mempty+  measure (Single x) = measure x+  measure (Deep vm f m r) = measure f <> vm <> measure r+ isTwo :: Digit a -> Bool isTwo (Two _ _) = True isTwo _ = False  empty :: MonadCredit m => m (Thunk m (FLazyCon m) (FingerTree v a m))-empty = delay $ FPure Empty+empty = value $ Empty  pair :: Measured a v => a -> a -> Tuple v a pair x y = Pair (measure x <> measure y) x y@@ -89,20 +90,16 @@ triple :: Measured a v => a -> a -> a -> Tuple v a triple x y z = Triple (measure x <> measure y <> measure z) x y z -deep :: (MonadCredit m, Measured a v) => Thunk m (Lazy m) v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)+deep :: (MonadCredit m, Measured a v) => v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m) deep v f m r = do-  let oneIfDangerous d = if isTwo d then 0 else 1-  mIsPure <- lazymatch m (\_ -> pure True) $ \case-    FPure _ -> pure True-    _ -> pure False-  unless mIsPure $-    m `hasAtLeast` (oneIfDangerous f + oneIfDangerous r)+  let dang d = if isTwo d then 0 else 1+  m `hasAtLeast` (dang f + dang r)+  lazymatch m (\m -> when (v /= measure m) $ error "invalid measure") (\_ -> pure ())   pure $ Deep v f m r -deep' :: (MonadCredit m, Measured a v) => Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)-deep' f mkM r = do+deep' :: (MonadCredit m, Measured a v) => v -> Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)+deep' vm f mkM r = do   m <- mkM-  vm <- delay $ Lazy $ measurement =<< force m   deep vm f m r  isEmpty :: FingerTree v a m -> Bool@@ -117,68 +114,90 @@ toTree :: (MonadCredit m, Measured a v) => [a] -> m (FingerTree v a m) toTree [] = pure Empty toTree [x] = pure $ Single x-toTree [x,y] = deep' (One x) empty (One y)-toTree [x,y,z] = deep' (Two x y) empty (One z)+toTree [x,y] = deep' mempty (One x) empty (One y)+toTree [x,y,z] = deep' mempty (Two x y) empty (One z)  toDigit :: Tuple v a -> Digit a toDigit (Pair _ x y) = Two x y toDigit (Triple _ x y z) = Three x y z  cons :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)-cons x q = tick >> cons' x q--cons' :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)-cons' x Empty = pure $ Single x-cons' x (Single y) = do-  deep' (One x) empty (One y)-cons' x (Deep vq pr q u) = case pr of-  One y       -> deep vq (Two x y) q u-  Two y z     -> creditWith q 1 >> pure (Deep vq (Three x y z) q u)-  Three y z w -> do-    q' <- delay $ FCons (pair z w) q-    if isTwo u-      then creditWith q 1-      else creditWith q' 1-    vq' <- delay $ Lazy $ measurement =<< force q'-    deep vq' (Two x y) q' u+cons x q = do+  tick+  case q of+    Empty -> pure $ Single x+    Single y -> do+      deep' mempty (One x) empty (One y)+    Deep vq (One y) q u -> do+      deep vq (Two x y) q u+    Deep vq (Two y z) q u -> do+      q `creditWith` 1+      deep vq (Three x y z) q u+    Deep vq (Three y z w) q u -> do+      q' <- delay $ FCons (pair z w) q+      if isTwo u+        then q  `creditWith` 1+        else q' `creditWith` 1+      deep (measure (z, w) <> vq) (Two x y) q' u  head :: MonadCredit m => FingerTree v a m -> m a head Empty = fail "head: empty queue" head (Single x) = pure x head (Deep _ s _ _) = pure $ let (h:_) = toList s in h -tail :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)-tail Empty = tick >> pure Empty-tail (Single _) = tick >> pure Empty-tail (Deep vq (Three _ x y) q u) = tick >> pure (Deep vq (Two x y) q u)-tail (Deep vq (Two _ x) q u) = tick >> creditWith q 1 >> pure (Deep vq (One x) q u)-tail (Deep _ (One _) q u) = tick >> do-  when (isTwo u) $ creditWith q 1-  q' <- force q-  deep0 q' u+tail :: (MonadCredit m, Measured a v)+     => FingerTree v a m -> m (FingerTree v a m)+tail q = do+  tick+  case q of+    Empty -> pure Empty+    Single _ -> pure Empty+    Deep vq (Three _ x y) q u -> do+      deep vq (Two x y) q u+    Deep vq (Two _ x) q u -> do+      q `creditWith` 1+      deep vq (One x) q u+    Deep _ (One _) q u -> do+      when (isTwo u) $ q `creditWith` 1+      force q >>= (`deep0` u) -deep0 :: (MonadCredit m, Measured a v) => FingerTree v (Tuple v a) m -> Digit a -> m (FingerTree v a m)-deep0 Empty s = toTree $ toList s+deep0 :: (MonadCredit m, Measured a v)+      => FingerTree v (Tuple v a) m -> Digit a+      -> m (FingerTree v a m)+deep0 Empty u = toTree $ toList u deep0 q u = do-  h <- head q-  case h of+  hd <- head q+  case hd of     Pair _ x y -> do       t <- delay $ FTail q-      unless (isTwo u) $ creditWith t 1-      vt <- delay $ Lazy $ measurement =<< force t-      deep vt (Two x y) t u+      unless (isTwo u) $ t `creditWith` 1+      let v = measureTail q+      deep v (Two x y) t u     Triple _ x _ _ -> do-      q' <- map1 chop q-      deep' (One x) (delay $ FPure q') u-      where chop (Triple _ _ y z) = pair y z+      let q' = map1 chop q+      q'' <- value q'+      deep (measure q') (One x) q'' u+  where chop (Triple _ _ y z) = pair y z -map1 :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)-map1 _ Empty = pure Empty-map1 f (Single x) = pure $ Single (f x)-map1 f (Deep vq (One x) q u) = deep vq (One (f x)) q u-map1 f (Deep vq (Two x y) q u) = deep vq (Two (f x) y) q u-map1 f (Deep vq (Three x y z) q u) = deep vq (Three (f x) y z) q u+map1 :: (Measured a v) => (a -> a)+     -> FingerTree v a m -> FingerTree v a m+map1 f q = case q of+  Empty -> Empty+  Single x -> Single (f x)+  Deep v (One x)       m sf -> Deep v (One (f x))       m sf+  Deep v (Two x y)     m sf -> Deep v (Two (f x) y)     m sf+  Deep v (Three x y z) m sf -> Deep v (Three (f x) y z) m sf +measureTail :: Measured a v+            => FingerTree v (Tuple v a) m -> v+measureTail q = case q of+  Empty -> mempty+  Single _ -> mempty+  Deep v pr _ sf -> case pr of+    One _       ->                   v <> measure sf+    Two _ y     -> measure y      <> v <> measure sf+    Three _ y z -> measure (y, z) <> v <> measure sf+ uncons :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (a, FingerTree v a m)) uncons q =   if isEmpty q@@ -188,15 +207,15 @@       t <- tail q       pure $ Just (h, t) -deepL :: (MonadCredit m, Measured a v) => [a] -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)+deepL :: (MonadCredit m, Measured a v) => [a] -> v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m) deepL [] _ m sf = do   m' <- uncons =<< force m   case m' of     Nothing -> toTree $ toList sf     Just (Pair _ x y, m'') -> do-      deep' (Two x y) (delay $ FPure m'') sf+      deep' (measure m'') (Two x y) (value m'') sf     Just (Triple _ x y z, m'') -> do-      deep' (Three x y z) (delay $ FPure m'') sf+      deep' (measure m'') (Three x y z) (value m'') sf deepL [x] vm m sf = deep vm (One x) m sf deepL [x,y] vm m sf = deep vm (Two x y) m sf deepL [x,y,z] vm m sf = deep vm (Three x y z) m sf@@ -206,50 +225,65 @@ last (Single x) = pure x last (Deep _ _ _ s) = pure $ let (h:_) = reverse $ toList s in h -snoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)-snoc q y = tick >> snoc' q y--snoc' :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)-snoc' Empty y = pure $ Single y-snoc' (Single x) y = deep' (One x) empty (One y)-snoc' (Deep vq u q (One x)) y = deep vq u q (Two x y)-snoc' (Deep vq u q (Two x y)) z = creditWith q 1 >> pure (Deep vq u q (Three x y z))-snoc' (Deep _ u q (Three x y z)) w = do-  q' <- delay $ FSnoc q (pair x y)-  if isTwo u-    then creditWith q 1-    else creditWith q' 1-  vq' <- delay $ Lazy $ measurement =<< force q'-  deep vq' u q' (Two z w)+snoc :: (MonadCredit m, Measured a v)+     => FingerTree v a m -> a -> m (FingerTree v a m)+snoc q w = do+  tick+  case q of+    Empty -> pure $ Single w+    Single x -> do+      em <- value Empty+      deep mempty (One x) em (One w)+    Deep v front middle (One x) ->+      deep v front middle (Two x w)+    Deep v front middle (Two x y) -> do+      middle `creditWith` 1+      deep v front middle (Three x y w)+    Deep v front middle (Three x y z) -> do+      t <- delay $ FSnoc middle (pair x y)+      if isTwo front+        then middle `creditWith` 1+        else t      `creditWith` 1+      deep (v <> measure (x, y)) front t (Two z w)  init :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)-init Empty = tick >> pure Empty-init (Single _) = tick >> pure Empty-init (Deep vq u q (Three x y _)) = tick >> pure (Deep vq u q (Two x y))-init (Deep vq u q (Two x _)) = tick >> creditWith q 1 >> pure (Deep vq u q (One x))-init (Deep _ u q (One _)) = tick >> when (isTwo u) (creditWith q 1) >> force q >>= deepN u+init q = do+  tick+  case q of+    Empty -> pure Empty+    Single _ -> pure Empty+    Deep vq f q (Three x y _) -> do+      deep vq f q (Two x y)+    Deep vq f q (Two x _) -> do+      q `creditWith` 1+      deep vq f q (One x)+    Deep _ f q (One _) -> do+      when (isTwo f) $+        q `creditWith` 1+      deepN f =<< force q  deepN :: (MonadCredit m, Measured a v) => Digit a -> FingerTree v (Tuple v a) m -> m (FingerTree v a m) deepN s Empty = toTree $ toList s-deepN u q = do-  l <- last q-  case l of-    Pair _ x y -> do-      t <- delay $ FInit q+deepN s (Single (Pair _ x y)) = do+  deep' mempty s empty (Two x y)+deepN s (Single (Triple _ x y z)) = do+  deep' (measure x <> measure y) s (value (Single (pair x y))) (One z)+deepN u (Deep vq pr q sf) = do+  case chopN sf of+    Left (vsf', x, y) -> do+      t <- delay $ FInit (Deep vq pr q sf)       unless (isTwo u) $ creditWith t 1-      vt <- delay $ Lazy $ measurement =<< force t-      deep vt u t (Two x y)-    Triple _ _ _ z -> do-      q' <- mapN chop q-      deep' u (delay $ FPure q') (One z)-      where chop (Triple _ x y _) = pair x y+      deep (measure pr <> vq <> vsf') u t (Two x y)+    Right (sf', x) -> do+      deep' (measure pr <> vq <> measure sf') u (value (Deep vq pr q sf')) (One x) -mapN :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)-mapN _ Empty = pure $ Empty-mapN f (Single x) = pure $ Single (f x)-mapN f (Deep vq u q (One x)) = deep vq u q (One (f x))-mapN f (Deep vq u q (Two x y)) = deep vq u q (Two x (f y))-mapN f (Deep vq u q (Three x y z)) = deep vq u q (Three x y (f z))+chopN :: (Measured a v) => Digit (Tuple v a) -> Either (v, a, a) (Digit (Tuple v a), a)+chopN (One (Pair _ x y)) = Left (mempty, x, y)+chopN (Two x (Pair _ y z)) = Left (measure x, y, z)+chopN (Three x y (Pair _ z w)) = Left (measure x <> measure y, z, w)+chopN (One (Triple _ x y z)) = Right (One (pair x y), z)+chopN (Two x (Triple _ y z w)) = Right (Two x (pair y z), w)+chopN (Three x y (Triple _ z w u)) = Right (Three x y (pair z w), u)  unsnoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (FingerTree v a m, a)) unsnoc q =@@ -260,15 +294,15 @@       t <- init q       pure $ Just (t, h) -deepR :: (MonadCredit m, Measured a v) => Digit a -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m)+deepR :: (MonadCredit m, Measured a v) => Digit a -> v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m) deepR s _ m [] = do   m' <- unsnoc =<< force m   case m' of     Nothing -> toTree $ toList s     Just (m'', Pair _ x y) -> do-      deep' s (delay $ FPure m'') (Two x y)+      deep' (measure m'') s (value m'') (Two x y)     Just (m'', Triple _ x y z) -> do-      deep' s (delay $ FPure m'') (Three x y z)+      deep' (measure m'') s (value m'') (Three x y z) deepR s vm m [x] = deep vm s m (One x) deepR s vm m [x, y] = deep vm s m (Two x y) deepR s vm m [x, y, z] = deep vm s m (Three x y z)@@ -290,14 +324,13 @@   creditWith q2 2   q2 <- force q2   q <- glue q1 (toTuples (toList v1 ++ as ++ toList u2)) q2-  deep' u1 (delay $ FPure q) v2+  deep' (measure q) u1 (value q) v2  concat' :: (MonadCredit m, Measured a v) => FingerTree v a m -> FingerTree v a m -> m (FingerTree v a m) concat' q1 q2 = glue q1 [] q2  data Split v a m = Split-  { measureOfSmaller :: v-  , smaller :: FingerTree v a m+  { smaller :: FingerTree v a m   , found   :: a   , bigger  :: FingerTree v a m   }@@ -312,38 +345,32 @@   | p (i <> measure x <> measure y) = ([x], y, [z])   | otherwise = ([x, y], z, []) --- For '(Split vml ml xs mr) <- splitTree p i m', we have 'vml = measurement ml'. splitTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Split v a m) splitTree p i Empty = fail "splitTree: empty tree"-splitTree p i (Single x) = pure $ Split mempty Empty x Empty-splitTree p i (Deep vm pr m sf) = tick >> do-  vm' <- force vm+splitTree p i (Single x) = pure $ Split Empty x Empty+splitTree p i (Deep vm pr m sf) = do+  tick+  m `creditWith` 2   let vpr = i <> measure pr-  let vprm = vpr <> vm'+  let vprm = vpr <> vm   if p vpr then do     let (l, x, r) = splitDigit p i pr-    Split (measure l) <$> toTree l <*> pure x <*> deepL r vm m sf+    Split <$> toTree l <*> pure x <*> deepL r vm m sf   else if p vprm then do-    Split vml ml xs mr <- splitTree p vpr =<< force m+    Split ml xs mr <- splitTree p vpr =<< force m+    let vml = measure ml     let (l, x, r) = splitDigit p (vpr <> vml) (toDigit xs)-    -- [ml', mr', vmr', vml'] <- mapM (delay . Lazy)-      -- [pure ml, pure mr, measurement mr, pure vml]-    ml' <- delay $ FPure ml-    mr' <- delay $ FPure mr-    vmr' <- delay $ Lazy $ measurement mr-    vml' <- delay $ Lazy $ pure vml-    Split (measure pr <> vml <> measure l) <$> deepR pr vml' ml' l <*> pure x <*> deepL r vmr' mr' sf+    [ml', mr'] <- mapM value [ml, mr]+    Split <$> deepR pr vml ml' l <*> pure x <*> deepL r (measure mr) mr' sf   else do     let (l, x, r) = splitDigit p vprm sf-    Split (measure pr <> vm' <> measure l) <$> deepR pr vm m l <*> pure x <*> toTree r+    Split <$> deepR pr vm m l <*> pure x <*> toTree r  split :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m, FingerTree v a m) split p Empty = pure (Empty, Empty) split p xs = do-  forceAll xs-  mxs <- measurement xs-  if p mxs-    then do (Split _ l x r) <- splitTree p mempty xs+  if p (measure xs)+    then do (Split l x r) <- splitTree p mempty xs             (l,) <$> cons x r     else pure (xs, Empty) @@ -356,8 +383,8 @@ lookupTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Maybe (v, a)) lookupTree p i Empty = pure Nothing lookupTree p i t = do-  forceAll t-  (Split ml _ x _) <- splitTree p i t+  (Split l x _) <- splitTree p i t+  let ml = measure l   pure $ Just (i <> ml, x)  instance MemoryCell m a => MemoryCell m (Digit a) where@@ -386,9 +413,6 @@     pure $ mkMCell "Triple" [a', b', c']  instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FLazyCon m a) where-  prettyCell (FPure x) = do-    x' <- prettyCell x-    pure $ mkMCell "FPure" [x']   prettyCell (FCons x m) = do     -- x' <- prettyCell x     m' <- prettyCell m@@ -476,10 +500,8 @@  newtype FingerRA a m = FingerRA (FingerTree Size (Elem a) m) --- Contrary to Hinze and Paterson, this is not O(1) but O(log n)--- because we need to force all thunks in the tree to get the size.-length :: MonadCredit m => FingerRA a m -> m Size-length (FingerRA t) = measurement t+len :: MonadCredit m => FingerRA a m -> Size+len (FingerRA t) = measure t  splitAt :: MonadCredit m => Int -> FingerRA a m -> m (FingerRA a m, FingerRA a m) splitAt i (FingerRA xs) = do@@ -497,14 +519,12 @@         pure $ Just (x, FingerRA m')   lookup i (FingerRA Empty) = pure Nothing   lookup i (FingerRA xs) = do-    forceAll xs-    (Split _ _ (Elem x) _) <- splitTree (fromIntegral i <) 0 xs+    Split _ (Elem x) _ <- splitTree (fromIntegral i <) 0 xs     pure $ Just x   update i a (FingerRA Empty) = pure $ FingerRA Empty   update i a (FingerRA xs) = do-    forceAll xs-    (Split ml l (Elem x) r) <- splitTree (fromIntegral i <) 0 xs-    if fromIntegral i > ml+    Split l (Elem x) r <- splitTree (fromIntegral i <) 0 xs+    if fromIntegral i > len (FingerRA l)       then FingerRA <$> snoc l (Elem x)       else FingerRA <$> (concat' l =<< cons (Elem a) r) @@ -544,9 +564,7 @@   merge (FingerHeap a) (FingerHeap b) = FingerHeap <$> concat' a b   splitMin (FingerHeap Empty) = pure Nothing   splitMin (FingerHeap xs) = do-    forceAll xs -- 2 * log n-    k <- measurement xs-    (Split _ l (Elem x) r) <- splitTree (k >=) mempty xs -- 3 * log n+    (Split l (Elem x) r) <- splitTree (measure xs >=) mempty xs -- 3 * log n     lr <- concat' l r -- 5 log n     pure $ Just (x, FingerHeap lr) @@ -573,7 +591,7 @@ instance Monoid (Key a) where   mempty = NoKey -instance Measured (Elem a) (Key a) where+instance Eq a => Measured (Elem a) (Key a) where   measure (Elem x) = Key x  newtype FingerSort a m = FingerSort (FingerTree (Key a) (Elem a) m)

@@ -17,7 +17,7 @@     ]  class Heap h where-  empty :: MonadCredit m => m (h a m)+  empty :: MonadLazy m => m (h a m)   insert :: MonadCredit m => Ord a => a -> h a m -> m (h a m)   merge :: MonadCredit m => Ord a => h a m -> h a m -> m (h a m)   splitMin :: MonadCredit m => Ord a => h a m -> m (Maybe (a, h a m))@@ -25,33 +25,25 @@ class Heap h => BoundedHeap h where   hcost :: Size -> HeapOp a -> Credit -data H h a m = E | H Size (h (PrettyCell a) m)+data H h a m = H (h (PrettyCell a) m)  instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (H h a m) where-  prettyCell E = pure $ mkMCell "" []-  prettyCell (H _ h) = prettyCell h+  prettyCell (H h) = prettyCell h  instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (H h a) where-  prettyStructure E = pure $ mkMCell "" []-  prettyStructure (H _ h) = prettyStructure h--act :: (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m)-act sz h (Insert x) = H (sz + 1) <$> insert (PrettyCell x) h-act sz h Merge = pure $ H sz h-act sz h SplitMin = do-  m <- splitMin h-  case m of-    Nothing -> pure E-    Just (_, h') -> pure $ H (max 0 (sz - 1)) h'+  prettyStructure (H h) = prettyStructure h  instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (H h a) (HeapOp a) where-  create = E-  action E op = (hcost @h 0 op, empty >>= flip (act 0) op)-  action (H sz h) op = (hcost @h sz op, act sz h op)--size :: H h a m -> Size-size E = 0-size (H sz _) = sz+  cost sz Merge = 0+  cost sz op = hcost @h sz op+  create = H <$> empty+  perform sz (H h) (Insert x) = (sz + 1,) <$> H <$> insert (PrettyCell x) h+  perform sz (H h) Merge = pure (sz, H h) -- no op+  perform sz (H h) SplitMin = do+    m <- splitMin h+    case m of+      Nothing -> (sz,) <$> H <$> empty+      Just (_, h') -> pure (sz - 1, H h')  data BH h a m = BH (H h a m) (H h a m) @@ -67,30 +59,19 @@     h2' <- prettyStructure h2     pure $ mkMCell "Merge" [h1', h2'] -act1 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)-act1 op (BH h1 h2) = do-  h1' <- case h1 of-    E -> empty-    H _ h -> pure h-  h1'' <- act (size h1) h1' op -  pure $ BH h1'' h2--act2 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)-act2 op (BH h1 h2) = do-  h2' <- case h2 of-    E -> empty-    H _ h -> pure h-  h2'' <- act (size h2) h2' op -  pure $ BH h1 h2''--mergeH :: (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m)-mergeH E E = pure E-mergeH (H sz1 h1) E = pure $ H sz1 h1-mergeH E (H sz2 h2) = pure $ H sz2 h2-mergeH (H sz1 h1) (H sz2 h2) = H (sz1 + sz2) <$> merge h1 h2- instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (BH h a) (HeapOp a) where-  create = BH E E-  action (BH h1 h2) (Insert a) = (hcost @h (size h1) (Insert a),      act1 (Insert a) (BH h1 h2))-  action (BH h1 h2) SplitMin   = (hcost @h (size h2) SplitMin,        act2 SplitMin (BH h1 h2))-  action (BH h1 h2) Merge      = (hcost @h (size h1 + size h2) Merge, BH E <$> mergeH h1 h2)+  cost = hcost @h+  create = do+    h1 <- empty+    h2 <- empty+    pure $ BH (H h1) (H h2)+  perform sz (BH h1 h2) (Insert a) = do+    (sz, h1) <- perform sz h1 (Insert a)+    pure (sz, BH h1 h2)+  perform sz (BH h1 h2) SplitMin = do+    (sz, h2) <- perform sz h2 SplitMin+    pure (sz, BH h1 h2)+  perform sz (BH (H h1) (H h2)) Merge = do+    h <- merge h1 h2+    e <- empty+    pure (sz, BH (H e) (H h))

@@ -3,7 +3,7 @@ module Test.Credit.Heap.Scheduled where  import Prettyprinter (Pretty)-import Control.Monad.Credit hiding (exec)+import Control.Monad.Credit import Test.Credit import Test.Credit.Heap.Base @@ -64,10 +64,10 @@       (_, Zero) -> SCons d1 <$> mrg ds1 ds2       (One t1, One t2) -> SCons Zero <$> (insTree (link t1 t2) =<< mrg ds1 ds2))) -normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Stream m (Digit a))+normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m () normalize ds = credit 1 ds >> smatch ds-    (pure SNil)-    (\d ds -> SCons d <$> normalize ds)+    (pure ())+    (\_ ds -> normalize ds)  exec :: MonadCredit m => Schedule m a -> m (Schedule m a) exec [] = pure []@@ -119,7 +119,7 @@  instance BoundedHeap Scheduled where   hcost _ (Insert _) = 5-  hcost n Merge = 4 + 8 * log2 n+  hcost n Merge = 8 * (1 + log2 n)   hcost n SplitMin = 1 + 5 * log2 n + 6 * log2 (2 * n)  instance MemoryCell m a => MemoryCell m (Tree a) where

@@ -1,47 +1,76 @@+{-# LANGUAGE LambdaCase, GADTs #-}+ module Test.Credit.Queue.Bankers where -import Prettyprinter (Pretty) import Control.Monad.Credit+import Data.Maybe (fromMaybe)+import Prettyprinter (Pretty) import Test.Credit import Test.Credit.Queue.Base import Test.Credit.Queue.Streams  data BQueue a m = BQueue-  { front :: Stream m a-  , flen :: !Int-  , rear :: Stream m a+  { flen :: !Int   , rlen :: !Int+  , front :: Stream m a+  , rear  :: Stream m a   } -bqueue :: MonadInherit m => BQueue a m -> m (BQueue a m)-bqueue (BQueue f fl r rl) = do-  ifIndirect f (`hasAtLeast` fromIntegral rl)+allEvaluated :: MonadInherit m => StreamCell m a -> m ()+allEvaluated SNil = pure ()+allEvaluated (SCons _ xs) = isEvaluated xs++isEvaluated :: MonadInherit m => Stream m a -> m ()+isEvaluated s = lazymatch s allEvaluated (error "Stream should be pure")++allInvariant :: MonadInherit m => Maybe Int -> StreamCell m a -> m ()+allInvariant _ SNil = pure ()+allInvariant rlen (SCons x xs) = invariant xs (fmap (subtract 2) rlen)++invariant :: MonadInherit m => Stream m a -> Maybe Int -> m ()+invariant front rlen = +  lazymatch front (allInvariant rlen) $ \case+    SAppend xs ys -> do+      lxs <- slength xs+      lys <- slength ys+      front `hasAtLeast` (fromIntegral $ fromMaybe (2 * lxs) rlen)+      invariant xs Nothing+      ys `hasAtLeast` (fromIntegral $ lys - lxs)+    SReverse xs ys -> do+      lxs <- slength xs+      front `hasAtLeast` (fromIntegral lxs)+      isEvaluated xs+      isEvaluated ys++bqueue :: MonadInherit m => Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)+bqueue fl rl f r = do+  isEvaluated r+  invariant f (Just rl)   if fl >= rl -    then pure $ BQueue f fl r rl+    then pure $ BQueue fl rl f r     else do-      r' <- delay (SReverse r SNil)+      r' <- delay . SReverse r =<< nil       r' `creditWith` 1-      f' <- delay (SAppend f (SIndirect r'))-      pure $ BQueue (SIndirect f') (fl + rl) SNil 0+      BQueue (fl + rl) 0 <$> (delay $ SAppend f r') <*> nil  instance Queue BQueue where-  empty = pure $ BQueue SNil 0 SNil 0-  snoc (BQueue f fl r rl) x = do-    credit f-    bqueue (BQueue f fl (SCons x r) (rl + 1))-  uncons (BQueue f fl r rl) = do-    credit f >> credit f-    smatch f-      (\x f -> do-        q <- bqueue (BQueue f (fl - 1) r rl)-        pure $ Just (x, q))-      (pure Nothing)+  empty = BQueue 0 0 <$> nil <*> nil+  snoc (BQueue fl rl f r) x = do+    f `creditWith` 1+    bqueue fl (rl + 1) f =<< cons x r+  uncons (BQueue fl rl f r) = do+    f `creditWith` 2+    force f >>= \case+      SCons x f' -> do+        q <- bqueue (fl - 1) rl f' r+        pure $ Just (x, q)+      SNil -> pure Nothing  isEmpty :: BQueue a m -> Bool-isEmpty (BQueue _ flen _ rlen) = flen == 0 && rlen == 0+isEmpty (BQueue flen rlen _ _) = flen == 0 && rlen == 0  lazyqueue :: MonadInherit m => BQueue a m -> m [a]-lazyqueue (BQueue f fl r rl) = do+lazyqueue (BQueue fl rl f r) = do   f' <- toList f   r' <- toList r   pure $ f' ++ reverse r'@@ -51,12 +80,12 @@   qcost _ Uncons = 4  instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BQueue a m) where-  prettyCell (BQueue f fl r rl) = do-    f' <- prettyCell f+  prettyCell (BQueue fl rl f r) = do     fl' <- prettyCell fl-    r' <- prettyCell r     rl' <- prettyCell rl-    pure $ mkMCell "Queue" [f', fl', r', rl']+    f' <- prettyCell f+    r' <- prettyCell r+    pure $ mkMCell "Queue" [fl', rl', f', r']  instance Pretty a => MemoryStructure (BQueue (PrettyCell a)) where   prettyStructure = prettyCell

@@ -3,7 +3,6 @@ module Test.Credit.Queue.Base where  import Control.Monad.Credit-import Prettyprinter import Test.Credit import Test.QuickCheck @@ -17,28 +16,25 @@     ]  class Queue q where-  empty :: MonadInherit m => m (q a m)+  empty :: MonadLazy m => m (q a m)   snoc :: MonadInherit m => q a m -> a -> m (q a m)   uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))  class Queue q => BoundedQueue q where   qcost :: Size -> QueueOp a -> Credit -data Q q a m = E | Q Size (q (PrettyCell a) m)+data Q q a m = Q (q (PrettyCell a) m)  instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (Q q a) where-  prettyStructure E = pure $ mkMCell "" []-  prettyStructure (Q _ q) = prettyStructure q--act :: (MonadInherit m, Queue q) => Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)-act sz q (Snoc x) = Q (sz + 1) <$> snoc q (PrettyCell x)-act sz q Uncons = do-  m <- uncons q-  case m of-    Nothing -> pure E-    Just (_, q') -> pure $ Q (max 0 (sz - 1)) q'+  prettyStructure (Q q) = prettyStructure q  instance (Arbitrary a, BoundedQueue q, Show a) => DataStructure (Q q a) (QueueOp a) where-  create = E-  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)-  action (Q sz q) op = (qcost @q sz op, act sz q op)+  cost = qcost @q+  create = Q <$> empty+  perform sz (Q q) (Snoc x) = (sz + 1,) <$> Q <$> snoc q (PrettyCell x)+  perform sz (Q q) Uncons = do+    m <- uncons q+    q' <- case m of+      Nothing -> empty+      Just (_, q') -> pure q'+    pure (max 0 (sz - 1), Q q')

@@ -24,12 +24,10 @@   | Deep (Digit a) (Thunk m (ILazyCon m) (Implicit (a, a) m)) (Digit a)  data ILazyCon m a where-  IPure :: a -> ILazyCon m a   ISnoc :: Thunk m (ILazyCon m) (Implicit a m) -> a -> ILazyCon m (Implicit a m)   ITail :: Implicit a m -> ILazyCon m (Implicit a m)  instance MonadCredit m => HasStep (ILazyCon m) m where-  step (IPure x) = pure x   step (ISnoc t p) = do     q <- force t     snoc' q p@@ -60,7 +58,7 @@   case q of     Shallow Zero -> pure $ Shallow (One y)     Shallow (One x) -> do-      middle <- delay $ IPure $ Shallow Zero+      middle <- value $ Shallow Zero       deep (Two x y) middle Zero     Deep front middle Zero -> do       middle `creditWith` 1@@ -100,7 +98,6 @@ showThunk :: (MonadLazy m, Show a)           => Thunk m (ILazyCon m) (Implicit a m) -> m String showThunk t = lazymatch t showImplicit $ \case-    IPure a -> showImplicit a     ISnoc middle xy -> do       m <- showThunk middle       pure $ "(snoc " ++ m ++ " " ++ show xy ++ ")"@@ -143,9 +140,6 @@     pure $ mkMCell "Two" [a', b']  instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where-  prettyCell (IPure x) = do-    x' <- prettyCell x-    pure $ mkMCell "IPure" [x']   prettyCell (ISnoc t _) = do     t' <- prettyCell t     pure $ mkMCell "ISnoc" [t']

@@ -1,16 +1,12 @@-module Test.Credit.Queue.Realtime where+{-# LANGUAGE LambdaCase #-} -import Prelude hiding (lookup, reverse)+module Test.Credit.Queue.Realtime where  import Prettyprinter (Pretty) import Control.Monad.Credit import Test.Credit.Queue.Base import Test.Credit.Queue.Streams --- | Delay a computation, but do not consume any credits-indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)-indirect t = delay t >>= pure . SIndirect- data RQueue a m = RQueue   { front :: Stream m a   , rear :: Stream m a@@ -18,20 +14,31 @@   }  rqueue :: MonadInherit m => RQueue a m -> m (RQueue a m)-rqueue (RQueue f r s) = credit s >> credit s >> smatch s-  (\x s -> pure $ RQueue f r s)-  (do-    r' <- indirect (SReverse r SNil)-    f' <- indirect (SAppend f r')-    credit r' >> evalone r'-    pure $ RQueue f' SNil f')+rqueue (RQueue f r s) = do+  s `creditWith` 2+  force s >>= \case+    SCons _ s -> pure $ RQueue f r s+    SNil -> do+      r' <- delay . SReverse r =<< nil+      f' <- delay $ SAppend f r'+      r' `creditWith` 1+      n <- nil+      pure $ RQueue f' n f'  instance Queue RQueue where-  empty = pure $ RQueue SNil SNil SNil-  snoc (RQueue f r s) x = rqueue (RQueue f (SCons x r) s)-  uncons (RQueue f r s) = credit f >> credit f >> smatch f-    (\x f -> rqueue (RQueue f r s) >>= \q -> pure $ Just (x, q))-    (pure Nothing)+  empty = do+    n <- nil+    pure $ RQueue n n n+  snoc (RQueue f r s) x = do+    r' <- cons x r+    rqueue $ RQueue f r' s+  uncons (RQueue f r s) = do+    f `creditWith` 2+    force f >>= \case+      SCons x f -> do+        q <- rqueue $ RQueue f r s+        pure $ Just (x, q)+      SNil -> pure Nothing  instance BoundedQueue RQueue where   qcost _ (Snoc _) = 4

@@ -1,84 +1,55 @@ {-# LANGUAGE GADTs, LambdaCase #-} -module Test.Credit.Queue.Streams (Stream(..), SThunk, SLazyCon(..), smatch, credit, evalone, toList, ifIndirect, test) where+module Test.Credit.Queue.Streams (Stream, StreamCell(..), SLazyCon(..), cons, nil, slength, toList, test) where  import Control.Monad import Control.Monad.Credit -data Stream m a+type Stream m a = Thunk m (SLazyCon m) (StreamCell m a)++data StreamCell m a   = SCons a (Stream m a)   | SNil-  | SIndirect (SThunk m (Stream m a)) -type SThunk m = Thunk m (SLazyCon m)- data SLazyCon m a where-  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)-  SReverse :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)+  SAppend  :: Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)+  SReverse :: Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)  instance MonadInherit m => HasStep (SLazyCon m) m where-  step (SAppend xs ys) = sappend xs ys-  step (SReverse xs ys) = sreverse xs ys---- | Smart destructor for streams, consuming one credit-smatch :: MonadInherit m => Stream m a -- ^ Scrutinee-       -> (a -> Stream m a -> m b) -- ^ Cons case-       -> m b -- ^ Nil case-       -> m b-smatch x cons nil = tick >> eval x-  where-    eval x = case x of-      SCons a as -> cons a as-      SNil -> nil-      SIndirect i -> force i >>= eval---- | delay a computation, consuming all credits-taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)-taildelay t = do-  x <- delay t-  creditAllTo x-  pure (SIndirect x)--sreverse :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)-sreverse xs ys = smatch xs-  (\x xs -> taildelay (SReverse xs (SCons x ys)))-  (pure ys)--ifIndirect :: Monad m => Stream m a -> (SThunk m (Stream m a) -> m ()) -> m ()-ifIndirect (SIndirect i) f = f i-ifIndirect _ _ = pure ()--credit :: MonadInherit m => Stream m a -> m ()-credit s = ifIndirect s (`creditWith` 1)+  step (SAppend  xs ys) = force =<< sappend  xs ys +  step (SReverse xs ys) = force =<< sreverse xs ys -evalone :: MonadInherit m => Stream m a -> m ()-evalone s = ifIndirect s (void . force)+cons :: MonadLazy m => a -> Stream m a -> m (Stream m a)+cons x xs = value $ SCons x xs -sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)-sappend xs ys = credit ys >> evalone ys >> smatch xs-  (\x xs -> SCons x <$> taildelay (SAppend xs ys))-  (pure ys)+nil :: MonadLazy m => m (Stream m a)+nil = value SNil -walk s = smatch s (\_ xs -> walk xs) (pure ())+sreverse :: MonadInherit m+          => Stream m a -> Stream m a -> m (Stream m a)+sreverse xs ys = tick >> force xs >>= \case+  SCons x xs -> sreverse xs =<< cons x ys+  SNil -> pure ys -foo :: MonadInherit m => Stream m a -> m ()-foo s = smatch s (\_ _ -> pure ()) (pure ())+sappend :: MonadInherit m+         => Stream m a -> Stream m a -> m (Stream m a)+sappend xs ys = do+  tick+  ys `creditWith` 1+  force xs >>= \case+    SCons x xs' -> do+      xs'ys <- delay $ SAppend xs' ys+      creditAllTo xs'ys+      cons x xs'ys+    SNil -> creditAllTo ys >> pure ys -test :: MonadInherit m => m ()-test = do-  s <- sappend (SCons 1 SNil) (SCons 2 SNil)-  credit s >> credit s-  foo s-  credit s-  walk s+cellToList :: MonadLazy m => StreamCell m a -> m [a]+cellToList SNil = pure []+cellToList (SCons x xs) = (x :) <$> toList xs  toList :: MonadLazy m => Stream m a -> m [a]-toList SNil = pure []-toList (SCons x xs) = do-  xs' <- toList xs-  pure $ x : xs'-toList (SIndirect t) = do-  lazymatch t toList $ \case+toList t = do+  lazymatch t cellToList $ \case       SAppend xs ys -> do         xs' <- toList xs         ys' <- toList ys@@ -88,6 +59,28 @@         ys' <- toList ys         pure $ reverse xs' ++ ys' +slength :: MonadLazy m => Stream m a -> m Int+slength s = length <$> toList s++walk :: MonadInherit m => Stream m a -> m ()+walk s = force s >>= \case+  SCons _ xs -> walk xs+  SNil -> pure ()++foo :: MonadInherit m => Stream m a -> m ()+foo s = void $ force s++test :: MonadInherit m => m ()+test = do+  nil <- value SNil+  one <- value (SCons 1 nil)+  two <- value (SCons 2 nil)+  s <- sappend one two+  creditWith s 2+  foo s+  creditWith s 1+  walk s+ instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where   prettyCell (SAppend xs ys) = do     xs' <- prettyCell xs@@ -98,13 +91,11 @@     ys' <- prettyCell ys     pure $ mkMCell "SReverse" [xs', ys'] -instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (StreamCell m a) where   prettyCell xs = mkMList <$> toList xs <*> toHole xs     where       toList SNil = pure $ []-      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs-      toList (SIndirect t) = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> lazymatch xs toList (\_ -> pure [])        toHole SNil = pure $ Nothing-      toHole (SCons x xs) = toHole xs-      toHole (SIndirect t) = Just <$> prettyCell t+      toHole (SCons x xs) = lazymatch xs toHole (\_ -> Just <$> prettyCell xs)

@@ -19,7 +19,7 @@     ]  class RandomAccess q where-  empty :: MonadCredit m => m (q a m)+  empty :: MonadLazy m => m (q a m)   cons :: MonadCredit m => a -> q a m  -> m (q a m)   uncons :: MonadCredit m => q a m -> m (Maybe (a, q a m))   lookup :: MonadCredit m => Int -> q a m -> m (Maybe a)@@ -28,15 +28,13 @@ class RandomAccess q => BoundedRandomAccess q where   qcost :: Size -> RandomAccessOp a -> Credit -data RA q a m = E | RA Size (q (PrettyCell a) m)+data RA q a m = RA (q (PrettyCell a) m)  instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (RA q a m) where-  prettyCell E = pure $ mkMCell "" []-  prettyCell (RA _ q) = prettyCell q+  prettyCell (RA q) = prettyCell q  instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (RA q a) where-  prettyStructure E = pure $ mkMCell "" []-  prettyStructure (RA _ q) = prettyStructure q+  prettyStructure (RA q) = prettyStructure q  idx :: Int -> Size -> Int idx i sz = if sz <= 0 then 0 else abs (i `mod` fromIntegral sz)@@ -46,19 +44,17 @@ norm sz (Update i a) = Update (idx i sz) a norm _ op = op -act :: (MonadCredit m, RandomAccess q) => Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)-act sz q (Cons x) = RA (sz + 1) <$> cons (PrettyCell x) q-act sz q Uncons = do-  m <- uncons q-  case m of-    Nothing -> pure E-    Just (_, q') -> pure $ RA (max 0 (sz - 1)) q'-act sz q (Lookup i) = do-  _ <- lookup i q-  pure $ RA sz q-act sz q (Update i a) = RA sz <$> update i (PrettyCell a) q- instance (Arbitrary a, BoundedRandomAccess q, Show a) => DataStructure (RA q a) (RandomAccessOp a) where-  create = E-  action E op = (qcost @q 0 (norm 0 op), empty >>= flip (act 0) (norm 0 op))-  action (RA sz q) op = (qcost @q sz (norm sz op), act sz q (norm sz op))+  cost sz op = qcost @q sz (norm sz op)+  create = RA <$> empty+  perform sz (RA q) (Cons x) = (sz + 1,) <$> RA <$> cons (PrettyCell x) q+  perform sz (RA q) Uncons = do+    m <- uncons q+    m' <- case m of+      Nothing -> empty+      Just (_, q') -> pure q'+    pure (max 0 (sz - 1), RA m')+  perform sz (RA q) (Lookup i) = do+    _ <- lookup (idx i sz) q+    pure $ (sz, RA q)+  perform sz (RA q) (Update i a) = (sz,) <$> RA <$> update (idx i sz) (PrettyCell a) q

@@ -4,7 +4,7 @@  import Prelude hiding (lookup) import Prettyprinter (Pretty)-import Control.Monad.Credit hiding (exec)+import Control.Monad.Credit import Test.Credit import Test.Credit.RandomAccess.Base 

@@ -4,7 +4,7 @@  import Prelude hiding (lookup) import Prettyprinter (Pretty)-import Control.Monad.Credit hiding (exec)+import Control.Monad.Credit import Test.Credit import Test.Credit.RandomAccess.Base 

@@ -16,30 +16,25 @@     ]  class Sortable q where-  empty :: MonadCredit m => m (q a m)+  empty :: MonadLazy m => m (q a m)   add :: MonadCredit m => Ord a => a -> q a m -> m (q a m)   sort :: MonadCredit m => Ord a => q a m -> m [a]   class Sortable q => BoundedSortable q where   scost :: Size -> SortableOp a -> Credit -data S q a m = E | S Size (q (PrettyCell a) m)+data S q a m = S (q (PrettyCell a) m)  instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (S q a m) where-  prettyCell E = pure $ mkMCell "" []-  prettyCell (S _ q) = prettyCell q+  prettyCell (S q) = prettyCell q  instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (S q a) where-  prettyStructure E = pure $ mkMCell "" []-  prettyStructure (S sz q) = prettyStructure q--act :: (MonadCredit m, Sortable q, Ord a) => Size -> q (PrettyCell a) m -> SortableOp a -> m (S q a m)-act sz q (Add x) = S (sz + 1) <$> add (PrettyCell x) q-act sz q Sort = do-  xs <- sort q-  pure $ S sz q+  prettyStructure (S q) = prettyStructure q  instance (Arbitrary a, Ord a, BoundedSortable q, Show a) => DataStructure (S q a) (SortableOp a) where-  create = E-  action E op = (scost @q 0 op, empty >>= flip (act 0) op)-  action (S sz q) op = (scost @q sz op, act sz q op)+  cost = scost @q+  create = S <$> empty+  perform sz (S q) (Add x) = (sz + 1,) <$> S <$> add (PrettyCell x) q+  perform sz (S q) Sort = do+    _ <- sort q+    pure (sz, S q)