```------------------------------------------------------------------------
-- A tiny library of derived combinators
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.Lib (Tok : Set) where

open import Coinduction
open import Data.Bool hiding (_∧_)
open import Data.Bool.Properties
open import Function hiding (_∋_)
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence using (module Equivalence)
open import Data.List
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product as Prod
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary.Decidable

import TotalRecognisers.LeftRecursion
open TotalRecognisers.LeftRecursion Tok

------------------------------------------------------------------------
-- Kleene star

-- The intended semantics of the Kleene star.

infixr 5 _∷_
infix  4 _∈[_]⋆

data _∈[_]⋆ {n} : List Tok → P n → Set where
[]  : ∀ {p}       → [] ∈[ p ]⋆
_∷_ : ∀ {s₁ s₂ p} → s₁ ∈ p → s₂ ∈[ p ]⋆ → s₁ ++ s₂ ∈[ p ]⋆

module KleeneStar₁ where

infix 15 _⋆ _+

-- This definition requires that the argument recognisers are not
-- nullable.

mutual

_⋆ : P false → P true
p ⋆ = empty ∣ p +

_+ : P false → P false
p + = p · ♯ (p ⋆)

-- The definition of _⋆ above is correct.

⋆-sound : ∀ {s p} → s ∈ p ⋆ → s ∈[ p ]⋆
⋆-sound (∣-left  empty)       = []
⋆-sound (∣-right (pr₁ · pr₂)) = pr₁ ∷ ⋆-sound pr₂

⋆-complete : ∀ {s p} → s ∈[ p ]⋆ → s ∈ p ⋆
⋆-complete []                    = ∣-left empty
⋆-complete (_∷_ {[]}    pr₁ pr₂) = ⋆-complete pr₂
⋆-complete (_∷_ {_ ∷ _} pr₁ pr₂) =
∣-right {n₁ = true} (pr₁ · ⋆-complete pr₂)

module KleeneStar₂ where

infix 15 _⋆

-- This definition works for any argument recogniser.

_⋆ : ∀ {n} → P n → P true
_⋆ = KleeneStar₁._⋆ ∘ nonempty

-- The definition of _⋆ above is correct.

⋆-sound : ∀ {s n} {p : P n} → s ∈ p ⋆ → s ∈[ p ]⋆
⋆-sound (∣-left  empty)                = []
⋆-sound (∣-right (nonempty pr₁ · pr₂)) = pr₁ ∷ ⋆-sound pr₂

⋆-complete : ∀ {s n} {p : P n} → s ∈[ p ]⋆ → s ∈ p ⋆
⋆-complete []                    = ∣-left empty
⋆-complete (_∷_ {[]}    pr₁ pr₂) = ⋆-complete pr₂
⋆-complete (_∷_ {_ ∷ _} pr₁ pr₂) =
∣-right {n₁ = true} (nonempty pr₁ · ⋆-complete pr₂)

-- Note, however, that for actual parsing the corresponding
-- definition would not be correct. The reason is that p would give
-- a result also when the empty string was accepted, and these
-- results are ignored by the definition above. In the case of
-- actual parsing the result of p ⋆, when p is nullable, should be a
-- stream and not a finite list.

------------------------------------------------------------------------
-- A simplified sequencing operator

infixl 10 _⊙_

_⊙_ : ∀ {n₁ n₂} → P n₁ → P n₂ → P (n₁ ∧ n₂)
_⊙_ {n₁ = n₁} p₁ p₂ = ♯? p₁ · ♯? {b = n₁} p₂

module ⊙ where

complete : ∀ {n₁ n₂ s₁ s₂} {p₁ : P n₁} {p₂ : P n₂} →
s₁ ∈ p₁ → s₂ ∈ p₂ → s₁ ++ s₂ ∈ p₁ ⊙ p₂
complete {n₁} {n₂} s₁∈p₁ s₂∈p₂ = add-♭♯ n₂ s₁∈p₁ · add-♭♯ n₁ s₂∈p₂

infixl 10 _⊙′_
infix   4 _⊙_∋_

data _⊙_∋_ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) : List Tok → Set where
_⊙′_ : ∀ {s₁ s₂} (s₁∈p₁ : s₁ ∈ p₁) (s₂∈p₂ : s₂ ∈ p₂) →
p₁ ⊙ p₂ ∋ s₁ ++ s₂

sound : ∀ {n₁} n₂ {s} {p₁ : P n₁} {p₂ : P n₂} →
s ∈ p₁ ⊙ p₂ → p₁ ⊙ p₂ ∋ s
sound {n₁} n₂ (s₁∈p₁ · s₂∈p₂) = drop-♭♯ n₂ s₁∈p₁ ⊙′ drop-♭♯ n₁ s₂∈p₂

------------------------------------------------------------------------
-- A combinator which repeats a recogniser a fixed number of times

⟨_^_⟩-nullable : Bool → ℕ → Bool
⟨ n ^ zero  ⟩-nullable = true
⟨ n ^ suc i ⟩-nullable = n ∧ ⟨ n ^ i ⟩-nullable

infixl 15 _^_

_^_ : ∀ {n} → P n → (i : ℕ) → P ⟨ n ^ i ⟩-nullable
p ^ 0     = empty
p ^ suc i = p ⊙ p ^ i

-- Some lemmas relating _^_ to _⋆.

open KleeneStar₂

^≤⋆ : ∀ {n} {p : P n} i → p ^ i ≤ p ⋆
^≤⋆ {n} {p} i s∈ = ⋆-complete \$ helper i s∈
where
helper : ∀ i {s} → s ∈ p ^ i → s ∈[ p ]⋆
helper zero    empty          = []
helper (suc i) (s₁∈p · s₂∈pⁱ) =
drop-♭♯ ⟨ n ^ i ⟩-nullable s₁∈p ∷ helper i (drop-♭♯ n s₂∈pⁱ)

⋆≤^ : ∀ {n} {p : P n} {s} → s ∈ p ⋆ → ∃ λ i → s ∈ p ^ i
⋆≤^ {n} {p} s∈p⋆ = helper (⋆-sound s∈p⋆)
where
helper : ∀ {s} → s ∈[ p ]⋆ → ∃ λ i → s ∈ p ^ i
helper []             = (0 , empty)
helper (s₁∈p ∷ s₂∈p⋆) =
Prod.map suc (λ {i} s₂∈pⁱ → add-♭♯ ⟨ n ^ i ⟩-nullable s₁∈p ·
(helper s₂∈p⋆)

------------------------------------------------------------------------
-- A recogniser which only accepts a given token

module Tok (dec : Decidable (_≡_ {A = Tok})) where

tok : Tok → P false
tok t = sat (⌊_⌋ ∘ dec t)

sound : ∀ {s t} → s ∈ tok t → s ≡ [ t ]
sound (sat ok) = cong [_] \$ sym \$ toWitness ok

complete : ∀ {t} → [ t ] ∈ tok t
complete = sat (fromWitness refl)

------------------------------------------------------------------------
-- A recogniser which accepts the empty string iff the argument is
-- true (and never accepts non-empty strings)

accept-if-true : ∀ b → P b
accept-if-true true  = empty
accept-if-true false = fail

module AcceptIfTrue where

sound : ∀ b {s} → s ∈ accept-if-true b → s ≡ [] × T b
sound true  empty = (refl , _)
sound false ()

complete : ∀ {b} → T b → [] ∈ accept-if-true b
complete ok with Equivalence.to T-≡ ⟨\$⟩ ok
... | refl = empty
```