README

## prerequisits

idris v0.99

## build && run

idris ./avl.idr -o avl && ./avl

## usage

REPL is also provided. 
Its command described below with format <command> : <description>

1. <number> : add number to avl tree
2. p : print avl-tree
3. e : exit

Avl.idr

{--
 - Copyright 2017 Pavel Begunkov.
 -
 - Permission is hereby granted, free of charge, to any person obtaining a
 - copy of this software and associated documentation files (the "Software"),
 - to deal in the Software without restriction, including without limitation
 - the rights to use, copy, modify, merge, publish, distribute, sublicense,
 - and/or sell copies of the Software, and to permit persons to whom the
 - Software is furnished to do so, subject to the following conditions:
 -
 - The above copyright notice and this permission notice shall be included in
 - all copies or substantial portions of the Software.
 - 
 - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 - IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 - FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL
 - THE COPYRIGHT HOLDER(S) OR AUTHOR(S) BE LIABLE FOR ANY CLAIM, DAMAGES OR
 - OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 - ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
 - OTHER DEALINGS IN THE SOFTWARE.
--}
module Main

data AVL : Nat -> Type -> Type where
    Nil : AVL 0 a
    NodeE : (x : a) -> {n : Nat} -> AVL n a -> AVL n a -> AVL (1+n) a
    NodeL : (x : a) -> {n : Nat} -> AVL (S n) a -> AVL n a -> AVL (2+n) a
    NodeR : (x : a) -> {n : Nat} -> AVL n a -> AVL (S n) a -> AVL (2+n) a
    
data Inv : Nat -> Type -> Type where
    DInv : {n : Nat} -> AVL n a -> Inv n a
    SInv : {n : Nat} -> AVL (1+n) a -> Inv n a
    
rotate : {n : Nat} -> AVL n a -> AVL n a
rotate Nil = Nil
rotate (NodeE x l r) = NodeE x r l
rotate (NodeL x l r) = NodeR x r l
rotate (NodeR x l r) = NodeL x r l

rotate' : {n : Nat} -> Inv n a -> Inv n a
rotate' (SInv t) = SInv $ rotate t
rotate' (DInv t) = DInv $ rotate t

uniteE : {n : Nat} -> (x : a) -> Inv n a -> AVL n a -> Inv (S n) a
uniteE x (DInv l) r = DInv $ NodeE x l r
uniteE x (SInv l) r = SInv $ NodeL x l r

uniteS : {n : Nat} -> (x : a) -> Inv n a -> AVL (S n) a -> AVL (2+n) a
uniteS x (DInv l) r = NodeR x l r
uniteS x (SInv l) r = NodeE x l r

rotateLeft : {n : Nat} -> (x : a) -> AVL (2+n) a -> AVL n a -> Inv (2+n) a
rotateLeft x (NodeL y alpha beta) gamma = DInv $ NodeE y alpha (NodeE x beta gamma)
rotateLeft x (NodeE y alpha beta) gamma = SInv $ NodeR y alpha (NodeL x beta gamma)
rotateLeft x (NodeR y alpha (NodeL z beta gamma)) delta = 
    DInv $ NodeE z (NodeE y alpha beta) (NodeR x gamma delta)
rotateLeft x (NodeR y alpha (NodeR z beta gamma)) delta = 
    DInv $ NodeE z (NodeL y alpha beta) (NodeE x gamma delta)
rotateLeft x (NodeR y alpha (NodeE z beta gamma)) delta = 
    DInv $ NodeE z (NodeE y alpha beta) (NodeE x gamma delta)

rotateRight : {n : Nat} -> (x : a) -> AVL n a -> AVL (2+n) a -> Inv (2+n) a
rotateRight x gamma (NodeR y beta alpha) = DInv $ NodeE y (NodeE x gamma beta) alpha
rotateRight x gamma (NodeE y beta alpha) = SInv $ NodeL y (NodeR x gamma beta) alpha 
rotateRight x delta (NodeL y (NodeR z gamma beta) alpha) = 
    DInv $ NodeE z (NodeL x delta gamma) (NodeE y beta alpha)
rotateRight x delta (NodeL y (NodeL z gamma beta) alpha) = 
    DInv $ NodeE z (NodeE x delta gamma) (NodeR y beta alpha)
rotateRight x delta (NodeL y (NodeE z gamma beta) alpha) = 
    DInv $ NodeE z (NodeE x delta gamma) (NodeE y beta alpha)


uniteLeft : {n : Nat} -> (x : a) -> Inv (S n) a -> AVL n a -> Inv (2+n) a
uniteLeft root (DInv l) r = DInv $ NodeL root l r
uniteLeft root (SInv l) r = rotateLeft root l r

uniteRight : {n : Nat} -> (x : a) -> AVL n a -> Inv (S n) a -> Inv (2+n) a
uniteRight root l (DInv r) = DInv $ NodeR root l r
uniteRight root l (SInv r) = rotateRight root l r

add : Ord a => {n : Nat} -> (x : a) -> AVL n a -> Inv n a
add x Nil = SInv $ NodeE x Nil Nil
add x (NodeE root l r) = 
    let prop = x < root
        (l', r') = if prop then (l, r) else (r, l)
    in (if prop then id else rotate') $ uniteE root (add x l') r'

add x (NodeR root l r) = 
    if x < root 
    then DInv $ uniteS root (add x l) r
    else uniteRight root l (add x r)

add x (NodeL root l r) = 
    if x < root 
    then uniteLeft root (add x l) r
    else DInv $ rotate $ uniteS root (add x r) l 

-- ---------------------
-- Repl 

generateIndent : Nat -> List Char
generateIndent indent = replicate indent ' '


mutual
    stringifyHelper' : Show a => Nat -> (x : a) -> AVL n a -> AVL m a -> List Char
    stringifyHelper' indent x l r = 
        let ni = indent + 6
            ls = stringifyHelper ni l
            rs = stringifyHelper ni r
            vs = generateIndent indent ++ unpack (show x) ++ ['\n']
        in rs ++ vs ++ ls

    stringifyHelper : Show a => Nat -> AVL n a -> List Char
    stringifyHelper indent Nil = generateIndent indent ++ unpack "Nil\n"
    stringifyHelper indent (NodeE x l r) = stringifyHelper' indent x l r
    stringifyHelper indent (NodeL x l r) = stringifyHelper' indent x l r
    stringifyHelper indent (NodeR x l r) = stringifyHelper' indent x l r

stringify : Show a => AVL n a -> String
stringify tree = pack $ stringifyHelper 0 tree

data Tree a = MkTree (AVL n a)

mkTreeFromInv : Inv n a -> Tree a
mkTreeFromInv (DInv t) = MkTree t
mkTreeFromInv (SInv t) = MkTree t

parseNum : String -> Maybe Integer
parseNum s =  case all isDigit (unpack s) of
              False => Nothing
              True => Just (cast s)

foo : Tree Integer -> String -> Maybe (String, Tree Integer)
foo (MkTree tree) "p" = Just (stringify tree, MkTree tree)
foo _ "e" = Nothing
foo (MkTree tree) s = case parseNum s of
    Nothing => Just ("wrong number format\n", MkTree tree)
    Just num => Just ("", mkTreeFromInv $ add num tree) 

main : IO ()
main = replWith (MkTree Nil) ">>" foo