From f0c9d84461339fa8bcd2d8bf7d6f5be5be029f46 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Tue, 15 Feb 2022 14:10:43 -0800 Subject: [PATCH] Prototyping: Parse type annotations (#366) Parses type annotations from the JSON output of `luau-ast`. --- prototyping/Examples/SmokeTest.lua | 5 ++ prototyping/Examples/SmokeTestOutput.lua | 8 ++- prototyping/Luau/Syntax/FromJSON.agda | 15 ++++-- prototyping/Luau/Type/FromJSON.agda | 66 ++++++++++++++++++++++++ 4 files changed, 88 insertions(+), 6 deletions(-) create mode 100644 prototyping/Luau/Type/FromJSON.agda diff --git a/prototyping/Examples/SmokeTest.lua b/prototyping/Examples/SmokeTest.lua index e1e37e3..e663534 100644 --- a/prototyping/Examples/SmokeTest.lua +++ b/prototyping/Examples/SmokeTest.lua @@ -10,4 +10,9 @@ local function comp(f) end local id2 = comp(id)(id) local nil2 = id2(nil) +local a : any = nil +local b : nil = nil +local c : (nil) -> nil = nil +local d : (any & nil) = nil +local e : any? = nil return id2(nil2) diff --git a/prototyping/Examples/SmokeTestOutput.lua b/prototyping/Examples/SmokeTestOutput.lua index b1b91e1..e663534 100644 --- a/prototyping/Examples/SmokeTestOutput.lua +++ b/prototyping/Examples/SmokeTestOutput.lua @@ -8,5 +8,11 @@ local function comp(f) end end end -local id2 = id(id) +local id2 = comp(id)(id) local nil2 = id2(nil) +local a : any = nil +local b : nil = nil +local c : (nil) -> nil = nil +local d : (any & nil) = nil +local e : any? = nil +return id2(nil2) diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 82f9519..8ae620b 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -1,6 +1,7 @@ module Luau.Syntax.FromJSON where -open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec) +open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec) +open import Luau.Type.FromJSON using (typeFromJSON) open import Agda.Builtin.List using (List; _∷_; []) @@ -43,10 +44,14 @@ blockFromArray : Array → Either String (Block maybe) varDecFromJSON (object arg) = varDecFromObject arg varDecFromJSON val = Left "VarDec not an object" -varDecFromObject obj with lookup name obj -varDecFromObject obj | just (string name) = Right (var name) -varDecFromObject obj | just _ = Left "AstLocal name is not a string" -varDecFromObject obj | nothing = Left "AstLocal missing name" +varDecFromObject obj with lookup name obj | lookup type obj +varDecFromObject obj | just (string name) | nothing = Right (var name) +varDecFromObject obj | just (string name) | just Value.null = Right (var name) +varDecFromObject obj | just (string name) | just tyValue with typeFromJSON tyValue +varDecFromObject obj | just (string name) | just tyValue | Right ty = Right (var name ∈ ty) +varDecFromObject obj | just (string name) | just tyValue | Left err = Left err +varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string" +varDecFromObject obj | nothing | _ = Left "AstLocal missing name" exprFromJSON (object obj) = exprFromObject obj exprFromJSON val = Left "AstExpr not an object" diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda new file mode 100644 index 0000000..45bda5f --- /dev/null +++ b/prototyping/Luau/Type/FromJSON.agda @@ -0,0 +1,66 @@ +module Luau.Type.FromJSON where + +open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any) + +open import Agda.Builtin.List using (List; _∷_; []) + +open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup) +open import FFI.Data.Bool using (true; false) +open import FFI.Data.Either using (Either; Left; Right) +open import FFI.Data.Maybe using (Maybe; nothing; just) +open import FFI.Data.String using (String; _++_) +open import FFI.Data.Vector using (head; tail; null; empty) + +name = fromString "name" +type = fromString "type" +argTypes = fromString "argTypes" +returnTypes = fromString "returnTypes" +types = fromString "types" + +{-# TERMINATING #-} +typeFromJSON : Value → Either String Type +compoundFromArray : (Type → Type → Type) → Array → Either String Type + +typeFromJSON (object o) with lookup type o +typeFromJSON (object o) | just (string "AstTypeFunction") with lookup argTypes o | lookup returnTypes o +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) with lookup types argsSet | lookup types retsSet +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) with head args | head rets +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue with typeFromJSON argValue | typeFromJSON retValue +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Right arg | Right ret = Right (arg ⇒ ret) +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Left err | _ = Left err +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | _ | Left err = Left err +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | _ | nothing = Left "No return type" +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | nothing | _ = Left "No argument type" +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just _ | _ = Left "argTypes.types is not an array" +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | _ | just _ = Left "retTypes.types is not an array" +typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | nothing | _ = Left "argTypes.types does not exist" +typeFromJSON (object o) | just (string "AstTypeFunction") | _ | just _ = Left "argTypes is not an object" +typeFromJSON (object o) | just (string "AstTypeFunction") | just _ | _ = Left "returnTypes is not an object" +typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing = Left "Missing argTypes and returnTypes" + +typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any +typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type" + +typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o +typeFromJSON (object o) | just (string "AstTypeUnion") | just (array types) = compoundFromArray _∪_ types +typeFromJSON (object o) | just (string "AstTypeUnion") | _ = Left "`types` field must be an array" + +typeFromJSON (object o) | just (string "AstTypeIntersection") with lookup types o +typeFromJSON (object o) | just (string "AstTypeIntersection") | just (array types) = compoundFromArray _∩_ types +typeFromJSON (object o) | just (string "AstTypeIntersection") | _ = Left "`types` field must be an array" + +typeFromJSON (object o) | just (string ty) = Left ("Unsupported type " ++ ty) +typeFromJSON (object o) | just _ = Left "`type` field must be a string" +typeFromJSON (object o) | nothing = Left "No `type` field" +typeFromJSON _ = Left "Unsupported JSON type" + +compoundFromArray ctor ts with head ts | tail ts +compoundFromArray ctor ts | just hd | tl with null tl +compoundFromArray ctor ts | just hd | tl | true = typeFromJSON hd +compoundFromArray ctor ts | just hd | tl | false with typeFromJSON hd | compoundFromArray ctor tl +compoundFromArray ctor ts | just hd | tl | false | Right hdTy | Right tlTy = Right (ctor hdTy tlTy) +compoundFromArray ctor ts | just hd | tl | false | Left err | _ = Left err +compoundFromArray ctor ts | just hd | tl | false | _ | Left Err = Left Err +compoundFromArray ctor ts | nothing | empty = Left "Empty types array?"