michael/luau
michael
/
luau
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Prototyping: Parse type annotations (#366) 

Parses type annotations from the JSON output of `luau-ast`.
This commit is contained in:
Lily Brown 2022-02-15 14:10:43 -08:00 committed by GitHub
parent 4b7e06e14f
commit f0c9d84461
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 88 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
prototyping/Examples/SmokeTest.lua
View File

@ -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)

8
prototyping/Examples/SmokeTestOutput.lua
View File

@ -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)

15
prototyping/Luau/Syntax/FromJSON.agda
View File

@ -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"

66
prototyping/Luau/Type/FromJSON.agda Normal file
View File

@ -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?"