Prototyping: strings (#390)

.github/workflows/prototyping.yml

@@ -37,8 +37,7 @@ jobs:
     - name: check targets
       working-directory: prototyping
       run: |
-        ~/.cabal/bin/agda Examples.agda
+        ~/.cabal/bin/agda Everything.agda
-        ~/.cabal/bin/agda Properties.agda
     - name: build executables
       working-directory: prototyping
       run: |

prototyping/Examples/Run.agda

@@ -4,7 +4,7 @@ module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Bool using (true; false)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool; ~=; string)
 open import Luau.Run using (run; return)
 
 ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ val nil) ∙ done) ≡ return nil _)
@@ -18,3 +18,6 @@ ex3 = refl
 
 ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) < (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _)
 ex4 = refl
+
+ex5 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (string "foo")) ~= (val (string "bar"))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _)
+ex5 = refl

prototyping/Luau/OpSem.agda

@@ -5,12 +5,13 @@ module Luau.OpSem where
 open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
 open import Agda.Builtin.Bool using (Bool; true; false)
+open import Agda.Builtin.String using (primStringEquality; primStringAppend)
 open import Utility.Bool using (not; _or_; _and_)
 open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; number; bool)
+open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; number; bool; string)
 open import Luau.RuntimeType using (RuntimeType; valueType)
 open import Properties.Product using (_×_; _,_)
 
@@ -37,7 +38,8 @@ data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
   >= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
   == : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
   ~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
-  
+  ·· : ∀ x y → (string x) ⟦ ·· ⟧ (string y) ⟶ string (primStringAppend x y)
+
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
 

prototyping/Luau/RuntimeError.agda

@@ -6,8 +6,8 @@ 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 (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp; +; -; *; /; <; >; <=; >=)
+open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; string; binexp; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.RuntimeType using (RuntimeType; valueType; function; number)
+open import Luau.RuntimeType using (RuntimeType; valueType; function; number; string)
 open import Properties.Equality using (_≢_)
 
 data BinOpError : BinaryOperator → RuntimeType → Set where
@@ -19,6 +19,7 @@ data BinOpError : BinaryOperator → RuntimeType → Set where
   > : ∀ {t} → (t ≢ number) → BinOpError > t
   <= : ∀ {t} → (t ≢ number) → BinOpError <= t
   >= : ∀ {t} → (t ≢ number) → BinOpError >= t
+  ·· : ∀ {t} → (t ≢ string) → BinOpError ·· t
   
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set

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/Luau/RuntimeType.agda

@@ -1,15 +1,17 @@
 module Luau.RuntimeType where
 
-open import Luau.Syntax using (Value; nil; addr; number; bool)
+open import Luau.Syntax using (Value; nil; addr; number; bool; string)
 
 data RuntimeType : Set where
   function : RuntimeType
   number : RuntimeType
   nil : RuntimeType
   boolean : RuntimeType
+  string : RuntimeType
 
 valueType : Value → RuntimeType
 valueType nil = nil
 valueType (addr a) = function
 valueType (number n) = number
 valueType (bool b) = boolean
+valueType (string x) = string

prototyping/Luau/RuntimeType/ToString.agda

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

prototyping/Luau/StrictMode.agda

@@ -4,8 +4,8 @@ module Luau.StrictMode where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=)
+open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; strict; nil; number; _⇒_; tgt)
+open import Luau.Type using (Type; strict; nil; number; string; _⇒_; tgt)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
@@ -25,6 +25,7 @@ data BinOpWarning : BinaryOperator → Type → Set where
   > : ∀ {T} → (T ≢ number) → BinOpWarning > T
   <= : ∀ {T} → (T ≢ number) → BinOpWarning <= T
   >= : ∀ {T} → (T ≢ number) → BinOpWarning >= T
+  ·· : ∀ {T} → (T ≢ string) → BinOpWarning ·· T
 
 data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
 data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set

prototyping/Luau/Syntax.agda

@@ -3,6 +3,7 @@ module Luau.Syntax where
 open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Bool using (Bool; true; false)
 open import Agda.Builtin.Float using (Float)
+open import Agda.Builtin.String using (String)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Type using (Type)
@@ -45,12 +46,14 @@ data BinaryOperator : Set where
   ~= : BinaryOperator
   <= : BinaryOperator
   >= : BinaryOperator
+  ·· : BinaryOperator
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
   number : Float → Value
   bool : Bool → Value
+  string : String → Value
 
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set

prototyping/Luau/Syntax/FromJSON.agda

@@ -2,7 +2,7 @@
 
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec;  binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=)
+open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec;  binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=; ··; string)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
@@ -65,6 +65,7 @@ binOpFromString "CompareLt" = Right <
 binOpFromString "CompareLe" = Right <=
 binOpFromString "CompareGt" = Right >
 binOpFromString "CompareGe" = Right >=
+binOpFromString "Concat" = Right ··
 binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
 
 varDecFromJSON (object arg) = varDecFromObject arg
@@ -122,6 +123,10 @@ exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
 exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (val (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 (val (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 "AstExprConstantBool") with lookup value obj
 exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool b) = Right (val (bool b))
 exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"

prototyping/Luau/Syntax/ToString.agda

@@ -2,7 +2,8 @@ module Luau.Syntax.ToString where
 
 open import Agda.Builtin.Bool using (true; false)
 open import Agda.Builtin.Float using (primShowFloat)
-open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; 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 (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; 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)
@@ -29,6 +30,7 @@ binOpToString == = "=="
 binOpToString ~= = "~="
 binOpToString <= = "<="
 binOpToString >= = ">="
+binOpToString ·· = ".."
 
 valueToString : Value → String
 valueToString nil = "nil"
@@ -36,6 +38,7 @@ valueToString (addr a) = addrToString a
 valueToString (number x) = primShowFloat x
 valueToString (bool false) = "false"
 valueToString (bool true) = "true"
+valueToString (string x) = primShowString x
 
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String

prototyping/Luau/Type.agda

@@ -13,6 +13,7 @@ data Type : Set where
   any : Type
   boolean : Type
   number : Type
+  string : Type
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
@@ -25,6 +26,7 @@ lhs none = none
 lhs any = any
 lhs number = number
 lhs boolean = boolean
+lhs string = string
 
 rhs : Type → Type
 rhs (_ ⇒ T) = T
@@ -35,6 +37,7 @@ rhs none = none
 rhs any = any
 rhs number = number
 rhs boolean = boolean
+rhs string = string
 
 _≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
 nil ≡ᵀ nil = yes refl
@@ -45,6 +48,14 @@ nil ≡ᵀ number = no (λ ())
 nil ≡ᵀ boolean = no (λ ())
 nil ≡ᵀ (S ∪ T) = no (λ ())
 nil ≡ᵀ (S ∩ T) = no (λ ())
+nil ≡ᵀ string = no (λ ())
+(S ⇒ T) ≡ᵀ string = no (λ ())
+none ≡ᵀ string = no (λ ())
+any ≡ᵀ string = no (λ ())
+boolean ≡ᵀ string = no (λ ())
+number ≡ᵀ string = no (λ ())
+(S ∪ T) ≡ᵀ string = no (λ ())
+(S ∩ T) ≡ᵀ string = no (λ ())
 (S ⇒ T) ≡ᵀ nil = no (λ ())
 (S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V) 
 (S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
@@ -88,6 +99,15 @@ boolean ≡ᵀ boolean = yes refl
 boolean ≡ᵀ number = no (λ ())
 boolean ≡ᵀ (T ∪ U) = no (λ ())
 boolean ≡ᵀ (T ∩ U) = no (λ ())
+string ≡ᵀ nil = no (λ ())
+string ≡ᵀ (x ⇒ x₁) = no (λ ())
+string ≡ᵀ none = no (λ ())
+string ≡ᵀ any = no (λ ())
+string ≡ᵀ boolean = no (λ ())
+string ≡ᵀ number = no (λ ())
+string ≡ᵀ string = yes refl
+string ≡ᵀ (U ∪ V) = no (λ ())
+string ≡ᵀ (U ∩ V) = no (λ ())
 (S ∪ T) ≡ᵀ nil = no (λ ())
 (S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
 (S ∪ T) ≡ᵀ none = no (λ ())
@@ -127,6 +147,7 @@ src : Mode → Type → Type
 src m nil = none
 src m number = none
 src m boolean = none
+src m string = none
 src m (S ⇒ T) = S
 -- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant
 src strict    (S ∪ T) = (src strict S) ∩ (src strict T)
@@ -145,6 +166,7 @@ tgt none = none
 tgt any = any
 tgt number = none
 tgt boolean = none
+tgt string = none
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
 

prototyping/Luau/Type/FromJSON.agda

@@ -2,7 +2,7 @@
 
 module Luau.Type.FromJSON where
 
-open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number; string)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 open import Agda.Builtin.Bool using (true; false)
@@ -44,6 +44,7 @@ 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") | just (string "string") = Right string
 typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
 
 typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o

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; number; boolean; _∪_; _∩_; normalizeOptional)
+open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; string; _∪_; _∩_; normalizeOptional)
 
 {-# TERMINATING #-}
 typeToString : Type → String
@@ -14,6 +14,7 @@ typeToString none = "none"
 typeToString any = "any"
 typeToString number = "number"
 typeToString boolean = "boolean"
+typeToString string = "string"
 typeToString (S ∪ T) with normalizeOptional(S ∪ T)
 typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
 typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"

prototyping/Luau/TypeCheck.agda

@@ -6,11 +6,11 @@ module Luau.TypeCheck (m : Mode) where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (Maybe; just)
-open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=)
+open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Type using (Type; Mode; nil; none; number; boolean; _⇒_; tgt)
+open import Luau.Type using (Type; Mode; nil; none; number; boolean; string; _⇒_; tgt)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
@@ -34,6 +34,7 @@ tgtBinOp == = boolean
 tgtBinOp ~= = boolean
 tgtBinOp <= = boolean
 tgtBinOp >= = boolean
+tgtBinOp ·· = string
 
 data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
 data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set
@@ -93,6 +94,11 @@ data _⊢ᴱ_∈_ where
 
     --------------------------
     Γ ⊢ᴱ val(bool b) ∈ boolean
+  
+  string : ∀ {x Γ} →
+
+    ---------------------------
+    Γ ⊢ᴱ val(string x) ∈ string
 
   app : ∀ {M N T U Γ} →
 

prototyping/Properties/Step.agda

@@ -5,11 +5,12 @@ module Properties.Step where
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess)
 open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.String using (primStringAppend)
 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; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=)
+open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; 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; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp; evalNeqOp)
+open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; ··; evalEqOp; evalNeqOp)
-open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=)
+open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=; ··)
 open import Luau.RuntimeType using (valueType; function; number)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Properties.Remember using (remember; _,_)
@@ -27,6 +28,16 @@ binOpStep (number m) + nil = error₂ (+ (λ ()))
 binOpStep (number m) + (addr a) = error₂ (+ (λ ()))
 binOpStep (number m) + (number n) = step (number (primFloatPlus m n)) (+ m n)
 binOpStep (number m) + (bool b) = error₂ (+ (λ ()))
+binOpStep (number m) + (string x) = error₂ (+ (λ ()))
+binOpStep (number m) - (string x) = error₂ (- (λ ()))
+binOpStep (number m) * (string x) = error₂ (* (λ ()))
+binOpStep (number m) / (string x) = error₂ (/ (λ ()))
+binOpStep (number m) < (string x) = error₂ (< (λ ()))
+binOpStep (number m) > (string x) = error₂ (> (λ ()))
+binOpStep (number m) == (string x) = step (bool false) (== (number m) (string x))
+binOpStep (number m) ~= (string x) = step (bool true) (~= (number m) (string x))
+binOpStep (number m) <= (string x) = error₂ (<= (λ ()))
+binOpStep (number m) >= (string x) = error₂ (>= (λ ()))
 binOpStep (bool b) + w = error₁ (+ (λ ()))
 binOpStep nil - w = error₁ (- (λ ()))
 binOpStep (addr a) - w = error₁ (- (λ ()))
@@ -79,6 +90,23 @@ binOpStep (number m) >= (addr a) = error₂ (>= (λ ()))
 binOpStep (number m) >= (number n) = step (bool (primFloatLess n m or primFloatEquality m n)) (>= m n)
 binOpStep (number m) >= (bool b) = error₂ (>= (λ ()))
 binOpStep (bool b) >= w = error₁ (>= (λ ()))
+binOpStep (string x) + w = error₁ (+ (λ ()))
+binOpStep (string x) - w = error₁ (- (λ ()))
+binOpStep (string x) * w = error₁ (* (λ ()))
+binOpStep (string x) / w = error₁ (/ (λ ()))
+binOpStep (string x) < w = error₁ (< (λ ()))
+binOpStep (string x) > w = error₁ (> (λ ()))
+binOpStep (string x) <= w = error₁ (<= (λ ()))
+binOpStep (string x) >= w = error₁ (>= (λ ()))
+binOpStep nil ·· y = error₁ (·· (λ ()))
+binOpStep (addr x) ·· y = error₁ (BinOpError.·· (λ ()))
+binOpStep (number x) ·· y = error₁ (BinOpError.·· (λ ()))
+binOpStep (bool x) ·· y = error₁ (BinOpError.·· (λ ()))
+binOpStep (string x) ·· nil = error₂ (·· (λ ()))
+binOpStep (string x) ·· (addr y) = error₂ (·· (λ ()))
+binOpStep (string x) ·· (number y) = error₂ (·· (λ ()))
+binOpStep (string x) ·· (bool y) = error₂ (·· (λ ()))
+binOpStep (string x) ·· (string y) = step (string (primStringAppend x y)) (·· x y)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
 data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
@@ -109,6 +137,7 @@ stepᴱ H (_ $ _) | value (addr a) refl | value w refl  | (just(function F is B
 stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ()))
 stepᴱ H (_ $ _) | value (number m) refl | value w refl = error (FunctionMismatch (number m) w (λ ()))
 stepᴱ H (_ $ _) | value (bool b) refl | value w refl = error (FunctionMismatch (bool b) w (λ ()))
+stepᴱ H (_ $ _) | value (string x) refl | value w refl = error (FunctionMismatch (string x) w (λ ()))
 stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
 stepᴱ H (M $ N) | error E = error (app₁ E)
 stepᴱ H (block b is B end) with stepᴮ H B
@@ -140,3 +169,4 @@ stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (r
 stepᴮ H (return _ ∙ B) | value V refl = return V refl
 stepᴮ H (return M ∙ B) | error E = error (return E)
 stepᴮ H done = done refl
+ 

prototyping/Properties/StrictMode.agda

@@ -6,9 +6,9 @@ import Agda.Builtin.Equality.Rewrite
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
-open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=)
+open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=; ··)
 open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
-open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
+open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
 open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
 open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
 open import Luau.Var using (_≡ⱽ_)
@@ -19,9 +19,9 @@ open import Properties.Remember using (remember; _,_)
 open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
 open import Properties.Contradiction using (CONTRADICTION)
-open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber)
+open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber; mustBeString)
-open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=)
+open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
-open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=)
+open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
 open import Luau.RuntimeType using (valueType)
 
 src = Luau.Type.src strict
@@ -86,6 +86,7 @@ heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (Una
 heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
 heap-weakeningᴱ H (val (number n)) h = ok refl
 heap-weakeningᴱ H (val (bool b)) h = ok refl
+heap-weakeningᴱ H (val (string x)) h = ok refl
 heap-weakeningᴱ H (binexp M op N) h = ok refl
 heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
 heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
@@ -110,6 +111,7 @@ typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)
 typeOf-val-not-none nil = ok (λ ())
 typeOf-val-not-none (number n) = ok (λ ())
 typeOf-val-not-none (bool b) = ok (λ ())
+typeOf-val-not-none (string x) = ok (λ ())
 typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
 typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
 typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)
@@ -153,6 +155,7 @@ binOpPreservation H (<= m n) = refl
 binOpPreservation H (>= m n) = refl
 binOpPreservation H (== v w) = refl
 binOpPreservation H (~= v w) = refl
+binOpPreservation H (·· v w) = refl
 
 preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
 preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)
@@ -444,6 +447,7 @@ runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q))
 runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q))
 runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q))
 runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q))
+runtimeBinOpWarning H v (·· p) = ·· (λ q → p (mustBeString H ∅ v q))
 
 runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
 runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)

prototyping/Properties/TypeCheck.agda

@@ -8,10 +8,10 @@ open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Bool using (Bool; true; false)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import FFI.Data.Either using (Either)
-open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
+open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
-open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
+open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
-open import Luau.Type using (Type; nil; any; none; number; boolean; _⇒_; tgt)
+open import Luau.Type using (Type; nil; any; none; number; boolean; string; _⇒_; tgt)
-open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType)
+open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
 open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import Luau.Addr using (Addr)
 open import Luau.Var using (Var; _≡ⱽ_)
@@ -37,6 +37,7 @@ typeOfⱽ H nil = just nil
 typeOfⱽ H (bool b) = just boolean
 typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ)
 typeOfⱽ H (number n) = just number
+typeOfⱽ H (string x) = just string
 
 typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
 typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
@@ -59,17 +60,23 @@ mustBeFunction H Γ (addr a) p = refl
 mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
 mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
 mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
+mustBeFunction H Γ (string x) p = CONTRADICTION (p refl)
 
 mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
-mustBeNumber H Γ nil ()
 mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
 mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
 mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
 mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
 mustBeNumber H Γ (addr a) p | nothing , q | ()
 mustBeNumber H Γ (number n) p = refl
-mustBeNumber H Γ (bool true) ()
+
-mustBeNumber H Γ (bool false) ()
+mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string)
+mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ)
+mustBeString H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
+mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeString H Γ (addr a) p | (nothing , q) | ()
+mustBeString H Γ (string x) p = refl
 
 typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
 typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))
@@ -79,6 +86,7 @@ typeCheckᴱ H Γ (val nil) = nil
 typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
 typeCheckᴱ H Γ (val (number n)) = number
 typeCheckᴱ H Γ (val (bool b)) = bool
+typeCheckᴱ H Γ (val (string x)) = string
 typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
 typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
 typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B)
@@ -101,3 +109,4 @@ typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)
 
 typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M)
 typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)
+ 

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/in.lua

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

prototyping/Tests/Interpreter/return_string/out.txt

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