From 90229615b5f23edaec296bff4990678053a36b20 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 17 Feb 2022 18:24:36 -0600 Subject: [PATCH] WIP --- prototyping/FFI/Data/Vector.agda | 2 + prototyping/Luau/AddrCtxt.agda | 18 --- prototyping/Luau/Heap.agda | 23 ++-- prototyping/Luau/RuntimeError.agda | 3 +- prototyping/Luau/StrictMode.agda | 77 ++++++++++-- prototyping/Luau/TypeCheck.agda | 87 ++++--------- prototyping/Luau/VarCtxt.agda | 8 +- prototyping/Properties/StrictMode.agda | 167 ++++++++++++++++++------- prototyping/Properties/TypeCheck.agda | 48 ++++--- 9 files changed, 266 insertions(+), 167 deletions(-) delete mode 100644 prototyping/Luau/AddrCtxt.agda diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 0835698f..8463769f 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -9,6 +9,7 @@ open import Agda.Builtin.Nat using (Nat) open import FFI.Data.Bool using (Bool; false; true) open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt) open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Properties.Equality using (_≢_) {-# FOREIGN GHC import qualified Data.Vector #-} @@ -35,6 +36,7 @@ postulate postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0) postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x) postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x) +postulate lookup-snoc-not : ∀ {A n} (x : A) (v : Vector A) → (n ≢ length v) → (lookup v n ≡ lookup (snoc v x) n) {-# REWRITE length-empty lookup-snoc lookup-snoc-empty #-} diff --git a/prototyping/Luau/AddrCtxt.agda b/prototyping/Luau/AddrCtxt.agda deleted file mode 100644 index 592c4645..00000000 --- a/prototyping/Luau/AddrCtxt.agda +++ /dev/null @@ -1,18 +0,0 @@ -{-# OPTIONS --rewriting #-} - -module Luau.AddrCtxt where - -open import Luau.Type using (Type) -open import Luau.Addr using (Addr) -open import FFI.Data.Vector using (Vector; empty; lookup) -open import FFI.Data.Maybe using (Maybe; just; nothing) -open import Luau.VarCtxt using (orBot) - -AddrCtxt : Set -AddrCtxt = Vector Type - -∅ : AddrCtxt -∅ = empty - -_[_] : AddrCtxt → Addr → Type -Σ [ a ] = orBot(lookup Σ a) diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index 6e30caa8..3c31c95b 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -4,31 +4,34 @@ module Luau.Heap where open import Agda.Builtin.Equality using (_≡_) open import FFI.Data.Maybe using (Maybe; just) -open import FFI.Data.Vector using (Vector; length; snoc; empty) +open import FFI.Data.Vector using (Vector; length; snoc; empty; lookup-snoc-not) open import Luau.Addr using (Addr) open import Luau.Var using (Var) open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end) +open import Properties.Equality using (_≢_) -data HeapValue (a : Annotated) : Set where - function_is_end : FunDec a → Block a → HeapValue a +-- Heap-allocated objects +data Object (a : Annotated) : Set where + + function_is_end : FunDec a → Block a → Object a Heap : Annotated → Set -Heap a = Vector (HeapValue a) +Heap a = Vector (Object a) -data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where +data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → Object a → Set where defn : ∀ {H val} → ----------------------------------- (snoc H val) ≡ H ⊕ (length H) ↦ val -_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a) +_[_] : ∀ {a} → Heap a → Addr → Maybe (Object a) _[_] = FFI.Data.Vector.lookup ∅ : ∀ {a} → Heap a ∅ = empty -data AllocResult a (H : Heap a) (V : HeapValue a) : Set where +data AllocResult a (H : Heap a) (V : Object a) : Set where ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V alloc : ∀ {a} H V → AllocResult a H V @@ -37,5 +40,9 @@ alloc H V = ok (length H) (snoc H V) defn next : ∀ {a} → Heap a → Addr next = length -allocated : ∀ {a} → Heap a → HeapValue a → Heap a +allocated : ∀ {a} → Heap a → Object a → Heap a allocated = snoc + +lookup-not-allocated : ∀ {a} {H H′ : Heap a} {b c O} → (H′ ≡ H ⊕ b ↦ O) → (c ≢ b) → (H [ c ] ≡ H′ [ c ]) +lookup-not-allocated {H = H} {O = O} defn p = lookup-snoc-not O H p + diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 91bcfd2c..0ec8b4e2 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -6,12 +6,13 @@ open import Agda.Builtin.Equality using (_≡_) open import Luau.Heap using (Heap; _[_]) open import FFI.Data.Maybe using (just; nothing) open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_) +open import Luau.Value using (val) data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M) + NilIsNotAFunction : ∀ {V} → RuntimeErrorᴱ H (nil $ val V) UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x) SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a) app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N) diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index e4823912..a72b5c4d 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -8,9 +8,10 @@ open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; var_∈_; open import Luau.Type using (Type; strict; bot; top; nil; _⇒_; tgt) open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; var; addr; app; block; return; local; function) +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ᴴ; typeCheckᴮ) +open import Properties.TypeCheck(strict) using (typeCheckᴮ) +open import Properties.Product using (_,_) src : Type → Type src = Luau.Type.src strict @@ -20,19 +21,18 @@ data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set data Warningᴱ H {Γ} where - BadlyTypedFunctionAddress : ∀ a f {x S T U B} → - - (H [ a ]ᴴ ≡ just (function f ⟨ var x ∈ T ⟩∈ U is B end)) → - Warningᴮ H (typeCheckᴮ H (x ↦ T) B) → - -------------------------------------------------------- - Warningᴱ H (addr a S) - UnallocatedAddress : ∀ a {T} → (H [ a ]ᴴ ≡ nothing) → - -------------------------------------------------------- + --------------------- Warningᴱ H (addr a T) + UnboundVariable : ∀ x {T} {p} → + + (Γ [ x ]ⱽ ≡ nothing) → + ------------------------ + Warningᴱ H (var x {T} p) + app₀ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → (src T ≢ U) → @@ -95,6 +95,12 @@ 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} → + + (U ≢ V) → + ------------------------------------- + Warningᴮ H (function f {U = U} D₁ D₂) + function₁ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → Warningᴮ H D₁ → @@ -106,3 +112,54 @@ data Warningᴮ H {Γ} where Warningᴮ H D₂ → -------------------- Warningᴮ H (function f D₁ D₂) + +data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where + + function₀ : ∀ f {x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → + + (U ≢ V) → + --------------------------------- + Warningᴼ H (function f {U = U} D) + + function₁ : ∀ f {x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → + + Warningᴮ H D → + --------------------------------- + Warningᴼ H (function f {U = U} D) + +data Warningᴴ H (D : ⊢ᴴ H) : Set where + + addr : ∀ a {O} → + + (p : H [ a ]ᴴ ≡ O) → + Warningᴼ H (D a p) → + --------------- + Warningᴴ H D + +data Warningᴴᴱ H {Γ M T} : (Γ ⊢ᴴᴱ H ▷ M ∈ T) → Set where + + heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} → + + Warningᴴ H D₁ → + ----------------- + Warningᴴᴱ H (D₁ , D₂) + + expr : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} → + + Warningᴱ H D₂ → + --------------------- + Warningᴴᴱ H (D₁ , D₂) + +data Warningᴴᴮ H {Γ B T} : (Γ ⊢ᴴᴮ H ▷ B ∈ T) → Set where + + heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} → + + Warningᴴ H D₁ → + ----------------- + Warningᴴᴮ H (D₁ , D₂) + + block : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} → + + Warningᴮ H D₂ → + --------------------- + Warningᴴᴮ H (D₁ , D₂) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index 0a787761..a29f2518 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -9,16 +9,21 @@ open import FFI.Data.Maybe using (Maybe; just) 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.Var using (Var) open import Luau.Addr using (Addr) -open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) +open import Luau.Heap using (Heap; Object; 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.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import FFI.Data.Vector using (Vector) open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Properties.Product using (_×_; _,_) src : Type → Type src = Luau.Type.src m +orBot : Maybe Type → Type +orBot nothing = bot +orBot (just T) = T + data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set @@ -59,9 +64,9 @@ data _⊢ᴱ_∈_ where var : ∀ x {T Γ} → - T ≡ Γ [ x ]ⱽ → - -------------- - Γ ⊢ᴱ var x ∈ T + T ≡ orBot(Γ [ x ]ⱽ) → + ---------------- + Γ ⊢ᴱ (var x) ∈ T addr : ∀ a T {Γ} → @@ -87,70 +92,24 @@ data _⊢ᴱ_∈_ where --------------------------- Γ ⊢ᴱ (block b is B end) ∈ T --- data _⊢ᴮ_∋_∈_⊣_ : VarCtxt → Type → Block yes → Type → VarCtxt → Set --- data _⊢ᴱ_∋_∈_⊣_ : VarCtxt → Type → Expr yes → Type → VarCtxt → Set +data ⊢ᴼ_ : Maybe(Object yes) → Set where --- data _⊢ᴮ_∋_∈_⊣_ where + nothing : --- done : ∀ {S Γ} → + --------- + ⊢ᴼ nothing --- ---------------------- --- Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ + function : ∀ f {x T U V B} → --- return : ∀ {M B S T U Γ Δ₁ Δ₂} → + (x ↦ T) ⊢ᴮ B ∈ V → + ---------------------------------------------- + ⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end) --- Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → --- Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂ → --- --------------------------------- --- Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ +⊢ᴴ_ : Heap yes → Set +⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O) --- local : ∀ {x M B S T U V Γ Δ₁ Δ₂} → +_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set +(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T) --- Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → --- (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → --- ---------------------------------------------------------- --- Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) - --- function : ∀ {f x B C S T U V 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)) - --- data _⊢ᴱ_∋_∈_⊣_ where - --- nil : ∀ {S Γ} → - --- ---------------------- --- Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ - --- var : ∀ x {S T Γ} → - --- T ≡ Γ [ x ]ⱽ → --- ---------------------------- --- Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) - --- addr : ∀ a T {S Γ} → - --- ------------------------- --- Γ ⊢ᴱ S ∋ (addr a) ∈ T ⊣ ∅ - --- app : ∀ {M N S T U Γ Δ₁ Δ₂} → - --- Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁ → --- Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → --- -------------------------------------- --- Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) - --- function : ∀ {f x B S T U V Γ Δ} → - --- (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ → --- ----------------------------------------------------------------------- --- Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) - --- block : ∀ b {B S T Γ Δ} → - --- Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → --- ---------------------------------------------------- --- Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ +_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set +(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T) diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index 9ad2e2f5..eaae45ac 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -9,10 +9,6 @@ open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; inse open import FFI.Data.Maybe using (Maybe; just; nothing) open import Properties.Equality using (cong) -orBot : Maybe Type → Type -orBot nothing = bot -orBot (just T) = T - VarCtxt : Set VarCtxt = KeyMap Type @@ -25,8 +21,8 @@ _⋒_ = unionWith _∩_ _⋓_ : VarCtxt → VarCtxt → VarCtxt _⋓_ = unionWith _∪_ -_[_] : VarCtxt → Var → Type -_[_] Γ x = orBot (lookup (fromString x) Γ) +_[_] : VarCtxt → Var → Maybe Type +_[_] Γ x = lookup (fromString x) Γ _⊝_ : VarCtxt → Var → VarCtxt Γ ⊝ x = delete (fromString x) Γ diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index f75b89d7..13e03731 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -5,30 +5,33 @@ 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) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) -open import Luau.StrictMode using (Warningᴱ; Warningᴮ; BadlyTypedFunctionAddress; UnallocatedAddress; app₀; app₁; app₂; block; return; local₀; local₁; local₂; function₀; function₁; function₂) +open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; block; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; addr) open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) open import Luau.Syntax using (Expr; yes; var; 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) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; nil; var; addr; app; function; block; done; return; local; orBot) open import Luau.Value using (val; nil; addr) open import Luau.Var using (_≡ⱽ_) 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 (_≢_; sym; cong; trans; subst₁) open import Properties.Dec using (Dec; yes; no) open import Properties.Contradiction using (CONTRADICTION) -open import Properties.TypeCheck(strict) using (declaredTypeᴴ; typeOfⱽ; typeOfᴴ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ) +open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ) open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) +open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) src = Luau.Type.src strict _≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) _≡ᵀ_ = {!!} +_≡ᴹᵀ_ : ∀ (T U : Maybe Type) → Dec(T ≡ U) +_≡ᴹᵀ_ = {!!} + data _⊑_ (H : Heap yes) : Heap yes → Set where refl : (H ⊑ H) snoc : ∀ {H′ H″ a V} → (H ⊑ H′) → (H″ ≡ᴴ H′ ⊕ a ↦ V) → (H ⊑ H″) @@ -100,16 +103,15 @@ preservationᴮ (return s) with preservationᴱ s preservationᴮ (return s) | ok p = ok p preservationᴮ (return s) | warning W = warning (return W) -reflect-substitutionᴱ : ∀ {H Γ Γ′ T} M v x → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H Γ′ M) +reflect-substitutionᴱ : ∀ {H Γ Γ′ T} M v x → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H Γ′ M) reflect-substitutionᴱ-whenever-yes : ∀ {H Γ Γ′ T} v x y (p : x ≡ y) → (typeOfᴱ H Γ (val v) ≡ T) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H Γ′ (var y)) reflect-substitutionᴱ-whenever-no : ∀ {H Γ Γ′ T} v x y (p : x ≢ y) → (typeOfᴱ H Γ (val v) ≡ T) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H Γ′ (var y)) -reflect-substitutionᴮ : ∀ {H Γ Γ′ T} B v x → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H Γ′ B) -reflect-substitutionᴮ-unless-yes : ∀ {H Γ Γ′ T} B v x y (r : x ≡ y) → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +reflect-substitutionᴮ : ∀ {H Γ Γ′ T} B v x → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H Γ′ 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ᴱ (var y) v x refl q W with x ≡ⱽ y -reflect-substitutionᴱ (var y) v x refl q W | yes r = reflect-substitutionᴱ-whenever-yes v x y r (typeOfᴱⱽ v) q W -reflect-substitutionᴱ (var y) v x refl q W | no r = reflect-substitutionᴱ-whenever-no v x y r (typeOfᴱⱽ v) q W -reflect-substitutionᴱ (addr a) v x p q (BadlyTypedFunctionAddress a f r W) = BadlyTypedFunctionAddress a f r W +reflect-substitutionᴱ (var y) v x p q W with x ≡ⱽ y +reflect-substitutionᴱ (var y) v x p q W | yes r = {!!} -- reflect-substitutionᴱ-whenever-yes v x y r (typeOfᴱⱽ v) p q W +reflect-substitutionᴱ (var y) v x p q W | no r = {!!} -- reflect-substitutionᴱ-whenever-no v x y r (typeOfᴱⱽ v) p q W reflect-substitutionᴱ (addr a) v x p q (UnallocatedAddress a r) = UnallocatedAddress a r reflect-substitutionᴱ (M $ N) v x p q (app₀ r) = {!!} reflect-substitutionᴱ (M $ N) v x p q (app₁ W) = app₁ (reflect-substitutionᴱ M v x p q W) @@ -120,15 +122,21 @@ reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p ref reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p refl (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ B v x p (⊕-swap r) W) reflect-substitutionᴱ (block b is B end) v x p q (block b W) = block b (reflect-substitutionᴮ B v x p q W) -reflect-substitutionᴱ-whenever-no v x y r refl refl () -reflect-substitutionᴱ-whenever-yes (addr a) x x refl refl refl (BadlyTypedFunctionAddress a f p W) = {!!} +reflect-substitutionᴱ-whenever-no v x y r refl refl (UnboundVariable y p) = UnboundVariable y {!!} reflect-substitutionᴱ-whenever-yes (addr a) x x refl refl refl (UnallocatedAddress a p) = {!!} -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₁ f W) = {!!} -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₂ f W) = {!!} +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₀ f r) = {!!} +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₁ f W) with (x ≡ⱽ y) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p refl (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes C v x y r p (⊕-overwrite r) W) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p refl (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ C v x p (⊕-swap r) W) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₂ f W) with (x ≡ⱽ f) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p refl (function₂ f W)| yes r = function₂ f (reflect-substitutionᴮ-unless-yes B v x f r p (⊕-overwrite r) W) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p refl (function₂ f W)| no r = function₂ f (reflect-substitutionᴮ B v x p (⊕-swap r) W) reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₀ r) = {!!} reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₁ W) = local₁ (reflect-substitutionᴱ M v x p q W) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₂ W) = {!!} +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₂ W) with (x ≡ⱽ y) +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p refl (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-overwrite r) W) +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p refl (local₂ W) | no r = local₂ (reflect-substitutionᴮ B v x p (⊕-swap r) W) reflect-substitutionᴮ (return M ∙ B) v x p q (return W) = return (reflect-substitutionᴱ M v x p q W) reflect-substitutionᴮ-unless-yes B v x y r p refl W = W @@ -136,9 +144,7 @@ reflect-substitutionᴮ-unless-yes B v x y r p refl W = W reflect-weakeningᴱ : ∀ {H H′ Γ M} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) reflect-weakeningᴮ : ∀ {H H′ Γ B} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) -reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) with lookup-⊑-just a h p -reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) | just q = BadlyTypedFunctionAddress a f q (reflect-weakeningᴮ h W) -reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) | nothing q = UnallocatedAddress a q +reflect-weakeningᴱ h (UnboundVariable x p) = (UnboundVariable x p) reflect-weakeningᴱ h (UnallocatedAddress a p) = UnallocatedAddress a (lookup-⊑-nothing a h p) reflect-weakeningᴱ h (app₀ p) with heap-weakeningᴱ h | heap-weakeningᴱ h reflect-weakeningᴱ h (app₀ p) | ok q₁ | ok q₂ = app₀ (λ r → p (trans (cong src (sym q₁)) (trans r q₂))) @@ -158,35 +164,112 @@ reflect-weakeningᴮ h (local₀ p) | ok q = local₀ (λ r → p (trans r q)) reflect-weakeningᴮ h (local₀ p) | warning W = local₁ W reflect-weakeningᴮ h (local₁ W) = local₁ (reflect-weakeningᴱ h W) reflect-weakeningᴮ h (local₂ W) = local₂ (reflect-weakeningᴮ h W) +reflect-weakeningᴮ h (function₀ f p) with heap-weakeningᴮ h +reflect-weakeningᴮ h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) +reflect-weakeningᴮ h (function₀ f p) | warning W = function₁ f W reflect-weakeningᴮ h (function₁ f W) = function₁ f (reflect-weakeningᴮ h W) reflect-weakeningᴮ h (function₂ f W) = function₂ f (reflect-weakeningᴮ h W) -reflectᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴱ H (typeCheckᴱ H ∅ M) -reflectᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴮ H (typeCheckᴮ H ∅ B) +reflect-weakeningᴼ : ∀ {H H′ O} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O) +reflect-weakeningᴼ h (function₀ f p) with heap-weakeningᴮ h +reflect-weakeningᴼ h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) +reflect-weakeningᴼ h (function₀ f p) | warning W = function₁ f W +reflect-weakeningᴼ h (function₁ f W′) = function₁ f (reflect-weakeningᴮ h W′) + +reflectᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) +reflectᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) -reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (BadlyTypedFunctionAddress a f refl W) = function₁ f (reflect-weakeningᴮ (snoc refl defn) W) reflectᴱ (app s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (redn-⊑ s) -reflectᴱ (app s) (app₀ p) | ok q | ok q′ = app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′)) -reflectᴱ (app s) (app₀ p) | warning W | _ = app₁ W -reflectᴱ (app s) (app₀ p) | _ | warning W = app₂ W -reflectᴱ (app s) (app₁ W) = app₁ (reflectᴱ s W) -reflectᴱ (app s) (app₂ W) = app₂ (reflect-weakeningᴱ (redn-⊑ s) W) -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₀ p)) = app₀ (λ r → p (trans (sym (cong src (cong declaredTypeᴴ q))) r)) -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = app₂ W -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₂ {T = T′} W)) = app₁ (BadlyTypedFunctionAddress a f q W) -reflectᴱ (block s) (block b W) = block b (reflectᴮ s W) -reflectᴱ (return q) W = block _ (return W) +reflectᴱ (app s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′))) +reflectᴱ (app s) (app₀ p) | warning W | _ = expr (app₁ W) +reflectᴱ (app s) (app₀ p) | _ | warning W = expr (app₂ W) +reflectᴱ (app s) (app₁ W′) with reflectᴱ s W′ +reflectᴱ (app s) (app₁ W′) | heap W = heap W +reflectᴱ (app s) (app₁ W′) | expr W = expr (app₁ W) +reflectᴱ (app s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (redn-⊑ s) W′)) +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₀ p)) = expr (app₀ (λ r → p (trans (cong src (cong orBot (cong typeOfᴹᴼ (sym q)))) r))) +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = expr (app₂ W) +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₂ W)) = heap (addr a q (function₁ f W)) +reflectᴱ (block s) (block b W′) with reflectᴮ s W′ +reflectᴱ (block s) (block b W′) | heap W = heap W +reflectᴱ (block s) (block b W′) | block W = expr (block b W) +reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (UnallocatedAddress a ()) +reflectᴱ (return q) W = expr (block _ (return W)) reflectᴮ (local s) (local₀ p) with preservationᴱ s -reflectᴮ (local s) (local₀ p) | ok q = local₀ (λ r → p (trans r q)) -reflectᴮ (local s) (local₀ p) | warning W = local₁ W -reflectᴮ (local s) (local₁ W) = local₁ (reflectᴱ s W) -reflectᴮ (local s) (local₂ W) = local₂ (reflect-weakeningᴮ (redn-⊑ s) W) -reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with T ≡ᵀ (typeOfᴱ H ∅ (val v)) -reflectᴮ (subst {x = var x ∈ T} {v = v}) W | yes refl = local₂ (reflect-substitutionᴮ _ v x (typeOfᴱⱽ v) refl W) -reflectᴮ (subst {x = var x ∈ T} {v = v}) W | no p = local₀ p -reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = function₂ f (reflect-weakeningᴮ (snoc refl defn) (reflect-substitutionᴮ _ _ f refl refl W)) -reflectᴮ (return s) (return W) = return (reflectᴱ s W) +reflectᴮ (local s) (local₀ p) | ok q = block (local₀ (λ r → p (trans r q))) +reflectᴮ (local s) (local₀ p) | warning W = block (local₁ W) +reflectᴮ (local s) (local₁ W′) with reflectᴱ s W′ -- local₁ (reflectᴱ s W) +reflectᴮ (local s) (local₁ W′) | heap W = heap W +reflectᴮ (local s) (local₁ W′) | expr W = block (local₁ W) +reflectᴮ (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ (redn-⊑ s) W′)) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with just T ≡ᴹᵀ typeOfⱽ H v +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W | yes p = block (local₂ (reflect-substitutionᴮ _ v x p refl W)) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = nil}) W | no p = block (local₀ λ r → p (cong just r)) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p with remember(H [ a ]ᴴ) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p | (nothing , q) = block (local₁ (UnallocatedAddress a q)) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p | (just O , q) = block (local₀ (λ r → p (trans (cong just (trans r (cong orBot (cong typeOfᴹᴼ q)))) (cong typeOfᴹᴼ (sym q))))) +reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = block (function₂ f (reflect-weakeningᴮ (snoc refl defn) (reflect-substitutionᴮ _ _ f refl refl W))) +reflectᴮ (return s) (return W′) with reflectᴱ s W′ +reflectᴮ (return s) (return W′) | heap W = heap W +reflectᴮ (return s) (return W′) | expr W = block (return W) + +reflectᴴᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴᴱ H′ (typeCheckᴴᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) +reflectᴴᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) + +reflectᴴᴱ s (expr W′) = reflectᴱ s W′ +reflectᴴᴱ (function {a = a} p) (heap (addr b refl W′)) with b ≡ᴬ a +reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc refl defn) +reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = expr (function₀ f λ q → p (trans q r)) +reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = expr (function₁ f W) +reflectᴴᴱ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = expr (function₁ f (reflect-weakeningᴮ (snoc refl defn) W′)) +reflectᴴᴱ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc refl p) W′)) +reflectᴴᴱ (app s) (heap W′) with reflectᴴᴱ s (heap W′) +reflectᴴᴱ (app s) (heap W′) | heap W = heap W +reflectᴴᴱ (app s) (heap W′) | expr W = expr (app₁ W) +reflectᴴᴱ (beta p) (heap W′) = heap W′ +reflectᴴᴱ (block s) (heap W′) with reflectᴴᴮ s (heap W′) +reflectᴴᴱ (block s) (heap W′) | heap W = heap W +reflectᴴᴱ (block s) (heap W′) | block W = expr (block _ W) +reflectᴴᴱ (return s) (heap W′) = heap W′ +reflectᴴᴱ done (heap W′) = heap W′ + +reflectᴴᴮ s (block W′) = reflectᴮ s W′ +reflectᴴᴮ (local {x = var x ∈ T} s) (heap W′) with reflectᴴᴱ s (heap W′) +reflectᴴᴮ (local {x = var x ∈ T} s) (heap W′) | heap W = heap W +reflectᴴᴮ (local {x = var x ∈ T} s) (heap W′) | expr W = block (local₁ W) +reflectᴴᴮ (subst) (heap W′) = heap W′ +reflectᴴᴮ (function {a = a} p) (heap (addr b refl W′)) with b ≡ᴬ a +reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc refl defn) +reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = block (function₀ f (λ q → p (trans q r))) +reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = block (function₁ f W) +reflectᴴᴮ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = block (function₁ f (reflect-weakeningᴮ (snoc refl defn) W′)) +reflectᴴᴮ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc refl p) W′)) +reflectᴴᴮ (return s) (heap W′) with reflectᴴᴱ s (heap W′) +reflectᴴᴮ (return s) (heap W′) | heap W = heap W +reflectᴴᴮ (return s) (heap W′) | expr W = block (return W) + +bot-not-obj : ∀ O → bot ≢ typeOfᴼ O +bot-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () + +runtimeWarningᴱ : ∀ {H M} → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M) +runtimeWarningᴮ : ∀ {H B} → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B) + +runtimeWarningᴱ (NilIsNotAFunction {V = nil}) = (app₀ (λ ())) +runtimeWarningᴱ {H} (NilIsNotAFunction {addr a}) with remember (H [ a ]ᴴ) +runtimeWarningᴱ (NilIsNotAFunction {addr a}) | (nothing , p) = app₂ (UnallocatedAddress a p) +runtimeWarningᴱ (NilIsNotAFunction {addr a}) | (just O , p) = app₀ λ r → bot-not-obj O (trans r (cong orBot (cong typeOfᴹᴼ p))) +runtimeWarningᴱ (UnboundVariable x) = UnboundVariable x refl +runtimeWarningᴱ (SEGV a p) = UnallocatedAddress a p +runtimeWarningᴱ (app err) = app₁ (runtimeWarningᴱ err) +runtimeWarningᴱ (block b err) = block b (runtimeWarningᴮ err) + +runtimeWarningᴮ (local (var x ∈ T) err) = local₁ (runtimeWarningᴱ err) +runtimeWarningᴮ (return err) = return (runtimeWarningᴱ err) + + + + -- reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (bot ()) -- reflectᴱ (function defn) (addr a T q) = CONTRADICTION (q refl) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 1ba1c0e7..7ffdf3ac 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -7,36 +7,39 @@ 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; unbound; addr; app; function; block; done; return; local; nothing; orBot) 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; 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.Value using (Value; nil; addr; val) -open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) +open import Luau.Heap using (Heap; Object; 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; _,_) +open import Properties.Product using (_×_; _,_) +open import Properties.Remember using (Remember; remember; _,_) src : Type → Type src = Luau.Type.src m -declaredTypeᴴ : Maybe(HeapValue yes) → Type -declaredTypeᴴ nothing = bot -declaredTypeᴴ (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) +typeOfᴼ : Object yes → Type +typeOfᴼ (function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) -typeOfⱽ : Heap yes → Value → Type -typeOfⱽ H nil = nil -typeOfⱽ H (addr a) = declaredTypeᴴ (H [ a ]ᴴ) +typeOfᴹᴼ : Maybe(Object yes) → Maybe Type +typeOfᴹᴼ nothing = nothing +typeOfᴹᴼ (just O) = just (typeOfᴼ O) + +typeOfⱽ : Heap yes → Value → Maybe Type +typeOfⱽ H nil = just nil +typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ) typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type typeOfᴱ H Γ nil = nil -typeOfᴱ H Γ (var x) = Γ [ x ]ⱽ -typeOfᴱ H Γ (addr a) = declaredTypeᴴ (H [ a ]ᴴ) +typeOfᴱ H Γ (var x) = orBot(Γ [ x ]ⱽ) +typeOfᴱ H Γ (addr a) = orBot(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 @@ -46,11 +49,7 @@ 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 -typeOfᴴ : Heap yes → Maybe(HeapValue yes) → Type -typeOfᴴ H nothing = bot -typeOfᴴ H (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ typeOfᴮ H (x ↦ S) B) - -typeOfᴱⱽ : ∀ {H Γ} v → (typeOfᴱ H Γ (val v) ≡ typeOfⱽ H v) +typeOfᴱⱽ : ∀ {H Γ} v → (typeOfᴱ H Γ (val v) ≡ orBot(typeOfⱽ H v)) typeOfᴱⱽ nil = refl typeOfᴱⱽ (addr a) = refl @@ -59,7 +58,7 @@ typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) typeCheckᴱ H Γ nil = nil typeCheckᴱ H Γ (var x) = var x refl -typeCheckᴱ H Γ (addr a) = addr a (declaredTypeᴴ (H [ a ]ᴴ)) +typeCheckᴱ H Γ (addr a) = addr a (orBot (typeOfᴹᴼ (H [ a ]ᴴ))) 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 b is B end) = block b (typeCheckᴮ H Γ B) @@ -68,3 +67,16 @@ typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = functio 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 → (⊢ᴴ H) +typeCheckᴴ H a {O} p = typeCheckᴼ H (O) + +typeCheckᴴᴱ : ∀ H Γ M → (Γ ⊢ᴴᴱ H ▷ M ∈ typeOfᴱ H Γ M) +typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M) + +typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M) +typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)