{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Test.StateMachine.Lockstep.Auxiliary (
Elem(..)
, npAt
, NTraversable(..)
, ntraverse
, ncfmap
, nfmap
, ncfoldMap
, nfoldMap
) where
import Control.Monad.State
import Data.Kind
(Type)
import Prelude
#if !MIN_VERSION_base(4,13,0)
import Data.Monoid
(Monoid)
#endif
import Data.Proxy
import Data.SOP
data Elem (xs :: [k]) (a :: k) where
ElemHead :: Elem (k ': ks) k
ElemTail :: Elem ks k -> Elem (k' ': ks) k
npAt' :: Elem xs a -> NP f xs -> f a
npAt' :: forall {k} (xs :: [k]) (a :: k) (f :: k -> *).
Elem xs a -> NP f xs -> f a
npAt' Elem xs a
ElemHead (f x
f :* NP f xs
_) = f x
f
npAt' (ElemTail Elem ks a
ix) (f x
_ :* NP f xs
fs) = forall {k} (xs :: [k]) (a :: k) (f :: k -> *).
Elem xs a -> NP f xs -> f a
npAt' Elem ks a
ix NP f xs
fs
npAt :: NP f xs -> Elem xs a -> f a
npAt :: forall {k} (f :: k -> *) (xs :: [k]) (a :: k).
NP f xs -> Elem xs a -> f a
npAt = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {k} (xs :: [k]) (a :: k) (f :: k -> *).
Elem xs a -> NP f xs -> f a
npAt'
class NTraversable (f :: (k -> Type) -> [k] -> Type) where
nctraverse :: (Applicative m, All c xs)
=> proxy c
-> (forall a. c a => Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse :: (NTraversable f, Applicative m, SListI xs)
=> (forall a. Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse :: forall {k} (f :: (k -> *) -> [k] -> *) (m :: * -> *) (xs :: [k])
(g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse forall (a :: k). Elem xs a -> g a -> m (h a)
f = forall k (f :: (k -> *) -> [k] -> *) (m :: * -> *)
(c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m (h a))
-> f g xs
-> m (f h xs)
nctraverse (forall {k} (t :: k). Proxy t
Proxy @Top) forall (a :: k). Elem xs a -> g a -> m (h a)
f
ncfmap :: (NTraversable f, All c xs)
=> proxy c
-> (forall a. c a => Elem xs a -> g a -> h a)
-> f g xs -> f h xs
ncfmap :: forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
(xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
(h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap proxy c
p forall (a :: k). c a => Elem xs a -> g a -> h a
f f g xs
xs = forall a. I a -> a
unI forall a b. (a -> b) -> a -> b
$ forall k (f :: (k -> *) -> [k] -> *) (m :: * -> *)
(c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m (h a))
-> f g xs
-> m (f h xs)
nctraverse proxy c
p (\Elem xs a
ix -> forall a. a -> I a
I forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). c a => Elem xs a -> g a -> h a
f Elem xs a
ix) f g xs
xs
nfmap :: (NTraversable f, SListI xs)
=> (forall a. Elem xs a -> g a -> h a)
-> f g xs -> f h xs
nfmap :: forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
(h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap forall (a :: k). Elem xs a -> g a -> h a
f f g xs
xs = forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
(xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
(h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap (forall {k} (t :: k). Proxy t
Proxy @Top) forall (a :: k). Elem xs a -> g a -> h a
f f g xs
xs
ncfoldMap :: forall proxy f g m c xs.
(NTraversable f, Monoid m, All c xs)
=> proxy c
-> (forall a. c a => Elem xs a -> g a -> m)
-> f g xs -> m
ncfoldMap :: forall {k} (proxy :: (k -> Constraint) -> *)
(f :: (k -> *) -> [k] -> *) (g :: k -> *) m (c :: k -> Constraint)
(xs :: [k]).
(NTraversable f, Monoid m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m) -> f g xs -> m
ncfoldMap proxy c
p forall (a :: k). c a => Elem xs a -> g a -> m
f = \f g xs
xs -> forall s a. State s a -> s -> s
execState (f g xs -> State m (f g xs)
aux f g xs
xs) forall a. Monoid a => a
mempty
where
aux :: f g xs -> State m (f g xs)
aux :: f g xs -> State m (f g xs)
aux f g xs
xs = forall k (f :: (k -> *) -> [k] -> *) (m :: * -> *)
(c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m (h a))
-> f g xs
-> m (f h xs)
nctraverse proxy c
p forall (a :: k). c a => Elem xs a -> g a -> State m (g a)
aux' f g xs
xs
aux' :: c a => Elem xs a -> g a -> State m (g a)
aux' :: forall (a :: k). c a => Elem xs a -> g a -> State m (g a)
aux' Elem xs a
ix g a
ga = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (a :: k). c a => Elem xs a -> g a -> m
f Elem xs a
ix g a
ga forall a. Monoid a => a -> a -> a
`mappend`) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return g a
ga
nfoldMap :: (NTraversable f, Monoid m, SListI xs)
=> (forall a. Elem xs a -> g a -> m)
-> f g xs -> m
nfoldMap :: forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap forall (a :: k). Elem xs a -> g a -> m
f f g xs
xs = forall {k} (proxy :: (k -> Constraint) -> *)
(f :: (k -> *) -> [k] -> *) (g :: k -> *) m (c :: k -> Constraint)
(xs :: [k]).
(NTraversable f, Monoid m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m) -> f g xs -> m
ncfoldMap (forall {k} (t :: k). Proxy t
Proxy @Top) forall (a :: k). Elem xs a -> g a -> m
f f g xs
xs