open import Mixfix.Expr
module Mixfix.Cyclic.Uniqueness
(i : PrecedenceGraphInterface)
(g : PrecedenceGraphInterface.PrecedenceGraph i)
where
open import Codata.Musical.Notation using (♭)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Unary.Any using (here)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product using (_,_; -,_; proj₂)
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open PrecedenceCorrect i g
open import TotalParserCombinators.Semantics hiding (_≅_)
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Cyclic.Lib as Lib
open Lib.Semantics
import Mixfix.Cyclic.Grammar
private module Grammar = Mixfix.Cyclic.Grammar i g
module Unique where
data _≋_ {A : Set} {x₁ : A} {s₁ p₁} (∈ : x₁ ∈⟦ p₁ ⟧· s₁) :
∀ {x₂ : A} {s₂ p₂} → x₂ ∈⟦ p₂ ⟧· s₂ → Set where
refl : ∈ ≋ ∈
mutual
precs : ∀ ps {s₁ s₂} {e₁ e₂ : Expr ps}
(∈₁ : e₁ ∈⟦ Grammar.precs ps ⟧· s₁)
(∈₂ : e₂ ∈⟦ Grammar.precs ps ⟧· s₂) →
e₁ ≡ e₂ → ∈₁ ≋ ∈₂
precs [] () () _
precs (p ∷ ps) (∣ʳ (<$>_ {x = ( _ ∙ _)} ∈₁))
(∣ʳ (<$>_ {x = (._ ∙ ._)} ∈₂)) refl with precs ps ∈₁ ∈₂ refl
precs (p ∷ ps) (∣ʳ (<$>_ {x = ( _ ∙ _)} ∈₁))
(∣ʳ (<$>_ {x = (._ ∙ ._)} .∈₁)) refl | refl = refl
precs (p ∷ ps) (∣ˡ (<$> ∈₁)) (∣ʳ (<$>_ {x = _ ∙ _} ∈₂)) ()
precs (p ∷ ps) (∣ʳ (<$>_ {x = _ ∙ _} ∈₁)) (∣ˡ (<$> ∈₂)) ()
precs (p ∷ ps) (∣ˡ (<$>_ {x = e₁} ∈₁)) (∣ˡ (<$>_ {x = e₂} ∈₂)) eq =
helper (lemma₁ eq) (lemma₂ eq) ∈₁ ∈₂
where
lemma₁ : ∀ {assoc₁ assoc₂}
{e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
(Expr._∙_ (here {xs = ps} refl) e₁) ≡ (here refl ∙ e₂) →
assoc₁ ≡ assoc₂
lemma₁ refl = refl
lemma₂ : ∀ {assoc₁ assoc₂}
{e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
(Expr._∙_ (here {xs = ps} refl) e₁) ≡ (here refl ∙ e₂) →
e₁ ≅ e₂
lemma₂ refl = refl
helper : ∀ {assoc₁ assoc₂ s₁ s₂}
{e₁ : ExprIn p assoc₁} {e₂ : ExprIn p assoc₂} →
assoc₁ ≡ assoc₂ → e₁ ≅ e₂ →
(∈₁ : (-, e₁) ∈⟦ Grammar.prec p ⟧· s₁) →
(∈₂ : (-, e₂) ∈⟦ Grammar.prec p ⟧· s₂) →
∣ˡ {p₁ = (λ e → here refl ∙ proj₂ e) <$> Grammar.prec p}
{p₂ = weakenE <$> Grammar.precs ps} (<$> ∈₁) ≋
∣ˡ {p₁ = (λ e → here refl ∙ proj₂ e) <$> Grammar.prec p}
{p₂ = weakenE <$> Grammar.precs ps} (<$> ∈₂)
helper refl refl ∈₁ ∈₂ with prec ∈₁ ∈₂
helper refl refl ∈ .∈ | refl = refl
prec : ∀ {p assoc s₁ s₂} {e : ExprIn p assoc}
(∈₁ : (-, e) ∈⟦ Grammar.prec p ⟧· s₁)
(∈₂ : (-, e) ∈⟦ Grammar.prec p ⟧· s₂) →
∈₁ ≋ ∈₂
prec {p} ∈₁′ ∈₂′ = prec′ ∈₁′ ∈₂′ refl
where
module P = Grammar.Prec p
preRight⁺ : ∀ {s₁ s₂} {e₁ e₂ : ExprIn p right}
(∈₁ : e₁ ∈⟦ P.preRight⁺ ⟧· s₁)
(∈₂ : e₂ ∈⟦ P.preRight⁺ ⟧· s₂) →
e₁ ≡ e₂ → ∈₁ ≋ ∈₂
preRight⁺ (∣ˡ (<$> ∈₁) ⊛∞ ∣ˡ (<$> ∈₂))
(∣ˡ (<$> ∈₁′) ⊛∞ ∣ˡ (<$> ∈₂′)) refl with inner _ ∈₁ ∈₁′ refl | preRight⁺ ∈₂ ∈₂′ refl
preRight⁺ (∣ˡ (<$> ∈₁) ⊛∞ ∣ˡ (<$> ∈₂))
(∣ˡ (<$> .∈₁) ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl = refl
preRight⁺ (∣ˡ (<$> ∈₁) ⊛∞ ∣ʳ (<$> ∈₂))
(∣ˡ (<$> ∈₁′) ⊛∞ ∣ʳ (<$> ∈₂′)) refl with inner _ ∈₁ ∈₁′ refl | precs _ ∈₂ ∈₂′ refl
preRight⁺ (∣ˡ (<$> ∈₁) ⊛∞ ∣ʳ (<$> ∈₂))
(∣ˡ (<$> .∈₁) ⊛∞ ∣ʳ (<$> .∈₂)) refl | refl | refl = refl
preRight⁺ (∣ʳ (<$> ∈₁ ⊛ ∈₃) ⊛∞ ∣ˡ (<$> ∈₂))
(∣ʳ (<$> ∈₁′ ⊛ ∈₃′) ⊛∞ ∣ˡ (<$> ∈₂′)) refl with precs _ ∈₁ ∈₁′ refl | preRight⁺ ∈₂ ∈₂′ refl | inner _ ∈₃ ∈₃′ refl
preRight⁺ (∣ʳ (<$> ∈₁ ⊛ ∈₃) ⊛∞ ∣ˡ (<$> ∈₂))
(∣ʳ (<$> .∈₁ ⊛ .∈₃) ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl | refl = refl
preRight⁺ (∣ʳ (<$> ∈₁ ⊛ ∈₃) ⊛∞ ∣ʳ (<$> ∈₂))
(∣ʳ (<$> ∈₁′ ⊛ ∈₃′) ⊛∞ ∣ʳ (<$> ∈₂′)) refl with precs _ ∈₁ ∈₁′ refl | precs _ ∈₂ ∈₂′ refl | inner _ ∈₃ ∈₃′ refl
preRight⁺ (∣ʳ (<$> ∈₁ ⊛ ∈₃) ⊛∞ ∣ʳ (<$> ∈₂))
(∣ʳ (<$> .∈₁ ⊛ .∈₃) ⊛∞ ∣ʳ (<$> .∈₂)) refl | refl | refl | refl = refl
preRight⁺ (∣ˡ (<$> _) ⊛∞ _)
(∣ʳ (<$> _ ⊛ _) ⊛∞ _) ()
preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ _)
(∣ˡ (<$> _) ⊛∞ _) ()
preRight⁺ (∣ˡ (<$> _) ⊛∞ ∣ˡ (<$> _))
(∣ˡ (<$> _) ⊛∞ ∣ʳ (<$> _)) ()
preRight⁺ (∣ˡ (<$> _) ⊛∞ ∣ʳ (<$> _))
(∣ˡ (<$> _) ⊛∞ ∣ˡ (<$> _)) ()
preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ˡ (<$> _))
(∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ʳ (<$> _)) ()
preRight⁺ (∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ʳ (<$> _))
(∣ʳ (<$> _ ⊛ _) ⊛∞ ∣ˡ (<$> _)) ()
postLeft⁺ : ∀ {s₁ s₂} {e₁ e₂ : ExprIn p left}
(∈₁ : e₁ ∈⟦ P.postLeft⁺ ⟧· s₁)
(∈₂ : e₂ ∈⟦ P.postLeft⁺ ⟧· s₂) →
e₁ ≡ e₂ → ∈₁ ≋ ∈₂
postLeft⁺ (<$> (∣ˡ (<$> ∈₁)) ⊛∞ ∣ˡ (<$> ∈₂))
(<$> (∣ˡ (<$> ∈₁′)) ⊛∞ ∣ˡ (<$> ∈₂′)) refl with postLeft⁺ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl
postLeft⁺ (<$> (∣ˡ (<$> ∈₁)) ⊛∞ ∣ˡ (<$> ∈₂))
(<$> (∣ˡ (<$> .∈₁)) ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl = refl
postLeft⁺ (<$> (∣ʳ (<$> ∈₁)) ⊛∞ ∣ˡ (<$> ∈₂))
(<$> (∣ʳ (<$> ∈₁′)) ⊛∞ ∣ˡ (<$> ∈₂′)) refl with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl
postLeft⁺ (<$> (∣ʳ (<$> ∈₁)) ⊛∞ ∣ˡ (<$> ∈₂))
(<$> (∣ʳ (<$> .∈₁)) ⊛∞ ∣ˡ (<$> .∈₂)) refl | refl | refl = refl
postLeft⁺ (<$> (∣ˡ (<$> ∈₁)) ⊛∞ ∣ʳ (<$> ∈₂ ⊛ ∈₃))
(<$> (∣ˡ (<$> ∈₁′)) ⊛∞ ∣ʳ (<$> ∈₂′ ⊛ ∈₃′)) refl with postLeft⁺ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
postLeft⁺ (<$> (∣ˡ (<$> ∈₁)) ⊛∞ ∣ʳ (<$> ∈₂ ⊛ ∈₃))
(<$> (∣ˡ (<$> .∈₁)) ⊛∞ ∣ʳ (<$> .∈₂ ⊛ .∈₃)) refl | refl | refl | refl = refl
postLeft⁺ (<$> (∣ʳ (<$> ∈₁)) ⊛∞ ∣ʳ (<$> ∈₂ ⊛ ∈₃))
(<$> (∣ʳ (<$> ∈₁′)) ⊛∞ ∣ʳ (<$> ∈₂′ ⊛ ∈₃′)) refl with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
postLeft⁺ (<$> (∣ʳ (<$> ∈₁)) ⊛∞ ∣ʳ (<$> ∈₂ ⊛ ∈₃))
(<$> (∣ʳ (<$> .∈₁)) ⊛∞ ∣ʳ (<$> .∈₂ ⊛ .∈₃)) refl | refl | refl | refl = refl
postLeft⁺ (<$> _ ⊛∞ ∣ˡ (<$> _))
(<$> _ ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()
postLeft⁺ (<$> _ ⊛∞ ∣ʳ (<$> _ ⊛ _))
(<$> _ ⊛∞ ∣ˡ (<$> _)) ()
postLeft⁺ (<$> (∣ˡ (<$> _)) ⊛∞ ∣ˡ (<$> _))
(<$> (∣ʳ (<$> _)) ⊛∞ ∣ˡ (<$> _)) ()
postLeft⁺ (<$> (∣ʳ (<$> _)) ⊛∞ ∣ˡ (<$> _))
(<$> (∣ˡ (<$> _)) ⊛∞ ∣ˡ (<$> _)) ()
postLeft⁺ (<$> (∣ˡ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _))
(<$> (∣ʳ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()
postLeft⁺ (<$> (∣ʳ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _))
(<$> (∣ˡ (<$> _)) ⊛∞ ∣ʳ (<$> _ ⊛ _)) ()
prec′ : ∀ {assoc s₁ s₂} {e₁ e₂ : ExprIn p assoc} →
(∈₁ : (-, e₁) ∈⟦ Grammar.prec p ⟧· s₁)
(∈₂ : (-, e₂) ∈⟦ Grammar.prec p ⟧· s₂) →
e₁ ≡ e₂ → ∈₁ ≋ ∈₂
prec′ (∥ˡ (<$> ∈₁)) (∥ˡ (<$> ∈₂)) refl with inner _ ∈₁ ∈₂ refl
prec′ (∥ˡ (<$> ∈₁)) (∥ˡ (<$> .∈₁)) refl | refl = refl
prec′ (∥ʳ (∥ˡ (<$> ∈₁ ⊛ ∈₂ ⊛∞ ∈₃ )))
(∥ʳ (∥ˡ (<$> ∈₁′ ⊛ ∈₂′ ⊛∞ ∈₃′))) refl
with precs _ ∈₁ ∈₁′ refl | inner _ ∈₂ ∈₂′ refl | precs _ ∈₃ ∈₃′ refl
prec′ (∥ʳ (∥ˡ (<$> ∈₁ ⊛ ∈₂ ⊛∞ ∈₃)))
(∥ʳ (∥ˡ (<$> .∈₁ ⊛ .∈₂ ⊛∞ .∈₃))) refl | refl | refl | refl = refl
prec′ (∥ʳ (∥ʳ (∥ˡ ∈₁))) (∥ʳ (∥ʳ (∥ˡ ∈₂))) refl with preRight⁺ ∈₁ ∈₂ refl
prec′ (∥ʳ (∥ʳ (∥ˡ ∈₁))) (∥ʳ (∥ʳ (∥ˡ .∈₁))) refl | refl = refl
prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ ∈₁)))) (∥ʳ (∥ʳ (∥ʳ (∥ˡ ∈₂)))) refl with postLeft⁺ ∈₁ ∈₂ refl
prec′ (∥ʳ (∥ʳ (∥ʳ (∥ˡ ∈₁)))) (∥ʳ (∥ʳ (∥ʳ (∥ˡ .∈₁)))) refl | refl = refl
prec′ (∥ˡ (<$> _)) (∥ʳ (∥ˡ (<$> _ ⊛ _ ⊛∞ _))) ()
prec′ (∥ʳ (∥ˡ (<$> _ ⊛ _ ⊛∞ _))) (∥ˡ (<$> _)) ()
prec′ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ())))) _ _
prec′ _ (∥ʳ (∥ʳ (∥ʳ (∥ʳ ())))) _
inner : ∀ {fix s₁ s₂} ops {e₁ e₂ : Inner {fix} ops}
(∈₁ : e₁ ∈⟦ Grammar.inner ops ⟧· s₁)
(∈₂ : e₂ ∈⟦ Grammar.inner ops ⟧· s₂) →
e₁ ≡ e₂ → ∈₁ ≋ ∈₂
inner [] () () _
inner ((_ , op) ∷ ops) (∣ˡ (<$> ∈₁))
(∣ˡ (<$> ∈₂)) refl with inner′ _ _ ∈₁ ∈₂
inner ((_ , op) ∷ ops) (∣ˡ (<$> ∈₁))
(∣ˡ (<$> .∈₁)) refl | refl = refl
inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = ( _ ∙ _)} ∈₁))
(∣ʳ (<$>_ {x = (._ ∙ ._)} ∈₂)) refl with inner ops ∈₁ ∈₂ refl
inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = ( _ ∙ _)} ∈₁))
(∣ʳ (<$>_ {x = (._ ∙ ._)} .∈₁)) refl | refl = refl
inner ((_ , op) ∷ ops) (∣ˡ (<$> ∈₁)) (∣ʳ (<$>_ {x = (_ ∙ _)} ∈₂)) ()
inner ((_ , op) ∷ ops) (∣ʳ (<$>_ {x = (_ ∙ _)} ∈₁)) (∣ˡ (<$> ∈₂)) ()
inner′ : ∀ {arity s₁ s₂}
(ns : Vec NamePart (1 + arity))
(args : Vec (Expr anyPrecedence) arity)
(∈₁ : args ∈⟦ Grammar.expr between ns ⟧· s₁)
(∈₂ : args ∈⟦ Grammar.expr between ns ⟧· s₂) →
∈₁ ≋ ∈₂
inner′ (n ∷ []) [] between-[] between-[] = refl
inner′ (n ∷ n′ ∷ ns) (arg ∷ args)
(between-∷ ∈₁ ∈⋯₁) (between-∷ ∈₂ ∈⋯₂)
with precs _ ∈₁ ∈₂ refl | inner′ (n′ ∷ ns) args ∈⋯₁ ∈⋯₂
inner′ (n ∷ n′ ∷ ns) (arg ∷ args)
(between-∷ ∈₁ ∈⋯₁) (between-∷ .∈₁ .∈⋯₁) | refl | refl = refl
unique : ∀ {e s₁ s₂} →
e ∈ Grammar.expression · s₁ →
e ∈ Grammar.expression · s₂ →
s₁ ≡ s₂
unique ∈₁ ∈₂ with ∈₁′ | ∈₂′ | Unique.precs _ ∈₁′ ∈₂′ refl
where
∈₁′ = Lib.Semantics.complete (♭ Grammar.expr) ∈₁
∈₂′ = Lib.Semantics.complete (♭ Grammar.expr) ∈₂
... | ∈ | .∈ | Unique.refl = refl