-
Notifications
You must be signed in to change notification settings - Fork 155
/
Maps.hs
235 lines (215 loc) · 8.35 KB
/
Maps.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Constrained.Spec.Maps (MapSpec (..), dom_, rng_) where
import Constrained.Base
import Constrained.Core
import Constrained.GenT
import Constrained.Instances ()
import Constrained.List
import Constrained.Spec.Generics
import Constrained.Univ
import Control.Monad
import Data.List (nub)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Prettyprinter
import Test.QuickCheck (shrinkList)
------------------------------------------------------------------------
-- HasSpec
------------------------------------------------------------------------
instance Ord a => Sized (Map.Map a b) where
sizeOf = toInteger . Map.size
liftSizeSpec sz = TypeSpec (MapSpec mempty mempty (typeSpec sz) TrueSpec NoFold) []
liftMemberSpec xs = typeSpec (MapSpec mempty mempty (MemberSpec xs) TrueSpec NoFold)
sizeOfTypeSpec (MapSpec mustk mustv size _ _) =
typeSpec (atLeastSize (sizeOf mustk))
<> typeSpec (atLeastSize (sizeOf mustv))
<> size
data MapSpec fn k v = MapSpec
{ mapSpecMustKeys :: Set k
, mapSpecMustValues :: [v]
, mapSpecSize :: Spec fn Integer
, mapSpecElem :: Spec fn (k, v)
, mapSpecFold :: FoldSpec fn v
}
deriving instance
( HasSpec fn (k, v)
, HasSpec fn k
, HasSpec fn v
, HasSpec fn [v]
) =>
Show (MapSpec fn k v)
instance Ord k => Forallable (Map k v) (k, v) where
forAllSpec kvs = typeSpec $ MapSpec mempty [] TrueSpec kvs NoFold
forAllToList = Map.toList
instance
(Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
HasSpec fn (Map k v)
where
type TypeSpec fn (Map k v) = MapSpec fn k v
type Prerequisites fn (Map k v) = (HasSpec fn k, HasSpec fn v)
emptySpec = MapSpec mempty mempty mempty mempty NoFold
combineSpec
(MapSpec mustKeys mustVals size kvs foldSpec)
(MapSpec mustKeys' mustVals' size' kvs' foldSpec') = fromGE ErrorSpec $ do
typeSpec
. MapSpec
(mustKeys <> mustKeys')
(nub $ mustVals <> mustVals')
(size <> size')
(kvs <> kvs')
<$> combineFoldSpec foldSpec 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 mustKeys mustVals size kvs foldSpec) = do
mustMap <- explain ["Make the mustMap"] $ forM (Set.toList mustKeys) $ \k -> do
let vSpec = constrained $ \v -> satisfies (app (fromGenericFn @fn) $ app (pairFn @fn) (Lit k) v) kvs
v <- explain [show $ "vSpec =" <+> pretty vSpec] $ genFromSpec vSpec
pure (k, v)
let haveVals = map snd mustMap
mustVals' = filter (`notElem` haveVals) mustVals
size' = constrained $ \sz ->
-- TODO, we should make sure size' is greater than or equal to 0
satisfies
(sz + Lit (sizeOf mustMap))
(size <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
foldSpec' = case foldSpec of
NoFold -> NoFold
FoldSpec fn sumSpec -> FoldSpec fn $ propagateSpecFun (theAddFn @fn) (HOLE :? Value mustSum :> Nil) sumSpec
where
mustSum = adds @fn (map (sem fn) haveVals)
let valsSpec =
ListSpec
Nothing
mustVals'
size'
(constrained $ \v -> unsafeExists $ \k -> pair_ k v `satisfies` kvs)
foldSpec'
restVals <-
explain
[ "Make the restVals"
, " valsSpec = " ++ show valsSpec
]
$ 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 <-
explain
[ "Make a key"
, show $ indent 4 $ "keySpec =" <+> pretty keySpec
]
$ genFromSpec keySpec
go (Map.insert k v m) restVals'
go (Map.fromList mustMap) restVals
shrinkWithTypeSpec (MapSpec _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)
toPreds m (MapSpec mustKeys mustVals size kvs foldSpec) =
toPred
[ assert $ app (subsetFn @fn) (app (domFn @fn) m) (Lit mustKeys)
, forAll (Lit mustVals) $ \val ->
app (elemFn @fn) val (app (rngFn @fn) m)
, -- TODO: make nice
satisfies (app (injectFn $ SizeOf @fn) $ app (rngFn @fn) m) size
, forAll m $ \kv -> satisfies kv kvs
, toPredsFoldSpec (app (rngFn @fn) m) foldSpec
]
------------------------------------------------------------------------
-- Functions
------------------------------------------------------------------------
instance BaseUniverse fn => Functions (MapFn fn) fn where
propagateSpecFun _ _ TrueSpec = TrueSpec
propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err
propagateSpecFun fn ctx spec = case fn of
_
| SuspendedSpec v ps <- spec
, ListCtx pre HOLE suf <- ctx ->
constrained $ \v' ->
let args = appendList (mapList (\(Value a) -> Lit a) pre) (v' :> mapList (\(Value a) -> Lit a) suf)
in Let (App (injectFn fn) args) (v :-> ps)
Dom ->
-- No TypeAbstractions in ghc-8.10
case fn of
(_ :: MapFn fn '[Map k v] (Set k))
| NilCtx HOLE <- ctx
, Evidence <- prerequisites @fn @(Map k v) ->
case spec of
MemberSpec [s] ->
typeSpec $
MapSpec s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold
TypeSpec (SetSpec must elemspec size) [] ->
typeSpec $
MapSpec
must
[]
size
(constrained $ \kv -> satisfies (app (fstFn @fn) (app (toGenericFn @fn) kv)) elemspec)
NoFold
_ -> ErrorSpec ["Dom on bad map spec", show spec]
Rng ->
-- No TypeAbstractions in ghc-8.10
case fn of
(_ :: MapFn fn '[Map k v] [v])
| NilCtx HOLE <- ctx
, Evidence <- prerequisites @fn @(Map k v) ->
case spec of
MemberSpec [r] ->
typeSpec $ MapSpec Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold
TypeSpec (ListSpec Nothing must size elemspec foldspec) [] ->
typeSpec $
MapSpec
Set.empty
must
size
(constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec)
foldspec
_ -> ErrorSpec ["Rng on bad map spec", show spec]
-- NOTE: this function over-approximates and returns a liberal spec.
mapTypeSpec f ts = case f of
-- TODO: consider checking against singleton member-specs in the other component
-- interacting with cant
Dom ->
-- No TypeAbstractions in ghc-8.10
case f of
(_ :: MapFn fn '[Map k v] (Set k))
| MapSpec mustSet _ sz kvSpec _ <- ts
, Evidence <- prerequisites @fn @(Map k v) ->
typeSpec $ SetSpec mustSet (mapSpec (fstFn @fn) $ toSimpleRepSpec kvSpec) sz
Rng ->
-- No TypeAbstractions in ghc-8.10
case f of
(_ :: MapFn fn '[Map k v] [v])
| MapSpec _ mustList sz kvSpec foldSpec <- ts
, Evidence <- prerequisites @fn @(Map k v) ->
typeSpec $ ListSpec Nothing mustList sz (mapSpec (sndFn @fn) $ toSimpleRepSpec kvSpec) foldSpec
------------------------------------------------------------------------
-- Syntax
------------------------------------------------------------------------
dom_ ::
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) ->
Term fn (Set k)
dom_ = app domFn
rng_ ::
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) ->
Term fn [v]
rng_ = app rngFn