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

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

open import Codata.Musical.Notation
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 ·
                                add-♭♯ n                  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