module Ditto.Proof where
import Control.Monad.Trans (lift)
import Data.Bifunctor (Bifunctor (bimap))
import Numeric (readDec, readFloat, readSigned)
import Ditto.Core (Form (..), Proved (..))
import Ditto.Result (Result (..))
data Proof m error proof a b
= Proof
{ proofName :: proof
, proofFunction :: a -> m (Either error b)
}
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) -> pure (xml, pure $ Error errs)
(Ok (Proved _ posi a)) ->
do
r <- lift $ lift $ f a
case r of
(Left err) -> pure (xml, pure $ Error [(posi, err)])
(Right b) ->
pure
( xml
, pure $
Ok
( Proved
{ proofs = p
, pos = posi
, unProved = b
}
)
)
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 = bimap (const ()) id (frm `prove` proof)
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)
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 (pure . func)
data NotNull = NotNull
notNullProof :: (Monad m) => error -> Proof m error NotNull [a] [a]
notNullProof errorMsg = Proof NotNull (pure . check)
where
check list =
if null list
then (Left errorMsg)
else (Right list)
data Decimal = Decimal
data RealFractional = RealFractional
data Signed a = Signed a
decimal
:: (Monad m, Eq i, Num i)
=> (String -> error)
-> Proof m error Decimal String i
decimal mkError = Proof Decimal (pure . toDecimal)
where
toDecimal str =
case readDec str of
[(d, [])] -> (Right d)
_ -> (Left $ mkError str)
signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i
signedDecimal mkError = Proof (Signed Decimal) (pure . toDecimal)
where
toDecimal str =
case (readSigned readDec) str of
[(d, [])] -> (Right d)
_ -> (Left $ mkError str)
realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error RealFractional String a
realFrac mkError = Proof RealFractional (pure . toRealFrac)
where
toRealFrac str =
case readFloat str of
[(f, [])] -> (Right f)
_ -> (Left $ mkError str)
realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a
realFracSigned mkError = Proof (Signed RealFractional) (pure . toRealFrac)
where
toRealFrac str =
case (readSigned readFloat) str of
[(f, [])] -> (Right f)
_ -> (Left $ mkError str)