-- | Universal property of foldr a la Zombie
-- | cite : http://www.seas.upenn.edu/~sweirich/papers/congruence-extended.pdf

{-@ LIQUID "--reflection"     @-}
{-@ LIQUID "--ple"     @-}

module FoldrUniversal where

import Language.Haskell.Liquid.ProofCombinators
import Prelude hiding (foldr)

-- | foldrUniversal
{-@ axiomatize foldr @-}
foldr :: (a -> b -> b) -> b -> L a -> b
foldr f b (C x xs) = f x (foldr f b xs)
foldr f b Emp      = b


{-@ axiomatize compose @-}
compose :: (b -> c) -> (a -> b) ->  a -> c
compose f g x = f (g x)

{-@ foldrUniversal
      :: f:(a -> b -> b)
      -> h:(L a -> b)
      -> e:b
      -> ys:L a
      -> base:{h Emp == e }
      -> step: (x:a -> xs:L a -> {h (C x xs) == f x (h xs)})
      -> { h ys == foldr f e ys }
  @-}
foldrUniversal
    :: (a -> b -> b)
    -> (L a -> b)
    -> b
    -> L a
    -> Proof
    -> (a -> L a -> Proof)
    -> Proof
foldrUniversal f h e Emp base step
  =   trivial
foldrUniversal f h e (C x xs) base step
  =   step x xs &&& foldrUniversal f h e xs base step


-- | foldrFunsion

{-@ foldrFusion :: h:(b -> c) -> f:(a -> b -> b) -> g:(a -> c -> c) -> e:b -> ys:L a
            -> fuse:(x:a -> y:b -> {h (f x y) == g x (h y)})
            -> { (compose h (foldr f e)) (ys) == foldr g (h e) ys }
  @-}
foldrFusion :: (b -> c) -> (a -> b -> b) -> (a -> c -> c) -> b -> L a
             -> (a -> b -> Proof)
             -> Proof
foldrFusion h f g e ys fuse
  = foldrUniversal g (compose h (foldr f e)) (h e) ys
       (fuse_base h f e)
       (fuse_step h f e g fuse)

fuse_step :: (b -> c) -> (a -> b -> b) -> b -> (a -> c -> c)
         -> (a -> b -> Proof)
         -> a -> L a -> Proof
{-@ fuse_step :: h:(b -> c) -> f:(a -> b -> b) -> e:b -> g:(a -> c -> c)
         -> thm:(x:a -> y:b -> { h (f x y) == g x (h y)})
         -> x:a -> xs:L a
         -> {(compose h (foldr f e)) (C x xs) == g x ((compose h (foldr f e)) (xs))}
  @-}
fuse_step h f e g thm x Emp
  = thm x e

fuse_step h f e g thm x (C y ys)
  = thm x (f y (foldr f e ys))

fuse_base :: (b->c) -> (a -> b -> b) -> b -> Proof
{-@ fuse_base :: h:(b->c) -> f:(a -> b -> b) -> e:b
              -> { compose h (foldr f e) Emp == h e } @-}
fuse_base h f e
  = trivial



data L a = Emp | C a (L a)
{-@ data L [llen] a = Emp | C {hs :: a, tl :: L a} @-}


{-@ measure llen @-}
llen :: L a -> Int
{-@ llen :: L a -> Nat @-}
llen Emp        = 0
llen (C _ xs) = 1 + llen xs