Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix isNormalized #522

Merged
merged 3 commits into from
Jul 30, 2018
Merged

Fix isNormalized #522

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
94a0f69
Fix `isNormalized`
Gabriella439 Jul 23, 2018
f68f359
Merge branch 'master' into gabriel/fix_isNormalized
Gabriella439 Jul 30, 2018
a384ec7
Use QuickCheck to verify correctness of `isNormalized`
Gabriella439 Jul 30, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
158 changes: 78 additions & 80 deletions src/Dhall/Core.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1769,7 +1769,7 @@ isNormalizedWith ctx e = e == (normalizeWith ctx e)


-- | Quickly check if an expression is in normal form
isNormalized :: Expr s a -> Bool
isNormalized :: Eq a => Expr s a -> Bool
isNormalized e = case denote e of
Const _ -> True
Var _ -> True
Expand Down Expand Up @@ -1813,37 +1813,32 @@ isNormalized e = case denote e of
Annot _ _ -> False
Bool -> True
BoolLit _ -> True
BoolAnd x y -> isNormalized x && isNormalized y &&
case x of
BoolLit _ ->
case y of
BoolLit _ -> False
_ -> True
_ -> True
BoolOr x y -> isNormalized x && isNormalized y &&
case x of
BoolLit _ ->
case y of
BoolLit _ -> False
_ -> True
_ -> True
BoolEQ x y -> isNormalized x && isNormalized y &&
case x of
BoolLit _ ->
case y of
BoolLit _ -> False
_ -> True
_ -> True
BoolNE x y -> isNormalized x && isNormalized y &&
case x of
BoolLit _ ->
case y of
BoolLit _ -> False
_ -> True
_ -> True
BoolIf b true false -> isNormalized b && case b of
BoolLit _ -> False
_ -> isNormalized true && isNormalized false
BoolAnd x y -> isNormalized x && isNormalized y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (judgmentallyEqual l r)
BoolOr x y -> isNormalized x && isNormalized y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (judgmentallyEqual l r)
BoolEQ x y -> isNormalized x && isNormalized y && decide x y
where
decide (BoolLit True) _ = False
decide _ (BoolLit True) = False
decide l r = not (judgmentallyEqual l r)
BoolNE x y -> isNormalized x && isNormalized y && decide x y
where
decide (BoolLit False) _ = False
decide _ (BoolLit False ) = False
decide l r = not (judgmentallyEqual l r)
BoolIf x y z ->
isNormalized x && isNormalized y && isNormalized z && decide x y z
where
decide (BoolLit _) _ _ = False
decide _ (BoolLit True) (BoolLit False) = False
decide _ l r = not (judgmentallyEqual l r)
Natural -> True
NaturalLit _ -> True
NaturalFold -> True
Expand All @@ -1853,20 +1848,20 @@ isNormalized e = case denote e of
NaturalOdd -> True
NaturalShow -> True
NaturalToInteger -> True
NaturalPlus x y -> isNormalized x && isNormalized y &&
case x of
NaturalLit _ ->
case y of
NaturalLit _ -> False
_ -> True
_ -> True
NaturalTimes x y -> isNormalized x && isNormalized y &&
case x of
NaturalLit _ ->
case y of
NaturalLit _ -> False
_ -> True
_ -> True
NaturalPlus x y -> isNormalized x && isNormalized y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
NaturalTimes x y -> isNormalized x && isNormalized y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit 1) _ = False
decide _ (NaturalLit 1) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
Integer -> True
IntegerLit _ -> True
IntegerShow -> True
Expand All @@ -1875,23 +1870,29 @@ isNormalized e = case denote e of
DoubleLit _ -> True
DoubleShow -> True
Text -> True
TextLit (Chunks xys _) -> all (all isNormalized) xys
TextAppend x y -> isNormalized x && isNormalized y &&
case x of
TextLit _ ->
case y of
TextLit _ -> False
_ -> True
_ -> True
TextLit (Chunks [("", _)] "") -> False
TextLit (Chunks xys _) -> all (all check) xys
where
check y = isNormalized y && case y of
TextLit _ -> False
_ -> True
TextAppend x y -> isNormalized x && isNormalized y && decide x y
where
isEmpty (Chunks [] "") = True
isEmpty _ = False

decide (TextLit m) _ | isEmpty m = False
decide _ (TextLit n) | isEmpty n = False
decide (TextLit _) (TextLit _) = False
decide _ _ = True
List -> True
ListLit t es -> all isNormalized t && all isNormalized es
ListAppend x y -> isNormalized x && isNormalized y &&
case x of
ListLit _ _ ->
case y of
ListLit _ _ -> False
_ -> True
_ -> True
ListAppend x y -> isNormalized x && isNormalized y && decide x y
where
decide (ListLit _ m) _ | Data.Sequence.null m = False
decide _ (ListLit _ n) | Data.Sequence.null n = False
decide (ListLit _ _) (ListLit _ _) = False
decide _ _ = True
ListBuild -> True
ListFold -> True
ListLength -> True
Expand All @@ -1907,28 +1908,25 @@ isNormalized e = case denote e of
RecordLit kvs -> all isNormalized kvs
Union kts -> all isNormalized kts
UnionLit _ v kvs -> isNormalized v && all isNormalized kvs
Combine x y -> isNormalized x && isNormalized y && combine
Combine x y -> isNormalized x && isNormalized y && decide x y
where
combine = case x of
RecordLit _ -> case y of
RecordLit _ -> False
_ -> True
_ -> True
CombineTypes x y -> isNormalized x && isNormalized y && combine
decide (RecordLit m) _ | Data.HashMap.Strict.InsOrd.null m = False
decide _ (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = False
decide (RecordLit _) (RecordLit _) = False
decide _ _ = True
CombineTypes x y -> isNormalized x && isNormalized y && decide x y
where
combine = case x of
Record _ -> case y of
Record _ -> False
_ -> True
_ -> True
Prefer x y -> isNormalized x && isNormalized y && combine
decide (Record m) _ | Data.HashMap.Strict.InsOrd.null m = False
decide _ (Record n) | Data.HashMap.Strict.InsOrd.null n = False
decide (Record _) (Record _) = False
decide _ _ = True
Prefer x y -> isNormalized x && isNormalized y && decide x y
where
combine = case x of
RecordLit _ -> case y of
RecordLit _ -> False
_ -> True
_ -> True
Merge x y t -> isNormalized x && isNormalized y && any isNormalized t &&
decide (RecordLit m) _ | Data.HashMap.Strict.InsOrd.null m = False
decide _ (RecordLit n) | Data.HashMap.Strict.InsOrd.null n = False
decide (RecordLit _) (RecordLit _) = False
decide _ _ = True
Merge x y t -> isNormalized x && isNormalized y && all isNormalized t &&
case x of
RecordLit kvsX ->
case y of
Expand Down
10 changes: 10 additions & 0 deletions tests/QuickCheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ import qualified Data.Coerce
import qualified Data.HashMap.Strict.InsOrd
import qualified Data.Sequence
import qualified Dhall.Binary
import qualified Dhall.Core
import qualified Test.QuickCheck
import qualified Test.Tasty.QuickCheck

Expand Down Expand Up @@ -327,11 +328,20 @@ binaryRoundtrip expression =
-> Either DeserialiseFailureWithEq a
wrap = Data.Coerce.coerce

isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property
isNormalizedIsConsistentWithNormalize expression =
Dhall.Core.isNormalized expression
=== (Dhall.Core.normalize expression == expression)

quickcheckTests :: TestTree
quickcheckTests
= Test.Tasty.QuickCheck.testProperties
"QuickCheck"
[ ( "Binary serialization should round-trip"
, Test.QuickCheck.property binaryRoundtrip
)
, ( "isNormalized should be consistent with normalize"
, Test.QuickCheck.property
(Test.QuickCheck.withMaxSuccess 10000 isNormalizedIsConsistentWithNormalize)
)
]