Tidy up Checker.cc/Checker.hpp a bit
This commit is contained in:
parent
75e0ebc14b
commit
fd462f6d05
SSH key fingerprint:
SHA256:dIg0ywU1OP+ZYifrYxy8c5esO72cIKB+4/9wkZj1VaY
2 changed files with 380 additions and 386 deletions
|
|
@ -9,6 +9,7 @@
|
|||
#include "bolt/Type.hpp"
|
||||
#include "bolt/Support/Graph.hpp"
|
||||
|
||||
#include <cstdlib>
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
#include <vector>
|
||||
|
|
@ -181,7 +182,7 @@ namespace bolt {
|
|||
|
||||
std::unordered_map<ByteString, std::vector<InstanceDeclaration*>> InstanceMap;
|
||||
|
||||
// std::vector<InferContext*> Contexts;
|
||||
/// Inference context management
|
||||
|
||||
InferContext* ActiveContext;
|
||||
|
||||
|
|
@ -189,13 +190,16 @@ namespace bolt {
|
|||
void setContext(InferContext* Ctx);
|
||||
void popContext();
|
||||
|
||||
/**
|
||||
* The queue that is used during solving to store any unsolved constraints.
|
||||
*/
|
||||
std::deque<class Constraint*> Queue;
|
||||
|
||||
void addConstraint(Constraint* Constraint);
|
||||
|
||||
/**
|
||||
* Get the return type for the current context. If none could be found, the
|
||||
* program will abort.
|
||||
*/
|
||||
Type* getReturnType();
|
||||
|
||||
/// Type inference
|
||||
|
||||
void forwardDeclare(Node* Node);
|
||||
void forwardDeclareFunctionDeclaration(FunctionDeclaration* N, TVSet* TVs, ConstraintSet* Constraints);
|
||||
|
||||
|
|
@ -210,6 +214,8 @@ namespace bolt {
|
|||
|
||||
Constraint* convertToConstraint(ConstraintExpression* C);
|
||||
|
||||
/// Factory methods
|
||||
|
||||
TCon* createConType(ByteString Name);
|
||||
TVar* createTypeVar();
|
||||
TVarRigid* createRigidVar(ByteString Name);
|
||||
|
|
@ -219,12 +225,10 @@ namespace bolt {
|
|||
ConstraintSet* Constraints = new ConstraintSet
|
||||
);
|
||||
|
||||
void addBinding(ByteString Name, Scheme* Scm);
|
||||
/// Environment manipulation
|
||||
|
||||
Scheme* lookup(ByteString Name);
|
||||
|
||||
void initialize(Node* N);
|
||||
|
||||
/**
|
||||
* Looks up a type/variable and ensures that it is a monomorphic type.
|
||||
*
|
||||
|
|
@ -239,40 +243,21 @@ namespace bolt {
|
|||
*/
|
||||
Type* lookupMono(ByteString Name);
|
||||
|
||||
/**
|
||||
* Get the return type for the current context. If none could be found, the program will abort.
|
||||
*/
|
||||
Type* getReturnType();
|
||||
void addBinding(ByteString Name, Scheme* Scm);
|
||||
|
||||
Type* instantiate(Scheme* S, Node* Source);
|
||||
|
||||
std::vector<TypeclassContext> findInstanceContext(TCon* Ty, TypeclassId& Class);
|
||||
void propagateClasses(TypeclassContext& Classes, Type* Ty);
|
||||
void propagateClassTycon(TypeclassId& Class, TCon* Ty);
|
||||
|
||||
// TODO Remove this
|
||||
Node* Source;
|
||||
/// Constraint solving
|
||||
|
||||
/**
|
||||
* Assign a type to a unification variable.
|
||||
*
|
||||
* If there are class constraints, those are propagated.
|
||||
*
|
||||
* If this type variable is solved during inference, it will be removed from
|
||||
* the inference context.
|
||||
*
|
||||
* Other side effects may occur.
|
||||
* The queue that is used during solving to store any unsolved constraints.
|
||||
*/
|
||||
void join(TVar* A, Type* B);
|
||||
std::deque<class Constraint*> Queue;
|
||||
|
||||
bool unify(Type* A, Type* B);
|
||||
|
||||
void unifyError();
|
||||
|
||||
void solveCEqual(CEqual* C);
|
||||
void solveEqual(CEqual* C);
|
||||
|
||||
void solve(Constraint* Constraint);
|
||||
|
||||
/// Helpers
|
||||
|
||||
void populate(SourceFile* SF);
|
||||
|
||||
/**
|
||||
|
|
@ -281,6 +266,10 @@ namespace bolt {
|
|||
*/
|
||||
void checkTypeclassSigs(Node* N);
|
||||
|
||||
Type* instantiate(Scheme* S, Node* Source);
|
||||
|
||||
void initialize(Node* N);
|
||||
|
||||
public:
|
||||
|
||||
Checker(const LanguageConfig& Config, DiagnosticEngine& DE);
|
||||
|
|
|
|||
705
src/Checker.cc
705
src/Checker.cc
|
|
@ -227,7 +227,7 @@ namespace bolt {
|
|||
}
|
||||
|
||||
if (MaxLevel == MinLevel || MaxLevelLeft == 0 || MaxLevelRight == 0) {
|
||||
solveCEqual(Y);
|
||||
solveEqual(Y);
|
||||
} else {
|
||||
Contexts[Contexts.size() - MaxLevel - 1]->Constraints->push_back(C);
|
||||
}
|
||||
|
|
@ -1307,26 +1307,42 @@ namespace bolt {
|
|||
auto TVs = new TVSet;
|
||||
auto Constraints = new ConstraintSet;
|
||||
for (auto N: Nodes) {
|
||||
if (N->getKind() != NodeKind::FunctionDeclaration) {
|
||||
continue;
|
||||
}
|
||||
auto Decl = static_cast<FunctionDeclaration*>(N);
|
||||
forwardDeclareFunctionDeclaration(Decl, TVs, Constraints);
|
||||
}
|
||||
}
|
||||
for (auto Nodes: SCCs) {
|
||||
for (auto N: Nodes) {
|
||||
if (N->getKind() != NodeKind::FunctionDeclaration) {
|
||||
continue;
|
||||
}
|
||||
auto Decl = static_cast<FunctionDeclaration*>(N);
|
||||
Decl->IsCycleActive = true;
|
||||
}
|
||||
for (auto N: Nodes) {
|
||||
if (N->getKind() != NodeKind::FunctionDeclaration) {
|
||||
continue;
|
||||
}
|
||||
auto Decl = static_cast<FunctionDeclaration*>(N);
|
||||
inferFunctionDeclaration(Decl);
|
||||
}
|
||||
for (auto N: Nodes) {
|
||||
if (N->getKind() != NodeKind::FunctionDeclaration) {
|
||||
continue;
|
||||
}
|
||||
auto Decl = static_cast<FunctionDeclaration*>(N);
|
||||
Decl->IsCycleActive = false;
|
||||
}
|
||||
}
|
||||
setContext(SF->Ctx);
|
||||
infer(SF);
|
||||
|
||||
// Important because otherwise some logic for some optimisations will kick in that are no longer active.
|
||||
ActiveContext = nullptr;
|
||||
|
||||
solve(new CMany(*SF->Ctx->Constraints));
|
||||
checkTypeclassSigs(SF);
|
||||
}
|
||||
|
|
@ -1362,7 +1378,7 @@ namespace bolt {
|
|||
|
||||
case ConstraintKind::Equal:
|
||||
{
|
||||
solveCEqual(static_cast<CEqual*>(Constraint));
|
||||
solveEqual(static_cast<CEqual*>(Constraint));
|
||||
break;
|
||||
}
|
||||
|
||||
|
|
@ -1391,81 +1407,6 @@ namespace bolt {
|
|||
ZEN_UNREACHABLE
|
||||
}
|
||||
|
||||
std::vector<TypeclassContext> Checker::findInstanceContext(TCon* Ty, TypeclassId& Class) {
|
||||
auto Match = InstanceMap.find(Class);
|
||||
std::vector<TypeclassContext> S;
|
||||
if (Match != InstanceMap.end()) {
|
||||
for (auto Instance: Match->second) {
|
||||
if (assignableTo(Ty, Instance->TypeExps[0]->getType())) {
|
||||
std::vector<TypeclassContext> S;
|
||||
// TODO handle TApp
|
||||
// for (auto Arg: Ty->Args) {
|
||||
// TypeclassContext Classes;
|
||||
// // TODO
|
||||
// S.push_back(Classes);
|
||||
// }
|
||||
return S;
|
||||
}
|
||||
}
|
||||
}
|
||||
DE.add<InstanceNotFoundDiagnostic>(Class, Ty, Source);
|
||||
// TODO handle TApp
|
||||
// for (auto Arg: Ty->Args) {
|
||||
// S.push_back({});
|
||||
// }
|
||||
return S;
|
||||
}
|
||||
|
||||
void Checker::propagateClasses(std::unordered_set<TypeclassId>& Classes, Type* Ty) {
|
||||
if (llvm::isa<TVar>(Ty)) {
|
||||
auto TV = llvm::cast<TVar>(Ty);
|
||||
for (auto Class: Classes) {
|
||||
TV->Contexts.emplace(Class);
|
||||
}
|
||||
} else if (llvm::isa<TCon>(Ty)) {
|
||||
for (auto Class: Classes) {
|
||||
propagateClassTycon(Class, llvm::cast<TCon>(Ty));
|
||||
}
|
||||
} else if (!Classes.empty()) {
|
||||
DE.add<InvalidTypeToTypeclassDiagnostic>(Ty, std::vector(Classes.begin(), Classes.end()), Source);
|
||||
}
|
||||
};
|
||||
|
||||
void Checker::propagateClassTycon(TypeclassId& Class, TCon* Ty) {
|
||||
auto S = findInstanceContext(Ty, Class);
|
||||
// TODO handle TApp
|
||||
// for (auto [Classes, Arg]: zen::zip(S, Ty->Args)) {
|
||||
// propagateClasses(Classes, Arg);
|
||||
// }
|
||||
};
|
||||
|
||||
void Checker::join(TVar* TV, Type* Ty) {
|
||||
|
||||
// std::cerr << describe(TV) << " => " << describe(Ty) << std::endl;
|
||||
|
||||
TV->set(Ty);
|
||||
|
||||
propagateClasses(TV->Contexts, Ty);
|
||||
|
||||
// This is a very specific adjustment that is critical to the
|
||||
// well-functioning of the infer/unify algorithm. When addConstraint() is
|
||||
// called, it may decide to solve the constraint immediately during
|
||||
// inference. If this happens, a type variable might get assigned a concrete
|
||||
// type such as Int. We therefore never want the variable to be polymorphic
|
||||
// and be instantiated with a fresh variable, as that would allow Bool to
|
||||
// collide with Int.
|
||||
//
|
||||
// Should it get assigned another unification variable, that's OK too
|
||||
// because then that variable is what matters and it will become the new
|
||||
// (possibly polymorphic) variable.
|
||||
if (ActiveContext) {
|
||||
// std::cerr << "erase " << describe(TV) << std::endl;
|
||||
auto TVs = ActiveContext->TVs;
|
||||
TVs->erase(TV);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
class ArrowCursor {
|
||||
|
||||
std::stack<std::tuple<TArrow*, bool>> Stack;
|
||||
|
|
@ -1531,76 +1472,154 @@ namespace bolt {
|
|||
return Constraint->Source;
|
||||
}
|
||||
|
||||
bool unify(Type* A, Type* B);
|
||||
bool unify(Type* A, Type* B, bool DidSwap);
|
||||
|
||||
bool unifyField(Type* A, Type* B);
|
||||
|
||||
bool unify() {
|
||||
return unify(Constraint->Left, Constraint->Right);
|
||||
return unify(Constraint->Left, Constraint->Right, false);
|
||||
}
|
||||
|
||||
std::vector<TypeclassContext> findInstanceContext(TCon* Ty, TypeclassId& Class) {
|
||||
auto Match = C.InstanceMap.find(Class);
|
||||
std::vector<TypeclassContext> S;
|
||||
if (Match != C.InstanceMap.end()) {
|
||||
for (auto Instance: Match->second) {
|
||||
if (assignableTo(Ty, Instance->TypeExps[0]->getType())) {
|
||||
std::vector<TypeclassContext> S;
|
||||
// TODO handle TApp
|
||||
// for (auto Arg: Ty->Args) {
|
||||
// TypeclassContext Classes;
|
||||
// // TODO
|
||||
// S.push_back(Classes);
|
||||
// }
|
||||
return S;
|
||||
}
|
||||
}
|
||||
}
|
||||
C.DE.add<InstanceNotFoundDiagnostic>(Class, Ty, getSource());
|
||||
// TODO handle TApp
|
||||
// for (auto Arg: Ty->Args) {
|
||||
// S.push_back({});
|
||||
// }
|
||||
return S;
|
||||
}
|
||||
|
||||
void propagateClasses(std::unordered_set<TypeclassId>& Classes, Type* Ty) {
|
||||
if (llvm::isa<TVar>(Ty)) {
|
||||
auto TV = llvm::cast<TVar>(Ty);
|
||||
for (auto Class: Classes) {
|
||||
TV->Contexts.emplace(Class);
|
||||
}
|
||||
} else if (llvm::isa<TCon>(Ty)) {
|
||||
for (auto Class: Classes) {
|
||||
propagateClassTycon(Class, llvm::cast<TCon>(Ty));
|
||||
}
|
||||
} else if (!Classes.empty()) {
|
||||
C.DE.add<InvalidTypeToTypeclassDiagnostic>(Ty, std::vector(Classes.begin(), Classes.end()), getSource());
|
||||
}
|
||||
};
|
||||
|
||||
void propagateClassTycon(TypeclassId& Class, TCon* Ty) {
|
||||
auto S = findInstanceContext(Ty, Class);
|
||||
// TODO handle TApp
|
||||
// for (auto [Classes, Arg]: zen::zip(S, Ty->Args)) {
|
||||
// propagateClasses(Classes, Arg);
|
||||
// }
|
||||
};
|
||||
|
||||
/**
|
||||
* Assign a type to a unification variable.
|
||||
*
|
||||
* If there are class constraints, those are propagated.
|
||||
*
|
||||
* If this type variable is solved during inference, it will be removed from
|
||||
* the inference context.
|
||||
*
|
||||
* Other side effects may occur.
|
||||
*/
|
||||
void join(TVar* TV, Type* Ty) {
|
||||
|
||||
// std::cerr << describe(TV) << " => " << describe(Ty) << std::endl;
|
||||
|
||||
TV->set(Ty);
|
||||
|
||||
propagateClasses(TV->Contexts, Ty);
|
||||
|
||||
// This is a very specific adjustment that is critical to the
|
||||
// well-functioning of the infer/unify algorithm. When addConstraint() is
|
||||
// called, it may decide to solve the constraint immediately during
|
||||
// inference. If this happens, a type variable might get assigned a concrete
|
||||
// type such as Int. We therefore never want the variable to be polymorphic
|
||||
// and be instantiated with a fresh variable, as that would allow Bool to
|
||||
// collide with Int.
|
||||
//
|
||||
// Should it get assigned another unification variable, that's OK too
|
||||
// because then that variable is what matters and it will become the new
|
||||
// (possibly polymorphic) variable.
|
||||
if (C.ActiveContext) {
|
||||
// std::cerr << "erase " << describe(TV) << std::endl;
|
||||
auto TVs = C.ActiveContext->TVs;
|
||||
TVs->erase(TV);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
class UnificationFrame {
|
||||
bool Unifier::unify(Type* A, Type* B, bool DidSwap) {
|
||||
|
||||
Unifier& U;
|
||||
Type* A;
|
||||
Type* B;
|
||||
bool DidSwap = false;
|
||||
A = C.simplifyType(A);
|
||||
B = C.simplifyType(B);
|
||||
|
||||
public:
|
||||
|
||||
UnificationFrame(Unifier& U, Type* A, Type* B):
|
||||
U(U), A(U.C.simplifyType(A)), B(U.C.simplifyType(B)) {}
|
||||
|
||||
void unifyError() {
|
||||
U.C.DE.add<UnificationErrorDiagnostic>(
|
||||
U.C.simplifyType(U.Constraint->Left),
|
||||
U.C.simplifyType(U.Constraint->Right),
|
||||
U.LeftPath,
|
||||
U.RightPath,
|
||||
U.Constraint->Source
|
||||
auto unifyError = [&]() {
|
||||
C.DE.add<UnificationErrorDiagnostic>(
|
||||
C.simplifyType(Constraint->Left),
|
||||
C.simplifyType(Constraint->Right),
|
||||
LeftPath,
|
||||
RightPath,
|
||||
Constraint->Source
|
||||
);
|
||||
}
|
||||
};
|
||||
|
||||
void pushLeft(TypeIndex I) {
|
||||
auto pushLeft = [&](TypeIndex I) {
|
||||
if (DidSwap) {
|
||||
U.RightPath.push_back(I);
|
||||
RightPath.push_back(I);
|
||||
} else {
|
||||
U.LeftPath.push_back(I);
|
||||
LeftPath.push_back(I);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void popLeft() {
|
||||
auto popLeft = [&]() {
|
||||
if (DidSwap) {
|
||||
U.RightPath.pop_back();
|
||||
RightPath.pop_back();
|
||||
} else {
|
||||
U.LeftPath.pop_back();
|
||||
LeftPath.pop_back();
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void pushRight(TypeIndex I) {
|
||||
auto pushRight = [&](TypeIndex I) {
|
||||
if (DidSwap) {
|
||||
U.LeftPath.push_back(I);
|
||||
LeftPath.push_back(I);
|
||||
} else {
|
||||
U.RightPath.push_back(I);
|
||||
RightPath.push_back(I);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void popRight() {
|
||||
auto popRight = [&]() {
|
||||
if (DidSwap) {
|
||||
U.LeftPath.pop_back();
|
||||
LeftPath.pop_back();
|
||||
} else {
|
||||
U.RightPath.pop_back();
|
||||
RightPath.pop_back();
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void swap() {
|
||||
auto swap = [&]() {
|
||||
std::swap(A, B);
|
||||
DidSwap = !DidSwap;
|
||||
}
|
||||
};
|
||||
|
||||
bool unifyField() {
|
||||
auto unifyField = [&](Type* A, Type* B) {
|
||||
if (llvm::isa<TAbsent>(A) && llvm::isa<TAbsent>(B)) {
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1609,251 +1628,237 @@ namespace bolt {
|
|||
}
|
||||
if (llvm::isa<TAbsent>(A)) {
|
||||
auto Present = static_cast<TPresent*>(B);
|
||||
U.C.DE.add<FieldNotFoundDiagnostic>(U.CurrentFieldName, U.C.simplifyType(U.getLeft()), U.LeftPath, U.getSource());
|
||||
C.DE.add<FieldNotFoundDiagnostic>(CurrentFieldName, C.simplifyType(getLeft()), LeftPath, getSource());
|
||||
return false;
|
||||
}
|
||||
auto Present1 = static_cast<TPresent*>(A);
|
||||
auto Present2 = static_cast<TPresent*>(B);
|
||||
return U.unify(Present1->Ty, Present2->Ty);
|
||||
return unify(Present1->Ty, Present2->Ty, DidSwap);
|
||||
};
|
||||
|
||||
if (llvm::isa<TVar>(A) && llvm::isa<TVar>(B)) {
|
||||
auto Var1 = static_cast<TVar*>(A);
|
||||
auto Var2 = static_cast<TVar*>(B);
|
||||
if (Var1->getVarKind() == VarKind::Rigid && Var2->getVarKind() == VarKind::Rigid) {
|
||||
if (Var1->Id != Var2->Id) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
TVar* To;
|
||||
TVar* From;
|
||||
if (Var1->getVarKind() == VarKind::Rigid && Var2->getVarKind() == VarKind::Unification) {
|
||||
To = Var1;
|
||||
From = Var2;
|
||||
} else {
|
||||
// Only cases left are Var1 = Unification, Var2 = Rigid and Var1 = Unification, Var2 = Unification
|
||||
// Either way, Var1, being Unification, is a good candidate for being unified away
|
||||
To = Var2;
|
||||
From = Var1;
|
||||
}
|
||||
if (From->Id != To->Id) {
|
||||
join(From, To);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool unify() {
|
||||
|
||||
if (llvm::isa<TVar>(A) && llvm::isa<TVar>(B)) {
|
||||
auto Var1 = static_cast<TVar*>(A);
|
||||
auto Var2 = static_cast<TVar*>(B);
|
||||
if (Var1->getVarKind() == VarKind::Rigid && Var2->getVarKind() == VarKind::Rigid) {
|
||||
if (Var1->Id != Var2->Id) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
TVar* To;
|
||||
TVar* From;
|
||||
if (Var1->getVarKind() == VarKind::Rigid && Var2->getVarKind() == VarKind::Unification) {
|
||||
To = Var1;
|
||||
From = Var2;
|
||||
} else {
|
||||
// Only cases left are Var1 = Unification, Var2 = Rigid and Var1 = Unification, Var2 = Unification
|
||||
// Either way, Var1, being Unification, is a good candidate for being unified away
|
||||
To = Var2;
|
||||
From = Var1;
|
||||
}
|
||||
if (From->Id != To->Id) {
|
||||
U.C.join(From, To);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TVar>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
if (llvm::isa<TVar>(A)) {
|
||||
|
||||
auto TV = static_cast<TVar*>(A);
|
||||
|
||||
// Rigid type variables can never unify with antything else than what we
|
||||
// have already handled in the previous if-statement, so issue an error.
|
||||
if (TV->getVarKind() == VarKind::Rigid) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
|
||||
// Occurs check
|
||||
if (B->hasTypeVar(TV)) {
|
||||
// NOTE Just like GHC, we just display an error message indicating that
|
||||
// A cannot match B, e.g. a cannot match [a]. It looks much better
|
||||
// than obsure references to an occurs check
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
|
||||
U.C.join(TV, B);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(A) && llvm::isa<TArrow>(B)) {
|
||||
auto C1 = ArrowCursor(static_cast<TArrow*>(A), DidSwap ? U.RightPath : U.LeftPath);
|
||||
auto C2 = ArrowCursor(static_cast<TArrow*>(B), DidSwap ? U.LeftPath : U.RightPath);
|
||||
bool Success = true;
|
||||
for (;;) {
|
||||
auto T1 = C1.next();
|
||||
auto T2 = C2.next();
|
||||
if (T1 == nullptr && T2 == nullptr) {
|
||||
break;
|
||||
}
|
||||
if (T1 == nullptr || T2 == nullptr) {
|
||||
unifyError();
|
||||
Success = false;
|
||||
break;
|
||||
}
|
||||
if (!U.unify(T1, T2)) {
|
||||
Success = false;
|
||||
}
|
||||
}
|
||||
return Success;
|
||||
/* if (Arr1->ParamTypes.size() != Arr2->ParamTypes.size()) { */
|
||||
/* return false; */
|
||||
/* } */
|
||||
/* auto Count = Arr1->ParamTypes.size(); */
|
||||
/* for (std::size_t I = 0; I < Count; I++) { */
|
||||
/* if (!unify(Arr1->ParamTypes[I], Arr2->ParamTypes[I], Solution)) { */
|
||||
/* return false; */
|
||||
/* } */
|
||||
/* } */
|
||||
/* return unify(Arr1->ReturnType, Arr2->ReturnType, Solution); */
|
||||
}
|
||||
|
||||
if (llvm::isa<TApp>(A) && llvm::isa<TApp>(B)) {
|
||||
auto App1 = static_cast<TApp*>(A);
|
||||
auto App2 = static_cast<TApp*>(B);
|
||||
bool Success = true;
|
||||
if (!U.unify(App1->Op, App2->Op)) {
|
||||
Success = false;
|
||||
}
|
||||
if (!U.unify(App1->Arg, App2->Arg)) {
|
||||
Success = false;
|
||||
}
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(A)) {
|
||||
auto Arr = static_cast<TArrow*>(A);
|
||||
if (Arr->ParamTypes.empty()) {
|
||||
auto Success = U.unify(Arr->ReturnType, B);
|
||||
return Success;
|
||||
}
|
||||
}
|
||||
|
||||
if (llvm::isa<TTuple>(A) && llvm::isa<TTuple>(B)) {
|
||||
auto Tuple1 = static_cast<TTuple*>(A);
|
||||
auto Tuple2 = static_cast<TTuple*>(B);
|
||||
if (Tuple1->ElementTypes.size() != Tuple2->ElementTypes.size()) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
auto Count = Tuple1->ElementTypes.size();
|
||||
bool Success = true;
|
||||
for (size_t I = 0; I < Count; I++) {
|
||||
U.LeftPath.push_back(TypeIndex::forTupleElement(I));
|
||||
U.RightPath.push_back(TypeIndex::forTupleElement(I));
|
||||
if (!U.unify(Tuple1->ElementTypes[I], Tuple2->ElementTypes[I])) {
|
||||
Success = false;
|
||||
}
|
||||
U.LeftPath.pop_back();
|
||||
U.RightPath.pop_back();
|
||||
}
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TTupleIndex>(A) || llvm::isa<TTupleIndex>(B)) {
|
||||
// Type(s) could not be simplified at the beginning of this function,
|
||||
// so we have to re-visit the constraint when there is more information.
|
||||
U.C.Queue.push_back(U.Constraint);
|
||||
return true;
|
||||
}
|
||||
|
||||
// if (llvm::isa<TTupleIndex>(A) && llvm::isa<TTupleIndex>(B)) {
|
||||
// auto Index1 = static_cast<TTupleIndex*>(A);
|
||||
// auto Index2 = static_cast<TTupleIndex*>(B);
|
||||
// return unify(Index1->Ty, Index2->Ty, Source);
|
||||
// }
|
||||
|
||||
if (llvm::isa<TCon>(A) && llvm::isa<TCon>(B)) {
|
||||
auto Con1 = static_cast<TCon*>(A);
|
||||
auto Con2 = static_cast<TCon*>(B);
|
||||
if (Con1->Id != Con2->Id) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TNil>(A) && llvm::isa<TNil>(B)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TField>(A) && llvm::isa<TField>(B)) {
|
||||
auto Field1 = static_cast<TField*>(A);
|
||||
auto Field2 = static_cast<TField*>(B);
|
||||
bool Success = true;
|
||||
if (Field1->Name == Field2->Name) {
|
||||
U.LeftPath.push_back(TypeIndex::forFieldType());
|
||||
U.RightPath.push_back(TypeIndex::forFieldType());
|
||||
U.CurrentFieldName = Field1->Name;
|
||||
if (!U.unifyField(Field1->Ty, Field2->Ty)) {
|
||||
Success = false;
|
||||
}
|
||||
U.LeftPath.pop_back();
|
||||
U.RightPath.pop_back();
|
||||
U.LeftPath.push_back(TypeIndex::forFieldRest());
|
||||
U.RightPath.push_back(TypeIndex::forFieldRest());
|
||||
if (!U.unify(Field1->RestTy, Field2->RestTy)) {
|
||||
Success = false;
|
||||
}
|
||||
U.LeftPath.pop_back();
|
||||
U.RightPath.pop_back();
|
||||
return Success;
|
||||
}
|
||||
auto NewRestTy = new TVar(U.C.NextTypeVarId++, VarKind::Unification);
|
||||
pushLeft(TypeIndex::forFieldRest());
|
||||
if (!U.unify(Field1->RestTy, new TField(Field2->Name, Field2->Ty, NewRestTy))) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
pushRight(TypeIndex::forFieldRest());
|
||||
if (!U.unify(new TField(Field1->Name, Field1->Ty, NewRestTy), Field2->RestTy)) {
|
||||
Success = false;
|
||||
}
|
||||
popRight();
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TNil>(A) && llvm::isa<TField>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
if (llvm::isa<TField>(A) && llvm::isa<TNil>(B)) {
|
||||
auto Field = static_cast<TField*>(A);
|
||||
bool Success = true;
|
||||
pushLeft(TypeIndex::forFieldType());
|
||||
U.CurrentFieldName = Field->Name;
|
||||
if (!U.unifyField(Field->Ty, new TAbsent)) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
pushLeft(TypeIndex::forFieldRest());
|
||||
if (!U.unify(Field->RestTy, B)) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
return Success;
|
||||
}
|
||||
|
||||
unifyError();
|
||||
return false;
|
||||
if (llvm::isa<TVar>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
};
|
||||
if (llvm::isa<TVar>(A)) {
|
||||
|
||||
bool Unifier::unify(Type* A, Type* B) {
|
||||
UnificationFrame Frame { *this, A, B };
|
||||
return Frame.unify();
|
||||
auto TV = static_cast<TVar*>(A);
|
||||
|
||||
// Rigid type variables can never unify with antything else than what we
|
||||
// have already handled in the previous if-statement, so issue an error.
|
||||
if (TV->getVarKind() == VarKind::Rigid) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
|
||||
// Occurs check
|
||||
if (B->hasTypeVar(TV)) {
|
||||
// NOTE Just like GHC, we just display an error message indicating that
|
||||
// A cannot match B, e.g. a cannot match [a]. It looks much better
|
||||
// than obsure references to an occurs check
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
|
||||
join(TV, B);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(A) && llvm::isa<TArrow>(B)) {
|
||||
auto C1 = ArrowCursor(static_cast<TArrow*>(A), DidSwap ? RightPath : LeftPath);
|
||||
auto C2 = ArrowCursor(static_cast<TArrow*>(B), DidSwap ? LeftPath : RightPath);
|
||||
bool Success = true;
|
||||
for (;;) {
|
||||
auto T1 = C1.next();
|
||||
auto T2 = C2.next();
|
||||
if (T1 == nullptr && T2 == nullptr) {
|
||||
break;
|
||||
}
|
||||
if (T1 == nullptr || T2 == nullptr) {
|
||||
unifyError();
|
||||
Success = false;
|
||||
break;
|
||||
}
|
||||
if (!unify(T1, T2, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
}
|
||||
return Success;
|
||||
/* if (Arr1->ParamTypes.size() != Arr2->ParamTypes.size()) { */
|
||||
/* return false; */
|
||||
/* } */
|
||||
/* auto Count = Arr1->ParamTypes.size(); */
|
||||
/* for (std::size_t I = 0; I < Count; I++) { */
|
||||
/* if (!unify(Arr1->ParamTypes[I], Arr2->ParamTypes[I], Solution)) { */
|
||||
/* return false; */
|
||||
/* } */
|
||||
/* } */
|
||||
/* return unify(Arr1->ReturnType, Arr2->ReturnType, Solution); */
|
||||
}
|
||||
|
||||
if (llvm::isa<TApp>(A) && llvm::isa<TApp>(B)) {
|
||||
auto App1 = static_cast<TApp*>(A);
|
||||
auto App2 = static_cast<TApp*>(B);
|
||||
bool Success = true;
|
||||
if (!unify(App1->Op, App2->Op, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
if (!unify(App1->Arg, App2->Arg, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
if (llvm::isa<TArrow>(A)) {
|
||||
auto Arr = static_cast<TArrow*>(A);
|
||||
if (Arr->ParamTypes.empty()) {
|
||||
auto Success = unify(Arr->ReturnType, B, DidSwap);
|
||||
return Success;
|
||||
}
|
||||
}
|
||||
|
||||
if (llvm::isa<TTuple>(A) && llvm::isa<TTuple>(B)) {
|
||||
auto Tuple1 = static_cast<TTuple*>(A);
|
||||
auto Tuple2 = static_cast<TTuple*>(B);
|
||||
if (Tuple1->ElementTypes.size() != Tuple2->ElementTypes.size()) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
auto Count = Tuple1->ElementTypes.size();
|
||||
bool Success = true;
|
||||
for (size_t I = 0; I < Count; I++) {
|
||||
LeftPath.push_back(TypeIndex::forTupleElement(I));
|
||||
RightPath.push_back(TypeIndex::forTupleElement(I));
|
||||
if (!unify(Tuple1->ElementTypes[I], Tuple2->ElementTypes[I], DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
LeftPath.pop_back();
|
||||
RightPath.pop_back();
|
||||
}
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TTupleIndex>(A) || llvm::isa<TTupleIndex>(B)) {
|
||||
// Type(s) could not be simplified at the beginning of this function,
|
||||
// so we have to re-visit the constraint when there is more information.
|
||||
C.Queue.push_back(Constraint);
|
||||
return true;
|
||||
}
|
||||
|
||||
// if (llvm::isa<TTupleIndex>(A) && llvm::isa<TTupleIndex>(B)) {
|
||||
// auto Index1 = static_cast<TTupleIndex*>(A);
|
||||
// auto Index2 = static_cast<TTupleIndex*>(B);
|
||||
// return unify(Index1->Ty, Index2->Ty, Source);
|
||||
// }
|
||||
|
||||
if (llvm::isa<TCon>(A) && llvm::isa<TCon>(B)) {
|
||||
auto Con1 = static_cast<TCon*>(A);
|
||||
auto Con2 = static_cast<TCon*>(B);
|
||||
if (Con1->Id != Con2->Id) {
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TNil>(A) && llvm::isa<TNil>(B)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (llvm::isa<TField>(A) && llvm::isa<TField>(B)) {
|
||||
auto Field1 = static_cast<TField*>(A);
|
||||
auto Field2 = static_cast<TField*>(B);
|
||||
bool Success = true;
|
||||
if (Field1->Name == Field2->Name) {
|
||||
LeftPath.push_back(TypeIndex::forFieldType());
|
||||
RightPath.push_back(TypeIndex::forFieldType());
|
||||
CurrentFieldName = Field1->Name;
|
||||
if (!unifyField(Field1->Ty, Field2->Ty)) {
|
||||
Success = false;
|
||||
}
|
||||
LeftPath.pop_back();
|
||||
RightPath.pop_back();
|
||||
LeftPath.push_back(TypeIndex::forFieldRest());
|
||||
RightPath.push_back(TypeIndex::forFieldRest());
|
||||
if (!unify(Field1->RestTy, Field2->RestTy, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
LeftPath.pop_back();
|
||||
RightPath.pop_back();
|
||||
return Success;
|
||||
}
|
||||
auto NewRestTy = new TVar(C.NextTypeVarId++, VarKind::Unification);
|
||||
pushLeft(TypeIndex::forFieldRest());
|
||||
if (!unify(Field1->RestTy, new TField(Field2->Name, Field2->Ty, NewRestTy), DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
pushRight(TypeIndex::forFieldRest());
|
||||
if (!unify(new TField(Field1->Name, Field1->Ty, NewRestTy), Field2->RestTy, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
popRight();
|
||||
return Success;
|
||||
}
|
||||
|
||||
if (llvm::isa<TNil>(A) && llvm::isa<TField>(B)) {
|
||||
swap();
|
||||
}
|
||||
|
||||
if (llvm::isa<TField>(A) && llvm::isa<TNil>(B)) {
|
||||
auto Field = static_cast<TField*>(A);
|
||||
bool Success = true;
|
||||
pushLeft(TypeIndex::forFieldType());
|
||||
CurrentFieldName = Field->Name;
|
||||
if (!unifyField(Field->Ty, new TAbsent)) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
pushLeft(TypeIndex::forFieldRest());
|
||||
if (!unify(Field->RestTy, B, DidSwap)) {
|
||||
Success = false;
|
||||
}
|
||||
popLeft();
|
||||
return Success;
|
||||
}
|
||||
|
||||
unifyError();
|
||||
return false;
|
||||
}
|
||||
|
||||
bool Unifier::unifyField(Type* A, Type* B) {
|
||||
UnificationFrame Frame { *this, A, B };
|
||||
return Frame.unifyField();
|
||||
}
|
||||
|
||||
void Checker::solveCEqual(CEqual* C) {
|
||||
void Checker::solveEqual(CEqual* C) {
|
||||
// std::cerr << describe(C->Left) << " ~ " << describe(C->Right) << std::endl;
|
||||
Unifier A { *this, C };
|
||||
A.unify();
|
||||
|
|
|
|||
Loading…
Reference in a new issue