From 7f867ac166c39a3b291a5a66e70500335e3211a3 Mon Sep 17 00:00:00 2001
From: Lily Brown <lbrown@roblox.com>
Date: Fri, 18 Feb 2022 11:09:00 -0800
Subject: [PATCH] Prototyping: numbers (#368)

Adds number support to the prototype. Binary operators are next.
---
 prototyping/Examples/OpSem.agda                   |  1 -
 prototyping/Examples/Run.agda                     |  7 +++++--
 prototyping/FFI/Data/Scientific.agda              | 15 +++++++++++++++
 prototyping/Interpreter.agda                      |  1 -
 prototyping/Luau/RuntimeError.agda                |  5 +++--
 prototyping/Luau/RuntimeError/ToString.agda       |  8 ++++++--
 prototyping/Luau/Substitution.agda                |  4 ++--
 prototyping/Luau/Syntax.agda                      |  3 ++-
 prototyping/Luau/Syntax/FromJSON.agda             |  8 +++++++-
 prototyping/Luau/Syntax/ToString.agda             |  4 +++-
 prototyping/Luau/Type.agda                        |  4 +++-
 prototyping/Luau/Type/FromJSON.agda               |  3 ++-
 prototyping/Luau/Type/ToString.agda               |  3 ++-
 prototyping/Luau/Value.agda                       |  7 ++++---
 prototyping/Luau/Value/ToString.agda              |  5 +++--
 prototyping/PrettyPrinter.agda                    |  1 -
 prototyping/Properties/Step.agda                  |  8 +++++---
 prototyping/Tests/PrettyPrinter/smoke_test/in.lua |  1 +
 .../Tests/PrettyPrinter/smoke_test/out.txt        |  1 +
 19 files changed, 64 insertions(+), 25 deletions(-)

diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda
index ec8bce7b..c4cfc5e5 100644
--- a/prototyping/Examples/OpSem.agda
+++ b/prototyping/Examples/OpSem.agda
@@ -6,4 +6,3 @@ open import Luau.Heap using (∅)
 
 ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
 ex1 = subst
-
diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda
index 88ca39b6..3cac564d 100644
--- a/prototyping/Examples/Run.agda
+++ b/prototyping/Examples/Run.agda
@@ -3,8 +3,8 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
-open import Luau.Value using (nil)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number)
+open import Luau.Value using (nil; number)
 open import Luau.Run using (run; return)
 open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
 
@@ -13,3 +13,6 @@ import Agda.Builtin.Equality.Rewrite
 
 ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
 ex1 = refl
+
+ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
+ex2 = refl
diff --git a/prototyping/FFI/Data/Scientific.agda b/prototyping/FFI/Data/Scientific.agda
index 8a5be39e..772d3367 100644
--- a/prototyping/FFI/Data/Scientific.agda
+++ b/prototyping/FFI/Data/Scientific.agda
@@ -1,6 +1,21 @@
 module FFI.Data.Scientific where
 
+open import Agda.Builtin.Float using (Float)
+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
+  toFloat : Scientific → Float
+
+{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
+{-# COMPILE GHC toFloat = \x -> Data.Scientific.toRealFloat x #-}
+
+show : Scientific → String
+show x = pack (showHaskell x)
diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda
index 3ec5b8d1..fe311e57 100644
--- a/prototyping/Interpreter.agda
+++ b/prototyping/Interpreter.agda
@@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-
diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index e514dc9d..f9e684b3 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -3,13 +3,15 @@ module Luau.RuntimeError where
 open import Agda.Builtin.Equality using (_≡_)
 open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
+open import FFI.Data.String using (String)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number)
 
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
   NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
+  NumberIsNotAFunction : ∀ n {M} → RuntimeErrorᴱ H ((number n) $ M)
   UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
   SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
   app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
@@ -18,4 +20,3 @@ data RuntimeErrorᴱ H where
 data RuntimeErrorᴮ H where
   local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
   return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
-
diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda
index e8287157..ac760fab 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -1,15 +1,18 @@
 module Luau.RuntimeError.ToString where
 
+open import Agda.Builtin.Float using (primShowFloat)
 open import FFI.Data.String using (String; _++_)
-open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block)
 open import Luau.Addr.ToString using (addrToString)
+open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
-open import Luau.Syntax using (name)
+open import Luau.Syntax using (name; _$_)
 
 errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
 errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
 
 errToStringᴱ NilIsNotAFunction = "nil is not a function"
+errToStringᴱ (NumberIsNotAFunction n) = "number " ++ primShowFloat n ++ " is not a function"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
 errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app E) = errToStringᴱ E
@@ -17,3 +20,4 @@ errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ v
 
 errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"
+ 
\ No newline at end of file
diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda
index b956aeae..e364a000 100644
--- a/prototyping/Luau/Substitution.agda
+++ b/prototyping/Luau/Substitution.agda
@@ -1,6 +1,6 @@
 module Luau.Substitution where
 
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -13,6 +13,7 @@ _[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block
 nil [ v / x ]ᴱ = nil
 var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
 addr a [ v / x ]ᴱ = addr a
+(number y) [ v / x ]ᴱ = number y
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
 function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
 block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
@@ -27,4 +28,3 @@ var y [ v / x ]ᴱwhenever no p = var y
 
 B [ v / x ]ᴮunless yes p = B
 B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ
-
diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda
index 04970b62..1313456b 100644
--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@@ -1,6 +1,7 @@
 module Luau.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float)
 open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
@@ -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 : Float → Expr a
diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda
index 8ae620bb..8191e9e7 100644
--- a/prototyping/Luau/Syntax/FromJSON.agda
+++ b/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; _∷_; [])
@@ -9,6 +9,7 @@ open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; f
 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)
+open import FFI.Data.Scientific using (toFloat)
 open import FFI.Data.String using (String; _++_)
 open import FFI.Data.Vector using (head; tail; null; empty)
 
@@ -19,6 +20,7 @@ lokal = fromString "local"
 list = fromString "list"
 name = fromString "name"
 type = fromString "type"
+value = fromString "value"
 values = fromString "values"
 vars = fromString "vars"
 
@@ -83,6 +85,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 (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 ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
 exprFromObject obj | nothing = Left "AstExpr missing type"
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 18d36175..a20b360b 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -1,6 +1,7 @@
 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 Agda.Builtin.Float using (primShowFloat)
+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 Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -36,6 +37,7 @@ exprToString′ lb (block b is B end) =
   "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
+exprToString′ lb (number x) = primShowFloat x
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 6e384c3b..af5f857c 100644
--- a/prototyping/Luau/Type.agda
+++ b/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
-
diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda
index 45bda5f3..c585c3f3 100644
--- a/prototyping/Luau/Type/FromJSON.agda
+++ b/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
diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda
index 698d6e8e..e7a7c1c0 100644
--- a/prototyping/Luau/Type/ToString.agda
+++ b/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′ ++ "?"
diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda
index 4768f859..1086d39c 100644
--- a/prototyping/Luau/Value.agda
+++ b/prototyping/Luau/Value.agda
@@ -1,15 +1,16 @@
 module Luau.Value where
 
+open import Agda.Builtin.Float using (Float)
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr)
+open import Luau.Syntax using (Block; Expr; nil; addr; number)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
+  number : Float → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
-
-
+val (number x) = number x
diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda
index 3cac3ee7..51c3fa78 100644
--- a/prototyping/Luau/Value/ToString.agda
+++ b/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 Agda.Builtin.Float using (primShowFloat)
+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) = primShowFloat x
diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda
index 4a6c7dd6..fdad32d6 100644
--- a/prototyping/PrettyPrinter.agda
+++ b/prototyping/PrettyPrinter.agda
@@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-
diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda
index eeda4ef2..620dc618 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -3,11 +3,11 @@ module Properties.Step where
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number)
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
-open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
+open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Value using (nil; addr; val)
+open import Luau.Value using (nil; addr; val; number)
 open import Properties.Remember using (remember; _,_)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@@ -30,9 +30,11 @@ stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
 stepᴱ H nil = value nil refl
 stepᴱ H (var x) = error (UnboundVariable x)
 stepᴱ H (addr a) = value (addr a) refl
+stepᴱ H (number x) = value (number x) refl
 stepᴱ H (M $ N) with stepᴱ H M
 stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
 stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
+stepᴱ H ((number _) $ N) | value (number x) refl = error (NumberIsNotAFunction x)
 stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
 stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
 stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
diff --git a/prototyping/Tests/PrettyPrinter/smoke_test/in.lua b/prototyping/Tests/PrettyPrinter/smoke_test/in.lua
index 0d23bbb2..d26e3a0d 100644
--- a/prototyping/Tests/PrettyPrinter/smoke_test/in.lua
+++ b/prototyping/Tests/PrettyPrinter/smoke_test/in.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 : number = 123
 return id2(nil2)
diff --git a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt
index e663534a..34e0c4fe 100644
--- a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt
+++ b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt
@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f : number = 123.0
 return id2(nil2)