never executed always true always false
1 {-# LANGUAGE KindSignatures #-}
2
3 module Conjure.Language.Lenses where
4
5 import Conjure.Prelude
6 import Conjure.Language.Definition
7 import Conjure.Language.Constant
8 import Conjure.Language.Domain
9 import Conjure.Language.Type
10 import Conjure.Language.TypeOf
11 import Conjure.Language.Expression.Op
12 import Conjure.Language.Pretty
13 import Conjure.Language.AdHoc
14 import qualified Data.Kind as T (Type)
15
16
17 -- | To use a lens for constructing stuf.
18 make :: (Proxy Identity -> (a, b)) -> a
19 make f = fst (f (Proxy :: Proxy Identity))
20
21 -- | To use a lens for deconstructing stuf.
22 match :: (Proxy (m :: T.Type -> T.Type) -> (a, b -> m c)) -> b -> m c
23 match f = snd (f Proxy)
24
25 followAliases :: CanBeAnAlias b => (b -> c) -> b -> c
26 followAliases m (isAlias -> Just x) = followAliases m x
27 followAliases m x = m x
28
29 tryMatch :: (Proxy Maybe -> (a, b -> Maybe c)) -> b -> Maybe c
30 tryMatch = match
31
32 matchOr :: c -> (Proxy Maybe -> (a, b -> Maybe c)) -> b -> c
33 matchOr defOut f inp = fromMaybe defOut (match f inp)
34
35 matchDef :: (Proxy Maybe -> (a, b -> Maybe b)) -> b -> b
36 matchDef f inp = matchOr inp f inp
37
38 matchDefs :: CanBeAnAlias b => [Proxy Maybe -> (a, b -> Maybe b)] -> b -> b
39 matchDefs fs inp =
40 case mapMaybe (`match` inp) fs of
41 [] -> inp
42 (out:_) -> matchDefs fs out
43
44
45 --------------------------------------------------------------------------------
46 -- Lenses (for a weird definition of lens) -------------------------------------
47 --------------------------------------------------------------------------------
48
49
50 opMinus
51 :: ( Op x :< x
52 , Pretty x
53 , MonadFailDoc m
54 )
55 => Proxy (m :: T.Type -> T.Type)
56 -> ( x -> x -> x
57 , x -> m (x,x)
58 )
59 opMinus _ =
60 ( \ x y -> inject (MkOpMinus (OpMinus x y))
61 , \ p -> do
62 op <- project p
63 case op of
64 MkOpMinus (OpMinus x y) -> return (x,y)
65 _ -> na ("Lenses.opMinus:" <++> pretty p)
66 )
67
68
69 opDiv
70 :: ( Op x :< x
71 , Pretty x
72 , MonadFailDoc m
73 )
74 => Proxy (m :: T.Type -> T.Type)
75 -> ( x -> x -> x
76 , x -> m (x,x)
77 )
78 opDiv _ =
79 ( \ x y -> inject (MkOpDiv (OpDiv x y))
80 , \ p -> do
81 op <- project p
82 case op of
83 MkOpDiv (OpDiv x y) -> return (x,y)
84 _ -> na ("Lenses.opDiv:" <++> pretty p)
85 )
86
87
88 opMod
89 :: ( Op x :< x
90 , Pretty x
91 , MonadFailDoc m
92 )
93 => Proxy (m :: T.Type -> T.Type)
94 -> ( x -> x -> x
95 , x -> m (x,x)
96 )
97 opMod _ =
98 ( \ x y -> inject (MkOpMod (OpMod x y))
99 , \ p -> do
100 op <- project p
101 case op of
102 MkOpMod (OpMod x y) -> return (x,y)
103 _ -> na ("Lenses.opMod:" <++> pretty p)
104 )
105
106
107 opPow
108 :: ( Op x :< x
109 , Pretty x
110 , MonadFailDoc m
111 )
112 => Proxy (m :: T.Type -> T.Type)
113 -> ( x -> x -> x
114 , x -> m (x,x)
115 )
116 opPow _ =
117 ( \ x y -> inject (MkOpPow (OpPow x y))
118 , \ p -> do
119 op <- project p
120 case op of
121 MkOpPow (OpPow x y) -> return (x,y)
122 _ -> na ("Lenses.opPow:" <++> pretty p)
123 )
124
125
126 opNegate
127 :: ( Op x :< x
128 , Pretty x
129 , MonadFailDoc m
130 )
131 => Proxy (m :: T.Type -> T.Type)
132 -> ( x -> x
133 , x -> m x
134 )
135 opNegate _ =
136 ( inject . MkOpNegate . OpNegate
137 , \ p -> do
138 op <- project p
139 case op of
140 MkOpNegate (OpNegate x) -> return x
141 _ -> na ("Lenses.opNegate:" <++> pretty p)
142 )
143
144
145 opDontCare
146 :: ( Op x :< x
147 , Pretty x
148 , MonadFailDoc m
149 )
150 => Proxy (m :: T.Type -> T.Type)
151 -> ( x -> x
152 , x -> m x
153 )
154 opDontCare _ =
155 ( inject . MkOpDontCare . OpDontCare
156 , \ p -> do
157 op <- project p
158 case op of
159 MkOpDontCare (OpDontCare x) -> return x
160 _ -> na ("Lenses.opDontCare:" <++> pretty p)
161 )
162
163
164 opDefined
165 :: MonadFailDoc m
166 => Proxy (m :: T.Type -> T.Type)
167 -> ( Expression -> Expression
168 , Expression -> m Expression
169 )
170 opDefined _ =
171 ( inject . MkOpDefined . OpDefined
172 , followAliases extract
173 )
174 where
175 extract (Op (MkOpDefined (OpDefined x))) = return x
176 extract p = na ("Lenses.opDefined:" <++> pretty p)
177
178
179 opRange
180 :: MonadFailDoc m
181 => Proxy (m :: T.Type -> T.Type)
182 -> ( Expression -> Expression
183 , Expression -> m Expression
184 )
185 opRange _ =
186 ( inject . MkOpRange . OpRange
187 , followAliases extract
188 )
189 where
190 extract (Op (MkOpRange (OpRange x))) = return x
191 extract p = na ("Lenses.opRange:" <++> pretty p)
192
193
194 opDefinedOrRange
195 :: ( Op x :< x
196 , Pretty x
197 , MonadFailDoc m
198 )
199 => Proxy (m :: T.Type -> T.Type)
200 -> ( (x -> x, x) -> x
201 , x -> m (x -> x, x)
202 )
203 opDefinedOrRange _ =
204 ( \ (mk, x) -> mk x
205 , \ p -> case project p of
206 Just (MkOpDefined (OpDefined x)) -> return (inject . MkOpDefined . OpDefined , x)
207 Just (MkOpRange (OpRange x)) -> return (inject . MkOpRange . OpRange , x)
208 _ -> na ("Lenses.opDefinedOrRange" <++> pretty p)
209 )
210
211
212 opRestrict
213 :: MonadFailDoc m
214 => Proxy (m :: T.Type -> T.Type)
215 -> ( Expression -> Domain () Expression -> Expression
216 , Expression -> m (Expression, Domain () Expression)
217 )
218 opRestrict _ =
219 ( \ x d -> inject $ MkOpRestrict $ OpRestrict x (Domain d)
220 , followAliases extract
221 )
222 where
223 extract (Op (MkOpRestrict (OpRestrict x (Domain d)))) = return (x, d)
224 extract p = na ("Lenses.opRestrict:" <++> pretty p)
225
226
227 opToInt
228 :: ( Op x :< x
229 , Pretty x
230 , MonadFailDoc m
231 )
232 => Proxy (m :: T.Type -> T.Type)
233 -> ( x -> x
234 , x -> m x
235 )
236 opToInt _ =
237 ( inject . MkOpToInt . OpToInt
238 , \ p -> do
239 op <- project p
240 case op of
241 MkOpToInt (OpToInt x) -> return x
242 _ -> na ("Lenses.opToInt:" <++> pretty p)
243 )
244
245
246 opPowerSet
247 :: ( Op x :< x
248 , Pretty x
249 , MonadFailDoc m
250 )
251 => Proxy (m :: T.Type -> T.Type)
252 -> ( x -> x
253 , x -> m x
254 )
255 opPowerSet _ =
256 ( inject . MkOpPowerSet . OpPowerSet
257 , \ p -> do
258 op <- project p
259 case op of
260 MkOpPowerSet (OpPowerSet x) -> return x
261 _ -> na ("Lenses.opPowerSet:" <++> pretty p)
262 )
263
264
265 opToSet
266 :: ( Op x :< x
267 , Pretty x
268 , MonadFailDoc m
269 )
270 => Proxy (m :: T.Type -> T.Type)
271 -> ( x -> x
272 , x -> m x
273 )
274 opToSet _ =
275 ( inject . MkOpToSet . OpToSet False
276 , \ p -> do
277 op <- project p
278 case op of
279 MkOpToSet (OpToSet _ x) -> return x
280 _ -> na ("Lenses.opToSet:" <++> pretty p)
281 )
282
283
284
285 opToSetWithFlag
286 :: ( Op x :< x
287 , Pretty x
288 , MonadFailDoc m
289 )
290 => Proxy (m :: T.Type -> T.Type)
291 -> ( Bool -> x -> x
292 , x -> m (Bool, x)
293 )
294 opToSetWithFlag _ =
295 ( \ b x -> inject $ MkOpToSet $ OpToSet b x
296 , \ p -> do
297 op <- project p
298 case op of
299 MkOpToSet (OpToSet b x) -> return (b, x)
300 _ -> na ("Lenses.opToSet:" <++> pretty p)
301 )
302
303
304 opToMSet
305 :: ( Op x :< x
306 , Pretty x
307 , MonadFailDoc m
308 )
309 => Proxy (m :: T.Type -> T.Type)
310 -> ( x -> x
311 , x -> m x
312 )
313 opToMSet _ =
314 ( inject . MkOpToMSet . OpToMSet
315 , \ p -> do
316 op <- project p
317 case op of
318 MkOpToMSet (OpToMSet x) -> return x
319 _ -> na ("Lenses.opToMSet:" <++> pretty p)
320 )
321
322
323 opToRelation
324 :: ( Op x :< x
325 , Pretty x
326 , MonadFailDoc m
327 )
328 => Proxy (m :: T.Type -> T.Type)
329 -> ( x -> x
330 , x -> m x
331 )
332 opToRelation _ =
333 ( inject . MkOpToRelation . OpToRelation
334 , \ p -> do
335 op <- project p
336 case op of
337 MkOpToRelation (OpToRelation x) -> return x
338 _ -> na ("Lenses.opToRelation:" <++> pretty p)
339 )
340
341
342 opParts
343 :: ( Op x :< x
344 , Pretty x
345 , MonadFailDoc m
346 )
347 => Proxy (m :: T.Type -> T.Type)
348 -> ( x -> x
349 , x -> m x
350 )
351 opParts _ =
352 ( inject . MkOpParts . OpParts
353 , \ p -> do
354 op <- project p
355 case op of
356 MkOpParts (OpParts x) -> return x
357 _ -> na ("Lenses.opParts:" <++> pretty p)
358 )
359
360
361 opParty
362 :: ( Op x :< x
363 , Pretty x
364 , MonadFailDoc m
365 )
366 => Proxy (m :: T.Type -> T.Type)
367 -> ( x -> x -> x
368 , x -> m (x, x)
369 )
370 opParty _ =
371 ( \ x y -> inject $ MkOpParty $ OpParty x y
372 , \ p -> do
373 op <- project p
374 case op of
375 MkOpParty (OpParty x y) -> return (x,y)
376 _ -> na ("Lenses.opParty:" <++> pretty p)
377 )
378
379
380 opParticipants
381 :: ( Op x :< x
382 , Pretty x
383 , MonadFailDoc m
384 )
385 => Proxy (m :: T.Type -> T.Type)
386 -> ( x -> x
387 , x -> m x
388 )
389 opParticipants _ =
390 ( inject . MkOpParticipants . OpParticipants
391 , \ p -> do
392 op <- project p
393 case op of
394 MkOpParticipants (OpParticipants x) -> return x
395 _ -> na ("Lenses.opParticipants:" <++> pretty p)
396 )
397
398
399 opImage
400 :: ( Op x :< x
401 , Pretty x
402 , MonadFailDoc m
403 )
404 => Proxy (m :: T.Type -> T.Type)
405 -> ( x -> x -> x
406 , x -> m (x, x)
407 )
408 opImage _ =
409 ( \ x y -> inject $ MkOpImage $ OpImage x y
410 , \ p -> do
411 op <- project p
412 case op of
413 MkOpImage (OpImage x y) -> return (x,y)
414 _ -> na ("Lenses.opImage:" <++> pretty p)
415 )
416
417
418 opImageSet
419 :: ( Op x :< x
420 , Pretty x
421 , MonadFailDoc m
422 )
423 => Proxy (m :: T.Type -> T.Type)
424 -> ( x -> x -> x
425 , x -> m (x, x)
426 )
427 opImageSet _ =
428 ( \ x y -> inject $ MkOpImageSet $ OpImageSet x y
429 , \ p -> do
430 op <- project p
431 case op of
432 MkOpImageSet (OpImageSet x y) -> return (x,y)
433 _ -> na ("Lenses.opImageSet:" <++> pretty p)
434 )
435
436 opTransform
437 :: ( Op x :< x
438 , Pretty x
439 , MonadFailDoc m
440 )
441 => Proxy (m :: T.Type -> T.Type)
442 -> ( [x] -> x -> x
443 , x -> m ([x], x)
444 )
445 opTransform _ =
446 ( \ x y -> inject $ MkOpTransform $ OpTransform x y
447 , \ p -> do
448 op <- project p
449 case op of
450 MkOpTransform (OpTransform x y) -> return (x,y)
451 _ -> na ("Lenses.opTransform:" <++> pretty p)
452 )
453
454
455 opQuickPermutationOrder
456 :: ( Op x :< x
457 , Pretty x
458 , MonadFailDoc m
459 )
460 => Proxy (m :: T.Type -> T.Type)
461 -> ( [x] -> x -> x
462 , x -> m ([x], x)
463 )
464 opQuickPermutationOrder _ =
465 ( \ x y -> inject $ MkOpQuickPermutationOrder $ OpQuickPermutationOrder x y
466 , \ p -> do
467 op <- project p
468 case op of
469 MkOpQuickPermutationOrder (OpQuickPermutationOrder x y) -> return (x,y)
470 _ -> na ("Lenses.opTransform:" <++> pretty p)
471 )
472
473 opRelationProj
474 :: ( Op x :< x
475 , Pretty x
476 , MonadFailDoc m
477 )
478 => Proxy (m :: T.Type -> T.Type)
479 -> ( x -> [Maybe x] -> x
480 , x -> m (x, [Maybe x])
481 )
482 opRelationProj _ =
483 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x ys
484 , \ p -> do
485 op <- project p
486 case op of
487 MkOpRelationProj (OpRelationProj x ys) -> return (x,ys)
488 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
489 )
490
491
492 opPermInverse
493 :: ( Op x :< x
494 , Pretty x
495 , MonadFailDoc m
496 )
497 => Proxy (m :: T.Type -> T.Type)
498 -> ( x -> x
499 , x -> m x
500 )
501 opPermInverse _ =
502 ( inject . MkOpPermInverse . OpPermInverse
503 , \ p -> do
504 op <- project p
505 case op of
506 MkOpPermInverse (OpPermInverse x) -> return x
507 _ -> na ("Lenses.opPermInverse:" <++> pretty p)
508 )
509
510
511 opRelationImage
512 :: ( Op x :< x
513 , Pretty x
514 , MonadFailDoc m
515 )
516 => Proxy (m :: T.Type -> T.Type)
517 -> ( x -> [x] -> x
518 , x -> m (x, [x])
519 )
520 opRelationImage _ =
521 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x (map Just ys)
522 , \ p -> do
523 op <- project p
524 case op of
525 MkOpRelationProj (OpRelationProj x ys)
526 | let ys' = catMaybes ys
527 , length ys' == length ys -- they were all Just's
528 -> return (x,ys')
529 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
530 )
531
532
533 opIndexing
534 :: ( Op x :< x
535 , Pretty x
536 , MonadFailDoc m
537 )
538 => Proxy (m :: T.Type -> T.Type)
539 -> ( x -> x -> x
540 , x -> m (x,x)
541 )
542 opIndexing _ =
543 ( \ x y -> inject (MkOpIndexing (OpIndexing x y))
544 , \ p -> do
545 op <- project p
546 case op of
547 MkOpIndexing (OpIndexing x y) -> return (x,y)
548 _ -> na ("Lenses.opIndexing:" <++> pretty p)
549 )
550
551
552 opMatrixIndexing
553 :: ( Op x :< x
554 , Pretty x
555 , TypeOf x
556 , MonadFailDoc m
557 , ?typeCheckerMode :: TypeCheckerMode
558 )
559 => Proxy (m :: T.Type -> T.Type)
560 -> ( x -> [x] -> x
561 , x -> m (x,[x])
562 )
563 opMatrixIndexing _ =
564 ( foldl (make opIndexing)
565 , \ p -> do
566 (m, is) <- go p
567 if null is
568 then na ("Lenses.opMatrixIndexing:" <+> pretty p)
569 else return (m, is)
570 )
571 where
572 go p = case project p of
573 Just (MkOpIndexing (OpIndexing x i)) -> do
574 ty <- typeOf x
575 case ty of
576 TypeMatrix{} -> return ()
577 TypeList{} -> return ()
578 _ -> na ("Lenses.opMatrixIndexing:" <+> pretty p)
579 (m,is) <- go x
580 return (m, is ++ [i])
581 _ -> return (p, [])
582
583
584 opMatrixIndexingSlicing
585 :: ( Op x :< x
586 , Pretty x
587 , MonadFailDoc m
588 , TypeOf x
589 , ?typeCheckerMode :: TypeCheckerMode
590 )
591 => Proxy (m :: T.Type -> T.Type)
592 -> ( x -> [Either x (Maybe x, Maybe x)] -> x
593 , x -> m (x, [Either x (Maybe x, Maybe x)]) -- either an index or a slice
594 )
595 opMatrixIndexingSlicing _ =
596 ( mk
597 , \ p -> do
598 (m, is, wasThereAnySlicing) <- go p
599 if not (null is) && wasThereAnySlicing
600 then return (m, is)
601 else na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
602 )
603 where
604 mk m [] = m
605 mk m (Left i:is) = mk (make opIndexing m i) is
606 mk m (Right (lb, ub):is) = mk (make opSlicing m lb ub) is
607
608 go p = case project p of
609 Just (MkOpIndexing (OpIndexing x i)) -> do
610 ty <- typeOf x
611 case ty of
612 TypeMatrix{} -> return ()
613 TypeList{} -> return ()
614 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
615 (m, is, wasThereAnySlicing) <- go x
616 return (m, is ++ [Left i], wasThereAnySlicing)
617 Just (MkOpSlicing (OpSlicing x lb ub)) -> do
618 ty <- typeOf x
619 case ty of
620 TypeMatrix{} -> return ()
621 TypeList{} -> return ()
622 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
623 (m, is, _) <- go x
624 return (m, is ++ [Right (lb, ub)], True)
625 _ -> return (p, [], False)
626
627
628 opSlicing
629 :: ( Op x :< x
630 , Pretty x
631 , MonadFailDoc m
632 )
633 => Proxy (m :: T.Type -> T.Type)
634 -> ( x -> Maybe x -> Maybe x -> x
635 , x -> m (x, Maybe x, Maybe x)
636 )
637 opSlicing _ =
638 ( \ x y z -> inject (MkOpSlicing (OpSlicing x y z))
639 , \ p -> do
640 op <- project p
641 case op of
642 MkOpSlicing (OpSlicing x y z) -> return (x,y,z)
643 _ -> na ("Lenses.opSlicing:" <++> pretty p)
644 )
645
646
647 opFlatten
648 :: ( Op x :< x
649 , Pretty x
650 , MonadFailDoc m
651 )
652 => Proxy (m :: T.Type -> T.Type)
653 -> ( x -> x
654 , x -> m x
655 )
656 opFlatten _ =
657 ( inject . MkOpFlatten . OpFlatten Nothing
658 , \ p -> do
659 op <- project p
660 case op of
661 MkOpFlatten (OpFlatten Nothing x) -> return x
662 _ -> na ("Lenses.opFlatten:" <++> pretty p)
663 )
664
665
666 flattenIfNeeded ::
667 Int ->
668 Expression ->
669 Expression
670 flattenIfNeeded dims m =
671 if dims > 1
672 then make opFlatten m
673 else m
674
675
676 oneDimensionaliser ::
677 Int -> -- current number of dimensions
678 Expression ->
679 Expression
680 oneDimensionaliser dims x =
681 case dims of
682 0 -> fromList [x]
683 1 -> x
684 _ -> make opFlatten x
685
686
687 opConcatenate
688 :: ( Op x :< x
689 , Pretty x
690 , MonadFailDoc m
691 )
692 => Proxy (m :: T.Type -> T.Type)
693 -> ( x -> x
694 , x -> m x
695 )
696 opConcatenate _ =
697 ( inject . MkOpFlatten . OpFlatten (Just 1)
698 , \ p -> do
699 op <- project p
700 case op of
701 MkOpFlatten (OpFlatten (Just 1) x) -> return x
702 _ -> na ("Lenses.opConcatenate:" <++> pretty p)
703 )
704
705
706 opIn
707 :: ( Op x :< x
708 , Pretty x
709 , MonadFailDoc m
710 )
711 => Proxy (m :: T.Type -> T.Type)
712 -> ( x -> x -> x
713 , x -> m (x,x)
714 )
715 opIn _ =
716 ( \ x y -> inject (MkOpIn (OpIn x y))
717 , \ p -> do
718 op <- project p
719 case op of
720 MkOpIn (OpIn x y) -> return (x,y)
721 _ -> na ("Lenses.opIn:" <++> pretty p)
722 )
723
724
725 opFreq
726 :: ( Op x :< x
727 , Pretty x
728 , MonadFailDoc m
729 )
730 => Proxy (m :: T.Type -> T.Type)
731 -> ( x -> x -> x
732 , x -> m (x,x)
733 )
734 opFreq _ =
735 ( \ x y -> inject (MkOpFreq (OpFreq x y))
736 , \ p -> do
737 op <- project p
738 case op of
739 MkOpFreq (OpFreq x y) -> return (x,y)
740 _ -> na ("Lenses.opFreq:" <++> pretty p)
741 )
742
743
744 opHist
745 :: ( Op x :< x
746 , Pretty x
747 , MonadFailDoc m
748 )
749 => Proxy (m :: T.Type -> T.Type)
750 -> ( x -> x
751 , x -> m x
752 )
753 opHist _ =
754 ( inject . MkOpHist . OpHist
755 , \ p -> do
756 op <- project p
757 case op of
758 MkOpHist (OpHist x) -> return x
759 _ -> na ("Lenses.opHist:" <++> pretty p)
760 )
761
762
763 opIntersect
764 :: ( Op x :< x
765 , Pretty x
766 , MonadFailDoc m
767 )
768 => Proxy (m :: T.Type -> T.Type)
769 -> ( x -> x -> x
770 , x -> m (x,x)
771 )
772 opIntersect _ =
773 ( \ x y -> inject (MkOpIntersect (OpIntersect x y))
774 , \ p -> do
775 op <- project p
776 case op of
777 MkOpIntersect (OpIntersect x y) -> return (x,y)
778 _ -> na ("Lenses.opIntersect:" <++> pretty p)
779 )
780
781
782 opUnion
783 :: ( Op x :< x
784 , Pretty x
785 , MonadFailDoc m
786 )
787 => Proxy (m :: T.Type -> T.Type)
788 -> ( x -> x -> x
789 , x -> m (x,x)
790 )
791 opUnion _ =
792 ( \ x y -> inject (MkOpUnion (OpUnion x y))
793 , \ p -> do
794 op <- project p
795 case op of
796 MkOpUnion (OpUnion x y) -> return (x,y)
797 _ -> na ("Lenses.opUnion:" <++> pretty p)
798 )
799
800
801 opSubsetEq
802 :: ( Op x :< x
803 , Pretty x
804 , MonadFailDoc m
805 )
806 => Proxy (m :: T.Type -> T.Type)
807 -> ( x -> x -> x
808 , x -> m (x,x)
809 )
810 opSubsetEq _ =
811 ( \ x y -> inject (MkOpSubsetEq (OpSubsetEq x y))
812 , \ p -> do
813 op <- project p
814 case op of
815 MkOpSubsetEq (OpSubsetEq x y) -> return (x,y)
816 _ -> na ("Lenses.opSubsetEq:" <++> pretty p)
817 )
818
819
820 opEq
821 :: ( Op x :< x
822 , Pretty x
823 , MonadFailDoc m
824 )
825 => Proxy (m :: T.Type -> T.Type)
826 -> ( x -> x -> x
827 , x -> m (x,x)
828 )
829 opEq _ =
830 ( \ x y -> inject (MkOpEq (OpEq x y))
831 , \ p -> do
832 op <- project p
833 case op of
834 MkOpEq (OpEq x y) -> return (x,y)
835 _ -> na ("Lenses.opEq:" <++> pretty p)
836 )
837
838
839 opNeq
840 :: ( Op x :< x
841 , Pretty x
842 , MonadFailDoc m
843 )
844 => Proxy (m :: T.Type -> T.Type)
845 -> ( x -> x -> x
846 , x -> m (x,x)
847 )
848 opNeq _ =
849 ( \ x y -> inject (MkOpNeq (OpNeq x y))
850 , \ p -> do
851 op <- project p
852 case op of
853 MkOpNeq (OpNeq x y) -> return (x,y)
854 _ -> na ("Lenses.opNeq:" <++> pretty p)
855 )
856
857
858 opLt
859 :: ( Op x :< x
860 , Pretty x
861 , MonadFailDoc m
862 )
863 => Proxy (m :: T.Type -> T.Type)
864 -> ( x -> x -> x
865 , x -> m (x,x)
866 )
867 opLt _ =
868 ( \ x y -> inject (MkOpLt (OpLt x y))
869 , \ p -> do
870 op <- project p
871 case op of
872 MkOpLt (OpLt x y) -> return (x,y)
873 _ -> na ("Lenses.opLt:" <++> pretty p)
874 )
875
876
877 opLeq
878 :: ( Op x :< x
879 , Pretty x
880 , MonadFailDoc m
881 )
882 => Proxy (m :: T.Type -> T.Type)
883 -> ( x -> x -> x
884 , x -> m (x,x)
885 )
886 opLeq _ =
887 ( \ x y -> inject (MkOpLeq (OpLeq x y))
888 , \ p -> do
889 op <- project p
890 case op of
891 MkOpLeq (OpLeq x y) -> return (x,y)
892 _ -> na ("Lenses.opLeq:" <++> pretty p)
893 )
894
895
896 opGt
897 :: ( Op x :< x
898 , Pretty x
899 , MonadFailDoc m
900 )
901 => Proxy (m :: T.Type -> T.Type)
902 -> ( x -> x -> x
903 , x -> m (x,x)
904 )
905 opGt _ =
906 ( \ x y -> inject (MkOpGt (OpGt x y))
907 , \ p -> do
908 op <- project p
909 case op of
910 MkOpGt (OpGt x y) -> return (x,y)
911 _ -> na ("Lenses.opGt:" <++> pretty p)
912 )
913
914
915 opGeq
916 :: ( Op x :< x
917 , Pretty x
918 , MonadFailDoc m
919 )
920 => Proxy (m :: T.Type -> T.Type)
921 -> ( x -> x -> x
922 , x -> m (x,x)
923 )
924 opGeq _ =
925 ( \ x y -> inject (MkOpGeq (OpGeq x y))
926 , \ p -> do
927 op <- project p
928 case op of
929 MkOpGeq (OpGeq x y) -> return (x,y)
930 _ -> na ("Lenses.opGeq:" <++> pretty p)
931 )
932
933
934 opDotLt
935 :: ( Op x :< x
936 , Pretty x
937 , MonadFailDoc m
938 )
939 => Proxy (m :: T.Type -> T.Type)
940 -> ( x -> x -> x
941 , x -> m (x,x)
942 )
943 opDotLt _ =
944 ( \ x y -> inject (MkOpDotLt (OpDotLt x y))
945 , \ p -> do
946 op <- project p
947 case op of
948 MkOpDotLt (OpDotLt x y) -> return (x,y)
949 _ -> na ("Lenses.opDotLt:" <++> pretty p)
950 )
951
952
953 opDotLeq
954 :: ( Op x :< x
955 , Pretty x
956 , MonadFailDoc m
957 )
958 => Proxy (m :: T.Type -> T.Type)
959 -> ( x -> x -> x
960 , x -> m (x,x)
961 )
962 opDotLeq _ =
963 ( \ x y -> inject (MkOpDotLeq (OpDotLeq x y))
964 , \ p -> do
965 op <- project p
966 case op of
967 MkOpDotLeq (OpDotLeq x y) -> return (x,y)
968 _ -> na ("Lenses.opDotLeq:" <++> pretty p)
969 )
970
971
972 opTildeLt
973 :: ( Op x :< x
974 , Pretty x
975 , MonadFailDoc m
976 )
977 => Proxy (m :: T.Type -> T.Type)
978 -> ( x -> x -> x
979 , x -> m (x,x)
980 )
981 opTildeLt _ =
982 ( \ x y -> inject (MkOpTildeLt (OpTildeLt x y))
983 , \ p -> do
984 op <- project p
985 case op of
986 MkOpTildeLt (OpTildeLt x y) -> return (x,y)
987 _ -> na ("Lenses.opTildeLt:" <++> pretty p)
988 )
989
990
991 opTildeLeq
992 :: ( Op x :< x
993 , Pretty x
994 , MonadFailDoc m
995 )
996 => Proxy (m :: T.Type -> T.Type)
997 -> ( x -> x -> x
998 , x -> m (x,x)
999 )
1000 opTildeLeq _ =
1001 ( \ x y -> inject (MkOpTildeLeq (OpTildeLeq x y))
1002 , \ p -> do
1003 op <- project p
1004 case op of
1005 MkOpTildeLeq (OpTildeLeq x y) -> return (x,y)
1006 _ -> na ("Lenses.opTildeLeq:" <++> pretty p)
1007 )
1008
1009
1010 opOr
1011 :: ( Op x :< x
1012 , Pretty x
1013 , MonadFailDoc m
1014 )
1015 => Proxy (m :: T.Type -> T.Type)
1016 -> ( x -> x
1017 , x -> m x
1018 )
1019 opOr _ =
1020 ( inject . MkOpOr . OpOr
1021 , \ p -> do
1022 op <- project p
1023 case op of
1024 MkOpOr (OpOr xs) -> return xs
1025 _ -> na ("Lenses.opOr:" <++> pretty p)
1026 )
1027
1028
1029 opAnd
1030 :: ( Op x :< x
1031 , Pretty x
1032 , MonadFailDoc m
1033 )
1034 => Proxy (m :: T.Type -> T.Type)
1035 -> ( x -> x
1036 , x -> m x
1037 )
1038 opAnd _ =
1039 ( inject . MkOpAnd . OpAnd
1040 , \ p -> do
1041 op <- project p
1042 case op of
1043 MkOpAnd (OpAnd xs) -> return xs
1044 _ -> na ("Lenses.opAnd:" <++> pretty p)
1045 )
1046
1047
1048 opMax
1049 :: ( Op x :< x
1050 , Pretty x
1051 , MonadFailDoc m
1052 )
1053 => Proxy (m :: T.Type -> T.Type)
1054 -> ( x -> x
1055 , x -> m x
1056 )
1057 opMax _ =
1058 ( inject . MkOpMax . OpMax
1059 , \ p -> do
1060 op <- project p
1061 case op of
1062 MkOpMax (OpMax xs) -> return xs
1063 _ -> na ("Lenses.opMax:" <++> pretty p)
1064 )
1065
1066
1067 opMin
1068 :: ( Op x :< x
1069 , Pretty x
1070 , MonadFailDoc m
1071 )
1072 => Proxy (m :: T.Type -> T.Type)
1073 -> ( x -> x
1074 , x -> m x
1075 )
1076 opMin _ =
1077 ( inject . MkOpMin . OpMin
1078 , \ p -> do
1079 op <- project p
1080 case op of
1081 MkOpMin (OpMin xs) -> return xs
1082 _ -> na ("Lenses.opMin:" <++> pretty p)
1083 )
1084
1085
1086 opImply
1087 :: ( Op x :< x
1088 , Pretty x
1089 , MonadFailDoc m
1090 )
1091 => Proxy (m :: T.Type -> T.Type)
1092 -> ( x -> x -> x
1093 , x -> m (x,x)
1094 )
1095 opImply _ =
1096 ( \ x y -> inject (MkOpImply (OpImply x y))
1097 , \ p -> do
1098 op <- project p
1099 case op of
1100 MkOpImply (OpImply x y) -> return (x,y)
1101 _ -> na ("Lenses.opImply:" <++> pretty p)
1102 )
1103
1104
1105 opNot
1106 :: ( Op x :< x
1107 , Pretty x
1108 , MonadFailDoc m
1109 )
1110 => Proxy (m :: T.Type -> T.Type)
1111 -> ( x -> x
1112 , x -> m x
1113 )
1114 opNot _ =
1115 ( inject . MkOpNot . OpNot
1116 , \ p -> do
1117 op <- project p
1118 case op of
1119 MkOpNot (OpNot x) -> return x
1120 _ -> na ("Lenses.opNot:" <++> pretty p)
1121 )
1122
1123
1124 opProduct
1125 :: ( Op x :< x
1126 , Pretty x
1127 , MonadFailDoc m
1128 )
1129 => Proxy (m :: T.Type -> T.Type)
1130 -> ( x -> x
1131 , x -> m x
1132 )
1133 opProduct _ =
1134 ( inject . MkOpProduct . OpProduct
1135 , \ p -> do
1136 op <- project p
1137 case op of
1138 MkOpProduct (OpProduct x) -> return x
1139 _ -> na ("Lenses.opProduct:" <++> pretty p)
1140 )
1141
1142
1143 opSum
1144 :: ( Op x :< x
1145 , Pretty x
1146 , MonadFailDoc m
1147 )
1148 => Proxy (m :: T.Type -> T.Type)
1149 -> ( x -> x
1150 , x -> m x
1151 )
1152 opSum _ =
1153 ( inject . MkOpSum . OpSum
1154 , \ p -> do
1155 op <- project p
1156 case op of
1157 MkOpSum (OpSum x) -> return x
1158 _ -> na ("Lenses.opSum:" <++> pretty p)
1159 )
1160
1161
1162 data ReducerType = RepetitionIsNotSignificant | RepetitionIsSignificant
1163 deriving (Eq, Ord, Show)
1164
1165 opReducer
1166 :: ( Op x :< x
1167 , Pretty x
1168 , MonadFailDoc m
1169 )
1170 => Proxy (m :: T.Type -> T.Type)
1171 -> ( (x -> x, x) -> x
1172 , x -> m ( ReducerType
1173 , Bool -- defined on []
1174 , x -> x
1175 , x
1176 )
1177 )
1178 opReducer _ =
1179 ( \ (mk, x) -> mk x
1180 , \ p -> do
1181 op <- project p
1182 let is = RepetitionIsSignificant
1183 let isn't = RepetitionIsNotSignificant
1184 case op of
1185 MkOpAnd (OpAnd x) -> return (isn't, True , inject . MkOpAnd . OpAnd , x)
1186 MkOpOr (OpOr x) -> return (isn't, True , inject . MkOpOr . OpOr , x)
1187 MkOpXor (OpXor x) -> return (is , False, inject . MkOpXor . OpXor , x)
1188 MkOpSum (OpSum x) -> return (is , True , inject . MkOpSum . OpSum , x)
1189 MkOpProduct (OpProduct x) -> return (is , True , inject . MkOpProduct . OpProduct , x)
1190 MkOpMax (OpMax x) -> return (isn't, False, inject . MkOpMax . OpMax , x)
1191 MkOpMin (OpMin x) -> return (isn't, False, inject . MkOpMin . OpMin , x)
1192 _ -> na ("Lenses.opReducer:" <++> pretty p)
1193 )
1194
1195
1196 opModifier
1197 :: ( Op x :< x
1198 , MonadFailDoc m
1199 )
1200 => Proxy (m :: T.Type -> T.Type)
1201 -> ( (x -> x, x) -> x
1202 , x -> m (x -> x, x)
1203 )
1204 opModifier _ =
1205 ( \ (mk, x) -> mk x
1206 , \ p -> case project p of
1207 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1208 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1209 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1210 Just (MkOpParts (OpParts x)) -> return (inject . MkOpParts . OpParts , x)
1211 _ -> return (id , p)
1212 )
1213
1214
1215 opModifierNoP
1216 :: ( Op x :< x
1217 , MonadFailDoc m
1218 )
1219 => Proxy (m :: T.Type -> T.Type)
1220 -> ( (x -> x, x) -> x
1221 , x -> m (x -> x, x)
1222 )
1223 opModifierNoP _ =
1224 ( \ (mk, x) -> mk x
1225 , \ p -> case project p of
1226 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1227 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1228 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1229 _ -> return (id , p)
1230 )
1231
1232
1233 opAllDiff
1234 :: ( Op x :< x
1235 , Pretty x
1236 , MonadFailDoc m
1237 )
1238 => Proxy (m :: T.Type -> T.Type)
1239 -> ( x -> x
1240 , x -> m x
1241 )
1242 opAllDiff _ =
1243 ( inject . MkOpAllDiff . OpAllDiff
1244 , \ p -> do
1245 op <- project p
1246 case op of
1247 MkOpAllDiff (OpAllDiff x) -> return x
1248 _ -> na ("Lenses.opAllDiff:" <++> pretty p)
1249 )
1250
1251
1252 opAllDiffExcept
1253 :: ( Op x :< x
1254 , Pretty x
1255 , MonadFailDoc m
1256 )
1257 => Proxy (m :: T.Type -> T.Type)
1258 -> ( x -> x -> x
1259 , x -> m (x, x)
1260 )
1261 opAllDiffExcept _ =
1262 ( \ x y -> inject $ MkOpAllDiffExcept $ OpAllDiffExcept x y
1263 , \ p -> do
1264 op <- project p
1265 case op of
1266 MkOpAllDiffExcept (OpAllDiffExcept x y) -> return (x, y)
1267 _ -> na ("Lenses.opAllDiffExcept:" <++> pretty p)
1268 )
1269
1270
1271 constantInt
1272 :: MonadFailDoc m
1273 => Proxy (m :: T.Type -> T.Type)
1274 -> ( Integer -> Expression
1275 , Expression -> m Integer
1276 )
1277 constantInt _ =
1278 ( Constant . ConstantInt TagInt
1279 , \ p -> case p of
1280 (Constant (ConstantInt TagInt i)) -> return i
1281 _ -> na ("Lenses.constantInt:" <++> pretty p)
1282 )
1283
1284
1285
1286 matrixLiteral
1287 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1288 => Proxy (m :: T.Type -> T.Type)
1289 -> ( Type -> Domain () Expression -> [Expression] -> Expression
1290 , Expression -> m (Type, Domain () Expression, [Expression])
1291 )
1292 matrixLiteral _ =
1293 ( \ ty index elems ->
1294 if null elems
1295 then Typed (AbstractLiteral (AbsLitMatrix index elems)) ty
1296 else AbstractLiteral (AbsLitMatrix index elems)
1297 , \ p -> do
1298 ty <- typeOf p
1299 (index, xs) <- followAliases extract p
1300 return (ty, index, xs)
1301 )
1302 where
1303 extract (Constant (ConstantAbstract (AbsLitMatrix index xs))) = return (fmap Constant index, map Constant xs)
1304 extract (AbstractLiteral (AbsLitMatrix index xs)) = return (index, xs)
1305 extract (Typed x _) = extract x
1306 extract (Constant (TypedConstant x _)) = extract (Constant x)
1307 extract p = na ("Lenses.matrixLiteral:" <+> pretty p)
1308
1309
1310 onMatrixLiteral
1311 :: (Functor m, Applicative m, Monad m, NameGen m)
1312 => Maybe Int -- how many levels to go down. all the way if Nothing.
1313 -> (Expression -> m Expression)
1314 -> Expression -> m Expression
1315 onMatrixLiteral mlvl f = case mlvl of
1316 Nothing -> followAliases go
1317 Just lvl -> followAliases (goL lvl)
1318 where
1319 go (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1320 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (go . Constant) xs
1321 go (AbstractLiteral (AbsLitMatrix index xs)) =
1322 AbstractLiteral . AbsLitMatrix index <$> mapM go xs
1323 go (Typed x _) = go x
1324 go (Constant (TypedConstant x _)) = go (Constant x)
1325 go p = f p
1326
1327 goL 0 p = f p
1328 goL lvl (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1329 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (goL (lvl-1) . Constant) xs
1330 goL lvl (AbstractLiteral (AbsLitMatrix index xs)) =
1331 AbstractLiteral . AbsLitMatrix index <$> mapM (goL (lvl-1)) xs
1332 goL lvl (Typed x _) = goL lvl x
1333 goL lvl (Constant (TypedConstant x _)) = goL lvl (Constant x)
1334 goL lvl p = do
1335 (iPat, i) <- quantifiedVar
1336 body <- goL (lvl-1) i
1337 return $ Comprehension body [Generator (GenInExpr iPat p)]
1338
1339
1340 setLiteral
1341 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1342 => Proxy (m :: T.Type -> T.Type)
1343 -> ( Type -> [Expression] -> Expression
1344 , Expression -> m (Type, [Expression])
1345 )
1346 setLiteral _ =
1347 ( \ ty elems ->
1348 if null elems
1349 then Typed (AbstractLiteral (AbsLitSet elems)) ty
1350 else AbstractLiteral (AbsLitSet elems)
1351 , \ p -> do
1352 ty <- typeOf p
1353 xs <- followAliases extract p
1354 return (ty, xs)
1355 )
1356 where
1357 extract (Constant (viewConstantSet -> Just xs)) = return (map Constant xs)
1358 extract (AbstractLiteral (AbsLitSet xs)) = return xs
1359 extract (Typed x _) = extract x
1360 extract (Constant (TypedConstant x _)) = extract (Constant x)
1361 extract p = na ("Lenses.setLiteral:" <+> pretty p)
1362
1363
1364 msetLiteral
1365 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1366 => Proxy (m :: T.Type -> T.Type)
1367 -> ( Type -> [Expression] -> Expression
1368 , Expression -> m (Type, [Expression])
1369 )
1370 msetLiteral _ =
1371 ( \ ty elems ->
1372 if null elems
1373 then Typed (AbstractLiteral (AbsLitMSet elems)) ty
1374 else AbstractLiteral (AbsLitMSet elems)
1375 , \ p -> do
1376 ty <- typeOf p
1377 xs <- followAliases extract p
1378 return (ty, xs)
1379 )
1380 where
1381 extract (Constant (viewConstantMSet -> Just xs)) = return (map Constant xs)
1382 extract (AbstractLiteral (AbsLitMSet xs)) = return xs
1383 extract (Typed x _) = extract x
1384 extract (Constant (TypedConstant x _)) = extract (Constant x)
1385 extract p = na ("Lenses.msetLiteral:" <+> pretty p)
1386
1387
1388 functionLiteral
1389 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1390 => Proxy (m :: T.Type -> T.Type)
1391 -> ( Type -> [(Expression,Expression)] -> Expression
1392 , Expression -> m (Type, [(Expression,Expression)])
1393 )
1394 functionLiteral _ =
1395 ( \ ty elems ->
1396 if null elems
1397 then Typed (AbstractLiteral (AbsLitFunction elems)) ty
1398 else AbstractLiteral (AbsLitFunction elems)
1399 , \ p -> do
1400 ty <- typeOf p
1401 xs <- followAliases extract p
1402 return (ty, xs)
1403 )
1404 where
1405 extract (Constant (viewConstantFunction -> Just xs)) = return [ (Constant a, Constant b) | (a,b) <- xs ]
1406 extract (AbstractLiteral (AbsLitFunction xs)) = return xs
1407 extract (Typed x _) = extract x
1408 extract (Constant (TypedConstant x _)) = extract (Constant x)
1409 extract p = na ("Lenses.functionLiteral:" <+> pretty p)
1410
1411
1412 permutationLiteral
1413 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1414 => Proxy (m :: T.Type -> T.Type )
1415 -> ( Type -> [[Expression]] -> Expression
1416 , Expression -> m (Type, [[Expression]])
1417 )
1418 permutationLiteral _ =
1419 ( \ ty elems ->
1420 if null elems
1421 then Typed (AbstractLiteral (AbsLitPermutation elems)) ty
1422 else AbstractLiteral (AbsLitPermutation elems)
1423 , \ p -> do
1424 ty <- typeOf p
1425 xs <- followAliases extract p
1426 return (ty, xs)
1427 )
1428 where
1429 extract (Constant (ConstantAbstract (AbsLitPermutation xs))) = return [ [Constant z | z <- x] | x <- xs ]
1430 extract (AbstractLiteral (AbsLitPermutation xs)) = return xs
1431 extract (Typed x _) = extract x
1432 extract (Constant (TypedConstant x _)) = extract (Constant x)
1433 extract p = na ("Lenses.permutationLiteral:" <+> pretty p)
1434
1435
1436
1437
1438 sequenceLiteral
1439 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1440 => Proxy (m :: T.Type -> T.Type)
1441 -> ( Type -> [Expression] -> Expression
1442 , Expression -> m (Type, [Expression])
1443 )
1444 sequenceLiteral _ =
1445 ( \ ty elems ->
1446 if null elems
1447 then Typed (AbstractLiteral (AbsLitSequence elems)) ty
1448 else AbstractLiteral (AbsLitSequence elems)
1449 , \ p -> do
1450 ty <- typeOf p
1451 xs <- followAliases extract p
1452 return (ty, xs)
1453 )
1454 where
1455 extract (Constant (viewConstantSequence -> Just xs)) = return (map Constant xs)
1456 extract (AbstractLiteral (AbsLitSequence xs)) = return xs
1457 extract (Typed x _) = extract x
1458 extract (Constant (TypedConstant x _)) = extract (Constant x)
1459 extract p = na ("Lenses.sequenceLiteral:" <+> pretty p)
1460
1461
1462 relationLiteral
1463 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1464 => Proxy (m :: T.Type -> T.Type)
1465 -> ( Type -> [[Expression]] -> Expression
1466 , Expression -> m (Type, [[Expression]])
1467 )
1468 relationLiteral _ =
1469 ( \ ty elems ->
1470 if null elems
1471 then Typed (AbstractLiteral (AbsLitRelation elems)) ty
1472 else AbstractLiteral (AbsLitRelation elems)
1473 , \ p -> do
1474 ty <- typeOf p
1475 xs <- followAliases extract p
1476 return (ty, xs)
1477 )
1478 where
1479 extract (Constant (viewConstantRelation -> Just xs)) = return (map (map Constant) xs)
1480 extract (AbstractLiteral (AbsLitRelation xs)) = return xs
1481 extract (Typed x _) = extract x
1482 extract (Constant (TypedConstant x _)) = extract (Constant x)
1483 extract p = na ("Lenses.relationLiteral:" <+> pretty p)
1484
1485
1486 partitionLiteral
1487 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1488 => Proxy (m :: T.Type -> T.Type)
1489 -> ( Type -> [[Expression]] -> Expression
1490 , Expression -> m (Type, [[Expression]])
1491 )
1492 partitionLiteral _ =
1493 ( \ ty elems ->
1494 if null elems
1495 then Typed (AbstractLiteral (AbsLitPartition elems)) ty
1496 else AbstractLiteral (AbsLitPartition elems)
1497 , \ p -> do
1498 ty <- typeOf p
1499 xs <- followAliases extract p
1500 return (ty, xs)
1501 )
1502 where
1503 extract (Constant (viewConstantPartition -> Just xs)) = return (map (map Constant) xs)
1504 extract (AbstractLiteral (AbsLitPartition xs)) = return xs
1505 extract (Typed x _) = extract x
1506 extract (Constant (TypedConstant x _)) = extract (Constant x)
1507 extract p = na ("Lenses.partitionLiteral:" <+> pretty p)
1508
1509
1510 opTwoBars
1511 :: ( Op x :< x
1512 , Pretty x
1513 , MonadFailDoc m
1514 )
1515 => Proxy (m :: T.Type -> T.Type)
1516 -> ( x -> x
1517 , x -> m x
1518 )
1519 opTwoBars _ =
1520 ( inject . MkOpTwoBars . OpTwoBars
1521 , \ p -> do
1522 op <- project p
1523 case op of
1524 MkOpTwoBars (OpTwoBars x) -> return x
1525 _ -> na ("Lenses.opTwoBars:" <++> pretty p)
1526 )
1527
1528
1529 opPreImage
1530 :: ( Op x :< x
1531 , Pretty x
1532 , MonadFailDoc m
1533 )
1534 => Proxy (m :: T.Type -> T.Type)
1535 -> ( x -> x -> x
1536 , x -> m (x,x)
1537 )
1538 opPreImage _ =
1539 ( \ x y -> inject (MkOpPreImage (OpPreImage x y))
1540 , \ p -> do
1541 op <- project p
1542 case op of
1543 MkOpPreImage (OpPreImage x y) -> return (x,y)
1544 _ -> na ("Lenses.opPreImage:" <++> pretty p)
1545 )
1546
1547
1548 opActive
1549 :: ( Op x :< x
1550 , Pretty x
1551 , MonadFailDoc m
1552 )
1553 => Proxy (m :: T.Type -> T.Type)
1554 -> ( x -> Name -> x
1555 , x -> m (x,Name)
1556 )
1557 opActive _ =
1558 ( \ x y -> inject (MkOpActive (OpActive x y))
1559 , \ p -> do
1560 op <- project p
1561 case op of
1562 MkOpActive (OpActive x y) -> return (x,y)
1563 _ -> na ("Lenses.opActive:" <++> pretty p)
1564 )
1565
1566
1567 opFactorial
1568 :: ( Op x :< x
1569 , Pretty x
1570 , MonadFailDoc m
1571 )
1572 => Proxy (m :: T.Type -> T.Type)
1573 -> ( x -> x
1574 , x -> m x
1575 )
1576 opFactorial _ =
1577 ( inject . MkOpFactorial . OpFactorial
1578 , \ p -> do
1579 op <- project p
1580 case op of
1581 MkOpFactorial (OpFactorial x) -> return x
1582 _ -> na ("Lenses.opFactorial:" <++> pretty p)
1583 )
1584
1585
1586 opLex
1587 :: ( Op x :< x
1588 , Pretty x
1589 , MonadFailDoc m
1590 )
1591 => Proxy (m :: T.Type -> T.Type)
1592 -> ( (x -> x -> x, (x,x)) -> x
1593 , x -> m (x -> x -> x, (x,x))
1594 )
1595 opLex _ =
1596 ( \ (mk, (x,y)) -> mk x y
1597 , \ p -> case project p of
1598 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1599 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1600 _ -> na ("Lenses.opLex:" <++> pretty p)
1601 )
1602
1603
1604 opOrdering
1605 :: ( Op x :< x
1606 , Pretty x
1607 , MonadFailDoc m
1608 )
1609 => Proxy (m :: T.Type -> T.Type)
1610 -> ( (x -> x -> x, (x,x)) -> x
1611 , x -> m (x -> x -> x, (x,x))
1612 )
1613 opOrdering _ =
1614 ( \ (mk, (x,y)) -> mk x y
1615 , \ p -> case project p of
1616 Just (MkOpLt (OpLt x y)) -> return (\ x' y' -> inject (MkOpLt (OpLt x' y')), (x,y) )
1617 Just (MkOpLeq (OpLeq x y)) -> return (\ x' y' -> inject (MkOpLeq (OpLeq x' y')), (x,y) )
1618 Just (MkOpDotLt (OpDotLt x y)) -> return (\ x' y' -> inject (MkOpDotLt (OpDotLt x' y')), (x,y) )
1619 Just (MkOpDotLeq (OpDotLeq x y)) -> return (\ x' y' -> inject (MkOpDotLeq (OpDotLeq x' y')), (x,y) )
1620 Just (MkOpTildeLt (OpTildeLt x y)) -> return (\ x' y' -> inject (MkOpTildeLt (OpTildeLt x' y')), (x,y) )
1621 Just (MkOpTildeLeq (OpTildeLeq x y)) -> return (\ x' y' -> inject (MkOpTildeLeq (OpTildeLeq x' y')), (x,y) )
1622 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1623 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1624 _ -> na ("Lenses.opOrdering:" <++> pretty p)
1625 )
1626
1627
1628 fixTHParsing :: Data a => a -> a
1629 fixTHParsing p =
1630 let ?typeCheckerMode = RelaxedIntegerTags
1631 in fixRelationProj p
1632
1633
1634 fixRelationProj :: (Data a, ?typeCheckerMode :: TypeCheckerMode) => a -> a
1635 fixRelationProj= transformBi f
1636 where
1637 f :: Expression -> Expression
1638 f p =
1639 case match opRelationProj p of
1640 Just (func, [Just arg]) ->
1641 case typeOf func of
1642 Just TypeFunction{} -> make opImage func arg
1643 Just TypeSequence{} -> make opImage func arg
1644 Just TypePermutation{} -> make opImage func arg
1645 _ -> p
1646 Just (func, args) | arg <- catMaybes args, length arg == length args ->
1647 case typeOf func of
1648 Just TypeFunction{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1649 Just TypeSequence{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1650 Just TypePermutation{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1651 _ -> p
1652 _ -> p
1653
1654
1655
1656 maxOfDomain ::
1657 MonadFailDoc m =>
1658 Pretty r =>
1659 Domain r Expression -> m Expression
1660 maxOfDomain (DomainIntE _ x) = return $ make opMax x
1661 maxOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.maxOfDomain []"
1662 maxOfDomain (DomainInt _ [r]) = maxOfRange r
1663 maxOfDomain (DomainInt _ rs ) = do
1664 xs <- mapM maxOfRange rs
1665 return (make opMax (fromList xs))
1666 maxOfDomain (DomainReference _ (Just d)) = maxOfDomain d
1667 maxOfDomain d = failDoc ("rule_DomainMinMax.maxOfDomain" <+> pretty d)
1668
1669 maxOfRange :: MonadFailDoc m => Range Expression -> m Expression
1670 maxOfRange (RangeSingle x) = return x
1671 maxOfRange (RangeBounded _ x) = return x
1672 maxOfRange (RangeUpperBounded x) = return x
1673 maxOfRange r = failDoc ("rule_DomainMinMax.maxOfRange" <+> pretty (show r))
1674
1675 minOfDomain ::
1676 (?typeCheckerMode::TypeCheckerMode) =>
1677 MonadFailDoc m =>
1678 Pretty r =>
1679 Domain r Expression -> m Expression
1680 minOfDomain (DomainIntE _ x) = return $ make opMin x
1681 minOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.minOfDomain []"
1682 minOfDomain (DomainInt _ [r]) = minOfRange r
1683 minOfDomain (DomainInt _ rs ) = do
1684 xs <- mapM minOfRange rs
1685 return (make opMin (fromList xs))
1686 minOfDomain (DomainReference _ (Just d)) = minOfDomain d
1687 minOfDomain d = failDoc ("rule_DomainMinMax.minOfDomain" <+> pretty d)
1688
1689 minOfRange ::
1690 MonadFailDoc m =>
1691 Range Expression -> m Expression
1692 minOfRange (RangeSingle x) = return x
1693 minOfRange (RangeBounded x _) = return x
1694 minOfRange (RangeLowerBounded x) = return x
1695 minOfRange r = failDoc ("rule_DomainMinMax.minOfRange" <+> pretty (show r))