Proof.hs

{- |
This module defines the 'Proof' type, some proofs, and some helper functions.

A 'Proof' does three things:

 - verifies that the input value meets some criteria
 - optionally transforms the input value to another value while preserving that criteria
 - puts the proof name in type-signature where the type-checker can use it
-}
module Text.Reform.Proof where

import Control.Applicative.Indexed (IndexedFunctor(imap))
import Control.Monad.Trans   (lift)
import Numeric               (readDec, readFloat, readSigned)
import Text.Reform.Result (FormRange, Result(..))
import Text.Reform.Core   (Form(..), Proved(..))

-- | A 'Proof' attempts to prove something about a value.
--
-- If successful, it can also transform the value to a new value. The
-- proof should hold for the new value as well.
--
-- Generally, each 'Proof' has a unique data-type associated with it
-- which names the proof, such as:
--
-- > data NotNull = NotNull
--
data Proof m error proof a b
    = Proof { proofName     :: proof                   -- ^ name of the thing to prove
            , proofFunction :: a -> m (Either error b) -- ^ function which provides the proof
            }

-- | apply a 'Proof' to a 'Form'
prove :: (Monad m) =>
         Form m input error view q a
      -> Proof m error proof a b
      -> Form m input error view proof b
prove (Form frm) (Proof p f) =
    Form $ do (xml, mval) <- frm
              val <- lift $ lift $ mval
              case val of
                (Error errs)            -> return (xml, return $ Error errs)
                (Ok (Proved _ pos a)) ->
                    do r <- lift $ lift $ f a
                       case r of
                         (Left err) -> return (xml, return $ Error [(pos, err)])
                         (Right b)  ->
                             return (xml, return $ Ok (Proved { proofs   = p
                                                              , pos      = pos
                                                              , unProved = b
                                                              }))

-- * transformations (proofs minus the proof).

-- | transform a 'Form' using a 'Proof', and the replace the proof with @()@.
--
-- This is useful when you want just want classic digestive-functors behaviour.
transform :: (Monad m) =>
             Form m input error view anyProof a
          -> Proof m error proof a b
          -> Form m input error view () b
transform frm proof = imap (const ()) id (frm `prove` proof)

-- | transform the 'Form' result using a monadic 'Either' function.
transformEitherM :: (Monad m) => Form m input error view anyProof a
                 -> (a -> m (Either error b))
                 -> Form m input error view () b
transformEitherM frm func = frm `transform` (Proof () func)

-- | transform the 'Form' result using an 'Either' function.
transformEither :: (Monad m) =>
                   Form m input error view anyProof a
                -> (a -> Either error b)
                -> Form m input error view () b
transformEither frm func = transformEitherM frm (return . func)

-- * Various Proofs

-- | proof that a list is not empty
data NotNull = NotNull

-- | prove that a list is not empty
notNullProof :: (Monad m) => error -> Proof m error NotNull [a] [a]
notNullProof errorMsg = Proof NotNull (return . check)
    where
    check list =
        if null list
          then (Left errorMsg)
          else (Right list)

-- | proof that a 'String' is a decimal number
data Decimal        = Decimal
-- | proof that a 'String' is a Real/Fractional number
data RealFractional = RealFractional
-- | proof that a number is also (allowed to be) signed
data Signed a       = Signed a

-- | read an unsigned number in decimal notation
decimal :: (Monad m, Eq i, Num i) =>
           (String -> error) -- ^ create an error message ('String' is the value that did not parse)
        -> Proof m error Decimal String i
decimal mkError = Proof Decimal (return . toDecimal)
    where
      toDecimal str =
          case readDec str of
            [(d,[])] -> (Right d)
            _        -> (Left $ mkError str)

-- | read signed decimal number
signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i
signedDecimal mkError = Proof (Signed Decimal) (return . toDecimal)
    where
      toDecimal str =
          case (readSigned readDec) str of
            [(d,[])] -> (Right d)
            _        -> (Left $ mkError str)

-- | read 'RealFrac' number
realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error RealFractional String a
realFrac mkError = Proof RealFractional (return . toRealFrac)
    where
      toRealFrac str =
          case readFloat str of
            [(f,[])] -> (Right f)
            _        -> (Left $ mkError str)

-- | read a signed 'RealFrac' number
realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a
realFracSigned mkError = Proof (Signed RealFractional) (return . toRealFrac)
    where
      toRealFrac str =
          case (readSigned readFloat) str of
            [(f,[])] -> (Right f)
            _        -> (Left $ mkError str)