--
-- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
--

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

module Language.Haskell.Liquid.RTick.Combinators
  (

  -- Basic:
    Proof         -- Simply the unit type.
  , QED(..)       -- 'ASS': Signify the end of an /unfinished/ proof.
                  -- 'QED': Signify the end of a /complete/ proof.
  , (&&&)         -- Combine proofs.
  , (***)         -- Discard final result at the end of a proof.
  , (?)           -- Appeal to an external theorem.
  , isAss         -- Check whether a proof is complete.
  , toProof       -- Cast to proof.
  , trivial       -- Trivial proof.
  , withTheorem   -- Appeal to an external theorem.
  -- Equational:
  , (==.)         -- Equality.
  , (==?)         -- Equality (assumption).
  , eq            -- Equality. Note: 'eq' is inlined in the logic.
  -- Inequational:
  , (<.)          -- Less than.
  , (<?)          -- Less than (assumption).
  , (<=.)         -- Less than or equal.
  , (<=?)         -- Less than or equal (assumption).
  , (>.)          -- Greater than.
  , (>?)          -- Greater than (assumption).
  , (>=.)         -- Greater than or equal.
  , (>=?)         -- Greater than or equal (assumption).
  , (<=>.)        -- Cost equivalence.
  , (<=>?)        -- Cost equivalence (assumption)
  , (>~>.)        -- Improvement.
  , (>~>?)        -- Improvement (assumption).
  , (.>==)        -- Quantified improvement.
  , (?>==)        -- Quantified improvement (assumption).
  , (<~<.)        -- Diminishment.
  , (<~<?)        -- Diminishment (assumption).
  , (.<==)        -- Quantified diminishment.
  , (?<==)        -- Quantified diminishment (assumption).
  -- Cost separators:
  , (==>.)        -- Quantified improvement.
  , (==>?)        -- Quantified improvement (assumption).
  , (==<.)        -- Quantified diminishment.
  , (==<?)        -- Quantified diminishment (assumption).
  , (==!)
  , assert
  ) where

import Language.Haskell.Liquid.RTick ( Tick(..) )

--
-- Proof combinators for extrinsic cost analysis.
--

-------------------------------------------------------------------------------
-- | Basic:
-------------------------------------------------------------------------------

{-@ assert :: b:{Bool | b} -> {b} @-}
assert :: Bool -> Proof
assert :: Bool -> Proof
assert Bool
_ = ()

-- unchecked
(==!) :: a -> a -> a
a
_ ==! :: a -> a -> a
==! a
x = a
x


type Proof = ()
data QED   = QED | ASS

{-@ toProof :: a -> Proof @-}
toProof :: a -> Proof
toProof :: a -> Proof
toProof a
_ = ()
{-# INLINE toProof #-}

{-@ trivial :: Proof @-}
trivial :: Proof
trivial :: Proof
trivial = ()
{-# INLINE trivial #-}

{-@ measure isAss @-}
isAss :: QED -> Bool
isAss :: QED -> Bool
isAss QED
ASS = Bool
True
isAss QED
QED = Bool
False

{-@ assume (***) :: a -> qed:QED -> { if (isAss qed) then false else true } @-}
infixl 1 ***
(***) :: a -> QED -> Proof
a
_ *** :: a -> QED -> Proof
*** QED
_ = ()
{-# INLINE (***) #-}

{-@ (?) :: x:a -> Proof -> { v:a | x == v } @-}
infixl 3 ?
(?) :: a -> Proof -> a
a
x ? :: a -> Proof -> a
? Proof
_ = a
x
{-# INLINE (?) #-}

{-@ (&&&) :: Proof -> Proof -> Proof @-}
infixl 3 &&&
(&&&) :: Proof -> Proof -> Proof
Proof
x &&& :: Proof -> Proof -> Proof
&&& Proof
_ = Proof
x
{-# INLINE (&&&) #-}

{-@ withTheorem :: x:a -> Proof -> { v:a | x == v } @-}
withTheorem :: a -> Proof -> a
withTheorem :: a -> Proof -> a
withTheorem a
x Proof
_ = a
x
{-# INLINE withTheorem #-}

-------------------------------------------------------------------------------
-- | Equational:
-------------------------------------------------------------------------------

--
-- Equality.
--
{-@ (==.) :: x:a -> { y:a | x == y } -> { v:a | x == v && y == v } @-}
infixl 3 ==.
(==.) :: a -> a -> a
a
_ ==. :: a -> a -> a
==. a
x = a
x
{-# INLINE (==.) #-}

{-@ assume (==?) :: x:a -> y:a -> { v:a | x == v && y == v } @-}
infixl 3 ==?
(==?) :: a -> a -> a
a
_ ==? :: a -> a -> a
==? a
x = a
x
{-# INLINE (==?) #-}

--
-- Equality. Note: 'eq' is inlined in the logic, so can be used in
-- reflected functions.
--
{-@ eq :: x:a -> { y:a | x == y } -> { v:a | x == v && y == v } @-}
eq :: a -> a -> a
a
_ eq :: a -> a -> a
`eq` a
x = a
x
{-# INLINE eq #-}

-------------------------------------------------------------------------------
-- | Inequational:
-------------------------------------------------------------------------------

--
-- Less than.
--
{-@ (<.) :: m:a -> { n:a | m < n } -> { o:a | o == n } @-}
infixl 3 <.
(<.) :: a -> a -> a
a
_ <. :: a -> a -> a
<. a
n = a
n
{-# INLINE (<.) #-}

{-@ assume (<?) :: m:a -> n:a -> { o:a | o == n && m < n } @-}
infixl 3 <?
(<?) :: a -> a -> a
a
_ <? :: a -> a -> a
<? a
n = a
n
{-# INLINE (<?) #-}

--
-- Less than or equal.
--
{-@ (<=.) :: m:a -> { n:a | m <= n } -> { o:a | o == n } @-}
infixl 3 <=.
(<=.) :: a -> a -> a
a
_ <=. :: a -> a -> a
<=. a
n = a
n
{-# INLINE (<=.) #-}

{-@ assume (<=?) :: m:a -> n:a -> { o:a | o == n && m <= n } @-}
infixl 3 <=?
(<=?) :: a -> a -> a
a
_ <=? :: a -> a -> a
<=? a
n = a
n
{-# INLINE (<=?) #-}

--
-- Greater than.
--
{-@ (>.) :: m:a -> { n:a | m > n } -> { o:a | o == n } @-}
infixl 3 >.
(>.) :: a -> a -> a
a
_ >. :: a -> a -> a
>. a
y = a
y
{-# INLINE (>.) #-}

{-@ assume (>?) :: m:a -> n:a -> { o:a | o == n && m > n } @-}
infixl 3 >?
(>?) :: a -> a -> a
a
_ >? :: a -> a -> a
>? a
y = a
y
{-# INLINE (>?) #-}

--
-- Greater than or equal.
--
{-@ (>=.) :: m:a -> { n:a | m >= n } -> { o:a | o == n } @-}
infixl 3 >=.
(>=.) :: a -> a -> a
a
_ >=. :: a -> a -> a
>=. a
n = a
n
{-# INLINE (>=.) #-}

{-@ assume (>=?) :: m:a -> n:a -> { o:a | o == n && m >= n } @-}
infixl 3 >=?
(>=?) :: a -> a -> a
a
_ >=? :: a -> a -> a
>=? a
n = a
n
{-# INLINE (>=?) #-}

--
-- Cost equivalence.
--
{-@ predicate COSTEQ T1 T2 = tval T1 == tval T2 && tcost T1 == tcost T2 @-}

{-@ (<=>.)
      :: t1:Tick a
      -> { t2:Tick a | COSTEQ t1 t2 }
      -> { t3:Tick a | COSTEQ t1 t2 && COSTEQ t1 t3 && COSTEQ t2 t3 }
@-}
infixl 3 <=>.
(<=>.) :: Tick a -> Tick a -> Tick a
<=>. :: Tick a -> Tick a -> Tick a
(<=>.) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (<=>.) #-}

{-@ assume (<=>?)
      :: t1:Tick a -> t2:Tick a
      -> { t3:Tick a | COSTEQ t1 t2 && COSTEQ t1 t3 && t2 == t3 }
@-}
infixl 3 <=>?
(<=>?) :: Tick a -> Tick a -> Tick a
<=>? :: Tick a -> Tick a -> Tick a
(<=>?) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (<=>?) #-}

--
-- Improvement.
--
{-@ predicate IMP T1 T2 = tval T1 == tval T2 && tcost T1 >= tcost T2 @-}

{-@ (>~>.)
      :: t1:Tick a
      -> { t2:Tick a | IMP t1 t2 }
      -> { t3:Tick a | IMP t1 t2 && IMP t1 t3 && t2 == t3 }
@-}
infixl 3 >~>.
(>~>.) :: Tick a -> Tick a -> Tick a
>~>. :: Tick a -> Tick a -> Tick a
(>~>.) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (>~>.) #-}

{-@ assume (>~>?)
      :: t1:Tick a -> t2:Tick a
      -> { t3:Tick a | IMP t1 t2 && IMP t1 t3 && t2 == t3 }
@-}
infixl 3 >~>?
(>~>?) :: Tick a -> Tick a -> Tick a
>~>? :: Tick a -> Tick a -> Tick a
(>~>?) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (>~>?) #-}

--
-- Quantified improvement.
--
{-@ predicate QIMP T1 N T2 = tval T1 == tval T2 && tcost T1 == tcost T2 + N @-}

{-@ (.>==)
      :: t1:Tick a
      -> n:Int
      -> { t2:Tick a | QIMP t1 n t2 }
      -> { t3:Tick a | QIMP t1 n t2 && QIMP t1 n t3 && t2 == t3 }
@-}
infixl 3 .>==
(.>==) :: Tick a -> Int -> Tick a -> Tick a
.>== :: Tick a -> Int -> Tick a -> Tick a
(.>==) Tick a
_ Int
_ Tick a
t2 = Tick a
t2
{-# INLINE (.>==) #-}

{-@ assume (?>==)
     :: t1:Tick a -> n:Nat -> t2:Tick a
     -> { t3:Tick a | QIMP t1 n t2 && QIMP t1 n t3 && t2 == t3 }
@-}
infixl 3 ?>==
(?>==) :: Tick a -> Int -> Tick a -> Tick a
?>== :: Tick a -> Int -> Tick a -> Tick a
(?>==) Tick a
_ Int
_ Tick a
t2 = Tick a
t2
{-# INLINE (?>==) #-}

--
-- Diminishment.
--
{-@ predicate DIM T1 T2 = tval T1 == tval T2 && tcost T1 <= tcost T2 @-}

{-@ (<~<.)
      :: t1:Tick a
      -> { t2:Tick a | DIM t1 t2 }
      -> { t3:Tick a | DIM t1 t2 && DIM t1 t3 && t2 == t3 }
@-}
infixl 3 <~<.
(<~<.) :: Tick a -> Tick a -> Tick a
<~<. :: Tick a -> Tick a -> Tick a
(<~<.) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (<~<.) #-}

{-@ assume (<~<?)
     :: t1:Tick a -> t2:Tick a
     -> { t3:Tick a | DIM t1 t2 && DIM t1 t3 && t2 == t3 }
@-}
infixl 3 <~<?
(<~<?) :: Tick a -> Tick a -> Tick a
<~<? :: Tick a -> Tick a -> Tick a
(<~<?) Tick a
_ Tick a
t2 = Tick a
t2
{-# INLINE (<~<?) #-}

--
-- Quantified diminishment.
--
{-@ predicate QDIM T1 N T2 = tval T1 == tval T2 && tcost T1 + N == tcost T2 @-}

{-@ (.<==)
      :: t1:Tick a
      -> n:Nat
      -> { t2:Tick a | QDIM t1 n t2 }
      -> { t3:Tick a | QDIM t1 n t2 && QDIM t1 n t3 && t2 == t3 }
@-}
infixl 3 .<==
(.<==) :: Tick a -> Int -> Tick a -> Tick a
.<== :: Tick a -> Int -> Tick a -> Tick a
(.<==) Tick a
_ Int
_ Tick a
t2 = Tick a
t2
{-# INLINE (.<==) #-}

{-@ assume (?<==)
      :: t1:Tick a -> n:Nat -> t2:Tick a
      -> { t3:Tick a | QDIM t1 n t2 && QDIM t1 n t3 && t2 == t3 }
@-}
infixl 3 ?<==
(?<==) :: Tick a -> Int -> Tick a -> Tick a
?<== :: Tick a -> Int -> Tick a -> Tick a
(?<==) Tick a
_ Int
_ Tick a
t2 = Tick a
t2
{-# INLINE (?<==) #-}

-------------------------------------------------------------------------------
-- | Cost separators:
-------------------------------------------------------------------------------

--
-- Quantified improvement.
--
{-@ (==>.) :: (a -> b) -> a -> b @-}
infixl 3 ==>.
(==>.) :: (a -> b) -> a -> b
a -> b
f ==>. :: (a -> b) -> a -> b
==>. a
a = a -> b
f a
a
{-# INLINE (==>.) #-}

--
-- Quantified improvement (assumption).
--
{-@ (==>?) :: (a -> b) -> a -> b @-}
infixl 3 ==>?
(==>?) :: (a -> b) -> a -> b
a -> b
f ==>? :: (a -> b) -> a -> b
==>? a
a = a -> b
f a
a
{-# INLINE (==>?) #-}

--
-- Quantified diminishment.
--
{-@ (==<.) :: (a -> b) -> a -> b @-}
infixl 3 ==<.
(==<.) :: (a -> b) -> a -> b
a -> b
f ==<. :: (a -> b) -> a -> b
==<. a
a = a -> b
f a
a
{-# INLINE (==<.) #-}

--
-- Quantified diminishment (assumption).
--
{-@ (==<?) :: (a -> b) -> a -> b @-}
infixl 3 ==<?
(==<?) :: (a -> b) -> a -> b
a -> b
f ==<? :: (a -> b) -> a -> b
==<? a
a = a -> b
f a
a
{-# INLINE (==<?) #-}