Prototyping a small subset of Luau in Agda (#350)

* First cut reading JSON into an Agda representation of Luau syntax

.github/workflows/prototyping.yml

@@ -0,0 +1,55 @@
+name: prototyping
+
+on:
+  push:
+    branches:
+      - 'master'
+    paths:
+      - '.github/workflows/**'
+      - 'prototyping/**'
+  pull_request:
+    paths:
+      - '.github/workflows/**'
+      - 'prototyping/**'
+
+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 PrettyPrinter
+      working-directory: prototyping
+      run: ~/.cabal/bin/agda --compile --ghc-flag=-v PrettyPrinter.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
+    - name: diff smoketest
+      working-directory: prototyping
+      run: diff Examples/SmokeTest.lua Examples/SmokeTestOutput.lua

prototyping/.gitignore

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

prototyping/Examples.agda

@@ -0,0 +1,4 @@
+module Examples where
+
+import Examples.Syntax
+

prototyping/Examples/SmokeTest.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; _∙; _∙_)
+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 ∙) ≡
+  "return nil"
+ex2 = refl
+
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡
+  "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/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,31 @@
+module FFI.Data.Vector where
+
+open import FFI.Data.Bool using (Bool; false; true)
+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)
+{-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
+{-# COMPILE GHC null = \_ -> Data.Vector.null #-}
+{-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
+{-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
+
+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/Luau/Syntax.agda

@@ -0,0 +1,35 @@
+module Luau.Syntax where
+
+open import Agda.Builtin.String using (String)
+
+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
+
+data Stat where
+  function_⟨_⟩_end : Var → Var → Block → Stat
+  local_←_ : Var → Expr → Stat
+  return : Expr → Stat
+
+data Expr where
+  nil : Expr
+  var : Var → Expr
+  _$_ : Expr → Expr → Expr
+  function⟨_⟩_end : Var → Block → Expr

prototyping/Luau/Syntax/FromJSON.agda

@@ -0,0 +1,127 @@
+module Luau.Syntax.FromJSON where
+
+open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; _∙; _∙_)
+
+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 = Left "Block should be a non-empty array"
+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)

prototyping/Luau/Syntax/ToString.agda

@@ -0,0 +1,41 @@
+module Luau.Syntax.ToString where
+
+open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; _∙)
+
+open import FFI.Data.String using (String; _++_)
+
+exprToString′ : String → Expr → String
+statToString′ : String → Stat → String
+blockToString′ : String → Block → String
+
+exprToString′ lb nil =
+  "nil"
+exprToString′ lb (var x) =
+  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"
+
+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 ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
+blockToString′ lb (S ∙) = statToString′ lb S
+
+exprToString : Expr → String
+exprToString = exprToString′ "\n"
+
+statToString : Stat → String
+statToString = statToString′ "\n"
+
+blockToString : Block → String
+blockToString = blockToString′ "\n"

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/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
+```