    {- |
    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 { Proof m error proof a b -> proof
    proofName     :: proof                   -- ^ name of the thing to prove
                , Proof m error proof a b -> a -> m (Either error b)
    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 m input error view q a
    -> Proof m error proof a b -> Form m input error view proof b
    prove (Form frm :: FormState m input (View error view, m (Result error (Proved q a)))
    frm) (Proof p :: proof
    p f :: a -> m (Either error b)
    f) =
        FormState
      m input (View error view, m (Result error (Proved proof b)))
    -> Form m input error view proof b
    forall (m :: * -> *) input error view proof a.
    FormState
      m input (View error view, m (Result error (Proved proof a)))
    -> Form m input error view proof a
    Form (FormState
       m input (View error view, m (Result error (Proved proof b)))
     -> Form m input error view proof b)
    -> FormState
         m input (View error view, m (Result error (Proved proof b)))
    -> Form m input error view proof b
    forall a b. (a -> b) -> a -> b
    $ do (xml :: View error view
    xml, mval :: m (Result error (Proved q a))
    mval) <- FormState m input (View error view, m (Result error (Proved q a)))
    frm
                  Result error (Proved q a)
    val <- StateT FormRange m (Result error (Proved q a))
    -> ReaderT
         (Environment m input)
         (StateT FormRange m)
         (Result error (Proved q a))
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT FormRange m (Result error (Proved q a))
     -> ReaderT
          (Environment m input)
          (StateT FormRange m)
          (Result error (Proved q a)))
    -> StateT FormRange m (Result error (Proved q a))
    -> ReaderT
         (Environment m input)
         (StateT FormRange m)
         (Result error (Proved q a))
    forall a b. (a -> b) -> a -> b
    $ m (Result error (Proved q a))
    -> StateT FormRange m (Result error (Proved q a))
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Result error (Proved q a))
     -> StateT FormRange m (Result error (Proved q a)))
    -> m (Result error (Proved q a))
    -> StateT FormRange m (Result error (Proved q a))
    forall a b. (a -> b) -> a -> b
    $ m (Result error (Proved q a))
    mval
                  case Result error (Proved q a)
    val of
                    (Error errs :: [(FormRange, error)]
    errs)            -> (View error view, m (Result error (Proved proof b)))
    -> FormState
         m input (View error view, m (Result error (Proved proof b)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (View error view
    xml, Result error (Proved proof b) -> m (Result error (Proved proof b))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result error (Proved proof b)
     -> m (Result error (Proved proof b)))
    -> Result error (Proved proof b)
    -> m (Result error (Proved proof b))
    forall a b. (a -> b) -> a -> b
    $ [(FormRange, error)] -> Result error (Proved proof b)
    forall e ok. [(FormRange, e)] -> Result e ok
    Error [(FormRange, error)]
    errs)
                    (Ok (Proved _ pos :: FormRange
    pos a :: a
    a)) ->
                        do Either error b
    r <- StateT FormRange m (Either error b)
    -> ReaderT
         (Environment m input) (StateT FormRange m) (Either error b)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT FormRange m (Either error b)
     -> ReaderT
          (Environment m input) (StateT FormRange m) (Either error b))
    -> StateT FormRange m (Either error b)
    -> ReaderT
         (Environment m input) (StateT FormRange m) (Either error b)
    forall a b. (a -> b) -> a -> b
    $ m (Either error b) -> StateT FormRange m (Either error b)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Either error b) -> StateT FormRange m (Either error b))
    -> m (Either error b) -> StateT FormRange m (Either error b)
    forall a b. (a -> b) -> a -> b
    $ a -> m (Either error b)
    f a
    a
                           case Either error b
    r of
                             (Left err :: error
    err) -> (View error view, m (Result error (Proved proof b)))
    -> FormState
         m input (View error view, m (Result error (Proved proof b)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (View error view
    xml, Result error (Proved proof b) -> m (Result error (Proved proof b))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result error (Proved proof b)
     -> m (Result error (Proved proof b)))
    -> Result error (Proved proof b)
    -> m (Result error (Proved proof b))
    forall a b. (a -> b) -> a -> b
    $ [(FormRange, error)] -> Result error (Proved proof b)
    forall e ok. [(FormRange, e)] -> Result e ok
    Error [(FormRange
    pos, error
    err)])
                             (Right b :: b
    b)  ->
                                 (View error view, m (Result error (Proved proof b)))
    -> FormState
         m input (View error view, m (Result error (Proved proof b)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (View error view
    xml, Result error (Proved proof b) -> m (Result error (Proved proof b))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result error (Proved proof b)
     -> m (Result error (Proved proof b)))
    -> Result error (Proved proof b)
    -> m (Result error (Proved proof b))
    forall a b. (a -> b) -> a -> b
    $ Proved proof b -> Result error (Proved proof b)
    forall e ok. ok -> Result e ok
    Ok (Proved :: forall proofs a. proofs -> FormRange -> a -> Proved proofs a
    Proved { proofs :: proof
    proofs   = proof
    p
                                                                  , pos :: FormRange
    pos      = FormRange
    pos
                                                                  , unProved :: b
    unProved = b
    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 :: Form m input error view anyProof a
    -> Proof m error proof a b -> Form m input error view () b
    transform frm :: Form m input error view anyProof a
    frm proof :: Proof m error proof a b
    proof = (proof -> ())
    -> (b -> b)
    -> Form m input error view proof b
    -> Form m input error view () b
    forall (f :: * -> * -> *) x y a b.
    IndexedFunctor f =>
    (x -> y) -> (a -> b) -> f x a -> f y b
    imap (() -> proof -> ()
    forall a b. a -> b -> a
    const ()) b -> b
    forall a. a -> a
    id (Form m input error view anyProof a
    frm Form m input error view anyProof a
    -> Proof m error proof a b -> Form m input error view proof b
    forall (m :: * -> *) input error view q a proof b.
    Monad m =>
    Form m input error view q a
    -> Proof m error proof a b -> Form m input error view proof b
    `prove` Proof m error proof a b
    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 :: Form m input error view anyProof a
    -> (a -> m (Either error b)) -> Form m input error view () b
    transformEitherM frm :: Form m input error view anyProof a
    frm func :: a -> m (Either error b)
    func = Form m input error view anyProof a
    frm Form m input error view anyProof a
    -> Proof m error () a b -> Form m input error view () b
    forall (m :: * -> *) input error view anyProof a proof b.
    Monad m =>
    Form m input error view anyProof a
    -> Proof m error proof a b -> Form m input error view () b
    `transform` (() -> (a -> m (Either error b)) -> Proof m error () a b
    forall (m :: * -> *) error proof a b.
    proof -> (a -> m (Either error b)) -> Proof m error proof a b
    Proof () a -> m (Either error b)
    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 :: Form m input error view anyProof a
    -> (a -> Either error b) -> Form m input error view () b
    transformEither frm :: Form m input error view anyProof a
    frm func :: a -> Either error b
    func = Form m input error view anyProof a
    -> (a -> m (Either error b)) -> Form m input error view () b
    forall (m :: * -> *) input error view anyProof a b.
    Monad m =>
    Form m input error view anyProof a
    -> (a -> m (Either error b)) -> Form m input error view () b
    transformEitherM Form m input error view anyProof a
    frm (Either error b -> m (Either error b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either error b -> m (Either error b))
    -> (a -> Either error b) -> a -> m (Either error b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Either error b
    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 :: error -> Proof m error NotNull [a] [a]
    notNullProof errorMsg :: error
    errorMsg = NotNull
    -> ([a] -> m (Either error [a])) -> Proof m error NotNull [a] [a]
    forall (m :: * -> *) error proof a b.
    proof -> (a -> m (Either error b)) -> Proof m error proof a b
    Proof NotNull
    NotNull (Either error [a] -> m (Either error [a])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either error [a] -> m (Either error [a]))
    -> ([a] -> Either error [a]) -> [a] -> m (Either error [a])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> Either error [a]
    forall (t :: * -> *) a. Foldable t => t a -> Either error (t a)
    check)
        where
        check :: t a -> Either error (t a)
    check list :: t a
    list =
            if t a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null t a
    list
              then (error -> Either error (t a)
    forall a b. a -> Either a b
    Left error
    errorMsg)
              else (t a -> Either error (t a)
    forall a b. b -> Either a b
    Right t a
    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 :: (String -> error) -> Proof m error Decimal String i
    decimal mkError :: String -> error
    mkError = Decimal
    -> (String -> m (Either error i)) -> Proof m error Decimal String i
    forall (m :: * -> *) error proof a b.
    proof -> (a -> m (Either error b)) -> Proof m error proof a b
    Proof Decimal
    Decimal (Either error i -> m (Either error i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either error i -> m (Either error i))
    -> (String -> Either error i) -> String -> m (Either error i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Either error i
    forall b. (Eq b, Num b) => String -> Either error b
    toDecimal)
        where
          toDecimal :: String -> Either error b
    toDecimal str :: String
    str =
              case ReadS b
    forall a. (Eq a, Num a) => ReadS a
    readDec String
    str of
                [(d :: b
    d,[])] -> (b -> Either error b
    forall a b. b -> Either a b
    Right b
    d)
                _        -> (error -> Either error b
    forall a b. a -> Either a b
    Left (error -> Either error b) -> error -> Either error b
    forall a b. (a -> b) -> a -> b
    $ String -> error
    mkError String
    str)

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

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

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