{-@ LIQUID "--higherorder"     @-}
{-@ LIQUID "--totality"        @-}
{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--higherorderqs" @-}

{-@ LIQUID "--automatic-instances=liquidinstances" @-}


{-# LANGUAGE IncoherentInstances   #-}
{-# LANGUAGE FlexibleContexts #-}
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 _ N        = N 
fmap f (C x xs) = C (f x) (fmap f 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 :: xs:L a -> { fmap id xs == id xs } @-}
fmap_id :: L a -> Proof
fmap_id N
  = trivial 
fmap_id (C x xs)
  = fmap_id (xs)

-- | Distribution

{-@ 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
  = trivial 
fmap_distrib f g (C x xs)
  = fmap_distrib f g xs


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


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