module Test.Falsify.Predicate (
Predicate
, Expr
, prettyExpr
, Fn
, fn
, fnWith
, transparent
, alwaysPass
, alwaysFail
, unary
, binary
, satisfies
, relatedBy
, dot
, split
, on
, flip
, matchEither
, matchBool
, eval
, (.$)
, at
, 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
type Var = String
data Expr =
Var Var
| App Expr Expr
| Infix Var Expr Expr
prettyExpr :: Expr -> String
prettyExpr :: Expr -> String
prettyExpr = Bool -> Expr -> String
go Bool
False
where
go ::
Bool
-> 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
, 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
")"
data Fn a b =
Visible Var (b -> String) (a -> b)
| Transparent (a -> b)
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)
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
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
data Input x = Input {
forall x. Input x -> Expr
inputExpr :: Expr
, forall x. Input x -> String
inputRendered :: String
, forall x. Input x -> x
inputValue :: x
}
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
type Err = String
data Predicate :: [Type] -> Type where
Prim :: (NP I xs -> Bool) -> (NP (K Expr) xs -> Err) -> Predicate xs
Pass :: Predicate xs
Fail :: Predicate xs
Both :: Predicate xs -> Predicate xs -> Predicate xs
Lam :: (Input x -> Predicate xs) -> Predicate (x ': xs)
At :: Predicate (x : xs) -> Input x -> Predicate xs
Dot :: Predicate (x' : xs) -> Fn x x' -> Predicate (x : xs)
Split :: Predicate (x' : y' : xs) -> (Fn x x', Fn y y') -> Predicate (x : y : xs)
Flip :: Predicate (x : y : zs) -> Predicate (y : x : zs)
Choose ::
Predicate ( a : xs)
-> Predicate ( b : xs)
-> Predicate (Either a b : xs)
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
prim ::
(NP I xs -> Bool)
-> (NP (K Expr) xs -> Err)
-> 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
alwaysPass :: Predicate xs
alwaysPass :: forall (a :: [*]). Predicate a
alwaysPass = forall (a :: [*]). Predicate a
Pass
alwaysFail :: Predicate xs
alwaysFail :: forall (a :: [*]). Predicate a
alwaysFail = forall (a :: [*]). Predicate a
Fail
unary ::
(a -> Bool)
-> (Expr -> Err)
-> 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 ::
(a -> b -> Bool)
-> (Expr -> Expr -> Err)
-> 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)
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)
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)
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
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
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)
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
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
matchBool ::
Predicate xs
-> Predicate xs
-> 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 ()
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
' '
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)
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
(.$) :: Show x => Predicate (x : xs) -> (Var, x) -> Predicate xs
Predicate (x : xs)
p .$ :: forall x (xs :: [*]).
Show x =>
Predicate (x : xs) -> (String, x) -> Predicate xs
.$ (String
n, x
x) = Predicate (x : xs)
p forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, String, x) -> Predicate xs
`at` (String -> Expr
Var String
n, forall a. Show a => a -> String
show x
x, x
x)
at ::
Predicate (x : xs)
-> (Expr, String, x)
-> Predicate xs
Predicate (x : xs)
p at :: forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, String, x) -> Predicate xs
`at` (Expr
e, String
r, x
x) = Predicate (x : xs)
p forall x (xs :: [*]). Predicate (x : xs) -> Input x -> Predicate xs
`At` (forall x. Expr -> String -> x -> Input x
Input Expr
e String
r x
x)
binaryInfix ::
Var
-> (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)
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
(==)
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
(/=)
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
(<)
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
(<=)
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
(>)
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
(>=)
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
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)
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)
]
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)
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)
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
pairwise :: forall a. Show a => Predicate [a, a] -> Predicate '[[a]]
pairwise :: forall a. Show a => Predicate '[a, a] -> Predicate '[[a]]
pairwise Predicate '[a, a]
p = forall x (xs :: [*]).
(Input x -> Predicate xs) -> Predicate (x : xs)
Lam forall a b. (a -> b) -> a -> b
$ \Input [a]
xs ->
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
(forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Expr -> (Word, a) -> (Word, a) -> Predicate '[]
pred (forall x. Input x -> Expr
inputExpr Input [a]
xs))
(forall x. [x] -> [(x, x)]
pairs forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Word
0..] (forall x. Input x -> x
inputValue Input [a]
xs))
where
pairs :: forall x. [x] -> [(x, x)]
pairs :: forall x. [x] -> [(x, x)]
pairs [] = []
pairs [x
_] = []
pairs (x
x : x
y : [x]
zs) = (x
x, x
y) forall a. a -> [a] -> [a]
: forall x. [x] -> [(x, x)]
pairs (x
y forall a. a -> [a] -> [a]
: [x]
zs)
pred :: Expr -> (Word, a) -> (Word, a) -> Predicate '[]
pred :: Expr -> (Word, a) -> (Word, a) -> Predicate '[]
pred Expr
xs (Word
i, a
x) (Word
j, a
y) =
Predicate '[a, a]
p
forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, String, x) -> Predicate xs
`at` (String -> Expr -> Expr -> Expr
Infix String
"!!" Expr
xs (String -> Expr
Var forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Word
i), forall a. Show a => a -> String
show a
x, a
x)
forall x (xs :: [*]).
Predicate (x : xs) -> (Expr, String, x) -> Predicate xs
`at` (String -> Expr -> Expr -> Expr
Infix String
"!!" Expr
xs (String -> Expr
Var forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Word
j), forall a. Show a => a -> String
show a
y, a
y)