content: {-@ LIQUID "--reflection"      @-}
  
  module MonadList where
  
  import Prelude hiding (return, (>>=))
  
  import Language.Haskell.Liquid.ProofCombinators 
  
  -- | Monad Laws :
  -- | Left identity:	  return a >>= f  ≡ f a
  -- | Right identity:	m >>= return    ≡ m
  -- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)
  
  {-@ reflect return @-}
  return :: a -> L a
  return x = x ::: Emp
  
  {-@ reflect bind @-}
  bind :: L a -> (a -> L b) -> L b
  bind m f
    | llen m > 0 = append (f (hd m)) (bind (tl m) f)
    | otherwise  = Emp
  
  
  {-@ reflect append @-}
  append :: L a -> L a -> L a
  append xs ys
    | llen xs == 0 = ys
    | otherwise    = hd xs ::: append (tl xs) ys
  
  -- | Left Identity
  {-@ left_identity :: x:a -> f:(a -> L b) -> { bind (return x) f == f x } @-}
  left_identity :: a -> (a -> L b) -> Proof
  left_identity x f
    =   bind (return x) f
    === bind (x ::: Emp) f
    === append (f x) (bind Emp f)
    === append (f x) Emp
      ? prop_append_neutral (f x)
    === f x                      
    *** QED
  
  -- | Right Identity
  
  {-@ right_identity :: x:L a -> { bind x return == x } @-}
  right_identity :: L a -> Proof
  right_identity Emp
    = bind Emp return
    === Emp
    *** QED
  
  right_identity (x ::: xs)
    =   bind (x ::: xs) return
    === append (return x)   (bind xs return)
    === append (x ::: Emp)    (bind xs return)
    === x ::: append Emp (bind xs return)
    === x ::: bind xs return
      ? right_identity xs
    === x ::: xs                              
    *** QED
  
  
  -- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)
  {-@ associativity :: m:L a -> f: (a -> L b) -> g:(b -> L c)
        -> {bind (bind m f) g == bind m (\x:a -> (bind (f x) g)) } @-}
  associativity :: L a -> (a -> L b) -> (b -> L c) -> Proof
  associativity Emp f g
    =   bind (bind Emp f) g
    === bind Emp g
    === Emp
    === bind Emp (\x -> (bind (f x) g))
    *** QED
  associativity (x ::: xs) f g
    =   bind (bind (x ::: xs) f) g
        ? bind_append (f x) (bind xs f) g
    === bind (append (f x) (bind xs f)) g                    
    === append (bind (f x) g) (bind (bind xs f) g)
        ? associativity xs f g
    === append (bind (f x) g) (bind xs (\y -> bind (f y) g)) 
        ? βequivalence f g x 
    === append ((\y -> bind (f y) g) x) (bind xs (\y -> bind (f y) g)) 
    === bind (x ::: xs) (\y -> bind (f y) g)
    *** QED
  
  
  
  {-@ assume βequivalence :: f:(a -> L b) -> g:(b -> L c) -> x:a -> 
       {bind (f x) g == (\y:a -> bind (f y) g) (x)}  @-}
  βequivalence :: (a -> L b) -> (b -> L c) -> a -> Proof
  βequivalence f g x = trivial 
  
  bind_append :: L a -> L a -> (a -> L b) -> Proof
  {-@ bind_append :: xs:L a -> ys:L a -> f:(a -> L b)
       -> { bind (append xs ys) f == append (bind xs f) (bind ys f) }
    @-}
  
  bind_append Emp ys f
    =   bind (append Emp ys) f
    === bind ys f
    === append Emp (bind ys f)
    === append (bind Emp f) (bind ys f)
    *** QED
  bind_append (x ::: xs) ys f
    =   bind (append (x ::: xs) ys) f
    === bind (x ::: append xs ys) f
    === append (f x) (bind (append xs ys) f)
        ? bind_append xs ys f
    === append (f x) (append (bind xs f) (bind ys f)) 
        ? prop_assoc (f x) (bind xs f) (bind ys f)
    === append (append (f x) (bind xs f)) (bind ys f) 
    === append (bind (x ::: xs) f) (bind ys f)
    *** QED
  
  {-@ data L [llen] @-}
  data L a = Emp | a ::: L a
  
  {-@ measure llen @-}
  llen :: L a -> Int
  {-@ llen :: L a -> Nat @-}
  llen Emp        = 0
  llen (_ ::: xs) = 1 + llen xs
  
  {-@ measure hd @-}
  {-@ hd :: {v:L a | llen v > 0 } -> a @-}
  hd :: L a -> a
  hd (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 (_ ::: xs) = xs
  
  
  -- NV TODO: import there
  
  -- imported from Append
  prop_append_neutral :: L a -> Proof
  {-@ prop_append_neutral :: xs:L a -> { append xs Emp == xs }  @-}
  prop_append_neutral Emp
    =   append Emp Emp 
    === Emp
    *** QED
  prop_append_neutral (x ::: xs)
    =   append (x ::: xs) Emp
    === x ::: append xs Emp
        ? prop_append_neutral xs
    === x ::: xs             
    *** QED
  
  {-@ prop_assoc :: xs:L a -> ys:L a -> zs:L a
                 -> { append (append xs ys) zs == append xs (append ys zs) } @-}
  prop_assoc :: L a -> L a -> L a -> Proof
  prop_assoc Emp ys zs
    =   append (append Emp ys) zs
    === append ys zs
    === append Emp (append ys zs)
    *** QED
  
  prop_assoc (x ::: xs) ys zs
    =   append (append (x ::: xs) ys) zs
    === append (x ::: append xs ys) zs
    === x ::: append (append xs ys) zs
        ? prop_assoc xs ys zs
    === x ::: append xs (append ys zs)  
    === append (x ::: xs) (append ys zs)
    *** QED
  