{-# 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'
, get
, put
, gets
, puts
, 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
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)
foldl' :: forall f a rs.
(forall x. a -> f x -> a)
-> a
-> Rec f rs
-> 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
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)