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