{-# LANGUAGE CPP                    #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE UndecidableInstances   #-}

#if __GLASGOW_HASKELL__ < 806
-- There is a bug in older versions of Haddock that don't allow documentation
-- on GADT arguments.
#define HADDOCK --
#else
#define HADDOCK -- ^
#endif

module Polysemy.Law
  ( Law (..)
  , runLaw
  , MakeLaw (..)
  , Citizen (..)
  , printf
  , module Test.QuickCheck
  ) where

import Control.Arrow (first)
import Data.Char
import Polysemy
import Test.QuickCheck


------------------------------------------------------------------------------
-- | Associates the name @r@ with the eventual type @a@. For example,
-- @'Citizen' (String -> Bool) Bool@ can produce arbitrary @Bool@s by calling
-- the given function with arbitrary @String@s.
class Citizen r a | r -> a where
  -- | Generate two @a@s via two @r@s. Additionally, produce a list of strings
  -- corresponding to any arbitrary arguments we needed to build.
  getCitizen :: r -> r -> Gen ([String], (a, a))

instance {-# OVERLAPPING #-} Citizen (Sem r a -> b) (Sem r a -> b) where
  getCitizen :: (Sem r a -> b)
-> (Sem r a -> b) -> Gen ([String], (Sem r a -> b, Sem r a -> b))
getCitizen Sem r a -> b
r1 Sem r a -> b
r2 = ([String], (Sem r a -> b, Sem r a -> b))
-> Gen ([String], (Sem r a -> b, Sem r a -> b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], (Sem r a -> b
r1, Sem r a -> b
r2))

instance Citizen (Sem r a) (Sem r a) where
  getCitizen :: Sem r a -> Sem r a -> Gen ([String], (Sem r a, Sem r a))
getCitizen Sem r a
r1 Sem r a
r2 = ([String], (Sem r a, Sem r a))
-> Gen ([String], (Sem r a, Sem r a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], (Sem r a
r1, Sem r a
r2))

instance (Arbitrary a, Show a, Citizen b r) => Citizen (a -> b) r where
  getCitizen :: (a -> b) -> (a -> b) -> Gen ([String], (r, r))
getCitizen a -> b
f1 a -> b
f2 = do
    a
a <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
    ([String] -> [String]) -> ([String], (r, r)) -> ([String], (r, r))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a -> String
forall a. Show a => a -> String
show a
a String -> [String] -> [String]
forall a. a -> [a] -> [a]
:) (([String], (r, r)) -> ([String], (r, r)))
-> Gen ([String], (r, r)) -> Gen ([String], (r, r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> b -> Gen ([String], (r, r))
forall r a. Citizen r a => r -> r -> Gen ([String], (a, a))
getCitizen (a -> b
f1 a
a) (a -> b
f2 a
a)


------------------------------------------------------------------------------
-- | A law that effect @e@ must satisfy whenever it is in environment @r@. You
-- can use 'runLaw' to transform these 'Law's into QuickCheck-able 'Property's.
data Law e r where
  -- | A pure 'Law', that doesn't require any access to 'IO'.
  Law
      :: ( Eq a
         , Show a
         , Citizen i12n (Sem r x -> a)
         , Citizen res (Sem (e ': r) x)
         )
      => i12n
         HADDOCK An interpretation from @'Sem' r x@ down to a pure value. This is
         -- likely 'run'.
      -> String
         HADDOCK A string representation of the left-hand of the rule. This is
         -- a formatted string, for more details, refer to 'printf'.
      -> res
         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
         -- is a function type, it's guaranteed to be called with the same
         -- arguments that the right-handed side was called with.
      -> String
         HADDOCK A string representation of the right-hand of the rule. This is
         -- a formatted string, for more details, refer to 'printf'.
      -> res
         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
         -- is a function type, it's guaranteed to be called with the same
         -- arguments that the left-handed side was called with.
      -> Law e r
  -- | Like 'Law', but for 'IO'-accessing effects.
  LawIO
      :: ( Eq a
         , Show a
         , Citizen i12n (Sem r x -> IO a)
         , Citizen res (Sem (e ': r) x)
         )
      => i12n
         HADDOCK An interpretation from @'Sem' r x@ down to an 'IO' value. This is
         -- likely 'runM'.
      -> String
         HADDOCK A string representation of the left-hand of the rule. This is
         -- a formatted string, for more details, refer to 'printf'.
      -> res
         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
         -- is a function type, it's guaranteed to be called with the same
         -- arguments that the right-handed side was called with.
      -> String
         HADDOCK A string representation of the right-hand of the rule. This is
         -- a formatted string, for more details, refer to 'printf'.
      -> res
         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
         -- is a function type, it's guaranteed to be called with the same
         -- arguments that the left-handed side was called with.
      -> Law e r


------------------------------------------------------------------------------
-- | A typeclass that provides the smart constructor 'mkLaw'.
class MakeLaw e r where
  -- | A smart constructor for building 'Law's.
  mkLaw
      :: (Eq a, Show a, Citizen res (Sem (e ': r) a))
      => String
      -> res
      -> String
      -> res
      -> Law e r

instance MakeLaw e '[] where
  mkLaw :: String -> res -> String -> res -> Law e '[]
mkLaw = (Sem '[] a -> a) -> String -> res -> String -> res -> Law e '[]
forall a i12n (r :: EffectRow) x res (e :: Effect).
(Eq a, Show a, Citizen i12n (Sem r x -> a),
 Citizen res (Sem (e : r) x)) =>
i12n -> String -> res -> String -> res -> Law e r
Law Sem '[] a -> a
forall a. Sem '[] a -> a
run

instance MakeLaw e '[Embed IO] where
  mkLaw :: String -> res -> String -> res -> Law e '[Embed IO]
mkLaw = (Sem '[Embed IO] a -> IO a)
-> String -> res -> String -> res -> Law e '[Embed IO]
forall a i12n (r :: EffectRow) x res (e :: Effect).
(Eq a, Show a, Citizen i12n (Sem r x -> IO a),
 Citizen res (Sem (e : r) x)) =>
i12n -> String -> res -> String -> res -> Law e r
LawIO Sem '[Embed IO] a -> IO a
forall (m :: * -> *) a. Monad m => Sem '[Embed m] a -> m a
runM


------------------------------------------------------------------------------
-- | Produces a QuickCheck-able 'Property' corresponding to whether the given
-- interpreter satisfies the 'Law'.
runLaw :: InterpreterFor e r -> Law e r -> Property
runLaw :: InterpreterFor e r -> Law e r -> Property
runLaw InterpreterFor e r
i12n (Law i12n
finish String
str1 res
a String
str2 res
b) = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  ([String]
_, (Sem r x -> a
lower, Sem r x -> a
_)) <- i12n -> i12n -> Gen ([String], (Sem r x -> a, Sem r x -> a))
forall r a. Citizen r a => r -> r -> Gen ([String], (a, a))
getCitizen i12n
finish i12n
finish
  ([String]
args, (Sem (e : r) x
ma, Sem (e : r) x
mb)) <- res -> res -> Gen ([String], (Sem (e : r) x, Sem (e : r) x))
forall r a. Citizen r a => r -> r -> Gen ([String], (a, a))
getCitizen res
a res
b
  let run_it :: Sem (e : r) x -> a
run_it = Sem r x -> a
lower (Sem r x -> a) -> (Sem (e : r) x -> Sem r x) -> Sem (e : r) x -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (e : r) x -> Sem r x
InterpreterFor e r
i12n
      a' :: a
a' = Sem (e : r) x -> a
run_it Sem (e : r) x
ma
      b' :: a
b' = Sem (e : r) x -> a
run_it Sem (e : r) x
mb
  Property -> Gen Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
      (String -> a -> String -> a -> [String] -> String
forall a.
Show a =>
String -> a -> String -> a -> [String] -> String
mkCounterexampleString String
str1 a
a' String
str2 a
b' [String]
args)
      (a
a' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b')
runLaw InterpreterFor e r
i12n (LawIO i12n
finish String
str1 res
a String
str2 res
b) = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  ([String]
_, (Sem r x -> IO a
lower, Sem r x -> IO a
_)) <- i12n -> i12n -> Gen ([String], (Sem r x -> IO a, Sem r x -> IO a))
forall r a. Citizen r a => r -> r -> Gen ([String], (a, a))
getCitizen i12n
finish i12n
finish
  ([String]
args, (Sem (e : r) x
ma, Sem (e : r) x
mb)) <- res -> res -> Gen ([String], (Sem (e : r) x, Sem (e : r) x))
forall r a. Citizen r a => r -> r -> Gen ([String], (a, a))
getCitizen res
a res
b
  let run_it :: Sem (e : r) x -> IO a
run_it = Sem r x -> IO a
lower (Sem r x -> IO a)
-> (Sem (e : r) x -> Sem r x) -> Sem (e : r) x -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (e : r) x -> Sem r x
InterpreterFor e r
i12n
  Property -> Gen Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    a
a' <- Sem (e : r) x -> IO a
run_it Sem (e : r) x
ma
    a
b' <- Sem (e : r) x -> IO a
run_it Sem (e : r) x
mb
    Property -> IO Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
      String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        (String -> a -> String -> a -> [String] -> String
forall a.
Show a =>
String -> a -> String -> a -> [String] -> String
mkCounterexampleString String
str1 a
a' String
str2 a
b' [String]
args)
        (a
a' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b')


------------------------------------------------------------------------------
-- | Make a string representation for a failing 'runLaw' property.
mkCounterexampleString
    :: Show a
    => String
    -> a
    -> String
    -> a
    -> [String]
    -> String
mkCounterexampleString :: String -> a -> String -> a -> [String] -> String
mkCounterexampleString String
str1 a
a String
str2 a
b [String]
args =
  [String] -> String
forall a. Monoid a => [a] -> a
mconcat
    [ String -> [String] -> String
printf String
str1 [String]
args , String
" (result: " , a -> String
forall a. Show a => a -> String
show a
a , String
")\n /= \n"
    , String -> [String] -> String
printf String
str2 [String]
args , String
" (result: " , a -> String
forall a. Show a => a -> String
show a
b , String
")"
    ]


------------------------------------------------------------------------------
-- | A bare-boned implementation of printf. This function will replace tokens
-- of the form @"%n"@ in the first string with @args !! n@.
--
-- This will only work for indexes up to 9.
--
-- For example:
--
-- >>> printf "hello %1 %2% %3 %1" ["world", "50"]
-- "hello world 50% %3 world"
printf :: String -> [String] -> String
printf :: String -> [String] -> String
printf String
str [String]
args = String -> String
splitArgs String
str
  where
    splitArgs :: String -> String
    splitArgs :: String -> String
splitArgs String
s =
      case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'%') String
s of
        (String
as, String
"") -> String
as
        (String
as, Char
_ : Char
b : String
bs)
          | Char -> Bool
isDigit Char
b
          , let d :: Int
d = String -> Int
forall a. Read a => String -> a
read [Char
b] Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
          , Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
args
            -> String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([String]
args [String] -> Int -> String
forall a. [a] -> Int -> a
!! Int
d) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
splitArgs String
bs
        (String
as, Char
_ : String
bs) ->  String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"%" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
splitArgs String
bs