Improved handling of Stat/Block

prototyping/Examples/Syntax.agda

@@ -2,7 +2,7 @@ module Examples.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.String using (_++_)
-open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end_)
+open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; _∙; _∙_)
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
 f = var "f"
@@ -12,11 +12,11 @@ ex1 : exprToString(f $ x) ≡
   "f(x)"
 ex1 = refl
 
-ex2 : blockToString(return nil) ≡
+ex2 : blockToString(return nil ∙) ≡
   "return nil"
 ex2 = refl
 
-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x end return f) ≡
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡
   "function f(x)\n" ++
   "  return x\n" ++
   "end\n" ++

prototyping/FFI/Data/Bool.agda

@@ -5,4 +5,4 @@ module FFI.Data.Bool where
 data Bool : Set where
   false : Bool
   true : Bool
-{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.True|Data.Bool.False) #-}
+{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}

prototyping/FFI/Data/Vector.agda

@@ -13,14 +13,19 @@ postulate
   empty : ∀ {A} → (Vector A)
   null : ∀ {A} → (Vector A) → Bool
   unsafeHead : ∀ {A} → (Vector A) → A
-  tail : ∀ {A} → (Vector A) → (Vector A)
+  unsafeTail : ∀ {A} → (Vector A) → (Vector A)
 {-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
 {-# COMPILE GHC null = \_ -> Data.Vector.null #-}
 {-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
-{-# COMPILE GHC tail = \_ -> Data.Vector.tail #-}
+{-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
 
 head : ∀ {A} → (Vector A) → (Maybe A)
 head vec with null vec
 head vec | false = just (unsafeHead vec)
 head vec | true = nothing
 
+tail : ∀ {A} → (Vector A) → Vector A
+tail vec with null vec
+tail vec | false = unsafeTail vec
+tail vec | true = empty
+

prototyping/Luau/Syntax.agda

@@ -2,6 +2,8 @@ module Luau.Syntax where
 
 open import Agda.Builtin.String using (String)
 
+infixr 5 _∙_
+
 data Type : Set where
   nil : Type
   _⇒_ : Type → Type → Type
@@ -14,12 +16,17 @@ Var : Set
 Var = String
 
 data Block : Set
+data Stat : Set
 data Expr : Set
 
 data Block where
-  function_⟨_⟩_end_ : Var → Var → Block → Block → Block
-  local_←_∙_ : Var → Expr → Block → Block
-  return : Expr → Block
+  _∙_ : Stat → Block → Block
+  _∙ : Stat → Block
+
+data Stat where
+  function_⟨_⟩_end : Var → Var → Block → Stat
+  local_←_ : Var → Expr → Stat
+  return : Expr → Stat
 
 data Expr where
   nil : Expr

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,22 +1,23 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Type; Block; Expr; nil; return)
-
-open import Agda.Builtin.String using (String)
+open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; return; _∙; _∙_)
 
 open import FFI.Data.Aeson using (Value; Array; Object; object; array; 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 (nothing; just)
-open import FFI.Data.Vector using (head; empty)
+open import FFI.Data.String using (String; _++_)
+open import FFI.Data.Vector using (head; tail; null; empty)
 
 AstExprConstantNil = fromString "AstExprConstantNil"
 AstStatReturn = fromString "AstStatReturn"
 
 exprFromJSON : Value → Either String Expr
 exprFromObject : Object → Either String Expr
+statFromJSON : Value → Either String Stat
+statFromObject : Object → Either String Stat
 blockFromJSON : Value → Either String Block
 blockFromArray : Array → Either String Block
-blockFromObject : Object → Array → Either String Block
 
 exprFromJSON (object obj) = exprFromObject obj
 exprFromJSON val = Left "Expr should be an object"
@@ -25,19 +26,25 @@ exprFromObject obj with lookup AstExprConstantNil obj
 exprFromObject obj | just val = Right nil
 exprFromObject obj | nothing = Left "Unsupported Expr"
 
-blockFromJSON (object obj) = blockFromObject obj empty
+{-# NON_TERMINATING #-}
+statFromJSON (object obj) = statFromObject obj
+statFromJSON _ = Left "Stat should be an object"
+
+statFromObject obj with lookup AstStatReturn obj
+statFromObject obj | just val with exprFromJSON val
+statFromObject obj | just val | Left err = Left err
+statFromObject obj | just val | Right exp = Right (return exp)
+statFromObject obj | nothing = Left "Unsupported Stat"
+
 blockFromJSON (array arr) = blockFromArray arr
-blockFromJSON _ = Left "Block should be an object or array"
+blockFromJSON _ = Left "Block should be an array"
 
 blockFromArray arr with head arr
-blockFromArray arr | nothing = Right (return nil)
-blockFromArray arr | just (object obj) = blockFromObject obj arr
-blockFromArray arr | just (x) = Left "Stat should be an object"
-
-blockFromObject obj arr with lookup AstStatReturn obj
-blockFromObject obj arr | just val with exprFromJSON val
-blockFromObject obj arr | just val | Left err = Left err
-blockFromObject obj arr | just val | Right exp = Right (return exp)
-blockFromObject obj arr | nothing = Left "Unsupported Stat"
-
-
+blockFromArray arr | nothing = Left "Block should be a non-empty array"
+blockFromArray arr | just value with statFromJSON value
+blockFromArray arr | just value | Left err = Left err
+blockFromArray arr | just value | Right S with null (tail arr)
+blockFromArray arr | just value | Right S | true = Right (S ∙)
+blockFromArray arr | just value | Right S | false with blockFromArray(tail arr)
+blockFromArray arr | just value | Right S | false | Left err = Left (err)
+blockFromArray arr | just value | Right S | false | Right B  = Right (S ∙ B)

prototyping/Luau/Syntax/ToString.agda

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

prototyping/README.md

@@ -21,5 +21,5 @@ Then compile
 
 and run!
 ```
-  echo '{"some": "JSON"}' | ./Main
+  echo '[{"AstStatReturn":{"AstExprConstantNil": {}}}]' | ./Main
 ```