-- | 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]
relatedBy :: forall a b. (String, a -> b -> Bool) -> Predicate '[a, b]
relatedBy (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) -> (String, String, x) -> Predicate xs
`at` (String
n, forall a. Show a => a -> String
show x
x, x
x)

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