Add files via upload

2025-05-04 10:33:46 +01:00 · 2022-07-30 22:27:46 -05:00 · 2022-07-30 22:27:46 -05:00 · 681359d4d1
commit 681359d4d1
parent d6827d480a
28 changed files with 1815 additions and 28 deletions
--- a/prototyping/lluz/Addr.agda
+++ b/prototyping/lluz/Addr.agda
@ -0,0 +1,18 @@
+module Luau.Addr where
+
+open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Nat using (Nat; _==_)
+open import Agda.Builtin.String using (String)
+open import Agda.Builtin.TrustMe using (primTrustMe)
+open import Properties.Dec using (Dec; yes; no)
+open import Properties.Equality using (_≢_)
+
+Addr : Set
+Addr = Nat
+
+_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b)
+a ≡ᴬ b with a == b
+a ≡ᴬ b | false = no p where postulate p : (a ≢ b)
+a ≡ᴬ b | true = yes primTrustMe
+
--- a/prototyping/lluz/Addr/ToString.agda
+++ b/prototyping/lluz/Addr/ToString.agda
@ -0,0 +1,8 @@
+module Luau.Addr.ToString where
+
+open import Agda.Builtin.String using (String; primStringAppend)
+open import Luau.Addr using (Addr)
+open import Agda.Builtin.Int using (Int; primShowInteger; pos)
+
+addrToString : Addr → String
+addrToString a = primStringAppend "a" (primShowInteger (pos a))
--- a/prototyping/lluz/Heap.agda
+++ b/prototyping/lluz/Heap.agda
@ -0,0 +1,49 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.Heap where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+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 (_≢_; trans)
+open import Properties.Remember using (remember; _,_)
+open import Properties.Dec using (yes; no)
+
+-- Heap-allocated objects
+data Object (a : Annotated) : Set where
+
+  function_is_end : FunDec a → Block a → Object a
+
+Heap : Annotated → Set
+Heap a = Vector (Object a)
+
+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 (Object a)
+_[_] = FFI.Data.Vector.lookup
+
+∅ : ∀ {a} → Heap a
+∅ = empty
+
+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
+alloc H V = ok (length H) (snoc H V) defn
+
+next : ∀ {a} → Heap a → Addr
+next = length
+
+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
--- a/prototyping/lluz/OpSem.agda
+++ b/prototyping/lluz/OpSem.agda
@ -0,0 +1,143 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.OpSem where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
+open import Agda.Builtin.Bool using (Bool; true; false)
+open import Agda.Builtin.String using (primStringEquality; primStringAppend)
+open import Utility.Bool using (not; _or_; _and_)
+open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
+open import Luau.Substitution using (_[_/_]ᴮ)
+open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; number; bool; string)
+open import Luau.RuntimeType using (RuntimeType; valueType)
+open import Properties.Product using (_×_; _,_)
+
+evalEqOp : Value → Value → Bool
+evalEqOp Value.nil Value.nil = true
+evalEqOp (addr x) (addr y) = (x ==ᴬ y)
+evalEqOp (number x) (number y) = primFloatEquality x y
+evalEqOp (bool true) (bool y) = y
+evalEqOp (bool false) (bool y) = not y
+evalEqOp _ _ = false
+
+evalNeqOp : Value → Value → Bool
+evalNeqOp (number x) (number y) = primFloatInequality x y
+evalNeqOp x y = not (evalEqOp x y)
+
+data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
+  + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)
+  - : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n)
+  / : ∀ m n → (number m) ⟦ / ⟧ (number n) ⟶ number (primFloatTimes m n)
+  * : ∀ m n → (number m) ⟦ * ⟧ (number n) ⟶ number (primFloatDiv m n)
+  < : ∀ m n → (number m) ⟦ < ⟧ (number n) ⟶ bool (primFloatLess m n)
+  > : ∀ m n → (number m) ⟦ > ⟧ (number n) ⟶ bool (primFloatLess n m)
+  <= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n))
+  >= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
+  == : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
+  ~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
+  ·· : ∀ x y → (string x) ⟦ ·· ⟧ (string y) ⟶ string (primStringAppend x y)
+
+data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
+data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
+
+data _⊢_⟶ᴱ_⊣_  where
+
+  function : ∀ a {H H′ F B} →
+
+    H′ ≡ H ⊕ a ↦ (function F is B end) →
+    -------------------------------------------
+    H ⊢ (function F is B end) ⟶ᴱ val(addr a) ⊣ H′
+
+  app₁ : ∀ {H H′ M M′ N} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    -----------------------------
+    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
+
+  app₂ : ∀ v {H H′ N N′} →
+
+    H ⊢ N ⟶ᴱ N′ ⊣ H′ →
+    -----------------------------
+    H ⊢ (val v $ N) ⟶ᴱ (val v $ N′) ⊣ H′
+
+  beta : ∀ O v {H a F B} →
+
+    (O ≡ function F is B end) →
+    H [ a ] ≡ just(O) →
+    -----------------------------------------------------------------------------
+    H ⊢ (val (addr a) $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H
+
+  block : ∀ {H H′ B B′ b} →
+ 
+    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
+    ----------------------------------------------------
+    H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′
+
+  return : ∀ v {H B b} →
+
+    --------------------------------------------------------
+    H ⊢ (block b is return (val v) ∙ B end) ⟶ᴱ val v ⊣ H
+
+  done : ∀ {H b} →
+ 
+    --------------------------------------------
+    H ⊢ (block b is done end) ⟶ᴱ (val nil) ⊣ H
+  
+  binOp₀ : ∀ {H op v₁ v₂ w} →
+
+    v₁ ⟦ op ⟧ v₂ ⟶ w → 
+    --------------------------------------------------
+    H ⊢ (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) ⊣ H
+
+  binOp₁ : ∀ {H H′ x x′ op y} →
+
+    H ⊢ x ⟶ᴱ x′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′
+  
+  binOp₂ : ∀ {H H′ x op y y′} →
+
+    H ⊢ y ⟶ᴱ y′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′
+
+data _⊢_⟶ᴮ_⊣_  where
+
+  local : ∀ {H H′ x M M′ B} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    -------------------------------------------------
+    H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′
+
+  subst : ∀ v {H x B} →
+  
+    ------------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H
+
+  function : ∀ a {H H′ F B C} →
+  
+    H′ ≡ H ⊕ a ↦ (function F is C end) →
+    --------------------------------------------------------------
+    H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) ⊣ H′
+
+  return : ∀ {H H′ M M′ B} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    --------------------------------------------
+    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
+
+data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where
+
+  refl : ∀ {H B} →
+
+    ----------------
+    H ⊢ B ⟶* B ⊣ H
+    
+  step : ∀ {H H′ H″ B B′ B″} →
+    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
+    H′ ⊢ B′ ⟶* B″ ⊣ H″ →
+    ------------------
+    H ⊢ B ⟶* B″ ⊣ H″
--- a/prototyping/lluz/ResolveOverloads.agda
+++ b/prototyping/lluz/ResolveOverloads.agda
@ -0,0 +1,98 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.ResolveOverloads where
+
+open import FFI.Data.Either using (Left; Right)
+open import Luau.Subtyping using (_<:_; _≮:_; Language; witness; scalar; unknown; never; function-ok)
+open import Luau.Type using (Type ; _⇒_; _∩_; _∪_; unknown; never)
+open import Luau.TypeSaturation using (saturate)
+open import Luau.TypeNormalization using (normalize)
+open import Properties.Contradiction using (CONTRADICTION)
+open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right)
+open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
+open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)
+
+-- The domain of a normalized type
+srcⁿ : Type → Type
+srcⁿ (S ⇒ T) = S
+srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
+srcⁿ never = unknown
+srcⁿ T = never
+
+-- To get the domain of a type, we normalize it first We need to do
+-- this, since if we try to use it on non-normalized types, we get
+--
+-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
+-- src(never) = unknown
+--
+-- so src doesn't respect type equivalence.
+src : Type → Type
+src (S ⇒ T) = S
+src T = srcⁿ(normalize T)
+
+-- Calculate the result of applying a function type `F` to an argument type `V`.
+-- We do this by finding an overload of `F` that has the most precise type,
+-- that is an overload `(Sʳ ⇒ Tʳ)` where `V <: Sʳ` and moreover
+-- for any other such overload `(S ⇒ T)` we have that `Tʳ <: T`.
+
+-- For example if `F` is `(number -> number) & (nil -> nil) & (number? -> number?)`
+-- then to resolve `F` with argument type `number`, we pick the `number -> number`
+-- overload, but if the argument is `number?`, we pick `number? -> number?`./
+
+-- Not all types have such a most precise overload, but saturated ones do.
+
+data ResolvedTo F G V : Set where
+
+  yes : ∀ Sʳ Tʳ →
+
+    Overloads F (Sʳ ⇒ Tʳ) →
+    (V <: Sʳ) → 
+    (∀ {S T} → Overloads G (S ⇒ T) → (V <: S) → (Tʳ <: T)) →
+    --------------------------------------------
+    ResolvedTo F G V
+
+  no :
+
+    (∀ {S T} → Overloads G (S ⇒ T) → (V ≮: S)) →
+    --------------------------------------------
+    ResolvedTo F G V
+
+Resolved : Type → Type → Set
+Resolved F V = ResolvedTo F F V
+
+target : ∀ {F V} → Resolved F V → Type
+target (yes _ T _ _ _) = T
+target (no _) = unknown
+
+-- We can resolve any saturated function type
+resolveˢ : ∀ {F G V} → FunType G → Saturated F → Normal V → (G ⊆ᵒ F) → ResolvedTo F G V
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F with dec-subtypingⁿ Vⁿ Sⁿ
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Left V≮:S = no (λ { here → V≮:S })
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Right V<:S = yes _ _ (G⊆F here) V<:S (λ { here _ → <:-refl })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F with resolveˢ Gᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ left) | resolveˢ Hᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ right)
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ with sat-∩ o₁ o₂
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ | defn o p₁ p₂ =
+  yes _ _ o (<:-trans (<:-∩-glb V<:S₁ V<:S₂) p₁) (λ { (left o) p → <:-trans p₂ (<:-trans <:-∩-left (tgt₁ o p)) ; (right o) p → <:-trans p₂ (<:-trans <:-∩-right (tgt₂ o p)) })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | no src₂ =
+  yes _ _ o₁ V<:S₁ (λ { (left o) p → tgt₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (src₂ o)) })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ =
+  yes _ _ o₂ V<:S₂ (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (src₁ o)) ; (right o) p → tgt₂ o p })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | no src₂ =
+  no (λ { (left o) → src₁ o ; (right o) → src₂ o })
+
+-- Which means we can resolve any normalized type, by saturating it first
+resolveᶠ : ∀ {F V} → FunType F → Normal V → Type
+resolveᶠ Fᶠ Vⁿ = target (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))
+
+resolveⁿ : ∀ {F V} → Normal F → Normal V → Type
+resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Vⁿ
+resolveⁿ (Fᶠ ∩ Gᶠ) Vⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Vⁿ
+resolveⁿ (Sⁿ ∪ Tˢ) Vⁿ = unknown
+resolveⁿ unknown Vⁿ = unknown
+resolveⁿ never Vⁿ = never
+
+-- Which means we can resolve any type, by normalizing it first
+resolve : Type → Type → Type
+resolve F V = resolveⁿ (normal F) (normal V)
--- a/prototyping/lluz/Run.agda
+++ b/prototyping/lluz/Run.agda
@ -0,0 +1,29 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.Run where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Luau.Heap using (Heap; ∅)
+open import Luau.Syntax using (Block; val; return; _∙_; done)
+open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
+open import Properties.Step using (stepᴮ; step; return; done; error)
+open import Luau.RuntimeError using (RuntimeErrorᴮ)
+
+data RunResult {a} (H : Heap a) (B : Block a) : Set where
+  return : ∀ v {B′ H′} → (H ⊢ B ⟶* (return (val v) ∙ B′) ⊣ H′) → RunResult H B
+  done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B
+  error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B
+
+{-# TERMINATING #-}
+run′ : ∀ {a} H B → RunResult {a} H B
+run′ H B with stepᴮ H B
+run′ H B | step H′ B′ D with run′ H′ B′
+run′ H B | step H′ B′ D | return V D′  = return V (step D D′)
+run′ H B | step H′ B′ D | done D′ = done (step D D′)
+run′ H B | step H′ B′ D | error E D′ = error E (step D D′)
+run′ H _ | return V refl = return V refl
+run′ H _ | done refl = done refl
+run′ H B | error E = error E refl
+
+run : ∀ {a} B → RunResult {a} ∅ B
+run = run′ ∅
--- a/prototyping/lluz/RuntimeError.agda
+++ b/prototyping/lluz/RuntimeError.agda
@ -0,0 +1,41 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.RuntimeError where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Luau.Heap using (Heap; _[_])
+open import FFI.Data.Maybe using (just; nothing)
+open import FFI.Data.String using (String)
+open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; string; binexp; +; -; *; /; <; >; <=; >=; ··)
+open import Luau.RuntimeType using (RuntimeType; valueType; function; number; string)
+open import Properties.Equality using (_≢_)
+
+data BinOpError : BinaryOperator → RuntimeType → Set where
+  + : ∀ {t} → (t ≢ number) → BinOpError + t
+  - : ∀ {t} → (t ≢ number) → BinOpError - t
+  * : ∀ {t} → (t ≢ number) → BinOpError * t
+  / : ∀ {t} → (t ≢ number) → BinOpError / t
+  < : ∀ {t} → (t ≢ number) → BinOpError < t
+  > : ∀ {t} → (t ≢ number) → BinOpError > t
+  <= : ∀ {t} → (t ≢ number) → BinOpError <= t
+  >= : ∀ {t} → (t ≢ number) → BinOpError >= t
+  ·· : ∀ {t} → (t ≢ string) → BinOpError ·· t
+  
+data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
+data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
+
+data RuntimeErrorᴱ H where
+  FunctionMismatch : ∀ v w → (valueType v ≢ function) → RuntimeErrorᴱ H (val v $ val w)
+  BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
+  BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
+  UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)
+  SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (val (addr a))
+  app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
+  app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
+  block : ∀ {b B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
+  bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
+  bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)
+
+data RuntimeErrorᴮ H where
+  local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
+  return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
--- a/prototyping/lluz/RuntimeError/ToString.agda
+++ b/prototyping/lluz/RuntimeError/ToString.agda
@ -0,0 +1,31 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.RuntimeError.ToString where
+
+open import Agda.Builtin.Float using (primShowFloat)
+open import FFI.Data.String using (String; _++_)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
+open import Luau.RuntimeType.ToString using (runtimeTypeToString)
+open import Luau.Addr.ToString using (addrToString)
+open import Luau.Syntax.ToString using (valueToString; exprToString)
+open import Luau.Var.ToString using (varToString)
+open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_; ··)
+
+errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String
+errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String
+
+errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
+errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
+errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
+errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
+errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
+errToStringᴱ (binexp M ·· N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a string"
+errToStringᴱ (binexp M ·· N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a string"
+errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
+errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
+errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
+errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E
+errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n  in call of function " ++ varToString (name b)
+
+errToStringᴮ (local x ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n  in definition of " ++ varToString (name x) 
+errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n  in return statement"
--- a/prototyping/lluz/RuntimeType.agda
+++ b/prototyping/lluz/RuntimeType.agda
@ -0,0 +1,17 @@
+module Luau.RuntimeType where
+
+open import Luau.Syntax using (Value; nil; addr; number; bool; string)
+
+data RuntimeType : Set where
+  function : RuntimeType
+  number : RuntimeType
+  nil : RuntimeType
+  boolean : RuntimeType
+  string : RuntimeType
+
+valueType : Value → RuntimeType
+valueType nil = nil
+valueType (addr a) = function
+valueType (number n) = number
+valueType (bool b) = boolean
+valueType (string x) = string
--- a/prototyping/lluz/RuntimeType/ToString.agda
+++ b/prototyping/lluz/RuntimeType/ToString.agda
@ -0,0 +1,11 @@
+module Luau.RuntimeType.ToString where
+
+open import FFI.Data.String using (String)
+open import Luau.RuntimeType using (RuntimeType; function; number; nil; boolean; string)
+
+runtimeTypeToString : RuntimeType → String
+runtimeTypeToString function = "function"
+runtimeTypeToString number = "number"
+runtimeTypeToString nil = "nil"
+runtimeTypeToString boolean = "boolean"
+runtimeTypeToString string = "string"
--- a/prototyping/lluz/StrictMode.agda
+++ b/prototyping/lluz/StrictMode.agda
@ -0,0 +1,194 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.StrictMode where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import FFI.Data.Maybe using (just; nothing)
+open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
+open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_)
+open import Luau.ResolveOverloads using (src; resolve)
+open import Luau.Subtyping using (_≮:_)
+open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
+open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
+open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function; srcBinOp)
+open import Properties.Contradiction using (¬)
+open import Properties.TypeCheck using (typeCheckᴮ)
+open import Properties.Product using (_,_)
+
+data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
+data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set
+
+data Warningᴱ H {Γ} where
+
+  UnallocatedAddress : ∀ {a T} →
+
+    (H [ a ]ᴴ ≡ nothing) →
+    ---------------------
+    Warningᴱ H (addr {a} T)
+
+  UnboundVariable : ∀ {x T p} →
+
+    (Γ [ x ]ⱽ ≡ nothing) →
+    ------------------------
+    Warningᴱ H (var {x} {T} p)
+
+  FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    (U ≮: src T) →
+    -----------------
+    Warningᴱ H (app D₁ D₂)
+  
+  app₁ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₁ →
+    -----------------
+    Warningᴱ H (app D₁ D₂)
+
+  app₂ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₂ →
+    -----------------
+    Warningᴱ H (app D₁ D₂)
+
+  BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    (T ≮: srcBinOp op) →
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    (U ≮: srcBinOp op) →
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  bin₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₁ →    
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  bin₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₂ →    
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+    
+  FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
+
+    (V ≮: U) →
+    -------------------------
+    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)
+
+  BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
+
+    (U ≮: T) →
+    ------------------------------
+    Warningᴱ H (block {b} {T = T} D)
+
+  block₁ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
+
+    Warningᴮ H D →
+    ------------------------------
+    Warningᴱ H (block {b} {T = T} D)
+
+data Warningᴮ H {Γ} where
+
+  return : ∀ {M B T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴮ B ∈ U} →
+
+    Warningᴱ H D₁ →
+    ------------------
+    Warningᴮ H (return D₁ D₂)
+
+  LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
+
+    (U ≮: T) →
+    --------------------
+    Warningᴮ H (local D₁ D₂)
+
+  local₁ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
+
+    Warningᴱ H D₁ →
+    --------------------
+    Warningᴮ H (local D₁ D₂)
+
+  local₂ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
+
+    Warningᴮ H D₂ →
+    --------------------
+    Warningᴮ H (local D₁ D₂)
+
+  FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
+
+    (V ≮: U) →
+    -------------------------------------
+    Warningᴮ H (function D₁ D₂)
+
+  function₁ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
+
+    Warningᴮ H D₁ →
+    --------------------
+    Warningᴮ H (function D₁ D₂)
+
+  function₂ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
+
+    Warningᴮ H D₂ →
+    --------------------
+    Warningᴮ H (function D₁ D₂)
+
+data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where
+
+  FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
+
+    (V ≮: U) →
+    ---------------------------------
+    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₂)
--- a/prototyping/lluz/StrictMode/ToString.agda
+++ b/prototyping/lluz/StrictMode/ToString.agda
@ -0,0 +1,61 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.StrictMode.ToString where
+
+open import Agda.Builtin.Nat using (Nat; suc)
+open import FFI.Data.String using (String; _++_)
+open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err; function-tgt)
+open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
+open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
+open import Luau.Type using (number; boolean; string; nil)
+open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
+open import Luau.Addr.ToString using (addrToString)
+open import Luau.Var.ToString using (varToString)
+open import Luau.Type.ToString using (typeToString)
+open import Luau.Syntax.ToString using (binOpToString)
+
+tmp : Nat → String
+tmp 0 = "w"
+tmp 1 = "x"
+tmp 2 = "y"
+tmp 3 = "z"
+tmp (suc (suc (suc n))) = tmp n ++ "'"
+
+treeToString : Tree → Nat → String → String
+treeToString (scalar number) n v = v ++ " is a number"
+treeToString (scalar boolean) n v = v ++ " is a boolean"
+treeToString (scalar string) n v = v ++ " is a string"
+treeToString (scalar nil) n v = v ++ " is nil"
+treeToString function n v = v ++ " is a function"
+treeToString (function-ok s t) n v = treeToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n  " ++ treeToString s (suc n) w where w = tmp n
+treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ treeToString t (suc n) w where w = tmp n
+treeToString (function-tgt t) n v = treeToString t n (v ++ "()")
+
+subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
+subtypeWarningToString (witness t p q) = "\n  because provided type contains v, where " ++ treeToString t 0 "v"
+
+warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String
+warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String
+
+warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
+warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated address " ++ addrToString a
+warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U ++ subtypeWarningToString p
+warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
+warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
+warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
+warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n  in function expression " ++ varToString f
+warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) =  "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U ++ subtypeWarningToString p
+warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n  in block " ++ varToString b
+warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T ++ subtypeWarningToString p
+warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U ++ subtypeWarningToString p
+warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
+warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W
+
+warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
+warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n  in function declaration " ++ varToString f
+warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W
+warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) =  "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U ++ subtypeWarningToString p
+warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n  in local variable declaration " ++ varToString x
+warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W
+warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n  in return statement"
+
--- a/prototyping/lluz/Substitution.agda
+++ b/prototyping/lluz/Substitution.agda
@ -0,0 +1,28 @@
+module Luau.Substitution where
+
+open import Luau.Syntax using (Value; Expr; Stat; Block; val; nil; bool; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
+open import Luau.Var using (Var; _≡ⱽ_)
+open import Properties.Dec using (Dec; yes; no)
+
+_[_/_]ᴱ : ∀ {a} → Expr a → Value → Var → Expr a
+_[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
+var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a
+_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
+
+val w [ v / x ]ᴱ = val w
+var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
+(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
+function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
+block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
+(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)
+
+(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name(fun F)))
+(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))
+(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
+done [ v / x ]ᴮ = done
+
+var y [ v / x ]ᴱwhenever yes p = val v
+var y [ v / x ]ᴱwhenever no p = var y
+
+B [ v / x ]ᴮunless yes p = B
+B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ
--- a/prototyping/lluz/Subtyping.agda
+++ b/prototyping/lluz/Subtyping.agda
@ -0,0 +1,67 @@
+{-# OPTIONS --rewriting #-}
+
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Properties.Equality using (_≢_)
+
+module Luau.Subtyping where
+
+-- An implementation of semantic subtyping
+
+-- We think of types as languages of trees
+
+data Tree : Set where
+
+  scalar : ∀ {T} → Scalar T → Tree
+  function : Tree
+  function-ok : Tree → Tree → Tree
+  function-err : Tree → Tree
+  function-tgt : Tree → Tree
+
+data Language : Type → Tree → Set
+data ¬Language : Type → Tree → Set
+
+data Language where
+
+  scalar : ∀ {T} → (s : Scalar T) → Language T (scalar s)
+  function : ∀ {T U} → Language (T ⇒ U) function
+  function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u)
+  function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t u)
+  function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
+  function-tgt : ∀ {T U t} → (Language U t) → Language (T ⇒ U) (function-tgt t)
+  left : ∀ {T U t} → Language T t → Language (T ∪ U) t
+  right : ∀ {T U u} → Language U u → Language (T ∪ U) u
+  _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
+  unknown : ∀ {t} → Language unknown t
+
+data ¬Language where
+
+  scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
+  scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
+  scalar-function-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u)
+  scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
+  scalar-function-tgt : ∀ {S t} → (Scalar S) → ¬Language S (function-tgt t)
+  function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
+  function-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u)
+  function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
+  function-tgt : ∀ {T U t} → (¬Language U t) → ¬Language (T ⇒ U) (function-tgt t)
+  _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
+  left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
+  right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
+  never : ∀ {t} → ¬Language never t
+
+-- Subtyping as language inclusion
+
+_<:_ : Type → Type → Set
+(T <: U) = ∀ t → (Language T t) → (Language U t)
+
+-- For warnings, we are interested in failures of subtyping,
+-- which is whrn there is a tree in T's language that isn't in U's.
+
+data _≮:_ (T U : Type) : Set where
+
+  witness : ∀ t →
+
+    Language T t →
+    ¬Language U t →
+    -----------------
+    T ≮: U
--- a/prototyping/lluz/Syntax.agda
+++ b/prototyping/lluz/Syntax.agda
@ -0,0 +1,110 @@
+module Luau.Syntax where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Bool using (Bool; true; false)
+open import Agda.Builtin.Float using (Float)
+open import Agda.Builtin.String using (String)
+open import Luau.Var using (Var)
+open import Luau.Addr using (Addr)
+open import Luau.Type using (Type)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
+infixr 5 _∙_
+
+data Annotated : Set where
+  maybe : Annotated
+  yes : Annotated
+
+data VarDec : Annotated → Set where
+  var : Var → VarDec maybe
+  var_∈_ : ∀ {a} → Var → Type → VarDec a
+
+name : ∀ {a} → VarDec a → Var
+name (var x) = x
+name (var x ∈ T) = x
+
+data FunDec : Annotated → Set where
+  _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
+  _⟨_⟩ : Var → VarDec maybe → FunDec maybe
+
+fun : ∀ {a} → FunDec a → VarDec a
+fun (f ⟨ x ⟩∈ T) = (var f ∈ T)
+fun (f ⟨ x ⟩) = (var f)
+
+arg : ∀ {a} → FunDec a → VarDec a
+arg (f ⟨ x ⟩∈ T) = x
+arg (f ⟨ x ⟩) = x
+
+data BinaryOperator : Set where
+  + : BinaryOperator
+  - : BinaryOperator
+  * : BinaryOperator
+  / : BinaryOperator
+  < : BinaryOperator
+  > : BinaryOperator
+  == : BinaryOperator
+  ~= : BinaryOperator
+  <= : BinaryOperator
+  >= : BinaryOperator
+  ·· : BinaryOperator
+
+data Value : Set where
+  nil : Value
+  addr : Addr → Value
+  number : Float → Value
+  bool : Bool → Value
+  string : String → Value
+
+data Block (a : Annotated) : Set
+data Stat (a : Annotated) : Set
+data Expr (a : Annotated) : Set
+
+data Block a where
+  _∙_ : Stat a → Block a → Block a
+  done : Block a
+
+data Stat a where
+  function_is_end : FunDec a → Block a → Stat a
+  local_←_ : VarDec a → Expr a → Stat a
+  return : Expr a → Stat a
+
+data Expr a where
+  var : Var → Expr a
+  val : Value → Expr a
+  _$_ : Expr a → Expr a → Expr a
+  function_is_end : FunDec a → Block a → Expr a
+  block_is_end : VarDec a → Block a → Expr a
+  binexp : Expr a → BinaryOperator → Expr a → Expr a
+
+isAnnotatedᴱ : ∀ {a} → Expr a → Maybe (Expr yes)
+isAnnotatedᴮ : ∀ {a} → Block a → Maybe (Block yes)
+
+isAnnotatedᴱ (var x) = just (var x)
+isAnnotatedᴱ (val v) = just (val v)
+isAnnotatedᴱ (M $ N) with isAnnotatedᴱ M | isAnnotatedᴱ N
+isAnnotatedᴱ (M $ N) | just M′ | just N′ = just (M′ $ N′)
+isAnnotatedᴱ (M $ N) | _ | _ = nothing
+isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) with isAnnotatedᴮ B
+isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | just B′ = just (function f ⟨ var x ∈ T ⟩∈ U is B′ end)
+isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | _ = nothing
+isAnnotatedᴱ (function _ is B end) = nothing
+isAnnotatedᴱ (block var b ∈ T is B end) with isAnnotatedᴮ B
+isAnnotatedᴱ (block var b ∈ T is B end) | just B′ = just (block var b ∈ T is B′ end)
+isAnnotatedᴱ (block var b ∈ T is B end) | _ = nothing
+isAnnotatedᴱ (block _ is B end) = nothing
+isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N
+isAnnotatedᴱ (binexp M op N) | just M′ | just N′ = just (binexp M′ op N′)
+isAnnotatedᴱ (binexp M op N) | _ | _ = nothing
+
+isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with isAnnotatedᴮ B | isAnnotatedᴮ C
+isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | just B′ | just C′ = just (function f ⟨ var x ∈ T ⟩∈ U is C′ end ∙ B′)
+isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | _ | _ = nothing
+isAnnotatedᴮ (function _ is C end ∙ B) = nothing
+isAnnotatedᴮ (local var x ∈ T ← M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
+isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | just M′ | just B′ = just (local var x ∈ T ← M′ ∙ B′)
+isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | _ | _ = nothing
+isAnnotatedᴮ (local _ ← M ∙ B) = nothing
+isAnnotatedᴮ (return M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
+isAnnotatedᴮ (return M ∙ B) | just M′ | just B′ = just (return M′ ∙ B′)
+isAnnotatedᴮ (return M ∙ B) | _ | _ = nothing
+isAnnotatedᴮ done = just done
--- a/prototyping/lluz/Syntax/FromJSON.agda
+++ b/prototyping/lluz/Syntax/FromJSON.agda
@ -0,0 +1,201 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.Syntax.FromJSON where
+
+open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec;  binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=; ··; string)
+open import Luau.Type.FromJSON using (typeFromJSON)
+
+open import Agda.Builtin.List using (List; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
+
+open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
+open import FFI.Data.Either using (Either; Left; Right)
+open import FFI.Data.Maybe using (Maybe; nothing; just)
+open import FFI.Data.Scientific using (toFloat)
+open import FFI.Data.String using (String; _++_)
+open import FFI.Data.Vector using (head; tail; null; empty)
+
+args = fromString "args"
+body = fromString "body"
+func = fromString "func"
+lokal = fromString "local"
+list = fromString "list"
+name = fromString "name"
+type = fromString "type"
+value = fromString "value"
+values = fromString "values"
+vars = fromString "vars"
+op = fromString "op"
+left = fromString "left"
+right = fromString "right"
+returnAnnotation = fromString "returnAnnotation"
+types = fromString "types"
+
+data Lookup : Set where
+  _,_ : String → Value → Lookup
+  nil : Lookup
+
+lookupIn : List String → Object → Lookup
+lookupIn [] obj = nil
+lookupIn (key ∷ keys) obj with lookup (fromString key) obj
+lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
+lookupIn (key ∷ keys) obj | just value = (key , value)
+
+binOpFromJSON : Value → Either String BinaryOperator
+binOpFromString : String → Either String BinaryOperator
+varDecFromJSON : Value → Either String (VarDec maybe)
+varDecFromObject : Object → Either String (VarDec maybe)
+exprFromJSON : Value → Either String (Expr maybe)
+exprFromObject : Object → Either String (Expr maybe)
+statFromJSON : Value → Either String (Stat maybe)
+statFromObject : Object → Either String (Stat maybe)
+blockFromJSON : Value → Either String (Block maybe)
+blockFromArray : Array → Either String (Block maybe)
+
+binOpFromJSON (string s) = binOpFromString s
+binOpFromJSON _ = Left "Binary operator not a string"
+
+binOpFromString "Add" = Right +
+binOpFromString "Sub" = Right -
+binOpFromString "Mul" = Right *
+binOpFromString "Div" = Right /
+binOpFromString "CompareEq" = Right ==
+binOpFromString "CompareNe" = Right ~=
+binOpFromString "CompareLt" = Right <
+binOpFromString "CompareLe" = Right <=
+binOpFromString "CompareGt" = Right >
+binOpFromString "CompareGe" = Right >=
+binOpFromString "Concat" = Right ··
+binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
+
+varDecFromJSON (object arg) = varDecFromObject arg
+varDecFromJSON _ = Left "VarDec not an object"
+
+varDecFromObject obj with lookup name obj | lookup type obj
+varDecFromObject obj | just (string name) | nothing = Right (var name)
+varDecFromObject obj | just (string name) | just Value.null = Right (var name)
+varDecFromObject obj | just (string name) | just tyValue with typeFromJSON tyValue
+varDecFromObject obj | just (string name) | just tyValue | Right ty = Right (var name ∈ ty)
+varDecFromObject obj | just (string name) | just tyValue | Left err = Left err
+varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string"
+varDecFromObject obj | nothing | _ = Left "AstLocal missing name"
+
+exprFromJSON (object obj) = exprFromObject obj
+exprFromJSON _ = Left "AstExpr not an object"
+
+exprFromObject obj with lookup type obj
+exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) with head arr
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 with exprFromJSON value | exprFromJSON value2
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Right fun | Right arg = Right (fun $ arg)
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Left err | _ = Left err
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | nothing = Left ("AstExprCall empty args")
+exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array")
+exprFromObject obj | just (string "AstExprCall") | nothing | _  = Left ("AstExprCall missing func")
+exprFromObject obj | just (string "AstExprCall") | _ | nothing  = Left ("AstExprCall missing args")
+exprFromObject obj | just (string "AstExprConstantNil") = Right (val nil)
+exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj | lookup returnAnnotation obj
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn with head arr | blockFromJSON blockValue
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B with varDecFromJSON argValue
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg with lookup types rtnObj
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) with head rtnTypes
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType with typeFromJSON rtnType
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Left err = Left err
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Right T = Right (function "" ⟨ arg ⟩∈ T is B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | nothing = Right (function "" ⟨ arg ⟩ is B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just _ = Left "returnAnnotation types not an array"
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | nothing = Left "returnAnnotation missing types"
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just _ | just argValue | Right B | Right arg  = Left "returnAnnotation not an object"
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B | Left err = Left err
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | nothing | Right B = Left "Unsupported AstExprFunction empty args"
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprFunction") | just _ | just _ | rtn = Left "AstExprFunction args not an array"
+exprFromObject obj | just (string "AstExprFunction") | nothing | _ | rtn = Left "AstExprFunction missing args"
+exprFromObject obj | just (string "AstExprFunction") | _ | nothing | rtn = Left "AstExprFunction missing body"
+exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
+exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
+exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
+exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
+exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
+exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (val (number (toFloat x)))
+exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
+exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
+exprFromObject obj | just (string "AstExprConstantString") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantString") | just (string x) = Right (val (string x))
+exprFromObject obj | just (string "AstExprConstantString") | just _ = Left "AstExprConstantString value is not a string"
+exprFromObject obj | just (string "AstExprConstantString") | nothing = Left "AstExprConstantString missing value"
+exprFromObject obj | just (string "AstExprConstantBool") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool b) = Right (val (bool b))
+exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
+exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool missing value"
+exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o′ | Right l′ | Right r′ = Right (binexp l′ o′ r′)
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary"
+exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
+exprFromObject obj | just _ = Left "AstExpr type not a string"
+exprFromObject obj | nothing = Left "AstExpr missing type"
+
+{-# NON_TERMINATING #-}
+statFromJSON (object obj) = statFromObject obj
+statFromJSON _ = Left "AstStat not an object"
+
+statFromObject obj with lookup type obj
+statFromObject obj | just(string "AstStatLocal") with lookup vars obj | lookup values obj
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) with head(arr1) | head(arr2)
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) with varDecFromJSON(x) | exprFromJSON(value)
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | Right x′ | Right M = Right (local x′ ← M)
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | Left err | _ = Left err
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | _ | Left err = Left err
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | nothing = Left "AstStatLocal empty values"
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | nothing | _ = Left "AstStatLocal empty vars"
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(_) = Left "AstStatLocal values not an array"
+statFromObject obj | just(string "AstStatLocal") | just(_) | just(_) = Left "AstStatLocal vars not an array"
+statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "AstStatLocal missing values"
+statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
+statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
+statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
+statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩ is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩ is B end)
+statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩∈ T is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩∈ T is B end)
+statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
+statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err
+statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
+statFromObject obj | just(string "AstStatLocalFunction") | nothing | _ = Left "AstStatFunction missing name"
+statFromObject obj | just(string "AstStatLocalFunction") | _ | nothing = Left "AstStatFunction missing func"
+statFromObject obj | just(string "AstStatReturn") with lookup list obj
+statFromObject obj | just(string "AstStatReturn") | just(array arr) with head arr
+statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value with exprFromJSON value
+statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Right M = Right (return M)
+statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Left err = Left err
+statFromObject obj | just(string "AstStatReturn") | just(array arr) | nothing = Left "AstStatReturn empty list"
+statFromObject obj | just(string "AstStatReturn") | just(_) = Left "AstStatReturn list not an array"
+statFromObject obj | just(string "AstStatReturn") | nothing = Left "AstStatReturn missing list"
+statFromObject obj | just (string ty) = Left ("TODO: Unsupported AstStat " ++ ty)
+statFromObject obj | just _ = Left "AstStat type not a string"
+statFromObject obj | nothing = Left "AstStat missing type"
+
+blockFromJSON (array arr) = blockFromArray arr
+blockFromJSON (object obj) with lookup type obj | lookup body obj
+blockFromJSON (object obj) | just (string "AstStatBlock") | just value = blockFromJSON value
+blockFromJSON (object obj) | just (string "AstStatBlock") | nothing = Left "AstStatBlock missing body"
+blockFromJSON (object obj) | just (string ty) | _ = Left ("Unsupported AstBlock " ++ ty)
+blockFromJSON (object obj) | just _ | _ = Left "AstStatBlock type not a string"
+blockFromJSON (object obj) | nothing | _ = Left "AstStatBlock missing type"
+blockFromJSON _ = Left "AstBlock not an array or AstStatBlock object"
+
+blockFromArray arr with head arr
+blockFromArray arr | nothing = Right done
+blockFromArray arr | just value with statFromJSON value
+blockFromArray arr | just value | Left err = Left err
+blockFromArray arr | just value | Right S with blockFromArray(tail arr)
+blockFromArray arr | just value | Right S | Left err = Left (err)
+blockFromArray arr | just value | Right S | Right B  = Right (S ∙ B)
+   
--- a/prototyping/lluz/Syntax/ToString.agda
+++ b/prototyping/lluz/Syntax/ToString.agda
@ -0,0 +1,83 @@
+module Luau.Syntax.ToString where
+
+open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.Float using (primShowFloat)
+open import Agda.Builtin.String using (primShowString)
+open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; binexp; string)
+open import FFI.Data.String using (String; _++_)
+open import Luau.Addr.ToString using (addrToString)
+open import Luau.Type.ToString using (typeToString)
+open import Luau.Var.ToString using (varToString)
+
+varDecToString : ∀ {a} → VarDec a → String
+varDecToString (var x) = varToString x
+varDecToString (var x ∈ T) =  varToString x ++ " : " ++ typeToString T
+
+funDecToString : ∀ {a} → FunDec a → String
+funDecToString ("" ⟨ x ⟩∈ T) = "function(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
+funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
+
+binOpToString : BinaryOperator → String
+binOpToString + = "+"
+binOpToString - = "-"
+binOpToString * = "*"
+binOpToString / = "/"
+binOpToString < = "<"
+binOpToString > = ">"
+binOpToString == = "=="
+binOpToString ~= = "~="
+binOpToString <= = "<="
+binOpToString >= = ">="
+binOpToString ·· = ".."
+
+valueToString : Value → String
+valueToString nil = "nil"
+valueToString (addr a) = addrToString a
+valueToString (number x) = primShowFloat x
+valueToString (bool false) = "false"
+valueToString (bool true) = "true"
+valueToString (string x) = primShowString x
+
+exprToString′ : ∀ {a} → String → Expr a → String
+statToString′ : ∀ {a} → String → Stat a → String
+blockToString′ : ∀ {a} → String → Block a → String
+
+exprToString′ lb (val v) =
+  valueToString(v)
+exprToString′ lb (var x) =
+  varToString(x)
+exprToString′ lb (M $ N) =
+  (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
+exprToString′ lb (function F is B end) =
+  funDecToString F ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end"
+exprToString′ lb (block b is B end) =
+  "(" ++ varDecToString b ++ "()" ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end)()"
+exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
+
+statToString′ lb (function F is B end) =
+  "local " ++ funDecToString F ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end"
+statToString′ lb (local x ← M) =
+  "local " ++ varDecToString x ++ " = " ++ (exprToString′ lb M)
+statToString′ lb (return M) =
+  "return " ++ (exprToString′ lb M)
+
+blockToString′ lb (S ∙ done) = statToString′ lb S
+blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
+blockToString′ lb (done) = ""
+
+exprToString : ∀ {a} → Expr a → String
+exprToString = exprToString′ "\n"
+
+statToString : ∀ {a} → Stat a → String
+statToString = statToString′ "\n"
+
+blockToString : ∀ {a} → Block a → String
+blockToString = blockToString′ "\n"
--- a/prototyping/lluz/Type.agda
+++ b/prototyping/lluz/Type.agda
@ -0,0 +1,164 @@
+module Luau.Type where
+
+open import FFI.Data.Maybe using (Maybe; just; nothing; just-inv)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Properties.Dec using (Dec; yes; no)
+open import Properties.Equality using (cong)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
+data Type : Set where
+  nil : Type
+  _⇒_ : Type → Type → Type
+  never : Type
+  unknown : Type
+  boolean : Type
+  number : Type
+  string : Type
+  _∪_ : Type → Type → Type
+  _∩_ : Type → Type → Type
+
+data Scalar : Type → Set where
+
+  number : Scalar number
+  boolean : Scalar boolean
+  string : Scalar string
+  nil : Scalar nil
+
+skalar = number ∪ (string ∪ (nil ∪ boolean))
+
+lhs : Type → Type
+lhs (T ⇒ _) = T
+lhs (T ∪ _) = T
+lhs (T ∩ _) = T
+lhs nil = nil
+lhs never = never
+lhs unknown = unknown
+lhs number = number
+lhs boolean = boolean
+lhs string = string
+
+rhs : Type → Type
+rhs (_ ⇒ T) = T
+rhs (_ ∪ T) = T
+rhs (_ ∩ T) = T
+rhs nil = nil
+rhs never = never
+rhs unknown = unknown
+rhs number = number
+rhs boolean = boolean
+rhs string = string
+
+_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
+nil ≡ᵀ nil = yes refl
+nil ≡ᵀ (S ⇒ T) = no (λ ())
+nil ≡ᵀ never = no (λ ())
+nil ≡ᵀ unknown = no (λ ())
+nil ≡ᵀ number = no (λ ())
+nil ≡ᵀ boolean = no (λ ())
+nil ≡ᵀ (S ∪ T) = no (λ ())
+nil ≡ᵀ (S ∩ T) = no (λ ())
+nil ≡ᵀ string = no (λ ())
+(S ⇒ T) ≡ᵀ string = no (λ ())
+never ≡ᵀ string = no (λ ())
+unknown ≡ᵀ string = no (λ ())
+boolean ≡ᵀ string = no (λ ())
+number ≡ᵀ string = no (λ ())
+(S ∪ T) ≡ᵀ string = no (λ ())
+(S ∩ T) ≡ᵀ string = no (λ ())
+(S ⇒ T) ≡ᵀ nil = no (λ ())
+(S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V) 
+(S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
+(S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q))
+(S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q))
+(S ⇒ T) ≡ᵀ never = no (λ ())
+(S ⇒ T) ≡ᵀ unknown = no (λ ())
+(S ⇒ T) ≡ᵀ number = no (λ ())
+(S ⇒ T) ≡ᵀ boolean = no (λ ())
+(S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ())
+(S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ())
+never ≡ᵀ nil = no (λ ())
+never ≡ᵀ (U ⇒ V) = no (λ ())
+never ≡ᵀ never = yes refl
+never ≡ᵀ unknown = no (λ ())
+never ≡ᵀ number = no (λ ())
+never ≡ᵀ boolean = no (λ ())
+never ≡ᵀ (U ∪ V) = no (λ ())
+never ≡ᵀ (U ∩ V) = no (λ ())
+unknown ≡ᵀ nil = no (λ ())
+unknown ≡ᵀ (U ⇒ V) = no (λ ())
+unknown ≡ᵀ never = no (λ ())
+unknown ≡ᵀ unknown = yes refl
+unknown ≡ᵀ number = no (λ ())
+unknown ≡ᵀ boolean = no (λ ())
+unknown ≡ᵀ (U ∪ V) = no (λ ())
+unknown ≡ᵀ (U ∩ V) = no (λ ())
+number ≡ᵀ nil = no (λ ())
+number ≡ᵀ (T ⇒ U) = no (λ ())
+number ≡ᵀ never = no (λ ())
+number ≡ᵀ unknown = no (λ ())
+number ≡ᵀ number = yes refl
+number ≡ᵀ boolean = no (λ ())
+number ≡ᵀ (T ∪ U) = no (λ ())
+number ≡ᵀ (T ∩ U) = no (λ ())
+boolean ≡ᵀ nil = no (λ ())
+boolean ≡ᵀ (T ⇒ U) = no (λ ())
+boolean ≡ᵀ never = no (λ ())
+boolean ≡ᵀ unknown = no (λ ())
+boolean ≡ᵀ boolean = yes refl
+boolean ≡ᵀ number = no (λ ())
+boolean ≡ᵀ (T ∪ U) = no (λ ())
+boolean ≡ᵀ (T ∩ U) = no (λ ())
+string ≡ᵀ nil = no (λ ())
+string ≡ᵀ (x ⇒ x₁) = no (λ ())
+string ≡ᵀ never = no (λ ())
+string ≡ᵀ unknown = no (λ ())
+string ≡ᵀ boolean = no (λ ())
+string ≡ᵀ number = no (λ ())
+string ≡ᵀ string = yes refl
+string ≡ᵀ (U ∪ V) = no (λ ())
+string ≡ᵀ (U ∩ V) = no (λ ())
+(S ∪ T) ≡ᵀ nil = no (λ ())
+(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
+(S ∪ T) ≡ᵀ never = no (λ ())
+(S ∪ T) ≡ᵀ unknown = no (λ ())
+(S ∪ T) ≡ᵀ number = no (λ ())
+(S ∪ T) ≡ᵀ boolean = no (λ ())
+(S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V) 
+(S ∪ T) ≡ᵀ (S ∪ T) | yes refl | yes refl = yes refl
+(S ∪ T) ≡ᵀ (U ∪ V) | _ | no p = no (λ q → p (cong rhs q))
+(S ∪ T) ≡ᵀ (U ∪ V) | no p | _ = no (λ q → p (cong lhs q))
+(S ∪ T) ≡ᵀ (U ∩ V) = no (λ ())
+(S ∩ T) ≡ᵀ nil = no (λ ())
+(S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ())
+(S ∩ T) ≡ᵀ never = no (λ ())
+(S ∩ T) ≡ᵀ unknown = no (λ ())
+(S ∩ T) ≡ᵀ number = no (λ ())
+(S ∩ T) ≡ᵀ boolean = no (λ ())
+(S ∩ T) ≡ᵀ (U ∪ V) = no (λ ())
+(S ∩ T) ≡ᵀ (U ∩ V) with (S ≡ᵀ U) | (T ≡ᵀ V) 
+(S ∩ T) ≡ᵀ (U ∩ V) | yes refl | yes refl = yes refl
+(S ∩ T) ≡ᵀ (U ∩ V) | _ | no p = no (λ q → p (cong rhs q))
+(S ∩ T) ≡ᵀ (U ∩ V) | no p | _ = no (λ q → p (cong lhs q))
+
+_≡ᴹᵀ_ : ∀ (T U : Maybe Type) → Dec(T ≡ U)
+nothing ≡ᴹᵀ nothing = yes refl
+nothing ≡ᴹᵀ just U = no (λ ())
+just T ≡ᴹᵀ nothing = no (λ ())
+just T ≡ᴹᵀ just U with T ≡ᵀ U
+(just T ≡ᴹᵀ just T) | yes refl = yes refl
+(just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))
+
+optional : Type → Type
+optional nil = nil
+optional (T ∪ nil) = (T ∪ nil)
+optional T = (T ∪ nil)
+
+normalizeOptional : Type → Type
+normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
+normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | S′         | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | (S′ ∪ nil) | T′         = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | S′         | nil        = optional S′
+normalizeOptional (S ∪ T) | nil        | T′         = optional T′
+normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
+normalizeOptional T = T
--- a/prototyping/lluz/Type/FromJSON.agda
+++ b/prototyping/lluz/Type/FromJSON.agda
@ -0,0 +1,72 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.Type.FromJSON where
+
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; unknown; never; number; string)
+
+open import Agda.Builtin.List using (List; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
+
+open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
+open import FFI.Data.Either using (Either; Left; Right)
+open import FFI.Data.Maybe using (Maybe; nothing; just)
+open import FFI.Data.String using (String; _++_)
+open import FFI.Data.Vector using (head; tail; null; empty)
+
+name = fromString "name"
+type = fromString "type"
+argTypes = fromString "argTypes"
+returnTypes = fromString "returnTypes"
+types = fromString "types"
+
+{-# TERMINATING #-}
+typeFromJSON : Value → Either String Type
+compoundFromArray : (Type → Type → Type) → Array → Either String Type
+
+typeFromJSON (object o) with lookup type o
+typeFromJSON (object o) | just (string "AstTypeFunction") with lookup argTypes o | lookup returnTypes o
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) with lookup types argsSet | lookup types retsSet
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) with head args | head rets
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue with typeFromJSON argValue | typeFromJSON retValue
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Right arg | Right ret = Right (arg ⇒ ret)
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Left err | _ = Left err
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | _ | Left err = Left err
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | _ | nothing = Left "No return type"
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | nothing | _ = Left "No argument type"
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just _ | _ = Left "argTypes.types is not an array"
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | _ | just _ = Left "retTypes.types is not an array"
+typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | nothing | _ = Left "argTypes.types does not exist"
+typeFromJSON (object o) | just (string "AstTypeFunction") | _ | just _ = Left "argTypes is not an object"
+typeFromJSON (object o) | just (string "AstTypeFunction") | just _ | _ = Left "returnTypes is not an object"
+typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing = Left "Missing argTypes and returnTypes"
+
+typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right unknown -- not quite right
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "unknown") = Right unknown
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "never") = Right never
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "string") = Right string
+typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
+
+typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o
+typeFromJSON (object o) | just (string "AstTypeUnion") | just (array types) = compoundFromArray _∪_ types
+typeFromJSON (object o) | just (string "AstTypeUnion") | _ = Left "`types` field must be an array"
+
+typeFromJSON (object o) | just (string "AstTypeIntersection") with lookup types o
+typeFromJSON (object o) | just (string "AstTypeIntersection") | just (array types) = compoundFromArray _∩_ types
+typeFromJSON (object o) | just (string "AstTypeIntersection") | _ = Left "`types` field must be an array"
+
+typeFromJSON (object o) | just (string ty) = Left ("Unsupported type " ++ ty)
+typeFromJSON (object o) | just _ = Left "`type` field must be a string"
+typeFromJSON (object o) | nothing = Left "No `type` field"
+typeFromJSON _ = Left "Unsupported JSON type"
+
+compoundFromArray ctor ts with head ts | tail ts
+compoundFromArray ctor ts | just hd | tl with null tl
+compoundFromArray ctor ts | just hd | tl | true = typeFromJSON hd
+compoundFromArray ctor ts | just hd | tl | false with typeFromJSON hd | compoundFromArray ctor tl
+compoundFromArray ctor ts | just hd | tl | false | Right hdTy | Right tlTy = Right (ctor hdTy tlTy)
+compoundFromArray ctor ts | just hd | tl | false | Left err | _ = Left err
+compoundFromArray ctor ts | just hd | tl | false | _ | Left Err = Left Err
+compoundFromArray ctor ts | nothing | empty = Left "Empty types array?"
--- a/prototyping/lluz/Type/ToString.agda
+++ b/prototyping/lluz/Type/ToString.agda
@ -0,0 +1,29 @@
+module Luau.Type.ToString where
+
+open import FFI.Data.String using (String; _++_)
+open import Luau.Type using (Type; nil; _⇒_; never; unknown; number; boolean; string; _∪_; _∩_; normalizeOptional)
+
+{-# TERMINATING #-}
+typeToString : Type → String
+typeToStringᵁ : Type → String
+typeToStringᴵ : Type → String
+
+typeToString nil = "nil"
+typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
+typeToString never = "never"
+typeToString unknown = "unknown"
+typeToString number = "number"
+typeToString boolean = "boolean"
+typeToString string = "string"
+typeToString (S ∪ T) with normalizeOptional(S ∪ T)
+typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
+typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
+typeToString (S ∪ T) | (S′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")"
+typeToString (S ∪ T) | T′ = typeToString T′
+typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")"
+
+typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T)
+typeToStringᵁ T = typeToString T
+
+typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
+typeToStringᴵ T = typeToString T
--- a/prototyping/lluz/TypeCheck.agda
+++ b/prototyping/lluz/TypeCheck.agda
@ -0,0 +1,160 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.TypeCheck where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import FFI.Data.Either using (Either; Left; Right)
+open import FFI.Data.Maybe using (Maybe; just)
+open import Luau.ResolveOverloads using (resolve)
+open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
+open import Luau.Var using (Var)
+open import Luau.Addr using (Addr)
+open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
+open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_)
+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.DecSubtyping using (dec-subtyping)
+open import Properties.Product using (_×_; _,_)
+
+orUnknown : Maybe Type → Type
+orUnknown nothing = unknown
+orUnknown (just T) = T
+
+srcBinOp : BinaryOperator → Type
+srcBinOp + = number
+srcBinOp - = number
+srcBinOp * = number
+srcBinOp / = number
+srcBinOp < = number
+srcBinOp > = number
+srcBinOp == = unknown
+srcBinOp ~= = unknown
+srcBinOp <= = number
+srcBinOp >= = number
+srcBinOp ·· = string
+
+tgtBinOp : BinaryOperator → Type
+tgtBinOp + = number
+tgtBinOp - = number
+tgtBinOp * = number
+tgtBinOp / = number
+tgtBinOp < = boolean
+tgtBinOp > = boolean
+tgtBinOp == = boolean
+tgtBinOp ~= = boolean
+tgtBinOp <= = boolean
+tgtBinOp >= = boolean
+tgtBinOp ·· = string
+
+data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
+data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set
+
+data _⊢ᴮ_∈_ where
+
+  done : ∀ {Γ} →
+
+    ---------------
+    Γ ⊢ᴮ done ∈ nil
+
+  return : ∀ {M B T U Γ} →
+
+    Γ ⊢ᴱ M ∈ T →
+    Γ ⊢ᴮ B ∈ U →
+    ---------------------
+    Γ ⊢ᴮ return M ∙ B ∈ T
+
+  local : ∀ {x M B T U V Γ} →
+
+    Γ ⊢ᴱ M ∈ U →
+    (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
+    --------------------------------
+    Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V
+
+  function : ∀ {f x B C T U V W Γ} →
+
+    (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V →
+    (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W →
+    -------------------------------------------------
+    Γ ⊢ᴮ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W
+
+data _⊢ᴱ_∈_ where
+
+  nil : ∀ {Γ} →
+
+    --------------------
+    Γ ⊢ᴱ (val nil) ∈ nil
+
+  var : ∀ {x T Γ} →
+
+    T ≡ orUnknown(Γ [ x ]ⱽ) →
+    ----------------
+    Γ ⊢ᴱ (var x) ∈ T
+
+  addr : ∀ {a Γ} T →
+
+    -----------------
+    Γ ⊢ᴱ val(addr a) ∈ T
+
+  number : ∀ {n Γ} →
+
+    ---------------------------
+    Γ ⊢ᴱ val(number n) ∈ number
+
+  bool : ∀ {b Γ} →
+
+    --------------------------
+    Γ ⊢ᴱ val(bool b) ∈ boolean
+  
+  string : ∀ {x Γ} →
+
+    ---------------------------
+    Γ ⊢ᴱ val(string x) ∈ string
+
+  app : ∀ {M N T U Γ} →
+
+    Γ ⊢ᴱ M ∈ T →
+    Γ ⊢ᴱ N ∈ U →
+    ----------------------------
+    Γ ⊢ᴱ (M $ N) ∈ (resolve T U)
+
+  function : ∀ {f x B T U V Γ} →
+
+    (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
+    -----------------------------------------------------
+    Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U)
+
+  block : ∀ {b B T U Γ} →
+
+    Γ ⊢ᴮ B ∈ U →
+    ------------------------------------
+    Γ ⊢ᴱ (block var b ∈ T is B end) ∈ T
+
+  binexp : ∀ {op Γ M N T U} →
+
+    Γ ⊢ᴱ M ∈ T →
+    Γ ⊢ᴱ N ∈ U →
+    ----------------------------------
+    Γ ⊢ᴱ (binexp M op N) ∈ tgtBinOp op
+
+data ⊢ᴼ_ : Maybe(Object yes) → Set where
+
+  nothing :
+
+    ---------
+    ⊢ᴼ nothing
+
+  function : ∀ {f x T U V B} →
+
+    (x ↦ T) ⊢ᴮ B ∈ V →
+    ----------------------------------------------
+    ⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end)
+
+⊢ᴴ_ : Heap yes → Set
+⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O)
+
+_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set
+(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T)
+
+_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set
+(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T)
--- a/prototyping/lluz/TypeNormalization.agda
+++ b/prototyping/lluz/TypeNormalization.agda
@ -0,0 +1,65 @@
+module Luau.TypeNormalization where
+
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+
+-- Operations on normalized types
+_∪ᶠ_ : Type → Type → Type
+_∪ⁿˢ_ : Type → Type → Type
+_∩ⁿˢ_ : Type → Type → Type
+_∪ⁿ_ : Type → Type → Type
+_∩ⁿ_ : Type → Type → Type
+
+-- Union of function types
+(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
+F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ (F ∪ᶠ G₂)
+(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ (S ∪ⁿ U)
+F ∪ᶠ G = F ∪ G
+
+-- Union of normalized types
+S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
+S ∪ⁿ unknown = unknown
+S ∪ⁿ never = S
+never ∪ⁿ T = T
+unknown ∪ⁿ T = unknown
+(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
+F ∪ⁿ G = F ∪ᶠ G
+
+-- Intersection of normalized types
+S ∩ⁿ (T₁ ∪ T₂) = (S ∩ⁿ T₁) ∪ⁿˢ (S ∩ⁿˢ T₂)
+S ∩ⁿ unknown = S
+S ∩ⁿ never = never
+(S₁ ∪ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
+unknown ∩ⁿ G = G
+never ∩ⁿ G = never
+F ∩ⁿ G = F ∩ G
+
+-- Intersection of normalized types with a scalar
+(S₁ ∪ nil) ∩ⁿˢ nil = nil
+(S₁ ∪ boolean) ∩ⁿˢ boolean = boolean
+(S₁ ∪ number) ∩ⁿˢ number = number
+(S₁ ∪ string) ∩ⁿˢ string = string
+(S₁ ∪ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
+unknown ∩ⁿˢ T = T
+F ∩ⁿˢ T = never
+
+-- Union of normalized types with an optional scalar
+S ∪ⁿˢ never = S
+unknown ∪ⁿˢ T = unknown
+(S₁ ∪ nil) ∪ⁿˢ nil = S₁ ∪ nil
+(S₁ ∪ boolean) ∪ⁿˢ boolean = S₁ ∪ boolean
+(S₁ ∪ number) ∪ⁿˢ number = S₁ ∪ number
+(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ string
+(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
+F ∪ⁿˢ T = F ∪ T
+
+-- Normalize!
+normalize : Type → Type
+normalize nil = never ∪ nil
+normalize (S ⇒ T) = (normalize S ⇒ normalize T)
+normalize never = never
+normalize unknown = unknown
+normalize boolean = never ∪ boolean
+normalize number = never ∪ number
+normalize string = never ∪ string
+normalize (S ∪ T) = normalize S ∪ⁿ normalize T
+normalize (S ∩ T) = normalize S ∩ⁿ normalize T
--- a/prototyping/lluz/TypeSaturation.agda
+++ b/prototyping/lluz/TypeSaturation.agda
@ -0,0 +1,66 @@
+module Luau.TypeSaturation where
+
+open import Luau.Type using (Type; _⇒_; _∩_; _∪_)
+open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
+
+-- So, there's a problem with overloaded functions
+-- (of the form (S_1 ⇒ T_1) ∩⋯∩ (S_n ⇒ T_n))
+-- which is that it's not good enough to compare them
+-- for subtyping by comparing all of their overloads.
+
+-- For example (nil → nil) is a subtype of (number? → number?) ∩ (string? → string?)
+-- but not a subtype of any of its overloads.
+
+-- To fix this, we adapt the semantic subtyping algorithm for
+-- function types, given in
+-- https://www.irif.fr/~gc/papers/covcon-again.pdf and
+-- https://pnwamk.github.io/sst-tutorial/
+
+-- A function type is *intersection-saturated* if for any overloads
+-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
+-- of ((S₁ ∩ S₂) ⇒ (T₁ ∩ T₂)).
+
+-- A function type is *union-saturated* if for any overloads
+-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
+-- of ((S₁ ∪ S₂) ⇒ (T₁ ∪ T₂)).
+
+-- A function type is *saturated* if it is both intersection- and
+-- union-saturated.
+
+-- For example (number? → number?) ∩ (string? → string?)
+-- is not saturated, but (number? → number?) ∩ (string? → string?) ∩ (nil → nil) ∩ ((number ∪ string)? → (number ∪ string)?)
+-- is.
+
+-- Saturated function types have the nice property that they can ber
+-- compared by just comparing their overloads: F <: G whenever for any
+-- overload of G, there is an overload os F which is a subtype of it.
+
+-- Forunately every function type can be saturated!
+_⋓_ : Type → Type → Type
+(S₁ ⇒ T₁) ⋓ (S₂ ⇒ T₂) = (S₁ ∪ⁿ S₂) ⇒ (T₁ ∪ⁿ T₂)
+(F₁ ∩ G₁) ⋓ F₂ = (F₁ ⋓ F₂) ∩ (G₁ ⋓ F₂)
+F₁ ⋓ (F₂ ∩ G₂) = (F₁ ⋓ F₂) ∩ (F₁ ⋓ G₂)
+F ⋓ G = F ∩ G
+
+_⋒_ : Type → Type → Type
+(S₁ ⇒ T₁) ⋒ (S₂ ⇒ T₂) = (S₁ ∩ⁿ S₂) ⇒ (T₁ ∩ⁿ T₂)
+(F₁ ∩ G₁) ⋒ F₂ = (F₁ ⋒ F₂) ∩ (G₁ ⋒ F₂)
+F₁ ⋒ (F₂ ∩ G₂) = (F₁ ⋒ F₂) ∩ (F₁ ⋒ G₂)
+F ⋒ G = F ∩ G
+
+_∩ᵘ_ : Type → Type → Type
+F ∩ᵘ G = (F ∩ G) ∩ (F ⋓ G)
+
+_∩ⁱ_ : Type → Type → Type
+F ∩ⁱ G = (F ∩ G) ∩ (F ⋒ G)
+
+∪-saturate : Type → Type
+∪-saturate (F ∩ G) = (∪-saturate F ∩ᵘ ∪-saturate G)
+∪-saturate F = F
+
+∩-saturate : Type → Type
+∩-saturate (F ∩ G) = (∩-saturate F ∩ⁱ ∩-saturate G)
+∩-saturate F = F
+
+saturate : Type → Type
+saturate F = ∪-saturate (∩-saturate F)
--- a/prototyping/lluz/Var.agda
+++ b/prototyping/lluz/Var.agda
@ -0,0 +1,16 @@
+module Luau.Var where
+
+open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.String using (String; primStringEquality)
+open import Agda.Builtin.TrustMe using (primTrustMe)
+open import Properties.Dec using (Dec; yes; no)
+open import Properties.Equality using (_≢_)
+
+Var : Set
+Var = String
+
+_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
+a ≡ⱽ b with primStringEquality a b
+a ≡ⱽ b | false = no p where postulate p : (a ≢ b)
+a ≡ⱽ b | true = yes primTrustMe
--- a/prototyping/lluz/Var/ToString.agda
+++ b/prototyping/lluz/Var/ToString.agda
@ -0,0 +1,8 @@
+module Luau.Var.ToString where
+
+open import Agda.Builtin.String using (String)
+open import Luau.Var using (Var)
+
+varToString : Var → String
+varToString x = x
+
--- a/prototyping/lluz/VarCtxt.agda
+++ b/prototyping/lluz/VarCtxt.agda
@ -0,0 +1,43 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.VarCtxt where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Luau.Type using (Type; _∪_; _∩_)
+open import Luau.Var using (Var)
+open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from; insert-swap; insert-over)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+open import Properties.Equality using (_≢_; cong; sym; trans)
+
+VarCtxt : Set
+VarCtxt = KeyMap Type
+
+∅ : VarCtxt
+∅ = empty
+
+_⋒_ : VarCtxt → VarCtxt → VarCtxt
+_⋒_ = unionWith _∩_
+
+_⋓_ : VarCtxt → VarCtxt → VarCtxt
+_⋓_ = unionWith _∪_
+
+_[_] : VarCtxt → Var → Maybe Type
+Γ [ x ] = lookup (fromString x) Γ
+
+_⊝_ : VarCtxt → Var → VarCtxt
+Γ ⊝ x = delete (fromString x) Γ
+
+_↦_ : Var → Type → VarCtxt
+x ↦ T = singleton (fromString x) T
+
+_⊕_↦_ : VarCtxt → Var → Type → VarCtxt
+Γ ⊕ x ↦ T = insert (fromString x) T Γ
+
+⊕-over : ∀ {Γ x y T U} → (x ≡ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ (Γ ⊕ y ↦ U)
+⊕-over p = insert-over _ _ _ _ _ (cong fromString (sym p))
+
+⊕-swap : ∀ {Γ x y T U} → (x ≢ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ ((Γ ⊕ y ↦ U) ⊕ x ↦ T)
+⊕-swap p = insert-swap _ _ _ _ _ (λ q → p (trans (sym (to-from _)) (trans (cong toString (sym q) ) (to-from _))) )
+
+⊕-lookup-miss : ∀ x y T Γ → (x ≢ y) → (Γ [ y ] ≡ (Γ ⊕ x ↦ T) [ y ])
+⊕-lookup-miss x y T Γ p = lookup-insert-not (fromString x) (fromString y) T Γ λ q → p (trans (sym (to-from x)) (trans (cong toString q) (to-from y)))
--- a/rfcs/README.md
+++ b/rfcs/README.md
@ -18,13 +18,6 @@ For changes in semantics, we should be asking:
 - Can it be sandboxed assuming malicious usage?
 - Is it compatible with type checking and other forms of static analysis?

-For new standard library functions, we should be asking:
-
- Is the new functionality used/useful often enough in existing code?
- Does the standard library implementation carry important performance benefits that can't be achieved in user code?
- Is the behavior general and unambiguous, as opposed to solving a problem / providing an interface that's too specific?
- Is the function interface amenable to type checking / linting?
-
 In addition to these questions, we also need to consider that every addition carries a cost, and too many features will result in a language that is harder to learn, harder to implement and ensure consistent implementation quality throughout, slower, etc. In addition, any language is greater than the sum of its parts and features often have non-intuitive interactions with each other.

 Since reversing these decisions is incredibly costly and can be impossible due to backwards compatibility implications, all user facing changes to Luau language and core libraries must go through an RFC process.
--- a/rfcs/syntax-string-interpolation.md
+++ b/rfcs/syntax-string-interpolation.md
@ -31,9 +31,9 @@ Because we care about backward compatibility, we need some new syntax in order t

 1. A string chunk (`` `...{ ``, `}...{`, and `` }...` ``) where `...` is a range of 0 to many characters.
   * `\` escapes `` ` ``, `{`, and itself `\`.
+   * Restriction: the string interpolation literal must have at least one value to interpolate. We do not need 3 ways to express a single line string literal.
   * The pairs must be on the same line (unless a `\` escapes the newline) but expressions needn't be on the same line.
 2. An expression between the braces. This is the value that will be interpolated into the string.
-   * Restriction: we explicitly reject `{{` as it is considered an attempt to escape and get a single `{` character at runtime.
 3. Formatting specification may follow after the expression, delimited by an unambiguous character.
   * Restriction: the formatting specification must be constant at parse time.
   * In the absence of an explicit formatting specification, the `%*` token will be used.
@ -61,6 +61,7 @@ local set2 = Set.new({0, 5, 4})
 print(`{set1} ∪ {set2} = {Set.union(set1, set2)}`)
 --> {0, 1, 3} ∪ {0, 5, 4} = {0, 1, 3, 4, 5}

+-- For illustrative purposes. These are illegal specifically because they don't interpolate anything.
 print(`Some example escaping the braces \{like so}`)
 print(`backslash \ that escapes the space is not a part of the string...`)
 print(`backslash \\ will escape the second backslash...`)
@ -87,25 +88,13 @@ print(`Welcome to \
 --  Luau!
 ```

-This expression can also come after a `prefixexp`:
+This expression will not be allowed to come after a `prefixexp`. I believe this is fully additive, so a future RFC may allow this. So for now, we explicitly reject the following:

 ```
 local name = "world"
 print`Hello {name}`
 ```

-The restriction on `{{` exists solely for the people coming from languages e.g. C#, Rust, or Python which uses `{{` to escape and get the character `{` at runtime. We're also rejecting this at parse time too, since the proper way to escape it is `\{`, so:
-
-```lua
-print(`{{1, 2, 3}} = {myCoolSet}`) -- parse error
-```
-
-If we did not apply this as a parse error, then the above would wind up printing as the following, which is obviously a gotcha we can and should avoid.
-
-```
--> table: 0xSOMEADDRESS = {1, 2, 3}
-```
-
 Since the string interpolation expression is going to be lowered into a `string.format` call, we'll also need to extend `string.format`. The bare minimum to support the lowering is to add a new token whose definition is to perform a `tostring` call. `%*` is currently an invalid token, so this is a backward compatible extension. This RFC shall define `%*` to have the same behavior as if `tostring` was called.

 ```lua
@ -132,13 +121,6 @@ print(string.format("%* %* %*", return_two_nils()))
 --> error: value #3 is missing, got 2
 ```

-It must be said that we are not allowing this style of string literals in type annotations at this time, regardless of zero or many interpolating expressions, so the following two type annotations below are illegal syntax:
-
-```lua
-local foo: `foo`
-local bar: `bar{baz}`
-```
-
 ## Drawbacks

 If we want to use backticks for other purposes, it may introduce some potential ambiguity. One option to solve that is to only ever produce string interpolation tokens from the context of an expression. This is messy but doable because the parser and the lexer are already implemented to work in tandem. The other option is to pick a different delimiter syntax to keep backticks available for use in the future.