{-# 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 (..)
    )

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 :: Expr s a -> Expr t a -> Bool
judgmentallyEqual = Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual
{-# INLINE judgmentallyEqual #-}

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

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

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

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

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

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

>>> mfb = Syntax.makeFunctionBinding
>>> alphaNormalize (Lam (mfb "a" (Const Type)) (Lam (mfb "b" (Const Type)) (Lam (mfb "x" "a") (Lam (mfb "y" "b") "x"))))
Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam (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 :: Expr s a -> Expr s a
alphaNormalize = Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Eval.alphaNormalize
{-# INLINE alphaNormalize #-}

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

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

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

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

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

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

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

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

{-| 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 :: NormalizerM m a -> Expr s a -> m (Expr t a)
normalizeWithM NormalizerM m a
ctx Expr s a
e0 = Expr t a -> m (Expr t a)
forall s. Expr s a -> m (Expr s a)
loop (Expr s a -> Expr t a
forall s a t. Expr s a -> Expr t a
Syntax.denote Expr s a
e0)
 where
 loop :: Expr s a -> m (Expr s a)
loop =  \case
    Const Const
k -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
k)
    Var Var
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var -> Expr s a
forall s a. Var -> Expr s a
Var Var
v)
    Lam (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 ->
        FunctionBinding s a -> Expr s a -> Expr s a
forall s a. FunctionBinding s a -> Expr s a -> Expr s a
Lam (FunctionBinding s a -> Expr s a -> Expr s a)
-> m (FunctionBinding s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Expr s a -> FunctionBinding s a
forall s a. Text -> Expr s a -> FunctionBinding s a
Syntax.makeFunctionBinding Text
x (Expr s a -> FunctionBinding s a)
-> m (Expr s a) -> m (FunctionBinding s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
_A') m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 Text
x Expr s a
_A Expr s a
_B -> Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi Text
x (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
_A' m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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
      Maybe (Expr s a)
res <- Expr s a -> m (Maybe (Expr s a))
NormalizerM m a
ctx (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
f Expr s a
a)
      case Maybe (Expr s a)
res of
          Just Expr s a
e1 -> Expr s a -> m (Expr s a)
loop Expr s a
e1
          Maybe (Expr s a)
Nothing -> 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 (FunctionBinding Maybe s
_ Text
x Maybe s
_ Maybe s
_ Expr s a
_A) Expr s a
b₀ -> do

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

                    Expr s a -> m (Expr s a)
loop Expr s a
b₂
                Expr s a
_ ->
                  case Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
f' Expr s a
a' of
                    App (App (App (App Expr s a
NaturalFold (NaturalLit Natural
n0)) Expr s a
t) Expr s a
succ') Expr s a
zero -> do
                      Expr s a
t' <- Expr s a -> m (Expr s a)
loop Expr s a
t
                      if Expr s a -> Bool
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 =       Integer -> m (Expr s a)
forall t. (Eq t, Num t) => t -> m (Expr s a)
strictLoop (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n0 :: Integer)
                        lazy :: m (Expr s a)
lazy   = Expr s a -> m (Expr s a)
loop (  Integer -> Expr s a
forall t. (Eq t, Num t) => t -> Expr s a
lazyLoop (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n0 :: Integer))

                        strictLoop :: t -> m (Expr s a)
strictLoop t
0 = Expr s a -> m (Expr s a)
loop Expr s a
zero
                        strictLoop !t
n = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
succ' (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> m (Expr s a)
strictLoop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) m (Expr s a) -> (Expr s a -> m (Expr s a)) -> m (Expr s a)
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 = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
succ' (t -> Expr s a
lazyLoop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1))
                    App Expr s a
NaturalBuild Expr s a
g -> Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
g Expr s a
forall s a. Expr s a
Natural) Expr s a
forall s a. Expr s a
succ) Expr s a
forall s a. Expr s a
zero)
                      where
                        succ :: Expr s a
succ = FunctionBinding s a -> Expr s a -> Expr s a
forall s a. FunctionBinding s a -> Expr s a -> Expr s a
Lam (Text -> Expr s a -> FunctionBinding s a
forall s a. Text -> Expr s a -> FunctionBinding s a
Syntax.makeFunctionBinding Text
"n" Expr s a
forall s a. Expr s a
Natural) (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
NaturalPlus Expr s a
"n" (Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
1))

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

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

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

                        nil :: Expr s a
nil = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit (Expr s a -> Maybe (Expr s a)
forall a. a -> Maybe a
Just (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
forall s a. Expr s a
List Expr s a
_A₀)) Seq (Expr s a)
forall (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 Expr s a -> Bool
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 =       (Expr s a -> m (Expr s a) -> m (Expr s a))
-> m (Expr s a) -> Seq (Expr s a) -> m (Expr s a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr s a -> m (Expr s a) -> m (Expr s a)
strictCons m (Expr s a)
strictNil Seq (Expr s a)
xs
                        lazy :: m (Expr s a)
lazy   = Expr s a -> m (Expr s a)
loop ((Expr s a -> Expr s a -> Expr s a)
-> Expr s a -> Seq (Expr s a) -> Expr s a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr   Expr s a -> Expr s a -> Expr s a
lazyCons   Expr s a
lazyNil Seq (Expr s a)
xs)

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

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

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

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

                        adapt :: a -> Expr s a -> Expr s a
adapt a
n Expr s a
a_ =
                            Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit ([(Text, RecordField s a)] -> Map Text (RecordField s a)
forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList [(Text, RecordField s a)]
kvs)
                          where
                            kvs :: [(Text, RecordField s a)]
kvs = [ (Text
"index", Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
forall a b. (a -> b) -> a -> b
$ Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit (a -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n))
                                  , (Text
"value", Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
a_)
                                  ]
                    App (App Expr s a
ListReverse Expr s a
_) (ListLit Maybe (Expr s a)
t Seq (Expr s a)
xs) ->
                        Expr s a -> m (Expr s a)
loop (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit Maybe (Expr s a)
t (Seq (Expr s a) -> Seq (Expr s a)
forall a. Seq a -> Seq a
Data.Sequence.reverse Seq (Expr s a)
xs))
                    App Expr s a
TextShow (TextLit (Chunks [] Text
oldText)) ->
                        Expr s a -> m (Expr s a)
loop (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
newText))
                      where
                        newText :: Text
newText = Text -> Text
Eval.textShow Text
oldText
                    App
                        (App (App Expr s a
TextReplace (TextLit (Chunks [] Text
""))) Expr s a
_)
                        Expr s a
haystack ->
                            Expr s a -> m (Expr s a)
forall (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
                                    (Text, Expr s a) -> [(Text, Expr s a)]
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

                            Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text, Expr s a)]
xys' Text
z'))
                    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 Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
lastText))
                                else do
                                    let remainder :: Text
remainder =
                                            Int -> Text -> Text
Text.drop
                                                (Text -> Int
Text.length Text
needleText)
                                                Text
suffix

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

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

                                    Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
prefix, Expr s a
replacement)] Text
"")) (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
forall s a. Expr s a
TextReplace (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
needleText))) Expr s a
replacement) (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks ((Text
remainder, Expr s a
firstInterpolation) (Text, Expr s a) -> [(Text, Expr s a)] -> [(Text, Expr s a)]
forall a. a -> [a] -> [a]
: [(Text, Expr s a)]
chunks) Text
lastText))))
                    Expr s a
_ -> do
                        Maybe (Expr s a)
res2 <- Expr s a -> m (Maybe (Expr s a))
NormalizerM m a
ctx (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
f' Expr s a
a')
                        case Maybe (Expr s a)
res2 of
                            Maybe (Expr s a)
Nothing -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
f' Expr s a
a')
                            Just Expr s a
app' -> Expr s a -> m (Expr s a)
loop Expr s a
app'
    Let (Binding Maybe s
_ Text
f Maybe s
_ Maybe (Maybe s, Expr s a)
_ Maybe s
_ Expr s a
r) Expr s a
b -> Expr s a -> m (Expr s a)
loop Expr s a
b''
      where
        r' :: Expr s a
r'  = Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
Syntax.shift   Int
1  (Text -> Int -> Var
V Text
f Int
0) Expr s a
r
        b' :: Expr s a
b'  = Var -> Expr s a -> Expr s a -> Expr s a
forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst (Text -> Int -> Var
V Text
f Int
0) Expr s a
r' Expr s a
b
        b'' :: Expr s a
b'' = Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
Syntax.shift (-Int
1) (Text -> Int -> Var
V Text
f Int
0) Expr s a
b'
    Annot Expr s a
x Expr s a
_ -> Expr s a -> m (Expr s a)
loop Expr s a
x
    Expr s a
Bool -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Bool
    BoolLit Bool
b -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
b)
    BoolAnd Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 (BoolLit Bool
True )  Expr s a
r              = Expr s a
r
        decide (BoolLit Bool
False)  Expr s a
_              = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
        decide  Expr s a
l              (BoolLit Bool
True ) = Expr s a
l
        decide  Expr s a
_              (BoolLit Bool
False) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
        decide  Expr s a
l               Expr s a
r
            | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r = Expr s a
l
            | Bool
otherwise                  = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolAnd Expr s a
l Expr s a
r
    BoolOr Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 (BoolLit Bool
False)  Expr s a
r              = Expr s a
r
        decide (BoolLit Bool
True )  Expr s a
_              = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
        decide  Expr s a
l              (BoolLit Bool
False) = Expr s a
l
        decide  Expr s a
_              (BoolLit Bool
True ) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
        decide  Expr s a
l               Expr s a
r
            | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r = Expr s a
l
            | Bool
otherwise                  = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolOr Expr s a
l Expr s a
r
    BoolEQ Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 (BoolLit Bool
True )  Expr s a
r              = Expr s a
r
        decide  Expr s a
l              (BoolLit Bool
True ) = Expr s a
l
        decide  Expr s a
l               Expr s a
r
            | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
            | Bool
otherwise                  = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolEQ Expr s a
l Expr s a
r
    BoolNE Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 (BoolLit Bool
False)  Expr s a
r              = Expr s a
r
        decide  Expr s a
l              (BoolLit Bool
False) = Expr s a
l
        decide  Expr s a
l               Expr s a
r
            | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
            | Bool
otherwise                  = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolNE Expr s a
l Expr s a
r
    BoolIf Expr s a
bool Expr s a
true Expr s a
false -> Expr s a -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
bool m (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
true m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (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 s a -> Expr s a -> Expr s a -> Expr s a
decide (BoolLit Bool
True )  Expr s a
l              Expr s a
_              = Expr s a
l
        decide (BoolLit Bool
False)  Expr s a
_              Expr s a
r              = Expr s a
r
        decide  Expr s a
b              (BoolLit Bool
True) (BoolLit Bool
False) = Expr s a
b
        decide  Expr s a
b               Expr s a
l              Expr s a
r
            | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r = Expr s a
l
            | Bool
otherwise                  = Expr s a -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
BoolIf Expr s a
b Expr s a
l Expr s a
r
    Expr s a
Natural -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Natural
    NaturalLit Natural
n -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
n)
    Expr s a
NaturalFold -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalFold
    Expr s a
NaturalBuild -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalBuild
    Expr s a
NaturalIsZero -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalIsZero
    Expr s a
NaturalEven -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalEven
    Expr s a
NaturalOdd -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalOdd
    Expr s a
NaturalToInteger -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalToInteger
    Expr s a
NaturalShow -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalShow
    Expr s a
NaturalSubtract -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
NaturalSubtract
    NaturalPlus Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (NaturalLit Natural
0)  Expr s a
r             = Expr s a
r
        decide  Expr s a
l             (NaturalLit Natural
0) = Expr s a
l
        decide (NaturalLit Natural
m) (NaturalLit Natural
n) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n)
        decide  Expr s a
l              Expr s a
r             = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
NaturalPlus Expr s a
l Expr s a
r
    NaturalTimes Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (NaturalLit Natural
1)  Expr s a
r             = Expr s a
r
        decide  Expr s a
l             (NaturalLit Natural
1) = Expr s a
l
        decide (NaturalLit Natural
0)  Expr s a
_             = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
0
        decide  Expr s a
_             (NaturalLit Natural
0) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
0
        decide (NaturalLit Natural
m) (NaturalLit Natural
n) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
n)
        decide  Expr s a
l              Expr s a
r             = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
NaturalTimes Expr s a
l Expr s a
r
    Expr s a
Integer -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Integer
    IntegerLit Integer
n -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Expr s a
forall s a. Integer -> Expr s a
IntegerLit Integer
n)
    Expr s a
IntegerClamp -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
IntegerClamp
    Expr s a
IntegerNegate -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
IntegerNegate
    Expr s a
IntegerShow -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
IntegerShow
    Expr s a
IntegerToDouble -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
IntegerToDouble
    Expr s a
Double -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Double
    DoubleLit DhallDouble
n -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DhallDouble -> Expr s a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n)
    Expr s a
DoubleShow -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
DoubleShow
    Expr s a
Text -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Text
    TextLit (Chunks [(Text, Expr s a)]
xys Text
z) -> do
        Chunks s a
chunks' <- [Chunks s a] -> Chunks s a
forall a. Monoid a => [a] -> a
mconcat ([Chunks s a] -> Chunks s a) -> m [Chunks s a] -> m (Chunks s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Chunks s a]
chunks
        case Chunks s a
chunks' of
            Chunks [(Text
"", Expr s a
x)] Text
"" -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
x
            Chunks s a
c                   -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit Chunks s a
c)
      where
        chunks :: m [Chunks s a]
chunks =
          (([Chunks s a] -> [Chunks s a] -> [Chunks s a]
forall a. [a] -> [a] -> [a]
++ [[(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
z]) ([Chunks s a] -> [Chunks s a])
-> ([[Chunks s a]] -> [Chunks s a])
-> [[Chunks s a]]
-> [Chunks s a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Chunks s a]] -> [Chunks s a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) ([[Chunks s a]] -> [Chunks s a])
-> m [[Chunks s a]] -> m [Chunks s a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, Expr s a) -> m [Chunks s a])
-> [(Text, Expr s a)] -> m [[Chunks s a]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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 -> [Chunks s a] -> m [Chunks s a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
x, Chunks s a
c]
            Expr s a
_         -> [Chunks s a] -> m [Chunks s a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
x, Expr s a
y')] Text
forall a. Monoid a => a
mempty]
    TextAppend Expr s a
x Expr s a
y -> Expr s a -> m (Expr s a)
loop (Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
"", Expr s a
x), (Text
"", Expr s a
y)] Text
""))
    Expr s a
TextReplace -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
TextReplace
    Expr s a
TextShow -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
TextShow
    Expr s a
List -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
List
    ListLit Maybe (Expr s a)
t Seq (Expr s a)
es
        | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
es -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Seq (Expr s a) -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t' m (Seq (Expr s a) -> Expr s a)
-> m (Seq (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Seq (Expr s a) -> m (Seq (Expr s a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Seq (Expr s a)
forall a. Seq a
Data.Sequence.empty
        | Bool
otherwise             -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit Maybe (Expr s a)
forall a. Maybe a
Nothing (Seq (Expr s a) -> Expr s a) -> m (Seq (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Seq (Expr s a))
es'
      where
        t' :: m (Maybe (Expr s a))
t'  = (Expr s a -> m (Expr s a))
-> Maybe (Expr s a) -> m (Maybe (Expr s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop Maybe (Expr s a)
t
        es' :: m (Seq (Expr s a))
es' = (Expr s a -> m (Expr s a)) -> Seq (Expr s a) -> m (Seq (Expr s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop Seq (Expr s a)
es
    ListAppend Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
m)  Expr s a
r            | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
m = Expr s a
r
        decide  Expr s a
l            (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
n) | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
n = Expr s a
l
        decide (ListLit Maybe (Expr s a)
t Seq (Expr s a)
m) (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
n)                        = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit Maybe (Expr s a)
t (Seq (Expr s a)
m Seq (Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
forall a. Semigroup a => a -> a -> a
<> Seq (Expr s a)
n)
        decide  Expr s a
l             Expr s a
r                                   = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
ListAppend Expr s a
l Expr s a
r
    Expr s a
ListBuild -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListBuild
    Expr s a
ListFold -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListFold
    Expr s a
ListLength -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListLength
    Expr s a
ListHead -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListHead
    Expr s a
ListLast -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListLast
    Expr s a
ListIndexed -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListIndexed
    Expr s a
ListReverse -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
ListReverse
    Expr s a
Optional -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
Optional
    Some Expr s a
a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Expr s a)
a'
      where
        a' :: m (Expr s a)
a' = Expr s a -> m (Expr s a)
loop Expr s a
a
    Expr s a
None -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
forall s a. Expr s a
None
    Record Map Text (RecordField s a)
kts -> Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
Record (Map Text (RecordField s a) -> Expr s a)
-> (Map Text (RecordField s a) -> Map Text (RecordField s a))
-> Map Text (RecordField s a)
-> Expr s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (RecordField s a) -> Map Text (RecordField s a)
forall k v. Map k v -> Map k v
Dhall.Map.sort (Map Text (RecordField s a) -> Expr s a)
-> m (Map Text (RecordField s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map Text (RecordField s a))
kts'
      where
        f :: RecordField s a -> m (RecordField s a)
f (RecordField Maybe s
s0 Expr s a
expr Maybe s
s1 Maybe s
s2) = (\Expr s a
e -> Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
forall s a.
Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
RecordField Maybe s
s0 Expr s a
e Maybe s
s1 Maybe s
s2) (Expr s a -> RecordField s a)
-> m (Expr s a) -> m (RecordField s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
expr
        kts' :: m (Map Text (RecordField s a))
kts' = (RecordField s a -> m (RecordField s a))
-> Map Text (RecordField s a) -> m (Map Text (RecordField s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse RecordField s a -> m (RecordField s a)
f Map Text (RecordField s a)
kts
    RecordLit Map Text (RecordField s a)
kvs -> Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (Map Text (RecordField s a) -> Expr s a)
-> (Map Text (RecordField s a) -> Map Text (RecordField s a))
-> Map Text (RecordField s a)
-> Expr s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (RecordField s a) -> Map Text (RecordField s a)
forall k v. Map k v -> Map k v
Dhall.Map.sort (Map Text (RecordField s a) -> Expr s a)
-> m (Map Text (RecordField s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map Text (RecordField s a))
kvs'
      where
        f :: RecordField s a -> m (RecordField s a)
f (RecordField Maybe s
s0 Expr s a
expr Maybe s
s1 Maybe s
s2) = (\Expr s a
e -> Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
forall s a.
Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
RecordField Maybe s
s0 Expr s a
e Maybe s
s1 Maybe s
s2) (Expr s a -> RecordField s a)
-> m (Expr s a) -> m (RecordField s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
expr
        kvs' :: m (Map Text (RecordField s a))
kvs' = (RecordField s a -> m (RecordField s a))
-> Map Text (RecordField s a) -> m (Map Text (RecordField s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse RecordField s a -> m (RecordField s a)
f Map Text (RecordField s a)
kvs
    Union Map Text (Maybe (Expr s a))
kts -> Map Text (Maybe (Expr s a)) -> Expr s a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union (Map Text (Maybe (Expr s a)) -> Expr s a)
-> (Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a)))
-> Map Text (Maybe (Expr s a))
-> Expr s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
forall k v. Map k v -> Map k v
Dhall.Map.sort (Map Text (Maybe (Expr s a)) -> Expr s a)
-> m (Map Text (Maybe (Expr s a))) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map Text (Maybe (Expr s a)))
kts'
      where
        kts' :: m (Map Text (Maybe (Expr s a)))
kts' = (Maybe (Expr s a) -> m (Maybe (Expr s a)))
-> Map Text (Maybe (Expr s a)) -> m (Map Text (Maybe (Expr s a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Expr s a -> m (Expr s a))
-> Maybe (Expr s a) -> m (Maybe (Expr s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> m (Expr s a)
loop) Map Text (Maybe (Expr s a))
kts
    Combine Maybe Text
mk Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (RecordLit Map Text (RecordField s a)
m) Expr s a
r | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m =
            Expr s a
r
        decide Expr s a
l (RecordLit Map Text (RecordField s a)
n) | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
n =
            Expr s a
l
        decide (RecordLit Map Text (RecordField s a)
m) (RecordLit Map Text (RecordField s a)
n) =
            Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit ((RecordField s a -> RecordField s a -> RecordField s a)
-> Map Text (RecordField s a)
-> Map Text (RecordField s a)
-> Map Text (RecordField s a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Dhall.Map.unionWith RecordField s a -> RecordField s a -> RecordField s a
f Map Text (RecordField s a)
m Map Text (RecordField s a)
n)
          where
            f :: RecordField s a -> RecordField s a -> RecordField s a
f (RecordField Maybe s
_ Expr s a
expr Maybe s
_ Maybe s
_) (RecordField Maybe s
_ Expr s a
expr' Maybe s
_ Maybe s
_) =
              Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
forall a b. (a -> b) -> a -> b
$ Expr s a -> Expr s a -> Expr s a
decide Expr s a
expr Expr s a
expr'
        decide Expr s a
l Expr s a
r =
            Maybe Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine Maybe Text
mk Expr s a
l Expr s a
r
    CombineTypes Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (Record Map Text (RecordField s a)
m) Expr s a
r | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m =
            Expr s a
r
        decide Expr s a
l (Record Map Text (RecordField s a)
n) | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
n =
            Expr s a
l
        decide (Record Map Text (RecordField s a)
m) (Record Map Text (RecordField s a)
n) =
            Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
Record ((RecordField s a -> RecordField s a -> RecordField s a)
-> Map Text (RecordField s a)
-> Map Text (RecordField s a)
-> Map Text (RecordField s a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Dhall.Map.unionWith RecordField s a -> RecordField s a -> RecordField s a
f Map Text (RecordField s a)
m Map Text (RecordField s a)
n)
          where
            f :: RecordField s a -> RecordField s a -> RecordField s a
f (RecordField Maybe s
_ Expr s a
expr Maybe s
_ Maybe s
_) (RecordField Maybe s
_ Expr s a
expr' Maybe s
_ Maybe s
_) =
              Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
forall a b. (a -> b) -> a -> b
$ Expr s a -> Expr s a -> Expr s a
decide Expr s a
expr Expr s a
expr'
        decide Expr s a
l Expr s a
r =
            Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
CombineTypes Expr s a
l Expr s a
r
    Prefer PreferAnnotation s a
_ Expr s a
x Expr s a
y -> Expr s a -> Expr s a -> Expr s a
forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
decide (Expr s a -> Expr s a -> Expr s a)
-> m (Expr s a) -> m (Expr s a -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> m (Expr s a)
loop Expr s a
x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> m (Expr s a)
loop Expr s a
y
      where
        decide :: Expr s a -> Expr s a -> Expr s a
decide (RecordLit Map Text (RecordField s a)
m) Expr s a
r | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m =
            Expr s a
r
        decide Expr s a
l (RecordLit Map Text (RecordField s a)
n) | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
n =
            Expr s a
l
        decide (RecordLit Map Text (RecordField s a)
m) (RecordLit Map Text (RecordField s a)
n) =
            Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (Map Text (RecordField s a)
-> Map Text (RecordField s a) -> Map Text (RecordField s a)
forall k v. Ord k => Map k v -> Map k v -> Map k v
Dhall.Map.union Map Text (RecordField s a)
n Map Text (RecordField s a)
m)
        decide Expr s a
l Expr s a
r | Expr s a -> Expr s a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr s a
r =
            Expr s a
l
        decide Expr s a
l Expr s a
r =
            PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation s a
forall s a. PreferAnnotation s a
PreferFromSource Expr s a
l Expr s a
r
    RecordCompletion Expr s a
x Expr s a
y ->
        Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Annot (PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation s a
forall s a. PreferAnnotation s a
PreferFromCompletion (Expr s a -> FieldSelection s -> Expr s a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr s a
x FieldSelection s
forall s. FieldSelection s
def) Expr s a
y) (Expr s a -> FieldSelection s -> Expr s a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr s a
x FieldSelection s
forall s. FieldSelection s
typ))
      where
        def :: FieldSelection s
def = Text -> FieldSelection s
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"default"
        typ :: FieldSelection s
typ = Text -> FieldSelection s
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"Type"
    Merge Expr s a
x Expr s a
y Maybe (Expr s a)
t      -> do
        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) (FieldSelection s -> Text
forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY) ->
                        case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (Maybe (Expr s a))
ktsY of
                            Just Maybe (Expr s a)
Nothing ->
                                case RecordField s a -> Expr s a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField s a -> Expr s a)
-> Maybe (RecordField s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (RecordField s a)
kvsX of
                                    Just Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                                    Maybe (Expr s a)
Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                            Maybe (Maybe (Expr s a))
_ ->
                                Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                    App (Field (Union Map Text (Maybe (Expr s a))
ktsY) (FieldSelection s -> Text
forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
kY)) Expr s a
vY ->
                        case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (Maybe (Expr s a))
ktsY of
                            Just (Just Expr s a
_) ->
                                case RecordField s a -> Expr s a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField s a -> Expr s a)
-> Maybe (RecordField s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (RecordField s a)
kvsX of
                                    Just Expr s a
vX -> Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
vX Expr s a
vY)
                                    Maybe (Expr s a)
Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                            Maybe (Maybe (Expr s a))
_ ->
                                Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                    Some Expr s a
a ->
                        case RecordField s a -> Expr s a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField s a -> Expr s a)
-> Maybe (RecordField s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
"Some" Map Text (RecordField s a)
kvsX of
                            Just Expr s a
vX -> Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr s a
vX Expr s a
a)
                            Maybe (Expr s a)
Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                    App Expr s a
None Expr s a
_ ->
                        case RecordField s a -> Expr s a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField s a -> Expr s a)
-> Maybe (RecordField s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Map Text (RecordField s a) -> Maybe (RecordField s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
"None" Map Text (RecordField s a)
kvsX of
                            Just Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                            Maybe (Expr s a)
Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
                    Expr s a
_ -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
            Expr s a
_ -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge Expr s a
x' Expr s a
y' (Maybe (Expr s a) -> Expr s a)
-> m (Maybe (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe (Expr s a))
t'
      where
        t' :: m (Maybe (Expr s a))
t' = (Expr s a -> m (Expr s a))
-> Maybe (Expr s a) -> m (Maybe (Expr s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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' <- (Expr s a -> m (Expr s a))
-> Maybe (Expr s a) -> m (Maybe (Expr s a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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) =
                        Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit
                            ([(Text, RecordField s a)] -> Map Text (RecordField s a)
forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList
                                [ (Text
"mapKey"  , Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField (Expr s a -> RecordField s a) -> Expr s a -> RecordField s a
forall a b. (a -> b) -> a -> b
$ Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [] Text
key))
                                , (Text
"mapValue", Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
value                  )
                                ]
                            )

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

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

                Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit Maybe (Expr s a)
listType Seq (Expr s a)
keyValues)
            Expr s a
_ ->
                Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr s a -> Maybe (Expr s a) -> Expr s a
forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
ToMap Expr s a
x' Maybe (Expr s a)
t')
    Field Expr s a
r k :: FieldSelection s
k@FieldSelection{fieldSelectionLabel :: forall s. FieldSelection s -> Text
fieldSelectionLabel = Text
x}        -> do
        let singletonRecordLit :: RecordField s a -> Expr s a
singletonRecordLit RecordField s a
v = Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (Text -> RecordField s a -> Map Text (RecordField s a)
forall k v. k -> v -> Map k v
Dhall.Map.singleton Text
x RecordField s a
v)

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

        Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Assert Expr s a
t')
    Equivalent 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

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

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

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

                        Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (Text
-> RecordField s a
-> Map Text (RecordField s a)
-> Map Text (RecordField s a)
forall k v. Ord k => k -> v -> Map k v -> Map k v
Dhall.Map.insert Text
k₀ (Expr s a -> RecordField s a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField Expr s a
e₂) Map Text (RecordField s a)
kvs))
            Expr s a
_ ->
                Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
forall s a. Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
With Expr s a
e' NonEmpty Text
ks Expr s a
v')
    Note s
_ Expr s a
e' -> Expr s a -> m (Expr s a)
loop Expr s a
e'
    ImportAlt Expr s a
l Expr s a
_r -> Expr s a -> m (Expr s a)
loop Expr s a
l
    Embed a
a -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Expr s a
forall s a. a -> Expr s a
Embed a
a)

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

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

-- | A reified 'Normalizer', which can be stored in structures without
-- running into impredicative polymorphism.
newtype ReifiedNormalizer a = ReifiedNormalizer
  { ReifiedNormalizer a
-> forall s. Expr s a -> Identity (Maybe (Expr s 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 :: Normalizer a -> Expr s a -> Bool
isNormalizedWith Normalizer a
ctx Expr s a
e = Expr s a
e Expr s a -> Expr s a -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe (ReifiedNormalizer a) -> Expr s a -> Expr s a
forall a s t.
Eq a =>
Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
normalizeWith (ReifiedNormalizer a -> Maybe (ReifiedNormalizer a)
forall a. a -> Maybe a
Just (Normalizer a -> ReifiedNormalizer a
forall a.
(forall s. Expr s a -> Identity (Maybe (Expr s 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 :: Expr s a -> Bool
isNormalized Expr s a
e0 = Expr Any a -> Bool
forall a t. Eq a => Expr t a -> Bool
loop (Expr s a -> Expr Any a
forall s a t. Expr s a -> Expr t a
Syntax.denote Expr s a
e0)
  where
    loop :: Expr t a -> Bool
loop Expr t a
e = case Expr t a
e of
      Const Const
_ -> Bool
True
      Var Var
_ -> Bool
True
      Lam (FunctionBinding Maybe t
Nothing Text
_ Maybe t
Nothing Maybe t
Nothing Expr t a
a) Expr t a
b -> Expr t a -> Bool
loop Expr t a
a Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
b
      Lam FunctionBinding t a
_ Expr t a
_ -> Bool
False
      Pi Text
_ Expr t a
a Expr t a
b -> Expr t a -> Bool
loop Expr t a
a Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
b
      App Expr t a
f Expr t a
a -> Expr t a -> Bool
loop Expr t a
f Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
a Bool -> Bool -> Bool
&& case Expr t a -> Expr t a -> Expr t a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr t a
f Expr t a
a of
          App (Lam FunctionBinding t a
_ Expr t a
_) Expr t a
_ -> Bool
False
          App (App (App (App Expr t a
NaturalFold (NaturalLit Natural
_)) Expr t a
_) Expr t a
_) Expr t a
_ -> Bool
False
          App Expr t a
NaturalBuild Expr t a
_ -> Bool
False
          App Expr t a
NaturalIsZero (NaturalLit Natural
_) -> Bool
False
          App Expr t a
NaturalEven (NaturalLit Natural
_) -> Bool
False
          App Expr t a
NaturalOdd (NaturalLit Natural
_) -> Bool
False
          App Expr t a
NaturalShow (NaturalLit Natural
_) -> Bool
False
          App (App Expr t a
NaturalSubtract (NaturalLit Natural
_)) (NaturalLit Natural
_) -> Bool
False
          App (App Expr t a
NaturalSubtract (NaturalLit Natural
0)) Expr t a
_ -> Bool
False
          App (App Expr t a
NaturalSubtract Expr t a
_) (NaturalLit Natural
0) -> Bool
False
          App (App Expr t a
NaturalSubtract Expr t a
x) Expr t a
y -> Bool -> Bool
not (Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr t a
x Expr t a
y)
          App Expr t a
NaturalToInteger (NaturalLit Natural
_) -> Bool
False
          App Expr t a
IntegerNegate (IntegerLit Integer
_) -> Bool
False
          App Expr t a
IntegerClamp (IntegerLit Integer
_) -> Bool
False
          App Expr t a
IntegerShow (IntegerLit Integer
_) -> Bool
False
          App Expr t a
IntegerToDouble (IntegerLit Integer
_) -> Bool
False
          App Expr t a
DoubleShow (DoubleLit DhallDouble
_) -> Bool
False
          App (App Expr t a
ListBuild Expr t a
_) Expr t a
_ -> Bool
False
          App (App (App (App (App (App Expr t a
ListFold Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_)) Expr t a
_) Expr t a
_) Expr t a
_) Expr t a
_ -> Bool
False
          App (App Expr t a
ListLength Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_) -> Bool
False
          App (App Expr t a
ListHead Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_) -> Bool
False
          App (App Expr t a
ListLast Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_) -> Bool
False
          App (App Expr t a
ListIndexed Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_) -> Bool
False
          App (App Expr t a
ListReverse Expr t a
_) (ListLit Maybe (Expr t a)
_ Seq (Expr t a)
_) -> Bool
False
          App Expr t a
TextShow (TextLit (Chunks [] Text
_)) ->
              Bool
False
          App (App (App Expr t a
TextReplace (TextLit (Chunks [] Text
""))) Expr t a
_) Expr t a
_ ->
              Bool
False
          App (App (App Expr t a
TextReplace (TextLit (Chunks [] Text
_))) Expr t a
_) (TextLit Chunks t a
_) ->
              Bool
False
          Expr t a
_ -> Bool
True
      Let Binding t a
_ Expr t a
_ -> Bool
False
      Annot Expr t a
_ Expr t a
_ -> Bool
False
      Expr t a
Bool -> Bool
True
      BoolLit Bool
_ -> Bool
True
      BoolAnd Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr t a -> Bool
decide (BoolLit Bool
_)  Expr t a
_          = Bool
False
          decide  Expr s a
_          (BoolLit Bool
_) = Bool
False
          decide  Expr s a
l           Expr t a
r          = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      BoolOr Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr t a -> Bool
decide (BoolLit Bool
_)  Expr t a
_          = Bool
False
          decide  Expr s a
_          (BoolLit Bool
_) = Bool
False
          decide  Expr s a
l           Expr t a
r          = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      BoolEQ Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr t a -> Bool
decide (BoolLit Bool
True)  Expr t a
_             = Bool
False
          decide  Expr s a
_             (BoolLit Bool
True) = Bool
False
          decide  Expr s a
l              Expr t a
r             = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      BoolNE Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr t a -> Bool
decide (BoolLit Bool
False)  Expr t a
_               = Bool
False
          decide  Expr s a
_              (BoolLit Bool
False ) = Bool
False
          decide  Expr s a
l               Expr t a
r               = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      BoolIf Expr t a
x Expr t a
y Expr t a
z ->
          Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
z Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Expr t a -> Bool
forall a s a s t. Eq a => Expr s a -> Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y Expr t a
z
        where
          decide :: Expr s a -> Expr s a -> Expr t a -> Bool
decide (BoolLit Bool
_)  Expr s a
_              Expr t a
_              = Bool
False
          decide  Expr s a
_          (BoolLit Bool
True) (BoolLit Bool
False) = Bool
False
          decide  Expr s a
_           Expr s a
l              Expr t a
r              = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      Expr t a
Natural -> Bool
True
      NaturalLit Natural
_ -> Bool
True
      Expr t a
NaturalFold -> Bool
True
      Expr t a
NaturalBuild -> Bool
True
      Expr t a
NaturalIsZero -> Bool
True
      Expr t a
NaturalEven -> Bool
True
      Expr t a
NaturalOdd -> Bool
True
      Expr t a
NaturalShow -> Bool
True
      Expr t a
NaturalSubtract -> Bool
True
      Expr t a
NaturalToInteger -> Bool
True
      NaturalPlus Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall s a s a. Expr s a -> Expr s a -> Bool
decide Expr t a
x Expr t 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 t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall s a s a. Expr s a -> Expr s a -> Bool
decide Expr t a
x Expr t 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 t a
Integer -> Bool
True
      IntegerLit Integer
_ -> Bool
True
      Expr t a
IntegerClamp -> Bool
True
      Expr t a
IntegerNegate -> Bool
True
      Expr t a
IntegerShow -> Bool
True
      Expr t a
IntegerToDouble -> Bool
True
      Expr t a
Double -> Bool
True
      DoubleLit DhallDouble
_ -> Bool
True
      Expr t a
DoubleShow -> Bool
True
      Expr t a
Text -> Bool
True
      TextLit (Chunks [(Text
"", Expr t a
_)] Text
"") -> Bool
False
      TextLit (Chunks [(Text, Expr t a)]
xys Text
_) -> ((Text, Expr t a) -> Bool) -> [(Text, Expr t a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Expr t a -> Bool) -> (Text, Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
check) [(Text, Expr t a)]
xys
        where
          check :: Expr t a -> Bool
check Expr t a
y = Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& case Expr t a
y of
              TextLit Chunks t a
_ -> Bool
False
              Expr t a
_         -> Bool
True
      TextAppend Expr t a
_ Expr t a
_ -> Bool
False
      Expr t a
TextReplace -> Bool
True
      Expr t a
TextShow -> Bool
True
      Expr t a
List -> Bool
True
      ListLit Maybe (Expr t a)
t Seq (Expr t a)
es -> (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Maybe (Expr t a)
t Bool -> Bool -> Bool
&& (Expr t a -> Bool) -> Seq (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Seq (Expr t a)
es
      ListAppend Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall s a s a. Expr s a -> Expr s a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr s a -> Bool
decide (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
m)  Expr s a
_            | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
m = Bool
False
          decide  Expr s a
_            (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
n) | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
n = Bool
False
          decide (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
_) (ListLit Maybe (Expr s a)
_ Seq (Expr s a)
_)                        = Bool
False
          decide  Expr s a
_             Expr s a
_                                   = Bool
True
      Expr t a
ListBuild -> Bool
True
      Expr t a
ListFold -> Bool
True
      Expr t a
ListLength -> Bool
True
      Expr t a
ListHead -> Bool
True
      Expr t a
ListLast -> Bool
True
      Expr t a
ListIndexed -> Bool
True
      Expr t a
ListReverse -> Bool
True
      Expr t a
Optional -> Bool
True
      Some Expr t a
a -> Expr t a -> Bool
loop Expr t a
a
      Expr t a
None -> Bool
True
      Record Map Text (RecordField t a)
kts -> Map Text (RecordField t a) -> Bool
forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (RecordField t a)
kts Bool -> Bool -> Bool
&& (RecordField t a -> Bool) -> Map Text (RecordField t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RecordField t a -> Bool
decide Map Text (RecordField t a)
kts
        where
          decide :: RecordField t a -> Bool
decide (RecordField Maybe t
Nothing Expr t a
exp' Maybe t
Nothing Maybe t
Nothing) = Expr t a -> Bool
loop Expr t a
exp'
          decide RecordField t a
_ = Bool
False
      RecordLit Map Text (RecordField t a)
kvs -> Map Text (RecordField t a) -> Bool
forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (RecordField t a)
kvs Bool -> Bool -> Bool
&& (RecordField t a -> Bool) -> Map Text (RecordField t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RecordField t a -> Bool
decide Map Text (RecordField t a)
kvs
        where
          decide :: RecordField t a -> Bool
decide (RecordField Maybe t
Nothing Expr t a
exp' Maybe t
Nothing Maybe t
Nothing) = Expr t a -> Bool
loop Expr t a
exp'
          decide RecordField t a
_ = Bool
False
      Union Map Text (Maybe (Expr t a))
kts -> Map Text (Maybe (Expr t a)) -> Bool
forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (Maybe (Expr t a))
kts Bool -> Bool -> Bool
&& (Maybe (Expr t a) -> Bool) -> Map Text (Maybe (Expr t a)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop) Map Text (Maybe (Expr t a))
kts
      Combine Maybe Text
_ Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall s a s a. Expr s a -> Expr s a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr s a -> Bool
decide (RecordLit Map Text (RecordField s a)
m) Expr s a
_ | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m = Bool
False
          decide Expr s a
_ (RecordLit Map Text (RecordField s a)
n) | Map Text (RecordField s a) -> Bool
forall (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 Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall s a s a. Expr s a -> Expr s a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr s a -> Bool
decide (Record Map Text (RecordField s a)
m) Expr s a
_ | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m = Bool
False
          decide Expr s a
_ (Record Map Text (RecordField s a)
n) | Map Text (RecordField s a) -> Bool
forall (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 PreferAnnotation t a
_ Expr t a
x Expr t a
y -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& Expr t a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
decide Expr t a
x Expr t a
y
        where
          decide :: Expr s a -> Expr t a -> Bool
decide (RecordLit Map Text (RecordField s a)
m) Expr t a
_ | Map Text (RecordField s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField s a)
m = Bool
False
          decide Expr s a
_ (RecordLit Map Text (RecordField t a)
n) | Map Text (RecordField t a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (RecordField t a)
n = Bool
False
          decide (RecordLit Map Text (RecordField s a)
_) (RecordLit Map Text (RecordField t a)
_) = Bool
False
          decide Expr s a
l Expr t a
r = Bool -> Bool
not (Expr s a -> Expr t a -> Bool
forall a s t. Eq a => Expr s a -> Expr t a -> Bool
Eval.judgmentallyEqual Expr s a
l Expr t a
r)
      RecordCompletion Expr t a
_ Expr t a
_ -> Bool
False
      Merge Expr t a
x Expr t a
y Maybe (Expr t a)
t -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Maybe (Expr t a)
t Bool -> Bool -> Bool
&& case Expr t a
x of
          RecordLit Map Text (RecordField t a)
_ -> case Expr t a
y of
              Field (Union Map Text (Maybe (Expr t a))
_) FieldSelection t
_ -> Bool
False
              App (Field (Union Map Text (Maybe (Expr t a))
_) FieldSelection t
_) Expr t a
_ -> Bool
False
              Some Expr t a
_ -> Bool
False
              App Expr t a
None Expr t a
_ -> Bool
False
              Expr t a
_ -> Bool
True
          Expr t a
_ -> Bool
True
      ToMap Expr t a
x Maybe (Expr t a)
t -> case Expr t a
x of
          RecordLit Map Text (RecordField t a)
_ -> Bool
False
          Expr t a
_ -> Expr t a -> Bool
loop Expr t a
x Bool -> Bool -> Bool
&& (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Maybe (Expr t a)
t
      Field Expr t a
r (FieldSelection Maybe t
Nothing Text
k Maybe t
Nothing) -> case Expr t a
r of
          RecordLit Map Text (RecordField t a)
_ -> Bool
False
          Project Expr t a
_ Either [Text] (Expr t a)
_ -> Bool
False
          Prefer PreferAnnotation t a
_ (RecordLit Map Text (RecordField t a)
m) Expr t a
_ -> Map Text (RecordField t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField t a)
m [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text
k] Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
r
          Prefer PreferAnnotation t a
_ Expr t a
_ (RecordLit Map Text (RecordField t a)
_) -> Bool
False
          Combine Maybe Text
_ (RecordLit Map Text (RecordField t a)
m) Expr t a
_ -> Map Text (RecordField t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField t a)
m [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text
k] Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
r
          Combine Maybe Text
_ Expr t a
_ (RecordLit Map Text (RecordField t a)
m) -> Map Text (RecordField t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (RecordField t a)
m [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text
k] Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
r
          Expr t a
_ -> Expr t a -> Bool
loop Expr t a
r
      Field Expr t a
_ FieldSelection t
_ -> Bool
False
      Project Expr t a
r Either [Text] (Expr t a)
p -> Expr t a -> Bool
loop Expr t a
r Bool -> Bool -> Bool
&&
          case Either [Text] (Expr t a)
p of
              Left [Text]
s -> case Expr t a
r of
                  RecordLit Map Text (RecordField t a)
_ -> Bool
False
                  Project Expr t a
_ Either [Text] (Expr t a)
_ -> Bool
False
                  Prefer PreferAnnotation t a
_ Expr t a
_ (RecordLit Map Text (RecordField t a)
_) -> Bool
False
                  Expr t a
_ -> Bool -> Bool
not ([Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
s) Bool -> Bool -> Bool
&& Set Text -> [Text]
forall a. Set a -> [a]
Data.Set.toList ([Text] -> Set Text
forall a. Ord a => [a] -> Set a
Data.Set.fromList [Text]
s) [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
s
              Right Expr t a
e' -> case Expr t a
e' of
                  Record Map Text (RecordField t a)
_ -> Bool
False
                  Expr t a
_ -> Expr t a -> Bool
loop Expr t a
e'
      Assert Expr t a
t -> Expr t a -> Bool
loop Expr t a
t
      Equivalent Expr t a
l Expr t a
r -> Expr t a -> Bool
loop Expr t a
l Bool -> Bool -> Bool
&& Expr t a -> Bool
loop Expr t a
r
      With{} -> Bool
False
      Note t
_ Expr t a
e' -> Expr t a -> Bool
loop Expr t a
e'
      ImportAlt Expr t a
_ Expr t 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 (Syntax.makeFunctionBinding "x" (Const Type)) "x"
False
-}
freeIn :: Eq a => Var -> Expr s a -> Bool
variable :: Var
variable@(V Text
var Int
i) freeIn :: Var -> Expr s a -> Bool
`freeIn` Expr s a
expression =
    Var -> Expr () a -> Expr () a -> Expr () a
forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst Var
variable (Var -> Expr () a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
var (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))) Expr () a
strippedExpression
      Expr () a -> Expr () a -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr () a
strippedExpression
  where
    denote' :: Expr t b -> Expr () b
    denote' :: Expr t b -> Expr () b
denote' = Expr t b -> Expr () b
forall s a t. Expr s a -> Expr t a
Syntax.denote

    strippedExpression :: Expr () a
strippedExpression = Expr s a -> Expr () a
forall t b. Expr t b -> Expr () b
denote' Expr s a
expression

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