------------------------------------------------------------------------
-- Parsing of matching parentheses, along with a correctness proof
------------------------------------------------------------------------

-- A solution to an exercise set by Helmut Schwichtenberg.

module TotalRecognisers.LeftRecursion.MatchingParentheses where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List
open import Data.List.Properties
open import Data.Product
open import Function.Bundles
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable as Decidable

private
  module ListMonoid {A : Set} = Monoid (++-monoid A)

import TotalRecognisers.LeftRecursion as LR
import TotalRecognisers.LeftRecursion.Lib as Lib

-- Parentheses.

data Paren : Set where
    : Paren

-- Strings of matching parentheses.

data Matching : List Paren  Set where
  nil : Matching []
  app :  {xs ys}
        (p₁ : Matching xs) (p₂ : Matching ys)  Matching (xs ++ ys)
  par :  {xs} (p : Matching xs)  Matching ([  ] ++ xs ++ [  ])

-- Our goal: decide Matching.

Goal : Set
Goal =  xs  Dec (Matching xs)

-- Equality of parentheses is decidable.

_≟-Paren_ : Decidable (_≡_ {A = Paren})
 ≟-Paren  = yes P.refl
 ≟-Paren  = no λ()
 ≟-Paren  = no λ()
 ≟-Paren  = yes P.refl

open LR Paren hiding (_∷_)
private
  open module Tok = Lib.Tok Paren _≟-Paren_ using (tok)

-- A (left and right recursive) grammar for matching parentheses. Note
-- the use of nonempty; without the two occurrences of nonempty the
-- grammar would not be well-formed.

matching : P _
matching =
    empty
    nonempty matching ·  nonempty matching
    (tok  ·  matching) ·  tok 

-- We can decide membership of matching.

decide-matching :  xs  Dec (xs  matching)
decide-matching xs = xs ∈? matching

-- Membership of matching is equivalent to satisfaction of Matching.

∈m⇔M :  {xs}  (xs  matching)  Matching xs
∈m⇔M = mk⇔ to from
  where
  to :  {xs}  xs  matching  Matching xs
  to (∣-left (∣-left empty))                        = nil
  to (∣-left (∣-right (nonempty p₁ · nonempty p₂))) = app (to p₁) (to p₂)
  to (∣-right (⟦∈ · p · ⟧∈))
    rewrite Tok.sound ⟦∈ | Tok.sound ⟧∈             = par (to p)

  from :  {xs}  Matching xs  xs  matching
  from nil                                    = ∣-left (∣-left empty)
  from (app {xs = []}                  p₁ p₂) = from p₂
  from (app {xs = x  xs} {ys = []}    p₁ p₂) rewrite proj₂ ListMonoid.identity xs = from p₁
  from (app {xs = _  _}  {ys = _  _} p₁ p₂) = ∣-left (∣-right {n₁ = true} (nonempty (from p₁) · nonempty (from p₂)))
  from (par p)                                = ∣-right {n₁ = true} (Tok.complete · from p · Tok.complete)

-- And thus we reach our goal.

goal : Goal
goal xs = Decidable.map ∈m⇔M (decide-matching xs)

-- Some examples.

ex₁ : Dec (Matching [])
ex₁ = goal _ -- = yes nil

ex₂ : Dec (Matching (    []))
ex₂ = goal _ -- = yes (par nil)

ex₃ : Dec (Matching (        []))
ex₃ = goal _ -- = yes (app (par nil) (par nil))

ex₄ : Dec (Matching (      []))
ex₄ = goal _ -- = no (λ x → …)