From 48e93005719454edcc254ae6ac136b9514549a96 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Wed, 2 Mar 2022 14:56:10 -0800 Subject: [PATCH] add concat operator --- prototyping/Luau/OpSem.agda | 5 +++-- prototyping/Luau/RuntimeError.agda | 5 +++-- prototyping/Luau/StrictMode.agda | 5 +++-- prototyping/Luau/Syntax.agda | 1 + prototyping/Luau/Syntax/FromJSON.agda | 3 ++- prototyping/Luau/Syntax/ToString.agda | 3 ++- prototyping/Luau/TypeCheck.agda | 3 ++- prototyping/Properties/Step.agda | 17 ++++++++++++++--- prototyping/Properties/StrictMode.agda | 10 ++++++---- prototyping/Properties/TypeCheck.agda | 12 ++++++++++-- 10 files changed, 46 insertions(+), 18 deletions(-) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 4afbda89..1f616c7e 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -5,13 +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) +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 (_×_; _,_) @@ -38,6 +38,7 @@ 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/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 0d8ca97b..d9175067 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -46,6 +46,7 @@ data BinaryOperator : Set where ~= : BinaryOperator <= : BinaryOperator >= : BinaryOperator + ·· : BinaryOperator data Value : Set where nil : Value diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index b2fdccb4..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; +; -; *; /; ==; ~=; <; >; <=; >=; string) +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 diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 8862db5b..1743071a 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -3,7 +3,7 @@ module Luau.Syntax.ToString where open import Agda.Builtin.Bool using (true; false) open import Agda.Builtin.Float using (primShowFloat) 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 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) @@ -30,6 +30,7 @@ binOpToString == = "==" binOpToString ~= = "~=" binOpToString <= = "<=" binOpToString >= = ">=" +binOpToString ·· = ".." valueToString : Value → String valueToString nil = "nil" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index ab611374..65ed1831 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -6,7 +6,7 @@ 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; string; 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 _[_]ᴴ) @@ -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 diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 65d75eca..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; +; -; *; /; <; >; <=; >=; ==; ~=; 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.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; _,_) @@ -97,6 +98,15 @@ 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 @@ -159,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 8d1e9814..77852f1a 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -6,7 +6,7 @@ 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; 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; _≡ᵀ_; _≡ᴹᵀ_) @@ -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 @@ -155,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′) @@ -446,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 1e2c97b3..bec68841 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -11,7 +11,7 @@ open import FFI.Data.Either using (Either) 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; 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; _≡ⱽ_) @@ -63,7 +63,6 @@ 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) | () @@ -71,6 +70,14 @@ mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeO mustBeNumber H Γ (addr a) p | nothing , q | () mustBeNumber H Γ (number n) p = refl +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)) @@ -102,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