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

module Rel8.Column.List
  ( HList, AHList(..)
  )
where

-- base
import Data.Kind ( Type )
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.List ( HListTable )
import Rel8.Schema.Insert ( Insert )
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.List ( ListTable( ListTable ) )
import Rel8.Table.Recontextualize ( Recontextualize )
import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )


type HList :: K.Context -> Type -> Type
type family HList context where
  HList (Reify context) = AHList context
  HList Aggregate = ListTable
  HList Expr = ListTable
  HList Insert = ListTable
  HList Name = ListTable
  HList Result = []


type AHList :: K.Context -> Type -> Type
newtype AHList context a = AHList (HList context a)


instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
  Table (Reify context) (AHList context a)
 where
  type Context (AHList context a) = Reify context
  type Columns (AHList context a) = HListTable (Columns a)
  type Unreify (AHList context a) = HList context (Unreify a)

  fromColumns :: Columns (AHList context a) (Col (Reify context))
-> AHList context a
fromColumns = SContext context
-> HListTable (Columns a) (Col (Reify context)) -> AHList context a
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> HListTable (Columns a) (Col (Reify context)) -> AHList context a
sfromColumnsList SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing
  toColumns :: AHList context a
-> Columns (AHList context a) (Col (Reify context))
toColumns = SContext context
-> AHList context a -> HListTable (Columns a) (Col (Reify context))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> AHList context a -> HListTable (Columns a) (Col (Reify context))
stoColumnsList SContext context
forall (context :: Context). Reifiable context => SContext context
contextSing

  reify :: (Reify context :~: Reify ctx)
-> Unreify (AHList context a) -> AHList context a
reify Reify context :~: Reify ctx
_ = Unreifiability context a
-> HList context (Unreify a) -> AHList context a
forall (context :: Context) a.
Table (Reify context) a =>
Unreifiability context a
-> HList context (Unreify a) -> AHList context a
sreifyList (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)
-> AHList context a -> Unreify (AHList context a)
unreify Reify context :~: Reify ctx
_ = Unreifiability context a
-> AHList context a -> HList context (Unreify a)
forall (context :: Context) a.
Table (Reify context) a =>
Unreifiability context a
-> AHList context a -> HList context (Unreify a)
sunreifyList (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')
    (AHList context a)
    (AHList context' a')


smapList :: Congruent a b
  => SContext context
  -> (a -> b)
  -> (HListTable (Columns a) (Col (Context a)) -> HListTable (Columns b) (Col (Context b)))
  -> AHList context a
  -> AHList context b
smapList :: SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList = \case
  SContext context
SAggregate -> \a -> b
_ HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f (AHList (ListTable a)) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList (HListTable (Columns b) (Col (Context b)) -> ListTable b
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable (HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f HListTable (Columns a) (Col (Context a))
a))
  SContext context
SExpr -> \a -> b
_ HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f (AHList (ListTable a)) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList (HListTable (Columns b) (Col (Context b)) -> ListTable b
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable (HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f HListTable (Columns a) (Col (Context a))
a))
  SContext context
SResult -> \a -> b
f HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
_ (AHList HList context a
as) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList ((a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f [a]
HList context a
as)
  SContext context
SInsert -> \a -> b
_ HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f (AHList (ListTable a)) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList (HListTable (Columns b) (Col (Context b)) -> ListTable b
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable (HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f HListTable (Columns a) (Col (Context a))
a))
  SContext context
SName -> \a -> b
_ HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f (AHList (ListTable a)) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList (HListTable (Columns b) (Col (Context b)) -> ListTable b
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable (HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
f HListTable (Columns a) (Col (Context a))
a))
  SReify SContext context
context -> \a -> b
f HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
g (AHList HList context a
as) -> HList context b -> AHList context b
forall (context :: Context) a. HList context a -> AHList context a
AHList (SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList SContext context
context a -> b
f HListTable (Columns a) (Col (Context a))
-> HListTable (Columns b) (Col (Context b))
g AHList context a
HList context a
as)


sfromColumnsList :: Table (Reify context) a
  => SContext context
  -> HListTable (Columns a) (Col (Reify context))
  -> AHList context a
sfromColumnsList :: SContext context
-> HListTable (Columns a) (Col (Reify context)) -> AHList context a
sfromColumnsList = \case
  SContext context
SAggregate -> ListTable a -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList (ListTable a -> AHList context a)
-> (HListTable (Columns a) (Col (Reify Aggregate)) -> ListTable a)
-> HListTable (Columns a) (Col (Reify Aggregate))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HListTable (Columns a) (Col (Reify Aggregate)) -> ListTable a
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable
  SContext context
SExpr -> ListTable a -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList (ListTable a -> AHList context a)
-> (HListTable (Columns a) (Col (Reify Expr)) -> ListTable a)
-> HListTable (Columns a) (Col (Reify Expr))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HListTable (Columns a) (Col (Reify Expr)) -> ListTable a
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable
  SContext context
SResult -> [a] -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList ([a] -> AHList context a)
-> (HListTable (Columns a) (Col (Reify context)) -> [a])
-> HListTable (Columns a) (Col (Reify context))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Columns a (Col Result) -> a) -> [Columns a (Col Result)] -> [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) ([Columns a (Col Result)] -> [a])
-> (HListTable (Columns a) (Col (Reify context))
    -> [Columns a (Col Result)])
-> HListTable (Columns a) (Col (Reify context))
-> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HVectorize [] (Columns a) (Col context) -> [Columns a (Col Result)]
forall (context :: Context) a.
Table context a =>
Columns a (Col context) -> a
fromColumns (HVectorize [] (Columns a) (Col context)
 -> [Columns a (Col Result)])
-> (HListTable (Columns a) (Col (Reify context))
    -> HVectorize [] (Columns a) (Col context))
-> HListTable (Columns a) (Col (Reify context))
-> [Columns a (Col Result)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HListTable (Columns a) (Col (Reify context))
-> HVectorize [] (Columns a) (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify
  SContext context
SInsert -> ListTable a -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList (ListTable a -> AHList context a)
-> (HListTable (Columns a) (Col (Reify Insert)) -> ListTable a)
-> HListTable (Columns a) (Col (Reify Insert))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HListTable (Columns a) (Col (Reify Insert)) -> ListTable a
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable
  SContext context
SName -> ListTable a -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList (ListTable a -> AHList context a)
-> (HListTable (Columns a) (Col (Reify Name)) -> ListTable a)
-> HListTable (Columns a) (Col (Reify Name))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HListTable (Columns a) (Col (Reify Name)) -> ListTable a
forall a. HListTable (Columns a) (Col (Context a)) -> ListTable a
ListTable
  SReify SContext context
context ->
    AHList context a -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList (AHList context a -> AHList context a)
-> (HListTable (Columns a) (Col (Reify context))
    -> AHList context a)
-> HListTable (Columns a) (Col (Reify context))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (Columns a (Col (Reify context)) -> a)
-> (HListTable
      (Columns (Columns a (Col (Reify context))))
      (Col (Context (Columns a (Col (Reify context)))))
    -> HListTable (Columns a) (Col (Context a)))
-> AHList context (Columns a (Col (Reify context)))
-> AHList context a
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList 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) HListTable
  (Columns (Columns a (Col (Reify context))))
  (Col (Context (Columns a (Col (Reify context)))))
-> HListTable (Columns a) (Col (Context a))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (AHList context (Columns a (Col (Reify context)))
 -> AHList context a)
-> (HListTable (Columns a) (Col (Reify context))
    -> AHList context (Columns a (Col (Reify context))))
-> HListTable (Columns a) (Col (Reify context))
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> HListTable
     (Columns (Columns a (Col (Reify context)))) (Col (Reify context))
-> AHList context (Columns a (Col (Reify context)))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> HListTable (Columns a) (Col (Reify context)) -> AHList context a
sfromColumnsList SContext context
context (HVectorize [] (Columns a) (Col context)
 -> AHList context (Columns a (Col (Reify context))))
-> (HListTable (Columns a) (Col (Reify context))
    -> HVectorize [] (Columns a) (Col context))
-> HListTable (Columns a) (Col (Reify context))
-> AHList context (Columns a (Col (Reify context)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    HListTable (Columns a) (Col (Reify context))
-> HVectorize [] (Columns a) (Col context)
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify


stoColumnsList :: Table (Reify context) a
  => SContext context
  -> AHList context a
  -> HListTable (Columns a) (Col (Reify context))
stoColumnsList :: SContext context
-> AHList context a -> HListTable (Columns a) (Col (Reify context))
stoColumnsList = \case
  SContext context
SAggregate -> \(AHList (ListTable a)) -> HListTable (Columns a) (Col (Reify context))
HListTable (Columns a) (Col (Context a))
a
  SContext context
SExpr -> \(AHList (ListTable a)) -> HListTable (Columns a) (Col (Reify context))
HListTable (Columns a) (Col (Context a))
a
  SContext context
SResult ->
    HVectorize [] (Columns a) (Col context)
-> HListTable (Columns a) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (HVectorize [] (Columns a) (Col context)
 -> HListTable (Columns a) (Col (Reify context)))
-> (AHList context a -> HVectorize [] (Columns a) (Col context))
-> AHList context a
-> HListTable (Columns a) (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Columns a (Col Result)] -> HVectorize [] (Columns a) (Col context)
forall (context :: Context) a.
Table context a =>
a -> Columns a (Col context)
toColumns ([Columns a (Col Result)]
 -> HVectorize [] (Columns a) (Col context))
-> (AHList context a -> [Columns a (Col Result)])
-> AHList context a
-> HVectorize [] (Columns a) (Col context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Columns a (Col Result)) -> [a] -> [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) ([a] -> [Columns a (Col Result)])
-> (AHList context a -> [a])
-> AHList context a
-> [Columns a (Col Result)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHList HList context a
a) -> [a]
HList context a
a)
  SContext context
SInsert -> \(AHList (ListTable a)) -> HListTable (Columns a) (Col (Reify context))
HListTable (Columns a) (Col (Context a))
a
  SContext context
SName -> \(AHList (ListTable a)) -> HListTable (Columns a) (Col (Reify context))
HListTable (Columns a) (Col (Context a))
a
  SReify SContext context
context ->
    HVectorize [] (Columns a) (Col context)
-> HListTable (Columns a) (Col (Reify context))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (HVectorize [] (Columns a) (Col context)
 -> HListTable (Columns a) (Col (Reify context)))
-> (AHList context a -> HVectorize [] (Columns a) (Col context))
-> AHList context a
-> HListTable (Columns a) (Col (Reify context))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> AHList context (Columns a (Col (Reify context)))
-> HListTable
     (Columns (Columns a (Col (Reify context)))) (Col (Reify context))
forall (context :: Context) a.
Table (Reify context) a =>
SContext context
-> AHList context a -> HListTable (Columns a) (Col (Reify context))
stoColumnsList SContext context
context (AHList context (Columns a (Col (Reify context)))
 -> HVectorize [] (Columns a) (Col context))
-> (AHList context a
    -> AHList context (Columns a (Col (Reify context))))
-> AHList context a
-> HVectorize [] (Columns a) (Col context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (a -> Columns a (Col (Reify context)))
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable
         (Columns (Columns a (Col (Reify context))))
         (Col (Context (Columns a (Col (Reify context))))))
-> AHList context a
-> AHList context (Columns a (Col (Reify context)))
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList 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) HListTable (Columns a) (Col (Context a))
-> HListTable
     (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 (AHList context a
 -> AHList context (Columns a (Col (Reify context))))
-> (AHList context a -> AHList context a)
-> AHList context a
-> AHList context (Columns a (Col (Reify context)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (\(AHList HList context a
a) -> AHList context a
HList context a
a)


sreifyList :: Table (Reify context) a
  => Unreifiability context a
  -> HList context (Unreify a)
  -> AHList context a
sreifyList :: Unreifiability context a
-> HList context (Unreify a) -> AHList context a
sreifyList = \case
  Unreifiability context a
UResult -> [a] -> AHList context a
forall (context :: Context) a. HList context a -> AHList context a
AHList ([a] -> AHList context a)
-> ([Unreify a] -> [a]) -> [Unreify a] -> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unreify a -> a) -> [Unreify a] -> [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)
-> (HListTable (Columns (Unreify a)) (Col (Context (Unreify a)))
    -> HListTable (Columns a) (Col (Context a)))
-> AHList context (Unreify a)
-> AHList context a
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList 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) HListTable (Columns (Unreify a)) (Col (Context (Unreify a)))
-> HListTable (Columns a) (Col (Context a))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col context) -> t (Col (Reify context))
hreify (AHList context (Unreify a) -> AHList context a)
-> (HList context (Unreify a) -> AHList context (Unreify a))
-> HList context (Unreify a)
-> AHList context a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    HList context (Unreify a) -> AHList context (Unreify a)
forall (context :: Context) a. HList context a -> AHList context a
AHList


sunreifyList :: Table (Reify context) a
  => Unreifiability context a
  -> AHList context a
  -> HList context (Unreify a)
sunreifyList :: Unreifiability context a
-> AHList context a -> HList context (Unreify a)
sunreifyList = \case
  Unreifiability context a
UResult -> (a -> Unreify a) -> [a] -> [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) ([a] -> [Unreify a])
-> (AHList context a -> [a]) -> AHList context a -> [Unreify a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(AHList HList context a
a) -> [a]
HList context a
a)
  Unreifiability SContext context
context ->
    (\(AHList HList context (Unreify a)
a) -> HList context (Unreify a)
a) (AHList context (Unreify a) -> HList context (Unreify a))
-> (AHList context a -> AHList context (Unreify a))
-> AHList context a
-> HList context (Unreify a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    SContext context
-> (a -> Unreify a)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns (Unreify a)) (Col (Context (Unreify a))))
-> AHList context a
-> AHList context (Unreify a)
forall a b (context :: Context).
Congruent a b =>
SContext context
-> (a -> b)
-> (HListTable (Columns a) (Col (Context a))
    -> HListTable (Columns b) (Col (Context b)))
-> AHList context a
-> AHList context b
smapList 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) HListTable (Columns a) (Col (Context a))
-> HListTable (Columns (Unreify a)) (Col (Context (Unreify a)))
forall (t :: HTable) (context :: Context).
HTable t =>
t (Col (Reify context)) -> t (Col context)
hunreify