module Mixfix.Cyclic.PrecedenceGraph where
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Data.Vec as Vec using (allFin)
open import Data.List using (List)
open import Data.Product using (∃)
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Expr hiding (module PrecedenceGraph)
record PrecedenceGraph : Set where
field
levels : ℕ
Precedence : Set
Precedence = Fin levels
field
ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
↑ : Precedence → List Precedence
anyPrecedence : List Precedence
anyPrecedence = Vec.toList (allFin levels)
cyclic : PrecedenceGraphInterface
cyclic = record
{ PrecedenceGraph = PrecedenceGraph
; Precedence = PrecedenceGraph.Precedence
; ops = PrecedenceGraph.ops
; ↑ = PrecedenceGraph.↑
; anyPrecedence = PrecedenceGraph.anyPrecedence
}