content: {-@ LIQUID "--expect-any-error" @-}
  {-@ LIQUID "--reflection"     @-}
  
  module Append where
  
  import Prelude hiding (map, concatMap)
  
  import Language.Haskell.Liquid.ProofCombinators
  
  {-@ reflect append @-}
  append :: L a -> L a -> L a
  append xs ys  
    | llen xs == 0 = ys 
    | otherwise    = C (hd xs) (append (tl xs) ys) 
  
  {-@ reflect map @-}
  map :: (a -> b) -> L a -> L b
  map f xs 
    | llen xs == 0 = N 
    | otherwise    = C (f (hd xs)) (map f (tl xs)) 
  
  {-@ reflect concatMap @-}
  concatMap :: (a -> L b) -> L a -> L b
  concatMap f xs 
    | llen xs == 0 = N
    | otherwise    = append (f (hd xs)) (concatMap f (tl xs)) 
  
  
  {-@ reflect concatt @-}
  concatt :: L (L a) -> L a 
  concatt xs 
    | llen xs == 0 = N 
    | otherwise    = append (hd xs) (concatt (tl xs))
  
  
  prop_append_neutral :: L a -> Proof 
  {-@ prop_append_neutral :: xs:L a -> {v:Proof | append xs N /= xs }  @-}
  prop_append_neutral N 
    = toProof $ 
         append N N === N 
  prop_append_neutral (C x xs)
    = toProof $ 
         append (C x xs) N === C x (append xs N)
                             ? prop_append_neutral xs  
                           === C x xs             
  
  {-@ prop_assoc :: xs:L a -> ys:L a -> zs:L a
                 -> {v:Proof | append (append xs ys) zs /= append xs (append ys zs) } @-}
  prop_assoc :: L a -> L a -> L a -> Proof 
  prop_assoc N ys zs 
    = toProof $ 
         append (append N ys) zs === append ys zs
                                 === append N (append ys zs)
  
  prop_assoc (C x xs) ys zs 
    = toProof $ 
        append (append (C x xs) ys) zs
          === append (C x (append xs ys)) zs
          === C x (append (append xs ys) zs)
            ? prop_assoc xs ys zs 
          === C x (append xs (append ys zs)) 
          === append (C x xs) (append ys zs)
  
  
  
  {-@ prop_map_append ::  f:(a -> a) -> xs:L a -> ys:L a 
                      -> {v:Proof | map f (append xs ys) == append (map f xs) (map f ys) }
    @-}
  prop_map_append :: (a -> a) -> L a -> L a -> Proof
  prop_map_append f N ys 
    = toProof $ 
         map f (append N ys) 
           === map f ys 
           === append N (map f ys)
           === append (map f N) (map f ys)
  prop_map_append f (C x xs) ys 
    = toProof $ 
         map f (append (C x xs) ys)
           === map f (C x (append xs ys))
           === C (f x) (map f (append xs ys))
               ? prop_map_append f xs ys
           === C (f x) (append (map f xs) (map f ys)) 
           === append (C (f x) (map f xs)) (map f ys)
           === append (map f (C x xs)) (map f ys)
  
  
  {-@ prop_concatMap :: f:(a -> L (L a)) -> xs:L a
                     -> {v:Proof | (concatt (map f xs) == concatMap f xs) }  @-}
  
  prop_concatMap :: (a -> L (L a)) -> L a -> Proof  
  prop_concatMap f N 
    = toProof $ 
        concatt (map f N) 
          === concatt N 
          === N 
          === concatMap f N 
  prop_concatMap f (C x xs)
    = toProof $ 
        concatt (map f (C x xs))
          === concatt (C (f x) (map f xs))
          === append (f x) (concatt (map f xs))
              ? prop_concatMap f xs 
          === append (f x) (concatMap f xs)       
          === concatMap f (C x xs)
  
  {-@ data L [llen] @-}
  data L a = N | C a (L a)
  
  
  {-@ measure llen @-}
  llen :: L a -> Int 
  {-@ llen :: L a -> Nat @-} 
  llen N        = 0 
  llen (C _ xs) = 1 + llen xs 
  
  {-@ measure hd @-}
  {-@ hd :: {v:L a | llen v > 0 } -> a @-}
  hd :: L a -> a 
  hd (C x _) = x 
  
  {-@ measure tl @-}
  {-@ tl :: xs:{L a | llen xs > 0 } -> {v:L a | llen v == llen xs - 1 } @-}
  tl :: L a -> L a 
  tl (C _ xs) = xs 
  