-- | Predicates -- -- Intended for qualified import. -- > import Test.Falsify.Predicate (Predicate, (.$)) -- > import qualified Test.Falsify.Predicate as P module Test.Falsify.Predicate ( Predicate -- opaque -- * Expressions , Expr -- opaque , prettyExpr -- * Functions , Fn -- opaque , fn , fnWith , transparent -- * Construction , alwaysPass , alwaysFail , unary , binary -- * Auxiliary construction , satisfies , relatedBy -- * Combinators , dot , split , on , flip , matchEither , matchBool -- * Evaluation and partial evaluation , eval , (.$) , at -- * Specific predicates , eq , ne , lt , le , gt , ge , towards , expect , between , even , odd , elem , pairwise ) where import Prelude hiding (all, flip, even, odd, pred, elem) import qualified Prelude import Data.Bifunctor import Data.Kind import Data.List (intercalate) import Data.Maybe (catMaybes) import Data.SOP (NP(..), K(..), I(..), SListI) import qualified Data.SOP as SOP {------------------------------------------------------------------------------- Small expression language -------------------------------------------------------------------------------} -- | Variable type Var = String -- | Simple expression language -- -- The internal details of this type are (currently) not exposed. data Expr = -- | Variable Var Var -- | Application | App Expr Expr -- | Non-associative infix operator | Infix Var Expr Expr prettyExpr :: Expr -> String prettyExpr :: Expr -> String prettyExpr = Bool -> Expr -> String go Bool False where go :: Bool -- Does the context require brackets? -> Expr -> String go :: Bool -> Expr -> String go Bool needsBrackets = \case Var String x -> String x App Expr e1 Expr e2 -> Bool -> String -> String parensIf Bool needsBrackets forall a b. (a -> b) -> a -> b $ forall a. [a] -> [[a]] -> [a] intercalate String " " [ Bool -> Expr -> String go Bool False Expr e1 -- application is left associative , Bool -> Expr -> String go Bool True Expr e2 ] Infix String op Expr e1 Expr e2 -> Bool -> String -> String parensIf Bool needsBrackets forall a b. (a -> b) -> a -> b $ forall a. [a] -> [[a]] -> [a] intercalate String " " [ Bool -> Expr -> String go Bool True Expr e1 , String op , Bool -> Expr -> String go Bool True Expr e2 ] parensIf :: Bool -> String -> String parensIf :: Bool -> String -> String parensIf Bool False = forall a. a -> a id parensIf Bool True = \String s -> String "(" forall a. [a] -> [a] -> [a] ++ String s forall a. [a] -> [a] -> [a] ++ String ")" {------------------------------------------------------------------------------- Functions -------------------------------------------------------------------------------} -- | Function (used for composition of a 'Predicate' with a function) data Fn a b = -- | Function that is visible in rendered results Visible Var (b -> String) (a -> b) -- | Function that should not be visible in rendered results -- -- See 'transparent' for an example. | Transparent (a -> b) -- | Default constructor for a function fn :: Show b => (Var, a -> b) -> Fn a b fn :: forall b a. Show b => (String, a -> b) -> Fn a b fn (String n, a -> b f) = forall b a. (String, b -> String, a -> b) -> Fn a b fnWith (String n, forall a. Show a => a -> String show, a -> b f) -- | Generalization of 'fn' that does not depend on 'Show' fnWith :: (Var, b -> String, a -> b) -> Fn a b fnWith :: forall b a. (String, b -> String, a -> b) -> Fn a b fnWith (String n, b -> String r, a -> b f) = forall a b. String -> (b -> String) -> (a -> b) -> Fn a b Visible String n b -> String r a -> b f -- | Function that should not be visible in any rendered failure -- -- Consider these two predicates: -- -- > p1, p2 :: Predicate '[Char, Char] -- > p1 = P.eq `P.on` (P.fn "ord" ord) -- > p2 = P.eq `P.on` (P.transparent ord) -- -- Both of these compare two characters on their codepoints (through 'ord'), but -- they result in different failures. The first would give us something like -- -- > (ord x) /= (ord y) -- > x : 'a' -- > y : 'b' -- > ord x: 97 -- > ord y: 98 -- -- whereas the second might give us something like -- -- > x /= y -- > x: 'a' -- > y: 'b' -- -- which of these is more useful is of course application dependent. transparent :: (a -> b) -> Fn a b transparent :: forall a b. (a -> b) -> Fn a b transparent = forall a b. (a -> b) -> Fn a b Transparent {------------------------------------------------------------------------------- Decorated predicate inputs This is internal API. -------------------------------------------------------------------------------} -- | Input to a 'Predicate' data Input x = Input { -- | Expression describing the input forall x. Input x -> Expr inputExpr :: Expr -- | Rendered value of the input , forall x. Input x -> String inputRendered :: String -- | The input proper , forall x. Input x -> x inputValue :: x } -- | Apply function to an argument -- -- If the funciton is visible, we also return the /input/ to the function -- (so that we can render both the input and the output); we return 'Nothing' -- for transparent functions. applyFn :: Fn a b -> Input a -> (Input b, Maybe (Expr, String)) applyFn :: forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, String)) applyFn (Visible String n b -> String r a -> b f) Input a x = ( Input { inputExpr :: Expr inputExpr = Expr -> Expr -> Expr App (String -> Expr Var String n) forall a b. (a -> b) -> a -> b $ forall x. Input x -> Expr inputExpr Input a x , inputRendered :: String inputRendered = b -> String r forall a b. (a -> b) -> a -> b $ a -> b f (forall x. Input x -> x inputValue Input a x) , inputValue :: b inputValue = a -> b f forall a b. (a -> b) -> a -> b $ forall x. Input x -> x inputValue Input a x } , forall a. a -> Maybe a Just forall a b. (a -> b) -> a -> b $ forall x. Input x -> (Expr, String) renderInput Input a x ) applyFn (Transparent a -> b f) Input a x = ( Input { inputExpr :: Expr inputExpr = forall x. Input x -> Expr inputExpr Input a x , inputRendered :: String inputRendered = forall x. Input x -> String inputRendered Input a x , inputValue :: b inputValue = a -> b f forall a b. (a -> b) -> a -> b $ forall x. Input x -> x inputValue Input a x } , forall a. Maybe a Nothing ) renderInput :: Input x -> (Expr, String) renderInput :: forall x. Input x -> (Expr, String) renderInput Input x x = (forall x. Input x -> Expr inputExpr Input x x, forall x. Input x -> String inputRendered Input x x) renderInputs :: SListI xs => NP Input xs -> [(Expr, String)] renderInputs :: forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, String)] renderInputs NP Input xs xs = forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a SOP.hcollapse forall a b. (a -> b) -> a -> b $ forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs SOP.hmap (forall k a (b :: k). a -> K a b K forall b c a. (b -> c) -> (a -> b) -> a -> c . forall x. Input x -> (Expr, String) renderInput) NP Input xs xs {------------------------------------------------------------------------------- Definition 'Predicate' is a relatively deep embedding, so that we can provide more powerful combinators. -------------------------------------------------------------------------------} -- | Error message (when the predicate fails) type Err = String -- | N-ary predicate -- -- A predicate of type -- -- > Predicate '[Int, Bool, Char, ..] -- -- is essentially a function @Int -> Bool -> Char -> .. -> Bool@, along with -- some metadata about that function that allows us to render it in a human -- readable way. In particular, we construct an 'Expr' for the values that the -- predicate has been applied to. data Predicate :: [Type] -> Type where -- | Primitive generator Prim :: (NP I xs -> Bool) -> (NP (K Expr) xs -> Err) -> Predicate xs -- | Predicate that always passes Pass :: Predicate xs -- | Predicate that always fails Fail :: Predicate xs -- | Conjunction Both :: Predicate xs -> Predicate xs -> Predicate xs -- | Abstraction Lam :: (Input x -> Predicate xs) -> Predicate (x ': xs) -- | Partial application At :: Predicate (x : xs) -> Input x -> Predicate xs -- | Function compostion Dot :: Predicate (x' : xs) -> Fn x x' -> Predicate (x : xs) -- | Analogue of 'Control.Arrow.(***)' Split :: Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs) -- | Analogue of 'Prelude.flip' Flip :: Predicate (x : y : zs) -> Predicate (y : x : zs) -- | Choice Choose :: Predicate ( a : xs) -> Predicate ( b : xs) -> Predicate (Either a b : xs) -- | Predicate that ignores its argument Const :: Predicate xs -> Predicate (x ': xs) instance Monoid (Predicate a) where mempty :: Predicate a mempty = forall (a :: [*]). Predicate a Pass instance Semigroup (Predicate a) where <> :: Predicate a -> Predicate a -> Predicate a (<>) = forall (a :: [*]). Predicate a -> Predicate a -> Predicate a Both -- | Primitive way to construct a predicate -- -- This is (currently) not part of the public API. prim :: (NP I xs -> Bool) -- ^ Predicate to check -> (NP (K Expr) xs -> Err) -- ^ Produce error message, given the expressions describing the inputs -> Predicate xs prim :: forall (xs :: [*]). (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> Predicate xs prim = forall (xs :: [*]). (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> Predicate xs Prim {------------------------------------------------------------------------------- Construction -------------------------------------------------------------------------------} -- | Constant 'True' alwaysPass :: Predicate xs alwaysPass :: forall (a :: [*]). Predicate a alwaysPass = forall (a :: [*]). Predicate a Pass -- | Constant 'False' alwaysFail :: Predicate xs alwaysFail :: forall (a :: [*]). Predicate a alwaysFail = forall (a :: [*]). Predicate a Fail -- | Unary predicate -- -- This is essentially a function @a -> Bool@; see 'Predicate' for detailed -- discussion. unary :: (a -> Bool) -- ^ The predicate proper -> (Expr -> Err) -- ^ Error message, given 'Expr' describing the input -> Predicate '[a] unary :: forall a. (a -> Bool) -> (Expr -> String) -> Predicate '[a] unary a -> Bool p Expr -> String msg = forall (xs :: [*]). (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> Predicate xs prim (\(I x x :* NP I xs Nil) -> a -> Bool p x x) (\(K Expr l :* NP (K Expr) xs Nil) -> Expr -> String msg Expr l) -- | Binary predicate -- -- This is essentially a function @a -> b -> Bool@; see 'Predicate' for detailed -- discussion. binary :: (a -> b -> Bool) -- ^ The predicate proper -> (Expr -> Expr -> Err) -- ^ Error message, given 'Expr' describing inputs -> Predicate [a, b] binary :: forall a b. (a -> b -> Bool) -> (Expr -> Expr -> String) -> Predicate '[a, b] binary a -> b -> Bool p Expr -> Expr -> String msg = forall (xs :: [*]). (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> Predicate xs prim (\(I x x :* I x y :* NP I xs Nil) -> a -> b -> Bool p x x x y) (\(K Expr lx :* K Expr ly :* NP (K Expr) xs Nil) -> Expr -> Expr -> String msg Expr lx Expr ly) {------------------------------------------------------------------------------- Auxiliary construction -------------------------------------------------------------------------------} -- | Specialization of 'unary' for unary relations satisfies :: (Var, a -> Bool) -> Predicate '[a] satisfies :: forall a. (String, a -> Bool) -> Predicate '[a] satisfies (String n, a -> Bool p) = forall a. (a -> Bool) -> (Expr -> String) -> Predicate '[a] unary a -> Bool p forall a b. (a -> b) -> a -> b $ \Expr x -> Expr -> String prettyExpr forall a b. (a -> b) -> a -> b $ String -> Expr Var String "not" Expr -> Expr -> Expr `App` (String -> Expr Var String n Expr -> Expr -> Expr `App` Expr x) -- | Specialization of 'binary' for relations relatedBy :: (Var, a -> b -> Bool) -> Predicate [a, b] (String n, a -> b -> Bool p) = forall a b. (a -> b -> Bool) -> (Expr -> Expr -> String) -> Predicate '[a, b] binary a -> b -> Bool p forall a b. (a -> b) -> a -> b $ \Expr x Expr y -> Expr -> String prettyExpr forall a b. (a -> b) -> a -> b $ String -> Expr Var String "not" Expr -> Expr -> Expr `App` (String -> Expr Var String n Expr -> Expr -> Expr `App` Expr x Expr -> Expr -> Expr `App` Expr y) {------------------------------------------------------------------------------- Combinators -------------------------------------------------------------------------------} -- | Function composition (analogue of '(.)') dot :: Predicate (x : xs) -> Fn y x -> Predicate (y : xs) dot :: forall x (xs :: [*]) y. Predicate (x : xs) -> Fn y x -> Predicate (y : xs) dot = forall x (xs :: [*]) y. Predicate (x : xs) -> Fn y x -> Predicate (y : xs) Dot -- | Analogue of 'Control.Arrow.(***)' split :: Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs) split :: forall x' y' (xs :: [*]) x y. Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs) split = forall x' y' (xs :: [*]) x y. Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs) Split -- | Analogue of 'Prelude.on' on :: Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs) on :: forall x (xs :: [*]) y. Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs) on Predicate (x : x : xs) p Fn y x f = Predicate (x : x : xs) p forall x' y' (xs :: [*]) x y. Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs) `split` (Fn y x f, Fn y x f) -- | Analogue of 'Prelude.flip' flip :: Predicate (x : y : zs) -> Predicate (y : x : zs) flip :: forall x y (zs :: [*]). Predicate (x : y : zs) -> Predicate (y : x : zs) flip = forall x y (zs :: [*]). Predicate (x : y : zs) -> Predicate (y : x : zs) Flip -- | Match on the argument, and apply whichever predicate is applicable. matchEither :: Predicate (a : xs) -> Predicate (b : xs) -> Predicate (Either a b : xs) matchEither :: forall a (xs :: [*]) b. Predicate (a : xs) -> Predicate (b : xs) -> Predicate (Either a b : xs) matchEither = forall a (xs :: [*]) b. Predicate (a : xs) -> Predicate (b : xs) -> Predicate (Either a b : xs) Choose -- | Conditional -- -- This is a variation on 'choose' that provides no evidence for which branch is -- taken. matchBool :: Predicate xs -- ^ Predicate to evaluate if the condition is true -> Predicate xs -- ^ Predicate to evaluate if the condition is false -> Predicate (Bool : xs) matchBool :: forall (xs :: [*]). Predicate xs -> Predicate xs -> Predicate (Bool : xs) matchBool Predicate xs t Predicate xs f = forall a (xs :: [*]) b. Predicate (a : xs) -> Predicate (b : xs) -> Predicate (Either a b : xs) matchEither (forall (x :: [*]) xs. Predicate x -> Predicate (xs : x) Const Predicate xs t) (forall (x :: [*]) xs. Predicate x -> Predicate (xs : x) Const Predicate xs f) forall x (xs :: [*]) y. Predicate (x : xs) -> Fn y x -> Predicate (y : xs) `dot` forall a b. (a -> b) -> Fn a b transparent Bool -> Either () () fromBool where fromBool :: Bool -> Either () () fromBool :: Bool -> Either () () fromBool Bool True = forall a b. a -> Either a b Left () fromBool Bool False = forall a b. b -> Either a b Right () {------------------------------------------------------------------------------- Failures -------------------------------------------------------------------------------} data Failure = Failure { Failure -> String failureErr :: Err , Failure -> [(Expr, String)] failureInputs :: [(Expr, String)] } addInputs :: [(Expr, String)] -> Failure -> Failure addInputs :: [(Expr, String)] -> Failure -> Failure addInputs [(Expr, String)] new Failure{String failureErr :: String failureErr :: Failure -> String failureErr, [(Expr, String)] failureInputs :: [(Expr, String)] failureInputs :: Failure -> [(Expr, String)] failureInputs} = Failure{ String failureErr :: String failureErr :: String failureErr , failureInputs :: [(Expr, String)] failureInputs = [(Expr, String)] new forall a. [a] -> [a] -> [a] ++ [(Expr, String)] failureInputs } prettyFailure :: Failure -> String prettyFailure :: Failure -> String prettyFailure Failure{String failureErr :: String failureErr :: Failure -> String failureErr, [(Expr, String)] failureInputs :: [(Expr, String)] failureInputs :: Failure -> [(Expr, String)] failureInputs} = [String] -> String unlines forall a b. (a -> b) -> a -> b $ String failureErr forall a. a -> [a] -> [a] : forall a b. (a -> b) -> [a] -> [b] map (forall a b c. (a -> b -> c) -> (a, b) -> c uncurry Expr -> String -> String padInput) [(Expr, String)] failureInputs where maxLabelLen :: Int maxLabelLen :: Int maxLabelLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a maximum forall a b. (a -> b) -> a -> b $ forall a b. (a -> b) -> [a] -> [b] map (forall (t :: * -> *) a. Foldable t => t a -> Int length forall b c a. (b -> c) -> (a -> b) -> a -> c . Expr -> String prettyExpr forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a b. (a, b) -> a fst) [(Expr, String)] failureInputs padInput :: Expr -> String -> String padInput :: Expr -> String -> String padInput Expr e String v = Int -> String -> String padTo Int maxLabelLen (Expr -> String prettyExpr Expr e) forall a. [a] -> [a] -> [a] ++ String ": " forall a. [a] -> [a] -> [a] ++ String v padTo :: Int -> String -> String padTo :: Int -> String -> String padTo Int n String xs = String xs forall a. [a] -> [a] -> [a] ++ forall a. Int -> a -> [a] replicate (Int n forall a. Num a => a -> a -> a - forall (t :: * -> *) a. Foldable t => t a -> Int length String xs) Char ' ' {------------------------------------------------------------------------------- Generalized evaluation This is internal API. Only the top-level 'eval' is exported. -------------------------------------------------------------------------------} evalPrim :: SListI xs => (NP I xs -> Bool) -> (NP (K Expr) xs -> Err) -> NP Input xs -> Either Failure () evalPrim :: forall (xs :: [*]). SListI xs => (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> NP Input xs -> Either Failure () evalPrim NP I xs -> Bool p NP (K Expr) xs -> String err NP Input xs xs | NP I xs -> Bool p (forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs SOP.hmap (forall a. a -> I a I forall b c a. (b -> c) -> (a -> b) -> a -> c . forall x. Input x -> x inputValue) NP Input xs xs) = forall a b. b -> Either a b Right () | Bool otherwise = forall a b. a -> Either a b Left Failure { failureErr :: String failureErr = NP (K Expr) xs -> String err forall a b. (a -> b) -> a -> b $ forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs SOP.hmap (forall k a (b :: k). a -> K a b K forall b c a. (b -> c) -> (a -> b) -> a -> c . forall x. Input x -> Expr inputExpr) NP Input xs xs , failureInputs :: [(Expr, String)] failureInputs = forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, String)] renderInputs NP Input xs xs } evalLam :: SListI xs => (Input x -> Predicate xs) -> NP Input (x : xs) -> Either Failure () evalLam :: forall (xs :: [*]) x. SListI xs => (Input x -> Predicate xs) -> NP Input (x : xs) -> Either Failure () evalLam Input x -> Predicate xs f (Input x x :* NP Input xs xs) = forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ([(Expr, String)] -> Failure -> Failure addInputs [forall x. Input x -> (Expr, String) renderInput Input x x]) forall a b. (a -> b) -> a -> b $ forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt (Input x -> Predicate xs f Input x x) NP Input xs xs evalDot :: SListI xs => Predicate (x : xs) -> Fn y x -> NP Input (y : xs) -> Either Failure () evalDot :: forall (xs :: [*]) x y. SListI xs => Predicate (x : xs) -> Fn y x -> NP Input (y : xs) -> Either Failure () evalDot Predicate (x : xs) p Fn y x f (Input x x :* NP Input xs xs) = forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ([(Expr, String)] -> Failure -> Failure addInputs forall a b. (a -> b) -> a -> b $ forall a. [Maybe a] -> [a] catMaybes [Maybe (Expr, String) x']) forall a b. (a -> b) -> a -> b $ forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (x : xs) p (Input x y forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input xs xs) where (Input x y, Maybe (Expr, String) x') = forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, String)) applyFn Fn y x f Input x x evalSplit :: SListI xs => Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> NP Input (x : y : xs) -> Either Failure () evalSplit :: forall (xs :: [*]) x' y' x y. SListI xs => Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> NP Input (x : y : xs) -> Either Failure () evalSplit Predicate (x' : y' : xs) p (Fn x x' f, Fn y y' g) (Input x x :* Input x y :* NP Input xs xs) = forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ([(Expr, String)] -> Failure -> Failure addInputs forall a b. (a -> b) -> a -> b $ forall a. [Maybe a] -> [a] catMaybes [Maybe (Expr, String) inp_x, Maybe (Expr, String) inp_y]) forall a b. (a -> b) -> a -> b $ forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (x' : y' : xs) p (Input x' x' forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* Input y' y' forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input xs xs) where (Input x' x', Maybe (Expr, String) inp_x) = forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, String)) applyFn Fn x x' f Input x x (Input y' y', Maybe (Expr, String) inp_y) = forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, String)) applyFn Fn y y' g Input x y evalChoice :: SListI xs => Predicate (a : xs) -> Predicate (b : xs) -> NP Input (Either a b : xs) -> Either Failure () evalChoice :: forall (xs :: [*]) a b. SListI xs => Predicate (a : xs) -> Predicate (b : xs) -> NP Input (Either a b : xs) -> Either Failure () evalChoice Predicate (a : xs) t Predicate (b : xs) f (Input x x :* NP Input xs xs) = forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ([(Expr, String)] -> Failure -> Failure addInputs [forall x. Input x -> (Expr, String) renderInput Input x x]) forall a b. (a -> b) -> a -> b $ case forall x. Input x -> x inputValue Input x x of Left a a -> forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (a : xs) t (Input x x{inputValue :: a inputValue = a a} forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input xs xs) Right b b -> forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (b : xs) f (Input x x{inputValue :: b inputValue = b b} forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input xs xs) evalAt :: SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt :: forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt (Prim NP I xs -> Bool p NP (K Expr) xs -> String err) NP Input xs xs = forall (xs :: [*]). SListI xs => (NP I xs -> Bool) -> (NP (K Expr) xs -> String) -> NP Input xs -> Either Failure () evalPrim NP I xs -> Bool p NP (K Expr) xs -> String err NP Input xs xs evalAt Predicate xs Pass NP Input xs _ = forall (m :: * -> *) a. Monad m => a -> m a return () evalAt Predicate xs Fail NP Input xs xs = forall a b. a -> Either a b Left forall a b. (a -> b) -> a -> b $ String -> [(Expr, String)] -> Failure Failure String "Fail" (forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, String)] renderInputs NP Input xs xs) evalAt (Both Predicate xs p1 Predicate xs p2) NP Input xs xs = forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate xs p1 NP Input xs xs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate xs p2 NP Input xs xs evalAt (Lam Input x -> Predicate xs f) NP Input xs xs = forall (xs :: [*]) x. SListI xs => (Input x -> Predicate xs) -> NP Input (x : xs) -> Either Failure () evalLam Input x -> Predicate xs f NP Input xs xs evalAt (Predicate (x : xs) p `At` Input x x) NP Input xs xs = forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (x : xs) p (Input x x forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input xs xs) evalAt (Predicate (x' : xs) p `Dot` Fn x x' f) NP Input xs xs = forall (xs :: [*]) x y. SListI xs => Predicate (x : xs) -> Fn y x -> NP Input (y : xs) -> Either Failure () evalDot Predicate (x' : xs) p Fn x x' f NP Input xs xs evalAt (Predicate (x' : y' : xs) p `Split` (Fn x x' f, Fn y y' g)) NP Input xs xs = forall (xs :: [*]) x' y' x y. SListI xs => Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> NP Input (x : y : xs) -> Either Failure () evalSplit Predicate (x' : y' : xs) p (Fn x x' f, Fn y y' g) NP Input xs xs evalAt (Flip Predicate (x : y : zs) p) NP Input xs xs = let (Input y Input x x :* Input x Input x y :* NP Input zs NP Input xs zs) = NP Input xs xs in forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate (x : y : zs) p (Input x y forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* Input y x forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x : xs) :* NP Input zs zs) evalAt (Choose Predicate (a : xs) l Predicate (b : xs) r) NP Input xs xs = forall (xs :: [*]) a b. SListI xs => Predicate (a : xs) -> Predicate (b : xs) -> NP Input (Either a b : xs) -> Either Failure () evalChoice Predicate (a : xs) l Predicate (b : xs) r NP Input xs xs evalAt (Const Predicate xs p) NP Input xs xs = forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate xs p (forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> NP f xs SOP.tl NP Input xs xs) {------------------------------------------------------------------------------- Evaluation and partial evaluation -------------------------------------------------------------------------------} -- | Evaluate fully applied predicate eval :: Predicate '[] -> Either Err () eval :: Predicate '[] -> Either String () eval Predicate '[] p = forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first Failure -> String prettyFailure forall a b. (a -> b) -> a -> b $ forall (xs :: [*]). SListI xs => Predicate xs -> NP Input xs -> Either Failure () evalAt Predicate '[] p forall {k} (a :: k -> *). NP a '[] Nil -- | Infix version of 'at' -- -- Typical usage example: -- -- > assert $ -- > P.relatedBy ("equiv", equiv) -- > .$ ("x", x) -- > .$ ("y", y) (.$) :: Show x => Predicate (x : xs) -> (Var, x) -> Predicate xs Predicate (x : xs) p .$ :: forall x (xs :: [*]). Show x => Predicate (x : xs) -> (String, x) -> Predicate xs .$ (String n, x x) = Predicate (x : xs) p forall x (xs :: [*]). Predicate (x : xs) -> (Expr, String, x) -> Predicate xs `at` (String -> Expr Var String n, forall a. Show a => a -> String show x x, x x) -- | Generation of '(.$)' that does not require a 'Show' instance at :: Predicate (x : xs) -> (Expr, String, x) -- ^ Renderded name, expression, and input proper -> Predicate xs Predicate (x : xs) p at :: forall x (xs :: [*]). Predicate (x : xs) -> (Expr, String, x) -> Predicate xs `at` (Expr e, String r, x x) = Predicate (x : xs) p forall x (xs :: [*]). Predicate (x : xs) -> Input x -> Predicate xs `At` (forall x. Expr -> String -> x -> Input x Input Expr e String r x x) {------------------------------------------------------------------------------- Specific predicates -------------------------------------------------------------------------------} -- | Construct predicate corresponding to some infix operator -- -- This is an internal auxiliary. binaryInfix :: Var -- ^ Infix operator corresponding to the relation /NOT/ holding -> (a -> b -> Bool) -> Predicate [a, b] binaryInfix :: forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String op a -> b -> Bool f = forall a b. (a -> b -> Bool) -> (Expr -> Expr -> String) -> Predicate '[a, b] binary a -> b -> Bool f forall a b. (a -> b) -> a -> b $ \Expr x Expr y -> Expr -> String prettyExpr (String -> Expr -> Expr -> Expr Infix String op Expr x Expr y) -- | Equal eq :: Eq a => Predicate [a, a] eq :: forall a. Eq a => Predicate '[a, a] eq = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String "/=" forall a. Eq a => a -> a -> Bool (==) -- | Not equal ne :: Eq a => Predicate [a, a] ne :: forall a. Eq a => Predicate '[a, a] ne = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String "==" forall a. Eq a => a -> a -> Bool (/=) -- | (Strictly) less than lt :: Ord a => Predicate [a, a] lt :: forall a. Ord a => Predicate '[a, a] lt = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String ">=" forall a. Ord a => a -> a -> Bool (<) -- | Less than or equal to le :: Ord a => Predicate [a, a] le :: forall a. Ord a => Predicate '[a, a] le = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String ">" forall a. Ord a => a -> a -> Bool (<=) -- | (Strictly) greater than gt :: Ord a => Predicate [a, a] gt :: forall a. Ord a => Predicate '[a, a] gt = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String "<=" forall a. Ord a => a -> a -> Bool (>) -- | Greater than or equal to ge :: Ord a => Predicate [a, a] ge :: forall a. Ord a => Predicate '[a, a] ge = forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix String "<" forall a. Ord a => a -> a -> Bool (>=) -- | Check that values get closed to the specified target towards :: forall a. (Show a, Ord a, Num a) => a -> Predicate [a, a] towards :: forall a. (Show a, Ord a, Num a) => a -> Predicate '[a, a] towards = \a target -> Predicate '[a, a, a] pred forall x (xs :: [*]). Show x => Predicate (x : xs) -> (String, x) -> Predicate xs .$ (String "target", a target) where pred :: Predicate [a, a, a] pred :: Predicate '[a, a, a] pred = forall x (xs :: [*]). (Input x -> Predicate xs) -> Predicate (x : xs) Lam forall a b. (a -> b) -> a -> b $ \Input a target -> forall a. Ord a => Predicate '[a, a] ge forall x (xs :: [*]) y. Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs) `on` forall b a. Show b => (String, a -> b) -> Fn a b fn (String "distanceToTarget", a -> a -> a distanceTo (forall x. Input x -> x inputValue Input a target)) distanceTo :: a -> a -> a distanceTo :: a -> a -> a distanceTo a target a x | a x forall a. Ord a => a -> a -> Bool <= a target = a target forall a. Num a => a -> a -> a - a x | Bool otherwise = a x forall a. Num a => a -> a -> a - a target -- | Specialization of 'eq', useful when expecting a specific value in a test expect :: (Show a, Eq a) => a -> Predicate '[a] expect :: forall a. (Show a, Eq a) => a -> Predicate '[a] expect a x = forall a. Eq a => Predicate '[a, a] eq forall x (xs :: [*]). Show x => Predicate (x : xs) -> (String, x) -> Predicate xs .$ (String "expected", a x) -- | Check that @lo <= x <= hi@ between :: (Show a, Ord a) => a -> a -> Predicate '[a] between :: forall a. (Show a, Ord a) => a -> a -> Predicate '[a] between a lo a hi = forall a. Monoid a => [a] -> a mconcat [ forall a. Ord a => Predicate '[a, a] le forall x (xs :: [*]). Show x => Predicate (x : xs) -> (String, x) -> Predicate xs .$ (String "lo", a lo) , forall x y (zs :: [*]). Predicate (x : y : zs) -> Predicate (y : x : zs) flip forall a. Ord a => Predicate '[a, a] le forall x (xs :: [*]). Show x => Predicate (x : xs) -> (String, x) -> Predicate xs .$ (String "hi", a hi) ] -- | Number is even even :: Integral a => Predicate '[a] even :: forall a. Integral a => Predicate '[a] even = forall a. (String, a -> Bool) -> Predicate '[a] satisfies (String "even", forall a. Integral a => a -> Bool Prelude.even) -- | Number is odd odd :: Integral a => Predicate '[a] odd :: forall a. Integral a => Predicate '[a] odd = forall a. (String, a -> Bool) -> Predicate '[a] satisfies (String "odd ", forall a. Integral a => a -> Bool Prelude.odd) -- | Membership check elem :: Eq a => Predicate [[a], a] elem :: forall a. Eq a => Predicate '[[a], a] elem = forall x y (zs :: [*]). Predicate (x : y : zs) -> Predicate (y : x : zs) flip forall a b. (a -> b) -> a -> b $ forall a b. String -> (a -> b -> Bool) -> Predicate '[a, b] binaryInfix (String "`notElem`") forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool Prelude.elem -- | Apply predicate to every pair of consecutive elements in the list pairwise :: forall a. Show a => Predicate [a, a] -> Predicate '[[a]] pairwise :: forall a. Show a => Predicate '[a, a] -> Predicate '[[a]] pairwise Predicate '[a, a] p = forall x (xs :: [*]). (Input x -> Predicate xs) -> Predicate (x : xs) Lam forall a b. (a -> b) -> a -> b $ \Input [a] xs -> forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap (forall a b c. (a -> b -> c) -> (a, b) -> c uncurry forall a b. (a -> b) -> a -> b $ Expr -> (Word, a) -> (Word, a) -> Predicate '[] pred (forall x. Input x -> Expr inputExpr Input [a] xs)) (forall x. [x] -> [(x, x)] pairs forall a b. (a -> b) -> a -> b $ forall a b. [a] -> [b] -> [(a, b)] zip [Word 0..] (forall x. Input x -> x inputValue Input [a] xs)) where pairs :: forall x. [x] -> [(x, x)] pairs :: forall x. [x] -> [(x, x)] pairs [] = [] pairs [x _] = [] pairs (x x : x y : [x] zs) = (x x, x y) forall a. a -> [a] -> [a] : forall x. [x] -> [(x, x)] pairs (x y forall a. a -> [a] -> [a] : [x] zs) pred :: Expr -> (Word, a) -> (Word, a) -> Predicate '[] pred :: Expr -> (Word, a) -> (Word, a) -> Predicate '[] pred Expr xs (Word i, a x) (Word j, a y) = Predicate '[a, a] p forall x (xs :: [*]). Predicate (x : xs) -> (Expr, String, x) -> Predicate xs `at` (String -> Expr -> Expr -> Expr Infix String "!!" Expr xs (String -> Expr Var forall a b. (a -> b) -> a -> b $ forall a. Show a => a -> String show Word i), forall a. Show a => a -> String show a x, a x) forall x (xs :: [*]). Predicate (x : xs) -> (Expr, String, x) -> Predicate xs `at` (String -> Expr -> Expr -> Expr Infix String "!!" Expr xs (String -> Expr Var forall a b. (a -> b) -> a -> b $ forall a. Show a => a -> String show Word j), forall a. Show a => a -> String show a y, a y)