    {-# LANGUAGE BangPatterns      #-}
    {-# LANGUAGE LambdaCase        #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE RankNTypes        #-}
    {-# LANGUAGE ViewPatterns      #-}

    module Dhall.Normalize (
          alphaNormalize
        , normalize
        , normalizeWith
        , normalizeWithM
        , Normalizer
        , NormalizerM
        , ReifiedNormalizer (..)
        , judgmentallyEqual
        , subst
        , Syntax.shift
        , isNormalized
        , isNormalizedWith
        , freeIn
        ) where

    import Control.Applicative   (empty)
    import Data.Foldable
    import Data.Functor.Identity (Identity (..))
    import Data.List.NonEmpty    (NonEmpty (..))
    import Data.Sequence         (ViewL (..), ViewR (..))
    import Data.Traversable
    import Instances.TH.Lift     ()
    import Prelude               hiding (succ)

    import Dhall.Syntax
        ( Binding (Binding)
        , Chunks (..)
        , DhallDouble (..)
        , Expr (..)
        , FieldSelection (..)
        , FunctionBinding (..)
        , PreferAnnotation (..)
        , RecordField (..)
        , Var (..)
        , WithComponent (..)
        )

    import qualified Data.Sequence
    import qualified Data.Set
    import qualified Data.Text     as Text
    import qualified Dhall.Eval    as Eval
    import qualified Dhall.Map
    import qualified Dhall.Syntax  as Syntax
    import qualified Lens.Micro    as Lens

    {-| Returns `True` if two expressions are α-equivalent and β-equivalent and
        `False` otherwise

        `judgmentallyEqual` can fail with an `error` if you compare ill-typed
        expressions
    -}
    judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
    judgmentallyEqual :: forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    judgmentallyEqual = Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual
    {-# INLINE judgmentallyEqual #-}

    {-| Substitute all occurrences of a variable with an expression

    > subst x C B  ~  B[x := C]
    -}
    subst :: Var -> Expr s a -> Expr s a -> Expr s a
    subst :: forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst Var
    _ Expr s a
    _ (Const Const
    a) = Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    a
    subst (V Text
    x Int
    n) Expr s a
    e (Lam Maybe CharacterSet
    cs (FunctionBinding Maybe s
    src0 Text
    y Maybe s
    src1 Maybe s
    src2 Expr s a
    _A) Expr s a
    b) =
        Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    Lam Maybe CharacterSet
    cs (Maybe s
    -> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
    forall s a.
    Maybe s
    -> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
    FunctionBinding Maybe s
    src0 Text
    y Maybe s
    src1 Maybe s
    src2 Expr s a
    _A') Expr s a
    b'
      where
        _A' :: Expr s a
    _A' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n )                         Expr s a
    e  Expr s a
    _A
        b' :: Expr s a
    b'  = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift Int
    1 (Text -> Int -> Var
    V Text
    y Int
    0) Expr s a
    e)  Expr s a
    b
        n' :: Int
    n'  = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 else Int
    n
    subst (V Text
    x Int
    n) Expr s a
    e (Pi Maybe CharacterSet
    cs Text
    y Expr s a
    _A Expr s a
    _B) = Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
    Pi Maybe CharacterSet
    cs Text
    y Expr s a
    _A' Expr s a
    _B'
      where
        _A' :: Expr s a
    _A' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n )                         Expr s a
    e  Expr s a
    _A
        _B' :: Expr s a
    _B' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift Int
    1 (Text -> Int -> Var
    V Text
    y Int
    0) Expr s a
    e) Expr s a
    _B
        n' :: Int
    n'  = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 else Int
    n
    subst Var
    v Expr s a
    e (Var Var
    v') = if Var
    v Var -> Var -> Bool
    forall a. Eq a => a -> a -> Bool
    == Var
    v' then Expr s a
    e else Var -> Expr s a
    forall s a. Var -> Expr s a
    Var Var
    v'
    subst (V Text
    x Int
    n) Expr s a
    e (Let (Binding Maybe s
    src0 Text
    f Maybe s
    src1 Maybe (Maybe s, Expr s a)
    mt Maybe s
    src2 Expr s a
    r) 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 Text
    f Maybe s
    src1 Maybe (Maybe s, Expr s a)
    mt' Maybe s
    src2 Expr s a
    r') Expr s a
    b'
      where
        b' :: Expr s a
    b' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift Int
    1 (Text -> Int -> Var
    V Text
    f Int
    0) Expr s a
    e) Expr s a
    b
          where
            n' :: Int
    n' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    f then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 else Int
    n

        mt' :: Maybe (Maybe s, Expr s a)
    mt' = ((Maybe s, Expr s a) -> (Maybe s, Expr s a))
    -> Maybe (Maybe s, Expr s a) -> Maybe (Maybe s, Expr s a)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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 a b. (a -> b) -> (Maybe s, a) -> (Maybe s, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n) Expr s a
    e)) Maybe (Maybe s, Expr s a)
    mt
        r' :: Expr s a
    r'  =             Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n) Expr s a
    e  Expr s a
    r
    subst Var
    x Expr s a
    e Expr s a
    expression = ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    -> (Expr s a -> Expr s a) -> Expr s a -> Expr s a
    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
    Lens.over ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    forall (f :: * -> *) s a.
    Applicative f =>
    (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
    Syntax.subExpressions (Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst Var
    x Expr s a
    e) Expr s a
    expression

    {-| This function is used to determine whether folds like @Natural/fold@ or
        @List/fold@ should be lazy or strict in their accumulator based on the type
        of the accumulator

        If this function returns `True`, then they will be strict in their
        accumulator since we can guarantee an upper bound on the amount of work to
        normalize the accumulator on each step of the loop.  If this function
        returns `False` then they will be lazy in their accumulator and only
        normalize the final result at the end of the fold
    -}
    boundedType :: Expr s a -> Bool
    boundedType :: forall s a. Expr s a -> Bool
    boundedType Expr s a
    Bool             = Bool
    True
    boundedType Expr s a
    Natural          = Bool
    True
    boundedType Expr s a
    Integer          = Bool
    True
    boundedType Expr s a
    Double           = Bool
    True
    boundedType Expr s a
    Text             = Bool
    True
    boundedType (App Expr s a
    List Expr s a
    _)     = Bool
    False
    boundedType (App Expr s a
    Optional Expr s a
    t) = Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType Expr s a
    t
    boundedType (Record Map Text (RecordField s a)
    kvs)     = (RecordField s a -> Bool) -> Map Text (RecordField s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType (Expr s a -> Bool)
    -> (RecordField s a -> Expr s a) -> RecordField s a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue) Map Text (RecordField s a)
    kvs
    boundedType (Union Map Text (Maybe (Expr s a))
    kvs)      = (Maybe (Expr s a) -> Bool) -> Map Text (Maybe (Expr s a)) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType) Map Text (Maybe (Expr s a))
    kvs
    boundedType Expr s a
    _                = Bool
    False

    {-| α-normalize an expression by renaming all bound variables to @\"_\"@ and
        using De Bruijn indices to distinguish them

    >>> mfb = Syntax.makeFunctionBinding
    >>> alphaNormalize (Lam mempty (mfb "a" (Const Type)) (Lam mempty (mfb "b" (Const Type)) (Lam mempty (mfb "x" "a") (Lam mempty (mfb "y" "b") "x"))))
    Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1)))))

        α-normalization does not affect free variables:

    >>> alphaNormalize "x"
    Var (V "x" 0)

    -}
    alphaNormalize :: Expr s a -> Expr s a
    alphaNormalize :: forall s a. Expr s a -> Expr s a
    alphaNormalize = Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Eval.alphaNormalize
    {-# INLINE alphaNormalize #-}

    {-| Reduce an expression to its normal form, performing beta reduction

        `normalize` does not type-check the expression.  You may want to type-check
        expressions before normalizing them since normalization can convert an
        ill-typed expression into a well-typed expression.

        `normalize` can also fail with `error` if you normalize an ill-typed
        expression
    -}
    normalize :: Eq a => Expr s a -> Expr t a
    normalize :: forall a s t. Eq a => Expr s a -> Expr t a
    normalize = Expr s a -> Expr t a
    forall a s t. Eq a => Expr s a -> Expr t a
    Eval.normalize
    {-# INLINE normalize #-}

    {-| Reduce an expression to its normal form, performing beta reduction and applying
        any custom definitions.

        `normalizeWith` is designed to be used with function `Dhall.TypeCheck.typeWith`. The `Dhall.TypeCheck.typeWith`
        function allows typing of Dhall functions in a custom typing context whereas
        `normalizeWith` allows evaluating Dhall expressions in a custom context.

        To be more precise `normalizeWith` applies the given normalizer when it finds an
        application term that it cannot reduce by other means.

        Note that the context used in normalization will determine the properties of normalization.
        That is, if the functions in custom context are not total then the Dhall language, evaluated
        with those functions is not total either.

        `normalizeWith` can fail with an `error` if you normalize an ill-typed
        expression
    -}
    normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith :: forall a s t.
    Eq a =>
    Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith (Just ReifiedNormalizer a
    ctx) Expr s a
    t = Identity (Expr t a) -> Expr t a
    forall a. Identity a -> a
    runIdentity (NormalizerM Identity a -> Expr s a -> Identity (Expr t a)
    forall (m :: * -> *) a s t.
    (Monad m, Eq a) =>
    NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM (ReifiedNormalizer a -> NormalizerM Identity a
    forall a. ReifiedNormalizer a -> Normalizer a
    getReifiedNormalizer ReifiedNormalizer a
    ctx) Expr s a
    t)
    normalizeWith Maybe (ReifiedNormalizer a)
    _          Expr s a
    t = Expr s a -> Expr t a
    forall a s t. Eq a => Expr s a -> Expr t a
    Eval.normalize Expr s a
    t
    {-# INLINABLE normalizeWith #-}

    {-| This function generalizes `normalizeWith` by allowing the custom normalizer
        to use an arbitrary `Monad`

        `normalizeWithM` can fail with an `error` if you normalize an ill-typed
        expression
    -}
    normalizeWithM
        :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM :: forall (m :: * -> *) a s t.
    (Monad m, Eq a) =>
    NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM NormalizerM m a
    ctx Expr s a
    e0 = Expr t a -> m (Expr t a)
    forall {s}. Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr t a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote Expr s a
    e0)
     where
      loop :: Expr s a -> m (Expr s a)
    loop Expr s a
    e = Expr s a -> m (Maybe (Expr s a))
    NormalizerM m a
    ctx Expr s a
    e m (Maybe (Expr s a))
    -> (Maybe (Expr s a) -> m (Expr s a)) -> m (Expr s a)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just Expr s a
    e' -> Expr s a -> m (Expr s a)
    loop Expr s a
    e'
          Maybe (Expr s a)
    Nothing -> case Expr s a
    e of
              Const Const
    k -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    k)
              Var Var
    v -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var Var
    v)
              Lam Maybe CharacterSet
    cs (FunctionBinding { functionBindingVariable :: forall s a. FunctionBinding s a -> Text
    functionBindingVariable = Text
    x, functionBindingAnnotation :: forall s a. FunctionBinding s a -> Expr s a
    functionBindingAnnotation = Expr s a
    _A }) Expr s a
    b ->
                  Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    Lam Maybe CharacterSet
    cs (FunctionBinding s a -> Expr s a -> Expr s a)
    -> m (FunctionBinding s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Text -> Expr s a -> FunctionBinding s a
    forall s a. Text -> Expr s a -> FunctionBinding s a
    Syntax.makeFunctionBinding Text
    x (Expr s a -> FunctionBinding s a)
    -> m (Expr s a) -> m (FunctionBinding s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    _A') m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (Expr s a)
    b'
                where
                  _A' :: m (Expr s a)
    _A' = Expr s a -> m (Expr s a)
    loop Expr s a
    _A
                  b' :: m (Expr s a)
    b'  = Expr s a -> m (Expr s a)
    loop Expr s a
    b
              Pi Maybe CharacterSet
    cs Text
    x Expr s a
    _A Expr s a
    _B -> Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
    Pi Maybe CharacterSet
    cs Text
    x (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    _A' m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (Expr s a)
    _B'
                where
                  _A' :: m (Expr s a)
    _A' = Expr s a -> m (Expr s a)
    loop Expr s a
    _A
                  _B' :: m (Expr s a)
    _B' = Expr s a -> m (Expr s a)
    loop Expr s a
    _B
              App Expr s a
    f Expr s a
    a -> do
                  f' <- Expr s a -> m (Expr s a)
    loop Expr s a
    f
                  a' <- loop a
                  case f' of
                    Lam Maybe CharacterSet
    _ (FunctionBinding Maybe s
    _ Text
    x Maybe s
    _ Maybe s
    _ Expr s a
    _A) Expr s a
    b₀ -> do

                        let a₂ :: Expr s a
    a₂ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift Int
    1 (Text -> Int -> Var
    V Text
    x Int
    0) Expr s a
    a'
                        let b₁ :: Expr s a
    b₁ = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    0) Expr s a
    a₂ Expr s a
    b₀
                        let b₂ :: Expr s a
    b₂ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift (-Int
    1) (Text -> Int -> Var
    V Text
    x Int
    0) Expr s a
    b₁

                        Expr s a -> m (Expr s a)
    loop Expr s a
    b₂
                    Expr s a
    _ ->
                      case Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a' of
                        App (App (App (App Expr s a
    NaturalFold (NaturalLit Natural
    n0)) Expr s a
    t) Expr s a
    succ') Expr s a
    zero -> do
                          t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t
                          if boundedType t' then strict else lazy
                          where
                            -- Use an `Integer` for the loop, due to the following
                            -- issue:
                            --
                            -- https://github.com/ghcjs/ghcjs/issues/782
                            strict :: m (Expr s a)
    strict =       Integer -> m (Expr s a)
    forall {t}. (Num t, Eq t) => t -> m (Expr s a)
    strictLoop (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n0 :: Integer)
                            lazy :: m (Expr s a)
    lazy   = Expr s a -> m (Expr s a)
    loop (  Integer -> Expr s a
    forall {t}. (Eq t, Num t) => t -> Expr s a
    lazyLoop (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n0 :: Integer))

                            strictLoop :: t -> m (Expr s a)
    strictLoop !t
    n = do
                                z <- Expr s a -> m (Expr s a)
    loop Expr s a
    zero
                                strictLoopShortcut n z

                            strictLoopShortcut :: t -> Expr s a -> m (Expr s a)
    strictLoopShortcut t
    0 !Expr s a
    previous = Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    previous
                            strictLoopShortcut !t
    n !Expr s a
    previous = do
                                current <- Expr s a -> m (Expr s a)
    loop (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
    succ' Expr s a
    previous)
                                if judgmentallyEqual previous current
                                    then pure previous
                                    else strictLoopShortcut (n - 1) current

                            lazyLoop :: t -> Expr s a
    lazyLoop t
    0 = Expr s a
    zero
                            lazyLoop !t
    n = 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
    succ' (t -> Expr s a
    lazyLoop (t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1))
                        App Expr s a
    NaturalBuild Expr s a
    g -> Expr s a -> m (Expr s a)
    loop (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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (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
    g Expr s a
    forall s a. Expr s a
    Natural) Expr s a
    forall s a. Expr s a
    succ) Expr s a
    forall s a. Expr s a
    zero)
                          where
                            succ :: Expr s a
    succ = Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    Lam Maybe CharacterSet
    forall a. Monoid a => a
    mempty (Text -> Expr s a -> FunctionBinding s a
    forall s a. Text -> Expr s a -> FunctionBinding s a
    Syntax.makeFunctionBinding Text
    "n" Expr s a
    forall s a. Expr s a
    Natural) (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
    "n" (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    1))

                            zero :: Expr s a
    zero = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0
                        App Expr s a
    NaturalIsZero (NaturalLit Natural
    n) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural
    n Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    0))
                        App Expr s a
    NaturalEven (NaturalLit Natural
    n) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    even Natural
    n))
                        App Expr s a
    NaturalOdd (NaturalLit Natural
    n) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    odd Natural
    n))
                        App Expr s a
    NaturalToInteger (NaturalLit Natural
    n) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger Natural
    n))
                        App Expr s a
    NaturalShow (NaturalLit Natural
    n) ->
                            Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Text.pack (Natural -> String
    forall a. Show a => a -> String
    show Natural
    n))))
                        App (App Expr s a
    NaturalSubtract (NaturalLit Natural
    x)) (NaturalLit Natural
    y)
                            -- Use an `Integer` for the subtraction, due to the
                            -- following issue:
                            --
                            -- https://github.com/ghcjs/ghcjs/issues/782
                            | Natural
    y Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Natural
    x ->
                                Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Integer -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    subtract (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    x :: Integer) (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    y :: Integer))))
                            | Bool
    otherwise ->
                                Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0)
                        App (App Expr s a
    NaturalSubtract (NaturalLit Natural
    0)) Expr s a
    y -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    y
                        App (App Expr s a
    NaturalSubtract Expr s a
    _) (NaturalLit Natural
    0) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0)
                        App (App Expr s a
    NaturalSubtract Expr s a
    x) Expr s a
    y | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    x Expr s a
    y -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0)
                        App Expr s a
    IntegerClamp (IntegerLit Integer
    n)
                            | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    n))
                            | Bool
    otherwise -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0)
                        App Expr s a
    IntegerNegate (IntegerLit Integer
    n) ->
                            Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    n))
                        App Expr s a
    IntegerShow (IntegerLit Integer
    n)
                            | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n    -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (Text
    "+" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack (Integer -> String
    forall a. Show a => a -> String
    show Integer
    n))))
                            | Bool
    otherwise -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Text.pack (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.
                        App Expr s a
    IntegerToDouble (IntegerLit Integer
    n) -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit ((Double -> DhallDouble
    DhallDouble (Double -> DhallDouble)
    -> (Integer -> Double) -> Integer -> DhallDouble
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Double
    forall a. Read a => String -> a
    read (String -> Double) -> (Integer -> String) -> Integer -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> String
    forall a. Show a => a -> String
    show) Integer
    n))
                        App Expr s a
    DoubleShow (DoubleLit (DhallDouble Double
    n)) ->
                            Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Text.pack (Double -> String
    forall a. Show a => a -> String
    show Double
    n))))
                        App (App Expr s a
    ListBuild Expr s a
    _A₀) Expr s a
    g -> Expr s a -> m (Expr s a)
    loop (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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (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
    g Expr s a
    list) Expr s a
    cons) Expr s a
    nil)
                          where
                            _A₁ :: Expr s a
    _A₁ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift Int
    1 Var
    "a" Expr s a
    _A₀

                            list :: Expr s a
    list = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₀

                            cons :: Expr s a
    cons =
                                Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    Lam Maybe CharacterSet
    forall a. Monoid a => a
    mempty (Text -> Expr s a -> FunctionBinding s a
    forall s a. Text -> Expr s a -> FunctionBinding s a
    Syntax.makeFunctionBinding Text
    "a" Expr s a
    _A₀)
                                    (Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
    Lam Maybe CharacterSet
    forall a. Monoid a => a
    mempty
                                        (Text -> Expr s a -> FunctionBinding s a
    forall s a. Text -> Expr s a -> FunctionBinding s a
    Syntax.makeFunctionBinding Text
    "as" (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₁))
                                        (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    forall a. Maybe a
    Nothing (Expr s a -> Seq (Expr s a)
    forall a. a -> Seq a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    "a")) Expr s a
    "as")
                                    )

                            nil :: Expr s a
    nil = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₀)) Seq (Expr s a)
    forall a. Seq a
    forall (f :: * -> *) a. Alternative f => f a
    empty
                        App (App (App (App (App Expr s a
    ListFold Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    xs)) Expr s a
    t) Expr s a
    cons) Expr s a
    nil -> do
                          t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t
                          if boundedType t' then strict else lazy
                          where
                            strict :: m (Expr s a)
    strict =       (Expr s a -> m (Expr s a) -> m (Expr s a))
    -> m (Expr s a) -> Seq (Expr s a) -> m (Expr s a)
    forall a b. (a -> b -> b) -> b -> Seq a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Expr s a -> m (Expr s a) -> m (Expr s a)
    strictCons m (Expr s a)
    strictNil Seq (Expr s a)
    xs
                            lazy :: m (Expr s a)
    lazy   = Expr s a -> m (Expr s a)
    loop ((Expr s a -> Expr s a -> Expr s a)
    -> Expr s a -> Seq (Expr s a) -> Expr s a
    forall a b. (a -> b -> b) -> b -> Seq a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr   Expr s a -> Expr s a -> Expr s a
    lazyCons   Expr s a
    lazyNil Seq (Expr s a)
    xs)

                            strictNil :: m (Expr s a)
    strictNil = Expr s a -> m (Expr s a)
    loop Expr s a
    nil
                            lazyNil :: Expr s a
    lazyNil   =      Expr s a
    nil

                            strictCons :: Expr s a -> m (Expr s a) -> m (Expr s a)
    strictCons Expr s a
    y m (Expr s a)
    ys =
                              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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    cons Expr s a
    y) (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    ys m (Expr s a) -> (Expr s a -> m (Expr s a)) -> m (Expr s a)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Expr s a -> m (Expr s a)
    loop
                            lazyCons :: Expr s a -> Expr s a -> Expr s a
    lazyCons   Expr s a
    y Expr s a
    ys =       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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    cons Expr s a
    y) Expr s a
    ys
                        App (App Expr s a
    ListLength Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    ys) ->
                            Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Seq (Expr s a) -> Int
    forall a. Seq a -> Int
    Data.Sequence.length Seq (Expr s a)
    ys)))
                        App (App Expr s a
    ListHead Expr s a
    t) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    ys) -> Expr s a -> m (Expr s a)
    loop Expr s a
    o
                          where
                            o :: Expr s a
    o = case Seq (Expr s a) -> ViewL (Expr s a)
    forall a. Seq a -> ViewL a
    Data.Sequence.viewl Seq (Expr s a)
    ys of
                                    Expr s a
    y :< Seq (Expr s a)
    _ -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    y
                                    ViewL (Expr s a)
    _      -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    t
                        App (App Expr s a
    ListLast Expr s a
    t) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    ys) -> Expr s a -> m (Expr s a)
    loop Expr s a
    o
                          where
                            o :: Expr s a
    o = case Seq (Expr s a) -> ViewR (Expr s a)
    forall a. Seq a -> ViewR a
    Data.Sequence.viewr Seq (Expr s a)
    ys of
                                    Seq (Expr s a)
    _ :> Expr s a
    y -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    y
                                    ViewR (Expr s a)
    _      -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    t
                        App (App Expr s a
    ListIndexed Expr s a
    _A₀) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    as₀) -> Expr s a -> m (Expr s a)
    loop (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    as₁)
                          where
                            as₁ :: Seq (Expr s a)
    as₁ = (Int -> Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
    forall a b. (Int -> a -> b) -> Seq a -> Seq b
    Data.Sequence.mapWithIndex Int -> Expr s a -> Expr s a
    forall {p} {s} {a}. Integral p => p -> Expr s a -> Expr s a
    adapt Seq (Expr s a)
    as₀

                            _A₂ :: Expr s a
    _A₂ = Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    Record ([(Text, RecordField s a)] -> Map Text (RecordField s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, RecordField s a)]
    kts)
                              where
                                kts :: [(Text, RecordField s a)]
    kts = [ (Text
    "index", Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField Expr s a
    forall s a. Expr s a
    Natural)
                                      , (Text
    "value", Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField Expr s a
    _A₀)
                                      ]

                            t :: Maybe (Expr s a)
    t | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Expr s a)
    as₀  = Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₂)
                              | Bool
    otherwise = Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                            adapt :: p -> Expr s a -> Expr s a
    adapt p
    n Expr s a
    a_ =
                                Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit ([(Text, RecordField s a)] -> Map Text (RecordField s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, RecordField s a)]
    kvs)
                              where
                                kvs :: [(Text, RecordField s a)]
    kvs = [ (Text
    "index", Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
    forall a b. (a -> b) -> a -> b
    $ Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (p -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral p
    n))
                                      , (Text
    "value", Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField Expr s a
    a_)
                                      ]
                        App (App Expr s a
    ListReverse Expr s a
    _) (ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    xs) ->
                            Expr s a -> m (Expr s a)
    loop (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t (Seq (Expr s a) -> Seq (Expr s a)
    forall a. Seq a -> Seq a
    Data.Sequence.reverse Seq (Expr s a)
    xs))
                        App Expr s a
    TextShow (TextLit (Chunks [] Text
    oldText)) ->
                            Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    newText))
                          where
                            newText :: Text
    newText = Text -> Text
    Eval.textShow Text
    oldText
                        App
                            (App (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    ""))) Expr s a
    _)
                            Expr s a
    haystack ->
                                Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    haystack
                        App (App
                                (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    needleText)))
                                (TextLit (Chunks [] Text
    replacementText))
                            )
                            (TextLit (Chunks [(Text, Expr s a)]
    xys Text
    z)) -> do
                                let xys' :: [(Text, Expr s a)]
    xys' = do
                                        (x, y) <- [(Text, Expr s a)]
    xys

                                        let x' = HasCallStack => Text -> Text -> Text -> Text
    Text -> Text -> Text -> Text
    Text.replace Text
    needleText Text
    replacementText Text
    x
                                        return (x', y)

                                let z' :: Text
    z' = HasCallStack => Text -> Text -> Text -> Text
    Text -> Text -> Text -> Text
    Text.replace Text
    needleText Text
    replacementText Text
    z

                                Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text, Expr s a)]
    xys' Text
    z'))
                        App (App
                                (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    needleText)))
                                Expr s a
    replacement
                            )
                            (TextLit (Chunks [] Text
    lastText)) -> do
                                let (Text
    prefix, Text
    suffix) =
                                        HasCallStack => Text -> Text -> (Text, Text)
    Text -> Text -> (Text, Text)
    Text.breakOn Text
    needleText Text
    lastText

                                if Text -> Bool
    Text.null Text
    suffix
                                    then Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    lastText))
                                    else do
                                        let remainder :: Text
    remainder =
                                                Int -> Text -> Text
    Text.drop
                                                    (Text -> Int
    Text.length Text
    needleText)
                                                    Text
    suffix

                                        Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    prefix, Expr s a
    replacement)] Text
    "")) (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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    TextReplace (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    needleText))) Expr s a
    replacement) (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    remainder))))
                        App (App
                                (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    needleText)))
                                Expr s a
    replacement
                            )
                            (TextLit
                                (Chunks
                                    ((Text
    firstText, Expr s a
    firstInterpolation) : [(Text, Expr s a)]
    chunks)
                                    Text
    lastText
                                )
                            ) -> do
                                let (Text
    prefix, Text
    suffix) =
                                        HasCallStack => Text -> Text -> (Text, Text)
    Text -> Text -> (Text, Text)
    Text.breakOn Text
    needleText Text
    firstText

                                if Text -> Bool
    Text.null Text
    suffix
                                    then do
                                        Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    firstText, Expr s a
    firstInterpolation)] Text
    "")) (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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    TextReplace (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    needleText))) Expr s a
    replacement) (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text, Expr s a)]
    chunks Text
    lastText))))
                                    else do
                                        let remainder :: Text
    remainder =
                                                Int -> Text -> Text
    Text.drop
                                                    (Text -> Int
    Text.length Text
    needleText)
                                                    Text
    suffix

                                        Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    TextAppend (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    prefix, Expr s a
    replacement)] Text
    "")) (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 -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    TextReplace (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    needleText))) Expr s a
    replacement) (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks ((Text
    remainder, Expr s a
    firstInterpolation) (Text, Expr s a) -> [(Text, Expr s a)] -> [(Text, Expr s a)]
    forall a. a -> [a] -> [a]
    : [(Text, Expr s a)]
    chunks) Text
    lastText))))
                        App Expr s a
    DateShow (DateLiteral Day
    date) ->
                            Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    text))
                          where
                            text :: Text
    text = Day -> Text
    Eval.dateShow Day
    date
                        App Expr s a
    TimeShow (TimeLiteral TimeOfDay
    time Word
    precision) ->
                            Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    text))
                          where
                            text :: Text
    text = TimeOfDay -> Word -> Text
    Eval.timeShow TimeOfDay
    time Word
    precision
                        App Expr s a
    TimeZoneShow (TimeZoneLiteral TimeZone
    timezone) ->
                            Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    text))
                          where
                            text :: Text
    text = TimeZone -> Text
    Eval.timezoneShow TimeZone
    timezone
                        Expr s a
    _ -> do
                            res2 <- Expr s a -> m (Maybe (Expr s a))
    NormalizerM m a
    ctx (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a')
                            case res2 of
                                Maybe (Expr s a)
    Nothing -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a')
                                Just Expr s a
    app' -> Expr s a -> m (Expr s a)
    loop Expr s a
    app'
              Let (Binding Maybe s
    _ Text
    f Maybe s
    _ Maybe (Maybe s, Expr s a)
    _ Maybe s
    _ Expr s a
    r) Expr s a
    b -> Expr s a -> m (Expr s a)
    loop Expr s a
    b''
                where
                  r' :: Expr s a
    r'  = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift   Int
    1  (Text -> Int -> Var
    V Text
    f Int
    0) Expr s a
    r
                  b' :: Expr s a
    b'  = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    f Int
    0) Expr s a
    r' Expr s a
    b
                  b'' :: Expr s a
    b'' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    Syntax.shift (-Int
    1) (Text -> Int -> Var
    V Text
    f Int
    0) Expr s a
    b'
              Annot Expr s a
    x Expr s a
    _ -> Expr s a -> m (Expr s a)
    loop Expr s a
    x
              Expr s a
    Bool -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Bool
              BoolLit Bool
    b -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    b)
              BoolAnd Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr t a -> Expr t a -> Expr t a
    decide (BoolLit Bool
    True )  Expr t a
    r              = Expr t a
    r
                  decide (BoolLit Bool
    False)  Expr t a
    _              = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
                  decide  Expr t a
    l              (BoolLit Bool
    True ) = Expr t a
    l
                  decide  Expr t a
    _              (BoolLit Bool
    False) = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
                  decide  Expr t a
    l               Expr t a
    r
                      | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r = Expr t a
    l
                      | Bool
    otherwise                  = Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolAnd Expr t a
    l Expr t a
    r
              BoolOr Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr t a -> Expr t a -> Expr t a
    decide (BoolLit Bool
    False)  Expr t a
    r              = Expr t a
    r
                  decide (BoolLit Bool
    True )  Expr t a
    _              = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
                  decide  Expr t a
    l              (BoolLit Bool
    False) = Expr t a
    l
                  decide  Expr t a
    _              (BoolLit Bool
    True ) = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
                  decide  Expr t a
    l               Expr t a
    r
                      | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r = Expr t a
    l
                      | Bool
    otherwise                  = Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolOr Expr t a
    l Expr t a
    r
              BoolEQ Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr t a -> Expr t a -> Expr t a
    decide (BoolLit Bool
    True )  Expr t a
    r              = Expr t a
    r
                  decide  Expr t a
    l              (BoolLit Bool
    True ) = Expr t a
    l
                  decide  Expr t a
    l               Expr t a
    r
                      | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
                      | Bool
    otherwise                  = Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolEQ Expr t a
    l Expr t a
    r
              BoolNE Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr t a -> Expr t a -> Expr t a
    decide (BoolLit Bool
    False)  Expr t a
    r              = Expr t a
    r
                  decide  Expr t a
    l              (BoolLit Bool
    False) = Expr t a
    l
                  decide  Expr t a
    l               Expr t a
    r
                      | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r = Bool -> Expr t a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
                      | Bool
    otherwise                  = Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolNE Expr t a
    l Expr t a
    r
              BoolIf Expr s a
    bool Expr s a
    true Expr s a
    false -> Expr s a -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}.
    Eq a =>
    Expr t a -> Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    bool m (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    true m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    false
                where
                  decide :: Expr t a -> Expr t a -> Expr t a -> Expr t a
    decide (BoolLit Bool
    True )  Expr t a
    l              Expr t a
    _              = Expr t a
    l
                  decide (BoolLit Bool
    False)  Expr t a
    _              Expr t a
    r              = Expr t a
    r
                  decide  Expr t a
    b              (BoolLit Bool
    True) (BoolLit Bool
    False) = Expr t a
    b
                  decide  Expr t a
    b               Expr t a
    l              Expr t a
    r
                      | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r = Expr t a
    l
                      | Bool
    otherwise                  = Expr t a -> Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
    BoolIf Expr t a
    b Expr t a
    l Expr t a
    r
              Expr s a
    Bytes -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Bytes
              BytesLit ByteString
    b -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ByteString -> Expr s a
    forall s a. ByteString -> Expr s a
    BytesLit ByteString
    b)
              Expr s a
    Natural -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Natural
              NaturalLit Natural
    n -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    n)
              Expr s a
    NaturalFold -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalFold
              Expr s a
    NaturalBuild -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalBuild
              Expr s a
    NaturalIsZero -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalIsZero
              Expr s a
    NaturalEven -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalEven
              Expr s a
    NaturalOdd -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalOdd
              Expr s a
    NaturalToInteger -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalToInteger
              Expr s a
    NaturalShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalShow
              Expr s a
    NaturalSubtract -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalSubtract
              NaturalPlus Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr s a -> Expr s a -> Expr s a
    decide (NaturalLit Natural
    0)  Expr s a
    r             = Expr s a
    r
                  decide  Expr s a
    l             (NaturalLit Natural
    0) = Expr s a
    l
                  decide (NaturalLit Natural
    m) (NaturalLit Natural
    n) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    n)
                  decide  Expr s a
    l              Expr s a
    r             = 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
    l Expr s a
    r
              NaturalTimes Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr s a -> Expr s a -> Expr s a
    decide (NaturalLit Natural
    1)  Expr s a
    r             = Expr s a
    r
                  decide  Expr s a
    l             (NaturalLit Natural
    1) = Expr s a
    l
                  decide (NaturalLit Natural
    0)  Expr s a
    _             = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0
                  decide  Expr s a
    _             (NaturalLit Natural
    0) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    0
                  decide (NaturalLit Natural
    m) (NaturalLit Natural
    n) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    n)
                  decide  Expr s a
    l              Expr s a
    r             = 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
    l Expr s a
    r
              Expr s a
    Integer -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Integer
              IntegerLit Integer
    n -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit Integer
    n)
              Expr s a
    IntegerClamp -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerClamp
              Expr s a
    IntegerNegate -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerNegate
              Expr s a
    IntegerShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerShow
              Expr s a
    IntegerToDouble -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerToDouble
              Expr s a
    Double -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Double
              DoubleLit DhallDouble
    n -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit DhallDouble
    n)
              Expr s a
    DoubleShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    DoubleShow
              Expr s a
    Text -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Text
              TextLit (Chunks [(Text, Expr s a)]
    xys Text
    z) -> do
                  chunks' <- [Chunks s a] -> Chunks s a
    forall a. Monoid a => [a] -> a
    mconcat ([Chunks s a] -> Chunks s a) -> m [Chunks s a] -> m (Chunks s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [Chunks s a]
    chunks
                  case chunks' of
                      Chunks [(Text
    "", Expr s a
    x)] Text
    "" -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    x
                      Chunks s a
    c                   -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit Chunks s a
    c)
                where
                  chunks :: m [Chunks s a]
    chunks =
                    (([Chunks s a] -> [Chunks s a] -> [Chunks s a]
    forall a. [a] -> [a] -> [a]
    ++ [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    z]) ([Chunks s a] -> [Chunks s a])
    -> ([[Chunks s a]] -> [Chunks s a])
    -> [[Chunks s a]]
    -> [Chunks s a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Chunks s a]] -> [Chunks s a]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat) ([[Chunks s a]] -> [Chunks s a])
    -> m [[Chunks s a]] -> m [Chunks s a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Text, Expr s a) -> m [Chunks s a])
    -> [(Text, Expr s a)] -> m [[Chunks s a]]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (Text, Expr s a) -> m [Chunks s a]
    process [(Text, Expr s a)]
    xys

                  process :: (Text, Expr s a) -> m [Chunks s a]
    process (Text
    x, Expr s a
    y) = do
                    y' <- Expr s a -> m (Expr s a)
    loop Expr s a
    y
                    case y' of
                      TextLit Chunks s a
    c -> [Chunks s a] -> m [Chunks s a]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    x, Chunks s a
    c]
                      Expr s a
    _         -> [Chunks s a] -> m [Chunks s a]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    x, Expr s a
    y')] Text
    forall a. Monoid a => a
    mempty]
              TextAppend Expr s a
    x Expr s a
    y -> Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    "", Expr s a
    x), (Text
    "", Expr s a
    y)] Text
    ""))
              Expr s a
    TextReplace -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TextReplace
              Expr s a
    TextShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TextShow
              Expr s a
    Date -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Date
              DateLiteral Day
    d -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Day -> Expr s a
    forall s a. Day -> Expr s a
    DateLiteral Day
    d)
              Expr s a
    DateShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    DateShow
              Expr s a
    Time -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Time
              TimeLiteral TimeOfDay
    t Word
    p -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TimeOfDay -> Word -> Expr s a
    forall s a. TimeOfDay -> Word -> Expr s a
    TimeLiteral TimeOfDay
    t Word
    p)
              Expr s a
    TimeShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TimeShow
              Expr s a
    TimeZone -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TimeZone
              TimeZoneLiteral TimeZone
    z -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TimeZone -> Expr s a
    forall s a. TimeZone -> Expr s a
    TimeZoneLiteral TimeZone
    z)
              Expr s a
    TimeZoneShow -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TimeZoneShow
              Expr s a
    List -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    List
              ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    es
                  | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    es -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Seq (Expr s a) -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t' m (Seq (Expr s a) -> Expr s a)
    -> m (Seq (Expr s a)) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Seq (Expr s a) -> m (Seq (Expr s a))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Seq (Expr s a)
    forall a. Seq a
    Data.Sequence.empty
                  | Bool
    otherwise             -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    forall a. Maybe a
    Nothing (Seq (Expr s a) -> Expr s a) -> m (Seq (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Seq (Expr s a))
    es'
                where
                  t' :: m (Maybe (Expr s a))
    t'  = (Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse Expr s a -> m (Expr s a)
    loop Maybe (Expr s a)
    t
                  es' :: m (Seq (Expr s a))
    es' = (Expr s a -> m (Expr s a)) -> Seq (Expr s a) -> m (Seq (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Seq a -> f (Seq b)
    traverse Expr s a -> m (Expr s a)
    loop Seq (Expr s a)
    es
              ListAppend Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr s a -> Expr s a -> Expr s a
    decide (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    m)  Expr s a
    r            | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    m = Expr s a
    r
                  decide  Expr s a
    l            (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    n) | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    n = Expr s a
    l
                  decide (ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    m) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    n)                        = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t (Seq (Expr s a)
    m Seq (Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
    forall a. Semigroup a => a -> a -> a
    <> Seq (Expr s a)
    n)
                  decide  Expr s a
    l             Expr s a
    r                                   = 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
    l Expr s a
    r
              Expr s a
    ListBuild -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListBuild
              Expr s a
    ListFold -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListFold
              Expr s a
    ListLength -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListLength
              Expr s a
    ListHead -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListHead
              Expr s a
    ListLast -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListLast
              Expr s a
    ListIndexed -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListIndexed
              Expr s a
    ListReverse -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListReverse
              Expr s a
    Optional -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Optional
              Some Expr s a
    a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    a'
                where
                  a' :: m (Expr s a)
    a' = Expr s a -> m (Expr s a)
    loop Expr s a
    a
              Expr s a
    None -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    None
              Record Map Text (RecordField s a)
    kts -> Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    Record (Map Text (RecordField s a) -> Expr s a)
    -> (Map Text (RecordField s a) -> Map Text (RecordField s a))
    -> Map Text (RecordField s a)
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (RecordField s a) -> Map Text (RecordField s a)
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (RecordField s a) -> Expr s a)
    -> m (Map Text (RecordField s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (RecordField s a))
    kts'
                where
                  f :: RecordField s a -> m (RecordField s a)
    f (RecordField Maybe s
    s0 Expr s a
    expr Maybe s
    s1 Maybe s
    s2) = (\Expr s a
    expr' -> Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
    forall s a.
    Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
    RecordField Maybe s
    s0 Expr s a
    expr' Maybe s
    s1 Maybe s
    s2) (Expr s a -> RecordField s a)
    -> m (Expr s a) -> m (RecordField s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    expr
                  kts' :: m (Map Text (RecordField s a))
    kts' = (RecordField s a -> m (RecordField s a))
    -> Map Text (RecordField s a) -> m (Map Text (RecordField s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Text a -> f (Map Text b)
    traverse RecordField s a -> m (RecordField s a)
    f Map Text (RecordField s a)
    kts
              RecordLit Map Text (RecordField s a)
    kvs -> Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Map Text (RecordField s a) -> Expr s a)
    -> (Map Text (RecordField s a) -> Map Text (RecordField s a))
    -> Map Text (RecordField s a)
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (RecordField s a) -> Map Text (RecordField s a)
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (RecordField s a) -> Expr s a)
    -> m (Map Text (RecordField s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (RecordField s a))
    kvs'
                where
                  f :: RecordField s a -> m (RecordField s a)
    f (RecordField Maybe s
    s0 Expr s a
    expr Maybe s
    s1 Maybe s
    s2) = (\Expr s a
    expr' -> Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
    forall s a.
    Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
    RecordField Maybe s
    s0 Expr s a
    expr' Maybe s
    s1 Maybe s
    s2) (Expr s a -> RecordField s a)
    -> m (Expr s a) -> m (RecordField s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    expr
                  kvs' :: m (Map Text (RecordField s a))
    kvs' = (RecordField s a -> m (RecordField s a))
    -> Map Text (RecordField s a) -> m (Map Text (RecordField s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Text a -> f (Map Text b)
    traverse RecordField s a -> m (RecordField s a)
    f Map Text (RecordField s a)
    kvs
              Union 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 (Map Text (Maybe (Expr s a)) -> Expr s a)
    -> (Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a)))
    -> Map Text (Maybe (Expr s a))
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (Maybe (Expr s a)) -> Expr s a)
    -> m (Map Text (Maybe (Expr s a))) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (Maybe (Expr s a)))
    kts'
                where
                  kts' :: m (Map Text (Maybe (Expr s a)))
    kts' = (Maybe (Expr s a) -> m (Maybe (Expr s a)))
    -> Map Text (Maybe (Expr s a)) -> m (Map Text (Maybe (Expr s a)))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Text a -> f (Map Text b)
    traverse ((Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse Expr s a -> m (Expr s a)
    loop) Map Text (Maybe (Expr s a))
    kts
              Combine Maybe CharacterSet
    cs Maybe Text
    mk Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr s a -> Expr s a -> Expr s a
    decide (RecordLit Map Text (RecordField s a)
    m) Expr s a
    r | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    m =
                      Expr s a
    r
                  decide Expr s a
    l (RecordLit Map Text (RecordField s a)
    n) | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    n =
                      Expr s a
    l
                  decide (RecordLit Map Text (RecordField s a)
    m) (RecordLit Map Text (RecordField s a)
    n) =
                      Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit ((RecordField s a -> RecordField s a -> RecordField s a)
    -> Map Text (RecordField s a)
    -> Map Text (RecordField s a)
    -> Map Text (RecordField s a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Dhall.Map.unionWith RecordField s a -> RecordField s a -> RecordField s a
    f Map Text (RecordField s a)
    m Map Text (RecordField s a)
    n)
                    where
                      f :: RecordField s a -> RecordField s a -> RecordField s a
    f (RecordField Maybe s
    _ Expr s a
    expr Maybe s
    _ Maybe s
    _) (RecordField Maybe s
    _ Expr s a
    expr' Maybe s
    _ Maybe s
    _) =
                        Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
    forall a b. (a -> b) -> a -> b
    $ Expr s a -> Expr s a -> Expr s a
    decide Expr s a
    expr Expr s a
    expr'
                  decide Expr s a
    l Expr s a
    r =
                      Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe CharacterSet
    cs Maybe Text
    mk Expr s a
    l Expr s a
    r
              CombineTypes Maybe CharacterSet
    cs Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr s a -> Expr s a -> Expr s a
    decide (Record Map Text (RecordField s a)
    m) Expr s a
    r | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    m =
                      Expr s a
    r
                  decide Expr s a
    l (Record Map Text (RecordField s a)
    n) | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    n =
                      Expr s a
    l
                  decide (Record Map Text (RecordField s a)
    m) (Record Map Text (RecordField s a)
    n) =
                      Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    Record ((RecordField s a -> RecordField s a -> RecordField s a)
    -> Map Text (RecordField s a)
    -> Map Text (RecordField s a)
    -> Map Text (RecordField s a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Dhall.Map.unionWith RecordField s a -> RecordField s a -> RecordField s a
    f Map Text (RecordField s a)
    m Map Text (RecordField s a)
    n)
                    where
                      f :: RecordField s a -> RecordField s a -> RecordField s a
    f (RecordField Maybe s
    _ Expr s a
    expr Maybe s
    _ Maybe s
    _) (RecordField Maybe s
    _ Expr s a
    expr' Maybe s
    _ Maybe s
    _) =
                        Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
    forall a b. (a -> b) -> a -> b
    $ Expr s a -> Expr s a -> Expr s a
    decide Expr s a
    expr Expr s a
    expr'
                  decide Expr s a
    l Expr s a
    r =
                      Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
    forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
    CombineTypes Maybe CharacterSet
    cs Expr s a
    l Expr s a
    r
              Prefer Maybe CharacterSet
    cs PreferAnnotation
    _ Expr s a
    x Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
                where
                  decide :: Expr t a -> Expr t a -> Expr t a
    decide (RecordLit Map Text (RecordField t a)
    m) Expr t a
    r | Map Text (RecordField t a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField t a)
    m =
                      Expr t a
    r
                  decide Expr t a
    l (RecordLit Map Text (RecordField t a)
    n) | Map Text (RecordField t a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField t a)
    n =
                      Expr t a
    l
                  decide (RecordLit Map Text (RecordField t a)
    m) (RecordLit Map Text (RecordField t a)
    n) =
                      Map Text (RecordField t a) -> Expr t a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Map Text (RecordField t a)
    -> Map Text (RecordField t a) -> Map Text (RecordField t a)
    forall k v. Ord k => Map k v -> Map k v -> Map k v
    Dhall.Map.union Map Text (RecordField t a)
    n Map Text (RecordField t a)
    m)
                  decide Expr t a
    l Expr t a
    r | Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    l Expr t a
    r =
                      Expr t a
    l
                  decide Expr t a
    l Expr t a
    r =
                      Maybe CharacterSet
    -> PreferAnnotation -> Expr t a -> Expr t a -> Expr t a
    forall s a.
    Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    Prefer Maybe CharacterSet
    cs PreferAnnotation
    PreferFromSource Expr t a
    l Expr t a
    r
              RecordCompletion Expr s a
    x Expr s a
    y ->
                  Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Annot (Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    Prefer Maybe CharacterSet
    forall a. Monoid a => a
    mempty PreferAnnotation
    PreferFromCompletion (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    x FieldSelection s
    forall {s}. FieldSelection s
    def) Expr s a
    y) (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    x FieldSelection s
    forall {s}. FieldSelection s
    typ))
                where
                  def :: FieldSelection s
    def = Text -> FieldSelection s
    forall s. Text -> FieldSelection s
    Syntax.makeFieldSelection Text
    "default"
                  typ :: FieldSelection s
    typ = Text -> FieldSelection s
    forall s. Text -> FieldSelection s
    Syntax.makeFieldSelection Text
    "Type"
              Merge Expr s a
    x Expr s a
    y Maybe (Expr s a)
    t      -> do
                  x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
                  y' <- loop y
                  case x' of
                      RecordLit Map Text (RecordField s a)
    kvsX ->
                          case Expr s a
    y' of
                              Field (Union Map Text (Maybe (Expr s a))
    ktsY) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    kY) ->
                                  case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                                      Just Maybe (Expr s a)
    Nothing ->
                                          case RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue (RecordField s a -> Expr s a)
    -> Maybe (RecordField s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (RecordField s a)
    kvsX of
                                              Just Expr s a
    vX -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    vX
                                              Maybe (Expr s a)
    Nothing -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                                      Maybe (Maybe (Expr s a))
    _ ->
                                          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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                              App (Field (Union Map Text (Maybe (Expr s a))
    ktsY) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    kY)) Expr s a
    vY ->
                                  case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                                      Just (Just Expr s a
    _) ->
                                          case RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue (RecordField s a -> Expr s a)
    -> Maybe (RecordField s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (RecordField s a)
    kvsX of
                                              Just Expr s a
    vX -> Expr s a -> m (Expr s a)
    loop (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
    vX Expr s a
    vY)
                                              Maybe (Expr s a)
    Nothing -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                                      Maybe (Maybe (Expr s a))
    _ ->
                                          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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                              Some Expr s a
    a ->
                                  case RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue (RecordField s a -> Expr s a)
    -> Maybe (RecordField s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    "Some" Map Text (RecordField s a)
    kvsX of
                                      Just Expr s a
    vX -> Expr s a -> m (Expr s a)
    loop (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
    vX Expr s a
    a)
                                      Maybe (Expr s a)
    Nothing -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                              App Expr s a
    None Expr s a
    _ ->
                                  case RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue (RecordField s a -> Expr s a)
    -> Maybe (RecordField s a) -> Maybe (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    "None" Map Text (RecordField s a)
    kvsX of
                                      Just Expr s a
    vX -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    vX
                                      Maybe (Expr s a)
    Nothing -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                              Expr s a
    _ -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                      Expr s a
    _ -> 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
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                where
                  t' :: m (Maybe (Expr s a))
    t' = (Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse Expr s a -> m (Expr s a)
    loop Maybe (Expr s a)
    t
              ToMap Expr s a
    x Maybe (Expr s a)
    t        -> do
                  x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
                  t' <- traverse loop t
                  case x' of
                      RecordLit Map Text (RecordField s a)
    kvsX -> do
                          let entry :: (Text, Expr s a) -> Expr s a
    entry (Text
    key, Expr s a
    value) =
                                  Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit
                                      ([(Text, RecordField s a)] -> Map Text (RecordField s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList
                                          [ (Text
    "mapKey"  , Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
    forall a b. (a -> b) -> a -> b
    $ Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    key))
                                          , (Text
    "mapValue", Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField Expr s a
    value                  )
                                          ]
                                      )

                          let keyValues :: Seq (Expr s a)
    keyValues = [Expr s a] -> Seq (Expr s a)
    forall a. [a] -> Seq a
    Data.Sequence.fromList (((Text, Expr s a) -> Expr s a) -> [(Text, Expr s a)] -> [Expr s a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text, Expr s a) -> Expr s a
    forall {s} {a}. (Text, Expr s a) -> Expr s a
    entry (Map Text (Expr s a) -> [(Text, Expr s a)]
    forall k v. Ord k => Map k v -> [(k, v)]
    Dhall.Map.toList (Map Text (Expr s a) -> [(Text, Expr s a)])
    -> Map Text (Expr s a) -> [(Text, Expr s a)]
    forall a b. (a -> b) -> a -> b
    $ RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue (RecordField s a -> Expr s a)
    -> Map Text (RecordField s a) -> Map Text (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Map Text (RecordField s a)
    kvsX))

                          let listType :: Maybe (Expr s a)
    listType = case Maybe (Expr s a)
    t' of
                                  Just Expr s a
    _ | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Expr s a)
    keyValues ->
                                      Maybe (Expr s a)
    t'
                                  Maybe (Expr s a)
    _ ->
                                      Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                          Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    listType Seq (Expr s a)
    keyValues)
                      Expr s a
    _ ->
                          Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
    ToMap Expr s a
    x' Maybe (Expr s a)
    t')
              ShowConstructor Expr s a
    x -> do
                  x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
                  return $ case x' of
                      Field (Union Map Text (Maybe (Expr s a))
    ktsY) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    kY) ->
                          case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                              Just Maybe (Expr s a)
    Nothing -> Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    kY)
                              Maybe (Maybe (Expr s a))
    _ -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    ShowConstructor Expr s a
    x'
                      App (Field (Union Map Text (Maybe (Expr s a))
    ktsY) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    kY)) Expr s a
    _ ->
                          case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                              Just (Just Expr s a
    _) -> Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    kY)
                              Maybe (Maybe (Expr s a))
    _ -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    ShowConstructor Expr s a
    x'
                      Some Expr s a
    _ ->
                          Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    "Some")
                      App Expr s a
    None Expr s a
    _ ->
                          Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    "None")
                      Expr s a
    _ -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    ShowConstructor Expr s a
    x'
              Field Expr s a
    r k :: FieldSelection s
    k@FieldSelection{fieldSelectionLabel :: forall s. FieldSelection s -> Text
    fieldSelectionLabel = Text
    x}        -> do
                  let singletonRecordLit :: RecordField s a -> Expr s a
    singletonRecordLit RecordField s a
    v = Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Text -> RecordField s a -> Map Text (RecordField s a)
    forall k v. k -> v -> Map k v
    Dhall.Map.singleton Text
    x RecordField s a
    v)

                  r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r
                  case r' of
                      RecordLit Map Text (RecordField s a)
    kvs ->
                          case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (RecordField s a)
    kvs of
                              Just RecordField s a
    v  -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> m (Expr s a)) -> Expr s a -> m (Expr s a)
    forall a b. (a -> b) -> a -> b
    $ RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue RecordField s a
    v
                              Maybe (RecordField s a)
    Nothing -> Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field (Expr s a -> FieldSelection s -> Expr s a)
    -> m (Expr s a) -> m (FieldSelection s -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Map Text (RecordField s a) -> Expr s a)
    -> m (Map Text (RecordField s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (RecordField s a -> m (RecordField s a))
    -> Map Text (RecordField s a) -> m (Map Text (RecordField s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Text a -> f (Map Text b)
    traverse ((Expr s a -> m (Expr s a))
    -> RecordField s a -> m (RecordField s a)
    forall (f :: * -> *) s a b.
    Applicative f =>
    (Expr s a -> f (Expr s b))
    -> RecordField s a -> f (RecordField s b)
    Syntax.recordFieldExprs Expr s a -> m (Expr s a)
    loop) Map Text (RecordField s a)
    kvs) m (FieldSelection s -> Expr s a)
    -> m (FieldSelection s) -> m (Expr s a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> FieldSelection s -> m (FieldSelection s)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure FieldSelection s
    k
                      Project Expr s a
    r_ Either [Text] (Expr s a)
    _ -> Expr s a -> m (Expr s a)
    loop (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    r_ FieldSelection s
    k)
                      Prefer Maybe CharacterSet
    cs PreferAnnotation
    _ (RecordLit Map Text (RecordField s a)
    kvs) Expr s a
    r_ -> case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (RecordField s a)
    kvs of
                          Just RecordField s a
    v -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field (Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    Prefer Maybe CharacterSet
    cs PreferAnnotation
    PreferFromSource (RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    singletonRecordLit RecordField s a
    v) Expr s a
    r_) FieldSelection s
    k)
                          Maybe (RecordField s a)
    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    r_ FieldSelection s
    k)
                      Prefer Maybe CharacterSet
    _ PreferAnnotation
    _ Expr s a
    l (RecordLit Map Text (RecordField s a)
    kvs) -> case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (RecordField s a)
    kvs of
                          Just RecordField s a
    v -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> m (Expr s a)) -> Expr s a -> m (Expr s a)
    forall a b. (a -> b) -> a -> b
    $ RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    recordFieldValue RecordField s a
    v
                          Maybe (RecordField s a)
    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    l FieldSelection s
    k)
                      Combine Maybe CharacterSet
    cs Maybe Text
    m (RecordLit Map Text (RecordField s a)
    kvs) Expr s a
    r_ -> case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (RecordField s a)
    kvs of
                          Just RecordField s a
    v -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field (Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe CharacterSet
    cs Maybe Text
    m (RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    singletonRecordLit RecordField s a
    v) Expr s a
    r_) FieldSelection s
    k)
                          Maybe (RecordField s a)
    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    r_ FieldSelection s
    k)
                      Combine Maybe CharacterSet
    cs Maybe Text
    m Expr s a
    l (RecordLit Map Text (RecordField s a)
    kvs) -> case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (RecordField s a)
    kvs of
                          Just RecordField s a
    v -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field (Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe CharacterSet
    cs Maybe Text
    m Expr s a
    l (RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    singletonRecordLit RecordField s a
    v)) FieldSelection s
    k)
                          Maybe (RecordField s a)
    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    l FieldSelection s
    k)
                      Expr s a
    _ -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> FieldSelection s -> Expr s a
    forall s a. Expr s a -> FieldSelection s -> Expr s a
    Field Expr s a
    r' FieldSelection s
    k)
              Project Expr s a
    x (Left [Text]
    fields)-> do
                  x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
                  let fieldsSet = [Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Data.Set.fromList [Text]
    fields
                  case x' of
                      RecordLit Map Text (RecordField s a)
    kvs ->
                          Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Map Text (RecordField s a)
    -> Set Text -> Map Text (RecordField s a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Dhall.Map.restrictKeys Map Text (RecordField s a)
    kvs Set Text
    fieldsSet))
                      Project Expr s a
    y Either [Text] (Expr s a)
    _ ->
                          Expr s a -> m (Expr s a)
    loop (Expr s a -> Either [Text] (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
    Project Expr s a
    y ([Text] -> Either [Text] (Expr s a)
    forall a b. a -> Either a b
    Left [Text]
    fields))
                      Prefer Maybe CharacterSet
    cs PreferAnnotation
    _ Expr s a
    l (RecordLit Map Text (RecordField s a)
    rKvs) -> do
                          let rKs :: Set Text
    rKs = Map Text (RecordField s a) -> Set Text
    forall k v. Map k v -> Set k
    Dhall.Map.keysSet Map Text (RecordField s a)
    rKvs
                          let l' :: Expr s a
    l' = Expr s a -> Either [Text] (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
    Project Expr s a
    l ([Text] -> Either [Text] (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> [Text]
    forall a. Set a -> [a]
    Data.Set.toList (Set Text -> Set Text -> Set Text
    forall a. Ord a => Set a -> Set a -> Set a
    Data.Set.difference Set Text
    fieldsSet Set Text
    rKs)))
                          let r' :: Expr s a
    r' = Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Map Text (RecordField s a)
    -> Set Text -> Map Text (RecordField s a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Dhall.Map.restrictKeys Map Text (RecordField s a)
    rKvs Set Text
    fieldsSet)
                          Expr s a -> m (Expr s a)
    loop (Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    Maybe CharacterSet
    -> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
    Prefer Maybe CharacterSet
    cs PreferAnnotation
    PreferFromSource Expr s a
    l' Expr s a
    r')
                      Expr s a
    _ | [Text] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Text]
    fields -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit Map Text (RecordField s a)
    forall a. Monoid a => a
    mempty)
                        | Bool
    otherwise   -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Either [Text] (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
    Project Expr s a
    x' ([Text] -> Either [Text] (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> [Text]
    forall a. Set a -> [a]
    Data.Set.toList ([Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Data.Set.fromList [Text]
    fields))))
              Project Expr s a
    r (Right Expr s a
    e1) -> do
                  e2 <- Expr s a -> m (Expr s a)
    loop Expr s a
    e1

                  case e2 of
                      Record Map Text (RecordField s a)
    kts ->
                          Expr s a -> m (Expr s a)
    loop (Expr s a -> Either [Text] (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
    Project Expr s a
    r ([Text] -> Either [Text] (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> [Text]
    forall a. Set a -> [a]
    Data.Set.toList (Map Text (RecordField s a) -> Set Text
    forall k v. Map k v -> Set k
    Dhall.Map.keysSet Map Text (RecordField s a)
    kts))))
                      Expr s a
    _ -> do
                          r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r
                          pure (Project r' (Right e2))
              Assert Expr s a
    t -> do
                  t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t

                  pure (Assert t')
              Equivalent Maybe CharacterSet
    cs Expr s a
    l Expr s a
    r -> do
                  l' <- Expr s a -> m (Expr s a)
    loop Expr s a
    l
                  r' <- loop r

                  pure (Equivalent cs l' r')
              With Expr s a
    r NonEmpty WithComponent
    ks Expr s a
    v -> do
                  r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r
                  v' <- loop v

                  case r' of
                      RecordLit Map Text (RecordField s a)
    kvs ->
                          case NonEmpty WithComponent
    ks of
                              WithLabel Text
    k :| [] ->
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit (Text
    -> RecordField s a
    -> Map Text (RecordField s a)
    -> Map Text (RecordField s a)
    forall k v. Ord k => k -> v -> Map k v -> Map k v
    Dhall.Map.insert Text
    k (Expr s a -> RecordField s a
    forall s a. Expr s a -> RecordField s a
    Syntax.makeRecordField Expr s a
    v') Map Text (RecordField s a)
    kvs))
                              WithLabel Text
    k₀ :| WithComponent
    k₁ : [WithComponent]
    ks' -> do
                                  let e₁ :: Expr s a
    e₁ =
                                          case Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    k₀ Map Text (RecordField s a)
    kvs of
                                              Maybe (RecordField s a)
    Nothing  -> Map Text (RecordField s a) -> Expr s a
    forall s a. Map Text (RecordField s a) -> Expr s a
    RecordLit Map Text (RecordField s a)
    forall a. Monoid a => a
    mempty
                                              Just RecordField s a
    val -> RecordField s a -> Expr s a
    forall s a. RecordField s a -> Expr s a
    Syntax.recordFieldValue RecordField s a
    val

                                  e₂ <- Expr s a -> m (Expr s a)
    loop (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    e₁ (WithComponent
    k₁ WithComponent -> [WithComponent] -> NonEmpty WithComponent
    forall a. a -> [a] -> NonEmpty a
    :| [WithComponent]
    ks') Expr s a
    v')

                                  return (RecordLit (Dhall.Map.insert k₀ (Syntax.makeRecordField e₂) kvs))
                              WithComponent
    WithQuestion :| [WithComponent]
    _ -> do
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    r' NonEmpty WithComponent
    ks Expr s a
    v')
                      Some Expr s a
    t ->
                          case NonEmpty WithComponent
    ks of
                              WithComponent
    WithQuestion :| [] -> do
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    v')
                              WithComponent
    WithQuestion :| WithComponent
    k : [WithComponent]
    ks' -> do
                                  w <- Expr s a -> m (Expr s a)
    loop (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    t (WithComponent
    k WithComponent -> [WithComponent] -> NonEmpty WithComponent
    forall a. a -> [a] -> NonEmpty a
    :| [WithComponent]
    ks') Expr s a
    v)
                                  return (Some w)
                              WithLabel Text
    _ :| [WithComponent]
    _ ->
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    r' NonEmpty WithComponent
    ks Expr s a
    v')
                      App Expr s a
    None Expr s a
    _T ->
                          case NonEmpty WithComponent
    ks of
                              WithComponent
    WithQuestion :| [WithComponent]
    _ ->
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    _T)
                              WithLabel Text
    _ :| [WithComponent]
    _ ->
                                  Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    r' NonEmpty WithComponent
    ks Expr s a
    v')
                      Expr s a
    _ ->
                          Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    forall s a.
    Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
    With Expr s a
    r' NonEmpty WithComponent
    ks Expr s a
    v')
              Note s
    _ Expr s a
    e' -> Expr s a -> m (Expr s a)
    loop Expr s a
    e'
              ImportAlt Expr s a
    l Expr s a
    _r -> Expr s a -> m (Expr s a)
    loop Expr s a
    l
              Embed a
    a -> Expr s a -> m (Expr s a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> Expr s a
    forall s a. a -> Expr s a
    Embed a
    a)

    -- | Use this to wrap you embedded functions (see `normalizeWith`) to make them
    --   polymorphic enough to be used.
    type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))

    -- | An variation on `NormalizerM` for pure normalizers
    type Normalizer a = NormalizerM Identity a

    -- | A reified 'Normalizer', which can be stored in structures without
    -- running into impredicative polymorphism.
    newtype ReifiedNormalizer a = ReifiedNormalizer
      { forall a. ReifiedNormalizer a -> Normalizer a
    getReifiedNormalizer :: Normalizer a }

    -- | Check if an expression is in a normal form given a context of evaluation.
    --   Unlike `isNormalized`, this will fully normalize and traverse through the expression.
    --
    --   It is much more efficient to use `isNormalized`.
    --
    --  `isNormalizedWith` can fail with an `error` if you check an ill-typed
    --  expression
    isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
    isNormalizedWith :: forall s a. (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
    isNormalizedWith Normalizer a
    ctx Expr s a
    e = Expr s a
    e Expr s a -> Expr s a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe (ReifiedNormalizer a) -> Expr s a -> Expr s a
    forall a s t.
    Eq a =>
    Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith (ReifiedNormalizer a -> Maybe (ReifiedNormalizer a)
    forall a. a -> Maybe a
    Just (Normalizer a -> ReifiedNormalizer a
    forall a. Normalizer a -> ReifiedNormalizer a
    ReifiedNormalizer Expr s a -> Identity (Maybe (Expr s a))
    Normalizer a
    ctx)) Expr s a
    e

    -- | Quickly check if an expression is in normal form
    --
    -- Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to
    -- @e == 'normalize' e@.
    --
    -- Given an ill-typed expression, 'isNormalized' may fail with an error, or
    -- evaluate to either False or True!
    isNormalized :: Eq a => Expr s a -> Bool
    isNormalized :: forall a s. Eq a => Expr s a -> Bool
    isNormalized Expr s a
    e0 = Expr (ZonkAny 0) a -> Bool
    forall a s. Eq a => Expr s a -> Bool
    loop (Expr s a -> Expr (ZonkAny 0) a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote Expr s a
    e0)
      where
        loop :: Expr s a -> Bool
    loop Expr s a
    e = case Expr s a
    e of
          Const Const
    _ -> Bool
    True
          Var Var
    _ -> Bool
    True
          Lam Maybe CharacterSet
    _ (FunctionBinding Maybe s
    Nothing Text
    _ Maybe s
    Nothing Maybe s
    Nothing Expr s a
    a) Expr s a
    b -> Expr s a -> Bool
    loop Expr s a
    a Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    b
          Lam Maybe CharacterSet
    _ FunctionBinding s a
    _ Expr s a
    _ -> Bool
    False
          Pi Maybe CharacterSet
    _ Text
    _ Expr s a
    a Expr s a
    b -> Expr s a -> Bool
    loop Expr s a
    a Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    b
          App Expr s a
    f Expr s a
    a -> Expr s a -> Bool
    loop Expr s a
    f Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    a Bool -> Bool -> Bool
    && case Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f Expr s a
    a of
              App (Lam Maybe CharacterSet
    _ FunctionBinding s a
    _ Expr s a
    _) Expr s a
    _ -> Bool
    False
              App (App (App (App Expr s a
    NaturalFold (NaturalLit Natural
    _)) Expr s a
    _) Expr s a
    _) Expr s a
    _ -> Bool
    False
              App Expr s a
    NaturalBuild Expr s a
    _ -> Bool
    False
              App Expr s a
    NaturalIsZero (NaturalLit Natural
    _) -> Bool
    False
              App Expr s a
    NaturalEven (NaturalLit Natural
    _) -> Bool
    False
              App Expr s a
    NaturalOdd (NaturalLit Natural
    _) -> Bool
    False
              App Expr s a
    NaturalShow (NaturalLit Natural
    _) -> Bool
    False
              App Expr s a
    DateShow (DateLiteral Day
    _) -> Bool
    False
              App Expr s a
    TimeShow (TimeLiteral TimeOfDay
    _ Word
    _) -> Bool
    False
              App Expr s a
    TimeZoneShow (TimeZoneLiteral TimeZone
    _) -> Bool
    False
              App (App Expr s a
    NaturalSubtract (NaturalLit Natural
    _)) (NaturalLit Natural
    _) -> Bool
    False
              App (App Expr s a
    NaturalSubtract (NaturalLit Natural
    0)) Expr s a
    _ -> Bool
    False
              App (App Expr s a
    NaturalSubtract Expr s a
    _) (NaturalLit Natural
    0) -> Bool
    False
              App (App Expr s a
    NaturalSubtract Expr s a
    x) Expr s a
    y -> Bool -> Bool
    not (Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    x Expr s a
    y)
              App Expr s a
    NaturalToInteger (NaturalLit Natural
    _) -> Bool
    False
              App Expr s a
    IntegerNegate (IntegerLit Integer
    _) -> Bool
    False
              App Expr s a
    IntegerClamp (IntegerLit Integer
    _) -> Bool
    False
              App Expr s a
    IntegerShow (IntegerLit Integer
    _) -> Bool
    False
              App Expr s a
    IntegerToDouble (IntegerLit Integer
    _) -> Bool
    False
              App Expr s a
    DoubleShow (DoubleLit DhallDouble
    _) -> Bool
    False
              App (App Expr s a
    ListBuild Expr s a
    _) Expr s a
    _ -> Bool
    False
              App (App (App (App (App (App Expr s a
    ListFold Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _)) Expr s a
    _) Expr s a
    _) Expr s a
    _) Expr s a
    _ -> Bool
    False
              App (App Expr s a
    ListLength Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) -> Bool
    False
              App (App Expr s a
    ListHead Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) -> Bool
    False
              App (App Expr s a
    ListLast Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) -> Bool
    False
              App (App Expr s a
    ListIndexed Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) -> Bool
    False
              App (App Expr s a
    ListReverse Expr s a
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) -> Bool
    False
              App Expr s a
    TextShow (TextLit (Chunks [] Text
    _)) ->
                  Bool
    False
              App (App (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    ""))) Expr s a
    _) Expr s a
    _ ->
                  Bool
    False
              App (App (App Expr s a
    TextReplace (TextLit (Chunks [] Text
    _))) Expr s a
    _) (TextLit Chunks s a
    _) ->
                  Bool
    False
              Expr s a
    _ -> Bool
    True
          Let Binding s a
    _ Expr s a
    _ -> Bool
    False
          Annot Expr s a
    _ Expr s a
    _ -> Bool
    False
          Expr s a
    Bool -> Bool
    True
          BoolLit Bool
    _ -> Bool
    True
          BoolAnd Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit Bool
    _)  Expr t a
    _          = Bool
    False
              decide  Expr s a
    _          (BoolLit Bool
    _) = Bool
    False
              decide  Expr s a
    l           Expr t a
    r          = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolOr Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit Bool
    _)  Expr t a
    _          = Bool
    False
              decide  Expr s a
    _          (BoolLit Bool
    _) = Bool
    False
              decide  Expr s a
    l           Expr t a
    r          = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolEQ Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit Bool
    True)  Expr t a
    _             = Bool
    False
              decide  Expr s a
    _             (BoolLit Bool
    True) = Bool
    False
              decide  Expr s a
    l              Expr t a
    r             = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolNE Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit Bool
    False)  Expr t a
    _               = Bool
    False
              decide  Expr s a
    _              (BoolLit Bool
    False ) = Bool
    False
              decide  Expr s a
    l               Expr t a
    r               = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolIf Expr s a
    x Expr s a
    y Expr s a
    z ->
              Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    z Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Expr s a -> Bool
    forall {a} {s} {a} {s} {t}.
    Eq a =>
    Expr s a -> Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y Expr s a
    z
            where
              decide :: Expr s a -> Expr s a -> Expr t a -> Bool
    decide (BoolLit Bool
    _)  Expr s a
    _              Expr t a
    _              = Bool
    False
              decide  Expr s a
    _          (BoolLit Bool
    True) (BoolLit Bool
    False) = Bool
    False
              decide  Expr s a
    _           Expr s a
    l              Expr t a
    r              = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          Expr s a
    Bytes -> Bool
    True
          BytesLit ByteString
    _ -> Bool
    True
          Expr s a
    Natural -> Bool
    True
          NaturalLit Natural
    _ -> Bool
    True
          Expr s a
    NaturalFold -> Bool
    True
          Expr s a
    NaturalBuild -> Bool
    True
          Expr s a
    NaturalIsZero -> Bool
    True
          Expr s a
    NaturalEven -> Bool
    True
          Expr s a
    NaturalOdd -> Bool
    True
          Expr s a
    NaturalShow -> Bool
    True
          Expr s a
    NaturalSubtract -> Bool
    True
          Expr s a
    NaturalToInteger -> Bool
    True
          NaturalPlus Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall {s} {a} {s} {a}. Expr s a -> Expr s a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (NaturalLit Natural
    0)  Expr s a
    _             = Bool
    False
              decide  Expr s a
    _             (NaturalLit Natural
    0) = Bool
    False
              decide (NaturalLit Natural
    _) (NaturalLit Natural
    _) = Bool
    False
              decide  Expr s a
    _              Expr s a
    _             = Bool
    True
          NaturalTimes Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall {s} {a} {s} {a}. Expr s a -> Expr s a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (NaturalLit Natural
    0)  Expr s a
    _             = Bool
    False
              decide  Expr s a
    _             (NaturalLit Natural
    0) = Bool
    False
              decide (NaturalLit Natural
    1)  Expr s a
    _             = Bool
    False
              decide  Expr s a
    _             (NaturalLit Natural
    1) = Bool
    False
              decide (NaturalLit Natural
    _) (NaturalLit Natural
    _) = Bool
    False
              decide  Expr s a
    _              Expr s a
    _             = Bool
    True
          Expr s a
    Integer -> Bool
    True
          IntegerLit Integer
    _ -> Bool
    True
          Expr s a
    IntegerClamp -> Bool
    True
          Expr s a
    IntegerNegate -> Bool
    True
          Expr s a
    IntegerShow -> Bool
    True
          Expr s a
    IntegerToDouble -> Bool
    True
          Expr s a
    Double -> Bool
    True
          DoubleLit DhallDouble
    _ -> Bool
    True
          Expr s a
    DoubleShow -> Bool
    True
          Expr s a
    Text -> Bool
    True
          TextLit (Chunks [(Text
    "", Expr s a
    _)] Text
    "") -> Bool
    False
          TextLit (Chunks [(Text, Expr s a)]
    xys Text
    _) -> ((Text, Expr s a) -> Bool) -> [(Text, Expr s a)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr s a -> Bool) -> (Text, Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    check) [(Text, Expr s a)]
    xys
            where
              check :: Expr s a -> Bool
    check Expr s a
    y = Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && case Expr s a
    y of
                  TextLit Chunks s a
    _ -> Bool
    False
                  Expr s a
    _         -> Bool
    True
          TextAppend Expr s a
    _ Expr s a
    _ -> Bool
    False
          Expr s a
    TextReplace -> Bool
    True
          Expr s a
    TextShow -> Bool
    True
          Expr s a
    Date -> Bool
    True
          DateLiteral Day
    _ -> Bool
    True
          Expr s a
    DateShow -> Bool
    True
          Expr s a
    Time -> Bool
    True
          TimeLiteral TimeOfDay
    _ Word
    _ -> Bool
    True
          Expr s a
    TimeShow -> Bool
    True
          Expr s a
    TimeZone -> Bool
    True
          TimeZoneLiteral TimeZone
    _ -> Bool
    True
          Expr s a
    TimeZoneShow -> Bool
    True
          Expr s a
    List -> Bool
    True
          ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    es -> (Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    loop Maybe (Expr s a)
    t Bool -> Bool -> Bool
    && (Expr s a -> Bool) -> Seq (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    loop Seq (Expr s a)
    es
          ListAppend Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall {s} {a} {s} {a}. Expr s a -> Expr s a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    m)  Expr s a
    _            | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    m = Bool
    False
              decide  Expr s a
    _            (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    n) | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    n = Bool
    False
              decide (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _) (ListLit Maybe (Expr s a)
    _ Seq (Expr s a)
    _)                        = Bool
    False
              decide  Expr s a
    _             Expr s a
    _                                   = Bool
    True
          Expr s a
    ListBuild -> Bool
    True
          Expr s a
    ListFold -> Bool
    True
          Expr s a
    ListLength -> Bool
    True
          Expr s a
    ListHead -> Bool
    True
          Expr s a
    ListLast -> Bool
    True
          Expr s a
    ListIndexed -> Bool
    True
          Expr s a
    ListReverse -> Bool
    True
          Expr s a
    Optional -> Bool
    True
          Some Expr s a
    a -> Expr s a -> Bool
    loop Expr s a
    a
          Expr s a
    None -> Bool
    True
          Record Map Text (RecordField s a)
    kts -> Map Text (RecordField s a) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (RecordField s a)
    kts Bool -> Bool -> Bool
    && (RecordField s a -> Bool) -> Map Text (RecordField s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all RecordField s a -> Bool
    decide Map Text (RecordField s a)
    kts
            where
              decide :: RecordField s a -> Bool
    decide (RecordField Maybe s
    Nothing Expr s a
    exp' Maybe s
    Nothing Maybe s
    Nothing) = Expr s a -> Bool
    loop Expr s a
    exp'
              decide RecordField s a
    _ = Bool
    False
          RecordLit Map Text (RecordField s a)
    kvs -> Map Text (RecordField s a) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (RecordField s a)
    kvs Bool -> Bool -> Bool
    && (RecordField s a -> Bool) -> Map Text (RecordField s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all RecordField s a -> Bool
    decide Map Text (RecordField s a)
    kvs
            where
              decide :: RecordField s a -> Bool
    decide (RecordField Maybe s
    Nothing Expr s a
    exp' Maybe s
    Nothing Maybe s
    Nothing) = Expr s a -> Bool
    loop Expr s a
    exp'
              decide RecordField s a
    _ = Bool
    False
          Union Map Text (Maybe (Expr s a))
    kts -> Map Text (Maybe (Expr s a)) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (Maybe (Expr s a))
    kts Bool -> Bool -> Bool
    && (Maybe (Expr s a) -> Bool) -> Map Text (Maybe (Expr s a)) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    loop) Map Text (Maybe (Expr s a))
    kts
          Combine Maybe CharacterSet
    _ Maybe Text
    _ Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall {s} {a} {s} {a}. Expr s a -> Expr s a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (RecordLit Map Text (RecordField s a)
    m) Expr s a
    _ | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    m = Bool
    False
              decide Expr s a
    _ (RecordLit Map Text (RecordField s a)
    n) | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    n = Bool
    False
              decide (RecordLit Map Text (RecordField s a)
    _) (RecordLit Map Text (RecordField s a)
    _) = Bool
    False
              decide  Expr s a
    _ Expr s a
    _ = Bool
    True
          CombineTypes Maybe CharacterSet
    _ Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall {s} {a} {s} {a}. Expr s a -> Expr s a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (Record Map Text (RecordField s a)
    m) Expr s a
    _ | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    m = Bool
    False
              decide Expr s a
    _ (Record Map Text (RecordField s a)
    n) | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    n = Bool
    False
              decide (Record Map Text (RecordField s a)
    _) (Record Map Text (RecordField s a)
    _) = Bool
    False
              decide  Expr s a
    _ Expr s a
    _ = Bool
    True
          Prefer Maybe CharacterSet
    _ PreferAnnotation
    _ Expr s a
    x Expr s a
    y -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr s a
    x Expr s a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (RecordLit Map Text (RecordField s a)
    m) Expr t a
    _ | Map Text (RecordField s a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField s a)
    m = Bool
    False
              decide Expr s a
    _ (RecordLit Map Text (RecordField t a)
    n) | Map Text (RecordField t a) -> Bool
    forall a. Map Text a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (RecordField t a)
    n = Bool
    False
              decide (RecordLit Map Text (RecordField s a)
    _) (RecordLit Map Text (RecordField t a)
    _) = Bool
    False
              decide Expr s a
    l Expr t a
    r = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          RecordCompletion Expr s a
    _ Expr s a
    _ -> Bool
    False
          Merge Expr s a
    x Expr s a
    y Maybe (Expr s a)
    t -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    y Bool -> Bool -> Bool
    && (Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    loop Maybe (Expr s a)
    t Bool -> Bool -> Bool
    && case Expr s a
    x of
              RecordLit Map Text (RecordField s a)
    _ -> case Expr s a
    y of
                  Field (Union Map Text (Maybe (Expr s a))
    _) FieldSelection s
    _ -> Bool
    False
                  App (Field (Union Map Text (Maybe (Expr s a))
    _) FieldSelection s
    _) Expr s a
    _ -> Bool
    False
                  Some Expr s a
    _ -> Bool
    False
                  App Expr s a
    None Expr s a
    _ -> Bool
    False
                  Expr s a
    _ -> Bool
    True
              Expr s a
    _ -> Bool
    True
          ToMap Expr s a
    x Maybe (Expr s a)
    t -> case Expr s a
    x of
              RecordLit Map Text (RecordField s a)
    _ -> Bool
    False
              Expr s a
    _ -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && (Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    loop Maybe (Expr s a)
    t
          ShowConstructor Expr s a
    x -> Expr s a -> Bool
    loop Expr s a
    x Bool -> Bool -> Bool
    && case Expr s a
    x of
              Field (Union Map Text (Maybe (Expr s a))
    kts) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    k) ->
                  case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    k Map Text (Maybe (Expr s a))
    kts of
                      Just Maybe (Expr s a)
    Nothing -> Bool
    False
                      Maybe (Maybe (Expr s a))
    _            -> Bool
    True
              App (Field (Union Map Text (Maybe (Expr s a))
    kts) (FieldSelection s -> Text
    forall s. FieldSelection s -> Text
    Syntax.fieldSelectionLabel -> Text
    k)) Expr s a
    _ ->
                  case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    k Map Text (Maybe (Expr s a))
    kts of
                      Just (Just Expr s a
    _) -> Bool
    False
                      Maybe (Maybe (Expr s a))
    _             -> Bool
    True
              Some Expr s a
    _ -> Bool
    False
              App Expr s a
    None Expr s a
    _ -> Bool
    False
              Expr s a
    _ -> Bool
    True
          Field Expr s a
    r (FieldSelection Maybe s
    Nothing Text
    k Maybe s
    Nothing) -> case Expr s a
    r of
              RecordLit Map Text (RecordField s a)
    _ -> Bool
    False
              Project Expr s a
    _ Either [Text] (Expr s a)
    _ -> Bool
    False
              Prefer Maybe CharacterSet
    _ PreferAnnotation
    _ (RecordLit Map Text (RecordField s a)
    m) Expr s a
    _ -> Map Text (RecordField s a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (RecordField s a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    r
              Prefer Maybe CharacterSet
    _ PreferAnnotation
    _ Expr s a
    _ (RecordLit Map Text (RecordField s a)
    _) -> Bool
    False
              Combine Maybe CharacterSet
    _ Maybe Text
    _ (RecordLit Map Text (RecordField s a)
    m) Expr s a
    _ -> Map Text (RecordField s a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (RecordField s a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    r
              Combine Maybe CharacterSet
    _ Maybe Text
    _ Expr s a
    _ (RecordLit Map Text (RecordField s a)
    m) -> Map Text (RecordField s a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (RecordField s a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    r
              Expr s a
    _ -> Expr s a -> Bool
    loop Expr s a
    r
          Field Expr s a
    _ FieldSelection s
    _ -> Bool
    False
          Project Expr s a
    r Either [Text] (Expr s a)
    p -> Expr s a -> Bool
    loop Expr s a
    r Bool -> Bool -> Bool
    &&
              case Either [Text] (Expr s a)
    p of
                  Left [Text]
    s -> case Expr s a
    r of
                      RecordLit Map Text (RecordField s a)
    _ -> Bool
    False
                      Project Expr s a
    _ Either [Text] (Expr s a)
    _ -> Bool
    False
                      Prefer Maybe CharacterSet
    _ PreferAnnotation
    _ Expr s a
    _ (RecordLit Map Text (RecordField s a)
    _) -> Bool
    False
                      Expr s a
    _ -> Bool -> Bool
    not ([Text] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Text]
    s) Bool -> Bool -> Bool
    && Set Text -> [Text]
    forall a. Set a -> [a]
    Data.Set.toList ([Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Data.Set.fromList [Text]
    s) [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text]
    s
                  Right Expr s a
    e' -> case Expr s a
    e' of
                      Record Map Text (RecordField s a)
    _ -> Bool
    False
                      Expr s a
    _ -> Expr s a -> Bool
    loop Expr s a
    e'
          Assert Expr s a
    t -> Expr s a -> Bool
    loop Expr s a
    t
          Equivalent Maybe CharacterSet
    _ Expr s a
    l Expr s a
    r -> Expr s a -> Bool
    loop Expr s a
    l Bool -> Bool -> Bool
    && Expr s a -> Bool
    loop Expr s a
    r
          With{} -> Bool
    False
          Note s
    _ Expr s a
    e' -> Expr s a -> Bool
    loop Expr s a
    e'
          ImportAlt Expr s a
    _ Expr s a
    _ -> Bool
    False
          Embed a
    _ -> Bool
    True

    {-| Detect if the given variable is free within the given expression

    >>> "x" `freeIn` "x"
    True
    >>> "x" `freeIn` "y"
    False
    >>> "x" `freeIn` Lam mempty (Syntax.makeFunctionBinding "x" (Const Type)) "x"
    False
    -}
    freeIn :: Eq a => Var -> Expr s a -> Bool
    variable :: Var
    variable@(V Text
    var Int
    i) freeIn :: forall a s. Eq a => Var -> Expr s a -> Bool
    `freeIn` Expr s a
    expression =
        Var -> Expr () a -> Expr () a -> Expr () a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst Var
    variable (Var -> Expr () a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    var (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1))) Expr () a
    strippedExpression
          Expr () a -> Expr () a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Expr () a
    strippedExpression
      where
        denote' :: Expr t b -> Expr () b
        denote' :: forall t b. Expr t b -> Expr () b
    denote' = Expr t b -> Expr () b
    forall s a t. Expr s a -> Expr t a
    Syntax.denote

        strippedExpression :: Expr () a
    strippedExpression = Expr s a -> Expr () a
    forall t b. Expr t b -> Expr () b
    denote' Expr s a
    expression
    {-# INLINABLE freeIn #-}

    {- $setup
    >>> import Dhall.Syntax (Const(..))
    -}