From 9ac0bec0d974bbedb6be991cacf66c5b9767d09c Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Mon, 7 Feb 2022 16:17:06 -0600 Subject: [PATCH] Got a smoke test to run --- prototyping/Examples/SmokeTest.lua | 14 ++ prototyping/Luau/Syntax/FromJSON.agda | 179 +++++++++++--------------- prototyping/README.md | 2 +- 3 files changed, 87 insertions(+), 108 deletions(-) create mode 100644 prototyping/Examples/SmokeTest.lua diff --git a/prototyping/Examples/SmokeTest.lua b/prototyping/Examples/SmokeTest.lua new file mode 100644 index 00000000..931b4f4e --- /dev/null +++ b/prototyping/Examples/SmokeTest.lua @@ -0,0 +1,14 @@ +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) + + diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 835966df..452a42f0 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -11,64 +11,13 @@ 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) -AstExprKeys = - "AstExprBinary" ∷ - "AstExprCall" ∷ - "AstExprConstantBool" ∷ - "AstExprConstantNil" ∷ - "AstExprConstantNumber" ∷ - "AstExprConstantString" ∷ - "AstExprError" ∷ - "AstExprFunction" ∷ - "AstExprGlobal" ∷ - "AstExprGroup" ∷ - "AstExprIndexExpr" ∷ - "AstExprIndexName" ∷ - "AstExprLocal" ∷ - "AstExprTable" ∷ - "AstExprTypeAssertion" ∷ - "AstExprUnary" ∷ - [] - -AstStatKeys = - "AstStatAssign" ∷ - "AstStatBlock" ∷ - "AstStatBreak" ∷ - "AstStatCompoundAssign" ∷ - "AstStatContinue" ∷ - "AstStatDeclareClass" ∷ - "AstStatDeclareFunction" ∷ - "AstStatDeclareGlobal" ∷ - "AstStatError" ∷ - "AstStatExpr" ∷ - "AstStatFor" ∷ - "AstStatForIn" ∷ - "AstStatFunction" ∷ - "AstStatIf" ∷ - "AstStatLocal" ∷ - "AstStatLocalFunction" ∷ - "AstStatRepeat" ∷ - "AstStatReturn" ∷ - "AstStatTypeAlias" ∷ - [] - -AstTypeKeys = - "AstTypeError" ∷ - "AstTypeFunction" ∷ - "AstTypeIntersection" ∷ - "AstTypePackExplicit" ∷ - "AstTypePackGeneric" ∷ - "AstTypePackVariadic" ∷ - "AstTypeReference" ∷ - "AstTypeTable" ∷ - "AstTypeTypeof" ∷ - "AstTypeUnion" ∷ - [] - args = fromString "args" body = fromString "body" func = fromString "func" +local = fromString "local" +list = fromString "list" name = fromString "name" +type = fromString "type" values = fromString "values" vars = fromString "vars" @@ -90,66 +39,82 @@ blockFromJSON : Value → Either String Block blockFromArray : Array → Either String Block exprFromJSON (object obj) = exprFromObject obj -exprFromJSON val = Left "Expr should be an object" +exprFromJSON val = Left "AstExpr not an object" -exprFromObject obj with lookupIn AstExprKeys obj -exprFromObject obj | ("AstExprCall" , object obj2) with lookup func obj2 | lookup args obj2 -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) with head arr -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) | just value2 with exprFromJSON value | exprFromJSON value2 -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) | just value2 | Right fun | Right arg = Right (fun $ arg) -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) | just value2 | Left err | _ = Left err -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) | just value2 | _ | Left err = Left err -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just (array arr) | nothing = Left ("AstExprCall empty args") -exprFromObject obj | ("AstExprCall" , object obj2) | just value | just _ = Left ("AstExprCall args not an array") -exprFromObject obj | ("AstExprCall" , object obj2) | nothing | _ = Left ("AstExprCall missing func") -exprFromObject obj | ("AstExprCall" , object obj2) | _ | nothing = Left ("AstExprCall missing args") -exprFromObject obj | ("AstExprConstantNil" , value) = Right nil -exprFromObject obj | ("AstExprFunction" , object obj2 ) with lookup args obj2 | lookup func obj2 -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just (array arr) | just value with head arr | blockFromJSON value -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just (array arr) | just value | just (string x) | Right B = Right (function⟨ x ⟩ B end) -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just (array arr) | just value | just _ | Right B = Left "AstExprFunction args not a string array" -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just (array arr) | just value | nothing | Right B = Left "Unsupported AstExprFunction empty args" -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just (array arr) | just value | _ | Left err = Left err -exprFromObject obj | ("AstExprFunction" , object obj2 ) | just _ | just _ = Left "AstExprFunction args not an array" -exprFromObject obj | ("AstExprFunction" , object obj2 ) | nothing | _ = Left "AstExprFunction missing args" -exprFromObject obj | ("AstExprFunction" , object obj2 ) | _ | nothing = Left "AstExprFunction missing body" -exprFromObject obj | ("AstExprLocal" , string x) = Right (var x) -exprFromObject obj | (key , value) = Left ("Unsupported " ++ key) -exprFromObject obj | nil = Left "Unexpected Expr 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 local 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 "Stat should be an object" +statFromJSON _ = Left "AstStat not an object" -statFromObject obj with lookupIn AstStatKeys obj -statFromObject obj | ("AstStatLocal" , object obj2) with lookup vars obj2 | lookup values obj2 -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) with head(arr1) | head(arr2) -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | just(string x) | just(value) with exprFromJSON(value) -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local x ← M) -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | just(string x) | just(value) | Left err = Left err -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | just(string x) | nothing = Left "AstStatLocal empty values" -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | just(_) | _ = Left "AstStatLocal vars not a string array" -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(array arr2) | nothing | _ = Left "AstStatLocal emptyvars" -statFromObject obj | ("AstStatLocal" , object obj2) | just(array arr1) | just(_) = Left "AstStatLocal values not an array" -statFromObject obj | ("AstStatLocal" , object obj2) | just(_) | just(_) = Left "AstStatLocal vars not an array" -statFromObject obj | ("AstStatLocal" , object obj2) | just(_) | nothing = Left "AstStatLocal missing values" -statFromObject obj | ("AstStatLocal" , object obj2) | nothing | _ = Left "AstStatLocal missing vars" -statFromObject obj | ("AstStatLocalFunction" , object obj2) with lookup name obj2 | lookup func obj2 -statFromObject obj | ("AstStatLocalFunction" , object obj2) | just (string f) | just value with exprFromJSON value -statFromObject obj | ("AstStatLocalFunction" , object obj2) | just (string f) | just value | Right (function⟨ x ⟩ B end) = Right (function f ⟨ x ⟩ B end) -statFromObject obj | ("AstStatLocalFunction" , object obj2) | just (string f) | just value | Left err = Left err -statFromObject obj | ("AstStatLocalFunction" , object obj2) | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction" -statFromObject obj | ("AstStatLocalFunction" , object obj2) | just _ | just _ = Left "AstStatLocalFunction name is not a string" -statFromObject obj | ("AstStatLocalFunction" , object obj2) | nothing | _ = Left "AstStatFunction missing name" -statFromObject obj | ("AstStatLocalFunction" , object obj2) | _ | nothing = Left "AstStatFunction missing func" -statFromObject obj | ("AstStatReturn" , value) with exprFromJSON value -statFromObject obj | ("AstStatReturn" , value) | Left err = Left err -statFromObject obj | ("AstStatReturn" , value) | Right expr = Right (return expr) -statFromObject obj | (key , value) = Left ("Unsupported " ++ key) -statFromObject obj | nil = Left "Unexpected Stat 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 _ = Left "Block should be an array" +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" diff --git a/prototyping/README.md b/prototyping/README.md index c8402f13..05f3c2e4 100644 --- a/prototyping/README.md +++ b/prototyping/README.md @@ -21,5 +21,5 @@ Then compile and run! ``` - echo '[{"AstStatReturn":{"AstExprConstantNil": {}}}]' | ./Main + luau-ast Examples/SmokeTest.lua | ./Main ```