module StructurallyRecursiveDescentParsing.Backend.Simplification where
open import Algebra
open import Coinduction
open import Data.Bool
open import Data.Product
open import Data.Product1 using (∃₁₁; _,_; proj₁₁₁; proj₁₁₂)
open import Data.List as List
private module LM {Tok} = Monoid (List.monoid Tok)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
open import Relation.Binary.PropositionalEquality1 as Eq₁
using (_≡₁_; refl)
open import StructurallyRecursiveDescentParsing.Coinduction
open import StructurallyRecursiveDescentParsing.Parser
open import StructurallyRecursiveDescentParsing.Parser.Semantics
hiding (sound; complete)
open import StructurallyRecursiveDescentParsing.Simplified.Lemmas
private
force : ∀ {Tok R xs} (p : ∞₁ (Parser Tok R xs)) → ∃₁₁ λ p′ → ♭₁ p ≈ p′
force p = (♭₁ p , (λ x∈ → x∈) , λ x∈ → x∈)
cast′ : ∀ {Tok R xs₁ xs₂} →
xs₁ ≡ xs₂ → Parser Tok R xs₁ → Parser Tok R xs₂
cast′ refl p = p
cast⁺ : ∀ {Tok R xs₁ xs₂ x s} {p : Parser Tok R xs₁} →
(eq : xs₁ ≡ xs₂) → x ∈ p · s → x ∈ cast′ eq p · s
cast⁺ refl x∈p = x∈p
cast⁻ : ∀ {Tok R xs₁ xs₂ x s} {p : Parser Tok R xs₁} →
(eq : xs₁ ≡ xs₂) → x ∈ cast′ eq p · s → x ∈ p · s
cast⁻ refl x∈p = x∈p
mutual
simplify₁ : ∀ {Tok R xs} (p : Parser Tok R xs) → ∃₁₁ λ p′ → p ≈ p′
simplify₁ (return x) = (return x , (λ x∈ → x∈) , λ x∈ → x∈)
simplify₁ fail = (fail , (λ ()) , λ ())
simplify₁ token = (token , (λ x∈ → x∈) , λ x∈ → x∈)
simplify₁ (f <$> p) with simplify₁ p
... | (fail , p≈∅) = (fail , (λ {_} → helper) , λ ())
where
helper : f <$> p ⊑ fail
helper (<$> x∈p) with proj₁₁₁ p≈∅ x∈p
... | ()
... | (return x , p≈ε) =
(return (f x) , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : f <$> p ⊑ return (f x)
helper₁ (<$> x∈p) with proj₁₁₁ p≈ε x∈p
... | return = return
helper₂ : return (f x) ⊑ f <$> p
helper₂ return = <$>_ {f = f} (proj₁₁₂ p≈ε return)
... | (p′ , p≈p′) = (f <$> p′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : f <$> p ⊑ f <$> p′
helper₁ (<$> x∈p) = <$> proj₁₁₁ p≈p′ x∈p
helper₂ : f <$> p′ ⊑ f <$> p
helper₂ (<$> x∈p′) = <$> proj₁₁₂ p≈p′ x∈p′
simplify₁ (p₁ ∣ p₂) with simplify₁ p₁ | simplify₁ p₂
simplify₁ (p₁ ∣ p₂) | (fail , p₁≈∅) | (p₂′ , p₂≈p₂′) =
(p₂′ , (λ {_} → helper) , λ x∈ → ∣ʳ [] (proj₁₁₂ p₂≈p₂′ x∈))
where
helper : p₁ ∣ p₂ ⊑ p₂′
helper (∣ʳ .[] x∈p₂) = proj₁₁₁ p₂≈p₂′ x∈p₂
helper (∣ˡ x∈p₁) with proj₁₁₁ p₁≈∅ x∈p₁
... | ()
simplify₁ (p₁ ∣ p₂) | (_>>=_ {f = f} token p₁′ , p₁≈…)
| (token >>= p₂′ , p₂≈…) =
( token >>= (λ t → ♯? (♭? (p₁′ t) ∣ ♭? (p₂′ t)))
, (λ {_} → helper₁) , λ {_} → helper₂
)
where
helper₁ : p₁ ∣ p₂ ⊑ token >>= (λ t → ♯? (♭? (p₁′ t) ∣ ♭? (p₂′ t)))
helper₁ (∣ˡ x∈p₁) with proj₁₁₁ p₁≈… x∈p₁
helper₁ (∣ˡ x∈p₁) | token >>= x∈p₁′ = token >>= ∣ˡ x∈p₁′
helper₁ (∣ʳ .[] x∈p₂) with proj₁₁₁ p₂≈… x∈p₂
helper₁ (∣ʳ .[] x∈p₂) | _>>=_ {x = x} token x∈p₂′ =
token >>= ∣ʳ (f x) x∈p₂′
helper₂ : token >>= (λ t → ♯? (♭? (p₁′ t) ∣ ♭? (p₂′ t))) ⊑ p₁ ∣ p₂
helper₂ (token >>= ∣ˡ y∈p₁′x) = ∣ˡ (proj₁₁₂ p₁≈… (token >>= y∈p₁′x))
helper₂ (token >>= ∣ʳ ._ y∈p₂′x) = ∣ʳ [] (proj₁₁₂ p₂≈… (token >>= y∈p₂′x))
simplify₁ (p₁ ∣ p₂) | (p₁′ , p₁≈p₁′) | (fail , p₂≈∅) =
(cast′ lem p₁′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
lem = sym (proj₂ LM.identity _)
helper₁ : p₁ ∣ p₂ ⊑ cast′ lem p₁′
helper₁ (∣ˡ x∈p₁) = cast⁺ lem (proj₁₁₁ p₁≈p₁′ x∈p₁)
helper₁ (∣ʳ ._ x∈p₂) with proj₁₁₁ p₂≈∅ x∈p₂
... | ()
helper₂ : cast′ lem p₁′ ⊑ p₁ ∣ p₂
helper₂ x∈p₁′ = ∣ˡ (proj₁₁₂ p₁≈p₁′ (cast⁻ lem x∈p₁′))
simplify₁ (_∣_ {xs₁ = xs₁} p₁ p₂) | (p₁′ , p₁≈p₁′) | (p₂′ , p₂≈p₂′) =
(p₁′ ∣ p₂′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : p₁ ∣ p₂ ⊑ p₁′ ∣ p₂′
helper₁ (∣ˡ x∈p₁) = ∣ˡ (proj₁₁₁ p₁≈p₁′ x∈p₁)
helper₁ (∣ʳ .xs₁ x∈p₂) = ∣ʳ xs₁ (proj₁₁₁ p₂≈p₂′ x∈p₂)
helper₂ : p₁′ ∣ p₂′ ⊑ p₁ ∣ p₂
helper₂ (∣ˡ x∈p₁′) = ∣ˡ (proj₁₁₂ p₁≈p₁′ x∈p₁′)
helper₂ (∣ʳ .xs₁ x∈p₂′) = ∣ʳ xs₁ (proj₁₁₂ p₂≈p₂′ x∈p₂′)
simplify₁ (p₁ ⊛ p₂) =
helper _ _ (simplify₁′ p₁) (simplify₁′ p₂) refl refl
where
cast₁ : ∀ {Tok R R₁ R₁′ xs xs′} {ys : List R} →
(R≡ : R₁ ≡₁ R₁′) → xs ≅ xs′ →
∞? (Parser Tok R₁′ xs′) ys →
∞? (Parser Tok R₁ xs ) ys
cast₁ refl refl p = p
helper : ∀ {Tok R₁ R₁′ R₂ fs xs xs′}
(p₁ : ∞? (Parser Tok (R₁ → R₂) fs ) xs)
(p₂ : ∞? (Parser Tok R₁′ xs′) fs) →
(∃₁₁ λ p₁′ → ♭? p₁ ≈ p₁′) →
(∃₁₁ λ p₂′ → ♭? p₂ ≈ p₂′) →
(R≡ : R₁ ≡₁ R₁′) →
(xs≅ : xs ≅ xs′) →
∃₁₁ λ p′ → p₁ ⊛ cast₁ R≡ xs≅ p₂ ≈ p′
helper {xs = xs} p₁ p₂ (fail , p₁≈∅) _ refl refl =
(cast′ lem fail , (λ {_} → helper₁) , λ {_} → helper₂)
where
lem = sym (>>=-∅ xs)
helper₁ : p₁ ⊛ p₂ ⊑ cast′ lem fail
helper₁ (f∈p₁ ⊛ x∈p₂) with proj₁₁₁ p₁≈∅ f∈p₁
... | ()
helper₂ : cast′ lem fail ⊑ p₁ ⊛ p₂
helper₂ x∈∅ with cast⁻ lem x∈∅
... | ()
helper p₁ p₂ _ (fail , p₂≈∅) refl refl =
(fail , (λ {_} → helper₁) , λ ())
where
helper₁ : p₁ ⊛ p₂ ⊑ fail
helper₁ (f∈p₁ ⊛ x∈p₂) with proj₁₁₁ p₂≈∅ x∈p₂
... | ()
helper p₁ p₂ (return f , p₁≈ε) (return x , p₂≈ε) refl refl =
(return (f x) , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : p₁ ⊛ p₂ ⊑ return (f x)
helper₁ (f∈p₁ ⊛ x∈p₂) with proj₁₁₁ p₁≈ε f∈p₁ | proj₁₁₁ p₂≈ε x∈p₂
... | return | return = return
helper₂ : return (f x) ⊑ p₁ ⊛ p₂
helper₂ return = proj₁₁₂ p₁≈ε return ⊛ proj₁₁₂ p₂≈ε return
helper p₁ p₂ (p₁′ , p₁≈p₁′) (p₂′ , p₂≈p₂′) R≡ xs≅ =
helper′ p₁ p₂ (p₁′ , p₁≈p₁′) (p₂′ , p₂≈p₂′) R≡ xs≅
where
helper′ : ∀ {Tok R₁ R₁′ R₂ fs xs xs′}
(p₁ : ∞? (Parser Tok (R₁ → R₂) fs ) xs)
(p₂ : ∞? (Parser Tok R₁′ xs′) fs) →
(∃₁₁ λ p₁′ → ♭? p₁ ≈ p₁′) →
(∃₁₁ λ p₂′ → ♭? p₂ ≈ p₂′) →
(R≡ : R₁ ≡₁ R₁′) →
(xs≅ : xs ≅ xs′) →
∃₁₁ λ p′ → p₁ ⊛ cast₁ R≡ xs≅ p₂ ≈ p′
helper′ {fs = fs} {xs} p₁ p₂ (p₁′ , p₁≈p₁′) (p₂′ , p₂≈p₂′)
refl refl =
( ♯? p₁′ ⊛ ♯? p₂′
, (λ {_} → helper₁) , λ {_} → helper₂
)
where
helper₁ : p₁ ⊛ p₂ ⊑ ♯? p₁′ ⊛ ♯? p₂′
helper₁ (f∈p₁ ⊛ x∈p₂) =
cast∈ refl (Eq₁.sym (♭?♯? xs)) refl (proj₁₁₁ p₁≈p₁′ f∈p₁) ⊛
cast∈ refl (Eq₁.sym (♭?♯? fs)) refl (proj₁₁₁ p₂≈p₂′ x∈p₂)
helper₂ : ♯? p₁′ ⊛ ♯? p₂′ ⊑ p₁ ⊛ p₂
helper₂ (f∈p₁′ ⊛ x∈p₂′) =
proj₁₁₂ p₁≈p₁′ (cast∈ refl (♭?♯? xs) refl f∈p₁′) ⊛
proj₁₁₂ p₂≈p₂′ (cast∈ refl (♭?♯? fs) refl x∈p₂′)
simplify₁ (p₁ >>= p₂) with simplify₁ p₁
simplify₁ (p₁ >>= p₂) | (fail , p₁≈∅) = (fail , (λ {_} → helper) , λ ())
where
helper : p₁ >>= p₂ ⊑ fail
helper (x∈p₁ >>= y∈p₂x) with proj₁₁₁ p₁≈∅ x∈p₁
... | ()
simplify₁ (p₁ >>= p₂) | (return x , p₁≈ε) with simplify₁′ (p₂ x)
simplify₁ (p₁ >>= p₂) | (return x , p₁≈ε) | (p₂′ , p₂x≈p₂′) =
(cast′ lem p₂′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
lem = sym (proj₂ LM.identity _)
helper₁ : p₁ >>= p₂ ⊑ cast′ lem p₂′
helper₁ (_>>=_ {y = y} {s₂ = s₂} x∈p₁ y∈p₂x) =
cast⁺ lem (helper (proj₁₁₁ p₁≈ε x∈p₁) y∈p₂x)
where
helper : ∀ {x′ s₁} → x′ ∈ return x · s₁ → y ∈ ♭? (p₂ x′) · s₂ →
y ∈ p₂′ · s₁ ++ s₂
helper return x∈p₂ = proj₁₁₁ p₂x≈p₂′ x∈p₂
helper₂ : cast′ lem p₂′ ⊑ p₁ >>= p₂
helper₂ y∈p₂′ =
_>>=_ {x = x} {p₂ = p₂} (proj₁₁₂ p₁≈ε (return {x = x}))
(proj₁₁₂ p₂x≈p₂′ (cast⁻ lem y∈p₂′))
simplify₁ (p₁ >>= p₂) | (p₁′ , p₁≈p₁′) =
(p₁′ >>= p₂ , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : p₁ >>= p₂ ⊑ p₁′ >>= p₂
helper₁ (x∈p₁ >>= y∈p₂x) = proj₁₁₁ p₁≈p₁′ x∈p₁ >>= y∈p₂x
helper₂ : p₁′ >>= p₂ ⊑ p₁ >>= p₂
helper₂ (x∈p₁ >>= y∈p₂x) = proj₁₁₂ p₁≈p₁′ x∈p₁ >>= y∈p₂x
simplify₁ (p₁ >>=! p₂) with force p₁
simplify₁ (p₁ >>=! p₂) | (fail , p₁≈∅) = (fail , (λ {_} → helper) , λ ())
where
helper : p₁ >>=! p₂ ⊑ fail
helper (x∈p₁ >>=! y∈p₂x) with proj₁₁₁ p₁≈∅ x∈p₁
... | ()
simplify₁ (p₁ >>=! p₂) | (return x , p₁≈ε) with simplify₁′ (p₂ x)
simplify₁ (p₁ >>=! p₂) | (return x , p₁≈ε) | (p₂′ , p₂x≈p₂′) =
(cast′ lem p₂′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
lem = sym (proj₂ LM.identity _)
helper₁ : p₁ >>=! p₂ ⊑ cast′ lem p₂′
helper₁ (_>>=!_ {y = y} {s₂ = s₂} x∈p₁ y∈p₂x) =
cast⁺ lem (helper (proj₁₁₁ p₁≈ε x∈p₁) y∈p₂x)
where
helper : ∀ {x′ s₁} → x′ ∈ return x · s₁ → y ∈ ♭? (p₂ x′) · s₂ →
y ∈ p₂′ · s₁ ++ s₂
helper return x∈p₂ = proj₁₁₁ p₂x≈p₂′ x∈p₂
helper₂ : cast′ lem p₂′ ⊑ p₁ >>=! p₂
helper₂ y∈p₂′ =
_>>=!_ {x = x} {p₂ = p₂} (proj₁₁₂ p₁≈ε (return {x = x}))
(proj₁₁₂ p₂x≈p₂′ (cast⁻ lem y∈p₂′))
simplify₁ (p₁ >>=! p₂) | (p₁′ , p₁≈p₁′) =
(♯₁ p₁′ >>=! p₂ , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : p₁ >>=! p₂ ⊑ _ >>=! p₂
helper₁ (x∈p₁ >>=! y∈p₂x) = proj₁₁₁ p₁≈p₁′ x∈p₁ >>=! y∈p₂x
helper₂ : _ >>=! p₂ ⊑ p₁ >>=! p₂
helper₂ (x∈p₁ >>=! y∈p₂x) = proj₁₁₂ p₁≈p₁′ x∈p₁ >>=! y∈p₂x
simplify₁ (nonempty p) with simplify₁ p
simplify₁ (nonempty p) | (fail , p≈∅) =
(fail , (λ {_} → helper) , λ ())
where
helper : nonempty p ⊑ fail
helper (nonempty x∈p) with proj₁₁₁ p≈∅ x∈p
... | ()
simplify₁ (nonempty p) | (p′ , p≈p′) =
(nonempty p′ , (λ {_} → helper₁) , λ {_} → helper₂)
where
helper₁ : nonempty p ⊑ nonempty p′
helper₁ (nonempty x∈p) = nonempty (proj₁₁₁ p≈p′ x∈p)
helper₂ : nonempty p′ ⊑ nonempty p
helper₂ (nonempty x∈p′) = nonempty (proj₁₁₂ p≈p′ x∈p′)
simplify₁ (cast refl p) with simplify₁ p
simplify₁ (cast refl p) | (p′ , p≈p′) =
(p′ , (λ {_} → helper) , λ x∈ → cast (proj₁₁₂ p≈p′ x∈))
where
helper : cast refl p ⊑ p′
helper (cast x∈p) = proj₁₁₁ p≈p′ x∈p
simplify₁′ : ∀ {Tok R R′ xs} {ys : List R′}
(p : ∞? (Parser Tok R xs) ys) → ∃₁₁ λ p′ → ♭? p ≈ p′
simplify₁′ ⟪ p ⟫ = (♭₁ p , (λ x∈ → x∈) , λ x∈ → x∈)
simplify₁′ ⟨ p ⟩ = simplify₁ p
simplify : ∀ {Tok R xs} → Parser Tok R xs → Parser Tok R xs
simplify p = proj₁₁₁ (simplify₁ p)
sound : ∀ {Tok R xs} {p : Parser Tok R xs} → simplify p ⊑ p
sound = proj₁₁₂ (proj₁₁₂ (simplify₁ _))
complete : ∀ {Tok R xs} {p : Parser Tok R xs} → p ⊑ simplify p
complete = proj₁₁₁ (proj₁₁₂ (simplify₁ _))