------------------------------------------------------------------------
-- Infinite grammars
------------------------------------------------------------------------

-- The grammar language introduced below is not more expressive than
-- the one in Grammar.Infinite.Basic. There are two reasons for
-- introducing this new language:
--
-- ⑴ The function final-whitespace? below analyses the structure of a
--   grammar, and can in some cases automatically prove a certain
--   theorem. It is quite hard to analyse grammars that contain
--   unrestricted corecursion and/or the higher-order bind combinator,
--   so the new language contains extra constructors intended to make
--   the analysis easier (in some cases).
--
-- ⑵ The extra constructors can also make it easier to convince Agda's
--   termination checker that certain infinite grammars are
--   productive.

module Grammar.Infinite where

open import Algebra
open import Category.Monad
open import Coinduction
open import Data.Bool
open import Data.Char
open import Data.Colist using (Colist; []; _∷_; _∈_; here; there)
open import Data.Empty
open import Data.List as List
open import Data.List.NonEmpty as List⁺
  using (List⁺; _∷_; _∷⁺_; head; tail)
open import Data.List.Properties as List-prop using (module List-solver)
open import Data.Maybe as Maybe
open import Data.Nat
open import Data.Product as Prod
open import Data.String as String using (String)
open import Data.Unit
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Nullary

private
  module LM {A : Set} = Monoid (List.monoid A)
  open module MM {f} = RawMonadPlus (Maybe.monadPlus {f = f})
    using () renaming (_<$>_ to _<$>M_; _⊛_ to _⊛M_)

import Grammar.Infinite.Basic as Basic; open Basic._∈_·_
open import Utilities

------------------------------------------------------------------------
-- A grammar language that is less minimal than the one in
-- Grammar.Infinite.Basic

mutual

  infix  30 _⋆
  infixl 20 _<$>_ _<$_ _⊛_ _<⊛_ _⊛>_
  infixl 15 _>>=_
  infixl 10 _∣_

  data Grammar : Set  Set₁ where

    -- The empty string.

    return :  {A}  A  Grammar A

    -- A single, arbitrary token.

    token  : Grammar Char

    -- Monadic sequencing.

    _>>=_  :  {c₁ c₂ A B} 
             ∞Grammar c₁ A  (A  ∞Grammar c₂ B)  Grammar B

    -- Symmetric choice.

    _∣_    :  {c₁ c₂ A}  ∞Grammar c₁ A  ∞Grammar c₂ A  Grammar A

    -- Failure.

    fail   :  {A}  Grammar A

    -- A specific token.

    tok    : Char  Grammar Char

    -- Map.

    _<$>_  :  {c A B}  (A  B)  ∞Grammar c A  Grammar B
    _<$_   :  {c A B}  A  ∞Grammar c B  Grammar A

    -- Applicative sequencing.

    _⊛_    :  {c₁ c₂ A B} 
             ∞Grammar c₁ (A  B)  ∞Grammar c₂ A  Grammar B
    _<⊛_   :  {c₁ c₂ A B}  ∞Grammar c₁ A  ∞Grammar c₂ B  Grammar A
    _⊛>_   :  {c₁ c₂ A B}  ∞Grammar c₁ A  ∞Grammar c₂ B  Grammar B

    -- Kleene star.

    _⋆     :  {c A}  ∞Grammar c A  Grammar (List A)

  -- Coinductive if the argument is true.
  --
  -- Conditional coinduction is used to avoid having to write the
  -- delay operator (♯_) all the time.

  ∞Grammar : Bool  Set  Set₁
  ∞Grammar true  A =  (Grammar A)
  ∞Grammar false A =    Grammar A

-- Families of grammars for specific values.

Grammar-for : Set  Set₁
Grammar-for A = (x : A)  Grammar ( λ x′  x′  x)

-- Forcing of a conditionally coinductive grammar.

♭? :  {c A}  ∞Grammar c A  Grammar A
♭? {true}  = 
♭? {false} = id

-- A grammar combinator: Kleene plus.

infix 30 _+

_+ :  {c A}  ∞Grammar c A  Grammar (List⁺ A)
g + = _∷_ <$> g  g 

-- The semantics of "extended" grammars is given by translation to
-- simple grammars.

⟦_⟧ :  {A}  Grammar A  Basic.Grammar A
 return x   = Basic.return x
 token      = Basic.token
 g₁ >>= g₂  =   ♭? g₁  Basic.>>= λ x    ♭? (g₂ x) 
 g₁  g₂    =   ♭? g₁  Basic.∣   ♭? g₂ 
 fail       = Basic.fail
 tok t      = Basic.tok t
 f <$> g    =   ♭? g   Basic.>>= λ x   Basic.return (f x)
 x <$ g     =   ♭? g   Basic.>>= λ _   Basic.return x
 g₁  g₂    =   ♭? g₁  Basic.>>= λ f    f <$> g₂ 
 g₁ <⊛ g₂   =   ♭? g₁  Basic.>>= λ x    x <$  g₂ 
 g₁ ⊛> g₂   =   ♭? g₁  Basic.>>= λ _       ♭? g₂ 
 g         =  Basic.return [] Basic.∣   List⁺.toList <$> g + 

------------------------------------------------------------------------
-- More grammar combinators

mutual

  -- Combinators that transform families of grammars for certain
  -- elements to families of grammars for certain lists.

  list :  {A}  Grammar-for A  Grammar-for (List A)
  list elem []       = return ([] , refl)
  list elem (x  xs) =
    Prod.map List⁺.toList
              eq  P.cong₂ _∷_ (P.cong head eq) (P.cong tail eq)) <$>
      list⁺ elem (x  xs)

  list⁺ :  {A}  Grammar-for A  Grammar-for (List⁺ A)
  list⁺ elem (x  xs) =
    Prod.zip _∷_ (P.cong₂ _∷_) <$> elem x  list elem xs

-- Elements preceded by something.

infixl 18 _prec-by_

_prec-by_ :  {A B}  Grammar A  Grammar B  Grammar (List A)
g prec-by prec = (prec ⊛> g) 

-- Elements separated by something.

infixl 18 _sep-by_

_sep-by_ :  {A B}  Grammar A  Grammar B  Grammar (List⁺ A)
g sep-by sep = _∷_ <$> g  (g prec-by sep)

-- The empty string if the argument is true, otherwise failure.

if-true : (b : Bool)  Grammar (T b)
if-true true  = return tt
if-true false = fail

-- A token satisfying a given predicate.

sat : (p : Char  Bool)  Grammar ( λ t  T (p t))
sat p = token >>= λ t  _,_ t <$> if-true (p t)

-- A given token satisfying a given predicate.

tok-sat : (p : Char  Bool)  Grammar-for ( (T  p))
tok-sat p (t , pt) = ((t , pt) , refl) <$ tok t

-- Whitespace.

whitespace : Grammar Char
whitespace = tok ' '  tok '\n'

-- The given string.

string : List Char  Grammar (List Char)
string []      = return []
string (t  s) = _∷_ <$> tok t  string s

-- A variant of string that takes a String rather than a list of
-- characters.

string′ : String  Grammar (List Char)
string′ = string  String.toList

-- The given string, possibly followed by some whitespace.

symbol : List Char  Grammar (List Char)
symbol s = string s <⊛ whitespace 

symbol′ : String  Grammar (List Char)
symbol′ = symbol  String.toList

------------------------------------------------------------------------
-- Alternative definition of the semantics

-- Pattern matching on values of type x Basic.∈ ⟦ g₁ ⊛ g₂ ⟧ · s (say)
-- is somewhat inconvenient: the patterns have the form
-- (>>=-sem _ (>>=-sem _ return-sem)). The following, direct
-- definition of the semantics may be easier to use.

infix 4 _∈_·_

data _∈_·_ :  {A}  A  Grammar A  List Char  Set₁ where
  return-sem :  {A} {x : A}  x  return x · []
  token-sem  :  {t}  t  token · [ t ]
  >>=-sem    :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A}
                 {g₂ : A  ∞Grammar c₂ B} {x y s₁ s₂} 
               x  ♭? g₁ · s₁  y  ♭? (g₂ x) · s₂ 
               y  g₁ >>= g₂ · s₁ ++ s₂
  left-sem   :  {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A}
                 {x s} 
               x  ♭? g₁ · s  x  g₁  g₂ · s
  right-sem  :  {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A}
                 {x s} 
               x  ♭? g₂ · s  x  g₁  g₂ · s
  tok-sem    :  {t}  t  tok t · [ t ]
  <$>-sem    :  {c A B} {f : A  B} {g : ∞Grammar c A} {x s} 
               x  ♭? g · s  f x  f <$> g · s
  <$-sem     :  {c A B} {x : A} {g : ∞Grammar c B} {y s} 
               y  ♭? g · s  x  x <$ g · s
  ⊛-sem      :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ (A  B)}
                 {g₂ : ∞Grammar c₂ A} {f x s₁ s₂} 
               f  ♭? g₁ · s₁  x  ♭? g₂ · s₂ 
               f x  g₁  g₂ · s₁ ++ s₂
  <⊛-sem     :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B}
                 {x y s₁ s₂} 
               x  ♭? g₁ · s₁  y  ♭? g₂ · s₂ 
               x  g₁ <⊛ g₂ · s₁ ++ s₂
  ⊛>-sem     :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B}
                 {x y s₁ s₂} 
               x  ♭? g₁ · s₁  y  ♭? g₂ · s₂ 
               y  g₁ ⊛> g₂ · s₁ ++ s₂
  ⋆-[]-sem   :  {c A} {g : ∞Grammar c A} 
               []  g  · []
  ⋆-+-sem    :  {c A} {g : ∞Grammar c A} {x xs s} 
               (x  xs)  g + · s  x  xs  g  · s

-- A weak form of "local unambiguity", unambiguity for a given string.
-- (Note that the parse trees are not required to be equal.)

Locally-unambiguous :  {A}  Grammar A  List Char  Set₁
Locally-unambiguous g s =  {x y}  x  g · s  y  g · s  x  y

-- A weak form of unambiguity.

Unambiguous :  {A}  Grammar A  Set₁
Unambiguous g =  {s}  Locally-unambiguous g s

-- Parsers.

Parser :  {A}  Grammar A  Set₁
Parser g =  s  Dec ( λ x  x  g · s)

-- Cast lemma.

cast :  {A} {g : Grammar A} {x s₁ s₂} 
       s₁  s₂  x  g · s₁  x  g · s₂
cast refl = id

-- The alternative semantics is isomorphic to the one above.

isomorphic :  {A x s} {g : Grammar A} 
             x  g · s  x Basic.∈  g  · s
isomorphic {g = g} = record
  { to         = P.→-to-⟶ sound
  ; from       = P.→-to-⟶ (complete g)
  ; inverse-of = record
    { left-inverse-of  = complete∘sound
    ; right-inverse-of = sound∘complete g
    }
  }
  where

  -- Some short lemmas.

  lemma₁ :  s  s ++ []  s
  lemma₁ = proj₂ LM.identity

  lemma₂ :  s₁ s₂  s₁ ++ s₂ ++ []  s₁ ++ s₂
  lemma₂ s₁ s₂ = P.cong (_++_ s₁) (lemma₁ s₂)

  lemma₃ :  s₁ s₂  s₁ ++ s₂  ((s₁ ++ []) ++ s₂ ++ []) ++ []
  lemma₃ s₁ s₂ = begin
    s₁ ++ s₂                        ≡⟨ P.cong₂ _++_ (P.sym $ lemma₁ s₁) (P.sym $ lemma₁ s₂) 
    (s₁ ++ []) ++ s₂ ++ []          ≡⟨ P.sym $ lemma₁ _ 
    ((s₁ ++ []) ++ s₂ ++ []) ++ []  
    where open P.≡-Reasoning

  tok-lemma :  {t t′ s}  t  t′ × s  [ t ]  t′  tok t · s
  tok-lemma (refl , refl) = tok-sem

  -- Soundness.

  sound :  {A x s} {g : Grammar A}  x  g · s  x Basic.∈  g  · s
  sound return-sem               = return-sem
  sound token-sem                = token-sem
  sound (>>=-sem x∈ y∈)          = >>=-sem (sound x∈) (sound y∈)
  sound (left-sem x∈)            = left-sem (sound x∈)
  sound (right-sem x∈)           = right-sem (sound x∈)
  sound tok-sem                  = Inverse.from Basic.tok-sem
                                     ⟨$⟩ (refl , refl)
  sound (<$>-sem x∈)             = Basic.cast (lemma₁ _)
                                     (>>=-sem (sound x∈) return-sem)
  sound (<$-sem x∈)              = Basic.cast (lemma₁ _)
                                     (>>=-sem (sound x∈) return-sem)
  sound (⊛-sem {s₁ = s₁} f∈ x∈)  = Basic.cast (lemma₂ s₁ _)
                                     (>>=-sem (sound f∈)
                                        (>>=-sem (sound x∈) return-sem))
  sound (<⊛-sem {s₁ = s₁} x∈ y∈) = Basic.cast (lemma₂ s₁ _)
                                     (>>=-sem (sound x∈)
                                        (>>=-sem (sound y∈) return-sem))
  sound (⊛>-sem {s₁ = s₁} x∈ y∈) = >>=-sem (sound x∈) (sound y∈)
  sound ⋆-[]-sem                 = left-sem return-sem
  sound (⋆-+-sem xs∈)            = Basic.cast (lemma₁ _)
                                     (right-sem
                                        (>>=-sem (sound xs∈)
                                                 return-sem))

  -- Completeness.

  complete :  {A x s} (g : Grammar A)  x Basic.∈  g  · s  x  g · s
  complete (return x)  return-sem      = return-sem
  complete token       token-sem       = token-sem
  complete (g₁ >>= g₂) (>>=-sem x∈ y∈) = >>=-sem (complete _ x∈)
                                                 (complete _ y∈)
  complete (g₁  g₂)   (left-sem x∈)   = left-sem  (complete _ x∈)
  complete (g₁  g₂)   (right-sem x∈)  = right-sem (complete _ x∈)

  complete fail    ∈fail = ⊥-elim (Basic.fail-sem⁻¹ ∈fail)
  complete (tok t) t∈    = tok-lemma (Inverse.to Basic.tok-sem ⟨$⟩ t∈)

  complete (f <$> g) (>>=-sem x∈ return-sem) =
    cast (P.sym $ lemma₁ _)
         (<$>-sem (complete _ x∈))
  complete (x <$ g) (>>=-sem x∈ return-sem) =
    cast (P.sym $ lemma₁ _)
         (<$-sem (complete _ x∈))
  complete (g₁  g₂) (>>=-sem {s₁ = s₁} f∈ (>>=-sem x∈ return-sem)) =
    cast (P.sym $ lemma₂ s₁ _)
         (⊛-sem (complete _ f∈) (complete _ x∈))
  complete (g₁ <⊛ g₂) (>>=-sem {s₁ = s₁} x∈ (>>=-sem y∈ return-sem)) =
    cast (P.sym $ lemma₂ s₁ _)
         (<⊛-sem (complete _ x∈) (complete _ y∈))
  complete (g₁ ⊛> g₂) (>>=-sem x∈ y∈) =
    ⊛>-sem (complete _ x∈) (complete _ y∈)

  complete (g ) (left-sem return-sem) = ⋆-[]-sem
  complete (g ) (right-sem (>>=-sem
                    (>>=-sem (>>=-sem {s₁ = s₁} x∈  return-sem)
                             (>>=-sem           xs∈ return-sem))
                    return-sem)) =
    cast (lemma₃ s₁ _)
         (⋆-+-sem (⊛-sem (<$>-sem (complete _ x∈)) (complete _ xs∈)))

  -- More short lemmas.

  sound-cast :
     {A x s₁ s₂}
    (g : Grammar A) (eq : s₁  s₂) (x∈ : x  g · s₁) 
    sound (cast eq x∈)  Basic.cast eq (sound x∈)
  sound-cast _ refl _ = refl

  complete-cast :
     {A x s₁ s₂}
    (g : Grammar A) (eq : s₁  s₂) (x∈ : x Basic.∈  g  · s₁) 
    complete g (Basic.cast eq x∈)  cast eq (complete g x∈)
  complete-cast _ refl _ = refl

  cast-cast :
     {A} {x : A} {s₁ s₂ g} (eq : s₁  s₂) {x∈ : x Basic.∈ g · s₁} 
    Basic.cast (P.sym eq) (Basic.cast eq x∈)  x∈
  cast-cast refl = refl

  cast-cast′ :
     {A} {x : A} {s₁ s₂ g}
    (eq₁ : s₂  s₁) (eq₂ : s₁  s₂) {x∈ : x Basic.∈ g · s₁} 
    Basic.cast eq₁ (Basic.cast eq₂ x∈)  x∈
  cast-cast′ refl refl = refl

  -- The functions sound and complete are inverses.

  complete∘sound :  {A x s} {g : Grammar A} (x∈ : x  g · s) 
                   complete g (sound x∈)  x∈
  complete∘sound return-sem      = refl
  complete∘sound token-sem       = refl
  complete∘sound (>>=-sem x∈ y∈) = P.cong₂ >>=-sem (complete∘sound x∈)
                                                   (complete∘sound y∈)
  complete∘sound (left-sem x∈)   = P.cong left-sem (complete∘sound x∈)
  complete∘sound (right-sem x∈)  = P.cong right-sem (complete∘sound x∈)

  complete∘sound (tok-sem {t = t})
    rewrite Inverse.right-inverse-of (Basic.tok-sem {t = t})
                                     (refl , refl)
    = refl

  complete∘sound (<$>-sem {s = s} x∈) with sound x∈ | complete∘sound x∈
  complete∘sound (<$>-sem {f = f} {g = g} {s = s}
                          .(complete _ x∈′)) | x∈′ | refl
    rewrite complete-cast (f <$> g) (lemma₁ s) (>>=-sem x∈′ return-sem)
          | lemma₁ s
    = refl

  complete∘sound (<$-sem {x = x} {g = g} {s = s} x∈) with sound x∈ | complete∘sound x∈
  complete∘sound (<$-sem {x = x} {g = g} {s = s}
                         .(complete _ x∈′)) | x∈′ | refl
    rewrite complete-cast (x <$ g) (lemma₁ s) (>>=-sem x∈′ return-sem)
          | lemma₁ s
    = refl

  complete∘sound (⊛-sem f∈ x∈) with sound f∈ | complete∘sound f∈
                                  | sound x∈ | complete∘sound x∈
  complete∘sound (⊛-sem {g₁ = g₁} {g₂ = g₂} {s₁ = s₁} {s₂ = s₂}
                        .(complete _ f∈′) .(complete _ x∈′))
    | f∈′ | refl | x∈′ | refl
    rewrite complete-cast (g₁  g₂) (lemma₂ s₁ s₂)
                          (>>=-sem f∈′ (>>=-sem x∈′ return-sem))
          | lemma₁ s₂
    = refl

  complete∘sound (<⊛-sem x∈ y∈) with sound x∈ | complete∘sound x∈
                                   | sound y∈ | complete∘sound y∈
  complete∘sound (<⊛-sem {g₁ = g₁} {g₂ = g₂} {s₁ = s₁} {s₂ = s₂}
                         .(complete _ x∈′) .(complete _ y∈′))
    | x∈′ | refl | y∈′ | refl
    rewrite complete-cast (g₁ <⊛ g₂) (lemma₂ s₁ s₂)
                          (>>=-sem x∈′ (>>=-sem y∈′ return-sem))
          | lemma₁ s₂
    = refl

  complete∘sound (⊛>-sem x∈ y∈) with sound x∈ | complete∘sound x∈
                                   | sound y∈ | complete∘sound y∈
  complete∘sound (⊛>-sem .(complete _ x∈′) .(complete _ y∈′))
    | x∈′ | refl | y∈′ | refl
    = refl

  complete∘sound ⋆-[]-sem      = refl
  complete∘sound (⋆-+-sem xs∈) with sound xs∈ | complete∘sound xs∈
  complete∘sound (⋆-+-sem {g = g}
                    .(complete _ (>>=-sem (>>=-sem x∈   return-sem)
                                          (>>=-sem xs∈′ return-sem))))
    | >>=-sem (>>=-sem {s₁ = s₁} x∈   return-sem)
              (>>=-sem {s₁ = s₂} xs∈′ return-sem)
    | refl
    rewrite complete-cast (g ) (lemma₁ ((s₁ ++ []) ++ s₂ ++ []))
                          (right-sem
                            (>>=-sem (>>=-sem (>>=-sem x∈   return-sem)
                                              (>>=-sem xs∈′ return-sem))
                                     return-sem))
          | lemma₁ s₁ | lemma₁ s₂ | lemma₁ (s₁ ++ s₂)
    = refl

  sound∘complete :  {A x s}
                   (g : Grammar A) (x∈ : x Basic.∈  g  · s) 
                   sound (complete g x∈)  x∈
  sound∘complete (return x)  return-sem      = refl
  sound∘complete token       token-sem       = refl
  sound∘complete (g₁ >>= g₂) (>>=-sem x∈ y∈) = P.cong₂ >>=-sem (sound∘complete (♭? g₁) x∈)
                                                               (sound∘complete (♭? (g₂ _)) y∈)
  sound∘complete (g₁  g₂)   (left-sem x∈)   = P.cong left-sem  (sound∘complete (♭? g₁) x∈)
  sound∘complete (g₁  g₂)   (right-sem x∈)  = P.cong right-sem (sound∘complete (♭? g₂) x∈)

  sound∘complete fail    ∈fail = ⊥-elim (Basic.fail-sem⁻¹ ∈fail)
  sound∘complete (tok t) t∈    =
    helper _ (Inverse.left-inverse-of Basic.tok-sem t∈)
    where
    helper :  {t t′ s} {t∈ : t′ Basic.∈ Basic.tok t · s}
             (eqs : t  t′ × s  [ t ]) 
             Inverse.from Basic.tok-sem ⟨$⟩ eqs  t∈ 
             sound (tok-lemma eqs)  t∈
    helper (refl , refl) ≡t∈ = ≡t∈

  sound∘complete (f <$> g) (>>=-sem x∈ return-sem)
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
  sound∘complete (f <$> g) (>>=-sem {s₁ = s₁} .(sound x∈′) return-sem)
    | x∈′ | refl
    rewrite sound-cast (f <$> g) (P.sym $ lemma₁ s₁) (<$>-sem x∈′)
    = cast-cast (lemma₁ s₁)

  sound∘complete (x <$ g) (>>=-sem x∈ return-sem)
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
  sound∘complete (x <$ g) (>>=-sem {s₁ = s₁} .(sound x∈′) return-sem)
    | x∈′ | refl
    rewrite sound-cast (x <$ g) (P.sym $ lemma₁ s₁) (<$-sem x∈′)
    = cast-cast (lemma₁ s₁)

  sound∘complete (g₁  g₂) (>>=-sem f∈ (>>=-sem x∈ return-sem))
    with complete (♭? g₁) f∈ | sound∘complete (♭? g₁) f∈
       | complete (♭? g₂) x∈ | sound∘complete (♭? g₂) x∈
  sound∘complete (g₁  g₂)
    (>>=-sem {s₁ = s₁} .(sound f∈′)
             (>>=-sem {s₁ = s₂} .(sound x∈′) return-sem))
    | f∈′ | refl | x∈′ | refl
    rewrite sound-cast (g₁  g₂) (P.sym $ lemma₂ s₁ s₂) (⊛-sem f∈′ x∈′)
    = cast-cast (lemma₂ s₁ s₂)

  sound∘complete (g₁ <⊛ g₂) (>>=-sem x∈ (>>=-sem y∈ return-sem))
    with complete (♭? g₁) x∈ | sound∘complete (♭? g₁) x∈
       | complete (♭? g₂) y∈ | sound∘complete (♭? g₂) y∈
  sound∘complete (g₁ <⊛ g₂)
    (>>=-sem {s₁ = s₁} .(sound x∈′)
             (>>=-sem {s₁ = s₂} .(sound y∈′) return-sem))
    | x∈′ | refl | y∈′ | refl
    rewrite sound-cast (g₁ <⊛ g₂) (P.sym $ lemma₂ s₁ s₂) (<⊛-sem x∈′ y∈′)
    = cast-cast (lemma₂ s₁ s₂)

  sound∘complete (g₁ ⊛> g₂) (>>=-sem x∈ y∈)
    with complete (♭? g₁) x∈ | sound∘complete (♭? g₁) x∈
       | complete (♭? g₂) y∈ | sound∘complete (♭? g₂) y∈
  sound∘complete (g₁ ⊛> g₂) (>>=-sem .(sound x∈′) .(sound y∈′))
    | x∈′ | refl | y∈′ | refl
    = refl

  sound∘complete (g ) (left-sem return-sem) = refl
  sound∘complete (g )
    (right-sem
       (>>=-sem (>>=-sem (>>=-sem x∈  return-sem)
                         (>>=-sem xs∈ return-sem))
                return-sem))
    with complete (♭? g) x∈ | sound∘complete (♭? g) x∈
       | complete (g ) xs∈ | sound∘complete (g ) xs∈
  sound∘complete (g )
    (right-sem
       (>>=-sem (>>=-sem (>>=-sem {s₁ = s₁} .(sound x∈′)  return-sem)
                         (>>=-sem {s₁ = s₂} .(sound xs∈′) return-sem))
                return-sem))
    | x∈′ | refl | xs∈′ | refl
    rewrite sound-cast (g ) (lemma₃ s₁ s₂)
                       (⋆-+-sem (⊛-sem (<$>-sem x∈′) xs∈′))
    = lemma g (lemma₃ s₁ s₂) (lemma₁ (s₁ ++ s₂))
              (lemma₂ s₁ s₂) (lemma₁ s₁)
              (>>=-sem (sound x∈′)  return-sem)
              (>>=-sem (sound xs∈′) return-sem)
    where
    lemma :
       {c A} {f : List A  List⁺ A} {xs s₁ s₁++s₂ s₁++[] s₂++[]}
      (g   : ∞Grammar c A)
      (eq₁ : s₁++s₂  (s₁++[] ++ s₂++[]) ++ [])
      (eq₂ : (s₁++s₂) ++ []  s₁++s₂)
      (eq₃ : s₁ ++ s₂++[]  s₁++s₂)
      (eq₄ : s₁++[]  s₁)
      (f∈  : f  Basic.∈  _∷_ <$> g  · s₁++[])
      (xs∈ : xs Basic.∈  f <$> g   · s₂++[]) 
      _≡_ {A = List⁺.toList xs Basic.∈  g   · _}
          (Basic.cast eq₁
             (Basic.cast eq₂
                (right-sem
                   (>>=-sem
                      (Basic.cast eq₃ (>>=-sem (Basic.cast eq₄ f∈) xs∈))
                      return-sem))))
          (right-sem (>>=-sem (>>=-sem f∈ xs∈) return-sem))
    lemma _ eq₁ eq₂ refl refl _ _ = cast-cast′ eq₁ eq₂

------------------------------------------------------------------------
-- Semantics combinators

+-sem :  {c A} {g : ∞Grammar c A} {x xs s₁ s₂} 
        x  ♭? g · s₁  xs  g  · s₂  (x  xs)  g + · s₁ ++ s₂
+-sem x∈ xs∈ = ⊛-sem (<$>-sem x∈) xs∈

⋆-∷-sem :  {c A} {g : ∞Grammar c A} {x xs s₁ s₂} 
          x  ♭? g · s₁  xs  g  · s₂  x  xs  g  · s₁ ++ s₂
⋆-∷-sem x∈ xs∈ = ⋆-+-sem (+-sem x∈ xs∈)

⋆-⋆-sem :  {c A} {g : ∞Grammar c A} {xs₁ xs₂ s₁ s₂} 
          xs₁  g  · s₁  xs₂  g  · s₂  xs₁ ++ xs₂  g  · s₁ ++ s₂
⋆-⋆-sem ⋆-[]-sem xs₂∈ = xs₂∈
⋆-⋆-sem (⋆-+-sem (⊛-sem (<$>-sem {s = s₁} x∈) xs₁∈)) xs₂∈ =
  cast (P.sym $ LM.assoc s₁ _ _)
       (⋆-∷-sem x∈ (⋆-⋆-sem xs₁∈ xs₂∈))

+-∷-sem :  {c A} {g : ∞Grammar c A} {x xs s₁ s₂} 
          x  ♭? g · s₁  xs  g + · s₂  x ∷⁺ xs  g + · s₁ ++ s₂
+-∷-sem x∈ xs∈ = +-sem x∈ (⋆-+-sem xs∈)

mutual

  list-sem :  {A} {g : Grammar-for A} {s : A  List Char} 
             (∀ x  (x , refl)  g x · s x) 
              xs  (xs , refl)  list g xs · concat (List.map s xs)
  list-sem elem []       = return-sem
  list-sem elem (x  xs) = <$>-sem (list⁺-sem elem (x  xs))

  list⁺-sem :
     {A} {g : Grammar-for A} {s : A  List Char} 
    (∀ x  (x , refl)  g x · s x) 
     xs  (xs , refl)  list⁺ g xs ·
           concat (List.map s (List⁺.toList xs))
  list⁺-sem elem (x  xs) = ⊛-sem (<$>-sem (elem x)) (list-sem elem xs)

sep-by-sem-singleton :
   {A B} {g : Grammar A} {sep : Grammar B} {x s} 
  x  g · s  x  []  g sep-by sep · s
sep-by-sem-singleton x∈ =
  cast (proj₂ LM.identity _)
             (⊛-sem (<$>-sem x∈) ⋆-[]-sem)

sep-by-sem-∷ :
   {A B} {g : Grammar A} {sep : Grammar B} {x y xs s₁ s₂ s₃} 
  x  g · s₁  y  sep · s₂  xs  g sep-by sep · s₃ 
  x ∷⁺ xs  g sep-by sep · s₁ ++ s₂ ++ s₃
sep-by-sem-∷ {s₂ = s₂} x∈ y∈ (⊛-sem (<$>-sem x′∈) xs∈) =
  ⊛-sem (<$>-sem x∈)
        (cast (LM.assoc s₂ _ _)
              (⋆-∷-sem (⊛>-sem y∈ x′∈) xs∈))

if-true-sem :  {b} (t : T b)  t  if-true b · []
if-true-sem {b = true}  _  = return-sem
if-true-sem {b = false} ()

sat-sem :  {p : Char  Bool} {t} (pt : T (p t)) 
          (t , pt)  sat p · [ t ]
sat-sem pt = >>=-sem token-sem (<$>-sem (if-true-sem pt))

tok-sat-sem :  {p : Char  Bool} {t} (pt : T (p t)) 
              ((t , pt) , refl)  tok-sat p (t , pt) · [ t ]
tok-sat-sem _ = <$-sem tok-sem

list-sem-lemma :  {A} {x : A} {g s} 
                 x  g · concat (List.map [_] s)  x  g · s
list-sem-lemma = cast (List-prop.Monad.right-identity _)

single-space-sem : (' '  [])  whitespace + · String.toList " "
single-space-sem = +-sem (left-sem tok-sem) ⋆-[]-sem

string-sem′ :  {s s′ s″}  s  string s′ · s″  (s  s′ × s′  s″)
string-sem′ = record
  { to         = P.→-to-⟶ (to _)
  ; from       = P.→-to-⟶ (from _)
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = to∘from _
    }
  }
  where
  to :  {s} s′ {s″}  s  string s′ · s″  s  s′ × s′  s″
  to []       return-sem                   = (refl , refl)
  to (c  s′) (⊛-sem (<$>-sem tok-sem) s∈) =
    Prod.map (P.cong (_∷_ c)) (P.cong (_∷_ c)) $ to s′ s∈

  from :  {s} s′ {s″}  s  s′ × s′  s″  s  string s′ · s″
  from []       (refl , refl) = return-sem
  from (c  s′) (refl , refl) =
    ⊛-sem (<$>-sem tok-sem) (from s′ (refl , refl))

  from∘to :  {s} s′ {s″} (s∈ : s  string s′ · s″) 
            from s′ (to s′ s∈)  s∈
  from∘to []       return-sem                   = refl
  from∘to (c  s′) (⊛-sem (<$>-sem tok-sem) s∈)
    with to s′ s∈ | from∘to s′ s∈
  from∘to (c  s′) (⊛-sem (<$>-sem tok-sem) .(from s′ (refl , refl)))
    | (refl , refl) | refl = refl

  to∘from :  {s} s′ {s″} (eqs : s  s′ × s′  s″) 
            to s′ (from s′ eqs)  eqs
  to∘from []       (refl , refl) = refl
  to∘from (c  s′) (refl , refl)
    rewrite to∘from s′ (refl , refl)
    = refl

string-sem :  {s}  s  string s · s
string-sem = Inverse.from string-sem′ ⟨$⟩ (refl , refl)

------------------------------------------------------------------------
-- Expressiveness

-- Every language that can be recursively enumerated can be
-- represented by a (unit-valued) grammar.
--
-- Note that, given a Turing machine that halts and accepts for
-- certain strings, and runs forever for other strings, one can define
-- a potentially infinite list of type Colist (Maybe (List Char)) that
-- contains exactly the strings accepted by the Turing machine
-- (assuming that there is some way to construct a stream containing
-- all strings of type List Char).

expressive : (enumeration : Colist (Maybe (List Char))) 
              λ (g : Grammar ) 
                {s}  tt  g · s  just s  enumeration
expressive ss = (g ss , g-sem ss)
  where
  maybe-string : Maybe (List Char)  Grammar 
  maybe-string nothing  = fail
  maybe-string (just s) = tt <$ string s

  g : Colist (Maybe (List Char))  Grammar 
  g []       = fail
  g (s  ss) = maybe-string s   g ( ss)

  maybe-string-sem :  {m s}  tt  maybe-string m · s  just s  m
  maybe-string-sem {nothing} = record
    { to         = P.→-to-⟶  ())
    ; from       = P.→-to-⟶  ())
    ; inverse-of = record
      { left-inverse-of  = λ ()
      ; right-inverse-of = λ ()
      }
    }
  maybe-string-sem {just s} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = to∘from
      }
    }
    where
    to :  {s′} 
         tt  tt <$ string s · s′  Maybe.Maybe.just s′  just s
    to (<$-sem s∈) =
      P.sym $ P.cong just $ proj₂ (Inverse.to string-sem′ ⟨$⟩ s∈)

    from :  {s′} 
           Maybe.Maybe.just s′  just s  tt  tt <$ string s · s′
    from refl = <$-sem (Inverse.from string-sem′ ⟨$⟩ (refl , refl))

    from∘to :  {s′} (tt∈ : tt  tt <$ string s · s′) 
              from (to tt∈)  tt∈
    from∘to (<$-sem s∈)
      with Inverse.to string-sem′ ⟨$⟩ s∈
         | Inverse.left-inverse-of string-sem′ s∈
    from∘to (<$-sem .(Inverse.from string-sem′ ⟨$⟩ (refl , refl)))
      | (refl , refl) | refl = refl

    to∘from :  {s′} (eq : Maybe.Maybe.just s′  just s) 
              to (from eq)  eq
    to∘from refl
      rewrite Inverse.right-inverse-of
                (string-sem′ {s = s}) (refl , refl)
      = refl

  g-sem :  ss {s}  tt  g ss · s  just s  ss
  g-sem ss = record
    { to         = P.→-to-⟶ (to   ss)
    ; from       = P.→-to-⟶ (from ss)
    ; inverse-of = record
      { left-inverse-of  = from∘to ss
      ; right-inverse-of = to∘from ss
      }
    }
    where
    to :  ss {s}  tt  g ss · s  just s  ss
    to []       ()
    to (s  ss) (left-sem  tt∈) = here (Inverse.to maybe-string-sem ⟨$⟩ tt∈)
    to (s  ss) (right-sem tt∈) = there (to ( ss) tt∈)

    from :  ss {s}  just s  ss  tt  g ss · s
    from []       ()
    from (s  ss) (here eq) = left-sem (Inverse.from maybe-string-sem ⟨$⟩ eq)
    from (s  ss) (there p) = right-sem (from ( ss) p)

    from∘to :  ss {s} (tt∈ : tt  g ss · s)  from ss (to ss tt∈)  tt∈
    from∘to []       ()
    from∘to (s  ss) (right-sem tt∈) = P.cong right-sem (from∘to ( ss) tt∈)
    from∘to (s  ss) (left-sem  tt∈) =
      P.cong left-sem (Inverse.left-inverse-of maybe-string-sem tt∈)

    to∘from :  ss {s} (eq : just s  ss)  to ss (from ss eq)  eq
    to∘from []       ()
    to∘from (s  ss) (there p) = P.cong there (to∘from ( ss) p)
    to∘from (s  ss) (here eq) =
      P.cong here (Inverse.right-inverse-of maybe-string-sem eq)

------------------------------------------------------------------------
-- Detecting the whitespace combinator

-- A predicate for the whitespace combinator.

data Is-whitespace :  {A}  Grammar A  Set₁ where
  is-whitespace : Is-whitespace whitespace

-- Detects the whitespace combinator.

is-whitespace? :  {A} (g : Grammar A)  Maybe (Is-whitespace g)
is-whitespace? (_∣_ {c₁ = false} {c₂ = false} (tok ' ') g) =
  helper _ refl
  where
  helper :  {A} (g : Grammar A) (eq : A  Char) 
           Maybe (Is-whitespace (tok ' '  P.subst Grammar eq g))
  helper (tok '\n') refl = just is-whitespace
  helper _          _    = nothing

is-whitespace? _ = nothing

------------------------------------------------------------------------
-- Trailing whitespace

-- A predicate for grammars that can "swallow" extra trailing
-- whitespace.

Trailing-whitespace :  {A}  Grammar A  Set₁
Trailing-whitespace g =
   {x s}  x  g <⊛ whitespace  · s  x  g · s

-- A similar but weaker property.

Trailing-whitespace′ :  {A}  Grammar A  Set₁
Trailing-whitespace′ g =
   {x s s₁ s₂} 
  x  g · s₁  s  whitespace  · s₂   λ y  y  g · s₁ ++ s₂

-- A heuristic (and rather incomplete) procedure that either proves
-- that a production can swallow trailing whitespace (in the weaker
-- sense), or returns "don't know" as the answer.
--
-- The natural number n is used to ensure termination.

trailing-whitespace′ :  (n : ) {A} (g : Grammar A) 
                       Maybe (Trailing-whitespace′ g)
trailing-whitespace′ = trailing?
  where
  <$>-lemma :  {c A B} {f : A  B} {g : ∞Grammar c A} 
              Trailing-whitespace′ (♭? g) 
              Trailing-whitespace′ (f <$> g)
  <$>-lemma t (<$>-sem x∈) w = , <$>-sem (proj₂ $ t x∈ w)

  <$-lemma :  {c A B} {x : A} {g : ∞Grammar c B} 
             Trailing-whitespace′ (♭? g) 
             Trailing-whitespace′ (x <$ g)
  <$-lemma t (<$-sem x∈) w = , <$-sem (proj₂ $ t x∈ w)

  ⊛-lemma :  {c₁ c₂ A B}
              {g₁ : ∞Grammar c₁ (A  B)} {g₂ : ∞Grammar c₂ A} 
            Trailing-whitespace′ (♭? g₂) 
            Trailing-whitespace′ (g₁  g₂)
  ⊛-lemma t₂ (⊛-sem {s₁ = s₁} f∈ x∈) w =
    , cast (P.sym $ LM.assoc s₁ _ _)
           (⊛-sem f∈ (proj₂ $ t₂ x∈ w))

  <⊛-lemma :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} 
             Trailing-whitespace′ (♭? g₂) 
             Trailing-whitespace′ (g₁ <⊛ g₂)
  <⊛-lemma t₂ (<⊛-sem {s₁ = s₁} x∈ y∈) w =
    , cast (P.sym $ LM.assoc s₁ _ _)
           (<⊛-sem x∈ (proj₂ $ t₂ y∈ w))

  ⊛>-lemma :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} 
             Trailing-whitespace′ (♭? g₂) 
             Trailing-whitespace′ (g₁ ⊛> g₂)
  ⊛>-lemma t₂ (⊛>-sem {s₁ = s₁} x∈ y∈) w =
    , cast (P.sym $ LM.assoc s₁ _ _)
           (⊛>-sem x∈ (proj₂ $ t₂ y∈ w))

  ∣-lemma :  {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} 
            Trailing-whitespace′ (♭? g₁) 
            Trailing-whitespace′ (♭? g₂) 
            Trailing-whitespace′ (g₁  g₂)
  ∣-lemma t₁ t₂ (left-sem  x∈) w = , left-sem  (proj₂ $ t₁ x∈ w)
  ∣-lemma t₁ t₂ (right-sem x∈) w = , right-sem (proj₂ $ t₂ x∈ w)

  whitespace⋆-lemma :
     {A} {g : Grammar A} 
    Is-whitespace g 
    Trailing-whitespace′ (g )
  whitespace⋆-lemma is-whitespace xs∈ w = , ⋆-⋆-sem xs∈ w

  trailing? :    {A} (g : Grammar A)  Maybe (Trailing-whitespace′ g)
  trailing? (suc n) fail               = just  ())
  trailing? (suc n) (f <$> g)          = <$>-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (x <$ g)           = <$-lemma  <$>M trailing? n (♭? g)
  trailing? (suc n) (g₁  g₂)          = ⊛-lemma   <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁ <⊛ g₂)         = <⊛-lemma  <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁ ⊛> g₂)         = ⊛>-lemma  <$>M trailing? n (♭? g₂)
  trailing? (suc n) (g₁  g₂)          = ∣-lemma   <$>M trailing? n (♭? g₁)
                                                     ⊛M trailing? n (♭? g₂)
  trailing? (suc n) (_⋆ {c = false} g) = whitespace⋆-lemma <$>M
                                           is-whitespace? g
  trailing? _       _                  = nothing

-- A heuristic (and rather incomplete) procedure that either proves
-- that a production can swallow trailing whitespace, or returns
-- "don't know" as the answer.
--
-- The natural number n is used to ensure termination.

trailing-whitespace :  (n : ) {A} (g : Grammar A) 
                      Maybe (Trailing-whitespace g)
trailing-whitespace n g = convert <$>M trailing? n g
  where
  -- An alternative formulation of Trailing-whitespace.

  Trailing-whitespace″ :  {A}  Grammar A  Set₁
  Trailing-whitespace″ g =
     {x s s₁ s₂} 
    x  g · s₁  s  whitespace  · s₂  x  g · s₁ ++ s₂

  convert :  {A} {g : Grammar A} 
            Trailing-whitespace″ g  Trailing-whitespace g
  convert t (<⊛-sem x∈ w) = t x∈ w

  ++-lemma = solve 2  a b  (a  b)  nil  (a  nil)  b) refl
    where open List-solver

  <$>-lemma :  {c A B} {f : A  B} {g : ∞Grammar c A} 
              Trailing-whitespace″ (♭? g) 
              Trailing-whitespace″ (f <$> g)
  <$>-lemma t (<$>-sem x∈) w = <$>-sem (t x∈ w)

  <$-lemma :  {c A B} {x : A} {g : ∞Grammar c B} 
             Trailing-whitespace′ (♭? g) 
             Trailing-whitespace″ (x <$ g)
  <$-lemma t (<$-sem x∈) w = <$-sem (proj₂ $ t x∈ w)

  ⊛-return-lemma :
     {c A B} {g : ∞Grammar c (A  B)} {x} 
    Trailing-whitespace″ (♭? g) 
    Trailing-whitespace″ (g  return x)
  ⊛-return-lemma t (⊛-sem {s₁ = s₁} f∈ return-sem) w =
    cast (++-lemma s₁ _)
         (⊛-sem (t f∈ w) return-sem)

  +-lemma :
     {c A} {g : ∞Grammar c A} 
    Trailing-whitespace″ (♭? g) 
    Trailing-whitespace″ (g +)
  +-lemma t (⊛-sem {s₁ = s₁} (<$>-sem x∈) ⋆-[]-sem) w =
    cast (++-lemma s₁ _)
         (+-sem (t x∈ w) ⋆-[]-sem)
  +-lemma t (⊛-sem {s₁ = s₁} (<$>-sem x∈) (⋆-+-sem xs∈)) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (+-∷-sem x∈ (+-lemma t xs∈ w))

  ⊛-⋆-lemma :
     {c₁ c₂ A B} {g₁ : ∞Grammar c₁ (List A  B)} {g₂ : ∞Grammar c₂ A} 
    Trailing-whitespace″ (♭? g₁) 
    Trailing-whitespace″ (♭? g₂) 
    Trailing-whitespace″ (g₁  g₂ )
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ ⋆-[]-sem) w =
    cast (++-lemma s₁ _)
         (⊛-sem (t₁ f∈ w) ⋆-[]-sem)
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ (⋆-+-sem xs∈)) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (⋆-+-sem (+-lemma t₂ xs∈ w)))

  ⊛-∣-lemma :  {c₁ c₂₁ c₂₂ A B} {g₁ : ∞Grammar c₁ (A  B)}
                {g₂₁ : ∞Grammar c₂₁ A} {g₂₂ : ∞Grammar c₂₂ A} 
              Trailing-whitespace″ (g₁  g₂₁) 
              Trailing-whitespace″ (g₁  g₂₂) 
              Trailing-whitespace″ (g₁  (g₂₁  g₂₂))
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
            (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂}
                   f∈ (left-sem x∈)) w
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₂ (⊛-sem f∈ x∈) w
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (left-sem x∈′)
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
            (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂}
                   f∈ (right-sem x∈)) w
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₃ (⊛-sem f∈ x∈) w
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (right-sem x∈′)

  ⊛-lemma :  {c₁ c₂ A B}
              {g₁ : ∞Grammar c₁ (A  B)} {g₂ : ∞Grammar c₂ A} 
            Trailing-whitespace″ (♭? g₂) 
            Trailing-whitespace″ (g₁  g₂)
  ⊛-lemma t₂ (⊛-sem {s₁ = s₁} f∈ x∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (t₂ x∈ w))

  <⊛-return-lemma :
     {c A B} {g : ∞Grammar c A} {x : B} 
    Trailing-whitespace″ (♭? g) 
    Trailing-whitespace″ (g <⊛ return x)
  <⊛-return-lemma t (<⊛-sem {s₁ = s₁} f∈ return-sem) w =
    cast (++-lemma s₁ _)
         (<⊛-sem (t f∈ w) return-sem)

  <⊛-lemma :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} 
             Trailing-whitespace′ (♭? g₂) 
             Trailing-whitespace″ (g₁ <⊛ g₂)
  <⊛-lemma t₂ (<⊛-sem {s₁ = s₁} x∈ y∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (<⊛-sem x∈ (proj₂ $ t₂ y∈ w))

  ⊛>-lemma :  {c₁ c₂ A B} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} 
             Trailing-whitespace″ (♭? g₂) 
             Trailing-whitespace″ (g₁ ⊛> g₂)
  ⊛>-lemma t₂ (⊛>-sem {s₁ = s₁} x∈ y∈) w =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛>-sem x∈ (t₂ y∈ w))

  ∣-lemma :  {c₁ c₂ A} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} 
            Trailing-whitespace″ (♭? g₁) 
            Trailing-whitespace″ (♭? g₂) 
            Trailing-whitespace″ (g₁  g₂)
  ∣-lemma t₁ t₂ (left-sem  x∈) w = left-sem  (t₁ x∈ w)
  ∣-lemma t₁ t₂ (right-sem x∈) w = right-sem (t₂ x∈ w)

  trailing? :    {A} (g : Grammar A)  Maybe (Trailing-whitespace″ g)

  trailing? (suc n) fail = just  ())

  trailing? (suc n) (f <$> g) = <$>-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (x <$ g)  = <$-lemma  <$>M trailing-whitespace′ (suc n) (♭? g)

  trailing? (suc n) (_⊛_ {c₂ = false} g  (return x))  = ⊛-return-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (_⊛_ {c₂ = false} g₁ (g₂ ))      = ⊛-⋆-lemma      <$>M trailing? n (♭? g₁)
                                                                         ⊛M trailing? n (♭? g₂)
  trailing? (suc n) (_⊛_ {c₂ = false} g₁ (g₂₁  g₂₂)) = ⊛-∣-lemma      <$>M trailing? n (g₁  g₂₁)
                                                                         ⊛M trailing? n (g₁  g₂₂)
  trailing? (suc n) (_⊛_              g₁ g₂)          = ⊛-lemma        <$>M trailing? n (♭? g₂)

  trailing? (suc n) (_<⊛_ {c₂ = false} g  (return x)) = <⊛-return-lemma <$>M trailing? n (♭? g)
  trailing? (suc n) (_<⊛_              g₁ g₂)         = <⊛-lemma <$>M
                                                          trailing-whitespace′ (suc n) (♭? g₂)

  trailing? (suc n) (g₁ ⊛> g₂) = ⊛>-lemma <$>M trailing? n (♭? g₂)

  trailing? (suc n) (g₁  g₂) = ∣-lemma <$>M trailing? n (♭? g₁)
                                          ⊛M trailing? n (♭? g₂)

  trailing? _ _ = nothing

private

  -- Some unit tests.

  test₁ : T (is-just (trailing-whitespace′ 1 (whitespace )))
  test₁ = _

  test₂ : T (is-just (trailing-whitespace′ 2 (whitespace +)))
  test₂ = _

  test₃ : T (is-just (trailing-whitespace 1 (tt <$ whitespace )))
  test₃ = _

  test₄ : T (is-just (trailing-whitespace 2 (tt <$ whitespace +)))
  test₄ = _