Linear.idr 659 Bytes
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
import Data.Fin
import Data.Vect

Nicola Botta's avatar
Nicola Botta committed
4
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
Nicola Botta's avatar
Nicola Botta committed
5
6
tail f = f . FS

Nicola Botta's avatar
Nicola Botta committed
7
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
Nicola Botta's avatar
Nicola Botta committed
8
9
10
11
toVectFun {n =   Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))

N : Nat
Nicola Botta's avatar
Nicola Botta committed
12
N = 800
Nicola Botta's avatar
Nicola Botta committed
13
14
15
16

xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat

Nicola Botta's avatar
Nicola Botta committed
17
18
19
20
fromNat : {n : Nat} -> Nat -> Fin n
fromNat {n = S m}  Z    = FZ
fromNat {n = S m} (S i) = if i < m then FS (fromNat i) else last 

Nicola Botta's avatar
Nicola Botta committed
21
22
main : IO ()
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
Nicola Botta's avatar
Nicola Botta committed
23
-- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))