{-# OPTIONS -fglasgow-exts #-}

-- Just a few functions for playing with StrictCheck

import Data.Generics
import StrictCheck


-- spine-strict variant of unzip
-- StrictCheck first finds same over-strictness as in standard unzip
unzip2 :: [(a, b)] -> ([a], [b])
unzip2 = foldr (\(x,y) (xs,ys) -> (x:xs,y:ys)) ([],[])


data MyNat = Zero | Succ MyNat deriving (Typeable,Data)

-- overly strict successor function
succ :: MyNat -> MyNat
succ x = go x Zero
  where
  go Zero x = x
  go (Succ x) y = go x (Succ y)


-- breadth-first numbering along Chris Okasaki, ICFP 2000

-- first the queue data type 

data Queue a = Q [a] [a]
  deriving (Show,Data,Typeable)

empty :: Queue a
empty = Q [] []

front :: Queue a -> Maybe (a,Queue a)
front (Q [] []) = Nothing
front (Q (x:xs) ys) = Just (x,Q xs ys)
front (Q [] ys) = Just (x,Q xs []) where x:xs = reverse ys

snoc :: Queue a -> a -> Queue a
snoc (Q xs ys) y = Q xs (y:ys)


data Tree a = E | T (Tree a) a (Tree a) 
  deriving (Show,Data,Typeable)

-- the actual breadth-first numbering function
bfNum :: Tree a -> Tree Int
bfNum t = t' 
  where
  Just (t',_) = front (bfNum' 1 (snoc empty t))

bfNum' :: Int -> Queue (Tree a) -> Queue (Tree Int)
bfNum' i q = case front q of
  Nothing -> empty
  Just (E,ts) -> bfNum' i ts `snoc` E
  Just (T l x r,ts) -> 
    let Just (r',ts'') = front (bfNum' (i+1) ((ts `snoc` l) `snoc` r))
        Just (l',ts') = front ts''
    in ts' `snoc` T l' i r'