FromInteger.idr

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
-}

This is the error message for f1:

 `-- FromInteger.idr line 66 col 0:
     When checking right hand side of f1:
     When checking argument prf to function FromInteger.fromInteger:
             Type mismatch between
                     IsJust (Just x) (Type of ItIsJust)
             and
                     IsJust (IntegerToElem 0 0 [0, 1, 2]) (Expected type)

             Specifically:
                     Type mismatch between
                             Just x
                     and
                             with block in FromInteger.IntegerToElem 0
                                                                     Integer
                                                                     0
                                                                     0
                                                                     (decEq 0 0)
                                                                     2
                                                                     [1, 2]
                                                                     Integer instance of Decidable.Equality.DecEq