Got interpreter to print a type error for any annotated program with a runtime error

This commit is contained in:
ajeffrey@roblox.com 2022-02-24 17:23:51 -06:00
parent 55f3f284a4
commit 05512cdbf8
3 changed files with 3678 additions and 163 deletions

3799
Makefile

File diff suppressed because it is too large Load diff

View file

@ -28,14 +28,14 @@ runBlock : ∀ a → Block a → IO
runBlock a block with run block
runBlock a block | return V D = putStrLn (valueToString V)
runBlock a block | done D = putStrLn "nil"
runBlock maybe block | error E D = putStrLn (errToStringᴮ _ E)
runBlock maybe block | error E D = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E)
runBlock yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
runBlock yes block | error E D | W = putStrLn (errToStringᴮ _ E) >> putStrLn (warningToStringᴮ _ W)
runBlock yes block | error E D | W = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E ++ "\n\nTYPE ERROR:\n" ++ warningToStringᴮ _ W)
runBlock : Block maybe IO
runBlock B with isAnnotatedᴮ B
runBlock B | nothing = runBlock maybe B
runBlock B | just B = runBlock yes B
runBlock B | nothing = putStrLn ("UNANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock maybe B
runBlock B | just B = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock yes B
runJSON : Value IO
runJSON value with blockFromJSON(value)

View file

@ -2,7 +2,7 @@
module Luau.Syntax.FromJSON where
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /)
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /)
open import Luau.Type.FromJSON using (typeFromJSON)
open import Agda.Builtin.List using (List; _∷_; [])
@ -28,6 +28,8 @@ vars = fromString "vars"
op = fromString "op"
left = fromString "left"
right = fromString "right"
returnAnnotation = fromString "returnAnnotation"
types = fromString "types"
data Lookup : Set where
_,_ : String Value Lookup
@ -86,16 +88,25 @@ exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("
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 blockValue with head arr | blockFromJSON blockValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | 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 "AstExprFunction") with lookup args obj | lookup body obj | lookup returnAnnotation obj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn with head arr | blockFromJSON blockValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B with varDecFromJSON argValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg with lookup types rtnObj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) with head rtnTypes
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType with typeFromJSON rtnType
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Right T = Right (function "" arg ⟩∈ T is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | nothing = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just _ = Left "returnAnnotation types not an array"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | nothing = Left "returnAnnotation missing types"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just _ | just argValue | Right B | Right arg = Left "returnAnnotation not an object"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | just argValue | Right B | Right arg = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | _ | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ | rtn = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ | rtn = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing | rtn = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
exprFromObject obj | just (string "AstExprLocal") | just x | Right x = Right (var (Luau.Syntax.name x))
@ -138,6 +149,7 @@ statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLo
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" x is B end) = Right (function (Luau.Syntax.name fnVar) x is B end)
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" x ⟩∈ T is B end) = Right (function (Luau.Syntax.name fnVar) x ⟩∈ T is B end)
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"