module FromInteger

import Data.Vect

-- This is inspired by the fromInteger definition for Fin.

IntegerToElem :
  DecEq a => (i : Integer) -> (x : a) -> (xs : Vect n a)
    -> Maybe (Elem x xs)
IntegerToElem i x []        = Nothing
IntegerToElem i x (y :: xs) with (decEq x y)
  IntegerToElem i x (x :: xs) | (Yes Refl)  =
    if i == 0
      then Just Here
      else if i < 0
        then Nothing
        else map There (IntegerToElem (i - 1) x xs)
  IntegerToElem i x (y :: xs) | (No contra) =
    if i <= 0
      then Nothing
      else map There (IntegerToElem (i - 1) x xs)

fromInteger :
  DecEq a => {x : a} -> {xs : Vect n a} -> (i : Integer)
    -> {default ItIsJust prf : IsJust (IntegerToElem i x xs)} -> Elem x xs
fromInteger {x} {xs} i {prf} with (IntegerToElem i x xs)
  fromInteger {x = x} {xs = xs} i {prf = ItIsJust} | Nothing impossible
  fromInteger {x = x} {xs = xs} i {prf = ItIsJust} | (Just y) = y

-- All of these work:

t1 : Elem True [True]
t1 = 0

t2 : Elem True [False, False, True]
t2 = 2

t3 : Elem True [True, True]
t3 = 1

t4 : Elem () [(), ()]
t4 = 0

t5 : Elem () [(), ()]
t5 = 1

t6 : Elem (the (Fin 8) 0) (the (Vect 8 (Fin 8)) Data.Vect.range)
t6 = 0

t7 : Elem (the (Fin 8) 7) (the (Vect 8 (Fin 8)) Data.Vect.range)
t7 = 7

t8 : Elem (the Nat 0) (the (Vect 3 Nat) [0,1,2])
t8 = 0

-- None of these work, but I don't know why ... :

{-
f1 : Elem (the Integer 0) (the (Vect 3 Integer) [0,1,2])
f1 = 0

f2 : Elem 'x' ['x']
f2 = 0
-}