mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-20 11:21:43 +03:00
00514887c4
This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
174 lines
5.0 KiB
Idris
174 lines
5.0 KiB
Idris
module Data.Fin
|
|
|
|
import Data.Maybe
|
|
import Data.Nat
|
|
import 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 bound
|
|
public export
|
|
data Fin : (n : Nat) -> Type where
|
|
FZ : Fin (S k)
|
|
FS : Fin k -> Fin (S k)
|
|
|
|
export
|
|
implementation Uninhabited (Fin Z) where
|
|
uninhabited FZ impossible
|
|
uninhabited (FS f) impossible
|
|
|
|
export
|
|
FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
|
|
FSInjective left _ Refl = Refl
|
|
|
|
export
|
|
implementation Eq (Fin n) where
|
|
(==) FZ FZ = True
|
|
(==) (FS k) (FS k') = k == k'
|
|
(==) _ _ = False
|
|
|
|
||| There are no elements of `Fin Z`
|
|
export
|
|
FinZAbsurd : Fin Z -> Void
|
|
FinZAbsurd FZ impossible
|
|
|
|
export
|
|
FinZElim : Fin Z -> a
|
|
FinZElim x = void (FinZAbsurd x)
|
|
|
|
||| Convert a Fin to a Nat
|
|
export
|
|
finToNat : Fin n -> Nat
|
|
finToNat FZ = Z
|
|
finToNat (FS k) = S (finToNat k)
|
|
|
|
||| `finToNat` is injective
|
|
export
|
|
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
|
|
finToNatInjective (FS m) FZ Refl impossible
|
|
finToNatInjective FZ (FS n) Refl impossible
|
|
finToNatInjective (FS m) (FS n) prf =
|
|
cong FS (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
|
|
finToNatInjective FZ FZ Refl = Refl
|
|
|
|
export
|
|
implementation Cast (Fin n) Nat where
|
|
cast x = finToNat x
|
|
|
|
||| Convert a Fin to an Integer
|
|
export
|
|
finToInteger : Fin n -> Integer
|
|
finToInteger FZ = 0
|
|
finToInteger (FS k) = 1 + finToInteger k
|
|
|
|
export
|
|
implementation Cast (Fin n) Integer where
|
|
cast x = finToInteger x
|
|
|
|
||| Weaken the bound on a Fin by 1
|
|
public export
|
|
weaken : Fin n -> Fin (S n)
|
|
weaken FZ = FZ
|
|
weaken (FS k) = FS (weaken k)
|
|
|
|
||| Weaken the bound on a Fin by some amount
|
|
public export
|
|
weakenN : (n : Nat) -> Fin m -> Fin (m + n)
|
|
weakenN n FZ = FZ
|
|
weakenN 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.
|
|
export
|
|
strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
|
|
strengthen {n = S k} FZ = Right FZ
|
|
strengthen {n = S k} (FS i) with (strengthen i)
|
|
strengthen (FS k) | Left x = Left (FS x)
|
|
strengthen (FS k) | 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 by
|
|
export
|
|
shift : (m : Nat) -> Fin n -> Fin (m + n)
|
|
shift Z f = f
|
|
shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
|
|
|
|
||| The largest element of some Fin type
|
|
export
|
|
last : {n : _} -> Fin (S n)
|
|
last {n=Z} = FZ
|
|
last {n=S _} = FS last
|
|
|
|
export total
|
|
FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
|
|
FSinjective Refl = Refl
|
|
|
|
export
|
|
implementation 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 Fin
|
|
export
|
|
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
|
|
natToFin Z (S j) = Just FZ
|
|
natToFin (S k) (S j)
|
|
= case natToFin k j of
|
|
Just k' => Just (FS k')
|
|
Nothing => Nothing
|
|
natToFin _ _ = Nothing
|
|
|
|
||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
|
|
||| @n The upper bound of the Fin
|
|
export
|
|
integerToFin : 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 bounds
|
|
export
|
|
fromInteger : (x : Integer) -> {n : Nat} ->
|
|
{auto prf : (IsJust (integerToFin x n))} ->
|
|
Fin n
|
|
fromInteger {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`
|
|
export
|
|
restrict : (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 total
|
|
FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
|
|
FZNotFS Refl impossible
|
|
|
|
export
|
|
implementation 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
|
|
|