{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE PatternSynonyms      #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns         #-}

{-# OPTIONS_GHC -O #-}

{-| Eval-apply environment machine with conversion checking and quoting to
    normal forms. Fairly similar to GHCI's STG machine algorithmically, but much
    simpler, with no known call optimization or environment trimming.

    Potential optimizations without changing Expr:

    * In conversion checking, get non-shadowing variables not by linear
      Env-walking, but by keeping track of Env size, and generating names which
      are known to be illegal as source-level names (to rule out shadowing).

    * Use HashMap Text chunks for large let-definitions blocks. "Large" vs
      "Small" is fairly cheap to determine at evaluation time.

    Potential optimizations with changing Expr:

    * Use actual full de Bruijn indices in Var instead of Text counting indices.
      Then, we'd switch to full de Bruijn levels in Val as well, and use proper
      constant time non-shadowing name generation.
-}

module Dhall.Eval (
    judgmentallyEqual
  , normalize
  , alphaNormalize
  , eval
  , quote
  , envNames
  , countNames
  , conv
  , toVHPi
  , Closure(..)
  , Names(..)
  , Environment(..)
  , Val(..)
  , (~>)
  , textShow
  ) where

import Data.Bifunctor     (first)
import Data.Foldable      (foldr', toList)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Sequence      (Seq, ViewL (..), ViewR (..))
import Data.Text          (Text)
import Data.Void          (Void)
import Dhall.Map          (Map)
import Dhall.Set          (Set)
import GHC.Natural        (Natural)
import Prelude            hiding (succ)

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

import qualified Data.Char
import qualified Data.Sequence as Sequence
import qualified Data.Set
import qualified Data.Text     as Text
import qualified Dhall.Map     as Map
import qualified Dhall.Set
import qualified Dhall.Syntax  as Syntax
import qualified Text.Printf

data Environment a
    = Empty
    | Skip   !(Environment a) {-# UNPACK #-} !Text
    | Extend !(Environment a) {-# UNPACK #-} !Text (Val a)

deriving instance (Show a, Show (Val a -> Val a)) => Show (Environment a)

errorMsg :: String
errorMsg :: String
errorMsg = [String] -> String
unlines
  [ String
_ERROR String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
": Compiler bug                                                        "
  , String
"                                                                                "
  , String
"An ill-typed expression was encountered during normalization.                   "
  , 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                              "
  ]
  where
    _ERROR :: String
    _ERROR :: String
_ERROR = String
"\ESC[1;31mError\ESC[0m"


data Closure a = Closure !Text !(Environment a) !(Expr Void a)

deriving instance (Show a, Show (Val a -> Val a)) => Show (Closure a)

data VChunks a = VChunks ![(Text, Val a)] !Text

deriving instance (Show a, Show (Val a -> Val a)) => Show (VChunks a)

instance Semigroup (VChunks a) where
  VChunks [(Text, Val a)]
xys Text
z <> :: VChunks a -> VChunks a -> VChunks a
<> VChunks [] Text
z' = [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [(Text, Val a)]
xys (Text
z Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
z')
  VChunks [(Text, Val a)]
xys Text
z <> VChunks ((Text
x', Val a
y'):[(Text, Val a)]
xys') Text
z' = [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks ([(Text, Val a)]
xys [(Text, Val a)] -> [(Text, Val a)] -> [(Text, Val a)]
forall a. [a] -> [a] -> [a]
++ (Text
z Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x', Val a
y')(Text, Val a) -> [(Text, Val a)] -> [(Text, Val a)]
forall a. a -> [a] -> [a]
:[(Text, Val a)]
xys') Text
z'

instance Monoid (VChunks a) where
  mempty :: VChunks a
mempty = [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
forall a. Monoid a => a
mempty

{-| Some information is lost when `eval` converts a `Lam` or a built-in function
    from the `Expr` type to a `VHLam` of the `Val` type and `quote` needs that
    information in order to reconstruct an equivalent `Expr`.  This `HLamInfo`
    type holds that extra information necessary to perform that reconstruction
-}
data HLamInfo a
  = Prim
  -- ^ Don't store any information
  | Typed !Text (Val a)
  -- ^ Store the original name and type of the variable bound by the `Lam`
  | NaturalSubtractZero
  -- ^ The original function was a @Natural/subtract 0@.  We need to preserve
  --   this information in case the @Natural/subtract@ ends up not being fully
  --   saturated, in which case we need to recover the unsaturated built-in

deriving instance (Show a, Show (Val a -> Val a)) => Show (HLamInfo a)

pattern VPrim :: (Val a -> Val a) -> Val a
pattern $bVPrim :: (Val a -> Val a) -> Val a
$mVPrim :: forall r a. Val a -> ((Val a -> Val a) -> r) -> (Void# -> r) -> r
VPrim f = VHLam Prim f

toVHPi :: Eq a => Val a -> Maybe (Text, Val a, Val a -> Val a)
toVHPi :: Val a -> Maybe (Text, Val a, Val a -> Val a)
toVHPi (VPi Val a
a b :: Closure a
b@(Closure Text
x Environment a
_ Expr Void a
_)) = (Text, Val a, Val a -> Val a)
-> Maybe (Text, Val a, Val a -> Val a)
forall a. a -> Maybe a
Just (Text
x, Val a
a, Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b)
toVHPi (VHPi Text
x Val a
a Val a -> Val a
b             ) = (Text, Val a, Val a -> Val a)
-> Maybe (Text, Val a, Val a -> Val a)
forall a. a -> Maybe a
Just (Text
x, Val a
a, Val a -> Val a
b)
toVHPi  Val a
_                        = Maybe (Text, Val a, Val a -> Val a)
forall a. Maybe a
Nothing

data Val a
    = VConst !Const
    | VVar !Text !Int
    | VPrimVar
    | VApp !(Val a) !(Val a)

    | VLam (Val a) {-# UNPACK #-} !(Closure a)
    | VHLam !(HLamInfo a) !(Val a -> Val a)

    | VPi (Val a) {-# UNPACK #-} !(Closure a)
    | VHPi !Text (Val a) !(Val a -> Val a)

    | VBool
    | VBoolLit !Bool
    | VBoolAnd !(Val a) !(Val a)
    | VBoolOr !(Val a) !(Val a)
    | VBoolEQ !(Val a) !(Val a)
    | VBoolNE !(Val a) !(Val a)
    | VBoolIf !(Val a) !(Val a) !(Val a)

    | VNatural
    | VNaturalLit !Natural
    | VNaturalFold !(Val a) !(Val a) !(Val a) !(Val a)
    | VNaturalBuild !(Val a)
    | VNaturalIsZero !(Val a)
    | VNaturalEven !(Val a)
    | VNaturalOdd !(Val a)
    | VNaturalToInteger !(Val a)
    | VNaturalShow !(Val a)
    | VNaturalSubtract !(Val a) !(Val a)
    | VNaturalPlus !(Val a) !(Val a)
    | VNaturalTimes !(Val a) !(Val a)

    | VInteger
    | VIntegerLit !Integer
    | VIntegerClamp !(Val a)
    | VIntegerNegate !(Val a)
    | VIntegerShow !(Val a)
    | VIntegerToDouble !(Val a)

    | VDouble
    | VDoubleLit !DhallDouble
    | VDoubleShow !(Val a)

    | VText
    | VTextLit !(VChunks a)
    | VTextAppend !(Val a) !(Val a)
    | VTextShow !(Val a)
    | VTextReplace !(Val a) !(Val a) !(Val a)

    | VList !(Val a)
    | VListLit !(Maybe (Val a)) !(Seq (Val a))
    | VListAppend !(Val a) !(Val a)
    | VListBuild   (Val a) !(Val a)
    | VListFold    (Val a) !(Val a) !(Val a) !(Val a) !(Val a)
    | VListLength  (Val a) !(Val a)
    | VListHead    (Val a) !(Val a)
    | VListLast    (Val a) !(Val a)
    | VListIndexed (Val a) !(Val a)
    | VListReverse (Val a) !(Val a)

    | VOptional (Val a)
    | VSome (Val a)
    | VNone (Val a)
    | VRecord !(Map Text (Val a))
    | VRecordLit !(Map Text (Val a))
    | VUnion !(Map Text (Maybe (Val a)))
    | VCombine !(Maybe Text) !(Val a) !(Val a)
    | VCombineTypes !(Val a) !(Val a)
    | VPrefer !(Val a) !(Val a)
    | VMerge !(Val a) !(Val a) !(Maybe (Val a))
    | VToMap !(Val a) !(Maybe (Val a))
    | VField !(Val a) !Text
    | VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
    | VProject !(Val a) !(Either (Set Text) (Val a))
    | VAssert !(Val a)
    | VEquivalent !(Val a) !(Val a)
    | VWith !(Val a) (NonEmpty Text) !(Val a)
    | VEmbed a

-- | For use with "Text.Show.Functions".
deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a)

(~>) :: Val a -> Val a -> Val a
~> :: Val a -> Val a -> Val a
(~>) Val a
a Val a
b = Text -> Val a -> (Val a -> Val a) -> Val a
forall a. Text -> Val a -> (Val a -> Val a) -> Val a
VHPi Text
"_" Val a
a (\Val a
_ -> Val a
b)
{-# INLINE (~>) #-}

infixr 5 ~>

countEnvironment :: Text -> Environment a -> Int
countEnvironment :: Text -> Environment a -> Int
countEnvironment Text
x = Int -> Environment a -> Int
forall a a. Num a => a -> Environment a -> a
go (Int
0 :: Int)
  where
    go :: a -> Environment a -> a
go !a
acc Environment a
Empty             = a
acc
    go  a
acc (Skip Environment a
env Text
x'    ) = a -> Environment a -> a
go (if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' then a
acc a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 else a
acc) Environment a
env
    go  a
acc (Extend Environment a
env Text
x' Val a
_) = a -> Environment a -> a
go (if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' then a
acc a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 else a
acc) Environment a
env

instantiate :: Eq a => Closure a -> Val a -> Val a
instantiate :: Closure a -> Val a -> Val a
instantiate (Closure Text
x Environment a
env Expr Void a
t) !Val a
u = Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval (Environment a -> Text -> Val a -> Environment a
forall a. Environment a -> Text -> Val a -> Environment a
Extend Environment a
env Text
x Val a
u) Expr Void a
t
{-# INLINE instantiate #-}

-- Out-of-env variables have negative de Bruijn levels.
vVar :: Environment a -> Var -> Val a
vVar :: Environment a -> Var -> Val a
vVar Environment a
env0 (V Text
x Int
i0) = Environment a -> Int -> Val a
forall a. Environment a -> Int -> Val a
go Environment a
env0 Int
i0
  where
    go :: Environment a -> Int -> Val a
go (Extend Environment a
env Text
x' Val a
v) Int
i
        | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' =
            if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Val a
v else Environment a -> Int -> Val a
go Environment a
env (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        | Bool
otherwise =
            Environment a -> Int -> Val a
go Environment a
env Int
i
    go (Skip Environment a
env Text
x') Int
i
        | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' =
            if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Text -> Int -> Val a
forall a. Text -> Int -> Val a
VVar Text
x (Text -> Environment a -> Int
forall a. Text -> Environment a -> Int
countEnvironment Text
x Environment a
env) else Environment a -> Int -> Val a
go Environment a
env (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        | Bool
otherwise =
            Environment a -> Int -> Val a
go Environment a
env Int
i
    go Environment a
Empty Int
i =
        Text -> Int -> Val a
forall a. Text -> Int -> Val a
VVar Text
x (Int -> Int
forall a. Num a => a -> a
negate Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

vApp :: Eq a => Val a -> Val a -> Val a
vApp :: Val a -> Val a -> Val a
vApp !Val a
t !Val a
u =
    case Val a
t of
        VLam Val a
_ Closure a
t'  -> Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t' Val a
u
        VHLam HLamInfo a
_ Val a -> Val a
t' -> Val a -> Val a
t' Val a
u
        Val a
t'        -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VApp Val a
t' Val a
u
{-# INLINE vApp #-}

vPrefer :: Eq a => Environment a -> Val a -> Val a -> Val a
vPrefer :: Environment a -> Val a -> Val a -> Val a
vPrefer Environment a
env Val a
t Val a
u =
    case (Val a
t, Val a
u) of
        (VRecordLit Map Text (Val a)
m, Val a
u') | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
u'
        (Val a
t', VRecordLit Map Text (Val a)
m) | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
t'
        (VRecordLit Map Text (Val a)
m, VRecordLit Map Text (Val a)
m') ->
            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit (Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
forall k v. Ord k => Map k v -> Map k v -> Map k v
Map.union Map Text (Val a)
m' Map Text (Val a)
m)
        (Val a
t', Val a
u') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
u' ->
            Val a
t'
        (Val a
t', Val a
u') ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VPrefer Val a
t' Val a
u'
{-# INLINE vPrefer #-}

vCombine :: Maybe Text -> Val a -> Val a -> Val a
vCombine :: Maybe Text -> Val a -> Val a -> Val a
vCombine Maybe Text
mk Val a
t Val a
u =
    case (Val a
t, Val a
u) of
        (VRecordLit Map Text (Val a)
m, Val a
u') | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
u'
        (Val a
t', VRecordLit Map Text (Val a)
m) | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
t'
        (VRecordLit Map Text (Val a)
m, VRecordLit Map Text (Val a)
m') ->
            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit ((Val a -> Val a -> Val a)
-> Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Map.unionWith (Maybe Text -> Val a -> Val a -> Val a
forall a. Maybe Text -> Val a -> Val a -> Val a
vCombine Maybe Text
forall a. Maybe a
Nothing) Map Text (Val a)
m Map Text (Val a)
m')
        (Val a
t', Val a
u') ->
            Maybe Text -> Val a -> Val a -> Val a
forall a. Maybe Text -> Val a -> Val a -> Val a
VCombine Maybe Text
mk Val a
t' Val a
u'

vCombineTypes :: Val a -> Val a -> Val a
vCombineTypes :: Val a -> Val a -> Val a
vCombineTypes Val a
t Val a
u =
    case (Val a
t, Val a
u) of
        (VRecord Map Text (Val a)
m, Val a
u') | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
u'
        (Val a
t', VRecord Map Text (Val a)
m) | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
            Val a
t'
        (VRecord Map Text (Val a)
m, VRecord Map Text (Val a)
m') ->
            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecord ((Val a -> Val a -> Val a)
-> Map Text (Val a) -> Map Text (Val a) -> Map Text (Val a)
forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
Map.unionWith Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vCombineTypes Map Text (Val a)
m Map Text (Val a)
m')
        (Val a
t', Val a
u') ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VCombineTypes Val a
t' Val a
u'

vListAppend :: Val a -> Val a -> Val a
vListAppend :: Val a -> Val a -> Val a
vListAppend Val a
t Val a
u =
    case (Val a
t, Val a
u) of
        (VListLit Maybe (Val a)
_ Seq (Val a)
xs, Val a
u') | Seq (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Val a)
xs ->
            Val a
u'
        (Val a
t', VListLit Maybe (Val a)
_ Seq (Val a)
ys) | Seq (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Val a)
ys ->
            Val a
t'
        (VListLit Maybe (Val a)
t' Seq (Val a)
xs, VListLit Maybe (Val a)
_ Seq (Val a)
ys) ->
            Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
t' (Seq (Val a)
xs Seq (Val a) -> Seq (Val a) -> Seq (Val a)
forall a. Semigroup a => a -> a -> a
<> Seq (Val a)
ys)
        (Val a
t', Val a
u') ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListAppend Val a
t' Val a
u'
{-# INLINE vListAppend #-}

vNaturalPlus :: Val a -> Val a -> Val a
vNaturalPlus :: Val a -> Val a -> Val a
vNaturalPlus Val a
t Val a
u =
    case (Val a
t, Val a
u) of
        (VNaturalLit Natural
0, Val a
u') ->
            Val a
u'
        (Val a
t', VNaturalLit Natural
0) ->
            Val a
t'
        (VNaturalLit Natural
m, VNaturalLit Natural
n) ->
            Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n)
        (Val a
t', Val a
u') ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalPlus Val a
t' Val a
u'
{-# INLINE vNaturalPlus #-}

vField :: Val a -> Text -> Val a
vField :: Val a -> Text -> Val a
vField Val a
t0 Text
k = Val a -> Val a
forall a. Val a -> Val a
go Val a
t0
  where
    go :: Val a -> Val a
go = \case
        VUnion Map Text (Maybe (Val a))
m -> case Text -> Map Text (Maybe (Val a)) -> Maybe (Maybe (Val a))
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Maybe (Val a))
m of
            Just (Just Val a
_) -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ ~Val a
u -> Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
forall a.
Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
VInject Map Text (Maybe (Val a))
m Text
k (Val a -> Maybe (Val a)
forall a. a -> Maybe a
Just Val a
u)
            Just Maybe (Val a)
Nothing  -> Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
forall a.
Map Text (Maybe (Val a)) -> Text -> Maybe (Val a) -> Val a
VInject Map Text (Maybe (Val a))
m Text
k Maybe (Val a)
forall a. Maybe a
Nothing
            Maybe (Maybe (Val a))
_             -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
        VRecordLit Map Text (Val a)
m
            | Just Val a
v <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m -> Val a
v
            | Bool
otherwise -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
        VProject Val a
t Either (Set Text) (Val a)
_ -> Val a -> Val a
go Val a
t
        VPrefer (VRecordLit Map Text (Val a)
m) Val a
r -> case Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m of
            Just Val a
v -> Val a -> Text -> Val a
forall a. Val a -> Text -> Val a
VField (Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VPrefer (Val a -> Val a
forall a. Val a -> Val a
singletonVRecordLit Val a
v) Val a
r) Text
k
            Maybe (Val a)
Nothing -> Val a -> Val a
go Val a
r
        VPrefer Val a
l (VRecordLit Map Text (Val a)
m) -> case Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m of
            Just Val a
v -> Val a
v
            Maybe (Val a)
Nothing -> Val a -> Val a
go Val a
l
        VCombine Maybe Text
mk (VRecordLit Map Text (Val a)
m) Val a
r -> case Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m of
            Just Val a
v -> Val a -> Text -> Val a
forall a. Val a -> Text -> Val a
VField (Maybe Text -> Val a -> Val a -> Val a
forall a. Maybe Text -> Val a -> Val a -> Val a
VCombine Maybe Text
mk (Val a -> Val a
forall a. Val a -> Val a
singletonVRecordLit Val a
v) Val a
r) Text
k
            Maybe (Val a)
Nothing -> Val a -> Val a
go Val a
r
        VCombine Maybe Text
mk Val a
l (VRecordLit Map Text (Val a)
m) -> case Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m of
            Just Val a
v -> Val a -> Text -> Val a
forall a. Val a -> Text -> Val a
VField (Maybe Text -> Val a -> Val a -> Val a
forall a. Maybe Text -> Val a -> Val a -> Val a
VCombine Maybe Text
mk Val a
l (Val a -> Val a
forall a. Val a -> Val a
singletonVRecordLit Val a
v)) Text
k
            Maybe (Val a)
Nothing -> Val a -> Val a
go Val a
l
        Val a
t -> Val a -> Text -> Val a
forall a. Val a -> Text -> Val a
VField Val a
t Text
k

    singletonVRecordLit :: Val a -> Val a
singletonVRecordLit Val a
v = Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit (Text -> Val a -> Map Text (Val a)
forall k v. k -> v -> Map k v
Map.singleton Text
k Val a
v)
{-# INLINE vField #-}

vTextReplace :: Text -> Val a -> Text -> VChunks a
vTextReplace :: Text -> Val a -> Text -> VChunks a
vTextReplace Text
needle Val a
replacement Text
haystack = Text -> VChunks a
go Text
haystack
  where
    go :: Text -> VChunks a
go Text
t
        | Text -> Bool
Text.null Text
suffix = [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
t
        | Bool
otherwise =
            let remainder :: Text
remainder = Int -> Text -> Text
Text.drop (Text -> Int
Text.length Text
needle) Text
suffix

                rest :: VChunks a
rest = Text -> VChunks a
go Text
remainder

            in  case Val a
replacement of
                    VTextLit VChunks a
replacementChunks ->
                        [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
prefix VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
replacementChunks VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
rest
                    Val a
_ ->
                        [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [(Text
prefix, Val a
replacement)] Text
"" VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
rest
      where
        (Text
prefix, Text
suffix) = Text -> Text -> (Text, Text)
Text.breakOn Text
needle Text
t

vProjectByFields :: Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields :: Environment a -> Val a -> Set Text -> Val a
vProjectByFields Environment a
env Val a
t Set Text
ks =
    if Set Text -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Text
ks
        then Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit Map Text (Val a)
forall a. Monoid a => a
mempty
        else case Val a
t of
            VRecordLit Map Text (Val a)
kvs ->
                let kvs' :: Map Text (Val a)
kvs' = Map Text (Val a) -> Set Text -> Map Text (Val a)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map Text (Val a)
kvs (Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.toSet Set Text
ks)
                in  Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit Map Text (Val a)
kvs'
            VProject Val a
t' Either (Set Text) (Val a)
_ ->
                Environment a -> Val a -> Set Text -> Val a
forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields Environment a
env Val a
t' Set Text
ks
            VPrefer Val a
l (VRecordLit Map Text (Val a)
kvs) ->
                let ksSet :: Set Text
ksSet = Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.toSet Set Text
ks

                    kvs' :: Map Text (Val a)
kvs' = Map Text (Val a) -> Set Text -> Map Text (Val a)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map Text (Val a)
kvs Set Text
ksSet

                    ks' :: Set Text
ks' =
                        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
ksSet (Map Text (Val a) -> Set Text
forall k v. Map k v -> Set k
Map.keysSet Map Text (Val a)
kvs'))

                in  Environment a -> Val a -> Val a -> Val a
forall a. Eq a => Environment a -> Val a -> Val a -> Val a
vPrefer Environment a
env (Environment a -> Val a -> Set Text -> Val a
forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields Environment a
env Val a
l Set Text
ks') (Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit Map Text (Val a)
kvs')
            Val a
t' ->
                Val a -> Either (Set Text) (Val a) -> Val a
forall a. Val a -> Either (Set Text) (Val a) -> Val a
VProject Val a
t' (Set Text -> Either (Set Text) (Val a)
forall a b. a -> Either a b
Left Set Text
ks)

vWith :: Val a -> NonEmpty Text -> Val a -> Val a
vWith :: Val a -> NonEmpty Text -> Val a -> Val a
vWith (VRecordLit Map Text (Val a)
kvs) (Text
k  :| []     ) Val a
v = Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit (Text -> Val a -> Map Text (Val a) -> Map Text (Val a)
forall k v. Ord k => k -> v -> Map k v -> Map k v
Map.insert Text
k  Val a
v  Map Text (Val a)
kvs)
vWith (VRecordLit Map Text (Val a)
kvs) (Text
k₀ :| Text
k₁ : [Text]
ks) Val a
v = Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit (Text -> Val a -> Map Text (Val a) -> Map Text (Val a)
forall k v. Ord k => k -> v -> Map k v -> Map k v
Map.insert Text
k₀ Val a
e₂ Map Text (Val a)
kvs)
  where
    e₁ :: Val a
e₁ =
        case Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k₀ Map Text (Val a)
kvs of
            Maybe (Val a)
Nothing  -> Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit Map Text (Val a)
forall a. Monoid a => a
mempty
            Just Val a
e₁' -> Val a
e₁'

    e₂ :: Val a
e₂ = Val a -> NonEmpty Text -> Val a -> Val a
forall a. Val a -> NonEmpty Text -> Val a -> Val a
vWith Val a
e₁ (Text
k₁ Text -> [Text] -> NonEmpty Text
forall a. a -> [a] -> NonEmpty a
:| [Text]
ks) Val a
v
vWith Val a
e₀ NonEmpty Text
ks Val a
v₀ = Val a -> NonEmpty Text -> Val a -> Val a
forall a. Val a -> NonEmpty Text -> Val a -> Val a
VWith Val a
e₀ NonEmpty Text
ks Val a
v₀

eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
eval :: Environment a -> Expr Void a -> Val a
eval !Environment a
env Expr Void a
t0 =
    case Expr Void a
t0 of
        Const Const
k ->
            Const -> Val a
forall a. Const -> Val a
VConst Const
k
        Var Var
v ->
            Environment a -> Var -> Val a
forall a. Environment a -> Var -> Val a
vVar Environment a
env Var
v
        Lam Maybe CharacterSet
_ (FunctionBinding { functionBindingVariable :: forall s a. FunctionBinding s a -> Text
functionBindingVariable = Text
x, functionBindingAnnotation :: forall s a. FunctionBinding s a -> Expr s a
functionBindingAnnotation = Expr Void a
a }) Expr Void a
t ->
            Val a -> Closure a -> Val a
forall a. Val a -> Closure a -> Val a
VLam (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
a) (Text -> Environment a -> Expr Void a -> Closure a
forall a. Text -> Environment a -> Expr Void a -> Closure a
Closure Text
x Environment a
env Expr Void a
t)
        Pi Maybe CharacterSet
_ Text
x Expr Void a
a Expr Void a
b ->
            Val a -> Closure a -> Val a
forall a. Val a -> Closure a -> Val a
VPi (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
a) (Text -> Environment a -> Expr Void a -> Closure a
forall a. Text -> Environment a -> Expr Void a -> Closure a
Closure Text
x Environment a
env Expr Void a
b)
        App Expr Void a
t Expr Void a
u ->
            Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        Let (Binding Maybe Void
_ Text
x Maybe Void
_ Maybe (Maybe Void, Expr Void a)
_mA Maybe Void
_ Expr Void a
a) Expr Void a
b ->
            let !env' :: Environment a
env' = Environment a -> Text -> Val a -> Environment a
forall a. Environment a -> Text -> Val a -> Environment a
Extend Environment a
env Text
x (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
a)
            in  Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env' Expr Void a
b
        Annot Expr Void a
t Expr Void a
_ ->
            Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t
        Expr Void a
Bool ->
            Val a
forall a. Val a
VBool
        BoolLit Bool
b ->
            Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
b
        BoolAnd Expr Void a
t Expr Void a
u ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u) of
                (VBoolLit Bool
True, Val a
u')       -> Val a
u'
                (VBoolLit Bool
False, Val a
_)       -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
False
                (Val a
t', VBoolLit Bool
True)       -> Val a
t'
                (Val a
_ , VBoolLit Bool
False)      -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
False
                (Val a
t', Val a
u') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
u' -> Val a
t'
                (Val a
t', Val a
u')                  -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VBoolAnd Val a
t' Val a
u'
        BoolOr Expr Void a
t Expr Void a
u ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u) of
                (VBoolLit Bool
False, Val a
u')      -> Val a
u'
                (VBoolLit Bool
True, Val a
_)        -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
True
                (Val a
t', VBoolLit Bool
False)      -> Val a
t'
                (Val a
_ , VBoolLit Bool
True)       -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
True
                (Val a
t', Val a
u') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
u' -> Val a
t'
                (Val a
t', Val a
u')                  -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VBoolOr Val a
t' Val a
u'
        BoolEQ Expr Void a
t Expr Void a
u ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u) of
                (VBoolLit Bool
True, Val a
u')       -> Val a
u'
                (Val a
t', VBoolLit Bool
True)       -> Val a
t'
                (Val a
t', Val a
u') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
u' -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
True
                (Val a
t', Val a
u')                  -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VBoolEQ Val a
t' Val a
u'
        BoolNE Expr Void a
t Expr Void a
u ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u) of
                (VBoolLit Bool
False, Val a
u')      -> Val a
u'
                (Val a
t', VBoolLit Bool
False)      -> Val a
t'
                (Val a
t', Val a
u') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
u' -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
False
                (Val a
t', Val a
u')                  -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VBoolNE Val a
t' Val a
u'
        BoolIf Expr Void a
b Expr Void a
t Expr Void a
f ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
b, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
f) of
                (VBoolLit Bool
True,  Val a
t', Val a
_ )            -> Val a
t'
                (VBoolLit Bool
False, Val a
_ , Val a
f')            -> Val a
f'
                (Val a
b', VBoolLit Bool
True, VBoolLit Bool
False) -> Val a
b'
                (Val a
_, Val a
t', Val a
f') | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t' Val a
f'        -> Val a
t'
                (Val a
b', Val a
t', Val a
f')                        -> Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a
VBoolIf Val a
b' Val a
t' Val a
f'
        Expr Void a
Natural ->
            Val a
forall a. Val a
VNatural
        NaturalLit Natural
n ->
            Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
n
        Expr Void a
NaturalFold ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
n ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
natural ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
succ ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
zero ->
            let inert :: Val a
inert = Val a -> Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a -> Val a
VNaturalFold Val a
n Val a
natural Val a
succ Val a
zero
            in  case Val a
zero of
                Val a
VPrimVar -> Val a
inert
                Val a
_ -> case Val a
succ of
                    Val a
VPrimVar -> Val a
inert
                    Val a
_ -> case Val a
natural of
                        Val a
VPrimVar -> Val a
inert
                        Val a
_ -> case Val a
n of
                            VNaturalLit Natural
n' ->
                                -- Use an `Integer` for the loop, due to the
                                -- following issue:
                                --
                                -- https://github.com/ghcjs/ghcjs/issues/782
                                let go :: Val a -> t -> Val a
go !Val a
acc t
0 = Val a
acc
                                    go  Val a
acc t
m = Val a -> t -> Val a
go (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
succ Val a
acc) (t
m t -> t -> t
forall a. Num a => a -> a -> a
- t
1)
                                in  Val a -> Integer -> Val a
forall t. (Num t, Eq t) => Val a -> t -> Val a
go Val a
zero (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n' :: Integer)
                            Val a
_ -> Val a
inert
        Expr Void a
NaturalBuild ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                Val a
VPrimVar ->
                    Val a -> Val a
forall a. Val a -> Val a
VNaturalBuild Val a
forall a. Val a
VPrimVar
                Val a
t ->       Val a
t
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Val a
forall a. Val a
VNatural
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` HLamInfo a -> (Val a -> Val a) -> Val a
forall a. HLamInfo a -> (Val a -> Val a) -> Val a
VHLam (Text -> Val a -> HLamInfo a
forall a. Text -> Val a -> HLamInfo a
Typed Text
"n" Val a
forall a. Val a
VNatural) (\Val a
n -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vNaturalPlus Val a
n (Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
1))
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0

        Expr Void a
NaturalIsZero -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0)
            Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalIsZero Val a
n
        Expr Void a
NaturalEven -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural -> Bool
forall a. Integral a => a -> Bool
even Natural
n)
            Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalEven Val a
n
        Expr Void a
NaturalOdd -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural -> Bool
forall a. Integral a => a -> Bool
odd Natural
n)
            Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalOdd Val a
n
        Expr Void a
NaturalToInteger -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
n -> Integer -> Val a
forall a. Integer -> Val a
VIntegerLit (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n)
            Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalToInteger Val a
n
        Expr Void a
NaturalShow -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
n -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit ([(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] (String -> Text
Text.pack (Natural -> String
forall a. Show a => a -> String
show Natural
n)))
            Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalShow Val a
n
        Expr Void a
NaturalSubtract -> (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
            VNaturalLit Natural
0 ->
                HLamInfo a -> (Val a -> Val a) -> Val a
forall a. HLamInfo a -> (Val a -> Val a) -> Val a
VHLam HLamInfo a
forall a. HLamInfo a
NaturalSubtractZero Val a -> Val a
forall a. a -> a
id
            x :: Val a
x@(VNaturalLit Natural
m) ->
                (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                    VNaturalLit Natural
n
                        | Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
m ->
                            -- Use an `Integer` for the subtraction, due to the
                            -- following issue:
                            --
                            -- https://github.com/ghcjs/ghcjs/issues/782
                            Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (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
m :: Integer) (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n :: Integer)))
                        | Bool
otherwise -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                    Val a
y -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalSubtract Val a
x Val a
y
            Val a
x ->
                (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                    VNaturalLit Natural
0    -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                    Val a
y | Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
x Val a
y -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                    Val a
y                -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalSubtract Val a
x Val a
y
        NaturalPlus Expr Void a
t Expr Void a
u ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vNaturalPlus (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        NaturalTimes Expr Void a
t Expr Void a
u ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u) of
                (VNaturalLit Natural
1, Val a
u'           ) -> Val a
u'
                (Val a
t'           , VNaturalLit Natural
1) -> Val a
t'
                (VNaturalLit Natural
0, Val a
_            ) -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                (Val a
_            , VNaturalLit Natural
0) -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                (VNaturalLit Natural
m, VNaturalLit Natural
n) -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
n)
                (Val a
t'           , Val a
u'           ) -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalTimes Val a
t' Val a
u'
        Expr Void a
Integer ->
            Val a
forall a. Val a
VInteger
        IntegerLit Integer
n ->
            Integer -> Val a
forall a. Integer -> Val a
VIntegerLit Integer
n
        Expr Void a
IntegerClamp ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VIntegerLit Integer
n
                    | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n    -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n)
                    | Bool
otherwise -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
0
                Val a
n -> Val a -> Val a
forall a. Val a -> Val a
VIntegerClamp Val a
n
        Expr Void a
IntegerNegate ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VIntegerLit Integer
n -> Integer -> Val a
forall a. Integer -> Val a
VIntegerLit (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n)
                Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VIntegerNegate Val a
n
        Expr Void a
IntegerShow ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VIntegerLit Integer
n
                    | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n    -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit ([(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] (String -> Text
Text.pack (Char
'+'Char -> ShowS
forall a. a -> [a] -> [a]
:Integer -> String
forall a. Show a => a -> String
show Integer
n)))
                    | Bool
otherwise -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit ([(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] (String -> Text
Text.pack (Integer -> String
forall a. Show a => a -> String
show Integer
n)))
                Val a
n -> Val a -> Val a
forall a. Val a -> Val a
VIntegerShow Val a
n
        Expr Void a
IntegerToDouble ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VIntegerLit Integer
n -> DhallDouble -> Val a
forall a. DhallDouble -> Val a
VDoubleLit (Double -> DhallDouble
DhallDouble (String -> Double
forall a. Read a => String -> a
read (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.
                Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VIntegerToDouble Val a
n
        Expr Void a
Double ->
            Val a
forall a. Val a
VDouble
        DoubleLit DhallDouble
n ->
            DhallDouble -> Val a
forall a. DhallDouble -> Val a
VDoubleLit DhallDouble
n
        Expr Void a
DoubleShow ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VDoubleLit (DhallDouble Double
n) -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit ([(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] (String -> Text
Text.pack (Double -> String
forall a. Show a => a -> String
show Double
n)))
                Val a
n                          -> Val a -> Val a
forall a. Val a -> Val a
VDoubleShow Val a
n
        Expr Void a
Text ->
            Val a
forall a. Val a
VText
        TextLit Chunks Void a
cs ->
            case Chunks Void a -> VChunks a
evalChunks Chunks Void a
cs of
                VChunks [(Text
"", Val a
t)] Text
"" -> Val a
t
                VChunks a
vcs                  -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit VChunks a
vcs
        TextAppend Expr Void a
t Expr Void a
u ->
            Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Chunks Void a -> Expr Void a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr Void a)] -> Text -> Chunks Void a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks [(Text
"", Expr Void a
t), (Text
"", Expr Void a
u)] Text
""))
        Expr Void a
TextShow ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VTextLit (VChunks [] Text
x) -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit ([(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] (Text -> Text
textShow Text
x))
                Val a
t                       -> Val a -> Val a
forall a. Val a -> Val a
VTextShow Val a
t
        Expr Void a
TextReplace ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
needle ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
replacement ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
haystack ->
                case Val a
needle of
                    VTextLit (VChunks [] Text
"") ->
                        Val a
haystack
                    VTextLit (VChunks [] Text
needleText) ->
                        case Val a
haystack of
                            VTextLit (VChunks [] Text
haystackText) ->
                                case Val a
replacement of
                                    VTextLit (VChunks [] Text
replacementText) ->
                                        VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit (VChunks a -> Val a) -> VChunks a -> Val a
forall a b. (a -> b) -> a -> b
$ [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks []
                                            (Text -> Text -> Text -> Text
Text.replace
                                                Text
needleText
                                                Text
replacementText
                                                Text
haystackText
                                            )
                                    Val a
_ ->
                                        VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit
                                            (Text -> Val a -> Text -> VChunks a
forall a. Text -> Val a -> Text -> VChunks a
vTextReplace
                                                Text
needleText
                                                Val a
replacement
                                                Text
haystackText
                                            )
                            Val a
_ ->
                                Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a
VTextReplace Val a
needle Val a
replacement Val a
haystack
                    Val a
_ ->
                        Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a
VTextReplace Val a
needle Val a
replacement Val a
haystack
        Expr Void a
List ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim Val a -> Val a
forall a. Val a -> Val a
VList
        ListLit Maybe (Expr Void a)
ma Seq (Expr Void a)
ts ->
            Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit ((Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env) Maybe (Expr Void a)
ma) ((Expr Void a -> Val a) -> Seq (Expr Void a) -> Seq (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env) Seq (Expr Void a)
ts)
        ListAppend Expr Void a
t Expr Void a
u ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vListAppend (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        Expr Void a
ListBuild ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                Val a
VPrimVar ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListBuild Val a
a Val a
forall a. Val a
VPrimVar
                Val a
t ->       Val a
t
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Val a -> Val a
forall a. Val a -> Val a
VList Val a
a
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` HLamInfo a -> (Val a -> Val a) -> Val a
forall a. HLamInfo a -> (Val a -> Val a) -> Val a
VHLam (Text -> Val a -> HLamInfo a
forall a. Text -> Val a -> HLamInfo a
Typed Text
"a" Val a
a) (\Val a
x ->
                           HLamInfo a -> (Val a -> Val a) -> Val a
forall a. HLamInfo a -> (Val a -> Val a) -> Val a
VHLam (Text -> Val a -> HLamInfo a
forall a. Text -> Val a -> HLamInfo a
Typed Text
"as" (Val a -> Val a
forall a. Val a -> Val a
VList Val a
a)) (\Val a
as ->
                           Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vListAppend (Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
forall a. Maybe a
Nothing (Val a -> Seq (Val a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Val a
x)) Val a
as))
                    Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit (Val a -> Maybe (Val a)
forall a. a -> Maybe a
Just (Val a -> Val a
forall a. Val a -> Val a
VList Val a
a)) Seq (Val a)
forall a. Monoid a => a
mempty

        Expr Void a
ListFold ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
as ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
list ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
cons ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \Val a
nil ->
            let inert :: Val a
inert = Val a -> Val a -> Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a -> Val a -> Val a
VListFold Val a
a Val a
as Val a
list Val a
cons Val a
nil
            in  case Val a
nil of
                Val a
VPrimVar -> Val a
inert
                Val a
_ -> case Val a
cons of
                    Val a
VPrimVar -> Val a
inert
                    Val a
_ -> case Val a
list of
                        Val a
VPrimVar -> Val a
inert
                        Val a
_ -> case Val a
a of
                            Val a
VPrimVar -> Val a
inert
                            Val a
_ -> case Val a
as of
                                VListLit Maybe (Val a)
_ Seq (Val a)
as' ->
                                    (Val a -> Val a -> Val a) -> Val a -> Seq (Val a) -> Val a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\Val a
x Val a
b -> Val a
cons Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Val a
x Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Val a
b) Val a
nil Seq (Val a)
as'
                                Val a
_ -> Val a
inert
        Expr Void a
ListLength ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VListLit Maybe (Val a)
_ Seq (Val a)
as -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Seq (Val a) -> Int
forall a. Seq a -> Int
Sequence.length Seq (Val a)
as))
                Val a
as            -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListLength Val a
a Val a
as
        Expr Void a
ListHead ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VListLit Maybe (Val a)
_ Seq (Val a)
as ->
                    case Seq (Val a) -> ViewL (Val a)
forall a. Seq a -> ViewL a
Sequence.viewl Seq (Val a)
as of
                        Val a
y :< Seq (Val a)
_ -> Val a -> Val a
forall a. Val a -> Val a
VSome Val a
y
                        ViewL (Val a)
_      -> Val a -> Val a
forall a. Val a -> Val a
VNone Val a
a
                Val a
as ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListHead Val a
a Val a
as
        Expr Void a
ListLast ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VListLit Maybe (Val a)
_ Seq (Val a)
as ->
                    case Seq (Val a) -> ViewR (Val a)
forall a. Seq a -> ViewR a
Sequence.viewr Seq (Val a)
as of
                        Seq (Val a)
_ :> Val a
t -> Val a -> Val a
forall a. Val a -> Val a
VSome Val a
t
                        ViewR (Val a)
_      -> Val a -> Val a
forall a. Val a -> Val a
VNone Val a
a
                Val a
as -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListLast Val a
a Val a
as
        Expr Void a
ListIndexed ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VListLit Maybe (Val a)
_ Seq (Val a)
as ->
                    let a' :: Maybe (Val a)
a' =
                            if Seq (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Val a)
as
                            then Val a -> Maybe (Val a)
forall a. a -> Maybe a
Just (Val a -> Val a
forall a. Val a -> Val a
VList (Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecord ([(Text, Val a)] -> Map Text (Val a)
forall k v. Ord k => [(k, v)] -> Map k v
Map.unorderedFromList [(Text
"index", Val a
forall a. Val a
VNatural), (Text
"value", Val a
a)])))
                            else Maybe (Val a)
forall a. Maybe a
Nothing

                        as' :: Seq (Val a)
as' =
                            (Int -> Val a -> Val a) -> Seq (Val a) -> Seq (Val a)
forall a b. (Int -> a -> b) -> Seq a -> Seq b
Sequence.mapWithIndex
                                (\Int
i Val a
t ->
                                    Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit
                                        ([(Text, Val a)] -> Map Text (Val a)
forall k v. Ord k => [(k, v)] -> Map k v
Map.unorderedFromList
                                            [ (Text
"index", Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
                                            , (Text
"value", Val a
t)
                                            ]
                                        )
                                )
                                Seq (Val a)
as

                        in  Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
a' Seq (Val a)
as'
                Val a
t ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListIndexed Val a
a Val a
t
        Expr Void a
ListReverse ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ ~Val a
a ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \case
                VListLit Maybe (Val a)
t Seq (Val a)
as | Seq (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Val a)
as ->
                    Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
t Seq (Val a)
as
                VListLit Maybe (Val a)
_ Seq (Val a)
as ->
                    Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
forall a. Maybe a
Nothing (Seq (Val a) -> Seq (Val a)
forall a. Seq a -> Seq a
Sequence.reverse Seq (Val a)
as)
                Val a
t ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListReverse Val a
a Val a
t
        Expr Void a
Optional ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim Val a -> Val a
forall a. Val a -> Val a
VOptional
        Some Expr Void a
t ->
            Val a -> Val a
forall a. Val a -> Val a
VSome (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t)
        Expr Void a
None ->
            (Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \ ~Val a
a -> Val a -> Val a
forall a. Val a -> Val a
VNone Val a
a
        Record Map Text (RecordField Void a)
kts ->
            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecord (Map Text (Val a) -> Map Text (Val a)
forall k v. Map k v -> Map k v
Map.sort (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Val a)
-> (RecordField Void a -> Expr Void a)
-> RecordField Void a
-> Val a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordField Void a -> Expr Void a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField Void a -> Val a)
-> Map Text (RecordField Void a) -> Map Text (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField Void a)
kts))
        RecordLit Map Text (RecordField Void a)
kts ->
            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit (Map Text (Val a) -> Map Text (Val a)
forall k v. Map k v -> Map k v
Map.sort (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Val a)
-> (RecordField Void a -> Expr Void a)
-> RecordField Void a
-> Val a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecordField Void a -> Expr Void a
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField Void a -> Val a)
-> Map Text (RecordField Void a) -> Map Text (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField Void a)
kts))
        Union Map Text (Maybe (Expr Void a))
kts ->
            Map Text (Maybe (Val a)) -> Val a
forall a. Map Text (Maybe (Val a)) -> Val a
VUnion (Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a))
forall k v. Map k v -> Map k v
Map.sort ((Maybe (Expr Void a) -> Maybe (Val a))
-> Map Text (Maybe (Expr Void a)) -> Map Text (Maybe (Val a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env)) Map Text (Maybe (Expr Void a))
kts))
        Combine Maybe CharacterSet
_ Maybe Text
mk Expr Void a
t Expr Void a
u ->
            Maybe Text -> Val a -> Val a -> Val a
forall a. Maybe Text -> Val a -> Val a -> Val a
vCombine Maybe Text
mk (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        CombineTypes Maybe CharacterSet
_ Expr Void a
t Expr Void a
u ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
vCombineTypes (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        Prefer Maybe CharacterSet
_ PreferAnnotation Void a
_ Expr Void a
t Expr Void a
u ->
            Environment a -> Val a -> Val a -> Val a
forall a. Eq a => Environment a -> Val a -> Val a -> Val a
vPrefer Environment a
env (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        RecordCompletion Expr Void a
t Expr Void a
u ->
            Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
Annot (Maybe CharacterSet
-> PreferAnnotation Void a
-> Expr Void a
-> Expr Void a
-> Expr Void a
forall s a.
Maybe CharacterSet
-> PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer Maybe CharacterSet
forall a. Monoid a => a
mempty PreferAnnotation Void a
forall s a. PreferAnnotation s a
PreferFromCompletion (Expr Void a -> FieldSelection Void -> Expr Void a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr Void a
t FieldSelection Void
forall s. FieldSelection s
def) Expr Void a
u) (Expr Void a -> FieldSelection Void -> Expr Void a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field Expr Void a
t FieldSelection Void
forall s. FieldSelection s
typ))
          where
            def :: FieldSelection s
def = Text -> FieldSelection s
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"default"
            typ :: FieldSelection s
typ = Text -> FieldSelection s
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
"Type"
        Merge Expr Void a
x Expr Void a
y Maybe (Expr Void a)
ma ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
x, Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
y, (Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env) Maybe (Expr Void a)
ma) of
                (VRecordLit Map Text (Val a)
m, VInject Map Text (Maybe (Val a))
_ Text
k Maybe (Val a)
mt, Maybe (Val a)
_)
                    | Just Val a
f <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
k Map Text (Val a)
m -> Val a -> (Val a -> Val a) -> Maybe (Val a) -> Val a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Val a
f (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
f) Maybe (Val a)
mt
                    | Bool
otherwise                -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
                (VRecordLit Map Text (Val a)
m, VSome Val a
t, Maybe (Val a)
_)
                    | Just Val a
f <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
"Some" Map Text (Val a)
m -> Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
f Val a
t
                    | Bool
otherwise                     -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
                (VRecordLit Map Text (Val a)
m, VNone Val a
_, Maybe (Val a)
_)
                    | Just Val a
t <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup Text
"None" Map Text (Val a)
m -> Val a
t
                    | Bool
otherwise                     -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
                (Val a
x', Val a
y', Maybe (Val a)
ma') -> Val a -> Val a -> Maybe (Val a) -> Val a
forall a. Val a -> Val a -> Maybe (Val a) -> Val a
VMerge Val a
x' Val a
y' Maybe (Val a)
ma'
        ToMap Expr Void a
x Maybe (Expr Void a)
ma ->
            case (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
x, (Expr Void a -> Val a) -> Maybe (Expr Void a) -> Maybe (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env) Maybe (Expr Void a)
ma) of
                (VRecordLit Map Text (Val a)
m, ma' :: Maybe (Val a)
ma'@(Just Val a
_)) | Map Text (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Text (Val a)
m ->
                    Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
ma' Seq (Val a)
forall a. Seq a
Sequence.empty
                (VRecordLit Map Text (Val a)
m, Maybe (Val a)
_) ->
                    let entry :: (Text, Val a) -> Val a
entry (Text
k, Val a
v) =
                            Map Text (Val a) -> Val a
forall a. Map Text (Val a) -> Val a
VRecordLit
                                ([(Text, Val a)] -> Map Text (Val a)
forall k v. Ord k => [(k, v)] -> Map k v
Map.unorderedFromList
                                    [ (Text
"mapKey", VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit (VChunks a -> Val a) -> VChunks a -> Val a
forall a b. (a -> b) -> a -> b
$ [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
k)
                                    , (Text
"mapValue", Val a
v)
                                    ]
                                )

                        s :: Seq (Val a)
s = ([Val a] -> Seq (Val a)
forall a. [a] -> Seq a
Sequence.fromList ([Val a] -> Seq (Val a))
-> (Map Text (Val a) -> [Val a]) -> Map Text (Val a) -> Seq (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Text, Val a) -> Val a) -> [(Text, Val a)] -> [Val a]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Val a) -> Val a
forall a. (Text, Val a) -> Val a
entry ([(Text, Val a)] -> [Val a])
-> (Map Text (Val a) -> [(Text, Val a)])
-> Map Text (Val a)
-> [Val a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text (Val a) -> [(Text, Val a)]
forall k v. Map k v -> [(k, v)]
Map.toAscList) Map Text (Val a)
m

                    in  Maybe (Val a) -> Seq (Val a) -> Val a
forall a. Maybe (Val a) -> Seq (Val a) -> Val a
VListLit Maybe (Val a)
forall a. Maybe a
Nothing Seq (Val a)
s
                (Val a
x', Maybe (Val a)
ma') ->
                    Val a -> Maybe (Val a) -> Val a
forall a. Val a -> Maybe (Val a) -> Val a
VToMap Val a
x' Maybe (Val a)
ma'
        Field Expr Void a
t (FieldSelection Void -> Text
forall s. FieldSelection s -> Text
Syntax.fieldSelectionLabel -> Text
k) ->
            Val a -> Text -> Val a
forall a. Val a -> Text -> Val a
vField (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) Text
k
        Project Expr Void a
t (Left [Text]
ks) ->
            Environment a -> Val a -> Set Text -> Val a
forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields Environment a
env (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Set Text -> Set Text
forall a. Ord a => Set a -> Set a
Dhall.Set.sort ([Text] -> Set Text
forall a. Ord a => [a] -> Set a
Dhall.Set.fromList [Text]
ks))
        Project Expr Void a
t (Right Expr Void a
e) ->
            case Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
e of
                VRecord Map Text (Val a)
kts ->
                    Environment a -> Val a -> Set Text -> Val a
forall a. Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields Environment a
env (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Set Text -> Set Text
forall a. Set a -> Set a
Dhall.Set.fromSet (Map Text (Val a) -> Set Text
forall k v. Map k v -> Set k
Map.keysSet Map Text (Val a)
kts))
                Val a
e' ->
                    Val a -> Either (Set Text) (Val a) -> Val a
forall a. Val a -> Either (Set Text) (Val a) -> Val a
VProject (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Val a -> Either (Set Text) (Val a)
forall a b. b -> Either a b
Right Val a
e')
        Assert Expr Void a
t ->
            Val a -> Val a
forall a. Val a -> Val a
VAssert (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t)
        Equivalent Expr Void a
t Expr Void a
u ->
            Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VEquivalent (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
u)
        With Expr Void a
e₀ NonEmpty Text
ks Expr Void a
v ->
            Val a -> NonEmpty Text -> Val a -> Val a
forall a. Val a -> NonEmpty Text -> Val a -> Val a
vWith (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
e₀) NonEmpty Text
ks (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
v)
        Note Void
_ Expr Void a
e ->
            Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
e
        ImportAlt Expr Void a
t Expr Void a
_ ->
            Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t
        Embed a
a ->
            a -> Val a
forall a. a -> Val a
VEmbed a
a
  where
    evalChunks :: Chunks Void a -> VChunks a
    evalChunks :: Chunks Void a -> VChunks a
evalChunks (Chunks [(Text, Expr Void a)]
xys Text
z) = ((Text, Expr Void a) -> VChunks a -> VChunks a)
-> VChunks a -> [(Text, Expr Void a)] -> VChunks a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (Text, Expr Void a) -> VChunks a -> VChunks a
cons VChunks a
forall a. VChunks a
nil [(Text, Expr Void a)]
xys
      where
        cons :: (Text, Expr Void a) -> VChunks a -> VChunks a
cons (Text
x, Expr Void a
t) VChunks a
vcs =
            case Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env Expr Void a
t of
                VTextLit VChunks a
vcs' -> [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
x VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
vcs' VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
vcs
                Val a
t'            -> [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [(Text
x, Val a
t')] Text
forall a. Monoid a => a
mempty VChunks a -> VChunks a -> VChunks a
forall a. Semigroup a => a -> a -> a
<> VChunks a
vcs

        nil :: VChunks a
nil = [(Text, Val a)] -> Text -> VChunks a
forall a. [(Text, Val a)] -> Text -> VChunks a
VChunks [] Text
z
    {-# INLINE evalChunks #-}

eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy a -> a -> Bool
f = [a] -> [a] -> Bool
go
  where
    go :: [a] -> [a] -> Bool
go (a
x:[a]
xs) (a
y:[a]
ys) | a -> a -> Bool
f a
x a
y = [a] -> [a] -> Bool
go [a]
xs [a]
ys
    go [] [] = Bool
True
    go [a]
_  [a]
_  = Bool
False
{-# INLINE eqListBy #-}

eqMapsBy :: Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy :: (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy v -> v -> Bool
f Map k v
mL Map k v
mR =
    Map k v -> Int
forall k v. Map k v -> Int
Map.size Map k v
mL Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Map k v -> Int
forall k v. Map k v -> Int
Map.size Map k v
mR
    Bool -> Bool -> Bool
&& ((k, v) -> (k, v) -> Bool) -> [(k, v)] -> [(k, v)] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy (k, v) -> (k, v) -> Bool
forall a. Eq a => (a, v) -> (a, v) -> Bool
eq (Map k v -> [(k, v)]
forall k v. Map k v -> [(k, v)]
Map.toAscList Map k v
mL) (Map k v -> [(k, v)]
forall k v. Map k v -> [(k, v)]
Map.toAscList Map k v
mR)
  where
    eq :: (a, v) -> (a, v) -> Bool
eq (a
kL, v
vL) (a
kR, v
vR) = a
kL a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
kR Bool -> Bool -> Bool
&& v -> v -> Bool
f v
vL v
vR
{-# INLINE eqMapsBy #-}

eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy a -> a -> Bool
f = Maybe a -> Maybe a -> Bool
go
  where
    go :: Maybe a -> Maybe a -> Bool
go (Just a
x) (Just a
y) = a -> a -> Bool
f a
x a
y
    go Maybe a
Nothing  Maybe a
Nothing  = Bool
True
    go Maybe a
_        Maybe a
_        = Bool
False
{-# INLINE eqMaybeBy #-}

-- | Utility that powers the @Text/show@ built-in
textShow :: Text -> Text
textShow :: Text -> Text
textShow Text
text = Text
"\"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Char -> Text) -> Text -> Text
Text.concatMap Char -> Text
f Text
text Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\""
  where
    f :: Char -> Text
f Char
'"'  = Text
"\\\""
    f Char
'$'  = Text
"\\u0024"
    f Char
'\\' = Text
"\\\\"
    f Char
'\b' = Text
"\\b"
    f Char
'\n' = Text
"\\n"
    f Char
'\r' = Text
"\\r"
    f Char
'\t' = Text
"\\t"
    f Char
'\f' = Text
"\\f"
    f Char
c | Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'\x1F' = String -> Text
Text.pack (String -> Int -> String
forall r. PrintfType r => String -> r
Text.Printf.printf String
"\\u%04x" (Char -> Int
Data.Char.ord Char
c))
        | Bool
otherwise   = Char -> Text
Text.singleton Char
c

conv :: forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv :: Environment a -> Val a -> Val a -> Bool
conv !Environment a
env Val a
t0 Val a
t0' =
    case (Val a
t0, Val a
t0') of
        (VConst Const
k, VConst Const
k') ->
            Const
k Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
k'
        (VVar Text
x Int
i, VVar Text
x' Int
i') ->
            Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i'
        (VLam Val a
_ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t)), VLam Val a
_ Closure a
t' ) ->
            Text -> Val a -> Val a -> Bool
convSkip Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t Val a
v) (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t' Val a
v)
        (VLam Val a
_ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t)), VHLam HLamInfo a
_ Val a -> Val a
t') ->
            Text -> Val a -> Val a -> Bool
convSkip Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t Val a
v) (Val a -> Val a
t' Val a
v)
        (VLam Val a
_ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t)), Val a
t'        ) ->
            Text -> Val a -> Val a -> Bool
convSkip Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t Val a
v) (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
t' Val a
v)
        (VHLam HLamInfo a
_ Val a -> Val a
t, VLam Val a
_ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t'))) ->
            Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a
t Val a
v) (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t' Val a
v)
        (VHLam HLamInfo a
_ Val a -> Val a
t, VHLam HLamInfo a
_ Val a -> Val a
t'                    ) ->
            let (Text
x, Val a
v) = Text -> (Text, Val a)
fresh Text
"x" in Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a
t Val a
v) (Val a -> Val a
t' Val a
v)
        (VHLam HLamInfo a
_ Val a -> Val a
t, Val a
t'                            ) ->
            let (Text
x, Val a
v) = Text -> (Text, Val a)
fresh Text
"x" in Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a
t Val a
v) (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
t' Val a
v)
        (Val a
t, VLam Val a
_ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t'))) ->
            Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
t Val a
v) (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t' Val a
v)
        (Val a
t, VHLam HLamInfo a
_ Val a -> Val a
t'  ) ->
            let (Text
x, Val a
v) = Text -> (Text, Val a)
fresh Text
"x" in Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
vApp Val a
t Val a
v) (Val a -> Val a
t' Val a
v)
        (VApp Val a
t Val a
u, VApp Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VPi Val a
a Closure a
b, VPi Val a
a' (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
b'))) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Text -> Val a -> Val a -> Bool
convSkip Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b Val a
v) (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b' Val a
v)
        (VPi Val a
a Closure a
b, VHPi (Text -> (Text, Val a)
fresh -> (Text
x, Val a
v)) Val a
a' Val a -> Val a
b') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Text -> Val a -> Val a -> Bool
convSkip Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b Val a
v) (Val a -> Val a
b' Val a
v)
        (VHPi Text
_ Val a
a Val a -> Val a
b, VPi Val a
a' (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
b'))) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a
b Val a
v) (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b' Val a
v)
        (VHPi Text
_ Val a
a Val a -> Val a
b, VHPi (Text -> (Text, Val a)
fresh -> (Text
x, Val a
v)) Val a
a' Val a -> Val a
b') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Text -> Val a -> Val a -> Bool
convSkip Text
x (Val a -> Val a
b Val a
v) (Val a -> Val a
b' Val a
v)
        (Val a
VBool, Val a
VBool) ->
            Bool
True
        (VBoolLit Bool
b, VBoolLit Bool
b') ->
            Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b'
        (VBoolAnd Val a
t Val a
u, VBoolAnd Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VBoolOr Val a
t Val a
u, VBoolOr Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VBoolEQ Val a
t Val a
u, VBoolEQ Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VBoolNE Val a
t Val a
u, VBoolNE Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VBoolIf Val a
t Val a
u Val a
v, VBoolIf Val a
t' Val a
u' Val a
v') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
v Val a
v'
        (Val a
VNatural, Val a
VNatural) ->
            Bool
True
        (VNaturalLit Natural
n, VNaturalLit Natural
n') ->
            Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n'
        (VNaturalFold Val a
t Val a
_ Val a
u Val a
v, VNaturalFold Val a
t' Val a
_ Val a
u' Val a
v') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
v Val a
v'
        (VNaturalBuild Val a
t, VNaturalBuild Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalIsZero Val a
t, VNaturalIsZero Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalEven Val a
t, VNaturalEven Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalOdd Val a
t, VNaturalOdd Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalToInteger Val a
t, VNaturalToInteger Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalShow Val a
t, VNaturalShow Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNaturalSubtract Val a
x Val a
y, VNaturalSubtract Val a
x' Val a
y') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
x Val a
x' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
y Val a
y'
        (VNaturalPlus Val a
t Val a
u, VNaturalPlus Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VNaturalTimes Val a
t Val a
u, VNaturalTimes Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (Val a
VInteger, Val a
VInteger) ->
            Bool
True
        (VIntegerLit Integer
t, VIntegerLit Integer
t') ->
            Integer
t Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
t'
        (VIntegerClamp Val a
t, VIntegerClamp Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VIntegerNegate Val a
t, VIntegerNegate Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VIntegerShow Val a
t, VIntegerShow Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VIntegerToDouble Val a
t, VIntegerToDouble Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (Val a
VDouble, Val a
VDouble) ->
            Bool
True
        (VDoubleLit DhallDouble
n, VDoubleLit DhallDouble
n') ->
            DhallDouble
n DhallDouble -> DhallDouble -> Bool
forall a. Eq a => a -> a -> Bool
== DhallDouble
n'
        (VDoubleShow Val a
t, VDoubleShow Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (Val a
VText, Val a
VText) ->
            Bool
True
        (VTextLit VChunks a
cs, VTextLit VChunks a
cs') ->
            VChunks a -> VChunks a -> Bool
convChunks VChunks a
cs VChunks a
cs'
        (VTextAppend Val a
t Val a
u, VTextAppend Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VTextShow Val a
t, VTextShow Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VTextReplace Val a
a Val a
b Val a
c, VTextReplace Val a
a' Val a
b' Val a
c') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
b Val a
b' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
c Val a
c'
        (VList Val a
a, VList Val a
a') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a'
        (VListLit Maybe (Val a)
_ Seq (Val a)
xs, VListLit Maybe (Val a)
_ Seq (Val a)
xs') ->
            (Val a -> Val a -> Bool) -> [Val a] -> [Val a] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env) (Seq (Val a) -> [Val a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Val a)
xs) (Seq (Val a) -> [Val a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Val a)
xs')
        (VListAppend Val a
t Val a
u, VListAppend Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VListBuild Val a
_ Val a
t, VListBuild Val a
_ Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListLength Val a
a Val a
t, VListLength Val a
a' Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListHead Val a
_ Val a
t, VListHead Val a
_ Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListLast Val a
_ Val a
t, VListLast Val a
_ Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListIndexed Val a
_ Val a
t, VListIndexed Val a
_ Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListReverse Val a
_ Val a
t, VListReverse Val a
_ Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VListFold Val a
a Val a
l Val a
_ Val a
t Val a
u, VListFold Val a
a' Val a
l' Val a
_ Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
l Val a
l' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VOptional Val a
a, VOptional Val a
a') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
a Val a
a'
        (VSome Val a
t, VSome Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VNone Val a
_, VNone Val a
_) ->
            Bool
True
        (VRecord Map Text (Val a)
m, VRecord Map Text (Val a)
m') ->
            (Val a -> Val a -> Bool)
-> Map Text (Val a) -> Map Text (Val a) -> Bool
forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env) Map Text (Val a)
m Map Text (Val a)
m'
        (VRecordLit Map Text (Val a)
m, VRecordLit Map Text (Val a)
m') ->
            (Val a -> Val a -> Bool)
-> Map Text (Val a) -> Map Text (Val a) -> Bool
forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env) Map Text (Val a)
m Map Text (Val a)
m'
        (VUnion Map Text (Maybe (Val a))
m, VUnion Map Text (Maybe (Val a))
m') ->
            (Maybe (Val a) -> Maybe (Val a) -> Bool)
-> Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a)) -> Bool
forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy ((Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env)) Map Text (Maybe (Val a))
m Map Text (Maybe (Val a))
m'
        (VCombine Maybe Text
_ Val a
t Val a
u, VCombine Maybe Text
_ Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VCombineTypes Val a
t Val a
u, VCombineTypes Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VPrefer Val a
t Val a
u, VPrefer Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VMerge Val a
t Val a
u Maybe (Val a)
_, VMerge Val a
t' Val a
u' Maybe (Val a)
_) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VToMap Val a
t Maybe (Val a)
_, VToMap Val a
t' Maybe (Val a)
_) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VField Val a
t Text
k, VField Val a
t' Text
k') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Text
k Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
k'
        (VProject Val a
t (Left Set Text
ks), VProject Val a
t' (Left Set Text
ks')) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Set Text
ks Set Text -> Set Text -> Bool
forall a. Eq a => a -> a -> Bool
== Set Text
ks'
        (VProject Val a
t (Right Val a
e), VProject Val a
t' (Right Val a
e')) ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
e Val a
e'
        (VAssert Val a
t, VAssert Val a
t') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t'
        (VEquivalent Val a
t Val a
u, VEquivalent Val a
t' Val a
u') ->
            Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
t Val a
t' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
u Val a
u'
        (VInject Map Text (Maybe (Val a))
m Text
k Maybe (Val a)
mt, VInject Map Text (Maybe (Val a))
m' Text
k' Maybe (Val a)
mt') ->
            (Maybe (Val a) -> Maybe (Val a) -> Bool)
-> Map Text (Maybe (Val a)) -> Map Text (Maybe (Val a)) -> Bool
forall k v. Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy ((Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env)) Map Text (Maybe (Val a))
m Map Text (Maybe (Val a))
m' Bool -> Bool -> Bool
&& Text
k Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
k' Bool -> Bool -> Bool
&& (Val a -> Val a -> Bool) -> Maybe (Val a) -> Maybe (Val a) -> Bool
forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy (Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env) Maybe (Val a)
mt Maybe (Val a)
mt'
        (VEmbed a
a, VEmbed a
a') ->
            a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a'
        (Val a
_, Val a
_) ->
            Bool
False
  where
    fresh :: Text -> (Text, Val a)
    fresh :: Text -> (Text, Val a)
fresh Text
x = (Text
x, Text -> Int -> Val a
forall a. Text -> Int -> Val a
VVar Text
x (Text -> Environment a -> Int
forall a. Text -> Environment a -> Int
countEnvironment Text
x Environment a
env))
    {-# INLINE fresh #-}

    freshClosure :: Closure a -> (Text, Val a, Closure a)
    freshClosure :: Closure a -> (Text, Val a, Closure a)
freshClosure closure :: Closure a
closure@(Closure Text
x Environment a
_ Expr Void a
_) = (Text
x, (Text, Val a) -> Val a
forall a b. (a, b) -> b
snd (Text -> (Text, Val a)
fresh Text
x), Closure a
closure)
    {-# INLINE freshClosure #-}

    convChunks :: VChunks a -> VChunks a -> Bool
    convChunks :: VChunks a -> VChunks a -> Bool
convChunks (VChunks [(Text, Val a)]
xys Text
z) (VChunks [(Text, Val a)]
xys' Text
z') =
      ((Text, Val a) -> (Text, Val a) -> Bool)
-> [(Text, Val a)] -> [(Text, Val a)] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy (\(Text
x, Val a
y) (Text
x', Val a
y') -> Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' Bool -> Bool -> Bool
&& Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
env Val a
y Val a
y') [(Text, Val a)]
xys [(Text, Val a)]
xys' Bool -> Bool -> Bool
&& Text
z Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
z'
    {-# INLINE convChunks #-}

    convSkip :: Text -> Val a -> Val a -> Bool
    convSkip :: Text -> Val a -> Val a -> Bool
convSkip Text
x = Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv (Environment a -> Text -> Environment a
forall a. Environment a -> Text -> Environment a
Skip Environment a
env Text
x)
    {-# INLINE convSkip #-}

judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual :: Expr s a -> Expr t a -> Bool
judgmentallyEqual (Expr s a -> Expr Void a
forall s a t. Expr s a -> Expr t a
Syntax.denote -> Expr Void a
t) (Expr t a -> Expr Void a
forall s a t. Expr s a -> Expr t a
Syntax.denote -> Expr Void a
u) =
    Environment a -> Val a -> Val a -> Bool
forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv Environment a
forall a. Environment a
Empty (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
forall a. Environment a
Empty Expr Void a
t) (Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
forall a. Environment a
Empty Expr Void a
u)

data Names
  = EmptyNames
  | Bind !Names {-# UNPACK #-} !Text
  deriving Int -> Names -> ShowS
[Names] -> ShowS
Names -> String
(Int -> Names -> ShowS)
-> (Names -> String) -> ([Names] -> ShowS) -> Show Names
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Names] -> ShowS
$cshowList :: [Names] -> ShowS
show :: Names -> String
$cshow :: Names -> String
showsPrec :: Int -> Names -> ShowS
$cshowsPrec :: Int -> Names -> ShowS
Show

envNames :: Environment a -> Names
envNames :: Environment a -> Names
envNames Environment a
Empty = Names
EmptyNames
envNames (Skip   Environment a
env Text
x  ) = Names -> Text -> Names
Bind (Environment a -> Names
forall a. Environment a -> Names
envNames Environment a
env) Text
x
envNames (Extend Environment a
env Text
x Val a
_) = Names -> Text -> Names
Bind (Environment a -> Names
forall a. Environment a -> Names
envNames Environment a
env) Text
x

countNames :: Text -> Names -> Int
countNames :: Text -> Names -> Int
countNames Text
x = Int -> Names -> Int
forall t. Num t => t -> Names -> t
go Int
0
  where
    go :: t -> Names -> t
go !t
acc Names
EmptyNames         = t
acc
    go  t
acc (Bind Names
env Text
x') = t -> Names -> t
go (if Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x' then t
acc t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 else t
acc) Names
env

-- | Quote a value into beta-normal form.
quote :: forall a. Eq a => Names -> Val a -> Expr Void a
quote :: Names -> Val a -> Expr Void a
quote !Names
env !Val a
t0 =
    case Val a
t0 of
        VConst Const
k ->
            Const -> Expr Void a
forall s a. Const -> Expr s a
Const Const
k
        VVar !Text
x !Int
i ->
            Var -> Expr Void a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
x (Text -> Names -> Int
countNames Text
x Names
env Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
        VApp Val a
t Val a
u ->
            Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t Expr Void a -> Val a -> Expr Void a
`qApp` Val a
u
        VLam Val a
a (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
t)) ->
            Maybe CharacterSet
-> FunctionBinding Void a -> Expr Void a -> Expr Void a
forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam
                Maybe CharacterSet
forall a. Monoid a => a
mempty
                (Text -> Expr Void a -> FunctionBinding Void a
forall s a. Text -> Expr s a -> FunctionBinding s a
Syntax.makeFunctionBinding Text
x (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
a))
                (Text -> Val a -> Expr Void a
quoteBind Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
t Val a
v))
        VHLam HLamInfo a
i Val a -> Val a
t ->
            case HLamInfo a
i of
                Typed (Text -> (Text, Val a)
fresh -> (Text
x, Val a
v)) Val a
a ->
                    Maybe CharacterSet
-> FunctionBinding Void a -> Expr Void a -> Expr Void a
forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam
                        Maybe CharacterSet
forall a. Monoid a => a
mempty
                        (Text -> Expr Void a -> FunctionBinding Void a
forall s a. Text -> Expr s a -> FunctionBinding s a
Syntax.makeFunctionBinding Text
x (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
a))
                        (Text -> Val a -> Expr Void a
quoteBind Text
x (Val a -> Val a
t Val a
v))
                HLamInfo a
Prim                      -> Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env (Val a -> Val a
t Val a
forall a. Val a
VPrimVar)
                HLamInfo a
NaturalSubtractZero       -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr Void a
forall s a. Expr s a
NaturalSubtract (Natural -> Expr Void a
forall s a. Natural -> Expr s a
NaturalLit Natural
0)

        VPi Val a
a (Closure a -> (Text, Val a, Closure a)
freshClosure -> (Text
x, Val a
v, Closure a
b)) ->
            Maybe CharacterSet
-> Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
forall a. Monoid a => a
mempty Text
x (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
a) (Text -> Val a -> Expr Void a
quoteBind Text
x (Closure a -> Val a -> Val a
forall a. Eq a => Closure a -> Val a -> Val a
instantiate Closure a
b Val a
v))
        VHPi (Text -> (Text, Val a)
fresh -> (Text
x, Val a
v)) Val a
a Val a -> Val a
b ->
            Maybe CharacterSet
-> Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
forall a. Monoid a => a
mempty Text
x (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
a) (Text -> Val a -> Expr Void a
quoteBind Text
x (Val a -> Val a
b Val a
v))
        Val a
VBool ->
            Expr Void a
forall s a. Expr s a
Bool
        VBoolLit Bool
b ->
            Bool -> Expr Void a
forall s a. Bool -> Expr s a
BoolLit Bool
b
        VBoolAnd Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolAnd (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VBoolOr Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolOr (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VBoolEQ Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolEQ (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VBoolNE Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
BoolNE (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VBoolIf Val a
t Val a
u Val a
v ->
            Expr Void a -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
BoolIf (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
v)
        Val a
VNatural ->
            Expr Void a
forall s a. Expr s a
Natural
        VNaturalLit Natural
n ->
            Natural -> Expr Void a
forall s a. Natural -> Expr s a
NaturalLit Natural
n
        VNaturalFold Val a
a Val a
t Val a
u Val a
v ->
            Expr Void a
forall s a. Expr s a
NaturalFold Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t Expr Void a -> Val a -> Expr Void a
`qApp` Val a
u Expr Void a -> Val a -> Expr Void a
`qApp` Val a
v
        VNaturalBuild Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalBuild Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalIsZero Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalIsZero Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalEven Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalEven Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalOdd Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalOdd Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalToInteger Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalToInteger Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalShow Val a
t ->
            Expr Void a
forall s a. Expr s a
NaturalShow Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VNaturalPlus Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
NaturalPlus (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VNaturalTimes Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
NaturalTimes (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VNaturalSubtract Val a
x Val a
y ->
            Expr Void a
forall s a. Expr s a
NaturalSubtract Expr Void a -> Val a -> Expr Void a
`qApp` Val a
x Expr Void a -> Val a -> Expr Void a
`qApp` Val a
y
        Val a
VInteger ->
            Expr Void a
forall s a. Expr s a
Integer
        VIntegerLit Integer
n ->
            Integer -> Expr Void a
forall s a. Integer -> Expr s a
IntegerLit Integer
n
        VIntegerClamp Val a
t ->
            Expr Void a
forall s a. Expr s a
IntegerClamp Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VIntegerNegate Val a
t ->
            Expr Void a
forall s a. Expr s a
IntegerNegate Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VIntegerShow Val a
t ->
            Expr Void a
forall s a. Expr s a
IntegerShow Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VIntegerToDouble Val a
t ->
            Expr Void a
forall s a. Expr s a
IntegerToDouble Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        Val a
VDouble ->
            Expr Void a
forall s a. Expr s a
Double
        VDoubleLit DhallDouble
n ->
            DhallDouble -> Expr Void a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n
        VDoubleShow Val a
t ->
            Expr Void a
forall s a. Expr s a
DoubleShow Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        Val a
VText ->
            Expr Void a
forall s a. Expr s a
Text
        VTextLit (VChunks [(Text, Val a)]
xys Text
z) ->
            Chunks Void a -> Expr Void a
forall s a. Chunks s a -> Expr s a
TextLit ([(Text, Expr Void a)] -> Text -> Chunks Void a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks (((Text, Val a) -> (Text, Expr Void a))
-> [(Text, Val a)] -> [(Text, Expr Void a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Val a -> Expr Void a) -> (Text, Val a) -> (Text, Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env)) [(Text, Val a)]
xys) Text
z)
        VTextAppend Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VTextShow Val a
t ->
            Expr Void a
forall s a. Expr s a
TextShow Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VTextReplace Val a
a Val a
b Val a
c ->
            Expr Void a
forall s a. Expr s a
TextReplace Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
b Expr Void a -> Val a -> Expr Void a
`qApp` Val a
c
        VList Val a
t ->
            Expr Void a
forall s a. Expr s a
List Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListLit Maybe (Val a)
ma Seq (Val a)
ts ->
            Maybe (Expr Void a) -> Seq (Expr Void a) -> Expr Void a
forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
ListLit ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env) Maybe (Val a)
ma) ((Val a -> Expr Void a) -> Seq (Val a) -> Seq (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env) Seq (Val a)
ts)
        VListAppend Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
ListAppend (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VListBuild Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListBuild Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListFold Val a
a Val a
l Val a
t Val a
u Val a
v ->
            Expr Void a
forall s a. Expr s a
ListFold Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
l Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t Expr Void a -> Val a -> Expr Void a
`qApp` Val a
u Expr Void a -> Val a -> Expr Void a
`qApp` Val a
v
        VListLength Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListLength Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListHead Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListHead Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListLast Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListLast Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListIndexed Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListIndexed Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VListReverse Val a
a Val a
t ->
            Expr Void a
forall s a. Expr s a
ListReverse Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VOptional Val a
a ->
            Expr Void a
forall s a. Expr s a
Optional Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a
        VSome Val a
t ->
            Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a
Some (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t)
        VNone Val a
t ->
            Expr Void a
forall s a. Expr s a
None Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VRecord Map Text (Val a)
m ->
            Map Text (RecordField Void a) -> Expr Void a
forall s a. Map Text (RecordField s a) -> Expr s a
Record ((Val a -> RecordField Void a)
-> Map Text (Val a) -> Map Text (RecordField Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> RecordField Void a
quoteRecordField Map Text (Val a)
m)
        VRecordLit Map Text (Val a)
m ->
            Map Text (RecordField Void a) -> Expr Void a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit ((Val a -> RecordField Void a)
-> Map Text (Val a) -> Map Text (RecordField Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> RecordField Void a
quoteRecordField Map Text (Val a)
m)
        VUnion Map Text (Maybe (Val a))
m ->
            Map Text (Maybe (Expr Void a)) -> Expr Void a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union ((Maybe (Val a) -> Maybe (Expr Void a))
-> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env)) Map Text (Maybe (Val a))
m)
        VCombine Maybe Text
mk Val a
t Val a
u ->
            Maybe CharacterSet
-> Maybe Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
Maybe CharacterSet
-> Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine Maybe CharacterSet
forall a. Monoid a => a
mempty Maybe Text
mk (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VCombineTypes Val a
t Val a
u ->
            Maybe CharacterSet -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
CombineTypes Maybe CharacterSet
forall a. Monoid a => a
mempty (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VPrefer Val a
t Val a
u ->
            Maybe CharacterSet
-> PreferAnnotation Void a
-> Expr Void a
-> Expr Void a
-> Expr Void a
forall s a.
Maybe CharacterSet
-> PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer Maybe CharacterSet
forall a. Monoid a => a
mempty PreferAnnotation Void a
forall s a. PreferAnnotation s a
PreferFromSource (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VMerge Val a
t Val a
u Maybe (Val a)
ma ->
            Expr Void a -> Expr Void a -> Maybe (Expr Void a) -> Expr Void a
forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
Merge (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u) ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env) Maybe (Val a)
ma)
        VToMap Val a
t Maybe (Val a)
ma ->
            Expr Void a -> Maybe (Expr Void a) -> Expr Void a
forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
ToMap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env) Maybe (Val a)
ma)
        VField Val a
t Text
k ->
            Expr Void a -> FieldSelection Void -> Expr Void a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (FieldSelection Void -> Expr Void a)
-> FieldSelection Void -> Expr Void a
forall a b. (a -> b) -> a -> b
$ Text -> FieldSelection Void
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
k
        VProject Val a
t Either (Set Text) (Val a)
p ->
            Expr Void a -> Either [Text] (Expr Void a) -> Expr Void a
forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
Project (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) ((Set Text -> [Text])
-> Either (Set Text) (Expr Void a) -> Either [Text] (Expr Void a)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Set Text -> [Text]
forall a. Set a -> [a]
Dhall.Set.toList ((Val a -> Expr Void a)
-> Either (Set Text) (Val a) -> Either (Set Text) (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env) Either (Set Text) (Val a)
p))
        VAssert Val a
t ->
            Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a
Assert (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t)
        VEquivalent Val a
t Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
Equivalent (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
        VWith Val a
e NonEmpty Text
ks Val a
v ->
            Expr Void a -> NonEmpty Text -> Expr Void a -> Expr Void a
forall s a. Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
With (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
e) NonEmpty Text
ks (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
v)
        VInject Map Text (Maybe (Val a))
m Text
k Maybe (Val a)
Nothing ->
            Expr Void a -> FieldSelection Void -> Expr Void a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field (Map Text (Maybe (Expr Void a)) -> Expr Void a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union ((Maybe (Val a) -> Maybe (Expr Void a))
-> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env)) Map Text (Maybe (Val a))
m)) (FieldSelection Void -> Expr Void a)
-> FieldSelection Void -> Expr Void a
forall a b. (a -> b) -> a -> b
$ Text -> FieldSelection Void
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
k
        VInject Map Text (Maybe (Val a))
m Text
k (Just Val a
t) ->
            Expr Void a -> FieldSelection Void -> Expr Void a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field (Map Text (Maybe (Expr Void a)) -> Expr Void a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union ((Maybe (Val a) -> Maybe (Expr Void a))
-> Map Text (Maybe (Val a)) -> Map Text (Maybe (Expr Void a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Val a -> Expr Void a) -> Maybe (Val a) -> Maybe (Expr Void a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env)) Map Text (Maybe (Val a))
m)) (Text -> FieldSelection Void
forall s. Text -> FieldSelection s
Syntax.makeFieldSelection Text
k) Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VEmbed a
a ->
            a -> Expr Void a
forall s a. a -> Expr s a
Embed a
a
        Val a
VPrimVar ->
            String -> Expr Void a
forall a. HasCallStack => String -> a
error String
errorMsg
  where
    fresh :: Text -> (Text, Val a)
    fresh :: Text -> (Text, Val a)
fresh Text
x = (Text
x, Text -> Int -> Val a
forall a. Text -> Int -> Val a
VVar Text
x (Text -> Names -> Int
countNames Text
x Names
env))
    {-# INLINE fresh #-}

    freshClosure :: Closure a -> (Text, Val a, Closure a)
    freshClosure :: Closure a -> (Text, Val a, Closure a)
freshClosure closure :: Closure a
closure@(Closure Text
x Environment a
_ Expr Void a
_) = (Text
x, (Text, Val a) -> Val a
forall a b. (a, b) -> b
snd (Text -> (Text, Val a)
fresh Text
x), Closure a
closure)
    {-# INLINE freshClosure #-}

    quoteBind :: Text -> Val a -> Expr Void a
    quoteBind :: Text -> Val a -> Expr Void a
quoteBind Text
x = Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote (Names -> Text -> Names
Bind Names
env Text
x)
    {-# INLINE quoteBind #-}

    qApp :: Expr Void a -> Val a -> Expr Void a
    qApp :: Expr Void a -> Val a -> Expr Void a
qApp Expr Void a
t Val a
VPrimVar = Expr Void a
t
    qApp Expr Void a
t Val a
u        = Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
App Expr Void a
t (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
    {-# INLINE qApp #-}

    quoteRecordField :: Val a -> RecordField Void a
    quoteRecordField :: Val a -> RecordField Void a
quoteRecordField = Expr Void a -> RecordField Void a
forall s a. Expr s a -> RecordField s a
Syntax.makeRecordField (Expr Void a -> RecordField Void a)
-> (Val a -> Expr Void a) -> Val a -> RecordField Void a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env
    {-# INLINE quoteRecordField #-}

-- | Normalize an expression in an environment of values. Any variable pointing out of
--   the environment is treated as opaque free variable.
nf :: Eq a => Environment a -> Expr s a -> Expr t a
nf :: Environment a -> Expr s a -> Expr t a
nf !Environment a
env = Expr Void a -> Expr t a
forall a s. Expr Void a -> Expr s a
Syntax.renote (Expr Void a -> Expr t a)
-> (Expr s a -> Expr Void a) -> Expr s a -> Expr t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote (Environment a -> Names
forall a. Environment a -> Names
envNames Environment a
env) (Val a -> Expr Void a)
-> (Expr s a -> Val a) -> Expr s a -> Expr Void a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Val a)
-> (Expr s a -> Expr Void a) -> Expr s a -> Val a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr s a -> Expr Void a
forall s a t. Expr s a -> Expr t a
Syntax.denote

normalize :: Eq a => Expr s a -> Expr t a
normalize :: Expr s a -> Expr t a
normalize = Environment a -> Expr s a -> Expr t a
forall a s t. Eq a => Environment a -> Expr s a -> Expr t a
nf Environment a
forall a. Environment a
Empty

alphaNormalize :: Expr s a -> Expr s a
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize = Names -> Expr s a -> Expr s a
forall s a. Names -> Expr s a -> Expr s a
goEnv Names
EmptyNames
  where
    goVar :: Names -> Text -> Int -> Expr s a
    goVar :: Names -> Text -> Int -> Expr s a
goVar Names
e Text
topX Int
topI = Int -> Names -> Int -> Expr s a
forall s a. Int -> Names -> Int -> Expr s a
go Int
0 Names
e Int
topI
      where
        go :: Int -> Names -> Int -> Expr s a
go !Int
acc (Bind Names
env Text
x) !Int
i
          | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
topX = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
"_" Int
acc) else Int -> Names -> Int -> Expr s a
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Names
env (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          | Bool
otherwise = Int -> Names -> Int -> Expr s a
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Names
env Int
i
        go Int
_ Names
EmptyNames Int
i = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V Text
topX Int
i)

    goEnv :: Names -> Expr s a -> Expr s a
    goEnv :: Names -> Expr s a -> Expr s a
goEnv !Names
e0 Expr s a
t0 =
        case Expr s a
t0 of
            Const Const
k ->
                Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
k
            Var (V Text
x Int
i) ->
                Names -> Text -> Int -> Expr s a
forall s a. Names -> Text -> Int -> Expr s a
goVar Names
e0 Text
x Int
i
            Lam Maybe CharacterSet
cs (FunctionBinding Maybe s
src0 Text
x Maybe s
src1 Maybe s
src2 Expr s a
t) Expr s a
u ->
                Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
forall s a.
Maybe CharacterSet -> FunctionBinding s a -> Expr s a -> Expr s a
Lam Maybe CharacterSet
cs (Maybe s
-> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
forall s a.
Maybe s
-> Text -> Maybe s -> Maybe s -> Expr s a -> FunctionBinding s a
FunctionBinding Maybe s
src0 Text
"_" Maybe s
src1 Maybe s
src2 (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t)) (Text -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a
goBind Text
x Expr s a
u)
            Pi Maybe CharacterSet
cs Text
x Expr s a
a Expr s a
b ->
                Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
cs Text
"_" (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
a) (Text -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a
goBind Text
x Expr s a
b)
            App Expr s a
t Expr s a
u ->
                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
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Let (Binding Maybe s
src0 Text
x Maybe s
src1 Maybe (Maybe s, Expr s a)
mA Maybe s
src2 Expr s a
a) 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
"_" Maybe s
src1 (((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 Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go) Maybe (Maybe s, Expr s a)
mA) Maybe s
src2 (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
a)) (Text -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a
goBind Text
x Expr s a
b)
            Annot Expr s a
t Expr s a
u ->
                Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Annot (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Expr s a
Bool ->
                Expr s a
forall s a. Expr s a
Bool
            BoolLit Bool
b ->
                Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
b
            BoolAnd Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            BoolOr Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            BoolEQ Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            BoolNE Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            BoolIf Expr s a
b Expr s a
t Expr s a
f ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
b) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
f)
            Expr s a
Natural ->
                Expr s a
forall s a. Expr s a
Natural
            NaturalLit Natural
n ->
                Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
n
            Expr s a
NaturalFold ->
                Expr s a
forall s a. Expr s a
NaturalFold
            Expr s a
NaturalBuild ->
                Expr s a
forall s a. Expr s a
NaturalBuild
            Expr s a
NaturalIsZero ->
                Expr s a
forall s a. Expr s a
NaturalIsZero
            Expr s a
NaturalEven ->
                Expr s a
forall s a. Expr s a
NaturalEven
            Expr s a
NaturalOdd ->
                Expr s a
forall s a. Expr s a
NaturalOdd
            Expr s a
NaturalToInteger ->
                Expr s a
forall s a. Expr s a
NaturalToInteger
            Expr s a
NaturalShow ->
                Expr s a
forall s a. Expr s a
NaturalShow
            Expr s a
NaturalSubtract ->
                Expr s a
forall s a. Expr s a
NaturalSubtract
            NaturalPlus Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            NaturalTimes Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Expr s a
Integer ->
                Expr s a
forall s a. Expr s a
Integer
            IntegerLit Integer
n ->
                Integer -> Expr s a
forall s a. Integer -> Expr s a
IntegerLit Integer
n
            Expr s a
IntegerClamp ->
                Expr s a
forall s a. Expr s a
IntegerClamp
            Expr s a
IntegerNegate ->
                Expr s a
forall s a. Expr s a
IntegerNegate
            Expr s a
IntegerShow ->
                Expr s a
forall s a. Expr s a
IntegerShow
            Expr s a
IntegerToDouble ->
                Expr s a
forall s a. Expr s a
IntegerToDouble
            Expr s a
Double ->
                Expr s a
forall s a. Expr s a
Double
            DoubleLit DhallDouble
n ->
                DhallDouble -> Expr s a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n
            Expr s a
DoubleShow ->
                Expr s a
forall s a. Expr s a
DoubleShow
            Expr s a
Text ->
                Expr s a
forall s a. Expr s a
Text
            TextLit Chunks s a
cs ->
                Chunks s a -> Expr s a
forall s a. Chunks s a -> Expr s a
TextLit (Chunks s a -> Chunks s a
forall s a. Chunks s a -> Chunks s a
goChunks Chunks s a
cs)
            TextAppend Expr s a
t Expr s a
u ->
                Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Expr s a
TextShow ->
                Expr s a
forall s a. Expr s a
TextShow
            Expr s a
TextReplace ->
                Expr s a
forall s a. Expr s a
TextReplace
            Expr s a
List ->
                Expr s a
forall s a. Expr s a
List
            ListLit Maybe (Expr s a)
ma Seq (Expr s a)
ts ->
                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 -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Maybe (Expr s a)
ma) ((Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Seq (Expr s a)
ts)
            ListAppend Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Expr s a
ListBuild ->
                Expr s a
forall s a. Expr s a
ListBuild
            Expr s a
ListFold ->
                Expr s a
forall s a. Expr s a
ListFold
            Expr s a
ListLength ->
                Expr s a
forall s a. Expr s a
ListLength
            Expr s a
ListHead ->
                Expr s a
forall s a. Expr s a
ListHead
            Expr s a
ListLast ->
                Expr s a
forall s a. Expr s a
ListLast
            Expr s a
ListIndexed ->
                Expr s a
forall s a. Expr s a
ListIndexed
            Expr s a
ListReverse ->
                Expr s a
forall s a. Expr s a
ListReverse
            Expr s a
Optional ->
                Expr s a
forall s a. Expr s a
Optional
            Some Expr s a
t ->
                Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t)
            Expr s a
None ->
                Expr s a
forall s a. Expr s a
None
            Record Map Text (RecordField s a)
kts ->
                Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
Record (RecordField s a -> RecordField s a
forall s a. RecordField s a -> RecordField s a
goRecordField (RecordField s a -> RecordField s a)
-> Map Text (RecordField s a) -> Map Text (RecordField s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField s a)
kts)
            RecordLit Map Text (RecordField s a)
kts ->
                Map Text (RecordField s a) -> Expr s a
forall s a. Map Text (RecordField s a) -> Expr s a
RecordLit (RecordField s a -> RecordField s a
forall s a. RecordField s a -> RecordField s a
goRecordField (RecordField s a -> RecordField s a)
-> Map Text (RecordField s a) -> Map Text (RecordField s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField s a)
kts)
            Union Map Text (Maybe (Expr s a))
kts ->
                Map Text (Maybe (Expr s a)) -> Expr s a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union ((Maybe (Expr s a) -> Maybe (Expr s a))
-> Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go) Map Text (Maybe (Expr s a))
kts)
            Combine Maybe CharacterSet
cs Maybe Text
m Expr s a
t Expr s a
u ->
                Maybe CharacterSet
-> Maybe Text -> Expr s a -> Expr s a -> Expr s a
forall s a.
Maybe CharacterSet
-> Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine Maybe CharacterSet
cs Maybe Text
m (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            CombineTypes Maybe CharacterSet
cs Expr s a
t Expr s a
u ->
                Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
forall s a. Maybe CharacterSet -> Expr s a -> Expr s a -> Expr s a
CombineTypes Maybe CharacterSet
cs (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Prefer Maybe CharacterSet
cs PreferAnnotation s a
b Expr s a
t Expr s a
u ->
                Maybe CharacterSet
-> PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
forall s a.
Maybe CharacterSet
-> PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer Maybe CharacterSet
cs PreferAnnotation s a
b (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            RecordCompletion Expr s a
t Expr s a
u ->
                Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
RecordCompletion (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Merge Expr s a
x Expr s a
y Maybe (Expr s a)
ma ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
x) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
y) ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Maybe (Expr s a)
ma)
            ToMap Expr s a
x Maybe (Expr s a)
ma ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
x) ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Maybe (Expr s a)
ma)
            Field Expr s a
t FieldSelection s
k ->
                Expr s a -> FieldSelection s -> Expr s a
forall s a. Expr s a -> FieldSelection s -> Expr s a
Field (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) FieldSelection s
k
            Project Expr s a
t Either [Text] (Expr s a)
ks ->
                Expr s a -> Either [Text] (Expr s a) -> Expr s a
forall s a. Expr s a -> Either [Text] (Expr s a) -> Expr s a
Project (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) ((Expr s a -> Expr s a)
-> Either [Text] (Expr s a) -> Either [Text] (Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Either [Text] (Expr s a)
ks)
            Assert Expr s a
t ->
                Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Assert (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t)
            Equivalent Expr s a
t Expr s a
u ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            With Expr s a
e NonEmpty Text
k Expr s a
v ->
                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 -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
e) NonEmpty Text
k (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
v)
            Note s
s Expr s a
e ->
                s -> Expr s a -> Expr s a
forall s a. s -> Expr s a -> Expr s a
Note s
s (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
e)
            ImportAlt Expr s a
t Expr s a
u ->
                Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
ImportAlt (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
            Embed a
a ->
                a -> Expr s a
forall s a. a -> Expr s a
Embed a
a
      where
        go :: Expr s a -> Expr s a
go                     = Names -> Expr s a -> Expr s a
forall s a. Names -> Expr s a -> Expr s a
goEnv Names
e0
        goBind :: Text -> Expr s a -> Expr s a
goBind Text
x               = Names -> Expr s a -> Expr s a
forall s a. Names -> Expr s a -> Expr s a
goEnv (Names -> Text -> Names
Bind Names
e0 Text
x)
        goChunks :: Chunks s a -> Chunks s a
goChunks (Chunks [(Text, Expr s a)]
ts Text
x) = [(Text, Expr s a)] -> Text -> Chunks s a
forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
Chunks (((Text, Expr s a) -> (Text, Expr s a))
-> [(Text, Expr s a)] -> [(Text, Expr s a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> (Text, Expr s a) -> (Text, Expr s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go) [(Text, Expr s a)]
ts) Text
x
        goRecordField :: RecordField s a -> RecordField s a
goRecordField (RecordField Maybe s
s0 Expr s a
e Maybe s
s1 Maybe s
s2) = Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
forall s a.
Maybe s -> Expr s a -> Maybe s -> Maybe s -> RecordField s a
RecordField Maybe s
s0 (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
e) Maybe s
s1 Maybe s
s2