module StructurallyRecursiveDescentParsing.Simplified.Lemmas where
open import Algebra
open import Category.Monad
open import Data.Function
open import Data.Product
import Data.List.NonEmpty as List⁺
open List⁺ using (List⁺; _∷_; [_]; _⁺++⁺_; head; tail)
open RawMonad List⁺.monad using () renaming (_>>=_ to _>>=⁺_)
open import Data.List.NonEmpty.Properties
import Data.List as List
open List using (List; _∷_; []; _++_)
private module LM {A} = Monoid (List.monoid A)
open RawMonad List.monad using () renaming (_>>=_ to _>>=′_)
import Data.List.Properties as ListProp
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
>>=-∅ : ∀ {A B} (xs : List A) →
(xs >>=′ const {List B} []) ≡ []
>>=-∅ [] = refl
>>=-∅ (x ∷ xs) = >>=-∅ xs
tail-++ : ∀ {A} (xs ys : List⁺ A) →
tail xs ++ List⁺.toList ys ≡ tail (xs ⁺++⁺ ys)
tail-++ [ x ] ys = refl
tail-++ (x ∷ xs) ys = toList-⁺++⁺ xs ys
head->>= : ∀ {A B} (f : A → List⁺ B) (xs : List⁺ A) →
head (f (head xs)) ≡ head (xs >>=⁺ f)
head->>= f [ x ] = refl
head->>= f (x ∷ xs) with f x
head->>= f (x ∷ xs) | [ y ] = refl
head->>= f (x ∷ xs) | (y ∷ ys) = refl
tail->>= : ∀ {A B} (f : A → List⁺ B) (xs : List⁺ A) →
tail (f (head xs)) ++ (tail xs >>=′ λ x → head (f x) ∷ tail (f x)) ≡
tail (xs >>=⁺ f)
tail->>= f [ x ] = proj₂ LM.identity _
tail->>= f (x ∷ xs) = begin
tail (f x) ++ (List⁺.toList xs >>=′ λ x → head (f x) ∷ tail (f x)) ≡⟨ cong (λ ys → tail (f x) ++ List.concat ys)
(ListProp.map-cong (η ∘ f) (List⁺.toList xs)) ⟩
tail (f x) ++ (List⁺.toList xs >>=′ List⁺.toList ∘ f) ≡⟨ cong (_++_ (tail (f x))) (toList->>= f xs) ⟩
tail (f x) ++ (List⁺.toList (xs >>=⁺ f)) ≡⟨ tail-++ (f x) (xs >>=⁺ f) ⟩
tail (f x ⁺++⁺ (xs >>=⁺ f)) ≡⟨ refl ⟩
tail (x ∷ xs >>=⁺ f) ∎