{-# 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 the
-- Note [Stable encoding of PLC] before touching anything in this
-- file.  Also see the Notes [Serialising unit annotations] and
-- [Serialising Scripts] before using anything in this file.

module PlutusCore.Flat
    ( AsSerialize (..)
    , safeEncodeBits
    ) where

import PlutusCore.Core
import PlutusCore.Data
import PlutusCore.DeBruijn
import PlutusCore.Name

import Codec.Serialise (Serialise, deserialiseOrFail, serialise)
import Data.Coerce
import Data.Functor
import Data.Proxy
import Data.Word (Word8)
import Flat
import Flat.Decoder
import Flat.Encoder
import GHC.Natural.Extras
import Universe

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

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

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

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

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

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

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

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

| Data type        | Function          | Used | Available |
|------------------|-------------------|------|-----------|
| default builtins | encodeBuiltin     | 47   | 128       |
| Kinds            | encodeKind        | 2    | 2         |
| Types            | encodeType        | 7    | 8         |
| Terms            | encodeTerm        | 10   | 16        |

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

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

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

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

{- Note [Index (Word64) (de)serialized through Natural]

With the recent change of CEK to use DeBruijn instead of Name,
we decided to change Index to be a Word instead of Natural, for performance reasons.

However, to be absolutely sure that the script format *does not change*
for plutus language version 1, we are converting from/to Word64 and (de)-serialize *only through Natural*,
to keep the old v1 flat format the same.

Natural and Word64 are flat-compatible up-to `maxBound :: Word64`.
However, the current blockchain might have already stored a plutus v1 script
containing a hugely-indexed variable `>maxBound::Word64` -- such a script must be failing
because such a huge index must be a free variable (given the current script-size constraints).

When decoding such an already-stored (failing) script
the Natural deserializer makes the script fail at the scopechecking step (previously undebruijnification step).
Hypotheically using the Word64 deserializer, the script would *hopefully* fail as well, although earlier
at the deserialization step. Initial tests and looking at flat internals make this likely,
but until proven, we postpone the transition to Word64 deserializer for version 2 language.
-}


-- | For deriving 'Flat' instances via 'Serialize'.
newtype AsSerialize a = AsSerialize
    { AsSerialize a -> a
unAsSerialize :: a
    } deriving newtype (Decoder s (AsSerialize a)
Decoder s [AsSerialize a]
[AsSerialize a] -> Encoding
AsSerialize a -> Encoding
(AsSerialize a -> Encoding)
-> (forall s. Decoder s (AsSerialize a))
-> ([AsSerialize a] -> Encoding)
-> (forall s. Decoder s [AsSerialize a])
-> Serialise (AsSerialize a)
forall s. Decoder s [AsSerialize a]
forall s. Decoder s (AsSerialize a)
forall a. Serialise a => [AsSerialize a] -> Encoding
forall a. Serialise a => AsSerialize a -> Encoding
forall a s. Serialise a => Decoder s [AsSerialize a]
forall a s. Serialise a => Decoder s (AsSerialize a)
forall a.
(a -> Encoding)
-> (forall s. Decoder s a)
-> ([a] -> Encoding)
-> (forall s. Decoder s [a])
-> Serialise a
decodeList :: Decoder s [AsSerialize a]
$cdecodeList :: forall a s. Serialise a => Decoder s [AsSerialize a]
encodeList :: [AsSerialize a] -> Encoding
$cencodeList :: forall a. Serialise a => [AsSerialize a] -> Encoding
decode :: Decoder s (AsSerialize a)
$cdecode :: forall a s. Serialise a => Decoder s (AsSerialize a)
encode :: AsSerialize a -> Encoding
$cencode :: forall a. Serialise a => AsSerialize a -> Encoding
Serialise)

instance Serialise a => Flat (AsSerialize a) where
    encode :: AsSerialize a -> Encoding
encode = ByteString -> Encoding
forall a. Flat a => a -> Encoding
encode (ByteString -> Encoding)
-> (AsSerialize a -> ByteString) -> AsSerialize a -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsSerialize a -> ByteString
forall a. Serialise a => a -> ByteString
serialise
    decode :: Get (AsSerialize a)
decode = do
        Either DeserialiseFailure (AsSerialize a)
errOrX <- ByteString -> Either DeserialiseFailure (AsSerialize a)
forall a. Serialise a => ByteString -> Either DeserialiseFailure a
deserialiseOrFail (ByteString -> Either DeserialiseFailure (AsSerialize a))
-> Get ByteString
-> Get (Either DeserialiseFailure (AsSerialize a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ByteString
forall a. Flat a => Get a
decode
        case Either DeserialiseFailure (AsSerialize a)
errOrX of
            Left DeserialiseFailure
err -> String -> Get (AsSerialize a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get (AsSerialize a)) -> String -> Get (AsSerialize a)
forall a b. (a -> b) -> a -> b
$ DeserialiseFailure -> String
forall a. Show a => a -> String
show DeserialiseFailure
err  -- Here we embed a 'Serialise' error into a 'Flat' one.
            Right AsSerialize a
x  -> AsSerialize a -> Get (AsSerialize a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure AsSerialize a
x
    size :: AsSerialize a -> NumBits -> NumBits
size = ByteString -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size (ByteString -> NumBits -> NumBits)
-> (AsSerialize a -> ByteString)
-> AsSerialize a
-> NumBits
-> NumBits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsSerialize a -> ByteString
forall a. Serialise a => a -> ByteString
serialise

safeEncodeBits :: NumBits -> Word8 -> Encoding
safeEncodeBits :: NumBits -> Word8 -> Encoding
safeEncodeBits NumBits
n Word8
v =
  if Word8
2 Word8 -> NumBits -> Word8
forall a b. (Num a, Integral b) => a -> b -> a
^ NumBits
n Word8 -> Word8 -> Bool
forall a. Ord a => a -> a -> Bool
< Word8
v
  then String -> Encoding
forall a. HasCallStack => String -> a
error (String -> Encoding) -> String -> Encoding
forall a b. (a -> b) -> a -> b
$ String
"Overflow detected, cannot fit "
               String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word8 -> String
forall a. Show a => a -> String
show Word8
v String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" in " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> NumBits -> String
forall a. Show a => a -> String
show NumBits
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" bits."
  else NumBits -> Word8 -> Encoding
eBits NumBits
n 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 AsSerialize Data instance Flat Data

decodeKindedUniFlat :: Closed uni => Get (SomeTypeIn (Kinded uni))
decodeKindedUniFlat :: 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    = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Failed to decode a universe"
        go (Just a
uni) = 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 (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 (t :: * -> *) a. Foldable t => t a -> NumBits
length (uni (Esc 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
bring (Proxy Flat
forall k (t :: k). 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 =
        Closed uni => Get (SomeTypeIn (Kinded uni))
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 (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   -> String -> Get (Some (ValueOf uni))
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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
bring (Proxy Flat
forall k (t :: k). Proxy t
Proxy @Flat) uni (Esc a)
uni (Esc a)
uni 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
bring (Proxy Flat
forall k (t :: k). 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 (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 ann => Flat (Version ann) where
    encode :: Version ann -> Encoding
encode (Version ann
ann Natural
n Natural
n' Natural
n'') = ann -> Encoding
forall a. Flat a => a -> Encoding
encode ann
ann 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' Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Natural -> Encoding
forall a. Flat a => a -> Encoding
encode Natural
n''
    decode :: Get (Version ann)
decode = ann -> Natural -> Natural -> Natural -> Version ann
forall ann. ann -> Natural -> Natural -> Natural -> Version ann
Version (ann -> Natural -> Natural -> Natural -> Version ann)
-> Get ann -> Get (Natural -> Natural -> Natural -> Version ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Natural -> Natural -> Natural -> Version ann)
-> Get Natural -> Get (Natural -> Natural -> Version ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get Natural
forall a. Flat a => Get a
decode Get (Natural -> Natural -> Version ann)
-> Get Natural -> Get (Natural -> Version ann)
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 ann) -> Get Natural -> Get (Version ann)
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 ann. (Eq a, Num a, Flat ann) => a -> Get (Kind ann)
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 ann)
go a
0 = ann -> Kind ann
forall ann. ann -> Kind ann
Type      (ann -> Kind ann) -> Get ann -> Get (Kind ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode
              go a
1 = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow (ann -> Kind ann -> Kind ann -> Kind ann)
-> Get ann -> Get (Kind ann -> Kind ann -> Kind ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Kind ann -> Kind ann -> Kind ann)
-> Get (Kind ann) -> Get (Kind ann -> Kind ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind ann)
forall a. Flat a => Get a
decode Get (Kind ann -> Kind ann) -> Get (Kind ann) -> Get (Kind ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind ann)
forall a. Flat a => Get a
decode
              go a
_ = String -> Get (Kind ann)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Failed to decode Kind ()"

    size :: Kind ann -> NumBits -> NumBits
size Kind ann
tm NumBits
sz = NumBits
kindTagWidth NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ case Kind ann
tm of
        Type ann
ann           -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann
        KindArrow ann
ann Kind ann
k Kind ann
k' -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Kind ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Kind ann
k NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Kind ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Kind ann
k'

-- | 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'

    decode :: Get (Type tyname uni ann)
decode = Word8 -> Get (Type tyname uni ann)
forall a ann a (uni :: * -> *).
(Eq a, Num a, Flat ann, Flat a, Closed uni) =>
a -> Get (Type a uni ann)
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 ann)
go a
0 = ann -> a -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar     (ann -> a -> Type a uni ann)
-> Get ann -> Get (a -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (a -> Type a uni ann) -> Get a -> Get (Type a uni ann)
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 = ann -> Type a uni ann -> Type a uni ann -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun     (ann -> Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get ann
-> Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode
              go a
2 = ann -> Type a uni ann -> Type a uni ann -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix    (ann -> Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get ann
-> Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode
              go a
3 = ann -> a -> Kind ann -> Type a uni ann -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall  (ann -> a -> Kind ann -> Type a uni ann -> Type a uni ann)
-> Get ann
-> Get (a -> Kind ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (a -> Kind ann -> Type a uni ann -> Type a uni ann)
-> Get a -> Get (Kind ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode Get (Kind ann -> Type a uni ann -> Type a uni ann)
-> Get (Kind ann) -> Get (Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind ann)
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode
              go a
4 = ann -> SomeTypeIn uni -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin (ann -> SomeTypeIn uni -> Type a uni ann)
-> Get ann -> Get (SomeTypeIn uni -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (SomeTypeIn uni -> Type a uni ann)
-> Get (SomeTypeIn uni) -> Get (Type a uni ann)
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 = ann -> a -> Kind ann -> Type a uni ann -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam     (ann -> a -> Kind ann -> Type a uni ann -> Type a uni ann)
-> Get ann
-> Get (a -> Kind ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (a -> Kind ann -> Type a uni ann -> Type a uni ann)
-> Get a -> Get (Kind ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get a
forall a. Flat a => Get a
decode Get (Kind ann -> Type a uni ann -> Type a uni ann)
-> Get (Kind ann) -> Get (Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind ann)
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode
              go a
6 = ann -> Type a uni ann -> Type a uni ann -> Type a uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp     (ann -> Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get ann
-> Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann -> Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode Get (Type a uni ann -> Type a uni ann)
-> Get (Type a uni ann) -> Get (Type a uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Type a uni ann)
forall a. Flat a => Get a
decode
              go a
_ = String -> Get (Type a uni ann)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Failed to decode Type TyName ()"

    size :: Type tyname uni ann -> NumBits -> NumBits
size Type tyname uni ann
tm NumBits
sz = NumBits
typeTagWidth NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ case Type tyname uni ann
tm of
        TyVar     ann
ann tyname
tn      -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ tyname -> NumBits
forall a. Flat a => a -> NumBits
getSize tyname
tn
        TyFun     ann
ann Type tyname uni ann
t Type tyname uni ann
t'    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t'
        TyIFix    ann
ann Type tyname uni ann
pat Type tyname uni ann
arg -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
pat NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
arg
        TyForall  ann
ann tyname
tn Kind ann
k Type tyname uni ann
t  -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ tyname -> NumBits
forall a. Flat a => a -> NumBits
getSize tyname
tn  NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Kind ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Kind ann
k NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t
        TyBuiltin ann
ann SomeTypeIn uni
con     -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ SomeTypeIn uni -> NumBits
forall a. Flat a => a -> NumBits
getSize SomeTypeIn uni
con
        TyLam     ann
ann tyname
n Kind ann
k Type tyname uni ann
t   -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ tyname -> NumBits
forall a. Flat a => a -> NumBits
getSize tyname
n   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Kind ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Kind ann
k NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t
        TyApp     ann
ann Type tyname uni ann
t Type tyname uni ann
t'    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
t'

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

    decode :: Get (Term tyname name uni fun ann)
decode = Word8 -> Get (Term tyname name uni fun ann)
forall (uni :: * -> *) a ann a tyname fun.
(Everywhere uni Flat, Eq a, Num a, Closed uni, Flat ann, Flat a,
 Flat tyname, Flat fun) =>
a -> Get (Term tyname a uni fun ann)
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 ann)
go a
0 = ann -> a -> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var      (ann -> a -> Term tyname a uni fun ann)
-> Get ann -> Get (a -> Term tyname a 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 (a -> Term tyname a uni fun ann)
-> Get a -> Get (Term tyname a uni fun ann)
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 = ann
-> tyname
-> Kind ann
-> Term tyname a uni fun ann
-> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs    (ann
 -> tyname
 -> Kind ann
 -> Term tyname a uni fun ann
 -> Term tyname a uni fun ann)
-> Get ann
-> Get
     (tyname
      -> Kind ann
      -> Term tyname a uni fun ann
      -> Term tyname a 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
  (tyname
   -> Kind ann
   -> Term tyname a uni fun ann
   -> Term tyname a uni fun ann)
-> Get tyname
-> Get
     (Kind ann
      -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
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
   -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Kind ann)
-> Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Kind ann)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode
              go a
2 = ann
-> a
-> Type tyname uni ann
-> Term tyname a uni fun ann
-> Term tyname a uni fun ann
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   (ann
 -> a
 -> Type tyname uni ann
 -> Term tyname a uni fun ann
 -> Term tyname a uni fun ann)
-> Get ann
-> Get
     (a
      -> Type tyname uni ann
      -> Term tyname a uni fun ann
      -> Term tyname a 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
  (a
   -> Type tyname uni ann
   -> Term tyname a uni fun ann
   -> Term tyname a uni fun ann)
-> Get a
-> Get
     (Type tyname uni ann
      -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
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 ann
   -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Type tyname uni ann)
-> Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
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 Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode
              go a
3 = ann
-> Term tyname a uni fun ann
-> Term tyname a uni fun ann
-> Term tyname a uni fun ann
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    (ann
 -> Term tyname a uni fun ann
 -> Term tyname a uni fun ann
 -> Term tyname a uni fun ann)
-> Get ann
-> Get
     (Term tyname a uni fun ann
      -> Term tyname a uni fun ann -> Term tyname a 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 tyname a uni fun ann
   -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode
              go a
4 = ann -> Some (ValueOf uni) -> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant (ann -> Some (ValueOf uni) -> Term tyname a uni fun ann)
-> Get ann -> Get (Some (ValueOf uni) -> Term tyname a 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 tyname a uni fun ann)
-> Get (Some (ValueOf uni)) -> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Some (ValueOf uni))
forall a. Flat a => Get a
decode
              go a
5 = ann
-> Term tyname a uni fun ann
-> Type tyname uni ann
-> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst   (ann
 -> Term tyname a uni fun ann
 -> Type tyname uni ann
 -> Term tyname a uni fun ann)
-> Get ann
-> Get
     (Term tyname a uni fun ann
      -> Type tyname uni ann -> Term tyname a 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 tyname a uni fun ann
   -> Type tyname uni ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Type tyname uni ann -> Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode Get (Type tyname uni ann -> Term tyname a uni fun ann)
-> Get (Type tyname uni ann) -> Get (Term tyname a uni fun ann)
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
              go a
6 = ann -> Term tyname a uni fun ann -> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap   (ann -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get ann
-> Get (Term tyname a uni fun ann -> Term tyname a 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 tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode
              go a
7 = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname a uni fun ann
-> Term tyname a uni fun ann
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    (ann
 -> Type tyname uni ann
 -> Type tyname uni ann
 -> Term tyname a uni fun ann
 -> Term tyname a uni fun ann)
-> Get ann
-> Get
     (Type tyname uni ann
      -> Type tyname uni ann
      -> Term tyname a uni fun ann
      -> Term tyname a 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
  (Type tyname uni ann
   -> Type tyname uni ann
   -> Term tyname a uni fun ann
   -> Term tyname a uni fun ann)
-> Get (Type tyname uni ann)
-> Get
     (Type tyname uni ann
      -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
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 Get
  (Type tyname uni ann
   -> Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Type tyname uni ann)
-> Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
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 Get (Term tyname a uni fun ann -> Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
-> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Term tyname a uni fun ann)
forall a. Flat a => Get a
decode
              go a
8 = ann -> Type tyname uni ann -> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error    (ann -> Type tyname uni ann -> Term tyname a uni fun ann)
-> Get ann
-> Get (Type tyname uni ann -> Term tyname a 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 (Type tyname uni ann -> Term tyname a uni fun ann)
-> Get (Type tyname uni ann) -> Get (Term tyname a uni fun ann)
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
              go a
9 = ann -> fun -> Term tyname a uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin  (ann -> fun -> Term tyname a uni fun ann)
-> Get ann -> Get (fun -> Term tyname a uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get ann
forall a. Flat a => Get a
decode Get (fun -> Term tyname a uni fun ann)
-> Get fun -> Get (Term tyname a uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get fun
forall a. Flat a => Get a
decode
              go a
_ = String -> Get (Term tyname a uni fun ann)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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 = NumBits
termTagWidth NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ NumBits
sz NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ case Term tyname name uni fun ann
tm of
        Var      ann
ann name
n         -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ name -> NumBits
forall a. Flat a => a -> NumBits
getSize name
n
        TyAbs    ann
ann tyname
tn Kind ann
k Term tyname name uni fun ann
t    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ tyname -> NumBits
forall a. Flat a => a -> NumBits
getSize tyname
tn  NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Kind ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Kind ann
k   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t
        LamAbs   ann
ann name
n Type tyname uni ann
ty Term tyname name uni fun ann
t    -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ name -> NumBits
forall a. Flat a => a -> NumBits
getSize name
n   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
ty  NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t
        Apply    ann
ann Term tyname name uni fun ann
t Term tyname name uni fun ann
t'      -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t'
        Constant ann
ann Some (ValueOf uni)
c         -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Some (ValueOf uni) -> NumBits
forall a. Flat a => a -> NumBits
getSize Some (ValueOf uni)
c
        TyInst   ann
ann Term tyname name uni fun ann
t Type tyname uni ann
ty      -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t   NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
ty
        Unwrap   ann
ann Term tyname name uni fun ann
t         -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize 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 -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
pat NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
arg NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Term tyname name uni fun ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Term tyname name uni fun ann
t
        Error    ann
ann Type tyname uni ann
ty        -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> NumBits
forall a. Flat a => a -> NumBits
getSize Type tyname uni ann
ty
        Builtin  ann
ann fun
bn        -> ann -> NumBits
forall a. Flat a => a -> NumBits
getSize ann
ann NumBits -> NumBits -> NumBits
forall a. Num a => a -> a -> a
+ fun -> NumBits
forall a. Flat a => a -> NumBits
getSize fun
bn

instance ( Closed uni
         , Flat fun
         , Flat ann
         , Flat tyname
         , Flat name
         ) => Flat (VarDecl tyname name uni fun ann) where
    encode :: VarDecl tyname name uni fun 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 fun ann)
decode = ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (ann
 -> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann)
-> Get ann
-> Get
     (name -> Type tyname uni ann -> VarDecl 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
  (name -> Type tyname uni ann -> VarDecl tyname name uni fun ann)
-> Get name
-> Get (Type tyname uni ann -> VarDecl tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get name
forall a. Flat a => Get a
decode Get (Type tyname uni ann -> VarDecl tyname name uni fun ann)
-> Get (Type tyname uni ann)
-> Get (VarDecl tyname name uni fun ann)
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 (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 (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 ann
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 ann -> Encoding
forall a. Flat a => a -> Encoding
encode Version ann
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 ann
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version ann
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program (ann
 -> Version ann
 -> Term tyname name uni fun ann
 -> Program tyname name uni fun ann)
-> Get ann
-> Get
     (Version ann
      -> 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 ann
   -> Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> Get (Version ann)
-> Get
     (Term tyname name uni fun ann -> Program tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Version ann)
forall a. Flat a => Get a
decode Get
  (Term 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 (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 [Index (Word64) (de)serialized through Natural]
instance Flat Index where
    -- encode from word64 to natural
    encode :: Index -> Encoding
encode = Flat Natural => Natural -> Encoding
forall a. Flat a => a -> Encoding
encode @Natural (Natural -> Encoding) -> (Index -> Natural) -> Index -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    -- decode from natural to word64
    decode :: Get Index
decode = do
        Natural
n <- Flat Natural => Get Natural
forall a. Flat a => Get a
decode @Natural
        case Natural -> Maybe Word64
naturalToWord64Maybe Natural
n of
            Maybe Word64
Nothing  -> String -> Get Index
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Get Index) -> String -> Get Index
forall a b. (a -> b) -> a -> b
$ String
"Index outside representable range: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n
            Just Word64
w64 -> Index -> Get Index
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index -> Get Index) -> Index -> Get Index
forall a b. (a -> b) -> a -> b
$ Word64 -> Index
Index Word64
w64
    -- to be exact, we must not let this be generically derived,
    -- because the `gsize` would derive the size of the underlying Word64,
    -- whereas we want the size of Natural
    size :: Index -> NumBits -> NumBits
size = Size Natural
sNatural Size Natural -> (Index -> Natural) -> Index -> NumBits -> NumBits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral

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 (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 (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 TyDeBruin) 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 very similar to the Flat DeBruijn instance.
-- NOTE: the serialization roundtrip holds iff the invariant name==fakeName holds
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 -- via debruijn
    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 -- via debruijn
    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 -- via debruijn

-- this instance is very similar to the Flat (Binder DeBruijn) instance.
-- NOTE: the serialization roundtrip holds iff the invariant name==fakeName holds
instance Flat (Binder FakeNamedDeBruijn) where
    size :: Binder FakeNamedDeBruijn -> NumBits -> NumBits
size  = DeBruijn -> NumBits -> NumBits
forall a. Flat a => a -> NumBits -> NumBits
size (DeBruijn -> NumBits -> NumBits)
-> (Binder FakeNamedDeBruijn -> DeBruijn)
-> Binder FakeNamedDeBruijn
-> NumBits
-> NumBits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FakeNamedDeBruijn -> DeBruijn
fromFake (FakeNamedDeBruijn -> DeBruijn)
-> (Binder FakeNamedDeBruijn -> FakeNamedDeBruijn)
-> Binder FakeNamedDeBruijn
-> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder FakeNamedDeBruijn -> FakeNamedDeBruijn
coerce -- via binder debruijn
    encode :: Binder FakeNamedDeBruijn -> Encoding
encode = DeBruijn -> Encoding
forall a. Flat a => a -> Encoding
encode (DeBruijn -> Encoding)
-> (Binder FakeNamedDeBruijn -> DeBruijn)
-> Binder FakeNamedDeBruijn
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FakeNamedDeBruijn -> DeBruijn
fromFake (FakeNamedDeBruijn -> DeBruijn)
-> (Binder FakeNamedDeBruijn -> FakeNamedDeBruijn)
-> Binder FakeNamedDeBruijn
-> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder FakeNamedDeBruijn -> FakeNamedDeBruijn
coerce -- via binder debruijn
    decode :: Get (Binder FakeNamedDeBruijn)
decode = FakeNamedDeBruijn -> Binder FakeNamedDeBruijn
coerce (FakeNamedDeBruijn -> Binder FakeNamedDeBruijn)
-> (Binder DeBruijn -> FakeNamedDeBruijn)
-> Binder DeBruijn
-> Binder FakeNamedDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> FakeNamedDeBruijn
toFake (DeBruijn -> FakeNamedDeBruijn)
-> (Binder DeBruijn -> DeBruijn)
-> Binder DeBruijn
-> FakeNamedDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder DeBruijn -> DeBruijn
coerce (Binder DeBruijn -> Binder FakeNamedDeBruijn)
-> Get (Binder DeBruijn) -> Get (Binder FakeNamedDeBruijn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Flat (Binder DeBruijn) => Get (Binder DeBruijn)
forall a. Flat a => Get a
decode @(Binder DeBruijn) -- via binder debruijn