module TotalParserCombinators.ExpressiveStrength where
open import Coinduction
open import Data.Bool
open import Function
open import Function.Inverse as Inv using (_⇿_)
open import Data.List as List
open import Data.List.Any
open Membership-≡
import Data.List.Properties as ListProp
open import Data.List.Reverse
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality
using (_≅_; _≇_; refl)
open import Relation.Nullary
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)
parser⇒fun : ∀ {R xs} (p : Parser Bool R xs) {x s} →
x ∈ p · s ⇿ x ∈ parse p s
parser⇒fun p = Backend.correct
module Monadic where
grammar : ∀ {Tok R} (f : List Tok → List R) → Parser Tok R (f [])
grammar f = token >>= (λ t → ♯ grammar (f ∘ _∷_ t))
∣ return⋆ (f [])
grammar-correct : ∀ {Tok R} (f : List Tok → List R) {x s} →
x ∈ grammar f · s ⇿ x ∈ f s
grammar-correct f {s = s} = record
{ to = P.→-to-⟶ (sound f)
; from = P.→-to-⟶ (complete f s)
; inverse-of = record
{ left-inverse-of = complete∘sound f
; right-inverse-of = sound∘complete f s
}
}
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
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) ⇿⟨ sym Backend.correct ⟩
x ∈ grammar f · s ⇿⟨ grammar-correct f ⟩
x ∈ f s ∎
where open Inv.EquationalReasoning
module Applicative where
specialise : {A B : Set} → (List A → B) → A → (List A → B)
specialise f x = λ xs → f (xs ∷ʳ x)
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 [])
grammar-correct : ∀ {R} (f : List Bool → List R) {x s} →
x ∈ grammar f · s ⇿ x ∈ f s
grammar-correct {R} f {s = s} = record
{ to = P.→-to-⟶ (sound f)
; from = P.→-to-⟶ (complete f (reverseView s))
; inverse-of = record
{ right-inverse-of = sound∘complete f (reverseView s)
; left-inverse-of = λ x∈ →
complete∘sound f (reverseView s) _ x∈ 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)
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) ⇿⟨ sym Backend.correct ⟩
x ∈ grammar f · s ⇿⟨ grammar-correct f ⟩
x ∈ f s ∎
where open Inv.EquationalReasoning