Skip to content

Commit

Permalink
agda: Use glub symbol for type meet
Browse files Browse the repository at this point in the history
  • Loading branch information
mirryi committed Oct 27, 2023
1 parent a6db26b commit 5e413d4
Show file tree
Hide file tree
Showing 9 changed files with 218 additions and 218 deletions.
2 changes: 1 addition & 1 deletion core/erasure.agda
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module core.erasure where
(⊢ ě₁ + ě₂) ⇒□ = ‵ (ě₁ ⇐□) + (ě₂ ⇐□)
⊢tt ⇒□ = ‵tt
⊢ff ⇒□ = ‵ff
⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□)
⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□)
⊢⟦_⟧ {y = y} ∌y ⇒□ = ‵ y
⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□)
⊢⟨ ě₁ , ě₂ ⟩ ⇒□ = ‵⟨ ě₁ ⇒□ , ě₂ ⇒□ ⟩
Expand Down
16 changes: 8 additions & 8 deletions core/lemmas.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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₃⇐τ₂′
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 ⟩
⊢⇒-⊢⇐ {τ′ = τ′} ⊢⟨ ě₁ , ě₂ ⟩
Expand Down
6 changes: 3 additions & 3 deletions core/mexp.agda
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ module core.mexp where
(ě₁ : Γ ⊢⇐ bool)
(ě₂ : Γ ⊢⇒ τ₁)
(ě₃ : Γ ⊢⇒ τ₂)
(τ₁τ₂ : τ₁ τ₂ ⇒ τ)
(τ₁τ₂ : τ₁ τ₂ ⇒ τ)
Γ ⊢⇒ τ

-- MSFree
Expand Down Expand Up @@ -307,11 +307,11 @@ module core.mexp where
{ě₁ : Γ ⊢⇐ bool}
{ě₂ : Γ ⊢⇒ τ₁}
{ě₃ : Γ ⊢⇒ τ₂}
{τ₁τ₂ : τ₁ τ₂ ⇒ τ}
{τ₁τ₂ : τ₁ τ₂ ⇒ τ}
(less₁ : Markless⇐ ě₁)
(less₂ : Markless⇒ ě₂)
(less₃ : Markless⇒ ě₃)
Markless⇒ {Γ} (⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁τ₂ ])
Markless⇒ {Γ} (⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁τ₂ ])

MLSPair : {Γ τ₁ τ₂}
{ě₁ : Γ ⊢⇒ τ₁}
Expand Down
Loading

0 comments on commit 5e413d4

Please sign in to comment.