    {-# LANGUAGE BangPatterns       #-}
    {-# LANGUAGE FlexibleContexts   #-}
    {-# LANGUAGE FlexibleInstances  #-}
    {-# LANGUAGE RecordWildCards    #-}
    {-# LANGUAGE OverloadedStrings  #-}

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

    {-| This module contains logic for converting Dhall expressions to and from
        CBOR expressions which can in turn be converted to and from a binary
        representation
    -}

    module Dhall.Binary
        ( -- * Standard versions
          StandardVersion(..)
        , renderStandardVersion

        -- * Encoding and decoding
        , encodeExpression
        , decodeExpression

        -- * Exceptions
        , DecodingFailure(..)
        ) where

    import Codec.CBOR.Decoding (Decoder, TokenType(..))
    import Codec.CBOR.Encoding (Encoding)
    import Codec.Serialise (Serialise(encode, decode))
    import Control.Applicative (empty, (<|>))
    import Control.Exception (Exception)
    import Data.ByteString.Lazy (ByteString)
    import Dhall.Syntax
        ( Binding(..)
        , Chunks(..)
        , Const(..)
        , Directory(..)
        , DhallDouble(..)
        , Expr(..)
        , File(..)
        , FilePrefix(..)
        , Import(..)
        , ImportHashed(..)
        , ImportMode(..)
        , ImportType(..)
        , MultiLet(..)
        , PreferAnnotation(..)
        , Scheme(..)
        , URL(..)
        , Var(..)
        )

    import Data.Foldable (toList, foldl')
    import Data.Monoid ((<>))
    import Data.Text (Text)
    import Data.Void (Void, absurd)
    import GHC.Float (double2Float, float2Double)
    import Numeric.Half (fromHalf, toHalf)

    import qualified Codec.CBOR.Decoding  as Decoding
    import qualified Codec.CBOR.Encoding  as Encoding
    import qualified Codec.CBOR.Read      as Read
    import qualified Codec.Serialise      as Serialise
    import qualified Control.Monad        as Monad
    import qualified Data.ByteArray
    import qualified Data.ByteString
    import qualified Data.ByteString.Lazy
    import qualified Data.Sequence
    import qualified Data.Text            as Text
    import qualified Dhall.Crypto
    import qualified Dhall.Map
    import qualified Dhall.Set
    import qualified Dhall.Syntax         as Syntax
    import qualified Text.Printf          as Printf

    {-| Supported version strings

        This exists primarily for backwards compatibility for expressions encoded
        before Dhall removed version tags from the binary encoding
    -}
    data StandardVersion
        = NoVersion
        -- ^ No version string
        | V_5_0_0
        -- ^ Version "5.0.0"
        | V_4_0_0
        -- ^ Version "4.0.0"
        | V_3_0_0
        -- ^ Version "3.0.0"
        | V_2_0_0
        -- ^ Version "2.0.0"
        | V_1_0_0
        -- ^ Version "1.0.0"
        deriving (Int -> StandardVersion
    StandardVersion -> Int
    StandardVersion -> [StandardVersion]
    StandardVersion -> StandardVersion
    StandardVersion -> StandardVersion -> [StandardVersion]
    StandardVersion
    -> StandardVersion -> StandardVersion -> [StandardVersion]
    (StandardVersion -> StandardVersion)
    -> (StandardVersion -> StandardVersion)
    -> (Int -> StandardVersion)
    -> (StandardVersion -> Int)
    -> (StandardVersion -> [StandardVersion])
    -> (StandardVersion -> StandardVersion -> [StandardVersion])
    -> (StandardVersion -> StandardVersion -> [StandardVersion])
    -> (StandardVersion
        -> StandardVersion -> StandardVersion -> [StandardVersion])
    -> Enum StandardVersion
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: StandardVersion
    -> StandardVersion -> StandardVersion -> [StandardVersion]
    $cenumFromThenTo :: StandardVersion
    -> StandardVersion -> StandardVersion -> [StandardVersion]
    enumFromTo :: StandardVersion -> StandardVersion -> [StandardVersion]
    $cenumFromTo :: StandardVersion -> StandardVersion -> [StandardVersion]
    enumFromThen :: StandardVersion -> StandardVersion -> [StandardVersion]
    $cenumFromThen :: StandardVersion -> StandardVersion -> [StandardVersion]
    enumFrom :: StandardVersion -> [StandardVersion]
    $cenumFrom :: StandardVersion -> [StandardVersion]
    fromEnum :: StandardVersion -> Int
    $cfromEnum :: StandardVersion -> Int
    toEnum :: Int -> StandardVersion
    $ctoEnum :: Int -> StandardVersion
    pred :: StandardVersion -> StandardVersion
    $cpred :: StandardVersion -> StandardVersion
    succ :: StandardVersion -> StandardVersion
    $csucc :: StandardVersion -> StandardVersion
    Enum, StandardVersion
    StandardVersion -> StandardVersion -> Bounded StandardVersion
    forall a. a -> a -> Bounded a
    maxBound :: StandardVersion
    $cmaxBound :: StandardVersion
    minBound :: StandardVersion
    $cminBound :: StandardVersion
    Bounded)

    -- | Render a `StandardVersion` as `Text`
    renderStandardVersion :: StandardVersion -> Text
    renderStandardVersion :: StandardVersion -> Text
    renderStandardVersion NoVersion = "none"
    renderStandardVersion V_1_0_0   = "1.0.0"
    renderStandardVersion V_2_0_0   = "2.0.0"
    renderStandardVersion V_3_0_0   = "3.0.0"
    renderStandardVersion V_4_0_0   = "4.0.0"
    renderStandardVersion V_5_0_0   = "5.0.0"

    {-| Convert a function applied to multiple arguments to the base function and
        the list of arguments
    -}
    unApply :: Expr s a -> (Expr s a, [Expr s a])
    unApply :: Expr s a -> (Expr s a, [Expr s a])
    unApply e₀ :: Expr s a
    e₀ = (Expr s a
    baseFunction₀, [Expr s a] -> [Expr s a]
    diffArguments₀ [])
      where
        ~(baseFunction₀ :: Expr s a
    baseFunction₀, diffArguments₀ :: [Expr s a] -> [Expr s a]
    diffArguments₀) = Expr s a -> (Expr s a, [Expr s a] -> [Expr s a])
    forall s a. Expr s a -> (Expr s a, [Expr s a] -> [Expr s a])
    go Expr s a
    e₀

        go :: Expr s a -> (Expr s a, [Expr s a] -> [Expr s a])
    go (App f :: Expr s a
    f a :: Expr s a
    a) = (Expr s a
    baseFunction, [Expr s a] -> [Expr s a]
    diffArguments ([Expr s a] -> [Expr s a])
    -> ([Expr s a] -> [Expr s a]) -> [Expr s a] -> [Expr s a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr s a
    a Expr s a -> [Expr s a] -> [Expr s a]
    forall a. a -> [a] -> [a]
    :))
          where
            ~(baseFunction :: Expr s a
    baseFunction, diffArguments :: [Expr s a] -> [Expr s a]
    diffArguments) = Expr s a -> (Expr s a, [Expr s a] -> [Expr s a])
    go Expr s a
    f

        go (Note _ e :: Expr s a
    e) = Expr s a -> (Expr s a, [Expr s a] -> [Expr s a])
    go Expr s a
    e

        go baseFunction :: Expr s a
    baseFunction = (Expr s a
    baseFunction, [Expr s a] -> [Expr s a]
    forall a. a -> a
    id)

    decodeExpressionInternal :: (Int -> Decoder s a) -> Decoder s (Expr t a)
    decodeExpressionInternal :: (Int -> Decoder s a) -> Decoder s (Expr t a)
    decodeExpressionInternal decodeEmbed :: Int -> Decoder s a
    decodeEmbed = Decoder s (Expr t a)
    forall s. Decoder s (Expr s a)
    go
      where
        go :: Decoder s (Expr s a)
    go = do
            let die :: String -> m a
    die message :: String
    message = String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Dhall.Binary.decodeExpressionInternal: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    message)

            TokenType
    tokenType₀ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

            case TokenType
    tokenType₀ of
                TypeUInt -> do
                    !Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "_" (Word -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word
    n)))

                TypeUInt64 -> do
                    !Word64
    n <- Decoder s Word64
    forall s. Decoder s Word64
    Decoding.decodeWord64

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "_" (Word64 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n)))

                TypeFloat16 -> do
                    !Float
    n <- Decoder s Float
    forall s. Decoder s Float
    Decoding.decodeFloat

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit (Double -> DhallDouble
    DhallDouble (Float -> Double
    float2Double Float
    n)))

                TypeFloat32 -> do
                    !Float
    n <- Decoder s Float
    forall s. Decoder s Float
    Decoding.decodeFloat

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit (Double -> DhallDouble
    DhallDouble (Float -> Double
    float2Double Float
    n)))

                TypeFloat64 -> do
                    !Double
    n <- Decoder s Double
    forall s. Decoder s Double
    Decoding.decodeDouble

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit (Double -> DhallDouble
    DhallDouble Double
    n))

                TypeBool -> do
                    !Bool
    b <- Decoder s Bool
    forall s. Decoder s Bool
    Decoding.decodeBool

                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    b)

                TypeString -> do
                    Text
    s <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                    case Text
    s of
                        "Natural/build"     -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalBuild
                        "Natural/fold"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalFold
                        "Natural/isZero"    -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalIsZero
                        "Natural/even"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalEven
                        "Natural/odd"       -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalOdd
                        "Natural/toInteger" -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalToInteger
                        "Natural/show"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalShow
                        "Natural/subtract"  -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    NaturalSubtract
                        "Integer/toDouble"  -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    IntegerToDouble
                        "Integer/clamp"     -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    IntegerClamp
                        "Integer/negate"    -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    IntegerNegate
                        "Integer/show"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    IntegerShow
                        "Double/show"       -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    DoubleShow
                        "List/build"        -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListBuild
                        "List/fold"         -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListFold
                        "List/length"       -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListLength
                        "List/head"         -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListHead
                        "List/last"         -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListLast
                        "List/indexed"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListIndexed
                        "List/reverse"      -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    ListReverse
                        "Optional/fold"     -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    OptionalFold
                        "Optional/build"    -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    OptionalBuild
                        "Bool"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Bool
                        "Optional"          -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Optional
                        "None"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    None
                        "Natural"           -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Natural
                        "Integer"           -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Integer
                        "Double"            -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Double
                        "Text"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    Text
                        "Text/show"         -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    TextShow
                        "List"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    forall s a. Expr s a
    List
                        "Type"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    Type)
                        "Kind"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    Kind)
                        "Sort"              -> Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    Sort)
                        _                   -> String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unrecognized built-in: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Text -> String
    Text.unpack Text
    s)

                TypeListLen -> do
                    Int
    len <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeListLen

                    case Int
    len of
                        0 -> String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die "Missing tag"
                        _ -> () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                    TokenType
    tokenType₁ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                    case TokenType
    tokenType₁ of
                        TypeString -> do
                            Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                            if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "_"
                                then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die "Non-standard encoding of an α-normalized variable"
                                else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                            TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                            case TokenType
    tokenType₂ of
                                TypeUInt -> do
                                    !Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    x (Word -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word
    n)))

                                TypeUInt64 -> do
                                    !Word64
    n <- Decoder s Word64
    forall s. Decoder s Word64
    Decoding.decodeWord64

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    x (Word64 -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n)))

                                _ -> do
                                    String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected token type for variable index: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₂)

                        TypeUInt -> do
                            Word
    tag <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                            case Word
    tag of
                                0 -> do
                                    Expr s a
    f <- Decoder s (Expr s a)
    go

                                    [Expr s a]
    xs <- Int -> Decoder s (Expr s a) -> Decoder s [Expr s a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 2) Decoder s (Expr s a)
    go

                                    if [Expr s a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Expr s a]
    xs
                                        then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die "Non-standard encoding of a function with no arguments"
                                        else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Expr s a -> Expr s a -> Expr s a)
    -> Expr s a -> [Expr s a] -> Expr s a
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f [Expr s a]
    xs)

                                1 -> do
                                    case Int
    len of
                                        3 -> do
                                            Expr s a
    _A <- Decoder s (Expr s a)
    go

                                            Expr s a
    b <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "_" Expr s a
    _A Expr s a
    b)

                                        4 -> do
                                            Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                            if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "_"
                                                then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die "Non-standard encoding of a λ expression"
                                                else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                                            Expr s a
    _A <- Decoder s (Expr s a)
    go

                                            Expr s a
    b <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    x Expr s a
    _A Expr s a
    b)

                                        _ -> do
                                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Incorrect number of tokens used to encode a λ expression: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    len)

                                2 -> do
                                    case Int
    len of
                                        3 -> do
                                            Expr s a
    _A <- Decoder s (Expr s a)
    go

                                            Expr s a
    _B <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi "_" Expr s a
    _A Expr s a
    _B)

                                        4 -> do
                                            Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                            if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "_"
                                                then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die "Non-standard encoding of a ∀ expression"
                                                else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                                            Expr s a
    _A <- Decoder s (Expr s a)
    go

                                            Expr s a
    _B <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    x Expr s a
    _A Expr s a
    _B)

                                        _ -> do
                                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Incorrect number of tokens used to encode a ∀ expression: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    len)

                                3 -> do
                                    Word
    opcode <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                                    Expr s a -> Expr s a -> Expr s a
    op <- case Word
    opcode of
                                        0  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolOr
                                        1  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolAnd
                                        2  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolEQ
                                        3  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolNE
                                        4  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalPlus
                                        5  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalTimes
                                        6  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend
                                        7  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend
                                        8  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe Text
    forall a. Maybe a
    Nothing)
                                        9  -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation s a
    forall s a. PreferAnnotation s a
    PreferFromSource)
                                        10 -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    CombineTypes
                                        11 -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ImportAlt
                                        12 -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Equivalent
                                        13 -> (Expr s a -> Expr s a -> Expr s a)
    -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    RecordCompletion
                                        _  -> String -> Decoder s (Expr s a -> Expr s a -> Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unrecognized operator code: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Word -> String
    forall a. Show a => a -> String
    show Word
    opcode)

                                    Expr s a
    l <- Decoder s (Expr s a)
    go

                                    Expr s a
    r <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Expr s a
    op Expr s a
    l Expr s a
    r)

                                4 -> do
                                    case Int
    len of
                                        2 -> do
                                            Expr s a
    _T <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _T)) Seq (Expr s a)
    forall (f :: * -> *) a. Alternative f => f a
    empty)

                                        _ -> do
                                            Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull

                                            [Expr s a]
    xs <- Int -> Decoder s (Expr s a) -> Decoder s [Expr s a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 2) Decoder s (Expr s a)
    go
                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    forall a. Maybe a
    Nothing ([Expr s a] -> Seq (Expr s a)
    forall a. [a] -> Seq a
    Data.Sequence.fromList [Expr s a]
    xs))

                                5 -> do
                                    Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull

                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    t)

                                6 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Expr s a
    u <- Decoder s (Expr s a)
    go

                                    case Int
    len of
                                        3 -> do
                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    t Expr s a
    u Maybe (Expr s a)
    forall a. Maybe a
    Nothing)

                                        4 -> do
                                            Expr s a
    _T <- Decoder s (Expr s a)
    go

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    t Expr s a
    u (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just Expr s a
    _T))

                                        _ -> do
                                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Incorrect number of tokens used to encode a `merge` expression: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    len)

                                7 -> do
                                    Int
    mapLength <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeMapLen

                                    [(Text, Expr s a)]
    xTs <- Int -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM Int
    mapLength (Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)])
    -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall a b. (a -> b) -> a -> b
    $ do
                                        Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                        Expr s a
    _T <- Decoder s (Expr s a)
    go

                                        (Text, Expr s a) -> Decoder s (Text, Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    x, Expr s a
    _T)

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record ([(Text, Expr s a)] -> Map Text (Expr s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, Expr s a)]
    xTs))

                                8 -> do
                                    Int
    mapLength <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeMapLen

                                    [(Text, Expr s a)]
    xts <- Int -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM Int
    mapLength (Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)])
    -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall a b. (a -> b) -> a -> b
    $ do
                                        Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                        Expr s a
    t <- Decoder s (Expr s a)
    go

                                        (Text, Expr s a) -> Decoder s (Text, Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    x, Expr s a
    t)

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit ([(Text, Expr s a)] -> Map Text (Expr s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, Expr s a)]
    xts))

                                9 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    t Text
    x)

                                10 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Either (Set Text) (Expr s a)
    xs <- case Int
    len of
                                        3 -> do
                                            TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                                            case TokenType
    tokenType₂ of
                                                TypeListLen -> do
                                                    Int
    _ <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeListLen

                                                    Expr s a
    _T <- Decoder s (Expr s a)
    go

                                                    Either (Set Text) (Expr s a)
    -> Decoder s (Either (Set Text) (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Either (Set Text) (Expr s a)
    forall a b. b -> Either a b
    Right Expr s a
    _T)

                                                TypeString -> do
                                                    Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString
                                                    Either (Set Text) (Expr s a)
    -> Decoder s (Either (Set Text) (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left ([Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Dhall.Set.fromList [Text
    x]))

                                                _ -> do
                                                    String -> Decoder s (Either (Set Text) (Expr s a))
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected token type for projection: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₂)

                                        _ -> do
                                            [Text]
    xs <- Int -> Decoder s Text -> Decoder s [Text]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 2) Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                            Either (Set Text) (Expr s a)
    -> Decoder s (Either (Set Text) (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left ([Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Dhall.Set.fromList [Text]
    xs))

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    t Either (Set Text) (Expr s a)
    xs)

                                11 -> do
                                    Int
    mapLength <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeMapLen

                                    [(Text, Maybe (Expr s a))]
    xTs <- Int
    -> Decoder s (Text, Maybe (Expr s a))
    -> Decoder s [(Text, Maybe (Expr s a))]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM Int
    mapLength (Decoder s (Text, Maybe (Expr s a))
     -> Decoder s [(Text, Maybe (Expr s a))])
    -> Decoder s (Text, Maybe (Expr s a))
    -> Decoder s [(Text, Maybe (Expr s a))]
    forall a b. (a -> b) -> a -> b
    $ do
                                        Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                        TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                                        Maybe (Expr s a)
    mT <- case TokenType
    tokenType₂ of
                                            TypeNull -> do
                                                Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull

                                                Maybe (Expr s a) -> Decoder s (Maybe (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                                            _ -> do
                                                Expr s a
    _T <- Decoder s (Expr s a)
    go

                                                Maybe (Expr s a) -> Decoder s (Maybe (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just Expr s a
    _T)

                                        (Text, Maybe (Expr s a)) -> Decoder s (Text, Maybe (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    x, Maybe (Expr s a)
    mT)

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Text (Maybe (Expr s a)) -> Expr s a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union ([(Text, Maybe (Expr s a))] -> Map Text (Maybe (Expr s a))
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, Maybe (Expr s a))]
    xTs))

                                14 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Expr s a
    l <- Decoder s (Expr s a)
    go

                                    Expr s a
    r <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
    BoolIf Expr s a
    t Expr s a
    l Expr s a
    r)

                                15 -> do
                                    TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                                    case TokenType
    tokenType₂ of
                                        TypeUInt -> do
                                            Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Word -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word
    n))

                                        TypeUInt64 -> do
                                            Word64
    n <- Decoder s Word64
    forall s. Decoder s Word64
    Decoding.decodeWord64

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Word64 -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n))

                                        TypeInteger -> do
                                            Integer
    n <- Decoder s Integer
    forall s. Decoder s Integer
    Decoding.decodeInteger
                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Integer -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    n))

                                        _ -> do
                                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected token type for Natural literal: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₂)

                                16 -> do
                                    TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                                    case TokenType
    tokenType₂ of
                                        TypeUInt -> do
                                            Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Word -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word
    n))

                                        TypeUInt64 -> do
                                            Word64
    n <- Decoder s Word64
    forall s. Decoder s Word64
    Decoding.decodeWord64

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n))

                                        TypeNInt -> do
                                            Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeNegWord

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (-1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Word -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word
    n))

                                        TypeNInt64 -> do
                                            Word64
    n <- Decoder s Word64
    forall s. Decoder s Word64
    Decoding.decodeNegWord64

                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (-1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n))
                                        TypeInteger -> do
                                            Integer
    n <- Decoder s Integer
    forall s. Decoder s Integer
    Decoding.decodeInteger
                                            Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit Integer
    n)

                                        _ -> do
                                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected token type for Integer literal: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₂)

                                18 -> do
                                    [(Text, Expr s a)]
    xys <- Int -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM ((Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 2) Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `quot` 2) (Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)])
    -> Decoder s (Text, Expr s a) -> Decoder s [(Text, Expr s a)]
    forall a b. (a -> b) -> a -> b
    $ do
                                        Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                        Expr s a
    y <- Decoder s (Expr s a)
    go

                                        (Text, Expr s a) -> Decoder s (Text, Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    x, Expr s a
    y)

                                    Text
    z <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text, Expr s a)]
    xys Text
    z))

                                19 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Assert Expr s a
    t)

                                24 -> do
                                    (a -> Expr s a) -> Decoder s a -> Decoder s (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Expr s a
    forall s a. a -> Expr s a
    Embed (Int -> Decoder s a
    decodeEmbed Int
    len)

                                25 -> do
                                    [Binding s a]
    bindings <- Int -> Decoder s (Binding s a) -> Decoder s [Binding s a]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM ((Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 2) Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `quot` 3) (Decoder s (Binding s a) -> Decoder s [Binding s a])
    -> Decoder s (Binding s a) -> Decoder s [Binding s a]
    forall a b. (a -> b) -> a -> b
    $ do
                                        Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                                        TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                                        Maybe (Maybe s, Expr s a)
    mA <- case TokenType
    tokenType₂ of
                                            TypeNull -> do
                                                Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull

                                                Maybe (Maybe s, Expr s a) -> Decoder s (Maybe (Maybe s, Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Maybe s, Expr s a)
    forall a. Maybe a
    Nothing

                                            _ -> do
                                                Expr s a
    _A <- Decoder s (Expr s a)
    go

                                                Maybe (Maybe s, Expr s a) -> Decoder s (Maybe (Maybe s, Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Maybe s, Expr s a) -> Maybe (Maybe s, Expr s a)
    forall a. a -> Maybe a
    Just (Maybe s
    forall a. Maybe a
    Nothing, Expr s a
    _A))

                                        Expr s a
    a <- Decoder s (Expr s a)
    go

                                        Binding s a -> Decoder s (Binding s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    forall s a.
    Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    Binding Maybe s
    forall a. Maybe a
    Nothing Text
    x Maybe s
    forall a. Maybe a
    Nothing Maybe (Maybe s, Expr s a)
    mA Maybe s
    forall a. Maybe a
    Nothing Expr s a
    a)

                                    Expr s a
    b <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Binding s a -> Expr s a -> Expr s a)
    -> Expr s a -> [Binding s a] -> Expr s a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Binding s a -> Expr s a -> Expr s a
    forall s a. Binding s a -> Expr s a -> Expr s a
    Let Expr s a
    b [Binding s a]
    bindings)

                                26 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Expr s a
    _T <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Annot Expr s a
    t Expr s a
    _T)

                                27 -> do
                                    Expr s a
    t <- Decoder s (Expr s a)
    go

                                    Maybe (Expr s a)
    mT <- case Int
    len of
                                        2 -> do
                                            Maybe (Expr s a) -> Decoder s (Maybe (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                                        3 -> do
                                            Expr s a
    _T <- Decoder s (Expr s a)
    go

                                            Maybe (Expr s a) -> Decoder s (Maybe (Expr s a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just Expr s a
    _T)

                                        _ -> do
                                            String -> Decoder s (Maybe (Expr s a))
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Incorrect number of tokens used to encode a type annotation: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    len)

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
    ToMap Expr s a
    t Maybe (Expr s a)
    mT)

                                28 -> do
                                    Expr s a
    _T <- Decoder s (Expr s a)
    go

                                    Expr s a -> Decoder s (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just Expr s a
    _T) Seq (Expr s a)
    forall (f :: * -> *) a. Alternative f => f a
    empty)

                                _ -> do
                                    String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected tag: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Word -> String
    forall a. Show a => a -> String
    show Word
    tag)

                        _ -> do
                            String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected tag type: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₁)

                _ -> do
                    String -> Decoder s (Expr s a)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected initial token: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₀)

    encodeExpressionInternal :: (a -> Encoding) -> Expr Void a -> Encoding
    encodeExpressionInternal :: (a -> Encoding) -> Expr Void a -> Encoding
    encodeExpressionInternal encodeEmbed :: a -> Encoding
    encodeEmbed = Expr Void a -> Encoding
    forall s. Expr s a -> Encoding
    go
      where
        go :: Expr s a -> Encoding
    go e :: Expr s a
    e = case Expr s a
    e of
            Var (V "_" n :: Int
    n) ->
                Int -> Encoding
    Encoding.encodeInt Int
    n

            Var (V x :: Text
    x n :: Int
    n) ->
                    Word -> Encoding
    Encoding.encodeListLen 2
                Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <>  Text -> Encoding
    Encoding.encodeString Text
    x
                Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <>  Int -> Encoding
    Encoding.encodeInt Int
    n

            NaturalBuild ->
                Text -> Encoding
    Encoding.encodeString "Natural/build"

            NaturalFold ->
                Text -> Encoding
    Encoding.encodeString "Natural/fold"

            NaturalIsZero ->
                Text -> Encoding
    Encoding.encodeString "Natural/isZero"

            NaturalEven ->
                Text -> Encoding
    Encoding.encodeString "Natural/even"

            NaturalOdd ->
                Text -> Encoding
    Encoding.encodeString "Natural/odd"

            NaturalToInteger ->
                Text -> Encoding
    Encoding.encodeString "Natural/toInteger"

            NaturalShow ->
                Text -> Encoding
    Encoding.encodeString "Natural/show"

            NaturalSubtract ->
                Text -> Encoding
    Encoding.encodeString "Natural/subtract"

            IntegerToDouble ->
                Text -> Encoding
    Encoding.encodeString "Integer/toDouble"

            IntegerClamp ->
                Text -> Encoding
    Encoding.encodeString "Integer/clamp"

            IntegerNegate ->
                Text -> Encoding
    Encoding.encodeString "Integer/negate"

            IntegerShow ->
                Text -> Encoding
    Encoding.encodeString "Integer/show"

            DoubleShow ->
                Text -> Encoding
    Encoding.encodeString "Double/show"

            ListBuild ->
                Text -> Encoding
    Encoding.encodeString "List/build"

            ListFold ->
                Text -> Encoding
    Encoding.encodeString "List/fold"

            ListLength ->
                Text -> Encoding
    Encoding.encodeString "List/length"

            ListHead ->
                Text -> Encoding
    Encoding.encodeString "List/head"

            ListLast ->
                Text -> Encoding
    Encoding.encodeString "List/last"

            ListIndexed ->
                Text -> Encoding
    Encoding.encodeString "List/indexed"

            ListReverse ->
                Text -> Encoding
    Encoding.encodeString "List/reverse"

            OptionalFold ->
                Text -> Encoding
    Encoding.encodeString "Optional/fold"

            OptionalBuild ->
                Text -> Encoding
    Encoding.encodeString "Optional/build"

            Bool ->
                Text -> Encoding
    Encoding.encodeString "Bool"

            Optional ->
                Text -> Encoding
    Encoding.encodeString "Optional"

            None ->
                Text -> Encoding
    Encoding.encodeString "None"

            Natural ->
                Text -> Encoding
    Encoding.encodeString "Natural"

            Integer ->
                Text -> Encoding
    Encoding.encodeString "Integer"

            Double ->
                Text -> Encoding
    Encoding.encodeString "Double"

            Text ->
                Text -> Encoding
    Encoding.encodeString "Text"

            TextShow ->
                Text -> Encoding
    Encoding.encodeString "Text/show"

            List ->
                Text -> Encoding
    Encoding.encodeString "List"

            Const Type ->
                Text -> Encoding
    Encoding.encodeString "Type"

            Const Kind ->
                Text -> Encoding
    Encoding.encodeString "Kind"

            Const Sort ->
                Text -> Encoding
    Encoding.encodeString "Sort"

            a :: Expr s a
    a@App{} ->
                Int -> [Encoding] -> Encoding
    encodeListN
                    (2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [Expr s a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Expr s a]
    arguments)
                    ( Int -> Encoding
    Encoding.encodeInt 0
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : Expr s a -> Encoding
    go Expr s a
    function
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : (Expr s a -> Encoding) -> [Expr s a] -> [Encoding]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr s a -> Encoding
    go [Expr s a]
    arguments
                    )
              where
                (function :: Expr s a
    function, arguments :: [Expr s a]
    arguments) = Expr s a -> (Expr s a, [Expr s a])
    forall s a. Expr s a -> (Expr s a, [Expr s a])
    unApply Expr s a
    a

            Lam "_" _A :: Expr s a
    _A b :: Expr s a
    b ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 1)
                    (Expr s a -> Encoding
    go Expr s a
    _A)
                    (Expr s a -> Encoding
    go Expr s a
    b)

            Lam x :: Text
    x _A :: Expr s a
    _A b :: Expr s a
    b ->
                Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4
                    (Int -> Encoding
    Encoding.encodeInt 1)
                    (Text -> Encoding
    Encoding.encodeString Text
    x)
                    (Expr s a -> Encoding
    go Expr s a
    _A)
                    (Expr s a -> Encoding
    go Expr s a
    b)

            Pi "_" _A :: Expr s a
    _A _B :: Expr s a
    _B ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 2)
                    (Expr s a -> Encoding
    go Expr s a
    _A)
                    (Expr s a -> Encoding
    go Expr s a
    _B)

            Pi x :: Text
    x _A :: Expr s a
    _A _B :: Expr s a
    _B ->
                Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4
                    (Int -> Encoding
    Encoding.encodeInt 2)
                    (Text -> Encoding
    Encoding.encodeString Text
    x)
                    (Expr s a -> Encoding
    go Expr s a
    _A)
                    (Expr s a -> Encoding
    go Expr s a
    _B)

            BoolOr l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 0 Expr s a
    l Expr s a
    r

            BoolAnd l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 1 Expr s a
    l Expr s a
    r

            BoolEQ l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 2 Expr s a
    l Expr s a
    r

            BoolNE l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 3 Expr s a
    l Expr s a
    r

            NaturalPlus l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 4 Expr s a
    l Expr s a
    r

            NaturalTimes l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 5 Expr s a
    l Expr s a
    r

            TextAppend l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 6 Expr s a
    l Expr s a
    r

            ListAppend l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 7 Expr s a
    l Expr s a
    r

            Combine _ l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 8 Expr s a
    l Expr s a
    r

            Prefer _ l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 9 Expr s a
    l Expr s a
    r

            CombineTypes l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 10 Expr s a
    l Expr s a
    r

            ImportAlt l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 11 Expr s a
    l Expr s a
    r

            Equivalent l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 12 Expr s a
    l Expr s a
    r

            RecordCompletion l :: Expr s a
    l r :: Expr s a
    r ->
                Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator 13 Expr s a
    l Expr s a
    r

            ListLit _T₀ :: Maybe (Expr s a)
    _T₀ xs :: Seq (Expr s a)
    xs
                | Seq (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Expr s a)
    xs ->
                    Encoding -> Encoding -> Encoding
    encodeList2 (Int -> Encoding
    Encoding.encodeInt Int
    label) Encoding
    _T₁
                | Bool
    otherwise ->
                    Int -> [Encoding] -> Encoding
    encodeListN
                        (2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Seq (Expr s a) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Seq (Expr s a)
    xs)
                        ( Int -> Encoding
    Encoding.encodeInt 4
                        Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : Encoding
    Encoding.encodeNull
                        Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : (Expr s a -> Encoding) -> [Expr s a] -> [Encoding]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr s a -> Encoding
    go (Seq (Expr s a) -> [Expr s a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Data.Foldable.toList Seq (Expr s a)
    xs)
                        )
              where
                (label :: Int
    label, _T₁ :: Encoding
    _T₁) = case Maybe (Expr s a)
    _T₀ of
                    Nothing           -> (4 , Encoding
    Encoding.encodeNull)
                    Just (App List t :: Expr s a
    t) -> (4 , Expr s a -> Encoding
    go Expr s a
    t               )
                    Just  t :: Expr s a
    t           -> (28, Expr s a -> Encoding
    go Expr s a
    t               )

            Some t :: Expr s a
    t ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 5)
                    Encoding
    Encoding.encodeNull
                    (Expr s a -> Encoding
    go Expr s a
    t)

            Merge t :: Expr s a
    t u :: Expr s a
    u Nothing ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 6)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Expr s a -> Encoding
    go Expr s a
    u)

            Merge t :: Expr s a
    t u :: Expr s a
    u (Just _T :: Expr s a
    _T) ->
                Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4
                    (Int -> Encoding
    Encoding.encodeInt 6)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Expr s a -> Encoding
    go Expr s a
    u)
                    (Expr s a -> Encoding
    go Expr s a
    _T)

            Record xTs :: Map Text (Expr s a)
    xTs ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 7)
                    ((Expr s a -> Encoding) -> Map Text (Expr s a) -> Encoding
    forall t. (t -> Encoding) -> Map Text t -> Encoding
    encodeMapWith Expr s a -> Encoding
    go Map Text (Expr s a)
    xTs)

            RecordLit xts :: Map Text (Expr s a)
    xts ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 8)
                    ((Expr s a -> Encoding) -> Map Text (Expr s a) -> Encoding
    forall t. (t -> Encoding) -> Map Text t -> Encoding
    encodeMapWith Expr s a -> Encoding
    go Map Text (Expr s a)
    xts)

            Field t :: Expr s a
    t x :: Text
    x ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 9)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Text -> Encoding
    Encoding.encodeString Text
    x)

            Project t :: Expr s a
    t (Left xs :: Set Text
    xs) ->
                Int -> [Encoding] -> Encoding
    encodeListN
                    (2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Set Text -> Int
    forall a. Set a -> Int
    Dhall.Set.size Set Text
    xs)
                    ( Int -> Encoding
    Encoding.encodeInt 10
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : Expr s a -> Encoding
    go Expr s a
    t
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : (Text -> Encoding) -> [Text] -> [Encoding]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Encoding
    Encoding.encodeString (Set Text -> [Text]
    forall a. Set a -> [a]
    Dhall.Set.toList Set Text
    xs)
                    )

            Project t :: Expr s a
    t (Right _T :: Expr s a
    _T) ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 10)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Encoding -> Encoding
    encodeList1 (Expr s a -> Encoding
    go Expr s a
    _T))

            Union xTs :: Map Text (Maybe (Expr s a))
    xTs ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 11)
                    ((Maybe (Expr s a) -> Encoding)
    -> Map Text (Maybe (Expr s a)) -> Encoding
    forall t. (t -> Encoding) -> Map Text t -> Encoding
    encodeMapWith Maybe (Expr s a) -> Encoding
    encodeValue Map Text (Maybe (Expr s a))
    xTs)
              where
                encodeValue :: Maybe (Expr s a) -> Encoding
    encodeValue  Nothing  = Encoding
    Encoding.encodeNull
                encodeValue (Just _T :: Expr s a
    _T) = Expr s a -> Encoding
    go Expr s a
    _T

            BoolLit b :: Bool
    b ->
                Bool -> Encoding
    Encoding.encodeBool Bool
    b

            BoolIf t :: Expr s a
    t l :: Expr s a
    l r :: Expr s a
    r ->
                Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4
                    (Int -> Encoding
    Encoding.encodeInt 14)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Expr s a -> Encoding
    go Expr s a
    l)
                    (Expr s a -> Encoding
    go Expr s a
    r)

            NaturalLit n :: Natural
    n ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 15)
                    (Integer -> Encoding
    Encoding.encodeInteger (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n))

            IntegerLit n :: Integer
    n ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 16)
                    (Integer -> Encoding
    Encoding.encodeInteger (Integer -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    n))

            DoubleLit (DhallDouble n64 :: Double
    n64)
                | Bool
    useHalf   -> Float -> Encoding
    Encoding.encodeFloat16 Float
    n32
                | Bool
    useFloat  -> Float -> Encoding
    Encoding.encodeFloat Float
    n32
                | Bool
    otherwise -> Double -> Encoding
    Encoding.encodeDouble Double
    n64
              where
                n32 :: Float
    n32 = Double -> Float
    double2Float Double
    n64

                n16 :: Half
    n16 = Float -> Half
    toHalf Float
    n32

                useFloat :: Bool
    useFloat = Double
    n64 Double -> Double -> Bool
    forall a. Eq a => a -> a -> Bool
    == Float -> Double
    float2Double Float
    n32

                useHalf :: Bool
    useHalf = Double
    n64 Double -> Double -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Float -> Double
    float2Double (Float -> Double) -> Float -> Double
    forall a b. (a -> b) -> a -> b
    $ Half -> Float
    fromHalf Half
    n16)

            -- Fast path for the common case of an uninterpolated string
            TextLit (Chunks [] z :: Text
    z) ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 18)
                    (Text -> Encoding
    Encoding.encodeString Text
    z)

            TextLit (Chunks xys :: [(Text, Expr s a)]
    xys z :: Text
    z) ->
                Int -> [Encoding] -> Encoding
    encodeListN
                    (2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * [(Text, Expr s a)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Text, Expr s a)]
    xys)
                    ( Int -> Encoding
    Encoding.encodeInt 18
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : ((Text, Expr s a) -> [Encoding])
    -> [(Text, Expr s a)] -> [Encoding]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Text, Expr s a) -> [Encoding]
    encodePair [(Text, Expr s a)]
    xys [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++ [ Text -> Encoding
    Encoding.encodeString Text
    z ]
                    )
              where
                encodePair :: (Text, Expr s a) -> [Encoding]
    encodePair (x :: Text
    x, y :: Expr s a
    y) = [ Text -> Encoding
    Encoding.encodeString Text
    x, Expr s a -> Encoding
    go Expr s a
    y ]

            Assert t :: Expr s a
    t ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 19)
                    (Expr s a -> Encoding
    go Expr s a
    t)

            Embed x :: a
    x ->
                a -> Encoding
    encodeEmbed a
    x

            Let a₀ :: Binding s a
    a₀ b₀ :: Expr s a
    b₀ ->
                Int -> [Encoding] -> Encoding
    encodeListN
                    (2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 3 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * NonEmpty (Binding s a) -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length NonEmpty (Binding s a)
    as)
                    ( Int -> Encoding
    Encoding.encodeInt 25
                    Encoding -> [Encoding] -> [Encoding]
    forall a. a -> [a] -> [a]
    : (Binding s a -> [Encoding]) -> [Binding s a] -> [Encoding]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Binding s a -> [Encoding]
    encodeBinding (NonEmpty (Binding s a) -> [Binding s a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList NonEmpty (Binding s a)
    as) [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++ [ Expr s a -> Encoding
    go Expr s a
    b₁ ]
                    )
              where
                MultiLet as :: NonEmpty (Binding s a)
    as b₁ :: Expr s a
    b₁ = Binding s a -> Expr s a -> MultiLet s a
    forall s a. Binding s a -> Expr s a -> MultiLet s a
    Syntax.multiLet Binding s a
    a₀ Expr s a
    b₀

                encodeBinding :: Binding s a -> [Encoding]
    encodeBinding (Binding _ x :: Text
    x _ mA₀ :: Maybe (Maybe s, Expr s a)
    mA₀ _ a :: Expr s a
    a) =
                    [ Text -> Encoding
    Encoding.encodeString Text
    x
                    , Encoding
    mA₁
                    , Expr s a -> Encoding
    go Expr s a
    a
                    ]
                  where
                    mA₁ :: Encoding
    mA₁ = case Maybe (Maybe s, Expr s a)
    mA₀ of
                        Nothing      -> Encoding
    Encoding.encodeNull
                        Just (_, _A :: Expr s a
    _A) -> Expr s a -> Encoding
    go Expr s a
    _A

            Annot t :: Expr s a
    t _T :: Expr s a
    _T ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 26)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Expr s a -> Encoding
    go Expr s a
    _T)

            ToMap t :: Expr s a
    t Nothing ->
                Encoding -> Encoding -> Encoding
    encodeList2
                    (Int -> Encoding
    Encoding.encodeInt 27)
                    (Expr s a -> Encoding
    go Expr s a
    t)

            ToMap t :: Expr s a
    t (Just _T :: Expr s a
    _T) ->
                Encoding -> Encoding -> Encoding -> Encoding
    encodeList3
                    (Int -> Encoding
    Encoding.encodeInt 27)
                    (Expr s a -> Encoding
    go Expr s a
    t)
                    (Expr s a -> Encoding
    go Expr s a
    _T)

            a :: Expr s a
    a@With{} ->
                Expr s a -> Encoding
    go (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Syntax.desugarWith Expr s a
    a)

            Note _ b :: Expr s a
    b ->
                Expr s a -> Encoding
    go Expr s a
    b

        encodeOperator :: Int -> Expr s a -> Expr s a -> Encoding
    encodeOperator n :: Int
    n l :: Expr s a
    l r :: Expr s a
    r =
            Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4
                (Int -> Encoding
    Encoding.encodeInt 3)
                (Int -> Encoding
    Encoding.encodeInt Int
    n)
                (Expr s a -> Encoding
    go Expr s a
    l)
                (Expr s a -> Encoding
    go Expr s a
    r)

        encodeMapWith :: (t -> Encoding) -> Map Text t -> Encoding
    encodeMapWith encodeValue :: t -> Encoding
    encodeValue m :: Map Text t
    m =
                Word -> Encoding
    Encoding.encodeMapLen (Int -> Word
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Map Text t -> Int
    forall k v. Map k v -> Int
    Dhall.Map.size Map Text t
    m))
            Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <>  ((Text, t) -> Encoding) -> [(Text, t)] -> Encoding
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (Text, t) -> Encoding
    encodeKeyValue (Map Text t -> [(Text, t)]
    forall k v. Ord k => Map k v -> [(k, v)]
    Dhall.Map.toList (Map Text t -> Map Text t
    forall k v. Map k v -> Map k v
    Dhall.Map.sort Map Text t
    m))
          where
            encodeKeyValue :: (Text, t) -> Encoding
    encodeKeyValue (k :: Text
    k, v :: t
    v) = Text -> Encoding
    Encoding.encodeString Text
    k Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> t -> Encoding
    encodeValue t
    v

    encodeList1 :: Encoding -> Encoding
    encodeList1 :: Encoding -> Encoding
    encodeList1 a :: Encoding
    a = Word -> Encoding
    Encoding.encodeListLen 1 Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    a
    {-# INLINE encodeList1 #-}

    encodeList2 :: Encoding -> Encoding -> Encoding
    encodeList2 :: Encoding -> Encoding -> Encoding
    encodeList2 a :: Encoding
    a b :: Encoding
    b = Word -> Encoding
    Encoding.encodeListLen 2 Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    a Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    b
    {-# INLINE encodeList2 #-}

    encodeList3 :: Encoding -> Encoding -> Encoding -> Encoding
    encodeList3 :: Encoding -> Encoding -> Encoding -> Encoding
    encodeList3 a :: Encoding
    a b :: Encoding
    b c :: Encoding
    c = Word -> Encoding
    Encoding.encodeListLen 3 Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    a Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    b Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    c
    {-# INLINE encodeList3 #-}

    encodeList4 :: Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4 :: Encoding -> Encoding -> Encoding -> Encoding -> Encoding
    encodeList4 a :: Encoding
    a b :: Encoding
    b c :: Encoding
    c d :: Encoding
    d = Word -> Encoding
    Encoding.encodeListLen 4 Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    a Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    b Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    c Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> Encoding
    d
    {-# INLINE encodeList4 #-}

    encodeListN :: Int -> [ Encoding ] -> Encoding
    encodeListN :: Int -> [Encoding] -> Encoding
    encodeListN len :: Int
    len xs :: [Encoding]
    xs = Word -> Encoding
    Encoding.encodeListLen (Int -> Word
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    len) Encoding -> Encoding -> Encoding
    forall a. Semigroup a => a -> a -> a
    <> [Encoding] -> Encoding
    forall a. Monoid a => [a] -> a
    mconcat [Encoding]
    xs
    {-# INLINE encodeListN #-}

    encodeList :: [ Encoding ] -> Encoding
    encodeList :: [Encoding] -> Encoding
    encodeList xs :: [Encoding]
    xs = Int -> [Encoding] -> Encoding
    encodeListN ([Encoding] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Encoding]
    xs) [Encoding]
    xs
    {-# INLINE encodeList #-}

    decodeImport :: Int -> Decoder s Import
    decodeImport :: Int -> Decoder s Import
    decodeImport len :: Int
    len = do
        let die :: String -> m a
    die message :: String
    message = String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Dhall.Binary.decodeImport: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    message)

        TokenType
    tokenType₀ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

        Maybe SHA256Digest
    hash <- case TokenType
    tokenType₀ of
            TypeNull -> do
                Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull

                Maybe SHA256Digest -> Decoder s (Maybe SHA256Digest)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe SHA256Digest
    forall a. Maybe a
    Nothing

            TypeBytes -> do
                ByteString
    bytes <- Decoder s ByteString
    forall s. Decoder s ByteString
    Decoding.decodeBytes

                let (prefix :: ByteString
    prefix, suffix :: ByteString
    suffix) = Int -> ByteString -> (ByteString, ByteString)
    Data.ByteString.splitAt 2 ByteString
    bytes

                case ByteString
    prefix of
                    "\x12\x20" -> () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                    _          -> String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unrecognized multihash prefix: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> ByteString -> String
    forall a. Show a => a -> String
    show ByteString
    prefix)
                case ByteString -> Maybe SHA256Digest
    Dhall.Crypto.sha256DigestFromByteString ByteString
    suffix of
                    Nothing     -> String -> Decoder s (Maybe SHA256Digest)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Invalid sha256 digest: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> ByteString -> String
    forall a. Show a => a -> String
    show ByteString
    bytes)
                    Just digest :: SHA256Digest
    digest -> Maybe SHA256Digest -> Decoder s (Maybe SHA256Digest)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SHA256Digest -> Maybe SHA256Digest
    forall a. a -> Maybe a
    Just SHA256Digest
    digest)

            _ -> do
                String -> Decoder s (Maybe SHA256Digest)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected hash token: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> TokenType -> String
    forall a. Show a => a -> String
    show TokenType
    tokenType₀)

        Word
    m <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

        ImportMode
    importMode <- case Word
    m of
            0 -> ImportMode -> Decoder s ImportMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportMode
    Code
            1 -> ImportMode -> Decoder s ImportMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportMode
    RawText
            2 -> ImportMode -> Decoder s ImportMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportMode
    Location
            _ -> String -> Decoder s ImportMode
    forall (m :: * -> *) a. MonadFail m => String -> m a
    die ("Unexpected code for import mode: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Word -> String
    forall a. Show a => a -> String
    show Word
    m)

        let remote :: Scheme -> Decoder s ImportType
    remote scheme :: Scheme
    scheme = do
                TokenType
    tokenType₁ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                Maybe (Expr Src Import)
    headers <- case TokenType
    tokenType₁ of
                    TypeNull -> do
                        Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull
                        Maybe (Expr Src Import) -> Decoder s (Maybe (Expr Src Import))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Expr Src Import)
    forall a. Maybe a
    Nothing

                    _ -> do
                        Expr Src Import
    headers <- (Int -> Decoder s Import) -> Decoder s (Expr Src Import)
    forall s a t. (Int -> Decoder s a) -> Decoder s (Expr t a)
    decodeExpressionInternal Int -> Decoder s Import
    forall s. Int -> Decoder s Import
    decodeImport

                        Maybe (Expr Src Import) -> Decoder s (Maybe (Expr Src Import))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr Src Import -> Maybe (Expr Src Import)
    forall a. a -> Maybe a
    Just Expr Src Import
    headers)

                Text
    authority <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                [Text]
    paths <- Int -> Decoder s Text -> Decoder s [Text]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 8) Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                Text
    file <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                TokenType
    tokenType₂ <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

                Maybe Text
    query <- case TokenType
    tokenType₂ of
                    TypeNull -> do
                        Decoder s ()
    forall s. Decoder s ()
    Decoding.decodeNull
                        Maybe Text -> Decoder s (Maybe Text)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Text
    forall a. Maybe a
    Nothing
                    _ -> do
                        (Text -> Maybe Text) -> Decoder s Text -> Decoder s (Maybe Text)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Text -> Maybe Text
    forall a. a -> Maybe a
    Just Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                let components :: [Text]
    components = [Text] -> [Text]
    forall a. [a] -> [a]
    reverse [Text]
    paths
                let directory :: Directory
    directory  = Directory :: [Text] -> Directory
    Directory {..}
                let path :: File
    path       = File :: Directory -> Text -> File
    File {..}

                ImportType -> Decoder s ImportType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (URL -> ImportType
    Remote (URL :: Scheme
    -> Text -> File -> Maybe Text -> Maybe (Expr Src Import) -> URL
    URL {..}))

        let local :: FilePrefix -> Decoder s ImportType
    local prefix :: FilePrefix
    prefix = do
                [Text]
    paths <- Int -> Decoder s Text -> Decoder s [Text]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    Monad.replicateM (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 5) Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                Text
    file <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                let components :: [Text]
    components = [Text] -> [Text]
    forall a. [a] -> [a]
    reverse [Text]
    paths
                let directory :: Directory
    directory  = Directory :: [Text] -> Directory
    Directory {..}

                ImportType -> Decoder s ImportType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePrefix -> File -> ImportType
    Local FilePrefix
    prefix (File :: Directory -> Text -> File
    File {..}))

        let missing :: Decoder s ImportType
    missing = ImportType -> Decoder s ImportType
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportType
    Missing

        let env :: Decoder s ImportType
    env = do
                Text
    x <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                ImportType -> Decoder s ImportType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> ImportType
    Env Text
    x)

        Word
    n <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeWord

        ImportType
    importType <- case Word
    n of
            0 -> Scheme -> Decoder s ImportType
    forall s. Scheme -> Decoder s ImportType
    remote Scheme
    HTTP
            1 -> Scheme -> Decoder s ImportType
    forall s. Scheme -> Decoder s ImportType
    remote Scheme
    HTTPS
            2 -> FilePrefix -> Decoder s ImportType
    forall s. FilePrefix -> Decoder s ImportType
    local FilePrefix
    Absolute
            3 -> FilePrefix -> Decoder s ImportType
    forall s. FilePrefix -> Decoder s ImportType
    local FilePrefix
    Here
            4 -> FilePrefix -> Decoder s ImportType
    forall s. FilePrefix -> Decoder s ImportType
    local FilePrefix
    Parent
            5 -> FilePrefix -> Decoder s ImportType
    forall s. FilePrefix -> Decoder s ImportType
    local FilePrefix
    Home
            6 -> Decoder s ImportType
    forall s. Decoder s ImportType
    env
            7 -> Decoder s ImportType
    missing
            _ -> String -> Decoder s ImportType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Unrecognized import type code: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Word -> String
    forall a. Show a => a -> String
    show Word
    n)

        let importHashed :: ImportHashed
    importHashed = ImportHashed :: Maybe SHA256Digest -> ImportType -> ImportHashed
    ImportHashed {..}

        Import -> Decoder s Import
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Import :: ImportHashed -> ImportMode -> Import
    Import {..})

    encodeImport :: Import -> Encoding
    encodeImport :: Import -> Encoding
    encodeImport import_ :: Import
    import_ =
        case ImportType
    importType of
            Remote (URL { scheme :: URL -> Scheme
    scheme = Scheme
    scheme₀, .. }) ->
                [Encoding] -> Encoding
    encodeList
                    (   [Encoding]
    prefix
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  [ Int -> Encoding
    Encoding.encodeInt Int
    scheme₁
                        , Encoding
    using
                        , Text -> Encoding
    Encoding.encodeString Text
    authority
                        ]
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  (Text -> Encoding) -> [Text] -> [Encoding]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Encoding
    Encoding.encodeString ([Text] -> [Text]
    forall a. [a] -> [a]
    reverse [Text]
    components)
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  [ Text -> Encoding
    Encoding.encodeString Text
    file ]
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  [ case Maybe Text
    query of
                             Nothing -> Encoding
    Encoding.encodeNull
                             Just q :: Text
    q  -> Text -> Encoding
    Encoding.encodeString Text
    q
                        ]
                    )
              where
                using :: Encoding
    using = case Maybe (Expr Src Import)
    headers of
                    Nothing ->
                        Encoding
    Encoding.encodeNull
                    Just h :: Expr Src Import
    h ->
                        (Import -> Encoding) -> Expr Void Import -> Encoding
    forall a. (a -> Encoding) -> Expr Void a -> Encoding
    encodeExpressionInternal Import -> Encoding
    encodeImport (Expr Src Import -> Expr Void Import
    forall s a t. Expr s a -> Expr t a
    Syntax.denote Expr Src Import
    h)

                scheme₁ :: Int
    scheme₁ = case Scheme
    scheme₀ of
                    HTTP  -> 0
                    HTTPS -> 1

                File{..} = File
    path

                Directory {..} = Directory
    directory

            Local prefix₀ :: FilePrefix
    prefix₀ path :: File
    path ->
                [Encoding] -> Encoding
    encodeList
                    (   [Encoding]
    prefix
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  [ Int -> Encoding
    Encoding.encodeInt Int
    prefix₁ ]
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  (Text -> Encoding) -> [Text] -> [Encoding]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Encoding
    Encoding.encodeString [Text]
    components₁
                    [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++  [ Text -> Encoding
    Encoding.encodeString Text
    file ]
                    )
              where
                File{..} = File
    path

                Directory{..} = Directory
    directory

                prefix₁ :: Int
    prefix₁ = case FilePrefix
    prefix₀ of
                    Absolute -> 2
                    Here     -> 3
                    Parent   -> 4
                    Home     -> 5

                components₁ :: [Text]
    components₁ = [Text] -> [Text]
    forall a. [a] -> [a]
    reverse [Text]
    components

            Env x :: Text
    x ->
                [Encoding] -> Encoding
    encodeList
                    ([Encoding]
    prefix [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++ [ Int -> Encoding
    Encoding.encodeInt 6, Text -> Encoding
    Encoding.encodeString Text
    x ])

            Missing ->
                [Encoding] -> Encoding
    encodeList ([Encoding]
    prefix [Encoding] -> [Encoding] -> [Encoding]
    forall a. [a] -> [a] -> [a]
    ++ [ Int -> Encoding
    Encoding.encodeInt 7 ])
      where
        prefix :: [Encoding]
    prefix = [ Int -> Encoding
    Encoding.encodeInt 24, Encoding
    h, Encoding
    m ]
          where
            h :: Encoding
    h = case Maybe SHA256Digest
    hash of
                Nothing ->
                    Encoding
    Encoding.encodeNull

                Just digest :: SHA256Digest
    digest ->
                    ByteString -> Encoding
    Encoding.encodeBytes ("\x12\x20" ByteString -> ByteString -> ByteString
    forall a. Semigroup a => a -> a -> a
    <> SHA256Digest -> ByteString
    forall bin bout.
    (ByteArrayAccess bin, ByteArray bout) =>
    bin -> bout
    Data.ByteArray.convert SHA256Digest
    digest)

            m :: Encoding
    m = Int -> Encoding
    Encoding.encodeInt (case ImportMode
    importMode of Code -> 0; RawText -> 1; Location -> 2;)

        Import{..} = Import
    import_

        ImportHashed{..} = ImportHashed
    importHashed

    decodeVoid :: Int -> Decoder s Void
    decodeVoid :: Int -> Decoder s Void
    decodeVoid _ = String -> Decoder s Void
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Dhall.Binary.decodeVoid: Cannot decode an uninhabited type"

    encodeVoid :: Void -> Encoding
    encodeVoid :: Void -> Encoding
    encodeVoid = Void -> Encoding
    forall a. Void -> a
    absurd

    instance Serialise (Expr Void Void) where
        encode :: Expr Void Void -> Encoding
    encode = (Void -> Encoding) -> Expr Void Void -> Encoding
    forall a. (a -> Encoding) -> Expr Void a -> Encoding
    encodeExpressionInternal Void -> Encoding
    encodeVoid

        decode :: Decoder s (Expr Void Void)
    decode = (Int -> Decoder s Void) -> Decoder s (Expr Void Void)
    forall s a t. (Int -> Decoder s a) -> Decoder s (Expr t a)
    decodeExpressionInternal Int -> Decoder s Void
    forall s. Int -> Decoder s Void
    decodeVoid

    instance Serialise (Expr Void Import) where
        encode :: Expr Void Import -> Encoding
    encode = (Import -> Encoding) -> Expr Void Import -> Encoding
    forall a. (a -> Encoding) -> Expr Void a -> Encoding
    encodeExpressionInternal Import -> Encoding
    encodeImport

        decode :: Decoder s (Expr Void Import)
    decode = (Int -> Decoder s Import) -> Decoder s (Expr Void Import)
    forall s a t. (Int -> Decoder s a) -> Decoder s (Expr t a)
    decodeExpressionInternal Int -> Decoder s Import
    forall s. Int -> Decoder s Import
    decodeImport

    -- | Encode a Dhall expression as a CBOR-encoded `ByteString`
    encodeExpression :: Expr Void Import -> ByteString
    encodeExpression :: Expr Void Import -> ByteString
    encodeExpression = Expr Void Import -> ByteString
    forall a. Serialise a => a -> ByteString
    Serialise.serialise

    -- | Decode a Dhall expression from a CBOR `Term`
    decodeExpression
        :: Serialise (Expr s a) => ByteString -> Either DecodingFailure (Expr s a)
    decodeExpression :: ByteString -> Either DecodingFailure (Expr s a)
    decodeExpression bytes :: ByteString
    bytes =
        case Maybe (Expr s a)
    decodeWithoutVersion Maybe (Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Maybe (Expr s a)
    decodeWithVersion of
            Just expression :: Expr s a
    expression -> Expr s a -> Either DecodingFailure (Expr s a)
    forall a b. b -> Either a b
    Right Expr s a
    expression
            Nothing         -> DecodingFailure -> Either DecodingFailure (Expr s a)
    forall a b. a -> Either a b
    Left (ByteString -> DecodingFailure
    CBORIsNotDhall ByteString
    bytes)
      where
        adapt :: Either a (a, a) -> Maybe a
    adapt (Right ("", x :: a
    x)) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x
        adapt  _              = Maybe a
    forall a. Maybe a
    Nothing

        decode' :: Decoder s (Expr s a)
    decode' = Decoder s (Expr s a) -> Decoder s (Expr s a)
    forall s a. Decoder s a -> Decoder s a
    decodeWith55799Tag Decoder s (Expr s a)
    forall a s. Serialise a => Decoder s a
    decode

        -- This is the behavior specified by the standard
        decodeWithoutVersion :: Maybe (Expr s a)
    decodeWithoutVersion = Either DeserialiseFailure (ByteString, Expr s a)
    -> Maybe (Expr s a)
    forall a a a. (Eq a, IsString a) => Either a (a, a) -> Maybe a
    adapt ((forall s. Decoder s (Expr s a))
    -> ByteString -> Either DeserialiseFailure (ByteString, Expr s a)
    forall a.
    (forall s. Decoder s a)
    -> ByteString -> Either DeserialiseFailure (ByteString, a)
    Read.deserialiseFromBytes forall s. Decoder s (Expr s a)
    decode' ByteString
    bytes)

        -- tag to ease the migration
        decodeWithVersion :: Maybe (Expr s a)
    decodeWithVersion = Either DeserialiseFailure (ByteString, Expr s a)
    -> Maybe (Expr s a)
    forall a a a. (Eq a, IsString a) => Either a (a, a) -> Maybe a
    adapt ((forall s. Decoder s (Expr s a))
    -> ByteString -> Either DeserialiseFailure (ByteString, Expr s a)
    forall a.
    (forall s. Decoder s a)
    -> ByteString -> Either DeserialiseFailure (ByteString, a)
    Read.deserialiseFromBytes forall s. Decoder s (Expr s a)
    decodeWithTag ByteString
    bytes)
          where
            decodeWithTag :: Decoder s (Expr s a)
    decodeWithTag = do
                Int
    2 <- Decoder s Int
    forall s. Decoder s Int
    Decoding.decodeListLen

                Text
    version <- Decoder s Text
    forall s. Decoder s Text
    Decoding.decodeString

                -- "_" has never been a valid version string, and this ensures that
                -- we don't interpret `[ "_", 0 ]` as the expression `_` (encoded as
                -- `0`) tagged with a version string of `"_"`
                if (Text
    version Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "_")
                    then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Dhall.Binary.decodeExpression: \"_\" is not a valid version string"
                    else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                Decoder s (Expr s a)
    forall s. Decoder s (Expr s a)
    decode'

    decodeWith55799Tag :: Decoder s a -> Decoder s a
    decodeWith55799Tag :: Decoder s a -> Decoder s a
    decodeWith55799Tag decoder :: Decoder s a
    decoder = do
        TokenType
    tokenType <- Decoder s TokenType
    forall s. Decoder s TokenType
    Decoding.peekTokenType

        case TokenType
    tokenType of
            TypeTag -> do
                Word
    w <- Decoder s Word
    forall s. Decoder s Word
    Decoding.decodeTag

                if Word
    w Word -> Word -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 55799
                    then String -> Decoder s ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Dhall.Binary.decodeWith55799Tag: Unexpected tag: " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> Word -> String
    forall a. Show a => a -> String
    show Word
    w)
                    else () -> Decoder s ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                Decoder s a
    decoder
            _ -> do
                Decoder s a
    decoder

    {-| This indicates that a given CBOR-encoded `ByteString` did not correspond to
        a valid Dhall expression
    -}
    newtype DecodingFailure = CBORIsNotDhall ByteString
        deriving (DecodingFailure -> DecodingFailure -> Bool
    (DecodingFailure -> DecodingFailure -> Bool)
    -> (DecodingFailure -> DecodingFailure -> Bool)
    -> Eq DecodingFailure
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: DecodingFailure -> DecodingFailure -> Bool
    $c/= :: DecodingFailure -> DecodingFailure -> Bool
    == :: DecodingFailure -> DecodingFailure -> Bool
    $c== :: DecodingFailure -> DecodingFailure -> Bool
    Eq)

    instance Exception DecodingFailure

    _ERROR :: String
    _ERROR :: String
    _ERROR = "\ESC[1;31mError\ESC[0m"

    instance Show DecodingFailure where
        show :: DecodingFailure -> String
    show (CBORIsNotDhall bytes :: ByteString
    bytes) =
                String
    _ERROR String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> ": Cannot decode CBOR to Dhall\n"
            String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <>  "\n"
            String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <>  "The following bytes do not encode a valid Dhall expression\n"
            String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <>  "\n"
            String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <>  "↳ 0x" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> (Word8 -> String) -> [Word8] -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Word8 -> String
    toHex (ByteString -> [Word8]
    Data.ByteString.Lazy.unpack ByteString
    bytes) String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> "\n"
          where
            toHex :: Word8 -> String
    toHex = String -> Word8 -> String
    forall r. PrintfType r => String -> r
    Printf.printf "%02x "