terminating sort in agda

sort.agda

data Uni : Set where
  U : Uni

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  []   : ∀{n} → Vec A n
  _::_ : ∀{n} → A → Vec A n → Vec A (S n)

Nat : ∀ s → Set
Nat s = Vec Uni s

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

-- Equality
-- --------

subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

cong : ∀ {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

-- ℕ
-- -

add : ℕ → ℕ → ℕ
add Z     m = m
add (S n) m = S (add n m)

+zero : ∀ {m} → add m Z ≡ m
+zero {Z}    = refl
+zero {S m}  = cong S +zero

+succ : ∀ {m n} → add m (S n) ≡ S (add m n)
+succ {Z}    = refl
+succ {S m}  = cong S +succ

-- Vector
-- ------

map : ∀{A B n} → (A → B) → Vec A n → Vec B n
map f []        = []
map f (x :: xs) = f x :: map f xs

-- The last argument is an accumulator (initially empty)
sort : ∀ {s n m} → Vec (Nat (S s)) n → Vec (Nat s) m → Vec (Nat (S s)) (add n m)
sort {Z}     {Z}     {m} []               ys = map (λ x → U :: x) ys
sort {Z}     {(S n)} {m} ([] :: xs)       ys = [] :: sort {Z} {n} {m} xs ys
sort {Z}     {(S n)} {m} ((u :: x) :: xs) ys = subst (λ x → Vec _ x) (+succ) (sort {Z} {n} {(S m)} xs (x :: ys))
sort {(S s)} {Z}     {m} []               ys = subst (λ x → Vec _ x) (+zero) (map (λ x → U :: x) (sort {s} {m} {Z} ys []))
sort {(S s)} {(S n)} {m} ([] :: xs)       ys = [] :: sort {(S s)} {n} {m} xs ys
sort {(S s)} {(S n)} {m} ((u :: x) :: xs) ys = subst (λ x → Vec _ x) (+succ) (sort {(S s)} {n} {(S m)} xs (x :: ys))
sort {s}     {n}     {m} xs               ys = []

-- Representation of numbers as vectors
n0 : ∀{n} → Nat n
n0 = []

n1 : ∀{n} → Nat (S n)
n1 = U :: []

n2 : ∀{n} → Nat (S (S n))
n2 = U :: (U :: [])

n3 : ∀{n} → Nat (S (S (S n)))
n3 = U :: (U :: (U :: []))

n4 : ∀{n} → Nat (S (S (S (S n))))
n4 = U :: (U :: (U :: (U :: [])))

vec : Vec (Nat (S (S (S Z)))) (S (S (S Z)))
vec = n3 :: (n1 :: (n2 :: []))

-- Example: sorting [3,1,2]
main : Vec (Nat (S (S (S Z)))) (S (S (S Z)))
main = sort {(S (S Z))} {(S (S (S Z)))} {Z} vec []