{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Data.Coders provides tools for writing 'EncCBOR' and 'DecCBOR' instances (see module
--   'Cardano.Binary') in an intuitive way that mirrors the way one constructs values of a
--   particular type. Advantages include:
--
-- 1. Book-keeping details neccesary to write correct instances are hidden from the user.
-- 2. Inverse 'EncCBOR' and 'DecCBOR' instances have visually similar definitions.
-- 3. Advanced instances involving sparse-encoding, compact-representation, and 'Annotator' instances are also supported.
--
-- A Guide to Visual inspection of Duality in Encode and Decode
--
-- 1. @(Sum c)@     and @(SumD c)@    are duals
-- 2. @(Rec c)@     and @(RecD c)@    are duals
-- 3. @(Keyed c)@   and @(KeyedD c)@  are duals
-- 4. @(OmitC x)@   and @(Emit x)@    are duals
-- 5. @(Omit p ..)@ and @(Emit x)@    are duals if (p x) is True
-- 6. @(To x)@      and @(From)@      are duals if (x::T) and (forall (y::T). isRight (roundTrip y))
-- 7. @(E enc x)@   and @(D dec)@     are duals if (forall x . isRight (roundTrip' enc dec x))
-- 6. @(ED d x)@    and @(DD f)@      are duals as long as d=(Dual enc dec) and (forall x . isRight (roundTrip' enc dec x))
-- 7. @(f !> x)@    and @(g <! y)@    are duals if (f and g are duals) and (x and y are duals)
--
-- Duality properties of @(Summands name decodeT)@ and @(SparseKeyed name (init::T) pick required)@ also exist
-- but are harder to describe succinctly.
module Cardano.Ledger.Binary.Encoding.Coders (
  -- * Creating encoders.

  --
  -- $Encoders
  Encode (..),
  (!>),
  encode,

  -- * Index types for well-formed Coders.

  --
  -- $Indexes
  runE, -- Used in testing
  encodeDual,

  -- * Containers, Combinators, Annotators

  --
  -- $Combinators
  encodeKeyedStrictMaybeWith,
  encodeKeyedStrictMaybe,
)
where

import Cardano.Ledger.Binary.Decoding.Coders (Density (Dense, Sparse), Wrapped (..))
import Cardano.Ledger.Binary.Decoding.DecCBOR (DecCBOR (..))
import Cardano.Ledger.Binary.Decoding.Decoder (Decoder)
import Cardano.Ledger.Binary.Encoding.EncCBOR (EncCBOR (encCBOR))
import Cardano.Ledger.Binary.Encoding.Encoder (
  Encoding,
  encodeListLen,
  encodeMapLen,
  encodeTag,
  encodeWord,
 )
import Cardano.Ledger.Binary.Group (EncCBORGroup (..))
import Data.Maybe.Strict (StrictMaybe (SJust, SNothing))

-- ====================================================================

-- ===============================================================================
-- Encode and Decode are typed data structures which specify encoders and decoders
-- for Algebraic data structures written in Haskell. They exploit types and count
-- the correct number fields in an encoding and decoding, which are automatically computed.
-- They are somewhat dual, and are designed so that visual inspection of a Encode and
-- its dual Decode can help the user conclude that the two are self-consistent.
-- They are also reusable abstractions that can be defined once, and then used many places.
--
-- (Encode t) is a data structure from which 3 things can be recovered
-- Given:    x :: Encode t
-- 1. get a value of type t
-- 2. get an Encoding for that value, which correctly encodes the number of "fields"
--    written to the ByteString. Care must still be taken that the Keys are correct.
-- 3. get a (MemoBytes t)
--
-- The advantage of using Encode with a MemoBytes, is we don't have to make a EncCBOR
-- instance. Instead the "instance" is spread amongst the pattern constuctors by using
-- (memoBytes encoding) in the where clause of the pattern contructor.
-- See some examples of this see the file Timelocks.hs
--

-- ===========================================================
-- The coders and the decoders as GADT datatypes
-- ===========================================================

-- Encoders

-- | A first-order domain specific langage for describing EncCBOR instances. Applying
--   the interpreter 'encode' to a well-typed @(Encode w T)@ always produces a valid encoding for @T@.
--   Constructing an Encode of type T is just like building a value of type T, applying a constructor
--   of @T@ to the correctly typed arguments. For example
--
-- @
-- data T = T Bool Word
--
-- instance EncCBOR T where
--   encCBOR (T b w) = encode (Rec T !> To b !> To w)
-- @
--
-- Note the similarity of
--
-- @(/T/ /b/ /w/)@ and @(/T/ $ /b/ $ /w/)@ and @(Rec /T/ !> To /b/ !> To /w/)@
--
-- Where ('!>') is the infx version of 'ApplyE' with the same infixity and precedence as ('$'). Note
-- how the constructor and each (component, field, argument) is labeled with one of the constructors
-- of 'Encode', and are combined with the application operator ('!>'). Using different constructors supports
-- different styles of encoding.
data Encode (w :: Wrapped) t where
  -- | Label the constructor of a Record-like datatype (one with exactly 1 constructor) as an Encode.
  Rec :: t -> Encode ('Closed 'Dense) t
  -- | Label one of the constructors of a sum datatype (one with multiple constructors) as an Encode
  Sum :: t -> Word -> Encode 'Open t
  -- | Label the constructor of a Record-like datatype as being encoded sparsely (storing only non-default values).
  Keyed :: t -> Encode ('Closed 'Sparse) t
  -- | Label an (component, field, argument) to be encoded using an existing EncCBOR instance.
  To :: EncCBOR a => a -> Encode ('Closed 'Dense) a
  -- | Label components, set of fields, or arguments to be encoded using an existing EncCBORGroup instance.
  ToGroup :: EncCBORGroup t => t -> Encode ('Closed 'Dense) t
  -- | Label an (component, field, argument) to be encoded using an existing EncCBOR instance.
  E :: (t -> Encoding) -> t -> Encode ('Closed 'Dense) t
  -- | Lift one Encode to another with a different type. Used to make a Functor instance of (Encode w).
  MapE :: (a -> b) -> Encode w a -> Encode w b
  -- | Skip over the  (component,field, argument), don't encode it at all (used in sparse encoding).
  OmitC :: t -> Encode w t
  -- | Precede the given encoding (in the produced bytes) with the given tag Word.
  Tag :: Word -> Encode ('Closed x) t -> Encode ('Closed x) t
  -- | Omit the  (component,field, argument) if the function is True, otherwise encode with the given encoding.
  Omit ::
    (t -> Bool) ->
    Encode ('Closed 'Sparse) t ->
    Encode ('Closed 'Sparse) t
  -- | Precede the encoding (in the produced bytes) with the key Word. Analagous to 'Tag', but lifts a 'Dense' encoding to a 'Sparse' encoding.
  Key :: Word -> Encode ('Closed 'Dense) t -> Encode ('Closed 'Sparse) t
  -- | Apply a functional encoding (arising from 'Rec' or 'Sum') to get (type wise) smaller encoding. A fully saturated chain of 'ApplyE' will be a complete encoding. See also '!>' which is infix 'ApplyE'.
  ApplyE :: Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t

-- The Wrapped index of ApplyE is determined by the index
-- at the bottom of its left spine. The choices are 'Open (Sum c tag),
-- ('Closed 'Dense) (Rec c), and ('Closed 'Sparse) (Keyed c).

infixl 4 !>

-- | Infix operator version of @ApplyE@. Has the same infxity and operator precedence as '$'
(!>) :: Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
Encode w (a -> t)
x !> :: forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Encode ('Closed r) a
y = forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
ApplyE Encode w (a -> t)
x Encode ('Closed r) a
y

runE :: Encode w t -> t
runE :: forall (w :: Wrapped) t. Encode w t -> t
runE (Sum t
cn Word
_) = t
cn
runE (Rec t
cn) = t
cn
runE (ApplyE Encode w (a -> t)
f Encode ('Closed r) a
x) = forall (w :: Wrapped) t. Encode w t -> t
runE Encode w (a -> t)
f (forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed r) a
x)
runE (To t
x) = t
x
runE (ToGroup t
x) = t
x
runE (E t -> Encoding
_ t
x) = t
x
runE (MapE a -> t
f Encode w a
x) = a -> t
f forall a b. (a -> b) -> a -> b
$ forall (w :: Wrapped) t. Encode w t -> t
runE Encode w a
x
runE (OmitC t
x) = t
x
runE (Omit t -> Bool
_ Encode ('Closed 'Sparse) t
x) = forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed 'Sparse) t
x
runE (Tag Word
_ Encode ('Closed x) t
x) = forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed x) t
x
runE (Key Word
_ Encode ('Closed 'Dense) t
x) = forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed 'Dense) t
x
runE (Keyed t
cn) = t
cn

gsize :: Encode w t -> Word
gsize :: forall (w :: Wrapped) t. Encode w t -> Word
gsize (Sum t
_ Word
_) = Word
0
gsize (Rec t
_) = Word
0
gsize (To t
_) = Word
1
gsize (ToGroup t
x) = forall a. EncCBORGroup a => a -> Word
listLen t
x
gsize (E t -> Encoding
_ t
_) = Word
1
gsize (MapE a -> t
_ Encode w a
x) = forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode w a
x
gsize (ApplyE Encode w (a -> t)
f Encode ('Closed r) a
x) = forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode w (a -> t)
f forall a. Num a => a -> a -> a
+ forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode ('Closed r) a
x
gsize (OmitC t
_) = Word
0
gsize (Omit t -> Bool
p Encode ('Closed 'Sparse) t
x) = if t -> Bool
p (forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed 'Sparse) t
x) then Word
0 else forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode ('Closed 'Sparse) t
x
gsize (Tag Word
_ Encode ('Closed x) t
_) = Word
1
gsize (Key Word
_ Encode ('Closed 'Dense) t
x) = forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode ('Closed 'Dense) t
x
gsize (Keyed t
_) = Word
0

-- | Translate a first-order @(Encode w d) domain specific langage program, into an 'Encoding' .
encode :: Encode w t -> Encoding
encode :: forall (w :: Wrapped) t. Encode w t -> Encoding
encode = forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
0
  where
    encodeCountPrefix :: Word -> Encode w t -> Encoding
    -- n is the number of fields we must write in the prefix.
    encodeCountPrefix :: forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
n (Sum t
_ Word
tag) = Word -> Encoding
encodeListLen (Word
n forall a. Num a => a -> a -> a
+ Word
1) forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
tag
    encodeCountPrefix Word
n (Keyed t
_) = Word -> Encoding
encodeMapLen Word
n
    encodeCountPrefix Word
n (Rec t
_) = Word -> Encoding
encodeListLen Word
n
    encodeCountPrefix Word
_ (To t
x) = forall a. EncCBOR a => a -> Encoding
encCBOR t
x
    encodeCountPrefix Word
_ (ToGroup t
x) = forall a. EncCBORGroup a => a -> Encoding
encCBORGroup t
x
    encodeCountPrefix Word
_ (E t -> Encoding
enc t
x) = t -> Encoding
enc t
x
    encodeCountPrefix Word
n (MapE a -> t
_ Encode w a
x) = forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
n Encode w a
x
    encodeCountPrefix Word
_ (OmitC t
_) = forall a. Monoid a => a
mempty
    encodeCountPrefix Word
n (Tag Word
tag Encode ('Closed x) t
x) = Word -> Encoding
encodeTag Word
tag forall a. Semigroup a => a -> a -> a
<> forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
n Encode ('Closed x) t
x
    encodeCountPrefix Word
n (Key Word
tag Encode ('Closed 'Dense) t
x) = Word -> Encoding
encodeWord Word
tag forall a. Semigroup a => a -> a -> a
<> forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
n Encode ('Closed 'Dense) t
x
    encodeCountPrefix Word
n (Omit t -> Bool
p Encode ('Closed 'Sparse) t
x) =
      if t -> Bool
p (forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed 'Sparse) t
x) then forall a. Monoid a => a
mempty else forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix Word
n Encode ('Closed 'Sparse) t
x
    encodeCountPrefix Word
n (ApplyE Encode w (a -> t)
ff Encode ('Closed r) a
xx) = forall (w :: Wrapped) t. Word -> Encode w t -> Encoding
encodeCountPrefix (Word
n forall a. Num a => a -> a -> a
+ forall (w :: Wrapped) t. Encode w t -> Word
gsize Encode ('Closed r) a
xx) Encode w (a -> t)
ff forall a. Semigroup a => a -> a -> a
<> forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed r) a
xx
      where
        encodeClosed :: Encode ('Closed d) t -> Encoding
        encodeClosed :: forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed (Rec t
_) = forall a. Monoid a => a
mempty
        encodeClosed (To t
x) = forall a. EncCBOR a => a -> Encoding
encCBOR t
x
        encodeClosed (ToGroup t
x) = forall a. EncCBORGroup a => a -> Encoding
encCBORGroup t
x
        encodeClosed (E t -> Encoding
enc t
x) = t -> Encoding
enc t
x
        encodeClosed (MapE a -> t
_ Encode ('Closed d) a
x) = forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed d) a
x
        encodeClosed (ApplyE Encode ('Closed d) (a -> t)
f Encode ('Closed r) a
x) = forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed d) (a -> t)
f forall a. Semigroup a => a -> a -> a
<> forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed r) a
x
        encodeClosed (OmitC t
_) = forall a. Monoid a => a
mempty
        encodeClosed (Omit t -> Bool
p Encode ('Closed 'Sparse) t
x) =
          if t -> Bool
p (forall (w :: Wrapped) t. Encode w t -> t
runE Encode ('Closed 'Sparse) t
x) then forall a. Monoid a => a
mempty else forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed 'Sparse) t
x
        encodeClosed (Tag Word
tag Encode ('Closed x) t
x) = Word -> Encoding
encodeTag Word
tag forall a. Semigroup a => a -> a -> a
<> forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed x) t
x
        encodeClosed (Key Word
tag Encode ('Closed 'Dense) t
x) = Word -> Encoding
encodeWord Word
tag forall a. Semigroup a => a -> a -> a
<> forall (d :: Density) t. Encode ('Closed d) t -> Encoding
encodeClosed Encode ('Closed 'Dense) t
x
        encodeClosed (Keyed t
_) = forall a. Monoid a => a
mempty

encodeKeyedStrictMaybeWith ::
  Word ->
  (a -> Encoding) ->
  StrictMaybe a ->
  Encode ('Closed 'Sparse) (StrictMaybe a)
encodeKeyedStrictMaybeWith :: forall a.
Word
-> (a -> Encoding)
-> StrictMaybe a
-> Encode ('Closed 'Sparse) (StrictMaybe a)
encodeKeyedStrictMaybeWith Word
_ a -> Encoding
_ StrictMaybe a
SNothing = forall t (w :: Wrapped). t -> Encode w t
OmitC forall a. StrictMaybe a
SNothing
encodeKeyedStrictMaybeWith Word
key a -> Encoding
enc (SJust a
x) = forall t.
Word -> Encode ('Closed 'Dense) t -> Encode ('Closed 'Sparse) t
Key Word
key (forall a b (w :: Wrapped). (a -> b) -> Encode w a -> Encode w b
MapE forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ forall t. (t -> Encoding) -> t -> Encode ('Closed 'Dense) t
E a -> Encoding
enc a
x)

encodeKeyedStrictMaybe ::
  EncCBOR a =>
  Word ->
  StrictMaybe a ->
  Encode ('Closed 'Sparse) (StrictMaybe a)
encodeKeyedStrictMaybe :: forall a.
EncCBOR a =>
Word -> StrictMaybe a -> Encode ('Closed 'Sparse) (StrictMaybe a)
encodeKeyedStrictMaybe Word
key = forall a.
Word
-> (a -> Encoding)
-> StrictMaybe a
-> Encode ('Closed 'Sparse) (StrictMaybe a)
encodeKeyedStrictMaybeWith Word
key forall a. EncCBOR a => a -> Encoding
encCBOR

-- | Use `encodeDual` and `Cardano.Ledger.Binary.Coders.decodeDual`, when you want to
-- guarantee that a type has both `EncCBOR` and `FromCBR` instances.
encodeDual :: forall t. (EncCBOR t, DecCBOR t) => t -> Encode ('Closed 'Dense) t
encodeDual :: forall t. (EncCBOR t, DecCBOR t) => t -> Encode ('Closed 'Dense) t
encodeDual = forall t. (t -> Encoding) -> t -> Encode ('Closed 'Dense) t
E forall a. EncCBOR a => a -> Encoding
encCBOR
  where
    -- Enforce DecCBOR constraint on t
    _decCBOR :: Decoder Any t
_decCBOR = forall a s. DecCBOR a => Decoder s a
decCBOR :: Decoder s t