{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE DefaultSignatures       #-}
{-# LANGUAGE ExplicitNamespaces      #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE NoStarIsType            #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE TypeFamilyDependencies  #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

-- | Exports the `POSable` class, which has a generic implementation `GPOSable`.
--   Also re-exports Generic.SOP, which is needed to derive POSable.
module Generics.POSable.POSable (POSable(..), Generic, Finite) where

import           Data.Finite                     (combineProduct, combineSum,
                                                  separateProduct, separateSum)
import           Generics.POSable.Representation
import           Generics.SOP                    hiding (Nil, shift)
import           Generics.SOP.NP                 hiding (Nil)

import           Data.Kind                       (Type)

import qualified Generics.SOP                    as SOP

import           GHC.Base                        (Nat)
import           GHC.TypeLits                    (KnownNat, natVal, type (*),
                                                  type (+))

import           Data.Finite.Internal

-- | POSable, the base of this library. Provide a compact memory representation
--   for a type and a function to get back to the original type.
--   This memory representation consist of `choices`, that represent all
--   constructor choices in the type in a single Finite integer, and `fields`
--   which represents all values in the type as a Product of Sums, which can
--   be mapped to a struct-of-arrays representation for use in array-based
--   languages like Accelerate.
class (KnownNat (Choices x)) => POSable x where
  type Choices x :: Nat
  type Choices x = GChoices (SOP I (Code x))

  choices :: x -> Finite (Choices x)
  default choices ::
    ( Generic x
    , GPOSable (SOP I (Code x))
    , GChoices (SOP I (Code x)) ~ Choices x
    ) => x -> Finite (Choices x)
  choices x
x = SOP I (Code x) -> Finite (GChoices (SOP I (Code x)))
forall x. GPOSable x => x -> Finite (GChoices x)
gchoices (SOP I (Code x) -> Finite (GChoices (SOP I (Code x))))
-> SOP I (Code x) -> Finite (GChoices (SOP I (Code x)))
forall a b. (a -> b) -> a -> b
$ x -> SOP I (Code x)
forall a. Generic a => a -> Rep a
from x
x

  -- | The `tags` function returns the range of each constructor.
  --   A few examples:
  --   >>> tags @Bool
  --   [1,1]
  --   >>> tags @(Either Float Float)
  --   [1,1]
  --   >>> tags @(Bool, Bool)
  --   [4]
  --   >>> tags @(Either Bool Bool)
  --   [2,2]
  tags :: [Integer]
  default tags ::
    ( GPOSable (SOP I (Code x))
    ) => [Integer]
  tags = GPOSable (SOP I (Code x)) => [Integer]
forall x. GPOSable x => [Integer]
gtags @(SOP I (Code x))

  fromPOSable :: Finite (Choices x) -> Product (Fields x) -> x

  default fromPOSable ::
    ( Generic x
    , GPOSable (SOP I (Code x))
    , Fields x ~ GFields (SOP I (Code x))
    , Choices x ~ GChoices (SOP I (Code x))
    ) => Finite (Choices x) -> Product (Fields x) -> x
  fromPOSable Finite (Choices x)
cs Product (Fields x)
fs = SOP I (Code x) -> x
forall a. Generic a => Rep a -> a
to (SOP I (Code x) -> x) -> SOP I (Code x) -> x
forall a b. (a -> b) -> a -> b
$ Finite (GChoices (SOP I (Code x)))
-> Product (GFields (SOP I (Code x))) -> SOP I (Code x)
forall x.
GPOSable x =>
Finite (GChoices x) -> Product (GFields x) -> x
gfromPOSable Finite (GChoices (SOP I (Code x)))
Finite (Choices x)
cs Product (GFields (SOP I (Code x)))
Product (Fields x)
fs

  type Fields x :: [[Type]]
  type Fields x = GFields (SOP I (Code x))

  fields :: x -> Product (Fields x)

  default fields ::
    ( Generic x
    , Fields x ~ GFields (SOP I (Code x))
    , GPOSable (SOP I (Code x))
    ) => x -> Product (Fields x)
  fields x
x = SOP I (Code x) -> Product (GFields (SOP I (Code x)))
forall x. GPOSable x => x -> Product (GFields x)
gfields (SOP I (Code x) -> Product (GFields (SOP I (Code x))))
-> SOP I (Code x) -> Product (GFields (SOP I (Code x)))
forall a b. (a -> b) -> a -> b
$ x -> SOP I (Code x)
forall a. Generic a => a -> Rep a
from x
x

  emptyFields :: ProductType (Fields x)

  default emptyFields ::
    ( GPOSable (SOP I (Code x))
    , Fields x ~ GFields (SOP I (Code x))
    ) => ProductType (Fields x)
  emptyFields  = GPOSable (SOP I (Code x)) => ProductType (GFields (SOP I (Code x)))
forall x. GPOSable x => ProductType (GFields x)
gemptyFields @(SOP I (Code x))


-----------------------------------------------------------------------
-- | Generic implementation of POSable,
class (KnownNat (GChoices x)) => GPOSable x where
  type GChoices x :: Nat
  gchoices :: x -> Finite (GChoices x)

  gtags :: [Integer]

  type GFields x :: [[Type]]
  gfields :: x -> Product (GFields x)

  gfromPOSable :: Finite (GChoices x) -> Product (GFields x) -> x

  gemptyFields :: ProductType (GFields x)

-----------------------------------------------------------------------
-- Generic instance for POSable
instance
  ( All2 POSable xss
  , KnownNat (Sums (MapProducts (Map2Choices xss)))
  , All2 KnownNat (Map2Choices xss)
  , All KnownNat (MapProducts (Map2Choices xss))
  , KnownNat (Length xss)
  ) => GPOSable (SOP I xss) where

  type GChoices (SOP I xss) = Sums (MapProducts (Map2Choices xss))
  gchoices :: SOP I xss -> Finite (GChoices (SOP I xss))
gchoices SOP I xss
x = NS Finite (MapProducts (Map2Choices xss))
-> Finite (Sums (MapProducts (Map2Choices xss)))
forall (xs :: [Nat]).
All KnownNat xs =>
NS Finite xs -> Finite (Sums xs)
sums (NS Finite (MapProducts (Map2Choices xss))
 -> Finite (Sums (MapProducts (Map2Choices xss))))
-> NS Finite (MapProducts (Map2Choices xss))
-> Finite (Sums (MapProducts (Map2Choices xss)))
forall a b. (a -> b) -> a -> b
$ NS (NP Finite) (Map2Choices xss)
-> NS Finite (MapProducts (Map2Choices xss))
forall (xss :: [[Nat]]).
All2 KnownNat xss =>
NS (NP Finite) xss -> NS Finite (MapProducts xss)
mapProducts (NS (NP Finite) (Map2Choices xss)
 -> NS Finite (MapProducts (Map2Choices xss)))
-> NS (NP Finite) (Map2Choices xss)
-> NS Finite (MapProducts (Map2Choices xss))
forall a b. (a -> b) -> a -> b
$ NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
forall (xss :: [[Type]]).
All2 POSable xss =>
NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
map2choices (NS (NP I) xss -> NS (NP Finite) (Map2Choices xss))
-> NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
forall a b. (a -> b) -> a -> b
$ SOP I xss -> NS (NP I) xss
forall k (f :: k -> Type) (xss :: [[k]]).
SOP f xss -> NS (NP f) xss
unSOP SOP I xss
x

  gtags :: [Integer]
gtags = NP ProductsMapChoices xss -> [Integer]
forall (xss :: [[Type]]).
All KnownNat (MapProducts (Map2Choices xss)) =>
NP ProductsMapChoices xss -> [Integer]
getTags ((All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NP ProductsMapChoices xss
forall (xss :: [[Type]]).
(All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NP ProductsMapChoices xss
pureChoices2 @xss)

  type GFields (SOP I xss) = FoldMerge (MapConcat (Map2Fields xss))
  gfields :: SOP I xss -> Product (GFields (SOP I xss))
gfields (SOP NS (NP I) xss
x)         = NP ProductType (MapConcat (Map2Fields xss))
-> NS Product (MapConcat (Map2Fields xss))
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
forall (xss :: [[[Type]]]).
NP ProductType xss -> NS Product xss -> Product (FoldMerge xss)
foldMerge
                              (NP (NP ProductType) (Map2Fields xss)
-> NP ProductType (MapConcat (Map2Fields xss))
forall (xss :: [[[[Type]]]]).
NP (NP ProductType) xss -> NP ProductType (MapConcat xss)
mapConcatT (All2 POSable xss => NP (NP ProductType) (Map2Fields xss)
forall (xss :: [[Type]]).
All2 POSable xss =>
NP (NP ProductType) (Map2Fields xss)
pureMap2Fields @xss))
                              (NS (NP Product) (Map2Fields xss)
-> NS Product (MapConcat (Map2Fields xss))
forall (xss :: [[[[Type]]]]).
NS (NP Product) xss -> NS Product (MapConcat xss)
mapConcat (NS (NP I) xss -> NS (NP Product) (Map2Fields xss)
forall (xss :: [[Type]]).
All2 POSable xss =>
NS (NP I) xss -> NS (NP Product) (Map2Fields xss)
map2Fields NS (NP I) xss
x))

  gemptyFields :: ProductType (GFields (SOP I xss))
gemptyFields = NP ProductType (MapConcat (Map2Fields xss))
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
forall (xss :: [[[Type]]]).
NP ProductType xss -> ProductType (FoldMerge xss)
foldMergeT (NP ProductType (MapConcat (Map2Fields xss))
 -> ProductType (FoldMerge (MapConcat (Map2Fields xss))))
-> NP ProductType (MapConcat (Map2Fields xss))
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
forall a b. (a -> b) -> a -> b
$ NP (NP ProductType) (Map2Fields xss)
-> NP ProductType (MapConcat (Map2Fields xss))
forall (xss :: [[[[Type]]]]).
NP (NP ProductType) xss -> NP ProductType (MapConcat xss)
mapConcatT (All2 POSable xss => NP (NP ProductType) (Map2Fields xss)
forall (xss :: [[Type]]).
All2 POSable xss =>
NP (NP ProductType) (Map2Fields xss)
pureMap2Fields @xss)

  gfromPOSable :: Finite (GChoices (SOP I xss))
-> Product (GFields (SOP I xss)) -> SOP I xss
gfromPOSable Finite (GChoices (SOP I xss))
cs Product (GFields (SOP I xss))
fs = NS (NP I) xss -> SOP I xss
forall k (f :: k -> Type) (xss :: [[k]]).
NS (NP f) xss -> SOP f xss
SOP (NS ProductsMapChoices xss
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
-> NP ProductConcatFieldsT xss
-> NS (NP I) xss
forall (xss :: [[Type]]).
(All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NS ProductsMapChoices xss
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
-> NP ProductConcatFieldsT xss
-> NS (NP I) xss
mapFromPOSable NS ProductsMapChoices xss
cs' Product (FoldMerge (MapConcat (Map2Fields xss)))
Product (GFields (SOP I xss))
fs (All2 POSable xss => NP ProductConcatFieldsT xss
forall (xss :: [[Type]]).
All2 POSable xss =>
NP ProductConcatFieldsT xss
pureConcatFields @xss))
    where
      cs' :: NS ProductsMapChoices xss
cs' = Finite (Sums (MapProducts (Map2Choices xss)))
-> NP ProductsMapChoices xss -> NS ProductsMapChoices xss
forall (xs :: [[Type]]).
All KnownNat (MapProducts (Map2Choices xs)) =>
Finite (Sums (MapProducts (Map2Choices xs)))
-> NP ProductsMapChoices xs -> NS ProductsMapChoices xs
unSums Finite (Sums (MapProducts (Map2Choices xss)))
Finite (GChoices (SOP I xss))
cs ((All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NP ProductsMapChoices xss
forall (xss :: [[Type]]).
(All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NP ProductsMapChoices xss
pureChoices2 @xss)


getTags :: All KnownNat (MapProducts (Map2Choices xss)) => NP ProductsMapChoices xss -> [Integer]
getTags :: NP ProductsMapChoices xss -> [Integer]
getTags NP ProductsMapChoices xss
SOP.Nil                      = []
getTags (ProductsMapChoices Finite (Products (MapChoices x))
x :* NP ProductsMapChoices xs
xs) = Finite (Products (MapChoices x)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Finite (Products (MapChoices x))
x Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: NP ProductsMapChoices xs -> [Integer]
forall (xss :: [[Type]]).
All KnownNat (MapProducts (Map2Choices xss)) =>
NP ProductsMapChoices xss -> [Integer]
getTags NP ProductsMapChoices xs
xs

--------------------------------------------------------------------------------
-- Supporting types and classes
--------------------------------------------------------------------------------

type family Length (xs :: [x]) :: Nat where
  Length '[] = 0
  Length (x ': xs) = Length xs + 1

type family MapLength (xss :: [[x]]) :: [Nat] where
  MapLength '[] = '[]
  MapLength (x ': xs) = Length x ': MapLength xs

type family MapChoices (xs :: [Type]) :: [Nat] where
  MapChoices '[] = '[]
  MapChoices (x ': xs) = Choices x ': MapChoices xs


type family Map2Choices (xss :: [[Type]]) :: [[Nat]] where
  Map2Choices '[] = '[]
  Map2Choices (xs ': xss) = MapChoices xs ': Map2Choices xss


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


type family Map2Fields (xss :: [[Type]]) :: [[[[Type]]]] where
  Map2Fields '[] = '[]
  Map2Fields (xs ': xss) = MapFields xs ': Map2Fields xss


type family Products (xs :: [Nat]) :: Nat where
  Products '[] = 1
  Products (x ': xs) = x * Products xs

type family MapProducts (xss :: [[Nat]]) :: [Nat] where
  MapProducts '[] = '[]
  MapProducts (xs ': xss) = Products xs ': MapProducts xss

type family Sums (xs :: [Nat]) :: Nat where
  Sums '[] = 0
  Sums (x ': xs) = x + Sums xs

--------------------------------------------------------------------------------
-- Functions that deal with Choices
--------------------------------------------------------------------------------

mapChoices :: forall xs . (All POSable xs) => NP I xs -> NP Finite (MapChoices xs)
mapChoices :: NP I xs -> NP Finite (MapChoices xs)
mapChoices NP I xs
SOP.Nil   = NP Finite (MapChoices xs)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
mapChoices (I x
x :* NP I xs
xs) = x -> Finite (Choices x)
forall x. POSable x => x -> Finite (Choices x)
choices (I x -> x
forall a. I a -> a
unI I x
x) Finite (Choices x)
-> NP Finite (MapChoices xs)
-> NP Finite (Choices x : MapChoices xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs -> NP Finite (MapChoices xs)
forall (xs :: [Type]).
All POSable xs =>
NP I xs -> NP Finite (MapChoices xs)
mapChoices NP I xs
xs

map2choices :: (All2 POSable xss) => NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
map2choices :: NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
map2choices (Z NP I x
x)  = NP Finite (MapChoices x)
-> NS (NP Finite) (MapChoices x : Map2Choices xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP I x -> NP Finite (MapChoices x)
forall (xs :: [Type]).
All POSable xs =>
NP I xs -> NP Finite (MapChoices xs)
mapChoices NP I x
x)
map2choices (S NS (NP I) xs
xs) = NS (NP Finite) (Map2Choices xs)
-> NS (NP Finite) (MapChoices x : Map2Choices xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS (NP I) xs -> NS (NP Finite) (Map2Choices xs)
forall (xss :: [[Type]]).
All2 POSable xss =>
NS (NP I) xss -> NS (NP Finite) (Map2Choices xss)
map2choices NS (NP I) xs
xs)

sums :: All KnownNat xs => NS Finite xs -> Finite (Sums xs)
sums :: NS Finite xs -> Finite (Sums xs)
sums (Z Finite x
y)  = Either (Finite x) (Finite (Sums xs)) -> Finite (x + Sums xs)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Either (Finite n) (Finite m) -> Finite (n + m)
combineSum (Finite x -> Either (Finite x) (Finite (Sums xs))
forall a b. a -> Either a b
Left Finite x
y)
sums (S NS Finite xs
ys) = Either (Finite x) (Finite (Sums xs)) -> Finite (x + Sums xs)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Either (Finite n) (Finite m) -> Finite (n + m)
combineSum (Finite (Sums xs) -> Either (Finite x) (Finite (Sums xs))
forall a b. b -> Either a b
Right (NS Finite xs -> Finite (Sums xs)
forall (xs :: [Nat]).
All KnownNat xs =>
NS Finite xs -> Finite (Sums xs)
sums NS Finite xs
ys))

mapProducts :: (All2 KnownNat xss) => NS (NP Finite) xss -> NS Finite (MapProducts xss)
mapProducts :: NS (NP Finite) xss -> NS Finite (MapProducts xss)
mapProducts (Z NP Finite x
x)  = Finite (Products x) -> NS Finite (Products x : MapProducts xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP Finite x -> Finite (Products x)
forall (xs :: [Nat]).
All KnownNat xs =>
NP Finite xs -> Finite (Products xs)
combineProducts NP Finite x
x)
mapProducts (S NS (NP Finite) xs
xs) = NS Finite (MapProducts xs)
-> NS Finite (Products x : MapProducts xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS (NP Finite) xs -> NS Finite (MapProducts xs)
forall (xss :: [[Nat]]).
All2 KnownNat xss =>
NS (NP Finite) xss -> NS Finite (MapProducts xss)
mapProducts NS (NP Finite) xs
xs)

combineProducts :: (All KnownNat xs) => NP Finite xs -> Finite (Products xs)
combineProducts :: NP Finite xs -> Finite (Products xs)
combineProducts NP Finite xs
SOP.Nil   = Finite (Products xs)
0
combineProducts (Finite x
y :* NP Finite xs
ys) = (Finite x, Finite (Products xs)) -> Finite (x * Products xs)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct (Finite x
y, NP Finite xs -> Finite (Products xs)
forall (xs :: [Nat]).
All KnownNat xs =>
NP Finite xs -> Finite (Products xs)
combineProducts NP Finite xs
ys)

--------------------------------------------------------------------------------
-- Functions that deal with Fields
--------------------------------------------------------------------------------

mapFields :: forall xs . (All POSable xs) => NP I xs -> NP Product (MapFields xs)
mapFields :: NP I xs -> NP Product (MapFields xs)
mapFields NP I xs
SOP.Nil   = NP Product (MapFields xs)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
mapFields (I x
x :* NP I xs
xs) = x -> Product (Fields x)
forall x. POSable x => x -> Product (Fields x)
fields (I x -> x
forall a. I a -> a
unI I x
x) Product (Fields x)
-> NP Product (MapFields xs)
-> NP Product (Fields x : MapFields xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs -> NP Product (MapFields xs)
forall (xs :: [Type]).
All POSable xs =>
NP I xs -> NP Product (MapFields xs)
mapFields NP I xs
xs

map2Fields :: (All2 POSable xss) => NS (NP I) xss -> NS (NP Product) (Map2Fields xss)
map2Fields :: NS (NP I) xss -> NS (NP Product) (Map2Fields xss)
map2Fields (Z NP I x
x)  = NP Product (MapFields x)
-> NS (NP Product) (MapFields x : Map2Fields xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP I x -> NP Product (MapFields x)
forall (xs :: [Type]).
All POSable xs =>
NP I xs -> NP Product (MapFields xs)
mapFields NP I x
x)
map2Fields (S NS (NP I) xs
xs) = NS (NP Product) (Map2Fields xs)
-> NS (NP Product) (MapFields x : Map2Fields xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS (NP I) xs -> NS (NP Product) (Map2Fields xs)
forall (xss :: [[Type]]).
All2 POSable xss =>
NS (NP I) xss -> NS (NP Product) (Map2Fields xss)
map2Fields NS (NP I) xs
xs)

mapConcat :: NS (NP Product) xss -> NS Product (MapConcat xss)
mapConcat :: NS (NP Product) xss -> NS Product (MapConcat xss)
mapConcat (Z NP Product x
x)  = Product (Concat x) -> NS Product (Concat x : MapConcat xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP Product x -> Product (Concat x)
forall (xs :: [[[Type]]]). NP Product xs -> Product (Concat xs)
appends NP Product x
x)
mapConcat (S NS (NP Product) xs
xs) = NS Product (MapConcat xs) -> NS Product (Concat x : MapConcat xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS (NP Product) xs -> NS Product (MapConcat xs)
forall (xss :: [[[[Type]]]]).
NS (NP Product) xss -> NS Product (MapConcat xss)
mapConcat NS (NP Product) xs
xs)

appends :: NP Product xs -> Product (Concat xs)
appends :: NP Product xs -> Product (Concat xs)
appends NP Product xs
SOP.Nil   = Product '[]
Product (Concat xs)
Nil
appends (Product x
x :* NP Product xs
xs) = Product x -> Product (Concat xs) -> Product (x ++ Concat xs)
forall (x :: [[Type]]) (y :: [[Type]]).
Product x -> Product y -> Product (x ++ y)
concatP Product x
x (NP Product xs -> Product (Concat xs)
forall (xs :: [[[Type]]]). NP Product xs -> Product (Concat xs)
appends NP Product xs
xs)

foldMerge :: NP ProductType xss -> NS Product xss -> Product (FoldMerge xss)
foldMerge :: NP ProductType xss -> NS Product xss -> Product (FoldMerge xss)
foldMerge (ProductType x
_ :* NP ProductType xs
SOP.Nil) (Z Product x
y)   = Product x
Product (FoldMerge xss)
y
foldMerge (ProductType x
_ :* NP ProductType xs
SOP.Nil) (S NS Product xs
_)   = [Char] -> Product x
forall a. HasCallStack => [Char] -> a
error [Char]
"Reached an inaccessible pattern"
foldMerge NP ProductType xss
SOP.Nil   NS Product xss
_            = Product '[]
Product (FoldMerge xss)
Nil
foldMerge (ProductType x
_ :* ProductType x
x' :* NP ProductType xs
xs) (Z Product x
y)  = Either
  (Product x, ProductType (FoldMerge (x : xs)))
  (ProductType x, Product (FoldMerge (x : xs)))
-> Product (Merge x (FoldMerge (x : xs)))
forall (l :: [[Type]]) (r :: [[Type]]).
Either (Product l, ProductType r) (ProductType l, Product r)
-> Product (Merge l r)
merge (Either
   (Product x, ProductType (FoldMerge (x : xs)))
   (ProductType x, Product (FoldMerge (x : xs)))
 -> Product (Merge x (FoldMerge (x : xs))))
-> Either
     (Product x, ProductType (FoldMerge (x : xs)))
     (ProductType x, Product (FoldMerge (x : xs)))
-> Product (Merge x (FoldMerge (x : xs)))
forall a b. (a -> b) -> a -> b
$ (Product x, ProductType (FoldMerge (x : xs)))
-> Either
     (Product x, ProductType (FoldMerge (x : xs)))
     (ProductType x, Product (FoldMerge (x : xs)))
forall a b. a -> Either a b
Left (Product x
y, NP ProductType (x : xs) -> ProductType (FoldMerge (x : xs))
forall (xss :: [[[Type]]]).
NP ProductType xss -> ProductType (FoldMerge xss)
foldMergeT (ProductType x
x' ProductType x -> NP ProductType xs -> NP ProductType (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductType xs
xs))
foldMerge (ProductType x
x :* ProductType x
x' :* NP ProductType xs
xs) (S NS Product xs
ys) = Either
  (Product x, ProductType (FoldMerge (x : xs)))
  (ProductType x, Product (FoldMerge (x : xs)))
-> Product (Merge x (FoldMerge (x : xs)))
forall (l :: [[Type]]) (r :: [[Type]]).
Either (Product l, ProductType r) (ProductType l, Product r)
-> Product (Merge l r)
merge (Either
   (Product x, ProductType (FoldMerge (x : xs)))
   (ProductType x, Product (FoldMerge (x : xs)))
 -> Product (Merge x (FoldMerge (x : xs))))
-> Either
     (Product x, ProductType (FoldMerge (x : xs)))
     (ProductType x, Product (FoldMerge (x : xs)))
-> Product (Merge x (FoldMerge (x : xs)))
forall a b. (a -> b) -> a -> b
$ (ProductType x, Product (FoldMerge (x : xs)))
-> Either
     (Product x, ProductType (FoldMerge (x : xs)))
     (ProductType x, Product (FoldMerge (x : xs)))
forall a b. b -> Either a b
Right (ProductType x
x, NP ProductType (x : xs)
-> NS Product (x : xs) -> Product (FoldMerge (x : xs))
forall (xss :: [[[Type]]]).
NP ProductType xss -> NS Product xss -> Product (FoldMerge xss)
foldMerge (ProductType x
x' ProductType x -> NP ProductType xs -> NP ProductType (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductType xs
xs) NS Product xs
NS Product (x : xs)
ys)

appendsT :: NP ProductType xs -> ProductType (Concat xs)
appendsT :: NP ProductType xs -> ProductType (Concat xs)
appendsT NP ProductType xs
SOP.Nil   = ProductType '[]
ProductType (Concat xs)
PTNil
appendsT (ProductType x
x :* NP ProductType xs
xs) = ProductType x
-> ProductType (Concat xs) -> ProductType (x ++ Concat xs)
forall (x :: [[Type]]) (y :: [[Type]]).
ProductType x -> ProductType y -> ProductType (x ++ y)
concatPT ProductType x
x (NP ProductType xs -> ProductType (Concat xs)
forall (xs :: [[[Type]]]).
NP ProductType xs -> ProductType (Concat xs)
appendsT NP ProductType xs
xs)

mapConcatT :: NP (NP ProductType) xss -> NP ProductType (MapConcat xss)
mapConcatT :: NP (NP ProductType) xss -> NP ProductType (MapConcat xss)
mapConcatT NP (NP ProductType) xss
SOP.Nil   = NP ProductType (MapConcat xss)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
mapConcatT (NP ProductType x
x :* NP (NP ProductType) xs
xs) = NP ProductType x -> ProductType (Concat x)
forall (xs :: [[[Type]]]).
NP ProductType xs -> ProductType (Concat xs)
appendsT NP ProductType x
x ProductType (Concat x)
-> NP ProductType (MapConcat xs)
-> NP ProductType (Concat x : MapConcat xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (NP ProductType) xs -> NP ProductType (MapConcat xs)
forall (xss :: [[[[Type]]]]).
NP (NP ProductType) xss -> NP ProductType (MapConcat xss)
mapConcatT NP (NP ProductType) xs
xs

foldMergeT :: NP ProductType xss -> ProductType (FoldMerge xss)
foldMergeT :: NP ProductType xss -> ProductType (FoldMerge xss)
foldMergeT (ProductType x
x :* NP ProductType xs
SOP.Nil)  = ProductType x
ProductType (FoldMerge xss)
x
foldMergeT NP ProductType xss
SOP.Nil         = ProductType '[]
ProductType (FoldMerge xss)
PTNil
foldMergeT (ProductType x
x :* ProductType x
x' :* NP ProductType xs
xs) = ProductType x
-> ProductType (FoldMerge (x : xs))
-> ProductType (Merge x (FoldMerge (x : xs)))
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType x
x (NP ProductType (x : xs) -> ProductType (FoldMerge (x : xs))
forall (xss :: [[[Type]]]).
NP ProductType xss -> ProductType (FoldMerge xss)
foldMergeT (ProductType x
x' ProductType x -> NP ProductType xs -> NP ProductType (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductType xs
xs))

--------------------------------------------------------------------------------
-- Functions that deal with creating Products from types

newtype ProductFields a = ProductFields (Product (Fields a))

newtype ProductFieldsT a = ProductFieldsT (ProductType (Fields a))

newtype ProductConcatFieldsT a = ProductConcatFieldsT (ProductType (Concat (MapFields a)))

newtype ProductMapFieldsT a = ProductMapFieldsT (NP ProductType (MapFields a))

pureMapFields :: forall xs . (All POSable xs) => NP ProductType (MapFields xs)
pureMapFields :: NP ProductType (MapFields xs)
pureMapFields = NP ProductFieldsT xs -> NP ProductType (MapFields xs)
forall (ys :: [Type]).
NP ProductFieldsT ys -> NP ProductType (MapFields ys)
convert (NP ProductFieldsT xs -> NP ProductType (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductType (MapFields xs)
forall a b. (a -> b) -> a -> b
$ All POSable xs => NP ProductFieldsT xs
forall (xs :: [Type]). All POSable xs => NP ProductFieldsT xs
pureFields @xs
  where
    convert :: NP ProductFieldsT ys -> NP ProductType (MapFields ys)
    convert :: NP ProductFieldsT ys -> NP ProductType (MapFields ys)
convert NP ProductFieldsT ys
SOP.Nil                  = NP ProductType (MapFields ys)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
    convert (ProductFieldsT ProductType (Fields x)
x :* NP ProductFieldsT xs
xs) = ProductType (Fields x)
x ProductType (Fields x)
-> NP ProductType (MapFields xs)
-> NP ProductType (Fields x : MapFields xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductFieldsT xs -> NP ProductType (MapFields xs)
forall (ys :: [Type]).
NP ProductFieldsT ys -> NP ProductType (MapFields ys)
convert NP ProductFieldsT xs
xs

pureFields :: (All POSable xs) => NP ProductFieldsT xs
pureFields :: NP ProductFieldsT xs
pureFields = Proxy POSable
-> (forall a. POSable a => ProductFieldsT a)
-> NP ProductFieldsT xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy POSable
forall k (t :: k). Proxy t
Proxy :: Proxy POSable) forall a. POSable a => ProductFieldsT a
pureProductFields
  where
    pureProductFields :: forall x . (POSable x) => ProductFieldsT x
    pureProductFields :: ProductFieldsT x
pureProductFields = ProductType (Fields x) -> ProductFieldsT x
forall a. ProductType (Fields a) -> ProductFieldsT a
ProductFieldsT (ProductType (Fields x) -> ProductFieldsT x)
-> ProductType (Fields x) -> ProductFieldsT x
forall a b. (a -> b) -> a -> b
$ POSable x => ProductType (Fields x)
forall x. POSable x => ProductType (Fields x)
emptyFields @x

pureMap2Fields :: forall xss . (All2 POSable xss) => NP (NP ProductType) (Map2Fields xss)
pureMap2Fields :: NP (NP ProductType) (Map2Fields xss)
pureMap2Fields = NP ProductMapFieldsT xss -> NP (NP ProductType) (Map2Fields xss)
forall (yss :: [[Type]]).
NP ProductMapFieldsT yss -> NP (NP ProductType) (Map2Fields yss)
convert (NP ProductMapFieldsT xss -> NP (NP ProductType) (Map2Fields xss))
-> NP ProductMapFieldsT xss -> NP (NP ProductType) (Map2Fields xss)
forall a b. (a -> b) -> a -> b
$ All2 POSable xss => NP ProductMapFieldsT xss
forall (zss :: [[Type]]).
All2 POSable zss =>
NP ProductMapFieldsT zss
pure2Fields @xss
  where
    convert :: NP ProductMapFieldsT yss -> NP (NP ProductType) (Map2Fields yss)
    convert :: NP ProductMapFieldsT yss -> NP (NP ProductType) (Map2Fields yss)
convert NP ProductMapFieldsT yss
SOP.Nil                     = NP (NP ProductType) (Map2Fields yss)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
    convert (ProductMapFieldsT NP ProductType (MapFields x)
x :* NP ProductMapFieldsT xs
xs) = NP ProductType (MapFields x)
x NP ProductType (MapFields x)
-> NP (NP ProductType) (Map2Fields xs)
-> NP (NP ProductType) (MapFields x : Map2Fields xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductMapFieldsT xs -> NP (NP ProductType) (Map2Fields xs)
forall (yss :: [[Type]]).
NP ProductMapFieldsT yss -> NP (NP ProductType) (Map2Fields yss)
convert NP ProductMapFieldsT xs
xs

pure2Fields :: (All2 POSable zss) => NP ProductMapFieldsT zss
pure2Fields :: NP ProductMapFieldsT zss
pure2Fields = Proxy (All POSable)
-> (forall (a :: [Type]). All POSable a => ProductMapFieldsT a)
-> NP ProductMapFieldsT zss
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy (All POSable)
forall k (t :: k). Proxy t
Proxy :: Proxy (All POSable)) forall (a :: [Type]). All POSable a => ProductMapFieldsT a
pureProductMapFieldsT
  where
    pureProductMapFieldsT :: forall xs . (All POSable xs) => ProductMapFieldsT xs
    pureProductMapFieldsT :: ProductMapFieldsT xs
pureProductMapFieldsT = NP ProductType (MapFields xs) -> ProductMapFieldsT xs
forall (a :: [Type]).
NP ProductType (MapFields a) -> ProductMapFieldsT a
ProductMapFieldsT (NP ProductType (MapFields xs) -> ProductMapFieldsT xs)
-> NP ProductType (MapFields xs) -> ProductMapFieldsT xs
forall a b. (a -> b) -> a -> b
$ All POSable xs => NP ProductType (MapFields xs)
forall (xs :: [Type]).
All POSable xs =>
NP ProductType (MapFields xs)
pureMapFields @xs

pureConcatFields :: forall xss . (All2 POSable xss) => NP ProductConcatFieldsT xss
pureConcatFields :: NP ProductConcatFieldsT xss
pureConcatFields = NP ProductMapFieldsT xss -> NP ProductConcatFieldsT xss
forall (yss :: [[Type]]).
NP ProductMapFieldsT yss -> NP ProductConcatFieldsT yss
convert (NP ProductMapFieldsT xss -> NP ProductConcatFieldsT xss)
-> NP ProductMapFieldsT xss -> NP ProductConcatFieldsT xss
forall a b. (a -> b) -> a -> b
$ All2 POSable xss => NP ProductMapFieldsT xss
forall (zss :: [[Type]]).
All2 POSable zss =>
NP ProductMapFieldsT zss
pure2Fields @xss
  where
    convert :: NP ProductMapFieldsT yss -> NP ProductConcatFieldsT yss
    convert :: NP ProductMapFieldsT yss -> NP ProductConcatFieldsT yss
convert NP ProductMapFieldsT yss
SOP.Nil         = NP ProductConcatFieldsT yss
forall k (a :: k -> Type). NP a '[]
SOP.Nil
    convert (ProductMapFieldsT NP ProductType (MapFields x)
x :* NP ProductMapFieldsT xs
xs) = ProductType (Concat (MapFields x)) -> ProductConcatFieldsT x
forall (a :: [Type]).
ProductType (Concat (MapFields a)) -> ProductConcatFieldsT a
ProductConcatFieldsT (NP ProductType (MapFields x) -> ProductType (Concat (MapFields x))
forall (xs :: [[[Type]]]).
NP ProductType xs -> ProductType (Concat xs)
appendsT NP ProductType (MapFields x)
x) ProductConcatFieldsT x
-> NP ProductConcatFieldsT xs -> NP ProductConcatFieldsT (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductMapFieldsT xs -> NP ProductConcatFieldsT xs
forall (yss :: [[Type]]).
NP ProductMapFieldsT yss -> NP ProductConcatFieldsT yss
convert NP ProductMapFieldsT xs
xs

--------------------------------------------------------------------------------
-- Functions that deal with creating Choices from types

newtype FChoices a = FChoices (Finite (Choices a))

newtype ProductsMapChoices a = ProductsMapChoices (Finite (Products (MapChoices a)))

newtype FMapChoices a = FMapChoices (NP Finite (MapChoices a))

pureChoices2 :: forall xss . (All2 KnownNat (Map2Choices xss)) => (All2 POSable xss) => NP ProductsMapChoices xss
pureChoices2 :: NP ProductsMapChoices xss
pureChoices2 = NP FMapChoices xss -> NP ProductsMapChoices xss
forall (yss :: [[Type]]).
All2 KnownNat (Map2Choices yss) =>
NP FMapChoices yss -> NP ProductsMapChoices yss
convert (NP FMapChoices xss -> NP ProductsMapChoices xss)
-> NP FMapChoices xss -> NP ProductsMapChoices xss
forall a b. (a -> b) -> a -> b
$ All2 POSable xss => NP FMapChoices xss
forall (xss :: [[Type]]). All2 POSable xss => NP FMapChoices xss
pure2Choices @xss
  where
    convert :: (All2 KnownNat (Map2Choices yss)) => NP FMapChoices yss -> NP ProductsMapChoices yss
    convert :: NP FMapChoices yss -> NP ProductsMapChoices yss
convert NP FMapChoices yss
SOP.Nil         = NP ProductsMapChoices yss
forall k (a :: k -> Type). NP a '[]
SOP.Nil
    convert (FMapChoices NP Finite (MapChoices x)
x :* NP FMapChoices xs
xs) = Finite (Products (MapChoices x)) -> ProductsMapChoices x
forall (a :: [Type]).
Finite (Products (MapChoices a)) -> ProductsMapChoices a
ProductsMapChoices (NP Finite (MapChoices x) -> Finite (Products (MapChoices x))
forall (xs :: [Nat]).
All KnownNat xs =>
NP Finite xs -> Finite (Products xs)
combineProducts NP Finite (MapChoices x)
x) ProductsMapChoices x
-> NP ProductsMapChoices xs -> NP ProductsMapChoices (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP FMapChoices xs -> NP ProductsMapChoices xs
forall (yss :: [[Type]]).
All2 KnownNat (Map2Choices yss) =>
NP FMapChoices yss -> NP ProductsMapChoices yss
convert NP FMapChoices xs
xs

pureMapChoices :: forall xs . (All POSable xs) => NP Finite (MapChoices xs)
pureMapChoices :: NP Finite (MapChoices xs)
pureMapChoices = NP FChoices xs -> NP Finite (MapChoices xs)
forall (ys :: [Type]). NP FChoices ys -> NP Finite (MapChoices ys)
convert (NP FChoices xs -> NP Finite (MapChoices xs))
-> NP FChoices xs -> NP Finite (MapChoices xs)
forall a b. (a -> b) -> a -> b
$ All POSable xs => NP FChoices xs
forall (xs :: [Type]). All POSable xs => NP FChoices xs
pureChoices @xs
  where
    convert :: NP FChoices ys -> NP Finite (MapChoices ys)
    convert :: NP FChoices ys -> NP Finite (MapChoices ys)
convert NP FChoices ys
SOP.Nil            = NP Finite (MapChoices ys)
forall k (a :: k -> Type). NP a '[]
SOP.Nil
    convert (FChoices Finite (Choices x)
x :* NP FChoices xs
xs) = Finite (Choices x)
x Finite (Choices x)
-> NP Finite (MapChoices xs)
-> NP Finite (Choices x : MapChoices xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP FChoices xs -> NP Finite (MapChoices xs)
forall (ys :: [Type]). NP FChoices ys -> NP Finite (MapChoices ys)
convert NP FChoices xs
xs

pureChoices :: (All POSable xs) => NP FChoices xs
pureChoices :: NP FChoices xs
pureChoices = Proxy POSable
-> (forall a. POSable a => FChoices a) -> NP FChoices xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy POSable
forall k (t :: k). Proxy t
Proxy :: Proxy POSable) (Finite (Choices a) -> FChoices a
forall a. Finite (Choices a) -> FChoices a
FChoices Finite (Choices a)
0)

pure2Choices :: (All2 POSable xss) => NP FMapChoices xss
pure2Choices :: NP FMapChoices xss
pure2Choices = Proxy (All POSable)
-> (forall (a :: [Type]). All POSable a => FMapChoices a)
-> NP FMapChoices xss
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy (All POSable)
forall k (t :: k). Proxy t
Proxy :: Proxy (All POSable)) forall (a :: [Type]). All POSable a => FMapChoices a
pureFMapChoices
  where
    pureFMapChoices :: forall xs . (All POSable xs) => FMapChoices xs
    pureFMapChoices :: FMapChoices xs
pureFMapChoices = NP Finite (MapChoices xs) -> FMapChoices xs
forall (a :: [Type]). NP Finite (MapChoices a) -> FMapChoices a
FMapChoices (NP Finite (MapChoices xs) -> FMapChoices xs)
-> NP Finite (MapChoices xs) -> FMapChoices xs
forall a b. (a -> b) -> a -> b
$ All POSable xs => NP Finite (MapChoices xs)
forall (xs :: [Type]). All POSable xs => NP Finite (MapChoices xs)
pureMapChoices @xs

-------------------------------------------------------
-- Functions to get back to the SOP representation

separateProducts :: (All KnownNat (MapChoices xs)) => ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
separateProducts :: ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
separateProducts ProductsMapChoices xs
_ NP FChoices xs
SOP.Nil   = NP FChoices xs
forall k (a :: k -> Type). NP a '[]
SOP.Nil
separateProducts (ProductsMapChoices Finite (Products (MapChoices xs))
x) (FChoices x
_ :* NP FChoices xs
ys) = Finite (Choices x) -> FChoices x
forall a. Finite (Choices a) -> FChoices a
FChoices Finite (Choices x)
x' FChoices x -> NP FChoices xs -> NP FChoices (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
forall (xs :: [Type]).
All KnownNat (MapChoices xs) =>
ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
separateProducts (Finite (Products (MapChoices xs)) -> ProductsMapChoices xs
forall (a :: [Type]).
Finite (Products (MapChoices a)) -> ProductsMapChoices a
ProductsMapChoices Finite (Products (MapChoices xs))
xs) NP FChoices xs
ys
  where
    (Finite (Choices x)
x', Finite (Products (MapChoices xs))
xs)  = Finite (Choices x * Products (MapChoices xs))
-> (Finite (Choices x), Finite (Products (MapChoices xs)))
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct Finite (Choices x * Products (MapChoices xs))
Finite (Products (MapChoices xs))
x

zipFromPOSable :: All POSable xs => NP FChoices xs -> NP ProductFields xs -> NP I xs
zipFromPOSable :: NP FChoices xs -> NP ProductFields xs -> NP I xs
zipFromPOSable NP FChoices xs
SOP.Nil NP ProductFields xs
SOP.Nil = NP I xs
forall k (a :: k -> Type). NP a '[]
SOP.Nil
zipFromPOSable (FChoices Finite (Choices x)
c :* NP FChoices xs
cs) (ProductFields Product (Fields x)
f :* NP ProductFields xs
fs) = x -> I x
forall a. a -> I a
I (Finite (Choices x) -> Product (Fields x) -> x
forall x.
POSable x =>
Finite (Choices x) -> Product (Fields x) -> x
fromPOSable Finite (Choices x)
c Product (Fields x)
Product (Fields x)
f) I x -> NP I xs -> NP I (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP FChoices xs -> NP ProductFields xs -> NP I xs
forall (xs :: [Type]).
All POSable xs =>
NP FChoices xs -> NP ProductFields xs -> NP I xs
zipFromPOSable NP FChoices xs
cs NP ProductFields xs
NP ProductFields xs
fs

foldMergeT2 :: NP ProductConcatFieldsT xss -> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
foldMergeT2 :: NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
foldMergeT2 (ProductConcatFieldsT ProductType (Concat (MapFields x))
x :* NP ProductConcatFieldsT xs
SOP.Nil)  = ProductType (FoldMerge (MapConcat (Map2Fields xss)))
ProductType (Concat (MapFields x))
x
foldMergeT2 NP ProductConcatFieldsT xss
SOP.Nil                              = ProductType '[]
ProductType (FoldMerge (MapConcat (Map2Fields xss)))
PTNil
foldMergeT2 (ProductConcatFieldsT ProductType (Concat (MapFields x))
x :* ProductConcatFieldsT x
x' :* NP ProductConcatFieldsT xs
xs) = ProductType (Concat (MapFields x))
-> ProductType
     (FoldMerge (Concat (MapFields x) : MapConcat (Map2Fields xs)))
-> ProductType
     (Merge
        (Concat (MapFields x))
        (FoldMerge (Concat (MapFields x) : MapConcat (Map2Fields xs))))
forall (l :: [[Type]]) (r :: [[Type]]).
ProductType l -> ProductType r -> ProductType (Merge l r)
mergeT ProductType (Concat (MapFields x))
x (NP ProductConcatFieldsT (x : xs)
-> ProductType (FoldMerge (MapConcat (Map2Fields (x : xs))))
forall (xss :: [[Type]]).
NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
foldMergeT2 (ProductConcatFieldsT x
x' ProductConcatFieldsT x
-> NP ProductConcatFieldsT xs -> NP ProductConcatFieldsT (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ProductConcatFieldsT xs
xs))

unSums :: (All KnownNat (MapProducts (Map2Choices xs))) => Finite (Sums (MapProducts (Map2Choices xs))) -> NP ProductsMapChoices xs -> NS ProductsMapChoices xs
unSums :: Finite (Sums (MapProducts (Map2Choices xs)))
-> NP ProductsMapChoices xs -> NS ProductsMapChoices xs
unSums Finite (Sums (MapProducts (Map2Choices xs)))
_ NP ProductsMapChoices xs
SOP.Nil = [Char] -> NS ProductsMapChoices xs
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot construct empty sum"
unSums Finite (Sums (MapProducts (Map2Choices xs)))
x (ProductsMapChoices x
_ :* NP ProductsMapChoices xs
ys) = case Finite
  (Products (MapChoices x) + Sums (MapProducts (Map2Choices xs)))
-> Either
     (Finite (Products (MapChoices x)))
     (Finite (Sums (MapProducts (Map2Choices xs))))
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n + m) -> Either (Finite n) (Finite m)
separateSum Finite
  (Products (MapChoices x) + Sums (MapProducts (Map2Choices xs)))
Finite (Sums (MapProducts (Map2Choices xs)))
x of
  Left Finite (Products (MapChoices x))
x'  -> ProductsMapChoices x -> NS ProductsMapChoices (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (Finite (Products (MapChoices x)) -> ProductsMapChoices x
forall (a :: [Type]).
Finite (Products (MapChoices a)) -> ProductsMapChoices a
ProductsMapChoices Finite (Products (MapChoices x))
x')
  Right Finite (Sums (MapProducts (Map2Choices xs)))
x' -> NS ProductsMapChoices xs -> NS ProductsMapChoices (x : xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (Finite (Sums (MapProducts (Map2Choices xs)))
-> NP ProductsMapChoices xs -> NS ProductsMapChoices xs
forall (xs :: [[Type]]).
All KnownNat (MapProducts (Map2Choices xs)) =>
Finite (Sums (MapProducts (Map2Choices xs)))
-> NP ProductsMapChoices xs -> NS ProductsMapChoices xs
unSums Finite (Sums (MapProducts (Map2Choices xs)))
x' NP ProductsMapChoices xs
ys)

mapFromPOSable
  :: forall xss .
  ( All2 KnownNat (Map2Choices xss)
  , All2 POSable xss
  ) => NS ProductsMapChoices xss
  -> Product (FoldMerge (MapConcat (Map2Fields xss)))
  -> NP ProductConcatFieldsT xss
  -> NS (NP I) xss
mapFromPOSable :: NS ProductsMapChoices xss
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
-> NP ProductConcatFieldsT xss
-> NS (NP I) xss
mapFromPOSable (Z ProductsMapChoices x
cs) Product (FoldMerge (MapConcat (Map2Fields xss)))
fs fts :: NP ProductConcatFieldsT xss
fts@(ProductConcatFieldsT x
_ :* ProductConcatFieldsT x
_ :* NP ProductConcatFieldsT xs
_) = NP I x -> NS (NP I) (x : x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP FChoices x -> NP ProductFields x -> NP I x
forall (xs :: [Type]).
All POSable xs =>
NP FChoices xs -> NP ProductFields xs -> NP I xs
zipFromPOSable NP FChoices x
cs' ( Product (Concat (MapFields x))
-> NP ProductFieldsT x -> NP ProductFields x
forall (xs :: [Type]).
Product (Concat (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductFields xs
unConcat (Product
  (Merge
     (Concat (MapFields x))
     (FoldMerge (MapConcat (Map2Fields (x : xs)))))
-> NP ProductConcatFieldsT (x : x : xs)
-> Product (Concat (MapFields x))
forall (xs :: [Type]) (xss :: [[Type]]).
Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> NP ProductConcatFieldsT (xs : xss)
-> Product (Concat (MapFields xs))
unMergeLeft Product (FoldMerge (MapConcat (Map2Fields xss)))
Product
  (Merge
     (Concat (MapFields x))
     (FoldMerge (MapConcat (Map2Fields (x : xs)))))
fs NP ProductConcatFieldsT xss
NP ProductConcatFieldsT (x : x : xs)
fts) NP ProductFieldsT x
forall (xs :: [Type]). All POSable xs => NP ProductFieldsT xs
pureFields))
  where
    cs' :: NP FChoices x
cs' = ProductsMapChoices x -> NP FChoices x -> NP FChoices x
forall (xs :: [Type]).
All KnownNat (MapChoices xs) =>
ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
separateProducts ProductsMapChoices x
cs NP FChoices x
forall (xs :: [Type]). All POSable xs => NP FChoices xs
pureChoices
mapFromPOSable (S NS ProductsMapChoices xs
cs) Product (FoldMerge (MapConcat (Map2Fields xss)))
fs fts :: NP ProductConcatFieldsT xss
fts@(ProductConcatFieldsT x
_ :* ProductConcatFieldsT x
_ :* NP ProductConcatFieldsT xs
_) = NS (NP I) xs -> NS (NP I) (x : xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS ProductsMapChoices xs
-> Product (FoldMerge (MapConcat (Map2Fields xs)))
-> NP ProductConcatFieldsT xs
-> NS (NP I) xs
forall (xss :: [[Type]]).
(All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NS ProductsMapChoices xss
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
-> NP ProductConcatFieldsT xss
-> NS (NP I) xss
mapFromPOSable NS ProductsMapChoices xs
cs (Product
  (Merge
     (Concat (MapFields x))
     (FoldMerge (MapConcat (Map2Fields (x : xs)))))
-> NP ProductConcatFieldsT (x : x : xs)
-> Product (FoldMerge (MapConcat (Map2Fields (x : xs))))
forall (xs :: [Type]) (xss :: [[Type]]).
Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> NP ProductConcatFieldsT (xs : xss)
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
unMergeRight Product (FoldMerge (MapConcat (Map2Fields xss)))
Product
  (Merge
     (Concat (MapFields x))
     (FoldMerge (MapConcat (Map2Fields (x : xs)))))
fs NP ProductConcatFieldsT xss
NP ProductConcatFieldsT (x : x : xs)
fts) (NP ProductConcatFieldsT (x : xs) -> NP ProductConcatFieldsT xs
forall k (f :: k -> Type) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl NP ProductConcatFieldsT xss
NP ProductConcatFieldsT (x : xs)
fts))
mapFromPOSable (Z ProductsMapChoices x
cs) Product (FoldMerge (MapConcat (Map2Fields xss)))
fs (ProductConcatFieldsT x
_ :* NP ProductConcatFieldsT xs
SOP.Nil) = NP I x -> NS (NP I) '[x]
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP FChoices x -> NP ProductFields x -> NP I x
forall (xs :: [Type]).
All POSable xs =>
NP FChoices xs -> NP ProductFields xs -> NP I xs
zipFromPOSable NP FChoices x
cs' (Product (Concat (MapFields x))
-> NP ProductFieldsT x -> NP ProductFields x
forall (xs :: [Type]).
Product (Concat (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductFields xs
unConcat Product (FoldMerge (MapConcat (Map2Fields xss)))
Product (Concat (MapFields x))
fs NP ProductFieldsT x
forall (xs :: [Type]). All POSable xs => NP ProductFieldsT xs
pureFields))
  where
    cs' :: NP FChoices x
cs' = ProductsMapChoices x -> NP FChoices x -> NP FChoices x
forall (xs :: [Type]).
All KnownNat (MapChoices xs) =>
ProductsMapChoices xs -> NP FChoices xs -> NP FChoices xs
separateProducts ProductsMapChoices x
cs NP FChoices x
forall (xs :: [Type]). All POSable xs => NP FChoices xs
pureChoices
mapFromPOSable (S NS ProductsMapChoices xs
cs) Product (FoldMerge (MapConcat (Map2Fields xss)))
_ fts :: NP ProductConcatFieldsT xss
fts@(ProductConcatFieldsT x
_ :* NP ProductConcatFieldsT xs
SOP.Nil) = NS (NP I) xs -> NS (NP I) (x : xs)
forall k (a :: k -> Type) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS ProductsMapChoices xs
-> Product (FoldMerge (MapConcat (Map2Fields xs)))
-> NP ProductConcatFieldsT xs
-> NS (NP I) xs
forall (xss :: [[Type]]).
(All2 KnownNat (Map2Choices xss), All2 POSable xss) =>
NS ProductsMapChoices xss
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
-> NP ProductConcatFieldsT xss
-> NS (NP I) xss
mapFromPOSable NS ProductsMapChoices xs
cs Product '[]
Product (FoldMerge (MapConcat (Map2Fields xs)))
Nil (NP ProductConcatFieldsT (x : xs) -> NP ProductConcatFieldsT xs
forall k (f :: k -> Type) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl NP ProductConcatFieldsT xss
NP ProductConcatFieldsT (x : xs)
fts))

unConcat :: Product (Concat (MapFields xs)) -> NP ProductFieldsT xs -> NP ProductFields xs
unConcat :: Product (Concat (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductFields xs
unConcat Product (Concat (MapFields xs))
Nil NP ProductFieldsT xs
SOP.Nil     = NP ProductFields xs
forall k (a :: k -> Type). NP a '[]
SOP.Nil
unConcat Product (Concat (MapFields xs))
xs  (ProductFieldsT ProductType (Fields x)
ys :* NP ProductFieldsT xs
yss) = Product (Fields x) -> ProductFields x
forall a. Product (Fields a) -> ProductFields a
ProductFields Product (Fields x)
x' ProductFields x -> NP ProductFields xs -> NP ProductFields (x : xs)
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* Product (Concat (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductFields xs
forall (xs :: [Type]).
Product (Concat (MapFields xs))
-> NP ProductFieldsT xs -> NP ProductFields xs
unConcat Product (Concat (MapFields xs))
xs' NP ProductFieldsT xs
yss
  where
    (Product (Fields x)
x', Product (Concat (MapFields xs))
xs') = Product (Fields x ++ Concat (MapFields xs))
-> ProductType (Fields x)
-> (Product (Fields x), Product (Concat (MapFields xs)))
forall (x :: [[Type]]) (y :: [[Type]]).
Product (x ++ y) -> ProductType x -> (Product x, Product y)
unConcatP Product (Concat (MapFields xs))
Product (Fields x ++ Concat (MapFields xs))
xs ProductType (Fields x)
ys

unMergeLeft :: forall xs xss . Product (Merge (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss)))) -> NP ProductConcatFieldsT (xs ': xss) -> Product (Concat (MapFields xs))
unMergeLeft :: Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> NP ProductConcatFieldsT (xs : xss)
-> Product (Concat (MapFields xs))
unMergeLeft Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
xs (ProductConcatFieldsT ProductType (Concat (MapFields x))
y :* NP ProductConcatFieldsT xs
ys) = Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> ProductType (Concat (MapFields xs))
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
-> Product (Concat (MapFields xs))
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product l
splitLeft Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
xs ProductType (Concat (MapFields xs))
ProductType (Concat (MapFields x))
y (NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
forall (xss :: [[Type]]).
NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
foldMergeT2 @xss NP ProductConcatFieldsT xss
NP ProductConcatFieldsT xs
ys)

unMergeRight :: forall xs xss . Product (Merge (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss)))) -> NP ProductConcatFieldsT (xs ': xss) -> Product (FoldMerge (MapConcat (Map2Fields xss)))
unMergeRight :: Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> NP ProductConcatFieldsT (xs : xss)
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
unMergeRight Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
xs (ProductConcatFieldsT ProductType (Concat (MapFields x))
y :* NP ProductConcatFieldsT xs
ys) = Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
-> ProductType (Concat (MapFields xs))
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
-> Product (FoldMerge (MapConcat (Map2Fields xss)))
forall (l :: [[Type]]) (r :: [[Type]]).
Product (Merge l r) -> ProductType l -> ProductType r -> Product r
splitRight Product
  (Merge
     (Concat (MapFields xs)) (FoldMerge (MapConcat (Map2Fields xss))))
xs ProductType (Concat (MapFields xs))
ProductType (Concat (MapFields x))
y (NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
forall (xss :: [[Type]]).
NP ProductConcatFieldsT xss
-> ProductType (FoldMerge (MapConcat (Map2Fields xss)))
foldMergeT2 @xss NP ProductConcatFieldsT xss
NP ProductConcatFieldsT xs
ys)