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
data Associativity : Set where
-
⇾
⇽
: Associativity
is-operator-char : Char → Bool
is-operator-char t =
List.any (_==_ t) (String.toList "+-*/.:^<>=!&|")
Operator-name : Set
Operator-name = List⁺ (∃ (T ∘ is-operator-char))
record Operator (assoc : Associativity) : Set where
constructor ⟪_⟫
field name : Operator-name
_≟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 _ _)
operator-name : Grammar-for Operator-name
operator-name n = list⁺ (tok-sat _) n
where open Grammar
operator-name-printer : Pretty-printer-for operator-name
operator-name-printer n = list⁺ tok-sat n
where open Pretty
operator : ∀ {assoc} → Grammar-for (Operator assoc)
operator op =
Prod.map ⟪_⟫ (P.cong ⟪_⟫) <$> operator-name (Operator.name op)
where open Grammar
operator-printer : ∀ {assoc} →
Pretty-printer-for (operator {assoc = assoc})
operator-printer op = <$> operator-name-printer (Operator.name op)
where open Pretty
record Precedence-graph : Set where
field
levels : ℕ
Precedence : Set
Precedence = Fin levels
field
ops : Precedence → (assoc : Associativity) → List (Operator assoc)
↑ : Precedence → List Precedence
all-precedences : List Precedence
all-precedences = Vec.toList (allFin levels)
∈-all-precedences : ∀ {p} → p ∈ all-precedences
∈-all-precedences {p} = ∈⇒List-∈ (∈-allFin p)
_∈?_ : ∀ (p : Precedence) ps → Dec (p ∈ ps)
p ∈? ps = Any.any (_≟F_ p) ps
module Expr (g : Precedence-graph) where
open Precedence-graph g
Op : Precedence → Associativity → Set
Op p assoc = ∃ λ op → op ∈ ops p assoc
mutual
data Expr : Set where
var : Identifier → Expr
app : ∀ {p} → ∃ (App p) → Expr
App : Precedence → Associativity → Set
App p assoc = Expr × Op p assoc × Expr
_⟨_⟩_ :
∀ {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
expr : Grammar Expr
expr = whitespace ⋆ ⊛> precs all-precedences <⊛ whitespace ⋆
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
prec : (p : Precedence) → Grammar (∃ (App p))
prec p = ,_ <$> non-assoc p
∣ ,_ <$> right⁺ p
∣ ,_ <$> left⁺ p
higher : Precedence → Grammar Expr
higher p = precs (↑ p)
non-assoc : (p : Precedence) → Grammar (App p -)
non-assoc p = (λ e₁ op e₂ → e₁ , op , e₂) <$>
higher p ⊛ operators (ops p -) ⊛ higher p
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⁺ : (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
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
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 _ =
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 | _ =
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 | _ =
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))
add : Operator ⇽
add = ⟪ str⁺ "+" ⟫
sub : Operator ⇽
sub = ⟪ str⁺ "-" ⟫
mul : Operator ⇽
mul = ⟪ str⁺ "*" ⟫
div : Operator ⇽
div = ⟪ str⁺ "/" ⟫
cons : Operator ⇾
cons = ⟪ str⁺ "<:" ⟫
snoc : Operator ⇽
snoc = ⟪ str⁺ ":>" ⟫
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
example : Expr
example =
(((var (str⁺ "y") ⟨ add ⟩ var (str⁺ "k"))
⟨ cons ⟩
(((var (str⁺ "i") ⟨ add ⟩ var (str⁺ "foo"))
⟨ add ⟩
((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"))
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
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