
  0 | ||| Like 'Pair' but type-aligned.  Called "Duo" because they are NOT
  1 | ||| two-of-a-kind ("pair", "double", "couple"), since the indexes may differ.
  2 | module TypeAligned.Duo
  3 | 
  4 | import Control.Relation
  5 | import Data.Linear.Notation
  6 | 
  7 | import LinearAnd
  8 | 
  9 | %default total
 10 | %prefix_record_projections off
 11 | 
 12 | ||| Two relationshpis / proofs that meet in the middle
 13 | public export
 14 | record Duo (p : Rel a) (x, z : a) where
 15 |   constructor MkDuo
 16 |   {0 y : a}
 17 |   1 fst : p x y
 18 |   1 snd : p y z
 19 | 
 20 | ||| Explicit prefix record projection
 21 | export
 22 | fst : (two : Duo p x z) -> p x two.y
 23 | fst = (.fst)
 24 | 
 25 | ||| Explicit prefix record projection
 26 | export
 27 | snd : (two : Duo p x z) -> p two.y z
 28 | snd = (.snd)
 29 | 
 30 | parameters {0 p : Rel a}
 31 |   ||| Linear 'eqMeet'
 32 |   export
 33 |   eqMeetOnce :
 34 |     ({0 x, y : a} -> p x y -@ p x y -@ Bool) ->
 35 |     (1 l, r : Duo p x z) -> (0 eqIndex : l.y = r.y) -> Bool
 36 |   eqMeetOnce eqP (MkDuo fstl sndl) (MkDuo fstr sndr) eqIndex =
 37 |     eqP fstl (rewrite eqIndex in fstr) -&& eqP sndl (rewrite eqIndex in sndr)
 38 | 
 39 |   ||| Something like "Eq", but I'm not sure it's useful.
 40 |   export
 41 |   eqMeet : ({0 x, y : a} -> p x y -> p x y -> Bool) -> (l, r : Duo p x z) -> (0 eqIndex : l.y = r.y) -> Bool
 42 |   eqMeet eqP l r eqIndex =
 43 |     eqP l.fst (rewrite eqIndex in r.fst) && eqP l.snd (rewrite eqIndex in r.snd)
 44 | 
 45 | ||| "(fst, snd)"
 46 | export
 47 | {0 p : Rel a} -> ({0 x, y : a} -> Show (p x y)) => Show (Duo p x y) where
 48 |   show two = "(" ++ show two.fst ++ ", " ++ show two.snd ++ ")"
 49 | 
 50 | parameters {0 p : Rel a}
 51 |   parameters {0 f : a -> b} {0 q : Rel b}
 52 |     parameters (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
 53 |       ||| Linear 'mapReduce'
 54 |       export
 55 |       mapReduceOnce : ({0 x, y, z : b} -> q x y -@ q y z -@ q x z) -> Duo p x y -@ q (f x) (f y)
 56 |       mapReduceOnce trans (MkDuo fst snd) = trans (pq fst) (pq snd)
 57 | 
 58 |       ||| Linear 'map'
 59 |       export
 60 |       mapOnce : Duo p x y -@ Duo q (f x) (f y)
 61 |       mapOnce (MkDuo fst snd) = MkDuo { fst = pq fst, snd = pq snd }
 62 | 
 63 |     parameters (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
 64 |       ||| Reduce while changing relation
 65 |       export
 66 |       mapReduce : ({0 x, y, z : b} -> q x y -> q y z -> q x z) -> Duo p x y -> q (f x) (f y)
 67 |       mapReduce trans two = trans (pq two.fst) (pq two.snd)
 68 | 
 69 |       ||| Change inner relation
 70 |       export
 71 |       map : Duo p x y -> Duo q (f x) (f y)
 72 |       map xy = MkDuo { fst = pq xy.fst, snd = pq xy.snd }
 73 | 
 74 |   ||| Linear 'reduce'
 75 |   export
 76 |   reduceOnce : ({0 x, y, z : a} -> p x y -@ p y z -@ p x z) -> Duo p x y -@ p x y
 77 |   reduceOnce trans (MkDuo fst snd) = trans fst snd
 78 | 
 79 |   ||| Reduce to inner relation
 80 |   export
 81 |   reduce : ({0 x, y, z : a} -> p x y -> p y z -> p x z) -> Duo p x y -> p x y
 82 |   reduce trans xy = trans xy.fst xy.snd
 83 |