module Mixfix.Acyclic.PrecedenceGraph where
open import Data.List
open import Data.Product
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Expr
data Precedence : Set where
precedence : (o : (fix : Fixity) → List (∃ (Operator fix)))
(s : List Precedence) →
Precedence
PrecedenceGraph : Set
PrecedenceGraph = List Precedence
ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
ops (precedence o s) = o
↑ : Precedence → List Precedence
↑ (precedence o s) = s
acyclic : PrecedenceGraphInterface
acyclic = record
{ PrecedenceGraph = PrecedenceGraph
; Precedence = λ _ → Precedence
; ops = λ _ → ops
; ↑ = λ _ → ↑
; anyPrecedence = λ g → g
}