0 | ||| Indexing Vectors.
 1 | |||
 2 | ||| `Elem` proofs give existential quantification that a given element
 3 | ||| *is* in the list, but not where in the list it is!  Here we give a
 4 | ||| predicate that presents proof that a given index of a vector,
 5 | ||| given by a `Fin` instance, will return a certain element.
 6 | |||
 7 | ||| Two decidable decision procedures are presented:
 8 | |||
 9 | ||| 1. Check that a given index points to the provided element in the
10 | |||    presented vector.
11 | |||
12 | ||| 2. Find the element at the given index in the presented vector.
13 | module Data.Vect.AtIndex
14 |
15 | import Data.Vect
16 | import Decidable.Equality
17 |
18 | %default total
19 |
20 | public export
21 | data AtIndex : (idx : Fin n)
22 |             -> (xs  : Vect n type)
23 |             -> (x   : type)
24 |                    -> Type
25 |   where
26 |     Here : AtIndex FZ (x::xs) x
27 |
28 |     There : (later : AtIndex     rest      xs  x)
29 |                   -> AtIndex (FS rest) (y::xs) x
30 |
31 | namespace Check
32 |   public export
33 |   elemDiffers : (y = x -> Void)
34 |               -> AtIndex FZ (y :: xs) x
35 |               -> Void
36 |   elemDiffers f Here
37 |     = f Refl
38 |
39 |   public export
40 |   elemNotInRest : (AtIndex z xs x -> Void)
41 |                ->  AtIndex (FS z) (y :: xs) x
42 |                ->  Void
43 |   elemNotInRest f (There later)
44 |     = f later
45 |
46 |   ||| Is the element at the given index?
47 |   |||
48 |   public export
49 |   index : DecEq type
50 |        => (idx : Fin n)
51 |        -> (x   : type)
52 |        -> (xs  : Vect n type)
53 |               -> Dec (AtIndex idx xs x)
54 |
55 |   index FZ _ [] impossible
56 |   index (FS y) _ [] impossible
57 |
58 |   index FZ x (y :: xs) with (decEq y x)
59 |     index FZ x (x :: xs) | (Yes Refl)
60 |       = Yes Here
61 |     index FZ x (y :: xs) | (No contra)
62 |       = No (elemDiffers contra)
63 |
64 |   index (FS z) x (y :: xs) with (Check.index z x xs)
65 |     index (FS z) x (y :: xs) | (Yes prf)
66 |       = Yes (There prf)
67 |     index (FS z) x (y :: xs) | (No contra)
68 |       = No (elemNotInRest contra)
69 |
70 | namespace Find
71 |   public export
72 |   elemNotInRest : (DPair type (AtIndex     x        xs)  -> Void)
73 |                ->  DPair type (AtIndex (FS x) (y :: xs)) -> Void
74 |
75 |   elemNotInRest f (MkDPair i (There later))
76 |     = f (MkDPair i later)
77 |
78 |   ||| What is the element at the given index?
79 |   |||
80 |   public export
81 |   index : DecEq type
82 |        => (idx : Fin n)
83 |        -> (xs  : Vect n type)
84 |               -> Dec (DPair type (AtIndex idx xs))
85 |   index FZ (x :: xs)
86 |     = Yes (MkDPair x Here)
87 |
88 |   index (FS x) (y :: xs) with (Find.index x xs)
89 |     index (FS x) (y :: xs) | (Yes (MkDPair i idx))
90 |       = Yes (MkDPair i (There idx))
91 |     index (FS x) (y :: xs) | (No contra) = No (elemNotInRest contra)
92 |
93 | -- [ EOF ]
94 |