Linear.lidr 689 Bytes
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
> import Data.Fin
> import Data.Vect

> tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
> tail f = f . FS

> toVectFun : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
> 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 (toIntegerNat N)) xs))
Nicola Botta's avatar
Nicola Botta committed
23
> -- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))