From 6c923b88021df9dc902ed788933996cee556dc30 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Wed, 2 Mar 2022 15:26:58 -0800 Subject: [PATCH] Prototyping: strings (#390) --- .github/workflows/prototyping.yml | 3 +- prototyping/Examples/Run.agda | 5 ++- prototyping/Luau/OpSem.agda | 6 ++-- prototyping/Luau/RuntimeError.agda | 5 +-- prototyping/Luau/RuntimeError/ToString.agda | 4 ++- prototyping/Luau/RuntimeType.agda | 4 ++- prototyping/Luau/RuntimeType/ToString.agda | 3 +- prototyping/Luau/StrictMode.agda | 5 +-- prototyping/Luau/Syntax.agda | 3 ++ prototyping/Luau/Syntax/FromJSON.agda | 7 +++- prototyping/Luau/Syntax/ToString.agda | 5 ++- prototyping/Luau/Type.agda | 22 ++++++++++++ prototyping/Luau/Type/FromJSON.agda | 3 +- prototyping/Luau/Type/ToString.agda | 3 +- prototyping/Luau/TypeCheck.agda | 10 ++++-- prototyping/Properties/Step.agda | 36 +++++++++++++++++-- prototyping/Properties/StrictMode.agda | 14 +++++--- prototyping/Properties/TypeCheck.agda | 23 ++++++++---- .../concat_number_and_string/in.lua | 3 ++ .../concat_number_and_string/out.txt | 11 ++++++ .../Interpreter/concat_two_strings/in.lua | 3 ++ .../Interpreter/concat_two_strings/out.txt | 6 ++++ .../Tests/Interpreter/return_string/in.lua | 1 + .../Tests/Interpreter/return_string/out.txt | 4 +++ 24 files changed, 156 insertions(+), 33 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 create mode 100644 prototyping/Tests/Interpreter/return_string/in.lua create mode 100644 prototyping/Tests/Interpreter/return_string/out.txt diff --git a/.github/workflows/prototyping.yml b/.github/workflows/prototyping.yml index c92e5803..6bc8a81b 100644 --- a/.github/workflows/prototyping.yml +++ b/.github/workflows/prototyping.yml @@ -37,8 +37,7 @@ jobs: - name: check targets working-directory: prototyping run: | - ~/.cabal/bin/agda Examples.agda - ~/.cabal/bin/agda Properties.agda + ~/.cabal/bin/agda Everything.agda - name: build executables working-directory: prototyping run: | diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 545ecf51..84ebf84e 100644 --- a/prototyping/Examples/Run.agda +++ b/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 diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index cbb55978..1f616c7e 100644 --- a/prototyping/Luau/OpSem.agda +++ b/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 diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 4440d2b7..0c8a594b 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/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.RuntimeType using (RuntimeType; valueType; function; number) +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; 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 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/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda index f6b8b4a4..d585b51b 100644 --- a/prototyping/Luau/RuntimeType.agda +++ b/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 diff --git a/prototyping/Luau/RuntimeType/ToString.agda b/prototyping/Luau/RuntimeType/ToString.agda index dfb7c955..f3dd1255 100644 --- a/prototyping/Luau/RuntimeType/ToString.agda +++ b/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" diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index d7b2129f..08e0f50b 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/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.Type using (Type; strict; nil; number; _⇒_; tgt) +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; 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 diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 8be0830f..d9175067 100644 --- a/prototyping/Luau/Syntax.agda +++ b/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 diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index a727a5b0..2263615d 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/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" diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 60ec471d..1743071a 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/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 diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 10f39c44..c5b76142 100644 --- a/prototyping/Luau/Type.agda +++ b/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) diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda index 9057fef4..2d6ba689 100644 --- a/prototyping/Luau/Type/FromJSON.agda +++ b/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 diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index dec7c14c..2efe6632 100644 --- a/prototyping/Luau/Type/ToString.agda +++ b/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′ ++ "?" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index f240e17e..65ed1831 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/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 Γ} → diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 0b5fd062..cadd1530 100644 --- a/prototyping/Properties/Step.agda +++ b/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.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.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.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 + \ No newline at end of file diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 08411188..77852f1a 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/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 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 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.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) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index c144bc12..bec68841 100644 --- a/prototyping/Properties/TypeCheck.agda +++ 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.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.Type using (Type; nil; any; none; number; boolean; _⇒_; tgt) -open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType) +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; 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; string; _⇒_; tgt) +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) + \ No newline at end of file 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/in.lua b/prototyping/Tests/Interpreter/return_string/in.lua new file mode 100644 index 00000000..67febb75 --- /dev/null +++ b/prototyping/Tests/Interpreter/return_string/in.lua @@ -0,0 +1 @@ +return "foo bar" diff --git a/prototyping/Tests/Interpreter/return_string/out.txt b/prototyping/Tests/Interpreter/return_string/out.txt new file mode 100644 index 00000000..81915c77 --- /dev/null +++ b/prototyping/Tests/Interpreter/return_string/out.txt @@ -0,0 +1,4 @@ +ANNOTATED PROGRAM: +return "foo bar" + +RAN WITH RESULT: "foo bar"