------------------------------------------------------------------------
-- Linearisation of mixfix operators
------------------------------------------------------------------------

open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
  using (acyclic; precedence)

module Mixfix.Acyclic.Show
         (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
         where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_)
open import Data.Vec using (Vec; []; _∷_)
import Data.DifferenceList as DiffList
open DiffList using (DiffList; _++_)
              renaming (_∷_ to cons; [_] to singleton)
open import Data.Product using (∃; _,_; ,_)
open import Function using (_∘_; flip)
open import Data.Maybe using (Maybe; nothing; just)
import Data.String as String
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open PrecedenceCorrect acyclic g
open import StructurallyRecursiveDescentParsing.Simplified
open import StructurallyRecursiveDescentParsing.Simplified.Semantics
  as Semantics
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Acyclic.Lib as Lib
open Lib.Semantics-⊕
import Mixfix.Acyclic.Grammar
import Mixfix.Acyclic.Lemma
private
  module Grammar = Mixfix.Acyclic.Grammar g
  module Lemma   = Mixfix.Acyclic.Lemma   g

------------------------------------------------------------------------
-- Linearisation

-- Note: The code assumes that the grammar is unambiguous.

module Show where

  mutual

    expr : ∀ {ps} → Expr ps → DiffList NamePart
    expr (_ ∙ e) = exprIn e

    exprIn : ∀ {p assoc} → ExprIn p assoc → DiffList NamePart
    exprIn    ⟪ op ⟫     =            inner op
    exprIn (l ⟨ op ⟫   ) = outer l ++ inner op
    exprIn (  ⟪ op ⟩  r) =            inner op ++ outer r
    exprIn (l ⟨ op ⟩  r) = expr  l ++ inner op ++ expr  r
    exprIn (l ⟨ op ⟩ˡ r) = outer l ++ inner op ++ expr  r
    exprIn (l ⟨ op ⟩ʳ r) = expr  l ++ inner op ++ outer r

    outer : ∀ {p assoc} → Outer p assoc → DiffList NamePart
    outer (similar e) = exprIn e
    outer (tighter e) = expr   e

    inner : ∀ {fix} {ops : List (∃ (Operator fix))} →
            Inner ops → DiffList NamePart
    inner (_∙_ {op = op} _ args) = inner′ (nameParts op) args

    inner′ : ∀ {arity} → Vec NamePart (1 + arity) → Vec (Expr g) arity →
             DiffList NamePart
    inner′ (n ∷ []) []           = singleton n
    inner′ (n ∷ ns) (arg ∷ args) = cons n (expr arg ++ inner′ ns args)

show : ∀ {ps} → Expr ps → List NamePart
show = DiffList.toList ∘ Show.expr

------------------------------------------------------------------------
-- Correctness

module Correctness where

  mutual

    expr : ∀ {ps s} (e : Expr ps) →
           e ⊕ s ∈⟦ Grammar.precs ps ⟧· Show.expr e s
    expr (here refl  ∙ e) = ∣ˡ (<$> exprIn e)
    expr (there x∈xs ∙ e) = ∣ʳ (<$> expr (x∈xs ∙ e))

    exprIn : ∀ {p assoc s} (e : ExprIn p assoc) →
             (, e) ⊕ s ∈⟦ Grammar.prec p ⟧· Show.exprIn e s
    exprIn {precedence ops sucs} e = exprIn′ _ e
      where
      p        = precedence ops sucs
      module N = Grammar.Prec ops sucs

      lemmaʳ : ∀ {f : Outer p right → ExprIn p right} {s e} {g : DiffList NamePart} →
               (∀ {s} → f ⊕ s ∈⟦ N.preRight ⟧· g s) →
                          e  ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧·    Show.exprIn e s →
               f (similar e) ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧· g (Show.exprIn e s)
      lemmaʳ f∈ (<$> fs∈ ⊛ e∈) = <$> +-∷ f∈ fs∈ ⊛ e∈

      preRight : ∀ {s} (e : ExprIn p right) →
                 e ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧· Show.exprIn e s
      preRight (  ⟪ op ⟩  tighter e) = <$> +-[] (∣ˡ (<$> inner op)) ⊛ expr e
      preRight (  ⟪ op ⟩  similar e) = lemmaʳ   (∣ˡ (<$> inner op)) (preRight e)
      preRight (l ⟨ op ⟩ʳ tighter e) = <$> +-[] (∣ʳ (<$> expr l ⊛ inner op)) ⊛ expr e
      preRight (l ⟨ op ⟩ʳ similar e) = lemmaʳ   (∣ʳ (<$> expr l ⊛ inner op)) (preRight e)

      lemmaˡ : ∀ {f : Outer p left → ExprIn p left} {s e} {g : DiffList NamePart} →
               (∀ {s} → f ⊕ s ∈⟦ N.postLeft ⟧· g s) →
                          e  ⊕ g s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e (g s) →
               f (similar e) ⊕   s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e (g s)
      lemmaˡ {f} f∈ (_⊛_ {x = fs} (<$>_ {x = e} e∈) fs∈) =
        Lib.Semantics-⊕.cast∈ (Lemma.appˡ-∷ʳ (tighter e) fs f) (<$> e∈ ⊛ +-∷ʳ fs∈ f∈)

      postLeft : ∀ {s} (e : ExprIn p left) →
                 e ⊕ s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e s
      postLeft (tighter e ⟨ op ⟫   ) = <$> expr e ⊛ +-[] (∣ˡ (<$> inner op))
      postLeft (similar e ⟨ op ⟫   ) = lemmaˡ            (∣ˡ (<$> inner op)) (postLeft e)
      postLeft (tighter e ⟨ op ⟩ˡ r) = <$> expr e ⊛
                                         +-[] (∣ʳ (<$> inner op ⊛ expr r))
      postLeft (similar e ⟨ op ⟩ˡ r) = lemmaˡ (∣ʳ (<$> inner op ⊛ expr r)) (postLeft e)

      exprIn′ : ∀ assoc {s} (e : ExprIn p assoc) →
                (, e) ⊕ s ∈⟦ Grammar.prec p ⟧· Show.exprIn e s
      exprIn′ non      ⟪ op ⟫    = ∥ˡ (<$> inner op)
      exprIn′ non   (l ⟨ op ⟩ r) = ∥ʳ (∥ˡ (<$> expr l ⊛ inner op ⊛ expr r))
      exprIn′ right e            = ∥ʳ (∥ʳ (∥ˡ (preRight e)))
      exprIn′ left  e            = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft e))))

    inner : ∀ {fix s ops} (i : Inner {fix} ops) →
            i ⊕ s ∈⟦ Grammar.inner ops ⟧· Show.inner i s
    inner {fix} {s} (_∙_ {arity} {op} op∈ops args) =
      helper op∈ops args
      where
      helper : {ops : List (∃ (Operator fix))}
               (op∈ : (arity , op) ∈ ops) (args : Vec (Expr g) arity) →
               let i = op∈ ∙ args in
               i ⊕ s ∈⟦ Grammar.inner ops ⟧· Show.inner i s
      helper (here refl) args = ∣ˡ (<$> inner′ (nameParts op) args)
      helper (there {x = _ , _} op∈) args =
        ∣ʳ (<$> helper op∈ args)

    inner′ : ∀ {arity s} (ns : Vec NamePart (1 + arity)) args →
             args ⊕ s ∈⟦ Grammar.expr between ns ⟧· Show.inner′ ns args s
    inner′ (n ∷ [])      []           = between-[]
    inner′ (n ∷ n′ ∷ ns) (arg ∷ args) =
      between-∷ (expr arg) (inner′ (n′ ∷ ns) args)

-- All generated strings are syntactically correct (but possibly
-- ambiguous). Note that this result implies that all
-- precedence-correct expressions are generated by the grammar.

correct : (e : Expr g) → e ∈ Grammar.expression · show e
correct e =
  Semantics.⊕-sound (Lib.Semantics-⊕.sound (Correctness.expr e))