From 5e413d459a6523022414af640ef54cbef431e0d4 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Thu, 26 Oct 2023 22:17:04 -0400 Subject: [PATCH] agda: Use glub symbol for type meet --- core/erasure.agda | 2 +- core/lemmas.agda | 16 +- core/mexp.agda | 6 +- core/typ.agda | 354 ++++++++++++++++++++-------------------- core/uexp.agda | 2 +- marking/marking.agda | 4 +- marking/totality.agda | 4 +- marking/unicity.agda | 24 +-- marking/wellformed.agda | 24 +-- 9 files changed, 218 insertions(+), 218 deletions(-) diff --git a/core/erasure.agda b/core/erasure.agda index 26c4027..75588fa 100644 --- a/core/erasure.agda +++ b/core/erasure.agda @@ -17,7 +17,7 @@ module core.erasure where (⊢ ě₁ + ě₂) ⇒□ = ‵ (ě₁ ⇐□) + (ě₂ ⇐□) ⊢tt ⇒□ = ‵tt ⊢ff ⇒□ = ‵ff - ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□) + ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□) ⊢⟦_⟧ {y = y} ∌y ⇒□ = ‵ y ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□) ⊢⟨ ě₁ , ě₂ ⟩ ⇒□ = ‵⟨ ě₁ ⇒□ , ě₂ ⇒□ ⟩ diff --git a/core/lemmas.agda b/core/lemmas.agda index 17565c0..cf59ee1 100644 --- a/core/lemmas.agda +++ b/core/lemmas.agda @@ -55,10 +55,10 @@ module core.lemmas where ⇒-unicity (USPlus e₁⇐num e₂⇐num) (USPlus e₁⇐num′ e₂⇐num′) = refl ⇒-unicity USTrue USTrue = refl ⇒-unicity USFalse USFalse = refl - ⇒-unicity (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (USIf e₁⇐bool′ e₂⇒τ₁′ e₃⇒τ₂′ τ₁⊔τ₂′) + ⇒-unicity (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) (USIf e₁⇐bool′ e₂⇒τ₁′ e₃⇒τ₂′ τ₁⊓τ₂′) rewrite ⇒-unicity e₂⇒τ₁ e₂⇒τ₁′ | ⇒-unicity e₃⇒τ₂ e₃⇒τ₂′ - | ⊔-unicity τ₁⊔τ₂ τ₁⊔τ₂′ = refl + | ⊓-unicity τ₁⊓τ₂ τ₁⊓τ₂′ = refl ⇒-unicity (USPair e₁⇒τ₁ e₂⇒τ₂) (USPair e₁⇒τ₁′ e₂⇒τ₂′) rewrite ⇒-unicity e₁⇒τ₁ e₁⇒τ₁′ | ⇒-unicity e₂⇒τ₂ e₂⇒τ₂′ = refl @@ -85,8 +85,8 @@ module core.lemmas where ⇒-~-⇐ (USPlus e₁⇐num e₂⇐num) τ′~num = UASubsume (USPlus e₁⇐num e₂⇐num) τ′~num USuPlus ⇒-~-⇐ USTrue τ′~bool = UASubsume USTrue τ′~bool USuTrue ⇒-~-⇐ USFalse τ′~bool = UASubsume USFalse τ′~bool USuFalse - ⇒-~-⇐ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) τ′~τ - with ⟨ τ₁~τ′ , τ₂~τ′ ⟩ ← ⊔⇒-~→~ τ₁⊔τ₂ (~-sym τ′~τ) + ⇒-~-⇐ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) τ′~τ + with ⟨ τ₁~τ′ , τ₂~τ′ ⟩ ← ⊓⇒-~→~ τ₁⊓τ₂ (~-sym τ′~τ) with e₂⇐τ₁′ ← ⇒-~-⇐ e₂⇒τ₁ (~-sym τ₁~τ′) | e₃⇐τ₂′ ← ⇒-~-⇐ e₃⇒τ₂ (~-sym τ₂~τ′) = UAIf e₁⇐bool e₂⇐τ₁′ e₃⇐τ₂′ @@ -116,9 +116,9 @@ module core.lemmas where ⊢⇐-⊢⇒ (⊢ ě₁ ∙ ě₂ ∙ ě₃) with ⟨ τ₁ , ⟨ ě₂′ , eq ⟩ ⟩ ← ⊢⇐-⊢⇒ ě₂ rewrite eq with ⟨ τ₂ , ⟨ ě₃′ , eq ⟩ ⟩ ← ⊢⇐-⊢⇒ ě₃ rewrite eq - with τ₁ ⊔? τ₂ - ... | yes ⟨ τ , τ₁⊔τ₂ ⟩ = ⟨ τ , ⟨ ⊢ ě₁ ∙ ě₂′ ∙ ě₃′ [ τ₁⊔τ₂ ] , refl ⟩ ⟩ - ... | no ¬τ₁⊔τ₂ = ⟨ unknown , ⟨ ⊢⦉ ě₁ ∙ ě₂′ ∙ ě₃′ ⦊[ ¬⊔→~̸ ¬τ₁⊔τ₂ ] , refl ⟩ ⟩ + with τ₁ ⊓? τ₂ + ... | yes ⟨ τ , τ₁⊓τ₂ ⟩ = ⟨ τ , ⟨ ⊢ ě₁ ∙ ě₂′ ∙ ě₃′ [ τ₁⊓τ₂ ] , refl ⟩ ⟩ + ... | no ¬τ₁⊓τ₂ = ⟨ unknown , ⟨ ⊢⦉ ě₁ ∙ ě₂′ ∙ ě₃′ ⦊[ ¬⊓→~̸ ¬τ₁⊓τ₂ ] , refl ⟩ ⟩ ⊢⇐-⊢⇒ ⊢⟨ ě₁ , ě₂ ⟩[ τ▸ ] with ⟨ τ₁ , ⟨ ě₁′ , eq ⟩ ⟩ ← ⊢⇐-⊢⇒ ě₁ rewrite eq with ⟨ τ₂ , ⟨ ě₂′ , eq ⟩ ⟩ ← ⊢⇐-⊢⇒ ě₂ rewrite eq @@ -162,7 +162,7 @@ module core.lemmas where ⊢⇒-⊢⇐ ě@(⊢ ě₁ + ě₂) = ⊢⇒-⊢⇐-subsume ě MSuPlus ⊢⇒-⊢⇐ ě@(⊢tt) = ⊢⇒-⊢⇐-subsume ě MSuTrue ⊢⇒-⊢⇐ ě@(⊢ff) = ⊢⇒-⊢⇐-subsume ě MSuFalse - ⊢⇒-⊢⇐ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + ⊢⇒-⊢⇐ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ] with ⟨ ě₂′ , eq ⟩ ← ⊢⇒-⊢⇐ ě₂ rewrite eq with ⟨ ě₃′ , eq ⟩ ← ⊢⇒-⊢⇐ ě₃ rewrite eq = ⟨ ⊢ ě₁ ∙ ě₂′ ∙ ě₃′ , refl ⟩ ⊢⇒-⊢⇐ {τ′ = τ′} ⊢⟨ ě₁ , ě₂ ⟩ diff --git a/core/mexp.agda b/core/mexp.agda index e62b4d4..21af67c 100644 --- a/core/mexp.agda +++ b/core/mexp.agda @@ -75,7 +75,7 @@ module core.mexp where → (ě₁ : Γ ⊢⇐ bool) → (ě₂ : Γ ⊢⇒ τ₁) → (ě₃ : Γ ⊢⇒ τ₂) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) + → (τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ) → Γ ⊢⇒ τ -- MSFree @@ -307,11 +307,11 @@ module core.mexp where → {ě₁ : Γ ⊢⇐ bool} → {ě₂ : Γ ⊢⇒ τ₁} → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → {τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ} → (less₁ : Markless⇐ ě₁) → (less₂ : Markless⇒ ě₂) → (less₃ : Markless⇒ ě₃) - → Markless⇒ {Γ} (⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ]) + → Markless⇒ {Γ} (⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ]) MLSPair : ∀ {Γ τ₁ τ₂} → {ě₁ : Γ ⊢⇒ τ₁} diff --git a/core/typ.agda b/core/typ.agda index 275edd0..578d617 100644 --- a/core/typ.agda +++ b/core/typ.agda @@ -398,225 +398,225 @@ module core.typ where open consistency -- greatest lower bound (where the unknown type is the top of the imprecision partial order) - data _⊔_⇒_ : (τ₁ τ₂ τ : Typ) → Set where - TJBase : {τ : Typ} → (b : τ base) → τ ⊔ τ ⇒ τ - TJUnknown : unknown ⊔ unknown ⇒ unknown - TJUnknownBase : {τ : Typ} → (b : τ base) → unknown ⊔ τ ⇒ τ - TJBaseUnknown : {τ : Typ} → (b : τ base) → τ ⊔ unknown ⇒ τ + data _⊓_⇒_ : (τ₁ τ₂ τ : Typ) → Set where + TJBase : {τ : Typ} → (b : τ base) → τ ⊓ τ ⇒ τ + TJUnknown : unknown ⊓ unknown ⇒ unknown + TJUnknownBase : {τ : Typ} → (b : τ base) → unknown ⊓ τ ⇒ τ + TJBaseUnknown : {τ : Typ} → (b : τ base) → τ ⊓ unknown ⇒ τ TJArr : {τ₁ τ₂ τ₁′ τ₂′ τ₁″ τ₂″ : Typ} - → (τ₁⊔τ₁′ : τ₁ ⊔ τ₁′ ⇒ τ₁″) - → (τ₂⊔τ₂′ : τ₂ ⊔ τ₂′ ⇒ τ₂″) - → τ₁ -→ τ₂ ⊔ τ₁′ -→ τ₂′ ⇒ τ₁″ -→ τ₂″ + → (τ₁⊓τ₁′ : τ₁ ⊓ τ₁′ ⇒ τ₁″) + → (τ₂⊓τ₂′ : τ₂ ⊓ τ₂′ ⇒ τ₂″) + → τ₁ -→ τ₂ ⊓ τ₁′ -→ τ₂′ ⇒ τ₁″ -→ τ₂″ TJUnknownArr : {τ₁ τ₂ : Typ} - → unknown ⊔ τ₁ -→ τ₂ ⇒ τ₁ -→ τ₂ + → unknown ⊓ τ₁ -→ τ₂ ⇒ τ₁ -→ τ₂ TJArrUnknown : {τ₁ τ₂ : Typ} - → τ₁ -→ τ₂ ⊔ unknown ⇒ τ₁ -→ τ₂ + → τ₁ -→ τ₂ ⊓ unknown ⇒ τ₁ -→ τ₂ TJProd : {τ₁ τ₂ τ₁′ τ₂′ τ₁″ τ₂″ : Typ} - → (τ₁⊔τ₁′ : τ₁ ⊔ τ₁′ ⇒ τ₁″) - → (τ₂⊔τ₂′ : τ₂ ⊔ τ₂′ ⇒ τ₂″) - → τ₁ -× τ₂ ⊔ τ₁′ -× τ₂′ ⇒ τ₁″ -× τ₂″ + → (τ₁⊓τ₁′ : τ₁ ⊓ τ₁′ ⇒ τ₁″) + → (τ₂⊓τ₂′ : τ₂ ⊓ τ₂′ ⇒ τ₂″) + → τ₁ -× τ₂ ⊓ τ₁′ -× τ₂′ ⇒ τ₁″ -× τ₂″ TJUnknownProd : {τ₁ τ₂ : Typ} - → unknown ⊔ τ₁ -× τ₂ ⇒ τ₁ -× τ₂ + → unknown ⊓ τ₁ -× τ₂ ⇒ τ₁ -× τ₂ TJProdUnknown : {τ₁ τ₂ : Typ} - → τ₁ -× τ₂ ⊔ unknown ⇒ τ₁ -× τ₂ + → τ₁ -× τ₂ ⊓ unknown ⇒ τ₁ -× τ₂ -- decidable meet - _⊔?_ : (τ₁ : Typ) → (τ₂ : Typ) → Dec (∃[ τ ] τ₁ ⊔ τ₂ ⇒ τ) - num ⊔? num = yes ⟨ num , TJBase TBNum ⟩ - num ⊔? bool = no λ() - num ⊔? unknown = yes ⟨ num , TJBaseUnknown TBNum ⟩ - num ⊔? (_ -→ _) = no λ() - num ⊔? (_ -× _) = no λ() - bool ⊔? num = no λ() - bool ⊔? bool = yes ⟨ bool , TJBase TBBool ⟩ - bool ⊔? unknown = yes ⟨ bool , TJBaseUnknown TBBool ⟩ - bool ⊔? (_ -→ _) = no λ() - bool ⊔? (_ -× _) = no λ() - unknown ⊔? num = yes ⟨ num , TJUnknownBase TBNum ⟩ - unknown ⊔? bool = yes ⟨ bool , TJUnknownBase TBBool ⟩ - unknown ⊔? unknown = yes ⟨ unknown , TJUnknown ⟩ - unknown ⊔? (τ₁ -→ τ₂) = yes ⟨ τ₁ -→ τ₂ , TJUnknownArr ⟩ - unknown ⊔? (τ₁ -× τ₂) = yes ⟨ τ₁ -× τ₂ , TJUnknownProd ⟩ - (τ₁ -→ τ₂) ⊔? num = no λ() - (τ₁ -→ τ₂) ⊔? bool = no λ() - (τ₁ -→ τ₂) ⊔? unknown = yes ⟨ τ₁ -→ τ₂ , TJArrUnknown ⟩ - (τ₁ -→ τ₂) ⊔? (τ₁′ -→ τ₂′) - with τ₁ ⊔? τ₁′ | τ₂ ⊔? τ₂′ - ... | yes ⟨ τ , τ₁⊔τ₁′ ⟩ | yes ⟨ τ′ , τ₂⊔τ₂′′ ⟩ = yes ⟨ τ -→ τ′ , TJArr τ₁⊔τ₁′ τ₂⊔τ₂′′ ⟩ - ... | _ | no ¬τ₂⊔τ₂′ = no λ { ⟨ .(_ -→ _) , TJArr {τ₂″ = τ₂″} τ₁⊔τ₁′″ τ₂⊔τ₂′″ ⟩ → ¬τ₂⊔τ₂′ ⟨ τ₂″ , τ₂⊔τ₂′″ ⟩ } - ... | no ¬τ₁⊔τ₁′ | _ = no λ { ⟨ .(_ -→ _) , TJArr {τ₁″ = τ₁″} τ₁⊔τ₁′″ τ₂⊔τ₂′″ ⟩ → ¬τ₁⊔τ₁′ ⟨ τ₁″ , τ₁⊔τ₁′″ ⟩ } - (τ₁ -→ τ₂) ⊔? (τ₁′ -× τ₂′) = no λ() - (τ₁ -× τ₂) ⊔? num = no λ() - (τ₁ -× τ₂) ⊔? bool = no λ() - (τ₁ -× τ₂) ⊔? unknown = yes ⟨ τ₁ -× τ₂ , TJProdUnknown ⟩ - (τ₁ -× τ₂) ⊔? (τ₁′ -→ τ₂′) = no λ() - (τ₁ -× τ₂) ⊔? (τ₁′ -× τ₂′) - with τ₁ ⊔? τ₁′ | τ₂ ⊔? τ₂′ - ... | yes ⟨ τ , τ₁⊔τ₁′ ⟩ | yes ⟨ τ′ , τ₂⊔τ₂′′ ⟩ = yes ⟨ τ -× τ′ , TJProd τ₁⊔τ₁′ τ₂⊔τ₂′′ ⟩ - ... | _ | no ¬τ₂⊔τ₂′ = no λ { ⟨ .(_ -× _) , TJProd {τ₂″ = τ₂″} τ₁⊔τ₁′″ τ₂⊔τ₂′″ ⟩ → ¬τ₂⊔τ₂′ ⟨ τ₂″ , τ₂⊔τ₂′″ ⟩ } - ... | no ¬τ₁⊔τ₁′ | _ = no λ { ⟨ .(_ -× _) , TJProd {τ₁″ = τ₁″} τ₁⊔τ₁′″ τ₂⊔τ₂′″ ⟩ → ¬τ₁⊔τ₁′ ⟨ τ₁″ , τ₁⊔τ₁′″ ⟩ } + _⊓?_ : (τ₁ : Typ) → (τ₂ : Typ) → Dec (∃[ τ ] τ₁ ⊓ τ₂ ⇒ τ) + num ⊓? num = yes ⟨ num , TJBase TBNum ⟩ + num ⊓? bool = no λ() + num ⊓? unknown = yes ⟨ num , TJBaseUnknown TBNum ⟩ + num ⊓? (_ -→ _) = no λ() + num ⊓? (_ -× _) = no λ() + bool ⊓? num = no λ() + bool ⊓? bool = yes ⟨ bool , TJBase TBBool ⟩ + bool ⊓? unknown = yes ⟨ bool , TJBaseUnknown TBBool ⟩ + bool ⊓? (_ -→ _) = no λ() + bool ⊓? (_ -× _) = no λ() + unknown ⊓? num = yes ⟨ num , TJUnknownBase TBNum ⟩ + unknown ⊓? bool = yes ⟨ bool , TJUnknownBase TBBool ⟩ + unknown ⊓? unknown = yes ⟨ unknown , TJUnknown ⟩ + unknown ⊓? (τ₁ -→ τ₂) = yes ⟨ τ₁ -→ τ₂ , TJUnknownArr ⟩ + unknown ⊓? (τ₁ -× τ₂) = yes ⟨ τ₁ -× τ₂ , TJUnknownProd ⟩ + (τ₁ -→ τ₂) ⊓? num = no λ() + (τ₁ -→ τ₂) ⊓? bool = no λ() + (τ₁ -→ τ₂) ⊓? unknown = yes ⟨ τ₁ -→ τ₂ , TJArrUnknown ⟩ + (τ₁ -→ τ₂) ⊓? (τ₁′ -→ τ₂′) + with τ₁ ⊓? τ₁′ | τ₂ ⊓? τ₂′ + ... | yes ⟨ τ , τ₁⊓τ₁′ ⟩ | yes ⟨ τ′ , τ₂⊓τ₂′′ ⟩ = yes ⟨ τ -→ τ′ , TJArr τ₁⊓τ₁′ τ₂⊓τ₂′′ ⟩ + ... | _ | no ¬τ₂⊓τ₂′ = no λ { ⟨ .(_ -→ _) , TJArr {τ₂″ = τ₂″} τ₁⊓τ₁′″ τ₂⊓τ₂′″ ⟩ → ¬τ₂⊓τ₂′ ⟨ τ₂″ , τ₂⊓τ₂′″ ⟩ } + ... | no ¬τ₁⊓τ₁′ | _ = no λ { ⟨ .(_ -→ _) , TJArr {τ₁″ = τ₁″} τ₁⊓τ₁′″ τ₂⊓τ₂′″ ⟩ → ¬τ₁⊓τ₁′ ⟨ τ₁″ , τ₁⊓τ₁′″ ⟩ } + (τ₁ -→ τ₂) ⊓? (τ₁′ -× τ₂′) = no λ() + (τ₁ -× τ₂) ⊓? num = no λ() + (τ₁ -× τ₂) ⊓? bool = no λ() + (τ₁ -× τ₂) ⊓? unknown = yes ⟨ τ₁ -× τ₂ , TJProdUnknown ⟩ + (τ₁ -× τ₂) ⊓? (τ₁′ -→ τ₂′) = no λ() + (τ₁ -× τ₂) ⊓? (τ₁′ -× τ₂′) + with τ₁ ⊓? τ₁′ | τ₂ ⊓? τ₂′ + ... | yes ⟨ τ , τ₁⊓τ₁′ ⟩ | yes ⟨ τ′ , τ₂⊓τ₂′′ ⟩ = yes ⟨ τ -× τ′ , TJProd τ₁⊓τ₁′ τ₂⊓τ₂′′ ⟩ + ... | _ | no ¬τ₂⊓τ₂′ = no λ { ⟨ .(_ -× _) , TJProd {τ₂″ = τ₂″} τ₁⊓τ₁′″ τ₂⊓τ₂′″ ⟩ → ¬τ₂⊓τ₂′ ⟨ τ₂″ , τ₂⊓τ₂′″ ⟩ } + ... | no ¬τ₁⊓τ₁′ | _ = no λ { ⟨ .(_ -× _) , TJProd {τ₁″ = τ₁″} τ₁⊓τ₁′″ τ₂⊓τ₂′″ ⟩ → ¬τ₁⊓τ₁′ ⟨ τ₁″ , τ₁⊓τ₁′″ ⟩ } -- meet of same type - ⊔-refl : ∀ {τ} → τ ⊔ τ ⇒ τ - ⊔-refl {num} = TJBase TBNum - ⊔-refl {bool} = TJBase TBBool - ⊔-refl {unknown} = TJUnknown - ⊔-refl {τ₁ -→ τ₂} - with τ₁⊔τ₁ ← ⊔-refl {τ₁} - | τ₂⊔τ₂ ← ⊔-refl {τ₂} - = TJArr τ₁⊔τ₁ τ₂⊔τ₂ - ⊔-refl {τ₁ -× τ₂} - with τ₁⊔τ₁ ← ⊔-refl {τ₁} - | τ₂⊔τ₂ ← ⊔-refl {τ₂} - = TJProd τ₁⊔τ₁ τ₂⊔τ₂ + ⊓-refl : ∀ {τ} → τ ⊓ τ ⇒ τ + ⊓-refl {num} = TJBase TBNum + ⊓-refl {bool} = TJBase TBBool + ⊓-refl {unknown} = TJUnknown + ⊓-refl {τ₁ -→ τ₂} + with τ₁⊓τ₁ ← ⊓-refl {τ₁} + | τ₂⊓τ₂ ← ⊓-refl {τ₂} + = TJArr τ₁⊓τ₁ τ₂⊓τ₂ + ⊓-refl {τ₁ -× τ₂} + with τ₁⊓τ₁ ← ⊓-refl {τ₁} + | τ₂⊓τ₂ ← ⊓-refl {τ₂} + = TJProd τ₁⊓τ₁ τ₂⊓τ₂ -- meet is symmetric - ⊔-sym : ∀ {τ₁ τ₂ τ} → τ₁ ⊔ τ₂ ⇒ τ → τ₂ ⊔ τ₁ ⇒ τ - ⊔-sym (TJBase b) = TJBase b - ⊔-sym TJUnknown = TJUnknown - ⊔-sym (TJUnknownBase b) = TJBaseUnknown b - ⊔-sym (TJBaseUnknown b) = TJUnknownBase b - ⊔-sym TJUnknownArr = TJArrUnknown - ⊔-sym TJArrUnknown = TJUnknownArr - ⊔-sym (TJArr ⊔⇒τ₁″ ⊔⇒τ₂″) = TJArr (⊔-sym ⊔⇒τ₁″) (⊔-sym ⊔⇒τ₂″) - ⊔-sym TJUnknownProd = TJProdUnknown - ⊔-sym TJProdUnknown = TJUnknownProd - ⊔-sym (TJProd ⊔⇒τ₁″ ⊔⇒τ₂″) = TJProd (⊔-sym ⊔⇒τ₁″) (⊔-sym ⊔⇒τ₂″) + ⊓-sym : ∀ {τ₁ τ₂ τ} → τ₁ ⊓ τ₂ ⇒ τ → τ₂ ⊓ τ₁ ⇒ τ + ⊓-sym (TJBase b) = TJBase b + ⊓-sym TJUnknown = TJUnknown + ⊓-sym (TJUnknownBase b) = TJBaseUnknown b + ⊓-sym (TJBaseUnknown b) = TJUnknownBase b + ⊓-sym TJUnknownArr = TJArrUnknown + ⊓-sym TJArrUnknown = TJUnknownArr + ⊓-sym (TJArr ⊓⇒τ₁″ ⊓⇒τ₂″) = TJArr (⊓-sym ⊓⇒τ₁″) (⊓-sym ⊓⇒τ₂″) + ⊓-sym TJUnknownProd = TJProdUnknown + ⊓-sym TJProdUnknown = TJUnknownProd + ⊓-sym (TJProd ⊓⇒τ₁″ ⊓⇒τ₂″) = TJProd (⊓-sym ⊓⇒τ₁″) (⊓-sym ⊓⇒τ₂″) -- meet with unknown - ⊔-unknown₁ : ∀ {τ} → unknown ⊔ τ ⇒ τ - ⊔-unknown₁ {num} = TJUnknownBase TBNum - ⊔-unknown₁ {bool} = TJUnknownBase TBBool - ⊔-unknown₁ {unknown} = TJUnknown - ⊔-unknown₁ {_ -→ _} = TJUnknownArr - ⊔-unknown₁ {_ -× _} = TJUnknownProd - - ⊔-unknown₂ : ∀ {τ} → τ ⊔ unknown ⇒ τ - ⊔-unknown₂ {num} = TJBaseUnknown TBNum - ⊔-unknown₂ {bool} = TJBaseUnknown TBBool - ⊔-unknown₂ {unknown} = TJUnknown - ⊔-unknown₂ {_ -→ _} = TJArrUnknown - ⊔-unknown₂ {_ -× _} = TJProdUnknown + ⊓-unknown₁ : ∀ {τ} → unknown ⊓ τ ⇒ τ + ⊓-unknown₁ {num} = TJUnknownBase TBNum + ⊓-unknown₁ {bool} = TJUnknownBase TBBool + ⊓-unknown₁ {unknown} = TJUnknown + ⊓-unknown₁ {_ -→ _} = TJUnknownArr + ⊓-unknown₁ {_ -× _} = TJUnknownProd + + ⊓-unknown₂ : ∀ {τ} → τ ⊓ unknown ⇒ τ + ⊓-unknown₂ {num} = TJBaseUnknown TBNum + ⊓-unknown₂ {bool} = TJBaseUnknown TBBool + ⊓-unknown₂ {unknown} = TJUnknown + ⊓-unknown₂ {_ -→ _} = TJArrUnknown + ⊓-unknown₂ {_ -× _} = TJProdUnknown -- meet unicity - ⊔-unicity : ∀ {τ₁ τ₂ τ τ′} → τ₁ ⊔ τ₂ ⇒ τ → τ₁ ⊔ τ₂ ⇒ τ′ → τ ≡ τ′ - ⊔-unicity (TJBase _) (TJBase _) = refl - ⊔-unicity TJUnknown TJUnknown = refl - ⊔-unicity (TJUnknownBase _) (TJUnknownBase _) = refl - ⊔-unicity (TJBaseUnknown _) (TJBaseUnknown _) = refl - ⊔-unicity TJUnknownArr TJUnknownArr = refl - ⊔-unicity TJArrUnknown TJArrUnknown = refl - ⊔-unicity (TJArr _ _) (TJBase ()) - ⊔-unicity (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) (TJArr τ₁⊔τ₁′′ τ₂⊔τ₂′′) = -→-≡ (⊔-unicity τ₁⊔τ₁′ τ₁⊔τ₁′′) (⊔-unicity τ₂⊔τ₂′ τ₂⊔τ₂′′) - ⊔-unicity TJUnknownProd TJUnknownProd = refl - ⊔-unicity TJProdUnknown TJProdUnknown = refl - ⊔-unicity (TJProd _ _) (TJBase ()) - ⊔-unicity (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) (TJProd τ₁⊔τ₁′′ τ₂⊔τ₂′′) = -×-≡ (⊔-unicity τ₁⊔τ₁′ τ₁⊔τ₁′′) (⊔-unicity τ₂⊔τ₂′ τ₂⊔τ₂′′) + ⊓-unicity : ∀ {τ₁ τ₂ τ τ′} → τ₁ ⊓ τ₂ ⇒ τ → τ₁ ⊓ τ₂ ⇒ τ′ → τ ≡ τ′ + ⊓-unicity (TJBase _) (TJBase _) = refl + ⊓-unicity TJUnknown TJUnknown = refl + ⊓-unicity (TJUnknownBase _) (TJUnknownBase _) = refl + ⊓-unicity (TJBaseUnknown _) (TJBaseUnknown _) = refl + ⊓-unicity TJUnknownArr TJUnknownArr = refl + ⊓-unicity TJArrUnknown TJArrUnknown = refl + ⊓-unicity (TJArr _ _) (TJBase ()) + ⊓-unicity (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) (TJArr τ₁⊓τ₁′′ τ₂⊓τ₂′′) = -→-≡ (⊓-unicity τ₁⊓τ₁′ τ₁⊓τ₁′′) (⊓-unicity τ₂⊓τ₂′ τ₂⊓τ₂′′) + ⊓-unicity TJUnknownProd TJUnknownProd = refl + ⊓-unicity TJProdUnknown TJProdUnknown = refl + ⊓-unicity (TJProd _ _) (TJBase ()) + ⊓-unicity (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) (TJProd τ₁⊓τ₁′′ τ₂⊓τ₂′′) = -×-≡ (⊓-unicity τ₁⊓τ₁′ τ₁⊓τ₁′′) (⊓-unicity τ₂⊓τ₂′ τ₂⊓τ₂′′) -- meet derivation equality - ⊔-≡ : ∀ {τ₁ τ₂ τ} → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) → (τ₁⊔τ₂′ : τ₁ ⊔ τ₂ ⇒ τ) → τ₁⊔τ₂ ≡ τ₁⊔τ₂′ - ⊔-≡ (TJBase b) (TJBase b′) + ⊓-≡ : ∀ {τ₁ τ₂ τ} → (τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ) → (τ₁⊓τ₂′ : τ₁ ⊓ τ₂ ⇒ τ) → τ₁⊓τ₂ ≡ τ₁⊓τ₂′ + ⊓-≡ (TJBase b) (TJBase b′) rewrite base-≡ b b′ = refl - ⊔-≡ TJUnknown TJUnknown = refl - ⊔-≡ (TJUnknownBase b) (TJUnknownBase b′) + ⊓-≡ TJUnknown TJUnknown = refl + ⊓-≡ (TJUnknownBase b) (TJUnknownBase b′) rewrite base-≡ b b′ = refl - ⊔-≡ (TJBaseUnknown b) (TJBaseUnknown b′) + ⊓-≡ (TJBaseUnknown b) (TJBaseUnknown b′) rewrite base-≡ b b′ = refl - ⊔-≡ (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) (TJArr τ₁⊔τ₁′′ τ₂⊔τ₂′′) - rewrite ⊔-≡ τ₁⊔τ₁′ τ₁⊔τ₁′′ - | ⊔-≡ τ₂⊔τ₂′ τ₂⊔τ₂′′ = refl - ⊔-≡ TJUnknownArr TJUnknownArr = refl - ⊔-≡ TJArrUnknown TJArrUnknown = refl - ⊔-≡ (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) (TJProd τ₁⊔τ₁′′ τ₂⊔τ₂′′) - rewrite ⊔-≡ τ₁⊔τ₁′ τ₁⊔τ₁′′ - | ⊔-≡ τ₂⊔τ₂′ τ₂⊔τ₂′′ = refl - ⊔-≡ TJUnknownProd TJUnknownProd = refl - ⊔-≡ TJProdUnknown TJProdUnknown = refl + ⊓-≡ (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) (TJArr τ₁⊓τ₁′′ τ₂⊓τ₂′′) + rewrite ⊓-≡ τ₁⊓τ₁′ τ₁⊓τ₁′′ + | ⊓-≡ τ₂⊓τ₂′ τ₂⊓τ₂′′ = refl + ⊓-≡ TJUnknownArr TJUnknownArr = refl + ⊓-≡ TJArrUnknown TJArrUnknown = refl + ⊓-≡ (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) (TJProd τ₁⊓τ₁′′ τ₂⊓τ₂′′) + rewrite ⊓-≡ τ₁⊓τ₁′ τ₁⊓τ₁′′ + | ⊓-≡ τ₂⊓τ₂′ τ₂⊓τ₂′′ = refl + ⊓-≡ TJUnknownProd TJUnknownProd = refl + ⊓-≡ TJProdUnknown TJProdUnknown = refl -- meet existence means that types are consistent - ⊔→~ : ∀ {τ τ₁ τ₂} → τ₁ ⊔ τ₂ ⇒ τ → τ₁ ~ τ₂ - ⊔→~ (TJBase b) = TCBase b - ⊔→~ TJUnknown = TCUnknown - ⊔→~ (TJUnknownBase b) = TCUnknownBase b - ⊔→~ (TJBaseUnknown b) = TCBaseUnknown b - ⊔→~ TJUnknownArr = TCUnknownArr - ⊔→~ TJArrUnknown = TCArrUnknown - ⊔→~ (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) = TCArr (⊔→~ τ₁⊔τ₁′) (⊔→~ τ₂⊔τ₂′) - ⊔→~ TJUnknownProd = TCUnknownProd - ⊔→~ TJProdUnknown = TCProdUnknown - ⊔→~ (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) = TCProd (⊔→~ τ₁⊔τ₁′) (⊔→~ τ₂⊔τ₂′) + ⊓→~ : ∀ {τ τ₁ τ₂} → τ₁ ⊓ τ₂ ⇒ τ → τ₁ ~ τ₂ + ⊓→~ (TJBase b) = TCBase b + ⊓→~ TJUnknown = TCUnknown + ⊓→~ (TJUnknownBase b) = TCUnknownBase b + ⊓→~ (TJBaseUnknown b) = TCBaseUnknown b + ⊓→~ TJUnknownArr = TCUnknownArr + ⊓→~ TJArrUnknown = TCArrUnknown + ⊓→~ (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) = TCArr (⊓→~ τ₁⊓τ₁′) (⊓→~ τ₂⊓τ₂′) + ⊓→~ TJUnknownProd = TCUnknownProd + ⊓→~ TJProdUnknown = TCProdUnknown + ⊓→~ (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) = TCProd (⊓→~ τ₁⊓τ₁′) (⊓→~ τ₂⊓τ₂′) -- consistent types have a meet - ~→⊔ : ∀ {τ₁ τ₂} → τ₁ ~ τ₂ → ∃[ τ ] τ₁ ⊔ τ₂ ⇒ τ - ~→⊔ TCUnknown = ⟨ unknown , TJUnknown ⟩ - ~→⊔ {τ₁ = τ } (TCBase b) = ⟨ τ , TJBase b ⟩ - ~→⊔ {τ₂ = τ₂} (TCUnknownBase b) = ⟨ τ₂ , TJUnknownBase b ⟩ - ~→⊔ {τ₁ = τ₁} (TCBaseUnknown b) = ⟨ τ₁ , TJBaseUnknown b ⟩ - ~→⊔ {τ₂ = τ₂} TCUnknownArr = ⟨ τ₂ , TJUnknownArr ⟩ - ~→⊔ {τ₁ = τ₁} TCArrUnknown = ⟨ τ₁ , TJArrUnknown ⟩ - ~→⊔ (TCArr τ₁~τ₁′ τ₂~τ₂′) - with ⟨ τ₁″ , ⊔⇒τ₁″ ⟩ ← ~→⊔ τ₁~τ₁′ - | ⟨ τ₂″ , ⊔⇒τ₂″ ⟩ ← ~→⊔ τ₂~τ₂′ - = ⟨ τ₁″ -→ τ₂″ , TJArr ⊔⇒τ₁″ ⊔⇒τ₂″ ⟩ - ~→⊔ {τ₂ = τ₂} TCUnknownProd = ⟨ τ₂ , TJUnknownProd ⟩ - ~→⊔ {τ₁ = τ₁} TCProdUnknown = ⟨ τ₁ , TJProdUnknown ⟩ - ~→⊔ (TCProd τ₁~τ₁′ τ₂~τ₂′) - with ⟨ τ₁″ , ⊔⇒τ₁″ ⟩ ← ~→⊔ τ₁~τ₁′ - | ⟨ τ₂″ , ⊔⇒τ₂″ ⟩ ← ~→⊔ τ₂~τ₂′ - = ⟨ τ₁″ -× τ₂″ , TJProd ⊔⇒τ₁″ ⊔⇒τ₂″ ⟩ + ~→⊓ : ∀ {τ₁ τ₂} → τ₁ ~ τ₂ → ∃[ τ ] τ₁ ⊓ τ₂ ⇒ τ + ~→⊓ TCUnknown = ⟨ unknown , TJUnknown ⟩ + ~→⊓ {τ₁ = τ } (TCBase b) = ⟨ τ , TJBase b ⟩ + ~→⊓ {τ₂ = τ₂} (TCUnknownBase b) = ⟨ τ₂ , TJUnknownBase b ⟩ + ~→⊓ {τ₁ = τ₁} (TCBaseUnknown b) = ⟨ τ₁ , TJBaseUnknown b ⟩ + ~→⊓ {τ₂ = τ₂} TCUnknownArr = ⟨ τ₂ , TJUnknownArr ⟩ + ~→⊓ {τ₁ = τ₁} TCArrUnknown = ⟨ τ₁ , TJArrUnknown ⟩ + ~→⊓ (TCArr τ₁~τ₁′ τ₂~τ₂′) + with ⟨ τ₁″ , ⊓⇒τ₁″ ⟩ ← ~→⊓ τ₁~τ₁′ + | ⟨ τ₂″ , ⊓⇒τ₂″ ⟩ ← ~→⊓ τ₂~τ₂′ + = ⟨ τ₁″ -→ τ₂″ , TJArr ⊓⇒τ₁″ ⊓⇒τ₂″ ⟩ + ~→⊓ {τ₂ = τ₂} TCUnknownProd = ⟨ τ₂ , TJUnknownProd ⟩ + ~→⊓ {τ₁ = τ₁} TCProdUnknown = ⟨ τ₁ , TJProdUnknown ⟩ + ~→⊓ (TCProd τ₁~τ₁′ τ₂~τ₂′) + with ⟨ τ₁″ , ⊓⇒τ₁″ ⟩ ← ~→⊓ τ₁~τ₁′ + | ⟨ τ₂″ , ⊓⇒τ₂″ ⟩ ← ~→⊓ τ₂~τ₂′ + = ⟨ τ₁″ -× τ₂″ , TJProd ⊓⇒τ₁″ ⊓⇒τ₂″ ⟩ -- meet nonexistence means types are inconsistent - ¬⊔→~̸ : ∀ {τ₁ τ₂} → ¬ (∃[ τ ] τ₁ ⊔ τ₂ ⇒ τ) → τ₁ ~̸ τ₂ - ¬⊔→~̸ ¬τ₁⊔τ₂ = λ { τ₁~τ₂ → ¬τ₁⊔τ₂ (~→⊔ τ₁~τ₂) } + ¬⊓→~̸ : ∀ {τ₁ τ₂} → ¬ (∃[ τ ] τ₁ ⊓ τ₂ ⇒ τ) → τ₁ ~̸ τ₂ + ¬⊓→~̸ ¬τ₁⊓τ₂ = λ { τ₁~τ₂ → ¬τ₁⊓τ₂ (~→⊓ τ₁~τ₂) } -- inconsistent types have no meet - ~̸→¬⊔ : ∀ {τ₁ τ₂} → τ₁ ~̸ τ₂ → ¬ (∃[ τ ] τ₁ ⊔ τ₂ ⇒ τ) - ~̸→¬⊔ τ₁~̸τ₂ = λ { ⟨ τ , τ₁⊔τ₂ ⟩ → τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂) } + ~̸→¬⊓ : ∀ {τ₁ τ₂} → τ₁ ~̸ τ₂ → ¬ (∃[ τ ] τ₁ ⊓ τ₂ ⇒ τ) + ~̸→¬⊓ τ₁~̸τ₂ = λ { ⟨ τ , τ₁⊓τ₂ ⟩ → τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂) } -- types are consistent with their meet - ⊔⇒→~ : ∀ {τ₁ τ₂ τ} → τ₁ ⊔ τ₂ ⇒ τ → τ₁ ~ τ × τ₂ ~ τ - ⊔⇒→~ (TJBase b) = ⟨ TCBase b , TCBase b ⟩ - ⊔⇒→~ TJUnknown = ⟨ TCUnknown , TCUnknown ⟩ - ⊔⇒→~ (TJUnknownBase b) = ⟨ TCUnknownBase b , TCBase b ⟩ - ⊔⇒→~ (TJBaseUnknown b) = ⟨ TCBase b , TCUnknownBase b ⟩ - ⊔⇒→~ (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) - with ⟨ τ₁~ , τ₁′~ ⟩ ← ⊔⇒→~ τ₁⊔τ₁′ - | ⟨ τ₂~ , τ₂′~ ⟩ ← ⊔⇒→~ τ₂⊔τ₂′ + ⊓⇒→~ : ∀ {τ₁ τ₂ τ} → τ₁ ⊓ τ₂ ⇒ τ → τ₁ ~ τ × τ₂ ~ τ + ⊓⇒→~ (TJBase b) = ⟨ TCBase b , TCBase b ⟩ + ⊓⇒→~ TJUnknown = ⟨ TCUnknown , TCUnknown ⟩ + ⊓⇒→~ (TJUnknownBase b) = ⟨ TCUnknownBase b , TCBase b ⟩ + ⊓⇒→~ (TJBaseUnknown b) = ⟨ TCBase b , TCUnknownBase b ⟩ + ⊓⇒→~ (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) + with ⟨ τ₁~ , τ₁′~ ⟩ ← ⊓⇒→~ τ₁⊓τ₁′ + | ⟨ τ₂~ , τ₂′~ ⟩ ← ⊓⇒→~ τ₂⊓τ₂′ = ⟨ TCArr τ₁~ τ₂~ , TCArr τ₁′~ τ₂′~ ⟩ - ⊔⇒→~ TJUnknownArr = ⟨ TCUnknownArr , TCArr ~-refl ~-refl ⟩ - ⊔⇒→~ TJArrUnknown = ⟨ TCArr ~-refl ~-refl , TCUnknownArr ⟩ - ⊔⇒→~ (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) - with ⟨ τ₁~ , τ₁′~ ⟩ ← ⊔⇒→~ τ₁⊔τ₁′ - | ⟨ τ₂~ , τ₂′~ ⟩ ← ⊔⇒→~ τ₂⊔τ₂′ + ⊓⇒→~ TJUnknownArr = ⟨ TCUnknownArr , TCArr ~-refl ~-refl ⟩ + ⊓⇒→~ TJArrUnknown = ⟨ TCArr ~-refl ~-refl , TCUnknownArr ⟩ + ⊓⇒→~ (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) + with ⟨ τ₁~ , τ₁′~ ⟩ ← ⊓⇒→~ τ₁⊓τ₁′ + | ⟨ τ₂~ , τ₂′~ ⟩ ← ⊓⇒→~ τ₂⊓τ₂′ = ⟨ TCProd τ₁~ τ₂~ , TCProd τ₁′~ τ₂′~ ⟩ - ⊔⇒→~ TJUnknownProd = ⟨ TCUnknownProd , TCProd ~-refl ~-refl ⟩ - ⊔⇒→~ TJProdUnknown = ⟨ TCProd ~-refl ~-refl , TCUnknownProd ⟩ + ⊓⇒→~ TJUnknownProd = ⟨ TCUnknownProd , TCProd ~-refl ~-refl ⟩ + ⊓⇒→~ TJProdUnknown = ⟨ TCProd ~-refl ~-refl , TCUnknownProd ⟩ -- types are consistent with types consistent to their meet - ⊔⇒-~→~ : ∀ {τ₁ τ₂ τ τ′} → τ₁ ⊔ τ₂ ⇒ τ → τ ~ τ′ → τ₁ ~ τ′ × τ₂ ~ τ′ - ⊔⇒-~→~ (TJBase b) τ~τ′ = ⟨ τ~τ′ , τ~τ′ ⟩ - ⊔⇒-~→~ TJUnknown τ~τ′ = ⟨ τ~τ′ , τ~τ′ ⟩ - ⊔⇒-~→~ (TJUnknownBase b) τ~τ′ = ⟨ ~-unknown₁ , τ~τ′ ⟩ - ⊔⇒-~→~ (TJBaseUnknown b) τ~τ′ = ⟨ τ~τ′ , ~-unknown₁ ⟩ - ⊔⇒-~→~ {τ = .(_ -→ _)} {unknown} (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) τ~τ′ + ⊓⇒-~→~ : ∀ {τ₁ τ₂ τ τ′} → τ₁ ⊓ τ₂ ⇒ τ → τ ~ τ′ → τ₁ ~ τ′ × τ₂ ~ τ′ + ⊓⇒-~→~ (TJBase b) τ~τ′ = ⟨ τ~τ′ , τ~τ′ ⟩ + ⊓⇒-~→~ TJUnknown τ~τ′ = ⟨ τ~τ′ , τ~τ′ ⟩ + ⊓⇒-~→~ (TJUnknownBase b) τ~τ′ = ⟨ ~-unknown₁ , τ~τ′ ⟩ + ⊓⇒-~→~ (TJBaseUnknown b) τ~τ′ = ⟨ τ~τ′ , ~-unknown₁ ⟩ + ⊓⇒-~→~ {τ = .(_ -→ _)} {unknown} (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) τ~τ′ = ⟨ TCArrUnknown , TCArrUnknown ⟩ - ⊔⇒-~→~ {τ = .(_ -→ _)} {τ₁″ -→ τ₂″} (TJArr τ₁⊔τ₁′ τ₂⊔τ₂′) (TCArr τ₁″~τ₁‴ τ₂″~τ₂‴) - with ⟨ τ₁~τ₁″ , τ₁′~τ₁″ ⟩ ← ⊔⇒-~→~ τ₁⊔τ₁′ τ₁″~τ₁‴ - with ⟨ τ₂~τ₂″ , τ₂′~τ₂″ ⟩ ← ⊔⇒-~→~ τ₂⊔τ₂′ τ₂″~τ₂‴ + ⊓⇒-~→~ {τ = .(_ -→ _)} {τ₁″ -→ τ₂″} (TJArr τ₁⊓τ₁′ τ₂⊓τ₂′) (TCArr τ₁″~τ₁‴ τ₂″~τ₂‴) + with ⟨ τ₁~τ₁″ , τ₁′~τ₁″ ⟩ ← ⊓⇒-~→~ τ₁⊓τ₁′ τ₁″~τ₁‴ + with ⟨ τ₂~τ₂″ , τ₂′~τ₂″ ⟩ ← ⊓⇒-~→~ τ₂⊓τ₂′ τ₂″~τ₂‴ = ⟨ TCArr τ₁~τ₁″ τ₂~τ₂″ , TCArr τ₁′~τ₁″ τ₂′~τ₂″ ⟩ - ⊔⇒-~→~ {τ = .(_ -→ _)} TJUnknownArr τ~τ′ + ⊓⇒-~→~ {τ = .(_ -→ _)} TJUnknownArr τ~τ′ = ⟨ ~-unknown₁ , τ~τ′ ⟩ - ⊔⇒-~→~ {τ = .(_ -→ _)} TJArrUnknown τ~τ′ + ⊓⇒-~→~ {τ = .(_ -→ _)} TJArrUnknown τ~τ′ = ⟨ τ~τ′ , ~-unknown₁ ⟩ - ⊔⇒-~→~ {τ = .(_ -× _)} {unknown} (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) τ~τ′ + ⊓⇒-~→~ {τ = .(_ -× _)} {unknown} (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) τ~τ′ = ⟨ TCProdUnknown , TCProdUnknown ⟩ - ⊔⇒-~→~ {τ = .(_ -× _)} {τ′} (TJProd τ₁⊔τ₁′ τ₂⊔τ₂′) (TCProd τ₁″~τ₁‴ τ₂″~τ₂‴) - with ⟨ τ₁~τ₁″ , τ₁′~τ₁″ ⟩ ← ⊔⇒-~→~ τ₁⊔τ₁′ τ₁″~τ₁‴ - with ⟨ τ₂~τ₂″ , τ₂′~τ₂″ ⟩ ← ⊔⇒-~→~ τ₂⊔τ₂′ τ₂″~τ₂‴ + ⊓⇒-~→~ {τ = .(_ -× _)} {τ′} (TJProd τ₁⊓τ₁′ τ₂⊓τ₂′) (TCProd τ₁″~τ₁‴ τ₂″~τ₂‴) + with ⟨ τ₁~τ₁″ , τ₁′~τ₁″ ⟩ ← ⊓⇒-~→~ τ₁⊓τ₁′ τ₁″~τ₁‴ + with ⟨ τ₂~τ₂″ , τ₂′~τ₂″ ⟩ ← ⊓⇒-~→~ τ₂⊓τ₂′ τ₂″~τ₂‴ = ⟨ TCProd τ₁~τ₁″ τ₂~τ₂″ , TCProd τ₁′~τ₁″ τ₂′~τ₂″ ⟩ - ⊔⇒-~→~ {τ = .(_ -× _)} TJUnknownProd τ~τ′ + ⊓⇒-~→~ {τ = .(_ -× _)} TJUnknownProd τ~τ′ = ⟨ ~-unknown₁ , τ~τ′ ⟩ - ⊔⇒-~→~ {τ = .(_ -× _)} TJProdUnknown τ~τ′ + ⊓⇒-~→~ {τ = .(_ -× _)} TJProdUnknown τ~τ′ = ⟨ τ~τ′ , ~-unknown₁ ⟩ open equality public diff --git a/core/uexp.agda b/core/uexp.agda index 791ba81..c784f7f 100644 --- a/core/uexp.agda +++ b/core/uexp.agda @@ -96,7 +96,7 @@ module core.uexp where → (e₁⇐bool : Γ ⊢ e₁ ⇐ bool) → (e₂⇒τ₁ : Γ ⊢ e₂ ⇒ τ₁) → (e₃⇒τ₂ : Γ ⊢ e₃ ⇒ τ₂) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) + → (τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ) → Γ ⊢ ‵ e₁ ∙ e₂ ∙ e₃ ⇒ τ USPair : ∀ {Γ e₁ e₂ τ₁ τ₂} diff --git a/marking/marking.agda b/marking/marking.agda index a980598..d7c89d6 100644 --- a/marking/marking.agda +++ b/marking/marking.agda @@ -71,8 +71,8 @@ module marking.marking where → (e₁↬⇐ě₁ : Γ ⊢ e₁ ↬⇐ ě₁) → (e₂↬⇐ě₂ : Γ ⊢ e₂ ↬⇒ ě₂) → (e₃↬⇐ě₃ : Γ ⊢ e₃ ↬⇒ ě₃) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) - → Γ ⊢ ‵ e₁ ∙ e₂ ∙ e₃ ↬⇒ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + → (τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ) + → Γ ⊢ ‵ e₁ ∙ e₂ ∙ e₃ ↬⇒ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ] MKSInconsistentBranches : ∀ {Γ e₁ e₂ e₃ τ₁ τ₂} → {ě₁ : Γ ⊢⇐ bool} diff --git a/marking/totality.agda b/marking/totality.agda index e03f92c..22695eb 100644 --- a/marking/totality.agda +++ b/marking/totality.agda @@ -44,8 +44,8 @@ module marking.totality where | ⟨ τ₂ , ⟨ ě₃ , e₃↬⇒ě₃ ⟩ ⟩ ← ↬⇒-totality Γ e₃ with τ₁ ~? τ₂ ... | yes τ₁~τ₂ - with ⟨ τ , ⊔⇒τ ⟩ ← ~→⊔ τ₁~τ₂ - = ⟨ τ , ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ ⊔⇒τ ] , MKSIf e₁↬⇐ě₁ e₂↬⇐ě₂ e₃↬⇒ě₃ ⊔⇒τ ⟩ ⟩ + with ⟨ τ , ⊓⇒τ ⟩ ← ~→⊓ τ₁~τ₂ + = ⟨ τ , ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ ⊓⇒τ ] , MKSIf e₁↬⇐ě₁ e₂↬⇐ě₂ e₃↬⇒ě₃ ⊓⇒τ ⟩ ⟩ ... | no τ₁~̸τ₂ = ⟨ unknown , ⟨ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] , MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇐ě₂ e₃↬⇒ě₃ τ₁~̸τ₂ ⟩ ⟩ ↬⇒-totality Γ ‵⟨ e₁ , e₂ ⟩ with ⟨ τ₁ , ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ⟩ ← ↬⇒-totality Γ e₁ diff --git a/marking/unicity.agda b/marking/unicity.agda index 5d72eb2..f61d592 100644 --- a/marking/unicity.agda +++ b/marking/unicity.agda @@ -29,15 +29,15 @@ module marking.unicity where ↬⇒-τ-unicity (MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂) (MKSPlus e₁↬⇐ě₁′ e₂↬⇐ě₂′) = refl ↬⇒-τ-unicity MKSTrue MKSTrue = refl ↬⇒-τ-unicity MKSFalse MKSFalse = refl - ↬⇒-τ-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊔τ₂′) + ↬⇒-τ-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊓τ₂′) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ - | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊔-unicity τ₁⊔τ₂ τ₁⊔τ₂′ - ↬⇒-τ-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂) + | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊓-unicity τ₁⊓τ₂ τ₁⊓τ₂′ + ↬⇒-τ-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ - | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) - ↬⇒-τ-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊔τ₂) + | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) + ↬⇒-τ-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊓τ₂) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ - | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) + | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) ↬⇒-τ-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂′) = refl ↬⇒-τ-unicity (MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂) (MKSPair e₁↬⇒ě₁′ e₂↬⇒ě₂′) rewrite ↬⇒-τ-unicity e₁↬⇒ě₁ e₁↬⇒ě₁′ @@ -97,19 +97,19 @@ module marking.unicity where | ↬⇐-ě-unicity e₂↬⇐ě₂ e₂↬⇐ě₂′ = refl ↬⇒-ě-unicity MKSTrue MKSTrue = refl ↬⇒-ě-unicity MKSFalse MKSFalse = refl - ↬⇒-ě-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊔τ₂′) + ↬⇒-ě-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊓τ₂′) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ rewrite ↬⇐-ě-unicity e₁↬⇐ě₁ e₁↬⇐ě₁′ | ↬⇒-ě-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ | ↬⇒-ě-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ - | ⊔-≡ τ₁⊔τ₂ τ₁⊔τ₂′ = refl - ↬⇒-ě-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂) + | ⊓-≡ τ₁⊓τ₂ τ₁⊓τ₂′ = refl + ↬⇒-ě-unicity (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ - | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) - ↬⇒-ě-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊔τ₂) + | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) + ↬⇒-ě-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSIf e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁⊓τ₂) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ - | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) + | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) ↬⇒-ě-unicity (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) (MKSInconsistentBranches e₁↬⇐ě₁′ e₂↬⇒ě₂′ e₃↬⇒ě₃′ τ₁~̸τ₂′) with refl ← ↬⇒-τ-unicity e₂↬⇒ě₂ e₂↬⇒ě₂′ | refl ← ↬⇒-τ-unicity e₃↬⇒ě₃ e₃↬⇒ě₃′ diff --git a/marking/wellformed.agda b/marking/wellformed.agda index 705ed02..7752582 100644 --- a/marking/wellformed.agda +++ b/marking/wellformed.agda @@ -29,7 +29,7 @@ module marking.wellformed where | ↬⇐□ e₂↬⇐ě₂ = refl ↬⇒□ MKSTrue = refl ↬⇒□ MKSFalse = refl - ↬⇒□ (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) + ↬⇒□ (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) rewrite ↬⇐□ e₁↬⇐ě₁ | ↬⇒□ e₂↬⇒ě₂ | ↬⇒□ e₃↬⇒ě₃ = refl @@ -97,10 +97,10 @@ module marking.wellformed where | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐num = ⟨ ⊢ ě₁ + ě₂ , MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂ ⟩ ⇒τ→↬⇒τ {e = ‵tt} USTrue = ⟨ ⊢tt , MKSTrue ⟩ ⇒τ→↬⇒τ {e = ‵ff} USFalse = ⟨ ⊢ff , MKSFalse ⟩ - ⇒τ→↬⇒τ {e = ‵ e₁ ∙ e₂ ∙ e₃} (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) + ⇒τ→↬⇒τ {e = ‵ e₁ ∙ e₂ ∙ e₃} (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) with ⟨ ě₁ , e₁↬⇐ě₁ ⟩ ← ⇐τ→↬⇐τ e₁⇐bool | ⟨ ě₂ , e₂↬⇒ě₂ ⟩ ← ⇒τ→↬⇒τ e₂⇒τ₁ - | ⟨ ě₃ , e₃↬⇒ě₃ ⟩ ← ⇒τ→↬⇒τ e₃⇒τ₂ = ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] , MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂ ⟩ + | ⟨ ě₃ , e₃↬⇒ě₃ ⟩ ← ⇒τ→↬⇒τ e₃⇒τ₂ = ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ] , MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂ ⟩ ⇒τ→↬⇒τ {e = ‵⟨ e₁ , e₂ ⟩} (USPair e₁⇒τ₁ e₂⇒τ₂) with ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ← ⇒τ→↬⇒τ e₁⇒τ₁ | ⟨ ě₂ , e₂↬⇒ě₂ ⟩ ← ⇒τ→↬⇒τ e₂⇒τ₂ = ⟨ ⊢⟨ ě₁ , ě₂ ⟩ , MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂ ⟩ @@ -160,15 +160,15 @@ module marking.wellformed where = refl ⇒-↬-≡ USFalse MKSFalse = refl - ⇒-↬-≡ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂′) + ⇒-↬-≡ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂′) with refl ← ⇒-↬-≡ e₂⇒τ₁ e₂↬⇒ě₂ with refl ← ⇒-↬-≡ e₃⇒τ₂ e₃↬⇒ě₃ - with refl ← ⊔-unicity τ₁⊔τ₂ τ₁⊔τ₂′ + with refl ← ⊓-unicity τ₁⊓τ₂ τ₁⊓τ₂′ = refl - ⇒-↬-≡ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) + ⇒-↬-≡ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) with refl ← ⇒-↬-≡ e₂⇒τ₁ e₂↬⇒ě₂ with refl ← ⇒-↬-≡ e₃⇒τ₂ e₃↬⇒ě₃ - = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) + = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) ⇒-↬-≡ (USPair e₁⇒τ₁ e₂⇒τ₂) (MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂) with refl ← ⇒-↬-≡ e₁⇒τ₁ e₁↬⇒ě₁ with refl ← ⇒-↬-≡ e₂⇒τ₂ e₂↬⇒ě₂ @@ -221,14 +221,14 @@ module marking.wellformed where = MLSTrue ⇒τ→markless USFalse MKSFalse = MLSFalse - ⇒τ→markless (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₃) + ⇒τ→markless (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₃) with refl ← ⇒-↬-≡ e₂⇒τ₁ e₂↬⇒ě₂ with refl ← ⇒-↬-≡ e₃⇒τ₂ e₃↬⇒ě₃ = MLSIf (⇐τ→markless e₁⇐bool e₁↬⇐ě₁) (⇒τ→markless e₂⇒τ₁ e₂↬⇒ě₂) (⇒τ→markless e₃⇒τ₂ e₃↬⇒ě₃) - ⇒τ→markless (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) + ⇒τ→markless (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊓τ₂) (MKSInconsistentBranches e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁~̸τ₂) with refl ← ⇒-↬-≡ e₂⇒τ₁ e₂↬⇒ě₂ with refl ← ⇒-↬-≡ e₃⇒τ₂ e₃↬⇒ě₃ - = ⊥-elim (τ₁~̸τ₂ (⊔→~ τ₁⊔τ₂)) + = ⊥-elim (τ₁~̸τ₂ (⊓→~ τ₁⊓τ₂)) ⇒τ→markless (USPair e₁⇒τ₁ e₂⇒τ₂) (MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂) = MLSPair (⇒τ→markless e₁⇒τ₁ e₁↬⇒ě₁) (⇒τ→markless e₂⇒τ₂ e₂↬⇒ě₂) ⇒τ→markless (USProjL e⇒τ τ▸) (MKSProjL1 e↬⇒ě τ▸′) @@ -299,11 +299,11 @@ module marking.wellformed where = USPlus e₁⇐τ₁ e₂⇐τ₂ ↬⇒τ-markless→⇒τ MKSTrue MLSTrue = USTrue ↬⇒τ-markless→⇒τ MKSFalse MLSFalse = USFalse - ↬⇒τ-markless→⇒τ (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) (MLSIf less₁ less₂ less₃) + ↬⇒τ-markless→⇒τ (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊓τ₂) (MLSIf less₁ less₂ less₃) with e₁⇐τ₁ ← ↬⇐τ-markless→⇐τ e₁↬⇐ě₁ less₁ | e₂⇒τ₂ ← ↬⇒τ-markless→⇒τ e₂↬⇒ě₂ less₂ | e₃⇒τ₃ ← ↬⇒τ-markless→⇒τ e₃↬⇒ě₃ less₃ - = USIf e₁⇐τ₁ e₂⇒τ₂ e₃⇒τ₃ τ₁⊔τ₂ + = USIf e₁⇐τ₁ e₂⇒τ₂ e₃⇒τ₃ τ₁⊓τ₂ ↬⇒τ-markless→⇒τ (MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂) (MLSPair less₁ less₂) with e₁⇒τ₁ ← ↬⇒τ-markless→⇒τ e₁↬⇒ě₁ less₁ | e₂⇒τ₂ ← ↬⇒τ-markless→⇒τ e₂↬⇒ě₂ less₂