From 331c729d29a9c3184978cc7757c2e2b3e3e7aceb Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 24 Feb 2022 13:57:42 -0600 Subject: [PATCH] WIP --- prototyping/Luau/StrictMode.agda | 42 ++-- prototyping/Luau/TypeCheck.agda | 16 +- prototyping/Properties/StrictMode.agda | 300 +++++++++++++------------ prototyping/Properties/TypeCheck.agda | 23 +- 4 files changed, 204 insertions(+), 177 deletions(-) diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index b679bbfb..264ee37d 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -21,17 +21,17 @@ data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set data Warningᴱ H {Γ} where - UnallocatedAddress : ∀ a {T} → + UnallocatedAddress : ∀ {a T} → (H [ a ]ᴴ ≡ nothing) → --------------------- - Warningᴱ H (addr a T) + Warningᴱ H (addr {a} T) UnboundVariable : ∀ x {T} {p} → (Γ [ x ]ⱽ ≡ nothing) → ------------------------ - Warningᴱ H (var x {T} p) + Warningᴱ H (var {x} {T} p) app₀ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → @@ -51,29 +51,29 @@ data Warningᴱ H {Γ} where ----------------- Warningᴱ H (app D₁ D₂) - function₀ : ∀ f {x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → + function₀ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → (U ≢ V) → ------------------------- - Warningᴱ H (function f {U = U} D) + Warningᴱ H (function {f} {U = U} D) - function₁ : ∀ f {x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → + function₁ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → Warningᴮ H D → ------------------------- - Warningᴱ H (function f {U = U} D) + Warningᴱ H (function {f} {U = U} D) - block₀ : ∀ b {B T U} {D : Γ ⊢ᴮ B ∈ U} → + block₀ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} → (T ≢ U) → ------------------------------ - Warningᴱ H (block b {T = T} D) + Warningᴱ H (block {b} {T = T} D) - block₁ : ∀ b {B T U} {D : Γ ⊢ᴮ B ∈ U} → + block₁ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} → Warningᴮ H D → ------------------------------ - Warningᴱ H (block b {T = T} D) + Warningᴱ H (block {b} {T = T} D) data Warningᴮ H {Γ} where @@ -101,37 +101,37 @@ data Warningᴮ H {Γ} where -------------------- Warningᴮ H (local D₁ D₂) - function₀ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → + function₀ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → (U ≢ V) → ------------------------------------- - Warningᴮ H (function f {U = U} D₁ D₂) + Warningᴮ H (function D₁ D₂) - function₁ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → + function₁ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → Warningᴮ H D₁ → -------------------- - Warningᴮ H (function f D₁ D₂) + Warningᴮ H (function D₁ D₂) - function₂ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → + function₂ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → Warningᴮ H D₂ → -------------------- - Warningᴮ H (function f D₁ D₂) + Warningᴮ H (function D₁ D₂) data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where - function₀ : ∀ f {x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → + function₀ : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → (U ≢ V) → --------------------------------- - Warningᴼ H (function f {U = U} D) + Warningᴼ H (function {f} {U = U} D) - function₁ : ∀ f {x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → + function₁ : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → Warningᴮ H D → --------------------------------- - Warningᴼ H (function f {U = U} D) + Warningᴼ H (function {f} {U = U} D) data Warningᴴ H (D : ⊢ᴴ H) : Set where diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index 8e23faf7..217abce2 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -48,7 +48,7 @@ data _⊢ᴮ_∈_ where -------------------------------- Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V - function : ∀ f {x B C T U V W Γ} → + function : ∀ {f x B C T U V W Γ} → (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V → (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W → @@ -62,18 +62,18 @@ data _⊢ᴱ_∈_ where -------------- Γ ⊢ᴱ nil ∈ nil - var : ∀ x {T Γ} → + var : ∀ {x T Γ} → T ≡ orBot(Γ [ x ]ⱽ) → ---------------- Γ ⊢ᴱ (var x) ∈ T - addr : ∀ a T {Γ} → + addr : ∀ {a Γ} T → ----------------- Γ ⊢ᴱ (addr a) ∈ T - number : ∀ n {Γ} → + number : ∀ {n Γ} → ------------------------ Γ ⊢ᴱ (number n) ∈ number @@ -85,19 +85,19 @@ data _⊢ᴱ_∈_ where ---------------------- Γ ⊢ᴱ (M $ N) ∈ (tgt T) - function : ∀ f {x B T U V Γ} → + function : ∀ {f x B T U V Γ} → (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V → ----------------------------------------------------- Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) - block : ∀ b {B T U Γ} → + block : ∀ {b B T U Γ} → Γ ⊢ᴮ B ∈ U → ------------------------------------ Γ ⊢ᴱ (block var b ∈ T is B end) ∈ T - binexp : ∀ op {Γ M N T U} → + binexp : ∀ {op Γ M N T U} → Γ ⊢ᴱ M ∈ T → Γ ⊢ᴱ N ∈ U → @@ -111,7 +111,7 @@ data ⊢ᴼ_ : Maybe(Object yes) → Set where --------- ⊢ᴼ nothing - function : ∀ f {x T U V B} → + function : ∀ {f x T U V B} → (x ↦ T) ⊢ᴮ B ∈ V → ---------------------------------------------- diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 8281ecd7..cf18663b 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -1,5 +1,4 @@ {-# OPTIONS --rewriting #-} -{-# OPTIONS --allow-unsolved-metas #-} module Properties.StrictMode where @@ -21,7 +20,7 @@ open import Properties.Remember using (remember; _,_) open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) open import Properties.Dec using (Dec; yes; no) open import Properties.Contradiction using (CONTRADICTION) -open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ) +open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction) open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₁; binOp₂; binOpEval; refl; step) open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return) @@ -83,7 +82,7 @@ heap-weakeningᴱ H (nil) h = ok refl heap-weakeningᴱ H (var x) h = ok refl heap-weakeningᴱ H (addr a) refl = ok refl heap-weakeningᴱ H (addr a) (snoc {a = b} defn) with a ≡ᴬ b -heap-weakeningᴱ H (addr a) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress a refl) +heap-weakeningᴱ H (addr a) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl) heap-weakeningᴱ H (addr a) (snoc {a = b} p) | no q = ok (cong orBot (cong typeOfᴹᴼ (lookup-not-allocated p q))) heap-weakeningᴱ H (number n) h = ok refl heap-weakeningᴱ H (binexp M op N) h = ok refl @@ -94,7 +93,7 @@ heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p -heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ f W) +heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W) heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W) @@ -111,37 +110,37 @@ typeOf-val-not-bot nil = ok (λ ()) typeOf-val-not-bot (number n) = ok (λ ()) typeOf-val-not-bot {H = H} (addr a) with remember (H [ a ]ᴴ) typeOf-val-not-bot {H = H} (addr a) | (just O , p) = ok (λ q → bot-not-obj O (trans q (cong orBot (cong typeOfᴹᴼ p)))) -typeOf-val-not-bot {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress a p) +typeOf-val-not-bot {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p) -substitutivityᴱ : ∀ {Γ T H} M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ)) -substitutivityᴱ-whenever-yes : ∀ {Γ T H} v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p))) -substitutivityᴱ-whenever-no : ∀ {Γ T H} v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p))) -substitutivityᴮ : ∀ {Γ T H} B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) -substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T H} B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p))) -substitutivityᴮ-unless-no : ∀ {Γ Γ′ T H} B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p))) +substitutivityᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ)) +substitutivityᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p))) +substitutivityᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p))) +substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) +substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p))) +substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p))) -substitutivityᴱ nil v x p = refl -substitutivityᴱ (var y) v x p with x ≡ⱽ y -substitutivityᴱ (var y) v x p | yes q = substitutivityᴱ-whenever-yes v x y q p -substitutivityᴱ (var y) v x p | no q = substitutivityᴱ-whenever-no v x y q p -substitutivityᴱ (addr a) v x p = refl -substitutivityᴱ (number n) v x p = refl -substitutivityᴱ (binexp M op N) v x p = refl -substitutivityᴱ (M $ N) v x p = cong tgt (substitutivityᴱ M v x p) -substitutivityᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = refl -substitutivityᴱ (block var b ∈ T is B end) v x p = refl -substitutivityᴱ-whenever-yes v x x refl q = trans (cong orBot q) (sym (typeOfᴱⱽ v)) -substitutivityᴱ-whenever-no v x y p q = cong orBot ( sym (⊕-lookup-miss x y _ _ p)) -substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f -substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x f q p (⊕-over q) -substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no B v x f q p (⊕-swap q) -substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y -substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x y q p (⊕-over q) -substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no B v x y q p (⊕-swap q) -substitutivityᴮ (return M ∙ B) v x p = substitutivityᴱ M v x p -substitutivityᴮ done v x p = refl -substitutivityᴮ-unless-yes B v x x refl q refl = refl -substitutivityᴮ-unless-no B v x y p q refl = substitutivityᴮ B v x q +substitutivityᴱ H nil v x p = refl +substitutivityᴱ H (var y) v x p with x ≡ⱽ y +substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p +substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p +substitutivityᴱ H (addr a) v x p = refl +substitutivityᴱ H (number n) v x p = refl +substitutivityᴱ H (binexp M op N) v x p = refl +substitutivityᴱ H (M $ N) v x p = cong tgt (substitutivityᴱ H M v x p) +substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = refl +substitutivityᴱ H (block var b ∈ T is B end) v x p = refl +substitutivityᴱ-whenever-yes H v x x refl q = trans (cong orBot q) (sym (typeOfᴱⱽ v)) +substitutivityᴱ-whenever-no H v x y p q = cong orBot ( sym (⊕-lookup-miss x y _ _ p)) +substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f +substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q) +substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q) +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q) +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x y q p (⊕-swap q) +substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p +substitutivityᴮ H done v x p = refl +substitutivityᴮ-unless-yes H B v x x refl q refl = refl +substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′) preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′) @@ -156,122 +155,128 @@ preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q) preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W)) preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v) preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!!}) -- (substitutivityᴮ H B v x (sym q))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ f r))) +preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orBot (cong typeOfᴹᴼ p))) +preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ r))) preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (app₀ (λ s → r (trans (trans (sym (cong src (cong orBot (cong typeOfᴹᴼ p)))) (trans s (typeOfᴱⱽ v))) (cong orBot q))))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-bot v -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ v) (cong orBot q)))) -preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W)) +preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-bot v +preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ v) (cong orBot q)))) +preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W)) preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl -preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) = {!!} -- ok refl -preservationᴱ H (block var b ∈ T is done end) (done) = {!!} -- ok refl +preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) with T ≡ᵀ typeOfᴱ H ∅ (val v) +preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p +preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (block₀ p)) +preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil +preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p +preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (block₀ p)) preservationᴱ H (binexp M op N) s = {!!} -preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H {!!} (rednᴱ⊑ s) +preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s) preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W)) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ B v x (sym p)) +preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p)) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (local₀ (λ r → q (trans r (trans (typeOfᴱⱽ v) (cong orBot p)))))) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-bot v preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (trans (typeOfᴱⱽ v) (cong orBot p)))) preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W)) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H {!!} (snoc defn) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ {T = T ⇒ U} B (addr a) f refl)) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ f W)) +preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H B (snoc defn) +preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl)) +preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W)) preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s preservationᴮ H (return M ∙ B) (return s) | ok p = ok p preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W)) preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W) -reflect-substitutionᴱ : ∀ {H Γ T} M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M) -reflect-substitutionᴱ-whenever-yes : ∀ {H Γ T} v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) -reflect-substitutionᴱ-whenever-no : ∀ {H Γ T} v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) -reflect-substitutionᴮ : ∀ {H Γ T} B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B) -reflect-substitutionᴮ-unless-yes : ∀ {H Γ Γ′ T} B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) -reflect-substitutionᴮ-unless-no : ∀ {H Γ Γ′ T} B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M) +reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) +reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) +reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) -reflect-substitutionᴱ (var y) v x p W with x ≡ⱽ y -reflect-substitutionᴱ (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes v x y r p W -reflect-substitutionᴱ (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no v x y r p W -reflect-substitutionᴱ (addr a) v x p (UnallocatedAddress a r) = UnallocatedAddress a r -reflect-substitutionᴱ (M $ N) v x p (app₀ q) = app₀ (λ s → q (trans (cong src (sym (substitutivityᴱ M v x p))) (trans s (substitutivityᴱ N v x p)))) -reflect-substitutionᴱ (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ M v x p W) -reflect-substitutionᴱ (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ N v x p W) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) with (x ≡ⱽ y) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes B v x y r p (⊕-over r)))) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) | no r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-no B v x y r p (⊕-swap r)))) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ f W) with (x ≡ⱽ y) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-over r) W) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ-unless-no B v x y r p (⊕-swap r) W) -reflect-substitutionᴱ (block var b ∈ T is B end) v x p (block₀ b W) = {!!} -reflect-substitutionᴱ (block var b ∈ T is B end) v x p (block₁ b W) = block₁ b (reflect-substitutionᴮ B v x p W) -reflect-substitutionᴱ (binexp M op N) x v p W = {!!} +reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y +reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W +reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W +reflect-substitutionᴱ H (addr a) v x p (UnallocatedAddress r) = UnallocatedAddress r +reflect-substitutionᴱ H (M $ N) v x p (app₀ q) = app₀ (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p)))) +reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W) +reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) with (x ≡ⱽ y) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) | yes r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r)))) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ q) | no r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r)))) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) +reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₀ q) = block₀ (λ r → q (trans r (substitutivityᴮ H B v x p))) +reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W) +reflect-substitutionᴱ H (binexp M op N) x v p W = {!!} -reflect-substitutionᴱ-whenever-no v x y p q (UnboundVariable y r) = UnboundVariable y (trans (sym (⊕-lookup-miss x y _ _ p)) r) -reflect-substitutionᴱ-whenever-yes (addr a) x x refl p (UnallocatedAddress a q) with trans p (cong typeOfᴹᴼ q) -reflect-substitutionᴱ-whenever-yes (addr a) x x refl p (UnallocatedAddress a q) | () +reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable y r) = UnboundVariable y (trans (sym (⊕-lookup-miss x y _ _ p)) r) +reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q) +reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | () -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) with (x ≡ⱽ y) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes C v x y r p (⊕-over r)))) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) | no r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-no C v x y r p (⊕-swap r)))) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) with (x ≡ⱽ y) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes C v x y r p (⊕-over r) W) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ-unless-no C v x y r p (⊕-swap r) W) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W) with (x ≡ⱽ f) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W)| yes r = function₂ f (reflect-substitutionᴮ-unless-yes B v x f r p (⊕-over r) W) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W)| no r = function₂ f (reflect-substitutionᴮ-unless-no B v x f r p (⊕-swap r) W) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₀ q) = local₀ (λ r → q (trans r (substitutivityᴱ M v x p))) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ M v x p W) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-over r) W) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no B v x y r p (⊕-swap r) W) -reflect-substitutionᴮ (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ M v x p W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) with (x ≡ⱽ y) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) | yes r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r)))) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ q) | no r = function₀ (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r)))) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₀ q) = local₀ (λ r → q (trans r (substitutivityᴱ H M v x p))) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) +reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W) -reflect-substitutionᴮ-unless-yes B v x y r p refl W = W -reflect-substitutionᴮ-unless-no B v x y r p refl W = reflect-substitutionᴮ B v x p W +reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W +reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) reflect-weakeningᴱ H (var x) h (UnboundVariable x p) = (UnboundVariable x p) -reflect-weakeningᴱ H (addr a) h (UnallocatedAddress a p) = UnallocatedAddress a (lookup-⊑-nothing a h p) -reflect-weakeningᴱ H (M $ N) h (app₀ p) with heap-weakeningᴱ H {!!} h | heap-weakeningᴱ H {!!} h +reflect-weakeningᴱ H (addr a) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p) +reflect-weakeningᴱ H (M $ N) h (app₀ p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h reflect-weakeningᴱ H (M $ N) h (app₀ p) | ok q₁ | ok q₂ = app₀ (λ r → p (trans (cong src (sym q₁)) (trans r q₂))) reflect-weakeningᴱ H (M $ N) h (app₀ p) | warning W | _ = app₁ W reflect-weakeningᴱ H (M $ N) h (app₀ p) | _ | warning W = app₂ W reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W) reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W) -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ f p) with heap-weakeningᴮ H {!!} h -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ f p) | warning W = function₁ f W -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ f W) = function₁ f (reflect-weakeningᴮ H B h W) -reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ b W) = {!!} -- block₁ b (reflect-weakeningᴮ H B h W) -reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ b W) = block₁ b (reflect-weakeningᴮ H B h W) +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) with heap-weakeningᴮ H B h +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | ok q = function₀ (λ r → p (trans r q)) +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | warning W = function₁ W +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W) +reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) with heap-weakeningᴮ H B h +reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) | ok q = block₀ (λ r → p (trans r q)) +reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₀ p) | warning W = block₁ W +reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W) reflect-weakeningᴮ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ H M h W) -reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) with heap-weakeningᴱ H {!!} h +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) with heap-weakeningᴱ H M h reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) | ok q = local₀ (λ r → p (trans r q)) reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₀ p) | warning W = local₁ W reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W) reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ f p) with heap-weakeningᴮ H {!!} h -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ f p) | warning W = function₁ f W -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ f W) = function₁ f (reflect-weakeningᴮ H C h W) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ f W) = function₂ f (reflect-weakeningᴮ H B h W) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) with heap-weakeningᴮ H C h +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) | ok q = function₀ (λ r → p (trans r q)) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₀ p) | warning W = function₁ W +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W) reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O) -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ f p) with heap-weakeningᴮ H {!!} h -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ f p) | warning W = function₁ f W -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ f W′) = function₁ f (reflect-weakeningᴮ H B h W′) +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) with heap-weakeningᴮ H B h +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) | ok q = function₀ (λ r → p (trans r q)) +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₀ p) | warning W = function₁ W +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′) reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) -reflectᴱ H (M $ N) (app₁ s) (app₀ p) with preservationᴱ H M s | heap-weakeningᴱ H {!!} (rednᴱ⊑ s) +reflectᴱ H (M $ N) (app₁ s) (app₀ p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s) reflectᴱ H (M $ N) (app₁ s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′))) reflectᴱ H (M $ N) (app₁ s) (app₀ p) | warning (expr W) | _ = expr (app₁ W) reflectᴱ H (M $ N) (app₁ s) (app₀ p) | warning (heap W) | _ = heap W @@ -280,29 +285,38 @@ reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′ reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W) reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′)) -reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) with heap-weakeningᴱ H {!!} (rednᴱ⊑ s) | preservationᴱ H N s +reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | ok q | ok q′ = expr (app₀ (λ r → p′ (trans (trans (cong src (sym q)) r) q′))) reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | warning W | _ = expr (app₁ W) -reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (expr W) = expr (app₂ W) -reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (heap W) = heap W +reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (expr W) = expr (app₂ W) +reflectᴱ H (M $ N) (app₂ p s) (app₀ p′) | _ | warning (heap W) = heap W reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′)) reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′ reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ f W′) = {!!} -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) with remember (typeOfⱽ H v) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just S , q) with S ≡ᵀ T -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just T , q) | yes refl = heap (addr a p (function₁ f (reflect-substitutionᴮ B v x (sym q) W′))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just S , q) | no r = expr (app₀ (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p)))))))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) with typeOf-val-not-bot v -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v)))) -reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) | warning W = expr (app₂ W) -reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ b W′) = {!!} -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ b W′) with reflectᴮ H B s W′ -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ b W′) | heap W = heap W -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ b W′) | block W = expr (block₁ b W) -reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress a ()) -reflectᴱ H (block var b ∈ T is return N ∙ B end) W = {!!} -- expr (block₁ _ (return W)) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) with remember (typeOfⱽ H v) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just S , r) with S ≡ᵀ T +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just T , r) | yes refl = heap (addr a p (function₀ (λ s → q (trans s (substitutivityᴮ H B v x (sym r)))))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (just S , r) | no s = expr (app₀ (λ t → s (trans (cong orBot (sym r)) (trans (sym (typeOfᴱⱽ v)) (trans (sym t) (cong src (cong orBot (cong typeOfᴹᴼ p)))))))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) with typeOf-val-not-bot v +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) | ok s = CONTRADICTION (s (trans (cong orBot (sym r)) (sym (typeOfᴱⱽ v)))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ q) | (nothing , r) | warning W = expr (app₂ W) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (app₀ (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p)))))))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-bot v +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v)))) +reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W) +reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) with preservationᴮ H B s +reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | ok q = expr (block₀ (λ r → p (trans r q))) +reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | warning (heap W) = heap W +reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | warning (block W) = expr (block₁ W) +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′ +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W) +reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ()) +reflectᴱ H (block var b ∈ T is return M ∙ B end) (return v) W′ = expr (block₁ (return W′)) reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) with preservationᴱ H M s reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) | ok q = block (local₀ (λ r → p (trans r q))) @@ -312,10 +326,14 @@ reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with refl reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W) reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′)) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W with just T ≡ᴹᵀ typeOfⱽ H v -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W | yes p = block (local₂ (reflect-substitutionᴮ _ v x p W)) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W | no p = {!!} -- block (local₀ λ r → p (cong just r)) -reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W = {!!} -- block (function₂ f (reflect-weakeningᴮ H (snoc defn) (reflect-substitutionᴮ _ _ f refl W))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′)) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (local₀ (λ r → q (trans (cong orBot (sym p)) (trans (sym (typeOfᴱⱽ v)) (sym r))))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-bot v +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (trans (cong orBot (sym p)) (sym (typeOfᴱⱽ v)))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W) +reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W′))) reflectᴮ H (return M ∙ B) (return s) (return W′) with reflectᴱ H M s W′ reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return W) @@ -325,10 +343,10 @@ reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warni reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′ reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ H {!!} (snoc defn) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = expr (function₀ f λ q → p (trans q r)) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = expr (function₁ f W) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ f W′))) | yes refl = expr (function₁ f (reflect-weakeningᴮ H B (snoc defn) W′)) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl with heap-weakeningᴮ H B (snoc defn) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | ok r = expr (function₀ λ q → p (trans q r)) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | warning W = expr (function₁ W) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′)) reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′) reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W @@ -339,7 +357,7 @@ reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W) reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′ reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′) reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W -reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ b W) +reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W) reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′ reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′ reflectᴴᴱ H (binexp M op N) s W′ = {!!} @@ -350,10 +368,10 @@ reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W = reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W) reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′ reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ H {!!} (snoc defn) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = block (function₀ f (λ q → p (trans q r))) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = block (function₁ f W) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ f W′))) | yes refl = block (function₁ f (reflect-weakeningᴮ H C (snoc defn) W′)) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl with heap-weakeningᴮ H C (snoc defn) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | ok r = block (function₀ (λ q → p (trans q r))) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₀ p))) | yes refl | warning W = block (function₁ W) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′)) reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′) reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W @@ -367,14 +385,16 @@ runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheck runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B) runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable x refl -runtimeWarningᴱ H (addr a) (SEGV p) = UnallocatedAddress a p -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w r) = {!!} -- app₁ (runtimeWarningᴱ H M err) +runtimeWarningᴱ H (addr a) (SEGV p) = UnallocatedAddress p +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-bot w +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = app₀ (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r)))) +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err) runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err) -runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ b (runtimeWarningᴮ H B err) +runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err) runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ v w p) = {!!} runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = {!!} -runtimeWarningᴱ H (binexp M op N) (bin₁ err) = {!!} +runtimeWarningᴱ H (binexp M op N) (bin₁ err) = {!bin₁!} runtimeWarningᴱ H (binexp M op N) (bin₂ err) = {!!} runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 4c2c8789..3384fc52 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -10,11 +10,13 @@ open import FFI.Data.Either using (Either) open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; app; function; block; binexp; done; return; local; nothing; orBot) open import Luau.Syntax using (Block; Expr; yes; nil; var; addr; number; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg) open import Luau.Type using (Type; nil; top; bot; number; _⇒_; tgt) +open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType) open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) open import Luau.Value using (Value; nil; addr; number; val) open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ) +open import Properties.Contradiction using (CONTRADICTION) open import Properties.Dec using (yes; no) open import Properties.Equality using (_≢_; sym; trans; cong) open import Properties.Product using (_×_; _,_) @@ -57,26 +59,31 @@ typeOfᴱⱽ nil = refl typeOfᴱⱽ (addr a) = refl typeOfᴱⱽ (number n) = refl +mustBeFunction : ∀ H Γ v → (bot ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v)) +mustBeFunction H Γ nil p = CONTRADICTION (p refl) +mustBeFunction H Γ (addr a) p = refl +mustBeFunction H Γ (number n) p = CONTRADICTION (p refl) + typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M)) typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) typeCheckᴱ H Γ nil = nil -typeCheckᴱ H Γ (var x) = var x refl -typeCheckᴱ H Γ (addr a) = addr a (orBot (typeOfᴹᴼ (H [ a ]ᴴ))) -typeCheckᴱ H Γ (number n) = number n +typeCheckᴱ H Γ (var x) = var refl +typeCheckᴱ H Γ (addr a) = addr (orBot (typeOfᴹᴼ (H [ a ]ᴴ))) +typeCheckᴱ H Γ (number n) = number typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N) -typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function f (typeCheckᴮ H (Γ ⊕ x ↦ T) B) -typeCheckᴱ H Γ (block var b ∈ T is B end) = block b (typeCheckᴮ H Γ B) -typeCheckᴱ H Γ (binexp M op N) = binexp op (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N) +typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B) +typeCheckᴱ H Γ (binexp M op N) = binexp (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N) -typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function f (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B) +typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B) typeCheckᴮ H Γ (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ ⊕ x ↦ T) B) typeCheckᴮ H Γ (return M ∙ B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B) typeCheckᴮ H Γ done = done typeCheckᴼ : ∀ H O → (⊢ᴼ O) typeCheckᴼ H nothing = nothing -typeCheckᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) = function f (typeCheckᴮ H (x ↦ T) B) +typeCheckᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (x ↦ T) B) typeCheckᴴ : ∀ H → (⊢ᴴ H) typeCheckᴴ H a {O} p = typeCheckᴼ H (O)