Property.hs

{-# 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 (a, b)) = SearchMotive (not a, b)

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

randomLarge :: Member Random r => [Integer] -> Sem r [Integer]
randomLarge [] = return []
randomLarge [_] = return []
randomLarge (x : y : xs) = (:) <$> randomR (x, y) <*> randomLarge (y : 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 Exhaustive e = return (E.enumerate e, Exhaustive)
generateSamples (Randomized n m) e
  | E.Finite k <- E.card e, k <= n + m = return (E.enumerate e, Exhaustive)
  | otherwise = do
      let small = [0 .. n]
      rs <- randomLarge [100, 1000, 10000, 100000, 1000000]
      let samples = map (E.select e) $ small ++ rs
      return (samples, Randomized n 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 r prop res =
  (if resultIsCertain r then "Certainly" else "Possibly") <+> text res <> ":" <+> pretty (eraseProperty prop)

prettyTestReason ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  Bool ->
  AProperty ->
  TestReason ->
  TestEnv ->
  Sem r (Doc ann)
prettyTestReason _ _ TestBool _ = empty
prettyTestReason b (ATAbs _ _ body) (TestFound (TestResult b' r' env')) env = do
  lunbind body $ \(_, p) ->
    prettyTestEnv ("Found " ++ if b then "example:" else "counterexample:") env
      $+$ prettyTestReason b' p r' env'
prettyTestReason b _ (TestNotFound Exhaustive) _
  | b = "No counterexamples exist; all possible values were checked."
  | otherwise = "No example exists; all possible values were checked."
prettyTestReason b _ (TestNotFound (Randomized n m)) _
  | b = "Checked" <+> text (show (n + m)) <+> "possibilities without finding a counterexample."
  | otherwise = "No example was found; checked" <+> text (show (n + m)) <+> "possibilities."
prettyTestReason _ _ (TestCmp _ t a1 a2) _ =
  bulletList
    "-"
    [ "Left side:  " <> prettyValue t a1
    , "Right side: " <> prettyValue t a2
    ]
prettyTestReason _ _ (TestRuntimeError ee) env =
  nest 2 $
    "Test failed with an error:"
      $+$ pretty (EvalErr ee)
      $+$ prettyTestEnv "Example inputs that caused the error:" env
prettyTestReason _ (ATApp _ (ATPrim _ (PrimBOp _)) (ATTup _ [p1, p2])) (TestBin _ tr1 tr2) _ =
  bulletList
    "-"
    [ nest 2 $ prettyTestResult p1 tr1
    , nest 2 $ prettyTestResult p2 tr2
    ]
-- See Note [prettyTestReason fallback]
prettyTestReason _ _ _ _ = 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 prop (TestResult bool tr env) =
  prettyResultCertainty tr prop (map toLower (show bool))
    $+$ prettyTestReason bool prop tr env

prettyTestEnv ::
  Members '[Input TyDefCtx, LFresh, Reader PA] r =>
  String ->
  TestEnv ->
  Sem r (Doc ann)
prettyTestEnv _ (TestEnv []) = empty
prettyTestEnv s (TestEnv vs) = nest 2 $ text s $+$ vcat (map prettyBind vs)
 where
  maxNameLen = maximum . map (\(n, _, _) -> length n) $ vs
  prettyBind (x, ty, v) =
    text x <> text (replicate (maxNameLen - length x) ' ') <+> "=" <+> prettyValue ty v