{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -O #-}
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.List.NonEmpty (NonEmpty(..))
import Data.Sequence (Seq, ViewL (..), ViewR (..))
import Data.Text (Text)
import Data.Void (Void)
import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Prelude hiding (succ)
import Dhall.Syntax
( Binding (..)
, Chunks (..)
, Const (..)
, DhallDouble (..)
, Expr (..)
, FunctionBinding (..)
, PreferAnnotation (..)
, RecordField (..)
, Var (..)
)
import qualified Data.Char
import qualified Data.Sequence as Sequence
import qualified Data.Set
import qualified Data.Text as Text
import qualified Dhall.Map as Map
import qualified Dhall.Set
import qualified Dhall.Syntax as Syntax
import qualified Text.Printf
data Environment a
= Empty
| Skip !(Environment a) {-# UNPACK #-} !Text
| Extend !(Environment a) {-# UNPACK #-} !Text (Val a)
deriving instance (Show a, Show (Val a -> Val a)) => Show (Environment a)
errorMsg :: String
errorMsg = unlines
[ _ERROR <> ": 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 = "\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 z <> VChunks [] z' = VChunks xys (z <> z')
VChunks xys z <> VChunks ((x', y'):xys') z' = VChunks (xys ++ (z <> x', y'):xys') z'
instance Monoid (VChunks a) where
mempty = VChunks [] mempty
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 VPrim f = VHLam Prim f
toVHPi :: Eq a => Val a -> Maybe (Text, Val a, Val a -> Val a)
toVHPi (VPi a b@(Closure x _ _)) = Just (x, a, instantiate b)
toVHPi (VHPi x a b ) = Just (x, a, b)
toVHPi _ = Nothing
data Val a
= VConst !Const
| VVar !Text !Int
| VPrimVar
| VApp !(Val a) !(Val a)
| VLam (Val a) {-# UNPACK #-} !(Closure a)
| VHLam !(HLamInfo a) !(Val a -> Val a)
| VPi (Val a) {-# UNPACK #-} !(Closure a)
| VHPi !Text (Val a) !(Val a -> Val a)
| VBool
| VBoolLit !Bool
| VBoolAnd !(Val a) !(Val a)
| VBoolOr !(Val a) !(Val a)
| VBoolEQ !(Val a) !(Val a)
| VBoolNE !(Val a) !(Val a)
| VBoolIf !(Val a) !(Val a) !(Val a)
| VNatural
| VNaturalLit !Natural
| VNaturalFold !(Val a) !(Val a) !(Val a) !(Val a)
| VNaturalBuild !(Val a)
| VNaturalIsZero !(Val a)
| VNaturalEven !(Val a)
| VNaturalOdd !(Val a)
| VNaturalToInteger !(Val a)
| VNaturalShow !(Val a)
| VNaturalSubtract !(Val a) !(Val a)
| VNaturalPlus !(Val a) !(Val a)
| VNaturalTimes !(Val a) !(Val a)
| VInteger
| VIntegerLit !Integer
| VIntegerClamp !(Val a)
| VIntegerNegate !(Val a)
| VIntegerShow !(Val a)
| VIntegerToDouble !(Val a)
| VDouble
| VDoubleLit !DhallDouble
| VDoubleShow !(Val a)
| VText
| VTextLit !(VChunks a)
| VTextAppend !(Val a) !(Val a)
| VTextShow !(Val a)
| VTextReplace !(Val a) !(Val a) !(Val a)
| VList !(Val a)
| VListLit !(Maybe (Val a)) !(Seq (Val a))
| VListAppend !(Val a) !(Val a)
| VListBuild (Val a) !(Val a)
| VListFold (Val a) !(Val a) !(Val a) !(Val a) !(Val a)
| VListLength (Val a) !(Val a)
| VListHead (Val a) !(Val a)
| VListLast (Val a) !(Val a)
| VListIndexed (Val a) !(Val a)
| VListReverse (Val a) !(Val a)
| VOptional (Val a)
| VSome (Val a)
| VNone (Val a)
| VRecord !(Map Text (Val a))
| VRecordLit !(Map Text (Val a))
| VUnion !(Map Text (Maybe (Val a)))
| VCombine !(Maybe Text) !(Val a) !(Val a)
| VCombineTypes !(Val a) !(Val a)
| VPrefer !(Val a) !(Val a)
| VMerge !(Val a) !(Val a) !(Maybe (Val a))
| VToMap !(Val a) !(Maybe (Val a))
| VField !(Val a) !Text
| VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
| VProject !(Val a) !(Either (Set Text) (Val a))
| VAssert !(Val a)
| VEquivalent !(Val a) !(Val a)
| VWith !(Val a) (NonEmpty Text) !(Val a)
| VEmbed a
deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a)
(~>) :: Val a -> Val a -> Val a
(~>) a b = VHPi "_" a (\_ -> b)
{-# INLINE (~>) #-}
infixr 5 ~>
countEnvironment :: Text -> Environment a -> Int
countEnvironment x = go (0 :: Int)
where
go !acc Empty = acc
go acc (Skip env x' ) = go (if x == x' then acc + 1 else acc) env
go acc (Extend env x' _) = go (if x == x' then acc + 1 else acc) env
instantiate :: Eq a => Closure a -> Val a -> Val a
instantiate (Closure x env t) !u = eval (Extend env x u) t
{-# INLINE instantiate #-}
vVar :: Environment a -> Var -> Val a
vVar env0 (V x i0) = go env0 i0
where
go (Extend env x' v) i
| x == x' =
if i == 0 then v else go env (i - 1)
| otherwise =
go env i
go (Skip env x') i
| x == x' =
if i == 0 then VVar x (countEnvironment x env) else go env (i - 1)
| otherwise =
go env i
go Empty i =
VVar x (negate i - 1)
vApp :: Eq a => Val a -> Val a -> Val a
vApp !t !u =
case t of
VLam _ t' -> instantiate t' u
VHLam _ t' -> t' u
t' -> VApp t' u
{-# INLINE vApp #-}
vPrefer :: Eq a => Environment a -> Val a -> Val a -> Val a
vPrefer env t u =
case (t, u) of
(VRecordLit m, u') | null m ->
u'
(t', VRecordLit m) | null m ->
t'
(VRecordLit m, VRecordLit m') ->
VRecordLit (Map.union m' m)
(t', u') | conv env t' u' ->
t'
(t', u') ->
VPrefer t' u'
{-# INLINE vPrefer #-}
vCombine :: Maybe Text -> Val a -> Val a -> Val a
vCombine mk t u =
case (t, u) of
(VRecordLit m, u') | null m ->
u'
(t', VRecordLit m) | null m ->
t'
(VRecordLit m, VRecordLit m') ->
VRecordLit (Map.unionWith (vCombine Nothing) m m')
(t', u') ->
VCombine mk t' u'
vCombineTypes :: Val a -> Val a -> Val a
vCombineTypes t u =
case (t, u) of
(VRecord m, u') | null m ->
u'
(t', VRecord m) | null m ->
t'
(VRecord m, VRecord m') ->
VRecord (Map.unionWith vCombineTypes m m')
(t', u') ->
VCombineTypes t' u'
vListAppend :: Val a -> Val a -> Val a
vListAppend t u =
case (t, u) of
(VListLit _ xs, u') | null xs ->
u'
(t', VListLit _ ys) | null ys ->
t'
(VListLit t' xs, VListLit _ ys) ->
VListLit t' (xs <> ys)
(t', u') ->
VListAppend t' u'
{-# INLINE vListAppend #-}
vNaturalPlus :: Val a -> Val a -> Val a
vNaturalPlus t u =
case (t, u) of
(VNaturalLit 0, u') ->
u'
(t', VNaturalLit 0) ->
t'
(VNaturalLit m, VNaturalLit n) ->
VNaturalLit (m + n)
(t', u') ->
VNaturalPlus t' u'
{-# INLINE vNaturalPlus #-}
vField :: Val a -> Text -> Val a
vField t0 k = go t0
where
go = \case
VUnion m -> case Map.lookup k m of
Just (Just _) -> VPrim $ \ ~u -> VInject m k (Just u)
Just Nothing -> VInject m k Nothing
_ -> error errorMsg
VRecordLit m
| Just v <- Map.lookup k m -> v
| otherwise -> error errorMsg
VProject t _ -> go t
VPrefer (VRecordLit m) r -> case Map.lookup k m of
Just v -> VField (VPrefer (singletonVRecordLit v) r) k
Nothing -> go r
VPrefer l (VRecordLit m) -> case Map.lookup k m of
Just v -> v
Nothing -> go l
VCombine mk (VRecordLit m) r -> case Map.lookup k m of
Just v -> VField (VCombine mk (singletonVRecordLit v) r) k
Nothing -> go r
VCombine mk l (VRecordLit m) -> case Map.lookup k m of
Just v -> VField (VCombine mk l (singletonVRecordLit v)) k
Nothing -> go l
t -> VField t k
singletonVRecordLit v = VRecordLit (Map.singleton k v)
{-# INLINE vField #-}
vTextReplaceSlow :: Text -> Val a -> VChunks a -> VChunks a
vTextReplaceSlow needle replacement haystack = go haystack
where
go (VChunks [] lastText) =
if Text.null suffix
then VChunks [] lastText
else
let remainder = Text.drop (Text.length needle) suffix
rest = go (VChunks [] remainder)
in case replacement of
VTextLit replacementChunks ->
VChunks [] prefix <> replacementChunks <> rest
_ ->
VChunks [(prefix, replacement)] "" <> rest
where
(prefix, suffix) = Text.breakOn needle lastText
go (VChunks ((firstText, firstInterpolation) : chunks) lastText) =
if Text.null suffix
then
let rest = go (VChunks chunks lastText)
in VChunks [(firstText, firstInterpolation)] "" <> rest
else
let remainder = Text.drop (Text.length needle) suffix
rest =
go (VChunks ((remainder, firstInterpolation) : chunks) lastText)
in case replacement of
VTextLit replacementChunks ->
VChunks [] prefix <> replacementChunks <> rest
_ ->
VChunks [(prefix, replacement)] "" <> rest
where
(prefix, suffix) = Text.breakOn needle firstText
vTextReplaceFast :: Text -> Text -> VChunks a -> VChunks a
vTextReplaceFast needle replacement (VChunks xys z) = VChunks xys' z'
where
xys' = do
(x, y) <- xys
return (Text.replace needle replacement x, y)
z' = Text.replace needle replacement z
vProjectByFields :: Eq a => Environment a -> Val a -> Set Text -> Val a
vProjectByFields env t ks =
if null ks
then VRecordLit mempty
else case t of
VRecordLit kvs ->
let kvs' = Map.restrictKeys kvs (Dhall.Set.toSet ks)
in VRecordLit kvs'
VProject t' _ ->
vProjectByFields env t' ks
VPrefer l (VRecordLit kvs) ->
let ksSet = Dhall.Set.toSet ks
kvs' = Map.restrictKeys kvs ksSet
ks' =
Dhall.Set.fromSet
(Data.Set.difference ksSet (Map.keysSet kvs'))
in vPrefer env (vProjectByFields env l ks') (VRecordLit kvs')
t' ->
VProject t' (Left ks)
vWith :: Val a -> NonEmpty Text -> Val a -> Val a
vWith (VRecordLit kvs) (k :| [] ) v = VRecordLit (Map.insert k v kvs)
vWith (VRecordLit kvs) (k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ kvs)
where
e₁ =
case Map.lookup k₀ kvs of
Nothing -> VRecordLit mempty
Just e₁' -> e₁'
e₂ = vWith e₁ (k₁ :| ks) v
vWith e₀ ks v₀ = VWith e₀ ks v₀
eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
eval !env t0 =
case t0 of
Const k ->
VConst k
Var v ->
vVar env v
Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t ->
VLam (eval env a) (Closure x env t)
Pi x a b ->
VPi (eval env a) (Closure x env b)
App t u ->
vApp (eval env t) (eval env u)
Let (Binding _ x _ _mA _ a) b ->
let !env' = Extend env x (eval env a)
in eval env' b
Annot t _ ->
eval env t
Bool ->
VBool
BoolLit b ->
VBoolLit b
BoolAnd t u ->
case (eval env t, eval env u) of
(VBoolLit True, u') -> u'
(VBoolLit False, _) -> VBoolLit False
(t', VBoolLit True) -> t'
(_ , VBoolLit False) -> VBoolLit False
(t', u') | conv env t' u' -> t'
(t', u') -> VBoolAnd t' u'
BoolOr t u ->
case (eval env t, eval env u) of
(VBoolLit False, u') -> u'
(VBoolLit True, _) -> VBoolLit True
(t', VBoolLit False) -> t'
(_ , VBoolLit True) -> VBoolLit True
(t', u') | conv env t' u' -> t'
(t', u') -> VBoolOr t' u'
BoolEQ t u ->
case (eval env t, eval env u) of
(VBoolLit True, u') -> u'
(t', VBoolLit True) -> t'
(t', u') | conv env t' u' -> VBoolLit True
(t', u') -> VBoolEQ t' u'
BoolNE t u ->
case (eval env t, eval env u) of
(VBoolLit False, u') -> u'
(t', VBoolLit False) -> t'
(t', u') | conv env t' u' -> VBoolLit False
(t', u') -> VBoolNE t' u'
BoolIf b t f ->
case (eval env b, eval env t, eval env f) of
(VBoolLit True, t', _ ) -> t'
(VBoolLit False, _ , f') -> f'
(b', VBoolLit True, VBoolLit False) -> b'
(_, t', f') | conv env t' f' -> t'
(b', t', f') -> VBoolIf b' t' f'
Natural ->
VNatural
NaturalLit n ->
VNaturalLit n
NaturalFold ->
VPrim $ \n ->
VPrim $ \natural ->
VPrim $ \succ ->
VPrim $ \zero ->
let inert = VNaturalFold n natural succ zero
in case zero of
VPrimVar -> inert
_ -> case succ of
VPrimVar -> inert
_ -> case natural of
VPrimVar -> inert
_ -> case n of
VNaturalLit n' ->
let go !acc 0 = acc
go acc m = go (vApp succ acc) (m - 1)
in go zero (fromIntegral n' :: Integer)
_ -> inert
NaturalBuild ->
VPrim $ \case
VPrimVar ->
VNaturalBuild VPrimVar
t -> t
`vApp` VNatural
`vApp` VHLam (Typed "n" VNatural) (\n -> vNaturalPlus n (VNaturalLit 1))
`vApp` VNaturalLit 0
NaturalIsZero -> VPrim $ \case
VNaturalLit n -> VBoolLit (n == 0)
n -> VNaturalIsZero n
NaturalEven -> VPrim $ \case
VNaturalLit n -> VBoolLit (even n)
n -> VNaturalEven n
NaturalOdd -> VPrim $ \case
VNaturalLit n -> VBoolLit (odd n)
n -> VNaturalOdd n
NaturalToInteger -> VPrim $ \case
VNaturalLit n -> VIntegerLit (fromIntegral n)
n -> VNaturalToInteger n
NaturalShow -> VPrim $ \case
VNaturalLit n -> VTextLit (VChunks [] (Text.pack (show n)))
n -> VNaturalShow n
NaturalSubtract -> VPrim $ \case
VNaturalLit 0 ->
VHLam NaturalSubtractZero id
x@(VNaturalLit m) ->
VPrim $ \case
VNaturalLit n
| n >= m ->
VNaturalLit (fromIntegral (subtract (fromIntegral m :: Integer) (fromIntegral n :: Integer)))
| otherwise -> VNaturalLit 0
y -> VNaturalSubtract x y
x ->
VPrim $ \case
VNaturalLit 0 -> VNaturalLit 0
y | conv env x y -> VNaturalLit 0
y -> VNaturalSubtract x y
NaturalPlus t u ->
vNaturalPlus (eval env t) (eval env u)
NaturalTimes t u ->
case (eval env t, eval env u) of
(VNaturalLit 1, u' ) -> u'
(t' , VNaturalLit 1) -> t'
(VNaturalLit 0, _ ) -> VNaturalLit 0
(_ , VNaturalLit 0) -> VNaturalLit 0
(VNaturalLit m, VNaturalLit n) -> VNaturalLit (m * n)
(t' , u' ) -> VNaturalTimes t' u'
Integer ->
VInteger
IntegerLit n ->
VIntegerLit n
IntegerClamp ->
VPrim $ \case
VIntegerLit n
| 0 <= n -> VNaturalLit (fromInteger n)
| otherwise -> VNaturalLit 0
n -> VIntegerClamp n
IntegerNegate ->
VPrim $ \case
VIntegerLit n -> VIntegerLit (negate n)
n -> VIntegerNegate n
IntegerShow ->
VPrim $ \case
VIntegerLit n
| 0 <= n -> VTextLit (VChunks [] (Text.pack ('+':show n)))
| otherwise -> VTextLit (VChunks [] (Text.pack (show n)))
n -> VIntegerShow n
IntegerToDouble ->
VPrim $ \case
VIntegerLit n -> VDoubleLit (DhallDouble (read (show n)))
n -> VIntegerToDouble n
Double ->
VDouble
DoubleLit n ->
VDoubleLit n
DoubleShow ->
VPrim $ \case
VDoubleLit (DhallDouble n) -> VTextLit (VChunks [] (Text.pack (show n)))
n -> VDoubleShow n
Text ->
VText
TextLit cs ->
case evalChunks cs of
VChunks [("", t)] "" -> t
vcs -> VTextLit vcs
TextAppend t u ->
eval env (TextLit (Chunks [("", t), ("", u)] ""))
TextShow ->
VPrim $ \case
VTextLit (VChunks [] x) -> VTextLit (VChunks [] (textShow x))
t -> VTextShow t
TextReplace ->
VPrim $ \needle ->
VPrim $ \replacement ->
VPrim $ \haystack ->
case haystack of
VTextLit haystackChunks ->
case needle of
VTextLit (VChunks [] "") ->
haystack
VTextLit (VChunks [] needleText) ->
case replacement of
VTextLit (VChunks [] replacementText) ->
VTextLit
(vTextReplaceFast
needleText
replacementText
haystackChunks
)
_ ->
VTextLit
(vTextReplaceSlow
needleText
replacement
haystackChunks
)
_ ->
VTextReplace needle replacement haystack
_ ->
VTextReplace needle replacement haystack
List ->
VPrim VList
ListLit ma ts ->
VListLit (fmap (eval env) ma) (fmap (eval env) ts)
ListAppend t u ->
vListAppend (eval env t) (eval env u)
ListBuild ->
VPrim $ \a ->
VPrim $ \case
VPrimVar ->
VListBuild a VPrimVar
t -> t
`vApp` VList a
`vApp` VHLam (Typed "a" a) (\x ->
VHLam (Typed "as" (VList a)) (\as ->
vListAppend (VListLit Nothing (pure x)) as))
`vApp` VListLit (Just (VList a)) mempty
ListFold ->
VPrim $ \a ->
VPrim $ \as ->
VPrim $ \list ->
VPrim $ \cons ->
VPrim $ \nil ->
let inert = VListFold a as list cons nil
in case nil of
VPrimVar -> inert
_ -> case cons of
VPrimVar -> inert
_ -> case list of
VPrimVar -> inert
_ -> case a of
VPrimVar -> inert
_ -> case as of
VListLit _ as' ->
foldr' (\x b -> cons `vApp` x `vApp` b) nil as'
_ -> inert
ListLength ->
VPrim $ \ a ->
VPrim $ \case
VListLit _ as -> VNaturalLit (fromIntegral (Sequence.length as))
as -> VListLength a as
ListHead ->
VPrim $ \ a ->
VPrim $ \case
VListLit _ as ->
case Sequence.viewl as of
y :< _ -> VSome y
_ -> VNone a
as ->
VListHead a as
ListLast ->
VPrim $ \ a ->
VPrim $ \case
VListLit _ as ->
case Sequence.viewr as of
_ :> t -> VSome t
_ -> VNone a
as -> VListLast a as
ListIndexed ->
VPrim $ \ a ->
VPrim $ \case
VListLit _ as ->
let a' =
if null as
then Just (VList (VRecord (Map.unorderedFromList [("index", VNatural), ("value", a)])))
else Nothing
as' =
Sequence.mapWithIndex
(\i t ->
VRecordLit
(Map.unorderedFromList
[ ("index", VNaturalLit (fromIntegral i))
, ("value", t)
]
)
)
as
in VListLit a' as'
t ->
VListIndexed a t
ListReverse ->
VPrim $ \ ~a ->
VPrim $ \case
VListLit t as | null as ->
VListLit t as
VListLit _ as ->
VListLit Nothing (Sequence.reverse as)
t ->
VListReverse a t
Optional ->
VPrim VOptional
Some t ->
VSome (eval env t)
None ->
VPrim $ \ ~a -> VNone a
Record kts ->
VRecord (Map.sort (eval env . recordFieldValue <$> kts))
RecordLit kts ->
VRecordLit (Map.sort (eval env . recordFieldValue <$> kts))
Union kts ->
VUnion (Map.sort (fmap (fmap (eval env)) kts))
Combine mk t u ->
vCombine mk (eval env t) (eval env u)
CombineTypes t u ->
vCombineTypes (eval env t) (eval env u)
Prefer _ t u ->
vPrefer env (eval env t) (eval env u)
RecordCompletion t u ->
eval env (Annot (Prefer PreferFromCompletion (Field t def) u) (Field t typ))
where
def = Syntax.makeFieldSelection "default"
typ = Syntax.makeFieldSelection "Type"
Merge x y ma ->
case (eval env x, eval env y, fmap (eval env) ma) of
(VRecordLit m, VInject _ k mt, _)
| Just f <- Map.lookup k m -> maybe f (vApp f) mt
| otherwise -> error errorMsg
(VRecordLit m, VSome t, _)
| Just f <- Map.lookup "Some" m -> vApp f t
| otherwise -> error errorMsg
(VRecordLit m, VNone _, _)
| Just t <- Map.lookup "None" m -> t
| otherwise -> error errorMsg
(x', y', ma') -> VMerge x' y' ma'
ToMap x ma ->
case (eval env x, fmap (eval env) ma) of
(VRecordLit m, ma'@(Just _)) | null m ->
VListLit ma' Sequence.empty
(VRecordLit m, _) ->
let entry (k, v) =
VRecordLit
(Map.unorderedFromList
[ ("mapKey", VTextLit $ VChunks [] k)
, ("mapValue", v)
]
)
s = (Sequence.fromList . map entry . Map.toAscList) m
in VListLit Nothing s
(x', ma') ->
VToMap x' ma'
Field t (Syntax.fieldSelectionLabel -> k) ->
vField (eval env t) k
Project t (Left ks) ->
vProjectByFields env (eval env t) (Dhall.Set.sort ks)
Project t (Right e) ->
case eval env e of
VRecord kts ->
eval env (Project t (Left (Dhall.Set.fromSet (Map.keysSet kts))))
e' ->
VProject (eval env t) (Right e')
Assert t ->
VAssert (eval env t)
Equivalent t u ->
VEquivalent (eval env t) (eval env u)
With e₀ ks v ->
vWith (eval env e₀) ks (eval env v)
Note _ e ->
eval env e
ImportAlt t _ ->
eval env t
Embed a ->
VEmbed a
where
evalChunks :: Chunks Void a -> VChunks a
evalChunks (Chunks xys z) = foldr' cons nil xys
where
cons (x, t) vcs =
case eval env t of
VTextLit vcs' -> VChunks [] x <> vcs' <> vcs
t' -> VChunks [(x, t')] mempty <> vcs
nil = VChunks [] z
{-# INLINE evalChunks #-}
eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy f = go
where
go (x:xs) (y:ys) | f x y = go xs ys
go [] [] = True
go _ _ = False
{-# INLINE eqListBy #-}
eqMapsBy :: Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
eqMapsBy f mL mR =
Map.size mL == Map.size mR
&& eqListBy eq (Map.toAscList mL) (Map.toAscList mR)
where
eq (kL, vL) (kR, vR) = kL == kR && f vL vR
{-# INLINE eqMapsBy #-}
eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eqMaybeBy f = go
where
go (Just x) (Just y) = f x y
go Nothing Nothing = True
go _ _ = False
{-# INLINE eqMaybeBy #-}
textShow :: Text -> Text
textShow text = "\"" <> Text.concatMap f text <> "\""
where
f '"' = "\\\""
f '$' = "\\u0024"
f '\\' = "\\\\"
f '\b' = "\\b"
f '\n' = "\\n"
f '\r' = "\\r"
f '\t' = "\\t"
f '\f' = "\\f"
f c | c <= '\x1F' = Text.pack (Text.Printf.printf "\\u%04x" (Data.Char.ord c))
| otherwise = Text.singleton c
conv :: forall a. Eq a => Environment a -> Val a -> Val a -> Bool
conv !env t0 t0' =
case (t0, t0') of
(VConst k, VConst k') ->
k == k'
(VVar x i, VVar x' i') ->
x == x' && i == i'
(VLam _ (freshClosure -> (x, v, t)), VLam _ t' ) ->
convSkip x (instantiate t v) (instantiate t' v)
(VLam _ (freshClosure -> (x, v, t)), VHLam _ t') ->
convSkip x (instantiate t v) (t' v)
(VLam _ (freshClosure -> (x, v, t)), t' ) ->
convSkip x (instantiate t v) (vApp t' v)
(VHLam _ t, VLam _ (freshClosure -> (x, v, t'))) ->
convSkip x (t v) (instantiate t' v)
(VHLam _ t, VHLam _ t' ) ->
let (x, v) = fresh "x" in convSkip x (t v) (t' v)
(VHLam _ t, t' ) ->
let (x, v) = fresh "x" in convSkip x (t v) (vApp t' v)
(t, VLam _ (freshClosure -> (x, v, t'))) ->
convSkip x (vApp t v) (instantiate t' v)
(t, VHLam _ t' ) ->
let (x, v) = fresh "x" in convSkip x (vApp t v) (t' v)
(VApp t u, VApp t' u') ->
conv env t t' && conv env u u'
(VPi a b, VPi a' (freshClosure -> (x, v, b'))) ->
conv env a a' && convSkip x (instantiate b v) (instantiate b' v)
(VPi a b, VHPi (fresh -> (x, v)) a' b') ->
conv env a a' && convSkip x (instantiate b v) (b' v)
(VHPi _ a b, VPi a' (freshClosure -> (x, v, b'))) ->
conv env a a' && convSkip x (b v) (instantiate b' v)
(VHPi _ a b, VHPi (fresh -> (x, v)) a' b') ->
conv env a a' && convSkip x (b v) (b' v)
(VBool, VBool) ->
True
(VBoolLit b, VBoolLit b') ->
b == b'
(VBoolAnd t u, VBoolAnd t' u') ->
conv env t t' && conv env u u'
(VBoolOr t u, VBoolOr t' u') ->
conv env t t' && conv env u u'
(VBoolEQ t u, VBoolEQ t' u') ->
conv env t t' && conv env u u'
(VBoolNE t u, VBoolNE t' u') ->
conv env t t' && conv env u u'
(VBoolIf t u v, VBoolIf t' u' v') ->
conv env t t' && conv env u u' && conv env v v'
(VNatural, VNatural) ->
True
(VNaturalLit n, VNaturalLit n') ->
n == n'
(VNaturalFold t _ u v, VNaturalFold t' _ u' v') ->
conv env t t' && conv env u u' && conv env v v'
(VNaturalBuild t, VNaturalBuild t') ->
conv env t t'
(VNaturalIsZero t, VNaturalIsZero t') ->
conv env t t'
(VNaturalEven t, VNaturalEven t') ->
conv env t t'
(VNaturalOdd t, VNaturalOdd t') ->
conv env t t'
(VNaturalToInteger t, VNaturalToInteger t') ->
conv env t t'
(VNaturalShow t, VNaturalShow t') ->
conv env t t'
(VNaturalSubtract x y, VNaturalSubtract x' y') ->
conv env x x' && conv env y y'
(VNaturalPlus t u, VNaturalPlus t' u') ->
conv env t t' && conv env u u'
(VNaturalTimes t u, VNaturalTimes t' u') ->
conv env t t' && conv env u u'
(VInteger, VInteger) ->
True
(VIntegerLit t, VIntegerLit t') ->
t == t'
(VIntegerClamp t, VIntegerClamp t') ->
conv env t t'
(VIntegerNegate t, VIntegerNegate t') ->
conv env t t'
(VIntegerShow t, VIntegerShow t') ->
conv env t t'
(VIntegerToDouble t, VIntegerToDouble t') ->
conv env t t'
(VDouble, VDouble) ->
True
(VDoubleLit n, VDoubleLit n') ->
n == n'
(VDoubleShow t, VDoubleShow t') ->
conv env t t'
(VText, VText) ->
True
(VTextLit cs, VTextLit cs') ->
convChunks cs cs'
(VTextAppend t u, VTextAppend t' u') ->
conv env t t' && conv env u u'
(VTextShow t, VTextShow t') ->
conv env t t'
(VTextReplace a b c, VTextReplace a' b' c') ->
conv env a a' && conv env b b' && conv env c c'
(VList a, VList a') ->
conv env a a'
(VListLit _ xs, VListLit _ xs') ->
eqListBy (conv env) (toList xs) (toList xs')
(VListAppend t u, VListAppend t' u') ->
conv env t t' && conv env u u'
(VListBuild _ t, VListBuild _ t') ->
conv env t t'
(VListLength a t, VListLength a' t') ->
conv env a a' && conv env t t'
(VListHead _ t, VListHead _ t') ->
conv env t t'
(VListLast _ t, VListLast _ t') ->
conv env t t'
(VListIndexed _ t, VListIndexed _ t') ->
conv env t t'
(VListReverse _ t, VListReverse _ t') ->
conv env t t'
(VListFold a l _ t u, VListFold a' l' _ t' u') ->
conv env a a' && conv env l l' && conv env t t' && conv env u u'
(VOptional a, VOptional a') ->
conv env a a'
(VSome t, VSome t') ->
conv env t t'
(VNone _, VNone _) ->
True
(VRecord m, VRecord m') ->
eqMapsBy (conv env) m m'
(VRecordLit m, VRecordLit m') ->
eqMapsBy (conv env) m m'
(VUnion m, VUnion m') ->
eqMapsBy (eqMaybeBy (conv env)) m m'
(VCombine _ t u, VCombine _ t' u') ->
conv env t t' && conv env u u'
(VCombineTypes t u, VCombineTypes t' u') ->
conv env t t' && conv env u u'
(VPrefer t u, VPrefer t' u') ->
conv env t t' && conv env u u'
(VMerge t u _, VMerge t' u' _) ->
conv env t t' && conv env u u'
(VToMap t _, VToMap t' _) ->
conv env t t'
(VField t k, VField t' k') ->
conv env t t' && k == k'
(VProject t (Left ks), VProject t' (Left ks')) ->
conv env t t' && ks == ks'
(VProject t (Right e), VProject t' (Right e')) ->
conv env t t' && conv env e e'
(VAssert t, VAssert t') ->
conv env t t'
(VEquivalent t u, VEquivalent t' u') ->
conv env t t' && conv env u u'
(VInject m k mt, VInject m' k' mt') ->
eqMapsBy (eqMaybeBy (conv env)) m m' && k == k' && eqMaybeBy (conv env) mt mt'
(VEmbed a, VEmbed a') ->
a == a'
(_, _) ->
False
where
fresh :: Text -> (Text, Val a)
fresh x = (x, VVar x (countEnvironment x env))
{-# INLINE fresh #-}
freshClosure :: Closure a -> (Text, Val a, Closure a)
freshClosure closure@(Closure x _ _) = (x, snd (fresh x), closure)
{-# INLINE freshClosure #-}
convChunks :: VChunks a -> VChunks a -> Bool
convChunks (VChunks xys z) (VChunks xys' z') =
eqListBy (\(x, y) (x', y') -> x == x' && conv env y y') xys xys' && z == z'
{-# INLINE convChunks #-}
convSkip :: Text -> Val a -> Val a -> Bool
convSkip x = conv (Skip env x)
{-# INLINE convSkip #-}
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual (Syntax.denote -> t) (Syntax.denote -> u) =
conv Empty (eval Empty t) (eval Empty u)
data Names
= EmptyNames
| Bind !Names {-# UNPACK #-} !Text
deriving Show
envNames :: Environment a -> Names
envNames Empty = EmptyNames
envNames (Skip env x ) = Bind (envNames env) x
envNames (Extend env x _) = Bind (envNames env) x
countNames :: Text -> Names -> Int
countNames x = go 0
where
go !acc EmptyNames = acc
go acc (Bind env x') = go (if x == x' then acc + 1 else acc) env
quote :: forall a. Eq a => Names -> Val a -> Expr Void a
quote !env !t0 =
case t0 of
VConst k ->
Const k
VVar !x !i ->
Var (V x (countNames x env - i - 1))
VApp t u ->
quote env t `qApp` u
VLam a (freshClosure -> (x, v, t)) ->
Lam
(Syntax.makeFunctionBinding x (quote env a))
(quoteBind x (instantiate t v))
VHLam i t ->
case i of
Typed (fresh -> (x, v)) a ->
Lam
(Syntax.makeFunctionBinding x (quote env a))
(quoteBind x (t v))
Prim -> quote env (t VPrimVar)
NaturalSubtractZero -> App NaturalSubtract (NaturalLit 0)
VPi a (freshClosure -> (x, v, b)) ->
Pi x (quote env a) (quoteBind x (instantiate b v))
VHPi (fresh -> (x, v)) a b ->
Pi x (quote env a) (quoteBind x (b v))
VBool ->
Bool
VBoolLit b ->
BoolLit b
VBoolAnd t u ->
BoolAnd (quote env t) (quote env u)
VBoolOr t u ->
BoolOr (quote env t) (quote env u)
VBoolEQ t u ->
BoolEQ (quote env t) (quote env u)
VBoolNE t u ->
BoolNE (quote env t) (quote env u)
VBoolIf t u v ->
BoolIf (quote env t) (quote env u) (quote env v)
VNatural ->
Natural
VNaturalLit n ->
NaturalLit n
VNaturalFold a t u v ->
NaturalFold `qApp` a `qApp` t `qApp` u `qApp` v
VNaturalBuild t ->
NaturalBuild `qApp` t
VNaturalIsZero t ->
NaturalIsZero `qApp` t
VNaturalEven t ->
NaturalEven `qApp` t
VNaturalOdd t ->
NaturalOdd `qApp` t
VNaturalToInteger t ->
NaturalToInteger `qApp` t
VNaturalShow t ->
NaturalShow `qApp` t
VNaturalPlus t u ->
NaturalPlus (quote env t) (quote env u)
VNaturalTimes t u ->
NaturalTimes (quote env t) (quote env u)
VNaturalSubtract x y ->
NaturalSubtract `qApp` x `qApp` y
VInteger ->
Integer
VIntegerLit n ->
IntegerLit n
VIntegerClamp t ->
IntegerClamp `qApp` t
VIntegerNegate t ->
IntegerNegate `qApp` t
VIntegerShow t ->
IntegerShow `qApp` t
VIntegerToDouble t ->
IntegerToDouble `qApp` t
VDouble ->
Double
VDoubleLit n ->
DoubleLit n
VDoubleShow t ->
DoubleShow `qApp` t
VText ->
Text
VTextLit (VChunks xys z) ->
TextLit (Chunks (fmap (fmap (quote env)) xys) z)
VTextAppend t u ->
TextAppend (quote env t) (quote env u)
VTextShow t ->
TextShow `qApp` t
VTextReplace a b c ->
TextReplace `qApp` a `qApp` b `qApp` c
VList t ->
List `qApp` t
VListLit ma ts ->
ListLit (fmap (quote env) ma) (fmap (quote env) ts)
VListAppend t u ->
ListAppend (quote env t) (quote env u)
VListBuild a t ->
ListBuild `qApp` a `qApp` t
VListFold a l t u v ->
ListFold `qApp` a `qApp` l `qApp` t `qApp` u `qApp` v
VListLength a t ->
ListLength `qApp` a `qApp` t
VListHead a t ->
ListHead `qApp` a `qApp` t
VListLast a t ->
ListLast `qApp` a `qApp` t
VListIndexed a t ->
ListIndexed `qApp` a `qApp` t
VListReverse a t ->
ListReverse `qApp` a `qApp` t
VOptional a ->
Optional `qApp` a
VSome t ->
Some (quote env t)
VNone t ->
None `qApp` t
VRecord m ->
Record (fmap quoteRecordField m)
VRecordLit m ->
RecordLit (fmap quoteRecordField m)
VUnion m ->
Union (fmap (fmap (quote env)) m)
VCombine mk t u ->
Combine mk (quote env t) (quote env u)
VCombineTypes t u ->
CombineTypes (quote env t) (quote env u)
VPrefer t u ->
Prefer PreferFromSource (quote env t) (quote env u)
VMerge t u ma ->
Merge (quote env t) (quote env u) (fmap (quote env) ma)
VToMap t ma ->
ToMap (quote env t) (fmap (quote env) ma)
VField t k ->
Field (quote env t) $ Syntax.makeFieldSelection k
VProject t p ->
Project (quote env t) (fmap (quote env) p)
VAssert t ->
Assert (quote env t)
VEquivalent t u ->
Equivalent (quote env t) (quote env u)
VWith e ks v ->
With (quote env e) ks (quote env v)
VInject m k Nothing ->
Field (Union (fmap (fmap (quote env)) m)) $ Syntax.makeFieldSelection k
VInject m k (Just t) ->
Field (Union (fmap (fmap (quote env)) m)) (Syntax.makeFieldSelection k) `qApp` t
VEmbed a ->
Embed a
VPrimVar ->
error errorMsg
where
fresh :: Text -> (Text, Val a)
fresh x = (x, VVar x (countNames x env))
{-# INLINE fresh #-}
freshClosure :: Closure a -> (Text, Val a, Closure a)
freshClosure closure@(Closure x _ _) = (x, snd (fresh x), closure)
{-# INLINE freshClosure #-}
quoteBind :: Text -> Val a -> Expr Void a
quoteBind x = quote (Bind env x)
{-# INLINE quoteBind #-}
qApp :: Expr Void a -> Val a -> Expr Void a
qApp t VPrimVar = t
qApp t u = App t (quote env u)
{-# INLINE qApp #-}
quoteRecordField :: Val a -> RecordField Void a
quoteRecordField = Syntax.makeRecordField . quote env
{-# INLINE quoteRecordField #-}
nf :: Eq a => Environment a -> Expr s a -> Expr t a
nf !env = Syntax.renote . quote (envNames env) . eval env . Syntax.denote
normalize :: Eq a => Expr s a -> Expr t a
normalize = nf Empty
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize = goEnv EmptyNames
where
goVar :: Names -> Text -> Int -> Expr s a
goVar e topX topI = go 0 e topI
where
go !acc (Bind env x) !i
| x == topX = if i == 0 then Var (V "_" acc) else go (acc + 1) env (i - 1)
| otherwise = go (acc + 1) env i
go _ EmptyNames i = Var (V topX i)
goEnv :: Names -> Expr s a -> Expr s a
goEnv !e0 t0 =
case t0 of
Const k ->
Const k
Var (V x i) ->
goVar e0 x i
Lam (FunctionBinding src0 x src1 src2 t) u ->
Lam (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u)
Pi x a b ->
Pi "_" (go a) (goBind x b)
App t u ->
App (go t) (go u)
Let (Binding src0 x src1 mA src2 a) b ->
Let (Binding src0 "_" src1 (fmap (fmap go) mA) src2 (go a)) (goBind x b)
Annot t u ->
Annot (go t) (go u)
Bool ->
Bool
BoolLit b ->
BoolLit b
BoolAnd t u ->
BoolAnd (go t) (go u)
BoolOr t u ->
BoolOr (go t) (go u)
BoolEQ t u ->
BoolEQ (go t) (go u)
BoolNE t u ->
BoolNE (go t) (go u)
BoolIf b t f ->
BoolIf (go b) (go t) (go f)
Natural ->
Natural
NaturalLit n ->
NaturalLit n
NaturalFold ->
NaturalFold
NaturalBuild ->
NaturalBuild
NaturalIsZero ->
NaturalIsZero
NaturalEven ->
NaturalEven
NaturalOdd ->
NaturalOdd
NaturalToInteger ->
NaturalToInteger
NaturalShow ->
NaturalShow
NaturalSubtract ->
NaturalSubtract
NaturalPlus t u ->
NaturalPlus (go t) (go u)
NaturalTimes t u ->
NaturalTimes (go t) (go u)
Integer ->
Integer
IntegerLit n ->
IntegerLit n
IntegerClamp ->
IntegerClamp
IntegerNegate ->
IntegerNegate
IntegerShow ->
IntegerShow
IntegerToDouble ->
IntegerToDouble
Double ->
Double
DoubleLit n ->
DoubleLit n
DoubleShow ->
DoubleShow
Text ->
Text
TextLit cs ->
TextLit (goChunks cs)
TextAppend t u ->
TextAppend (go t) (go u)
TextShow ->
TextShow
TextReplace ->
TextReplace
List ->
List
ListLit ma ts ->
ListLit (fmap go ma) (fmap go ts)
ListAppend t u ->
ListAppend (go t) (go u)
ListBuild ->
ListBuild
ListFold ->
ListFold
ListLength ->
ListLength
ListHead ->
ListHead
ListLast ->
ListLast
ListIndexed ->
ListIndexed
ListReverse ->
ListReverse
Optional ->
Optional
Some t ->
Some (go t)
None ->
None
Record kts ->
Record (goRecordField <$> kts)
RecordLit kts ->
RecordLit (goRecordField <$> kts)
Union kts ->
Union (fmap (fmap go) kts)
Combine m t u ->
Combine m (go t) (go u)
CombineTypes t u ->
CombineTypes (go t) (go u)
Prefer b t u ->
Prefer b (go t) (go u)
RecordCompletion t u ->
RecordCompletion (go t) (go u)
Merge x y ma ->
Merge (go x) (go y) (fmap go ma)
ToMap x ma ->
ToMap (go x) (fmap go ma)
Field t k ->
Field (go t) k
Project t ks ->
Project (go t) (fmap go ks)
Assert t ->
Assert (go t)
Equivalent t u ->
Equivalent (go t) (go u)
With e k v ->
With (go e) k (go v)
Note s e ->
Note s (go e)
ImportAlt t u ->
ImportAlt (go t) (go u)
Embed a ->
Embed a
where
go = goEnv e0
goBind x = goEnv (Bind e0 x)
goChunks (Chunks ts x) = Chunks (fmap (fmap go) ts) x
goRecordField (RecordField s0 e s1 s2) = RecordField s0 (go e) s1 s2