------------------------------------------------------------------------
-- One can construct combinators which do not preserve equality
------------------------------------------------------------------------

module TotalParserCombinators.NotACongruence where

open import Coinduction
open import Data.Bool
open import Data.List
open import Function
open import Function.Equality
open import Function.Inverse as Inv
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary

open import TotalParserCombinators.Congruence using (_≅P_; _∷_)
open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S using (_∈_·_; _≅_)

-- It is easy to construct a combinator which does not preserve
-- equality. All it takes is to inspect the input combinator's
-- structure (or that of its index), and make some suitable decision
-- based on this information. Examples:

module Example₁ where

  -- A combinator which removes ambiguity.

  unambiguous :  {Tok R xs} 
                Parser Tok R xs  Parser Tok R (take 1 xs)
  unambiguous {xs = xs} p =
      token >>=  t   unambiguous (D t p))
     return⋆ (take 1 xs)

  -- The following two parsers are (parser) equal.

  p₁ : Parser Bool Bool (true  (false  []))
  p₁ = return true  return false

  p₂ : Parser Bool Bool (false  (true  []))
  p₂ = return false  return true

  equal : p₁ ≅P p₂
  equal = AdditiveMonoid.commutative (return true) (return false)

  -- However, unambiguous does not respect this equality.

  unambiguous-is-not-a-congruence :
    ¬ (unambiguous p₁  unambiguous p₂)
  unambiguous-is-not-a-congruence eq =
    case Inverse.to eq ⟨$⟩ S.∣-right [] (S.∣-left S.return) of λ
      { (S.∣-right .[] (S.∣-left               ()))
      ; (S.∣-right .[] (S.∣-right .([ false ]) ()))
      ; (S.∣-left []∈)  helper refl []∈
      }
    where
    helper :  {s} {f : Bool  List Bool}
               {p :  b   (Parser Bool Bool (f b))} 
               s  [] 
             ¬ (true  token >>= p · s)
    helper () (S._>>=_ S.token _)

module Example₂ where

  -- A combinator which returns true (without consuming input) if its
  -- argument is "fail", and false otherwise.

  is-fail-bag :  {Tok R xs}  Parser Tok R xs  List Bool
  is-fail-bag fail = [ true  ]
  is-fail-bag _    = [ false ]

  is-fail :  {Tok R xs}
            (p : Parser Tok R xs)  Parser Tok Bool (is-fail-bag p)
  is-fail fail             = return true
  is-fail (return x)       = return false
  is-fail token            = return false
  is-fail (p₁  p₂)        = return false
  is-fail (f <$> p)        = return false
  is-fail (p₁  p₂)        = return false
  is-fail (p₁ >>= p₂)      = return false
  is-fail (nonempty p)     = return false
  is-fail (cast xs₁≈xs₂ p) = return false

  -- The following parsers are equal, but is-fail treats them
  -- differently.

  p₁ : Parser Bool Bool []
  p₁ = fail

  p₂ : Parser Bool Bool []
  p₂ = fail  fail

  equal : p₁ ≅P p₂
  equal = Inv.id  λ _   equal

  is-fail-is-not-a-congruence : ¬ (is-fail p₁  is-fail p₂)
  is-fail-is-not-a-congruence eq with Inverse.to eq ⟨$⟩ S.return
  ... | ()