Merge branch 'master' into merge

.github/workflows/prototyping.yml

@@ -0,0 +1,61 @@
+name: prototyping
+
+on:
+  push:
+    branches:
+      - 'master'
+    paths:
+      - '.github/workflows/**'
+      - 'prototyping/**'
+      - 'Analysis/src/JsonEncoder.cpp'
+  pull_request:
+    paths:
+      - '.github/workflows/**'
+      - 'prototyping/**'
+      - 'Analysis/src/JsonEncoder.cpp'
+
+jobs:
+  linux:
+    strategy:
+      matrix:
+        agda: [2.6.2.1]
+    name: prototyping
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v1
+    - uses: actions/cache@v2
+      with:
+        path: ~/.cabal/store
+        key: prototyping-${{ runner.os }}-${{ matrix.agda }}
+    - name: install cabal
+      run: sudo apt-get install -y cabal-install
+    - name: cabal update
+      working-directory: prototyping
+      run: cabal update
+    - name: cabal install
+      working-directory: prototyping
+      run: |
+        cabal install Agda-${{ matrix.agda }}
+        cabal install --lib scientific --package-env .
+        cabal install --lib vector --package-env .
+        cabal install --lib aeson --package-env .
+    - name: check examples
+      working-directory: prototyping
+      run: ~/.cabal/bin/agda Examples.agda
+    - name: build executables
+      working-directory: prototyping
+      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
+        ../luau-ast Examples/SmokeTest.lua | ./Interpreter
+    - name: diff smoketest
+      working-directory: prototyping
+      run: diff Examples/SmokeTest.lua Examples/SmokeTestOutput.lua

CLI/Ast.cpp

@@ -0,0 +1,84 @@
+// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details
+#include <optional>
+
+#include "Luau/Common.h"
+#include "Luau/Ast.h"
+#include "Luau/JsonEncoder.h"
+#include "Luau/Parser.h"
+#include "Luau/ParseOptions.h"
+
+#include "FileUtils.h"
+
+static void displayHelp(const char* argv0)
+{
+    printf("Usage: %s [file]\n", argv0);
+}
+
+static int assertionHandler(const char* expr, const char* file, int line, const char* function)
+{
+    printf("%s(%d): ASSERTION FAILED: %s\n", file, line, expr);
+    return 1;
+}
+
+int main(int argc, char** argv)
+{
+    Luau::assertHandler() = assertionHandler;
+
+    for (Luau::FValue<bool>* flag = Luau::FValue<bool>::list; flag; flag = flag->next)
+        if (strncmp(flag->name, "Luau", 4) == 0)
+            flag->value = true;
+
+    if (argc >= 2 && strcmp(argv[1], "--help") == 0)
+    {
+        displayHelp(argv[0]);
+        return 0;
+    }
+    else if (argc < 2)
+    {
+        displayHelp(argv[0]);
+        return 1;
+    }
+
+    const char* name = argv[1];
+    std::optional<std::string> maybeSource = std::nullopt;
+    if (strcmp(name, "-") == 0)
+    {
+        maybeSource = readStdin();
+    }
+    else
+    {
+        maybeSource = readFile(name);
+    }
+
+    if (!maybeSource)
+    {
+        fprintf(stderr, "Couldn't read source %s\n", name);
+        return 1;
+    }
+
+    std::string source = *maybeSource;
+
+    Luau::Allocator allocator;
+    Luau::AstNameTable names(allocator);
+
+    Luau::ParseOptions options;
+    options.supportContinueStatement = true;
+    options.allowTypeAnnotations = true;
+    options.allowDeclarationSyntax = true;
+
+    Luau::ParseResult parseResult = Luau::Parser::parse(source.data(), source.size(), names, allocator, options);
+
+    if (parseResult.errors.size() > 0)
+    {
+        fprintf(stderr, "Parse errors were encountered:\n");
+        for (const Luau::ParseError& error : parseResult.errors)
+        {
+            fprintf(stderr, "  %s - %s\n", toString(error.getLocation()).c_str(), error.getMessage().c_str());
+        }
+        fprintf(stderr, "\n");
+    }
+
+    printf("%s", Luau::toJson(parseResult.root).c_str());
+
+    return parseResult.errors.size() > 0 ? 1 : 0;
+}

CMakeLists.txt

@@ -5,13 +5,20 @@ if(EXT_PLATFORM_STRING)
 endif()
 
 cmake_minimum_required(VERSION 3.0)
-project(Luau LANGUAGES CXX C)
 
 option(LUAU_BUILD_CLI "Build CLI" ON)
 option(LUAU_BUILD_TESTS "Build tests" ON)
 option(LUAU_BUILD_WEB "Build Web module" OFF)
 option(LUAU_WERROR "Warnings as errors" OFF)
+option(LUAU_STATIC_CRT "Link with the static CRT (/MT)" OFF)
 
+if(LUAU_STATIC_CRT)
+    cmake_minimum_required(VERSION 3.15)
+    cmake_policy(SET CMP0091 NEW)
+    set(CMAKE_MSVC_RUNTIME_LIBRARY "MultiThreaded$<$<CONFIG:Debug>:Debug>")
+endif()
+
+project(Luau LANGUAGES CXX C)
 add_library(Luau.Ast STATIC)
 add_library(Luau.Compiler STATIC)
 add_library(Luau.Analysis STATIC)
@@ -21,10 +28,12 @@ add_library(isocline STATIC)
 if(LUAU_BUILD_CLI)
     add_executable(Luau.Repl.CLI)
     add_executable(Luau.Analyze.CLI)
+    add_executable(Luau.Ast.CLI)
 
     # This also adds target `name` on Linux/macOS and `name.exe` on Windows
     set_target_properties(Luau.Repl.CLI PROPERTIES OUTPUT_NAME luau)
     set_target_properties(Luau.Analyze.CLI PROPERTIES OUTPUT_NAME luau-analyze)
+    set_target_properties(Luau.Ast.CLI PROPERTIES OUTPUT_NAME luau-ast)
 endif()
 
 if(LUAU_BUILD_TESTS)
@@ -98,6 +107,7 @@ endif()
 if(LUAU_BUILD_CLI)
     target_compile_options(Luau.Repl.CLI PRIVATE ${LUAU_OPTIONS})
     target_compile_options(Luau.Analyze.CLI PRIVATE ${LUAU_OPTIONS})
+    target_compile_options(Luau.Ast.CLI PRIVATE ${LUAU_OPTIONS})
 
     target_include_directories(Luau.Repl.CLI PRIVATE extern extern/isocline/include)
 
@@ -111,6 +121,8 @@ if(LUAU_BUILD_CLI)
     endif()
 
     target_link_libraries(Luau.Analyze.CLI PRIVATE Luau.Analysis)
+
+    target_link_libraries(Luau.Ast.CLI PRIVATE Luau.Ast Luau.Analysis)
 endif()
 
 if(LUAU_BUILD_TESTS)

Sources.cmake

@@ -193,6 +193,13 @@ if(TARGET Luau.Analyze.CLI)
         CLI/Analyze.cpp)
 endif()
 
+if (TARGET Luau.Ast.CLI)
+    target_sources(Luau.Ast.CLI PRIVATE
+        CLI/FileUtils.h
+        CLI/FileUtils.cpp
+        CLI/Ast.cpp)
+endif()
+
 if(TARGET Luau.UnitTest)
     # Luau.UnitTest Sources
     target_sources(Luau.UnitTest PRIVATE

docs/_pages/library.md

@@ -128,7 +128,8 @@ Returns the type of the object, which is one of `"nil"`, `"boolean"`, `"number"`
 function typeof(obj: any): string
 ```
 
-Returns the type of the object; for userdata objects that have a metatable with the `__type` field, returns the value for that key.
+Returns the type of the object; for userdata objects that have a metatable with the `__type` field *and* are defined by the host with an internal tag, returns the value for that key.
+For custom userdata objects, such as ones returned by `newproxy`, this function returns `"userdata"` to make sure host-defined types can not be spoofed.
 
 ```
 function ipairs(t: table): <iterator>

docs/_pages/lint.md

@@ -294,6 +294,7 @@ table.insert(t, 0, 42) -- table.insert uses index 0 but arrays are 1-based; did
 
 table.insert(t, #t+1, 42) -- table.insert will append the value to the table; consider removing the second argument for efficiency
 ```
+
 ## DuplicateCondition (24)
 
 When checking multiple conditions via `and/or` or `if/elseif`, a copy & paste error may result in checking the same condition redundantly. This almost always indicates a bug, so a warning is emitted when use of a duplicate condition is detected.
@@ -301,3 +302,18 @@ When checking multiple conditions via `and/or` or `if/elseif`, a copy & paste er
 ```lua
 assert(self._adorns[normID1] and self._adorns[normID1]) -- Condition has already been checked on column 8
 ```
+
+## MisleadingAndOr (25)
+
+In Lua, there is no first-class ternary operator but it can be emulated via `a and b or c` pattern. However, due to how boolean evaluation works, if `b` is `false` or `nil`, the resulting expression evaluates to `c` regardless of the value of `a`. Luau solves this problem with the `if a then b else c` expression; a warning is emitted for and-or expressions where the first alternative is `false` or `nil` because it's almost always a bug.
+
+```lua
+-- The and-or expression always evaluates to the second alternative because the first alternative is false; consider using if-then-else expression instead
+local x = flag and false or true
+```
+
+The code above can be rewritten as follows to avoid the warning and the associated bug:
+
+```lua
+local x = if flag then false else true
+```

docs/_pages/performance.md

@@ -167,3 +167,11 @@ While Luau uses an incremental garbage collector, once per each collector cycle
 Normally objects that have been modified after the GC marked them in an incremental mark phase need to be rescanned during atomic phase, so frequent modifications of existing tables may result in a slow atomic step. To address this, we run a "remark" step where we traverse objects that have been modified after being marked once more (incrementally); additionally, the write barrier that triggers for object modifications changes the transition logic during remark phase to reduce the probability that the object will need to be rescanned.
 
 Another source of scalability challenges is coroutines. Writes to coroutine stacks don't use a write barrier, since that's prohibitively expensive as they are too frequent. This means that coroutine stacks need to be traversed during atomic step, so applications with many coroutines suffer large atomic pauses. To address this, we implement incremental marking of coroutines: marking a coroutine makes it "inactive" and resuming a coroutine (or pushing extra objects on the coroutine stack via C API) makes it "active". Atomic step only needs to traverse active coroutines again, which reduces the cost of atomic step by effectively making coroutine collection incremental as well.
+
+While large tables can be a problem for incremental GC in general since currently marking a single object is indivisible, large weak tables are a unique challenge because they also need to be processed during atomic phase, and the main use case for weak tables - object caches - may result in tables with large capacity but few live objects in long-running applications that exhibit bursts of activity. To address this, weak tables in Luau can be marked as "shrinkable" by including `s` as part of `__mode` string, which results in weak tables being resized to the optimal capacity during GC. This option may result in missing keys during table iteration if the table is resized while iteration is in progress and as such is only recommended for use in specific circumstances.
+
+## Optimized garbage collector sweeping
+
+The incremental garbage collector in Luau runs three phases for each cycle: mark, atomic and sweep. Mark incrementally traverses all live objects, atomic finishes various operations that need to happen without mutator intervention (see previous section), and sweep traverses all objects in the heap, reclaiming memory used by dead objects and performing minor fixup for live objects. While objects allocated during the mark phase are traversed in the same cycle and thus may get reclaimed, objects allocated during the sweep phase are considered live. Because of this, the faster the sweep phase completes, the less garbage will accumulate; and, of course, the less time sweeping takes the less overhead there is from this phase of garbage collection on the process.
+
+Since sweeping traverses the whole heap, we maximize the efficiency of this traversal by allocating garbage-collected objects of the same size in 16 KB pages, and traversing each page at a time, which is otherwise known as a paged sweeper. This ensures good locality of reference as consecutively swept objects are contiugous in memory, and allows us to spend no memory for each object on sweep-related data or allocation metadata, since paged sweeper doesn't need to be able to free objects without knowing which page they are in. Compared to linked list based sweeping that Lua/LuaJIT implement, paged sweeper is 2-3x faster, and saves 16 bytes per object on 64-bit platforms.

prototyping/.gitignore

@@ -0,0 +1,6 @@
+*~
+*.agdai
+Main
+MAlonzo
+PrettyPrinter
+.ghc.*

prototyping/Examples.agda

@@ -0,0 +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

@@ -0,0 +1,13 @@
+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 = 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

@@ -0,0 +1,24 @@
+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.ToString using (exprToString; blockToString)
+
+f = var "f"
+x = var "x"
+
+ex1 : exprToString(f $ x) ≡
+  "f(x)"
+ex1 = refl
+
+ex2 : blockToString(return nil ∙ done) ≡
+  "return nil"
+ex2 = refl
+
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
+  "local function f(x)\n" ++
+  "  return x\n" ++
+  "end\n" ++
+  "return f"
+ex3 = refl

prototyping/FFI/Data/Aeson.agda

@@ -0,0 +1,50 @@
+module FFI.Data.Aeson where
+
+open import Agda.Builtin.Bool using (Bool)
+open import Agda.Builtin.String using (String)
+
+open import FFI.Data.ByteString using (ByteString)
+open import FFI.Data.HaskellString using (HaskellString; pack)
+open import FFI.Data.Maybe using (Maybe)
+open import FFI.Data.Either using (Either; mapLeft)
+open import FFI.Data.Scientific using (Scientific)
+open import FFI.Data.Vector using (Vector)
+
+{-# FOREIGN GHC import qualified Data.Aeson #-}
+{-# FOREIGN GHC import qualified Data.Aeson.Key #-}
+{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}
+
+postulate
+  KeyMap : Set → Set
+  Key : Set
+  fromString : String → Key
+  toString : Key → String
+  lookup : ∀ {A} → Key -> KeyMap A -> Maybe A
+{-# POLARITY KeyMap ++ #-}
+{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
+{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
+{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
+{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
+{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}
+
+data Value : Set where
+  object : KeyMap Value → Value
+  array : Vector Value → Value
+  string : String → Value
+  number : Scientific → Value
+  bool : Bool → Value
+  null : Value
+{-# COMPILE GHC Value = data Data.Aeson.Value (Data.Aeson.Object|Data.Aeson.Array|Data.Aeson.String|Data.Aeson.Number|Data.Aeson.Bool|Data.Aeson.Null) #-}
+
+Object = KeyMap Value
+Array = Vector Value
+
+postulate
+  decode : ByteString → Maybe Value
+  eitherHDecode : ByteString → Either HaskellString Value
+{-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
+{-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}
+
+eitherDecode : ByteString → Either String Value
+eitherDecode bytes = mapLeft pack (eitherHDecode bytes)
+

prototyping/FFI/Data/Bool.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Bool where
+
+{-# FOREIGN GHC import qualified Data.Bool #-}
+
+data Bool : Set where
+  false : Bool
+  true : Bool
+{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}

prototyping/FFI/Data/ByteString.agda

@@ -0,0 +1,7 @@
+module FFI.Data.ByteString where
+
+{-# FOREIGN GHC import qualified Data.ByteString #-}
+
+postulate ByteString : Set
+{-# COMPILE GHC ByteString = type Data.ByteString.ByteString #-}
+

prototyping/FFI/Data/Either.agda

@@ -0,0 +1,16 @@
+module FFI.Data.Either where
+
+{-# FOREIGN GHC import qualified Data.Either #-}
+
+data Either (A B : Set) : Set where
+  Left : A → Either A B
+  Right : B → Either A B
+{-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-}
+
+mapLeft : ∀ {A B C} → (A → B) → (Either A C) → (Either B C)
+mapLeft f (Left x) = Left (f x)
+mapLeft f (Right x) = Right x
+
+mapRight : ∀ {A B C} → (B → C) → (Either A B) → (Either A C)
+mapRight f (Left x) = Left x
+mapRight f (Right x) = Right (f x)

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/HaskellString.agda

@@ -0,0 +1,16 @@
+module FFI.Data.HaskellString where
+
+open import Agda.Builtin.String using (String)
+
+{-# FOREIGN GHC import qualified Data.String #-}
+{-# FOREIGN GHC import qualified Data.Text #-}
+
+postulate HaskellString : Set
+{-# COMPILE GHC HaskellString = type Data.String.String #-}
+
+postulate pack : HaskellString → String
+{-# COMPILE GHC pack = Data.Text.pack #-}
+
+postulate unpack : String → HaskellString
+{-# COMPILE GHC unpack = Data.Text.unpack #-}
+

prototyping/FFI/Data/Maybe.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Maybe where
+
+{-# FOREIGN GHC import qualified Data.Maybe #-}
+
+data Maybe (A : Set) : Set where
+  nothing : Maybe A
+  just : A → Maybe A
+{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}

prototyping/FFI/Data/Scientific.agda

@@ -0,0 +1,6 @@
+module FFI.Data.Scientific where
+
+{-# FOREIGN GHC import qualified Data.Scientific #-}
+
+postulate Scientific : Set
+{-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}

prototyping/FFI/Data/String.agda

@@ -0,0 +1,8 @@
+module FFI.Data.String where
+
+import Agda.Builtin.String
+
+String = Agda.Builtin.String.String
+
+infixr 5 _++_
+_++_ = Agda.Builtin.String.primStringAppend

prototyping/FFI/Data/Text/Encoding.agda

@@ -0,0 +1,10 @@
+module FFI.Data.Text.Encoding where
+
+open import Agda.Builtin.String using (String)
+
+open import FFI.Data.ByteString using (ByteString)
+
+{-# FOREIGN GHC import qualified Data.Text.Encoding #-}
+
+postulate encodeUtf8 : String → ByteString
+{-# COMPILE GHC encodeUtf8 = Data.Text.Encoding.encodeUtf8 #-}

prototyping/FFI/Data/Vector.agda

@@ -0,0 +1,44 @@
+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 #-}
+
+postulate Vector : Set → Set
+{-# POLARITY Vector ++ #-}
+{-# COMPILE GHC Vector = type Data.Vector.Vector #-}
+
+postulate
+  empty : ∀ {A} → (Vector A)
+  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
+head vec | false = just (unsafeHead vec)
+head vec | true = nothing
+
+tail : ∀ {A} → (Vector A) → Vector A
+tail vec with null vec
+tail vec | false = unsafeTail vec
+tail vec | true = empty

prototyping/FFI/IO.agda

@@ -0,0 +1,34 @@
+module FFI.IO where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+open import Agda.Builtin.String using (String)
+
+open import FFI.Data.HaskellString using (HaskellString; pack ; unpack)
+
+infixl 1 _>>=_
+infixl 1 _>>_
+
+postulate
+  return : ∀ {a} {A : Set a} → A → IO A
+  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
+  fmap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B
+
+{-# COMPILE GHC return = \_ _ -> return    #-}
+{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
+{-# COMPILE GHC fmap  = \_ _ _ _ -> fmap #-}
+
+postulate getHContents : IO HaskellString
+{-# COMPILE GHC getHContents = getContents #-}
+
+postulate putHStrLn : HaskellString → IO ⊤
+{-# COMPILE GHC putHStrLn = putStrLn #-}
+
+getContents : IO String
+getContents = fmap pack getHContents
+
+putStrLn : String → IO ⊤
+putStrLn txt = putHStrLn (unpack txt)
+
+_>>_ : ∀ {a} {A : Set a} → IO ⊤ → IO A → IO A
+a >> b = a >>= (λ _ → b )

prototyping/FFI/System/Exit.agda

@@ -0,0 +1,29 @@
+module FFI.System.Exit where
+
+open import Agda.Builtin.Int using (Int)
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+
+data ExitCode : Set where
+  ExitSuccess : ExitCode
+  ExitFailure : Int → ExitCode
+
+{-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
+{-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}
+
+{-# FOREIGN GHC import qualified System.Exit #-}
+
+{-# FOREIGN GHC
+toExitCode :: AgdaExitCode -> System.Exit.ExitCode
+toExitCode AgdaExitSuccess = System.Exit.ExitSuccess
+toExitCode (AgdaExitFailure n) = System.Exit.ExitFailure (fromIntegral n)
+
+fromExitCode :: System.Exit.ExitCode -> AgdaExitCode
+fromExitCode System.Exit.ExitSuccess = AgdaExitSuccess
+fromExitCode (System.Exit.ExitFailure n) = AgdaExitFailure (fromIntegral n)
+#-}
+
+postulate
+  exitWith : ExitCode → IO ⊤
+
+{-# COMPILE GHC exitWith = System.Exit.exitWith . toExitCode #-}

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

@@ -0,0 +1,27 @@
+module Luau.Syntax where
+
+open import Luau.Var using (Var)
+open import Luau.Addr using (Addr)
+
+infixr 5 _∙_
+
+data Block : Set
+data Stat : Set
+data Expr : Set
+
+data Block where
+  _∙_ : Stat → Block → Block
+  done : Block
+
+data Stat where
+  function_⟨_⟩_end : Var → Var → Block → Stat
+  local_←_ : Var → Expr → Stat
+  return : Expr → Stat
+
+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

@@ -0,0 +1,125 @@
+module Luau.Syntax.FromJSON where
+
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
+
+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)
+
+args = fromString "args"
+body = fromString "body"
+func = fromString "func"
+lokal = fromString "local"
+list = fromString "list"
+name = fromString "name"
+type = fromString "type"
+values = fromString "values"
+vars = fromString "vars"
+
+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)
+
+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
+
+exprFromJSON (object obj) = exprFromObject obj
+exprFromJSON val = 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 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 _ | 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") | nothing = Left "AstExprLocal missing local"
+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(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) | 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") | 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)

prototyping/Luau/Syntax/ToString.agda

@@ -0,0 +1,49 @@
+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 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
+blockToString′ : String → Block → String
+
+exprToString′ lb nil =
+  "nil"
+exprToString′ lb (addr a) =
+  addrToString(a)
+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 ++
+  "  " ++ (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 ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end"
+statToString′ lb (local x ← M) =
+  "local " ++ 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 : Expr → String
+exprToString = exprToString′ "\n"
+
+statToString : Stat → String
+statToString = statToString′ "\n"
+
+blockToString : Block → String
+blockToString = blockToString′ "\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/PrettyPrinter.agda

@@ -0,0 +1,33 @@
+module PrettyPrinter 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)
+
+runBlock : Block → IO ⊤
+runBlock block = putStrLn (blockToString block)
+
+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/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

prototyping/README.md

@@ -0,0 +1,27 @@
+# Prototyping Luau
+
+![prototyping workflow](https://github.com/Roblox/luau/actions/workflows/prototyping.yml/badge.svg)
+
+An experimental prototyping system for the Luau type system. This is
+intended to allow core language features to be tested quickly, without
+having to interact with all the features of production Lua.
+
+## Building
+
+First install Haskell and Agda.
+
+Install dependencies:
+```
+  cabal update
+  cabal install --lib aeson scientific vector
+```
+
+Then compile
+```
+  agda --compile PrettyPrinter.agda
+```
+
+and run!
+```
+  luau-ast Examples/SmokeTest.lua | ./PrettyPrinter
+```