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
data Paren : Set where
⟦ ⟧ : Paren
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 ++ [ ⟧ ])
Goal : Set
Goal = ∀ xs → Dec (Matching xs)
_≟-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)
matching : P _
matching =
empty
∣ ♯ nonempty matching · ♯ nonempty matching
∣ ♯ (tok ⟦ · ♯ matching) · ♯ tok ⟧
decide-matching : ∀ xs → Dec (xs ∈ matching)
decide-matching xs = xs ∈? 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)
goal : Goal
goal xs = Decidable.map ∈m⇔M (decide-matching xs)
ex₁ : Dec (Matching [])
ex₁ = goal _
ex₂ : Dec (Matching (⟦ ∷ ⟧ ∷ []))
ex₂ = goal _
ex₃ : Dec (Matching (⟦ ∷ ⟧ ∷ ⟦ ∷ ⟧ ∷ []))
ex₃ = goal _
ex₄ : Dec (Matching (⟦ ∷ ⟧ ∷ ⟦ ∷ []))
ex₄ = goal _