agda: Use glub symbol for type meet

hazelgrove · Oct 27, 2023 · 2dd1f15 · 2dd1f15
1 parent cc263a2
commit 2dd1f15
Show file tree

Hide file tree

Showing 9 changed files with 218 additions and 218 deletions.
diff --git 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
@@ -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
@@ -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 : ∀ {Γ τ₁ τ₂}
         → {ě₁ : Γ ⊢⇒ τ₁}