From ffff25a9e502df4555c3bb30feb5f3625fd7d135 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Thu, 7 Apr 2022 09:16:44 -0700 Subject: [PATCH 1/4] Improve the UX of reading tagged unions a smidge. (#449) The page is a little narrow, and having to scroll on this horizontally isn't too nice. This fixes the UX for this specific part. --- docs/_pages/typecheck.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/_pages/typecheck.md b/docs/_pages/typecheck.md index 20f73987..63e4c8bb 100644 --- a/docs/_pages/typecheck.md +++ b/docs/_pages/typecheck.md @@ -392,18 +392,20 @@ local account: Account = Account.new("Alexander", 500) Tagged unions are just union types! In particular, they're union types of tables where they have at least _some_ common properties but the structure of the tables are different enough. Here's one example: ```lua -type Result = { type: "ok", value: T } | { type: "err", error: E } +type Ok = { type: "ok", value: T } +type Err = { type: "err", error: E } +type Result = Ok | Err ``` This `Result` type can be discriminated by using type refinements on the property `type`, like so: ```lua if result.type == "ok" then - -- result is known to be { type: "ok", value: T } + -- result is known to be Ok -- and attempting to index for error here will fail print(result.value) elseif result.type == "err" then - -- result is known to be { type: "err", error: E } + -- result is known to be Err -- and attempting to index for value here will fail print(result.error) end From de1381e3f131f2c307f68033ea494d1c35f2c3ca Mon Sep 17 00:00:00 2001 From: Arseny Kapoulkine Date: Thu, 7 Apr 2022 14:29:01 -0700 Subject: [PATCH 2/4] Sync to upstream/release/522 (#450) --- Analysis/include/Luau/Clone.h | 25 ++ Analysis/include/Luau/Frontend.h | 23 +- Analysis/include/Luau/Module.h | 29 +- Analysis/include/Luau/TypeInfer.h | 10 + Analysis/include/Luau/TypeVar.h | 2 + Analysis/include/Luau/Variant.h | 36 +- Analysis/src/Autocomplete.cpp | 117 +++++- Analysis/src/Clone.cpp | 371 ++++++++++++++++++ Analysis/src/Error.cpp | 1 + Analysis/src/Frontend.cpp | 144 +++++-- Analysis/src/IostreamHelpers.cpp | 419 +++++++++------------ Analysis/src/Module.cpp | 359 +----------------- Analysis/src/TxnLog.cpp | 31 +- Analysis/src/TypeInfer.cpp | 156 +++++--- Analysis/src/TypeVar.cpp | 4 + Ast/include/Luau/TimeTrace.h | 11 +- Ast/src/Parser.cpp | 11 + Ast/src/TimeTrace.cpp | 19 +- Compiler/src/ConstantFolding.cpp | 3 +- Sources.cmake | 2 + VM/src/lfunc.h | 2 +- VM/src/ltablib.cpp | 2 +- tests/Autocomplete.test.cpp | 139 ++++++- tests/Compiler.test.cpp | 33 ++ tests/Fixture.cpp | 5 +- tests/Fixture.h | 2 +- tests/Frontend.test.cpp | 64 ++++ tests/Module.test.cpp | 1 + tests/Parser.test.cpp | 21 ++ tests/TypeInfer.functions.test.cpp | 39 +- tests/TypeInfer.intersectionTypes.test.cpp | 39 +- tests/TypeInfer.primitives.test.cpp | 2 + tests/TypeInfer.tables.test.cpp | 15 + tests/TypeInfer.tryUnify.test.cpp | 26 ++ tests/TypeInfer.unionTypes.test.cpp | 25 ++ tools/lldb_formatters.py | 4 +- 36 files changed, 1407 insertions(+), 785 deletions(-) create mode 100644 Analysis/include/Luau/Clone.h create mode 100644 Analysis/src/Clone.cpp diff --git a/Analysis/include/Luau/Clone.h b/Analysis/include/Luau/Clone.h new file mode 100644 index 00000000..917ef801 --- /dev/null +++ b/Analysis/include/Luau/Clone.h @@ -0,0 +1,25 @@ +// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details +#pragma once + +#include "Luau/TypeVar.h" + +#include + +namespace Luau +{ + +// Only exposed so they can be unit tested. +using SeenTypes = std::unordered_map; +using SeenTypePacks = std::unordered_map; + +struct CloneState +{ + int recursionCount = 0; + bool encounteredFreeType = false; +}; + +TypePackId clone(TypePackId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); +TypeId clone(TypeId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); +TypeFun clone(const TypeFun& typeFun, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); + +} // namespace Luau diff --git a/Analysis/include/Luau/Frontend.h b/Analysis/include/Luau/Frontend.h index 0bf8f362..2266f548 100644 --- a/Analysis/include/Luau/Frontend.h +++ b/Analysis/include/Luau/Frontend.h @@ -12,6 +12,8 @@ #include #include +LUAU_FASTFLAG(LuauSeparateTypechecks) + namespace Luau { @@ -55,10 +57,19 @@ std::optional pathExprToModuleName(const ModuleName& currentModuleNa struct SourceNode { + bool isDirty(bool forAutocomplete) const + { + if (FFlag::LuauSeparateTypechecks) + return forAutocomplete ? dirtyAutocomplete : dirty; + else + return dirty; + } + ModuleName name; std::unordered_set requires; std::vector> requireLocations; bool dirty = true; + bool dirtyAutocomplete = true; }; struct FrontendOptions @@ -71,12 +82,16 @@ struct FrontendOptions // When true, we run typechecking twice, once in the regular mode, and once in strict mode // in order to get more precise type information (e.g. for autocomplete). - bool typecheckTwice = false; + bool typecheckTwice_DEPRECATED = false; + + // Run typechecking only in mode required for autocomplete (strict mode in order to get more precise type information) + bool forAutocomplete = false; }; struct CheckResult { std::vector errors; + std::vector timeoutHits; }; struct FrontendModuleResolver : ModuleResolver @@ -123,7 +138,7 @@ struct Frontend CheckResult check(const SourceModule& module); // OLD. TODO KILL LintResult lint(const SourceModule& module, std::optional enabledLintWarnings = {}); - bool isDirty(const ModuleName& name) const; + bool isDirty(const ModuleName& name, bool forAutocomplete = false) const; void markDirty(const ModuleName& name, std::vector* markedDirty = nullptr); /** Borrow a pointer into the SourceModule cache. @@ -147,10 +162,10 @@ struct Frontend void applyBuiltinDefinitionToEnvironment(const std::string& environmentName, const std::string& definitionName); private: - std::pair getSourceNode(CheckResult& checkResult, const ModuleName& name); + std::pair getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete); SourceModule parse(const ModuleName& name, std::string_view src, const ParseOptions& parseOptions); - bool parseGraph(std::vector& buildQueue, CheckResult& checkResult, const ModuleName& root); + bool parseGraph(std::vector& buildQueue, CheckResult& checkResult, const ModuleName& root, bool forAutocomplete); static LintResult classifyLints(const std::vector& warnings, const Config& config); diff --git a/Analysis/include/Luau/Module.h b/Analysis/include/Luau/Module.h index 6c689b7c..9a32f614 100644 --- a/Analysis/include/Luau/Module.h +++ b/Analysis/include/Luau/Module.h @@ -29,8 +29,8 @@ struct SourceModule std::optional environmentName; bool cyclic = false; - std::unique_ptr allocator; - std::unique_ptr names; + std::shared_ptr allocator; + std::shared_ptr names; std::vector parseErrors; AstStatBlock* root = nullptr; @@ -48,6 +48,12 @@ struct SourceModule bool isWithinComment(const SourceModule& sourceModule, Position pos); +struct RequireCycle +{ + Location location; + std::vector path; // one of the paths for a require() to go all the way back to the originating module +}; + struct TypeArena { TypedAllocator typeVars; @@ -77,20 +83,6 @@ struct TypeArena void freeze(TypeArena& arena); void unfreeze(TypeArena& arena); -// Only exposed so they can be unit tested. -using SeenTypes = std::unordered_map; -using SeenTypePacks = std::unordered_map; - -struct CloneState -{ - int recursionCount = 0; - bool encounteredFreeType = false; -}; - -TypePackId clone(TypePackId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); -TypeId clone(TypeId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); -TypeFun clone(const TypeFun& typeFun, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState); - struct Module { ~Module(); @@ -98,6 +90,10 @@ struct Module TypeArena interfaceTypes; TypeArena internalTypes; + // Scopes and AST types refer to parse data, so we need to keep that alive + std::shared_ptr allocator; + std::shared_ptr names; + std::vector> scopes; // never empty DenseHashMap astTypes{nullptr}; @@ -109,6 +105,7 @@ struct Module ErrorVec errors; Mode mode; SourceCode::Type type; + bool timeout = false; ScopePtr getModuleScope() const; diff --git a/Analysis/include/Luau/TypeInfer.h b/Analysis/include/Luau/TypeInfer.h index 839043cc..215da67f 100644 --- a/Analysis/include/Luau/TypeInfer.h +++ b/Analysis/include/Luau/TypeInfer.h @@ -124,6 +124,12 @@ struct HashBoolNamePair size_t operator()(const std::pair& pair) const; }; +class TimeLimitError : public std::exception +{ +public: + virtual const char* what() const throw(); +}; + // All TypeVars are retained via Environment::typeVars. All TypeIds // within a program are borrowed pointers into this set. struct TypeChecker @@ -413,6 +419,10 @@ public: UnifierSharedState unifierState; + std::vector requireCycles; + + std::optional finishTime; + public: const TypeId nilType; const TypeId numberType; diff --git a/Analysis/include/Luau/TypeVar.h b/Analysis/include/Luau/TypeVar.h index b8c4b362..f61e4044 100644 --- a/Analysis/include/Luau/TypeVar.h +++ b/Analysis/include/Luau/TypeVar.h @@ -513,6 +513,8 @@ struct SingletonTypes const TypeId stringType; const TypeId booleanType; const TypeId threadType; + const TypeId trueType; + const TypeId falseType; const TypeId anyType; const TypeId optionalNumberType; diff --git a/Analysis/include/Luau/Variant.h b/Analysis/include/Luau/Variant.h index 63d5a65c..5efe89ed 100644 --- a/Analysis/include/Luau/Variant.h +++ b/Analysis/include/Luau/Variant.h @@ -2,45 +2,14 @@ #pragma once #include "Luau/Common.h" - -#ifndef LUAU_USE_STD_VARIANT -#define LUAU_USE_STD_VARIANT 0 -#endif - -#if LUAU_USE_STD_VARIANT -#include -#else #include #include #include #include -#endif namespace Luau { -#if LUAU_USE_STD_VARIANT -template -using Variant = std::variant; - -template -auto visit(Visitor&& vis, Variant&& var) -{ - // This change resolves the ABI issues with std::variant on libc++; std::visit normally throws bad_variant_access - // but it requires an update to libc++.dylib which ships with macOS 10.14. To work around this, we assert on valueless - // variants since we will never generate them and call into a libc++ function that doesn't throw. - LUAU_ASSERT(!var.valueless_by_exception()); - -#ifdef __APPLE__ - // See https://stackoverflow.com/a/53868971/503215 - return std::__variant_detail::__visitation::__variant::__visit_value(vis, var); -#else - return std::visit(vis, var); -#endif -} - -using std::get_if; -#else template class Variant { @@ -248,6 +217,8 @@ static void fnVisitV(Visitor& vis, std::conditional_t, const template auto visit(Visitor&& vis, const Variant& var) { + static_assert(std::conjunction_v...>, "visitor must accept every alternative as an argument"); + using Result = std::invoke_result_t::first_alternative>; static_assert(std::conjunction_v>...>, "visitor result type must be consistent between alternatives"); @@ -273,6 +244,8 @@ auto visit(Visitor&& vis, const Variant& var) template auto visit(Visitor&& vis, Variant& var) { + static_assert(std::conjunction_v...>, "visitor must accept every alternative as an argument"); + using Result = std::invoke_result_t::first_alternative&>; static_assert(std::conjunction_v>...>, "visitor result type must be consistent between alternatives"); @@ -294,7 +267,6 @@ auto visit(Visitor&& vis, Variant& var) return res; } } -#endif template inline constexpr bool always_false_v = false; diff --git a/Analysis/src/Autocomplete.cpp b/Analysis/src/Autocomplete.cpp index 492edf25..b7201ab3 100644 --- a/Analysis/src/Autocomplete.cpp +++ b/Analysis/src/Autocomplete.cpp @@ -14,6 +14,7 @@ #include LUAU_FASTFLAGVARIABLE(LuauIfElseExprFixCompletionIssue, false); +LUAU_FASTFLAGVARIABLE(LuauAutocompleteSingletonTypes, false); LUAU_FASTFLAG(LuauSelfCallAutocompleteFix) static const std::unordered_set kStatementStartingKeywords = { @@ -625,6 +626,31 @@ AutocompleteEntryMap autocompleteModuleTypes(const Module& module, Position posi return result; } +static void autocompleteStringSingleton(TypeId ty, bool addQuotes, AutocompleteEntryMap& result) +{ + auto formatKey = [addQuotes](const std::string& key) { + if (addQuotes) + return "\"" + escape(key) + "\""; + + return escape(key); + }; + + ty = follow(ty); + + if (auto ss = get(get(ty))) + { + result[formatKey(ss->value)] = AutocompleteEntry{AutocompleteEntryKind::String, ty, false, false, TypeCorrectKind::Correct}; + } + else if (auto uty = get(ty)) + { + for (auto el : uty) + { + if (auto ss = get(get(el))) + result[formatKey(ss->value)] = AutocompleteEntry{AutocompleteEntryKind::String, ty, false, false, TypeCorrectKind::Correct}; + } + } +}; + static bool canSuggestInferredType(ScopePtr scope, TypeId ty) { ty = follow(ty); @@ -1309,17 +1335,38 @@ static void autocompleteExpression(const SourceModule& sourceModule, const Modul scope = scope->parent; } - TypeCorrectKind correctForNil = checkTypeCorrectKind(module, typeArena, node, position, typeChecker.nilType); - TypeCorrectKind correctForBoolean = checkTypeCorrectKind(module, typeArena, node, position, typeChecker.booleanType); - TypeCorrectKind correctForFunction = - functionIsExpectedAt(module, node, position).value_or(false) ? TypeCorrectKind::Correct : TypeCorrectKind::None; + if (FFlag::LuauAutocompleteSingletonTypes) + { + TypeCorrectKind correctForNil = checkTypeCorrectKind(module, typeArena, node, position, typeChecker.nilType); + TypeCorrectKind correctForTrue = checkTypeCorrectKind(module, typeArena, node, position, getSingletonTypes().trueType); + TypeCorrectKind correctForFalse = checkTypeCorrectKind(module, typeArena, node, position, getSingletonTypes().falseType); + TypeCorrectKind correctForFunction = + functionIsExpectedAt(module, node, position).value_or(false) ? TypeCorrectKind::Correct : TypeCorrectKind::None; - result["if"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false}; - result["true"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForBoolean}; - result["false"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForBoolean}; - result["nil"] = {AutocompleteEntryKind::Keyword, typeChecker.nilType, false, false, correctForNil}; - result["not"] = {AutocompleteEntryKind::Keyword}; - result["function"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false, correctForFunction}; + result["if"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false}; + result["true"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForTrue}; + result["false"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForFalse}; + result["nil"] = {AutocompleteEntryKind::Keyword, typeChecker.nilType, false, false, correctForNil}; + result["not"] = {AutocompleteEntryKind::Keyword}; + result["function"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false, correctForFunction}; + + if (auto ty = findExpectedTypeAt(module, node, position)) + autocompleteStringSingleton(*ty, true, result); + } + else + { + TypeCorrectKind correctForNil = checkTypeCorrectKind(module, typeArena, node, position, typeChecker.nilType); + TypeCorrectKind correctForBoolean = checkTypeCorrectKind(module, typeArena, node, position, typeChecker.booleanType); + TypeCorrectKind correctForFunction = + functionIsExpectedAt(module, node, position).value_or(false) ? TypeCorrectKind::Correct : TypeCorrectKind::None; + + result["if"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false}; + result["true"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForBoolean}; + result["false"] = {AutocompleteEntryKind::Keyword, typeChecker.booleanType, false, false, correctForBoolean}; + result["nil"] = {AutocompleteEntryKind::Keyword, typeChecker.nilType, false, false, correctForNil}; + result["not"] = {AutocompleteEntryKind::Keyword}; + result["function"] = {AutocompleteEntryKind::Keyword, std::nullopt, false, false, correctForFunction}; + } } } @@ -1625,17 +1672,33 @@ static AutocompleteResult autocomplete(const SourceModule& sourceModule, const M } else if (node->is()) { + AutocompleteEntryMap result; + + if (FFlag::LuauAutocompleteSingletonTypes) + { + if (auto it = module->astExpectedTypes.find(node->asExpr())) + autocompleteStringSingleton(*it, false, result); + } + if (finder.ancestry.size() >= 2) { if (auto idxExpr = finder.ancestry.at(finder.ancestry.size() - 2)->as()) { if (auto it = module->astTypes.find(idxExpr->expr)) + autocompleteProps(*module, typeArena, follow(*it), PropIndexType::Point, finder.ancestry, result); + } + else if (auto binExpr = finder.ancestry.at(finder.ancestry.size() - 2)->as(); + binExpr && FFlag::LuauAutocompleteSingletonTypes) + { + if (binExpr->op == AstExprBinary::CompareEq || binExpr->op == AstExprBinary::CompareNe) { - return {autocompleteProps(*module, typeArena, follow(*it), PropIndexType::Point, finder.ancestry), finder.ancestry}; + if (auto it = module->astTypes.find(node == binExpr->left ? binExpr->right : binExpr->left)) + autocompleteStringSingleton(*it, false, result); } } } - return {}; + + return {result, finder.ancestry}; } if (node->is()) @@ -1653,18 +1716,31 @@ static AutocompleteResult autocomplete(const SourceModule& sourceModule, const M AutocompleteResult autocomplete(Frontend& frontend, const ModuleName& moduleName, Position position, StringCompletionCallback callback) { - // FIXME: We can improve performance here by parsing without checking. - // The old type graph is probably fine. (famous last words!) - // FIXME: We don't need to typecheck for script analysis here, just for autocomplete. - frontend.check(moduleName); + if (FFlag::LuauSeparateTypechecks) + { + // FIXME: We can improve performance here by parsing without checking. + // The old type graph is probably fine. (famous last words!) + FrontendOptions opts; + opts.forAutocomplete = true; + frontend.check(moduleName, opts); + } + else + { + // FIXME: We can improve performance here by parsing without checking. + // The old type graph is probably fine. (famous last words!) + // FIXME: We don't need to typecheck for script analysis here, just for autocomplete. + frontend.check(moduleName); + } const SourceModule* sourceModule = frontend.getSourceModule(moduleName); if (!sourceModule) return {}; - TypeChecker& typeChecker = (frontend.options.typecheckTwice ? frontend.typeCheckerForAutocomplete : frontend.typeChecker); - ModulePtr module = (frontend.options.typecheckTwice ? frontend.moduleResolverForAutocomplete.getModule(moduleName) - : frontend.moduleResolver.getModule(moduleName)); + TypeChecker& typeChecker = + (frontend.options.typecheckTwice_DEPRECATED || FFlag::LuauSeparateTypechecks ? frontend.typeCheckerForAutocomplete : frontend.typeChecker); + ModulePtr module = + (frontend.options.typecheckTwice_DEPRECATED || FFlag::LuauSeparateTypechecks ? frontend.moduleResolverForAutocomplete.getModule(moduleName) + : frontend.moduleResolver.getModule(moduleName)); if (!module) return {}; @@ -1692,7 +1768,8 @@ OwningAutocompleteResult autocompleteSource(Frontend& frontend, std::string_view sourceModule->mode = Mode::Strict; sourceModule->commentLocations = std::move(result.commentLocations); - TypeChecker& typeChecker = (frontend.options.typecheckTwice ? frontend.typeCheckerForAutocomplete : frontend.typeChecker); + TypeChecker& typeChecker = + (frontend.options.typecheckTwice_DEPRECATED || FFlag::LuauSeparateTypechecks ? frontend.typeCheckerForAutocomplete : frontend.typeChecker); ModulePtr module = typeChecker.check(*sourceModule, Mode::Strict); diff --git a/Analysis/src/Clone.cpp b/Analysis/src/Clone.cpp new file mode 100644 index 00000000..ac9705a7 --- /dev/null +++ b/Analysis/src/Clone.cpp @@ -0,0 +1,371 @@ +// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details + +#include "Luau/Clone.h" +#include "Luau/Module.h" +#include "Luau/RecursionCounter.h" +#include "Luau/TypePack.h" +#include "Luau/Unifiable.h" + +LUAU_FASTINTVARIABLE(LuauTypeCloneRecursionLimit, 300) + +namespace Luau +{ + +namespace +{ + +struct TypePackCloner; + +/* + * Both TypeCloner and TypePackCloner work by depositing the requested type variable into the appropriate 'seen' set. + * They do not return anything because their sole consumer (the deepClone function) already has a pointer into this storage. + */ + +struct TypeCloner +{ + TypeCloner(TypeArena& dest, TypeId typeId, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) + : dest(dest) + , typeId(typeId) + , seenTypes(seenTypes) + , seenTypePacks(seenTypePacks) + , cloneState(cloneState) + { + } + + TypeArena& dest; + TypeId typeId; + SeenTypes& seenTypes; + SeenTypePacks& seenTypePacks; + CloneState& cloneState; + + template + void defaultClone(const T& t); + + void operator()(const Unifiable::Free& t); + void operator()(const Unifiable::Generic& t); + void operator()(const Unifiable::Bound& t); + void operator()(const Unifiable::Error& t); + void operator()(const PrimitiveTypeVar& t); + void operator()(const SingletonTypeVar& t); + void operator()(const FunctionTypeVar& t); + void operator()(const TableTypeVar& t); + void operator()(const MetatableTypeVar& t); + void operator()(const ClassTypeVar& t); + void operator()(const AnyTypeVar& t); + void operator()(const UnionTypeVar& t); + void operator()(const IntersectionTypeVar& t); + void operator()(const LazyTypeVar& t); +}; + +struct TypePackCloner +{ + TypeArena& dest; + TypePackId typePackId; + SeenTypes& seenTypes; + SeenTypePacks& seenTypePacks; + CloneState& cloneState; + + TypePackCloner(TypeArena& dest, TypePackId typePackId, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) + : dest(dest) + , typePackId(typePackId) + , seenTypes(seenTypes) + , seenTypePacks(seenTypePacks) + , cloneState(cloneState) + { + } + + template + void defaultClone(const T& t) + { + TypePackId cloned = dest.addTypePack(TypePackVar{t}); + seenTypePacks[typePackId] = cloned; + } + + void operator()(const Unifiable::Free& t) + { + cloneState.encounteredFreeType = true; + + TypePackId err = getSingletonTypes().errorRecoveryTypePack(getSingletonTypes().anyTypePack); + TypePackId cloned = dest.addTypePack(*err); + seenTypePacks[typePackId] = cloned; + } + + void operator()(const Unifiable::Generic& t) + { + defaultClone(t); + } + void operator()(const Unifiable::Error& t) + { + defaultClone(t); + } + + // While we are a-cloning, we can flatten out bound TypeVars and make things a bit tighter. + // We just need to be sure that we rewrite pointers both to the binder and the bindee to the same pointer. + void operator()(const Unifiable::Bound& t) + { + TypePackId cloned = clone(t.boundTo, dest, seenTypes, seenTypePacks, cloneState); + seenTypePacks[typePackId] = cloned; + } + + void operator()(const VariadicTypePack& t) + { + TypePackId cloned = dest.addTypePack(TypePackVar{VariadicTypePack{clone(t.ty, dest, seenTypes, seenTypePacks, cloneState)}}); + seenTypePacks[typePackId] = cloned; + } + + void operator()(const TypePack& t) + { + TypePackId cloned = dest.addTypePack(TypePack{}); + TypePack* destTp = getMutable(cloned); + LUAU_ASSERT(destTp != nullptr); + seenTypePacks[typePackId] = cloned; + + for (TypeId ty : t.head) + destTp->head.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); + + if (t.tail) + destTp->tail = clone(*t.tail, dest, seenTypes, seenTypePacks, cloneState); + } +}; + +template +void TypeCloner::defaultClone(const T& t) +{ + TypeId cloned = dest.addType(t); + seenTypes[typeId] = cloned; +} + +void TypeCloner::operator()(const Unifiable::Free& t) +{ + cloneState.encounteredFreeType = true; + TypeId err = getSingletonTypes().errorRecoveryType(getSingletonTypes().anyType); + TypeId cloned = dest.addType(*err); + seenTypes[typeId] = cloned; +} + +void TypeCloner::operator()(const Unifiable::Generic& t) +{ + defaultClone(t); +} + +void TypeCloner::operator()(const Unifiable::Bound& t) +{ + TypeId boundTo = clone(t.boundTo, dest, seenTypes, seenTypePacks, cloneState); + seenTypes[typeId] = boundTo; +} + +void TypeCloner::operator()(const Unifiable::Error& t) +{ + defaultClone(t); +} + +void TypeCloner::operator()(const PrimitiveTypeVar& t) +{ + defaultClone(t); +} + +void TypeCloner::operator()(const SingletonTypeVar& t) +{ + defaultClone(t); +} + +void TypeCloner::operator()(const FunctionTypeVar& t) +{ + TypeId result = dest.addType(FunctionTypeVar{TypeLevel{0, 0}, {}, {}, nullptr, nullptr, t.definition, t.hasSelf}); + FunctionTypeVar* ftv = getMutable(result); + LUAU_ASSERT(ftv != nullptr); + + seenTypes[typeId] = result; + + for (TypeId generic : t.generics) + ftv->generics.push_back(clone(generic, dest, seenTypes, seenTypePacks, cloneState)); + + for (TypePackId genericPack : t.genericPacks) + ftv->genericPacks.push_back(clone(genericPack, dest, seenTypes, seenTypePacks, cloneState)); + + ftv->tags = t.tags; + ftv->argTypes = clone(t.argTypes, dest, seenTypes, seenTypePacks, cloneState); + ftv->argNames = t.argNames; + ftv->retType = clone(t.retType, dest, seenTypes, seenTypePacks, cloneState); +} + +void TypeCloner::operator()(const TableTypeVar& t) +{ + // If table is now bound to another one, we ignore the content of the original + if (t.boundTo) + { + TypeId boundTo = clone(*t.boundTo, dest, seenTypes, seenTypePacks, cloneState); + seenTypes[typeId] = boundTo; + return; + } + + TypeId result = dest.addType(TableTypeVar{}); + TableTypeVar* ttv = getMutable(result); + LUAU_ASSERT(ttv != nullptr); + + *ttv = t; + + seenTypes[typeId] = result; + + ttv->level = TypeLevel{0, 0}; + + for (const auto& [name, prop] : t.props) + ttv->props[name] = {clone(prop.type, dest, seenTypes, seenTypePacks, cloneState), prop.deprecated, {}, prop.location, prop.tags}; + + if (t.indexer) + ttv->indexer = TableIndexer{clone(t.indexer->indexType, dest, seenTypes, seenTypePacks, cloneState), + clone(t.indexer->indexResultType, dest, seenTypes, seenTypePacks, cloneState)}; + + for (TypeId& arg : ttv->instantiatedTypeParams) + arg = clone(arg, dest, seenTypes, seenTypePacks, cloneState); + + for (TypePackId& arg : ttv->instantiatedTypePackParams) + arg = clone(arg, dest, seenTypes, seenTypePacks, cloneState); + + if (ttv->state == TableState::Free) + { + cloneState.encounteredFreeType = true; + + ttv->state = TableState::Sealed; + } + + ttv->definitionModuleName = t.definitionModuleName; + ttv->methodDefinitionLocations = t.methodDefinitionLocations; + ttv->tags = t.tags; +} + +void TypeCloner::operator()(const MetatableTypeVar& t) +{ + TypeId result = dest.addType(MetatableTypeVar{}); + MetatableTypeVar* mtv = getMutable(result); + seenTypes[typeId] = result; + + mtv->table = clone(t.table, dest, seenTypes, seenTypePacks, cloneState); + mtv->metatable = clone(t.metatable, dest, seenTypes, seenTypePacks, cloneState); +} + +void TypeCloner::operator()(const ClassTypeVar& t) +{ + TypeId result = dest.addType(ClassTypeVar{t.name, {}, std::nullopt, std::nullopt, t.tags, t.userData}); + ClassTypeVar* ctv = getMutable(result); + + seenTypes[typeId] = result; + + for (const auto& [name, prop] : t.props) + ctv->props[name] = {clone(prop.type, dest, seenTypes, seenTypePacks, cloneState), prop.deprecated, {}, prop.location, prop.tags}; + + if (t.parent) + ctv->parent = clone(*t.parent, dest, seenTypes, seenTypePacks, cloneState); + + if (t.metatable) + ctv->metatable = clone(*t.metatable, dest, seenTypes, seenTypePacks, cloneState); +} + +void TypeCloner::operator()(const AnyTypeVar& t) +{ + defaultClone(t); +} + +void TypeCloner::operator()(const UnionTypeVar& t) +{ + std::vector options; + options.reserve(t.options.size()); + + for (TypeId ty : t.options) + options.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); + + TypeId result = dest.addType(UnionTypeVar{std::move(options)}); + seenTypes[typeId] = result; +} + +void TypeCloner::operator()(const IntersectionTypeVar& t) +{ + TypeId result = dest.addType(IntersectionTypeVar{}); + seenTypes[typeId] = result; + + IntersectionTypeVar* option = getMutable(result); + LUAU_ASSERT(option != nullptr); + + for (TypeId ty : t.parts) + option->parts.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); +} + +void TypeCloner::operator()(const LazyTypeVar& t) +{ + defaultClone(t); +} + +} // anonymous namespace + +TypePackId clone(TypePackId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) +{ + if (tp->persistent) + return tp; + + RecursionLimiter _ra(&cloneState.recursionCount, FInt::LuauTypeCloneRecursionLimit); + + TypePackId& res = seenTypePacks[tp]; + + if (res == nullptr) + { + TypePackCloner cloner{dest, tp, seenTypes, seenTypePacks, cloneState}; + Luau::visit(cloner, tp->ty); // Mutates the storage that 'res' points into. + } + + return res; +} + +TypeId clone(TypeId typeId, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) +{ + if (typeId->persistent) + return typeId; + + RecursionLimiter _ra(&cloneState.recursionCount, FInt::LuauTypeCloneRecursionLimit); + + TypeId& res = seenTypes[typeId]; + + if (res == nullptr) + { + TypeCloner cloner{dest, typeId, seenTypes, seenTypePacks, cloneState}; + Luau::visit(cloner, typeId->ty); // Mutates the storage that 'res' points into. + + // Persistent types are not being cloned and we get the original type back which might be read-only + if (!res->persistent) + asMutable(res)->documentationSymbol = typeId->documentationSymbol; + } + + return res; +} + +TypeFun clone(const TypeFun& typeFun, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) +{ + TypeFun result; + + for (auto param : typeFun.typeParams) + { + TypeId ty = clone(param.ty, dest, seenTypes, seenTypePacks, cloneState); + std::optional defaultValue; + + if (param.defaultValue) + defaultValue = clone(*param.defaultValue, dest, seenTypes, seenTypePacks, cloneState); + + result.typeParams.push_back({ty, defaultValue}); + } + + for (auto param : typeFun.typePackParams) + { + TypePackId tp = clone(param.tp, dest, seenTypes, seenTypePacks, cloneState); + std::optional defaultValue; + + if (param.defaultValue) + defaultValue = clone(*param.defaultValue, dest, seenTypes, seenTypePacks, cloneState); + + result.typePackParams.push_back({tp, defaultValue}); + } + + result.type = clone(typeFun.type, dest, seenTypes, seenTypePacks, cloneState); + + return result; +} + +} // namespace Luau diff --git a/Analysis/src/Error.cpp b/Analysis/src/Error.cpp index 210c0191..5eb2ea2a 100644 --- a/Analysis/src/Error.cpp +++ b/Analysis/src/Error.cpp @@ -1,6 +1,7 @@ // This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details #include "Luau/Error.h" +#include "Luau/Clone.h" #include "Luau/Module.h" #include "Luau/StringUtils.h" #include "Luau/ToString.h" diff --git a/Analysis/src/Frontend.cpp b/Analysis/src/Frontend.cpp index d8906f6e..000769fe 100644 --- a/Analysis/src/Frontend.cpp +++ b/Analysis/src/Frontend.cpp @@ -2,6 +2,7 @@ #include "Luau/Frontend.h" #include "Luau/Common.h" +#include "Luau/Clone.h" #include "Luau/Config.h" #include "Luau/FileResolver.h" #include "Luau/Parser.h" @@ -16,8 +17,11 @@ #include #include +LUAU_FASTFLAG(LuauCyclicModuleTypeSurface) LUAU_FASTFLAG(LuauInferInNoCheckMode) LUAU_FASTFLAGVARIABLE(LuauKnowsTheDataModel3, false) +LUAU_FASTFLAGVARIABLE(LuauSeparateTypechecks, false) +LUAU_FASTINTVARIABLE(LuauAutocompleteCheckTimeoutMs, 0) namespace Luau { @@ -234,12 +238,6 @@ ErrorVec accumulateErrors( return result; } -struct RequireCycle -{ - Location location; - std::vector path; // one of the paths for a require() to go all the way back to the originating module -}; - // Given a source node (start), find all requires that start a transitive dependency path that ends back at start // For each such path, record the full path and the location of the require in the starting module. // Note that this is O(V^2) for a fully connected graph and produces O(V) paths of length O(V) @@ -356,33 +354,55 @@ CheckResult Frontend::check(const ModuleName& name, std::optionalsecond.dirty) + if (it != sourceNodes.end() && !it->second.isDirty(frontendOptions.forAutocomplete)) { // No recheck required. - auto it2 = moduleResolver.modules.find(name); - if (it2 == moduleResolver.modules.end() || it2->second == nullptr) - throw std::runtime_error("Frontend::modules does not have data for " + name); + if (FFlag::LuauSeparateTypechecks) + { + if (frontendOptions.forAutocomplete) + { + auto it2 = moduleResolverForAutocomplete.modules.find(name); + if (it2 == moduleResolverForAutocomplete.modules.end() || it2->second == nullptr) + throw std::runtime_error("Frontend::modules does not have data for " + name); + } + else + { + auto it2 = moduleResolver.modules.find(name); + if (it2 == moduleResolver.modules.end() || it2->second == nullptr) + throw std::runtime_error("Frontend::modules does not have data for " + name); + } - return CheckResult{accumulateErrors(sourceNodes, moduleResolver.modules, name)}; + return CheckResult{accumulateErrors( + sourceNodes, frontendOptions.forAutocomplete ? moduleResolverForAutocomplete.modules : moduleResolver.modules, name)}; + } + else + { + auto it2 = moduleResolver.modules.find(name); + if (it2 == moduleResolver.modules.end() || it2->second == nullptr) + throw std::runtime_error("Frontend::modules does not have data for " + name); + + return CheckResult{accumulateErrors(sourceNodes, moduleResolver.modules, name)}; + } } std::vector buildQueue; - bool cycleDetected = parseGraph(buildQueue, checkResult, name); - - FrontendOptions frontendOptions = optionOverride.value_or(options); + bool cycleDetected = parseGraph(buildQueue, checkResult, name, frontendOptions.forAutocomplete); // Keep track of which AST nodes we've reported cycles in std::unordered_set reportedCycles; + double autocompleteTimeLimit = FInt::LuauAutocompleteCheckTimeoutMs / 1000.0; + for (const ModuleName& moduleName : buildQueue) { LUAU_ASSERT(sourceNodes.count(moduleName)); SourceNode& sourceNode = sourceNodes[moduleName]; - if (!sourceNode.dirty) + if (!sourceNode.isDirty(frontendOptions.forAutocomplete)) continue; LUAU_ASSERT(sourceModules.count(moduleName)); @@ -408,13 +428,44 @@ CheckResult Frontend::check(const ModuleName& name, std::optionaltimeout) + checkResult.timeoutHits.push_back(moduleName); + + stats.timeCheck += getTimestamp() - timestamp; + stats.filesStrict += 1; + + sourceNode.dirtyAutocomplete = false; + continue; + } + + if (FFlag::LuauCyclicModuleTypeSurface) + typeChecker.requireCycles = requireCycles; + ModulePtr module = typeChecker.check(sourceModule, mode, environmentScope); // If we're typechecking twice, we do so. // The second typecheck is always in strict mode with DM awareness // to provide better typen information for IDE features. - if (frontendOptions.typecheckTwice) + if (!FFlag::LuauSeparateTypechecks && frontendOptions.typecheckTwice_DEPRECATED) { + if (FFlag::LuauCyclicModuleTypeSurface) + typeCheckerForAutocomplete.requireCycles = requireCycles; + ModulePtr moduleForAutocomplete = typeCheckerForAutocomplete.check(sourceModule, Mode::Strict); moduleResolverForAutocomplete.modules[moduleName] = moduleForAutocomplete; } @@ -467,7 +518,7 @@ CheckResult Frontend::check(const ModuleName& name, std::optional& buildQueue, CheckResult& checkResult, const ModuleName& root) +bool Frontend::parseGraph(std::vector& buildQueue, CheckResult& checkResult, const ModuleName& root, bool forAutocomplete) { LUAU_TIMETRACE_SCOPE("Frontend::parseGraph", "Frontend"); LUAU_TIMETRACE_ARGUMENT("root", root.c_str()); @@ -486,7 +537,7 @@ bool Frontend::parseGraph(std::vector& buildQueue, CheckResult& chec bool cyclic = false; { - auto [sourceNode, _] = getSourceNode(checkResult, root); + auto [sourceNode, _] = getSourceNode(checkResult, root, forAutocomplete); if (sourceNode) stack.push_back(sourceNode); } @@ -538,7 +589,7 @@ bool Frontend::parseGraph(std::vector& buildQueue, CheckResult& chec // this relies on the fact that markDirty marks reverse-dependencies dirty as well // thus if a node is not dirty, all its transitive deps aren't dirty, which means that they won't ever need // to be built, *and* can't form a cycle with any nodes we did process. - if (!it->second.dirty) + if (!it->second.isDirty(forAutocomplete)) continue; // note: this check is technically redundant *except* that getSourceNode has somewhat broken memoization @@ -550,7 +601,7 @@ bool Frontend::parseGraph(std::vector& buildQueue, CheckResult& chec } } - auto [sourceNode, _] = getSourceNode(checkResult, dep); + auto [sourceNode, _] = getSourceNode(checkResult, dep, forAutocomplete); if (sourceNode) { stack.push_back(sourceNode); @@ -594,7 +645,7 @@ LintResult Frontend::lint(const ModuleName& name, std::optionalsecond.dirty; + return it == sourceNodes.end() || it->second.isDirty(forAutocomplete); } /* @@ -699,8 +750,16 @@ bool Frontend::isDirty(const ModuleName& name) const */ void Frontend::markDirty(const ModuleName& name, std::vector* markedDirty) { - if (!moduleResolver.modules.count(name)) - return; + if (FFlag::LuauSeparateTypechecks) + { + if (!moduleResolver.modules.count(name) && !moduleResolverForAutocomplete.modules.count(name)) + return; + } + else + { + if (!moduleResolver.modules.count(name)) + return; + } std::unordered_map> reverseDeps; for (const auto& module : sourceNodes) @@ -722,10 +781,21 @@ void Frontend::markDirty(const ModuleName& name, std::vector* marked if (markedDirty) markedDirty->push_back(next); - if (sourceNode.dirty) - continue; + if (FFlag::LuauSeparateTypechecks) + { + if (sourceNode.dirty && sourceNode.dirtyAutocomplete) + continue; - sourceNode.dirty = true; + sourceNode.dirty = true; + sourceNode.dirtyAutocomplete = true; + } + else + { + if (sourceNode.dirty) + continue; + + sourceNode.dirty = true; + } if (0 == reverseDeps.count(name)) continue; @@ -752,13 +822,13 @@ const SourceModule* Frontend::getSourceModule(const ModuleName& moduleName) cons } // Read AST into sourceModules if necessary. Trace require()s. Report parse errors. -std::pair Frontend::getSourceNode(CheckResult& checkResult, const ModuleName& name) +std::pair Frontend::getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete) { LUAU_TIMETRACE_SCOPE("Frontend::getSourceNode", "Frontend"); LUAU_TIMETRACE_ARGUMENT("name", name.c_str()); auto it = sourceNodes.find(name); - if (it != sourceNodes.end() && !it->second.dirty) + if (it != sourceNodes.end() && !it->second.isDirty(forAutocomplete)) { auto moduleIt = sourceModules.find(name); if (moduleIt != sourceModules.end()) @@ -801,7 +871,19 @@ std::pair Frontend::getSourceNode(CheckResult& check sourceNode.name = name; sourceNode.requires.clear(); sourceNode.requireLocations.clear(); - sourceNode.dirty = true; + + if (FFlag::LuauSeparateTypechecks) + { + if (it == sourceNodes.end()) + { + sourceNode.dirty = true; + sourceNode.dirtyAutocomplete = true; + } + } + else + { + sourceNode.dirty = true; + } for (const auto& [moduleName, location] : requireTrace.requires) sourceNode.requires.insert(moduleName); diff --git a/Analysis/src/IostreamHelpers.cpp b/Analysis/src/IostreamHelpers.cpp index 19c2ddab..a8f67589 100644 --- a/Analysis/src/IostreamHelpers.cpp +++ b/Analysis/src/IostreamHelpers.cpp @@ -23,9 +23,178 @@ std::ostream& operator<<(std::ostream& stream, const AstName& name) return stream << ""; } -std::ostream& operator<<(std::ostream& stream, const TypeMismatch& tm) +template +static void errorToString(std::ostream& stream, const T& err) { - return stream << "TypeMismatch { " << toString(tm.wantedType) << ", " << toString(tm.givenType) << " }"; + if constexpr (false) + { + } + else if constexpr (std::is_same_v) + stream << "TypeMismatch { " << toString(err.wantedType) << ", " << toString(err.givenType) << " }"; + else if constexpr (std::is_same_v) + stream << "UnknownSymbol { " << err.name << " , context " << err.context << " }"; + else if constexpr (std::is_same_v) + stream << "UnknownProperty { " << toString(err.table) << ", key = " << err.key << " }"; + else if constexpr (std::is_same_v) + stream << "NotATable { " << toString(err.ty) << " }"; + else if constexpr (std::is_same_v) + stream << "CannotExtendTable { " << toString(err.tableType) << ", context " << err.context << ", prop \"" << err.prop << "\" }"; + else if constexpr (std::is_same_v) + stream << "OnlyTablesCanHaveMethods { " << toString(err.tableType) << " }"; + else if constexpr (std::is_same_v) + stream << "DuplicateTypeDefinition { " << err.name << " }"; + else if constexpr (std::is_same_v) + stream << "CountMismatch { expected " << err.expected << ", got " << err.actual << ", context " << err.context << " }"; + else if constexpr (std::is_same_v) + stream << "FunctionDoesNotTakeSelf { }"; + else if constexpr (std::is_same_v) + stream << "FunctionRequiresSelf { extraNils " << err.requiredExtraNils << " }"; + else if constexpr (std::is_same_v) + stream << "OccursCheckFailed { }"; + else if constexpr (std::is_same_v) + stream << "UnknownRequire { " << err.modulePath << " }"; + else if constexpr (std::is_same_v) + { + stream << "IncorrectGenericParameterCount { name = " << err.name; + + if (!err.typeFun.typeParams.empty() || !err.typeFun.typePackParams.empty()) + { + stream << "<"; + bool first = true; + for (auto param : err.typeFun.typeParams) + { + if (first) + first = false; + else + stream << ", "; + + stream << toString(param.ty); + } + + for (auto param : err.typeFun.typePackParams) + { + if (first) + first = false; + else + stream << ", "; + + stream << toString(param.tp); + } + + stream << ">"; + } + + stream << ", typeFun = " << toString(err.typeFun.type) << ", actualCount = " << err.actualParameters << " }"; + } + else if constexpr (std::is_same_v) + stream << "SyntaxError { " << err.message << " }"; + else if constexpr (std::is_same_v) + stream << "CodeTooComplex {}"; + else if constexpr (std::is_same_v) + stream << "UnificationTooComplex {}"; + else if constexpr (std::is_same_v) + { + stream << "UnknownPropButFoundLikeProp { key = '" << err.key << "', suggested = { "; + + bool first = true; + for (Name name : err.candidates) + { + if (first) + first = false; + else + stream << ", "; + + stream << "'" << name << "'"; + } + + stream << " }, table = " << toString(err.table) << " } "; + } + else if constexpr (std::is_same_v) + stream << "GenericError { " << err.message << " }"; + else if constexpr (std::is_same_v) + stream << "CannotCallNonFunction { " << toString(err.ty) << " }"; + else if constexpr (std::is_same_v) + stream << "ExtraInformation { " << err.message << " }"; + else if constexpr (std::is_same_v) + stream << "DeprecatedApiUsed { " << err.symbol << ", useInstead = " << err.useInstead << " }"; + else if constexpr (std::is_same_v) + { + stream << "ModuleHasCyclicDependency {"; + + bool first = true; + for (const ModuleName& name : err.cycle) + { + if (first) + first = false; + else + stream << ", "; + + stream << name; + } + + stream << "}"; + } + else if constexpr (std::is_same_v) + stream << "IllegalRequire { " << err.moduleName << ", reason = " << err.reason << " }"; + else if constexpr (std::is_same_v) + stream << "FunctionExitsWithoutReturning {" << toString(err.expectedReturnType) << "}"; + else if constexpr (std::is_same_v) + stream << "DuplicateGenericParameter { " + err.parameterName + " }"; + else if constexpr (std::is_same_v) + stream << "CannotInferBinaryOperation { op = " + toString(err.op) + ", suggested = '" + + (err.suggestedToAnnotate ? *err.suggestedToAnnotate : "") + "', kind " + << err.kind << "}"; + else if constexpr (std::is_same_v) + { + stream << "MissingProperties { superType = '" << toString(err.superType) << "', subType = '" << toString(err.subType) << "', properties = { "; + + bool first = true; + for (Name name : err.properties) + { + if (first) + first = false; + else + stream << ", "; + + stream << "'" << name << "'"; + } + + stream << " }, context " << err.context << " } "; + } + else if constexpr (std::is_same_v) + stream << "SwappedGenericTypeParameter { name = '" + err.name + "', kind = " + std::to_string(err.kind) + " }"; + else if constexpr (std::is_same_v) + stream << "OptionalValueAccess { optional = '" + toString(err.optional) + "' }"; + else if constexpr (std::is_same_v) + { + stream << "MissingUnionProperty { type = '" + toString(err.type) + "', missing = { "; + + bool first = true; + for (auto ty : err.missing) + { + if (first) + first = false; + else + stream << ", "; + + stream << "'" << toString(ty) << "'"; + } + + stream << " }, key = '" + err.key + "' }"; + } + else if constexpr (std::is_same_v) + stream << "TypesAreUnrelated { left = '" + toString(err.left) + "', right = '" + toString(err.right) + "' }"; + else + static_assert(always_false_v, "Non-exhaustive type switch"); +} + +std::ostream& operator<<(std::ostream& stream, const TypeErrorData& data) +{ + auto cb = [&](const auto& e) { + return errorToString(stream, e); + }; + visit(cb, data); + return stream; } std::ostream& operator<<(std::ostream& stream, const TypeError& error) @@ -33,241 +202,6 @@ std::ostream& operator<<(std::ostream& stream, const TypeError& error) return stream << "TypeError { \"" << error.moduleName << "\", " << error.location << ", " << error.data << " }"; } -std::ostream& operator<<(std::ostream& stream, const UnknownSymbol& error) -{ - return stream << "UnknownSymbol { " << error.name << " , context " << error.context << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const UnknownProperty& error) -{ - return stream << "UnknownProperty { " << toString(error.table) << ", key = " << error.key << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const NotATable& ge) -{ - return stream << "NotATable { " << toString(ge.ty) << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const CannotExtendTable& error) -{ - return stream << "CannotExtendTable { " << toString(error.tableType) << ", context " << error.context << ", prop \"" << error.prop << "\" }"; -} - -std::ostream& operator<<(std::ostream& stream, const OnlyTablesCanHaveMethods& error) -{ - return stream << "OnlyTablesCanHaveMethods { " << toString(error.tableType) << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const DuplicateTypeDefinition& error) -{ - return stream << "DuplicateTypeDefinition { " << error.name << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const CountMismatch& error) -{ - return stream << "CountMismatch { expected " << error.expected << ", got " << error.actual << ", context " << error.context << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const FunctionDoesNotTakeSelf&) -{ - return stream << "FunctionDoesNotTakeSelf { }"; -} - -std::ostream& operator<<(std::ostream& stream, const FunctionRequiresSelf& error) -{ - return stream << "FunctionRequiresSelf { extraNils " << error.requiredExtraNils << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const OccursCheckFailed&) -{ - return stream << "OccursCheckFailed { }"; -} - -std::ostream& operator<<(std::ostream& stream, const UnknownRequire& error) -{ - return stream << "UnknownRequire { " << error.modulePath << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const IncorrectGenericParameterCount& error) -{ - stream << "IncorrectGenericParameterCount { name = " << error.name; - - if (!error.typeFun.typeParams.empty() || !error.typeFun.typePackParams.empty()) - { - stream << "<"; - bool first = true; - for (auto param : error.typeFun.typeParams) - { - if (first) - first = false; - else - stream << ", "; - - stream << toString(param.ty); - } - - for (auto param : error.typeFun.typePackParams) - { - if (first) - first = false; - else - stream << ", "; - - stream << toString(param.tp); - } - - stream << ">"; - } - - stream << ", typeFun = " << toString(error.typeFun.type) << ", actualCount = " << error.actualParameters << " }"; - return stream; -} - -std::ostream& operator<<(std::ostream& stream, const SyntaxError& ge) -{ - return stream << "SyntaxError { " << ge.message << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const CodeTooComplex&) -{ - return stream << "CodeTooComplex {}"; -} - -std::ostream& operator<<(std::ostream& stream, const UnificationTooComplex&) -{ - return stream << "UnificationTooComplex {}"; -} - -std::ostream& operator<<(std::ostream& stream, const UnknownPropButFoundLikeProp& e) -{ - stream << "UnknownPropButFoundLikeProp { key = '" << e.key << "', suggested = { "; - - bool first = true; - for (Name name : e.candidates) - { - if (first) - first = false; - else - stream << ", "; - - stream << "'" << name << "'"; - } - - return stream << " }, table = " << toString(e.table) << " } "; -} - -std::ostream& operator<<(std::ostream& stream, const GenericError& ge) -{ - return stream << "GenericError { " << ge.message << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const CannotCallNonFunction& e) -{ - return stream << "CannotCallNonFunction { " << toString(e.ty) << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const FunctionExitsWithoutReturning& error) -{ - return stream << "FunctionExitsWithoutReturning {" << toString(error.expectedReturnType) << "}"; -} - -std::ostream& operator<<(std::ostream& stream, const ExtraInformation& e) -{ - return stream << "ExtraInformation { " << e.message << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const DeprecatedApiUsed& e) -{ - return stream << "DeprecatedApiUsed { " << e.symbol << ", useInstead = " << e.useInstead << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const ModuleHasCyclicDependency& e) -{ - stream << "ModuleHasCyclicDependency {"; - - bool first = true; - for (const ModuleName& name : e.cycle) - { - if (first) - first = false; - else - stream << ", "; - - stream << name; - } - - return stream << "}"; -} - -std::ostream& operator<<(std::ostream& stream, const IllegalRequire& e) -{ - return stream << "IllegalRequire { " << e.moduleName << ", reason = " << e.reason << " }"; -} - -std::ostream& operator<<(std::ostream& stream, const MissingProperties& e) -{ - stream << "MissingProperties { superType = '" << toString(e.superType) << "', subType = '" << toString(e.subType) << "', properties = { "; - - bool first = true; - for (Name name : e.properties) - { - if (first) - first = false; - else - stream << ", "; - - stream << "'" << name << "'"; - } - - return stream << " }, context " << e.context << " } "; -} - -std::ostream& operator<<(std::ostream& stream, const DuplicateGenericParameter& error) -{ - return stream << "DuplicateGenericParameter { " + error.parameterName + " }"; -} - -std::ostream& operator<<(std::ostream& stream, const CannotInferBinaryOperation& error) -{ - return stream << "CannotInferBinaryOperation { op = " + toString(error.op) + ", suggested = '" + - (error.suggestedToAnnotate ? *error.suggestedToAnnotate : "") + "', kind " - << error.kind << "}"; -} - -std::ostream& operator<<(std::ostream& stream, const SwappedGenericTypeParameter& error) -{ - return stream << "SwappedGenericTypeParameter { name = '" + error.name + "', kind = " + std::to_string(error.kind) + " }"; -} - -std::ostream& operator<<(std::ostream& stream, const OptionalValueAccess& error) -{ - return stream << "OptionalValueAccess { optional = '" + toString(error.optional) + "' }"; -} - -std::ostream& operator<<(std::ostream& stream, const MissingUnionProperty& error) -{ - stream << "MissingUnionProperty { type = '" + toString(error.type) + "', missing = { "; - - bool first = true; - for (auto ty : error.missing) - { - if (first) - first = false; - else - stream << ", "; - - stream << "'" << toString(ty) << "'"; - } - - return stream << " }, key = '" + error.key + "' }"; -} - -std::ostream& operator<<(std::ostream& stream, const TypesAreUnrelated& error) -{ - stream << "TypesAreUnrelated { left = '" + toString(error.left) + "', right = '" + toString(error.right) + "' }"; - return stream; -} - std::ostream& operator<<(std::ostream& stream, const TableState& tv) { return stream << static_cast::type>(tv); @@ -283,15 +217,4 @@ std::ostream& operator<<(std::ostream& stream, const TypePackVar& tv) return stream << toString(tv); } -std::ostream& operator<<(std::ostream& lhs, const TypeErrorData& ted) -{ - Luau::visit( - [&](const auto& a) { - lhs << a; - }, - ted); - - return lhs; -} - } // namespace Luau diff --git a/Analysis/src/Module.cpp b/Analysis/src/Module.cpp index 0787d3a4..6bb45245 100644 --- a/Analysis/src/Module.cpp +++ b/Analysis/src/Module.cpp @@ -2,6 +2,7 @@ #include "Luau/Module.h" #include "Luau/Common.h" +#include "Luau/Clone.h" #include "Luau/RecursionCounter.h" #include "Luau/Scope.h" #include "Luau/TypeInfer.h" @@ -12,7 +13,6 @@ #include LUAU_FASTFLAGVARIABLE(DebugLuauFreezeArena, false) -LUAU_FASTINTVARIABLE(LuauTypeCloneRecursionLimit, 300) LUAU_FASTFLAGVARIABLE(LuauCloneDeclaredGlobals, false) namespace Luau @@ -113,363 +113,6 @@ TypePackId TypeArena::addTypePack(TypePackVar tp) return allocated; } -namespace -{ - -struct TypePackCloner; - -/* - * Both TypeCloner and TypePackCloner work by depositing the requested type variable into the appropriate 'seen' set. - * They do not return anything because their sole consumer (the deepClone function) already has a pointer into this storage. - */ - -struct TypeCloner -{ - TypeCloner(TypeArena& dest, TypeId typeId, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) - : dest(dest) - , typeId(typeId) - , seenTypes(seenTypes) - , seenTypePacks(seenTypePacks) - , cloneState(cloneState) - { - } - - TypeArena& dest; - TypeId typeId; - SeenTypes& seenTypes; - SeenTypePacks& seenTypePacks; - CloneState& cloneState; - - template - void defaultClone(const T& t); - - void operator()(const Unifiable::Free& t); - void operator()(const Unifiable::Generic& t); - void operator()(const Unifiable::Bound& t); - void operator()(const Unifiable::Error& t); - void operator()(const PrimitiveTypeVar& t); - void operator()(const SingletonTypeVar& t); - void operator()(const FunctionTypeVar& t); - void operator()(const TableTypeVar& t); - void operator()(const MetatableTypeVar& t); - void operator()(const ClassTypeVar& t); - void operator()(const AnyTypeVar& t); - void operator()(const UnionTypeVar& t); - void operator()(const IntersectionTypeVar& t); - void operator()(const LazyTypeVar& t); -}; - -struct TypePackCloner -{ - TypeArena& dest; - TypePackId typePackId; - SeenTypes& seenTypes; - SeenTypePacks& seenTypePacks; - CloneState& cloneState; - - TypePackCloner(TypeArena& dest, TypePackId typePackId, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) - : dest(dest) - , typePackId(typePackId) - , seenTypes(seenTypes) - , seenTypePacks(seenTypePacks) - , cloneState(cloneState) - { - } - - template - void defaultClone(const T& t) - { - TypePackId cloned = dest.addTypePack(TypePackVar{t}); - seenTypePacks[typePackId] = cloned; - } - - void operator()(const Unifiable::Free& t) - { - cloneState.encounteredFreeType = true; - - TypePackId err = getSingletonTypes().errorRecoveryTypePack(getSingletonTypes().anyTypePack); - TypePackId cloned = dest.addTypePack(*err); - seenTypePacks[typePackId] = cloned; - } - - void operator()(const Unifiable::Generic& t) - { - defaultClone(t); - } - void operator()(const Unifiable::Error& t) - { - defaultClone(t); - } - - // While we are a-cloning, we can flatten out bound TypeVars and make things a bit tighter. - // We just need to be sure that we rewrite pointers both to the binder and the bindee to the same pointer. - void operator()(const Unifiable::Bound& t) - { - TypePackId cloned = clone(t.boundTo, dest, seenTypes, seenTypePacks, cloneState); - seenTypePacks[typePackId] = cloned; - } - - void operator()(const VariadicTypePack& t) - { - TypePackId cloned = dest.addTypePack(TypePackVar{VariadicTypePack{clone(t.ty, dest, seenTypes, seenTypePacks, cloneState)}}); - seenTypePacks[typePackId] = cloned; - } - - void operator()(const TypePack& t) - { - TypePackId cloned = dest.addTypePack(TypePack{}); - TypePack* destTp = getMutable(cloned); - LUAU_ASSERT(destTp != nullptr); - seenTypePacks[typePackId] = cloned; - - for (TypeId ty : t.head) - destTp->head.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); - - if (t.tail) - destTp->tail = clone(*t.tail, dest, seenTypes, seenTypePacks, cloneState); - } -}; - -template -void TypeCloner::defaultClone(const T& t) -{ - TypeId cloned = dest.addType(t); - seenTypes[typeId] = cloned; -} - -void TypeCloner::operator()(const Unifiable::Free& t) -{ - cloneState.encounteredFreeType = true; - TypeId err = getSingletonTypes().errorRecoveryType(getSingletonTypes().anyType); - TypeId cloned = dest.addType(*err); - seenTypes[typeId] = cloned; -} - -void TypeCloner::operator()(const Unifiable::Generic& t) -{ - defaultClone(t); -} - -void TypeCloner::operator()(const Unifiable::Bound& t) -{ - TypeId boundTo = clone(t.boundTo, dest, seenTypes, seenTypePacks, cloneState); - seenTypes[typeId] = boundTo; -} - -void TypeCloner::operator()(const Unifiable::Error& t) -{ - defaultClone(t); -} - -void TypeCloner::operator()(const PrimitiveTypeVar& t) -{ - defaultClone(t); -} - -void TypeCloner::operator()(const SingletonTypeVar& t) -{ - defaultClone(t); -} - -void TypeCloner::operator()(const FunctionTypeVar& t) -{ - TypeId result = dest.addType(FunctionTypeVar{TypeLevel{0, 0}, {}, {}, nullptr, nullptr, t.definition, t.hasSelf}); - FunctionTypeVar* ftv = getMutable(result); - LUAU_ASSERT(ftv != nullptr); - - seenTypes[typeId] = result; - - for (TypeId generic : t.generics) - ftv->generics.push_back(clone(generic, dest, seenTypes, seenTypePacks, cloneState)); - - for (TypePackId genericPack : t.genericPacks) - ftv->genericPacks.push_back(clone(genericPack, dest, seenTypes, seenTypePacks, cloneState)); - - ftv->tags = t.tags; - ftv->argTypes = clone(t.argTypes, dest, seenTypes, seenTypePacks, cloneState); - ftv->argNames = t.argNames; - ftv->retType = clone(t.retType, dest, seenTypes, seenTypePacks, cloneState); -} - -void TypeCloner::operator()(const TableTypeVar& t) -{ - // If table is now bound to another one, we ignore the content of the original - if (t.boundTo) - { - TypeId boundTo = clone(*t.boundTo, dest, seenTypes, seenTypePacks, cloneState); - seenTypes[typeId] = boundTo; - return; - } - - TypeId result = dest.addType(TableTypeVar{}); - TableTypeVar* ttv = getMutable(result); - LUAU_ASSERT(ttv != nullptr); - - *ttv = t; - - seenTypes[typeId] = result; - - ttv->level = TypeLevel{0, 0}; - - for (const auto& [name, prop] : t.props) - ttv->props[name] = {clone(prop.type, dest, seenTypes, seenTypePacks, cloneState), prop.deprecated, {}, prop.location, prop.tags}; - - if (t.indexer) - ttv->indexer = TableIndexer{clone(t.indexer->indexType, dest, seenTypes, seenTypePacks, cloneState), - clone(t.indexer->indexResultType, dest, seenTypes, seenTypePacks, cloneState)}; - - for (TypeId& arg : ttv->instantiatedTypeParams) - arg = clone(arg, dest, seenTypes, seenTypePacks, cloneState); - - for (TypePackId& arg : ttv->instantiatedTypePackParams) - arg = clone(arg, dest, seenTypes, seenTypePacks, cloneState); - - if (ttv->state == TableState::Free) - { - cloneState.encounteredFreeType = true; - - ttv->state = TableState::Sealed; - } - - ttv->definitionModuleName = t.definitionModuleName; - ttv->methodDefinitionLocations = t.methodDefinitionLocations; - ttv->tags = t.tags; -} - -void TypeCloner::operator()(const MetatableTypeVar& t) -{ - TypeId result = dest.addType(MetatableTypeVar{}); - MetatableTypeVar* mtv = getMutable(result); - seenTypes[typeId] = result; - - mtv->table = clone(t.table, dest, seenTypes, seenTypePacks, cloneState); - mtv->metatable = clone(t.metatable, dest, seenTypes, seenTypePacks, cloneState); -} - -void TypeCloner::operator()(const ClassTypeVar& t) -{ - TypeId result = dest.addType(ClassTypeVar{t.name, {}, std::nullopt, std::nullopt, t.tags, t.userData}); - ClassTypeVar* ctv = getMutable(result); - - seenTypes[typeId] = result; - - for (const auto& [name, prop] : t.props) - ctv->props[name] = {clone(prop.type, dest, seenTypes, seenTypePacks, cloneState), prop.deprecated, {}, prop.location, prop.tags}; - - if (t.parent) - ctv->parent = clone(*t.parent, dest, seenTypes, seenTypePacks, cloneState); - - if (t.metatable) - ctv->metatable = clone(*t.metatable, dest, seenTypes, seenTypePacks, cloneState); -} - -void TypeCloner::operator()(const AnyTypeVar& t) -{ - defaultClone(t); -} - -void TypeCloner::operator()(const UnionTypeVar& t) -{ - std::vector options; - options.reserve(t.options.size()); - - for (TypeId ty : t.options) - options.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); - - TypeId result = dest.addType(UnionTypeVar{std::move(options)}); - seenTypes[typeId] = result; -} - -void TypeCloner::operator()(const IntersectionTypeVar& t) -{ - TypeId result = dest.addType(IntersectionTypeVar{}); - seenTypes[typeId] = result; - - IntersectionTypeVar* option = getMutable(result); - LUAU_ASSERT(option != nullptr); - - for (TypeId ty : t.parts) - option->parts.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState)); -} - -void TypeCloner::operator()(const LazyTypeVar& t) -{ - defaultClone(t); -} - -} // anonymous namespace - -TypePackId clone(TypePackId tp, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) -{ - if (tp->persistent) - return tp; - - RecursionLimiter _ra(&cloneState.recursionCount, FInt::LuauTypeCloneRecursionLimit); - - TypePackId& res = seenTypePacks[tp]; - - if (res == nullptr) - { - TypePackCloner cloner{dest, tp, seenTypes, seenTypePacks, cloneState}; - Luau::visit(cloner, tp->ty); // Mutates the storage that 'res' points into. - } - - return res; -} - -TypeId clone(TypeId typeId, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) -{ - if (typeId->persistent) - return typeId; - - RecursionLimiter _ra(&cloneState.recursionCount, FInt::LuauTypeCloneRecursionLimit); - - TypeId& res = seenTypes[typeId]; - - if (res == nullptr) - { - TypeCloner cloner{dest, typeId, seenTypes, seenTypePacks, cloneState}; - Luau::visit(cloner, typeId->ty); // Mutates the storage that 'res' points into. - - // Persistent types are not being cloned and we get the original type back which might be read-only - if (!res->persistent) - asMutable(res)->documentationSymbol = typeId->documentationSymbol; - } - - return res; -} - -TypeFun clone(const TypeFun& typeFun, TypeArena& dest, SeenTypes& seenTypes, SeenTypePacks& seenTypePacks, CloneState& cloneState) -{ - TypeFun result; - - for (auto param : typeFun.typeParams) - { - TypeId ty = clone(param.ty, dest, seenTypes, seenTypePacks, cloneState); - std::optional defaultValue; - - if (param.defaultValue) - defaultValue = clone(*param.defaultValue, dest, seenTypes, seenTypePacks, cloneState); - - result.typeParams.push_back({ty, defaultValue}); - } - - for (auto param : typeFun.typePackParams) - { - TypePackId tp = clone(param.tp, dest, seenTypes, seenTypePacks, cloneState); - std::optional defaultValue; - - if (param.defaultValue) - defaultValue = clone(*param.defaultValue, dest, seenTypes, seenTypePacks, cloneState); - - result.typePackParams.push_back({tp, defaultValue}); - } - - result.type = clone(typeFun.type, dest, seenTypes, seenTypePacks, cloneState); - - return result; -} - ScopePtr Module::getModuleScope() const { LUAU_ASSERT(!scopes.empty()); diff --git a/Analysis/src/TxnLog.cpp b/Analysis/src/TxnLog.cpp index 876f5f05..5fbb596d 100644 --- a/Analysis/src/TxnLog.cpp +++ b/Analysis/src/TxnLog.cpp @@ -7,6 +7,8 @@ #include #include +LUAU_FASTFLAGVARIABLE(LuauTxnLogPreserveOwner, false) + namespace Luau { @@ -78,11 +80,32 @@ void TxnLog::concat(TxnLog rhs) void TxnLog::commit() { - for (auto& [ty, rep] : typeVarChanges) - *asMutable(ty) = rep.get()->pending; + if (FFlag::LuauTxnLogPreserveOwner) + { + for (auto& [ty, rep] : typeVarChanges) + { + TypeArena* owningArena = ty->owningArena; + TypeVar* mtv = asMutable(ty); + *mtv = rep.get()->pending; + mtv->owningArena = owningArena; + } - for (auto& [tp, rep] : typePackChanges) - *asMutable(tp) = rep.get()->pending; + for (auto& [tp, rep] : typePackChanges) + { + TypeArena* owningArena = tp->owningArena; + TypePackVar* mpv = asMutable(tp); + *mpv = rep.get()->pending; + mpv->owningArena = owningArena; + } + } + else + { + for (auto& [ty, rep] : typeVarChanges) + *asMutable(ty) = rep.get()->pending; + + for (auto& [tp, rep] : typePackChanges) + *asMutable(tp) = rep.get()->pending; + } clear(); } diff --git a/Analysis/src/TypeInfer.cpp b/Analysis/src/TypeInfer.cpp index 6df6bff0..10930248 100644 --- a/Analysis/src/TypeInfer.cpp +++ b/Analysis/src/TypeInfer.cpp @@ -22,6 +22,9 @@ LUAU_FASTINTVARIABLE(LuauTypeInferRecursionLimit, 500) LUAU_FASTINTVARIABLE(LuauTypeInferTypePackLoopLimit, 5000) LUAU_FASTINTVARIABLE(LuauCheckRecursionLimit, 500) LUAU_FASTFLAG(LuauKnowsTheDataModel3) +LUAU_FASTFLAG(LuauSeparateTypechecks) +LUAU_FASTFLAG(LuauAutocompleteSingletonTypes) +LUAU_FASTFLAGVARIABLE(LuauCyclicModuleTypeSurface, false) LUAU_FASTFLAGVARIABLE(LuauEqConstraint, false) LUAU_FASTFLAGVARIABLE(LuauWeakEqConstraint, false) // Eventually removed as false. LUAU_FASTFLAGVARIABLE(DebugLuauFreezeDuringUnification, false) @@ -35,7 +38,7 @@ LUAU_FASTFLAGVARIABLE(LuauExpectedTypesOfProperties, false) LUAU_FASTFLAGVARIABLE(LuauErrorRecoveryType, false) LUAU_FASTFLAGVARIABLE(LuauOnlyMutateInstantiatedTables, false) LUAU_FASTFLAGVARIABLE(LuauPropertiesGetExpectedType, false) -LUAU_FASTFLAGVARIABLE(LuauStatFunctionSimplify3, false) +LUAU_FASTFLAGVARIABLE(LuauStatFunctionSimplify4, false) LUAU_FASTFLAGVARIABLE(LuauUnsealedTableLiteral, false) LUAU_FASTFLAG(LuauTypeMismatchModuleName) LUAU_FASTFLAGVARIABLE(LuauTwoPassAliasDefinitionFix, false) @@ -46,6 +49,7 @@ LUAU_FASTFLAGVARIABLE(LuauDoNotTryToReduce, false) LUAU_FASTFLAGVARIABLE(LuauDoNotAccidentallyDependOnPointerOrdering, false) LUAU_FASTFLAGVARIABLE(LuauFixArgumentCountMismatchAmountWithGenericTypes, false) LUAU_FASTFLAGVARIABLE(LuauFixIncorrectLineNumberDuplicateType, false) +LUAU_FASTFLAGVARIABLE(LuauCheckImplicitNumbericKeys, false) LUAU_FASTFLAG(LuauAnyInIsOptionalIsOptional) LUAU_FASTFLAGVARIABLE(LuauDecoupleOperatorInferenceFromUnifiedTypeInference, false) LUAU_FASTFLAGVARIABLE(LuauArgCountMismatchSaysAtLeastWhenVariadic, false) @@ -53,6 +57,11 @@ LUAU_FASTFLAGVARIABLE(LuauArgCountMismatchSaysAtLeastWhenVariadic, false) namespace Luau { +const char* TimeLimitError::what() const throw() +{ + return "Typeinfer failed to complete in allotted time"; +} + static bool typeCouldHaveMetatable(TypeId ty) { return get(follow(ty)) || get(follow(ty)) || get(follow(ty)); @@ -251,6 +260,12 @@ ModulePtr TypeChecker::check(const SourceModule& module, Mode mode, std::optiona currentModule.reset(new Module()); currentModule->type = module.type; + if (FFlag::LuauSeparateTypechecks) + { + currentModule->allocator = module.allocator; + currentModule->names = module.names; + } + iceHandler->moduleName = module.name; ScopePtr parentScope = environmentScope.value_or(globalScope); @@ -271,7 +286,21 @@ ModulePtr TypeChecker::check(const SourceModule& module, Mode mode, std::optiona if (prepareModuleScope) prepareModuleScope(module.name, currentModule->getModuleScope()); - checkBlock(moduleScope, *module.root); + if (FFlag::LuauSeparateTypechecks) + { + try + { + checkBlock(moduleScope, *module.root); + } + catch (const TimeLimitError&) + { + currentModule->timeout = true; + } + } + else + { + checkBlock(moduleScope, *module.root); + } if (get(follow(moduleScope->returnType))) moduleScope->returnType = addTypePack(TypePack{{}, std::nullopt}); @@ -366,6 +395,9 @@ void TypeChecker::check(const ScopePtr& scope, const AstStat& program) } else ice("Unknown AstStat"); + + if (FFlag::LuauSeparateTypechecks && finishTime && TimeTrace::getClock() > *finishTime) + throw TimeLimitError(); } // This particular overload is for do...end. If you need to not increase the scope level, use checkBlock directly. @@ -1115,22 +1147,18 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco scope->bindings[name->local] = {anyIfNonstrict(quantify(funScope, ty, name->local->location)), name->local->location}; return; } - else if (auto name = function.name->as(); name && FFlag::LuauStatFunctionSimplify3) + else if (auto name = function.name->as(); name && FFlag::LuauStatFunctionSimplify4) { TypeId exprTy = checkExpr(scope, *name->expr).type; TableTypeVar* ttv = getMutableTableType(exprTy); - if (!ttv) + + if (!getIndexTypeFromType(scope, exprTy, name->index.value, name->indexLocation, false)) { - if (isTableIntersection(exprTy)) + if (ttv || isTableIntersection(exprTy)) reportError(TypeError{function.location, CannotExtendTable{exprTy, CannotExtendTable::Property, name->index.value}}); - else if (!get(exprTy) && !get(exprTy)) + else reportError(TypeError{function.location, OnlyTablesCanHaveMethods{exprTy}}); } - else if (ttv->state == TableState::Sealed) - { - if (!getIndexTypeFromType(scope, exprTy, name->index.value, name->indexLocation, false)) - reportError(TypeError{function.location, CannotExtendTable{exprTy, CannotExtendTable::Property, name->index.value}}); - } ty = follow(ty); @@ -1153,7 +1181,7 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco if (ttv && ttv->state != TableState::Sealed) ttv->props[name->index.value] = {follow(quantify(funScope, ty, name->indexLocation)), /* deprecated */ false, {}, name->indexLocation}; } - else if (FFlag::LuauStatFunctionSimplify3) + else if (FFlag::LuauStatFunctionSimplify4) { LUAU_ASSERT(function.name->is()); @@ -1163,7 +1191,7 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco } else if (function.func->self) { - LUAU_ASSERT(!FFlag::LuauStatFunctionSimplify3); + LUAU_ASSERT(!FFlag::LuauStatFunctionSimplify4); AstExprIndexName* indexName = function.name->as(); if (!indexName) @@ -1202,7 +1230,7 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco } else { - LUAU_ASSERT(!FFlag::LuauStatFunctionSimplify3); + LUAU_ASSERT(!FFlag::LuauStatFunctionSimplify4); TypeId leftType = checkLValueBinding(scope, *function.name); @@ -2030,7 +2058,11 @@ TypeId TypeChecker::checkExprTable( indexer = expectedTable->indexer; if (indexer) + { + if (FFlag::LuauCheckImplicitNumbericKeys) + unify(numberType, indexer->indexType, value->location); unify(valueType, indexer->indexResultType, value->location); + } else indexer = TableIndexer{numberType, anyIfNonstrict(valueType)}; } @@ -2984,35 +3016,33 @@ TypeId TypeChecker::checkFunctionName(const ScopePtr& scope, AstExpr& funName, T else if (auto indexName = funName.as()) { TypeId lhsType = checkExpr(scope, *indexName->expr).type; - if (get(lhsType) || get(lhsType)) + + if (!FFlag::LuauStatFunctionSimplify4 && (get(lhsType) || get(lhsType))) return lhsType; TableTypeVar* ttv = getMutableTableType(lhsType); - if (!ttv) + + if (FFlag::LuauStatFunctionSimplify4) { - if (!FFlag::LuauErrorRecoveryType && !isTableIntersection(lhsType)) - // This error now gets reported when we check the function body. - reportError(TypeError{funName.location, OnlyTablesCanHaveMethods{lhsType}}); - - return errorRecoveryType(scope); - } - - if (FFlag::LuauStatFunctionSimplify3) - { - if (lhsType->persistent) - return errorRecoveryType(scope); - - // Cannot extend sealed table, but we dont report an error here because it will be reported during AstStatFunction check - if (ttv->state == TableState::Sealed) + if (!ttv || ttv->state == TableState::Sealed) { - if (ttv->indexer && isPrim(ttv->indexer->indexType, PrimitiveTypeVar::String)) - return ttv->indexer->indexResultType; - else - return errorRecoveryType(scope); + if (auto ty = getIndexTypeFromType(scope, lhsType, indexName->index.value, indexName->indexLocation, false)) + return *ty; + + return errorRecoveryType(scope); } } else { + if (!ttv) + { + if (!FFlag::LuauErrorRecoveryType && !isTableIntersection(lhsType)) + // This error now gets reported when we check the function body. + reportError(TypeError{funName.location, OnlyTablesCanHaveMethods{lhsType}}); + + return errorRecoveryType(scope); + } + if (lhsType->persistent || ttv->state == TableState::Sealed) return errorRecoveryType(scope); } @@ -3020,7 +3050,12 @@ TypeId TypeChecker::checkFunctionName(const ScopePtr& scope, AstExpr& funName, T Name name = indexName->index.value; if (ttv->props.count(name)) - return errorRecoveryType(scope); + { + if (FFlag::LuauStatFunctionSimplify4) + return ttv->props[name].type; + else + return errorRecoveryType(scope); + } Property& property = ttv->props[name]; @@ -4155,6 +4190,20 @@ TypeId TypeChecker::checkRequire(const ScopePtr& scope, const ModuleInfo& module return anyType; } + // Types of requires that transitively refer to current module have to be replaced with 'any' + std::string humanReadableName; + + if (FFlag::LuauCyclicModuleTypeSurface) + { + humanReadableName = resolver->getHumanReadableModuleName(moduleInfo.name); + + for (const auto& [location, path] : requireCycles) + { + if (!path.empty() && path.front() == humanReadableName) + return anyType; + } + } + ModulePtr module = resolver->getModule(moduleInfo.name); if (!module) { @@ -4163,8 +4212,15 @@ TypeId TypeChecker::checkRequire(const ScopePtr& scope, const ModuleInfo& module // we will already have reported the error. if (!resolver->moduleExists(moduleInfo.name) && !moduleInfo.optional) { - std::string reportedModulePath = resolver->getHumanReadableModuleName(moduleInfo.name); - reportError(TypeError{location, UnknownRequire{reportedModulePath}}); + if (FFlag::LuauCyclicModuleTypeSurface) + { + reportError(TypeError{location, UnknownRequire{humanReadableName}}); + } + else + { + std::string reportedModulePath = resolver->getHumanReadableModuleName(moduleInfo.name); + reportError(TypeError{location, UnknownRequire{reportedModulePath}}); + } } return errorRecoveryType(scope); @@ -4172,8 +4228,15 @@ TypeId TypeChecker::checkRequire(const ScopePtr& scope, const ModuleInfo& module if (module->type != SourceCode::Module) { - std::string humanReadableName = resolver->getHumanReadableModuleName(moduleInfo.name); - reportError(location, IllegalRequire{humanReadableName, "Module is not a ModuleScript. It cannot be required."}); + if (FFlag::LuauCyclicModuleTypeSurface) + { + reportError(location, IllegalRequire{humanReadableName, "Module is not a ModuleScript. It cannot be required."}); + } + else + { + std::string humanReadableName = resolver->getHumanReadableModuleName(moduleInfo.name); + reportError(location, IllegalRequire{humanReadableName, "Module is not a ModuleScript. It cannot be required."}); + } return errorRecoveryType(scope); } @@ -4185,8 +4248,15 @@ TypeId TypeChecker::checkRequire(const ScopePtr& scope, const ModuleInfo& module std::optional moduleType = first(modulePack); if (!moduleType) { - std::string humanReadableName = resolver->getHumanReadableModuleName(moduleInfo.name); - reportError(location, IllegalRequire{humanReadableName, "Module does not return exactly 1 value. It cannot be required."}); + if (FFlag::LuauCyclicModuleTypeSurface) + { + reportError(location, IllegalRequire{humanReadableName, "Module does not return exactly 1 value. It cannot be required."}); + } + else + { + std::string humanReadableName = resolver->getHumanReadableModuleName(moduleInfo.name); + reportError(location, IllegalRequire{humanReadableName, "Module does not return exactly 1 value. It cannot be required."}); + } return errorRecoveryType(scope); } @@ -4629,7 +4699,9 @@ TypeId TypeChecker::freshType(TypeLevel level) TypeId TypeChecker::singletonType(bool value) { - // TODO: cache singleton types + if (FFlag::LuauAutocompleteSingletonTypes) + return value ? getSingletonTypes().trueType : getSingletonTypes().falseType; + return currentModule->internalTypes.addType(TypeVar(SingletonTypeVar(BooleanSingleton{value}))); } diff --git a/Analysis/src/TypeVar.cpp b/Analysis/src/TypeVar.cpp index 36545ad9..dbc412fc 100644 --- a/Analysis/src/TypeVar.cpp +++ b/Analysis/src/TypeVar.cpp @@ -652,6 +652,8 @@ static TypeVar numberType_{PrimitiveTypeVar{PrimitiveTypeVar::Number}, /*persist static TypeVar stringType_{PrimitiveTypeVar{PrimitiveTypeVar::String}, /*persistent*/ true}; static TypeVar booleanType_{PrimitiveTypeVar{PrimitiveTypeVar::Boolean}, /*persistent*/ true}; static TypeVar threadType_{PrimitiveTypeVar{PrimitiveTypeVar::Thread}, /*persistent*/ true}; +static TypeVar trueType_{SingletonTypeVar{BooleanSingleton{true}}, /*persistent*/ true}; +static TypeVar falseType_{SingletonTypeVar{BooleanSingleton{false}}, /*persistent*/ true}; static TypeVar anyType_{AnyTypeVar{}}; static TypeVar errorType_{ErrorTypeVar{}}; static TypeVar optionalNumberType_{UnionTypeVar{{&numberType_, &nilType_}}}; @@ -665,6 +667,8 @@ SingletonTypes::SingletonTypes() , stringType(&stringType_) , booleanType(&booleanType_) , threadType(&threadType_) + , trueType(&trueType_) + , falseType(&falseType_) , anyType(&anyType_) , optionalNumberType(&optionalNumberType_) , anyTypePack(&anyTypePack_) diff --git a/Ast/include/Luau/TimeTrace.h b/Ast/include/Luau/TimeTrace.h index 5018456f..9f7b2bdf 100644 --- a/Ast/include/Luau/TimeTrace.h +++ b/Ast/include/Luau/TimeTrace.h @@ -9,14 +9,21 @@ LUAU_FASTFLAG(DebugLuauTimeTracing) +namespace Luau +{ +namespace TimeTrace +{ +double getClock(); +uint32_t getClockMicroseconds(); +} // namespace TimeTrace +} // namespace Luau + #if defined(LUAU_ENABLE_TIME_TRACE) namespace Luau { namespace TimeTrace { -uint32_t getClockMicroseconds(); - struct Token { const char* name; diff --git a/Ast/src/Parser.cpp b/Ast/src/Parser.cpp index f6dfd904..f9d32178 100644 --- a/Ast/src/Parser.cpp +++ b/Ast/src/Parser.cpp @@ -10,6 +10,7 @@ // See docs/SyntaxChanges.md for an explanation. LUAU_FASTINTVARIABLE(LuauRecursionLimit, 1000) LUAU_FASTINTVARIABLE(LuauParseErrorLimit, 100) +LUAU_FASTFLAGVARIABLE(LuauParseRecoverUnexpectedPack, false) namespace Luau { @@ -1420,6 +1421,11 @@ AstType* Parser::parseTypeAnnotation(TempVector& parts, const Location parts.push_back(parseSimpleTypeAnnotation(/* allowPack= */ false).type); isIntersection = true; } + else if (FFlag::LuauParseRecoverUnexpectedPack && c == Lexeme::Dot3) + { + report(lexer.current().location, "Unexpected '...' after type annotation"); + nextLexeme(); + } else break; } @@ -1536,6 +1542,11 @@ AstTypeOrPack Parser::parseSimpleTypeAnnotation(bool allowPack) prefix = name.name; name = parseIndexName("field name", pointPosition); } + else if (FFlag::LuauParseRecoverUnexpectedPack && lexer.current().type == Lexeme::Dot3) + { + report(lexer.current().location, "Unexpected '...' after type name; type pack is not allowed in this context"); + nextLexeme(); + } else if (name.name == "typeof") { Lexeme typeofBegin = lexer.current(); diff --git a/Ast/src/TimeTrace.cpp b/Ast/src/TimeTrace.cpp index 19564f05..e3807683 100644 --- a/Ast/src/TimeTrace.cpp +++ b/Ast/src/TimeTrace.cpp @@ -26,9 +26,6 @@ #include LUAU_FASTFLAGVARIABLE(DebugLuauTimeTracing, false) - -#if defined(LUAU_ENABLE_TIME_TRACE) - namespace Luau { namespace TimeTrace @@ -67,6 +64,14 @@ static double getClockTimestamp() #endif } +double getClock() +{ + static double period = getClockPeriod(); + static double start = getClockTimestamp(); + + return (getClockTimestamp() - start) * period; +} + uint32_t getClockMicroseconds() { static double period = getClockPeriod() * 1e6; @@ -74,7 +79,15 @@ uint32_t getClockMicroseconds() return uint32_t((getClockTimestamp() - start) * period); } +} // namespace TimeTrace +} // namespace Luau +#if defined(LUAU_ENABLE_TIME_TRACE) + +namespace Luau +{ +namespace TimeTrace +{ struct GlobalContext { GlobalContext() = default; diff --git a/Compiler/src/ConstantFolding.cpp b/Compiler/src/ConstantFolding.cpp index 60a7c169..35ea0bf0 100644 --- a/Compiler/src/ConstantFolding.cpp +++ b/Compiler/src/ConstantFolding.cpp @@ -290,7 +290,8 @@ struct ConstantVisitor : AstVisitor Constant la = analyze(expr->left); Constant ra = analyze(expr->right); - if (la.type != Constant::Type_Unknown && ra.type != Constant::Type_Unknown) + // note: ra doesn't need to be constant to fold and/or + if (la.type != Constant::Type_Unknown) foldBinary(result, expr->op, la, ra); } else if (AstExprTypeAssertion* expr = node->as()) diff --git a/Sources.cmake b/Sources.cmake index 59b38497..6f110f1f 100644 --- a/Sources.cmake +++ b/Sources.cmake @@ -47,6 +47,7 @@ target_sources(Luau.Analysis PRIVATE Analysis/include/Luau/Autocomplete.h Analysis/include/Luau/BuiltinDefinitions.h Analysis/include/Luau/Config.h + Analysis/include/Luau/Clone.h Analysis/include/Luau/Documentation.h Analysis/include/Luau/Error.h Analysis/include/Luau/FileResolver.h @@ -85,6 +86,7 @@ target_sources(Luau.Analysis PRIVATE Analysis/src/Autocomplete.cpp Analysis/src/BuiltinDefinitions.cpp Analysis/src/Config.cpp + Analysis/src/Clone.cpp Analysis/src/Error.cpp Analysis/src/Frontend.cpp Analysis/src/IostreamHelpers.cpp diff --git a/VM/src/lfunc.h b/VM/src/lfunc.h index 8047cebe..a260d00a 100644 --- a/VM/src/lfunc.h +++ b/VM/src/lfunc.h @@ -14,6 +14,6 @@ LUAI_FUNC UpVal* luaF_findupval(lua_State* L, StkId level); LUAI_FUNC void luaF_close(lua_State* L, StkId level); LUAI_FUNC void luaF_freeproto(lua_State* L, Proto* f, struct lua_Page* page); LUAI_FUNC void luaF_freeclosure(lua_State* L, Closure* c, struct lua_Page* page); -void luaF_unlinkupval(UpVal* uv); +LUAI_FUNC void luaF_unlinkupval(UpVal* uv); LUAI_FUNC void luaF_freeupval(lua_State* L, UpVal* uv, struct lua_Page* page); LUAI_FUNC const LocVar* luaF_getlocal(const Proto* func, int local_number, int pc); diff --git a/VM/src/ltablib.cpp b/VM/src/ltablib.cpp index 241a99e3..41887f4b 100644 --- a/VM/src/ltablib.cpp +++ b/VM/src/ltablib.cpp @@ -201,7 +201,7 @@ static int tmove(lua_State* L) void (*telemetrycb)(lua_State* L, int f, int e, int t, int nf, int nt) = lua_table_move_telemetry; - if (DFFlag::LuauTableMoveTelemetry2 && telemetrycb) + if (DFFlag::LuauTableMoveTelemetry2 && telemetrycb && e >= f) { int nf = lua_objlen(L, 1); int nt = lua_objlen(L, tt); diff --git a/tests/Autocomplete.test.cpp b/tests/Autocomplete.test.cpp index 4e8a1d55..2e7902f5 100644 --- a/tests/Autocomplete.test.cpp +++ b/tests/Autocomplete.test.cpp @@ -14,6 +14,7 @@ LUAU_FASTFLAG(LuauTraceTypesInNonstrictMode2) LUAU_FASTFLAG(LuauSetMetatableDoesNotTimeTravel) +LUAU_FASTFLAG(LuauSeparateTypechecks) using namespace Luau; @@ -25,6 +26,11 @@ static std::optional nullCallback(std::string tag, std::op template struct ACFixtureImpl : BaseType { + ACFixtureImpl() + : Fixture(true, true) + { + } + AutocompleteResult autocomplete(unsigned row, unsigned column) { return Luau::autocomplete(this->frontend, "MainModule", Position{row, column}, nullCallback); @@ -72,7 +78,25 @@ struct ACFixtureImpl : BaseType } LUAU_ASSERT("Digit expected after @ symbol" && prevChar != '@'); - return Fixture::check(filteredSource); + return BaseType::check(filteredSource); + } + + LoadDefinitionFileResult loadDefinition(const std::string& source) + { + if (FFlag::LuauSeparateTypechecks) + { + TypeChecker& typeChecker = this->frontend.typeCheckerForAutocomplete; + unfreeze(typeChecker.globalTypes); + LoadDefinitionFileResult result = loadDefinitionFile(typeChecker, typeChecker.globalScope, source, "@test"); + freeze(typeChecker.globalTypes); + + REQUIRE_MESSAGE(result.success, "loadDefinition: unable to load definition file"); + return result; + } + else + { + return BaseType::loadDefinition(source); + } } const Position& getPosition(char marker) const @@ -2496,7 +2520,7 @@ local t = { CHECK(ac.entryMap.count("second")); } -TEST_CASE_FIXTURE(Fixture, "autocomplete_documentation_symbols") +TEST_CASE_FIXTURE(ACFixture, "autocomplete_documentation_symbols") { loadDefinition(R"( declare y: { @@ -2504,13 +2528,11 @@ TEST_CASE_FIXTURE(Fixture, "autocomplete_documentation_symbols") } )"); - fileResolver.source["Module/A"] = R"( - local a = y. - )"; + check(R"( + local a = y.@1 + )"); - frontend.check("Module/A"); - - auto ac = autocomplete(frontend, "Module/A", Position{1, 21}, nullCallback); + auto ac = autocomplete('1'); REQUIRE(ac.entryMap.count("x")); CHECK_EQ(ac.entryMap["x"].documentationSymbol, "@test/global/y.x"); @@ -2736,6 +2758,107 @@ TEST_CASE_FIXTURE(ACFixture, "autocomplete_on_string_singletons") CHECK(ac.entryMap.count("format")); } +TEST_CASE_FIXTURE(ACFixture, "autocomplete_string_singletons") +{ + ScopedFastFlag luauAutocompleteSingletonTypes{"LuauAutocompleteSingletonTypes", true}; + ScopedFastFlag luauExpectedTypesOfProperties{"LuauExpectedTypesOfProperties", true}; + + check(R"( + type tag = "cat" | "dog" + local function f(a: tag) end + f("@1") + f(@2) + local x: tag = "@3" + )"); + + auto ac = autocomplete('1'); + + CHECK(ac.entryMap.count("cat")); + CHECK(ac.entryMap.count("dog")); + + ac = autocomplete('2'); + + CHECK(ac.entryMap.count("\"cat\"")); + CHECK(ac.entryMap.count("\"dog\"")); + + ac = autocomplete('3'); + + CHECK(ac.entryMap.count("cat")); + CHECK(ac.entryMap.count("dog")); + + check(R"( + type tagged = {tag:"cat", fieldx:number} | {tag:"dog", fieldy:number} + local x: tagged = {tag="@4"} + )"); + + ac = autocomplete('4'); + + CHECK(ac.entryMap.count("cat")); + CHECK(ac.entryMap.count("dog")); +} + +TEST_CASE_FIXTURE(ACFixture, "autocomplete_string_singleton_equality") +{ + ScopedFastFlag luauAutocompleteSingletonTypes{"LuauAutocompleteSingletonTypes", true}; + + check(R"( + type tagged = {tag:"cat", fieldx:number} | {tag:"dog", fieldy:number} + local x: tagged = {tag="cat", fieldx=2} + if x.tag == "@1" or "@2" ~= x.tag then end + )"); + + auto ac = autocomplete('1'); + + CHECK(ac.entryMap.count("cat")); + CHECK(ac.entryMap.count("dog")); + + ac = autocomplete('2'); + + CHECK(ac.entryMap.count("cat")); + CHECK(ac.entryMap.count("dog")); + + // CLI-48823: assignment to x.tag should also autocomplete, but union l-values are not supported yet +} + +TEST_CASE_FIXTURE(ACFixture, "autocomplete_boolean_singleton") +{ + ScopedFastFlag luauAutocompleteSingletonTypes{"LuauAutocompleteSingletonTypes", true}; + + check(R"( +local function f(x: true) end +f(@1) + )"); + + auto ac = autocomplete('1'); + + REQUIRE(ac.entryMap.count("true")); + CHECK(ac.entryMap["true"].typeCorrect == TypeCorrectKind::Correct); + REQUIRE(ac.entryMap.count("false")); + CHECK(ac.entryMap["false"].typeCorrect == TypeCorrectKind::None); +} + +TEST_CASE_FIXTURE(ACFixture, "autocomplete_string_singleton_escape") +{ + ScopedFastFlag luauAutocompleteSingletonTypes{"LuauAutocompleteSingletonTypes", true}; + + check(R"( + type tag = "strange\t\"cat\"" | 'nice\t"dog"' + local function f(x: tag) end + f(@1) + f("@2") + )"); + + auto ac = autocomplete('1'); + + CHECK(ac.entryMap.count("\"strange\\t\\\"cat\\\"\"")); + CHECK(ac.entryMap.count("\"nice\\t\\\"dog\\\"\"")); + + ac = autocomplete('2'); + + CHECK(ac.entryMap.count("strange\\t\\\"cat\\\"")); + CHECK(ac.entryMap.count("nice\\t\\\"dog\\\"")); +} + TEST_CASE_FIXTURE(ACFixture, "function_in_assignment_has_parentheses_2") { check(R"( diff --git a/tests/Compiler.test.cpp b/tests/Compiler.test.cpp index 3dc57da0..83dad729 100644 --- a/tests/Compiler.test.cpp +++ b/tests/Compiler.test.cpp @@ -1074,6 +1074,39 @@ RETURN R1 1 )"); } +TEST_CASE("AndOrFoldLeft") +{ + // constant folding and/or expression is possible even if just the left hand is constant + CHECK_EQ("\n" + compileFunction0("local a = false if a and b then b() end"), R"( +RETURN R0 0 +)"); + + CHECK_EQ("\n" + compileFunction0("local a = true if a or b then b() end"), R"( +GETIMPORT R0 1 +CALL R0 0 0 +RETURN R0 0 +)"); + + // however, if right hand side is constant we can't constant fold the entire expression + // (note that we don't need to evaluate the right hand side, but we do need a branch) + CHECK_EQ("\n" + compileFunction0("local a = false if b and a then b() end"), R"( +GETIMPORT R0 1 +JUMPIFNOT R0 +4 +RETURN R0 0 +GETIMPORT R0 1 +CALL R0 0 0 +RETURN R0 0 +)"); + + CHECK_EQ("\n" + compileFunction0("local a = true if b or a then b() end"), R"( +GETIMPORT R0 1 +JUMPIF R0 +0 +GETIMPORT R0 1 +CALL R0 0 0 +RETURN R0 0 +)"); +} + TEST_CASE("AndOrChainCodegen") { const char* source = R"( diff --git a/tests/Fixture.cpp b/tests/Fixture.cpp index a7e7ea39..9dc9feee 100644 --- a/tests/Fixture.cpp +++ b/tests/Fixture.cpp @@ -83,7 +83,7 @@ std::optional TestFileResolver::getEnvironmentForModule(const Modul return std::nullopt; } -Fixture::Fixture(bool freeze) +Fixture::Fixture(bool freeze, bool prepareAutocomplete) : sff_DebugLuauFreezeArena("DebugLuauFreezeArena", freeze) , frontend(&fileResolver, &configResolver, {/* retainFullTypeGraphs= */ true}) , typeChecker(frontend.typeChecker) @@ -93,8 +93,11 @@ Fixture::Fixture(bool freeze) configResolver.defaultConfig.parseOptions.captureComments = true; registerBuiltinTypes(frontend.typeChecker); + if (prepareAutocomplete) + registerBuiltinTypes(frontend.typeCheckerForAutocomplete); registerTestTypes(); Luau::freeze(frontend.typeChecker.globalTypes); + Luau::freeze(frontend.typeCheckerForAutocomplete.globalTypes); Luau::setPrintLine([](auto s) {}); } diff --git a/tests/Fixture.h b/tests/Fixture.h index 4e45a952..0d1233bf 100644 --- a/tests/Fixture.h +++ b/tests/Fixture.h @@ -91,7 +91,7 @@ struct TestConfigResolver : ConfigResolver struct Fixture { - explicit Fixture(bool freeze = true); + explicit Fixture(bool freeze = true, bool prepareAutocomplete = false); ~Fixture(); // Throws Luau::ParseErrors if the parse fails. diff --git a/tests/Frontend.test.cpp b/tests/Frontend.test.cpp index 8a59acd1..9fc0a005 100644 --- a/tests/Frontend.test.cpp +++ b/tests/Frontend.test.cpp @@ -384,6 +384,70 @@ TEST_CASE_FIXTURE(FrontendFixture, "cycle_error_paths") CHECK_EQ(ce2->cycle[1], "game/Gui/Modules/A"); } +TEST_CASE_FIXTURE(FrontendFixture, "cycle_incremental_type_surface") +{ + ScopedFastFlag luauCyclicModuleTypeSurface{"LuauCyclicModuleTypeSurface", true}; + + fileResolver.source["game/A"] = R"( + return {hello = 2} + )"; + + CheckResult result = frontend.check("game/A"); + LUAU_REQUIRE_NO_ERRORS(result); + + fileResolver.source["game/A"] = R"( + local me = require(game.A) + return {hello = 2} + )"; + frontend.markDirty("game/A"); + + result = frontend.check("game/A"); + LUAU_REQUIRE_ERRORS(result); + + auto ty = requireType("game/A", "me"); + CHECK_EQ(toString(ty), "any"); +} + +TEST_CASE_FIXTURE(FrontendFixture, "cycle_incremental_type_surface_longer") +{ + ScopedFastFlag luauCyclicModuleTypeSurface{"LuauCyclicModuleTypeSurface", true}; + + fileResolver.source["game/A"] = R"( + return {mod_a = 2} + )"; + + CheckResult result = frontend.check("game/A"); + LUAU_REQUIRE_NO_ERRORS(result); + + fileResolver.source["game/B"] = R"( + local me = require(game.A) + return {mod_b = 4} + )"; + + result = frontend.check("game/B"); + LUAU_REQUIRE_NO_ERRORS(result); + + fileResolver.source["game/A"] = R"( + local me = require(game.B) + return {mod_a_prime = 3} + )"; + + frontend.markDirty("game/A"); + frontend.markDirty("game/B"); + + result = frontend.check("game/A"); + LUAU_REQUIRE_ERRORS(result); + + TypeId tyA = requireType("game/A", "me"); + CHECK_EQ(toString(tyA), "any"); + + result = frontend.check("game/B"); + LUAU_REQUIRE_ERRORS(result); + + TypeId tyB = requireType("game/B", "me"); + CHECK_EQ(toString(tyB), "any"); +} + TEST_CASE_FIXTURE(FrontendFixture, "dont_reparse_clean_file_when_linting") { fileResolver.source["Modules/A"] = R"( diff --git a/tests/Module.test.cpp b/tests/Module.test.cpp index 82b7a350..de063121 100644 --- a/tests/Module.test.cpp +++ b/tests/Module.test.cpp @@ -1,4 +1,5 @@ // This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details +#include "Luau/Clone.h" #include "Luau/Module.h" #include "Luau/Scope.h" diff --git a/tests/Parser.test.cpp b/tests/Parser.test.cpp index 7dacc669..79f9ecab 100644 --- a/tests/Parser.test.cpp +++ b/tests/Parser.test.cpp @@ -2022,6 +2022,15 @@ TEST_CASE_FIXTURE(Fixture, "parse_type_alias_default_type_errors") matchParseError("type Y number> = {}", "Expected type pack after '=', got type", Location{{0, 14}, {0, 32}}); } +TEST_CASE_FIXTURE(Fixture, "parse_type_pack_errors") +{ + ScopedFastFlag luauParseRecoverUnexpectedPack{"LuauParseRecoverUnexpectedPack", true}; + + matchParseError("type Y = {a: T..., b: number}", "Unexpected '...' after type name; type pack is not allowed in this context", + Location{{0, 20}, {0, 23}}); + matchParseError("type Y = {a: (number | string)...", "Unexpected '...' after type annotation", Location{{0, 36}, {0, 39}}); +} + TEST_CASE_FIXTURE(Fixture, "parse_if_else_expression") { { @@ -2590,4 +2599,16 @@ type Y = (T...) -> U... CHECK_EQ(1, result.errors.size()); } +TEST_CASE_FIXTURE(Fixture, "recover_unexpected_type_pack") +{ + ScopedFastFlag luauParseRecoverUnexpectedPack{"LuauParseRecoverUnexpectedPack", true}; + + ParseResult result = tryParse(R"( +type X = { a: T..., b: number } +type Y = { a: T..., b: number } +type Z = { a: string | T..., b: number } + )"); + REQUIRE_EQ(3, result.errors.size()); +} + TEST_SUITE_END(); diff --git a/tests/TypeInfer.functions.test.cpp b/tests/TypeInfer.functions.test.cpp index dbae7b54..1713216a 100644 --- a/tests/TypeInfer.functions.test.cpp +++ b/tests/TypeInfer.functions.test.cpp @@ -1270,7 +1270,7 @@ caused by: TEST_CASE_FIXTURE(Fixture, "function_decl_quantify_right_type") { - ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify3", true}; + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; fileResolver.source["game/isAMagicMock"] = R"( --!nonstrict @@ -1294,7 +1294,7 @@ end TEST_CASE_FIXTURE(Fixture, "function_decl_non_self_sealed_overwrite") { - ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify3", true}; + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; CheckResult result = check(R"( function string.len(): number @@ -1316,7 +1316,7 @@ print(string.len('hello')) TEST_CASE_FIXTURE(Fixture, "function_decl_non_self_sealed_overwrite_2") { - ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify3", true}; + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; ScopedFastFlag inferStatFunction{"LuauInferStatFunction", true}; CheckResult result = check(R"( @@ -1324,12 +1324,12 @@ local t: { f: ((x: number) -> number)? } = {} function t.f(x) print(x + 5) - return x .. "asd" + return x .. "asd" -- 1st error: we know that return type is a number, not a string end t.f = function(x) print(x + 5) - return x .. "asd" + return x .. "asd" -- 2nd error: we know that return type is a number, not a string end )"); @@ -1338,6 +1338,33 @@ end CHECK_EQ(toString(result.errors[1]), R"(Type 'string' could not be converted into 'number')"); } +TEST_CASE_FIXTURE(Fixture, "function_decl_non_self_unsealed_overwrite") +{ + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; + ScopedFastFlag inferStatFunction{"LuauInferStatFunction", true}; + + CheckResult result = check(R"( +local t = { f = nil :: ((x: number) -> number)? } + +function t.f(x: string): string -- 1st error: new function value type is incompatible + return x .. "asd" +end + +t.f = function(x) + print(x + 5) + return x .. "asd" -- 2nd error: we know that return type is a number, not a string +end + )"); + + LUAU_REQUIRE_ERROR_COUNT(2, result); + CHECK_EQ(toString(result.errors[0]), R"(Type '(string) -> string' could not be converted into '((number) -> number)?' +caused by: + None of the union options are compatible. For example: Type '(string) -> string' could not be converted into '(number) -> number' +caused by: + Argument #1 type is not compatible. Type 'number' could not be converted into 'string')"); + CHECK_EQ(toString(result.errors[1]), R"(Type 'string' could not be converted into 'number')"); +} + TEST_CASE_FIXTURE(Fixture, "strict_mode_ok_with_missing_arguments") { ScopedFastFlag sff{"LuauAnyInIsOptionalIsOptional", true}; @@ -1352,7 +1379,7 @@ TEST_CASE_FIXTURE(Fixture, "strict_mode_ok_with_missing_arguments") TEST_CASE_FIXTURE(Fixture, "function_statement_sealed_table_assignment_through_indexer") { - ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify3", true}; + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; CheckResult result = check(R"( local t: {[string]: () -> number} = {} diff --git a/tests/TypeInfer.intersectionTypes.test.cpp b/tests/TypeInfer.intersectionTypes.test.cpp index d146f4e8..ac7a6532 100644 --- a/tests/TypeInfer.intersectionTypes.test.cpp +++ b/tests/TypeInfer.intersectionTypes.test.cpp @@ -311,6 +311,8 @@ TEST_CASE_FIXTURE(Fixture, "table_intersection_write_sealed") TEST_CASE_FIXTURE(Fixture, "table_intersection_write_sealed_indirect") { + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; + CheckResult result = check(R"( type X = { x: (number) -> number } type Y = { y: (string) -> string } @@ -326,10 +328,39 @@ TEST_CASE_FIXTURE(Fixture, "table_intersection_write_sealed_indirect") function xy:w(a:number) return a * 10 end )"); - LUAU_REQUIRE_ERROR_COUNT(3, result); - CHECK_EQ(toString(result.errors[0]), "Cannot add property 'z' to table 'X & Y'"); - CHECK_EQ(toString(result.errors[1]), "Cannot add property 'y' to table 'X & Y'"); - CHECK_EQ(toString(result.errors[2]), "Cannot add property 'w' to table 'X & Y'"); + LUAU_REQUIRE_ERROR_COUNT(4, result); + CHECK_EQ(toString(result.errors[0]), R"(Type '(string, number) -> string' could not be converted into '(string) -> string' +caused by: + Argument count mismatch. Function expects 2 arguments, but only 1 is specified)"); + CHECK_EQ(toString(result.errors[1]), "Cannot add property 'z' to table 'X & Y'"); + CHECK_EQ(toString(result.errors[2]), "Type 'number' could not be converted into 'string'"); + CHECK_EQ(toString(result.errors[3]), "Cannot add property 'w' to table 'X & Y'"); +} + +TEST_CASE_FIXTURE(Fixture, "table_write_sealed_indirect") +{ + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; + + // After normalization, previous 'table_intersection_write_sealed_indirect' is identical to this one + CheckResult result = check(R"( + type XY = { x: (number) -> number, y: (string) -> string } + + local xy : XY = { + x = function(a: number) return -a end, + y = function(a: string) return a .. "b" end + } + function xy.z(a:number) return a * 10 end + function xy:y(a:number) return a * 10 end + function xy:w(a:number) return a * 10 end + )"); + + LUAU_REQUIRE_ERROR_COUNT(4, result); + CHECK_EQ(toString(result.errors[0]), R"(Type '(string, number) -> string' could not be converted into '(string) -> string' +caused by: + Argument count mismatch. Function expects 2 arguments, but only 1 is specified)"); + CHECK_EQ(toString(result.errors[1]), "Cannot add property 'z' to table 'XY'"); + CHECK_EQ(toString(result.errors[2]), "Type 'number' could not be converted into 'string'"); + CHECK_EQ(toString(result.errors[3]), "Cannot add property 'w' to table 'XY'"); } TEST_CASE_FIXTURE(Fixture, "table_intersection_setmetatable") diff --git a/tests/TypeInfer.primitives.test.cpp b/tests/TypeInfer.primitives.test.cpp index 44b7b0d0..3ddf9813 100644 --- a/tests/TypeInfer.primitives.test.cpp +++ b/tests/TypeInfer.primitives.test.cpp @@ -95,6 +95,8 @@ end )"); LUAU_REQUIRE_ERROR_COUNT(2, result); + CHECK_EQ(toString(result.errors[0]), "Cannot add method to non-table type 'number'"); + CHECK_EQ(toString(result.errors[1]), "Type 'number' could not be converted into 'string'"); } TEST_SUITE_END(); diff --git a/tests/TypeInfer.tables.test.cpp b/tests/TypeInfer.tables.test.cpp index 0cc12d19..0484351d 100644 --- a/tests/TypeInfer.tables.test.cpp +++ b/tests/TypeInfer.tables.test.cpp @@ -2922,4 +2922,19 @@ TEST_CASE_FIXTURE(Fixture, "inferred_properties_of_a_table_should_start_with_the LUAU_REQUIRE_NO_ERRORS(result); } +TEST_CASE_FIXTURE(Fixture, "mixed_tables_with_implicit_numbered_keys") +{ + ScopedFastFlag sff{"LuauCheckImplicitNumbericKeys", true}; + + CheckResult result = check(R"( + local t: { [string]: number } = { 5, 6, 7 } + )"); + + LUAU_REQUIRE_ERROR_COUNT(3, result); + + CHECK_EQ("Type 'number' could not be converted into 'string'", toString(result.errors[0])); + CHECK_EQ("Type 'number' could not be converted into 'string'", toString(result.errors[1])); + CHECK_EQ("Type 'number' could not be converted into 'string'", toString(result.errors[2])); +} + TEST_SUITE_END(); diff --git a/tests/TypeInfer.tryUnify.test.cpp b/tests/TypeInfer.tryUnify.test.cpp index d8de2594..c21e1625 100644 --- a/tests/TypeInfer.tryUnify.test.cpp +++ b/tests/TypeInfer.tryUnify.test.cpp @@ -242,4 +242,30 @@ TEST_CASE_FIXTURE(TryUnifyFixture, "cli_50320_follow_in_any_unification") state.tryUnify(&func, typeChecker.anyType); } +TEST_CASE_FIXTURE(TryUnifyFixture, "txnlog_preserves_type_owner") +{ + ScopedFastFlag luauTxnLogPreserveOwner{"LuauTxnLogPreserveOwner", true}; + + TypeId a = arena.addType(TypeVar{FreeTypeVar{TypeLevel{}}}); + TypeId b = typeChecker.numberType; + + state.tryUnify(a, b); + state.log.commit(); + + CHECK_EQ(a->owningArena, &arena); +} + +TEST_CASE_FIXTURE(TryUnifyFixture, "txnlog_preserves_pack_owner") +{ + ScopedFastFlag luauTxnLogPreserveOwner{"LuauTxnLogPreserveOwner", true}; + + TypePackId a = arena.addTypePack(TypePackVar{FreeTypePack{TypeLevel{}}}); + TypePackId b = typeChecker.anyTypePack; + + state.tryUnify(a, b); + state.log.commit(); + + CHECK_EQ(a->owningArena, &arena); +} + TEST_SUITE_END(); diff --git a/tests/TypeInfer.unionTypes.test.cpp b/tests/TypeInfer.unionTypes.test.cpp index 68b7c4fb..ff207a18 100644 --- a/tests/TypeInfer.unionTypes.test.cpp +++ b/tests/TypeInfer.unionTypes.test.cpp @@ -513,4 +513,29 @@ TEST_CASE_FIXTURE(Fixture, "dont_allow_cyclic_unions_to_be_inferred") LUAU_REQUIRE_NO_ERRORS(result); } +TEST_CASE_FIXTURE(Fixture, "table_union_write_indirect") +{ + ScopedFastFlag statFunctionSimplify{"LuauStatFunctionSimplify4", true}; + + CheckResult result = check(R"( + type A = { x: number, y: (number) -> string } | { z: number, y: (number) -> string } + + local a:A = nil + + function a.y(x) + return tostring(x * 2) + end + + function a.y(x: string): number + return tonumber(x) or 0 + end + )"); + + LUAU_REQUIRE_ERROR_COUNT(1, result); + // NOTE: union normalization will improve this message + CHECK_EQ(toString(result.errors[0]), + R"(Type '(string) -> number' could not be converted into '((number) -> string) | ((number) -> string)'; none of the union options are compatible)"); +} + + TEST_SUITE_END(); diff --git a/tools/lldb_formatters.py b/tools/lldb_formatters.py index 40f8d6be..b3d2b4f5 100644 --- a/tools/lldb_formatters.py +++ b/tools/lldb_formatters.py @@ -37,7 +37,7 @@ def getType(target, typeName): return ty def luau_variant_summary(valobj, internal_dict, options): - type_id = valobj.GetChildMemberWithName("typeid").GetValueAsUnsigned() + type_id = valobj.GetChildMemberWithName("typeId").GetValueAsUnsigned() storage = valobj.GetChildMemberWithName("storage") params = templateParams(valobj.GetType().GetCanonicalType().GetName()) stored_type = params[type_id] @@ -89,7 +89,7 @@ class LuauVariantSyntheticChildrenProvider: return None def update(self): - self.type_index = self.valobj.GetChildMemberWithName("typeid").GetValueAsSigned() + self.type_index = self.valobj.GetChildMemberWithName("typeId").GetValueAsSigned() self.type_params = templateParams(self.valobj.GetType().GetCanonicalType().GetName()) if len(self.type_params) > self.type_index: From 510aed7d3ffcb509aaad264f6fd763c4b9c7f6b2 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Fri, 8 Apr 2022 11:26:47 -0700 Subject: [PATCH 3/4] Fix JsonEncoder for AstExprTable (#454) JsonEncoder wasn't producing valid JSON for `AstExprTable`s. This PR fixes it. The new output looks like ```json { "type": "AstStatBlock", "location": "0,0 - 6,4", "body": [ { "type": "AstStatLocal", "location": "1,8 - 5,9", "vars": [ { "name": "x", "location": "1,14 - 1,15" } ], "values": [ { "type": "AstExprTable", "location": "3,12 - 5,9", "items": [ { "kind": "record", "key": { "type": "AstExprConstantString", "location": "4,12 - 4,15", "value": "foo" }, "value": { "type": "AstExprConstantNumber", "location": "4,18 - 4,21", "value": 123 } } ] } ] } ] } ``` --- Analysis/src/JsonEncoder.cpp | 21 ++++++--------------- tests/JsonEncoder.test.cpp | 21 +++++++++++++++++++++ 2 files changed, 27 insertions(+), 15 deletions(-) diff --git a/Analysis/src/JsonEncoder.cpp b/Analysis/src/JsonEncoder.cpp index 811e7c24..829ffa02 100644 --- a/Analysis/src/JsonEncoder.cpp +++ b/Analysis/src/JsonEncoder.cpp @@ -403,35 +403,26 @@ struct AstJsonEncoder : public AstVisitor void write(const AstExprTable::Item& item) { writeRaw("{"); - bool comma = pushComma(); + bool c = pushComma(); write("kind", item.kind); switch (item.kind) { case AstExprTable::Item::List: - write(item.value); + write("value", item.value); break; default: - write(item.key); - writeRaw(","); - write(item.value); + write("key", item.key); + write("value", item.value); break; } - popComma(comma); + popComma(c); writeRaw("}"); } void write(class AstExprTable* node) { writeNode(node, "AstExprTable", [&]() { - bool comma = false; - for (const auto& prop : node->items) - { - if (comma) - writeRaw(","); - else - comma = true; - write(prop); - } + PROP(items); }); } diff --git a/tests/JsonEncoder.test.cpp b/tests/JsonEncoder.test.cpp index cb508072..6711d979 100644 --- a/tests/JsonEncoder.test.cpp +++ b/tests/JsonEncoder.test.cpp @@ -1,6 +1,7 @@ // This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details #include "Luau/Ast.h" #include "Luau/JsonEncoder.h" +#include "Luau/Parser.h" #include "doctest.h" @@ -50,4 +51,24 @@ TEST_CASE("encode_AstStatBlock") toJson(&block)); } +TEST_CASE("encode_tables") +{ + std::string src = R"( + local x: { + foo: number + } = { + foo = 123, + } + )"; + + Allocator allocator; + AstNameTable names(allocator); + ParseResult parseResult = Parser::parse(src.c_str(), src.length(), names, allocator); + + REQUIRE(parseResult.errors.size() == 0); + std::string json = toJson(parseResult.root); + + CHECK(json == R"({"type":"AstStatBlock","location":"0,0 - 6,4","body":[{"type":"AstStatLocal","location":"1,8 - 5,9","vars":[{"type":{"type":"AstTypeTable","location":"1,17 - 3,9","props":[{"name":"foo","location":"2,12 - 2,15","type":{"type":"AstTypeReference","location":"2,17 - 2,23","name":"number","parameters":[]}}],"indexer":false},"name":"x","location":"1,14 - 1,15"}],"values":[{"type":"AstExprTable","location":"3,12 - 5,9","items":[{"kind":"record","key":{"type":"AstExprConstantString","location":"4,12 - 4,15","value":"foo"},"value":{"type":"AstExprConstantNumber","location":"4,18 - 4,21","value":123}}]}]}]})"); +} + TEST_SUITE_END(); From d37d0c857ba543ea47f0b8fce5678f7aadf5239e Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Sat, 9 Apr 2022 00:07:08 -0500 Subject: [PATCH 4/4] Prototype: Renamed any/none to unknown/never (#447) * Renamed any/none to unknown/never * Pin hackage version * Update Agda version --- .github/workflows/prototyping.yml | 10 +- prototyping/Luau/StrictMode.agda | 2 +- prototyping/Luau/Subtyping.agda | 6 +- prototyping/Luau/Type.agda | 104 +++++++-------- prototyping/Luau/Type/FromJSON.agda | 6 +- prototyping/Luau/Type/ToString.agda | 6 +- prototyping/Luau/TypeCheck.agda | 14 +- prototyping/Properties/StrictMode.agda | 62 ++++----- prototyping/Properties/Subtyping.agda | 122 +++++++++--------- prototyping/Properties/TypeCheck.agda | 20 +-- .../Tests/PrettyPrinter/smoke_test/out.txt | 6 +- 11 files changed, 181 insertions(+), 177 deletions(-) diff --git a/.github/workflows/prototyping.yml b/.github/workflows/prototyping.yml index 6bc8a81b..ff66881d 100644 --- a/.github/workflows/prototyping.yml +++ b/.github/workflows/prototyping.yml @@ -10,7 +10,9 @@ jobs: linux: strategy: matrix: - agda: [2.6.2.1] + agda: [2.6.2.2] + hackageDate: ["2022-04-07"] + hackageTime: ["23:06:28"] name: prototyping runs-on: ubuntu-latest steps: @@ -18,7 +20,7 @@ jobs: - uses: actions/cache@v2 with: path: ~/.cabal/store - key: prototyping-${{ runner.os }}-${{ matrix.agda }} + key: "prototyping-${{ runner.os }}-${{ matrix.agda }}-${{ matrix.hackageDate }}-${{ matrix.hackageTime }}" - uses: actions/cache@v2 id: luau-ast-cache with: @@ -28,12 +30,12 @@ jobs: run: sudo apt-get install -y cabal-install - name: cabal update working-directory: prototyping - run: cabal update + run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z" - name: cabal install working-directory: prototyping run: | - cabal install Agda-${{ matrix.agda }} cabal install --lib scientific vector aeson --package-env . + cabal install --allow-newer Agda-${{ matrix.agda }} - name: check targets working-directory: prototyping run: | diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 0b5fe0da..b6769f01 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -5,7 +5,7 @@ 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; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Luau.Type using (Type; strict; nil; number; string; boolean; _⇒_; _∪_; _∩_; tgt) open import Luau.Subtyping using (_≮:_) open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda index 7d67eb43..943f459b 100644 --- a/prototyping/Luau/Subtyping.agda +++ b/prototyping/Luau/Subtyping.agda @@ -1,6 +1,6 @@ {-# OPTIONS --rewriting #-} -open import Luau.Type using (Type; Scalar; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_) +open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_) open import Properties.Equality using (_≢_) module Luau.Subtyping where @@ -29,7 +29,7 @@ data Language where left : ∀ {T U t} → Language T t → Language (T ∪ U) t right : ∀ {T U u} → Language U u → Language (T ∪ U) u _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t - any : ∀ {t} → Language any t + unknown : ∀ {t} → Language unknown t data ¬Language where @@ -42,7 +42,7 @@ data ¬Language where _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u - none : ∀ {t} → ¬Language none t + never : ∀ {t} → ¬Language never t -- Subtyping as language inclusion diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 87815ddb..30c45388 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -9,8 +9,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) data Type : Set where nil : Type _⇒_ : Type → Type → Type - none : Type - any : Type + never : Type + unknown : Type boolean : Type number : Type string : Type @@ -29,8 +29,8 @@ lhs (T ⇒ _) = T lhs (T ∪ _) = T lhs (T ∩ _) = T lhs nil = nil -lhs none = none -lhs any = any +lhs never = never +lhs unknown = unknown lhs number = number lhs boolean = boolean lhs string = string @@ -40,8 +40,8 @@ rhs (_ ⇒ T) = T rhs (_ ∪ T) = T rhs (_ ∩ T) = T rhs nil = nil -rhs none = none -rhs any = any +rhs never = never +rhs unknown = unknown rhs number = number rhs boolean = boolean rhs string = string @@ -49,16 +49,16 @@ rhs string = string _≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) nil ≡ᵀ nil = yes refl nil ≡ᵀ (S ⇒ T) = no (λ ()) -nil ≡ᵀ none = no (λ ()) -nil ≡ᵀ any = no (λ ()) +nil ≡ᵀ never = no (λ ()) +nil ≡ᵀ unknown = no (λ ()) 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 (λ ()) +never ≡ᵀ string = no (λ ()) +unknown ≡ᵀ string = no (λ ()) boolean ≡ᵀ string = no (λ ()) number ≡ᵀ string = no (λ ()) (S ∪ T) ≡ᵀ string = no (λ ()) @@ -68,48 +68,48 @@ number ≡ᵀ string = no (λ ()) (S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl (S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q)) (S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q)) -(S ⇒ T) ≡ᵀ none = no (λ ()) -(S ⇒ T) ≡ᵀ any = no (λ ()) +(S ⇒ T) ≡ᵀ never = no (λ ()) +(S ⇒ T) ≡ᵀ unknown = no (λ ()) (S ⇒ T) ≡ᵀ number = no (λ ()) (S ⇒ T) ≡ᵀ boolean = no (λ ()) (S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ()) (S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ()) -none ≡ᵀ nil = no (λ ()) -none ≡ᵀ (U ⇒ V) = no (λ ()) -none ≡ᵀ none = yes refl -none ≡ᵀ any = no (λ ()) -none ≡ᵀ number = no (λ ()) -none ≡ᵀ boolean = no (λ ()) -none ≡ᵀ (U ∪ V) = no (λ ()) -none ≡ᵀ (U ∩ V) = no (λ ()) -any ≡ᵀ nil = no (λ ()) -any ≡ᵀ (U ⇒ V) = no (λ ()) -any ≡ᵀ none = no (λ ()) -any ≡ᵀ any = yes refl -any ≡ᵀ number = no (λ ()) -any ≡ᵀ boolean = no (λ ()) -any ≡ᵀ (U ∪ V) = no (λ ()) -any ≡ᵀ (U ∩ V) = no (λ ()) +never ≡ᵀ nil = no (λ ()) +never ≡ᵀ (U ⇒ V) = no (λ ()) +never ≡ᵀ never = yes refl +never ≡ᵀ unknown = no (λ ()) +never ≡ᵀ number = no (λ ()) +never ≡ᵀ boolean = no (λ ()) +never ≡ᵀ (U ∪ V) = no (λ ()) +never ≡ᵀ (U ∩ V) = no (λ ()) +unknown ≡ᵀ nil = no (λ ()) +unknown ≡ᵀ (U ⇒ V) = no (λ ()) +unknown ≡ᵀ never = no (λ ()) +unknown ≡ᵀ unknown = yes refl +unknown ≡ᵀ number = no (λ ()) +unknown ≡ᵀ boolean = no (λ ()) +unknown ≡ᵀ (U ∪ V) = no (λ ()) +unknown ≡ᵀ (U ∩ V) = no (λ ()) number ≡ᵀ nil = no (λ ()) number ≡ᵀ (T ⇒ U) = no (λ ()) -number ≡ᵀ none = no (λ ()) -number ≡ᵀ any = no (λ ()) +number ≡ᵀ never = no (λ ()) +number ≡ᵀ unknown = no (λ ()) number ≡ᵀ number = yes refl number ≡ᵀ boolean = no (λ ()) number ≡ᵀ (T ∪ U) = no (λ ()) number ≡ᵀ (T ∩ U) = no (λ ()) boolean ≡ᵀ nil = no (λ ()) boolean ≡ᵀ (T ⇒ U) = no (λ ()) -boolean ≡ᵀ none = no (λ ()) -boolean ≡ᵀ any = no (λ ()) +boolean ≡ᵀ never = no (λ ()) +boolean ≡ᵀ unknown = no (λ ()) 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 ≡ᵀ never = no (λ ()) +string ≡ᵀ unknown = no (λ ()) string ≡ᵀ boolean = no (λ ()) string ≡ᵀ number = no (λ ()) string ≡ᵀ string = yes refl @@ -117,8 +117,8 @@ string ≡ᵀ (U ∪ V) = no (λ ()) string ≡ᵀ (U ∩ V) = no (λ ()) (S ∪ T) ≡ᵀ nil = no (λ ()) (S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ()) -(S ∪ T) ≡ᵀ none = no (λ ()) -(S ∪ T) ≡ᵀ any = no (λ ()) +(S ∪ T) ≡ᵀ never = no (λ ()) +(S ∪ T) ≡ᵀ unknown = no (λ ()) (S ∪ T) ≡ᵀ number = no (λ ()) (S ∪ T) ≡ᵀ boolean = no (λ ()) (S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V) @@ -128,8 +128,8 @@ string ≡ᵀ (U ∩ V) = no (λ ()) (S ∪ T) ≡ᵀ (U ∩ V) = no (λ ()) (S ∩ T) ≡ᵀ nil = no (λ ()) (S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ()) -(S ∩ T) ≡ᵀ none = no (λ ()) -(S ∩ T) ≡ᵀ any = no (λ ()) +(S ∩ T) ≡ᵀ never = no (λ ()) +(S ∩ T) ≡ᵀ unknown = no (λ ()) (S ∩ T) ≡ᵀ number = no (λ ()) (S ∩ T) ≡ᵀ boolean = no (λ ()) (S ∩ T) ≡ᵀ (U ∪ V) = no (λ ()) @@ -151,29 +151,29 @@ data Mode : Set where nonstrict : Mode src : Mode → Type → Type -src m nil = none -src m number = none -src m boolean = none -src m string = none +src m nil = never +src m number = never +src m boolean = never +src m string = never 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) src nonstrict (S ∪ T) = (src nonstrict S) ∪ (src nonstrict T) src strict (S ∩ T) = (src strict S) ∪ (src strict T) src nonstrict (S ∩ T) = (src nonstrict S) ∩ (src nonstrict T) -src strict none = any -src nonstrict none = none -src strict any = none -src nonstrict any = any +src strict never = unknown +src nonstrict never = never +src strict unknown = never +src nonstrict unknown = unknown tgt : Type → Type -tgt nil = none +tgt nil = never tgt (S ⇒ T) = T -tgt none = none -tgt any = any -tgt number = none -tgt boolean = none -tgt string = none +tgt never = never +tgt unknown = unknown +tgt number = never +tgt boolean = never +tgt string = never 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 2d6ba689..e3d1e8e7 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; string) +open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; unknown; never; number; string) open import Agda.Builtin.List using (List; _∷_; []) open import Agda.Builtin.Bool using (true; false) @@ -42,7 +42,9 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing = 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 "any") = Right unknown -- not quite right +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "unknown") = Right unknown +typeFromJSON (object o) | just (string "AstTypeReference") | just (string "never") = Right never 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" diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index 2efe6632..a41ecec2 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; string; _∪_; _∩_; normalizeOptional) +open import Luau.Type using (Type; nil; _⇒_; never; unknown; number; boolean; string; _∪_; _∩_; normalizeOptional) {-# TERMINATING #-} typeToString : Type → String @@ -10,8 +10,8 @@ typeToStringᴵ : Type → String typeToString nil = "nil" typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T) -typeToString none = "none" -typeToString any = "any" +typeToString never = "never" +typeToString unknown = "unknown" typeToString number = "number" typeToString boolean = "boolean" typeToString string = "string" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index c22618bc..aea6507a 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -10,7 +10,7 @@ open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr 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; any; number; boolean; string; _⇒_; tgt) +open import Luau.Type using (Type; Mode; nil; unknown; 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) @@ -19,9 +19,9 @@ open import Properties.Product using (_×_; _,_) src : Type → Type src = Luau.Type.src m -orAny : Maybe Type → Type -orAny nothing = any -orAny (just T) = T +orUnknown : Maybe Type → Type +orUnknown nothing = unknown +orUnknown (just T) = T srcBinOp : BinaryOperator → Type srcBinOp + = number @@ -30,8 +30,8 @@ srcBinOp * = number srcBinOp / = number srcBinOp < = number srcBinOp > = number -srcBinOp == = any -srcBinOp ~= = any +srcBinOp == = unknown +srcBinOp ~= = unknown srcBinOp <= = number srcBinOp >= = number srcBinOp ·· = string @@ -89,7 +89,7 @@ data _⊢ᴱ_∈_ where var : ∀ {x T Γ} → - T ≡ orAny(Γ [ x ]ⱽ) → + T ≡ orUnknown(Γ [ x ]ⱽ) → ---------------- Γ ⊢ᴱ (var x) ∈ T diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 2ff2b153..1165fdaa 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -9,10 +9,10 @@ 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ᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; 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.Subtyping using (_≮:_; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) +open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) 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; number; boolean; string; _⇒_; none; any; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orAny; srcBinOp; tgtBinOp) +open import Luau.Type using (Type; strict; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) @@ -22,7 +22,7 @@ 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.Functions using (_∘_) -open import Properties.Subtyping using (any-≮:; ≡-trans-≮:; ≮:-trans-≡; none-tgt-≮:; tgt-none-≮:; src-any-≮:; any-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-none; any-≮:-scalar; scalar-≮:-none; any-≮:-none) +open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ) 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; +; -; *; /; <; >; <=; >=; ··) @@ -68,12 +68,12 @@ heap-weakeningᴱ Γ H (var x) h p = p heap-weakeningᴱ Γ H (val nil) h p = p heap-weakeningᴱ Γ H (val (addr a)) refl p = p heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p with a ≡ᴬ b -heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = any-≮: p -heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ (lookup-not-allocated q r))) p +heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = unknown-≮: p +heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ (lookup-not-allocated q r))) p heap-weakeningᴱ Γ H (val (number x)) h p = p heap-weakeningᴱ Γ H (val (bool x)) h p = p heap-weakeningᴱ Γ H (val (string x)) h p = p -heap-weakeningᴱ Γ H (M $ N) h p = none-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-none-≮: p)) +heap-weakeningᴱ Γ H (M $ N) h p = never-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-never-≮: p)) heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p heap-weakeningᴱ Γ H (binexp M op N) h p = p @@ -94,11 +94,11 @@ substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p substitutivityᴱ H (val w) v x p = Left p substitutivityᴱ H (binexp M op N) v x p = Left p -substitutivityᴱ H (M $ N) v x p = mapL none-tgt-≮: (substitutivityᴱ H M v x (tgt-none-≮: p)) +substitutivityᴱ H (M $ N) v x p = mapL never-tgt-≮: (substitutivityᴱ H M v x (tgt-never-≮: p)) substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q) -substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orAny (sym (⊕-lookup-miss x y _ _ p))) q) +substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orUnknown (sym (⊕-lookup-miss x y _ _ p))) q) substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p @@ -125,9 +125,9 @@ binOpPreservation H (·· v w) = refl reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M)) reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B)) -reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR none-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-none-≮: p)) -reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (none-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-none-≮: p))) -reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orAny (cong typeOfᴹᴼ q))) p) +reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR never-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-never-≮: p)) +reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (never-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-never-≮: p))) +reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orUnknown (cong typeOfᴹᴼ q))) p) reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p)) @@ -152,8 +152,8 @@ reflect-substitutionᴱ H (var y) v x W = reflect-substitutionᴱ-whenever H v x reflect-substitutionᴱ H (val (addr a)) v x (UnallocatedAddress r) = Left (UnallocatedAddress r) reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with substitutivityᴱ H N v x p reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Right W = Right (Right W) -reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-any-≮: q) -reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ any-src-≮: q) r) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-unknown-≮: q) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ unknown-src-≮: q) r) reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Right W = Right (Right W) reflect-substitutionᴱ H (M $ N) v x (app₁ W) = mapL app₁ (reflect-substitutionᴱ H M v x W) reflect-substitutionᴱ H (M $ N) v x (app₂ W) = mapL app₂ (reflect-substitutionᴱ H N v x W) @@ -187,7 +187,7 @@ reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (t reflect-weakeningᴱ Γ H (var x) h (UnboundVariable p) = (UnboundVariable p) reflect-weakeningᴱ Γ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p) -reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (any-src-≮: p (heap-weakeningᴱ Γ H M h (src-any-≮: p)))) +reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (unknown-src-≮: p (heap-weakeningᴱ Γ H M h (src-unknown-≮: p)))) reflect-weakeningᴱ Γ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ Γ H M h W) reflect-weakeningᴱ Γ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ Γ H N h W) reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₁ p) = BinOpMismatch₁ (heap-weakeningᴱ Γ H M h p) @@ -214,19 +214,19 @@ reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (fu reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H)) reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H)) -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ any-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-any-≮: p)) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ unknown-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-unknown-≮: p)) reflectᴱ H (M $ N) (app₁ s) (app₁ W′) = mapL app₁ (reflectᴱ H M s W′) reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = Left (app₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′)) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (any-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-any-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (unknown-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-unknown-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q) reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = Left (app₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′)) reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) = mapL app₂ (reflectᴱ H N s W′) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with substitutivityᴮ H B v x q reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Left r = Right (addr a p (FunctionDefnMismatch r)) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orAny (cong typeOfᴹᴼ (sym p))))))) +reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orUnknown (cong typeOfᴹᴼ (sym p))))))) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with reflect-substitutionᴮ _ B v x W′ reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Left W = Right (addr a p (function₁ W)) reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Left W) = Left (app₂ W) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orAny (cong typeOfᴹᴼ (sym p)))))) +reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orUnknown (cong typeOfᴹᴼ (sym p)))))) reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (reflect-subtypingᴮ H B s p)) reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) = mapL block₁ (reflectᴮ H B s W′) reflectᴱ H (block var b ∈ T is B end) (return v) W′ = Left (block₁ (return W′)) @@ -283,8 +283,8 @@ reflect* H B (step s t) W = cond (reflectᴮ H B s) (reflectᴴᴮ H B s) (refle isntNumber : ∀ H v → (valueType v ≢ number) → (typeOfᴱ H ∅ (val v) ≮: number) isntNumber H nil p = scalar-≢-impl-≮: nil number (λ ()) isntNumber H (addr a) p with remember (H [ a ]ᴴ) -isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar number) -isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar number) +isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar number) +isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar number) isntNumber H (number x) p = CONTRADICTION (p refl) isntNumber H (bool x) p = scalar-≢-impl-≮: boolean number (λ ()) isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ()) @@ -292,8 +292,8 @@ isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ()) isntString : ∀ H v → (valueType v ≢ string) → (typeOfᴱ H ∅ (val v) ≮: string) isntString H nil p = scalar-≢-impl-≮: nil string (λ ()) isntString H (addr a) p with remember (H [ a ]ᴴ) -isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar string) -isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar string) +isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar string) +isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar string) isntString H (number x) p = scalar-≢-impl-≮: number string (λ ()) isntString H (bool x) p = scalar-≢-impl-≮: boolean string (λ ()) isntString H (string x) p = CONTRADICTION (p refl) @@ -305,14 +305,14 @@ isntFunction H (number x) p = scalar-≮:-function number isntFunction H (bool x) p = scalar-≮:-function boolean isntFunction H (string x) p = scalar-≮:-function string -isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: none) -isntEmpty H nil = scalar-≮:-none nil +isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: never) +isntEmpty H nil = scalar-≮:-never nil isntEmpty H (addr a) with remember (H [ a ]ᴴ) -isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) function-≮:-none -isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) any-≮:-none -isntEmpty H (number x) = scalar-≮:-none number -isntEmpty H (bool x) = scalar-≮:-none boolean -isntEmpty H (string x) = scalar-≮:-none string +isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) function-≮:-never +isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) unknown-≮:-never +isntEmpty H (number x) = scalar-≮:-never number +isntEmpty H (bool x) = scalar-≮:-never boolean +isntEmpty H (string x) = scalar-≮:-never string runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → (typeOfᴱ H ∅ (val v) ≮: srcBinOp op) runtimeBinOpWarning H v (+ p) = isntNumber H v p @@ -330,7 +330,7 @@ runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheck runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (any-src-≮: (isntEmpty H w) (isntFunction H v p)) +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (unknown-src-≮: (isntEmpty H w) (isntFunction H v p)) runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err) runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err) runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 0a20f244..cc6bb5c1 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -4,8 +4,8 @@ module Properties.Subtyping where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond) -open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_) -open import Luau.Type using (Type; Scalar; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_) +open import Luau.Type using (Type; Scalar; strict; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; tgt) open import Properties.Contradiction using (CONTRADICTION; ¬) open import Properties.Equality using (_≢_) open import Properties.Functions using (_∘_) @@ -47,8 +47,8 @@ dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s) dec-language (T₁ ⇒ T₂) function = Right function dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t) dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t)) -dec-language none t = Left none -dec-language any t = Right any +dec-language never t = Left never +dec-language unknown t = Right unknown dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t) dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t) @@ -60,7 +60,7 @@ language-comp t (left p) (q₁ , q₂) = language-comp t p q₁ language-comp t (right p) (q₁ , q₂) = language-comp t p q₂ language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function -language-comp (scalar s) none (scalar ()) +language-comp (scalar s) never (scalar ()) language-comp function (scalar-function ()) function language-comp (function-ok t) (scalar-function-ok ()) (function-ok q) language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q @@ -104,11 +104,11 @@ function-≮:-scalar s = witness function function (scalar-function s) scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T)) scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s) -any-≮:-scalar : ∀ {U} → (Scalar U) → (any ≮: U) -any-≮:-scalar s = witness (function-ok (scalar s)) any (scalar-function-ok s) +unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U) +unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s) -scalar-≮:-none : ∀ {U} → (Scalar U) → (U ≮: none) -scalar-≮:-none s = witness (scalar s) (scalar s) none +scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never) +scalar-≮:-never s = witness (scalar s) (scalar s) never scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U) scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p) @@ -117,8 +117,8 @@ scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-s tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t) tgt-function-ok {T = nil} (scalar ()) tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p -tgt-function-ok {T = none} (scalar ()) -tgt-function-ok {T = any} p = any +tgt-function-ok {T = never} (scalar ()) +tgt-function-ok {T = unknown} p = unknown tgt-function-ok {T = boolean} (scalar ()) tgt-function-ok {T = number} (scalar ()) tgt-function-ok {T = string} (scalar ()) @@ -131,7 +131,7 @@ function-ok-tgt (function-ok p) = p function-ok-tgt (left p) = left (function-ok-tgt p) function-ok-tgt (right p) = right (function-ok-tgt p) function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂) -function-ok-tgt any = any +function-ok-tgt unknown = unknown skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) @@ -142,22 +142,22 @@ skalar-scalar boolean = right (right (right (scalar boolean))) skalar-scalar string = right (left (scalar string)) skalar-scalar nil = right (right (left (scalar nil))) -tgt-none-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (none ⇒ U))) -tgt-none-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) +tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U))) +tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) -none-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (none ⇒ U))) → (tgt T ≮: U) -none-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) -none-tgt-≮: (witness function p (q₁ , scalar-function ())) -none-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ -none-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) +never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U) +never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) +never-tgt-≮: (witness function p (q₁ , scalar-function ())) +never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ +never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) -- Properties of src function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t) -function-err-src {T = nil} none = scalar-function-err nil +function-err-src {T = nil} never = scalar-function-err nil function-err-src {T = T₁ ⇒ T₂} p = function-err p -function-err-src {T = none} (scalar-scalar number () p) -function-err-src {T = none} (scalar-function-ok ()) -function-err-src {T = any} none = any +function-err-src {T = never} (scalar-scalar number () p) +function-err-src {T = never} (scalar-function-ok ()) +function-err-src {T = unknown} never = unknown function-err-src {T = boolean} p = scalar-function-err boolean function-err-src {T = number} p = scalar-function-err number function-err-src {T = string} p = scalar-function-err string @@ -168,8 +168,8 @@ function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , fun ¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t) ¬function-err-src {T = nil} (scalar ()) ¬function-err-src {T = T₁ ⇒ T₂} p = function-err p -¬function-err-src {T = none} any = none -¬function-err-src {T = any} (scalar ()) +¬function-err-src {T = never} unknown = never +¬function-err-src {T = unknown} (scalar ()) ¬function-err-src {T = boolean} (scalar ()) ¬function-err-src {T = number} (scalar ()) ¬function-err-src {T = string} (scalar ()) @@ -178,53 +178,53 @@ function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , fun ¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p) src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t) -src-¬function-err {T = nil} p = none +src-¬function-err {T = nil} p = never src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p -src-¬function-err {T = none} (scalar-function-err ()) -src-¬function-err {T = any} p = none -src-¬function-err {T = boolean} p = none -src-¬function-err {T = number} p = none -src-¬function-err {T = string} p = none +src-¬function-err {T = never} (scalar-function-err ()) +src-¬function-err {T = unknown} p = never +src-¬function-err {T = boolean} p = never +src-¬function-err {T = number} p = never +src-¬function-err {T = string} p = never src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p) src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p) src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂) src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t) -src-¬scalar number (scalar number) = none -src-¬scalar boolean (scalar boolean) = none -src-¬scalar string (scalar string) = none -src-¬scalar nil (scalar nil) = none +src-¬scalar number (scalar number) = never +src-¬scalar boolean (scalar boolean) = never +src-¬scalar string (scalar string) = never +src-¬scalar nil (scalar nil) = never src-¬scalar s (left p) = left (src-¬scalar s p) src-¬scalar s (right p) = right (src-¬scalar s p) src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂) -src-¬scalar s any = none +src-¬scalar s unknown = never -src-any-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ any)) -src-any-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) +src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown)) +src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) -any-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ any)) → (U ≮: src T) -any-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) -any-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) -any-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) -any-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) +unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T) +unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) +unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) +unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) +unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) --- Properties of any and none -any-≮: : ∀ {T U} → (T ≮: U) → (any ≮: U) -any-≮: (witness t p q) = witness t any q +-- Properties of unknown and never +unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U) +unknown-≮: (witness t p q) = witness t unknown q -none-≮: : ∀ {T U} → (T ≮: U) → (T ≮: none) -none-≮: (witness t p q) = witness t p none +never-≮: : ∀ {T U} → (T ≮: U) → (T ≮: never) +never-≮: (witness t p q) = witness t p never -any-≮:-none : (any ≮: none) -any-≮:-none = witness (scalar nil) any none +unknown-≮:-never : (unknown ≮: never) +unknown-≮:-never = witness (scalar nil) unknown never -function-≮:-none : ∀ {T U} → ((T ⇒ U) ≮: none) -function-≮:-none = witness function function none +function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never) +function-≮:-never = witness function function never -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf) -- defines a "set-theoretic" model (sec 2.5) -- Unfortunately we don't quite have this property, due to uninhabited types, --- for example (none -> T) is equivalent to (none -> U) +-- for example (never -> T) is equivalent to (never -> U) -- when types are interpreted as sets of syntactic values. _⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set @@ -258,7 +258,7 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → -- We don't quite have that this is a set-theoretic model -- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited - -- in particular it's not true when T₁ is none, or T₂ is any. + -- in particular it's not true when T₁ is never, or T₂ is unknown. ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ → -- This is the "only if" part of being a set-theoretic model @@ -285,11 +285,11 @@ not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ -- A counterexample when the argument type is empty. -set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language none) ⊗ Comp(Language number)) → Q ⊆ Comp((Language none) ⊗ Comp(Language string))) +set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string))) set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p) set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p) -set-theoretic-counterexample-two : (none ⇒ number) ≮: (none ⇒ string) +set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string) set-theoretic-counterexample-two = witness (function-ok (scalar number)) (function-ok (scalar number)) (function-ok (scalar-scalar number string (λ ()))) @@ -298,14 +298,14 @@ set-theoretic-counterexample-two = witness -- The reason why this is connected to overloaded functions is that currently we have that the type of -- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U), -- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V) --- and tgt(none => T) should be any. For example +-- and tgt(never => T) should be unknown. For example -- -- tgt((number => string) & (string => bool))(number) -- is tgt(number => string)(number) & tgt(string => bool)(number) --- is tgt(number => string)(number) & tgt(string => bool)(number&any) --- is tgt(number => string)(number) & tgt(string&number => bool)(any) --- is tgt(number => string)(number) & tgt(none => bool)(any) --- is string & any +-- is tgt(number => string)(number) & tgt(string => bool)(number&unknown) +-- is tgt(number => string)(number) & tgt(string&number => bool)(unknown) +-- is tgt(number => string)(number) & tgt(never => bool)(unknown) +-- is string & unknown -- is string -- -- there's some discussion of this in the Gentle Introduction paper. diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index ead0c097..a5916a13 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; string; app; function; block; binexp; done; return; local; nothing; orAny; tgtBinOp) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; 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.Type using (Type; nil; unknown; never; 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) @@ -42,8 +42,8 @@ typeOfⱽ H (string x) = just string typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type -typeOfᴱ H Γ (var x) = orAny(Γ [ x ]ⱽ) -typeOfᴱ H Γ (val v) = orAny(typeOfⱽ H v) +typeOfᴱ H Γ (var x) = orUnknown(Γ [ x ]ⱽ) +typeOfᴱ H Γ (val v) = orUnknown(typeOfⱽ H v) typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M) typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T typeOfᴱ H Γ (block var b ∈ T is B end) = T @@ -54,7 +54,7 @@ typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M typeOfᴮ H Γ done = nil -mustBeFunction : ∀ H Γ v → (none ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v)) +mustBeFunction : ∀ H Γ v → (never ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v)) mustBeFunction H Γ nil p = CONTRADICTION (p refl) mustBeFunction H Γ (addr a) p = refl mustBeFunction H Γ (number n) p = CONTRADICTION (p refl) @@ -64,17 +64,17 @@ mustBeFunction H Γ (string x) p = CONTRADICTION (p refl) mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number) mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ) -mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orUnknown (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 orAny (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p 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 orAny (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (just O , q) with trans (cong orUnknown (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 orAny (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p mustBeString H Γ (addr a) p | (nothing , q) | () mustBeString H Γ (string x) p = refl @@ -83,7 +83,7 @@ typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) typeCheckᴱ H Γ (var x) = var refl typeCheckᴱ H Γ (val nil) = nil -typeCheckᴱ H Γ (val (addr a)) = addr (orAny (typeOfᴹᴼ (H [ a ]ᴴ))) +typeCheckᴱ H Γ (val (addr a)) = addr (orUnknown (typeOfᴹᴼ (H [ a ]ᴴ))) typeCheckᴱ H Γ (val (number n)) = number typeCheckᴱ H Γ (val (bool b)) = bool typeCheckᴱ H Γ (val (string x)) = string diff --git a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt index 34e0c4fe..ca95cae9 100644 --- a/prototyping/Tests/PrettyPrinter/smoke_test/out.txt +++ b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt @@ -10,10 +10,10 @@ local function comp(f) end local id2 = comp(id)(id) local nil2 = id2(nil) -local a : any = nil +local a : unknown = nil local b : nil = nil local c : (nil) -> nil = nil -local d : (any & nil) = nil -local e : any? = nil +local d : (unknown & nil) = nil +local e : unknown? = nil local f : number = 123.0 return id2(nil2)