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

module Dhall.Syntax.Operations
    ( -- * Optics
      subExpressions
    , subExpressionsWith
    , unsafeSubExpressions

      -- * Handling 'Note's
    , denote
    , renote
    , shallowDenote

      -- * Reserved identifiers
    , reservedIdentifiers
    , reservedKeywords

      -- * Utilities
    , internalError
      -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a
      -- module cycle
    , shift
    ) where

import Data.HashSet                 (HashSet)
import Data.Text                    (Text)
import Data.Void                    (Void)
import Dhall.Syntax.Binding         (Binding (..), bindingExprs)
import Dhall.Syntax.Chunks          (chunkExprs)
import Dhall.Syntax.Expr
import Dhall.Syntax.FunctionBinding
import Dhall.Syntax.RecordField     (RecordField (..), recordFieldExprs)
import Dhall.Syntax.Types
import Dhall.Syntax.Var
import Unsafe.Coerce                (unsafeCoerce)

import qualified Data.HashSet
import qualified Data.Text
import qualified Lens.Family  as Lens


-- | A traversal over the immediate sub-expressions of an expression.
subExpressions
    :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions :: forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions = forall (f :: * -> *) a s b.
Applicative f =>
(a -> f (Expr s b))
-> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
subExpressionsWith (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. a -> Expr s a
Embed)
{-# INLINABLE subExpressions #-}

{-| A traversal over the immediate sub-expressions of an expression which
    allows mapping embedded values
-}
subExpressionsWith
    :: Applicative f => (a -> f (Expr s b)) -> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
subExpressionsWith :: forall (f :: * -> *) a s b.
Applicative f =>
(a -> f (Expr s b))
-> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
subExpressionsWith a -> f (Expr s b)
h Expr s a -> f (Expr s b)
_ (Embed a
a) = a -> f (Expr s b)
h a
a
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (Note s
a Expr s a
b) = forall s a. s -> Expr s a -> Expr s a
Note s
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr s b)
f Expr s a
b
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (Let Binding s a
a Expr s a
b) = forall s a. Binding s a -> Expr s a -> Expr s a
Let forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) s a b.
Applicative f =>
(Expr s a -> f (Expr s b)) -> Binding s a -> f (Binding s b)
bindingExprs Expr s a -> f (Expr s b)
f Binding s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr s b)
f Expr s a
b
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (Record Map Text (RecordField s a)
a) = forall s a. Map Text (RecordField s a) -> Expr s a
Record forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (f :: * -> *) s a b.
Applicative f =>
(Expr s a -> f (Expr s b))
-> RecordField s a -> f (RecordField s b)
recordFieldExprs Expr s a -> f (Expr s b)
f) Map Text (RecordField s a)
a
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (RecordLit Map Text (RecordField s a)
a) = forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (f :: * -> *) s a b.
Applicative f =>
(Expr s a -> f (Expr s b))
-> RecordField s a -> f (RecordField s b)
recordFieldExprs Expr s a -> f (Expr s b)
f) Map Text (RecordField s a)
a
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (Lam Maybe CharacterSet
cs FunctionBinding s a
fb Expr s a
e) = forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam Maybe CharacterSet
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) s a b.
Applicative f =>
(Expr s a -> f (Expr s b))
-> FunctionBinding s a -> f (FunctionBinding s b)
functionBindingExprs Expr s a -> f (Expr s b)
f FunctionBinding s a
fb forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr s b)
f Expr s a
e
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f (Field Expr s a
a FieldSelection s
b) = forall s a. Expr s a -> FieldSelection s -> Expr s a
Field forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr s b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure FieldSelection s
b
subExpressionsWith a -> f (Expr s b)
_ Expr s a -> f (Expr s b)
f Expr s a
expression = forall (f :: * -> *) s a t b.
Applicative f =>
(Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
unsafeSubExpressions Expr s a -> f (Expr s b)
f Expr s a
expression
{-# INLINABLE subExpressionsWith #-}

{-| An internal utility used to implement transformations that require changing
    one of the type variables of the `Expr` type

    This utility only works because the implementation is partial, not
    handling the `Let`, `Note`, or `Embed` cases, which need to be handled by
    the caller.
-}
unsafeSubExpressions
    :: Applicative f => (Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
unsafeSubExpressions :: forall (f :: * -> *) s a t b.
Applicative f =>
(Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Const Const
c) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Const -> Expr s a
Const Const
c)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Var Var
v) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Var -> Expr s a
Var Var
v)
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Pi Maybe CharacterSet
cs Text
a Expr s a
b Expr s a
c) = forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
cs Text
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
c
unsafeSubExpressions Expr s a -> f (Expr t b)
f (App Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Annot Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
Annot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Bool = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Bool
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (BoolLit Bool
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Bool -> Expr s a
BoolLit Bool
b)
unsafeSubExpressions Expr s a -> f (Expr t b)
f (BoolAnd Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
BoolAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (BoolOr Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
BoolOr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (BoolEQ Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
BoolEQ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (BoolNE Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
BoolNE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (BoolIf Expr s a
a Expr s a
b Expr s a
c) = forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
BoolIf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
c
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Bytes = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Bytes
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (BytesLit ByteString
a) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. ByteString -> Expr s a
BytesLit ByteString
a)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Natural = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Natural
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (NaturalLit Natural
n) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Natural -> Expr s a
NaturalLit Natural
n)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalFold = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalFold
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalBuild = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalBuild
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalIsZero = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalIsZero
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalEven = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalEven
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalOdd = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalOdd
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalToInteger = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalToInteger
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
NaturalSubtract = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
NaturalSubtract
unsafeSubExpressions Expr s a -> f (Expr t b)
f (NaturalPlus Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
NaturalPlus forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (NaturalTimes Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
NaturalTimes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Integer = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Integer
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (IntegerLit Integer
n) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Integer -> Expr s a
IntegerLit Integer
n)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
IntegerClamp = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerClamp
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
IntegerNegate = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerNegate
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
IntegerShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
IntegerToDouble = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
IntegerToDouble
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Double = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Double
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (DoubleLit DhallDouble
n) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
DoubleShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
DoubleShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Text = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Text
unsafeSubExpressions Expr s a -> f (Expr t b)
f (TextLit Chunks s a
chunks) = forall s a. Chunks s a -> Expr s a
TextLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) s a t b.
Applicative f =>
(Expr s a -> f (Expr t b)) -> Chunks s a -> f (Chunks t b)
chunkExprs Expr s a -> f (Expr t b)
f Chunks s a
chunks
unsafeSubExpressions Expr s a -> f (Expr t b)
f (TextAppend Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
TextReplace = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TextReplace
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
TextShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TextShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Date = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Date
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (DateLiteral Day
a) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. Day -> Expr s a
DateLiteral Day
a)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
DateShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
DateShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Time = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Time
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (TimeLiteral TimeOfDay
a Word
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. TimeOfDay -> Word -> Expr s a
TimeLiteral TimeOfDay
a Word
b)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
TimeShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
TimeZone = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeZone
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (TimeZoneLiteral TimeZone
a) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s a. TimeZone -> Expr s a
TimeZoneLiteral TimeZone
a)
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
TimeZoneShow = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
TimeZoneShow
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
List = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
List
unsafeSubExpressions Expr s a -> f (Expr t b)
f (ListLit Maybe (Expr s a)
a Seq (Expr s a)
b) = forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f Maybe (Expr s a)
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f Seq (Expr s a)
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (ListAppend Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
ListAppend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListBuild = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListBuild
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListFold = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListFold
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListLength = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListLength
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListHead = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListHead
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListLast = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListLast
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListIndexed = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListIndexed
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
ListReverse = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
ListReverse
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
Optional = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
Optional
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Some Expr s a
a) = forall s a. Expr s a -> Expr s a
Some forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a
unsafeSubExpressions Expr s a -> f (Expr t b)
_ Expr s a
None = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall s a. Expr s a
None
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Union Map Text (Maybe (Expr s a))
a) = forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f) Map Text (Maybe (Expr s a))
a
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Combine Maybe CharacterSet
cs Maybe Text
a Expr s a
b Expr s a
c) = forall s a.
Maybe CharacterSet
-> Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine Maybe CharacterSet
cs Maybe Text
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
c
unsafeSubExpressions Expr s a -> f (Expr t b)
f (CombineTypes Maybe CharacterSet
cs Expr s a
a Expr s a
b) = forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
CombineTypes Maybe CharacterSet
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Prefer Maybe CharacterSet
cs PreferAnnotation
a Expr s a
b Expr s a
c) = forall s a.
Maybe CharacterSet
-> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
Prefer Maybe CharacterSet
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure PreferAnnotation
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
c
unsafeSubExpressions Expr s a -> f (Expr t b)
f (RecordCompletion Expr s a
a Expr s a
b) = forall s a. Expr s a -> Expr s a -> Expr s a
RecordCompletion forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Merge Expr s a
a Expr s a
b Maybe (Expr s a)
t) = forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f Maybe (Expr s a)
t
unsafeSubExpressions Expr s a -> f (Expr t b)
f (ToMap Expr s a
a Maybe (Expr s a)
t) = forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
ToMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f Maybe (Expr s a)
t
unsafeSubExpressions Expr s a -> f (Expr t b)
f (ShowConstructor Expr s a
a) = forall s a. Expr s a -> Expr s a
ShowConstructor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Project Expr s a
a Either [Text] (Expr s a)
b) = forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
Project forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr s a -> f (Expr t b)
f Either [Text] (Expr s a)
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Assert Expr s a
a) = forall s a. Expr s a -> Expr s a
Assert forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a
unsafeSubExpressions Expr s a -> f (Expr t b)
f (Equivalent Maybe CharacterSet
cs Expr s a
a Expr s a
b) = forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
Equivalent Maybe CharacterSet
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
b
unsafeSubExpressions Expr s a -> f (Expr t b)
f (With Expr s a
a NonEmpty WithComponent
b Expr s a
c) = forall s a.
Expr s a -> NonEmpty WithComponent -> Expr s a -> Expr s a
With forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure NonEmpty WithComponent
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
c
unsafeSubExpressions Expr s a -> f (Expr t b)
f (ImportAlt Expr s a
l Expr s a
r) = forall s a. Expr s a -> Expr s a -> Expr s a
ImportAlt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr s a -> f (Expr t b)
f Expr s a
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr s a -> f (Expr t b)
f Expr s a
r
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Let {}) = forall a. Text -> a
unhandledConstructor Text
"Let"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Note {}) = forall a. Text -> a
unhandledConstructor Text
"Note"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Embed {}) = forall a. Text -> a
unhandledConstructor Text
"Embed"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Record {}) = forall a. Text -> a
unhandledConstructor Text
"Record"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (RecordLit {}) = forall a. Text -> a
unhandledConstructor Text
"RecordLit"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Lam {}) = forall a. Text -> a
unhandledConstructor Text
"Lam"
unsafeSubExpressions Expr s a -> f (Expr t b)
_ (Field {}) = forall a. Text -> a
unhandledConstructor Text
"Field"
{-# INLINABLE unsafeSubExpressions #-}

unhandledConstructor :: Text -> a
unhandledConstructor :: forall a. Text -> a
unhandledConstructor Text
constructor =
    Text -> forall b. b
internalError
        (   Text
"Dhall.Syntax.unsafeSubExpressions: Unhandled "
        forall a. Semigroup a => a -> a -> a
<>  Text
constructor
        forall a. Semigroup a => a -> a -> a
<>  Text
" construtor"
        )

-- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)
--
-- This also remove CharacterSet annotations.
denote :: Expr s a -> Expr t a
denote :: forall s a t. Expr s a -> Expr t a
denote = \case
    Note s
_ Expr s a
b -> forall s a t. Expr s a -> Expr t a
denote Expr s a
b
    Let Binding s a
a Expr s a
b -> forall s a. Binding s a -> Expr s a -> Expr s a
Let (forall {s} {a} {s}. Binding s a -> Binding s a
denoteBinding Binding s a
a) (forall s a t. Expr s a -> Expr t a
denote Expr s a
b)
    Embed a
a -> forall s a. a -> Expr s a
Embed a
a
    Combine Maybe CharacterSet
_ Maybe Text
_ Expr s a
b Expr s a
c -> forall s a.
Maybe CharacterSet
-> Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine forall a. Maybe a
Nothing forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
b) (forall s a t. Expr s a -> Expr t a
denote Expr s a
c)
    CombineTypes Maybe CharacterSet
_ Expr s a
b Expr s a
c -> forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
CombineTypes forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
b) (forall s a t. Expr s a -> Expr t a
denote Expr s a
c)
    Prefer Maybe CharacterSet
_ PreferAnnotation
a Expr s a
b Expr s a
c -> forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.over forall (f :: * -> *) s a t b.
Applicative f =>
(Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
unsafeSubExpressions forall s a t. Expr s a -> Expr t a
denote forall a b. (a -> b) -> a -> b
$ forall s a.
Maybe CharacterSet
-> PreferAnnotation -> Expr s a -> Expr s a -> Expr s a
Prefer forall a. Maybe a
Nothing PreferAnnotation
a Expr s a
b Expr s a
c
    Record Map Text (RecordField s a)
a -> forall s a. Map Text (RecordField s a) -> Expr s a
Record forall a b. (a -> b) -> a -> b
$ forall {s} {a} {s}. RecordField s a -> RecordField s a
denoteRecordField forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField s a)
a
    RecordLit Map Text (RecordField s a)
a -> forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit forall a b. (a -> b) -> a -> b
$ forall {s} {a} {s}. RecordField s a -> RecordField s a
denoteRecordField forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField s a)
a
    Lam Maybe CharacterSet
_ FunctionBinding s a
a Expr s a
b -> forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam forall a. Maybe a
Nothing (forall {s} {a} {s}. FunctionBinding s a -> FunctionBinding s a
denoteFunctionBinding FunctionBinding s a
a) (forall s a t. Expr s a -> Expr t a
denote Expr s a
b)
    Pi Maybe CharacterSet
_ Text
t Expr s a
a Expr s a
b -> forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi forall a. Maybe a
Nothing Text
t (forall s a t. Expr s a -> Expr t a
denote Expr s a
a) (forall s a t. Expr s a -> Expr t a
denote Expr s a
b)
    Field Expr s a
a (FieldSelection Maybe s
_ Text
b Maybe s
_) -> forall s a. Expr s a -> FieldSelection s -> Expr s a
Field (forall s a t. Expr s a -> Expr t a
denote Expr s a
a) (forall s. Maybe s -> Text -> Maybe s -> FieldSelection s
FieldSelection forall a. Maybe a
Nothing Text
b forall a. Maybe a
Nothing)
    Equivalent Maybe CharacterSet
_ Expr s a
a Expr s a
b -> forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
Equivalent forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
a) (forall s a t. Expr s a -> Expr t a
denote Expr s a
b)
    Expr s a
expression -> forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.over forall (f :: * -> *) s a t b.
Applicative f =>
(Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
unsafeSubExpressions forall s a t. Expr s a -> Expr t a
denote Expr s a
expression
  where
    denoteRecordField :: RecordField s a -> RecordField s a
denoteRecordField (RecordField Maybe s
_ Expr s a
e Maybe s
_ Maybe s
_) = forall s a.
Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
RecordField forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
e) forall a. Maybe a
Nothing forall a. Maybe a
Nothing

    denoteBinding :: Binding s a -> Binding s a
denoteBinding (Binding Maybe s
_ Text
c Maybe s
_ Maybe (Maybe s, Expr s a)
d Maybe s
_ Expr s a
e) =
        forall s a.
Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
Binding forall a. Maybe a
Nothing Text
c forall a. Maybe a
Nothing (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {s} {a} {a} {t}. (a, Expr s a) -> (Maybe a, Expr t a)
denoteBindingAnnotation Maybe (Maybe s, Expr s a)
d) forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
e)

    denoteBindingAnnotation :: (a, Expr s a) -> (Maybe a, Expr t a)
denoteBindingAnnotation (a
_, Expr s a
f) = (forall a. Maybe a
Nothing, forall s a t. Expr s a -> Expr t a
denote Expr s a
f)

    denoteFunctionBinding :: FunctionBinding s a -> FunctionBinding s a
denoteFunctionBinding (FunctionBinding Maybe s
_ Text
l Maybe s
_ Maybe s
_ Expr s a
t) =
        forall s a.
Maybe s
-> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
FunctionBinding forall a. Maybe a
Nothing Text
l forall a. Maybe a
Nothing forall a. Maybe a
Nothing (forall s a t. Expr s a -> Expr t a
denote Expr s a
t)

-- | The \"opposite\" of `denote`, like @first absurd@ but faster
renote :: Expr Void a -> Expr s a
renote :: forall a s. Expr Void a -> Expr s a
renote = forall a b. a -> b
unsafeCoerce
{-# INLINE renote #-}

{-| Remove any outermost `Note` constructors

    This is typically used when you want to get the outermost non-`Note`
    constructor without removing internal `Note` constructors
-}
shallowDenote :: Expr s a -> Expr s a
shallowDenote :: forall s a. Expr s a -> Expr s a
shallowDenote (Note s
_ Expr s a
e) = forall s a. Expr s a -> Expr s a
shallowDenote Expr s a
e
shallowDenote         Expr s a
e  = Expr s a
e

-- | The set of reserved keywords according to the @keyword@ rule in the grammar
reservedKeywords :: HashSet Text
reservedKeywords :: HashSet Text
reservedKeywords =
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
Data.HashSet.fromList
        [ Text
"if"
        , Text
"then"
        , Text
"else"
        , Text
"let"
        , Text
"in"
        , Text
"using"
        , Text
"missing"
        , Text
"as"
        , Text
"Infinity"
        , Text
"NaN"
        , Text
"merge"
        , Text
"Some"
        , Text
"toMap"
        , Text
"assert"
        , Text
"forall"
        , Text
"with"
        ]

-- | The set of reserved identifiers for the Dhall language
-- | Contains also all keywords from "reservedKeywords"
reservedIdentifiers :: HashSet Text
reservedIdentifiers :: HashSet Text
reservedIdentifiers = HashSet Text
reservedKeywords forall a. Semigroup a => a -> a -> a
<>
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
Data.HashSet.fromList
        [ -- Builtins according to the `builtin` rule in the grammar
          Text
"Natural/fold"
        , Text
"Natural/build"
        , Text
"Natural/isZero"
        , Text
"Natural/even"
        , Text
"Natural/odd"
        , Text
"Natural/toInteger"
        , Text
"Natural/show"
        , Text
"Natural/subtract"
        , Text
"Integer"
        , Text
"Integer/clamp"
        , Text
"Integer/negate"
        , Text
"Integer/show"
        , Text
"Integer/toDouble"
        , Text
"Integer/show"
        , Text
"Natural/subtract"
        , Text
"Double/show"
        , Text
"List/build"
        , Text
"List/fold"
        , Text
"List/length"
        , Text
"List/head"
        , Text
"List/last"
        , Text
"List/indexed"
        , Text
"List/reverse"
        , Text
"Text/replace"
        , Text
"Text/show"
        , Text
"Date/show"
        , Text
"Time/show"
        , Text
"TimeZone/show"
        , Text
"Bool"
        , Text
"Bytes"
        , Text
"True"
        , Text
"False"
        , Text
"Optional"
        , Text
"None"
        , Text
"Natural"
        , Text
"Integer"
        , Text
"Double"
        , Text
"Text"
        , Text
"Date"
        , Text
"Time"
        , Text
"TimeZone"
        , Text
"List"
        , Text
"Type"
        , Text
"Kind"
        , Text
"Sort"
        ]

{-| `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 :: forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d (V Text
x Int
n) (Var (V Text
x' Int
n')) = forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
x' Int
n'')
  where
    n'' :: Int
n'' = if Text
x forall a. Eq a => a -> a -> Bool
== Text
x' Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
<= Int
n' then Int
n' forall a. Num a => a -> a -> a
+ Int
d else Int
n'
shift Int
d (V Text
x Int
n) (Lam Maybe CharacterSet
cs (FunctionBinding Maybe s
src0 Text
x' Maybe s
src1 Maybe s
src2 Expr s a
_A) Expr s a
b) =
    forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam Maybe CharacterSet
cs (forall s a.
Maybe s
-> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
FunctionBinding Maybe s
src0 Text
x' Maybe s
src1 Maybe s
src2 Expr s a
_A') Expr s a
b'
  where
    _A' :: Expr s a
_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'  = 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 forall a. Eq a => a -> a -> Bool
== Text
x' then Int
n forall a. Num a => a -> a -> a
+ Int
1 else Int
n
shift Int
d (V Text
x Int
n) (Pi Maybe CharacterSet
cs Text
x' Expr s a
_A Expr s a
_B) = forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
cs Text
x' Expr s a
_A' Expr s a
_B'
  where
    _A' :: Expr s a
_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' = 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 forall a. Eq a => a -> a -> Bool
== Text
x' then Int
n forall a. Num a => a -> a -> a
+ Int
1 else Int
n
shift Int
d (V Text
x Int
n) (Let (Binding Maybe s
src0 Text
f Maybe s
src1 Maybe (Maybe s, Expr s a)
mt Maybe s
src2 Expr s a
r) Expr s a
e) =
    forall s a. Binding s a -> Expr s a -> Expr s a
Let (forall s a.
Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
Binding Maybe s
src0 Text
f Maybe s
src1 Maybe (Maybe s, Expr s a)
mt' Maybe s
src2 Expr s a
r') Expr s a
e'
  where
    e' :: Expr s a
e' = 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 forall a. Eq a => a -> a -> Bool
== Text
f then Int
n forall a. Num a => a -> a -> a
+ Int
1 else Int
n

    mt' :: Maybe (Maybe s, Expr s a)
mt' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall s a. 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'  =             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 Int
d Var
v Expr s a
expression = forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.over forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions (forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
d Var
v) Expr s a
expression

_ERROR :: String
_ERROR :: String
_ERROR = String
"\ESC[1;31mError\ESC[0m"

{-| Utility function used to throw internal errors that should never happen
    (in theory) but that are not enforced by the type system
-}
internalError :: Data.Text.Text -> forall b . b
internalError :: Text -> forall b. b
internalError Text
text = forall a. HasCallStack => String -> a
error ([String] -> String
unlines
    [ String
_ERROR forall a. Semigroup a => a -> a -> a
<> String
": Compiler bug                                                        "
    , String
"                                                                                "
    , String
"Explanation: This error message means that there is a bug in the Dhall compiler."
    , String
"You didn't do anything wrong, but if you would like to see this problem fixed   "
    , String
"then you should report the bug at:                                              "
    , String
"                                                                                "
    , String
"https://github.com/dhall-lang/dhall-haskell/issues                              "
    , String
"                                                                                "
    , String
"Please include the following text in your bug report:                           "
    , String
"                                                                                "
    , String
"```                                                                             "
    , Text -> String
Data.Text.unpack Text
text forall a. Semigroup a => a -> a -> a
<> String
"                                                       "
    , String
"```                                                                             "
    ] )