ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add a new environment machine normalizer (#876)

Browse Source 
- Dhall.Eval: new evaluator, conversion checker and normalizer.
  There is no standalone alpha normalizer yet.
- There is a new option "new-normalize" for dhall executable, which uses
  the new normalizer.
- Type checker is unchanged.
- new implementation: alphaNormalize, judgmentallyEqual, normalize
- normalizeWith takes a Maybe ReifiedNormalizer argument now, and switches to
  the new evaluator whenever the input normalizer is Nothing
- QuickCheck test for isNormalized removed, because we don't support evaluation
  of ill-typed terms, which the test would require.
This commit is contained in:
AndrasKovacs 2019-04-18 01:41:04 +02:00 committed by Gabriel Gonzalez
parent 91f3cae1bf
commit fcca883e00
18 changed files with 1163 additions and 344 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
dhall/benchmark/examples/normalize/ChurchEval.dhall Normal file
View File

@ -0,0 +1,22 @@
let Nat = ∀(N : Type) → (N → N) → N → N
let n2 = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s z)
let n5 = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s (s (s (s z))))
let mul =
λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N (b N s) z
let add =
λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N s (b N s z)
let n10 = mul n2 n5
let n100 = mul n10 n10
let n1k = mul n10 n100
let n10k = mul n100 n100
let n100k = mul n10 n10k
let n1M = mul n10k n100
let n5M = mul n1M n5
let n10M = mul n1M n10
let n20M = mul n10M n2
in n1M Natural (λ (x:Natural) → x + 1) 0

18
dhall/benchmark/examples/normalize/FunCompose.dhall Normal file
View File

@ -0,0 +1,18 @@
let compose
: ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
= λ(A : Type)
→ λ(B : Type)
→ λ(C : Type)
→ λ(f : A → B)
→ λ(g : B → C)
→ λ(x : A)
→ g (f x)
let composeN : ∀ (a : Type) → Natural → (a → a) → a → a
= λ (a : Type)
→ λ (n : Natural)
→ λ (f : a → a)
→ Natural/fold n (a → a) (compose a a a f) (λ (x : a) → x)
in composeN Natural 100000 (λ (x : Natural) → x + 1) 0

75
dhall/benchmark/examples/normalize/ListBench.dhall Normal file
View File

@ -0,0 +1,75 @@
let iterate
= λ(n : Natural)
→ λ(a : Type)
→ λ(f : a → a)
→ λ(x : a)
→ List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type)
→ λ(cons : {} → list → list)
→ Natural/fold n list (cons {=})
)
)
)
list
( λ(y : { index : Natural, value : {} })
→ cons (Natural/fold y.index a f x)
)
)
let countTo =
λ (x : Natural)
→ iterate x Natural (λ (x : Natural) → x + 1) 0
let sum =
λ (xs : List Natural)
→ List/fold Natural xs Natural (λ (x : Natural) → λ (acc : Natural) → x + acc) 0
let map
: ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
= λ(a : Type)
→ λ(b : Type)
→ λ(f : a → b)
→ λ(xs : List a)
→ List/build
b
( λ(list : Type)
→ λ(cons : b → list → list)
→ List/fold a xs list (λ(x : a) → cons (f x))
)
let any
: ∀(a : Type) → (a → Bool) → List a → Bool
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : List a)
→ List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
let filter
: ∀(a : Type) → (a → Bool) → List a → List a
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : List a)
→ List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ List/fold
a
xs
list
(λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)
)
in sum (filter Natural Natural/even
(map Natural Natural (λ(x:Natural) → x + 10) (countTo 1000)))

45
dhall/benchmark/examples/normalize/ListBenchAlt.dhall Normal file
View File

@ -0,0 +1,45 @@
let iterate =
λ(n : Natural)
→ λ(a : Type)
→ λ(f : a → a)
→ λ(x : a)
→ (Natural/fold n
(a → List a → {fst:a, snd:List a})
(λ (hyp : a → List a → {fst:a, snd:List a}) →
λ (x : a) → λ (xs : List a)
→ let tup = hyp x xs
in {fst = f (tup.fst), snd = tup.snd # [tup.fst]})
(λ (x : a) → λ (xs : List a) → {fst=x, snd=xs})
x ([] : List a)).snd
let countTo =
λ (x : Natural)
→ iterate x Natural (λ (x : Natural) → x + 1) 0
let sum =
λ (xs : List Natural)
→ List/fold Natural xs Natural (λ (x : Natural) → λ (acc : Natural) → x + acc) 0
let map
= λ(a : Type)
→ λ(b : Type)
→ λ(f : a → b)
→ λ(xs : List a)
→ List/fold a xs (List b) (λ (x : a) → λ (xs : List b) → [f x] # xs) ([] : List b)
let any
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : List a)
→ List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
let filter
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : List a)
→ List/fold a xs (List a)
(λ (x : a) → λ (xs : List a) → if f x then [x] # xs else xs) ([] : List a)
in sum (filter Natural Natural/even
(map Natural Natural (λ(x:Natural) → x + 10) (countTo 1000)))

2
dhall/dhall-lang

@ -1 +1 @@
Subproject commit 318cdfcc4c9f1dd9e1d3c4456f4f78de51e65c4a
Subproject commit c77f22cb10f25d9c3e29801760849c81b8595407

2
dhall/dhall.cabal
View File

@ -25,6 +25,7 @@ Category: Compiler
Extra-Source-Files:
benchmark/deep-nested-large-record/*.dhall
benchmark/examples/*.dhall
benchmark/examples/normalize/*.dhall
CHANGELOG.md
dhall-lang/Prelude/Bool/and
dhall-lang/Prelude/Bool/build
@ -448,6 +449,7 @@ Library
Dhall.Parser.Combinators,
Dhall.Parser.Token,
Dhall.Import.Types,
Dhall.Eval,
Dhall.Util,
Paths_dhall
if flag(with-http)

20
dhall/src/Dhall.hs
View File

@ -185,7 +185,7 @@ instance (Pretty s, Pretty a, Typeable s, Typeable a) => Show (InvalidType s a)
where
txt0 = Dhall.Util.insert invalidTypeExpected
txt1 = Dhall.Util.insert invalidTypeExpression
instance (Pretty s, Pretty a, Typeable s, Typeable a) => Exception (InvalidType s a)
@ -231,7 +231,7 @@ sourceName k s =
-- | @since 1.16
data EvaluateSettings = EvaluateSettings
{ _startingContext :: Dhall.Context.Context (Expr Src X)
, _normalizer :: Dhall.Core.ReifiedNormalizer X
, _normalizer :: Maybe (Dhall.Core.ReifiedNormalizer X)
, _standardVersion :: StandardVersion
}
@ -242,7 +242,7 @@ data EvaluateSettings = EvaluateSettings
defaultEvaluateSettings :: EvaluateSettings
defaultEvaluateSettings = EvaluateSettings
{ _startingContext = Dhall.Context.empty
, _normalizer = Dhall.Core.ReifiedNormalizer (const (pure Nothing))
, _normalizer = Nothing
, _standardVersion = Dhall.Binary.defaultStandardVersion
}
@ -263,11 +263,11 @@ startingContext = evaluateSettings . l
-- @since 1.16
normalizer
:: (Functor f, HasEvaluateSettings s)
=> LensLike' f s (Dhall.Core.ReifiedNormalizer X)
=> LensLike' f s (Maybe (Dhall.Core.ReifiedNormalizer X))
normalizer = evaluateSettings . l
where
l :: (Functor f)
=> LensLike' f EvaluateSettings (Dhall.Core.ReifiedNormalizer X)
=> LensLike' f EvaluateSettings (Maybe (Dhall.Core.ReifiedNormalizer X))
l k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s))
-- | Access the standard version (used primarily when encoding or decoding
@ -360,10 +360,8 @@ inputWithSettings settings (Type {..}) txt = do
_ ->
Annot expr' expected
_ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) annot)
let normExpr = Dhall.Core.normalizeWith
(Dhall.Core.getReifiedNormalizer
(view normalizer settings))
expr'
let normExpr = Dhall.Core.normalizeWith (view normalizer settings) expr'
case extract normExpr of
Just x -> return x
Nothing -> Control.Exception.throwIO
@ -450,7 +448,7 @@ inputExprWithSettings settings txt = do
expr' <- State.evalStateT (Dhall.Import.loadWith expr) status
_ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) expr')
pure (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr')
pure (Dhall.Core.normalizeWith (view normalizer settings) expr')
-- | Use this function to extract Haskell values directly from Dhall AST.
-- The intended use case is to allow easy extraction of Dhall values for
@ -834,7 +832,7 @@ instance Interpret a => Interpret (Vector a) where
instance (Inject a, Interpret b) => Interpret (a -> b) where
autoWith opts = Type extractOut expectedOut
where
normalizer_ = Dhall.Core.getReifiedNormalizer (inputNormalizer opts)
normalizer_ = Just (inputNormalizer opts)
extractOut e = Just (\i -> case extractIn (Dhall.Core.normalizeWith normalizer_ (App e (embed i))) of
Just o -> o

325
dhall/src/Dhall/Core.hs
View File

@ -33,7 +33,7 @@ module Dhall.Core (
, Expr(..)
-- * Normalization
, alphaNormalize
, Dhall.Core.alphaNormalize
, normalize
, normalizeWith
, normalizeWithM
@ -59,7 +59,6 @@ module Dhall.Core (
, pathCharacter
) where
import Codec.CBOR.Term (Term)
#if MIN_VERSION_base(4,8,0)
#else
import Control.Applicative (Applicative(..), (<$>))
@ -78,7 +77,6 @@ import Data.Sequence (Seq, ViewL(..), ViewR(..))
import Data.Text (Text)
import Data.Text.Prettyprint.Doc (Doc, Pretty)
import Data.Traversable
import {-# SOURCE #-} Dhall.Binary
import Dhall.Map (Map)
import Dhall.Set (Set)
import {-# SOURCE #-} Dhall.Pretty.Internal
@ -89,6 +87,7 @@ import Prelude hiding (succ)
import qualified Control.Monad
import qualified Crypto.Hash
import qualified Data.Char
import {-# SOURCE #-} qualified Dhall.Eval
import qualified Data.HashSet
import qualified Data.Sequence
import qualified Data.Text
@ -97,6 +96,7 @@ import qualified Dhall.Map
import qualified Dhall.Set
import qualified Text.Printf
{-| Constants for a pure type system
The axioms are:
@ -1157,293 +1157,7 @@ Var (V "x" 0)
-}
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize (Const c) =
Const c
alphaNormalize (Var v) =
Var v
alphaNormalize (Lam "_" _A₀ b₀) =
Lam "_" _A₁ b₁
where
_A₁ = alphaNormalize _A₀
b₁ = alphaNormalize b₀
alphaNormalize (Lam x _A₀ b₀) =
Lam "_" _A₁ b₄
where
_A₁ = alphaNormalize _A₀
b₁ = shift 1 (V "_" 0) b₀
b₂ = subst (V x 0) (Var (V "_" 0)) b₁
b₃ = shift (-1) (V x 0) b₂
b₄ = alphaNormalize b₃
alphaNormalize (Pi "_" _A₀ _B₀) =
Pi "_" _A₁ _B₁
where
_A₁ = alphaNormalize _A₀
_B₁ = alphaNormalize _B₀
alphaNormalize (Pi x _A₀ _B₀) =
Pi "_" _A₁ _B₄
where
_A₁ = alphaNormalize _A₀
_B₁ = shift 1 (V "_" 0) _B₀
_B₂ = subst (V x 0) (Var (V "_" 0)) _B₁
_B₃ = shift (-1) (V x 0) _B₂
_B₄ = alphaNormalize _B₃
alphaNormalize (App f₀ a₀) =
App f₁ a₁
where
f₁ = alphaNormalize f₀
a₁ = alphaNormalize a₀
alphaNormalize (Let (Binding "_" mA₀ a₀ :| []) b₀) =
Let (Binding "_" mA₁ a₁ :| []) b₁
where
mA₁ = fmap alphaNormalize mA₀
a₁ = alphaNormalize a₀
b₁ = alphaNormalize b₀
alphaNormalize (Let (Binding "_" mA₀ a₀ :| (l₀ : ls₀)) b₀) =
case alphaNormalize (Let (l₀ :| ls₀) b₀) of
Let (l₁ :| ls₁) b₁ -> Let (Binding "_" mA₁ a₁ :| (l₁ : ls₁)) b₁
e -> Let (Binding "_" mA₁ a₁ :| [] ) e
where
mA₁ = fmap alphaNormalize mA₀
a₁ = alphaNormalize a₀
alphaNormalize (Let (Binding x mA₀ a₀ :| []) b₀) =
Let (Binding "_" mA₁ a₁ :| []) b₄
where
mA₁ = fmap alphaNormalize mA₀
a₁ = alphaNormalize a₀
b₁ = shift 1 (V "_" 0) b₀
b₂ = subst (V x 0) (Var (V "_" 0)) b₁
b₃ = shift (-1) (V x 0) b₂
b₄ = alphaNormalize b₃
alphaNormalize (Let (Binding x mA₀ a₀ :| (l₀ : ls₀)) b₀) =
case alphaNormalize (Let (l₀ :| ls₀) b₃) of
Let (l₁ :| ls₁) b₄ -> Let (Binding "_" mA₁ a₁ :| (l₁ : ls₁)) b₄
e -> Let (Binding "_" mA₁ a₁ :| [] ) e
where
mA₁ = fmap alphaNormalize mA₀
a₁ = alphaNormalize a₀
b₁ = shift 1 (V "_" 0) b₀
b₂ = subst (V x 0) (Var (V "_" 0)) b₁
b₃ = shift (-1) (V x 0) b₂
alphaNormalize (Annot t₀ _T₀) =
Annot t₁ _T₁
where
t₁ = alphaNormalize t₀
_T₁ = alphaNormalize _T₀
alphaNormalize Bool =
Bool
alphaNormalize (BoolLit b) =
BoolLit b
alphaNormalize (BoolAnd l₀ r₀) =
BoolAnd l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (BoolOr l₀ r₀) =
BoolOr l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (BoolEQ l₀ r₀) =
BoolEQ l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (BoolNE l₀ r₀) =
BoolNE l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (BoolIf t₀ l₀ r₀) =
BoolIf t₁ l₁ r₁
where
t₁ = alphaNormalize t₀
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize Natural =
Natural
alphaNormalize (NaturalLit n) =
NaturalLit n
alphaNormalize NaturalFold =
NaturalFold
alphaNormalize NaturalBuild =
NaturalBuild
alphaNormalize NaturalIsZero =
NaturalIsZero
alphaNormalize NaturalEven =
NaturalEven
alphaNormalize NaturalOdd =
NaturalOdd
alphaNormalize NaturalToInteger =
NaturalToInteger
alphaNormalize NaturalShow =
NaturalShow
alphaNormalize (NaturalPlus l₀ r₀) =
NaturalPlus l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (NaturalTimes l₀ r₀) =
NaturalTimes l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize Integer =
Integer
alphaNormalize (IntegerLit n) =
IntegerLit n
alphaNormalize IntegerShow =
IntegerShow
alphaNormalize IntegerToDouble =
IntegerToDouble
alphaNormalize Double =
Double
alphaNormalize (DoubleLit n) =
DoubleLit n
alphaNormalize DoubleShow =
DoubleShow
alphaNormalize Text =
Text
alphaNormalize (TextLit (Chunks xys₀ z)) =
TextLit (Chunks xys₁ z)
where
xys₁ = do
(x, y₀) <- xys₀
let y₁ = alphaNormalize y₀
return (x, y₁)
alphaNormalize (TextAppend l₀ r₀) =
TextAppend l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize TextShow =
TextShow
alphaNormalize List =
List
alphaNormalize (ListLit (Just _T₀) ts₀) =
ListLit (Just _T₁) ts₁
where
_T₁ = alphaNormalize _T₀
ts₁ = fmap alphaNormalize ts₀
alphaNormalize (ListLit Nothing ts₀) =
ListLit Nothing ts₁
where
ts₁ = fmap alphaNormalize ts₀
alphaNormalize (ListAppend l₀ r₀) =
ListAppend l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize ListBuild =
ListBuild
alphaNormalize ListFold =
ListFold
alphaNormalize ListLength =
ListLength
alphaNormalize ListHead =
ListHead
alphaNormalize ListLast =
ListLast
alphaNormalize ListIndexed =
ListIndexed
alphaNormalize ListReverse =
ListReverse
alphaNormalize Optional =
Optional
alphaNormalize (OptionalLit _T₀ ts₀) =
OptionalLit _T₁ ts₁
where
_T₁ = alphaNormalize _T₀
ts₁ = fmap alphaNormalize ts₀
alphaNormalize (Some a₀) = Some a₁
where
a₁ = alphaNormalize a₀
alphaNormalize None = None
alphaNormalize OptionalFold =
OptionalFold
alphaNormalize OptionalBuild =
OptionalBuild
alphaNormalize (Record kts₀) =
Record kts₁
where
kts₁ = fmap alphaNormalize kts₀
alphaNormalize (RecordLit kvs₀) =
RecordLit kvs₁
where
kvs₁ = fmap alphaNormalize kvs₀
alphaNormalize (Union kts₀) =
Union kts₁
where
kts₁ = fmap (fmap alphaNormalize) kts₀
alphaNormalize (UnionLit k v₀ kts₀) =
UnionLit k v₁ kts₁
where
v₁ = alphaNormalize v₀
kts₁ = fmap (fmap alphaNormalize) kts₀
alphaNormalize (Combine l₀ r₀) =
Combine l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (CombineTypes l₀ r₀) =
CombineTypes l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (Prefer l₀ r₀) =
Prefer l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (Merge t₀ u₀ _T₀) =
Merge t₁ u₁ _T₁
where
t₁ = alphaNormalize t₀
u₁ = alphaNormalize u₀
_T₁ = fmap alphaNormalize _T₀
alphaNormalize (Field e₀ a) =
Field e₁ a
where
e₁ = alphaNormalize e₀
alphaNormalize (Project e₀ a) =
Project e₁ a
where
e₁ = alphaNormalize e₀
alphaNormalize (Note s e₀) =
Note s e₁
where
e₁ = alphaNormalize e₀
alphaNormalize (ImportAlt l₀ r₀) =
ImportAlt l₁ r₁
where
l₁ = alphaNormalize l₀
r₁ = alphaNormalize r₀
alphaNormalize (Embed a) =
Embed a
alphaNormalize = Dhall.Eval.alphaNormalize
{-| Reduce an expression to its normal form, performing beta reduction
@ -1454,8 +1168,10 @@ alphaNormalize (Embed a) =
However, `normalize` will not fail if the expression is ill-typed and will
leave ill-typed sub-expressions unevaluated.
-}
normalize :: ToTerm a => Expr s a -> Expr t a
normalize = normalizeWith (const (pure Nothing))
normalize :: Eq a => Expr s a -> Expr t a
normalize = Dhall.Eval.nfEmpty
{-| This function is used to determine whether folds like @Natural/fold@ or
@List/fold@ should be lazy or strict in their accumulator based on the type
@ -1564,11 +1280,12 @@ denote (Embed a ) = Embed a
with those functions is not total either.
-}
normalizeWith :: ToTerm a => Normalizer a -> Expr s a -> Expr t a
normalizeWith ctx = runIdentity . normalizeWithM ctx
normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
normalizeWith (Just ctx) t = runIdentity (normalizeWithM (getReifiedNormalizer ctx) t)
normalizeWith _ t = Dhall.Eval.nfEmpty t
normalizeWithM
:: (Monad m, ToTerm a) => NormalizerM m a -> Expr s a -> m (Expr t a)
:: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
normalizeWithM ctx e0 = loop (denote e0)
where
loop e = case e of
@ -1979,14 +1696,8 @@ textShow text = "\"" <> Data.Text.concatMap f text <> "\""
{-| Returns `True` if two expressions are α-equivalent and β-equivalent and
`False` otherwise
-}
judgmentallyEqual :: ToTerm a => Expr s a -> Expr t a -> Bool
judgmentallyEqual eL0 eR0 = term eL0 == term eR0
where
alphaBetaNormalize :: ToTerm a => Expr s a -> Expr () a
alphaBetaNormalize = alphaNormalize . normalize
term :: ToTerm a => Expr s a -> Term
term = Dhall.Binary.encode . alphaBetaNormalize
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual = Dhall.Eval.convEmpty
-- | Use this to wrap you embedded functions (see `normalizeWith`) to make them
-- polymorphic enough to be used.
@ -1996,18 +1707,18 @@ type Normalizer a = NormalizerM Identity a
-- | A reified 'Normalizer', which can be stored in structures without
-- running into impredicative polymorphism.
data ReifiedNormalizer a = ReifiedNormalizer
newtype ReifiedNormalizer a = ReifiedNormalizer
{ getReifiedNormalizer :: Normalizer a }
-- | Check if an expression is in a normal form given a context of evaluation.
-- Unlike `isNormalized`, this will fully normalize and traverse through the expression.
--
-- It is much more efficient to use `isNormalized`.
isNormalizedWith :: (Eq s, Eq a, ToTerm a) => Normalizer a -> Expr s a -> Bool
isNormalizedWith ctx e = e == normalizeWith ctx e
isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e
-- | Quickly check if an expression is in normal form
isNormalized :: ToTerm a => Expr s a -> Bool
isNormalized :: Eq a => Expr s a -> Bool
isNormalized e0 = loop (denote e0)
where
loop e = case e of

2
dhall/src/Dhall/Core.hs-boot
View File

@ -7,3 +7,5 @@ data Var
data Expr s a
data Import
denote :: Expr s a -> Expr t a

936
dhall/src/Dhall/Eval.hs Normal file
View File

@ -0,0 +1,936 @@
{-# LANGUAGE
BangPatterns,
CPP,
LambdaCase,
OverloadedStrings,
PatternSynonyms,
RankNTypes,
ScopedTypeVariables,
TupleSections,
ViewPatterns
#-}
{-# OPTIONS_GHC
-O
-fno-warn-name-shadowing
-fno-warn-unused-matches
#-}
{-|
Eval-apply environment machine with conversion checking and quoting to normal
forms. Fairly similar to GHCI's STG machine algorithmically, but much simpler,
with no known call optimization or environment trimming.
Potential optimizations without changing Expr:
- In conversion checking, get non-shadowing variables not by linear
Env-walking, but by keeping track of Env size, and generating names which
are known to be illegal as source-level names (to rule out shadowing).
- Use HashMap Text chunks for large let-definitions blocks. "Large" vs "Small"
is fairly cheap to determine at evaluation time.
Potential optimizations with changing Expr:
- Use Int in Var instead of Integer. Overflow is practically impossible.
- Use actual full de Bruijn indices in Var instead of Text counting indices. Then, we'd
switch to full de Bruijn levels in Val as well, and use proper constant time non-shadowing
name generation.
-}
module Dhall.Eval (
Env(..)
, Names(..)
, Closure(..)
, VChunks(..)
, Val(..)
, Void
, inst
, eval
, conv
, convEmpty
, quote
, nf
, nfEmpty
, Dhall.Eval.alphaNormalize
) where
#if MIN_VERSION_base(4,8,0)
#else
import Control.Applicative (Applicative(..), (<$>))
#endif
import Data.Foldable (foldr', foldl', toList)
import Data.List.NonEmpty (NonEmpty(..), cons)
import Data.Semigroup (Semigroup(..))
import Data.Sequence (Seq)
import Data.Text (Text)
import Dhall.Core (
Expr(..)
, Binding(..)
, Chunks(..)
, Const(..)
, Import
, Var(..)
, denote
)
-- import Control.Exception (throw)
-- import Dhall.Import.Types (InternalError)
import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)
import qualified Data.Char
import qualified Data.List.NonEmpty
import qualified Data.Sequence
import qualified Data.Text
import qualified Dhall.Binary
import qualified Dhall.Map
import qualified Text.Printf
----------------------------------------------------------------------------------------------------
data Env a =
Empty
| Skip !(Env a) {-# unpack #-} !Text
| Extend !(Env a) {-# unpack #-} !Text (Val a)
data Void
coeExprVoid :: Expr Void a -> Expr s a
coeExprVoid = unsafeCoerce
{-# inline coeExprVoid #-}
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 = Cl !Text !(Env a) !(Expr Void a)
data VChunks a = VChunks ![(Text, Val a)] !Text
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
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
data HLamInfo a
= Prim
| Typed !Text (Val a)
| NaturalFoldCl (Val a)
| ListFoldCl (Val a)
| OptionalFoldCl (Val a)
pattern VPrim :: (Val a -> Val a) -> Val a
pattern VPrim f = VHLam Prim f
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)
| VNaturalPlus !(Val a) !(Val a)
| VNaturalTimes !(Val a) !(Val a)
| VInteger
| VIntegerLit !Integer
| VIntegerShow !(Val a)
| VIntegerToDouble !(Val a)
| VDouble
| VDoubleLit !Double
| 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)))
| VUnionLit !Text !(Val a) !(Map Text (Maybe (Val a)))
| VCombine !(Val a) !(Val a)
| VCombineTypes !(Val a) !(Val a)
| VPrefer !(Val a) !(Val a)
| VMerge !(Val a) !(Val a) !(Maybe (Val a))
| VField !(Val a) !Text
| VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
| VProject !(Val a) !(Set Text)
| VEmbed a
vFun :: Val a -> Val a -> Val a
vFun a b = VHPi "_" a (\_ -> b)
{-# inline vFun #-}
-- Evaluation
----------------------------------------------------------------------------------------------------
textShow :: Text -> Text
textShow text = "\"" <> Data.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' = Data.Text.pack (Text.Printf.printf "\\u%04x" (Data.Char.ord c))
| otherwise = Data.Text.singleton c
countName :: Text -> Env a -> Int
countName 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
inst :: Eq a => Closure a -> Val a -> Val a
inst (Cl x env t) !u = eval (Extend env x u) t
{-# inline inst #-}
-- Out-of-env variables have negative de Bruijn levels.
vVar :: Env a -> Var -> Val a
vVar env (V x (fromInteger -> i :: Int)) = go env i 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 (countName x env) else go env (i - 1)
| otherwise = go env i
go Empty i = VVar x (0 - i - 1)
vApp :: Eq a => Val a -> Val a -> Val a
vApp !t !u = case t of
VLam _ t -> inst t u
VHLam _ t -> t u
t -> VApp t u
{-# inline vApp #-}
vCombine :: Val a -> Val a -> Val a
vCombine t u = case (t, u) of
(VRecordLit m, u) | null m -> u
(t, VRecordLit m) | null m -> t
(VRecordLit m, VRecordLit m') -> VRecordLit (Dhall.Map.sort (Dhall.Map.unionWith vCombine m m'))
(t, u) -> VCombine 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 (Dhall.Map.sort (Dhall.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 #-}
eval :: forall a. Eq a => Env a -> Expr Void a -> Val a
eval !env t =
let
evalE :: Expr Void a -> Val a
evalE = eval env
{-# inline evalE #-}
evalChunks :: Chunks Void a -> VChunks a
evalChunks (Chunks xys z) =
foldr' (\(x, t) vcs ->
case evalE t of
VTextLit vcs' -> VChunks [] x <> vcs' <> vcs
t -> VChunks [(x, t)] mempty <> vcs)
(VChunks [] z)
xys
{-# inline evalChunks #-}
in case t of
Const k -> VConst k
Var v -> vVar env v
Lam x a t -> VLam (evalE a) (Cl x env t)
Pi x a b -> VPi (evalE a) (Cl x env b)
App t u -> vApp (evalE t) (evalE u)
Let (b :| bs) t -> go env (b:bs) where
go !env [] = eval env t
go env (b:bs) = go (Extend env (variable b)
(eval env (value b))) bs
Annot t _ -> evalE t
Bool -> VBool
BoolLit b -> VBoolLit b
BoolAnd t u -> case (evalE t, evalE u) of
(VBoolLit True, u) -> u
(VBoolLit False, u) -> VBoolLit False
(t, VBoolLit True) -> t
(t, VBoolLit False) -> VBoolLit False
(t, u) | conv env t u -> t
(t, u) -> VBoolAnd t u
BoolOr t u -> case (evalE t, evalE u) of
(VBoolLit False, u) -> u
(VBoolLit True, u) -> VBoolLit True
(t, VBoolLit False) -> t
(t, VBoolLit True) -> VBoolLit True
(t, u) | conv env t u -> t
(t, u) -> VBoolOr t u
BoolEQ t u -> case (evalE t, evalE 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 (evalE t, evalE 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 (evalE b, evalE t, evalE f) of
(VBoolLit True, t, f) -> t
(VBoolLit False, t, f) -> f
(b, VBoolLit True, VBoolLit False) -> b
(b, t, f) | conv env t f -> t
(b, t, f) -> VBoolIf b t f
Natural -> VNatural
NaturalLit n -> VNaturalLit n
NaturalFold -> VPrim $ \case
VNaturalLit n ->
VHLam (Typed "natural" (VConst Type)) $ \natural ->
VHLam (Typed "succ" (vFun natural natural)) $ \succ ->
VHLam (Typed "zero" natural) $ \zero ->
let go !acc 0 = acc
go acc n = go (vApp succ acc) (n - 1)
in go zero n
n ->
VHLam (NaturalFoldCl n) $ \natural -> VPrim $ \succ -> VPrim $ \zero ->
VNaturalFold n natural succ zero
NaturalBuild -> VPrim $ \case
VHLam (NaturalFoldCl x) _ -> x
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 [] (Data.Text.pack (show n)))
n -> VNaturalShow n
NaturalPlus t u -> vNaturalPlus (evalE t) (evalE u)
NaturalTimes t u -> case (evalE t, evalE u) of
(VNaturalLit 1, u ) -> u
(t, VNaturalLit 1) -> t
(VNaturalLit 0, u ) -> VNaturalLit 0
(t, VNaturalLit 0) -> VNaturalLit 0
(VNaturalLit m, VNaturalLit n) -> VNaturalLit (m * n)
(t, u ) -> VNaturalTimes t u
Integer -> VInteger
IntegerLit n -> VIntegerLit n
IntegerShow -> VPrim $ \case
VIntegerLit n
| 0 <= n -> VTextLit (VChunks [] (Data.Text.pack ('+':show n)))
| otherwise -> VTextLit (VChunks [] (Data.Text.pack (show n)))
n -> VIntegerShow n
IntegerToDouble -> VPrim $ \case VIntegerLit n -> VDoubleLit (read (show n))
-- `(read . show)` is used instead of `fromInteger`
-- because `read` uses the correct rounding rule
n -> VIntegerToDouble n
Double -> VDouble
DoubleLit n -> VDoubleLit n
DoubleShow -> VPrim $ \case VDoubleLit n -> VTextLit (VChunks [] (Data.Text.pack (show n)))
n -> VDoubleShow n
Text -> VText
TextLit cs -> case evalChunks cs of
VChunks [("", t)] "" -> t
vcs -> VTextLit vcs
TextAppend t u -> case (evalE t, evalE u) of
(VTextLit (VChunks [] ""), u) -> u
(t, VTextLit (VChunks [] "")) -> t
(VTextLit x, VTextLit y) -> VTextLit (x <> y)
(t, u) -> VTextAppend t u
TextShow -> VPrim $ \case
VTextLit (VChunks [] x) -> VTextLit (VChunks [] (textShow x))
t -> VTextShow t
List -> VPrim VList
ListLit ma ts -> VListLit (evalE <$> ma) (evalE <$> ts)
ListAppend t u -> vListAppend (evalE t) (evalE u)
ListBuild -> VPrim $ \a -> VPrim $ \case
VHLam (ListFoldCl x) _ -> x
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 a) mempty
ListFold -> VPrim $ \a -> VPrim $ \case
VListLit _ as ->
VHLam (Typed "list" (VConst Type)) $ \list ->
VHLam (Typed "cons" (vFun a $ vFun list list) ) $ \cons ->
VHLam (Typed "nil" list) $ \nil ->
foldr' (\x b -> cons `vApp` x `vApp` b) nil as
as ->
VHLam (ListFoldCl as) $ \t -> VPrim $ \c -> VPrim $ \n ->
VListFold a as t c n
ListLength -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> VNaturalLit (fromIntegral (Data.Sequence.length as))
as -> VListLength a as
ListHead -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> case Data.Sequence.viewl as of
y Data.Sequence.:< _ -> VSome y
_ -> VNone a
as -> VListHead a as
ListLast -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> case Data.Sequence.viewr as of
_ Data.Sequence.:> t -> VSome t
_ -> VNone a
as -> VListLast a as
ListIndexed -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> let
a' = if null as then
Just (VRecord (Dhall.Map.fromList
[("index", VNatural), ("value", a)]))
else
Nothing
as' = Data.Sequence.mapWithIndex
(\i t -> VRecordLit
(Dhall.Map.fromList [("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 (Data.Sequence.reverse as)
VListLit t as -> VListLit Nothing (Data.Sequence.reverse as)
t -> VListReverse a t
Optional -> VPrim VOptional
OptionalLit a mt -> maybe (VNone (evalE a)) (\t -> VSome (evalE t)) mt
Some t -> VSome (evalE t)
None -> VPrim $ \ ~a -> VNone a
OptionalFold -> VPrim $ \ ~a -> VPrim $ \case
VNone _ ->
VHLam (Typed "optional" (VConst Type)) $ \optional ->
VHLam (Typed "some" (vFun a optional)) $ \some ->
VHLam (Typed "none" optional) $ \none ->
none
VSome t ->
VHLam (Typed "optional" (VConst Type)) $ \optional ->
VHLam (Typed "some" (vFun a optional)) $ \some ->
VHLam (Typed "none" optional) $ \none ->
some `vApp` t
opt ->
VHLam (OptionalFoldCl opt) $ \o ->
VPrim $ \s ->
VPrim $ \n ->
VOptionalFold a opt o s n
OptionalBuild -> VPrim $ \ ~a -> VPrim $ \case
VHLam (OptionalFoldCl x) _ -> x
VPrimVar -> VOptionalBuild a VPrimVar
t -> t `vApp` VOptional a
`vApp` VHLam (Typed "a" a) VSome
`vApp` VNone a
Record kts -> VRecord (Dhall.Map.sort (evalE <$> kts))
RecordLit kts -> VRecordLit (Dhall.Map.sort (evalE <$> kts))
Union kts -> VUnion (Dhall.Map.sort ((evalE <$>) <$> kts))
UnionLit k v kts -> VUnionLit k (evalE v) (Dhall.Map.sort ((evalE <$>) <$> kts))
Combine t u -> vCombine (evalE t) (evalE u)
CombineTypes t u -> vCombineTypes (evalE t) (evalE u)
Prefer t u -> case (evalE t, evalE u) of
(VRecordLit m, u) | null m -> u
(t, VRecordLit m) | null m -> t
(VRecordLit m, VRecordLit m') ->
VRecordLit (Dhall.Map.sort (Dhall.Map.union m' m))
(t, u) -> VPrefer t u
Merge x y ma -> case (evalE x, evalE y, evalE <$> ma) of
(VRecordLit m, VUnionLit k v _, _)
| Just f <- Dhall.Map.lookup k m -> f `vApp` v
| otherwise -> error errorMsg
(VRecordLit m, VInject _ k mt, _)
| Just f <- Dhall.Map.lookup k m -> maybe f (vApp f) mt
| otherwise -> error errorMsg
(x, y, ma) -> VMerge x y ma
Field t k -> case evalE t of
VRecordLit m
| Just v <- Dhall.Map.lookup k m -> v
| otherwise -> error errorMsg
VUnion m -> case Dhall.Map.lookup k m of
Just (Just _) -> VPrim $ \ ~u -> VInject m k (Just u)
Just Nothing -> VInject m k Nothing
_ -> error errorMsg
t -> VField t k
Project t ks -> if null ks then
VRecordLit mempty
else case evalE t of
VRecordLit kvs
| Just s <- traverse (\k -> (k,) <$> Dhall.Map.lookup k kvs) (toList ks)
-> VRecordLit (Dhall.Map.sort (Dhall.Map.fromList s))
| otherwise -> error errorMsg
t -> VProject t ks
Note _ e -> evalE e
ImportAlt t _ -> evalE t
Embed a -> VEmbed a
-- Conversion checking
--------------------------------------------------------------------------------
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 #-}
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 #-}
conv :: forall a. Eq a => Env a -> Val a -> Val a -> Bool
conv !env t t' =
let
fresh :: Text -> (Text, Val a)
fresh x = (x, VVar x (countName x env))
{-# inline fresh #-}
freshCl :: Closure a -> (Text, Val a, Closure a)
freshCl cl@(Cl x _ _) = (x, snd (fresh x), cl)
{-# inline freshCl #-}
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 #-}
convE :: Val a -> Val a -> Bool
convE = conv env
{-# inline convE #-}
convSkip :: Text -> Val a -> Val a -> Bool
convSkip x = conv (Skip env x)
{-# inline convSkip #-}
in case (t, t') of
(VConst k, VConst k') -> k == k'
(VVar x i, VVar x' i') -> x == x' && i == i'
(VLam _ (freshCl -> (x, v, t)), VLam _ t' ) -> convSkip x (inst t v) (inst t' v)
(VLam _ (freshCl -> (x, v, t)), VHLam _ t') -> convSkip x (inst t v) (t' v)
(VLam _ (freshCl -> (x, v, t)), t' ) -> convSkip x (inst t v) (vApp t' v)
(VHLam _ t, VLam _ (freshCl -> (x, v, t'))) -> convSkip x (t v) (inst 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 _ (freshCl -> (x, v, t'))) -> convSkip x (vApp t v) (inst t' v)
(t, VHLam _ t' ) -> let (x, v) = fresh "x" in convSkip x (vApp t v) (t' v)
(VApp t u, VApp t' u') -> convE t t' && convE u u'
(VPi a b, VPi a' (freshCl -> (x, v, b'))) ->
convE a a' && convSkip x (inst b v) (inst b' v)
(VPi a b, VHPi (fresh -> (x, v)) a' b') ->
convE a a' && convSkip x (inst b v) (b' v)
(VHPi _ a b, VPi a' (freshCl -> (x, v, b'))) ->
convE a a' && convSkip x (b v) (inst b' v)
(VHPi _ a b, VHPi (fresh -> (x, v)) a' b') ->
convE a a' && convSkip x (b v) (b' v)
(VBool , VBool ) -> True
(VBoolLit b , VBoolLit b' ) -> b == b'
(VBoolAnd t u, VBoolAnd t' u' ) -> convE t t' && convE u u'
(VBoolOr t u, VBoolOr t' u' ) -> convE t t' && convE u u'
(VBoolEQ t u, VBoolEQ t' u' ) -> convE t t' && convE u u'
(VBoolNE t u, VBoolNE t' u' ) -> convE t t' && convE u u'
(VBoolIf t u v, VBoolIf t' u' v') -> convE t t' && convE u u' && convE v v'
(VNatural, VNatural) -> True
(VNaturalLit n, VNaturalLit n') -> n == n'
(VNaturalFold t _ u v, VNaturalFold t' _ u' v') ->
convE t t' && convE u u' && convE v v'
(VNaturalBuild t , VNaturalBuild t') -> convE t t'
(VNaturalIsZero t , VNaturalIsZero t') -> convE t t'
(VNaturalEven t , VNaturalEven t') -> convE t t'
(VNaturalOdd t , VNaturalOdd t') -> convE t t'
(VNaturalToInteger t , VNaturalToInteger t') -> convE t t'
(VNaturalShow t , VNaturalShow t') -> convE t t'
(VNaturalPlus t u , VNaturalPlus t' u') -> convE t t' && convE u u'
(VNaturalTimes t u , VNaturalTimes t' u') -> convE t t' && convE u u'
(VInteger , VInteger) -> True
(VIntegerLit t , VIntegerLit t') -> t == t'
(VIntegerShow t , VIntegerShow t') -> convE t t'
(VIntegerToDouble t , VIntegerToDouble t') -> convE t t'
(VDouble , VDouble) -> True
(VDoubleLit n , VDoubleLit n') -> Dhall.Binary.encode (DoubleLit n :: Expr Void Import) ==
Dhall.Binary.encode (DoubleLit n' :: Expr Void Import)
(VDoubleShow t , VDoubleShow t') -> convE t t'
(VText, VText) -> True
(VTextLit cs , VTextLit cs') -> convChunks cs cs'
(VTextAppend t u , VTextAppend t' u') -> convE t t' && convE u u'
(VTextShow t , VTextShow t') -> convE t t'
(VList a , VList a' ) -> convE a a'
(VListLit _ xs , VListLit _ xs') -> eqListBy convE (toList xs) (toList xs')
(VListAppend t u , VListAppend t' u' ) -> convE t t' && convE u u'
(VListBuild a t , VListBuild a' t' ) -> convE t t'
(VListLength a t , VListLength a' t' ) -> convE a a' && convE t t'
(VListHead _ t , VListHead _ t' ) -> convE t t'
(VListLast _ t , VListLast _ t' ) -> convE t t'
(VListIndexed _ t , VListIndexed _ t' ) -> convE t t'
(VListReverse _ t , VListReverse _ t' ) -> convE t t'
(VListFold a l _ t u , VListFold a' l' _ t' u' ) ->
convE a a' && convE l l' && convE t t' && convE u u'
(VOptional a , VOptional a' ) -> convE a a'
(VSome t , VSome t' ) -> convE t t'
(VNone _ , VNone _ ) -> True
(VOptionalBuild _ t , VOptionalBuild _ t' ) -> convE t t'
(VRecord m , VRecord m' ) -> eqListBy convE (toList m) (toList m')
(VRecordLit m , VRecordLit m' ) -> eqListBy convE (toList m) (toList m')
(VUnion m , VUnion m' ) -> eqListBy (eqMaybeBy convE) (toList m) (toList m')
(VUnionLit k v m , VUnionLit k' v' m' ) -> k == k' && convE v v' &&
eqListBy (eqMaybeBy convE) (toList m) (toList m')
(VCombine t u , VCombine t' u' ) -> convE t t' && convE u u'
(VCombineTypes t u , VCombineTypes t' u' ) -> convE t t' && convE u u'
(VPrefer t u , VPrefer t' u' ) -> convE t t' && convE u u'
(VMerge t u _ , VMerge t' u' _ ) -> convE t t' && convE u u'
(VField t k , VField t' k' ) -> convE t t' && k == k'
(VProject t ks , VProject t' ks' ) -> convE t t' && ks == ks'
(VInject m k mt , VInject m' k' mt' ) -> eqListBy (eqMaybeBy convE) (toList m) (toList m')
&& k == k' && eqMaybeBy convE mt mt'
(VEmbed a , VEmbed a' ) -> a == a'
(VOptionalFold a t _ u v , VOptionalFold a' t' _ u' v' ) ->
convE a a' && convE t t' && convE u u' && convE v v'
(_, _) -> False
convEmpty :: Eq a => Expr s a -> Expr t a -> Bool
convEmpty (denote -> t) (denote -> u) = conv Empty (eval Empty t) (eval Empty u)
-- Quoting
----------------------------------------------------------------------------------------------------
data Names
= NEmpty
| NBind !Names {-# unpack #-} !Text
deriving Show
envNames :: Env a -> Names
envNames Empty = NEmpty
envNames (Skip env x ) = NBind (envNames env) x
envNames (Extend env x _) = NBind (envNames env) x
countName' :: Text -> Names -> Int
countName' x = go 0 where
go !acc NEmpty = acc
go acc (NBind env x') = go (if x == x' then acc + 1 else acc) env
-- | Quote a value into beta-normal form.
quote :: forall a. Eq a => Names -> Val a -> Expr Void a
quote !env !t =
let
fresh :: Text -> (Text, Val a)
fresh x = (x, VVar x (countName' x env))
{-# inline fresh #-}
freshCl :: Closure a -> (Text, Val a, Closure a)
freshCl cl@(Cl x _ _) = (x, snd (fresh x), cl)
{-# inline freshCl #-}
qVar :: Text -> Int -> Expr Void a
qVar !x !i = Var (V x (fromIntegral (countName' x env - i - 1)))
{-# inline qVar #-}
quoteE :: Val a -> Expr Void a
quoteE = quote env
{-# inline quoteE #-}
quoteBind :: Text -> Val a -> Expr Void a
quoteBind x = quote (NBind env x)
{-# inline quoteBind #-}
qApp :: Expr Void a -> Val a -> Expr Void a
qApp t VPrimVar = t
qApp t u = App t (quoteE u)
{-# inline qApp #-}
in case t of
VConst k -> Const k
VVar x i -> qVar x i
VApp t u -> quoteE t `qApp` u
VLam a (freshCl -> (x, v, t)) -> Lam x (quoteE a) (quoteBind x (inst t v))
VHLam i t -> case i of
Typed (fresh -> (x, v)) a -> Lam x (quoteE a) (quoteBind x (t v))
Prim -> quote env (t VPrimVar)
NaturalFoldCl{} -> quote env (t VPrimVar)
ListFoldCl{} -> quote env (t VPrimVar)
OptionalFoldCl{} -> quote env (t VPrimVar)
VPi a (freshCl -> (x, v, b)) -> Pi x (quoteE a) (quoteBind x (inst b v))
VHPi (fresh -> (x, v)) a b -> Pi x (quoteE a) (quoteBind x (b v))
VBool -> Bool
VBoolLit b -> BoolLit b
VBoolAnd t u -> BoolAnd (quoteE t) (quoteE u)
VBoolOr t u -> BoolOr (quoteE t) (quoteE u)
VBoolEQ t u -> BoolEQ (quoteE t) (quoteE u)
VBoolNE t u -> BoolNE (quoteE t) (quoteE u)
VBoolIf t u v -> BoolIf (quoteE t) (quoteE u) (quoteE 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 (quoteE t) (quoteE u)
VNaturalTimes t u -> NaturalTimes (quoteE t) (quoteE u)
VInteger -> Integer
VIntegerLit n -> IntegerLit n
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 ((quoteE <$>) <$> xys) z)
VTextAppend t u -> TextAppend (quoteE t) (quoteE u)
VTextShow t -> TextShow `qApp` t
VList t -> List `qApp` t
VListLit ma ts -> ListLit (quoteE <$> ma) (quoteE <$> ts)
VListAppend t u -> ListAppend (quoteE t) (quoteE 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 (quoteE t)
VNone t -> None `qApp` t
VOptionalFold a o t u v -> OptionalFold `qApp` a `qApp` o `qApp` t `qApp` u `qApp` v
VOptionalBuild a t -> OptionalBuild `qApp` a `qApp` t
VRecord m -> Record (quoteE <$> m)
VRecordLit m -> RecordLit (quoteE <$> m)
VUnion m -> Union ((quoteE <$>) <$> m)
VUnionLit k v m -> UnionLit k (quoteE v) ((quoteE <$>) <$> m)
VCombine t u -> Combine (quoteE t) (quoteE u)
VCombineTypes t u -> CombineTypes (quoteE t) (quoteE u)
VPrefer t u -> Prefer (quoteE t) (quoteE u)
VMerge t u ma -> Merge (quoteE t) (quoteE u) (quoteE <$> ma)
VField t k -> Field (quoteE t) k
VProject t ks -> Project (quoteE t) ks
VInject m k Nothing -> Field (Union ((quoteE <$>) <$> m)) k
VInject m k (Just t) -> Field (Union ((quoteE <$>) <$> m)) k `qApp` t
VEmbed a -> Embed a
VPrimVar -> error errorMsg
-- Normalization
----------------------------------------------------------------------------------------------------
-- | Normalize an expression in an environment of values. Any variable pointing out of
-- the environment is treated as opaque free variable.
nf :: Eq a => Env a -> Expr s a -> Expr t a
nf !env = coeExprVoid . quote (envNames env) . eval env . denote
-- | Normalize an expression in an empty environment.
nfEmpty :: Eq a => Expr s a -> Expr t a
nfEmpty = nf Empty
-- Alpha-renaming
--------------------------------------------------------------------------------
-- | Rename all binders to "_".
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize = goEnv NEmpty where
goVar :: Names -> Text -> Integer -> Expr s a
goVar e topX topI = go 0 e topI where
go !acc (NBind 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 acc NEmpty i = Var (V topX topI)
goEnv :: Names -> Expr s a -> Expr s a
goEnv !e t = let
go = goEnv e
goBind x = goEnv (NBind e x)
goChunks (Chunks ts x) = Chunks ((go <$>) <$> ts) x
in case t of
Const k -> Const k
Var (V x i) -> goVar e x i
Lam x t u -> Lam "_" (go t) (goBind x u)
Pi x a b -> Pi "_" (go a) (goBind x b)
App t u -> App (go t) (go u)
Let (b :| bs) u ->
let Binding x a t = b
nil = (NBind e x, Binding "_" (goEnv e <$> a) (goEnv e t) :| [])
snoc (e, bs) (Binding x a t) =
(NBind e x, cons (Binding "_" (goEnv e <$> a) (goEnv e t)) bs)
(e', Data.List.NonEmpty.reverse -> bs') = foldl' snoc nil bs
in Let bs' (goEnv e' u)
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 t) (go t) (go f)
Natural -> Natural
NaturalLit n -> NaturalLit n
NaturalFold -> NaturalFold
NaturalBuild -> NaturalBuild
NaturalIsZero -> NaturalIsZero
NaturalEven -> NaturalEven
NaturalOdd -> NaturalOdd
NaturalToInteger -> NaturalToInteger
NaturalShow -> NaturalShow
NaturalPlus t u -> NaturalPlus (go t) (go u)
NaturalTimes t u -> NaturalTimes (go t) (go u)
Integer -> Integer
IntegerLit n -> IntegerLit n
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
List -> List
ListLit ma ts -> ListLit (go <$> ma) (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
OptionalLit a mt -> OptionalLit (go a) (go <$> mt)
Some t -> Some (go t)
None -> None
OptionalFold -> OptionalFold
OptionalBuild -> OptionalBuild
Record kts -> Record (go <$> kts)
RecordLit kts -> RecordLit (go <$> kts)
Union kts -> Union ((go <$>) <$> kts)
UnionLit k v kts -> UnionLit k (go v) ((go <$>) <$> kts)
Combine t u -> Combine (go t) (go u)
CombineTypes t u -> CombineTypes (go t) (go u)
Prefer t u -> Prefer (go t) (go u)
Merge x y ma -> Merge (go x) (go y) (go <$> ma)
Field t k -> Field (go t) k
Project t ks -> Project (go t) ks
Note s e -> Note s (go e)
ImportAlt t u -> ImportAlt (go t) (go u)
Embed a -> Embed a

8
dhall/src/Dhall/Eval.hs-boot Normal file
View File

@ -0,0 +1,8 @@
module Dhall.Eval where
import {-# SOURCE #-} Dhall.Core
convEmpty :: Eq a => Expr s a -> Expr t a -> Bool
nfEmpty :: Eq a => Expr s a -> Expr t a
alphaNormalize :: Expr s a -> Expr s a

7
dhall/src/Dhall/Import.hs
View File

@ -157,7 +157,6 @@ import Dhall.Core
, ImportType(..)
, ImportMode(..)
, Import(..)
, ReifiedNormalizer(..)
, URL(..)
)
#ifdef MIN_VERSION_http_client
@ -512,7 +511,7 @@ exprToImport here expression = do
let normalizedExpression =
Dhall.Core.alphaNormalize
(Dhall.Core.normalizeWith
(getReifiedNormalizer _normalizer)
_normalizer
expression
)
@ -799,7 +798,7 @@ loadWith expr₀ = case expr₀ of
-- cached, since they have already been checked
expr''' <- case Dhall.TypeCheck.typeWith _startingContext expr'' of
Left err -> throwM (Imported _stack' err)
Right _ -> return (Dhall.Core.normalizeWith (getReifiedNormalizer _normalizer) expr'')
Right _ -> return (Dhall.Core.normalizeWith _normalizer expr'')
zoom cache (State.modify' (Map.insert child (childNodeId, expr''')))
return expr'''
@ -831,7 +830,7 @@ loadWith expr₀ = case expr₀ of
throwM (SourcedException (Src begin end text₂) (MissingImports (es₀ ++ es₁)))
where
text₂ = text₀ <> " ? " <> text₁
Const a -> pure (Const a)
Var a -> pure (Var a)
Lam a b c -> Lam <$> pure a <*> loadWith b <*> loadWith c

8
dhall/src/Dhall/Import/Types.hs
View File

@ -56,7 +56,7 @@ data Status m = Status
, _standardVersion :: StandardVersion
, _normalizer :: ReifiedNormalizer X
, _normalizer :: Maybe (ReifiedNormalizer X)
, _startingContext :: Context (Expr Src X)
@ -85,7 +85,7 @@ emptyStatusWith _resolver _cacher rootDirectory = Status {..}
_standardVersion = Dhall.Binary.defaultStandardVersion
_normalizer = ReifiedNormalizer (const (pure Nothing))
_normalizer = Nothing
_startingContext = Dhall.Context.empty
@ -135,8 +135,8 @@ standardVersion :: Functor f => LensLike' f (Status m) StandardVersion
standardVersion k s =
fmap (\x -> s { _standardVersion = x }) (k (_standardVersion s))
normalizer :: Functor f => LensLike' f (Status m) (ReifiedNormalizer X)
normalizer k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s))
normalizer :: Functor f => LensLike' f (Status m) (Maybe (ReifiedNormalizer X))
normalizer k s = fmap (\x -> s {_normalizer = x}) (k (_normalizer s))
startingContext :: Functor f => LensLike' f (Status m) (Context (Expr Src X))
startingContext k s =

2
dhall/src/Dhall/TypeCheck.hs
View File

@ -97,7 +97,7 @@ type Typer a = forall s. a -> Expr s a
constructor with custom logic
-}
typeWithA
:: ToTerm a
:: Eq a
=> Typer a
-> Context (Expr s a)
-> Expr s a

3
dhall/tests/Dhall/Test/Main.hs
View File

@ -23,7 +23,8 @@ import System.FilePath ((</>))
allTests :: TestTree
allTests =
Test.Tasty.testGroup "Dhall Tests"
[ Dhall.Test.Normalization.tests
[
Dhall.Test.Normalization.tests
, Dhall.Test.Parser.tests
, Dhall.Test.Regression.tests
, Dhall.Test.Tutorial.tests

6
dhall/tests/Dhall/Test/Normalization.hs
View File

@ -370,10 +370,12 @@ unitTests =
alphaNormalizationTests :: TestTree
alphaNormalizationTests =
testGroup "α-normalization tests"
[ shouldOnlyAlphaNormalize "FunctionBindingUnderscore"
, shouldOnlyAlphaNormalize "FunctionBindingX"
[ shouldOnlyAlphaNormalize "FunctionBindingX"
, shouldOnlyAlphaNormalize "FunctionTypeBindingX"
, shouldOnlyAlphaNormalize "FunctionTypeNestedBindingX"
, shouldOnlyAlphaNormalize "FunctionNestedBindingX"
, shouldOnlyAlphaNormalize "FunctionTypeBindingUnderscore"
, shouldOnlyAlphaNormalize "FunctionBindingUnderscore"
]
simplifications :: TestTree

21
dhall/tests/Dhall/Test/QuickCheck.hs
View File

@ -39,7 +39,6 @@ import qualified Data.List
import qualified Dhall.Map
import qualified Data.Sequence
import qualified Dhall.Binary
import qualified Dhall.Core
import qualified Dhall.Diff
import qualified Dhall.Set
import qualified Dhall.TypeCheck
@ -308,9 +307,9 @@ instance Arbitrary URL where
instance Arbitrary Var where
arbitrary =
Test.QuickCheck.oneof
[ fmap (V "_") natural
[ fmap (V "_") (fromIntegral <$> (natural :: Gen Int))
, lift1 (\t -> V t 0)
, lift1 V <*> natural
, lift1 V <*> (fromIntegral <$> (natural :: Gen Int))
]
shrink = genericShrink
@ -333,10 +332,10 @@ binaryRoundtrip expression =
-> Either DeserialiseFailureWithEq a
wrap = Data.Coerce.coerce
isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property
isNormalizedIsConsistentWithNormalize expression =
Dhall.Core.isNormalized expression
=== (Dhall.Core.normalize expression == expression)
-- isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property
-- isNormalizedIsConsistentWithNormalize expression =
-- Dhall.Core.isNormalized expression
-- === (Dhall.Core.normalize expression == expression)
isSameAsSelf :: Expr () Import -> Property
isSameAsSelf expression =
@ -353,10 +352,10 @@ tests =
[ ( "Binary serialization should round-trip"
, Test.QuickCheck.property binaryRoundtrip
)
, ( "isNormalized should be consistent with normalize"
, Test.QuickCheck.property
(Test.QuickCheck.withMaxSuccess 10000 isNormalizedIsConsistentWithNormalize)
)
-- , ( "isNormalized should be consistent with normalize"
-- , Test.QuickCheck.property
-- (Test.QuickCheck.withMaxSuccess 10000 isNormalizedIsConsistentWithNormalize)
-- )
, ( "An expression should have no difference with itself"
, Test.QuickCheck.property
(Test.QuickCheck.withMaxSuccess 10000 isSameAsSelf)

5
dhall/tests/Dhall/Test/Util.hs
View File

@ -18,7 +18,7 @@ import qualified Data.Functor
import Data.Bifunctor (first)
import Data.Text (Text)
import qualified Dhall.Core
import Dhall.Core (Expr, Normalizer)
import Dhall.Core (Expr, Normalizer, ReifiedNormalizer(..))
import qualified Dhall.Context
import Dhall.Context (Context)
import qualified Dhall.Import
@ -32,7 +32,8 @@ normalize' :: Expr Src X -> Text
normalize' = Dhall.Core.pretty . Dhall.Core.normalize
normalizeWith' :: Normalizer X -> Expr Src X -> Text
normalizeWith' ctx = Dhall.Core.pretty . Dhall.Core.normalizeWith ctx
normalizeWith' ctx t =
Dhall.Core.pretty (Dhall.Core.normalizeWith (Just (ReifiedNormalizer ctx)) t)
code :: Text -> IO (Expr Src X)
code = codeWith Dhall.Context.empty