lhs.hs

module LHbasics where

-- sorted lists

data List a = Emp
            | (:::) a (List a)

data IncList a = IncEmp
               | (:<) { hd :: a, tl :: IncList a }

{-@ data IncList a = IncEmp
                   | (:<) { hd :: a, tl :: IncList {v:a | hd <= v} } @-}


insert :: (Ord a) => a -> IncList a -> IncList a
insert x IncEmp  = x :< IncEmp
insert x (y :< ys)
  | x <= y    = x :< (y :< ys)
  | otherwise = y :< insert x ys

insertSort :: (Ord a) => [a] -> IncList a
insertSort [] = IncEmp
insertSort (x:xs) = insert x (insertSort xs)

merge :: (Ord a) => IncList a -> IncList a -> IncList a
merge xs IncEmp = xs
merge IncEmp ys = ys
merge (x :< xs) (y :< ys)
  | x <= y     = x :< merge xs (y :< ys)
  | otherwise  = y :< merge (x :< xs) ys

mergeSort :: (Ord a) => [a] -> IncList a
mergeSort []   = IncEmp
mergeSort [x]  = x :< IncEmp
mergeSort xs   = merge (mergeSort ys) (mergeSort zs)
  where (ys, zs) = splitAt (length xs `div` 2) xs

{-@ join :: x:a -> IncList ({v:a | v <= x}) -> IncList ({v:a | x <= v}) -> IncList a @-}
join :: a -> IncList a -> IncList a -> IncList a
join z IncEmp ys = z :< ys
join z (x :< xs) ys = x :< join z xs ys

quickSort :: (Ord a) => [a] -> IncList a
quickSort [] = IncEmp
quickSort (x:xs) = join x lessers greaters
  where lessers  = quickSort [y | y <- xs, y < x]
        greaters = quickSort [z | z <- xs, z >= x]

-- search trees

{-@ inline max @-}
max :: Int -> Int -> Int
max y x = if x > y then x else y

data BST a = BLeaf
           | BNode { root  :: a
                  , left  :: BST a
                  , right :: BST a
                  }

{-@ data BST a = BLeaf
               | BNode { root  :: a
                      , left  :: BST { v:a | v < root }
                      , right :: BST { v:a | root < v}
                      } @-}

{-@ measure height @-}
{-@ height :: BST a -> Nat @-}
height :: BST a -> Int
height BLeaf = 0
height (BNode _ l r) = 1 + LHbasics.max (height l) (height r)

data AVL a = Leaf
           | Node { key :: a
                  , l   :: AVL a
                  , r   :: AVL a
                  , ah  :: Int
                  }
            deriving Show

{-@ type AVLL a X = AVL {v:a | v < X} @-}
{-@ type AVLR a X = AVL {v:a | X < v} @-}

{-@ measure realHeight @-}
realHeight                :: AVL a -> Int
realHeight Leaf           = 0
realHeight (Node _ l r _) = nodeHeight l r

{-@ inline nodeHeight @-}
nodeHeight l r = 1 + LHbasics.max hl hr
  where
    hl         = realHeight l
    hr         = realHeight r

{-@ inline isReal @-}
isReal v l r = v == nodeHeight l r

{-@ inline isBal @-}
isBal l r n = 0 - n <= d && d <= n
  where
    d       = realHeight l - realHeight r

{-@ data AVL a = Leaf
               | Node { key :: a
                      , l   :: AVLL a key
                      , r   :: {v:AVLR a key | isBal l v 1}
                      , ah  :: {v:Nat        | isReal v l r}
                      } @-}

-- | Trees of height N
{-@ type AVLN a N = {v: AVL a | realHeight v = N} @-}

-- | Trees of height equal to that of another T
{-@ type AVLT a T = AVLN a {realHeight T} @-}

{-@ empty :: AVLN a 0 @-}
empty = Leaf

{-@ singleton :: a -> AVLN a 1 @-}
singleton x =  Node x empty empty 1

{-@ getHeight :: t:AVL a -> {v:Nat | v == realHeight t }@-}
getHeight (Leaf)= 0
getHeight (Node _ _ _ h) = h

{-@ mkNode :: x:a -> l:AVLL a x -> r: { v:AVLR a x | isBal l v 1}
           -> AVLN a {nodeHeight l r}
  @-}
mkNode x l r = Node x l r h
 where
   h       = 1 + LHbasics.max hl hr
   hl      = getHeight l
   hr      = getHeight r