input-output-hk / constrained-generators / 414

Committed 21 Nov 2025 07:55AM UTC coverage: 76.458% (-0.8%) from 77.228%

Build # 414

Build Type

push

github

Committed by

web-flow

Commit Message

Speed up generation by threading seeds instead of splitting them in non-`Gen` part of `GenT` (#57)

Run Details

33 of 44 new or added lines in 1 file covered. (75.0%)

58 existing lines in 7 files now uncovered.

3907 of 5110 relevant lines covered (76.46%)

1.44 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

68.84

/src/Constrained/Spec/Map.hs

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | `HasSpec` instance for `Map` and functions for working with `Map`s
module Constrained.Spec.Map (
  MapSpec (..),
  defaultMapSpec,
  MapW (..),
  lookup_,
  mapMember_,
  dom_,
  rng_,
) where

import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generation
import Constrained.Generic (Prod (..))
import Constrained.List
import Constrained.NumOrd (cardinality, geqSpec, leqSpec, nubOrd)
import Constrained.PrettyUtils
import Constrained.Spec.List
import Constrained.Spec.Set
import Constrained.Spec.SumProd
import Constrained.Syntax
import Constrained.TheKnot
import Control.Monad
import Data.Foldable
import Data.Kind
import Data.List (nub)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics
import Prettyprinter
import Test.QuickCheck hiding (Fun, Witness, forAll)

------------------------------------------------------------------------
-- HasSpec
------------------------------------------------------------------------

instance Ord a => Sized (Map.Map a b) where
  sizeOf = toInteger . Map.size
  liftSizeSpec sz cant = typeSpec $ defaultMapSpec {mapSpecSize = TypeSpec sz cant}
  liftMemberSpec xs = case NE.nonEmpty (nubOrd xs) of
    Nothing -> ErrorSpec (pure "In liftMemberSpec for the (Sized Map) instance, xs is the empty list")
    Just ys -> typeSpec $ defaultMapSpec {mapSpecSize = MemberSpec ys}
  sizeOfTypeSpec (MapSpec _ mustk mustv size _ _) =
    geqSpec (sizeOf mustk)
      <> geqSpec (sizeOf mustv)
      <> size

-- | Custom `TypeSpec` for `Map`
data MapSpec k v = MapSpec
  { mapSpecHint :: Maybe Integer
  , mapSpecMustKeys :: Set k
  , mapSpecMustValues :: [v]
  , mapSpecSize :: Specification Integer
  , mapSpecElem :: Specification (k, v)
  , mapSpecFold :: FoldSpec v
  }
  deriving (Generic)

-- | emptySpec without all the constraints
defaultMapSpec :: Ord k => MapSpec k v
defaultMapSpec = MapSpec Nothing mempty mempty TrueSpec TrueSpec NoFold

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Pretty (WithPrec (MapSpec k v))
  where
  pretty (WithPrec d s) =
    parensIf (d > 10) $
      "MapSpec"
        /> vsep
          [ "hint       =" <+> viaShow (mapSpecHint s)
          , "mustKeys   =" <+> viaShow (mapSpecMustKeys s)
          , "mustValues =" <+> viaShow (mapSpecMustValues s)
          , "size       =" <+> pretty (mapSpecSize s)
          , "elem       =" <+> pretty (mapSpecElem s)
          , "fold       =" <+> pretty (mapSpecFold s)
          ]

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Show (MapSpec k v)
  where
  showsPrec d = shows . prettyPrec d

instance Ord k => Forallable (Map k v) (k, v) where
  fromForAllSpec kvs = typeSpec $ defaultMapSpec {mapSpecElem = kvs}
  forAllToList = Map.toList

-- ============================================================
-- We will need to take projections on (Specification (a,b))

fstSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification k
fstSpec s = mapSpec ProdFstW (mapSpec ToGenericW s)

sndSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification v
sndSpec s = mapSpec ProdSndW (mapSpec ToGenericW s)

-- ======================================================================
-- The HasSpec instance for Maps

instance
  (Ord k, HasSpec (Prod k v), HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasSpec (Map k v)
  where
  type TypeSpec (Map k v) = MapSpec k v
  type Prerequisites (Map k v) = (HasSpec k, HasSpec v)

  emptySpec = defaultMapSpec

  combineSpec
    (MapSpec mHint mustKeys mustVals size kvs foldSpec)
    (MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = case combineFoldSpec foldSpec foldSpec' of
      Left msgs ->
        ErrorSpec $
          NE.fromList $
            [ "Error in combining FoldSpec in combineSpec for Map"
            , "  " ++ show foldSpec
            , "  " ++ show foldSpec'
            ]
              ++ msgs
      Right foldSpec'' ->
        typeSpec $
          MapSpec
            -- This is min because that allows more compositionality - if a spec specifies a
            -- low upper bound because some part of the spec will be slow it doesn't make sense
            -- to increase it somewhere else because that part isn't slow.
            (unionWithMaybe min mHint mHint')
            (mustKeys <> mustKeys')
            (nub $ mustVals <> mustVals')
            (size <> size')
            (kvs <> kvs')
            foldSpec''

  conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec) =
    and
      [ mustKeys `Set.isSubsetOf` Map.keysSet m
      , all (`elem` Map.elems m) mustVals
      , sizeOf m `conformsToSpec` size
      , all (`conformsToSpec` kvs) (Map.toList m)
      , Map.elems m `conformsToFoldSpec` foldSpec
      ]

  genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) NoFold)
    | null mustKeys
    , null mustVals = do
        let size' =
              fold
                [ maybe TrueSpec (leqSpec . max 0) mHint
                , size
                , maxSpec (cardinality (fstSpec kvs))
                , maxSpec (cardinalTrueSpec @k)
                , geqSpec 0
                ]
        n <- genFromSpecT size'
        let go sz 0 slow kvs' m
              | fromInteger sz == Map.size m = pure m
              | not slow = go sz (sz - fromIntegral (Map.size m)) True (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty)) m
              | otherwise = fatalError "The impossible happened"
            go sz n' slow kvs' m = do
              mkv <- inspect $ genFromSpecT kvs'
              case mkv of
                Result (k, v) ->
                  go
                    sz
                    (n' - 1)
                    slow
                    (kvs' <> if slow then typeSpec (Cartesian (notEqualSpec k) mempty) else mempty)
                    (Map.insert k v m)
                GenError msgs ->
                  if sizeOf m `conformsToSpec` size
                    then pure m
                    else
                      genErrorNE
                        (pure "Gen error while trying to generate enough elements for a Map." <> catMessageList msgs)
                FatalError msgs ->
                  genErrorNE
                    ( NE.fromList
                        [ "Fatal error while trying to generate enough elements for a map:"
                        , "  The ones we have generated so far = " ++ show m
                        , "  The number we need to still generate: n' = " ++ show n'
                        , "The original size spec " ++ show size
                        , "The refined  size spec " ++ show size'
                        , "The computed target size " ++ show n
                        , "Fatal error messages"
                        , "<<<---"
                        ]
                        <> catMessageList msgs
                        <> (pure "--->>>")
                    )
        explain ("  The number we are trying for: n = " ++ show n) $ go n n False kvs mempty
  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) $ genFromSpecT vSpec
      pure (k, v)
    let haveVals = map snd mustMap
        mustVals' = filter (`notElem` haveVals) mustVals
        size' = simplifySpec $ constrained $ \sz ->
          -- TODO, we should make sure size' is greater than or equal to 0
          satisfies
            (sz + Lit (sizeOf mustMap))
            ( maybe TrueSpec (leqSpec . max 0) mHint
                <> size
                <> maxSpec (cardinality (fstSpec kvs)) -- (mapSpec FstW $ mapSpec ToGenericW kvs))
                <> maxSpec (cardinalTrueSpec @k)
            )
        !foldSpec' = case foldSpec of
          NoFold -> NoFold
          FoldSpec fn@(Fun symbol) sumSpec -> FoldSpec fn $ propagate theAddFn (HOLE :? Value mustSum :> Nil) sumSpec
            where
              mustSum = adds (map (semantics symbol) haveVals)
    let !valsSpec =
          ListSpec
            Nothing
            mustVals'
            size'
            (simplifySpec $ constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs)
            foldSpec'

    !restVals <-
      explainNE
        ( NE.fromList
            [ "Make the restVals"
            , show $ "  valsSpec =" <+> pretty valsSpec
            , show $ "  mustMap =" <+> viaShow mustMap
            , show $ "  size' =" <+> pretty size'
            ]
        )
        $ genFromTypeSpec
        $ valsSpec
    let go m [] = pure m
        go m (v : restVals') = do
          let keySpec = notMemberSpec (Map.keysSet m) <> constrained (\k -> pair_ k (Lit v) `satisfies` kvs)
          k <-
            explainNE
              ( NE.fromList
                  [ "Make a key"
                  , show $ indent 4 $ "keySpec =" <+> pretty keySpec
                  ]
              )
              $ genFromSpecT keySpec
          go (Map.insert k v m) restVals'

    go (Map.fromList mustMap) restVals

  cardinalTypeSpec _ = TrueSpec

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

  fixupWithTypeSpec _ _ = Nothing

  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 k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasGenHint (Map k v)
  where
  type Hint (Map k v) = Integer
  giveHint h = typeSpec $ defaultMapSpec {mapSpecHint = Just h}

------------------------------------------------------------------------
-- Logic instances for
------------------------------------------------------------------------

-- | Function symbols for talking about maps
data MapW (dom :: [Type]) (rng :: Type) where
  DomW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] (Set k)
  RngW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] [v]
  LookupW ::
    (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[k, Map k v] (Maybe v)

deriving instance Eq (MapW dom rng)

instance Semantics MapW where
  semantics DomW = Map.keysSet
  semantics RngW = Map.elems
  semantics LookupW = Map.lookup

instance Syntax MapW

instance Show (MapW d r) where
  show DomW = "dom_"
  show RngW = "rng_"
  show LookupW = "lookup_"

instance Logic MapW where
  propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s
  propagate _ _ TrueSpec = TrueSpec
  propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs
  propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)
  propagate DomW (Unary HOLE) spec =
    case spec of
      MemberSpec (s :| []) ->
        typeSpec $
          MapSpec Nothing s [] (equalSpec $ sizeOf s) TrueSpec NoFold
      TypeSpec (SetSpec must elemspec size) [] ->
        typeSpec $
          MapSpec
            Nothing
            must
            []
            size
            (constrained $ \kv -> satisfies (fst_ kv) elemspec)
            NoFold
      _ -> ErrorSpec (NE.fromList ["Dom on bad map spec", show spec])
  propagate RngW (Unary HOLE) spec =
    case spec of
      TypeSpec (ListSpec listHint must size elemspec foldspec) [] ->
        typeSpec $
          MapSpec
            listHint
            Set.empty
            must
            size
            (constrained $ \kv -> satisfies (snd_ kv) elemspec)
            foldspec
      -- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that
      -- requires not only that the elements of the map are fixed to what is in `r`,
      -- but they appear in the order that they are in `r`. That's
      -- very difficult to achieve!
      _ -> ErrorSpec (NE.fromList ["Rng on bad map spec", show spec])
  propagate LookupW (Value k :! Unary HOLE) spec =
    constrained $ \m ->
      [Assert $ Lit k `member_` dom_ m | not $ Nothing `conformsToSpec` spec]
        ++ [ forAll m $ \kv ->
               letBind (fst_ kv) $ \k' ->
                 letBind (snd_ kv) $ \v ->
                   whenTrue (Lit k ==. k') $
                     -- TODO: What you want to write is `just_ v `satisfies` spec` but we can't
                     -- do that because we don't have access to `IsNormalType v` here. When
                     -- we refactor the `IsNormalType` machinery we will be able to make
                     -- this nicer.
                     case spec of
                       MemberSpec as -> Assert $ v `elem_` Lit [a | Just a <- NE.toList as]
                       TypeSpec (SumSpec _ _ vspec) cant ->
                         v `satisfies` (vspec <> notMemberSpec [a | Just a <- cant])
           ]
  propagate LookupW (HOLE :? Value m :> Nil) spec =
    if Nothing `conformsToSpec` spec
      then notMemberSpec [k | (k, v) <- Map.toList m, not $ Just v `conformsToSpec` spec]
      else
        memberSpec
          (Map.keys $ Map.filter ((`conformsToSpec` spec) . Just) m)
          ( NE.fromList
              [ "propagate (lookup HOLE ms) on (MemberSpec ms)"
              , "forall pairs (d,r) in ms, no 'd' conforms to spec"
              , "  " ++ show spec
              ]
          )

  mapTypeSpec DomW (MapSpec _ mustSet _ sz kvSpec _) = typeSpec $ SetSpec mustSet (fstSpec kvSpec) sz
  mapTypeSpec RngW (MapSpec _ _ mustList sz kvSpec foldSpec) = typeSpec $ ListSpec Nothing mustList sz (sndSpec kvSpec) foldSpec

------------------------------------------------------------------------
-- Syntax
------------------------------------------------------------------------

-- | Take the domain of a `Map` as a `Set`
dom_ ::
  (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term (Set k)
dom_ = appTerm DomW

-- | Take the range of a `Map` as a list
rng_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term [v]
rng_ = appTerm RngW

-- | Lookup a key in the `Map`
lookup_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term k ->
  Term (Map k v) ->
  Term (Maybe v)
lookup_ = appTerm LookupW

-- | Check if a key is a member of the map
mapMember_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term k ->
  Term (Map k v) ->
  Term Bool
mapMember_ k m = not_ $ lookup_ k m ==. lit Nothing

1	{-# LANGUAGE BangPatterns #-}
2	{-# LANGUAGE DataKinds #-}
3	{-# LANGUAGE DeriveGeneric #-}
4	{-# LANGUAGE FlexibleContexts #-}
5	{-# LANGUAGE FlexibleInstances #-}
6	{-# LANGUAGE GADTs #-}
7	{-# LANGUAGE MultiParamTypeClasses #-}
8	{-# LANGUAGE OverloadedStrings #-}
9	{-# LANGUAGE ScopedTypeVariables #-}
10	{-# LANGUAGE StandaloneDeriving #-}
11	{-# LANGUAGE TypeApplications #-}
12	{-# LANGUAGE TypeFamilies #-}
13	{-# LANGUAGE UndecidableInstances #-}
14	{-# LANGUAGE ViewPatterns #-}
15	{-# OPTIONS_GHC -Wno-orphans #-}
16
17	-- \| `HasSpec` instance for `Map` and functions for working with `Map`s
18	module Constrained.Spec.Map (
19	MapSpec (..),
20	defaultMapSpec,
21	MapW (..),
22	lookup_,
23	mapMember_,
24	dom_,
25	rng_,
26	) where
27
28	import Constrained.AbstractSyntax
29	import Constrained.Base
30	import Constrained.Conformance
31	import Constrained.Core
32	import Constrained.FunctionSymbol
33	import Constrained.GenT
34	import Constrained.Generation
35	import Constrained.Generic (Prod (..))
36	import Constrained.List
37	import Constrained.NumOrd (cardinality, geqSpec, leqSpec, nubOrd)
38	import Constrained.PrettyUtils
39	import Constrained.Spec.List
40	import Constrained.Spec.Set
41	import Constrained.Spec.SumProd
42	import Constrained.Syntax
43	import Constrained.TheKnot
44	import Control.Monad
45	import Data.Foldable
46	import Data.Kind
47	import Data.List (nub)
48	import qualified Data.List.NonEmpty as NE
49	import Data.Map (Map)
50	import qualified Data.Map as Map
51	import Data.Set (Set)
52	import qualified Data.Set as Set
53	import GHC.Generics
54	import Prettyprinter
55	import Test.QuickCheck hiding (Fun, Witness, forAll)
56
57	------------------------------------------------------------------------
58	-- HasSpec
59	------------------------------------------------------------------------
60
61	instance Ord a => Sized (Map.Map a b) where
62	sizeOf = toInteger . Map.size	2✔
63	liftSizeSpec sz cant = typeSpec $ defaultMapSpec {mapSpecSize = TypeSpec sz cant}	2✔
64	liftMemberSpec xs = case NE.nonEmpty (nubOrd xs) of	2✔
65	Nothing -> ErrorSpec (pure "In liftMemberSpec for the (Sized Map) instance, xs is the empty list")	×
66	Just ys -> typeSpec $ defaultMapSpec {mapSpecSize = MemberSpec ys}	2✔
67	sizeOfTypeSpec (MapSpec _ mustk mustv size _ _) =	×
68	geqSpec (sizeOf mustk)	×
69	<> geqSpec (sizeOf mustv)	×
70	<> size	×
71
72	-- \| Custom `TypeSpec` for `Map`
73	data MapSpec k v = MapSpec
74	{ mapSpecHint :: Maybe Integer	×
75	, mapSpecMustKeys :: Set k	×
76	, mapSpecMustValues :: [v]	×
77	, mapSpecSize :: Specification Integer	×
78	, mapSpecElem :: Specification (k, v)	×
79	, mapSpecFold :: FoldSpec v	×
80	}
81	deriving (Generic)	×
82
83	-- \| emptySpec without all the constraints
84	defaultMapSpec :: Ord k => MapSpec k v
85	defaultMapSpec = MapSpec Nothing mempty mempty TrueSpec TrueSpec NoFold	2✔
86
87	instance
88	( HasSpec (k, v)	×
89	, HasSpec k
90	, HasSpec v
91	, HasSpec [v]
92	) =>
93	Pretty (WithPrec (MapSpec k v))
94	where
95	pretty (WithPrec d s) =	×
96	parensIf (d > 10) $	×
97	"MapSpec"	×
98	/> vsep	×
99	[ "hint =" <+> viaShow (mapSpecHint s)	×
100	, "mustKeys =" <+> viaShow (mapSpecMustKeys s)	×
101	, "mustValues =" <+> viaShow (mapSpecMustValues s)	×
102	, "size =" <+> pretty (mapSpecSize s)	×
103	, "elem =" <+> pretty (mapSpecElem s)	×
104	, "fold =" <+> pretty (mapSpecFold s)	×
105	]
106
107	instance
108	( HasSpec (k, v)	×
109	, HasSpec k
110	, HasSpec v
111	, HasSpec [v]
112	) =>
113	Show (MapSpec k v)
114	where
115	showsPrec d = shows . prettyPrec d	×
116
117	instance Ord k => Forallable (Map k v) (k, v) where
118	fromForAllSpec kvs = typeSpec $ defaultMapSpec {mapSpecElem = kvs}	2✔
119	forAllToList = Map.toList	2✔
120
121	-- ============================================================
122	-- We will need to take projections on (Specification (a,b))
123
124	fstSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification k
125	fstSpec s = mapSpec ProdFstW (mapSpec ToGenericW s)	2✔
126
127	sndSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification v
128	sndSpec s = mapSpec ProdSndW (mapSpec ToGenericW s)	×
129
130	-- ======================================================================
131	-- The HasSpec instance for Maps
132
133	instance
134	(Ord k, HasSpec (Prod k v), HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>	×
135	HasSpec (Map k v)
136	where
137	type TypeSpec (Map k v) = MapSpec k v
138	type Prerequisites (Map k v) = (HasSpec k, HasSpec v)
139
140	emptySpec = defaultMapSpec	2✔
141
142	combineSpec	2✔
143	(MapSpec mHint mustKeys mustVals size kvs foldSpec)
144	(MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = case combineFoldSpec foldSpec foldSpec' of	2✔
145	Left msgs ->
146	ErrorSpec $	×
147	NE.fromList $	×
148	[ "Error in combining FoldSpec in combineSpec for Map"	×
149	, " " ++ show foldSpec	×
150	, " " ++ show foldSpec'	×
151	]
152	++ msgs	×
153	Right foldSpec'' ->
154	typeSpec $	2✔
155	MapSpec	2✔
156	-- This is min because that allows more compositionality - if a spec specifies a
157	-- low upper bound because some part of the spec will be slow it doesn't make sense
158	-- to increase it somewhere else because that part isn't slow.
159	(unionWithMaybe min mHint mHint')	2✔
160	(mustKeys <> mustKeys')	2✔
161	(nub $ mustVals <> mustVals')	2✔
162	(size <> size')	2✔
163	(kvs <> kvs')	2✔
164	foldSpec''	2✔
165
166	conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec) =	2✔
167	and	2✔
168	[ mustKeys `Set.isSubsetOf` Map.keysSet m	2✔
169	, all (`elem` Map.elems m) mustVals	2✔
170	, sizeOf m `conformsToSpec` size	2✔
171	, all (`conformsToSpec` kvs) (Map.toList m)	2✔
172	, Map.elems m `conformsToFoldSpec` foldSpec	2✔
173	]
174
175	genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) NoFold)	2✔
176	\| null mustKeys	2✔
177	, null mustVals = do	2✔
178	let size' =	2✔
179	fold	2✔
180	[ maybe TrueSpec (leqSpec . max 0) mHint	2✔
181	, size	2✔
182	, maxSpec (cardinality (fstSpec kvs))	2✔
183	, maxSpec (cardinalTrueSpec @k)	2✔
184	, geqSpec 0	2✔
185	]
186	n <- genFromSpecT size'	2✔
187	let go sz 0 slow kvs' m	2✔
188	\| fromInteger sz == Map.size m = pure m	2✔
189	\| not slow = go sz (sz - fromIntegral (Map.size m)) True (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty)) m	1✔
190	\| otherwise = fatalError "The impossible happened"	×
191	go sz n' slow kvs' m = do	2✔
192	mkv <- inspect $ genFromSpecT kvs'	2✔
193	case mkv of	2✔
194	Result (k, v) ->
195	go	2✔
196	sz	2✔
197	(n' - 1)	2✔
198	slow	2✔
199	(kvs' <> if slow then typeSpec (Cartesian (notEqualSpec k) mempty) else mempty)	2✔
200	(Map.insert k v m)	2✔
201	GenError msgs ->
202	if sizeOf m `conformsToSpec` size	1✔
203	then pure m	2✔
204	else
UNCOV 205	genErrorNE	×
206	(pure "Gen error while trying to generate enough elements for a Map." <> catMessageList msgs)	×
207	FatalError msgs ->
UNCOV 208	genErrorNE	×
209	( NE.fromList	×
210	[ "Fatal error while trying to generate enough elements for a map:"	×
211	, " The ones we have generated so far = " ++ show m	×
212	, " The number we need to still generate: n' = " ++ show n'	×
213	, "The original size spec " ++ show size	×
214	, "The refined size spec " ++ show size'	×
215	, "The computed target size " ++ show n	×
216	, "Fatal error messages"	×
217	, "<<<---"	×
218	]
219	<> catMessageList msgs	×
220	<> (pure "--->>>")	×
221	)
222	explain (" The number we are trying for: n = " ++ show n) $ go n n False kvs mempty	1✔
223	genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do	2✔
224	!mustMap <- explain "Make the mustMap" $ forM (Set.toList mustKeys) $ \k -> do	2✔
225	let vSpec = constrained $ \v -> satisfies (pair_ (Lit k) v) kvs	2✔
226	v <- explain (show $ "vSpec =" <+> pretty vSpec) $ genFromSpecT vSpec	1✔
227	pure (k, v)	2✔
228	let haveVals = map snd mustMap	2✔
229	mustVals' = filter (`notElem` haveVals) mustVals	2✔
230	size' = simplifySpec $ constrained $ \sz ->	2✔
231	-- TODO, we should make sure size' is greater than or equal to 0
232	satisfies	2✔
233	(sz + Lit (sizeOf mustMap))	2✔
234	( maybe TrueSpec (leqSpec . max 0) mHint	2✔
235	<> size	2✔
236	<> maxSpec (cardinality (fstSpec kvs)) -- (mapSpec FstW $ mapSpec ToGenericW kvs))	2✔
237	<> maxSpec (cardinalTrueSpec @k)	2✔
238	)
239	!foldSpec' = case foldSpec of	2✔
240	NoFold -> NoFold	2✔
241	FoldSpec fn@(Fun symbol) sumSpec -> FoldSpec fn $ propagate theAddFn (HOLE :? Value mustSum :> Nil) sumSpec	2✔
242	where
243	mustSum = adds (map (semantics symbol) haveVals)	2✔
244	let !valsSpec =	2✔
245	ListSpec	2✔
246	Nothing	2✔
247	mustVals'	2✔
248	size'	2✔
249	(simplifySpec $ constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs)	2✔
250	foldSpec'	2✔
251
252	!restVals <-
253	explainNE	2✔
254	( NE.fromList	×
255	[ "Make the restVals"	×
256	, show $ " valsSpec =" <+> pretty valsSpec	×
257	, show $ " mustMap =" <+> viaShow mustMap	×
258	, show $ " size' =" <+> pretty size'	×
259	]
260	)
261	$ genFromTypeSpec	2✔
262	$ valsSpec	2✔
263	let go m [] = pure m	2✔
264	go m (v : restVals') = do	2✔
265	let keySpec = notMemberSpec (Map.keysSet m) <> constrained (\k -> pair_ k (Lit v) `satisfies` kvs)	2✔
266	k <-
267	explainNE	2✔
268	( NE.fromList	×
269	[ "Make a key"	×
270	, show $ indent 4 $ "keySpec =" <+> pretty keySpec	×
271	]
272	)
273	$ genFromSpecT keySpec	2✔
274	go (Map.insert k v m) restVals'	2✔
275
276	go (Map.fromList mustMap) restVals	2✔
277
278	cardinalTypeSpec _ = TrueSpec	×
279
280	shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)	2✔
281
282	fixupWithTypeSpec _ _ = Nothing	2✔
283
284	toPreds m (MapSpec mHint mustKeys mustVals size kvs foldSpec) =	2✔
285	toPred	2✔
286	[ Assert $ Lit mustKeys `subset_` dom_ m	2✔
287	, forAll (Lit mustVals) $ \val ->	2✔
288	val `elem_` rng_ m	2✔
289	, sizeOf_ (rng_ m) `satisfies` size	2✔
290	, forAll m $ \kv -> satisfies kv kvs	2✔
291	, toPredsFoldSpec (rng_ m) foldSpec	2✔
292	, maybe TruePred (`genHint` m) mHint	2✔
293	]
294
295	instance
296	(Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
297	HasGenHint (Map k v)
298	where
299	type Hint (Map k v) = Integer
300	giveHint h = typeSpec $ defaultMapSpec {mapSpecHint = Just h}	2✔
301
302	------------------------------------------------------------------------
303	-- Logic instances for
304	------------------------------------------------------------------------
305
306	-- \| Function symbols for talking about maps
307	data MapW (dom :: [Type]) (rng :: Type) where
308	DomW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] (Set k)
309	RngW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] [v]
310	LookupW ::
311	(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[k, Map k v] (Maybe v)
312
313	deriving instance Eq (MapW dom rng)	×
314
315	instance Semantics MapW where
316	semantics DomW = Map.keysSet	2✔
317	semantics RngW = Map.elems	2✔
318	semantics LookupW = Map.lookup	2✔
319
320	instance Syntax MapW	×
321
322	instance Show (MapW d r) where	×
323	show DomW = "dom_"	2✔
324	show RngW = "rng_"	2✔
325	show LookupW = "lookup_"	2✔
326
327	instance Logic MapW where	1✔
328	propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s	2✔
329	propagate _ _ TrueSpec = TrueSpec	2✔
330	propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs	1✔
331	propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)	2✔
332	propagate DomW (Unary HOLE) spec =
333	case spec of	2✔
334	MemberSpec (s :\| []) ->
335	typeSpec $	2✔
336	MapSpec Nothing s [] (equalSpec $ sizeOf s) TrueSpec NoFold	2✔
337	TypeSpec (SetSpec must elemspec size) [] ->
338	typeSpec $	2✔
339	MapSpec	2✔
340	Nothing	2✔
341	must	2✔
342	[]	2✔
343	size	2✔
344	(constrained $ \kv -> satisfies (fst_ kv) elemspec)	2✔
345	NoFold	2✔
346	_ -> ErrorSpec (NE.fromList ["Dom on bad map spec", show spec])	1✔
347	propagate RngW (Unary HOLE) spec =
348	case spec of	2✔
349	TypeSpec (ListSpec listHint must size elemspec foldspec) [] ->
350	typeSpec $	2✔
351	MapSpec	2✔
352	listHint	2✔
353	Set.empty	2✔
354	must	2✔
355	size	2✔
356	(constrained $ \kv -> satisfies (snd_ kv) elemspec)	2✔
357	foldspec	2✔
358	-- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that
359	-- requires not only that the elements of the map are fixed to what is in `r`,
360	-- but they appear in the order that they are in `r`. That's
361	-- very difficult to achieve!
362	_ -> ErrorSpec (NE.fromList ["Rng on bad map spec", show spec])	1✔
363	propagate LookupW (Value k :! Unary HOLE) spec =
364	constrained $ \m ->	2✔
365	[Assert $ Lit k `member_` dom_ m \| not $ Nothing `conformsToSpec` spec]	2✔
366	++ [ forAll m $ \kv ->	2✔
367	letBind (fst_ kv) $ \k' ->	2✔
368	letBind (snd_ kv) $ \v ->	2✔
369	whenTrue (Lit k ==. k') $	2✔
370	-- TODO: What you want to write is `just_ v `satisfies` spec` but we can't
371	-- do that because we don't have access to `IsNormalType v` here. When
372	-- we refactor the `IsNormalType` machinery we will be able to make
373	-- this nicer.
374	case spec of	2✔
375	MemberSpec as -> Assert $ v `elem_` Lit [a \| Just a <- NE.toList as]	2✔
376	TypeSpec (SumSpec _ _ vspec) cant ->
377	v `satisfies` (vspec <> notMemberSpec [a \| Just a <- cant])	2✔
378	]
379	propagate LookupW (HOLE :? Value m :> Nil) spec =
380	if Nothing `conformsToSpec` spec	2✔
381	then notMemberSpec [k \| (k, v) <- Map.toList m, not $ Just v `conformsToSpec` spec]	2✔
382	else
383	memberSpec	2✔
384	(Map.keys $ Map.filter ((`conformsToSpec` spec) . Just) m)	2✔
385	( NE.fromList	×
386	[ "propagate (lookup HOLE ms) on (MemberSpec ms)"	×
387	, "forall pairs (d,r) in ms, no 'd' conforms to spec"	×
388	, " " ++ show spec	×
389	]
390	)
391
392	mapTypeSpec DomW (MapSpec _ mustSet _ sz kvSpec _) = typeSpec $ SetSpec mustSet (fstSpec kvSpec) sz	×
393	mapTypeSpec RngW (MapSpec _ _ mustList sz kvSpec foldSpec) = typeSpec $ ListSpec Nothing mustList sz (sndSpec kvSpec) foldSpec	×
394
395	------------------------------------------------------------------------
396	-- Syntax
397	------------------------------------------------------------------------
398
399	-- \| Take the domain of a `Map` as a `Set`
400	dom_ ::
401	(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) =>
402	Term (Map k v) ->
403	Term (Set k)
404	dom_ = appTerm DomW	2✔
405
406	-- \| Take the range of a `Map` as a list
407	rng_ ::
408	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
409	Term (Map k v) ->
410	Term [v]
411	rng_ = appTerm RngW	2✔
412
413	-- \| Lookup a key in the `Map`
414	lookup_ ::
415	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
416	Term k ->
417	Term (Map k v) ->
418	Term (Maybe v)
419	lookup_ = appTerm LookupW	2✔
420
421	-- \| Check if a key is a member of the map
422	mapMember_ ::
423	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
424	Term k ->
425	Term (Map k v) ->
426	Term Bool
427	mapMember_ k m = not_ $ lookup_ k m ==. lit Nothing	×

input-output-hk / constrained-generators / 414

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous