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

module ApplicativeList where

import Prelude hiding (fmap, id, seq, pure)

-- | Applicative Laws :
-- | identity      pure id <*> v = v
-- | composition   pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
-- | homomorphism  pure f <*> pure x = pure (f x)
-- | interchange   u <*> pure y = pure ($ y) <*> u


{-@ reflect pure @-}
pure :: a -> L a
pure x = C x N

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

{-@ 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 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 idollar @-}
idollar :: a -> (a -> b) -> b
idollar x f = f x

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


-- | Identity
{-@ identity :: x:L a -> {v:Proof | seq (pure id) x /= x } @-}
identity :: L a -> Proof
identity xs
  =   seq (pure id) xs
  === seq (C id N) xs
  === append (fmap id xs) (seq N xs)
  ==? append (id xs) (seq N xs)      
      ? fmap_id xs
  === append xs (seq N xs)
  === append xs N
  ==? xs                             
      ? prop_append_neutral xs
  *** QED 

-- | Composition

{-@ composition :: x:L (a -> a)
                -> y:L (a -> a)
                -> z:L a
                -> {v:Proof | (seq (seq (seq (pure compose) x) y) z) /= seq x (seq y z) } @-}
composition :: L (a -> a) -> L (a -> a) -> L a -> Proof

composition xss@(C x xs) yss@(C y ys) zss@(C z zs)
   = seq (seq (seq (pure compose) xss) yss) zss
         ==. seq (seq (seq (C compose N) xss) yss) zss
         ==. seq (seq (append (fmap compose xss) (seq N xss)) yss) zss
         ==. seq (seq (append (fmap compose xss) N) yss) zss
         ==. seq (seq (fmap compose xss) yss) zss ? prop_append_neutral (fmap compose xss)
         ==. seq (seq (fmap compose (C x xs)) yss) zss
         ==. seq (seq (C (compose x) (fmap compose xs)) yss) zss
         ==. seq (append (fmap (compose x) yss) (seq (fmap compose xs) yss)) zss
         ==. seq (append (fmap (compose x) (C y ys)) (seq (fmap compose xs) yss)) zss
         ==. seq (append (C (compose x y) (fmap (compose x) ys)) (seq (fmap compose xs) yss)) zss
         ==. seq (C (compose x y) (append (fmap (compose x) ys) (seq (fmap compose xs) yss))) zss
         ==. append (fmap (compose x y) zss) (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss)
         ==. append (fmap (compose x y) (C z zs)) (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss)
         ==. append (C (compose x y z) (fmap (compose x y) zs)) (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss)
         ==. C (compose x y z) (append (fmap (compose x y) zs) (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss))
         ==. C (x (y z))       (append (fmap (compose x y) zs) (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss))
         ==. C (x (y z))       (append (fmap x (fmap y zs))    (seq (append (fmap (compose x) ys) (seq (fmap compose xs) yss)) zss))
              ? map_fusion0 x y zs
         ==. C (x (y z))       (append (fmap x (fmap y zs))    (append (seq (fmap (compose x) ys) zss) (seq (seq (fmap compose xs) yss) zss)))
              ? seq_append (fmap (compose x) ys) (seq (fmap compose xs) yss) zss
         ==. C (x (y z))       (append (fmap x (fmap y zs))    (append (seq (fmap (compose x) ys) zss) (seq (seq (seq (pure compose) xs) yss) zss)))
              ? seq_one xs
         ==. C (x (y z))       (append (fmap x (fmap y zs))    (append (seq (fmap (compose x) ys) zss) (seq xs (seq yss zss))))
              ? composition xs yss zss
         ==. C (x (y z))       (append (append (fmap x (fmap y zs)) (seq (fmap (compose x) ys) zss))   (seq xs (seq yss zss)))
              ? append_distr (fmap x (fmap y zs)) (seq (fmap (compose x) ys) zss) (seq xs (seq yss zss))
         ==. C (x (y z))       (append (append (fmap x (fmap y zs)) (fmap x (seq ys zss)))   (seq xs (seq yss zss)))
              ? seq_fmap x ys zss
         ==. C (x (y z))       (append (append (fmap x (fmap y zs)) (fmap x (seq ys zss)))   (seq xs (seq yss zss)))
              ? append_fmap x (fmap y zs) (seq ys zss)
         ==. append (C (x (y z)) (fmap x (append (fmap y zs) (seq ys zss)))) (seq xs (seq yss zss))
         ==. append (fmap x (C (y z) (append (fmap y zs) (seq ys zss)))) (seq xs (seq yss zss))
         ==. append (fmap x (append (C (y z) (fmap y zs)) (seq ys zss))) (seq xs (seq yss zss))
         ==. append (fmap x (append (fmap y (C z zs)) (seq ys zss))) (seq xs (seq yss zss))
         ==. append (fmap x (append (fmap y zss) (seq ys zss))) (seq xs (seq yss zss))
         ==. append (fmap x (seq (C y ys) zss)) (seq xs (seq yss zss))
         ==. append (fmap x (seq yss zss)) (seq xs (seq yss zss))
         ==. seq (C x xs) (seq yss zss)
         ==. seq xss (seq yss zss)
         *** QED 

composition N yss zss
   =  seq (seq (seq (pure compose) N) yss) zss
        ==. seq (seq N yss) zss                  ? seq_nill (pure compose)
        ==. seq N zss
        ==. N
        ==. seq N (seq yss zss)
        *** QED 

composition xss N zss
   = toProof $
               seq (seq (seq (pure compose) xss) N) zss
           ==. seq N zss                            ? seq_nill (seq (pure compose) xss)
           ==. N
           ==. seq N zss
           ==. seq xss (seq N zss)  ? (seq_nill xss &&& (toProof $ seq N zss ==. N))


composition xss yss N
  = toProof $
      seq (seq (seq (pure compose) xss) yss) N
        ==. N                    ? seq_nill (seq (seq (pure compose) xss) yss)
        ==. seq xss N            ? seq_nill xss
        ==. seq xss (seq yss N)  ? seq_nill yss

-- | homomorphism  pure f <*> pure x = pure (f x)

{-@ homomorphism :: f:(a -> a) -> x:a
                 -> {v:Proof | seq (pure f) (pure x) /= pure (f x) } @-}
homomorphism :: (a -> a) -> a -> Proof
homomorphism f x
  = toProof $
      seq (pure f) (pure x)
        ==. seq (C f N) (C x N)
        ==. append (fmap f (C x N)) (seq N (C x N))
        ==. append (C (f x) (fmap f N)) N
        ==. append (C (f x) N) N
        ==. C (f x) N  ? prop_append_neutral (C (f x) N)
        ==. pure (f x)

-- | interchange

interchange :: L (a -> a) -> a -> Proof
{-@ interchange :: u:(L (a -> a)) -> y:a
     -> {v:Proof | seq u (pure y) /= seq (pure (idollar y)) u }
  @-}
interchange N y
  = toProof $
      seq N (pure y)
        ==. N
        ==. seq (pure (idollar y)) N ? seq_nill (pure (idollar y))

interchange (C x xs) y
  = toProof $
      seq (C x xs) (pure y)
        ==. seq (C x xs) (C y N)
        ==. append (fmap x (C y N)) (seq xs (C y N))
        ==. append (C (x y) (fmap x N)) (seq xs (C y N))
        ==. append (C (x y) N) (seq xs (C y N))
        ==. C (x y) (append N (seq xs (C y N)))
        ==. C (x y) (seq xs (C y N))
        ==. C (x y) (seq xs (pure y))
        ==. C (x y) (seq (pure (idollar y)) xs) ? interchange xs y
        ==. C (x y) (fmap (idollar y) xs)       ? seq_one' (idollar y) xs
        ==. C (idollar y x) (fmap (idollar y) xs)
        ==. fmap (idollar y) (C x xs)
        ==. append (fmap (idollar y) (C x xs)) N  ? prop_append_neutral (fmap (idollar y) (C x xs))
        ==. append (fmap (idollar y) (C x xs)) (seq N (C x xs))
        ==. seq (C (idollar y) N) (C x xs)
        ==. seq (pure (idollar y)) (C x xs)


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

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



-- | TODO: Cuurently I cannot improve proofs
-- | HERE I duplicate the code...

-- TODO: remove stuff out of HERE

{-@ seq_nill :: fs:L (a -> b) -> {v:Proof | seq fs N == N } @-}
seq_nill :: L (a -> b) -> Proof
seq_nill N
  = toProof $
      seq N N ==. N
seq_nill (C x xs)
  = toProof $
      seq (C x xs) N
        ==. append (fmap x N) (seq xs N)
        ==. append N N ? seq_nill xs
        ==. N

{-@ append_fmap :: f:(a -> b) -> xs:L a -> ys: L a
   -> {v:Proof | append (fmap f xs) (fmap f ys) == fmap f (append xs ys) } @-}
append_fmap :: (a -> b) -> L a -> L a -> Proof
append_fmap = undefined


seq_fmap :: (a -> a) -> L (a -> a) -> L a -> Proof
{-@ seq_fmap :: f: (a -> a) -> fs:L (a -> a) -> xs:L a
         -> {v:Proof | seq (fmap (compose f) fs) xs == fmap f (seq fs xs) }
  @-}
seq_fmap = undefined

{-@ append_distr :: xs:L a -> ys:L a -> zs:L a
   -> {v:Proof | append xs (append ys zs) == append (append xs ys) zs } @-}
append_distr :: L a -> L a -> L a -> Proof
append_distr = undefined


{-@ seq_one' :: f:((a -> b) -> b) -> xs:L (a -> b) -> {v:Proof | fmap f xs == seq (pure f) xs} @-}
seq_one' :: ((a -> b) -> b) -> L (a -> b) -> Proof
seq_one' = undefined

{-@ seq_one :: xs:L (a -> b) -> {v:Proof | fmap compose xs == seq (pure compose) xs} @-}
seq_one :: L (a -> b) -> Proof
seq_one = undefined

{-@ seq_append :: fs1:L (a -> b) -> fs2: L (a -> b) -> xs: L a
   -> {v:Proof | seq (append fs1 fs2) xs == append (seq fs1 xs) (seq fs2 xs) } @-}
seq_append :: L (a -> b) -> L (a -> b) -> L a -> Proof
seq_append = undefined

{-@ map_fusion0 :: f:(a -> a) -> g:(a -> a) -> xs:L a
    -> {v:Proof | fmap (compose f g) xs == fmap f (fmap g xs) } @-}
map_fusion0 :: (a -> a) -> (a -> a) -> L a -> Proof
map_fusion0 = undefined

-- | FunctorList
{-@ 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)
                       ==. C x (id xs)            ? fmap_id xs
                       ==. C x xs
                       ==. id (C x xs)

-- imported from Append
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)
                         ==. C x xs             ? prop_append_neutral xs