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