input-output-hk / constrained-generators / 416

Committed 21 Nov 2025 08:35AM UTC coverage: 76.66% (+0.2%) from 76.458%

Build # 416

Build Type

push

github

Committed by

web-flow

Commit Message

fourmolu (#60)

Run Details

179 of 191 new or added lines in 14 files covered. (93.72%)

10 existing lines in 4 files now uncovered.

3948 of 5150 relevant lines covered (76.66%)

1.45 hits per line

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

68.78

/src/Constrained/Spec/Map.hs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  emptySpec = defaultMapSpec

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

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

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

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

    go (Map.fromList mustMap) restVals

  cardinalTypeSpec _ = TrueSpec

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

  fixupWithTypeSpec _ _ = Nothing

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

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

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

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

deriving instance Eq (MapW dom rng)

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

instance Syntax MapW

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

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

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

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

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

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

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

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

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

input-output-hk / constrained-generators / 416

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