{-# LANGUAGE OverloadedStrings #-}

-- | Predicates
--
-- Intended for qualified import.
--
-- > import Test.Falsify
-- > import qualified Test.Falsify.Predicate as P
--
-- = Motivation
--
-- Testing libraries must have a way to assert and check intended-to-be-true
-- facts. For example, suppose we have
--
-- > x, y :: Int
-- > x = 5
-- > y = 10
--
-- and we want to assert that @x@ and @y@ are equal. The simplest form that this
-- might take is simply a boolean predicate; for example, @tasty-hunit@ offers
-- [@assertBool@](https://hackage-content.haskell.org/package/tasty-hunit-0.10.2/docs/Test-Tasty-HUnit.html#v:assertBool),
-- and in @QuickCheck@ we have a
-- [@Testable@](https://hackage-content.haskell.org/package/QuickCheck-2.18.0.0/docs/Test-QuickCheck.html#t:Testable)
-- instance for 'Bool'. This allows us to write
--
-- > test_hunit_bool :: HUnit.Assertion
-- > test_hunit_bool = HUnit.assertBool "uhoh" $ x == y
-- >
-- > test_qc_bool :: QuickCheck.Property
-- > test_qc_bool = QuickCheck.property $ x == y
--
-- However, when such a property fails we don't get very useful output; we are
-- merely told /that/ the property failed. Both @tasty-hunit@ and @QuickCheck@
-- offer limited support for producing nicer test ouput; in the specific case of
-- equality, we can write
--
-- > test_hunit_equal :: HUnit.Assertion
-- > test_hunit_equal = HUnit.assertEqual "uhoh" x y
-- >
-- > test_qc_equal :: QuickCheck.Property
-- > test_qc_equal = QuickCheck.property $ x QuickCheck.=== y
--
-- instead, which would produce output
--
-- > uhoh
-- > expected: 5
-- >  but got: 10 (expected failure)
--
-- and
--
-- > *** Failed! Falsified (after 1 test):
-- > 5 /= 10
--
-- respectively, where we are not only told that the property failed, but also
-- /how/; in this case, what the values of @x@ and @y@ are. /Predicates/ in
-- @falsify@ as a generalization of this concept.
--
-- = Introduction to predicates
--
-- Think of a predicate of type 'Predicate' @'[a, b, ..]@ as a function
-- @a -> b -> .. -> Bool@, which can additionally produce useful test output
-- when the predicate does not hold. In order be able to produce that output, a
-- predicate is equipped with a function to generate a description of the
-- failure, given a description of the inputs; those inputs are described by
-- /expressions/ ('Expr'). For example, here is a very simple way in which we
-- might define a predicate to check that its argument is 'even':
--
-- > even1 :: Integral a => Predicate '[a]
-- > even1 = P.unary even $ \a -> "not even: " ++ P.prettyExpr a
--
-- When a predicate is applied to an argument, it must be told how to /name/
-- that argument, how to /render/ the argument, and the /value/ of the argument.
-- For example,
--
-- > test_even1 :: Property ()
-- > test_even1 = assert $ even1 `P.at` ("x", show x, x)
--
-- will result in
--
-- >  even1:   FAIL
-- >    failed after 0 shrinks
-- >    not even: x
-- >    x: 5
--
-- Typically we will use 'show' to render the argument, in which case we can
-- use '.$':
--
-- > test_even2 :: Property ()
-- > test_even2 = assert $ even1 .$ ("x", x)
--
-- This scales nicely to any number of arguments; for example, to come back the
-- equality example from the previous section:
--
-- > test_equal :: Property ()
-- > test_equal = assert $
-- >     P.eq .$ ("x", x)
-- >          .$ ("y", y)
--
-- will produce
--
-- > equal:   FAIL
-- >   failed after 0 shrinks
-- >   x /= y
-- >   x: 5
-- >   y: 10
--
-- = Compositionality
--
-- Suppose that we want to verify that @x@ and @y@ have the same polarity (both
-- are even or both are odd). We /could/ use 'eq' again:
--
-- > test_samePolarity1 :: Property ()
-- > test_samePolarity1 = assert $
-- >     P.eq .$ ("even x", even x)
-- >          .$ ("even y", even y)
--
-- but if we run that, we get
--
-- >  samePolarity1: FAIL
-- >    failed after 0 shrinks
-- >    even x /= even y
-- >    even x: False
-- >    even y: True
--
-- In order to debug the problem, we might like to the value of @x@ and @y@, not
-- just whether they are even or not. We could instead define a custom predicate
-- specifically for this purpose:
--
-- > samePolarity :: Integral a => Predicate '[a, a]
-- > samePolarity =
-- >     P.binary
-- >       (\a b -> even a == even b)
-- >       (\a b -> P.prettyExpr a ++ " and " ++ P.prettyExpr b ++ " have different polarity")
-- >
-- > test_samePolarity2 :: Property ()
-- > test_samePolarity2 = assert $ samePolarity .$ ("x", x) .$ ("y", y)
--
-- which would produce
--
-- > samePolarity2: FAIL
-- >   failed after 0 shrinks
-- >   x and y have different polarity
-- >   x: 5
-- >   y: 10
--
-- but now we have the opposite problem: we see the values of @x@ and @y@, but
-- not their polarity. Fortunately, we can take advantage of the
-- compositionality of predicates, and state very directly that the function
-- 'even', applied 'on' both arguments, must produce the same result:
--
-- > samePolarity' :: Integral a => Predicate '[a, a]
-- > samePolarity' = P.eq `P.on` P.fn ("even", even)
-- >
-- > test_samePolarity3 :: Property ()
-- > test_samePolarity3 = assert $
-- >     samePolarity'
-- >       .$ ("x", x)
-- >       .$ ("y", y)
--
-- produces
--
-- > samePolarity3: FAIL
-- >   failed after 0 shrinks
-- >   (even x) /= (even y)
-- >   x     : 5
-- >   y     : 10
-- >   even x: False
-- >   even y: True
--
-- Occassionally it is useful to suppress the results of functions applications;
-- for example, suppose we have
--
-- > newtype T = WrapT Int
-- >   deriving stock (Show)
-- >
-- > unwrapT :: T -> Int
-- > unwrapT (WrapT a) = a
--
-- and we want to check whether @X 5@ and @X 10@ have the same polarity; in this
-- case, there isn't much point explicitly including the output of @unwrapT@,
-- so we can suppress it with 'transparent':
--
-- > test_samePolarity4 :: Property ()
-- > test_samePolarity4 = assert $
-- >     samePolarity' `P.on` P.transparent unwrapT
-- >       .$ ("x", WrapT 5)
-- >       .$ ("y", WrapT 10)
--
-- = N-ary predicates
--
-- Most predicates are either 'unary' or 'binary'; these can usually easily be
-- defined using 'satisfies' and 'relatedBy' respectively, which will take care
-- of producing a nice error message. In the general case you can construct
-- predicates of arbitrary arity using 'lam', 'pass' and 'fail', though in that
-- case you will be responsible for constructing your own error messages.
--
-- For example, suppose we have a "real" implementation of some kind of security
-- policy implementation as well as a "model" implementation:
--
-- > applyReal, applyModel :: Policy -> Operation -> Resource -> Actor -> Bool
--
-- Then we could define a predicate that compares these two as follows:
--
-- > realVsModel :: Predicate '[Policy, Operation, Resource, Actor]
-- > realVsModel = P.lam $ \p -> P.lam $ \o -> P.lam $ \r -> P.lam $ \a ->
-- >     let real  = applyReal  p o r a
-- >         model = applyModel p o r a
-- >     in if real == model then
-- >          P.pass
-- >        else
-- >          P.fail $ "real says " ++ show real ++ ", model says " ++ show model
--
-- Such a predicate can then be used like any other, and rendering of the
-- arguments /to/ the predicate is handled automatically. For example:
--
-- > test_realVsModel :: Property ()
-- > test_realVsModel = assert $
-- >     realVsModel
-- >       .$ ( "policy"    , policy    )
-- >       .$ ( "operation" , operation )
-- >       .$ ( "resource"  , resource  )
-- >       .$ ( "actor"     , actor     )
--
-- (Usually of course these inputs would be randomly generated.) This property
-- might result in
--
-- > realVsModel: FAIL
-- >   failed after 0 shrinks
-- >   real says False, model says True
-- >   policy   : "strict"
-- >   operation: "delete"
-- >   resource : "db"
-- >   actor    : "joe"
module Test.Falsify.Predicate (
    Predicate -- opaque
    -- * Expressions
  , Expr -- opaque
  , prettyExpr
    -- * Functions
  , Fn     -- opaque
  , FnName -- opaque
  , fn
  , fnWith
  , transparent
    -- * Construction
  , pass
  , fail
  , unary
  , binary
    -- * Auxiliary construction
  , satisfies
  , relatedBy
    -- * Combinators
  , dot
  , split
  , on
  , flip
  , matchEither
  , matchBool
  , lam
    -- * Evaluation and partial evaluation
  , VarName -- opaque
  , Err
  , 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, fail)
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 Data.String

import qualified Data.SOP as SOP

{-------------------------------------------------------------------------------
  Small expression language
-------------------------------------------------------------------------------}

-- | Variable
newtype VarName = WrapVarName{
      VarName -> [Char]
unwrapVarName :: String
    }
  deriving newtype ([Char] -> VarName
([Char] -> VarName) -> IsString VarName
forall a. ([Char] -> a) -> IsString a
$cfromString :: [Char] -> VarName
fromString :: [Char] -> VarName
IsString)

-- | Simple expression language
--
-- The internal details of this type are (currently) not exposed.
data Expr =
    -- | Variable
    Var VarName

    -- | Function
    --
    -- We distinguish between v'Var' and v'Fn' only for improved readability.
  | Fn FnName

    -- | Application
  | App Expr Expr

    -- | Non-associative infix operator
  | Infix FnName Expr Expr

-- | Pretty-print expression
prettyExpr :: Expr -> String
prettyExpr :: Expr -> [Char]
prettyExpr = Bool -> Expr -> [Char]
go Bool
False
  where
    go ::
         Bool -- Does the context require brackets?
      -> Expr -> String
    go :: Bool -> Expr -> [Char]
go Bool
needsBrackets = \case
        Var VarName
x          -> VarName -> [Char]
unwrapVarName VarName
x
        Fn FnName
f           -> FnName -> [Char]
unwrapFnName FnName
f
        App Expr
e1 Expr
e2      -> Bool -> [Char] -> [Char]
parensIf Bool
needsBrackets ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " [
                              Bool -> Expr -> [Char]
go Bool
False Expr
e1 -- application is left associative
                            , Bool -> Expr -> [Char]
go Bool
True  Expr
e2
                            ]
        Infix FnName
op Expr
e1 Expr
e2 -> Bool -> [Char] -> [Char]
parensIf Bool
needsBrackets ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " [
                              Bool -> Expr -> [Char]
go Bool
True Expr
e1
                            , FnName -> [Char]
unwrapFnName FnName
op
                            , Bool -> Expr -> [Char]
go Bool
True Expr
e2
                            ]

    parensIf :: Bool -> String -> String
    parensIf :: Bool -> [Char] -> [Char]
parensIf Bool
False = [Char] -> [Char]
forall a. a -> a
id
    parensIf Bool
True  = \[Char]
s -> [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

{-------------------------------------------------------------------------------
  Functions
-------------------------------------------------------------------------------}

-- | Function name
newtype FnName = WrapFnName{
      FnName -> [Char]
unwrapFnName :: String
    }
  deriving newtype ([Char] -> FnName
([Char] -> FnName) -> IsString FnName
forall a. ([Char] -> a) -> IsString a
$cfromString :: [Char] -> FnName
fromString :: [Char] -> FnName
IsString)

-- | Function (used for composition of a 'Predicate' with a function)
data Fn a b =
    -- | Function that is visible in rendered results
    Visible FnName (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 => (FnName, a -> b) -> Fn a b
fn :: forall b a. Show b => (FnName, a -> b) -> Fn a b
fn (FnName
n, a -> b
f) = (FnName, b -> [Char], a -> b) -> Fn a b
forall b a. (FnName, b -> [Char], a -> b) -> Fn a b
fnWith (FnName
n, b -> [Char]
forall a. Show a => a -> [Char]
show, a -> b
f)

-- | Generalization of 'fn' that does not depend on 'Show'
fnWith :: (FnName, b -> String, a -> b) -> Fn a b
fnWith :: forall b a. (FnName, b -> [Char], a -> b) -> Fn a b
fnWith (FnName
n, b -> [Char]
r, a -> b
f) = FnName -> (b -> [Char]) -> (a -> b) -> Fn a b
forall a b. FnName -> (b -> [Char]) -> (a -> b) -> Fn a b
Visible FnName
n b -> [Char]
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 = (a -> b) -> Fn a b
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 -> [Char]
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, [Char]))
applyFn (Visible FnName
n b -> [Char]
r a -> b
f) Input a
x = (
      Input {
          inputExpr :: Expr
inputExpr     = Expr -> Expr -> Expr
App (FnName -> Expr
Fn FnName
n) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Input a -> Expr
forall x. Input x -> Expr
inputExpr Input a
x
        , inputRendered :: [Char]
inputRendered = b -> [Char]
r (b -> [Char]) -> b -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> b
f (Input a -> a
forall x. Input x -> x
inputValue Input a
x)
        , inputValue :: b
inputValue    = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Input a -> a
forall x. Input x -> x
inputValue Input a
x
        }
    , (Expr, [Char]) -> Maybe (Expr, [Char])
forall a. a -> Maybe a
Just ((Expr, [Char]) -> Maybe (Expr, [Char]))
-> (Expr, [Char]) -> Maybe (Expr, [Char])
forall a b. (a -> b) -> a -> b
$ Input a -> (Expr, [Char])
forall x. Input x -> (Expr, [Char])
renderInput Input a
x
    )
applyFn (Transparent a -> b
f) Input a
x = (
      Input {
          inputExpr :: Expr
inputExpr     = Input a -> Expr
forall x. Input x -> Expr
inputExpr Input a
x
        , inputRendered :: [Char]
inputRendered = Input a -> [Char]
forall x. Input x -> [Char]
inputRendered Input a
x
        , inputValue :: b
inputValue    = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Input a -> a
forall x. Input x -> x
inputValue Input a
x
        }
    , Maybe (Expr, [Char])
forall a. Maybe a
Nothing
    )

renderInput :: Input x -> (Expr, String)
renderInput :: forall x. Input x -> (Expr, [Char])
renderInput Input x
x = (Input x -> Expr
forall x. Input x -> Expr
inputExpr Input x
x, Input x -> [Char]
forall x. Input x -> [Char]
inputRendered Input x
x)

renderInputs :: SListI xs => NP Input xs -> [(Expr, String)]
renderInputs :: forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, [Char])]
renderInputs NP Input xs
xs = NP (K (Expr, [Char])) xs -> CollapseTo NP (Expr, [Char])
forall (xs :: [*]) a.
SListIN NP xs =>
NP (K a) xs -> CollapseTo NP a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
SOP.hcollapse (NP (K (Expr, [Char])) xs -> CollapseTo NP (Expr, [Char]))
-> NP (K (Expr, [Char])) xs -> CollapseTo NP (Expr, [Char])
forall a b. (a -> b) -> a -> b
$ (forall a. Input a -> K (Expr, [Char]) a)
-> NP Input xs -> NP (K (Expr, [Char])) xs
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 ((Expr, [Char]) -> K (Expr, [Char]) a
forall k a (b :: k). a -> K a b
K ((Expr, [Char]) -> K (Expr, [Char]) a)
-> (Input a -> (Expr, [Char])) -> Input a -> K (Expr, [Char]) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input a -> (Expr, [Char])
forall x. Input x -> (Expr, [Char])
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 :: Err -> 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 = Predicate a
forall (a :: [*]). Predicate a
Pass
instance Semigroup (Predicate a) where <> :: Predicate a -> Predicate a -> Predicate a
(<>)   = 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 -> [Char]) -> Predicate xs
prim = (NP I xs -> Bool) -> (NP (K Expr) xs -> [Char]) -> Predicate xs
forall (xs :: [*]).
(NP I xs -> Bool) -> (NP (K Expr) xs -> [Char]) -> Predicate xs
Prim

{-------------------------------------------------------------------------------
  Construction
-------------------------------------------------------------------------------}

-- | Constant 'True'
pass :: Predicate xs
pass :: forall (a :: [*]). Predicate a
pass = Predicate xs
forall (a :: [*]). Predicate a
Pass

-- | Constant 'False'
fail :: Err -> Predicate xs
fail :: forall (xs :: [*]). [Char] -> Predicate xs
fail = [Char] -> Predicate xs
forall (xs :: [*]). [Char] -> Predicate xs
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 -> [Char]) -> Predicate '[a]
unary a -> Bool
p Expr -> [Char]
msg =
    (NP I '[a] -> Bool)
-> (NP (K Expr) '[a] -> [Char]) -> Predicate '[a]
forall (xs :: [*]).
(NP I xs -> Bool) -> (NP (K Expr) xs -> [Char]) -> Predicate xs
prim
      (\(I x
x :* NP I xs
Nil) -> a -> Bool
p   a
x
x)
      (\(K Expr
l :* NP (K Expr) xs
Nil) -> Expr -> [Char]
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 -> [Char]) -> Predicate '[a, b]
binary a -> b -> Bool
p Expr -> Expr -> [Char]
msg =
    (NP I '[a, b] -> Bool)
-> (NP (K Expr) '[a, b] -> [Char]) -> Predicate '[a, b]
forall (xs :: [*]).
(NP I xs -> Bool) -> (NP (K Expr) xs -> [Char]) -> Predicate xs
prim
      (\(I  x
x :* I  x
y :* NP I xs
Nil) -> a -> b -> Bool
p    a
x
x  b
x
y)
      (\(K Expr
lx :* K Expr
ly :* NP (K Expr) xs
Nil) -> Expr -> Expr -> [Char]
msg Expr
lx Expr
ly)

{-------------------------------------------------------------------------------
  Auxiliary construction
-------------------------------------------------------------------------------}

-- | Specialization of 'unary' for unary relations
satisfies :: (FnName, a -> Bool) -> Predicate '[a]
satisfies :: forall a. (FnName, a -> Bool) -> Predicate '[a]
satisfies (FnName
n, a -> Bool
p) =
    (a -> Bool) -> (Expr -> [Char]) -> Predicate '[a]
forall a. (a -> Bool) -> (Expr -> [Char]) -> Predicate '[a]
unary a -> Bool
p ((Expr -> [Char]) -> Predicate '[a])
-> (Expr -> [Char]) -> Predicate '[a]
forall a b. (a -> b) -> a -> b
$ \Expr
x ->
      Expr -> [Char]
prettyExpr (Expr -> [Char]) -> Expr -> [Char]
forall a b. (a -> b) -> a -> b
$ FnName -> Expr
Fn FnName
"not" Expr -> Expr -> Expr
`App` (FnName -> Expr
Fn FnName
n Expr -> Expr -> Expr
`App` Expr
x)

-- | Specialization of 'binary' for relations
relatedBy :: (FnName, a -> b -> Bool) -> Predicate [a, b]
relatedBy :: forall a b. (FnName, a -> b -> Bool) -> Predicate '[a, b]
relatedBy (FnName
n, a -> b -> Bool
p) =
    (a -> b -> Bool) -> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
forall a b.
(a -> b -> Bool) -> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
binary a -> b -> Bool
p ((Expr -> Expr -> [Char]) -> Predicate '[a, b])
-> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
forall a b. (a -> b) -> a -> b
$ \Expr
x Expr
y ->
      Expr -> [Char]
prettyExpr (Expr -> [Char]) -> Expr -> [Char]
forall a b. (a -> b) -> a -> b
$ FnName -> Expr
Fn FnName
"not" Expr -> Expr -> Expr
`App` (FnName -> Expr
Fn FnName
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 = Predicate (x : xs) -> Fn y x -> Predicate (y : xs)
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 = Predicate (x' : y' : xs)
-> (Fn x x', Fn y y') -> Predicate (x : y : xs)
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 Predicate (x : x : xs)
-> (Fn y x, Fn y x) -> Predicate (y : y : xs)
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 = Predicate (x : y : zs) -> Predicate (y : x : zs)
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 = Predicate (a : xs)
-> Predicate (b : xs) -> Predicate (Either a b : xs)
forall a (xs :: [*]) b.
Predicate (a : xs)
-> Predicate (b : xs) -> Predicate (Either a b : xs)
Choose

-- | Conditional
--
-- This is a variation on 'matchEither' 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 =
    Predicate (() : xs)
-> Predicate (() : xs) -> Predicate (Either () () : xs)
forall a (xs :: [*]) b.
Predicate (a : xs)
-> Predicate (b : xs) -> Predicate (Either a b : xs)
matchEither (Predicate xs -> Predicate (() : xs)
forall (x :: [*]) xs. Predicate x -> Predicate (xs : x)
Const Predicate xs
t) (Predicate xs -> Predicate (() : xs)
forall (x :: [*]) xs. Predicate x -> Predicate (xs : x)
Const Predicate xs
f) Predicate (Either () () : xs)
-> Fn Bool (Either () ()) -> Predicate (Bool : xs)
forall x (xs :: [*]) y.
Predicate (x : xs) -> Fn y x -> Predicate (y : xs)
`dot` (Bool -> Either () ()) -> Fn Bool (Either () ())
forall a b. (a -> b) -> Fn a b
transparent Bool -> Either () ()
fromBool
  where
    fromBool :: Bool -> Either () ()
    fromBool :: Bool -> Either () ()
fromBool Bool
True  = () -> Either () ()
forall a b. a -> Either a b
Left  ()
    fromBool Bool
False = () -> Either () ()
forall a b. b -> Either a b
Right ()

-- | Lambda abstraction
--
-- See module documentation of "Test.Falsify.Predicate" for discussion.
lam :: (x -> Predicate xs) -> Predicate (x : xs)
lam :: forall x (xs :: [*]). (x -> Predicate xs) -> Predicate (x : xs)
lam x -> Predicate xs
k = (Input x -> Predicate xs) -> Predicate (x : xs)
forall x (xs :: [*]).
(Input x -> Predicate xs) -> Predicate (x : xs)
Lam ((Input x -> Predicate xs) -> Predicate (x : xs))
-> (Input x -> Predicate xs) -> Predicate (x : xs)
forall a b. (a -> b) -> a -> b
$ \Input{x
inputValue :: forall x. Input x -> x
inputValue :: x
inputValue} -> x -> Predicate xs
k x
inputValue

{-------------------------------------------------------------------------------
  Failures
-------------------------------------------------------------------------------}

data Failure = Failure {
      Failure -> [Char]
failureErr    :: Err
    , Failure -> [(Expr, [Char])]
failureInputs :: [(Expr, String)]
    }

addInputs :: [(Expr, String)] -> Failure -> Failure
addInputs :: [(Expr, [Char])] -> Failure -> Failure
addInputs [(Expr, [Char])]
new Failure{[Char]
failureErr :: Failure -> [Char]
failureErr :: [Char]
failureErr, [(Expr, [Char])]
failureInputs :: Failure -> [(Expr, [Char])]
failureInputs :: [(Expr, [Char])]
failureInputs} = Failure{
      [Char]
failureErr :: [Char]
failureErr :: [Char]
failureErr
    , failureInputs :: [(Expr, [Char])]
failureInputs = [(Expr, [Char])]
new [(Expr, [Char])] -> [(Expr, [Char])] -> [(Expr, [Char])]
forall a. [a] -> [a] -> [a]
++ [(Expr, [Char])]
failureInputs
    }

prettyFailure :: Failure -> String
prettyFailure :: Failure -> [Char]
prettyFailure Failure{[Char]
failureErr :: Failure -> [Char]
failureErr :: [Char]
failureErr, [(Expr, [Char])]
failureInputs :: Failure -> [(Expr, [Char])]
failureInputs :: [(Expr, [Char])]
failureInputs} =
   [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
failureErr [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ((Expr, [Char]) -> [Char]) -> [(Expr, [Char])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> [Char] -> [Char]) -> (Expr, [Char]) -> [Char]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> [Char] -> [Char]
padInput) [(Expr, [Char])]
failureInputs
  where
    maxLabelLen :: Int
    maxLabelLen :: Int
maxLabelLen = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ((Expr, [Char]) -> Int) -> [(Expr, [Char])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Char] -> Int)
-> ((Expr, [Char]) -> [Char]) -> (Expr, [Char]) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Char]
prettyExpr (Expr -> [Char])
-> ((Expr, [Char]) -> Expr) -> (Expr, [Char]) -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, [Char]) -> Expr
forall a b. (a, b) -> a
fst) [(Expr, [Char])]
failureInputs

    padInput :: Expr -> String -> String
    padInput :: Expr -> [Char] -> [Char]
padInput Expr
e [Char]
v = Int -> [Char] -> [Char]
padTo Int
maxLabelLen (Expr -> [Char]
prettyExpr Expr
e) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
v

    padTo :: Int -> String -> String
    padTo :: Int -> [Char] -> [Char]
padTo Int
n [Char]
xs = [Char]
xs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
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 -> [Char]) -> NP Input xs -> Either Failure ()
evalPrim NP I xs -> Bool
p NP (K Expr) xs -> [Char]
err NP Input xs
xs
  | NP I xs -> Bool
p ((forall a. Input a -> I a) -> NP Input xs -> NP I xs
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 (a -> I a
forall a. a -> I a
I (a -> I a) -> (Input a -> a) -> Input a -> I a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input a -> a
forall x. Input x -> x
inputValue) NP Input xs
xs)
  = () -> Either Failure ()
forall a b. b -> Either a b
Right ()

  | Bool
otherwise
  = Failure -> Either Failure ()
forall a b. a -> Either a b
Left Failure {
        failureErr :: [Char]
failureErr    = NP (K Expr) xs -> [Char]
err (NP (K Expr) xs -> [Char]) -> NP (K Expr) xs -> [Char]
forall a b. (a -> b) -> a -> b
$ (forall a. Input a -> K Expr a) -> NP Input xs -> NP (K Expr) xs
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 (Expr -> K Expr a
forall k a (b :: k). a -> K a b
K (Expr -> K Expr a) -> (Input a -> Expr) -> Input a -> K Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input a -> Expr
forall x. Input x -> Expr
inputExpr) NP Input xs
xs
      , failureInputs :: [(Expr, [Char])]
failureInputs = NP Input xs -> [(Expr, [Char])]
forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, [Char])]
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) =
    (Failure -> Failure) -> Either Failure () -> Either Failure ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(Expr, [Char])] -> Failure -> Failure
addInputs [Input x -> (Expr, [Char])
forall x. Input x -> (Expr, [Char])
renderInput Input x
x]) (Either Failure () -> Either Failure ())
-> Either Failure () -> Either Failure ()
forall a b. (a -> b) -> a -> b
$
      Predicate xs -> NP Input xs -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt (Input x -> Predicate xs
f Input x
Input x
x) NP Input xs
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) =
    (Failure -> Failure) -> Either Failure () -> Either Failure ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(Expr, [Char])] -> Failure -> Failure
addInputs ([(Expr, [Char])] -> Failure -> Failure)
-> [(Expr, [Char])] -> Failure -> Failure
forall a b. (a -> b) -> a -> b
$ [Maybe (Expr, [Char])] -> [(Expr, [Char])]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Expr, [Char])
x']) (Either Failure () -> Either Failure ())
-> Either Failure () -> Either Failure ()
forall a b. (a -> b) -> a -> b
$
      Predicate (x : xs) -> NP Input (x : xs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (x : xs)
p (Input x
y Input x -> NP Input xs -> NP Input (x : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP Input xs
NP Input xs
xs)
  where
    (Input x
y, Maybe (Expr, [Char])
x') = Fn y x -> Input y -> (Input x, Maybe (Expr, [Char]))
forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, [Char]))
applyFn Fn y x
f Input y
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) =
    (Failure -> Failure) -> Either Failure () -> Either Failure ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(Expr, [Char])] -> Failure -> Failure
addInputs ([(Expr, [Char])] -> Failure -> Failure)
-> [(Expr, [Char])] -> Failure -> Failure
forall a b. (a -> b) -> a -> b
$ [Maybe (Expr, [Char])] -> [(Expr, [Char])]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Expr, [Char])
inp_x, Maybe (Expr, [Char])
inp_y]) (Either Failure () -> Either Failure ())
-> Either Failure () -> Either Failure ()
forall a b. (a -> b) -> a -> b
$
      Predicate (x' : y' : xs)
-> NP Input (x' : y' : xs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (x' : y' : xs)
p (Input x'
x' Input x' -> NP Input (y' : xs) -> NP Input (x' : y' : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* Input y'
y' Input y' -> NP Input xs -> NP Input (y' : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP Input xs
NP Input xs
xs)
  where
    (Input x'
x', Maybe (Expr, [Char])
inp_x) = Fn x x' -> Input x -> (Input x', Maybe (Expr, [Char]))
forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, [Char]))
applyFn Fn x x'
f Input x
Input x
x
    (Input y'
y', Maybe (Expr, [Char])
inp_y) = Fn y y' -> Input y -> (Input y', Maybe (Expr, [Char]))
forall a b. Fn a b -> Input a -> (Input b, Maybe (Expr, [Char]))
applyFn Fn y y'
g Input y
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) =
    (Failure -> Failure) -> Either Failure () -> Either Failure ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(Expr, [Char])] -> Failure -> Failure
addInputs [Input x -> (Expr, [Char])
forall x. Input x -> (Expr, [Char])
renderInput Input x
x]) (Either Failure () -> Either Failure ())
-> Either Failure () -> Either Failure ()
forall a b. (a -> b) -> a -> b
$
      case Input x -> x
forall x. Input x -> x
inputValue Input x
x of
        Left  a
a -> Predicate (a : xs) -> NP Input (a : xs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (a : xs)
t (Input x
x{inputValue = a} Input a -> NP Input xs -> NP Input (a : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP Input xs
NP Input xs
xs)
        Right b
b -> Predicate (b : xs) -> NP Input (b : xs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (b : xs)
f (Input x
x{inputValue = b} Input b -> NP Input xs -> NP Input (b : xs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP Input 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 -> [Char]
err)       NP Input xs
xs = (NP I xs -> Bool)
-> (NP (K Expr) xs -> [Char]) -> NP Input xs -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
(NP I xs -> Bool)
-> (NP (K Expr) xs -> [Char]) -> NP Input xs -> Either Failure ()
evalPrim NP I xs -> Bool
p NP (K Expr) xs -> [Char]
err NP Input xs
xs
evalAt Predicate xs
Pass               NP Input xs
_  = () -> Either Failure ()
forall a. a -> Either Failure a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
evalAt (Fail [Char]
err)         NP Input xs
xs = Failure -> Either Failure ()
forall a b. a -> Either a b
Left (Failure -> Either Failure ()) -> Failure -> Either Failure ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [(Expr, [Char])] -> Failure
Failure [Char]
err (NP Input xs -> [(Expr, [Char])]
forall (xs :: [*]). SListI xs => NP Input xs -> [(Expr, [Char])]
renderInputs NP Input xs
xs)
evalAt (Both Predicate xs
p1 Predicate xs
p2)       NP Input xs
xs = Predicate xs -> NP Input xs -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate xs
p1 NP Input xs
xs Either Failure () -> Either Failure () -> Either Failure ()
forall a b.
Either Failure a -> Either Failure b -> Either Failure b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Predicate xs -> NP Input xs -> Either Failure ()
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 = (Input x -> Predicate xs) -> NP Input (x : xs) -> Either Failure ()
forall (xs :: [*]) x.
SListI xs =>
(Input x -> Predicate xs) -> NP Input (x : xs) -> Either Failure ()
evalLam Input x -> Predicate xs
f NP Input xs
NP Input (x : xs)
xs
evalAt (Predicate (x : xs)
p `At` Input x
x)         NP Input xs
xs = Predicate (x : xs) -> NP Input (x : xs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (x : xs)
p (Input x
x Input x -> NP Input xs -> NP Input (x : xs)
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 = Predicate (x' : xs)
-> Fn x x' -> NP Input (x : xs) -> Either Failure ()
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
NP Input (x : xs)
xs
evalAt (Predicate (x' : y' : xs)
p `Split` (Fn x x'
f, Fn y y'
g)) NP Input xs
xs = Predicate (x' : y' : xs)
-> (Fn x x', Fn y y') -> NP Input (x : y : xs) -> Either Failure ()
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
NP Input (x : y : 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
                               Predicate (x : y : zs)
-> NP Input (x : y : zs) -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate (x : y : zs)
p (Input x
y Input x -> NP Input (y : zs) -> NP Input (x : y : zs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* Input y
x Input y -> NP Input zs -> NP Input (y : zs)
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 = Predicate (a : xs)
-> Predicate (b : xs)
-> NP Input (Either a b : xs)
-> Either Failure ()
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
NP Input (Either a b : xs)
xs
evalAt (Const Predicate xs
p)          NP Input xs
xs = Predicate xs -> NP Input xs -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate xs
p (NP Input (x : xs) -> NP Input xs
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
SOP.tl NP Input xs
NP Input (x : xs)
xs)

{-------------------------------------------------------------------------------
  Evaluation and partial evaluation
-------------------------------------------------------------------------------}

-- | Evaluate fully applied predicate
eval :: Predicate '[] -> Either Err ()
eval :: Predicate '[] -> Either [Char] ()
eval Predicate '[]
p = (Failure -> [Char]) -> Either Failure () -> Either [Char] ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Failure -> [Char]
prettyFailure (Either Failure () -> Either [Char] ())
-> Either Failure () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ Predicate '[] -> NP Input '[] -> Either Failure ()
forall (xs :: [*]).
SListI xs =>
Predicate xs -> NP Input xs -> Either Failure ()
evalAt Predicate '[]
p NP Input '[]
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) -> (VarName, x) -> Predicate xs
Predicate (x : xs)
p .$ :: forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (VarName, x) -> Predicate xs
.$ (VarName
n, x
x) = Predicate (x : xs)
p Predicate (x : xs) -> (VarName, [Char], x) -> Predicate xs
forall x (xs :: [*]).
Predicate (x : xs) -> (VarName, [Char], x) -> Predicate xs
`at` (VarName
n, x -> [Char]
forall a. Show a => a -> [Char]
show x
x, x
x)

-- | Generalization of '(.$)' that does not require a 'Show' instance
at ::
     Predicate (x : xs)
  -> (VarName, String, x) -- ^ Rendered name, expression, and input proper
  -> Predicate xs
Predicate (x : xs)
p at :: forall x (xs :: [*]).
Predicate (x : xs) -> (VarName, [Char], x) -> Predicate xs
`at` (VarName
n, [Char]
r, x
x) = Predicate (x : xs)
p Predicate (x : xs) -> (Expr, [Char], x) -> Predicate xs
forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, [Char], x) -> Predicate xs
`atExpr` (VarName -> Expr
Var VarName
n, [Char]
r, x
x)

-- | Generalization of 'at' for an arbitrary 'Expr'
--
-- This is not currently part of the public API, since we haven't yet decided
-- how exactly we want to expose 'Expr' (if at all).
atExpr ::
     Predicate (x : xs)
  -> (Expr, String, x) -- ^ Rendered name, expression, and input proper
  -> Predicate xs
Predicate (x : xs)
p atExpr :: forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, [Char], x) -> Predicate xs
`atExpr` (Expr
e, [Char]
r, x
x) = Predicate (x : xs)
p Predicate (x : xs) -> Input x -> Predicate xs
forall x (xs :: [*]). Predicate (x : xs) -> Input x -> Predicate xs
`At` (Expr -> [Char] -> x -> Input x
forall x. Expr -> [Char] -> x -> Input x
Input Expr
e [Char]
r x
x)

{-------------------------------------------------------------------------------
  Specific predicates
-------------------------------------------------------------------------------}

-- | Construct predicate corresponding to some infix operator
--
-- This is an internal auxiliary.
binaryInfix ::
     FnName  -- ^ Infix operator corresponding to the relation /NOT/ holding
  -> (a -> b -> Bool) -> Predicate [a, b]
binaryInfix :: forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
op a -> b -> Bool
f = (a -> b -> Bool) -> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
forall a b.
(a -> b -> Bool) -> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
binary a -> b -> Bool
f ((Expr -> Expr -> [Char]) -> Predicate '[a, b])
-> (Expr -> Expr -> [Char]) -> Predicate '[a, b]
forall a b. (a -> b) -> a -> b
$ \Expr
x Expr
y -> Expr -> [Char]
prettyExpr (FnName -> Expr -> Expr -> Expr
Infix FnName
op Expr
x Expr
y)

-- | Equal
eq :: Eq a => Predicate [a, a]
eq :: forall a. Eq a => Predicate '[a, a]
eq = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
"/=" a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- | Not equal
ne :: Eq a => Predicate [a, a]
ne :: forall a. Eq a => Predicate '[a, a]
ne = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
"==" a -> a -> Bool
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 = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
">=" a -> a -> Bool
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 = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
">"  a -> a -> Bool
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 = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
"<=" a -> a -> Bool
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 = FnName -> (a -> a -> Bool) -> Predicate '[a, a]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix FnName
"<"  a -> a -> Bool
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 Predicate '[a, a, a] -> (VarName, a) -> Predicate '[a, a]
forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (VarName, x) -> Predicate xs
.$ (VarName
"target", a
target)
  where
    pred :: Predicate [a, a, a]
    pred :: Predicate '[a, a, a]
pred = (Input a -> Predicate '[a, a]) -> Predicate '[a, a, a]
forall x (xs :: [*]).
(Input x -> Predicate xs) -> Predicate (x : xs)
Lam ((Input a -> Predicate '[a, a]) -> Predicate '[a, a, a])
-> (Input a -> Predicate '[a, a]) -> Predicate '[a, a, a]
forall a b. (a -> b) -> a -> b
$ \Input a
target ->
        Predicate '[a, a]
forall a. Ord a => Predicate '[a, a]
ge Predicate '[a, a] -> Fn a a -> Predicate '[a, a]
forall x (xs :: [*]) y.
Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs)
`on` (FnName, a -> a) -> Fn a a
forall b a. Show b => (FnName, a -> b) -> Fn a b
fn (FnName
"distanceToTarget", a -> a -> a
distanceTo (Input a -> a
forall x. Input x -> x
inputValue Input a
target))

    distanceTo :: a -> a -> a
    distanceTo :: a -> a -> a
distanceTo a
target a
x
      | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
target = a
target a -> a -> a
forall a. Num a => a -> a -> a
- a
x
      | Bool
otherwise   = a
x a -> a -> a
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 = Predicate '[a, a]
forall a. Eq a => Predicate '[a, a]
eq Predicate '[a, a] -> (VarName, a) -> Predicate '[a]
forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (VarName, x) -> Predicate xs
.$ (VarName
"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 = [Predicate '[a]] -> Predicate '[a]
forall a. Monoid a => [a] -> a
mconcat [
           Predicate '[a, a]
forall a. Ord a => Predicate '[a, a]
le Predicate '[a, a] -> (VarName, a) -> Predicate '[a]
forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (VarName, x) -> Predicate xs
.$ (VarName
"lo", a
lo)
    , Predicate '[a, a] -> Predicate '[a, a]
forall x y (zs :: [*]).
Predicate (x : y : zs) -> Predicate (y : x : zs)
flip Predicate '[a, a]
forall a. Ord a => Predicate '[a, a]
le Predicate '[a, a] -> (VarName, a) -> Predicate '[a]
forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (VarName, x) -> Predicate xs
.$ (VarName
"hi", a
hi)
    ]

-- | Number is even
even :: Integral a => Predicate '[a]
even :: forall a. Integral a => Predicate '[a]
even = (FnName, a -> Bool) -> Predicate '[a]
forall a. (FnName, a -> Bool) -> Predicate '[a]
satisfies (FnName
"even", a -> Bool
forall a. Integral a => a -> Bool
Prelude.even)

-- | Number is odd
odd :: Integral a => Predicate '[a]
odd :: forall a. Integral a => Predicate '[a]
odd  = (FnName, a -> Bool) -> Predicate '[a]
forall a. (FnName, a -> Bool) -> Predicate '[a]
satisfies (FnName
"odd ", a -> Bool
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 = Predicate '[a, [a]] -> Predicate '[[a], a]
forall x y (zs :: [*]).
Predicate (x : y : zs) -> Predicate (y : x : zs)
flip (Predicate '[a, [a]] -> Predicate '[[a], a])
-> Predicate '[a, [a]] -> Predicate '[[a], a]
forall a b. (a -> b) -> a -> b
$ FnName -> (a -> [a] -> Bool) -> Predicate '[a, [a]]
forall a b. FnName -> (a -> b -> Bool) -> Predicate '[a, b]
binaryInfix (FnName
"`notElem`") a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 = (Input [a] -> Predicate '[]) -> Predicate '[[a]]
forall x (xs :: [*]).
(Input x -> Predicate xs) -> Predicate (x : xs)
Lam ((Input [a] -> Predicate '[]) -> Predicate '[[a]])
-> (Input [a] -> Predicate '[]) -> Predicate '[[a]]
forall a b. (a -> b) -> a -> b
$ \Input [a]
xs ->
    (((Word, a), (Word, a)) -> Predicate '[])
-> [((Word, a), (Word, a))] -> Predicate '[]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
      (((Word, a) -> (Word, a) -> Predicate '[])
-> ((Word, a), (Word, a)) -> Predicate '[]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (((Word, a) -> (Word, a) -> Predicate '[])
 -> ((Word, a), (Word, a)) -> Predicate '[])
-> ((Word, a) -> (Word, a) -> Predicate '[])
-> ((Word, a), (Word, a))
-> Predicate '[]
forall a b. (a -> b) -> a -> b
$ Expr -> (Word, a) -> (Word, a) -> Predicate '[]
pred (Input [a] -> Expr
forall x. Input x -> Expr
inputExpr Input [a]
xs))
      ([(Word, a)] -> [((Word, a), (Word, a))]
forall x. [x] -> [(x, x)]
pairs ([(Word, a)] -> [((Word, a), (Word, a))])
-> [(Word, a)] -> [((Word, a), (Word, a))]
forall a b. (a -> b) -> a -> b
$ [Word] -> [a] -> [(Word, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Word
0..] (Input [a] -> [a]
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) (x, x) -> [(x, x)] -> [(x, x)]
forall a. a -> [a] -> [a]
: [x] -> [(x, x)]
forall x. [x] -> [(x, x)]
pairs (x
y x -> [x] -> [x]
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
        Predicate '[a, a] -> (Expr, [Char], a) -> Predicate '[a]
forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, [Char], x) -> Predicate xs
`atExpr` (FnName -> Expr -> Expr -> Expr
Infix FnName
"!!" Expr
xs (VarName -> Expr
Var (VarName -> Expr) -> VarName -> Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> VarName
WrapVarName ([Char] -> VarName) -> [Char] -> VarName
forall a b. (a -> b) -> a -> b
$ Word -> [Char]
forall a. Show a => a -> [Char]
show Word
i), a -> [Char]
forall a. Show a => a -> [Char]
show a
x, a
x)
        Predicate '[a] -> (Expr, [Char], a) -> Predicate '[]
forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, [Char], x) -> Predicate xs
`atExpr` (FnName -> Expr -> Expr -> Expr
Infix FnName
"!!" Expr
xs (VarName -> Expr
Var (VarName -> Expr) -> VarName -> Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> VarName
WrapVarName ([Char] -> VarName) -> [Char] -> VarName
forall a b. (a -> b) -> a -> b
$ Word -> [Char]
forall a. Show a => a -> [Char]
show Word
j), a -> [Char]
forall a. Show a => a -> [Char]
show a
y, a
y)