From 1f4d77bac9ef4b7a79a686d9525ba102b4f78c7f Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 15 Feb 2022 22:47:59 -0600 Subject: [PATCH] WIP --- prototyping/FFI/Data/Aeson.agda | 1 + prototyping/Luau/Heap.agda | 2 +- prototyping/Luau/OpSem.agda | 1 + prototyping/Luau/StrictMode.agda | 93 +++++---- prototyping/Luau/TypeCheck.agda | 88 ++++----- prototyping/Properties/Equality.agda | 6 + prototyping/Properties/StrictMode.agda | 260 ++++++++++++++++++++----- prototyping/Properties/TypeCheck.agda | 83 ++++---- 8 files changed, 354 insertions(+), 180 deletions(-) diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index 0d90a8d5..69c973a1 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -40,6 +40,7 @@ postulate postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m) ≡ just v) postulate lookup-empty : ∀ {A} k → (lookup {A} k empty ≡ nothing) +postulate singleton-insert-empty : ∀ {A} k (v : A) → (singleton k v ≡ insert k v empty) data Value : Set where object : KeyMap Value → Value diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index a6333e3f..1d5d9c30 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -5,7 +5,7 @@ open import FFI.Data.Maybe using (Maybe; just) open import FFI.Data.Vector using (Vector; length; snoc; empty) open import Luau.Addr using (Addr) open import Luau.Var using (Var) -open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end) +open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end) data HeapValue (a : Annotated) : Set where function_is_end : FunDec a → Block a → HeapValue a diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 2bc9be13..c7b33a75 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -6,6 +6,7 @@ open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end) open import Luau.Substitution using (_[_/_]ᴮ) open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg) open import Luau.Value using (addr; val) +open import Luau.Type using (Type) data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index bfd0c998..da0ec058 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -3,52 +3,79 @@ module Luau.StrictMode where open import Agda.Builtin.Equality using (_≡_) open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name) open import Luau.Type using (Type; strict; bot; top; nil; _⇒_; tgt) -open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) +open import Luau.Heap using (Heap) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) -open import Luau.TypeCheck(strict) using (_▷_⊢ᴮ_∋_∈_⊣_; _▷_⊢ᴱ_∋_∈_⊣_; var; addr; app; block; return; local) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∋_∈_⊣_; _⊢ᴱ_∋_∈_⊣_; var; addr; app; block; return; local; function) +open import Properties.Equality using (_≢_) +open import Properties.TypeCheck(strict) using (typeOfᴴ) src : Type → Type src = Luau.Type.src strict -data Warningᴱ {Σ Γ S} : ∀ {M T Δ} → (Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → Set -data Warningᴮ {Σ Γ S} : ∀ {B T Δ} → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → Set +data Warningᴱ (H : Heap yes) {Γ S} : ∀ {M T Δ} → (Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → Set +data Warningᴮ (H : Heap yes) {Γ S} : ∀ {B T Δ} → (Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → Set -data Warningᴱ {Σ Γ S} where +data Warningᴱ H {Γ S} where - bot : ∀ {M T Δ} {D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → + bot : ∀ {M T Δ} {D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → (T ≡ bot) → + ------------ + Warningᴱ H D + + addr : ∀ a T → + + (T ≢ typeOfᴴ(H [ a ]ᴴ)) → + ------------------------- + Warningᴱ H (addr a T) + + app₁ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + + Warningᴱ H D₁ → + ----------------- + Warningᴱ H (app D₁ D₂) + + app₂ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + + Warningᴱ H D₂ → + ----------------- + Warningᴱ H(app D₁ D₂) + + block : ∀ b {B T Δ} {D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → + + Warningᴮ H D → + ----------------- + Warningᴱ H(block b D) + +data Warningᴮ H {Γ S} where + + disagree : ∀ {B T Δ} {D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → + + (S ≢ T) → ----------- - Warningᴱ(D) + Warningᴮ H D - app₁ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + return : ∀ {M B T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂} → - Warningᴱ D₁ → - ----------------- - Warningᴱ(app D₁ D₂) - - app₂ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → - - Warningᴱ D₂ → - ----------------- - Warningᴱ(app D₁ D₂) - - block : ∀ b {B T Δ} {D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → - - Warningᴮ D → - ----------------- - Warningᴱ(block b D) - -data Warningᴮ {Σ Γ S} where - - return : ∀ {M B T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴮ top ∋ B ∈ U ⊣ Δ₂} → - - Warningᴱ(D₁) → + Warningᴱ H D₁ → ------------------ - Warningᴮ(return D₁ D₂) + Warningᴮ H (return D₁ D₂) - local₁ : ∀ {x M B T U V Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁} {D₂ : Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂} → + local₁ : ∀ {x M B T U V Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂} → - Warningᴱ(D₁) → + Warningᴱ H D₁ → -------------------- - Warningᴮ(local D₁ D₂) + Warningᴮ H (local D₁ D₂) + +-- data Warningᴴ {H} : ∀ {V T} → (H ▷ V ∈ T) → Set where + +-- nothing : + +-- ----------------- +-- Warningᴴ(nothing) + +-- function : ∀ f {x B T U V W} {D : (x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ (x ↦ W)} → + +-- Warningᴮ(D) → +-- -------------------- +-- Warningᴴ(function f D) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index b94592c4..a144a0f9 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -10,7 +10,6 @@ open import Luau.Addr using (Addr) open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.Value using (addr; val) open import Luau.Type using (Type; Mode; nil; bot; top; _⇒_; tgt) -open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import FFI.Data.Vector using (Vector) open import FFI.Data.Maybe using (Maybe; just; nothing) @@ -18,87 +17,70 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) src : Type → Type src = Luau.Type.src m -data _▷_⊢ᴮ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Block yes → Type → VarCtxt → Set -data _▷_⊢ᴱ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Expr yes → Type → VarCtxt → Set +data _⊢ᴮ_∋_∈_⊣_ : VarCtxt → Type → Block yes → Type → VarCtxt → Set +data _⊢ᴱ_∋_∈_⊣_ : VarCtxt → Type → Expr yes → Type → VarCtxt → Set -data _▷_⊢ᴮ_∋_∈_⊣_ where +data _⊢ᴮ_∋_∈_⊣_ where - done : ∀ {Σ S Γ} → + done : ∀ {S Γ} → ---------------------- - Σ ▷ Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ + Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ - return : ∀ {Σ M B S T U Γ Δ₁ Δ₂} → + return : ∀ {M B S T U Γ Δ₁ Δ₂} → - Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → - Σ ▷ Γ ⊢ᴮ top ∋ B ∈ U ⊣ Δ₂ → + Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → + Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂ → --------------------------------- - Σ ▷ Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ + Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ - local : ∀ {Σ x M B S T U V Γ Δ₁ Δ₂} → + local : ∀ {x M B S T U V Γ Δ₁ Δ₂} → - Σ ▷ Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → - Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → + Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → + (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → ---------------------------------------------------------- - Σ ▷ Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) + Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) - function : ∀ {Σ f x B C S T U V W Γ Δ₁ Δ₂} → + function : ∀ {f x B C S T U V W Γ Δ₁ Δ₂} → - Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ C ∈ V ⊣ Δ₁ → - Σ ▷ (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ W ⊣ Δ₂ → + (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ C ∈ V ⊣ Δ₁ → + (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ W ⊣ Δ₂ → --------------------------------------------------------------------------------- - Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) + Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) -data _▷_⊢ᴱ_∋_∈_⊣_ where +data _⊢ᴱ_∋_∈_⊣_ where - nil : ∀ {Σ S Γ} → + nil : ∀ {S Γ} → ---------------------- - Σ ▷ Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ + Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ - var : ∀ x {Σ S T Γ} → + var : ∀ x {S T Γ} → T ≡ Γ [ x ]ⱽ → ---------------------------- - Σ ▷ Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) + Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) - addr : ∀ a {Σ S T Γ} → + addr : ∀ a T {S Γ} → - T ≡ Σ [ a ]ᴬ → - ---------------------------- - Σ ▷ Γ ⊢ᴱ S ∋ addr a ∈ T ⊣ ∅ + ------------------------- + Γ ⊢ᴱ S ∋ (addr a) ∈ T ⊣ ∅ - app : ∀ {Σ M N S T U Γ Δ₁ Δ₂} → + app : ∀ {M N S T U Γ Δ₁ Δ₂} → - Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁ → - Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → + Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁ → + Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → -------------------------------------- - Σ ▷ Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) + Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) - function : ∀ {Σ f x B S T U V Γ Δ} → + function : ∀ {f x B S T U V Γ Δ} → - Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ → + (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ → ----------------------------------------------------------------------- - Σ ▷ Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) + Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) - block : ∀ b {Σ B S T Γ Δ} → + block : ∀ b {B S T Γ Δ} → - Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → + Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → ---------------------------------------------------- - Σ ▷ Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ - -data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → Type → Set where - - nothing : - - ----------------- - Σ ▷ nothing ∈ bot - - function : ∀ {f x B T U V W} → - - Σ ▷ (x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ (x ↦ W) → - --------------------------------------------------------- - Σ ▷ just (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) - -_▷_✓ : AddrCtxt → Heap yes → Set -(Σ ▷ H ✓) = (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) + Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ diff --git a/prototyping/Properties/Equality.agda b/prototyping/Properties/Equality.agda index 605b690d..c027bee3 100644 --- a/prototyping/Properties/Equality.agda +++ b/prototyping/Properties/Equality.agda @@ -12,6 +12,12 @@ trans refl refl = refl cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b) cong f refl = refl +subst₁ : ∀ {A : Set} {a b : A} (F : A → Set) → (a ≡ b) → (F a) → (F b) +subst₁ F refl x = x + +subst₂ : ∀ {A B : Set} {a b : A} {c d : B} (F : A → B → Set) → (a ≡ b) → (c ≡ d) → (F a c) → (F b d) +subst₂ F refl refl x = x + _≢_ : ∀ {A : Set} → A → A → Set (a ≢ b) = ¬(a ≡ b) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index f84b739f..31a44580 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -5,73 +5,225 @@ module Properties.StrictMode where import Agda.Builtin.Equality.Rewrite open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Maybe using (Maybe; just; nothing) -open import Luau.Heap using (Heap; HeapValue; function_is_end; defn; alloc; ok; next; lookup-next) renaming (_[_] to _[_]ᴴ) -open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; app₁; app₂; block; return; local₁) -open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; nil; block_is_end; done; return; local_←_; _∙_; fun; arg) +open import Luau.Heap using (Heap; HeapValue; function_is_end; defn; alloc; ok; next; lookup-next) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; disagree; addr; app₁; app₂; block; return; local₁) +open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ) +open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg) open import Luau.Type using (Type; strict; nil; _⇒_; bot; tgt) -open import Luau.TypeCheck(strict) using (_▷_⊢ᴮ_∋_∈_⊣_; _▷_⊢ᴱ_∋_∈_⊣_; _▷_∈_; _▷_✓; nil; var; addr; app; function; block; done; return; local; nothing) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∋_∈_⊣_; _⊢ᴱ_∋_∈_⊣_; nil; var; addr; app; function; block; done; return; local) open import Luau.Value using (val; nil; addr) +open import Luau.Addr using (_≡ᴬ_) open import Luau.AddrCtxt using (AddrCtxt) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ∅-[]) renaming (_[_] to _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅) open import Properties.Remember using (remember; _,_) -open import Properties.Equality using (cong) -open import Properties.TypeCheck(strict) using (typeOfᴱ; typeCheckᴱ) +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ᴮ; typeCheckᴱ; typeCheckᴮ) open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) -{-# REWRITE ∅-[] #-} +{-# REWRITE lookup-next #-} -heap-miss : ∀ {Σ HV T} → (Σ ▷ HV ∈ T) → (HV ≡ nothing) → (T ≡ bot) -heap-miss nothing refl = refl +src = Luau.Type.src strict -data ProgressResultᴱ {Σ Γ S M T Δ} (H : Heap yes) (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) : Set -data ProgressResultᴮ {Σ Γ S B T Δ} (H : Heap yes) (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) : Set +data _⊑_ (H : Heap yes) : Heap yes → Set where + refl : (H ⊑ H) + snoc : ∀ {H′ H″ a V} → (H ⊑ H′) → (H″ ≡ᴴ H′ ⊕ a ↦ V) → (H ⊑ H″) -data ProgressResultᴱ {Σ Γ S M T Δ} H D where +warning-⊑ : ∀ {H H′ Γ Δ S T M} {D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → (H ⊑ H′) → (Warningᴱ H′ D) → Warningᴱ H D +warning-⊑ = {!!} - value : ∀ V → (M ≡ val V) → ProgressResultᴱ H D - warning : (Warningᴱ D) → ProgressResultᴱ H D - step : ∀ {M′ H′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → ProgressResultᴱ H D +data TypeOfᴱ-⊑-Result H H′ Γ M : Set where + ok : (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M) → TypeOfᴱ-⊑-Result H H′ Γ M + warning : (∀ {S} → Warningᴱ H (typeCheckᴱ H Γ S M)) → TypeOfᴱ-⊑-Result H H′ Γ M -data ProgressResultᴮ {Σ Γ S B T Δ} H D where +data TypeOfᴮ-⊑-Result H H′ Γ B : Set where + ok : (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B) → TypeOfᴮ-⊑-Result H H′ Γ B + warning : (∀ {S} → Warningᴮ H (typeCheckᴮ H Γ S B)) → TypeOfᴮ-⊑-Result H H′ Γ B - done : (B ≡ done) → ProgressResultᴮ H D - return : ∀ V {C} → (B ≡ (return (val V) ∙ C)) → ProgressResultᴮ H D - warning : (Warningᴮ D) → ProgressResultᴮ H D - step : ∀ {B′ H′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → ProgressResultᴮ H D +typeOfᴱ-⊑ : ∀ {H H′ Γ M} → (H ⊑ H′) → (TypeOfᴱ-⊑-Result H H′ Γ M) +typeOfᴱ-⊑ = {!!} -progressᴱ : ∀ {Σ Γ S M T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴱ H D -progressᴮ : ∀ {Σ Γ S B T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴮ H D +typeOfᴮ-⊑ : ∀ {H H′ Γ B} → (H ⊑ H′) → (TypeOfᴮ-⊑-Result H H′ Γ B) +typeOfᴮ-⊑ = {!!} -progressᴱ H h nil _ = value nil refl -progressᴱ H h (var x p) refl = warning (bot p) -progressᴱ H h (addr a refl) _ = value (addr a) refl -progressᴱ H h (app D₁ D₂) p with progressᴱ H h D₁ p -progressᴱ H h (app nil D₂) p | value nil refl = warning (bot refl) -progressᴱ H h (app (var _ _) D₂) p | value nil () -progressᴱ H h (app (app _ _) D₂) p | value nil () -progressᴱ H h (app (function _) D₂) p | value nil () -progressᴱ H h (app (block _ _) D₂) p | value nil () -progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl with remember(H [ a ]ᴴ) -progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (nothing , r) = warning (bot (cong tgt (heap-miss (h a) r))) -progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (just(function f ⟨ var x ∈ S ⟩∈ T is B end) , r) = step (beta r) -progressᴱ H h (app D₁ D₂) p | warning W = warning (app₁ W) -progressᴱ H h (app D₁ D₂) p | step S = step (app S) -progressᴱ H h (function D) _ with alloc H _ -progressᴱ H h (function D) _ | ok a H′ r = step (function r) -progressᴱ H h (block b D) q with progressᴮ H h D q -progressᴱ H h (block b D) q | done refl = step done -progressᴱ H h (block b D) q | return V refl = step (return refl) -progressᴱ H h (block b D) q | warning W = warning (block b W) -progressᴱ H h (block b D) q | step S = step (block S) +blah : ∀ {H H′ Γ S S′ M} → (H ⊑ H′) → (S ≡ S′) → (Warningᴱ H′ (typeCheckᴱ H′ Γ S′ M)) → (Warningᴱ H (typeCheckᴱ H Γ S M)) +blah = {!!} -progressᴮ H h done q = done refl -progressᴮ H h (return D₁ D₂) q with progressᴱ H h D₁ q -progressᴮ H h (return D₁ D₂) q | value V refl = return V refl -progressᴮ H h (return D₁ D₂) q | warning W = warning (return W) -progressᴮ H h (return D₁ D₂) q | step S = step (return S) -progressᴮ H h (local D₁ D₂) q with progressᴱ H h D₁ q -progressᴮ H h (local D₁ D₂) q | value V refl = step subst -progressᴮ H h (local D₁ D₂) q | warning W = warning (local₁ W) -progressᴮ H h (local D₁ D₂) q | step S = step (local S) -progressᴮ H h (function D₁ D₂) q with alloc H _ -progressᴮ H h (function D₁ D₂) q | ok a H′ r = step (function r) +bloz : ∀ {H Γ S S′ M} → (S ≡ S′) → (Warningᴱ H (typeCheckᴱ H Γ S′ M)) → (Warningᴱ H (typeCheckᴱ H Γ S M)) +bloz = {!!} + +redn-⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′) +redn-⊑ = {!!} + +substitutivityᴱ : ∀ {Γ T H M v x} → (T ≡ typeOfᴱ H Γ (val v)) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ)) +substitutivityᴮ : ∀ {Γ T H B v x} → (T ≡ typeOfᴱ H Γ (val v)) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) + +substitutivityᴱ = {!!} +substitutivityᴮ = {!!} + +preservationᴱ : ∀ {H H′ M M′ Γ} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M′) +preservationᴮ : ∀ {H H′ B B′ Γ} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B′) + +preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = refl +preservationᴱ (app s) = cong tgt (preservationᴱ s) +preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ T} p) = trans (cong tgt (cong typeOfᴴ p)) {!!} +preservationᴱ (block s) = preservationᴮ s +preservationᴱ (return p) = refl +preservationᴱ done = refl + +preservationᴮ (local {x = var x ∈ T} {B = B} s) with typeOfᴮ-⊑ {B = B} (redn-⊑ s) +preservationᴮ (local {x = var x ∈ T} s) | ok p = p +preservationᴮ (local {x = var x ∈ T} s) | warning W = {!!} +preservationᴮ (subst {x = var x ∈ T} {B = B}) = substitutivityᴮ {B = B} {!!} +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) with typeOfᴮ-⊑ {B = B} (snoc refl defn) +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | ok r = trans r (substitutivityᴮ {T = S ⇒ T} {B = B} refl) +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | warning W = {!!} +preservationᴮ (return s) = preservationᴱ s + +reflectᴱ : ∀ {H H′ M M′ S} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ S M′) → Warningᴱ H (typeCheckᴱ H ∅ S M) +reflectᴮ : ∀ {H H′ B B′ S} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ S B′) → Warningᴮ H (typeCheckᴮ H ∅ S B) + +reflectᴱ s W with redn-⊑ s +reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (addr a _ r) | p = CONTRADICTION (r refl) +reflectᴱ (app s) (bot x) | p = {!x!} +reflectᴱ (app s) (app₁ W) | p with typeOfᴱ-⊑ p +reflectᴱ (app s) (app₁ W) | p | ok q = app₁ (bloz (cong (λ ∙ → ∙ ⇒ _) q) (reflectᴱ s W)) +reflectᴱ (app s) (app₁ W) | p | warning W′ = app₂ W′ +reflectᴱ (app s) (app₂ W) | p = app₂ (blah p (cong src (preservationᴱ s)) W) +reflectᴱ (beta s) (bot x₁) | p = {!!} +reflectᴱ (beta {F = f ⟨ var x ∈ T ⟩∈ U} q) (block _ (disagree x₁)) | p = {!!} +reflectᴱ (beta {F = f ⟨ var x ∈ T ⟩∈ U} q) (block _ (local₁ W)) | p = app₂ (bloz (cong src (cong typeOfᴴ q)) W) +reflectᴱ (block s) (bot x₁) | p = {!!} +reflectᴱ (block s) (block b W) | p = block b (reflectᴮ s W) +reflectᴱ (return q) W | p = block _ (return W) +reflectᴱ done (bot x) | p = {!!} + +reflectᴮ s = {!!} + +-- reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (bot ()) +-- reflectᴱ (function defn) (addr a T q) = CONTRADICTION (q refl) +-- reflectᴱ (app s) (bot x) = {!x!} +-- reflectᴱ (app s) (app₁ W) = app₁ {!reflectᴱ s W!} +-- reflectᴱ (app s) (app₂ W) = {!!} +-- reflectᴱ (beta x) W = {!!} +-- reflectᴱ (block x) W = {!!} +-- reflectᴱ (return x) W = {!!} +-- reflectᴱ done W = {!!} + +-- heap-miss : ∀ {Σ HV T} → (Σ ▷ HV ∈ T) → (HV ≡ nothing) → (T ≡ bot) +-- heap-miss nothing refl = refl + +-- data ProgressResultᴱ {Σ Γ S M T Δ} (H : Heap yes) (D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) : Set +-- data ProgressResultᴮ {Σ Γ S B T Δ} (H : Heap yes) (D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) : Set + +-- data ProgressResultᴱ {Σ Γ S M T Δ} H D where + +-- value : ∀ V → (M ≡ val V) → ProgressResultᴱ H D +-- warning : (Warningᴱ Σ D) → ProgressResultᴱ H D +-- step : ∀ {M′ H′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → ProgressResultᴱ H D + +-- data ProgressResultᴮ {Σ Γ S B T Δ} H D where + +-- done : (B ≡ done) → ProgressResultᴮ H D +-- return : ∀ V {C} → (B ≡ (return (val V) ∙ C)) → ProgressResultᴮ H D +-- warning : (Warningᴮ Σ D) → ProgressResultᴮ H D +-- step : ∀ {B′ H′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → ProgressResultᴮ H D + +-- progressᴱ : ∀ {Σ Γ S M T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴱ H D +-- progressᴮ : ∀ {Σ Γ S B T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴮ H D + +-- progressᴱ H h nil _ = value nil refl +-- progressᴱ H h (var x p) refl = warning (bot p) +-- progressᴱ H h (addr a refl) _ = value (addr a) refl +-- progressᴱ H h (app D₁ D₂) p with progressᴱ H h D₁ p +-- progressᴱ H h (app nil D₂) p | value nil refl = warning (bot refl) +-- progressᴱ H h (app (var _ _) D₂) p | value nil () +-- progressᴱ H h (app (app _ _) D₂) p | value nil () +-- progressᴱ H h (app (function _) D₂) p | value nil () +-- progressᴱ H h (app (block _ _) D₂) p | value nil () +-- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl with remember(H [ a ]ᴴ) +-- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (nothing , r) = warning (bot (cong tgt (heap-miss (h a) r))) +-- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (just(function f ⟨ var x ∈ S ⟩∈ T is B end) , r) = step (beta r) +-- progressᴱ H h (app D₁ D₂) p | warning W = warning (app₁ W) +-- progressᴱ H h (app D₁ D₂) p | step S = step (app S) +-- progressᴱ H h (function D) _ with alloc H _ +-- progressᴱ H h (function D) _ | ok a H′ r = step (function r) +-- progressᴱ H h (block b D) q with progressᴮ H h D q +-- progressᴱ H h (block b D) q | done refl = step done +-- progressᴱ H h (block b D) q | return V refl = step (return refl) +-- progressᴱ H h (block b D) q | warning W = warning (block b W) +-- progressᴱ H h (block b D) q | step S = step (block S) + +-- progressᴮ H h done q = done refl +-- progressᴮ H h (return D₁ D₂) q with progressᴱ H h D₁ q +-- progressᴮ H h (return D₁ D₂) q | value V refl = return V refl +-- progressᴮ H h (return D₁ D₂) q | warning W = warning (return W) +-- progressᴮ H h (return D₁ D₂) q | step S = step (return S) +-- progressᴮ H h (local D₁ D₂) q with progressᴱ H h D₁ q +-- progressᴮ H h (local D₁ D₂) q | value V refl = step subst +-- progressᴮ H h (local D₁ D₂) q | warning W = warning (local₁ W) +-- progressᴮ H h (local D₁ D₂) q | step S = step (local S) +-- progressᴮ H h (function D₁ D₂) q with alloc H _ +-- progressᴮ H h (function D₁ D₂) q | ok a H′ r = step (function r) + +import FFI.Data.Aeson +{-# REWRITE FFI.Data.Aeson.singleton-insert-empty #-} + +_≡ᵀ_ : (T U : Type) → Dec (T ≡ U) +_≡ᵀ_ = {!!} + +-- data LookupResult {Σ V S} (D : Σ ▷ V ∈ S) : Set where + +-- function : ∀ f {x B T U W} → +-- (S ≡ (T ⇒ U)) → +-- (V ≡ just(function f ⟨ var x ∈ T ⟩∈ U is B end)) → +-- (Σ ▷ (x ↦ T) ⊢ᴮ U ∋ B ∈ U ⊣ (x ↦ W)) → +-- LookupResult D + +-- warningᴴ : +-- Warningᴴ(D) → +-- LookupResult D + +-- lookup : ∀ {Σ V T} (D : Σ ▷ V ∈ T) → LookupResult D +-- lookup nothing = warningᴴ nothing +-- lookup (function f {U = U} {V = V} D) with U ≡ᵀ V +-- lookup (function f D) | yes refl = function f refl refl D +-- lookup (function f D) | no p = warningᴴ (function f (disagree p)) + +-- data PreservationResultᴮ {Σ S Δ T H B} (D : ∅ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) M′ H′ : Set where + +-- ok : ∀ {Δ′} → (∅ ⊢ᴮ S ∋ M′ ∈ T ⊣ Δ′) → PreservationResultᴮ D M′ H′ +-- warning : Warningᴮ Σ D → PreservationResultᴮ D M′ H′ + +-- data PreservationResultᴱ {Σ S Δ T M} (D : ∅ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) M′ : Set where + +-- ok : ∀ {Δ′} → (∅ ⊢ᴱ S ∋ M′ ∈ T ⊣ Δ′) → PreservationResultᴱ D M′ H′ +-- warning : Warningᴱ Σ D → PreservationResultᴱ D M′ H′ + +-- preservationᴱ : ∀ {Σ S Δ T H H′ M M′} → (D : ∅ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (s : H ⊢ M ⟶ᴱ M′ ⊣ H′) → PreservationResultᴱ D M′ H′ +-- preservationᴱ {S = S} {T = T} h D s with S ≡ᵀ T +-- preservationᴱ h D s | no p = warning (disagree p) +-- preservationᴱ h (app D₁ D₂) (app s) | yes refl with preservationᴱ h D₁ s +-- preservationᴱ h (app D₁ D₂) (app s) | yes refl | ok h′ D₁′ = ok h′ (app D₁′ {!D₂!}) +-- preservationᴱ h (app D₁ D₂) (app s) | yes refl | warning W = warning (app₁ W) +-- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl with lookup (h a) +-- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | function f r₁ r₂ D₁ with trans p r₁ | trans (sym q) r₂ +-- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | function f r₁ r₂ D₁ | refl | refl = ok h (block f (local D₂ D₁)) +-- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | warningᴴ W = warningᴴ a W + +-- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) with subst₂ (λ X Y → _ ▷ X ∈ Y) q (sym p) (h a) +-- -- preservationᴱ {S = S} h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} {V = V′} D with S ≡ᵀ U′ | U′ ≡ᵀ V′ +-- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} {V = V′} D | yes refl | yes refl = ok h (block _ (local D₂ D)) +-- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} D | no r | _ = warningᴱ (disagree r) +-- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} D | yes refl | no r = warningᴴ a {!function f (disagree r)!} -- (subst₁ Warningᴴ {!!} {!(function f (disagree r))!}) -- (function f (disagree r)) + +-- -- with src T ≡ᵀ U -- = ok h (block f (local {!D₂!} {!!})) +-- -- preservationᴱ h (app {T = T} {U = U} D₁ D₂) (beta {F = f ⟨ var x ∈ _ ⟩∈ R} p) | yes refl = ok h (block f (local D₂ {!!})) -- with src T ≡ᵀ S -- = ok h (block f (local {!D₂!} {!!})) +-- -- preservationᴱ h (app {T = T} {U = U} D₁ D₂) (beta {F = f ⟨ var x ∈ S ⟩∈ R} p) | no q = warning (app₀ {!q!}) -- with src T ≡ᵀ S -- = ok h (block f (local {!D₂!} {!!})) +-- preservationᴱ h D s | yes refl = {!!} +-- preservationᴱ h (function D) (function p) = {!x!} +-- preservationᴱ h (block b D) (block s) = {!!} +-- preservationᴱ h (block b D) (return p) = {!x!} +-- preservationᴱ h (block b D) done = {!!} diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 8e6b9bb0..98495f25 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -5,13 +5,14 @@ module Properties.TypeCheck (m : Mode) where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Maybe using (Maybe; just; nothing) open import FFI.Data.Either using (Either) -open import Luau.TypeCheck(m) using (_▷_⊢ᴱ_∋_∈_⊣_; _▷_⊢ᴮ_∋_∈_⊣_; nil; var; addr; app; function; block; done; return; local) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∋_∈_⊣_; _⊢ᴮ_∋_∈_⊣_; nil; var; addr; app; function; block; done; return; local) open import Luau.Syntax using (Block; Expr; yes; nil; var; addr; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg) -open import Luau.Type using (Type; nil; top; _⇒_; tgt) +open import Luau.Type using (Type; nil; top; bot; _⇒_; tgt) open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_; ⊕-[]) renaming (_[_] to _[_]ⱽ) +open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) -open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) +open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) open import Properties.Dec using (yes; no) open import Properties.Equality using (_≢_; sym; trans; cong) open import Properties.Remember using (remember; _,_) @@ -19,47 +20,51 @@ open import Properties.Remember using (remember; _,_) src : Type → Type src = Luau.Type.src m -typeOfᴱ : AddrCtxt → VarCtxt → (Expr yes) → Type -typeOfᴮ : AddrCtxt → VarCtxt → (Block yes) → Type +typeOfᴴ : Maybe(HeapValue yes) → Type +typeOfᴴ nothing = bot +typeOfᴴ (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) -typeOfᴱ Σ Γ nil = nil -typeOfᴱ Σ Γ (var x) = Γ [ x ]ⱽ -typeOfᴱ Σ Γ (addr a) = Σ [ a ]ᴬ -typeOfᴱ Σ Γ (M $ N) = tgt(typeOfᴱ Σ Γ M) -typeOfᴱ Σ Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T -typeOfᴱ Σ Γ (block b is B end) = typeOfᴮ Σ Γ B +typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type +typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type -typeOfᴮ Σ Γ (function f ⟨ var x ∈ S ⟩∈ T is C end ∙ B) = typeOfᴮ Σ (Γ ⊕ f ↦ (S ⇒ T)) B -typeOfᴮ Σ Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ Σ (Γ ⊕ x ↦ T) B -typeOfᴮ Σ Γ (return M ∙ B) = typeOfᴱ Σ Γ M -typeOfᴮ Σ Γ done = nil +typeOfᴱ H Γ nil = nil +typeOfᴱ H Γ (var x) = Γ [ x ]ⱽ +typeOfᴱ H Γ (addr a) = typeOfᴴ (H [ a ]ᴴ) +typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M) +typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T +typeOfᴱ H Γ (block b is B end) = typeOfᴮ H Γ B -contextOfᴱ : AddrCtxt → VarCtxt → Type → (Expr yes) → VarCtxt -contextOfᴮ : AddrCtxt → VarCtxt → Type → (Block yes) → VarCtxt +typeOfᴮ H Γ (function f ⟨ var x ∈ S ⟩∈ T is C end ∙ B) = typeOfᴮ H (Γ ⊕ f ↦ (S ⇒ T)) B +typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B +typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M +typeOfᴮ H Γ done = nil -contextOfᴱ Σ Γ S nil = ∅ -contextOfᴱ Σ Γ S (var x) = (x ↦ S) -contextOfᴱ Σ Γ S (addr a) = ∅ -contextOfᴱ Σ Γ S (M $ N) = (contextOfᴱ Σ Γ (U ⇒ S) M) ⋒ (contextOfᴱ Σ Γ (src T) N) where T = typeOfᴱ Σ Γ M; U = typeOfᴱ Σ Γ N -contextOfᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = (contextOfᴮ Σ (Γ ⊕ x ↦ T) U B) ⊝ x -contextOfᴱ Σ Γ S (block b is B end) = (contextOfᴮ Σ Γ S B) +contextOfᴱ : Heap yes → VarCtxt → Type → (Expr yes) → VarCtxt +contextOfᴮ : Heap yes → VarCtxt → Type → (Block yes) → VarCtxt -contextOfᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = ((contextOfᴮ Σ (Γ ⊕ x ↦ T) U C) ⊝ x) ⋒ ((contextOfᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B) ⊝ f) -contextOfᴮ Σ Γ S (local var x ∈ T ← M ∙ B) = (contextOfᴱ Σ Γ T M) ⋒ ((contextOfᴮ Σ (Γ ⊕ x ↦ T)S B) ⊝ x) -contextOfᴮ Σ Γ S (return M ∙ B) = (contextOfᴱ Σ Γ S M) -contextOfᴮ Σ Γ S done = ∅ +contextOfᴱ H Γ S nil = ∅ +contextOfᴱ H Γ S (var x) = (x ↦ S) +contextOfᴱ H Γ S (addr a) = ∅ +contextOfᴱ H Γ S (M $ N) = (contextOfᴱ H Γ (U ⇒ S) M) ⋒ (contextOfᴱ H Γ (src T) N) where T = typeOfᴱ H Γ M; U = typeOfᴱ H Γ N +contextOfᴱ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = (contextOfᴮ H (Γ ⊕ x ↦ T) U B) ⊝ x +contextOfᴱ H Γ S (block b is B end) = (contextOfᴮ H Γ S B) -typeCheckᴱ : ∀ Σ Γ S M → (Σ ▷ Γ ⊢ᴱ S ∋ M ∈ (typeOfᴱ Σ Γ M) ⊣ (contextOfᴱ Σ Γ S M)) -typeCheckᴮ : ∀ Σ Γ S B → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ Σ Γ B) ⊣ (contextOfᴮ Σ Γ S B)) +contextOfᴮ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = ((contextOfᴮ H (Γ ⊕ x ↦ T) U C) ⊝ x) ⋒ ((contextOfᴮ H (Γ ⊕ f ↦ (T ⇒ U)) S B) ⊝ f) +contextOfᴮ H Γ S (local var x ∈ T ← M ∙ B) = (contextOfᴱ H Γ T M) ⋒ ((contextOfᴮ H (Γ ⊕ x ↦ T)S B) ⊝ x) +contextOfᴮ H Γ S (return M ∙ B) = (contextOfᴱ H Γ S M) +contextOfᴮ H Γ S done = ∅ -typeCheckᴱ Σ Γ S nil = nil -typeCheckᴱ Σ Γ S (var x) = var x refl -typeCheckᴱ Σ Γ S (addr a) = addr a refl -typeCheckᴱ Σ Γ S (M $ N) = app (typeCheckᴱ Σ Γ (typeOfᴱ Σ Γ N ⇒ S) M) (typeCheckᴱ Σ Γ (src (typeOfᴱ Σ Γ M)) N) -typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = function(typeCheckᴮ Σ (Γ ⊕ x ↦ T) U B) -typeCheckᴱ Σ Γ S (block b is B end) = block b (typeCheckᴮ Σ Γ S B) +typeCheckᴱ : ∀ H Γ S M → (Γ ⊢ᴱ S ∋ M ∈ (typeOfᴱ H Γ M) ⊣ (contextOfᴱ H Γ S M)) +typeCheckᴮ : ∀ H Γ S B → (Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ H Γ B) ⊣ (contextOfᴮ H Γ S B)) -typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function(typeCheckᴮ Σ (Γ ⊕ x ↦ T) U C) (typeCheckᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B) -typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ Σ Γ T M) (typeCheckᴮ Σ (Γ ⊕ x ↦ T) S B) -typeCheckᴮ Σ Γ S (return M ∙ B) = return (typeCheckᴱ Σ Γ S M) (typeCheckᴮ Σ Γ top B) -typeCheckᴮ Σ Γ S done = done +typeCheckᴱ H Γ S nil = nil +typeCheckᴱ H Γ S (var x) = var x refl +typeCheckᴱ H Γ S (addr a) = addr a (typeOfᴴ (H [ a ]ᴴ)) +typeCheckᴱ H Γ S (M $ N) = app (typeCheckᴱ H Γ (typeOfᴱ H Γ N ⇒ S) M) (typeCheckᴱ H Γ (src (typeOfᴱ H Γ M)) N) +typeCheckᴱ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = function(typeCheckᴮ H (Γ ⊕ x ↦ T) U B) +typeCheckᴱ H Γ S (block b is B end) = block b (typeCheckᴮ H Γ S B) + +typeCheckᴮ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function(typeCheckᴮ H (Γ ⊕ x ↦ T) U C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) S B) +typeCheckᴮ H Γ S (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ T M) (typeCheckᴮ H (Γ ⊕ x ↦ T) S B) +typeCheckᴮ H Γ S (return M ∙ B) = return (typeCheckᴱ H Γ S M) (typeCheckᴮ H Γ nil B) +typeCheckᴮ H Γ S done = done