polysemy-commutative.hs

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE DeriveAnyClass            #-}
{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE DerivingStrategies        #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE InstanceSigs              #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE MultiWayIf                #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

{-# OPTIONS_GHC -Wredundant-constraints #-}

{-# LANGUAGE ConstraintKinds #-}
module Lib
  where

import qualified Data.Set as S
import Data.Set (Set)
import           Control.Applicative (liftA2)
import           Control.Monad (guard, void)
import           Data.Function (on)
import           Data.Functor.Classes (Eq1)
import           Data.IORef (IORef, newIORef, readIORef, writeIORef)
import           Data.Kind (Type, Constraint)
import           Data.Maybe (isJust, fromMaybe, maybeToList)
import qualified Data.Vector.Unboxed.Mutable as V
import           Data.Vector.Unboxed.Mutable (IOVector)
import           GHC.Generics (Generic, Generic1)
import           Test.QuickCheck (quickCheck, Gen, Positive(..), Property, arbitrary, elements, frequency, shrink, (===), discard, ioProperty, property)
import           Test.QuickCheck.Monadic (monadicIO)
import           Test.StateMachine
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Polysemy
import Polysemy.Internal.Union
import Polysemy.State (State)
import Polysemy.State hiding (State(..))
import Data.Functor.Const
import Polysemy.Internal (send, liftSem)
import Data.Typeable (Typeable)
import Data.Data (Proxy(Proxy), Data)
import Test.QuickCheck.Gen (oneof)
import Type.Reflection
import Data.Coerce (coerce)
import Data.Typeable ((:~:))
import Polysemy.Internal
import Unsafe.Coerce
import Polysemy.Law
import Generics.Kind
import Generics.Kind.TH
import GHC.Exts (type (~~))
import Data.Foldable (traverse_)
import Polysemy.Output
import Polysemy.State
import Debug.Trace (traceM)

data ATypeRep where
  ATypeRep :: TypeRep (a :: Type) -> ATypeRep

instance Eq ATypeRep where
  ATypeRep a == ATypeRep b = (==) (SomeTypeRep a) (SomeTypeRep b)

instance Ord ATypeRep where
  ATypeRep a `compare` ATypeRep b = compare (SomeTypeRep a) (SomeTypeRep b)

type family TypesOf (f :: LoT Effect -> Type) :: [Type] where
  TypesOf (M1 _1 _2 f) = TypesOf f
  TypesOf (f :+: g) = Append (TypesOf f) (TypesOf g)
  TypesOf (('Kon (~~) ':@: Var1 ':@: 'Kon a) :=>: f) = '[a]
  TypesOf (('Kon ((~~) a) ':@: Var1) :=>: f) = '[a]

data CircleBuffer m a where
  PutE :: Int -> CircleBuffer m ()
  GetE :: CircleBuffer m Int
  LenE :: CircleBuffer m Int

deriving instance Show (CircleBuffer m a)

data Worker m a where
  Worker :: Bool -> Int -> Worker m ()

deriving instance Show (Worker m ())

makeSem ''CircleBuffer
deriveGenericK ''CircleBuffer
deriveGenericK ''Worker

deriveGenericK ''State
deriveGenericK ''Output

deriving instance Show s => Show (State s (Sem r) a)
deriving instance Show o => Show (Output o (Sem r) a)

type a :~~~: b = 'Kon (~~) ':@: a ':@: b

------------------------------------------------------------------------------

class GTypesOf (f :: LoT Effect -> Type) where
  gtypesofk :: Set ATypeRep

instance (GTypesOf f, GTypesOf g) => GTypesOf (f :+: g) where
  gtypesofk = gtypesofk @f <> gtypesofk @g

instance Typeable a => GTypesOf (Var1 :~~~: 'Kon (a :: Type) :=>: _1) where
  gtypesofk = S.singleton $ ATypeRep $ typeRep @a

instance (GTypesOf f) => GTypesOf (M1 _1 _2 f) where
  gtypesofk = gtypesofk @f


------------------------------------------------------------------------------

class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where
  garbitraryk :: [Gen (f x)]

instance GArbitraryK a U1 where
  garbitraryk = pure $ pure U1

instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :*: g) where
  garbitraryk = liftA2 (liftA2 (:*:)) (garbitraryk @a) (garbitraryk @a)

instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) where
  garbitraryk = fmap (fmap L1) (garbitraryk @a @f)
             <> fmap (fmap R1) (garbitraryk @a @g)

instance GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where
  garbitraryk = fmap SuchThat <$> garbitraryk1

instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where
  garbitraryk = []

instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where
  garbitraryk = []

instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where
  garbitraryk = fmap M1 <$> garbitraryk @a

------------------------------------------------------------------------------

type family ArbitraryForAll (as :: [Type]) (m :: Type -> Type) :: Constraint where
  ArbitraryForAll '[] f = ()
  ArbitraryForAll (a ': as) f = (Eq a, Show a, GArbitraryK a (RepK (f a)), ArbitraryForAll as f)

type Yo e m = ArbitraryForAll (TypesOf (RepK e)) (e m)

------------------------------------------------------------------------------

debugEffGen :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)
debugEffGen = fmap toK $ oneof $ garbitraryk @a @(RepK (e m a))

debugGen :: Yo CircleBuffer m => Gen (CircleBuffer m Int)
debugGen = debugEffGen

---

data SomeEff e (r :: EffectRow) where
  SomeEff :: (Member e r, Eq a, Show a, Show (e (Sem r) a)) => e (Sem r) a -> SomeEff e r

instance Show (SomeEff e r) where
  show (SomeEff ema) = show ema

instance Show (SomeSomeEff r) where
  show (SomeSomeEff sse) = show sse


data SomeSomeEff (r :: EffectRow) where
  SomeSomeEff :: SomeEff e r -> SomeSomeEff r

class GetAnEffGen (es :: EffectRow) (r :: EffectRow) where
  getAnEffGen :: [Gen (SomeSomeEff r)]

class GetAParticularEffGen (as :: [Type]) (e :: Effect) (r :: EffectRow) where
  getAParticularEffGen :: [Gen (SomeEff e r)]

instance GetAParticularEffGen '[] e r where
  getAParticularEffGen = []

instance
    ( GetAParticularEffGen as e r
    , Eq a
    , Show a
    , Member e r
    , Show (e (Sem r) a)
    , GenericK (e (Sem r) a)
    , GArbitraryK a (RepK (e (Sem r) a))
    )
    => GetAParticularEffGen (a : as) e r
    where
  getAParticularEffGen = (fmap SomeEff $ debugEffGen @e @a @(Sem r)) : getAParticularEffGen @as @e @r

instance GetAnEffGen '[] r where
  getAnEffGen = []

instance
    (GetAnEffGen es r, GetAParticularEffGen (TypesOf (RepK e)) e r)
    => GetAnEffGen (e ': es) r
    where
  getAnEffGen = fmap (fmap SomeSomeEff) (getAParticularEffGen @(TypesOf (RepK e)) @e @r)
             <> getAnEffGen @es @r


prop_writerStateComm :: Property
prop_writerStateComm =
  prepropCommutative @(State Int) @(Output Int) @'[Output Int, State Int] $ pure . run . evalState 0 . fmap snd . runOutputList



prepropCommutative
    :: forall e1 e2 r
     . ( GetAnEffGen r r
       , GetAnEffGen '[e1] r
       , GetAnEffGen '[e2] r
       )
    => (forall a. Sem r a -> IO a)
    -> Property
prepropCommutative run = property @(Gen Property) $ do
  SomeSomeEff (SomeEff m) <- oneof $ getAnEffGen @r @r
  SomeSomeEff (SomeEff e1) <- oneof $ getAnEffGen @'[e1] @r
  SomeSomeEff (SomeEff e2) <- oneof $ getAnEffGen @'[e2] @r
  pure $
    counterexample (show e1) $
    counterexample (show e2) $
    counterexample (show m) $
      ioProperty $ do
        r1 <- run $ send e1 >> send e2 >> send m
        r2 <- run $ send e2 >> send e1 >> send m
        pure $ r1 === r2



---


synthesizeAny
    :: forall e a m
     . (GArbitraryK a (RepK (e m a)), GenericK (e m a))
    => TypeRep a
    -> Maybe (Gen (e m a))
synthesizeAny _ =
  case garbitraryk @a @(RepK (e m a)) of
    [] -> Nothing
    a -> Just $ fmap toK $ oneof a


------------------------------------------------------------------------------

class GArbitraryK1 (f :: LoT Type -> Type) where
  garbitraryk1 :: [Gen (f x)]

instance (GArbitraryK1 f, GArbitraryK1 g) => GArbitraryK1 (f :*: g) where
  garbitraryk1 = liftA2 (liftA2 (:*:)) garbitraryk1 garbitraryk1

instance Arbitrary t => GArbitraryK1 (Field ('Kon t)) where
  garbitraryk1 = pure $ fmap Field arbitrary

instance (GArbitraryK1 f) => GArbitraryK1 (M1 _1 _2 f) where
  garbitraryk1 = fmap M1 <$> garbitraryk1

instance GArbitraryK1 U1 where
  garbitraryk1 = pure $ pure U1