module Language.Haskell.Liquid.Equational where 

-------------------------------------------------------------------------------
-- | Proof is just unit
-------------------------------------------------------------------------------

type Proof = ()

-------------------------------------------------------------------------------
-- | Casting expressions to Proof using the "postfix" `*** QED` 
-------------------------------------------------------------------------------

data QED = QED 

infixl 2 ***
(***) :: a -> QED -> Proof
a
_ *** :: a -> QED -> Proof
*** QED
QED = () 

-------------------------------------------------------------------------------
-- | Equational Reasoning operators 
-- | The `eq` operator is inlined in the logic, so can be used in reflected 
-- | functions while ignoring the equality steps. 
-------------------------------------------------------------------------------

infixl 3 ==., `eq` 


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


{-@ eq :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
eq :: a -> a -> a 
a
_ eq :: a -> a -> a
`eq` a
x = a
x 
{-# INLINE eq #-} 

-------------------------------------------------------------------------------
-- | Explanations
-------------------------------------------------------------------------------

infixl 3 ?

{-@ (?) :: forall a b <pa :: a -> Bool>. a<pa> -> b -> a<pa> @-}
(?) :: a -> b -> a 
a
x ? :: a -> b -> a
? b
_ = a
x 
{-# INLINE (?)   #-} 

-------------------------------------------------------------------------------
-- | Using proofs as theorems 
-------------------------------------------------------------------------------

withTheorem :: a -> Proof -> a 
withTheorem :: a -> Proof -> a
withTheorem a
z Proof
_ = a
z