Idris2-boot/tests/idris2/total004/Total.idr

128 lines
3.0 KiB
Idris
Raw Normal View History

import Data.List
ack : Nat -> Nat -> Nat
ack 0 n = S n
ack (S k) 0 = ack k 1
ack (S j) (S k) = ack j (ack (S j) k)
foo : Nat -> Nat
foo Z = Z
foo (S Z) = (S Z)
foo (S (S k)) = foo (S k)
data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
ordElim : (x : Ord) ->
(p : Ord -> Type) ->
(p Zero) ->
((x : Ord) -> p x -> p (Suc x)) ->
((f : Nat -> Ord) -> ((n : Nat) -> p (f n)) ->
p (Sup f)) -> p x
ordElim Zero p mZ mSuc mSup = mZ
ordElim (Suc o) p mZ mSuc mSup = mSuc o (ordElim o p mZ mSuc mSup)
ordElim (Sup f) p mZ mSuc mSup =
mSup f (\n => ordElim (f n) p mZ mSuc mSup)
mutual
bar : Nat -> Lazy Nat -> Nat
bar x y = mp x y
mp : Nat -> Nat -> Nat
mp Z y = y
mp (S k) y = S (bar k y)
mutual
swapR : Nat -> Nat -> Nat
swapR x (S y) = swapL y x
swapR x Z = x
swapL : Nat -> Nat -> Nat
swapL (S x) y = swapR y (S x)
swapL Z y = y
loopy : a
loopy = loopy
data Bin = EPS | C0 Bin | C1 Bin
foom : Bin -> Nat
foom EPS = Z
foom (C0 EPS) = Z
foom (C0 (C1 x)) = S (foom (C1 x))
foom (C0 (C0 x)) = foom (C0 x)
foom (C1 x) = S (foom x)
pfoom : Bin -> Nat
pfoom EPS = Z
pfoom (C0 EPS) = Z
pfoom (C0 (C1 x)) = S (pfoom (C0 x))
pfoom (C0 (C0 x)) = pfoom (C0 x)
pfoom (C1 x) = S (foom x)
even : Nat -> Bool
even Z = True
even (S k) = odd k
where
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
vtrans : Vect n a -> Vect n a -> List a
vtrans [] _ = []
vtrans (x :: xs) ys = x :: vtrans ys ys
data GTree : Type -> Type where
MkGTree : List (GTree a) -> GTree a
size : GTree a -> Nat
size (MkGTree []) = Z
size (MkGTree xs) = sizeAll xs
where
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
sizeAll : List (GTree a) -> Nat
sizeAll [] = Z
sizeAll (x :: xs) = plus (size x) (sizeAll xs)
qsortBad : Ord a => List a -> List a
qsortBad [] = []
qsortBad (x :: xs)
= qsortBad (filter (< x) xs) ++ x :: qsortBad (filter (> x) xs)
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
x :: qsort (assert_smaller (x :: xs) (filter (> x) xs))
qsort' : Ord a => List a -> List a
qsort' [] = []
qsort' (x :: xs)
= let (xs_low, xs_high) = partition x xs in
qsort' (assert_smaller (x :: xs) xs_low) ++
x :: qsort' (assert_smaller (x :: xs) xs_high)
where
partition : a -> List a -> (List a, List a)
partition x xs = (filter (< x) xs, filter (>= x) xs)
sorted : Ord a => List a -> Bool
sorted [] = True
sorted (x::xs) =
case xs of
Nil => True
(y::ys) => x <= y && sorted (y::ys)
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order [] right = right
mergeBy order left [] = left
mergeBy order (x::xs) (y::ys) =
case order x y of
LT => x :: mergeBy order xs (y::ys)
_ => y :: mergeBy order (x::xs) ys