{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Flat instances for Plutus Core types. Make sure to read Note [Stable
-- encoding of TPLC] and Note [Stable encoding of UPLC] before touching anything
-- in this file.
module PlutusCore.Flat
    ( safeEncodeBits
    ) where

import Codec.Extras.FlatViaSerialise
import PlutusCore.Core
import PlutusCore.Data (Data)
import PlutusCore.DeBruijn
import PlutusCore.Name.Unique

import Data.Proxy
import Flat
import Flat.Decoder
import Flat.Encoder
import PlutusPrelude
import Universe

{- Note [Stable encoding of TPLC]
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 TPLC 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 about Typed-PLC and not UPLC. See `UntypedPlutusCore.Core.Instance.Flat`**

| Data type        | Function          | Bit Width | Total | Used | Remaining |
|------------------|-------------------|-----------|-------|------|-----------|
| default builtins | encodeBuiltin     | 7         | 128   | 54   | 74        |
| Kinds            | encodeKind        | 1         | 2     | 2    | 0         |
| Types            | encodeType        | 3         | 8     | 7    | 1         |
| Terms            | encodeTerm        | 4         | 16    | 12   | 4         |

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 [DeBruijn Index serialization]

Back in the days, `Index` was a Natural and we flat (de)-serialized it via Natural.
Later `Index` was changed to Word64 (for performance reasons):
its flat encoding remained via Natural,
but its decoding was changed to a *custom* Word64 decoder.

Why custom decoder: there was a bug in Word64 decoder of flat versions <0.5.2 and
fixed in flat>=0.5.2.

We are now running flat>=0.6, so we switch to the non-custom, fixed flat Word64 decoder.

Since we are there, we also switch the encoder of Index from the Natural encoder
to Word64 encoder. This encoding change only breaks client-code and not nodes' behavior:
the script would just fail earlier at encoding phase (in the client's software)
than the later decoding phase (when trying to send the encoded script to the node network and
only get back a decoding error, aka phase-1 validation error).
This phase-1 validation is in place both for normal (locked scripts) and for inline scripts,
so the nodes' behavior does not change.
-}

safeEncodeBits :: NumBits -> Word8 -> Encoding
safeEncodeBits :: NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
maxBits Word8
v =
  if Word8
2 Word8 -> NumBits -> Word8
forall a b. (Num a, Integral b) => a -> b -> a
^ NumBits
maxBits Word8 -> Word8 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word8
v
  then [Char] -> Encoding
forall a. HasCallStack => [Char] -> a
error ([Char] -> Encoding) -> [Char] -> Encoding
forall a b. (a -> b) -> a -> b
$ [Char]
"Overflow detected, cannot fit "
               [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Word8 -> [Char]
forall a. Show a => a -> [Char]
show Word8
v [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" in " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> NumBits -> [Char]
forall a. Show a => a -> [Char]
show NumBits
maxBits [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" bits."
  else NumBits -> Word8 -> Encoding
eBits NumBits
maxBits Word8
v

constantWidth :: NumBits
constantWidth :: NumBits
constantWidth = NumBits
4

encodeConstant :: Word8 -> Encoding
encodeConstant :: Word8 -> Encoding
encodeConstant = NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
constantWidth

decodeConstant :: Get Word8
decodeConstant :: Get Word8
decodeConstant = NumBits -> Get Word8
dBEBits8 NumBits
constantWidth

deriving via FlatViaSerialise Data instance Flat Data

decodeKindedUniFlat :: Closed uni => Get (SomeTypeIn (Kinded uni))
decodeKindedUniFlat :: forall (uni :: * -> *). Closed uni => Get (SomeTypeIn (Kinded uni))
decodeKindedUniFlat =
    Maybe (SomeTypeIn (Kinded uni)) -> Get (SomeTypeIn (Kinded uni))
forall {m :: * -> *} {a}. MonadFail m => Maybe a -> m a
go (Maybe (SomeTypeIn (Kinded uni)) -> Get (SomeTypeIn (Kinded uni)))
-> ([Word8] -> Maybe (SomeTypeIn (Kinded uni)))
-> [Word8]
-> Get (SomeTypeIn (Kinded uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NumBits] -> Maybe (SomeTypeIn (Kinded uni))
forall (uni :: * -> *).
Closed uni =>
[NumBits] -> Maybe (SomeTypeIn (Kinded uni))
decodeKindedUni ([NumBits] -> Maybe (SomeTypeIn (Kinded uni)))
-> ([Word8] -> [NumBits])
-> [Word8]
-> Maybe (SomeTypeIn (Kinded uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word8 -> NumBits) -> [Word8] -> [NumBits]
forall a b. (a -> b) -> [a] -> [b]
map (Word8 -> NumBits
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Word8 -> Int)
        ([Word8] -> Get (SomeTypeIn (Kinded uni)))
-> Get [Word8] -> Get (SomeTypeIn (Kinded uni))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8 -> Get [Word8]
forall a. Get a -> Get [a]
decodeListWith Get Word8
decodeConstant
        where
        go :: Maybe a -> m a
go Maybe a
Nothing    = [Char] -> m a
forall a. [Char] -> m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Failed to decode a universe"
        go (Just a
uni) = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
uni

-- See Note [The G, the Tag and the Auto].
instance Closed uni => Flat (SomeTypeIn uni) where
    encode :: SomeTypeIn uni -> Encoding
encode (SomeTypeIn uni (Esc a)
uni) =
      (Word8 -> Encoding) -> [Word8] -> Encoding
forall t. (t -> Encoding) -> [t] -> Encoding
encodeListWith Word8 -> Encoding
encodeConstant ([Word8] -> Encoding)
-> ([NumBits] -> [Word8]) -> [NumBits] -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        (NumBits -> Word8) -> [NumBits] -> [Word8]
forall a b. (a -> b) -> [a] -> [b]
map (NumBits -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int -> Word8) ([NumBits] -> Encoding) -> [NumBits] -> Encoding
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> [NumBits]
forall a. uni a -> [NumBits]
forall (uni :: * -> *) a. Closed uni => uni a -> [NumBits]
encodeUni uni (Esc a)
uni

    decode :: Get (SomeTypeIn uni)
decode = Get (SomeTypeIn (Kinded uni))
forall (uni :: * -> *). Closed uni => Get (SomeTypeIn (Kinded uni))
decodeKindedUniFlat Get (SomeTypeIn (Kinded uni))
-> (SomeTypeIn (Kinded uni) -> SomeTypeIn uni)
-> Get (SomeTypeIn uni)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(SomeTypeIn (Kinded uni (Esc a)
uni)) -> uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn uni (Esc a)
uni

    -- Encode a view of the universe, not the universe itself.
    size :: SomeTypeIn uni -> NumBits -> NumBits
size (SomeTypeIn uni (Esc a)
uni) NumBits
acc =
      NumBits
acc NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+
      [NumBits] -> NumBits
forall a. [a] -> NumBits
forall (t :: * -> *) a. Foldable t => t a -> NumBits
length (uni (Esc a) -> [NumBits]
forall a. uni a -> [NumBits]
forall (uni :: * -> *) a. Closed uni => uni a -> [NumBits]
encodeUni uni (Esc a)
uni) NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
* (NumBits
1 NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
constantWidth) NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ -- List Cons (1 bit) + constant
      NumBits
1 -- List Nil (1 bit)

-- See Note [The G, the Tag and the Auto].
instance (Closed uni, uni `Everywhere` Flat) => Flat (Some (ValueOf uni)) where
    encode :: Some (ValueOf uni) -> Encoding
encode (Some (ValueOf uni (Esc a)
uni a
x)) = SomeTypeIn uni -> Encoding
forall a. Flat a => a -> Encoding
encode (uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn uni (Esc a)
uni) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Proxy Flat -> uni (Esc a) -> (Flat a => Encoding) -> Encoding
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Flat) uni (Esc a)
uni (a -> Encoding
forall a. Flat a => a -> Encoding
encode a
x)

    decode :: Get (Some (ValueOf uni))
decode =
        forall (uni :: * -> *). Closed uni => Get (SomeTypeIn (Kinded uni))
decodeKindedUniFlat @uni Get (SomeTypeIn (Kinded uni))
-> (SomeTypeIn (Kinded uni) -> Get (Some (ValueOf uni)))
-> Get (Some (ValueOf uni))
forall a b. Get a -> (a -> Get b) -> Get b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(SomeTypeIn (Kinded uni (Esc a)
uni)) ->
            -- See Note [Decoding universes].
            case uni (Esc a) -> Maybe (k :~: *)
forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar uni (Esc a)
uni of
                Maybe (k :~: *)
Nothing   -> [Char] -> Get (Some (ValueOf uni))
forall a. [Char] -> Get a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"A non-star type can't have a value to decode"
                Just k :~: *
Refl -> ValueOf uni a -> Some (ValueOf uni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf uni a -> Some (ValueOf uni))
-> (a -> ValueOf uni a) -> a -> Some (ValueOf uni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> a -> ValueOf uni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf uni (Esc a)
uni (Esc a)
uni (a -> Some (ValueOf uni)) -> Get a -> Get (Some (ValueOf uni))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Flat -> uni (Esc a) -> (Flat a => Get a) -> Get a
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Flat) uni (Esc a)
uni (Esc a)
uni Get a
Flat a => Get a
forall a. Flat a => Get a
decode

    -- We need to get the flat instance in scope.
    size :: Some (ValueOf uni) -> NumBits -> NumBits
size (Some (ValueOf uni (Esc a)
uni a
x)) NumBits
acc = SomeTypeIn uni -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size (uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn uni (Esc a)
uni) NumBits
acc
                                        NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Proxy Flat -> uni (Esc a) -> (Flat a => NumBits) -> NumBits
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere uni constr =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Flat) uni (Esc a)
uni (a -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size a
x NumBits
0)

deriving newtype instance Flat Unique -- via int

instance Flat Name where
    encode :: Name -> Encoding
encode (Name Text
txt Unique
u) = Text -> Encoding
forall a. Flat a => a -> Encoding
encode Text
txt Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Unique -> Encoding
forall a. Flat a => a -> Encoding
encode Unique
u
    decode :: Get Name
decode = Text -> Unique -> Name
Name (Text -> Unique -> Name) -> Get Text -> Get (Unique -> Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Text
forall a. Flat a => Get a
decode Get (Unique -> Name) -> Get Unique -> Get Name
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Unique
forall a. Flat a => Get a
decode

deriving newtype instance Flat TyName -- via Name

instance Flat Version where
    encode :: Version -> Encoding
encode (Version Natural
n Natural
n' Natural
n'') = Natural -> Encoding
forall a. Flat a => a -> Encoding
encode Natural
n Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Natural -> Encoding
forall a. Flat a => a -> Encoding
encode Natural
n' Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Natural -> Encoding
forall a. Flat a => a -> Encoding
encode Natural
n''
    decode :: Get Version
decode = Natural -> Natural -> Natural -> Version
Version (Natural -> Natural -> Natural -> Version)
-> Get Natural -> Get (Natural -> Natural -> Version)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Natural
forall a. Flat a => Get a
decode Get (Natural -> Natural -> Version)
-> Get Natural -> Get (Natural -> Version)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Natural
forall a. Flat a => Get a
decode Get (Natural -> Version) -> Get Natural -> Get Version
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Natural
forall a. Flat a => Get a
decode

-- | Use 1 bit to encode kind tags.
kindTagWidth :: NumBits
kindTagWidth :: NumBits
kindTagWidth = NumBits
1

encodeKind :: Word8 -> Encoding
encodeKind :: Word8 -> Encoding
encodeKind = NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
kindTagWidth

decodeKind :: Get Word8
decodeKind :: Get Word8
decodeKind = NumBits -> Get Word8
dBEBits8 NumBits
kindTagWidth

instance Flat ann => Flat (Kind ann) where
    encode :: Kind ann -> Encoding
encode = \case
        Type ann
ann           -> Word8 -> Encoding
encodeKind Word8
0 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann
        KindArrow ann
ann Kind ann
k Kind ann
k' -> Word8 -> Encoding
encodeKind 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
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
k  Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
k'

    decode :: Get (Kind ann)
decode = Word8 -> Get (Kind ann)
forall {a} {a}. (Eq a, Num a, Flat a) => a -> Get (Kind a)
go (Word8 -> Get (Kind ann)) -> Get Word8 -> Get (Kind ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8
decodeKind
        where go :: a -> Get (Kind a)
go a
0 = a -> Kind a
forall ann. ann -> Kind ann
Type      (a -> Kind a) -> Get a -> Get (Kind a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode
              go a
1 = a -> Kind a -> Kind a -> Kind a
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow (a -> Kind a -> Kind a -> Kind a)
-> Get a -> Get (Kind a -> Kind a -> Kind a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Kind a -> Kind a -> Kind a)
-> Get (Kind a) -> Get (Kind a -> Kind a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind a)
forall a. Flat a => Get a
decode Get (Kind a -> Kind a) -> Get (Kind a) -> Get (Kind a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind a)
forall a. Flat a => Get a
decode
              go a
_ = [Char] -> Get (Kind a)
forall a. [Char] -> Get a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Failed to decode Kind ()"

    size :: Kind ann -> NumBits -> NumBits
size Kind ann
tm NumBits
sz =
      let
        sz' :: NumBits
sz' = NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
kindTagWidth
      in case Kind ann
tm of
        Type ann
ann           -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann NumBits
sz'
        KindArrow ann
ann Kind ann
k Kind ann
k' -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Kind ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Kind ann
k (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Kind ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Kind ann
k' NumBits
sz'

-- | Use 3 bits to encode type tags.
typeTagWidth :: NumBits
typeTagWidth :: NumBits
typeTagWidth = NumBits
3

encodeType :: Word8 -> Encoding
encodeType :: Word8 -> Encoding
encodeType = NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
typeTagWidth

decodeType :: Get Word8
decodeType :: Get Word8
decodeType = NumBits -> Get Word8
dBEBits8 NumBits
typeTagWidth

instance (Closed uni, Flat ann, Flat tyname) => Flat (Type tyname uni ann) where
    encode :: Type tyname uni ann -> Encoding
encode = \case
        TyVar     ann
ann tyname
tn      -> Word8 -> Encoding
encodeType 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
<> tyname -> Encoding
forall a. Flat a => a -> Encoding
encode tyname
tn
        TyFun     ann
ann Type tyname uni ann
t Type tyname uni ann
t'    -> Word8 -> Encoding
encodeType 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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t'
        TyIFix    ann
ann Type tyname uni ann
pat Type tyname uni ann
arg -> Word8 -> Encoding
encodeType 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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
pat Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
arg
        TyForall  ann
ann tyname
tn Kind ann
k Type tyname uni ann
t  -> Word8 -> Encoding
encodeType 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
<> tyname -> Encoding
forall a. Flat a => a -> Encoding
encode tyname
tn  Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
k Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t
        TyBuiltin ann
ann SomeTypeIn uni
con     -> Word8 -> Encoding
encodeType 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
<> SomeTypeIn uni -> Encoding
forall a. Flat a => a -> Encoding
encode SomeTypeIn uni
con
        TyLam     ann
ann tyname
n Kind ann
k Type tyname uni ann
t   -> Word8 -> Encoding
encodeType 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
<> tyname -> Encoding
forall a. Flat a => a -> Encoding
encode tyname
n   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
k Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t
        TyApp     ann
ann Type tyname uni ann
t Type tyname uni ann
t'    -> Word8 -> Encoding
encodeType Word8
6 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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
t'
        -- Note that this relies on the instance for lists. We shouldn't use this in the
        -- serious on-chain version but it's okay here.
        TySOP    ann
ann [[Type tyname uni ann]]
tyls     -> Word8 -> Encoding
encodeType 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
<> [[Type tyname uni ann]] -> Encoding
forall a. Flat a => a -> Encoding
encode [[Type tyname uni ann]]
tyls

    decode :: Get (Type tyname uni ann)
decode = Word8 -> Get (Type tyname uni ann)
forall {a} {a} {a} {uni :: * -> *}.
(Eq a, Num a, Flat a, Flat a, Closed uni) =>
a -> Get (Type a uni a)
go (Word8 -> Get (Type tyname uni ann))
-> Get Word8 -> Get (Type tyname uni ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8
decodeType
        where go :: a -> Get (Type a uni a)
go a
0 = a -> a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar     (a -> a -> Type a uni a) -> Get a -> Get (a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (a -> Type a uni a) -> Get a -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode
              go a
1 = a -> Type a uni a -> Type a uni a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun     (a -> Type a uni a -> Type a uni a -> Type a uni a)
-> Get a -> Get (Type a uni a -> Type a uni a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode
              go a
2 = a -> Type a uni a -> Type a uni a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix    (a -> Type a uni a -> Type a uni a -> Type a uni a)
-> Get a -> Get (Type a uni a -> Type a uni a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode
              go a
3 = a -> a -> Kind a -> Type a uni a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall  (a -> a -> Kind a -> Type a uni a -> Type a uni a)
-> Get a -> Get (a -> Kind a -> Type a uni a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (a -> Kind a -> Type a uni a -> Type a uni a)
-> Get a -> Get (Kind a -> Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode Get (Kind a -> Type a uni a -> Type a uni a)
-> Get (Kind a) -> Get (Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind a)
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode
              go a
4 = a -> SomeTypeIn uni -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin (a -> SomeTypeIn uni -> Type a uni a)
-> Get a -> Get (SomeTypeIn uni -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (SomeTypeIn uni -> Type a uni a)
-> Get (SomeTypeIn uni) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (SomeTypeIn uni)
forall a. Flat a => Get a
decode
              go a
5 = a -> a -> Kind a -> Type a uni a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam     (a -> a -> Kind a -> Type a uni a -> Type a uni a)
-> Get a -> Get (a -> Kind a -> Type a uni a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (a -> Kind a -> Type a uni a -> Type a uni a)
-> Get a -> Get (Kind a -> Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode Get (Kind a -> Type a uni a -> Type a uni a)
-> Get (Kind a) -> Get (Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind a)
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode
              go a
6 = a -> Type a uni a -> Type a uni a -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp     (a -> Type a uni a -> Type a uni a -> Type a uni a)
-> Get a -> Get (Type a uni a -> Type a uni a -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a -> Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode Get (Type a uni a -> Type a uni a)
-> Get (Type a uni a) -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni a)
forall a. Flat a => Get a
decode
              go a
7 = a -> [[Type a uni a]] -> Type a uni a
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP     (a -> [[Type a uni a]] -> Type a uni a)
-> Get a -> Get ([[Type a uni a]] -> Type a uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get ([[Type a uni a]] -> Type a uni a)
-> Get [[Type a uni a]] -> Get (Type a uni a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get [[Type a uni a]]
forall a. Flat a => Get a
decode
              go a
_ = [Char] -> Get (Type a uni a)
forall a. [Char] -> Get a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Failed to decode Type TyName ()"

    size :: Type tyname uni ann -> NumBits -> NumBits
size Type tyname uni ann
tm NumBits
sz =
      let
        sz' :: NumBits
sz' = NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
typeTagWidth
      in case Type tyname uni ann
tm of
        TyVar     ann
ann tyname
tn      -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ tyname -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size tyname
tn NumBits
sz'
        TyFun     ann
ann Type tyname uni ann
t Type tyname uni 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t' NumBits
sz'
        TyIFix    ann
ann Type tyname uni ann
pat Type tyname uni ann
arg -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
pat (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
arg NumBits
sz'
        TyForall  ann
ann tyname
tn Kind ann
k Type tyname uni 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
$ tyname -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size tyname
tn (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Kind ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Kind ann
k (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t NumBits
sz'
        TyBuiltin ann
ann SomeTypeIn uni
con     -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ SomeTypeIn uni -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size SomeTypeIn uni
con NumBits
sz'
        TyLam     ann
ann tyname
n Kind ann
k Type tyname uni 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
$ tyname -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size tyname
n (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Kind ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Kind ann
k (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t NumBits
sz'
        TyApp     ann
ann Type tyname uni ann
t Type tyname uni 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
t' NumBits
sz'
        TySOP     ann
ann [[Type tyname uni ann]]
tyls    -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ [[Type tyname uni ann]] -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size [[Type tyname uni ann]]
tyls NumBits
sz'

termTagWidth :: NumBits
termTagWidth :: NumBits
termTagWidth = NumBits
4

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

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

instance ( Closed uni
         , uni `Everywhere` Flat
         , Flat fun
         , Flat ann
         , Flat tyname
         , Flat name
         ) => Flat (Term tyname name uni fun ann) where
    encode :: Term tyname name uni fun ann -> Encoding
encode = \case
        Var      ann
ann name
n         -> Word8 -> Encoding
encodeTerm 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
        TyAbs    ann
ann tyname
tn Kind ann
k Term tyname name uni fun ann
t    -> Word8 -> Encoding
encodeTerm 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
<> tyname -> Encoding
forall a. Flat a => a -> Encoding
encode tyname
tn  Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
k   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t
        LamAbs   ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t    -> Word8 -> Encoding
encodeTerm 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
<> name -> Encoding
forall a. Flat a => a -> Encoding
encode name
n   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
ty  Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t
        Apply    ann
ann Term tyname name uni fun ann
t Term tyname name uni fun ann
t'      -> Word8 -> Encoding
encodeTerm 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 tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t'
        Constant ann
ann Some (ValueOf uni)
c         -> Word8 -> Encoding
encodeTerm 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
        TyInst   ann
ann Term tyname name uni fun ann
t Type tyname uni ann
ty      -> Word8 -> Encoding
encodeTerm 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 tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t   Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
ty
        Unwrap   ann
ann Term tyname name uni fun ann
t         -> Word8 -> Encoding
encodeTerm Word8
6 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 tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t
        IWrap    ann
ann Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
t -> Word8 -> Encoding
encodeTerm 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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
pat Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
arg Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t
        Error    ann
ann Type tyname uni ann
ty        -> Word8 -> Encoding
encodeTerm 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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
ty
        Builtin  ann
ann fun
bn        -> Word8 -> Encoding
encodeTerm 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
<> fun -> Encoding
forall a. Flat a => a -> Encoding
encode fun
bn
        Constr   ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es   ->
          Word8 -> Encoding
encodeTerm Word8
10
          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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
ty
          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 tyname name uni fun ann] -> Encoding
forall a. Flat a => a -> Encoding
encode [Term tyname name uni fun ann]
es
        Case     ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs ->
          Word8 -> Encoding
encodeTerm Word8
11
          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
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
ty
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
arg
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [Term tyname name uni fun ann] -> Encoding
forall a. Flat a => a -> Encoding
encode [Term tyname name uni fun ann]
cs

    decode :: Get (Term tyname name uni fun ann)
decode = Word8 -> Get (Term tyname name uni fun ann)
forall {uni :: * -> *} {a} {a} {a} {tyname} {fun}.
(Everywhere uni Flat, Eq a, Num a, Closed uni, Flat a, Flat a,
 Flat tyname, Flat fun) =>
a -> Get (Term tyname a uni fun a)
go (Word8 -> Get (Term tyname name uni fun ann))
-> Get Word8 -> Get (Term tyname name uni fun ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8
decodeTerm
        where go :: a -> Get (Term tyname a uni fun a)
go a
0  = a -> a -> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var      (a -> a -> Term tyname a uni fun a)
-> Get a -> Get (a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (a -> Term tyname a uni fun a)
-> Get a -> Get (Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode
              go a
1  = a
-> tyname
-> Kind a
-> Term tyname a uni fun a
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs    (a
 -> tyname
 -> Kind a
 -> Term tyname a uni fun a
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (tyname
      -> Kind a -> Term tyname a uni fun a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (tyname
   -> Kind a -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get tyname
-> Get
     (Kind a -> Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get tyname
forall a. Flat a => Get a
decode Get (Kind a -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Kind a)
-> Get (Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind a)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a) -> Get (Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode
              go a
2  = a
-> a
-> Type tyname uni a
-> Term tyname a uni fun a
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs   (a
 -> a
 -> Type tyname uni a
 -> Term tyname a uni fun a
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (a
      -> Type tyname uni a
      -> Term tyname a uni fun a
      -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (a
   -> Type tyname uni a
   -> Term tyname a uni fun a
   -> Term tyname a uni fun a)
-> Get a
-> Get
     (Type tyname uni a
      -> Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode Get
  (Type tyname uni a
   -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Type tyname uni a)
-> Get (Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a) -> Get (Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode
              go a
3  = a
-> Term tyname a uni fun a
-> Term tyname a uni fun a
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply    (a
 -> Term tyname a uni fun a
 -> Term tyname a uni fun a
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (Term tyname a uni fun a
      -> Term tyname a uni fun a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (Term tyname a uni fun a
   -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a)
-> Get (Term tyname a uni fun a -> Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a) -> Get (Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode
              go a
4  = a -> Some (ValueOf uni) -> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant (a -> Some (ValueOf uni) -> Term tyname a uni fun a)
-> Get a -> Get (Some (ValueOf uni) -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Some (ValueOf uni) -> Term tyname a uni fun a)
-> Get (Some (ValueOf uni)) -> Get (Term tyname a uni fun a)
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
              go a
5  = a
-> Term tyname a uni fun a
-> Type tyname uni a
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst   (a
 -> Term tyname a uni fun a
 -> Type tyname uni a
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (Term tyname a uni fun a
      -> Type tyname uni a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (Term tyname a uni fun a
   -> Type tyname uni a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a)
-> Get (Type tyname uni a -> Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode Get (Type tyname uni a -> Term tyname a uni fun a)
-> Get (Type tyname uni a) -> Get (Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode
              go a
6  = a -> Term tyname a uni fun a -> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap   (a -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get a
-> Get (Term tyname a uni fun a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a) -> Get (Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode
              go a
7  = a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname a uni fun a
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap    (a
 -> Type tyname uni a
 -> Type tyname uni a
 -> Term tyname a uni fun a
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (Type tyname uni a
      -> Type tyname uni a
      -> Term tyname a uni fun a
      -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (Type tyname uni a
   -> Type tyname uni a
   -> Term tyname a uni fun a
   -> Term tyname a uni fun a)
-> Get (Type tyname uni a)
-> Get
     (Type tyname uni a
      -> Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode Get
  (Type tyname uni a
   -> Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Type tyname uni a)
-> Get (Term tyname a uni fun a -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun a -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a) -> Get (Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode
              go a
8  = a -> Type tyname uni a -> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error    (a -> Type tyname uni a -> Term tyname a uni fun a)
-> Get a -> Get (Type tyname uni a -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (Type tyname uni a -> Term tyname a uni fun a)
-> Get (Type tyname uni a) -> Get (Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode
              go a
9  = a -> fun -> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin  (a -> fun -> Term tyname a uni fun a)
-> Get a -> Get (fun -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get (fun -> Term tyname a uni fun a)
-> Get fun -> Get (Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get fun
forall a. Flat a => Get a
decode
              go a
10 = a
-> Type tyname uni a
-> Word64
-> [Term tyname a uni fun a]
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr   (a
 -> Type tyname uni a
 -> Word64
 -> [Term tyname a uni fun a]
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (Type tyname uni a
      -> Word64 -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (Type tyname uni a
   -> Word64 -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
-> Get (Type tyname uni a)
-> Get
     (Word64 -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode Get
  (Word64 -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
-> Get Word64
-> Get ([Term tyname a uni fun a] -> Term tyname a uni fun a)
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 tyname a uni fun a] -> Term tyname a uni fun a)
-> Get [Term tyname a uni fun a] -> Get (Term tyname a uni fun a)
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 tyname a uni fun a]
forall a. Flat a => Get a
decode
              go a
11 = a
-> Type tyname uni a
-> Term tyname a uni fun a
-> [Term tyname a uni fun a]
-> Term tyname a uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case     (a
 -> Type tyname uni a
 -> Term tyname a uni fun a
 -> [Term tyname a uni fun a]
 -> Term tyname a uni fun a)
-> Get a
-> Get
     (Type tyname uni a
      -> Term tyname a uni fun a
      -> [Term tyname a uni fun a]
      -> Term tyname a uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall a. Flat a => Get a
decode Get
  (Type tyname uni a
   -> Term tyname a uni fun a
   -> [Term tyname a uni fun a]
   -> Term tyname a uni fun a)
-> Get (Type tyname uni a)
-> Get
     (Term tyname a uni fun a
      -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type tyname uni a)
forall a. Flat a => Get a
decode Get
  (Term tyname a uni fun a
   -> [Term tyname a uni fun a] -> Term tyname a uni fun a)
-> Get (Term tyname a uni fun a)
-> Get ([Term tyname a uni fun a] -> Term tyname a uni fun a)
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 tyname a uni fun a)
forall a. Flat a => Get a
decode Get ([Term tyname a uni fun a] -> Term tyname a uni fun a)
-> Get [Term tyname a uni fun a] -> Get (Term tyname a uni fun a)
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 tyname a uni fun a]
forall a. Flat a => Get a
decode
              go a
_  = [Char] -> Get (Term tyname a uni fun a)
forall a. [Char] -> Get a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Failed to decode Term TyName Name ()"

    size :: Term tyname name uni fun ann -> NumBits -> NumBits
size Term tyname 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 tyname 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'
        TyAbs    ann
ann tyname
tn Kind ann
k Term tyname 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
$ tyname -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size tyname
tn (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Kind ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Kind ann
k  (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t NumBits
sz'
        LamAbs   ann
ann name
n Type tyname uni ann
ty Term tyname 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
ty (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t NumBits
sz'
        Apply    ann
ann Term tyname name uni fun ann
t Term tyname 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 tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname 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'
        TyInst   ann
ann Term tyname name uni fun ann
t Type tyname uni ann
ty      -> 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 tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
ty NumBits
sz'
        Unwrap   ann
ann Term tyname 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 tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t NumBits
sz'
        IWrap    ann
ann Type tyname uni ann
pat Type tyname uni ann
arg Term tyname 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
pat (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
arg (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
t NumBits
sz'
        Error    ann
ann Type tyname uni ann
ty        -> ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size ann
ann (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
ty 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 Type tyname uni ann
ty Word64
i [Term tyname 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
ty (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 tyname name uni fun ann] -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size [Term tyname name uni fun ann]
es NumBits
sz'
        Case     ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname 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
$ Type tyname uni ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Type tyname uni ann
ty (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size Term tyname name uni fun ann
arg (NumBits -> NumBits) -> NumBits -> NumBits
forall a b. (a -> b) -> a -> b
$ [Term tyname name uni fun ann] -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size [Term tyname name uni fun ann]
cs NumBits
sz'

instance ( Closed uni
         , Flat ann
         , Flat tyname
         , Flat name
         ) => Flat (VarDecl tyname name uni ann) where
    encode :: VarDecl tyname name uni ann -> Encoding
encode (VarDecl ann
t name
name Type tyname uni ann
tyname ) = ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
t Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> name -> Encoding
forall a. Flat a => a -> Encoding
encode name
name Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Type tyname uni ann -> Encoding
forall a. Flat a => a -> Encoding
encode Type tyname uni ann
tyname
    decode :: Get (VarDecl tyname name uni ann)
decode = ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl (ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann)
-> Get ann
-> Get (name -> Type tyname uni ann -> VarDecl tyname name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (name -> Type tyname uni ann -> VarDecl tyname name uni ann)
-> Get name
-> Get (Type tyname uni ann -> VarDecl tyname name uni 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 Get (Type tyname uni ann -> VarDecl tyname name uni ann)
-> Get (Type tyname uni ann) -> Get (VarDecl tyname name uni 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 (Type tyname uni ann)
forall a. Flat a => Get a
decode

instance (Flat ann, Flat tyname)  => Flat (TyVarDecl tyname ann) where
    encode :: TyVarDecl tyname ann -> Encoding
encode (TyVarDecl ann
t tyname
tyname Kind ann
kind) = ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
t Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> tyname -> Encoding
forall a. Flat a => a -> Encoding
encode tyname
tyname Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Kind ann -> Encoding
forall a. Flat a => a -> Encoding
encode Kind ann
kind
    decode :: Get (TyVarDecl tyname ann)
decode = ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl (ann -> tyname -> Kind ann -> TyVarDecl tyname ann)
-> Get ann -> Get (tyname -> Kind ann -> TyVarDecl tyname ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (tyname -> Kind ann -> TyVarDecl tyname ann)
-> Get tyname -> Get (Kind ann -> TyVarDecl tyname 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 tyname
forall a. Flat a => Get a
decode Get (Kind ann -> TyVarDecl tyname ann)
-> Get (Kind ann) -> Get (TyVarDecl tyname 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 (Kind ann)
forall a. Flat a => Get a
decode

instance ( Flat ann
         , Flat (Term tyname name uni fun ann)
         ) => Flat (Program tyname name uni fun ann) where
    encode :: Program tyname name uni fun ann -> Encoding
encode (Program ann
ann Version
v Term tyname 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 tyname name uni fun ann -> Encoding
forall a. Flat a => a -> Encoding
encode Term tyname name uni fun ann
t
    decode :: Get (Program tyname name uni fun ann)
decode = ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program (ann
 -> Version
 -> Term tyname name uni fun ann
 -> Program tyname name uni fun ann)
-> Get ann
-> Get
     (Version
      -> Term tyname name uni fun ann -> Program tyname 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
   -> Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> Get Version
-> Get
     (Term tyname name uni fun ann -> Program tyname 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 Version
forall a. Flat a => Get a
decode Get
  (Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> Get (Term tyname name uni fun ann)
-> Get (Program tyname 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 tyname name uni fun ann)
forall a. Flat a => Get a
decode

deriving newtype instance (Flat a) => Flat (Normalized a)

-- See Note [DeBruijn Index serialization]
deriving newtype instance Flat Index -- via word64

deriving newtype instance Flat DeBruijn -- via index
deriving newtype instance Flat TyDeBruijn -- via debruijn

instance Flat NamedDeBruijn where
    encode :: NamedDeBruijn -> Encoding
encode (NamedDeBruijn Text
txt Index
ix) = Text -> Encoding
forall a. Flat a => a -> Encoding
encode Text
txt Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Index -> Encoding
forall a. Flat a => a -> Encoding
encode Index
ix
    decode :: Get NamedDeBruijn
decode = Text -> Index -> NamedDeBruijn
NamedDeBruijn (Text -> Index -> NamedDeBruijn)
-> Get Text -> Get (Index -> NamedDeBruijn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Text
forall a. Flat a => Get a
decode Get (Index -> NamedDeBruijn) -> Get Index -> Get NamedDeBruijn
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Index
forall a. Flat a => Get a
decode

deriving newtype instance Flat NamedTyDeBruijn -- via nameddebruijn

-- NOTE: the serialization roundtrip holds iff the invariant binder.index==0 holds
instance Flat (Binder DeBruijn) where
    size :: Binder DeBruijn -> NumBits -> NumBits
size Binder DeBruijn
_ = NumBits -> NumBits
forall a. a -> a
id -- zero cost
    encode :: Binder DeBruijn -> Encoding
encode Binder DeBruijn
_ = Encoding
forall a. Monoid a => a
mempty
    decode :: Get (Binder DeBruijn)
decode = Binder DeBruijn -> Get (Binder DeBruijn)
forall a. a -> Get a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binder DeBruijn -> Get (Binder DeBruijn))
-> Binder DeBruijn -> Get (Binder DeBruijn)
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Binder DeBruijn
forall name. name -> Binder name
Binder (DeBruijn -> Binder DeBruijn) -> DeBruijn -> Binder DeBruijn
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
deBruijnInitIndex

-- (Binder TyDeBruijn) could similarly have a flat instance, but we don't need it.

deriving newtype instance Flat (Binder Name)
deriving newtype instance Flat (Binder TyName)
-- We could use an alternative, manual Flat-serialization of Named(Ty)DeBruijn
-- where we store the name only at the binder and the index only at the use-site (Var/TyVar).
-- That would be more compact, but we don't need it at the moment.
deriving newtype instance Flat (Binder NamedDeBruijn)
deriving newtype instance Flat (Binder NamedTyDeBruijn)

{- This instance is going via Flat DeBruijn.
FakeNamedDeBruijn <-> DeBruijn are isomorphic: we could use iso-deriving package,
but we do not need any other isomorphic Flat deriving for the moment.
See Note [Why newtype FakeNamedDeBruijn]
-}
instance Flat FakeNamedDeBruijn where
    size :: FakeNamedDeBruijn -> NumBits -> NumBits
size = DeBruijn -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size (DeBruijn -> NumBits -> NumBits)
-> (FakeNamedDeBruijn -> DeBruijn)
-> FakeNamedDeBruijn
-> NumBits
-> NumBits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FakeNamedDeBruijn -> DeBruijn
fromFake
    encode :: FakeNamedDeBruijn -> Encoding
encode = DeBruijn -> Encoding
forall a. Flat a => a -> Encoding
encode (DeBruijn -> Encoding)
-> (FakeNamedDeBruijn -> DeBruijn) -> FakeNamedDeBruijn -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FakeNamedDeBruijn -> DeBruijn
fromFake
    decode :: Get FakeNamedDeBruijn
decode =  DeBruijn -> FakeNamedDeBruijn
toFake (DeBruijn -> FakeNamedDeBruijn)
-> Get DeBruijn -> Get FakeNamedDeBruijn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get DeBruijn
forall a. Flat a => Get a
decode

{- This instance is going via Flat (Binder DeBruijn) instance.
Binder FakeNamedDeBruijn <-> Binder DeBruijn are isomorphic because
FakeNamedDeBruijn <-> DeBruijn are isomorphic and Binder is a functor:
we could use iso-deriving package,
but  we do not need any other isomorphic Flat deriving for the moment.
See Note [Why newtype FakeNamedDeBruijn]
NOTE: the serialization roundtrip holds iff the invariant binder.index==0 holds
-}
instance Flat (Binder FakeNamedDeBruijn) where
    size :: Binder FakeNamedDeBruijn -> NumBits -> NumBits
size = Binder DeBruijn -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size (Binder DeBruijn -> NumBits -> NumBits)
-> (Binder FakeNamedDeBruijn -> Binder DeBruijn)
-> Binder FakeNamedDeBruijn
-> NumBits
-> NumBits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FakeNamedDeBruijn -> DeBruijn)
-> Binder FakeNamedDeBruijn -> Binder DeBruijn
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FakeNamedDeBruijn -> DeBruijn
fromFake
    encode :: Binder FakeNamedDeBruijn -> Encoding
encode = Binder DeBruijn -> Encoding
forall a. Flat a => a -> Encoding
encode (Binder DeBruijn -> Encoding)
-> (Binder FakeNamedDeBruijn -> Binder DeBruijn)
-> Binder FakeNamedDeBruijn
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FakeNamedDeBruijn -> DeBruijn)
-> Binder FakeNamedDeBruijn -> Binder DeBruijn
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FakeNamedDeBruijn -> DeBruijn
fromFake
    decode :: Get (Binder FakeNamedDeBruijn)
decode =  (DeBruijn -> FakeNamedDeBruijn)
-> Binder DeBruijn -> Binder FakeNamedDeBruijn
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijn -> FakeNamedDeBruijn
toFake (Binder DeBruijn -> Binder FakeNamedDeBruijn)
-> Get (Binder DeBruijn) -> Get (Binder FakeNamedDeBruijn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (Binder DeBruijn)
forall a. Flat a => Get a
decode