module Mixfix.Expr where
open import Data.Vec using (Vec)
open import Data.List using (List; []; _∷_)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_)
open import Data.Product using (∃; _,_)
open import Mixfix.Fixity
open import Mixfix.Operator
record PrecedenceGraphInterface : Set₁ where
field
PrecedenceGraph : Set
Precedence : PrecedenceGraph → Set
ops : (g : PrecedenceGraph) →
Precedence g → (fix : Fixity) → List (∃ (Operator fix))
↑ : (g : PrecedenceGraph) → Precedence g → List (Precedence g)
anyPrecedence : (g : PrecedenceGraph) → List (Precedence g)
module PrecedenceGraph
(i : PrecedenceGraphInterface)
(g : PrecedenceGraphInterface.PrecedenceGraph i)
where
PrecedenceGraph : Set
PrecedenceGraph = PrecedenceGraphInterface.PrecedenceGraph i
Precedence : Set
Precedence = PrecedenceGraphInterface.Precedence i g
ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
ops = PrecedenceGraphInterface.ops i g
↑ : Precedence → List Precedence
↑ = PrecedenceGraphInterface.↑ i g
anyPrecedence : List Precedence
anyPrecedence = PrecedenceGraphInterface.anyPrecedence i g
module PrecedenceCorrect
(i : PrecedenceGraphInterface)
(g : PrecedenceGraphInterface.PrecedenceGraph i)
where
open PrecedenceGraph i g public
mutual
infixl 4 _⟨_⟩ˡ_
infixr 4 _⟨_⟩ʳ_
infix 4 _⟨_⟩_ _⟨_⟫ ⟪_⟩_ _∙_
data Expr (ps : List Precedence) : Set where
_∙_ : ∀ {p assoc} (p∈ps : p ∈ ps) (e : ExprIn p assoc) → Expr ps
data ExprIn (p : Precedence) : Associativity → Set where
⟪_⟫ : (op : Inner (ops p closed )) → ExprIn p non
_⟨_⟫ : (l : Outer p left) (op : Inner (ops p postfx )) → ExprIn p left
⟪_⟩_ : (op : Inner (ops p prefx )) (r : Outer p right) → ExprIn p right
_⟨_⟩_ : (l : Expr (↑ p) ) (op : Inner (ops p (infx non ))) (r : Expr (↑ p) ) → ExprIn p non
_⟨_⟩ˡ_ : (l : Outer p left) (op : Inner (ops p (infx left ))) (r : Expr (↑ p) ) → ExprIn p left
_⟨_⟩ʳ_ : (l : Expr (↑ p) ) (op : Inner (ops p (infx right))) (r : Outer p right) → ExprIn p right
data Outer (p : Precedence) (assoc : Associativity) : Set where
similar : (e : ExprIn p assoc) → Outer p assoc
tighter : (e : Expr (↑ p)) → Outer p assoc
data Inner {fix} (ops : List (∃ (Operator fix))) : Set where
_∙_ : ∀ {arity op}
(op∈ops : (arity , op) ∈ ops)
(args : Vec (Expr anyPrecedence) arity) →
Inner ops
weakenE : ∀ {p ps} → Expr ps → Expr (p ∷ ps)
weakenE (p∈ps ∙ e) = there p∈ps ∙ e
weakenI : ∀ {fix ops} {op : ∃ (Operator fix)} →
Inner ops → Inner (op ∷ ops)
weakenI (op∈ops ∙ args) = there op∈ops ∙ args