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

module FunctorList where

import Prelude hiding (fmap, id)
import Language.Haskell.Liquid.ProofCombinators

-- | Functor Laws :
-- | fmap-id fmap id ≡ id
-- | fmap-distrib ∀ g h . fmap (g ◦ h) ≡ fmap g ◦ fmap h

{-@ reflect fmap @-}
fmap :: (a -> b) -> L a -> L b
fmap f xs
  | llen xs == 0 = N
  | otherwise    = C (f (hd xs)) (fmap f (tl xs))

{-@ reflect id @-}
id :: a -> a
id x = x

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

{-@ fmap_id' :: {v:Proof | fmap id /= id } @-}
fmap_id' :: Proof
fmap_id' = abstract (fmap id) id fmap_id


{-@ fmap_id :: xs:L a -> {v:Proof | fmap id xs /= id xs } @-}
fmap_id :: L a -> Proof
fmap_id N
  = toProof $
      fmap id N === N
                === id N
fmap_id (C x xs)
  = toProof $
      fmap id (C x xs) === C (id x) (fmap id xs)
                       === C x (fmap id xs)
                         ? fmap_id xs
                       === C x (id xs)            
                       === C x xs
                       === id (C x xs)


-- | Distribution

{-@ fmap_distrib' :: f:(a -> a) -> g:(a -> a)
               -> {v:Proof | fmap  (compose f g) /= compose (fmap f) (fmap g) } @-}
fmap_distrib' :: (a -> a) -> (a -> a) -> Proof
fmap_distrib' f g
  = abstract (fmap  (compose f g)) (compose (fmap f) (fmap g))
       (fmap_distrib f g)


{-@ fmap_distrib :: f:(a -> a) -> g:(a -> a) -> xs:L a
               -> {v:Proof | fmap  (compose f g) xs /= (compose (fmap f) (fmap g)) (xs) } @-}
fmap_distrib :: (a -> a) -> (a -> a) -> L a -> Proof
fmap_distrib f g N
  = toProof $
      (compose (fmap f) (fmap g)) N
        === (fmap f) ((fmap g) N)
        === fmap f (fmap g N)
        === fmap f N
        === N
        === fmap (compose f g) N
fmap_distrib f g (C x xs)
  = toProof $
      fmap (compose f g) (C x xs)
       === C ((compose f g) x) (fmap (compose f g) xs)
         ? fmap_distrib f g xs
       === C ((compose f g) x) ((compose (fmap f) (fmap g)) xs) 
       === C ((compose f g) x) (fmap f (fmap g xs))
       === C (f (g x)) (fmap f (fmap g xs))
       === fmap f (C (g x) (fmap g xs))
       === (fmap f) (C (g x) (fmap g xs))
       === (fmap f) (fmap g (C x xs))
       === (fmap f) ((fmap g) (C x xs))
       === (compose (fmap f) (fmap g)) (C x xs)


data L a = N | C a (L a)
{-@ data L [llen] @-}

{-@ measure nill @-}
nill :: L a -> Bool
nill N = True
nill _ = False

{-@ 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

{-@ assume abstract :: f:(a -> b) -> g:(a -> b) -> (x:a -> {v:Proof | f x == g x })
             -> {v:Proof | f == g } @-}
abstract :: (a -> b) -> (a -> b) -> (a -> Proof) -> Proof
abstract _ _ _ = trivial