Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

agda: Use meet symbol for meet #25

Merged
merged 2 commits into from
Oct 27, 2023
Merged

agda: Use meet symbol for meet #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a6db26b
formalism: Use meet symbol for meet
mirryi Oct 27, 2023
5e413d4
agda: Use glub symbol for type meet
mirryi Oct 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion core/erasure.agda
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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