{-# 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 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.Random
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 {} <- 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 [] = [Integer] -> Sem r [Integer]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
randomLarge [Integer
_] = [Integer] -> Sem r [Integer]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
randomLarge (Integer
x : Integer
y : [Integer]
xs) = (:) (Integer -> [Integer] -> [Integer])
-> Sem r Integer -> Sem r ([Integer] -> [Integer])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Sem r Integer
forall (r :: EffectRow) x.
(Member Random r, Random x) =>
(x, x) -> Sem r x
randomR (Integer
x, Integer
y) Sem r ([Integer] -> [Integer])
-> Sem r [Integer] -> Sem r [Integer]
forall a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Integer] -> Sem r [Integer]
forall (r :: EffectRow).
Member Random r =>
[Integer] -> Sem r [Integer]
randomLarge (Integer
y Integer -> [Integer] -> [Integer]
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 = ([a], SearchType) -> Sem r ([a], SearchType)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (IEnumeration a -> [a]
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 <- IEnumeration a -> Cardinality
forall a. IEnumeration a -> Cardinality
E.card IEnumeration a
e, Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m = ([a], SearchType) -> Sem r ([a], SearchType)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (IEnumeration a -> [a]
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 <- [Integer] -> Sem r [Integer]
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 = (Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (IEnumeration a -> Integer -> a
forall a. IEnumeration a -> Integer -> a
E.select IEnumeration a
e) ([Integer] -> [a]) -> [Integer] -> [a]
forall a b. (a -> b) -> a -> b
$ [Integer]
small [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
rs
      ([a], SearchType) -> Sem r ([a], SearchType)
forall a. a -> Sem r a
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") Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
res Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
":" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Property -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Property -> Sem r (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 ->
  TestEnv ->
  Sem r (Doc ann)
prettyTestReason :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestReason -> TestEnv -> Sem r (Doc ann)
prettyTestReason Bool
_ AProperty
_ TestReason
TestBool TestEnv
_ = Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyTestReason Bool
b (ATAbs Quantifier
_ Type
_ Bind [APattern] AProperty
body) (TestFound (TestResult Bool
b' TestReason
r' TestEnv
env')) TestEnv
env = do
  Bind [APattern] AProperty
-> (([APattern], AProperty) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [APattern] AProperty
body ((([APattern], AProperty) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([APattern], AProperty) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([APattern]
_, AProperty
p) ->
    String -> TestEnv -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r (Doc ann)
prettyTestEnv (String
"Found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool
b then String
"example:" else String
"counterexample:") TestEnv
env
      Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Bool -> AProperty -> TestReason -> TestEnv -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestReason -> TestEnv -> Sem r (Doc ann)
prettyTestReason Bool
b' AProperty
p TestReason
r' TestEnv
env'
prettyTestReason Bool
b AProperty
_ (TestNotFound SearchType
Exhaustive) TestEnv
_
  | Bool
b = Sem r (Doc ann)
"No counterexamples exist; all possible values were checked."
  | Bool
otherwise = Sem r (Doc ann)
"No example exists; all possible values were checked."
prettyTestReason Bool
b AProperty
_ (TestNotFound (Randomized Integer
n Integer
m)) TestEnv
_
  | Bool
b = Sem r (Doc ann)
"Checked" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Integer -> String
forall a. Show a => a -> String
show (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"possibilities without finding a counterexample."
  | Bool
otherwise = Sem r (Doc ann)
"No example was found; checked" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Integer -> String
forall a. Show a => a -> String
show (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"possibilities."
prettyTestReason Bool
_ AProperty
_ (TestCmp BOp
_ Type
t Value
a1 Value
a2) TestEnv
_ =
  Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
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:  " Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Type -> Value -> Sem r (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: " Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Type -> Value -> Sem r (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) TestEnv
env =
  Int -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ann)
"Test failed with an error:"
      Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ DiscoError -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
DiscoError -> Sem r (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)
      Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ String -> TestEnv -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r (Doc ann)
prettyTestEnv String
"Example inputs that caused the error:" TestEnv
env
prettyTestReason Bool
_ (ATApp Type
_ (ATPrim Type
_ (PrimBOp BOp
_)) (ATTup Type
_ [AProperty
p1, AProperty
p2])) (TestBin LOp
_ TestResult
tr1 TestResult
tr2) TestEnv
_ =
  Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
bulletList
    Sem r (Doc ann)
"-"
    [ Int -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ AProperty -> TestResult -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult AProperty
p1 TestResult
tr1
    , Int -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ AProperty -> TestResult -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestResult -> Sem r (Doc ann)
prettyTestResult AProperty
p2 TestResult
tr2
    ]
-- See Note [prettyTestReason fallback]
prettyTestReason Bool
_ AProperty
_ TestReason
_ TestEnv
_ = Sem r (Doc ann)
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 =>
  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
bool TestReason
tr TestEnv
env) =
  TestReason -> AProperty -> String -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
TestReason -> AProperty -> String -> Sem r (Doc ann)
prettyResultCertainty TestReason
tr AProperty
prop ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Bool -> String
forall a. Show a => a -> String
show Bool
bool))
    Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Bool -> AProperty -> TestReason -> TestEnv -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Bool -> AProperty -> TestReason -> TestEnv -> Sem r (Doc ann)
prettyTestReason Bool
bool AProperty
prop TestReason
tr 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 []) = Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyTestEnv String
s (TestEnv [(String, Type, Value)]
vs) = Int -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (((String, Type, Value) -> Sem r (Doc ann))
-> [(String, Type, Value)] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type, Value) -> Sem r (Doc ann)
prettyBind [(String, Type, Value)]
vs)
 where
  maxNameLen :: Int
maxNameLen = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int)
-> ([(String, Type, Value)] -> [Int])
-> [(String, Type, Value)]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type, Value) -> Int) -> [(String, Type, Value)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, Type
_, Value
_) -> String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) ([(String, Type, Value)] -> Int) -> [(String, Type, Value)] -> Int
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) =
    String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
x Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxNameLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x) Char
' ') Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v