{-# 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


-- | Locally closed values (i.e., not binding forms) of a given type.
-- TODO: come up with a better name
type LC (a :: Hakaru) = '( '[], a )

----------------------------------------------------------------
-- TODO: ideally we'd like to make SArgs totally flat, like tuples and arrays. Is there a way to do that with data families?
-- TODO: is there any good way to reuse 'List1' instead of defining 'SArgs' (aka @List2@)?

-- TODO: come up with a better name for 'End'
-- TODO: unify this with 'List1'? However, strictness differences...
--
-- | The arguments to a @(':$')@ node in the 'Term'; that is, a list
-- of ASTs, where the whole list is indexed by a (type-level) list
-- of the indices of each element.
data SArgs :: ([Hakaru] -> Hakaru -> *) -> [([Hakaru], Hakaru)] -> *
    where
    End :: SArgs abt '[]
    (:*) :: !(abt vars a)
        -> !(SArgs abt args)
        -> SArgs abt ( '(vars, a) ': args)

infixr 5 :* -- Chosen to match (:)

-- TODO: instance Read (SArgs abt args)

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