{-# language DataKinds #-}
{-# language FlexibleContexts #-}
{-# language LambdaCase #-}
{-# language MultiParamTypeClasses #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeFamilies #-}
{-# language UndecidableInstances #-}

module Rel8.Column.NonEmpty
  ( HNonEmpty, AHNonEmpty(..)
  )
where

-- base
import Data.Kind ( Type )
import Data.List.NonEmpty ( NonEmpty )
import Data.Type.Equality ( (:~:)( Refl ) )
import Prelude

-- rel8
import Rel8.Aggregate ( Aggregate )
import Rel8.Expr ( Expr )
import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
import Rel8.Schema.Context ( Col )
import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
import qualified Rel8.Schema.Kind as K
import Rel8.Schema.Name ( Name )
import Rel8.Schema.Reify ( Reify, hreify, hunreify )
import Rel8.Schema.Result ( Result )
import Rel8.Table
  ( Table, Columns, Congruent, Context, fromColumns, toColumns
  , Unreify, reify, unreify
  )
import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
import Rel8.Table.Recontextualize ( Recontextualize )
import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )


-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
-- 'NonEmptyTable' @a@ in the 'Expr' context, and a 'NonEmpty' @a@ in the
-- 'Result' context.
type HNonEmpty :: K.Context -> Type -> Type
type family HNonEmpty context where
  HNonEmpty (Reify context) = AHNonEmpty context
  HNonEmpty Aggregate = NonEmptyTable
  HNonEmpty Expr = NonEmptyTable
  HNonEmpty Name = NonEmptyTable
  HNonEmpty Result = NonEmpty


type AHNonEmpty :: K.Context -> Type -> Type
newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)


instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
  Table (Reify context) (AHNonEmpty context a)
 where
  type Context (AHNonEmpty context a) = Reify context
  type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
  type Unreify (AHNonEmpty context a) = HNonEmpty context (Unreify a)

  fromColumns :: Columns (AHNonEmpty context a) (Col (Reify context))
-> AHNonEmpty context a
fromColumns = SContext context
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
sfromColumnsNonEmpty SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing
  toColumns :: AHNonEmpty context a
-> Columns (AHNonEmpty context a) (Col (Reify context))
toColumns = SContext context
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
stoColumnsNonEmpty SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing

  reify :: (Reify context :~: Reify ctx)
-> Unreify (AHNonEmpty context a) -> AHNonEmpty context a
reify Reify context :~: Reify ctx
_ = Unreifiability context a
-> HNonEmpty context (Unreify a) -> AHNonEmpty context a
forall (context :: Context) a.
Table (Reify context) a =>
Unreifiability context a
-> HNonEmpty context (Unreify a) -> AHNonEmpty context a
sreifyNonEmpty (SContext context -> Unreifiability context a
forall a (context :: Context).
(Context a ~ Reify context, Unreifiable a) =>
SContext context -> Unreifiability context a
unreifiability SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing)
  unreify :: (Reify context :~: Reify ctx)
-> AHNonEmpty context a -> Unreify (AHNonEmpty context a)
unreify Reify context :~: Reify ctx
_ = Unreifiability context a
-> AHNonEmpty context a -> HNonEmpty context (Unreify a)
forall (context :: Context) a.
Table (Reify context) a =>
Unreifiability context a
-> AHNonEmpty context a -> HNonEmpty context (Unreify a)
sunreifyNonEmpty (SContext context -> Unreifiability context a
forall a (context :: Context).
(Context a ~ Reify context, Unreifiable a) =>
SContext context -> Unreifiability context a
unreifiability SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing)


instance
  ( Reifiable context, Reifiable context'
  , Unreifiable a, Unreifiable a'
  , Recontextualize (Reify context) (Reify context') a a'
  )
  => Recontextualize
    (Reify context)
    (Reify context')
    (AHNonEmpty context a)
    (AHNonEmpty context' a')


smapNonEmpty :: Congruent a b
  => SContext context
  -> (a -> b)
  -> (HNonEmptyTable (Columns a) (Col (Context a)) -> HNonEmptyTable (Columns b) (Col (Context b)))
  -> AHNonEmpty context a
  -> AHNonEmpty context b
smapNonEmpty :: SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty = \case
  SContext context
SAggregate -> \a -> b
_ HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f (AHNonEmpty (NonEmptyTable a)) -> HNonEmpty context b -> AHNonEmpty context b
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (HNonEmptyTable (Columns b) (Col (Context b)) -> NonEmptyTable b
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f HNonEmptyTable (Columns a) (Col (Context a))
a))
  SContext context
SExpr -> \a -> b
_ HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f (AHNonEmpty (NonEmptyTable a)) -> HNonEmpty context b -> AHNonEmpty context b
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (HNonEmptyTable (Columns b) (Col (Context b)) -> NonEmptyTable b
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f HNonEmptyTable (Columns a) (Col (Context a))
a))
  SContext context
SResult -> \a -> b
f HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
_ (AHNonEmpty HNonEmpty context a
as) -> HNonEmpty context b -> AHNonEmpty context b
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty ((a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f NonEmpty a
HNonEmpty context a
as)
  SContext context
SName -> \a -> b
_ HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f (AHNonEmpty (NonEmptyTable a)) -> HNonEmpty context b -> AHNonEmpty context b
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (HNonEmptyTable (Columns b) (Col (Context b)) -> NonEmptyTable b
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
f HNonEmptyTable (Columns a) (Col (Context a))
a))
  SReify SContext context
context -> \a -> b
f HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
g (AHNonEmpty HNonEmpty context a
as) -> HNonEmpty context b -> AHNonEmpty context b
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty SContext context
context a -> b
f HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns b) (Col (Context b))
g AHNonEmpty context a
HNonEmpty context a
as)


sfromColumnsNonEmpty :: Table (Reify context) a
  => SContext context
  -> HNonEmptyTable (Columns a) (Col (Reify context))
  -> AHNonEmpty context a
sfromColumnsNonEmpty :: SContext context
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
sfromColumnsNonEmpty = \case
  SContext context
SAggregate -> NonEmptyTable a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (NonEmptyTable a -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify Aggregate))
    -> NonEmptyTable a)
-> HNonEmptyTable (Columns a) (Col (Reify Aggregate))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HNonEmptyTable (Columns a) (Col (Reify Aggregate))
-> NonEmptyTable a
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable
  SContext context
SExpr -> NonEmptyTable a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (NonEmptyTable a -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify Expr))
    -> NonEmptyTable a)
-> HNonEmptyTable (Columns a) (Col (Reify Expr))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HNonEmptyTable (Columns a) (Col (Reify Expr)) -> NonEmptyTable a
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable
  SContext context
SResult ->
    NonEmpty a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (NonEmpty a -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify context)) -> NonEmpty a)
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Columns a (Col Result) -> a)
-> NonEmpty (Columns a (Col Result)) -> NonEmpty a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Columns a (Col (Reify Result)) -> a
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (Columns a (Col (Reify Result)) -> a)
-> (Columns a (Col Result) -> Columns a (Col (Reify Result)))
-> Columns a (Col Result)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns a (Col Result) -> Columns a (Col (Reify Result))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify) (NonEmpty (Columns a (Col Result)) -> NonEmpty a)
-> (HNonEmptyTable (Columns a) (Col (Reify context))
    -> NonEmpty (Columns a (Col Result)))
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> NonEmpty a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HVectorize NonEmpty (Columns a) (Col context)
-> NonEmpty (Columns a (Col Result))
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (HVectorize NonEmpty (Columns a) (Col context)
 -> NonEmpty (Columns a (Col Result)))
-> (HNonEmptyTable (Columns a) (Col (Reify context))
    -> HVectorize NonEmpty (Columns a) (Col context))
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> NonEmpty (Columns a (Col Result))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HNonEmptyTable (Columns a) (Col (Reify context))
-> HVectorize NonEmpty (Columns a) (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SContext context
SName -> NonEmptyTable a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (NonEmptyTable a -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify Name))
    -> NonEmptyTable a)
-> HNonEmptyTable (Columns a) (Col (Reify Name))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HNonEmptyTable (Columns a) (Col (Reify Name)) -> NonEmptyTable a
forall a.
HNonEmptyTable (Columns a) (Col (Context a)) -> NonEmptyTable a
NonEmptyTable
  SReify SContext context
context ->
    AHNonEmpty context a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (AHNonEmpty context a -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify context))
    -> AHNonEmpty context a)
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (Columns a (Col (Reify context)) -> a)
-> (HNonEmptyTable
      (Columns (Columns a (Col (Reify context))))
      (Col (Context (Columns a (Col (Reify context)))))
    -> HNonEmptyTable (Columns a) (Col (Context a)))
-> AHNonEmpty context (Columns a (Col (Reify context)))
-> AHNonEmpty context a
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty SContext context
context (Columns a (Col (Reify (Reify context))) -> a
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (Columns a (Col (Reify (Reify context))) -> a)
-> (Columns a (Col (Reify context))
    -> Columns a (Col (Reify (Reify context))))
-> Columns a (Col (Reify context))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Columns a (Col (Reify context))
-> Columns a (Col (Reify (Reify context)))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify) HNonEmptyTable
  (Columns (Columns a (Col (Reify context))))
  (Col (Context (Columns a (Col (Reify context)))))
-> HNonEmptyTable (Columns a) (Col (Context a))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (AHNonEmpty context (Columns a (Col (Reify context)))
 -> AHNonEmpty context a)
-> (HNonEmptyTable (Columns a) (Col (Reify context))
    -> AHNonEmpty context (Columns a (Col (Reify context))))
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> HNonEmptyTable
     (Columns (Columns a (Col (Reify context)))) (Col (Reify context))
-> AHNonEmpty context (Columns a (Col (Reify context)))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context a
sfromColumnsNonEmpty SContext context
context (HVectorize NonEmpty (Columns a) (Col context)
 -> AHNonEmpty context (Columns a (Col (Reify context))))
-> (HNonEmptyTable (Columns a) (Col (Reify context))
    -> HVectorize NonEmpty (Columns a) (Col context))
-> HNonEmptyTable (Columns a) (Col (Reify context))
-> AHNonEmpty context (Columns a (Col (Reify context)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    HNonEmptyTable (Columns a) (Col (Reify context))
-> HVectorize NonEmpty (Columns a) (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify


stoColumnsNonEmpty :: Table (Reify context) a
  => SContext context
  -> AHNonEmpty context a
  -> HNonEmptyTable (Columns a) (Col (Reify context))
stoColumnsNonEmpty :: SContext context
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
stoColumnsNonEmpty = \case
  SContext context
SAggregate -> \(AHNonEmpty (NonEmptyTable a)) -> HNonEmptyTable (Columns a) (Col (Reify context))
HNonEmptyTable (Columns a) (Col (Context a))
a
  SContext context
SExpr -> \(AHNonEmpty (NonEmptyTable a)) -> HNonEmptyTable (Columns a) (Col (Reify context))
HNonEmptyTable (Columns a) (Col (Context a))
a
  SContext context
SResult ->
    HVectorize NonEmpty (Columns a) (Col context)
-> HNonEmptyTable (Columns a) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (HVectorize NonEmpty (Columns a) (Col context)
 -> HNonEmptyTable (Columns a) (Col (Reify context)))
-> (AHNonEmpty context a
    -> HVectorize NonEmpty (Columns a) (Col context))
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Columns a (Col Result))
-> HVectorize NonEmpty (Columns a) (Col context)
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns (NonEmpty (Columns a (Col Result))
 -> HVectorize NonEmpty (Columns a) (Col context))
-> (AHNonEmpty context a -> NonEmpty (Columns a (Col Result)))
-> AHNonEmpty context a
-> HVectorize NonEmpty (Columns a) (Col context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Columns a (Col Result))
-> NonEmpty a -> NonEmpty (Columns a (Col Result))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Columns a (Col (Reify Result)) -> Columns a (Col Result)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Columns a (Col (Reify Result)) -> Columns a (Col Result))
-> (a -> Columns a (Col (Reify Result)))
-> a
-> Columns a (Col Result)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Columns a (Col (Reify Result))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns) (NonEmpty a -> NonEmpty (Columns a (Col Result)))
-> (AHNonEmpty context a -> NonEmpty a)
-> AHNonEmpty context a
-> NonEmpty (Columns a (Col Result))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHNonEmpty HNonEmpty context a
a) -> NonEmpty a
HNonEmpty context a
a)
  SContext context
SName -> \(AHNonEmpty (NonEmptyTable a)) -> HNonEmptyTable (Columns a) (Col (Reify context))
HNonEmptyTable (Columns a) (Col (Context a))
a
  SReify SContext context
context ->
    HVectorize NonEmpty (Columns a) (Col context)
-> HNonEmptyTable (Columns a) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (HVectorize NonEmpty (Columns a) (Col context)
 -> HNonEmptyTable (Columns a) (Col (Reify context)))
-> (AHNonEmpty context a
    -> HVectorize NonEmpty (Columns a) (Col context))
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> AHNonEmpty context (Columns a (Col (Reify context)))
-> HNonEmptyTable
     (Columns (Columns a (Col (Reify context)))) (Col (Reify context))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> AHNonEmpty context a
-> HNonEmptyTable (Columns a) (Col (Reify context))
stoColumnsNonEmpty SContext context
context (AHNonEmpty context (Columns a (Col (Reify context)))
 -> HVectorize NonEmpty (Columns a) (Col context))
-> (AHNonEmpty context a
    -> AHNonEmpty context (Columns a (Col (Reify context))))
-> AHNonEmpty context a
-> HVectorize NonEmpty (Columns a) (Col context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (a -> Columns a (Col (Reify context)))
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable
         (Columns (Columns a (Col (Reify context))))
         (Col (Context (Columns a (Col (Reify context))))))
-> AHNonEmpty context a
-> AHNonEmpty context (Columns a (Col (Reify context)))
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty SContext context
context (Columns a (Col (Reify (Reify context)))
-> Columns a (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (Columns a (Col (Reify (Reify context)))
 -> Columns a (Col (Reify context)))
-> (a -> Columns a (Col (Reify (Reify context))))
-> a
-> Columns a (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Columns a (Col (Reify (Reify context)))
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns) HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable
     (Columns (Columns a (Col (Reify context))))
     (Col (Context (Columns a (Col (Reify context)))))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify (AHNonEmpty context a
 -> AHNonEmpty context (Columns a (Col (Reify context))))
-> (AHNonEmpty context a -> AHNonEmpty context a)
-> AHNonEmpty context a
-> AHNonEmpty context (Columns a (Col (Reify context)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (\(AHNonEmpty HNonEmpty context a
a) -> AHNonEmpty context a
HNonEmpty context a
a)


sreifyNonEmpty :: Table (Reify context) a
  => Unreifiability context a
  -> HNonEmpty context (Unreify a)
  -> AHNonEmpty context a
sreifyNonEmpty :: Unreifiability context a
-> HNonEmpty context (Unreify a) -> AHNonEmpty context a
sreifyNonEmpty = \case
  Unreifiability context a
UResult -> NonEmpty a -> AHNonEmpty context a
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty (NonEmpty a -> AHNonEmpty context a)
-> (NonEmpty (Unreify a) -> NonEmpty a)
-> NonEmpty (Unreify a)
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unreify a -> a) -> NonEmpty (Unreify a) -> NonEmpty a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Reify Result :~: Reify Result) -> Unreify a -> a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify Reify Result :~: Reify Result
forall k (a :: k). a :~: a
Refl)
  Unreifiability SContext context
context ->
    SContext context
-> (Unreify a -> a)
-> (HNonEmptyTable
      (Columns (Unreify a)) (Col (Context (Unreify a)))
    -> HNonEmptyTable (Columns a) (Col (Context a)))
-> AHNonEmpty context (Unreify a)
-> AHNonEmpty context a
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty SContext context
context ((Reify context :~: Reify context) -> Unreify a -> a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> Unreify a -> a
reify Reify context :~: Reify context
forall k (a :: k). a :~: a
Refl) HNonEmptyTable (Columns (Unreify a)) (Col (Context (Unreify a)))
-> HNonEmptyTable (Columns a) (Col (Context a))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (AHNonEmpty context (Unreify a) -> AHNonEmpty context a)
-> (HNonEmpty context (Unreify a)
    -> AHNonEmpty context (Unreify a))
-> HNonEmpty context (Unreify a)
-> AHNonEmpty context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    HNonEmpty context (Unreify a) -> AHNonEmpty context (Unreify a)
forall (context :: Context) a.
HNonEmpty context a -> AHNonEmpty context a
AHNonEmpty


sunreifyNonEmpty :: Table (Reify context) a
  => Unreifiability context a
  -> AHNonEmpty context a
  -> HNonEmpty context (Unreify a)
sunreifyNonEmpty :: Unreifiability context a
-> AHNonEmpty context a -> HNonEmpty context (Unreify a)
sunreifyNonEmpty = \case
  Unreifiability context a
UResult -> (a -> Unreify a) -> NonEmpty a -> NonEmpty (Unreify a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Reify Result :~: Reify Result) -> a -> Unreify a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify Reify Result :~: Reify Result
forall k (a :: k). a :~: a
Refl) (NonEmpty a -> NonEmpty (Unreify a))
-> (AHNonEmpty context a -> NonEmpty a)
-> AHNonEmpty context a
-> NonEmpty (Unreify a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHNonEmpty HNonEmpty context a
a) -> NonEmpty a
HNonEmpty context a
a)
  Unreifiability SContext context
context ->
    (\(AHNonEmpty HNonEmpty context (Unreify a)
a) -> HNonEmpty context (Unreify a)
a) (AHNonEmpty context (Unreify a) -> HNonEmpty context (Unreify a))
-> (AHNonEmpty context a -> AHNonEmpty context (Unreify a))
-> AHNonEmpty context a
-> HNonEmpty context (Unreify a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (a -> Unreify a)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable
         (Columns (Unreify a)) (Col (Context (Unreify a))))
-> AHNonEmpty context a
-> AHNonEmpty context (Unreify a)
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HNonEmptyTable (Columns a) (Col (Context a))
    -> HNonEmptyTable (Columns b) (Col (Context b)))
-> AHNonEmpty context a
-> AHNonEmpty context b
smapNonEmpty SContext context
context ((Reify context :~: Reify context) -> a -> Unreify a
forall (context :: Context) a (ctx :: Context).
Table context a =>
(context :~: Reify ctx) -> a -> Unreify a
unreify Reify context :~: Reify context
forall k (a :: k). a :~: a
Refl) HNonEmptyTable (Columns a) (Col (Context a))
-> HNonEmptyTable (Columns (Unreify a)) (Col (Context (Unreify a)))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify