test concat

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

prototyping/Tests/Interpreter/concat_number_and_string/in.lua

@@ -0,0 +1,3 @@
+local x: string = "hello"
+local y: string = 37
+return x .. y

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

prototyping/Tests/Interpreter/concat_two_strings/in.lua

@@ -0,0 +1,3 @@
+local x: string = "hello"
+local y: string = "world"
+return x .. y

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"

prototyping/Tests/Interpreter/return_string/out.txt

@@ -1 +1,4 @@
-"foo bar"
+ANNOTATED PROGRAM:
+return "foo bar"
+
+RAN WITH RESULT: "foo bar"