git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/base/Data/Fin.idr
212 lines 7.0 kB history raw
1module Data.Fin
3%default total
4%access public export
6||| Numbers strictly less than some bound. The name comes from "finite sets".
7|||
8||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
9||| exceedingly inefficient at run time.
10||| @ n the upper bound
11data Fin : (n : Nat) -> Type where
12 FZ : Fin (S k)
13 FS : Fin k -> Fin (S k)
15implementation Uninhabited (Fin Z) where
16 uninhabited FZ impossible
17 uninhabited (FS f) impossible
19FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
20FSInjective left _ Refl = Refl
22implementation Eq (Fin n) where
23 (==) FZ FZ = True
24 (==) (FS k) (FS k') = k == k'
25 (==) _ _ = False
27||| There are no elements of `Fin Z`
28FinZAbsurd : Fin Z -> Void
29FinZAbsurd FZ impossible
31FinZElim : Fin Z -> a
32FinZElim x = void (FinZAbsurd x)
34||| Convert a Fin to a Nat
35finToNat : Fin n -> Nat
36finToNat FZ = Z
37finToNat (FS k) = S (finToNat k)
39||| `finToNat` is injective
40finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
41finToNatInjective FZ FZ Refl = Refl
42finToNatInjective (FS m) FZ Refl impossible
43finToNatInjective FZ (FS n) Refl impossible
44finToNatInjective (FS m) (FS n) prf =
45 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
47implementation Cast (Fin n) Nat where
48 cast x = finToNat x
50||| Convert a Fin to an Integer
51finToInteger : Fin n -> Integer
52finToInteger FZ = 0
53finToInteger (FS k) = 1 + finToInteger k
55implementation Cast (Fin n) Integer where
56 cast x = finToInteger x
58||| Weaken the bound on a Fin by 1
59weaken : Fin n -> Fin (S n)
60weaken FZ = FZ
61weaken (FS k) = FS (weaken k)
63||| Weaken the bound on a Fin by some amount
64weakenN : (n : Nat) -> Fin m -> Fin (m + n)
65weakenN n FZ = FZ
66weakenN n (FS f) = FS (weakenN n f)
68||| Attempt to tighten the bound on a Fin.
69||| Return `Left` if the bound could not be tightened, or `Right` if it could.
70strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
71strengthen {n = S k} FZ = Right FZ
72strengthen {n = S k} (FS i) with (strengthen i)
73 strengthen (FS k) | Left x = Left (FS x)
74 strengthen (FS k) | Right x = Right (FS x)
75strengthen f = Left f
77||| Add some natural number to a Fin, extending the bound accordingly
78||| @ n the previous bound
79||| @ m the number to increase the Fin by
80shift : (m : Nat) -> Fin n -> Fin (m + n)
81shift Z f = f
82shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
84||| The largest element of some Fin type
85last : Fin (S n)
86last {n=Z} = FZ
87last {n=S _} = FS last
89total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
90FSinjective Refl = Refl
92implementation Ord (Fin n) where
93 compare FZ FZ = EQ
94 compare FZ (FS _) = LT
95 compare (FS _) FZ = GT
96 compare (FS x) (FS y) = compare x y
98implementation MinBound (Fin (S n)) where
99 minBound = FZ
101implementation MaxBound (Fin (S n)) where
102 maxBound = last
105-- Construct a Fin from an integer literal which must fit in the given Fin
107natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
108natToFin Z (S j) = Just FZ
109natToFin (S k) (S j) with (natToFin k j)
110 | Just k' = Just (FS k')
111 | Nothing = Nothing
112natToFin _ _ = Nothing
114||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
115||| @n The upper bound of the Fin
116integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
117integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
118integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
120||| Allow overloading of Integer literals for Fin.
121||| @ x the Integer that the user typed
122||| @ prf an automatically-constructed proof that `x` is in bounds
123fromInteger : (x : Integer) ->
124 {default ItIsJust
125 prf : (IsJust (integerToFin x n))} ->
126 Fin n
127fromInteger {n} x {prf} with (integerToFin x n)
128 fromInteger {n} x {prf = ItIsJust} | Just y = y
130||| Convert an Integer to a Fin in the required bounds/
131||| This is essentially a composition of `mod` and `fromInteger`
132export
133restrict : (n : Nat) -> Integer -> Fin (S n)
134restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
135 -- reasoning about primitives, so we need the
136 -- 'believe_me'. It's fine because val' must be
137 -- in the right range
138 fromInteger val'
139 {prf = believe_me {a=IsJust (Just val')} ItIsJust}
141%language ErrorReflection
143||| Attempt to convert a reflected (fromInteger n) to a Nat
144total private
145getNat' : TT -> Maybe TT
146getNat' `(fromInteger ~(TConst (BI c)) : Nat) = Just $ quote (the Nat (fromInteger c))
147getNat' _ = Nothing
149||| Attempt to convert a reflected (fromInteger n) to a Nat. Return
150||| the original term on failure.
151total private
152getNat : TT -> TT
153getNat tm = maybe tm id $ getNat' tm
155total private
156mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
157mkFinIntegerErr lit finSize subErr
158 = Just [ TextPart "When using", TermPart lit
159 , TextPart "as a literal for a"
160 , TermPart `(Fin ~(getNat finSize))
161 , SubReport subErr
162 ]
163total export
164finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
165finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
166 = mkFinIntegerErr (TConst c) m
167 [ TermPart (TConst c)
168 , TextPart "is not strictly less than"
169 , TermPart (getNat m)
170 ]
171finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
172 = mkFinIntegerErr (P Bound n t) m
173 [ TextPart "Could not show that", TermPart (P Bound n t)
174 , TextPart "is less than", TermPart (getNat m)
175 , TextPart "because", TermPart (P Bound n t)
176 , TextPart "is a bound variable instead of a constant"
177 , TermPart `(Integer : Type)
178 ]
179finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
180 = mkFinIntegerErr n m
181 [ TextPart "Could not show that" , TermPart n
182 , TextPart "is less than" , TermPart (getNat m)
183 ]
184finFromIntegerErrors _ = Nothing
186%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
188implementation Enum (Fin (S n)) where
189 pred FZ = FZ
190 pred (FS n) = weaken n
191 succ n = case strengthen (FS n) of
192 Left _ => last
193 Right k => k
194 toNat n = cast n
195 fromNat {n=n} m = case natToFin m (S n) of
196 Just k => k
197 Nothing => last
199--------------------------------------------------------------------------------
200-- DecEq
201--------------------------------------------------------------------------------
203total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
204FZNotFS Refl impossible
206implementation DecEq (Fin n) where
207 decEq FZ FZ = Yes Refl
208 decEq FZ (FS f) = No FZNotFS
209 decEq (FS f) FZ = No $ negEqSym FZNotFS
210 decEq (FS f) (FS f') with (decEq f f')
211 | Yes p = Yes $ cong p
212 | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h