content: module Trees where
  
  {-@ LIQUID "--no-termination" @-}
  
  import Language.Haskell.Liquid.Prelude
  
  data Tree a = Leaf a | Node [Tree a] 
  
  {-@ data Tree a = Leaf (xx :: a) | Node (yy :: {mickeymouse : [{v:Tree a | size v < sizes mickeymouse}] | true}) @-}
  
  {-@ measure size  @-}
  {-@ measure sizes  @-}
  
  {-@ invariant {v: [Tree a] | sizes v >= 0  } @-}
  {-@ invariant {v: Tree a | size v >= 0  } @-}
  
  {-@ size           :: t:Tree a -> {v:Nat | v = size t} / [size t, 0] @-}
  size :: Tree a -> Int
  size (Leaf _)  = 1
  size (Node xs) = 1 + sizes xs
  
  {-@ sizes         :: xs:[Tree a] -> {v:Nat | v = sizes xs} / [sizes xs, len xs] @-}
  sizes :: [Tree a ] -> Int
  sizes []      = 0
  sizes (t:ts)  = size t + sizes ts
  
  {-@ test1 :: tt:Tree a -> Tree a / [size tt] @-}
  test1 tt = case tt of
               Leaf x  -> Leaf x
               Node ts -> liquidAssert (sizes ts < size tt) $ Node (goo tt ts)
  
  {-@ goo :: tt:Tree a -> [{v: Tree a | size v < size tt}] -> [Tree a] @-}
  goo :: Tree a -> [Tree a] -> [Tree a]
  goo _ []      = []
  goo tt (t:ts) = t : goo tt ts
  
  {-@ test2 :: tt:Tree a -> Tree a / [size tt] @-}
  test2 tt = case tt of
               Leaf x  -> Leaf x
               Node ts -> liquidAssert (sizes ts < size tt) $ Node (moo ts ts)
  
  {-@ moo :: ts:[Tree a] -> [{v: Tree a | size v < sizes ts}] -> [Tree a] @-}
  moo :: [Tree a] -> [Tree a] -> [Tree a]
  moo _  []      = []
  moo ts (t:ts') = t : moo ts ts'
  
  
  
  {-@ qualif SZ(v:a, x:b): size v < size x @-}
  
  foo tt = case tt of
             Leaf x  -> () 
             Node ts -> liquidAssert (1 + sizes ts == size tt) ()
  
  