------------------------------------------------------------------------
-- Precedence-correct expressions
------------------------------------------------------------------------

module Mixfix.Expr where

open import Data.Vec  using (Vec)
open import Data.List using (List; []; _∷_)
open import Data.List.Any using (here; there)
open import Data.List.Any.Membership.Propositional using (_∈_)
open import Data.Product using (; _,_)

open import Mixfix.Fixity
open import Mixfix.Operator

------------------------------------------------------------------------
-- An abstract definition of precedence graphs

-- The interface of precedence graphs.

record PrecedenceGraphInterface : Set₁ where
  field
    -- Precedence graphs.
    PrecedenceGraph : Set

    -- Precedence levels.
    Precedence : PrecedenceGraph  Set

    -- The operators of the given precedence.
    ops : (g : PrecedenceGraph) 
          Precedence g  (fix : Fixity)  List ( (Operator fix))

    -- The immediate successors of the precedence level.
     : (g : PrecedenceGraph)  Precedence g  List (Precedence g)

    -- All precedence levels in the graph.
    anyPrecedence : (g : PrecedenceGraph)  List (Precedence g)

-- When a precedence graph is given the following module may be
-- convenient to avoid having to write "g" all the time.

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

------------------------------------------------------------------------
-- Precedence-correct operator applications

-- Parameterised on a precedence graph.

module PrecedenceCorrect
         (i : PrecedenceGraphInterface)
         (g : PrecedenceGraphInterface.PrecedenceGraph i)
         where

  open PrecedenceGraph i g public

  mutual

    infixl 4 _⟨_⟩ˡ_
    infixr 4 _⟨_⟩ʳ_
    infix  4 _⟨_⟩_ _⟨_⟫ ⟪_⟩_ _∙_

    -- Expr ps contains expressions where the outermost operator has
    -- one of the precedences in ps.

    data Expr (ps : List Precedence) : Set where
      _∙_ :  {p assoc} (p∈ps : p  ps) (e : ExprIn p assoc)  Expr ps

    -- ExprIn p assoc contains expressions where the outermost
    -- operator has precedence p (is /in/ precedence level p) and the
    -- associativity assoc.

    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

    -- Outer p fix contains expressions where the head operator either
    --   ⑴ has precedence p and associativity assoc or
    --   ⑵ binds strictly tighter than p.

    data Outer (p : Precedence) (assoc : Associativity) : Set where
      similar : (e : ExprIn p assoc)  Outer p assoc
      tighter : (e : Expr ( p))      Outer p assoc

    -- Inner ops contains the internal parts (operator plus
    -- internal arguments) of operator applications. The operators
    -- have to be members of ops.

    data Inner {fix} (ops : List ( (Operator fix))) : Set where
      _∙_ :  {arity op}
            (op∈ops : (arity , op)  ops)
            (args : Vec (Expr anyPrecedence) arity) 
            Inner ops

  -- "Weakening".

  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