Equational.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
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
_ *** 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 
_ ==. x = x 
{-# INLINE (==.) #-} 


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

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

infixl 3 ?

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

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

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