{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE NamedFieldPuns       #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module UntypedPlutusCore.Core.Instance.Flat where

import UntypedPlutusCore.Core.Type

import PlutusCore.Flat
import PlutusCore.Pretty

import Data.Word (Word8)
import Flat
import Flat.Decoder
import Flat.Decoder.Types
import Flat.Encoder
import Universe

import Data.Primitive (Ptr)
import Data.Proxy
import Foreign (minusPtr)
import GHC.TypeLits

{-
The definitions in this file rely on some Flat instances defined for typed plutus core.
You can find those in PlutusCore.Flat.
-}

{- Note [Stable encoding of PLC]
READ THIS BEFORE TOUCHING ANYTHING IN THIS FILE

We need the encoding of PLC on the blockchain to be *extremely* stable. It *must not* change
arbitrarily, otherwise we'll be unable to read back old transactions and validate them.

Consequently we don't use the derivable instances of `Flat` for the PLC types that go
on the chain.

However, the instances in this file *are* constrained by instances for names, type names,
and annotations. What's to stop the instances for *those* changing, thus changing
the overall encoding on the chain?

The answer is that what goes on the chain is *always* a `Program TyName Name ()`. The instances
for `TyName` and `Name` are nailed down here, and the instance for `()` is standard.

However, having this flexibility allows us to encode e.g. PLC with substantial annotations
(like position information) in situation where the stability is *not* critical, such as
for testing.
-}

{- Note [Encoding/decoding constructor tags using Flat]
Flat saves space when compared to CBOR by allowing tags to use the minimum
number of bits required for their encoding.

This requires specialised encode/decode functions for each constructor
that encodes a different number of possibilities. Here is a list of the
tags and their used/available encoding possibilities.

| Data type       | Function          | Used | Available |
|-----------------|-------------------|------|-----------|
| Terms           | encodeTerm        | 8    | 16        |

For format stability we are manually assigning the tag values to the
constructors (and we do not use a generic algorithm that may change this order).

All encodings use the function `safeEncodeBits :: NumBits -> Word8 -> Encoding`, which encodes
at most 8 bits of data, and the first argument specifies how many bits from the 8
available are actually used. This function also checks the size of the `Word8`
argument at runtime.

Flat uses an extra function in its class definition called `size`. Since we want
to reserve some space for future data constructors and we don't want to have the
sizes desynchronised from the encoding and decoding functions we have manual
implementations for them (if they have any constructors reserved for future use).

By default, Flat does not use any space to serialise `()`.
-}

{- Note [Deserialization size limits]
In order to prevent people encoding copyright or otherwise illegal data on the chain, we restrict the
amount of space which can be used for a leaf serialized node to 64 bytes, and we enforce this during
deserialization.

We do this by asking Flat how far through the input it is before and after parsing a constant. That way
we can tell generically how much data was used to parse a constant.
-}

-- | Using 4 bits to encode term tags.
termTagWidth :: NumBits
termTagWidth :: NumBits
termTagWidth = NumBits
4

encodeTermTag :: Word8 -> Encoding
encodeTermTag :: Word8 -> Encoding
encodeTermTag = NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
termTagWidth

decodeTermTag :: Get Word8
decodeTermTag :: Get Word8
decodeTermTag = NumBits -> Get Word8
dBEBits8 NumBits
termTagWidth

encodeTerm
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , PrettyPlc (Term name uni fun ann)
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Term name uni fun ann
    -> Encoding
encodeTerm :: Term name uni fun ann -> Encoding
encodeTerm = \case
    Var      ann
ann name
n    -> Word8 -> Encoding
encodeTermTag Word8
0 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> name -> Encoding
forall a. Flat a => a -> Encoding
encode name
n
    Delay    ann
ann Term name uni fun ann
t    -> Word8 -> Encoding
encodeTermTag Word8
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t
    LamAbs   ann
ann name
n Term name uni fun ann
t  -> Word8 -> Encoding
encodeTermTag Word8
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Binder name -> Encoding
forall a. Flat a => a -> Encoding
encode (name -> Binder name
forall name. name -> Binder name
Binder name
n) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t
    Apply    ann
ann Term name uni fun ann
t Term name uni fun ann
t' -> Word8 -> Encoding
encodeTermTag Word8
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t'
    Constant ann
ann Some (ValueOf uni)
c    -> Word8 -> Encoding
encodeTermTag Word8
4 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Some (ValueOf uni) -> Encoding
forall a. Flat a => a -> Encoding
encode Some (ValueOf uni)
c
    Force    ann
ann Term name uni fun ann
t    -> Word8 -> Encoding
encodeTermTag Word8
5 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t
    Error    ann
ann      -> Word8 -> Encoding
encodeTermTag Word8
6 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann
    Builtin  ann
ann fun
bn   -> Word8 -> Encoding
encodeTermTag Word8
7 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> fun -> Encoding
forall a. Flat a => a -> Encoding
encode fun
bn

data SizeLimit = NoLimit | Limit Integer

decodeTerm
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , PrettyPlc (Term name uni fun ann)
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => SizeLimit
    -> Get (Term name uni fun ann)
decodeTerm :: SizeLimit -> Get (Term name uni fun ann)
decodeTerm SizeLimit
sizeLimit = Word8 -> Get (Term name uni fun ann)
forall a. (Eq a, Num a, Show a) => a -> Get (Term name uni fun ann)
go (Word8 -> Get (Term name uni fun ann))
-> Get Word8 -> Get (Term name uni fun ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8
decodeTermTag
    where go :: a -> Get (Term name uni fun ann)
go a
0 = ann -> name -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var      (ann -> name -> Term name uni fun ann)
-> Get ann -> Get (name -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (name -> Term name uni fun ann)
-> Get name -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get name
forall a. Flat a => Get a
decode
          go a
1 = ann -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay    (ann -> Term name uni fun ann -> Term name uni fun ann)
-> Get ann -> Get (Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Term name uni fun ann -> Term name uni fun ann)
-> Get (Term name uni fun ann) -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode
          go a
2 = ann -> name -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs   (ann -> name -> Term name uni fun ann -> Term name uni fun ann)
-> Get ann
-> Get (name -> Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (name -> Term name uni fun ann -> Term name uni fun ann)
-> Get name -> Get (Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Binder name -> name
forall name. Binder name -> name
unBinder (Binder name -> name) -> Get (Binder name) -> Get name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Binder name)
forall a. Flat a => Get a
decode) Get (Term name uni fun ann -> Term name uni fun ann)
-> Get (Term name uni fun ann) -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode
          go a
3 = ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply    (ann
 -> Term name uni fun ann
 -> Term name uni fun ann
 -> Term name uni fun ann)
-> Get ann
-> Get
     (Term name uni fun ann
      -> Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get
  (Term name uni fun ann
   -> Term name uni fun ann -> Term name uni fun ann)
-> Get (Term name uni fun ann)
-> Get (Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode Get (Term name uni fun ann -> Term name uni fun ann)
-> Get (Term name uni fun ann) -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode
          go a
4 = do
              ann
ann <- Get ann
forall a. Flat a => Get a
decode

              -- See Note [Deserialization size limits]
              Ptr Word8
posPre <- Get (Ptr Word8)
getCurPtr
              Some (ValueOf uni)
con <- Get (Some (ValueOf uni))
forall a. Flat a => Get a
decode
              Ptr Word8
posPost <- Get (Ptr Word8)
getCurPtr
              let usedBytes :: NumBits
usedBytes = Ptr Word8
posPost Ptr Word8 -> Ptr Word8 -> NumBits
forall a b. Ptr a -> Ptr b -> NumBits
`minusPtr` Ptr Word8
posPre

              let conNode :: Term name uni fun ann
                  conNode :: Term name uni fun ann
conNode = ann -> Some (ValueOf uni) -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
              case SizeLimit
sizeLimit of
                  SizeLimit
NoLimit -> Term name uni fun ann -> Get (Term name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun ann
conNode
                  Limit Integer
n ->
                      if NumBits -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral NumBits
usedBytes Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n
                      then String -> Get (Term name uni fun ann)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get (Term name uni fun ann))
-> String -> Get (Term name uni fun ann)
forall a b. (a -> b) -> a -> b
$ String
"Used more than " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" bytes decoding the constant: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Term name uni fun ann -> Doc Any
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcDef Term name uni fun ann
conNode)
                      else Term name uni fun ann -> Get (Term name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun ann
conNode
            where
                -- Get the pointer where flat is currently decoding from. Requires digging into the innards of flat a bit.
                getCurPtr :: Get (Ptr Word8)
                getCurPtr :: Get (Ptr Word8)
getCurPtr = (Ptr Word8 -> S -> IO (GetResult (Ptr Word8))) -> Get (Ptr Word8)
forall a. (Ptr Word8 -> S -> IO (GetResult a)) -> Get a
Get ((Ptr Word8 -> S -> IO (GetResult (Ptr Word8))) -> Get (Ptr Word8))
-> (Ptr Word8 -> S -> IO (GetResult (Ptr Word8)))
-> Get (Ptr Word8)
forall a b. (a -> b) -> a -> b
$ \Ptr Word8
_ s :: S
s@S{Ptr Word8
currPtr :: S -> Ptr Word8
currPtr :: Ptr Word8
currPtr} -> GetResult (Ptr Word8) -> IO (GetResult (Ptr Word8))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GetResult (Ptr Word8) -> IO (GetResult (Ptr Word8)))
-> GetResult (Ptr Word8) -> IO (GetResult (Ptr Word8))
forall a b. (a -> b) -> a -> b
$ S -> Ptr Word8 -> GetResult (Ptr Word8)
forall a. S -> a -> GetResult a
GetResult S
s Ptr Word8
currPtr
          go a
5 = ann -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force    (ann -> Term name uni fun ann -> Term name uni fun ann)
-> Get ann -> Get (Term name uni fun ann -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Term name uni fun ann -> Term name uni fun ann)
-> Get (Term name uni fun ann) -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode
          go a
6 = ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error    (ann -> Term name uni fun ann)
-> Get ann -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode
          go a
7 = ann -> fun -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin  (ann -> fun -> Term name uni fun ann)
-> Get ann -> Get (fun -> Term name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (fun -> Term name uni fun ann)
-> Get fun -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get fun
forall a. Flat a => Get a
decode
          go a
t = String -> Get (Term name uni fun ann)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get (Term name uni fun ann))
-> String -> Get (Term name uni fun ann)
forall a b. (a -> b) -> a -> b
$ String
"Unknown term constructor tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t

sizeTerm
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , PrettyPlc (Term name uni fun ann)
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Term name uni fun ann
    -> NumBits
    -> NumBits
sizeTerm :: Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
tm NumBits
sz = NumBits
termTagWidth NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ case Term name uni fun ann
tm of
    Var      ann
ann name
n    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ name -> NumBits
forall a. Flat a => a -> NumBits
getSize name
n
    Delay    ann
ann Term name uni fun ann
t    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t
    LamAbs   ann
ann name
n Term name uni fun ann
t  -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ name -> NumBits
forall a. Flat a => a -> NumBits
getSize name
n NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t
    Apply    ann
ann Term name uni fun ann
t Term name uni fun ann
t' -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t'
    Constant ann
ann Some (ValueOf uni)
c    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Some (ValueOf uni) -> NumBits
forall a. Flat a => a -> NumBits
getSize Some (ValueOf uni)
c
    Force    ann
ann Term name uni fun ann
t    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t
    Error    ann
ann      -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann
    Builtin  ann
ann fun
bn   -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ fun -> NumBits
forall a. Flat a => a -> NumBits
getSize fun
bn

-- | A newtype to indicate that the program should be serialized with size checks
-- for constants.
newtype WithSizeLimits (n :: Nat) a = WithSizeLimits a

instance ( Closed uni
         , uni `Everywhere` Flat
         , PrettyPlc (Term name uni fun ann)
         , Flat fun
         , Flat ann
         , Flat name
         , Flat (Binder name)
         ) => Flat (Term name uni fun ann) where
    encode :: Term name uni fun ann -> Encoding
encode = Term name uni fun ann -> Encoding
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm
    decode :: Get (Term name uni fun ann)
decode = SizeLimit -> Get (Term name uni fun ann)
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
SizeLimit -> Get (Term name uni fun ann)
decodeTerm SizeLimit
NoLimit
    size :: Term name uni fun ann -> NumBits -> NumBits
size = Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm

instance ( Closed uni
         , uni `Everywhere` Flat
         , PrettyPlc (Term name uni fun ann)
         , Flat fun
         , Flat ann
         , Flat name
         , Flat (Binder name)
         , KnownNat n
         ) => Flat (WithSizeLimits n (Term name uni fun ann)) where
    encode :: WithSizeLimits n (Term name uni fun ann) -> Encoding
encode (WithSizeLimits Term name uni fun ann
t) = Term name uni fun ann -> Encoding
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm Term name uni fun ann
t
    decode :: Get (WithSizeLimits n (Term name uni fun ann))
decode = Term name uni fun ann -> WithSizeLimits n (Term name uni fun ann)
forall (n :: Nat) a. a -> WithSizeLimits n a
WithSizeLimits (Term name uni fun ann -> WithSizeLimits n (Term name uni fun ann))
-> Get (Term name uni fun ann)
-> Get (WithSizeLimits n (Term name uni fun ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SizeLimit -> Get (Term name uni fun ann)
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
SizeLimit -> Get (Term name uni fun ann)
decodeTerm (Integer -> SizeLimit
Limit (Integer -> SizeLimit) -> Integer -> SizeLimit
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n
forall k (t :: k). Proxy t
Proxy @n)
    size :: WithSizeLimits n (Term name uni fun ann) -> NumBits -> NumBits
size (WithSizeLimits Term name uni fun ann
t) = Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat,
 PrettyPlc (Term name uni fun ann), Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t

instance ( Closed uni
         , uni `Everywhere` Flat
         , PrettyPlc (Term name uni fun ann)
         , Flat fun
         , Flat ann
         , Flat name
         , Flat (Binder name)
         ) => Flat (Program name uni fun ann) where
    encode :: Program name uni fun ann -> Encoding
encode (Program ann
ann Version ann
v Term name uni fun ann
t) = ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Version ann -> Encoding
forall a. Flat a => a -> Encoding
encode Version ann
v Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term name uni fun ann
t
    decode :: Get (Program name uni fun ann)
decode = ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
Program (ann
 -> Version ann
 -> Term name uni fun ann
 -> Program name uni fun ann)
-> Get ann
-> Get
     (Version ann -> Term name uni fun ann -> Program name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get
  (Version ann -> Term name uni fun ann -> Program name uni fun ann)
-> Get (Version ann)
-> Get (Term name uni fun ann -> Program name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Version ann)
forall a. Flat a => Get a
decode Get (Term name uni fun ann -> Program name uni fun ann)
-> Get (Term name uni fun ann) -> Get (Program name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
forall a. Flat a => Get a
decode
    size :: Program name uni fun ann -> NumBits -> NumBits
size (Program ann
a Version ann
v Term name uni fun ann
t) NumBits
n = NumBits
n NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
a NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Version ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Version ann
v NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term name uni fun ann
t

instance ( Closed uni
         , uni `Everywhere` Flat
         , PrettyPlc (Term name uni fun ann)
         , Flat fun
         , Flat ann
         , Flat name
         , Flat (Binder name)
         , KnownNat n
         ) => Flat (WithSizeLimits n (Program name uni fun ann)) where
    encode :: WithSizeLimits n (Program name uni fun ann) -> Encoding
encode (WithSizeLimits (Program ann
ann Version ann
v Term name uni fun ann
t)) = ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Version ann -> Encoding
forall a. Flat a => a -> Encoding
encode Version ann
v Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> WithSizeLimits n (Term name uni fun ann) -> Encoding
forall a. Flat a => a -> Encoding
encode (Term name uni fun ann -> WithSizeLimits n (Term name uni fun ann)
forall (n :: Nat) a. a -> WithSizeLimits n a
WithSizeLimits @n Term name uni fun ann
t)
    decode :: Get (WithSizeLimits n (Program name uni fun ann))
decode = do
        ann
ann <- Get ann
forall a. Flat a => Get a
decode
        Version ann
v <- Get (Version ann)
forall a. Flat a => Get a
decode
        (WithSizeLimits Term name uni fun ann
t) <- Flat (WithSizeLimits n (Term name uni fun ann)) =>
Get (WithSizeLimits n (Term name uni fun ann))
forall a. Flat a => Get a
decode @(WithSizeLimits n (Term name uni fun ann))
        WithSizeLimits n (Program name uni fun ann)
-> Get (WithSizeLimits n (Program name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WithSizeLimits n (Program name uni fun ann)
 -> Get (WithSizeLimits n (Program name uni fun ann)))
-> WithSizeLimits n (Program name uni fun ann)
-> Get (WithSizeLimits n (Program name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Program name uni fun ann
-> WithSizeLimits n (Program name uni fun ann)
forall (n :: Nat) a. a -> WithSizeLimits n a
WithSizeLimits (Program name uni fun ann
 -> WithSizeLimits n (Program name uni fun ann))
-> Program name uni fun ann
-> WithSizeLimits n (Program name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
Program ann
ann Version ann
v Term name uni fun ann
t
    size :: WithSizeLimits n (Program name uni fun ann) -> NumBits -> NumBits
size (WithSizeLimits Program name uni fun ann
p) = Program name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Program name uni fun ann
p