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