{-# 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.Family   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 = 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) = 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) =
    forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam Maybe CharacterSet
cs (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' = 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'  = forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst (Text -> Int -> Var
V Text
x Int
n') (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 forall a. Eq a => a -> a -> Bool
== Text
y then Int
n 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) = 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' = 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' = forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst (Text -> Int -> Var
V Text
x Int
n') (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 forall a. Eq a => a -> a -> Bool
== Text
y then Int
n 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 forall a. Eq a => a -> a -> Bool
== Var
v' then Expr s a
e else 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) =
    forall s a. Binding s a -> Expr s a -> Expr s a
Let (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' = forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst (Text -> Int -> Var
V Text
x Int
n') (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 forall a. Eq a => a -> a -> Bool
== Text
f then Int
n forall a. Num a => a -> a -> a
+ Int
1 else Int
n

    mt' :: Maybe (Maybe s, Expr s a)
mt' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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'  =             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 = forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.over forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
Syntax.subExpressions (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) = forall s a. Expr s a -> Bool
boundedType Expr s a
t
boundedType (Record Map Text (RecordField s a)
kvs)     = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall s a. Expr s a -> Bool
boundedType forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)      = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all 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 = 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 = 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 = forall a. Identity a -> a
runIdentity (forall (m :: * -> *) a s t.
(Monad m, Eq a) =>
NormalizerM m a -> Expr s a -> m (Expr t a)
normalizeWithM (forall a. ReifiedNormalizer a -> Normalizer a
getReifiedNormalizer ReifiedNormalizer a
ctx) Expr s a
t)
normalizeWith Maybe (ReifiedNormalizer a)
_          Expr s a
t = 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 = forall {s}. Expr s a -> m (Expr s a)
loop (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 = NormalizerM m a
ctx Expr s a
e 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Const -> Expr s a
Const Const
k)
          Var Var
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 ->
              forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam Maybe CharacterSet
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall s a. Text -> Expr s a -> FunctionBinding s a
Syntax.makeFunctionBinding Text
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
_A') 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 -> forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
cs Text
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
_A' 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
              Expr s a
f' <- Expr s a -> m (Expr s a)
loop Expr s a
f
              Expr s a
a' <- Expr s a -> m (Expr s a)
loop Expr s a
a
              case Expr s a
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₂ = 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₁ = 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₂ = 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 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
                      Expr s a
t' <- Expr s a -> m (Expr s a)
loop Expr s a
t
                      if forall s a. Expr s a -> Bool
boundedType Expr s a
t' then m (Expr s a)
strict else m (Expr s a)
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 =       forall {t}. (Eq t, Num t) => t -> m (Expr s a)
strictLoop (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 (  forall {t}. (Eq t, Num t) => t -> Expr s a
lazyLoop (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n0 :: Integer))

                        strictLoop :: t -> m (Expr s a)
strictLoop t
0 = Expr s a -> m (Expr s a)
loop Expr s a
zero
                        strictLoop !t
n = forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
succ' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> m (Expr s a)
strictLoop (t
n forall a. Num a => a -> a -> a
- t
1) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr s a -> m (Expr s a)
loop

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

                        zero :: Expr s a
zero = forall s a. Natural -> Expr s a
NaturalLit Natural
0
                    App Expr s a
NaturalIsZero (NaturalLit Natural
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Bool -> Expr s a
BoolLit (Natural
n forall a. Eq a => a -> a -> Bool
== Natural
0))
                    App Expr s a
NaturalEven (NaturalLit Natural
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Bool -> Expr s a
BoolLit (forall a. Integral a => a -> Bool
even Natural
n))
                    App Expr s a
NaturalOdd (NaturalLit Natural
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Bool -> Expr s a
BoolLit (forall a. Integral a => a -> Bool
odd Natural
n))
                    App Expr s a
NaturalToInteger (NaturalLit Natural
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Integer -> Expr s a
IntegerLit (forall a. Integral a => a -> Integer
toInteger Natural
n))
                    App Expr s a
NaturalShow (NaturalLit Natural
n) ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] (String -> Text
Text.pack (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 forall a. Ord a => a -> a -> Bool
>= Natural
x ->
                            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Num a => a -> a -> a
subtract (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
x :: Integer) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
y :: Integer))))
                        | Bool
otherwise ->
                            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
0)
                    App (App Expr s a
NaturalSubtract (NaturalLit Natural
0)) Expr s a
y -> 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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
0)
                    App (App Expr s a
NaturalSubtract Expr s a
x) Expr s a
y | forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
x Expr s a
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
0)
                    App Expr s a
IntegerClamp (IntegerLit Integer
n)
                        | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit (forall a. Num a => Integer -> a
fromInteger Integer
n))
                        | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
0)
                    App Expr s a
IntegerNegate (IntegerLit Integer
n) ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Integer -> Expr s a
IntegerLit (forall a. Num a => a -> a
negate Integer
n))
                    App Expr s a
IntegerShow (IntegerLit Integer
n)
                        | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
n    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] (Text
"+" forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (forall a. Show a => a -> String
show Integer
n))))
                        | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] (String -> Text
Text.pack (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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. DhallDouble -> Expr s a
DoubleLit ((Double -> DhallDouble
DhallDouble forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Read a => String -> a
read forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Integer
n))
                    App Expr s a
DoubleShow (DoubleLit (DhallDouble Double
n)) ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] (String -> Text
Text.pack (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 (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App (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₁ = 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 = forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
List Expr s a
_A₀

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

                        nil :: Expr s a
nil = forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit (forall a. a -> Maybe a
Just (forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
List Expr s a
_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
                      Expr s a
t' <- Expr s a -> m (Expr s a)
loop Expr s a
t
                      if forall s a. Expr s a -> Bool
boundedType Expr s a
t' then m (Expr s a)
strict else m (Expr s a)
lazy
                      where
                        strict :: m (Expr s a)
strict =       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 (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 =
                          forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
cons Expr s a
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
ys 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 =       forall s a. Expr s a -> Expr s a -> Expr s a
App (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) ->
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 forall a. Seq a -> ViewL a
Data.Sequence.viewl Seq (Expr s a)
ys of
                                Expr s a
y :< Seq (Expr s a)
_ -> forall s a. Expr s a -> Expr s a
Some Expr s a
y
                                ViewL (Expr s a)
_      -> forall s a. Expr s a -> Expr s a -> Expr s a
App 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 forall a. Seq a -> ViewR a
Data.Sequence.viewr Seq (Expr s a)
ys of
                                Seq (Expr s a)
_ :> Expr s a
y -> forall s a. Expr s a -> Expr s a
Some Expr s a
y
                                ViewR (Expr s a)
_      -> forall s a. Expr s a -> Expr s a -> Expr s a
App 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 (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₁ = forall a b. (Int -> a -> b) -> Seq a -> Seq b
Data.Sequence.mapWithIndex forall {p} {s} {a}. Integral p => p -> Expr s a -> Expr s a
adapt Seq (Expr s a)
as₀

                        _A₂ :: Expr s a
_A₂ = forall s a. Map Text (RecordField s a) -> Expr s a
Record (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", forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField forall s a. Expr s a
Natural)
                                  , (Text
"value", forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
_A₀)
                                  ]

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

                        adapt :: p -> Expr s a -> Expr s a
adapt p
n Expr s a
a_ =
                            forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (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", forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField forall a b. (a -> b) -> a -> b
$ forall s a. Natural -> Expr s a
NaturalLit (forall a b. (Integral a, Num b) => a -> b
fromIntegral p
n))
                                  , (Text
"value", 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 (forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit Maybe (Expr s a)
t (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 (forall s a. Chunks s a -> Expr s a
TextLit (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 ->
                            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
                                    (Text
x, Expr s a
y) <- [(Text, Expr s a)]
xys

                                    let x' :: Text
x' = Text -> Text -> Text -> Text
Text.replace Text
needleText Text
replacementText Text
x
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (Text
x', Expr s a
y)

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

                            forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Chunks s a -> Expr s a
TextLit (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) =
                                    Text -> Text -> (Text, Text)
Text.breakOn Text
needleText Text
lastText

                            if Text -> Bool
Text.null Text
suffix
                                then forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Chunks s a -> Expr s a
TextLit (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 (forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
prefix, Expr s a
replacement)] Text
"")) (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
TextReplace (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
needleText))) Expr s a
replacement) (forall s a. Chunks s a -> Expr s a
TextLit (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) =
                                    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 (forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
firstText, Expr s a
firstInterpolation)] Text
"")) (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
TextReplace (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
needleText))) Expr s a
replacement) (forall s a. Chunks s a -> Expr s a
TextLit (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 (forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
prefix, Expr s a
replacement)] Text
"")) (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App (forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
TextReplace (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
needleText))) Expr s a
replacement) (forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks ((Text
remainder, Expr s a
firstInterpolation) 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 (forall s a. Chunks s a -> Expr s a
TextLit (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 (forall s a. Chunks s a -> Expr s a
TextLit (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 (forall s a. Chunks s a -> Expr s a
TextLit (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
                        Maybe (Expr s a)
res2 <- NormalizerM m a
ctx (forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
f' Expr s a
a')
                        case Maybe (Expr s a)
res2 of
                            Maybe (Expr s a)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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'  = 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'  = 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'' = 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Bool
          BoolLit Bool
b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Bool -> Expr s a
BoolLit Bool
b)
          BoolAnd Expr s a
x Expr s a
y -> forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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
_              = 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) = forall s a. Bool -> Expr s a
BoolLit Bool
False
              decide  Expr t a
l               Expr t a
r
                  | 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                  = 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 -> forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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
_              = 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 ) = forall s a. Bool -> Expr s a
BoolLit Bool
True
              decide  Expr t a
l               Expr t a
r
                  | 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                  = 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 -> forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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
                  | forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr t a
l Expr t a
r = forall s a. Bool -> Expr s a
BoolLit Bool
True
                  | Bool
otherwise                  = 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 -> forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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
                  | forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr t a
l Expr t a
r = forall s a. Bool -> Expr s a
BoolLit Bool
False
                  | Bool
otherwise                  = 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 -> forall {a} {t}.
Eq a =>
Expr t a -> Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
bool 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 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
                  | 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                  = 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Bytes
          BytesLit ByteString
b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. ByteString -> Expr s a
BytesLit ByteString
b)
          Expr s a
Natural -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Natural
          NaturalLit Natural
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
n)
          Expr s a
NaturalFold -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalFold
          Expr s a
NaturalBuild -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalBuild
          Expr s a
NaturalIsZero -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalIsZero
          Expr s a
NaturalEven -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalEven
          Expr s a
NaturalOdd -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalOdd
          Expr s a
NaturalToInteger -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalToInteger
          Expr s a
NaturalShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalShow
          Expr s a
NaturalSubtract -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalSubtract
          NaturalPlus Expr s a
x Expr s a
y -> forall s a. Expr s a -> Expr s a -> Expr s a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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) = forall s a. Natural -> Expr s a
NaturalLit (Natural
m forall a. Num a => a -> a -> a
+ Natural
n)
              decide  Expr s a
l              Expr s a
r             = 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 -> forall s a. Expr s a -> Expr s a -> Expr s a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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
_             = forall s a. Natural -> Expr s a
NaturalLit Natural
0
              decide  Expr s a
_             (NaturalLit Natural
0) = forall s a. Natural -> Expr s a
NaturalLit Natural
0
              decide (NaturalLit Natural
m) (NaturalLit Natural
n) = forall s a. Natural -> Expr s a
NaturalLit (Natural
m forall a. Num a => a -> a -> a
* Natural
n)
              decide  Expr s a
l              Expr s a
r             = 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Integer
          IntegerLit Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Integer -> Expr s a
IntegerLit Integer
n)
          Expr s a
IntegerClamp -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerClamp
          Expr s a
IntegerNegate -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerNegate
          Expr s a
IntegerShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerShow
          Expr s a
IntegerToDouble -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerToDouble
          Expr s a
Double -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Double
          DoubleLit DhallDouble
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n)
          Expr s a
DoubleShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
DoubleShow
          Expr s a
Text -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Text
          TextLit (Chunks [(Text, Expr s a)]
xys Text
z) -> do
              Chunks s a
chunks' <- forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Chunks s a]
chunks
              case Chunks s a
chunks' of
                  Chunks [(Text
"", Expr s a
x)] Text
"" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
x
                  Chunks s a
c                   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Chunks s a -> Expr s a
TextLit Chunks s a
c)
            where
              chunks :: m [Chunks s a]
chunks =
                ((forall a. [a] -> [a] -> [a]
++ [forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
z]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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
                Expr s a
y' <- Expr s a -> m (Expr s a)
loop Expr s a
y
                case Expr s a
y' of
                  TextLit Chunks s a
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
x, Chunks s a
c]
                  Expr s a
_         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
x, Expr s a
y')] forall a. Monoid a => a
mempty]
          TextAppend Expr s a
x Expr s a
y -> Expr s a -> m (Expr s a)
loop (forall s a. Chunks s a -> Expr s a
TextLit (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TextReplace
          Expr s a
TextShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TextShow
          Expr s a
Date -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Date
          DateLiteral Day
d -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Day -> Expr s a
DateLiteral Day
d)
          Expr s a
DateShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
DateShow
          Expr s a
Time -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Time
          TimeLiteral TimeOfDay
t Word
p -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. TimeOfDay -> Word -> Expr s a
TimeLiteral TimeOfDay
t Word
p)
          Expr s a
TimeShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeShow
          Expr s a
TimeZone -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeZone
          TimeZoneLiteral TimeZone
z -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. TimeZone -> Expr s a
TimeZoneLiteral TimeZone
z)
          Expr s a
TimeZoneShow -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeZoneShow
          Expr s a
List -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
List
          ListLit Maybe (Expr s a)
t Seq (Expr s a)
es
              | forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
es -> forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Seq a
Data.Sequence.empty
              | Bool
otherwise             -> forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit forall a. Maybe a
Nothing 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'  = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop Maybe (Expr s a)
t
              es' :: m (Seq (Expr s a))
es' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop Seq (Expr s a)
es
          ListAppend Expr s a
x Expr s a
y -> forall s a. Expr s a -> Expr s a -> Expr s a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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            | 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) | 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)                        = 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 forall a. Semigroup a => a -> a -> a
<> Seq (Expr s a)
n)
              decide  Expr s a
l             Expr s a
r                                   = 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListBuild
          Expr s a
ListFold -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListFold
          Expr s a
ListLength -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListLength
          Expr s a
ListHead -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListHead
          Expr s a
ListLast -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListLast
          Expr s a
ListIndexed -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListIndexed
          Expr s a
ListReverse -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListReverse
          Expr s a
Optional -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Optional
          Some Expr s a
a -> forall s a. Expr s a -> Expr s a
Some 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
None
          Record Map Text (RecordField s a)
kts -> forall s a. Map Text (RecordField s a) -> Expr s a
Record forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Map k v -> Map k v
Dhall.Map.sort 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' -> 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) 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse RecordField s a -> m (RecordField s a)
f Map Text (RecordField s a)
kts
          RecordLit Map Text (RecordField s a)
kvs -> forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Map k v -> Map k v
Dhall.Map.sort 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' -> 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) 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse RecordField s a -> m (RecordField s a)
f Map Text (RecordField s a)
kvs
          Union Map Text (Maybe (Expr s a))
kts -> forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Map k v -> Map k v
Dhall.Map.sort 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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 -> forall s a. Expr s a -> Expr s a -> Expr s a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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 | 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) | 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) =
                  forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (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
_) =
                    forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField 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 =
                  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 -> forall s a. Expr s a -> Expr s a -> Expr s a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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 | 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) | 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) =
                  forall s a. Map Text (RecordField s a) -> Expr s a
Record (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
_) =
                    forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField 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 =
                  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 -> forall {a} {t}. Eq a => Expr t a -> Expr t a -> Expr t a
decide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x 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 | 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) | 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) =
                  forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (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 | 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 =
                  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 (forall s a. Expr s a -> Expr s a -> Expr s a
Annot (forall s a.
Maybe CharacterSet
-> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
Prefer forall a. Monoid a => a
mempty PreferAnnotation
PreferFromCompletion (forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr s a
x forall {s}. FieldSelection s
def) Expr s a
y) (forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr s a
x forall {s}. FieldSelection s
typ))
            where
              def :: FieldSelection s
def = forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"default"
              typ :: FieldSelection s
typ = forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"Type"
          Merge Expr s a
x Expr s a
y Maybe (Expr s a)
t      -> do
              Expr s a
x' <- Expr s a -> m (Expr s a)
loop Expr s a
x
              Expr s a
y' <- Expr s a -> m (Expr s a)
loop Expr s a
y
              case Expr s a
x' of
                  RecordLit Map Text (RecordField s a)
kvsX ->
                      case Expr s a
y' of
                          Field (Union Map Text (Maybe (Expr s a))
ktsY) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY) ->
                              case 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 forall s a. RecordField s a -> Expr s a
recordFieldValue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                                          Maybe (Expr s a)
Nothing -> 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' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                                  Maybe (Maybe (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' 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) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY)) Expr s a
vY ->
                              case 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 forall s a. RecordField s a -> Expr s a
recordFieldValue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (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 -> 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' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                                  Maybe (Maybe (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' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                          Some Expr s a
a ->
                              case forall s a. RecordField s a -> Expr s a
recordFieldValue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (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 -> 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' 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 forall s a. RecordField s a -> Expr s a
recordFieldValue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                                  Maybe (Expr s a)
Nothing -> 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' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                          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' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                  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' 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' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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
              Expr s a
x' <- Expr s a -> m (Expr s a)
loop Expr s a
x
              Maybe (Expr s a)
t' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop Maybe (Expr s a)
t
              case Expr s a
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) =
                              forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit
                                  (forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList
                                      [ (Text
"mapKey"  , forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField forall a b. (a -> b) -> a -> b
$ forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
key))
                                      , (Text
"mapValue", forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
value                  )
                                      ]
                                  )

                      let keyValues :: Seq (Expr s a)
keyValues = forall a. [a] -> Seq a
Data.Sequence.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall {s} {a}. (Text, Expr s a) -> Expr s a
entry (forall k v. Ord k => Map k v -> [(k, v)]
Dhall.Map.toList forall a b. (a -> b) -> a -> b
$ forall s a. RecordField s a -> Expr s a
recordFieldValue 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
_ | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Expr s a)
keyValues ->
                                  Maybe (Expr s a)
t'
                              Maybe (Expr s a)
_ ->
                                  forall a. Maybe a
Nothing

                      forall (m :: * -> *) a. Monad m => a -> m a
return (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
_ ->
                      forall (m :: * -> *) a. Monad m => a -> m a
return (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
              Expr s a
x' <- Expr s a -> m (Expr s a)
loop Expr s a
x
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Expr s a
x' of
                  Field (Union Map Text (Maybe (Expr s a))
ktsY) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY) ->
                      case 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 -> forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
kY)
                          Maybe (Maybe (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) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY)) Expr s a
_ ->
                      case 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
_) -> forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
kY)
                          Maybe (Maybe (Expr s a))
_ -> forall s a. Expr s a -> Expr s a
ShowConstructor Expr s a
x'
                  Some Expr s a
_ ->
                      forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
"Some")
                  App Expr s a
None Expr s a
_ ->
                      forall s a. Chunks s a -> Expr s a
TextLit (forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
"None")
                  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 = forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (forall k v. k -> v -> Map k v
Dhall.Map.singleton Text
x RecordField s a
v)

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

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

              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Expr s a -> Expr s a
Assert Expr s a
t')
          Equivalent Maybe CharacterSet
cs Expr s a
l Expr s a
r -> do
              Expr s a
l' <- Expr s a -> m (Expr s a)
loop Expr s a
l
              Expr s a
r' <- Expr s a -> m (Expr s a)
loop Expr s a
r

              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
Equivalent Maybe CharacterSet
cs Expr s a
l' Expr s a
r')
          With Expr s a
r NonEmpty WithComponent
ks Expr s a
v -> do
              Expr s a
r' <- Expr s a -> m (Expr s a)
loop Expr s a
r
              Expr s a
v' <- Expr s a -> m (Expr s a)
loop Expr s a
v

              case Expr s a
r' of
                  RecordLit Map Text (RecordField s a)
kvs ->
                      case NonEmpty WithComponent
ks of
                          WithLabel Text
k :| [] ->
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (forall k v. Ord k => k -> v -> Map k v -> Map k v
Dhall.Map.insert Text
k (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 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  -> forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit forall a. Monoid a => a
mempty
                                          Just RecordField s a
val -> forall s a. RecordField s a -> Expr s a
Syntax.recordFieldValue RecordField s a
val

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

                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (forall k v. Ord k => k -> v -> Map k v -> Map k v
Dhall.Map.insert Text
k₀ (forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
e₂) Map Text (RecordField s a)
kvs))
                          WithComponent
WithQuestion :| [WithComponent]
_ -> do
                              forall (m :: * -> *) a. Monad m => a -> m a
return (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
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Expr s a -> Expr s a
Some Expr s a
v')
                          WithComponent
WithQuestion :| WithComponent
k : [WithComponent]
ks' -> do
                              Expr s a
w <- Expr s a -> m (Expr s a)
loop (forall s a.
Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
With Expr s a
t (WithComponent
k forall a. a -> [a] -> NonEmpty a
:| [WithComponent]
ks') Expr s a
v)
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Expr s a -> Expr s a
Some Expr s a
w)
                          WithLabel Text
_ :| [WithComponent]
_ ->
                              forall (m :: * -> *) a. Monad m => a -> m a
return (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]
_ ->
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall s a. Expr s a -> Expr s a -> Expr s a
App forall s a. Expr s a
None Expr s a
_T)
                          WithLabel Text
_ :| [WithComponent]
_ ->
                              forall (m :: * -> *) a. Monad m => a -> m a
return (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
_ ->
                      forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 forall a. Eq a => a -> a -> Bool
== forall a s t.
Eq a =>
Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
normalizeWith (forall a. a -> Maybe a
Just (forall a. Normalizer a -> ReifiedNormalizer a
ReifiedNormalizer 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 = forall a s. Eq a => Expr s a -> Bool
loop (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 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 (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
&& 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 (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
&& 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 (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
&& 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 (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
&& 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 (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
&& 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 (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
&& 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
&& 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
_) -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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 -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr s a -> Bool
loop Maybe (Expr s a)
t Bool -> Bool -> 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
&& 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
_            | 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) | 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 -> forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (RecordField s a)
kts Bool -> Bool -> 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 -> forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (RecordField s a)
kvs Bool -> Bool -> 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 -> forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (Maybe (Expr s a))
kts Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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
&& 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
_ | 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) | 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
&& 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
_ | 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) | 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
&& 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
_ | 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) | 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 (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
&& 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
&& 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) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
k) ->
              case 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) (forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
k)) Expr s a
_ ->
              case 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
_ -> forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField s a)
m 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
_ -> forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField s a)
m 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) -> forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField s a)
m 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
s) Bool -> Bool -> Bool
&& forall a. Set a -> [a]
Data.Set.toList (forall a. Ord a => [a] -> Set a
Data.Set.fromList [Text]
s) 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 =
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst Var
variable (forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
var (Int
i forall a. Num a => a -> a -> a
+ Int
1))) Expr () a
strippedExpression
      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' = forall s a t. Expr s a -> Expr t a
Syntax.denote

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

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