-- |
-- Description : Let GHC prove program equations
-- Copyright : (c) Joachim Breitner, 2017
-- License : MIT
-- Maintainer : mail@joachim-breitner.de
-- Portability : GHC specifc
--
-- This module supports the accompanying GHC plugin "GHC.Proof.Plugin" and adds
-- to GHC the ability to verify simple program equations.
--
-- = Synopis
--
-- Consider this module:
--
-- > {-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
-- > module Simple where
-- >
-- > import GHC.Proof
-- > import Data.Maybe
-- >
-- > my_proof1 :: (a -> b) -> Maybe a -> Proof
-- > my_proof1 f x = isNothing (fmap f x)
-- > === isNothing x
-- >
-- > my_proof2 :: a -> Maybe a -> Proof
-- > my_proof2 d x = fromMaybe d x
-- > === maybe d id x
--
-- Compiling it will result in this output:
--
-- > $ ghc Simple.hs
-- > [1 of 1] Compiling Simple ( Simple.hs, Simple.o )
-- > GHC.Proof: Proving my_proof1 …
-- > GHC.Proof: Proving my_proof2 …
-- > GHC.Proof proved 2 equalities
--
-- = Usage
--
-- To use this plugin, you have to
--
-- * Make sure you load the plugin @GHC.Proof.Plugin@, either by passing
-- @-fplugin GHC.Proof.Plugin@ to GHC or, more conveniently, using the
-- @OPTIONS_GHC@ pragma as above.
--
-- * Import the @GHC.Proof@ module.
--
-- * Define proof obligations using the 'proof' function or, equilvalently, the
-- '===' operator. Type signatures are optional.
--
-- These proof obligation must occur direclty on the
-- right-hand side of a top-level definition, where all parameters (if any)
-- are plain variables. For example, this would (currently) not work:
--
-- > not_good (f,x) = isNothing (fmap f x) === isNothing x
--
-- If your module has an explicit export list, then these functions need to
-- be exported (otherwise the compiler deletes them too quickly).
--
-- * Compile. If all proof obligations can be proven, compilation continues as
-- usual; otherwise it aborts.
--
-- = What can I prove this way?
--
-- Who knows... but generally you can only expect interesting results when you
-- use functions that are either non-recursive, or have an extensive rewrite
-- rule setup (such as lists). See the @examples/@ directory for some examples
-- of what works.
module GHC.Proof where
-- | A dummy data type, to give 'proof' a nicely readable type signature.
data Proof = Proof
-- | Instructs the compiler to see if it can prove the two arguments to 'proof'
-- to be equivalent.
proof :: a -> a -> Proof
proof _ _ = Proof
{-# INLINE [0] proof #-}
-- | Infix operator for 'proof'.
(===) :: a -> a -> Proof
(===) = proof
infix 0 ===
-- | Instructs the compiler to try to prove the two arguments to 'proof'
-- to be equivalent, but do not abort if it fails.
--
-- This is useful to document equalities that you would like to be proven, but
-- where @ghc-proofs@ does not work well enough.
non_proof :: a -> a -> Proof
non_proof _ _ = Proof
{-# INLINE [0] non_proof #-}
-- | Infix operator for 'non_proof'.
(=/=) :: a -> a -> Proof
(=/=) = non_proof
infix 0 =/=