module List+ where

open import Prelude
open import Logic.Base
open import Logic.Identity
open import Logic.ChainReasoning

data List⁺ (A : Set) : Set where
  [_]⁺ : A -> List⁺ A
  _::⁺_ : A -> List⁺ A -> List⁺ A

infixr 50 _::⁺_ 

module ChainR = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)
open ChainR


foldr⁺ : {A B : Set} -> (A -> B -> B) -> (A -> B) -> List⁺ A -> B
foldr⁺ f g [ a ]⁺ = g a
foldr⁺ f g (a ::⁺ x) = f a (foldr⁺ f g x)

map⁺ : {A B : Set} -> (A -> B) -> List⁺ A -> List⁺ B
map⁺ f = foldr⁺ (\a x -> f a ::⁺ x) ([_]⁺ ∘ f)

_++⁺_ : {A : Set} -> List⁺ A -> List⁺ A -> List⁺ A
x ++⁺ y = foldr⁺ _::⁺_ (\a -> a ::⁺ y) x

concat⁺ : {A : Set} -> List⁺ (List⁺ A) -> List⁺ A
concat⁺ = foldr⁺ _++⁺_ id 



foldr⁺-fusion : {A B C : Set} ->  
  (h : B -> C) -> {f : A -> B -> B} -> {g : A -> C -> C} -> {k : A -> B} -> {l : A -> C} ->
   ((a : A) -> (b : B) -> h (f a b) ≡ g a (h b)) ->
      ((a : A) -> h (k a) ≡ l a) ->
        ∀ (\x -> h (foldr⁺ f k x) ≡ foldr⁺ g l x)
foldr⁺-fusion h {f} {g} {k} {l} _ q [ a ]⁺ = q a
foldr⁺-fusion h {f} {g} {k} {l} p q (a ::⁺ x) =
   chain> h (foldr⁺ f k (a ::⁺ x))  
      === h (f a (foldr⁺ f k x))      by refl 
      === g a (h (foldr⁺ f k x))      by p a (foldr⁺ f k x)
      === g a (foldr⁺ g l x)          by cong (g a) (foldr⁺-fusion h p q x) 
      === foldr⁺ g l (a ::⁺ x)        by refl


foldr⁺-fusion' : {A B C : Set} ->  
  (h : B -> C) -> {f : A -> B -> B} -> {g : A -> C -> C} -> {k : A -> B} ->
   ((a : A) -> (b : B) -> h (f a b) ≡ g a (h b)) ->
        ∀ (\x -> h (foldr⁺ f k x) ≡ foldr⁺ g (h ∘ k) x)
foldr⁺-fusion' h {f} {g} {k} p x = foldr⁺-fusion h {f} {g} {k} {h ∘ k} p (\_ -> refl) x



idIsFold⁺ : {A : Set} -> (x : List⁺ A) -> 
               (x ≡ foldr⁺ _::⁺_ [_]⁺ x)
idIsFold⁺ {_} [ a ]⁺ = refl
idIsFold⁺ {_} (a ::⁺ x) = 
   chain> (a ::⁺ x)
      === a ::⁺ foldr⁺ _::⁺_ [_]⁺ x    by cong (_::⁺_ a) (idIsFold⁺ x)
      === foldr⁺ _::⁺_ [_]⁺ (a ::⁺ x)  by refl

map⁺-compose : {A B C : Set} -> {g : B -> C} -> {f : A -> B} -> 
                (x : List⁺ A) -> (map⁺ (g ∘ f) x ≡ (map⁺ g ∘ map⁺ f) x)
map⁺-compose {A} {B} {C} {g} {f} x = 
   chain> map⁺ (g ∘ f) x
      === map⁺ (g ∘ f) (foldr⁺ _::⁺_ [_]⁺ x)
             by cong (map⁺ (g ∘ f)) (idIsFold⁺ x)
      === foldr⁺ (\a y -> g (f a) ::⁺ y) ([_]⁺ ∘ g ∘ f) x
             by foldr⁺-fusion' (map⁺ (g ∘ f)) (\_ _ -> refl) x
      === (map⁺ g ∘ foldr⁺ (\a y -> f a ::⁺ y) ([_]⁺ ∘ f)) x 
             by sym (foldr⁺-fusion' (map⁺ g) (\_ _ -> refl) x)
      === (map⁺ g ∘ map⁺ f) x
             by refl

map⁺-cat⁺ : {A B : Set} -> {f : A -> B} -> (x : List⁺ A) -> {y : List⁺ A} ->
      map⁺ f (x ++⁺ y) ≡ (map⁺ f x ++⁺ map⁺ f y)
map⁺-cat⁺ {A} {B} {f} x {y} = 
  chain> map⁺ f (x ++⁺ y) 
     === map⁺ f (foldr⁺ _::⁺_ (\a -> a ::⁺ y) x)
                 by refl
     === foldr⁺ (\a z -> f a ::⁺ z) (\a -> f a ::⁺ map⁺ f y) x    
                 by foldr⁺-fusion' (map⁺ f) (\_ _ -> refl) x
     === foldr⁺ (\a z -> f a ::⁺ z) ([_]⁺ ∘ f) x ++⁺ (map⁺ f y) 
                 by sym (foldr⁺-fusion' (\z -> z ++⁺ map⁺ f y) (\_ _ -> refl) x)
     === map⁺ f x ++⁺ map⁺ f y
                 by refl

concat⁺-map⁺ : {A B : Set} -> {f : A -> B} -> 
         ∀ (\xs -> concat⁺ (map⁺ (map⁺ f) xs) ≡ map⁺ f (concat⁺ xs))
concat⁺-map⁺ {A} {B} {f} xs = 
  chain> concat⁺ (map⁺ (map⁺ f) xs) 
     === concat⁺ (foldr⁺ (\x ys -> map⁺ f x ::⁺ ys) ([_]⁺ ∘ map⁺ f) xs) by refl
     === foldr⁺ (\x xs -> map⁺ f x ++⁺ xs) (map⁺ f) xs          by foldr⁺-fusion' concat⁺ (\_ _ -> refl) xs
     === map⁺ f (concat⁺ xs)                           
           by sym (foldr⁺-fusion' (map⁺ f) (\z w -> map⁺-cat⁺ z) xs)


foldr⁺-eq : {A B : Set} -> {f g : A -> B -> B} -> {h k : A -> B} ->
             (forall a -> forall b -> f a b ≡ g a b) ->
              (forall a -> h a ≡ k a) -> 
               forall x -> foldr⁺ f h x ≡ foldr⁺ g k x
foldr⁺-eq {A} {B} {f} {g} {h} {k} f≡g h≡k x =
   chain> foldr⁺ f h x 
      === foldr⁺ f h (foldr⁺ _::⁺_ [_]⁺ x)  by cong (foldr⁺ f h) (idIsFold⁺ x)
      === foldr⁺ g k x                     by foldr⁺-fusion (foldr⁺ f h) (\a x -> f≡g a (foldr⁺ f h x)) h≡k x

map⁺-eq : {A B : Set} -> {f g : A -> B} ->
           (forall a -> f a ≡ g a) -> forall x -> map⁺ f x ≡ map⁺ g x
map⁺-eq {A} {B} {f} {g} f≡g x = 
    chain> map⁺ f x
       === foldr⁺ (\a y -> f a ::⁺ y) ([_]⁺ ∘ f) x  
              by refl
       === foldr⁺ (\a y -> g a ::⁺ y) ([_]⁺ ∘ g) x 
              by foldr⁺-eq (\a y -> cong (\b -> b ::⁺ y) (f≡g a)) (\a -> cong [_]⁺ (f≡g a)) x
       === map⁺ g x                                 
              by refl