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(..))
data Proof m error proof a b
= Proof { Proof m error proof a b -> proof
proofName :: proof
, Proof m error proof a b -> a -> m (Either error b)
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 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
}))
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)
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)
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)
data NotNull = NotNull
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)
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 :: (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)
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)
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)
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)