-----------------------------------------------------------------------------
-----------------------------------------------------------------------------
{-# LANGUAGE OverloadedStrings #-}

-- |
-- Module      :  Disco.Property
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Properties of disco functions.
module Disco.Property (
  -- * Generation
  generateSamples,

  -- * Utility
  invertMotive,
  invertPropResult,

  -- * Pretty-printing
  prettyTestResult,
)
where

import Prelude hiding ((<>))

import Data.Char (toLower)
import qualified Data.Enumeration.Invertible as E

import Disco.Effects.Random
import Polysemy

import Disco.AST.Typed
import Disco.Effects.Input
import Disco.Effects.LFresh
import Disco.Error
import Disco.Pretty
import Disco.Syntax.Prims
import Disco.Typecheck.Erase (eraseProperty)
import Disco.Types (TyDefCtx)
import Disco.Value
import Polysemy.Reader

-- | Toggles which outcome (finding or not finding the thing being
--   searched for) qualifies as success, without changing the thing
--   being searched for.
invertMotive :: SearchMotive -> SearchMotive
invertMotive :: SearchMotive -> SearchMotive
invertMotive (SearchMotive (Bool
a, Bool
b)) = (Bool, Bool) -> SearchMotive
SearchMotive (Bool -> Bool
not Bool
a, Bool
b)

-- | Flips the success or failure status of a @PropResult@, leaving
--   the explanation unchanged.
invertPropResult :: TestResult -> TestResult
invertPropResult :: TestResult -> TestResult
invertPropResult res :: TestResult
res@(TestResult Bool
b TestReason
r TestEnv
env)
  | TestRuntimeError EvalError
_ <- TestReason
r = TestResult
res
  | Bool
otherwise = Bool -> TestReason -> TestEnv -> TestResult
TestResult (Bool -> Bool
not Bool
b) TestReason
r TestEnv
env

randomLarge :: Member Random r => [Integer] -> Sem r [Integer]
randomLarge :: forall (r :: EffectRow).
Member Random r =>
[Integer] -> Sem r [Integer]
randomLarge [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
randomLarge [Integer
_] = forall (m :: * -> *) a. Monad m => a -> m a
return []
randomLarge (Integer
x : Integer
y : [Integer]
xs) = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) x.
(Member Random r, Random x) =>
(x, x) -> Sem r x
randomR (Integer
x, Integer
y) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: EffectRow).
Member Random r =>
[Integer] -> Sem r [Integer]
randomLarge (Integer
y forall a. a -> [a] -> [a]
: [Integer]
xs)

-- | Select samples from an enumeration according to a search type. Also returns
--   a 'SearchType' describing the results, which may be 'Exhaustive' if the
--   enumeration is no larger than the number of samples requested.
generateSamples :: Member Random r => SearchType -> E.IEnumeration a -> Sem r ([a], SearchType)
generateSamples :: forall (r :: EffectRow) a.
Member Random r =>
SearchType -> IEnumeration a -> Sem r ([a], SearchType)
generateSamples SearchType
Exhaustive IEnumeration a
e = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. IEnumeration a -> [a]
E.enumerate IEnumeration a
e, SearchType
Exhaustive)
generateSamples (Randomized Integer
n Integer
m) IEnumeration a
e
  | E.Finite Integer
k <- forall a. IEnumeration a -> Cardinality
E.card IEnumeration a
e, Integer
k forall a. Ord a => a -> a -> Bool
<= Integer
n forall a. Num a => a -> a -> a
+ Integer
m = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. IEnumeration a -> [a]
E.enumerate IEnumeration a
e, SearchType
Exhaustive)
  | Bool
otherwise = do
      let small :: [Integer]
small = [Integer
0 .. Integer
n]
      [Integer]
rs <- forall (r :: EffectRow).
Member Random r =>
[Integer] -> Sem r [Integer]
randomLarge [Integer
100, Integer
1000, Integer
10000, Integer
100000, Integer
1000000]
      let samples :: [a]
samples = forall a b. (a -> b) -> [a] -> [b]
map (forall a. IEnumeration a -> Integer -> a
E.select IEnumeration a
e) forall a b. (a -> b) -> a -> b
$ [Integer]
small forall a. [a] -> [a] -> [a]
++ [Integer]
rs
      forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
samples, Integer -> Integer -> SearchType
Randomized Integer
n Integer
m)

-- XXX do shrinking for randomly generated test cases?

------------------------------------------------------------
-- Pretty-printing for test results
------------------------------------------------------------

prettyResultCertainty :: Members '[LFresh, Reader PA] r => TestReason -> AProperty -> String -> Sem r (Doc ann)
prettyResultCertainty :: forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
TestReason -> AProperty -> String -> Sem r (Doc ann)
prettyResultCertainty TestReason
r AProperty
prop String
res =
  (if TestReason -> Bool
resultIsCertain TestReason
r then Sem r (Doc ann)
"Certainly" else Sem r (Doc ann)
"Possibly") forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
res forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
":" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (AProperty -> Property
eraseProperty AProperty
prop)

prettyTestReason ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  Bool ->
  AProperty ->
  TestReason ->
  Sem r (Doc ann)
prettyTestReason :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestReason -> Sem r (Doc ann)
prettyTestReason Bool
_ AProperty
_ TestReason
TestBool = forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyTestReason Bool
b AProperty
_ (TestFound (TestResult Bool
_ TestReason
_ TestEnv
env))
  | Bool
b = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r (Doc ann)
prettyTestEnv String
"Found example:" TestEnv
env
  | Bool -> Bool
not Bool
b = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r (Doc ann)
prettyTestEnv String
"Found counterexample:" TestEnv
env
prettyTestReason Bool
b AProperty
_ (TestNotFound SearchType
Exhaustive)
  | Bool
b = Sem r (Doc ann)
"No counterexamples exist; all possible values were checked."
  | Bool -> Bool
not Bool
b = Sem r (Doc ann)
"No example exists; all possible values were checked."
prettyTestReason Bool
b AProperty
_ (TestNotFound (Randomized Integer
n Integer
m))
  | Bool
b = Sem r (Doc ann)
"Checked" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show (Integer
n forall a. Num a => a -> a -> a
+ Integer
m)) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"possibilities without finding a counterexample."
  | Bool -> Bool
not Bool
b = Sem r (Doc ann)
"No example was found; checked" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show (Integer
n forall a. Num a => a -> a -> a
+ Integer
m)) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"possibilities."
prettyTestReason Bool
_ AProperty
_ (TestEqual Type
t Value
a1 Value
a2) =
  forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
bulletList
    Sem r (Doc ann)
"-"
    [ Sem r (Doc ann)
"Left side:  " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
t Value
a1
    , Sem r (Doc ann)
"Right side: " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
t Value
a2
    ]
prettyTestReason Bool
_ AProperty
_ (TestLt Type
t Value
a1 Value
a2) =
  forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
bulletList
    Sem r (Doc ann)
"-"
    [ Sem r (Doc ann)
"Left side:  " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
t Value
a1
    , Sem r (Doc ann)
"Right side: " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
t Value
a2
    ]
prettyTestReason Bool
_ AProperty
_ (TestRuntimeError EvalError
ee) =
  forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ann)
"Test failed with an error:"
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (EvalError -> DiscoError
EvalErr EvalError
ee)
-- \$+$
-- prettyTestEnv "Example inputs that caused the error:" env
-- See #364
prettyTestReason Bool
b (ATApp Type
_ (ATPrim Type
_ (PrimBOp BOp
_)) (ATTup Type
_ [AProperty
p1, AProperty
p2])) (TestBin LOp
_ TestResult
tr1 TestResult
tr2) =
  forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
bulletList
    Sem r (Doc ann)
"-"
    [ forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Left side:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult' Bool
b AProperty
p1 TestResult
tr1
    , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Right side:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult' Bool
b AProperty
p2 TestResult
tr2
    ]
-- See Note [prettyTestReason fallback]
prettyTestReason Bool
_ AProperty
_ TestReason
_ = forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty

-- ~~~~ Note [prettyTestReason fallback]
--
-- prettyTestReason can do a decent job printing out reasons for a
-- test result when operators like /\, \/, etc. are written
-- explicitly; then it can structurally recurse on the original Prop
-- expression in parllel with the TestReason.  However, it is possible
-- to e.g. write a function which returns a Prop, making the structure
-- of the Prop expression opaque.  For example, consider this example
-- (from test/prop-higher-order):
--
-- !!! all [true, true, true, false, true]
-- all : List(Prop) -> Prop
-- all ps = reduce(~/\~, true, ps)
--
-- This test is false, and the TestReason ends up with a bunch of
-- nested TestBin LAnd.  However, the proposition is literally a
-- function application so we cannot see that it matches the structure
-- of the test result.  So we just give up and decline to print a
-- reason.

prettyTestResult' ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  Bool ->
  AProperty ->
  TestResult ->
  Sem r (Doc ann)
prettyTestResult' :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult' Bool
_ AProperty
prop (TestResult Bool
bool TestReason
tr TestEnv
_) =
  forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
TestReason -> AProperty -> String -> Sem r (Doc ann)
prettyResultCertainty TestReason
tr AProperty
prop (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (forall a. Show a => a -> String
show Bool
bool))
    forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestReason -> Sem r (Doc ann)
prettyTestReason Bool
bool AProperty
prop TestReason
tr

prettyTestResult ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  AProperty ->
  TestResult ->
  Sem r (Doc ann)
prettyTestResult :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult AProperty
prop (TestResult Bool
b TestReason
r TestEnv
env) = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult' Bool
b AProperty
prop (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
b TestReason
r TestEnv
env)

prettyTestEnv ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  String ->
  TestEnv ->
  Sem r (Doc ann)
prettyTestEnv :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r (Doc ann)
prettyTestEnv String
_ (TestEnv []) = forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyTestEnv String
s (TestEnv [(String, Type, Value)]
vs) = forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (forall a b. (a -> b) -> [a] -> [b]
map (String, Type, Value) -> Sem r (Doc ann)
prettyBind [(String, Type, Value)]
vs)
 where
  maxNameLen :: Int
maxNameLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, Type
_, Value
_) -> forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) forall a b. (a -> b) -> a -> b
$ [(String, Type, Value)]
vs
  prettyBind :: (String, Type, Value) -> Sem r (Doc ann)
prettyBind (String
x, Type
ty, Value
v) =
    forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Int -> a -> [a]
replicate (Int
maxNameLen forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x) Char
' ') forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v