module Data.Fin import Data.Maybeimport Data.Natimport Decidable.Equality ||| Numbers strictly less than some bound.  The name comes from "finite sets".|||||| It's probably not a good idea to use `Fin` for arithmetic, and they will be||| exceedingly inefficient at run time.||| @ n the upper boundpublic exportdata Fin : (n : Nat) -> Type where    FZ : Fin (S k)    FS : Fin k -> Fin (S k) exportimplementation Uninhabited (Fin Z) where  uninhabited FZ impossible  uninhabited (FS f) impossible exportFSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = nFSInjective left _ Refl = Refl exportimplementation Eq (Fin n) where    (==) FZ FZ = True    (==) (FS k) (FS k') = k == k'    (==) _ _ = False ||| There are no elements of `Fin Z`exportFinZAbsurd : Fin Z -> VoidFinZAbsurd FZ impossible exportFinZElim : Fin Z -> aFinZElim x = void (FinZAbsurd x) ||| Convert a Fin to a Natpublic exportfinToNat : Fin n -> NatfinToNat FZ = ZfinToNat (FS k) = S (finToNat k) ||| `finToNat` is injectiveexportfinToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fnfinToNatInjective (FS m) FZ     Refl impossiblefinToNatInjective FZ     (FS n) Refl impossiblefinToNatInjective (FS m) (FS n) prf  =  cong FS (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))finToNatInjective FZ     FZ     Refl = Refl exportimplementation Cast (Fin n) Nat where    cast x = finToNat x ||| Convert a Fin to an Integerpublic exportfinToInteger : Fin n -> IntegerfinToInteger FZ     = 0finToInteger (FS k) = 1 + finToInteger k exportimplementation Cast (Fin n) Integer where    cast x = finToInteger x ||| Weaken the bound on a Fin by 1public exportweaken : Fin n -> Fin (S n)weaken FZ     = FZweaken (FS k) = FS (weaken k) ||| Weaken the bound on a Fin by some amountpublic exportweakenN : (n : Nat) -> Fin m -> Fin (m + n)weakenN n FZ = FZweakenN n (FS f) = FS (weakenN n f) ||| Attempt to tighten the bound on a Fin.||| Return `Left` if the bound could not be tightened, or `Right` if it could.exportstrengthen : {n : _} -> Fin (S n) -> Either (Fin (S n)) (Fin n)strengthen {n = S k} FZ = Right FZstrengthen {n = S k} (FS i) with (strengthen i)  strengthen (FS i) | Left x   = Left (FS x)  strengthen (FS i) | Right x  = Right (FS x)strengthen f = Left f ||| Add some natural number to a Fin, extending the bound accordingly||| @ n the previous bound||| @ m the number to increase the Fin bypublic exportshift : (m : Nat) -> Fin n -> Fin (m + n)shift Z f = fshift {n=n} (S m) f = FS {k = (m + n)} (shift m f) ||| The largest element of some Fin typepublic exportlast : {n : _} -> Fin (S n)last {n=Z} = FZlast {n=S _} = FS last export totalFSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'FSinjective Refl = Refl exportimplementation Ord (Fin n) where  compare  FZ     FZ    = EQ  compare  FZ    (FS _) = LT  compare (FS _)  FZ    = GT  compare (FS x) (FS y) = compare x y  -- Construct a Fin from an integer literal which must fit in the given Finpublic exportnatToFin : Nat -> (n : Nat) -> Maybe (Fin n)natToFin Z     (S j) = Just FZnatToFin (S k) (S j)    = case natToFin k j of           Just k' => Just (FS k')           Nothing => NothingnatToFin _ _ = Nothing ||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.||| @n The upper bound of the Finpublic exportintegerToFin : Integer -> (n : Nat) -> Maybe (Fin n)integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!integerToFin x n = if x >= 0 then natToFin (fromInteger x) n else Nothing ||| Allow overloading of Integer literals for Fin.||| @ x the Integer that the user typed||| @ prf an automatically-constructed proof that `x` is in boundspublic exportfromInteger : (x : Integer) -> {n : Nat} ->              {auto prf : (IsJust (integerToFin x n))} ->              Fin nfromInteger {n} x {prf} with (integerToFin x n)  fromInteger {n} x {prf = ItIsJust} | Just y = y ||| Convert an Integer to a Fin in the required bounds/||| This is essentially a composition of `mod` and `fromInteger`public exportrestrict : (n : Nat) -> Integer -> Fin (S n)restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in                     -- reasoning about primitives, so we need the                     -- 'believe_me'. It's fine because val' must be                     -- in the right range                     fromInteger {n = S n} val'                         {prf = believe_me {a=IsJust (Just val')} ItIsJust} ---------------------------------------------------------------------------------- DecEq-------------------------------------------------------------------------------- export totalFZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> VoidFZNotFS Refl impossible exportimplementation DecEq (Fin n) where  decEq FZ FZ = Yes Refl  decEq FZ (FS f) = No FZNotFS  decEq (FS f) FZ = No $ negEqSym FZNotFS  decEq (FS f) (FS f')      = case decEq f f' of             Yes p => Yes $ cong FS p             No p => No $ \h => p $ FSinjective {f = f} {f' = f'} h