module Sorted where data Nat : Set where ze : Nat su : Nat -> Nat data Zero : Set where record One : Set where _<=_ : Nat -> Nat -> Set ze <= _ = One su _ <= ze = Zero su x <= su y = x <= y data OWOTO {X : Set}(R : X -> X -> Set)(x y : X) : Set where lr : R x y -> OWOTO R x y rl : R y x -> OWOTO R x y owotoNat : (x y : Nat) -> OWOTO _<=_ x y owotoNat ze y = lr _ owotoNat (su x) ze = rl _ owotoNat (su x) (su y) with owotoNat x y ... | lr p = lr{x = su x}{y = su y} p ... | rl p = rl{x = su x}{y = su y} p data ToB (X : Set) : Set where top : ToB X el : X -> ToB X bot : ToB X TBLE : {X : Set} -> (X -> X -> Set) -> ToB X -> ToB X -> Set TBLE _ _ top = One TBLE _ bot _ = One TBLE R (el x) (el y) = R x y TBLE _ _ _ = Zero owotoTB : {X : Set}{R : X -> X -> Set} -> ((x y : X) -> OWOTO R x y) -> (x y : ToB X) -> OWOTO (TBLE R) x y owotoTB ow x top = lr _ owotoTB ow top (el y) = rl _ owotoTB ow (el y) (el y') with ow y y' ... | lr p = lr p ... | rl p = rl p owotoTB ow bot (el y) = lr _ owotoTB ow top bot = rl _ owotoTB ow (el y) bot = rl _ owotoTB ow bot bot = rl _ data List (X : Set) : Set where nil : List X cons : X -> List X -> List X data OList {X : Set}(R : X -> X -> Set)(l u : ToB X) : Set where onil : TBLE R l u -> OList R l u ocons : (x : X) -> TBLE R l (el x) -> OList R (el x) u -> OList R l u insert : {l u : ToB Nat} (x : Nat) -> {_ : TBLE _<=_ l (el x)}{_ : TBLE _<=_ (el x) u} -> OList _<=_ l u -> OList _<=_ l u insert x {lx}{xu} (onil lu) = ocons x lx (onil xu) insert x {lx}{xu} (ocons y ly ys) with owotoNat x y ... | lr xy = ocons x lx (ocons y xy ys) ... | rl yx = ocons y ly (insert x {yx} {xu} ys) isort : List Nat -> OList _<=_ bot top isort nil = onil _ isort (cons x xs) = insert x (isort xs) data OTree {X : Set}(R : X -> X -> Set)(l u : ToB X) : Set where oleaf : TBLE R l u -> OTree R l u onode : (x : X) -> OTree R l (el x) -> OTree R (el x) u -> OTree R l u inTree : {l u : ToB Nat} (x : Nat) -> {_ : TBLE _<=_ l (el x)}{_ : TBLE _<=_ (el x) u} -> OTree _<=_ l u -> OTree _<=_ l u inTree x {lx}{xu} (oleaf lu) = onode x (oleaf lx) (oleaf xu) inTree x {lx}{xu} (onode y lo hi) with owotoNat x y ... | lr xy = onode y (inTree x {lx}{xy} lo) hi ... | rl yx = onode y lo (inTree x {yx}{xu} hi) mkTree : List Nat -> OTree _<=_ bot top mkTree nil = oleaf _ mkTree (cons x xs) = inTree x (mkTree xs) flatNode : forall {X : Set}{R : X -> X -> Set}{l u : ToB X} (x : X) -> OList R l (el x) -> OList R (el x) u -> OList R l u flatNode x (onil lx) xs = ocons x lx xs flatNode x (ocons y ly ys) zs = ocons y ly (flatNode x ys zs) flatTree : forall {l u} -> OTree _<=_ l u -> OList _<=_ l u flatTree (oleaf lu) = onil lu flatTree (onode x lo hi) = flatNode x (flatTree lo) (flatTree hi) {- merge : forall {l u} -> OList _<=_ l u -> OList _<=_ l u -> OList _<=_ l u merge (onil _) ys = ys merge xs (onil _) = xs merge (ocons x lx xs) (ocons y ly ys) with owotoNat x y ... | lr xy = ocons x lx (merge xs (ocons y xy ys)) ... | rl yx = ocons y ly (merge (ocons x yx xs) ys) -} mutual merge : forall {l u} -> OList _<=_ l u -> OList _<=_ l u -> OList _<=_ l u merge (onil _) ys = ys merge (ocons x lx xs) ys = mergeHelp x lx xs ys mergeHelp : forall {l u} -> (x : Nat)(lx : TBLE _<=_ l (el x)) -> OList _<=_ (el x) u -> OList _<=_ l u -> OList _<=_ l u mergeHelp x lx xs (onil lu) = ocons x lx xs mergeHelp x lx xs (ocons y ly ys) with owotoNat x y ... | lr xy = ocons x lx (merge xs (ocons y xy ys)) ... | rl yx = ocons y ly (mergeHelp x yx xs ys) data Tree (X : Set) : Set where none : Tree X leaf : X -> Tree X node : Tree X -> Tree X -> Tree X twistin : forall {X} -> X -> Tree X -> Tree X twistin x none = leaf x twistin x (leaf y) = node (leaf x) (leaf y) twistin x (node l r) = node (twistin x r) l dealTree : forall {X} -> List X -> Tree X dealTree nil = none dealTree (cons x xs) = twistin x (dealTree xs) mergeTree : Tree Nat -> OList _<=_ bot top mergeTree none = onil _ mergeTree (leaf x) = ocons x _ (onil _) mergeTree (node l r) = merge (mergeTree l) (mergeTree r) msort : List Nat -> OList _<=_ bot top msort xs = mergeTree (dealTree xs)