agda: Call unbound variables "free"

hazelgrove · Jul 12, 2023 · 2636fae · 2636fae
1 parent d98a845
commit 2636fae
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 16 deletions.
diff --git a/core/lemmas.agda b/core/lemmas.agda
@@ -179,5 +179,5 @@ module core.lemmas where
   ⊢⇒-⊢⇐ ě@(⊢π₁⸨ _ ⸩[ τ!▸ ]) = ⊢⇒-⊢⇐-subsume ě MSuProjL2
   ⊢⇒-⊢⇐ ě@(⊢π₂ _ [ τ▸ ]) = ⊢⇒-⊢⇐-subsume ě MSuProjR1
   ⊢⇒-⊢⇐ ě@(⊢π₂⸨ _ ⸩[ τ!▸ ]) = ⊢⇒-⊢⇐-subsume ě MSuProjR2
-  ⊢⇒-⊢⇐ ě@(⊢⟦ ∌y ⟧)                           = ⊢⇒-⊢⇐-subsume ě MSuUnbound
+  ⊢⇒-⊢⇐ ě@(⊢⟦ ∌y ⟧)                           = ⊢⇒-⊢⇐-subsume ě MSuFree
   ⊢⇒-⊢⇐ ě@(⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ])        = ⊢⇒-⊢⇐-subsume ě MSuInconsistentBranches
diff --git a/core/mexp.agda b/core/mexp.agda
@@ -78,7 +78,7 @@ module core.mexp where
         → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ)
         → Γ ⊢⇒ τ
 
-      -- MSUnbound
+      -- MSFree
       ⊢⟦_⟧ : ∀ {Γ y}
         → (∌y : Γ ∌ y)
         → Γ ⊢⇒ unknown
@@ -157,7 +157,7 @@ module core.mexp where
       MSuFalse : ∀ {Γ}
         → MSubsumable {Γ} (⊢ff)
 
-      MSuUnbound : ∀ {Γ y}
+      MSuFree : ∀ {Γ y}
         → {∌y : Γ ∌ y}
         → MSubsumable {Γ} (⊢⟦ ∌y ⟧)
 

diff --git a/marking/marking.agda b/marking/marking.agda
@@ -16,7 +16,7 @@ module marking.marking where
         → (∋x : Γ ∋ x ∶ τ)
         → Γ ⊢ ‵ x ↬⇒ ⊢ ∋x
 
-      MKSUnbound : ∀ {Γ y}
+      MKSFree : ∀ {Γ y}
         → (∌y : Γ ∌ y)
         → Γ ⊢ ‵ y ↬⇒ ⊢⟦ ∌y ⟧
 
@@ -118,7 +118,7 @@ module marking.marking where
     USu→MSu : ∀ {e : UExp} {Γ : Ctx} {τ : Typ} {ě : Γ ⊢⇒ τ} → USubsumable e → Γ ⊢ e ↬⇒ ě → MSubsumable ě
     USu→MSu {ě = ⊢⦇-⦈^ u}             USuHole  _ = MSuHole
     USu→MSu {ě = ⊢_ {x = x} ∋x}       USuVar   _ = MSuVar
-    USu→MSu {ě = ⊢⟦ x ⟧}              USuVar   _ = MSuUnbound
+    USu→MSu {ě = ⊢⟦ x ⟧}              USuVar   _ = MSuFree
     USu→MSu {ě = ⊢ ě₁ ∙ ě₂ [ τ▸ ]}    USuAp    _ = MSuAp1
     USu→MSu {ě = ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ]} USuAp    _ = MSuAp2
     USu→MSu {ě = ⊢ℕ n}                USuNum   _ = MSuNum

diff --git a/marking/totality.agda b/marking/totality.agda
@@ -13,7 +13,7 @@ module marking.totality where
       with Γ ∋?? x
     ...  | yes (Z {τ = τ})         = ⟨ τ       , ⟨ ⊢ Z           , MKSVar Z           ⟩ ⟩
     ...  | yes (S {τ = τ} x≢x′ ∋x) = ⟨ τ       , ⟨ ⊢ (S x≢x′ ∋x) , MKSVar (S x≢x′ ∋x) ⟩ ⟩
-    ...  | no  ∌x                  = ⟨ unknown , ⟨ ⊢⟦ ∌x ⟧       , MKSUnbound ∌x      ⟩ ⟩
+    ...  | no  ∌x                  = ⟨ unknown , ⟨ ⊢⟦ ∌x ⟧       , MKSFree ∌x      ⟩ ⟩
     ↬⇒-totality Γ (‵λ x ∶ τ ∙ e)
       with ⟨ τ′ , ⟨ ě , e↬⇒ě ⟩ ⟩ ← ↬⇒-totality (Γ , x ∶ τ) e
          = ⟨ τ -→ τ′ , ⟨ ⊢λ x ∶ τ ∙ ě , MKSLam e↬⇒ě ⟩ ⟩

diff --git a/marking/unicity.agda b/marking/unicity.agda
@@ -10,9 +10,9 @@ module marking.unicity where
                → τ₁ ≡ τ₂
   ↬⇒-τ-unicity           MKSHole         MKSHole          = refl
   ↬⇒-τ-unicity           (MKSVar ∋x)     (MKSVar ∋x′)     = ∋→τ-≡ ∋x ∋x′
-  ↬⇒-τ-unicity {τ₁ = τ₁} (MKSVar ∋x)     (MKSUnbound ∌x)  = ⊥-elim (∌x ⟨ τ₁ , ∋x ⟩)
-  ↬⇒-τ-unicity {τ₂ = τ₂} (MKSUnbound ∌x) (MKSVar ∋x)      = ⊥-elim (∌x ⟨ τ₂ , ∋x ⟩)
-  ↬⇒-τ-unicity           (MKSUnbound ∌x) (MKSUnbound ∌x′) = refl
+  ↬⇒-τ-unicity {τ₁ = τ₁} (MKSVar ∋x)     (MKSFree ∌x)  = ⊥-elim (∌x ⟨ τ₁ , ∋x ⟩)
+  ↬⇒-τ-unicity {τ₂ = τ₂} (MKSFree ∌x) (MKSVar ∋x)      = ⊥-elim (∌x ⟨ τ₂ , ∋x ⟩)
+  ↬⇒-τ-unicity           (MKSFree ∌x) (MKSFree ∌x′) = refl
   ↬⇒-τ-unicity (MKSLam e↬⇒ě) (MKSLam e↬⇒ě′)
     rewrite ↬⇒-τ-unicity e↬⇒ě e↬⇒ě′ = refl
   ↬⇒-τ-unicity (MKSAp1 e₁↬⇒ě₁ τ▸ e₂↬⇐ě₂) (MKSAp1 e₁↬⇒ě₁′ τ′▸ e₂↬⇐ě₂′)
@@ -65,9 +65,9 @@ module marking.unicity where
     ↬⇒-ě-unicity MKSHole MKSHole = refl
     ↬⇒-ě-unicity (MKSVar ∋x) (MKSVar ∋x′)
       rewrite ∋-≡ ∋x ∋x′ = refl
-    ↬⇒-ě-unicity (MKSVar ∋x) (MKSUnbound ∌x) = ⊥-elim (∌x ⟨ unknown , ∋x ⟩)
-    ↬⇒-ě-unicity (MKSUnbound ∌x) (MKSVar ∋x) = ⊥-elim (∌x ⟨ unknown , ∋x ⟩)
-    ↬⇒-ě-unicity (MKSUnbound ∌x) (MKSUnbound ∌x′)
+    ↬⇒-ě-unicity (MKSVar ∋x) (MKSFree ∌x) = ⊥-elim (∌x ⟨ unknown , ∋x ⟩)
+    ↬⇒-ě-unicity (MKSFree ∌x) (MKSVar ∋x) = ⊥-elim (∌x ⟨ unknown , ∋x ⟩)
+    ↬⇒-ě-unicity (MKSFree ∌x) (MKSFree ∌x′)
       rewrite assimilation ∌x ∌x′ = refl
     ↬⇒-ě-unicity (MKSLam e↬⇒ě) (MKSLam e↬⇒ě′)
       rewrite ↬⇒-ě-unicity e↬⇒ě e↬⇒ě′ = refl
@@ -155,7 +155,7 @@ module marking.unicity where
                       → USu→MSu s e↬⇒ě ≡ USu→MSu s e↬⇒ě′
     USu→MSu-unicity USuHole  MKSHole         _ = refl
     USu→MSu-unicity USuVar   (MKSVar _)      _ = refl
-    USu→MSu-unicity USuVar   (MKSUnbound _)  _ = refl
+    USu→MSu-unicity USuVar   (MKSFree _)  _ = refl
     USu→MSu-unicity USuAp    (MKSAp1 _ _ _)  _ = refl
     USu→MSu-unicity USuAp    (MKSAp2 _ _ _)  _ = refl
     USu→MSu-unicity USuNum   MKSNum          _ = refl

diff --git a/marking/wellformed.agda b/marking/wellformed.agda
@@ -11,7 +11,7 @@ module marking.wellformed where
         → ě ⇒□ ≡ e
     ↬⇒□ MKSHole           = refl
     ↬⇒□ (MKSVar ∋x)       = refl
-    ↬⇒□ (MKSUnbound ∌x)   = refl
+    ↬⇒□ (MKSFree ∌x)   = refl
     ↬⇒□ (MKSLam e↬⇒ě)
       rewrite ↬⇒□ e↬⇒ě   = refl
     ↬⇒□ (MKSAp1 e₁↬⇒ě₁ τ▸ e₂↬⇐ě₂)
@@ -134,7 +134,7 @@ module marking.wellformed where
          → τ ≡ τ′
   ⇒-↬-≡ USHole MKSHole = refl
   ⇒-↬-≡ (USVar ∋x) (MKSVar ∋x′) = ∋→τ-≡ ∋x ∋x′
-  ⇒-↬-≡ (USVar {τ = τ} ∋x) (MKSUnbound ∌y) = ⊥-elim (∌y ⟨ τ , ∋x ⟩)
+  ⇒-↬-≡ (USVar {τ = τ} ∋x) (MKSFree ∌y) = ⊥-elim (∌y ⟨ τ , ∋x ⟩)
   ⇒-↬-≡ (USLam e⇒τ) (MKSLam e↬⇒ě)
     rewrite ⇒-↬-≡ e⇒τ e↬⇒ě = refl
   ⇒-↬-≡ (USAp e⇒τ τ▸ e₁⇐τ₁) (MKSAp1 e↬⇒ě τ▸′ e₂↬⇐ě₂)
@@ -190,7 +190,7 @@ module marking.wellformed where
          = MLSHole
     ⇒τ→markless (USVar ∋x) (MKSVar ∋x′)
          = MLSVar
-    ⇒τ→markless (USVar ∋x) (MKSUnbound ∌y)
+    ⇒τ→markless (USVar ∋x) (MKSFree ∌y)
          = ⊥-elim (∌y ⟨ unknown , ∋x ⟩)
     ⇒τ→markless (USLam e⇒τ) (MKSLam e↬⇒ě)
          = MLSLam (⇒τ→markless e⇒τ e↬⇒ě)