From f765d144caf7dc9593a15b28180f805acec9101a Mon Sep 17 00:00:00 2001
From: Lily Brown <lbrown@roblox.com>
Date: Wed, 16 Feb 2022 11:47:51 -0800
Subject: [PATCH] numbers work

---
 prototyping/.gitignore                      | 2 ++
 prototyping/Examples/OpSem.agda             | 1 -
 prototyping/Examples/Run.agda               | 7 +++++--
 prototyping/FFI/Data/Scientific.agda        | 3 +++
 prototyping/Luau/RuntimeError.agda          | 4 ++--
 prototyping/Luau/RuntimeError/ToString.agda | 8 +++++---
 prototyping/Luau/Substitution.agda          | 4 ++--
 prototyping/Luau/Syntax.agda                | 4 ++--
 prototyping/Luau/Syntax/FromJSON.agda       | 3 ++-
 prototyping/Luau/Syntax/ToString.agda       | 4 ++--
 prototyping/Luau/Value.agda                 | 4 ++--
 prototyping/Luau/Value/ToString.agda        | 4 ++--
 prototyping/Properties/Step.agda            | 8 +++++---
 13 files changed, 34 insertions(+), 22 deletions(-)

diff --git a/prototyping/.gitignore b/prototyping/.gitignore
index cca4f464..ae412818 100644
--- a/prototyping/.gitignore
+++ b/prototyping/.gitignore
@@ -4,3 +4,5 @@ Main
 MAlonzo
 PrettyPrinter
 .ghc.*
+Interpreter
+Examples
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..5818ee0c 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 (Luau.Syntax.Expr.number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (Luau.Value.Value.number 123.0) _)
+ex2 = refl
diff --git a/prototyping/FFI/Data/Scientific.agda b/prototyping/FFI/Data/Scientific.agda
index 50388781..772d3367 100644
--- a/prototyping/FFI/Data/Scientific.agda
+++ b/prototyping/FFI/Data/Scientific.agda
@@ -1,5 +1,6 @@
 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)
 
@@ -11,8 +12,10 @@ postulate Scientific : Set
 
 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/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index e514dc9d..17ff7930 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -3,13 +3,14 @@ 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 FFI.Data.String using (String)
 open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
 
 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)
+  ValueNotCallable : ∀ x → RuntimeErrorᴱ H x
   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 +19,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..9ebec69b 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -1,15 +1,17 @@
 module Luau.RuntimeError.ToString where
 
 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; ValueNotCallable; 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ᴱ (ValueNotCallable (x $ _)) = "value " ++ exprToString x ++ " is not callable"
+errToStringᴱ (ValueNotCallable x) = "value " ++ exprToString x ++ " is not callable"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
 errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app E) = errToStringᴱ E
diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda
index b956aeae..f8092c8a 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 bdea974a..a1898a92 100644
--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@@ -1,11 +1,11 @@
 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)
 open import Luau.Type using (Type)
-open import FFI.Data.Scientific using (Scientific)
 
 infixr 5 _∙_
 
@@ -53,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
+  number_ : Float → Expr a
diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda
index 6e7dfcd6..94beec75 100644
--- a/prototyping/Luau/Syntax/FromJSON.agda
+++ b/prototyping/Luau/Syntax/FromJSON.agda
@@ -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)
 
@@ -85,7 +86,7 @@ exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right
 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 (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)
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 0d928bc4..cd4f9702 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -1,8 +1,8 @@
 module Luau.Syntax.ToString where
 
+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 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)
@@ -37,7 +37,7 @@ exprToString′ lb (block b is B end) =
   "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
-exprToString′ lb (number x) = show x
+exprToString′ lb (number x) = primShowFloat x
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++
diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda
index 721ace67..7453d323 100644
--- a/prototyping/Luau/Value.agda
+++ b/prototyping/Luau/Value.agda
@@ -1,6 +1,6 @@
 module Luau.Value where
 
-open import FFI.Data.Scientific using (Scientific)
+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.Var using (Var)
@@ -8,7 +8,7 @@ open import Luau.Var using (Var)
 data Value : Set where
   nil : Value
   addr : Addr → Value
-  number : Scientific → Value
+  number : Float → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda
index 4ff38f7d..51c3fa78 100644
--- a/prototyping/Luau/Value/ToString.agda
+++ b/prototyping/Luau/Value/ToString.agda
@@ -1,11 +1,11 @@
 module Luau.Value.ToString where
 
 open import Agda.Builtin.String using (String)
-open import FFI.Data.Scientific using (show)
+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) = show x
+valueToString (number x) = primShowFloat x
diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda
index eeda4ef2..e42a30a9 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -3,9 +3,9 @@ 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ᴮ; ValueNotCallable; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val)
 open import Properties.Remember using (remember; _,_)
@@ -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 (Luau.Value.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 (nil $ N) | value nil refl = error (ValueNotCallable (nil $ N))
+stepᴱ H ((number _) $ N) | value (Luau.Value.Value.number x) refl = error (ValueNotCallable ((number x) $ N))
 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)