{-

A (slightly broken) implementation of regular expressions using the
final coalgebra of 𝟚 × X^Σ.  Co-developed with Philip.

https://wwwcip.cs.fau.de/~oc45ujef/misc/regex.agda
-}
{-# OPTIONS --guardedness #-}
open import Data.Bool renaming (Bool to 𝟚 ; true to ⊤ ; false to ⊥)

record 𝓐 (Σ : Set) : Set where
  coinductive
  field
    F : 𝟚
    δ : Σ → 𝓐 Σ

open 𝓐

module example where
  data Σ : Set where
    A : Σ
    B : Σ

  data Q : Set where
    q₁ : Q
    q₂ : Q

  flippy : Q → 𝓐 Σ
  F (flippy q₂) = ⊤
  δ (flippy q₂) A = flippy q₂
  δ (flippy q₂) B = flippy q₁
  F (flippy q₁) = ⊥
  δ (flippy q₁) A = flippy q₁
  δ (flippy q₁) B = flippy q₂

infixr 50 _∷_
data _⋆ (Σ : Set) : Set where
  ε : Σ ⋆
  _∷_ : Σ → Σ ⋆ → Σ ⋆

unfold : ∀ {Σ : Set} → 𝓐 Σ → (Σ ⋆ → 𝟚)
unfold x ε = F x
unfold x (σ ∷ w) = unfold (δ x σ) w

infixr 55 _,_
infix 60 `_
infixr 50 _∣_
data Regex (Σ : Set) : Set where
  ∅ : Regex Σ
  ϵ : Regex Σ
  `_ : Σ → Regex Σ
  _∣_ : Regex Σ → Regex Σ → Regex Σ
  _,_ : Regex Σ → Regex Σ → Regex Σ
  _* : Regex Σ → Regex Σ

module _ (Σ : Set) (_≈_ : Σ → Σ → 𝟚) where

  _acceptor : 𝟚 → 𝓐 Σ
  F (b acceptor) = b
  δ (b acceptor) = λ _ → b acceptor

  final-acceptor : 𝓐 Σ
  F final-acceptor = ⊤
  δ final-acceptor _ = ⊥ acceptor

  char : Σ → 𝓐 Σ
  F (char a) = ⊥
  δ (char a) a' with a ≈ a'
  ... | ⊤ = final-acceptor
  ... | ⊥ = ⊥ acceptor

  _∪_ : 𝓐 Σ → 𝓐 Σ → 𝓐 Σ
  F (p ∪ q) = F p ∨ F q
  δ (p ∪ q) a = δ p a ∪ δ q a

  {-# TERMINATING #-}           -- trust me chap
  _;_ : 𝓐 Σ → 𝓐 Σ → 𝓐 Σ
  F (p ; q) = F p ∧ F q
  δ (p ; q) a with F p
  ... | ⊤ = (δ p a ; q) ∪ δ q a
  ... | ⊥ = δ p a ; q

  {-# TERMINATING #-}           -- you won't regret it
  repeater : 𝓐 Σ → 𝓐 Σ
  F (repeater p) = ⊤
  δ (repeater p) a = (δ p a) ; repeater p
  
  regex : Regex Σ → 𝓐 Σ
  regex ∅ = ⊥ acceptor
  regex ϵ = final-acceptor
  regex (` a) = char a
  regex (s ∣ t) = (regex s) ∪ (regex t)
  regex (s , t) = (regex s) ; (regex t)
  regex (s *) = repeater (regex s)

module example2 where
  data Σ : Set where
    f : Σ
    o : Σ

  _≈_ : Σ → Σ → 𝟚
  f ≈ f = ⊤
  f ≈ o = ⊥
  o ≈ f = ⊥
  o ≈ o = ⊤

  foo : Regex Σ
  foo = (ϵ ∣ ` f ∣ ` o) , (` o) *

  word : Σ ⋆
  word = f ∷ o ∷ o ∷ ε