{-# 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.Syntax
  ( Binding(..)
  , Expr(..)
  , Chunks(..)
  , Const(..)
  , DhallDouble(..)
  , Var(..)
  )

import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Prelude hiding (succ)

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
<> ": Compiler bug                                                        "
  , "                                                                                "
  , "An ill-typed expression was encountered during normalization.                   "
  , "Explanation: This error message means that there is a bug in the Dhall compiler."
  , "You didn't do anything wrong, but if you would like to see this problem fixed   "
  , "then you should report the bug at:                                              "
  , "                                                                                "
  , "https://github.com/dhall-lang/dhall-haskell/issues                              "
  ]
  where
    _ERROR :: String
    _ERROR :: String
_ERROR = "\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 xys :: [(Text, Val a)]
xys z :: Text
z <> :: VChunks a -> VChunks a -> VChunks a
<> VChunks [] z' :: 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 xys :: [(Text, Val a)]
xys z :: Text
z <> VChunks ((x' :: Text
x', y' :: Val a
y'):xys' :: [(Text, Val a)]
xys') z' :: 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 a :: Val a
a b :: Closure a
b@(Closure x :: Text
x _ _)) = (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 x :: Text
x a :: Val a
a b :: 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  _                        = 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)
    | VOptionalFold (Val a) !(Val a) (Val a) !(Val a) !(Val a)
    | VOptionalBuild (Val a) !(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
(~>) a :: Val a
a b :: Val a
b = Text -> Val a -> (Val a -> Val a) -> Val a
forall a. Text -> Val a -> (Val a -> Val a) -> Val a
VHPi "_" Val a
a (\_ -> Val a
b)
{-# INLINE (~>) #-}

infixr 5 ~>

countEnvironment :: Text -> Environment a -> Int
countEnvironment :: Text -> Environment a -> Int
countEnvironment x :: Text
x = Int -> Environment a -> Int
forall a a. Num a => a -> Environment a -> a
go (0 :: Int)
  where
    go :: a -> Environment a -> a
go !a
acc Empty             = a
acc
    go  acc :: a
acc (Skip env :: Environment a
env x' :: 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
+ 1 else a
acc) Environment a
env
    go  acc :: a
acc (Extend env :: Environment a
env x' :: 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
+ 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 x :: Text
x env :: Environment a
env t :: 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 env0 :: Environment a
env0 (V x :: Text
x i0 :: 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 env :: Environment a
env x' :: Text
x' v :: Val a
v) i :: 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
== 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
- 1)
        | Bool
otherwise =
            Environment a -> Int -> Val a
go Environment a
env Int
i
    go (Skip env :: Environment a
env x' :: Text
x') i :: 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
== 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
- 1)
        | Bool
otherwise =
            Environment a -> Int -> Val a
go Environment a
env Int
i
    go Empty i :: Int
i =
        Text -> Int -> Val a
forall a. Text -> Int -> Val a
VVar Text
x (0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 _ t' :: 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 _ t' :: Val a -> Val a
t' -> Val a -> Val a
t' Val a
u
        t' :: 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 env :: Environment a
env t :: Val a
t u :: Val a
u =
    case (Val a
t, Val a
u) of
        (VRecordLit m :: Map Text (Val a)
m, u' :: 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'
        (t' :: Val a
t', VRecordLit m :: 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 m :: Map Text (Val a)
m, VRecordLit m' :: 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)
        (t' :: Val a
t', u' :: 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'
        (t' :: Val a
t', u' :: 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 mk :: Maybe Text
mk t :: Val a
t u :: Val a
u =
    case (Val a
t, Val a
u) of
        (VRecordLit m :: Map Text (Val a)
m, u' :: 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'
        (t' :: Val a
t', VRecordLit m :: 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 m :: Map Text (Val a)
m, VRecordLit m' :: 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')
        (t' :: Val a
t', u' :: 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 t :: Val a
t u :: Val a
u =
    case (Val a
t, Val a
u) of
        (VRecord m :: Map Text (Val a)
m, u' :: 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'
        (t' :: Val a
t', VRecord m :: 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 m :: Map Text (Val a)
m, VRecord m' :: 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')
        (t' :: Val a
t', u' :: 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 t :: Val a
t u :: Val a
u =
    case (Val a
t, Val a
u) of
        (VListLit _ xs :: Seq (Val a)
xs, u' :: Val a
u') | Seq (Val a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Val a)
xs ->
            Val a
u'
        (t' :: Val a
t', VListLit _ ys :: 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 t' :: Maybe (Val a)
t' xs :: Seq (Val a)
xs, VListLit _ ys :: 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)
        (t' :: Val a
t', u' :: 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 t :: Val a
t u :: Val a
u =
    case (Val a
t, Val a
u) of
        (VNaturalLit 0, u' :: Val a
u') ->
            Val a
u'
        (t' :: Val a
t', VNaturalLit 0) ->
            Val a
t'
        (VNaturalLit m :: Natural
m, VNaturalLit n :: 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)
        (t' :: Val a
t', u' :: 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 t0 :: Val a
t0 k :: 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 m :: 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
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 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
            _             -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
        VRecordLit m :: Map Text (Val a)
m
            | Just v :: 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 t :: Val a
t _ -> Val a -> Val a
go Val a
t
        VPrefer (VRecordLit m :: Map Text (Val a)
m) r :: 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 v :: 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
            Nothing -> Val a -> Val a
go Val a
r
        VPrefer l :: Val a
l (VRecordLit m :: 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 v :: Val a
v -> Val a
v
            Nothing -> Val a -> Val a
go Val a
l
        VCombine mk :: Maybe Text
mk (VRecordLit m :: Map Text (Val a)
m) r :: 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 v :: 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
            Nothing -> Val a -> Val a
go Val a
r
        VCombine mk :: Maybe Text
mk l :: Val a
l (VRecordLit m :: 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 v :: 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
            Nothing -> Val a -> Val a
go Val a
l
        t :: 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 v :: 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 env :: Environment a
env t :: Val a
t ks :: 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 kvs :: 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 t' :: Val a
t' _ ->
                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 l :: Val a
l (VRecordLit kvs :: 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')
            t' :: 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 t0 :: Expr Void a
t0 =
    case Expr Void a
t0 of
        Const k :: Const
k ->
            Const -> Val a
forall a. Const -> Val a
VConst Const
k
        Var v :: Var
v ->
            Environment a -> Var -> Val a
forall a. Environment a -> Var -> Val a
vVar Environment a
env Var
v
        Lam x :: Text
x a :: Expr Void a
a t :: 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 x :: Text
x a :: Expr Void a
a b :: 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 t :: Expr Void a
t u :: 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 _ x :: Text
x _ _mA :: Maybe (Maybe Void, Expr Void a)
_mA _ a :: Expr Void a
a) b :: 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 t :: 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
t
        Bool ->
            Val a
forall a. Val a
VBool
        BoolLit b :: Bool
b ->
            Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
b
        BoolAnd t :: Expr Void a
t u :: 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 True, u' :: Val a
u')       -> Val a
u'
                (VBoolLit False, _)       -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
False
                (t' :: Val a
t', VBoolLit True)       -> Val a
t'
                (_ , VBoolLit False)      -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
False
                (t' :: Val a
t', u' :: 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'
                (t' :: Val a
t', u' :: 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 t :: Expr Void a
t u :: 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 False, u' :: Val a
u')      -> Val a
u'
                (VBoolLit True, _)        -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
True
                (t' :: Val a
t', VBoolLit False)      -> Val a
t'
                (_ , VBoolLit True)       -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit Bool
True
                (t' :: Val a
t', u' :: 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'
                (t' :: Val a
t', u' :: 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 t :: Expr Void a
t u :: 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 True, u' :: Val a
u')       -> Val a
u'
                (t' :: Val a
t', VBoolLit True)       -> Val a
t'
                (t' :: Val a
t', u' :: 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
                (t' :: Val a
t', u' :: 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 t :: Expr Void a
t u :: 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 False, u' :: Val a
u')      -> Val a
u'
                (t' :: Val a
t', VBoolLit False)      -> Val a
t'
                (t' :: Val a
t', u' :: 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
                (t' :: Val a
t', u' :: 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 b :: Expr Void a
b t :: Expr Void a
t f :: 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 True,  t' :: Val a
t', _ )            -> Val a
t'
                (VBoolLit False, _ , f' :: Val a
f')            -> Val a
f'
                (b' :: Val a
b', VBoolLit True, VBoolLit False) -> Val a
b'
                (_, t' :: Val a
t', f' :: 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'
                (b' :: Val a
b', t' :: Val a
t', f' :: 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'
        Natural ->
            Val a
forall a. Val a
VNatural
        NaturalLit n :: Natural
n ->
            Natural -> Val a
forall a. Natural -> Val a
VNaturalLit Natural
n
        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
$ \case
                VNaturalLit n :: Natural
n ->
                    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 "natural" (Const -> Val a
forall a. Const -> Val a
VConst Const
Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \natural :: Val a
natural ->
                    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 "succ" (Val a
natural Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
~> Val a
natural)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \succ :: Val a
succ ->
                    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 "zero" Val a
natural) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \zero :: Val a
zero ->
                    let go :: Val a -> t -> Val a
go !Val a
acc 0 = Val a
acc
                        go  acc :: Val a
acc m :: 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
- 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)
                n :: 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
$ \natural :: 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
$ \succ :: 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
$ \zero :: Val a
zero ->
                    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
        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
                VPrimVar ->
                    Val a -> Val a
forall a. Val a -> Val a
VNaturalBuild Val a
forall a. Val a
VPrimVar
                t :: 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 "n" Val a
forall a. Val a
VNatural) (\n :: 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 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 0

        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 n :: Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 0)
            n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalIsZero Val a
n
        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 n :: Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural -> Bool
forall a. Integral a => a -> Bool
even Natural
n)
            n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalEven Val a
n
        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 n :: Natural
n -> Bool -> Val a
forall a. Bool -> Val a
VBoolLit (Natural -> Bool
forall a. Integral a => a -> Bool
odd Natural
n)
            n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalOdd Val a
n
        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 n :: 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)
            n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalToInteger Val a
n
        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 n :: 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)))
            n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VNaturalShow Val a
n
        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 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 m :: 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 n :: Natural
n
                        | Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
m    -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
subtract Natural
m Natural
n)
                        | Bool
otherwise -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit 0
                    y :: Val a
y -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalSubtract Val a
x Val a
y
            x :: 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 0    -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit 0
                    y :: 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 0
                    y :: 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 t :: Expr Void a
t u :: 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 t :: Expr Void a
t u :: 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 1, u' :: Val a
u'           ) -> Val a
u'
                (t' :: Val a
t'           , VNaturalLit 1) -> Val a
t'
                (VNaturalLit 0, _            ) -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit 0
                (_            , VNaturalLit 0) -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit 0
                (VNaturalLit m :: Natural
m, VNaturalLit n :: 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)
                (t' :: Val a
t'           , u' :: Val a
u'           ) -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VNaturalTimes Val a
t' Val a
u'
        Integer ->
            Val a
forall a. Val a
VInteger
        IntegerLit n :: Integer
n ->
            Integer -> Val a
forall a. Integer -> Val a
VIntegerLit Integer
n
        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 n :: Integer
n
                    | 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 0
                n :: Val a
n -> Val a -> Val a
forall a. Val a -> Val a
VIntegerClamp Val a
n
        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 n :: Integer
n -> Integer -> Val a
forall a. Integer -> Val a
VIntegerLit (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n)
                n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VIntegerNegate Val a
n
        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 n :: Integer
n
                    | 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 -> 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)))
                n :: Val a
n -> Val a -> Val a
forall a. Val a -> Val a
VIntegerShow Val a
n
        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 n :: 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.
                n :: Val a
n             -> Val a -> Val a
forall a. Val a -> Val a
VIntegerToDouble Val a
n
        Double ->
            Val a
forall a. Val a
VDouble
        DoubleLit n :: DhallDouble
n ->
            DhallDouble -> Val a
forall a. DhallDouble -> Val a
VDoubleLit DhallDouble
n
        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 n :: 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)))
                n :: Val a
n                          -> Val a -> Val a
forall a. Val a -> Val a
VDoubleShow Val a
n
        Text ->
            Val a
forall a. Val a
VText
        TextLit cs :: Chunks Void a
cs ->
            case Chunks Void a -> VChunks a
evalChunks Chunks Void a
cs of
                VChunks [("", t :: Val a
t)] "" -> Val a
t
                vcs :: VChunks a
vcs                  -> VChunks a -> Val a
forall a. VChunks a -> Val a
VTextLit VChunks a
vcs
        TextAppend t :: Expr Void a
t u :: 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 [("", Expr Void a
t), ("", Expr Void a
u)] ""))
        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 [] x :: 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))
                t :: Val a
t                       -> Val a -> Val a
forall a. Val a -> Val a
VTextShow Val a
t
        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 ma :: Maybe (Expr Void a)
ma ts :: 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 t :: Expr Void a
t u :: 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)
        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
$ \a :: 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
                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
                t :: 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 "a" Val a
a) (\x :: 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 "as" (Val a -> Val a
forall a. Val a -> Val a
VList Val a
a)) (\as :: 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

        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
$ \a :: 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 _ as :: Seq (Val a)
as ->
                    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 "list" (Const -> Val a
forall a. Const -> Val a
VConst Const
Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \list :: Val a
list ->
                    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 "cons" (Val a
a Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
~> Val a
list Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
~> Val a
list) ) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \cons :: Val a
cons ->
                    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 "nil"  Val a
list) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \nil :: Val a
nil ->
                    (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' (\x :: Val a
x b :: 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
                as :: 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
$ \t :: Val a
t ->
                    (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
$ \c :: Val a
c ->
                    (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
$ \n :: Val a
n ->
                    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
t Val a
c Val a
n
        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
$ \ a :: 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 _ as :: 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))
                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
        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
$ \ a :: 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 _ as :: Seq (Val a)
as ->
                    case Seq (Val a) -> ViewL (Val a)
forall a. Seq a -> ViewL a
Sequence.viewl Seq (Val a)
as of
                        y :: Val a
y :< _ -> Val a -> Val a
forall a. Val a -> Val a
VSome Val a
y
                        _      -> Val a -> Val a
forall a. Val a -> Val a
VNone Val a
a
                as :: Val a
as ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListHead Val a
a Val a
as
        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
$ \ a :: 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 _ as :: Seq (Val a)
as ->
                    case Seq (Val a) -> ViewR (Val a)
forall a. Seq a -> ViewR a
Sequence.viewr Seq (Val a)
as of
                        _ :> t :: Val a
t -> Val a -> Val a
forall a. Val a -> Val a
VSome Val a
t
                        _      -> Val a -> Val a
forall a. Val a -> Val a
VNone Val a
a
                as :: Val a
as -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListLast Val a
a Val a
as
        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
$ \ a :: 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 _ as :: 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 [("index", Val a
forall a. Val a
VNatural), ("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
                                (\i :: Int
i t :: 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
                                            [ ("index", Natural -> Val a
forall a. Natural -> Val a
VNaturalLit (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
                                            , ("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'
                t :: Val a
t ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListIndexed Val a
a Val a
t
        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 t :: Maybe (Val a)
t as :: 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 _ as :: 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)
                t :: Val a
t ->
                    Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VListReverse Val a
a Val a
t
        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 t :: 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)
        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
        OptionalFold ->
            (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
                VNone _ ->
                    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 "optional" (Const -> Val a
forall a. Const -> Val a
VConst Const
Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \optional :: Val a
optional ->
                    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 "some" (Val a
a Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
~> Val a
optional)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \_some :: Val a
_some ->
                    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 "none" Val a
optional) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \none :: Val a
none ->
                    Val a
none
                VSome t :: Val a
t ->
                    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 "optional" (Const -> Val a
forall a. Const -> Val a
VConst Const
Type)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \optional :: Val a
optional ->
                    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 "some" (Val a
a Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
~> Val a
optional)) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \some :: Val a
some ->
                    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 "none" Val a
optional) ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \_none :: Val a
_none ->
                    Val a
some Val a -> Val a -> Val a
forall a. Eq a => Val a -> Val a -> Val a
`vApp` Val a
t
                opt :: Val a
opt ->
                    (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
$ \o :: Val a
o ->
                    (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
$ \s :: Val a
s ->
                    (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
$ \n :: Val a
n ->
                    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
VOptionalFold Val a
a Val a
opt Val a
o Val a
s Val a
n
        OptionalBuild ->
            (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
                VPrimVar -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a
VOptionalBuild Val a
a Val a
forall a. Val a
VPrimVar
                t :: 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
VOptional 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 "a" Val a
a) Val a -> Val a
forall a. Val a -> Val a
VSome
                    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
VNone Val a
a
        Record kts :: 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 kts :: 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 kts :: 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 mk :: Maybe Text
mk t :: Expr Void a
t u :: 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 t :: Expr Void a
t u :: 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 t :: Expr Void a
t u :: 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 t :: Expr Void a
t u :: 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 (Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer (Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> Expr s a
Field Expr Void a
t "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 "Type"))
        Merge x :: Expr Void a
x y :: Expr Void a
y ma :: 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 m :: Map Text (Val a)
m, VInject _ k :: Text
k mt :: Maybe (Val a)
mt, _)
                    | Just f :: 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 m :: Map Text (Val a)
m, VSome t :: Val a
t, _)
                    | Just f :: Val a
f <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup "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 m :: Map Text (Val a)
m, VNone _, _)
                    | Just t :: Val a
t <- Text -> Map Text (Val a) -> Maybe (Val a)
forall k v. Ord k => k -> Map k v -> Maybe v
Map.lookup "None" Map Text (Val a)
m -> Val a
t
                    | Bool
otherwise                     -> String -> Val a
forall a. HasCallStack => String -> a
error String
errorMsg
                (x' :: Val a
x', y' :: Val a
y', ma' :: 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 x :: Expr Void a
x ma :: 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 m :: Map Text (Val a)
m, ma' :: Maybe (Val a)
ma'@(Just _)) | 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 m :: Map Text (Val a)
m, _) ->
                    let entry :: (Text, Val a) -> Val a
entry (k :: Text
k, v :: 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
                                    [ ("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)
                                    , ("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
                (x' :: Val a
x', ma' :: 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 t :: Expr Void a
t k :: 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 t :: Expr Void a
t (Left ks :: 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 t :: Expr Void a
t (Right e :: 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 kts :: 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))))
                e' :: 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 t :: 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 t :: Expr Void a
t u :: 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)
        Note _ e :: 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 t :: 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
t
        Embed a :: 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 xys :: [(Text, Expr Void a)]
xys z :: 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 (x :: Text
x, t :: Expr Void a
t) vcs :: 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 vcs' :: 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
                t' :: 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 f :: a -> a -> Bool
f = [a] -> [a] -> Bool
go
  where
    go :: [a] -> [a] -> Bool
go (x :: a
x:xs :: [a]
xs) (y :: a
y:ys :: [a]
ys) | a -> a -> Bool
f a
x a
y = [a] -> [a] -> Bool
go [a]
xs [a]
ys
    go [] [] = Bool
True
    go _  _  = 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 f :: v -> v -> Bool
f mL :: Map k v
mL mR :: 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 (kL :: a
kL, vL :: v
vL) (kR :: a
kR, vR :: 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 f :: a -> a -> Bool
f = Maybe a -> Maybe a -> Bool
go
  where
    go :: Maybe a -> Maybe a -> Bool
go (Just x :: a
x) (Just y :: a
y) = a -> a -> Bool
f a
x a
y
    go Nothing  Nothing  = Bool
True
    go _        _        = 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
<> "\""
  where
    f :: Char -> Text
f '"'  = "\\\""
    f '$'  = "\\u0024"
    f '\\' = "\\\\"
    f '\b' = "\\b"
    f '\n' = "\\n"
    f '\r' = "\\r"
    f '\t' = "\\t"
    f '\f' = "\\f"
    f c :: Char
c | Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= '\x1F' = String -> Text
Text.pack (String -> Int -> String
forall r. PrintfType r => String -> r
Text.Printf.printf "\\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 t0 :: Val a
t0 t0' :: Val a
t0' =
    case (Val a
t0, Val a
t0') of
        (VConst k :: Const
k, VConst k' :: Const
k') ->
            Const
k Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
k'
        (VVar x :: Text
x i :: Int
i, VVar x' :: Text
x' i' :: 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 _ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t :: Closure a
t)), VLam _ t' :: 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 _ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t :: Closure a
t)), VHLam _ t' :: 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 _ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t :: Closure a
t)), 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 _ t :: Val a -> Val a
t, VLam _ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t' :: 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 _ t :: Val a -> Val a
t, VHLam _ t' :: Val a -> Val a
t'                    ) ->
            let (x :: Text
x, v :: Val a
v) = Text -> (Text, Val a)
fresh "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 _ t :: Val a -> Val a
t, t' :: Val a
t'                            ) ->
            let (x :: Text
x, v :: Val a
v) = Text -> (Text, Val a)
fresh "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)
        (t :: Val a
t, VLam _ (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t' :: 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)
        (t :: Val a
t, VHLam _ t' :: Val a -> Val a
t'  ) ->
            let (x :: Text
x, v :: Val a
v) = Text -> (Text, Val a)
fresh "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 t :: Val a
t u :: Val a
u, VApp t' :: Val a
t' u' :: 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 a :: Val a
a b :: Closure a
b, VPi a' :: Val a
a' (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, b' :: 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 a :: Val a
a b :: Closure a
b, VHPi (Text -> (Text, Val a)
fresh -> (x :: Text
x, v :: Val a
v)) a' :: Val a
a' b' :: 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 _ a :: Val a
a b :: Val a -> Val a
b, VPi a' :: Val a
a' (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, b' :: 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 _ a :: Val a
a b :: Val a -> Val a
b, VHPi (Text -> (Text, Val a)
fresh -> (x :: Text
x, v :: Val a
v)) a' :: Val a
a' b' :: 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)
        (VBool, VBool) ->
            Bool
True
        (VBoolLit b :: Bool
b, VBoolLit b' :: Bool
b') ->
            Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b'
        (VBoolAnd t :: Val a
t u :: Val a
u, VBoolAnd t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VBoolOr t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VBoolEQ t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VBoolNE t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u v :: Val a
v, VBoolIf t' :: Val a
t' u' :: Val a
u' v' :: 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'
        (VNatural, VNatural) ->
            Bool
True
        (VNaturalLit n :: Natural
n, VNaturalLit n' :: Natural
n') ->
            Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n'
        (VNaturalFold t :: Val a
t _ u :: Val a
u v :: Val a
v, VNaturalFold t' :: Val a
t' _ u' :: Val a
u' v' :: 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 t :: Val a
t, VNaturalBuild t' :: 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 t :: Val a
t, VNaturalIsZero t' :: 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 t :: Val a
t, VNaturalEven t' :: 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 t :: Val a
t, VNaturalOdd t' :: 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 t :: Val a
t, VNaturalToInteger t' :: 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 t :: Val a
t, VNaturalShow t' :: 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 x :: Val a
x y :: Val a
y, VNaturalSubtract x' :: Val a
x' y' :: 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 t :: Val a
t u :: Val a
u, VNaturalPlus t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VNaturalTimes t' :: Val a
t' u' :: 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'
        (VInteger, VInteger) ->
            Bool
True
        (VIntegerLit t :: Integer
t, VIntegerLit t' :: Integer
t') ->
            Integer
t Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
t'
        (VIntegerClamp t :: Val a
t, VIntegerClamp t' :: 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 t :: Val a
t, VIntegerNegate t' :: 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 t :: Val a
t, VIntegerShow t' :: 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 t :: Val a
t, VIntegerToDouble t' :: 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'
        (VDouble, VDouble) ->
            Bool
True
        (VDoubleLit n :: DhallDouble
n, VDoubleLit n' :: DhallDouble
n') ->
            DhallDouble
n DhallDouble -> DhallDouble -> Bool
forall a. Eq a => a -> a -> Bool
== DhallDouble
n'
        (VDoubleShow t :: Val a
t, VDoubleShow t' :: 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'
        (VText, VText) ->
            Bool
True
        (VTextLit cs :: VChunks a
cs, VTextLit cs' :: VChunks a
cs') ->
            VChunks a -> VChunks a -> Bool
convChunks VChunks a
cs VChunks a
cs'
        (VTextAppend t :: Val a
t u :: Val a
u, VTextAppend t' :: Val a
t' u' :: 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 t :: Val a
t, VTextShow t' :: 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 a :: Val a
a, VList a' :: 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 _ xs :: Seq (Val a)
xs, VListLit _ xs' :: 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 t :: Val a
t u :: Val a
u, VListAppend t' :: Val a
t' u' :: 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 _ t :: Val a
t, VListBuild _ t' :: 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 a :: Val a
a t :: Val a
t, VListLength a' :: Val a
a' t' :: 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 _ t :: Val a
t, VListHead _ t' :: 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 _ t :: Val a
t, VListLast _ t' :: 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 _ t :: Val a
t, VListIndexed _ t' :: 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 _ t :: Val a
t, VListReverse _ t' :: 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 a :: Val a
a l :: Val a
l _ t :: Val a
t u :: Val a
u, VListFold a' :: Val a
a' l' :: Val a
l' _ t' :: Val a
t' u' :: 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 a :: Val a
a, VOptional a' :: 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 t :: Val a
t, VSome t' :: 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 _, VNone _) ->
            Bool
True
        (VOptionalBuild _ t :: Val a
t, VOptionalBuild _ t' :: 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'
        (VRecord m :: Map Text (Val a)
m, VRecord m' :: 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 m :: Map Text (Val a)
m, VRecordLit m' :: 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 m :: Map Text (Maybe (Val a))
m, VUnion m' :: 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 _ t :: Val a
t u :: Val a
u, VCombine _ t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VCombineTypes t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u, VPrefer t' :: Val a
t' u' :: 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 t :: Val a
t u :: Val a
u _, VMerge t' :: Val a
t' u' :: 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'
        (VToMap t :: Val a
t _, VToMap t' :: 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'
        (VField t :: Val a
t k :: Text
k, VField t' :: Val a
t' k' :: 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 t :: Val a
t (Left ks :: Set Text
ks), VProject t' :: Val a
t' (Left ks' :: 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 t :: Val a
t (Right e :: Val a
e), VProject t' :: Val a
t' (Right e' :: 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 t :: Val a
t, VAssert t' :: 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 t :: Val a
t u :: Val a
u, VEquivalent t' :: Val a
t' u' :: 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 m :: Map Text (Maybe (Val a))
m k :: Text
k mt :: Maybe (Val a)
mt, VInject m' :: Map Text (Maybe (Val a))
m' k' :: Text
k' mt' :: 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
a, VEmbed a' :: a
a') ->
            a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a'
        (VOptionalFold a :: Val a
a t :: Val a
t _ u :: Val a
u v :: Val a
v, VOptionalFold a' :: Val a
a' t' :: Val a
t' _ u' :: Val a
u' v' :: 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
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' 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'
        (_, _) ->
            Bool
False
  where
    fresh :: Text -> (Text, Val a)
    fresh :: Text -> (Text, Val a)
fresh x :: 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 x :: Text
x _ _) = (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 xys :: [(Text, Val a)]
xys z :: Text
z) (VChunks xys' :: [(Text, Val a)]
xys' z' :: 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 (\(x :: Text
x, y :: Val a
y) (x' :: Text
x', y' :: 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 x :: 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 Empty = Names
EmptyNames
envNames (Skip   env :: Environment a
env x :: Text
x  ) = Names -> Text -> Names
Bind (Environment a -> Names
forall a. Environment a -> Names
envNames Environment a
env) Text
x
envNames (Extend env :: Environment a
env x :: Text
x _) = 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 x :: Text
x = Int -> Names -> Int
forall t. Num t => t -> Names -> t
go 0
  where
    go :: t -> Names -> t
go !t
acc EmptyNames         = t
acc
    go  acc :: t
acc (Bind env :: Names
env x' :: 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
+ 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 k :: 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
- 1))
        VApp t :: Val a
t u :: 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 a :: Val a
a (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, t :: 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 i :: HLamInfo a
i t :: Val a -> Val a
t ->
            case HLamInfo a
i of
                Typed (Text -> (Text, Val a)
fresh -> (x :: Text
x, v :: Val a
v)) a :: 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))
                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)
                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 0)

        VPi a :: Val a
a (Closure a -> (Text, Val a, Closure a)
freshClosure -> (x :: Text
x, v :: Val a
v, b :: 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 -> (x :: Text
x, v :: Val a
v)) a :: Val a
a b :: 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))
        VBool ->
            Expr Void a
forall s a. Expr s a
Bool
        VBoolLit b :: Bool
b ->
            Bool -> Expr Void a
forall s a. Bool -> Expr s a
BoolLit Bool
b
        VBoolAnd t :: Val a
t u :: 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 t :: Val a
t u :: 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 t :: Val a
t u :: 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 t :: Val a
t u :: 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 t :: Val a
t u :: Val a
u v :: 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)
        VNatural ->
            Expr Void a
forall s a. Expr s a
Natural
        VNaturalLit n :: Natural
n ->
            Natural -> Expr Void a
forall s a. Natural -> Expr s a
NaturalLit Natural
n
        VNaturalFold a :: Val a
a t :: Val a
t u :: Val a
u v :: 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 t :: 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 t :: 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 t :: 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 t :: 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 t :: 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 t :: 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 t :: Val a
t u :: 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 t :: Val a
t u :: 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 x :: Val a
x y :: 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
        VInteger ->
            Expr Void a
forall s a. Expr s a
Integer
        VIntegerLit n :: Integer
n ->
            Integer -> Expr Void a
forall s a. Integer -> Expr s a
IntegerLit Integer
n
        VIntegerClamp t :: 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 t :: 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 t :: 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 t :: 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
        VDouble ->
            Expr Void a
forall s a. Expr s a
Double
        VDoubleLit n :: DhallDouble
n ->
            DhallDouble -> Expr Void a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n
        VDoubleShow t :: 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
        VText ->
            Expr Void a
forall s a. Expr s a
Text
        VTextLit (VChunks xys :: [(Text, Val a)]
xys z :: 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 t :: Val a
t u :: 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 t :: 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 t :: 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 ma :: Maybe (Val a)
ma ts :: 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 t :: Val a
t u :: 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 a :: Val a
a t :: 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 a :: Val a
a l :: Val a
l t :: Val a
t u :: Val a
u v :: 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 a :: Val a
a t :: 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 a :: Val a
a t :: 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 a :: Val a
a t :: 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 a :: Val a
a t :: 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 a :: Val a
a t :: 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 a :: 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 t :: 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 t :: 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
        VOptionalFold a :: Val a
a o :: Val a
o t :: Val a
t u :: Val a
u v :: Val a
v ->
            Expr Void a
forall s a. Expr s a
OptionalFold Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
o 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
        VOptionalBuild a :: Val a
a t :: Val a
t ->
            Expr Void a
forall s a. Expr s a
OptionalBuild Expr Void a -> Val a -> Expr Void a
`qApp` Val a
a Expr Void a -> Val a -> Expr Void a
`qApp` Val a
t
        VRecord m :: 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 m :: 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 m :: 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 mk :: Maybe Text
mk t :: Val a
t u :: 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 t :: Val a
t u :: 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 t :: Val a
t u :: Val a
u ->
            Expr Void a -> Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer (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 t :: Val a
t u :: Val a
u ma :: 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 t :: Val a
t ma :: 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 t :: Val a
t k :: 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 t :: Val a
t p :: 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 t :: 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 t :: Val a
t u :: 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 m :: Map Text (Maybe (Val a))
m k :: Text
k 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 m :: Map Text (Maybe (Val a))
m k :: Text
k (Just t :: 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 ->
            a -> Expr Void a
forall s a. a -> Expr s a
Embed a
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 x :: 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 x :: Text
x _ _) = (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 x :: 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 t :: Expr Void a
t VPrimVar = Expr Void a
t
    qApp t :: Expr Void a
t u :: 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 e :: Names
e topX :: Text
topX topI :: Int
topI = Int -> Names -> Int -> Expr s a
forall s a. Int -> Names -> Int -> Expr s a
go 0 Names
e Int
topI
      where
        go :: Int -> Names -> Int -> Expr s a
go !Int
acc (Bind env :: Names
env x :: 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
== 0 then Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "_" Int
acc) else Int -> Names -> Int -> Expr s a
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Names
env (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
          | Bool
otherwise = Int -> Names -> Int -> Expr s a
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Names
env Int
i
        go _ EmptyNames i :: 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 t0 :: Expr s a
t0 =
        case Expr s a
t0 of
            Const k :: Const
k ->
                Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
k
            Var (V x :: Text
x i :: 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 x :: Text
x t :: Expr s a
t u :: 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 "_" (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 x :: Text
x a :: Expr s a
a b :: Expr s a
b ->
                Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" (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 t :: Expr s a
t u :: 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 src0 :: Maybe s
src0 x :: Text
x src1 :: Maybe s
src1 mA :: Maybe (Maybe s, Expr s a)
mA src2 :: Maybe s
src2 a :: Expr s a
a) b :: Expr s a
b ->
                Binding s a -> Expr s a -> Expr s a
forall s a. Binding s a -> Expr s a -> Expr s a
Let (Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
forall s a.
Maybe s
-> Text
-> Maybe s
-> Maybe (Maybe s, Expr s a)
-> Maybe s
-> Expr s a
-> Binding s a
Binding Maybe s
src0 "_" 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 t :: Expr s a
t u :: 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)
            Bool ->
                Expr s a
forall s a. Expr s a
Bool
            BoolLit b :: Bool
b ->
                Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
b
            BoolAnd t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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 b :: Expr s a
b t :: Expr s a
t f :: 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)
            Natural ->
                Expr s a
forall s a. Expr s a
Natural
            NaturalLit n :: Natural
n ->
                Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
n
            NaturalFold ->
                Expr s a
forall s a. Expr s a
NaturalFold
            NaturalBuild ->
                Expr s a
forall s a. Expr s a
NaturalBuild
            NaturalIsZero ->
                Expr s a
forall s a. Expr s a
NaturalIsZero
            NaturalEven ->
                Expr s a
forall s a. Expr s a
NaturalEven
            NaturalOdd ->
                Expr s a
forall s a. Expr s a
NaturalOdd
            NaturalToInteger ->
                Expr s a
forall s a. Expr s a
NaturalToInteger
            NaturalShow ->
                Expr s a
forall s a. Expr s a
NaturalShow
            NaturalSubtract ->
                Expr s a
forall s a. Expr s a
NaturalSubtract
            NaturalPlus t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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)
            Integer ->
                Expr s a
forall s a. Expr s a
Integer
            IntegerLit n :: Integer
n ->
                Integer -> Expr s a
forall s a. Integer -> Expr s a
IntegerLit Integer
n
            IntegerClamp ->
                Expr s a
forall s a. Expr s a
IntegerClamp
            IntegerNegate ->
                Expr s a
forall s a. Expr s a
IntegerNegate
            IntegerShow ->
                Expr s a
forall s a. Expr s a
IntegerShow
            IntegerToDouble ->
                Expr s a
forall s a. Expr s a
IntegerToDouble
            Double ->
                Expr s a
forall s a. Expr s a
Double
            DoubleLit n :: DhallDouble
n ->
                DhallDouble -> Expr s a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
n
            DoubleShow ->
                Expr s a
forall s a. Expr s a
DoubleShow
            Text ->
                Expr s a
forall s a. Expr s a
Text
            TextLit cs :: 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 t :: Expr s a
t u :: 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)
            TextShow ->
                Expr s a
forall s a. Expr s a
TextShow
            List ->
                Expr s a
forall s a. Expr s a
List
            ListLit ma :: Maybe (Expr s a)
ma ts :: 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 t :: Expr s a
t u :: 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)
            ListBuild ->
                Expr s a
forall s a. Expr s a
ListBuild
            ListFold ->
                Expr s a
forall s a. Expr s a
ListFold
            ListLength ->
                Expr s a
forall s a. Expr s a
ListLength
            ListHead ->
                Expr s a
forall s a. Expr s a
ListHead
            ListLast ->
                Expr s a
forall s a. Expr s a
ListLast
            ListIndexed ->
                Expr s a
forall s a. Expr s a
ListIndexed
            ListReverse ->
                Expr s a
forall s a. Expr s a
ListReverse
            Optional ->
                Expr s a
forall s a. Expr s a
Optional
            Some t :: 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)
            None ->
                Expr s a
forall s a. Expr s a
None
            OptionalFold ->
                Expr s a
forall s a. Expr s a
OptionalFold
            OptionalBuild ->
                Expr s a
forall s a. Expr s a
OptionalBuild
            Record kts :: Map Text (Expr s a)
kts ->
                Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
Record ((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 kts :: Map Text (Expr s a)
kts ->
                Map Text (Expr s a) -> Expr s a
forall s a. Map Text (Expr s a) -> Expr s a
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 kts :: Map Text (Maybe (Expr s a))
kts ->
                Map Text (Maybe (Expr s a)) -> Expr s a
forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
Union ((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 m :: Maybe Text
m t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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 t :: Expr s a
t u :: 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
Prefer (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 t :: Expr s a
t u :: 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 x :: Expr s a
x y :: Expr s a
y ma :: 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 x :: Expr s a
x ma :: 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 t :: Expr s a
t k :: 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 t :: Expr s a
t ks :: 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 t :: 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 t :: Expr s a
t u :: 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)
            Note s :: s
s e :: 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 t :: Expr s a
t u :: 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 ->
                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 x :: 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 ts :: [(Text, Expr s a)]
ts x :: 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