module Rot1 where -- Depends on my customized Agda prelude -- http://bitbucket.org/robsimmons/agda-lib/src/518998444312 open import Prelude renaming (_≡_ to _==_ ; _≡≡_ to _===_ ; ∃ to exists ; _×_ to _&&_) -- ******************************** -- -- Part 1: Trees and tree rotations -- -- ******************************** -- data Tree (A : Set) : Set where Nil : Tree A Node : Tree A -> A -> Tree A -> Tree A -- (t1 ++> t2) appends t2 to the rightmost leaf of t1 _++>_ : {A : Set} -> Tree A -> Tree A -> Tree A Nil ++> t = t (Node t1 x t2) ++> t = Node t1 x (t2 ++> t) -- ****************************************************** -- -- Part 2: Setting up an induction metric "TM t" on terms -- -- ****************************************************** -- data TM {A : Set} : Tree A -> Set where Done : TM Nil Recurse : {x : A}{t : Tree A} -> TM t -> TM (Node Nil x t) Rotate : {x y : A}{t1 t2 t3 : Tree A} -> TM (Node t1 x (Node t2 y t3)) -> TM (Node (Node t1 x t2) y t3) metric : {A : Set} (t : Tree A) -> TM t metric Nil = Done metric (Node t1 x t2) = helper t1 (metric t2) where append : {A : Set}{t1 t2 : Tree A} -> TM t1 -> TM t2 -> TM (t1 ++> t2) append Done t2 = t2 append (Recurse t1) t2 = Recurse (append t1 t2) append (Rotate t1) t2 = Rotate (append t1 t2) helper : {A : Set} {x : A}{t2 : Tree A} (t1 : Tree A) -> TM t2 -> TM (Node t1 x t2) helper Nil tt = Recurse tt helper (Node t1 x t2) tt = Rotate (helper t1 (append (helper t2 Done) tt)) -- ************************************* -- -- Part 3 - Putting trees in normal form -- -- ************************************* -- norm : {A : Set} -> Tree A -> Tree A norm t = helper t (metric t) where helper : {A : Set} -> (t : Tree A) -> TM t -> Tree A helper Nil Done = Nil helper (Node Nil x t) (Recurse tm) = Node Nil x (helper t tm) helper (Node (Node t1 x t2) y t3) (Rotate tm) = helper (Node t1 x (Node t2 y t3)) tm