diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-28 14:51:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-28 14:51:41 -0500 |
commit | 3ed42d7aba07db5801cf8245890035192aa06b15 (patch) | |
tree | 83299050be1fa63e14acf55455032f0763372b63 /src/parser/parser.cpp | |
parent | a61f77fd58c8da0f38de4d094258f78f71774383 (diff) |
Convert symbol table from Expr-level to Term-level (#5355)
This task is left over from parser migration.
This PR also drops support for a case of symbol overloading, in particular symbols (constructors, selectors) for parametric datatypes cannot be overloaded. One regression is disabled as a result.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index e58172b92..e815d9024 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -82,7 +82,7 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type) assert(isDeclared(name, type)); assert(type == SYM_VARIABLE); // Functions share var namespace - return api::Term(d_solver, d_symtab->lookup(name)); + return d_symtab->lookup(name); } api::Term Parser::getVariable(const std::string& name) @@ -159,7 +159,7 @@ api::Sort Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name)); + api::Sort t = d_symtab->lookupType(name); return t; } @@ -168,8 +168,7 @@ api::Sort Parser::getSort(const std::string& name, { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = api::Sort( - d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params))); + api::Sort t = d_symtab->lookupType(name, params); return t; } @@ -279,7 +278,7 @@ void Parser::defineVar(const std::string& name, bool doOverload) { Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; - if (!d_symtab->bind(name, val.getExpr(), levelZero, doOverload)) + if (!d_symtab->bind(name, val, levelZero, doOverload)) { std::stringstream ss; ss << "Cannot bind " << name << " to symbol of type " << val.getSort(); @@ -296,10 +295,10 @@ void Parser::defineType(const std::string& name, { if (skipExisting && isDeclared(name, SYM_SORT)) { - assert(api::Sort(d_solver, d_symtab->lookupType(name)) == type); + assert(d_symtab->lookupType(name) == type); return; } - d_symtab->bindType(name, type.getType(), levelZero); + d_symtab->bindType(name, type, levelZero); assert(isDeclared(name, SYM_SORT)); } @@ -308,8 +307,7 @@ void Parser::defineType(const std::string& name, const api::Sort& type, bool levelZero) { - d_symtab->bindType( - name, api::sortVectorToTypes(params), type.getType(), levelZero); + d_symtab->bindType(name, params, type, levelZero); assert(isDeclared(name, SYM_SORT)); } |