input-output-hk / constrained-generators / 388

Committed 13 Nov 2025 02:13PM UTC coverage: 77.127% (-0.06%) from 77.191%

Build # 388

Build Type

push

github

Committed by

web-flow

Commit Message

Optimise how we deal with either specs (#54)

Run Details

38 of 39 new or added lines in 6 files covered. (97.44%)

13 existing lines in 7 files now uncovered.

3925 of 5089 relevant lines covered (77.13%)

1.46 hits per line

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

68.57

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

input-output-hk / constrained-generators / 388

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