-- editorconfig-checker-disable-file
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module UntypedPlutusCore.Core.Instance.Flat where

import PlutusCore.Flat
import PlutusCore.Pretty
import PlutusCore.Version qualified as PLC
import PlutusPrelude
import UntypedPlutusCore.Core.Instance.Pretty ()
import UntypedPlutusCore.Core.Type

import Control.Lens
import Control.Monad
import Data.Vector qualified as V
import Flat
import Flat.Decoder
import Flat.Encoder
import Flat.Encoder.Strict (sizeListWith)
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 UPLC]
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 UPLC 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.

** The BELOW table is for UPLC. **

| Data type        | Function          | Bit Width | Total | Used | Remaining |
|------------------|-------------------|-----------|-------|------|-----------|
| default builtins | encodeBuiltin     | 7         | 128   | 54   | 74        |
| Terms            | encodeTerm        | 4         | 16    | 10   | 6         |

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 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
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Term name uni fun ann
    -> Encoding
encodeTerm :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
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, 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, 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, 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, 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, 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
    Constr   ann
ann Word64
i [Term name uni fun ann]
es   -> Word8 -> Encoding
encodeTermTag Word8
8 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
<> Word64 -> Encoding
forall a. Flat a => a -> Encoding
encode Word64
i Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> (Term name uni fun ann -> Encoding)
-> [Term name uni fun ann] -> Encoding
forall t. (t -> Encoding) -> [t] -> Encoding
encodeListWith Term name uni fun ann -> Encoding
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm [Term name uni fun ann]
es
    Case     ann
ann Term name uni fun ann
arg Vector (Term name uni fun ann)
cs -> Word8 -> Encoding
encodeTermTag Word8
9 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, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm Term name uni fun ann
arg Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> (Term name uni fun ann -> Encoding)
-> [Term name uni fun ann] -> Encoding
forall t. (t -> Encoding) -> [t] -> Encoding
encodeListWith Term name uni fun ann -> Encoding
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm (Vector (Term name uni fun ann) -> [Term name uni fun ann]
forall a. Vector a -> [a]
V.toList Vector (Term name uni fun ann)
cs)

decodeTerm
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Version
    -> (fun -> Maybe String)
    -> Get (Term name uni fun ann)
decodeTerm :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Version -> (fun -> Maybe String) -> Get (Term name uni fun ann)
decodeTerm Version
version fun -> Maybe String
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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 a b. Get (a -> b) -> Get a -> Get b
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
            case fun -> Maybe String
builtinPred fun
fun of
                Maybe String
Nothing -> Term name uni fun ann -> Get (Term name uni fun ann)
forall a. a -> Get a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term name uni fun ann
t
                Just String
e  -> String -> Get (Term name uni fun ann)
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
e
        handleTerm Word8
8 = do
            Bool -> Get () -> Get ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Version
version Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
>= Version
PLC.plcVersion110) (Get () -> Get ()) -> Get () -> Get ()
forall a b. (a -> b) -> a -> b
$ String -> Get ()
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get ()) -> String -> Get ()
forall a b. (a -> b) -> a -> b
$ String
"'constr' is not allowed before version 1.1.0, this program has version: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Version -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Version -> Doc ann
pretty Version
version)
            ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr   (ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann)
-> Get ann
-> Get (Word64 -> [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 (Word64 -> [Term name uni fun ann] -> Term name uni fun ann)
-> Get Word64
-> Get ([Term name uni fun ann] -> Term name uni fun ann)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Word64
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 a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann) -> Get [Term name uni fun ann]
forall a. Get a -> Get [a]
decodeListWith Get (Term name uni fun ann)
go
        handleTerm Word8
9 = do
            Bool -> Get () -> Get ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Version
version Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
>= Version
PLC.plcVersion110) (Get () -> Get ()) -> Get () -> Get ()
forall a b. (a -> b) -> a -> b
$ String -> Get ()
forall a. String -> Get a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get ()) -> String -> Get ()
forall a b. (a -> b) -> a -> b
$ String
"'case' is not allowed before version 1.1.0, this program has version: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Version -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Version -> Doc ann
pretty Version
version)
            ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case     (ann
 -> Term name uni fun ann
 -> Vector (Term name uni fun ann)
 -> Term name uni fun ann)
-> Get ann
-> Get
     (Term name uni fun ann
      -> Vector (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
   -> Vector (Term name uni fun ann) -> Term name uni fun ann)
-> Get (Term name uni fun ann)
-> Get (Vector (Term name uni fun ann) -> Term name uni fun ann)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term name uni fun ann)
go Get (Vector (Term name uni fun ann) -> Term name uni fun ann)
-> Get (Vector (Term name uni fun ann))
-> Get (Term name uni fun ann)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Term name uni fun ann] -> Vector (Term name uni fun ann)
forall a. [a] -> Vector a
V.fromList ([Term name uni fun ann] -> Vector (Term name uni fun ann))
-> Get [Term name uni fun ann]
-> Get (Vector (Term name uni fun ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Term name uni fun ann) -> Get [Term name uni fun ann]
forall a. Get a -> Get [a]
decodeListWith Get (Term name uni fun ann)
go)
        handleTerm Word8
t = String -> Get (Term name uni fun ann)
forall a. String -> Get a
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
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Term name uni fun ann
    -> NumBits
    -> NumBits
sizeTerm :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
tm NumBits
sz =
  let
    sz' :: NumBits
sz' = NumBits
termTagWidth NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
sz
  in case Term name uni fun ann
tm of
    Var      ann
ann name
n      -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ name -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size name
n NumBits
sz'
    Delay    ann
ann Term name uni fun ann
t      -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t NumBits
sz'
    LamAbs   ann
ann name
n Term name uni fun ann
t    -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ name -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size name
n (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t NumBits
sz'
    Apply    ann
ann Term name uni fun ann
t Term name uni fun ann
t'   -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t' NumBits
sz'
    Constant ann
ann Some (ValueOf uni)
c      -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Some (ValueOf uni) -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Some (ValueOf uni)
c NumBits
sz'
    Force    ann
ann Term name uni fun ann
t      -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t NumBits
sz'
    Error    ann
ann        -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann NumBits
sz'
    Builtin  ann
ann fun
bn     -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ fun -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size fun
bn NumBits
sz'
    Constr   ann
ann Word64
i [Term name uni fun ann]
es   -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Word64 -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Word64
i (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ (Term name uni fun ann -> NumBits -> NumBits)
-> [Term name uni fun ann] -> NumBits -> NumBits
forall (t1 :: * -> *) t2 t3.
(Foldable t1, Num t2) =>
(t3 -> t2 -> t2) -> t1 t3 -> t2 -> t2
sizeListWith Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm [Term name uni fun ann]
es NumBits
sz'
    Case     ann
ann Term name uni fun ann
arg Vector (Term name uni fun ann)
cs -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
arg (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ (Term name uni fun ann -> NumBits -> NumBits)
-> [Term name uni fun ann] -> NumBits -> NumBits
forall (t1 :: * -> *) t2 t3.
(Foldable t1, Num t2) =>
(t3 -> t2 -> t2) -> t1 t3 -> t2 -> t2
sizeListWith Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm (Vector (Term name uni fun ann) -> [Term name uni fun ann]
forall a. Vector a -> [a]
V.toList Vector (Term name uni fun ann)
cs) NumBits
sz'

-- | An encoder for programs.
--
-- It is not easy to use this correctly with @flat@. The simplest thing
-- is to go via the instance for 'UnrestrictedProgram', which uses this
encodeProgram
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Program name uni fun ann
    -> Encoding
encodeProgram :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Program name uni fun ann -> Encoding
encodeProgram (Program ann
ann Version
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 -> Encoding
forall a. Flat a => a -> Encoding
encode Version
v 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, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> Encoding
encodeTerm Term name uni fun ann
t

decodeProgram
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => (fun -> Maybe String)
    -> Get (Program name uni fun ann)
decodeProgram :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
(fun -> Maybe String) -> Get (Program name uni fun ann)
decodeProgram fun -> Maybe String
builtinPred = do
  ann
ann <- Get ann
forall a. Flat a => Get a
decode
  Version
v <- Get Version
forall a. Flat a => Get a
decode
  ann -> Version -> Term name uni fun ann -> Program name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Version -> Term name uni fun ann -> Program name uni fun ann
Program ann
ann Version
v (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. Functor f => (a -> b) -> f a -> f b
<$> Version -> (fun -> Maybe String) -> Get (Term name uni fun ann)
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Version -> (fun -> Maybe String) -> Get (Term name uni fun ann)
decodeTerm Version
v fun -> Maybe String
builtinPred

sizeProgram
    :: forall name uni fun ann
    . ( Closed uni
    , uni `Everywhere` Flat
    , Flat fun
    , Flat ann
    , Flat name
    , Flat (Binder name)
    )
    => Program name uni fun ann
    -> NumBits
    -> NumBits
sizeProgram :: forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Program name uni fun ann -> NumBits -> NumBits
sizeProgram (Program ann
ann Version
v Term name uni fun ann
t) NumBits
sz = ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Version -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Version
v (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Term name uni fun ann -> NumBits -> NumBits
sizeTerm Term name uni fun ann
t NumBits
sz

-- | A program that can be serialized without any restrictions, e.g.
-- on the set of allowable builtins or term constructs. It is generally
-- safe to use this newtype for serializing, but it should only be used
-- for deserializing in tests.
newtype UnrestrictedProgram name uni fun ann = UnrestrictedProgram { forall name (uni :: * -> *) fun ann.
UnrestrictedProgram name uni fun ann -> Program name uni fun ann
unUnrestrictedProgram :: Program name uni fun ann }
    deriving newtype ((forall a b.
 (a -> b)
 -> UnrestrictedProgram name uni fun a
 -> UnrestrictedProgram name uni fun b)
-> (forall a b.
    a
    -> UnrestrictedProgram name uni fun b
    -> UnrestrictedProgram name uni fun a)
-> Functor (UnrestrictedProgram name uni fun)
forall a b.
a
-> UnrestrictedProgram name uni fun b
-> UnrestrictedProgram name uni fun a
forall a b.
(a -> b)
-> UnrestrictedProgram name uni fun a
-> UnrestrictedProgram name uni fun b
forall name (uni :: * -> *) fun a b.
a
-> UnrestrictedProgram name uni fun b
-> UnrestrictedProgram name uni fun a
forall name (uni :: * -> *) fun a b.
(a -> b)
-> UnrestrictedProgram name uni fun a
-> UnrestrictedProgram name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall name (uni :: * -> *) fun a b.
(a -> b)
-> UnrestrictedProgram name uni fun a
-> UnrestrictedProgram name uni fun b
fmap :: forall a b.
(a -> b)
-> UnrestrictedProgram name uni fun a
-> UnrestrictedProgram name uni fun b
$c<$ :: forall name (uni :: * -> *) fun a b.
a
-> UnrestrictedProgram name uni fun b
-> UnrestrictedProgram name uni fun a
<$ :: forall a b.
a
-> UnrestrictedProgram name uni fun b
-> UnrestrictedProgram name uni fun a
Functor)
makeWrapped ''UnrestrictedProgram

deriving newtype instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (UnrestrictedProgram name uni fun ann)

deriving via PrettyAny (UnrestrictedProgram name uni fun ann)
    instance DefaultPrettyPlcStrategy (UnrestrictedProgram name uni fun ann) =>
        PrettyBy PrettyConfigPlc (UnrestrictedProgram name uni fun ann)

deriving newtype instance
    (PrettyClassic name, PrettyUni uni, Pretty fun, Pretty ann)
    => PrettyBy (PrettyConfigClassic PrettyConfigName) (UnrestrictedProgram name uni fun ann)

deriving newtype instance
    (PrettyReadable name, PrettyUni uni, Pretty fun)
    => PrettyBy (PrettyConfigReadable PrettyConfigName) (UnrestrictedProgram name uni fun ann)

-- This instance does _not_ check for allowable builtins
instance ( Closed uni
         , uni `Everywhere` Flat
         , Flat fun
         , Flat ann
         , Flat name
         , Flat (Binder name)
         ) => Flat (UnrestrictedProgram name uni fun ann) where
    encode :: UnrestrictedProgram name uni fun ann -> Encoding
encode (UnrestrictedProgram Program name uni fun ann
p) = Program name uni fun ann -> Encoding
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Program name uni fun ann -> Encoding
encodeProgram Program name uni fun ann
p
    decode :: Get (UnrestrictedProgram name uni fun ann)
decode = Program name uni fun ann -> UnrestrictedProgram name uni fun ann
forall name (uni :: * -> *) fun ann.
Program name uni fun ann -> UnrestrictedProgram name uni fun ann
UnrestrictedProgram (Program name uni fun ann -> UnrestrictedProgram name uni fun ann)
-> Get (Program name uni fun ann)
-> Get (UnrestrictedProgram name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (fun -> Maybe String) -> Get (Program name uni fun ann)
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
(fun -> Maybe String) -> Get (Program name uni fun ann)
decodeProgram (Maybe String -> fun -> Maybe String
forall a b. a -> b -> a
const Maybe String
forall a. Maybe a
Nothing)

    size :: UnrestrictedProgram name uni fun ann -> NumBits -> NumBits
size (UnrestrictedProgram Program name uni fun ann
p) = Program name uni fun ann -> NumBits -> NumBits
forall name (uni :: * -> *) fun ann.
(Closed uni, Everywhere uni Flat, Flat fun, Flat ann, Flat name,
 Flat (Binder name)) =>
Program name uni fun ann -> NumBits -> NumBits
sizeProgram Program name uni fun ann
p