open import Mixfix.Expr
module Mixfix.Cyclic.Grammar
(i : PrecedenceGraphInterface)
(g : PrecedenceGraphInterface.PrecedenceGraph i)
where
open import Codata.Musical.Notation
open import Function using (flip; _$_)
open import Data.List using (List; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
import Relation.Binary.PropositionalEquality as P
open PrecedenceCorrect i g
import TotalParserCombinators.Parser as Parser
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Cyclic.Lib renaming (ParserProg to Parser)
mutual
expr : ∞ (Parser (Expr anyPrecedence))
expr = ♯ precs anyPrecedence
precs : (ps : List Precedence) → Parser (Expr ps)
precs [] = fail
precs (p ∷ ps) = (λ e → here P.refl ∙ proj₂ e) <$> prec p
∣ weakenE <$> precs ps
prec : (p : Precedence) → Parser (∃ (ExprIn p))
prec p = closedOps ∥ nonAssoc ∥ preRight⁺ ∥ postLeft⁺ ∥ fail
module Prec where
[_] = λ (fix : Fixity) → inner (ops p fix)
p↑ = precs (↑ p)
closedOps : Parser (ExprIn p non)
closedOps = ⟪_⟫ <$> [ closed ]
nonAssoc : Parser (ExprIn p non)
nonAssoc = ♯ (_⟨_⟩_ <$> p↑ ⊛ [ infx non ]) ⊛∞ ♯ p↑
preRight : Parser (Outer p right → ExprIn p right)
preRight = ⟪_⟩_ <$> [ prefx ]
∣ _⟨_⟩ʳ_ <$> p↑ ⊛ [ infx right ]
preRight⁺ : Parser (ExprIn p right)
preRight⁺ = ♯ preRight
⊛∞
♯ (similar <$> preRight⁺ ∣ tighter <$> p↑)
postLeft : Parser (Outer p left → ExprIn p left)
postLeft = (λ op e₁ → e₁ ⟨ op ⟫ ) <$> [ postfx ]
∣ (λ op e₂ e₁ → e₁ ⟨ op ⟩ˡ e₂) <$> [ infx left ] ⊛ p↑
postLeft⁺ : Parser (ExprIn p left)
postLeft⁺ = ♯ (flip _$_ <$> ( similar <$> postLeft⁺
∣ tighter <$> p↑
))
⊛∞
♯ postLeft
inner : ∀ {fix} (ops : List (∃ (Operator fix))) →
Parser (Inner ops)
inner [] = fail
inner ((_ , op) ∷ ops) =
(λ args → here P.refl ∙ args) <$> (expr between nameParts op)
∣ weakenI <$> inner ops
expression : Parser.Parser NamePart (Expr anyPrecedence) []
expression = ⟦ ♭ expr ⟧