Merge branch 'master' into merge

2025-04-04 02:40:53 +01:00 · 2022-02-17 16:42:08 -08:00 · 2022-02-17 16:42:08 -08:00 · eea0374fad
commit eea0374fad
parent a08f52a6d2 e541e19f44
31 changed files with 576 additions and 149 deletions
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@ -9,12 +9,14 @@ on:
      - 'papers/**'
      - 'rfcs/**'
      - '*.md'
+      - 'prototyping/**'
  pull_request:
    paths-ignore:
      - 'docs/**'
      - 'papers/**'
      - 'rfcs/**'
      - '*.md'
+      - 'prototyping/**'

 jobs:
  unix:
--- a/.github/workflows/prototyping.yml
+++ b/.github/workflows/prototyping.yml
@ -4,15 +4,22 @@ on:
  push:
    branches:
      - 'master'
+      - 'prototyping-*'
    paths:
      - '.github/workflows/**'
      - 'prototyping/**'
-      - 'Analysis/src/JsonEncoder.cpp'
+      - 'Analysis/**'
+      - 'Ast/**'
+      - 'CLI/Ast.cpp'
+      - 'CLI/FileUtils.*'
  pull_request:
    paths:
      - '.github/workflows/**'
      - 'prototyping/**'
-      - 'Analysis/src/JsonEncoder.cpp'
+      - 'Analysis/**'
+      - 'Ast/**'
+      - 'CLI/Ast.cpp'
+      - 'CLI/FileUtils.*'

 jobs:
  linux:
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@ -9,6 +9,7 @@ on:
      - 'papers/**'
      - 'rfcs/**'
      - '*.md'
+      - 'prototyping/**'

 jobs:
  build:
--- a/Analysis/src/JsonEncoder.cpp
+++ b/Analysis/src/JsonEncoder.cpp
@ -150,6 +150,10 @@ struct AstJsonEncoder : public AstVisitor
    {
        writeRaw(std::to_string(i));
    }
+    void write(std::nullptr_t)
+    {
+        writeRaw("null");
+    }
    void write(std::string_view str)
    {
        writeString(str);
@ -177,7 +181,16 @@ struct AstJsonEncoder : public AstVisitor

    void write(AstLocal* local)
    {
-        write(local->name);
+        writeRaw("{");
+        bool c = pushComma();
+        if (local->annotation != nullptr)
+            write("type", local->annotation);
+        else
+            write("type", nullptr);
+        write("name", local->name);
+        write("location", local->location);
+        popComma(c);
+        writeRaw("}");
    }

    void writeNode(AstNode* node)
--- a/prototyping/Examples.agda
+++ b/prototyping/Examples.agda
@ -4,4 +4,4 @@ module Examples where
 import Examples.Syntax
 import Examples.OpSem
 import Examples.Run
-
+import Examples.Type
--- a/prototyping/Examples/OpSem.agda
+++ b/prototyping/Examples/OpSem.agda
@ -1,11 +1,9 @@
 module Examples.OpSem where

 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
-open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return)
-open import Luau.Heap using (emp)
+open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end)
+open import Luau.Heap using (∅)

-x = var "x"
-
-ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
+ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
 ex1 = subst

--- a/prototyping/Examples/Run.agda
+++ b/prototyping/Examples/Run.agda
@ -3,16 +3,13 @@
 module Examples.Run where

 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_⟨_⟩_end; return; _∙_; done)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
 open import Luau.Value using (nil)
 open import Luau.Run using (run; return)
-open import Luau.Heap using (emp; lookup-next; next-emp; lookup-next-emp)
+open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)

 import Agda.Builtin.Equality.Rewrite
 {-# REWRITE lookup-next next-emp lookup-next-emp #-}

-x = var "x"
-id = var "id"
-
-ex1 : (run (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
+ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
 ex1 = refl
--- a/prototyping/Examples/SmokeTest.lua
+++ b/prototyping/Examples/SmokeTest.lua
@ -10,4 +10,9 @@ local function comp(f)
 end
 local id2 = comp(id)(id)
 local nil2 = id2(nil)
+local a : any = nil
+local b : nil = nil
+local c : (nil) -> nil = nil
+local d : (any & nil) = nil
+local e : any? = nil
 return id2(nil2)
--- a/prototyping/Examples/SmokeTestOutput.lua
+++ b/prototyping/Examples/SmokeTestOutput.lua
@ -8,5 +8,11 @@ local function comp(f)
    end
  end
 end
-local id2 = id(id)
+local id2 = comp(id)(id)
 local nil2 = id2(nil)
+local a : any = nil
+local b : nil = nil
+local c : (nil) -> nil = nil
+local d : (any & nil) = nil
+local e : any? = nil
+return id2(nil2)
--- a/prototyping/Examples/Syntax.agda
+++ b/prototyping/Examples/Syntax.agda
@ -2,21 +2,21 @@ module Examples.Syntax where

 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.String using (_++_)
-open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
+open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
 open import Luau.Syntax.ToString using (exprToString; blockToString)

-f = var "f"
-x = var "x"
-
-ex1 : exprToString(f $ x) ≡
-  "f(x)"
+ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
+  "function(x)\n" ++
+  "  return f(x)\n" ++
+  "end"
 ex1 = refl

-ex2 : blockToString(return nil ∙ done) ≡
-  "return nil"
+ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡
+  "local x = nil\n" ++
+  "return x"
 ex2 = refl

-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
+ex3 : blockToString(function "f" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "f") ∙ done) ≡
  "local function f(x)\n" ++
  "  return x\n" ++
  "end\n" ++
--- a/prototyping/Examples/Type.agda
+++ b/prototyping/Examples/Type.agda
@ -0,0 +1,27 @@
+module Examples.Type where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.String using (_++_)
+open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
+open import Luau.Type.ToString using (typeToString)
+
+ex1 : typeToString(nil) ≡ "nil"
+ex1 = refl
+
+ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
+ex2 = refl
+
+ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
+ex3 = refl
+
+ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
+ex4 = refl
+
+ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
+ex5 = refl
+
+ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)"
+ex6 = refl
+
+ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
+ex7 = refl
--- a/prototyping/Interpreter.agda
+++ b/prototyping/Interpreter.agda
@ -18,7 +18,7 @@ open import Luau.Run using (run; return; done; error)
 open import Luau.RuntimeError.ToString using (errToStringᴮ)
 open import Luau.Value.ToString using (valueToString)

-runBlock : Block → IO ⊤
+runBlock : ∀ {a} → Block a → IO ⊤
 runBlock block with run block
 runBlock block | return V D = putStrLn (valueToString V)
 runBlock block | done D = putStrLn "nil"
--- a/prototyping/Luau/Heap.agda
+++ b/prototyping/Luau/Heap.agda
@ -5,39 +5,40 @@ open import FFI.Data.Maybe using (Maybe; just)
 open import FFI.Data.Vector using (Vector; length; snoc; empty)
 open import Luau.Addr using (Addr)
 open import Luau.Var using (Var)
-open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)

-data HeapValue : Set where
-  function_⟨_⟩_end : Var → Var → Block → HeapValue
+data HeapValue (a : Annotated) : Set where
+  function_is_end : FunDec a → Block a → HeapValue a

-Heap = Vector HeapValue
+Heap : Annotated → Set
+Heap a = Vector (HeapValue a)

-data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where
+data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where

  defn : ∀ {H val} →

    -----------------------------------
    (snoc H val) ≡ H ⊕ (length H) ↦ val

-lookup : Heap → Addr → Maybe HeapValue
-lookup = FFI.Data.Vector.lookup
+_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a)
+_[_] = FFI.Data.Vector.lookup

-emp : Heap
-emp = empty
+∅ : ∀ {a} → Heap a
+∅ = empty

-data AllocResult (H : Heap) (V : HeapValue) : Set where
-  ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
+data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
+  ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V

-alloc : ∀ H V → AllocResult H V
+alloc : ∀ {a} H V → AllocResult a H V
 alloc H V = ok (length H) (snoc H V) defn

-next : Heap → Addr
+next : ∀ {a} → Heap a → Addr
 next = length

-allocated : Heap → HeapValue → Heap
+allocated : ∀ {a} → Heap a → HeapValue a → Heap a
 allocated = snoc

-- next-emp : (length empty ≡ 0)
+-- next-emp : (length ∅ ≡ 0)
 next-emp = FFI.Data.Vector.length-empty

 -- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@ -2,13 +2,13 @@ module Luau.OpSem where

 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just)
-open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function_⟨_⟩_end)
+open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg)
 open import Luau.Value using (addr; val)

-data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
-data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
+data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
+data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set

 data _⊢_⟶ᴱ_⊣_  where

@ -17,11 +17,11 @@ data _⊢_⟶ᴱ_⊣_  where
    -------------------
    H ⊢ nil ⟶ᴱ nil ⊣ H

-  function : ∀ {H H′ a x B} →
+  function : ∀ {H H′ a F B} →

-    H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
+    H′ ≡ H ⊕ a ↦ (function F is B end) →
    -------------------------------------------
-    H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
+    H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′

  app : ∀ {H H′ M M′ N} →
  
@ -29,11 +29,11 @@ data _⊢_⟶ᴱ_⊣_  where
    -----------------------------
    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′

-  beta : ∀ {H M a f x B} →
+  beta : ∀ {H M a F B} →
  
-    (lookup H a) ≡ just(function f ⟨ x ⟩ B end) →
+    H [ a ] ≡ just(function F is B end) →
    -----------------------------------------------------
-    H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H
+    H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H

  block : ∀ {H H′ B B′ b} →
 
@ -61,14 +61,14 @@ data _⊢_⟶ᴮ_⊣_  where

  subst : ∀ {H x v B} →
  
-    -------------------------------------------------
-    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
+    ------------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H

-  function : ∀ {H H′ a f x B C} →
+  function : ∀ {H H′ a F B C} →
  
-    H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
+    H′ ≡ H ⊕ a ↦ (function F is C end) →
    --------------------------------------------------------------
-    H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
+    H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′

  return : ∀ {H H′ M M′ B} →
  
@ -76,7 +76,7 @@ data _⊢_⟶ᴮ_⊣_  where
    --------------------------------------------
    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′

-data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → Set where
+data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where

  refl : ∀ {H B} →

--- a/prototyping/Luau/Run.agda
+++ b/prototyping/Luau/Run.agda
@ -1,20 +1,20 @@
 module Luau.Run where

 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Heap using (Heap; emp)
+open import Luau.Heap using (Heap; ∅)
 open import Luau.Syntax using (Block; return; _∙_; done)
 open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
 open import Luau.Value using (val)
 open import Properties.Step using (stepᴮ; step; return; done; error)
 open import Luau.RuntimeError using (RuntimeErrorᴮ)

-data RunResult (H : Heap) (B : Block) : Set where
+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′ : ∀ H B → RunResult H B
+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′)
@ -24,5 +24,5 @@ run′ H _ | return V refl = return V refl
 run′ H _ | done refl = done refl
 run′ H B | error E = error E refl

-run : ∀ B → RunResult emp B
-run = run′ emp
+run : ∀ {a} B → RunResult {a} ∅ B
+run = run′ ∅
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@ -1,17 +1,17 @@
 module Luau.RuntimeError where

 open import Agda.Builtin.Equality using (_≡_)
-open import Luau.Heap using (Heap; lookup)
+open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)

-data RuntimeErrorᴮ (H : Heap) : Block → Set
-data RuntimeErrorᴱ (H : Heap) : Expr → Set
+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)
  UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
-  SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
+  SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
  app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
  block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)

--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@ -4,9 +4,10 @@ open import FFI.Data.String using (String; _++_)
 open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Var.ToString using (varToString)
+open import Luau.Syntax using (name)

-errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
-errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String
+errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
+errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String

 errToStringᴱ NilIsNotAFunction = "nil is not a function"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
@ -14,5 +15,5 @@ errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app E) = errToStringᴱ E
 errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b

-errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString x 
+errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"
--- a/prototyping/Luau/Substitution.agda
+++ b/prototyping/Luau/Substitution.agda
@ -1,24 +1,24 @@
 module Luau.Substitution where

-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)

-_[_/_]ᴱ : Expr → Value → Var → Expr
-_[_/_]ᴮ : Block → Value → Var → Block
-var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr
-_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block
+_[_/_]ᴱ : ∀ {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

 nil [ v / x ]ᴱ = nil
 var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
 addr a [ v / x ]ᴱ = addr a
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
-function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ y) end
+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

-(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
-(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y))
+(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 ≡ⱽ 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

--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@ -1,27 +1,55 @@
 module Luau.Syntax where

+open import Agda.Builtin.Equality using (_≡_)
+open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
+open import Luau.Type using (Type)

 infixr 5 _∙_

-data Block : Set
-data Stat : Set
-data Expr : Set
+data Annotated : Set where
+  maybe : Annotated
+  yes : Annotated

-data Block where
-  _∙_ : Stat → Block → Block
-  done : Block
+data VarDec : Annotated → Set where
+  var : Var → VarDec maybe
+  var_∈_ : ∀ {a} → Var → Type → VarDec a

-data Stat where
-  function_⟨_⟩_end : Var → Var → Block → Stat
-  local_←_ : Var → Expr → Stat
-  return : Expr → Stat
+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 → Var
+fun (f ⟨ x ⟩∈ T) = f
+fun (f ⟨ x ⟩) = f
+
+arg : ∀ {a} → FunDec a → VarDec a
+arg (f ⟨ x ⟩∈ T) = x
+arg (f ⟨ x ⟩) = x
+
+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
+  nil : Expr a
+  var : Var → Expr a
+  addr : Addr → Expr a
+  _$_ : Expr a → Expr a → Expr a
+  function_is_end : FunDec a → Block a → Expr a
+  block_is_end : Var → Block a → Expr a

-data Expr where
-  nil : Expr
-  var : Var → Expr
-  addr : Addr → Expr
-  _$_ : Expr → Expr → Expr
-  function⟨_⟩_end : Var → Block → Expr
-  block_is_end : Var → Block → Expr
--- a/prototyping/Luau/Syntax/FromJSON.agda
+++ b/prototyping/Luau/Syntax/FromJSON.agda
@ -1,6 +1,7 @@
 module Luau.Syntax.FromJSON where

-open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec)
+open import Luau.Type.FromJSON using (typeFromJSON)

 open import Agda.Builtin.List using (List; _∷_; [])

@ -31,12 +32,26 @@ 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)

-exprFromJSON : Value → Either String Expr
-exprFromObject : Object → Either String Expr
-statFromJSON : Value → Either String Stat
-statFromObject : Object → Either String Stat
-blockFromJSON : Value → Either String Block
-blockFromArray : Array → Either String Block
+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)
+
+varDecFromJSON (object arg) = varDecFromObject arg
+varDecFromJSON val = 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 val = Left "AstExpr not an object"
@ -54,17 +69,19 @@ exprFromObject obj | just (string "AstExprCall") | nothing | _  = Left ("AstExpr
 exprFromObject obj | just (string "AstExprCall") | _ | nothing  = Left ("AstExprCall missing args")
 exprFromObject obj | just (string "AstExprConstantNil") = Right nil
 exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value with head arr | blockFromJSON value
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function⟨ x ⟩ B end)
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just _ | Right B = Left "AstExprFunction args not a string array"
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | nothing | Right B = Left "Unsupported AstExprFunction empty args"
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue with head arr | blockFromJSON blockValue
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args"
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | Left err = Left err
 exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
 exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
 exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
 exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
-exprFromObject obj | just (string "AstExprLocal") | just (string x) = Right (var x)
-exprFromObject obj | just (string "AstExprLocal") | just (_) = Left "AstExprLocal local not a string"
+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 ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
@ -77,22 +94,22 @@ 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(string x) | just(value) with exprFromJSON(value)
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local x ← M)
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Left err = Left err
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | nothing = Left "AstStatLocal empty values"
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(_) | _ = Left "AstStatLocal vars not a string array"
+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 (string f) | just value with exprFromJSON value
-statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function⟨ x ⟩ B end) = Right (function f ⟨ x ⟩ B end)
-statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Left err = Left err
-statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
-statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ =  Left "AstStatLocalFunction name is not a string"
+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 | 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
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@ -1,13 +1,24 @@
 module Luau.Syntax.ToString where

-open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
 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)

-exprToString′ : String → Expr → String
-statToString′ : String → Stat → String
-blockToString′ : String → Block → String
+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 ++ ")"
+
+exprToString′ : ∀ {a} → String → Expr a → String
+statToString′ : ∀ {a} → String → Stat a → String
+blockToString′ : ∀ {a} → String → Block a → String

 exprToString′ lb nil =
  "nil"
@ -17,21 +28,21 @@ exprToString′ lb (var x) =
  varToString(x)
 exprToString′ lb (M $ N) =
  (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
-exprToString′ lb (function⟨ x ⟩ B end) =
-  "function(" ++ x ++ ")" ++ lb ++
+exprToString′ lb (function F is B end) =
+  funDecToString F ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
 exprToString′ lb (block b is B end) =
-  "(function " ++ b ++ "()" ++ lb ++
+  "(" ++ b ++ "()" ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end)()"

-statToString′ lb (function f ⟨ x ⟩ B end) =
-  "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
+statToString′ lb (function F is B end) =
+  "local " ++ funDecToString F ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
 statToString′ lb (local x ← M) =
-  "local " ++ x ++ " = " ++ (exprToString′ lb M)
+  "local " ++ varDecToString x ++ " = " ++ (exprToString′ lb M)
 statToString′ lb (return M) =
  "return " ++ (exprToString′ lb M)

@ -39,11 +50,11 @@ blockToString′ lb (S ∙ done) = statToString′ lb S
 blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
 blockToString′ lb (done) = ""

-exprToString : Expr → String
+exprToString : ∀ {a} → Expr a → String
 exprToString = exprToString′ "\n"

-statToString : Stat → String
+statToString : ∀ {a} → Stat a → String
 statToString = statToString′ "\n"

-blockToString : Block → String
+blockToString : ∀ {a} → Block a → String
 blockToString = blockToString′ "\n"
--- a/prototyping/Luau/Type.agda
+++ b/prototyping/Luau/Type.agda
@ -1,5 +1,7 @@
 module Luau.Type where

+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
 data Type : Set where
  nil : Type
  _⇒_ : Type → Type → Type
@ -8,3 +10,34 @@ data Type : Set where
  _∪_ : Type → Type → Type
  _∩_ : Type → Type → Type

+src : Type → Type
+src nil = none
+src (S ⇒ T) = S
+src none = none
+src any = any
+src (S ∪ T) = (src S) ∪ (src T)
+src (S ∩ T) = (src S) ∩ (src T)
+
+tgt : Type → Type
+tgt nil = none
+tgt (S ⇒ T) = T
+tgt none = none
+tgt any = any
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+
+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/Luau/Type/FromJSON.agda
+++ b/prototyping/Luau/Type/FromJSON.agda
@ -0,0 +1,66 @@
+module Luau.Type.FromJSON where
+
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any)
+
+open import Agda.Builtin.List using (List; _∷_; [])
+
+open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
+open import FFI.Data.Bool using (true; false)
+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 any
+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/Luau/Type/ToString.agda
+++ b/prototyping/Luau/Type/ToString.agda
@ -0,0 +1,26 @@
+module Luau.Type.ToString where
+
+open import FFI.Data.String using (String; _++_)
+open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
+
+{-# TERMINATING #-}
+typeToString : Type → String
+typeToStringᵁ : Type → String
+typeToStringᴵ : Type → String
+
+typeToString nil = "nil"
+typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
+typeToString none = "none"
+typeToString any = "any"
+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/Luau/Value.agda
+++ b/prototyping/Luau/Value.agda
@ -1,14 +1,14 @@
 module Luau.Value where

 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; nil; addr)
 open import Luau.Var using (Var)

 data Value : Set where
  nil : Value
  addr : Addr → Value

-val : Value → Expr
+val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a

--- a/prototyping/PrettyPrinter.agda
+++ b/prototyping/PrettyPrinter.agda
@ -15,7 +15,7 @@ open import Luau.Syntax using (Block)
 open import Luau.Syntax.FromJSON using (blockFromJSON)
 open import Luau.Syntax.ToString using (blockToString)

-runBlock : Block → IO ⊤
+runBlock : ∀ {a} → Block a → IO ⊤
 runBlock block = putStrLn (blockToString block)

 runJSON : Value → IO ⊤
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@ -1,3 +1,5 @@
 module Properties where

 import Properties.Dec
+import Properties.Step
+import Properties.Remember
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@ -2,16 +2,16 @@ module Properties.Step where

 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Heap using (Heap; lookup; alloc; ok; function_⟨_⟩_end)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
+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)
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
 open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val)
 open import Properties.Remember using (remember; _,_)

-data StepResultᴮ (H : Heap) (B : Block) : Set
-data StepResultᴱ (H : Heap) (M : Expr) : Set
+data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
+data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set

 data StepResultᴮ H B where
  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
@ -24,8 +24,8 @@ data StepResultᴱ H M where
  value : ∀ V → (M ≡ val V) → StepResultᴱ H M
  error : (RuntimeErrorᴱ H M) → StepResultᴱ H M

-stepᴱ : ∀ H M → StepResultᴱ H M
-stepᴮ : ∀ H B → StepResultᴮ H B
+stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
+stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B

 stepᴱ H nil = value nil refl
 stepᴱ H (var x) = error (UnboundVariable x)
@ -33,23 +33,23 @@ stepᴱ H (addr a) = value (addr a) 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 (addr a $ N) | value (addr a) refl with remember (lookup H a)
+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))
-stepᴱ H (addr a $ N) | value (addr a) refl | (just(function f ⟨ x ⟩ B end) , p) = step H (block f is local x ← N ∙ B end) (beta p)
+stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
 stepᴱ H (M $ N) | error E = error (app E)
-stepᴱ H (function⟨ x ⟩ B end) with alloc H (function "anon" ⟨ x ⟩ B end)
-stepᴱ H (function⟨ x ⟩ B end) | ok a H′ p = step H′ (addr a) (function p)
 stepᴱ H (block b is B end) with stepᴮ H B
 stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
 stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
 stepᴱ H (block b is done end) | done refl = step H nil done
 stepᴱ H (block b is B end) | error E = error (block b E)
+stepᴱ H (function F is C end) with alloc H (function F is C end)
+stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)

-stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function f ⟨ x ⟩ C end)
-stepᴮ H (function f ⟨ x ⟩ C end ∙ B) | ok a H′ p = step H′ (B [ addr a / f ]ᴮ) (function p)
+stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
+stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
 stepᴮ H (local x ← M ∙ B) with stepᴱ H M
 stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
-stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / x ]ᴮ) subst
+stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
 stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
 stepᴮ H (return M ∙ B) with stepᴱ H M
 stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
--- a/rfcs/STATUS.md
+++ b/rfcs/STATUS.md
@ -0,0 +1,64 @@
+This document tracks unimplemented RFCs.
+
+## Deprecate getfenv/setfenv
+
+[RFC: Deprecate getfenv/setfenv](https://github.com/Roblox/luau/blob/master/rfcs/deprecate-getfenv-setfenv.md)
+
+**Status**: Needs implementation.
+
+**Notes**: Implementing this RFC triggers warnings across the board in the apps ecosystem, in particular in testing libraries. Pending code changes / decisions.
+
+## Read-only and write-only properties
+
+[RFC: Read-only properties](https://github.com/Roblox/luau/blob/master/rfcs/property-readonly.md) |
+[RFC: Write-only properties](https://github.com/Roblox/luau/blob/master/rfcs/property-writeonly.md)
+
+**Status**: Needs implementation
+
+## Sealed/unsealed typing changes
+
+[RFC: Sealed table subtyping](https://github.com/Roblox/luau/blob/master/rfcs/sealed-table-subtyping.md) |
+[RFC: Unsealed table literals](https://github.com/Roblox/luau/blob/master/rfcs/unsealed-table-literals.md) |
+[RFC: Only strip optional properties from unsealed tables during subtyping](https://github.com/Roblox/luau/blob/master/rfcs/unsealed-table-subtyping-strips-optional-properties.md)
+
+**Status**: Implemented but depends on new transaction log implementation that is not fully live yet.
+
+## Default type parameters
+
+[RFC: Default type alias type parameters](https://github.com/Roblox/luau/blob/master/rfcs/syntax-default-type-alias-type-parameters.md)
+
+**Status**: Implemented but not fully rolled out yet.
+
+## Singleton types
+
+[RFC: Singleton types](https://github.com/Roblox/luau/blob/master/rfcs/syntax-singleton-types.md)
+
+**Status**: Implemented but not fully rolled out yet.
+
+## Nil-forgiving operator
+
+[RFC: nil-forgiving postfix operator !](https://github.com/Roblox/luau/blob/master/rfcs/syntax-nil-forgiving-operator.md)
+
+**Status**: Needs implementation.
+
+**Notes**: Do we need to reevaluate the necessity given `assert` and improved refinements?
+
+## Safe navigation operator
+
+[RFC: Safe navigation postfix operator (?)](https://github.com/Roblox/luau/blob/master/rfcs/syntax-safe-navigation-operator.md)
+
+**Status**: Needs implementation.
+
+**Notes**: We have unresolved issues with interaction between this feature and Roblox instance hierarchy. This may affect the viability of this proposal.
+
+## String interpolation
+
+[RFC: String interpolation](https://github.com/Roblox/luau/blob/master/rfcs/syntax-string-interpolation.md)
+
+**Status**: Needs implementation
+
+## Generalized iteration
+
+[RFC: Generalized iteration](https://github.com/Roblox/luau/blob/master/rfcs/generalized-iteration.md)
+
+**Status**: Needs implementation
--- a/rfcs/generalized-iteration.md
+++ b/rfcs/generalized-iteration.md
@ -0,0 +1,122 @@
+# Generalized iteration
+
+## Summary
+
+Introduce support for iterating over tables without using `pairs`/`ipairs` as well as a generic customization point for iteration via `__iter` metamethod.
+
+## Motivation
+
+Today there are many different ways to iterate through various containers that are syntactically incompatible.
+
+To iterate over arrays, you need to use `ipairs`: `for i, v in ipairs(t) do`. The traversal goes over a sequence `1..k` of numeric keys until `t[k] == nil`, preserving order.
+
+To iterate over dictionaries, you need to use `pairs`: `for k, v in pairs(t) do`. The traversal goes over all keys, numeric and otherwise, but doesn't guarantee an order; when iterating over arrays this may happen to work but is not guaranteed to work, as it depends on how keys are distributed between array and hash portion.
+
+To iterate over custom objects, whether they are represented as tables (user-specified) or userdata (host-specified), you need to expose special iteration methods, for example `for k, v in obj:Iterator() do`.
+
+All of these rely on the standard Lua iteration protocol, but it's impossible to trigger them in a generic fashion. Additionally, you *must* use one of `pairs`/`ipairs`/`next` to iterate over tables, which is easy to forget - a naive `for k, v in tab do` doesn't work and produces a hard-to-understand error `attempt to call a table value`.
+
+This proposal solves all of these by providing a way to implement uniform iteration with self-iterating objects by allowing to iterate over objects and tables directly via convenient `for k, v in obj do` syntax, and specifies the default iteration behavior for tables, thus mostly rendering `pairs`/`ipairs` obsolete - making Luau easier to use and teach.
+
+## Design
+
+In Lua, `for vars in iter do` has the following semantics (otherwise known as the iteration protocol): `iter` is expanded into three variables, `gen`, `state` and `index` (using `nil` if `iter` evaluates to fewer than 3 results); after this the loop is converted to the following pseudocode:
+
+```lua
+while true do
+  vars... = gen(state, index)
+  index = vars... -- copy the first variable into the index
+  if index == nil then break end
+  
+  -- loop body goes here
+end
+```
+
+This is a general mechanism that can support iteration through many containers, especially if `gen` is allowed to mutate state. Importantly, the *first* returned variable (which is exposed to the user) is used to continue the process on the next iteration - this can be limiting because it may require `gen` or `state` to carry extra internal iteration data for efficiency. To work around this for table iteration to avoid repeated calls to `next`, Luau compiler produces a special instruction sequence that recognizes `pairs`/`ipairs` iterators and stores the iteration index separately.
+
+Thus, today the loop `for k, v in tab do` effectively executes `k, v = tab()` on the first iteration, which is why it yields `attempt to call a table value`. If the object defines `__call` metamethod then it can act as a self-iterating method, but this is not idiomatic, not efficient and not pure/clean.
+
+This proposal comes in two parts: general support for `__iter` metamethod and default implementation for tables without one. With both of these in place, there's going to be a single, idiomatic, general and performant way to iterate through the object of any type:
+
+```lua
+for k, v in obj do
+...
+end
+```
+
+### __iter
+
+To support self-iterating objects, we modify the iteration protocol as follows: instead of simply expanding the result of expression `iter` into three variables (`gen`, `state` and `index`), we check if the first result has an `__iter` metamethod (which can be the case if it's a table, userdata or another composite object (e.g. a record in the future). If it does, the metamethod is called with `gen` as the first argument, and the returned three values replace `gen`/`state`/`index`. This happens *before* the loop:
+
+```lua
+if getmetatable(gen) and getmetatable(gen).__iter then
+   gen, state, index = getmetatable(gen).__iter(gen)
+end
+```
+
+This check is comparatively trivial: usually `gen` is a function, and functions don't have metatables; as such we can simply check the type of `gen` and if it's a table/userdata, we can check if it has a metamethod `__iter`. Due to tag-method cache, this check is also very cheap if the metamethod is absent.
+
+This allows objects to provide a custom function that guides the iteration. Since the function is called once, it is easy to reuse other functions in the implementation, for example here's a node object that exposes iteration through its children:
+
+```lua
+local Node = {}
+Node.__index = Node
+
+function Node.new(children)
+  return setmetatable({ children = children }, Node)
+end
+
+function Node:__iter()
+  return next, self.children
+end
+```
+
+Luau compiler already emits a bytecode instruction, FORGPREP*, to perform initial loop setup - this is where we can evaluate `__iter` as well.
+
+Naturally, this means that if the table has `__iter` metamethod and you need to iterate through the table fields instead of using the provided metamethod, you can't rely on the general iteration scheme and need to use `pairs`. This is similar to other parts of the language, like `t[k]` vs `rawget(t, 'k')`, where the default behavior is overrideable but a library function can help peek behind the curtain.
+
+### Default table iteration
+
+If the argument is a table and it does not implement `__iter` metamethod, we treat this as an attempt to iterate through the table using the builtin iteration order.
+
+> Note: we also check if the table implements `__call`; if it does, we fall back to the default handling. We may be able to remove this check in the future, but we will need this initially to preserve backwards compatibility with custom table-driven iterator objects that implement `__call`. In either case, we will be able to collect detailed analytics about the use of `__call` in iteration, and if neither is present we can emit a specialized error message such as `object X is not iteratable`.
+
+To have a single, unified, iteration scheme over tables regardless of whether they are arrays or dictionaries, we establish the following semantics:
+
+- First, the traversal goes over numeric keys in range `1..k` up until reaching the first `k` such that `t[k] == nil`
+- Then, the traversal goes over the remaining keys (with non-nil values), numeric and otherwise, in unspecified order.
+
+For arrays with gaps, this iterates until the first gap in order, and the remaining order is not specified.
+
+> Note: This behavior is similar to what `pairs` happens to provide today, but `pairs` doesn't give any guarantees, and it doesn't always provide this behavior in practice.
+
+To ensure that this traversal is performant, the actual implementation of the traversal involves going over the array part (in index order) and then over the hash part (in hash order). For that implementation to satisfy the criteria above, we need to make two additional changes to table insertion/rehash:
+
+- When inserting key `k` in the table when `k == t->sizearray + 1`, we force the table to rehash (resize its array portion). Today this is only performed if the hash portion is full, as such sometimes numeric keys can end up in the hash part.
+- When rehashing the table, we ensure that the hash part doesn't contain the key `newsizearray + 1`. This requires checking if the table has this key, which may require an additional hash lookup but we only need to do this in rare cases based on the analysis of power-of-two key buckets that we already collect during rehash.
+
+These changes guarantee that the order observed via standard traversal with `next`/`pairs` matches the guarantee above, which is nice because it means we can minimize the complexity cost of this change by reusing the traversal code, including VM optimizations. They also mean that the array boundary (aka `#t`) can *always* be computed from just the array portion, which simplifies the table length computation and may slightly speed it up.
+
+## Drawbacks
+
+This makes `for` desugaring and implementation a little more complicated; it's not a large complexity factor in Luau because we already have special handling for `for` loops in the VM, but it's something to keep in mind.
+
+While the proposed iteration scheme should be a superset to both `pairs` and `ipairs` for tables, for arrays `ipairs` may in some cases be faster because it stops at the first `nil`, whereas the proposed new scheme (like `pairs`) needs to iterate through the rest of the table's array storage. This may be fixable in the future, if we replace our cached table length (`aboundary`) with Lua 5.4's `alimit`, which maintains the invariant that all values after `alimit` in the array are `nil`. This would make default table iteration maximally performant as well as help us accelerate GC in some cases, but will require extra checks during table assignments which is a cost we may not be willing to pay. Thus it is theoretically possible that we will end up with `ipairs` being a slightly faster equivalent for array iteration forever.
+
+The resulting iteration behavior, while powerful, increases the divergence between Luau and Lua, making more programs that are written for Luau not runnable in Lua. Luau language in general does not consider this type of compatibility essential, but this is noted for posterity.
+
+The changes in insertion behavior that facilitate single iteration order may have a small cost; that said, they are currently understood to belong to paths that are already slow and the added cost is minimal.
+
+The extra semantics will make inferring the types of the variables in a for loop more difficult - if we know the type of the expression that is being iterated through it probably is not a problem though.
+
+## Alternatives
+
+Other major designs have been considered.
+
+A minor variation of the proposal involves having `__iter` be called on every iteration instead of at loop startup, effectively having `__iter` work as an alternative to `__call`. The issue with this variant is that while it's a little simpler to specify and implement, it restricts the options when implementing custom iteratable objects, because it would be difficult for iteratable objects to store custom iteration state elsewhere since `__iter` method would effectively need to be pure, as it can't modify the object itself as more than one concurrent iteration needs to be supported.
+
+A major variation of the proposal involves instead supporting `__pairs` from Lua 5.2. The issue with this variant is that it still requires the use of a library method, `pairs`, to work, which doesn't make the language simpler as far as table iteration, which is the 95% case, is concerned. Additionally, with some rare exceptions metamethods today extend the *language* behavior, not the *library* behavior, and extending extra library functions with metamethods does not seem true to the core of the language. Finally, this only works if the user uses `pairs` to iterate and doesn't work with `ipairs`/`next`.
+
+Another variation involves using a new pseudo-keyword, `foreach`, instead of overloading existing `for`, and only using the new `__iter` semantics there. This can more cleanly separate behavior, requiring the object to have an `__iter` metamethod (or be a table) in `foreach` - which also avoids having to deal with `__call` - but it also requires teaching the users a new keyword which fragments the iteration space a little bit more. Compared to that, the main proposal doesn't introduce new divergent syntax, and merely tweaks existing behavior to be more general, thus making an existing construct easier to use.
+
+Finally, the author also considered and rejected extending the iteration protocol as part of this change. One problem with the current protocol is that the iterator requires an allocation (per loop execution) to keep extra state that isn't exposed to the user. The builtin iterators like `pairs`/`ipairs` work around this by feeding the user-visible index back to the search function, but that's not always practical. That said, having a different iteration protocol in effect only when `__iter` is used makes the language more complicated for unclear efficiency gains, thus this design doesn't suggest a new core protocol to favor simplicity.
--- a/tests/JsonEncoder.test.cpp
+++ b/tests/JsonEncoder.test.cpp
@ -46,7 +46,7 @@ TEST_CASE("encode_AstStatBlock")
    AstStatBlock block{Location(), bodyArray};

    CHECK_EQ(
-        (R"({"type":"AstStatBlock","location":"0,0 - 0,0","body":[{"type":"AstStatLocal","location":"0,0 - 0,0","vars":["a_local"],"values":[]}]})"),
+        (R"({"type":"AstStatBlock","location":"0,0 - 0,0","body":[{"type":"AstStatLocal","location":"0,0 - 0,0","vars":[{"type":null,"name":"a_local","location":"0,0 - 0,0"}],"values":[]}]})"),
        toJson(&block));
 }