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 import Conjure.Rules.Vertical.Variant (onTagged)
7
8 rules_Transform :: [Rule]
9 rules_Transform =
10 [ rule_Transform_Sequence_Literal,
11 rule_Transform_Functorially,
12 rule_Transform_Comprehension,
13 rule_Transform_Product_Types,
14 rule_Transform_Matrix,
15 rule_Transform_Partition,
16 rule_Transform_Sequence,
17 rule_Transform_Sequence_Defined,
18 rule_Transformed_Indexing,
19 rule_Lift_Transformed_Indexing,
20 rule_Transform_Indexing,
21 rule_Transform_Unifying,
22 rule_Transform_Variant_Literal,
23 rule_Transform_Variant_Eq,
24 rule_Transform_Variant_Neq,
25 rule_Transform_Variant_Lt,
26 rule_Transform_Variant_Leq,
27 rule_Transformed_Variant_Index,
28 rule_Transformed_Variant_Active
29 ]
30
31 rule_Transform_Functorially :: Rule
32 rule_Transform_Functorially = "transform-functorially" `namedRule` theRule
33 where
34 theRule (Comprehension body gensOrConds) = do
35 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
36 Generator (GenInExpr (Single pat) expr) ->
37 return (pat, matchDefs [opToSet, opToMSet] expr)
38 _ -> na "rule_Transform_Functorially"
39 (morphism, y) <- match opTransform x
40 ty <- typeOf y
41 inn <- morphing =<< typeOf morphism
42 if let ?typeCheckerMode = StronglyTyped in ty `containsTypeFunctorially` inn
43 then
44 return
45 ( "Horizontal rule for transform of functorially",
46 do
47 (dPat, d) <- quantifiedVar
48 return
49 ( Comprehension body
50 $ gocBefore
51 ++ [Generator (GenInExpr dPat y)]
52 ++ ( ( ComprehensionLetting
53 (Single pat)
54 [essence|
55 transform(&morphism, &d) |]
56 )
57 : gocAfter
58 )
59 )
60 )
61 else na "rule_Transform_Functorially"
62 theRule _ = na "rule_Transform_Functorially"
63
64 rule_Transform_Comprehension :: Rule
65 rule_Transform_Comprehension = "transform-comprehension" `namedRule` theRule
66 where
67 theRule x = do
68 (morphism, cmp@(Comprehension body gensOrConds)) <- match opTransform x
69 ty <- typeOf cmp
70 inn <- morphing =<< typeOf morphism
71 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
72 then
73 return
74 ( "Horizontal rule for transform comprehension",
75 do
76 gox <- sequence (transformOverGenOrCond morphism <$> gensOrConds)
77 return
78 $ Comprehension
79 [essence| transform(&morphism, &body) |]
80 (join gox)
81 )
82 else na "rule_Transform_Comprehension"
83 transformOverGenOrCond m (Generator g) = transformOverGenerator m g
84 transformOverGenOrCond m (Condition e) =
85 return [Condition [essence| transform(&m,&e) |]]
86 transformOverGenOrCond m (ComprehensionLetting pat e) =
87 return [ComprehensionLetting pat [essence| transform(&m,&e) |]]
88
89 transformOverGenerator m (GenDomainHasRepr a d) = do
90 (Single nm, n) <- quantifiedVarOverDomain $ forgetRepr d
91 return
92 [ Generator (GenDomainHasRepr nm d),
93 ComprehensionLetting (Single a) [essence| transform(&m, &n) |]
94 ]
95 transformOverGenerator m (GenInExpr a e) =
96 return [Generator (GenInExpr a [essence| transform(&m,&e) |])]
97 transformOverGenerator m (GenDomainNoRepr absPat d) = do
98 (rPat, ns) <- clonePattern absPat
99 return
100 $ [Generator (GenDomainNoRepr rPat d)]
101 ++ ( ( \(pat, exp) ->
102 ComprehensionLetting (Single pat) [essence| transform(&m,&exp) |]
103 )
104 <$> ns
105 )
106
107 clonePattern (Single name) = do
108 (nPat, n) <- quantifiedVar
109 return (nPat, [(name, n)])
110 clonePattern (AbsPatTuple pats) = do
111 rec <- sequence (clonePattern <$> pats)
112 return
113 ( AbsPatTuple $ fst <$> rec,
114 join $ snd <$> rec
115 )
116 clonePattern (AbsPatMatrix pats) = do
117 rec <- sequence (clonePattern <$> pats)
118 return
119 ( AbsPatMatrix $ fst <$> rec,
120 join $ snd <$> rec
121 )
122 clonePattern (AbsPatSet pats) = do
123 rec <- sequence (clonePattern <$> pats)
124 return
125 ( AbsPatSet $ fst <$> rec,
126 join $ snd <$> rec
127 )
128 clonePattern _ =
129 bug "rule_Transform_Comprehension: clonePattern: unsupported Abstract Pattern"
130
131 rule_Transform_Product_Types :: Rule
132 rule_Transform_Product_Types = "transform-product-types" `namedRule` theRule
133 where
134 theRule [essence| transform(&morphism, &i) |] = do
135 inn <- morphing =<< typeOf morphism
136 ti <- typeOf i
137 if let ?typeCheckerMode = StronglyTyped in ti `containsProductType` inn
138 then case ti of
139 (TypeTuple tint) -> do
140 let tupleIndexTransform indx =
141 let indexexpr = Constant (ConstantInt TagInt indx)
142 in [essence| transform(&morphism, &i[&indexexpr]) |]
143 tupleExpression =
144 AbstractLiteral
145 $ AbsLitTuple
146 $ (tupleIndexTransform <$> [1 .. (fromIntegral $ length tint)])
147 return
148 ( "Horizontal rule for transform of tuple",
149 return tupleExpression
150 )
151 (TypeRecord namet) -> do
152 let recordIndexTransform indx =
153 let indexexpr =
154 Reference (fst indx)
155 $ Just
156 $ RecordField (fst indx) (snd indx)
157 in (fst indx, [essence| transform(&morphism, &i[&indexexpr]) |])
158 recordExpression =
159 AbstractLiteral
160 $ AbsLitRecord
161 $ (recordIndexTransform <$> namet)
162 return
163 ( "Horizontal rule for transform of record",
164 return recordExpression
165 )
166 _ -> bug "rule_Transform_Product_Types this is a bug"
167 else na "rule_Transform_Product_Types"
168 theRule _ = na "rule_Transform_Product_Types"
169
170 rule_Transform_Matrix :: Rule
171 rule_Transform_Matrix = "transform-matrix" `namedRule` theRule
172 where
173 theRule (Comprehension body gensOrConds) = do
174 (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
175 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
176 _ -> na "rule_Transform_Matrix"
177 (morphism, matexp) <- match opTransform exp
178 DomainMatrix domIndx _ <- domainOf matexp
179 ty <- typeOf matexp
180 inn <- morphing =<< typeOf morphism
181 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
182 then
183 return
184 ( "Horizontal rule for transform matrix in comprehension generator",
185 do
186 (dPat, d) <- quantifiedVar
187 (Single mName, m) <- quantifiedVar
188 (Single iName, i) <- quantifiedVar
189 return
190 ( Comprehension body
191 $ gocBefore
192 ++ [Generator (GenDomainNoRepr dPat (forgetRepr domIndx))]
193 ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &d) |]]
194 ++ [ComprehensionLetting (Single mName) [essence| &matexp[&i] |]]
195 ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]]
196 ++ gocAfter
197 )
198 )
199 else na "rule_Transform_Matrix"
200 theRule _ = na "rule_Transform_Matrix"
201
202 rule_Transform_Partition :: Rule
203 rule_Transform_Partition = "transform-partition" `namedRule` theRule
204 where
205 theRule (Comprehension body gensOrConds) = do
206 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
207 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
208 _ -> na "rule_Transform_Partition"
209 z <- match opParts x
210 (morphism, y) <- match opTransform z
211 ty <- typeOf y
212 case ty of TypePartition {} -> return (); _ -> na "only applies to partitions"
213 inn <- morphing =<< typeOf morphism
214 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
215 then do
216 return
217 ( "Horizontal rule for transform of partition",
218 do
219 (dPat, d) <- quantifiedVar
220 return
221 ( Comprehension body
222 $ gocBefore
223 ++ [Generator (GenInExpr dPat [essence| parts(&y) |])]
224 ++ ((ComprehensionLetting (Single pat) [essence| transform(&morphism, &d) |]) : gocAfter)
225 )
226 )
227 else na "rule_Transform_Partition"
228 theRule _ = na "rule_Transform_Partition"
229
230 rule_Transform_Sequence :: Rule
231 rule_Transform_Sequence = "transform-sequence" `namedRule` theRule
232 where
233 theRule (Comprehension body gensOrConds) = do
234 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
235 Generator (GenInExpr (Single pat) expr) ->
236 return (pat, matchDefs [opToSet, opToMSet] expr)
237 _ -> na "rule_Transform_Sequence"
238 (morphism, y) <- match opTransform x
239 ty <- typeOf y
240 case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences"
241 inn <- morphing =<< typeOf morphism
242 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
243 then do
244 return
245 ( "Horizontal rule for transform of sequence",
246 do
247 (dPat, d) <- quantifiedVar
248 return
249 ( Comprehension body
250 $ gocBefore
251 ++ [Generator (GenInExpr dPat y)]
252 ++ ( ( ComprehensionLetting
253 (Single pat)
254 [essence|
255 (&d[1], transform(&morphism, &d[2])) |]
256 )
257 : gocAfter
258 )
259 )
260 )
261 else na "rule_Transform_Sequence"
262 theRule _ = na "rule_Transform_Sequence"
263
264 rule_Transform_Sequence_Defined :: Rule
265 rule_Transform_Sequence_Defined = "transform-sequence-defined" `namedRule` theRule
266 where
267 theRule (Comprehension body gensOrConds) = do
268 (gocBefore, (pat, x), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
269 Generator (GenInExpr pat@Single {} expr) ->
270 return (pat, matchDefs [opToSet, opToMSet] expr)
271 _ -> na "rule_Transform_Sequence_Defined"
272 defi <- match opDefined x
273 (morphism, y) <- match opTransform defi
274 ty <- typeOf y
275 case ty of TypeSequence {} -> return (); _ -> na "only applies to sequences"
276 inn <- morphing =<< typeOf morphism
277 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
278 then do
279 return
280 ( "Horizontal rule for transform of sequence defined",
281 do
282 return
283 ( Comprehension body
284 $ gocBefore
285 ++ [Generator (GenInExpr pat [essence| defined(&y) |])]
286 ++ gocAfter
287 )
288 )
289 else na "rule_Transform_Sequence_Defined"
290 theRule _ = na "rule_Transform_Sequence_Defined"
291
292 rule_Transformed_Indexing :: Rule
293 rule_Transformed_Indexing = "transformed-indexing" `namedRule` theRule
294 where
295 theRule (Comprehension body gensOrConds) = do
296 (gocBefore, (pat, exp), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
297 Generator (GenInExpr (Single pat) expr) -> return (pat, expr)
298 _ -> na "rule_Transformed_Indexing"
299 (matexp, indexer) <- match opIndexing exp
300 (morphism, mat) <- match opTransform matexp
301 ty <- typeOf mat
302 inn <- morphing =<< typeOf morphism
303 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
304 then do
305 return
306 ( "Horizontal rule for transformed indexing",
307 do
308 (Single mName, m) <- quantifiedVar
309 return
310 ( Comprehension body
311 $ gocBefore
312 ++ [ComprehensionLetting (Single mName) [essence| &matexp[&indexer] |]]
313 ++ [ComprehensionLetting (Single pat) [essence| transform(&morphism, &m) |]]
314 ++ gocAfter
315 )
316 )
317 else na "rule_Transformed_Indexing"
318 theRule _ = na "rule_Transformed_Indexing"
319
320 rule_Lift_Transformed_Indexing :: Rule
321 rule_Lift_Transformed_Indexing = "lift-transformed-indexing" `namedRule` theRule
322 where
323 matchIndexing ::
324 (?typeCheckerMode :: TypeCheckerMode) =>
325 Expression ->
326 Maybe (Expression, Expression, Expression, Expression)
327 matchIndexing exp = do
328 (matexp, indexer) <- match opIndexing exp
329 (morphism, mat) <- match opTransform matexp
330 return (exp, morphism, mat, indexer)
331
332 liftIndexing (exp, morphism, mat, indexer) = do
333 (Single nm, m) <- quantifiedVar
334 return
335 ( (exp, [essence| transform(&morphism, &m) |]),
336 ComprehensionLetting (Single nm) [essence| &mat[&indexer] |]
337 )
338
339 transformBody bdy [] = bdy
340 transformBody bdy ((orig, repl) : rest) =
341 let nbdy =
342 transformBi
343 ( \e ->
344 if e == orig
345 then repl
346 else e
347 )
348 bdy
349 in transformBody nbdy rest
350
351 theRule (Comprehension body gensOrConds) = do
352 let matched = catMaybes [matchIndexing exp | exp <- universeBi body]
353 case matched of
354 [] -> na "rule_Lift_Transformed_Indexing: nothing to lift"
355 _ -> do
356 replacements <- sequence (liftIndexing <$> matched)
357 return
358 ( "Horizontal rule for lift transformed indexing",
359 return
360 ( Comprehension (transformBody body (fst <$> replacements))
361 $ gensOrConds
362 ++ (snd <$> replacements)
363 )
364 )
365 theRule _ = na "rule_Lift_Transformed_Indexing"
366
367 rule_Transform_Indexing :: Rule
368 rule_Transform_Indexing = "transform-indexing" `namedRule` theRule
369 where
370 theRule (Comprehension body gensOrConds) = do
371 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \goc -> case goc of
372 Generator (GenInExpr pat expr) -> return (pat, expr)
373 _ -> na "rule_Transform_Indexing"
374 (morphism, matexp) <- match opTransform expr
375 (mat, indexer) <- match opIndexing matexp
376 ty <- typeOf mat
377 inn <- morphing =<< typeOf morphism
378 if let ?typeCheckerMode = StronglyTyped in ty `containsType` inn
379 then do
380 return
381 ( "Horizontal rule for transform indexing",
382 do
383 (Single mName, m) <- quantifiedVar
384 (Single iName, i) <- quantifiedVar
385 return
386 ( Comprehension body
387 $ gocBefore
388 ++ [ComprehensionLetting (Single iName) [essence| transform(&morphism, &indexer) |]]
389 ++ [ComprehensionLetting (Single mName) [essence| &mat[&i] |]]
390 ++ [Generator (GenInExpr pat [essence| transform(&morphism, &m) |])]
391 ++ gocAfter
392 )
393 )
394 else na "rule_Transform_Indexing"
395 theRule _ = na "rule_Transform_Indexing"
396
397 rule_Transform_Unifying :: Rule
398 rule_Transform_Unifying = "transform-unifying" `namedRule` theRule
399 where
400 theRule [essence| transform(&morphism, &i) |] = do
401 inner <- morphing =<< typeOf morphism
402 typeI <- typeOf i
403 if let ?typeCheckerMode = StronglyTyped in typesUnify [inner, typeI]
404 then
405 return
406 ( "Horizontal rule for transform unifying",
407 return [essence| image(&morphism, &i) |]
408 )
409 else
410 if let ?typeCheckerMode = StronglyTyped in typeI `containsType` inner
411 then na "rule_Transform_Unifying"
412 else
413 return
414 ( "Horizontal rule for transform shortcut",
415 return i
416 )
417 theRule _ = na "rule_Transform_Unifying"
418
419 rule_Transform_Sequence_Literal :: Rule
420 rule_Transform_Sequence_Literal = "transform-sequence-literal" `namedRule` theRule
421 where
422 theRule p = do
423 _ <- match opTransform p
424 let (x, rx) = matchManyTransforms p
425 TypeSequence {} <- typeOf x
426 (_, as) <- match sequenceLiteral x
427 return
428 ( "Horizontal rule for transform sequence literal",
429 return $ AbstractLiteral $ AbsLitSequence $ rx <$> as
430 )
431
432 rule_Transform_Variant_Literal :: Rule
433 rule_Transform_Variant_Literal = "transform-variant-literal" `namedRule` theRule
434 where
435 theRule p = do
436 _ <- match opTransform p
437 let (x, rx) = matchManyTransforms p
438 case x of
439 AbstractLiteral (AbsLitVariant d n a) ->
440 return
441 ( "Horizontal rule for transform variant literal",
442 return $ AbstractLiteral $ AbsLitVariant d n $ rx a
443 )
444 _ -> na "rule_Transform_Variant_Literal"
445
446 atLeastOneTransform :: (MonadFailDoc m) => (Expression, Expression) -> m ()
447 atLeastOneTransform (l, r) = do
448 case (match opTransform l, match opTransform r) of
449 (Nothing, Nothing) -> na "no transforms on either side"
450 _ -> return ()
451
452 matchManyTransforms ::
453 Expression ->
454 (Expression, Expression -> Expression)
455 matchManyTransforms exp =
456 case match opTransform exp of
457 Nothing -> (exp, id)
458 Just (morphism, so) ->
459 let (nexp, ntrans) = matchManyTransforms so
460 in ( nexp,
461 \x -> let nx = ntrans x in [essence| transform(&morphism, &nx) |]
462 )
463
464 rule_Transform_Variant_Eq :: Rule
465 rule_Transform_Variant_Eq = "transform-variant-eq" `namedRule` theRule
466 where
467 theRule p = do
468 (l, r) <- match opEq p
469 atLeastOneTransform (l, r)
470 let (x, rx) = matchManyTransforms l
471 let (y, ry) = matchManyTransforms r
472 TypeVariant {} <- typeOf x
473 TypeVariant {} <- typeOf y
474 (xWhich : xs) <- downX1 x
475 (yWhich : ys) <- downX1 y
476 return
477 ( "Vertical rule for right transformed variant equality",
478 return
479 $ make opAnd
480 $ fromList
481 [ [essence| &xWhich = &yWhich |],
482 onTagged (make opEq) xWhich (rx <$> xs) (ry <$> ys)
483 ]
484 )
485
486 rule_Transform_Variant_Neq :: Rule
487 rule_Transform_Variant_Neq = "transform-variant-neq" `namedRule` theRule
488 where
489 theRule p = do
490 (l, r) <- match opNeq p
491 atLeastOneTransform (l, r)
492 let (x, rx) = matchManyTransforms l
493 let (y, ry) = matchManyTransforms r
494 TypeVariant {} <- typeOf x
495 TypeVariant {} <- typeOf y
496 (xWhich : xs) <- downX1 x
497 (yWhich : ys) <- downX1 y
498 return
499 ( "Vertical rule for right transformed variant nequality",
500 return
501 $ make opOr
502 $ fromList
503 [ [essence| &xWhich != &yWhich |],
504 make opAnd
505 $ fromList
506 [ [essence| &xWhich = &yWhich |],
507 onTagged (make opNeq) xWhich (rx <$> xs) (ry <$> ys)
508 ]
509 ]
510 )
511
512 rule_Transform_Variant_Lt :: Rule
513 rule_Transform_Variant_Lt = "transform-variant-lt" `namedRule` theRule
514 where
515 theRule p = do
516 (l, r) <- match opLt p
517 atLeastOneTransform (l, r)
518 let (x, rx) = matchManyTransforms l
519 let (y, ry) = matchManyTransforms r
520 TypeVariant {} <- typeOf x
521 TypeVariant {} <- typeOf y
522 (xWhich : xs) <- downX1 x
523 (yWhich : ys) <- downX1 y
524 return
525 ( "Vertical rule for right transformed variant less than",
526 return
527 $ make opOr
528 $ fromList
529 [ [essence| &xWhich < &yWhich |],
530 make opAnd
531 $ fromList
532 [ [essence| &xWhich = &yWhich |],
533 onTagged (make opLt) xWhich (rx <$> xs) (ry <$> ys)
534 ]
535 ]
536 )
537
538 rule_Transform_Variant_Leq :: Rule
539 rule_Transform_Variant_Leq = "transform-variant-leq" `namedRule` theRule
540 where
541 theRule p = do
542 (l, r) <- match opLeq p
543 atLeastOneTransform (l, r)
544 let (x, rx) = matchManyTransforms l
545 let (y, ry) = matchManyTransforms r
546 TypeVariant {} <- typeOf x
547 TypeVariant {} <- typeOf y
548 (xWhich : xs) <- downX1 x
549 (yWhich : ys) <- downX1 y
550 return
551 ( "Vertical rule for right transformed variant less than eq",
552 return
553 $ make opOr
554 $ fromList
555 [ [essence| &xWhich < &yWhich |],
556 make opAnd
557 $ fromList
558 [ [essence| &xWhich = &yWhich |],
559 onTagged (make opLeq) xWhich (rx <$> xs) (ry <$> ys)
560 ]
561 ]
562 )
563
564 rule_Transformed_Variant_Index :: Rule
565 rule_Transformed_Variant_Index = "transformed-variant-index" `namedRule` theRule
566 where
567 theRule p = do
568 (l, arg) <- match opIndexing p
569 atLeastOneTransform (l, l)
570 let (x, rx) = matchManyTransforms l
571 TypeVariant ds <- typeOf x
572 (xWhich : xs) <- downX1 x
573 name <- nameOut arg
574 argInt <-
575 case elemIndex name (map fst ds) of
576 Nothing -> failDoc "Variant indexing, not a member of the type."
577 Just argInt -> return argInt
578 return
579 ( "Variant indexing on:" <+> pretty p,
580 return
581 $ WithLocals
582 (rx (atNote "Variant indexing" xs argInt))
583 ( DefinednessConstraints
584 [ [essence| &xWhich = &argInt2 |]
585 | let argInt2 = fromInt (fromIntegral (argInt + 1))
586 ]
587 )
588 )
589
590 rule_Transformed_Variant_Active :: Rule
591 rule_Transformed_Variant_Active = "transformed-variant-active" `namedRule` theRule
592 where
593 theRule p = do
594 (l, name) <- match opActive p
595 atLeastOneTransform (l, l)
596 let (x, _) = matchManyTransforms l
597 TypeVariant ds <- typeOf x
598 (xWhich : _) <- downX1 x
599 argInt <- case elemIndex name (map fst ds) of
600 Nothing -> failDoc "Variant indexing, not a member of the type."
601 Just argInt -> return $ fromInt $ fromIntegral $ argInt + 1
602 return
603 ( "Variant active on:" <+> pretty p,
604 return $ [essence| &xWhich = &argInt |]
605 )