From 71bb56931db5623c9d6d063efbfb1060edf1d778 Mon Sep 17 00:00:00 2001 From: Simon Jakobi Date: Fri, 6 Sep 2019 20:05:51 +0200 Subject: [PATCH] Use generic-random for Expr's Arbitrary instance (#1282) Full coverage of all Expr constructors is now checked by the type-checker. This revealed that that the IntegerToDouble, TextShow, Some and None constructors were missing. Also: * Increase frequency for Lam, Pi and App * Fix a few inconsistencies in normalization * Remove some dead code in D.T.QuickCheck Closes #1256. --- dhall/dhall.cabal | 1 + dhall/src/Dhall/Core.hs | 48 +++++-- dhall/tests/Dhall/Test/QuickCheck.hs | 189 +++++++++++++++------------ nix/generic-random.nix | 13 ++ stack-lts-6.yaml | 1 + 5 files changed, 154 insertions(+), 98 deletions(-) create mode 100644 nix/generic-random.nix diff --git a/dhall/dhall.cabal b/dhall/dhall.cabal index 2ce0cc7..a38fd38 100644 --- a/dhall/dhall.cabal +++ b/dhall/dhall.cabal @@ -598,6 +598,7 @@ Test-Suite tasty directory , filepath , foldl < 1.5 , + generic-random >= 1.2.0.0 && < 1.3 , lens-family-core >= 1.0.0 && < 2.1 , megaparsec , prettyprinter , diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs index 1194e7c..4087b39 100644 --- a/dhall/src/Dhall/Core.hs +++ b/dhall/src/Dhall/Core.hs @@ -1487,6 +1487,20 @@ normalizeWithM ctx e0 = loop (denote e0) ) nil = ListLit (Just (App List _A₀)) empty + App (App ListFold t) (ListLit _ xs) -> do + t' <- loop t + let list = Var (V "list" 0) + let lam term = + Lam "list" (Const Type) + (Lam "cons" (Pi "_" t' (Pi "_" list list)) + (Lam "nil" list term)) + term <- foldrM + (\x acc -> do + x' <- loop x + pure (App (App (Var (V "cons" 0)) x') acc)) + (Var (V "nil" 0)) + xs + pure (lam term) App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do t' <- loop t if boundedType t' then strict else lazy @@ -1531,14 +1545,23 @@ normalizeWithM ctx e0 = loop (denote e0) kvs = [ ("index", NaturalLit (fromIntegral n)) , ("value", a_) ] - App (App ListReverse t) (ListLit _ xs) -> - loop (ListLit m (Data.Sequence.reverse xs)) - where - m = if Data.Sequence.null xs then Just (App List t) else Nothing - App (App (App (App (App OptionalFold _) (App None _)) _) _) nothing -> - loop nothing - App (App (App (App (App OptionalFold _) (Some x)) _) just) _ -> - loop (App just x) + App (App ListReverse _) (ListLit t xs) -> + loop (ListLit t (Data.Sequence.reverse xs)) + + App (App OptionalFold t0) x0 -> do + t1 <- loop t0 + let optional = Var (V "optional" 0) + let lam term = (Lam "optional" + (Const Type) + (Lam "some" + (Pi "_" t1 optional) + (Lam "none" optional term))) + x1 <- loop x0 + pure $ case x1 of + App None _ -> lam (Var (V "none" 0)) + Some x' -> lam (App (Var (V "some" 0)) x') + _ -> App (App OptionalFold t1) x1 + App TextShow (TextLit (Chunks [] oldText)) -> loop (TextLit (Chunks [] newText)) where @@ -1902,17 +1925,14 @@ isNormalized e0 = loop (denote e0) App DoubleShow (DoubleLit _) -> False App (App OptionalBuild _) _ -> False App (App ListBuild _) _ -> False - App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ -> - False + App (App ListFold _) (ListLit _ _) -> False App (App ListLength _) (ListLit _ _) -> False App (App ListHead _) (ListLit _ _) -> False App (App ListLast _) (ListLit _ _) -> False App (App ListIndexed _) (ListLit _ _) -> False App (App ListReverse _) (ListLit _ _) -> False - App (App (App (App (App OptionalFold _) (Some _)) _) _) _ -> - False - App (App (App (App (App OptionalFold _) (App None _)) _) _) _ -> - False + App (App OptionalFold _) (Some _) -> False + App (App OptionalFold _) (App None _) -> False App TextShow (TextLit (Chunks [] _)) -> False _ -> True diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index 946d0d5..7af84e4 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -1,6 +1,13 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} + +#if __GLASGOW_HASKELL__ >= 800 +{-# LANGUAGE OverloadedLabels #-} +#endif {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -30,7 +37,7 @@ import Data.Functor.Identity (Identity(..)) import Dhall.Set (Set) import Dhall.Src (Src(..)) import Dhall.TypeCheck (Typer) -import Numeric.Natural (Natural) +import Generic.Random (Weights, W, (%), (:+)(..)) import Test.QuickCheck (Arbitrary(..), Gen, Positive(..), Property, NonNegative(..), genericShrink, (===), (==>)) import Test.QuickCheck.Instances () @@ -43,6 +50,7 @@ import qualified Codec.Serialise import qualified Data.Coerce import qualified Data.List import qualified Data.Sequence +import qualified Data.Text as Text import qualified Dhall.Binary import qualified Dhall.Context import qualified Dhall.Core @@ -50,6 +58,7 @@ import qualified Dhall.Diff import qualified Dhall.Map import qualified Dhall.Set import qualified Dhall.TypeCheck +import qualified Generic.Random import qualified Test.QuickCheck import qualified Test.Tasty import qualified Test.Tasty.QuickCheck @@ -162,93 +171,105 @@ instance Arbitrary Directory where shrink = genericShrink -averageDepth :: Natural -averageDepth = 3 - -averageNumberOfSubExpressions :: Double -averageNumberOfSubExpressions = 1 - 1 / fromIntegral averageDepth - -probabilityOfNullaryConstructor :: Double -probabilityOfNullaryConstructor = 1 / fromIntegral averageDepth - -numberOfConstructors :: Natural -numberOfConstructors = 50 - instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where arbitrary = Test.QuickCheck.suchThat - (Test.QuickCheck.frequency - [ ( 7, lift1 Const) - , ( 7, lift1 Var) - , ( 1, Test.QuickCheck.oneof [ lift2 (Lam "_"), lift3 Lam ]) - , ( 1, Test.QuickCheck.oneof [ lift2 (Pi "_"), lift3 Pi ]) - , ( 1, lift2 App) - , ( 7, lift2 Let) - , ( 1, lift2 Annot) - , ( 1, lift0 Bool) - , ( 7, lift1 BoolLit) - , ( 1, lift2 BoolAnd) - , ( 1, lift2 BoolOr) - , ( 1, lift2 BoolEQ) - , ( 1, lift2 BoolNE) - , ( 1, lift3 BoolIf) - , ( 1, lift0 Natural) - , ( 7, fmap NaturalLit arbitrary) - , ( 1, lift0 NaturalFold) - , ( 1, lift0 NaturalBuild) - , ( 1, lift0 NaturalIsZero) - , ( 1, lift0 NaturalEven) - , ( 1, lift0 NaturalOdd) - , ( 1, lift0 NaturalToInteger) - , ( 1, lift0 NaturalShow) - , ( 1, lift2 NaturalPlus) - , ( 1, lift2 NaturalTimes) - , ( 1, lift0 NaturalSubtract) - , ( 1, lift0 Integer) - , ( 7, fmap IntegerLit integer) - , ( 1, lift0 IntegerShow) - , ( 1, lift0 Double) - , ( 7, lift1 DoubleLit) - , ( 1, lift0 DoubleShow) - , ( 1, lift0 Text) - , ( 1, lift1 TextLit) - , ( 1, lift2 TextAppend) - , ( 1, lift0 List) - , let listLit = do - n <- Test.QuickCheck.choose (0, 3) - xs <- Test.QuickCheck.vectorOf n arbitrary - let ys = Data.Sequence.fromList xs - ListLit <$> arbitrary <*> pure ys - - in ( 1, listLit) - , ( 1, lift2 ListAppend) - , ( 1, lift0 ListBuild) - , ( 1, lift0 ListFold) - , ( 1, lift0 ListLength) - , ( 1, lift0 ListHead) - , ( 1, lift0 ListLast) - , ( 1, lift0 ListIndexed) - , ( 1, lift0 ListReverse) - , ( 1, lift0 Optional) - , ( 1, lift0 OptionalFold) - , ( 1, lift0 OptionalBuild) - , ( 1, lift1 Record) - , ( 7, lift1 RecordLit) - , ( 1, lift1 Union) - , ( 7, lift2 Combine) - , ( 1, lift2 CombineTypes) - , ( 7, lift2 Prefer) - , ( 1, lift3 Merge) - , ( 1, lift2 ToMap) - , ( 7, lift2 Field) - , ( 7, lift2 Project) - , ( 1, lift1 Assert) - , ( 1, lift2 Equivalent) - , ( 7, lift1 Embed) - , ( 7, lift2 ImportAlt) - ] - ) + (Generic.Random.genericArbitraryRecG customGens weights) standardizedExpression + where + customGens + :: Gen Integer -- Generates all Integer fields in Expr + :+ Gen Text.Text -- Generates all Text fields in Expr + :+ () + customGens = + integer + -- 'Lam's and 'Pi's are encoded differently when the binding is + -- the special string "_", so we generate some of these strings + -- to improve test coverage for these code paths. + :+ Test.QuickCheck.oneof [pure "_", arbitrary] + :+ () + + -- These weights determine the frequency of constructors in the generated + -- Expr. + -- They will fail to compile if the constructors don't appear in the order + -- in which they are defined in 'Expr'! + weights :: Weights (Expr s a) +-- TODO: Get rid of the CPP once +-- https://github.com/Lysxia/generic-random/pull/16 +-- has been released. +#if __GLASGOW_HASKELL__ >= 800 + weights = + (7 :: W "Const") + % (7 :: W "Var") + % (7 :: W "Lam") + % (7 :: W "Pi") + % (7 :: W "App") + % (7 :: W "Let") + % (1 :: W "Annot") + % (1 :: W "Bool") + % (7 :: W "BoolLit") + % (1 :: W "BoolAnd") + % (1 :: W "BoolOr") + % (1 :: W "BoolEQ") + % (1 :: W "BoolNE") + % (1 :: W "BoolIf") + % (1 :: W "Natural") + % (7 :: W "NaturalLit") + % (1 :: W "NaturalFold") + % (1 :: W "NaturalBuild") + % (1 :: W "NaturalIsZero") + % (1 :: W "NaturalEven") + % (1 :: W "NaturalOdd") + % (1 :: W "NaturalToInteger") + % (1 :: W "NaturalShow") + % (1 :: W "NaturalSubtract") + % (1 :: W "NaturalPlus") + % (1 :: W "NaturalTimes") + % (1 :: W "Integer") + % (7 :: W "IntegerLit") + % (1 :: W "IntegerShow") + % (1 :: W "IntegerToDouble") + % (1 :: W "Double") + % (7 :: W "DoubleLit") + % (1 :: W "DoubleShow") + % (1 :: W "Text") + % (1 :: W "TextLit") + % (1 :: W "TextAppend") + % (1 :: W "TextShow") + % (1 :: W "List") + % (1 :: W "ListLit") + % (1 :: W "ListAppend") + % (1 :: W "ListBuild") + % (1 :: W "ListFold") + % (1 :: W "ListLength") + % (1 :: W "ListHead") + % (1 :: W "ListLast") + % (1 :: W "ListIndexed") + % (1 :: W "ListReverse") + % (1 :: W "Optional") + % (7 :: W "Some") + % (1 :: W "None") + % (1 :: W "OptionalFold") + % (1 :: W "OptionalBuild") + % (1 :: W "Record") + % (7 :: W "RecordLit") + % (1 :: W "Union") + % (7 :: W "Combine") + % (1 :: W "CombineTypes") + % (7 :: W "Prefer") + % (1 :: W "Merge") + % (1 :: W "ToMap") + % (7 :: W "Field") + % (7 :: W "Project") + % (1 :: W "Assert") + % (1 :: W "Equivalent") + % (0 :: W "Note") + % (7 :: W "ImportAlt") + % (7 :: W "Embed") + % () +#else + weights = Generic.Random.uniform +#endif shrink expression = filter standardizedExpression (genericShrink expression) diff --git a/nix/generic-random.nix b/nix/generic-random.nix new file mode 100644 index 0000000..4e255f6 --- /dev/null +++ b/nix/generic-random.nix @@ -0,0 +1,13 @@ +{ mkDerivation, base, deepseq, QuickCheck, stdenv }: +mkDerivation { + pname = "generic-random"; + version = "1.2.0.0"; + sha256 = "9b1e00d2f06b582695a34cfdb2d8b62b32f64152c6ed43f5c2d776e6e9aa148c"; + revision = "1"; + editedCabalFile = "1d0hx41r7yq2a86ydnfh2fv540ah8cz05l071s2z4wxcjw0ymyn4"; + libraryHaskellDepends = [ base QuickCheck ]; + testHaskellDepends = [ base deepseq QuickCheck ]; + homepage = "http://github.com/lysxia/generic-random"; + description = "Generic random generators"; + license = stdenv.lib.licenses.mit; +} diff --git a/stack-lts-6.yaml b/stack-lts-6.yaml index 72115f2..534e0f4 100644 --- a/stack-lts-6.yaml +++ b/stack-lts-6.yaml @@ -30,6 +30,7 @@ extra-deps: - foldl-1.4.5 - formatting-6.3.2 - foundation-0.0.19 +- generic-random-1.2.0.0 - hashable-1.2.7.0 - haskeline-0.7.4.2 - integer-logarithms-1.0.3