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

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

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

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

import qualified Data.Sequence
import qualified Data.Set
import qualified Data.Text
import qualified Dhall.Eval    as Eval
import qualified Dhall.Map
import qualified Dhall.Set
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 #-}

{-| `shift` is used by both normalization and type-checking to avoid variable
    capture by shifting variable indices

    For example, suppose that you were to normalize the following expression:

> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x

    If you were to substitute @y@ with @x@ without shifting any variable
    indices, then you would get the following incorrect result:

> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form

    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
    order to avoid being misinterpreted as the @x@ bound by the innermost
    lambda.  If we perform that `shift` then we get the correct result:

> λ(a : Type) → λ(x : a) → λ(x : a) → x@1

    As a more worked example, suppose that you were to normalize the following
    expression:

>     λ(a : Type)
> →   λ(f : a → a → a)
> →   λ(x : a)
> →   λ(x : a)
> →   (λ(x : a) → f x x@1) x@1

    The correct normalized result would be:

>     λ(a : Type)
> →   λ(f : a → a → a)
> →   λ(x : a)
> →   λ(x : a)
> →   f x@1 x

    The above example illustrates how we need to both increase and decrease
    variable indices as part of substitution:

    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
      substitute it into the body of the innermost lambda expression in order
      to avoid variable capture.  This substitution changes the body of the
      lambda expression to @(f x\@2 x\@1)@

    * We then remove the innermost lambda and therefore decrease the indices of
      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
      less @x@ variable is now bound within that scope

    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
    the indices of all variables named @x@ whose indices are greater than
    @(n + m)@, where @m@ is the number of bound variables of the same name
    within that scope

    In practice, @d@ is always @1@ or @-1@ because we either:

    * increment variables by @1@ to avoid variable capture during substitution
    * decrement variables by @1@ when deleting lambdas after substitution

    @n@ starts off at @0@ when substitution begins and increments every time we
    descend into a lambda or let expression that binds a variable of the same
    name in order to avoid shifting the bound variables by mistake.
-}
shift :: Int -> Var -> Expr s a -> Expr s a
shift :: Int -> Var -> Expr s a -> Expr s a
shift d :: Int
d (V x :: Text
x n :: Int
n) (Var (V x' :: Text
x' n' :: Int
n')) = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
x' Int
n'')
  where
    n'' :: Int
n'' = if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n' then Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d else Int
n'
shift d :: Int
d (V x :: Text
x n :: Int
n) (Lam x' :: Text
x' _A :: Expr s a
_A b :: Expr s a
b) = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam Text
x' Expr s a
_A' Expr s a
b'
  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
shift Int
d (Text -> Int -> Var
V Text
x Int
n ) Expr s a
_A
    b' :: Expr s a
b'  = Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (Text -> Int -> Var
V Text
x Int
n') Expr s a
b
      where
        n' :: Int
n' = if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' then Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
n
shift d :: Int
d (V x :: Text
x n :: Int
n) (Pi x' :: Text
x' _A :: Expr s a
_A _B :: Expr s a
_B) = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi Text
x' Expr s a
_A' Expr s a
_B'
  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
shift Int
d (Text -> Int -> Var
V Text
x Int
n ) Expr s a
_A
    _B' :: Expr s a
_B' = Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (Text -> Int -> Var
V Text
x Int
n') Expr s a
_B
      where
        n' :: Int
n' = if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' then Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
n
shift d :: Int
d (V x :: Text
x n :: Int
n) (Let (Binding src0 :: Maybe s
src0 f :: Text
f src1 :: Maybe s
src1 mt :: Maybe (Maybe s, Expr s a)
mt src2 :: Maybe s
src2 r :: Expr s a
r) e :: Expr s a
e) =
    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
e'
  where
    e' :: Expr s a
e' = Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (Text -> Int -> Var
V Text
x Int
n') Expr s a
e
      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
+ 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 (Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (Text -> Int -> Var
V Text
x Int
n))) Maybe (Maybe s, Expr s a)
mt
    r' :: Expr s a
r'  =             Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (Text -> Int -> Var
V Text
x Int
n)  Expr s a
r
shift d :: Int
d v :: Var
v expression :: 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 (Int -> Var -> Expr s a -> Expr s a
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d Var
v) Expr s a
expression

{-| 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 _ _ (Const a :: Const
a) = Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
a
subst (V x :: Text
x n :: Int
n) e :: Expr s a
e (Lam y :: Text
y _A :: Expr s a
_A b :: Expr s a
b) = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam 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
shift 1 (Text -> Int -> Var
V Text
y 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
+ 1 else Int
n
subst (V x :: Text
x n :: Int
n) e :: Expr s a
e (Pi y :: Text
y _A :: Expr s a
_A _B :: Expr s a
_B) = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi 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
shift 1 (Text -> Int -> Var
V Text
y 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
+ 1 else Int
n
subst v :: Var
v e :: Expr s a
e (Var v' :: 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 x :: Text
x n :: Int
n) e :: Expr s a
e (Let (Binding src0 :: Maybe s
src0 f :: Text
f src1 :: Maybe s
src1 mt :: Maybe (Maybe s, Expr s a)
mt src2 :: Maybe s
src2 r :: Expr s a
r) b :: Expr s a
b) =
    Binding s a -> Expr s a -> Expr s a
forall s a. Binding s a -> Expr s a -> Expr s a
Let (Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
forall s a.
Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
Binding Maybe s
src0 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
shift 1 (Text -> Int -> Var
V Text
f 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
+ 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 x :: Var
x e :: Expr s a
e expression :: 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 Bool             = Bool
True
boundedType Natural          = Bool
True
boundedType Integer          = Bool
True
boundedType Double           = Bool
True
boundedType Text             = Bool
True
boundedType (App List _)     = Bool
False
boundedType (App Optional t :: Expr s a
t) = Expr s a -> Bool
forall s a. Expr s a -> Bool
boundedType Expr s a
t
boundedType (Record kvs :: Map Text (Expr s a)
kvs)     = (Expr s a -> Bool) -> Map Text (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 (Expr s a)
kvs
boundedType (Union kvs :: 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 _                = Bool
False

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

>>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x"))))
Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (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 `typeWith`. The `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 ctx :: ReifiedNormalizer a
ctx) t :: 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 _          t :: 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 ctx :: NormalizerM m a
ctx e0 :: 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 e :: Expr s a
e =  case Expr s a
e of
    Const k :: 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 v :: 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 x :: Text
x _A :: Expr s a
_A b :: Expr s a
b -> Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam 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
    Pi x :: Text
x _A :: Expr s a
_A _B :: Expr s a
_B -> Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi 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 f :: Expr s a
f a :: 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 e1 :: Expr s a
e1 -> Expr s a -> m (Expr s a)
loop Expr s a
e1
          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 x :: Text
x _A :: Expr s a
_A b₀ :: 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
shift 1 (Text -> Int -> Var
V Text
x 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 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
shift (-1) (Text -> Int -> Var
V Text
x 0) Expr s a
b₁

                    Expr s a -> m (Expr s a)
loop Expr s a
b₂
                _ -> do
                  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 NaturalFold (NaturalLit n0 :: Natural
n0)) t :: Expr s a
t) succ' :: Expr s a
succ') zero :: 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
- 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
- 1))
                    App NaturalBuild g :: 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 = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "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 "n" (Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 1))

                        zero :: Expr s a
zero = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
                    App NaturalIsZero (NaturalLit n :: 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
== 0))
                    App NaturalEven (NaturalLit n :: 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 NaturalOdd (NaturalLit n :: 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 NaturalToInteger (NaturalLit n :: 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 NaturalShow (NaturalLit n :: 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
Data.Text.pack (Natural -> String
forall a. Show a => a -> String
show Natural
n))))
                    App (App NaturalSubtract (NaturalLit x :: Natural
x)) (NaturalLit y :: 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 0)
                    App (App NaturalSubtract (NaturalLit 0)) y :: 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 NaturalSubtract _) (NaturalLit 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 0)
                    App (App NaturalSubtract x :: Expr s a
x) y :: 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 0)
                    App IntegerClamp (IntegerLit n :: Integer
n)
                        | 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 0)
                    App IntegerNegate (IntegerLit n :: 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 IntegerShow (IntegerLit n :: Integer
n)
                        | 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
forall a. Semigroup a => a -> a -> a
<> String -> Text
Data.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
Data.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 IntegerToDouble (IntegerLit n :: 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 DoubleShow (DoubleLit (DhallDouble n :: 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
Data.Text.pack (Double -> String
forall a. Show a => a -> String
show Double
n))))
                    App (App OptionalBuild _A₀ :: Expr s a
_A₀) g :: 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
optional) Expr s a
just) Expr s a
nothing)
                      where
                        optional :: Expr s a
optional = 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
Optional Expr s a
_A₀

                        just :: Expr s a
just = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "a" Expr s a
_A₀ (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some "a")

                        nothing :: Expr s a
nothing = 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
_A₀
                    App (App ListBuild _A₀ :: Expr s a
_A₀) g :: 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
shift 1 "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 =
                            Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "a" Expr s a
_A₀
                                (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "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 "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 ListFold _) (ListLit _ xs :: Seq (Expr s a)
xs)) t :: Expr s a
t) cons :: Expr s a
cons) nil :: 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 y :: Expr s a
y ys :: m (Expr s a)
ys = do
                          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   y :: Expr s a
y ys :: 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 ListLength _) (ListLit _ ys :: 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 ListHead t :: Expr s a
t) (ListLit _ ys :: 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
                                y :: Expr s a
y :< _ -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some 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
App Expr s a
forall s a. Expr s a
None Expr s a
t
                    App (App ListLast t :: Expr s a
t) (ListLit _ ys :: 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
                                _ :> y :: Expr s a
y -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some 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
App Expr s a
forall s a. Expr s a
None Expr s a
t
                    App (App ListIndexed _A₀ :: Expr s a
_A₀) (ListLit _ as₀ :: 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 (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
Record ([(Text, Expr s a)] -> Map Text (Expr s a)
forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList [(Text, Expr s a)]
kts)
                          where
                            kts :: [(Text, Expr s a)]
kts = [ ("index", Expr s a
forall s a. Expr s a
Natural)
                                  , ("value", 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 n :: a
n a_ :: Expr s a
a_ =
                            Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit ([(Text, Expr s a)] -> Map Text (Expr s a)
forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList [(Text, Expr s a)]
kvs)
                          where
                            kvs :: [(Text, Expr s a)]
kvs = [ ("index", 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))
                                  , ("value", Expr s a
a_)
                                  ]
                    App (App ListReverse _) (ListLit t :: Maybe (Expr s a)
t xs :: 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 (App OptionalFold t0 :: Expr s a
t0) x0 :: Expr s a
x0 -> do
                        Expr s a
t1 <- Expr s a -> m (Expr s a)
loop Expr s a
t0
                        let optional :: Expr s a
optional = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "optional" 0)
                        let lam :: Expr s a -> Expr s a
lam term :: Expr s a
term = (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "optional"
                                           (Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
Type)
                                           (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "some"
                                               (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" Expr s a
t1 Expr s a
forall s a. Expr s a
optional)
                                               (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "none" Expr s a
forall s a. Expr s a
optional Expr s a
term)))
                        Expr s a
x1 <- Expr s a -> m (Expr s a)
loop Expr s a
x0
                        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
$ case Expr s a
x1 of
                            App None _ -> Expr s a -> Expr s a
lam (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "none" 0))
                            Some x' :: Expr s a
x'    -> Expr s a -> Expr s a
lam (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "some" 0)) Expr s a
x')
                            _          -> 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
OptionalFold Expr s a
t1) Expr s a
x1

                    App TextShow (TextLit (Chunks [] oldText :: 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
                    _ -> 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
                            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 app' :: Expr s a
app' -> Expr s a -> m (Expr s a)
loop Expr s a
app'
    Let (Binding _ f :: Text
f _ _ _ r :: Expr s a
r) b :: 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
shift   1  (Text -> Int -> Var
V Text
f 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 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
shift (-1) (Text -> Int -> Var
V Text
f 0) Expr s a
b'
    Annot x :: Expr s a
x _ -> Expr s a -> m (Expr s a)
loop Expr s a
x
    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 b :: 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 x :: Expr s a
x y :: 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 True )  r :: Expr s a
r              = Expr s a
r
        decide (BoolLit False)  _              = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
        decide  l :: Expr s a
l              (BoolLit True ) = Expr s a
l
        decide  _              (BoolLit False) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
        decide  l :: Expr s a
l               r :: 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 x :: Expr s a
x y :: 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 False)  r :: Expr s a
r              = Expr s a
r
        decide (BoolLit True )  _              = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
        decide  l :: Expr s a
l              (BoolLit False) = Expr s a
l
        decide  _              (BoolLit True ) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
        decide  l :: Expr s a
l               r :: 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 x :: Expr s a
x y :: 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 True )  r :: Expr s a
r              = Expr s a
r
        decide  l :: Expr s a
l              (BoolLit True ) = Expr s a
l
        decide  l :: Expr s a
l               r :: 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 x :: Expr s a
x y :: 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 False)  r :: Expr s a
r              = Expr s a
r
        decide  l :: Expr s a
l              (BoolLit False) = Expr s a
l
        decide  l :: Expr s a
l               r :: 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 bool :: Expr s a
bool true :: Expr s a
true false :: 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 True )  l :: Expr s a
l              _              = Expr s a
l
        decide (BoolLit False)  _              r :: Expr s a
r              = Expr s a
r
        decide  b :: Expr s a
b              (BoolLit True) (BoolLit False) = Expr s a
b
        decide  b :: Expr s a
b               l :: Expr s a
l              r :: 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
    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 n :: 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)
    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
    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
    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
    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
    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
    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
    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
    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 x :: Expr s a
x y :: 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 0)  r :: Expr s a
r             = Expr s a
r
        decide  l :: Expr s a
l             (NaturalLit 0) = Expr s a
l
        decide (NaturalLit m :: Natural
m) (NaturalLit n :: 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  l :: Expr s a
l              r :: 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 x :: Expr s a
x y :: 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 1)  r :: Expr s a
r             = Expr s a
r
        decide  l :: Expr s a
l             (NaturalLit 1) = Expr s a
l
        decide (NaturalLit 0)  _             = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
        decide  _             (NaturalLit 0) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
        decide (NaturalLit m :: Natural
m) (NaturalLit n :: 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  l :: Expr s a
l              r :: 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
    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 n :: 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)
    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
    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
    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
    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
    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 n :: 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)
    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
    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 xys :: [(Text, Expr s a)]
xys z :: 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 [("", x :: Expr s a
x)] "" -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
x
            c :: 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 (x :: Text
x, y :: 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 c :: 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]
            _         -> [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 x :: Expr s a
x y :: 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 [("", Expr s a
x), ("", Expr s a
y)] ""))
    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
    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 t :: Maybe (Expr s a)
t es :: 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 x :: Expr s a
x y :: 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 _ m :: Seq (Expr s a)
m)  r :: 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  l :: Expr s a
l            (ListLit _ n :: 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 t :: Maybe (Expr s a)
t m :: Seq (Expr s a)
m) (ListLit _ n :: 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  l :: Expr s a
l             r :: 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
    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
    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
    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
    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
    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
    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
    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
    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 a :: 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
    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
    OptionalFold -> 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
OptionalFold
    OptionalBuild -> 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
OptionalBuild
    Record kts :: Map Text (Expr s a)
kts -> Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
Record (Map Text (Expr s a) -> Expr s a)
-> (Map Text (Expr s a) -> Map Text (Expr s a))
-> Map Text (Expr s a)
-> Expr s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (Expr s a) -> Map Text (Expr s a)
forall k v. Map k v -> Map k v
Dhall.Map.sort (Map Text (Expr s a) -> Expr s a)
-> m (Map Text (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map Text (Expr s a))
kts'
      where
        kts' :: m (Map Text (Expr s a))
kts' = (Expr s a -> m (Expr s a))
-> Map Text (Expr s a) -> m (Map Text (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 (Expr s a)
kts
    RecordLit kvs :: Map Text (Expr s a)
kvs -> Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Map Text (Expr s a) -> Expr s a)
-> (Map Text (Expr s a) -> Map Text (Expr s a))
-> Map Text (Expr s a)
-> Expr s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (Expr s a) -> Map Text (Expr s a)
forall k v. Map k v -> Map k v
Dhall.Map.sort (Map Text (Expr s a) -> Expr s a)
-> m (Map Text (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map Text (Expr s a))
kvs'
      where
        kvs' :: m (Map Text (Expr s a))
kvs' = (Expr s a -> m (Expr s a))
-> Map Text (Expr s a) -> m (Map Text (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 (Expr s a)
kvs
    Union kts :: Map Text (Maybe (Expr s a))
kts -> Map Text (Maybe (Expr s a)) -> Expr s a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union (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 mk :: Maybe Text
mk x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: Expr s a
r | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m =
            Expr s a
r
        decide l :: Expr s a
l (RecordLit n :: Map Text (Expr s a)
n) | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
n =
            Expr s a
l
        decide (RecordLit m :: Map Text (Expr s a)
m) (RecordLit n :: Map Text (Expr s a)
n) =
            Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit ((Expr s a -> Expr s a -> Expr s a)
-> Map Text (Expr s a)
-> Map Text (Expr s a)
-> Map Text (Expr s a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Dhall.Map.unionWith Expr s a -> Expr s a -> Expr s a
decide Map Text (Expr s a)
m Map Text (Expr s a)
n)
        decide l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: Expr s a
r | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m =
            Expr s a
r
        decide l :: Expr s a
l (Record n :: Map Text (Expr s a)
n) | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
n =
            Expr s a
l
        decide (Record m :: Map Text (Expr s a)
m) (Record n :: Map Text (Expr s a)
n) =
            Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
Record ((Expr s a -> Expr s a -> Expr s a)
-> Map Text (Expr s a)
-> Map Text (Expr s a)
-> Map Text (Expr s a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Dhall.Map.unionWith Expr s a -> Expr s a -> Expr s a
decide Map Text (Expr s a)
m Map Text (Expr s a)
n)
        decide l :: Expr s a
l r :: 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 _ x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: Expr s a
r | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m =
            Expr s a
r
        decide l :: Expr s a
l (RecordLit n :: Map Text (Expr s a)
n) | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
n =
            Expr s a
l
        decide (RecordLit m :: Map Text (Expr s a)
m) (RecordLit n :: Map Text (Expr s a)
n) =
            Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Map Text (Expr s a) -> Map Text (Expr s a) -> Map Text (Expr s a)
forall k v. Ord k => Map k v -> Map k v -> Map k v
Dhall.Map.union Map Text (Expr s a)
n Map Text (Expr s a)
m)
        decide l :: Expr s a
l r :: 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 l :: Expr s a
l r :: 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 x :: Expr s a
x y :: Expr s a
y -> 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
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 -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
x "default") Expr s a
y) (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
x "Type"))
    Merge x :: Expr s a
x y :: Expr s a
y t :: 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 kvsX :: Map Text (Expr s a)
kvsX ->
                case Expr s a
y' of
                    Field (Union ktsY :: Map Text (Maybe (Expr s a))
ktsY) kY :: 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 Nothing ->
                                case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (Expr s a)
kvsX of
                                    Just vX :: Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                                    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 -> 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 ktsY :: Map Text (Maybe (Expr s a))
ktsY) kY :: Text
kY) vY :: 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 _) ->
                                case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
kY Map Text (Expr s a)
kvsX of
                                    Just vX :: 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)
                                    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 -> 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 a :: Expr s a
a ->
                        case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup "Some" Map Text (Expr s a)
kvsX of
                            Just vX :: 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)
                            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 None _ ->
                        case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup "None" Map Text (Expr s a)
kvsX of
                            Just vX :: Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
                            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 -> 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 -> 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 x :: Expr s a
x t :: 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 kvsX :: Map Text (Expr s a)
kvsX -> do
                let entry :: (Text, Expr s a) -> Expr s a
entry (key :: Text
key, value :: Expr s a
value) =
                        Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit
                            ([(Text, Expr s a)] -> Map Text (Expr s a)
forall k v. Ord k => [(k, v)] -> Map k v
Dhall.Map.fromList
                                [ ("mapKey"  , 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))
                                , ("mapValue", 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)
kvsX))

                let listType :: Maybe (Expr s a)
listType = case Maybe (Expr s a)
t' of
                        Just _ | 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)
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)
            _ -> do
                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 r :: Expr s a
r x :: Text
x        -> do
        let singletonRecordLit :: Expr s a -> Expr s a
singletonRecordLit v :: Expr s a
v = Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Text -> Expr s a -> Map Text (Expr s a)
forall k v. k -> v -> Map k v
Dhall.Map.singleton Text
x Expr 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 kvs :: Map Text (Expr s a)
kvs ->
                case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
x Map Text (Expr s a)
kvs of
                    Just v :: Expr s a
v  -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
v
                    Nothing -> Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field (Expr s a -> Text -> Expr s a)
-> m (Expr s a) -> m (Text -> Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Map Text (Expr s a) -> Expr s a)
-> m (Map Text (Expr s a)) -> m (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr s a -> m (Expr s a))
-> Map Text (Expr s a) -> m (Map Text (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 (Expr s a)
kvs) m (Text -> Expr s a) -> m Text -> m (Expr s a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Text -> m Text
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
x
            Project r_ :: Expr s a
r_ _ -> Expr s a -> m (Expr s a)
loop (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
r_ Text
x)
            Prefer _ (RecordLit kvs :: Map Text (Expr s a)
kvs) r_ :: Expr s a
r_ -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
x Map Text (Expr s a)
kvs of
                Just v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> 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 (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
singletonRecordLit Expr s a
v) Expr s a
r_) Text
x)
                Nothing -> Expr s a -> m (Expr s a)
loop (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
r_ Text
x)
            Prefer _ l :: Expr s a
l (RecordLit kvs :: Map Text (Expr s a)
kvs) -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
x Map Text (Expr s a)
kvs of
                Just v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
v
                Nothing -> Expr s a -> m (Expr s a)
loop (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
l Text
x)
            Combine m :: Maybe Text
m (RecordLit kvs :: Map Text (Expr s a)
kvs) r_ :: Expr s a
r_ -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
x Map Text (Expr s a)
kvs of
                Just v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> 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 -> Expr s a
forall s a. Expr s a -> Expr s a
singletonRecordLit Expr s a
v) Expr s a
r_) Text
x)
                Nothing -> Expr s a -> m (Expr s a)
loop (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
r_ Text
x)
            Combine m :: Maybe Text
m l :: Expr s a
l (RecordLit kvs :: Map Text (Expr s a)
kvs) -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
forall k v. Ord k => k -> Map k v -> Maybe v
Dhall.Map.lookup Text
x Map Text (Expr s a)
kvs of
                Just v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> 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 (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
singletonRecordLit Expr s a
v)) Text
x)
                Nothing -> Expr s a -> m (Expr s a)
loop (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
l Text
x)
            _ -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
r' Text
x)
    Project x :: Expr s a
x (Left fields :: Set Text
fields)-> do
        Expr s a
x' <- Expr s a -> m (Expr s a)
loop Expr s a
x
        let fieldsSet :: Set Text
fieldsSet = Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.toSet Set Text
fields
        case Expr s a
x' of
            RecordLit kvs :: Map Text (Expr s a)
kvs ->
                Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Map Text (Expr s a) -> Set Text -> Map Text (Expr s a)
forall k a. Ord k => Map k a -> Set k -> Map k a
Dhall.Map.restrictKeys Map Text (Expr s a)
kvs Set Text
fieldsSet))
            Project y :: Expr s a
y _ ->
                Expr s a -> m (Expr s a)
loop (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr s a
y (Set Text -> Either (Set Text) (Expr s a)
forall a b. a -> Either a b
Left Set Text
fields))
            Prefer _ l :: Expr s a
l (RecordLit rKvs :: Map Text (Expr s a)
rKvs) -> do
                let rKs :: Set Text
rKs = Map Text (Expr s a) -> Set Text
forall k v. Map k v -> Set k
Dhall.Map.keysSet Map Text (Expr s a)
rKvs
                let l' :: Expr s a
l' = Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr s a
l (Set Text -> Either (Set Text) (Expr s a)
forall a b. a -> Either a b
Left (Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.fromSet (Set Text -> Set Text -> Set Text
forall a. Ord a => Set a -> Set a -> Set a
Data.Set.difference Set Text
fieldsSet Set Text
rKs)))
                let r' :: Expr s a
r' = Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit (Map Text (Expr s a) -> Set Text -> Map Text (Expr s a)
forall k a. Ord k => Map k a -> Set k -> Map k a
Dhall.Map.restrictKeys Map Text (Expr 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')
            _ | Set Text -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Text
fields -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit Map Text (Expr 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 (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr s a
x' (Set Text -> Either (Set Text) (Expr s a)
forall a b. a -> Either a b
Left (Set Text -> Set Text
forall a. Ord a => Set a -> Set a
Dhall.Set.sort Set Text
fields)))
    Project r :: Expr s a
r (Right e1 :: 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 kts :: Map Text (Expr s a)
kts -> do
                Expr s a -> m (Expr s a)
loop (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr s a
r (Set Text -> Either (Set Text) (Expr s a)
forall a b. a -> Either a b
Left (Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.fromSet (Map Text (Expr s a) -> Set Text
forall k v. Map k v -> Set k
Dhall.Map.keysSet Map Text (Expr s a)
kts))))
            _ -> 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 (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr s a
r' (Expr s a -> Either (Set Text) (Expr s a)
forall a b. b -> Either a b
Right Expr s a
e2))
    Assert t :: 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 l :: Expr s a
l r :: 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 e' :: Expr s a
e' k :: NonEmpty Text
k v :: Expr s a
v -> do
        Expr s a -> m (Expr s a)
loop (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Syntax.desugarWith (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
k Expr s a
v))
    Note _ e' :: Expr s a
e' -> Expr s a -> m (Expr s a)
loop Expr s a
e'
    ImportAlt l :: Expr s a
l _r :: Expr s a
_r -> Expr s a -> m (Expr s a)
loop Expr s a
l
    Embed a :: 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 ctx :: Normalizer a
ctx e :: 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 e0 :: 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 e :: Expr t a
e = case Expr t a
e of
      Const _ -> Bool
True
      Var _ -> Bool
True
      Lam _ a :: Expr t a
a b :: 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
      Pi _ a :: Expr t a
a b :: 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 f :: Expr t a
f a :: 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 _ _ _) _ -> Bool
False
          App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> Bool
False
          App NaturalBuild _ -> Bool
False
          App NaturalIsZero (NaturalLit _) -> Bool
False
          App NaturalEven (NaturalLit _) -> Bool
False
          App NaturalOdd (NaturalLit _) -> Bool
False
          App NaturalShow (NaturalLit _) -> Bool
False
          App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> Bool
False
          App (App NaturalSubtract (NaturalLit 0)) _ -> Bool
False
          App (App NaturalSubtract _) (NaturalLit 0) -> Bool
False
          App (App NaturalSubtract x :: Expr t a
x) y :: 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 NaturalToInteger (NaturalLit _) -> Bool
False
          App IntegerNegate (IntegerLit _) -> Bool
False
          App IntegerClamp (IntegerLit _) -> Bool
False
          App IntegerShow (IntegerLit _) -> Bool
False
          App IntegerToDouble (IntegerLit _) -> Bool
False
          App DoubleShow (DoubleLit _) -> Bool
False
          App (App OptionalBuild _) _ -> Bool
False
          App (App ListBuild _) _ -> Bool
False
          App (App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _) _ -> Bool
False
          App (App ListLength _) (ListLit _ _) -> Bool
False
          App (App ListHead _) (ListLit _ _) -> Bool
False
          App (App ListLast _) (ListLit _ _) -> Bool
False
          App (App ListIndexed _) (ListLit _ _) -> Bool
False
          App (App ListReverse _) (ListLit _ _) -> Bool
False
          App (App OptionalFold _) (Some _) -> Bool
False
          App (App OptionalFold _) (App None _) -> Bool
False
          App TextShow (TextLit (Chunks [] _)) ->
              Bool
False
          _ -> Bool
True
      Let _ _ -> Bool
False
      Annot _ _ -> Bool
False
      Bool -> Bool
True
      BoolLit _ -> Bool
True
      BoolAnd x :: Expr t a
x y :: 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
          decide  _          (BoolLit _) = Bool
False
          decide  l :: Expr s a
l           r :: 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 x :: Expr t a
x y :: 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
          decide  _          (BoolLit _) = Bool
False
          decide  l :: Expr s a
l           r :: 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 x :: Expr t a
x y :: 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 True)  _             = Bool
False
          decide  _             (BoolLit True) = Bool
False
          decide  l :: Expr s a
l              r :: 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 x :: Expr t a
x y :: 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 False)  _               = Bool
False
          decide  _              (BoolLit False ) = Bool
False
          decide  l :: Expr s a
l               r :: 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 x :: Expr t a
x y :: Expr t a
y z :: 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
False
          decide  _          (BoolLit True) (BoolLit False) = Bool
False
          decide  _           l :: Expr s a
l              r :: 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)
      Natural -> Bool
True
      NaturalLit _ -> Bool
True
      NaturalFold -> Bool
True
      NaturalBuild -> Bool
True
      NaturalIsZero -> Bool
True
      NaturalEven -> Bool
True
      NaturalOdd -> Bool
True
      NaturalShow -> Bool
True
      NaturalSubtract -> Bool
True
      NaturalToInteger -> Bool
True
      NaturalPlus x :: Expr t a
x y :: 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 0)  _             = Bool
False
          decide  _             (NaturalLit 0) = Bool
False
          decide (NaturalLit _) (NaturalLit _) = Bool
False
          decide  _              _             = Bool
True
      NaturalTimes x :: Expr t a
x y :: 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 0)  _             = Bool
False
          decide  _             (NaturalLit 0) = Bool
False
          decide (NaturalLit 1)  _             = Bool
False
          decide  _             (NaturalLit 1) = Bool
False
          decide (NaturalLit _) (NaturalLit _) = Bool
False
          decide  _              _             = Bool
True
      Integer -> Bool
True
      IntegerLit _ -> Bool
True
      IntegerClamp -> Bool
True
      IntegerNegate -> Bool
True
      IntegerShow -> Bool
True
      IntegerToDouble -> Bool
True
      Double -> Bool
True
      DoubleLit _ -> Bool
True
      DoubleShow -> Bool
True
      Text -> Bool
True
      TextLit (Chunks [("", _)] "") -> Bool
False
      TextLit (Chunks xys :: [(Text, Expr t a)]
xys _) -> ((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 y :: Expr t a
y = Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& case Expr t a
y of
              TextLit _ -> Bool
False
              _         -> Bool
True
      TextAppend _ _ -> Bool
False
      TextShow -> Bool
True
      List -> Bool
True
      ListLit t :: Maybe (Expr t a)
t es :: 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 x :: Expr t a
x y :: 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 _ m :: Seq (Expr s a)
m)  _            | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
m = Bool
False
          decide  _            (ListLit _ n :: 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 _ _) (ListLit _ _)                        = Bool
False
          decide  _             _                                   = Bool
True
      ListBuild -> Bool
True
      ListFold -> Bool
True
      ListLength -> Bool
True
      ListHead -> Bool
True
      ListLast -> Bool
True
      ListIndexed -> Bool
True
      ListReverse -> Bool
True
      Optional -> Bool
True
      Some a :: Expr t a
a -> Expr t a -> Bool
loop Expr t a
a
      None -> Bool
True
      OptionalFold -> Bool
True
      OptionalBuild -> Bool
True
      Record kts :: Map Text (Expr t a)
kts -> Map Text (Expr t a) -> Bool
forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (Expr t a)
kts Bool -> Bool -> Bool
&& (Expr t a -> Bool) -> Map Text (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Map Text (Expr t a)
kts
      RecordLit kvs :: Map Text (Expr t a)
kvs -> Map Text (Expr t a) -> Bool
forall k v. Eq k => Map k v -> Bool
Dhall.Map.isSorted Map Text (Expr t a)
kvs Bool -> Bool -> Bool
&& (Expr t a -> Bool) -> Map Text (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr t a -> Bool
loop Map Text (Expr t a)
kvs
      Union kts :: 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 _ x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m = Bool
False
          decide _ (RecordLit n :: Map Text (Expr s a)
n) | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
n = Bool
False
          decide (RecordLit _) (RecordLit _) = Bool
False
          decide  _ _ = Bool
True
      CombineTypes x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m = Bool
False
          decide _ (Record n :: Map Text (Expr s a)
n) | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
n = Bool
False
          decide (Record _) (Record _) = Bool
False
          decide  _ _ = Bool
True
      Prefer _ x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | Map Text (Expr s a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr s a)
m = Bool
False
          decide _ (RecordLit n :: Map Text (Expr t a)
n) | Map Text (Expr t a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Data.Foldable.null Map Text (Expr t a)
n = Bool
False
          decide (RecordLit _) (RecordLit _) = Bool
False
          decide l :: Expr s a
l r :: 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 _ _ -> Bool
False
      Merge x :: Expr t a
x y :: Expr t a
y t :: 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 _ -> case Expr t a
y of
              Field (Union _) _ -> Bool
False
              App (Field (Union _) _) _ -> Bool
False
              Some _ -> Bool
False
              App None _ -> Bool
False
              _ -> Bool
True
          _ -> Bool
True
      ToMap x :: Expr t a
x t :: Maybe (Expr t a)
t -> case Expr t a
x of
          RecordLit _ -> Bool
False
          _ -> 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 r :: Expr t a
r k :: Text
k -> case Expr t a
r of
          RecordLit _ -> Bool
False
          Project _ _ -> Bool
False
          Prefer _ (RecordLit m :: Map Text (Expr t a)
m) _ -> Map Text (Expr t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (Expr 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 _ _ (RecordLit _) -> Bool
False
          Combine _ (RecordLit m :: Map Text (Expr t a)
m) _ -> Map Text (Expr t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (Expr 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 _ _ (RecordLit m :: Map Text (Expr t a)
m) -> Map Text (Expr t a) -> [Text]
forall k v. Map k v -> [k]
Dhall.Map.keys Map Text (Expr 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 -> Bool
loop Expr t a
r
      Project r :: Expr t a
r p :: Either (Set Text) (Expr t a)
p -> Expr t a -> Bool
loop Expr t a
r Bool -> Bool -> Bool
&&
          case Either (Set Text) (Expr t a)
p of
              Left s :: Set Text
s -> case Expr t a
r of
                  RecordLit _ -> Bool
False
                  Project _ _ -> Bool
False
                  Prefer _ _ (RecordLit _) -> Bool
False
                  _ -> Bool -> Bool
not (Set Text -> Bool
forall a. Set a -> Bool
Dhall.Set.null Set Text
s) Bool -> Bool -> Bool
&& Set Text -> Bool
forall a. Ord a => Set a -> Bool
Dhall.Set.isSorted Set Text
s
              Right e' :: Expr t a
e' -> case Expr t a
e' of
                  Record _ -> Bool
False
                  _ -> Expr t a -> Bool
loop Expr t a
e'
      Assert t :: Expr t a
t -> Expr t a -> Bool
loop Expr t a
t
      Equivalent l :: Expr t a
l r :: 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 _ e' :: Expr t a
e' -> Expr t a -> Bool
loop Expr t a
e'
      ImportAlt _ _ -> Bool
False
      Embed _ -> Bool
True

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

>>> "x" `freeIn` "x"
True
>>> "x" `freeIn` "y"
False
>>> "x" `freeIn` Lam "x" (Const Type) "x"
False
-}
freeIn :: Eq a => Var -> Expr s a -> Bool
variable :: Var
variable@(V var :: Text
var i :: Int
i) freeIn :: Var -> Expr s a -> Bool
`freeIn` expression :: 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
+ 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