{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE NamedFieldPuns       #-}
{-# 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.Encoder
import Universe

{-
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 would like to
restrict the amount of data that can be controlled in an unrestricted fashion by the user. Fortunately,
most of the encoding does no allow much leeway for a user to control its content (when accounting for the
structure of the format itself). The main thing to worry about is bytestrings, but even there, the flat
encoding of bytestrings is a a sequence of 255-byte chunks. This is okay, since user-controlled data will
be broken up by the chunk metadata.
-}

-- | 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 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
    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 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
    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 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 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> 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'
    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 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
    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

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)
    )
    => (fun -> Bool)
    -> Get (Term name uni fun ann)
decodeTerm :: (fun -> Bool) -> Get (Term name uni fun ann)
decodeTerm fun -> Bool
builtinPred = Get (Term name uni fun ann)
go
    where
        go :: Get (Term name uni fun ann)
go = Word8 -> Get (Term name uni fun ann)
handleTerm (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
        handleTerm :: Word8 -> Get (Term name uni fun ann)
handleTerm Word8
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
        handleTerm Word8
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)
go
        handleTerm Word8
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)
go
        handleTerm Word8
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)
go 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)
go
        handleTerm Word8
4 = 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 -> Some (ValueOf uni) -> Term name uni fun ann)
-> Get ann -> Get (Some (ValueOf uni) -> 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 (Some (ValueOf uni) -> Term name uni fun ann)
-> Get (Some (ValueOf uni)) -> Get (Term name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Some (ValueOf uni))
forall a. Flat a => Get a
decode
        handleTerm Word8
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)
go
        handleTerm Word8
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
        handleTerm Word8
7 = do
            ann
ann <- Get ann
forall a. Flat a => Get a
decode
            fun
fun <- Get fun
forall a. Flat a => Get a
decode
            let t :: Term name uni fun ann
                t :: Term name uni fun ann
t = ann -> fun -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ann
ann fun
fun
            if fun -> Bool
builtinPred fun
fun
            then 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
t
            else 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
"Forbidden builtin function: " 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
t)
        handleTerm Word8
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]
++ Word8 -> String
forall a. Show a => a -> String
show Word8
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

decodeProgram
    :: 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)
    )
    => (fun -> Bool)
    -> Get (Program name uni fun ann)
decodeProgram :: (fun -> Bool) -> Get (Program name uni fun ann)
decodeProgram fun -> Bool
builtinPred = 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
<*> (fun -> Bool) -> 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)) =>
(fun -> Bool) -> Get (Term name uni fun ann)
decodeTerm fun -> Bool
builtinPred

{- Note [Deserialization on the chain]
As discussed in Note [Deserialization size limits], we want to limit how big constants are when deserializing.
But the 'Flat' instances for plain terms and programs provided here don't do that: they implement unrestricted deserialization.

In practice we use a specialized decoder for the on-chain decoding which calls 'decodeProgram' directly.
Possibly we should remove these instances in future and only have instances for newtypes that clearly communicate
the expected behaviour.
-}

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 = (fun -> Bool) -> 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)) =>
(fun -> Bool) -> Get (Term name uni fun ann)
decodeTerm (Bool -> fun -> Bool
forall a b. a -> b -> a
const Bool
True)
    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

-- This instance could probably be derived, but better to write it explicitly ourselves so we have control!
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

    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