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
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
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)
correct : (e : Expr g) → e ∈ Grammar.expression · show e
correct e =
Semantics.⊕-sound (Lib.Semantics-⊕.sound (Correctness.expr e))