diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/clash-lib-hedgehog.cabal b/clash-lib-hedgehog.cabal new file mode 100644 --- /dev/null +++ b/clash-lib-hedgehog.cabal @@ -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, diff --git a/src/Clash/Hedgehog/Core/DataCon.hs b/src/Clash/Hedgehog/Core/DataCon.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/DataCon.hs @@ -0,0 +1,210 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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) diff --git a/src/Clash/Hedgehog/Core/Literal.hs b/src/Clash/Hedgehog/Core/Literal.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Literal.hs @@ -0,0 +1,110 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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)) diff --git a/src/Clash/Hedgehog/Core/Monad.hs b/src/Clash/Hedgehog/Core/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Monad.hs @@ -0,0 +1,103 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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 diff --git a/src/Clash/Hedgehog/Core/Name.hs b/src/Clash/Hedgehog/Core/Name.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Name.hs @@ -0,0 +1,113 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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) diff --git a/src/Clash/Hedgehog/Core/Term.hs b/src/Clash/Hedgehog/Core/Term.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Term.hs @@ -0,0 +1,358 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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] diff --git a/src/Clash/Hedgehog/Core/TyCon.hs b/src/Clash/Hedgehog/Core/TyCon.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/TyCon.hs @@ -0,0 +1,305 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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. +-} diff --git a/src/Clash/Hedgehog/Core/Type.hs b/src/Clash/Hedgehog/Core/Type.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Type.hs @@ -0,0 +1,539 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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) diff --git a/src/Clash/Hedgehog/Core/Var.hs b/src/Clash/Hedgehog/Core/Var.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Core/Var.hs @@ -0,0 +1,94 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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) diff --git a/src/Clash/Hedgehog/Internal/Bias.hs b/src/Clash/Hedgehog/Internal/Bias.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Internal/Bias.hs @@ -0,0 +1,66 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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) diff --git a/src/Clash/Hedgehog/Unique.hs b/src/Clash/Hedgehog/Unique.hs new file mode 100644 --- /dev/null +++ b/src/Clash/Hedgehog/Unique.hs @@ -0,0 +1,123 @@ +{-| +Copyright : (C) 2021, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : QBayLogic B.V. + +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