never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Vertical.Matrix where
4
5 import Conjure.Rules.Import
6 import Conjure.Rules.Vertical.Tuple ( decomposeLexLt, decomposeLexLeq )
7
8 -- uniplate
9 import Data.Generics.Uniplate.Zipper ( hole )
10 import Data.Generics.Uniplate.Zipper as Zipper ( up )
11
12
13 rule_Comprehension_Literal :: Rule
14 rule_Comprehension_Literal = "matrix-comprehension-literal" `namedRuleZ` theRule where
15 theRule z (Comprehension body gensOrConds) = do
16 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
17 Generator (GenInExpr pat expr) -> return (pat, expr)
18 _ -> na "rule_Comprehension_Literal"
19 (_, _index, elems) <- match matrixLiteral expr
20 notInsideMinMax z
21 tyInner <- typeOf body
22 let ty = TypeMatrix (TypeInt TagInt) tyInner
23 return
24 ( "Vertical rule for matrix-comprehension on matrix literal"
25 , return $
26 case elems of
27 [] -> make matrixLiteral ty (mkDomainIntB 1 0) []
28 [el] -> Comprehension body
29 $ gocBefore
30 ++ [ComprehensionLetting pat el]
31 ++ gocAfter
32 _ -> make opConcatenate $ AbstractLiteral $ AbsLitMatrix
33 (mkDomainIntB 1 (fromInt $ genericLength elems))
34 [ Comprehension body
35 $ gocBefore
36 ++ [ComprehensionLetting pat el]
37 ++ gocAfter
38 | el <- elems
39 ]
40 )
41 theRule _ _ = na "rule_Comprehension_Literal"
42
43 notInsideMinMax z0 =
44 case Zipper.up z0 of
45 Nothing -> na "rule_Comprehension_Literal 1"
46 Just z1 -> do
47 let h = hole z1
48 case match opReducer h of
49 Just (_, False, _, _) -> na "rule_Comprehension_Literal"
50 Just (_, True , _, _) -> return ()
51 Nothing -> case Zipper.up z1 of
52 Nothing -> return ()
53 Just u -> notInsideMinMax u
54
55
56 rule_Comprehension :: Rule
57 rule_Comprehension = "matrix-comprehension" `namedRule` theRule where
58 theRule (Comprehension body gensOrConds) = do
59 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
60 Generator (GenInExpr pat expr) -> return (pat, expr)
61 _ -> na "rule_Comprehension"
62 case match matrixLiteral expr of
63 Just{} -> na "rule_Comprehension" -- this case is handled in rule_Comprehension_Literal
64 Nothing -> return ()
65 indexDom:_ <- indexDomainsOf expr
66 case indexDom of
67 DomainAny{} -> na "rule_Comprehension"
68 DomainInt _ [RangeLowerBounded _] -> na "rule_Comprehension"
69 _ -> return ()
70 return
71 ( "Comprehension on a matrix"
72 , do
73 (iPat, i) <- quantifiedVar
74 return $ Comprehension body
75 $ gocBefore
76 ++ [ Generator (GenDomainNoRepr iPat indexDom)
77 , ComprehensionLetting pat [essence| &expr[&i] |]
78 ]
79 ++ gocAfter
80 )
81 theRule _ = na "rule_Comprehension"
82
83
84 rule_Comprehension_Flatten :: Rule
85 rule_Comprehension_Flatten = "matrix-comprehension-flatten" `namedRule` theRule where
86 theRule (Comprehension body gensOrConds) = do
87 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
88 Generator (GenInExpr pat expr) -> return (pat, expr)
89 _ -> na "rule_Comprehension_Flatten"
90 m <- match opFlatten expr
91 indexDoms <- indexDomainsOf m
92 forM_ indexDoms $ \case
93 DomainAny{} -> na "rule_Comprehension_Flatten"
94 _ -> return ()
95 when (null indexDoms) $ na "rule_Comprehension_Flatten"
96 return
97 ( "Comprehension on a matrix flatten"
98 , do
99 (gens, is) <- unzip <$> sequence
100 [ do
101 (iPat, i) <- quantifiedVar
102 return (Generator (GenDomainNoRepr iPat d), i)
103 | d <- indexDoms
104 ]
105 return $ Comprehension body
106 $ gocBefore
107 ++ gens
108 ++ [ ComprehensionLetting pat (make opMatrixIndexing m is) ]
109 ++ gocAfter
110 )
111 theRule _ = na "rule_Comprehension_Flatten"
112
113
114 -- | input: [ i | i <- m[j] ] with m = [a,b,c]
115 -- output: [ [ i | i <- a ]
116 -- , [ i | i <- b ]
117 -- , [ i | i <- c ]
118 -- ][j]
119 -- namely: [ [ m[k]
120 -- | k : int(1..3)
121 -- ]
122 -- , [ i | i <- b ]
123 -- , [ i | i <- c ]
124 -- ][j]
125
126 rule_ModifierAroundIndexedMatrixLiteral :: Rule
127 rule_ModifierAroundIndexedMatrixLiteral = "modifier-around-indexed-matrix-literal" `namedRule` theRule where
128 theRule p = do
129 (mkM, p2) <- match opModifier p
130 (matrix, indices) <- match opMatrixIndexing p2
131 case match opMatrixIndexing p of
132 Nothing -> return ()
133 Just{} -> na "rule_ModifierAroundIndexedMatrixLiteral, no modifier"
134 let
135 fullyMatrixLiteral 0 _ = return True
136 fullyMatrixLiteral n m =
137 case match matrixLiteral m of
138 Nothing -> return False
139 Just (_, _, elems) -> and <$> mapM (fullyMatrixLiteral (n-1)) elems
140 True <- fullyMatrixLiteral (length indices) matrix
141 return
142 ( "Pushing a modifier inwards, through a matrix literal"
143 , do
144 matrix' <- onMatrixLiteral Nothing (return . mkM) matrix
145 return $ make opMatrixIndexing matrix' indices
146 )
147
148
149 rule_Comprehension_LiteralIndexed :: Rule
150 rule_Comprehension_LiteralIndexed = "matrix-comprehension-literal-indexed" `namedRule` theRule where
151 theRule (Comprehension body gensOrConds) = do
152 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
153 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
154 _ -> na "rule_Comprehension_LiteralIndexed"
155 tyExpr <- typeOf expr
156 (matrix, indices) <- match opMatrixIndexing expr
157 (_, _index, elems) <- match matrixLiteral matrix
158 return
159 ( "Vertical rule for matrix-comprehension on matrix literal"
160 , case indices of
161 [] -> bug "rule_Comprehension_LiteralIndexed indices=[]"
162 [index] ->
163 return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
164 (mkDomainIntB 1 (fromInt $ genericLength elems))
165 [ Comprehension body
166 $ gocBefore
167 ++ [ Generator (GenInExpr pat el)
168 , Condition [essence| &num = &index |]
169 ]
170 ++ gocAfter
171 | (num', el') <- zip [1..] elems
172 , let num = fromInt num'
173 -- let's not lose the type information for empty collections
174 , let el = if emptyCollectionX el'
175 then case el' of Typed{} -> el'
176 _ -> Typed el' tyExpr
177 else el'
178 ]
179 (index:rest) ->
180 return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
181 (mkDomainIntB 1 (fromInt $ genericLength elems))
182 [ Comprehension body
183 $ gocBefore
184 ++ [ Generator (GenInExpr pat (make opMatrixIndexing el rest))
185 , Condition [essence| &num = &index |]
186 ]
187 ++ gocAfter
188 | (num', el') <- zip [1..] elems
189 , let num = fromInt num'
190 -- let's not lose the type information for empty collections
191 , let el = if emptyCollectionX el'
192 then case el' of Typed{} -> el'
193 _ -> Typed el' tyExpr
194 else el'
195 ]
196 )
197 theRule _ = na "rule_Comprehension_LiteralIndexed"
198
199
200 rule_Comprehension_ToSet_Matrix :: Rule
201 rule_Comprehension_ToSet_Matrix = "matrix-toSet-matrixInside" `namedRule` theRule where
202 theRule (Comprehension body gensOrConds) = do
203 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
204 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
205 _ -> na "rule_Comprehension_ToSet"
206 matrix <- match opToSet expr
207 TypeMatrix{} <- typeOf matrix
208 -- matrices, except comprehensions
209 case matrix of
210 Comprehension{} -> na "rule_Comprehension_ToSet"
211 _ -> return ()
212 let upd val old = lambdaToFunction pat old val
213 return
214 ( "Vertical rule for comprehension over matrix-toSet, matrix inside"
215 , do
216 (iPat, i) <- quantifiedVar
217 let val = make opIndexing i 1
218 let over = make opHist matrix
219 return $ Comprehension (upd val body)
220 $ gocBefore
221 ++ [Generator (GenInExpr iPat over)]
222 ++ transformBi (upd val) gocAfter
223 )
224 theRule _ = na "rule_Comprehension_ToSet"
225
226
227 rule_Comprehension_ToSet_List :: Rule
228 rule_Comprehension_ToSet_List = "matrix-toSet-listInside" `namedRule` theRule where
229 theRule p = do
230 -- we cannot assume that the list is duplicate-free
231 (False, Comprehension body gensOrConds) <- match opToSetWithFlag p
232 bodyDomain <- domainOf body
233 let auxDomain = DomainSet () (SetAttr SizeAttr_None) bodyDomain
234 return
235 ( "Vertical rule for comprehension over matrix-toSet, list inside"
236 , do
237 (auxName, aux) <- auxiliaryVar
238 (iPat, i) <- quantifiedVar
239 return $ WithLocals aux $
240 AuxiliaryVars
241 [ Declaration (FindOrGiven LocalFind auxName auxDomain)
242 , SuchThat
243 -- forAll i in list . i in aux
244 [ make opAnd $ Comprehension
245 [essence| &body in &aux |]
246 gensOrConds
247 -- forAll i in aux . exists j in list . i = j
248 , make opAnd $ Comprehension
249 (make opOr (Comprehension [essence| &i = &body |] gensOrConds))
250 [Generator (GenInExpr iPat aux)]
251 ]
252 ]
253 )
254
255
256 rule_Comprehension_ToSet_List_DuplicateFree :: Rule
257 rule_Comprehension_ToSet_List_DuplicateFree = "matrix-toSet-listInside-nodups" `namedRule` theRule where
258 theRule (Comprehension body gensOrConds) = do
259 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
260 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToMSet] expr)
261 _ -> na "rule_Comprehension_ToSet"
262 -- we *can* assume that the list is duplicate-free!
263 (True, list) <- match opToSetWithFlag expr
264 case list of
265 Comprehension{} -> return ()
266 _ -> na "rule_Comprehension_ToSet_List_DuplicateFree"
267 return
268 ( "Vertical rule for comprehension over matrix-toSet, list inside, assumed no duplicates"
269 , return $ Comprehension body
270 $ gocBefore
271 ++ [Generator (GenInExpr pat list)]
272 ++ gocAfter
273 )
274 theRule _ = na "rule_Comprehension_ToSet_List_DuplicateFree"
275
276
277 -- [ i | ... , i <- [ j | ... j ... ], ... i ... ]
278 -- [ j | ... , ... j ..., ... j ... ]
279 rule_Comprehension_Nested :: Rule
280 rule_Comprehension_Nested = "matrix-comprehension-nested" `namedRule` theRule where
281 theRule (Comprehension body gensOrConds) = do
282 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
283 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToMSet] expr)
284 _ -> na "rule_Comprehension_Nested"
285 let
286 extract (isAlias -> Just x) = extract x
287 extract (Comprehension innerBody innerGocs) = return (innerBody, innerGocs)
288 extract _ = na "rule_Comprehension_Nested"
289 (innerBody, innerGocs) <- extract expr
290 let upd val old = lambdaToFunction pat old val
291 let
292 -- update the quantified variable names inside innerBody&innerGocs_ here,
293 -- because they may be shadowed.
294 updateQuantified innerBody_ innerGocs_ = do
295 let olds = concatMap collectOldQuantifiers innerGocs_
296 if null olds
297 then return (innerBody_, innerGocs_)
298 else do
299 oldnews <- forM olds $ \ old -> do
300 (Single new, _) <- quantifiedVar
301 return (old, new)
302 let
303 f :: Name -> Name
304 f nm = fromMaybe nm (lookup nm oldnews)
305 return (transformBi f (innerBody_, innerGocs_))
306
307 collectOldQuantifiers = \case
308 Generator (GenDomainNoRepr pt _) -> universeBi pt
309 Generator (GenDomainHasRepr nm _) -> [nm]
310 Generator (GenInExpr pt _) -> universeBi pt
311 Condition _ -> []
312 ComprehensionLetting pt _ -> universeBi pt
313
314 (innerBody', innerGocs') <- updateQuantified innerBody innerGocs
315 return
316 ( "Nested matrix comprehension"
317 , return $ Comprehension (upd innerBody' body)
318 $ gocBefore
319 ++ innerGocs'
320 ++ transformBi (upd innerBody') gocAfter
321 )
322 theRule _ = na "rule_Comprehension_Nested"
323
324
325 rule_Comprehension_Hist :: Rule
326 rule_Comprehension_Hist = "matrix-hist" `namedRule` theRule where
327 theRule (Comprehension body gensOrConds) = do
328 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
329 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
330 _ -> na "rule_Comprehension_Hist"
331 matrix <- match opHist expr
332 TypeMatrix{} <- typeOf matrix
333 index:_ <- indexDomainsOf matrix
334 let upd val old = lambdaToFunction pat old val
335 return
336 ( "Vertical rule for comprehension over matrix-hist"
337 , do
338 (iPat, i) <- quantifiedVar
339 (jPat, j) <- quantifiedVar
340 let value = [essence| &matrix[&i] |]
341 -- if this is the left-most occurrence of value
342 -- count all
343 -- otherwise, 0
344 count = [essence|
345 sum([ 1 $ number of occurrences of this value in the matrix
346 | &jPat : &index
347 , &matrix[&i] = &matrix[&j]
348 ])
349 |]
350 val = AbstractLiteral $ AbsLitTuple [value, count]
351 appearsBefore = [essence|
352 or([ &matrix[&j] = &matrix[&i]
353 | &jPat : &index
354 , &j < &i
355 ])
356 |]
357 return $ Comprehension (upd val body)
358 $ gocBefore
359 ++ [ Generator (GenDomainNoRepr iPat index)
360 , Condition [essence| ! &appearsBefore |]
361 ]
362 ++ transformBi (upd val) gocAfter
363 )
364 theRule _ = na "rule_Comprehension_Hist"
365
366
367 rule_Matrix_Eq :: Rule
368 rule_Matrix_Eq = "matrix-eq" `namedRule` theRule where
369 theRule p = do
370 (x,y) <- match opEq p
371 TypeMatrix{} <- typeOf x -- TODO: check if x and y have the same arity
372 TypeMatrix{} <- typeOf y
373 indexX:_ <- indexDomainsOf x
374 indexY:_ <- indexDomainsOf y
375 return
376 ( "Horizontal rule for matrix ="
377 , do
378 (iPat, i) <- quantifiedVar
379 (jPat, j) <- quantifiedVar
380 -- avoid generating the index equality constraint, if the indices are literally the same
381 if indexX == indexY
382 then
383 return [essence|
384 (forAll &iPat : &indexX . &x[&i] = &y[&i])
385 |]
386 else
387 return [essence|
388 (forAll &iPat : &indexX . &x[&i] = &y[&i])
389 /\
390 (forAll &iPat : &indexX . exists &jPat : &indexY . &i = &j)
391 /\
392 (forAll &iPat : &indexY . exists &jPat : &indexX . &i = &j)
393 |]
394 )
395
396
397 rule_Matrix_Neq :: Rule
398 rule_Matrix_Neq = "matrix-neq" `namedRule` theRule where
399 theRule p = do
400 (x,y) <- match opNeq p
401 TypeMatrix{} <- typeOf x -- TODO: check if x and y have the same arity
402 TypeMatrix{} <- typeOf y
403 indexX:_ <- indexDomainsOf x
404 indexY:_ <- indexDomainsOf y
405 return
406 ( "Horizontal rule for matrix !="
407 , do
408 (iPat, i) <- quantifiedVar
409 return [essence|
410 (exists &iPat : &indexX . &x[&i] != &y[&i])
411 \/
412 (exists &iPat : &indexY . &x[&i] != &y[&i])
413 |]
414 )
415
416
417
418 -- Predefined ordering must recurse through abstract entries, rather than their
419 -- representations. In particular, Boolean ~<= uses false before true; .<= is
420 -- allowed to use a different, representation-dependent Boolean key.
421 rule_Matrix_TildeOrdering :: Rule
422 rule_Matrix_TildeOrdering = "matrix-tilde-ordering" `namedRule` theRule where
423 theRule p = do
424 (x0, y0, strict) <- case (match opTildeLt p, match opTildeLeq p) of
425 (Just (x, y), _) -> return (x, y, True)
426 (_, Just (x, y)) -> return (x, y, False)
427 _ -> na "rule_Matrix_TildeOrdering"
428 let x = followAliases id x0
429 y = followAliases id y0
430 tx <- typeOf x
431 ty <- typeOf y
432 unless (matrixNumDims tx > 0 && matrixNumDims ty > 0) $
433 na "rule_Matrix_TildeOrdering: expected matrices"
434 -- Check that matrix domains are available while testing applicability.
435 -- Tuple projections and other child expressions may still need rewriting;
436 -- failures here must defer this rule, not abort its selected RuleResult.
437 if isPrimitiveType tx && isPrimitiveType ty
438 then do
439 indicesX <- imageIndices x
440 indicesY <- imageIndices y
441 return
442 ( "Predefined lexicographic ordering of primitive matrices"
443 , do
444 xs <- primitiveVector x tx indicesX
445 ys <- primitiveVector y ty indicesY
446 return $ if strict then [essence| &xs <lex &ys |]
447 else [essence| &xs <=lex &ys |]
448 )
449 else do
450 indexX:_ <- indexDomainsOf x
451 indexY:_ <- indexDomainsOf y
452 return
453 ( "Predefined lexicographic ordering of abstract matrix entries"
454 , if indexX == indexY
455 then sameIndexComparison strict x y indexX
456 else positionalComparison strict x y indexX indexY
457 )
458
459 imageIndices x = case match opTransform x of
460 Just{} -> Just <$> indexDomainsOf x
461 Nothing -> return Nothing
462
463 primitiveVector x ty Nothing = return $ flattenIfNeeded (matrixNumDims ty) x
464 primitiveVector x _ (Just indices) = do
465 -- Read the image at its original coordinates before flattening, so the
466 -- existing transformed-indexing rule can apply inverse index actions.
467 pairs <- forM indices $ \index -> do
468 (pat, i) <- quantifiedVar
469 return (Generator (GenDomainNoRepr pat index), i)
470 return $ Comprehension (make opMatrixIndexing x (map snd pairs)) (map fst pairs)
471
472 sameIndexComparison strict x y index = do
473 (iPat, i) <- quantifiedVar
474 (jPat, j) <- quantifiedVar
475 let less = [essence|
476 exists &iPat : &index .
477 &x[&i] ~< &y[&i] /\
478 (forAll &jPat : &index , &j < &i . &x[&j] = &y[&j])
479 |]
480 if strict
481 then return less
482 else do
483 (kPat, k) <- quantifiedVar
484 return [essence| &less \/ (forAll &kPat : &index . &x[&k] = &y[&k]) |]
485
486 -- Different lengths use the usual lexicographic prefix rule. Enumerating
487 -- indices gives positional access even for shifted index domains. The
488 -- common-domain path above avoids this indirection in symmetry comparisons.
489 positionalComparison strict x y indexX indexY = do
490 (aPat, a) <- quantifiedVar
491 (bPat, b) <- quantifiedVar
492 let indicesX = Comprehension a [Generator (GenDomainNoRepr aPat indexX)]
493 indicesY = Comprehension b [Generator (GenDomainNoRepr bPat indexY)]
494 sizeX = make opTwoBars (Domain indexX)
495 sizeY = make opTwoBars (Domain indexY)
496 common = mkDomainIntB 1 [essence| min([&sizeX, &sizeY]) |]
497 atX pos = make opIndexing x (make opIndexing indicesX pos)
498 atY pos = make opIndexing y (make opIndexing indicesY pos)
499 (iPat, i) <- quantifiedVar
500 (jPat, j) <- quantifiedVar
501 (kPat, k) <- quantifiedVar
502 let xi = atX i
503 yi = atY i
504 xj = atX j
505 yj = atY j
506 xk = atX k
507 yk = atY k
508 lengthOrder = if strict then [essence| &sizeX < &sizeY |]
509 else [essence| &sizeX <= &sizeY |]
510 return [essence|
511 (exists &iPat : &common .
512 &xi ~< &yi /\ (forAll &jPat : &common , &j < &i . &xj = &yj))
513 \/ ((forAll &kPat : &common . &xk = &yk) /\ &lengthOrder)
514 |]
515
516 rule_Matrix_Lt_Primitive :: Rule
517 rule_Matrix_Lt_Primitive = "matrix-Lt-primitive" `namedRule` theRule where
518 theRule p = do
519 (x,y) <- match opLt p
520 tx <- typeOf x -- TODO: check if x and y have the same arity
521 ty <- typeOf y
522 unless (matrixNumDims tx > 0 && isPrimitiveType tx) $ failDoc ("not a primitive type:" <+> pretty tx)
523 unless (matrixNumDims ty > 0 && isPrimitiveType ty) $ failDoc ("not a primitive type:" <+> pretty ty)
524 let x' = flattenIfNeeded (matrixNumDims tx) x
525 let y' = flattenIfNeeded (matrixNumDims ty) y
526 return
527 ( "Horizontal rule for matrix <"
528 , return [essence| &x' .< &y' |]
529 )
530
531
532 rule_Matrix_Leq_Primitive :: Rule
533 rule_Matrix_Leq_Primitive = "matrix-Leq-primitive" `namedRule` theRule where
534 theRule p = do
535 (x,y) <- match opLeq p
536 tx <- typeOf x -- TODO: check if x and y have the same arity
537 ty <- typeOf y
538 unless (matrixNumDims tx > 0 && isPrimitiveType tx) $ failDoc ("not a primitive type:" <+> pretty tx)
539 unless (matrixNumDims ty > 0 && isPrimitiveType ty) $ failDoc ("not a primitive type:" <+> pretty ty)
540 let x' = flattenIfNeeded (matrixNumDims tx) x
541 let y' = flattenIfNeeded (matrixNumDims ty) y
542 return
543 ( "Horizontal rule for matrix <="
544 , return [essence| &x' .<= &y' |]
545 )
546
547
548 rule_Matrix_Lt_Decompose :: Rule
549 rule_Matrix_Lt_Decompose = "matrix-Lt-tuple" `namedRule` theRule where
550 theRule p = do
551 (x,y) <- match opLt p
552 tx@TypeMatrix{} <- typeOf x -- TODO: check matrix index & tuple arity
553 ty@TypeMatrix{} <- typeOf y
554 when (isPrimitiveType tx) $ failDoc ("this is a primitive type:" <+> pretty tx)
555 when (isPrimitiveType ty) $ failDoc ("this is a primitive type:" <+> pretty ty)
556 xs <- downX1 x
557 ys <- downX1 y
558 return
559 ( "Horizontal rule for matrix <, decomposing"
560 , return $ decomposeLexLt p xs ys
561 )
562
563
564 rule_Matrix_Leq_Decompose :: Rule
565 rule_Matrix_Leq_Decompose = "matrix-Leq-tuple" `namedRule` theRule where
566 theRule p = do
567 (x,y) <- match opLeq p
568 tx@TypeMatrix{} <- typeOf x -- TODO: check matrix index & tuple arity
569 ty@TypeMatrix{} <- typeOf y
570 when (isPrimitiveType tx) $ failDoc ("this is a primitive type:" <+> pretty tx)
571 when (isPrimitiveType ty) $ failDoc ("this is a primitive type:" <+> pretty ty)
572 xs <- downX1 x
573 ys <- downX1 y
574 return
575 ( "Horizontal rule for matrix <=, decomposing"
576 , return $ decomposeLexLeq p xs ys
577 )
578
579
580 rule_Comprehension_SingletonDomain :: Rule
581 rule_Comprehension_SingletonDomain = "matrix-comprehension-singleton-domain" `namedRule` theRule where
582 theRule (Comprehension body gensOrConds) = do
583 (gocBefore, (pat, singleVal), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
584 Generator (GenDomainHasRepr patName (singletonDomainInt -> Just a)) -> return (Single patName, a)
585 _ -> na "rule_Comprehension_SingletonDomain"
586 let upd val old = lambdaToFunction pat old val
587 return
588 ( "Removing matrix-comprehension of a singleton int domain"
589 , return $
590 if null gocBefore && null gocAfter
591 then AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 1) [upd singleVal body]
592 else Comprehension (upd singleVal body)
593 $ gocBefore
594 ++ transformBi (upd singleVal) gocAfter
595 )
596 theRule _ = na "rule_Comprehension_SingletonDomain"
597
598
599 rule_Comprehension_Singleton :: Rule
600 rule_Comprehension_Singleton = "matrix-comprehension-singleton" `namedRule` theRule where
601 theRule p = do
602 (_, _, _mkQuan, AbstractLiteral (AbsLitMatrix _ [singleVal])) <- match opReducer p
603 return
604 ( "Removing quantifier of a single item"
605 , return singleVal
606 )
607
608
609 rule_Concatenate_Singleton :: Rule
610 rule_Concatenate_Singleton = "matrix-concatenate-singleton" `namedRule` theRule where
611 theRule p = do
612 AbstractLiteral (AbsLitMatrix _ [singleVal]) <- match opConcatenate p
613 return
614 ( "Removing concatenate of a single item"
615 , return singleVal
616 )
617
618
619 rule_MatrixIndexing :: Rule
620 rule_MatrixIndexing = "matrix-indexing" `namedRule` theRule where
621 theRule p = do
622 (matrix, indexer) <- match opIndexing p
623 (_, DomainInt _ ranges, elems) <- match matrixLiteral matrix
624 indexInts <- rangesInts ranges
625 indexerInt <- intOut "rule_MatrixIndexing" indexer
626 if length indexInts == length elems
627 then
628 case lookup indexerInt (zip indexInts elems) of
629 Nothing -> na "rule_MatrixIndexing"
630 Just v ->
631 return
632 ( "Matrix indexing"
633 , return v
634 )
635 else na "rule_MatrixIndexing"
636
637
638 rule_IndexingIdentical :: Rule
639 rule_IndexingIdentical = "matrix-indexing-identical" `namedRule` theRule where
640 theRule p = do
641 (matrix, indexer) <- match opIndexing p
642 (_, indexDomain, firstElem:restElems) <- match matrixLiteral matrix
643 indexerDomain <- domainOf indexer
644 if indexDomain == forgetRepr indexerDomain && all (firstElem==) restElems
645 then return
646 ( "rule_IndexingIdentical"
647 , return firstElem
648 )
649 else na "rule_IndexingIdentical"
650
651
652 rule_ExpandSlices :: Rule
653 rule_ExpandSlices = "matrix-expand-slices" `namedRule` theRule where
654 theRule p = do
655 let
656 flattenSlicingMultiD =
657 case match opFlatten p >>= match opMatrixIndexingSlicing of
658 Just (m, is)
659 | countSlices is > 1 -> return (m, is)
660 _ -> Nothing
661 slicing1D =
662 case match opMatrixIndexingSlicing p of
663 Just (m, is)
664 | countSlices is == 1 -> return (m, is)
665 _ -> Nothing
666 countSlices is =
667 length [ () | Right _ <- is ]
668 (m, is) <- case flattenSlicingMultiD <|> slicing1D of
669 Just (m, is) -> return (m, is)
670 _ -> na "rule_ExpandSlices"
671 indexDoms <- indexDomainsOf m
672 unless (length is == length indexDoms) $ na "rule_ExpandSlices"
673 (is', gocs) <- unzip <$> sequence
674 [ case index of
675 Left i -> -- indexing
676 return
677 ( Left i
678 , []
679 )
680 Right (mLowerBound, mUpperBound) -> do -- slicing
681 (jPat, j) <- quantifiedVar
682 return
683 ( Left j
684 , concat [ [ Generator (GenDomainNoRepr jPat indexDom) ]
685 , [ Condition [essence| &j >= &lb |] | Just lb <- [mLowerBound] ]
686 , [ Condition [essence| &j <= &ub |] | Just ub <- [mUpperBound] ]
687 ]
688 )
689 | (index, indexDom) <- zip is indexDoms
690 ]
691 when (null gocs) $ na "rule_ExpandSlices: this was all indexing and no slicing"
692 return ( "Expanding a matrix slice"
693 , return $ Comprehension (make opMatrixIndexingSlicing m is') (concat gocs)
694 )
695
696
697 -- freq(matrix,arg) ~~> sum([ toInt(arg = i) | i in matrix ])
698 rule_Freq :: Rule
699 rule_Freq = "matrix-freq" `namedRule` theRule where
700 theRule p = do
701 (m, arg) <- match opFreq p
702 TypeMatrix{} <- typeOf m
703 [indexDom] <- indexDomainsOf m
704 return
705 ( "Horizontal rule for matrix-freq."
706 , do
707 (iPat, i) <- quantifiedVar
708 let mis = (make opMatrixIndexing m [i])
709 return $ make opSum $ Comprehension [essence| toInt(&mis = &arg) |]
710 [Generator (GenDomainNoRepr iPat indexDom)]
711 )