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