{-# LANGUAGE
    DeriveFunctor
  , NamedFieldPuns
  , ScopedTypeVariables
#-}

{- |
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 Ditto.Proof where

import Control.Monad.Trans (lift)
import Ditto.Core (Form(..))
import Ditto.Backend (FormError(..))
import Ditto.Types (Proved(..), Result(..))
import Numeric (readDec, readFloat, readSigned)

-- | 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 Proof m err a b = Proof
  { Proof m err a b -> a -> m (Either err b)
proofFunction :: a -> m (Either err b) -- ^ function which provides the proof
  , Proof m err a b -> a -> b
proofNewInitialValue :: a -> b -- ^ usually @const b@
  } deriving (a -> Proof m err a b -> Proof m err a a
(a -> b) -> Proof m err a a -> Proof m err a b
(forall a b. (a -> b) -> Proof m err a a -> Proof m err a b)
-> (forall a b. a -> Proof m err a b -> Proof m err a a)
-> Functor (Proof m err a)
forall a b. a -> Proof m err a b -> Proof m err a a
forall a b. (a -> b) -> Proof m err a a -> Proof m err a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) err a a b.
Functor m =>
a -> Proof m err a b -> Proof m err a a
forall (m :: * -> *) err a a b.
Functor m =>
(a -> b) -> Proof m err a a -> Proof m err a b
<$ :: a -> Proof m err a b -> Proof m err a a
$c<$ :: forall (m :: * -> *) err a a b.
Functor m =>
a -> Proof m err a b -> Proof m err a a
fmap :: (a -> b) -> Proof m err a a -> Proof m err a b
$cfmap :: forall (m :: * -> *) err a a b.
Functor m =>
(a -> b) -> Proof m err a a -> Proof m err a b
Functor)

-- | apply a 'Proof' to a 'Form'
prove
  :: (Monad m, Monoid view, FormError input error)
  => Form m input error view a
  -> Proof m error a b
  -> Form m input error view b
prove :: Form m input error view a
-> Proof m error a b -> Form m input error view b
prove Form{input -> m (Either error a)
formDecodeInput :: forall (m :: * -> *) input err view a.
Form m input err view a -> input -> m (Either err a)
formDecodeInput :: input -> m (Either error a)
formDecodeInput, m a
formInitialValue :: forall (m :: * -> *) input err view a.
Form m input err view a -> m a
formInitialValue :: m a
formInitialValue, FormState m (View error view, Result error (Proved a))
formFormlet :: forall (m :: * -> *) input err view a.
Form m input err view a
-> FormState m (View err view, Result err (Proved a))
formFormlet :: FormState m (View error view, Result error (Proved a))
formFormlet} (Proof a -> m (Either error b)
f a -> b
ivB) = (input -> m (Either error b))
-> m b
-> FormState m (View error view, Result error (Proved b))
-> Form m input error view b
forall (m :: * -> *) input err view a.
(input -> m (Either err a))
-> m a
-> FormState m (View err view, Result err (Proved a))
-> Form m input err view a
Form
  (\input
input -> do
    Either error a
a <- input -> m (Either error a)
formDecodeInput input
input
    case Either error a
a of
      Left error
x -> Either error b -> m (Either error b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either error b -> m (Either error b))
-> Either error b -> m (Either error b)
forall a b. (a -> b) -> a -> b
$ error -> Either error b
forall a b. a -> Either a b
Left error
x
      Right a
x -> a -> m (Either error b)
f a
x
  )
  ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
ivB m a
formInitialValue)
  ( do
    (View error view
html, Result error (Proved a)
a) <- FormState m (View error view, Result error (Proved a))
formFormlet
    Result error (Proved b)
res <- m (Result error (Proved b))
-> StateT FormRange m (Result error (Proved b))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Result error (Proved b))
 -> StateT FormRange m (Result error (Proved b)))
-> m (Result error (Proved b))
-> StateT FormRange m (Result error (Proved b))
forall a b. (a -> b) -> a -> b
$ case Result error (Proved a)
a of
      Error [(FormRange, error)]
xs -> Result error (Proved b) -> m (Result error (Proved b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result error (Proved b) -> m (Result error (Proved b)))
-> Result error (Proved b) -> m (Result error (Proved b))
forall a b. (a -> b) -> a -> b
$ [(FormRange, error)] -> Result error (Proved b)
forall e ok. [(FormRange, e)] -> Result e ok
Error [(FormRange, error)]
xs
      Ok (Proved FormRange
pos a
x) -> do
        Either error b
eeb <- a -> m (Either error b)
f a
x
        case Either error b
eeb of
          Left error
err -> Result error (Proved b) -> m (Result error (Proved b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result error (Proved b) -> m (Result error (Proved b)))
-> Result error (Proved b) -> m (Result error (Proved b))
forall a b. (a -> b) -> a -> b
$ [(FormRange, error)] -> Result error (Proved b)
forall e ok. [(FormRange, e)] -> Result e ok
Error [(FormRange
pos, error
err)]
          Right b
res -> Result error (Proved b) -> m (Result error (Proved b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result error (Proved b) -> m (Result error (Proved b)))
-> Result error (Proved b) -> m (Result error (Proved b))
forall a b. (a -> b) -> a -> b
$ Proved b -> Result error (Proved b)
forall e ok. ok -> Result e ok
Ok (FormRange -> b -> Proved b
forall a. FormRange -> a -> Proved a
Proved FormRange
pos b
res)
    (View error view, Result error (Proved b))
-> FormState m (View error view, Result error (Proved b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( View error view
html
      , Result error (Proved b)
res
      )
  )

-- * transformations (proofs minus the proof).

-- | transform the 'Form' result using a monadic 'Either' function.
transformEitherM
  :: (Monad m, Monoid view, FormError input error)
  => Form m input error view a
  -> (a -> m (Either error b))
  -> (a -> b)
  -> Form m input error view b
transformEitherM :: Form m input error view a
-> (a -> m (Either error b))
-> (a -> b)
-> Form m input error view b
transformEitherM Form m input error view a
frm a -> m (Either error b)
func a -> b
ivb = Form m input error view a
frm Form m input error view a
-> Proof m error a b -> Form m input error view b
forall (m :: * -> *) view input error a b.
(Monad m, Monoid view, FormError input error) =>
Form m input error view a
-> Proof m error a b -> Form m input error view b
`prove` (a -> m (Either error b)) -> (a -> b) -> Proof m error a b
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof a -> m (Either error b)
func a -> b
ivb

-- | transform the 'Form' result using an 'Either' function.
transformEither
  :: (Monad m, Monoid view, FormError input error)
  => Form m input error view a
  -> (a -> Either error b)
  -> (a -> b)
  -> Form m input error view b
transformEither :: Form m input error view a
-> (a -> Either error b) -> (a -> b) -> Form m input error view b
transformEither Form m input error view a
frm a -> Either error b
func a -> b
ivb = Form m input error view a
-> (a -> m (Either error b))
-> (a -> b)
-> Form m input error view b
forall (m :: * -> *) view input error a b.
(Monad m, Monoid view, FormError input error) =>
Form m input error view a
-> (a -> m (Either error b))
-> (a -> b)
-> Form m input error view b
transformEitherM Form m input error view a
frm (Either error b -> m (Either error b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) a -> b
ivb

-- * Various Proofs

-- | prove that a list is not empty
notNullProof :: (Monad m) => error -> Proof m error [a] [a]
notNullProof :: error -> Proof m error [a] [a]
notNullProof error
errorMsg = ([a] -> m (Either error [a]))
-> ([a] -> [a]) -> Proof m error [a] [a]
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof (Either error [a] -> m (Either error [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) [a] -> [a]
forall a. a -> a
id
  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

-- | 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)
  -> i
  -> Proof m error String i
decimal :: (String -> error) -> i -> Proof m error String i
decimal String -> error
mkError i
i = (String -> m (Either error i))
-> (String -> i) -> Proof m error String i
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof (Either error i -> m (Either error i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) (i -> String -> i
forall a b. a -> b -> a
const i
i)
  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)
  -> i
  -> Proof m error String i
signedDecimal :: (String -> error) -> i -> Proof m error String i
signedDecimal String -> error
mkError i
i = (String -> m (Either error i))
-> (String -> i) -> Proof m error String i
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof (Either error i -> m (Either error i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) (i -> String -> i
forall a b. a -> b -> a
const i
i)
  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)
  -> a
  -> Proof m error String a
realFrac :: (String -> error) -> a -> Proof m error String a
realFrac String -> error
mkError a
a = (String -> m (Either error a))
-> (String -> a) -> Proof m error String a
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof (Either error a -> m (Either error a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) (a -> String -> a
forall a b. a -> b -> a
const a
a)
  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)
  -> a
  -> Proof m error String a
realFracSigned :: (String -> error) -> a -> Proof m error String a
realFracSigned String -> error
mkError a
a = (String -> m (Either error a))
-> (String -> a) -> Proof m error String a
forall (m :: * -> *) err a b.
(a -> m (Either err b)) -> (a -> b) -> Proof m err a b
Proof (Either error a -> m (Either error a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) (a -> String -> a
forall a b. a -> b -> a
const a
a)
  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