2020-05-18 15:59:07 +03:00
|
|
|
module Data.Fin
|
|
|
|
|
Fix import loading
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)
This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
things were being imported that shouldn't have been. The new way is
correct!
An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
2020-05-27 17:49:03 +03:00
|
|
|
import public Data.Maybe
|
2020-05-18 15:59:07 +03:00
|
|
|
import Data.Nat
|
2020-12-04 04:49:26 +03:00
|
|
|
import Decidable.Equality.Core
|
2020-05-18 15:59:07 +03:00
|
|
|
|
2020-06-30 01:35:34 +03:00
|
|
|
%default total
|
|
|
|
|
2020-05-18 15:59:07 +03:00
|
|
|
||| 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
|
2020-07-05 20:52:16 +03:00
|
|
|
Uninhabited (Fin Z) where
|
2020-05-18 15:59:07 +03:00
|
|
|
uninhabited FZ impossible
|
|
|
|
uninhabited (FS f) impossible
|
|
|
|
|
2020-06-30 03:55:47 +03:00
|
|
|
export
|
|
|
|
Uninhabited (FZ = FS k) where
|
|
|
|
uninhabited Refl impossible
|
|
|
|
|
|
|
|
export
|
|
|
|
Uninhabited (FS k = FZ) where
|
|
|
|
uninhabited Refl impossible
|
|
|
|
|
2020-05-18 15:59:07 +03:00
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
fsInjective : FS m = FS n -> m = n
|
|
|
|
fsInjective Refl = Refl
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
Eq (Fin n) where
|
2020-05-18 15:59:07 +03:00
|
|
|
(==) FZ FZ = True
|
|
|
|
(==) (FS k) (FS k') = k == k'
|
|
|
|
(==) _ _ = False
|
|
|
|
|
|
|
|
||| Convert a Fin to a Nat
|
|
|
|
public export
|
|
|
|
finToNat : Fin n -> Nat
|
|
|
|
finToNat FZ = Z
|
2020-07-05 20:52:16 +03:00
|
|
|
finToNat (FS k) = S $ finToNat k
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
||| `finToNat` is injective
|
|
|
|
export
|
|
|
|
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
|
2020-07-05 20:52:16 +03:00
|
|
|
finToNatInjective FZ FZ _ = Refl
|
|
|
|
finToNatInjective (FS _) FZ Refl impossible
|
|
|
|
finToNatInjective FZ (FS _) Refl impossible
|
2020-05-18 15:59:07 +03:00
|
|
|
finToNatInjective (FS m) (FS n) prf =
|
2020-07-05 20:52:16 +03:00
|
|
|
cong FS $ finToNatInjective m n $ succInjective (finToNat m) (finToNat n) prf
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
Cast (Fin n) Nat where
|
|
|
|
cast = finToNat
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
||| Convert a Fin to an Integer
|
|
|
|
public export
|
|
|
|
finToInteger : Fin n -> Integer
|
|
|
|
finToInteger FZ = 0
|
|
|
|
finToInteger (FS k) = 1 + finToInteger k
|
|
|
|
|
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
Cast (Fin n) Integer where
|
|
|
|
cast = finToInteger
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
||| Weaken the bound on a Fin by 1
|
|
|
|
public export
|
|
|
|
weaken : Fin n -> Fin (S n)
|
|
|
|
weaken FZ = FZ
|
2020-07-05 20:52:16 +03:00
|
|
|
weaken (FS k) = FS $ weaken k
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
||| Weaken the bound on a Fin by some amount
|
|
|
|
public export
|
2021-02-08 23:37:14 +03:00
|
|
|
weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)
|
2020-05-18 15:59:07 +03:00
|
|
|
weakenN n FZ = FZ
|
2020-07-05 20:52:16 +03:00
|
|
|
weakenN n (FS f) = FS $ weakenN n f
|
2020-05-18 15:59:07 +03:00
|
|
|
|
2020-06-12 00:14:11 +03:00
|
|
|
||| Weaken the bound on a Fin using a constructive comparison
|
|
|
|
public export
|
|
|
|
weakenLTE : Fin n -> LTE n m -> Fin m
|
|
|
|
weakenLTE FZ LTEZero impossible
|
|
|
|
weakenLTE (FS _) LTEZero impossible
|
2020-07-05 20:52:16 +03:00
|
|
|
weakenLTE FZ (LTESucc _) = FZ
|
2020-06-12 00:14:11 +03:00
|
|
|
weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
|
|
|
|
|
2020-05-18 15:59:07 +03:00
|
|
|
||| Attempt to tighten the bound on a Fin.
|
|
|
|
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
|
|
|
|
export
|
|
|
|
strengthen : {n : _} -> Fin (S n) -> Either (Fin (S n)) (Fin n)
|
2020-07-05 20:52:16 +03:00
|
|
|
strengthen {n = S _} FZ = Right FZ
|
|
|
|
strengthen {n = S _} (FS i) with (strengthen i)
|
|
|
|
strengthen (FS _) | Left x = Left $ FS x
|
|
|
|
strengthen (FS _) | Right x = Right $ FS x
|
2020-05-18 15:59:07 +03:00
|
|
|
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
|
|
|
|
public export
|
|
|
|
shift : (m : Nat) -> Fin n -> Fin (m + n)
|
|
|
|
shift Z f = f
|
2020-07-05 20:52:16 +03:00
|
|
|
shift (S m) f = FS $ shift m f
|
2020-05-18 15:59:07 +03:00
|
|
|
|
|
|
|
||| The largest element of some Fin type
|
|
|
|
public export
|
|
|
|
last : {n : _} -> Fin (S n)
|
|
|
|
last {n=Z} = FZ
|
|
|
|
last {n=S _} = FS last
|
|
|
|
|
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
Ord (Fin n) where
|
2020-05-18 15:59:07 +03:00
|
|
|
compare FZ FZ = EQ
|
|
|
|
compare FZ (FS _) = LT
|
|
|
|
compare (FS _) FZ = GT
|
|
|
|
compare (FS x) (FS y) = compare x y
|
|
|
|
|
|
|
|
public export
|
|
|
|
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
|
2020-07-05 20:52:16 +03:00
|
|
|
natToFin Z (S _) = Just FZ
|
2020-05-18 15:59:07 +03:00
|
|
|
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
|
|
|
|
public 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
|
|
|
|
public export
|
|
|
|
fromInteger : (x : Integer) -> {n : Nat} ->
|
2021-02-11 16:18:13 +03:00
|
|
|
{auto 0 prf : (IsJust (integerToFin x n))} ->
|
2020-05-18 15:59:07 +03:00
|
|
|
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`
|
|
|
|
public 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
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
2020-06-30 01:35:34 +03:00
|
|
|
export
|
2020-07-05 20:52:16 +03:00
|
|
|
DecEq (Fin n) where
|
2020-05-18 15:59:07 +03:00
|
|
|
decEq FZ FZ = Yes Refl
|
2020-07-05 20:52:16 +03:00
|
|
|
decEq FZ (FS f) = No absurd
|
|
|
|
decEq (FS f) FZ = No absurd
|
2020-05-18 15:59:07 +03:00
|
|
|
decEq (FS f) (FS f')
|
|
|
|
= case decEq f f' of
|
|
|
|
Yes p => Yes $ cong FS p
|
2020-07-05 20:52:16 +03:00
|
|
|
No p => No $ p . fsInjective
|