syntax understands numbers

prototyping/Examples/SmokeTest.lua

@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f = 123
 return id2(nil2)

prototyping/FFI/Data/Scientific.agda

@@ -1,6 +1,18 @@
 module FFI.Data.Scientific where
 
+open import FFI.Data.String using (String)
+open import FFI.Data.HaskellString using (HaskellString; pack; unpack)
+
 {-# FOREIGN GHC import qualified Data.Scientific #-}
+{-# FOREIGN GHC import qualified Text.Show #-}
 
 postulate Scientific : Set
 {-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}
+
+postulate
+  showHaskell : Scientific → HaskellString
+
+{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
+
+show : Scientific → String
+show x = pack (showHaskell x)

prototyping/Luau/Syntax.agda

@@ -5,6 +5,7 @@ open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Type using (Type)
+open import FFI.Data.Scientific using (Scientific)
 
 infixr 5 _∙_
 
@@ -52,4 +53,4 @@ data Expr a where
   _$_ : Expr a → Expr a → Expr a
   function_is_end : FunDec a → Block a → Expr a
   block_is_end : Var → Block a → Expr a
-
+  number_ : Scientific → Expr a

prototyping/Luau/Syntax/FromJSON.agda

@@ -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)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number_)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
@@ -19,6 +19,7 @@ lokal = fromString "local"
 list = fromString "list"
 name = fromString "name"
 type = fromString "type"
+value = fromString "value"
 values = fromString "values"
 vars = fromString "vars"
 
@@ -83,6 +84,10 @@ 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′))
 exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
 exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
+exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number 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 ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
 exprFromObject obj | nothing = Left "AstExpr missing type"

prototyping/Luau/Syntax/ToString.agda

@@ -1,7 +1,8 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number_)
 open import FFI.Data.String using (String; _++_)
+open import FFI.Data.Scientific using (show)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
 open import Luau.Var.ToString using (varToString)
@@ -36,6 +37,7 @@ exprToString′ lb (block b is B end) =
   "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
+exprToString′ lb (number x) = show x
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++

prototyping/Luau/Type.agda

@@ -7,6 +7,7 @@ data Type : Set where
   _⇒_ : Type → Type → Type
   none : Type
   any : Type
+  number : Type
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
@@ -15,6 +16,7 @@ src nil = none
 src (S ⇒ T) = S
 src none = none
 src any = any
+src number = none
 src (S ∪ T) = (src S) ∪ (src T)
 src (S ∩ T) = (src S) ∩ (src T)
 
@@ -23,6 +25,7 @@ tgt nil = none
 tgt (S ⇒ T) = T
 tgt none = none
 tgt any = any
+tgt number = none
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
 
@@ -40,4 +43,3 @@ normalizeOptional (S ∪ T) | S′         | nil        = optional S′
 normalizeOptional (S ∪ T) | nil        | T′         = optional T′
 normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
 normalizeOptional T = T
-

prototyping/Luau/Type/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Type.FromJSON where
 
-open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any)
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
@@ -41,6 +41,7 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
 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") | just (string "number") = Right number
 typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
 
 typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o

prototyping/Luau/Type/ToString.agda

@@ -1,7 +1,7 @@
 module Luau.Type.ToString where
 
 open import FFI.Data.String using (String; _++_)
-open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
+open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)
 
 {-# TERMINATING #-}
 typeToString : Type → String
@@ -12,6 +12,7 @@ typeToString nil = "nil"
 typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
 typeToString none = "none"
 typeToString any = "any"
+typeToString number = "number"
 typeToString (S ∪ T) with normalizeOptional(S ∪ T)
 typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
 typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"

prototyping/Luau/Value.agda

@@ -1,5 +1,6 @@
 module Luau.Value where
 
+open import FFI.Data.Scientific using (Scientific)
 open import Luau.Addr using (Addr)
 open import Luau.Syntax using (Block; Expr; nil; addr)
 open import Luau.Var using (Var)
@@ -7,9 +8,9 @@ open import Luau.Var using (Var)
 data Value : Set where
   nil : Value
   addr : Addr → Value
+  number : Scientific → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
-
+val (number x) = Luau.Syntax.Expr.number x
-

prototyping/Luau/Value/ToString.agda

@@ -1,10 +1,11 @@
 module Luau.Value.ToString where
 
 open import Agda.Builtin.String using (String)
-open import Luau.Value using (Value; nil; addr)
+open import FFI.Data.Scientific using (show)
+open import Luau.Value using (Value; nil; addr; number)
 open import Luau.Addr.ToString using (addrToString)
 
 valueToString : Value → String
 valueToString nil = "nil"
 valueToString (addr a) = addrToString a
- 
+valueToString (number x) = show x