Completed translating lambda-calculus + nil from JSON to Agda

prototyping/Luau/Syntax.agda

@@ -32,3 +32,4 @@ data Expr where
   nil : Expr
   var : Var → Expr
   _$_ : Expr → Expr → Expr
+  function⟨_⟩_end : Var → Block → Expr

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,10 +1,10 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; return; _∙; _∙_)
+open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; _∙; _∙_)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
-open import FFI.Data.Aeson using (Value; Array; Object; object; array; fromString; lookup)
+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)
@@ -65,6 +65,13 @@ AstTypeKeys =
   "AstTypeUnion" ∷
   []
 
+args = fromString "args"
+body = fromString "body"
+func = fromString "func"
+name = fromString "name"
+values = fromString "values"
+vars = fromString "vars"
+
 data Lookup : Set where
   _,_ : String → Value → Lookup
   nil : Lookup
@@ -86,7 +93,27 @@ exprFromJSON (object obj) = exprFromObject obj
 exprFromJSON val = Left "Expr should be 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"
 
@@ -95,6 +122,26 @@ statFromJSON (object obj) = statFromObject obj
 statFromJSON _ = Left "Stat should be 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)

prototyping/Luau/Syntax/ToString.agda

@@ -1,29 +1,39 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; return ; function_⟨_⟩_end ; local_←_; _∙_; _∙)
+open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; _∙)
 
 open import FFI.Data.String using (String; _++_)
 
-exprToString : Expr → String
+exprToString′ : String → Expr → String
-exprToString nil = "nil"
-exprToString (var x) = x
-exprToString (M $ N) = (exprToString M) ++ "(" ++ (exprToString N) ++ ")"
-
 statToString′ : String → Stat → String
 blockToString′ : String → Block → String
 
+exprToString′ lb nil =
+  "nil"
+exprToString′ lb (var x) =
+  x
+exprToString′ lb (M $ N) =
+  (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
+exprToString′ lb (function⟨ x ⟩ B end) =
+  "function (" ++ x ++ ")" ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end"
+
 statToString′ lb (function f ⟨ x ⟩ B end) =
   "function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 statToString′ lb (local x ← M) =
-  "local " ++ x ++ " = " ++ (exprToString M)
+  "local " ++ x ++ " = " ++ (exprToString′ lb M)
 statToString′ lb (return M) =
-  "return " ++ (exprToString M)
+  "return " ++ (exprToString′ lb M)
 
 blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
 blockToString′ lb (S ∙) = statToString′ lb S
 
+exprToString : Expr → String
+exprToString = exprToString′ "\n"
+
 statToString : Stat → String
 statToString = statToString′ "\n"