{-# 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 #-}
module Dhall.Eval (
judgmentallyEqual
, normalize
, alphaNormalize
, eval
, quote
, envNames
, countNames
, conv
, toVHPi
, Closure(..)
, Names(..)
, Environment(..)
, Val(..)
, (~>)
, textShow
) where
import Data.Foldable (foldr', toList)
import Data.Semigroup (Semigroup(..))
import Data.Sequence (Seq, ViewL(..), ViewR(..))
import Data.Text (Text)
import Data.Void (Void)
import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Prelude hiding (succ)
import Dhall.Syntax
( Binding(..)
, Expr(..)
, Chunks(..)
, Const(..)
, DhallDouble(..)
, PreferAnnotation(..)
, Var(..)
)
import qualified Data.Char
import qualified Data.Sequence as Sequence
import qualified Data.Set
import qualified Data.Text as Text
import qualified Dhall.Syntax as Syntax
import qualified Dhall.Map as Map
import qualified Dhall.Set
import qualified Text.Printf
data Environment a
= Empty
| Skip !(Environment a) {-# UNPACK #-} !Text
| Extend !(Environment a) {-# UNPACK #-} !Text (Val a)
deriving instance (Show a, Show (Val a -> Val a)) => Show (Environment a)
errorMsg :: String
errorMsg :: String
errorMsg = [String] -> String
unlines
[ String
_ERROR String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ": 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
data HLamInfo a
= Prim
| Typed !Text (Val a)
| NaturalSubtractZero
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
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 #-}
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
$ \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 ->
let inert :: Val a
inert = Val a -> Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a -> Val a
VNaturalFold Val a
n Val a
natural Val a
succ Val a
zero
in case Val a
zero of
VPrimVar -> Val a
inert
_ -> case Val a
succ of
VPrimVar -> Val a
inert
_ -> case Val a
natural of
VPrimVar -> Val a
inert
_ -> case Val a
n of
VNaturalLit n' :: Natural
n' ->
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)
_ -> Val a
inert
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 (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
m :: Integer) (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n :: Integer)))
| Bool
otherwise -> Natural -> Val a
forall a. Natural -> Val a
VNaturalLit 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)))
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
$ \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
$ \list :: Val a
list ->
(Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \cons :: Val a
cons ->
(Val a -> Val a) -> Val a
forall a. (Val a -> Val a) -> Val a
VPrim ((Val a -> Val a) -> Val a) -> (Val a -> Val a) -> Val a
forall a b. (a -> b) -> a -> b
$ \nil :: Val a
nil ->
let inert :: Val a
inert = Val a -> Val a -> Val a -> Val a -> Val a -> Val a
forall a. Val a -> Val a -> Val a -> Val a -> Val a -> Val a
VListFold Val a
a Val a
as Val a
list Val a
cons Val a
nil
in case Val a
nil of
VPrimVar -> Val a
inert
_ -> case Val a
cons of
VPrimVar -> Val a
inert
_ -> case Val a
list of
VPrimVar -> Val a
inert
_ -> case Val a
a of
VPrimVar -> Val a
inert
_ -> case Val a
as of
VListLit _ as' :: Seq (Val a)
as' ->
(Val a -> Val a -> Val a) -> Val a -> Seq (Val a) -> Val a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\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'
_ -> Val a
inert
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 (PreferAnnotation Void a
-> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation Void a
forall s a. PreferAnnotation s a
PreferFromCompletion (Expr Void a -> Text -> Expr Void a
forall s a. Expr s a -> Text -> Expr s a
Field Expr Void a
t "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)
e :: Expr Void a
e@With{} ->
Environment a -> Expr Void a -> Val a
forall a. Eq a => Environment a -> Expr Void a -> Val a
eval Environment a
env (Expr Void a -> Expr Void a
forall s a. Expr s a -> Expr s a
Syntax.desugarWith Expr Void a
e)
Note _ 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 #-}
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 :: 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 ->
PreferAnnotation Void a
-> Expr Void a -> Expr Void a -> Expr Void a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation Void a
forall s a. PreferAnnotation s a
PreferFromSource (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
t) (Names -> Val a -> Expr Void a
forall a. Eq a => Names -> Val a -> Expr Void a
quote Names
env Val a
u)
VMerge 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 #-}
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 b :: PreferAnnotation s a
b t :: Expr s a
t u :: Expr s a
u ->
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
forall s a.
PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
Prefer PreferAnnotation s a
b (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
t) (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
u)
RecordCompletion 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)
With e :: Expr s a
e k :: NonEmpty Text
k v :: Expr s a
v ->
Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
forall s a. Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
With (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
e) NonEmpty Text
k (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
go Expr s a
v)
Note s :: s
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