{-# LANGUAGE
MultiParamTypeClasses
, FlexibleContexts
, FunctionalDependencies
, TemplateHaskellQuotes
#-}
module Data.Validation
(
Proof(..)
, fromVCtx
, ValueCtx(..)
, getValue
, setValue
, withField
, withValue
, Validatable(..)
, validate
, refute
, refuteMany
, refuteWith
, refuteWithProof
, dispute
, disputeMany
, disputeWith
, disputeWithFact
, isRequired
, isRequiredWhen
, isRequiredUnless
, isLeft
, isRight
, isNull
, isNotNull
, minLength
, maxLength
, isLength
, isEqual
, isNotEqual
, isLessThan
, isLessThanOrEqual
, isGreaterThan
, isGreaterThanOrEqual
, hasElem
, doesNotHaveElem
, ifAny
, ifAll
, ifEach
, ifEachProven
, isMatch
, validateField
, optional
, whenJust
, aggregateFailures
, (<!)
, isValid
, isInvalid
, flattenProofs
, VCtx
, Name
, mkName
, nameBase
) where
import Prelude hiding (foldl)
import Data.Bool
import Data.Either (rights, lefts)
import Data.Foldable (fold)
import Data.Map hiding (null, fold)
import Data.Maybe
import Language.Haskell.TH (Name, mkName, nameBase)
import Data.Validation.Internal
data Proof f a
= Valid a
| Invalid [f] (Map [Name] [f])
deriving (Int -> Proof f a -> ShowS
[Proof f a] -> ShowS
Proof f a -> String
(Int -> Proof f a -> ShowS)
-> (Proof f a -> String)
-> ([Proof f a] -> ShowS)
-> Show (Proof f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f a. (Show a, Show f) => Int -> Proof f a -> ShowS
forall f a. (Show a, Show f) => [Proof f a] -> ShowS
forall f a. (Show a, Show f) => Proof f a -> String
showList :: [Proof f a] -> ShowS
$cshowList :: forall f a. (Show a, Show f) => [Proof f a] -> ShowS
show :: Proof f a -> String
$cshow :: forall f a. (Show a, Show f) => Proof f a -> String
showsPrec :: Int -> Proof f a -> ShowS
$cshowsPrec :: forall f a. (Show a, Show f) => Int -> Proof f a -> ShowS
Show, Proof f a -> Proof f a -> Bool
(Proof f a -> Proof f a -> Bool)
-> (Proof f a -> Proof f a -> Bool) -> Eq (Proof f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f a. (Eq a, Eq f) => Proof f a -> Proof f a -> Bool
/= :: Proof f a -> Proof f a -> Bool
$c/= :: forall f a. (Eq a, Eq f) => Proof f a -> Proof f a -> Bool
== :: Proof f a -> Proof f a -> Bool
$c== :: forall f a. (Eq a, Eq f) => Proof f a -> Proof f a -> Bool
Eq)
instance Semigroup a => Semigroup (Proof f a) where
(Valid a1 :: a
a1) <> :: Proof f a -> Proof f a -> Proof f a
<> (Valid a2 :: a
a2) = a -> Proof f a
forall f a. a -> Proof f a
Valid (a
a1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a2)
(Invalid gfs1 :: [f]
gfs1 lfs1 :: Map [Name] [f]
lfs1) <> (Invalid gfs2 :: [f]
gfs2 lfs2 :: Map [Name] [f]
lfs2) = [f] -> Map [Name] [f] -> Proof f a
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid ([f]
gfs1 [f] -> [f] -> [f]
forall a. Semigroup a => a -> a -> a
<> [f]
gfs2) (([f] -> [f] -> [f])
-> Map [Name] [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
unionWith [f] -> [f] -> [f]
forall a. Semigroup a => a -> a -> a
(<>) Map [Name] [f]
lfs1 Map [Name] [f]
lfs2)
(Valid _) <> (Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) = [f] -> Map [Name] [f] -> Proof f a
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
(Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) <> (Valid _) = [f] -> Map [Name] [f] -> Proof f a
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
instance Monoid a => Monoid (Proof f a) where
mempty :: Proof f a
mempty = a -> Proof f a
forall f a. a -> Proof f a
Valid a
forall a. Monoid a => a
mempty
instance Functor (Proof f) where
fmap :: (a -> b) -> Proof f a -> Proof f b
fmap fn :: a -> b
fn (Valid a :: a
a) = b -> Proof f b
forall f a. a -> Proof f a
Valid (a -> b
fn a
a)
fmap _ (Invalid gps :: [f]
gps lps :: Map [Name] [f]
lps) = [f] -> Map [Name] [f] -> Proof f b
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gps Map [Name] [f]
lps
instance Applicative (Proof f) where
pure :: a -> Proof f a
pure = a -> Proof f a
forall f a. a -> Proof f a
Valid
(Invalid gfs1 :: [f]
gfs1 lfs1 :: Map [Name] [f]
lfs1) <*> :: Proof f (a -> b) -> Proof f a -> Proof f b
<*> (Invalid gfs2 :: [f]
gfs2 lfs2 :: Map [Name] [f]
lfs2) = [f] -> Map [Name] [f] -> Proof f b
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid ([f]
gfs1 [f] -> [f] -> [f]
forall a. Semigroup a => a -> a -> a
<> [f]
gfs2) (([f] -> [f] -> [f])
-> Map [Name] [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
unionWith [f] -> [f] -> [f]
forall a. Semigroup a => a -> a -> a
(<>) Map [Name] [f]
lfs1 Map [Name] [f]
lfs2)
(Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) <*> (Valid _) = [f] -> Map [Name] [f] -> Proof f b
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
(Valid _) <*> (Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) = [f] -> Map [Name] [f] -> Proof f b
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
Valid fn :: a -> b
fn <*> Valid a :: a
a = b -> Proof f b
forall f a. a -> Proof f a
Valid (b -> Proof f b) -> b -> Proof f b
forall a b. (a -> b) -> a -> b
$ a -> b
fn a
a
instance Monad (Proof f) where
(Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) >>= :: Proof f a -> (a -> Proof f b) -> Proof f b
>>= _ = [f] -> Map [Name] [f] -> Proof f b
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
(Valid a :: a
a) >>= fn :: a -> Proof f b
fn = a -> Proof f b
fn a
a
fromVCtx :: VCtx f a -> Proof f a
fromVCtx :: VCtx f a -> Proof f a
fromVCtx (ValidCtx a :: a
a) = a -> Proof f a
forall f a. a -> Proof f a
Valid a
a
fromVCtx (DisputedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs _) = [f] -> Map [Name] [f] -> Proof f a
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
fromVCtx (RefutedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs) = [f] -> Map [Name] [f] -> Proof f a
forall f a. [f] -> Map [Name] [f] -> Proof f a
Invalid [f]
gfs Map [Name] [f]
lfs
data ValueCtx a
= Field Name a
| Global a
deriving (Int -> ValueCtx a -> ShowS
[ValueCtx a] -> ShowS
ValueCtx a -> String
(Int -> ValueCtx a -> ShowS)
-> (ValueCtx a -> String)
-> ([ValueCtx a] -> ShowS)
-> Show (ValueCtx a)
forall a. Show a => Int -> ValueCtx a -> ShowS
forall a. Show a => [ValueCtx a] -> ShowS
forall a. Show a => ValueCtx a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValueCtx a] -> ShowS
$cshowList :: forall a. Show a => [ValueCtx a] -> ShowS
show :: ValueCtx a -> String
$cshow :: forall a. Show a => ValueCtx a -> String
showsPrec :: Int -> ValueCtx a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ValueCtx a -> ShowS
Show, ValueCtx a -> ValueCtx a -> Bool
(ValueCtx a -> ValueCtx a -> Bool)
-> (ValueCtx a -> ValueCtx a -> Bool) -> Eq (ValueCtx a)
forall a. Eq a => ValueCtx a -> ValueCtx a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValueCtx a -> ValueCtx a -> Bool
$c/= :: forall a. Eq a => ValueCtx a -> ValueCtx a -> Bool
== :: ValueCtx a -> ValueCtx a -> Bool
$c== :: forall a. Eq a => ValueCtx a -> ValueCtx a -> Bool
Eq)
instance Functor ValueCtx where
fmap :: (a -> b) -> ValueCtx a -> ValueCtx b
fmap fn :: a -> b
fn (Field n :: Name
n a :: a
a) = Name -> b -> ValueCtx b
forall a. Name -> a -> ValueCtx a
Field Name
n (a -> b
fn a
a)
fmap fn :: a -> b
fn (Global a :: a
a) = b -> ValueCtx b
forall a. a -> ValueCtx a
Global (a -> b
fn a
a)
getValue :: ValueCtx a -> a
getValue :: ValueCtx a -> a
getValue (Field _ a :: a
a) = a
a
getValue (Global a :: a
a) = a
a
setValue :: ValueCtx a -> b -> ValueCtx b
setValue :: ValueCtx a -> b -> ValueCtx b
setValue v :: ValueCtx a
v b :: b
b = b
b b -> ValueCtx a -> ValueCtx b
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ValueCtx a
v
withField :: Name -> a -> (ValueCtx a -> VCtx f (ValueCtx b)) -> VCtx f b
withField :: Name -> a -> (ValueCtx a -> VCtx f (ValueCtx b)) -> VCtx f b
withField n :: Name
n a :: a
a fn :: ValueCtx a -> VCtx f (ValueCtx b)
fn = ValueCtx a -> VCtx f (ValueCtx b)
fn (Name -> a -> ValueCtx a
forall a. Name -> a -> ValueCtx a
Field Name
n a
a) VCtx f (ValueCtx b) -> (ValueCtx b -> VCtx f b) -> VCtx f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> VCtx f b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> VCtx f b) -> (ValueCtx b -> b) -> ValueCtx b -> VCtx f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueCtx b -> b
forall a. ValueCtx a -> a
getValue
withValue :: a -> (ValueCtx a -> VCtx f (ValueCtx b)) -> VCtx f b
withValue :: a -> (ValueCtx a -> VCtx f (ValueCtx b)) -> VCtx f b
withValue a :: a
a fn :: ValueCtx a -> VCtx f (ValueCtx b)
fn = ValueCtx a -> VCtx f (ValueCtx b)
fn (a -> ValueCtx a
forall a. a -> ValueCtx a
Global a
a) VCtx f (ValueCtx b) -> (ValueCtx b -> VCtx f b) -> VCtx f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> VCtx f b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> VCtx f b) -> (ValueCtx b -> b) -> ValueCtx b -> VCtx f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueCtx b -> b
forall a. ValueCtx a -> a
getValue
class Validatable f a b | a -> f b where
validation :: a -> VCtx f b
validate :: Validatable f a b => a -> Proof f b
validate :: a -> Proof f b
validate = VCtx f b -> Proof f b
forall f a. VCtx f a -> Proof f a
fromVCtx (VCtx f b -> Proof f b) -> (a -> VCtx f b) -> a -> Proof f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> VCtx f b
forall f a b. Validatable f a b => a -> VCtx f b
validation
refute :: ValueCtx a -> f -> VCtx f b
refute :: ValueCtx a -> f -> VCtx f b
refute (Field n :: Name
n _) f :: f
f = [f] -> Map [Name] [f] -> VCtx f b
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] ([Name] -> [f] -> Map [Name] [f]
forall k a. k -> a -> Map k a
singleton [Name
n] [f
f])
refute (Global _) f :: f
f = [f] -> Map [Name] [f] -> VCtx f b
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f
f] Map [Name] [f]
forall k a. Map k a
empty
refuteMany :: ValueCtx a -> [f] -> VCtx f b
refuteMany :: ValueCtx a -> [f] -> VCtx f b
refuteMany (Field n :: Name
n _) fs :: [f]
fs = [f] -> Map [Name] [f] -> VCtx f b
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] ([Name] -> [f] -> Map [Name] [f]
forall k a. k -> a -> Map k a
singleton [Name
n] [f]
fs)
refuteMany (Global _) fs :: [f]
fs = [f] -> Map [Name] [f] -> VCtx f b
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f]
fs Map [Name] [f]
forall k a. Map k a
empty
dispute :: ValueCtx a -> f -> VCtx f (ValueCtx a)
dispute :: ValueCtx a -> f -> VCtx f (ValueCtx a)
dispute v :: ValueCtx a
v@(Field n :: Name
n _) f :: f
f = [f] -> Map [Name] [f] -> ValueCtx a -> VCtx f (ValueCtx a)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [] ([Name] -> [f] -> Map [Name] [f]
forall k a. k -> a -> Map k a
singleton [Name
n] [f
f]) ValueCtx a
v
dispute v :: ValueCtx a
v@(Global _) f :: f
f = [f] -> Map [Name] [f] -> ValueCtx a -> VCtx f (ValueCtx a)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [f
f] Map [Name] [f]
forall k a. Map k a
empty ValueCtx a
v
disputeMany :: ValueCtx a -> [f] -> VCtx f (ValueCtx a)
disputeMany :: ValueCtx a -> [f] -> VCtx f (ValueCtx a)
disputeMany v :: ValueCtx a
v@(Field n :: Name
n _) fs :: [f]
fs = [f] -> Map [Name] [f] -> ValueCtx a -> VCtx f (ValueCtx a)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [] ([Name] -> [f] -> Map [Name] [f]
forall k a. k -> a -> Map k a
singleton [Name
n] [f]
fs) ValueCtx a
v
disputeMany v :: ValueCtx a
v@(Global _) fs :: [f]
fs = [f] -> Map [Name] [f] -> ValueCtx a -> VCtx f (ValueCtx a)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [f]
fs Map [Name] [f]
forall k a. Map k a
empty ValueCtx a
v
disputeWith :: (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith :: (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith fn :: a -> Maybe f
fn v :: ValueCtx a
v = case a -> Maybe f
fn (ValueCtx a -> a
forall a. ValueCtx a -> a
getValue ValueCtx a
v) of
Just f :: f
f -> ValueCtx a -> f -> VCtx f (ValueCtx a)
forall a f. ValueCtx a -> f -> VCtx f (ValueCtx a)
dispute ValueCtx a
v f
f
Nothing -> ValueCtx a -> VCtx f (ValueCtx a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ValueCtx a
v
disputeWithFact :: f -> (a -> Bool) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWithFact :: f -> (a -> Bool) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWithFact f :: f
f fn :: a -> Bool
fn = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith (Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
fn)
refuteWith :: (a -> Either f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWith :: (a -> Either f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWith fn :: a -> Either f b
fn v :: ValueCtx a
v = case a -> Either f b
fn (ValueCtx a -> a
forall a. ValueCtx a -> a
getValue ValueCtx a
v) of
Left f :: f
f -> ValueCtx a -> f -> VCtx f (ValueCtx b)
forall a f b. ValueCtx a -> f -> VCtx f b
refute ValueCtx a
v f
f
Right b :: b
b -> ValueCtx b -> VCtx f (ValueCtx b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ValueCtx b -> VCtx f (ValueCtx b))
-> ValueCtx b -> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ ValueCtx a -> b -> ValueCtx b
forall a b. ValueCtx a -> b -> ValueCtx b
setValue ValueCtx a
v b
b
refuteWithProof :: (a -> Proof f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWithProof :: (a -> Proof f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWithProof f :: a -> Proof f b
f (Global a :: a
a) = case a -> Proof f b
f a
a of
Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f]
gfs Map [Name] [f]
lfs
Valid b :: b
b -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. a -> VCtx f a
ValidCtx (ValueCtx b -> VCtx f (ValueCtx b))
-> ValueCtx b -> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ b -> ValueCtx b
forall a. a -> ValueCtx a
Global b
b
refuteWithProof f :: a -> Proof f b
f (Field n :: Name
n a :: a
a) = case a -> Proof f b
f a
a of
Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] (Map [Name] [f] -> VCtx f (ValueCtx b))
-> Map [Name] [f] -> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ [Name] -> [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert [Name
n] [f]
gfs Map [Name] [f]
lfs
Valid b :: b
b -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. a -> VCtx f a
ValidCtx (ValueCtx b -> VCtx f (ValueCtx b))
-> ValueCtx b -> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ Name -> b -> ValueCtx b
forall a. Name -> a -> ValueCtx a
Field Name
n b
b
isRequired :: f -> ValueCtx (Maybe a) -> VCtx f (ValueCtx a)
isRequired :: f -> ValueCtx (Maybe a) -> VCtx f (ValueCtx a)
isRequired f :: f
f = (Maybe a -> Either f a)
-> ValueCtx (Maybe a) -> VCtx f (ValueCtx a)
forall a f b.
(a -> Either f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWith ((Maybe a -> Either f a)
-> ValueCtx (Maybe a) -> VCtx f (ValueCtx a))
-> (Maybe a -> Either f a)
-> ValueCtx (Maybe a)
-> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ \ma :: Maybe a
ma -> case Maybe a
ma of
Nothing -> f -> Either f a
forall a b. a -> Either a b
Left f
f
Just a :: a
a -> a -> Either f a
forall a b. b -> Either a b
Right a
a
isRequiredWhen :: f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
isRequiredWhen :: f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
isRequiredWhen _ False v :: ValueCtx (Maybe a)
v = ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return ValueCtx (Maybe a)
v
isRequiredWhen f :: f
f True v :: ValueCtx (Maybe a)
v = ((Maybe a -> Maybe f)
-> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a)))
-> ValueCtx (Maybe a)
-> (Maybe a -> Maybe f)
-> VCtx f (ValueCtx (Maybe a))
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe a -> Maybe f)
-> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ValueCtx (Maybe a)
v ((Maybe a -> Maybe f) -> VCtx f (ValueCtx (Maybe a)))
-> (Maybe a -> Maybe f) -> VCtx f (ValueCtx (Maybe a))
forall a b. (a -> b) -> a -> b
$ \ma :: Maybe a
ma -> case Maybe a
ma of
Nothing -> f -> Maybe f
forall a. a -> Maybe a
Just f
f
Just _ -> Maybe f
forall a. Maybe a
Nothing
isRequiredUnless :: f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
isRequiredUnless :: f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
isRequiredUnless f :: f
f b :: Bool
b v :: ValueCtx (Maybe a)
v = f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
forall f a.
f -> Bool -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe a))
isRequiredWhen f
f (Bool -> Bool
not Bool
b) ValueCtx (Maybe a)
v
isLeft :: f -> ValueCtx (Either a b) -> VCtx f (ValueCtx a)
isLeft :: f -> ValueCtx (Either a b) -> VCtx f (ValueCtx a)
isLeft f :: f
f = (Either a b -> Either f a)
-> ValueCtx (Either a b) -> VCtx f (ValueCtx a)
forall a f b.
(a -> Either f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWith ((Either a b -> Either f a)
-> ValueCtx (Either a b) -> VCtx f (ValueCtx a))
-> (Either a b -> Either f a)
-> ValueCtx (Either a b)
-> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ \e :: Either a b
e -> case Either a b
e of
Left a :: a
a -> a -> Either f a
forall a b. b -> Either a b
Right a
a
Right _ -> f -> Either f a
forall a b. a -> Either a b
Left f
f
isRight :: f -> ValueCtx (Either a b) -> VCtx f (ValueCtx b)
isRight :: f -> ValueCtx (Either a b) -> VCtx f (ValueCtx b)
isRight f :: f
f = (Either a b -> Either f b)
-> ValueCtx (Either a b) -> VCtx f (ValueCtx b)
forall a f b.
(a -> Either f b) -> ValueCtx a -> VCtx f (ValueCtx b)
refuteWith ((Either a b -> Either f b)
-> ValueCtx (Either a b) -> VCtx f (ValueCtx b))
-> (Either a b -> Either f b)
-> ValueCtx (Either a b)
-> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ \e :: Either a b
e -> case Either a b
e of
Right b :: b
b -> b -> Either f b
forall a b. b -> Either a b
Right b
b
Left _ -> f -> Either f b
forall a b. a -> Either a b
Left f
f
isNull :: Foldable t => f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isNull :: f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isNull f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
isNotNull :: Foldable t => f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isNotNull :: f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isNotNull f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (t a -> Bool) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
minLength :: Foldable t => Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
minLength :: Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
minLength l :: Int
l f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Int
l (Int -> Bool) -> (t a -> Int) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
maxLength :: Foldable t => Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
maxLength :: Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
maxLength l :: Int
l f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>=) Int
l (Int -> Bool) -> (t a -> Int) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
isLength :: Foldable t => Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isLength :: Int -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
isLength l :: Int
l f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) Int
l (Int -> Bool) -> (t a -> Int) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
isEqual :: Eq a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isEqual :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isEqual a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) a
a
isNotEqual :: Eq a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isNotEqual :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isNotEqual a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(/=) a
a
isLessThan :: Ord a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isLessThan :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isLessThan a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>) a
a
isGreaterThan :: Ord a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isGreaterThan :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isGreaterThan a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<) a
a
isLessThanOrEqual :: Ord a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isLessThanOrEqual :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isLessThanOrEqual a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=) a
a
isGreaterThanOrEqual :: Ord a => a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isGreaterThanOrEqual :: a -> f -> ValueCtx a -> VCtx f (ValueCtx a)
isGreaterThanOrEqual a :: a
a f :: f
f = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a))
-> (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (a -> Bool) -> a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=) a
a
hasElem :: (Foldable t, Eq a) => a -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
hasElem :: a -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
hasElem e :: a
e f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
e
doesNotHaveElem :: (Foldable t, Eq a) => a -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
doesNotHaveElem :: a -> f -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
doesNotHaveElem e :: a
e f :: f
f = (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith ((t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a)))
-> (t a -> Maybe f) -> ValueCtx (t a) -> VCtx f (ValueCtx (t a))
forall a b. (a -> b) -> a -> b
$ Maybe f -> Maybe f -> Bool -> Maybe f
forall a. a -> a -> Bool -> a
bool (f -> Maybe f
forall a. a -> Maybe a
Just f
f) Maybe f
forall a. Maybe a
Nothing (Bool -> Maybe f) -> (t a -> Bool) -> t a -> Maybe f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (t a -> Bool) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
e
ifAny :: (a -> Maybe f) -> ValueCtx [a] -> VCtx f (ValueCtx [a])
ifAny :: (a -> Maybe f) -> ValueCtx [a] -> VCtx f (ValueCtx [a])
ifAny fn :: a -> Maybe f
fn v :: ValueCtx [a]
v =
let
xs :: [a]
xs = ValueCtx [a] -> [a]
forall a. ValueCtx a -> a
getValue ValueCtx [a]
v
fs :: [f]
fs = [Maybe f] -> [f]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe f] -> [f]) -> [Maybe f] -> [f]
forall a b. (a -> b) -> a -> b
$ (a -> Maybe f) -> [a] -> [Maybe f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe f
fn [a]
xs
in if [f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [f]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs
then ValueCtx [a] -> [f] -> VCtx f (ValueCtx [a])
forall a f. ValueCtx a -> [f] -> VCtx f (ValueCtx a)
disputeMany ValueCtx [a]
v [f]
fs
else ValueCtx [a] -> VCtx f (ValueCtx [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ValueCtx [a]
v
ifAll :: (a -> Maybe f) -> ValueCtx [a] -> VCtx f (ValueCtx [a])
ifAll :: (a -> Maybe f) -> ValueCtx [a] -> VCtx f (ValueCtx [a])
ifAll fn :: a -> Maybe f
fn v :: ValueCtx [a]
v = case [Maybe f] -> [f]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe f] -> [f]) -> ([a] -> [Maybe f]) -> [a] -> [f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe f) -> [a] -> [Maybe f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe f
fn ([a] -> [f]) -> [a] -> [f]
forall a b. (a -> b) -> a -> b
$ ValueCtx [a] -> [a]
forall a. ValueCtx a -> a
getValue ValueCtx [a]
v of
[] -> ValueCtx [a] -> VCtx f (ValueCtx [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ValueCtx [a]
v
fs :: [f]
fs -> ValueCtx [a] -> [f] -> VCtx f (ValueCtx [a])
forall a f. ValueCtx a -> [f] -> VCtx f (ValueCtx a)
disputeMany ValueCtx [a]
v [f]
fs
ifEach :: (a -> Either f b) -> ValueCtx [a] -> VCtx f (ValueCtx [b])
ifEach :: (a -> Either f b) -> ValueCtx [a] -> VCtx f (ValueCtx [b])
ifEach fn :: a -> Either f b
fn v :: ValueCtx [a]
v =
let es :: [Either f b]
es = (a -> Either f b) -> [a] -> [Either f b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either f b
fn ([a] -> [Either f b]) -> [a] -> [Either f b]
forall a b. (a -> b) -> a -> b
$ ValueCtx [a] -> [a]
forall a. ValueCtx a -> a
getValue ValueCtx [a]
v
in case [Either f b] -> [f]
forall a b. [Either a b] -> [a]
lefts [Either f b]
es of
[] -> ValueCtx [b] -> VCtx f (ValueCtx [b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ValueCtx [b] -> VCtx f (ValueCtx [b]))
-> ([b] -> ValueCtx [b]) -> [b] -> VCtx f (ValueCtx [b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueCtx [a] -> [b] -> ValueCtx [b]
forall a b. ValueCtx a -> b -> ValueCtx b
setValue ValueCtx [a]
v ([b] -> VCtx f (ValueCtx [b])) -> [b] -> VCtx f (ValueCtx [b])
forall a b. (a -> b) -> a -> b
$ [Either f b] -> [b]
forall a b. [Either a b] -> [b]
rights [Either f b]
es
fs :: [f]
fs -> ValueCtx [a] -> [f] -> VCtx f (ValueCtx [b])
forall a f b. ValueCtx a -> [f] -> VCtx f b
refuteMany ValueCtx [a]
v [f]
fs
ifEachProven :: (a -> Proof f b) -> ValueCtx [a] -> VCtx f (ValueCtx [b])
ifEachProven :: (a -> Proof f b) -> ValueCtx [a] -> VCtx f (ValueCtx [b])
ifEachProven fn :: a -> Proof f b
fn v :: ValueCtx [a]
v =
let p :: Proof f [b]
p = [Proof f [b]] -> Proof f [b]
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Proof f [b]] -> Proof f [b]) -> [Proof f [b]] -> Proof f [b]
forall a b. (a -> b) -> a -> b
$ (a -> Proof f [b]) -> [a] -> [Proof f [b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> [b]) -> Proof f b -> Proof f [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b :: b
b -> [b
b]) (Proof f b -> Proof f [b]) -> (a -> Proof f b) -> a -> Proof f [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Proof f b
fn) ([a] -> [Proof f [b]]) -> [a] -> [Proof f [b]]
forall a b. (a -> b) -> a -> b
$ ValueCtx [a] -> [a]
forall a. ValueCtx a -> a
getValue ValueCtx [a]
v
in case Proof f [b]
p of
Valid es :: [b]
es -> ValueCtx [b] -> VCtx f (ValueCtx [b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ValueCtx [b] -> VCtx f (ValueCtx [b]))
-> ValueCtx [b] -> VCtx f (ValueCtx [b])
forall a b. (a -> b) -> a -> b
$ ValueCtx [a] -> [b] -> ValueCtx [b]
forall a b. ValueCtx a -> b -> ValueCtx b
setValue ValueCtx [a]
v [b]
es
Invalid gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> case ValueCtx [a]
v of
Global _ -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx [b])
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f]
gfs Map [Name] [f]
lfs
Field n :: Name
n _ -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx [b])
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] (Map [Name] [f] -> VCtx f (ValueCtx [b]))
-> Map [Name] [f] -> VCtx f (ValueCtx [b])
forall a b. (a -> b) -> a -> b
$ [Name] -> [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert [Name
n] [f]
gfs Map [Name] [f]
lfs
isMatch :: Eq a => f -> VCtx f a -> ValueCtx a -> VCtx f (ValueCtx a)
isMatch :: f -> VCtx f a -> ValueCtx a -> VCtx f (ValueCtx a)
isMatch f :: f
f (ValidCtx a :: a
a) = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith (f -> a -> a -> Maybe f
forall a f. Eq a => f -> a -> a -> Maybe f
testMatch f
f a
a)
isMatch f :: f
f (DisputedCtx _ _ a :: a
a) = (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
forall a f. (a -> Maybe f) -> ValueCtx a -> VCtx f (ValueCtx a)
disputeWith (f -> a -> a -> Maybe f
forall a f. Eq a => f -> a -> a -> Maybe f
testMatch f
f a
a)
isMatch _ (RefutedCtx _ _) = ValueCtx a -> VCtx f (ValueCtx a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
validateField :: Validatable f a b => ValueCtx a -> VCtx f (ValueCtx b)
validateField :: ValueCtx a -> VCtx f (ValueCtx b)
validateField (Global a :: a
a) = case a -> VCtx f b
forall f a b. Validatable f a b => a -> VCtx f b
validation a
a of
ValidCtx b :: b
b -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. a -> VCtx f a
ValidCtx (b -> ValueCtx b
forall a. a -> ValueCtx a
Global b
b)
DisputedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs b :: b
b -> [f] -> Map [Name] [f] -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [f]
gfs Map [Name] [f]
lfs (b -> ValueCtx b
forall a. a -> ValueCtx a
Global b
b)
RefutedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f]
gfs Map [Name] [f]
lfs
validateField (Field n :: Name
n a :: a
a) = case a -> VCtx f b
forall f a b. Validatable f a b => a -> VCtx f b
validation a
a of
ValidCtx b :: b
b -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. a -> VCtx f a
ValidCtx (Name -> b -> ValueCtx b
forall a. Name -> a -> ValueCtx a
Field Name
n b
b)
DisputedCtx [] lfs :: Map [Name] [f]
lfs b :: b
b -> [f] -> Map [Name] [f] -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [] (([Name] -> [Name]) -> Map [Name] [f] -> Map [Name] [f]
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (\k :: [Name]
k -> [Name
n] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
k) Map [Name] [f]
lfs) (Name -> b -> ValueCtx b
forall a. Name -> a -> ValueCtx a
Field Name
n b
b)
DisputedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs b :: b
b -> [f] -> Map [Name] [f] -> ValueCtx b -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [] ([Name] -> [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert [Name
n] [f]
gfs (Map [Name] [f] -> Map [Name] [f])
-> Map [Name] [f] -> Map [Name] [f]
forall a b. (a -> b) -> a -> b
$ ([Name] -> [Name]) -> Map [Name] [f] -> Map [Name] [f]
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (\k :: [Name]
k -> [Name
n] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
k) Map [Name] [f]
lfs) (Name -> b -> ValueCtx b
forall a. Name -> a -> ValueCtx a
Field Name
n b
b)
RefutedCtx [] lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] (([Name] -> [Name]) -> Map [Name] [f] -> Map [Name] [f]
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (\k :: [Name]
k -> [Name
n] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
k) Map [Name] [f]
lfs)
RefutedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (ValueCtx b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [] ([Name] -> [f] -> Map [Name] [f] -> Map [Name] [f]
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert [Name
n] [f]
gfs (Map [Name] [f] -> Map [Name] [f])
-> Map [Name] [f] -> Map [Name] [f]
forall a b. (a -> b) -> a -> b
$ ([Name] -> [Name]) -> Map [Name] [f] -> Map [Name] [f]
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
mapKeys (\k :: [Name]
k -> [Name
n] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
k) Map [Name] [f]
lfs)
optional :: Maybe a -> (a -> VCtx f b) -> VCtx f (Maybe b)
optional :: Maybe a -> (a -> VCtx f b) -> VCtx f (Maybe b)
optional Nothing _ = Maybe b -> VCtx f (Maybe b)
forall f a. a -> VCtx f a
ValidCtx Maybe b
forall a. Maybe a
Nothing
optional (Just a :: a
a) f :: a -> VCtx f b
f =
case a -> VCtx f b
f a
a of
ValidCtx b :: b
b -> Maybe b -> VCtx f (Maybe b)
forall f a. a -> VCtx f a
ValidCtx (b -> Maybe b
forall a. a -> Maybe a
Just b
b)
DisputedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs b :: b
b -> [f] -> Map [Name] [f] -> Maybe b -> VCtx f (Maybe b)
forall f a. [f] -> Map [Name] [f] -> a -> VCtx f a
DisputedCtx [f]
gfs Map [Name] [f]
lfs (b -> Maybe b
forall a. a -> Maybe a
Just b
b)
RefutedCtx gfs :: [f]
gfs lfs :: Map [Name] [f]
lfs -> [f] -> Map [Name] [f] -> VCtx f (Maybe b)
forall f a. [f] -> Map [Name] [f] -> VCtx f a
RefutedCtx [f]
gfs Map [Name] [f]
lfs
whenJust :: (ValueCtx a -> VCtx f (ValueCtx b)) -> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe b))
whenJust :: (ValueCtx a -> VCtx f (ValueCtx b))
-> ValueCtx (Maybe a) -> VCtx f (ValueCtx (Maybe b))
whenJust fn :: ValueCtx a -> VCtx f (ValueCtx b)
fn v :: ValueCtx (Maybe a)
v = case ValueCtx (Maybe a) -> Maybe a
forall a. ValueCtx a -> a
getValue ValueCtx (Maybe a)
v of
Nothing -> ValueCtx (Maybe b) -> VCtx f (ValueCtx (Maybe b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ValueCtx (Maybe b) -> VCtx f (ValueCtx (Maybe b)))
-> ValueCtx (Maybe b) -> VCtx f (ValueCtx (Maybe b))
forall a b. (a -> b) -> a -> b
$ Maybe b
forall a. Maybe a
Nothing Maybe b -> ValueCtx (Maybe a) -> ValueCtx (Maybe b)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ValueCtx (Maybe a)
v
Just a :: a
a -> (ValueCtx b -> ValueCtx (Maybe b))
-> VCtx f (ValueCtx b) -> VCtx f (ValueCtx (Maybe b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> Maybe b) -> ValueCtx b -> ValueCtx (Maybe b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Maybe b
forall a. a -> Maybe a
Just) (VCtx f (ValueCtx b) -> VCtx f (ValueCtx (Maybe b)))
-> VCtx f (ValueCtx b) -> VCtx f (ValueCtx (Maybe b))
forall a b. (a -> b) -> a -> b
$ ValueCtx a -> VCtx f (ValueCtx b)
fn (ValueCtx a -> VCtx f (ValueCtx b))
-> ValueCtx a -> VCtx f (ValueCtx b)
forall a b. (a -> b) -> a -> b
$ a
a a -> ValueCtx (Maybe a) -> ValueCtx a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ValueCtx (Maybe a)
v
isValid :: Proof f a -> Bool
isValid :: Proof f a -> Bool
isValid (Valid _) = Bool
True
isValid (Invalid _ _) = Bool
False
isInvalid :: Proof f a -> Bool
isInvalid :: Proof f a -> Bool
isInvalid = Bool -> Bool
not (Bool -> Bool) -> (Proof f a -> Bool) -> Proof f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof f a -> Bool
forall f a. Proof f a -> Bool
isValid
flattenProofs :: [Proof f a] -> Proof f [a]
flattenProofs :: [Proof f a] -> Proof f [a]
flattenProofs al :: [Proof f a]
al = [Proof f [a]] -> Proof f [a]
forall a. Monoid a => [a] -> a
mconcat ([Proof f [a]] -> Proof f [a]) -> [Proof f [a]] -> Proof f [a]
forall a b. (a -> b) -> a -> b
$ (a -> [a]) -> Proof f a -> Proof f [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[]) (Proof f a -> Proof f [a]) -> [Proof f a] -> [Proof f [a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Proof f a]
al