input-output-hk / constrained-generators / 500

Committed 08 Jan 2026 10:49AM UTC coverage: 77.318% (+0.1%) from 77.177%

Build # 500

Build Type

push

github

Committed by

web-flow

Commit Message

Test and fix for bad behaviour of chooseSpec (#68)

Run Details

32 of 34 new or added lines in 4 files covered. (94.12%)

2 existing lines in 2 files now uncovered.

4019 of 5198 relevant lines covered (77.32%)

1.46 hits per line

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

70.54

/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 fc sz 0 slow kvs' m
              | fromInteger sz == Map.size m = pure m
              | not slow =
                  go
                    fc
                    sz
                    (sz - fromIntegral (Map.size m))
                    True
                    (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty))
                    m
              | otherwise = fatalError "The impossible happened"
            go fc sz n' slow kvs' m = do
              mkv <- inspect $ genFromSpecT kvs'
              case mkv of
                Result (k, v) ->
                  go
                    fc
                    sz
                    (n' - 1)
                    slow
                    (kvs' <> if slow then typeSpec (Cartesian (notEqualSpec k) mempty) else mempty)
                    (Map.insert k v m)
                GenError {} | fc > 0 -> go (fc - 1) sz n' slow kvs' 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 (10 * n) 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 fc sz 0 slow kvs' m	2✔
188	\| fromInteger sz == Map.size m = pure m	2✔
189	\| not slow =	1✔
190	go	2✔
191	fc	2✔
192	sz	2✔
193	(sz - fromIntegral (Map.size m))	2✔
194	True	2✔
195	(kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty))	2✔
196	m	2✔
197	\| otherwise = fatalError "The impossible happened"	×
198	go fc sz n' slow kvs' m = do	2✔
199	mkv <- inspect $ genFromSpecT kvs'	2✔
200	case mkv of	2✔
201	Result (k, v) ->
202	go	2✔
203	fc	2✔
204	sz	2✔
205	(n' - 1)	2✔
206	slow	2✔
207	(kvs' <> if slow then typeSpec (Cartesian (notEqualSpec k) mempty) else mempty)	2✔
208	(Map.insert k v m)	2✔
209	GenError {} \| fc > 0 -> go (fc - 1) sz n' slow kvs' m	2✔
210	GenError msgs ->
211	if sizeOf m `conformsToSpec` size	1✔
UNCOV 212	then pure m	×
213	else
214	genErrorNE	2✔
215	(pure "Gen error while trying to generate enough elements for a Map." <> catMessageList msgs)	×
216	FatalError msgs ->
217	genErrorNE	2✔
218	( NE.fromList	×
219	[ "Fatal error while trying to generate enough elements for a map:"	×
220	, " The ones we have generated so far = " ++ show m	×
221	, " The number we need to still generate: n' = " ++ show n'	×
222	, "The original size spec " ++ show size	×
223	, "The refined size spec " ++ show size'	×
224	, "The computed target size " ++ show n	×
225	, "Fatal error messages"	×
226	, "<<<---"	×
227	]
228	<> catMessageList msgs	×
229	<> (pure "--->>>")	×
230	)
231	explain (" The number we are trying for: n = " ++ show n) $ go (10 * n) n n False kvs mempty	1✔
232	genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do	2✔
233	!mustMap <- explain "Make the mustMap" $ forM (Set.toList mustKeys) $ \k -> do	1✔
234	let vSpec = constrained $ \v -> satisfies (pair_ (Lit k) v) kvs	2✔
235	v <- explain (show $ "vSpec =" <+> pretty vSpec) $ genFromSpecT vSpec	1✔
236	pure (k, v)	2✔
237	let haveVals = map snd mustMap	2✔
238	mustVals' = filter (`notElem` haveVals) mustVals	2✔
239	size' = simplifySpec $ constrained $ \sz ->	2✔
240	-- TODO, we should make sure size' is greater than or equal to 0
241	satisfies	2✔
242	(sz + Lit (sizeOf mustMap))	2✔
243	( maybe TrueSpec (leqSpec . max 0) mHint	2✔
244	<> size	2✔
245	<> maxSpec (cardinality (fstSpec kvs)) -- (mapSpec FstW $ mapSpec ToGenericW kvs))	2✔
246	<> maxSpec (cardinalTrueSpec @k)	2✔
247	)
248	!foldSpec' = case foldSpec of	2✔
249	NoFold -> NoFold	2✔
250	FoldSpec fn@(Fun symbol) sumSpec -> FoldSpec fn $ propagate theAddFn (HOLE :? Value mustSum :> Nil) sumSpec	2✔
251	where
252	mustSum = adds (map (semantics symbol) haveVals)	2✔
253	let !valsSpec =	2✔
254	ListSpec	2✔
255	Nothing	2✔
256	mustVals'	2✔
257	size'	2✔
258	(simplifySpec $ constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs)	2✔
259	foldSpec'	2✔
260
261	!restVals <-
262	explainNE	2✔
263	( NE.fromList	×
264	[ "Make the restVals"	×
265	, show $ " valsSpec =" <+> pretty valsSpec	×
266	, show $ " mustMap =" <+> viaShow mustMap	×
267	, show $ " size' =" <+> pretty size'	×
268	]
269	)
270	$ genFromTypeSpec	2✔
271	$ valsSpec	2✔
272	let go m [] = pure m	2✔
273	go m (v : restVals') = do	2✔
274	let keySpec = notMemberSpec (Map.keysSet m) <> constrained (\k -> pair_ k (Lit v) `satisfies` kvs)	2✔
275	k <-
276	explainNE	2✔
277	( NE.fromList	×
278	[ "Make a key"	×
279	, show $ indent 4 $ "keySpec =" <+> pretty keySpec	×
280	]
281	)
282	$ genFromSpecT keySpec	2✔
283	go (Map.insert k v m) restVals'	2✔
284
285	go (Map.fromList mustMap) restVals	2✔
286
287	cardinalTypeSpec _ = TrueSpec	×
288
289	shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)	2✔
290
291	fixupWithTypeSpec _ _ = Nothing	2✔
292
293	toPreds m (MapSpec mHint mustKeys mustVals size kvs foldSpec) =	2✔
294	toPred	2✔
295	[ Assert $ Lit mustKeys `subset_` dom_ m	2✔
296	, forAll (Lit mustVals) $ \val ->	2✔
297	val `elem_` rng_ m	2✔
298	, sizeOf_ (rng_ m) `satisfies` size	2✔
299	, forAll m $ \kv -> satisfies kv kvs	2✔
300	, toPredsFoldSpec (rng_ m) foldSpec	2✔
301	, maybe TruePred (`genHint` m) mHint	2✔
302	]
303
304	instance
305	(Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
306	HasGenHint (Map k v)
307	where
308	type Hint (Map k v) = Integer
309	giveHint h = typeSpec $ defaultMapSpec {mapSpecHint = Just h}	2✔
310
311	------------------------------------------------------------------------
312	-- Logic instances for
313	------------------------------------------------------------------------
314
315	-- \| Function symbols for talking about maps
316	data MapW (dom :: [Type]) (rng :: Type) where
317	DomW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] (Set k)
318	RngW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] [v]
319	LookupW ::
320	(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[k, Map k v] (Maybe v)
321
322	deriving instance Eq (MapW dom rng)	×
323
324	instance Semantics MapW where
325	semantics DomW = Map.keysSet	2✔
326	semantics RngW = Map.elems	2✔
327	semantics LookupW = Map.lookup	2✔
328
329	instance Syntax MapW	×
330
331	instance Show (MapW d r) where	×
332	show DomW = "dom_"	2✔
333	show RngW = "rng_"	2✔
334	show LookupW = "lookup_"	2✔
335
336	instance Logic MapW where	1✔
337	propagate f ctxt (ExplainSpec es s) = explainSpec es $ propagate f ctxt s	2✔
338	propagate _ _ TrueSpec = TrueSpec	2✔
339	propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs	1✔
340	propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps)	2✔
341	propagate DomW (Unary HOLE) spec =
342	case spec of	2✔
343	MemberSpec (s :\| []) ->
344	typeSpec $	2✔
345	MapSpec Nothing s [] (equalSpec $ sizeOf s) TrueSpec NoFold	2✔
346	TypeSpec (SetSpec must elemspec size) [] ->
347	typeSpec $	2✔
348	MapSpec	2✔
349	Nothing	2✔
350	must	2✔
351	[]	2✔
352	size	2✔
353	(constrained $ \kv -> satisfies (fst_ kv) elemspec)	2✔
354	NoFold	2✔
355	_ -> ErrorSpec (NE.fromList ["Dom on bad map spec", show spec])	1✔
356	propagate RngW (Unary HOLE) spec =
357	case spec of	2✔
358	TypeSpec (ListSpec listHint must size elemspec foldspec) [] ->
359	typeSpec $	2✔
360	MapSpec	2✔
361	listHint	2✔
362	Set.empty	2✔
363	must	2✔
364	size	2✔
365	(constrained $ \kv -> satisfies (snd_ kv) elemspec)	2✔
366	foldspec	2✔
367	-- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that
368	-- requires not only that the elements of the map are fixed to what is in `r`,
369	-- but they appear in the order that they are in `r`. That's
370	-- very difficult to achieve!
371	_ -> ErrorSpec (NE.fromList ["Rng on bad map spec", show spec])	1✔
372	propagate LookupW (Value k :! Unary HOLE) spec =
373	constrained $ \m ->	2✔
374	[Assert $ Lit k `member_` dom_ m \| not $ Nothing `conformsToSpec` spec]	2✔
375	++ [ forAll m $ \kv ->	2✔
376	letBind (fst_ kv) $ \k' ->	2✔
377	letBind (snd_ kv) $ \v ->	2✔
378	whenTrue (Lit k ==. k') $	2✔
379	-- TODO: What you want to write is `just_ v `satisfies` spec` but we can't
380	-- do that because we don't have access to `IsNormalType v` here. When
381	-- we refactor the `IsNormalType` machinery we will be able to make
382	-- this nicer.
383	case spec of	2✔
384	MemberSpec as -> Assert $ v `elem_` Lit [a \| Just a <- NE.toList as]	2✔
385	TypeSpec (SumSpec _ _ vspec) cant ->
386	v `satisfies` (vspec <> notMemberSpec [a \| Just a <- cant])	2✔
387	]
388	propagate LookupW (HOLE :? Value m :> Nil) spec =
389	if Nothing `conformsToSpec` spec	2✔
390	then notMemberSpec [k \| (k, v) <- Map.toList m, not $ Just v `conformsToSpec` spec]	2✔
391	else
392	memberSpec	2✔
393	(Map.keys $ Map.filter ((`conformsToSpec` spec) . Just) m)	2✔
394	( NE.fromList	×
395	[ "propagate (lookup HOLE ms) on (MemberSpec ms)"	×
396	, "forall pairs (d,r) in ms, no 'd' conforms to spec"	×
397	, " " ++ show spec	×
398	]
399	)
400
401	mapTypeSpec DomW (MapSpec _ mustSet _ sz kvSpec _) = typeSpec $ SetSpec mustSet (fstSpec kvSpec) sz	×
402	mapTypeSpec RngW (MapSpec _ _ mustList sz kvSpec foldSpec) = typeSpec $ ListSpec Nothing mustList sz (sndSpec kvSpec) foldSpec	×
403
404	------------------------------------------------------------------------
405	-- Syntax
406	------------------------------------------------------------------------
407
408	-- \| Take the domain of a `Map` as a `Set`
409	dom_ ::
410	(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) =>
411	Term (Map k v) ->
412	Term (Set k)
413	dom_ = appTerm DomW	2✔
414
415	-- \| Take the range of a `Map` as a list
416	rng_ ::
417	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
418	Term (Map k v) ->
419	Term [v]
420	rng_ = appTerm RngW	2✔
421
422	-- \| Lookup a key in the `Map`
423	lookup_ ::
424	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
425	Term k ->
426	Term (Map k v) ->
427	Term (Maybe v)
428	lookup_ = appTerm LookupW	2✔
429
430	-- \| Check if a key is a member of the map
431	mapMember_ ::
432	(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
433	Term k ->
434	Term (Map k v) ->
435	Term Bool
436	mapMember_ k m = not_ $ lookup_ k m ==. lit Nothing	×

input-output-hk / constrained-generators / 500

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