Implement a prototype interpreter (#353)

* First cut interpreter

.github/workflows/prototyping.yml

@@ -7,10 +7,12 @@ on:
     paths:
       - '.github/workflows/**'
       - 'prototyping/**'
+      - 'Analysis/src/JsonEncoder.cpp'
   pull_request:
     paths:
       - '.github/workflows/**'
       - 'prototyping/**'
+      - 'Analysis/src/JsonEncoder.cpp'
 
 jobs:
   linux:
@@ -40,16 +42,20 @@ jobs:
     - name: check examples
       working-directory: prototyping
       run: ~/.cabal/bin/agda Examples.agda
-    - name: build PrettyPrinter
+    - name: build executables
       working-directory: prototyping
-      run: ~/.cabal/bin/agda --compile --ghc-flag=-v PrettyPrinter.agda
+      run: |
+        ~/.cabal/bin/agda --compile PrettyPrinter.agda
+        ~/.cabal/bin/agda --compile Interpreter.agda
     - name: cmake configure
       run: cmake .
     - name: cmake build luau-ast
       run: cmake --build . --target Luau.Ast.CLI
     - name: run smoketest
       working-directory: prototyping
-      run: ../luau-ast Examples/SmokeTest.lua | ./PrettyPrinter > Examples/SmokeTestOutput.lua
+      run: |
+        ../luau-ast Examples/SmokeTest.lua | ./PrettyPrinter > Examples/SmokeTestOutput.lua
+        ../luau-ast Examples/SmokeTest.lua | ./Interpreter
     - name: diff smoketest
       working-directory: prototyping
       run: diff Examples/SmokeTest.lua Examples/SmokeTestOutput.lua

prototyping/Examples.agda

@@ -1,4 +1,7 @@
+{-# OPTIONS --rewriting #-}
 module Examples where
 
 import Examples.Syntax
+import Examples.OpSem
+import Examples.Run
 

prototyping/Examples/OpSem.agda

@@ -0,0 +1,11 @@
+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)
+
+x = var "x"
+
+ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
+ex1 = subst
+

prototyping/Examples/Run.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --rewriting #-}
+
+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.Value using (nil)
+open import Luau.Run using (run; return)
+open import Luau.Heap using (emp; 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 = refl

prototyping/Examples/SmokeTest.lua

@@ -8,5 +8,6 @@ local function comp(f)
     end
   end
 end
-local id2 = id(id)
+local id2 = comp(id)(id)
 local nil2 = id2(nil)
+return id2(nil2)

prototyping/Examples/SmokeTestOutput.lua

@@ -0,0 +1,12 @@
+local function id(x)
+  return x
+end
+local function comp(f)
+  return function(g)
+    return function(x)
+      return f(g(x))
+    end
+  end
+end
+local id2 = id(id)
+local nil2 = id2(nil)

prototyping/Examples/Syntax.agda

@@ -2,7 +2,7 @@ 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; _∙; _∙_)
+open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
 f = var "f"
@@ -12,11 +12,11 @@ ex1 : exprToString(f $ x) ≡
   "f(x)"
 ex1 = refl
 
-ex2 : blockToString(return nil ∙) ≡
+ex2 : blockToString(return nil ∙ done) ≡
   "return nil"
 ex2 = refl
 
-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
   "local function f(x)\n" ++
   "  return x\n" ++
   "end\n" ++

prototyping/FFI/Data/HaskellInt.agda

@@ -0,0 +1,14 @@
+module FFI.Data.HaskellInt where
+
+open import Agda.Builtin.Int using (Int)
+
+{-# FOREIGN GHC import qualified Data.Int #-}
+
+postulate HaskellInt : Set
+{-# COMPILE GHC HaskellInt = type Data.Int.Int #-}
+
+postulate
+  intToHaskellInt : Int → HaskellInt
+  haskellIntToInt : HaskellInt → Int
+{-# COMPILE GHC intToHaskellInt = fromIntegral #-}
+{-# COMPILE GHC haskellIntToInt = fromIntegral #-}

prototyping/FFI/Data/Vector.agda

@@ -1,6 +1,10 @@
 module FFI.Data.Vector where
 
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Int using (Int; pos; negsuc)
+open import Agda.Builtin.Nat using (Nat)
 open import FFI.Data.Bool using (Bool; false; true)
+open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 
 {-# FOREIGN GHC import qualified Data.Vector #-}
@@ -14,10 +18,20 @@ postulate
   null : ∀ {A} → (Vector A) → Bool
   unsafeHead : ∀ {A} → (Vector A) → A
   unsafeTail : ∀ {A} → (Vector A) → (Vector A)
+  length : ∀ {A} → (Vector A) → Nat
+  lookup : ∀ {A} → (Vector A) → Nat → (Maybe A)
+  snoc : ∀ {A} → (Vector A) → A → (Vector A)
 {-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
 {-# COMPILE GHC null = \_ -> Data.Vector.null #-}
 {-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
 {-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
+{-# COMPILE GHC length = \_ -> (fromIntegral . Data.Vector.length) #-}
+{-# COMPILE GHC lookup = \_ v -> ((v Data.Vector.!?) . fromIntegral) #-}
+{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}
+
+postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0)
+postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x)
+postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x)
 
 head : ∀ {A} → (Vector A) → (Maybe A)
 head vec with null vec
@@ -28,4 +42,3 @@ tail : ∀ {A} → (Vector A) → Vector A
 tail vec with null vec
 tail vec | false = unsafeTail vec
 tail vec | true = empty
-

prototyping/Interpreter.agda

@@ -0,0 +1,39 @@
+module Interpreter where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Int using (pos)
+open import Agda.Builtin.Unit using (⊤)
+
+open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
+open import FFI.Data.Aeson using (Value; eitherDecode)
+open import FFI.Data.Either using (Left; Right)
+open import FFI.Data.String using (String; _++_)
+open import FFI.Data.Text.Encoding using (encodeUtf8)
+open import FFI.System.Exit using (exitWith; ExitFailure)
+
+open import Luau.Syntax using (Block)
+open import Luau.Syntax.FromJSON using (blockFromJSON)
+open import Luau.Syntax.ToString using (blockToString)
+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 block with run block
+runBlock block | return V D = putStrLn (valueToString V)
+runBlock block | done D = putStrLn "nil"
+runBlock block | error E D = putStrLn (errToStringᴮ E)
+
+runJSON : Value → IO ⊤
+runJSON value with blockFromJSON(value)
+runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
+runJSON value | (Right block) = runBlock block
+
+runString : String → IO ⊤
+runString txt with eitherDecode (encodeUtf8 txt)
+runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
+runString txt | (Right value) = runJSON value
+
+main : IO ⊤
+main = getContents >>= runString
+

prototyping/Luau/Addr.agda

@@ -0,0 +1,17 @@
+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; ⊥)
+
+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
+

prototyping/Luau/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))

prototyping/Luau/Heap.agda

@@ -0,0 +1,48 @@
+module Luau.Heap where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import FFI.Data.Maybe using (Maybe; just)
+open import FFI.Data.Vector using (Vector; length; snoc; empty)
+open import Luau.Addr using (Addr)
+open import Luau.Var using (Var)
+open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+
+data HeapValue : Set where
+  function_⟨_⟩_end : Var → Var → Block → HeapValue
+
+Heap = Vector HeapValue
+
+data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where
+
+  defn : ∀ {H val} →
+
+    -----------------------------------
+    (snoc H val) ≡ H ⊕ (length H) ↦ val
+
+lookup : Heap → Addr → Maybe HeapValue
+lookup = FFI.Data.Vector.lookup
+
+emp : Heap
+emp = empty
+
+data AllocResult (H : Heap) (V : HeapValue) : Set where
+  ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
+
+alloc : ∀ H V → AllocResult H V
+alloc H V = ok (length H) (snoc H V) defn
+
+next : Heap → Addr
+next = length
+
+allocated : Heap → HeapValue → Heap
+allocated = snoc
+
+-- next-emp : (length empty ≡ 0)
+next-emp = FFI.Data.Vector.length-empty
+
+-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
+lookup-next = FFI.Data.Vector.lookup-snoc
+
+-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
+lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty
+

prototyping/Luau/OpSem.agda

@@ -0,0 +1,92 @@
+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.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.Value using (addr; val)
+
+data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
+data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
+
+data _⊢_⟶ᴱ_⊣_  where
+
+  nil : ∀ {H} →
+
+    -------------------
+    H ⊢ nil ⟶ᴱ nil ⊣ H
+
+  function : ∀ {H H′ a x B} →
+
+    H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
+    -------------------------------------------
+    H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
+
+  app : ∀ {H H′ M M′ N} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    -----------------------------
+    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
+
+  beta : ∀ {H M a f x B} →
+  
+    (lookup H a) ≡ just(function f ⟨ x ⟩ B end) →
+    -----------------------------------------------------
+    H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B 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 : ∀ {H V B b} →
+ 
+    --------------------------------------------------------
+    H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H
+
+  done : ∀ {H b} →
+ 
+    ---------------------------------
+    H ⊢ (block b is done end) ⟶ᴱ nil ⊣ 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 : ∀ {H x v B} →
+  
+    -------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
+
+  function : ∀ {H H′ a f x B C} →
+  
+    H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
+    --------------------------------------------------------------
+    H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
+
+  return : ∀ {H H′ M M′ B} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    --------------------------------------------
+    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
+
+data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → 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″
+
+

prototyping/Luau/Run.agda

@@ -0,0 +1,28 @@
+module Luau.Run where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Luau.Heap using (Heap; emp)
+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
+  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′ 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 : ∀ B → RunResult emp B
+run = run′ emp

prototyping/Luau/RuntimeError.agda

@@ -0,0 +1,21 @@
+module Luau.RuntimeError where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Luau.Heap using (Heap; lookup)
+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; _∙_)
+
+data RuntimeErrorᴮ (H : Heap) : Block → Set
+data RuntimeErrorᴱ (H : Heap) : Expr → 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)
+  app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
+  block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
+
+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)
+

prototyping/Luau/RuntimeError/ToString.agda

@@ -0,0 +1,18 @@
+module Luau.RuntimeError.ToString where
+
+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)
+
+errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
+errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String
+
+errToStringᴱ NilIsNotAFunction = "nil is not a function"
+errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
+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ᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"

prototyping/Luau/Substitution.agda

@@ -0,0 +1,30 @@
+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.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
+
+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
+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))
+(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 ]ᴮ
+

prototyping/Luau/Syntax.agda

@@ -1,27 +1,17 @@
 module Luau.Syntax where
 
-open import Agda.Builtin.String using (String)
+open import Luau.Var using (Var)
+open import Luau.Addr using (Addr)
 
 infixr 5 _∙_
 
-data Type : Set where
-  nil : Type
-  _⇒_ : Type → Type → Type
-  none : Type
-  any : Type
-  _∪_ : Type → Type → Type
-  _∩_ : Type → Type → Type
-
-Var : Set
-Var = String
-
 data Block : Set
 data Stat : Set
 data Expr : Set
 
 data Block where
   _∙_ : Stat → Block → Block
-  _∙ : Stat → Block
+  done : Block
 
 data Stat where
   function_⟨_⟩_end : Var → Var → Block → Stat
@@ -31,5 +21,7 @@ data Stat where
 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

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; _∙; _∙_)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
@@ -117,11 +117,9 @@ 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 = Left "Block should be a non-empty array"
+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 null (tail arr)
-blockFromArray arr | just value | Right S | true = Right (S ∙)
-blockFromArray arr | just value | Right S | false with blockFromArray(tail arr)
-blockFromArray arr | just value | Right S | false | Left err = Left (err)
-blockFromArray arr | just value | Right S | false | Right B  = Right (S ∙ B)
+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)

prototyping/Luau/Syntax/ToString.agda

@@ -1,8 +1,9 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; _∙)
-
+open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
 open import FFI.Data.String using (String; _++_)
+open import Luau.Addr.ToString using (addrToString)
+open import Luau.Var.ToString using (varToString)
 
 exprToString′ : String → Expr → String
 statToString′ : String → Stat → String
@@ -10,14 +11,20 @@ blockToString′ : String → Block → String
 
 exprToString′ lb nil =
   "nil"
+exprToString′ lb (addr a) =
+  addrToString(a)
 exprToString′ lb (var x) =
-  x
+  varToString(x)
 exprToString′ lb (M $ N) =
   (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
 exprToString′ lb (function⟨ x ⟩ B end) =
   "function(" ++ x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
+exprToString′ lb (block b is B end) =
+  "(function " ++ b ++ "()" ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end)()"
 
 statToString′ lb (function f ⟨ x ⟩ B end) =
   "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
@@ -28,8 +35,9 @@ statToString′ lb (local x ← 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 (S ∙) = statToString′ lb S
+blockToString′ lb (done) = ""
 
 exprToString : Expr → String
 exprToString = exprToString′ "\n"

prototyping/Luau/Type.agda

@@ -0,0 +1,10 @@
+module Luau.Type where
+
+data Type : Set where
+  nil : Type
+  _⇒_ : Type → Type → Type
+  none : Type
+  any : Type
+  _∪_ : Type → Type → Type
+  _∩_ : Type → Type → Type
+

prototyping/Luau/Value.agda

@@ -0,0 +1,15 @@
+module Luau.Value where
+
+open import Luau.Addr using (Addr)
+open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+open import Luau.Var using (Var)
+
+data Value : Set where
+  nil : Value
+  addr : Addr → Value
+
+val : Value → Expr
+val nil = nil
+val (addr a) = addr a
+
+

prototyping/Luau/Value/ToString.agda

@@ -0,0 +1,10 @@
+module Luau.Value.ToString where
+
+open import Agda.Builtin.String using (String)
+open import Luau.Value using (Value; nil; addr)
+open import Luau.Addr.ToString using (addrToString)
+
+valueToString : Value → String
+valueToString nil = "nil"
+valueToString (addr a) = addrToString a
+ 

prototyping/Luau/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; ⊥)
+
+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
+

prototyping/Luau/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
+

prototyping/Properties.agda

@@ -0,0 +1,3 @@
+module Properties where
+
+import Properties.Dec

prototyping/Properties/Dec.agda

@@ -0,0 +1,8 @@
+module Properties.Dec where
+
+data ⊥ : Set where
+
+data Dec(A : Set) : Set where
+  yes : A → Dec A
+  no : (A → ⊥) → Dec A
+

prototyping/Properties/Remember.agda

@@ -0,0 +1,9 @@
+module Properties.Remember where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+
+data Remember {A : Set} (a : A) : Set where
+  _,_ : ∀ b → (a ≡ b) → Remember(a)
+  
+remember : ∀ {A} (a : A) → Remember(a)
+remember a = (a , refl)

prototyping/Properties/Step.agda

@@ -0,0 +1,58 @@
+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.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ᴮ H B where
+  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
+  return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B
+  done : (B ≡ done) → StepResultᴮ H B
+  error : (RuntimeErrorᴮ H B) → StepResultᴮ H B
+
+data StepResultᴱ H M where
+  step : ∀ H′ M′ → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → StepResultᴱ H M
+  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ᴱ H nil = value nil refl
+stepᴱ H (var x) = error (UnboundVariable x)
+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 | (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 (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 ⟨ 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 (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 ← 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)
+stepᴮ H (return _ ∙ B) | value V refl = return V refl
+stepᴮ H (return M ∙ B) | error E = error (return E)
+stepᴮ H done = done refl