From bb7af77ff30c5a040a998edc4a4b27f4e5190c51 Mon Sep 17 00:00:00 2001
From: Lily Brown <lbrown@roblox.com>
Date: Wed, 2 Mar 2022 15:03:19 -0800
Subject: [PATCH] test concat

---
 prototyping/Luau/RuntimeError/ToString.agda           |  4 +++-
 .../Tests/Interpreter/concat_number_and_string/in.lua |  3 +++
 .../Interpreter/concat_number_and_string/out.txt      | 11 +++++++++++
 .../Tests/Interpreter/concat_two_strings/in.lua       |  3 +++
 .../Tests/Interpreter/concat_two_strings/out.txt      |  6 ++++++
 prototyping/Tests/Interpreter/return_string/out.txt   |  5 ++++-
 6 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 prototyping/Tests/Interpreter/concat_number_and_string/in.lua
 create mode 100644 prototyping/Tests/Interpreter/concat_number_and_string/out.txt
 create mode 100644 prototyping/Tests/Interpreter/concat_two_strings/in.lua
 create mode 100644 prototyping/Tests/Interpreter/concat_two_strings/out.txt

diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda
index 6a6ed3e2..cd5f18f2 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -9,7 +9,7 @@ open import Luau.RuntimeType.ToString using (runtimeTypeToString)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Syntax.ToString using (valueToString; exprToString)
 open import Luau.Var.ToString using (varToString)
-open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_)
+open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_; ··)
 
 errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String
 errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String
@@ -19,6 +19,8 @@ errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is un
 errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
 errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
 errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
+errToStringᴱ (binexp M ·· N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a string"
+errToStringᴱ (binexp M ·· N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a string"
 errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
 errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
 errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
diff --git a/prototyping/Tests/Interpreter/concat_number_and_string/in.lua b/prototyping/Tests/Interpreter/concat_number_and_string/in.lua
new file mode 100644
index 00000000..ba5acb32
--- /dev/null
+++ b/prototyping/Tests/Interpreter/concat_number_and_string/in.lua
@@ -0,0 +1,3 @@
+local x: string = "hello"
+local y: string = 37
+return x .. y
diff --git a/prototyping/Tests/Interpreter/concat_number_and_string/out.txt b/prototyping/Tests/Interpreter/concat_number_and_string/out.txt
new file mode 100644
index 00000000..a437438d
--- /dev/null
+++ b/prototyping/Tests/Interpreter/concat_number_and_string/out.txt
@@ -0,0 +1,11 @@
+ANNOTATED PROGRAM:
+local x : string = "hello"
+local y : string = 37.0
+return x .. y
+
+RUNTIME ERROR:
+value 37.0 is not a string
+  in return statement
+
+TYPE ERROR:
+Local variable y has type string but expression has type number
diff --git a/prototyping/Tests/Interpreter/concat_two_strings/in.lua b/prototyping/Tests/Interpreter/concat_two_strings/in.lua
new file mode 100644
index 00000000..c6ccdce6
--- /dev/null
+++ b/prototyping/Tests/Interpreter/concat_two_strings/in.lua
@@ -0,0 +1,3 @@
+local x: string = "hello"
+local y: string = "world"
+return x .. y
diff --git a/prototyping/Tests/Interpreter/concat_two_strings/out.txt b/prototyping/Tests/Interpreter/concat_two_strings/out.txt
new file mode 100644
index 00000000..d45f589f
--- /dev/null
+++ b/prototyping/Tests/Interpreter/concat_two_strings/out.txt
@@ -0,0 +1,6 @@
+ANNOTATED PROGRAM:
+local x : string = "hello"
+local y : string = "world"
+return x .. y
+
+RAN WITH RESULT: "helloworld"
diff --git a/prototyping/Tests/Interpreter/return_string/out.txt b/prototyping/Tests/Interpreter/return_string/out.txt
index c6d2990e..81915c77 100644
--- a/prototyping/Tests/Interpreter/return_string/out.txt
+++ b/prototyping/Tests/Interpreter/return_string/out.txt
@@ -1 +1,4 @@
-"foo bar"
+ANNOTATED PROGRAM:
+return "foo bar"
+
+RAN WITH RESULT: "foo bar"