{- |
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 FormState m input (View error view, m (Result error (Proved q a)))
frm) (Proof proof
p 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 (View error view
xml, 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 [(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 q
_ FormRange
pos 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 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)  ->
                             (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 Form m input error view anyProof a
frm 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 Form m input error view anyProof a
frm 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 Form m input error view anyProof a
frm 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 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 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 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 String
str =
          case ReadS b
forall a. (Eq a, Num a) => ReadS a
readDec String
str of
            [(b
d,[])] -> (b -> Either error b
forall a b. b -> Either a b
Right b
d)
            [(b, String)]
_        -> (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 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 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
            [(b
d,[])] -> (b -> Either error b
forall a b. b -> Either a b
Right b
d)
            [(b, String)]
_        -> (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 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 String
str =
          case ReadS b
forall a. RealFrac a => ReadS a
readFloat String
str of
            [(b
f,[])] -> (b -> Either error b
forall a b. b -> Either a b
Right b
f)
            [(b, String)]
_        -> (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 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 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
            [(b
f,[])] -> (b -> Either error b
forall a b. b -> Either a b
Right b
f)
            [(b, String)]
_        -> (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)