{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE OverloadedStrings #-}

module BytePatch where

import           StreamPatch.Patch
import qualified StreamPatch.Patch.Binary as Bin
import qualified StreamPatch.Patch.Align  as Align

import           Numeric.Natural
import           Data.Functor.Const
import           Data.Vinyl
import           Data.Vinyl.TypeLevel
import           Data.Aeson
import           GHC.Generics ( Generic )

data MultiPatch s a = MultiPatch
  { forall (s :: SeekKind) a. MultiPatch s a -> a
mpData :: a
  , forall (s :: SeekKind) a. MultiPatch s a -> [Seek s a]
mpAt :: [Seek s a]
  } deriving ((forall x. MultiPatch s a -> Rep (MultiPatch s a) x)
-> (forall x. Rep (MultiPatch s a) x -> MultiPatch s a)
-> Generic (MultiPatch s a)
forall x. Rep (MultiPatch s a) x -> MultiPatch s a
forall x. MultiPatch s a -> Rep (MultiPatch s a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: SeekKind) a x.
Rep (MultiPatch s a) x -> MultiPatch s a
forall (s :: SeekKind) a x.
MultiPatch s a -> Rep (MultiPatch s a) x
$cto :: forall (s :: SeekKind) a x.
Rep (MultiPatch s a) x -> MultiPatch s a
$cfrom :: forall (s :: SeekKind) a x.
MultiPatch s a -> Rep (MultiPatch s a) x
Generic)

deriving instance (Eq   a, Eq   (SeekRep s)) => Eq   (MultiPatch s a)
deriving instance (Show a, Show (SeekRep s)) => Show (MultiPatch s a)

data Seek s a = Seek
  { forall (s :: SeekKind) a. Seek s a -> SeekRep s
sSeek :: SeekRep s
  , forall (s :: SeekKind) a. Seek s a -> Maybe a
sExpected :: Maybe a
  , forall (s :: SeekKind) a. Seek s a -> Maybe (SeekRep 'FwdSeek)
sNullTerminates :: Maybe (SeekRep 'FwdSeek)
  , forall (s :: SeekKind) a. Seek s a -> Maybe (SeekRep 'FwdSeek)
sMaxBytes :: Maybe (SeekRep 'FwdSeek) -- TODO confirm meaning, maybe improve name
  , forall (s :: SeekKind) a. Seek s a -> Maybe Natural
sAligned :: Maybe Natural
  } deriving ((forall x. Seek s a -> Rep (Seek s a) x)
-> (forall x. Rep (Seek s a) x -> Seek s a) -> Generic (Seek s a)
forall x. Rep (Seek s a) x -> Seek s a
forall x. Seek s a -> Rep (Seek s a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: SeekKind) a x. Rep (Seek s a) x -> Seek s a
forall (s :: SeekKind) a x. Seek s a -> Rep (Seek s a) x
$cto :: forall (s :: SeekKind) a x. Rep (Seek s a) x -> Seek s a
$cfrom :: forall (s :: SeekKind) a x. Seek s a -> Rep (Seek s a) x
Generic)

deriving instance (Eq   a, Eq   (SeekRep s)) => Eq   (Seek s a)
deriving instance (Show a, Show (SeekRep s)) => Show (Seek s a)

-- TODO write a Text newtype for Haskell-style negated integers -- allowing
-- negative hex integers!
data Aligned p = Aligned
  { forall p. Aligned p -> SeekRep 'RelSeek
alignedAlign   :: SeekRep 'RelSeek
  , forall p. Aligned p -> [p]
alignedPatches :: [p]
  } deriving (Aligned p -> Aligned p -> Bool
(Aligned p -> Aligned p -> Bool)
-> (Aligned p -> Aligned p -> Bool) -> Eq (Aligned p)
forall p. Eq p => Aligned p -> Aligned p -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Aligned p -> Aligned p -> Bool
$c/= :: forall p. Eq p => Aligned p -> Aligned p -> Bool
== :: Aligned p -> Aligned p -> Bool
$c== :: forall p. Eq p => Aligned p -> Aligned p -> Bool
Eq, Int -> Aligned p -> ShowS
[Aligned p] -> ShowS
Aligned p -> String
(Int -> Aligned p -> ShowS)
-> (Aligned p -> String)
-> ([Aligned p] -> ShowS)
-> Show (Aligned p)
forall p. Show p => Int -> Aligned p -> ShowS
forall p. Show p => [Aligned p] -> ShowS
forall p. Show p => Aligned p -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Aligned p] -> ShowS
$cshowList :: forall p. Show p => [Aligned p] -> ShowS
show :: Aligned p -> String
$cshow :: forall p. Show p => Aligned p -> String
showsPrec :: Int -> Aligned p -> ShowS
$cshowsPrec :: forall p. Show p => Int -> Aligned p -> ShowS
Show, (forall x. Aligned p -> Rep (Aligned p) x)
-> (forall x. Rep (Aligned p) x -> Aligned p)
-> Generic (Aligned p)
forall x. Rep (Aligned p) x -> Aligned p
forall x. Aligned p -> Rep (Aligned p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p x. Rep (Aligned p) x -> Aligned p
forall p x. Aligned p -> Rep (Aligned p) x
$cto :: forall p x. Rep (Aligned p) x -> Aligned p
$cfrom :: forall p x. Aligned p -> Rep (Aligned p) x
Generic)

--------------------------------------------------------------------------------

jsonCfgCamelDrop :: Int -> Options
jsonCfgCamelDrop :: Int -> Options
jsonCfgCamelDrop Int
x = Options
defaultOptions
  { fieldLabelModifier :: ShowS
fieldLabelModifier = Char -> ShowS
camelTo2 Char
'_' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
x
  , rejectUnknownFields :: Bool
rejectUnknownFields = Bool
False }

instance (ToJSON   (SeekRep s), ToJSON   a) => ToJSON   (MultiPatch s a) where
    toJSON :: MultiPatch s a -> Value
toJSON     = Options -> MultiPatch s a -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON     (Options -> MultiPatch s a -> Value)
-> Options -> MultiPatch s a -> Value
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
2
    toEncoding :: MultiPatch s a -> Encoding
toEncoding = Options -> MultiPatch s a -> Encoding
forall a.
(Generic a, GToJSON' Encoding Zero (Rep a)) =>
Options -> a -> Encoding
genericToEncoding (Options -> MultiPatch s a -> Encoding)
-> Options -> MultiPatch s a -> Encoding
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
2
instance (FromJSON (SeekRep s), FromJSON a) => FromJSON (MultiPatch s a) where
    parseJSON :: Value -> Parser (MultiPatch s a)
parseJSON  = Options -> Value -> Parser (MultiPatch s a)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON  (Options -> Value -> Parser (MultiPatch s a))
-> Options -> Value -> Parser (MultiPatch s a)
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
2

instance (ToJSON   (SeekRep s), ToJSON   a) => ToJSON   (Seek s a) where
    toJSON :: Seek s a -> Value
toJSON     = Options -> Seek s a -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON     (Options -> Seek s a -> Value) -> Options -> Seek s a -> Value
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
1
    toEncoding :: Seek s a -> Encoding
toEncoding = Options -> Seek s a -> Encoding
forall a.
(Generic a, GToJSON' Encoding Zero (Rep a)) =>
Options -> a -> Encoding
genericToEncoding (Options -> Seek s a -> Encoding)
-> Options -> Seek s a -> Encoding
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
1
instance (FromJSON (SeekRep s), FromJSON a) => FromJSON (Seek s a) where
    parseJSON :: Value -> Parser (Seek s a)
parseJSON  = Options -> Value -> Parser (Seek s a)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON  (Options -> Value -> Parser (Seek s a))
-> Options -> Value -> Parser (Seek s a)
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
1

instance (ToJSON   p) => ToJSON   (Aligned p) where
    toJSON :: Aligned p -> Value
toJSON     = Options -> Aligned p -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON     (Options -> Aligned p -> Value) -> Options -> Aligned p -> Value
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
7
    toEncoding :: Aligned p -> Encoding
toEncoding = Options -> Aligned p -> Encoding
forall a.
(Generic a, GToJSON' Encoding Zero (Rep a)) =>
Options -> a -> Encoding
genericToEncoding (Options -> Aligned p -> Encoding)
-> Options -> Aligned p -> Encoding
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
7
instance (FromJSON p) => FromJSON (Aligned p) where
    parseJSON :: Value -> Parser (Aligned p)
parseJSON  = Options -> Value -> Parser (Aligned p)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON  (Options -> Value -> Parser (Aligned p))
-> Options -> Value -> Parser (Aligned p)
forall a b. (a -> b) -> a -> b
$ Int -> Options
jsonCfgCamelDrop Int
7

--------------------------------------------------------------------------------

convert :: (Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert :: forall (s :: SeekKind) a (fs :: [* -> *]).
(Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert Seek s a -> Rec (Flap a) fs
f MultiPatch s a
p = (Seek s a -> Patch s fs a) -> [Seek s a] -> [Patch s fs a]
forall a b. (a -> b) -> [a] -> [b]
map Seek s a -> Patch s fs a
go (MultiPatch s a -> [Seek s a]
forall (s :: SeekKind) a. MultiPatch s a -> [Seek s a]
mpAt MultiPatch s a
p)
  where go :: Seek s a -> Patch s fs a
go Seek s a
s = Patch :: forall (s :: SeekKind) (fs :: [* -> *]) a.
a -> SeekRep s -> FunctorRec fs a -> Patch s fs a
Patch { patchData :: a
patchData = MultiPatch s a -> a
forall (s :: SeekKind) a. MultiPatch s a -> a
mpData MultiPatch s a
p
                     , patchSeek :: SeekRep s
patchSeek = Seek s a -> SeekRep s
forall (s :: SeekKind) a. Seek s a -> SeekRep s
sSeek Seek s a
s
                     , patchMeta :: FunctorRec fs a
patchMeta = Rec (Flap a) fs -> FunctorRec fs a
forall (fs :: [* -> *]) a. Rec (Flap a) fs -> FunctorRec fs a
FunctorRec (Rec (Flap a) fs -> FunctorRec fs a)
-> Rec (Flap a) fs -> FunctorRec fs a
forall a b. (a -> b) -> a -> b
$ Seek s a -> Rec (Flap a) fs
f Seek s a
s }

-- TODO how to clean up (it's like liftA2 over n instead of 2. like a fold)
-- likely 'ap'!
convertBinAlign
    :: forall s a
    .  SeekRep s ~ Natural
    => MultiPatch 'RelSeek a
    -> [Patch 'RelSeek '[Const (Align.Meta s), Const Bin.Meta, Bin.MetaStream] a]
convertBinAlign :: forall (s :: SeekKind) a.
(SeekRep s ~ Natural) =>
MultiPatch 'RelSeek a
-> [Patch 'RelSeek '[Const (Meta s), Const Meta, MetaStream] a]
convertBinAlign MultiPatch 'RelSeek a
p = (Seek 'RelSeek a
 -> Rec (Flap a) '[Const (Meta s), Const Meta, MetaStream])
-> MultiPatch 'RelSeek a
-> [Patch 'RelSeek '[Const (Meta s), Const Meta, MetaStream] a]
forall (s :: SeekKind) a (fs :: [* -> *]).
(Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert Seek 'RelSeek a
-> Rec (Flap a) '[Const (Meta s), Const Meta, MetaStream]
forall {s :: SeekKind} {a}.
(SeekRep s ~ Natural) =>
Seek 'RelSeek a
-> Rec (Flap a) '[Const (Meta s), Const Meta, MetaStream]
go MultiPatch 'RelSeek a
p
  where go :: Seek 'RelSeek a
-> Rec (Flap a) ('[Const (Meta s)] ++ '[Const Meta, MetaStream])
go Seek 'RelSeek a
s = Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)]
forall (s :: SeekKind) a.
(SeekRep s ~ Natural) =>
Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)]
cmAlign Seek 'RelSeek a
s Rec (Flap a) '[Const (Meta s)]
-> Rec (Flap a) '[Const Meta, MetaStream]
-> Rec (Flap a) ('[Const (Meta s)] ++ '[Const Meta, MetaStream])
forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Seek 'RelSeek a -> Rec (Flap a) '[Const Meta]
forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[Const Meta]
cmBin Seek 'RelSeek a
s Rec (Flap a) '[Const Meta]
-> Rec (Flap a) '[MetaStream]
-> Rec (Flap a) ('[Const Meta] ++ '[MetaStream])
forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Seek 'RelSeek a -> Rec (Flap a) '[MetaStream]
forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[MetaStream]
cmBinStream Seek 'RelSeek a
s

convertBin
    :: forall s a
    .  MultiPatch s a
    -> [Patch s '[Const Bin.Meta, Bin.MetaStream] a]
convertBin :: forall (s :: SeekKind) a.
MultiPatch s a -> [Patch s '[Const Meta, MetaStream] a]
convertBin MultiPatch s a
p = (Seek s a -> Rec (Flap a) '[Const Meta, MetaStream])
-> MultiPatch s a -> [Patch s '[Const Meta, MetaStream] a]
forall (s :: SeekKind) a (fs :: [* -> *]).
(Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert Seek s a -> Rec (Flap a) '[Const Meta, MetaStream]
forall {s :: SeekKind} {a}.
Seek s a -> Rec (Flap a) '[Const Meta, MetaStream]
go MultiPatch s a
p
  where go :: Seek s a -> Rec (Flap a) ('[Const Meta] ++ '[MetaStream])
go Seek s a
s = Seek s a -> Rec (Flap a) '[Const Meta]
forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[Const Meta]
cmBin Seek s a
s Rec (Flap a) '[Const Meta]
-> Rec (Flap a) '[MetaStream]
-> Rec (Flap a) ('[Const Meta] ++ '[MetaStream])
forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Seek s a -> Rec (Flap a) '[MetaStream]
forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[MetaStream]
cmBinStream Seek s a
s

convertAlign
    :: forall s a
    .  SeekRep s ~ Natural
    => MultiPatch 'RelSeek a
    -> [Patch 'RelSeek '[Const (Align.Meta s)] a]
convertAlign :: forall (s :: SeekKind) a.
(SeekRep s ~ Natural) =>
MultiPatch 'RelSeek a -> [Patch 'RelSeek '[Const (Meta s)] a]
convertAlign MultiPatch 'RelSeek a
p = (Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)])
-> MultiPatch 'RelSeek a -> [Patch 'RelSeek '[Const (Meta s)] a]
forall (s :: SeekKind) a (fs :: [* -> *]).
(Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)]
forall (s :: SeekKind) a.
(SeekRep s ~ Natural) =>
Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)]
cmAlign MultiPatch 'RelSeek a
p

convertEmpty
    :: forall s a
    .  MultiPatch s a
    -> [Patch s '[] a]
convertEmpty :: forall (s :: SeekKind) a. MultiPatch s a -> [Patch s '[] a]
convertEmpty MultiPatch s a
p = (Seek s a -> Rec (Flap a) '[]) -> MultiPatch s a -> [Patch s '[] a]
forall (s :: SeekKind) a (fs :: [* -> *]).
(Seek s a -> Rec (Flap a) fs) -> MultiPatch s a -> [Patch s fs a]
convert (Rec (Flap a) '[] -> Seek s a -> Rec (Flap a) '[]
forall a b. a -> b -> a
const Rec (Flap a) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil) MultiPatch s a
p

--------------------------------------------------------------------------------

align
    :: forall s a ss rs is i r
    .  ( SeekRep s ~ Natural
       , r ~ Const (Align.Meta s)
       , rs ~ RDelete r ss
       , RElem r ss i
       , RSubset rs ss is )
    => Aligned (Patch 'RelSeek ss a)
    -> Either (Align.Error s) [Patch s rs a]
align :: forall (s :: SeekKind) a (ss :: [* -> *]) (rs :: [* -> *])
       (is :: [Nat]) (i :: Nat) (r :: * -> *).
(SeekRep s ~ Natural, r ~ Const (Meta s), rs ~ RDelete r ss,
 RElem r ss i, RSubset rs ss is) =>
Aligned (Patch 'RelSeek ss a) -> Either (Error s) [Patch s rs a]
align (Aligned SeekRep 'RelSeek
a [Patch 'RelSeek ss a]
ps) = (Patch 'RelSeek ss a -> Either (Error s) (Patch s rs a))
-> [Patch 'RelSeek ss a] -> Either (Error s) [Patch s rs a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SeekRep 'RelSeek
-> Patch 'RelSeek ss a -> Either (Error s) (Patch s rs a)
forall (s :: SeekKind) a (ss :: [* -> *]) (rs :: [* -> *])
       (is :: [Nat]) (i :: Nat) (r :: * -> *).
(SeekRep s ~ Natural, r ~ Const (Meta s), rs ~ RDelete r ss,
 RElem r ss i, RSubset rs ss is) =>
SeekRep 'RelSeek
-> Patch 'RelSeek ss a -> Either (Error s) (Patch s rs a)
Align.align SeekRep 'RelSeek
a) [Patch 'RelSeek ss a]
ps

--------------------------------------------------------------------------------

cmBin :: Seek s a -> Rec (Flap a) '[Const Bin.Meta]
cmBin :: forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[Const Meta]
cmBin Seek s a
s = Const Meta a -> Rec (Flap a) '[Const Meta]
forall (f :: * -> *) a. f a -> Rec (Flap a) '[f]
cm (Const Meta a -> Rec (Flap a) '[Const Meta])
-> Const Meta a -> Rec (Flap a) '[Const Meta]
forall a b. (a -> b) -> a -> b
$ Meta -> Const Meta a
forall {k} a (b :: k). a -> Const a b
Const (Meta -> Const Meta a) -> Meta -> Const Meta a
forall a b. (a -> b) -> a -> b
$ Meta :: Maybe (SeekRep 'FwdSeek) -> Meta
Bin.Meta { mMaxBytes :: Maybe (SeekRep 'FwdSeek)
Bin.mMaxBytes = Seek s a -> Maybe (SeekRep 'FwdSeek)
forall (s :: SeekKind) a. Seek s a -> Maybe (SeekRep 'FwdSeek)
sMaxBytes Seek s a
s }

cmBinStream :: Seek s a -> Rec (Flap a) '[Bin.MetaStream]
cmBinStream :: forall (s :: SeekKind) a. Seek s a -> Rec (Flap a) '[MetaStream]
cmBinStream Seek s a
s = MetaStream a -> Rec (Flap a) '[MetaStream]
forall (f :: * -> *) a. f a -> Rec (Flap a) '[f]
cm (MetaStream a -> Rec (Flap a) '[MetaStream])
-> MetaStream a -> Rec (Flap a) '[MetaStream]
forall a b. (a -> b) -> a -> b
$ MetaStream :: forall a. Maybe (SeekRep 'FwdSeek) -> Maybe a -> MetaStream a
Bin.MetaStream
    { msNullTerminates :: Maybe (SeekRep 'FwdSeek)
Bin.msNullTerminates = Seek s a -> Maybe (SeekRep 'FwdSeek)
forall (s :: SeekKind) a. Seek s a -> Maybe (SeekRep 'FwdSeek)
sNullTerminates Seek s a
s
    , msExpected :: Maybe a
Bin.msExpected = Seek s a -> Maybe a
forall (s :: SeekKind) a. Seek s a -> Maybe a
sExpected Seek s a
s }

cmAlign :: SeekRep s ~ Natural => Seek 'RelSeek a -> Rec (Flap a) '[Const (Align.Meta s)]
cmAlign :: forall (s :: SeekKind) a.
(SeekRep s ~ Natural) =>
Seek 'RelSeek a -> Rec (Flap a) '[Const (Meta s)]
cmAlign Seek 'RelSeek a
s = Const (Meta s) a -> Rec (Flap a) '[Const (Meta s)]
forall (f :: * -> *) a. f a -> Rec (Flap a) '[f]
cm (Const (Meta s) a -> Rec (Flap a) '[Const (Meta s)])
-> Const (Meta s) a -> Rec (Flap a) '[Const (Meta s)]
forall a b. (a -> b) -> a -> b
$ Meta s -> Const (Meta s) a
forall {k} a (b :: k). a -> Const a b
Const (Meta s -> Const (Meta s) a) -> Meta s -> Const (Meta s) a
forall a b. (a -> b) -> a -> b
$ Meta :: forall (s :: SeekKind). Maybe (SeekRep s) -> Meta s
Align.Meta { mExpected :: Maybe (SeekRep s)
Align.mExpected = Seek 'RelSeek a -> Maybe Natural
forall (s :: SeekKind) a. Seek s a -> Maybe Natural
sAligned Seek 'RelSeek a
s }

cm :: f a -> Rec (Flap a) '[f]
cm :: forall (f :: * -> *) a. f a -> Rec (Flap a) '[f]
cm f a
fa = f a -> Flap a f
forall a (f :: * -> *). f a -> Flap a f
Flap f a
fa Flap a f -> Rec (Flap a) '[] -> Rec (Flap a) '[f]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec (Flap a) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil