open import Relation.Binary
open import Relation.Binary.PropositionalEquality
module TotalRecognisers.Simple.AlternativeBackend
(Tok : Set)
(_≟_ : Decidable (_≡_ {A = Tok}))
where
open import Codata.Musical.Notation
open import Data.Bool hiding (_≟_)
open import Data.List
open import Relation.Nullary.Decidable
import TotalRecognisers.Simple as S
open S Tok _≟_ hiding (_∈?_)
data Proc : Set where
tokenBind : (p : Tok → ∞ Proc) → Proc
emptyOr : (p : Proc) → Proc
fail : Proc
run : Proc → List Tok → Bool
run (tokenBind p) (c ∷ s) = run (♭ (p c)) s
run (emptyOr p) s = null s ∨ run p s
run _ _ = false
infixl 5 _∣_
data ProcP : Set where
tokenBind : (p : Tok → ∞ ProcP) → ProcP
emptyOr : (p : ProcP) → ProcP
fail : ProcP
_∣_ : (p₁ p₂ : ProcP) → ProcP
toProc : ∀ {n} (p : P n) (κ : ProcP) → ProcP
data ProcW : Set where
tokenBind : (p : Tok → ∞ ProcP) → ProcW
emptyOr : (p : ProcW) → ProcW
fail : ProcW
program : ProcW → ProcP
program (tokenBind p) = tokenBind p
program (emptyOr p) = emptyOr (program p)
program fail = fail
_∣W_ : ProcW → ProcW → ProcW
tokenBind p₁ ∣W tokenBind p₂ = tokenBind (λ c → ♯ (♭ (p₁ c) ∣ ♭ (p₂ c)))
emptyOr p₁ ∣W emptyOr p₂ = emptyOr (p₁ ∣W p₂)
emptyOr p₁ ∣W p₂ = emptyOr (p₁ ∣W p₂)
p₁ ∣W emptyOr p₂ = emptyOr (p₁ ∣W p₂)
fail ∣W p₂ = p₂
p₁ ∣W fail = p₁
mutual
toProcW′ : ∀ {n} → P n → if n then ProcW else ProcP → ProcW
toProcW′ fail κ = fail
toProcW′ empty κ = κ
toProcW′ (tok t) κ = tokenBind (λ t′ →
if ⌊ t ≟ t′ ⌋ then ♯ κ else ♯ fail)
toProcW′ (_∣_ {n₁ = true } {n₂ = true } p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
toProcW′ (_∣_ {n₁ = true } {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW p₂ κ
toProcW′ (_∣_ {n₁ = false} {n₂ = true } p₁ p₂) κ = toProcW p₁ κ ∣W toProcW′ p₂ κ
toProcW′ (_∣_ {n₁ = false} {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
toProcW′ (_·_ {n₁ = true } p₁ p₂) κ = toProcW′ p₁ (toProcW′ p₂ κ)
toProcW′ (_·_ {n₁ = false} p₁ p₂) κ = toProcW′ p₁ (toProc (♭ p₂) κ)
toProcW : ∀ {n} → P n → ProcW → ProcW
toProcW {true } p κ = toProcW′ p κ
toProcW {false} p κ = toProcW′ p (program κ)
whnf : ProcP → ProcW
whnf (tokenBind p) = tokenBind p
whnf (emptyOr p) = emptyOr (whnf p)
whnf fail = fail
whnf (p₁ ∣ p₂) = whnf p₁ ∣W whnf p₂
whnf (toProc p κ) = toProcW p (whnf κ)
mutual
⟦_⟧W : ProcW → Proc
⟦ tokenBind p ⟧W = tokenBind (λ c → ♯ ⟦ ♭ (p c) ⟧P)
⟦ emptyOr p ⟧W = emptyOr ⟦ p ⟧W
⟦ fail ⟧W = fail
⟦_⟧P : ProcP → Proc
⟦ p ⟧P = ⟦ whnf p ⟧W
infix 4 _∈?_
_∈?_ : ∀ {n} → List Tok → P n → Bool
s ∈? p = run ⟦ toProc p (emptyOr fail) ⟧P s