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 opPermutationOrderDelayed
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 opPermutationOrderDelayed _ =
465 ( \ x y -> inject $ MkOpPermutationOrderDelayed $ OpPermutationOrderDelayed x y
466 , \ p -> do
467 op <- project p
468 case op of
469 MkOpPermutationOrderDelayed (OpPermutationOrderDelayed x y) -> return (x,y)
470 _ -> na ("Lenses.opTransform:" <++> pretty p)
471 )
472
473 opPermutationOrderEager
474 :: ( Op x :< x
475 , Pretty x
476 , MonadFailDoc m
477 )
478 => Proxy (m :: T.Type -> T.Type)
479 -> ( [x] -> x -> x
480 , x -> m ([x], x)
481 )
482 opPermutationOrderEager _ =
483 ( \ x y -> inject $ MkOpPermutationOrderEager $ OpPermutationOrderEager x y
484 , \ p -> do
485 op <- project p
486 case op of
487 MkOpPermutationOrderEager (OpPermutationOrderEager x y) -> return (x,y)
488 _ -> na ("Lenses.opTransform:" <++> pretty p)
489 )
490
491 opRelationProj
492 :: ( Op x :< x
493 , Pretty x
494 , MonadFailDoc m
495 )
496 => Proxy (m :: T.Type -> T.Type)
497 -> ( x -> [Maybe x] -> x
498 , x -> m (x, [Maybe x])
499 )
500 opRelationProj _ =
501 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x ys
502 , \ p -> do
503 op <- project p
504 case op of
505 MkOpRelationProj (OpRelationProj x ys) -> return (x,ys)
506 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
507 )
508
509
510 opPermInverse
511 :: ( Op x :< x
512 , Pretty x
513 , MonadFailDoc m
514 )
515 => Proxy (m :: T.Type -> T.Type)
516 -> ( x -> x
517 , x -> m x
518 )
519 opPermInverse _ =
520 ( inject . MkOpPermInverse . OpPermInverse
521 , \ p -> do
522 op <- project p
523 case op of
524 MkOpPermInverse (OpPermInverse x) -> return x
525 _ -> na ("Lenses.opPermInverse:" <++> pretty p)
526 )
527
528
529 opRelationImage
530 :: ( Op x :< x
531 , Pretty x
532 , MonadFailDoc m
533 )
534 => Proxy (m :: T.Type -> T.Type)
535 -> ( x -> [x] -> x
536 , x -> m (x, [x])
537 )
538 opRelationImage _ =
539 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x (map Just ys)
540 , \ p -> do
541 op <- project p
542 case op of
543 MkOpRelationProj (OpRelationProj x ys)
544 | let ys' = catMaybes ys
545 , length ys' == length ys -- they were all Just's
546 -> return (x,ys')
547 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
548 )
549
550
551 opIndexing
552 :: ( Op x :< x
553 , Pretty x
554 , MonadFailDoc m
555 )
556 => Proxy (m :: T.Type -> T.Type)
557 -> ( x -> x -> x
558 , x -> m (x,x)
559 )
560 opIndexing _ =
561 ( \ x y -> inject (MkOpIndexing (OpIndexing x y))
562 , \ p -> do
563 op <- project p
564 case op of
565 MkOpIndexing (OpIndexing x y) -> return (x,y)
566 _ -> na ("Lenses.opIndexing:" <++> pretty p)
567 )
568
569
570 opMatrixIndexing
571 :: ( Op x :< x
572 , Pretty x
573 , TypeOf x
574 , MonadFailDoc m
575 , ?typeCheckerMode :: TypeCheckerMode
576 )
577 => Proxy (m :: T.Type -> T.Type)
578 -> ( x -> [x] -> x
579 , x -> m (x,[x])
580 )
581 opMatrixIndexing _ =
582 ( foldl (make opIndexing)
583 , \ p -> do
584 (m, is) <- go p
585 if null is
586 then na ("Lenses.opMatrixIndexing:" <+> pretty p)
587 else return (m, is)
588 )
589 where
590 go p = case project p of
591 Just (MkOpIndexing (OpIndexing x i)) -> do
592 ty <- typeOf x
593 case ty of
594 TypeMatrix{} -> return ()
595 TypeList{} -> return ()
596 _ -> na ("Lenses.opMatrixIndexing:" <+> pretty p)
597 (m,is) <- go x
598 return (m, is ++ [i])
599 _ -> return (p, [])
600
601
602 opMatrixIndexingSlicing
603 :: ( Op x :< x
604 , Pretty x
605 , MonadFailDoc m
606 , TypeOf x
607 , ?typeCheckerMode :: TypeCheckerMode
608 )
609 => Proxy (m :: T.Type -> T.Type)
610 -> ( x -> [Either x (Maybe x, Maybe x)] -> x
611 , x -> m (x, [Either x (Maybe x, Maybe x)]) -- either an index or a slice
612 )
613 opMatrixIndexingSlicing _ =
614 ( mk
615 , \ p -> do
616 (m, is, wasThereAnySlicing) <- go p
617 if not (null is) && wasThereAnySlicing
618 then return (m, is)
619 else na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
620 )
621 where
622 mk m [] = m
623 mk m (Left i:is) = mk (make opIndexing m i) is
624 mk m (Right (lb, ub):is) = mk (make opSlicing m lb ub) is
625
626 go p = case project p of
627 Just (MkOpIndexing (OpIndexing x i)) -> do
628 ty <- typeOf x
629 case ty of
630 TypeMatrix{} -> return ()
631 TypeList{} -> return ()
632 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
633 (m, is, wasThereAnySlicing) <- go x
634 return (m, is ++ [Left i], wasThereAnySlicing)
635 Just (MkOpSlicing (OpSlicing x lb ub)) -> do
636 ty <- typeOf x
637 case ty of
638 TypeMatrix{} -> return ()
639 TypeList{} -> return ()
640 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
641 (m, is, _) <- go x
642 return (m, is ++ [Right (lb, ub)], True)
643 _ -> return (p, [], False)
644
645
646 opSlicing
647 :: ( Op x :< x
648 , Pretty x
649 , MonadFailDoc m
650 )
651 => Proxy (m :: T.Type -> T.Type)
652 -> ( x -> Maybe x -> Maybe x -> x
653 , x -> m (x, Maybe x, Maybe x)
654 )
655 opSlicing _ =
656 ( \ x y z -> inject (MkOpSlicing (OpSlicing x y z))
657 , \ p -> do
658 op <- project p
659 case op of
660 MkOpSlicing (OpSlicing x y z) -> return (x,y,z)
661 _ -> na ("Lenses.opSlicing:" <++> pretty p)
662 )
663
664
665 opFlatten
666 :: ( Op x :< x
667 , Pretty x
668 , MonadFailDoc m
669 )
670 => Proxy (m :: T.Type -> T.Type)
671 -> ( x -> x
672 , x -> m x
673 )
674 opFlatten _ =
675 ( inject . MkOpFlatten . OpFlatten Nothing
676 , \ p -> do
677 op <- project p
678 case op of
679 MkOpFlatten (OpFlatten Nothing x) -> return x
680 _ -> na ("Lenses.opFlatten:" <++> pretty p)
681 )
682
683
684 flattenIfNeeded ::
685 Int ->
686 Expression ->
687 Expression
688 flattenIfNeeded dims m =
689 if dims > 1
690 then make opFlatten m
691 else m
692
693
694 oneDimensionaliser ::
695 Int -> -- current number of dimensions
696 Expression ->
697 Expression
698 oneDimensionaliser dims x =
699 case dims of
700 0 -> fromList [x]
701 1 -> x
702 _ -> make opFlatten x
703
704
705 opConcatenate
706 :: ( Op x :< x
707 , Pretty x
708 , MonadFailDoc m
709 )
710 => Proxy (m :: T.Type -> T.Type)
711 -> ( x -> x
712 , x -> m x
713 )
714 opConcatenate _ =
715 ( inject . MkOpFlatten . OpFlatten (Just 1)
716 , \ p -> do
717 op <- project p
718 case op of
719 MkOpFlatten (OpFlatten (Just 1) x) -> return x
720 _ -> na ("Lenses.opConcatenate:" <++> pretty p)
721 )
722
723
724 opIn
725 :: ( Op x :< x
726 , Pretty x
727 , MonadFailDoc m
728 )
729 => Proxy (m :: T.Type -> T.Type)
730 -> ( x -> x -> x
731 , x -> m (x,x)
732 )
733 opIn _ =
734 ( \ x y -> inject (MkOpIn (OpIn x y))
735 , \ p -> do
736 op <- project p
737 case op of
738 MkOpIn (OpIn x y) -> return (x,y)
739 _ -> na ("Lenses.opIn:" <++> pretty p)
740 )
741
742
743 opFreq
744 :: ( Op x :< x
745 , Pretty x
746 , MonadFailDoc m
747 )
748 => Proxy (m :: T.Type -> T.Type)
749 -> ( x -> x -> x
750 , x -> m (x,x)
751 )
752 opFreq _ =
753 ( \ x y -> inject (MkOpFreq (OpFreq x y))
754 , \ p -> do
755 op <- project p
756 case op of
757 MkOpFreq (OpFreq x y) -> return (x,y)
758 _ -> na ("Lenses.opFreq:" <++> pretty p)
759 )
760
761
762 opHist
763 :: ( Op x :< x
764 , Pretty x
765 , MonadFailDoc m
766 )
767 => Proxy (m :: T.Type -> T.Type)
768 -> ( x -> x
769 , x -> m x
770 )
771 opHist _ =
772 ( inject . MkOpHist . OpHist
773 , \ p -> do
774 op <- project p
775 case op of
776 MkOpHist (OpHist x) -> return x
777 _ -> na ("Lenses.opHist:" <++> pretty p)
778 )
779
780
781 opIntersect
782 :: ( Op x :< x
783 , Pretty x
784 , MonadFailDoc m
785 )
786 => Proxy (m :: T.Type -> T.Type)
787 -> ( x -> x -> x
788 , x -> m (x,x)
789 )
790 opIntersect _ =
791 ( \ x y -> inject (MkOpIntersect (OpIntersect x y))
792 , \ p -> do
793 op <- project p
794 case op of
795 MkOpIntersect (OpIntersect x y) -> return (x,y)
796 _ -> na ("Lenses.opIntersect:" <++> pretty p)
797 )
798
799
800 opUnion
801 :: ( Op x :< x
802 , Pretty x
803 , MonadFailDoc m
804 )
805 => Proxy (m :: T.Type -> T.Type)
806 -> ( x -> x -> x
807 , x -> m (x,x)
808 )
809 opUnion _ =
810 ( \ x y -> inject (MkOpUnion (OpUnion x y))
811 , \ p -> do
812 op <- project p
813 case op of
814 MkOpUnion (OpUnion x y) -> return (x,y)
815 _ -> na ("Lenses.opUnion:" <++> pretty p)
816 )
817
818
819 opSubsetEq
820 :: ( Op x :< x
821 , Pretty x
822 , MonadFailDoc m
823 )
824 => Proxy (m :: T.Type -> T.Type)
825 -> ( x -> x -> x
826 , x -> m (x,x)
827 )
828 opSubsetEq _ =
829 ( \ x y -> inject (MkOpSubsetEq (OpSubsetEq x y))
830 , \ p -> do
831 op <- project p
832 case op of
833 MkOpSubsetEq (OpSubsetEq x y) -> return (x,y)
834 _ -> na ("Lenses.opSubsetEq:" <++> pretty p)
835 )
836
837
838 opEq
839 :: ( Op x :< x
840 , Pretty x
841 , MonadFailDoc m
842 )
843 => Proxy (m :: T.Type -> T.Type)
844 -> ( x -> x -> x
845 , x -> m (x,x)
846 )
847 opEq _ =
848 ( \ x y -> inject (MkOpEq (OpEq x y))
849 , \ p -> do
850 op <- project p
851 case op of
852 MkOpEq (OpEq x y) -> return (x,y)
853 _ -> na ("Lenses.opEq:" <++> pretty p)
854 )
855
856
857 opNeq
858 :: ( Op x :< x
859 , Pretty x
860 , MonadFailDoc m
861 )
862 => Proxy (m :: T.Type -> T.Type)
863 -> ( x -> x -> x
864 , x -> m (x,x)
865 )
866 opNeq _ =
867 ( \ x y -> inject (MkOpNeq (OpNeq x y))
868 , \ p -> do
869 op <- project p
870 case op of
871 MkOpNeq (OpNeq x y) -> return (x,y)
872 _ -> na ("Lenses.opNeq:" <++> pretty p)
873 )
874
875
876 opLt
877 :: ( Op x :< x
878 , Pretty x
879 , MonadFailDoc m
880 )
881 => Proxy (m :: T.Type -> T.Type)
882 -> ( x -> x -> x
883 , x -> m (x,x)
884 )
885 opLt _ =
886 ( \ x y -> inject (MkOpLt (OpLt x y))
887 , \ p -> do
888 op <- project p
889 case op of
890 MkOpLt (OpLt x y) -> return (x,y)
891 _ -> na ("Lenses.opLt:" <++> pretty p)
892 )
893
894
895 opLeq
896 :: ( Op x :< x
897 , Pretty x
898 , MonadFailDoc m
899 )
900 => Proxy (m :: T.Type -> T.Type)
901 -> ( x -> x -> x
902 , x -> m (x,x)
903 )
904 opLeq _ =
905 ( \ x y -> inject (MkOpLeq (OpLeq x y))
906 , \ p -> do
907 op <- project p
908 case op of
909 MkOpLeq (OpLeq x y) -> return (x,y)
910 _ -> na ("Lenses.opLeq:" <++> pretty p)
911 )
912
913
914 opGt
915 :: ( Op x :< x
916 , Pretty x
917 , MonadFailDoc m
918 )
919 => Proxy (m :: T.Type -> T.Type)
920 -> ( x -> x -> x
921 , x -> m (x,x)
922 )
923 opGt _ =
924 ( \ x y -> inject (MkOpGt (OpGt x y))
925 , \ p -> do
926 op <- project p
927 case op of
928 MkOpGt (OpGt x y) -> return (x,y)
929 _ -> na ("Lenses.opGt:" <++> pretty p)
930 )
931
932
933 opGeq
934 :: ( Op x :< x
935 , Pretty x
936 , MonadFailDoc m
937 )
938 => Proxy (m :: T.Type -> T.Type)
939 -> ( x -> x -> x
940 , x -> m (x,x)
941 )
942 opGeq _ =
943 ( \ x y -> inject (MkOpGeq (OpGeq x y))
944 , \ p -> do
945 op <- project p
946 case op of
947 MkOpGeq (OpGeq x y) -> return (x,y)
948 _ -> na ("Lenses.opGeq:" <++> pretty p)
949 )
950
951
952 opDotLt
953 :: ( Op x :< x
954 , Pretty x
955 , MonadFailDoc m
956 )
957 => Proxy (m :: T.Type -> T.Type)
958 -> ( x -> x -> x
959 , x -> m (x,x)
960 )
961 opDotLt _ =
962 ( \ x y -> inject (MkOpDotLt (OpDotLt x y))
963 , \ p -> do
964 op <- project p
965 case op of
966 MkOpDotLt (OpDotLt x y) -> return (x,y)
967 _ -> na ("Lenses.opDotLt:" <++> pretty p)
968 )
969
970
971 opDotLeq
972 :: ( Op x :< x
973 , Pretty x
974 , MonadFailDoc m
975 )
976 => Proxy (m :: T.Type -> T.Type)
977 -> ( x -> x -> x
978 , x -> m (x,x)
979 )
980 opDotLeq _ =
981 ( \ x y -> inject (MkOpDotLeq (OpDotLeq x y))
982 , \ p -> do
983 op <- project p
984 case op of
985 MkOpDotLeq (OpDotLeq x y) -> return (x,y)
986 _ -> na ("Lenses.opDotLeq:" <++> pretty p)
987 )
988
989
990 opTildeLt
991 :: ( Op x :< x
992 , Pretty x
993 , MonadFailDoc m
994 )
995 => Proxy (m :: T.Type -> T.Type)
996 -> ( x -> x -> x
997 , x -> m (x,x)
998 )
999 opTildeLt _ =
1000 ( \ x y -> inject (MkOpTildeLt (OpTildeLt x y))
1001 , \ p -> do
1002 op <- project p
1003 case op of
1004 MkOpTildeLt (OpTildeLt x y) -> return (x,y)
1005 _ -> na ("Lenses.opTildeLt:" <++> pretty p)
1006 )
1007
1008
1009 opTildeLeq
1010 :: ( Op x :< x
1011 , Pretty x
1012 , MonadFailDoc m
1013 )
1014 => Proxy (m :: T.Type -> T.Type)
1015 -> ( x -> x -> x
1016 , x -> m (x,x)
1017 )
1018 opTildeLeq _ =
1019 ( \ x y -> inject (MkOpTildeLeq (OpTildeLeq x y))
1020 , \ p -> do
1021 op <- project p
1022 case op of
1023 MkOpTildeLeq (OpTildeLeq x y) -> return (x,y)
1024 _ -> na ("Lenses.opTildeLeq:" <++> pretty p)
1025 )
1026
1027
1028 opOr
1029 :: ( Op x :< x
1030 , Pretty x
1031 , MonadFailDoc m
1032 )
1033 => Proxy (m :: T.Type -> T.Type)
1034 -> ( x -> x
1035 , x -> m x
1036 )
1037 opOr _ =
1038 ( inject . MkOpOr . OpOr
1039 , \ p -> do
1040 op <- project p
1041 case op of
1042 MkOpOr (OpOr xs) -> return xs
1043 _ -> na ("Lenses.opOr:" <++> pretty p)
1044 )
1045
1046
1047 opAnd
1048 :: ( Op x :< x
1049 , Pretty x
1050 , MonadFailDoc m
1051 )
1052 => Proxy (m :: T.Type -> T.Type)
1053 -> ( x -> x
1054 , x -> m x
1055 )
1056 opAnd _ =
1057 ( inject . MkOpAnd . OpAnd
1058 , \ p -> do
1059 op <- project p
1060 case op of
1061 MkOpAnd (OpAnd xs) -> return xs
1062 _ -> na ("Lenses.opAnd:" <++> pretty p)
1063 )
1064
1065
1066 opMax
1067 :: ( Op x :< x
1068 , Pretty x
1069 , MonadFailDoc m
1070 )
1071 => Proxy (m :: T.Type -> T.Type)
1072 -> ( x -> x
1073 , x -> m x
1074 )
1075 opMax _ =
1076 ( inject . MkOpMax . OpMax
1077 , \ p -> do
1078 op <- project p
1079 case op of
1080 MkOpMax (OpMax xs) -> return xs
1081 _ -> na ("Lenses.opMax:" <++> pretty p)
1082 )
1083
1084
1085 opMin
1086 :: ( Op x :< x
1087 , Pretty x
1088 , MonadFailDoc m
1089 )
1090 => Proxy (m :: T.Type -> T.Type)
1091 -> ( x -> x
1092 , x -> m x
1093 )
1094 opMin _ =
1095 ( inject . MkOpMin . OpMin
1096 , \ p -> do
1097 op <- project p
1098 case op of
1099 MkOpMin (OpMin xs) -> return xs
1100 _ -> na ("Lenses.opMin:" <++> pretty p)
1101 )
1102
1103
1104 opImply
1105 :: ( Op x :< x
1106 , Pretty x
1107 , MonadFailDoc m
1108 )
1109 => Proxy (m :: T.Type -> T.Type)
1110 -> ( x -> x -> x
1111 , x -> m (x,x)
1112 )
1113 opImply _ =
1114 ( \ x y -> inject (MkOpImply (OpImply x y))
1115 , \ p -> do
1116 op <- project p
1117 case op of
1118 MkOpImply (OpImply x y) -> return (x,y)
1119 _ -> na ("Lenses.opImply:" <++> pretty p)
1120 )
1121
1122
1123 opNot
1124 :: ( Op x :< x
1125 , Pretty x
1126 , MonadFailDoc m
1127 )
1128 => Proxy (m :: T.Type -> T.Type)
1129 -> ( x -> x
1130 , x -> m x
1131 )
1132 opNot _ =
1133 ( inject . MkOpNot . OpNot
1134 , \ p -> do
1135 op <- project p
1136 case op of
1137 MkOpNot (OpNot x) -> return x
1138 _ -> na ("Lenses.opNot:" <++> pretty p)
1139 )
1140
1141
1142 opProduct
1143 :: ( Op x :< x
1144 , Pretty x
1145 , MonadFailDoc m
1146 )
1147 => Proxy (m :: T.Type -> T.Type)
1148 -> ( x -> x
1149 , x -> m x
1150 )
1151 opProduct _ =
1152 ( inject . MkOpProduct . OpProduct
1153 , \ p -> do
1154 op <- project p
1155 case op of
1156 MkOpProduct (OpProduct x) -> return x
1157 _ -> na ("Lenses.opProduct:" <++> pretty p)
1158 )
1159
1160
1161 opSum
1162 :: ( Op x :< x
1163 , Pretty x
1164 , MonadFailDoc m
1165 )
1166 => Proxy (m :: T.Type -> T.Type)
1167 -> ( x -> x
1168 , x -> m x
1169 )
1170 opSum _ =
1171 ( inject . MkOpSum . OpSum
1172 , \ p -> do
1173 op <- project p
1174 case op of
1175 MkOpSum (OpSum x) -> return x
1176 _ -> na ("Lenses.opSum:" <++> pretty p)
1177 )
1178
1179
1180 data ReducerType = RepetitionIsNotSignificant | RepetitionIsSignificant
1181 deriving (Eq, Ord, Show)
1182
1183 opReducer
1184 :: ( Op x :< x
1185 , Pretty x
1186 , MonadFailDoc m
1187 )
1188 => Proxy (m :: T.Type -> T.Type)
1189 -> ( (x -> x, x) -> x
1190 , x -> m ( ReducerType
1191 , Bool -- defined on []
1192 , x -> x
1193 , x
1194 )
1195 )
1196 opReducer _ =
1197 ( \ (mk, x) -> mk x
1198 , \ p -> do
1199 op <- project p
1200 let is = RepetitionIsSignificant
1201 let isn't = RepetitionIsNotSignificant
1202 case op of
1203 MkOpAnd (OpAnd x) -> return (isn't, True , inject . MkOpAnd . OpAnd , x)
1204 MkOpOr (OpOr x) -> return (isn't, True , inject . MkOpOr . OpOr , x)
1205 MkOpXor (OpXor x) -> return (is , False, inject . MkOpXor . OpXor , x)
1206 MkOpSum (OpSum x) -> return (is , True , inject . MkOpSum . OpSum , x)
1207 MkOpProduct (OpProduct x) -> return (is , True , inject . MkOpProduct . OpProduct , x)
1208 MkOpMax (OpMax x) -> return (isn't, False, inject . MkOpMax . OpMax , x)
1209 MkOpMin (OpMin x) -> return (isn't, False, inject . MkOpMin . OpMin , x)
1210 _ -> na ("Lenses.opReducer:" <++> pretty p)
1211 )
1212
1213
1214 opModifier
1215 :: ( Op x :< x
1216 , MonadFailDoc m
1217 )
1218 => Proxy (m :: T.Type -> T.Type)
1219 -> ( (x -> x, x) -> x
1220 , x -> m (x -> x, x)
1221 )
1222 opModifier _ =
1223 ( \ (mk, x) -> mk x
1224 , \ p -> case project p of
1225 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1226 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1227 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1228 Just (MkOpParts (OpParts x)) -> return (inject . MkOpParts . OpParts , x)
1229 _ -> return (id , p)
1230 )
1231
1232
1233 opModifierNoP
1234 :: ( Op x :< x
1235 , MonadFailDoc m
1236 )
1237 => Proxy (m :: T.Type -> T.Type)
1238 -> ( (x -> x, x) -> x
1239 , x -> m (x -> x, x)
1240 )
1241 opModifierNoP _ =
1242 ( \ (mk, x) -> mk x
1243 , \ p -> case project p of
1244 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1245 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1246 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1247 _ -> return (id , p)
1248 )
1249
1250
1251 opAllDiff
1252 :: ( Op x :< x
1253 , Pretty x
1254 , MonadFailDoc m
1255 )
1256 => Proxy (m :: T.Type -> T.Type)
1257 -> ( x -> x
1258 , x -> m x
1259 )
1260 opAllDiff _ =
1261 ( inject . MkOpAllDiff . OpAllDiff
1262 , \ p -> do
1263 op <- project p
1264 case op of
1265 MkOpAllDiff (OpAllDiff x) -> return x
1266 _ -> na ("Lenses.opAllDiff:" <++> pretty p)
1267 )
1268
1269
1270 opAllDiffExcept
1271 :: ( Op x :< x
1272 , Pretty x
1273 , MonadFailDoc m
1274 )
1275 => Proxy (m :: T.Type -> T.Type)
1276 -> ( x -> x -> x
1277 , x -> m (x, x)
1278 )
1279 opAllDiffExcept _ =
1280 ( \ x y -> inject $ MkOpAllDiffExcept $ OpAllDiffExcept x y
1281 , \ p -> do
1282 op <- project p
1283 case op of
1284 MkOpAllDiffExcept (OpAllDiffExcept x y) -> return (x, y)
1285 _ -> na ("Lenses.opAllDiffExcept:" <++> pretty p)
1286 )
1287
1288
1289 constantInt
1290 :: MonadFailDoc m
1291 => Proxy (m :: T.Type -> T.Type)
1292 -> ( Integer -> Expression
1293 , Expression -> m Integer
1294 )
1295 constantInt _ =
1296 ( Constant . ConstantInt TagInt
1297 , \ p -> case p of
1298 (Constant (ConstantInt TagInt i)) -> return i
1299 _ -> na ("Lenses.constantInt:" <++> pretty p)
1300 )
1301
1302
1303
1304 matrixLiteral
1305 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1306 => Proxy (m :: T.Type -> T.Type)
1307 -> ( Type -> Domain () Expression -> [Expression] -> Expression
1308 , Expression -> m (Type, Domain () Expression, [Expression])
1309 )
1310 matrixLiteral _ =
1311 ( \ ty index elems ->
1312 if null elems
1313 then Typed (AbstractLiteral (AbsLitMatrix index elems)) ty
1314 else AbstractLiteral (AbsLitMatrix index elems)
1315 , \ p -> do
1316 ty <- typeOf p
1317 (index, xs) <- followAliases extract p
1318 return (ty, index, xs)
1319 )
1320 where
1321 extract (Constant (ConstantAbstract (AbsLitMatrix index xs))) = return (fmap Constant index, map Constant xs)
1322 extract (AbstractLiteral (AbsLitMatrix index xs)) = return (index, xs)
1323 extract (Typed x _) = extract x
1324 extract (Constant (TypedConstant x _)) = extract (Constant x)
1325 extract p = na ("Lenses.matrixLiteral:" <+> pretty p)
1326
1327
1328 onMatrixLiteral
1329 :: (Functor m, Applicative m, Monad m, NameGen m)
1330 => Maybe Int -- how many levels to go down. all the way if Nothing.
1331 -> (Expression -> m Expression)
1332 -> Expression -> m Expression
1333 onMatrixLiteral mlvl f = case mlvl of
1334 Nothing -> followAliases go
1335 Just lvl -> followAliases (goL lvl)
1336 where
1337 go (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1338 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (go . Constant) xs
1339 go (AbstractLiteral (AbsLitMatrix index xs)) =
1340 AbstractLiteral . AbsLitMatrix index <$> mapM go xs
1341 go (Typed x _) = go x
1342 go (Constant (TypedConstant x _)) = go (Constant x)
1343 go p = f p
1344
1345 goL 0 p = f p
1346 goL lvl (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1347 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (goL (lvl-1) . Constant) xs
1348 goL lvl (AbstractLiteral (AbsLitMatrix index xs)) =
1349 AbstractLiteral . AbsLitMatrix index <$> mapM (goL (lvl-1)) xs
1350 goL lvl (Typed x _) = goL lvl x
1351 goL lvl (Constant (TypedConstant x _)) = goL lvl (Constant x)
1352 goL lvl p = do
1353 (iPat, i) <- quantifiedVar
1354 body <- goL (lvl-1) i
1355 return $ Comprehension body [Generator (GenInExpr iPat p)]
1356
1357
1358 setLiteral
1359 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1360 => Proxy (m :: T.Type -> T.Type)
1361 -> ( Type -> [Expression] -> Expression
1362 , Expression -> m (Type, [Expression])
1363 )
1364 setLiteral _ =
1365 ( \ ty elems ->
1366 if null elems
1367 then Typed (AbstractLiteral (AbsLitSet elems)) ty
1368 else AbstractLiteral (AbsLitSet elems)
1369 , \ p -> do
1370 ty <- typeOf p
1371 xs <- followAliases extract p
1372 return (ty, xs)
1373 )
1374 where
1375 extract (Constant (viewConstantSet -> Just xs)) = return (map Constant xs)
1376 extract (AbstractLiteral (AbsLitSet xs)) = return xs
1377 extract (Typed x _) = extract x
1378 extract (Constant (TypedConstant x _)) = extract (Constant x)
1379 extract p = na ("Lenses.setLiteral:" <+> pretty p)
1380
1381
1382 msetLiteral
1383 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1384 => Proxy (m :: T.Type -> T.Type)
1385 -> ( Type -> [Expression] -> Expression
1386 , Expression -> m (Type, [Expression])
1387 )
1388 msetLiteral _ =
1389 ( \ ty elems ->
1390 if null elems
1391 then Typed (AbstractLiteral (AbsLitMSet elems)) ty
1392 else AbstractLiteral (AbsLitMSet elems)
1393 , \ p -> do
1394 ty <- typeOf p
1395 xs <- followAliases extract p
1396 return (ty, xs)
1397 )
1398 where
1399 extract (Constant (viewConstantMSet -> Just xs)) = return (map Constant xs)
1400 extract (AbstractLiteral (AbsLitMSet xs)) = return xs
1401 extract (Typed x _) = extract x
1402 extract (Constant (TypedConstant x _)) = extract (Constant x)
1403 extract p = na ("Lenses.msetLiteral:" <+> pretty p)
1404
1405
1406 functionLiteral
1407 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1408 => Proxy (m :: T.Type -> T.Type)
1409 -> ( Type -> [(Expression,Expression)] -> Expression
1410 , Expression -> m (Type, [(Expression,Expression)])
1411 )
1412 functionLiteral _ =
1413 ( \ ty elems ->
1414 if null elems
1415 then Typed (AbstractLiteral (AbsLitFunction elems)) ty
1416 else AbstractLiteral (AbsLitFunction elems)
1417 , \ p -> do
1418 ty <- typeOf p
1419 xs <- followAliases extract p
1420 return (ty, xs)
1421 )
1422 where
1423 extract (Constant (viewConstantFunction -> Just xs)) = return [ (Constant a, Constant b) | (a,b) <- xs ]
1424 extract (AbstractLiteral (AbsLitFunction xs)) = return xs
1425 extract (Typed x _) = extract x
1426 extract (Constant (TypedConstant x _)) = extract (Constant x)
1427 extract p = na ("Lenses.functionLiteral:" <+> pretty p)
1428
1429
1430 permutationLiteral
1431 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1432 => Proxy (m :: T.Type -> T.Type )
1433 -> ( Type -> [[Expression]] -> Expression
1434 , Expression -> m (Type, [[Expression]])
1435 )
1436 permutationLiteral _ =
1437 ( \ ty elems ->
1438 if null elems
1439 then Typed (AbstractLiteral (AbsLitPermutation elems)) ty
1440 else AbstractLiteral (AbsLitPermutation elems)
1441 , \ p -> do
1442 ty <- typeOf p
1443 xs <- followAliases extract p
1444 return (ty, xs)
1445 )
1446 where
1447 extract (Constant (ConstantAbstract (AbsLitPermutation xs))) = return [ [Constant z | z <- x] | x <- xs ]
1448 extract (AbstractLiteral (AbsLitPermutation xs)) = return xs
1449 extract (Typed x _) = extract x
1450 extract (Constant (TypedConstant x _)) = extract (Constant x)
1451 extract p = na ("Lenses.permutationLiteral:" <+> pretty p)
1452
1453
1454
1455
1456 sequenceLiteral
1457 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1458 => Proxy (m :: T.Type -> T.Type)
1459 -> ( Type -> [Expression] -> Expression
1460 , Expression -> m (Type, [Expression])
1461 )
1462 sequenceLiteral _ =
1463 ( \ ty elems ->
1464 if null elems
1465 then Typed (AbstractLiteral (AbsLitSequence elems)) ty
1466 else AbstractLiteral (AbsLitSequence elems)
1467 , \ p -> do
1468 ty <- typeOf p
1469 xs <- followAliases extract p
1470 return (ty, xs)
1471 )
1472 where
1473 extract (Constant (viewConstantSequence -> Just xs)) = return (map Constant xs)
1474 extract (AbstractLiteral (AbsLitSequence xs)) = return xs
1475 extract (Typed x _) = extract x
1476 extract (Constant (TypedConstant x _)) = extract (Constant x)
1477 extract p = na ("Lenses.sequenceLiteral:" <+> pretty p)
1478
1479
1480 relationLiteral
1481 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1482 => Proxy (m :: T.Type -> T.Type)
1483 -> ( Type -> [[Expression]] -> Expression
1484 , Expression -> m (Type, [[Expression]])
1485 )
1486 relationLiteral _ =
1487 ( \ ty elems ->
1488 if null elems
1489 then Typed (AbstractLiteral (AbsLitRelation elems)) ty
1490 else AbstractLiteral (AbsLitRelation elems)
1491 , \ p -> do
1492 ty <- typeOf p
1493 xs <- followAliases extract p
1494 return (ty, xs)
1495 )
1496 where
1497 extract (Constant (viewConstantRelation -> Just xs)) = return (map (map Constant) xs)
1498 extract (AbstractLiteral (AbsLitRelation xs)) = return xs
1499 extract (Typed x _) = extract x
1500 extract (Constant (TypedConstant x _)) = extract (Constant x)
1501 extract p = na ("Lenses.relationLiteral:" <+> pretty p)
1502
1503
1504 partitionLiteral
1505 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1506 => Proxy (m :: T.Type -> T.Type)
1507 -> ( Type -> [[Expression]] -> Expression
1508 , Expression -> m (Type, [[Expression]])
1509 )
1510 partitionLiteral _ =
1511 ( \ ty elems ->
1512 if null elems
1513 then Typed (AbstractLiteral (AbsLitPartition elems)) ty
1514 else AbstractLiteral (AbsLitPartition elems)
1515 , \ p -> do
1516 ty <- typeOf p
1517 xs <- followAliases extract p
1518 return (ty, xs)
1519 )
1520 where
1521 extract (Constant (viewConstantPartition -> Just xs)) = return (map (map Constant) xs)
1522 extract (AbstractLiteral (AbsLitPartition xs)) = return xs
1523 extract (Typed x _) = extract x
1524 extract (Constant (TypedConstant x _)) = extract (Constant x)
1525 extract p = na ("Lenses.partitionLiteral:" <+> pretty p)
1526
1527
1528 opTwoBars
1529 :: ( Op x :< x
1530 , Pretty x
1531 , MonadFailDoc m
1532 )
1533 => Proxy (m :: T.Type -> T.Type)
1534 -> ( x -> x
1535 , x -> m x
1536 )
1537 opTwoBars _ =
1538 ( inject . MkOpTwoBars . OpTwoBars
1539 , \ p -> do
1540 op <- project p
1541 case op of
1542 MkOpTwoBars (OpTwoBars x) -> return x
1543 _ -> na ("Lenses.opTwoBars:" <++> pretty p)
1544 )
1545
1546
1547 opPreImage
1548 :: ( Op x :< x
1549 , Pretty x
1550 , MonadFailDoc m
1551 )
1552 => Proxy (m :: T.Type -> T.Type)
1553 -> ( x -> x -> x
1554 , x -> m (x,x)
1555 )
1556 opPreImage _ =
1557 ( \ x y -> inject (MkOpPreImage (OpPreImage x y))
1558 , \ p -> do
1559 op <- project p
1560 case op of
1561 MkOpPreImage (OpPreImage x y) -> return (x,y)
1562 _ -> na ("Lenses.opPreImage:" <++> pretty p)
1563 )
1564
1565
1566 opActive
1567 :: ( Op x :< x
1568 , Pretty x
1569 , MonadFailDoc m
1570 )
1571 => Proxy (m :: T.Type -> T.Type)
1572 -> ( x -> Name -> x
1573 , x -> m (x,Name)
1574 )
1575 opActive _ =
1576 ( \ x y -> inject (MkOpActive (OpActive x y))
1577 , \ p -> do
1578 op <- project p
1579 case op of
1580 MkOpActive (OpActive x y) -> return (x,y)
1581 _ -> na ("Lenses.opActive:" <++> pretty p)
1582 )
1583
1584
1585 opFactorial
1586 :: ( Op x :< x
1587 , Pretty x
1588 , MonadFailDoc m
1589 )
1590 => Proxy (m :: T.Type -> T.Type)
1591 -> ( x -> x
1592 , x -> m x
1593 )
1594 opFactorial _ =
1595 ( inject . MkOpFactorial . OpFactorial
1596 , \ p -> do
1597 op <- project p
1598 case op of
1599 MkOpFactorial (OpFactorial x) -> return x
1600 _ -> na ("Lenses.opFactorial:" <++> pretty p)
1601 )
1602
1603
1604 opLex
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 opLex _ =
1614 ( \ (mk, (x,y)) -> mk x y
1615 , \ p -> case project p of
1616 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1617 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1618 _ -> na ("Lenses.opLex:" <++> pretty p)
1619 )
1620
1621
1622 opOrdering
1623 :: ( Op x :< x
1624 , Pretty x
1625 , MonadFailDoc m
1626 )
1627 => Proxy (m :: T.Type -> T.Type)
1628 -> ( (x -> x -> x, (x,x)) -> x
1629 , x -> m (x -> x -> x, (x,x))
1630 )
1631 opOrdering _ =
1632 ( \ (mk, (x,y)) -> mk x y
1633 , \ p -> case project p of
1634 Just (MkOpLt (OpLt x y)) -> return (\ x' y' -> inject (MkOpLt (OpLt x' y')), (x,y) )
1635 Just (MkOpLeq (OpLeq x y)) -> return (\ x' y' -> inject (MkOpLeq (OpLeq x' y')), (x,y) )
1636 Just (MkOpDotLt (OpDotLt x y)) -> return (\ x' y' -> inject (MkOpDotLt (OpDotLt x' y')), (x,y) )
1637 Just (MkOpDotLeq (OpDotLeq x y)) -> return (\ x' y' -> inject (MkOpDotLeq (OpDotLeq x' y')), (x,y) )
1638 Just (MkOpTildeLt (OpTildeLt x y)) -> return (\ x' y' -> inject (MkOpTildeLt (OpTildeLt x' y')), (x,y) )
1639 Just (MkOpTildeLeq (OpTildeLeq x y)) -> return (\ x' y' -> inject (MkOpTildeLeq (OpTildeLeq x' y')), (x,y) )
1640 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1641 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1642 _ -> na ("Lenses.opOrdering:" <++> pretty p)
1643 )
1644
1645
1646 fixTHParsing :: Data a => a -> a
1647 fixTHParsing p =
1648 let ?typeCheckerMode = RelaxedIntegerTags
1649 in fixRelationProj p
1650
1651
1652 fixRelationProj :: (Data a, ?typeCheckerMode :: TypeCheckerMode) => a -> a
1653 fixRelationProj= transformBi f
1654 where
1655 f :: Expression -> Expression
1656 f p =
1657 case match opRelationProj p of
1658 Just (func, [Just arg]) ->
1659 case typeOf func of
1660 Just TypeFunction{} -> make opImage func arg
1661 Just TypeSequence{} -> make opImage func arg
1662 Just TypePermutation{} -> make opImage func arg
1663 _ -> p
1664 Just (func, args) | arg <- catMaybes args, length arg == length args ->
1665 case typeOf func of
1666 Just TypeFunction{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1667 Just TypeSequence{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1668 Just TypePermutation{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1669 _ -> p
1670 _ -> p
1671
1672
1673
1674 maxOfDomain ::
1675 MonadFailDoc m =>
1676 Pretty r =>
1677 Domain r Expression -> m Expression
1678 maxOfDomain (DomainIntE _ x) = return $ make opMax x
1679 maxOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.maxOfDomain []"
1680 maxOfDomain (DomainInt _ [r]) = maxOfRange r
1681 maxOfDomain (DomainInt _ rs ) = do
1682 xs <- mapM maxOfRange rs
1683 return (make opMax (fromList xs))
1684 maxOfDomain (DomainReference _ (Just d)) = maxOfDomain d
1685 maxOfDomain d = failDoc ("rule_DomainMinMax.maxOfDomain" <+> pretty d)
1686
1687 maxOfRange :: MonadFailDoc m => Range Expression -> m Expression
1688 maxOfRange (RangeSingle x) = return x
1689 maxOfRange (RangeBounded _ x) = return x
1690 maxOfRange (RangeUpperBounded x) = return x
1691 maxOfRange r = failDoc ("rule_DomainMinMax.maxOfRange" <+> pretty (show r))
1692
1693 minOfDomain ::
1694 (?typeCheckerMode::TypeCheckerMode) =>
1695 MonadFailDoc m =>
1696 Pretty r =>
1697 Domain r Expression -> m Expression
1698 minOfDomain (DomainIntE _ x) = return $ make opMin x
1699 minOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.minOfDomain []"
1700 minOfDomain (DomainInt _ [r]) = minOfRange r
1701 minOfDomain (DomainInt _ rs ) = do
1702 xs <- mapM minOfRange rs
1703 return (make opMin (fromList xs))
1704 minOfDomain (DomainReference _ (Just d)) = minOfDomain d
1705 minOfDomain d = failDoc ("rule_DomainMinMax.minOfDomain" <+> pretty d)
1706
1707 minOfRange ::
1708 MonadFailDoc m =>
1709 Range Expression -> m Expression
1710 minOfRange (RangeSingle x) = return x
1711 minOfRange (RangeBounded x _) = return x
1712 minOfRange (RangeLowerBounded x) = return x
1713 minOfRange r = failDoc ("rule_DomainMinMax.minOfRange" <+> pretty (show r))