module UVMHS.Lib.Dataframe where

import UVMHS.Core

import UVMHS.Lib.Pretty

import qualified Data.Vector          as Vector
import qualified Data.ByteString.Lazy as BSL
import qualified Data.Csv             as CSV
import qualified Data.Text.Encoding   as Text
import qualified Prelude              as HS
import qualified Text.Read            as HS

data FrameType =
    B_FT
  | N_FT
  | Z_FT
  | D_FT
  | S_FT
  deriving (FrameType -> FrameType -> 𝔹
(FrameType -> FrameType -> 𝔹)
-> (FrameType -> FrameType -> 𝔹) -> Eq FrameType
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: FrameType -> FrameType -> 𝔹
== :: FrameType -> FrameType -> 𝔹
$c/= :: FrameType -> FrameType -> 𝔹
/= :: FrameType -> FrameType -> 𝔹
Eq,Eq FrameType
Eq FrameType =>
(FrameType -> FrameType -> Ordering)
-> (FrameType -> FrameType -> 𝔹)
-> (FrameType -> FrameType -> 𝔹)
-> (FrameType -> FrameType -> 𝔹)
-> (FrameType -> FrameType -> 𝔹)
-> (FrameType -> FrameType -> FrameType)
-> (FrameType -> FrameType -> FrameType)
-> Ord FrameType
FrameType -> FrameType -> 𝔹
FrameType -> FrameType -> Ordering
FrameType -> FrameType -> FrameType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameType -> FrameType -> Ordering
compare :: FrameType -> FrameType -> Ordering
$c< :: FrameType -> FrameType -> 𝔹
< :: FrameType -> FrameType -> 𝔹
$c<= :: FrameType -> FrameType -> 𝔹
<= :: FrameType -> FrameType -> 𝔹
$c> :: FrameType -> FrameType -> 𝔹
> :: FrameType -> FrameType -> 𝔹
$c>= :: FrameType -> FrameType -> 𝔹
>= :: FrameType -> FrameType -> 𝔹
$cmax :: FrameType -> FrameType -> FrameType
max :: FrameType -> FrameType -> FrameType
$cmin :: FrameType -> FrameType -> FrameType
min :: FrameType -> FrameType -> FrameType
Ord,Int -> FrameType -> ShowS
[FrameType] -> ShowS
FrameType -> String
(Int -> FrameType -> ShowS)
-> (FrameType -> String)
-> ([FrameType] -> ShowS)
-> Show FrameType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameType -> ShowS
showsPrec :: Int -> FrameType -> ShowS
$cshow :: FrameType -> String
show :: FrameType -> String
$cshowList :: [FrameType] -> ShowS
showList :: [FrameType] -> ShowS
Show)
makePrisms ''FrameType

frameTypeCode ∷ FrameType → 𝕊
frameTypeCode :: FrameType -> 𝕊
frameTypeCode = \case
  FrameType
B_FT → 𝕊
"bool"
  FrameType
N_FT → 𝕊
"nat"
  FrameType
Z_FT → 𝕊
"int"
  FrameType
D_FT → 𝕊
"dbl"
  FrameType
S_FT → 𝕊
"str"

data FrameVal = 
    B_FV 𝔹
  | N_FV ℕ64
  | Z_FV ℤ64
  | D_FV 𝔻
  | S_FV 𝕊
  deriving (FrameVal -> FrameVal -> 𝔹
(FrameVal -> FrameVal -> 𝔹)
-> (FrameVal -> FrameVal -> 𝔹) -> Eq FrameVal
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: FrameVal -> FrameVal -> 𝔹
== :: FrameVal -> FrameVal -> 𝔹
$c/= :: FrameVal -> FrameVal -> 𝔹
/= :: FrameVal -> FrameVal -> 𝔹
Eq,Eq FrameVal
Eq FrameVal =>
(FrameVal -> FrameVal -> Ordering)
-> (FrameVal -> FrameVal -> 𝔹)
-> (FrameVal -> FrameVal -> 𝔹)
-> (FrameVal -> FrameVal -> 𝔹)
-> (FrameVal -> FrameVal -> 𝔹)
-> (FrameVal -> FrameVal -> FrameVal)
-> (FrameVal -> FrameVal -> FrameVal)
-> Ord FrameVal
FrameVal -> FrameVal -> 𝔹
FrameVal -> FrameVal -> Ordering
FrameVal -> FrameVal -> FrameVal
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameVal -> FrameVal -> Ordering
compare :: FrameVal -> FrameVal -> Ordering
$c< :: FrameVal -> FrameVal -> 𝔹
< :: FrameVal -> FrameVal -> 𝔹
$c<= :: FrameVal -> FrameVal -> 𝔹
<= :: FrameVal -> FrameVal -> 𝔹
$c> :: FrameVal -> FrameVal -> 𝔹
> :: FrameVal -> FrameVal -> 𝔹
$c>= :: FrameVal -> FrameVal -> 𝔹
>= :: FrameVal -> FrameVal -> 𝔹
$cmax :: FrameVal -> FrameVal -> FrameVal
max :: FrameVal -> FrameVal -> FrameVal
$cmin :: FrameVal -> FrameVal -> FrameVal
min :: FrameVal -> FrameVal -> FrameVal
Ord,Int -> FrameVal -> ShowS
[FrameVal] -> ShowS
FrameVal -> String
(Int -> FrameVal -> ShowS)
-> (FrameVal -> String) -> ([FrameVal] -> ShowS) -> Show FrameVal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameVal -> ShowS
showsPrec :: Int -> FrameVal -> ShowS
$cshow :: FrameVal -> String
show :: FrameVal -> String
$cshowList :: [FrameVal] -> ShowS
showList :: [FrameVal] -> ShowS
Show)
makePrisms ''FrameVal
makePrettyUnion ''FrameVal

data FrameCol =
    B_FC (𝕌 𝔹)
  | N_FC (𝕌 ℕ64)
  | Z_FC (𝕌 ℤ64)
  | D_FC (𝕌 𝔻)
  | S_FC (𝕍 𝕊)
  deriving (FrameCol -> FrameCol -> 𝔹
(FrameCol -> FrameCol -> 𝔹)
-> (FrameCol -> FrameCol -> 𝔹) -> Eq FrameCol
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: FrameCol -> FrameCol -> 𝔹
== :: FrameCol -> FrameCol -> 𝔹
$c/= :: FrameCol -> FrameCol -> 𝔹
/= :: FrameCol -> FrameCol -> 𝔹
Eq,Eq FrameCol
Eq FrameCol =>
(FrameCol -> FrameCol -> Ordering)
-> (FrameCol -> FrameCol -> 𝔹)
-> (FrameCol -> FrameCol -> 𝔹)
-> (FrameCol -> FrameCol -> 𝔹)
-> (FrameCol -> FrameCol -> 𝔹)
-> (FrameCol -> FrameCol -> FrameCol)
-> (FrameCol -> FrameCol -> FrameCol)
-> Ord FrameCol
FrameCol -> FrameCol -> 𝔹
FrameCol -> FrameCol -> Ordering
FrameCol -> FrameCol -> FrameCol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameCol -> FrameCol -> Ordering
compare :: FrameCol -> FrameCol -> Ordering
$c< :: FrameCol -> FrameCol -> 𝔹
< :: FrameCol -> FrameCol -> 𝔹
$c<= :: FrameCol -> FrameCol -> 𝔹
<= :: FrameCol -> FrameCol -> 𝔹
$c> :: FrameCol -> FrameCol -> 𝔹
> :: FrameCol -> FrameCol -> 𝔹
$c>= :: FrameCol -> FrameCol -> 𝔹
>= :: FrameCol -> FrameCol -> 𝔹
$cmax :: FrameCol -> FrameCol -> FrameCol
max :: FrameCol -> FrameCol -> FrameCol
$cmin :: FrameCol -> FrameCol -> FrameCol
min :: FrameCol -> FrameCol -> FrameCol
Ord,Int -> FrameCol -> ShowS
[FrameCol] -> ShowS
FrameCol -> String
(Int -> FrameCol -> ShowS)
-> (FrameCol -> String) -> ([FrameCol] -> ShowS) -> Show FrameCol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameCol -> ShowS
showsPrec :: Int -> FrameCol -> ShowS
$cshow :: FrameCol -> String
show :: FrameCol -> String
$cshowList :: [FrameCol] -> ShowS
showList :: [FrameCol] -> ShowS
Show)
makePrisms ''FrameCol

frameColType ∷ FrameCol → FrameType
frameColType :: FrameCol -> FrameType
frameColType = \case
  B_FC 𝕌 𝔹
_ → FrameType
B_FT
  N_FC 𝕌 ℕ64
_ → FrameType
N_FT
  Z_FC 𝕌 ℤ64
_ → FrameType
Z_FT
  D_FC 𝕌 𝔻
_ → FrameType
D_FT
  S_FC 𝕍 𝕊
_ → FrameType
S_FT

frameColPack ∷ FrameType → 𝐼C FrameVal → 𝑂 FrameCol
frameColPack :: FrameType -> 𝐼C FrameVal -> 𝑂 FrameCol
frameColPack FrameType
t 𝐼C FrameVal
vs = case FrameType
t of
  FrameType
B_FT → (𝐼C 𝔹 -> FrameCol) -> 𝑂 (𝐼C 𝔹) -> 𝑂 FrameCol
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕌 𝔹 -> FrameCol
B_FC (𝕌 𝔹 -> FrameCol) -> (𝐼C 𝔹 -> 𝕌 𝔹) -> 𝐼C 𝔹 -> FrameCol
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼C 𝔹 -> 𝕌 𝔹
forall a t. (Storable a, ToIterC a t) => t -> 𝕌 a
uvecC) (𝑂 (𝐼C 𝔹) -> 𝑂 FrameCol) -> 𝑂 (𝐼C 𝔹) -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝑂 𝔹) -> 𝑂 (𝐼C 𝔹)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼C (𝑂 𝔹) -> 𝑂 (𝐼C 𝔹)) -> 𝐼C (𝑂 𝔹) -> 𝑂 (𝐼C 𝔹)
forall a b. (a -> b) -> a -> b
$ (FrameVal -> 𝑂 𝔹) -> 𝐼C FrameVal -> 𝐼C (𝑂 𝔹)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((FrameVal ⌲ 𝔹) -> FrameVal -> 𝑂 𝔹
forall a b. (a ⌲ b) -> a -> 𝑂 b
view FrameVal ⌲ 𝔹
b_FVL) 𝐼C FrameVal
vs
  FrameType
N_FT → (𝐼C ℕ64 -> FrameCol) -> 𝑂 (𝐼C ℕ64) -> 𝑂 FrameCol
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕌 ℕ64 -> FrameCol
N_FC (𝕌 ℕ64 -> FrameCol) -> (𝐼C ℕ64 -> 𝕌 ℕ64) -> 𝐼C ℕ64 -> FrameCol
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼C ℕ64 -> 𝕌 ℕ64
forall a t. (Storable a, ToIterC a t) => t -> 𝕌 a
uvecC) (𝑂 (𝐼C ℕ64) -> 𝑂 FrameCol) -> 𝑂 (𝐼C ℕ64) -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝑂 ℕ64) -> 𝑂 (𝐼C ℕ64)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼C (𝑂 ℕ64) -> 𝑂 (𝐼C ℕ64)) -> 𝐼C (𝑂 ℕ64) -> 𝑂 (𝐼C ℕ64)
forall a b. (a -> b) -> a -> b
$ (FrameVal -> 𝑂 ℕ64) -> 𝐼C FrameVal -> 𝐼C (𝑂 ℕ64)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((FrameVal ⌲ ℕ64) -> FrameVal -> 𝑂 ℕ64
forall a b. (a ⌲ b) -> a -> 𝑂 b
view FrameVal ⌲ ℕ64
n_FVL) 𝐼C FrameVal
vs
  FrameType
Z_FT → (𝐼C ℤ64 -> FrameCol) -> 𝑂 (𝐼C ℤ64) -> 𝑂 FrameCol
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕌 ℤ64 -> FrameCol
Z_FC (𝕌 ℤ64 -> FrameCol) -> (𝐼C ℤ64 -> 𝕌 ℤ64) -> 𝐼C ℤ64 -> FrameCol
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼C ℤ64 -> 𝕌 ℤ64
forall a t. (Storable a, ToIterC a t) => t -> 𝕌 a
uvecC) (𝑂 (𝐼C ℤ64) -> 𝑂 FrameCol) -> 𝑂 (𝐼C ℤ64) -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝑂 ℤ64) -> 𝑂 (𝐼C ℤ64)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼C (𝑂 ℤ64) -> 𝑂 (𝐼C ℤ64)) -> 𝐼C (𝑂 ℤ64) -> 𝑂 (𝐼C ℤ64)
forall a b. (a -> b) -> a -> b
$ (FrameVal -> 𝑂 ℤ64) -> 𝐼C FrameVal -> 𝐼C (𝑂 ℤ64)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((FrameVal ⌲ ℤ64) -> FrameVal -> 𝑂 ℤ64
forall a b. (a ⌲ b) -> a -> 𝑂 b
view FrameVal ⌲ ℤ64
z_FVL) 𝐼C FrameVal
vs
  FrameType
D_FT → (𝐼C 𝔻 -> FrameCol) -> 𝑂 (𝐼C 𝔻) -> 𝑂 FrameCol
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕌 𝔻 -> FrameCol
D_FC (𝕌 𝔻 -> FrameCol) -> (𝐼C 𝔻 -> 𝕌 𝔻) -> 𝐼C 𝔻 -> FrameCol
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼C 𝔻 -> 𝕌 𝔻
forall a t. (Storable a, ToIterC a t) => t -> 𝕌 a
uvecC) (𝑂 (𝐼C 𝔻) -> 𝑂 FrameCol) -> 𝑂 (𝐼C 𝔻) -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝑂 𝔻) -> 𝑂 (𝐼C 𝔻)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼C (𝑂 𝔻) -> 𝑂 (𝐼C 𝔻)) -> 𝐼C (𝑂 𝔻) -> 𝑂 (𝐼C 𝔻)
forall a b. (a -> b) -> a -> b
$ (FrameVal -> 𝑂 𝔻) -> 𝐼C FrameVal -> 𝐼C (𝑂 𝔻)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((FrameVal ⌲ 𝔻) -> FrameVal -> 𝑂 𝔻
forall a b. (a ⌲ b) -> a -> 𝑂 b
view FrameVal ⌲ 𝔻
d_FVL) 𝐼C FrameVal
vs
  FrameType
S_FT → (𝐼C 𝕊 -> FrameCol) -> 𝑂 (𝐼C 𝕊) -> 𝑂 FrameCol
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕍 𝕊 -> FrameCol
S_FC (𝕍 𝕊 -> FrameCol) -> (𝐼C 𝕊 -> 𝕍 𝕊) -> 𝐼C 𝕊 -> FrameCol
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼C 𝕊 -> 𝕍 𝕊
forall a t. ToIterC a t => t -> 𝕍 a
vecC) (𝑂 (𝐼C 𝕊) -> 𝑂 FrameCol) -> 𝑂 (𝐼C 𝕊) -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝑂 𝕊) -> 𝑂 (𝐼C 𝕊)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼C (𝑂 𝕊) -> 𝑂 (𝐼C 𝕊)) -> 𝐼C (𝑂 𝕊) -> 𝑂 (𝐼C 𝕊)
forall a b. (a -> b) -> a -> b
$ (FrameVal -> 𝑂 𝕊) -> 𝐼C FrameVal -> 𝐼C (𝑂 𝕊)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((FrameVal ⌲ 𝕊) -> FrameVal -> 𝑂 𝕊
forall a b. (a ⌲ b) -> a -> 𝑂 b
view FrameVal ⌲ 𝕊
s_FVL) 𝐼C FrameVal
vs

frameColUnpack ∷ FrameCol → 𝐼C FrameVal
frameColUnpack :: FrameCol -> 𝐼C FrameVal
frameColUnpack = \case
  B_FC 𝕌 𝔹
vs → 𝔹 -> FrameVal
B_FV (𝔹 -> FrameVal) -> 𝐼C 𝔹 -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 𝔹 -> 𝐼C 𝔹
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕌 𝔹
vs
  N_FC 𝕌 ℕ64
vs → ℕ64 -> FrameVal
N_FV (ℕ64 -> FrameVal) -> 𝐼C ℕ64 -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 ℕ64 -> 𝐼C ℕ64
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕌 ℕ64
vs
  Z_FC 𝕌 ℤ64
vs → ℤ64 -> FrameVal
Z_FV (ℤ64 -> FrameVal) -> 𝐼C ℤ64 -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 ℤ64 -> 𝐼C ℤ64
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕌 ℤ64
vs
  D_FC 𝕌 𝔻
vs → 𝔻 -> FrameVal
D_FV (𝔻 -> FrameVal) -> 𝐼C 𝔻 -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 𝔻 -> 𝐼C 𝔻
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕌 𝔻
vs
  S_FC 𝕍 𝕊
vs → 𝕊 -> FrameVal
S_FV (𝕊 -> FrameVal) -> 𝐼C 𝕊 -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕍 𝕊 -> 𝐼C 𝕊
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕍 𝕊
vs

frameColIndex ∷ ℕ64 → FrameCol → 𝑂 FrameVal
frameColIndex :: ℕ64 -> FrameCol -> 𝑂 FrameVal
frameColIndex ℕ64
n = \case
  B_FC 𝕌 𝔹
vs → 𝔹 -> FrameVal
B_FV (𝔹 -> FrameVal) -> 𝑂 𝔹 -> 𝑂 FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 𝔹
vs 𝕌 𝔹 -> ℕ64 -> 𝑂 𝔹
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
n
  N_FC 𝕌 ℕ64
vs → ℕ64 -> FrameVal
N_FV (ℕ64 -> FrameVal) -> 𝑂 ℕ64 -> 𝑂 FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 ℕ64
vs 𝕌 ℕ64 -> ℕ64 -> 𝑂 ℕ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
n
  Z_FC 𝕌 ℤ64
vs → ℤ64 -> FrameVal
Z_FV (ℤ64 -> FrameVal) -> 𝑂 ℤ64 -> 𝑂 FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 ℤ64
vs 𝕌 ℤ64 -> ℕ64 -> 𝑂 ℤ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
n
  D_FC 𝕌 𝔻
vs → 𝔻 -> FrameVal
D_FV (𝔻 -> FrameVal) -> 𝑂 𝔻 -> 𝑂 FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕌 𝔻
vs 𝕌 𝔻 -> ℕ64 -> 𝑂 𝔻
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
n
  S_FC 𝕍 𝕊
vs → 𝕊 -> FrameVal
S_FV (𝕊 -> FrameVal) -> 𝑂 𝕊 -> 𝑂 FrameVal
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕍 𝕊
vs 𝕍 𝕊 -> ℕ64 -> 𝑂 𝕊
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
n

data FrameGrouping v =
    B_FG (𝔹 ⇰ v)
  | N_FG (ℕ64 ⇰ v)
  | Z_FG (ℤ64 ⇰ v)
  | D_FG (𝔻 ⇰ v)
  | S_FG (𝕊 ⇰ v)
  deriving (FrameGrouping v -> FrameGrouping v -> 𝔹
(FrameGrouping v -> FrameGrouping v -> 𝔹)
-> (FrameGrouping v -> FrameGrouping v -> 𝔹)
-> Eq (FrameGrouping v)
forall v. Eq v => FrameGrouping v -> FrameGrouping v -> 𝔹
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: forall v. Eq v => FrameGrouping v -> FrameGrouping v -> 𝔹
== :: FrameGrouping v -> FrameGrouping v -> 𝔹
$c/= :: forall v. Eq v => FrameGrouping v -> FrameGrouping v -> 𝔹
/= :: FrameGrouping v -> FrameGrouping v -> 𝔹
Eq,Eq (FrameGrouping v)
Eq (FrameGrouping v) =>
(FrameGrouping v -> FrameGrouping v -> Ordering)
-> (FrameGrouping v -> FrameGrouping v -> 𝔹)
-> (FrameGrouping v -> FrameGrouping v -> 𝔹)
-> (FrameGrouping v -> FrameGrouping v -> 𝔹)
-> (FrameGrouping v -> FrameGrouping v -> 𝔹)
-> (FrameGrouping v -> FrameGrouping v -> FrameGrouping v)
-> (FrameGrouping v -> FrameGrouping v -> FrameGrouping v)
-> Ord (FrameGrouping v)
FrameGrouping v -> FrameGrouping v -> 𝔹
FrameGrouping v -> FrameGrouping v -> Ordering
FrameGrouping v -> FrameGrouping v -> FrameGrouping v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (FrameGrouping v)
forall v. Ord v => FrameGrouping v -> FrameGrouping v -> 𝔹
forall v. Ord v => FrameGrouping v -> FrameGrouping v -> Ordering
forall v.
Ord v =>
FrameGrouping v -> FrameGrouping v -> FrameGrouping v
$ccompare :: forall v. Ord v => FrameGrouping v -> FrameGrouping v -> Ordering
compare :: FrameGrouping v -> FrameGrouping v -> Ordering
$c< :: forall v. Ord v => FrameGrouping v -> FrameGrouping v -> 𝔹
< :: FrameGrouping v -> FrameGrouping v -> 𝔹
$c<= :: forall v. Ord v => FrameGrouping v -> FrameGrouping v -> 𝔹
<= :: FrameGrouping v -> FrameGrouping v -> 𝔹
$c> :: forall v. Ord v => FrameGrouping v -> FrameGrouping v -> 𝔹
> :: FrameGrouping v -> FrameGrouping v -> 𝔹
$c>= :: forall v. Ord v => FrameGrouping v -> FrameGrouping v -> 𝔹
>= :: FrameGrouping v -> FrameGrouping v -> 𝔹
$cmax :: forall v.
Ord v =>
FrameGrouping v -> FrameGrouping v -> FrameGrouping v
max :: FrameGrouping v -> FrameGrouping v -> FrameGrouping v
$cmin :: forall v.
Ord v =>
FrameGrouping v -> FrameGrouping v -> FrameGrouping v
min :: FrameGrouping v -> FrameGrouping v -> FrameGrouping v
Ord,Int -> FrameGrouping v -> ShowS
[FrameGrouping v] -> ShowS
FrameGrouping v -> String
(Int -> FrameGrouping v -> ShowS)
-> (FrameGrouping v -> String)
-> ([FrameGrouping v] -> ShowS)
-> Show (FrameGrouping v)
forall v. Show v => Int -> FrameGrouping v -> ShowS
forall v. Show v => [FrameGrouping v] -> ShowS
forall v. Show v => FrameGrouping v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> FrameGrouping v -> ShowS
showsPrec :: Int -> FrameGrouping v -> ShowS
$cshow :: forall v. Show v => FrameGrouping v -> String
show :: FrameGrouping v -> String
$cshowList :: forall v. Show v => [FrameGrouping v] -> ShowS
showList :: [FrameGrouping v] -> ShowS
Show)
makePrettyUnion ''FrameGrouping

instance Functor FrameGrouping where
  map :: forall a b. (a -> b) -> FrameGrouping a -> FrameGrouping b
map a -> b
f = \case
   B_FG 𝔹 ⇰ a
kvs → (𝔹 ⇰ b) -> FrameGrouping b
forall v. (𝔹 ⇰ v) -> FrameGrouping v
B_FG ((𝔹 ⇰ b) -> FrameGrouping b) -> (𝔹 ⇰ b) -> FrameGrouping b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (𝔹 ⇰ a) -> 𝔹 ⇰ b
forall a b. (a -> b) -> (𝔹 ⇰ a) -> 𝔹 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f 𝔹 ⇰ a
kvs
   N_FG ℕ64 ⇰ a
kvs → (ℕ64 ⇰ b) -> FrameGrouping b
forall v. (ℕ64 ⇰ v) -> FrameGrouping v
N_FG ((ℕ64 ⇰ b) -> FrameGrouping b) -> (ℕ64 ⇰ b) -> FrameGrouping b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (ℕ64 ⇰ a) -> ℕ64 ⇰ b
forall a b. (a -> b) -> (ℕ64 ⇰ a) -> ℕ64 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f ℕ64 ⇰ a
kvs
   Z_FG ℤ64 ⇰ a
kvs → (ℤ64 ⇰ b) -> FrameGrouping b
forall v. (ℤ64 ⇰ v) -> FrameGrouping v
Z_FG ((ℤ64 ⇰ b) -> FrameGrouping b) -> (ℤ64 ⇰ b) -> FrameGrouping b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (ℤ64 ⇰ a) -> ℤ64 ⇰ b
forall a b. (a -> b) -> (ℤ64 ⇰ a) -> ℤ64 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f ℤ64 ⇰ a
kvs
   D_FG 𝔻 ⇰ a
kvs → (𝔻 ⇰ b) -> FrameGrouping b
forall v. (𝔻 ⇰ v) -> FrameGrouping v
D_FG ((𝔻 ⇰ b) -> FrameGrouping b) -> (𝔻 ⇰ b) -> FrameGrouping b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (𝔻 ⇰ a) -> 𝔻 ⇰ b
forall a b. (a -> b) -> (𝔻 ⇰ a) -> 𝔻 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f 𝔻 ⇰ a
kvs
   S_FG 𝕊 ⇰ a
kvs → (𝕊 ⇰ b) -> FrameGrouping b
forall v. (𝕊 ⇰ v) -> FrameGrouping v
S_FG ((𝕊 ⇰ b) -> FrameGrouping b) -> (𝕊 ⇰ b) -> FrameGrouping b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (𝕊 ⇰ a) -> 𝕊 ⇰ b
forall a b. (a -> b) -> (𝕊 ⇰ a) -> 𝕊 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f 𝕊 ⇰ a
kvs

instance FunctorM FrameGrouping where
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FrameGrouping a -> m (FrameGrouping b)
mapM a -> m b
f = \case
   B_FG 𝔹 ⇰ a
kvs → (𝔹 ⇰ b) -> FrameGrouping b
forall v. (𝔹 ⇰ v) -> FrameGrouping v
B_FG ((𝔹 ⇰ b) -> FrameGrouping b) -> m (𝔹 ⇰ b) -> m (FrameGrouping b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> (𝔹 ⇰ a) -> m (𝔹 ⇰ b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (𝔹 ⇰ a) -> m (𝔹 ⇰ b)
mapM a -> m b
f 𝔹 ⇰ a
kvs
   N_FG ℕ64 ⇰ a
kvs → (ℕ64 ⇰ b) -> FrameGrouping b
forall v. (ℕ64 ⇰ v) -> FrameGrouping v
N_FG ((ℕ64 ⇰ b) -> FrameGrouping b)
-> m (ℕ64 ⇰ b) -> m (FrameGrouping b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> (ℕ64 ⇰ a) -> m (ℕ64 ⇰ b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (ℕ64 ⇰ a) -> m (ℕ64 ⇰ b)
mapM a -> m b
f ℕ64 ⇰ a
kvs
   Z_FG ℤ64 ⇰ a
kvs → (ℤ64 ⇰ b) -> FrameGrouping b
forall v. (ℤ64 ⇰ v) -> FrameGrouping v
Z_FG ((ℤ64 ⇰ b) -> FrameGrouping b)
-> m (ℤ64 ⇰ b) -> m (FrameGrouping b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> (ℤ64 ⇰ a) -> m (ℤ64 ⇰ b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (ℤ64 ⇰ a) -> m (ℤ64 ⇰ b)
mapM a -> m b
f ℤ64 ⇰ a
kvs
   D_FG 𝔻 ⇰ a
kvs → (𝔻 ⇰ b) -> FrameGrouping b
forall v. (𝔻 ⇰ v) -> FrameGrouping v
D_FG ((𝔻 ⇰ b) -> FrameGrouping b) -> m (𝔻 ⇰ b) -> m (FrameGrouping b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> (𝔻 ⇰ a) -> m (𝔻 ⇰ b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (𝔻 ⇰ a) -> m (𝔻 ⇰ b)
mapM a -> m b
f 𝔻 ⇰ a
kvs
   S_FG 𝕊 ⇰ a
kvs → (𝕊 ⇰ b) -> FrameGrouping b
forall v. (𝕊 ⇰ v) -> FrameGrouping v
S_FG ((𝕊 ⇰ b) -> FrameGrouping b) -> m (𝕊 ⇰ b) -> m (FrameGrouping b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> (𝕊 ⇰ a) -> m (𝕊 ⇰ b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (𝕊 ⇰ a) -> m (𝕊 ⇰ b)
mapM a -> m b
f 𝕊 ⇰ a
kvs

frameGroupingInterWithM
  ∷ (Monad m,MonadFail m) 
  ⇒ (v₁ → v₂ → m v₃) 
  → FrameGrouping v₁ 
  → FrameGrouping v₂ 
  → m (FrameGrouping v₃)
frameGroupingInterWithM :: forall (m :: * -> *) v₁ v₂ v₃.
(Monad m, MonadFail m) =>
(v₁ -> v₂ -> m v₃)
-> FrameGrouping v₁ -> FrameGrouping v₂ -> m (FrameGrouping v₃)
frameGroupingInterWithM v₁ -> v₂ -> m v₃
f FrameGrouping v₁
vs₁ FrameGrouping v₂
vs₂ = case (FrameGrouping v₁
vs₁,FrameGrouping v₂
vs₂) of
  (B_FG 𝔹 ⇰ v₁
kvs₁,B_FG 𝔹 ⇰ v₂
kvs₂) → (𝔹 ⇰ v₃) -> FrameGrouping v₃
forall v. (𝔹 ⇰ v) -> FrameGrouping v
B_FG ((𝔹 ⇰ v₃) -> FrameGrouping v₃)
-> m (𝔹 ⇰ v₃) -> m (FrameGrouping v₃)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (v₁ -> v₂ -> m v₃) -> (𝔹 ⇰ v₁) -> (𝔹 ⇰ v₂) -> m (𝔹 ⇰ v₃)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM v₁ -> v₂ -> m v₃
f 𝔹 ⇰ v₁
kvs₁ 𝔹 ⇰ v₂
kvs₂
  (N_FG ℕ64 ⇰ v₁
kvs₁,N_FG ℕ64 ⇰ v₂
kvs₂) → (ℕ64 ⇰ v₃) -> FrameGrouping v₃
forall v. (ℕ64 ⇰ v) -> FrameGrouping v
N_FG ((ℕ64 ⇰ v₃) -> FrameGrouping v₃)
-> m (ℕ64 ⇰ v₃) -> m (FrameGrouping v₃)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (v₁ -> v₂ -> m v₃) -> (ℕ64 ⇰ v₁) -> (ℕ64 ⇰ v₂) -> m (ℕ64 ⇰ v₃)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM v₁ -> v₂ -> m v₃
f ℕ64 ⇰ v₁
kvs₁ ℕ64 ⇰ v₂
kvs₂
  (Z_FG ℤ64 ⇰ v₁
kvs₁,Z_FG ℤ64 ⇰ v₂
kvs₂) → (ℤ64 ⇰ v₃) -> FrameGrouping v₃
forall v. (ℤ64 ⇰ v) -> FrameGrouping v
Z_FG ((ℤ64 ⇰ v₃) -> FrameGrouping v₃)
-> m (ℤ64 ⇰ v₃) -> m (FrameGrouping v₃)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (v₁ -> v₂ -> m v₃) -> (ℤ64 ⇰ v₁) -> (ℤ64 ⇰ v₂) -> m (ℤ64 ⇰ v₃)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM v₁ -> v₂ -> m v₃
f ℤ64 ⇰ v₁
kvs₁ ℤ64 ⇰ v₂
kvs₂
  (D_FG 𝔻 ⇰ v₁
kvs₁,D_FG 𝔻 ⇰ v₂
kvs₂) → (𝔻 ⇰ v₃) -> FrameGrouping v₃
forall v. (𝔻 ⇰ v) -> FrameGrouping v
D_FG ((𝔻 ⇰ v₃) -> FrameGrouping v₃)
-> m (𝔻 ⇰ v₃) -> m (FrameGrouping v₃)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (v₁ -> v₂ -> m v₃) -> (𝔻 ⇰ v₁) -> (𝔻 ⇰ v₂) -> m (𝔻 ⇰ v₃)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM v₁ -> v₂ -> m v₃
f 𝔻 ⇰ v₁
kvs₁ 𝔻 ⇰ v₂
kvs₂
  (S_FG 𝕊 ⇰ v₁
kvs₁,S_FG 𝕊 ⇰ v₂
kvs₂) → (𝕊 ⇰ v₃) -> FrameGrouping v₃
forall v. (𝕊 ⇰ v) -> FrameGrouping v
S_FG ((𝕊 ⇰ v₃) -> FrameGrouping v₃)
-> m (𝕊 ⇰ v₃) -> m (FrameGrouping v₃)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (v₁ -> v₂ -> m v₃) -> (𝕊 ⇰ v₁) -> (𝕊 ⇰ v₂) -> m (𝕊 ⇰ v₃)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM v₁ -> v₂ -> m v₃
f 𝕊 ⇰ v₁
kvs₁ 𝕊 ⇰ v₂
kvs₂
  (FrameGrouping v₁, FrameGrouping v₂)
_ → m (FrameGrouping v₃)
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort

data FrameData =
    Vec_FD ℕ64 (𝕊 ⇰ FrameCol)
  | Grp_FD 𝕊 (FrameGrouping FrameData)
  deriving (FrameData -> FrameData -> 𝔹
(FrameData -> FrameData -> 𝔹)
-> (FrameData -> FrameData -> 𝔹) -> Eq FrameData
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: FrameData -> FrameData -> 𝔹
== :: FrameData -> FrameData -> 𝔹
$c/= :: FrameData -> FrameData -> 𝔹
/= :: FrameData -> FrameData -> 𝔹
Eq,Eq FrameData
Eq FrameData =>
(FrameData -> FrameData -> Ordering)
-> (FrameData -> FrameData -> 𝔹)
-> (FrameData -> FrameData -> 𝔹)
-> (FrameData -> FrameData -> 𝔹)
-> (FrameData -> FrameData -> 𝔹)
-> (FrameData -> FrameData -> FrameData)
-> (FrameData -> FrameData -> FrameData)
-> Ord FrameData
FrameData -> FrameData -> 𝔹
FrameData -> FrameData -> Ordering
FrameData -> FrameData -> FrameData
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameData -> FrameData -> Ordering
compare :: FrameData -> FrameData -> Ordering
$c< :: FrameData -> FrameData -> 𝔹
< :: FrameData -> FrameData -> 𝔹
$c<= :: FrameData -> FrameData -> 𝔹
<= :: FrameData -> FrameData -> 𝔹
$c> :: FrameData -> FrameData -> 𝔹
> :: FrameData -> FrameData -> 𝔹
$c>= :: FrameData -> FrameData -> 𝔹
>= :: FrameData -> FrameData -> 𝔹
$cmax :: FrameData -> FrameData -> FrameData
max :: FrameData -> FrameData -> FrameData
$cmin :: FrameData -> FrameData -> FrameData
min :: FrameData -> FrameData -> FrameData
Ord,Int -> FrameData -> ShowS
[FrameData] -> ShowS
FrameData -> String
(Int -> FrameData -> ShowS)
-> (FrameData -> String)
-> ([FrameData] -> ShowS)
-> Show FrameData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameData -> ShowS
showsPrec :: Int -> FrameData -> ShowS
$cshow :: FrameData -> String
show :: FrameData -> String
$cshowList :: [FrameData] -> ShowS
showList :: [FrameData] -> ShowS
Show)

data Frame = Frame
  { Frame -> 𝑃 𝕊
frameColP ∷ 𝑃 𝕊
  , Frame -> 𝕍 𝕊
frameColV ∷ 𝕍 𝕊
  , Frame -> 𝕊 ⇰ FrameType
frameColT ∷ 𝕊 ⇰ FrameType
  , Frame -> 𝕊 ⇰ FrameType
frameGrpT ∷ 𝕊 ⇰ FrameType
  , Frame -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
frameData ∷ (𝕊 ⇰ FrameVal) ⇰ ℕ64 ∧ (𝕊 ⇰ FrameCol)
  } deriving (Frame -> Frame -> 𝔹
(Frame -> Frame -> 𝔹) -> (Frame -> Frame -> 𝔹) -> Eq Frame
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: Frame -> Frame -> 𝔹
== :: Frame -> Frame -> 𝔹
$c/= :: Frame -> Frame -> 𝔹
/= :: Frame -> Frame -> 𝔹
Eq,Eq Frame
Eq Frame =>
(Frame -> Frame -> Ordering)
-> (Frame -> Frame -> 𝔹)
-> (Frame -> Frame -> 𝔹)
-> (Frame -> Frame -> 𝔹)
-> (Frame -> Frame -> 𝔹)
-> (Frame -> Frame -> Frame)
-> (Frame -> Frame -> Frame)
-> Ord Frame
Frame -> Frame -> 𝔹
Frame -> Frame -> Ordering
Frame -> Frame -> Frame
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Frame -> Frame -> Ordering
compare :: Frame -> Frame -> Ordering
$c< :: Frame -> Frame -> 𝔹
< :: Frame -> Frame -> 𝔹
$c<= :: Frame -> Frame -> 𝔹
<= :: Frame -> Frame -> 𝔹
$c> :: Frame -> Frame -> 𝔹
> :: Frame -> Frame -> 𝔹
$c>= :: Frame -> Frame -> 𝔹
>= :: Frame -> Frame -> 𝔹
$cmax :: Frame -> Frame -> Frame
max :: Frame -> Frame -> Frame
$cmin :: Frame -> Frame -> Frame
min :: Frame -> Frame -> Frame
Ord,Int -> Frame -> ShowS
[Frame] -> ShowS
Frame -> String
(Int -> Frame -> ShowS)
-> (Frame -> String) -> ([Frame] -> ShowS) -> Show Frame
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Frame -> ShowS
showsPrec :: Int -> Frame -> ShowS
$cshow :: Frame -> String
show :: Frame -> String
$cshowList :: [Frame] -> ShowS
showList :: [Frame] -> ShowS
Show)

frameProduct ∷ Frame → Frame → 𝑂 Frame
frameProduct :: Frame -> Frame -> 𝑂 Frame
frameProduct Frame
fr₁ Frame
fr₂ = do
  let Frame 𝑃 𝕊
colp₁ 𝕍 𝕊
colv₁ 𝕊 ⇰ FrameType
colt₁ 𝕊 ⇰ FrameType
grpt₁ (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data₁ = Frame
fr₁
      Frame 𝑃 𝕊
colp₂ 𝕍 𝕊
colv₂ 𝕊 ⇰ FrameType
colt₂ 𝕊 ⇰ FrameType
grpt₂ (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data₂ = Frame
fr₂
      colp₁' ∷ 𝑃 𝕊
      colp₁' :: 𝑃 𝕊
colp₁' = 𝐼 𝕊 -> 𝑃 𝕊
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 𝕊 -> 𝑃 𝕊) -> 𝐼 𝕊 -> 𝑃 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐼 𝕊 -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 𝕊
colp₁) ((𝕊 -> 𝕊) -> 𝐼 𝕊) -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_L"
      colp₂' ∷ 𝑃 𝕊
      colp₂' :: 𝑃 𝕊
colp₂' = 𝐼 𝕊 -> 𝑃 𝕊
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 𝕊 -> 𝑃 𝕊) -> 𝐼 𝕊 -> 𝑃 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐼 𝕊 -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 𝕊
colp₂) ((𝕊 -> 𝕊) -> 𝐼 𝕊) -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_R"
      colv₁' ∷ 𝕍 𝕊
      colv₁' :: 𝕍 𝕊
colv₁' = 𝕍 𝕊 -> (𝕊 -> 𝕊) -> 𝕍 𝕊
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 𝕊
colv₁ ((𝕊 -> 𝕊) -> 𝕍 𝕊) -> (𝕊 -> 𝕊) -> 𝕍 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_L"
      colv₂' ∷ 𝕍 𝕊
      colv₂' :: 𝕍 𝕊
colv₂' = 𝕍 𝕊 -> (𝕊 -> 𝕊) -> 𝕍 𝕊
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 𝕊
colv₂ ((𝕊 -> 𝕊) -> 𝕍 𝕊) -> (𝕊 -> 𝕊) -> 𝕍 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_R"
      colt₁' ∷ 𝕊 ⇰ FrameType
      colt₁' :: 𝕊 ⇰ FrameType
colt₁' = 𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType)
-> 𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ FrameType)
-> ((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ FrameType
colt₁) (((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType))
-> ((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType)
-> (𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_L"
      colt₂' ∷ 𝕊 ⇰ FrameType
      colt₂' :: 𝕊 ⇰ FrameType
colt₂' = 𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType)
-> 𝐼 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ FrameType)
-> ((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ FrameType
colt₂) (((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType))
-> ((𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType) -> 𝐼 (𝕊 ∧ FrameType)
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType)
-> (𝕊 -> 𝕊) -> (𝕊 ∧ FrameType) -> 𝕊 ∧ FrameType
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_R"
      colp'  ∷ 𝑃 𝕊
      colp' :: 𝑃 𝕊
colp'  = 𝑃 𝕊
colp₁' 𝑃 𝕊 -> 𝑃 𝕊 -> 𝑃 𝕊
forall e s. Set e s => s -> s -> s
∪ 𝑃 𝕊
colp₂'
      colv'  ∷ 𝕍 𝕊
      colv' :: 𝕍 𝕊
colv'  = 𝕍 𝕊
colv₁' 𝕍 𝕊 -> 𝕍 𝕊 -> 𝕍 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕍 𝕊
colv₂'
      colt'  ∷ 𝕊 ⇰ FrameType
      colt' :: 𝕊 ⇰ FrameType
colt'  = 𝕊 ⇰ FrameType
colt₁' (𝕊 ⇰ FrameType) -> (𝕊 ⇰ FrameType) -> 𝕊 ⇰ FrameType
forall a. (𝕊 ⇰ a) -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
⩌ 𝕊 ⇰ FrameType
colt₂'
  𝕊 ⇰ FrameType
grpt' ∷ 𝕊 ⇰ FrameType
        ← (FrameType -> FrameType -> 𝑂 FrameType)
-> (𝕊 ⇰ FrameType) -> (𝕊 ⇰ FrameType) -> 𝑂 (𝕊 ⇰ FrameType)
forall (m :: * -> *) k s (d :: * -> *) a b c.
(Monad m, Dict k s d) =>
(a -> b -> m c) -> d a -> d b -> m (d c)
dinterByM (\ FrameType
τ₁ FrameType
τ₂ → do 𝔹 -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard (𝔹 -> 𝑂 ()) -> 𝔹 -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ FrameType
τ₁ FrameType -> FrameType -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ FrameType
τ₂ ; FrameType -> 𝑂 FrameType
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return FrameType
τ₁) 𝕊 ⇰ FrameType
grpt₁ 𝕊 ⇰ FrameType
grpt₂
  let data' :: (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data' = ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol))
    -> (ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall k s (d :: * -> *) a b c.
Dict k s d =>
d a -> d b -> (a -> b -> c) -> d c
dinterByOn (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data₁ (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data₂ (((ℕ64 ∧ (𝕊 ⇰ FrameCol))
  -> (ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
 -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol))
    -> (ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a b. (a -> b) -> a -> b
$ \ (ℕ64
n₁ :* 𝕊 ⇰ FrameCol
svss₁) (ℕ64
n₂ :* 𝕊 ⇰ FrameCol
svss₂) → 
        let svss₁'₁ ∷ 𝕊 ⇰ FrameCol
            svss₁'₁ :: 𝕊 ⇰ FrameCol
svss₁'₁ = 𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol)
-> 𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ FrameCol)
-> ((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ FrameCol
svss₁) (((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol))
-> ((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol)
-> (𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_L"
            svss₂'₁ ∷ 𝕊 ⇰ FrameCol

            svss₂'₁ :: 𝕊 ⇰ FrameCol
svss₂'₁ = 𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol)
-> 𝐼 (𝕊 ∧ FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ FrameCol)
-> ((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ FrameCol
svss₂) (((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol))
-> ((𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol) -> 𝐼 (𝕊 ∧ FrameCol)
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol)
-> (𝕊 -> 𝕊) -> (𝕊 ∧ FrameCol) -> 𝕊 ∧ FrameCol
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝕊 -> 𝕊) -> 𝕊 -> 𝕊 -> 𝕊
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
(⧺) 𝕊
"_R"
            svss₁'₂ ∷ 𝐼C (𝕊 ⇰ FrameVal)
            svss₁'₂ :: 𝐼C (𝕊 ⇰ FrameVal)
svss₁'₂ = 𝐼C ℕ64 -> (ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (ℕ64 -> 𝐼C ℕ64
uptoC ℕ64
n₁) ((ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal))
-> (ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a b. (a -> b) -> a -> b
$ \ ℕ64
n → (𝕊 ⇰ FrameCol) -> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕊 ⇰ FrameCol
svss₁'₁ ((FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal)
-> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall a b. (a -> b) -> a -> b
$ (𝑂 FrameVal ⌲ FrameVal) -> 𝑂 FrameVal -> FrameVal
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameVal ⌲ FrameVal
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameVal -> FrameVal)
-> (FrameCol -> 𝑂 FrameVal) -> FrameCol -> FrameVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> FrameCol -> 𝑂 FrameVal
frameColIndex ℕ64
n
            svss₂'₂ ∷ 𝐼C (𝕊 ⇰ FrameVal)
            svss₂'₂ :: 𝐼C (𝕊 ⇰ FrameVal)
svss₂'₂ = 𝐼C ℕ64 -> (ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (ℕ64 -> 𝐼C ℕ64
uptoC ℕ64
n₂) ((ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal))
-> (ℕ64 -> 𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a b. (a -> b) -> a -> b
$ \ ℕ64
n → (𝕊 ⇰ FrameCol) -> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕊 ⇰ FrameCol
svss₂'₁ ((FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal)
-> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall a b. (a -> b) -> a -> b
$ (𝑂 FrameVal ⌲ FrameVal) -> 𝑂 FrameVal -> FrameVal
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameVal ⌲ FrameVal
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameVal -> FrameVal)
-> (FrameCol -> 𝑂 FrameVal) -> FrameCol -> FrameVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> FrameCol -> 𝑂 FrameVal
frameColIndex ℕ64
n
            svss'₁ ∷ 𝕍 (𝕊 ⇰ FrameVal)
            svss'₁ :: 𝕍 (𝕊 ⇰ FrameVal)
svss'₁ = 𝐼C (𝕊 ⇰ FrameVal) -> 𝕍 (𝕊 ⇰ FrameVal)
forall a t. ToIterC a t => t -> 𝕍 a
vecC (𝐼C (𝕊 ⇰ FrameVal) -> 𝕍 (𝕊 ⇰ FrameVal))
-> 𝐼C (𝕊 ⇰ FrameVal) -> 𝕍 (𝕊 ⇰ FrameVal)
forall a b. (a -> b) -> a -> b
$ ((𝕊 ⇰ FrameVal) -> (𝕊 ⇰ FrameVal) -> 𝕊 ⇰ FrameVal)
-> 𝐼C (𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a b c. (a -> b -> c) -> 𝐼C a -> 𝐼C b -> 𝐼C c
prodWith𝐼C (𝕊 ⇰ FrameVal) -> (𝕊 ⇰ FrameVal) -> 𝕊 ⇰ FrameVal
forall a. (𝕊 ⇰ a) -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
(⩌) 𝐼C (𝕊 ⇰ FrameVal)
svss₁'₂ 𝐼C (𝕊 ⇰ FrameVal)
svss₂'₂
            svss'₂ ∷ 𝕊 ⇰ FrameCol

            rows :: ℕ64
rows = 𝕍 (𝕊 ⇰ FrameVal) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (𝕊 ⇰ FrameVal)
svss'₁

            svss'₂ :: 𝕊 ⇰ FrameCol
svss'₂ = (𝕊 ⇰ FrameType) -> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn 𝕊 ⇰ FrameType
colt' ((𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol)
-> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ \ 𝕊
s FrameType
τ → 
              (𝑂 FrameCol ⌲ FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameCol ⌲ FrameCol
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameCol -> FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝐼C FrameVal -> 𝑂 FrameCol
frameColPack FrameType
τ (𝐼C FrameVal -> 𝑂 FrameCol) -> 𝐼C FrameVal -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝕊 ⇰ FrameVal) -> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝕍 (𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕍 (𝕊 ⇰ FrameVal)
svss'₁) (((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal)
-> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊 -> (𝕊 ⇰ FrameVal) -> FrameVal
forall k v t. Lookup k v t => k -> t -> v
lupΩ 𝕊
s
        in ℕ64
rows ℕ64 -> (𝕊 ⇰ FrameCol) -> ℕ64 ∧ (𝕊 ⇰ FrameCol)
forall a b. a -> b -> a ∧ b
:* 𝕊 ⇰ FrameCol
svss'₂
  Frame -> 𝑂 Frame
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return (Frame -> 𝑂 Frame) -> Frame -> 𝑂 Frame
forall a b. (a -> b) -> a -> b
$ 𝑃 𝕊
-> 𝕍 𝕊
-> (𝕊 ⇰ FrameType)
-> (𝕊 ⇰ FrameType)
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> Frame
Frame 𝑃 𝕊
colp' 𝕍 𝕊
colv' 𝕊 ⇰ FrameType
colt' 𝕊 ⇰ FrameType
grpt' (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data'

frameGroup ∷ 𝕊 → 𝕊 → Frame → 𝑂 Frame
frameGroup :: 𝕊 -> 𝕊 -> Frame -> 𝑂 Frame
frameGroup 𝕊
col 𝕊
s₀ (Frame 𝑃 𝕊
colp 𝕍 𝕊
colv 𝕊 ⇰ FrameType
colt 𝕊 ⇰ FrameType
grpt (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data') = do
  𝔹 -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard (𝔹 -> 𝑂 ()) -> 𝔹 -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ 𝕊
col 𝕊 -> 𝑃 𝕊 -> 𝔹
forall e s. Set e s => e -> s -> 𝔹
∈ 𝑃 𝕊
colp
  𝔹 -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard (𝔹 -> 𝑂 ()) -> 𝔹 -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> 𝔹
not (𝔹 -> 𝔹) -> 𝔹 -> 𝔹
forall a b. (a -> b) -> a -> b
$ 𝕊
s₀ 𝕊 -> (𝕊 ⇰ FrameType) -> 𝔹
forall a. 𝕊 -> (𝕊 ⇰ a) -> 𝔹
forall k s (d :: * -> *) a. Dict k s d => k -> d a -> 𝔹
⋿ 𝕊 ⇰ FrameType
grpt
  Frame -> 𝑂 Frame
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return (Frame -> 𝑂 Frame) -> Frame -> 𝑂 Frame
forall a b. (a -> b) -> a -> b
$
    let colp' ∷ 𝑃 𝕊
        colp' :: 𝑃 𝕊
colp' = 𝑃 𝕊
colp 𝑃 𝕊 -> 𝑃 𝕊 -> 𝑃 𝕊
forall e s. Set e s => s -> s -> s
∖ 𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
col
        colv' ∷ 𝕍 𝕊
        colv' :: 𝕍 𝕊
colv' = 𝐼 𝕊 -> 𝕍 𝕊
forall a t. ToIter a t => t -> 𝕍 a
vec (𝐼 𝕊 -> 𝕍 𝕊) -> 𝐼 𝕊 -> 𝕍 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 -> 𝔹) -> 𝕍 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => (a -> 𝔹) -> t -> 𝐼 a
filter (𝕊 -> 𝕊 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≢ 𝕊
col) 𝕍 𝕊
colv
        colt' ∷ 𝕊 ⇰ FrameType
        colt' :: 𝕊 ⇰ FrameType
colt' = 𝑃 𝕊 -> (𝕊 ⇰ FrameType) -> 𝕊 ⇰ FrameType
forall a. 𝑃 𝕊 -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => s -> d a -> d a
dtoss (𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
col) 𝕊 ⇰ FrameType
colt 
        grpt' ∷ 𝕊 ⇰ FrameType
        grpt' :: 𝕊 ⇰ FrameType
grpt' = [𝕊 ⇰ FrameType] -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict [𝕊
s₀ 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕊 ⇰ FrameType
colt (𝕊 ⇰ FrameType) -> 𝕊 -> FrameType
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col,𝕊 ⇰ FrameType
grpt]
        data'₁ ∷ (𝕊 ⇰ FrameVal) ⇰ FrameVal ⇰ ℕ64 ∧ (𝕊 ⇰ FrameCol)
        data'₁ :: (𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
data'₁ = ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data' (((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
 -> (𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))))
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall a b. (a -> b) -> a -> b
$ \ (ℕ64
n :* 𝕊 ⇰ FrameCol
svss) →
          let svs ∷ FrameCol
              svs :: FrameCol
svs = 𝕊 ⇰ FrameCol
svss (𝕊 ⇰ FrameCol) -> 𝕊 -> FrameCol
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col
              svss'₁ ∷ 𝕊 ⇰ FrameCol
              svss'₁ :: 𝕊 ⇰ FrameCol
svss'₁ = 𝑃 𝕊 -> (𝕊 ⇰ FrameCol) -> 𝕊 ⇰ FrameCol
forall a. 𝑃 𝕊 -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => s -> d a -> d a
dtoss (𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
col) 𝕊 ⇰ FrameCol
svss
              svss'₂ ∷ FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
              svss'₂ :: FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
svss'₂ = 𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)) -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)) -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
-> 𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)) -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
forall a b. (a -> b) -> a -> b
$ 𝐼 ℕ64
-> (ℕ64 -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
-> 𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (ℕ64 -> 𝐼 ℕ64
forall n. (Eq n, Zero n, One n, Plus n) => n -> 𝐼 n
upto ℕ64
n) ((ℕ64 -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
 -> 𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)))
-> (ℕ64 -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
-> 𝐼 (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
forall a b. (a -> b) -> a -> b
$ \ ℕ64
nᵢ → 
                let vᵢ :: FrameVal
vᵢ   = (𝑂 FrameVal ⌲ FrameVal) -> 𝑂 FrameVal -> FrameVal
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameVal ⌲ FrameVal
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameVal -> FrameVal) -> 𝑂 FrameVal -> FrameVal
forall a b. (a -> b) -> a -> b
$ ℕ64 -> FrameCol -> 𝑂 FrameVal
frameColIndex ℕ64
nᵢ FrameCol
svs
                    svsᵢ :: 𝕊 ⇰ FrameVal
svsᵢ = (𝕊 ⇰ FrameCol) -> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕊 ⇰ FrameCol
svss'₁ ((FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal)
-> (FrameCol -> FrameVal) -> 𝕊 ⇰ FrameVal
forall a b. (a -> b) -> a -> b
$ (𝑂 FrameVal ⌲ FrameVal) -> 𝑂 FrameVal -> FrameVal
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameVal ⌲ FrameVal
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameVal -> FrameVal)
-> (FrameCol -> 𝑂 FrameVal) -> FrameCol -> FrameVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> FrameCol -> 𝑂 FrameVal
frameColIndex ℕ64
nᵢ
                in FrameVal
vᵢ FrameVal -> 𝐼C (𝕊 ⇰ FrameVal) -> FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
forall a. FrameVal -> a -> FrameVal ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ (𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a t. Single a t => a -> t
single 𝕊 ⇰ FrameVal
svsᵢ
              svss'₃ ∷ FrameVal ⇰ ℕ64 ∧ (𝕊 ⇰ FrameCol)
              svss'₃ :: FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
svss'₃ = (FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal))
-> (𝐼C (𝕊 ⇰ FrameVal) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn FrameVal ⇰ 𝐼C (𝕊 ⇰ FrameVal)
svss'₂ ((𝐼C (𝕊 ⇰ FrameVal) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
 -> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (𝐼C (𝕊 ⇰ FrameVal) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a b. (a -> b) -> a -> b
$ \ 𝐼C (𝕊 ⇰ FrameVal)
svssᵢ →
                let rows :: ℕ64
rows = 𝐼C (𝕊 ⇰ FrameVal) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝐼C (𝕊 ⇰ FrameVal)
svssᵢ
                    svsᵢ :: 𝕊 ⇰ FrameCol
svsᵢ = (𝕊 ⇰ FrameType) -> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn 𝕊 ⇰ FrameType
colt' ((𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol)
-> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ \ 𝕊
s FrameType
τ → 
                      (𝑂 FrameCol ⌲ FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameCol ⌲ FrameCol
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameCol -> FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝐼C FrameVal -> 𝑂 FrameCol
frameColPack FrameType
τ (𝐼C FrameVal -> 𝑂 FrameCol) -> 𝐼C FrameVal -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝕊 ⇰ FrameVal) -> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐼C (𝕊 ⇰ FrameVal)
svssᵢ (((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal)
-> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊 -> (𝕊 ⇰ FrameVal) -> FrameVal
forall k v t. Lookup k v t => k -> t -> v
lupΩ 𝕊
s
                in ℕ64
rows ℕ64 -> (𝕊 ⇰ FrameCol) -> ℕ64 ∧ (𝕊 ⇰ FrameCol)
forall a b. a -> b -> a ∧ b
:* 𝕊 ⇰ FrameCol
svsᵢ
          in FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
svss'₃
        data'₂ ∷ (𝕊 ⇰ FrameVal) ⇰ ℕ64 ∧ (𝕊 ⇰ FrameCol)
        data'₂ :: (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data'₂ = 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
 -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a b. (a -> b) -> a -> b
$ do
          𝕊 ⇰ FrameVal
svs :* FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
vnsvss ← ((𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))))
-> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))))
forall a t. ToIter a t => t -> 𝐼 a
iter (𝕊 ⇰ FrameVal) ⇰ (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
data'₁
          FrameVal
v :* ℕ64 ∧ (𝕊 ⇰ FrameCol)
nsvss ← (FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> 𝐼 (FrameVal ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall a t. ToIter a t => t -> 𝐼 a
iter FrameVal ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
vnsvss
          ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
 -> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol))))
-> ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall a b. (a -> b) -> a -> b
$ [𝕊 ⇰ FrameVal] -> 𝕊 ⇰ FrameVal
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict [𝕊
s₀ 𝕊 -> FrameVal -> 𝕊 ⇰ FrameVal
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameVal
v,𝕊 ⇰ FrameVal
svs] (𝕊 ⇰ FrameVal)
-> (ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a b. a -> b -> a ∧ b
:* ℕ64 ∧ (𝕊 ⇰ FrameCol)
nsvss
    in
    𝑃 𝕊
-> 𝕍 𝕊
-> (𝕊 ⇰ FrameType)
-> (𝕊 ⇰ FrameType)
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> Frame
Frame 𝑃 𝕊
colp' 𝕍 𝕊
colv' 𝕊 ⇰ FrameType
colt' 𝕊 ⇰ FrameType
grpt' (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data'₂

frameUngroup ∷ 𝕊 → 𝕊 → Frame → 𝑂 Frame
frameUngroup :: 𝕊 -> 𝕊 -> Frame -> 𝑂 Frame
frameUngroup 𝕊
grp 𝕊
s₀ (Frame 𝑃 𝕊
colp 𝕍 𝕊
colv 𝕊 ⇰ FrameType
colt 𝕊 ⇰ FrameType
grpt (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data') = do
  𝔹 -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard (𝔹 -> 𝑂 ()) -> 𝔹 -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ 𝕊
grp 𝕊 -> (𝕊 ⇰ FrameType) -> 𝔹
forall a. 𝕊 -> (𝕊 ⇰ a) -> 𝔹
forall k s (d :: * -> *) a. Dict k s d => k -> d a -> 𝔹
⋿ 𝕊 ⇰ FrameType
grpt
  𝔹 -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard (𝔹 -> 𝑂 ()) -> 𝔹 -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> 𝔹
not (𝔹 -> 𝔹) -> 𝔹 -> 𝔹
forall a b. (a -> b) -> a -> b
$ 𝕊
s₀ 𝕊 -> 𝑃 𝕊 -> 𝔹
forall e s. Set e s => e -> s -> 𝔹
∈ 𝑃 𝕊
colp
  Frame -> 𝑂 Frame
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return (Frame -> 𝑂 Frame) -> Frame -> 𝑂 Frame
forall a b. (a -> b) -> a -> b
$
    let colp' ∷ 𝑃 𝕊
        colp' :: 𝑃 𝕊
colp' = 𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
s₀ 𝑃 𝕊 -> 𝑃 𝕊 -> 𝑃 𝕊
forall e s. Set e s => s -> s -> s
∪ 𝑃 𝕊
colp
        colv' ∷ 𝕍 𝕊
        colv' :: 𝕍 𝕊
colv' = 𝕊 -> 𝕍 𝕊
forall a t. Single a t => a -> t
single 𝕊
s₀ 𝕍 𝕊 -> 𝕍 𝕊 -> 𝕍 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕍 𝕊
colv
        colt' ∷ 𝕊 ⇰ FrameType
        colt' :: 𝕊 ⇰ FrameType
colt' = [𝕊 ⇰ FrameType] -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict [𝕊
s₀ 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕊 ⇰ FrameType
grpt (𝕊 ⇰ FrameType) -> 𝕊 -> FrameType
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
grp,𝕊 ⇰ FrameType
colt]
        grpt' ∷ 𝕊 ⇰ FrameType
        grpt' :: 𝕊 ⇰ FrameType
grpt' = 𝑃 𝕊 -> (𝕊 ⇰ FrameType) -> 𝕊 ⇰ FrameType
forall a. 𝑃 𝕊 -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => s -> d a -> d a
dtoss (𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
grp) 𝕊 ⇰ FrameType
grpt
        data'₁ ∷ (𝕊 ⇰ FrameVal) ⇰ ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)
        data'₁ :: (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
data'₁ = 𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
 -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
forall a b. (a -> b) -> a -> b
$ 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> (((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
    -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
forall a t. ToIter a t => t -> 𝐼 a
iter (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data') ((((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
  -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
 -> 𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))))
-> (((𝕊 ⇰ FrameVal) ∧ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
    -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> 𝐼 ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
forall a b. (a -> b) -> a -> b
$ \ (𝕊 ⇰ FrameVal
svs :* (ℕ64
n :* 𝕊 ⇰ FrameCol
svss)) → 
          let svs' ∷ 𝕊 ⇰ FrameVal
              svs' :: 𝕊 ⇰ FrameVal
svs' = 𝑃 𝕊 -> (𝕊 ⇰ FrameVal) -> 𝕊 ⇰ FrameVal
forall a. 𝑃 𝕊 -> (𝕊 ⇰ a) -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => s -> d a -> d a
dtoss (𝕊 -> 𝑃 𝕊
forall a t. Single a t => a -> t
single 𝕊
grp) 𝕊 ⇰ FrameVal
svs 
              v ∷ FrameVal
              v :: FrameVal
v = 𝕊 ⇰ FrameVal
svs (𝕊 ⇰ FrameVal) -> 𝕊 -> FrameVal
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
grp
              svss' ∷ 𝕊 ⇰ 𝐼C FrameVal
              svss' :: 𝕊 ⇰ 𝐼C FrameVal
svss' = [𝕊 ⇰ 𝐼C FrameVal] -> 𝕊 ⇰ 𝐼C FrameVal
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict
                [ 𝕊 -> 𝐼C FrameVal -> 𝕊 ⇰ 𝐼C FrameVal
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) 𝕊
s₀ (𝐼C FrameVal -> 𝕊 ⇰ 𝐼C FrameVal) -> 𝐼C FrameVal -> 𝕊 ⇰ 𝐼C FrameVal
forall a b. (a -> b) -> a -> b
$ 𝐼C ℕ64 -> (ℕ64 -> FrameVal) -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (ℕ64 -> 𝐼C ℕ64
uptoC ℕ64
n) ((ℕ64 -> FrameVal) -> 𝐼C FrameVal)
-> (ℕ64 -> FrameVal) -> 𝐼C FrameVal
forall a b. (a -> b) -> a -> b
$ FrameVal -> ℕ64 -> FrameVal
forall a b. a -> b -> a
const FrameVal
v
                , (FrameCol -> 𝐼C FrameVal) -> (𝕊 ⇰ FrameCol) -> 𝕊 ⇰ 𝐼C FrameVal
forall a b. (a -> b) -> (𝕊 ⇰ a) -> 𝕊 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map FrameCol -> 𝐼C FrameVal
frameColUnpack 𝕊 ⇰ FrameCol
svss
                ]
          in
          𝕊 ⇰ FrameVal
svs' (𝕊 ⇰ FrameVal)
-> (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
forall a. (𝕊 ⇰ FrameVal) -> a -> (𝕊 ⇰ FrameVal) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
n ℕ64 -> (𝕊 ⇰ 𝐼C FrameVal) -> ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)
forall a b. a -> b -> a ∧ b
:* 𝕊 ⇰ 𝐼C FrameVal
svss'
        data'₂ ∷ (𝕊 ⇰ FrameVal) ⇰ ℕ64 ∧ (𝕊 ⇰ FrameCol)
        data'₂ :: (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data'₂ = ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)))
-> ((ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal))
data'₁ (((ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
 -> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((ℕ64 ∧ (𝕊 ⇰ 𝐼C FrameVal)) -> ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a b. (a -> b) -> a -> b
$ \ (ℕ64
n :* 𝕊 ⇰ 𝐼C FrameVal
svss) → 
          let svss' ∷ 𝕊 ⇰ FrameCol
              svss' :: 𝕊 ⇰ FrameCol
svss' = (𝕊 ⇰ 𝐼C FrameVal) -> (𝕊 -> 𝐼C FrameVal -> FrameCol) -> 𝕊 ⇰ FrameCol
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn 𝕊 ⇰ 𝐼C FrameVal
svss ((𝕊 -> 𝐼C FrameVal -> FrameCol) -> 𝕊 ⇰ FrameCol)
-> (𝕊 -> 𝐼C FrameVal -> FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ \ 𝕊
s 𝐼C FrameVal
vs →
                let τ ∷ FrameType
                    τ :: FrameType
τ = 𝕊 ⇰ FrameType
colt' (𝕊 ⇰ FrameType) -> 𝕊 -> FrameType
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
s
                    vs' ∷ FrameCol
                    vs' :: FrameCol
vs' = (𝑂 FrameCol ⌲ FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameCol ⌲ FrameCol
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameCol -> FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝐼C FrameVal -> 𝑂 FrameCol
frameColPack FrameType
τ 𝐼C FrameVal
vs
                in FrameCol
vs'
          in
          ℕ64
n ℕ64 -> (𝕊 ⇰ FrameCol) -> ℕ64 ∧ (𝕊 ⇰ FrameCol)
forall a b. a -> b -> a ∧ b
:* 𝕊 ⇰ FrameCol
svss'
    in
    𝑃 𝕊
-> 𝕍 𝕊
-> (𝕊 ⇰ FrameType)
-> (𝕊 ⇰ FrameType)
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> Frame
Frame 𝑃 𝕊
colp' 𝕍 𝕊
colv' 𝕊 ⇰ FrameType
colt' 𝕊 ⇰ FrameType
grpt' (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data'₂

frameValParse ∷ 𝕊 → FrameType → IO FrameVal
frameValParse :: 𝕊 -> FrameType -> IO FrameVal
frameValParse 𝕊
s = \case
  FrameType
B_FT → do
    if | 𝕊
s 𝕊 -> 𝕊 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ 𝕊
"true"  → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝔹 -> FrameVal
B_FV 𝔹
True
       | 𝕊
s 𝕊 -> 𝕊 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ 𝕊
"false" → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝔹 -> FrameVal
B_FV 𝔹
False
       | 𝔹
otherwise   → 𝕊 -> IO FrameVal
forall a. 𝕊 -> IO a
failIO (𝕊 -> IO FrameVal) -> 𝕊 -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊
"fail parse (bool): " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
s
  FrameType
N_FT → do
    case String -> Maybe ℕ64
forall a. Read a => String -> Maybe a
HS.readMaybe (String -> Maybe ℕ64) -> String -> Maybe ℕ64
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
forall a t. ToIter a t => t -> [a]
lazyList 𝕊
s of
      HS.Just ℕ64
n  → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ ℕ64 -> FrameVal
N_FV ℕ64
n
      Maybe ℕ64
HS.Nothing → 𝕊 -> IO FrameVal
forall a. 𝕊 -> IO a
failIO (𝕊 -> IO FrameVal) -> 𝕊 -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊
"fail parse (nat): " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
s
  FrameType
Z_FT → do
    case String -> Maybe ℤ64
forall a. Read a => String -> Maybe a
HS.readMaybe (String -> Maybe ℤ64) -> String -> Maybe ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
forall a t. ToIter a t => t -> [a]
lazyList 𝕊
s of
      HS.Just ℤ64
i  → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ ℤ64 -> FrameVal
Z_FV ℤ64
i
      Maybe ℤ64
HS.Nothing → 𝕊 -> IO FrameVal
forall a. 𝕊 -> IO a
failIO (𝕊 -> IO FrameVal) -> 𝕊 -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊
"fail parse (int): " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
s
  FrameType
D_FT → do
    case String -> Maybe 𝔻
forall a. Read a => String -> Maybe a
HS.readMaybe (String -> Maybe 𝔻) -> String -> Maybe 𝔻
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
forall a t. ToIter a t => t -> [a]
lazyList 𝕊
s of
      HS.Just 𝔻
d  → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝔻 -> FrameVal
D_FV 𝔻
d
      Maybe 𝔻
HS.Nothing → 𝕊 -> IO FrameVal
forall a. 𝕊 -> IO a
failIO (𝕊 -> IO FrameVal) -> 𝕊 -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊
"fail parse (dbl) " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
s
  FrameType
S_FT → FrameVal -> IO FrameVal
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (FrameVal -> IO FrameVal) -> FrameVal -> IO FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊 -> FrameVal
S_FV 𝕊
s

frameParse ∷ 𝕊 → IO Frame
frameParse :: 𝕊 -> IO Frame
frameParse 𝕊
s = do
  𝕍 (𝕍 𝕊)
sss ∷ 𝕍 (𝕍 𝕊) ← 
    (𝐿 Char -> IO (𝕍 (𝕍 𝕊)))
-> (Vector (Vector ByteString) -> IO (𝕍 (𝕍 𝕊)))
-> (𝐿 Char ∨ Vector (Vector ByteString))
-> IO (𝕍 (𝕍 𝕊))
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice (𝕊 -> IO (𝕍 (𝕍 𝕊))
forall a. 𝕊 -> IO a
failIO (𝕊 -> IO (𝕍 (𝕍 𝕊))) -> (𝐿 Char -> 𝕊) -> 𝐿 Char -> IO (𝕍 (𝕍 𝕊))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 Char -> 𝕊
forall t. ToIter Char t => t -> 𝕊
string) (𝕍 (𝕍 𝕊) -> IO (𝕍 (𝕍 𝕊))
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (𝕍 (𝕍 𝕊) -> IO (𝕍 (𝕍 𝕊)))
-> (𝕍 (Vector ByteString) -> 𝕍 (𝕍 𝕊))
-> 𝕍 (Vector ByteString)
-> IO (𝕍 (𝕍 𝕊))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Vector ByteString -> 𝕍 𝕊) -> 𝕍 (Vector ByteString) -> 𝕍 (𝕍 𝕊)
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((ByteString -> 𝕊) -> 𝕍 ByteString -> 𝕍 𝕊
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ByteString -> 𝕊
Text.decodeUtf8 (ByteString -> 𝕊) -> (ByteString -> ByteString) -> ByteString -> 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ByteString -> ByteString
BSL.toStrict) (𝕍 ByteString -> 𝕍 𝕊)
-> (Vector ByteString -> 𝕍 ByteString) -> Vector ByteString -> 𝕍 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Vector ByteString -> 𝕍 ByteString
forall a. Vector a -> 𝕍 a
𝕍) (𝕍 (Vector ByteString) -> IO (𝕍 (𝕍 𝕊)))
-> (Vector (Vector ByteString) -> 𝕍 (Vector ByteString))
-> Vector (Vector ByteString)
-> IO (𝕍 (𝕍 𝕊))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Vector (Vector ByteString) -> 𝕍 (Vector ByteString)
forall a. Vector a -> 𝕍 a
𝕍) ((𝐿 Char ∨ Vector (Vector ByteString)) -> IO (𝕍 (𝕍 𝕊)))
-> (𝐿 Char ∨ Vector (Vector ByteString)) -> IO (𝕍 (𝕍 𝕊))
forall a b. (a -> b) -> a -> b
$ 
      Either String (Vector (Vector ByteString))
-> 𝐿 Char ∨ Vector (Vector ByteString)
forall a b. CHS a b => b -> a
frhs (Either String (Vector (Vector ByteString))
 -> 𝐿 Char ∨ Vector (Vector ByteString))
-> Either String (Vector (Vector ByteString))
-> 𝐿 Char ∨ Vector (Vector ByteString)
forall a b. (a -> b) -> a -> b
$ forall a.
FromRecord a =>
HasHeader -> ByteString -> Either String (Vector a)
CSV.decode @(Vector.Vector BSL.ByteString) HasHeader
CSV.NoHeader (ByteString -> Either String (Vector (Vector ByteString)))
-> ByteString -> Either String (Vector (Vector ByteString))
forall a b. (a -> b) -> a -> b
$ 
        ByteString -> ByteString
BSL.fromStrict (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ 𝕊 -> ByteString
Text.encodeUtf8 𝕊
s
  𝐿 𝕊
cols ∷ 𝐿 𝕊 ← IO (𝐿 𝕊) -> 𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (𝕊 -> IO (𝐿 𝕊)
forall a. 𝕊 -> IO a
failIO 𝕊
"bad1") (𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)) -> 𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)
forall a b. (a -> b) -> a -> b
$ 𝕍 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list (𝕍 𝕊 -> 𝐿 𝕊) -> 𝑂 (𝕍 𝕊) -> 𝑂 (𝐿 𝕊)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕍 (𝕍 𝕊)
sss 𝕍 (𝕍 𝕊) -> ℕ64 -> 𝑂 (𝕍 𝕊)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
0
  𝐿 𝕊
typs ∷ 𝐿 𝕊 ← IO (𝐿 𝕊) -> 𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (𝕊 -> IO (𝐿 𝕊)
forall a. 𝕊 -> IO a
failIO 𝕊
"bad2") (𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)) -> 𝑂 (𝐿 𝕊) -> IO (𝐿 𝕊)
forall a b. (a -> b) -> a -> b
$ 𝕍 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list (𝕍 𝕊 -> 𝐿 𝕊) -> 𝑂 (𝕍 𝕊) -> 𝑂 (𝐿 𝕊)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝕍 (𝕍 𝕊)
sss 𝕍 (𝕍 𝕊) -> ℕ64 -> 𝑂 (𝕍 𝕊)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? ℕ64
1
  let sss' ∷ 𝕍 (𝕍 𝕊)
      sss' :: 𝕍 (𝕍 𝕊)
sss' = ℕ64 -> (ℕ64 -> 𝕍 𝕊) -> 𝕍 (𝕍 𝕊)
forall a. ℕ64 -> (ℕ64 -> a) -> 𝕍 a
vecF (𝕍 (𝕍 𝕊) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (𝕍 𝕊)
sss ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
2) ((ℕ64 -> 𝕍 𝕊) -> 𝕍 (𝕍 𝕊)) -> (ℕ64 -> 𝕍 𝕊) -> 𝕍 (𝕍 𝕊)
forall a b. (a -> b) -> a -> b
$ \ ℕ64
i → 𝕍 (𝕍 𝕊)
sss 𝕍 (𝕍 𝕊) -> ℕ64 -> 𝕍 𝕊
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! (ℕ64
i ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
2)
      rows ∷ ℕ64
      rows :: ℕ64
rows = 𝕍 (𝕍 𝕊) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (𝕍 𝕊)
sss'
  𝐿 FrameType
typs' ∷ 𝐿 FrameType ← IO (𝐿 FrameType) -> 𝑂 (𝐿 FrameType) -> IO (𝐿 FrameType)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (𝕊 -> IO (𝐿 FrameType)
forall a. 𝕊 -> IO a
failIO 𝕊
"bad3") (𝑂 (𝐿 FrameType) -> IO (𝐿 FrameType))
-> 𝑂 (𝐿 FrameType) -> IO (𝐿 FrameType)
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊 -> (𝕊 -> 𝑂 FrameType) -> 𝑂 (𝐿 FrameType)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 𝕊
typs ((𝕊 -> 𝑂 FrameType) -> 𝑂 (𝐿 FrameType))
-> (𝕊 -> 𝑂 FrameType) -> 𝑂 (𝐿 FrameType)
forall a b. (a -> b) -> a -> b
$ (𝕊 -> (𝕊 ⇰ FrameType) -> 𝑂 FrameType)
-> (𝕊 ⇰ FrameType) -> 𝕊 -> 𝑂 FrameType
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕊 -> (𝕊 ⇰ FrameType) -> 𝑂 FrameType
forall k v t. Lookup k v t => k -> t -> 𝑂 v
lup ((𝕊 ⇰ FrameType) -> 𝕊 -> 𝑂 FrameType)
-> (𝕊 ⇰ FrameType) -> 𝕊 -> 𝑂 FrameType
forall a b. (a -> b) -> a -> b
$ forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (d a) t) =>
t -> d a
dict @((⇰) _)
    [ FrameType -> 𝕊
frameTypeCode FrameType
B_FT 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameType
B_FT
    , FrameType -> 𝕊
frameTypeCode FrameType
N_FT 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameType
N_FT
    , FrameType -> 𝕊
frameTypeCode FrameType
Z_FT 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameType
Z_FT
    , FrameType -> 𝕊
frameTypeCode FrameType
D_FT 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameType
D_FT
    , FrameType -> 𝕊
frameTypeCode FrameType
S_FT 𝕊 -> FrameType -> 𝕊 ⇰ FrameType
forall a. 𝕊 -> a -> 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ FrameType
S_FT
    ]
  𝐿 (𝕊 ∧ FrameType)
coltyps ∷ 𝐿 (𝕊 ∧ FrameType) ← IO (𝐿 (𝕊 ∧ FrameType))
-> 𝑂 (𝐿 (𝕊 ∧ FrameType)) -> IO (𝐿 (𝕊 ∧ FrameType))
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (𝕊 -> IO (𝐿 (𝕊 ∧ FrameType))
forall a. 𝕊 -> IO a
failIO 𝕊
"bad4") (𝑂 (𝐿 (𝕊 ∧ FrameType)) -> IO (𝐿 (𝕊 ∧ FrameType)))
-> 𝑂 (𝐿 (𝕊 ∧ FrameType)) -> IO (𝐿 (𝕊 ∧ FrameType))
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊 -> 𝐿 FrameType -> 𝑂 (𝐿 (𝕊 ∧ FrameType))
forall a b. 𝐿 a -> 𝐿 b -> 𝑂 (𝐿 (a ∧ b))
zipSameLength 𝐿 𝕊
cols 𝐿 FrameType
typs'
  let coltyps' ∷ 𝕊 ⇰ FrameType
      coltyps' :: 𝕊 ⇰ FrameType
coltyps' = 𝐿 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc 𝐿 (𝕊 ∧ FrameType)
coltyps
  𝕍 (𝕊 ⇰ FrameVal)
svss ∷ 𝕍 (𝕊 ⇰ FrameVal) ← 𝕍 (𝕍 𝕊) -> (𝕍 𝕊 -> IO (𝕊 ⇰ FrameVal)) -> IO (𝕍 (𝕊 ⇰ FrameVal))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝕍 (𝕍 𝕊)
sss' ((𝕍 𝕊 -> IO (𝕊 ⇰ FrameVal)) -> IO (𝕍 (𝕊 ⇰ FrameVal)))
-> (𝕍 𝕊 -> IO (𝕊 ⇰ FrameVal)) -> IO (𝕍 (𝕊 ⇰ FrameVal))
forall a b. (a -> b) -> a -> b
$ \ 𝕍 𝕊
ss → do
    𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)
stss ← IO (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
-> 𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)) -> IO (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (𝕊 -> IO (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
forall a. 𝕊 -> IO a
failIO 𝕊
"unexpected row") (𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)) -> IO (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)))
-> 𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)) -> IO (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
forall a b. (a -> b) -> a -> b
$ 𝐿 (𝕊 ∧ FrameType) -> 𝐿 𝕊 -> 𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
forall a b. 𝐿 a -> 𝐿 b -> 𝑂 (𝐿 (a ∧ b))
zipSameLength 𝐿 (𝕊 ∧ FrameType)
coltyps (𝐿 𝕊 -> 𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)))
-> 𝐿 𝕊 -> 𝑂 (𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊))
forall a b. (a -> b) -> a -> b
$ 𝕍 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list 𝕍 𝕊
ss
    𝐿 (𝕊 ∧ FrameVal) -> 𝕊 ⇰ FrameVal
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐿 (𝕊 ∧ FrameVal) -> 𝕊 ⇰ FrameVal)
-> IO (𝐿 (𝕊 ∧ FrameVal)) -> IO (𝕊 ⇰ FrameVal)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)
-> (((𝕊 ∧ FrameType) ∧ 𝕊) -> IO (𝕊 ∧ FrameVal))
-> IO (𝐿 (𝕊 ∧ FrameVal))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 ((𝕊 ∧ FrameType) ∧ 𝕊)
stss ((((𝕊 ∧ FrameType) ∧ 𝕊) -> IO (𝕊 ∧ FrameVal))
 -> IO (𝐿 (𝕊 ∧ FrameVal)))
-> (((𝕊 ∧ FrameType) ∧ 𝕊) -> IO (𝕊 ∧ FrameVal))
-> IO (𝐿 (𝕊 ∧ FrameVal))
forall a b. (a -> b) -> a -> b
$ \ ((𝕊
key :* FrameType
t) :* 𝕊
sᵢ) → do
      FrameVal
v ← 𝕊 -> FrameType -> IO FrameVal
frameValParse 𝕊
sᵢ FrameType
t
      (𝕊 ∧ FrameVal) -> IO (𝕊 ∧ FrameVal)
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return ((𝕊 ∧ FrameVal) -> IO (𝕊 ∧ FrameVal))
-> (𝕊 ∧ FrameVal) -> IO (𝕊 ∧ FrameVal)
forall a b. (a -> b) -> a -> b
$ 𝕊
key 𝕊 -> FrameVal -> 𝕊 ∧ FrameVal
forall a b. a -> b -> a ∧ b
:* FrameVal
v
  let svss' ∷ 𝕊 ⇰ FrameCol
      svss' :: 𝕊 ⇰ FrameCol
svss' = (𝕊 ⇰ FrameType) -> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn 𝕊 ⇰ FrameType
coltyps' ((𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol)
-> (𝕊 -> FrameType -> FrameCol) -> 𝕊 ⇰ FrameCol
forall a b. (a -> b) -> a -> b
$ \ 𝕊
sᵢ FrameType
τ → 
        (𝑂 FrameCol ⌲ FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a ⌲ b) -> a -> b
viewΩ 𝑂 FrameCol ⌲ FrameCol
forall a. 𝑂 a ⌲ a
someL (𝑂 FrameCol -> FrameCol) -> 𝑂 FrameCol -> FrameCol
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝐼C FrameVal -> 𝑂 FrameCol
frameColPack FrameType
τ (𝐼C FrameVal -> 𝑂 FrameCol) -> 𝐼C FrameVal -> 𝑂 FrameCol
forall a b. (a -> b) -> a -> b
$ 𝐼C (𝕊 ⇰ FrameVal) -> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝕍 (𝕊 ⇰ FrameVal) -> 𝐼C (𝕊 ⇰ FrameVal)
forall a t. ToIterC a t => t -> 𝐼C a
iterC 𝕍 (𝕊 ⇰ FrameVal)
svss) (((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal)
-> ((𝕊 ⇰ FrameVal) -> FrameVal) -> 𝐼C FrameVal
forall a b. (a -> b) -> a -> b
$ 𝕊 -> (𝕊 ⇰ FrameVal) -> FrameVal
forall k v t. Lookup k v t => k -> t -> v
lupΩ 𝕊
sᵢ
  Frame -> IO Frame
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return (Frame -> IO Frame) -> Frame -> IO Frame
forall a b. (a -> b) -> a -> b
$ 𝑃 𝕊
-> 𝕍 𝕊
-> (𝕊 ⇰ FrameType)
-> (𝕊 ⇰ FrameType)
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> Frame
Frame (𝐿 𝕊 -> 𝑃 𝕊
forall s t e. (ToIter e t, Set e s) => t -> s
pow 𝐿 𝕊
cols) (𝐿 𝕊 -> 𝕍 𝕊
forall a t. ToIter a t => t -> 𝕍 a
vec 𝐿 𝕊
cols) (𝐿 (𝕊 ∧ FrameType) -> 𝕊 ⇰ FrameType
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc 𝐿 (𝕊 ∧ FrameType)
coltyps) 𝕊 ⇰ FrameType
forall a. Null a => a
null (((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))) -> Frame)
-> ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))) -> Frame
forall a b. (a -> b) -> a -> b
$ 𝕊 ⇰ FrameVal
forall a. Null a => a
null (𝕊 ⇰ FrameVal)
-> (ℕ64 ∧ (𝕊 ⇰ FrameCol))
-> (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
forall a. (𝕊 ⇰ FrameVal) -> a -> (𝕊 ⇰ FrameVal) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ (ℕ64
rows ℕ64 -> (𝕊 ⇰ FrameCol) -> ℕ64 ∧ (𝕊 ⇰ FrameCol)
forall a b. a -> b -> a ∧ b
:* 𝕊 ⇰ FrameCol
svss')

instance Pretty Frame where
  pretty :: Frame -> Doc
pretty (Frame 𝑃 𝕊
_colp 𝕍 𝕊
colv 𝕊 ⇰ FrameType
colt 𝕊 ⇰ FrameType
grps (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data') = 
    let data'' :: (𝕊 ⇰ FrameVal) ⇰ Doc
data'' = ((𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol)))
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> Doc) -> (𝕊 ⇰ FrameVal) ⇰ Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝕊 ⇰ FrameVal) ⇰ (ℕ64 ∧ (𝕊 ⇰ FrameCol))
data' (((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> Doc) -> (𝕊 ⇰ FrameVal) ⇰ Doc)
-> ((ℕ64 ∧ (𝕊 ⇰ FrameCol)) -> Doc) -> (𝕊 ⇰ FrameVal) ⇰ Doc
forall a b. (a -> b) -> a -> b
$ \ (ℕ64
rows :* 𝕊 ⇰ FrameCol
svss) → 
          let svss' ∷ 𝕊 ⇰ 𝕍 𝕊
              svss' :: 𝕊 ⇰ 𝕍 𝕊
svss' = (FrameCol -> 𝕍 𝕊) -> (𝕊 ⇰ FrameCol) -> 𝕊 ⇰ 𝕍 𝕊
forall a b. (a -> b) -> (𝕊 ⇰ a) -> 𝕊 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝐼C 𝕊 -> 𝕍 𝕊
forall a t. ToIterC a t => t -> 𝕍 a
vecC (𝐼C 𝕊 -> 𝕍 𝕊) -> (𝐼C FrameVal -> 𝐼C 𝕊) -> 𝐼C FrameVal -> 𝕍 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (FrameVal -> 𝕊) -> 𝐼C FrameVal -> 𝐼C 𝕊
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map FrameVal -> 𝕊
forall a. Pretty a => a -> 𝕊
ppshow (𝐼C FrameVal -> 𝕍 𝕊)
-> (FrameCol -> 𝐼C FrameVal) -> FrameCol -> 𝕍 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ FrameCol -> 𝐼C FrameVal
frameColUnpack) 𝕊 ⇰ FrameCol
svss
              colWidths ∷ 𝕍 (𝕊 ∧ ℕ64)
              colWidths :: 𝕍 (𝕊 ∧ ℕ64)
colWidths = 𝕍 𝕊 -> (𝕊 -> 𝕊 ∧ ℕ64) -> 𝕍 (𝕊 ∧ ℕ64)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 𝕊
colv ((𝕊 -> 𝕊 ∧ ℕ64) -> 𝕍 (𝕊 ∧ ℕ64)) -> (𝕊 -> 𝕊 ∧ ℕ64) -> 𝕍 (𝕊 ∧ ℕ64)
forall a b. (a -> b) -> a -> b
$ \ 𝕊
col → 
                𝕊 -> ℕ64 -> 𝕊 ∧ ℕ64
forall a b. a -> b -> a ∧ b
(:*) 𝕊
col (ℕ64 -> 𝕊 ∧ ℕ64) -> ℕ64 -> 𝕊 ∧ ℕ64
forall a b. (a -> b) -> a -> b
$ [ℕ64] -> ℕ64
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins
                  [ 𝕊 -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕊
col
                  , 𝕊 -> ℕ64
forall a. CSized a => a -> ℕ64
csize (𝕊 -> ℕ64) -> 𝕊 -> ℕ64
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝕊
frameTypeCode (FrameType -> 𝕊) -> FrameType -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 ⇰ FrameType
colt (𝕊 ⇰ FrameType) -> 𝕊 -> FrameType
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col
                  , 𝕍 ℕ64 -> ℕ64
forall a t. (JoinLattice a, ToIter a t) => t -> a
joins (𝕍 ℕ64 -> ℕ64) -> 𝕍 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ (𝕊 -> ℕ64) -> 𝕍 𝕊 -> 𝕍 ℕ64
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝕊 -> ℕ64
forall a. CSized a => a -> ℕ64
csize (𝕍 𝕊 -> 𝕍 ℕ64) -> 𝕍 𝕊 -> 𝕍 ℕ64
forall a b. (a -> b) -> a -> b
$ 𝕊 ⇰ 𝕍 𝕊
svss' (𝕊 ⇰ 𝕍 𝕊) -> 𝕊 -> 𝕍 𝕊
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col
                  ]
          in 
          [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
            [ Doc
ppForceBreak
            , [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
                [ 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝕍 Doc -> 𝐼 Doc
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween (𝕊 -> Doc
ppComment 𝕊
"|") (𝕍 Doc -> 𝐼 Doc) -> 𝕍 Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 𝕍 (𝕊 ∧ ℕ64) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 (𝕊 ∧ ℕ64)
colWidths (((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝕊
col :* ℕ64
width) → 
                    𝕊 -> Doc
ppCon (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊 -> 𝕊
alignLeft (ℕ64 -> ℕ
forall a. ToNat a => a -> ℕ
nat ℕ64
width) 𝕊
col
                , 𝕊 -> Doc
ppComment (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 Char -> 𝕊
forall t. ToIter Char t => t -> 𝕊
string (𝐼 Char -> 𝕊) -> 𝐼 Char -> 𝕊
forall a b. (a -> b) -> a -> b
$ 
                    ℕ64 -> Char -> 𝐼 Char
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate ([ℕ64] -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum [𝕍 ℕ64 -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum (𝕍 ℕ64 -> ℕ64) -> 𝕍 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ((𝕊 ∧ ℕ64) -> ℕ64) -> 𝕍 (𝕊 ∧ ℕ64) -> 𝕍 ℕ64
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕊 ∧ ℕ64) -> ℕ64
forall a b. (a ∧ b) -> b
snd 𝕍 (𝕊 ∧ ℕ64)
colWidths,(𝕍 (𝕊 ∧ ℕ64) -> ℕ64
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count 𝕍 (𝕊 ∧ ℕ64)
colWidths ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
1 ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
1) ℕ64 -> ℕ64 -> ℕ64
forall a. Times a => a -> a -> a
× ℕ64
3]) Char
'-'
                , 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝕍 Doc -> 𝐼 Doc
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween (𝕊 -> Doc
ppComment 𝕊
"|") (𝕍 Doc -> 𝐼 Doc) -> 𝕍 Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 𝕍 (𝕊 ∧ ℕ64) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 (𝕊 ∧ ℕ64)
colWidths (((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝕊
col :* ℕ64
width) →
                    𝕊 -> Doc
ppComment (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊 -> 𝕊
alignLeft (ℕ64 -> ℕ
forall a. ToNat a => a -> ℕ
nat ℕ64
width) (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ FrameType -> 𝕊
frameTypeCode (FrameType -> 𝕊) -> FrameType -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 ⇰ FrameType
colt (𝕊 ⇰ FrameType) -> 𝕊 -> FrameType
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col
                , 𝕊 -> Doc
ppComment (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 Char -> 𝕊
forall t. ToIter Char t => t -> 𝕊
string (𝐼 Char -> 𝕊) -> 𝐼 Char -> 𝕊
forall a b. (a -> b) -> a -> b
$ 
                    ℕ64 -> Char -> 𝐼 Char
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate ([ℕ64] -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum [𝕍 ℕ64 -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum (𝕍 ℕ64 -> ℕ64) -> 𝕍 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ((𝕊 ∧ ℕ64) -> ℕ64) -> 𝕍 (𝕊 ∧ ℕ64) -> 𝕍 ℕ64
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕊 ∧ ℕ64) -> ℕ64
forall a b. (a ∧ b) -> b
snd 𝕍 (𝕊 ∧ ℕ64)
colWidths,(𝕍 (𝕊 ∧ ℕ64) -> ℕ64
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count 𝕍 (𝕊 ∧ ℕ64)
colWidths ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
1 ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
1) ℕ64 -> ℕ64 -> ℕ64
forall a. Times a => a -> a -> a
× ℕ64
3]) Char
'-'
                , 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 ℕ64 -> (ℕ64 -> Doc) -> 𝐼 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (ℕ64 -> 𝐼 ℕ64
forall n. (Eq n, Zero n, One n, Plus n) => n -> 𝐼 n
upto ℕ64
rows) ((ℕ64 -> Doc) -> 𝐼 Doc) -> (ℕ64 -> Doc) -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ \ ℕ64
n →
                    𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝕍 Doc -> 𝐼 Doc
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween (𝕊 -> Doc
ppComment 𝕊
"|") (𝕍 Doc -> 𝐼 Doc) -> 𝕍 Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 𝕍 (𝕊 ∧ ℕ64) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 (𝕊 ∧ ℕ64)
colWidths (((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc) -> ((𝕊 ∧ ℕ64) -> Doc) -> 𝕍 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝕊
col :* ℕ64
width) →
                      𝕊 -> Doc
ppLit (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊 -> 𝕊
alignLeft (ℕ64 -> ℕ
forall a. ToNat a => a -> ℕ
nat ℕ64
width) (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ (𝕊 ⇰ 𝕍 𝕊
svss' (𝕊 ⇰ 𝕍 𝕊) -> 𝕊 -> 𝕍 𝕊
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊
col) 𝕍 𝕊 -> ℕ64 -> 𝕊
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℕ64
n
                , 𝕊 -> Doc
ppComment (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊
"⇈ ROWS: " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ ℕ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ64
rows
                ]
            ]
    in 
    if
    | (𝕊 ⇰ FrameType) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝕊 ⇰ FrameType
grps → Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (𝕊 ⇰ FrameVal) ⇰ Doc
data'' ((𝕊 ⇰ FrameVal) ⇰ Doc) -> (𝕊 ⇰ FrameVal) -> Doc
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! 𝕊 ⇰ FrameVal
forall a. Null a => a
null
    | 𝔹
otherwise    → ((𝕊 ⇰ FrameVal) ⇰ Doc) -> Doc
forall a. Pretty a => a -> Doc
pretty (𝕊 ⇰ FrameVal) ⇰ Doc
data''