module Productivity (char : Set) where

  infix  50 _⋆ _+
  infixl 40 _⊛_
  infixl 30 _∣_

  codata P : Set where
    ε   : P
    sym : char -> P
    _⊛_ : P -> P -> P
    _∣_ : P -> P -> P

  mutual

    _⋆ : P -> P
    p ⋆ ~ ε ∣ p +

    _+ : P -> P
    p + ~ p ⊛ p ⋆

  _sepBy_ : P -> P -> P
  p sepBy sep = p ⊛ (sep ⊛ p) ⋆

  postulate
    addOp  : P
    mulOp  : P
    number : P
    openP  : char
    closeP : char

  -- Not guarded:

  mutual
    expr   ~ term sepBy addOp
    term   ~ factor sepBy mulOp
    factor ~ number ∣ sym openP ⊛ expr ⊛ sym closeP

  -- Guarded and incomprehensible:

  mutual
    expr₁ ~ term₁ ⊛ expr₂
    expr₂ ~ ε ∣ expr₃
    expr₃ ~ (addOp ⊛ term₁) ⊛ expr₂

    term₁ ~ factor₁ ⊛ term₂
    term₂ ~ ε ∣ term₃
    term₃ ~ (mulOp ⊛ factor₁) ⊛ term₂

    factor₁ ~ number ∣ sym openP ⊛ expr₁ ⊛ sym closeP