From c57371f0b21c04ae4d3d6fffb5db1a4afd0c83a5 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Sat, 30 Sep 2023 01:36:21 -0400 Subject: [PATCH] agda: Clean up formatting --- hazelnut/action.agda | 38 ++++----- hazelnut/untyped/action.agda | 102 ++++++++++++------------- hazelnut/untyped/constructability.agda | 10 +-- hazelnut/untyped/determinism.agda | 42 +++++----- hazelnut/untyped/erasure.agda | 34 ++++----- hazelnut/untyped/mei.agda | 76 +++++++++--------- marking/totality.agda | 4 +- marking/unicity.agda | 10 +-- marking/wellformed.agda | 74 ++++++++++-------- 9 files changed, 199 insertions(+), 191 deletions(-) diff --git a/hazelnut/action.agda b/hazelnut/action.agda index b78d707..7bce7d3 100644 --- a/hazelnut/action.agda +++ b/hazelnut/action.agda @@ -68,40 +68,40 @@ module hazelnut.action where data _eshape : Shape → Set where ASortVar : (x : Var) - → (var x) eshape + → (var x) eshape ASortLam : (x : Var) - → (lam x) eshape + → (lam x) eshape ASortAp₁ : (u : Hole) - → (ap₁ u) eshape + → (ap₁ u) eshape ASortAp₂ : (u : Hole) - → (ap₂ u) eshape + → (ap₂ u) eshape ASortLet₁ : (x : Var) - → (u : Hole) - → (let₁ x u) eshape + → (u : Hole) + → (let₁ x u) eshape ASortLet₂ : (x : Var) - → (u : Hole) - → (let₂ x u) eshape + → (u : Hole) + → (let₂ x u) eshape ASortNum : (n : ℕ) - → (num n) eshape + → (num n) eshape ASortPlus₁ : (u : Hole) - → (plus₁ u) eshape + → (plus₁ u) eshape ASortPlus₂ : (u : Hole) - → (plus₂ u) eshape + → (plus₂ u) eshape ASortTrue : tt eshape ASortFalse : ff eshape ASortIf₁ : (u₁ : Hole) - → (u₂ : Hole) - → (if₁ u₁ u₂) eshape + → (u₂ : Hole) + → (if₁ u₁ u₂) eshape ASortIf₂ : (u₁ : Hole) - → (u₂ : Hole) - → (if₂ u₁ u₂) eshape + → (u₂ : Hole) + → (if₂ u₁ u₂) eshape ASortIf₃ : (u₁ : Hole) - → (u₂ : Hole) - → (if₃ u₁ u₂) eshape + → (u₂ : Hole) + → (if₃ u₁ u₂) eshape ASortPair₁ : (u : Hole) - → (pair₁ u) eshape + → (pair₁ u) eshape ASortPair₂ : (u : Hole) - → (pair₂ u) eshape + → (pair₂ u) eshape ASortProjL : projl eshape ASortProjR : projr eshape diff --git a/hazelnut/untyped/action.agda b/hazelnut/untyped/action.agda index 99dab24..6c3e882 100644 --- a/hazelnut/untyped/action.agda +++ b/hazelnut/untyped/action.agda @@ -58,32 +58,32 @@ module hazelnut.untyped.action where -- expression actions data _+_+e>_ : (ê : ZExp) → (α : Action) → (ê′ : ZExp) → Set where -- movement - AEMLamChild1 : ∀ {x τ e} - → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 1) +e> (‵λ₁ x ∶ ▹ τ ◃ ∙ e) - AEMLamChild2 : ∀ {x τ e} - → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 2) +e> (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) - AEMLamParent1 : ∀ {x τ e} - → (‵λ₁ x ∶ ▹ τ ◃ ∙ e) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃ - AEMLamParent2 : ∀ {x τ e} - → (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃ - - AEMApChild1 : ∀ {e₁ e₂} - → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂) - AEMApChild2 : ∀ {e₁ e₂} - → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃) - AEMApParent1 : ∀ {e₁ e₂} - → (‵ ‵▹ e₁ ◃ ∙₁ e₂) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃ - AEMApParent2 : ∀ {e₁ e₂} - → (‵ e₁ ∙₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃ - - AEMLetChild1 : ∀ {x e₁ e₂} - → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) - AEMLetChild2 : ∀ {x e₁ e₂} - → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) - AEMLetParent1 : ∀ {x e₁ e₂} - → (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃ - AEMLetParent2 : ∀ {x e₁ e₂} - → (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + AEMLamChild1 : ∀ {x τ e} + → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 1) +e> (‵λ₁ x ∶ ▹ τ ◃ ∙ e) + AEMLamChild2 : ∀ {x τ e} + → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 2) +e> (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) + AEMLamParent1 : ∀ {x τ e} + → (‵λ₁ x ∶ ▹ τ ◃ ∙ e) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃ + AEMLamParent2 : ∀ {x τ e} + → (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃ + + AEMApChild1 : ∀ {e₁ e₂} + → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂) + AEMApChild2 : ∀ {e₁ e₂} + → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃) + AEMApParent1 : ∀ {e₁ e₂} + → (‵ ‵▹ e₁ ◃ ∙₁ e₂) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃ + AEMApParent2 : ∀ {e₁ e₂} + → (‵ e₁ ∙₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃ + + AEMLetChild1 : ∀ {x e₁ e₂} + → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) + AEMLetChild2 : ∀ {x e₁ e₂} + → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) + AEMLetParent1 : ∀ {x e₁ e₂} + → (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + AEMLetParent2 : ∀ {x e₁ e₂} + → (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃ AEMPlusChild1 : ∀ {e₁ e₂} → ‵▹ ‵ e₁ + e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ +₁ e₂) @@ -94,36 +94,36 @@ module hazelnut.untyped.action where AEMPlusParent2 : ∀ {e₁ e₂} → (‵ e₁ +₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ + e₂ ◃ - AEMIfChild1 : ∀ {e₁ e₂ e₃} - → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) - AEMIfChild2 : ∀ {e₁ e₂ e₃} - → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) - AEMIfChild3 : ∀ {e₁ e₂ e₃} - → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 3) +e> (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) - AEMIfParent1 : ∀ {e₁ e₂ e₃} - → (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ - AEMIfParent2 : ∀ {e₁ e₂ e₃} - → (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ - AEMIfParent3 : ∀ {e₁ e₂ e₃} - → (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ - - AEMPairChild1 : ∀ {e₁ e₂} - → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 1) +e> ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ - AEMPairChild2 : ∀ {e₁ e₂} - → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 2) +e> ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ + AEMIfChild1 : ∀ {e₁ e₂ e₃} + → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) + AEMIfChild2 : ∀ {e₁ e₂ e₃} + → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) + AEMIfChild3 : ∀ {e₁ e₂ e₃} + → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 3) +e> (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) + AEMIfParent1 : ∀ {e₁ e₂ e₃} + → (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + AEMIfParent2 : ∀ {e₁ e₂ e₃} + → (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + AEMIfParent3 : ∀ {e₁ e₂ e₃} + → (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + + AEMPairChild1 : ∀ {e₁ e₂} + → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 1) +e> ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ + AEMPairChild2 : ∀ {e₁ e₂} + → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 2) +e> ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ AEMPairParent1 : ∀ {e₁ e₂} - → ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + → ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ AEMPairParent2 : ∀ {e₁ e₂} - → ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + → ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ - AEMProjLChild : ∀ {e} - → ‵▹ ‵π₁ e ◃ + move (child 1) +e> (‵π₁ ‵▹ e ◃) + AEMProjLChild : ∀ {e} + → ‵▹ ‵π₁ e ◃ + move (child 1) +e> (‵π₁ ‵▹ e ◃) AEMProjLParent : ∀ {e} - → (‵π₁ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₁ e ◃ - AEMProjRChild : ∀ {e} - → ‵▹ ‵π₂ e ◃ + move (child 1) +e> (‵π₂ ‵▹ e ◃) + → (‵π₁ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₁ e ◃ + AEMProjRChild : ∀ {e} + → ‵▹ ‵π₂ e ◃ + move (child 1) +e> (‵π₂ ‵▹ e ◃) AEMProjRParent : ∀ {e} - → (‵π₂ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₂ e ◃ + → (‵π₂ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₂ e ◃ -- deletion AEDel : ∀ {e u} diff --git a/hazelnut/untyped/constructability.agda b/hazelnut/untyped/constructability.agda index a9dd7c0..416e7ba 100644 --- a/hazelnut/untyped/constructability.agda +++ b/hazelnut/untyped/constructability.agda @@ -9,9 +9,9 @@ open import hazelnut.untyped.erasure module hazelnut.untyped.constructability where -- constructability of types constructability-τ : (τ : Typ) → ∃[ ᾱ ] ▹ unknown ◃ + ᾱ +τ>* ▹ τ ◃ - constructability-τ num = ⟨ ∣[ construct tnum ] , ATITyp ATConNum ATIRefl ⟩ - constructability-τ bool = ⟨ ∣[ construct tbool ] , ATITyp ATConBool ATIRefl ⟩ - constructability-τ unknown = ⟨ [] , ATIRefl ⟩ + constructability-τ num = ⟨ ∣[ construct tnum ] , ATITyp ATConNum ATIRefl ⟩ + constructability-τ bool = ⟨ ∣[ construct tbool ] , ATITyp ATConBool ATIRefl ⟩ + constructability-τ unknown = ⟨ [] , ATIRefl ⟩ constructability-τ (τ₁ -→ τ₂) with ⟨ ᾱ₁ , +>*τ₁ ⟩ ← constructability-τ τ₁ | ⟨ ᾱ₂ , +>*τ₂ ⟩ ← constructability-τ τ₂ @@ -28,8 +28,8 @@ module hazelnut.untyped.constructability where -- constructability of expressions constructability-e : ∀ {u} → (e : UExp) → ∃[ ᾱ ] ‵▹ ‵⦇-⦈^ u ◃ + ᾱ +e>* ‵▹ e ◃ - constructability-e (‵⦇-⦈^ u) = ⟨ ∣[ del _ ] , AEIExp AEDel AEIRefl ⟩ - constructability-e (‵ x) = ⟨ ∣[ construct (var x) ] , AEIExp AEConVar AEIRefl ⟩ + constructability-e (‵⦇-⦈^ u) = ⟨ ∣[ del _ ] , AEIExp AEDel AEIRefl ⟩ + constructability-e (‵ x) = ⟨ ∣[ construct (var x) ] , AEIExp AEConVar AEIRefl ⟩ constructability-e (‵λ x ∶ τ ∙ e) with ⟨ ᾱ₁ , +>*e ⟩ ← constructability-e e | ⟨ ᾱ₂ , +>*τ ⟩ ← constructability-τ τ diff --git a/hazelnut/untyped/determinism.agda b/hazelnut/untyped/determinism.agda index c820919..566a755 100644 --- a/hazelnut/untyped/determinism.agda +++ b/hazelnut/untyped/determinism.agda @@ -29,19 +29,19 @@ module hazelnut.untyped.determinism where determinism-τ ATConBool ATConBool = refl determinism-τ (ATZipArr1 ()) ATMArrParent1 determinism-τ (ATZipArr1 τ^+>τ^′) (ATZipArr1 τ^+>τ^″) - rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl + rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl determinism-τ (ATZipArr2 τ^+>τ^′) (ATZipArr2 τ^+>τ^″) - rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl + rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl determinism-τ (ATZipProd1 τ^+>τ^′) (ATZipProd1 τ^+>τ^″) - rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl + rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl determinism-τ (ATZipProd2 τ^+>τ^′) (ATZipProd2 τ^+>τ^″) - rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl + rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl determinism*-τ : ∀ {τ^ τ^′ τ^″ ᾱ} → τ^ + ᾱ +τ>* τ^′ → τ^ + ᾱ +τ>* τ^″ → τ^′ ≡ τ^″ determinism*-τ ATIRefl ATIRefl = refl determinism*-τ (ATITyp τ₁^+>τ₂^ τ₂^+>*τ₃^) (ATITyp τ₁^+>τ₂^′ τ₂^+>*τ₃^′) rewrite determinism-τ τ₁^+>τ₂^ τ₁^+>τ₂^′ - rewrite determinism*-τ τ₂^+>*τ₃^ τ₂^+>*τ₃^′ = refl + rewrite determinism*-τ τ₂^+>*τ₃^ τ₂^+>*τ₃^′ = refl determinism-e : ∀ {ê ê′ ê″ α} → ê + α +e> ê′ → ê + α +e> ê″ → ê′ ≡ ê″ determinism-e AEMLamChild1 AEMLamChild1 = refl @@ -94,38 +94,38 @@ module hazelnut.untyped.determinism where determinism-e AEConProjL AEConProjL = refl determinism-e AEConProjR AEConProjR = refl determinism-e (AEZipLam1 τ^+>τ^′) (AEZipLam1 τ^+>τ^″) - rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl + rewrite determinism-τ τ^+>τ^′ τ^+>τ^″ = refl determinism-e (AEZipLam2 ê+>ê′) (AEZipLam2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipAp1 ê+>ê′) (AEZipAp1 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipAp2 ê+>ê′) (AEZipAp2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipLet1 ê+>ê′) (AEZipLet1 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipLet2 ê+>ê′) (AEZipLet2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipPlus1 ê+>ê′) (AEZipPlus1 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipPlus2 ê+>ê′) (AEZipPlus2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipIf1 ê+>ê′) (AEZipIf1 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipIf2 ê+>ê′) (AEZipIf2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipIf3 ê+>ê′) (AEZipIf3 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipPair1 ê+>ê′) (AEZipPair1 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipPair2 ê+>ê′) (AEZipPair2 ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipProjL ê+>ê′) (AEZipProjL ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism-e (AEZipProjR ê+>ê′) (AEZipProjR ê+>ê″) - rewrite determinism-e ê+>ê′ ê+>ê″ = refl + rewrite determinism-e ê+>ê′ ê+>ê″ = refl determinism*-e : ∀ {ê ê′ ê″ ᾱ} → ê + ᾱ +e>* ê′ → ê + ᾱ +e>* ê″ → ê′ ≡ ê″ determinism*-e AEIRefl AEIRefl = refl determinism*-e (AEIExp ê₁+>ê₂ ê₂+>*ê₃) (AEIExp ê₁+>ê₂′ ê₂+>*ê₃′) rewrite determinism-e ê₁+>ê₂ ê₁+>ê₂′ - rewrite determinism*-e ê₂+>*ê₃ ê₂+>*ê₃′ = refl + rewrite determinism*-e ê₂+>*ê₃ ê₂+>*ê₃′ = refl diff --git a/hazelnut/untyped/erasure.agda b/hazelnut/untyped/erasure.agda index 167c4ee..58739d5 100644 --- a/hazelnut/untyped/erasure.agda +++ b/hazelnut/untyped/erasure.agda @@ -6,9 +6,9 @@ open import hazelnut.untyped.zexp module hazelnut.untyped.erasure where -- judgmental cursor erasure data erase-τ : (τ^ : ZTyp) → (τ : Typ) → Set where - ETTop : ∀ {τ} → erase-τ (▹ τ ◃) τ - ETArr1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂) - ETArr2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂) + ETTop : ∀ {τ} → erase-τ (▹ τ ◃) τ + ETArr1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂) + ETArr2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂) ETProd1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -×₁ τ₂) (τ₁ -× τ₂) ETProd2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -×₂ τ₂^) (τ₁ -× τ₂) @@ -104,33 +104,33 @@ module hazelnut.untyped.erasure where erase-e→◇ (EELam1 τ^◇) rewrite erase-τ→◇ τ^◇ = refl erase-e→◇ (EELam2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEAp1 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEAp2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EELet1 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EELet2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEPlus1 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEPlus2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEIf1 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEIf2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEIf3 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEPair1 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEPair2 ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEProjL ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl erase-e→◇ (EEProjR ê◇) - rewrite erase-e→◇ ê◇ = refl + rewrite erase-e→◇ ê◇ = refl -- convert functional cursor erasure to judgmental cursor erasure ◇τ→erase : ∀ {τ^ τ} → τ^ ◇τ ≡ τ → erase-τ τ^ τ diff --git a/hazelnut/untyped/mei.agda b/hazelnut/untyped/mei.agda index d9ceb67..001199a 100644 --- a/hazelnut/untyped/mei.agda +++ b/hazelnut/untyped/mei.agda @@ -9,54 +9,54 @@ open import hazelnut.untyped.erasure module hazelnut.untyped.mei where -- movement erasure invariance movement-erasure-invariance-τ : ∀ {τ^ τ^′ δ} → τ^ + move δ +τ> τ^′ → τ^ ◇τ ≡ τ^′ ◇τ - movement-erasure-invariance-τ ATMArrChild1 = refl - movement-erasure-invariance-τ ATMArrChild2 = refl - movement-erasure-invariance-τ ATMArrParent1 = refl - movement-erasure-invariance-τ ATMArrParent2 = refl + movement-erasure-invariance-τ ATMArrChild1 = refl + movement-erasure-invariance-τ ATMArrChild2 = refl + movement-erasure-invariance-τ ATMArrParent1 = refl + movement-erasure-invariance-τ ATMArrParent2 = refl movement-erasure-invariance-τ (ATZipArr1 τ^+>τ^′) rewrite movement-erasure-invariance-τ τ^+>τ^′ = refl movement-erasure-invariance-τ (ATZipArr2 τ^+>τ^′) rewrite movement-erasure-invariance-τ τ^+>τ^′ = refl - movement-erasure-invariance-τ ATMProdChild1 = refl - movement-erasure-invariance-τ ATMProdChild2 = refl - movement-erasure-invariance-τ ATMProdParent1 = refl - movement-erasure-invariance-τ ATMProdParent2 = refl + movement-erasure-invariance-τ ATMProdChild1 = refl + movement-erasure-invariance-τ ATMProdChild2 = refl + movement-erasure-invariance-τ ATMProdParent1 = refl + movement-erasure-invariance-τ ATMProdParent2 = refl movement-erasure-invariance-τ (ATZipProd1 τ^+>τ^′) rewrite movement-erasure-invariance-τ τ^+>τ^′ = refl movement-erasure-invariance-τ (ATZipProd2 τ^+>τ^′) rewrite movement-erasure-invariance-τ τ^+>τ^′ = refl movement-erasure-invariance-e : ∀ {ê ê′ δ} → ê + move δ +e> ê′ → ê ◇ ≡ ê′ ◇ - movement-erasure-invariance-e AEMLamChild1 = refl - movement-erasure-invariance-e AEMLamChild2 = refl - movement-erasure-invariance-e AEMLamParent1 = refl - movement-erasure-invariance-e AEMLamParent2 = refl - movement-erasure-invariance-e AEMApChild1 = refl - movement-erasure-invariance-e AEMApChild2 = refl - movement-erasure-invariance-e AEMApParent1 = refl - movement-erasure-invariance-e AEMApParent2 = refl - movement-erasure-invariance-e AEMLetChild1 = refl - movement-erasure-invariance-e AEMLetChild2 = refl - movement-erasure-invariance-e AEMLetParent1 = refl - movement-erasure-invariance-e AEMLetParent2 = refl - movement-erasure-invariance-e AEMPlusChild1 = refl - movement-erasure-invariance-e AEMPlusChild2 = refl - movement-erasure-invariance-e AEMPlusParent1 = refl - movement-erasure-invariance-e AEMPlusParent2 = refl - movement-erasure-invariance-e AEMIfChild1 = refl - movement-erasure-invariance-e AEMIfChild2 = refl - movement-erasure-invariance-e AEMIfChild3 = refl - movement-erasure-invariance-e AEMIfParent1 = refl - movement-erasure-invariance-e AEMIfParent2 = refl - movement-erasure-invariance-e AEMIfParent3 = refl - movement-erasure-invariance-e AEMPairChild1 = refl - movement-erasure-invariance-e AEMPairChild2 = refl - movement-erasure-invariance-e AEMPairParent1 = refl - movement-erasure-invariance-e AEMPairParent2 = refl - movement-erasure-invariance-e AEMProjLChild = refl - movement-erasure-invariance-e AEMProjLParent = refl - movement-erasure-invariance-e AEMProjRChild = refl - movement-erasure-invariance-e AEMProjRParent = refl + movement-erasure-invariance-e AEMLamChild1 = refl + movement-erasure-invariance-e AEMLamChild2 = refl + movement-erasure-invariance-e AEMLamParent1 = refl + movement-erasure-invariance-e AEMLamParent2 = refl + movement-erasure-invariance-e AEMApChild1 = refl + movement-erasure-invariance-e AEMApChild2 = refl + movement-erasure-invariance-e AEMApParent1 = refl + movement-erasure-invariance-e AEMApParent2 = refl + movement-erasure-invariance-e AEMLetChild1 = refl + movement-erasure-invariance-e AEMLetChild2 = refl + movement-erasure-invariance-e AEMLetParent1 = refl + movement-erasure-invariance-e AEMLetParent2 = refl + movement-erasure-invariance-e AEMPlusChild1 = refl + movement-erasure-invariance-e AEMPlusChild2 = refl + movement-erasure-invariance-e AEMPlusParent1 = refl + movement-erasure-invariance-e AEMPlusParent2 = refl + movement-erasure-invariance-e AEMIfChild1 = refl + movement-erasure-invariance-e AEMIfChild2 = refl + movement-erasure-invariance-e AEMIfChild3 = refl + movement-erasure-invariance-e AEMIfParent1 = refl + movement-erasure-invariance-e AEMIfParent2 = refl + movement-erasure-invariance-e AEMIfParent3 = refl + movement-erasure-invariance-e AEMPairChild1 = refl + movement-erasure-invariance-e AEMPairChild2 = refl + movement-erasure-invariance-e AEMPairParent1 = refl + movement-erasure-invariance-e AEMPairParent2 = refl + movement-erasure-invariance-e AEMProjLChild = refl + movement-erasure-invariance-e AEMProjLParent = refl + movement-erasure-invariance-e AEMProjRChild = refl + movement-erasure-invariance-e AEMProjRParent = refl movement-erasure-invariance-e (AEZipLam1 τ^+>τ^′) rewrite movement-erasure-invariance-τ τ^+>τ^′ = refl movement-erasure-invariance-e (AEZipLam2 ê+>ê′) diff --git a/marking/totality.agda b/marking/totality.agda index 359640c..e03f92c 100644 --- a/marking/totality.agda +++ b/marking/totality.agda @@ -8,12 +8,12 @@ module marking.totality where ↬⇒-totality : (Γ : Ctx) → (e : UExp) → Σ[ τ ∈ Typ ] Σ[ ě ∈ Γ ⊢⇒ τ ] (Γ ⊢ e ↬⇒ ě) - ↬⇒-totality Γ (‵⦇-⦈^ x) = ⟨ unknown , ⟨ ⊢⦇-⦈^ x , MKSHole ⟩ ⟩ + ↬⇒-totality Γ (‵⦇-⦈^ x) = ⟨ unknown , ⟨ ⊢⦇-⦈^ x , MKSHole ⟩ ⟩ ↬⇒-totality Γ (‵ x) 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 ⟧ , MKSFree ∌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 index 743ee4c..5d72eb2 100644 --- a/marking/unicity.agda +++ b/marking/unicity.agda @@ -8,10 +8,10 @@ module marking.unicity where → Γ ⊢ e ↬⇒ ě₁ → Γ ⊢ e ↬⇒ ě₂ → τ₁ ≡ τ₂ - ↬⇒-τ-unicity MKSHole MKSHole = refl - ↬⇒-τ-unicity (MKSVar ∋x) (MKSVar ∋x′) = ∋→τ-≡ ∋x ∋x′ - ↬⇒-τ-unicity {τ₁ = τ₁} (MKSVar ∋x) (MKSFree ∌x) = ⊥-elim (∌x ⟨ τ₁ , ∋x ⟩) - ↬⇒-τ-unicity {τ₂ = τ₂} (MKSFree ∌x) (MKSVar ∋x) = ⊥-elim (∌x ⟨ τ₂ , ∋x ⟩) + ↬⇒-τ-unicity MKSHole MKSHole = refl + ↬⇒-τ-unicity (MKSVar ∋x) (MKSVar ∋x′) = ∋→τ-≡ ∋x ∋x′ + ↬⇒-τ-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 @@ -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 (MKSFree _) _ = 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 index 80c289c..705ed02 100644 --- a/marking/wellformed.agda +++ b/marking/wellformed.agda @@ -9,9 +9,9 @@ module marking.wellformed where ↬⇒□ : ∀ {Γ : Ctx} {e : UExp} {τ : Typ} {ě : Γ ⊢⇒ τ} → Γ ⊢ e ↬⇒ ě → ě ⇒□ ≡ e - ↬⇒□ MKSHole = refl - ↬⇒□ (MKSVar ∋x) = refl - ↬⇒□ (MKSFree ∌x) = refl + ↬⇒□ MKSHole = refl + ↬⇒□ (MKSVar ∋x) = refl + ↬⇒□ (MKSFree ∌x) = refl ↬⇒□ (MKSLam e↬⇒ě) rewrite ↬⇒□ e↬⇒ě = refl ↬⇒□ (MKSAp1 e₁↬⇒ě₁ τ▸ e₂↬⇐ě₂) @@ -23,12 +23,12 @@ module marking.wellformed where ↬⇒□ (MKSLet e₁↬⇒ě₁ e₂↬⇒ě₂) rewrite ↬⇒□ e₁↬⇒ě₁ | ↬⇒□ e₂↬⇒ě₂ = refl - ↬⇒□ MKSNum = refl + ↬⇒□ MKSNum = refl ↬⇒□ (MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂) rewrite ↬⇐□ e₁↬⇐ě₁ | ↬⇐□ e₂↬⇐ě₂ = refl - ↬⇒□ MKSTrue = refl - ↬⇒□ MKSFalse = refl + ↬⇒□ MKSTrue = refl + ↬⇒□ MKSFalse = refl ↬⇒□ (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂) rewrite ↬⇐□ e₁↬⇐ě₁ | ↬⇒□ e₂↬⇒ě₂ @@ -41,13 +41,13 @@ module marking.wellformed where rewrite ↬⇒□ e₁↬⇒ě₁ | ↬⇒□ e₂↬⇒ě₂ = refl ↬⇒□ (MKSProjL1 e↬⇒ě τ▸) - rewrite ↬⇒□ e↬⇒ě = refl + rewrite ↬⇒□ e↬⇒ě = refl ↬⇒□ (MKSProjL2 e↬⇒ě τ!▸) - rewrite ↬⇒□ e↬⇒ě = refl + rewrite ↬⇒□ e↬⇒ě = refl ↬⇒□ (MKSProjR1 e↬⇒ě τ▸) - rewrite ↬⇒□ e↬⇒ě = refl + rewrite ↬⇒□ e↬⇒ě = refl ↬⇒□ (MKSProjR2 e↬⇒ě τ!▸) - rewrite ↬⇒□ e↬⇒ě = refl + rewrite ↬⇒□ e↬⇒ě = refl ↬⇐□ : ∀ {Γ : Ctx} {e : UExp} {τ : Typ} {ě : Γ ⊢⇐ τ} → Γ ⊢ e ↬⇐ ě @@ -81,50 +81,50 @@ module marking.wellformed where ⇒τ→↬⇒τ : ∀ {Γ : Ctx} {e : UExp} {τ : Typ} → Γ ⊢ e ⇒ τ → Σ[ ě ∈ Γ ⊢⇒ τ ] Γ ⊢ e ↬⇒ ě - ⇒τ→↬⇒τ {e = ‵⦇-⦈^ u} USHole = ⟨ ⊢⦇-⦈^ u , MKSHole ⟩ - ⇒τ→↬⇒τ {e = ‵ x} (USVar ∋x) = ⟨ ⊢ ∋x , MKSVar ∋x ⟩ - ⇒τ→↬⇒τ {e = ‵λ x ∶ τ ∙ e} (USLam e⇒τ) + ⇒τ→↬⇒τ {e = ‵⦇-⦈^ u} USHole = ⟨ ⊢⦇-⦈^ u , MKSHole ⟩ + ⇒τ→↬⇒τ {e = ‵ x} (USVar ∋x) = ⟨ ⊢ ∋x , MKSVar ∋x ⟩ + ⇒τ→↬⇒τ {e = ‵λ x ∶ τ ∙ e} (USLam e⇒τ) with ⟨ ě , e↬⇒ě ⟩ ← ⇒τ→↬⇒τ e⇒τ = ⟨ ⊢λ x ∶ τ ∙ ě , MKSLam e↬⇒ě ⟩ ⇒τ→↬⇒τ {e = ‵ e₁ ∙ e₂} (USAp e₁⇒τ τ▸ e₂⇐τ₂) with ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ← ⇒τ→↬⇒τ e₁⇒τ | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐τ₂ = ⟨ ⊢ ě₁ ∙ ě₂ [ τ▸ ] , MKSAp1 e₁↬⇒ě₁ τ▸ e₂↬⇐ě₂ ⟩ - ⇒τ→↬⇒τ {e = ‵ x ← e₁ ∙ e₂} (USLet e₁⇒τ e₂⇒τ₂) + ⇒τ→↬⇒τ {e = ‵ x ← e₁ ∙ e₂} (USLet e₁⇒τ e₂⇒τ₂) with ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ← ⇒τ→↬⇒τ e₁⇒τ | ⟨ ě₂ , e₂↬⇒ě₂ ⟩ ← ⇒τ→↬⇒τ e₂⇒τ₂ = ⟨ ⊢ x ← ě₁ ∙ ě₂ , MKSLet e₁↬⇒ě₁ e₂↬⇒ě₂ ⟩ - ⇒τ→↬⇒τ {e = ‵ℕ n} USNum = ⟨ ⊢ℕ n , MKSNum ⟩ - ⇒τ→↬⇒τ {e = ‵ e₁ + e₂} (USPlus e₁⇐num e₂⇐num) + ⇒τ→↬⇒τ {e = ‵ℕ n} USNum = ⟨ ⊢ℕ n , MKSNum ⟩ + ⇒τ→↬⇒τ {e = ‵ e₁ + e₂} (USPlus e₁⇐num e₂⇐num) with ⟨ ě₁ , e₁↬⇐ě₁ ⟩ ← ⇐τ→↬⇐τ e₁⇐num | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐num = ⟨ ⊢ ě₁ + ě₂ , MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂ ⟩ - ⇒τ→↬⇒τ {e = ‵tt} USTrue = ⟨ ⊢tt , MKSTrue ⟩ - ⇒τ→↬⇒τ {e = ‵ff} USFalse = ⟨ ⊢ff , MKSFalse ⟩ + ⇒τ→↬⇒τ {e = ‵tt} USTrue = ⟨ ⊢tt , MKSTrue ⟩ + ⇒τ→↬⇒τ {e = ‵ff} USFalse = ⟨ ⊢ff , MKSFalse ⟩ ⇒τ→↬⇒τ {e = ‵ e₁ ∙ e₂ ∙ e₃} (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) with ⟨ ě₁ , e₁↬⇐ě₁ ⟩ ← ⇐τ→↬⇐τ e₁⇐bool | ⟨ ě₂ , e₂↬⇒ě₂ ⟩ ← ⇒τ→↬⇒τ e₂⇒τ₁ | ⟨ ě₃ , e₃↬⇒ě₃ ⟩ ← ⇒τ→↬⇒τ e₃⇒τ₂ = ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] , MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂ ⟩ - ⇒τ→↬⇒τ {e = ‵⟨ e₁ , e₂ ⟩} (USPair e₁⇒τ₁ e₂⇒τ₂) + ⇒τ→↬⇒τ {e = ‵⟨ e₁ , e₂ ⟩} (USPair e₁⇒τ₁ e₂⇒τ₂) with ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ← ⇒τ→↬⇒τ e₁⇒τ₁ | ⟨ ě₂ , e₂↬⇒ě₂ ⟩ ← ⇒τ→↬⇒τ e₂⇒τ₂ = ⟨ ⊢⟨ ě₁ , ě₂ ⟩ , MKSPair e₁↬⇒ě₁ e₂↬⇒ě₂ ⟩ - ⇒τ→↬⇒τ {e = ‵π₁ e} (USProjL e⇒τ τ▸) + ⇒τ→↬⇒τ {e = ‵π₁ e} (USProjL e⇒τ τ▸) with ⟨ ě , e↬⇒ě ⟩ ← ⇒τ→↬⇒τ e⇒τ = ⟨ ⊢π₁ ě [ τ▸ ] , MKSProjL1 e↬⇒ě τ▸ ⟩ - ⇒τ→↬⇒τ {e = ‵π₂ e} (USProjR e⇒τ τ▸) + ⇒τ→↬⇒τ {e = ‵π₂ e} (USProjR e⇒τ τ▸) with ⟨ ě , e↬⇒ě ⟩ ← ⇒τ→↬⇒τ e⇒τ = ⟨ ⊢π₂ ě [ τ▸ ] , MKSProjR1 e↬⇒ě τ▸ ⟩ ⇐τ→↬⇐τ : ∀ {Γ : Ctx} {e : UExp} {τ : Typ} → Γ ⊢ e ⇐ τ → Σ[ ě ∈ Γ ⊢⇐ τ ] Γ ⊢ e ↬⇐ ě - ⇐τ→↬⇐τ {e = ‵λ x ∶ τ ∙ e} (UALam τ₃▸ τ~τ₁ e⇐τ₂) + ⇐τ→↬⇐τ {e = ‵λ x ∶ τ ∙ e} (UALam τ₃▸ τ~τ₁ e⇐τ₂) with ⟨ ě , e↬⇐ě ⟩ ← ⇐τ→↬⇐τ e⇐τ₂ = ⟨ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] , MKALam1 τ₃▸ τ~τ₁ e↬⇐ě ⟩ - ⇐τ→↬⇐τ {e = ‵ x ← e₁ ∙ e₂} (UALet e₁⇒τ e₂⇐τ₂) + ⇐τ→↬⇐τ {e = ‵ x ← e₁ ∙ e₂} (UALet e₁⇒τ e₂⇐τ₂) with ⟨ ě₁ , e₁↬⇒ě₁ ⟩ ← ⇒τ→↬⇒τ e₁⇒τ | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐τ₂ = ⟨ ⊢ x ← ě₁ ∙ ě₂ , MKALet e₁↬⇒ě₁ e₂↬⇐ě₂ ⟩ ⇐τ→↬⇐τ {e = ‵ e₁ ∙ e₂ ∙ e₃} (UAIf e₁⇐τ e₂⇐τ₁ e₃⇐τ₂) with ⟨ ě₁ , e₁↬⇐ě₁ ⟩ ← ⇐τ→↬⇐τ e₁⇐τ | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐τ₁ | ⟨ ě₃ , e₃↬⇐ě₃ ⟩ ← ⇐τ→↬⇐τ e₃⇐τ₂ = ⟨ ⊢ ě₁ ∙ ě₂ ∙ ě₃ , MKAIf e₁↬⇐ě₁ e₂↬⇐ě₂ e₃↬⇐ě₃ ⟩ - ⇐τ→↬⇐τ {e = ‵⟨ e₁ , e₂ ⟩} (UAPair τ▸ e₁⇐τ₁ e₂⇐τ₂) + ⇐τ→↬⇐τ {e = ‵⟨ e₁ , e₂ ⟩} (UAPair τ▸ e₁⇐τ₁ e₂⇐τ₂) with ⟨ ě₁ , e₁↬⇐ě₁ ⟩ ← ⇐τ→↬⇐τ e₁⇐τ₁ | ⟨ ě₂ , e₂↬⇐ě₂ ⟩ ← ⇐τ→↬⇐τ e₂⇐τ₂ = ⟨ ⊢⟨ ě₁ , ě₂ ⟩[ τ▸ ] , MKAPair1 e₁↬⇐ě₁ e₂↬⇐ě₂ τ▸ ⟩ - ⇐τ→↬⇐τ {e = e} (UASubsume e⇒τ′ τ~τ′ su) + ⇐τ→↬⇐τ {e = e} (UASubsume e⇒τ′ τ~τ′ su) with ⟨ ě , e↬⇒ě ⟩ ← ⇒τ→↬⇒τ e⇒τ′ = ⟨ ⊢∙ ě [ τ~τ′ ∙ USu→MSu su e↬⇒ě ] , MKASubsume e↬⇒ě τ~τ′ su ⟩ -- marking synthesizes the same type as synthesis @@ -132,11 +132,15 @@ module marking.wellformed where → Γ ⊢ e ⇒ τ → Γ ⊢ e ↬⇒ ě → τ ≡ τ′ - ⇒-↬-≡ USHole MKSHole = refl - ⇒-↬-≡ (USVar ∋x) (MKSVar ∋x′) = ∋→τ-≡ ∋x ∋x′ - ⇒-↬-≡ (USVar {τ = τ} ∋x) (MKSFree ∌y) = ⊥-elim (∌y ⟨ τ , ∋x ⟩) + ⇒-↬-≡ USHole MKSHole + = refl + ⇒-↬-≡ (USVar ∋x) (MKSVar ∋x′) + = ∋→τ-≡ ∋x ∋x′ + ⇒-↬-≡ (USVar {τ = τ} ∋x) (MKSFree ∌y) + = ⊥-elim (∌y ⟨ τ , ∋x ⟩) ⇒-↬-≡ (USLam e⇒τ) (MKSLam e↬⇒ě) - rewrite ⇒-↬-≡ e⇒τ e↬⇒ě = refl + rewrite ⇒-↬-≡ e⇒τ e↬⇒ě + = refl ⇒-↬-≡ (USAp e⇒τ τ▸ e₁⇐τ₁) (MKSAp1 e↬⇒ě τ▸′ e₂↬⇐ě₂) with refl ← ⇒-↬-≡ e⇒τ e↬⇒ě with refl ← ▸-→-unicity τ▸ τ▸′ @@ -148,10 +152,14 @@ module marking.wellformed where with refl ← ⇒-↬-≡ e₁⇒τ₁ e₁↬⇒ě₁ with refl ← ⇒-↬-≡ e₂⇒τ₂ e₂↬⇒ě₂ = refl - ⇒-↬-≡ USNum MKSNum = refl - ⇒-↬-≡ (USPlus e₁⇐num e₂⇐num) (MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂) = refl - ⇒-↬-≡ USTrue MKSTrue = refl - ⇒-↬-≡ USFalse MKSFalse = refl + ⇒-↬-≡ USNum MKSNum + = refl + ⇒-↬-≡ (USPlus e₁⇐num e₂⇐num) (MKSPlus e₁↬⇐ě₁ e₂↬⇐ě₂) + = refl + ⇒-↬-≡ USTrue MKSTrue + = refl + ⇒-↬-≡ USFalse MKSFalse + = refl ⇒-↬-≡ (USIf e₁⇐bool e₂⇒τ₁ e₃⇒τ₂ τ₁⊔τ₂) (MKSIf e₁↬⇐ě₁ e₂↬⇒ě₂ e₃↬⇒ě₃ τ₁⊔τ₂′) with refl ← ⇒-↬-≡ e₂⇒τ₁ e₂↬⇒ě₂ with refl ← ⇒-↬-≡ e₃⇒τ₂ e₃↬⇒ě₃