Skip to content

Commit

Permalink
add genHint for maps
Browse files Browse the repository at this point in the history
  • Loading branch information
MaximilianAlgehed committed Apr 25, 2024
1 parent 3c3a5f1 commit d24ef53
Show file tree
Hide file tree
Showing 6 changed files with 49 additions and 26 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,7 @@ import Cardano.Ledger.UTxO
import Cardano.Ledger.Val (Val)
import Constrained hiding (Value)
import Constrained qualified as C
import Constrained.Spec.Map
import Control.Monad.Trans.Fail.String
import Crypto.Hash (Blake2b_224)
import Data.ByteString qualified as BS
Expand Down Expand Up @@ -730,10 +731,12 @@ instance IsConwayUniv fn => HasSpec fn Network

instance HasSimpleRep (MultiAsset c)
instance (IsConwayUniv fn, Crypto c) => HasSpec fn (MultiAsset c) where
emptySpec = flip (MapSpec mempty [] mempty) NoFold $
constrained' $ \_ innerMap ->
forAll innerMap $ \kv' ->
lit 0 <=. snd_ kv'
emptySpec =
defaultMapSpec
{ mapSpecElem = constrained' $ \_ innerMap ->
forAll innerMap $ \kv' ->
lit 0 <=. snd_ kv'
}

instance HasSimpleRep AssetName where
type SimpleRep AssetName = ShortByteString
Expand Down
2 changes: 1 addition & 1 deletion libs/constrained-generators/constrained-generators.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ library
Constrained.Graph
Constrained.Spec.Generics
Constrained.Spec.Pairs
Constrained.Spec.Maps
Constrained.Spec.Map
Constrained.Spec.Tree
Constrained.Internals
Constrained.Examples
Expand Down
4 changes: 4 additions & 0 deletions libs/constrained-generators/src/Constrained/Examples/Map.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,3 +57,7 @@ fixedRange = constrained $ \m ->
[ forAll (rng_ m) (\x -> x ==. 5)
, assert $ (sizeOf_ m) ==. 1
]

rangeHint :: Specification BaseFn (Map Int Int)
rangeHint = constrained $ \m ->
genHint 10 (rng_ m)
2 changes: 1 addition & 1 deletion libs/constrained-generators/src/Constrained/Spec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module Constrained.Spec (
import Constrained.Base as X
import Constrained.Instances ()
import Constrained.Spec.Generics as X
import Constrained.Spec.Maps as X
import Constrained.Spec.Map as X
import Constrained.Spec.Pairs as X
import Constrained.Spec.Tree as X
import Constrained.Univ ()
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Constrained.Spec.Maps (MapSpec (..), dom_, rng_) where
module Constrained.Spec.Map (MapSpec (..), defaultMapSpec, dom_, rng_) where

import Constrained.Base
import Constrained.Core
Expand All @@ -36,21 +36,25 @@ import Test.QuickCheck (shrinkList)

instance Ord a => Sized (Map.Map a b) where
sizeOf = toInteger . Map.size
liftSizeSpec sz = TypeSpec (MapSpec mempty mempty (typeSpec sz) TrueSpec NoFold) []
liftMemberSpec xs = typeSpec (MapSpec mempty mempty (MemberSpec xs) TrueSpec NoFold)
sizeOfTypeSpec (MapSpec mustk mustv size _ _) =
liftSizeSpec sz = typeSpec $ defaultMapSpec {mapSpecSize = typeSpec sz}
liftMemberSpec xs = typeSpec $ defaultMapSpec {mapSpecSize = MemberSpec xs}
sizeOfTypeSpec (MapSpec _ mustk mustv size _ _) =
typeSpec (atLeastSize (sizeOf mustk))
<> typeSpec (atLeastSize (sizeOf mustv))
<> size

data MapSpec fn k v = MapSpec
{ mapSpecMustKeys :: Set k
{ mapSpecHint :: Maybe Integer
, mapSpecMustKeys :: Set k
, mapSpecMustValues :: [v]
, mapSpecSize :: Specification fn Integer
, mapSpecElem :: Specification fn (k, v)
, mapSpecFold :: FoldSpec fn v
}

defaultMapSpec :: Ord k => MapSpec fn k v
defaultMapSpec = MapSpec Nothing mempty mempty TrueSpec TrueSpec NoFold

deriving instance
( HasSpec fn (k, v)
, HasSpec fn k
Expand All @@ -59,7 +63,7 @@ deriving instance
) =>
Show (MapSpec fn k v)
instance Ord k => Forallable (Map k v) (k, v) where
forAllSpec kvs = typeSpec $ MapSpec mempty [] TrueSpec kvs NoFold
forAllSpec kvs = typeSpec $ defaultMapSpec {mapSpecElem = kvs}
forAllToList = Map.toList

instance
Expand All @@ -69,20 +73,21 @@ instance
type TypeSpec fn (Map k v) = MapSpec fn k v
type Prerequisites fn (Map k v) = (HasSpec fn k, HasSpec fn v)

emptySpec = MapSpec mempty mempty mempty mempty NoFold
emptySpec = defaultMapSpec

combineSpec
(MapSpec mustKeys mustVals size kvs foldSpec)
(MapSpec mustKeys' mustVals' size' kvs' foldSpec') = fromGE ErrorSpec $ do
(MapSpec mHint mustKeys mustVals size kvs foldSpec)
(MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = fromGE ErrorSpec $ do
typeSpec
. MapSpec
(unionWithMaybe min mHint mHint')
(mustKeys <> mustKeys')
(nub $ mustVals <> mustVals')
(size <> size')
(kvs <> kvs')
<$> combineFoldSpec foldSpec foldSpec'

conformsTo m (MapSpec mustKeys mustVals size kvs foldSpec) =
conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec) =
and
[ mustKeys `Set.isSubsetOf` Map.keysSet m
, all (`elem` Map.elems m) mustVals
Expand All @@ -91,7 +96,7 @@ instance
, Map.elems m `conformsToFoldSpec` foldSpec
]

genFromTypeSpec (MapSpec mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do
genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do
mustMap <- explain ["Make the mustMap"] $ forM (Set.toList mustKeys) $ \k -> do
let vSpec = constrained $ \v -> satisfies (pair_ (lit k) v) kvs
v <- explain [show $ "vSpec =" <+> pretty vSpec] $ genFromSpec vSpec
Expand All @@ -102,7 +107,7 @@ instance
-- TODO, we should make sure size' is greater than or equal to 0
satisfies
(sz + Lit (sizeOf mustMap))
(size <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
(maybe TrueSpec leqSpec mHint <> size <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
foldSpec' = case foldSpec of
NoFold -> NoFold
FoldSpec fn sumSpec -> FoldSpec fn $ propagateSpecFun (theAddFn @fn) (HOLE :? Value mustSum :> Nil) sumSpec
Expand Down Expand Up @@ -135,18 +140,26 @@ instance
go (Map.insert k v m) restVals'
go (Map.fromList mustMap) restVals

shrinkWithTypeSpec (MapSpec _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)
shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)

toPreds m (MapSpec mustKeys mustVals size kvs foldSpec) =
toPreds m (MapSpec mHint mustKeys mustVals size kvs foldSpec) =
toPred
[ assert $ lit mustKeys `subset_` dom_ m
, forAll (Lit mustVals) $ \val ->
val `elem_` rng_ m
, sizeOf_ (rng_ m) `satisfies` size
, forAll m $ \kv -> satisfies kv kvs
, toPredsFoldSpec (rng_ m) foldSpec
, maybe TruePred (`genHint` m) mHint
]

instance
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
HasGenHint fn (Map k v)
where
type Hint (Map k v) = Integer
giveHint h = typeSpec $ defaultMapSpec {mapSpecHint = Just h}

------------------------------------------------------------------------
-- Functions
------------------------------------------------------------------------
Expand All @@ -170,10 +183,11 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
case spec of
MemberSpec [s] ->
typeSpec $
MapSpec s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold
MapSpec Nothing s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold
TypeSpec (SetSpec must elemspec size) [] ->
typeSpec $
MapSpec
Nothing
must
[]
size
Expand All @@ -188,10 +202,11 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
, Evidence <- prerequisites @fn @(Map k v) ->
case spec of
MemberSpec [r] ->
typeSpec $ MapSpec Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold
TypeSpec (ListSpec Nothing must size elemspec foldspec) [] ->
typeSpec $ MapSpec Nothing Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold
TypeSpec (ListSpec listHint must size elemspec foldspec) [] ->
typeSpec $
MapSpec
listHint
Set.empty
must
size
Expand All @@ -207,14 +222,14 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
-- No TypeAbstractions in ghc-8.10
case f of
(_ :: MapFn fn '[Map k v] (Set k))
| MapSpec mustSet _ sz kvSpec _ <- ts
| MapSpec _ mustSet _ sz kvSpec _ <- ts
, Evidence <- prerequisites @fn @(Map k v) ->
typeSpec $ SetSpec mustSet (mapSpec (fstFn @fn) $ toSimpleRepSpec kvSpec) sz
Rng ->
-- No TypeAbstractions in ghc-8.10
case f of
(_ :: MapFn fn '[Map k v] [v])
| MapSpec _ mustList sz kvSpec foldSpec <- ts
| MapSpec _ _ mustList sz kvSpec foldSpec <- ts
, Evidence <- prerequisites @fn @(Map k v) ->
typeSpec $ ListSpec Nothing mustList sz (mapSpec (sndFn @fn) $ toSimpleRepSpec kvSpec) foldSpec

Expand Down
3 changes: 2 additions & 1 deletion libs/constrained-generators/test/Constrained/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,8 @@ tests =
testSpec "existsUnfree" existsUnfree
-- TODO: double shrinking
testSpecNoShrink "reifyYucky" reifyYucky
testSpec "fixedRangeElements" fixedRange
testSpec "fixedRange" fixedRange
testSpec "rangeHint" rangeHint
numberyTests
sizeTests
numNumSpecTree
Expand Down

0 comments on commit d24ef53

Please sign in to comment.