    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE BangPatterns        #-}
    {-# LANGUAGE CPP                 #-}
    {-# LANGUAGE FlexibleContexts    #-}
    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE OverloadedStrings   #-}
    {-# LANGUAGE PatternSynonyms     #-}
    {-# LANGUAGE RankNTypes          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TupleSections       #-}
    {-# LANGUAGE ViewPatterns        #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -O #-}

    {-| Eval-apply environment machine with conversion checking and quoting to
        normal forms. Fairly similar to GHCI's STG machine algorithmically, but much
        simpler, with no known call optimization or environment trimming.

        Potential optimizations without changing Expr:

        * In conversion checking, get non-shadowing variables not by linear
          Env-walking, but by keeping track of Env size, and generating names which
          are known to be illegal as source-level names (to rule out shadowing).

        * Use HashMap Text chunks for large let-definitions blocks. "Large" vs
          "Small" is fairly cheap to determine at evaluation time.

        Potential optimizations with changing Expr:

        * Use actual full de Bruijn indices in Var instead of Text counting indices.
          Then, we'd switch to full de Bruijn levels in Val as well, and use proper
          constant time non-shadowing name generation.
    -}

    module Dhall.Eval (
        judgmentallyEqual
      , normalize
      , alphaNormalize
      , eval
      , quote
      , envNames
      , countNames
      , conv
      , toVHPi
      , Closure(..)
      , Names(..)
      , Environment(..)
      , Val(..)
      , (~>)
      , textShow
      ) where

    import Data.Foldable (foldr', toList)
    import Data.Semigroup (Semigroup(..))
    import Data.Sequence (Seq, ViewL(..), ViewR(..))
    import Data.Text (Text)
    import Data.Void (Void)
    import Dhall.Map (Map)
    import Dhall.Set (Set)
    import GHC.Natural (Natural)
    import Prelude hiding (succ)

    import Dhall.Syntax
      ( Binding(..)
      , Expr(..)
      , Chunks(..)
      , Const(..)
      , DhallDouble(..)
      , PreferAnnotation(..)
      , Var(..)
      )

    import qualified Data.Char
    import qualified Data.Sequence   as Sequence
    import qualified Data.Set
    import qualified Data.Text       as Text
    import qualified Dhall.Syntax    as Syntax
    import qualified Dhall.Map       as Map
    import qualified Dhall.Set
    import qualified Text.Printf

    data Environment a
        = Empty
        | Skip   !(Environment a) {-# UNPACK #-} !Text
        | Extend !(Environment a) {-# UNPACK #-} !Text (Val a)

    deriving instance (Show a, Show (Val a -> Val a)) => Show (Environment a)

    errorMsg :: String
    errorMsg :: String
    errorMsg = [String] -> String
    unlines
      [ String
    _ERROR String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> ": Compiler bug                                                        "
      , "                                                                                "
      , "An ill-typed expression was encountered during normalization.                   "
      , "Explanation: This error message means that there is a bug in the Dhall compiler."
      , "You didn't do anything wrong, but if you would like to see this problem fixed   "
      , "then you should report the bug at:                                              "
      , "                                                                                "
      , "https://github.com/dhall-lang/dhall-haskell/issues                              "
      ]
      where
        _ERROR :: String
        _ERROR :: String
    _ERROR = "\ESC[1;31mError\ESC[0m"

    data Closure a = Closure !Text !(Environment a) !(Expr Void a)

    deriving instance (Show a, Show (Val a -> Val a)) => Show (Closure a)

    data VChunks a = VChunks ![(Text, Val a)] !Text

    deriving instance (Show a, Show (Val a -> Val a)) => Show (VChunks a)

    instance Semigroup (VChunks a) where
      VChunks xys :: [(Text, Val a)]
    xys z :: Text
    z <> :: VChunks a -> VChunks a -> VChunks a
    <> VChunks [] z' :: Text
    z' = [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [(Text, Val a)]
    xys (Text
    z Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    z')
      VChunks xys :: [(Text, Val a)]
    xys z :: Text
    z <> VChunks ((x' :: Text
    x', y' :: Val a
    y'):xys' :: [(Text, Val a)]
    xys') z' :: Text
    z' = [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks ([(Text, Val a)]
    xys [(Text, Val a)] -> [(Text, Val a)] -> [(Text, Val a)]
    forall a. [a] -> [a] -> [a]
    ++ (Text
    z Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    x', Val a
    y')(Text, Val a) -> [(Text, Val a)] -> [(Text, Val a)]
    forall a. a -> [a] -> [a]
    :[(Text, Val a)]
    xys') Text
    z'

    instance Monoid (VChunks a) where
      mempty :: VChunks a
    mempty = [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] Text
    forall a. Monoid a => a
    mempty

    #if !(MIN_VERSION_base(4,11,0))
      mappend = (<>)
    #endif

    {-| Some information is lost when `eval` converts a `Lam` or a built-in function
        from the `Expr` type to a `VHLam` of the `Val` type and `quote` needs that
        information in order to reconstruct an equivalent `Expr`.  This `HLamInfo`
        type holds that extra information necessary to perform that reconstruction
    -}
    data HLamInfo a
      = Prim
      -- ^ Don't store any information
      | Typed !Text (Val a)
      -- ^ Store the original name and type of the variable bound by the `Lam`
      | NaturalSubtractZero
      -- ^ The original function was a @Natural/subtract 0@.  We need to preserve
      --   this information in case the @Natural/subtract@ ends up not being fully
      --   saturated, in which case we need to recover the unsaturated built-in

    deriving instance (Show a, Show (Val a -> Val a)) => Show (HLamInfo a)

    pattern VPrim :: (Val a -> Val a) -> Val a
    pattern $bVPrim :: (Val a -> Val a) -> Val a
    $mVPrim :: forall r a. Val a -> ((Val a -> Val a) -> r) -> (Void# -> r) -> r
    VPrim f = VHLam Prim f

    toVHPi :: Eq a => Val a -> Maybe (Text, Val a, Val a -> Val a)
    toVHPi :: Val a -> Maybe (Text, Val a, Val a -> Val a)
    toVHPi (VPi a :: Val a
    a b :: Closure a
    b@(Closure x :: Text
    x _ _)) = (Text, Val a, Val a -> Val a)
    -> Maybe (Text, Val a, Val a -> Val a)
    forall a. a -> Maybe a
    Just (Text
    x, Val a
    a, Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b)
    toVHPi (VHPi x :: Text
    x a :: Val a
    a b :: Val a -> Val a
    b             ) = (Text, Val a, Val a -> Val a)
    -> Maybe (Text, Val a, Val a -> Val a)
    forall a. a -> Maybe a
    Just (Text
    x, Val a
    a, Val a -> Val a
    b)
    toVHPi  _                        = Maybe (Text, Val a, Val a -> Val a)
    forall a. Maybe a
    Nothing

    data Val a
        = VConst !Const
        | VVar !Text !Int
        | VPrimVar
        | VApp !(Val a) !(Val a)

        | VLam (Val a) {-# UNPACK #-} !(Closure a)
        | VHLam !(HLamInfo a) !(Val a -> Val a)

        | VPi (Val a) {-# UNPACK #-} !(Closure a)
        | VHPi !Text (Val a) !(Val a -> Val a)

        | VBool
        | VBoolLit !Bool
        | VBoolAnd !(Val a) !(Val a)
        | VBoolOr !(Val a) !(Val a)
        | VBoolEQ !(Val a) !(Val a)
        | VBoolNE !(Val a) !(Val a)
        | VBoolIf !(Val a) !(Val a) !(Val a)

        | VNatural
        | VNaturalLit !Natural
        | VNaturalFold !(Val a) !(Val a) !(Val a) !(Val a)
        | VNaturalBuild !(Val a)
        | VNaturalIsZero !(Val a)
        | VNaturalEven !(Val a)
        | VNaturalOdd !(Val a)
        | VNaturalToInteger !(Val a)
        | VNaturalShow !(Val a)
        | VNaturalSubtract !(Val a) !(Val a)
        | VNaturalPlus !(Val a) !(Val a)
        | VNaturalTimes !(Val a) !(Val a)

        | VInteger
        | VIntegerLit !Integer
        | VIntegerClamp !(Val a)
        | VIntegerNegate !(Val a)
        | VIntegerShow !(Val a)
        | VIntegerToDouble !(Val a)

        | VDouble
        | VDoubleLit !DhallDouble
        | VDoubleShow !(Val a)

        | VText
        | VTextLit !(VChunks a)
        | VTextAppend !(Val a) !(Val a)
        | VTextShow !(Val a)

        | VList !(Val a)
        | VListLit !(Maybe (Val a)) !(Seq (Val a))
        | VListAppend !(Val a) !(Val a)
        | VListBuild   (Val a) !(Val a)
        | VListFold    (Val a) !(Val a) !(Val a) !(Val a) !(Val a)
        | VListLength  (Val a) !(Val a)
        | VListHead    (Val a) !(Val a)
        | VListLast    (Val a) !(Val a)
        | VListIndexed (Val a) !(Val a)
        | VListReverse (Val a) !(Val a)

        | VOptional (Val a)
        | VSome (Val a)
        | VNone (Val a)
        | VOptionalFold (Val a) !(Val a) (Val a) !(Val a) !(Val a)
        | VOptionalBuild (Val a) !(Val a)
        | VRecord !(Map Text (Val a))
        | VRecordLit !(Map Text (Val a))
        | VUnion !(Map Text (Maybe (Val a)))
        | VCombine !(Maybe Text) !(Val a) !(Val a)
        | VCombineTypes !(Val a) !(Val a)
        | VPrefer !(Val a) !(Val a)
        | VMerge !(Val a) !(Val a) !(Maybe (Val a))
        | VToMap !(Val a) !(Maybe (Val a))
        | VField !(Val a) !Text
        | VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
        | VProject !(Val a) !(Either (Set Text) (Val a))
        | VAssert !(Val a)
        | VEquivalent !(Val a) !(Val a)
        | VEmbed a

    -- | For use with "Text.Show.Functions".
    deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a)

    (~>) :: Val a -> Val a -> Val a
    ~> :: Val a -> Val a -> Val a
    (~>) a :: Val a
    a b :: Val a
    b = Text -> Val a -> (Val a -> Val a) -> Val a
    forall a. Text -> Val a -> (Val a -> Val a) -> Val a
    VHPi "_" Val a
    a (\_ -> Val a
    b)
    {-# INLINE (~>) #-}

    infixr 5 ~>

    countEnvironment :: Text -> Environment a -> Int
    countEnvironment :: Text -> Environment a -> Int
    countEnvironment x :: Text
    x = Int -> Environment a -> Int
    forall a a. Num a => a -> Environment a -> a
    go (0 :: Int)
      where
        go :: a -> Environment a -> a
    go !a
    acc Empty             = a
    acc
        go  acc :: a
    acc (Skip env :: Environment a
    env x' :: Text
    x'    ) = a -> Environment a -> a
    go (if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' then a
    acc a -> a -> a
    forall a. Num a => a -> a -> a
    + 1 else a
    acc) Environment a
    env
        go  acc :: a
    acc (Extend env :: Environment a
    env x' :: Text
    x' _) = a -> Environment a -> a
    go (if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' then a
    acc a -> a -> a
    forall a. Num a => a -> a -> a
    + 1 else a
    acc) Environment a
    env

    instantiate :: Eq a => Closure a -> Val a -> Val a
    instantiate :: Closure a -> Val a -> Val a
    instantiate (Closure x :: Text
    x env :: Environment a
    env t :: Expr Void a
    t) !Val a
    u = Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval (Environment a -> Text -> Val a -> Environment a
    forall a. Environment a -> Text -> Val a -> Environment a
    Extend Environment a
    env Text
    x Val a
    u) Expr Void a
    t
    {-# INLINE instantiate #-}

    -- Out-of-env variables have negative de Bruijn levels.
    vVar :: Environment a -> Var -> Val a
    vVar :: Environment a -> Var -> Val a
    vVar env0 :: Environment a
    env0 (V x :: Text
    x i0 :: Int
    i0) = Environment a -> Int -> Val a
    forall a. Environment a -> Int -> Val a
    go Environment a
    env0 Int
    i0
      where
        go :: Environment a -> Int -> Val a
    go (Extend env :: Environment a
    env x' :: Text
    x' v :: Val a
    v) i :: Int
    i
            | Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' =
                if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then Val a
    v else Environment a -> Int -> Val a
    go Environment a
    env (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
            | Bool
    otherwise =
                Environment a -> Int -> Val a
    go Environment a
    env Int
    i
        go (Skip env :: Environment a
    env x' :: Text
    x') i :: Int
    i
            | Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' =
                if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then Text -> Int -> Val a
    forall a. Text -> Int -> Val a
    VVar Text
    x (Text -> Environment a -> Int
    forall a. Text -> Environment a -> Int
    countEnvironment Text
    x Environment a
    env) else Environment a -> Int -> Val a
    go Environment a
    env (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
            | Bool
    otherwise =
                Environment a -> Int -> Val a
    go Environment a
    env Int
    i
        go Empty i :: Int
    i =
            Text -> Int -> Val a
    forall a. Text -> Int -> Val a
    VVar Text
    x (0 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)

    vApp :: Eq a => Val a -> Val a -> Val a
    vApp :: Val a -> Val a -> Val a
    vApp !Val a
    t !Val a
    u =
        case Val a
    t of
            VLam _ t' :: Closure a
    t'  -> Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t' Val a
    u
            VHLam _ t' :: Val a -> Val a
    t' -> Val a -> Val a
    t' Val a
    u
            t' :: Val a
    t'        -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VApp Val a
    t' Val a
    u
    {-# INLINE vApp #-}

    vPrefer :: Eq a => Environment a -> Val a -> Val a -> Val a
    vPrefer :: Environment a -> Val a -> Val a -> Val a
    vPrefer env :: Environment a
    env t :: Val a
    t u :: Val a
    u =
        case (Val a
    t, Val a
    u) of
            (VRecordLit m :: Map Text (Val a)
    m, u' :: Val a
    u') | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    u'
            (t' :: Val a
    t', VRecordLit m :: Map Text (Val a)
    m) | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    t'
            (VRecordLit m :: Map Text (Val a)
    m, VRecordLit m' :: Map Text (Val a)
    m') ->
                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit (Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
    forall k v. Ord k => Map k v -> Map k v -> Map k v
    Map.union Map Text (Val a)
    m' Map Text (Val a)
    m)
            (t' :: Val a
    t', u' :: Val a
    u') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    u' ->
                Val a
    t'
            (t' :: Val a
    t', u' :: Val a
    u') ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VPrefer Val a
    t' Val a
    u'
    {-# INLINE vPrefer #-}

    vCombine :: Maybe Text -> Val a -> Val a -> Val a
    vCombine :: Maybe Text -> Val a -> Val a -> Val a
    vCombine mk :: Maybe Text
    mk t :: Val a
    t u :: Val a
    u =
        case (Val a
    t, Val a
    u) of
            (VRecordLit m :: Map Text (Val a)
    m, u' :: Val a
    u') | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    u'
            (t' :: Val a
    t', VRecordLit m :: Map Text (Val a)
    m) | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    t'
            (VRecordLit m :: Map Text (Val a)
    m, VRecordLit m' :: Map Text (Val a)
    m') ->
                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit ((Val a -> Val a -> Val a)
    -> Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Map.unionWith (Maybe Text -> Val a -> Val a -> Val a
    forall a. Maybe Text -> Val a -> Val a -> Val a
    vCombine Maybe Text
    forall a. Maybe a
    Nothing) Map Text (Val a)
    m Map Text (Val a)
    m')
            (t' :: Val a
    t', u' :: Val a
    u') ->
                Maybe Text -> Val a -> Val a -> Val a
    forall a. Maybe Text -> Val a -> Val a -> Val a
    VCombine Maybe Text
    mk Val a
    t' Val a
    u'

    vCombineTypes :: Val a -> Val a -> Val a
    vCombineTypes :: Val a -> Val a -> Val a
    vCombineTypes t :: Val a
    t u :: Val a
    u =
        case (Val a
    t, Val a
    u) of
            (VRecord m :: Map Text (Val a)
    m, u' :: Val a
    u') | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    u'
            (t' :: Val a
    t', VRecord m :: Map Text (Val a)
    m) | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                Val a
    t'
            (VRecord m :: Map Text (Val a)
    m, VRecord m' :: Map Text (Val a)
    m') ->
                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecord ((Val a -> Val a -> Val a)
    -> Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Map.unionWith Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vCombineTypes Map Text (Val a)
    m Map Text (Val a)
    m')
            (t' :: Val a
    t', u' :: Val a
    u') ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VCombineTypes Val a
    t' Val a
    u'

    vListAppend :: Val a -> Val a -> Val a
    vListAppend :: Val a -> Val a -> Val a
    vListAppend t :: Val a
    t u :: Val a
    u =
        case (Val a
    t, Val a
    u) of
            (VListLit _ xs :: Seq (Val a)
    xs, u' :: Val a
    u') | Seq (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Val a)
    xs ->
                Val a
    u'
            (t' :: Val a
    t', VListLit _ ys :: Seq (Val a)
    ys) | Seq (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Val a)
    ys ->
                Val a
    t'
            (VListLit t' :: Maybe (Val a)
    t' xs :: Seq (Val a)
    xs, VListLit _ ys :: Seq (Val a)
    ys) ->
                Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    t' (Seq (Val a)
    xs Seq (Val a) -> Seq (Val a) -> Seq (Val a)
    forall a. Semigroup a => a -> a -> a
    <> Seq (Val a)
    ys)
            (t' :: Val a
    t', u' :: Val a
    u') ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListAppend Val a
    t' Val a
    u'
    {-# INLINE vListAppend #-}

    vNaturalPlus :: Val a -> Val a -> Val a
    vNaturalPlus :: Val a -> Val a -> Val a
    vNaturalPlus t :: Val a
    t u :: Val a
    u =
        case (Val a
    t, Val a
    u) of
            (VNaturalLit 0, u' :: Val a
    u') ->
                Val a
    u'
            (t' :: Val a
    t', VNaturalLit 0) ->
                Val a
    t'
            (VNaturalLit m :: Natural
    m, VNaturalLit n :: Natural
    n) ->
                Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    n)
            (t' :: Val a
    t', u' :: Val a
    u') ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VNaturalPlus Val a
    t' Val a
    u'
    {-# INLINE vNaturalPlus #-}

    vField :: Val a -> Text -> Val a
    vField :: Val a -> Text -> Val a
    vField t0 :: Val a
    t0 k :: Text
    k = Val a -> Val a
    forall a. Val a -> Val a
    go Val a
    t0
      where
        go :: Val a -> Val a
    go = \case
            VUnion m :: Map Text (Maybe (Val a))
    m -> case Text -> Map Text (Maybe (Val a)) -> Maybe (Maybe (Val a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Maybe (Val a))
    m of
                Just (Just _) -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ ~Val a
    u -> Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
    forall a.
    Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
    VInject Map Text (Maybe (Val a))
    m Text
    k (Val a -> Maybe (Val a)
    forall a. a -> Maybe a
    Just Val a
    u)
                Just Nothing  -> Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
    forall a.
    Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
    VInject Map Text (Maybe (Val a))
    m Text
    k Maybe (Val a)
    forall a. Maybe a
    Nothing
                _             -> String -> Val a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
            VRecordLit m :: Map Text (Val a)
    m
                | Just v :: Val a
    v <- Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m -> Val a
    v
                | Bool
    otherwise -> String -> Val a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
            VProject t :: Val a
    t _ -> Val a -> Val a
    go Val a
    t
            VPrefer (VRecordLit m :: Map Text (Val a)
    m) r :: Val a
    r -> case Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m of
                Just v :: Val a
    v -> Val a -> Text -> Val a
    forall a. Val a -> Text -> Val a
    VField (Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VPrefer (Val a -> Val a
    forall a. Val a -> Val a
    singletonVRecordLit Val a
    v) Val a
    r) Text
    k
                Nothing -> Val a -> Val a
    go Val a
    r
            VPrefer l :: Val a
    l (VRecordLit m :: Map Text (Val a)
    m) -> case Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m of
                Just v :: Val a
    v -> Val a
    v
                Nothing -> Val a -> Val a
    go Val a
    l
            VCombine mk :: Maybe Text
    mk (VRecordLit m :: Map Text (Val a)
    m) r :: Val a
    r -> case Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m of
                Just v :: Val a
    v -> Val a -> Text -> Val a
    forall a. Val a -> Text -> Val a
    VField (Maybe Text -> Val a -> Val a -> Val a
    forall a. Maybe Text -> Val a -> Val a -> Val a
    VCombine Maybe Text
    mk (Val a -> Val a
    forall a. Val a -> Val a
    singletonVRecordLit Val a
    v) Val a
    r) Text
    k
                Nothing -> Val a -> Val a
    go Val a
    r
            VCombine mk :: Maybe Text
    mk l :: Val a
    l (VRecordLit m :: Map Text (Val a)
    m) -> case Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m of
                Just v :: Val a
    v -> Val a -> Text -> Val a
    forall a. Val a -> Text -> Val a
    VField (Maybe Text -> Val a -> Val a -> Val a
    forall a. Maybe Text -> Val a -> Val a -> Val a
    VCombine Maybe Text
    mk Val a
    l (Val a -> Val a
    forall a. Val a -> Val a
    singletonVRecordLit Val a
    v)) Text
    k
                Nothing -> Val a -> Val a
    go Val a
    l
            t :: Val a
    t -> Val a -> Text -> Val a
    forall a. Val a -> Text -> Val a
    VField Val a
    t Text
    k

        singletonVRecordLit :: Val a -> Val a
    singletonVRecordLit v :: Val a
    v = Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit (Text -> Val a -> Map Text (Val a)
    forall k v. k -> v -> Map k v
    Map.singleton Text
    k Val a
    v)
    {-# INLINE vField #-}

    vProjectByFields :: Eq a => Environment a -> Val a -> Set Text -> Val a
    vProjectByFields :: Environment a -> Val a -> Set Text -> Val a
    vProjectByFields env :: Environment a
    env t :: Val a
    t ks :: Set Text
    ks =
        if Set Text -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set Text
    ks
            then Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit Map Text (Val a)
    forall a. Monoid a => a
    mempty
            else case Val a
    t of
                VRecordLit kvs :: Map Text (Val a)
    kvs ->
                    let kvs' :: Map Text (Val a)
    kvs' = Map Text (Val a) -> Set Text -> Map Text (Val a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Map.restrictKeys Map Text (Val a)
    kvs (Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.toSet Set Text
    ks)
                    in  Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit Map Text (Val a)
    kvs'
                VProject t' :: Val a
    t' _ ->
                    Environment a -> Val a -> Set Text -> Val a
    forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
    vProjectByFields Environment a
    env Val a
    t' Set Text
    ks
                VPrefer l :: Val a
    l (VRecordLit kvs :: Map Text (Val a)
    kvs) ->
                    let ksSet :: Set Text
    ksSet = Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.toSet Set Text
    ks

                        kvs' :: Map Text (Val a)
    kvs' = Map Text (Val a) -> Set Text -> Map Text (Val a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Map.restrictKeys Map Text (Val a)
    kvs Set Text
    ksSet

                        ks' :: Set Text
    ks' =
                            Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.fromSet
                                (Set Text -> Set Text -> Set Text
    forall a. Ord a => Set a -> Set a -> Set a
    Data.Set.difference Set Text
    ksSet (Map Text (Val a) -> Set Text
    forall k v. Map k v -> Set k
    Map.keysSet Map Text (Val a)
    kvs'))

                    in  Environment a -> Val a -> Val a -> Val a
    forall a. Eq a => Environment a -> Val a -> Val a -> Val a
    vPrefer Environment a
    env (Environment a -> Val a -> Set Text -> Val a
    forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
    vProjectByFields Environment a
    env Val a
    l Set Text
    ks') (Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit Map Text (Val a)
    kvs')
                t' :: Val a
    t' ->
                    Val a -> Either (Set Text) (Val a) -> Val a
    forall a. Val a -> Either (Set Text) (Val a) -> Val a
    VProject Val a
    t' (Set Text -> Either (Set Text) (Val a)
    forall a b. a -> Either a b
    Left Set Text
    ks)

    eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval :: Environment a -> Expr Void a -> Val a
    eval !Environment a
    env t0 :: Expr Void a
    t0 =
        case Expr Void a
    t0 of
            Const k :: Const
    k ->
                Const -> Val a
    forall a. Const -> Val a
    VConst Const
    k
            Var v :: Var
    v ->
                Environment a -> Var -> Val a
    forall a. Environment a -> Var -> Val a
    vVar Environment a
    env Var
    v
            Lam x :: Text
    x a :: Expr Void a
    a t :: Expr Void a
    t ->
                Val a -> Closure a -> Val a
    forall a. Val a -> Closure a -> Val a
    VLam (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    a) (Text -> Environment a -> Expr Void a -> Closure a
    forall a. Text -> Environment a -> Expr Void a -> Closure a
    Closure Text
    x Environment a
    env Expr Void a
    t)
            Pi x :: Text
    x a :: Expr Void a
    a b :: Expr Void a
    b ->
                Val a -> Closure a -> Val a
    forall a. Val a -> Closure a -> Val a
    VPi (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    a) (Text -> Environment a -> Expr Void a -> Closure a
    forall a. Text -> Environment a -> Expr Void a -> Closure a
    Closure Text
    x Environment a
    env Expr Void a
    b)
            App t :: Expr Void a
    t u :: Expr Void a
    u ->
                Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            Let (Binding _ x :: Text
    x _ _mA :: Maybe (Maybe Void, Expr Void a)
    _mA _ a :: Expr Void a
    a) b :: Expr Void a
    b ->
                let !env' :: Environment a
    env' = Environment a -> Text -> Val a -> Environment a
    forall a. Environment a -> Text -> Val a -> Environment a
    Extend Environment a
    env Text
    x (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    a)
                in  Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env' Expr Void a
    b
            Annot t :: Expr Void a
    t _ ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t
            Bool ->
                Val a
    forall a. Val a
    VBool
            BoolLit b :: Bool
    b ->
                Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    b
            BoolAnd t :: Expr Void a
    t u :: Expr Void a
    u ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u) of
                    (VBoolLit True, u' :: Val a
    u')       -> Val a
    u'
                    (VBoolLit False, _)       -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    False
                    (t' :: Val a
    t', VBoolLit True)       -> Val a
    t'
                    (_ , VBoolLit False)      -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    False
                    (t' :: Val a
    t', u' :: Val a
    u') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    u' -> Val a
    t'
                    (t' :: Val a
    t', u' :: Val a
    u')                  -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VBoolAnd Val a
    t' Val a
    u'
            BoolOr t :: Expr Void a
    t u :: Expr Void a
    u ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u) of
                    (VBoolLit False, u' :: Val a
    u')      -> Val a
    u'
                    (VBoolLit True, _)        -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    True
                    (t' :: Val a
    t', VBoolLit False)      -> Val a
    t'
                    (_ , VBoolLit True)       -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    True
                    (t' :: Val a
    t', u' :: Val a
    u') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    u' -> Val a
    t'
                    (t' :: Val a
    t', u' :: Val a
    u')                  -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VBoolOr Val a
    t' Val a
    u'
            BoolEQ t :: Expr Void a
    t u :: Expr Void a
    u ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u) of
                    (VBoolLit True, u' :: Val a
    u')       -> Val a
    u'
                    (t' :: Val a
    t', VBoolLit True)       -> Val a
    t'
                    (t' :: Val a
    t', u' :: Val a
    u') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    u' -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    True
                    (t' :: Val a
    t', u' :: Val a
    u')                  -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VBoolEQ Val a
    t' Val a
    u'
            BoolNE t :: Expr Void a
    t u :: Expr Void a
    u ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u) of
                    (VBoolLit False, u' :: Val a
    u')      -> Val a
    u'
                    (t' :: Val a
    t', VBoolLit False)      -> Val a
    t'
                    (t' :: Val a
    t', u' :: Val a
    u') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    u' -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit Bool
    False
                    (t' :: Val a
    t', u' :: Val a
    u')                  -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VBoolNE Val a
    t' Val a
    u'
            BoolIf b :: Expr Void a
    b t :: Expr Void a
    t f :: Expr Void a
    f ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    b, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    f) of
                    (VBoolLit True,  t' :: Val a
    t', _ )            -> Val a
    t'
                    (VBoolLit False, _ , f' :: Val a
    f')            -> Val a
    f'
                    (b' :: Val a
    b', VBoolLit True, VBoolLit False) -> Val a
    b'
                    (_, t' :: Val a
    t', f' :: Val a
    f') | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t' Val a
    f'        -> Val a
    t'
                    (b' :: Val a
    b', t' :: Val a
    t', f' :: Val a
    f')                        -> Val a -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a -> Val a
    VBoolIf Val a
    b' Val a
    t' Val a
    f'
            Natural ->
                Val a
    forall a. Val a
    VNatural
            NaturalLit n :: Natural
    n ->
                Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit Natural
    n
            NaturalFold ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \n :: Val a
    n ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \natural :: Val a
    natural ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \succ :: Val a
    succ ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \zero :: Val a
    zero ->
                let inert :: Val a
    inert = Val a -> Val a -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a -> Val a -> Val a
    VNaturalFold Val a
    n Val a
    natural Val a
    succ Val a
    zero
                in  case Val a
    zero of
                    VPrimVar -> Val a
    inert
                    _ -> case Val a
    succ of
                        VPrimVar -> Val a
    inert
                        _ -> case Val a
    natural of
                            VPrimVar -> Val a
    inert
                            _ -> case Val a
    n of
                                VNaturalLit n' :: Natural
    n' ->
                                    -- Use an `Integer` for the loop, due to the
                                    -- following issue:
                                    --
                                    -- https://github.com/ghcjs/ghcjs/issues/782
                                    let go :: Val a -> t -> Val a
    go !Val a
    acc 0 = Val a
    acc
                                        go  acc :: Val a
    acc m :: t
    m = Val a -> t -> Val a
    go (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    succ Val a
    acc) (t
    m t -> t -> t
    forall a. Num a => a -> a -> a
    - 1)
                                    in  Val a -> Integer -> Val a
    forall t. (Num t, Eq t) => Val a -> t -> Val a
    go Val a
    zero (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n' :: Integer)
                                _ -> Val a
    inert
            NaturalBuild ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VPrimVar ->
                        Val a -> Val a
    forall a. Val a -> Val a
    VNaturalBuild Val a
    forall a. Val a
    VPrimVar
                    t :: Val a
    t ->       Val a
    t
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a
    forall a. Val a
    VNatural
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "n" Val a
    forall a. Val a
    VNatural) (\n :: Val a
    n -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vNaturalPlus Val a
    n (Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 1))
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0

            NaturalIsZero -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit n :: Natural
    n -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit (Natural
    n Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0)
                n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VNaturalIsZero Val a
    n
            NaturalEven -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit n :: Natural
    n -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    even Natural
    n)
                n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VNaturalEven Val a
    n
            NaturalOdd -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit n :: Natural
    n -> Bool -> Val a
    forall a. Bool -> Val a
    VBoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    odd Natural
    n)
                n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VNaturalOdd Val a
    n
            NaturalToInteger -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit n :: Natural
    n -> Integer -> Val a
    forall a. Integer -> Val a
    VIntegerLit (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n)
                n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VNaturalToInteger Val a
    n
            NaturalShow -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit n :: Natural
    n -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit ([(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] (String -> Text
    Text.pack (Natural -> String
    forall a. Show a => a -> String
    show Natural
    n)))
                n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VNaturalShow Val a
    n
            NaturalSubtract -> (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                VNaturalLit 0 ->
                    HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam HLamInfo a
    forall a. HLamInfo a
    NaturalSubtractZero Val a -> Val a
    forall a. a -> a
    id
                x :: Val a
    x@(VNaturalLit m :: Natural
    m) ->
                    (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                        VNaturalLit n :: Natural
    n
                            | Natural
    n Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Natural
    m ->
                                -- Use an `Integer` for the subtraction, due to the
                                -- following issue:
                                --
                                -- https://github.com/ghcjs/ghcjs/issues/782
                                Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Integer -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    subtract (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    m :: Integer) (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n :: Integer)))
                            | Bool
    otherwise -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                        y :: Val a
    y -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VNaturalSubtract Val a
    x Val a
    y
                x :: Val a
    x ->
                    (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                        VNaturalLit 0    -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                        y :: Val a
    y | Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    x Val a
    y -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                        y :: Val a
    y                -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VNaturalSubtract Val a
    x Val a
    y
            NaturalPlus t :: Expr Void a
    t u :: Expr Void a
    u ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vNaturalPlus (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            NaturalTimes t :: Expr Void a
    t u :: Expr Void a
    u ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u) of
                    (VNaturalLit 1, u' :: Val a
    u'           ) -> Val a
    u'
                    (t' :: Val a
    t'           , VNaturalLit 1) -> Val a
    t'
                    (VNaturalLit 0, _            ) -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                    (_            , VNaturalLit 0) -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                    (VNaturalLit m :: Natural
    m, VNaturalLit n :: Natural
    n) -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    n)
                    (t' :: Val a
    t'           , u' :: Val a
    u'           ) -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VNaturalTimes Val a
    t' Val a
    u'
            Integer ->
                Val a
    forall a. Val a
    VInteger
            IntegerLit n :: Integer
    n ->
                Integer -> Val a
    forall a. Integer -> Val a
    VIntegerLit Integer
    n
            IntegerClamp ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VIntegerLit n :: Integer
    n
                        | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n    -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
                        | Bool
    otherwise -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit 0
                    n :: Val a
    n -> Val a -> Val a
    forall a. Val a -> Val a
    VIntegerClamp Val a
    n
            IntegerNegate ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VIntegerLit n :: Integer
    n -> Integer -> Val a
    forall a. Integer -> Val a
    VIntegerLit (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    n)
                    n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VIntegerNegate Val a
    n
            IntegerShow ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VIntegerLit n :: Integer
    n
                        | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n    -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit ([(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] (String -> Text
    Text.pack ('+'Char -> ShowS
    forall a. a -> [a] -> [a]
    :Integer -> String
    forall a. Show a => a -> String
    show Integer
    n)))
                        | Bool
    otherwise -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit ([(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] (String -> Text
    Text.pack (Integer -> String
    forall a. Show a => a -> String
    show Integer
    n)))
                    n :: Val a
    n -> Val a -> Val a
    forall a. Val a -> Val a
    VIntegerShow Val a
    n
            IntegerToDouble ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VIntegerLit n :: Integer
    n -> DhallDouble -> Val a
    forall a. DhallDouble -> Val a
    VDoubleLit (Double -> DhallDouble
    DhallDouble (String -> Double
    forall a. Read a => String -> a
    read (Integer -> String
    forall a. Show a => a -> String
    show Integer
    n)))
                    -- `(read . show)` is used instead of `fromInteger`
                    -- because `read` uses the correct rounding rule.
                    -- See https://gitlab.haskell.org/ghc/ghc/issues/17231.
                    n :: Val a
    n             -> Val a -> Val a
    forall a. Val a -> Val a
    VIntegerToDouble Val a
    n
            Double ->
                Val a
    forall a. Val a
    VDouble
            DoubleLit n :: DhallDouble
    n ->
                DhallDouble -> Val a
    forall a. DhallDouble -> Val a
    VDoubleLit DhallDouble
    n
            DoubleShow ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VDoubleLit (DhallDouble n :: Double
    n) -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit ([(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] (String -> Text
    Text.pack (Double -> String
    forall a. Show a => a -> String
    show Double
    n)))
                    n :: Val a
    n                          -> Val a -> Val a
    forall a. Val a -> Val a
    VDoubleShow Val a
    n
            Text ->
                Val a
    forall a. Val a
    VText
            TextLit cs :: Chunks Void a
    cs ->
                case Chunks Void a -> VChunks a
    evalChunks Chunks Void a
    cs of
                    VChunks [("", t :: Val a
    t)] "" -> Val a
    t
                    vcs :: VChunks a
    vcs                  -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit VChunks a
    vcs
            TextAppend t :: Expr Void a
    t u :: Expr Void a
    u ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env (Chunks Void a -> Expr Void a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr Void a)] -> Text -> Chunks Void a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [("", Expr Void a
    t), ("", Expr Void a
    u)] ""))
            TextShow ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VTextLit (VChunks [] x :: Text
    x) -> VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit ([(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] (Text -> Text
    textShow Text
    x))
                    t :: Val a
    t                       -> Val a -> Val a
    forall a. Val a -> Val a
    VTextShow Val a
    t
            List ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim Val a -> Val a
    forall a. Val a -> Val a
    VList
            ListLit ma :: Maybe (Expr Void a)
    ma ts :: Seq (Expr Void a)
    ts ->
                Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit ((Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Maybe (Expr Void a)
    ma) ((Expr Void a -> Val a) -> Seq (Expr Void a) -> Seq (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Seq (Expr Void a)
    ts)
            ListAppend t :: Expr Void a
    t u :: Expr Void a
    u ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vListAppend (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            ListBuild ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VPrimVar ->
                        Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListBuild Val a
    a Val a
    forall a. Val a
    VPrimVar
                    t :: Val a
    t ->       Val a
    t
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a -> Val a
    forall a. Val a -> Val a
    VList Val a
    a
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "a" Val a
    a) (\x :: Val a
    x ->
                               HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "as" (Val a -> Val a
    forall a. Val a -> Val a
    VList Val a
    a)) (\as :: Val a
    as ->
                               Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vListAppend (Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    forall a. Maybe a
    Nothing (Val a -> Seq (Val a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Val a
    x)) Val a
    as))
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit (Val a -> Maybe (Val a)
    forall a. a -> Maybe a
    Just (Val a -> Val a
    forall a. Val a -> Val a
    VList Val a
    a)) Seq (Val a)
    forall a. Monoid a => a
    mempty

            ListFold ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \as :: Val a
    as ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \list :: Val a
    list ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \cons :: Val a
    cons ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \nil :: Val a
    nil ->
                let inert :: Val a
    inert = Val a -> Val a -> Val a -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a -> Val a -> Val a -> Val a
    VListFold Val a
    a Val a
    as Val a
    list Val a
    cons Val a
    nil
                in  case Val a
    nil of
                    VPrimVar -> Val a
    inert
                    _ -> case Val a
    cons of
                        VPrimVar -> Val a
    inert
                        _ -> case Val a
    list of
                            VPrimVar -> Val a
    inert
                            _ -> case Val a
    a of
                                VPrimVar -> Val a
    inert
                                _ -> case Val a
    as of
                                    VListLit _ as' :: Seq (Val a)
    as' ->
                                        (Val a -> Val a -> Val a) -> Val a -> Seq (Val a) -> Val a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr' (\x :: Val a
    x b :: Val a
    b -> Val a
    cons Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a
    x Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a
    b) Val a
    nil Seq (Val a)
    as'
                                    _ -> Val a
    inert
            ListLength ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VListLit _ as :: Seq (Val a)
    as -> Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Seq (Val a) -> Int
    forall a. Seq a -> Int
    Sequence.length Seq (Val a)
    as))
                    as :: Val a
    as            -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListLength Val a
    a Val a
    as
            ListHead ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VListLit _ as :: Seq (Val a)
    as ->
                        case Seq (Val a) -> ViewL (Val a)
    forall a. Seq a -> ViewL a
    Sequence.viewl Seq (Val a)
    as of
                            y :: Val a
    y :< _ -> Val a -> Val a
    forall a. Val a -> Val a
    VSome Val a
    y
                            _      -> Val a -> Val a
    forall a. Val a -> Val a
    VNone Val a
    a
                    as :: Val a
    as ->
                        Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListHead Val a
    a Val a
    as
            ListLast ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VListLit _ as :: Seq (Val a)
    as ->
                        case Seq (Val a) -> ViewR (Val a)
    forall a. Seq a -> ViewR a
    Sequence.viewr Seq (Val a)
    as of
                            _ :> t :: Val a
    t -> Val a -> Val a
    forall a. Val a -> Val a
    VSome Val a
    t
                            _      -> Val a -> Val a
    forall a. Val a -> Val a
    VNone Val a
    a
                    as :: Val a
    as -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListLast Val a
    a Val a
    as
            ListIndexed ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ a :: Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VListLit _ as :: Seq (Val a)
    as ->
                        let a' :: Maybe (Val a)
    a' =
                                if Seq (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Val a)
    as
                                then Val a -> Maybe (Val a)
    forall a. a -> Maybe a
    Just (Val a -> Val a
    forall a. Val a -> Val a
    VList (Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecord ([(Text, Val a)] -> Map Text (Val a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Map.unorderedFromList [("index", Val a
    forall a. Val a
    VNatural), ("value", Val a
    a)])))
                                else Maybe (Val a)
    forall a. Maybe a
    Nothing

                            as' :: Seq (Val a)
    as' =
                                (Int -> Val a -> Val a) -> Seq (Val a) -> Seq (Val a)
    forall a b. (Int -> a -> b) -> Seq a -> Seq b
    Sequence.mapWithIndex
                                    (\i :: Int
    i t :: Val a
    t ->
                                        Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit
                                            ([(Text, Val a)] -> Map Text (Val a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Map.unorderedFromList
                                                [ ("index", Natural -> Val a
    forall a. Natural -> Val a
    VNaturalLit (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    i))
                                                , ("value", Val a
    t)
                                                ]
                                            )
                                    )
                                    Seq (Val a)
    as

                            in  Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    a' Seq (Val a)
    as'
                    t :: Val a
    t ->
                        Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListIndexed Val a
    a Val a
    t
            ListReverse ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ ~Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VListLit t :: Maybe (Val a)
    t as :: Seq (Val a)
    as | Seq (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Val a)
    as ->
                        Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    t Seq (Val a)
    as
                    VListLit _ as :: Seq (Val a)
    as ->
                        Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    forall a. Maybe a
    Nothing (Seq (Val a) -> Seq (Val a)
    forall a. Seq a -> Seq a
    Sequence.reverse Seq (Val a)
    as)
                    t :: Val a
    t ->
                        Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VListReverse Val a
    a Val a
    t
            Optional ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim Val a -> Val a
    forall a. Val a -> Val a
    VOptional
            Some t :: Expr Void a
    t ->
                Val a -> Val a
    forall a. Val a -> Val a
    VSome (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t)
            None ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ ~Val a
    a -> Val a -> Val a
    forall a. Val a -> Val a
    VNone Val a
    a
            OptionalFold ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ ~Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VNone _ ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "optional" (Const -> Val a
    forall a. Const -> Val a
    VConst Const
    Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \optional :: Val a
    optional ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "some" (Val a
    a Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    ~> Val a
    optional)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \_some :: Val a
    _some ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "none" Val a
    optional) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \none :: Val a
    none ->
                        Val a
    none
                    VSome t :: Val a
    t ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "optional" (Const -> Val a
    forall a. Const -> Val a
    VConst Const
    Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \optional :: Val a
    optional ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "some" (Val a
    a Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    ~> Val a
    optional)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \some :: Val a
    some ->
                        HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "none" Val a
    optional) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \_none :: Val a
    _none ->
                        Val a
    some Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a
    t
                    opt :: Val a
    opt ->
                        (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \o :: Val a
    o ->
                        (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \s :: Val a
    s ->
                        (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \n :: Val a
    n ->
                        Val a -> Val a -> Val a -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a -> Val a -> Val a -> Val a
    VOptionalFold Val a
    a Val a
    opt Val a
    o Val a
    s Val a
    n
            OptionalBuild ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \ ~Val a
    a ->
                (Val a -> Val a) -> Val a
    forall a. (Val a -> Val a) -> Val a
    VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
    forall a b. (a -> b) -> a -> b
    $ \case
                    VPrimVar -> Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VOptionalBuild Val a
    a Val a
    forall a. Val a
    VPrimVar
                    t :: Val a
    t ->       Val a
    t
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a -> Val a
    forall a. Val a -> Val a
    VOptional Val a
    a
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` HLamInfo a -> (Val a -> Val a) -> Val a
    forall a. HLamInfo a -> (Val a -> Val a) -> Val a
    VHLam (Text -> Val a -> HLamInfo a
    forall a. Text -> Val a -> HLamInfo a
    Typed "a" Val a
    a) Val a -> Val a
    forall a. Val a -> Val a
    VSome
                        Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    `vApp` Val a -> Val a
    forall a. Val a -> Val a
    VNone Val a
    a
            Record kts :: Map Text (Expr Void a)
    kts ->
                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecord (Map Text (Val a) -> Map Text (Val a)
    forall k v. Map k v -> Map k v
    Map.sort ((Expr Void a -> Val a)
    -> Map Text (Expr Void a) -> Map Text (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Map Text (Expr Void a)
    kts))
            RecordLit kts :: Map Text (Expr Void a)
    kts ->
                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit (Map Text (Val a) -> Map Text (Val a)
    forall k v. Map k v -> Map k v
    Map.sort ((Expr Void a -> Val a)
    -> Map Text (Expr Void a) -> Map Text (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Map Text (Expr Void a)
    kts))
            Union kts :: Map Text (Maybe (Expr Void a))
    kts ->
                Map Text (Maybe (Val a)) -> Val a
    forall a. Map Text (Maybe (Val a)) -> Val a
    VUnion (Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a))
    forall k v. Map k v -> Map k v
    Map.sort ((Maybe (Expr Void a) -> Maybe (Val a))
    -> Map Text (Maybe (Expr Void a)) -> Map Text (Maybe (Val a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env)) Map Text (Maybe (Expr Void a))
    kts))
            Combine mk :: Maybe Text
    mk t :: Expr Void a
    t u :: Expr Void a
    u ->
                Maybe Text -> Val a -> Val a -> Val a
    forall a. Maybe Text -> Val a -> Val a -> Val a
    vCombine Maybe Text
    mk (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            CombineTypes t :: Expr Void a
    t u :: Expr Void a
    u ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    vCombineTypes (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            Prefer _ t :: Expr Void a
    t u :: Expr Void a
    u ->
                Environment a -> Val a -> Val a -> Val a
    forall a. Eq a => Environment a -> Val a -> Val a -> Val a
    vPrefer Environment a
    env (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            RecordCompletion t :: Expr Void a
    t u :: Expr Void a
    u ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env (Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Annot (PreferAnnotation Void a
    -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation Void a
    forall s a. PreferAnnotation s a
    PreferFromCompletion (Expr Void a -> Text -> Expr Void a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr Void a
    t "default") Expr Void a
    u) (Expr Void a -> Text -> Expr Void a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr Void a
    t "Type"))
            Merge x :: Expr Void a
    x y :: Expr Void a
    y ma :: Maybe (Expr Void a)
    ma ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    x, Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    y, (Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Maybe (Expr Void a)
    ma) of
                    (VRecordLit m :: Map Text (Val a)
    m, VInject _ k :: Text
    k mt :: Maybe (Val a)
    mt, _)
                        | Just f :: Val a
    f <- Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup Text
    k Map Text (Val a)
    m -> Val a -> (Val a -> Val a) -> Maybe (Val a) -> Val a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Val a
    f (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    f) Maybe (Val a)
    mt
                        | Bool
    otherwise                -> String -> Val a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
                    (VRecordLit m :: Map Text (Val a)
    m, VSome t :: Val a
    t, _)
                        | Just f :: Val a
    f <- Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup "Some" Map Text (Val a)
    m -> Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    f Val a
    t
                        | Bool
    otherwise                     -> String -> Val a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
                    (VRecordLit m :: Map Text (Val a)
    m, VNone _, _)
                        | Just t :: Val a
    t <- Text -> Map Text (Val a) -> Maybe (Val a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Map.lookup "None" Map Text (Val a)
    m -> Val a
    t
                        | Bool
    otherwise                     -> String -> Val a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
                    (x' :: Val a
    x', y' :: Val a
    y', ma' :: Maybe (Val a)
    ma') -> Val a -> Val a -> Maybe (Val a) -> Val a
    forall a. Val a -> Val a -> Maybe (Val a) -> Val a
    VMerge Val a
    x' Val a
    y' Maybe (Val a)
    ma'
            ToMap x :: Expr Void a
    x ma :: Maybe (Expr Void a)
    ma ->
                case (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    x, (Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env) Maybe (Expr Void a)
    ma) of
                    (VRecordLit m :: Map Text (Val a)
    m, ma' :: Maybe (Val a)
    ma'@(Just _)) | Map Text (Val a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Text (Val a)
    m ->
                        Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    ma' Seq (Val a)
    forall a. Seq a
    Sequence.empty
                    (VRecordLit m :: Map Text (Val a)
    m, _) ->
                        let entry :: (Text, Val a) -> Val a
    entry (k :: Text
    k, v :: Val a
    v) =
                                Map Text (Val a) -> Val a
    forall a. Map Text (Val a) -> Val a
    VRecordLit
                                    ([(Text, Val a)] -> Map Text (Val a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Map.unorderedFromList
                                        [ ("mapKey", VChunks a -> Val a
    forall a. VChunks a -> Val a
    VTextLit (VChunks a -> Val a) -> VChunks a -> Val a
    forall a b. (a -> b) -> a -> b
    $ [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] Text
    k)
                                        , ("mapValue", Val a
    v)
                                        ]
                                    )

                            s :: Seq (Val a)
    s = ([Val a] -> Seq (Val a)
    forall a. [a] -> Seq a
    Sequence.fromList ([Val a] -> Seq (Val a))
    -> (Map Text (Val a) -> [Val a]) -> Map Text (Val a) -> Seq (Val a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Text, Val a) -> Val a) -> [(Text, Val a)] -> [Val a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text, Val a) -> Val a
    forall a. (Text, Val a) -> Val a
    entry ([(Text, Val a)] -> [Val a])
    -> (Map Text (Val a) -> [(Text, Val a)])
    -> Map Text (Val a)
    -> [Val a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (Val a) -> [(Text, Val a)]
    forall k v. Map k v -> [(k, v)]
    Map.toAscList) Map Text (Val a)
    m

                        in  Maybe (Val a) -> Seq (Val a) -> Val a
    forall a. Maybe (Val a) -> Seq (Val a) -> Val a
    VListLit Maybe (Val a)
    forall a. Maybe a
    Nothing Seq (Val a)
    s
                    (x' :: Val a
    x', ma' :: Maybe (Val a)
    ma') ->
                        Val a -> Maybe (Val a) -> Val a
    forall a. Val a -> Maybe (Val a) -> Val a
    VToMap Val a
    x' Maybe (Val a)
    ma'
            Field t :: Expr Void a
    t k :: Text
    k ->
                Val a -> Text -> Val a
    forall a. Val a -> Text -> Val a
    vField (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) Text
    k
            Project t :: Expr Void a
    t (Left ks :: Set Text
    ks) ->
                Environment a -> Val a -> Set Text -> Val a
    forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
    vProjectByFields Environment a
    env (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Set Text -> Set Text
    forall a. Ord a => Set a -> Set a
    Dhall.Set.sort Set Text
    ks)
            Project t :: Expr Void a
    t (Right e :: Expr Void a
    e) ->
                case Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    e of
                    VRecord kts :: Map Text (Val a)
    kts ->
                        Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env (Expr Void a -> Either (Set Text) (Expr Void a) -> Expr Void a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr Void a
    t (Set Text -> Either (Set Text) (Expr Void a)
    forall a b. a -> Either a b
    Left (Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.fromSet (Map Text (Val a) -> Set Text
    forall k v. Map k v -> Set k
    Map.keysSet Map Text (Val a)
    kts))))
                    e' :: Val a
    e' ->
                        Val a -> Either (Set Text) (Val a) -> Val a
    forall a. Val a -> Either (Set Text) (Val a) -> Val a
    VProject (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Val a -> Either (Set Text) (Val a)
    forall a b. b -> Either a b
    Right Val a
    e')
            Assert t :: Expr Void a
    t ->
                Val a -> Val a
    forall a. Val a -> Val a
    VAssert (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t)
            Equivalent t :: Expr Void a
    t u :: Expr Void a
    u ->
                Val a -> Val a -> Val a
    forall a. Val a -> Val a -> Val a
    VEquivalent (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    u)
            e :: Expr Void a
    e@With{} ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env (Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a
    Syntax.desugarWith Expr Void a
    e)
            Note _ e :: Expr Void a
    e ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    e
            ImportAlt t :: Expr Void a
    t _ ->
                Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t
            Embed a :: a
    a ->
                a -> Val a
    forall a. a -> Val a
    VEmbed a
    a
      where
        evalChunks :: Chunks Void a -> VChunks a
        evalChunks :: Chunks Void a -> VChunks a
    evalChunks (Chunks xys :: [(Text, Expr Void a)]
    xys z :: Text
    z) = ((Text, Expr Void a) -> VChunks a -> VChunks a)
    -> VChunks a -> [(Text, Expr Void a)] -> VChunks a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr' (Text, Expr Void a) -> VChunks a -> VChunks a
    cons VChunks a
    forall a. VChunks a
    nil [(Text, Expr Void a)]
    xys
          where
            cons :: (Text, Expr Void a) -> VChunks a -> VChunks a
    cons (x :: Text
    x, t :: Expr Void a
    t) vcs :: VChunks a
    vcs =
                case Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env Expr Void a
    t of
                    VTextLit vcs' :: VChunks a
    vcs' -> [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] Text
    x VChunks a -> VChunks a -> VChunks a
    forall a. Semigroup a => a -> a -> a
    <> VChunks a
    vcs' VChunks a -> VChunks a -> VChunks a
    forall a. Semigroup a => a -> a -> a
    <> VChunks a
    vcs
                    t' :: Val a
    t'            -> [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [(Text
    x, Val a
    t')] Text
    forall a. Monoid a => a
    mempty VChunks a -> VChunks a -> VChunks a
    forall a. Semigroup a => a -> a -> a
    <> VChunks a
    vcs

            nil :: VChunks a
    nil = [(Text, Val a)] -> Text -> VChunks a
    forall a. [(Text, Val a)] -> Text -> VChunks a
    VChunks [] Text
    z
        {-# INLINE evalChunks #-}

    eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
    eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
    eqListBy f :: a -> a -> Bool
    f = [a] -> [a] -> Bool
    go
      where
        go :: [a] -> [a] -> Bool
    go (x :: a
    x:xs :: [a]
    xs) (y :: a
    y:ys :: [a]
    ys) | a -> a -> Bool
    f a
    x a
    y = [a] -> [a] -> Bool
    go [a]
    xs [a]
    ys
        go [] [] = Bool
    True
        go _  _  = Bool
    False
    {-# INLINE eqListBy #-}

    eqMapsBy :: Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy :: (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy f :: v -> v -> Bool
    f mL :: Map k v
    mL mR :: Map k v
    mR =
        Map k v -> Int
    forall k v. Map k v -> Int
    Map.size Map k v
    mL Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Map k v -> Int
    forall k v. Map k v -> Int
    Map.size Map k v
    mR
        Bool -> Bool -> Bool
    && ((k, v) -> (k, v) -> Bool) -> [(k, v)] -> [(k, v)] -> Bool
    forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
    eqListBy (k, v) -> (k, v) -> Bool
    forall a. Eq a => (a, v) -> (a, v) -> Bool
    eq (Map k v -> [(k, v)]
    forall k v. Map k v -> [(k, v)]
    Map.toAscList Map k v
    mL) (Map k v -> [(k, v)]
    forall k v. Map k v -> [(k, v)]
    Map.toAscList Map k v
    mR)
      where
        eq :: (a, v) -> (a, v) -> Bool
    eq (kL :: a
    kL, vL :: v
    vL) (kR :: a
    kR, vR :: v
    vR) = a
    kL a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    kR Bool -> Bool -> Bool
    && v -> v -> Bool
    f v
    vL v
    vR
    {-# INLINE eqMapsBy #-}

    eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
    eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
    eqMaybeBy f :: a -> a -> Bool
    f = Maybe a -> Maybe a -> Bool
    go
      where
        go :: Maybe a -> Maybe a -> Bool
    go (Just x :: a
    x) (Just y :: a
    y) = a -> a -> Bool
    f a
    x a
    y
        go Nothing  Nothing  = Bool
    True
        go _        _        = Bool
    False
    {-# INLINE eqMaybeBy #-}

    -- | Utility that powers the @Text/show@ built-in
    textShow :: Text -> Text
    textShow :: Text -> Text
    textShow text :: Text
    text = "\"" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> (Char -> Text) -> Text -> Text
    Text.concatMap Char -> Text
    f Text
    text Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> "\""
      where
        f :: Char -> Text
    f '"'  = "\\\""
        f '$'  = "\\u0024"
        f '\\' = "\\\\"
        f '\b' = "\\b"
        f '\n' = "\\n"
        f '\r' = "\\r"
        f '\t' = "\\t"
        f '\f' = "\\f"
        f c :: Char
    c | Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= '\x1F' = String -> Text
    Text.pack (String -> Int -> String
    forall r. PrintfType r => String -> r
    Text.Printf.printf "\\u%04x" (Char -> Int
    Data.Char.ord Char
    c))
            | Bool
    otherwise   = Char -> Text
    Text.singleton Char
    c

    conv :: forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv :: Environment a -> Val a -> Val a -> Bool
    conv !Environment a
    env t0 :: Val a
    t0 t0' :: Val a
    t0' =
        case (Val a
    t0, Val a
    t0') of
            (VConst k :: Const
    k, VConst k' :: Const
    k') ->
                Const
    k Const -> Const -> Bool
    forall a. Eq a => a -> a -> Bool
    == Const
    k'
            (VVar x :: Text
    x i :: Int
    i, VVar x' :: Text
    x' i' :: Int
    i') ->
                Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' Bool -> Bool -> Bool
    && Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i'
            (VLam _ (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t :: Closure a
    t)), VLam _ t' :: Closure a
    t' ) ->
                Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t Val a
    v) (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t' Val a
    v)
            (VLam _ (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t :: Closure a
    t)), VHLam _ t' :: Val a -> Val a
    t') ->
                Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t Val a
    v) (Val a -> Val a
    t' Val a
    v)
            (VLam _ (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t :: Closure a
    t)), t' :: Val a
    t'        ) ->
                Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t Val a
    v) (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    t' Val a
    v)
            (VHLam _ t :: Val a -> Val a
    t, VLam _ (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t' :: Closure a
    t'))) ->
                Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a
    t Val a
    v) (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t' Val a
    v)
            (VHLam _ t :: Val a -> Val a
    t, VHLam _ t' :: Val a -> Val a
    t'                    ) ->
                let (x :: Text
    x, v :: Val a
    v) = Text -> (Text, Val a)
    fresh "x" in Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a
    t Val a
    v) (Val a -> Val a
    t' Val a
    v)
            (VHLam _ t :: Val a -> Val a
    t, t' :: Val a
    t'                            ) ->
                let (x :: Text
    x, v :: Val a
    v) = Text -> (Text, Val a)
    fresh "x" in Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a
    t Val a
    v) (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    t' Val a
    v)
            (t :: Val a
    t, VLam _ (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t' :: Closure a
    t'))) ->
                Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    t Val a
    v) (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t' Val a
    v)
            (t :: Val a
    t, VHLam _ t' :: Val a -> Val a
    t'  ) ->
                let (x :: Text
    x, v :: Val a
    v) = Text -> (Text, Val a)
    fresh "x" in Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a -> Val a
    forall a. Eq a => Val a -> Val a -> Val a
    vApp Val a
    t Val a
    v) (Val a -> Val a
    t' Val a
    v)
            (VApp t :: Val a
    t u :: Val a
    u, VApp t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VPi a :: Val a
    a b :: Closure a
    b, VPi a' :: Val a
    a' (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, b' :: Closure a
    b'))) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b Val a
    v) (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b' Val a
    v)
            (VPi a :: Val a
    a b :: Closure a
    b, VHPi (Text -> (Text, Val a)
    fresh -> (x :: Text
    x, v :: Val a
    v)) a' :: Val a
    a' b' :: Val a -> Val a
    b') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b Val a
    v) (Val a -> Val a
    b' Val a
    v)
            (VHPi _ a :: Val a
    a b :: Val a -> Val a
    b, VPi a' :: Val a
    a' (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, b' :: Closure a
    b'))) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a
    b Val a
    v) (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b' Val a
    v)
            (VHPi _ a :: Val a
    a b :: Val a -> Val a
    b, VHPi (Text -> (Text, Val a)
    fresh -> (x :: Text
    x, v :: Val a
    v)) a' :: Val a
    a' b' :: Val a -> Val a
    b') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Text -> Val a -> Val a -> Bool
    convSkip Text
    x (Val a -> Val a
    b Val a
    v) (Val a -> Val a
    b' Val a
    v)
            (VBool, VBool) ->
                Bool
    True
            (VBoolLit b :: Bool
    b, VBoolLit b' :: Bool
    b') ->
                Bool
    b Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    b'
            (VBoolAnd t :: Val a
    t u :: Val a
    u, VBoolAnd t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VBoolOr t :: Val a
    t u :: Val a
    u, VBoolOr t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VBoolEQ t :: Val a
    t u :: Val a
    u, VBoolEQ t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VBoolNE t :: Val a
    t u :: Val a
    u, VBoolNE t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VBoolIf t :: Val a
    t u :: Val a
    u v :: Val a
    v, VBoolIf t' :: Val a
    t' u' :: Val a
    u' v' :: Val a
    v') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    v Val a
    v'
            (VNatural, VNatural) ->
                Bool
    True
            (VNaturalLit n :: Natural
    n, VNaturalLit n' :: Natural
    n') ->
                Natural
    n Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    n'
            (VNaturalFold t :: Val a
    t _ u :: Val a
    u v :: Val a
    v, VNaturalFold t' :: Val a
    t' _ u' :: Val a
    u' v' :: Val a
    v') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    v Val a
    v'
            (VNaturalBuild t :: Val a
    t, VNaturalBuild t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalIsZero t :: Val a
    t, VNaturalIsZero t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalEven t :: Val a
    t, VNaturalEven t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalOdd t :: Val a
    t, VNaturalOdd t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalToInteger t :: Val a
    t, VNaturalToInteger t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalShow t :: Val a
    t, VNaturalShow t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNaturalSubtract x :: Val a
    x y :: Val a
    y, VNaturalSubtract x' :: Val a
    x' y' :: Val a
    y') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    x Val a
    x' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    y Val a
    y'
            (VNaturalPlus t :: Val a
    t u :: Val a
    u, VNaturalPlus t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VNaturalTimes t :: Val a
    t u :: Val a
    u, VNaturalTimes t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VInteger, VInteger) ->
                Bool
    True
            (VIntegerLit t :: Integer
    t, VIntegerLit t' :: Integer
    t') ->
                Integer
    t Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    t'
            (VIntegerClamp t :: Val a
    t, VIntegerClamp t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VIntegerNegate t :: Val a
    t, VIntegerNegate t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VIntegerShow t :: Val a
    t, VIntegerShow t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VIntegerToDouble t :: Val a
    t, VIntegerToDouble t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VDouble, VDouble) ->
                Bool
    True
            (VDoubleLit n :: DhallDouble
    n, VDoubleLit n' :: DhallDouble
    n') ->
                DhallDouble
    n DhallDouble -> DhallDouble -> Bool
    forall a. Eq a => a -> a -> Bool
    == DhallDouble
    n'
            (VDoubleShow t :: Val a
    t, VDoubleShow t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VText, VText) ->
                Bool
    True
            (VTextLit cs :: VChunks a
    cs, VTextLit cs' :: VChunks a
    cs') ->
                VChunks a -> VChunks a -> Bool
    convChunks VChunks a
    cs VChunks a
    cs'
            (VTextAppend t :: Val a
    t u :: Val a
    u, VTextAppend t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VTextShow t :: Val a
    t, VTextShow t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VList a :: Val a
    a, VList a' :: Val a
    a') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a'
            (VListLit _ xs :: Seq (Val a)
    xs, VListLit _ xs' :: Seq (Val a)
    xs') ->
                (Val a -> Val a -> Bool) -> [Val a] -> [Val a] -> Bool
    forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
    eqListBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env) (Seq (Val a) -> [Val a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Seq (Val a)
    xs) (Seq (Val a) -> [Val a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Seq (Val a)
    xs')
            (VListAppend t :: Val a
    t u :: Val a
    u, VListAppend t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VListBuild _ t :: Val a
    t, VListBuild _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListLength a :: Val a
    a t :: Val a
    t, VListLength a' :: Val a
    a' t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListHead _ t :: Val a
    t, VListHead _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListLast _ t :: Val a
    t, VListLast _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListIndexed _ t :: Val a
    t, VListIndexed _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListReverse _ t :: Val a
    t, VListReverse _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VListFold a :: Val a
    a l :: Val a
    l _ t :: Val a
    t u :: Val a
    u, VListFold a' :: Val a
    a' l' :: Val a
    l' _ t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    l Val a
    l' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VOptional a :: Val a
    a, VOptional a' :: Val a
    a') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a'
            (VSome t :: Val a
    t, VSome t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VNone _, VNone _) ->
                Bool
    True
            (VOptionalBuild _ t :: Val a
    t, VOptionalBuild _ t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VRecord m :: Map Text (Val a)
    m, VRecord m' :: Map Text (Val a)
    m') ->
                (Val a -> Val a -> Bool)
    -> Map Text (Val a) -> Map Text (Val a) -> Bool
    forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env) Map Text (Val a)
    m Map Text (Val a)
    m'
            (VRecordLit m :: Map Text (Val a)
    m, VRecordLit m' :: Map Text (Val a)
    m') ->
                (Val a -> Val a -> Bool)
    -> Map Text (Val a) -> Map Text (Val a) -> Bool
    forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env) Map Text (Val a)
    m Map Text (Val a)
    m'
            (VUnion m :: Map Text (Maybe (Val a))
    m, VUnion m' :: Map Text (Maybe (Val a))
    m') ->
                (Maybe (Val a) -> Maybe (Val a) -> Bool)
    -> Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a)) -> Bool
    forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy ((Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
    forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
    eqMaybeBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env)) Map Text (Maybe (Val a))
    m Map Text (Maybe (Val a))
    m'
            (VCombine _ t :: Val a
    t u :: Val a
    u, VCombine _ t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VCombineTypes t :: Val a
    t u :: Val a
    u, VCombineTypes t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VPrefer t :: Val a
    t u :: Val a
    u, VPrefer t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VMerge t :: Val a
    t u :: Val a
    u _, VMerge t' :: Val a
    t' u' :: Val a
    u' _) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VToMap t :: Val a
    t _, VToMap t' :: Val a
    t' _) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VField t :: Val a
    t k :: Text
    k, VField t' :: Val a
    t' k' :: Text
    k') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Text
    k Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    k'
            (VProject t :: Val a
    t (Left ks :: Set Text
    ks), VProject t' :: Val a
    t' (Left ks' :: Set Text
    ks')) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Set Text
    ks Set Text -> Set Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Set Text
    ks'
            (VProject t :: Val a
    t (Right e :: Val a
    e), VProject t' :: Val a
    t' (Right e' :: Val a
    e')) ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    e Val a
    e'
            (VAssert t :: Val a
    t, VAssert t' :: Val a
    t') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t'
            (VEquivalent t :: Val a
    t u :: Val a
    u, VEquivalent t' :: Val a
    t' u' :: Val a
    u') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u'
            (VInject m :: Map Text (Maybe (Val a))
    m k :: Text
    k mt :: Maybe (Val a)
    mt, VInject m' :: Map Text (Maybe (Val a))
    m' k' :: Text
    k' mt' :: Maybe (Val a)
    mt') ->
                (Maybe (Val a) -> Maybe (Val a) -> Bool)
    -> Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a)) -> Bool
    forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
    eqMapsBy ((Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
    forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
    eqMaybeBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env)) Map Text (Maybe (Val a))
    m Map Text (Maybe (Val a))
    m' Bool -> Bool -> Bool
    && Text
    k Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    k' Bool -> Bool -> Bool
    && (Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
    forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
    eqMaybeBy (Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env) Maybe (Val a)
    mt Maybe (Val a)
    mt'
            (VEmbed a :: a
    a, VEmbed a' :: a
    a') ->
                a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    a'
            (VOptionalFold a :: Val a
    a t :: Val a
    t _ u :: Val a
    u v :: Val a
    v, VOptionalFold a' :: Val a
    a' t' :: Val a
    t' _ u' :: Val a
    u' v' :: Val a
    v') ->
                Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    a Val a
    a' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    t Val a
    t' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    u Val a
    u' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    v Val a
    v'
            (_, _) ->
                Bool
    False
      where
        fresh :: Text -> (Text, Val a)
        fresh :: Text -> (Text, Val a)
    fresh x :: Text
    x = (Text
    x, Text -> Int -> Val a
    forall a. Text -> Int -> Val a
    VVar Text
    x (Text -> Environment a -> Int
    forall a. Text -> Environment a -> Int
    countEnvironment Text
    x Environment a
    env))
        {-# INLINE fresh #-}

        freshClosure :: Closure a -> (Text, Val a, Closure a)
        freshClosure :: Closure a -> (Text, Val a, Closure a)
    freshClosure closure :: Closure a
    closure@(Closure x :: Text
    x _ _) = (Text
    x, (Text, Val a) -> Val a
    forall a b. (a, b) -> b
    snd (Text -> (Text, Val a)
    fresh Text
    x), Closure a
    closure)
        {-# INLINE freshClosure #-}

        convChunks :: VChunks a -> VChunks a -> Bool
        convChunks :: VChunks a -> VChunks a -> Bool
    convChunks (VChunks xys :: [(Text, Val a)]
    xys z :: Text
    z) (VChunks xys' :: [(Text, Val a)]
    xys' z' :: Text
    z') =
          ((Text, Val a) -> (Text, Val a) -> Bool)
    -> [(Text, Val a)] -> [(Text, Val a)] -> Bool
    forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
    eqListBy (\(x :: Text
    x, y :: Val a
    y) (x' :: Text
    x', y' :: Val a
    y') -> Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' Bool -> Bool -> Bool
    && Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    env Val a
    y Val a
    y') [(Text, Val a)]
    xys [(Text, Val a)]
    xys' Bool -> Bool -> Bool
    && Text
    z Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    z'
        {-# INLINE convChunks #-}

        convSkip :: Text -> Val a -> Val a -> Bool
        convSkip :: Text -> Val a -> Val a -> Bool
    convSkip x :: Text
    x = Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv (Environment a -> Text -> Environment a
    forall a. Environment a -> Text -> Environment a
    Skip Environment a
    env Text
    x)
        {-# INLINE convSkip #-}

    judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
    judgmentallyEqual :: Expr s a -> Expr t a -> Bool
    judgmentallyEqual (Expr s a -> Expr Void a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote -> Expr Void a
    t) (Expr t a -> Expr Void a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote -> Expr Void a
    u) =
        Environment a -> Val a -> Val a -> Bool
    forall a. Eq a => Environment a -> Val a -> Val a -> Bool
    conv Environment a
    forall a. Environment a
    Empty (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    forall a. Environment a
    Empty Expr Void a
    t) (Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    forall a. Environment a
    Empty Expr Void a
    u)

    data Names
      = EmptyNames
      | Bind !Names {-# UNPACK #-} !Text
      deriving Int -> Names -> ShowS
    [Names] -> ShowS
    Names -> String
    (Int -> Names -> ShowS)
    -> (Names -> String) -> ([Names] -> ShowS) -> Show Names
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Names] -> ShowS
    $cshowList :: [Names] -> ShowS
    show :: Names -> String
    $cshow :: Names -> String
    showsPrec :: Int -> Names -> ShowS
    $cshowsPrec :: Int -> Names -> ShowS
    Show

    envNames :: Environment a -> Names
    envNames :: Environment a -> Names
    envNames Empty = Names
    EmptyNames
    envNames (Skip   env :: Environment a
    env x :: Text
    x  ) = Names -> Text -> Names
    Bind (Environment a -> Names
    forall a. Environment a -> Names
    envNames Environment a
    env) Text
    x
    envNames (Extend env :: Environment a
    env x :: Text
    x _) = Names -> Text -> Names
    Bind (Environment a -> Names
    forall a. Environment a -> Names
    envNames Environment a
    env) Text
    x

    countNames :: Text -> Names -> Int
    countNames :: Text -> Names -> Int
    countNames x :: Text
    x = Int -> Names -> Int
    forall t. Num t => t -> Names -> t
    go 0
      where
        go :: t -> Names -> t
    go !t
    acc EmptyNames         = t
    acc
        go  acc :: t
    acc (Bind env :: Names
    env x' :: Text
    x') = t -> Names -> t
    go (if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' then t
    acc t -> t -> t
    forall a. Num a => a -> a -> a
    + 1 else t
    acc) Names
    env

    -- | Quote a value into beta-normal form.
    quote :: forall a. Eq a => Names -> Val a -> Expr Void a
    quote :: Names -> Val a -> Expr Void a
    quote !Names
    env !Val a
    t0 =
        case Val a
    t0 of
            VConst k :: Const
    k ->
                Const -> Expr Void a
    forall s a. Const -> Expr s a
    Const Const
    k
            VVar !Text
    x !Int
    i ->
                Var -> Expr Void a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    x (Text -> Names -> Int
    countNames Text
    x Names
    env Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1))
            VApp t :: Val a
    t u :: Val a
    u ->
                Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    u
            VLam a :: Val a
    a (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, t :: Closure a
    t)) ->
                Text -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    x (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    a) (Text -> Val a -> Expr Void a
    quoteBind Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    t Val a
    v))
            VHLam i :: HLamInfo a
    i t :: Val a -> Val a
    t ->
                case HLamInfo a
    i of
                    Typed (Text -> (Text, Val a)
    fresh -> (x :: Text
    x, v :: Val a
    v)) a :: Val a
    a -> Text -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    x (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    a) (Text -> Val a -> Expr Void a
    quoteBind Text
    x (Val a -> Val a
    t Val a
    v))
                    Prim                      -> Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env (Val a -> Val a
    t Val a
    forall a. Val a
    VPrimVar)
                    NaturalSubtractZero       -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr Void a
    forall s a. Expr s a
    NaturalSubtract (Natural -> Expr Void a
    forall s a. Natural -> Expr s a
    NaturalLit 0)

            VPi a :: Val a
    a (Closure a -> (Text, Val a, Closure a)
    freshClosure -> (x :: Text
    x, v :: Val a
    v, b :: Closure a
    b)) ->
                Text -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    x (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    a) (Text -> Val a -> Expr Void a
    quoteBind Text
    x (Closure a -> Val a -> Val a
    forall a. Eq a => Closure a -> Val a -> Val a
    instantiate Closure a
    b Val a
    v))
            VHPi (Text -> (Text, Val a)
    fresh -> (x :: Text
    x, v :: Val a
    v)) a :: Val a
    a b :: Val a -> Val a
    b ->
                Text -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    x (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    a) (Text -> Val a -> Expr Void a
    quoteBind Text
    x (Val a -> Val a
    b Val a
    v))
            VBool ->
                Expr Void a
    forall s a. Expr s a
    Bool
            VBoolLit b :: Bool
    b ->
                Bool -> Expr Void a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    b
            VBoolAnd t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolAnd (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VBoolOr t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolOr (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VBoolEQ t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolEQ (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VBoolNE t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolNE (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VBoolIf t :: Val a
    t u :: Val a
    u v :: Val a
    v ->
                Expr Void a -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
    BoolIf (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    v)
            VNatural ->
                Expr Void a
    forall s a. Expr s a
    Natural
            VNaturalLit n :: Natural
    n ->
                Natural -> Expr Void a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    n
            VNaturalFold a :: Val a
    a t :: Val a
    t u :: Val a
    u v :: Val a
    v ->
                Expr Void a
    forall s a. Expr s a
    NaturalFold Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    u Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    v
            VNaturalBuild t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalBuild Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalIsZero t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalIsZero Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalEven t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalEven Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalOdd t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalOdd Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalToInteger t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalToInteger Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalShow t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    NaturalShow Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VNaturalPlus t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalPlus (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VNaturalTimes t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalTimes (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VNaturalSubtract x :: Val a
    x y :: Val a
    y ->
                Expr Void a
    forall s a. Expr s a
    NaturalSubtract Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    x Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    y
            VInteger ->
                Expr Void a
    forall s a. Expr s a
    Integer
            VIntegerLit n :: Integer
    n ->
                Integer -> Expr Void a
    forall s a. Integer -> Expr s a
    IntegerLit Integer
    n
            VIntegerClamp t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    IntegerClamp Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VIntegerNegate t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    IntegerNegate Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VIntegerShow t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    IntegerShow Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VIntegerToDouble t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    IntegerToDouble Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VDouble ->
                Expr Void a
    forall s a. Expr s a
    Double
            VDoubleLit n :: DhallDouble
    n ->
                DhallDouble -> Expr Void a
    forall s a. DhallDouble -> Expr s a
    DoubleLit DhallDouble
    n
            VDoubleShow t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    DoubleShow Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VText ->
                Expr Void a
    forall s a. Expr s a
    Text
            VTextLit (VChunks xys :: [(Text, Val a)]
    xys z :: Text
    z) ->
                Chunks Void a -> Expr Void a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr Void a)] -> Text -> Chunks Void a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks (((Text, Val a) -> (Text, Expr Void a))
    -> [(Text, Val a)] -> [(Text, Expr Void a)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Val a -> Expr Void a) -> (Text, Val a) -> (Text, Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env)) [(Text, Val a)]
    xys) Text
    z)
            VTextAppend t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VTextShow t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    TextShow Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VList t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    List Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListLit ma :: Maybe (Val a)
    ma ts :: Seq (Val a)
    ts ->
                Maybe (Expr Void a) -> Seq (Expr Void a) -> Expr Void a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Maybe (Val a)
    ma) ((Val a -> Expr Void a) -> Seq (Val a) -> Seq (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Seq (Val a)
    ts)
            VListAppend t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VListBuild a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListBuild Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListFold a :: Val a
    a l :: Val a
    l t :: Val a
    t u :: Val a
    u v :: Val a
    v ->
                Expr Void a
    forall s a. Expr s a
    ListFold Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    l Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    u Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    v
            VListLength a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListLength Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListHead a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListHead Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListLast a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListLast Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListIndexed a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListIndexed Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VListReverse a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    ListReverse Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VOptional a :: Val a
    a ->
                Expr Void a
    forall s a. Expr s a
    Optional Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a
            VSome t :: Val a
    t ->
                Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a
    Some (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t)
            VNone t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    None Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VOptionalFold a :: Val a
    a o :: Val a
    o t :: Val a
    t u :: Val a
    u v :: Val a
    v ->
                Expr Void a
    forall s a. Expr s a
    OptionalFold Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    o Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    u Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    v
            VOptionalBuild a :: Val a
    a t :: Val a
    t ->
                Expr Void a
    forall s a. Expr s a
    OptionalBuild Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    a Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VRecord m :: Map Text (Val a)
    m ->
                Map Text (Expr Void a) -> Expr Void a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record ((Val a -> Expr Void a)
    -> Map Text (Val a) -> Map Text (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Map Text (Val a)
    m)
            VRecordLit m :: Map Text (Val a)
    m ->
                Map Text (Expr Void a) -> Expr Void a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit ((Val a -> Expr Void a)
    -> Map Text (Val a) -> Map Text (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Map Text (Val a)
    m)
            VUnion m :: Map Text (Maybe (Val a))
    m ->
                Map Text (Maybe (Expr Void a)) -> Expr Void a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union ((Maybe (Val a) -> Maybe (Expr Void a))
    -> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env)) Map Text (Maybe (Val a))
    m)
            VCombine mk :: Maybe Text
    mk t :: Val a
    t u :: Val a
    u ->
                Maybe Text -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe Text
    mk (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VCombineTypes t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    CombineTypes (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VPrefer t :: Val a
    t u :: Val a
    u ->
                PreferAnnotation Void a
    -> Expr Void a -> Expr Void a -> Expr Void a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation Void a
    forall s a. PreferAnnotation s a
    PreferFromSource (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VMerge t :: Val a
    t u :: Val a
    u ma :: Maybe (Val a)
    ma ->
                Expr Void a -> Expr Void a -> Maybe (Expr Void a) -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u) ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Maybe (Val a)
    ma)
            VToMap t :: Val a
    t ma :: Maybe (Val a)
    ma ->
                Expr Void a -> Maybe (Expr Void a) -> Expr Void a
    forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
    ToMap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Maybe (Val a)
    ma)
            VField t :: Val a
    t k :: Text
    k ->
                Expr Void a -> Text -> Expr Void a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) Text
    k
            VProject t :: Val a
    t p :: Either (Set Text) (Val a)
    p ->
                Expr Void a -> Either (Set Text) (Expr Void a) -> Expr Void a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) ((Val a -> Expr Void a)
    -> Either (Set Text) (Val a) -> Either (Set Text) (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env) Either (Set Text) (Val a)
    p)
            VAssert t :: Val a
    t ->
                Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a
    Assert (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t)
            VEquivalent t :: Val a
    t u :: Val a
    u ->
                Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Equivalent (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    t) (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
            VInject m :: Map Text (Maybe (Val a))
    m k :: Text
    k Nothing ->
                Expr Void a -> Text -> Expr Void a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Map Text (Maybe (Expr Void a)) -> Expr Void a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union ((Maybe (Val a) -> Maybe (Expr Void a))
    -> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env)) Map Text (Maybe (Val a))
    m)) Text
    k
            VInject m :: Map Text (Maybe (Val a))
    m k :: Text
    k (Just t :: Val a
    t) ->
                Expr Void a -> Text -> Expr Void a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Map Text (Maybe (Expr Void a)) -> Expr Void a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union ((Maybe (Val a) -> Maybe (Expr Void a))
    -> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env)) Map Text (Maybe (Val a))
    m)) Text
    k Expr Void a -> Val a -> Expr Void a
    `qApp` Val a
    t
            VEmbed a :: a
    a ->
                a -> Expr Void a
    forall s a. a -> Expr s a
    Embed a
    a
            VPrimVar ->
                String -> Expr Void a
    forall a. HasCallStack => String -> a
    error String
    errorMsg
      where
        fresh :: Text -> (Text, Val a)
        fresh :: Text -> (Text, Val a)
    fresh x :: Text
    x = (Text
    x, Text -> Int -> Val a
    forall a. Text -> Int -> Val a
    VVar Text
    x (Text -> Names -> Int
    countNames Text
    x Names
    env))
        {-# INLINE fresh #-}

        freshClosure :: Closure a -> (Text, Val a, Closure a)
        freshClosure :: Closure a -> (Text, Val a, Closure a)
    freshClosure closure :: Closure a
    closure@(Closure x :: Text
    x _ _) = (Text
    x, (Text, Val a) -> Val a
    forall a b. (a, b) -> b
    snd (Text -> (Text, Val a)
    fresh Text
    x), Closure a
    closure)
        {-# INLINE freshClosure #-}

        quoteBind :: Text -> Val a -> Expr Void a
        quoteBind :: Text -> Val a -> Expr Void a
    quoteBind x :: Text
    x = Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote (Names -> Text -> Names
    Bind Names
    env Text
    x)
        {-# INLINE quoteBind #-}

        qApp :: Expr Void a -> Val a -> Expr Void a
        qApp :: Expr Void a -> Val a -> Expr Void a
    qApp t :: Expr Void a
    t VPrimVar = Expr Void a
    t
        qApp t :: Expr Void a
    t u :: Val a
    u        = Expr Void a -> Expr Void a -> Expr Void a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr Void a
    t (Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote Names
    env Val a
    u)
        {-# INLINE qApp #-}

    -- | Normalize an expression in an environment of values. Any variable pointing out of
    --   the environment is treated as opaque free variable.
    nf :: Eq a => Environment a -> Expr s a -> Expr t a
    nf :: Environment a -> Expr s a -> Expr t a
    nf !Environment a
    env = Expr Void a -> Expr t a
    forall a s. Expr Void a -> Expr s a
    Syntax.renote (Expr Void a -> Expr t a)
    -> (Expr s a -> Expr Void a) -> Expr s a -> Expr t a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Names -> Val a -> Expr Void a
    forall a. Eq a => Names -> Val a -> Expr Void a
    quote (Environment a -> Names
    forall a. Environment a -> Names
    envNames Environment a
    env) (Val a -> Expr Void a)
    -> (Expr s a -> Val a) -> Expr s a -> Expr Void a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Environment a -> Expr Void a -> Val a
    forall a. Eq a => Environment a -> Expr Void a -> Val a
    eval Environment a
    env (Expr Void a -> Val a)
    -> (Expr s a -> Expr Void a) -> Expr s a -> Val a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr s a -> Expr Void a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote

    normalize :: Eq a => Expr s a -> Expr t a
    normalize :: Expr s a -> Expr t a
    normalize = Environment a -> Expr s a -> Expr t a
    forall a s t. Eq a => Environment a -> Expr s a -> Expr t a
    nf Environment a
    forall a. Environment a
    Empty

    alphaNormalize :: Expr s a -> Expr s a
    alphaNormalize :: Expr s a -> Expr s a
    alphaNormalize = Names -> Expr s a -> Expr s a
    forall s a. Names -> Expr s a -> Expr s a
    goEnv Names
    EmptyNames
      where
        goVar :: Names -> Text -> Int -> Expr s a
        goVar :: Names -> Text -> Int -> Expr s a
    goVar e :: Names
    e topX :: Text
    topX topI :: Int
    topI = Int -> Names -> Int -> Expr s a
    forall s a. Int -> Names -> Int -> Expr s a
    go 0 Names
    e Int
    topI
          where
            go :: Int -> Names -> Int -> Expr s a
    go !Int
    acc (Bind env :: Names
    env x :: Text
    x) !Int
    i
              | Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    topX = if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "_" Int
    acc) else Int -> Names -> Int -> Expr s a
    go (Int
    acc Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1) Names
    env (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
              | Bool
    otherwise = Int -> Names -> Int -> Expr s a
    go (Int
    acc Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1) Names
    env Int
    i
            go _ EmptyNames i :: Int
    i = Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    topX Int
    i)

        goEnv :: Names -> Expr s a -> Expr s a
        goEnv :: Names -> Expr s a -> Expr s a
    goEnv !Names
    e0 t0 :: Expr s a
    t0 =
            case Expr s a
    t0 of
                Const k :: Const
    k ->
                    Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    k
                Var (V x :: Text
    x i :: Int
    i) ->
                    Names -> Text -> Int -> Expr s a
    forall s a. Names -> Text -> Int -> Expr s a
    goVar Names
    e0 Text
    x Int
    i
                Lam x :: Text
    x t :: Expr s a
    t u :: Expr s a
    u ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Text -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a
    goBind Text
    x Expr s a
    u)
                Pi x :: Text
    x a :: Expr s a
    a b :: Expr s a
    b ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    a) (Text -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a
    goBind Text
    x Expr s a
    b)
                App t :: Expr s a
    t u :: Expr s a
    u ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Let (Binding src0 :: Maybe s
    src0 x :: Text
    x src1 :: Maybe s
    src1 mA :: Maybe (Maybe s, Expr s a)
    mA src2 :: Maybe s
    src2 a :: Expr s a
    a) b :: Expr s a
    b ->
                    Binding s a -> Expr s a -> Expr s a
    forall s a. Binding s a -> Expr s a -> Expr s a
    Let (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
    src0 "_" Maybe s
    src1 (((Maybe s, Expr s a) -> (Maybe s, Expr s a))
    -> Maybe (Maybe s, Expr s a) -> Maybe (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr s a -> Expr s a)
    -> (Maybe s, Expr s a) -> (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go) Maybe (Maybe s, Expr s a)
    mA) Maybe s
    src2 (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    a)) (Text -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a
    goBind Text
    x Expr s a
    b)
                Annot t :: Expr s a
    t u :: Expr s a
    u ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Bool ->
                    Expr s a
    forall s a. Expr s a
    Bool
                BoolLit b :: Bool
    b ->
                    Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    b
                BoolAnd t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolAnd (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                BoolOr t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolOr  (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                BoolEQ t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolEQ  (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                BoolNE t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolNE  (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                BoolIf b :: Expr s a
    b t :: Expr s a
    t f :: Expr s a
    f ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    b) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    f)
                Natural ->
                    Expr s a
    forall s a. Expr s a
    Natural
                NaturalLit n :: Natural
    n ->
                    Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    n
                NaturalFold ->
                    Expr s a
    forall s a. Expr s a
    NaturalFold
                NaturalBuild ->
                    Expr s a
    forall s a. Expr s a
    NaturalBuild
                NaturalIsZero ->
                    Expr s a
    forall s a. Expr s a
    NaturalIsZero
                NaturalEven ->
                    Expr s a
    forall s a. Expr s a
    NaturalEven
                NaturalOdd ->
                    Expr s a
    forall s a. Expr s a
    NaturalOdd
                NaturalToInteger ->
                    Expr s a
    forall s a. Expr s a
    NaturalToInteger
                NaturalShow ->
                    Expr s a
    forall s a. Expr s a
    NaturalShow
                NaturalSubtract ->
                    Expr s a
    forall s a. Expr s a
    NaturalSubtract
                NaturalPlus t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalPlus (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                NaturalTimes t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalTimes (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Integer ->
                    Expr s a
    forall s a. Expr s a
    Integer
                IntegerLit n :: Integer
    n ->
                    Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit Integer
    n
                IntegerClamp ->
                    Expr s a
    forall s a. Expr s a
    IntegerClamp
                IntegerNegate ->
                    Expr s a
    forall s a. Expr s a
    IntegerNegate
                IntegerShow ->
                    Expr s a
    forall s a. Expr s a
    IntegerShow
                IntegerToDouble ->
                    Expr s a
    forall s a. Expr s a
    IntegerToDouble
                Double ->
                    Expr s a
    forall s a. Expr s a
    Double
                DoubleLit n :: DhallDouble
    n ->
                    DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit DhallDouble
    n
                DoubleShow ->
                    Expr s a
    forall s a. Expr s a
    DoubleShow
                Text ->
                    Expr s a
    forall s a. Expr s a
    Text
                TextLit cs :: Chunks s a
    cs ->
                    Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit (Chunks s a -> Chunks s a
    forall s a. Chunks s a -> Chunks s a
    goChunks Chunks s a
    cs)
                TextAppend t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                TextShow ->
                    Expr s a
    forall s a. Expr s a
    TextShow
                List ->
                    Expr s a
    forall s a. Expr s a
    List
                ListLit ma :: Maybe (Expr s a)
    ma ts :: Seq (Expr s a)
    ts ->
                    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 -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Maybe (Expr s a)
    ma) ((Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Seq (Expr s a)
    ts)
                ListAppend t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                ListBuild ->
                    Expr s a
    forall s a. Expr s a
    ListBuild
                ListFold ->
                    Expr s a
    forall s a. Expr s a
    ListFold
                ListLength ->
                    Expr s a
    forall s a. Expr s a
    ListLength
                ListHead ->
                    Expr s a
    forall s a. Expr s a
    ListHead
                ListLast ->
                    Expr s a
    forall s a. Expr s a
    ListLast
                ListIndexed ->
                    Expr s a
    forall s a. Expr s a
    ListIndexed
                ListReverse ->
                    Expr s a
    forall s a. Expr s a
    ListReverse
                Optional ->
                    Expr s a
    forall s a. Expr s a
    Optional
                Some t :: Expr s a
    t ->
                    Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t)
                None ->
                    Expr s a
    forall s a. Expr s a
    None
                OptionalFold ->
                    Expr s a
    forall s a. Expr s a
    OptionalFold
                OptionalBuild ->
                    Expr s a
    forall s a. Expr s a
    OptionalBuild
                Record kts :: Map Text (Expr s a)
    kts ->
                    Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record ((Expr s a -> Expr s a)
    -> Map Text (Expr s a) -> Map Text (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Map Text (Expr s a)
    kts)
                RecordLit kts :: Map Text (Expr s a)
    kts ->
                    Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit ((Expr s a -> Expr s a)
    -> Map Text (Expr s a) -> Map Text (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Map Text (Expr s a)
    kts)
                Union kts :: Map Text (Maybe (Expr s a))
    kts ->
                    Map Text (Maybe (Expr s a)) -> Expr s a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union ((Maybe (Expr s a) -> Maybe (Expr s a))
    -> Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go) Map Text (Maybe (Expr s a))
    kts)
                Combine m :: Maybe Text
    m t :: Expr s a
    t u :: Expr s a
    u ->
                    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
    m (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                CombineTypes t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    CombineTypes (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Prefer b :: PreferAnnotation s a
    b t :: Expr s a
    t u :: Expr s a
    u ->
                    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
    b (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                RecordCompletion t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    RecordCompletion (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Merge x :: Expr s a
    x y :: Expr s a
    y ma :: Maybe (Expr s a)
    ma ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    x) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    y) ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Maybe (Expr s a)
    ma)
                ToMap x :: Expr s a
    x ma :: Maybe (Expr s a)
    ma ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    x) ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Maybe (Expr s a)
    ma)
                Field t :: Expr s a
    t k :: Text
    k ->
                    Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) Text
    k
                Project t :: Expr s a
    t ks :: Either (Set Text) (Expr s a)
    ks ->
                    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 -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) ((Expr s a -> Expr s a)
    -> Either (Set Text) (Expr s a) -> Either (Set Text) (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Either (Set Text) (Expr s a)
    ks)
                Assert t :: Expr s a
    t ->
                    Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Assert (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t)
                Equivalent t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Equivalent (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                With e :: Expr s a
    e k :: NonEmpty Text
    k v :: Expr s a
    v ->
                    Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
    forall s a. Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
    With (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    e) NonEmpty Text
    k (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    v)
                Note s :: s
    s e :: Expr s a
    e ->
                    s -> Expr s a -> Expr s a
    forall s a. s -> Expr s a -> Expr s a
    Note s
    s (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    e)
                ImportAlt t :: Expr s a
    t u :: Expr s a
    u ->
                    Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ImportAlt (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    t) (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go Expr s a
    u)
                Embed a :: a
    a ->
                    a -> Expr s a
    forall s a. a -> Expr s a
    Embed a
    a
          where
            go :: Expr s a -> Expr s a
    go                     = Names -> Expr s a -> Expr s a
    forall s a. Names -> Expr s a -> Expr s a
    goEnv Names
    e0
            goBind :: Text -> Expr s a -> Expr s a
    goBind x :: Text
    x               = Names -> Expr s a -> Expr s a
    forall s a. Names -> Expr s a -> Expr s a
    goEnv (Names -> Text -> Names
    Bind Names
    e0 Text
    x)
            goChunks :: Chunks s a -> Chunks s a
    goChunks (Chunks ts :: [(Text, Expr s a)]
    ts x :: Text
    x) = [(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks (((Text, Expr s a) -> (Text, Expr s a))
    -> [(Text, Expr s a)] -> [(Text, Expr s a)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr s a -> Expr s a) -> (Text, Expr s a) -> (Text, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    go) [(Text, Expr s a)]
    ts) Text
    x