0 | ||| Trio because they are NOT three-of-a-kind ("triple", "triad") since the indexes may differ.
  1 | module TypeAligned.Trio
  2 |
  3 | import Control.Relation
  4 | import Data.Linear.Notation
  5 |
  6 | import TypeAligned.Duo
  7 | import LinearAnd
  8 |
  9 | %default total
 10 | %prefix_record_projections off
 11 |
 12 | ||| Three relationships / proofs that link up
 13 | public export
 14 | record Trio (p : Rel a) (w, z : a) where
 15 |   constructor MkTrio
 16 |   {0 x, y : a}
 17 |   1 fst3 : p w x
 18 |   1 snd3 : p x y
 19 |   1 thrd : p y z
 20 |
 21 | ||| Explicit prefix record projection
 22 | export
 23 | fst3, head : (three : Trio p w z) -> p w three.x
 24 | fst3 = (.fst3)
 25 | head = fst3
 26 |
 27 | ||| Explicit prefix record projection
 28 | export
 29 | snd3 : (three : Trio p w z) -> p three.x three.y
 30 | snd3 = (.snd3)
 31 |
 32 | ||| Explicit prefix record projection
 33 | export
 34 | thrd, last : (three : Trio p w z) -> p three.y z
 35 | thrd = (.thrd)
 36 | last = thrd
 37 |
 38 | ||| Drop first relationship
 39 | export
 40 | tail : (three : Trio p w z) -> Duo p three.x z
 41 | tail three = MkDuo { fst = three.snd3, snd = three.thrd }
 42 |
 43 | ||| Drop last relationship
 44 | export
 45 | init : (three : Trio p w z) -> Duo p w three.y
 46 | init three = MkDuo { fst = three.fst3, snd = three.snd3 }
 47 |
 48 | parameters {0 p : a -> a -> Type}
 49 |   ||| Linear 'eqMeet'
 50 |   export
 51 |   eqMeetOnce :
 52 |     ({0 x, y : a} -> p x y -@ p x y -@ Bool) ->
 53 |     (1 l, r : Trio p w z) -> (0 eqX : l.x = r.x) -> (0 eqY : l.y = r.y) -> Bool
 54 |   eqMeetOnce eqP (MkTrio fstl sndl thrl) (MkTrio fstr sndr thrr) eqX eqY =
 55 |     eqP fstl (rewrite eqX in fstr) -&& eqP sndl (rewrite eqX in rewrite eqY in sndr) -&& eqP thrl (rewrite eqY in thrr)
 56 |
 57 |   ||| Something like "Eq", but I'm not sure it's useful
 58 |   export
 59 |   eqMeet :
 60 |     ({0 x, y : a} -> p x y -> p x y -> Bool) -> (l, r : Trio p w z) -> (0 eqX : l.x = r.x) -> (0 eqY : l.y = r.y) -> Bool
 61 |   eqMeet eqP l r eqX eqY =
 62 |     eqP l.fst3 (rewrite eqX in r.fst3)
 63 |       && eqP l.snd3 (rewrite eqX in rewrite eqY in r.snd3)
 64 |       && eqP l.thrd (rewrite eqY in r.thrd)
 65 |
 66 | ||| "(fst3, snd3, thrd)"
 67 | export
 68 | {0 p : Rel a} -> ({0 x, y : a} -> Show (p x y)) => Show (Trio p x y) where
 69 |   show three = "(" ++ show three.fst3 ++ ", " ++ show three.snd3 ++ ", " ++ show three.thrd ++ ")"
 70 |
 71 | parameters {0 p : Rel a}
 72 |   parameters {0 f : a -> b} {0 q : Rel b}
 73 |     parameters (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
 74 |       ||| Linear 'mapReduce'
 75 |       export
 76 |       mapReduceOnce : ({0 x, y, z : b} -> q x y -@ q y z -@ q x z) -> Trio p x y -@ q (f x) (f y)
 77 |       mapReduceOnce trans (MkTrio fst3 snd3 thrd) = trans (trans (pq fst3) (pq snd3)) (pq thrd)
 78 |
 79 |       ||| Linear 'map'
 80 |       export
 81 |       mapOnce : Trio p x y -@ Trio q (f x) (f y)
 82 |       mapOnce (MkTrio fst3 snd3 thrd) = MkTrio { fst3 = pq fst3, snd3 = pq snd3, thrd = pq thrd }
 83 |
 84 |     parameters (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
 85 |       ||| Reduce while changing inner relation
 86 |       export
 87 |       mapReduce : ({0 x, y, z : b} -> q x y -> q y z -> q x z) -> Trio p x y -> q (f x) (f y)
 88 |       mapReduce trans xy = trans (trans (pq xy.fst3) (pq xy.snd3)) (pq xy.thrd)
 89 |
 90 |       ||| Change inner relation
 91 |       export
 92 |       map : Trio p x y -> Trio q (f x) (f y)
 93 |       map xy = MkTrio { fst3 = pq xy.fst3, snd3 = pq xy.snd3, thrd = pq xy.thrd }
 94 |
 95 |   ||| Linear 'reduce'
 96 |   export
 97 |   reduceOnce : ({0 x, y, z : a} -> p x y -@ p y z -@ p x z) -> Trio p x y -@ p x y
 98 |   reduceOnce trans (MkTrio fst3 snd3 thrd) = trans (trans fst3 snd3) thrd
 99 |
100 |   ||| Reduce to inner relation
101 |   export
102 |   reduce : ({0 x, y, z : a} -> p x y -> p y z -> p x z) -> Trio p x y -> p x y
103 |   reduce trans xy = trans (trans xy.fst3 xy.snd3) xy.thrd
104 |