```------------------------------------------------------------------------
-- A general grammar and pretty-printer for binary operators of
-- various (not necessarily linearly ordered) precedences
------------------------------------------------------------------------

-- The code below uses a variant of the operator grammars described by
-- Ulf Norell and me in "Parsing Mixfix Operators". For simplicity the
-- code only handles binary infix operators.

module Examples.Precedence where

open import Coinduction
open import Data.Bool using (Bool; T)
import Data.Bool.Properties as Bool-prop
open import Data.Char as Char using (Char; _==_)
open import Data.Fin using (Fin; zero; suc; #_)
import Data.Fin.Dec as Fin-dec
open import Data.Fin.Props using () renaming (_≟_ to _≟F_)
open import Data.List as List
open import Data.List.Any as Any; open Any.Membership-≡
open import Data.List.NonEmpty
open import Data.Nat using (ℕ)
open import Data.Product as Prod
import Data.String as String
open import Data.Unit
open import Data.Vec as Vec using (allFin)
open import Data.Vec.Properties
open import Function using (id; _∘_; _∘′_)
open import Relation.Binary
import Relation.Binary.List.Pointwise as Pointwise
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product

open import Examples.Identifier
open import Grammar.Infinite as Grammar using (Grammar-for)
open import Pretty using (Pretty-printer-for)
open import Renderer
open import Utilities

------------------------------------------------------------------------
-- Binary operators

-- Associativities.

data Associativity : Set where
-   -- Non-associative.
⇾  -- Right associative.
⇽  -- Left associative.
: Associativity

-- Operator names.

is-operator-char : Char → Bool
is-operator-char t =
List.any (_==_ t) (String.toList "+-*/.:^<>=!&|")

Operator-name : Set
Operator-name = List⁺ (∃ (T ∘ is-operator-char))

-- Operators (parametrised by their associativity).

record Operator (assoc : Associativity) : Set where
constructor ⟪_⟫
field name : Operator-name

-- Equality of operators can be decided.

_≟O_ : ∀ {assoc} → Decidable (_≡_ {A = Operator assoc})
⟪ n₁ ∷ ns₁ ⟫ ≟O ⟪ n₂ ∷ ns₂ ⟫ =
Dec.map′
(P.cong ⟪_⟫ ∘ uncurry (P.cong₂ _,_))
(< P.cong proj₁ , P.cong proj₂ > ∘′ P.cong Operator.name)
((n₁ ≟OC n₂)
×-dec
Dec.map′ Pointwise.Rel≡⇒≡ Pointwise.≡⇒Rel≡
(Pointwise.decidable _≟OC_ ns₁ ns₂))
where
_≟OC_ : Decidable (_≡_ {A = ∃ (T ∘ is-operator-char)})
(c₁ , _) ≟OC (c₂ , _) =
Dec.map′ lemma (P.cong proj₁) (c₁ Char.≟ c₂)
where
lemma : {p₁ p₂ : ∃ (T ∘ is-operator-char)} →
proj₁ p₁ ≡ proj₁ p₂ → p₁ ≡ p₂
lemma P.refl = P.cong ,_ (Bool-prop.proof-irrelevance _ _)

-- A grammar for a given operator name.

operator-name : Grammar-for Operator-name
operator-name n = list⁺ (tok-sat _) n
where open Grammar

-- A pretty-printer for operator names.

operator-name-printer : Pretty-printer-for operator-name
operator-name-printer n = list⁺ tok-sat n
where open Pretty

-- A grammar for a given operator.

operator : ∀ {assoc} → Grammar-for (Operator assoc)
operator op =
Prod.map ⟪_⟫ (P.cong ⟪_⟫) <\$> operator-name (Operator.name op)
where open Grammar

-- A pretty-printer for operators.

operator-printer : ∀ {assoc} →
Pretty-printer-for (operator {assoc = assoc})
operator-printer op = <\$> operator-name-printer (Operator.name op)
where open Pretty

------------------------------------------------------------------------
-- Precedence graphs

-- Precedence graphs are represented by the number of precedence
-- levels, plus functions mapping node identifiers (precedences) to
-- node contents and successor precedences.

record Precedence-graph : Set where
field

-- The number of precedence levels.

levels : ℕ

-- Precedence levels.

Precedence : Set
Precedence = Fin levels

field

-- The precedence level's operators.

ops : Precedence → (assoc : Associativity) → List (Operator assoc)

-- The immediate successors of the precedence level.

↑ : Precedence → List Precedence

-- All precedence levels.

all-precedences : List Precedence
all-precedences = Vec.toList (allFin levels)

-- Every precedence level is a member of all-precedences.

∈-all-precedences : ∀ {p} → p ∈ all-precedences
∈-all-precedences {p} = ∈⇒List-∈ (∈-allFin p)

-- A membership test for precedences.

_∈?_ : ∀ (p : Precedence) ps → Dec (p ∈ ps)
p ∈? ps = Any.any (_≟F_ p) ps

------------------------------------------------------------------------
-- Expressions

-- The code is parametrised by a precedence graph.

module Expr (g : Precedence-graph) where

open Precedence-graph g

-- Operators with a given precedence and associativity.

Op : Precedence → Associativity → Set
Op p assoc = ∃ λ op → op ∈ ops p assoc

mutual

-- Expressions.

data Expr : Set where
var : Identifier → Expr
app : ∀ {p} → ∃ (App p) → Expr

-- Binary operator applications where the operator has a given
-- precedence and associativity.

App : Precedence → Associativity → Set
App p assoc = Expr × Op p assoc × Expr

-- The following function can be convenient to use when constructing
-- examples.

_⟨_⟩_ :
∀ {assoc} → Expr → (op : Operator assoc) →
{member : True (Fin-dec.any? λ p →
Any.any (_≟O_ op) (ops p assoc))} →
Expr → Expr
_⟨_⟩_ e₁ op {member} e₂ =
app (_ , e₁ , (op , proj₂ (toWitness member)) , e₂)

module _ where

open Grammar

mutual

-- Expression grammar.

expr : Grammar Expr
expr = whitespace ⋆ ⊛> precs all-precedences <⊛ whitespace ⋆

-- Grammar for a given list of precedence levels.

precs : List Precedence → Grammar Expr
precs ps = string′ "(" ⊛> ♯ expr <⊛ string′ ")"
∣ var <\$> identifier
∣ precs′ ps

precs′ : List Precedence → Grammar Expr
precs′ []       = fail
precs′ (p ∷ ps) = app <\$> ♯ prec p
∣ precs′ ps

-- Grammar for a given precedence level.

prec : (p : Precedence) → Grammar (∃ (App p))
prec p = ,_ <\$> non-assoc p
∣ ,_ <\$> right⁺ p
∣ ,_ <\$> left⁺ p

-- Grammar for higher precedence levels.

higher : Precedence → Grammar Expr
higher p = precs (↑ p)

-- Non-associative operators.

non-assoc : (p : Precedence) → Grammar (App p -)
non-assoc p = (λ e₁ op e₂ → e₁ , op , e₂) <\$>
higher p ⊛ operators (ops p -) ⊛ higher p

-- Right-associative operators.

right⁺ : (p : Precedence) → Grammar (App p ⇾)
right⁺ p = (λ e₁ op e₂ → e₁ , op , e₂) <\$>
higher p ⊛ operators (ops p ⇾) ⊛ right⁺↑ p

right⁺↑ : Precedence → Grammar Expr
right⁺↑ p = (app ∘ ,_) <\$> ♯ right⁺ p
∣ higher p

-- Left-associative operators.

left⁺ : (p : Precedence) → Grammar (App p ⇽)
left⁺ p = (λ e₁ op e₂ → e₁ , op , e₂) <\$>
left⁺↑ p ⊛ operators (ops p ⇽) ⊛ higher p

left⁺↑ : Precedence → Grammar Expr
left⁺↑ p = (app ∘ ,_) <\$> ♯ left⁺ p
∣ higher p

-- An operator from a given list of operators.

operators : ∀ {assoc} (os : List (Operator assoc)) →
Grammar (∃ λ op → op ∈ os)
operators []         = fail
operators (op ∷ ops) =    whitespace ⋆
⊛> (Prod.map id here <\$> operator op)
<⊛ whitespace ⋆
∣ Prod.map id there <\$> operators ops

open Pretty

mutual

-- Pretty-printer. The produced layout could probably be improved,
-- I have not tried very hard to make it pretty.

expr-printer : Pretty-printer expr
expr-printer e = nil-⋆ ⊛> precs-printer e <⊛ nil-⋆

precs-printer : ∀ {ps} → Pretty-printer (precs ps)
precs-printer e = group (precs-printer′ e)
where
precs-printer′ : ∀ {ps} → Pretty-printer (precs ps)
precs-printer′ (var x) = left (right (<\$> identifier-printer x))
precs-printer′ {ps} (app {p = p} e)
with p ∈? ps
... | yes p∈ps = right (precs′-printer p∈ps e)
... | no  _    =
-- Incorrect precedence level: insert parentheses.
left (left (text ⊛> nest 1 d <⊛ text))
where
d = nil-⋆                                       ⊛>
right (precs′-printer ∈-all-precedences e) <⊛
nil-⋆

precs′-printer :
∀ {p ps} → p ∈ ps → (e : ∃ (App p)) → Doc (precs′ ps) (app e)
precs′-printer (here P.refl) e = left  (<\$> prec-printer e)
precs′-printer (there p∈ps)  e = right (precs′-printer p∈ps e)

prec-printer : ∀ {p} → Pretty-printer (prec p)
prec-printer (- , e) = left (left (<\$> non-assoc-printer e))
prec-printer (⇾ , e) = left (right (<\$> right⁺-printer e))
prec-printer (⇽ , e) = right (<\$> left⁺-printer e)

non-assoc-printer : ∀ {p} → Pretty-printer (non-assoc p)
non-assoc-printer (e₁ , op , e₂) =
<\$> higher-printer e₁ ⊛ operators-printer op ⊛ higher-printer e₂

right⁺-printer : ∀ {p} → Pretty-printer (right⁺ p)
right⁺-printer (e₁ , op , e₂) =
<\$> higher-printer e₁ ⊛ operators-printer op ⊛ right⁺↑-printer e₂

right⁺↑-printer : ∀ {p} → Pretty-printer (right⁺↑ p)
right⁺↑-printer {p₁} (app {p = p₂} (⇾ , e))
with p₁ ≟F p₂ | higher-printer (app (⇾ , e))
right⁺↑-printer (app (⇾ , e)) | yes P.refl | _ =
-- Matching precedence and associativity.
left (<\$> right⁺-printer e)
right⁺↑-printer (app (⇾ , e)) | no _ | d = right d
right⁺↑-printer e = right (higher-printer e)

left⁺-printer : ∀ {p} → Pretty-printer (left⁺ p)
left⁺-printer (e₁ , op , e₂) =
<\$> left⁺↑-printer e₁ ⊛ operators-printer op ⊛ higher-printer e₂

left⁺↑-printer : ∀ {p} → Pretty-printer (left⁺↑ p)
left⁺↑-printer {p₁} (app {p = p₂} (⇽ , e))
with p₁ ≟F p₂ | higher-printer (app (⇽ , e))
left⁺↑-printer (app (⇽ , e)) | yes P.refl | _ =
-- Matching precedence and associativity.
left (<\$> left⁺-printer e)
left⁺↑-printer (app (⇽ , e)) | no _ | d = right d
left⁺↑-printer e = right (higher-printer e)

higher-printer : ∀ {p} → Pretty-printer (higher p)
higher-printer e = nest 2 (precs-printer e)

operators-printer : ∀ {assoc} {os : List (Operator assoc)} →
Pretty-printer (operators os)
operators-printer {os = []}     (_  , ())
operators-printer {os = ._ ∷ _} (op , here P.refl) =
left (line⋆ tt-⊛> <\$> operator-printer op <⊛ space)
operators-printer {os =  _ ∷ _} (_  , there op∈os) =
right (<\$> operators-printer (_ , op∈os))

------------------------------------------------------------------------
-- An example

-- Some operators.

add = ⟪ str⁺ "+" ⟫

sub : Operator ⇽
sub = ⟪ str⁺ "-" ⟫

mul : Operator ⇽
mul = ⟪ str⁺ "*" ⟫

div : Operator ⇽
div = ⟪ str⁺ "/" ⟫

cons : Operator ⇾
cons = ⟪ str⁺ "<:" ⟫

snoc : Operator ⇽
snoc = ⟪ str⁺ ":>" ⟫

-- A precedence graph.

g : Precedence-graph
g = record { ops = ops; ↑ = ↑ }
where
ops : Fin 3 → (assoc : Associativity) → List (Operator assoc)
ops zero             ⇽ = snoc ∷ []
ops zero             ⇾ = cons ∷ []
ops (suc zero)       ⇽ = add ∷ sub ∷ []
ops (suc (suc zero)) ⇽ = mul ∷ div ∷ []
ops _                _ = []

↑ : Fin 3 → List (Fin 3)
↑ zero          = # 1 ∷ # 2 ∷ []
↑ (suc zero)    = # 2 ∷ []
↑ (suc (suc p)) = []

open Precedence-graph g
open Expr g

-- An expression.

example : Expr
example =
(((var (str⁺ "y") ⟨ add ⟩ var (str⁺ "k"))
⟨ cons ⟩
(((var (str⁺ "i") ⟨ add ⟩ var (str⁺ "foo"))
((var (str⁺ "a")
⟨ div ⟩
(var (str⁺ "b") ⟨ sub ⟩ var (str⁺ "c")))
⟨ mul ⟩
var (str⁺ "c")))
⟨ cons ⟩
(var (str⁺ "xs"))))
⟨ snoc ⟩
(var (str⁺ "x")))
⟨ snoc ⟩
(var (str⁺ "z") ⟨ mul ⟩ var (str⁺ "z"))

-- Some unit tests.

test₁ : render 80 (expr-printer example) ≡
"(y + k <: i + foo + a / (b - c) * c <: xs) :> x :> z * z"
test₁ = P.refl

test₂ : render 50 (expr-printer example) ≡
"(y + k <: i + foo + a / (b - c) * c <: xs)\n:> x\n:> z * z"
test₂ = P.refl

test₃ : render 40 (expr-printer example) ≡
"(y + k\n   <: i + foo + a / (b - c) * c\n   <: xs)\n:> x\n:> z * z"
test₃ = P.refl

test₄ : render 30 (expr-printer example) ≡
"(y + k\n   <: i\n     + foo\n     + a / (b - c) * c\n   <: xs)\n:> x\n:> z * z"
test₄ = P.refl

test₅ : render 20 (expr-printer example) ≡
"(y + k\n   <: i\n     + foo\n     + a\n       / (b - c)\n       * c\n   <: xs)\n:> x\n:> z * z"
test₅ = P.refl

test₆ : render 6 (expr-printer example) ≡
"(y + k\n   <: i\n     + foo\n     + a\n       / (b\n          - c)\n       * c\n   <: xs)\n:> x\n:> z\n  * z"
test₆ = P.refl

-- The rendering of "y + k" in the following test may seem strange: if
-- no newline had been inserted before +, then the total width of this
-- subexpression would have been smaller.
--
-- Wadler's pretty-printing algorithm is not always optimal for texts
-- that do not fit in the allotted width, if by "optimal" we mean
-- "with as little overflow as possible". To see what I mean, try
-- running the following Haskell code, where the functions are
-- implemented as in Wadler's paper:
--
--   pretty 1 (group (nest 20 (line <> text "x")))
--
-- The result is "\n                    x", which can be seen as much
-- worse than the alternative result " x". However, note that Wadler
-- uses a lexicographic definition of "better", in which
-- "\n                    x" is better than " x", because the first
-- line of "\n                    x" fits, but the first line of " x"
-- doesn't.

test₇ : render 5 (expr-printer example) ≡
"(y\n     + k\n   <: i\n     + foo\n     + a\n       / (b\n          - c)\n       * c\n   <: xs)\n:> x\n:> z\n  * z"
test₇ = P.refl
```