Merge branch 'main' into prototyping-strings

This commit is contained in:
Lily Brown 2022-03-02 14:13:55 -08:00
commit d700c08e9d
94 changed files with 2720 additions and 1226 deletions

View file

@ -1,25 +1,10 @@
name: prototyping
on:
push:
branches:
- 'master'
- 'prototyping-*'
paths:
- '.github/workflows/**'
- 'prototyping/**'
- 'Analysis/**'
- 'Ast/**'
- 'CLI/Ast.cpp'
- 'CLI/FileUtils.*'
pull_request:
paths:
- '.github/workflows/**'
- '.github/workflows/prototyping.yml'
- 'prototyping/**'
- 'Analysis/**'
- 'Ast/**'
- 'CLI/Ast.cpp'
- 'CLI/FileUtils.*'
jobs:
linux:

View file

@ -13,8 +13,6 @@
#include <unordered_map>
#include <optional>
LUAU_FASTFLAG(LuauPrepopulateUnionOptionsBeforeAllocation)
namespace Luau
{
@ -60,11 +58,8 @@ struct TypeArena
template<typename T>
TypeId addType(T tv)
{
if (FFlag::LuauPrepopulateUnionOptionsBeforeAllocation)
{
if constexpr (std::is_same_v<T, UnionTypeVar>)
LUAU_ASSERT(tv.options.size() >= 2);
}
if constexpr (std::is_same_v<T, UnionTypeVar>)
LUAU_ASSERT(tv.options.size() >= 2);
return addTV(TypeVar(std::move(tv)));
}

View file

@ -31,6 +31,7 @@ bool doesCallError(const AstExprCall* call);
bool hasBreak(AstStat* node);
const AstStat* getFallthrough(const AstStat* node);
struct UnifierOptions;
struct Unifier;
// A substitution which replaces generic types in a given set by free types.
@ -245,6 +246,7 @@ struct TypeChecker
* Treat any failures as type errors in the final typecheck report.
*/
bool unify(TypeId subTy, TypeId superTy, const Location& location);
bool unify(TypeId subTy, TypeId superTy, const Location& location, const UnifierOptions& options);
bool unify(TypePackId subTy, TypePackId superTy, const Location& location, CountMismatch::Context ctx = CountMismatch::Context::Arg);
/** Attempt to unify the types.

View file

@ -13,7 +13,7 @@ namespace Luau
using ScopePtr = std::shared_ptr<struct Scope>;
std::optional<TypeId> findMetatableEntry(ErrorVec& errors, const ScopePtr& globalScope, TypeId type, std::string entry, Location location);
std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, const ScopePtr& globalScope, TypeId ty, Name name, Location location);
std::optional<TypeId> findMetatableEntry(ErrorVec& errors, TypeId type, std::string entry, Location location);
std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, TypeId ty, Name name, Location location);
} // namespace Luau

View file

@ -19,11 +19,31 @@ enum Variance
Invariant
};
// A substitution which replaces singleton types by their wider types
struct Widen : Substitution
{
Widen(TypeArena* arena)
: Substitution(TxnLog::empty(), arena)
{
}
bool isDirty(TypeId ty) override;
bool isDirty(TypePackId ty) override;
TypeId clean(TypeId ty) override;
TypePackId clean(TypePackId ty) override;
bool ignoreChildren(TypeId ty) override;
};
// TODO: Use this more widely.
struct UnifierOptions
{
bool isFunctionCall = false;
};
struct Unifier
{
TypeArena* const types;
Mode mode;
ScopePtr globalScope; // sigh. Needed solely to get at string's metatable.
DEPRECATED_TxnLog DEPRECATED_log;
TxnLog log;
@ -34,9 +54,9 @@ struct Unifier
UnifierSharedState& sharedState;
Unifier(TypeArena* types, Mode mode, ScopePtr globalScope, const Location& location, Variance variance, UnifierSharedState& sharedState,
Unifier(TypeArena* types, Mode mode, const Location& location, Variance variance, UnifierSharedState& sharedState,
TxnLog* parentLog = nullptr);
Unifier(TypeArena* types, Mode mode, ScopePtr globalScope, std::vector<std::pair<TypeId, TypeId>>* sharedSeen, const Location& location,
Unifier(TypeArena* types, Mode mode, std::vector<std::pair<TypeId, TypeId>>* sharedSeen, const Location& location,
Variance variance, UnifierSharedState& sharedState, TxnLog* parentLog = nullptr);
// Test whether the two type vars unify. Never commits the result.
@ -65,7 +85,10 @@ private:
void tryUnifyWithMetatable(TypeId subTy, TypeId superTy, bool reversed);
void tryUnifyWithClass(TypeId subTy, TypeId superTy, bool reversed);
void tryUnifyIndexer(const TableIndexer& subIndexer, const TableIndexer& superIndexer);
TypeId widen(TypeId ty);
TypeId deeplyOptional(TypeId ty, std::unordered_map<TypeId, TypeId> seen = {});
void cacheResult(TypeId subTy, TypeId superTy);
public:

View file

@ -236,10 +236,10 @@ static TypeCorrectKind checkTypeCorrectKind(const Module& module, TypeArena* typ
{
ty = follow(ty);
auto canUnify = [&typeArena, &module](TypeId subTy, TypeId superTy) {
auto canUnify = [&typeArena](TypeId subTy, TypeId superTy) {
InternalErrorReporter iceReporter;
UnifierSharedState unifierState(&iceReporter);
Unifier unifier(typeArena, Mode::Strict, module.getModuleScope(), Location(), Variance::Covariant, unifierState);
Unifier unifier(typeArena, Mode::Strict, Location(), Variance::Covariant, unifierState);
if (FFlag::LuauAutocompleteAvoidMutation && !FFlag::LuauUseCommittingTxnLog)
{

View file

@ -201,6 +201,7 @@ static bool similar(AstExpr* lhs, AstExpr* rhs)
return true;
}
CASE(AstExprIfElse) return similar(le->condition, re->condition) && similar(le->trueExpr, re->trueExpr) && similar(le->falseExpr, re->falseExpr);
else
{
LUAU_ASSERT(!"Unknown expression type");

View file

@ -16,7 +16,6 @@ LUAU_FASTFLAGVARIABLE(DebugLuauTrackOwningArena, false) // Remove with FFlagLuau
LUAU_FASTINTVARIABLE(LuauTypeCloneRecursionLimit, 300)
LUAU_FASTFLAG(LuauTypeAliasDefaults)
LUAU_FASTFLAG(LuauImmutableTypes)
LUAU_FASTFLAGVARIABLE(LuauPrepopulateUnionOptionsBeforeAllocation, false)
namespace Luau
{
@ -379,28 +378,14 @@ void TypeCloner::operator()(const AnyTypeVar& t)
void TypeCloner::operator()(const UnionTypeVar& t)
{
if (FFlag::LuauPrepopulateUnionOptionsBeforeAllocation)
{
std::vector<TypeId> options;
options.reserve(t.options.size());
std::vector<TypeId> options;
options.reserve(t.options.size());
for (TypeId ty : t.options)
options.push_back(clone(ty, dest, seenTypes, seenTypePacks, cloneState));
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;
}
else
{
TypeId result = dest.addType(UnionTypeVar{});
seenTypes[typeId] = result;
UnionTypeVar* option = getMutable<UnionTypeVar>(result);
LUAU_ASSERT(option != nullptr);
for (TypeId ty : t.options)
option->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)

View file

@ -1153,6 +1153,14 @@ struct Printer
writer.symbol(")");
}
}
else if (const auto& a = typeAnnotation.as<AstTypeSingletonBool>())
{
writer.keyword(a->value ? "true" : "false");
}
else if (const auto& a = typeAnnotation.as<AstTypeSingletonString>())
{
writer.string(std::string_view(a->value.data, a->value.size));
}
else if (typeAnnotation.is<AstTypeError>())
{
writer.symbol("%error-type%");

View file

@ -29,7 +29,6 @@ LUAU_FASTFLAGVARIABLE(DebugLuauFreezeDuringUnification, false)
LUAU_FASTFLAGVARIABLE(LuauRecursiveTypeParameterRestriction, false)
LUAU_FASTFLAGVARIABLE(LuauGenericFunctionsDontCacheTypeParams, false)
LUAU_FASTFLAGVARIABLE(LuauImmutableTypes, false)
LUAU_FASTFLAGVARIABLE(LuauNoSealedTypeMod, false)
LUAU_FASTFLAGVARIABLE(LuauQuantifyInPlace2, false)
LUAU_FASTFLAGVARIABLE(LuauSealExports, false)
LUAU_FASTFLAGVARIABLE(LuauSingletonTypes, false)
@ -38,14 +37,14 @@ LUAU_FASTFLAGVARIABLE(LuauTypeAliasDefaults, false)
LUAU_FASTFLAGVARIABLE(LuauExpectedTypesOfProperties, false)
LUAU_FASTFLAGVARIABLE(LuauErrorRecoveryType, false)
LUAU_FASTFLAGVARIABLE(LuauPropertiesGetExpectedType, false)
LUAU_FASTFLAGVARIABLE(LuauProperTypeLevels, false)
LUAU_FASTFLAGVARIABLE(LuauAscribeCorrectLevelToInferredProperitesOfFreeTables, false)
LUAU_FASTFLAG(LuauUnionTagMatchFix)
LUAU_FASTFLAGVARIABLE(LuauUnsealedTableLiteral, false)
LUAU_FASTFLAGVARIABLE(LuauTwoPassAliasDefinitionFix, false)
LUAU_FASTFLAGVARIABLE(LuauAssertStripsFalsyTypes, false)
LUAU_FASTFLAGVARIABLE(LuauReturnAnyInsteadOfICE, false) // Eventually removed as false.
LUAU_FASTFLAGVARIABLE(LuauAnotherTypeLevelFix, false)
LUAU_FASTFLAG(LuauWidenIfSupertypeIsFree)
LUAU_FASTFLAGVARIABLE(LuauDoNotTryToReduce, false)
namespace Luau
{
@ -1125,7 +1124,7 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco
ty = follow(ty);
if (tableSelf && (FFlag::LuauNoSealedTypeMod ? tableSelf->state != TableState::Sealed : !selfTy->persistent))
if (tableSelf && tableSelf->state != TableState::Sealed)
tableSelf->props[indexName->index.value] = {ty, /* deprecated */ false, {}, indexName->indexLocation};
const FunctionTypeVar* funTy = get<FunctionTypeVar>(ty);
@ -1138,7 +1137,7 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco
checkFunctionBody(funScope, ty, *function.func);
if (tableSelf && (FFlag::LuauNoSealedTypeMod ? tableSelf->state != TableState::Sealed : !selfTy->persistent))
if (tableSelf && tableSelf->state != TableState::Sealed)
tableSelf->props[indexName->index.value] = {
follow(quantify(funScope, ty, indexName->indexLocation)), /* deprecated */ false, {}, indexName->indexLocation};
}
@ -1210,8 +1209,7 @@ void TypeChecker::check(const ScopePtr& scope, const AstStatTypeAlias& typealias
{
ScopePtr aliasScope = childScope(scope, typealias.location);
aliasScope->level = scope->level.incr();
if (FFlag::LuauProperTypeLevels)
aliasScope->level.subLevel = subLevel;
aliasScope->level.subLevel = subLevel;
auto [generics, genericPacks] =
createGenericTypes(aliasScope, scope->level, typealias, typealias.generics, typealias.genericPacks, /* useCache = */ true);
@ -1624,7 +1622,7 @@ ExprResult<TypeId> TypeChecker::checkExpr(const ScopePtr& scope, const AstExprIn
std::optional<TypeId> TypeChecker::findTablePropertyRespectingMeta(TypeId lhsType, Name name, const Location& location)
{
ErrorVec errors;
auto result = Luau::findTablePropertyRespectingMeta(errors, globalScope, lhsType, name, location);
auto result = Luau::findTablePropertyRespectingMeta(errors, lhsType, name, location);
reportErrors(errors);
return result;
}
@ -1632,7 +1630,7 @@ std::optional<TypeId> TypeChecker::findTablePropertyRespectingMeta(TypeId lhsTyp
std::optional<TypeId> TypeChecker::findMetatableEntry(TypeId type, std::string entry, const Location& location)
{
ErrorVec errors;
auto result = Luau::findMetatableEntry(errors, globalScope, type, entry, location);
auto result = Luau::findMetatableEntry(errors, type, entry, location);
reportErrors(errors);
return result;
}
@ -1751,13 +1749,23 @@ std::optional<TypeId> TypeChecker::getIndexTypeFromType(
return std::nullopt;
}
// TODO(amccord): Write some logic to correctly handle intersections. CLI-34659
std::vector<TypeId> result = reduceUnion(parts);
if (FFlag::LuauDoNotTryToReduce)
{
if (parts.size() == 1)
return parts[0];
if (result.size() == 1)
return result[0];
return addType(IntersectionTypeVar{std::move(parts)}); // Not at all correct.
}
else
{
// TODO(amccord): Write some logic to correctly handle intersections. CLI-34659
std::vector<TypeId> result = reduceUnion(parts);
return addType(IntersectionTypeVar{result});
if (result.size() == 1)
return result[0];
return addType(IntersectionTypeVar{result});
}
}
if (addErrors)
@ -2823,10 +2831,7 @@ TypeId TypeChecker::checkLValueBinding(const ScopePtr& scope, const AstExprIndex
TypeId TypeChecker::checkFunctionName(const ScopePtr& scope, AstExpr& funName, TypeLevel level)
{
auto freshTy = [&]() {
if (FFlag::LuauProperTypeLevels)
return freshType(level);
else
return freshType(scope);
return freshType(level);
};
if (auto globalName = funName.as<AstExprGlobal>())
@ -3790,7 +3795,14 @@ std::optional<ExprResult<TypePackId>> TypeChecker::checkCallOverload(const Scope
// has been instantiated, so is a monotype. We can therefore
// unify it with a monomorphic function.
TypeId r = addType(FunctionTypeVar(scope->level, argPack, retPack));
unify(fn, r, expr.location);
if (FFlag::LuauWidenIfSupertypeIsFree)
{
UnifierOptions options;
options.isFunctionCall = true;
unify(r, fn, expr.location, options);
}
else
unify(fn, r, expr.location);
return {{retPack}};
}
@ -4243,9 +4255,15 @@ TypeId TypeChecker::anyIfNonstrict(TypeId ty) const
}
bool TypeChecker::unify(TypeId subTy, TypeId superTy, const Location& location)
{
UnifierOptions options;
return unify(subTy, superTy, location, options);
}
bool TypeChecker::unify(TypeId subTy, TypeId superTy, const Location& location, const UnifierOptions& options)
{
Unifier state = mkUnifier(location);
state.tryUnify(subTy, superTy);
state.tryUnify(subTy, superTy, options.isFunctionCall);
if (FFlag::LuauUseCommittingTxnLog)
state.log.commit();
@ -4654,7 +4672,7 @@ void TypeChecker::diagnoseMissingTableKey(UnknownProperty* utk, TypeErrorData& d
}
};
if (auto ttv = getTableType(FFlag::LuauUnionTagMatchFix ? utk->table : follow(utk->table)))
if (auto ttv = getTableType(utk->table))
accumulate(ttv->props);
else if (auto ctv = get<ClassTypeVar>(follow(utk->table)))
{
@ -4691,8 +4709,7 @@ ScopePtr TypeChecker::childFunctionScope(const ScopePtr& parent, const Location&
ScopePtr TypeChecker::childScope(const ScopePtr& parent, const Location& location)
{
ScopePtr scope = std::make_shared<Scope>(parent);
if (FFlag::LuauProperTypeLevels)
scope->level = parent->level;
scope->level = parent->level;
scope->varargPack = parent->varargPack;
currentModule->scopes.push_back(std::make_pair(location, scope));
@ -4724,7 +4741,7 @@ void TypeChecker::merge(RefinementMap& l, const RefinementMap& r)
Unifier TypeChecker::mkUnifier(const Location& location)
{
return Unifier{&currentModule->internalTypes, currentModule->mode, globalScope, location, Variance::Covariant, unifierState};
return Unifier{&currentModule->internalTypes, currentModule->mode, location, Variance::Covariant, unifierState};
}
TypeId TypeChecker::freshType(const ScopePtr& scope)
@ -5444,7 +5461,7 @@ GenericTypeDefinitions TypeChecker::createGenericTypes(const ScopePtr& scope, st
void TypeChecker::refineLValue(const LValue& lvalue, RefinementMap& refis, const ScopePtr& scope, TypeIdPredicate predicate)
{
LUAU_ASSERT(FFlag::LuauDiscriminableUnions2);
LUAU_ASSERT(FFlag::LuauDiscriminableUnions2 || FFlag::LuauAssertStripsFalsyTypes);
const LValue* target = &lvalue;
std::optional<LValue> key; // If set, we know we took the base of the lvalue path and should be walking down each option of the base's type.

View file

@ -10,7 +10,7 @@ LUAU_FASTFLAGVARIABLE(LuauTerminateCyclicMetatableIndexLookup, false)
namespace Luau
{
std::optional<TypeId> findMetatableEntry(ErrorVec& errors, const ScopePtr& globalScope, TypeId type, std::string entry, Location location)
std::optional<TypeId> findMetatableEntry(ErrorVec& errors, TypeId type, std::string entry, Location location)
{
type = follow(type);
@ -37,7 +37,7 @@ std::optional<TypeId> findMetatableEntry(ErrorVec& errors, const ScopePtr& globa
return std::nullopt;
}
std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, const ScopePtr& globalScope, TypeId ty, Name name, Location location)
std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, TypeId ty, Name name, Location location)
{
if (get<AnyTypeVar>(ty))
return ty;
@ -49,7 +49,7 @@ std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, const Sc
return it->second.type;
}
std::optional<TypeId> mtIndex = findMetatableEntry(errors, globalScope, ty, "__index", location);
std::optional<TypeId> mtIndex = findMetatableEntry(errors, ty, "__index", location);
int count = 0;
while (mtIndex)
{
@ -82,7 +82,7 @@ std::optional<TypeId> findTablePropertyRespectingMeta(ErrorVec& errors, const Sc
else
errors.push_back(TypeError{location, GenericError{"__index should either be a function or table. Got " + toString(index)}});
mtIndex = findMetatableEntry(errors, globalScope, *mtIndex, "__index", location);
mtIndex = findMetatableEntry(errors, *mtIndex, "__index", location);
}
return std::nullopt;

View file

@ -23,9 +23,7 @@ LUAU_FASTFLAG(DebugLuauFreezeArena)
LUAU_FASTINTVARIABLE(LuauTypeMaximumStringifierLength, 500)
LUAU_FASTINTVARIABLE(LuauTableTypeMaximumStringifierLength, 0)
LUAU_FASTINT(LuauTypeInferRecursionLimit)
LUAU_FASTFLAGVARIABLE(LuauRefactorTypeVarQuestions, false)
LUAU_FASTFLAG(LuauErrorRecoveryType)
LUAU_FASTFLAG(LuauUnionTagMatchFix)
LUAU_FASTFLAG(LuauDiscriminableUnions2)
namespace Luau
@ -145,20 +143,13 @@ bool isNil(TypeId ty)
bool isBoolean(TypeId ty)
{
if (FFlag::LuauRefactorTypeVarQuestions)
{
if (isPrim(ty, PrimitiveTypeVar::Boolean) || get<BooleanSingleton>(get<SingletonTypeVar>(follow(ty))))
return true;
if (isPrim(ty, PrimitiveTypeVar::Boolean) || get<BooleanSingleton>(get<SingletonTypeVar>(follow(ty))))
return true;
if (auto utv = get<UnionTypeVar>(follow(ty)))
return std::all_of(begin(utv), end(utv), isBoolean);
if (auto utv = get<UnionTypeVar>(follow(ty)))
return std::all_of(begin(utv), end(utv), isBoolean);
return false;
}
else
{
return isPrim(ty, PrimitiveTypeVar::Boolean);
}
return false;
}
bool isNumber(TypeId ty)
@ -168,20 +159,13 @@ bool isNumber(TypeId ty)
bool isString(TypeId ty)
{
if (FFlag::LuauRefactorTypeVarQuestions)
{
if (isPrim(ty, PrimitiveTypeVar::String) || get<StringSingleton>(get<SingletonTypeVar>(follow(ty))))
return true;
if (isPrim(ty, PrimitiveTypeVar::String) || get<StringSingleton>(get<SingletonTypeVar>(follow(ty))))
return true;
if (auto utv = get<UnionTypeVar>(follow(ty)))
return std::all_of(begin(utv), end(utv), isString);
if (auto utv = get<UnionTypeVar>(follow(ty)))
return std::all_of(begin(utv), end(utv), isString);
return false;
}
else
{
return isPrim(ty, PrimitiveTypeVar::String);
}
return false;
}
bool isThread(TypeId ty)
@ -194,45 +178,11 @@ bool isOptional(TypeId ty)
if (isNil(ty))
return true;
if (FFlag::LuauRefactorTypeVarQuestions)
{
auto utv = get<UnionTypeVar>(follow(ty));
if (!utv)
return false;
return std::any_of(begin(utv), end(utv), isNil);
}
else
{
std::unordered_set<TypeId> seen;
std::deque<TypeId> queue{ty};
while (!queue.empty())
{
TypeId current = follow(queue.front());
queue.pop_front();
if (seen.count(current))
continue;
seen.insert(current);
if (isNil(current))
return true;
if (auto u = get<UnionTypeVar>(current))
{
for (TypeId option : u->options)
{
if (isNil(option))
return true;
queue.push_back(option);
}
}
}
auto utv = get<UnionTypeVar>(follow(ty));
if (!utv)
return false;
}
return std::any_of(begin(utv), end(utv), isNil);
}
bool isTableIntersection(TypeId ty)
@ -263,38 +213,24 @@ std::optional<TypeId> getMetatable(TypeId type)
return mtType->metatable;
else if (const ClassTypeVar* classType = get<ClassTypeVar>(type))
return classType->metatable;
else if (FFlag::LuauRefactorTypeVarQuestions)
else if (isString(type))
{
if (isString(type))
{
auto ptv = get<PrimitiveTypeVar>(getSingletonTypes().stringType);
LUAU_ASSERT(ptv && ptv->metatable);
return ptv->metatable;
}
else
return std::nullopt;
}
else
{
if (const PrimitiveTypeVar* primitiveType = get<PrimitiveTypeVar>(type); primitiveType && primitiveType->metatable)
{
LUAU_ASSERT(primitiveType->type == PrimitiveTypeVar::String);
return primitiveType->metatable;
}
else
return std::nullopt;
auto ptv = get<PrimitiveTypeVar>(getSingletonTypes().stringType);
LUAU_ASSERT(ptv && ptv->metatable);
return ptv->metatable;
}
return std::nullopt;
}
const TableTypeVar* getTableType(TypeId type)
{
if (FFlag::LuauUnionTagMatchFix)
type = follow(type);
type = follow(type);
if (const TableTypeVar* ttv = get<TableTypeVar>(type))
return ttv;
else if (const MetatableTypeVar* mtv = get<MetatableTypeVar>(type))
return get<TableTypeVar>(FFlag::LuauUnionTagMatchFix ? follow(mtv->table) : mtv->table);
return get<TableTypeVar>(follow(mtv->table));
else
return nullptr;
}
@ -311,7 +247,7 @@ const std::string* getName(TypeId type)
{
if (mtv->syntheticName)
return &*mtv->syntheticName;
type = FFlag::LuauUnionTagMatchFix ? follow(mtv->table) : mtv->table;
type = follow(mtv->table);
}
if (auto ttv = get<TableTypeVar>(type))

View file

@ -21,9 +21,8 @@ LUAU_FASTFLAGVARIABLE(LuauTableSubtypingVariance2, false);
LUAU_FASTFLAGVARIABLE(LuauTableUnificationEarlyTest, false)
LUAU_FASTFLAG(LuauSingletonTypes)
LUAU_FASTFLAG(LuauErrorRecoveryType);
LUAU_FASTFLAG(LuauProperTypeLevels);
LUAU_FASTFLAGVARIABLE(LuauUnionTagMatchFix, false)
LUAU_FASTFLAGVARIABLE(LuauFollowWithCommittingTxnLogInAnyUnification, false)
LUAU_FASTFLAGVARIABLE(LuauWidenIfSupertypeIsFree, false)
namespace Luau
{
@ -122,7 +121,7 @@ struct PromoteTypeLevels
}
};
void promoteTypeLevels(DEPRECATED_TxnLog& DEPRECATED_log, TxnLog& log, const TypeArena* typeArena, TypeLevel minLevel, TypeId ty)
static void promoteTypeLevels(DEPRECATED_TxnLog& DEPRECATED_log, TxnLog& log, const TypeArena* typeArena, TypeLevel minLevel, TypeId ty)
{
// Type levels of types from other modules are already global, so we don't need to promote anything inside
if (FFlag::LuauImmutableTypes && ty->owningArena != typeArena)
@ -133,6 +132,7 @@ void promoteTypeLevels(DEPRECATED_TxnLog& DEPRECATED_log, TxnLog& log, const Typ
visitTypeVarOnce(ty, ptl, seen);
}
// TODO: use this and make it static.
void promoteTypeLevels(DEPRECATED_TxnLog& DEPRECATED_log, TxnLog& log, const TypeArena* typeArena, TypeLevel minLevel, TypePackId tp)
{
// Type levels of types from other modules are already global, so we don't need to promote anything inside
@ -247,6 +247,48 @@ struct SkipCacheForType
bool result = false;
};
bool Widen::isDirty(TypeId ty)
{
return FFlag::LuauUseCommittingTxnLog ? log->is<SingletonTypeVar>(ty) : bool(get<SingletonTypeVar>(ty));
}
bool Widen::isDirty(TypePackId)
{
return false;
}
TypeId Widen::clean(TypeId ty)
{
LUAU_ASSERT(isDirty(ty));
auto stv = FFlag::LuauUseCommittingTxnLog ? log->getMutable<SingletonTypeVar>(ty) : getMutable<SingletonTypeVar>(ty);
LUAU_ASSERT(stv);
if (get<StringSingleton>(stv))
return getSingletonTypes().stringType;
else
{
// If this assert trips, it's likely we now have number singletons.
LUAU_ASSERT(get<BooleanSingleton>(stv));
return getSingletonTypes().booleanType;
}
}
TypePackId Widen::clean(TypePackId)
{
throw std::runtime_error("Widen attempted to clean a dirty type pack?");
}
bool Widen::ignoreChildren(TypeId ty)
{
// Sometimes we unify ("hi") -> free1 with (free2) -> free3, so don't ignore functions.
// TODO: should we be doing this? we would need to rework how checkCallOverload does the unification.
if (FFlag::LuauUseCommittingTxnLog ? log->is<FunctionTypeVar>(ty) : bool(get<FunctionTypeVar>(ty)))
return false;
// We only care about unions.
return !(FFlag::LuauUseCommittingTxnLog ? log->is<UnionTypeVar>(ty) : bool(get<UnionTypeVar>(ty)));
}
static std::optional<TypeError> hasUnificationTooComplex(const ErrorVec& errors)
{
auto isUnificationTooComplex = [](const TypeError& te) {
@ -263,43 +305,22 @@ static std::optional<TypeError> hasUnificationTooComplex(const ErrorVec& errors)
// Used for tagged union matching heuristic, returns first singleton type field
static std::optional<std::pair<Luau::Name, const SingletonTypeVar*>> getTableMatchTag(TypeId type)
{
if (FFlag::LuauUnionTagMatchFix)
if (auto ttv = getTableType(type))
{
if (auto ttv = getTableType(type))
for (auto&& [name, prop] : ttv->props)
{
for (auto&& [name, prop] : ttv->props)
{
if (auto sing = get<SingletonTypeVar>(follow(prop.type)))
return {{name, sing}};
}
}
}
else
{
type = follow(type);
if (auto ttv = get<TableTypeVar>(type))
{
for (auto&& [name, prop] : ttv->props)
{
if (auto sing = get<SingletonTypeVar>(follow(prop.type)))
return {{name, sing}};
}
}
else if (auto mttv = get<MetatableTypeVar>(type))
{
return getTableMatchTag(mttv->table);
if (auto sing = get<SingletonTypeVar>(follow(prop.type)))
return {{name, sing}};
}
}
return std::nullopt;
}
Unifier::Unifier(TypeArena* types, Mode mode, ScopePtr globalScope, const Location& location, Variance variance, UnifierSharedState& sharedState,
Unifier::Unifier(TypeArena* types, Mode mode, const Location& location, Variance variance, UnifierSharedState& sharedState,
TxnLog* parentLog)
: types(types)
, mode(mode)
, globalScope(std::move(globalScope))
, log(parentLog)
, location(location)
, variance(variance)
@ -308,11 +329,10 @@ Unifier::Unifier(TypeArena* types, Mode mode, ScopePtr globalScope, const Locati
LUAU_ASSERT(sharedState.iceHandler);
}
Unifier::Unifier(TypeArena* types, Mode mode, ScopePtr globalScope, std::vector<std::pair<TypeId, TypeId>>* sharedSeen, const Location& location,
Unifier::Unifier(TypeArena* types, Mode mode, std::vector<std::pair<TypeId, TypeId>>* sharedSeen, const Location& location,
Variance variance, UnifierSharedState& sharedState, TxnLog* parentLog)
: types(types)
, mode(mode)
, globalScope(std::move(globalScope))
, DEPRECATED_log(sharedSeen)
, log(parentLog, sharedSeen)
, location(location)
@ -435,6 +455,8 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
}
else if (superFree)
{
TypeLevel superLevel = superFree->level;
occursCheck(superTy, subTy);
bool occursFailed = false;
if (FFlag::LuauUseCommittingTxnLog)
@ -442,8 +464,6 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
else
occursFailed = bool(get<ErrorTypeVar>(superTy));
TypeLevel superLevel = superFree->level;
// Unification can't change the level of a generic.
auto subGeneric = FFlag::LuauUseCommittingTxnLog ? log.getMutable<GenericTypeVar>(subTy) : get<GenericTypeVar>(subTy);
if (subGeneric && !subGeneric->level.subsumes(superLevel))
@ -459,20 +479,14 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
if (FFlag::LuauUseCommittingTxnLog)
{
promoteTypeLevels(DEPRECATED_log, log, types, superLevel, subTy);
log.replace(superTy, BoundTypeVar(subTy));
log.replace(superTy, BoundTypeVar(widen(subTy)));
}
else
{
if (FFlag::LuauProperTypeLevels)
promoteTypeLevels(DEPRECATED_log, log, types, superLevel, subTy);
else if (auto subLevel = getMutableLevel(subTy))
{
if (!subLevel->subsumes(superFree->level))
*subLevel = superFree->level;
}
promoteTypeLevels(DEPRECATED_log, log, types, superLevel, subTy);
DEPRECATED_log(superTy);
*asMutable(superTy) = BoundTypeVar(subTy);
*asMutable(superTy) = BoundTypeVar(widen(subTy));
}
}
@ -507,16 +521,7 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
}
else
{
if (FFlag::LuauProperTypeLevels)
promoteTypeLevels(DEPRECATED_log, log, types, subLevel, superTy);
else if (auto superLevel = getMutableLevel(superTy))
{
if (!superLevel->subsumes(subFree->level))
{
DEPRECATED_log(superTy);
*superLevel = subFree->level;
}
}
promoteTypeLevels(DEPRECATED_log, log, types, subLevel, superTy);
DEPRECATED_log(subTy);
*asMutable(subTy) = BoundTypeVar(superTy);
@ -2064,6 +2069,17 @@ void Unifier::tryUnifyTables(TypeId subTy, TypeId superTy, bool isIntersection)
}
}
TypeId Unifier::widen(TypeId ty)
{
if (!FFlag::LuauWidenIfSupertypeIsFree)
return ty;
Widen widen{types};
std::optional<TypeId> result = widen.substitute(ty);
// TODO: what does it mean for substitution to fail to widen?
return result.value_or(ty);
}
TypeId Unifier::deeplyOptional(TypeId ty, std::unordered_map<TypeId, TypeId> seen)
{
ty = follow(ty);
@ -2915,7 +2931,7 @@ void Unifier::tryUnifyWithAny(TypePackId subTy, TypePackId anyTp)
std::optional<TypeId> Unifier::findTablePropertyRespectingMeta(TypeId lhsType, Name name)
{
return Luau::findTablePropertyRespectingMeta(errors, globalScope, lhsType, name, location);
return Luau::findTablePropertyRespectingMeta(errors, lhsType, name, location);
}
void Unifier::occursCheck(TypeId needle, TypeId haystack)
@ -3096,9 +3112,9 @@ void Unifier::occursCheck(DenseHashSet<TypePackId>& seen, TypePackId needle, Typ
Unifier Unifier::makeChildUnifier()
{
if (FFlag::LuauUseCommittingTxnLog)
return Unifier{types, mode, globalScope, log.sharedSeen, location, variance, sharedState, &log};
return Unifier{types, mode, log.sharedSeen, location, variance, sharedState, &log};
else
return Unifier{types, mode, globalScope, DEPRECATED_log.sharedSeen, location, variance, sharedState, &log};
return Unifier{types, mode, DEPRECATED_log.sharedSeen, location, variance, sharedState, &log};
}
bool Unifier::isNonstrictMode() const

View file

@ -12,7 +12,6 @@ LUAU_FASTINTVARIABLE(LuauRecursionLimit, 1000)
LUAU_FASTINTVARIABLE(LuauParseErrorLimit, 100)
LUAU_FASTFLAGVARIABLE(LuauParseSingletonTypes, false)
LUAU_FASTFLAGVARIABLE(LuauParseTypeAliasDefaults, false)
LUAU_FASTFLAGVARIABLE(LuauParseRecoverTypePackEllipsis, false)
LUAU_FASTFLAGVARIABLE(LuauParseAllHotComments, false)
LUAU_FASTFLAGVARIABLE(LuauTableFieldFunctionDebugname, false)
@ -2372,11 +2371,11 @@ std::pair<AstArray<AstGenericType>, AstArray<AstGenericTypePack>> Parser::parseG
{
Location nameLocation = lexer.current().location;
AstName name = parseName().name;
if (lexer.current().type == Lexeme::Dot3 || (FFlag::LuauParseRecoverTypePackEllipsis && seenPack))
if (lexer.current().type == Lexeme::Dot3 || seenPack)
{
seenPack = true;
if (FFlag::LuauParseRecoverTypePackEllipsis && lexer.current().type != Lexeme::Dot3)
if (lexer.current().type != Lexeme::Dot3)
report(lexer.current().location, "Generic types come before generic type packs");
else
nextLexeme();
@ -2414,9 +2413,6 @@ std::pair<AstArray<AstGenericType>, AstArray<AstGenericTypePack>> Parser::parseG
}
else
{
if (!FFlag::LuauParseRecoverTypePackEllipsis && seenPack)
report(lexer.current().location, "Generic types come before generic type packs");
if (withDefaultValues && lexer.current().type == '=')
{
seenDefault = true;

View file

@ -64,7 +64,7 @@ Makefile builds combine both into a single target and can be ran via `make test`
Luau uses C++ as its implementation language. The runtime requires C++11, whereas the compiler and analysis components require C++17. It should build without issues using Microsoft Visual Studio 2017 or later, or gcc-7 or clang-7 or later.
Other than the STL/CRT, Luau library components don't have external dependencies. The test suite depends on [doctest](https://github.com/onqtam/doctest) testing framework, and the REPL command-line depends on [cpp-linenoise](https://github.com/yhirose/cpp-linenoise).
Other than the STL/CRT, Luau library components don't have external dependencies. The test suite depends on [doctest](https://github.com/onqtam/doctest) testing framework, and the REPL command-line depends on [isocline](https://github.com/daanx/isocline).
# License

View file

@ -44,7 +44,7 @@ typedef int (*lua_Continuation)(lua_State* L, int status);
** prototype for memory-allocation functions
*/
typedef void* (*lua_Alloc)(lua_State* L, void* ud, void* ptr, size_t osize, size_t nsize);
typedef void* (*lua_Alloc)(void* ud, void* ptr, size_t osize, size_t nsize);
/* non-return type */
#define l_noret void LUA_NORETURN

View file

@ -151,8 +151,7 @@ l_noret luaD_throw(lua_State* L, int errcode)
static void correctstack(lua_State* L, TValue* oldstack)
{
L->top = (L->top - oldstack) + L->stack;
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
for (UpVal* up = L->openupval; up != NULL; up = (UpVal*)up->next)
for (UpVal* up = L->openupval; up != NULL; up = up->u.l.threadnext)
up->v = (up->v - oldstack) + L->stack;
for (CallInfo* ci = L->base_ci; ci <= L->ci; ci++)
{

View file

@ -6,13 +6,10 @@
#include "lmem.h"
#include "lgc.h"
LUAU_FASTFLAGVARIABLE(LuauNoDirectUpvalRemoval, false)
LUAU_FASTFLAG(LuauGcPagedSweep)
Proto* luaF_newproto(lua_State* L)
{
Proto* f = luaM_newgco(L, Proto, sizeof(Proto), L->activememcat);
luaC_link(L, f, LUA_TPROTO);
luaC_init(L, f, LUA_TPROTO);
f->k = NULL;
f->sizek = 0;
f->p = NULL;
@ -40,7 +37,7 @@ Proto* luaF_newproto(lua_State* L)
Closure* luaF_newLclosure(lua_State* L, int nelems, Table* e, Proto* p)
{
Closure* c = luaM_newgco(L, Closure, sizeLclosure(nelems), L->activememcat);
luaC_link(L, c, LUA_TFUNCTION);
luaC_init(L, c, LUA_TFUNCTION);
c->isC = 0;
c->env = e;
c->nupvalues = cast_byte(nelems);
@ -55,7 +52,7 @@ Closure* luaF_newLclosure(lua_State* L, int nelems, Table* e, Proto* p)
Closure* luaF_newCclosure(lua_State* L, int nelems, Table* e)
{
Closure* c = luaM_newgco(L, Closure, sizeCclosure(nelems), L->activememcat);
luaC_link(L, c, LUA_TFUNCTION);
luaC_init(L, c, LUA_TFUNCTION);
c->isC = 1;
c->env = e;
c->nupvalues = cast_byte(nelems);
@ -82,8 +79,7 @@ UpVal* luaF_findupval(lua_State* L, StkId level)
return p;
}
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
pp = (UpVal**)&p->next;
pp = &p->u.l.threadnext;
}
UpVal* uv = luaM_newgco(L, UpVal, sizeof(UpVal), L->activememcat); /* not found: create a new one */
@ -94,19 +90,10 @@ UpVal* luaF_findupval(lua_State* L, StkId level)
// chain the upvalue in the threads open upvalue list at the proper position
UpVal* next = *pp;
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
uv->next = (GCObject*)next;
if (FFlag::LuauGcPagedSweep)
{
uv->u.l.threadprev = pp;
if (next)
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
next->u.l.threadprev = (UpVal**)&uv->next;
}
}
uv->u.l.threadnext = next;
uv->u.l.threadprev = pp;
if (next)
next->u.l.threadprev = &uv->u.l.threadnext;
*pp = uv;
@ -125,15 +112,11 @@ void luaF_unlinkupval(UpVal* uv)
uv->u.l.next->u.l.prev = uv->u.l.prev;
uv->u.l.prev->u.l.next = uv->u.l.next;
if (FFlag::LuauGcPagedSweep)
{
// unlink upvalue from the thread open upvalue list
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and this and the following cast will not be required
*uv->u.l.threadprev = (UpVal*)uv->next;
// unlink upvalue from the thread open upvalue list
*uv->u.l.threadprev = uv->u.l.threadnext;
if (UpVal* next = (UpVal*)uv->next)
next->u.l.threadprev = uv->u.l.threadprev;
}
if (UpVal* next = uv->u.l.threadnext)
next->u.l.threadprev = uv->u.l.threadprev;
}
void luaF_freeupval(lua_State* L, UpVal* uv, lua_Page* page)
@ -145,34 +128,27 @@ void luaF_freeupval(lua_State* L, UpVal* uv, lua_Page* page)
void luaF_close(lua_State* L, StkId level)
{
global_State* g = L->global; // TODO: remove with FFlagLuauNoDirectUpvalRemoval
global_State* g = L->global;
UpVal* uv;
while (L->openupval != NULL && (uv = L->openupval)->v >= level)
{
GCObject* o = obj2gco(uv);
LUAU_ASSERT(!isblack(o) && uv->v != &uv->u.value);
if (!FFlag::LuauGcPagedSweep)
L->openupval = (UpVal*)uv->next; /* remove from `open' list */
// by removing the upvalue from global/thread open upvalue lists, L->openupval will be pointing to the next upvalue
luaF_unlinkupval(uv);
if (FFlag::LuauGcPagedSweep && isdead(g, o))
if (isdead(g, o))
{
// by removing the upvalue from global/thread open upvalue lists, L->openupval will be pointing to the next upvalue
luaF_unlinkupval(uv);
// close the upvalue without copying the dead data so that luaF_freeupval will not unlink again
uv->v = &uv->u.value;
}
else if (!FFlag::LuauNoDirectUpvalRemoval && isdead(g, o))
{
luaF_freeupval(L, uv, NULL); /* free upvalue */
}
else
{
// by removing the upvalue from global/thread open upvalue lists, L->openupval will be pointing to the next upvalue
luaF_unlinkupval(uv);
setobj(L, &uv->u.value, uv->v);
uv->v = &uv->u.value; /* now current value lives here */
luaC_linkupval(L, uv); /* link upvalue into `gcroot' list */
uv->v = &uv->u.value;
// GC state of a new closed upvalue has to be initialized
luaC_initupval(L, uv);
}
}
}

View file

@ -13,8 +13,6 @@
#include <string.h>
LUAU_FASTFLAGVARIABLE(LuauGcPagedSweep, false)
#define GC_SWEEPMAX 40
#define GC_SWEEPCOST 10
#define GC_SWEEPPAGESTEPCOST 4
@ -64,7 +62,6 @@ static void recordGcStateTime(global_State* g, int startgcstate, double seconds,
case GCSatomic:
g->gcstats.currcycle.atomictime += seconds;
break;
case GCSsweepstring:
case GCSsweep:
g->gcstats.currcycle.sweeptime += seconds;
break;
@ -490,65 +487,6 @@ static void freeobj(lua_State* L, GCObject* o, lua_Page* page)
}
}
#define sweepwholelist(L, p) sweeplist(L, p, SIZE_MAX)
static GCObject** sweeplist(lua_State* L, GCObject** p, size_t count)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
GCObject* curr;
global_State* g = L->global;
int deadmask = otherwhite(g);
LUAU_ASSERT(testbit(deadmask, FIXEDBIT)); /* make sure we never sweep fixed objects */
while ((curr = *p) != NULL && count-- > 0)
{
int alive = (curr->gch.marked ^ WHITEBITS) & deadmask;
if (curr->gch.tt == LUA_TTHREAD)
{
sweepwholelist(L, (GCObject**)&gco2th(curr)->openupval); /* sweep open upvalues */
lua_State* th = gco2th(curr);
if (alive)
{
resetbit(th->stackstate, THREAD_SLEEPINGBIT);
shrinkstack(th);
}
}
if (alive)
{ /* not dead? */
LUAU_ASSERT(!isdead(g, curr));
makewhite(g, curr); /* make it white (for next cycle) */
p = &curr->gch.next;
}
else
{ /* must erase `curr' */
LUAU_ASSERT(isdead(g, curr));
*p = curr->gch.next;
if (curr == g->rootgc) /* is the first element of the list? */
g->rootgc = curr->gch.next; /* adjust first */
freeobj(L, curr, NULL);
}
}
return p;
}
static void deletelist(lua_State* L, GCObject** p, GCObject* limit)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
GCObject* curr;
while ((curr = *p) != limit)
{
if (curr->gch.tt == LUA_TTHREAD) /* delete open upvalues of each thread */
deletelist(L, (GCObject**)&gco2th(curr)->openupval, NULL);
*p = curr->gch.next;
freeobj(L, curr, NULL);
}
}
static void shrinkbuffers(lua_State* L)
{
global_State* g = L->global;
@ -570,8 +508,6 @@ static void shrinkbuffersfull(lua_State* L)
static bool deletegco(void* context, lua_Page* page, GCObject* gco)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
// we are in the process of deleting everything
// threads with open upvalues will attempt to close them all on removal
// but those upvalues might point to stack values that were already deleted
@ -598,32 +534,13 @@ void luaC_freeall(lua_State* L)
LUAU_ASSERT(L == g->mainthread);
if (FFlag::LuauGcPagedSweep)
{
luaM_visitgco(L, L, deletegco);
luaM_visitgco(L, L, deletegco);
for (int i = 0; i < g->strt.size; i++) /* free all string lists */
LUAU_ASSERT(g->strt.hash[i] == NULL);
for (int i = 0; i < g->strt.size; i++) /* free all string lists */
LUAU_ASSERT(g->strt.hash[i] == NULL);
LUAU_ASSERT(L->global->strt.nuse == 0);
LUAU_ASSERT(g->strbufgc == NULL);
}
else
{
LUAU_ASSERT(L->next == NULL); /* mainthread is at the end of rootgc list */
deletelist(L, &g->rootgc, obj2gco(L));
for (int i = 0; i < g->strt.size; i++) /* free all string lists */
deletelist(L, (GCObject**)&g->strt.hash[i], NULL);
LUAU_ASSERT(L->global->strt.nuse == 0);
deletelist(L, (GCObject**)&g->strbufgc, NULL);
// unfortunately, when string objects are freed, the string table use count is decremented
// even when the string is a buffer that wasn't placed into the table
L->global->strt.nuse = 0;
}
LUAU_ASSERT(L->global->strt.nuse == 0);
LUAU_ASSERT(g->strbufgc == NULL);
}
static void markmt(global_State* g)
@ -687,26 +604,13 @@ static size_t atomic(lua_State* L)
g->weak = NULL;
/* flip current white */
g->currentwhite = cast_byte(otherwhite(g));
g->sweepstrgc = 0;
if (FFlag::LuauGcPagedSweep)
{
g->sweepgcopage = g->allgcopages;
g->gcstate = GCSsweep;
}
else
{
g->sweepgc = &g->rootgc;
g->gcstate = GCSsweepstring;
}
g->sweepgcopage = g->allgcopages;
g->gcstate = GCSsweep;
return work;
}
static bool sweepgco(lua_State* L, lua_Page* page, GCObject* gco)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
int deadmask = otherwhite(g);
@ -740,8 +644,6 @@ static bool sweepgco(lua_State* L, lua_Page* page, GCObject* gco)
// a version of generic luaM_visitpage specialized for the main sweep stage
static int sweepgcopage(lua_State* L, lua_Page* page)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
char* start;
char* end;
int busyBlocks;
@ -819,75 +721,29 @@ static size_t gcstep(lua_State* L, size_t limit)
cost = atomic(L); /* finish mark phase */
if (FFlag::LuauGcPagedSweep)
LUAU_ASSERT(g->gcstate == GCSsweep);
else
LUAU_ASSERT(g->gcstate == GCSsweepstring);
break;
}
case GCSsweepstring:
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
while (g->sweepstrgc < g->strt.size && cost < limit)
{
sweepwholelist(L, (GCObject**)&g->strt.hash[g->sweepstrgc++]);
cost += GC_SWEEPCOST;
}
// nothing more to sweep?
if (g->sweepstrgc >= g->strt.size)
{
// sweep string buffer list and preserve used string count
uint32_t nuse = L->global->strt.nuse;
sweepwholelist(L, (GCObject**)&g->strbufgc);
L->global->strt.nuse = nuse;
g->gcstate = GCSsweep; // end sweep-string phase
}
LUAU_ASSERT(g->gcstate == GCSsweep);
break;
}
case GCSsweep:
{
if (FFlag::LuauGcPagedSweep)
while (g->sweepgcopage && cost < limit)
{
while (g->sweepgcopage && cost < limit)
{
lua_Page* next = luaM_getnextgcopage(g->sweepgcopage); // page sweep might destroy the page
lua_Page* next = luaM_getnextgcopage(g->sweepgcopage); // page sweep might destroy the page
int steps = sweepgcopage(L, g->sweepgcopage);
int steps = sweepgcopage(L, g->sweepgcopage);
g->sweepgcopage = next;
cost += steps * GC_SWEEPPAGESTEPCOST;
}
// nothing more to sweep?
if (g->sweepgcopage == NULL)
{
// don't forget to visit main thread
sweepgco(L, NULL, obj2gco(g->mainthread));
shrinkbuffers(L);
g->gcstate = GCSpause; /* end collection */
}
g->sweepgcopage = next;
cost += steps * GC_SWEEPPAGESTEPCOST;
}
else
// nothing more to sweep?
if (g->sweepgcopage == NULL)
{
while (*g->sweepgc && cost < limit)
{
g->sweepgc = sweeplist(L, g->sweepgc, GC_SWEEPMAX);
// don't forget to visit main thread
sweepgco(L, NULL, obj2gco(g->mainthread));
cost += GC_SWEEPMAX * GC_SWEEPCOST;
}
if (*g->sweepgc == NULL)
{ /* nothing more to sweep? */
shrinkbuffers(L);
g->gcstate = GCSpause; /* end collection */
}
shrinkbuffers(L);
g->gcstate = GCSpause; /* end collection */
}
break;
}
@ -1013,26 +869,18 @@ void luaC_fullgc(lua_State* L)
if (g->gcstate <= GCSatomic)
{
/* reset sweep marks to sweep all elements (returning them to white) */
g->sweepstrgc = 0;
if (FFlag::LuauGcPagedSweep)
g->sweepgcopage = g->allgcopages;
else
g->sweepgc = &g->rootgc;
g->sweepgcopage = g->allgcopages;
/* reset other collector lists */
g->gray = NULL;
g->grayagain = NULL;
g->weak = NULL;
if (FFlag::LuauGcPagedSweep)
g->gcstate = GCSsweep;
else
g->gcstate = GCSsweepstring;
g->gcstate = GCSsweep;
}
LUAU_ASSERT(g->gcstate == GCSsweepstring || g->gcstate == GCSsweep);
LUAU_ASSERT(g->gcstate == GCSsweep);
/* finish any pending sweep phase */
while (g->gcstate != GCSpause)
{
LUAU_ASSERT(g->gcstate == GCSsweepstring || g->gcstate == GCSsweep);
LUAU_ASSERT(g->gcstate == GCSsweep);
gcstep(L, SIZE_MAX);
}
@ -1120,30 +968,19 @@ void luaC_barrierback(lua_State* L, Table* t)
g->grayagain = o;
}
void luaC_linkobj(lua_State* L, GCObject* o, uint8_t tt)
void luaC_initobj(lua_State* L, GCObject* o, uint8_t tt)
{
global_State* g = L->global;
if (!FFlag::LuauGcPagedSweep)
{
o->gch.next = g->rootgc;
g->rootgc = o;
}
o->gch.marked = luaC_white(g);
o->gch.tt = tt;
o->gch.memcat = L->activememcat;
}
void luaC_linkupval(lua_State* L, UpVal* uv)
void luaC_initupval(lua_State* L, UpVal* uv)
{
global_State* g = L->global;
GCObject* o = obj2gco(uv);
if (!FFlag::LuauGcPagedSweep)
{
o->gch.next = g->rootgc; /* link upvalue into `rootgc' list */
g->rootgc = o;
}
if (isgray(o))
{
if (keepinvariant(g))
@ -1221,9 +1058,6 @@ const char* luaC_statename(int state)
case GCSatomic:
return "atomic";
case GCSsweepstring:
return "sweepstring";
case GCSsweep:
return "sweep";

View file

@ -13,9 +13,7 @@
#define GCSpropagate 1
#define GCSpropagateagain 2
#define GCSatomic 3
// TODO: remove with FFlagLuauGcPagedSweep
#define GCSsweepstring 4
#define GCSsweep 5
#define GCSsweep 4
/*
** macro to tell when main invariant (white objects cannot point to black
@ -132,13 +130,13 @@
luaC_wakethread(L); \
}
#define luaC_link(L, o, tt) luaC_linkobj(L, cast_to(GCObject*, (o)), tt)
#define luaC_init(L, o, tt) luaC_initobj(L, cast_to(GCObject*, (o)), tt)
LUAI_FUNC void luaC_freeall(lua_State* L);
LUAI_FUNC void luaC_step(lua_State* L, bool assist);
LUAI_FUNC void luaC_fullgc(lua_State* L);
LUAI_FUNC void luaC_linkobj(lua_State* L, GCObject* o, uint8_t tt);
LUAI_FUNC void luaC_linkupval(lua_State* L, UpVal* uv);
LUAI_FUNC void luaC_initobj(lua_State* L, GCObject* o, uint8_t tt);
LUAI_FUNC void luaC_initupval(lua_State* L, UpVal* uv);
LUAI_FUNC void luaC_barrierupval(lua_State* L, GCObject* v);
LUAI_FUNC void luaC_barrierf(lua_State* L, GCObject* o, GCObject* v);
LUAI_FUNC void luaC_barriertable(lua_State* L, Table* t, GCObject* v);

View file

@ -13,8 +13,6 @@
#include <string.h>
#include <stdio.h>
LUAU_FASTFLAG(LuauGcPagedSweep)
static void validateobjref(global_State* g, GCObject* f, GCObject* t)
{
LUAU_ASSERT(!isdead(g, t));
@ -104,8 +102,7 @@ static void validatestack(global_State* g, lua_State* l)
if (l->namecall)
validateobjref(g, obj2gco(l), obj2gco(l->namecall));
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
for (UpVal* uv = l->openupval; uv; uv = (UpVal*)uv->next)
for (UpVal* uv = l->openupval; uv; uv = uv->u.l.threadnext)
{
LUAU_ASSERT(uv->tt == LUA_TUPVAL);
LUAU_ASSERT(uv->v != &uv->u.value);
@ -141,7 +138,7 @@ static void validateobj(global_State* g, GCObject* o)
/* dead objects can only occur during sweep */
if (isdead(g, o))
{
LUAU_ASSERT(g->gcstate == GCSsweepstring || g->gcstate == GCSsweep);
LUAU_ASSERT(g->gcstate == GCSsweep);
return;
}
@ -180,18 +177,6 @@ static void validateobj(global_State* g, GCObject* o)
}
}
static void validatelist(global_State* g, GCObject* o)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
while (o)
{
validateobj(g, o);
o = o->gch.next;
}
}
static void validategraylist(global_State* g, GCObject* o)
{
if (!keepinvariant(g))
@ -224,8 +209,6 @@ static void validategraylist(global_State* g, GCObject* o)
static bool validategco(void* context, lua_Page* page, GCObject* gco)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
lua_State* L = (lua_State*)context;
global_State* g = L->global;
@ -248,20 +231,9 @@ void luaC_validate(lua_State* L)
validategraylist(g, g->gray);
validategraylist(g, g->grayagain);
if (FFlag::LuauGcPagedSweep)
{
validategco(L, NULL, obj2gco(g->mainthread));
validategco(L, NULL, obj2gco(g->mainthread));
luaM_visitgco(L, L, validategco);
}
else
{
for (int i = 0; i < g->strt.size; ++i)
validatelist(g, (GCObject*)(g->strt.hash[i]));
validatelist(g, g->rootgc);
validatelist(g, (GCObject*)(g->strbufgc));
}
luaM_visitgco(L, L, validategco);
for (UpVal* uv = g->uvhead.u.l.next; uv != &g->uvhead; uv = uv->u.l.next)
{
@ -521,30 +493,8 @@ static void dumpobj(FILE* f, GCObject* o)
}
}
static void dumplist(FILE* f, GCObject* o)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
while (o)
{
dumpref(f, o);
fputc(':', f);
dumpobj(f, o);
fputc(',', f);
fputc('\n', f);
// thread has additional list containing collectable objects that are not present in rootgc
if (o->gch.tt == LUA_TTHREAD)
dumplist(f, (GCObject*)gco2th(o)->openupval);
o = o->gch.next;
}
}
static bool dumpgco(void* context, lua_Page* page, GCObject* gco)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
FILE* f = (FILE*)context;
dumpref(f, gco);
@ -563,19 +513,9 @@ void luaC_dump(lua_State* L, void* file, const char* (*categoryName)(lua_State*
fprintf(f, "{\"objects\":{\n");
if (FFlag::LuauGcPagedSweep)
{
dumpgco(f, NULL, obj2gco(g->mainthread));
dumpgco(f, NULL, obj2gco(g->mainthread));
luaM_visitgco(L, f, dumpgco);
}
else
{
dumplist(f, g->rootgc);
dumplist(f, (GCObject*)(g->strbufgc));
for (int i = 0; i < g->strt.size; ++i)
dumplist(f, (GCObject*)(g->strt.hash[i]));
}
luaM_visitgco(L, f, dumpgco);
fprintf(f, "\"0\":{\"type\":\"userdata\",\"cat\":0,\"size\":0}\n"); // to avoid issues with trailing ,
fprintf(f, "},\"roots\":{\n");

View file

@ -68,7 +68,7 @@ void luaL_sandboxthread(lua_State* L)
lua_setsafeenv(L, LUA_GLOBALSINDEX, true);
}
static void* l_alloc(lua_State* L, void* ud, void* ptr, size_t osize, size_t nsize)
static void* l_alloc(void* ud, void* ptr, size_t osize, size_t nsize)
{
(void)ud;
(void)osize;

View file

@ -78,8 +78,6 @@
* allocated pages.
*/
LUAU_FASTFLAG(LuauGcPagedSweep)
#ifndef __has_feature
#define __has_feature(x) 0
#endif
@ -98,8 +96,10 @@ LUAU_FASTFLAG(LuauGcPagedSweep)
* To prevent some of them accidentally growing and us losing memory without realizing it, we're going to lock
* the sizes of all critical structures down.
*/
#if defined(__APPLE__) && !defined(__MACH__)
#if defined(__APPLE__)
#define ABISWITCH(x64, ms32, gcc32) (sizeof(void*) == 8 ? x64 : gcc32)
#elif defined(__i386__)
#define ABISWITCH(x64, ms32, gcc32) (gcc32)
#else
// Android somehow uses a similar ABI to MSVC, *not* to iOS...
#define ABISWITCH(x64, ms32, gcc32) (sizeof(void*) == 8 ? x64 : ms32)
@ -114,14 +114,8 @@ static_assert(sizeof(LuaNode) == ABISWITCH(32, 32, 32), "size mismatch for table
#endif
static_assert(offsetof(TString, data) == ABISWITCH(24, 20, 20), "size mismatch for string header");
// TODO (FFlagLuauGcPagedSweep): this will become ABISWITCH(16, 16, 16)
static_assert(offsetof(Udata, data) == ABISWITCH(24, 16, 16), "size mismatch for userdata header");
// TODO (FFlagLuauGcPagedSweep): this will become ABISWITCH(48, 32, 32)
static_assert(sizeof(Table) == ABISWITCH(56, 36, 36), "size mismatch for table header");
// TODO (FFlagLuauGcPagedSweep): new code with old 'next' pointer requires that GCObject start at the same point as TString/UpVal
static_assert(offsetof(GCObject, uv) == 0, "UpVal data must be located at the start of the GCObject");
static_assert(offsetof(GCObject, ts) == 0, "TString data must be located at the start of the GCObject");
static_assert(offsetof(Udata, data) == ABISWITCH(16, 16, 12), "size mismatch for userdata header");
static_assert(sizeof(Table) == ABISWITCH(48, 32, 32), "size mismatch for table header");
const size_t kSizeClasses = LUA_SIZECLASSES;
const size_t kMaxSmallSize = 512;
@ -208,53 +202,13 @@ l_noret luaM_toobig(lua_State* L)
luaG_runerror(L, "memory allocation error: block too big");
}
static lua_Page* newpageold(lua_State* L, uint8_t sizeClass)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
global_State* g = L->global;
lua_Page* page = (lua_Page*)(*g->frealloc)(L, g->ud, NULL, 0, kPageSize);
if (!page)
luaD_throw(L, LUA_ERRMEM);
int blockSize = kSizeClassConfig.sizeOfClass[sizeClass] + kBlockHeader;
int blockCount = (kPageSize - offsetof(lua_Page, data)) / blockSize;
ASAN_POISON_MEMORY_REGION(page->data, blockSize * blockCount);
// setup page header
page->prev = NULL;
page->next = NULL;
page->gcolistprev = NULL;
page->gcolistnext = NULL;
page->pageSize = kPageSize;
page->blockSize = blockSize;
// note: we start with the last block in the page and move downward
// either order would work, but that way we don't need to store the block count in the page
// additionally, GC stores objects in singly linked lists, and this way the GC lists end up in increasing pointer order
page->freeList = NULL;
page->freeNext = (blockCount - 1) * blockSize;
page->busyBlocks = 0;
// prepend a page to page freelist (which is empty because we only ever allocate a new page when it is!)
LUAU_ASSERT(!g->freepages[sizeClass]);
g->freepages[sizeClass] = page;
return page;
}
static lua_Page* newpage(lua_State* L, lua_Page** gcopageset, int pageSize, int blockSize, int blockCount)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
LUAU_ASSERT(pageSize - int(offsetof(lua_Page, data)) >= blockSize * blockCount);
lua_Page* page = (lua_Page*)(*g->frealloc)(L, g->ud, NULL, 0, pageSize);
lua_Page* page = (lua_Page*)(*g->frealloc)(g->ud, NULL, 0, pageSize);
if (!page)
luaD_throw(L, LUA_ERRMEM);
@ -290,8 +244,6 @@ static lua_Page* newpage(lua_State* L, lua_Page** gcopageset, int pageSize, int
static lua_Page* newclasspage(lua_State* L, lua_Page** freepageset, lua_Page** gcopageset, uint8_t sizeClass, bool storeMetadata)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
int blockSize = kSizeClassConfig.sizeOfClass[sizeClass] + (storeMetadata ? kBlockHeader : 0);
int blockCount = (kPageSize - offsetof(lua_Page, data)) / blockSize;
@ -304,29 +256,8 @@ static lua_Page* newclasspage(lua_State* L, lua_Page** freepageset, lua_Page** g
return page;
}
static void freepageold(lua_State* L, lua_Page* page, uint8_t sizeClass)
{
LUAU_ASSERT(!FFlag::LuauGcPagedSweep);
global_State* g = L->global;
// remove page from freelist
if (page->next)
page->next->prev = page->prev;
if (page->prev)
page->prev->next = page->next;
else if (g->freepages[sizeClass] == page)
g->freepages[sizeClass] = page->next;
// so long
(*g->frealloc)(L, g->ud, page, kPageSize, 0);
}
static void freepage(lua_State* L, lua_Page** gcopageset, lua_Page* page)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
if (gcopageset)
@ -342,13 +273,11 @@ static void freepage(lua_State* L, lua_Page** gcopageset, lua_Page* page)
}
// so long
(*g->frealloc)(L, g->ud, page, page->pageSize, 0);
(*g->frealloc)(g->ud, page, page->pageSize, 0);
}
static void freeclasspage(lua_State* L, lua_Page** freepageset, lua_Page** gcopageset, lua_Page* page, uint8_t sizeClass)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
// remove page from freelist
if (page->next)
page->next->prev = page->prev;
@ -368,12 +297,7 @@ static void* newblock(lua_State* L, int sizeClass)
// slow path: no page in the freelist, allocate a new one
if (!page)
{
if (FFlag::LuauGcPagedSweep)
page = newclasspage(L, g->freepages, NULL, sizeClass, true);
else
page = newpageold(L, sizeClass);
}
page = newclasspage(L, g->freepages, NULL, sizeClass, true);
LUAU_ASSERT(!page->prev);
LUAU_ASSERT(page->freeList || page->freeNext >= 0);
@ -416,8 +340,6 @@ static void* newblock(lua_State* L, int sizeClass)
static void* newgcoblock(lua_State* L, int sizeClass)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
lua_Page* page = g->freegcopages[sizeClass];
@ -496,17 +418,11 @@ static void freeblock(lua_State* L, int sizeClass, void* block)
// if it's the last block in the page, we don't need the page
if (page->busyBlocks == 0)
{
if (FFlag::LuauGcPagedSweep)
freeclasspage(L, g->freepages, NULL, page, sizeClass);
else
freepageold(L, page, sizeClass);
}
freeclasspage(L, g->freepages, NULL, page, sizeClass);
}
static void freegcoblock(lua_State* L, int sizeClass, void* block, lua_Page* page)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
LUAU_ASSERT(page && page->busyBlocks > 0);
LUAU_ASSERT(page->blockSize == kSizeClassConfig.sizeOfClass[sizeClass]);
LUAU_ASSERT(block >= page->data && block < (char*)page + page->pageSize);
@ -544,7 +460,7 @@ void* luaM_new_(lua_State* L, size_t nsize, uint8_t memcat)
int nclass = sizeclass(nsize);
void* block = nclass >= 0 ? newblock(L, nclass) : (*g->frealloc)(L, g->ud, NULL, 0, nsize);
void* block = nclass >= 0 ? newblock(L, nclass) : (*g->frealloc)(g->ud, NULL, 0, nsize);
if (block == NULL && nsize > 0)
luaD_throw(L, LUA_ERRMEM);
@ -556,9 +472,6 @@ void* luaM_new_(lua_State* L, size_t nsize, uint8_t memcat)
GCObject* luaM_newgco_(lua_State* L, size_t nsize, uint8_t memcat)
{
if (!FFlag::LuauGcPagedSweep)
return (GCObject*)luaM_new_(L, nsize, memcat);
// we need to accommodate space for link for free blocks (freegcolink)
LUAU_ASSERT(nsize >= kGCOLinkOffset + sizeof(void*));
@ -602,7 +515,7 @@ void luaM_free_(lua_State* L, void* block, size_t osize, uint8_t memcat)
if (oclass >= 0)
freeblock(L, oclass, block);
else
(*g->frealloc)(L, g->ud, block, osize, 0);
(*g->frealloc)(g->ud, block, osize, 0);
g->totalbytes -= osize;
g->memcatbytes[memcat] -= osize;
@ -610,12 +523,6 @@ void luaM_free_(lua_State* L, void* block, size_t osize, uint8_t memcat)
void luaM_freegco_(lua_State* L, GCObject* block, size_t osize, uint8_t memcat, lua_Page* page)
{
if (!FFlag::LuauGcPagedSweep)
{
luaM_free_(L, block, osize, memcat);
return;
}
global_State* g = L->global;
LUAU_ASSERT((osize == 0) == (block == NULL));
@ -652,7 +559,7 @@ void* luaM_realloc_(lua_State* L, void* block, size_t osize, size_t nsize, uint8
// if either block needs to be allocated using a block allocator, we can't use realloc directly
if (nclass >= 0 || oclass >= 0)
{
result = nclass >= 0 ? newblock(L, nclass) : (*g->frealloc)(L, g->ud, NULL, 0, nsize);
result = nclass >= 0 ? newblock(L, nclass) : (*g->frealloc)(g->ud, NULL, 0, nsize);
if (result == NULL && nsize > 0)
luaD_throw(L, LUA_ERRMEM);
@ -662,11 +569,11 @@ void* luaM_realloc_(lua_State* L, void* block, size_t osize, size_t nsize, uint8
if (oclass >= 0)
freeblock(L, oclass, block);
else
(*g->frealloc)(L, g->ud, block, osize, 0);
(*g->frealloc)(g->ud, block, osize, 0);
}
else
{
result = (*g->frealloc)(L, g->ud, block, osize, nsize);
result = (*g->frealloc)(g->ud, block, osize, nsize);
if (result == NULL && nsize > 0)
luaD_throw(L, LUA_ERRMEM);
}
@ -679,8 +586,6 @@ void* luaM_realloc_(lua_State* L, void* block, size_t osize, size_t nsize, uint8
void luaM_getpagewalkinfo(lua_Page* page, char** start, char** end, int* busyBlocks, int* blockSize)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
int blockCount = (page->pageSize - offsetof(lua_Page, data)) / page->blockSize;
LUAU_ASSERT(page->freeNext >= -page->blockSize && page->freeNext <= (blockCount - 1) * page->blockSize);
@ -700,8 +605,6 @@ lua_Page* luaM_getnextgcopage(lua_Page* page)
void luaM_visitpage(lua_Page* page, void* context, bool (*visitor)(void* context, lua_Page* page, GCObject* gco))
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
char* start;
char* end;
int busyBlocks;
@ -730,8 +633,6 @@ void luaM_visitpage(lua_Page* page, void* context, bool (*visitor)(void* context
void luaM_visitgco(lua_State* L, void* context, bool (*visitor)(void* context, lua_Page* page, GCObject* gco))
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
for (lua_Page* curr = g->allgcopages; curr;)

View file

@ -7,11 +7,7 @@
struct lua_Page;
union GCObject;
// TODO: remove with FFlagLuauGcPagedSweep and rename luaM_newgco to luaM_new
#define luaM_new(L, t, size, memcat) cast_to(t*, luaM_new_(L, size, memcat))
#define luaM_newgco(L, t, size, memcat) cast_to(t*, luaM_newgco_(L, size, memcat))
// TODO: remove with FFlagLuauGcPagedSweep and rename luaM_freegco to luaM_free
#define luaM_free(L, p, size, memcat) luaM_free_(L, (p), size, memcat)
#define luaM_freegco(L, p, size, memcat, page) luaM_freegco_(L, obj2gco(p), size, memcat, page)
#define luaM_arraysize_(n, e) ((cast_to(size_t, (n)) <= SIZE_MAX / (e)) ? (n) * (e) : (luaM_toobig(L), SIZE_MAX))

View file

@ -15,7 +15,6 @@ typedef union GCObject GCObject;
*/
// clang-format off
#define CommonHeader \
GCObject* next; /* TODO: remove with FFlagLuauGcPagedSweep */ \
uint8_t tt; uint8_t marked; uint8_t memcat
// clang-format on
@ -233,6 +232,8 @@ typedef struct TString
int16_t atom;
// 2 byte padding
TString* next; // next string in the hash table bucket or the string buffer linked list
unsigned int hash;
unsigned int len;
@ -327,7 +328,7 @@ typedef struct UpVal
struct UpVal* next;
/* thread double linked list (when open) */
// TODO: when FFlagLuauGcPagedSweep is removed, old outer 'next' value will be placed here
struct UpVal* threadnext;
/* note: this is the location of a pointer to this upvalue in the previous element that can be either an UpVal or a lua_State */
struct UpVal** threadprev;
} l;

View file

@ -10,7 +10,6 @@
#include "ldo.h"
#include "ldebug.h"
LUAU_FASTFLAG(LuauGcPagedSweep)
LUAU_FASTFLAGVARIABLE(LuauReduceStackReallocs, false)
/*
@ -90,8 +89,6 @@ static void close_state(lua_State* L)
global_State* g = L->global;
luaF_close(L, L->stack); /* close all upvalues for this thread */
luaC_freeall(L); /* collect all objects */
if (!FFlag::LuauGcPagedSweep)
LUAU_ASSERT(g->rootgc == obj2gco(L));
LUAU_ASSERT(g->strbufgc == NULL);
LUAU_ASSERT(g->strt.nuse == 0);
luaM_freearray(L, L->global->strt.hash, L->global->strt.size, TString*, 0);
@ -99,22 +96,20 @@ static void close_state(lua_State* L)
for (int i = 0; i < LUA_SIZECLASSES; i++)
{
LUAU_ASSERT(g->freepages[i] == NULL);
if (FFlag::LuauGcPagedSweep)
LUAU_ASSERT(g->freegcopages[i] == NULL);
LUAU_ASSERT(g->freegcopages[i] == NULL);
}
if (FFlag::LuauGcPagedSweep)
LUAU_ASSERT(g->allgcopages == NULL);
LUAU_ASSERT(g->allgcopages == NULL);
LUAU_ASSERT(g->totalbytes == sizeof(LG));
LUAU_ASSERT(g->memcatbytes[0] == sizeof(LG));
for (int i = 1; i < LUA_MEMORY_CATEGORIES; i++)
LUAU_ASSERT(g->memcatbytes[i] == 0);
(*g->frealloc)(L, g->ud, L, sizeof(LG), 0);
(*g->frealloc)(g->ud, L, sizeof(LG), 0);
}
lua_State* luaE_newthread(lua_State* L)
{
lua_State* L1 = luaM_newgco(L, lua_State, sizeof(lua_State), L->activememcat);
luaC_link(L, L1, LUA_TTHREAD);
luaC_init(L, L1, LUA_TTHREAD);
preinit_state(L1, L->global);
L1->activememcat = L->activememcat; // inherit the active memory category
stack_init(L1, L); /* init stack */
@ -184,13 +179,11 @@ lua_State* lua_newstate(lua_Alloc f, void* ud)
int i;
lua_State* L;
global_State* g;
void* l = (*f)(NULL, ud, NULL, 0, sizeof(LG));
void* l = (*f)(ud, NULL, 0, sizeof(LG));
if (l == NULL)
return NULL;
L = (lua_State*)l;
g = &((LG*)L)->g;
if (!FFlag::LuauGcPagedSweep)
L->next = NULL;
L->tt = LUA_TTHREAD;
L->marked = g->currentwhite = bit2mask(WHITE0BIT, FIXEDBIT);
L->memcat = 0;
@ -214,11 +207,6 @@ lua_State* lua_newstate(lua_Alloc f, void* ud)
setnilvalue(&g->pseudotemp);
setnilvalue(registry(L));
g->gcstate = GCSpause;
if (!FFlag::LuauGcPagedSweep)
g->rootgc = obj2gco(L);
g->sweepstrgc = 0;
if (!FFlag::LuauGcPagedSweep)
g->sweepgc = &g->rootgc;
g->gray = NULL;
g->grayagain = NULL;
g->weak = NULL;
@ -230,14 +218,10 @@ lua_State* lua_newstate(lua_Alloc f, void* ud)
for (i = 0; i < LUA_SIZECLASSES; i++)
{
g->freepages[i] = NULL;
if (FFlag::LuauGcPagedSweep)
g->freegcopages[i] = NULL;
}
if (FFlag::LuauGcPagedSweep)
{
g->allgcopages = NULL;
g->sweepgcopage = NULL;
g->freegcopages[i] = NULL;
}
g->allgcopages = NULL;
g->sweepgcopage = NULL;
for (i = 0; i < LUA_T_COUNT; i++)
g->mt[i] = NULL;
for (i = 0; i < LUA_UTAG_LIMIT; i++)

View file

@ -142,11 +142,6 @@ typedef struct global_State
uint8_t gcstate; /* state of garbage collector */
int sweepstrgc; /* position of sweep in `strt' */
// TODO: remove with FFlagLuauGcPagedSweep
GCObject* rootgc; /* list of all collectable objects */
// TODO: remove with FFlagLuauGcPagedSweep
GCObject** sweepgc; /* position of sweep in `rootgc' */
GCObject* gray; /* list of gray objects */
GCObject* grayagain; /* list of objects to be traversed atomically */
GCObject* weak; /* list of weak tables (to be cleared) */

View file

@ -7,8 +7,6 @@
#include <string.h>
LUAU_FASTFLAG(LuauGcPagedSweep)
unsigned int luaS_hash(const char* str, size_t len)
{
// Note that this hashing algorithm is replicated in BytecodeBuilder.cpp, BytecodeBuilder::getStringHash
@ -46,8 +44,6 @@ unsigned int luaS_hash(const char* str, size_t len)
void luaS_resize(lua_State* L, int newsize)
{
if (L->global->gcstate == GCSsweepstring)
return; /* cannot resize during GC traverse */
TString** newhash = luaM_newarray(L, newsize, TString*, 0);
stringtable* tb = &L->global->strt;
for (int i = 0; i < newsize; i++)
@ -58,13 +54,11 @@ void luaS_resize(lua_State* L, int newsize)
TString* p = tb->hash[i];
while (p)
{ /* for each node in the list */
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
TString* next = (TString*)p->next; /* save next */
TString* next = p->next; /* save next */
unsigned int h = p->hash;
int h1 = lmod(h, newsize); /* new position */
LUAU_ASSERT(cast_int(h % newsize) == lmod(h, newsize));
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
p->next = (GCObject*)newhash[h1]; /* chain it */
p->next = newhash[h1]; /* chain it */
newhash[h1] = p;
p = next;
}
@ -91,8 +85,7 @@ static TString* newlstr(lua_State* L, const char* str, size_t l, unsigned int h)
ts->atom = L->global->cb.useratom ? L->global->cb.useratom(ts->data, l) : -1;
tb = &L->global->strt;
h = lmod(h, tb->size);
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the case will not be required
ts->next = (GCObject*)tb->hash[h]; /* chain new entry */
ts->next = tb->hash[h]; /* chain new entry */
tb->hash[h] = ts;
tb->nuse++;
if (tb->nuse > cast_to(uint32_t, tb->size) && tb->size <= INT_MAX / 2)
@ -104,20 +97,9 @@ static void linkstrbuf(lua_State* L, TString* ts)
{
global_State* g = L->global;
if (FFlag::LuauGcPagedSweep)
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
ts->next = (GCObject*)g->strbufgc;
g->strbufgc = ts;
ts->marked = luaC_white(g);
}
else
{
GCObject* o = obj2gco(ts);
o->gch.next = (GCObject*)g->strbufgc;
g->strbufgc = gco2ts(o);
o->gch.marked = luaC_white(g);
}
ts->next = g->strbufgc;
g->strbufgc = ts;
ts->marked = luaC_white(g);
}
static void unlinkstrbuf(lua_State* L, TString* ts)
@ -130,14 +112,12 @@ static void unlinkstrbuf(lua_State* L, TString* ts)
{
if (curr == ts)
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
*p = (TString*)curr->next;
*p = curr->next;
return;
}
else
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
p = (TString**)&curr->next;
p = &curr->next;
}
}
@ -167,8 +147,7 @@ TString* luaS_buffinish(lua_State* L, TString* ts)
int bucket = lmod(h, tb->size);
// search if we already have this string in the hash table
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
for (TString* el = tb->hash[bucket]; el != NULL; el = (TString*)el->next)
for (TString* el = tb->hash[bucket]; el != NULL; el = el->next)
{
if (el->len == ts->len && memcmp(el->data, ts->data, ts->len) == 0)
{
@ -187,8 +166,7 @@ TString* luaS_buffinish(lua_State* L, TString* ts)
// Complete string object
ts->atom = L->global->cb.useratom ? L->global->cb.useratom(ts->data, ts->len) : -1;
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
ts->next = (GCObject*)tb->hash[bucket]; // chain new entry
ts->next = tb->hash[bucket]; // chain new entry
tb->hash[bucket] = ts;
tb->nuse++;
@ -201,8 +179,7 @@ TString* luaS_buffinish(lua_State* L, TString* ts)
TString* luaS_newlstr(lua_State* L, const char* str, size_t l)
{
unsigned int h = luaS_hash(str, l);
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
for (TString* el = L->global->strt.hash[lmod(h, L->global->strt.size)]; el != NULL; el = (TString*)el->next)
for (TString* el = L->global->strt.hash[lmod(h, L->global->strt.size)]; el != NULL; el = el->next)
{
if (el->len == l && (memcmp(str, getstr(el), l) == 0))
{
@ -217,8 +194,6 @@ TString* luaS_newlstr(lua_State* L, const char* str, size_t l)
static bool unlinkstr(lua_State* L, TString* ts)
{
LUAU_ASSERT(FFlag::LuauGcPagedSweep);
global_State* g = L->global;
TString** p = &g->strt.hash[lmod(ts->hash, g->strt.size)];
@ -227,14 +202,12 @@ static bool unlinkstr(lua_State* L, TString* ts)
{
if (curr == ts)
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
*p = (TString*)curr->next;
*p = curr->next;
return true;
}
else
{
// TODO (FFlagLuauGcPagedSweep): 'next' type will change after removal of the flag and the cast will not be required
p = (TString**)&curr->next;
p = &curr->next;
}
}
@ -243,20 +216,11 @@ static bool unlinkstr(lua_State* L, TString* ts)
void luaS_free(lua_State* L, TString* ts, lua_Page* page)
{
if (FFlag::LuauGcPagedSweep)
{
// Unchain from the string table
if (!unlinkstr(L, ts))
unlinkstrbuf(L, ts); // An unlikely scenario when we have a string buffer on our hands
else
L->global->strt.nuse--;
luaM_freegco(L, ts, sizestring(ts->len), ts->memcat, page);
}
// Unchain from the string table
if (!unlinkstr(L, ts))
unlinkstrbuf(L, ts); // An unlikely scenario when we have a string buffer on our hands
else
{
L->global->strt.nuse--;
luaM_free(L, ts, sizestring(ts->len), ts->memcat);
}
luaM_freegco(L, ts, sizestring(ts->len), ts->memcat, page);
}

View file

@ -425,7 +425,7 @@ static void rehash(lua_State* L, Table* t, const TValue* ek)
Table* luaH_new(lua_State* L, int narray, int nhash)
{
Table* t = luaM_newgco(L, Table, sizeof(Table), L->activememcat);
luaC_link(L, t, LUA_TTABLE);
luaC_init(L, t, LUA_TTABLE);
t->metatable = NULL;
t->flags = cast_byte(~0);
t->array = NULL;
@ -742,7 +742,7 @@ int luaH_getn(Table* t)
Table* luaH_clone(lua_State* L, Table* tt)
{
Table* t = luaM_newgco(L, Table, sizeof(Table), L->activememcat);
luaC_link(L, t, LUA_TTABLE);
luaC_init(L, t, LUA_TTABLE);
t->metatable = tt->metatable;
t->flags = tt->flags;
t->array = NULL;

View file

@ -12,7 +12,7 @@ Udata* luaU_newudata(lua_State* L, size_t s, int tag)
if (s > INT_MAX - sizeof(Udata))
luaM_toobig(L);
Udata* u = luaM_newgco(L, Udata, sizeudata(s), L->activememcat);
luaC_link(L, u, LUA_TUSERDATA);
luaC_init(L, u, LUA_TUSERDATA);
u->len = int(s);
u->metatable = NULL;
LUAU_ASSERT(tag >= 0 && tag <= 255);

View file

@ -0,0 +1,164 @@
---
layout: single
title: "Luau Recap: February 2022"
---
Luau is our new language that you can read more about at [https://luau-lang.org](https://luau-lang.org).
[Cross-posted to the [Roblox Developer Forum](https://devforum.roblox.com/t/luau-recap-february-2022/).]
## Default type alias type parameters
We have introduced a syntax to provide default type arguments inside the type alias type parameter list.
It is now possible to have type functions where the instantiation can omit some type arguments.
You can provide concrete types:
```lua
--!strict
type FieldResolver<T, Data = {[string]: any}> = (T, Data) -> number
local a: FieldResolver<number> = ...
local b: FieldResolver<number, {name: string}> = ...
```
Or reference parameters defined earlier in the list:
```lua
--!strict
type EqComp<T, U = T> = (l: T, r: U) -> boolean
local a: EqComp<number> = ... -- (l: number, r: number) -> boolean
local b: EqComp<number, string> = ... -- (l: number, r: string) -> boolean
```
Type pack parameters can also have a default type pack:
```lua
--!strict
type Process<T, U... = ...string> = (T) -> U...
local a: Process<number> = ... -- (number) -> ...string
local b: Process<number, (boolean, string)> = ... -- (number) -> (boolean, string)
```
If all type parameters have a default type, it is now possible to reference that without providing any type arguments:
```lua
--!strict
type All<T = string, U = number> = (T) -> U
local a: All -- ok
local b: All<> -- ok as well
```
For more details, you can read the original [RFC proposal](https://github.com/Roblox/luau/blob/master/rfcs/syntax-default-type-alias-type-parameters.md).
## Typechecking improvements
This month we had many fixes to improve our type inference and reduce false positive errors.
if-then-else expression can now have different types in each branch:
```lua
--!strict
local a = if x then 5 else nil -- 'a' will have type 'number?'
local b = if x then 1 else '2' -- 'b' will have type 'number | string'
```
And if the expected result type is known, you will not get an error in cases like these:
```lua
--!strict
type T = {number | string}
-- different array element types don't give an error if that is expected
local c: T = if x then {1, "x", 2, "y"} else {0}
```
---
`assert` result is now known to not be 'falsy' (`false` or `nil`):
```lua
--!strict
local function f(x: number?): number
return assert(x) -- no longer an error
end
```
---
We fixed cases where length operator `#` reported an error when used on a compatible type:
```lua
--!strict
local union: {number} | {string}
local a = #union -- no longer an error
```
---
Functions with different variadic argument/return types are no longer compatible:
```lua
--!strict
local function f(): (number, ...string)
return 2, "a", "b"
end
local g: () -> (number, ...boolean) = f -- error
```
---
We have also fixed:
* false positive errors caused by incorrect reuse of generic types across different function declarations
* issues with forward-declared intersection types
* wrong return type annotation for table.move
* various crashes reported by developers
## Linter improvements
A new static analysis warning was introduced to mark incorrect use of a '`a and b or c`' pattern. When 'b' is 'falsy' (`false` or `nil`), result will always be 'c', even if the expression 'a' was true:
```lua
local function f(x: number)
-- The and-or expression always evaluates to the second alternative because the first alternative is false; consider using if-then-else expression instead
return x < 0.5 and false or 42
end
```
Like we say in the warning, new if-then-else expression doesn't have this pitfall:
```lua
local function g(x: number)
return if x < 0.5 then false else 42
end
```
---
We have also introduced a check for misspelled comment directives:
```lua
--!non-strict
-- ^ Unknown comment directive 'non-strict'; did you mean 'nonstrict'?
```
## Performance improvements
For performance, we have changed how our Garbage Collector collects unreachable memory.
This rework makes it possible to free memory 2.5x faster and also comes with a small change to how we store Luau objects in memory. For example, each table now uses 16 fewer bytes on 64-bit platforms.
Another optimization was made for `select(_, ...)` call.
It is now using a special fast path that has constant-time complexity in number of arguments (~3x faster with 10 arguments).
## Thanks
A special thanks to all the fine folks who contributed PRs this month!
* [mikejsavage](https://github.com/mikejsavage)
* [TheGreatSageEqualToHeaven](https://github.com/TheGreatSageEqualToHeaven)
* [petrihakkinen](https://github.com/petrihakkinen)

View file

@ -1,10 +1,12 @@
// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details
#include <string>
#include "Luau/TypeInfer.h"
#include "Luau/Linter.h"
#include "Luau/BuiltinDefinitions.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Common.h"
#include "Luau/Linter.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Parser.h"
#include "Luau/TypeInfer.h"
extern "C" int LLVMFuzzerTestOneInput(const uint8_t* Data, size_t Size)
{

View file

@ -96,11 +96,13 @@ message ExprIndexExpr {
}
message ExprFunction {
repeated Local args = 1;
required bool vararg = 2;
required StatBlock body = 3;
repeated Type types = 4;
repeated Type rettypes = 5;
repeated Typename generics = 1;
repeated Typename genericpacks = 2;
repeated Local args = 3;
required bool vararg = 4;
required StatBlock body = 5;
repeated Type types = 6;
repeated Type rettypes = 7;
}
message TableItem {
@ -153,7 +155,10 @@ message ExprBinary {
message ExprIfElse {
required Expr cond = 1;
required Expr then = 2;
required Expr else = 3;
oneof else_oneof {
Expr else = 3;
ExprIfElse elseif = 4;
}
}
message LValue {
@ -183,6 +188,7 @@ message Stat {
StatFunction function = 14;
StatLocalFunction local_function = 15;
StatTypeAlias type_alias = 16;
StatRequireIntoLocalHelper require_into_local = 17;
}
}
@ -276,9 +282,16 @@ message StatLocalFunction {
}
message StatTypeAlias {
required Typename name = 1;
required Type type = 2;
repeated Typename generics = 3;
required bool export = 1;
required Typename name = 2;
required Type type = 3;
repeated Typename generics = 4;
repeated Typename genericpacks = 5;
}
message StatRequireIntoLocalHelper {
required Local var = 1;
required int32 modulenum = 2;
}
message Type {
@ -292,6 +305,8 @@ message Type {
TypeIntersection intersection = 7;
TypeClass class = 8;
TypeRef ref = 9;
TypeBoolean boolean = 10;
TypeString string = 11;
}
}
@ -301,7 +316,8 @@ message TypePrimitive {
message TypeLiteral {
required Typename name = 1;
repeated Typename generics = 2;
repeated Type generics = 2;
repeated Typename genericpacks = 3;
}
message TypeTableItem {
@ -320,8 +336,10 @@ message TypeTable {
}
message TypeFunction {
repeated Type args = 1;
repeated Type rets = 2;
repeated Typename generics = 1;
repeated Typename genericpacks = 2;
repeated Type args = 3;
repeated Type rets = 4;
// TODO: vararg?
}
@ -347,3 +365,16 @@ message TypeRef {
required Local prefix = 1;
required Typename index = 2;
}
message TypeBoolean {
required bool val = 1;
}
message TypeString {
required string val = 1;
}
message ModuleSet {
optional StatBlock module = 1;
required StatBlock program = 2;
}

View file

@ -2,16 +2,17 @@
#include "src/libfuzzer/libfuzzer_macro.h"
#include "luau.pb.h"
#include "Luau/TypeInfer.h"
#include "Luau/BuiltinDefinitions.h"
#include "Luau/ModuleResolver.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Compiler.h"
#include "Luau/Linter.h"
#include "Luau/BytecodeBuilder.h"
#include "Luau/Common.h"
#include "Luau/Compiler.h"
#include "Luau/Frontend.h"
#include "Luau/Linter.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Parser.h"
#include "Luau/ToString.h"
#include "Luau/Transpiler.h"
#include "Luau/TypeInfer.h"
#include "lua.h"
#include "lualib.h"
@ -30,7 +31,7 @@ const bool kFuzzTypes = true;
static_assert(!(kFuzzVM && !kFuzzCompiler), "VM requires the compiler!");
std::string protoprint(const luau::StatBlock& stat, bool types);
std::vector<std::string> protoprint(const luau::ModuleSet& stat, bool types);
LUAU_FASTINT(LuauTypeInferRecursionLimit)
LUAU_FASTINT(LuauTypeInferTypePackLoopLimit)
@ -38,6 +39,7 @@ LUAU_FASTINT(LuauCheckRecursionLimit)
LUAU_FASTINT(LuauTableTypeMaximumStringifierLength)
LUAU_FASTINT(LuauTypeInferIterationLimit)
LUAU_FASTINT(LuauTarjanChildLimit)
LUAU_FASTFLAG(DebugLuauFreezeArena)
std::chrono::milliseconds kInterruptTimeout(10);
std::chrono::time_point<std::chrono::system_clock> interruptDeadline;
@ -135,10 +137,58 @@ int registerTypes(Luau::TypeChecker& env)
return 0;
}
struct FuzzFileResolver : Luau::FileResolver
{
std::optional<Luau::SourceCode> readSource(const Luau::ModuleName& name) override
{
auto it = source.find(name);
if (it == source.end())
return std::nullopt;
static std::string debugsource;
return Luau::SourceCode{it->second, Luau::SourceCode::Module};
}
DEFINE_PROTO_FUZZER(const luau::StatBlock& message)
std::optional<Luau::ModuleInfo> resolveModule(const Luau::ModuleInfo* context, Luau::AstExpr* expr) override
{
if (Luau::AstExprGlobal* g = expr->as<Luau::AstExprGlobal>())
return Luau::ModuleInfo{g->name.value};
return std::nullopt;
}
std::string getHumanReadableModuleName(const Luau::ModuleName& name) const override
{
return name;
}
std::optional<std::string> getEnvironmentForModule(const Luau::ModuleName& name) const override
{
return std::nullopt;
}
std::unordered_map<Luau::ModuleName, std::string> source;
};
struct FuzzConfigResolver : Luau::ConfigResolver
{
FuzzConfigResolver()
{
defaultConfig.mode = Luau::Mode::Nonstrict; // typecheckTwice option will cover Strict mode
defaultConfig.enabledLint.warningMask = ~0ull;
defaultConfig.parseOptions.captureComments = true;
}
virtual const Luau::Config& getConfig(const Luau::ModuleName& name) const override
{
return defaultConfig;
}
Luau::Config defaultConfig;
};
static std::vector<std::string> debugsources;
DEFINE_PROTO_FUZZER(const luau::ModuleSet& message)
{
FInt::LuauTypeInferRecursionLimit.value = 100;
FInt::LuauTypeInferTypePackLoopLimit.value = 100;
@ -151,91 +201,90 @@ DEFINE_PROTO_FUZZER(const luau::StatBlock& message)
if (strncmp(flag->name, "Luau", 4) == 0)
flag->value = true;
Luau::Allocator allocator;
Luau::AstNameTable names(allocator);
FFlag::DebugLuauFreezeArena.value = true;
std::string source = protoprint(message, kFuzzTypes);
std::vector<std::string> sources = protoprint(message, kFuzzTypes);
// stash source in a global for easier crash dump debugging
debugsource = source;
Luau::ParseResult parseResult = Luau::Parser::parse(source.c_str(), source.size(), names, allocator);
// "static" here is to accelerate fuzzing process by only creating and populating the type environment once
static Luau::NullModuleResolver moduleResolver;
static Luau::InternalErrorReporter iceHandler;
static Luau::TypeChecker sharedEnv(&moduleResolver, &iceHandler);
static int once = registerTypes(sharedEnv);
(void)once;
static int once2 = (Luau::freeze(sharedEnv.globalTypes), 0);
(void)once2;
iceHandler.onInternalError = [](const char* error) {
printf("ICE: %s\n", error);
LUAU_ASSERT(!"ICE");
};
debugsources = sources;
static bool debug = getenv("LUAU_DEBUG") != 0;
if (debug)
{
fprintf(stdout, "--\n%s\n", source.c_str());
for (std::string& source : sources)
fprintf(stdout, "--\n%s\n", source.c_str());
fflush(stdout);
}
std::string bytecode;
// parse all sources
std::vector<std::unique_ptr<Luau::Allocator>> parseAllocators;
std::vector<std::unique_ptr<Luau::AstNameTable>> parseNameTables;
// compile
if (kFuzzCompiler && parseResult.errors.empty())
Luau::ParseOptions parseOptions;
parseOptions.captureComments = true;
std::vector<Luau::ParseResult> parseResults;
for (std::string& source : sources)
{
Luau::CompileOptions compileOptions;
parseAllocators.push_back(std::make_unique<Luau::Allocator>());
parseNameTables.push_back(std::make_unique<Luau::AstNameTable>(*parseAllocators.back()));
try
{
Luau::BytecodeBuilder bcb;
Luau::compileOrThrow(bcb, parseResult.root, names, compileOptions);
bytecode = bcb.getBytecode();
}
catch (const Luau::CompileError&)
{
// not all valid ASTs can be compiled due to limits on number of registers
}
parseResults.push_back(Luau::Parser::parse(source.c_str(), source.size(), *parseNameTables.back(), *parseAllocators.back(), parseOptions));
}
// typecheck
if (kFuzzTypeck && parseResult.root)
{
Luau::SourceModule sourceModule;
sourceModule.root = parseResult.root;
sourceModule.mode = Luau::Mode::Nonstrict;
Luau::TypeChecker typeck(&moduleResolver, &iceHandler);
typeck.globalScope = sharedEnv.globalScope;
Luau::ModulePtr module = nullptr;
try
{
module = typeck.check(sourceModule, Luau::Mode::Nonstrict);
}
catch (std::exception&)
{
// This catches internal errors that the type checker currently (unfortunately) throws in some cases
}
// lint (note that we need access to types so we need to do this with typeck in scope)
if (kFuzzLinter)
{
Luau::LintOptions lintOptions = {~0u};
Luau::lint(parseResult.root, names, sharedEnv.globalScope, module.get(), {}, lintOptions);
}
}
// validate sharedEnv post-typecheck; valuable for debugging some typeck crashes but slows fuzzing down
// note: it's important for typeck to be destroyed at this point!
// typecheck all sources
if (kFuzzTypeck)
{
for (auto& p : sharedEnv.globalScope->bindings)
static FuzzFileResolver fileResolver;
static Luau::NullConfigResolver configResolver;
static Luau::FrontendOptions options{true, true};
static Luau::Frontend frontend(&fileResolver, &configResolver, options);
static int once = registerTypes(frontend.typeChecker);
(void)once;
static int once2 = (Luau::freeze(frontend.typeChecker.globalTypes), 0);
(void)once2;
frontend.iceHandler.onInternalError = [](const char* error) {
printf("ICE: %s\n", error);
LUAU_ASSERT(!"ICE");
};
// restart
frontend.clear();
fileResolver.source.clear();
// load sources
for (size_t i = 0; i < sources.size(); i++)
{
std::string name = "module" + std::to_string(i);
fileResolver.source[name] = sources[i];
}
// check sources
for (size_t i = 0; i < sources.size(); i++)
{
std::string name = "module" + std::to_string(i);
try
{
Luau::CheckResult result = frontend.check(name, std::nullopt);
// lint (note that we need access to types so we need to do this with typeck in scope)
if (kFuzzLinter && result.errors.empty())
frontend.lint(name, std::nullopt);
}
catch (std::exception&)
{
// This catches internal errors that the type checker currently (unfortunately) throws in some cases
}
}
// validate sharedEnv post-typecheck; valuable for debugging some typeck crashes but slows fuzzing down
// note: it's important for typeck to be destroyed at this point!
for (auto& p : frontend.typeChecker.globalScope->bindings)
{
Luau::ToStringOptions opts;
opts.exhaustive = true;
@ -246,12 +295,44 @@ DEFINE_PROTO_FUZZER(const luau::StatBlock& message)
}
}
if (kFuzzTranspile && parseResult.root)
if (kFuzzTranspile)
{
transpileWithTypes(*parseResult.root);
for (Luau::ParseResult& parseResult : parseResults)
{
if (parseResult.root)
transpileWithTypes(*parseResult.root);
}
}
// run resulting bytecode
std::string bytecode;
// compile
if (kFuzzCompiler)
{
for (size_t i = 0; i < parseResults.size(); i++)
{
Luau::ParseResult& parseResult = parseResults[i];
Luau::AstNameTable& parseNameTable = *parseNameTables[i];
if (parseResult.errors.empty())
{
Luau::CompileOptions compileOptions;
try
{
Luau::BytecodeBuilder bcb;
Luau::compileOrThrow(bcb, parseResult.root, parseNameTable, compileOptions);
bytecode = bcb.getBytecode();
}
catch (const Luau::CompileError&)
{
// not all valid ASTs can be compiled due to limits on number of registers
}
}
}
}
// run resulting bytecode (from last successfully compiler module)
if (kFuzzVM && bytecode.size())
{
static lua_State* globalState = createGlobalState();

View file

@ -208,6 +208,35 @@ struct ProtoToLuau
source += std::to_string(name.index() & 0xff);
}
template<typename T>
void genericidents(const T& node)
{
if (node.generics_size() || node.genericpacks_size())
{
source += '<';
bool first = true;
for (size_t i = 0; i < node.generics_size(); ++i)
{
if (!first)
source += ',';
first = false;
ident(node.generics(i));
}
for (size_t i = 0; i < node.genericpacks_size(); ++i)
{
if (!first)
source += ',';
first = false;
ident(node.genericpacks(i));
source += "...";
}
source += '>';
}
}
void print(const luau::Expr& expr)
{
if (expr.has_group())
@ -240,6 +269,8 @@ struct ProtoToLuau
print(expr.unary());
else if (expr.has_binary())
print(expr.binary());
else if (expr.has_ifelse())
print(expr.ifelse());
else
source += "_";
}
@ -350,6 +381,7 @@ struct ProtoToLuau
void function(const luau::ExprFunction& expr)
{
genericidents(expr);
source += "(";
for (int i = 0; i < expr.args_size(); ++i)
{
@ -478,12 +510,21 @@ struct ProtoToLuau
void print(const luau::ExprIfElse& expr)
{
source += " if ";
source += "if ";
print(expr.cond());
source += " then ";
print(expr.then());
source += " else ";
print(expr.else_());
if (expr.has_else_())
{
source += " else ";
print(expr.else_());
}
else if (expr.has_elseif())
{
source += " else";
print(expr.elseif());
}
}
void print(const luau::LValue& expr)
@ -534,6 +575,8 @@ struct ProtoToLuau
print(stat.local_function());
else if (stat.has_type_alias())
print(stat.type_alias());
else if (stat.has_require_into_local())
print(stat.require_into_local());
else
source += "do end\n";
}
@ -804,26 +847,24 @@ struct ProtoToLuau
void print(const luau::StatTypeAlias& stat)
{
if (stat.export_())
source += "export ";
source += "type ";
ident(stat.name());
if (stat.generics_size())
{
source += '<';
for (size_t i = 0; i < stat.generics_size(); ++i)
{
if (i != 0)
source += ',';
ident(stat.generics(i));
}
source += '>';
}
genericidents(stat);
source += " = ";
print(stat.type());
source += '\n';
}
void print(const luau::StatRequireIntoLocalHelper& stat)
{
source += "local ";
print(stat.var());
source += " = require(module" + std::to_string(stat.modulenum() % 2) + ")\n";
}
void print(const luau::Type& type)
{
if (type.has_primitive())
@ -844,6 +885,10 @@ struct ProtoToLuau
print(type.class_());
else if (type.has_ref())
print(type.ref());
else if (type.has_boolean())
print(type.boolean());
else if (type.has_string())
print(type.string());
else
source += "any";
}
@ -858,15 +903,28 @@ struct ProtoToLuau
{
ident(type.name());
if (type.generics_size())
if (type.generics_size() || type.genericpacks_size())
{
source += '<';
bool first = true;
for (size_t i = 0; i < type.generics_size(); ++i)
{
if (i != 0)
if (!first)
source += ',';
ident(type.generics(i));
first = false;
print(type.generics(i));
}
for (size_t i = 0; i < type.genericpacks_size(); ++i)
{
if (!first)
source += ',';
first = false;
ident(type.genericpacks(i));
source += "...";
}
source += '>';
}
}
@ -893,6 +951,7 @@ struct ProtoToLuau
void print(const luau::TypeFunction& type)
{
genericidents(type);
source += '(';
for (size_t i = 0; i < type.args_size(); ++i)
{
@ -950,12 +1009,38 @@ struct ProtoToLuau
source += '.';
ident(type.index());
}
void print(const luau::TypeBoolean& type)
{
source += type.val() ? "true" : "false";
}
void print(const luau::TypeString& type)
{
source += '"';
for (char ch : type.val())
if (isgraph(ch))
source += ch;
source += '"';
}
};
std::string protoprint(const luau::StatBlock& stat, bool types)
std::vector<std::string> protoprint(const luau::ModuleSet& stat, bool types)
{
std::vector<std::string> result;
if (stat.has_module())
{
ProtoToLuau printer;
printer.types = types;
printer.print(stat.module());
result.push_back(printer.source);
}
ProtoToLuau printer;
printer.types = types;
printer.print(stat);
return printer.source;
printer.print(stat.program());
result.push_back(printer.source);
return result;
}

View file

@ -2,11 +2,15 @@
#include "src/libfuzzer/libfuzzer_macro.h"
#include "luau.pb.h"
std::string protoprint(const luau::StatBlock& stat, bool types);
std::vector<std::string> protoprint(const luau::ModuleSet& stat, bool types);
DEFINE_PROTO_FUZZER(const luau::StatBlock& message)
DEFINE_PROTO_FUZZER(const luau::ModuleSet& message)
{
std::string source = protoprint(message, true);
std::vector<std::string> sources = protoprint(message, true);
printf("%s\n", source.c_str());
for (size_t i = 0; i < sources.size(); i++)
{
printf("Module 'l%d':\n", int(i));
printf("%s\n", sources[i].c_str());
}
}

View file

@ -1,9 +1,11 @@
// This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details
#include <string>
#include "Luau/TypeInfer.h"
#include "Luau/BuiltinDefinitions.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Common.h"
#include "Luau/ModuleResolver.h"
#include "Luau/Parser.h"
#include "Luau/TypeInfer.h"
LUAU_FASTINT(LuauTypeInferRecursionLimit)
LUAU_FASTINT(LuauTypeInferTypePackLoopLimit)

View file

@ -2,10 +2,8 @@
*.agdai
Main
MAlonzo
Examples
PrettyPrinter
Interpreter
Properties
!Tests/Interpreter
!Tests/PrettyPrinter
.ghc.*

View file

@ -0,0 +1,8 @@
{-# OPTIONS --rewriting #-}
module Everything where
import Examples
import Properties
import PrettyPrinter
import Interpreter

View file

@ -1,8 +1,10 @@
{-# OPTIONS --rewriting #-}
module Examples.OpSem where
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end)
open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)
open import Luau.Heap using ()
ex1 : (local (var "x") nil return (var "x") done) ⟶ᴮ (return nil done)
ex1 = subst
ex1 : (local (var "x") val nil return (var "x") done) ⟶ᴮ (return (val nil) done)
ex1 = subst nil

View file

@ -4,25 +4,20 @@ module Examples.Run where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Bool using (true; false)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; true; false; ≅; string)
open import Luau.Value using (nil; number; bool)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool; ~=; string)
open import Luau.Run using (run; return)
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
import Agda.Builtin.Equality.Rewrite
{-# REWRITE lookup-next next-emp lookup-next-emp #-}
ex1 : (run (function "id" var "x" is return (var "x") done end return (var "id" $ nil) done) return nil _)
ex1 : (run (function "id" var "x" is return (var "x") done end return (var "id" $ val nil) done) return nil _)
ex1 = refl
ex2 : (run (function "fn" var "x" is return (number 123.0) done end return (var "fn" $ nil) done) return (number 123.0) _)
ex2 : (run (function "fn" var "x" is return (val (number 123.0)) done end return (var "fn" $ val nil) done) return (number 123.0) _)
ex2 = refl
ex3 : (run (function "fn" var "x" is return (binexp (number 1.0) + (number 2.0)) done end return (var "fn" $ nil) done) return (number 3.0) _)
ex3 : (run (function "fn" var "x" is return (binexp (val (number 1.0)) + (val (number 2.0))) done end return (var "fn" $ val nil) done) return (number 3.0) _)
ex3 = refl
ex4 : (run (function "fn" var "x" is return (binexp (number 1.0) < (number 2.0)) done end return (var "fn" $ nil) done) return (bool true) _)
ex4 : (run (function "fn" var "x" is return (binexp (val (number 1.0)) < (val (number 2.0))) done end return (var "fn" $ val nil) done) return (bool true) _)
ex4 = refl
ex5 : (run (function "fn" var "x" is return (binexp (string "foo") (string "bar")) done end return (var "fn" $ nil) done) return (bool true) _)
ex5 : (run (function "fn" var "x" is return (binexp (val (string "foo")) ~= (val (string "bar"))) done end return (var "fn" $ val nil) done) return (bool true) _)
ex5 = refl

View file

@ -2,7 +2,7 @@ module Examples.Syntax where
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.String using (_++_)
open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
open import Luau.Syntax using (var; _$_; return; val; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
open import Luau.Syntax.ToString using (exprToString; blockToString)
ex1 : exprToString(function "" var "x" is return (var "f" $ var "x") done end)
@ -11,7 +11,7 @@ ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙
"end"
ex1 = refl
ex2 : blockToString(local var "x" nil return (var "x") done)
ex2 : blockToString(local var "x" (val nil) return (var "x") done)
"local x = nil\n" ++
"return x"
ex2 = refl

View file

@ -25,3 +25,4 @@ ex6 = refl
ex7 : typeToString((nil nil) ((nil (nil nil)) nil)) "((nil) -> nil | (nil) -> (nil) -> nil)?"
ex7 = refl

View file

@ -1,15 +1,21 @@
{-# OPTIONS --rewriting #-}
module FFI.Data.Aeson where
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Equality.Rewrite using ()
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.String using (String)
open import FFI.Data.ByteString using (ByteString)
open import FFI.Data.HaskellString using (HaskellString; pack)
open import FFI.Data.Maybe using (Maybe)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Either using (Either; mapLeft)
open import FFI.Data.Scientific using (Scientific)
open import FFI.Data.Vector using (Vector)
open import Properties.Equality using (_≢_)
{-# FOREIGN GHC import qualified Data.Aeson #-}
{-# FOREIGN GHC import qualified Data.Aeson.Key #-}
{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}
@ -19,14 +25,35 @@ postulate
Key : Set
fromString : String Key
toString : Key String
empty : {A} KeyMap A
singleton : {A} Key A (KeyMap A)
insert : {A} Key A (KeyMap A) (KeyMap A)
delete : {A} Key (KeyMap A) (KeyMap A)
unionWith : {A} (A A A) (KeyMap A) (KeyMap A) (KeyMap A)
lookup : {A} Key -> KeyMap A -> Maybe A
{-# POLARITY KeyMap ++ #-}
{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
{-# COMPILE GHC empty = \_ -> Data.Aeson.KeyMap.empty #-}
{-# COMPILE GHC singleton = \_ -> Data.Aeson.KeyMap.singleton #-}
{-# COMPILE GHC insert = \_ -> Data.Aeson.KeyMap.insert #-}
{-# COMPILE GHC delete = \_ -> Data.Aeson.KeyMap.delete #-}
{-# COMPILE GHC unionWith = \_ -> Data.Aeson.KeyMap.unionWith #-}
{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}
postulate lookup-insert : {A} k v (m : KeyMap A) (lookup k (insert k v m) just v)
postulate lookup-empty : {A} k (lookup {A} k empty nothing)
postulate lookup-insert-not : {A} j k v (m : KeyMap A) (j k) (lookup k m lookup k (insert j v m))
postulate singleton-insert-empty : {A} k (v : A) (singleton k v insert k v empty)
postulate insert-swap : {A} j k (v w : A) m (j k) insert j v (insert k w m) insert k w (insert j v m)
postulate insert-over : {A} j k (v w : A) m (j k) insert j v (insert k w m) insert j v m
postulate to-from : k toString(fromString k) k
postulate from-to : k fromString(toString k) k
{-# REWRITE lookup-insert lookup-empty singleton-insert-empty #-}
data Value : Set where
object : KeyMap Value Value
array : Vector Value Value

View file

@ -1,8 +1,14 @@
module FFI.Data.Maybe where
open import Agda.Builtin.Equality using (_≡_; refl)
{-# FOREIGN GHC import qualified Data.Maybe #-}
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A Maybe A
{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}
just-inv : {A} {x y : A} (just x just y) (x y)
just-inv refl = refl

View file

@ -1,11 +1,15 @@
{-# OPTIONS --rewriting #-}
module FFI.Data.Vector where
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Equality.Rewrite using ()
open import Agda.Builtin.Int using (Int; pos; negsuc)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Bool using (Bool; false; true)
open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Equality using (_≢_)
{-# FOREIGN GHC import qualified Data.Vector #-}
@ -30,8 +34,13 @@ postulate
{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}
postulate length-empty : {A} (length (empty {A}) 0)
postulate lookup-empty : {A} n (lookup (empty {A}) n nothing)
postulate lookup-snoc : {A} (x : A) (v : Vector A) (lookup (snoc v x) (length v) just x)
postulate lookup-length : {A} (v : Vector A) (lookup v (length v) nothing)
postulate lookup-snoc-empty : {A} (x : A) (lookup (snoc empty x) 0 just x)
postulate lookup-snoc-not : {A n} (x : A) (v : Vector A) (n length v) (lookup v n lookup (snoc v x) n)
{-# REWRITE length-empty lookup-snoc lookup-length lookup-snoc-empty lookup-empty #-}
head : {A} (Vector A) (Maybe A)
head vec with null vec

View file

@ -1,3 +1,5 @@
{-# OPTIONS --rewriting #-}
module Interpreter where
open import Agda.Builtin.IO using (IO)
@ -7,31 +9,41 @@ open import Agda.Builtin.Unit using ()
open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
open import FFI.Data.Aeson using (Value; eitherDecode)
open import FFI.Data.Either using (Left; Right)
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Text.Encoding using (encodeUtf8)
open import FFI.System.Exit using (exitWith; ExitFailure)
open import Luau.Syntax using (Block)
open import Luau.StrictMode.ToString using (warningToStringᴮ)
open import Luau.Syntax using (Block; yes; maybe; isAnnotatedᴮ)
open import Luau.Syntax.FromJSON using (blockFromJSON)
open import Luau.Syntax.ToString using (blockToString)
open import Luau.Syntax.ToString using (blockToString; valueToString)
open import Luau.Run using (run; return; done; error)
open import Luau.RuntimeError.ToString using (errToStringᴮ)
open import Luau.Value.ToString using (valueToString)
runBlock : {a} Block a IO
runBlock block with run block
runBlock block | return V D = putStrLn (valueToString V)
runBlock block | done D = putStrLn "nil"
runBlock block | error E D = putStrLn (errToStringᴮ E)
open import Properties.StrictMode using (wellTypedProgramsDontGoWrong)
runBlock : a Block a IO
runBlock a block with run block
runBlock a block | return V D = putStrLn ("\nRAN WITH RESULT: " ++ valueToString V)
runBlock a block | done D = putStrLn ("\nRAN")
runBlock maybe block | error E D = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E)
runBlock yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
runBlock yes block | error E D | W = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E ++ "\n\nTYPE ERROR:\n" ++ warningToStringᴮ _ W)
runBlock : Block maybe IO
runBlock B with isAnnotatedᴮ B
runBlock B | nothing = putStrLn ("UNANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock maybe B
runBlock B | just B = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock yes B
runJSON : Value IO
runJSON value with blockFromJSON(value)
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Left err) = putStrLn ("LUAU ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Right block) = runBlock block
runString : String IO
runString txt with eitherDecode (encodeUtf8 txt)
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Left err) = putStrLn ("JSON ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Right value) = runJSON value
main : IO

View file

@ -5,13 +5,14 @@ open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Nat using (Nat; _==_)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.TrustMe using (primTrustMe)
open import Properties.Dec using (Dec; yes; no; )
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (_≢_)
Addr : Set
Addr = Nat
_≡ᴬ_ : (a b : Addr) Dec (a b)
a ≡ᴬ b with a == b
a ≡ᴬ b | false = no p where postulate p : (a b)
a ≡ᴬ b | false = no p where postulate p : (a b)
a ≡ᴬ b | true = yes primTrustMe

View file

@ -1,32 +1,39 @@
{-# OPTIONS --rewriting #-}
module Luau.Heap where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import FFI.Data.Vector using (Vector; length; snoc; empty)
open import Luau.Addr using (Addr)
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Vector using (Vector; length; snoc; empty; lookup-snoc-not)
open import Luau.Addr using (Addr; _≡ᴬ_)
open import Luau.Var using (Var)
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end)
open import Properties.Equality using (_≢_; trans)
open import Properties.Remember using (remember; _,_)
open import Properties.Dec using (yes; no)
data HeapValue (a : Annotated) : Set where
function_is_end : FunDec a Block a HeapValue a
-- Heap-allocated objects
data Object (a : Annotated) : Set where
function_is_end : FunDec a Block a Object a
Heap : Annotated Set
Heap a = Vector (HeapValue a)
Heap a = Vector (Object a)
data _≡_⊕_↦_ {a} : Heap a Heap a Addr HeapValue a Set where
data _≡_⊕_↦_ {a} : Heap a Heap a Addr Object a Set where
defn : {H val}
-----------------------------------
(snoc H val) H (length H) val
_[_] : {a} Heap a Addr Maybe (HeapValue a)
_[_] : {a} Heap a Addr Maybe (Object a)
_[_] = FFI.Data.Vector.lookup
: {a} Heap a
= empty
data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
data AllocResult a (H : Heap a) (V : Object a) : Set where
ok : b H (H H b V) AllocResult a H V
alloc : {a} H V AllocResult a H V
@ -35,15 +42,8 @@ alloc H V = ok (length H) (snoc H V) defn
next : {a} Heap a Addr
next = length
allocated : {a} Heap a HeapValue a Heap a
allocated : {a} Heap a Object a Heap a
allocated = snoc
-- next-emp : (length ∅ ≡ 0)
next-emp = FFI.Data.Vector.length-empty
-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
lookup-next = FFI.Data.Vector.lookup-snoc
-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty
lookup-not-allocated : {a} {H H : Heap a} {b c O} (H H b O) (c b) (H [ c ] H [ c ])
lookup-not-allocated {H = H} {O = O} defn p = lookup-snoc-not O H p

View file

@ -1,3 +1,5 @@
{-# OPTIONS --rewriting #-}
module Luau.OpSem where
open import Agda.Builtin.Equality using (_≡_)
@ -5,66 +7,48 @@ open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; prim
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.String using (primStringEquality)
open import Utility.Bool using (not; _or_; _and_)
open import Agda.Builtin.Nat using (_==_)
open import FFI.Data.Maybe using (just)
open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; number)
open import Luau.Value using (addr; val; number; Value; bool; string)
open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; number; bool)
open import Luau.RuntimeType using (RuntimeType; valueType)
open import Properties.Product using (_×_; _,_)
evalNumOp : Float BinaryOperator Float Value
evalNumOp x + y = number (primFloatPlus x y)
evalNumOp x - y = number (primFloatMinus x y)
evalNumOp x * y = number (primFloatTimes x y)
evalNumOp x / y = number (primFloatDiv x y)
evalNumOp x < y = bool (primFloatLess x y)
evalNumOp x > y = bool (primFloatLess y x)
evalNumOp x y = bool (primFloatEquality x y)
evalNumOp x y = bool (primFloatInequality x y)
evalNumOp x y = bool ((primFloatLess x y) or (primFloatEquality x y))
evalNumOp x y = bool ((primFloatLess y x) or (primFloatEquality x y))
evalEqOp : Value Value Bool
evalEqOp Value.nil Value.nil = true
evalEqOp (addr x) (addr y) = (x == y)
evalEqOp (number x) (number y) = primFloatEquality x y
evalEqOp (bool true) (bool y) = y
evalEqOp (bool false) (bool y) = not y
evalEqOp _ _ = false
evalEqOp : Value Value Value
evalEqOp Value.nil Value.nil = bool true
evalEqOp (addr x) (addr y) = bool (x == y)
evalEqOp (number x) (number y) = bool (primFloatEquality x y)
evalEqOp (bool true) (bool y) = bool y
evalEqOp (bool false) (bool y) = bool (not y)
evalEqOp (string x) (string y) = bool (primStringEquality x y)
evalEqOp _ _ = bool false
evalNeqOp : Value Value Bool
evalNeqOp (number x) (number y) = primFloatInequality x y
evalNeqOp x y = not (evalEqOp x y)
evalNeqOp : Value Value Value
evalNeqOp Value.nil Value.nil = bool false
evalNeqOp (addr x) (addr y) = bool (not (x == y))
evalNeqOp (number x) (number y) = bool (primFloatInequality x y)
evalNeqOp (bool true) (bool y) = bool (not y)
evalNeqOp (bool false) (bool y) = bool y
evalNeqOp (string x) (string y) = bool (not (primStringEquality x y))
evalNeqOp _ _ = bool true
coerceToBool : Value Bool
coerceToBool Value.nil = false
coerceToBool (addr x) = true
coerceToBool (number x) = true
coerceToBool (bool x) = x
coerceToBool (string x) = true
data _⟦_⟧_⟶_ : Value BinaryOperator Value Value Set where
+ : m n (number m) + (number n) number (primFloatPlus m n)
- : m n (number m) - (number n) number (primFloatMinus m n)
/ : m n (number m) / (number n) number (primFloatTimes m n)
* : m n (number m) * (number n) number (primFloatDiv m n)
< : m n (number m) < (number n) bool (primFloatLess m n)
> : m n (number m) > (number n) bool (primFloatLess n m)
<= : m n (number m) <= (number n) bool ((primFloatLess m n) or (primFloatEquality m n))
>= : m n (number m) >= (number n) bool ((primFloatLess n m) or (primFloatEquality m n))
== : v w v == w bool (evalEqOp v w)
~= : v w v ~= w bool (evalNeqOp v w)
data _⊢_⟶ᴮ_⊣_ {a} : Heap a Block a Block a Heap a Set
data _⊢_⟶ᴱ_⊣_ {a} : Heap a Expr a Expr a Heap a Set
data _⊢_⟶ᴱ_⊣_ where
nil : {H}
-------------------
H nil ⟶ᴱ nil H
function : {H H a F B}
function : a {H H F B}
H H a (function F is B end)
-------------------------------------------
H (function F is B end) ⟶ᴱ (addr a) H
H (function F is B end) ⟶ᴱ val(addr a) H
app₁ : {H H M M N}
@ -72,17 +56,18 @@ data _⊢_⟶ᴱ_⊣_ where
-----------------------------
H (M $ N) ⟶ᴱ (M $ N) H
app₂ : {H H V N N}
app₂ : v {H H N N}
H N ⟶ᴱ N H
-----------------------------
H (val V $ N) ⟶ᴱ (val V $ N) H
H (val v $ N) ⟶ᴱ (val v $ N) H
beta : {H a F B V}
H [ a ] just(function F is B end)
beta : O v {H a F B}
(O function F is B end)
H [ a ] just(O)
-----------------------------------------------------------------------------
H (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) H
H (val (addr a) $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) H
block : {H H B B b}
@ -90,44 +75,34 @@ data _⊢_⟶ᴱ_⊣_ where
----------------------------------------------------
H (block b is B end) ⟶ᴱ (block b is B end) H
return : {H V B b}
return : v {H B b}
--------------------------------------------------------
H (block b is return (val V) B end) ⟶ᴱ (val V) H
H (block b is return (val v) B end) ⟶ᴱ val v H
done : {H b}
---------------------------------
H (block b is done end) ⟶ᴱ nil H
--------------------------------------------
H (block b is done end) ⟶ᴱ (val nil) H
binOpEquality :
{H x y}
---------------------------------------------------------------------------
H (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) H
binOpInequality :
{H x y}
----------------------------------------------------------------------------
H (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) H
binOpNumbers :
{H x op y}
-----------------------------------------------------------------------
H (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) H
binOp₁ :
{H H x x op y}
binOp₀ : {H op v₁ v₂ w}
v₁ op v₂ w
--------------------------------------------------
H (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) H
binOp₁ : {H H x x op y}
H x ⟶ᴱ x H
---------------------------------------------
H (binexp x op y) ⟶ᴱ (binexp x op y) H
binOp₂ :
{H H x op y y}
binOp₂ : {H H x op y y}
H y ⟶ᴱ y H
---------------------------------------------
H (binexp x op y) ⟶ᴱ (binexp x op y) H
data _⊢_⟶ᴮ_⊣_ where
local : {H H x M M B}
@ -136,16 +111,16 @@ data _⊢_⟶ᴮ_⊣_ where
-------------------------------------------------
H (local x M B) ⟶ᴮ (local x M B) H
subst : {H x v B}
subst : v {H x B}
------------------------------------------------------
H (local x val v B) ⟶ᴮ (B [ v / name x ]ᴮ) H
function : {H H a F B C}
function : a {H H F B C}
H H a (function F is C end)
--------------------------------------------------------------
H (function F is C end B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) H
H (function F is C end B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) H
return : {H H M M B}

View file

@ -1,15 +1,16 @@
{-# OPTIONS --rewriting #-}
module Luau.Run where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Luau.Heap using (Heap; )
open import Luau.Syntax using (Block; return; _∙_; done)
open import Luau.Syntax using (Block; val; return; _∙_; done)
open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
open import Luau.Value using (val)
open import Properties.Step using (stepᴮ; step; return; done; error)
open import Luau.RuntimeError using (RuntimeErrorᴮ)
data RunResult {a} (H : Heap a) (B : Block a) : Set where
return : V {B H} (H B ⟶* (return (val V) B) H) RunResult H B
return : v {B H} (H B ⟶* (return (val v) B) H) RunResult H B
done : {H} (H B ⟶* done H) RunResult H B
error : {B H} (RuntimeErrorᴮ H B) (H B ⟶* B H) RunResult H B

View file

@ -1,27 +1,40 @@
{-# OPTIONS --rewriting #-}
module Luau.RuntimeError where
open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; _[_])
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String)
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp)
open import Luau.RuntimeType using (RuntimeType; valueType)
open import Luau.Value using (val)
open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp; +; -; *; /; <; >; <=; >=)
open import Luau.RuntimeType using (RuntimeType; valueType; function; number)
open import Properties.Equality using (_≢_)
data BinOpError : BinaryOperator RuntimeType Set where
+ : {t} (t number) BinOpError + t
- : {t} (t number) BinOpError - t
* : {t} (t number) BinOpError * t
/ : {t} (t number) BinOpError / t
< : {t} (t number) BinOpError < t
> : {t} (t number) BinOpError > t
<= : {t} (t number) BinOpError <= t
>= : {t} (t number) BinOpError >= t
data RuntimeErrorᴮ {a} (H : Heap a) : Block a Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a Set
data RuntimeErrorᴱ H where
TypeMismatch : t v (t valueType v) RuntimeErrorᴱ H (val v)
UnboundVariable : x RuntimeErrorᴱ H (var x)
SEGV : a (H [ a ] nothing) RuntimeErrorᴱ H (addr a)
FunctionMismatch : v w (function valueType v) RuntimeErrorᴱ H (val v $ val w)
BinOpMismatch₁ : v w {op} (BinOpError op (valueType v)) RuntimeErrorᴱ H (binexp (val v) op (val w))
BinOpMismatch₂ : v w {op} (BinOpError op (valueType w)) RuntimeErrorᴱ H (binexp (val v) op (val w))
UnboundVariable : {x} RuntimeErrorᴱ H (var x)
SEGV : {a} (H [ a ] nothing) RuntimeErrorᴱ H (val (addr a))
app₁ : {M N} RuntimeErrorᴱ H M RuntimeErrorᴱ H (M $ N)
app₂ : {M N} RuntimeErrorᴱ H N RuntimeErrorᴱ H (M $ N)
block : b {B} RuntimeErrorᴮ H B RuntimeErrorᴱ H (block b is B end)
block : {b B} RuntimeErrorᴮ H B RuntimeErrorᴱ H (block b is B end)
bin₁ : {M N op} RuntimeErrorᴱ H M RuntimeErrorᴱ H (binexp M op N)
bin₂ : {M N op} RuntimeErrorᴱ H N RuntimeErrorᴱ H (binexp M op N)
data RuntimeErrorᴮ H where
local : x {M B} RuntimeErrorᴱ H M RuntimeErrorᴮ H (local x M B)
local : {x M B} RuntimeErrorᴱ H M RuntimeErrorᴮ H (local x M B)
return : {M B} RuntimeErrorᴱ H M RuntimeErrorᴮ H (return M B)

View file

@ -1,27 +1,29 @@
{-# OPTIONS --rewriting #-}
module Luau.RuntimeError.ToString where
open import Agda.Builtin.Float using (primShowFloat)
open import FFI.Data.String using (String; _++_)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
open import Luau.RuntimeType.ToString using (runtimeTypeToString)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (exprToString)
open import Luau.Syntax.ToString using (valueToString; exprToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Value.ToString using (valueToString)
open import Luau.Syntax using (name; _$_)
open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_)
errToStringᴱ : {a H B} RuntimeErrorᴱ {a} H B String
errToStringᴮ : {a H B} RuntimeErrorᴮ {a} H B String
errToStringᴱ : {a H} M RuntimeErrorᴱ {a} H M String
errToStringᴮ : {a H} B RuntimeErrorᴮ {a} H B String
errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (app₁ E) = errToStringᴱ E
errToStringᴱ (app₂ E) = errToStringᴱ E
errToStringᴱ (bin₁ E) = errToStringᴱ E
errToStringᴱ (bin₂ E) = errToStringᴱ E
errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b
errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t
errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E
errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n in call of function " ++ varToString (name b)
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x)
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement"
errToStringᴮ (local x M B) (local E) = errToStringᴱ M E ++ "\n in definition of " ++ varToString (name x)
errToStringᴮ (return M B) (return E) = errToStringᴱ M E ++ "\n in return statement"

View file

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

View file

@ -0,0 +1,205 @@
{-# OPTIONS --rewriting #-}
module Luau.StrictMode where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=)
open import Luau.Type using (Type; strict; nil; number; _⇒_; tgt)
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
open import Properties.Equality using (_≢_)
open import Properties.TypeCheck(strict) using (typeCheckᴮ)
open import Properties.Product using (_,_)
src : Type Type
src = Luau.Type.src strict
data BinOpWarning : BinaryOperator Type Set where
+ : {T} (T number) BinOpWarning + T
- : {T} (T number) BinOpWarning - T
* : {T} (T number) BinOpWarning * T
/ : {T} (T number) BinOpWarning / T
< : {T} (T number) BinOpWarning < T
> : {T} (T number) BinOpWarning > T
<= : {T} (T number) BinOpWarning <= T
>= : {T} (T number) BinOpWarning >= T
data Warningᴱ (H : Heap yes) {Γ} : {M T} (Γ ⊢ᴱ M T) Set
data Warningᴮ (H : Heap yes) {Γ} : {B T} (Γ ⊢ᴮ B T) Set
data Warningᴱ H {Γ} where
UnallocatedAddress : {a T}
(H [ a ]ᴴ nothing)
---------------------
Warningᴱ H (addr {a} T)
UnboundVariable : {x T p}
(Γ [ x ]ⱽ nothing)
------------------------
Warningᴱ H (var {x} {T} p)
FunctionCallMismatch : {M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
(src T U)
-----------------
Warningᴱ H (app D₁ D₂)
app₁ : {M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
Warningᴱ H D₁
-----------------
Warningᴱ H (app D₁ D₂)
app₂ : {M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
Warningᴱ H D₂
-----------------
Warningᴱ H (app D₁ D₂)
BinOpMismatch₁ : {op M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
BinOpWarning op T
------------------------------
Warningᴱ H (binexp {op} D₁ D₂)
BinOpMismatch₂ : {op M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
BinOpWarning op U
------------------------------
Warningᴱ H (binexp {op} D₁ D₂)
bin₁ : {op M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
Warningᴱ H D₁
------------------------------
Warningᴱ H (binexp {op} D₁ D₂)
bin₂ : {op M N T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴱ N U}
Warningᴱ H D₂
------------------------------
Warningᴱ H (binexp {op} D₁ D₂)
FunctionDefnMismatch : {f x B T U V} {D : (Γ x T) ⊢ᴮ B V}
(U V)
-------------------------
Warningᴱ H (function {f} {U = U} D)
function₁ : {f x B T U V} {D : (Γ x T) ⊢ᴮ B V}
Warningᴮ H D
-------------------------
Warningᴱ H (function {f} {U = U} D)
BlockMismatch : {b B T U} {D : Γ ⊢ᴮ B U}
(T U)
------------------------------
Warningᴱ H (block {b} {T = T} D)
block₁ : {b B T U} {D : Γ ⊢ᴮ B U}
Warningᴮ H D
------------------------------
Warningᴱ H (block {b} {T = T} D)
data Warningᴮ H {Γ} where
return : {M B T U} {D₁ : Γ ⊢ᴱ M T} {D₂ : Γ ⊢ᴮ B U}
Warningᴱ H D₁
------------------
Warningᴮ H (return D₁ D₂)
LocalVarMismatch : {x M B T U V} {D₁ : Γ ⊢ᴱ M U} {D₂ : (Γ x T) ⊢ᴮ B V}
(T U)
--------------------
Warningᴮ H (local D₁ D₂)
local₁ : {x M B T U V} {D₁ : Γ ⊢ᴱ M U} {D₂ : (Γ x T) ⊢ᴮ B V}
Warningᴱ H D₁
--------------------
Warningᴮ H (local D₁ D₂)
local₂ : {x M B T U V} {D₁ : Γ ⊢ᴱ M U} {D₂ : (Γ x T) ⊢ᴮ B V}
Warningᴮ H D₂
--------------------
Warningᴮ H (local D₁ D₂)
FunctionDefnMismatch : {f x B C T U V W} {D₁ : (Γ x T) ⊢ᴮ C V} {D₂ : (Γ f (T U)) ⊢ᴮ B W}
(U V)
-------------------------------------
Warningᴮ H (function D₁ D₂)
function₁ : {f x B C T U V W} {D₁ : (Γ x T) ⊢ᴮ C V} {D₂ : (Γ f (T U)) ⊢ᴮ B W}
Warningᴮ H D₁
--------------------
Warningᴮ H (function D₁ D₂)
function₂ : {f x B C T U V W} {D₁ : (Γ x T) ⊢ᴮ C V} {D₂ : (Γ f (T U)) ⊢ᴮ B W}
Warningᴮ H D₂
--------------------
Warningᴮ H (function D₁ D₂)
data Warningᴼ (H : Heap yes) : {V} (⊢ᴼ V) Set where
FunctionDefnMismatch : {f x B T U V} {D : (x T) ⊢ᴮ B V}
(U V)
---------------------------------
Warningᴼ H (function {f} {U = U} D)
function₁ : {f x B T U V} {D : (x T) ⊢ᴮ B V}
Warningᴮ H D
---------------------------------
Warningᴼ H (function {f} {U = U} D)
data Warningᴴ H (D : ⊢ᴴ H) : Set where
addr : a {O}
(p : H [ a ]ᴴ O)
Warningᴼ H (D a p)
---------------
Warningᴴ H D
data Warningᴴᴱ H {Γ M T} : (Γ ⊢ᴴᴱ H M T) Set where
heap : {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M T}
Warningᴴ H D₁
-----------------
Warningᴴᴱ H (D₁ , D₂)
expr : {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M T}
Warningᴱ H D₂
---------------------
Warningᴴᴱ H (D₁ , D₂)
data Warningᴴᴮ H {Γ B T} : (Γ ⊢ᴴᴮ H B T) Set where
heap : {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B T}
Warningᴴ H D₁
-----------------
Warningᴴᴮ H (D₁ , D₂)
block : {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B T}
Warningᴮ H D₂
---------------------
Warningᴴᴮ H (D₁ , D₂)

View file

@ -0,0 +1,39 @@
{-# OPTIONS --rewriting #-}
module Luau.StrictMode.ToString where
open import FFI.Data.String using (String; _++_)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
open import Luau.Type using (strict)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Type.ToString using (typeToString)
open import Luau.Syntax.ToString using (binOpToString)
warningToStringᴱ : {H Γ T} M {D : Γ ⊢ᴱ M T} Warningᴱ H D String
warningToStringᴮ : {H Γ T} B {D : Γ ⊢ᴮ B T} Warningᴮ H D String
warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a
warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U
warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
warningToStringᴱ (function f var x T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
warningToStringᴱ (function f var x T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n in function expression " ++ varToString f
warningToStringᴱ block var b T is B end (BlockMismatch {U = U} p) = "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U
warningToStringᴱ block var b T is B end (block₁ W) = warningToStringᴮ B W ++ "\n in block " ++ varToString b
warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T
warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U
warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W
warningToStringᴮ (function f var x T ⟩∈ U is C end B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
warningToStringᴮ (function f var x T ⟩∈ U is C end B) (function₁ W) = warningToStringᴮ C W ++ "\n in function declaration " ++ varToString f
warningToStringᴮ (function f var x T ⟩∈ U is C end B) (function₂ W) = warningToStringᴮ B W
warningToStringᴮ (local var x T M B) (LocalVarMismatch {U = U} p) = "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U
warningToStringᴮ (local var x T M B) (local₁ W) = warningToStringᴱ M W ++ "\n in local variable declaration " ++ varToString x
warningToStringᴮ (local var x T M B) (local₂ W) = warningToStringᴮ B W
warningToStringᴮ (return M B) (return W) = warningToStringᴱ M W ++ "\n in return statement"

View file

@ -1,7 +1,6 @@
module Luau.Substitution where
open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp; string)
open import Luau.Value using (Value; val)
open import Luau.Syntax using (Value; Expr; Stat; Block; val; nil; bool; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
open import Luau.Var using (Var; _≡ⱽ_)
open import Properties.Dec using (Dec; yes; no)
@ -10,19 +9,14 @@ _[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
var_[_/_]ᴱwhenever_ : {a P} Var Value Var (Dec P) Expr a
_[_/_]ᴮunless_ : {a P} Block a Value Var (Dec P) Block a
nil [ v / x ]ᴱ = nil
true [ v / x ]ᴱ = true
false [ v / x ]ᴱ = false
val w [ v / x ]ᴱ = val w
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
addr a [ v / x ]ᴱ = addr a
(number y) [ v / x ]ᴱ = number y
(string y) [ v / x ]ᴱ = string y
(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)
(function F is C end B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
(function F is C end B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end (B [ v / x ]ᴮunless (x ≡ⱽ name(fun F)))
(local y M B) [ v / x ]ᴮ = local y (M [ v / x ]ᴱ) (B [ v / x ]ᴮunless (x ≡ⱽ name y))
(return M B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) (B [ v / x ]ᴮ)
done [ v / x ]ᴮ = done

View file

@ -1,12 +1,13 @@
module Luau.Syntax where
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Float using (Float)
open import Agda.Builtin.String using (String)
open import Properties.Dec using ()
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Type using (Type)
open import FFI.Data.Maybe using (Maybe; just; nothing)
infixr 5 _∙_
@ -26,9 +27,9 @@ data FunDec : Annotated → Set where
_⟨_⟩∈_ : {a} Var VarDec a Type FunDec a
_⟨_⟩ : Var VarDec maybe FunDec maybe
fun : {a} FunDec a Var
fun (f x ⟩∈ T) = f
fun (f x ) = f
fun : {a} FunDec a VarDec a
fun (f x ⟩∈ T) = (var f T)
fun (f x ) = (var f)
arg : {a} FunDec a VarDec a
arg (f x ⟩∈ T) = x
@ -41,10 +42,17 @@ data BinaryOperator : Set where
/ : BinaryOperator
< : BinaryOperator
> : BinaryOperator
: BinaryOperator
: BinaryOperator
: BinaryOperator
: BinaryOperator
== : BinaryOperator
~= : BinaryOperator
<= : BinaryOperator
>= : BinaryOperator
data Value : Set where
nil : Value
addr : Addr Value
number : Float Value
bool : Bool Value
string : String Value
data Block (a : Annotated) : Set
data Stat (a : Annotated) : Set
@ -60,14 +68,42 @@ data Stat a where
return : Expr a Stat a
data Expr a where
nil : Expr a
true : Expr a
false : Expr a
var : Var Expr a
addr : Addr Expr a
val : Value Expr a
_$_ : Expr a Expr a Expr a
function_is_end : FunDec a Block a Expr a
block_is_end : Var Block a Expr a
number : Float Expr a
block_is_end : VarDec a Block a Expr a
binexp : Expr a BinaryOperator Expr a Expr a
string : String Expr a
isAnnotatedᴱ : {a} Expr a Maybe (Expr yes)
isAnnotatedᴮ : {a} Block a Maybe (Block yes)
isAnnotatedᴱ (var x) = just (var x)
isAnnotatedᴱ (val v) = just (val v)
isAnnotatedᴱ (M $ N) with isAnnotatedᴱ M | isAnnotatedᴱ N
isAnnotatedᴱ (M $ N) | just M | just N = just (M $ N)
isAnnotatedᴱ (M $ N) | _ | _ = nothing
isAnnotatedᴱ (function f var x T ⟩∈ U is B end) with isAnnotatedᴮ B
isAnnotatedᴱ (function f var x T ⟩∈ U is B end) | just B = just (function f var x T ⟩∈ U is B end)
isAnnotatedᴱ (function f var x T ⟩∈ U is B end) | _ = nothing
isAnnotatedᴱ (function _ is B end) = nothing
isAnnotatedᴱ (block var b T is B end) with isAnnotatedᴮ B
isAnnotatedᴱ (block var b T is B end) | just B = just (block var b T is B end)
isAnnotatedᴱ (block var b T is B end) | _ = nothing
isAnnotatedᴱ (block _ is B end) = nothing
isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N
isAnnotatedᴱ (binexp M op N) | just M | just N = just (binexp M op N)
isAnnotatedᴱ (binexp M op N) | _ | _ = nothing
isAnnotatedᴮ (function f var x T ⟩∈ U is C end B) with isAnnotatedᴮ B | isAnnotatedᴮ C
isAnnotatedᴮ (function f var x T ⟩∈ U is C end B) | just B | just C = just (function f var x T ⟩∈ U is C end B)
isAnnotatedᴮ (function f var x T ⟩∈ U is C end B) | _ | _ = nothing
isAnnotatedᴮ (function _ is C end B) = nothing
isAnnotatedᴮ (local var x T M B) with isAnnotatedᴱ M | isAnnotatedᴮ B
isAnnotatedᴮ (local var x T M B) | just M | just B = just (local var x T M B)
isAnnotatedᴮ (local var x T M B) | _ | _ = nothing
isAnnotatedᴮ (local _ M B) = nothing
isAnnotatedᴮ (return M B) with isAnnotatedᴱ M | isAnnotatedᴮ B
isAnnotatedᴮ (return M B) | just M | just B = just (return M B)
isAnnotatedᴮ (return M B) | _ | _ = nothing
isAnnotatedᴮ done = just done

View file

@ -1,6 +1,8 @@
{-# OPTIONS --rewriting #-}
module Luau.Syntax.FromJSON where
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /; ≡; ≅; <; >; ≤; ; string)
open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=; string)
open import Luau.Type.FromJSON using (typeFromJSON)
open import Agda.Builtin.List using (List; _∷_; [])
@ -26,6 +28,8 @@ vars = fromString "vars"
op = fromString "op"
left = fromString "left"
right = fromString "right"
returnAnnotation = fromString "returnAnnotation"
types = fromString "types"
data Lookup : Set where
_,_ : String Value Lookup
@ -49,22 +53,22 @@ blockFromJSON : Value → Either String (Block maybe)
blockFromArray : Array Either String (Block maybe)
binOpFromJSON (string s) = binOpFromString s
binOpFromJSON val = Left "Binary operator not a string"
binOpFromJSON _ = Left "Binary operator not a string"
binOpFromString "Add" = Right +
binOpFromString "Sub" = Right -
binOpFromString "Mul" = Right *
binOpFromString "Div" = Right /
binOpFromString "CompareEq" = Right
binOpFromString "CompareNe" = Right
binOpFromString "CompareEq" = Right ==
binOpFromString "CompareNe" = Right ~=
binOpFromString "CompareLt" = Right <
binOpFromString "CompareLe" = Right
binOpFromString "CompareLe" = Right <=
binOpFromString "CompareGt" = Right >
binOpFromString "CompareGe" = Right
binOpFromString "CompareGe" = Right >=
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
varDecFromJSON (object arg) = varDecFromObject arg
varDecFromJSON val = Left "VarDec not an object"
varDecFromJSON _ = Left "VarDec not an object"
varDecFromObject obj with lookup name obj | lookup type obj
varDecFromObject obj | just (string name) | nothing = Right (var name)
@ -76,7 +80,7 @@ varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string"
varDecFromObject obj | nothing | _ = Left "AstLocal missing name"
exprFromJSON (object obj) = exprFromObject obj
exprFromJSON val = Left "AstExpr not an object"
exprFromJSON _ = Left "AstExpr not an object"
exprFromObject obj with lookup type obj
exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj
@ -89,33 +93,41 @@ exprFromObject obj | just (string "AstExprCall") | just value | just (array arr)
exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array")
exprFromObject obj | just (string "AstExprCall") | nothing | _ = Left ("AstExprCall missing func")
exprFromObject obj | just (string "AstExprCall") | _ | nothing = Left ("AstExprCall missing args")
exprFromObject obj | just (string "AstExprConstantNil") = Right nil
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue with head arr | blockFromJSON blockValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprConstantNil") = Right (val nil)
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj | lookup returnAnnotation obj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn with head arr | blockFromJSON blockValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B with varDecFromJSON argValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg with lookup types rtnObj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) with head rtnTypes
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType with typeFromJSON rtnType
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Right T = Right (function "" arg ⟩∈ T is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | nothing = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just _ = Left "returnAnnotation types not an array"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | nothing = Left "returnAnnotation missing types"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just _ | just argValue | Right B | Right arg = Left "returnAnnotation not an object"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | just argValue | Right B | Right arg = Right (function "" arg is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | _ | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ | rtn = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ | rtn = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing | rtn = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
exprFromObject obj | just (string "AstExprLocal") | just x | Right x = Right (var (Luau.Syntax.name x))
exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (val (number (toFloat x)))
exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
exprFromObject obj | just (string "AstExprConstantString") with lookup value obj
exprFromObject obj | just (string "AstExprConstantString") | just (string x) = Right (string x)
exprFromObject obj | just (string "AstExprConstantString") | just (string x) = Right (val (string x))
exprFromObject obj | just (string "AstExprConstantString") | just _ = Left "AstExprConstantString value is not a string"
exprFromObject obj | just (string "AstExprConstantString") | nothing = Left "AstExprConstantString missing value"
exprFromObject obj | just (string "AstExprConstantBool") with lookup value obj
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool b) = Right (val (bool b))
exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool missing value"
exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
@ -151,6 +163,7 @@ statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLo
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" x is B end) = Right (function (Luau.Syntax.name fnVar) x is B end)
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" x ⟩∈ T is B end) = Right (function (Luau.Syntax.name fnVar) x ⟩∈ T is B end)
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
@ -184,4 +197,4 @@ blockFromArray arr | just value | Left err = Left err
blockFromArray arr | just value | Right S with blockFromArray(tail arr)
blockFromArray arr | just value | Right S | Left err = Left (err)
blockFromArray arr | just value | Right S | Right B = Right (S B)

View file

@ -1,8 +1,9 @@
module Luau.Syntax.ToString where
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Float using (primShowFloat)
open import Agda.Builtin.String using (primShowString)
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; binexp; true; false; string)
open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; binexp; string)
open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Type.ToString using (typeToString)
@ -25,19 +26,25 @@ binOpToString * = "*"
binOpToString / = "/"
binOpToString < = "<"
binOpToString > = ">"
binOpToString = "=="
binOpToString = "~="
binOpToString = "<="
binOpToString = ">="
binOpToString == = "=="
binOpToString ~= = "~="
binOpToString <= = "<="
binOpToString >= = ">="
valueToString : Value String
valueToString nil = "nil"
valueToString (addr a) = addrToString a
valueToString (number x) = primShowFloat x
valueToString (bool false) = "false"
valueToString (bool true) = "true"
valueToString (string x) = primShowString x
exprToString : {a} String Expr a String
statToString : {a} String Stat a String
blockToString : {a} String Block a String
exprToString lb nil =
"nil"
exprToString lb (addr a) =
addrToString(a)
exprToString lb (val v) =
valueToString(v)
exprToString lb (var x) =
varToString(x)
exprToString lb (M $ N) =
@ -47,14 +54,10 @@ exprToString lb (function F is B end) =
" " ++ (blockToString (lb ++ " ") B) ++ lb ++
"end"
exprToString lb (block b is B end) =
"(" ++ b ++ "()" ++ lb ++
"(" ++ varDecToString b ++ "()" ++ lb ++
" " ++ (blockToString (lb ++ " ") B) ++ lb ++
"end)()"
exprToString lb (number x) = primShowFloat x
exprToString lb (string x) = primShowString x
exprToString lb (binexp x op y) = exprToString lb x ++ " " ++ binOpToString op ++ " " ++ exprToString lb y
exprToString lb true = "true"
exprToString lb false = "false"
statToString lb (function F is B end) =
"local " ++ funDecToString F ++ lb ++

View file

@ -1,5 +1,9 @@
module Luau.Type where
open import FFI.Data.Maybe using (Maybe; just; nothing; just-inv)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (cong)
open import FFI.Data.Maybe using (Maybe; just; nothing)
data Type : Set where
@ -7,18 +11,132 @@ data Type : Set where
_⇒_ : Type Type Type
none : Type
any : Type
boolean : Type
number : Type
__ : Type Type Type
_∩_ : Type Type Type
src : Type Type
src nil = none
src (S T) = S
src none = none
src any = any
src number = none
src (S T) = (src S) (src T)
src (S T) = (src S) (src T)
lhs : Type Type
lhs (T _) = T
lhs (T _) = T
lhs (T _) = T
lhs nil = nil
lhs none = none
lhs any = any
lhs number = number
lhs boolean = boolean
rhs : Type Type
rhs (_ T) = T
rhs (_ T) = T
rhs (_ T) = T
rhs nil = nil
rhs none = none
rhs any = any
rhs number = number
rhs boolean = boolean
_≡ᵀ_ : (T U : Type) Dec(T U)
nil ≡ᵀ nil = yes refl
nil ≡ᵀ (S T) = no (λ ())
nil ≡ᵀ none = no (λ ())
nil ≡ᵀ any = no (λ ())
nil ≡ᵀ number = no (λ ())
nil ≡ᵀ boolean = no (λ ())
nil ≡ᵀ (S T) = no (λ ())
nil ≡ᵀ (S T) = no (λ ())
(S T) ≡ᵀ nil = no (λ ())
(S T) ≡ᵀ (U V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(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) ≡ᵀ 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 (λ ())
number ≡ᵀ nil = no (λ ())
number ≡ᵀ (T U) = no (λ ())
number ≡ᵀ none = no (λ ())
number ≡ᵀ any = 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 ≡ᵀ boolean = yes refl
boolean ≡ᵀ number = no (λ ())
boolean ≡ᵀ (T U) = no (λ ())
boolean ≡ᵀ (T U) = no (λ ())
(S T) ≡ᵀ nil = no (λ ())
(S T) ≡ᵀ (U V) = no (λ ())
(S T) ≡ᵀ none = no (λ ())
(S T) ≡ᵀ any = no (λ ())
(S T) ≡ᵀ number = no (λ ())
(S T) ≡ᵀ boolean = no (λ ())
(S T) ≡ᵀ (U V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(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) ≡ᵀ (U V) = no (λ ())
(S T) ≡ᵀ nil = no (λ ())
(S T) ≡ᵀ (U V) = no (λ ())
(S T) ≡ᵀ none = no (λ ())
(S T) ≡ᵀ any = no (λ ())
(S T) ≡ᵀ number = no (λ ())
(S T) ≡ᵀ boolean = no (λ ())
(S T) ≡ᵀ (U V) = no (λ ())
(S T) ≡ᵀ (U V) with (S ≡ᵀ U) | (T ≡ᵀ V)
(S T) ≡ᵀ (U V) | 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))
_≡ᴹᵀ_ : (T U : Maybe Type) Dec(T U)
nothing ≡ᴹᵀ nothing = yes refl
nothing ≡ᴹᵀ just U = no (λ ())
just T ≡ᴹᵀ nothing = no (λ ())
just T ≡ᴹᵀ just U with T ≡ᵀ U
(just T ≡ᴹᵀ just T) | yes refl = yes refl
(just T ≡ᴹᵀ just U) | no p = no (λ q p (just-inv q))
data Mode : Set where
strict : Mode
nonstrict : Mode
src : Mode Type Type
src m nil = none
src m number = none
src m boolean = none
src m (S T) = S
-- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant
src strict (S T) = (src strict S) (src strict T)
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
tgt : Type Type
tgt nil = none
@ -26,6 +144,7 @@ tgt (S ⇒ T) = T
tgt none = none
tgt any = any
tgt number = none
tgt boolean = none
tgt (S T) = (tgt S) (tgt T)
tgt (S T) = (tgt S) (tgt T)

View file

@ -1,3 +1,5 @@
{-# OPTIONS --rewriting #-}
module Luau.Type.FromJSON where
open import Luau.Type using (Type; nil; _⇒_; __; _∩_; any; number)

View file

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

View file

@ -0,0 +1,143 @@
{-# OPTIONS --rewriting #-}
open import Luau.Type using (Mode)
module Luau.TypeCheck (m : Mode) where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.Type using (Type; Mode; nil; none; number; boolean; _⇒_; tgt)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import FFI.Data.Vector using (Vector)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Product using (_×_; _,_)
src : Type Type
src = Luau.Type.src m
orNone : Maybe Type Type
orNone nothing = none
orNone (just T) = T
tgtBinOp : BinaryOperator Type
tgtBinOp + = number
tgtBinOp - = number
tgtBinOp * = number
tgtBinOp / = number
tgtBinOp < = boolean
tgtBinOp > = boolean
tgtBinOp == = boolean
tgtBinOp ~= = boolean
tgtBinOp <= = boolean
tgtBinOp >= = boolean
data _⊢ᴮ_∈_ : VarCtxt Block yes Type Set
data _⊢ᴱ_∈_ : VarCtxt Expr yes Type Set
data _⊢ᴮ_∈_ where
done : {Γ}
---------------
Γ ⊢ᴮ done nil
return : {M B T U Γ}
Γ ⊢ᴱ M T
Γ ⊢ᴮ B U
---------------------
Γ ⊢ᴮ return M B T
local : {x M B T U V Γ}
Γ ⊢ᴱ M U
(Γ x T) ⊢ᴮ B V
--------------------------------
Γ ⊢ᴮ local var x T M B V
function : {f x B C T U V W Γ}
(Γ x T) ⊢ᴮ C V
(Γ f (T U)) ⊢ᴮ B W
-------------------------------------------------
Γ ⊢ᴮ function f var x T ⟩∈ U is C end B W
data _⊢ᴱ_∈_ where
nil : {Γ}
--------------------
Γ ⊢ᴱ (val nil) nil
var : {x T Γ}
T orNone(Γ [ x ]ⱽ)
----------------
Γ ⊢ᴱ (var x) T
addr : {a Γ} T
-----------------
Γ ⊢ᴱ val(addr a) T
number : {n Γ}
---------------------------
Γ ⊢ᴱ val(number n) number
bool : {b Γ}
--------------------------
Γ ⊢ᴱ val(bool b) boolean
app : {M N T U Γ}
Γ ⊢ᴱ M T
Γ ⊢ᴱ N U
----------------------
Γ ⊢ᴱ (M $ N) (tgt T)
function : {f x B T U V Γ}
(Γ x T) ⊢ᴮ B V
-----------------------------------------------------
Γ ⊢ᴱ (function f var x T ⟩∈ U is B end) (T U)
block : {b B T U Γ}
Γ ⊢ᴮ B U
------------------------------------
Γ ⊢ᴱ (block var b T is B end) T
binexp : {op Γ M N T U}
Γ ⊢ᴱ M T
Γ ⊢ᴱ N U
----------------------------------
Γ ⊢ᴱ (binexp M op N) tgtBinOp op
data ⊢ᴼ_ : Maybe(Object yes) Set where
nothing :
---------
⊢ᴼ nothing
function : {f x T U V B}
(x T) ⊢ᴮ B V
----------------------------------------------
⊢ᴼ (just function f var x T ⟩∈ U is B end)
⊢ᴴ_ : Heap yes Set
⊢ᴴ H = a {O} (H [ a ]ᴴ O) (⊢ᴼ O)
_⊢ᴴᴱ_▷_∈_ : VarCtxt Heap yes Expr yes Type Set
(Γ ⊢ᴴᴱ H M T) = (⊢ᴴ H) × (Γ ⊢ᴱ M T)
_⊢ᴴᴮ_▷_∈_ : VarCtxt Heap yes Block yes Type Set
(Γ ⊢ᴴᴮ H B T) = (⊢ᴴ H) × (Γ ⊢ᴮ B T)

View file

@ -1,23 +0,0 @@
module Luau.Value where
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Float using (Float)
open import Agda.Builtin.String using (String)
open import Luau.Addr using (Addr)
open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false; string)
open import Luau.Var using (Var)
data Value : Set where
nil : Value
addr : Addr Value
number : Float Value
bool : Bool Value
string : String Value
val : {a} Value Expr a
val nil = nil
val (addr a) = addr a
val (number x) = number x
val (bool false) = false
val (bool true) = true
val (string x) = string x

View file

@ -1,15 +0,0 @@
module Luau.Value.ToString where
open import Agda.Builtin.String using (String; primShowString)
open import Agda.Builtin.Float using (primShowFloat)
open import Agda.Builtin.Bool using (true; false)
open import Luau.Value using (Value; nil; addr; number; bool; string)
open import Luau.Addr.ToString using (addrToString)
valueToString : Value String
valueToString nil = "nil"
valueToString (addr a) = addrToString a
valueToString (number x) = primShowFloat x
valueToString (bool false) = "false"
valueToString (bool true) = "true"
valueToString (string x) = primShowString x

View file

@ -4,13 +4,13 @@ open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.String using (String; primStringEquality)
open import Agda.Builtin.TrustMe using (primTrustMe)
open import Properties.Dec using (Dec; yes; no; )
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (_≢_)
Var : Set
Var = String
_≡ⱽ_ : (a b : Var) Dec (a b)
a ≡ⱽ b with primStringEquality a b
a ≡ⱽ b | false = no p where postulate p : (a b)
a ≡ⱽ b | false = no p where postulate p : (a b)
a ≡ⱽ b | true = yes primTrustMe

View file

@ -0,0 +1,43 @@
{-# OPTIONS --rewriting #-}
module Luau.VarCtxt where
open import Agda.Builtin.Equality using (_≡_)
open import Luau.Type using (Type; __; _∩_)
open import Luau.Var using (Var)
open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from; insert-swap; insert-over)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Equality using (_≢_; cong; sym; trans)
VarCtxt : Set
VarCtxt = KeyMap Type
: VarCtxt
= empty
_⋒_ : VarCtxt VarCtxt VarCtxt
_⋒_ = unionWith _∩_
_⋓_ : VarCtxt VarCtxt VarCtxt
_⋓_ = unionWith __
_[_] : VarCtxt Var Maybe Type
Γ [ x ] = lookup (fromString x) Γ
_⊝_ : VarCtxt Var VarCtxt
Γ x = delete (fromString x) Γ
_↦_ : Var Type VarCtxt
x T = singleton (fromString x) T
_⊕_↦_ : VarCtxt Var Type VarCtxt
Γ x T = insert (fromString x) T Γ
⊕-over : {Γ x y T U} (x y) ((Γ x T) y U) (Γ y U)
⊕-over p = insert-over _ _ _ _ _ (cong fromString (sym p))
⊕-swap : {Γ x y T U} (x y) ((Γ x T) y U) ((Γ y U) x T)
⊕-swap p = insert-swap _ _ _ _ _ (λ q p (trans (sym (to-from _)) (trans (cong toString (sym q) ) (to-from _))) )
⊕-lookup-miss : x y T Γ (x y) (Γ [ y ] (Γ x T) [ y ])
⊕-lookup-miss x y T Γ p = lookup-insert-not (fromString x) (fromString y) T Γ λ q p (trans (sym (to-from x)) (trans (cong toString q) (to-from y)))

View file

@ -1,3 +1,5 @@
{-# OPTIONS --rewriting #-}
module PrettyPrinter where
open import Agda.Builtin.IO using (IO)

View file

@ -1,7 +1,11 @@
{-# OPTIONS --rewriting #-}
module Properties where
import Properties.Contradiction
import Properties.Dec
import Properties.Equality
import Properties.Step
import Properties.Remember
import Properties.Step
import Properties.StrictMode
import Properties.TypeCheck

View file

@ -1,8 +1,7 @@
module Properties.Dec where
data : Set where
open import Properties.Contradiction using (¬)
data Dec(A : Set) : Set where
yes : A Dec A
no : (A ) Dec A
no : ¬ A Dec A

View file

@ -0,0 +1,14 @@
module Properties.Product where
infixr 5 _×_ _,_
record Σ {A : Set} (B : A Set) : Set where
constructor _,_
field fst : A
field snd : B fst
open Σ public
_×_ : Set Set Set
A × B = Σ (λ (a : A) B)

View file

@ -1,24 +1,109 @@
{-# OPTIONS --rewriting #-}
module Properties.Step where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess)
open import Agda.Builtin.Bool using (true; false)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
open import Luau.Syntax using (Block; Expr; nil; var; addr; true; false; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; ; string)
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
open import Luau.RuntimeType using (function; number)
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=; string)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp; evalNeqOp)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=)
open import Luau.RuntimeType using (valueType; function; number)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Value using (nil; addr; val; number; bool; string)
open import Properties.Remember using (remember; _,_)
open import Utility.Bool using (not; _or_)
data BinOpStepResult v op w : Set where
step : x (v op w x) BinOpStepResult v op w
error₁ : BinOpError op (valueType(v)) BinOpStepResult v op w
error₂ : BinOpError op (valueType(w)) BinOpStepResult v op w
binOpStep : v op w BinOpStepResult v op w
binOpStep nil + w = error₁ (+ (λ ()))
binOpStep (addr a) + w = error₁ (+ (λ ()))
binOpStep (number m) + nil = error₂ (+ (λ ()))
binOpStep (number m) + (addr a) = error₂ (+ (λ ()))
binOpStep (number m) + (number n) = step (number (primFloatPlus m n)) (+ m n)
binOpStep (number m) + (bool b) = error₂ (+ (λ ()))
binOpStep (number m) + (string x) = error₂ (+ (λ ()))
binOpStep (number m) - (string x) = error₂ (- (λ ()))
binOpStep (number m) * (string x) = error₂ (* (λ ()))
binOpStep (number m) / (string x) = error₂ (/ (λ ()))
binOpStep (number m) < (string x) = error₂ (< (λ ()))
binOpStep (number m) > (string x) = error₂ (> (λ ()))
binOpStep (number m) == (string x) = step (bool false) (== (number m) (string x))
binOpStep (number m) ~= (string x) = step (bool true) (~= (number m) (string x))
binOpStep (number m) <= (string x) = error₂ (<= (λ ()))
binOpStep (number m) >= (string x) = error₂ (>= (λ ()))
binOpStep (bool b) + w = error₁ (+ (λ ()))
binOpStep nil - w = error₁ (- (λ ()))
binOpStep (addr a) - w = error₁ (- (λ ()))
binOpStep (number x) - nil = error₂ (- (λ ()))
binOpStep (number x) - (addr a) = error₂ (- (λ ()))
binOpStep (number x) - (number n) = step (number (primFloatMinus x n)) (- x n)
binOpStep (number x) - (bool b) = error₂ (- (λ ()))
binOpStep (bool b) - w = error₁ (- (λ ()))
binOpStep nil * w = error₁ (* (λ ()))
binOpStep (addr a) * w = error₁ (* (λ ()))
binOpStep (number m) * nil = error₂ (* (λ ()))
binOpStep (number m) * (addr a) = error₂ (* (λ ()))
binOpStep (number m) * (number n) = step (number (primFloatDiv m n)) (* m n)
binOpStep (number m) * (bool b) = error₂ (* (λ ()))
binOpStep (bool b) * w = error₁ (* (λ ()))
binOpStep nil / w = error₁ (/ (λ ()))
binOpStep (addr a) / w = error₁ (/ (λ ()))
binOpStep (number m) / nil = error₂ (/ (λ ()))
binOpStep (number m) / (addr a) = error₂ (/ (λ ()))
binOpStep (number m) / (number n) = step (number (primFloatTimes m n)) (/ m n)
binOpStep (number m) / (bool b) = error₂ (/ (λ ()))
binOpStep (bool b) / w = error₁ (/ (λ ()))
binOpStep nil < w = error₁ (< (λ ()))
binOpStep (addr a) < w = error₁ (< (λ ()))
binOpStep (number m) < nil = error₂ (< (λ ()))
binOpStep (number m) < (addr a) = error₂ (< (λ ()))
binOpStep (number m) < (number n) = step (bool (primFloatLess m n)) (< m n)
binOpStep (number m) < (bool b) = error₂ (< (λ ()))
binOpStep (bool b) < w = error₁ (< (λ ()))
binOpStep nil > w = error₁ (> (λ ()))
binOpStep (addr a) > w = error₁ (> (λ ()))
binOpStep (number m) > nil = error₂ (> (λ ()))
binOpStep (number m) > (addr a) = error₂ (> (λ ()))
binOpStep (number m) > (number n) = step (bool (primFloatLess n m)) (> m n)
binOpStep (number m) > (bool b) = error₂ (> (λ ()))
binOpStep (bool b) > w = error₁ (> (λ ()))
binOpStep v == w = step (bool (evalEqOp v w)) (== v w)
binOpStep v ~= w = step (bool (evalNeqOp v w)) (~= v w)
binOpStep nil <= w = error₁ (<= (λ ()))
binOpStep (addr a) <= w = error₁ (<= (λ ()))
binOpStep (number m) <= nil = error₂ (<= (λ ()))
binOpStep (number m) <= (addr a) = error₂ (<= (λ ()))
binOpStep (number m) <= (number n) = step (bool (primFloatLess m n or primFloatEquality m n)) (<= m n)
binOpStep (number m) <= (bool b) = error₂ (<= (λ ()))
binOpStep (bool b) <= w = error₁ (<= (λ ()))
binOpStep nil >= w = error₁ (>= (λ ()))
binOpStep (addr a) >= w = error₁ (>= (λ ()))
binOpStep (number m) >= nil = error₂ (>= (λ ()))
binOpStep (number m) >= (addr a) = error₂ (>= (λ ()))
binOpStep (number m) >= (number n) = step (bool (primFloatLess n m or primFloatEquality m n)) (>= m n)
binOpStep (number m) >= (bool b) = error₂ (>= (λ ()))
binOpStep (bool b) >= w = error₁ (>= (λ ()))
binOpStep (string x) + w = error₁ (+ (λ ()))
binOpStep (string x) - w = error₁ (- (λ ()))
binOpStep (string x) * w = error₁ (* (λ ()))
binOpStep (string x) / w = error₁ (/ (λ ()))
binOpStep (string x) < w = error₁ (< (λ ()))
binOpStep (string x) > w = error₁ (> (λ ()))
binOpStep (string x) <= w = error₁ (<= (λ ()))
binOpStep (string x) >= w = error₁ (>= (λ ()))
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
data StepResultᴮ H B where
step : H B (H B ⟶ᴮ B H) StepResultᴮ H B
return : V {B} (B (return (val V) B)) StepResultᴮ H B
return : v {B} (B (return (val v) B)) StepResultᴮ H B
done : (B done) StepResultᴮ H B
error : (RuntimeErrorᴮ H B) StepResultᴮ H B
@ -30,58 +115,45 @@ data StepResultᴱ H M where
stepᴱ : {a} H M StepResultᴱ {a} H M
stepᴮ : {a} H B StepResultᴮ {a} H B
stepᴱ H nil = value nil refl
stepᴱ H (var x) = error (UnboundVariable x)
stepᴱ H (addr a) = value (addr a) refl
stepᴱ H (number x) = value (number x) refl
stepᴱ H (string x) = value (string x) refl
stepᴱ H (true) = value (bool true) refl
stepᴱ H (false) = value (bool false) refl
stepᴱ H (val v) = value v refl
stepᴱ H (var x) = error UnboundVariable
stepᴱ H (M $ N) with stepᴱ H M
stepᴱ H (M $ N) | step H M D = step H (M $ N) (app₁ D)
stepᴱ H (_ $ N) | value V refl with stepᴱ H N
stepᴱ H (_ $ N) | value V refl | step H N s = step H (val V $ N) (app₂ s)
stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
stepᴱ H (_ $ _) | value (string x) refl | value W refl = error (app₁ (TypeMismatch function (string x) λ()))
stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ()))
stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (nothing , p) = error (app₁ (SEGV a p))
stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
stepᴱ H (_ $ N) | value v refl with stepᴱ H N
stepᴱ H (_ $ N) | value v refl | step H N s = step H (val v $ N) (app₂ v s)
stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ])
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV p))
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p)
stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ()))
stepᴱ H (_ $ _) | value (number m) refl | value w refl = error (FunctionMismatch (number m) w (λ ()))
stepᴱ H (_ $ _) | value (bool b) refl | value w refl = error (FunctionMismatch (bool b) w (λ ()))
stepᴱ H (_ $ _) | value (string x) refl | value w refl = error (FunctionMismatch (string x) w (λ ()))
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
stepᴱ H (M $ N) | error E = error (app₁ E)
stepᴱ H (block b is B end) with stepᴮ H B
stepᴱ H (block b is B end) | step H B D = step H (block b is B end) (block D)
stepᴱ H (block b is (return _ B) end) | return V refl = step H (val V) return
stepᴱ H (block b is done end) | done refl = step H nil done
stepᴱ H (block b is B end) | error E = error (block b E)
stepᴱ H (block b is (return _ B) end) | return v refl = step H (val v) (return v)
stepᴱ H (block b is done end) | done refl = step H (val nil) done
stepᴱ H (block b is B end) | error E = error (block E)
stepᴱ H (function F is C end) with alloc H (function F is C end)
stepᴱ H function F is C end | ok a H p = step H (addr a) (function p)
stepᴱ H (binexp x op y) with stepᴱ H x
stepᴱ H (binexp x op y) | value x refl with stepᴱ H y
-- Have to use explicit form for ≡ here because it's a heavily overloaded symbol
stepᴱ H (binexp x Luau.Syntax.≡ y) | value x refl | value y refl = step H (val (evalEqOp x y)) binOpEquality
stepᴱ H (binexp x y) | value x refl | value y refl = step H (val (evalNeqOp x y)) binOpInequality
stepᴱ H (binexp x op y) | value (number x) refl | value (number y) refl = step H (val (evalNumOp x op y)) binOpNumbers
stepᴱ H (binexp x op y) | value (number x) refl | step H y s = step H (binexp (number x) op y) (binOp₂ s)
stepᴱ H (binexp x op y) | value (number x) refl | error E = error (bin₂ E)
stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ()))
stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
stepᴱ H (binexp x op y) | value (string x) refl | _ = error (bin₁ (TypeMismatch number (string x) λ()))
stepᴱ H (binexp x op y) | _ | value (string x) refl = error (bin₂ (TypeMismatch number (string x) λ()))
stepᴱ H (binexp x op y) | value (bool x) refl | _ = error (bin₁ (TypeMismatch number (bool x) λ()))
stepᴱ H (binexp x op y) | _ | value (bool y) refl = error (bin₂ (TypeMismatch number (bool y) λ()))
stepᴱ H (binexp x op y) | step H x s = step H (binexp x op y) (binOp₁ s)
stepᴱ H (binexp x op y) | error E = error (bin₁ E)
stepᴱ H function F is C end | ok a H p = step H (val (addr a)) (function a p)
stepᴱ H (binexp M op N) with stepᴱ H M
stepᴱ H (binexp M op N) | step H M s = step H (binexp M op N) (binOp₁ s)
stepᴱ H (binexp M op N) | error E = error (bin₁ E)
stepᴱ H (binexp M op N) | value v refl with stepᴱ H N
stepᴱ H (binexp M op N) | value v refl | step H N s = step H (binexp (val v) op N) (binOp₂ s)
stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E)
stepᴱ H (binexp M op N) | value v refl | value w refl with binOpStep v op w
stepᴱ H (binexp M op N) | value v refl | value w refl | step x p = step H (val x) (binOp₀ p)
stepᴱ H (binexp M op N) | value v refl | value w refl | error₁ E = error (BinOpMismatch₁ v w E)
stepᴱ H (binexp M op N) | value v refl | value w refl | error₂ E = error (BinOpMismatch₂ v w E)
stepᴮ H (function F is C end B) with alloc H (function F is C end)
stepᴮ H (function F is C end B) | ok a H p = step H (B [ addr a / fun F ]ᴮ) (function p)
stepᴮ H (function F is C end B) | ok a H p = step H (B [ addr a / name (fun F) ]ᴮ) (function a p)
stepᴮ H (local x M B) with stepᴱ H M
stepᴮ H (local x M B) | step H M D = step H (local x M B) (local D)
stepᴮ H (local x _ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
stepᴮ H (local x M B) | error E = error (local x E)
stepᴮ H (local x _ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v)
stepᴮ H (local x M B) | error E = error (local E)
stepᴮ H (return M B) with stepᴱ H M
stepᴮ H (return M B) | step H M D = step H (return M B) (return D)
stepᴮ H (return _ B) | value V refl = return V refl

View file

@ -0,0 +1,470 @@
{-# OPTIONS --rewriting #-}
module Properties.StrictMode where
import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; to ∅ᴴ)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=)
open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
open import Luau.Var using (_≡ⱽ_)
open import Luau.Addr using (_≡ᴬ_)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
open import Luau.VarCtxt using (VarCtxt; )
open import Properties.Remember using (remember; _,_)
open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=)
open import Luau.RuntimeType using (valueType)
src = Luau.Type.src strict
data _⊑_ (H : Heap yes) : Heap yes Set where
refl : (H H)
snoc : {H a V} (H ≡ᴴ H a V) (H H)
rednᴱ⊑ : {H H M M} (H M ⟶ᴱ M H) (H H)
rednᴮ⊑ : {H H B B} (H B ⟶ᴮ B H) (H H)
rednᴱ⊑ (function a p) = snoc p
rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
rednᴱ⊑ (beta O v p q) = refl
rednᴱ⊑ (block s) = rednᴮ⊑ s
rednᴱ⊑ (return v) = refl
rednᴱ⊑ done = refl
rednᴱ⊑ (binOp₀ p) = refl
rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s
rednᴮ⊑ (local s) = rednᴱ⊑ s
rednᴮ⊑ (subst v) = refl
rednᴮ⊑ (function a p) = snoc p
rednᴮ⊑ (return s) = rednᴱ⊑ s
data LookupResult (H : Heap yes) a V : Set where
just : (H [ a ]ᴴ just V) LookupResult H a V
nothing : (H [ a ]ᴴ nothing) LookupResult H a V
lookup-⊑-nothing : {H H} a (H H) (H [ a ]ᴴ nothing) (H [ a ]ᴴ nothing)
lookup-⊑-nothing {H} a refl p = p
lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p
data OrWarningᴱ {Γ M T} (H : Heap yes) (D : Γ ⊢ᴱ M T) A : Set where
ok : A OrWarningᴱ H D A
warning : Warningᴱ H D OrWarningᴱ H D A
data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B T) A : Set where
ok : A OrWarningᴮ H D A
warning : Warningᴮ H D OrWarningᴮ H D A
data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H M T) A : Set where
ok : A OrWarningᴴᴱ H D A
warning : Warningᴴᴱ H D OrWarningᴴᴱ H D A
data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H B T) A : Set where
ok : A OrWarningᴴᴮ H D A
warning : Warningᴴᴮ H D OrWarningᴴᴮ H D A
heap-weakeningᴱ : H M {H Γ} (H H) OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M typeOfᴱ H Γ M)
heap-weakeningᴮ : H B {H Γ} (H H) OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B typeOfᴮ H Γ B)
heap-weakeningᴱ H (var x) h = ok refl
heap-weakeningᴱ H (val nil) h = ok refl
heap-weakeningᴱ H (val (addr a)) refl = ok refl
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} defn) with a ≡ᴬ b
heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl)
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
heap-weakeningᴱ H (val (number n)) h = ok refl
heap-weakeningᴱ H (val (bool b)) h = ok refl
heap-weakeningᴱ H (binexp M op N) h = ok refl
heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W)
heap-weakeningᴱ H (function f var x T ⟩∈ U is B end) h = ok refl
heap-weakeningᴱ H (block var b T is B end) h = ok refl
heap-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h with heap-weakeningᴮ H B h
heap-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h | ok p = ok p
heap-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h | warning W = warning (function₂ W)
heap-weakeningᴮ H (local var x T M B) h with heap-weakeningᴮ H B h
heap-weakeningᴮ H (local var x T M B) h | ok p = ok p
heap-weakeningᴮ H (local var x T M B) h | warning W = warning (local₂ W)
heap-weakeningᴮ H (return M B) h with heap-weakeningᴱ H M h
heap-weakeningᴮ H (return M B) h | ok p = ok p
heap-weakeningᴮ H (return M B) h | warning W = warning (return W)
heap-weakeningᴮ H (done) h = ok refl
none-not-obj : O none typeOfᴼ O
none-not-obj (function f var x T ⟩∈ U is B end) ()
typeOf-val-not-none : {H Γ} v OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (none typeOfᴱ H Γ (val v))
typeOf-val-not-none nil = ok (λ ())
typeOf-val-not-none (number n) = ok (λ ())
typeOf-val-not-none (bool b) = ok (λ ())
typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)
substitutivityᴱ : {Γ T} H M v x (just T typeOfⱽ H v) (typeOfᴱ H (Γ x T) M typeOfᴱ H Γ (M [ v / x ]ᴱ))
substitutivityᴱ-whenever-yes : {Γ T} H v x y (p : x y) (just T typeOfⱽ H v) (typeOfᴱ H (Γ x T) (var y) typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p)))
substitutivityᴱ-whenever-no : {Γ T} H v x y (p : x y) (just T typeOfⱽ H v) (typeOfᴱ H (Γ x T) (var y) typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p)))
substitutivityᴮ : {Γ T} H B v x (just T typeOfⱽ H v) (typeOfᴮ H (Γ x T) B typeOfᴮ H Γ (B [ v / x ]ᴮ))
substitutivityᴮ-unless-yes : {Γ Γ′ T} H B v x y (p : x y) (just T typeOfⱽ H v) (Γ′ Γ) (typeOfᴮ H Γ′ B typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p)))
substitutivityᴮ-unless-no : {Γ Γ′ T} H B v x y (p : x y) (just T typeOfⱽ H v) (Γ′ Γ x T) (typeOfᴮ H Γ′ B typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p)))
substitutivityᴱ H (var y) v x p with x ≡ⱽ y
substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p
substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p
substitutivityᴱ H (val w) v x p = refl
substitutivityᴱ H (binexp M op N) v x p = refl
substitutivityᴱ H (M $ N) v x p = cong tgt (substitutivityᴱ H M v x p)
substitutivityᴱ H (function f var y T ⟩∈ U is B end) v x p = refl
substitutivityᴱ H (block var b T is B end) v x p = refl
substitutivityᴱ-whenever-yes H v x x refl q = cong orNone q
substitutivityᴱ-whenever-no H v x y p q = cong orNone ( sym (⊕-lookup-miss x y _ _ p))
substitutivityᴮ H (function f var y T ⟩∈ U is C end B) v x p with x ≡ⱽ f
substitutivityᴮ H (function f var y T ⟩∈ U is C end B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q)
substitutivityᴮ H (function f var y T ⟩∈ U is C end B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q)
substitutivityᴮ H (local var y T M B) v x p with x ≡ⱽ y
substitutivityᴮ H (local var y T M B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q)
substitutivityᴮ H (local var y T M B) v x p | no q = substitutivityᴮ-unless-no H B v x y q p (⊕-swap q)
substitutivityᴮ H (return M B) v x p = substitutivityᴱ H M v x p
substitutivityᴮ H done v x p = refl
substitutivityᴮ-unless-yes H B v x x refl q refl = refl
substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q
binOpPreservation : H {op v w x} (v op w x) (tgtBinOp op typeOfᴱ H (val x))
binOpPreservation H (+ m n) = refl
binOpPreservation H (- m n) = refl
binOpPreservation H (/ m n) = refl
binOpPreservation H (* m n) = refl
binOpPreservation H (< m n) = refl
binOpPreservation H (> m n) = refl
binOpPreservation H (<= m n) = refl
binOpPreservation H (>= m n) = refl
binOpPreservation H (== v w) = refl
binOpPreservation H (~= v w) = refl
preservationᴱ : H M {H M} (H M ⟶ᴱ M H) OrWarningᴴᴱ H (typeCheckᴴᴱ H M) (typeOfᴱ H M typeOfᴱ H M)
preservationᴮ : H B {H B} (H B ⟶ᴮ B H) OrWarningᴴᴮ H (typeCheckᴴᴮ H B) (typeOfᴮ H B typeOfᴮ H B)
preservationᴱ H (function f var x T ⟩∈ U is B end) (function a defn) = ok refl
preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s
preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p)
preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W))
preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W)
preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s)
preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q)
preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W))
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x S) B
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orNone (cong typeOfᴹᴼ p)))
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r)))
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s r (trans (trans (sym (cong src (cong orNone (cong typeOfᴹᴼ p)))) s) (cong orNone q)))))
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-none v
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (cong orNone q)))
preservationᴱ H (val (addr a) $ N) (beta (function f var x S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
preservationᴱ H (block var b T is B end) (block s) = ok refl
preservationᴱ H (block var b T is return M B end) (return v) with T ≡ᵀ typeOfᴱ H (val v)
preservationᴱ H (block var b T is return M B end) (return v) | yes p = ok p
preservationᴱ H (block var b T is return M B end) (return v) | no p = warning (expr (BlockMismatch p))
preservationᴱ H (block var b T is done end) (done) with T ≡ᵀ nil
preservationᴱ H (block var b T is done end) (done) | yes p = ok p
preservationᴱ H (block var b T is done end) (done) | no p = warning (expr (BlockMismatch p))
preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s)
preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl
preservationᴮ H (local var x T M B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s)
preservationᴮ H (local var x T M B) (local s) | ok p = ok p
preservationᴮ H (local var x T M B) (local s) | warning W = warning (block (local₂ W))
preservationᴮ H (local var x T M B) (subst v) with remember (typeOfⱽ H v)
preservationᴮ H (local var x T M B) (subst v) | (just U , p) with T ≡ᵀ U
preservationᴮ H (local var x T M B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p))
preservationᴮ H (local var x T M B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r q (trans r (cong orNone p)))))
preservationᴮ H (local var x T M B) (subst v) | (nothing , p) with typeOf-val-not-none v
preservationᴮ H (local var x T M B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orNone p)))
preservationᴮ H (local var x T M B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W))
preservationᴮ H (function f var x T ⟩∈ U is C end B) (function a defn) with heap-weakeningᴮ H B (snoc defn)
preservationᴮ H (function f var x T ⟩∈ U is C end B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl))
preservationᴮ H (function f var x T ⟩∈ U is C end B) (function a defn) | warning W = warning (block (function₂ W))
preservationᴮ H (return M B) (return s) with preservationᴱ H M s
preservationᴮ H (return M B) (return s) | ok p = ok p
preservationᴮ H (return M B) (return s) | warning (expr W) = warning (block (return W))
preservationᴮ H (return M B) (return s) | warning (heap W) = warning (heap W)
reflect-substitutionᴱ : {Γ T} H M v x (just T typeOfⱽ H v) Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) Warningᴱ H (typeCheckᴱ H (Γ x T) M)
reflect-substitutionᴱ-whenever-yes : {Γ T} H v x y (p : x y) (just T typeOfⱽ H v) Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) Warningᴱ H (typeCheckᴱ H (Γ x T) (var y))
reflect-substitutionᴱ-whenever-no : {Γ T} H v x y (p : x y) (just T typeOfⱽ H v) Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) Warningᴱ H (typeCheckᴱ H (Γ x T) (var y))
reflect-substitutionᴮ : {Γ T} H B v x (just T typeOfⱽ H v) Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) Warningᴮ H (typeCheckᴮ H (Γ x T) B)
reflect-substitutionᴮ-unless-yes : {Γ Γ′ T} H B v x y (r : x y) (just T typeOfⱽ H v) (Γ′ Γ) Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) Warningᴮ H (typeCheckᴮ H Γ′ B)
reflect-substitutionᴮ-unless-no : {Γ Γ′ T} H B v x y (r : x y) (just T typeOfⱽ H v) (Γ′ Γ x T) Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) Warningᴮ H (typeCheckᴮ H Γ′ B)
reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y
reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W
reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W
reflect-substitutionᴱ H (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r
reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p))))
reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W)
reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W)
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r))))
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r))))
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y)
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
reflect-substitutionᴱ H (function f var y T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
reflect-substitutionᴱ H (block var b T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r q (trans r (substitutivityᴮ H B v x p)))
reflect-substitutionᴱ H (block var b T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W)
reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₁ q) = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q)
reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q)
reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W)
reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W)
reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r)
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q)
reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | ()
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r))))
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r))))
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₁ W) with (x ≡ⱽ y)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₂ W) with (x ≡ⱽ f)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W)
reflect-substitutionᴮ H (function f var y T ⟩∈ U is C end B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W)
reflect-substitutionᴮ H (local var y T M B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r q (trans r (substitutivityᴱ H M v x p)))
reflect-substitutionᴮ H (local var y T M B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W)
reflect-substitutionᴮ H (local var y T M B) v x p (local₂ W) with (x ≡ⱽ y)
reflect-substitutionᴮ H (local var y T M B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
reflect-substitutionᴮ H (local var y T M B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
reflect-substitutionᴮ H (return M B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W)
reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W
reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W
reflect-weakeningᴱ : H M {H Γ} (H H) Warningᴱ H (typeCheckᴱ H Γ M) Warningᴱ H (typeCheckᴱ H Γ M)
reflect-weakeningᴮ : H B {H Γ} (H H) Warningᴮ H (typeCheckᴮ H Γ B) Warningᴮ H (typeCheckᴮ H Γ B)
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) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r p (trans (cong src (sym q₁)) (trans r q₂)))
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W
reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W
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) with heap-weakeningᴱ H M h
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)
reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | warning W = bin₂ W
reflect-weakeningᴱ H (binexp M op N) h (bin₁ W) = bin₁ (reflect-weakeningᴱ H M h W)
reflect-weakeningᴱ H (binexp M op N) h (bin₂ W) = bin₂ (reflect-weakeningᴱ H N h W)
reflect-weakeningᴱ H (function f var y T ⟩∈ U is B end) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴱ H (function f var y T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r p (trans r q))
reflect-weakeningᴱ H (function f var y T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴱ H (function f var y T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴱ H (block var b T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴱ H (block var b T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r p (trans r q))
reflect-weakeningᴱ H (block var b T is B end) h (BlockMismatch p) | warning W = block₁ W
reflect-weakeningᴱ H (block var b T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴮ H (return M B) h (return W) = return (reflect-weakeningᴱ H M h W)
reflect-weakeningᴮ H (local var y T M B) h (LocalVarMismatch p) with heap-weakeningᴱ H M h
reflect-weakeningᴮ H (local var y T M B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r p (trans r q))
reflect-weakeningᴮ H (local var y T M B) h (LocalVarMismatch p) | warning W = local₁ W
reflect-weakeningᴮ H (local var y T M B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W)
reflect-weakeningᴮ H (local var y T M B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h
reflect-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r p (trans r q))
reflect-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W)
reflect-weakeningᴮ H (function f var x T ⟩∈ U is C end B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W)
reflect-weakeningᴼ : H O {H} (H H) Warningᴼ H (typeCheckᴼ H O) Warningᴼ H (typeCheckᴼ H O)
reflect-weakeningᴼ H (just (function f var x T ⟩∈ U is B end)) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
reflect-weakeningᴼ H (just (function f var x T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r p (trans r q))
reflect-weakeningᴼ H (just (function f var x T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W
reflect-weakeningᴼ H (just (function f var x T ⟩∈ U is B end)) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W)
reflectᴱ : H M {H M} (H M ⟶ᴱ M H) Warningᴱ H (typeCheckᴱ H M) Warningᴴᴱ H (typeCheckᴴᴱ H M)
reflectᴮ : H B {H B} (H B ⟶ᴮ B H) Warningᴮ H (typeCheckᴮ H B) Warningᴴᴮ H (typeCheckᴴᴮ H B)
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s)
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q = expr (FunctionCallMismatch (λ r p (trans (trans (cong src (sym q)) r) q)))
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W)
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W = expr (app₂ W)
reflectᴱ H (M $ N) (app₁ s) (app₁ W) with reflectᴱ H M s W
reflectᴱ H (M $ N) (app₁ s) (app₁ W) | heap W = heap W
reflectᴱ H (M $ N) (app₁ s) (app₁ W) | expr W = expr (app₁ W)
reflectᴱ H (M $ N) (app₁ s) (app₂ W) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W))
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p) | ok q | ok q = expr (FunctionCallMismatch (λ r p (trans (trans (cong src (sym q)) r) q)))
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p) | warning W | _ = expr (app₁ W)
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p) | _ | warning (expr W) = expr (app₂ W)
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p) | _ | warning (heap W) = heap W
reflectᴱ H (M $ N) (app₂ p s) (app₁ W) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W))
reflectᴱ H (M $ N) (app₂ p s) (app₂ W) with reflectᴱ H N s W
reflectᴱ H (M $ N) (app₂ p s) (app₂ W) | heap W = heap W
reflectᴱ H (M $ N) (app₂ p s) (app₂ W) | expr W = expr (app₂ W)
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v)
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s q (trans s (substitutivityᴮ H B v x (sym r))))))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t s (trans (cong orNone (sym r)) (trans (sym t) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-none v
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (cong orNone (sym r)))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W)
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) with remember (typeOfⱽ H v)
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (just S , q) with S ≡ᵀ T
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W)))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (just S , q) | no r = expr (FunctionCallMismatch (λ s r (trans (cong orNone (sym q)) (trans (sym s) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (nothing , q) with typeOf-val-not-none v
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (nothing , q) | ok r = CONTRADICTION (r (cong orNone (sym q)))
reflectᴱ H (val (addr a) $ N) (beta (function f var x T ⟩∈ U is B end) v refl p) (block₁ W) | (nothing , q) | warning W = expr (app₂ W)
reflectᴱ H (block var b T is B end) (block s) (BlockMismatch p) with preservationᴮ H B s
reflectᴱ H (block var b T is B end) (block s) (BlockMismatch p) | ok q = expr (BlockMismatch (λ r p (trans r q)))
reflectᴱ H (block var b T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W
reflectᴱ H (block var b T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W)
reflectᴱ H (block var b T is B end) (block s) (block₁ W) with reflectᴮ H B s W
reflectᴱ H (block var b T is B end) (block s) (block₁ W) | heap W = heap W
reflectᴱ H (block var b T is B end) (block s) (block₁ W) | block W = expr (block₁ W)
reflectᴱ H (block var b T is B end) (return v) W = expr (block₁ (return W))
reflectᴱ H (function f var x T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) with preservationᴱ H M s
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p)))
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W) with reflectᴱ H M s W
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W) | heap W = heap W
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W) | expr W = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s)
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W)
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W)
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W))
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W) with reflectᴱ H N s W
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W) | heap W = heap W
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W) | expr W = expr (bin₂ W)
reflectᴮ H (local var x T M B) (local s) (LocalVarMismatch p) with preservationᴱ H M s
reflectᴮ H (local var x T M B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r p (trans r q)))
reflectᴮ H (local var x T M B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W)
reflectᴮ H (local var x T M B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W
reflectᴮ H (local var x T M B) (local s) (local₁ W) with reflectᴱ H M s W
reflectᴮ H (local var x T M B) (local s) (local₁ W) | heap W = heap W
reflectᴮ H (local var x T M B) (local s) (local₁ W) | expr W = block (local₁ W)
reflectᴮ H (local var x T M B) (local s) (local₂ W) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W))
reflectᴮ H (local var x T M B) (subst v) W with remember (typeOfⱽ H v)
reflectᴮ H (local var x T M B) (subst v) W | (just S , p) with S ≡ᵀ T
reflectᴮ H (local var x T M B) (subst v) W | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W))
reflectᴮ H (local var x T M B) (subst v) W | (just S , p) | no q = block (LocalVarMismatch (λ r q (trans (cong orNone (sym p)) (sym r))))
reflectᴮ H (local var x T M B) (subst v) W | (nothing , p) with typeOf-val-not-none v
reflectᴮ H (local var x T M B) (subst v) W | (nothing , p) | ok r = CONTRADICTION (r (cong orNone (sym p)))
reflectᴮ H (local var x T M B) (subst v) W | (nothing , p) | warning W = block (local₁ W)
reflectᴮ H (function f var y T ⟩∈ U is C end B) (function a defn) W = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W)))
reflectᴮ H (return M B) (return s) (return W) with reflectᴱ H M s W
reflectᴮ H (return M B) (return s) (return W) | heap W = heap W
reflectᴮ H (return M B) (return s) (return W) | expr W = block (return W)
reflectᴴᴱ : H M {H M} (H M ⟶ᴱ M H) Warningᴴᴱ H (typeCheckᴴᴱ H M) Warningᴴᴱ H (typeCheckᴴᴱ H M)
reflectᴴᴮ : H B {H B} (H B ⟶ᴮ B H) Warningᴴᴮ H (typeCheckᴴᴮ H B) Warningᴴᴮ H (typeCheckᴴᴮ H B)
reflectᴴᴱ H M s (expr W) = reflectᴱ H M s W
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a p) (heap (addr b refl W)) with b ≡ᴬ a
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn)
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q p (trans q r))
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W)
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W))
reflectᴴᴱ H (function f var x T ⟩∈ U is B end) (function a p) (heap (addr b refl W)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W))
reflectᴴᴱ H (M $ N) (app₁ s) (heap W) with reflectᴴᴱ H M s (heap W)
reflectᴴᴱ H (M $ N) (app₁ s) (heap W) | heap W = heap W
reflectᴴᴱ H (M $ N) (app₁ s) (heap W) | expr W = expr (app₁ W)
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W) with reflectᴴᴱ H N s (heap W)
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W) | heap W = heap W
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W) | expr W = expr (app₂ W)
reflectᴴᴱ H (M $ N) (beta O v p q) (heap W) = heap W
reflectᴴᴱ H (block var b T is B end) (block s) (heap W) with reflectᴴᴮ H B s (heap W)
reflectᴴᴱ H (block var b T is B end) (block s) (heap W) | heap W = heap W
reflectᴴᴱ H (block var b T is B end) (block s) (heap W) | block W = expr (block₁ W)
reflectᴴᴱ H (block var b T is return N B end) (return v) (heap W) = heap W
reflectᴴᴱ H (block var b T is done end) done (heap W) = heap W
reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W) = heap W
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W) with reflectᴴᴱ H M s (heap W)
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W) | heap W = heap W
reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W) | expr W = expr (bin₁ W)
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W) with reflectᴴᴱ H N s (heap W)
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W) | heap W = heap W
reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W) | expr W = expr (bin₂ W)
reflectᴴᴮ H B s (block W) = reflectᴮ H B s W
reflectᴴᴮ H (local var x T M B) (local s) (heap W) with reflectᴴᴱ H M s (heap W)
reflectᴴᴮ H (local var x T M B) (local s) (heap W) | heap W = heap W
reflectᴴᴮ H (local var x T M B) (local s) (heap W) | expr W = block (local₁ W)
reflectᴴᴮ H (local var x T M B) (subst v) (heap W) = heap W
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a p) (heap (addr b refl W)) with b ≡ᴬ a
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn)
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q p (trans q r)))
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W)
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a defn) (heap (addr a refl (function₁ W))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W))
reflectᴴᴮ H (function f var y T ⟩∈ U is C end B) (function a p) (heap (addr b refl W)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W))
reflectᴴᴮ H (return M B) (return s) (heap W) with reflectᴴᴱ H M s (heap W)
reflectᴴᴮ H (return M B) (return s) (heap W) | heap W = heap W
reflectᴴᴮ H (return M B) (return s) (heap W) | expr W = block (return W)
reflect* : H B {H B} (H B ⟶* B H) Warningᴴᴮ H (typeCheckᴴᴮ H B) Warningᴴᴮ H (typeCheckᴴᴮ H B)
reflect* H B refl W = W
reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
runtimeBinOpWarning : H {op} v BinOpError op (valueType v) BinOpWarning op (orNone (typeOfⱽ H v))
runtimeBinOpWarning H v (+ p) = + (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (- p) = - (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (* p) = * (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (/ p) = / (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (< p) = < (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (> p) = > (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (<= p) = <= (λ q p (mustBeNumber H v q))
runtimeBinOpWarning H v (>= p) = >= (λ q p (mustBeNumber H v q))
runtimeWarningᴱ : H M RuntimeErrorᴱ H M Warningᴱ H (typeCheckᴱ H M)
runtimeWarningᴮ : H B RuntimeErrorᴮ H B Warningᴮ H (typeCheckᴮ H B)
runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl
runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-none w
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = FunctionCallMismatch (λ r p (mustBeFunction H v (λ r q (trans r r))))
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W
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)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₁ v w p) = BinOpMismatch₁ (runtimeBinOpWarning H v p)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₂ v w p) = BinOpMismatch₂ (runtimeBinOpWarning H w p)
runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err)
runtimeWarningᴮ H (local var x T M B) (local err) = local₁ (runtimeWarningᴱ H M err)
runtimeWarningᴮ H (return M B) (return err) = return (runtimeWarningᴱ H M err)
wellTypedProgramsDontGoWrong : H B B (∅ᴴ B ⟶* B H) (RuntimeErrorᴮ H B) Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ B)
wellTypedProgramsDontGoWrong H B B t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H B err))
wellTypedProgramsDontGoWrong H B B t err | heap (addr a refl ())
wellTypedProgramsDontGoWrong H B B t err | block W = W

View file

@ -0,0 +1,103 @@
{-# OPTIONS --rewriting #-}
open import Luau.Type using (Mode)
module Properties.TypeCheck (m : Mode) where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Bool using (Bool; true; false)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Either using (Either)
open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Type using (Type; nil; any; none; number; boolean; _⇒_; tgt)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType)
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.Addr using (Addr)
open import Luau.Var using (Var; _≡ⱽ_)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.Dec using (yes; no)
open import Properties.Equality using (_≢_; sym; trans; cong)
open import Properties.Product using (_×_; _,_)
open import Properties.Remember using (Remember; remember; _,_)
src : Type Type
src = Luau.Type.src m
typeOfᴼ : Object yes Type
typeOfᴼ (function f var x S ⟩∈ T is B end) = (S T)
typeOfᴹᴼ : Maybe(Object yes) Maybe Type
typeOfᴹᴼ nothing = nothing
typeOfᴹᴼ (just O) = just (typeOfᴼ O)
typeOfⱽ : Heap yes Value Maybe Type
typeOfⱽ H nil = just nil
typeOfⱽ H (bool b) = just boolean
typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ)
typeOfⱽ H (number n) = just number
typeOfᴱ : Heap yes VarCtxt (Expr yes) Type
typeOfᴮ : Heap yes VarCtxt (Block yes) Type
typeOfᴱ H Γ (var x) = orNone(Γ [ x ]ⱽ)
typeOfᴱ H Γ (val v) = orNone(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
typeOfᴱ H Γ (binexp M op N) = tgtBinOp op
typeOfᴮ H Γ (function f var x S ⟩∈ T is C end B) = typeOfᴮ H (Γ f (S T)) B
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 Γ nil p = CONTRADICTION (p refl)
mustBeFunction H Γ (addr a) p = refl
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
mustBeNumber : H Γ v (typeOfᴱ H Γ (val v) number) (valueType(v) number)
mustBeNumber H Γ nil ()
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | (just function f var x T ⟩∈ U is B end , q) | ()
mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | nothing , q | ()
mustBeNumber H Γ (number n) p = refl
mustBeNumber H Γ (bool true) ()
mustBeNumber H Γ (bool false) ()
typeCheckᴱ : H Γ M (Γ ⊢ᴱ M (typeOfᴱ H Γ M))
typeCheckᴮ : H Γ B (Γ ⊢ᴮ B (typeOfᴮ H Γ B))
typeCheckᴱ H Γ (var x) = var refl
typeCheckᴱ H Γ (val nil) = nil
typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
typeCheckᴱ H Γ (val (number n)) = number
typeCheckᴱ H Γ (val (bool b)) = bool
typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
typeCheckᴱ H Γ (function f var x T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ x T) B)
typeCheckᴱ H Γ (block var b T is B end) = block (typeCheckᴮ H Γ B)
typeCheckᴱ H Γ (binexp M op N) = binexp (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
typeCheckᴮ H Γ (function f var x T ⟩∈ U is C end B) = function (typeCheckᴮ H (Γ x T) C) (typeCheckᴮ H (Γ f (T U)) B)
typeCheckᴮ H Γ (local var x T M B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ x T) B)
typeCheckᴮ H Γ (return M B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B)
typeCheckᴮ H Γ done = done
typeCheckᴼ : H O (⊢ᴼ O)
typeCheckᴼ H nothing = nothing
typeCheckᴼ H (just function f var x T ⟩∈ U is B end) = function (typeCheckᴮ H (x T) B)
typeCheckᴴ : H (⊢ᴴ H)
typeCheckᴴ H a {O} p = typeCheckᴼ H (O)
typeCheckᴴᴱ : H Γ M (Γ ⊢ᴴᴱ H M typeOfᴱ H Γ M)
typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)
typeCheckᴴᴮ : H Γ M (Γ ⊢ᴴᴮ H M typeOfᴮ H Γ M)
typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)

View file

@ -1 +1,4 @@
false
ANNOTATED PROGRAM:
return true == false
RAN WITH RESULT: false

View file

@ -1 +1,4 @@
true
ANNOTATED PROGRAM:
return 1.0 == 1.0
RAN WITH RESULT: true

View file

@ -1 +1,4 @@
1.0
ANNOTATED PROGRAM:
return 1.0 + 2.0 - 2.0 * 2.0 / 2.0
RAN WITH RESULT: 1.0

View file

@ -1 +1,7 @@
nil
UNANNOTATED PROGRAM:
local function foo(x)
return nil
end
return foo(nil)
RAN WITH RESULT: nil

View file

@ -56,3 +56,9 @@ This document tracks unimplemented RFCs.
[RFC: Generalized iteration](https://github.com/Roblox/luau/blob/master/rfcs/generalized-iteration.md)
**Status**: Needs implementation
## table.clone
[RFC: table.clone](https://github.com/Roblox/luau/blob/master/rfcs/function-table-clone.md)
**Status**: Needs implementation

View file

@ -0,0 +1,64 @@
# table.clone
## Summary
Add `table.clone` function that, given a table, produces a copy of that table with the same keys/values/metatable.
## Motivation
There are multiple cases today when cloning tables is a useful operation.
- When working with tables as data containers, some algorithms may require modifying the table that can't be done in place for some reason.
- When working with tables as objects, it can be useful to obtain an identical copy of the object for further modification, preserving the metatable.
- When working with immutable data structures, any modification needs to clone some parts of the data structure to produce a new version of the object.
While it's possible to implement this function in user code today, it's impossible to implement it with maximum efficiency; furthermore, cloning is a reasonably fundamental
operation so from the ergonomics perspective it can be expected to be provided by the standard library.
## Design
`table.clone(t)` takes a table, `t`, and returns a new table that:
- has the same metatable
- has the same keys and values
- is not frozen, even if `t` was
The copy is shallow: implementing a deep recursive copy automatically is challenging (for similar reasons why we decided to avoid this in `table.freeze`), and often only certain keys need to be cloned recursively which can be done after the initial clone.
The table can be modified after cloning; as such, functions that compute a slightly modified copy of the table can be easily built on top of `table.clone`.
`table.clone(t)` is functionally equivalent to the following code, but it's more ergonomic (on the account of being built-in) and significantly faster:
```lua
assert(type(t) == "table")
local nt = {}
for k,v in pairs(t) do
nt[k] = v
end
if type(getmetatable(t)) == "table" then
setmetatable(nt, getmetatable(t))
end
```
The reason why `table.clone` can be dramatically more efficient is that it can directly copy the internal structure, preserving capacity and exact key order, and is thus
limited purely by memory bandwidth. In comparison, the code above can't predict the table size ahead of time, has to recreate the internal table structure one key at a time,
and bears the interpreter overhead (which can be avoided for numeric keys with `table.move` but that doesn't work for the general case of dictionaries).
Out of the abundance of caution, `table.clone` will fail to clone the table if it has a protected metatable. This is motivated by the fact that you can't do this today, so
there are no new potential vectors to escape various sandboxes. Superficially it seems like it's probably reasonable to allow cloning tables with protected metatables, but
there may be cases where code manufactures tables with unique protected metatables expecting 1-1 relationship and cloning would break that, so for now this RFC proposes a more
conservative route. We are likely to relax this restriction in the future.
## Drawbacks
Adding a new function to `table` library theoretically increases complexity. In practice though, we already effectively implement `table.clone` internally for some VM optimizations, so exposing this to the users bears no cost.
Assigning a type to this function is a little difficult if we want to enforce the "argument must be a table" constraint. It's likely that we'll need to type this as `table.clone(T): T` for the time being, which is less precise.
## Alternatives
We can implement something similar to `Object.assign` from JavaScript instead, that simultaneously assigns extra keys. However, this won't be fundamentally more efficient than
assigning the keys afterwards, and can be implemented in user space. Additionally, we can later extend `clone` with an extra argument if we so choose, so this proposal is the
minimal viable one.
We can immediately remove the rule wrt protected metatables, as it's not clear that it's actually problematic to be able to clone tables with protected metatables.

View file

@ -2752,7 +2752,6 @@ TEST_CASE_FIXTURE(ACFixture, "autocomplete_on_string_singletons")
ScopedFastFlag sffs[] = {
{"LuauParseSingletonTypes", true},
{"LuauSingletonTypes", true},
{"LuauRefactorTypeVarQuestions", true},
};
check(R"(

View file

@ -837,7 +837,7 @@ TEST_CASE("ExceptionObject")
return ExceptionResult{false, ""};
};
auto reallocFunc = [](lua_State* L, void* /*ud*/, void* ptr, size_t /*osize*/, size_t nsize) -> void* {
auto reallocFunc = [](void* /*ud*/, void* ptr, size_t /*osize*/, size_t nsize) -> void* {
if (nsize == 0)
{
free(ptr);
@ -964,4 +964,53 @@ TEST_CASE("StringConversion")
runConformance("strconv.lua");
}
TEST_CASE("GCDump")
{
// internal function, declared in lgc.h - not exposed via lua.h
extern void luaC_dump(lua_State* L, void* file, const char* (*categoryName)(lua_State* L, uint8_t memcat));
StateRef globalState(luaL_newstate(), lua_close);
lua_State* L = globalState.get();
// push various objects on stack to cover different paths
lua_createtable(L, 1, 2);
lua_pushstring(L, "value");
lua_setfield(L, -2, "key");
lua_pushinteger(L, 42);
lua_rawseti(L, -2, 1000);
lua_pushinteger(L, 42);
lua_rawseti(L, -2, 1);
lua_pushvalue(L, -1);
lua_setmetatable(L, -2);
lua_newuserdata(L, 42);
lua_pushvalue(L, -2);
lua_setmetatable(L, -2);
lua_pushinteger(L, 1);
lua_pushcclosure(L, lua_silence, "test", 1);
lua_State* CL = lua_newthread(L);
lua_pushstring(CL, "local x x = {} local function f() x[1] = math.abs(42) end function foo() coroutine.yield() end foo() return f");
lua_loadstring(CL);
lua_resume(CL, nullptr, 0);
#ifdef _WIN32
const char* path = "NUL";
#else
const char* path = "/dev/null";
#endif
FILE* f = fopen(path, "w");
REQUIRE(f);
luaC_dump(L, f, nullptr);
fclose(f);
}
TEST_SUITE_END();

View file

@ -1594,4 +1594,17 @@ TEST_CASE_FIXTURE(Fixture, "WrongCommentMuteSelf")
REQUIRE_EQ(result.warnings.size(), 0); // --!nolint disables WrongComment lint :)
}
TEST_CASE_FIXTURE(Fixture, "DuplicateConditionsIfStatAndExpr")
{
LintResult result = lint(R"(
if if 1 then 2 else 3 then
elseif if 1 then 2 else 3 then
elseif if 0 then 5 else 4 then
end
)");
REQUIRE_EQ(result.warnings.size(), 1);
CHECK_EQ(result.warnings[0].text, "Condition has already been checked on line 2");
}
TEST_SUITE_END();

View file

@ -2575,7 +2575,6 @@ do end
TEST_CASE_FIXTURE(Fixture, "recover_expected_type_pack")
{
ScopedFastFlag luauParseTypeAliasDefaults{"LuauParseTypeAliasDefaults", true};
ScopedFastFlag luauParseRecoverTypePackEllipsis{"LuauParseRecoverTypePackEllipsis", true};
ParseResult result = tryParse(R"(
type Y<T..., U = T...> = (T...) -> U...

View file

@ -651,4 +651,19 @@ local a: Packed<number>
CHECK_EQ(code, transpile(code, {}, true).code);
}
TEST_CASE_FIXTURE(Fixture, "transpile_singleton_types")
{
ScopedFastFlag luauParseSingletonTypes{"LuauParseSingletonTypes", true};
std::string code = R"(
type t1 = 'hello'
type t2 = true
type t3 = ''
type t4 = false
)";
CHECK_EQ(code, transpile(code, {}, true).code);
}
TEST_SUITE_END();

View file

@ -175,6 +175,8 @@ TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_with_property_guarante
TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_works_at_arbitrary_depth")
{
ScopedFastFlag sff{"LuauDoNotTryToReduce", true};
CheckResult result = check(R"(
type A = {x: {y: {z: {thing: string}}}}
type B = {x: {y: {z: {thing: string}}}}
@ -184,7 +186,7 @@ TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_works_at_arbitrary_dep
)");
LUAU_REQUIRE_NO_ERRORS(result);
CHECK_EQ(*typeChecker.stringType, *requireType("r"));
CHECK_EQ("string & string", toString(requireType("r")));
}
TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_with_mixed_types")
@ -218,7 +220,7 @@ TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_with_one_part_missing_
TEST_CASE_FIXTURE(Fixture, "index_on_an_intersection_type_with_one_property_of_type_any")
{
CheckResult result = check(R"(
type A = {x: number}
type A = {y: number}
type B = {x: any}
local t: A & B

View file

@ -1115,6 +1115,22 @@ TEST_CASE_FIXTURE(Fixture, "discriminate_on_properties_of_disjoint_tables_where_
LUAU_REQUIRE_NO_ERRORS(result);
}
TEST_CASE_FIXTURE(Fixture, "refine_a_property_not_to_be_nil_through_an_intersection_table")
{
ScopedFastFlag sff{"LuauDoNotTryToReduce", true};
CheckResult result = check(R"(
type T = {} & {f: ((string) -> string)?}
local function f(t: T, x)
if t.f then
t.f(x)
end
end
)");
LUAU_REQUIRE_NO_ERRORS(result);
}
TEST_CASE_FIXTURE(RefinementClassFixture, "discriminate_from_isa_of_x")
{
ScopedFastFlag sff[] = {

View file

@ -439,4 +439,128 @@ local a: Animal = if true then { tag = 'cat', catfood = 'something' } else { tag
LUAU_REQUIRE_NO_ERRORS(result);
}
TEST_CASE_FIXTURE(Fixture, "widen_the_supertype_if_it_is_free_and_subtype_has_singleton")
{
ScopedFastFlag sff[]{
{"LuauSingletonTypes", true},
{"LuauEqConstraint", true},
{"LuauDiscriminableUnions2", true},
{"LuauWidenIfSupertypeIsFree", true},
{"LuauWeakEqConstraint", false},
};
CheckResult result = check(R"(
local function foo(f, x)
if x == "hi" then
f(x)
f("foo")
end
end
)");
LUAU_REQUIRE_NO_ERRORS(result);
CHECK_EQ(R"("hi")", toString(requireTypeAtPosition({3, 18})));
// should be <a...>((string) -> a..., string) -> () but needs lower bounds calculation
CHECK_EQ("<a, b...>((string) -> (b...), a) -> ()", toString(requireType("foo")));
}
// TEST_CASE_FIXTURE(Fixture, "return_type_of_f_is_not_widened")
// {
// ScopedFastFlag sff[]{
// {"LuauParseSingletonTypes", true},
// {"LuauSingletonTypes", true},
// {"LuauDiscriminableUnions2", true},
// {"LuauEqConstraint", true},
// {"LuauWidenIfSupertypeIsFree", true},
// {"LuauWeakEqConstraint", false},
// };
// CheckResult result = check(R"(
// local function foo(f, x): "hello"? -- anyone there?
// return if x == "hi"
// then f(x)
// else nil
// end
// )");
// LUAU_REQUIRE_NO_ERRORS(result);
// CHECK_EQ(R"("hi")", toString(requireTypeAtPosition({3, 23})));
// CHECK_EQ(R"(<a, b...>((string) -> ("hello"?, b...), a) -> "hello"?)", toString(requireType("foo")));
// }
TEST_CASE_FIXTURE(Fixture, "widening_happens_almost_everywhere")
{
ScopedFastFlag sff[]{
{"LuauParseSingletonTypes", true},
{"LuauSingletonTypes", true},
{"LuauWidenIfSupertypeIsFree", true},
};
CheckResult result = check(R"(
local foo: "foo" = "foo"
local copy = foo
)");
LUAU_REQUIRE_NO_ERRORS(result);
CHECK_EQ("string", toString(requireType("copy")));
}
TEST_CASE_FIXTURE(Fixture, "widening_happens_almost_everywhere_except_for_tables")
{
ScopedFastFlag sff[]{
{"LuauParseSingletonTypes", true},
{"LuauSingletonTypes", true},
{"LuauDiscriminableUnions2", true},
{"LuauWidenIfSupertypeIsFree", true},
};
CheckResult result = check(R"(
type Cat = {tag: "Cat", meows: boolean}
type Dog = {tag: "Dog", barks: boolean}
type Animal = Cat | Dog
local function f(tag: "Cat" | "Dog"): Animal?
if tag == "Cat" then
local result = {tag = tag, meows = true}
return result
elseif tag == "Dog" then
local result = {tag = tag, barks = true}
return result
else
return nil
end
end
)");
LUAU_REQUIRE_NO_ERRORS(result);
}
TEST_CASE_FIXTURE(Fixture, "table_insert_with_a_singleton_argument")
{
ScopedFastFlag sff[]{
{"LuauParseSingletonTypes", true},
{"LuauSingletonTypes", true},
{"LuauWidenIfSupertypeIsFree", true},
};
CheckResult result = check(R"(
local function foo(t, x)
if x == "hi" or x == "bye" then
table.insert(t, x)
end
return t
end
local t = foo({}, "hi")
table.insert(t, "totally_unrelated_type" :: "totally_unrelated_type")
)");
LUAU_REQUIRE_NO_ERRORS(result);
CHECK_EQ("{string}", toString(requireType("t")));
}
TEST_SUITE_END();

View file

@ -2239,4 +2239,22 @@ TEST_CASE_FIXTURE(Fixture, "give_up_after_one_metatable_index_look_up")
CHECK_EQ("Type 't2' does not have key 'x'", toString(result.errors[0]));
}
TEST_CASE_FIXTURE(Fixture, "confusing_indexing")
{
ScopedFastFlag sff{"LuauDoNotTryToReduce", true};
CheckResult result = check(R"(
type T = {} & {p: number | string}
local function f(t: T)
return t.p
end
local foo = f({p = "string"})
)");
LUAU_REQUIRE_NO_ERRORS(result);
CHECK_EQ("number | string", toString(requireType("foo")));
}
TEST_SUITE_END();

View file

@ -5127,8 +5127,6 @@ TEST_CASE_FIXTURE(Fixture, "cli_50041_committing_txnlog_in_apollo_client_error")
TEST_CASE_FIXTURE(Fixture, "do_not_modify_imported_types")
{
ScopedFastFlag noSealedTypeMod{"LuauNoSealedTypeMod", true};
fileResolver.source["game/A"] = R"(
export type Type = { unrelated: boolean }
return {}
@ -5190,7 +5188,6 @@ TEST_CASE_FIXTURE(Fixture, "indexing_on_string_singletons")
{
ScopedFastFlag sff[]{
{"LuauDiscriminableUnions2", true},
{"LuauRefactorTypeVarQuestions", true},
{"LuauSingletonTypes", true},
};
@ -5210,7 +5207,6 @@ TEST_CASE_FIXTURE(Fixture, "indexing_on_union_of_string_singletons")
{
ScopedFastFlag sff[]{
{"LuauDiscriminableUnions2", true},
{"LuauRefactorTypeVarQuestions", true},
{"LuauSingletonTypes", true},
};
@ -5230,7 +5226,6 @@ TEST_CASE_FIXTURE(Fixture, "taking_the_length_of_string_singleton")
{
ScopedFastFlag sff[]{
{"LuauDiscriminableUnions2", true},
{"LuauRefactorTypeVarQuestions", true},
{"LuauSingletonTypes", true},
};
@ -5250,7 +5245,6 @@ TEST_CASE_FIXTURE(Fixture, "taking_the_length_of_union_of_string_singleton")
{
ScopedFastFlag sff[]{
{"LuauDiscriminableUnions2", true},
{"LuauRefactorTypeVarQuestions", true},
{"LuauSingletonTypes", true},
};

View file

@ -19,7 +19,7 @@ struct TryUnifyFixture : Fixture
ScopePtr globalScope{new Scope{arena.addTypePack({TypeId{}})}};
InternalErrorReporter iceHandler;
UnifierSharedState unifierState{&iceHandler};
Unifier state{&arena, Mode::Strict, globalScope, Location{}, Variance::Covariant, unifierState};
Unifier state{&arena, Mode::Strict, Location{}, Variance::Covariant, unifierState};
};
TEST_SUITE_BEGIN("TryUnifyTests");
@ -261,8 +261,6 @@ TEST_CASE_FIXTURE(TryUnifyFixture, "free_tail_is_grown_properly")
TEST_CASE_FIXTURE(TryUnifyFixture, "recursive_metatable_getmatchtag")
{
ScopedFastFlag luauUnionTagMatchFix{"LuauUnionTagMatchFix", true};
TypeVar redirect{FreeTypeVar{TypeLevel{}}};
TypeVar table{TableTypeVar{}};
TypeVar metatable{MetatableTypeVar{&redirect, &table}};

View file

@ -361,16 +361,12 @@ local b: (T, T, T) -> T
TEST_CASE("isString_on_string_singletons")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar helloString{SingletonTypeVar{StringSingleton{"hello"}}};
CHECK(isString(&helloString));
}
TEST_CASE("isString_on_unions_of_various_string_singletons")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar helloString{SingletonTypeVar{StringSingleton{"hello"}}};
TypeVar byeString{SingletonTypeVar{StringSingleton{"bye"}}};
TypeVar union_{UnionTypeVar{{&helloString, &byeString}}};
@ -380,8 +376,6 @@ TEST_CASE("isString_on_unions_of_various_string_singletons")
TEST_CASE("proof_that_isString_uses_all_of")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar helloString{SingletonTypeVar{StringSingleton{"hello"}}};
TypeVar byeString{SingletonTypeVar{StringSingleton{"bye"}}};
TypeVar booleanType{PrimitiveTypeVar{PrimitiveTypeVar::Boolean}};
@ -392,16 +386,12 @@ TEST_CASE("proof_that_isString_uses_all_of")
TEST_CASE("isBoolean_on_boolean_singletons")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar trueBool{SingletonTypeVar{BooleanSingleton{true}}};
CHECK(isBoolean(&trueBool));
}
TEST_CASE("isBoolean_on_unions_of_true_or_false_singletons")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar trueBool{SingletonTypeVar{BooleanSingleton{true}}};
TypeVar falseBool{SingletonTypeVar{BooleanSingleton{false}}};
TypeVar union_{UnionTypeVar{{&trueBool, &falseBool}}};
@ -411,8 +401,6 @@ TEST_CASE("isBoolean_on_unions_of_true_or_false_singletons")
TEST_CASE("proof_that_isBoolean_uses_all_of")
{
ScopedFastFlag sff{"LuauRefactorTypeVarQuestions", true};
TypeVar trueBool{SingletonTypeVar{BooleanSingleton{true}}};
TypeVar falseBool{SingletonTypeVar{BooleanSingleton{false}}};
TypeVar stringType{PrimitiveTypeVar{PrimitiveTypeVar::String}};

View file

@ -183,13 +183,12 @@
<Expand>
<LinkedListItems>
<HeadPointer>openupval</HeadPointer>
<NextPointer>u.l.next</NextPointer>
<NextPointer>u.l.threadnext</NextPointer>
<ValueNode>this</ValueNode>
</LinkedListItems>
</Expand>
</Synthetic>
<Item Name="l_gt">l_gt</Item>
<Item Name="env">env</Item>
<Item Name="globals">gt</Item>
<Item Name="userdata">userdata</Item>
</Expand>
</Type>