never executed always true always false
1 -- {-# LANGUAGE Rank2Types #-}
2 {-# LANGUAGE RecordWildCards #-}
3 {-# LANGUAGE QuasiQuotes #-}
4
5 module Conjure.Representations.Partition.Occurrence ( partitionOccurrence ) where
6
7 -- conjure
8 import Conjure.Prelude
9 import Conjure.Bug
10 import Conjure.Language
11 import Conjure.Language.DomainSizeOf
12 import Conjure.Language.Expression.DomainSizeOf ()
13 import Conjure.Language.ZeroVal ( zeroVal, EnumerateDomain )
14 import Conjure.Representations.Internal
15 import Conjure.Representations.Common
16 import Conjure.Representations.Function.Function1D ( domainValues )
17
18
19 -- | works for "partition from A", where A can be used as an index of a matrix
20 -- _WhichPart: matrix indexed by [A] of int(1..maxNumParts)
21 -- (indicating which part an element belongs to)
22 -- _NumParts : int(1..maxNumParts)
23 -- (indicating the total number of parts)
24 -- only use part numbers from 1.._NumParts, never use the others
25 -- part(i) is used -> part(i-1) is used, forAll i:int(3..maxNumParts)
26 partitionOccurrence :: forall m . (MonadFailDoc m, NameGen m, EnumerateDomain m) => Representation m
27 partitionOccurrence = Representation chck downD structuralCons downC up symmetryOrdering
28
29 where
30
31 chck :: TypeOf_ReprCheck m
32 chck f (DomainPartition _ attrs innerDomain)
33 | domainCanIndexMatrix innerDomain
34 = map (DomainPartition Partition_Occurrence attrs) <$> f innerDomain
35 chck _ _ = return []
36
37 nameNumParts = mkOutName (Just "NumParts")
38 nameWhichPart = mkOutName (Just "WhichPart")
39 namePartSizes = mkOutName (Just "PartSizes")
40 nameFirstIndex = mkOutName (Just "FirstIndex")
41
42 getMaxNumParts attrs d =
43 case partsNum attrs of
44 SizeAttr_Size x -> return x
45 SizeAttr_MaxSize x -> return x
46 SizeAttr_MinMaxSize _ x -> return x
47 _ -> domainSizeOf d
48
49 getMaxPartSizes attrs d =
50 case partsSize attrs of
51 SizeAttr_Size x -> return x
52 SizeAttr_MaxSize x -> return x
53 SizeAttr_MinMaxSize _ x -> return x
54 _ -> domainSizeOf d
55
56 -- downD :: TypeOf_DownD m
57 downD (name, domain@(DomainPartition Partition_Occurrence attrs innerDomain))
58 | domainCanIndexMatrix innerDomain = do
59 maxNumParts <- getMaxNumParts attrs innerDomain
60 maxPartSizes <- getMaxPartSizes attrs innerDomain
61 return $ Just
62 [
63 -- number of active parts
64 ( nameNumParts domain name
65 , DomainInt TagInt [RangeBounded 1 maxNumParts]
66 )
67 -- for each element, the part it belongs to
68 , ( nameWhichPart domain name
69 , DomainMatrix
70 (forgetRepr innerDomain)
71 (DomainInt TagInt [RangeBounded 1 maxNumParts])
72 )
73 -- for each part, number of elements in the part
74 , ( namePartSizes domain name
75 , DomainMatrix
76 (DomainInt TagInt [RangeBounded 1 maxNumParts])
77 (DomainInt TagInt [RangeBounded 0 maxPartSizes])
78 )
79 -- wtf was this?
80 , ( nameFirstIndex domain name
81 , DomainMatrix
82 (DomainInt TagInt [RangeBounded 1 maxNumParts])
83 innerDomain -- dontCare if not used
84 )
85 ]
86 downD _ = na "{downD} Occurrence"
87
88 structuralCons :: TypeOf_Structural m
89 structuralCons _ downX1 (DomainPartition _ attrs innerDomain)
90 | domainCanIndexMatrix innerDomain = do
91 maxNumParts <- getMaxNumParts attrs innerDomain
92 let
93 numPartsChannelling whichPart numPartsVar = do
94 (iPat, i) <- quantifiedVar
95 return $ return -- for list
96 [essence|
97 &numPartsVar =
98 max([ &whichPart[&i] | &iPat : &innerDomain ])
99 |]
100
101 partSizesChannelling whichPart partSizesVar = do
102 (iPat, i) <- quantifiedVar
103 (jPat, j) <- quantifiedVar
104 return $ return -- for list
105 [essence|
106 and([ &partSizesVar[&i] = sum([ 1 | &jPat : &innerDomain , &whichPart[&j] = &i ])
107 | &iPat : int(1..&maxNumParts)
108 ])
109 |]
110
111 firstIndexChannelling whichPart numPartsVar firstIndexVar = do
112 (iPat, i) <- quantifiedVar
113 (jPat, j) <- quantifiedVar
114 return
115 [ -- firstIndexVar[i] is <= all indices belonging to part i
116 [essence|
117 forAll &iPat : int(1..&maxNumParts) , &i <= &numPartsVar .
118 forAll &jPat : &innerDomain .
119 &whichPart[&j] = &i -> &firstIndexVar[&i] <= &j
120 |]
121 , -- firstIndexVar[i] is equal to one of those
122 [essence|
123 forAll &iPat : int(1..&maxNumParts) , &i <= &numPartsVar .
124 exists &jPat : &innerDomain .
125 &whichPart[&j] = &i /\ &firstIndexVar[&i] = &j
126 |]
127 , -- firstIndexVar[i] is dontCare, if nothing is in part i
128 [essence|
129 forAll &iPat : int(1..&maxNumParts) , &i > &numPartsVar .
130 dontCare(&firstIndexVar[&i])
131 |]
132 ]
133
134 symmetryBreaking numPartsVar firstIndexVar = do
135 (iPat, i) <- quantifiedVar
136 (jPat, j) <- quantifiedVar
137 return $ return -- for list
138 [essence|
139 forAll &iPat, &jPat : int(1..&maxNumParts) , &i <= &numPartsVar /\ &j <= &numPartsVar .
140 &i < &j <-> &firstIndexVar[&i] < &firstIndexVar[&j]
141 |]
142
143 numPartsCons numPartsVar =
144 return $ mkSizeCons (partsNum attrs) numPartsVar
145
146 partSizeCons numPartsVar partSizesVar = do
147 (iPat, i) <- quantifiedVar
148 let theConsForI = make opAnd $ fromList $
149 mkSizeCons (partsSize attrs) [essence| &partSizesVar[&i] |]
150 return
151 [ [essence|
152 and([ &theConsForI
153 | &iPat : int(1..&maxNumParts) $ forAll part numbers
154 , &i <= &numPartsVar $ that are active
155 ])
156 |]
157 , [essence|
158 and([ &partSizesVar[&i] = 0
159 | &iPat : int(1..&maxNumParts) $ forAll part numbers
160 , &i > &numPartsVar $ that are inactive
161 ])
162 |]
163 ]
164
165 noGaps whichPart numPartsVar = do
166 (iPat, i) <- quantifiedVar
167 (jPat, j) <- quantifiedVar
168 return $ return -- for list
169 [essence|
170 and([ or([ &whichPart[&j] = &i $ there must be a member in that part
171 | &jPat : &innerDomain
172 ])
173 | &iPat : int(3..&maxNumParts) $ forAll part numbers (except 1 and 2)
174 , &i <= &numPartsVar $ that are active
175 ])
176 |]
177
178 fixedPartSize =
179 case attrs of
180 PartitionAttr _ SizeAttr_Size{} _ -> True
181 _ -> False
182
183 regular numPartsVar partSizesVar | isRegular attrs && not fixedPartSize = do
184 (iPat, i) <- quantifiedVar
185 return $ return -- for list
186 [essence|
187 and([ &partSizesVar[&i-1] = &partSizesVar[&i]
188 | &iPat : int(2..&maxNumParts)
189 , &i <= &numPartsVar
190 ])
191 |]
192 regular _ _ = return []
193
194 return $ \ inpPartition -> do
195 [numPartsVar, whichPart, partSizesVar, firstIndexVar] <- downX1 inpPartition
196 concat <$> sequence
197 [ partSizeCons numPartsVar partSizesVar
198 , numPartsCons numPartsVar
199 , noGaps whichPart numPartsVar
200 , regular numPartsVar partSizesVar
201 , numPartsChannelling whichPart numPartsVar
202 , partSizesChannelling whichPart partSizesVar
203 , firstIndexChannelling whichPart numPartsVar firstIndexVar
204 , symmetryBreaking numPartsVar firstIndexVar
205 ]
206 structuralCons _ _ domain = na $ vcat [ "{structuralCons} Occurrence"
207 , "domain:" <+> pretty domain
208 ]
209
210 downC :: TypeOf_DownC m
211 downC ( name
212 , inDom@(DomainPartition Partition_Occurrence attrs innerDomain)
213 , inConstant@(viewConstantPartition -> Just vals)
214 ) = do
215 Just [ ( numPartsVar , numPartsDom )
216 , ( whichPart , whichPartDom )
217 , ( partSizesVar , partSizesDom )
218 , ( firstIndexVar , firstIndexDom )
219 ] <- downD (name, inDom)
220 members <- domainValues innerDomain
221 maxNumParts' <- getMaxNumParts attrs innerDomain
222 maxNumParts <- case viewConstantInt maxNumParts' of
223 Just i -> return i
224 Nothing -> bug ("expecting an integer literal, but got:" <++> pretty maxNumParts')
225 z <- zeroVal innerDomain
226 let
227 whichPartValInside :: [(Integer, Constant)]
228 whichPartValInside =
229 [ case whichPartIsIt of
230 [p] -> p
231 [] -> bug $ vcat [ "Not found:" <+> pretty mem
232 , "Inside:" <+> pretty inConstant
233 ]
234 _ -> bug $ vcat [ "Found multiple times:" <+> pretty mem
235 , "Inside:" <+> pretty inConstant
236 ]
237 | mem <- members
238 , let whichPartIsIt = [ (p, mem)
239 | (p, pVals) <- zip [1..] vals
240 , mem `elem` pVals
241 ]
242 ]
243 numPartsVal = ConstantInt TagInt (genericLength vals)
244 whichPartVal = ConstantAbstract (AbsLitMatrix
245 (forgetRepr innerDomain)
246 (map (ConstantInt TagInt . fst) whichPartValInside))
247 partSizesVal = ConstantAbstract (AbsLitMatrix
248 (DomainInt TagInt [RangeBounded 1 maxNumParts'])
249 (map (ConstantInt TagInt . genericLength) vals
250 ++ replicate (fromInteger (maxNumParts - genericLength vals))
251 (ConstantInt TagInt 0)))
252 firstIndexVal = ConstantAbstract (AbsLitMatrix
253 (DomainInt TagInt [RangeBounded 1 maxNumParts'])
254 ([ case lookup p whichPartValInside of
255 Nothing -> bug $ vcat [ "Not found:" <+> pretty p
256 , "Inside:" <+> prettyList id "," whichPartValInside
257 ]
258 Just i -> i
259 | p <- [1..genericLength vals] ]
260 ++ replicate (fromInteger (maxNumParts - genericLength vals))
261 z))
262 return $ Just
263 [ ( numPartsVar , numPartsDom , numPartsVal )
264 , ( whichPart , whichPartDom , whichPartVal )
265 , ( partSizesVar , partSizesDom , partSizesVal )
266 , ( firstIndexVar , firstIndexDom , firstIndexVal )
267 ]
268 downC (name, domain, constant) = na $ vcat [ "{downC} Occurrence"
269 , "name:" <+> pretty name
270 , "domain:" <+> pretty domain
271 , "constant:" <+> pretty constant
272 ]
273
274 up :: TypeOf_Up m
275 up ctxt (name, domain@(DomainPartition Partition_Occurrence _ innerDomain)) =
276 case (lookup (nameNumParts domain name) ctxt, lookup (nameWhichPart domain name) ctxt) of
277 ( Just (viewConstantInt -> Just numPartsValue) ,
278 Just (viewConstantMatrix -> Just (_, whichPartValues)) ) -> do
279 members <- domainValues innerDomain
280 return
281 ( name
282 , normaliseConstant $ ConstantAbstract $ AbsLitPartition
283 [ [ member | (member, b) <- zip members whichPartValues, b == ConstantInt TagInt bucket ]
284 | bucket <- [1..numPartsValue]
285 ]
286 )
287 (Just val, _) -> failDoc $ vcat $
288 [ "(in Partition Occurrence up)"
289 , "Expecting an integer literal for:" <+> pretty (nameNumParts domain name)
290 , "But got:" <+> pretty val
291 , "When working on:" <+> pretty name
292 , "With domain:" <+> pretty domain
293 ] ++
294 ("Bindings in context:" : prettyContext ctxt)
295 (_, Just val) -> failDoc $ vcat $
296 [ "(in Partition Occurrence up)"
297 , "Expecting a matrix literal for:" <+> pretty (nameWhichPart domain name)
298 , "But got:" <+> pretty val
299 , "When working on:" <+> pretty name
300 , "With domain:" <+> pretty domain
301 ] ++
302 ("Bindings in context:" : prettyContext ctxt)
303 (Nothing, _) -> failDoc $ vcat $
304 [ "(in Partition Occurrence up)"
305 , "No value for:" <+> pretty (nameNumParts domain name)
306 , "When working on:" <+> pretty name
307 , "With domain:" <+> pretty domain
308 ] ++
309 ("Bindings in context:" : prettyContext ctxt)
310 up ctxt (name, domain) =
311 na $ vcat [ "{up} Occurrence"
312 , "name:" <+> pretty name
313 , "domain:" <+> pretty domain
314 , "ctxt:" <+> vcat (map pretty ctxt)
315 ]
316
317 symmetryOrdering :: TypeOf_SymmetryOrdering m
318 symmetryOrdering innerSO downX1 inp domain = do
319 xs <- downX1 inp
320 Just xsDoms' <- downD ("SO", domain)
321 let xsDoms = map snd xsDoms'
322 soValues <- sequence [ innerSO downX1 x xDom | (x, xDom) <- zip xs xsDoms ]
323 return $ AbstractLiteral $ AbsLitTuple soValues
324