clash-lib-hedgehog (empty) → 1.6.0
raw patch · 12 files changed
+2111/−0 lines, 12 filesdep +basedep +clash-libdep +containers
Dependencies added: base, clash-lib, containers, data-binary-ieee754, fakedata, ghc-typelits-knownnat, ghc-typelits-natnormalise, hedgehog, hedgehog-fakedata, mmorph, mtl, pretty-show, primitive, text, transformers
Files
- LICENSE +22/−0
- clash-lib-hedgehog.cabal +68/−0
- src/Clash/Hedgehog/Core/DataCon.hs +210/−0
- src/Clash/Hedgehog/Core/Literal.hs +110/−0
- src/Clash/Hedgehog/Core/Monad.hs +103/−0
- src/Clash/Hedgehog/Core/Name.hs +113/−0
- src/Clash/Hedgehog/Core/Term.hs +358/−0
- src/Clash/Hedgehog/Core/TyCon.hs +305/−0
- src/Clash/Hedgehog/Core/Type.hs +539/−0
- src/Clash/Hedgehog/Core/Var.hs +94/−0
- src/Clash/Hedgehog/Internal/Bias.hs +66/−0
- src/Clash/Hedgehog/Unique.hs +123/−0
+ LICENSE view
@@ -0,0 +1,22 @@+Copyright (c) 2021 QBayLogic B.V.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+ list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ clash-lib-hedgehog.cabal view
@@ -0,0 +1,68 @@+cabal-version: 2.2++name: clash-lib-hedgehog+version: 1.6.0+synopsis: Hedgehog Generators for clash-lib+description: Hedgehog Generators for clash-lib+bug-reports: https://github.com/clash-lang/clash-compiler/issues+license: BSD-2-Clause+license-file: LICENSE+author: QBayLogic B.V.+maintainer: devops@qbaylogic.com+copyright: Copyright © 2021, QBayLogic B.V.+category: Hardware+build-type: Simple++common basic-config+ default-language: Haskell2010++ default-extensions:+ BinaryLiterals+ DataKinds+ ScopedTypeVariables+ TypeApplications+ TypeFamilies+ TypeOperators++ if impl(ghc >= 8.6)+ default-extensions:+ NoStarIsType++ ghc-options:+ -Wall -Wcompat++ build-depends:+ base >= 4.11 && < 5,+ hedgehog >= 1.0.3 && < 1.1,++library+ import: basic-config+ hs-source-dirs: src++ exposed-modules:+ Clash.Hedgehog.Core.DataCon+ Clash.Hedgehog.Core.Literal+ Clash.Hedgehog.Core.Monad+ Clash.Hedgehog.Core.Name+ Clash.Hedgehog.Core.Term+ Clash.Hedgehog.Core.TyCon+ Clash.Hedgehog.Core.Type+ Clash.Hedgehog.Core.Var+ Clash.Hedgehog.Internal.Bias+ Clash.Hedgehog.Unique++ build-depends:+ containers >= 0.5.0.0 && < 0.7,+ data-binary-ieee754 >= 0.4.4 && < 0.6,+ fakedata >= 1.0.2 && < 1.1,+ ghc-typelits-knownnat >= 0.7.2 && < 0.8,+ ghc-typelits-natnormalise >= 0.7.2 && < 0.8,+ hedgehog-fakedata >= 0.0.1.4 && < 0.1,+ mmorph >= 1.1.5 && < 1.2,+ mtl >= 2.1.2 && < 2.3,+ pretty-show >= 1.9 && < 2.0,+ primitive >= 0.5.0.1 && < 1.0,+ text >= 1.2.2 && < 1.4,+ transformers >= 0.5.2.0 && < 0.7,++ clash-lib == 1.6.0,
+ src/Clash/Hedgehog/Core/DataCon.hs view
@@ -0,0 +1,210 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random type-directed generation of data constructors.+-}++module Clash.Hedgehog.Core.DataCon+ ( genDataConsFrom+ ) where++import Control.Monad (replicateM, zipWithM)+import Control.Monad.Morph (hoist)+import Data.Either (partitionEithers)+import Data.Functor.Identity (Identity(runIdentity))+import Data.Text (Text)+import qualified Faker.Lorem as Fake+import Hedgehog (GenT, Range)+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Gen.Faker as Gen++import Clash.Core.DataCon+import Clash.Core.Name+import Clash.Core.TyCon+import Clash.Core.Type+import Clash.Core.TysPrim (liftedTypeKind)+import Clash.Unique++import Clash.Hedgehog.Core.Monad+import Clash.Hedgehog.Core.Name+import Clash.Hedgehog.Core.Type+import Clash.Hedgehog.Core.Var++-- | Generate a list of data constructors for a type. This biases towards+-- creating constructors which match some common form seen in code, such as+-- simple enums with no fields, or records.+--+genDataConsFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => Range Int+ -- ^ The number of constructors to create for the data type+ -> TyConMap+ -- ^ The types already in scope when defining this type+ -> TyConName+ -- ^ The name of the @AlgTyCon@ the constructors belong to+ -> Kind+ -- ^ The kind of the @AlgTyCon@ the constructors belong to+ -> CoreGenT m [DataCon]+genDataConsFrom range tcm tcn kn = do+ -- We want to bias towards sometimes just having a single constructor. This+ -- is pretty common, e.g. for record types and non-GADT existential types.+ numConstructors <- Gen.choice [Gen.constant 1, Gen.int range]+ names <- genNames numConstructors genDataConName++ -- Universal tyvars are generated now so they can be shared between each+ -- data constructor. This matches what GHC would produce.+ let (knTvs, knTys) = partitionEithers $ fst (splitFunForallTy kn)+ univTvs <- mappend knTvs <$> genVars genTyVar knTys genVarName++ Gen.choice+ [ genSimpleDataCons tcn univTvs names+ , genRecordDataCons tcm tcn univTvs names+ , genAnyDataCons tcm tcn univTvs names+ ]++-- | Generate data constructors for a type+--+-- data D a1 a2 ... an = C1 | C2 | ... | CK+--+-- where every constructor is nullary, but the type constructor may have an+-- arbitrary number of phantom type parameters.+--+genSimpleDataCons+ :: forall m+ . Applicative m+ => TyConName+ -> [TyVar]+ -> [DcName]+ -> CoreGenT m [DataCon]+genSimpleDataCons tcn univTvs =+ pure . zipWith go [1..]+ where+ go :: ConTag -> DcName -> DataCon+ go tag name = MkData+ { dcName = name+ , dcUniq = nameUniq name+ , dcTag = tag+ , dcType = mkTyConApp tcn (fmap VarTy univTvs)+ , dcUnivTyVars = univTvs+ , dcExtTyVars = []+ , dcArgTys = []+ , dcArgStrict = []+ , dcFieldLabels = []+ }++-- | Generate data constructors for a type+--+-- data D a1 a2 ... an+-- = C1 { ... }+-- | C2 { ... }+-- | ...+-- | CK { ... }+--+-- where every constructor is either nullary, or a record.+--+genRecordDataCons+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> TyConName+ -> [TyVar]+ -> [DcName]+ -> CoreGenT m [DataCon]+genRecordDataCons tcm tcn univTvs =+ zipWithM go [1..]+ where+ go :: ConTag -> DcName -> CoreGenT m DataCon+ go tag name = do+ let resTy = mkTyConApp tcn (fmap VarTy univTvs)+ let bound = listToUniqMap (zip univTvs univTvs)+ let argGen = genMonoTypeFrom tcm bound liftedTypeKind -- TODO Make polymorphic+ ty <- genWithCodomain resTy argGen++ -- If there are type variables, getMonoTypeFrom is wrong.+ let ([], argTys) = partitionEithers $ fst (splitFunForallTy ty)+ bangs <- traverse (genStrictness tcm) argTys+ fields <- replicateM (length argTys) genFieldLabel++ pure MkData+ { dcName = name+ , dcUniq = nameUniq name+ , dcTag = tag+ , dcType = ty+ , dcUnivTyVars = univTvs+ , dcExtTyVars = []+ , dcArgTys = argTys+ , dcArgStrict = bangs+ , dcFieldLabels = fields+ }++-- | Generate data constructors for a type which does not match any common+-- idiom. Since this can generate any possible data constructor, it can+-- sometimes produce less representative results.+genAnyDataCons+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> TyConName+ -> [TyVar]+ -> [DcName]+ -> CoreGenT m [DataCon]+genAnyDataCons tcm tcn univTvs =+ zipWithM go [1..]+ where+ go :: ConTag -> DcName -> CoreGenT m DataCon+ go tag name = do+ let resTy = mkTyConApp tcn (fmap VarTy univTvs)+ let bound = listToUniqMap (zip univTvs univTvs)+ let argGen = genMonoTypeFrom tcm bound liftedTypeKind -- TODO Make polymorphic.+ ty <- genWithCodomain resTy argGen++ -- Determine the argument types from the data constructor type+ -- Generate strictness and field labels from the argument types+ let (extTvs, argTys) = partitionEithers $ fst (splitFunForallTy ty)+ bangs <- traverse (genStrictness tcm) argTys++ pure MkData+ { dcName = name+ , dcUniq = nameUniq name+ , dcTag = tag+ , dcType = ty+ , dcUnivTyVars = univTvs+ , dcExtTyVars = extTvs+ , dcArgTys = argTys+ , dcArgStrict = bangs+ , dcFieldLabels = []+ }++-- TODO genGadt, which can insert ~# arguments after the existential type+-- variables are introduced. I may also want a `genConstraints` in+-- Clash.Hedgehog.Core.Type to generate any constraints for a type.++-- | Generate strictness annotations for data constructor arguments. This+-- ensures that any types which are always strict, e.g. Int#, are strict and+-- types which may be lazy have a random strictness assigned.+--+-- This generator shrinks towards choosing lazy by default for types where it+-- is possible.+genStrictness+ :: forall m. MonadGen m => TyConMap -> Kind -> m DcStrictness+genStrictness tcm kn+ -- Assume that any primitive type constructor is always strict. This may+ -- overapproximate strictness, as it means Type, Nat and Symbol are strict.+ | TyConApp tc [] <- tyView kn+ , Just PrimTyCon{} <- lookupUniqMap tc tcm+ = pure Strict++ -- Shrink towards laziness as this is the default in Haskell (assuming no+ -- extensions like -XStrict or -XStrictData are enabled).+ | otherwise+ = Gen.element [Lazy, Strict]++-- | Generate a field label for use in a record.+genFieldLabel :: forall m. MonadGen m => m Text+genFieldLabel =+ fromGenT $ hoist @GenT @Identity @(GenBase m)+ (pure . runIdentity)+ (Gen.fake Fake.words)
+ src/Clash/Hedgehog/Core/Literal.hs view
@@ -0,0 +1,110 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random type-directed generation of literals.+-}++module Clash.Hedgehog.Core.Literal+ ( genLiteralFrom+ ) where++import Data.Binary.IEEE754 (doubleToWord, floatToWord)+import qualified Data.Primitive.ByteArray as BA (byteArrayFromList)+import Hedgehog (MonadGen)+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range++import Clash.Core.Literal+import Clash.Core.Pretty (showPpr)+import Clash.Core.Subst (aeqType)+import Clash.Core.Type (Type)+import Clash.Core.TysPrim++-- | Generate a 'Literal' with the specified core type. If the type does not+-- correspond to a known 'PrimTyCon' (as defined in "Clash.Core.TysPrim") then+-- an error is returned.+--+genLiteralFrom+ :: forall m+ . MonadGen m+ => Type+ -- ^ The type of the literal to generate+ -> m Literal+genLiteralFrom ty+ | aeqType ty integerPrimTy = genIntegerLiteral+ | aeqType ty intPrimTy = genIntLiteral+ | aeqType ty wordPrimTy = genWordLiteral+ | aeqType ty int64PrimTy = genInt64Literal+ | aeqType ty word64PrimTy = genWord64Literal+ | aeqType ty stringPrimTy = genStringLiteral+ | aeqType ty floatPrimTy = genFloatLiteral+ | aeqType ty doublePrimTy = genDoubleLiteral+ | aeqType ty charPrimTy = genCharLiteral+ | aeqType ty naturalPrimTy = genNaturalLiteral+ | aeqType ty byteArrayPrimTy = genByteArrayLiteral+ | otherwise =+ error $ unlines+ [ "genLiteralFrom: No constructors for " <> showPpr ty+ , "Check that this type is a primitive, and is not a void type."+ ]++-- TODO It would be nice to pass ranges into these types instead of just+-- guessing using some default range. However, that makes 'genLiteralFrom'+-- slightly more involved to write.+--+-- Without passing ranges to these, they may bias towards unrealistic values+-- which makes generating entire random programs less realistic.++genIntegerLiteral :: forall m. MonadGen m => m Literal+genIntegerLiteral =+ fmap IntegerLiteral . Gen.sized $ \size ->+ let upper = 2 ^ Range.unSize size+ lower = negate upper+ in Gen.integral (Range.linear lower upper)++genIntLiteral :: forall m. MonadGen m => m Literal+genIntLiteral =+ IntLiteral <$> (toInteger <$> Gen.int Range.linearBounded)++genWordLiteral :: forall m. MonadGen m => m Literal+genWordLiteral =+ WordLiteral <$> (toInteger <$> Gen.word Range.linearBounded)++genInt64Literal :: forall m. MonadGen m => m Literal+genInt64Literal =+ Int64Literal <$> (toInteger <$> Gen.int64 Range.linearBounded)++genWord64Literal :: forall m. MonadGen m => m Literal+genWord64Literal =+ Word64Literal <$> (toInteger <$> Gen.word64 Range.linearBounded)++genStringLiteral :: forall m. MonadGen m => m Literal+genStringLiteral =+ StringLiteral <$> Gen.string (Range.linear 10 50) Gen.unicode++genFloatLiteral :: forall m. MonadGen m => m Literal+genFloatLiteral =+ let range = Range.linearFrac 1.17549435e-38 3.40282347e+38+ in FloatLiteral <$> (floatToWord <$> Gen.float range)++genDoubleLiteral :: forall m. MonadGen m => m Literal+genDoubleLiteral =+ let range = Range.linearFrac 2.2250738585072014e-308 1.7976931348623157e+308+ in DoubleLiteral <$> (doubleToWord <$> Gen.double range)++genCharLiteral :: forall m. MonadGen m => m Literal+genCharLiteral =+ CharLiteral <$> Gen.ascii++genNaturalLiteral :: forall m. MonadGen m => m Literal+genNaturalLiteral =+ fmap NaturalLiteral . Gen.sized $ \size ->+ let upper = 2 ^ Range.unSize size+ in Gen.integral (Range.linear 0 upper)++genByteArrayLiteral :: forall m. MonadGen m => m Literal+genByteArrayLiteral = do+ bytes <- Gen.list (Range.linear 0 16) (Gen.word8 Range.linearBounded)+ pure (ByteArrayLiteral (BA.byteArrayFromList bytes))
+ src/Clash/Hedgehog/Core/Monad.hs view
@@ -0,0 +1,103 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Monad for random generation of clash-core types.+-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++module Clash.Hedgehog.Core.Monad+ ( CoreGenT+ , runCoreGenT+ , CoreGenConfig(..)+ , defaultConfig+ , canGenDataKinds+ , canGenPolyKinds+ , canGenRankNTypes+ , canGenTypeFamilies+ , canGenUndecidableInstances++ -- * Re-exports+ , Alternative(..)+ , MonadGen(..)+ , MonadReader(..)+ ) where++import Control.Applicative (Alternative(..))+import Control.Monad.IO.Class (MonadIO)+#if __GLASGOW_HASKELL__ <= 806+import Control.Monad.Fail (MonadFail)+#endif+import Control.Monad.Reader (MonadReader(..), ReaderT, runReaderT)+import Control.Monad.Trans (MonadTrans)+import Hedgehog (MonadGen(..))++-- | The CoreGenT monad keeps track of features like language extensions which+-- have an impact on what can be generated. This allows more meaningful random+-- generation, as the output of generators can be constrained to the same+-- variant of Haskell / Clash used by the caller.+--+newtype CoreGenT m a+ = CoreGenT (ReaderT CoreGenConfig m a)+ deriving newtype+ ( Alternative+ , Applicative+ , Functor+ , Monad+ , MonadFail+ , MonadGen+ , MonadIO+ , MonadReader CoreGenConfig+ , MonadTrans+ )++-- | Run a generator that generates types from @clash-lib@. This is intended+-- to transform another monad which implements 'MonadGen'.+--+runCoreGenT :: CoreGenT m a -> CoreGenConfig -> m a+runCoreGenT (CoreGenT act) = runReaderT act++-- | The configuration of Haskell / Clash which the generated source adheres+-- to. These are typically things which change what a user could potentially+-- have written in a source file, such as language extensions.+--+data CoreGenConfig = CoreGenConfig+ { allowDataKinds :: Bool+ , allowPolyKinds :: Bool+ , allowRankNTypes :: Bool+ , allowTypeFamilies :: Bool+ , allowUndecidableInstances :: Bool+ } deriving stock (Show)++-- | The default configuration matches the set of language extensions which+-- are enabled by default when running @clash@ / @clashi@. For most projects,+-- this will likely be the most representative set of options.+--+defaultConfig :: CoreGenConfig+defaultConfig = CoreGenConfig+ { allowDataKinds = True+ , allowPolyKinds = False+ , allowRankNTypes = False+ , allowTypeFamilies = True+ , allowUndecidableInstances = False+ }++canGenDataKinds :: forall m. Monad m => CoreGenT m Bool+canGenDataKinds = reader allowDataKinds++canGenPolyKinds :: forall m. Monad m => CoreGenT m Bool+canGenPolyKinds = reader allowPolyKinds++canGenRankNTypes :: forall m. Monad m => CoreGenT m Bool+canGenRankNTypes = reader allowRankNTypes++canGenTypeFamilies :: forall m. Monad m => CoreGenT m Bool+canGenTypeFamilies = reader allowTypeFamilies++canGenUndecidableInstances :: forall m. Monad m => CoreGenT m Bool+canGenUndecidableInstances = reader allowUndecidableInstances
+ src/Clash/Hedgehog/Core/Name.hs view
@@ -0,0 +1,113 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random generation of names.+-}++module Clash.Hedgehog.Core.Name+ ( genKindName+ , genTypeName+ , genTyConName+ , genTermName+ , genDataConName+ , genVarName+ , genFreshName+ , genNames+ ) where++import Control.Monad.Morph (hoist)+import Data.Functor.Identity (Identity(runIdentity))+import qualified Data.Text as Text+import qualified Faker.Lorem as Fake+import Hedgehog (GenT, MonadGen(GenBase, fromGenT))+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Gen.Faker as Gen++import Clash.Core.DataCon (DcName)+import Clash.Core.Term (TmName)+import Clash.Core.TyCon (TyConName)+import Clash.Core.Type (KiName, TyName)+import Clash.Core.Name+import Clash.Unique (UniqSet, elemUniqSetDirectly, emptyUniqSet, extendUniqSet)++import Clash.Hedgehog.Unique (genUnique)++-- | Generate a name by applying a function to arbitrary text. This is used to+-- ensure that names have the correct case for the thing being named.+--+genOccNameWith :: forall m. MonadGen m => (OccName -> OccName) -> m OccName+genOccNameWith f =+ fromGenT $ hoist @GenT @Identity @(GenBase m)+ (pure . runIdentity)+ (fmap f (Gen.fake Fake.words))++genName :: forall m a. MonadGen m => m OccName -> m (Name a)+genName genOccName =+ Name+ <$> Gen.element [User, System, Internal]+ <*> genOccName+ <*> genUnique+ <*> pure noSrcSpan++genKindName :: forall m. MonadGen m => m KiName+genKindName = genName (genOccNameWith Text.toTitle)++genTypeName :: forall m. MonadGen m => m TyName+genTypeName = genName (genOccNameWith Text.toTitle)++genTyConName :: forall m. MonadGen m => m TyConName+genTyConName = genName (genOccNameWith Text.toTitle)++genTermName :: forall m. MonadGen m => m TmName+genTermName = genName (genOccNameWith Text.toLower)++genDataConName :: forall m. MonadGen m => m DcName+genDataConName = genName (genOccNameWith Text.toTitle)++genVarName :: forall m a. MonadGen m => m (Name a)+genVarName = genName (genOccNameWith Text.toLower)++-- | Generate a name using the given generator, while ensuring the unique of+-- the generated name does not occur in the given @UniqSet@.+--+genFreshName+ :: forall m a b+ . MonadGen m+ => UniqSet b+ -> m (Name a)+ -> m (Name a)+genFreshName used =+ Gen.filterT (not . flip elemUniqSetDirectly used . nameUniq)++mapAccumLM+ :: forall m acc x y+ . Monad m+ => (acc -> x -> m (acc, y))+ -> acc+ -> [x]+ -> m (acc, [y])+mapAccumLM _ acc [] = return (acc, [])+mapAccumLM f acc (x:xs) = do+ (acc', y) <- f acc x+ (acc'', ys) <- mapAccumLM f acc' xs+ return (acc'', y:ys)++-- | Generate a collection of names, from a supplied function to generate names+-- and the number of names to generate.+--+-- TODO While this gives "unique" names because the uniques are different, it+-- can generate multiple names with the same OccName.+genNames+ :: forall m a+ . MonadGen m+ => Int+ -> m (Name a)+ -> m [Name a]+genNames n gen =+ snd <$> mapAccumLM go emptyUniqSet [1..n]+ where+ go used _ = do+ name <- genFreshName used gen+ pure (extendUniqSet used name, name)
+ src/Clash/Hedgehog/Core/Term.hs view
@@ -0,0 +1,358 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random, type-directed generation of Term.+-}++{-# LANGUAGE TupleSections #-}++module Clash.Hedgehog.Core.Term+ ( genTermFrom+ ) where++import Control.Monad (forM)+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range++import Clash.Core.DataCon+import Clash.Core.HasType+import Clash.Core.Pretty (showPpr)+import Clash.Core.Term+import Clash.Core.TyCon+import Clash.Core.Type+import Clash.Core.TysPrim (liftedTypeKind, typeSymbolKind)+import Clash.Core.Util (listToLets)+import Clash.Core.Var+import Clash.Unique++import Clash.Hedgehog.Core.Literal+import Clash.Hedgehog.Core.Monad+import Clash.Hedgehog.Core.Name+import Clash.Hedgehog.Core.Type+import Clash.Hedgehog.Core.Var+import Clash.Hedgehog.Unique++-- | Sample a data constructor from the environment, potentially partially+-- applying it so that the type fits the hole. If there are no possible fits+-- for the hole in the environment, an alternative generator is used instead.+sampleDataConOr+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -- ^ The types in scope while generating+ -> Type+ -- ^ The hole to generate a fit for+ -> (Type -> CoreGenT m Term)+ -- ^ A generator for sub-holes (used when partially applying a fit)+ -> CoreGenT m Term+ -- ^ A generator to use if there are no hole fits+ -> CoreGenT m Term+sampleDataConOr tcm hole genSub genOr =+ sampleDataCon <|> genOr+ where+ sampleDataCon = do+ -- TODO We cannot fill in any datacon where the type is polymorphic. This+ -- is because sampleUniqMap will never pick one because it cannot see the+ -- fit is valid without unification. See the TODO by sampleUniqMap.+ --+ -- We mitigate this by not generating algebraic type constructors with+ -- kinds other than Type, i.e. no type params / poly kinds. See the+ -- 'genAlgTyCon' function and NOTE [finding more complex fits].+ let dcs = concatMap tyConDataCons tcm+ let dcm = listToUniqMap (zip dcs dcs)+ (dc, holes) <- sampleUniqMap (const True) hole dcm+ holeFills <- traverse genSub holes++ pure (mkTmApps (Data dc) holeFills)++-- | Attempt to sample an identifier which can be made to fit a hole of the+-- desired type. If this is not possible (due to nothing in the environment+-- matching) then the given alternative generator is used instead.+--+sampleIdOr+ :: forall m+ . (Alternative m, MonadGen m)+ => UniqMap (Either TyVar Id)+ -- ^ The currently bound type and term variables+ -> Type+ -- ^ The hole to generate a fit for+ -> (Type -> CoreGenT m Term)+ -- ^ A generator for sub-holes (used when partially applying a fit)+ -> CoreGenT m Term+ -- ^ A generator to use if there are no hole fits+ -> CoreGenT m Term+sampleIdOr env hole genSub genOr =+ sampleId <|> genOr+ where+ sampleId = do+ let tmEnv = mapMaybeUniqMap (either (const Nothing) Just) env+ (i, holes) <- sampleUniqMap (const True) hole tmEnv+ holeFills <- traverse genSub holes++ pure (mkTmApps (Var i) holeFills)++-- | Generate a term that is valid for the given type constructor map and+-- environment of free type and term variables. The term generated must have+-- the specified type.+--+genTermFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -- ^ The types in scope while generating+ -> UniqMap (Either TyVar Id)+ -- ^ The currently bound type and term variables+ -> Type+ -- ^ The type of the term being generated+ -> CoreGenT m Term+genTermFrom tcm env hole =+ let genSub = genTermFrom tcm env+ genOr = genFreshTerm tcm env hole+ in Gen.choice+ [ sampleDataConOr tcm hole genSub genOr+ , sampleIdOr env hole genSub genOr+ ]++{-+NOTE [generated terms]+~~~~~~~~~~~~~~~~~~~~~~+Term generation is currently limited in some ways. This is for no particular+reason other than to make the generator easier to understand. For example++ * when the hole is a forall or a function, a lambda (or tick) is inserted+ instead of allowing expressions like letrec or case which could still have+ the desired type++ * primitives are not currently generated, as we likely want to build a+ collection of known primitives when we build the environments before making+ types and terms for tests++ * casts are currently not generated, as the majority are discarded by Clash+ during the GHC2Core stage. See PR #1064.+-}++-- | Generate a "fresh" term, i.e. one which is randomly created according to+-- the type of the hole, rather than sampling from the known variables or data+-- constructors.+--+-- This generator will fail if there are no values for the given hole.+--+genFreshTerm+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap (Either TyVar Id)+ -> Type+ -> CoreGenT m Term+genFreshTerm tcm env hole =+ -- We need to normalize in case the hole is a type family.+ --+ -- TODO When casts are supported, this will need a cast between the+ -- normalized type and the given type.+ case normalizeType tcm hole of+ -- Hole: forall i. a+ normHole@(ForAllTy i a) ->+ Gen.recursive Gen.choice+ [TyLam i <$> genTermFrom tcm (extendUniqMap i (Left i) env) a]+ [Tick <$> genTickInfo tcm <*> genFreshTerm tcm env normHole]++ AnnType _ a ->+ genTermFrom tcm env a++ normHole ->+ case tyView normHole of+ -- Hole: a -> b+ FunTy a b ->+ Gen.recursive Gen.choice+ [do i <- genLocalId a (genFreshName (uniqMapToUniqSet env) genVarName)+ Gen.subterm (genTermFrom tcm (extendUniqMap i (Right i) env) b) (Lam i)+ ]+ [Tick <$> genTickInfo tcm <*> genFreshTerm tcm env normHole]++ -- Hole: Primitive type constructor.+ TyConApp tcn []+ | Just PrimTyCon{} <- lookupUniqMap tcn tcm+ -> Gen.recursive Gen.choice+ [Literal <$> genLiteralFrom normHole]+ -- We may fail to generate a case expression if there is nothing+ -- in scope to use as a subject. If this happens, let bindings+ -- are introduced so next time genCase is called it does not fail.+ [ genCase tcm env normHole <|> genLet tcm env normHole+ , genLet tcm env normHole+ ]++ -- Hole: Algebraic type constructor.+ TyConApp tcn _+ | Just AlgTyCon{} <- lookupUniqMap tcn tcm+ -- We may have got here by trying to fill the hole with an identifier, so+ -- it makes sense to try again. If we got here by sampleDataConOr, the+ -- data constructor is isomorphic to Void, and we will hit the error.+ -> Gen.recursive Gen.choice+ [sampleDataConOr tcm hole (genTermFrom tcm env)+ (error ("No term level value for hole: " <> showPpr hole))]+ -- We may fail to generate a case expression if there is nothing+ -- in scope to use as a subject. If this happens, let bindings+ -- are introduced so next time genCase is called it does not fail.+ [ genCase tcm env normHole <|> genLet tcm env normHole+ , genLet tcm env normHole+ ]++ _ ->+ error ("No term level value for hole: " <> showPpr normHole)++-- TODO+-- genIsMultiPrim+-- genPrimInfo+-- genPrimUnfolding+-- genMultiPrimInfo+-- genWorkInfo++genLet+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap (Either TyVar Id)+ -> Type+ -> CoreGenT m Term+genLet tcm env hole = do+ binds <- genLetBindings tcm env+ let vars = fmap fst binds+ let env' = extendListUniqMap env (zip vars (fmap Right vars))++ body <- genTermFrom tcm env' hole++ pure (listToLets binds body)++genLetBindings+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap (Either TyVar Id)+ -> CoreGenT m [LetBinding]+genLetBindings tcm env = do+ let tyEnv = mapMaybeUniqMap (either Just (const Nothing)) env+ -- Limit the number of new bindings to 8 to prevent an explosion in the+ -- number of sub-holes to generate.+ types <- Gen.list (Range.linear 1 8) (genMonoTypeFrom tcm tyEnv liftedTypeKind)+ vars <- genVars genLocalId types genVarName++ forM (zip vars types) $ \(v, ty) ->+ -- Bindings can be indirectly recursive, but not directly recursive. This+ -- stops the generator from generating let x = x in ...+ let vars' = filter (/= v) vars+ env' = extendListUniqMap env (zip vars' (fmap Right vars'))+ in (v,) <$> genTermFrom tcm env' ty++{-+NOTE [generating useful case expressions]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+When generating case expressions, it is perfectly valid to generate something+like the following:++ case C x_1 ... x_n of+ C p_1 ... p_n -> ...++However, we want to favour generating the more interesting case expressions+where the subject is an application on variables, like so++ case v x_1 ... x_n of+ C p_1 ... p_i -> ...+ D p_1 ... p_j -> ...+ E p_1 ... p_k -> ...++Likewise, we want to avoid generating case expressions with literals as the+subject, or function types (where the only viable pattern is DefaultPat). While+these are valid terms to generate, the generator will naturally bias towards+them, making too many of the tests too "artificial" in nature.++A downside of this approach is that generating a case expression is not+guaranteed to work, as if there is nothing in the environment that can be used+as the subject then the generator will return 'empty'. However, since letrec+always passes and introduces new bindings, we fallback to this if case fails.+This means the failure will happen at most once when generating.+-}++genCase+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap (Either TyVar Id)+ -> Type+ -> CoreGenT m Term+genCase tcm env altTy = do+ -- I need to select something as the subject. It can be any type, but should+ -- bias towards something from the environment where possible. It may not be+ -- possible though, so I should be able to fallback to just building a term.+ let tmEnv = mapMaybeUniqMap (either (const Nothing) Just) env+ subj <- sampleSubjFrom tmEnv+ let subjTy = inferCoreTypeOf tcm subj++ case fmap fst (splitTyConAppM subjTy) of+ Just tcn ->+ case lookupUniqMap tcn tcm of+ Just tc@AlgTyCon{} -> do+ dcs <- Gen.subsequence (tyConDataCons tc)+ dcPats <- traverse genDataPatFrom dcs+ alts <- traverse genAltFrom (DefaultPat : dcPats)++ pure (Case subj altTy alts)++ Just PrimTyCon{} -> do+ -- Upper bound is 8 to prevent explosion in number of sub-holes.+ litPats <- Gen.list (Range.linear 0 8) (LitPat <$> genLiteralFrom subjTy)+ alts <- traverse genAltFrom (DefaultPat : litPats)++ pure (Case subj altTy alts)++ _ -> do+ alt <- genAltFrom DefaultPat+ pure (Case subj altTy [alt])++ _ -> do+ alt <- genAltFrom DefaultPat+ pure (Case subj altTy [alt])+ where+ -- Subjects are applications on variables in the environment.+ -- See NOTE [generating useful case expressions].+ sampleSubjFrom :: UniqMap Id -> CoreGenT m Term+ sampleSubjFrom tmEnv = do+ (v, holes) <- sampleAnyUniqMap tmEnv+ holeFills <- traverse (genTermFrom tcm env) holes++ pure (mkTmApps (Var v) holeFills)++ genDataPatFrom :: DataCon -> CoreGenT m Pat+ genDataPatFrom dc = do+ ids <- genVars genLocalId (dcArgTys dc) genVarName+ pure (DataPat dc (dcExtTyVars dc) ids)++ genAltFrom :: Pat -> CoreGenT m Alt+ genAltFrom pat = do+ let (tvs, ids) = patIds pat+ let toTvBind x = (varUniq x, Left x)+ let toIdBind x = (varUniq x, Right x)++ -- Generate the terms in alternatives with the newly bound vars in scope.+ let env' = extendListUniqMap env (fmap toTvBind tvs <> fmap toIdBind ids)+ term <- genTermFrom tcm env' altTy++ pure (pat, term)++-- TODO genCast++genTickInfo+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> CoreGenT m TickInfo+genTickInfo tcm =+ Gen.choice+ [ NameMod <$> genNameMod <*> genClosedKindFrom tcm typeSymbolKind+ , Gen.constant DeDup+ , Gen.constant NoDeDup+ ]++genNameMod :: forall m. MonadGen m => m NameMod+genNameMod = Gen.element [PrefixName, SuffixName, SuffixNameP, SetName]
+ src/Clash/Hedgehog/Core/TyCon.hs view
@@ -0,0 +1,305 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random generation of type constructors.+-}++{-# LANGUAGE LambdaCase #-}++module Clash.Hedgehog.Core.TyCon+ ( genTyConMap+ ) where++import Control.Monad (forM)+import Data.Coerce (coerce)+import Data.Either (rights)+import Hedgehog (Range)+import qualified Hedgehog.Gen as Gen++import Clash.Core.DataCon+import Clash.Core.HasType+import Clash.Core.Name (nameUniq)+import Clash.Core.Subst+import Clash.Core.TyCon+import Clash.Core.Type (Kind, Type(VarTy), mkTyConApp, splitFunForallTy)+import Clash.Core.TysPrim (liftedTypeKind, tysPrimMap)+import Clash.Core.Var+import Clash.Core.VarEnv+import Clash.Unique++import Clash.Hedgehog.Core.DataCon+import Clash.Hedgehog.Core.Monad+import Clash.Hedgehog.Core.Name+import Clash.Hedgehog.Core.Type+import Clash.Hedgehog.Core.Var+import Clash.Hedgehog.Unique++{-+Note [order of generation]+~~~~~~~~~~~~~~~~~~~~~~~~~~+In Clash core (as with GHC core), there is a degree of circularity:++ * A type can be a type constructor (referenced by name)+ * A type constructor has a type (kind)+ * A data constructor has a type+ * A type constructor may contain data constructors++This makes it impossible to naively write a generator for these parts of the+core IR, as such a generator may never terminate. However not everything+generated is completely random, e.g. the codomain of a data constructor is+always the type constructor the data constructor belongs to.++A reasonable approximation of a real program can be made by first generating+an environment, then generating things which exist within that environment. To+that end, the first thing (typically) to generate is a TyConMap, which contains+information about all type constructors that exist. This leads to a sensible+order of generation, e.g.++ * generate a TyConMap, `tcm`+ * generate a kind that exists in `tcm`, `k`+ * generate a type of kind `k` that exists in `tcm`, `a`+ * generate a term of type `a` that exists in `tcm`++By generating the TyConMap first, the generation of complete programs becomes+a more manageable process of running increasingly more constrained generators.+This helps ensure that generated data is well-formed, as a constrained+generator produces random hole-fits instead of completely arbitrary values.+-}++arityOf :: Kind -> Int+arityOf = length . fst . splitFunForallTy++-- | A TyConMap contains all the algebraic data types and type families that+-- are used in a program. This is typically the first thing that should be+-- generated, as calls to other generators like 'genKind' or 'genTypeFrom' will+-- likely want to use the type constructors added to the TyConMap.+--+-- TODO It would be nice if this also included types from @clash-prelude@ like+-- Signal and the sized number types. Maybe we want to hook into @clash-ghc@+-- to load type constructors and primitives from @Clash.Prelude@.+--+genTyConMap+ :: forall m+ . (Alternative m, MonadGen m)+ => Range Int+ -> CoreGenT m TyConMap+genTyConMap numDcs = go tysPrimMap+ where+ -- Either stop adding new items to the TyConMap, or generate a new item.+ -- 'Gen.recursive' is necessary to ensure termination.+ go tcm =+ Gen.recursive Gen.choice+ [Gen.constant tcm]+ [Gen.subtermM (extendTyConMap tcm) go]++ extendTyConMap tcm = do+ -- We return new UniqMap instead of individual TyCon, because for AlgTyCon+ -- we may also generate PromotedDataCon for -XDataKinds.+ new <- canGenTypeFamilies >>= \case+ True -> Gen.choice+ [ genAlgTyConFrom numDcs tcm+ , genFunTyConFrom tcm <|> genAlgTyConFrom numDcs tcm+ ]+ False -> Gen.choice [genAlgTyConFrom numDcs tcm]++ pure (unionUniqMap tcm new)++-- | Generate a new algebraic type constructor using the types that are already+-- in scope. This will also promote data constructors if the configuration+-- supports @-XDataKinds@.+--+genAlgTyConFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => Range Int+ -> TyConMap+ -> CoreGenT m TyConMap+genAlgTyConFrom range tcm = do+ let used = uniqMapToUniqSet (fmap tyConUniq tcm)+ name <- genFreshName used genTyConName++ -- TODO We want to use this, but we cannot sample polymorphic constructors+ -- when making Term / Type, so we avoid generating polymorphic data now.+ --+ -- See NOTE [finding more complex fits] in Clash.Hedgehog.Unique.+ --+ -- let argGen = genClosedKindFrom tcm liftedTypeKind+ -- kn <- genWithCodomain liftedTypeKind argGen++ -- All ADTs live in the kind Type+ let kn = liftedTypeKind+ let arity = arityOf kn++ rhs <- Gen.choice+ [ DataTyCon <$> genDataConsFrom range tcm name kn+ -- TODO Generate NewTyCon+ ]++ let tc = AlgTyCon (nameUniq name) name kn arity rhs False++ canGenDataKinds >>= \case+ True ->+ -- Promote all the data constructors in the TyCon.+ let dcs = tyConDataCons tc+ in pure (listToUniqMap ((name, tc) : fmap promoteDataCon dcs))++ False ->+ pure (unitUniqMap name tc)+ where+ promoteDataCon dc =+ let tcn = coerce (dcName dc)+ arity = arityOf (dcType dc)+ in (tcn, PromotedDataCon (dcUniq dc) tcn (dcType dc) arity dc)++-- TODO In the future we may want to also generate indirectly recursive type+-- families. For example:+--+-- Even 0 = 'True Odd 0 = 'False+-- Even n = Odd (n - 1) Odd n = Even (n - 1)++-- | Generate a new type family, using the types that are already in scope.+--+genFunTyConFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> CoreGenT m TyConMap+genFunTyConFrom tcm = do+ let used = uniqMapToUniqSet (fmap tyConUniq tcm)+ name <- genFreshName used genTyConName++ kn <- genClosedKindFrom tcm liftedTypeKind+ let arity = arityOf kn++ let (argKns, resKn) = splitFunForallTy kn+ substs <- genSubsts name (rights argKns) resKn++ let tc = FunTyCon (nameUniq name) name kn arity substs+ pure (unitUniqMap name tc)+ where+ genSubsts :: TyConName -> [Kind] -> Kind -> CoreGenT m [([Type], Type)]+ genSubsts _ [] rhsKn = do+ -- Nullary type family, we only need to generate the RHS type+ let tcm' = filterUniqMap (not . isPrimTc) tcm+ rhs <- genMonoTypeFrom tcm' emptyUniqMap rhsKn++ pure [([], rhs)]++ genSubsts name argKns rhsKn = do+ let tcm' = filterUniqMap (not . isPrimTc) tcm++ tvs <- genVars genTyVar argKns genVarName+ let acc = fmap (\x -> (unitUniqMap x x, VarTy x)) tvs++ lhss <- refineArgs tcm acc++ forM lhss $ \args -> do+ -- The RHS of each equation can use free vars in the types, since types+ -- in the LHS of a type family are treated more like patterns.+ let free = mconcat (fmap fst args)++ -- Direct recursion in type families requires -XUndecidableInstances.+ rhs <- canGenUndecidableInstances >>= \case+ True -> Gen.choice+ [ genMonoTypeFrom tcm' free rhsKn+ , mkTyConApp name+ <$> traverse (genMonoTypeFrom tcm' free) argKns+ ]+ False -> genMonoTypeFrom tcm' free rhsKn++ pure (fmap snd args, rhs)++refineArgs+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> [(UniqMap TyVar, Type)]+ -> m [[(UniqMap TyVar, Type)]]+refineArgs tcm args = go [args]+ where+ go acc =+ Gen.recursive Gen.choice+ [Gen.constant acc]+ [Gen.subtermM (refineAgain acc) go]++ refineAgain acc@(xs:_) = do+ -- Every arg can be refined or left alone.+ let gen x = Gen.choice [uncurry (refineArg tcm) x, Gen.constant x]+ refined <- traverse gen xs+ pure (refined : acc)++ refineAgain [] =+ error "refineArgs: No types to refine."++-- | Refine a type, selecting one of the free variables and substituting it+-- for a type constructor of the desired kind (filling in any holes with new+-- type variables). For example, successive calls may give+--+-- a ~> A b c ~> A (B b) c ~> A (B b) C ~> A (B D) C+--+refineArg+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Type+ -> m (UniqMap TyVar, Type)+refineArg tcm free ty+ | nullUniqMap free+ = pure (free, ty)++ | otherwise+ = do -- Pick a free variable and remove it from free vars+ fv <- fst <$> sampleAnyUniqMap free+ let free' = delUniqMap free fv++ -- Pick a type constructor that fits that free variable. This cannot be+ -- an unboxed primitive type, so for now all primitive types are excluded.+ -- This is slightly too strict, as Integer and Natural can be used.+ (tc, holes) <- sampleUniqMapBiased (not . isPrimTc) (coreTypeOf fv) tcm++ -- Take any holes for that constructor and make them new free variables.+ holeVars <- genVars genTyVar holes genVarName+ let free'' = extendListUniqMap free' (zip holeVars holeVars)++ -- Substitute the removed free variable for the type constructor with+ -- any new free variables applied to it.+ let inScope = extendInScopeSetList emptyInScopeSet (eltsUniqMap free'')+ let substTv = unitVarEnv fv (mkTyConApp (tyConName tc) (fmap VarTy holeVars))+ let subst = mkTvSubst inScope substTv++ -- Return the refined type and free variable environment.+ pure (free'', substTy subst ty)++{-+Note [generating substs]+~~~~~~~~~~~~~~~~~~~~~~~~+When generating a FunTyCon, we generate a sequence of alternatives like so:++ type family F t_1 t_2 ... t_n :: k where+ F a_1 a_2 ... a_n = k_1+ F b_1 b_2 ... b_n = k_2+ ...++In "real" code, these would typically be written in a way where no alternatives+become dead, i.e. if you start with++ F v_1 v_2 ... v_n++where all arguments v_1 are type variables, this pattern will always be used+and the other alternatives never considered. To ensure FunTyCon are more+realistic, alternatives should be ordered from more specific to more general.++We can achieve this by starting from the most general solution and working+towards a more specific solution. At each step we can either return the list+of alternatives, or make a more specific alternative based on the previous+most specific alternative and put this at the head of the list. The returned+list is then guaranteed to not have any dead alternatives. Multiple of these+lists can be merged provided the merge operation preserves the ordering of+more to less specific.++If there is need to test type families where some alternatives may be dead, we+can use Gen.shuffle to rearrange the substs before taking a subsequence.+-}
+ src/Clash/Hedgehog/Core/Type.hs view
@@ -0,0 +1,539 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random kind-directed generation of Kind and Type.+-}++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE LambdaCase #-}++module Clash.Hedgehog.Core.Type+ ( genKindFrom+ , genClosedKindFrom+ , genPolyTypeFrom+ , genClosedPolyType+ , genMonoTypeFrom+ , genClosedMonoType+ , genWithCodomain+ ) where++import Data.Coerce (coerce)+import Data.Monoid (Any(..))+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range++import Clash.Core.DataCon+import Clash.Core.HasType (piResultTys)+import Clash.Core.Pretty (showPpr)+import Clash.Core.Subst (aeqType)+import Clash.Core.TyCon+import Clash.Core.Type+import Clash.Core.TysPrim+import Clash.Unique++import Clash.Hedgehog.Core.Monad+import Clash.Hedgehog.Core.Name+import Clash.Hedgehog.Core.Var+import Clash.Hedgehog.Unique++-- | Classify a type or kind according to some criteria. The classification+-- of a type or kind is used to determine the pre-defined types / kinds which+-- can be used in hole fills. See 'classify' and 'useTyCon'.+--+data Class = Class+ { cData :: !Any -- ^ Uses -XDataKinds+ , cPoly :: !Any -- ^ Uses -XPolyKinds (if classifying a kind)+ , cRankN :: !Any -- ^ Uses -XRankNTypes+ , cFamily :: !Any -- ^ Uses -XTypeFamilies+ } deriving (Show)++instance Semigroup Class where+ x <> y = Class+ { cData = cData x <> cData y+ , cPoly = cPoly x <> cPoly y+ , cRankN = cRankN x <> cRankN y+ , cFamily = cFamily x <> cFamily y+ }++instance Monoid Class where+ mempty = Class mempty mempty mempty mempty++-- | Classify the groups that a type / kind belongs to, in order to filter out+-- kinds which are not compatible with the chosen 'CoreGenConfig'. This+-- combines multiple checks into one for efficiency, to prevent multiple passes+-- over each kind which can potentially be used.+--+classify :: Bool -> TyConMap -> KindOrType -> Class+classify isKind tcm = go+ where+ go ty =+ case tyView ty of+ FunTy a b ->+ -- If the domain is polymorphic then we have -XRankNTypes.+ mempty { cRankN = Any (isPolyTy a) } <> go a <> go b++ TyConApp tcn args ->+ let tc = lookupUniqMap' tcm tcn+ isPoly = isPolyTy (piResultTys tcm (tyConKind tc) args)+ in case lookupUniqMap' tcm tcn of+ AlgTyCon{} ->+ -- If the constructor is algebraic then we have -XDataKinds if+ -- we are classifying a Kind instead of a Type.+ mempty { cData = Any isKind, cPoly = Any isPoly }+ <> mconcat (fmap go args)++ PromotedDataCon{} ->+ -- If the constructor is a promoted data constructor then we+ -- have -XDataKinds.+ mempty { cData = Any True, cPoly = Any isPoly }+ <> mconcat (fmap go args)++ FunTyCon{} ->+ -- If the constructor is a function then we have -XTypeFamilies.+ mempty { cPoly = Any isPoly, cFamily = Any True }+ <> mconcat (fmap go args)++ PrimTyCon{}+ -- There's nothing special about Type.+ | aeqType ty liftedTypeKind -> mempty++ -- If the constructor is Nat or Symbol, we have -XDataKinds.+ | aeqType ty typeNatKind -> mempty { cData = Any True }+ | aeqType ty typeSymbolKind -> mempty { cData = Any True }++ -- If the constructor is ~# then we have -XTypeFamilies.+ | aeqType ty eqPrimTy ->+ mempty { cPoly = Any isPoly, cFamily = Any True }+ <> mconcat (fmap go args)++ -- If the constructor is anything else we have -XDataKinds if+ -- we are classifying a Kind instead of a Type.+ | otherwise ->+ mempty { cData = Any isKind, cPoly = Any isPoly }+ <> mconcat (fmap go args)++ OtherType{} ->+ case ty of+ ForAllTy _ a ->+ -- If there are quantifiers then we have polymorphism.+ mempty { cPoly = Any True } <> go a++ LitTy{} ->+ -- If there are literals then we have -XDataKinds.+ mempty { cData = Any True }++ VarTy _ -> mempty+ AppTy a b -> go a <> go b+ AnnType _ a -> go a+ ConstTy _ -> error ("classify: Naked ConstTy: " <> showPpr ty)++-- | Decide whether to use a type constructor based on the configuration and+-- the result of 'classifyKind'. A type constructor is not usable if it uses+-- any features which are not included in the current configuration.+--+useTyCon :: Bool -> CoreGenConfig -> TyConMap -> TyCon -> Bool+useTyCon isKind config tcm tc+ | isKind+ = and+ -- We don't generate equalities at the kind level, because the only+ -- witness we have for equality is a term-level primitive (_CO_).+ [ isPrimKind ty+ , getAny (cData c) --> allowDataKinds config+ , getAny (cPoly c) --> allowPolyKinds config+ , getAny (cRankN c) --> allowRankNTypes config+ , getAny (cFamily c) --> allowTypeFamilies config+ ]++ | otherwise+ = and+ -- We don't generate Type, Nat or Symbol at the type level, because they+ -- have no term-level inhabitants. We also don't generate constraints+ -- like ~# because constraints are generated separately.+ [ not (isPrimKind ty)+ , not (aeqType ty eqPrimTy)+ , getAny (cData c) --> allowDataKinds config+ , getAny (cRankN c) --> allowRankNTypes config+ , getAny (cFamily c) --> allowTypeFamilies config+ ]+ where+ a --> b = not a || b+ isPrimKind a = any (aeqType a) [liftedTypeKind, typeNatKind, typeSymbolKind]+ ty = mkTyConTy (tyConName tc)+ c = classify isKind tcm ty++-- | Generate a function where the codomain is the given type / kind. Any other+-- restrictions are enforced by the given generator. This can be used with+-- generators for kinds and types.+--+genWithCodomain+ :: forall m+ . (Alternative m, MonadGen m)+ => Kind+ -> CoreGenT m KindOrType+ -> CoreGenT m KindOrType+genWithCodomain cod gen = do+ (args, res) <- fmap splitFunForallTy gen+ pure (mkPolyFunTy cod (args <> [Right res]))++-- TODO+-- genConstraints+-- genConstrained++-- | Generate a closed kind (one without any free variables). If you want to+-- be able to use free variables in a kind, see 'genKindFrom'.+--+genClosedKindFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> Kind+ -> CoreGenT m Kind+genClosedKindFrom tcm =+ genKindFrom tcm emptyUniqMap++-- | Generate a kind which is valid for the given 'TyConMap'. The kind may+-- contain free variables which are given in a 'UniqMap', and is a valid fit+-- for a hole with the given kind.+--+-- __N.B.__ Although the kind generated is a fit for the given hole, calling+-- a function like 'Clash.Core.HasType.inferCoreKindOf' may return a different+-- kind. This is because quantifiers are both the introduction rule for kind+-- arrows and a kind former of their own right, so for the hole+--+-- Type -> Type+--+-- a generated fit might be+--+-- forall a. a -> a+--+-- but this is then inferred to have the kind+--+-- Type+--+genKindFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Kind+genKindFrom tcm env hole =+ let genSub = genKindFrom tcm env+ -- A special case for holes of kind Type: we do not attempt to generate+ -- a fresh hole fit as this will produce an endless stream of (->) when+ -- not using -XPolyKinds.+ genOr = if aeqType hole liftedTypeKind+ then empty+ else genFreshKind tcm env hole+ in Gen.choice+ [ sampleTyConOr True tcm hole genSub+ (sampleTyVarOr env hole genSub genOr)+ , sampleTyVarOr env hole genSub+ (sampleTyConOr True tcm hole genSub genOr)+ ]++-- | Generate a polymorphic type which is valid for the given environment.+-- The generated type should have the specified kind, and no free variables.+--+genClosedPolyType+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> Kind+ -> CoreGenT m Type+genClosedPolyType tcm =+ genPolyTypeFrom tcm emptyUniqMap++-- | Generate a polymorphic type which is valid for the given environment.+-- The generated type should have the specified kind, and may contain the+-- specified free variables.+--+genPolyTypeFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Type+genPolyTypeFrom tcm env hole =+ let genSub = genPolyTypeFrom tcm env+ genOr = genFreshPolyType tcm env hole+ in Gen.choice+ [ sampleTyConOr False tcm hole genSub+ (sampleTyVarOr env hole genSub genOr)+ , sampleTyVarOr env hole genSub+ (sampleTyConOr False tcm hole genSub genOr)+ , genFreshPolyType tcm env hole+ ]++-- | Generate a monomorphic type which is valid for the given environment.+-- The generated type should have the specified kind, and no free variables.+--+genClosedMonoType+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> Kind+ -> CoreGenT m Type+genClosedMonoType tcm =+ genMonoTypeFrom tcm emptyUniqMap++-- | Generate a monomorphic type which is valid for the given environment.+-- The generated type should have the specified kind, and may contain the+-- specified free variables.+--+genMonoTypeFrom+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Type+genMonoTypeFrom tcm env hole =+ let genSub = genMonoTypeFrom tcm env+ -- TODO Maybe this can be changed for types, because it is always free+ -- to generate a forall, and the new binder may help break loops.+ genOr = if aeqType hole liftedTypeKind+ then empty+ else genFreshMonoType tcm env hole+ in Gen.choice+ [ sampleTyConOr False tcm hole genSub+ (sampleTyVarOr env hole genSub genOr)+ , sampleTyVarOr env hole genSub+ (sampleTyConOr False tcm hole genSub genOr)+ , genFreshMonoType tcm env hole+ ]++-- | For the given hole, attempt to use a variable in the environment to fill+-- the hole, potentially solving subgoals if the variable is function kinded+-- and the hole is the codomain.+--+sampleTyVarOr+ :: forall m+ . (Alternative m, MonadGen m)+ => UniqMap TyVar+ -> Kind+ -> (Kind -> CoreGenT m KindOrType)+ -> CoreGenT m KindOrType+ -> CoreGenT m KindOrType+sampleTyVarOr env hole genSub genOr =+ sampleTyVar <|> genOr+ where+ sampleTyVar = do+ (tv, holes) <- sampleUniqMap (const True) hole env+ holeFills <- traverse genSub holes++ pure (foldr AppTy (VarTy tv) holeFills)++-- | For the given hole, attempt to use a type constructor in the 'TyConMap' to+-- fill the hole, potentially solving subgoals if the constructor is function+-- kinded and the hole is the codomain.+--+sampleTyConOr+ :: forall m+ . (Alternative m, MonadGen m)+ => Bool+ -> TyConMap+ -> Kind+ -> (Kind -> CoreGenT m KindOrType)+ -> CoreGenT m KindOrType+ -> CoreGenT m KindOrType+sampleTyConOr isKind tcm hole genSub genOr =+ sampleTyCon <|> genOr+ where+ sampleTyCon = do+ config <- ask+ (tc, holes) <- sampleUniqMapBiased (useTyCon isKind config tcm) hole tcm+ holeFills <- traverse genSub holes++ pure (mkTyConApp (tyConName tc) holeFills)++genForAll+ :: forall m+ . (Alternative m, MonadGen m)+ => UniqMap TyVar+ -> Kind+ -> Kind+ -> (UniqMap TyVar -> Kind -> CoreGenT m KindOrType)+ -> CoreGenT m KindOrType+genForAll env k1 k2 genSub = do+ v <- genTyVar k1 (genFreshName (uniqMapToUniqSet env) genVarName)+ Gen.subterm (genSub (extendUniqMap v v env) k2) (ForAllTy v)++-- | Generate a "fresh" kind. This involves using the shape of the hole to+-- generate a layer of the result kind, then solving any subgoal with either+-- a variable, type constructor or another "fresh" kind.+--+genFreshKind+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Kind+genFreshKind tcm env hole =+ canGenPolyKinds >>= \case+ True -> genPolyKind tcm env hole+ False -> genMonoKind tcm env hole++-- | Generate a potentially polymorphic kind to fill a hole. This should not be+-- exported as it can be used to circumvent constraints on generation which are+-- given by the 'CoreGenConfig'.+--+genPolyKind+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Kind+genPolyKind tcm env hole+ -- Hole: forall v. a+ | ForAllTy v a <- hole+ = let env' = extendUniqMap v v env+ in Gen.subterm (genKindFrom tcm env' a) (ForAllTy v)++ -- Hole: a -> b+ | FunTy a b <- tyView hole+ = genForAll env a b (genKindFrom tcm)++ -- Hole: Type+ --+ -- If -XRankNTypes is not enabled, then we make sure the LHS of a generated+ -- arrow kind is a monomorphic kind.+ --+ -- As we shrink, it becomes more likely we just return Type for this hole.+ -- This rule is needed to prevent the generator recursing infinitely.+ | aeqType hole liftedTypeKind+ = canGenRankNTypes >>= \case+ True ->+ let polyGen = genKindFrom tcm env liftedTypeKind+ in Gen.choice+ [ Gen.subterm2 polyGen polyGen mkFunTy+ , genForAll env liftedTypeKind liftedTypeKind (genKindFrom tcm)+ ]++ False ->+ let polyGen = genKindFrom tcm env liftedTypeKind+ monoGen = local (\r -> r { allowPolyKinds = False }) polyGen+ in Gen.choice+ [ Gen.subterm2 monoGen polyGen mkFunTy+ , genForAll env liftedTypeKind liftedTypeKind (genKindFrom tcm)+ ]++ -- The hole is not anything which may result in a quantifier being generated,+ -- so we can fallback to genMonoKind for these cases.+ | otherwise+ = genMonoKind tcm env hole++genMonoKind+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Kind+genMonoKind tcm env hole+ -- Hole: C+ | ConstTy (TyCon tcn) <- hole+ , Just tc <- lookupUniqMap tcn tcm+ , let dcs = tyConDataCons tc+ , not (null dcs)+ = do dc <- Gen.element dcs+ args <- traverse (genKindFrom tcm env) (dcArgTys dc)+ pure (mkTyConApp (coerce (dcName dc)) args)++ -- Hole: Nat+ | aeqType hole typeNatKind+ = canGenDataKinds >>= \case+ True -> LitTy . NumTy . toInteger <$> Gen.word Range.linearBounded+ False -> error "genMonoKind: Cannot generate Nat without -XDataKinds"++ -- Hole: Symbol+ | aeqType hole typeSymbolKind+ = canGenDataKinds >>= \case+ True -> LitTy . SymTy <$> Gen.string (Range.linear 5 10) Gen.alphaNum+ False -> error "genMonoKind: Cannot generate Symbol without -XDataKinds"++ -- Hole: Type+ --+ -- As we shrink, it becomes more likely we just return Type for this hole.+ -- This rule is needed to prevent the generator recursing infinitely.+ | aeqType hole liftedTypeKind+ = let gen = genKindFrom tcm env liftedTypeKind+ in Gen.subterm2 gen gen mkFunTy++ | otherwise+ = error ("genMonoKind: Cannot generate fit for hole: " <> showPpr hole)++genFreshPolyType+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Type+genFreshPolyType tcm env hole+ | ForAllTy tv kn <- hole+ = let env' = extendUniqMap tv tv env+ in Gen.subterm (genPolyTypeFrom tcm env' kn) (ForAllTy tv)++ | FunTy a b <- tyView hole+ = genForAll env a b (genPolyTypeFrom tcm)++ | aeqType hole liftedTypeKind+ = canGenRankNTypes >>= \case+ True ->+ let polyGen = genPolyTypeFrom tcm env liftedTypeKind+ in Gen.choice+ [ genFreshMonoType tcm env liftedTypeKind+ , Gen.subterm2 polyGen polyGen mkFunTy+ , genForAll env liftedTypeKind liftedTypeKind (genPolyTypeFrom tcm)+ ]++ False ->+ let polyGen = genPolyTypeFrom tcm env liftedTypeKind+ monoGen = genMonoTypeFrom tcm env liftedTypeKind+ in Gen.choice+ [ genFreshMonoType tcm env hole+ , Gen.subterm2 monoGen polyGen mkFunTy+ , genForAll env liftedTypeKind liftedTypeKind (genPolyTypeFrom tcm)+ ]++ | otherwise+ = genFreshMonoType tcm env hole++genFreshMonoType+ :: forall m+ . (Alternative m, MonadGen m)+ => TyConMap+ -> UniqMap TyVar+ -> Kind+ -> CoreGenT m Type+genFreshMonoType tcm env hole+ | ConstTy (TyCon tcn) <- hole+ , Just tc <- lookupUniqMap tcn tcm+ , let dcs = tyConDataCons tc+ , not (null dcs)+ = do dc <- Gen.element dcs+ args <- traverse (genMonoTypeFrom tcm env) (dcArgTys dc)+ pure (mkTyConApp (coerce (dcName dc)) args)++ | aeqType hole typeNatKind+ = canGenDataKinds >>= \case+ True -> LitTy . NumTy . toInteger <$> Gen.word Range.linearBounded+ False -> error "genFreshMonoType: Cannot generate Nat without -XDataKinds"++ | aeqType hole typeSymbolKind+ = canGenDataKinds >>= \case+ True -> LitTy . SymTy <$> Gen.string (Range.linear 5 10) Gen.alphaNum+ False -> error "genFreshMonoType: Cannot generate Symbol without -XDataKinds"++ | aeqType hole liftedTypeKind+ = let gen = genMonoTypeFrom tcm env liftedTypeKind+ in Gen.subterm2 gen gen mkFunTy++ | otherwise+ = error ("genFreshMonoType: Cannot generate fit for hole: " <> showPpr hole)
+ src/Clash/Hedgehog/Core/Var.hs view
@@ -0,0 +1,94 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random generation of core variables.+-}++module Clash.Hedgehog.Core.Var+ ( genAttr'+ , genTyVar+ , genId+ , genLocalId+ , genGlobalId+ , genVars+ ) where++import Hedgehog (MonadGen, Range)+import qualified Hedgehog.Gen as Gen++import Clash.Core.Name (Name(nameUniq))+import Clash.Core.Term (TmName)+import Clash.Core.Type (Kind, KindOrType, TyName, Type)+import Clash.Core.Var (Attr'(..), Id, IdScope(..), TyVar, Var(..))+import Clash.Unique++import Clash.Hedgehog.Core.Name (genFreshName)++genAttr' :: forall m. MonadGen m => Range Int -> m Attr'+genAttr' range =+ Gen.choice+ [ BoolAttr' <$> genAlphaNum <*> Gen.bool+ , IntegerAttr' <$> genAlphaNum <*> genInteger+ , StringAttr' <$> genAlphaNum <*> genAlphaNum+ , Attr' <$> genAlphaNum+ ]+ where+ genAlphaNum = Gen.string range Gen.alphaNum+ genInteger = toInteger <$> Gen.integral range++-- | Generate a fresh type variable of the specified kind.+genTyVar :: forall m. MonadGen m => Kind -> m TyName -> m TyVar+genTyVar kn genName = do+ name <- genName+ pure (TyVar name (nameUniq name) kn)++-- | Generate a fresh identifier of the specified kind.+genId :: forall m. MonadGen m => Type -> m TmName -> m Id+genId ty genName = do+ name <- genName+ scope <- Gen.element [GlobalId, LocalId]+ pure (Id name (nameUniq name) ty scope)++-- | Generate a fresh local identifier of the specified kind.+genLocalId :: forall m. MonadGen m => Type -> m TmName -> m Id+genLocalId ty =+ fmap (\i -> i { idScope = LocalId }) . genId ty++-- | Generate a fresh global identifier of the specified kind.+genGlobalId :: forall m. MonadGen m => Type -> m TmName -> m Id+genGlobalId ty =+ fmap (\i -> i { idScope = GlobalId }) . genId ty++mapAccumLM+ :: forall m acc x y+ . Monad m+ => (acc -> x -> m (acc, y))+ -> acc+ -> [x]+ -> m (acc, [y])+mapAccumLM _ acc [] = return (acc, [])+mapAccumLM f acc (x:xs) = do+ (acc', y) <- f acc x+ (acc'', ys) <- mapAccumLM f acc' xs+ return (acc'', y:ys)++-- | Generate a collection of variables, from a supplied function to generate+-- variables and the kinds / types of variables to generate.+--+-- TODO While this gives "unique" vars because the uniques are different, it+-- can generate multiple vars with the same OccName.+genVars+ :: forall m a+ . MonadGen m+ => (KindOrType -> m (Name a) -> m (Var a))+ -> [KindOrType]+ -> m (Name a)+ -> m [Var a]+genVars genVar kts genName =+ snd <$> mapAccumLM go emptyUniqSet kts+ where+ go used kt = do+ var <- genVar kt (genFreshName used genName)+ pure (extendUniqSet used var, var)
+ src/Clash/Hedgehog/Internal/Bias.hs view
@@ -0,0 +1,66 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Bias for influencing generator choice.+-}++module Clash.Hedgehog.Internal.Bias+ ( Bias(..)+ ) where++import Clash.Core.Subst (aeqType)+import Clash.Core.TyCon+import Clash.Core.Type+import Clash.Core.TysPrim++-- | Determine the bias of an item. This is used to set the weight of that item+-- so we can sample using the 'Hedgehog.Gen.frequency' generator instead of+-- 'Hedgehog.Gen.element' or 'Hedgehog.Gen.choice'.+--+-- Where might you want to introduce such a bias? If there is a collection of+-- elements where there is a likeliness that real code would use certain values+-- more or less, we want to be able to capture this. An obvious example of this+-- is the @TyConMap@, where without it every constructor would have an even+-- weighting, when in reality some (like @Void#@ or @Addr#@ are much less+-- likely to appear in code written by a Clash user).+--+class Bias a where+ biasOf :: a -> Int++-- Remember, the bias we pick here does not necessarily matter. Only+-- constructors with the correct shape will ever be considered.+--+-- TODO These biases are only very loosely based in reality, and could be+-- completely useless at generating the kinds / types we want to see.+instance Bias TyCon where+ biasOf tc@PrimTyCon{}+ | aeqType ty liftedTypeKind = biasBy 3 -- Type+ | aeqType ty typeNatKind = biasBy 2 -- Nat+ | aeqType ty typeSymbolKind = biasBy 1 -- Symbol++ | aeqType ty integerPrimTy = biasBy 5 -- Integer, Natural, Int#, Word#+ | aeqType ty naturalPrimTy = biasBy 5+ | aeqType ty intPrimTy = biasBy 5+ | aeqType ty wordPrimTy = biasBy 5+ | aeqType ty int64PrimTy = biasBy 4 -- Int64#, Word64#+ | aeqType ty word64PrimTy = biasBy 4+ | aeqType ty floatPrimTy = biasBy 3 -- Float#, Double#+ | aeqType ty doublePrimTy = biasBy 3+ | aeqType ty charPrimTy = biasBy 2 -- Char#, ByteArray#, Addr#+ | aeqType ty byteArrayPrimTy = biasBy 2+ | aeqType ty stringPrimTy = biasBy 2+ | aeqType ty voidPrimTy = biasBy 1 -- Void#++ | otherwise = baseBias -- Anything else is base+ where+ baseBias = 10+ ty = mkTyConTy (tyConName tc)++ biasBy :: Int -> Int+ biasBy n = baseBias ^ n++ biasOf AlgTyCon{} = 20 ^ (4 :: Int)+ biasOf PromotedDataCon{} = 20 ^ (3 :: Int)+ biasOf FunTyCon{} = 20 ^ (3 :: Int)
+ src/Clash/Hedgehog/Unique.hs view
@@ -0,0 +1,123 @@+{-|+Copyright : (C) 2021, QBayLogic B.V.+License : BSD2 (see the file LICENSE)+Maintainer : QBayLogic B.V. <devops@qbaylogic.com>++Random generation of unique variables and unique containers.+-}++{-# LANGUAGE TupleSections #-}++module Clash.Hedgehog.Unique+ ( genUnique+ , genUniqMap+ , sampleUniqMap+ , sampleAnyUniqMap+ , genUniqSet+ , Bias(..)+ , sampleUniqMapBiased+ ) where++import Control.Applicative (Alternative(empty))+import Data.Either (rights)+import Hedgehog (MonadGen, Range)+import qualified Hedgehog.Gen as Gen+import qualified Hedgehog.Range as Range++import Clash.Core.HasType+import Clash.Core.Subst (aeqType)+import Clash.Core.Type+import Clash.Unique++import Clash.Hedgehog.Internal.Bias++genUnique :: forall m. MonadGen m => m Unique+genUnique = Gen.int Range.linearBounded++genUniqMap+ :: forall m k v+ . (MonadGen m, Uniquable k)+ => Range Int+ -> m k+ -> m v+ -> m (UniqMap v)+genUniqMap range genKey genValue =+ listToUniqMap <$> Gen.list range ((,) <$> genKey <*> genValue)++sampleAnyUniqMap+ :: forall m v+ . (Alternative m, MonadGen m, HasType v)+ => UniqMap v+ -> m (v, [Type])+sampleAnyUniqMap xs =+ let xs' = filterUniqMap (not . isPolyTy . coreTypeOf) xs+ in if nullUniqMap xs' then empty else do+ x <- Gen.element (eltsUniqMap xs')+ let holes = rights . fst $ splitFunForallTy (coreTypeOf x)++ pure (x, holes)++sampleUniqMap+ :: forall m v+ . (Alternative m, MonadGen m, HasType v)+ => (v -> Bool)+ -> Type+ -> UniqMap v+ -> m (v, [Type])+sampleUniqMap p hole xs =+ let xs' = mapMaybeUniqMap findFit (filterUniqMap p xs)+ in if nullUniqMap xs' then empty else Gen.element (eltsUniqMap xs')+ where+ findFit x =+ fmap (x,) (findFitArgs (coreTypeOf x))++ -- NOTE [finding more complex fits]+ -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+ -- This is not good enough. If I have a hole of type A -> B and I have+ -- a candidate of type forall a. a -> B, I will give up because it is not+ -- alpha equalivalent or a function type. I could return [Either TyVar Type]+ -- and include foralls, but this would still not fit polymorphic holes. For+ -- example, if I have the hole A -> B, and the candidate forall a. a -> B, it+ -- would:+ --+ -- 1. not aeq to hole, add Left a to params+ -- 2. not aeq to hole, add Right a to params+ -- 3. not aeq to hole, discard+ --+ -- The correct approach to take here is to figure out which arguments need+ -- to be provided such that the hole and the type of the candidate can be+ -- unified. However, unification is (1) not provided by clash-lib currently+ -- and (2) very non-trivial to implement given we have -XTypeFamilies.+ findFitArgs a+ | aeqType hole a = Just []+ | FunTy b c <- tyView a = fmap (b :) (findFitArgs c)+ | otherwise = Nothing++sampleUniqMapBiased+ :: forall m v+ . (Alternative m, MonadGen m, HasType v, Bias v)+ => (v -> Bool)+ -> Type+ -> UniqMap v+ -> m (v, [Type])+sampleUniqMapBiased p hole xs =+ let xs' = eltsUniqMap $ mapMaybeUniqMap findFit (filterUniqMap p xs)+ bs = fmap (biasOf . fst) xs'+ in if null xs' then empty else Gen.frequency (zip bs (Gen.constant <$> xs'))+ where+ findFit x =+ fmap (x,) (findFitArgs (coreTypeOf x))++ findFitArgs a+ | aeqType hole a = Just []+ | FunTy b c <- tyView a = fmap (b :) (findFitArgs c)+ | otherwise = Nothing++genUniqSet+ :: forall m v+ . (MonadGen m, Uniquable v)+ => Range Int+ -> m v+ -> m (UniqSet v)+genUniqSet range genValue =+ mkUniqSet <$> Gen.list range genValue