open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
using (acyclic; precedence)
module Mixfix.Acyclic.Grammar
(g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
where
open import Coinduction
open import Data.List using (List; []; _∷_)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_)
open import Data.List.NonEmpty using (foldr; foldl)
open import Data.Product
open import Data.Bool
import Data.String as String
open import Relation.Binary.PropositionalEquality
open PrecedenceCorrect acyclic g
import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (Parser; ⟦_⟧)
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Acyclic.Lib renaming (ParserProg to Parser)
mutual
expr : ∞ (Parser (Expr g))
expr = ♯ precs g
precs : (ps : List Precedence) → Parser (Expr ps)
precs [] = fail
precs (p ∷ ps) = (λ e → here refl ∙ proj₂ e) <$> prec p
∣ weakenE <$> precs ps
prec : (p : Precedence) → Parser (∃ (ExprIn p))
prec (precedence ops sucs) =
⟪_⟫ <$> [ closed ]
∥ _⟨_⟩_ <$> p↑ ⊛ [ infx non ] ⊛ p↑
∥ appʳ <$> preRight + ⊛ p↑
∥ appˡ <$> p↑ ⊛ postLeft +
∥ fail
module Prec where
p = precedence ops sucs
[_] = λ (fix : Fixity) → inner (ops fix)
p↑ = precs sucs
preRight : Parser (Outer p right → ExprIn p right)
preRight = ⟪_⟩_ <$> [ prefx ]
∣ _⟨_⟩ʳ_ <$> p↑ ⊛ [ infx right ]
postLeft : Parser (Outer p left → ExprIn p left)
postLeft = (λ op e₁ → e₁ ⟨ op ⟫ ) <$> [ postfx ]
∣ (λ op e₂ e₁ → e₁ ⟨ op ⟩ˡ e₂) <$> [ infx left ] ⊛ p↑
appʳ = λ fs e → foldr (λ f e → f (similar e)) (λ f → f (tighter e)) fs
appˡ = λ e fs → foldl (λ e f → f (similar e)) (λ f → f (tighter e)) fs
inner : ∀ {fix} (ops : List (∃ (Operator fix))) →
Parser (Inner ops)
inner [] = fail
inner ((_ , op) ∷ ops) =
(λ args → here refl ∙ args) <$> (expr between nameParts op)
∣ weakenI <$> inner ops
expression : Simplified.Parser NamePart false (Expr g)
expression = ⟦ ♭ expr ⟧