WIP

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 #-}
 

prototyping/Luau/AddrCtxt.agda

@@ -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)

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
+-- Heap-allocated objects
-  function_is_end : FunDec a → Block a → HeapValue a
+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
+

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)

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₂)

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 ]ⱽ →
+    T ≡ orBot(Γ [ x ]ⱽ) →
-    --------------
+    ----------------
-    Γ ⊢ᴱ var x ∈ T
+    Γ ⊢ᴱ (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 ⊢ᴼ_ : Maybe(Object yes) → Set where
--- data _⊢ᴱ_∋_∈_⊣_ : VarCtxt → Type → Expr yes → Type → VarCtxt → Set
 
--- data _⊢ᴮ_∋_∈_⊣_ where
+  nothing :
 
---   done : ∀ {S Γ} →
+    ---------
+    ⊢ᴼ nothing
 
---     ----------------------
+  function : ∀ f {x T U V B} →
---     Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅
 
---   return : ∀ {M B S T U Γ Δ₁ Δ₂} →
+    (x ↦ T) ⊢ᴮ B ∈ V →
+    ----------------------------------------------
+    ⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end)
 
---     Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ →
+⊢ᴴ_ : Heap yes → Set
---     Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂ →
+⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O)
---     ---------------------------------
---     Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁
 
---   local : ∀ {x M B S T U V Γ Δ₁ Δ₂} →
+_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set
+(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T)
 
---     Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ →
+_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set
---     (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ →
+(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T)
---     ----------------------------------------------------------
---     Γ ⊢ᴮ 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 ⊣ Δ

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
+_[_] : VarCtxt → Var → Maybe Type
-_[_] Γ x = orBot (lookup (fromString x) Γ)
+_[_] Γ x = lookup (fromString x) Γ
 
 _⊝_ : VarCtxt → Var → VarCtxt
 Γ ⊝ x = delete (fromString x) Γ

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.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) 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.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ᴮ : ∀ {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) → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → 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 p 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 p q W | yes r = {!!} -- reflect-substitutionᴱ-whenever-yes v x y r (typeOfᴱⱽ v) p 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ᴱ (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 (BadlyTypedFunctionAddress a f r W) = BadlyTypedFunctionAddress a f r 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-no v x y r refl refl (UnboundVariable y p) = UnboundVariable y {!!}
-reflect-substitutionᴱ-whenever-yes (addr a) x x refl refl refl (BadlyTypedFunctionAddress a f p W) = {!!}
 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 r) = {!!}
-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) 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 (UnboundVariable x p) = (UnboundVariable x 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 (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-weakeningᴼ : ∀ {H H′ O} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
-reflectᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴮ H (typeCheckᴮ H ∅ B)
+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) | ok q | ok q′ = expr (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 | _ = expr (app₁ W)
-reflectᴱ (app s) (app₀ p) | _ | warning W  = app₂ W
+reflectᴱ (app s) (app₀ p) | _ | warning W  = expr (app₂ W)
-reflectᴱ (app s) (app₁ W) = app₁ (reflectᴱ s W)
+reflectᴱ (app s) (app₁ W′) with reflectᴱ s W′
-reflectᴱ (app s) (app₂ W) = app₂ (reflect-weakeningᴱ (redn-⊑ s) W)
+reflectᴱ (app s) (app₁ W′) | heap W = heap 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ᴱ (app s) (app₁ W′) | expr W = expr (app₁ W)
-reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = 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₂ {T = T′} W)) = app₁ (BadlyTypedFunctionAddress a f q 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ᴱ (block s) (block b W)  = block b (reflectᴮ s W)
+reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = expr (app₂ W)
-reflectᴱ (return q) W = block _ (return 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) | ok q = block (local₀ (λ r → p (trans r q)))
-reflectᴮ (local s) (local₀ p) | warning W = local₁ W
+reflectᴮ (local s) (local₀ p) | warning W = block (local₁ W)
-reflectᴮ (local s) (local₁ W) = local₁ (reflectᴱ s W)
+reflectᴮ (local s) (local₁ W′) with reflectᴱ s W′ -- local₁ (reflectᴱ s W)
-reflectᴮ (local s) (local₂ W) = local₂ (reflect-weakeningᴮ (redn-⊑ s) W)
+reflectᴮ (local s) (local₁ W′) | heap W = heap W
-reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with T ≡ᵀ (typeOfᴱ H ∅ (val v))
+reflectᴮ (local s) (local₁ W′) | expr W = block (local₁ W)
-reflectᴮ (subst {x = var x ∈ T} {v = v}) W | yes refl = local₂ (reflect-substitutionᴮ _ v x (typeOfᴱⱽ v) refl W)
+reflectᴮ (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ (redn-⊑ s) W′))
-reflectᴮ (subst {x = var x ∈ T} {v = v}) W | no p = local₀ p
+reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with just T ≡ᴹᵀ typeOfⱽ H v
-reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = function₂ f (reflect-weakeningᴮ (snoc refl defn) (reflect-substitutionᴮ _ _ f refl refl W))
+reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W | yes p = block (local₂ (reflect-substitutionᴮ _ v x p refl W))
-reflectᴮ (return s) (return W) = return (reflectᴱ s 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)

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
+typeOfᴼ : Object yes → Type
-declaredTypeᴴ nothing = bot
+typeOfᴼ (function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T)
-declaredTypeᴴ (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T)
 
-typeOfⱽ : Heap yes → Value → Type
+typeOfᴹᴼ : Maybe(Object yes) → Maybe Type
-typeOfⱽ H nil = nil
+typeOfᴹᴼ nothing = nothing
-typeOfⱽ H (addr a) = declaredTypeᴴ (H [ a ]ᴴ)
+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 Γ (var x) = orBot(Γ [ x ]ⱽ)
-typeOfᴱ H Γ (addr a) = declaredTypeᴴ (H [ a ]ᴴ)
+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 Γ} v → (typeOfᴱ H Γ (val v) ≡ orBot(typeOfⱽ H v))
-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ᴱⱽ 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)