gistfile1.txt

module MergeSort where

open import Function
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

data Order : Set where
  le : Order
  ge : Order

data List (X : Set) : Set where
  nil : List X
  _∷_ : (x : X) -> (xs : List X) -> List X

order : (x : ℕ) (y : ℕ) -> Order
order zero y = le
order (suc n) zero = ge
order (suc n) (suc n') = order n n'

merge : List ℕ -> List ℕ -> List ℕ
merge nil ys = ys
merge xs nil = xs
merge (x ∷ xs') (y ∷ ys') with order x y | merge xs' (y ∷ ys') | merge (x ∷ xs') ys'
merge (x ∷ xs') (y ∷ ys') | le | m1 | m2 = x ∷ m1
merge (x ∷ xs') (y ∷ ys') | ge | m1 | m2 = y ∷ m2

deal : {X : Set} (xs : List X) -> List X × List X
deal nil = nil , nil
deal (y ∷ nil) = y ∷ nil , nil
deal (y ∷ (y' ∷ y0)) with deal y0
deal (y' ∷ (y1 ∷ y0)) | proj₁ , y = y' ∷ proj₁ , y1 ∷ y

data Parity : Set where
  p₀ : Parity
  p₁ : Parity

data DealT (X : Set) : Set where
  empT : DealT X
  leafT : (x : X) -> DealT X
  nodeT : (p : Parity) -> (l : DealT X) -> (r : DealT X) -> DealT X

insertT : {X : Set} (x : X) -> (t : DealT X) -> DealT X
insertT x empT = leafT x
insertT x (leafT x') = nodeT p₀ (leafT x') (leafT x)
insertT x (nodeT p₀ l r) = nodeT p₁ (insertT x l) r
insertT x (nodeT p₁ l r) = nodeT p₀ l (insertT x r)

dealT : {X : Set} (xs : List X) -> DealT X
dealT nil = empT
dealT (x ∷ xs) = insertT x (dealT xs)

mergeT : DealT ℕ -> List ℕ
mergeT empT = nil
mergeT (leafT x) = x ∷ nil
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)

sort : List ℕ -> List ℕ
sort = mergeT ∘ dealT

data Vec (X : Set) : ℕ -> Set where
  vnil : Vec X 0
  vcons : ∀ {n : ℕ} -> (x : X) -> (v : Vec X n) -> Vec X (suc n)

vtail : {n : ℕ} {X : Set} -> (Vec X (suc n)) -> Vec X n
vtail (vcons x v) = v

infixl 5 _<+>_

_<+>_ : {S T : Set} {n : ℕ} -> Vec (S -> T) n -> Vec S n -> Vec T n
vnil <+> vnil = vnil
vcons f fv <+> vcons x xs = vcons (f x) (fv <+> xs)

infixl 5 _++_

_++_ : {n m : ℕ} {X : Set} -> Vec X n -> Vec X m -> Vec X (n + m)
vnil ++ ys = ys
vcons x v ++ ys = vcons x (v ++ ys)

vec : {X : Set} {n : ℕ} (x : X) -> Vec X n
vec {_} {0} x = vnil
vec {_} {suc n} x = vcons x (vec x)

xpose : {i j : ℕ} {X : Set} -> Vec (Vec X j) i -> Vec (Vec X i) j
xpose vnil = vec vnil
xpose (vcons x v) = vec vcons <+> x <+> xpose v

plusSuc : (k : ℕ) -> (n : ℕ) -> k + (suc n) ≡ suc (k + n)
plusSuc zero n = refl
plusSuc (suc n) n' with (plusSuc n n')
... | p = cong suc p

vrevacc : {X : Set}{n m : ℕ} -> Vec X n -> Vec X m -> Vec X (n + m)
vrevacc vnil ys = ys
vrevacc {X} {suc k} {m} (vcons x v) ys with (plusSuc k m)
... | p = vrevacc {!!} (vcons x ys)