{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
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
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
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
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
+
NumBits
1
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)) ->
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
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
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
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
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'
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'
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)
deriving newtype instance Flat Index
deriving newtype instance Flat DeBruijn
deriving newtype instance Flat TyDeBruijn
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
instance Flat (Binder DeBruijn) where
size :: Binder DeBruijn -> NumBits -> NumBits
size Binder DeBruijn
_ = NumBits -> NumBits
forall a. a -> a
id
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
deriving newtype instance Flat (Binder Name)
deriving newtype instance Flat (Binder TyName)
deriving newtype instance Flat (Binder NamedDeBruijn)
deriving newtype instance Flat (Binder NamedTyDeBruijn)
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
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