@@ -49,10 +49,7 @@ std::vector<TypeEnvironment::UnificationFailure> TypeEnvironment::unify(Type _a,
49
49
std::visit (util::GenericVisitor{
50
50
[&](TypeVariable _left, TypeVariable _right) {
51
51
if (_left.index () == _right.index ())
52
- {
53
- if (_left.sort () != _right.sort ())
54
- unificationFailure ();
55
- }
52
+ solAssert (_left.sort () == _right.sort ());
56
53
else
57
54
{
58
55
if (_left.sort () <= _right.sort ())
@@ -154,7 +151,7 @@ TypeSystem::TypeSystem()
154
151
Sort typeSort{{classType}};
155
152
m_typeConstructors.at (m_primitiveTypeConstructors.at (PrimitiveType::TypeFunction).m_index ).arities = {Arity{std::vector<Sort>{{typeSort},{typeSort}}, classType}};
156
153
m_typeConstructors.at (m_primitiveTypeConstructors.at (PrimitiveType::Function).m_index ).arities = {Arity{std::vector<Sort>{{typeSort, typeSort}}, classType}};
157
- m_typeConstructors.at (m_primitiveTypeConstructors.at (PrimitiveType::Function ).m_index ).arities = {Arity{std::vector<Sort>{{typeSort, typeSort}}, classType}};
154
+ m_typeConstructors.at (m_primitiveTypeConstructors.at (PrimitiveType::Itself ).m_index ).arities = {Arity{std::vector<Sort>{{typeSort, typeSort}}, classType}};
158
155
}
159
156
160
157
experimental::Type TypeSystem::freshVariable (Sort _sort)
@@ -171,9 +168,10 @@ experimental::Type TypeSystem::freshTypeVariable(Sort _sort)
171
168
172
169
std::vector<TypeEnvironment::UnificationFailure> TypeEnvironment::instantiate (TypeVariable _variable, Type _type)
173
170
{
174
- for (auto typeVar: TypeEnvironmentHelpers{*this }.typeVars (_type))
175
- if (typeVar.index () == _variable.index ())
176
- return {UnificationFailure{RecursiveUnification{_variable, _type}}};
171
+ for (auto const & maybeTypeVar: TypeEnvironmentHelpers{*this }.typeVars (_type))
172
+ if (auto const * typeVar = std::get_if<TypeVariable>(&maybeTypeVar))
173
+ if (typeVar->index () == _variable.index ())
174
+ return {UnificationFailure{RecursiveUnification{_variable, _type}}};
177
175
Sort typeSort = sort (_type);
178
176
if (!(_variable.sort () <= typeSort))
179
177
{
@@ -197,19 +195,19 @@ experimental::Type TypeEnvironment::resolve(Type _type) const
197
195
experimental::Type TypeEnvironment::resolveRecursive (Type _type) const
198
196
{
199
197
return std::visit (util::GenericVisitor{
200
- [&](TypeConstant const & _type ) -> Type {
198
+ [&](TypeConstant const & _typeConstant ) -> Type {
201
199
return TypeConstant{
202
- _type .constructor ,
203
- _type .arguments | ranges::views::transform ([&](Type _argType) {
200
+ _typeConstant .constructor ,
201
+ _typeConstant .arguments | ranges::views::transform ([&](Type const & _argType) {
204
202
return resolveRecursive (_argType);
205
203
}) | ranges::to<std::vector<Type>>
206
204
};
207
205
},
208
- [& ](TypeVariable const &) -> Type {
209
- return _type ;
206
+ [](TypeVariable const & _typeVar ) -> Type {
207
+ return _typeVar ;
210
208
},
211
- [& ](std::monostate) -> Type {
212
- return _type ;
209
+ [](std::monostate _nothing ) -> Type {
210
+ return _nothing ;
213
211
}
214
212
}, resolve (_type));
215
213
}
@@ -306,7 +304,7 @@ experimental::Type TypeSystem::type(TypeConstructor _constructor, std::vector<Ty
306
304
307
305
experimental::Type TypeEnvironment::fresh (Type _type)
308
306
{
309
- std::unordered_map<uint64_t , Type> mapping;
307
+ std::unordered_map<size_t , Type> mapping;
310
308
auto freshImpl = [&](Type _type, auto _recurse) -> Type {
311
309
return std::visit (util::GenericVisitor{
312
310
[&](TypeConstant const & _type) -> Type {
0 commit comments