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

{-# 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.Foldable (foldr', toList)
import Data.Semigroup (Semigroup(..))
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(..)
  , Expr(..)
  , Chunks(..)
  , Const(..)
  , DhallDouble(..)
  , PreferAnnotation(..)
  , Var(..)
  )

import qualified Data.Char
import qualified Data.Sequence   as Sequence
import qualified Data.Set
import qualified Data.Text       as Text
import qualified Dhall.Syntax    as Syntax
import qualified Dhall.Map       as Map
import qualified Dhall.Set
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

#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

{-| 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)

    | 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)
    | 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
0 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 :: 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 #-}

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)

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 Text
x 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 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
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 (Expr 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 ((Expr Void a -> Val a)
-> Map Text (Expr Void a) -> Map Text (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 (Expr Void a)
kts))
        RecordLit Map Text (Expr 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 ((Expr Void a -> Val a)
-> Map Text (Expr Void a) -> Map Text (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 (Expr 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 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 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 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 (PreferAnnotation Void a
-> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation Void a
forall s a. PreferAnnotation s a
PreferFromCompletion (Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> Expr s a
Field Expr Void a
t Text
"default") Expr Void a
u) (Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> Expr s a
Field Expr Void a
t 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 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 Set 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 Set 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 -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Either (Set Text) (Expr Void a) -> Expr Void a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project Expr Void a
t (Set Text -> Either (Set Text) (Expr Void a)
forall a b. a -> Either a b
Left (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)
        e :: Expr Void a
e@With{} ->
            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
forall s a. Expr s a -> Expr s a
Syntax.desugarWith Expr Void a
e)
        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'
        (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)) ->
            Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam 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 -> Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam 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)) ->
            Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi 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 ->
            Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi 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
        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 (Expr Void a) -> Expr Void a
forall s a. Map Text (Expr s a) -> Expr s a
Record ((Val a -> Expr Void a)
-> Map Text (Val a) -> Map 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) Map Text (Val a)
m)
        VRecordLit Map Text (Val a)
m ->
            Map Text (Expr Void a) -> Expr Void a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit ((Val a -> Expr Void a)
-> Map Text (Val a) -> Map 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) 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 Text -> Expr Void a -> Expr Void a -> Expr Void a
forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine 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 ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
CombineTypes (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 ->
            PreferAnnotation Void a
-> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer 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 -> Text -> Expr Void a
forall s a. Expr s a -> Text -> 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) Text
k
        VProject Val a
t Either (Set Text) (Val a)
p ->
            Expr Void a -> Either (Set Text) (Expr Void a) -> Expr Void a
forall s a. Expr s a -> Either (Set 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) ((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)
        VInject Map Text (Maybe (Val a))
m Text
k Maybe (Val a)
Nothing ->
            Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> 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
k
        VInject Map Text (Maybe (Val a))
m Text
k (Just Val a
t) ->
            Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> 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
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 #-}

-- | 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 Text
x Expr s a
t Expr s a
u ->
                Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam Text
"_" (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 Text
x Expr s a
a Expr s a
b ->
                Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi Text
"_" (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
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 (Expr s a)
kts ->
                Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
Record ((Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map 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 Map Text (Expr s a)
kts)
            RecordLit Map Text (Expr s a)
kts ->
                Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
RecordLit ((Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map 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 Map Text (Expr 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 Text
m Expr s a
t Expr s a
u ->
                Maybe Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
Combine Maybe Text
m (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
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 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
CombineTypes (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 PreferAnnotation s a
b Expr s a
t Expr s a
u ->
                PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation s a
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 Text
k ->
                Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) Text
k
            Project Expr s a
t Either (Set Text) (Expr s a)
ks ->
                Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
Project (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) ((Expr s a -> Expr s a)
-> Either (Set Text) (Expr s a) -> Either (Set 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 (Set 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