{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE ExplicitNamespaces    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | This module exports the `Product` and `Sum` type, and type- and valuelevel
--   functions on these types.
module Generics.POSable.Representation
  ( type (++)
  , ProductType(..)
  , concatPT
  , Product(..)
  , concatP
  , SumType(..)
  , Sum(..)
  , Merge
  , FoldMerge
  , MapConcat
  , Concat
  , Ground(..)
  , mergeT
  , merge
  , splitLeft
  , splitRight
  , unConcatP
  , Undef(..)
) where
import           Data.Kind
import           Data.Typeable (Typeable)
import           GHC.Generics  as GHC
import           Generics.SOP  as SOP (All, All2, Generic)

-- | Concatenation of typelevel lists
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
    '[]       ++ ys = ys
    (x ': xs) ++ ys = x ': xs ++ ys

infixr 5 ++


-- | The set of types that can exist in the sums.
--   This set can be extended by the user by providing an instance of Ground
--   for their types. The mkGround function gives a default value for the type.
--   Ground depends on Typeable, as this makes it possible for library users
--   to inspect the types of the contents of the sums.
class (Typeable a) => Ground a where
  mkGround :: a

-----------------------------------------------------------------------
-- Heterogeneous lists with explicit types

-- | Type witness for `Product`
data ProductType :: [[Type]] -> Type where
  PTNil :: ProductType '[]
  PTCons :: SumType x -> ProductType xs -> ProductType (x ': xs)

instance (All2 Show (Map2TypeRep xs)) => Show (ProductType xs) where
  show :: ProductType xs -> String
show ProductType xs
PTNil         = String
"PTNil"
  show (PTCons SumType x
a ProductType xs
as) = String
"PTCons" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SumType x -> String
forall a. Show a => a -> String
show SumType x
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ProductType xs -> String
forall a. Show a => a -> String
show ProductType xs
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Concatenates `ProductType` values
concatPT :: ProductType x -> ProductType y -> ProductType (x ++ y)
concatPT :: ProductType x -> ProductType y -> ProductType (x ++ y)
concatPT ProductType x
PTNil ProductType y
ys         = ProductType y
ProductType (x ++ y)
ys
concatPT (PTCons SumType x
x ProductType xs
xs) ProductType y
ys = SumType x -> ProductType (xs ++ y) -> ProductType (x : (xs ++ y))
forall (xs :: [Type]) (xs :: [[Type]]).
SumType xs -> ProductType xs -> ProductType (xs : xs)
PTCons SumType x
x (ProductType xs -> ProductType y -> ProductType (xs ++ y)
forall (x :: [[Type]]) (y :: [[Type]]).
ProductType x -> ProductType y -> ProductType (x ++ y)
concatPT ProductType xs
xs ProductType y
ys)

-- | Typelevel product of `Sum`s with values
data Product :: [[Type]] -> Type where
  Nil :: Product '[]
  Cons :: Sum x -> Product xs -> Product (x ': xs)

deriving instance (All2 Eq xs) => Eq (Product xs)

instance (All2 Show xs) => Show (Product xs) where
  show :: Product xs -> String
show Product xs
Nil         = String
"Nil"
  show (Cons Sum x
a Product xs
as) = String
"Cons " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sum x -> String
forall a. Show a => a -> String
show Sum x
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Product xs -> String
forall a. Show a => a -> String
show Product xs
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Concatenates `Product` values
concatP :: Product x -> Product y -> Product (x ++ y)
concatP :: Product x -> Product y -> Product (x ++ y)
concatP Product x
Nil         Product y
ys = Product y
Product (x ++ y)
ys
concatP (Cons Sum x
x Product xs
xs) Product y
ys = Sum x -> Product (xs ++ y) -> Product (x : (xs ++ y))
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons Sum x
x (Product xs -> Product y -> Product (xs ++ y)
forall (x :: [[Type]]) (y :: [[Type]]).
Product x -> Product y -> Product (x ++ y)
concatP Product xs
xs Product y
ys)

-- | Type witness for `Sum`
data SumType :: [Type] -> Type where
  STSucc :: (Ground x) => x -> SumType xs -> SumType (x ': xs)
  STZero :: SumType '[]

-- | Typelevel sum, contains one value from the typelevel list of types, or
--   undefined.
data Sum :: [Type] -> Type where
  Pick :: (Ground x) => x -> Sum (x ': xs)
  Skip :: (Ground x) => Sum xs -> Sum (x ': xs)

data Undef = Undef
  deriving (Undef -> Undef -> Bool
(Undef -> Undef -> Bool) -> (Undef -> Undef -> Bool) -> Eq Undef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Undef -> Undef -> Bool
$c/= :: Undef -> Undef -> Bool
== :: Undef -> Undef -> Bool
$c== :: Undef -> Undef -> Bool
Eq, Int -> Undef -> ShowS
[Undef] -> ShowS
Undef -> String
(Int -> Undef -> ShowS)
-> (Undef -> String) -> ([Undef] -> ShowS) -> Show Undef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Undef] -> ShowS
$cshowList :: [Undef] -> ShowS
show :: Undef -> String
$cshow :: Undef -> String
showsPrec :: Int -> Undef -> ShowS
$cshowsPrec :: Int -> Undef -> ShowS
Show, (forall x. Undef -> Rep Undef x)
-> (forall x. Rep Undef x -> Undef) -> Generic Undef
forall x. Rep Undef x -> Undef
forall x. Undef -> Rep Undef x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Undef x -> Undef
$cfrom :: forall x. Undef -> Rep Undef x
GHC.Generic, All SListI (Code Undef)
All SListI (Code Undef)
-> (Undef -> Rep Undef) -> (Rep Undef -> Undef) -> Generic Undef
Rep Undef -> Undef
Undef -> Rep Undef
forall a.
All SListI (Code a) -> (a -> Rep a) -> (Rep a -> a) -> Generic a
to :: Rep Undef -> Undef
$cto :: Rep Undef -> Undef
from :: Undef -> Rep Undef
$cfrom :: Undef -> Rep Undef
$cp1Generic :: All SListI (Code Undef)
SOP.Generic)

-- Undef is the only default Ground, because we need to mark when no value
-- is when 2 non-equal-lenght types are zipped
instance Ground Undef where
  mkGround :: Undef
mkGround = Undef
Undef

deriving instance (All Eq xs) => Eq (Sum xs)

type family MapTypeRep (xs :: [Type]) :: [Type] where
  MapTypeRep '[] = '[]
  MapTypeRep (x ': xs) = x ': MapTypeRep xs

type family Map2TypeRep (xss :: [[Type]]) :: [[Type]] where
  Map2TypeRep '[] = '[]
  Map2TypeRep (x ': xs) = MapTypeRep x ': Map2TypeRep xs

instance (All Show (MapTypeRep xs)) => Show (SumType xs) where
  show :: SumType xs -> String
show (STSucc x
x SumType xs
xs) = String
"STSucc" String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SumType xs -> String
forall a. Show a => a -> String
show SumType xs
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show SumType xs
STZero        = String
"STZero"

instance (All Show x) => Show (Sum x) where
  show :: Sum x -> String
show (Pick x
x) = String
"Pick " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
x
  show (Skip Sum xs
x) = String
"Skip " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sum xs -> String
forall a. Show a => a -> String
show Sum xs
x

-- only used in examples
data A
data B
data C
data D
data E
data F
data G
data H

----------------------------------------
-- Type functions on lists

-- | Concatenate a list of lists, typelevel equivalent of
--
-- > concat :: [[a]] -> [a]`
--
--    Example:
--
-- >>> :kind! Concat '[ '[A, B], '[C, D]]
-- Concat '[ '[A, B], '[C, D]] :: [Type]
-- = '[A, B, C, D]
--
type family Concat (xss :: [[x]]) :: [x] where
  Concat '[] = '[]
  Concat (xs ': xss) = xs ++ Concat xss

-- | Map `Concat` over a list (of lists, of lists), typelevel equivalent of
--
-- > map . concat :: [[[a]]] -> [[a]]
--
--   Example:
--
-- >>> :kind! MapConcat '[ '[ '[A, B], '[C, D]], '[[E, F], '[G, H]]]
-- MapConcat '[ '[ '[A, B], '[C, D]], '[[E, F], '[G, H]]] :: [[Type]]
-- = '[ '[A, B, C, D], '[E, F, G, H]]
--
type family MapConcat (xsss :: [[[x]]]) :: [[x]] where
  MapConcat '[] = '[]
  MapConcat (xss ': xsss) = Concat xss ': MapConcat xsss

-- | Zip two lists of lists with  ++` as operator, while keeping the length of
--   the longest outer list
--
--   Example:
--
-- >>> :kind! Merge '[ '[A, B, C], '[D, E]] '[ '[F, G]]
-- Merge '[ '[A, B, C], '[D, E]] '[ '[F, G]] :: [[Type]]
-- = '[ '[A, B, C, F, G], '[D, E]]
--
type family Merge (xs :: [[Type]]) (ys :: [[Type]]) :: [[Type]] where
  Merge '[] '[] = '[]
  Merge '[] (b ': bs) = (Undef ': b) ': Merge '[] bs
  Merge (a ': as) '[] = (a ++ '[Undef]) ': Merge as '[]
  Merge (a ': as) (b ': bs) = (a ++ b) ': Merge as bs

-- | Fold `Merge` over a list (of lists, of lists)
--
--   Example:
--
-- >>> :kind! FoldMerge '[ '[ '[A, B, C], '[D, E]], '[ '[F, G]], '[ '[H]]]
-- FoldMerge '[ '[ '[A, B, C], '[D, E]], '[ '[F, G]], '[ '[H]]] :: [[Type]]
-- = '[ '[A, B, C, F, G, H], '[D, E]]
--
type family FoldMerge (xss :: [[[Type]]]) :: [[Type]] where
  FoldMerge '[a] = a
  FoldMerge (a ': as) = Merge a (FoldMerge as)
  FoldMerge '[] = '[]

----------------------------------------
-- Functions on Products and Sums

-- | Merge a `ProductType` and a `Product`, putting the values of the `Product` in
--   the right argument of `Merge`
zipSumRight :: ProductType l -> Product r -> Product (Merge l r)
zipSumRight :: ProductType l -> Product r -> Product (Merge l r)
zipSumRight ProductType l
PTNil         Product r
Nil         = Product '[]
Product (Merge l r)
Nil
zipSumRight ProductType l
PTNil         (Cons Sum x
y Product xs
ys) = Sum (Undef : x)
-> Product (Merge '[] xs) -> Product ((Undef : x) : Merge '[] xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum x -> Sum (Undef : x)
forall (r :: [Type]). Sum r -> Sum (Undef : r)
takeRightUndef Sum x
y) (ProductType '[] -> Product xs -> Product (Merge '[] xs)
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> Product r -> Product (Merge l r)
zipSumRight ProductType '[]
PTNil Product xs
ys)
zipSumRight (PTCons SumType x
x ProductType xs
xs) Product r
Nil         = Sum (x ++ '[Undef])
-> Product (Merge xs '[])
-> Product ((x ++ '[Undef]) : Merge xs '[])
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (SumType x -> Sum (x ++ '[Undef])
forall (x :: [Type]). SumType x -> Sum (x ++ '[Undef])
makeUndefRight SumType x
x) (ProductType xs -> Product '[] -> Product (Merge xs '[])
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> Product r -> Product (Merge l r)
zipSumRight ProductType xs
xs Product '[]
Nil)
zipSumRight (PTCons SumType x
x ProductType xs
xs) (Cons Sum x
y Product xs
ys) = Sum (x ++ x)
-> Product (Merge xs xs) -> Product ((x ++ x) : Merge xs xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (SumType x -> Sum x -> Sum (x ++ x)
forall (l :: [Type]) (r :: [Type]).
SumType l -> Sum r -> Sum (l ++ r)
takeRight SumType x
x Sum x
y) (ProductType xs -> Product xs -> Product (Merge xs xs)
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> Product r -> Product (Merge l r)
zipSumRight ProductType xs
xs Product xs
ys)

makeUndefRight :: SumType x -> Sum (x ++ '[Undef])
makeUndefRight :: SumType x -> Sum (x ++ '[Undef])
makeUndefRight (STSucc x
_ SumType xs
xs) = Sum (xs ++ '[Undef]) -> Sum (x : (xs ++ '[Undef]))
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (SumType xs -> Sum (xs ++ '[Undef])
forall (x :: [Type]). SumType x -> Sum (x ++ '[Undef])
makeUndefRight SumType xs
xs)
makeUndefRight SumType x
STZero        = Undef -> Sum '[Undef]
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick Undef
Undef

makeUndefLeft :: SumType x -> Sum (Undef ': x)
makeUndefLeft :: SumType x -> Sum (Undef : x)
makeUndefLeft SumType x
_ = Undef -> Sum (Undef : x)
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick Undef
Undef

takeRightUndef :: Sum r -> Sum (Undef ': r)
takeRightUndef :: Sum r -> Sum (Undef : r)
takeRightUndef = Sum r -> Sum (Undef : r)
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip

takeLeftUndef :: Sum x -> Sum (x ++ '[Undef])
takeLeftUndef :: Sum x -> Sum (x ++ '[Undef])
takeLeftUndef (Pick x
x)  = x -> Sum (x : (xs ++ '[Undef]))
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick x
x
takeLeftUndef (Skip Sum xs
xs) = Sum (xs ++ '[Undef]) -> Sum (x : (xs ++ '[Undef]))
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (Sum xs -> Sum (xs ++ '[Undef])
forall (x :: [Type]). Sum x -> Sum (x ++ '[Undef])
takeLeftUndef Sum xs
xs)

-- | Merge a `ProductType` and a `Product`
merge :: Either (Product l, ProductType r) (ProductType l, Product r) -> Product (Merge l r)
merge :: Either (Product l, ProductType r) (ProductType l, Product r)
-> Product (Merge l r)
merge (Left (Product l
l, ProductType r
r))  = Product l -> ProductType r -> Product (Merge l r)
forall (l :: [[Type]]) (r :: [[Type]]).
Product l -> ProductType r -> Product (Merge l r)
zipSumLeft Product l
l ProductType r
r
merge (Right (ProductType l
l, Product r
r)) = ProductType l -> Product r -> Product (Merge l r)
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> Product r -> Product (Merge l r)
zipSumRight ProductType l
l Product r
r

-- | Merge a `ProductType` and a `Product`, putting the values of the `Product`
--   in the left argument of `Merge`
zipSumLeft :: Product l -> ProductType r -> Product (Merge l r)
zipSumLeft :: Product l -> ProductType r -> Product (Merge l r)
zipSumLeft Product l
Nil         ProductType r
PTNil         = Product '[]
Product (Merge l r)
Nil
zipSumLeft Product l
Nil         (PTCons SumType x
y ProductType xs
ys) = Sum (Undef : x)
-> Product (Merge '[] xs) -> Product ((Undef : x) : Merge '[] xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (SumType x -> Sum (Undef : x)
forall (x :: [Type]). SumType x -> Sum (Undef : x)
makeUndefLeft SumType x
y) (Product '[] -> ProductType xs -> Product (Merge '[] xs)
forall (l :: [[Type]]) (r :: [[Type]]).
Product l -> ProductType r -> Product (Merge l r)
zipSumLeft Product '[]
Nil ProductType xs
ys)
zipSumLeft (Cons Sum x
x Product xs
xs) ProductType r
PTNil         = Sum (x ++ '[Undef])
-> Product (Merge xs '[])
-> Product ((x ++ '[Undef]) : Merge xs '[])
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum x -> Sum (x ++ '[Undef])
forall (x :: [Type]). Sum x -> Sum (x ++ '[Undef])
takeLeftUndef Sum x
x) (Product xs -> ProductType '[] -> Product (Merge xs '[])
forall (l :: [[Type]]) (r :: [[Type]]).
Product l -> ProductType r -> Product (Merge l r)
zipSumLeft Product xs
xs ProductType '[]
PTNil)
zipSumLeft (Cons Sum x
x Product xs
xs) (PTCons SumType x
y ProductType xs
ys) = Sum (x ++ x)
-> Product (Merge xs xs) -> Product ((x ++ x) : Merge xs xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum x -> SumType x -> Sum (x ++ x)
forall (l :: [Type]) (r :: [Type]).
Sum l -> SumType r -> Sum (l ++ r)
takeLeft Sum x
x SumType x
y) (Product xs -> ProductType xs -> Product (Merge xs xs)
forall (l :: [[Type]]) (r :: [[Type]]).
Product l -> ProductType r -> Product (Merge l r)
zipSumLeft Product xs
xs ProductType xs
ys)

-- | Merge two `ProductType`s
mergeT :: ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT :: ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType l
PTNil ProductType r
PTNil                 = ProductType '[]
ProductType (Merge l r)
PTNil
mergeT ProductType l
PTNil (PTCons SumType x
y ProductType xs
ys)         = SumType (Undef : x)
-> ProductType (Merge '[] xs)
-> ProductType ((Undef : x) : Merge '[] xs)
forall (xs :: [Type]) (xs :: [[Type]]).
SumType xs -> ProductType xs -> ProductType (xs : xs)
PTCons (SumType x -> SumType (Undef : x)
forall (x :: [Type]). SumType x -> SumType (Undef : x)
makeUndefLeftT SumType x
y) (ProductType '[] -> ProductType xs -> ProductType (Merge '[] xs)
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType '[]
PTNil ProductType xs
ys)
mergeT (PTCons SumType x
x ProductType xs
xs) ProductType r
PTNil         = SumType (x ++ '[Undef])
-> ProductType (Merge xs '[])
-> ProductType ((x ++ '[Undef]) : Merge xs '[])
forall (xs :: [Type]) (xs :: [[Type]]).
SumType xs -> ProductType xs -> ProductType (xs : xs)
PTCons (SumType x -> SumType (x ++ '[Undef])
forall (x :: [Type]). SumType x -> SumType (x ++ '[Undef])
makeUndefRightT SumType x
x) (ProductType xs -> ProductType '[] -> ProductType (Merge xs '[])
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType xs
xs ProductType '[]
PTNil)
mergeT (PTCons SumType x
x ProductType xs
xs) (PTCons SumType x
y ProductType xs
ys) = SumType (x ++ x)
-> ProductType (Merge xs xs)
-> ProductType ((x ++ x) : Merge xs xs)
forall (xs :: [Type]) (xs :: [[Type]]).
SumType xs -> ProductType xs -> ProductType (xs : xs)
PTCons (SumType x -> SumType x -> SumType (x ++ x)
forall (l :: [Type]) (r :: [Type]).
SumType l -> SumType r -> SumType (l ++ r)
takeST SumType x
x SumType x
y) (ProductType xs -> ProductType xs -> ProductType (Merge xs xs)
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType xs
xs ProductType xs
ys)

makeUndefRightT :: SumType x -> SumType (x ++ '[Undef])
makeUndefRightT :: SumType x -> SumType (x ++ '[Undef])
makeUndefRightT (STSucc x
x SumType xs
xs) = x -> SumType (xs ++ '[Undef]) -> SumType (x : (xs ++ '[Undef]))
forall x (xs :: [Type]).
Ground x =>
x -> SumType xs -> SumType (x : xs)
STSucc x
x (SumType xs -> SumType (xs ++ '[Undef])
forall (x :: [Type]). SumType x -> SumType (x ++ '[Undef])
makeUndefRightT SumType xs
xs)
makeUndefRightT SumType x
STZero        = Undef -> SumType '[] -> SumType '[Undef]
forall x (xs :: [Type]).
Ground x =>
x -> SumType xs -> SumType (x : xs)
STSucc Undef
Undef SumType '[]
STZero

makeUndefLeftT :: SumType x -> SumType (Undef ': x)
makeUndefLeftT :: SumType x -> SumType (Undef : x)
makeUndefLeftT = Undef -> SumType x -> SumType (Undef : x)
forall x (xs :: [Type]).
Ground x =>
x -> SumType xs -> SumType (x : xs)
STSucc Undef
Undef

takeST :: SumType l -> SumType r -> SumType (l ++ r)
takeST :: SumType l -> SumType r -> SumType (l ++ r)
takeST (STSucc x
l SumType xs
ls) SumType r
rs = x -> SumType (xs ++ r) -> SumType (x : (xs ++ r))
forall x (xs :: [Type]).
Ground x =>
x -> SumType xs -> SumType (x : xs)
STSucc x
l (SumType xs -> SumType r -> SumType (xs ++ r)
forall (l :: [Type]) (r :: [Type]).
SumType l -> SumType r -> SumType (l ++ r)
takeST SumType xs
ls SumType r
rs)
takeST SumType l
STZero        SumType r
rs = SumType r
SumType (l ++ r)
rs

takeLeft :: Sum l -> SumType r -> Sum (l ++ r)
takeLeft :: Sum l -> SumType r -> Sum (l ++ r)
takeLeft (Pick x
l)  SumType r
_  = x -> Sum (x : (xs ++ r))
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick x
l
takeLeft (Skip Sum xs
ls) SumType r
rs = Sum (xs ++ r) -> Sum (x : (xs ++ r))
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (Sum xs -> SumType r -> Sum (xs ++ r)
forall (l :: [Type]) (r :: [Type]).
Sum l -> SumType r -> Sum (l ++ r)
takeLeft Sum xs
ls SumType r
rs)

takeRight :: SumType l -> Sum r -> Sum (l ++ r)
takeRight :: SumType l -> Sum r -> Sum (l ++ r)
takeRight (STSucc x
_ SumType xs
ls) Sum r
rs = Sum (xs ++ r) -> Sum (x : (xs ++ r))
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (SumType xs -> Sum r -> Sum (xs ++ r)
forall (l :: [Type]) (r :: [Type]).
SumType l -> Sum r -> Sum (l ++ r)
takeRight SumType xs
ls Sum r
rs)
takeRight SumType l
STZero        Sum r
rs = Sum r
Sum (l ++ r)
rs

-- | UnMerge a `Product`, using two `ProductType`s as witnesses for the left and
--   right argument of `Merge`. Produces a value of type Product right
splitRight :: Product (Merge l r) -> ProductType l -> ProductType r -> Product r
splitRight :: Product (Merge l r) -> ProductType l -> ProductType r -> Product r
splitRight (Cons Sum x
x Product xs
xs) ProductType l
PTNil (PTCons SumType x
_ ProductType xs
rs) = Sum x -> Product xs -> Product (x : xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum (Undef : x) -> Sum x
forall (x :: [Type]). Sum (Undef : x) -> Sum x
removeUndefLeft Sum x
Sum (Undef : x)
x) (Product (Merge '[] xs)
-> ProductType '[] -> ProductType xs -> Product xs
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product r
splitRight Product xs
Product (Merge '[] xs)
xs ProductType '[]
PTNil ProductType xs
rs)
splitRight Product (Merge l r)
_  ProductType l
_ ProductType r
PTNil = Product r
Product '[]
Nil
splitRight (Cons Sum x
x Product xs
xs) (PTCons SumType x
l ProductType xs
ls) (PTCons SumType x
r ProductType xs
rs) = Sum x -> Product xs -> Product (x : xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum (x ++ x) -> SumType x -> SumType x -> Sum x
forall (l :: [Type]) (r :: [Type]).
Sum (l ++ r) -> SumType l -> SumType r -> Sum r
splitSumRight Sum x
Sum (x ++ x)
x SumType x
l SumType x
r) (Product (Merge xs xs)
-> ProductType xs -> ProductType xs -> Product xs
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product r
splitRight Product xs
Product (Merge xs xs)
xs ProductType xs
ls ProductType xs
rs)

removeUndefLeft :: Sum (Undef ': x) -> Sum x
removeUndefLeft :: Sum (Undef : x) -> Sum x
removeUndefLeft (Pick x
Undef) = String -> Sum x
forall a. HasCallStack => String -> a
error String
"Undefined value where I expected an actual value"
removeUndefLeft (Skip Sum xs
xs)    = Sum x
Sum xs
xs

removeUndefRight :: SumType x -> Sum (x ++ '[Undef]) -> Sum x
removeUndefRight :: SumType x -> Sum (x ++ '[Undef]) -> Sum x
removeUndefRight SumType x
STZero        Sum (x ++ '[Undef])
_            = String -> Sum x
forall a. HasCallStack => String -> a
error String
"Undefined value where I expected an actual value"
removeUndefRight (STSucc x
_ SumType xs
_)  (Pick x
y)     = x -> Sum (x : xs)
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick x
y
removeUndefRight (STSucc x
_ SumType xs
xs) (Skip Sum xs
ys) = Sum xs -> Sum (x : xs)
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (SumType xs -> Sum (xs ++ '[Undef]) -> Sum xs
forall (x :: [Type]). SumType x -> Sum (x ++ '[Undef]) -> Sum x
removeUndefRight SumType xs
xs Sum xs
Sum (xs ++ '[Undef])
ys)

-- | UnMerge a `Product`, using two `ProductType`s as witnesses for the left and
--   right argument of `Merge`. Produces a value of type Product left
splitLeft :: Product (Merge l r) -> ProductType l -> ProductType r -> Product l
splitLeft :: Product (Merge l r) -> ProductType l -> ProductType r -> Product l
splitLeft Product (Merge l r)
_ ProductType l
PTNil ProductType r
_ = Product l
Product '[]
Nil
splitLeft (Cons Sum x
x Product xs
xs) (PTCons SumType x
l ProductType xs
ls) ProductType r
PTNil = Sum x -> Product xs -> Product (x : xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (SumType x -> Sum (x ++ '[Undef]) -> Sum x
forall (x :: [Type]). SumType x -> Sum (x ++ '[Undef]) -> Sum x
removeUndefRight SumType x
l Sum x
Sum (x ++ '[Undef])
x) (Product (Merge xs '[])
-> ProductType xs -> ProductType '[] -> Product xs
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product l
splitLeft Product xs
Product (Merge xs '[])
xs ProductType xs
ls ProductType '[]
PTNil)
splitLeft (Cons Sum x
x Product xs
xs) (PTCons SumType x
l ProductType xs
ls) (PTCons SumType x
r ProductType xs
rs) = Sum x -> Product xs -> Product (x : xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons (Sum (x ++ x) -> SumType x -> SumType x -> Sum x
forall (l :: [Type]) (r :: [Type]).
Sum (l ++ r) -> SumType l -> SumType r -> Sum l
splitSumLeft Sum x
Sum (x ++ x)
x SumType x
l SumType x
r) (Product (Merge xs xs)
-> ProductType xs -> ProductType xs -> Product xs
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product l
splitLeft Product xs
Product (Merge xs xs)
xs ProductType xs
ls ProductType xs
rs)

splitSumRight :: Sum (l ++ r) -> SumType l -> SumType r -> Sum r
splitSumRight :: Sum (l ++ r) -> SumType l -> SumType r -> Sum r
splitSumRight Sum (l ++ r)
xs        SumType l
STZero        SumType r
_  = Sum r
Sum (l ++ r)
xs
splitSumRight (Pick x
_)  (STSucc x
_ SumType xs
_)  SumType r
_  = String -> Sum r
forall a. HasCallStack => String -> a
error String
"No value found in right side of Sum"
splitSumRight (Skip Sum xs
xs) (STSucc x
_ SumType xs
ls) SumType r
rs = Sum (xs ++ r) -> SumType xs -> SumType r -> Sum r
forall (l :: [Type]) (r :: [Type]).
Sum (l ++ r) -> SumType l -> SumType r -> Sum r
splitSumRight Sum xs
Sum (xs ++ r)
xs SumType xs
ls SumType r
rs

splitSumLeft :: Sum (l ++ r) -> SumType l -> SumType r -> Sum l
splitSumLeft :: Sum (l ++ r) -> SumType l -> SumType r -> Sum l
splitSumLeft (Pick x
x)  (STSucc x
_ SumType xs
_) SumType r
_   = x -> Sum (x : xs)
forall x (xs :: [Type]). Ground x => x -> Sum (x : xs)
Pick x
x
splitSumLeft Sum (l ++ r)
_        SumType l
STZero        SumType r
_   = String -> Sum l
forall a. HasCallStack => String -> a
error String
"No value value found in left side of Sum"
splitSumLeft (Skip Sum xs
xs) (STSucc x
_ SumType xs
ls) SumType r
rs = Sum xs -> Sum (x : xs)
forall xs (x :: [Type]). Ground xs => Sum x -> Sum (xs : x)
Skip (Sum xs -> Sum (x : xs)) -> Sum xs -> Sum (x : xs)
forall a b. (a -> b) -> a -> b
$ Sum (xs ++ r) -> SumType xs -> SumType r -> Sum xs
forall (l :: [Type]) (r :: [Type]).
Sum (l ++ r) -> SumType l -> SumType r -> Sum l
splitSumLeft Sum xs
Sum (xs ++ r)
xs SumType xs
ls SumType r
rs

-- | UnConcat a `Product`, using a `ProductType` as the witness for the first
--   argument of `++`. Produces a tuple with the first and second argument of `++`
unConcatP :: Product (x ++ y) -> ProductType x -> (Product x, Product y)
unConcatP :: Product (x ++ y) -> ProductType x -> (Product x, Product y)
unConcatP Product (x ++ y)
xs ProductType x
PTNil                  = (Product x
Product '[]
Nil, Product y
Product (x ++ y)
xs)
unConcatP (Cons Sum x
x Product xs
xs) (PTCons SumType x
_ ProductType xs
ts) = (Sum x -> Product xs -> Product (x : xs)
forall (xs :: [Type]) (xs :: [[Type]]).
Sum xs -> Product xs -> Product (xs : xs)
Cons Sum x
x Product xs
xs', Product y
ys')
  where
    (Product xs
xs', Product y
ys') = Product (xs ++ y) -> ProductType xs -> (Product xs, Product y)
forall (x :: [[Type]]) (y :: [[Type]]).
Product (x ++ y) -> ProductType x -> (Product x, Product y)
unConcatP Product xs
Product (xs ++ y)
xs ProductType xs
ts