open import Mixfix.Expr
module Mixfix.Cyclic.Grammar
(i : PrecedenceGraphInterface)
(g : PrecedenceGraphInterface.PrecedenceGraph i)
where
open import Coinduction
open import Function using (flip; _$_)
open import Data.List using (List; []; _∷_)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
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 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 refl ∙ args) <$> (expr between nameParts op)
∣ weakenI <$> inner ops
expression : Parser.Parser NamePart (Expr anyPrecedence) []
expression = ⟦ ♭ expr ⟧