```------------------------------------------------------------------------
-- Simple expressions
------------------------------------------------------------------------

-- Several examples based on Matsuda and Wang's "FliPpr: A Prettier
-- Invertible Printing System".

module Examples.Expression where

open import Algebra
open import Coinduction
open import Data.List as List
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

private
module LM {A : Set} = Monoid (List.monoid A)

open import Examples.Identifier
import Grammar.Infinite as Grammar
import Pretty
open import Renderer
open import Utilities

-- Very simple expressions.

module Expression₁ where

data Expr : Set where
one : Expr
sub : Expr → Expr → Expr

module _ where

open Grammar

mutual

expr : Grammar Expr
expr = term
∣ sub <\$> ♯ expr
<⊛ whitespace ⋆
<⊛ string′ "-"
<⊛ whitespace ⋆
⊛  term

term : Grammar Expr
term = one <\$ string′ "1"
∣    string′ "("
⊛> whitespace ⋆
⊛> ♯ expr
<⊛ whitespace ⋆
<⊛ string′ ")"

open Pretty

one-doc : Doc term one
one-doc = left (<\$ text)

mutual

expr-printer : Pretty-printer expr
expr-printer one         = left one-doc
expr-printer (sub e₁ e₂) =
group (right (<\$> expr-printer e₁ <⊛-tt
nest 2 line⋆ <⊛ text <⊛ space ⊛
nest 2 (term-printer e₂)))

term-printer : Pretty-printer term
term-printer one = one-doc
term-printer e   =
right (text ⊛> nil-⋆ ⊛> expr-printer e <⊛ nil-⋆ <⊛ text)

example : Expr
example = sub (sub one one) (sub one one)

test₁ : render 80 (expr-printer example) ≡ "1 - 1 - (1 - 1)"
test₁ = refl

test₂ : render 11 (expr-printer example) ≡ "1 - 1\n  - (1 - 1)"
test₂ = refl

test₃ : render 8 (expr-printer example) ≡ "1 - 1\n  - (1\n    - 1)"
test₃ = refl

-- Expression₁.expr does not accept final whitespace. The grammar
-- below does.

module Expression₂ where

open Expression₁ using (Expr; one; sub; example)

module _ where

open Grammar

mutual

expr : Grammar Expr
expr = term
∣ sub <\$> ♯ expr <⊛ symbol′ "-" ⊛ term

term : Grammar Expr
term = one <\$ symbol′ "1"
∣ symbol′ "(" ⊛> ♯ expr <⊛ symbol′ ")"

private

-- A manual proof of Trailing-whitespace expr (included for
-- illustrative purposes; not used below).

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

tw′-whitespace : Trailing-whitespace′ (whitespace ⋆)
tw′-whitespace ⋆-[]-sem                                  w = _ , w
tw′-whitespace (⋆-+-sem (⊛-sem {s₁ = s₁} (<\$>-sem p) q)) w
with tw′-whitespace q w
... | _ , r = _ , cast (P.sym \$ LM.assoc s₁ _ _)
(⋆-+-sem (⊛-sem (<\$>-sem p) r))

tw″-symbol : ∀ {s} → Trailing-whitespace″ (symbol s)
tw″-symbol (<⊛-sem {s₁ = s₁} p q) w =
cast (P.sym \$ LM.assoc s₁ _ _)
(<⊛-sem p (proj₂ (tw′-whitespace q w)))

tw″-term : Trailing-whitespace″ term
tw″-term (left-sem (<\$-sem p)) w =
left-sem (<\$-sem (tw″-symbol p w))
tw″-term (right-sem (<⊛-sem {s₁ = s₁} p q)) w =
cast (P.sym \$ LM.assoc s₁ _ _)
(right-sem (<⊛-sem p (tw″-symbol q w)))

tw″-expr : Trailing-whitespace″ expr
tw″-expr (left-sem p) w =
left-sem (tw″-term p w)
tw″-expr (right-sem (⊛-sem {s₁ = s₁} p q)) w =
cast (P.sym \$ LM.assoc s₁ _ _)
(right-sem (⊛-sem p (tw″-term q w)))

tw-expr : Trailing-whitespace expr
tw-expr (<⊛-sem p w) = tw″-expr p w

open Pretty

one-doc : Doc term one
one-doc = left (<\$ symbol)

mutual

expr-printer : Pretty-printer expr
expr-printer one         = left one-doc
expr-printer (sub e₁ e₂) =
group (right (<\$> final-line 6 (expr-printer e₁) 2 <⊛
symbol-space ⊛ nest 2 (term-printer e₂)))

term-printer : Pretty-printer term
term-printer one = one-doc
term-printer e   = right (symbol ⊛> expr-printer e <⊛ symbol)

test₁ : render 80 (expr-printer example) ≡ "1 - 1 - (1 - 1)"
test₁ = refl

test₂ : render 11 (expr-printer example) ≡ "1 - 1\n  - (1 - 1)"
test₂ = refl

test₃ : render 8 (expr-printer example) ≡ "1 - 1\n  - (1\n    - 1)"
test₃ = refl

-- A somewhat larger expression example.

module Expression₃ where

-- Expressions.

data Expr : Set where
one : Expr
sub : Expr → Expr → Expr
div : Expr → Expr → Expr
var : Identifier → Expr

-- Precedences.

data Prec : Set where
′5 ′6 ′7 : Prec

module _ where

open Grammar

-- One expression grammar for each precedence level.

expr : Prec → Grammar Expr
expr ′5 = ♯ expr ′6
∣ sub <\$> ♯ expr ′5 <⊛ symbol′ "-" ⊛ ♯ expr ′6
expr ′6 = ♯ expr ′7
∣ div <\$> ♯ expr ′6 <⊛ symbol′ "/" ⊛ ♯ expr ′7
expr ′7 = one <\$ symbol′ "1"
∣ var <\$> identifier-w
∣ symbol′ "(" ⊛> ♯ expr ′5 <⊛ symbol′ ")"

open Pretty

-- Document for one.

one-doc : Doc (expr ′7) one
one-doc = left (left (<\$ symbol))

-- Documents for variables.

var-doc : ∀ x → Doc (expr ′7) (var x)
var-doc x = left (right (<\$> identifier-w-printer x))

-- Adds parentheses to a document.

parens : ∀ {e} → Doc (expr ′5) e → Doc (expr ′7) e
parens d = right (symbol ⊛> d <⊛ symbol)

-- Adds parentheses only when necessary (when p₁ < p₂).

parens-if[_<_] : ∀ p₁ p₂ {e} → Doc (expr p₁) e → Doc (expr p₂) e
parens-if[ ′5 < ′5 ] = id
parens-if[ ′5 < ′6 ] = left ∘ parens
parens-if[ ′5 < ′7 ] = parens
parens-if[ ′6 < ′5 ] = left
parens-if[ ′6 < ′6 ] = id
parens-if[ ′6 < ′7 ] = parens ∘ left
parens-if[ ′7 < ′5 ] = left ∘ left
parens-if[ ′7 < ′6 ] = left
parens-if[ ′7 < ′7 ] = id

mutual

-- Pretty-printers.

expr-printer : ∀ p → Pretty-printer (expr p)
expr-printer p (sub e₁ e₂) = parens-if[ ′5 < p ] (sub-printer e₁ e₂)
expr-printer p (div e₁ e₂) = parens-if[ ′6 < p ] (div-printer e₁ e₂)
expr-printer p one         = parens-if[ ′7 < p ] one-doc
expr-printer p (var x)     = parens-if[ ′7 < p ] (var-doc x)

sub-printer : ∀ e₁ e₂ → Doc (expr ′5) (sub e₁ e₂)
sub-printer e₁ e₂ =
group (right (<\$> final-line 10 (expr-printer ′5 e₁) 2 <⊛
symbol-space ⊛ nest 2 (expr-printer ′6 e₂)))

div-printer : ∀ e₁ e₂ → Doc (expr ′6) (div e₁ e₂)
div-printer e₁ e₂ =
group (right (<\$> final-line 10 (expr-printer ′6 e₁) 2 <⊛
symbol-space ⊛ nest 2 (expr-printer ′7 e₂)))

-- Unit tests.

example : Expr
example = sub (div (var (str⁺ "x")) one) (sub one (var (str⁺ "y")))

test₁ : render 80 (expr-printer ′5 example) ≡ "x / 1 - (1 - y)"
test₁ = refl

test₂ : render 11 (expr-printer ′5 example) ≡ "x / 1\n  - (1 - y)"
test₂ = refl

test₃ : render 8 (expr-printer ′5 example) ≡ "x / 1\n  - (1\n    - y)"
test₃ = refl

test₄ : render 11 (expr-printer ′6 example) ≡ "(x / 1\n  - (1\n    - y))"
test₄ = refl

test₅ : render 12 (expr-printer ′6 example) ≡ "(x / 1\n  - (1 - y))"
test₅ = refl
```