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.
This commit is contained in:
Simon Jakobi
mergify[bot]
parent
8c8ea2a7ce
commit
71bb56931d
|
|
@ -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 ,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue