0 | ||| Type primarily for internal usage holding either two or three relationships.
  1 | ||| Used internally to provide fast append, even for when the meeting point is "ragged".
  2 | module TypeAligned.TwoThree
  3 |
  4 | import Control.Relation
  5 | import Data.Linear.Notation
  6 |
  7 | import TypeAligned.Sum
  8 | import public TypeAligned.Duo
  9 | import public TypeAligned.Trio
 10 |
 11 | %default total
 12 |
 13 | ||| Utility type for 2-3 tree/list nesting
 14 | public export
 15 | 0 TwoThree : Rel a -> Rel a
 16 | TwoThree p = Sum (Duo p) (Trio p)
 17 |
 18 | parameters {0 p : Rel a}
 19 |   ||| Convenience constructor
 20 |   export
 21 |   twice : p x y -@ p y z -@ TwoThree p x z
 22 |   twice xy yz = Left (MkDuo { fst = xy, snd = yz })
 23 |
 24 |   ||| Convenience constructor, unrestricted
 25 |   export
 26 |   two : p x y -> p y z -> TwoThree p x z
 27 |   two xy yz = twice xy yz
 28 |
 29 |   ||| Convenience constructor
 30 |   export
 31 |   thrice : p w x -@ p x y -@ p y z -@ TwoThree p w z
 32 |   thrice wx xy yz = Right (MkTrio { fst3 = wx, snd3 = xy, thrd = yz})
 33 |
 34 |   ||| Convenience constructor, unrestricted
 35 |   export
 36 |   three : p w x -> p x y -> p y z -> TwoThree p w z
 37 |   three wx xy yz = thrice wx xy yz
 38 |
 39 |   ||| Synthetic accessor; first (or only) meeting index
 40 |   export
 41 |   0 (.x) : TwoThree p w z -> a
 42 |   (.x) (Left two) = two.y
 43 |   (.x) (Right three) = three.x
 44 |
 45 |   ||| Synthetic accessor; last (or only) meeting index
 46 |   export
 47 |   0 (.y) : TwoThree p w z -> a
 48 |   (.y) (Left two) = two.y
 49 |   (.y) (Right three) = three.y
 50 |
 51 | ||| Synthetic accessor
 52 | export
 53 | head, (.head) : (tt : TwoThree p w z) -> p w tt.x
 54 | head (Left two) = fst two
 55 | head (Right three) = fst3 three
 56 | (.head) = head
 57 |
 58 | ||| Drop first relationship
 59 | export
 60 | tail : (tt : TwoThree p w z) -> Sum p (Duo p) tt.x z
 61 | tail (Left two) = Left two.snd
 62 | tail (Right three) = Right (tail three)
 63 |
 64 | ||| Synthetic accessor
 65 | export
 66 | last, (.last) : (tt : TwoThree p w z) -> p tt.y z
 67 | last (Left two) = snd two
 68 | last (Right three) = thrd three
 69 | (.last) = last
 70 |
 71 | ||| Drop last relationship
 72 | export
 73 | init : (tt : TwoThree p w z) -> Sum p (Duo p) w tt.y
 74 | init (Left two) = Left two.fst
 75 | init (Right three) = Right (init three)
 76 |
 77 | parameters {0 p : Rel a}
 78 |   parameters {0 f : a -> b} {0 q : Rel b}
 79 |     parameters (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
 80 |       ||| Reduce while changing inner relation
 81 |       export
 82 |       mapReduceOnce : ({0 x, y, z : b} -> q x y -@ q y z -@ q x z) -> TwoThree p x y -@ q (f x) (f y)
 83 |       mapReduceOnce trans (Left two) = mapReduceOnce {q} pq trans two
 84 |       mapReduceOnce trans (Right three) = mapReduceOnce {q} pq trans three
 85 |
 86 |       ||| Linear 'map'
 87 |       export
 88 |       mapOnce : TwoThree p x y -@ TwoThree q (f x) (f y)
 89 |       mapOnce = bimapOnce {f} (mapOnce pq) (mapOnce pq)
 90 |
 91 |     parameters (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
 92 |       ||| Reduce while changing inner relation
 93 |       export
 94 |       mapReduce : ({0 x, y, z : b} -> q x y -> q y z -> q x z) -> TwoThree p x y -> q (f x) (f y)
 95 |       mapReduce trans (Left two) = mapReduce {q} pq trans two
 96 |       mapReduce trans (Right three) = mapReduce {q} pq trans three
 97 |
 98 |       ||| Change inner relation
 99 |       export
100 |       map : TwoThree p x y -> TwoThree q (f x) (f y)
101 |       map = bimap {f} (map pq) (map pq)
102 |
103 |   ||| Linear 'reduce'
104 |   export
105 |   reduceOnce : ({0 x, y, z : a} -> p x y -@ p y z -@ p x z) -> TwoThree p x y -@ p x y
106 |   reduceOnce trans (Left two) = reduceOnce trans two
107 |   reduceOnce trans (Right three) = reduceOnce trans three
108 |
109 |   ||| Reduce to inner relation
110 |   export
111 |   reduce : ({0 x, y, z : a} -> p x y -> p y z -> p x z) -> TwoThree p x y -> p x y
112 |   reduce trans (Left two) = reduce trans two
113 |   reduce trans (Right three) = reduce trans three
114 |