### Bounded Nat complexity tests.

parent 7221c669
 module BoundedNat.BoundedNat import Data.Nat import Sigma.Sigma ||| Natural numbers bounded by LT public export LTB : Nat -> Type LTB b = Sigma Nat (\ n => LT n b) ||| Natural numbers bounded by LTE public export LTEB : Nat -> Type LTEB b = Sigma Nat (\ n => LTE n b) ||| public export implementation Uninhabited (LTB Z) where uninhabited (MkSigma n prf) = absurd prf
 module BoundedNat.Operations import Data.Nat import Data.Vect import Sigma.Sigma import BoundedNat.BoundedNat ||| idx : {n : Nat} -> Vect n alpha -> LTB n -> alpha idx {n = Z} Nil (MkSigma i prf) = absurd prf idx {n = S m} (x :: xs) (MkSigma Z prf) = x idx {n = S m} (x :: xs) (MkSigma (S k) (LTESucc prf)) = idx xs (MkSigma k prf)
 import Data.Fin import Data.Vect import Data.Nat LTB : Nat -> Type LTB b = DPair Nat (\ n => LT n b) idx : {n : Nat} -> Vect n alpha -> LTB n -> alpha idx {n = Z} Nil (MkDPair i prf) = absurd prf idx {n = S m} (x :: xs) (MkDPair Z prf) = x idx {n = S m} (x :: xs) (MkDPair (S k) (LTESucc prf)) = idx xs (MkDPair k prf) tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A) tail f = f . FS toVectFun : {0 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 N = 8 xs : Vect (S N) Nat xs = toVectFun {n = S N} finToNat lemma : (n : Nat) -> LT n (S n) lemma Z = LTESucc LTEZero lemma (S m) = LTESucc (lemma m) main : IO () -- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs)) main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (idx xs (MkDPair N (lemma N))))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment