module TotalParserCombinators.InitialSet where
open import Data.List
open import Data.List.Any as Any
open import Data.List.Any.Membership
open import Data.List.Any.Properties
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_⇿_)
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality as H
using (refl) renaming (_≅_ to _≅′_)
open Any.Membership-≡ using (_∈_) renaming (_≈[_]_ to _List-≈[_]_)
open Inv.Inverse
import TotalParserCombinators.Applicative as ⊛
open import TotalParserCombinators.Coinduction
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
mutual
complete : ∀ {Tok R xs x} {p : Parser Tok R xs} →
x ∈ p · [] → x ∈ xs
complete x∈p = complete′ x∈p refl
private
complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
x ∈ p · s → s ≡ [] → x ∈ xs
complete′ return refl = to return⇿ ⟨$⟩ refl
complete′ (∣ˡ x∈p₁) refl = to ++⇿ ⟨$⟩ inj₁ (complete x∈p₁)
complete′ (∣ʳ xs₁ x∈p₂) refl = to (++⇿ {xs = xs₁}) ⟨$⟩ inj₂ (complete x∈p₂)
complete′ (<$> x∈p) refl = to map-∈⇿ ⟨$⟩ (_ , complete x∈p , refl)
complete′ (_⊛_ {s₁ = []} {fs = fs} f∈p₁ x∈p₂) refl = to ⊛.⇿ ⟨$⟩ (_ , _ , complete f∈p₁ , complete x∈p₂ , refl)
complete′ (_>>=_ {s₁ = []} {xs = _ ∷ _} {f} x∈p₁ y∈p₂x) refl = to (>>=-∈⇿ {f = f}) ⟨$⟩ (_ , complete x∈p₁ , complete y∈p₂x)
complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p) refl = to xs₁≈xs₂ ⟨$⟩ complete x∈p
complete′ (_>>=_ {s₁ = []} {xs = []} x∈p₁ y∈p₂x) refl with complete x∈p₁
... | ()
complete′ (_>>=!_ {s₁ = []} x∈p₁ y∈p₂x) refl with complete y∈p₂x
... | ()
complete′ token ()
complete′ (_⊛_ {s₁ = _ ∷ _} _ _) ()
complete′ (_>>=_ {s₁ = _ ∷ _} _ _) ()
complete′ (_>>=!_ {s₁ = _ ∷ _} _ _) ()
complete′ (nonempty _) ()
mutual
sound : ∀ {Tok R xs x} (p : Parser Tok R xs) →
x ∈ xs → x ∈ p · []
sound (return x) (here refl) = return
sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs with from (++⇿ {xs = xs₁}) ⟨$⟩ x∈xs
... | inj₁ x∈xs₁ = ∣ˡ (sound p₁ x∈xs₁)
... | inj₂ x∈xs₂ = ∣ʳ xs₁ (sound p₂ x∈xs₂)
sound (_<$>_ {xs = xs} f p) x∈xs with from (map-∈⇿ {xs = xs}) ⟨$⟩ x∈xs
... | (y , y∈xs , refl) = <$> sound p y∈xs
sound (_⊛_ {fs = fs} {x ∷ xs} ⟨ p₁ ⟩ p₂) y∈ys
with from (⊛.⇿ {fs = fs} {xs = x ∷ xs}) ⟨$⟩ y∈ys
sound (_⊛_ {xs = x ∷ xs} ⟨ p₁ ⟩ ⟪ p₂ ⟫) y∈ys | (f′ , x′ , () , x′∈x∷xs , refl)
sound (_⊛_ {xs = x ∷ xs} ⟨ p₁ ⟩ ⟨ p₂ ⟩) y∈ys | (f′ , x′ , f′∈fs , x′∈x∷xs , refl) =
sound p₁ f′∈fs ⊛ sound p₂ x′∈x∷xs
sound (_>>=_ {xs = zs} {f} p₁ p₂) y∈ys
with from (>>=-∈⇿ {xs = zs} {f = f}) ⟨$⟩ y∈ys
... | (x , x∈zs , y∈fx) =
_>>=_ {f = f} (sound p₁ x∈zs) (sound′ (p₂ x) x∈zs y∈fx)
sound (cast xs₁≈xs₂ p) x∈xs = cast (sound p (from xs₁≈xs₂ ⟨$⟩ x∈xs))
sound (return _) (there ())
sound fail ()
sound token ()
sound (⟪ _ ⟫ ⊛ _) ()
sound (_ >>=! _) ()
sound (nonempty _) ()
private
sound′ : ∀ {Tok R₁ R₂ x y xs} {zs : List R₁}
(p : ∞? (Parser Tok R₂ xs) zs) →
x ∈ zs → y ∈ xs → y ∈ ♭? p · []
sound′ ⟨ p ⟩ _ = sound p
sound′ ⟪ p ⟫ ()
mutual
sound∘complete : ∀ {Tok R xs x} {p : Parser Tok R xs}
(x∈p : x ∈ p · []) →
sound p (complete x∈p) ≡ x∈p
sound∘complete x∈p = H.≅-to-≡ (sound∘complete′ x∈p refl)
private
sound∘complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs}
(x∈p : x ∈ p · s) (s≡[] : s ≡ []) →
sound p (complete′ x∈p s≡[]) ≅′ x∈p
sound∘complete′ return refl = refl
sound∘complete′ (∣ˡ {xs₁ = xs₁} {xs₂ = xs₂} x∈p₁) refl rewrite left-inverse-of (++⇿ {xs = xs₁} {ys = xs₂}) (inj₁ (complete x∈p₁)) =
H.cong ((_ → _ ∈ _ · _) ∶ ∣ˡ) (sound∘complete′ x∈p₁ refl)
sound∘complete′ (∣ʳ xs₁ x∈p₂) refl rewrite left-inverse-of (++⇿ {xs = xs₁}) (inj₂ (complete x∈p₂)) =
H.cong ((_ → _ ∈ _ · _) ∶ ∣ʳ xs₁) (sound∘complete′ x∈p₂ refl)
sound∘complete′ (<$>_ {f = f} x∈p) refl rewrite left-inverse-of (map-∈⇿ {f = f}) (_ , complete x∈p , refl) =
H.cong ((_ → _ ∈ _ · _) ∶ <$>_) (sound∘complete′ x∈p refl)
sound∘complete′ (_⊛_ {s₁ = []} {fs = fs} {xs = x ∷ xs} {p₁ = ⟨ p₁ ⟩} f∈p₁ x∈p₂) refl
with complete f∈p₁ | complete x∈p₂
| from (⊛.⇿ {fs = fs} {xs = x ∷ xs}) ⟨$⟩
(to ⊛.⇿ ⟨$⟩ (_ , _ , complete f∈p₁ , complete x∈p₂ , refl))
| left-inverse-of ⊛.⇿ (_ , _ , complete f∈p₁ , complete x∈p₂ , refl)
| sound∘complete f∈p₁ | sound∘complete x∈p₂
sound∘complete′ (_⊛_ {s₁ = []} {fs = []} {xs = _ ∷ _} {p₁ = ⟨ _ ⟩} {p₂ = ⟪ _ ⟫} _ _) refl | () | _ | _ | _ | _ | _
sound∘complete′ (_⊛_ {s₁ = []} {fs = f ∷ fs} {xs = x ∷ xs} {p₁ = ⟨ p₁ ⟩} {p₂ = ⟨ p₂ ⟩}
.(sound p₁ ∈f∷fs) .(sound p₂ ∈x∷xs)) refl
| ∈f∷fs | ∈x∷xs | ._ | refl | refl | refl = refl
sound∘complete′ (_>>=_ {x = x} {y = y} {s₁ = []} {xs = _ ∷ _} {f} {p₁ = p₁} {p₂ = p₂} x∈p₁ y∈p₂x) refl
rewrite left-inverse-of (>>=-∈⇿ {f = f}) (_ , complete x∈p₁ , complete y∈p₂x)
with sound p₁ (complete x∈p₁)
| sound∘complete x∈p₁
| sound′ (p₂ x) (complete x∈p₁) (complete y∈p₂x)
| helper (p₂ x) (complete x∈p₁) y∈p₂x
where
helper : ∀ {Tok R₁ R₂ x y ys} {xs : List R₁}
(p : ∞? (Parser Tok R₂ ys) xs) →
(x∈xs : x ∈ xs) (y∈p : y ∈ ♭? p · []) →
sound′ p x∈xs (complete y∈p) ≡ y∈p
helper ⟪ p ⟫ () _
helper ⟨ p ⟩ _ y∈p = sound∘complete y∈p
... | ._ | refl | ._ | refl = refl
sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p) refl with complete x∈p | sound∘complete x∈p
sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} .(sound _ x∈xs)) refl | x∈xs | refl
rewrite left-inverse-of xs₁≈xs₂ x∈xs = refl
sound∘complete′ (_⊛_ {s₁ = []} {xs = []} _ x∈p₂) refl with complete x∈p₂
... | ()
sound∘complete′ (_>>=_ {s₁ = []} {xs = []} x∈p₁ y∈p₂x) refl with complete x∈p₁
... | ()
sound∘complete′ (_>>=!_ {s₁ = []} x∈p₁ y∈p₂x) refl with complete y∈p₂x
... | ()
sound∘complete′ token ()
sound∘complete′ (_⊛_ {s₁ = _ ∷ _} _ _) ()
sound∘complete′ (_>>=_ {s₁ = _ ∷ _} _ _) ()
sound∘complete′ (_>>=!_ {s₁ = _ ∷ _} _ _) ()
sound∘complete′ (nonempty _) ()
complete∘sound : ∀ {Tok R xs x}
(p : Parser Tok R xs) (x∈p : x ∈ xs) →
complete (sound p x∈p) ≡ x∈p
complete∘sound (return x) (here refl) = refl
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs
with from (++⇿ {xs = xs₁}) ⟨$⟩ x∈xs
| right-inverse-of (++⇿ {xs = xs₁}) x∈xs
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to ++⇿ ⟨$⟩ inj₁ x∈xs₁) | inj₁ x∈xs₁ | refl =
P.cong (_⟨$⟩_ (to ++⇿) ∘ inj₁) $ complete∘sound p₁ x∈xs₁
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to (++⇿ {xs = xs₁}) ⟨$⟩ inj₂ x∈xs₂) | inj₂ x∈xs₂ | refl =
P.cong (_⟨$⟩_ (to (++⇿ {xs = xs₁})) ∘ inj₂) $ complete∘sound p₂ x∈xs₂
complete∘sound (_<$>_ {xs = xs} f p) x∈xs
with from (map-∈⇿ {xs = xs}) ⟨$⟩ x∈xs
| right-inverse-of map-∈⇿ x∈xs
complete∘sound (_<$>_ {xs = xs} f p) .(to map-∈⇿ ⟨$⟩ (y , y∈xs , refl)) | (y , y∈xs , refl) | refl =
P.cong (λ y∈ → to map-∈⇿ ⟨$⟩ (y , y∈ , refl)) $ complete∘sound p y∈xs
complete∘sound (_⊛_ {fs = fs} {x ∷ xs} ⟨ p₁ ⟩ p₂) y∈ys
with from (⊛.⇿ {fs = fs} {xs = x ∷ xs}) ⟨$⟩ y∈ys
| right-inverse-of (⊛.⇿ {fs = fs} {xs = x ∷ xs}) y∈ys
complete∘sound (_⊛_ {xs = x ∷ xs} ⟨ p₁ ⟩ ⟪ p₂ ⟫)
y∈ys | (f′ , x′ , () , x′∈x∷xs , refl) | _
complete∘sound (_⊛_ {xs = x ∷ xs} ⟨ p₁ ⟩ ⟨ p₂ ⟩)
.(to ⊛.⇿ ⟨$⟩ (f′ , x′ , f′∈fs , x′∈x∷xs , refl)) | (f′ , x′ , f′∈fs , x′∈x∷xs , refl) | refl =
P.cong₂ (λ f′∈ x′∈ → to ⊛.⇿ ⟨$⟩ (f′ , x′ , f′∈ , x′∈ , refl))
(complete∘sound p₁ f′∈fs)
(complete∘sound p₂ x′∈x∷xs)
complete∘sound (_>>=_ {xs = zs} {f} p₁ p₂) y∈ys
with from (>>=-∈⇿ {xs = zs} {f = f}) ⟨$⟩ y∈ys
| right-inverse-of (>>=-∈⇿ {xs = zs} {f = f}) y∈ys
complete∘sound (_>>=_ {xs = []} {f} p₁ p₂) ._ | (x , () , y∈fx) | refl
complete∘sound (_>>=_ {xs = z ∷ zs} {f} p₁ p₂) .(to (>>=-∈⇿ {f = f}) ⟨$⟩ (x , x∈z∷zs , y∈fx)) | (x , x∈z∷zs , y∈fx) | refl =
P.cong₂ (λ x∈ y∈ → to (>>=-∈⇿ {f = f}) ⟨$⟩ (x , x∈ , y∈))
(complete∘sound p₁ x∈z∷zs)
(helper (p₂ x) x∈z∷zs y∈fx)
where
helper : ∀ {Tok R₁ R₂ x y xs z} {zs : List R₁}
(p : ∞? (Parser Tok R₂ xs) (z ∷ zs))
(x∈z∷zs : x ∈ z ∷ zs) (y∈xs : y ∈ xs) →
complete (sound′ p x∈z∷zs y∈xs) ≡ y∈xs
helper ⟨ p ⟩ x∈z∷zs y∈xs = complete∘sound p y∈xs
complete∘sound (cast xs₁≈xs₂ p) x∈xs
rewrite complete∘sound p (from xs₁≈xs₂ ⟨$⟩ x∈xs) =
right-inverse-of xs₁≈xs₂ x∈xs
complete∘sound (return _) (there ())
complete∘sound fail ()
complete∘sound token ()
complete∘sound (⟪ _ ⟫ ⊛ _) ()
complete∘sound (_ >>=! _) ()
complete∘sound (nonempty _) ()
correct : ∀ {Tok R xs x} {p : Parser Tok R xs} → x ∈ p · [] ⇿ x ∈ xs
correct {p = p} = record
{ to = P.→-to-⟶ complete
; from = P.→-to-⟶ $ sound p
; inverse-of = record
{ left-inverse-of = sound∘complete
; right-inverse-of = complete∘sound p
}
}
same-set : ∀ {k Tok R xs₁ xs₂}
{p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
p₁ ≈[ k ] p₂ → xs₁ List-≈[ k ] xs₂
same-set {xs₁ = xs₁} {xs₂} {p₁} {p₂} p₁≈p₂ {x} =
(x ∈ xs₁) ⇿⟨ sym correct ⟩
x ∈ p₁ · [] ≈⟨ p₁≈p₂ ⟩
x ∈ p₂ · [] ⇿⟨ correct ⟩
(x ∈ xs₂) ∎
where open Inv.EquationalReasoning