------------------------------------------------------------------------
-- Acyclic precedence graphs
------------------------------------------------------------------------

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

-- Precedence graphs are represented by their unfoldings as forests
-- (one tree for every node in the graph). This does not take into
-- account the sharing of the precedence graphs, but this code is
-- not aimed at efficiency.

-- Precedence trees.

data Precedence : Set where
  precedence : (o : (fix : Fixity) → List (∃ (Operator fix)))
               (s : List Precedence) →
               Precedence

-- Precedence forests.

PrecedenceGraph : Set
PrecedenceGraph = List Precedence

-- The operators of the given precedence.

ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
ops (precedence o s) = o

-- The immediate successors of the precedence level.

↑ : Precedence → List Precedence
↑ (precedence o s) = s

-- Acyclic precedence graphs.

acyclic : PrecedenceGraphInterface
acyclic = record
  { PrecedenceGraph = PrecedenceGraph
  ; Precedence      = λ _ → Precedence
  ; ops             = λ _ → ops
  ; ↑               = λ _ → ↑
  ; anyPrecedence   = λ g → g
  }