{-# 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 Prelude hiding (map,zipWith,foldMap,traverse)
import Topaz.Types (Elem(..),type (++),Rec(..))
import Data.Exists
import qualified Data.Semigroup as SG

-- | infix RecCons with proper fixity
infixr 7 <:
(<:) :: forall a (f :: a -> *) (r :: a) (rs :: [a]).  f r -> Rec f rs -> Rec f (r : rs)
<: :: f r -> Rec f rs -> Rec f (r : rs)
(<:) = 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 (x :: k). f x -> g x) -> Rec f as -> Rec g as
map forall (x :: k). f x -> g x
_ Rec f as
RecNil = Rec g as
forall k (f :: k -> *). Rec f '[]
RecNil
map forall (x :: k). f x -> g x
f (RecCons f r
x Rec f rs
xs) = g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (f r -> g r
forall (x :: k). f x -> g x
f f r
x) ((forall (x :: k). f x -> g x) -> Rec f rs -> Rec g rs
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 (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 = Rec h rs
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) =
  h r -> Rec h rs -> Rec h (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (f r -> g r -> h r
forall (x :: k). f x -> g x -> h x
f f r
a g r
g r
b) ((forall (x :: k). f x -> g x -> h x)
-> Rec f rs -> Rec g rs -> Rec h rs
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
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 (x :: k). a -> f x -> a) -> a -> Rec f rs -> a
foldl' forall (x :: k). a -> f x -> a
g !a
a0 = a -> Rec f rs -> a
forall (ss :: [k]). a -> Rec f ss -> a
go a
a0 where
  go :: forall ss. a -> Rec f ss -> a
  go :: 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) = a -> Rec f rs -> a
forall (ss :: [k]). a -> Rec f ss -> a
go (a -> f r -> a
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 (x :: k). f x -> m) -> Rec f rs -> m
foldMap forall (x :: k). f x -> m
f = m -> Rec f rs -> m
forall (ss :: [k]). m -> Rec f ss -> m
go m
forall a. Monoid a => a
mempty
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: 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 -> m -> Rec f rs -> m
forall (ss :: [k]). m -> Rec f ss -> m
go (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend m
m (f r -> 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 (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) = m -> Rec f rs -> m
forall (ss :: [k]). m -> Rec f ss -> m
go (f r -> m
forall (x :: k). f x -> m
f f r
b) Rec f rs
bs
  where
  go :: forall ss. m -> Rec f ss -> m
  go :: 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 -> m -> Rec f rs -> m
forall (ss :: [k]). m -> Rec f ss -> m
go (m
m m -> m -> m
forall a. Semigroup a => a -> a -> a
SG.<> (f r -> m
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 (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 = Rec g '[] -> h (Rec g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec g '[]
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) = g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons (g r -> Rec g rs -> Rec g (r : rs))
-> h (g r) -> h (Rec g rs -> Rec g (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r -> h (g r)
forall (x :: k). f x -> h (g x)
f f r
x h (Rec g rs -> Rec g (r : rs))
-> h (Rec g rs) -> h (Rec g (r : rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
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 (x :: k). f x -> h b) -> Rec f rs -> h ()
traverse_ forall (x :: k). f x -> h b
_ Rec f rs
RecNil = () -> h ()
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) = f r -> h b
forall (x :: k). f x -> h b
f f r
x h b -> h () -> h ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (forall (x :: k). f x -> h b) -> Rec f rs -> h ()
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 :: Elem rs r -> Rec f rs -> f r
get Elem rs r
ElemHere (RecCons f r
r Rec f rs
_) = f r
f r
r
get (ElemThere Elem rs r
ix) (RecCons f r
_ Rec f rs
rs) = Elem rs r -> Rec f rs -> f r
forall k (rs :: [k]) (r :: k) (f :: k -> *).
Elem rs r -> Rec f rs -> f r
get Elem rs r
ix Rec f rs
Rec f rs
rs

put :: Elem rs r -> f r -> Rec f rs -> Rec f rs
put :: 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) = 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 f r
r' Rec f rs
rs
put (ElemThere Elem rs r
ix) f r
r' (RecCons f r
r Rec f rs
rs) = 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 f r
r (Elem rs r -> f r -> Rec f rs -> Rec f rs
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
Rec f rs
rs)

gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
gets Rec (Elem rs) ss
ixs Rec f rs
rec = (forall (x :: k). Elem rs x -> f x) -> Rec (Elem rs) ss -> Rec f ss
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 -> Elem rs x -> Rec f rs -> f x
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 :: 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) = Elem rs r -> f r -> Rec f rs -> Rec f rs
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
f r
s (Rec (Elem rs) rs -> Rec f rs -> Rec f rs -> Rec f rs
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
Rec f rs
ss)

append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
append Rec f as
RecNil Rec f bs
ys = Rec f bs
Rec f (as ++ bs)
ys
append (RecCons f r
x Rec f rs
xs) Rec f bs
ys = f r -> Rec f (rs ++ bs) -> Rec f (r : (rs ++ bs))
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons f r
x (Rec f rs -> Rec f bs -> Rec f (rs ++ bs)
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 :: SingList as -> Rec Sing as
fromSingList SingList as
SingListNil = Rec Sing as
forall k (f :: k -> *). Rec f '[]
RecNil
fromSingList (SingListCons Sing r
r SingList rs
rs) = Sing r -> Rec Sing rs -> Rec Sing (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
RecCons Sing r
r (SingList rs -> Rec Sing rs
forall k (as :: [k]). SingList as -> Rec Sing as
fromSingList SingList rs
rs)

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

fromList :: [Exists f] -> Exists (Rec f)
fromList :: [Exists f] -> Exists (Rec f)
fromList [] = Rec f '[] -> Exists (Rec f)
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists Rec f '[]
forall k (f :: k -> *). Rec f '[]
RecNil
fromList (Exists f a
x : [Exists f]
xs) = case [Exists f] -> Exists (Rec f)
forall k (f :: k -> *). [Exists f] -> Exists (Rec f)
fromList [Exists f]
xs of
  Exists Rec f a
ys -> Rec f (a : a) -> Exists (Rec f)
forall k (f :: k -> *) (a :: k). f a -> Exists f
Exists (f a -> Rec f a -> Rec f (a : a)
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)