------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of regular expressions and their semantics
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (DecPoset)

module Text.Regex.Properties {a e r} (P? : DecPoset a e r) where

open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.All using (all?)
open import Data.List.Relation.Unary.Any using (any?)
open import Data.Product.Base using (_×_; _,_; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_$_)

open import Relation.Nullary.Decidable
  using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_)
open import Relation.Nullary.Negation
  using (¬_; contradiction)

import Relation.Unary  as U
open import Relation.Binary.Definitions using (Decidable)

open DecPoset P? renaming (Carrier to A)
open import Text.Regex.Base preorder
open import Data.List.Relation.Binary.Pointwise.Base using ([])
open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}

------------------------------------------------------------------------
-- Publicly re-export core properties

open import Text.Regex.Properties.Core preorder public

------------------------------------------------------------------------
-- Decidability results

[]∈?_ : U.Decidable ([] ∈_)
[]∈? ε       = yes ε
[]∈? [ rs ]  = no (λ ())
[]∈? [^ rs ] = no (λ ())
[]∈? (e ∣ f) = map′ sum (λ where (sum pr) → pr)
             $ ([]∈? e) ⊎-dec ([]∈? f)
[]∈? (e ∙ f) = map′ (uncurry (prod ([]++ []))) []∈e∙f-inv
             $ ([]∈? e) ×-dec ([]∈? f)
[]∈? (e ⋆)   = yes (star (sum (inj₁ ε)))

infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_]

_∈ᴿ?_ : Decidable _∈ᴿ_
c ∈ᴿ? [ a ]     = map′ [_] (λ where [ eq ] → eq) (c ≟ a)
c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le)
                $ (lb ≤? c) ×-dec (c ≤? ub)

_∉ᴿ?_ : Decidable _∉ᴿ_
a ∉ᴿ? r = ¬? (a ∈ᴿ? r)

_∈?ε : U.Decidable (_∈ ε)
[]      ∈?ε = yes ε
(a ∷ _) ∈?ε = no (λ ())

_∈?[_] : ∀ w rs → Dec (w ∈ [ rs ])
[]          ∈?[ rs ] = no (λ ())
(a ∷ b ∷ _) ∈?[ rs ] = no (λ ())
(a ∷ [])    ∈?[ rs ] = map′ [_] (λ where [ p ] → p)
                      $ any? (a ∈ᴿ?_) rs

_∈?[^_] : ∀ w rs → Dec (w ∈ [^ rs ])
[]          ∈?[^ rs ] = no (λ ())
(a ∷ [])    ∈?[^ rs ] = map′ [^_] (λ where [^ p ] → p) $ all? (a ∉ᴿ?_) rs
(a ∷ b ∷ _) ∈?[^ rs ] = no (λ ())