parsing works

This commit is contained in:
Lily Brown 2022-02-18 16:02:26 -08:00
parent 9d583be8ae
commit 64ce6c2367
3 changed files with 27 additions and 3 deletions

View file

@ -1,6 +1,6 @@
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)
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; _∷_; [])
@ -23,6 +23,9 @@ type = fromString "type"
value = fromString "value"
values = fromString "values"
vars = fromString "vars"
op = fromString "op"
left = fromString "left"
right = fromString "right"
data Lookup : Set where
_,_ : String Value Lookup
@ -34,6 +37,8 @@ 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)
binOpFromJSON : Value Either String BinaryOperator
binOpFromString : String Either String BinaryOperator
varDecFromJSON : Value Either String (VarDec maybe)
varDecFromObject : Object Either String (VarDec maybe)
exprFromJSON : Value Either String (Expr maybe)
@ -43,6 +48,15 @@ statFromObject : Object → Either String (Stat maybe)
blockFromJSON : Value Either String (Block maybe)
blockFromArray : Array Either String (Block maybe)
binOpFromJSON (string s) = binOpFromString s
binOpFromJSON val = Left "Binary operator not a string"
binOpFromString "Add" = Right +
binOpFromString "Sub" = Right -
binOpFromString "Mul" = Right *
binOpFromString "Div" = Right /
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
varDecFromJSON (object arg) = varDecFromObject arg
varDecFromJSON val = Left "VarDec not an object"
@ -89,6 +103,15 @@ exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o | Right l | Right r = Right (binexp l o r)
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err
exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary"
exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary"
exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary"
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"
@ -146,3 +169,4 @@ blockFromArray arr | just value | Left err = Left err
blockFromArray arr | just value | Right S with blockFromArray(tail arr)
blockFromArray arr | just value | Right S | Left err = Left (err)
blockFromArray arr | just value | Right S | Right B = Right (S B)

View file

@ -1 +1 @@
return 1 + 2 - 3
return 1 + 2 - 2 * 2 / 2

View file

@ -1 +1 @@
-1.0
1.0