
   0 | ||| Type-aligned sequences.  Transitive closures of (binary) relations that also provide fast reflection / destruction.
   1 | module TypeAligned
   2 | 
   3 | import Control.Relation
   4 | import Data.Linear.Bifunctor
   5 | import Data.Linear.LEither
   6 | import public Data.Linear.Notation -- Q: Avoid public import?
   7 | 
   8 | import TypeAligned.Sum
   9 | import public TypeAligned.ZeroOne
  10 | import TypeAligned.TwoThree
  11 | 
  12 | %default total
  13 | %prefix_record_projections off
  14 | 
  15 | export
  16 | data TypeAligned : Rel a -> Rel a
  17 | -- forward declaration
  18 | 
  19 | namespace Multiple
  20 |   ||| 2 or more relationships / proofs stiched together, cons, snoc, uncons, and unsnoc are all amortized constant time.
  21 |   record Multiple (p : Rel a) (u : a) (z : a) where
  22 |     constructor MkMultiple
  23 |     {0 v, w, x, y : a}
  24 |     1 head : p u v
  25 |     1 front : ZeroOne p v w
  26 |     1 body : TypeAligned (TwoThree p) w x
  27 |     1 back : ZeroOne p x y
  28 |     1 last : p y z
  29 | 
  30 | ||| 1 or more, transitive closure of a relationship.  Name is in the pattern of `List1`.
  31 | export
  32 | data TypeAligned1 : Rel a -> Rel a where
  33 |   One : {0 p : Rel a} -> p x y -@ TypeAligned1 p x y
  34 |   Ton : Multiple p x y -@ TypeAligned1 p x y
  35 | 
  36 | -- definition only
  37 | ||| Reflexive, transition closure of a relationship
  38 | data TypeAligned : Rel a -> Rel a where
  39 |   None : (0 eq : x = y) -> TypeAligned p x y
  40 |   Some : TypeAligned1 p x y -@ TypeAligned p x y
  41 | 
  42 | namespace Multiple
  43 |   ||| Explicit, linear prefix accessor
  44 |   head : (m : Multiple p u z) -> p u m.v
  45 |   head (MkMultiple h _ _ _ _) = h
  46 | 
  47 |   ||| Explicit, linear prefix accessor
  48 |   front : (m : Multiple p u z) -> ZeroOne p m.v m.w
  49 |   front (MkMultiple _ f _ _ _) = f
  50 | 
  51 |   ||| Explicit, linear prefix accessor
  52 |   body : (m : Multiple p u z) -> TypeAligned (TwoThree p) m.w m.x
  53 |   body (MkMultiple _ _ b _ _) = b
  54 | 
  55 |   ||| Explicit, linear prefix accessor
  56 |   back : (m : Multiple p u z) -> ZeroOne p m.x m.y
  57 |   back (MkMultiple _ _ _ b _) = b
  58 | 
  59 |   ||| Explicit, linear prefix accessor
  60 |   last : (m : Multiple p u z) -> p m.y z
  61 |   last (MkMultiple _ _ _ _ l) = l
  62 | 
  63 | parameters {0 p : Rel a}
  64 |   namespace NonEmpty
  65 |     ||| Synthetic accesssor; second index
  66 |     export
  67 |     0 (.x) : TypeAligned1 p w z -> a
  68 |     (.x) (One _) = z
  69 |     (.x) (Ton m) = m.v
  70 | 
  71 |     ||| Synthetic accessor; second-last index
  72 |     export
  73 |     0 (.y) : TypeAligned1 p w z -> a
  74 |     (.y) (One _) = w
  75 |     (.y) (Ton m) = m.y
  76 | 
  77 |   ||| Synthetic accesssor; second index
  78 |   export
  79 |   0 (.x) : TypeAligned p w z -> a
  80 |   (.x) (None _) = z
  81 |   (.x) (Some s) = s.x
  82 | 
  83 |   ||| Synthetic accessor; second-last index
  84 |   export
  85 |   0 (.y) : TypeAligned p w z -> a
  86 |   (.y) (None _) = w
  87 |   (.y) (Some s) = s.y
  88 | 
  89 | namespace NonEmpty
  90 |   ||| Synthetic accessor
  91 |   export
  92 |   head, (.head) : (ne : TypeAligned1 p w z) -> p w ne.x
  93 |   head (One wz) = wz
  94 |   head (Ton m) = m.head
  95 |   (.head) = head
  96 | 
  97 |   ||| Synthetic accessor
  98 |   export
  99 |   last, (.last) : (ne : TypeAligned1 p w z) -> p ne.y z
 100 |   last (One wz) = wz
 101 |   last (Ton m) = m.last
 102 |   (.last) = last
 103 | 
 104 | ||| List and SnocList empty syntax
 105 | export
 106 | Nil, Lin : TypeAligned p x x
 107 | Nil = None Refl
 108 | Lin = Nil
 109 | 
 110 | ||| Linear `nonEmpty`
 111 | export
 112 | nonEmptyOnce : TypeAligned p x y -@ ZeroOne (TypeAligned1 p) x y
 113 | nonEmptyOnce (None eq) = Zero (irrelevantEq eq)
 114 | nonEmptyOnce (Some ne) = One ne
 115 | 
 116 | ||| Determine if a possibly empty sequence is non-empty.
 117 | export
 118 | nonEmpty : TypeAligned p x y -> ZeroOne (TypeAligned1 p) x y
 119 | nonEmpty xy = nonEmptyOnce xy
 120 | 
 121 | ||| Helper for equality tests
 122 | heqNonEmpty : (TypeAligned1 p w x -> TypeAligned1 p y z -> Bool) -> TypeAligned p w x -> TypeAligned p y z -> Bool
 123 | heqNonEmpty heqNe = hne
 124 | where
 125 |   hne : TypeAligned p w x -> TypeAligned p y z -> Bool
 126 |   hne (None _) (None _) = True
 127 |   hne (None _) _ = False
 128 |   hne (Some neL) (Some neR) = heqNe neL neR
 129 |   hne (Some _) _ = False
 130 | 
 131 | ||| Linear `fromNonEmpty`
 132 | export
 133 | fromNonEmptyOnce : {0 p : Rel a} -> TypeAligned1 p x y -@ TypeAligned p x y
 134 | fromNonEmptyOnce = Some
 135 | 
 136 | ||| Treat a non-empty sequence as possibly empty
 137 | export
 138 | fromNonEmpty : {0 p : Rel a} -> TypeAligned1 p x y -> TypeAligned p x y
 139 | fromNonEmpty ne = fromNonEmptyOnce ne
 140 | 
 141 | parameters {0 p : Rel a}
 142 |   parameters (1 xy : p x y)
 143 |     namespace NonEmpty
 144 |       ||| Linear `singleton`
 145 |       export
 146 |       singletonce : TypeAligned1 p x y
 147 |       singletonce = One xy
 148 | 
 149 |     ||| Linear `singleton`
 150 |     export
 151 |     singletonce : TypeAligned p x y
 152 |     singletonce = Some singletonce
 153 | 
 154 |   parameters (xy : p x y)
 155 |     namespace NonEmpty
 156 |       ||| Single-relationsip non-empty sequence
 157 |       export
 158 |       singleton : TypeAligned1 p x y
 159 |       singleton = singletonce xy
 160 | 
 161 |     ||| Single-relations sequence
 162 |     export
 163 |     singleton : TypeAligned p x y
 164 |     singleton = fromNonEmpty singleton
 165 | 
 166 | namespace NonEmpty
 167 |   ||| Linear `cons`
 168 |   export
 169 |   consOnce : {0 p : Rel a} -> p x y -@ TypeAligned1 p y z -@ TypeAligned1 p x z
 170 |   -- forward declaration
 171 | 
 172 | parameters {0 p : Rel a}
 173 |   parameters (1 xy : p x y)
 174 |     namespace Multiple
 175 |       ||| Linear `cons`
 176 |       consOnce : Multiple p y z -@ Multiple p x z
 177 |       consOnce (MkMultiple head (Zero eqvw) body back last) =
 178 |         MkMultiple { head = xy, front = One (rewrite sym eqvw in head), body = body, back = back, last = last }
 179 |       consOnce (MkMultiple head (One vw) (None eqwx) (Zero eqxy) last) =
 180 |         MkMultiple
 181 |           { head = xy, front = One head, body = Nil, back = One (rewrite sym (trans eqwx eqxy) in vw), last = last }
 182 |       consOnce (MkMultiple head (One vw) (None eqwx) (One bxy) last) =
 183 |         MkMultiple
 184 |           { head = xy, front = ZeroEq, body = singletonce (twice head (rewrite sym eqwx in vw)), back = One bxy, last = last }
 185 |       consOnce (MkMultiple head (One vw) (Some ne) back last) =
 186 |         MkMultiple
 187 |           { head = xy, front = ZeroEq, body = fromNonEmptyOnce (consOnce (twice head vw) ne), back = back, last = last }
 188 | 
 189 |     namespace NonEmpty
 190 |       ||| Linear `cons2`
 191 |       cons2Once : TypeAligned1 p y z -@ Multiple p x z
 192 |       cons2Once (One yz) = MkMultiple { head = xy, front = ZeroEq, body = Nil, back = ZeroEq, last = yz}
 193 |       cons2Once (Ton yz) = consOnce yz
 194 | 
 195 |     ||| Linear `cons1`
 196 |     export
 197 |     cons1Once : TypeAligned p y z -@ TypeAligned1 p x z
 198 |     cons1Once (None Refl) = One xy
 199 |     cons1Once (Some ne) = consOnce xy ne
 200 | 
 201 |     ||| Linear `cons`
 202 |     export
 203 |     consOnce : TypeAligned p y z -@ TypeAligned p x z
 204 |     consOnce ta = Some (cons1Once ta)
 205 | 
 206 |   parameters (xy : p x y)
 207 |     namespace Multiple
 208 |       ||| Add one relationship to the beginning
 209 |       cons, (::) : Multiple p y z -> Multiple p x z
 210 |       cons yz = consOnce xy yz
 211 |       (::) = cons
 212 | 
 213 |     namespace NonEmpty
 214 |       ||| cons to non-empty is multiple
 215 |       cons2 : TypeAligned1 p y z -> Multiple p x z
 216 |       cons2 yz = cons2Once xy yz
 217 | 
 218 |       ||| Add one relationship to the beginning
 219 |       export
 220 |       cons, (::) : TypeAligned1 p y z -> TypeAligned1 p x z
 221 |       cons yz = Ton (cons2 yz)
 222 |       (::) = cons
 223 | 
 224 |     ||| cons is non-empty
 225 |     export
 226 |     cons1 : TypeAligned p y z -> TypeAligned1 p x z
 227 |     cons1 yz = cons1Once xy yz
 228 | 
 229 |     ||| Add one relationship to the beginning
 230 |     export
 231 |     cons, (::) : TypeAligned p y z -> TypeAligned p x z
 232 |     cons yz = Some (cons1 yz)
 233 |     (::) = cons
 234 | 
 235 | namespace NonEmpty
 236 |   -- definition only
 237 |   consOnce xy ne = Ton (cons2Once xy ne)
 238 | 
 239 | namespace NonEmpty
 240 |   ||| Linear `uncons`
 241 |   export
 242 |   unconsOnce : (1 ne : TypeAligned1 p w z) -> LPair (p w ne.x) (TypeAligned p ne.x z)
 243 |   -- forward declaraction
 244 | 
 245 | namespace Multiple
 246 |   ||| Linear `uncons`
 247 |   unconsOnce : (1 uz : Multiple p u z) -> LPair (p u uz.v) (TypeAligned1 p uz.v z)
 248 |   unconsOnce (MkMultiple {v} {w} {x} {y} head front body back last) = head # tail front body back last
 249 |   where
 250 |     tail : ZeroOne p v w -@ TypeAligned (TwoThree p) w x -@ ZeroOne p x y -@ p y z -@ TypeAligned1 p v z
 251 |     tail (Zero eqvw) (None eqwx) (Zero eqxy) last = One (rewrite trans (trans eqvw eqwx) eqxy in last)
 252 |     tail (Zero eqvw) (None eqwx) (One back) last =
 253 |       Ton (MkMultiple { head = rewrite trans eqvw eqwx in back, front = ZeroEq, body = Nil, back = ZeroEq, last = last})
 254 |     tail (Zero eqvw) (Some ne) back last = Ton (rewrite eqvw in body (unconsOnce ne) back last)
 255 |     where
 256 |       body : LPair (TwoThree p w ne.x) (TypeAligned (TwoThree p) ne.x x) -@ ZeroOne p x y -@ p y z -@ Multiple p w z
 257 |       body (Left (MkDuo fst snd) # bodyTail) back last =
 258 |         MkMultiple { head = fst, front = One snd, body = bodyTail, back = back, last = last }
 259 |       body (Right (MkTrio fst3 snd3 thrd) # bodyTail) back last =
 260 |         MkMultiple { head = fst3, front = ZeroEq, body = consOnce (twice snd3 thrd) bodyTail, back = back, last = last }
 261 |     tail (One vw) body back last = Ton (MkMultiple { head = vw, front = ZeroEq, body = body, back = back, last = last })
 262 | 
 263 | namespace NonEmpty
 264 |   -- definition only
 265 |   unconsOnce (One uz) = uz # Nil
 266 |   unconsOnce (Ton m) = mapSnd fromNonEmptyOnce (unconsOnce m)
 267 | 
 268 | ||| Instead of Nothing, failure to uncons proves index equality
 269 | export
 270 | unconsOnce : (1 ta : TypeAligned p w z) -> LEither (w = z) (LPair (p w ta.x) (TypeAligned p ta.x z))
 271 | unconsOnce (None eq) = Left (irrelevantEq eq)
 272 | unconsOnce (Some ne) = Right (unconsOnce ne)
 273 | 
 274 | namespace Multiple
 275 |   ||| View/remove the leftmost (first) primitive
 276 |   uncons : (uz : Multiple p u z) -> (p u uz.v, TypeAligned1 p uz.v z)
 277 |   uncons uz = uc (unconsOnce uz)
 278 |   where
 279 |     uc : LPair (p u uz.v) (TypeAligned1 p uz.v z) -> (p u uz.v, TypeAligned1 p uz.v z)
 280 |     uc (head # tail) = (head, tail)
 281 | 
 282 |   ||| Drop the first primitive
 283 |   tail : (uz : Multiple p u z) -> TypeAligned1 p uz.v z
 284 |   tail uz = snd (uncons uz)
 285 | 
 286 | namespace NonEmpty
 287 |   ||| View/remove the leftmost (first) primitive
 288 |   export
 289 |   uncons : (ne : TypeAligned1 p w z) -> (p w ne.x, TypeAligned p ne.x z)
 290 |   uncons (One xz) = (xz, Nil)
 291 |   uncons (Ton xz) = map fromNonEmpty (uncons xz)
 292 | 
 293 |   ||| Drop the first primitive
 294 |   export
 295 |   tail : (ne : TypeAligned1 p w z) -> TypeAligned p ne.x z
 296 |   tail ne = snd (uncons ne)
 297 | 
 298 | ||| Instead of Nothing, failure to uncons proves index equality
 299 | export
 300 | uncons : (ta : TypeAligned p w z) -> Either (w = z) (p w ta.x, TypeAligned p ta.x z)
 301 | uncons (None eq) = Left (irrelevantEq eq)
 302 | uncons (Some xz) = Right (uncons xz)
 303 | 
 304 | ||| Extract the first primitive, if none prove index equality
 305 | export
 306 | head : (ta : TypeAligned p w z) -> Either (w = z) (p w ta.x)
 307 | head ta = map fst (uncons ta)
 308 | 
 309 | ||| Drop the first prinitive, if none prove index equality
 310 | export
 311 | tail : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p ta.x z)
 312 | tail ta = map snd (uncons ta)
 313 | 
 314 | namespace NonEmpty
 315 |   ||| Equality test like a non-empty list
 316 |   export
 317 |   heqCons : ({0 w, x, y, z : a} -> p w x -> p y z -> Bool) -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool
 318 |   heqCons heqP = hc
 319 |   where
 320 |     hc : {0 w, x, y, z : a} -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool
 321 |     hc l r = hp (uncons l) (uncons r)
 322 |     where
 323 |       hp : {0 w, x, y, z : a} -> (p w l.x, TypeAligned p l.x x) -> (p y r.x, TypeAligned p r.x z) -> Bool
 324 |       hp (headL, tailL) (headR, tailR) = heqP headL headR && assert_total (heqNonEmpty hc tailL tailR) -- smaller by heads
 325 | 
 326 | ||| Equality test like a list
 327 | export
 328 | heqCons : ({0 w, x, y, z : a} -> p w x -> p y z -> Bool) -> TypeAligned p w x -> TypeAligned p y z -> Bool
 329 | heqCons heqP = heqNonEmpty (heqCons heqP)
 330 | 
 331 | namespace NonEmpty
 332 |   ||| Linear `snoc`
 333 |   export
 334 |   snocOnce : TypeAligned1 p x y -@ p y z -@ TypeAligned1 p x z
 335 |   -- forward declaration
 336 | 
 337 | namespace Multiple
 338 |   ||| Linear `snoc`
 339 |   snocOnce : Multiple p x y -@ p y z -@ Multiple p x z
 340 |   snocOnce (MkMultiple head front body (Zero eqxy) last) yz =
 341 |     MkMultiple { head = head, front = front, body = body, back = One (rewrite eqxy in last), last = yz }
 342 |   snocOnce (MkMultiple head (Zero eqvw) (None eqwx) (One back) last) yz =
 343 |     MkMultiple { head = head, front = One (rewrite trans eqvw eqwx in back), body = Lin, back = One last, last = yz }
 344 |   snocOnce (MkMultiple head (One front) (None eqwx) (One back) last) yz =
 345 |     MkMultiple
 346 |       { head = head, front = One front, body = singletonce (twice (rewrite eqwx in back) last), back = ZeroEq, last = yz }
 347 |   snocOnce (MkMultiple head front (Some body) (One back) last) yz =
 348 |     MkMultiple
 349 |       { head = head, front = front, body = fromNonEmptyOnce (snocOnce body (twice back last)), back = ZeroEq, last = yz }
 350 | 
 351 | namespace NonEmpty
 352 |   ||| Linear `snoc2`
 353 |   snoc2Once : TypeAligned1 p x y -@ p y z -@ Multiple p x z
 354 |   snoc2Once (One xy) yz = MkMultiple { head = xy, front = ZeroEq, body = Lin, back = ZeroEq, last = yz }
 355 |   snoc2Once (Ton m) yz = snocOnce m yz
 356 | 
 357 |   -- definition only
 358 |   snocOnce xy yz = Ton (snoc2Once xy yz)
 359 | 
 360 | ||| Linear `snoc1`
 361 | export
 362 | snoc1Once : TypeAligned p x y -@ p y z -@ TypeAligned1 p x z
 363 | snoc1Once (None Refl) yz = One yz
 364 | snoc1Once (Some xy) yz = snocOnce xy yz
 365 | 
 366 | ||| Linear `snoc`
 367 | export
 368 | snocOnce : TypeAligned p x y -@ p y z -@ TypeAligned p x z
 369 | snocOnce xy yz = Some (snoc1Once xy yz)
 370 | 
 371 | namespace Multiple
 372 |   ||| Add one relationship to the right
 373 |   snoc, (:<) : Multiple p x y -> p y z -> Multiple p x z
 374 |   snoc xy yz = snocOnce xy yz
 375 |   (:<) = snoc
 376 | 
 377 | namespace NonEmpty
 378 |   ||| snoc guarantees a Multiple result
 379 |   snoc2 : TypeAligned1 p x y -> p y z -> Multiple p x z
 380 |   snoc2 xy yz = snoc2Once xy yz
 381 | 
 382 |   ||| Add one relationship to the right
 383 |   export
 384 |   snoc, (:<) : TypeAligned1 p x y -> p y z -> TypeAligned1 p x z
 385 |   snoc xy yz = Ton (snoc2 xy yz)
 386 |   (:<) = snoc
 387 | 
 388 | ||| snoc guarantees a non-empty result
 389 | export
 390 | snoc1 : TypeAligned p x y -> p y z -> TypeAligned1 p x z
 391 | snoc1 xy yz = snoc1Once xy yz
 392 | 
 393 | ||| Add one relationship to the right
 394 | export
 395 | snoc, (:<) : TypeAligned p x y -> p y z -> TypeAligned p x z
 396 | snoc xy yz = Some (snoc1 xy yz)
 397 | (:<) = snoc
 398 | 
 399 | namespace NonEmpty
 400 |   ||| Linear `unsnoc`
 401 |   export
 402 |   unsnocOnce : (1 ne : TypeAligned1 p w z) -> LPair (TypeAligned p w ne.y) (p ne.y z)
 403 |   -- forward declaration
 404 | 
 405 | namespace Multiple
 406 |   ||| Linear `unsnoc`
 407 |   unsnocOnce : (1 m : Multiple p u z) -> LPair (TypeAligned1 p u m.y) (p m.y z)
 408 |   unsnocOnce (MkMultiple {v} {w} {x} {y} head front body back last) = init head front body back # last
 409 |   where
 410 |     init : p u v -@ ZeroOne p v w -@ TypeAligned (TwoThree p) w x -@ ZeroOne p x y -@ TypeAligned1 p u y
 411 |     init head (Zero eqvw) (None eqwx) (Zero eqxy) = One (rewrite sym (trans eqvw (trans eqwx eqxy)) in head)
 412 |     init head (One front) (None eqwx) (Zero eqxy) =
 413 |       Ton
 414 |         (MkMultiple { head = head, front = ZeroEq, body = Lin, back = ZeroEq, last = rewrite sym (trans eqwx eqxy) in front })
 415 |     init head front (Some ne) (Zero eqxy) = Ton (rewrite sym eqxy in body head front (unsnocOnce ne))
 416 |     where
 417 |       body : p u v -@ ZeroOne p v w -@ LPair (TypeAligned (TwoThree p) w ne.y) (TwoThree p ne.y x) -@ Multiple p u x
 418 |       body head front (init # Left (MkDuo fst snd)) =
 419 |         MkMultiple { head = head, front = front, body = init, back = One fst, last = snd }
 420 |       body head front (init # Right (MkTrio fst3 snd3 thrd)) =
 421 |         MkMultiple { head = head, front = front, body = snocOnce init (twice fst3 snd3), back = ZeroEq, last = thrd }
 422 |     init head front body (One back) = Ton (MkMultiple { head = head, front = front, body = body, back = ZeroEq, last = back })
 423 | 
 424 | namespace NonEmpty
 425 |   -- definition only
 426 |   unsnocOnce (One wz) = Lin # wz
 427 |   unsnocOnce (Ton m) = mapFst fromNonEmptyOnce (unsnocOnce m)
 428 | 
 429 | ||| Linear `unsnoc`
 430 | export
 431 | unsnocOnce : (1 ta : TypeAligned p w z) -> LEither (w = z) (LPair (TypeAligned p w ta.y) (p ta.y z))
 432 | unsnocOnce (None eq) = Left (irrelevantEq eq)
 433 | unsnocOnce (Some ne) = Right (unsnocOnce ne)
 434 | 
 435 | namespace Multiple
 436 |   ||| View/remove rightmost (last) relationship
 437 |   unsnoc : (uz : Multiple p u z) -> (TypeAligned1 p u uz.y, p uz.y z)
 438 |   unsnoc uz = us (unsnocOnce uz)
 439 |   where
 440 |     us : LPair (TypeAligned1 p u uz.y) (p uz.y z) -> (TypeAligned1 p u uz.y, p uz.y z)
 441 |     us (init # last) = (init, last)
 442 | 
 443 |   ||| Drop last relationship
 444 |   init : (uz : Multiple p u z) -> TypeAligned1 p u uz.y
 445 |   init uz = fst (unsnoc uz)
 446 | 
 447 | namespace NonEmpty
 448 |   ||| View/remove rightmost (last) relationship
 449 |   export
 450 |   unsnoc : (ne : TypeAligned1 p w z) -> (TypeAligned p w ne.y, p ne.y z)
 451 |   unsnoc (One xz) = (Lin, xz)
 452 |   unsnoc (Ton xz) = mapFst fromNonEmpty (unsnoc xz)
 453 | 
 454 |   ||| Drop last relationship
 455 |   export
 456 |   init : (ne : TypeAligned1 p w z) -> TypeAligned p w ne.y
 457 |   init ne = fst (unsnoc ne)
 458 | 
 459 | ||| Rather than Nothing, failure to unsnoc proves index equality.
 460 | export
 461 | unsnoc : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p w ta.y, p ta.y z)
 462 | unsnoc (None eq) = Left (irrelevantEq eq)
 463 | unsnoc (Some xz) = Right (unsnoc xz)
 464 | 
 465 | ||| Drop last relationship, if none prove index equality.
 466 | export
 467 | init : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p w ta.y)
 468 | init ta = map fst (unsnoc ta)
 469 | 
 470 | ||| Extract last relationship, if none prove index equality.
 471 | export
 472 | last : (ta : TypeAligned p w z) -> Either (w = z) (p ta.y z)
 473 | last ta = map snd (unsnoc ta)
 474 | 
 475 | namespace NonEmpty
 476 |   ||| Equality test like a non-empty snoc list
 477 |   export
 478 |   heqSnoc : ({0 w, x, y, z : a} -> p w x -> p y z -> Bool) -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool
 479 |   heqSnoc heqP = hs
 480 |   where
 481 |     hs : {0 w, x, y, z : a} -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool
 482 |     hs l r = hp (unsnoc l) (unsnoc r)
 483 |     where
 484 |       hp : {0 w, x, y, z : a} -> (TypeAligned p w l.y, p l.y x) -> (TypeAligned p y r.y, p r.y z) -> Bool
 485 |       hp (initL, lastL) (initR, lastR) = assert_total {- smaller by tails -} (heqNonEmpty hs initL initR) && heqP lastL lastR
 486 | 
 487 | ||| Equality test like a snoc list
 488 | export
 489 | heqSnoc : ({0 w, x, y, z : a} -> p w x -> p y z -> Bool) -> TypeAligned p w x -> TypeAligned p y z -> Bool
 490 | heqSnoc heqP = heqNonEmpty (heqSnoc heqP)
 491 | 
 492 | ||| Linear `append`
 493 | export
 494 | appendOnce : TypeAligned p x y -@ TypeAligned p y z -@ TypeAligned p x z
 495 | -- forward declaration
 496 | 
 497 | namespace Multiple
 498 |   ||| Linear `append`
 499 |   appendOnce : Multiple p x y -@ Multiple p y z -@ Multiple p x z
 500 |   appendOnce
 501 |     (MkMultiple {w=lw} {x=lx} {y=ly} lhead lfront lbody lback llast)
 502 |     (MkMultiple {v} {w=rw} {x=rx} rhead rfront rbody rback rlast)
 503 |     =
 504 |     MkMultiple
 505 |       { head = lhead
 506 |       , front = lfront
 507 |       , body = assert_total (body lbody lback llast rhead rfront rbody) -- at lest 2 elements (lhead, rlast) smaller
 508 |       , back = rback
 509 |       , last = rlast
 510 |       }
 511 |   where
 512 |     body :
 513 |       TypeAligned (TwoThree p) lw lx -@ ZeroOne p lx ly -@ p ly y -@
 514 |       p y v -@ ZeroOne p v rw -@ TypeAligned (TwoThree p) rw rx -@
 515 |       TypeAligned (TwoThree p) lw rx
 516 |     body i (Zero eqlxy) l h (Zero eqrvw) t =
 517 |       appendOnce i (consOnce (twice (rewrite eqlxy in l) (rewrite sym eqrvw in h)) t)
 518 |     body i (Zero eqlxy) l h (One rvw) t =
 519 |       appendOnce i (consOnce (thrice (rewrite eqlxy in l) h rvw) t)
 520 |     body i (One lxy) l h (Zero eqrvw) t =
 521 |       appendOnce (snocOnce i (thrice lxy l (rewrite sym eqrvw in h))) t
 522 |     body i (One lxy) l h (One rvw) t =
 523 |       appendOnce (snocOnce i (twice lxy l)) (consOnce (twice h rvw) t)
 524 | 
 525 | namespace NonEmpty
 526 |   ||| Linear `append2`
 527 |   append2Once : TypeAligned1 p x y -@ TypeAligned1 p y z -@ Multiple p x z
 528 |   append2Once (One l) = cons2Once l
 529 |   append2Once (Ton l) = prepend l
 530 |   where
 531 |     prepend : Multiple p x y -@ TypeAligned1 p y z -@ Multiple p x z
 532 |     prepend l (One r) = snocOnce l r
 533 |     prepend l (Ton r) = appendOnce l r
 534 | 
 535 |   ||| Linear `append`
 536 |   export
 537 |   appendOnce : TypeAligned1 p x y -@ TypeAligned1 p y z -@ TypeAligned1 p x z
 538 |   appendOnce l r = Ton (append2Once l r)
 539 | 
 540 | -- definition only
 541 | appendOnce (None Refl) r = r
 542 | appendOnce l (None Refl) = l
 543 | appendOnce (Some l) (Some r) = Some (appendOnce l r)
 544 | 
 545 | namespace Multiple
 546 |   ||| Join two Multiple values (2 or more type-aligned primitives)
 547 |   append, (++) : Multiple p x y -> Multiple p y z -> Multiple p x z
 548 |   append xy yz = appendOnce xy yz
 549 |   (++) = append
 550 | 
 551 | namespace NonEmpty
 552 |   ||| Appending two non-empty lists is guaranteed to product a Multiple
 553 |   append2 : TypeAligned1 p x y -> TypeAligned1 p y z -> Multiple p x z
 554 |   append2 l r = append2Once l r
 555 | 
 556 |   ||| Join two TypeAligned1 sequences
 557 |   export
 558 |   append, (++) : TypeAligned1 p x y -> TypeAligned1 p y z -> TypeAligned1 p x z
 559 |   append l r = Ton (append2 l r)
 560 |   (++) = append
 561 | 
 562 | ||| Join two TypeAligned sequences
 563 | export
 564 | append, (++) : TypeAligned p x y -> TypeAligned p y z -> TypeAligned p x z
 565 | append l r = appendOnce l r
 566 | (++) = append
 567 | 
 568 | parameters {0 f : a -> b} {0 q : Rel b}
 569 |   namespace NonEmpty
 570 |     ||| Linear `mapReduce`
 571 |     export
 572 |     mapReduceOnce :
 573 |       {0 p : Rel a} ->
 574 |       ({0 x, y : a} -> p x y -@ q (f x) (f y)) -> ({0 x, y, z : b} -> q x y -@ q y z -@ q x z) ->
 575 |       TypeAligned1 p x y -@ q (f x) (f y)
 576 |     -- forward declaration
 577 | 
 578 |   namespace Multiple
 579 |     ||| Linear `mapReduce`
 580 |     mapReduceOnce :
 581 |       {0 p : Rel a} ->
 582 |       ({0 x, y : a} -> p x y -@ q (f x) (f y)) -> ({0 x, y, z : b} -> q x y -@ q y z -@ q x z) ->
 583 |       Multiple p u z -@ q (f u) (f z)
 584 |     mapReduceOnce pq trans (MkMultiple {v} {w} {x} {y} head front body back last) =
 585 |       trans (left (pq head) front) (middleOut body (right back (pq last)))
 586 |     where
 587 |       middleOut : TypeAligned (TwoThree p) w x -@ q (f x) (f z) -@ q (f w) (f z)
 588 |       middleOut (None eqwx) qRight = rewrite eqwx in qRight
 589 |       middleOut (Some   wx) qRight = trans (mapReduceOnce (mapReduceOnce {q} pq trans) trans wx) qRight
 590 |       left : q (f u) (f v) -@ ZeroOne p v w -@ q (f u) (f w)
 591 |       left qHead (Zero eqvw) = rewrite sym eqvw in qHead
 592 |       left qHead (One    vw) = trans qHead (pq vw)
 593 |       right : ZeroOne p x y -@ q (f y) (f z) -@ q (f x) (f z)
 594 |       right (Zero eqxy) qLast = rewrite eqxy in qLast
 595 |       right (One    xy) qLast = trans (pq xy) qLast
 596 | 
 597 |   namespace NonEmpty
 598 |     -- definition only
 599 |     mapReduceOnce pq     _ (One xy) = pq xy
 600 |     mapReduceOnce pq trans (Ton xy) = mapReduceOnce pq trans xy
 601 | 
 602 |   parameters
 603 |       {0 p : Rel a}
 604 |       (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
 605 |       (trans : {0 x, y, z : b} -> q x y -@ q y z -@ q x z)
 606 |     ||| Linear `mapReduceL`
 607 |     export
 608 |     mapReduceLOnce : q (f x) (f x) -> TypeAligned p x y -@ q (f x) (f y)
 609 |     mapReduceLOnce refl (None Refl) = refl
 610 |     mapReduceLOnce    _ (Some ne) = mapReduceOnce pq trans ne
 611 | 
 612 |     ||| Linear `mapReduceR`
 613 |     export
 614 |     mapReduceROnce : q (f y) (f y) -> TypeAligned p x y -@ q (f x) (f y)
 615 |     mapReduceROnce refl (None Refl) = refl
 616 |     mapReduceROnce    _ (Some ne) = mapReduceOnce pq trans ne
 617 | 
 618 |   namespace NonEmpty
 619 |     ||| Reduce while transforming to a different primitive.
 620 |     export
 621 |     mapReduce :
 622 |       {0 p : Rel a} ->
 623 |       ({0 x, y : a} -> p x y -> q (f x) (f y)) -> ({0 x, y, z : b} -> q x y -> q y z -> q x z) ->
 624 |       TypeAligned1 p x y -> q (f x) (f y)
 625 |     -- forward declaration
 626 | 
 627 |   namespace Multiple
 628 |     ||| Reduce while transforming to a different primitive.
 629 |     mapReduce :
 630 |       {0 p : Rel a} ->
 631 |       ({0 x, y : a} -> p x y -> q (f x) (f y)) -> ({0 x, y, z : b} -> q x y -> q y z -> q x z) ->
 632 |       Multiple p u z -> q (f u) (f z)
 633 |     mapReduce pq trans uz = middleOut uz.body
 634 |     where
 635 |       qHead : q (f u) (f uz.v)
 636 |       qHead = pq uz.head
 637 |       left : ZeroOne p uz.v uz.w -> q (f u) (f uz.w)
 638 |       left (Zero eqvw) = rewrite sym eqvw in qHead
 639 |       left (One vw) = trans qHead (pq vw)
 640 |       qLast : q (f uz.y) (f z)
 641 |       qLast = pq uz.last
 642 |       right : ZeroOne p uz.x uz.y -> q (f uz.x) (f z)
 643 |       right (Zero eqxy) = rewrite eqxy in qLast
 644 |       right (One xy) = trans (pq xy) qLast
 645 |       qLeft : q (f u) (f uz.w)
 646 |       qLeft = left uz.front
 647 |       qRight : q (f uz.x) (f z)
 648 |       qRight = right uz.back
 649 |       middleOut : TypeAligned (TwoThree p) uz.w uz.x -> q (f u) (f z)
 650 |       middleOut (None eqwx) = trans qLeft (rewrite eqwx in qRight)
 651 |       middleOut (Some wx) = trans qLeft (trans (mapReduce (mapReduce {q} pq trans) trans (assert_smaller uz wx)) qRight)
 652 | 
 653 |   namespace NonEmpty
 654 |     -- definition only
 655 |     mapReduce pq     _ (One xy) = pq xy
 656 |     mapReduce pq trans (Ton xy) = mapReduce pq trans xy
 657 | 
 658 |   parameters
 659 |       {0 p : Rel a}
 660 |       (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
 661 |       (trans : {0 x, y, z : b} -> q x y -> q y z -> q x z)
 662 |     export
 663 |     ||| Reduce from the left while transforming.
 664 |     mapReduceL : q (f x) (f x) -> TypeAligned p x y -> q (f x) (f y)
 665 |     mapReduceL refl (None Refl) = refl
 666 |     mapReduceL    _ (Some ne) = mapReduce pq trans ne
 667 | 
 668 |     ||| Reduce from the right while transforming.
 669 |     export
 670 |     mapReduceR : q (f y) (f y) -> TypeAligned p x y -> q (f x) (f y)
 671 |     mapReduceR refl (None Refl) = refl
 672 |     mapReduceR    _ (Some ne) = mapReduce pq trans ne
 673 | 
 674 | parameters {0 f : a -> b}
 675 |   ||| Linear `map`
 676 |   export
 677 |   mapOnce :
 678 |     {0 p : Rel a} -> {0 q : Rel b} -> ({0 x, y : a} -> p x y -@ q (f x) (f y)) ->
 679 |     TypeAligned p x y -@ TypeAligned q (f x) (f y)
 680 |   -- forward declaration
 681 | 
 682 |   parameters {0 p : Rel a} {0 q : Rel b} (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
 683 |     namespace Multiple
 684 |       ||| Linear `map`
 685 |       mapOnce : Multiple p x y -@ Multiple q (f x) (f y)
 686 |       mapOnce (MkMultiple head front body back last) =
 687 |         MkMultiple
 688 |           { head = pq head
 689 |           , front = mapOnce pq front
 690 |           , body = assert_total (mapOnce (mapOnce pq) body) -- at least 2 elements (head, last) smaller
 691 |           , back = mapOnce pq back
 692 |           , last = pq last
 693 |           }
 694 | 
 695 |     namespace NonEmpty
 696 |       ||| Linear `map`
 697 |       export
 698 |       mapOnce : TypeAligned1 p x y -@ TypeAligned1 q (f x) (f y)
 699 |       mapOnce (One xy) = One (pq xy)
 700 |       mapOnce (Ton m) = Ton (mapOnce m)
 701 | 
 702 |   -- definition only
 703 |   mapOnce pq (None eq) = None (cong f eq)
 704 |   mapOnce pq (Some ne) = Some (mapOnce pq ne)
 705 | 
 706 |   ||| Change inner relation
 707 |   export
 708 |   map :
 709 |     {0 p : Rel a} -> {0 q : Rel b} -> ({0 x, y : a} -> p x y -> q (f x) (f y)) ->
 710 |     TypeAligned p x y -> TypeAligned q (f x) (f y)
 711 |   -- forward declaration
 712 | 
 713 |   parameters {0 p : Rel a} {0 q : Rel b} (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
 714 |     namespace Multiple
 715 |       ||| Change inner relation
 716 |       map : Multiple p x y -> Multiple q (f x) (f y)
 717 |       map xy =
 718 |         MkMultiple
 719 |           { head = pq xy.head
 720 |           , front = map pq xy.front
 721 |           , body = assert_total (map (map pq) xy.body) -- Q: Why is assert_smaller is not powerful enough
 722 |           , back = map pq xy.back
 723 |           , last = pq xy.last
 724 |           }
 725 | 
 726 |     namespace NonEmpty
 727 |       ||| Change inner relation
 728 |       export
 729 |       map : TypeAligned1 p x y -> TypeAligned1 q (f x) (f y)
 730 |       map (One xy) = One (pq xy)
 731 |       map (Ton m) = Ton (map m)
 732 | 
 733 |   -- definition only
 734 |   map  _ (None eq) = None (cong f eq)
 735 |   map pq (Some ne) = Some (map pq ne)
 736 | 
 737 | parameters {0 p : Rel a} (trans : {0 x, y, z : a} -> p x y -@ p y z -@ p x z)
 738 |   namespace Multiple
 739 |     ||| Linear `reduce`
 740 |     reduceOnce : Multiple p u z -@ p u z
 741 |     reduceOnce uz = mapReduceOnce {q=p} id trans uz
 742 | 
 743 |   namespace NonEmpty
 744 |     ||| Linear `reduce`
 745 |     export
 746 |     reduceOnce : TypeAligned1 p x y -@ p x y
 747 |     reduceOnce (One xy) = xy
 748 |     reduceOnce (Ton xy) = reduceOnce xy
 749 | 
 750 |   ||| Linear `reduceL`
 751 |   export
 752 |   reduceLOnce : p x x -> TypeAligned p x y -@ p x y
 753 |   reduceLOnce refl (None Refl) = refl
 754 |   reduceLOnce    _ (Some ne) = reduceOnce ne
 755 | 
 756 |   ||| Linear `reduceR`
 757 |   export
 758 |   reduceROnce : p y y -> TypeAligned p x y -@ p x y
 759 |   reduceROnce refl (None Refl) = refl
 760 |   reduceROnce    _ (Some ne) = reduceOnce ne
 761 | 
 762 | parameters {0 p : Rel a} (trans : {0 x, y, z : a} -> p x y -> p y z -> p x z)
 763 |   namespace Multiple
 764 |     ||| Reduce to a single primitive.
 765 |     reduce : Multiple p u z -> p u z
 766 |     reduce uz = mapReduce {q=p} id trans uz -- Q: expand to avoid `id` calls?
 767 | 
 768 |   namespace NonEmpty
 769 |     ||| Reduce to a single primitive.
 770 |     export
 771 |     reduce : TypeAligned1 p x y -> p x y
 772 |     reduce (One xy) = xy
 773 |     reduce (Ton xy) = reduce xy
 774 | 
 775 |   ||| Reduce from the left.
 776 |   export
 777 |   reduceL : p x x -> TypeAligned p x y -> p x y
 778 |   reduceL refl (None Refl) = refl
 779 |   reduceL    _ (Some ne) = reduce ne
 780 | 
 781 |   ||| Reduce from the right.
 782 |   export
 783 |   reduceR : p y y -> TypeAligned p x y -> p x y
 784 |   reduceR refl (None Refl) = refl
 785 |   reduceR    _ (Some ne) = reduce ne
 786 | 
 787 | %prefix_record_projections on
 788 | record StringRel (x : a) (y : a) where
 789 |   constructor MkStringRel
 790 |   1 unStringRel : String
 791 | 
 792 | Show (StringRel x y) where
 793 |   show sr = show sr.unStringRel
 794 | 
 795 | showRel : {0 p : Rel a} -> Show (p x y) => p x y -> StringRel x y
 796 | showRel p = MkStringRel (show p)
 797 | 
 798 | transCommaSpace : StringRel x y -> StringRel y z -> StringRel x z
 799 | transCommaSpace l r = MkStringRel (l.unStringRel ++ ", " ++ r.unStringRel)
 800 | 
 801 | ||| Use a list-like display based on being able to show primitive relationships.  E.g. `[Refl]`.
 802 | export
 803 | {0 p : Rel a} -> ({0 x, y : a} -> Show (p x y)) => Show (TypeAligned1 p x y) where
 804 |   show ne = "[" ++ unStringRel {x} (mapReduce {q=StringRel} showRel transCommaSpace ne) ++ "]"
 805 | 
 806 | ||| Use a list-like display based on being able to show primitive relationships.  E.g. `[]`.
 807 | export
 808 | {0 p : Rel a} -> ({0 x, y : a} -> Show (p x y)) => Show (TypeAligned p x y) where
 809 |   show ta = "[" ++ unStringRel {x} (mapReduceR {q=StringRel} showRel transCommaSpace (MkStringRel "") ta) ++ "]"
 810 | 
 811 | ||| Use a list-ish display based on being able to show primitive relationships.  E.g. `[0 <=, 1 <=, 1 <=, 2 <=]`.
 812 | ||| The body is displayed as a TwoThree List, since if you have a Multiple value you are already exposed to those internals.
 813 | export
 814 | {0 p : Rel a} -> ({0 x, y : a} -> Show (p x y)) => Show (Multiple p x y) where
 815 |   show m =
 816 |     "[" ++ show m.head ++ ", "
 817 |       ++ showOpt m.front
 818 |       ++ assert_total (showOpt (nonEmpty m.body)) -- Q: Why assert_smaller not good enough?
 819 |       ++ showOpt m.back
 820 |       ++ show m.last ++ "]"
 821 |   where
 822 |     showOpt : {0 p : Rel a} -> {0 x, y : a} -> Show (p x y) => ZeroOne p x y -> String
 823 |     showOpt (Zero _) = ""
 824 |     showOpt (One p) = show p ++ ", "
 825 | 
 826 | ||| TypeAligned is reflective indepedent of the primitive.
 827 | export
 828 | Reflexive a (TypeAligned p) where
 829 |   reflexive = None Refl
 830 | 
 831 | ||| Multiple is transitive independent of the primitive.
 832 | export
 833 | Transitive a (Multiple p) where
 834 |   transitive = append
 835 | 
 836 | ||| TypeAligned1 is transitive independent of the primitive.
 837 | export
 838 | Transitive a (TypeAligned1 p) where
 839 |   transitive = append
 840 | 
 841 | ||| TypeAligned is transitive independent of the primitive.
 842 | export
 843 | Transitive a (TypeAligned p) where
 844 |   transitive = append
 845 | 
 846 | ||| Multiple is reflexive if the underlying primitive is reflexive.  NB: This does introduce multiple reflexive primitives.
 847 | export
 848 | Reflexive a p => Reflexive a (Multiple p) where
 849 |   reflexive = MkMultiple { head = reflexive, front = ZeroEq, body = None Refl, back = ZeroEq, last = reflexive }
 850 | 
 851 | ||| TypeAligned1 is reflexive if the underlying primitive is reflexive.
 852 | export
 853 | Reflexive a p => Reflexive a (TypeAligned1 p) where
 854 |   reflexive = One reflexive
 855 |