import Syntax.Simple.Signature as S
import Syntax.BiTyped.Signature as B
import Theory.ModeCorrectness.Signature as MC
module Theory.ModeCorrectness.UniqueSynthesised
{SD : S.SigD} (D : B.SigD SD) (mc : MC.ModeCorrect SD D) where
open import Prelude
open MC SD
open B SD
open import Syntax.Simple SD
open import Syntax.Context SD
open import Syntax.BiTyped.Functor SD
import Syntax.Typed.Raw.Functor SD as R
open import Theory.Erasure
open import Syntax.BiTyped.Term D
open import Syntax.Typed.Raw.Term (erase D)
import Theory.ModeCorrectness.Functor SD as M
private variable
Ξ : ℕ
xs : Fins# Ξ
Γ : Cxt 0
A B : TExp Ξ
As : TExps Ξ
ρ₁ ρ₂ : TSub Ξ 0
uniq-⇒-var : (i : A ∈ Γ) (j : B ∈ Γ) → L.index i ≡ L.index j → A ≡ B
uniq-⇒-var (here refl) (here refl) _ = refl
uniq-⇒-var (there i) (there j) eq = uniq-⇒-var i j (F.suc-injective eq)
mutual
uniq-⇒
: {r : Raw (length Γ)}
→ (⊢t : Γ ⊢ r ⇒ A) (⊢u : Γ ⊢ r ⇒ B)
→ A ≡ B
uniq-⇒ (var i ieq) (var j jeq) = uniq-⇒-var i j (trans ieq (sym jeq))
uniq-⇒ (A ∋ t) (.A ∋ u) = refl
uniq-⇒ {r = op (i , rs)} (op (deq , _ , refl , ts)) (op (_ , _ , refl , us)) =
uniq-⇒ᶜ (SigD.ar D i) deq (mc i) ts us
uniq-⇒ᶜ
: (D@(ι d A Ds) : OpD) → d ≡ Syn → ModeCorrectᶜ D
→ ∀ {rs ρ₁ ρ₂}
→ ⟦ Ds ⟧ᵃˢ Raw _⊢_[_]_ ρ₁ Γ rs
→ ⟦ Ds ⟧ᵃˢ Raw _⊢_[_]_ ρ₂ Γ rs
→ A ⟨ ρ₁ ⟩ ≡ A ⟨ ρ₂ ⟩
uniq-⇒ᶜ (ι Syn A Ds) refl (⊆xs , SDs) ts us =
≡-fv A λ x → uniq-⇒ⁿ Ds SDs ts us (⊆xs _)
uniq-⇒ⁿ
: (Ds : ArgsD Ξ) → ModeCorrectᵃˢ [] Ds
→ {rs : R.⟦ eraseᵃˢ Ds ⟧ᵃˢ Raw (length Γ)}
→ (ts : ⟦ Ds ⟧ᵃˢ Raw _⊢_[_]_ ρ₁ Γ rs)
→ (us : ⟦ Ds ⟧ᵃˢ Raw _⊢_[_]_ ρ₂ Γ rs)
→ ∀ {x} → x #∈ (known Ds)
→ ρ₁ x ≡ ρ₂ x
uniq-⇒ⁿ [] _ _ _ ()
uniq-⇒ⁿ (_ ⊢[ Chk ] _ ∷ Ds) (_ , SDs) (_ , ⊢ts) (_ , ⊢us) =
uniq-⇒ⁿ Ds SDs ⊢ts ⊢us
uniq-⇒ⁿ (Δ ⊢[ Syn ] A ∷ Ds) (SD , SDs) (⊢t , ⊢ts) (⊢u , ⊢us) x∈ with ∈-∪⁻ (vars A) x∈
... | inl x∈A = uniq-⇒ᵃ A Δ SD ⊢t ⊢u (uniq-⇒ⁿ Ds SDs ⊢ts ⊢us) x∈A
... | inr x∈Ds = uniq-⇒ⁿ Ds SDs ⊢ts ⊢us x∈Ds
uniq-⇒ᵃ
: (C : TExp Ξ) (Δ : TExps Ξ) → Cover xs Δ
→ {r : R.⟦ Δ ⟧ᵃ Raw (length Γ)}
→ (t : ⟦ Δ ⟧ᵃ Raw (_⊢_[ Syn ] (C ⟨ ρ₁ ⟩)) ρ₁ Γ r)
→ (u : ⟦ Δ ⟧ᵃ Raw (_⊢_[ Syn ] (C ⟨ ρ₂ ⟩)) ρ₂ Γ r)
→ (∀ {x} → x #∈ xs → ρ₁ x ≡ ρ₂ x)
→ ∀ {x} → x #∈ vars C
→ ρ₁ x ≡ ρ₂ x
uniq-⇒ᵃ C [] _ ⊢t ⊢u f x = ≡-fv-inv C (uniq-⇒ ⊢t ⊢u) (∈vars→∈ᵥ x)
uniq-⇒ᵃ C (A ∷ Δ) (A⊆xs ∷ Δ⊆xs) ⊢t ⊢u f =
uniq-⇒ᵃ C Δ Δ⊆xs (subst (λ A → (⟦ Δ ⟧ᵃ _ _) _ (A ∷ _) _) A₁=A₂ ⊢t) ⊢u f
where A₁=A₂ = ≡-fv A λ x∈ → f (A⊆xs (∈ᵥ→∈vars x∈))
¬switch
: {r : Raw (length Γ)}
→ Γ ⊢ r ⇒ A
→ B ≢ A
→ ¬ Γ ⊢ r ⇐ B
¬switch ⊢t B≠A (⊢t′ ↑ B=A) rewrite uniq-⇒ ⊢t ⊢t′ = B≠A B=A
¬switch (op (d≡Syn , _)) B≠A (op (d≡Chk , _)) = Chk≢Syn (trans (sym d≡Chk) d≡Syn)
uniqᵐ-⇒
: (Δ : TExps Ξ) {(xs , ρ) (xs′ , ρ′): ∃Sub⊆ Ξ} {Δ⊆ : Cover xs Δ} {Δ⊆′ : Cover xs′ Δ}
→ (xs , ρ) ≤ (xs′ , ρ′)
→ {Γ : Cxt 0}
→ {t : R.⟦ Δ ⟧ᵃ Raw (length Γ)} → ∀ {B C}
→ M.⟦ Δ ⟧ᵃ (xs , ρ) Δ⊆ Raw (_⊢_⇒ B) Γ t
→ M.⟦ Δ ⟧ᵃ (xs′ , ρ′) Δ⊆′ Raw (_⊢_⇒ C) Γ t
→ B ≡ C
uniqᵐ-⇒ [] _ ⊢t ⊢t′ =
uniq-⇒ ⊢t ⊢t′
uniqᵐ-⇒ (A ∷ Δ) {xs , ρ} {xs′ , ρ′} {A⊆ ∷ Δ⊆} {A⊆′ ∷ Δ⊆′} p@(≤-con xs⊆xs′ ρ≤ρ′) {Γ} {t} ⊢t ⊢t′ =
uniqᵐ-⇒ Δ {_} {_} {_} {Δ⊆′} p ⊢t
$ subst (λ A → M.⟦ Δ ⟧ᵃ (xs′ , ρ′) Δ⊆′ Raw (_⊢_⇒ _) (A ∷ Γ) t)
(ρ=σ→subρ=subσ A ρ′ ρ A⊆′ A⊆ (sym ∘ helper)) ⊢t′
where
open ≡-Reasoning
helper : ∀ {x} (x∈ : x #∈ vars A) → ρ (A⊆ x∈) ≡ ρ′ (A⊆′ x∈)
helper x∈ = begin
ρ (A⊆ x∈)
≡⟨ ρ≤ρ′ (A⊆ x∈) ⟩
ρ′ (xs⊆xs′ (A⊆ x∈))
≡⟨ cong ρ′ (#∈-uniq _ _) ⟩
ρ′ (A⊆′ x∈)
∎