------------------------------------------------------------------------
-- The two methods used to specify the grammars are (language)
-- equivalent (for acyclic graphs)
------------------------------------------------------------------------

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

module Mixfix.Equivalence
  (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
  where

open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.List.NonEmpty using (_∷_)
open import Data.Nat using (; zero; suc; _+_)
open import Data.Product
open import Data.Vec using (Vec; []; _∷_)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
open import TotalParserCombinators.Semantics.Continuation as ContSem
import StructurallyRecursiveDescentParsing.Simplified as Simplified
import StructurallyRecursiveDescentParsing.Simplified.Semantics as SSem

open import Mixfix.Fixity
open import Mixfix.Operator
import Mixfix.Acyclic.Grammar
import Mixfix.Cyclic.Grammar
import Mixfix.Acyclic.Lemma
private
  module Acyclic = Mixfix.Acyclic.Grammar        g
  module ALemma  = Mixfix.Acyclic.Lemma          g
  module Cyclic  = Mixfix.Cyclic.Grammar acyclic g
open import Mixfix.Acyclic.Lib as ALib
open ALib.Semantics-⊕ renaming (_⊕_∈⟦_⟧·_ to _⊕_∈⟦_⟧A·_)
open import Mixfix.Cyclic.Lib as CLib renaming (⟦_⟧ to ⟦_⟧C)
open CLib.Semantics-⊕ renaming (_⊕_∈⟦_⟧·_ to _⊕_∈⟦_⟧C·_)

open PrecedenceCorrect acyclic g

⟦_⟧A :  {R}  ALib.ParserProg R  Parser NamePart R []
 p ⟧A = Simplified.⟦_⟧ (ALib.⟦_⟧ p)

module AcyclicToCyclic where

  mutual

    precs :  ps {s s′ e} 
            e  s′ ∈⟦ Acyclic.precs ps ⟧A· s 
            e  s′ ∈⟦  Cyclic.precs ps ⟧C· s
    precs []       ()
    precs (p  ps) (∣ˡ (<$> e∈p))  = ∣ˡ (<$> prec  p  e∈p)
    precs (p  ps) (∣ʳ (<$> e∈ps)) = ∣ʳ (<$> precs ps e∈ps)

    prec :  p {s s′ e} 
           e  s′ ∈⟦ Acyclic.prec p ⟧A· s 
           e  s′ ∈⟦  Cyclic.prec p ⟧C· s
    prec (precedence ops sucs) e∈ = prec′ e∈
      where
      p = precedence ops sucs

      module A = Acyclic.Prec ops sucs
      module C =  Cyclic.Prec p

      preRight :  {s s′ f} 
                 f  s′ ∈⟦ A.preRight ⟧A· s 
                 f  s′ ∈⟦ C.preRight ⟧C· s
      preRight (∣ˡ (<$>      i∈)) = ∣ˡ (<$>              inner _ i∈)
      preRight (∣ʳ (<$> ↑∈  i∈)) = ∣ʳ (<$> precs _ ↑∈  inner _ i∈)

      preRight⁺ :  {s s′ s″ fs e} 
                 fs           s′ ∈⟦ A.preRight +       ⟧A· s  
                 e            s″ ∈⟦ Acyclic.precs sucs ⟧A· s′ 
                 A.appʳ fs e  s″ ∈⟦ C.preRight⁺        ⟧C· s
      preRight⁺ {fs = _  ._} (+-[] f∈)     ↑∈ = preRight f∈ ⊛∞ ∣ʳ (<$> precs _ ↑∈)
      preRight⁺ {fs = _  ._} (+-∷  f∈ fs∈) ↑∈ = preRight f∈ ⊛∞ ∣ˡ (<$> preRight⁺ fs∈ ↑∈)

      postLeft :  {s s′ f} 
                 f  s′ ∈⟦ A.postLeft ⟧A· s 
                 f  s′ ∈⟦ C.postLeft ⟧C· s
      postLeft (∣ˡ (<$> i∈     )) = ∣ˡ (<$> inner _ i∈)
      postLeft (∣ʳ (<$> i∈  ↑∈)) = ∣ʳ (<$> inner _ i∈  precs _ ↑∈)

      postLeft⁺ :  {s s′ s″ o fs} 
                  o                 s′ ∈⟦ similar <$> C.postLeft⁺
                                          tighter <$> C.p↑ ⟧C· s 
                  fs                s″ ∈⟦ A.postLeft +       ⟧A· s′ 
                  ALemma.appˡ o fs  s″ ∈⟦ C.postLeft⁺        ⟧C· s
      postLeft⁺ {fs = _  ._} o∈ (+-[] f∈)     =                     <$> o∈ ⊛∞ postLeft f∈
      postLeft⁺ {fs = _  ._} o∈ (+-∷  f∈ fs∈) = postLeft⁺ (∣ˡ (<$> (<$> o∈ ⊛∞ postLeft f∈))) fs∈

      prec′ :  {s s′ assoc} {e : ExprIn p assoc} 
              (-, e)  s′ ∈⟦ Acyclic.prec p ⟧A· s 
              (-, e)  s′ ∈⟦  Cyclic.prec p ⟧C· s
      prec′ (∥ˡ (<$> i∈))                      = ∥ˡ (<$> inner _ i∈)
      prec′ (∥ʳ (∥ˡ (<$> ↑₁∈  i∈  ↑₂∈)))     = ∥ʳ (∥ˡ (<$> precs _ ↑₁∈  inner _ i∈ ⊛∞ precs _ ↑₂∈ ))
      prec′ (∥ʳ (∥ʳ (∥ˡ (<$> fs∈  ↑∈))))      = ∥ʳ (∥ʳ (∥ˡ (preRight⁺ fs∈ ↑∈)))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ (<$> ↑∈  fs∈))))) = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft⁺ (∣ʳ (<$> precs _ ↑∈)) fs∈))))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ()))))

    inner :  {fix} (ops : List ( (Operator fix))) {s s′ i} 
            i  s′ ∈⟦ Acyclic.inner ops ⟧A· s 
            i  s′ ∈⟦  Cyclic.inner ops ⟧C· s
    inner []               ()
    inner ((_ , op)  ops) (∣ˡ (<$> i∈)) = ∣ˡ (<$> inner′ _ i∈)
    inner ((_ , op)  ops) (∣ʳ (<$> i∈)) = ∣ʳ (<$> inner ops i∈)

    inner′ :  {arity} (ns : Vec NamePart (1 + arity)) {s s′ i} 
             i  s′ ∈⟦ Acyclic.expr between ns ⟧A· s 
             i  s′ ∈⟦  Cyclic.expr between ns ⟧C· s
    inner′ (n  .[]) between-[]           = between-[]
    inner′ (n  ns)  (between-∷ e∈g es∈g) =
      between-∷ (precs g e∈g) (inner′ ns es∈g)

module CyclicToAcyclic where

  mutual

    precs :  ps {s s′ e} 
            e  s′ ∈⟦  Cyclic.precs ps ⟧C· s 
            e  s′ ∈⟦ Acyclic.precs ps ⟧A· s
    precs []       ()
    precs (p  ps) (∣ˡ (<$> e∈p))  = ∣ˡ (<$> prec  p  e∈p)
    precs (p  ps) (∣ʳ (<$> e∈ps)) = ∣ʳ (<$> precs ps e∈ps)

    prec :  p {s s′ e} 
           e  s′ ∈⟦  Cyclic.prec p ⟧C· s 
           e  s′ ∈⟦ Acyclic.prec p ⟧A· s
    prec (precedence ops sucs) e∈ = prec′ e∈
      where
      p = precedence ops sucs

      module A = Acyclic.Prec ops sucs
      module C =  Cyclic.Prec p

      preRight :  {s s′ f} 
                 f  s′ ∈⟦ C.preRight ⟧C· s 
                 f  s′ ∈⟦ A.preRight ⟧A· s
      preRight (∣ˡ (<$>      i∈)) = ∣ˡ (<$>              inner _ i∈)
      preRight (∣ʳ (<$> ↑∈  i∈)) = ∣ʳ (<$> precs _ ↑∈  inner _ i∈)

      preRight⁺ :  {s s′ e} 
                  e  s′ ∈⟦ C.preRight⁺                    ⟧C· s 
                  e  s′ ∈⟦ A.appʳ <$> A.preRight +  A.p↑ ⟧A· s
      preRight⁺ (f∈ ⊛∞ ∣ˡ (<$> pre∈)) with preRight⁺ pre∈
      preRight⁺ (f∈ ⊛∞ ∣ˡ (<$> pre∈)) | <$> fs∈  ↑∈ = <$> +-∷  (preRight f∈) fs∈  ↑∈
      preRight⁺ (f∈ ⊛∞ ∣ʳ (<$> ↑∈)  ) =                <$> +-[] (preRight f∈)      precs _ ↑∈

      postLeft :  {s s′ f} 
                 f  s′ ∈⟦ C.postLeft ⟧C· s 
                 f  s′ ∈⟦ A.postLeft ⟧A· s
      postLeft (∣ˡ (<$> i∈     )) = ∣ˡ (<$> inner _ i∈)
      postLeft (∣ʳ (<$> i∈  ↑∈)) = ∣ʳ (<$> inner _ i∈  precs _ ↑∈)

      postLeft⁺ :  {s s′ e} 
                  e  s′ ∈⟦ C.postLeft⁺                    ⟧C· s 
                  e  s′ ∈⟦ A.appˡ <$> A.p↑  A.postLeft + ⟧A· s
      postLeft⁺ (<$> ∣ˡ (<$> post∈) ⊛∞ f∈) with postLeft⁺ post∈
      postLeft⁺ (<$> ∣ˡ (<$> post∈) ⊛∞ f∈)
        | _⊛_ {x = fs} (<$> ↑∈) fs∈ = AS.cast∈ (ALemma.appˡ-∷ʳ _ fs _) (
                                             <$>         ↑∈  AS.+-∷ʳ fs∈ (postLeft f∈))
        where module AS = ALib.Semantics-⊕
      postLeft⁺ (<$> ∣ʳ (<$> ↑∈)    ⊛∞ f∈) = <$> precs _ ↑∈     +-[]     (postLeft f∈)

      prec′ :  {s s′ assoc} {e : ExprIn p assoc} 
              (-, e)  s′ ∈⟦  Cyclic.prec p ⟧C· s 
              (-, e)  s′ ∈⟦ Acyclic.prec p ⟧A· s
      prec′ (∥ˡ (<$> i∈))                   = ∥ˡ (<$> inner _ i∈)
      prec′ (∥ʳ (∥ˡ (<$> ↑₁∈  i∈ ⊛∞ ↑₂∈))) = ∥ʳ (∥ˡ (<$> precs _ ↑₁∈  inner _ i∈  precs _ ↑₂∈ ))
      prec′ (∥ʳ (∥ʳ (∥ˡ pre∈)))             = ∥ʳ (∥ʳ (∥ˡ (preRight⁺ pre∈)))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ post∈))))       = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft⁺ post∈))))
      prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ()))))

    inner :  {fix} (ops : List ( (Operator fix))) {s s′ i} 
            i  s′ ∈⟦  Cyclic.inner ops ⟧C· s 
            i  s′ ∈⟦ Acyclic.inner ops ⟧A· s
    inner []               ()
    inner ((_ , op)  ops) (∣ˡ (<$> i∈)) = ∣ˡ (<$> inner′ _ i∈)
    inner ((_ , op)  ops) (∣ʳ (<$> i∈)) = ∣ʳ (<$> inner ops i∈)

    inner′ :  {arity} (ns : Vec NamePart (1 + arity)) {s s′ i} 
             i  s′ ∈⟦  Cyclic.expr between ns ⟧C· s 
             i  s′ ∈⟦ Acyclic.expr between ns ⟧A· s
    inner′ (n  .[]) between-[]           = between-[]
    inner′ (n  ns)  (between-∷ e∈g es∈g) =
      between-∷ (precs g e∈g) (inner′ ns es∈g)

acyclicToCyclic
  :  {e s}  e  Simplified.⟦_⟧ Acyclic.expression · s 
              e                  Cyclic.expression · s
acyclicToCyclic =
  ContSem.sound               
  CLib.Semantics-⊕.sound      
  AcyclicToCyclic.precs _     
  ALib.Semantics-⊕.complete _ 
  SSem.⊕-complete             
  SSem.complete _

cyclicToAcyclic
  :  {e s}  e                  Cyclic.expression · s 
              e  Simplified.⟦_⟧ Acyclic.expression · s
cyclicToAcyclic =
  SSem.sound                  
  SSem.⊕-sound                
  ALib.Semantics-⊕.sound      
  CyclicToAcyclic.precs _     
  CLib.Semantics-⊕.complete _ 
  ContSem.complete