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..ab611374 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) @@ -93,6 +93,11 @@ data _⊢ᴱ_∈_ where -------------------------- Γ ⊢ᴱ val(bool b) ∈ boolean + + string : ∀ {x Γ} → + + --------------------------- + Γ ⊢ᴱ val(string x) ∈ string app : ∀ {M N T U Γ} → diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 08411188..8d1e9814 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -8,7 +8,7 @@ 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.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 (_≡ⱽ_) @@ -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) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index c144bc12..1e2c97b3 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -8,9 +8,9 @@ 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.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.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) @@ -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,6 +60,7 @@ 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 () @@ -68,8 +70,6 @@ mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B en 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) () typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M)) typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) @@ -79,6 +79,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)