From 01bea991b164478c48b20c9279bd0a6ba12d8672 Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Fri, 9 Jun 2023 07:26:57 +0900 Subject: [PATCH 1/2] agda: Remove typed hazelnut agda stuff --- hazelnut.agda | 1 - hazelnut/typed.agda | 4 - hazelnut/typed/action.agda | 509 ---------------------------- hazelnut/typed/zexp.agda | 666 ------------------------------------- hazelnut/typed/ztyp.agda | 32 -- 5 files changed, 1212 deletions(-) delete mode 100644 hazelnut/typed.agda delete mode 100644 hazelnut/typed/action.agda delete mode 100644 hazelnut/typed/zexp.agda delete mode 100644 hazelnut/typed/ztyp.agda diff --git a/hazelnut.agda b/hazelnut.agda index 9078b2f..ea6092b 100644 --- a/hazelnut.agda +++ b/hazelnut.agda @@ -1,4 +1,3 @@ module hazelnut where import hazelnut.action import hazelnut.untyped - import hazelnut.typed diff --git a/hazelnut/typed.agda b/hazelnut/typed.agda deleted file mode 100644 index 61841f9..0000000 --- a/hazelnut/typed.agda +++ /dev/null @@ -1,4 +0,0 @@ -module hazelnut.typed where - open import hazelnut.typed.ztyp public - open import hazelnut.typed.zexp public - open import hazelnut.typed.action public diff --git a/hazelnut/typed/action.agda b/hazelnut/typed/action.agda deleted file mode 100644 index 996fdf3..0000000 --- a/hazelnut/typed/action.agda +++ /dev/null @@ -1,509 +0,0 @@ -open import prelude -open import core -open import marking - -open import hazelnut.action -open import hazelnut.typed.ztyp -open import hazelnut.typed.zexp - -module hazelnut.typed.action where - -- type actions - data _~_~τ>_ : (τ : ZTyp) → (α : Action) → (τ′ : ZTyp) → Set where - -- movement - TMArrChild1 : ∀ {τ₁ τ₂ : Typ} - → ▹ τ₁ -→ τ₂ ◃ ~ move (child 1) ~τ> ▹ τ₁ ◃ -→₁ τ₂ - TMArrChild2 : ∀ {τ₁ τ₂ : Typ} - → ▹ τ₁ -→ τ₂ ◃ ~ move (child 2) ~τ> τ₁ -→₂ ▹ τ₂ ◃ - TMArrParent1 : ∀ {τ₁ τ₂ : Typ} - → ▹ τ₁ ◃ -→₁ τ₂ ~ move parent ~τ> ▹ τ₁ -→ τ₂ ◃ - TMArrParent2 : ∀ {τ₁ τ₂ : Typ} - → τ₁ -→₂ ▹ τ₂ ◃ ~ move parent ~τ> ▹ τ₁ -→ τ₂ ◃ - - -- deletion - TDel : ∀ {τ : Typ} {u : Hole} - → ▹ τ ◃ ~ (del u) ~τ> ▹ unknown ◃ - - -- construction - TConArrow1 : ∀ {τ : Typ} - → ▹ τ ◃ ~ construct tarrow₁ ~τ> τ -→₂ ▹ unknown ◃ - TConArrow2 : ∀ {τ : Typ} - → ▹ τ ◃ ~ construct tarrow₂ ~τ> ▹ unknown ◃ -→₁ τ - TConNum : ▹ unknown ◃ ~ construct tnum ~τ> ▹ num ◃ - TConBool : ▹ unknown ◃ ~ construct tbool ~τ> ▹ bool ◃ - - -- zipper - TZipArr1 : ∀ {τ^ τ^′ : ZTyp} {τ : Typ} {α : Action} - → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) - → τ^ -→₁ τ ~ α ~τ> τ^′ -→₁ τ - TZipArr2 : ∀ {τ^ τ^′ : ZTyp} {τ : Typ} {α : Action} - → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) - → τ -→₂ τ^ ~ α ~τ> τ -→₂ τ^′ - - -- iterated type actions - data _~_~τ>*_ : (τ^ : ZTyp) → (ᾱ : ActionList) → (τ^′ : ZTyp) → Set where - TIRefl : ∀ {τ^} - → τ^ ~ [] ~τ>* τ^ - TITyp : ∀ {τ^ τ^′ τ^″ α ᾱ} - → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) - → (τ^′~>*τ^″ : τ^′ ~ ᾱ ~τ>* τ^″) - → τ^ ~ α ∷ ᾱ ~τ>* τ^″ - - ~τ>*-++ : ∀ {τ^ τ^′ τ^″ ᾱ₁ ᾱ₂} → τ^ ~ ᾱ₁ ~τ>* τ^′ → τ^′ ~ ᾱ₂ ~τ>* τ^″ → τ^ ~ (ᾱ₁ ++ ᾱ₂) ~τ>* τ^″ - ~τ>*-++ TIRefl τ^~>*τ^″ = τ^~>*τ^″ - ~τ>*-++ (TITyp τ^~>τ^′ τ^′~>*τ^″) τ^″~>*τ^‴ = TITyp τ^~>τ^′ (~τ>*-++ τ^′~>*τ^″ τ^″~>*τ^‴) - - -- type zippers - ziplem-tarr1 : ∀ {τ^ τ^′ τ ᾱ} → τ^ ~ ᾱ ~τ>* τ^′ → (τ^ -→₁ τ) ~ ᾱ ~τ>* (τ^′ -→₁ τ) - ziplem-tarr1 TIRefl = TIRefl - ziplem-tarr1 (TITyp τ^~>τ^′ τ^′~>*τ^″) = TITyp (TZipArr1 τ^~>τ^′) (ziplem-tarr1 τ^′~>*τ^″) - - ziplem-tarr2 : ∀ {τ^ τ^′ τ ᾱ} → τ^ ~ ᾱ ~τ>* τ^′ → (τ -→₂ τ^) ~ ᾱ ~τ>* (τ -→₂ τ^′) - ziplem-tarr2 TIRefl = TIRefl - ziplem-tarr2 (TITyp τ^~>τ^′ τ^′~>*τ^″) = TITyp (TZipArr2 τ^~>τ^′) (ziplem-tarr2 τ^′~>*τ^″) - - mutual - -- synthetic expression movements - data _+_+⇒_ : ∀ {Γ τ τ′} → (ê : - Γ ⊢⇒ τ) → (δ : Dir) → (ê′ : - Γ ⊢⇒ τ′) → Set where - -- movement - ESMLamChild1 : ∀ {Γ x τ} - → {ě : Γ , x ∶ τ ⊢⇒ τ} - → ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + child 1 +⇒ (⊢λ₁ x ∶ ▹ τ ◃ ∙ ě) - ESMLamChild2 : ∀ {Γ x τ} - → {ě : Γ , x ∶ τ ⊢⇒ τ} - → ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + child 2 +⇒ (⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃) - ESMLamParent1 : ∀ {Γ x τ} - → {ě : Γ , x ∶ τ ⊢⇒ τ} - → (⊢λ₁ x ∶ ▹ τ ◃ ∙ ě) + parent +⇒ ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ - ESMLamParent2 : ∀ {Γ x τ} - → {ě : Γ , x ∶ τ ⊢⇒ τ} - → (⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃) + parent +⇒ ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ - - ESMAp1Child1 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → {ě₂ : Γ ⊢⇐ τ₁} - → ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + child 1 +⇒ ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ [ τ▸ ] - ESMAp1Child2 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → {ě₂ : Γ ⊢⇐ τ₁} - → ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + child 2 +⇒ ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ [ τ▸ ] - ESMAp1Parent1 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → {ě₂ : Γ ⊢⇐ τ₁} - → ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ [ τ▸ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ - ESMAp1Parent2 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → {ě₂ : Γ ⊢⇐ τ₁} - → ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ [ τ▸ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ - - ESMAp2Child1 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {τ!▸ : τ !▸-→} - → {ě₂ : Γ ⊢⇐ unknown} - → ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + child 1 +⇒ ⊢⸨ ⊢▹ ě₁ ◃ ⸩∙₁ ě₂ [ τ!▸ ] - ESMAp2Child2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {τ!▸ : τ !▸-→} - → {ě₂ : Γ ⊢⇐ unknown} - → ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + child 2 +⇒ ⊢⸨ ě₁ ⸩∙₂ ⊢▹ ě₂ ◃ [ τ!▸ ] - ESMAp2Parent1 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {τ!▸ : τ !▸-→} - → {ě₂ : Γ ⊢⇐ unknown} - → ⊢⸨ ⊢▹ ě₁ ◃ ⸩∙₁ ě₂ [ τ!▸ ] + parent +⇒ ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ - ESMAp2Parent2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {τ!▸ : τ !▸-→} - → {ě₂ : Γ ⊢⇐ unknown} - → ⊢⸨ ě₁ ⸩∙₂ ⊢▹ ě₂ ◃ [ τ!▸ ] + parent +⇒ ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ - - ESMLetChild1 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} - → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 1 +⇒ (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) - ESMLetChild2 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} - → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 2 +⇒ (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) - ESMLetParent1 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} - → (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + parent +⇒ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ - ESMLetParent2 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} - → (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + parent +⇒ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ - - ESMPlusChild1 : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → ⊢▹ ⊢ ě₁ + ě₂ ◃ + child 1 +⇒ (⊢ ⊢▹ ě₁ ◃ +₁ ě₂) - ESMPlusChild2 : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → ⊢▹ ⊢ ě₁ + ě₂ ◃ + child 2 +⇒ (⊢ ě₁ +₂ ⊢▹ ě₂ ◃) - ESMPlusParent1 : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → (⊢ ⊢▹ ě₁ ◃ +₁ ě₂) + parent +⇒ ⊢▹ ⊢ ě₁ + ě₂ ◃ - ESMPlusParent2 : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → (⊢ ě₁ +₂ ⊢▹ ě₂ ◃) + parent +⇒ ⊢▹ ⊢ ě₁ + ě₂ ◃ - - ESMIfChild1 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 1 +⇒ ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] - ESMIfChild2 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 2 +⇒ ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ [ τ₁⊔τ₂ ] - ESMIfChild3 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 3 +⇒ ⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ [ τ₁⊔τ₂ ] - ESMIfParent1 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ - ESMIfParent2 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ - ESMIfParent3 : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → ⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ - - ESMInconsistentBranchesChild1 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 1 +⇒ ⊢⦉ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] - ESMInconsistentBranchesChild2 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 2 +⇒ ⊢⦉ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] - ESMInconsistentBranchesChild3 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 3 +⇒ ⊢⦉ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ ⦊[ τ₁~̸τ₂ ] - ESMInconsistentBranchesParent1 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢⦉ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ - ESMInconsistentBranchesParent2 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢⦉ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ - ESMInconsistentBranchesParent3 : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ⊢⦉ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ - - MSu-+⇒ : ∀ {Γ τ} {ě : Γ ⊢⇒ τ} {n : ℕ} {ê : - Γ ⊢⇒ τ} → MSubsumable ě → ⊢▹ ě ◃ + child n +⇒ ê → ZSubsumable ê - MSu-+⇒ MSuAp1 ESMAp1Child1 = ZSuZipApL1 - MSu-+⇒ MSuAp1 ESMAp1Child2 = ZSuZipApR1 - MSu-+⇒ MSuAp2 ESMAp2Child1 = ZSuZipApL2 - MSu-+⇒ MSuAp2 ESMAp2Child2 = ZSuZipApR2 - MSu-+⇒ MSuPlus ESMPlusChild1 = ZSuPlus1 - MSu-+⇒ MSuPlus ESMPlusChild2 = ZSuPlus2 - MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild1 = ZSuInconsistentBranchesC - MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild2 = ZSuInconsistentBranchesL - MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild3 = ZSuInconsistentBranchesR - - ZSu-+⇒ : ∀ {Γ τ} {ê : - Γ ⊢⇒ τ} {ě : Γ ⊢⇒ τ} → ZSubsumable ê → ê + parent +⇒ ⊢▹ ě ◃ → MSubsumable ě - ZSu-+⇒ ZSuZipApL1 ESMAp1Parent1 = MSuAp1 - ZSu-+⇒ ZSuZipApR1 ESMAp1Parent2 = MSuAp1 - ZSu-+⇒ ZSuZipApL2 ESMAp2Parent1 = MSuAp2 - ZSu-+⇒ ZSuZipApR2 ESMAp2Parent2 = MSuAp2 - ZSu-+⇒ ZSuPlus1 ESMPlusParent1 = MSuPlus - ZSu-+⇒ ZSuPlus2 ESMPlusParent2 = MSuPlus - ZSu-+⇒ ZSuInconsistentBranchesC ESMInconsistentBranchesParent1 = MSuInconsistentBranches - ZSu-+⇒ ZSuInconsistentBranchesL ESMInconsistentBranchesParent2 = MSuInconsistentBranches - ZSu-+⇒ ZSuInconsistentBranchesR ESMInconsistentBranchesParent3 = MSuInconsistentBranches - - -- analytic expression movements - data _+_+⇐_ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → (δ : Dir) → (ê′ : - Γ ⊢⇐ τ) → Set where - EAMLam1Child1 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : τ ~ τ₁} - → ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + child 1 +⇐ ⊢λ₁ x ∶ ▹ τ ◃ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] - EAMLam1Child2 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : τ ~ τ₁} - → ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + child 2 +⇐ ⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~τ₁ ] - EAMLam1Parent1 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : τ ~ τ₁} - → ⊢λ₁ x ∶ ▹ τ ◃ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ - EAMLam1Parent2 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : τ ~ τ₁} - → ⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ - - EAMLam2Child1 : ∀ {Γ x τ τ′} - → {ě : Γ , x ∶ τ ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + child 1 +⇐ ⊢⸨λ₁ x ∶ ▹ τ ◃ ∙ ě ⸩[ τ′!▸ ] - EAMLam2Child2 : ∀ {Γ x τ τ′} - → {ě : Γ , x ∶ τ ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + child 2 +⇐ ⊢⸨λ₂ x ∶ τ ∙ ⊢▹ ě ◃ ⸩[ τ′!▸ ] - EAMLam2Parent1 : ∀ {Γ x τ τ′} - → {ě : Γ , x ∶ τ ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → ⊢⸨λ₁ x ∶ ▹ τ ◃ ∙ ě ⸩[ τ′!▸ ] + parent +⇐ ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ - EAMLam2Parent2 : ∀ {Γ x τ τ′} - → {ě : Γ , x ∶ τ ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → ⊢⸨λ₂ x ∶ τ ∙ ⊢▹ ě ◃ ⸩[ τ′!▸ ] + parent +⇐ ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ - - EAMLam3Child1 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : τ ~̸ τ₁} - → ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + child 1 +⇐ ⊢λ₁ x ∶⸨ ▹ τ ◃ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] - EAMLam3Child2 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : τ ~̸ τ₁} - → ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + child 2 +⇐ ⊢λ₂ x ∶⸨ τ ⸩∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~̸τ₁ ] - EAMLam3Parent1 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : τ ~̸ τ₁} - → ⊢λ₁ x ∶⸨ ▹ τ ◃ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ - EAMLam3Parent2 : ∀ {Γ x τ τ₁ τ₂ τ₃} - → {ě : Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : τ ~̸ τ₁} - → ⊢λ₂ x ∶⸨ τ ⸩∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~̸τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ - - EAMLetChild1 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} - → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 1 +⇐ (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) - EAMLetChild2 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} - → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 2 +⇐ (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) - EAMLetParent1 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} - → (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + parent +⇐ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ - EAMLetParent2 : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} - → (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + parent +⇐ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ - - EAMIfChild1 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 1 +⇐ (⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃) - EAMIfChild2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 2 +⇐ (⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃) - EAMIfChild3 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 3 +⇐ (⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃) - EAMIfParent1 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → (⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ - EAMIfParent2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → (⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ - EAMIfParent3 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → (⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ - - EAMInconsistentTypesChild : ∀ {Γ τ τ′ n} - → {ě : Γ ⊢⇒ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {+⇒ê : ⊢▹ ě ◃ + child n +⇒ ê} - → {τ~̸τ′ : τ ~̸ τ′} - → {su : MSubsumable ě} - → ⊢▹ ⊢⸨ ě ⸩[ τ~̸τ′ ∙ su ] ◃ + child n +⇐ ⊢⸨ ê ⸩[ τ~̸τ′ ∙ MSu-+⇒ su +⇒ê ] - EAMInconsistentTypesParent : ∀ {Γ τ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {ě : Γ ⊢⇒ τ′} - → {ê+⇒ : ê + parent +⇒ ⊢▹ ě ◃} - → {τ~̸τ′ : τ ~̸ τ′} - → {zsu : ZSubsumable ê} - → ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] + parent +⇐ ⊢▹ ⊢⸨ ě ⸩[ τ~̸τ′ ∙ ZSu-+⇒ zsu ê+⇒ ] ◃ - - EAMSubsumeChild : ∀ {Γ τ τ′ n} - → {ě : Γ ⊢⇒ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {+⇒ê : ⊢▹ ě ◃ + child n +⇒ ê} - → {τ~τ′ : τ ~ τ′} - → {su : MSubsumable ě} - → ⊢▹ ⊢∙ ě [ τ~τ′ ∙ su ] ◃ + child n +⇐ ⊢∙ ê [ τ~τ′ ∙ MSu-+⇒ su +⇒ê ] - EAMSubsumeParent : ∀ {Γ τ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {ě : Γ ⊢⇒ τ′} - → {ê+⇒ : ê + parent +⇒ ⊢▹ ě ◃} - → {τ~τ′ : τ ~ τ′} - → {zsu : ZSubsumable ê} - → ⊢∙ ê [ τ~τ′ ∙ zsu ] + parent +⇐ ⊢▹ ⊢∙ ě [ τ~τ′ ∙ ZSu-+⇒ zsu ê+⇒ ] ◃ - - mutual - -- synthetic expression actions - data _⊢_~_~⇒_ : ∀ {τ τ′ : Typ} → (Γ : Ctx) → (ê : - Γ ⊢⇒ τ) → (α : Action) → (ê : - Γ ⊢⇒ τ′) → Set where - -- movement - ESMove : ∀ {Γ τ δ} - → {ê : - Γ ⊢⇒ τ} - → {ê′ : - Γ ⊢⇒ τ} - → {ê+⇒ê′ : ê + δ +⇒ ê′} - → Γ ⊢ ê ~ move δ ~⇒ ê′ - - -- deletion - ESDel : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ del u ~⇒ ⊢▹ ⊢⦇-⦈^ u ◃ - - -- construction - ESConBoundVar : ∀ {Γ u τ x} - → (∋x : Γ ∋ x ∶ τ) - → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (var x) ~⇒ ⊢▹ ⊢ ∋x ◃ - ESConUnboundVar : ∀ {Γ u y} - → (∌y : Γ ∌ y) - → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (var y) ~⇒ ⊢▹ ⊢⟦ ∌y ⟧ ◃ - ESConLam : ∀ {Γ τ x τ′} - → {ě : Γ ⊢⇒ τ} - → {ě′ : Γ , x ∶ unknown ⊢⇒ τ′} - → (↬⇒ě′ : Γ , x ∶ unknown ⊢ (ě ⇒□) ↬⇒ ě′) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (lam x) ~⇒ (⊢λ₁ x ∶ ▹ unknown ◃ ∙ ě′) - ESConApL1 : ∀ {Γ τ τ₁ τ₂ u} - → {ě : Γ ⊢⇒ τ} - → (τ▸ : τ ▸ τ₁ -→ τ₂) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₁ u) ~⇒ ⊢ ě ∙₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) [ τ▸ ] - ESConApL2 : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → (τ!▸ : τ !▸-→) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₁ u) ~⇒ ⊢⸨ ě ⸩∙₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) [ τ!▸ ] - ESConApR : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₂ u) ~⇒ ⊢ (⊢▹ ⊢⦇-⦈^ u ◃) ∙₁ (proj₁ (⊢⇒-⊢⇐ ě)) [ TMAUnknown ] - ESConLet1 : ∀ {Γ τ x u} - → {ě : Γ ⊢⇒ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ construct (let₁ x u) ~⇒ (⊢ x ←₂ ě ∙ ⊢▹ ⊢⦇-⦈^ u ◃) - ESConLet2 : ∀ {Γ τ x u τ′} - → {ě : Γ ⊢⇒ τ} - → {ě′ : Γ , x ∶ unknown ⊢⇒ τ′} - → (↬⇒ě′ : Γ , x ∶ unknown ⊢ (ě ⇒□) ↬⇒ ě′) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (let₂ x u) ~⇒ (⊢ x ←₁ ⊢▹ ⊢⦇-⦈^ u ◃ ∙ ě′) - ESConNum : ∀ {Γ u n} - → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (num n) ~⇒ ⊢▹ ⊢ℕ n ◃ - ESConPlusL1 : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → (τ~num : τ ~ num) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₁ u) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) +₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃)) - ESConPlusL2 : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → (τ~̸num : τ ~̸ num) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₁ u) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) +₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃)) - ESConPlusR1 : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → (τ~num : τ ~ num) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₂ u) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) +₁ (proj₁ (⊢⇒-⊢⇐ ě))) - ESConPlusR2 : ∀ {Γ τ u} - → {ě : Γ ⊢⇒ τ} - → (τ~̸num : τ ~̸ num) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₂ u) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) +₁ (proj₁ (⊢⇒-⊢⇐ ě))) - ESConIfC1 : ∀ {Γ τ u₁ u₂} - → {ě : Γ ⊢⇒ τ} - → (τ~bool : τ ~ bool) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₁ u₁ u₂) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) ∙₂ (⊢▹ ⊢⦇-⦈^ u₁ ◃) ∙ (⊢⦇-⦈^ u₂) [ TJUnknown ]) - ESConIfC2 : ∀ {Γ τ u₁ u₂} - → {ě : Γ ⊢⇒ τ} - → (τ~̸bool : τ ~̸ bool) - → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₁ u₁ u₂) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) ∙₂ (⊢▹ ⊢⦇-⦈^ u₁ ◃) ∙ (⊢⦇-⦈^ u₂) [ TJUnknown ]) - ESConIfL : ∀ {Γ τ u₁ u₂} - → {ě : Γ ⊢⇒ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₂ u₁ u₂) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u₁ [ ~-unknown₂ ∙ MSuHole ] ◃) ∙₁ ě ∙ (⊢⦇-⦈^ u₂) [ ⊔-unknown₂ ]) - ESConIfR : ∀ {Γ τ u₁ u₂} - → {ě : Γ ⊢⇒ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₃ u₁ u₂) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u₁ [ ~-unknown₂ ∙ MSuHole ] ◃) ∙₁ (⊢⦇-⦈^ u₂) ∙ ě [ ⊔-unknown₁ ]) - - -- zipper cases - ESZipLamT1 : ∀ {Γ x τ₁^ τ₁^′ τ₂ α} - → {ě : Γ , x ∶ (τ₁^ ◇τ) ⊢⇒ τ₂} - → (~>τ₁′ : τ₁^ ~ α ~τ> τ₁^′) - → (τ₁^≡τ₁′ : (τ₁^ ◇τ) ≡ (τ₁^′ ◇τ)) - → Γ ⊢ (⊢λ₁ x ∶ τ₁^ ∙ ě) ~ α ~⇒ (⊢λ₁ x ∶ τ₁^′ ∙ proj₁ (◇≡-⊢⇒ {Γ} {x} {τ₁^} {τ₁^′} ě τ₁^≡τ₁′)) - ESZipLamT2 : ∀ {Γ x τ₁^ τ₁^′ τ₂ τ₂′ α} - → {ě : Γ , x ∶ (τ₁^ ◇τ) ⊢⇒ τ₂} - → {ě′ : Γ , x ∶ (τ₁^′ ◇τ) ⊢⇒ τ₂′} - → (~>τ₁′ : τ₁^ ~ α ~τ> τ₁^′) - → (τ₁^≢τ₁′ : (τ₁^ ◇τ) ≢ (τ₁^′ ◇τ)) - → (↬⇒ě′ : Γ , x ∶ (τ₁^′ ◇τ) ⊢ (ě ⇒□) ↬⇒ ě′) - → Γ ⊢ (⊢λ₁ x ∶ τ₁^ ∙ ě) ~ α ~⇒ (⊢λ₁ x ∶ τ₁^′ ∙ ě′) - ESZipLamE : ∀ {Γ x τ₁ τ₂ τ₂′ α} - → {ê : - Γ , x ∶ τ₁ ⊢⇒ τ₂} - → {ê′ : - Γ , x ∶ τ₁ ⊢⇒ τ₂′} - → (~⇒ê′ : (Γ , x ∶ τ₁) ⊢ ê ~ α ~⇒ ê′) - → Γ ⊢ (⊢λ₂ x ∶ τ₁ ∙ ê) ~ α ~⇒ (⊢λ₂ x ∶ τ₁ ∙ ê′) - -- ESZipApL1 : ∀ {Γ τ τ₁ τ₂ τ₃ τ₁′ τ₂′ τ₃′ α} - -- → {τ₁▸ : τ₁ ▸ τ₂ -→ τ₃} - -- → (ê₁ : - Γ ⊢⇒ τ₁) - -- → {ê₁′ : - Γ ⊢⇒ τ₁′} - -- → {τ₁′▸ : τ₁′ ▸ τ₂′ -→ τ₃′} - -- → {ě₂ : Γ ⊢⇐ τ₂} - -- → Γ ⊢ ⊢ ê₁ ∙₁ ě₂ [ τ₁▸ ] ~ α ~⇒ ⊢ ê₁′ ∙₁ (proj₁ (⊢⇐-⊢⇐ ě₂)) [ τ₁′▸ ] - - -- analytic expression actions - data _⊢_~_~⇐_ : ∀ {τ : Typ} → (Γ : Ctx) → (ê : - Γ ⊢⇐ τ) → (α : Action) → (ê : - Γ ⊢⇐ τ) → Set where - -- movement - EAMove : ∀ {Γ τ δ} - → {ê : - Γ ⊢⇐ τ} - → {ê′ : - Γ ⊢⇐ τ} - → {ê+⇐ê′ : ê + δ +⇐ ê′} - → Γ ⊢ ê ~ move δ ~⇐ ê′ - - -- deletion - EADel : ∀ {Γ τ u} - → {ě : Γ ⊢⇐ τ} - → Γ ⊢ ⊢▹ ě ◃ ~ del u ~⇐ ⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃ diff --git a/hazelnut/typed/zexp.agda b/hazelnut/typed/zexp.agda deleted file mode 100644 index a64dfa7..0000000 --- a/hazelnut/typed/zexp.agda +++ /dev/null @@ -1,666 +0,0 @@ -open import prelude -open import core - -open import hazelnut.typed.ztyp - --- cursor expressions -module hazelnut.typed.zexp where - -- zippered expressions - mutual - data -_⊢⇒_ : (Γ : Ctx) → (τ : Typ) → Set where - ⊢▹_◃ : ∀ {Γ : Ctx} {τ} - → (ě : Γ ⊢⇒ τ) - → - Γ ⊢⇒ τ - - ⊢λ₁_∶_∙_ : ∀ {Γ τ} - → (x : Var) - → (τ^ : ZTyp) - → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ) - → - Γ ⊢⇒ ((τ^ ◇τ) -→ τ) - - ⊢λ₂_∶_∙_ : ∀ {Γ τ′} - → (x : Var) - → (τ : Typ) - → (ê : - Γ , x ∶ τ ⊢⇒ τ′) - → - Γ ⊢⇒ (τ -→ τ′) - - ⊢_∙₁_[_] : ∀ {Γ τ τ₁ τ₂} - → (ê₁ : - Γ ⊢⇒ τ) - → (ě₂ : Γ ⊢⇐ τ₁) - → (τ▸ : τ ▸ τ₁ -→ τ₂) - → - Γ ⊢⇒ τ₂ - - ⊢_∙₂_[_] : ∀ {Γ τ τ₁ τ₂} - → (ě₁ : Γ ⊢⇒ τ) - → (ê₂ : - Γ ⊢⇐ τ₁) - → (τ▸ : τ ▸ τ₁ -→ τ₂) - → - Γ ⊢⇒ τ₂ - - ⊢⸨_⸩∙₁_[_] : ∀ {Γ τ} - → (ê₁ : - Γ ⊢⇒ τ) - → (ě₂ : Γ ⊢⇐ unknown) - → (τ!▸ : τ !▸-→) - → - Γ ⊢⇒ unknown - - ⊢⸨_⸩∙₂_[_] : ∀ {Γ τ} - → (ě₁ : Γ ⊢⇒ τ) - → (ê₂ : - Γ ⊢⇐ unknown) - → (τ!▸ : τ !▸-→) - → - Γ ⊢⇒ unknown - - ⊢_←₁_∙_ : ∀ {Γ τ₁ τ₂} - → (x : Var) - → (ê₁ : - Γ ⊢⇒ τ₁) - → (ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂) - → - Γ ⊢⇒ τ₂ - - ⊢_←₂_∙_ : ∀ {Γ τ₁ τ₂} - → (x : Var) - → (ě₁ : Γ ⊢⇒ τ₁) - → (ê₂ : - Γ , x ∶ τ₁ ⊢⇒ τ₂) - → - Γ ⊢⇒ τ₂ - - ⊢_+₁_ : ∀ {Γ} - → (ê₁ : - Γ ⊢⇐ num) - → (ě₂ : Γ ⊢⇐ num) - → - Γ ⊢⇒ num - - ⊢_+₂_ : ∀ {Γ} - → (ě₁ : Γ ⊢⇐ num) - → (ê₂ : - Γ ⊢⇐ num) - → - Γ ⊢⇒ num - - ⊢_∙₁_∙_[_] : ∀ {Γ τ₁ τ₂ τ} - → (ê₁ : - Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇒ τ₁) - → (ě₃ : Γ ⊢⇒ τ₂) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) - → - Γ ⊢⇒ τ - - ⊢_∙₂_∙_[_] : ∀ {Γ τ₁ τ₂ τ} - → (ě₁ : Γ ⊢⇐ bool) - → (ê₂ : - Γ ⊢⇒ τ₁) - → (ě₃ : Γ ⊢⇒ τ₂) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) - → - Γ ⊢⇒ τ - - ⊢_∙₃_∙_[_] : ∀ {Γ τ₁ τ₂ τ} - → (ě₁ : Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇒ τ₁) - → (ê₃ : - Γ ⊢⇒ τ₂) - → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) - → - Γ ⊢⇒ τ - - ⊢⦉_∙₁_∙_⦊[_] : ∀ {Γ τ₁ τ₂} - → (ê₁ : - Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇒ τ₁) - → (ě₃ : Γ ⊢⇒ τ₂) - → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) - → - Γ ⊢⇒ unknown - - ⊢⦉_∙₂_∙_⦊[_] : ∀ {Γ τ₁ τ₂} - → (ě₁ : Γ ⊢⇐ bool) - → (ê₂ : - Γ ⊢⇒ τ₁) - → (ě₃ : Γ ⊢⇒ τ₂) - → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) - → - Γ ⊢⇒ unknown - - ⊢⦉_∙₃_∙_⦊[_] : ∀ {Γ τ₁ τ₂} - → (ě₁ : Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇒ τ₁) - → (ê₃ : - Γ ⊢⇒ τ₂) - → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) - → - Γ ⊢⇒ unknown - - data ZSubsumable : {Γ : Ctx} {τ : Typ} → (ê : - Γ ⊢⇒ τ) → Set where - ZSuCursor : ∀ {Γ τ} - → {ě : Γ ⊢⇒ τ} - → (su : MSubsumable ě) - → ZSubsumable {Γ} (⊢▹ ě ◃) - - ZSuZipApL1 : ∀ {Γ τ τ₁ τ₂} - → {ê₁ : - Γ ⊢⇒ τ} - → {ě₂ : Γ ⊢⇐ τ₁} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → ZSubsumable {Γ} (⊢ ê₁ ∙₁ ě₂ [ τ▸ ]) - - ZSuZipApR1 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {ê₂ : - Γ ⊢⇐ τ₁} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → ZSubsumable {Γ} (⊢ ě₁ ∙₂ ê₂ [ τ▸ ]) - - ZSuZipApL2 : ∀ {Γ τ} - → {ê₁ : - Γ ⊢⇒ τ} - → {ě₂ : Γ ⊢⇐ unknown} - → {τ!▸ : τ !▸-→} - → ZSubsumable {Γ} (⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ]) - - ZSuZipApR2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {ê₂ : - Γ ⊢⇐ unknown} - → {τ!▸ : τ !▸-→} - → ZSubsumable {Γ} (⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ]) - - ZSuPlus1 : ∀ {Γ} - → {ê₁ : - Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → ZSubsumable {Γ} (⊢ ê₁ +₁ ě₂) - - ZSuPlus2 : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ê₂ : - Γ ⊢⇐ num} - → ZSubsumable {Γ} (⊢ ě₁ +₂ ê₂) - - ZSuInconsistentBranchesC : ∀ {Γ τ₁ τ₂} - → {ê₁ : - Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ZSubsumable {Γ} (⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) - - ZSuInconsistentBranchesL : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ê₂ : - Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ZSubsumable {Γ} (⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) - - ZSuInconsistentBranchesR : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ê₃ : - Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → ZSubsumable {Γ} (⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ]) - - data -_⊢⇐_ : (Γ : Ctx) → (τ : Typ) → Set where - ⊢▹_◃ : ∀ {Γ : Ctx} {τ} - → (ě : Γ ⊢⇐ τ) - → - Γ ⊢⇐ τ - - ⊢λ₁_∶_∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} - → (x : Var) - → (τ^ : ZTyp) - → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂) - → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) - → (τ~τ₁ : (τ^ ◇τ) ~ τ₁) - → - Γ ⊢⇐ τ₃ - - ⊢λ₂_∶_∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} - → (x : Var) - → (τ : Typ) - → (ê : - Γ , x ∶ τ ⊢⇐ τ₂) - → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) - → (τ~τ₁ : τ ~ τ₁) - → - Γ ⊢⇐ τ₃ - - ⊢⸨λ₁_∶_∙_⸩[_] : ∀ {Γ τ′} - → (x : Var) - → (τ^ : ZTyp) - → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ unknown) - → (τ′!▸ : τ′ !▸-→) - → - Γ ⊢⇐ τ′ - - ⊢⸨λ₂_∶_∙_⸩[_] : ∀ {Γ τ′} - → (x : Var) - → (τ : Typ) - → (ê : - Γ , x ∶ τ ⊢⇐ unknown) - → (τ′!▸ : τ′ !▸-→) - → - Γ ⊢⇐ τ′ - - ⊢λ₁_∶⸨_⸩∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} - → (x : Var) - → (τ^ : ZTyp) - → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂) - → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) - → (τ~̸τ₁ : (τ^ ◇τ) ~̸ τ₁) - → - Γ ⊢⇐ τ₃ - - ⊢λ₂_∶⸨_⸩∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} - → (x : Var) - → (τ : Typ) - → (ê : - Γ , x ∶ τ ⊢⇐ τ₂) - → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) - → (τ~̸τ₁ : τ ~̸ τ₁) - → - Γ ⊢⇐ τ₃ - - ⊢_←₁_∙_ : ∀ {Γ τ₁ τ₂} - → (x : Var) - → (ê₁ : - Γ ⊢⇒ τ₁) - → (ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂) - → - Γ ⊢⇐ τ₂ - - ⊢_←₂_∙_ : ∀ {Γ τ₁ τ₂} - → (x : Var) - → (ě₁ : Γ ⊢⇒ τ₁) - → (ê₂ : - Γ , x ∶ τ₁ ⊢⇐ τ₂) - → - Γ ⊢⇐ τ₂ - - ⊢_∙₁_∙_ : ∀ {Γ τ} - → (ê₁ : - Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇐ τ) - → (ě₃ : Γ ⊢⇐ τ) - → - Γ ⊢⇐ τ - - ⊢_∙₂_∙_ : ∀ {Γ τ} - → (ě₁ : Γ ⊢⇐ bool) - → (ê₂ : - Γ ⊢⇐ τ) - → (ě₃ : Γ ⊢⇐ τ) - → - Γ ⊢⇐ τ - - ⊢_∙₃_∙_ : ∀ {Γ τ} - → (ě₁ : Γ ⊢⇐ bool) - → (ě₂ : Γ ⊢⇐ τ) - → (ê₃ : - Γ ⊢⇐ τ) - → - Γ ⊢⇐ τ - - ⊢⸨_⸩[_∙_] : ∀ {Γ τ τ′} - → (ê : - Γ ⊢⇒ τ′) - → (τ~̸τ′ : τ ~̸ τ′) - → (zsu : ZSubsumable ê) - → - Γ ⊢⇐ τ - - ⊢∙_[_∙_] : ∀ {Γ τ τ′} - → (ê : - Γ ⊢⇒ τ′) - → (τ~τ′ : τ ~ τ′) - → (zsu : ZSubsumable ê) - → - Γ ⊢⇐ τ - - -- well-formedness judgments - mutual - data _WF⇒ : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Set where - WFCursor : ∀ {Γ : Ctx} {τ} - → {ě : Γ ⊢⇒ τ} - → ⊢▹ ě ◃ WF⇒ - - WFLamT : ∀ {Γ x τ} - → {τ^ : ZTyp} - → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ} - → (⊢λ₁ x ∶ τ^ ∙ ě) WF⇒ - - WFLamE : ∀ {Γ x τ′} - → {τ : Typ} - → {ê : - Γ , x ∶ τ ⊢⇒ τ′} - → (wf : ê WF⇒) - → (⊢λ₂ x ∶ τ ∙ ê) WF⇒ - - WFApL1 : ∀ {Γ τ τ₁ τ₂} - → {ê₁ : - Γ ⊢⇒ τ} - → {ě₂ : Γ ⊢⇐ τ₁} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → (wf : ê₁ WF⇒) - → ⊢ ê₁ ∙₁ ě₂ [ τ▸ ] WF⇒ - - WFApR1 : ∀ {Γ τ τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ} - → {ê₂ : - Γ ⊢⇐ τ₁} - → {τ▸ : τ ▸ τ₁ -→ τ₂} - → (wf : ê₂ WF⇐) - → ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] WF⇒ - - WFApL2 : ∀ {Γ τ} - → {ê₁ : - Γ ⊢⇒ τ} - → {ě₂ : Γ ⊢⇐ unknown} - → {τ!▸ : τ !▸-→} - → (wf : ê₁ WF⇒) - → ⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ] WF⇒ - - WFApR2 : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇒ τ} - → {ê₂ : - Γ ⊢⇐ unknown} - → {τ!▸ : τ !▸-→} - → (wf : ê₂ WF⇐) - → ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] WF⇒ - - WFLetL : ∀ {Γ x τ₁ τ₂} - → {ê₁ : - Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} - → (wf : ê₁ WF⇒) - → (⊢ x ←₁ ê₁ ∙ ě₂) WF⇒ - - WFLetR : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ê₂ : - Γ , x ∶ τ₁ ⊢⇒ τ₂} - → (wf : ê₂ WF⇒) - → (⊢ x ←₂ ě₁ ∙ ê₂) WF⇒ - - WFPlusL : ∀ {Γ} - → {ê₁ : - Γ ⊢⇐ num} - → {ě₂ : Γ ⊢⇐ num} - → (wf : ê₁ WF⇐) - → (⊢ ê₁ +₁ ě₂) WF⇒ - - WFPlusR : ∀ {Γ} - → {ě₁ : Γ ⊢⇐ num} - → {ê₂ : - Γ ⊢⇐ num} - → (wf : ê₂ WF⇐) - → (⊢ ě₁ +₂ ê₂) WF⇒ - - WFIfC : ∀ {Γ τ₁ τ₂ τ} - → {ê₁ : - Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → (wf : ê₁ WF⇐) - → ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒ - - WFIfL : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ê₂ : - Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → (wf : ê₂ WF⇒) - → ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒ - - WFIfR : ∀ {Γ τ₁ τ₂ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ê₃ : - Γ ⊢⇒ τ₂} - → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} - → (wf : ê₃ WF⇒) - → ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] WF⇒ - - WFInconsistentBranchesC : ∀ {Γ τ₁ τ₂} - → {ê₁ : - Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → (wf : ê₁ WF⇐) - → ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒ - - WFInconsistentBranchesL : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ê₂ : - Γ ⊢⇒ τ₁} - → {ě₃ : Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → (wf : ê₂ WF⇒) - → ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒ - - WFInconsistentBranchesR : ∀ {Γ τ₁ τ₂} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇒ τ₁} - → {ê₃ : - Γ ⊢⇒ τ₂} - → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} - → (wf : ê₃ WF⇒) - → ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] WF⇒ - - data _WF⇐ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Set where - WFCursor : ∀ {Γ : Ctx} {τ} - → {ě : Γ ⊢⇐ τ} - → ⊢▹ ě ◃ WF⇐ - - WFLamT1 : ∀ {Γ x τ₁ τ₂ τ₃} - → {τ^ : ZTyp} - → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : (τ^ ◇τ) ~ τ₁} - → ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] WF⇐ - - WFLamE1 : ∀ {Γ x τ₁ τ₂ τ₃} - → {τ : Typ} - → {ê : - Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~τ₁ : τ ~ τ₁} - → (wf : ê WF⇐) - → ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] WF⇐ - - WFLamT2 : ∀ {Γ x τ′} - → {τ^ : ZTyp} - → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] WF⇐ - - WFLamE2 : ∀ {Γ x τ′} - → {τ : Typ} - → {ê : - Γ , x ∶ τ ⊢⇐ unknown} - → {τ′!▸ : τ′ !▸-→} - → (wf : ê WF⇐) - → ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] WF⇐ - - WFLamT3 : ∀ {Γ x τ₁ τ₂ τ₃} - → {τ^ : ZTyp} - → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : (τ^ ◇τ) ~̸ τ₁} - → ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐ - - WFLamE3 : ∀ {Γ x τ₁ τ₂ τ₃} - → {τ : Typ} - → {ê : - Γ , x ∶ τ ⊢⇐ τ₂} - → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} - → {τ~̸τ₁ : τ ~̸ τ₁} - → (wf : ê WF⇐) - → ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐ - - WFLetL : ∀ {Γ x τ₁ τ₂} - → {ê₁ : - Γ ⊢⇒ τ₁} - → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} - → (wf : ê₁ WF⇒) - → (⊢ x ←₁ ê₁ ∙ ě₂) WF⇐ - - WFLetR : ∀ {Γ x τ₁ τ₂} - → {ě₁ : Γ ⊢⇒ τ₁} - → {ê₂ : - Γ , x ∶ τ₁ ⊢⇐ τ₂} - → (wf : ê₂ WF⇐) - → (⊢ x ←₂ ě₁ ∙ ê₂) WF⇐ - - WFIfC : ∀ {Γ τ} - → {ê₁ : - Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → (wf : ê₁ WF⇐) - → (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) WF⇐ - - WFIfL : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ê₂ : - Γ ⊢⇐ τ} - → {ě₃ : Γ ⊢⇐ τ} - → (wf : ê₂ WF⇐) - → (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) WF⇐ - - WFIfR : ∀ {Γ τ} - → {ě₁ : Γ ⊢⇐ bool} - → {ě₂ : Γ ⊢⇐ τ} - → {ê₃ : - Γ ⊢⇐ τ} - → (wf : ê₃ WF⇐) - → (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) WF⇐ - - WFInconsistentTypes : ∀ {Γ τ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {τ~̸τ′ : τ ~̸ τ′} - → {zsu : ZSubsumable ê} - → (wf : ê WF⇒) - → (nc : ¬ (∃[ ě ] ê ≡ ⊢▹ ě ◃)) - → ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] WF⇐ - - WFSubsume : ∀ {Γ τ τ′} - → {ê : - Γ ⊢⇒ τ′} - → {τ~τ′ : τ ~ τ′} - → {zsu : ZSubsumable ê} - → (wf : ê WF⇒) - → ⊢∙ ê [ τ~τ′ ∙ zsu ] WF⇐ - - -- well-formedness decidability - is-cursor? : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Dec (∃[ ě ] ê ≡ ⊢▹ ě ◃) - is-cursor? ⊢▹ ě ◃ = yes ⟨ ě , refl ⟩ - is-cursor? (⊢λ₁ x ∶ τ^ ∙ ě) = no λ() - is-cursor? (⊢λ₂ x ∶ τ ∙ ê) = no λ() - is-cursor? ⊢ ê ∙₁ ě₂ [ τ▸ ] = no λ() - is-cursor? ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] = no λ() - is-cursor? ⊢⸨ ê ⸩∙₁ ě₂ [ τ!▸ ] = no λ() - is-cursor? ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] = no λ() - is-cursor? (⊢ x ←₁ ê ∙ ě₂) = no λ() - is-cursor? (⊢ x ←₂ ě₁ ∙ ê₂) = no λ() - is-cursor? (⊢ ê₁ +₁ ě₂) = no λ() - is-cursor? (⊢ ě₁ +₂ ê₂) = no λ() - is-cursor? ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] = no λ() - is-cursor? ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] = no λ() - is-cursor? ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] = no λ() - is-cursor? ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] = no λ() - is-cursor? ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] = no λ() - is-cursor? ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] = no λ() - - mutual - _WF⇒? : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Dec (ê WF⇒) - ⊢▹ ě ◃ WF⇒? = yes WFCursor - (⊢λ₁ x ∶ τ^ ∙ ě) WF⇒? = yes WFLamT - (⊢λ₂ x ∶ τ ∙ ê) WF⇒? - with ê WF⇒? - ... | yes wf = yes (WFLamE wf) - ... | no !wf = no λ { (WFLamE wf) → !wf wf } - ⊢ ê₁ ∙₁ ě₂ [ τ▸ ] WF⇒? - with ê₁ WF⇒? - ... | yes wf = yes (WFApL1 wf) - ... | no !wf = no λ { (WFApL1 wf) → !wf wf } - ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] WF⇒? - with ê₂ WF⇐? - ... | yes wf = yes (WFApR1 wf) - ... | no !wf = no λ { (WFApR1 wf) → !wf wf } - ⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ] WF⇒? - with ê₁ WF⇒? - ... | yes wf = yes (WFApL2 wf) - ... | no !wf = no λ { (WFApL2 wf) → !wf wf } - ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] WF⇒? - with ê₂ WF⇐? - ... | yes wf = yes (WFApR2 wf) - ... | no !wf = no λ { (WFApR2 wf) → !wf wf } - (⊢ x ←₁ ê₁ ∙ ě₂) WF⇒? - with ê₁ WF⇒? - ... | yes wf = yes (WFLetL wf) - ... | no !wf = no λ { (WFLetL wf) → !wf wf } - (⊢ x ←₂ ě₁ ∙ ê₂) WF⇒? - with ê₂ WF⇒? - ... | yes wf = yes (WFLetR wf) - ... | no !wf = no λ { (WFLetR wf) → !wf wf } - (⊢ ê₁ +₁ ě₂) WF⇒? - with ê₁ WF⇐? - ... | yes wf = yes (WFPlusL wf) - ... | no !wf = no λ { (WFPlusL wf) → !wf wf } - (⊢ ě₁ +₂ ê₂) WF⇒? - with ê₂ WF⇐? - ... | yes wf = yes (WFPlusR wf) - ... | no !wf = no λ { (WFPlusR wf) → !wf wf } - ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒? - with ê₁ WF⇐? - ... | yes wf = yes (WFIfC wf) - ... | no !wf = no λ { (WFIfC wf) → !wf wf } - ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒? - with ê₂ WF⇒? - ... | yes wf = yes (WFIfL wf) - ... | no !wf = no λ { (WFIfL wf) → !wf wf } - ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] WF⇒? - with ê₃ WF⇒? - ... | yes wf = yes (WFIfR wf) - ... | no !wf = no λ { (WFIfR wf) → !wf wf } - ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒? - with ê₁ WF⇐? - ... | yes wf = yes (WFInconsistentBranchesC wf) - ... | no !wf = no λ { (WFInconsistentBranchesC wf) → !wf wf } - ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒? - with ê₂ WF⇒? - ... | yes wf = yes (WFInconsistentBranchesL wf) - ... | no !wf = no λ { (WFInconsistentBranchesL wf) → !wf wf } - ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] WF⇒? - with ê₃ WF⇒? - ... | yes wf = yes (WFInconsistentBranchesR wf) - ... | no !wf = no λ { (WFInconsistentBranchesR wf) → !wf wf } - - _WF⇐? : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Dec (ê WF⇐) - ⊢▹ ě ◃ WF⇐? = yes WFCursor - ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] WF⇐? = yes WFLamT1 - ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] WF⇐? - with ê WF⇐? - ... | yes wf = yes (WFLamE1 wf) - ... | no !wf = no λ { (WFLamE1 wf) → !wf wf } - ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] WF⇐? = yes WFLamT2 - ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] WF⇐? - with ê WF⇐? - ... | yes wf = yes (WFLamE2 wf) - ... | no !wf = no λ { (WFLamE2 wf) → !wf wf } - ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐? = yes WFLamT3 - ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐? - with ê WF⇐? - ... | yes wf = yes (WFLamE3 wf) - ... | no !wf = no λ { (WFLamE3 wf) → !wf wf } - (⊢ x ←₁ ê₁ ∙ ě₂) WF⇐? - with ê₁ WF⇒? - ... | yes wf = yes (WFLetL wf) - ... | no !wf = no λ { (WFLetL wf) → !wf wf } - (⊢ x ←₂ ě₁ ∙ ê₂) WF⇐? - with ê₂ WF⇐? - ... | yes wf = yes (WFLetR wf) - ... | no !wf = no λ { (WFLetR wf) → !wf wf } - (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) WF⇐? - with ê₁ WF⇐? - ... | yes wf = yes (WFIfC wf) - ... | no !wf = no λ { (WFIfC wf) → !wf wf } - (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) WF⇐? - with ê₂ WF⇐? - ... | yes wf = yes (WFIfL wf) - ... | no !wf = no λ { (WFIfL wf) → !wf wf } - (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) WF⇐? - with ê₃ WF⇐? - ... | yes wf = yes (WFIfR wf) - ... | no !wf = no λ { (WFIfR wf) → !wf wf } - ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] WF⇐? - with ê WF⇒? - ... | no !wf = no λ { (WFInconsistentTypes wf nc) → !wf wf } - ... | yes wf with is-cursor? ê - ... | yes ic = no λ { (WFInconsistentTypes wf nc) → nc ic } - ... | no nc = yes (WFInconsistentTypes wf nc) - ⊢∙ ê [ τ~τ′ ∙ zsu ] WF⇐? - with ê WF⇒? - ... | yes wf = yes (WFSubsume wf) - ... | no !wf = no λ { (WFSubsume wf) → !wf wf } - - -- functional cursor erasure - mutual - _◇⇒ : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Γ ⊢⇒ τ - ⊢▹ ě ◃ ◇⇒ = ě - (⊢λ₁ x ∶ τ^ ∙ ě) ◇⇒ = ⊢λ x ∶ (τ^ ◇τ) ∙ ě - (⊢λ₂ x ∶ τ ∙ ê) ◇⇒ = ⊢λ x ∶ τ ∙ (ê ◇⇒) - (⊢ ê ∙₁ ě [ τ▸ ]) ◇⇒ = ⊢ (ê ◇⇒) ∙ ě [ τ▸ ] - (⊢ ě ∙₂ ê [ τ▸ ]) ◇⇒ = ⊢ ě ∙ (ê ◇⇐) [ τ▸ ] - (⊢⸨ ê ⸩∙₁ ě [ τ!▸ ]) ◇⇒ = ⊢⸨ (ê ◇⇒) ⸩∙ ě [ τ!▸ ] - (⊢⸨ ě ⸩∙₂ ê [ τ!▸ ]) ◇⇒ = ⊢⸨ ě ⸩∙ (ê ◇⇐) [ τ!▸ ] - (⊢ x ←₁ ê ∙ ě) ◇⇒ = ⊢ x ← (ê ◇⇒) ∙ ě - (⊢ x ←₂ ě ∙ ê) ◇⇒ = ⊢ x ← ě ∙ (ê ◇⇒) - (⊢ ê +₁ ě) ◇⇒ = ⊢ (ê ◇⇐) + ě - (⊢ ě +₂ ê) ◇⇒ = ⊢ ě + (ê ◇⇐) - (⊢ ê ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ (ê ◇⇐) ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] - (⊢ ě₁ ∙₂ ê ∙ ě₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ ě₁ ∙ (ê ◇⇒) ∙ ě₃ [ τ₁⊔τ₂ ] - (⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇒) [ τ₁⊔τ₂ ] - (⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ (ê₁ ◇⇐) ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] - (⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ ě₁ ∙ (ê₂ ◇⇒) ∙ ě₃ ⦊[ τ₁~̸τ₂ ] - (⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇒) ⦊[ τ₁~̸τ₂ ] - - ZSu→MSu : ∀ {Γ τ} {ê : - Γ ⊢⇒ τ} → (zsu : ZSubsumable ê) → MSubsumable (ê ◇⇒) - ZSu→MSu (ZSuCursor su) = su - ZSu→MSu ZSuZipApL1 = MSuAp1 - ZSu→MSu ZSuZipApR1 = MSuAp1 - ZSu→MSu ZSuZipApL2 = MSuAp2 - ZSu→MSu ZSuZipApR2 = MSuAp2 - ZSu→MSu ZSuPlus1 = MSuPlus - ZSu→MSu ZSuPlus2 = MSuPlus - ZSu→MSu ZSuInconsistentBranchesC = MSuInconsistentBranches - ZSu→MSu ZSuInconsistentBranchesL = MSuInconsistentBranches - ZSu→MSu ZSuInconsistentBranchesR = MSuInconsistentBranches - - _◇⇐ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Γ ⊢⇐ τ - ⊢▹ ě ◃ ◇⇐ = ě - ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◇⇐ = ⊢λ x ∶ (τ^ ◇τ) ∙ ě [ τ₃▸ ∙ τ~τ₁ ] - ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] ◇⇐ = ⊢λ x ∶ τ ∙ (ê ◇⇐) [ τ₃▸ ∙ τ~τ₁ ] - ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] ◇⇐ = ⊢⸨λ x ∶ (τ^ ◇τ) ∙ ě ⸩[ τ′!▸ ] - ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] ◇⇐ = ⊢⸨λ x ∶ τ ∙ (ê ◇⇐) ⸩[ τ′!▸ ] - ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◇⇐ = ⊢λ x ∶⸨ τ^ ◇τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] - ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] ◇⇐ = ⊢λ x ∶⸨ τ ⸩∙ (ê ◇⇐) [ τ₃▸ ∙ τ~̸τ₁ ] - (⊢ x ←₁ ê₁ ∙ ě₂) ◇⇐ = ⊢ x ← (ê₁ ◇⇒) ∙ ě₂ - (⊢ x ←₂ ě₁ ∙ ê₂) ◇⇐ = ⊢ x ← ě₁ ∙ (ê₂ ◇⇐) - (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) ◇⇐ = ⊢ (ê₁ ◇⇐) ∙ ě₂ ∙ ě₃ - (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) ◇⇐ = ⊢ ě₁ ∙ (ê₂ ◇⇐) ∙ ě₃ - (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) ◇⇐ = ⊢ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇐) - ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] ◇⇐ = ⊢⸨ ê ◇⇒ ⸩[ τ~̸τ′ ∙ (ZSu→MSu zsu) ] - ⊢∙ ê [ τ~τ′ ∙ zsu ] ◇⇐ = ⊢∙ (ê ◇⇒) [ τ~τ′ ∙ (ZSu→MSu zsu) ] - - ◇≡-⊢⇒ : ∀ {Γ x τ^ τ^′ τ} → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ) → (τ^ ◇τ) ≡ (τ^′ ◇τ) → Σ[ ě′ ∈ Γ , x ∶ (τ^′ ◇τ) ⊢⇒ τ ] (ě ⇒□) ≡ (ě′ ⇒□) - ◇≡-⊢⇒ ě eq rewrite eq = ⟨ ě , refl ⟩ diff --git a/hazelnut/typed/ztyp.agda b/hazelnut/typed/ztyp.agda deleted file mode 100644 index b3eda74..0000000 --- a/hazelnut/typed/ztyp.agda +++ /dev/null @@ -1,32 +0,0 @@ -open import prelude -open import core - --- zippered types -module hazelnut.typed.ztyp where - data ZTyp : Set where - ▹_◃ : (τ : Typ) → ZTyp - _-→₁_ : (τ^ : ZTyp) → (τ : Typ) → ZTyp - _-→₂_ : (τ : Typ) → (τ^ : ZTyp) → ZTyp - - infixr 25 _-→₁_ - infixr 25 _-→₂_ - - -- judgmental cursor erasure - data erase-τ : (τ^ : ZTyp) → (τ : Typ) → Set where - ETTop : ∀ {τ} → erase-τ (▹ τ ◃) τ - ETArr1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂) - ETArr2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂) - - -- functional cursor erasure - _◇τ : (τ^ : ZTyp) → Typ - ▹ τ ◃ ◇τ = τ - (τ^ -→₁ τ) ◇τ = (τ^ ◇τ) -→ τ - (τ -→₂ τ^) ◇τ = τ -→ (τ^ ◇τ) - - -- convert judgmental cursor erasure to functional cursor erasure - erase-τ→◇ : ∀ {τ^ τ} → erase-τ τ^ τ → τ^ ◇τ ≡ τ - erase-τ→◇ ETTop = refl - erase-τ→◇ (ETArr1 τ₁^◇) - rewrite erase-τ→◇ τ₁^◇ = refl - erase-τ→◇ (ETArr2 τ₂^◇) - rewrite erase-τ→◇ τ₂^◇ = refl From 739b74aaadf8522c2b1d2d3486cefdb991842c3a Mon Sep 17 00:00:00 2001 From: Eric Zhao <21zhaoe@protonmail.com> Date: Fri, 9 Jun 2023 07:27:50 +0900 Subject: [PATCH 2/2] agda: Add back wip typed hazelnut agda --- hazelnut.agda | 1 + hazelnut/typed.agda | 4 + hazelnut/typed/action.agda | 509 ++++++++++++++++++++++++++++ hazelnut/typed/zexp.agda | 666 +++++++++++++++++++++++++++++++++++++ hazelnut/typed/ztyp.agda | 32 ++ 5 files changed, 1212 insertions(+) create mode 100644 hazelnut/typed.agda create mode 100644 hazelnut/typed/action.agda create mode 100644 hazelnut/typed/zexp.agda create mode 100644 hazelnut/typed/ztyp.agda diff --git a/hazelnut.agda b/hazelnut.agda index ea6092b..9078b2f 100644 --- a/hazelnut.agda +++ b/hazelnut.agda @@ -1,3 +1,4 @@ module hazelnut where import hazelnut.action import hazelnut.untyped + import hazelnut.typed diff --git a/hazelnut/typed.agda b/hazelnut/typed.agda new file mode 100644 index 0000000..61841f9 --- /dev/null +++ b/hazelnut/typed.agda @@ -0,0 +1,4 @@ +module hazelnut.typed where + open import hazelnut.typed.ztyp public + open import hazelnut.typed.zexp public + open import hazelnut.typed.action public diff --git a/hazelnut/typed/action.agda b/hazelnut/typed/action.agda new file mode 100644 index 0000000..996fdf3 --- /dev/null +++ b/hazelnut/typed/action.agda @@ -0,0 +1,509 @@ +open import prelude +open import core +open import marking + +open import hazelnut.action +open import hazelnut.typed.ztyp +open import hazelnut.typed.zexp + +module hazelnut.typed.action where + -- type actions + data _~_~τ>_ : (τ : ZTyp) → (α : Action) → (τ′ : ZTyp) → Set where + -- movement + TMArrChild1 : ∀ {τ₁ τ₂ : Typ} + → ▹ τ₁ -→ τ₂ ◃ ~ move (child 1) ~τ> ▹ τ₁ ◃ -→₁ τ₂ + TMArrChild2 : ∀ {τ₁ τ₂ : Typ} + → ▹ τ₁ -→ τ₂ ◃ ~ move (child 2) ~τ> τ₁ -→₂ ▹ τ₂ ◃ + TMArrParent1 : ∀ {τ₁ τ₂ : Typ} + → ▹ τ₁ ◃ -→₁ τ₂ ~ move parent ~τ> ▹ τ₁ -→ τ₂ ◃ + TMArrParent2 : ∀ {τ₁ τ₂ : Typ} + → τ₁ -→₂ ▹ τ₂ ◃ ~ move parent ~τ> ▹ τ₁ -→ τ₂ ◃ + + -- deletion + TDel : ∀ {τ : Typ} {u : Hole} + → ▹ τ ◃ ~ (del u) ~τ> ▹ unknown ◃ + + -- construction + TConArrow1 : ∀ {τ : Typ} + → ▹ τ ◃ ~ construct tarrow₁ ~τ> τ -→₂ ▹ unknown ◃ + TConArrow2 : ∀ {τ : Typ} + → ▹ τ ◃ ~ construct tarrow₂ ~τ> ▹ unknown ◃ -→₁ τ + TConNum : ▹ unknown ◃ ~ construct tnum ~τ> ▹ num ◃ + TConBool : ▹ unknown ◃ ~ construct tbool ~τ> ▹ bool ◃ + + -- zipper + TZipArr1 : ∀ {τ^ τ^′ : ZTyp} {τ : Typ} {α : Action} + → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) + → τ^ -→₁ τ ~ α ~τ> τ^′ -→₁ τ + TZipArr2 : ∀ {τ^ τ^′ : ZTyp} {τ : Typ} {α : Action} + → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) + → τ -→₂ τ^ ~ α ~τ> τ -→₂ τ^′ + + -- iterated type actions + data _~_~τ>*_ : (τ^ : ZTyp) → (ᾱ : ActionList) → (τ^′ : ZTyp) → Set where + TIRefl : ∀ {τ^} + → τ^ ~ [] ~τ>* τ^ + TITyp : ∀ {τ^ τ^′ τ^″ α ᾱ} + → (τ^~>τ^′ : τ^ ~ α ~τ> τ^′) + → (τ^′~>*τ^″ : τ^′ ~ ᾱ ~τ>* τ^″) + → τ^ ~ α ∷ ᾱ ~τ>* τ^″ + + ~τ>*-++ : ∀ {τ^ τ^′ τ^″ ᾱ₁ ᾱ₂} → τ^ ~ ᾱ₁ ~τ>* τ^′ → τ^′ ~ ᾱ₂ ~τ>* τ^″ → τ^ ~ (ᾱ₁ ++ ᾱ₂) ~τ>* τ^″ + ~τ>*-++ TIRefl τ^~>*τ^″ = τ^~>*τ^″ + ~τ>*-++ (TITyp τ^~>τ^′ τ^′~>*τ^″) τ^″~>*τ^‴ = TITyp τ^~>τ^′ (~τ>*-++ τ^′~>*τ^″ τ^″~>*τ^‴) + + -- type zippers + ziplem-tarr1 : ∀ {τ^ τ^′ τ ᾱ} → τ^ ~ ᾱ ~τ>* τ^′ → (τ^ -→₁ τ) ~ ᾱ ~τ>* (τ^′ -→₁ τ) + ziplem-tarr1 TIRefl = TIRefl + ziplem-tarr1 (TITyp τ^~>τ^′ τ^′~>*τ^″) = TITyp (TZipArr1 τ^~>τ^′) (ziplem-tarr1 τ^′~>*τ^″) + + ziplem-tarr2 : ∀ {τ^ τ^′ τ ᾱ} → τ^ ~ ᾱ ~τ>* τ^′ → (τ -→₂ τ^) ~ ᾱ ~τ>* (τ -→₂ τ^′) + ziplem-tarr2 TIRefl = TIRefl + ziplem-tarr2 (TITyp τ^~>τ^′ τ^′~>*τ^″) = TITyp (TZipArr2 τ^~>τ^′) (ziplem-tarr2 τ^′~>*τ^″) + + mutual + -- synthetic expression movements + data _+_+⇒_ : ∀ {Γ τ τ′} → (ê : - Γ ⊢⇒ τ) → (δ : Dir) → (ê′ : - Γ ⊢⇒ τ′) → Set where + -- movement + ESMLamChild1 : ∀ {Γ x τ} + → {ě : Γ , x ∶ τ ⊢⇒ τ} + → ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + child 1 +⇒ (⊢λ₁ x ∶ ▹ τ ◃ ∙ ě) + ESMLamChild2 : ∀ {Γ x τ} + → {ě : Γ , x ∶ τ ⊢⇒ τ} + → ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + child 2 +⇒ (⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃) + ESMLamParent1 : ∀ {Γ x τ} + → {ě : Γ , x ∶ τ ⊢⇒ τ} + → (⊢λ₁ x ∶ ▹ τ ◃ ∙ ě) + parent +⇒ ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + ESMLamParent2 : ∀ {Γ x τ} + → {ě : Γ , x ∶ τ ⊢⇒ τ} + → (⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃) + parent +⇒ ⊢▹ ⊢λ x ∶ τ ∙ ě ◃ + + ESMAp1Child1 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → {ě₂ : Γ ⊢⇐ τ₁} + → ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + child 1 +⇒ ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ [ τ▸ ] + ESMAp1Child2 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → {ě₂ : Γ ⊢⇐ τ₁} + → ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + child 2 +⇒ ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ [ τ▸ ] + ESMAp1Parent1 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → {ě₂ : Γ ⊢⇐ τ₁} + → ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ [ τ▸ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + ESMAp1Parent2 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → {ě₂ : Γ ⊢⇐ τ₁} + → ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ [ τ▸ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ [ τ▸ ] ◃ + + ESMAp2Child1 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {τ!▸ : τ !▸-→} + → {ě₂ : Γ ⊢⇐ unknown} + → ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + child 1 +⇒ ⊢⸨ ⊢▹ ě₁ ◃ ⸩∙₁ ě₂ [ τ!▸ ] + ESMAp2Child2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {τ!▸ : τ !▸-→} + → {ě₂ : Γ ⊢⇐ unknown} + → ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + child 2 +⇒ ⊢⸨ ě₁ ⸩∙₂ ⊢▹ ě₂ ◃ [ τ!▸ ] + ESMAp2Parent1 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {τ!▸ : τ !▸-→} + → {ě₂ : Γ ⊢⇐ unknown} + → ⊢⸨ ⊢▹ ě₁ ◃ ⸩∙₁ ě₂ [ τ!▸ ] + parent +⇒ ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + ESMAp2Parent2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {τ!▸ : τ !▸-→} + → {ě₂ : Γ ⊢⇐ unknown} + → ⊢⸨ ě₁ ⸩∙₂ ⊢▹ ě₂ ◃ [ τ!▸ ] + parent +⇒ ⊢▹ ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ] ◃ + + ESMLetChild1 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} + → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 1 +⇒ (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + ESMLetChild2 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} + → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 2 +⇒ (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + ESMLetParent1 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} + → (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + parent +⇒ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + ESMLetParent2 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} + → (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + parent +⇒ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + + ESMPlusChild1 : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → ⊢▹ ⊢ ě₁ + ě₂ ◃ + child 1 +⇒ (⊢ ⊢▹ ě₁ ◃ +₁ ě₂) + ESMPlusChild2 : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → ⊢▹ ⊢ ě₁ + ě₂ ◃ + child 2 +⇒ (⊢ ě₁ +₂ ⊢▹ ě₂ ◃) + ESMPlusParent1 : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → (⊢ ⊢▹ ě₁ ◃ +₁ ě₂) + parent +⇒ ⊢▹ ⊢ ě₁ + ě₂ ◃ + ESMPlusParent2 : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → (⊢ ě₁ +₂ ⊢▹ ě₂ ◃) + parent +⇒ ⊢▹ ⊢ ě₁ + ě₂ ◃ + + ESMIfChild1 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 1 +⇒ ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + ESMIfChild2 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 2 +⇒ ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ [ τ₁⊔τ₂ ] + ESMIfChild3 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + child 3 +⇒ ⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ [ τ₁⊔τ₂ ] + ESMIfParent1 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + ESMIfParent2 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + ESMIfParent3 : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → ⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ [ τ₁⊔τ₂ ] + parent +⇒ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] ◃ + + ESMInconsistentBranchesChild1 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 1 +⇒ ⊢⦉ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + ESMInconsistentBranchesChild2 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 2 +⇒ ⊢⦉ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + ESMInconsistentBranchesChild3 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + child 3 +⇒ ⊢⦉ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ ⦊[ τ₁~̸τ₂ ] + ESMInconsistentBranchesParent1 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢⦉ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + ESMInconsistentBranchesParent2 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢⦉ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + ESMInconsistentBranchesParent3 : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ⊢⦉ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃ ⦊[ τ₁~̸τ₂ ] + parent +⇒ ⊢▹ ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] ◃ + + MSu-+⇒ : ∀ {Γ τ} {ě : Γ ⊢⇒ τ} {n : ℕ} {ê : - Γ ⊢⇒ τ} → MSubsumable ě → ⊢▹ ě ◃ + child n +⇒ ê → ZSubsumable ê + MSu-+⇒ MSuAp1 ESMAp1Child1 = ZSuZipApL1 + MSu-+⇒ MSuAp1 ESMAp1Child2 = ZSuZipApR1 + MSu-+⇒ MSuAp2 ESMAp2Child1 = ZSuZipApL2 + MSu-+⇒ MSuAp2 ESMAp2Child2 = ZSuZipApR2 + MSu-+⇒ MSuPlus ESMPlusChild1 = ZSuPlus1 + MSu-+⇒ MSuPlus ESMPlusChild2 = ZSuPlus2 + MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild1 = ZSuInconsistentBranchesC + MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild2 = ZSuInconsistentBranchesL + MSu-+⇒ MSuInconsistentBranches ESMInconsistentBranchesChild3 = ZSuInconsistentBranchesR + + ZSu-+⇒ : ∀ {Γ τ} {ê : - Γ ⊢⇒ τ} {ě : Γ ⊢⇒ τ} → ZSubsumable ê → ê + parent +⇒ ⊢▹ ě ◃ → MSubsumable ě + ZSu-+⇒ ZSuZipApL1 ESMAp1Parent1 = MSuAp1 + ZSu-+⇒ ZSuZipApR1 ESMAp1Parent2 = MSuAp1 + ZSu-+⇒ ZSuZipApL2 ESMAp2Parent1 = MSuAp2 + ZSu-+⇒ ZSuZipApR2 ESMAp2Parent2 = MSuAp2 + ZSu-+⇒ ZSuPlus1 ESMPlusParent1 = MSuPlus + ZSu-+⇒ ZSuPlus2 ESMPlusParent2 = MSuPlus + ZSu-+⇒ ZSuInconsistentBranchesC ESMInconsistentBranchesParent1 = MSuInconsistentBranches + ZSu-+⇒ ZSuInconsistentBranchesL ESMInconsistentBranchesParent2 = MSuInconsistentBranches + ZSu-+⇒ ZSuInconsistentBranchesR ESMInconsistentBranchesParent3 = MSuInconsistentBranches + + -- analytic expression movements + data _+_+⇐_ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → (δ : Dir) → (ê′ : - Γ ⊢⇐ τ) → Set where + EAMLam1Child1 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : τ ~ τ₁} + → ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + child 1 +⇐ ⊢λ₁ x ∶ ▹ τ ◃ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] + EAMLam1Child2 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : τ ~ τ₁} + → ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + child 2 +⇐ ⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~τ₁ ] + EAMLam1Parent1 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : τ ~ τ₁} + → ⊢λ₁ x ∶ ▹ τ ◃ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + EAMLam1Parent2 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : τ ~ τ₁} + → ⊢λ₂ x ∶ τ ∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◃ + + EAMLam2Child1 : ∀ {Γ x τ τ′} + → {ě : Γ , x ∶ τ ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + child 1 +⇐ ⊢⸨λ₁ x ∶ ▹ τ ◃ ∙ ě ⸩[ τ′!▸ ] + EAMLam2Child2 : ∀ {Γ x τ τ′} + → {ě : Γ , x ∶ τ ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + child 2 +⇐ ⊢⸨λ₂ x ∶ τ ∙ ⊢▹ ě ◃ ⸩[ τ′!▸ ] + EAMLam2Parent1 : ∀ {Γ x τ τ′} + → {ě : Γ , x ∶ τ ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → ⊢⸨λ₁ x ∶ ▹ τ ◃ ∙ ě ⸩[ τ′!▸ ] + parent +⇐ ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + EAMLam2Parent2 : ∀ {Γ x τ τ′} + → {ě : Γ , x ∶ τ ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → ⊢⸨λ₂ x ∶ τ ∙ ⊢▹ ě ◃ ⸩[ τ′!▸ ] + parent +⇐ ⊢▹ ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ] ◃ + + EAMLam3Child1 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : τ ~̸ τ₁} + → ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + child 1 +⇐ ⊢λ₁ x ∶⸨ ▹ τ ◃ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] + EAMLam3Child2 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : τ ~̸ τ₁} + → ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + child 2 +⇐ ⊢λ₂ x ∶⸨ τ ⸩∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~̸τ₁ ] + EAMLam3Parent1 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : τ ~̸ τ₁} + → ⊢λ₁ x ∶⸨ ▹ τ ◃ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + EAMLam3Parent2 : ∀ {Γ x τ τ₁ τ₂ τ₃} + → {ě : Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : τ ~̸ τ₁} + → ⊢λ₂ x ∶⸨ τ ⸩∙ ⊢▹ ě ◃ [ τ₃▸ ∙ τ~̸τ₁ ] + parent +⇐ ⊢▹ ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◃ + + EAMLetChild1 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} + → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 1 +⇐ (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + EAMLetChild2 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} + → ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + child 2 +⇐ (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + EAMLetParent1 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} + → (⊢ x ←₁ ⊢▹ ě₁ ◃ ∙ ě₂) + parent +⇐ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + EAMLetParent2 : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} + → (⊢ x ←₂ ě₁ ∙ ⊢▹ ě₂ ◃) + parent +⇐ ⊢▹ ⊢ x ← ě₁ ∙ ě₂ ◃ + + EAMIfChild1 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 1 +⇐ (⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃) + EAMIfChild2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 2 +⇐ (⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃) + EAMIfChild3 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + child 3 +⇐ (⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃) + EAMIfParent1 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → (⊢ ⊢▹ ě₁ ◃ ∙₁ ě₂ ∙ ě₃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + EAMIfParent2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → (⊢ ě₁ ∙₂ ⊢▹ ě₂ ◃ ∙ ě₃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + EAMIfParent3 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → (⊢ ě₁ ∙₃ ě₂ ∙ ⊢▹ ě₃ ◃) + parent +⇐ ⊢▹ ⊢ ě₁ ∙ ě₂ ∙ ě₃ ◃ + + EAMInconsistentTypesChild : ∀ {Γ τ τ′ n} + → {ě : Γ ⊢⇒ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {+⇒ê : ⊢▹ ě ◃ + child n +⇒ ê} + → {τ~̸τ′ : τ ~̸ τ′} + → {su : MSubsumable ě} + → ⊢▹ ⊢⸨ ě ⸩[ τ~̸τ′ ∙ su ] ◃ + child n +⇐ ⊢⸨ ê ⸩[ τ~̸τ′ ∙ MSu-+⇒ su +⇒ê ] + EAMInconsistentTypesParent : ∀ {Γ τ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {ě : Γ ⊢⇒ τ′} + → {ê+⇒ : ê + parent +⇒ ⊢▹ ě ◃} + → {τ~̸τ′ : τ ~̸ τ′} + → {zsu : ZSubsumable ê} + → ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] + parent +⇐ ⊢▹ ⊢⸨ ě ⸩[ τ~̸τ′ ∙ ZSu-+⇒ zsu ê+⇒ ] ◃ + + EAMSubsumeChild : ∀ {Γ τ τ′ n} + → {ě : Γ ⊢⇒ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {+⇒ê : ⊢▹ ě ◃ + child n +⇒ ê} + → {τ~τ′ : τ ~ τ′} + → {su : MSubsumable ě} + → ⊢▹ ⊢∙ ě [ τ~τ′ ∙ su ] ◃ + child n +⇐ ⊢∙ ê [ τ~τ′ ∙ MSu-+⇒ su +⇒ê ] + EAMSubsumeParent : ∀ {Γ τ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {ě : Γ ⊢⇒ τ′} + → {ê+⇒ : ê + parent +⇒ ⊢▹ ě ◃} + → {τ~τ′ : τ ~ τ′} + → {zsu : ZSubsumable ê} + → ⊢∙ ê [ τ~τ′ ∙ zsu ] + parent +⇐ ⊢▹ ⊢∙ ě [ τ~τ′ ∙ ZSu-+⇒ zsu ê+⇒ ] ◃ + + mutual + -- synthetic expression actions + data _⊢_~_~⇒_ : ∀ {τ τ′ : Typ} → (Γ : Ctx) → (ê : - Γ ⊢⇒ τ) → (α : Action) → (ê : - Γ ⊢⇒ τ′) → Set where + -- movement + ESMove : ∀ {Γ τ δ} + → {ê : - Γ ⊢⇒ τ} + → {ê′ : - Γ ⊢⇒ τ} + → {ê+⇒ê′ : ê + δ +⇒ ê′} + → Γ ⊢ ê ~ move δ ~⇒ ê′ + + -- deletion + ESDel : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ del u ~⇒ ⊢▹ ⊢⦇-⦈^ u ◃ + + -- construction + ESConBoundVar : ∀ {Γ u τ x} + → (∋x : Γ ∋ x ∶ τ) + → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (var x) ~⇒ ⊢▹ ⊢ ∋x ◃ + ESConUnboundVar : ∀ {Γ u y} + → (∌y : Γ ∌ y) + → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (var y) ~⇒ ⊢▹ ⊢⟦ ∌y ⟧ ◃ + ESConLam : ∀ {Γ τ x τ′} + → {ě : Γ ⊢⇒ τ} + → {ě′ : Γ , x ∶ unknown ⊢⇒ τ′} + → (↬⇒ě′ : Γ , x ∶ unknown ⊢ (ě ⇒□) ↬⇒ ě′) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (lam x) ~⇒ (⊢λ₁ x ∶ ▹ unknown ◃ ∙ ě′) + ESConApL1 : ∀ {Γ τ τ₁ τ₂ u} + → {ě : Γ ⊢⇒ τ} + → (τ▸ : τ ▸ τ₁ -→ τ₂) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₁ u) ~⇒ ⊢ ě ∙₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) [ τ▸ ] + ESConApL2 : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → (τ!▸ : τ !▸-→) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₁ u) ~⇒ ⊢⸨ ě ⸩∙₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) [ τ!▸ ] + ESConApR : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ construct (ap₂ u) ~⇒ ⊢ (⊢▹ ⊢⦇-⦈^ u ◃) ∙₁ (proj₁ (⊢⇒-⊢⇐ ě)) [ TMAUnknown ] + ESConLet1 : ∀ {Γ τ x u} + → {ě : Γ ⊢⇒ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ construct (let₁ x u) ~⇒ (⊢ x ←₂ ě ∙ ⊢▹ ⊢⦇-⦈^ u ◃) + ESConLet2 : ∀ {Γ τ x u τ′} + → {ě : Γ ⊢⇒ τ} + → {ě′ : Γ , x ∶ unknown ⊢⇒ τ′} + → (↬⇒ě′ : Γ , x ∶ unknown ⊢ (ě ⇒□) ↬⇒ ě′) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (let₂ x u) ~⇒ (⊢ x ←₁ ⊢▹ ⊢⦇-⦈^ u ◃ ∙ ě′) + ESConNum : ∀ {Γ u n} + → Γ ⊢ ⊢▹ ⊢⦇-⦈^ u ◃ ~ construct (num n) ~⇒ ⊢▹ ⊢ℕ n ◃ + ESConPlusL1 : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → (τ~num : τ ~ num) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₁ u) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) +₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃)) + ESConPlusL2 : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → (τ~̸num : τ ~̸ num) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₁ u) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) +₂ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃)) + ESConPlusR1 : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → (τ~num : τ ~ num) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₂ u) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) +₁ (proj₁ (⊢⇒-⊢⇐ ě))) + ESConPlusR2 : ∀ {Γ τ u} + → {ě : Γ ⊢⇒ τ} + → (τ~̸num : τ ~̸ num) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (plus₂ u) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃) +₁ (proj₁ (⊢⇒-⊢⇐ ě))) + ESConIfC1 : ∀ {Γ τ u₁ u₂} + → {ě : Γ ⊢⇒ τ} + → (τ~bool : τ ~ bool) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₁ u₁ u₂) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) ∙₂ (⊢▹ ⊢⦇-⦈^ u₁ ◃) ∙ (⊢⦇-⦈^ u₂) [ TJUnknown ]) + ESConIfC2 : ∀ {Γ τ u₁ u₂} + → {ě : Γ ⊢⇒ τ} + → (τ~̸bool : τ ~̸ bool) + → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₁ u₁ u₂) ~⇒ (⊢ (proj₁ (⊢⇒-⊢⇐ ě)) ∙₂ (⊢▹ ⊢⦇-⦈^ u₁ ◃) ∙ (⊢⦇-⦈^ u₂) [ TJUnknown ]) + ESConIfL : ∀ {Γ τ u₁ u₂} + → {ě : Γ ⊢⇒ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₂ u₁ u₂) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u₁ [ ~-unknown₂ ∙ MSuHole ] ◃) ∙₁ ě ∙ (⊢⦇-⦈^ u₂) [ ⊔-unknown₂ ]) + ESConIfR : ∀ {Γ τ u₁ u₂} + → {ě : Γ ⊢⇒ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ construct (if₃ u₁ u₂) ~⇒ (⊢ (⊢▹ ⊢∙ ⊢⦇-⦈^ u₁ [ ~-unknown₂ ∙ MSuHole ] ◃) ∙₁ (⊢⦇-⦈^ u₂) ∙ ě [ ⊔-unknown₁ ]) + + -- zipper cases + ESZipLamT1 : ∀ {Γ x τ₁^ τ₁^′ τ₂ α} + → {ě : Γ , x ∶ (τ₁^ ◇τ) ⊢⇒ τ₂} + → (~>τ₁′ : τ₁^ ~ α ~τ> τ₁^′) + → (τ₁^≡τ₁′ : (τ₁^ ◇τ) ≡ (τ₁^′ ◇τ)) + → Γ ⊢ (⊢λ₁ x ∶ τ₁^ ∙ ě) ~ α ~⇒ (⊢λ₁ x ∶ τ₁^′ ∙ proj₁ (◇≡-⊢⇒ {Γ} {x} {τ₁^} {τ₁^′} ě τ₁^≡τ₁′)) + ESZipLamT2 : ∀ {Γ x τ₁^ τ₁^′ τ₂ τ₂′ α} + → {ě : Γ , x ∶ (τ₁^ ◇τ) ⊢⇒ τ₂} + → {ě′ : Γ , x ∶ (τ₁^′ ◇τ) ⊢⇒ τ₂′} + → (~>τ₁′ : τ₁^ ~ α ~τ> τ₁^′) + → (τ₁^≢τ₁′ : (τ₁^ ◇τ) ≢ (τ₁^′ ◇τ)) + → (↬⇒ě′ : Γ , x ∶ (τ₁^′ ◇τ) ⊢ (ě ⇒□) ↬⇒ ě′) + → Γ ⊢ (⊢λ₁ x ∶ τ₁^ ∙ ě) ~ α ~⇒ (⊢λ₁ x ∶ τ₁^′ ∙ ě′) + ESZipLamE : ∀ {Γ x τ₁ τ₂ τ₂′ α} + → {ê : - Γ , x ∶ τ₁ ⊢⇒ τ₂} + → {ê′ : - Γ , x ∶ τ₁ ⊢⇒ τ₂′} + → (~⇒ê′ : (Γ , x ∶ τ₁) ⊢ ê ~ α ~⇒ ê′) + → Γ ⊢ (⊢λ₂ x ∶ τ₁ ∙ ê) ~ α ~⇒ (⊢λ₂ x ∶ τ₁ ∙ ê′) + -- ESZipApL1 : ∀ {Γ τ τ₁ τ₂ τ₃ τ₁′ τ₂′ τ₃′ α} + -- → {τ₁▸ : τ₁ ▸ τ₂ -→ τ₃} + -- → (ê₁ : - Γ ⊢⇒ τ₁) + -- → {ê₁′ : - Γ ⊢⇒ τ₁′} + -- → {τ₁′▸ : τ₁′ ▸ τ₂′ -→ τ₃′} + -- → {ě₂ : Γ ⊢⇐ τ₂} + -- → Γ ⊢ ⊢ ê₁ ∙₁ ě₂ [ τ₁▸ ] ~ α ~⇒ ⊢ ê₁′ ∙₁ (proj₁ (⊢⇐-⊢⇐ ě₂)) [ τ₁′▸ ] + + -- analytic expression actions + data _⊢_~_~⇐_ : ∀ {τ : Typ} → (Γ : Ctx) → (ê : - Γ ⊢⇐ τ) → (α : Action) → (ê : - Γ ⊢⇐ τ) → Set where + -- movement + EAMove : ∀ {Γ τ δ} + → {ê : - Γ ⊢⇐ τ} + → {ê′ : - Γ ⊢⇐ τ} + → {ê+⇐ê′ : ê + δ +⇐ ê′} + → Γ ⊢ ê ~ move δ ~⇐ ê′ + + -- deletion + EADel : ∀ {Γ τ u} + → {ě : Γ ⊢⇐ τ} + → Γ ⊢ ⊢▹ ě ◃ ~ del u ~⇐ ⊢▹ ⊢∙ ⊢⦇-⦈^ u [ ~-unknown₂ ∙ MSuHole ] ◃ diff --git a/hazelnut/typed/zexp.agda b/hazelnut/typed/zexp.agda new file mode 100644 index 0000000..a64dfa7 --- /dev/null +++ b/hazelnut/typed/zexp.agda @@ -0,0 +1,666 @@ +open import prelude +open import core + +open import hazelnut.typed.ztyp + +-- cursor expressions +module hazelnut.typed.zexp where + -- zippered expressions + mutual + data -_⊢⇒_ : (Γ : Ctx) → (τ : Typ) → Set where + ⊢▹_◃ : ∀ {Γ : Ctx} {τ} + → (ě : Γ ⊢⇒ τ) + → - Γ ⊢⇒ τ + + ⊢λ₁_∶_∙_ : ∀ {Γ τ} + → (x : Var) + → (τ^ : ZTyp) + → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ) + → - Γ ⊢⇒ ((τ^ ◇τ) -→ τ) + + ⊢λ₂_∶_∙_ : ∀ {Γ τ′} + → (x : Var) + → (τ : Typ) + → (ê : - Γ , x ∶ τ ⊢⇒ τ′) + → - Γ ⊢⇒ (τ -→ τ′) + + ⊢_∙₁_[_] : ∀ {Γ τ τ₁ τ₂} + → (ê₁ : - Γ ⊢⇒ τ) + → (ě₂ : Γ ⊢⇐ τ₁) + → (τ▸ : τ ▸ τ₁ -→ τ₂) + → - Γ ⊢⇒ τ₂ + + ⊢_∙₂_[_] : ∀ {Γ τ τ₁ τ₂} + → (ě₁ : Γ ⊢⇒ τ) + → (ê₂ : - Γ ⊢⇐ τ₁) + → (τ▸ : τ ▸ τ₁ -→ τ₂) + → - Γ ⊢⇒ τ₂ + + ⊢⸨_⸩∙₁_[_] : ∀ {Γ τ} + → (ê₁ : - Γ ⊢⇒ τ) + → (ě₂ : Γ ⊢⇐ unknown) + → (τ!▸ : τ !▸-→) + → - Γ ⊢⇒ unknown + + ⊢⸨_⸩∙₂_[_] : ∀ {Γ τ} + → (ě₁ : Γ ⊢⇒ τ) + → (ê₂ : - Γ ⊢⇐ unknown) + → (τ!▸ : τ !▸-→) + → - Γ ⊢⇒ unknown + + ⊢_←₁_∙_ : ∀ {Γ τ₁ τ₂} + → (x : Var) + → (ê₁ : - Γ ⊢⇒ τ₁) + → (ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂) + → - Γ ⊢⇒ τ₂ + + ⊢_←₂_∙_ : ∀ {Γ τ₁ τ₂} + → (x : Var) + → (ě₁ : Γ ⊢⇒ τ₁) + → (ê₂ : - Γ , x ∶ τ₁ ⊢⇒ τ₂) + → - Γ ⊢⇒ τ₂ + + ⊢_+₁_ : ∀ {Γ} + → (ê₁ : - Γ ⊢⇐ num) + → (ě₂ : Γ ⊢⇐ num) + → - Γ ⊢⇒ num + + ⊢_+₂_ : ∀ {Γ} + → (ě₁ : Γ ⊢⇐ num) + → (ê₂ : - Γ ⊢⇐ num) + → - Γ ⊢⇒ num + + ⊢_∙₁_∙_[_] : ∀ {Γ τ₁ τ₂ τ} + → (ê₁ : - Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇒ τ₁) + → (ě₃ : Γ ⊢⇒ τ₂) + → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) + → - Γ ⊢⇒ τ + + ⊢_∙₂_∙_[_] : ∀ {Γ τ₁ τ₂ τ} + → (ě₁ : Γ ⊢⇐ bool) + → (ê₂ : - Γ ⊢⇒ τ₁) + → (ě₃ : Γ ⊢⇒ τ₂) + → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) + → - Γ ⊢⇒ τ + + ⊢_∙₃_∙_[_] : ∀ {Γ τ₁ τ₂ τ} + → (ě₁ : Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇒ τ₁) + → (ê₃ : - Γ ⊢⇒ τ₂) + → (τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ) + → - Γ ⊢⇒ τ + + ⊢⦉_∙₁_∙_⦊[_] : ∀ {Γ τ₁ τ₂} + → (ê₁ : - Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇒ τ₁) + → (ě₃ : Γ ⊢⇒ τ₂) + → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) + → - Γ ⊢⇒ unknown + + ⊢⦉_∙₂_∙_⦊[_] : ∀ {Γ τ₁ τ₂} + → (ě₁ : Γ ⊢⇐ bool) + → (ê₂ : - Γ ⊢⇒ τ₁) + → (ě₃ : Γ ⊢⇒ τ₂) + → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) + → - Γ ⊢⇒ unknown + + ⊢⦉_∙₃_∙_⦊[_] : ∀ {Γ τ₁ τ₂} + → (ě₁ : Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇒ τ₁) + → (ê₃ : - Γ ⊢⇒ τ₂) + → (τ₁~̸τ₂ : τ₁ ~̸ τ₂) + → - Γ ⊢⇒ unknown + + data ZSubsumable : {Γ : Ctx} {τ : Typ} → (ê : - Γ ⊢⇒ τ) → Set where + ZSuCursor : ∀ {Γ τ} + → {ě : Γ ⊢⇒ τ} + → (su : MSubsumable ě) + → ZSubsumable {Γ} (⊢▹ ě ◃) + + ZSuZipApL1 : ∀ {Γ τ τ₁ τ₂} + → {ê₁ : - Γ ⊢⇒ τ} + → {ě₂ : Γ ⊢⇐ τ₁} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → ZSubsumable {Γ} (⊢ ê₁ ∙₁ ě₂ [ τ▸ ]) + + ZSuZipApR1 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {ê₂ : - Γ ⊢⇐ τ₁} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → ZSubsumable {Γ} (⊢ ě₁ ∙₂ ê₂ [ τ▸ ]) + + ZSuZipApL2 : ∀ {Γ τ} + → {ê₁ : - Γ ⊢⇒ τ} + → {ě₂ : Γ ⊢⇐ unknown} + → {τ!▸ : τ !▸-→} + → ZSubsumable {Γ} (⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ]) + + ZSuZipApR2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {ê₂ : - Γ ⊢⇐ unknown} + → {τ!▸ : τ !▸-→} + → ZSubsumable {Γ} (⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ]) + + ZSuPlus1 : ∀ {Γ} + → {ê₁ : - Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → ZSubsumable {Γ} (⊢ ê₁ +₁ ě₂) + + ZSuPlus2 : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ê₂ : - Γ ⊢⇐ num} + → ZSubsumable {Γ} (⊢ ě₁ +₂ ê₂) + + ZSuInconsistentBranchesC : ∀ {Γ τ₁ τ₂} + → {ê₁ : - Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ZSubsumable {Γ} (⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) + + ZSuInconsistentBranchesL : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ê₂ : - Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ZSubsumable {Γ} (⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) + + ZSuInconsistentBranchesR : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ê₃ : - Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → ZSubsumable {Γ} (⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ]) + + data -_⊢⇐_ : (Γ : Ctx) → (τ : Typ) → Set where + ⊢▹_◃ : ∀ {Γ : Ctx} {τ} + → (ě : Γ ⊢⇐ τ) + → - Γ ⊢⇐ τ + + ⊢λ₁_∶_∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} + → (x : Var) + → (τ^ : ZTyp) + → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂) + → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) + → (τ~τ₁ : (τ^ ◇τ) ~ τ₁) + → - Γ ⊢⇐ τ₃ + + ⊢λ₂_∶_∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} + → (x : Var) + → (τ : Typ) + → (ê : - Γ , x ∶ τ ⊢⇐ τ₂) + → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) + → (τ~τ₁ : τ ~ τ₁) + → - Γ ⊢⇐ τ₃ + + ⊢⸨λ₁_∶_∙_⸩[_] : ∀ {Γ τ′} + → (x : Var) + → (τ^ : ZTyp) + → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ unknown) + → (τ′!▸ : τ′ !▸-→) + → - Γ ⊢⇐ τ′ + + ⊢⸨λ₂_∶_∙_⸩[_] : ∀ {Γ τ′} + → (x : Var) + → (τ : Typ) + → (ê : - Γ , x ∶ τ ⊢⇐ unknown) + → (τ′!▸ : τ′ !▸-→) + → - Γ ⊢⇐ τ′ + + ⊢λ₁_∶⸨_⸩∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} + → (x : Var) + → (τ^ : ZTyp) + → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂) + → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) + → (τ~̸τ₁ : (τ^ ◇τ) ~̸ τ₁) + → - Γ ⊢⇐ τ₃ + + ⊢λ₂_∶⸨_⸩∙_[_∙_] : ∀ {Γ τ₁ τ₂ τ₃} + → (x : Var) + → (τ : Typ) + → (ê : - Γ , x ∶ τ ⊢⇐ τ₂) + → (τ₃▸ : τ₃ ▸ τ₁ -→ τ₂) + → (τ~̸τ₁ : τ ~̸ τ₁) + → - Γ ⊢⇐ τ₃ + + ⊢_←₁_∙_ : ∀ {Γ τ₁ τ₂} + → (x : Var) + → (ê₁ : - Γ ⊢⇒ τ₁) + → (ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂) + → - Γ ⊢⇐ τ₂ + + ⊢_←₂_∙_ : ∀ {Γ τ₁ τ₂} + → (x : Var) + → (ě₁ : Γ ⊢⇒ τ₁) + → (ê₂ : - Γ , x ∶ τ₁ ⊢⇐ τ₂) + → - Γ ⊢⇐ τ₂ + + ⊢_∙₁_∙_ : ∀ {Γ τ} + → (ê₁ : - Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇐ τ) + → (ě₃ : Γ ⊢⇐ τ) + → - Γ ⊢⇐ τ + + ⊢_∙₂_∙_ : ∀ {Γ τ} + → (ě₁ : Γ ⊢⇐ bool) + → (ê₂ : - Γ ⊢⇐ τ) + → (ě₃ : Γ ⊢⇐ τ) + → - Γ ⊢⇐ τ + + ⊢_∙₃_∙_ : ∀ {Γ τ} + → (ě₁ : Γ ⊢⇐ bool) + → (ě₂ : Γ ⊢⇐ τ) + → (ê₃ : - Γ ⊢⇐ τ) + → - Γ ⊢⇐ τ + + ⊢⸨_⸩[_∙_] : ∀ {Γ τ τ′} + → (ê : - Γ ⊢⇒ τ′) + → (τ~̸τ′ : τ ~̸ τ′) + → (zsu : ZSubsumable ê) + → - Γ ⊢⇐ τ + + ⊢∙_[_∙_] : ∀ {Γ τ τ′} + → (ê : - Γ ⊢⇒ τ′) + → (τ~τ′ : τ ~ τ′) + → (zsu : ZSubsumable ê) + → - Γ ⊢⇐ τ + + -- well-formedness judgments + mutual + data _WF⇒ : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Set where + WFCursor : ∀ {Γ : Ctx} {τ} + → {ě : Γ ⊢⇒ τ} + → ⊢▹ ě ◃ WF⇒ + + WFLamT : ∀ {Γ x τ} + → {τ^ : ZTyp} + → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ} + → (⊢λ₁ x ∶ τ^ ∙ ě) WF⇒ + + WFLamE : ∀ {Γ x τ′} + → {τ : Typ} + → {ê : - Γ , x ∶ τ ⊢⇒ τ′} + → (wf : ê WF⇒) + → (⊢λ₂ x ∶ τ ∙ ê) WF⇒ + + WFApL1 : ∀ {Γ τ τ₁ τ₂} + → {ê₁ : - Γ ⊢⇒ τ} + → {ě₂ : Γ ⊢⇐ τ₁} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → (wf : ê₁ WF⇒) + → ⊢ ê₁ ∙₁ ě₂ [ τ▸ ] WF⇒ + + WFApR1 : ∀ {Γ τ τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ} + → {ê₂ : - Γ ⊢⇐ τ₁} + → {τ▸ : τ ▸ τ₁ -→ τ₂} + → (wf : ê₂ WF⇐) + → ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] WF⇒ + + WFApL2 : ∀ {Γ τ} + → {ê₁ : - Γ ⊢⇒ τ} + → {ě₂ : Γ ⊢⇐ unknown} + → {τ!▸ : τ !▸-→} + → (wf : ê₁ WF⇒) + → ⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ] WF⇒ + + WFApR2 : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇒ τ} + → {ê₂ : - Γ ⊢⇐ unknown} + → {τ!▸ : τ !▸-→} + → (wf : ê₂ WF⇐) + → ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] WF⇒ + + WFLetL : ∀ {Γ x τ₁ τ₂} + → {ê₁ : - Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇒ τ₂} + → (wf : ê₁ WF⇒) + → (⊢ x ←₁ ê₁ ∙ ě₂) WF⇒ + + WFLetR : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ê₂ : - Γ , x ∶ τ₁ ⊢⇒ τ₂} + → (wf : ê₂ WF⇒) + → (⊢ x ←₂ ě₁ ∙ ê₂) WF⇒ + + WFPlusL : ∀ {Γ} + → {ê₁ : - Γ ⊢⇐ num} + → {ě₂ : Γ ⊢⇐ num} + → (wf : ê₁ WF⇐) + → (⊢ ê₁ +₁ ě₂) WF⇒ + + WFPlusR : ∀ {Γ} + → {ě₁ : Γ ⊢⇐ num} + → {ê₂ : - Γ ⊢⇐ num} + → (wf : ê₂ WF⇐) + → (⊢ ě₁ +₂ ê₂) WF⇒ + + WFIfC : ∀ {Γ τ₁ τ₂ τ} + → {ê₁ : - Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → (wf : ê₁ WF⇐) + → ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒ + + WFIfL : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ê₂ : - Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → (wf : ê₂ WF⇒) + → ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒ + + WFIfR : ∀ {Γ τ₁ τ₂ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ê₃ : - Γ ⊢⇒ τ₂} + → {τ₁⊔τ₂ : τ₁ ⊔ τ₂ ⇒ τ} + → (wf : ê₃ WF⇒) + → ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] WF⇒ + + WFInconsistentBranchesC : ∀ {Γ τ₁ τ₂} + → {ê₁ : - Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → (wf : ê₁ WF⇐) + → ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒ + + WFInconsistentBranchesL : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ê₂ : - Γ ⊢⇒ τ₁} + → {ě₃ : Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → (wf : ê₂ WF⇒) + → ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒ + + WFInconsistentBranchesR : ∀ {Γ τ₁ τ₂} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇒ τ₁} + → {ê₃ : - Γ ⊢⇒ τ₂} + → {τ₁~̸τ₂ : τ₁ ~̸ τ₂} + → (wf : ê₃ WF⇒) + → ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] WF⇒ + + data _WF⇐ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Set where + WFCursor : ∀ {Γ : Ctx} {τ} + → {ě : Γ ⊢⇐ τ} + → ⊢▹ ě ◃ WF⇐ + + WFLamT1 : ∀ {Γ x τ₁ τ₂ τ₃} + → {τ^ : ZTyp} + → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : (τ^ ◇τ) ~ τ₁} + → ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] WF⇐ + + WFLamE1 : ∀ {Γ x τ₁ τ₂ τ₃} + → {τ : Typ} + → {ê : - Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~τ₁ : τ ~ τ₁} + → (wf : ê WF⇐) + → ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] WF⇐ + + WFLamT2 : ∀ {Γ x τ′} + → {τ^ : ZTyp} + → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] WF⇐ + + WFLamE2 : ∀ {Γ x τ′} + → {τ : Typ} + → {ê : - Γ , x ∶ τ ⊢⇐ unknown} + → {τ′!▸ : τ′ !▸-→} + → (wf : ê WF⇐) + → ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] WF⇐ + + WFLamT3 : ∀ {Γ x τ₁ τ₂ τ₃} + → {τ^ : ZTyp} + → {ě : Γ , x ∶ (τ^ ◇τ) ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : (τ^ ◇τ) ~̸ τ₁} + → ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐ + + WFLamE3 : ∀ {Γ x τ₁ τ₂ τ₃} + → {τ : Typ} + → {ê : - Γ , x ∶ τ ⊢⇐ τ₂} + → {τ₃▸ : τ₃ ▸ τ₁ -→ τ₂} + → {τ~̸τ₁ : τ ~̸ τ₁} + → (wf : ê WF⇐) + → ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐ + + WFLetL : ∀ {Γ x τ₁ τ₂} + → {ê₁ : - Γ ⊢⇒ τ₁} + → {ě₂ : Γ , x ∶ τ₁ ⊢⇐ τ₂} + → (wf : ê₁ WF⇒) + → (⊢ x ←₁ ê₁ ∙ ě₂) WF⇐ + + WFLetR : ∀ {Γ x τ₁ τ₂} + → {ě₁ : Γ ⊢⇒ τ₁} + → {ê₂ : - Γ , x ∶ τ₁ ⊢⇐ τ₂} + → (wf : ê₂ WF⇐) + → (⊢ x ←₂ ě₁ ∙ ê₂) WF⇐ + + WFIfC : ∀ {Γ τ} + → {ê₁ : - Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → (wf : ê₁ WF⇐) + → (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) WF⇐ + + WFIfL : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ê₂ : - Γ ⊢⇐ τ} + → {ě₃ : Γ ⊢⇐ τ} + → (wf : ê₂ WF⇐) + → (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) WF⇐ + + WFIfR : ∀ {Γ τ} + → {ě₁ : Γ ⊢⇐ bool} + → {ě₂ : Γ ⊢⇐ τ} + → {ê₃ : - Γ ⊢⇐ τ} + → (wf : ê₃ WF⇐) + → (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) WF⇐ + + WFInconsistentTypes : ∀ {Γ τ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {τ~̸τ′ : τ ~̸ τ′} + → {zsu : ZSubsumable ê} + → (wf : ê WF⇒) + → (nc : ¬ (∃[ ě ] ê ≡ ⊢▹ ě ◃)) + → ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] WF⇐ + + WFSubsume : ∀ {Γ τ τ′} + → {ê : - Γ ⊢⇒ τ′} + → {τ~τ′ : τ ~ τ′} + → {zsu : ZSubsumable ê} + → (wf : ê WF⇒) + → ⊢∙ ê [ τ~τ′ ∙ zsu ] WF⇐ + + -- well-formedness decidability + is-cursor? : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Dec (∃[ ě ] ê ≡ ⊢▹ ě ◃) + is-cursor? ⊢▹ ě ◃ = yes ⟨ ě , refl ⟩ + is-cursor? (⊢λ₁ x ∶ τ^ ∙ ě) = no λ() + is-cursor? (⊢λ₂ x ∶ τ ∙ ê) = no λ() + is-cursor? ⊢ ê ∙₁ ě₂ [ τ▸ ] = no λ() + is-cursor? ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] = no λ() + is-cursor? ⊢⸨ ê ⸩∙₁ ě₂ [ τ!▸ ] = no λ() + is-cursor? ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] = no λ() + is-cursor? (⊢ x ←₁ ê ∙ ě₂) = no λ() + is-cursor? (⊢ x ←₂ ě₁ ∙ ê₂) = no λ() + is-cursor? (⊢ ê₁ +₁ ě₂) = no λ() + is-cursor? (⊢ ě₁ +₂ ê₂) = no λ() + is-cursor? ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] = no λ() + is-cursor? ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] = no λ() + is-cursor? ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] = no λ() + is-cursor? ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] = no λ() + is-cursor? ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] = no λ() + is-cursor? ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] = no λ() + + mutual + _WF⇒? : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Dec (ê WF⇒) + ⊢▹ ě ◃ WF⇒? = yes WFCursor + (⊢λ₁ x ∶ τ^ ∙ ě) WF⇒? = yes WFLamT + (⊢λ₂ x ∶ τ ∙ ê) WF⇒? + with ê WF⇒? + ... | yes wf = yes (WFLamE wf) + ... | no !wf = no λ { (WFLamE wf) → !wf wf } + ⊢ ê₁ ∙₁ ě₂ [ τ▸ ] WF⇒? + with ê₁ WF⇒? + ... | yes wf = yes (WFApL1 wf) + ... | no !wf = no λ { (WFApL1 wf) → !wf wf } + ⊢ ě₁ ∙₂ ê₂ [ τ▸ ] WF⇒? + with ê₂ WF⇐? + ... | yes wf = yes (WFApR1 wf) + ... | no !wf = no λ { (WFApR1 wf) → !wf wf } + ⊢⸨ ê₁ ⸩∙₁ ě₂ [ τ!▸ ] WF⇒? + with ê₁ WF⇒? + ... | yes wf = yes (WFApL2 wf) + ... | no !wf = no λ { (WFApL2 wf) → !wf wf } + ⊢⸨ ě₁ ⸩∙₂ ê₂ [ τ!▸ ] WF⇒? + with ê₂ WF⇐? + ... | yes wf = yes (WFApR2 wf) + ... | no !wf = no λ { (WFApR2 wf) → !wf wf } + (⊢ x ←₁ ê₁ ∙ ě₂) WF⇒? + with ê₁ WF⇒? + ... | yes wf = yes (WFLetL wf) + ... | no !wf = no λ { (WFLetL wf) → !wf wf } + (⊢ x ←₂ ě₁ ∙ ê₂) WF⇒? + with ê₂ WF⇒? + ... | yes wf = yes (WFLetR wf) + ... | no !wf = no λ { (WFLetR wf) → !wf wf } + (⊢ ê₁ +₁ ě₂) WF⇒? + with ê₁ WF⇐? + ... | yes wf = yes (WFPlusL wf) + ... | no !wf = no λ { (WFPlusL wf) → !wf wf } + (⊢ ě₁ +₂ ê₂) WF⇒? + with ê₂ WF⇐? + ... | yes wf = yes (WFPlusR wf) + ... | no !wf = no λ { (WFPlusR wf) → !wf wf } + ⊢ ê₁ ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒? + with ê₁ WF⇐? + ... | yes wf = yes (WFIfC wf) + ... | no !wf = no λ { (WFIfC wf) → !wf wf } + ⊢ ě₁ ∙₂ ê₂ ∙ ě₃ [ τ₁⊔τ₂ ] WF⇒? + with ê₂ WF⇒? + ... | yes wf = yes (WFIfL wf) + ... | no !wf = no λ { (WFIfL wf) → !wf wf } + ⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ] WF⇒? + with ê₃ WF⇒? + ... | yes wf = yes (WFIfR wf) + ... | no !wf = no λ { (WFIfR wf) → !wf wf } + ⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒? + with ê₁ WF⇐? + ... | yes wf = yes (WFInconsistentBranchesC wf) + ... | no !wf = no λ { (WFInconsistentBranchesC wf) → !wf wf } + ⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] WF⇒? + with ê₂ WF⇒? + ... | yes wf = yes (WFInconsistentBranchesL wf) + ... | no !wf = no λ { (WFInconsistentBranchesL wf) → !wf wf } + ⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ] WF⇒? + with ê₃ WF⇒? + ... | yes wf = yes (WFInconsistentBranchesR wf) + ... | no !wf = no λ { (WFInconsistentBranchesR wf) → !wf wf } + + _WF⇐? : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Dec (ê WF⇐) + ⊢▹ ě ◃ WF⇐? = yes WFCursor + ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] WF⇐? = yes WFLamT1 + ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] WF⇐? + with ê WF⇐? + ... | yes wf = yes (WFLamE1 wf) + ... | no !wf = no λ { (WFLamE1 wf) → !wf wf } + ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] WF⇐? = yes WFLamT2 + ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] WF⇐? + with ê WF⇐? + ... | yes wf = yes (WFLamE2 wf) + ... | no !wf = no λ { (WFLamE2 wf) → !wf wf } + ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐? = yes WFLamT3 + ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] WF⇐? + with ê WF⇐? + ... | yes wf = yes (WFLamE3 wf) + ... | no !wf = no λ { (WFLamE3 wf) → !wf wf } + (⊢ x ←₁ ê₁ ∙ ě₂) WF⇐? + with ê₁ WF⇒? + ... | yes wf = yes (WFLetL wf) + ... | no !wf = no λ { (WFLetL wf) → !wf wf } + (⊢ x ←₂ ě₁ ∙ ê₂) WF⇐? + with ê₂ WF⇐? + ... | yes wf = yes (WFLetR wf) + ... | no !wf = no λ { (WFLetR wf) → !wf wf } + (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) WF⇐? + with ê₁ WF⇐? + ... | yes wf = yes (WFIfC wf) + ... | no !wf = no λ { (WFIfC wf) → !wf wf } + (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) WF⇐? + with ê₂ WF⇐? + ... | yes wf = yes (WFIfL wf) + ... | no !wf = no λ { (WFIfL wf) → !wf wf } + (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) WF⇐? + with ê₃ WF⇐? + ... | yes wf = yes (WFIfR wf) + ... | no !wf = no λ { (WFIfR wf) → !wf wf } + ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] WF⇐? + with ê WF⇒? + ... | no !wf = no λ { (WFInconsistentTypes wf nc) → !wf wf } + ... | yes wf with is-cursor? ê + ... | yes ic = no λ { (WFInconsistentTypes wf nc) → nc ic } + ... | no nc = yes (WFInconsistentTypes wf nc) + ⊢∙ ê [ τ~τ′ ∙ zsu ] WF⇐? + with ê WF⇒? + ... | yes wf = yes (WFSubsume wf) + ... | no !wf = no λ { (WFSubsume wf) → !wf wf } + + -- functional cursor erasure + mutual + _◇⇒ : ∀ {Γ τ} → (ê : - Γ ⊢⇒ τ) → Γ ⊢⇒ τ + ⊢▹ ě ◃ ◇⇒ = ě + (⊢λ₁ x ∶ τ^ ∙ ě) ◇⇒ = ⊢λ x ∶ (τ^ ◇τ) ∙ ě + (⊢λ₂ x ∶ τ ∙ ê) ◇⇒ = ⊢λ x ∶ τ ∙ (ê ◇⇒) + (⊢ ê ∙₁ ě [ τ▸ ]) ◇⇒ = ⊢ (ê ◇⇒) ∙ ě [ τ▸ ] + (⊢ ě ∙₂ ê [ τ▸ ]) ◇⇒ = ⊢ ě ∙ (ê ◇⇐) [ τ▸ ] + (⊢⸨ ê ⸩∙₁ ě [ τ!▸ ]) ◇⇒ = ⊢⸨ (ê ◇⇒) ⸩∙ ě [ τ!▸ ] + (⊢⸨ ě ⸩∙₂ ê [ τ!▸ ]) ◇⇒ = ⊢⸨ ě ⸩∙ (ê ◇⇐) [ τ!▸ ] + (⊢ x ←₁ ê ∙ ě) ◇⇒ = ⊢ x ← (ê ◇⇒) ∙ ě + (⊢ x ←₂ ě ∙ ê) ◇⇒ = ⊢ x ← ě ∙ (ê ◇⇒) + (⊢ ê +₁ ě) ◇⇒ = ⊢ (ê ◇⇐) + ě + (⊢ ě +₂ ê) ◇⇒ = ⊢ ě + (ê ◇⇐) + (⊢ ê ∙₁ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ (ê ◇⇐) ∙ ě₂ ∙ ě₃ [ τ₁⊔τ₂ ] + (⊢ ě₁ ∙₂ ê ∙ ě₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ ě₁ ∙ (ê ◇⇒) ∙ ě₃ [ τ₁⊔τ₂ ] + (⊢ ě₁ ∙₃ ě₂ ∙ ê₃ [ τ₁⊔τ₂ ]) ◇⇒ = ⊢ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇒) [ τ₁⊔τ₂ ] + (⊢⦉ ê₁ ∙₁ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ (ê₁ ◇⇐) ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + (⊢⦉ ě₁ ∙₂ ê₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ ě₁ ∙ (ê₂ ◇⇒) ∙ ě₃ ⦊[ τ₁~̸τ₂ ] + (⊢⦉ ě₁ ∙₃ ě₂ ∙ ê₃ ⦊[ τ₁~̸τ₂ ]) ◇⇒ = ⊢⦉ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇒) ⦊[ τ₁~̸τ₂ ] + + ZSu→MSu : ∀ {Γ τ} {ê : - Γ ⊢⇒ τ} → (zsu : ZSubsumable ê) → MSubsumable (ê ◇⇒) + ZSu→MSu (ZSuCursor su) = su + ZSu→MSu ZSuZipApL1 = MSuAp1 + ZSu→MSu ZSuZipApR1 = MSuAp1 + ZSu→MSu ZSuZipApL2 = MSuAp2 + ZSu→MSu ZSuZipApR2 = MSuAp2 + ZSu→MSu ZSuPlus1 = MSuPlus + ZSu→MSu ZSuPlus2 = MSuPlus + ZSu→MSu ZSuInconsistentBranchesC = MSuInconsistentBranches + ZSu→MSu ZSuInconsistentBranchesL = MSuInconsistentBranches + ZSu→MSu ZSuInconsistentBranchesR = MSuInconsistentBranches + + _◇⇐ : ∀ {Γ τ} → (ê : - Γ ⊢⇐ τ) → Γ ⊢⇐ τ + ⊢▹ ě ◃ ◇⇐ = ě + ⊢λ₁ x ∶ τ^ ∙ ě [ τ₃▸ ∙ τ~τ₁ ] ◇⇐ = ⊢λ x ∶ (τ^ ◇τ) ∙ ě [ τ₃▸ ∙ τ~τ₁ ] + ⊢λ₂ x ∶ τ ∙ ê [ τ₃▸ ∙ τ~τ₁ ] ◇⇐ = ⊢λ x ∶ τ ∙ (ê ◇⇐) [ τ₃▸ ∙ τ~τ₁ ] + ⊢⸨λ₁ x ∶ τ^ ∙ ě ⸩[ τ′!▸ ] ◇⇐ = ⊢⸨λ x ∶ (τ^ ◇τ) ∙ ě ⸩[ τ′!▸ ] + ⊢⸨λ₂ x ∶ τ ∙ ê ⸩[ τ′!▸ ] ◇⇐ = ⊢⸨λ x ∶ τ ∙ (ê ◇⇐) ⸩[ τ′!▸ ] + ⊢λ₁ x ∶⸨ τ^ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ◇⇐ = ⊢λ x ∶⸨ τ^ ◇τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] + ⊢λ₂ x ∶⸨ τ ⸩∙ ê [ τ₃▸ ∙ τ~̸τ₁ ] ◇⇐ = ⊢λ x ∶⸨ τ ⸩∙ (ê ◇⇐) [ τ₃▸ ∙ τ~̸τ₁ ] + (⊢ x ←₁ ê₁ ∙ ě₂) ◇⇐ = ⊢ x ← (ê₁ ◇⇒) ∙ ě₂ + (⊢ x ←₂ ě₁ ∙ ê₂) ◇⇐ = ⊢ x ← ě₁ ∙ (ê₂ ◇⇐) + (⊢ ê₁ ∙₁ ě₂ ∙ ě₃) ◇⇐ = ⊢ (ê₁ ◇⇐) ∙ ě₂ ∙ ě₃ + (⊢ ě₁ ∙₂ ê₂ ∙ ě₃) ◇⇐ = ⊢ ě₁ ∙ (ê₂ ◇⇐) ∙ ě₃ + (⊢ ě₁ ∙₃ ě₂ ∙ ê₃) ◇⇐ = ⊢ ě₁ ∙ ě₂ ∙ (ê₃ ◇⇐) + ⊢⸨ ê ⸩[ τ~̸τ′ ∙ zsu ] ◇⇐ = ⊢⸨ ê ◇⇒ ⸩[ τ~̸τ′ ∙ (ZSu→MSu zsu) ] + ⊢∙ ê [ τ~τ′ ∙ zsu ] ◇⇐ = ⊢∙ (ê ◇⇒) [ τ~τ′ ∙ (ZSu→MSu zsu) ] + + ◇≡-⊢⇒ : ∀ {Γ x τ^ τ^′ τ} → (ě : Γ , x ∶ (τ^ ◇τ) ⊢⇒ τ) → (τ^ ◇τ) ≡ (τ^′ ◇τ) → Σ[ ě′ ∈ Γ , x ∶ (τ^′ ◇τ) ⊢⇒ τ ] (ě ⇒□) ≡ (ě′ ⇒□) + ◇≡-⊢⇒ ě eq rewrite eq = ⟨ ě , refl ⟩ diff --git a/hazelnut/typed/ztyp.agda b/hazelnut/typed/ztyp.agda new file mode 100644 index 0000000..b3eda74 --- /dev/null +++ b/hazelnut/typed/ztyp.agda @@ -0,0 +1,32 @@ +open import prelude +open import core + +-- zippered types +module hazelnut.typed.ztyp where + data ZTyp : Set where + ▹_◃ : (τ : Typ) → ZTyp + _-→₁_ : (τ^ : ZTyp) → (τ : Typ) → ZTyp + _-→₂_ : (τ : Typ) → (τ^ : ZTyp) → ZTyp + + infixr 25 _-→₁_ + infixr 25 _-→₂_ + + -- judgmental cursor erasure + data erase-τ : (τ^ : ZTyp) → (τ : Typ) → Set where + ETTop : ∀ {τ} → erase-τ (▹ τ ◃) τ + ETArr1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂) + ETArr2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂) + + -- functional cursor erasure + _◇τ : (τ^ : ZTyp) → Typ + ▹ τ ◃ ◇τ = τ + (τ^ -→₁ τ) ◇τ = (τ^ ◇τ) -→ τ + (τ -→₂ τ^) ◇τ = τ -→ (τ^ ◇τ) + + -- convert judgmental cursor erasure to functional cursor erasure + erase-τ→◇ : ∀ {τ^ τ} → erase-τ τ^ τ → τ^ ◇τ ≡ τ + erase-τ→◇ ETTop = refl + erase-τ→◇ (ETArr1 τ₁^◇) + rewrite erase-τ→◇ τ₁^◇ = refl + erase-τ→◇ (ETArr2 τ₂^◇) + rewrite erase-τ→◇ τ₂^◇ = refl