From 005258185136f47c6e02c362455e3385b86369f9 Mon Sep 17 00:00:00 2001
From: Lily Brown <lbrown@roblox.com>
Date: Fri, 18 Feb 2022 14:47:39 -0800
Subject: [PATCH] checkpoint

---
 prototyping/Luau/RuntimeError.agda | 4 +++-
 prototyping/Properties/Step.agda   | 4 ++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index 5e0d4684..f6ff7e36 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -6,12 +6,14 @@ open import FFI.Data.Maybe using (just; nothing)
 open import FFI.Data.String using (String)
 open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number)
 open import Luau.RuntimeType using (RuntimeType; valueType)
+open import Luau.Value using (val)
+open import Properties.Equality using (_≢_)
 
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  TypeMismatch : ∀ {t} → RuntimeErrorᴱ H (number n)
+  TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (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/Properties/Step.agda b/prototyping/Properties/Step.agda
index bb851202..a5edb3af 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -6,7 +6,7 @@ open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
 open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +)
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst; binOp; evalBinOp)
-open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
+open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val; number)
 open import Properties.Remember using (remember; _,_)
@@ -34,7 +34,7 @@ stepᴱ H (addr a) = value (addr a) refl
 stepᴱ H (number x) = value (number x) refl
 stepᴱ H (M $ N) with stepᴱ H M
 stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
-stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
+stepᴱ H (nil $ N) | value nil refl = error (TypeMismatch nil (nil $ N))
 stepᴱ H ((number _) $ N) | value (number x) refl = error (NumberIsNotAFunction x)
 stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
 stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))