------------------------------------------------------------------------
-- 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