--
-- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
-- Martin A.T. Handley, Niki Vazou, and Graham Hutton.
--

{-@ LIQUID "--reflection" @-}

module Language.Haskell.Liquid.RTick
  (

  -- Tick datatype:
    Tick(..)
  -- Primitive resource operators:
  , fmap
  , pure
  , (<*>)
  , liftA2
  , return
  , (>>=)
  , (=<<)
  , eqBind
  , leqBind
  , geqBind
  , ap
  , liftM
  , liftM2
  -- Resource modifiers:
  , step
  , wait      -- step 1       . return
  , waitN     -- step (n > 0) . return
  , go        -- step (-1)    . return
  , goN       -- step (n < 0) . return
  , wmap      -- step 1       . fmap f
  , wmapN     -- step (n > 0) . fmap f
  , gmap      -- step (-1)    . fmap f
  , gmapN     -- step (n < 0) . fmap f
  , (</>)     -- step 1       . (f <*>)
  , (<//>)    -- step 2       . (f <*>)
  , (<\>)     -- step (-1)    . (f <*>)
  , (<\\>)    -- step (-2)    . (f <*>)
  , (>/=)     -- step 1       . (>>= f)
  , (=/<)     -- step 1       . (>>= f)
  , (>//=)    -- step 2       . (>>= f)
  , (=//<)    -- step 2       . (>>= f)
  , (>\=)     -- step (-1)    . (>>= f)
  , (=\<)     -- step (-1)    . (>>= f)
  , (>\\=)    -- step (-2)    . (>>= f)
  , (=\\<)    -- step (-2)    . (>>= f)
  -- Memoisation:
  , pay
  , zipWithM


  ) where

import Prelude hiding ( Functor(..), Applicative(..), Monad(..), (=<<) )

import qualified Control.Applicative as A
import qualified Control.Monad       as M
import qualified Data.Functor        as F

--
-- The 'Tick' datatype and its corresponding resource modifiers.
--
-- See 'ResourceModifiers.hs' for proofs that all resource modifiers
-- can be defined using 'return', '(>>=) 'and 'step'.
--

-------------------------------------------------------------------------------
-- | 'Tick' datatype for recording resource usage:
-------------------------------------------------------------------------------

{-@ data Tick a = Tick { tcost :: Int, tval :: a } @-}
data Tick a = Tick { Tick a -> Int
tcost :: Int, Tick a -> a
tval :: a }

-------------------------------------------------------------------------------
-- | Primitive resource operators:
-------------------------------------------------------------------------------

instance F.Functor Tick where
  fmap :: (a -> b) -> Tick a -> Tick b
fmap = (a -> b) -> Tick a -> Tick b
forall a b. (a -> b) -> Tick a -> Tick b
fmap

{-@ reflect fmap @-}
{-@ fmap :: f:(a -> b) -> t1:Tick a
      -> { t:Tick b | Tick (tcost t1) (f (tval t1)) == t }
@-}
fmap :: (a -> b) -> Tick a -> Tick b
fmap :: (a -> b) -> Tick a -> Tick b
fmap a -> b
f (Tick Int
m a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick Int
m (a -> b
f a
x)

instance A.Applicative Tick where
  pure :: a -> Tick a
pure  = a -> Tick a
forall a. a -> Tick a
pure
  <*> :: Tick (a -> b) -> Tick a -> Tick b
(<*>) = Tick (a -> b) -> Tick a -> Tick b
forall a b. Tick (a -> b) -> Tick a -> Tick b
(<*>)

{-@ reflect pure @-}
{-@ pure :: x:a -> { t:Tick a | x == tval t && 0 == tcost t } @-}
pure :: a -> Tick a
pure :: a -> Tick a
pure a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick Int
0 a
x

{-@ reflect <*> @-}
{-@ (<*>) :: t1:Tick (a -> b) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                    tcost t1 + tcost t2 == tcost t }
@-}
infixl 4 <*>
(<*>) :: Tick (a -> b) -> Tick a -> Tick b
Tick Int
m a -> b
f <*> :: Tick (a -> b) -> Tick a -> Tick b
<*> Tick Int
n a
x = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b
f a
x)

{-@ reflect liftA2 @-}
{-@ liftA2 :: f:(a -> b -> c) -> t1:Tick a -> t2:Tick b
      -> { t:Tick c | f (tval t1) (tval t2) == tval  t &&
                      tcost t1 + tcost t2 == tcost t }
@-}
liftA2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c
liftA2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c
liftA2 a -> b -> c
f (Tick Int
m a
x) (Tick Int
n b
y) = Int -> c -> Tick c
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b -> c
f a
x b
y)

instance M.Monad Tick where
  return :: a -> Tick a
return = a -> Tick a
forall a. a -> Tick a
return
  >>= :: Tick a -> (a -> Tick b) -> Tick b
(>>=)  = Tick a -> (a -> Tick b) -> Tick b
forall a b. Tick a -> (a -> Tick b) -> Tick b
(>>=)

{-@ reflect return @-}
{-@ return :: x:a -> { t:Tick a | x == tval t && 0 == tcost t } @-}
return :: a -> Tick a
return :: a -> Tick a
return a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick Int
0 a
x

{-@ reflect >>= @-}
{-@ (>>=) :: t1:Tick a -> f:(a -> Tick b)
      -> { t:Tick b | tval (f (tval t1))  == tval  t &&
         tcost t1 + tcost (f (tval t1)) == tcost t }
@-}
infixl 4 >>=
(>>=) :: Tick a -> (a -> Tick b) -> Tick b
Tick Int
m a
x >>= :: Tick a -> (a -> Tick b) -> Tick b
>>= a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

{-@ reflect =<< @-}
{-@ (=<<) :: f:(a -> Tick b) -> t1:Tick a
      -> { t:Tick b | tval (f (tval t1))  == tval  t &&
         tcost t1 + tcost (f (tval t1)) == tcost t }
@-}
infixl 4 =<<
(=<<) :: (a -> Tick b) -> Tick a -> Tick b
a -> Tick b
f =<< :: (a -> Tick b) -> Tick a -> Tick b
=<< Tick Int
m a
x = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

{-@ reflect ap @-}
{-@ ap :: t1:(Tick (a -> b)) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                    tcost t1 + tcost t2 == tcost t }
@-}
ap :: Tick (a -> b) -> Tick a -> Tick b
ap :: Tick (a -> b) -> Tick a -> Tick b
ap (Tick Int
m a -> b
f) (Tick Int
n a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b
f a
x)

{-@ reflect liftM @-}
{-@ liftM :: f:(a -> b) -> t1:Tick a -> { t:Tick b | tcost t1 == tcost t } @-}
liftM :: (a -> b) -> Tick a -> Tick b
liftM :: (a -> b) -> Tick a -> Tick b
liftM a -> b
f (Tick Int
m a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick Int
m (a -> b
f a
x)

{-@ reflect liftM2 @-}
{-@ liftM2 :: f:(a -> b -> c) -> t1:Tick a -> t2:Tick b
      -> { t:Tick c | f (tval t1) (tval t2) == tval  t &&
                      tcost t1 + tcost t2 == tcost t }
@-}
liftM2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c
liftM2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c
liftM2 a -> b -> c
f (Tick Int
m a
x) (Tick Int
n b
y) = Int -> c -> Tick c
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b -> c
f a
x b
y)

-------------------------------------------------------------------------------

{-@ reflect eqBind @-}
{-@ eqBind :: n:Int -> t1:Tick a
      -> f:(a -> { tf:Tick b | n == tcost tf })
      -> { t:Tick b | tval (f (tval t1))  == tval  t &&
                           tcost t1 + n == tcost t }
@-}
eqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
eqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
eqBind Int
_ (Tick Int
m a
x) a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

{-@ reflect leqBind @-}
{-@ leqBind :: n:Int -> t1:Tick a
      -> f:(a -> { tf:Tick b | n >= tcost tf })
      -> { t:Tick b | tcost t1 + n >= tcost t }
@-}
leqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
leqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
leqBind Int
_ (Tick Int
m a
x) a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

{-@ reflect geqBind @-}
{-@ geqBind :: n:Int -> t1:Tick a
      -> f:(a -> { tf:Tick b | n <= tcost tf })
      -> { t2:Tick b | tcost t1 + n <= tcost t2 }
@-}
geqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
geqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
geqBind Int
_ (Tick Int
m a
x) a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

-------------------------------------------------------------------------------
-- | Resource modifiers:
-------------------------------------------------------------------------------

{-@ reflect step @-}
{-@ step :: m:Int -> t1:Tick a
      -> { t:Tick a | tval t1 == tval t && m + tcost t1 == tcost t }
@-}
step :: Int -> Tick a -> Tick a
step :: Int -> Tick a -> Tick a
step Int
m (Tick Int
n a
x) = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) a
x

--
-- @wait := step 1 . return@.
--
{-@ reflect wait @-}
{-@ wait :: x:a -> { t:Tick a | x == tval t && 1 == tcost t } @-}
wait :: a -> Tick a
wait :: a -> Tick a
wait a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick Int
1 a
x

--
-- @waitN (n > 0) := step n . return@.
--
{-@ reflect waitN @-}
{-@ waitN :: n:Nat -> x:a
      -> { t:Tick a | x == tval t && n == tcost t }
@-}
waitN :: Int -> a -> Tick a
waitN :: Int -> a -> Tick a
waitN Int
n a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick Int
n a
x

--
-- @go := step (-1) . return@.
--
{-@ reflect go @-}
{-@ go :: x:a -> { t:Tick a | x == tval t && (-1) == tcost t } @-}
go :: a -> Tick a
go :: a -> Tick a
go a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick (-Int
1) a
x

--
-- @goN (n > 0) := step (-n) . return@.
--
{-@ reflect goN @-}
{-@ goN :: { n:Nat | n > 0 } -> x:a
      -> { t:Tick a | x == tval t && (-n) == tcost t }
@-}
goN :: Int -> a -> Tick a
goN :: Int -> a -> Tick a
goN Int
n a
x = Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick (-Int
n) a
x

--
-- @wmap f := step 1 . fmap f@.
--
{-@ reflect wmap @-}
{-@ wmap :: f:(a -> b) -> t1:Tick a
      -> { t:Tick b | Tick (1 + tcost t1) (f (tval t1)) == t }
@-}
wmap :: (a -> b) -> Tick a -> Tick b
wmap :: (a -> b) -> Tick a -> Tick b
wmap a -> b
f (Tick Int
m a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) (a -> b
f a
x)

--
-- @wmapN (n > 0) f := step n . fmap f@.
--
{-@ reflect wmapN @-}
{-@ wmapN :: { m:Nat | m > 0 } -> f:(a -> b) -> t1:Tick a
      -> { t:Tick b | Tick (m + tcost t1) (f (tval t1)) == t }
@-}
wmapN :: Int -> (a -> b) -> Tick a -> Tick b
wmapN :: Int -> (a -> b) -> Tick a -> Tick b
wmapN Int
m a -> b
f (Tick Int
n a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b
f a
x)

--
-- @gmap f := step (-1) . fmap f@.
--
{-@ reflect gmap @-}
{-@ gmap :: f:(a -> b) -> t1:Tick a
      -> { t:Tick b | Tick (tcost t1 - 1) (f (tval t1)) == t }
@-}
gmap :: (a -> b) -> Tick a -> Tick b
gmap :: (a -> b) -> Tick a -> Tick b
gmap a -> b
f (Tick Int
m a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (a -> b
f a
x)

--
-- @gmapN (n > 0) f := step (-n) . fmap f@.
--
{-@ reflect gmapN @-}
{-@ gmapN :: { m:Nat | m > 0 } -> f:(a -> b) -> t1:Tick a
      -> { t:Tick b | Tick (tcost t1 - m) (f (tval t1)) == t }
@-}
gmapN :: Int -> (a -> b) -> Tick a -> Tick b
gmapN :: Int -> (a -> b) -> Tick a -> Tick b
gmapN Int
m a -> b
f (Tick Int
n a
x) = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) (a -> b
f a
x)

--
-- \"wapp\": @(f </>) := step 1 . (f <*>)@.
--
{-@ reflect </> @-}
{-@ (</>) :: t1:(Tick (a -> b)) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                1 + tcost t1 + tcost t2 == tcost t }
@-}
infixl 4 </>
(</>) :: Tick (a -> b) -> Tick a -> Tick b
Tick Int
m a -> b
f </> :: Tick (a -> b) -> Tick a -> Tick b
</> Tick Int
n a
x = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b
f a
x)

--
-- \"wwapp\": @(f <//>) := step 2 . (f <*>)@.
--
{-@ reflect <//> @-}
{-@ (<//>) :: t1:(Tick (a -> b)) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                2 + tcost t1 + tcost t2 == tcost t }
@-}
infixl 4 <//>
(<//>) :: Tick (a -> b) -> Tick a -> Tick b
Tick Int
m a -> b
f <//> :: Tick (a -> b) -> Tick a -> Tick b
<//> Tick Int
n a
x = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (a -> b
f a
x)

--
-- \"gapp\": @(f <\>) := step (-1) . (f <*>)@.
--
{-@ reflect <\> @-}
{-@ (<\>) :: t1:(Tick (a -> b)) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                tcost t1 + tcost t2 - 1 == tcost t }
@-}
infixl 4 <\>
(<\>) :: Tick (a -> b) -> Tick a -> Tick b
Tick Int
m a -> b
f <\> :: Tick (a -> b) -> Tick a -> Tick b
<\> Tick Int
n a
x = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (a -> b
f a
x)

--
-- \"ggapp\": @(f <\\>) := step (-2) . (f <*>)@.
--
{-@ reflect <\\> @-}
{-@ (<\\>) :: t1:(Tick (a -> b)) -> t2:Tick a
      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&
                tcost t1 + tcost t2 - 2 == tcost t }
@-}
infixl 4 <\\>
(<\\>) :: Tick (a -> b) -> Tick a -> Tick b
Tick Int
m a -> b
f <\\> :: Tick (a -> b) -> Tick a -> Tick b
<\\> Tick Int
n a
x = Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) (a -> b
f a
x)

--
-- \"wbind\": @(>/= f) := step 1 . (>>= f)@.
--
{-@ reflect >/= @-}
{-@ (>/=) :: t1:Tick a -> f:(a -> Tick b)
      -> { t:Tick b | (tval (f (tval t1))      == tval  t) &&
         (1 + tcost t1 + tcost (f (tval t1))) == tcost t }
@-}
infixl 4 >/=
(>/=) :: Tick a -> (a -> Tick b) -> Tick b
Tick Int
m a
x >/= :: Tick a -> (a -> Tick b) -> Tick b
>/= a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

--
-- \"wbind\": @(f =/<) := step 1 . (f =<<)@.
--
{-@ reflect =/< @-}
{-@ (=/<) :: f:(a -> Tick b) -> t1:Tick a
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         1 + tcost t1 + tcost (f (tval t1)) == tcost t }
@-}
infixl 4 =/<
(=/<) :: (a -> Tick b) -> Tick a -> Tick b
a -> Tick b
f =/< :: (a -> Tick b) -> Tick a -> Tick b
=/< Tick Int
m a
x = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

--
-- \"wwbind\": @(>//= f) := step 2 . (>>= f)@.
--
{-@ reflect >//= @-}
{-@ (>//=) :: t1:Tick a -> f:(a -> Tick b)
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         2 + tcost t1 + tcost (f (tval t1)) == tcost t }
@-}
infixl 4 >//=
(>//=) :: Tick a -> (a -> Tick b) -> Tick b
Tick Int
m a
x >//= :: Tick a -> (a -> Tick b) -> Tick b
>//= a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

--
-- \"wwbind\": @(f =//<) := step 2 . (f =<<)@.
--
{-@ reflect =//< @-}
{-@ (=//<) :: f:(a -> Tick b) -> t1:Tick a
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         2 + tcost t1 + tcost (f (tval t1)) == tcost t }
@-}
infixl 4 =//<
(=//<) :: (a -> Tick b) -> Tick a -> Tick b
a -> Tick b
f =//< :: (a -> Tick b) -> Tick a -> Tick b
=//< Tick Int
m a
x = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) b
y

--
-- \"gbind\": @(>\= f) := step (-1) . (>>= f)@.
--
{-@ reflect >\= @-}
{-@ (>\=) :: t1:Tick a -> f:(a -> Tick b)
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         tcost t1 + tcost (f (tval t1)) - 1 == tcost t }
@-}
infixl 4 >\=
(>\=) :: Tick a -> (a -> Tick b) -> Tick b
Tick Int
m a
x >\= :: Tick a -> (a -> Tick b) -> Tick b
>\= a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) b
y

--
-- \"gbind\": @(f =\<) := step (-1) . (f =<<)@.
--
{-@ reflect =\< @-}
{-@ (=\<) :: f:(a -> Tick b) -> t1:Tick a
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         tcost t1 + tcost (f (tval t1)) - 1 == tcost t }
@-}
infixl 4 =\<
(=\<) :: (a -> Tick b) -> Tick a -> Tick b
a -> Tick b
f =\< :: (a -> Tick b) -> Tick a -> Tick b
=\< Tick Int
m a
x = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) b
y

--
-- \"ggbind\": @(>\= f) := step (-2) . (>>= f)@.
--
{-@ reflect >\\= @-}
{-@ (>\\=) :: t1:Tick a -> f:(a -> Tick b)
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         tcost t1 + tcost (f (tval t1)) - 2 == tcost t }
@-}
infixl 4 >\\=
(>\\=) :: Tick a -> (a -> Tick b) -> Tick b
Tick Int
m a
x >\\= :: Tick a -> (a -> Tick b) -> Tick b
>\\= a -> Tick b
f = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) b
y

--
-- \"ggbind\": @(f =\\<) := step (-2) . (f =<<)@.
--
{-@ reflect =\\< @-}
{-@ (=\\<) :: f:(a -> Tick b) -> t1:Tick a
      -> { t:Tick b | tval (f (tval t1))      == tval  t &&
         tcost t1 + tcost (f (tval t1)) - 2 == tcost t }
@-}
infixl 4 =\\<
(=\\<) :: (a -> Tick b) -> Tick a -> Tick b
a -> Tick b
f =\\< :: (a -> Tick b) -> Tick a -> Tick b
=\\< Tick Int
m a
x = let Tick Int
n b
y = a -> Tick b
f a
x in Int -> b -> Tick b
forall a. Int -> a -> Tick a
Tick (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) b
y

-------------------------------------------------------------------------------
-- | Memoisation:
-------------------------------------------------------------------------------

{-@ reflect pay @-}
{-@ pay :: m:Int
      -> { t1:Tick a | m <= tcost t1 }
      -> { t:Tick ({ t2 : Tick a | tcost t1 - m == tcost t2 }) | m == tcost t }
@-}
pay :: Int -> Tick a -> Tick (Tick a)
pay :: Int -> Tick a -> Tick (Tick a)
pay Int
m (Tick Int
n a
x) = Int -> Tick a -> Tick (Tick a)
forall a. Int -> a -> Tick a
Tick Int
m (Int -> a -> Tick a
forall a. Int -> a -> Tick a
Tick (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) a
x)


{-@ reflect zipWithM @-}
{-@ zipWithM :: f:(a -> b -> Tick c) -> x:Tick a -> y:Tick b
      -> {t:Tick c | tcost t == tcost x + tcost y + tcost (f (tval x) (tval y))} @-}
zipWithM :: (a -> b -> Tick c) -> Tick a -> Tick b -> Tick c
zipWithM :: (a -> b -> Tick c) -> Tick a -> Tick b -> Tick c
zipWithM a -> b -> Tick c
f (Tick Int
c1 a
x1) (Tick Int
c2 b
x2) = let Tick Int
c c
x = a -> b -> Tick c
f a
x1 b
x2 in Int -> c -> Tick c
forall a. Int -> a -> Tick a
Tick (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
c2) c
x