{-# LANGUAGE CPP
, DataKinds
, PolyKinds
, GADTs
, RankNTypes
, TypeOperators
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.SArgs
( module Language.Hakaru.Syntax.SArgs
) where
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (pure,(<$>),(<*>),Applicative)
import Data.Monoid (Monoid(mempty,mappend))
#endif
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
type LC (a :: Hakaru) = '( '[], a )
data SArgs :: ([Hakaru] -> Hakaru -> *) -> [([Hakaru], Hakaru)] -> *
where
End :: SArgs abt '[]
(:*) :: !(abt vars a)
-> !(SArgs abt args)
-> SArgs abt ( '(vars, a) ': args)
infixr 5 :*
instance Show2 abt => Show1 (SArgs abt) where
showsPrec1 :: Int -> SArgs abt i -> ShowS
showsPrec1 Int
_ SArgs abt i
End = String -> ShowS
showString String
"End"
showsPrec1 Int
p (abt vars a
e :* SArgs abt args
es) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5)
( Int -> abt vars a -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) abt vars a
e
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :* "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SArgs abt args -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SArgs abt args
es
)
instance Show2 abt => Show (SArgs abt args) where
showsPrec :: Int -> SArgs abt args -> ShowS
showsPrec = Int -> SArgs abt args -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: SArgs abt args -> String
show = SArgs abt args -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Eq2 abt => Eq1 (SArgs abt) where
eq1 :: SArgs abt i -> SArgs abt i -> Bool
eq1 SArgs abt i
End SArgs abt i
End = Bool
True
eq1 (abt vars a
x :* SArgs abt args
xs) (abt vars a
y :* SArgs abt args
ys) = abt vars a -> abt vars a -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt vars a
x abt vars a
abt vars a
y Bool -> Bool -> Bool
&& SArgs abt args -> SArgs abt args -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 SArgs abt args
xs SArgs abt args
SArgs abt args
ys
instance Eq2 abt => Eq (SArgs abt args) where
== :: SArgs abt args -> SArgs abt args -> Bool
(==) = SArgs abt args -> SArgs abt args -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Functor21 SArgs where
fmap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> SArgs a j -> SArgs b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (a vars a
e :* SArgs a args
es) = a vars a -> b vars a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a vars a
e b vars a -> SArgs b args -> SArgs b ('(vars, a) : args)
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> SArgs a args -> SArgs b args
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f SArgs a args
es
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ SArgs a j
End = SArgs b j
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
instance Foldable21 SArgs where
foldMap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> SArgs a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (a vars a
e :* SArgs a args
es) = a vars a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a vars a
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> SArgs a args -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f SArgs a args
es
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ SArgs a j
End = m
forall a. Monoid a => a
mempty
instance Traversable21 SArgs where
traverse21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> SArgs a j -> f (SArgs b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (a vars a
e :* SArgs a args
es) = b vars a -> SArgs b args -> SArgs b ('(vars, a) : args)
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
(:*) (b vars a -> SArgs b args -> SArgs b ('(vars, a) : args))
-> f (b vars a) -> f (SArgs b args -> SArgs b ('(vars, a) : args))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a vars a -> f (b vars a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a vars a
e f (SArgs b args -> SArgs b ('(vars, a) : args))
-> f (SArgs b args) -> f (SArgs b ('(vars, a) : args))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> SArgs a args -> f (SArgs b args)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f SArgs a args
es
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ SArgs a j
End = SArgs b '[] -> f (SArgs b '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure SArgs b '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
type SArgsSing = SArgs (Pointwise (Lift1 ()) Sing)
getSArgsSing
:: forall abt xs m
. (Applicative m)
=> (forall ys a . abt ys a -> m (Sing a))
-> SArgs abt xs
-> m (SArgsSing xs)
getSArgsSing :: (forall (ys :: [Hakaru]) (a :: Hakaru). abt ys a -> m (Sing a))
-> SArgs abt xs -> m (SArgsSing xs)
getSArgsSing forall (ys :: [Hakaru]) (a :: Hakaru). abt ys a -> m (Sing a)
k = (forall (h :: [Hakaru]) (i :: Hakaru).
abt h i -> m (Pointwise (Lift1 ()) Sing h i))
-> SArgs abt xs -> m (SArgsSing xs)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 ((forall (h :: [Hakaru]) (i :: Hakaru).
abt h i -> m (Pointwise (Lift1 ()) Sing h i))
-> SArgs abt xs -> m (SArgsSing xs))
-> (forall (h :: [Hakaru]) (i :: Hakaru).
abt h i -> m (Pointwise (Lift1 ()) Sing h i))
-> SArgs abt xs
-> m (SArgsSing xs)
forall a b. (a -> b) -> a -> b
$ \abt h i
x -> Lift1 () h -> Sing i -> Pointwise (Lift1 ()) Sing h i
forall k0 k1 (f :: k0 -> *) (x :: k0) (g :: k1 -> *) (y :: k1).
f x -> g y -> Pointwise f g x y
Pw (() -> Lift1 () h
forall k a (i :: k). a -> Lift1 a i
Lift1 ()) (Sing i -> Pointwise (Lift1 ()) Sing h i)
-> m (Sing i) -> m (Pointwise (Lift1 ()) Sing h i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt h i -> m (Sing i)
forall (ys :: [Hakaru]) (a :: Hakaru). abt ys a -> m (Sing a)
k abt h i
x