{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}

module Test.Credit.RandomAccess.Base where

import Prelude hiding (lookup)
import Control.Monad.Credit
import Test.Credit
import Test.QuickCheck

data RandomAccessOp a = Cons a | Uncons | Lookup Int | Update Int a
  deriving (RandomAccessOp a -> RandomAccessOp a -> Bool
(RandomAccessOp a -> RandomAccessOp a -> Bool)
-> (RandomAccessOp a -> RandomAccessOp a -> Bool)
-> Eq (RandomAccessOp a)
forall a. Eq a => RandomAccessOp a -> RandomAccessOp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RandomAccessOp a -> RandomAccessOp a -> Bool
== :: RandomAccessOp a -> RandomAccessOp a -> Bool
$c/= :: forall a. Eq a => RandomAccessOp a -> RandomAccessOp a -> Bool
/= :: RandomAccessOp a -> RandomAccessOp a -> Bool
Eq, Eq (RandomAccessOp a)
Eq (RandomAccessOp a) =>
(RandomAccessOp a -> RandomAccessOp a -> Ordering)
-> (RandomAccessOp a -> RandomAccessOp a -> Bool)
-> (RandomAccessOp a -> RandomAccessOp a -> Bool)
-> (RandomAccessOp a -> RandomAccessOp a -> Bool)
-> (RandomAccessOp a -> RandomAccessOp a -> Bool)
-> (RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a)
-> (RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a)
-> Ord (RandomAccessOp a)
RandomAccessOp a -> RandomAccessOp a -> Bool
RandomAccessOp a -> RandomAccessOp a -> Ordering
RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (RandomAccessOp a)
forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Bool
forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Ordering
forall a.
Ord a =>
RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
$ccompare :: forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Ordering
compare :: RandomAccessOp a -> RandomAccessOp a -> Ordering
$c< :: forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Bool
< :: RandomAccessOp a -> RandomAccessOp a -> Bool
$c<= :: forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Bool
<= :: RandomAccessOp a -> RandomAccessOp a -> Bool
$c> :: forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Bool
> :: RandomAccessOp a -> RandomAccessOp a -> Bool
$c>= :: forall a. Ord a => RandomAccessOp a -> RandomAccessOp a -> Bool
>= :: RandomAccessOp a -> RandomAccessOp a -> Bool
$cmax :: forall a.
Ord a =>
RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
max :: RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
$cmin :: forall a.
Ord a =>
RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
min :: RandomAccessOp a -> RandomAccessOp a -> RandomAccessOp a
Ord, Int -> RandomAccessOp a -> ShowS
[RandomAccessOp a] -> ShowS
RandomAccessOp a -> String
(Int -> RandomAccessOp a -> ShowS)
-> (RandomAccessOp a -> String)
-> ([RandomAccessOp a] -> ShowS)
-> Show (RandomAccessOp a)
forall a. Show a => Int -> RandomAccessOp a -> ShowS
forall a. Show a => [RandomAccessOp a] -> ShowS
forall a. Show a => RandomAccessOp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RandomAccessOp a -> ShowS
showsPrec :: Int -> RandomAccessOp a -> ShowS
$cshow :: forall a. Show a => RandomAccessOp a -> String
show :: RandomAccessOp a -> String
$cshowList :: forall a. Show a => [RandomAccessOp a] -> ShowS
showList :: [RandomAccessOp a] -> ShowS
Show)

instance Arbitrary a => Arbitrary (RandomAccessOp a) where
  arbitrary :: Gen (RandomAccessOp a)
arbitrary = [(Int, Gen (RandomAccessOp a))] -> Gen (RandomAccessOp a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
13, a -> RandomAccessOp a
forall a. a -> RandomAccessOp a
Cons (a -> RandomAccessOp a) -> Gen a -> Gen (RandomAccessOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary)
    , (Int
6, RandomAccessOp a -> Gen (RandomAccessOp a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RandomAccessOp a
forall a. RandomAccessOp a
Uncons)
    , (Int
1, Int -> RandomAccessOp a
forall a. Int -> RandomAccessOp a
Lookup (Int -> RandomAccessOp a) -> Gen Int -> Gen (RandomAccessOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary)
    , (Int
1, Int -> a -> RandomAccessOp a
forall a. Int -> a -> RandomAccessOp a
Update (Int -> a -> RandomAccessOp a)
-> Gen Int -> Gen (a -> RandomAccessOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary Gen (a -> RandomAccessOp a) -> Gen a -> Gen (RandomAccessOp a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen a
forall a. Arbitrary a => Gen a
arbitrary)
    ]

class RandomAccess q where
  empty :: MonadCredit 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)
  update :: MonadCredit m => Int -> a -> q a m -> m (q a m)

class RandomAccess q => BoundedRandomAccess q where
  qcost :: Size -> RandomAccessOp a -> Credit

data RA q a m = E | RA Size (q (PrettyCell a) m)

instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (RA q a m) where
  prettyCell :: RA q a m -> m Memory
prettyCell RA q a m
E = Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"" []
  prettyCell (RA Size
_ q (PrettyCell a) m
q) = q (PrettyCell a) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell q (PrettyCell a) m
q

instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (RA q a) where
  prettyStructure :: forall (m :: * -> *). MonadMemory m => RA q a m -> m Memory
prettyStructure RA q a m
E = Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"" []
  prettyStructure (RA Size
_ q (PrettyCell a) m
q) = q (PrettyCell a) m -> m Memory
forall (m :: * -> *).
MonadMemory m =>
q (PrettyCell a) m -> m Memory
forall (t :: (* -> *) -> *) (m :: * -> *).
(MemoryStructure t, MonadMemory m) =>
t m -> m Memory
prettyStructure q (PrettyCell a) m
q

idx :: Int -> Size -> Int
idx :: Int -> Size -> Int
idx Int
i Size
sz = if Size
sz Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
<= Size
0 then Int
0 else Int -> Int
forall a. Num a => a -> a
abs (Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
sz)

norm :: Size -> RandomAccessOp a -> RandomAccessOp a
norm :: forall a. Size -> RandomAccessOp a -> RandomAccessOp a
norm Size
sz (Lookup Int
i) = Int -> RandomAccessOp a
forall a. Int -> RandomAccessOp a
Lookup (Int -> Size -> Int
idx Int
i Size
sz)
norm Size
sz (Update Int
i a
a) = Int -> a -> RandomAccessOp a
forall a. Int -> a -> RandomAccessOp a
Update (Int -> Size -> Int
idx Int
i Size
sz) a
a
norm Size
_ RandomAccessOp a
op = RandomAccessOp a
op

act :: (MonadCredit m, RandomAccess q) => Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
act :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadCredit m, RandomAccess q) =>
Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
act Size
sz q (PrettyCell a) m
q (Cons a
x) = Size -> q (PrettyCell a) m -> RA q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> RA q a m
RA (Size
sz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) (q (PrettyCell a) m -> RA q a m)
-> m (q (PrettyCell a) m) -> m (RA q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrettyCell a -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadCredit m => a -> q a m -> m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(RandomAccess q, MonadCredit m) =>
a -> q a m -> m (q a m)
cons (a -> PrettyCell a
forall a. a -> PrettyCell a
PrettyCell a
x) q (PrettyCell a) m
q
act Size
sz q (PrettyCell a) m
q RandomAccessOp a
Uncons = do
  Maybe (PrettyCell a, q (PrettyCell a) m)
m <- q (PrettyCell a) m -> m (Maybe (PrettyCell a, q (PrettyCell a) m))
forall (m :: * -> *) a.
MonadCredit m =>
q a m -> m (Maybe (a, q a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(RandomAccess q, MonadCredit m) =>
q a m -> m (Maybe (a, q a m))
uncons q (PrettyCell a) m
q
  case Maybe (PrettyCell a, q (PrettyCell a) m)
m of
    Maybe (PrettyCell a, q (PrettyCell a) m)
Nothing -> RA q a m -> m (RA q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RA q a m
forall {k} (q :: * -> k -> *) a (m :: k). RA q a m
E
    Just (PrettyCell a
_, q (PrettyCell a) m
q') -> RA q a m -> m (RA q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RA q a m -> m (RA q a m)) -> RA q a m -> m (RA q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> RA q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> RA q a m
RA (Size -> Size -> Size
forall a. Ord a => a -> a -> a
max Size
0 (Size
sz Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1)) q (PrettyCell a) m
q'
act Size
sz q (PrettyCell a) m
q (Lookup Int
i) = do
  Maybe (PrettyCell a)
_ <- Int -> q (PrettyCell a) m -> m (Maybe (PrettyCell a))
forall (m :: * -> *) a.
MonadCredit m =>
Int -> q a m -> m (Maybe a)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(RandomAccess q, MonadCredit m) =>
Int -> q a m -> m (Maybe a)
lookup Int
i q (PrettyCell a) m
q
  RA q a m -> m (RA q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RA q a m -> m (RA q a m)) -> RA q a m -> m (RA q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> RA q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> RA q a m
RA Size
sz q (PrettyCell a) m
q
act Size
sz q (PrettyCell a) m
q (Update Int
i a
a) = Size -> q (PrettyCell a) m -> RA q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> RA q a m
RA Size
sz (q (PrettyCell a) m -> RA q a m)
-> m (q (PrettyCell a) m) -> m (RA q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> PrettyCell a -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall (m :: * -> *) a.
MonadCredit m =>
Int -> a -> q a m -> m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(RandomAccess q, MonadCredit m) =>
Int -> a -> q a m -> m (q a m)
update Int
i (a -> PrettyCell a
forall a. a -> PrettyCell a
PrettyCell a
a) q (PrettyCell a) m
q

instance (Arbitrary a, BoundedRandomAccess q, Show a) => DataStructure (RA q a) (RandomAccessOp a) where
  create :: forall (m :: * -> *). MonadInherit m => RA q a m
create = RA q a m
forall {k} (q :: * -> k -> *) a (m :: k). RA q a m
E
  action :: forall (m :: * -> *).
MonadInherit m =>
RA q a m -> RandomAccessOp a -> (Credit, m (RA q a m))
action RA q a m
E RandomAccessOp a
op = (forall (q :: * -> (* -> *) -> *) a.
BoundedRandomAccess q =>
Size -> RandomAccessOp a -> Credit
qcost @q Size
0 (Size -> RandomAccessOp a -> RandomAccessOp a
forall a. Size -> RandomAccessOp a -> RandomAccessOp a
norm Size
0 RandomAccessOp a
op), m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadCredit m => m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(RandomAccess q, MonadCredit m) =>
m (q a m)
empty m (q (PrettyCell a) m)
-> (q (PrettyCell a) m -> m (RA q a m)) -> m (RA q a m)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m))
-> RandomAccessOp a -> q (PrettyCell a) m -> m (RA q a m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadCredit m, RandomAccess q) =>
Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
act Size
0) (Size -> RandomAccessOp a -> RandomAccessOp a
forall a. Size -> RandomAccessOp a -> RandomAccessOp a
norm Size
0 RandomAccessOp a
op))
  action (RA Size
sz q (PrettyCell a) m
q) RandomAccessOp a
op = (forall (q :: * -> (* -> *) -> *) a.
BoundedRandomAccess q =>
Size -> RandomAccessOp a -> Credit
qcost @q Size
sz (Size -> RandomAccessOp a -> RandomAccessOp a
forall a. Size -> RandomAccessOp a -> RandomAccessOp a
norm Size
sz RandomAccessOp a
op), Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadCredit m, RandomAccess q) =>
Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
act Size
sz q (PrettyCell a) m
q (Size -> RandomAccessOp a -> RandomAccessOp a
forall a. Size -> RandomAccessOp a -> RandomAccessOp a
norm Size
sz RandomAccessOp a
op))