------------------------------------------------------------------------
-- Not
------------------------------------------------------------------------

module TotalParserCombinators.Not where

open import Axiom.Extensionality.Propositional
open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Unit
open import Function
import Function.Properties.Inverse as Inv
open import Function.Related.Propositional
import Function.Related.TypeIsomorphisms as Iso
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

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

-- not-index xs is non-empty iff xs is empty.

not-index : {R : Set} → List R → List ⊤
not-index xs = if null xs then [ tt ] else []

-- not-index preserves equality.

not-index-cong : ∀ {k R} {xs xs′ : List R} →
                 xs List-∼[ ⌊ k ⌋⇔ ] xs′ →
                 not-index xs List-∼[ ⌊ k ⌋⇔ ] not-index xs′
not-index-cong {xs = []   } {xs′ = []   } eq = ↔⇒ (Inv.refl _)
not-index-cong {xs = _ ∷ _} {xs′ = _ ∷ _} eq = ↔⇒ (Inv.refl _)
not-index-cong {xs = []   } {xs′ = _ ∷ _} eq
  with Equivalence.from (⇒⇔ eq) $ here P.refl
... | ()
not-index-cong {xs = _ ∷ _} {xs′ = []   } eq
  with Equivalence.to   (⇒⇔ eq) $ here P.refl
... | ()

-- not-index is correct, assuming that propositional equality is
-- extensional.

not-index-correct :
  Extensionality zero zero →
  ∀ {R} (xs : List R) → tt ∈ not-index xs ↔ ∄ λ x → x ∈ xs
not-index-correct ext [] =
  mk↔ {to = to} {from = from}
    ( (λ { P.refl → to∘from _ })
    , (λ { P.refl → from∘to _ })
    )
  where
  to : tt ∈ [ tt ] → ∄ λ x → x ∈ []
  to _ (_ , ())

  from : (∄ λ x → x ∈ []) → tt ∈ [ tt ]
  from _ = here P.refl

  to∘from : (p : ∄ λ x → x ∈ []) → to (from p) ≡ p
  to∘from p = ext helper
    where
    helper : (∈[] : ∃ λ x → x ∈ []) → to (from p) ∈[] ≡ p ∈[]
    helper (_ , ())

  from∘to : (p : tt ∈ [ tt ]) → from (to p) ≡ p
  from∘to (here P.refl) = P.refl
  from∘to (there ())

not-index-correct ext (x ∷ xs) =
  mk↔ {to = to} {from = from}
    ( (λ {          P.refl → to∘from _ })
    , (λ { {x = ()} P.refl })
    )
  where
  ys = x ∷ xs

  to : tt ∈ [] → ∄ λ y → y ∈ ys
  to ()

  from : (∄ λ y → y ∈ ys) → tt ∈ []
  from y∉∷ with y∉∷ (-, here P.refl)
  ... | ()

  to∘from : (p : ∄ λ y → y ∈ ys) → to (from p) ≡ p
  to∘from y∉∷ with y∉∷ (-, here P.refl)
  ... | ()

------------------------------------------------------------------------
-- Not

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

private
  module Not {R : Set} =
    Pointwise ⊥ R ⌊_⌋⇔ (const not-index) (const not-index-cong)

infix  ¬_ ¬-cong_

-- ¬ p returns a result if p doesn't.

¬_ : ∀ {Tok R xs} → Parser Tok R xs → Parser Tok ⊤ (not-index xs)
¬_ = Not.lift fail

-- D distributes over ¬_.

D-¬ : ∀ {Tok R xs t} (p : Parser Tok R xs) → D t (¬ p) ≅P ¬ D t p
D-¬ = Not.D-lift fail

-- ¬_ preserves equality.

¬-cong_ : ∀ {k Tok R xs xs′}
            {p : Parser Tok R xs} {p′ : Parser Tok R xs′} →
          p ∼[ ⌊ k ⌋⇔ ]P p′ → ¬ p ∼[ ⌊ k ⌋⇔ ]P ¬ p′
¬-cong_ = Not.lift-cong C.fail

-- ¬_ is correct (assuming that propositional equality is
-- extensional).

correct : (∀ {ℓ} → Extensionality ℓ zero) →
          ∀ {Tok R xs s} (p : Parser Tok R xs) →
          tt ∈ ¬ p · s ↔ ∄ λ x → x ∈ p · s
correct ext =
  Not.lift-property
    (λ _ G H → H tt ↔ ∄ G)
    (λ _ G↔G′ H↔H′ →
       Iso.Related-cong
         (H↔H′ tt)
         (Iso.→-cong ext ext (Σ.cong (Inv.refl _) λ {x} → G↔G′ x)
            (Inv.refl _)))
    (not-index-correct ext _)
    fail