------------------------------------------------------------------------
-- This module proves that the parser combinators correspond exactly
-- to functions of type List Tok → List R (if bag equality is used for
-- the lists of results)
------------------------------------------------------------------------

module TotalParserCombinators.ExpressiveStrength where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.List as List
open import Data.List.Membership.Propositional
import Data.List.Properties as ListProp
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.Relation.Unary.Any
open import Data.List.Reverse
open import Data.Product
open import Function
import Function.Related.Propositional as Related
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality
  using (_≅_; _≇_; refl)
open import Relation.Nullary

open Related using (SK-sym)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S
  hiding (_≅_; _∼[_]_; token)
open import TotalParserCombinators.Lib
private
  open module Tok = Token Bool _≟_ using (tok)
open import TotalParserCombinators.BreadthFirst as Backend
  using (parse)

------------------------------------------------------------------------
-- Expressive strength

-- One direction of the correspondence has already been established:
-- For every parser there is an equivalent function.

parser⇒fun : ∀ {R xs} (p : Parser Bool R xs) {x s} →
             x ∈ p · s ↔ x ∈ parse p s
parser⇒fun p = Backend.parse-correct

-- For every function there is a corresponding parser.

module Monadic where

  -- The parser.

  grammar : ∀ {Tok R} (f : List Tok → List R) → Parser Tok R (f [])
  grammar f = token >>= (λ t → ♯ grammar (f ∘ _∷_ t))
            ∣ return⋆ (f [])

  -- Correctness proof.

  grammar-correct : ∀ {Tok R} (f : List Tok → List R) {x s} →
                    x ∈ grammar f · s ↔ x ∈ f s
  grammar-correct f {s = s} =
    mk↔ {from = complete f s}
      ( (λ { P.refl → sound∘complete f s _ })
      , (λ { P.refl → complete∘sound f _ })
      )
    where
    sound : ∀ {Tok R x s} (f : List Tok → List R) →
            x ∈ grammar f · s → x ∈ f s
    sound f (∣-right ._ x∈) with Return⋆.sound (f []) x∈
    ... | (refl , x∈′) = x∈′
    sound f (∣-left (S.token {t} >>= x∈)) = sound (f ∘ _∷_ t) x∈

    complete : ∀ {Tok R x} (f : List Tok → List R) s →
               x ∈ f s → x ∈ grammar f · s
    complete f []      x∈ = ∣-right [] (Return⋆.complete x∈)
    complete f (t ∷ s) x∈ =
      ∣-left ([ ○ - ◌ ] S.token >>= complete (f ∘ _∷_ t) s x∈)

    complete∘sound : ∀ {Tok R x s} (f : List Tok → List R)
                     (x∈pf : x ∈ grammar f · s) →
                     complete f s (sound f x∈pf) ≡ x∈pf
    complete∘sound f (∣-left (S.token {t} >>= x∈))
      rewrite complete∘sound (f ∘ _∷_ t) x∈ = refl
    complete∘sound f (∣-right .[] x∈)
      with Return⋆.sound (f []) x∈ | Return⋆.complete∘sound (f []) x∈
    complete∘sound f (∣-right .[] .(Return⋆.complete x∈f[]))
      | (refl , x∈f[]) | refl = refl

    sound∘complete : ∀ {Tok R x} (f : List Tok → List R) s
                     (x∈fs : x ∈ f s) →
                     sound f (complete f s x∈fs) ≡ x∈fs
    sound∘complete       f (t ∷ s) x∈ = sound∘complete (f ∘ _∷_ t) s x∈
    sound∘complete {Tok} f []      x∈
      with Return⋆.sound {Tok = Tok} (f []) (Return⋆.complete x∈)
         | Return⋆.sound∘complete {Tok = Tok} x∈
    ... | (refl , .x∈) | refl = refl

  -- A corollary.

  maximally-expressive :
    ∀ {Tok R} (f : List Tok → List R) {s} →
    parse (grammar f) s ∼[ bag ] f s
  maximally-expressive f {s} {x} =
    (x ∈ parse (grammar f) s)  ↔⟨ SK-sym Backend.parse-correct ⟩
    x ∈ grammar f · s          ↔⟨ grammar-correct f ⟩
    x ∈ f s                    ∎
    where open Related.EquationalReasoning

-- If the token type is finite (in this case Bool), then the result
-- above can be established without the use of bind (_>>=_). (The
-- definition of tok uses bind, but if bind were removed it would be
-- reasonable to either add tok as a primitive combinator, or make it
-- possible to define tok using other combinators.)

module Applicative where

  -- A helper function.

  specialise : {A B : Set} → (List A → B) → A → (List A → B)
  specialise f x = λ xs → f (xs ∷ʳ x)

  -- The parser.

  grammar : ∀ {R} (f : List Bool → List R) → Parser Bool R (f [])
  grammar f =
      ♯ (const <$> grammar (specialise f true )) ⊛ tok true
    ∣ ♯ (const <$> grammar (specialise f false)) ⊛ tok false
    ∣ return⋆ (f [])

  -- Correctness proof.

  grammar-correct : ∀ {R} (f : List Bool → List R) {x s} →
                    x ∈ grammar f · s ↔ x ∈ f s
  grammar-correct {R} f {s = s} =
    mk↔ {from = complete f (reverseView s)}
      ( (λ { P.refl → sound∘complete f (reverseView s) _ })
      , (λ { P.refl → complete∘sound f (reverseView s) _ _ refl refl })
      )
    where
    sound : ∀ {x : R} {s} f → x ∈ grammar f · s → x ∈ f s
    sound f (∣-right ._ x∈) with Return⋆.sound (f []) x∈
    ... | (refl , x∈′) = x∈′
    sound f (∣-left (∣-left (<$> x∈ ⊛ t∈))) with Tok.sound true t∈
    ... | (refl , refl) = sound (specialise f true ) x∈
    sound f (∣-left (∣-right ._ (<$> x∈ ⊛ t∈))) with Tok.sound false t∈
    ... | (refl , refl) = sound (specialise f false) x∈

    complete : ∀ {x : R} {s} f → Reverse s →
               x ∈ f s → x ∈ grammar f · s
    complete f []                 x∈ = ∣-right [] (Return⋆.complete x∈)
    complete f (bs ∶ rs ∶ʳ true ) x∈ =
      ∣-left {xs₁ = []} (∣-left (
        [ ◌ - ○ ] <$> complete (specialise f true ) rs x∈ ⊛ Tok.complete))
    complete f (bs ∶ rs ∶ʳ false) x∈ =
      ∣-left (∣-right [] (
        [ ◌ - ○ ] <$> complete (specialise f false) rs x∈ ⊛ Tok.complete))

    sound∘complete : ∀ {x : R} {s} f (rs : Reverse s) (x∈fs : x ∈ f s) →
                     sound f (complete f rs x∈fs) ≡ x∈fs
    sound∘complete f [] x∈
      rewrite Return⋆.sound∘complete {Tok = Bool} x∈ = refl
    sound∘complete f (bs ∶ rs ∶ʳ true) x∈ =
      sound∘complete (specialise f true) rs x∈
    sound∘complete f (bs ∶ rs ∶ʳ false) x∈ =
      sound∘complete (specialise f false) rs x∈

    complete∘sound : ∀ {x : R} {s s′ : List Bool}
                     f (rs : Reverse s) (rs′ : Reverse s′)
                     (x∈pf : x ∈ grammar f · s) → s ≡ s′ → rs ≅ rs′ →
                     complete f rs (sound f x∈pf) ≡ x∈pf

    complete∘sound f rs rs′ (∣-right ._ x∈) s≡ rs≅
      with Return⋆.sound (f []) x∈
         | Return⋆.complete∘sound (f []) x∈
    complete∘sound f ._ []                 (∣-right ._ .(Return⋆.complete x∈′)) refl refl | (refl , x∈′) | refl = refl
    complete∘sound f _  ([]      ∶ _ ∶ʳ _) (∣-right ._ .(Return⋆.complete x∈′)) ()   _    | (refl , x∈′) | refl
    complete∘sound f _  ((_ ∷ _) ∶ _ ∶ʳ _) (∣-right ._ .(Return⋆.complete x∈′)) ()   _    | (refl , x∈′) | refl

    complete∘sound f rs rs′ (∣-left (∣-left (<$> x∈ ⊛ t∈))) s≡ rs≅ with Tok.sound true t∈
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₁ $ ListProp.∷ʳ-injective bs bs′ s≡
    complete∘sound f rs (.bs ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl with s≡ | rs≅
    complete∘sound f ._ (.bs ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl | refl | refl
      rewrite complete∘sound (specialise f true) rs′ rs′ x∈ refl refl
            | Tok.η t∈ = refl
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ false) (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₂ $ ListProp.∷ʳ-injective bs bs′ s≡
    ... | ()
    complete∘sound f rs []                   (∣-left (∣-left (_⊛_ {s₁ = []}    (<$> x∈) t∈))) () _   | (refl , refl)
    complete∘sound f rs []                   (∣-left (∣-left (_⊛_ {s₁ = _ ∷ _} (<$> x∈) t∈))) () _   | (refl , refl)

    complete∘sound f rs rs′ (∣-left (∣-right ._ (<$> x∈ ⊛ t∈))) s≡ rs≅ with Tok.sound false t∈
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₁ $ ListProp.∷ʳ-injective bs bs′ s≡
    complete∘sound f rs (.bs ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl with s≡ | rs≅
    complete∘sound f ._ (.bs ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl | refl | refl
      rewrite complete∘sound (specialise f false) rs′ rs′ x∈ refl refl
            | Tok.η t∈ = refl
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ true)  (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₂ $ ListProp.∷ʳ-injective bs bs′ s≡
    ... | ()
    complete∘sound f rs []                   (∣-left (∣-right ._ (_⊛_ {s₁ = []} (<$> x∈) t∈))) () _   | (refl , refl)
    complete∘sound f rs []                (∣-left (∣-right ._ (_⊛_ {s₁ = _ ∷ _} (<$> x∈) t∈))) () _   | (refl , refl)

  -- A corollary.

  maximally-expressive :
    ∀ {R} (f : List Bool → List R) {s} →
    parse (grammar f) s ∼[ bag ] f s
  maximally-expressive f {s} {x} =
    (x ∈ parse (grammar f) s)  ↔⟨ SK-sym Backend.parse-correct ⟩
    x ∈ grammar f · s          ↔⟨ grammar-correct f ⟩
    x ∈ f s                    ∎
    where open Related.EquationalReasoning