module rbt_varif where

open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Binary
open import Data.Nat hiding (_@$\leq$@_  ; _@$\leq$@?_)
open import Data.List hiding ([_])
open import Data.Product
open import Data.Nat.Properties as NP



mutual
  data  right-List : Set where
    [] : right-List
    [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List
    _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List

  top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@
  top-r [] = {!!}
  top-r [ x ] = x
  top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x

  insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List
  insert-r x [] = {!!}
  insert-r x [ y ] with <-cmp x y
  ... | tri< a @$\neg$@b @$\neg$@c = [ y ]
  ... | tri≈ @$\neg$@a b @$\neg$@c = [ y ]
  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@>  [ y ] Cond c
  insert-r x (y @$\text{::}$@> ys Cond p) with <-cmp x y
  ... | tri< a @$\neg$@b @$\neg$@c = (y @$\text{::}$@> ys Cond p)
  ... | tri≈ @$\neg$@a b @$\neg$@c = (y @$\text{::}$@> ys Cond p)
  ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> (y @$\text{::}$@> ys Cond p) Cond c

  data  left-List : Set where
    [] : left-List
    [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List
    _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List

  top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@
  top-l [] = {!!}
  top-l [ x ] = x
  top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x

  insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List
  insert-l x [] = [ x ]
  insert-l x l@([ y ]) with <-cmp x y
  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
  ... | tri≈ @$\neg$@a b @$\neg$@c = l
  ... | tri> @$\neg$@a @$\neg$@b c = l
  insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y
  ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a
  ... | tri≈ @$\neg$@a b @$\neg$@c = l

  ... | tri> @$\neg$@a @$\neg$@b c = l