------------------------------------------------------------------------
-- The parser equivalence proof language is sound
------------------------------------------------------------------------

module TotalParserCombinators.Congruence.Sound where

open import Category.Monad
open import Coinduction
open import Data.List as List
import Data.List.Properties as ListProp
import Data.List.Any as Any
open import Data.List.Any.BagAndSetEquality
open import Data.Maybe
open import Data.Product
open import Function
import Function.Related as Related
open import Level
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

open Any.Membership-≡ using (bag; _∈_; [_]-Order)
                      renaming (_∼[_]_ to _List-∼[_]_)
open Related.EquationalReasoning
  renaming (_∼⟨_⟩_ to _∼⟨_⟩′_; _∎ to _∎′; sym to sym′)
open RawMonad {f = zero} List.monad
  using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)
private
  module BSOrd {k} {A : Set} = Preorder ([ k ]-Order A)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.CoinductiveEquality as CE
  using (_∼[_]c_; _∷_)
open import TotalParserCombinators.Congruence
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib using (return⋆)
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics using (_∼[_]_)

------------------------------------------------------------------------
-- Some lemmas

private

  ⊛flatten-lemma :  {k} {R₁ R₂ : Set} {fs₁ fs₂ : List (R₁  R₂)}
                   (xs₁ xs₂ : Maybe (List R₁)) 
                   fs₁ List-∼[ k ] fs₂ 
                   flatten xs₁ List-∼[ k ] flatten xs₂ 
                   fs₁ ⊛flatten xs₁ List-∼[ k ] fs₂ ⊛flatten xs₂
  ⊛flatten-lemma {k} {fs₁ = fs₁} {fs₂} xs₁ xs₂ fs₁≈fs₂ = helper xs₁ xs₂
    where
    helper :  xs₁ xs₂ 
             flatten xs₁ List-∼[ k ] flatten xs₂ 
             fs₁ ⊛flatten xs₁ List-∼[ k ] fs₂ ⊛flatten xs₂
    helper nothing    nothing     []∼[]      = BSOrd.refl
    helper (just xs₁) (just xs₂) xs₁≈xs₂     = ⊛-cong fs₁≈fs₂ xs₁≈xs₂
    helper nothing    (just xs₂)  []≈xs₂ {x} =
      x  []            ↔⟨ BSOrd.reflexive $ P.sym $
                             ListProp.Applicative.right-zero fs₂ 
      x  (fs₂ ⊛′ [])   ∼⟨ ⊛-cong (BSOrd.refl {x = fs₂}) []≈xs₂ ⟩′
      x  (fs₂ ⊛′ xs₂)  ∎′
    helper (just xs₁) nothing    xs₁∼[]  {x} =
      x  (fs₁ ⊛′ xs₁)  ∼⟨ ⊛-cong (BSOrd.refl {x = fs₁}) xs₁∼[] ⟩′
      x  (fs₁ ⊛′ [])   ↔⟨ BSOrd.reflexive $
                             ListProp.Applicative.right-zero fs₁ 
      x  []            ∎′

  []-⊛flatten :  {A B : Set} (xs : Maybe (List A)) 
                [] ⊛flatten xs List-∼[ bag ] [] {A = B}
  []-⊛flatten nothing   = BSOrd.refl
  []-⊛flatten (just xs) = BSOrd.refl

  bind-lemma :  {k} {R₁ R₂ : Set} {xs₁ xs₂ : Maybe (List R₁)}
               (f₁ f₂ : Maybe (R₁  List R₂)) 
               flatten xs₁ List-∼[ k ] flatten xs₂ 
               (∀ x  apply f₁ x List-∼[ k ] apply f₂ x) 
               bind xs₁ f₁ List-∼[ k ] bind xs₂ f₂
  bind-lemma {k} {xs₁ = xs₁} {xs₂} f₁ f₂ xs₁≈xs₂ = helper f₁ f₂
    where
    helper :  f₁ f₂ 
             (∀ x  apply f₁ x List-∼[ k ] apply f₂ x) 
             bind xs₁ f₁ List-∼[ k ] bind xs₂ f₂
    helper nothing   nothing   []∼[]     = BSOrd.refl
    helper (just f₁) (just f₂) f₁≈f₂     = >>=-cong xs₁≈xs₂ f₁≈f₂
    helper nothing   (just f₂) []≈f₂ {x} =
      x  []                           ∼⟨ BSOrd.reflexive $ P.sym $
                                             ListProp.Monad.right-zero (flatten xs₂) ⟩′
      x  (flatten xs₂ >>=′ λ _  [])  ∼⟨ >>=-cong (BSOrd.refl {x = flatten xs₂}) []≈f₂ ⟩′
      x  (flatten xs₂ >>=′ f₂)        ∎′
    helper (just f₁) nothing   f₁∼[] {x} =
      x  (flatten xs₁ >>=′ f₁)        ∼⟨ >>=-cong (BSOrd.refl {x = flatten xs₁}) f₁∼[] ⟩′
      x  (flatten xs₁ >>=′ λ _  [])  ∼⟨ BSOrd.reflexive $
                                            ListProp.Monad.right-zero (flatten xs₁) ⟩′
      x  []                           ∎′

  bind-nothing :  {A B : Set} (f : Maybe (A  List B)) 
                 bind nothing f List-∼[ bag ] []
  bind-nothing nothing  = BSOrd.refl
  bind-nothing (just f) = BSOrd.refl

------------------------------------------------------------------------
-- Equality is closed under initial-bag

initial-bag-cong :
   {k Tok R xs₁ xs₂} {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} 
  p₁ ∼[ k ]P p₂  initial-bag p₁ List-∼[ k ] initial-bag p₂
initial-bag-cong (xs₁≈xs₂  Dp₁≈Dp₂)   = xs₁≈xs₂
initial-bag-cong (p )                 = BSOrd.refl
initial-bag-cong (p₁ ∼⟨ p₁≈p₂  p₂≈p₃) = _ ∼⟨ initial-bag-cong p₁≈p₂ ⟩′ initial-bag-cong p₂≈p₃
initial-bag-cong (p₁ ≅⟨ p₁≅p₂  p₂≈p₃) = _ ↔⟨ initial-bag-cong p₁≅p₂   initial-bag-cong p₂≈p₃
initial-bag-cong (sym p₁≈p₂)           = sym′ (initial-bag-cong p₁≈p₂)
initial-bag-cong (return x₁≡x₂)        = BSOrd.reflexive $ P.cong [_] x₁≡x₂
initial-bag-cong fail                  = BSOrd.refl
initial-bag-cong token                 = BSOrd.refl
initial-bag-cong (p₁≈p₃  p₂≈p₄)       = ++-cong (initial-bag-cong p₁≈p₃) (initial-bag-cong p₂≈p₄)
initial-bag-cong (f₁≗f₂ <$> p₁≈p₂)     = map-cong f₁≗f₂ $ initial-bag-cong p₁≈p₂
initial-bag-cong (nonempty p₁≈p₂)      = BSOrd.refl

initial-bag-cong (cast {xs₁  = xs₁}  {xs₂  = xs₂}
                       {xs₁′ = xs₁′} {xs₂′ = xs₂′}
                       {xs₁≈xs₁′ = xs₁≈xs₁′} {xs₂≈xs₂′ = xs₂≈xs₂′}
                       p₁≈p₂) {x} =
  x  xs₁′  ↔⟨ sym′ xs₁≈xs₁′ 
  x  xs₁   ∼⟨ initial-bag-cong p₁≈p₂ ⟩′
  x  xs₂   ↔⟨ xs₂≈xs₂′ 
  x  xs₂′  ∎′

initial-bag-cong ([ nothing          - _       ] p₁≈p₃  p₂≈p₄)     = BSOrd.refl
initial-bag-cong ([ just (xs₁ , xs₂) - just _  ] p₁≈p₃  p₂≈p₄)     = ⊛flatten-lemma xs₁ xs₂
                                                                        (initial-bag-cong p₁≈p₃) (initial-bag-cong p₂≈p₄)
initial-bag-cong ([ just (xs₁ , xs₂) - nothing ] p₁≈p₃  p₂≈p₄) {x} =
  x  [] ⊛flatten xs₁  ↔⟨ []-⊛flatten xs₁ 
  x  []               ↔⟨ sym′ $ []-⊛flatten xs₂ 
  x  [] ⊛flatten xs₂  ∎′

initial-bag-cong ([ nothing        - _       ] p₁≈p₃ >>= p₂≈p₄)     = BSOrd.refl
initial-bag-cong ([ just (f₁ , f₂) - just _  ] p₁≈p₃ >>= p₂≈p₄)     = bind-lemma f₁ f₂
                                                                        (initial-bag-cong p₁≈p₃)  x  initial-bag-cong (p₂≈p₄ x))
initial-bag-cong ([ just (f₁ , f₂) - nothing ] p₁≈p₃ >>= p₂≈p₄) {x} =
  x  bind nothing f₁  ↔⟨ bind-nothing f₁ 
  x  []               ↔⟨ sym′ $ bind-nothing f₂ 
  x  bind nothing f₂  ∎′

------------------------------------------------------------------------
-- Equality is closed under D

D-cong :  {k Tok R xs₁ xs₂}
           {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} 
         p₁ ∼[ k ]P p₂   {t}  D t p₁ ∼[ k ]P D t p₂
D-cong (xs₁≈xs₂  Dp₁≈Dp₂)   {t} =  (Dp₁≈Dp₂ t)
D-cong (p )                 {t} = D t p 
D-cong (p₁ ∼⟨ p₁≈p₂  p₂≈p₃) {t} = D t p₁ ∼⟨ D-cong p₁≈p₂  D-cong p₂≈p₃
D-cong (p₁ ≅⟨ p₁≅p₂  p₂≈p₃) {t} = D t p₁ ≅⟨ D-cong p₁≅p₂  D-cong p₂≈p₃
D-cong (sym p₁≈p₂)               = sym (D-cong p₁≈p₂)
D-cong (return x₁≡x₂)            = fail 
D-cong fail                      = fail 
D-cong token                 {t} = return t 
D-cong (p₁≈p₃  p₂≈p₄)           = D-cong p₁≈p₃  D-cong p₂≈p₄
D-cong (f₁≗f₂ <$> p₁≈p₂)         = f₁≗f₂ <$> D-cong p₁≈p₂
D-cong (nonempty p₁≈p₂)          = D-cong p₁≈p₂
D-cong (cast p₁≈p₂)              = D-cong p₁≈p₂

D-cong ([_-_]_⊛_ nothing nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁  p₂)  ∼⟨ [ nothing - just ( , ) ]  D-cong ( p₁≈p₃)   p₂≈p₄ 
  D t (p₃  p₄)  
D-cong ([_-_]_⊛_ nothing (just (fs₁ , fs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁  p₂)                                               ≅⟨ D.D-⊛ p₁ p₂ 
    D t ( p₁)  ♭? p₂  return⋆ (flatten fs₁)  D t (♭? p₂)  ≅⟨ [  -  -  -  ] D t ( p₁)   (♭? p₂ )  (_ ) 
   D t ( p₁)  ♭? p₂  return⋆ (flatten fs₁)  D t (♭? p₂)  ∼⟨ [ nothing - just ( , ) ]  D-cong ( p₁≈p₃)  p₂≈p₄ 
                                                                 [ just ( , ) - just ( , ) ]
                                                                   Return⋆.cong (initial-bag-cong ( p₁≈p₃))  D-cong p₂≈p₄ 
   D t ( p₃)  ♭? p₄  return⋆ (flatten fs₂)  D t (♭? p₄)  ≅⟨ [  -  -  -  ] D t ( p₃)   (♭? p₄ )  (_ ) 
    D t ( p₃)  ♭? p₄  return⋆ (flatten fs₂)  D t (♭? p₄)  ≅⟨ sym $ D.D-⊛ p₃ p₄ 
  D t (p₃  p₄)                                               
D-cong ([_-_]_⊛_ (just _) nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁  p₂)                                   ≅⟨ D.D-⊛ p₁ p₂ 
  D t (♭? p₁)   p₂  return⋆ []    D t ( p₂)  ≅⟨ (D t (♭? p₁)   p₂ ) 
                                                     [  -  -  -  ] return⋆ []   (D t ( p₂) ) 
  D t (♭? p₁)   p₂  return⋆ []   D t ( p₂)  ∼⟨ [ just ( , ) - just ( , ) ] D-cong p₁≈p₃   p₂≈p₄ 
                                                     [ just ( , ) - nothing ] (return⋆ [] )   D-cong ( p₂≈p₄) 
  D t (♭? p₃)   p₄  return⋆ []   D t ( p₄)  ≅⟨ (D t (♭? p₃)   p₄ ) 
                                                     [  -  -  -  ] return⋆ []   (D t ( p₄) ) 
  D t (♭? p₃)   p₄  return⋆ []    D t ( p₄)  ≅⟨ sym $ D.D-⊛ p₃ p₄ 
  D t (p₃  p₄)                                   
D-cong ([_-_]_⊛_ (just _) (just (fs₁ , fs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁  p₂)                                              ≅⟨ D.D-⊛ p₁ p₂ 
  D t (♭? p₁)  ♭? p₂  return⋆ (flatten fs₁)  D t (♭? p₂)  ∼⟨ [ just ( , ) - just ( , ) ] D-cong p₁≈p₃  p₂≈p₄ 
                                                                [ just ( , ) - just ( , ) ] Return⋆.cong (initial-bag-cong p₁≈p₃) 
                                                                                                D-cong p₂≈p₄ 
  D t (♭? p₃)  ♭? p₄  return⋆ (flatten fs₂)  D t (♭? p₄)  ≅⟨ sym $ D.D-⊛ p₃ p₄ 
  D t (p₃  p₄)                                              

D-cong ([_-_]_>>=_ nothing nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)  ∼⟨ [ nothing - just ( , ) ]  D-cong ( p₁≈p₃) >>= (  p₂≈p₄) 
  D t (p₃ >>= p₄)  
D-cong ([_-_]_>>=_ nothing (just (xs₁ , xs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                         ≅⟨ D.D->>= p₁ p₂ 
    D t ( p₁) >>= (♭?  p₂)  return⋆ (flatten xs₁) >>= (D t  ♭?  p₂)  ≅⟨ [  -  -  -  ] D t ( p₁)  >>=  x  ♭? (p₂ x) ) 
                                                                             (_ ) 
   D t ( p₁) >>= (♭?  p₂)  return⋆ (flatten xs₁) >>= (D t  ♭?  p₂)  ∼⟨ [ nothing - just ( , ) ]  D-cong ( p₁≈p₃) >>= p₂≈p₄ 
                                                                             [ just ( , ) - just ( , ) ]
                                                                               Return⋆.cong (initial-bag-cong ( p₁≈p₃)) >>=
                                                                                x  D-cong (p₂≈p₄ x)) 
   D t ( p₃) >>= (♭?  p₄)  return⋆ (flatten xs₂) >>= (D t  ♭?  p₄)  ≅⟨ [  -  -  -  ] D t ( p₃)  >>=  x  ♭? (p₄ x) ) 
                                                                             (_ ) 
    D t ( p₃) >>= (♭?  p₄)  return⋆ (flatten xs₂) >>= (D t  ♭?  p₄)  ≅⟨ sym $ D.D->>= p₃ p₄ 
  D t (p₃ >>= p₄)                                                         
D-cong ([_-_]_>>=_ (just _) nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                     ≅⟨ D.D->>= p₁ p₂ 
  D t (♭? p₁) >>= (  p₂)  return⋆ [] >>= (D t    p₂)            ≅⟨ (D t (♭? p₁) >>= (  p₂) ) 
                                                                         [  -  -  -  ] return⋆ []  >>=  x  D t ( (p₂ x)) ) 
  D t (♭? p₁) >>= (  p₂)  return⋆ [] >>=  x   D t ( (p₂ x)))  ∼⟨ [ just ( , ) - just ( , ) ] D-cong p₁≈p₃ >>= (  p₂≈p₄) 
                                                                         [ just ( , ) - nothing ] (return⋆ [] ) >>=
                                                                                                     x   D-cong ( (p₂≈p₄ x))) 
  D t (♭? p₃) >>= (  p₄)  return⋆ [] >>=  x   D t ( (p₄ x)))  ≅⟨ (D t (♭? p₃) >>= (  p₄) ) 
                                                                         [  -  -  -  ] return⋆ []  >>=  x  D t ( (p₄ x)) ) 
  D t (♭? p₃) >>= (  p₄)  return⋆ [] >>= (D t    p₄)            ≅⟨ sym $ D.D->>= p₃ p₄ 
  D t (p₃ >>= p₄)                                                     
D-cong ([_-_]_>>=_ (just _) (just (xs₁ , xs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                        ≅⟨ D.D->>= p₁ p₂ 
  D t (♭? p₁) >>= (♭?  p₂)  return⋆ (flatten xs₁) >>= (D t  ♭?  p₂)  ∼⟨ [ just ( , ) - just ( , ) ] D-cong p₁≈p₃ >>= p₂≈p₄ 
                                                                            [ just ( , ) - just ( , ) ]
                                                                              Return⋆.cong (initial-bag-cong p₁≈p₃) >>=
                                                                               x  D-cong (p₂≈p₄ x)) 
  D t (♭? p₃) >>= (♭?  p₄)  return⋆ (flatten xs₂) >>= (D t  ♭?  p₄)  ≅⟨ sym $ D.D->>= p₃ p₄ 
  D t (p₃ >>= p₄)                                                        

------------------------------------------------------------------------
-- Soundness

sound :  {k Tok R xs₁ xs₂}
          {p₁ : Parser Tok R xs₁}
          {p₂ : Parser Tok R xs₂} 
        p₁ ∼[ k ]P p₂  p₁ ∼[ k ] p₂
sound = CE.sound  sound′
  where
  sound′ :  {k Tok R xs₁ xs₂}
             {p₁ : Parser Tok R xs₁}
             {p₂ : Parser Tok R xs₂} 
           p₁ ∼[ k ]P p₂  p₁ ∼[ k ]c p₂
  sound′ p₁≈p₂ = initial-bag-cong p₁≈p₂  λ t   sound′ (D-cong p₁≈p₂)