{-# OPTIONS --guardedness #-}

module Parentheses where

import Level
open import Level.Bounded hiding (List)

open import Data.Maybe
open import Data.Char
open import Data.List.Base as List using (List; []; _∷_; _++_)
import Data.List.Sized.Interface
open import Data.Bool
open import Data.Unit.Base using (tt)

open import Relation.Nullary
open import Relation.Binary hiding (DecidableEquality)

open import Agda.Builtin.Equality
open import Function

open import Base Level.zero

-- Well-parenthesised string
data PAR : Set where
  LPAR RPAR : PAR
  LCUR RCUR : PAR
  LSQU RSQU : PAR

eqPAR : Decidable {A = PAR} _≡_
eqPAR LPAR LPAR = yes refl
eqPAR RPAR RPAR = yes refl
eqPAR LCUR LCUR = yes refl
eqPAR RCUR RCUR = yes refl
eqPAR LSQU LSQU = yes refl
eqPAR RSQU RSQU = yes refl
-- catchall for no
eqPAR _ _ = no whatever where
  postulate whatever : {A : Set} → A


instance
  _ : DecidableEquality PAR
  _ = record { decide = eqPAR }

  tokPAR : Tokenizer [ PAR ]
  tokPAR = mkTokenizer $ List.foldr (_++_ ∘ toPAR) [] where

    toPAR : Char → List PAR
    toPAR c = if c == '(' then LPAR ∷ []
         else if c == ')' then RPAR ∷ []
         else if c == '{' then LCUR ∷ []
         else if c == '}' then RCUR ∷ []
         else if c == '[' then LSQU ∷ []
         else if c == ']' then RSQU ∷ []
         else [] -- ignoring other characters as noise


Pars : Parameters Level.zero
Pars = vec [ PAR ]

PAR′ : ∀[ Parser Pars ⊤ ]
PAR′ = fix (Parser Pars ⊤) $ λ rec →
   let _R?_R? : PAR → PAR → Parser Pars ⊤ _
       _R?_R? p q = tt <$ ((exact p <&?> rec) <& box (exact q <&?> rec))
   in    LPAR R? RPAR R?
     <|> LCUR R? RCUR R?
     <|> LSQU R? RSQU R?

-- tests

_ : "hel[{(lo({((wor))ld})wan)t}som{e()[n]o}i(s)e]?" ∈ PAR′
_ = _ !