------------------------------------------------------------------------
-- Asymmetric choice
------------------------------------------------------------------------

module TotalParserCombinators.AsymmetricChoice where

open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Properties
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any using (here)
open import Data.Product
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Unit
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (module Equivalence; _⇔_)
open import Function.Inverse as Inv using (_↔_)
open import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Relation.Nullary

open import TotalParserCombinators.Congruence using (_∼[_]P_; _≅P_)
open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Pointwise as Pointwise
open import TotalParserCombinators.Semantics using (_∈_·_)
open import TotalParserCombinators.Semantics.Continuation as S
  using (_⊕_∈_·_)

------------------------------------------------------------------------
-- An initial bag operator

-- first-nonempty returns the left-most non-empty initial bag, if any.

first-nonempty : {R : Set}  List R  List R  List R
first-nonempty [] ys = ys
first-nonempty xs ys = xs

-- first-nonempty preserves equality.

first-nonempty-cong :
   {k R} {xs₁ xs₁′ xs₂ xs₂′ : List R} 
  xs₁ List-∼[  k ⌋⇔ ] xs₁′  xs₂ List-∼[  k ⌋⇔ ] xs₂′ 
  first-nonempty xs₁ xs₂ List-∼[  k ⌋⇔ ] first-nonempty xs₁′ xs₂′
first-nonempty-cong {xs₁ = []}    {[]}    eq₁ eq₂ = eq₂
first-nonempty-cong {xs₁ = _  _} {_  _} eq₁ eq₂ = eq₁
first-nonempty-cong {xs₁ = []} {_  _} eq₁ eq₂
  with Equivalence.from (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()
first-nonempty-cong {xs₁ = _  _} {[]} eq₁ eq₂
  with Equivalence.to (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()

-- first-nonempty is correct.

first-nonempty-left :
   {k R} {xs₁ xs₂ : List R} 
  ( λ y  y  xs₁)  first-nonempty xs₁ xs₂ List-∼[ k ] xs₁
first-nonempty-left {xs₁ = []}    (_ , ())
first-nonempty-left {xs₁ = _  _} _        = _ 
  where open Related.EquationalReasoning

first-nonempty-right :
   {k R} {xs₁ xs₂ : List R} 
  ( λ y  y  xs₁)  first-nonempty xs₁ xs₂ List-∼[ k ] xs₂
first-nonempty-right {xs₁ = x  _} ∉x∷ = ⊥-elim $ ∉x∷ (x , here P.refl)
first-nonempty-right {xs₁ = []}    _   = _ 
  where open Related.EquationalReasoning

------------------------------------------------------------------------
-- Asymmetric choice

-- _◃_ is defined as a pointwise lifting of first-nonempty. Note that
-- _◃_ preserves parser and language equality, but not the
-- sub-/superparser and sub-/superlanguage relations.

private
  module AC {R} = Pointwise R R ⌊_⌋⇔ first-nonempty first-nonempty-cong

-- p₁ ◃ p₂ returns a result if either p₁ or p₂ does. For a given
-- string results are returned either from p₁ or from p₂, not both.

infixl 5 _◃_ _◃-cong_

_◃_ :  {Tok R xs₁ xs₂} 
      Parser Tok R xs₁  Parser Tok R xs₂ 
      Parser Tok R (first-nonempty xs₁ xs₂)
_◃_ = AC.lift

-- D distributes over _◃_.

D-◃ :  {Tok R xs₁ xs₂ t}
      (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) 
      D t (p₁  p₂) ≅P D t p₁  D t p₂
D-◃ = AC.D-lift

-- _◃_ preserves equality.

_◃-cong_ :  {k Tok R xs₁ xs₁′ xs₂ xs₂′}
             {p₁  : Parser Tok R xs₁} {p₁′ : Parser Tok R xs₁′}
             {p₂  : Parser Tok R xs₂} {p₂′ : Parser Tok R xs₂′} 
           p₁ ∼[  k ⌋⇔ ]P p₁′  p₂ ∼[  k ⌋⇔ ]P p₂′ 
           p₁  p₂ ∼[  k ⌋⇔ ]P p₁′  p₂′
_◃-cong_ = AC.lift-cong

-- If p₁ accepts s, then p₁ ◃ p₂ behaves as p₁ when applied to s.

left :  {Tok R xs₁ xs₂ x s}
       (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) 
       ( λ y  y  p₁ · s)  x  p₁  p₂ · s  x  p₁ · s
left {x = x} =
  AC.lift-property
     F _ H   F  H x  F x)
     F↔F′ _ H↔H′ 
       Σ.cong Inv.id  {x}  ↔⇒ (F↔F′ x))
         →-cong-⇔
       Related-cong (H↔H′ x) (F↔F′ x))
     ∈xs₁  first-nonempty-left ∈xs₁)

-- If p₁ does not accept s, then p₁ ◃ p₂ behaves as p₂ when applied to
-- s.

right :  {Tok R xs₁ xs₂ x s}
        (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) 
        ( λ y  y  p₁ · s)  x  p₁  p₂ · s  x  p₂ · s
right {x = x} =
  AC.lift-property
     F G H   F  H x  G x)
     F↔F′ G↔G′ H↔H′ 
       ((Σ.cong Inv.id λ {x}  ↔⇒ (F↔F′ x)) →-cong-⇔ Equiv.id)
         →-cong-⇔
       Related-cong (H↔H′ x) (G↔G′ x))
     ∉xs₁  first-nonempty-right ∉xs₁)

-- In "Parsing with First-Class Derivatives" Brachthäuser, Rendel and
-- Ostermann state that "[...] and biased alternative cannot be
-- expressed as user defined combinators". Here I give a formal proof
-- of a variant of this statement (in the present setting): it is not
-- possible to construct an asymmetric choice operator that, in a
-- certain sense, is more like the prioritised choice of parsing
-- expression grammars (see Ford's "Parsing Expression Grammars: A
-- Recognition-Based Syntactic Foundation") without changing the
-- interface of the parser combinator library.

not-PEG-choice :
  ¬ ∃₂ λ (_◅-bag_ : {R : Set}  List R  List R  List R)
         (_◅_ :  {Tok R xs₁ xs₂} 
               Parser Tok R xs₁  Parser Tok R xs₂ 
               Parser Tok R (xs₁ ◅-bag xs₂)) 
       {Tok R xs₁ xs₂ s₁}
      (p₁ : Parser Tok R xs₁)
      (p₂ : Parser Tok R xs₂) 
      ((∃₂ λ y s₂  y  s₂  p₁ · s₁) 
        {x s₂}  x  s₂  p₁  p₂ · s₁  x  s₂  p₁ · s₁)
        ×
      (¬ (∃₂ λ y s₂  y  s₂  p₁ · s₁) 
        {x s₂}  x  s₂  p₁  p₂ · s₁  x  s₂  p₂ · s₁)
not-PEG-choice (_ , _◅_ , correct) = false∉p₁⊛·[-] false∈p₁⊛·[-]
  where
  p₁ p₂ : Parser  Bool _
  p₁ = const true <$> token
  p₂ = return false

  false∈p₂·[] : false  []  p₂ · []
  false∈p₂·[] = S.return

  ∄∈p₁·[] : ¬ ∃₂  b s  b  s  p₁ · [])
  ∄∈p₁·[] (_ , _ , S.<$> ())

  false∈p₁◅p₂·[] : false  []  p₁  p₂ · []
  false∈p₁◅p₂·[] =
    Equivalence.from (proj₂ (correct _ _) ∄∈p₁·[]) ⟨$⟩ false∈p₂·[]

  false∈p₁◅p₂·[-] : false  [ _ ]  p₁  p₂ · [ _ ]
  false∈p₁◅p₂·[-] = S.extend false∈p₁◅p₂·[]

  true∈p₁·[-] : true  []  p₁ · [ _ ]
  true∈p₁·[-] = S.<$> S.token

  false∈p₁·[-] : false  [ _ ]  p₁ · [ _ ]
  false∈p₁·[-] =
    Equivalence.to (proj₁ (correct _ _) (-, -, true∈p₁·[-])) ⟨$⟩
      false∈p₁◅p₂·[-]

  false∈p₁⊛·[-] :
    false  []  const <$> p₁  (return _  token) · [ _ ]
  false∈p₁⊛·[-] = S.[ _ - _ ] S.<$> false∈p₁·[-]  S.∣-right _ S.token

  false∉p₁⊛·[-] :
    ¬ false  []  const <$> p₁  (return _  token) · [ _ ]
  false∉p₁⊛·[-] = flip lemma P.refl
    where
    lemma :
       {b} 
      b  []  const <$> p₁  (return _  token) · [ _ ]  b  false
    lemma (S.[ _ - _ ] S.<$> (S.<$> S.token)  _) ()