strings

prototyping/Luau/RuntimeType.agda

@@ -1,13 +1,15 @@
 module Luau.RuntimeType where
 
-open import Luau.Value using (Value; nil; addr; number)
+open import Luau.Value using (Value; nil; addr; number; string)
 
 data RuntimeType : Set where
   function : RuntimeType
   number : RuntimeType
   nil : RuntimeType
+  string : RuntimeType
 
 valueType : Value → RuntimeType
 valueType nil = nil
 valueType (addr x) = function
 valueType (number x) = number
+valueType (string x) = string

prototyping/Luau/RuntimeType/ToString.agda

@@ -1,9 +1,10 @@
 module Luau.RuntimeType.ToString where
 
 open import FFI.Data.String using (String)
-open import Luau.RuntimeType using (RuntimeType; function; number; nil)
+open import Luau.RuntimeType using (RuntimeType; function; number; nil; string)
 
 runtimeTypeToString : RuntimeType → String
 runtimeTypeToString function = "function"
 runtimeTypeToString number = "number"
 runtimeTypeToString nil = "nil"
+runtimeTypeToString string = "string"

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; number; binexp)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp; string)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -14,6 +14,7 @@ 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
+(string y) [ v / x ]ᴱ = string 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

prototyping/Luau/Syntax.agda

@@ -2,6 +2,7 @@ module Luau.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Float using (Float)
+open import Agda.Builtin.String using (String)
 open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
@@ -61,3 +62,4 @@ data Expr a where
   block_is_end : Var → Block a → Expr a
   number : Float → Expr a
   binexp : Expr a → BinaryOperator → Expr a → Expr a
+  string : String → 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; number; binexp; BinaryOperator; +; -; *; /)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /; string)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
@@ -103,6 +103,10 @@ 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 "AstExprConstantString") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantString") | just (string x) = Right (string x)
+exprFromObject obj | just (string "AstExprConstantString") | just _ = Left "AstExprConstantString value is not a string"
+exprFromObject obj | just (string "AstExprConstantString") | nothing = Left "AstExprConstantString missing value"
 exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
 exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
 exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o′ | Right l′ | Right r′ = Right (binexp l′ o′ r′)

prototyping/Luau/Syntax/ToString.agda

@@ -1,7 +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; BinaryOperator; +; -; *; /; binexp)
+open import Agda.Builtin.String using (primShowString)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; binexp; string)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -44,6 +45,7 @@ exprToString′ lb (block b is B end) =
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
 exprToString′ lb (number x) = primShowFloat x
+exprToString′ lb (string x) = primShowString x
 exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
 
 statToString′ lb (function F is B end) =

prototyping/Luau/Value.agda

@@ -1,16 +1,19 @@
 module Luau.Value where
 
 open import Agda.Builtin.Float using (Float)
+open import Agda.Builtin.String using (String)
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr; number)
+open import Luau.Syntax using (Block; Expr; nil; addr; number; string)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
   number : Float → Value
+  string : String → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
 val (number x) = number x
+val (string x) = string x

prototyping/Luau/Value/ToString.agda

@@ -1,11 +1,12 @@
 module Luau.Value.ToString where
 
-open import Agda.Builtin.String using (String)
+open import Agda.Builtin.String using (String; primShowString)
 open import Agda.Builtin.Float using (primShowFloat)
-open import Luau.Value using (Value; nil; addr; number)
+open import Luau.Value using (Value; nil; addr; number; string)
 open import Luau.Addr.ToString using (addrToString)
 
 valueToString : Value → String
 valueToString nil = "nil"
 valueToString (addr a) = addrToString a
 valueToString (number x) = primShowFloat x
+valueToString (string x) = primShowString x

prototyping/Properties/Step.agda

@@ -4,12 +4,12 @@ open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
 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; number; binexp; +)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; string)
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpEval; evalBinOp; binOp₁; binOp₂)
 open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
 open import Luau.RuntimeType using (function; number)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Value using (nil; addr; val; number)
+open import Luau.Value using (nil; addr; val; number; string)
 open import Properties.Remember using (remember; _,_)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@@ -33,12 +33,14 @@ 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 (string x) = value (string 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 (_ $ N) | value V refl with stepᴱ H N
 stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s)
 stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
 stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
+stepᴱ H (_ $ _) | value (string x) refl | value W refl = error (app₁ (TypeMismatch function (string x) λ()))
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (nothing , p) = error (app₁ (SEGV a p))
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
@@ -60,6 +62,8 @@ stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch num
 stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
 stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
 stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
+stepᴱ H (binexp x op y) | value (string x′) refl | _ = error (bin₁ (TypeMismatch number (string x′) λ()))
+stepᴱ H (binexp x op y) | _ | value (string x′) refl = error (bin₂ (TypeMismatch number (string x′) λ()))
 stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s)
 stepᴱ H (binexp x op y) | error E = error (bin₁ E)
 

prototyping/Tests/Interpreter/return_string/in.lua

@@ -0,0 +1 @@
+return "foo bar"

prototyping/Tests/Interpreter/return_string/out.txt

@@ -0,0 +1 @@
+"foo bar"