{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}

-- This file is part of the Wire Server implementation.
--
-- Copyright (C) 2022 Wire Swiss GmbH <opensource@wire.com>
--
-- This program is free software: you can redistribute it and/or modify it under
-- the terms of the GNU Affero General Public License as published by the Free
-- Software Foundation, either version 3 of the License, or (at your option) any
-- later version.
--
-- This program is distributed in the hope that it will be useful, but WITHOUT
-- ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
-- FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for more
-- details.
--
-- You should have received a copy of the GNU Affero General Public License along
-- with this program. If not, see <https://www.gnu.org/licenses/>.

module Wire.Sem.Now.Spec (propsForInterpreter) where

import Imports
import Polysemy
import Polysemy.Check
import Polysemy.Input
import Test.Hspec
import Test.Hspec.QuickCheck
import Test.QuickCheck
import qualified Wire.Sem.Now as E

propsForInterpreter ::
  (PropConstraints r f) =>
  String ->
  (forall a. Sem r a -> IO (f a)) ->
  Spec
propsForInterpreter :: forall (r :: EffectRow) (f :: * -> *).
PropConstraints r f =>
String -> (forall a. Sem r a -> IO (f a)) -> Spec
propsForInterpreter String
interpreter forall a. Sem r a -> IO (f a)
lower = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
interpreter (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"now/now" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ Maybe (f Bool -> String)
-> (forall a. Sem r a -> IO (f a)) -> Property
forall (r :: EffectRow) (f :: * -> *).
PropConstraints r f =>
Maybe (f Bool -> String)
-> (forall a. Sem r a -> IO (f a)) -> Property
prop_nowNow Maybe (f Bool -> String)
forall a. Maybe a
Nothing Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower

-- | All the constraints we need to generalize properties in this module.
-- A regular type synonym doesn't work due to dreaded impredicative
-- polymorphism.
class
  (Functor f, Member E.Now r, Member (Input ()) r, forall z. (Show z) => Show (f z), forall z. (Eq z) => Eq (f z)) =>
  PropConstraints r f

instance
  (Functor f, Member E.Now r, Member (Input ()) r, forall z. (Show z) => Show (f z), forall z. (Eq z) => Eq (f z)) =>
  PropConstraints r f

prop_nowNow ::
  (PropConstraints r f) =>
  Maybe (f Bool -> String) ->
  (forall a. Sem r a -> IO (f a)) ->
  Property
prop_nowNow :: forall (r :: EffectRow) (f :: * -> *).
PropConstraints r f =>
Maybe (f Bool -> String)
-> (forall a. Sem r a -> IO (f a)) -> Property
prop_nowNow =
  -- NOTE: This @Input ()@ effect is a workaround to an oversight in
  -- @polysemy-check@. 'prepropLaw' wants to synthesize some actions to run
  -- before and after its generators, and check their results for equality. We
  -- can't use 'Now' as this effect, because 'E.get' won't return equivalent
  -- results! And we can't keep it empty, because that triggers a crash in
  -- @polysemy-check@. Thus @Input ()@, which isn't beautiful, but works fine.
  forall (effs :: EffectRow) x (r :: EffectRow) a (f :: * -> *).
(forall z. Eq z => Eq (f z), forall z. Show z => Show (f z), Eq a,
 Show a, Functor f, ArbitraryEff effs r, Eq x, Show x) =>
Gen (Law r x a)
-> Maybe (f a -> String)
-> (forall z. Sem r (a, z) -> IO (f (a, z)))
-> Property
prepropLaw @'[Input ()] (Gen (Law r () Bool)
 -> Maybe (f Bool -> String)
 -> (forall z. Sem r (Bool, z) -> IO (f (Bool, z)))
 -> Property)
-> Gen (Law r () Bool)
-> Maybe (f Bool -> String)
-> (forall z. Sem r (Bool, z) -> IO (f (Bool, z)))
-> Property
forall a b. (a -> b) -> a -> b
$ do
    Law r () Bool -> Gen (Law r () Bool)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Law r () Bool -> Gen (Law r () Bool))
-> Law r () Bool -> Gen (Law r () Bool)
forall a b. (a -> b) -> a -> b
$
      Sem r Bool -> Sem r Bool -> Law r () Bool
forall (r :: EffectRow) a. Sem r a -> Sem r a -> Law r () a
simpleLaw
        ((UTCTime -> UTCTime -> Bool)
-> Sem r UTCTime -> Sem r UTCTime -> Sem r Bool
forall a b c. (a -> b -> c) -> Sem r a -> Sem r b -> Sem r c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Sem r UTCTime
forall (r :: EffectRow). Member Now r => Sem r UTCTime
E.get Sem r UTCTime
forall (r :: EffectRow). Member Now r => Sem r UTCTime
E.get)
        ( Bool -> Sem r Bool
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
        )