never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Transform (rules_Transform) where
4
5 import Conjure.Rules.Import
6
7 -- import Conjure.Rules.Vertical.Variant (onTagged)
8
9 rules_Transform :: [Rule]
10 rules_Transform =
11 [ rule_Transform_DisjointPermutations,
12 rule_Transform_DotLess_matrix,
13 rule_Transform_DotLess_function,
14 rule_Transform_DotLess_set,
15 rule_Transform_DotLess_relation,
16 -- rule_Transform_Sequence_Literal,
17 rule_Transform_FunctionImage,
18 rule_Transform_Tuple,
19 rule_Transform_Matrix_Literal,
20 rule_Transform_Functorially,
21 rule_Transform_Comprehension,
22 rule_Transform_Product_Types,
23 rule_Transform_Matrix,
24 rule_Transform_Partition,
25 rule_Transform_Sequence,
26 rule_Transform_Sequence_Defined,
27 rule_Transformed_Indexing,
28 rule_Lift_Transformed_Indexing,
29 rule_Transform_Indexing,
30 rule_TransformToImage,
31 rule_Transform_Unifying
32 -- rule_Transform_Variant_Literal,
33 -- rule_Transform_Variant_Eq,
34 -- rule_Transform_Variant_Neq,
35 -- rule_Transform_Variant_Lt,
36 -- rule_Transform_Variant_Leq,
37 -- rule_Transformed_Variant_Index,
38 -- rule_Transformed_Variant_Active
39 ]
40
41
42 -- Actions on distinct types commute. Lower them one at a time so the existing
43 -- comprehension rule can preserve each domain's inverse-index substitution.
44 rule_Transform_DisjointPermutations :: Rule
45 rule_Transform_DisjointPermutations = "transform-disjoint-permutations" `namedRule` theRule where
46 theRule (match opTransform -> Just (ps, x)) | length ps > 1 = do
47 domains <- forM ps $ \p -> do
48 TypePermutation d <- typeOf p
49 return d
50 let distinct = and [not (let ?typeCheckerMode = StronglyTyped in typesUnify [a,b])
51 | (i,a) <- zip [0 :: Int ..] domains
52 , (j,b) <- zip [0 :: Int ..] domains, i < j]
53 unless distinct $ na "transform-disjoint-permutations: overlapping types"
54 return ("Apply commuting actions on distinct types",
55 return $ foldr (\p v -> make opTransform [p] v) x ps)
56 theRule _ = na "rule_Transform_DisjointPermutations"
57
58
59 rule_Transform_DotLess_matrix :: Rule
60 rule_Transform_DotLess_matrix = "transform-dotless" `namedRule` theRule
61 where
62 theRule p
63 | Just (x, rhs) <- match opDotLeq p <|> match opDotLt p,
64 Just (ps, y) <- match opTransform rhs = do
65 let mk = case match opDotLeq p of Just _ -> make opDotLeq; Nothing -> make opDotLt
66 ty_x <- typeOf x
67 xIndices <- case ty_x of
68 TypeMatrix {} -> indexDomainsOf x
69 TypeList {} ->
70 case x of
71 Comprehension _ [Generator (GenDomainHasRepr _ d)] -> return [forgetRepr d]
72 _ -> na "rule_Transform_DotLess_matrix"
73 _ -> na "rule_Transform_DotLess_matrix"
74 case xIndices of
75 [xInd] ->
76 return
77 ( "",
78 do
79 (iPat, i) <- quantifiedVar
80 let transformed_i = make opTransform (map (make opPermInverse) ps) i
81 let transformed_y_i = make opTransform ps [essence| &y[&transformed_i] |]
82 return $ mk x [essence| [ &transformed_y_i | &iPat : &xInd ] |]
83 )
84 [xInd1, xInd2] ->
85 return
86 ( "",
87 do
88 (iPat1, i1) <- quantifiedVar
89 (iPat2, i2) <- quantifiedVar
90 let transformed_i1 = make opTransform (map (make opPermInverse) ps) i1
91 let transformed_i2 = make opTransform (map (make opPermInverse) ps) i2
92 let transformed_y_i1_i2 = make opTransform ps [essence| &y[&transformed_i1, &transformed_i2] |]
93 return
94 $ mk
95 [essence| [ &x[&i1, &i2] | &iPat1 : &xInd1 , &iPat2 : &xInd2 ] |]
96 [essence| [ &transformed_y_i1_i2 | &iPat1 : &xInd1 , &iPat2 : &xInd2 ] |]
97 )
98 _ -> na "rule_Transform_DotLess"
99 theRule _ = na "rule_Transform_DotLess"
100
101 rule_Transform_DotLess_function :: Rule
102 rule_Transform_DotLess_function = "transform-dotless-function" `namedRule` theRule
103 where
104 theRule p
105 | Just (x, rhs) <- match opDotLeq p <|> match opDotLt p,
106 Just (ps, y) <- match opTransform rhs,
107 x == y = do
108 let mk :: Expression -> Expression -> Expression = case match opDotLeq p of Just _ -> make opDotLeq; Nothing -> make opDotLt
109 TypeFunction {} <- typeOf x
110 domain_x@(DomainFunction _ _ _fr _to) <- domainOf x
111
112 return
113 ( "",
114 do
115 (auxName, x') <- auxiliaryVar
116 (iPat, i) <- quantifiedVar
117
118 let lhs1_inner = make opTransform ps [essence| &i[1] |]
119 let lhs1 = make opImage x' lhs1_inner
120 let rhs1 = make opTransform ps [essence| &i[2] |]
121
122 let lhs2_inner = make opTransform (map (make opPermInverse) ps) [essence| &i[1] |]
123 let lhs2 = make opImage x lhs2_inner
124 let rhs2 = make opTransform (map (make opPermInverse) ps) [essence| &i[2] |]
125
126 return
127 $ WithLocals
128 (mk x x')
129 ( AuxiliaryVars
130 [ Declaration (FindOrGiven LocalFind auxName domain_x),
131 SuchThat
132 [ [essence| forAll &iPat in &x . &lhs1 = &rhs1 |],
133 [essence| forAll &iPat in &x' . &lhs2 = &rhs2 |]
134 ]
135 ]
136 )
137 )
138 -- na ""
139
140 -- x : function T --> U
141 -- x' : function T --> U
142 -- such that forAll (t,u) in x . x'(transform(ps, t)) = transform(ps, u)
143 -- such that forAll (t,u) in x' . x(transform(permInverse(ps), t)) = transform(permInverse(ps), u)
144
145 -- x: set/mset/func...
146 -- forAll i : innerDomainOf(x) . INSIDE-LHS = INSIDE-RHS
147
148 -- INSIDE-LHS
149 -- set: i in x
150 -- mset: freq(i, x)
151 -- function: i in x -- same as (x[i[0]] = i[1])
152 -- partition: i in parts(x)
153
154 -- INSIDE-RHS
155 -- set: transform(ps, i) in x'
156 -- mset: freq(transform(ps, i), x')
157 -- function: transform(ps, i) in x'
158 -- relation: same as func
159 -- partition: transform(ps, i) in parts(x')
160
161 -- x, x' : set of T
162 -- set: forAll i : . i in x <-> transform(ps, i) in x'
163 -- mset: forAll i : T . i in x <-> transform(ps, i) in x'
164
165 -- such that forAll t in x . transform(ps, t) in x'
166 -- such that forAll t in x' . transform(permInverse(ps), t) in x
167
168 -- x, x' : mset of T
169 -- such that forAll t in x . freq(transform(ps, t), x') = freq(t, x)
170 -- such that forAll t in x' . freq(transform(permInverse(ps), t), x) = freq(t, x')
171
172 -- x, x' : relation (A,B,C)
173 -- such that forAll entry in x . transform(ps, entry) in x'
174 -- such that forAll entry in x' . transform(permInverse(ps), entry) in x
175
176 -- x, x' : partition of set of T
177 -- such that forAll i1, i2 : set of T . together({i1, i2}, x) <-> together({transform(ps, x), transform(ps, y)}, x')
178
179 theRule _ = na "rule_Transform_DotLess"
180
181 rule_Transform_DotLess_set :: Rule
182 rule_Transform_DotLess_set = "transform-dotless-set" `namedRule` theRule
183 where
184 theRule p
185 | Just (x, rhs) <- match opDotLeq p <|> match opDotLt p,
186 Just (ps, y) <- match opTransform rhs,
187 x == y = do
188 let mk :: Expression -> Expression -> Expression = case match opDotLeq p of Just _ -> make opDotLeq; Nothing -> make opDotLt
189 TypeSet {} <- typeOf x
190 domain_x@DomainSet {} <- domainOf x
191
192 return
193 ( "",
194 do
195 (auxName, x') <- auxiliaryVar
196 (iPat, i) <- quantifiedVar
197
198 let transform_i = make opTransform ps i
199 let transform_i' = make opTransform (map (make opPermInverse) ps) i
200
201 return
202 $ WithLocals
203 (mk x x')
204 ( AuxiliaryVars
205 [ Declaration (FindOrGiven LocalFind auxName domain_x),
206 SuchThat
207 [ [essence| forAll &iPat in &x . &transform_i in &x' |],
208 [essence| forAll &iPat in &x' . &transform_i' in &x |]
209 ]
210 ]
211 )
212 )
213 theRule _ = na "rule_Transform_DotLess"
214
215 rule_Transform_DotLess_relation :: Rule
216 rule_Transform_DotLess_relation = "transform-dotless-relation" `namedRule` theRule
217 where
218 theRule p
219 | Just (x, rhs) <- match opDotLeq p <|> match opDotLt p,
220 Just (ps, y) <- match opTransform rhs,
221 x == y = do
222 let mk :: Expression -> Expression -> Expression = case match opDotLeq p of Just _ -> make opDotLeq; Nothing -> make opDotLt
223 TypeRelation {} <- typeOf x
224 domain_x@DomainRelation {} <- domainOf x
225
226 return
227 ( "",
228 do
229 (auxName, x') <- auxiliaryVar
230 (iPat, i) <- quantifiedVar
231
232 let transform_i = make opTransform ps i
233 let transform_i' = make opTransform (map (make opPermInverse) ps) i
234
235 return
236 $ WithLocals
237 (mk x x')
238 ( AuxiliaryVars
239 [ Declaration (FindOrGiven LocalFind auxName domain_x),
240 SuchThat
241 [ [essence| forAll &iPat in &x . &transform_i in &x' |],
242 [essence| forAll &iPat in &x' . &transform_i' in &x |]
243 ]
244 ]
245 )
246 )
247 theRule _ = na "rule_Transform_DotLess"
248
249 -- transform(p, x)[i] ~~> transform(p, x[transform(permInverse(p), i)])
250 -- transform(p, f)[x] ~~> transform(p, f[transform(permInverse(p), x)])
251 -- image(transform(p, f), x) ~~> transform(p, image(f, transform(permInverse(p), x)))
252 rule_Transform_FunctionImage :: Rule
253 rule_Transform_FunctionImage = "transform-function-image" `namedRule` theRule
254 where
255 theRule [essence| image(transform([&p], &f), &x) |] = do
256 return ("", return [essence| transform([&p], image(&f, transform([permInverse(&p)], &x))) |])
257 theRule _ = na "rule_Transform_FunctionImage"
258
259 -- transform(p, x)[i] ~~> transform(p, x[transform(permInverse(p), i)])
260 -- transform(p, f)[x] ~~> transform(p, f[transform(permInverse(p), x)])
261 -- image(transform(p, f), x) ~~> transform(p, image(f, transform(permInverse(p), x)))
262 rule_Transform_Tuple :: Rule
263 rule_Transform_Tuple = "transform-tuple" `namedRule` theRule
264 where
265 theRule p
266 | Just (ps, tup) <- match opTransform p,
267 Just (TypeTuple tup_types) <- typeOf tup =
268 return
269 ( "",
270 return
271 $ AbstractLiteral
272 $ AbsLitTuple
273 [ make opTransform ps [essence| &tup[&i] |]
274 | iInt <- take (length tup_types) allNats,
275 let i = fromInt iInt
276 ]
277 )
278 theRule _ = na "rule_Transform_Tuple"
279
280 -- transform(p, [a, b, c]) ~~> [transform(p, a), transform(p, b), transform(p, c)]
281 -- Only valid when the index domain of the matrix is untouched by the morphisms,
282 -- otherwise the entries would have to be reordered as well.
283 rule_Transform_Matrix_Literal :: Rule
284 rule_Transform_Matrix_Literal = "transform-matrix-literal" `namedRule` theRule
285 where
286 theRule p = do
287 (morphisms, x) <- match opTransform p
288 (index, elems) <- case x of
289 AbstractLiteral (AbsLitMatrix index elems) -> return (index, elems)
290 _ -> na "rule_Transform_Matrix_Literal"
291 TypeMatrix tyIndex _ <- typeOf x
292 forM_ morphisms $ \morphism -> do
293 inn <- morphing =<< typeOf morphism
294 when (let ?typeCheckerMode = StronglyTyped in tyIndex `containsType` inn)
295 $ na "rule_Transform_Matrix_Literal"
296 return
297 ( "Horizontal rule for transform of a matrix literal",
298 return
299 $ AbstractLiteral
300 $ AbsLitMatrix index
301 $ [make opTransform morphisms e | e <- elems]
302 )
303
304 rule_Transform_Functorially :: Rule
305 rule_Transform_Functorially = "transform-functorially" `namedRule` theRule
306 where
307 theRule (Comprehension body gensOrConds) = do
308 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \case
309 Generator (GenInExpr (Single pat) expr) ->
310 return (pat, matchDefs [opToSet, opToMSet] expr)
311 _ -> na "rule_Transform_Functorially"
312 (morphisms, y) <- match opTransform x
313 return
314 ( "Horizontal rule for transform of functorially",
315 do
316 (dPat, d) <- quantifiedVar
317 return
318 ( Comprehension body
319 $ gocBefore
320 ++ [Generator (GenInExpr dPat y)]
321 ++ ( ComprehensionLetting
322 (Single pat)
323 (make opTransform morphisms d)
324 : gocAfter
325 )
326 )
327 )
328 theRule _ = na "rule_Transform_Functorially"
329
330 rule_Transform_Comprehension :: Rule
331 rule_Transform_Comprehension = "transform-comprehension" `namedRule` theRule
332 where
333 theRule x = do
334 ([morphism], cmp@(Comprehension body gensOrConds)) <- match opTransform x
335 ty <- typeOf cmp
336 inn <- morphing =<< typeOf morphism
337 -- A comprehension over a domain is a matrix indexed by that domain, and the image
338 -- of a matrix m under a permutation p is [ p(m[permInverse(p)(i)]) | i : indexDom ].
339 -- So the quantified index has to be mapped back through the *inverse* morphism,
340 -- while everything else is mapped forwards. Getting this wrong permutes the entries
341 -- of the result into the wrong order, which is invisible for set-like uses but
342 -- silently wrong under .<= / <=lex.
343 morphismInv <-
344 if any isDomainGenerator gensOrConds
345 then do
346 TypePermutation {} <- typeOf morphism
347 return [essence| permInverse(&morphism) |]
348 else return morphism
349 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
350 then
351 return
352 ( "Horizontal rule for transform comprehension",
353 do
354 gox <- mapM (transformOverGenOrCond morphism morphismInv) gensOrConds
355 return $ Comprehension [essence| transform([&morphism], &body) |] (join gox)
356 )
357 else na "rule_Transform_Comprehension"
358
359 isDomainGenerator (Generator GenDomainHasRepr {}) = True
360 isDomainGenerator (Generator GenDomainNoRepr {}) = True
361 isDomainGenerator _ = False
362
363 transformOverGenOrCond m mInv (Generator g) = transformOverGenerator m mInv g
364 transformOverGenOrCond m _ (Condition e) =
365 return [Condition [essence| transform([&m], &e) |]]
366 transformOverGenOrCond m _ (ComprehensionLetting pat e) =
367 return [ComprehensionLetting pat [essence| transform([&m], &e) |]]
368
369 transformOverGenerator _ mInv (GenDomainHasRepr a d) = do
370 (Single nm, n) <- quantifiedVarOverDomain $ forgetRepr d
371 return
372 [ Generator (GenDomainHasRepr nm d),
373 ComprehensionLetting (Single a) [essence| transform([&mInv], &n) |]
374 ]
375 transformOverGenerator m _ (GenInExpr a e) =
376 return [Generator (GenInExpr a [essence| transform([&m], &e) |])]
377 transformOverGenerator _ mInv (GenDomainNoRepr absPat d) = do
378 (rPat, ns) <- clonePattern absPat
379 return
380 $ Generator (GenDomainNoRepr rPat d)
381 : ( ( \(pat, exp) ->
382 ComprehensionLetting (Single pat) [essence| transform([&mInv], &exp) |]
383 )
384 <$> ns
385 )
386
387 clonePattern (Single name) = do
388 (nPat, n) <- quantifiedVar
389 return (nPat, [(name, n)])
390 clonePattern (AbsPatTuple pats) = do
391 rec <- mapM clonePattern pats
392 return
393 ( AbsPatTuple $ fst <$> rec,
394 snd =<< rec
395 )
396 clonePattern (AbsPatMatrix pats) = do
397 rec <- mapM clonePattern pats
398 return
399 ( AbsPatMatrix $ fst <$> rec,
400 snd =<< rec
401 )
402 clonePattern (AbsPatSet pats) = do
403 rec <- mapM clonePattern pats
404 return
405 ( AbsPatSet $ fst <$> rec,
406 snd =<< rec
407 )
408 clonePattern _ =
409 bug "rule_Transform_Comprehension: clonePattern: unsupported Abstract Pattern"
410
411 rule_Transform_Product_Types :: Rule
412 rule_Transform_Product_Types = "transform-product-types" `namedRule` theRule
413 where
414 theRule [essence| transform([&morphism], &i) |] = do
415 inn <- morphing =<< typeOf morphism
416 ti <- typeOf i
417 if let ?typeCheckerMode = StronglyTyped in ti `containsProductType` inn
418 then case ti of
419 (TypeTuple tint) -> do
420 let tupleIndexTransform indx =
421 let indexexpr = Constant (ConstantInt TagInt indx)
422 in [essence| transform([&morphism], &i[&indexexpr]) |]
423 tupleExpression =
424 AbstractLiteral
425 $ AbsLitTuple (tupleIndexTransform <$> [1 .. (fromIntegral $ length tint)])
426 return
427 ( "Horizontal rule for transform of tuple",
428 return tupleExpression
429 )
430 (TypeRecord namet) -> do
431 let recordIndexTransform indx =
432 let indexexpr =
433 Reference (fst indx)
434 $ Just
435 $ uncurry RecordField indx
436 in (fst indx, [essence| transform([&morphism], &i[&indexexpr]) |])
437 recordExpression =
438 AbstractLiteral
439 $ AbsLitRecord
440 $ recordIndexTransform
441 <$> namet
442 return
443 ( "Horizontal rule for transform of record",
444 return recordExpression
445 )
446 _ -> bug "rule_Transform_Product_Types this is a bug"
447 else na "rule_Transform_Product_Types"
448 theRule _ = na "rule_Transform_Product_Types"
449
450 rule_Transform_Matrix :: Rule
451 rule_Transform_Matrix = "transform-matrix" `namedRule` theRule
452 where
453 theRule (Comprehension body gensOrConds) = do
454 (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \case
455 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
456 _ -> na "rule_Transform_Matrix"
457 ([morphism], matexp) <- match opTransform exp
458 DomainMatrix domIndx _ <- domainOf matexp
459 ty <- typeOf matexp
460 inn <- morphing =<< typeOf morphism
461 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
462 then
463 return
464 ( "Horizontal rule for transform matrix in comprehension generator",
465 do
466 (dPat, d) <- quantifiedVar
467 (Single mName, m) <- quantifiedVar
468 (Single iName, i) <- quantifiedVar
469 return
470 ( Comprehension body
471 $ gocBefore
472 ++ [Generator (GenDomainNoRepr dPat (forgetRepr domIndx))]
473 ++ [ComprehensionLetting (Single iName) [essence| transform([&morphism], &d) |]]
474 ++ [ComprehensionLetting (Single mName) [essence| &matexp[&i] |]]
475 ++ [ComprehensionLetting (Single pat) [essence| transform([&morphism], &m) |]]
476 ++ gocAfter
477 )
478 )
479 else na "rule_Transform_Matrix"
480 theRule _ = na "rule_Transform_Matrix"
481
482 rule_Transform_Partition :: Rule
483 rule_Transform_Partition = "transform-partition" `namedRule` theRule
484 where
485 theRule (Comprehension body gensOrConds) = do
486 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \case
487 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
488 _ -> na "rule_Transform_Partition"
489 z <- match opParts x
490 ([morphism], y) <- match opTransform z
491 ty <- typeOf y
492 case ty of TypePartition {} -> return (); _ -> na "only applies to partitions"
493 inn <- morphing =<< typeOf morphism
494 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
495 then do
496 return
497 ( "Horizontal rule for transform of partition",
498 do
499 (dPat, d) <- quantifiedVar
500 return
501 ( Comprehension body
502 $ gocBefore
503 ++ [Generator (GenInExpr dPat [essence| parts(&y) |])]
504 ++ (ComprehensionLetting (Single pat) [essence| transform([&morphism], &d) |] : gocAfter)
505 )
506 )
507 else na "rule_Transform_Partition"
508 theRule _ = na "rule_Transform_Partition"
509
510 rule_Transform_Sequence :: Rule
511 rule_Transform_Sequence = "transform-sequence" `namedRule` theRule
512 where
513 theRule (Comprehension body gensOrConds) = do
514 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \case
515 Generator (GenInExpr (Single pat) expr) ->
516 return (pat, matchDefs [opToSet, opToMSet] expr)
517 _ -> na "rule_Transform_Sequence"
518 ([morphism], y) <- match opTransform x
519 ty <- typeOf y
520 case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences"
521 inn <- morphing =<< typeOf morphism
522 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
523 then do
524 return
525 ( "Horizontal rule for transform of sequence",
526 do
527 (dPat, d) <- quantifiedVar
528 return
529 ( Comprehension body
530 $ gocBefore
531 ++ [Generator (GenInExpr dPat y)]
532 ++ ( ComprehensionLetting
533 (Single pat)
534 [essence| (&d[1], transform([&morphism], &d[2])) |]
535 : gocAfter
536 )
537 )
538 )
539 else na "rule_Transform_Sequence"
540 theRule _ = na "rule_Transform_Sequence"
541
542 rule_Transform_Sequence_Defined :: Rule
543 rule_Transform_Sequence_Defined = "transform-sequence-defined" `namedRule` theRule
544 where
545 theRule (Comprehension body gensOrConds) = do
546 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \case
547 Generator (GenInExpr pat@Single {} expr) ->
548 return (pat, matchDefs [opToSet, opToMSet] expr)
549 _ -> na "rule_Transform_Sequence_Defined"
550 defi <- match opDefined x
551 ([morphism], y) <- match opTransform defi
552 ty <- typeOf y
553 case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences"
554 inn <- morphing =<< typeOf morphism
555 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
556 then do
557 return
558 ( "Horizontal rule for transform of sequence defined",
559 do
560 return
561 ( Comprehension body
562 $ gocBefore
563 ++ [Generator (GenInExpr pat [essence| defined(&y) |])]
564 ++ gocAfter
565 )
566 )
567 else na "rule_Transform_Sequence_Defined"
568 theRule _ = na "rule_Transform_Sequence_Defined"
569
570 rule_Transformed_Indexing :: Rule
571 rule_Transformed_Indexing = "transformed-indexing" `namedRule` theRule
572 where
573 theRule (Comprehension body gensOrConds) = do
574 (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \case
575 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
576 _ -> na "rule_Transformed_Indexing"
577 (matexp, indexer) <- match opIndexing exp
578 TypeMatrix {} <- typeOf matexp
579 ([morphism], mat) <- match opTransform matexp
580 ty <- typeOf mat
581 inn <- morphing =<< typeOf morphism
582 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
583 then do
584 return
585 ( "Horizontal rule for transformed indexing",
586 do
587 (Single mName, m) <- quantifiedVar
588 return
589 ( Comprehension body
590 $ gocBefore
591 ++ [ComprehensionLetting (Single mName) [essence| &matexp[&indexer] |]]
592 ++ [ComprehensionLetting (Single pat) [essence| transform([&morphism], &m) |]]
593 ++ gocAfter
594 )
595 )
596 else na "rule_Transformed_Indexing"
597 theRule _ = na "rule_Transformed_Indexing"
598
599 rule_Lift_Transformed_Indexing :: Rule
600 rule_Lift_Transformed_Indexing = "lift-transformed-indexing" `namedRule` theRule
601 where
602 theRule [essence| transform([&p], &x)[&i] |] = do
603 TypePermutation {} <- typeOf p
604 tx <- typeOf x
605 index <- case tx of
606 -- Tuple positions and record fields are structural selectors, not
607 -- values in the permuted domain. They must remain constant.
608 TypeTuple{} -> return i
609 TypeRecord{} -> return i
610 TypeMatrix{} -> return [essence| transform([permInverse(&p)], &i) |]
611 TypeList{} -> return [essence| transform([permInverse(&p)], &i) |]
612 _ -> na "lift-transformed-indexing: unsupported container"
613 return
614 ( "transformed indexing",
615 return [essence| transform([&p], &x[&index]) |]
616 )
617 theRule _ = na "rule_Lift_Transformed_Indexing"
618
619 rule_Transform_Indexing :: Rule
620 rule_Transform_Indexing = "transform-indexing" `namedRule` theRule
621 where
622 theRule (Comprehension body gensOrConds) = do
623 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
624 Generator (GenInExpr pat expr) -> return (pat, expr)
625 _ -> na "rule_Transform_Indexing"
626 ([morphism], matexp) <- match opTransform expr
627 (mat, indexer) <- match opIndexing matexp
628 TypeMatrix {} <- typeOf mat
629 ty <- typeOf mat
630 inn <- morphing =<< typeOf morphism
631 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
632 then do
633 return
634 ( "Horizontal rule for transform indexing",
635 do
636 (Single mName, m) <- quantifiedVar
637 (Single iName, i) <- quantifiedVar
638 return
639 ( Comprehension body
640 $ gocBefore
641 ++ [ComprehensionLetting (Single iName) [essence| transform([&morphism], &indexer) |]]
642 ++ [ComprehensionLetting (Single mName) [essence| &mat[&i] |]]
643 ++ [Generator (GenInExpr pat [essence| transform([&morphism], &m) |])]
644 ++ gocAfter
645 )
646 )
647 else na "rule_Transform_Indexing"
648 theRule _ = na "rule_Transform_Indexing"
649
650 rule_TransformToImage :: Rule
651 rule_TransformToImage = "transform-to-image" `namedRule` theRule
652 where
653 -- transform([f], i) ~~> image(f, i) if the types match
654 theRule [essence| transform([&morphism], &i) |] = do
655 inner <- morphing =<< typeOf morphism
656 typeI <- typeOf i
657 if (let ?typeCheckerMode = StronglyTyped in typesUnify [inner, typeI])
658 then
659 return
660 ( "Horizontal rule for transform unifying",
661 return [essence| image(&morphism, &i) |]
662 )
663 else na "rule_Transform_Unifying"
664 theRule _ = na "rule_Transform_Unifying"
665
666 rule_Transform_Unifying :: Rule
667 rule_Transform_Unifying = "transform-unifying" `namedRule` theRule
668 where
669 -- drop transforms that do not apply
670 theRule p | Just (morphisms :: [Expression], i) <- match opTransform p = do
671 typeI <- typeOf i
672 morphisms' <- fmap catMaybes $ forM morphisms $ \morphism -> do
673 inner <- morphing =<< typeOf morphism
674
675 if (let ?typeCheckerMode = StronglyTyped in containsType typeI inner)
676 -- if containsType typeI inner
677 then return (Just morphism)
678 else return Nothing
679 if length morphisms' == length morphisms
680 then na "rule_Transform_Unifying" -- didn't drop anything
681 else
682 if null morphisms'
683 then
684 return
685 ( "Horizontal rule for transform unifying -- none of them apply",
686 return i
687 )
688 else
689 return
690 ( "Horizontal rule for transform unifying -- some of them apply",
691 return $ make opTransform morphisms' i
692 )
693 theRule _ = na "rule_Transform_Unifying"
694
695 -- rule_Transform_Sequence_Literal :: Rule
696 -- rule_Transform_Sequence_Literal = "transform-sequence-literal" `namedRule` theRule
697 -- where
698 -- theRule p = do
699 -- _ <- match opTransform p
700 -- let (x, rx) = matchManyTransforms p
701 -- TypeSequence {} <- typeOf x
702 -- (_, as) <- match sequenceLiteral x
703 -- return
704 -- ( "Horizontal rule for transform sequence literal",
705 -- return $ AbstractLiteral $ AbsLitSequence $ rx <$> as
706 -- )
707
708 -- rule_Transform_Variant_Literal :: Rule
709 -- rule_Transform_Variant_Literal = "transform-variant-literal" `namedRule` theRule
710 -- where
711 -- theRule p = do
712 -- _ <- match opTransform p
713 -- let (x, rx) = matchManyTransforms p
714 -- case x of
715 -- AbstractLiteral (AbsLitVariant d n a) ->
716 -- return
717 -- ( "Horizontal rule for transform variant literal",
718 -- return $ AbstractLiteral $ AbsLitVariant d n $ rx a
719 -- )
720 -- _ -> na "rule_Transform_Variant_Literal"
721
722 -- atLeastOneTransform :: (MonadFailDoc m) => (Expression, Expression) -> m ()
723 -- atLeastOneTransform (l, r) = do
724 -- case (match opTransform l, match opTransform r) of
725 -- (Nothing, Nothing) -> na "no transforms on either side"
726 -- _ -> return ()
727
728 -- matchManyTransforms ::
729 -- Expression ->
730 -- (Expression, Expression -> Expression)
731 -- matchManyTransforms exp =
732 -- case match opTransform exp of
733 -- Nothing -> (exp, id)
734 -- Just ([morphism], so) ->
735 -- let (nexp, ntrans) = matchManyTransforms so
736 -- in ( nexp,
737 -- \x -> let nx = ntrans x in [essence| transform([&morphism], &nx) |]
738 -- )
739 -- _ -> bug "matchManyTransforms"
740
741 -- rule_Transform_Variant_Eq :: Rule
742 -- rule_Transform_Variant_Eq = "transform-variant-eq" `namedRule` theRule
743 -- where
744 -- theRule p = do
745 -- (l, r) <- match opEq p
746 -- atLeastOneTransform (l, r)
747 -- let (x, rx) = matchManyTransforms l
748 -- let (y, ry) = matchManyTransforms r
749 -- TypeVariant {} <- typeOf x
750 -- TypeVariant {} <- typeOf y
751 -- (xWhich : xs) <- downX1 x
752 -- (yWhich : ys) <- downX1 y
753 -- return
754 -- ( "Vertical rule for right transformed variant equality",
755 -- return
756 -- $ make opAnd
757 -- $ fromList
758 -- [ [essence| &xWhich = &yWhich |],
759 -- onTagged (make opEq) xWhich (rx <$> xs) (ry <$> ys)
760 -- ]
761 -- )
762
763 -- rule_Transform_Variant_Neq :: Rule
764 -- rule_Transform_Variant_Neq = "transform-variant-neq" `namedRule` theRule
765 -- where
766 -- theRule p = do
767 -- (l, r) <- match opNeq p
768 -- atLeastOneTransform (l, r)
769 -- let (x, rx) = matchManyTransforms l
770 -- let (y, ry) = matchManyTransforms r
771 -- TypeVariant {} <- typeOf x
772 -- TypeVariant {} <- typeOf y
773 -- (xWhich : xs) <- downX1 x
774 -- (yWhich : ys) <- downX1 y
775 -- return
776 -- ( "Vertical rule for right transformed variant nequality",
777 -- return
778 -- $ make opOr
779 -- $ fromList
780 -- [ [essence| &xWhich != &yWhich |],
781 -- make opAnd
782 -- $ fromList
783 -- [ [essence| &xWhich = &yWhich |],
784 -- onTagged (make opNeq) xWhich (rx <$> xs) (ry <$> ys)
785 -- ]
786 -- ]
787 -- )
788
789 -- rule_Transform_Variant_Lt :: Rule
790 -- rule_Transform_Variant_Lt = "transform-variant-lt" `namedRule` theRule
791 -- where
792 -- theRule p = do
793 -- (l, r) <- match opLt p
794 -- atLeastOneTransform (l, r)
795 -- let (x, rx) = matchManyTransforms l
796 -- let (y, ry) = matchManyTransforms r
797 -- TypeVariant {} <- typeOf x
798 -- TypeVariant {} <- typeOf y
799 -- (xWhich : xs) <- downX1 x
800 -- (yWhich : ys) <- downX1 y
801 -- return
802 -- ( "Vertical rule for right transformed variant less than",
803 -- return
804 -- $ make opOr
805 -- $ fromList
806 -- [ [essence| &xWhich < &yWhich |],
807 -- make opAnd
808 -- $ fromList
809 -- [ [essence| &xWhich = &yWhich |],
810 -- onTagged (make opLt) xWhich (rx <$> xs) (ry <$> ys)
811 -- ]
812 -- ]
813 -- )
814
815 -- rule_Transform_Variant_Leq :: Rule
816 -- rule_Transform_Variant_Leq = "transform-variant-leq" `namedRule` theRule
817 -- where
818 -- theRule p = do
819 -- (l, r) <- match opLeq p
820 -- atLeastOneTransform (l, r)
821 -- let (x, rx) = matchManyTransforms l
822 -- let (y, ry) = matchManyTransforms r
823 -- TypeVariant {} <- typeOf x
824 -- TypeVariant {} <- typeOf y
825 -- (xWhich : xs) <- downX1 x
826 -- (yWhich : ys) <- downX1 y
827 -- return
828 -- ( "Vertical rule for right transformed variant less than eq",
829 -- return
830 -- $ make opOr
831 -- $ fromList
832 -- [ [essence| &xWhich < &yWhich |],
833 -- make opAnd
834 -- $ fromList
835 -- [ [essence| &xWhich = &yWhich |],
836 -- onTagged (make opLeq) xWhich (rx <$> xs) (ry <$> ys)
837 -- ]
838 -- ]
839 -- )
840
841 -- rule_Transformed_Variant_Index :: Rule
842 -- rule_Transformed_Variant_Index = "transformed-variant-index" `namedRule` theRule
843 -- where
844 -- theRule p = do
845 -- (l, arg) <- match opIndexing p
846 -- atLeastOneTransform (l, l)
847 -- let (x, rx) = matchManyTransforms l
848 -- TypeVariant ds <- typeOf x
849 -- (xWhich : xs) <- downX1 x
850 -- name <- nameOut arg
851 -- argInt <-
852 -- case elemIndex name (map fst ds) of
853 -- Nothing -> failDoc "Variant indexing, not a member of the type."
854 -- Just argInt -> return argInt
855 -- return
856 -- ( "Variant indexing on:" <+> pretty p,
857 -- return
858 -- $ WithLocals
859 -- (rx (atNote "Variant indexing" xs argInt))
860 -- ( DefinednessConstraints
861 -- [ [essence| &xWhich = &argInt2 |]
862 -- | let argInt2 = fromInt (fromIntegral (argInt + 1))
863 -- ]
864 -- )
865 -- )
866
867 -- rule_Transformed_Variant_Active :: Rule
868 -- rule_Transformed_Variant_Active = "transformed-variant-active" `namedRule` theRule
869 -- where
870 -- theRule p = do
871 -- (l, name) <- match opActive p
872 -- atLeastOneTransform (l, l)
873 -- let (x, _) = matchManyTransforms l
874 -- TypeVariant ds <- typeOf x
875 -- (xWhich : _) <- downX1 x
876 -- argInt <- case elemIndex name (map fst ds) of
877 -- Nothing -> failDoc "Variant indexing, not a member of the type."
878 -- Just argInt -> return $ fromInt $ fromIntegral $ argInt + 1
879 -- return
880 -- ( "Variant active on:" <+> pretty p,
881 -- return [essence| &xWhich = &argInt |]
882 -- )