open import Relation.Binary
open import Relation.Binary.PropositionalEquality
module TotalRecognisers.Simple
(Tok : Set)
(_≟_ : Decidable (_≡_ {A = Tok}))
where
open import Algebra
open import Coinduction
open import Data.Bool
import Data.Bool.Properties as Bool
private
module BoolCS = CommutativeSemiring Bool.commutativeSemiring-∧-∨
open import Function
open import Data.List
open import Data.Product
open import Relation.Nullary
infixl 10 _·_
infixl 5 _∣_
mutual
data P : Bool → Set where
fail : P false
empty : P true
tok : Tok → P false
_∣_ : ∀ {n₁ n₂} → P n₁ → P n₂ → P (n₁ ∨ n₂)
_·_ : ∀ {n₁ n₂} → P n₁ → ∞⟨ not n₁ ⟩P n₂ → P (n₁ ∧ n₂)
∞⟨_⟩P : Bool → Bool → Set
∞⟨ true ⟩P n = ∞ (P n)
∞⟨ false ⟩P n = P n
delayed? : ∀ {b n} → ∞⟨ b ⟩P n → Bool
delayed? {b = b} _ = b
♭? : ∀ {b n} → ∞⟨ b ⟩P n → P n
♭? {true} x = ♭ x
♭? {false} x = x
♯? : ∀ {b n} → P n → ∞⟨ b ⟩P n
♯? {true} x = ♯ x
♯? {false} x = x
♭?♯? : ∀ b {n} {p : P n} → ♭? {b} (♯? p) ≡ p
♭?♯? true = refl
♭?♯? false = refl
infix 4 _∈_
data _∈_ : ∀ {n} → List Tok → P n → Set where
empty : [] ∈ empty
tok : ∀ {t} → [ t ] ∈ tok t
∣-left : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
s ∈ p₁ → s ∈ p₁ ∣ p₂
∣-right : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
s ∈ p₂ → s ∈ p₁ ∣ p₂
_·_ : ∀ {s₁ s₂ n₁ n₂} {p₁ : P n₁} {p₂ : ∞⟨ not n₁ ⟩P n₂} →
s₁ ∈ p₁ → s₂ ∈ ♭? p₂ → s₁ ++ s₂ ∈ p₁ · p₂
cast : ∀ {n} {p p′ : P n} {s} → p ≡ p′ → s ∈ p → s ∈ p′
cast refl s∈ = s∈
⇒ : ∀ {n} {p : P n} → [] ∈ p → n ≡ true
⇒ pr = ⇒′ pr refl
where
⇒′ : ∀ {n s} {p : P n} → s ∈ p → s ≡ [] → n ≡ true
⇒′ empty refl = refl
⇒′ tok ()
⇒′ (∣-left pr₁) refl with ⇒ pr₁
⇒′ (∣-left pr₁) refl | refl = refl
⇒′ (∣-right pr₂) refl with ⇒ pr₂
⇒′ (∣-right {n₁ = n₁} pr₂) refl | refl = proj₂ BoolCS.zero n₁
⇒′ (_·_ {[]} pr₁ pr₂) refl = cong₂ _∧_ (⇒ pr₁) (⇒ pr₂)
⇒′ (_·_ {_ ∷ _} pr₁ pr₂) ()
⇐ : ∀ {n} (p : P n) → n ≡ true → [] ∈ p
⇐ fail ()
⇐ empty refl = empty
⇐ (tok t) ()
⇐ (_∣_ {true} p₁ p₂) refl = ∣-left (⇐ p₁ refl)
⇐ (_∣_ {false} {true} p₁ p₂) refl = ∣-right {p₁ = p₁} (⇐ p₂ refl)
⇐ (_∣_ {false} {false} p₁ p₂) ()
⇐ (_·_ {true} p₁ p₂) refl = ⇐ p₁ refl · ⇐ p₂ refl
⇐ (_·_ {false} p₁ p₂) ()
nullable? : ∀ {n} (p : P n) → Dec ([] ∈ p)
nullable? {true} p = yes (⇐ p refl)
nullable? {false} p = no helper
where
helper : ¬ [] ∈ p
helper []∈p with ⇒ []∈p
... | ()
D-nullable : ∀ {n} → Tok → P n → Bool
D-nullable t fail = false
D-nullable t empty = false
D-nullable t (tok t′) with t′ ≟ t
D-nullable t (tok t′) | yes t′≡t = true
D-nullable t (tok t′) | no t′≢t = false
D-nullable t (p₁ ∣ p₂) = D-nullable t p₁ ∨ D-nullable t p₂
D-nullable t (p₁ · p₂) with delayed? p₂
D-nullable t (p₁ · p₂) | true = D-nullable t p₁ ∧ _
D-nullable t (p₁ · p₂) | false = D-nullable t p₁ ∧ _ ∨ D-nullable t p₂
D : ∀ {n} (t : Tok) (p : P n) → P (D-nullable t p)
D t fail = fail
D t empty = fail
D t (tok t′) with t′ ≟ t
D t (tok t′) | yes t′≡t = empty
D t (tok t′) | no t′≢t = fail
D t (p₁ ∣ p₂) = D t p₁ ∣ D t p₂
D t (p₁ · p₂) with delayed? p₂
D t (p₁ · p₂) | true = D t p₁ · ♯? (♭ p₂)
D t (p₁ · p₂) | false = D t p₁ · ♯? p₂ ∣ D t p₂
D-sound : ∀ {s n} {t} {p : P n} → s ∈ D t p → t ∷ s ∈ p
D-sound s∈ = D-sound′ _ _ s∈
where
D-sound′ : ∀ {s n} t (p : P n) → s ∈ D t p → t ∷ s ∈ p
D-sound′ t fail ()
D-sound′ t empty ()
D-sound′ t (tok t′) _ with t′ ≟ t
D-sound′ t (tok .t) empty | yes refl = tok
D-sound′ t (tok t′) () | no t′≢t
D-sound′ t (p₁ ∣ p₂) (∣-left ∈₁) = ∣-left (D-sound′ t p₁ ∈₁)
D-sound′ t (p₁ ∣ p₂) (∣-right ∈₂) = ∣-right {p₁ = p₁} (D-sound′ t p₂ ∈₂)
D-sound′ t (_·_ {true} p₁ p₂) (∣-left (∈₁ · ∈₂)) = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂
D-sound′ t (_·_ {true} p₁ p₂) (∣-right ∈₂) = ⇐ p₁ refl · D-sound′ t p₂ ∈₂
D-sound′ t (_·_ {false} p₁ p₂) (∈₁ · ∈₂) = D-sound′ t p₁ ∈₁ · cast (♭?♯? (not (D-nullable t p₁))) ∈₂
D-complete : ∀ {s n} {t} {p : P n} → t ∷ s ∈ p → s ∈ D t p
D-complete {t = t} t∷s∈ = D-complete′ _ t∷s∈ refl
where
D-complete′ : ∀ {s s′ n} (p : P n) → s′ ∈ p → s′ ≡ t ∷ s → s ∈ D t p
D-complete′ fail () refl
D-complete′ empty () refl
D-complete′ (tok t′) _ refl with t′ ≟ t
D-complete′ (tok .t) tok refl | yes refl = empty
D-complete′ {[]} (tok .t) tok refl | no t′≢t with t′≢t refl
D-complete′ {[]} (tok .t) tok refl | no t′≢t | ()
D-complete′ {_ ∷ _} (tok t′) () refl | no t′≢t
D-complete′ (p₁ ∣ p₂) (∣-left ∈₁) refl = ∣-left (D-complete ∈₁)
D-complete′ (p₁ ∣ p₂) (∣-right ∈₂) refl = ∣-right {p₁ = D t p₁} (D-complete ∈₂)
D-complete′ (_·_ {true} p₁ p₂) (_·_ {[]} ∈₁ ∈₂) refl = ∣-right {p₁ = D t p₁ · _} (D-complete ∈₂)
D-complete′ (_·_ {true} p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = ∣-left (D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂)
D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]} ∈₁ ∈₂) refl with ⇒ ∈₁
D-complete′ (_·_ {false} p₁ p₂) (_·_ {[]} ∈₁ ∈₂) refl | ()
D-complete′ (_·_ {false} p₁ p₂) (_·_ {._ ∷ _} ∈₁ ∈₂) refl = D-complete ∈₁ · cast (sym (♭?♯? (not (D-nullable t p₁)))) ∈₂
infix 4 _∈?_
_∈?_ : ∀ {n} (s : List Tok) (p : P n) → Dec (s ∈ p)
[] ∈? p = nullable? p
t ∷ s ∈? p with s ∈? D t p
t ∷ s ∈? p | yes s∈Dtp = yes (D-sound s∈Dtp)
t ∷ s ∈? p | no s∉Dtp = no (s∉Dtp ∘ D-complete)