
  0 | ||| Conversions of `Fin`s to `Fin`s
  1 | module Data.Fin.ToFin
  2 | 
  3 | import public Data.Fin
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | tryToFit : {to : _} -> Fin from -> Maybe $ Fin to
  9 | tryToFit {to=0}   _      = Nothing
 10 | tryToFit {to=S _} FZ     = Just FZ
 11 | tryToFit {to=S _} (FS x) = FS <$> tryToFit x
 12 | 
 13 | -- weakens the left part, shifts the right one
 14 | public export
 15 | weakenOrShift : (left, mid : _) -> Fin (left + right) -> Fin (left + mid + right)
 16 | weakenOrShift Z     mid x      = shift mid x
 17 | weakenOrShift (S n) mid FZ     = FZ
 18 | weakenOrShift (S n) mid (FS x) = FS $ weakenOrShift n mid x
 19 | 
 20 | public export
 21 | weakenToSuper : {i : Fin n} -> Fin (finToNat i) -> Fin n
 22 | weakenToSuper {i = FS _} FZ     = FZ
 23 | weakenToSuper {i = FS _} (FS x) = FS $ weakenToSuper x
 24 | 
 25 | export
 26 | weakenToSuper_correct : {i : Fin n} -> (x : Fin $ finToNat i) -> finToNat (weakenToSuper {i} x) = finToNat x
 27 | weakenToSuper_correct {i = FS _} FZ     = Refl
 28 | weakenToSuper_correct {i = FS _} (FS x) = cong S $ weakenToSuper_correct x
 29 | 
 30 | export
 31 | weakenOrShiftWithNoShiftIsWeakenN : (left, mid : _) -> (x' : Fin $ left + 0) -> (x : Fin left) -> x' ~~~ x =>
 32 |                                     weakenOrShift left mid {right=0} x' ~~~ weakenN mid x
 33 | weakenOrShiftWithNoShiftIsWeakenN _        _   FZ      FZ             = FZ
 34 | weakenOrShiftWithNoShiftIsWeakenN (S left) mid (FS x') (FS x) @{FS _} = FS $ weakenOrShiftWithNoShiftIsWeakenN left mid x' x
 35 |