module StructurallyRecursiveDescentParsing.Simplified.Semantics where
open import Algebra
open import Coinduction
open import Data.Bool
open import Data.List as List
private
module LM {Tok} = Monoid (List.monoid Tok)
import Data.Product as Prod
open import Data.Product1 as Prod1 renaming (∃₀₁ to ∃; map₀₁ to map)
open import Data.Function
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality1 using (_≡₁_; refl)
open import StructurallyRecursiveDescentParsing.Coinduction
open import StructurallyRecursiveDescentParsing.Simplified
import StructurallyRecursiveDescentParsing.Parser.Semantics
as Semantics
open Semantics using (return; token; ∣ˡ; ∣ʳ; _>>=_; cast)
renaming (_∈_·_ to _∈′_·_)
infixl 10 _?>>=_ _!>>=_
infix 4 _∈_·_
data _∈_·_ {Tok} : ∀ {R e} → R → Parser Tok e R → List Tok → Set1 where
return : ∀ {R} {x : R} → x ∈ return x · []
token : ∀ {x} → x ∈ token · [ x ]
∣ˡ : ∀ {R x e₁ e₂ s} {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₁ : x ∈ p₁ · s) → x ∈ p₁ ∣ p₂ · s
∣ʳ : ∀ {R x e₂ s} e₁ {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₂ : x ∈ p₂ · s) → x ∈ p₁ ∣ p₂ · s
_?>>=_ : ∀ {R₁ R₂ x y e₂ s₁ s₂}
{p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
(x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ p₂ x · s₂) →
y ∈ p₁ ?>>= p₂ · s₁ ++ s₂
_!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s₁ s₂}
{p₁ : Parser Tok false R₁}
{p₂ : (x : R₁) → ∞₁ (Parser Tok (e₂ x) R₂)}
(x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ ♭₁ (p₂ x) · s₂) →
y ∈ p₁ !>>= p₂ · s₁ ++ s₂
sound : ∀ {Tok e R} {p : Parser Tok e R} {x s} →
x ∈ p · s → x ∈′ ⟦ p ⟧ · s
sound return = return
sound token = token
sound (∣ˡ x∈p₁) = cast (∣ˡ (sound x∈p₁))
sound (∣ʳ _ {p₁} x∈p₂) = cast (∣ʳ (initial p₁) (sound x∈p₂))
sound (_?>>=_ {p₂ = p₂}
x∈p₁ y∈p₂x) = cast (_>>=_ {p₂ = λ x → ⟨ ⟦ p₂ x ⟧ ⟩}
(sound x∈p₁) (sound y∈p₂x))
sound (x∈p₁ !>>= y∈p₂x) = sound x∈p₁ >>= sound y∈p₂x
complete : ∀ {Tok e R} (p : Parser Tok e R) {x s} →
x ∈′ ⟦ p ⟧ · s → x ∈ p · s
complete (return x) return = return
complete fail ()
complete token token = token
complete (p₁ ∣ p₂) (cast (∣ˡ x∈p₁)) = ∣ˡ (complete p₁ x∈p₁)
complete (_∣_ {e₁} p₁ p₂) (cast (∣ʳ ._ x∈p₂)) = ∣ʳ e₁ (complete p₂ x∈p₂)
complete (p₁ ?>>= p₂) (cast
(x∈p₁ >>= y∈p₂x)) = complete p₁ x∈p₁ ?>>=
complete (p₂ _) y∈p₂x
complete (p₁ !>>= p₂) (x∈p₁ >>= y∈p₂x) = complete p₁ x∈p₁ !>>=
complete (♭₁ (p₂ _)) y∈p₂x
cast∈ : ∀ {Tok e R} {p p′ : Parser Tok e R} {x x′ s s′} →
x ≡ x′ → p ≡₁ p′ → s ≡ s′ → x ∈ p · s → x′ ∈ p′ · s′
cast∈ refl refl refl x∈ = x∈
infix 4 _⊕_∈_·_
data _⊕_∈_·_ {Tok} : ∀ {R e} → R → List Tok →
Parser Tok e R → List Tok → Set1 where
return : ∀ {R} {x : R} {s} → x ⊕ s ∈ return x · s
token : ∀ {x s} → x ⊕ s ∈ token · x ∷ s
∣ˡ : ∀ {R x e₁ e₂ s s₁}
{p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
∣ʳ : ∀ {R x e₂ s s₁} e₁
{p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
(x∈p₂ : x ⊕ s₁ ∈ p₂ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
_?>>=_ : ∀ {R₁ R₂ x y e₂ s s₁ s₂}
{p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ p₂ x · s₁) →
y ⊕ s₂ ∈ p₁ ?>>= p₂ · s
_!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s s₁ s₂}
{p₁ : Parser Tok false R₁}
{p₂ : (x : R₁) → ∞₁ (Parser Tok (e₂ x) R₂)}
(x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ ♭₁ (p₂ x) · s₁) →
y ⊕ s₂ ∈ p₁ !>>= p₂ · s
⊕-sound′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
x ⊕ s₂ ∈ p · s → ∃ λ s₁ → Σ₀₁ (s ≡ s₁ ++ s₂) λ _ → x ∈ p · s₁
⊕-sound′ return = ([] , refl , return)
⊕-sound′ {x = x} token = ([ x ] , refl , token)
⊕-sound′ (∣ˡ x∈p₁) with ⊕-sound′ x∈p₁
⊕-sound′ (∣ˡ x∈p₁) | (s₁ , refl , x∈p₁′) = (s₁ , refl , ∣ˡ x∈p₁′)
⊕-sound′ (∣ʳ e₁ x∈p₁) with ⊕-sound′ x∈p₁
⊕-sound′ (∣ʳ e₁ x∈p₁) | (s₁ , refl , x∈p₁′) = (s₁ , refl , ∣ʳ e₁ x∈p₁′)
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) | (s₁ , refl , x∈p₁′) | (s₂ , refl , y∈p₂x′) =
(s₁ ++ s₂ , sym (LM.assoc s₁ s₂ _)
, x∈p₁′ ?>>= y∈p₂x′)
⊕-sound′ (x∈p₁ !>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ !>>= y∈p₂x) | (s₁ , refl , x∈p₁′) | (s₂ , refl , y∈p₂x′) =
(s₁ ++ s₂ , sym (LM.assoc s₁ s₂ _)
, x∈p₁′ !>>= y∈p₂x′)
⊕-sound : ∀ {Tok R e x s} {p : Parser Tok e R} →
x ⊕ [] ∈ p · s → x ∈ p · s
⊕-sound x∈p with ⊕-sound′ x∈p
⊕-sound x∈p | (s , refl , x∈p′) with s ++ [] | Prod.proj₂ LM.identity s
⊕-sound x∈p | (s , refl , x∈p′) | .s | refl = x∈p′
extend : ∀ {Tok R e x s s′ s″} {p : Parser Tok e R} →
x ⊕ s′ ∈ p · s → x ⊕ s′ ++ s″ ∈ p · s ++ s″
extend return = return
extend token = token
extend (∣ˡ x∈p₁) = ∣ˡ (extend x∈p₁)
extend (∣ʳ e₁ x∈p₂) = ∣ʳ e₁ (extend x∈p₂)
extend (x∈p₁ ?>>= y∈p₂x) = extend x∈p₁ ?>>= extend y∈p₂x
extend (x∈p₁ !>>= y∈p₂x) = extend x∈p₁ !>>= extend y∈p₂x
⊕-complete : ∀ {Tok R e x s} {p : Parser Tok e R} →
x ∈ p · s → x ⊕ [] ∈ p · s
⊕-complete return = return
⊕-complete token = token
⊕-complete (∣ˡ x∈p₁) = ∣ˡ (⊕-complete x∈p₁)
⊕-complete (∣ʳ e₁ x∈p₂) = ∣ʳ e₁ (⊕-complete x∈p₂)
⊕-complete (x∈p₁ ?>>= y∈p₂x) = extend (⊕-complete x∈p₁) ?>>=
⊕-complete y∈p₂x
⊕-complete (x∈p₁ !>>= y∈p₂x) = extend (⊕-complete x∈p₁) !>>=
⊕-complete y∈p₂x
⊕-complete′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
(∃ λ s₁ → Σ₀₁ (s ≡ s₁ ++ s₂) λ _ → x ∈ p · s₁) →
x ⊕ s₂ ∈ p · s
⊕-complete′ (s₁ , refl , x∈p) = extend (⊕-complete x∈p)