{-
  Revisiting https://wwwcip.cs.fau.de/~oc45ujef/misc/regex.agda using sized types.
-}
{-# OPTIONS --sized-types #-}
open import Data.Bool renaming (Bool to 𝟚 ; true to ⊤ ; false to ⊥)
open import Relation.Nullary.Decidable using (yes ; no)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Size
import Level

record 𝓛 (i : Size) (Σ : Set) : Set where
  coinductive
  field
    accept : 𝟚
    δ : ∀ {j : Size< i} → Σ → 𝓛 j Σ

open 𝓛

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

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

  flippy : {i : Size} → Q → 𝓛 i Σ
  flippy q₁ .accept = ⊥
  flippy q₂ .accept = ⊤
  flippy q₁ .δ A = flippy q₁
  flippy q₁ .δ B = flippy q₂
  flippy q₂ .δ A = flippy q₂
  flippy q₂ .δ B = flippy q₁

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

unfold : ∀ {Σ : Set} → 𝓛 ∞ Σ → (Σ ⋆ → 𝟚)
unfold x [] = accept x
unfold x (σ ∷ w) = unfold (δ x σ) w

module regex {Σ : Set} {_≈_ : DecidableEquality Σ} where
  ∅ : {i : Size} → 𝓛 i Σ
  ∅ .accept = ⊥
  ∅ .δ _ = ∅

  ε : {i : Size} → 𝓛 i Σ
  ε .accept = ⊤
  ε .δ _ = ∅

  infix 15 `_
  `_ : {i : Size} → Σ → 𝓛 i Σ
  (` c) .accept = ⊥
  (` c) .δ x with c ≈ x
  ... | yes _ = ε
  ... | no _ = ∅

  infixl 10 _∪_
  _∪_ : {i : Size} → 𝓛 i Σ → 𝓛 i Σ → 𝓛 i Σ
  (s ∪ t) .accept = accept s ∨ accept t
  (s ∪ t) .δ x = (δ s x) ∪ δ t x

  infixl 20 _;_
  _;_ : {i : Size} → 𝓛 i Σ → 𝓛 i Σ → 𝓛 i Σ
  (s ; t) .accept = accept s ∧ accept t
  (s ; t) .δ x with accept s
  ... | ⊤ = δ s x ; t ∪ δ t x
  ... | ⊥ = δ s x ; t

  infixl 30 _*
  _* : {i : Size} → 𝓛 i Σ → 𝓛 i Σ
  (s *) .accept = ⊤
  (s *) .δ x = δ s x ; s *

  match : Σ ⋆ → 𝓛 ∞ Σ → 𝟚
  match w L = unfold L w

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

  _≈_ : DecidableEquality Σ
  f ≈ f = yes refl
  f ≈ o = no (λ ())
  o ≈ f = no λ ()
  o ≈ o = yes refl

  open regex {Σ} {_≈_}

  foo : 𝓛 ∞ Σ
  foo = (ε ∪ ` f ∪ ` o) ; (` o) *

  word : Σ ⋆
  word = f ∷ o ∷ o ∷ []

  bar : 𝓛 ∞ Σ
  bar = (` f) * ; (` o)


module da {Σ : Set} {_≈_ : DecidableEquality Σ} where

  record 𝓐 (Q : Set) : Set₁ where
    field
      δᴬ : Q → Σ → Q
      F : Q → 𝟚
      s : Q
  open 𝓐

  _at_accepts_ : ∀ {Q : Set} (A : 𝓐 Q) → Q → Σ ⋆ → 𝟚
  _at_accepts_ A q [] = 𝓐.F A q
  _at_accepts_ A q (x ∷ xs) = A at (δᴬ A q x) accepts xs

  eval : ∀ {Q : Set} (A : 𝓐 Q) → Σ ⋆ → 𝟚
  eval A x = A at 𝓐.s A accepts x

  langat : ∀ {Q : Set} {i : Size} → 𝓐 Q → Q → 𝓛 i Σ
  langat A q .accept = 𝓐.F A q
  langat A q .δ x = langat A (δᴬ A q x)

  lang : ∀ {Q : Set} → 𝓐 Q → 𝓛 ∞ Σ
  lang A = langat A (𝓐.s A)

  open import Relation.Binary.PropositionalEquality -- TODO: switch to decidable predicates to avoid this
  open regex {Σ} {_≈_}
  coincideat : ∀ {Q : Set} {i : Size} → (A : 𝓐 Q) → (q : Q) → (w : Σ ⋆) → A at q accepts w ≡ ⊤ → match w (langat A q) ≡ ⊤
  coincideat A q [] H = H
  coincideat A q (x ∷ w) H = coincideat A (δᴬ A q x) w H

  coincide : ∀ {Q : Set} {i : Size} → (A : 𝓐 Q) → (w : Σ ⋆) → eval A w ≡ ⊤ → match w (lang A) ≡ ⊤
  coincide A w H = coincideat A (𝓐.s A) w H