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 f = match f
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 opToSetWithFlag
285 :: ( Op x :< x
286 , Pretty x
287 , MonadFailDoc m
288 )
289 => Proxy (m :: T.Type -> T.Type)
290 -> ( Bool -> x -> x
291 , x -> m (Bool, x)
292 )
293 opToSetWithFlag _ =
294 ( \ b x -> inject $ MkOpToSet $ OpToSet b x
295 , \ p -> do
296 op <- project p
297 case op of
298 MkOpToSet (OpToSet b x) -> return (b, x)
299 _ -> na ("Lenses.opToSet:" <++> pretty p)
300 )
301
302
303 opToMSet
304 :: ( Op x :< x
305 , Pretty x
306 , MonadFailDoc m
307 )
308 => Proxy (m :: T.Type -> T.Type)
309 -> ( x -> x
310 , x -> m x
311 )
312 opToMSet _ =
313 ( inject . MkOpToMSet . OpToMSet
314 , \ p -> do
315 op <- project p
316 case op of
317 MkOpToMSet (OpToMSet x) -> return x
318 _ -> na ("Lenses.opToMSet:" <++> pretty p)
319 )
320
321
322 opToRelation
323 :: ( Op x :< x
324 , Pretty x
325 , MonadFailDoc m
326 )
327 => Proxy (m :: T.Type -> T.Type)
328 -> ( x -> x
329 , x -> m x
330 )
331 opToRelation _ =
332 ( inject . MkOpToRelation . OpToRelation
333 , \ p -> do
334 op <- project p
335 case op of
336 MkOpToRelation (OpToRelation x) -> return x
337 _ -> na ("Lenses.opToRelation:" <++> pretty p)
338 )
339
340
341 opParts
342 :: ( Op x :< x
343 , Pretty x
344 , MonadFailDoc m
345 )
346 => Proxy (m :: T.Type -> T.Type)
347 -> ( x -> x
348 , x -> m x
349 )
350 opParts _ =
351 ( inject . MkOpParts . OpParts
352 , \ p -> do
353 op <- project p
354 case op of
355 MkOpParts (OpParts x) -> return x
356 _ -> na ("Lenses.opParts:" <++> pretty p)
357 )
358
359
360 opParty
361 :: ( Op x :< x
362 , Pretty x
363 , MonadFailDoc m
364 )
365 => Proxy (m :: T.Type -> T.Type)
366 -> ( x -> x -> x
367 , x -> m (x, x)
368 )
369 opParty _ =
370 ( \ x y -> inject $ MkOpParty $ OpParty x y
371 , \ p -> do
372 op <- project p
373 case op of
374 MkOpParty (OpParty x y) -> return (x,y)
375 _ -> na ("Lenses.opParty:" <++> pretty p)
376 )
377
378
379 opParticipants
380 :: ( Op x :< x
381 , Pretty x
382 , MonadFailDoc m
383 )
384 => Proxy (m :: T.Type -> T.Type)
385 -> ( x -> x
386 , x -> m x
387 )
388 opParticipants _ =
389 ( inject . MkOpParticipants . OpParticipants
390 , \ p -> do
391 op <- project p
392 case op of
393 MkOpParticipants (OpParticipants x) -> return x
394 _ -> na ("Lenses.opParticipants:" <++> pretty p)
395 )
396
397
398 opImage
399 :: ( Op x :< x
400 , Pretty x
401 , MonadFailDoc m
402 )
403 => Proxy (m :: T.Type -> T.Type)
404 -> ( x -> x -> x
405 , x -> m (x, x)
406 )
407 opImage _ =
408 ( \ x y -> inject $ MkOpImage $ OpImage x y
409 , \ p -> do
410 op <- project p
411 case op of
412 MkOpImage (OpImage x y) -> return (x,y)
413 _ -> na ("Lenses.opImage:" <++> pretty p)
414 )
415
416
417 opImageSet
418 :: ( Op x :< x
419 , Pretty x
420 , MonadFailDoc m
421 )
422 => Proxy (m :: T.Type -> T.Type)
423 -> ( x -> x -> x
424 , x -> m (x, x)
425 )
426 opImageSet _ =
427 ( \ x y -> inject $ MkOpImageSet $ OpImageSet x y
428 , \ p -> do
429 op <- project p
430 case op of
431 MkOpImageSet (OpImageSet x y) -> return (x,y)
432 _ -> na ("Lenses.opImageSet:" <++> pretty p)
433 )
434
435 opTransform
436 :: ( Op x :< x
437 , Pretty x
438 , MonadFailDoc m
439 )
440 => Proxy (m :: T.Type -> T.Type)
441 -> ( x -> x -> x
442 , x -> m (x, x)
443 )
444 opTransform _ =
445 ( \ x y -> inject $ MkOpTransform $ OpTransform x y
446 , \ p -> do
447 op <- project p
448 case op of
449 MkOpTransform (OpTransform x y) -> return (x,y)
450 _ -> na ("Lenses.opTransform:" <++> pretty p)
451 )
452
453
454 opRelationProj
455 :: ( Op x :< x
456 , Pretty x
457 , MonadFailDoc m
458 )
459 => Proxy (m :: T.Type -> T.Type)
460 -> ( x -> [Maybe x] -> x
461 , x -> m (x, [Maybe x])
462 )
463 opRelationProj _ =
464 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x ys
465 , \ p -> do
466 op <- project p
467 case op of
468 MkOpRelationProj (OpRelationProj x ys) -> return (x,ys)
469 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
470 )
471
472
473 opRelationImage
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 opRelationImage _ =
483 ( \ x ys -> inject $ MkOpRelationProj $ OpRelationProj x (map Just ys)
484 , \ p -> do
485 op <- project p
486 case op of
487 MkOpRelationProj (OpRelationProj x ys)
488 | let ys' = catMaybes ys
489 , length ys' == length ys -- they were all Just's
490 -> return (x,ys')
491 _ -> na ("Lenses.opRelationProj:" <++> pretty p)
492 )
493
494
495 opIndexing
496 :: ( Op x :< x
497 , Pretty x
498 , MonadFailDoc m
499 )
500 => Proxy (m :: T.Type -> T.Type)
501 -> ( x -> x -> x
502 , x -> m (x,x)
503 )
504 opIndexing _ =
505 ( \ x y -> inject (MkOpIndexing (OpIndexing x y))
506 , \ p -> do
507 op <- project p
508 case op of
509 MkOpIndexing (OpIndexing x y) -> return (x,y)
510 _ -> na ("Lenses.opIndexing:" <++> pretty p)
511 )
512
513
514 opMatrixIndexing
515 :: ( Op x :< x
516 , Pretty x
517 , TypeOf x
518 , MonadFailDoc m
519 , ?typeCheckerMode :: TypeCheckerMode
520 )
521 => Proxy (m :: T.Type -> T.Type)
522 -> ( x -> [x] -> x
523 , x -> m (x,[x])
524 )
525 opMatrixIndexing _ =
526 ( foldl (make opIndexing)
527 , \ p -> do
528 (m, is) <- go p
529 if null is
530 then na ("Lenses.opMatrixIndexing:" <+> pretty p)
531 else return (m, is)
532 )
533 where
534 go p = case project p of
535 Just (MkOpIndexing (OpIndexing x i)) -> do
536 ty <- typeOf x
537 case ty of
538 TypeMatrix{} -> return ()
539 TypeList{} -> return ()
540 _ -> na ("Lenses.opMatrixIndexing:" <+> pretty p)
541 (m,is) <- go x
542 return (m, is ++ [i])
543 _ -> return (p, [])
544
545
546 opMatrixIndexingSlicing
547 :: ( Op x :< x
548 , Pretty x
549 , MonadFailDoc m
550 , TypeOf x
551 , ?typeCheckerMode :: TypeCheckerMode
552 )
553 => Proxy (m :: T.Type -> T.Type)
554 -> ( x -> [Either x (Maybe x, Maybe x)] -> x
555 , x -> m (x, [Either x (Maybe x, Maybe x)]) -- either an index or a slice
556 )
557 opMatrixIndexingSlicing _ =
558 ( mk
559 , \ p -> do
560 (m, is, wasThereAnySlicing) <- go p
561 if not (null is) && wasThereAnySlicing
562 then return (m, is)
563 else na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
564 )
565 where
566 mk m [] = m
567 mk m (Left i:is) = mk (make opIndexing m i) is
568 mk m (Right (lb, ub):is) = mk (make opSlicing m lb ub) is
569
570 go p = case project p of
571 Just (MkOpIndexing (OpIndexing x i)) -> do
572 ty <- typeOf x
573 case ty of
574 TypeMatrix{} -> return ()
575 TypeList{} -> return ()
576 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
577 (m, is, wasThereAnySlicing) <- go x
578 return (m, is ++ [Left i], wasThereAnySlicing)
579 Just (MkOpSlicing (OpSlicing x lb ub)) -> do
580 ty <- typeOf x
581 case ty of
582 TypeMatrix{} -> return ()
583 TypeList{} -> return ()
584 _ -> na ("Lenses.opMatrixIndexingSlicing:" <+> pretty p)
585 (m, is, _) <- go x
586 return (m, is ++ [Right (lb, ub)], True)
587 _ -> return (p, [], False)
588
589
590 opSlicing
591 :: ( Op x :< x
592 , Pretty x
593 , MonadFailDoc m
594 )
595 => Proxy (m :: T.Type -> T.Type)
596 -> ( x -> Maybe x -> Maybe x -> x
597 , x -> m (x, Maybe x, Maybe x)
598 )
599 opSlicing _ =
600 ( \ x y z -> inject (MkOpSlicing (OpSlicing x y z))
601 , \ p -> do
602 op <- project p
603 case op of
604 MkOpSlicing (OpSlicing x y z) -> return (x,y,z)
605 _ -> na ("Lenses.opSlicing:" <++> pretty p)
606 )
607
608
609 opFlatten
610 :: ( Op x :< x
611 , Pretty x
612 , MonadFailDoc m
613 )
614 => Proxy (m :: T.Type -> T.Type)
615 -> ( x -> x
616 , x -> m x
617 )
618 opFlatten _ =
619 ( inject . MkOpFlatten . OpFlatten Nothing
620 , \ p -> do
621 op <- project p
622 case op of
623 MkOpFlatten (OpFlatten Nothing x) -> return x
624 _ -> na ("Lenses.opFlatten:" <++> pretty p)
625 )
626
627
628 flattenIfNeeded ::
629 Int ->
630 Expression ->
631 Expression
632 flattenIfNeeded dims m =
633 if dims > 1
634 then make opFlatten m
635 else m
636
637
638 oneDimensionaliser ::
639 Int -> -- current number of dimensions
640 Expression ->
641 Expression
642 oneDimensionaliser dims x =
643 case dims of
644 0 -> fromList [x]
645 1 -> x
646 _ -> make opFlatten x
647
648
649 opConcatenate
650 :: ( Op x :< x
651 , Pretty x
652 , MonadFailDoc m
653 )
654 => Proxy (m :: T.Type -> T.Type)
655 -> ( x -> x
656 , x -> m x
657 )
658 opConcatenate _ =
659 ( inject . MkOpFlatten . OpFlatten (Just 1)
660 , \ p -> do
661 op <- project p
662 case op of
663 MkOpFlatten (OpFlatten (Just 1) x) -> return x
664 _ -> na ("Lenses.opConcatenate:" <++> pretty p)
665 )
666
667
668 opIn
669 :: ( Op x :< x
670 , Pretty x
671 , MonadFailDoc m
672 )
673 => Proxy (m :: T.Type -> T.Type)
674 -> ( x -> x -> x
675 , x -> m (x,x)
676 )
677 opIn _ =
678 ( \ x y -> inject (MkOpIn (OpIn x y))
679 , \ p -> do
680 op <- project p
681 case op of
682 MkOpIn (OpIn x y) -> return (x,y)
683 _ -> na ("Lenses.opIn:" <++> pretty p)
684 )
685
686
687 opFreq
688 :: ( Op x :< x
689 , Pretty x
690 , MonadFailDoc m
691 )
692 => Proxy (m :: T.Type -> T.Type)
693 -> ( x -> x -> x
694 , x -> m (x,x)
695 )
696 opFreq _ =
697 ( \ x y -> inject (MkOpFreq (OpFreq x y))
698 , \ p -> do
699 op <- project p
700 case op of
701 MkOpFreq (OpFreq x y) -> return (x,y)
702 _ -> na ("Lenses.opFreq:" <++> pretty p)
703 )
704
705
706 opHist
707 :: ( Op x :< x
708 , Pretty x
709 , MonadFailDoc m
710 )
711 => Proxy (m :: T.Type -> T.Type)
712 -> ( x -> x
713 , x -> m x
714 )
715 opHist _ =
716 ( inject . MkOpHist . OpHist
717 , \ p -> do
718 op <- project p
719 case op of
720 MkOpHist (OpHist x) -> return x
721 _ -> na ("Lenses.opHist:" <++> pretty p)
722 )
723
724
725 opIntersect
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 opIntersect _ =
735 ( \ x y -> inject (MkOpIntersect (OpIntersect x y))
736 , \ p -> do
737 op <- project p
738 case op of
739 MkOpIntersect (OpIntersect x y) -> return (x,y)
740 _ -> na ("Lenses.opIntersect:" <++> pretty p)
741 )
742
743
744 opUnion
745 :: ( Op x :< x
746 , Pretty x
747 , MonadFailDoc m
748 )
749 => Proxy (m :: T.Type -> T.Type)
750 -> ( x -> x -> x
751 , x -> m (x,x)
752 )
753 opUnion _ =
754 ( \ x y -> inject (MkOpUnion (OpUnion x y))
755 , \ p -> do
756 op <- project p
757 case op of
758 MkOpUnion (OpUnion x y) -> return (x,y)
759 _ -> na ("Lenses.opUnion:" <++> pretty p)
760 )
761
762
763 opSubsetEq
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 opSubsetEq _ =
773 ( \ x y -> inject (MkOpSubsetEq (OpSubsetEq x y))
774 , \ p -> do
775 op <- project p
776 case op of
777 MkOpSubsetEq (OpSubsetEq x y) -> return (x,y)
778 _ -> na ("Lenses.opSubsetEq:" <++> pretty p)
779 )
780
781
782 opEq
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 opEq _ =
792 ( \ x y -> inject (MkOpEq (OpEq x y))
793 , \ p -> do
794 op <- project p
795 case op of
796 MkOpEq (OpEq x y) -> return (x,y)
797 _ -> na ("Lenses.opEq:" <++> pretty p)
798 )
799
800
801 opNeq
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 opNeq _ =
811 ( \ x y -> inject (MkOpNeq (OpNeq x y))
812 , \ p -> do
813 op <- project p
814 case op of
815 MkOpNeq (OpNeq x y) -> return (x,y)
816 _ -> na ("Lenses.opNeq:" <++> pretty p)
817 )
818
819
820 opLt
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 opLt _ =
830 ( \ x y -> inject (MkOpLt (OpLt x y))
831 , \ p -> do
832 op <- project p
833 case op of
834 MkOpLt (OpLt x y) -> return (x,y)
835 _ -> na ("Lenses.opLt:" <++> pretty p)
836 )
837
838
839 opLeq
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 opLeq _ =
849 ( \ x y -> inject (MkOpLeq (OpLeq x y))
850 , \ p -> do
851 op <- project p
852 case op of
853 MkOpLeq (OpLeq x y) -> return (x,y)
854 _ -> na ("Lenses.opLeq:" <++> pretty p)
855 )
856
857
858 opGt
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 opGt _ =
868 ( \ x y -> inject (MkOpGt (OpGt x y))
869 , \ p -> do
870 op <- project p
871 case op of
872 MkOpGt (OpGt x y) -> return (x,y)
873 _ -> na ("Lenses.opGt:" <++> pretty p)
874 )
875
876
877 opGeq
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 opGeq _ =
887 ( \ x y -> inject (MkOpGeq (OpGeq x y))
888 , \ p -> do
889 op <- project p
890 case op of
891 MkOpGeq (OpGeq x y) -> return (x,y)
892 _ -> na ("Lenses.opGeq:" <++> pretty p)
893 )
894
895
896 opDotLt
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 opDotLt _ =
906 ( \ x y -> inject (MkOpDotLt (OpDotLt x y))
907 , \ p -> do
908 op <- project p
909 case op of
910 MkOpDotLt (OpDotLt x y) -> return (x,y)
911 _ -> na ("Lenses.opDotLt:" <++> pretty p)
912 )
913
914
915 opDotLeq
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 opDotLeq _ =
925 ( \ x y -> inject (MkOpDotLeq (OpDotLeq x y))
926 , \ p -> do
927 op <- project p
928 case op of
929 MkOpDotLeq (OpDotLeq x y) -> return (x,y)
930 _ -> na ("Lenses.opDotLeq:" <++> pretty p)
931 )
932
933
934 opTildeLt
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 opTildeLt _ =
944 ( \ x y -> inject (MkOpTildeLt (OpTildeLt x y))
945 , \ p -> do
946 op <- project p
947 case op of
948 MkOpTildeLt (OpTildeLt x y) -> return (x,y)
949 _ -> na ("Lenses.opTildeLt:" <++> pretty p)
950 )
951
952
953 opTildeLeq
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 opTildeLeq _ =
963 ( \ x y -> inject (MkOpTildeLeq (OpTildeLeq x y))
964 , \ p -> do
965 op <- project p
966 case op of
967 MkOpTildeLeq (OpTildeLeq x y) -> return (x,y)
968 _ -> na ("Lenses.opTildeLeq:" <++> pretty p)
969 )
970
971
972 opOr
973 :: ( Op x :< x
974 , Pretty x
975 , MonadFailDoc m
976 )
977 => Proxy (m :: T.Type -> T.Type)
978 -> ( x -> x
979 , x -> m x
980 )
981 opOr _ =
982 ( inject . MkOpOr . OpOr
983 , \ p -> do
984 op <- project p
985 case op of
986 MkOpOr (OpOr xs) -> return xs
987 _ -> na ("Lenses.opOr:" <++> pretty p)
988 )
989
990
991 opAnd
992 :: ( Op x :< x
993 , Pretty x
994 , MonadFailDoc m
995 )
996 => Proxy (m :: T.Type -> T.Type)
997 -> ( x -> x
998 , x -> m x
999 )
1000 opAnd _ =
1001 ( inject . MkOpAnd . OpAnd
1002 , \ p -> do
1003 op <- project p
1004 case op of
1005 MkOpAnd (OpAnd xs) -> return xs
1006 _ -> na ("Lenses.opAnd:" <++> pretty p)
1007 )
1008
1009
1010 opMax
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 opMax _ =
1020 ( inject . MkOpMax . OpMax
1021 , \ p -> do
1022 op <- project p
1023 case op of
1024 MkOpMax (OpMax xs) -> return xs
1025 _ -> na ("Lenses.opMax:" <++> pretty p)
1026 )
1027
1028
1029 opMin
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 opMin _ =
1039 ( inject . MkOpMin . OpMin
1040 , \ p -> do
1041 op <- project p
1042 case op of
1043 MkOpMin (OpMin xs) -> return xs
1044 _ -> na ("Lenses.opMin:" <++> pretty p)
1045 )
1046
1047
1048 opImply
1049 :: ( Op x :< x
1050 , Pretty x
1051 , MonadFailDoc m
1052 )
1053 => Proxy (m :: T.Type -> T.Type)
1054 -> ( x -> x -> x
1055 , x -> m (x,x)
1056 )
1057 opImply _ =
1058 ( \ x y -> inject (MkOpImply (OpImply x y))
1059 , \ p -> do
1060 op <- project p
1061 case op of
1062 MkOpImply (OpImply x y) -> return (x,y)
1063 _ -> na ("Lenses.opImply:" <++> pretty p)
1064 )
1065
1066
1067 opNot
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 opNot _ =
1077 ( inject . MkOpNot . OpNot
1078 , \ p -> do
1079 op <- project p
1080 case op of
1081 MkOpNot (OpNot x) -> return x
1082 _ -> na ("Lenses.opNot:" <++> pretty p)
1083 )
1084
1085
1086 opProduct
1087 :: ( Op x :< x
1088 , Pretty x
1089 , MonadFailDoc m
1090 )
1091 => Proxy (m :: T.Type -> T.Type)
1092 -> ( x -> x
1093 , x -> m x
1094 )
1095 opProduct _ =
1096 ( inject . MkOpProduct . OpProduct
1097 , \ p -> do
1098 op <- project p
1099 case op of
1100 MkOpProduct (OpProduct x) -> return x
1101 _ -> na ("Lenses.opProduct:" <++> pretty p)
1102 )
1103
1104
1105 opSum
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 opSum _ =
1115 ( inject . MkOpSum . OpSum
1116 , \ p -> do
1117 op <- project p
1118 case op of
1119 MkOpSum (OpSum x) -> return x
1120 _ -> na ("Lenses.opSum:" <++> pretty p)
1121 )
1122
1123
1124 data ReducerType = RepetitionIsNotSignificant | RepetitionIsSignificant
1125 deriving (Eq, Ord, Show)
1126
1127 opReducer
1128 :: ( Op x :< x
1129 , Pretty x
1130 , MonadFailDoc m
1131 )
1132 => Proxy (m :: T.Type -> T.Type)
1133 -> ( (x -> x, x) -> x
1134 , x -> m ( ReducerType
1135 , Bool -- defined on []
1136 , x -> x
1137 , x
1138 )
1139 )
1140 opReducer _ =
1141 ( \ (mk, x) -> mk x
1142 , \ p -> do
1143 op <- project p
1144 let is = RepetitionIsSignificant
1145 let isn't = RepetitionIsNotSignificant
1146 case op of
1147 MkOpAnd (OpAnd x) -> return (isn't, True , inject . MkOpAnd . OpAnd , x)
1148 MkOpOr (OpOr x) -> return (isn't, True , inject . MkOpOr . OpOr , x)
1149 MkOpXor (OpXor x) -> return (is , False, inject . MkOpXor . OpXor , x)
1150 MkOpSum (OpSum x) -> return (is , True , inject . MkOpSum . OpSum , x)
1151 MkOpProduct (OpProduct x) -> return (is , True , inject . MkOpProduct . OpProduct , x)
1152 MkOpMax (OpMax x) -> return (isn't, False, inject . MkOpMax . OpMax , x)
1153 MkOpMin (OpMin x) -> return (isn't, False, inject . MkOpMin . OpMin , x)
1154 _ -> na ("Lenses.opReducer:" <++> pretty p)
1155 )
1156
1157
1158 opModifier
1159 :: ( Op x :< x
1160 , MonadFailDoc m
1161 )
1162 => Proxy (m :: T.Type -> T.Type)
1163 -> ( (x -> x, x) -> x
1164 , x -> m (x -> x, x)
1165 )
1166 opModifier _ =
1167 ( \ (mk, x) -> mk x
1168 , \ p -> case project p of
1169 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1170 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1171 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1172 Just (MkOpParts (OpParts x)) -> return (inject . MkOpParts . OpParts , x)
1173 _ -> return (id , p)
1174 )
1175
1176
1177 opModifierNoP
1178 :: ( Op x :< x
1179 , MonadFailDoc m
1180 )
1181 => Proxy (m :: T.Type -> T.Type)
1182 -> ( (x -> x, x) -> x
1183 , x -> m (x -> x, x)
1184 )
1185 opModifierNoP _ =
1186 ( \ (mk, x) -> mk x
1187 , \ p -> case project p of
1188 Just (MkOpToSet (OpToSet _ x)) -> return (inject . MkOpToSet . OpToSet False , x)
1189 Just (MkOpToMSet (OpToMSet x)) -> return (inject . MkOpToMSet . OpToMSet , x)
1190 Just (MkOpToRelation (OpToRelation x)) -> return (inject . MkOpToRelation . OpToRelation , x)
1191 _ -> return (id , p)
1192 )
1193
1194
1195 opAllDiff
1196 :: ( Op x :< x
1197 , Pretty x
1198 , MonadFailDoc m
1199 )
1200 => Proxy (m :: T.Type -> T.Type)
1201 -> ( x -> x
1202 , x -> m x
1203 )
1204 opAllDiff _ =
1205 ( inject . MkOpAllDiff . OpAllDiff
1206 , \ p -> do
1207 op <- project p
1208 case op of
1209 MkOpAllDiff (OpAllDiff x) -> return x
1210 _ -> na ("Lenses.opAllDiff:" <++> pretty p)
1211 )
1212
1213
1214 opAllDiffExcept
1215 :: ( Op x :< x
1216 , Pretty x
1217 , MonadFailDoc m
1218 )
1219 => Proxy (m :: T.Type -> T.Type)
1220 -> ( x -> x -> x
1221 , x -> m (x, x)
1222 )
1223 opAllDiffExcept _ =
1224 ( \ x y -> inject $ MkOpAllDiffExcept $ OpAllDiffExcept x y
1225 , \ p -> do
1226 op <- project p
1227 case op of
1228 MkOpAllDiffExcept (OpAllDiffExcept x y) -> return (x, y)
1229 _ -> na ("Lenses.opAllDiffExcept:" <++> pretty p)
1230 )
1231
1232
1233 constantInt
1234 :: MonadFailDoc m
1235 => Proxy (m :: T.Type -> T.Type)
1236 -> ( Integer -> Expression
1237 , Expression -> m Integer
1238 )
1239 constantInt _ =
1240 ( Constant . ConstantInt TagInt
1241 , \ p -> case p of
1242 (Constant (ConstantInt TagInt i)) -> return i
1243 _ -> na ("Lenses.constantInt:" <++> pretty p)
1244 )
1245
1246
1247 matrixLiteral
1248 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1249 => Proxy (m :: T.Type -> T.Type)
1250 -> ( Type -> Domain () Expression -> [Expression] -> Expression
1251 , Expression -> m (Type, Domain () Expression, [Expression])
1252 )
1253 matrixLiteral _ =
1254 ( \ ty index elems ->
1255 if null elems
1256 then Typed (AbstractLiteral (AbsLitMatrix index elems)) ty
1257 else AbstractLiteral (AbsLitMatrix index elems)
1258 , \ p -> do
1259 ty <- typeOf p
1260 (index, xs) <- followAliases extract p
1261 return (ty, index, xs)
1262 )
1263 where
1264 extract (Constant (ConstantAbstract (AbsLitMatrix index xs))) = return (fmap Constant index, map Constant xs)
1265 extract (AbstractLiteral (AbsLitMatrix index xs)) = return (index, xs)
1266 extract (Typed x _) = extract x
1267 extract (Constant (TypedConstant x _)) = extract (Constant x)
1268 extract p = na ("Lenses.matrixLiteral:" <+> pretty p)
1269
1270
1271 onMatrixLiteral
1272 :: (Functor m, Applicative m, Monad m, NameGen m)
1273 => Maybe Int -- how many levels to go down. all the way if Nothing.
1274 -> (Expression -> m Expression)
1275 -> Expression -> m Expression
1276 onMatrixLiteral mlvl f = case mlvl of
1277 Nothing -> followAliases go
1278 Just lvl -> followAliases (goL lvl)
1279 where
1280 go (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1281 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (go . Constant) xs
1282 go (AbstractLiteral (AbsLitMatrix index xs)) =
1283 AbstractLiteral . AbsLitMatrix index <$> mapM go xs
1284 go (Typed x _) = go x
1285 go (Constant (TypedConstant x _)) = go (Constant x)
1286 go p = f p
1287
1288 goL 0 p = f p
1289 goL lvl (Constant (ConstantAbstract (AbsLitMatrix index xs))) =
1290 AbstractLiteral . AbsLitMatrix (fmap Constant index) <$> mapM (goL (lvl-1) . Constant) xs
1291 goL lvl (AbstractLiteral (AbsLitMatrix index xs)) =
1292 AbstractLiteral . AbsLitMatrix index <$> mapM (goL (lvl-1)) xs
1293 goL lvl (Typed x _) = goL lvl x
1294 goL lvl (Constant (TypedConstant x _)) = goL lvl (Constant x)
1295 goL lvl p = do
1296 (iPat, i) <- quantifiedVar
1297 body <- goL (lvl-1) i
1298 return $ Comprehension body [Generator (GenInExpr iPat p)]
1299
1300
1301 setLiteral
1302 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1303 => Proxy (m :: T.Type -> T.Type)
1304 -> ( Type -> [Expression] -> Expression
1305 , Expression -> m (Type, [Expression])
1306 )
1307 setLiteral _ =
1308 ( \ ty elems ->
1309 if null elems
1310 then Typed (AbstractLiteral (AbsLitSet elems)) ty
1311 else AbstractLiteral (AbsLitSet elems)
1312 , \ p -> do
1313 ty <- typeOf p
1314 xs <- followAliases extract p
1315 return (ty, xs)
1316 )
1317 where
1318 extract (Constant (viewConstantSet -> Just xs)) = return (map Constant xs)
1319 extract (AbstractLiteral (AbsLitSet xs)) = return xs
1320 extract (Typed x _) = extract x
1321 extract (Constant (TypedConstant x _)) = extract (Constant x)
1322 extract p = na ("Lenses.setLiteral:" <+> pretty p)
1323
1324
1325 msetLiteral
1326 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1327 => Proxy (m :: T.Type -> T.Type)
1328 -> ( Type -> [Expression] -> Expression
1329 , Expression -> m (Type, [Expression])
1330 )
1331 msetLiteral _ =
1332 ( \ ty elems ->
1333 if null elems
1334 then Typed (AbstractLiteral (AbsLitMSet elems)) ty
1335 else AbstractLiteral (AbsLitMSet elems)
1336 , \ p -> do
1337 ty <- typeOf p
1338 xs <- followAliases extract p
1339 return (ty, xs)
1340 )
1341 where
1342 extract (Constant (viewConstantMSet -> Just xs)) = return (map Constant xs)
1343 extract (AbstractLiteral (AbsLitMSet xs)) = return xs
1344 extract (Typed x _) = extract x
1345 extract (Constant (TypedConstant x _)) = extract (Constant x)
1346 extract p = na ("Lenses.msetLiteral:" <+> pretty p)
1347
1348
1349 functionLiteral
1350 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1351 => Proxy (m :: T.Type -> T.Type)
1352 -> ( Type -> [(Expression,Expression)] -> Expression
1353 , Expression -> m (Type, [(Expression,Expression)])
1354 )
1355 functionLiteral _ =
1356 ( \ ty elems ->
1357 if null elems
1358 then Typed (AbstractLiteral (AbsLitFunction elems)) ty
1359 else AbstractLiteral (AbsLitFunction elems)
1360 , \ p -> do
1361 ty <- typeOf p
1362 xs <- followAliases extract p
1363 return (ty, xs)
1364 )
1365 where
1366 extract (Constant (viewConstantFunction -> Just xs)) = return [ (Constant a, Constant b) | (a,b) <- xs ]
1367 extract (AbstractLiteral (AbsLitFunction xs)) = return xs
1368 extract (Typed x _) = extract x
1369 extract (Constant (TypedConstant x _)) = extract (Constant x)
1370 extract p = na ("Lenses.functionLiteral:" <+> pretty p)
1371
1372
1373 sequenceLiteral
1374 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1375 => Proxy (m :: T.Type -> T.Type)
1376 -> ( Type -> [Expression] -> Expression
1377 , Expression -> m (Type, [Expression])
1378 )
1379 sequenceLiteral _ =
1380 ( \ ty elems ->
1381 if null elems
1382 then Typed (AbstractLiteral (AbsLitSequence elems)) ty
1383 else AbstractLiteral (AbsLitSequence elems)
1384 , \ p -> do
1385 ty <- typeOf p
1386 xs <- followAliases extract p
1387 return (ty, xs)
1388 )
1389 where
1390 extract (Constant (viewConstantSequence -> Just xs)) = return (map Constant xs)
1391 extract (AbstractLiteral (AbsLitSequence xs)) = return xs
1392 extract (Typed x _) = extract x
1393 extract (Constant (TypedConstant x _)) = extract (Constant x)
1394 extract p = na ("Lenses.sequenceLiteral:" <+> pretty p)
1395
1396
1397 relationLiteral
1398 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1399 => Proxy (m :: T.Type -> T.Type)
1400 -> ( Type -> [[Expression]] -> Expression
1401 , Expression -> m (Type, [[Expression]])
1402 )
1403 relationLiteral _ =
1404 ( \ ty elems ->
1405 if null elems
1406 then Typed (AbstractLiteral (AbsLitRelation elems)) ty
1407 else AbstractLiteral (AbsLitRelation elems)
1408 , \ p -> do
1409 ty <- typeOf p
1410 xs <- followAliases extract p
1411 return (ty, xs)
1412 )
1413 where
1414 extract (Constant (viewConstantRelation -> Just xs)) = return (map (map Constant) xs)
1415 extract (AbstractLiteral (AbsLitRelation xs)) = return xs
1416 extract (Typed x _) = extract x
1417 extract (Constant (TypedConstant x _)) = extract (Constant x)
1418 extract p = na ("Lenses.relationLiteral:" <+> pretty p)
1419
1420
1421 partitionLiteral
1422 :: (MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode)
1423 => Proxy (m :: T.Type -> T.Type)
1424 -> ( Type -> [[Expression]] -> Expression
1425 , Expression -> m (Type, [[Expression]])
1426 )
1427 partitionLiteral _ =
1428 ( \ ty elems ->
1429 if null elems
1430 then Typed (AbstractLiteral (AbsLitPartition elems)) ty
1431 else AbstractLiteral (AbsLitPartition elems)
1432 , \ p -> do
1433 ty <- typeOf p
1434 xs <- followAliases extract p
1435 return (ty, xs)
1436 )
1437 where
1438 extract (Constant (viewConstantPartition -> Just xs)) = return (map (map Constant) xs)
1439 extract (AbstractLiteral (AbsLitPartition xs)) = return xs
1440 extract (Typed x _) = extract x
1441 extract (Constant (TypedConstant x _)) = extract (Constant x)
1442 extract p = na ("Lenses.partitionLiteral:" <+> pretty p)
1443
1444
1445 opTwoBars
1446 :: ( Op x :< x
1447 , Pretty x
1448 , MonadFailDoc m
1449 )
1450 => Proxy (m :: T.Type -> T.Type)
1451 -> ( x -> x
1452 , x -> m x
1453 )
1454 opTwoBars _ =
1455 ( inject . MkOpTwoBars . OpTwoBars
1456 , \ p -> do
1457 op <- project p
1458 case op of
1459 MkOpTwoBars (OpTwoBars x) -> return x
1460 _ -> na ("Lenses.opTwoBars:" <++> pretty p)
1461 )
1462
1463
1464 opPreImage
1465 :: ( Op x :< x
1466 , Pretty x
1467 , MonadFailDoc m
1468 )
1469 => Proxy (m :: T.Type -> T.Type)
1470 -> ( x -> x -> x
1471 , x -> m (x,x)
1472 )
1473 opPreImage _ =
1474 ( \ x y -> inject (MkOpPreImage (OpPreImage x y))
1475 , \ p -> do
1476 op <- project p
1477 case op of
1478 MkOpPreImage (OpPreImage x y) -> return (x,y)
1479 _ -> na ("Lenses.opPreImage:" <++> pretty p)
1480 )
1481
1482
1483 opActive
1484 :: ( Op x :< x
1485 , Pretty x
1486 , MonadFailDoc m
1487 )
1488 => Proxy (m :: T.Type -> T.Type)
1489 -> ( x -> Name -> x
1490 , x -> m (x,Name)
1491 )
1492 opActive _ =
1493 ( \ x y -> inject (MkOpActive (OpActive x y))
1494 , \ p -> do
1495 op <- project p
1496 case op of
1497 MkOpActive (OpActive x y) -> return (x,y)
1498 _ -> na ("Lenses.opActive:" <++> pretty p)
1499 )
1500
1501
1502 opFactorial
1503 :: ( Op x :< x
1504 , Pretty x
1505 , MonadFailDoc m
1506 )
1507 => Proxy (m :: T.Type -> T.Type)
1508 -> ( x -> x
1509 , x -> m x
1510 )
1511 opFactorial _ =
1512 ( inject . MkOpFactorial . OpFactorial
1513 , \ p -> do
1514 op <- project p
1515 case op of
1516 MkOpFactorial (OpFactorial x) -> return x
1517 _ -> na ("Lenses.opFactorial:" <++> pretty p)
1518 )
1519
1520
1521 opLex
1522 :: ( Op x :< x
1523 , Pretty x
1524 , MonadFailDoc m
1525 )
1526 => Proxy (m :: T.Type -> T.Type)
1527 -> ( (x -> x -> x, (x,x)) -> x
1528 , x -> m (x -> x -> x, (x,x))
1529 )
1530 opLex _ =
1531 ( \ (mk, (x,y)) -> mk x y
1532 , \ p -> case project p of
1533 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1534 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1535 _ -> na ("Lenses.opLex:" <++> pretty p)
1536 )
1537
1538
1539 opOrdering
1540 :: ( Op x :< x
1541 , Pretty x
1542 , MonadFailDoc m
1543 )
1544 => Proxy (m :: T.Type -> T.Type)
1545 -> ( (x -> x -> x, (x,x)) -> x
1546 , x -> m (x -> x -> x, (x,x))
1547 )
1548 opOrdering _ =
1549 ( \ (mk, (x,y)) -> mk x y
1550 , \ p -> case project p of
1551 Just (MkOpLt (OpLt x y)) -> return (\ x' y' -> inject (MkOpLt (OpLt x' y')), (x,y) )
1552 Just (MkOpLeq (OpLeq x y)) -> return (\ x' y' -> inject (MkOpLeq (OpLeq x' y')), (x,y) )
1553 Just (MkOpTildeLt (OpTildeLt x y)) -> return (\ x' y' -> inject (MkOpTildeLt (OpTildeLt x' y')), (x,y) )
1554 Just (MkOpTildeLeq (OpTildeLeq x y)) -> return (\ x' y' -> inject (MkOpTildeLeq (OpTildeLeq x' y')), (x,y) )
1555 Just (MkOpLexLt (OpLexLt x y)) -> return (\ x' y' -> inject (MkOpLexLt (OpLexLt x' y')), (x,y) )
1556 Just (MkOpLexLeq (OpLexLeq x y)) -> return (\ x' y' -> inject (MkOpLexLeq (OpLexLeq x' y')), (x,y) )
1557 _ -> na ("Lenses.opOrdering:" <++> pretty p)
1558 )
1559
1560
1561 fixTHParsing :: Data a => a -> a
1562 fixTHParsing p =
1563 let ?typeCheckerMode = RelaxedIntegerTags
1564 in fixRelationProj p
1565
1566
1567 fixRelationProj :: (Data a, ?typeCheckerMode :: TypeCheckerMode) => a -> a
1568 fixRelationProj= transformBi f
1569 where
1570 f :: Expression -> Expression
1571 f p =
1572 case match opRelationProj p of
1573 Just (func, [Just arg]) ->
1574 case typeOf func of
1575 Just TypeFunction{} -> make opImage func arg
1576 Just TypeSequence{} -> make opImage func arg
1577 _ -> p
1578 Just (func, args) | arg <- catMaybes args, length arg == length args ->
1579 case typeOf func of
1580 Just TypeFunction{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1581 Just TypeSequence{} -> make opImage func $ AbstractLiteral $ AbsLitTuple arg
1582 _ -> p
1583 _ -> p
1584
1585
1586
1587 maxOfDomain :: (MonadFailDoc m, Pretty r) => Domain r Expression -> m Expression
1588 maxOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.maxOfDomain []"
1589 maxOfDomain (DomainInt _ [r]) = maxOfRange r
1590 maxOfDomain (DomainInt _ rs ) = do
1591 xs <- mapM maxOfRange rs
1592 return (make opMax (fromList xs))
1593 maxOfDomain (DomainReference _ (Just d)) = maxOfDomain d
1594 maxOfDomain d = failDoc ("rule_DomainMinMax.maxOfDomain" <+> pretty d)
1595
1596 maxOfRange :: MonadFailDoc m => Range Expression -> m Expression
1597 maxOfRange (RangeSingle x) = return x
1598 maxOfRange (RangeBounded _ x) = return x
1599 maxOfRange (RangeUpperBounded x) = return x
1600 maxOfRange r = failDoc ("rule_DomainMinMax.maxOfRange" <+> pretty (show r))
1601
1602 minOfDomain :: (MonadFailDoc m, Pretty r) => Domain r Expression -> m Expression
1603 minOfDomain (DomainInt _ [] ) = failDoc "rule_DomainMinMax.minOfDomain []"
1604 minOfDomain (DomainInt _ [r]) = minOfRange r
1605 minOfDomain (DomainInt _ rs ) = do
1606 xs <- mapM minOfRange rs
1607 return (make opMin (fromList xs))
1608 minOfDomain (DomainReference _ (Just d)) = minOfDomain d
1609 minOfDomain d = failDoc ("rule_DomainMinMax.minOfDomain" <+> pretty d)
1610
1611 minOfRange :: MonadFailDoc m => Range Expression -> m Expression
1612 minOfRange (RangeSingle x) = return x
1613 minOfRange (RangeBounded x _) = return x
1614 minOfRange (RangeLowerBounded x) = return x
1615 minOfRange r = failDoc ("rule_DomainMinMax.minOfRange" <+> pretty (show r))