------------------------------------------------------------------------
-- Unambiguity
------------------------------------------------------------------------

module TotalParserCombinators.Unambiguity where

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as H
  renaming (_≅_ to _≅′_)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

-- A parser is unambiguous if every string can be parsed in at most
-- one way.

Unambiguous : ∀ {Tok R xs} → Parser Tok R xs → Set₁
Unambiguous p =
  ∀ {x₁ x₂ s} (x₁∈p : x₁ ∈ p · s) (x₂∈p : x₂ ∈ p · s) →
  x₁ ≡ x₂ × x₁∈p ≅′ x₂∈p

-- Language and parser equivalence coincide for unambiguous parsers.

≈⇒≅ : ∀ {Tok R xs₁ xs₂}
        {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
      Unambiguous p₁ → Unambiguous p₂ → p₁ ≈ p₂ → p₁ ≅ p₂
≈⇒≅ u₁ u₂ p₁≈p₂ =
  mk↔ {to = Equivalence.to p₁≈p₂} {from = Equivalence.from p₁≈p₂}
    ( (λ { refl → H.≅-to-≡ $ proj₂ $ u₂ _ _ })
    , (λ { refl → H.≅-to-≡ $ proj₂ $ u₁ _ _ })
    )