{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_GHC -Wall #-}

module Topaz.Rec
  ( Rec(..)
  , (<:)
  , map
  , append
  , traverse
  , traverse_
  , zipWith
  , foldMap
  , foldMap1
  , foldl'
    -- * Access
  , get
  , put
  , gets
  , puts
    -- * Conversion
  , fromSingList
  , toSingList
  , fromList
  ) where

import Data.Exists
import Data.Kind (Type)
import Prelude hiding (map,zipWith,foldMap,traverse)
import Topaz.Types (Elem(..),type (++),Rec(..))

import qualified Data.Semigroup as SG

-- | infix RecCons with proper fixity
infixr 7 <:
(<:) :: forall a (f :: a -> Type) (r :: a) (rs :: [a]).  f r -> Rec f rs -> Rec f (r : rs)
<: :: forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
(<:) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons

map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
map :: forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (x :: k). f x -> g x) -> Rec f as -> Rec g as
map forall (x :: k). f x -> g x
_ Rec f as
RecNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
map forall (x :: k). f x -> g x
f (RecCons f r
x Rec f rs
xs) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall (x :: k). f x -> g x
f f r
x) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (x :: k). f x -> g x) -> Rec f as -> Rec g as
map forall (x :: k). f x -> g x
f Rec f rs
xs)

zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
zipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
zipWith forall (x :: k). f x -> g x -> h x
_ Rec f rs
RecNil Rec g rs
RecNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
zipWith forall (x :: k). f x -> g x -> h x
f (RecCons f r
a Rec f rs
as) (RecCons g r
b Rec g rs
bs) =
  forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (forall (x :: k). f x -> g x -> h x
f f r
a g r
b) (forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (rs :: [k]).
(forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
zipWith forall (x :: k). f x -> g x -> h x
f Rec f rs
as Rec g rs
bs)

-- | Strict left fold over the elements of a record.
foldl' :: forall f a rs.
     (forall x. a -> f x -> a) -- ^ Reduction
  -> a -- ^ Initial accumulator
  -> Rec f rs -- ^ Record
  -> a
foldl' :: forall {k} (f :: k -> *) a (rs :: [k]).
(forall (x :: k). a -> f x -> a) -> a -> Rec f rs -> a
foldl' forall (x :: k). a -> f x -> a
g !a
a0 = forall (ss :: [k]). a -> Rec f ss -> a
go a
a0 where
  go :: forall ss. a -> Rec f ss -> a
  go :: forall (ss :: [k]). a -> Rec f ss -> a
go !a
a Rec f ss
RecNil = a
a
  go !a
a (RecCons f r
r Rec f rs
rs) = forall (ss :: [k]). a -> Rec f ss -> a
go (forall (x :: k). a -> f x -> a
g a
a f r
r) Rec f rs
rs

-- | Map each element of a record to a monoid and combine the results.
foldMap :: forall f m rs. Monoid m
  => (forall x. f x -> m)
  -> Rec f rs
  -> m
foldMap :: forall {k} (f :: k -> *) m (rs :: [k]).
Monoid m =>
(forall (x :: k). f x -> m) -> Rec f rs -> m
foldMap forall (x :: k). f x -> m
f = forall (ss :: [k]). m -> Rec f ss -> m
go forall a. Monoid a => a
mempty
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: forall (ss :: [k]). m -> Rec f ss -> m
go !m
m Rec f ss
record = case Rec f ss
record of
    Rec f ss
RecNil -> m
m
    RecCons f r
r Rec f rs
rs -> forall (ss :: [k]). m -> Rec f ss -> m
go (forall a. Monoid a => a -> a -> a
mappend m
m (forall (x :: k). f x -> m
f f r
r)) Rec f rs
rs
  {-# INLINABLE go #-}
{-# INLINE foldMap #-}

foldMap1 :: forall f m r rs. Semigroup m
  => (forall x. f x -> m)
  -> Rec f (r ': rs)
  -> m
foldMap1 :: forall {k} (f :: k -> *) m (r :: k) (rs :: [k]).
Semigroup m =>
(forall (x :: k). f x -> m) -> Rec f (r : rs) -> m
foldMap1 forall (x :: k). f x -> m
f (RecCons f r
b Rec f rs
bs) = forall (ss :: [k]). m -> Rec f ss -> m
go (forall (x :: k). f x -> m
f f r
b) Rec f rs
bs
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: forall (ss :: [k]). m -> Rec f ss -> m
go !m
m Rec f ss
record = case Rec f ss
record of
    Rec f ss
RecNil -> m
m
    RecCons f r
r Rec f rs
rs -> forall (ss :: [k]). m -> Rec f ss -> m
go (m
m forall a. Semigroup a => a -> a -> a
SG.<> (forall (x :: k). f x -> m
f f r
r)) Rec f rs
rs
  {-# INLINABLE go #-}
{-# INLINE foldMap1 #-}

traverse
  :: Applicative h
  => (forall x. f x -> h (g x))
  -> Rec f rs
  -> h (Rec g rs)
traverse :: forall {k} (h :: * -> *) (f :: k -> *) (g :: k -> *) (rs :: [k]).
Applicative h =>
(forall (x :: k). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
traverse forall (x :: k). f x -> h (g x)
_ Rec f rs
RecNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). Rec f '[]
RecNil
traverse forall (x :: k). f x -> h (g x)
f (RecCons f r
x Rec f rs
xs) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). f x -> h (g x)
f f r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (h :: * -> *) (f :: k -> *) (g :: k -> *) (rs :: [k]).
Applicative h =>
(forall (x :: k). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
traverse forall (x :: k). f x -> h (g x)
f Rec f rs
xs
{-# INLINABLE traverse #-}

traverse_
  :: Applicative h
  => (forall x. f x -> h b)
  -> Rec f rs
  -> h ()
traverse_ :: forall {k} (h :: * -> *) (f :: k -> *) b (rs :: [k]).
Applicative h =>
(forall (x :: k). f x -> h b) -> Rec f rs -> h ()
traverse_ forall (x :: k). f x -> h b
_ Rec f rs
RecNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
traverse_ forall (x :: k). f x -> h b
f (RecCons f r
x Rec f rs
xs) = forall (x :: k). f x -> h b
f f r
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall {k} (h :: * -> *) (f :: k -> *) b (rs :: [k]).
Applicative h =>
(forall (x :: k). f x -> h b) -> Rec f rs -> h ()
traverse_ forall (x :: k). f x -> h b
f Rec f rs
xs
{-# INLINABLE traverse_ #-}

get :: Elem rs r -> Rec f rs -> f r
get :: forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> Rec f rs -> f r
get Elem rs r
ElemHere (RecCons f r
r Rec f rs
_) = f r
r
get (ElemThere Elem rs r
ix) (RecCons f r
_ Rec f rs
rs) = forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> Rec f rs -> f r
get Elem rs r
ix Rec f rs
rs

put :: Elem rs r -> f r -> Rec f rs -> Rec f rs
put :: forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> f r -> Rec f rs -> Rec f rs
put Elem rs r
ElemHere f r
r' (RecCons f r
_ Rec f rs
rs) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
r' Rec f rs
rs
put (ElemThere Elem rs r
ix) f r
r' (RecCons f r
r Rec f rs
rs) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
r (forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> f r -> Rec f rs -> Rec f rs
put Elem rs r
ix f r
r' Rec f rs
rs)

gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
gets :: forall {k} (rs :: [k]) (ss :: [k]) (f :: k -> *).
Rec (Elem rs) ss -> Rec f rs -> Rec f ss
gets Rec (Elem rs) ss
ixs Rec f rs
rec = forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (x :: k). f x -> g x) -> Rec f as -> Rec g as
map (\Elem rs x
e -> forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> Rec f rs -> f r
get Elem rs x
e Rec f rs
rec) Rec (Elem rs) ss
ixs

puts :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
puts :: forall {k} (rs :: [k]) (ss :: [k]) (f :: k -> *).
Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
puts Rec (Elem rs) ss
RecNil Rec f rs
rs Rec f ss
_ = Rec f rs
rs
puts (RecCons Elem rs r
ix Rec (Elem rs) rs
ixs) Rec f rs
rs (RecCons f r
s Rec f rs
ss) = forall {k} (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> f r -> Rec f rs -> Rec f rs
put Elem rs r
ix f r
s (forall {k} (rs :: [k]) (ss :: [k]) (f :: k -> *).
Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
puts Rec (Elem rs) rs
ixs Rec f rs
rs Rec f rs
ss)

append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
append :: forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
append Rec f as
RecNil Rec f bs
ys = Rec f bs
ys
append (RecCons f r
x Rec f rs
xs) Rec f bs
ys = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
x (forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
append Rec f rs
xs Rec f bs
ys)

fromSingList :: SingList as -> Rec Sing as
fromSingList :: forall {k} (as :: [k]). SingList as -> Rec Sing as
fromSingList SingList as
SingListNil = forall {k} (f :: k -> *). Rec f '[]
RecNil
fromSingList (SingListCons Sing r
r SingList rs
rs) = forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons Sing r
r (forall {k} (as :: [k]). SingList as -> Rec Sing as
fromSingList SingList rs
rs)

toSingList :: Rec Sing as -> SingList as
toSingList :: forall {k} (as :: [k]). Rec Sing as -> SingList as
toSingList Rec Sing as
RecNil = forall {k}. SingList '[]
SingListNil
toSingList (RecCons Sing r
r Rec Sing rs
rs) = forall {k} (r :: k) (rs :: [k]).
Sing r -> SingList rs -> SingList (r : rs)
SingListCons Sing r
r (forall {k} (as :: [k]). Rec Sing as -> SingList as
toSingList Rec Sing rs
rs)

fromList :: [Exists f] -> Exists (Rec f)
fromList :: forall {k} (f :: k -> *). [Exists f] -> Exists (Rec f)
fromList [] = forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists forall {k} (f :: k -> *). Rec f '[]
RecNil
fromList (Exists f a
x : [Exists f]
xs) = case forall {k} (f :: k -> *). [Exists f] -> Exists (Rec f)
fromList [Exists f]
xs of
  Exists Rec f a
ys -> forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f a
x Rec f a
ys)