input-output-hk / constrained-generators / 457

Committed 10 Dec 2025 01:30PM UTC coverage: 76.948% (-0.5%) from 77.401%

Build # 457

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 7c2c067b5 into 966f65f3c

Run Details

15 of 15 new or added lines in 2 files covered. (100.0%)

24 existing lines in 5 files now uncovered.

3969 of 5158 relevant lines covered (76.95%)

1.45 hits per line

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

68.92

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

input-output-hk / constrained-generators / 457

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