}
SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
- size_t arity) const {
+ size_t arity,
+ uint32_t flags) const
+{
NodeManagerScope nms(d_nodeManager);
- return SortConstructorType(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
+ return SortConstructorType(
+ Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags))));
}
/**
/** Make a sort constructor from a name and arity. */
SortConstructorType mkSortConstructor(const std::string& name,
- size_t arity) const;
+ size_t arity,
+ uint32_t flags = SORT_FLAG_NONE) const;
/**
* Get the type of an expression.
}
TypeNode NodeManager::mkSortConstructor(const std::string& name,
- size_t arity) {
+ size_t arity,
+ uint32_t flags)
+{
Assert(arity > 0);
NodeBuilder<> nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
setAttribute(type, expr::VarNameAttr(), name);
setAttribute(type, expr::SortArityAttr(), arity);
for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewSortConstructor(type);
+ (*i)->nmNotifyNewSortConstructor(type, flags);
}
return type;
}
public:
virtual ~NodeManagerListener() {}
virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
- virtual void nmNotifyNewSortConstructor(TypeNode tn) {}
+ virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
uint32_t flags) {}
virtual void nmNotifyNewDatatypes(
uint32_t flags = ExprManager::SORT_FLAG_NONE);
/** Make a new sort with the given name and arity. */
- TypeNode mkSortConstructor(const std::string& name, size_t arity);
+ TypeNode mkSortConstructor(const std::string& name,
+ size_t arity,
+ uint32_t flags = ExprManager::SORT_FLAG_NONE);
/**
* Get the type for the given node and optionally do type checking.
}
SortConstructorType Parser::mkSortConstructor(const std::string& name,
- size_t arity) {
+ size_t arity,
+ uint32_t flags)
+{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
+ SortConstructorType type =
+ d_exprManager->mkSortConstructor(name, arity, flags);
defineType(name, vector<Type>(arity), type);
return type;
}
SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
size_t arity) {
- SortConstructorType unresolved = mkSortConstructor(name, arity);
+ SortConstructorType unresolved =
+ mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER);
d_unresolved.insert(unresolved);
return unresolved;
}
const std::string& name, const std::vector<Type>& params) {
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
- SortConstructorType unresolved =
- d_exprManager->mkSortConstructor(name, params.size());
+ SortConstructorType unresolved = d_exprManager->mkSortConstructor(
+ name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
defineType(name, params, unresolved);
Type t = getSort(name, params);
d_unresolved.insert(unresolved);
/**
* Creates a new sort constructor with the given name and arity.
*/
- SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
+ SortConstructorType mkSortConstructor(
+ const std::string& name,
+ size_t arity,
+ uint32_t flags = ExprManager::SORT_FLAG_NONE);
/**
* Creates a new "unresolved type," used only during parsing.
PARSER_STATE->pushScope(true); }
LPAREN_TOK /* parametric sorts */
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
- { sorts.push_back( PARSER_STATE->mkSort(name) ); }
+ { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
)*
RPAREN_TOK
LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
}
( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
- { params.push_back( PARSER_STATE->mkSort(name) ); }
+ { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
)*
RPAREN_TOK {
// if the arity was fixed by prelude and is not equal to the number of parameters
// APPLY_UF, APPLY_CONSTRUCTOR, etc.
Assert( n.hasOperator() );
TypeNode opt = n.getOperator().getType();
+ if (n.getKind() == kind::APPLY_CONSTRUCTOR)
+ {
+ Type tn = n.getType().toType();
+ // may be parametric, in which case the constructor type must be
+ // specialized
+ const Datatype& dt = static_cast<DatatypeType>(tn).getDatatype();
+ if (dt.isParametric())
+ {
+ unsigned ci = Datatype::indexOf(n.getOperator().toExpr());
+ opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn));
+ }
+ }
Assert( opt.getNumChildren() == n.getNumChildren() + 1 );
for(size_t i = 0; i < n.getNumChildren(); ++i ) {
force_child_type[i] = opt[i];
++i)
{
const Datatype& d = i->getDatatype();
+ if (d.isParametric())
+ {
+ out << "(par (";
+ for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++)
+ {
+ out << (p > 0 ? " " : "") << d.getParameter(p);
+ }
+ out << ")";
+ }
out << "(";
toStream(out, d);
out << ")";
+ if (d.isParametric())
+ {
+ out << ")";
+ }
}
out << ")";
}
else
{
- out << " () (";
+ out << " (";
+ // Can only print if all datatypes in this block have the same parameters.
+ // In theory, given input language 2.6 and output language 2.5, it could
+ // be impossible to print a datatype block where datatypes were given
+ // different parameter lists.
+ bool success = true;
+ const Datatype& d = datatypes[0].getDatatype();
+ unsigned nparam = d.getNumParameters();
+ for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
+ {
+ const Datatype& dj = datatypes[j].getDatatype();
+ if (dj.getNumParameters() != nparam)
+ {
+ success = false;
+ }
+ else
+ {
+ // must also have identical parameter lists
+ for (unsigned k = 0; k < nparam; k++)
+ {
+ if (dj.getParameter(k) != d.getParameter(k))
+ {
+ success = false;
+ break;
+ }
+ }
+ }
+ if (!success)
+ {
+ break;
+ }
+ }
+ if (success)
+ {
+ for (unsigned j = 0; j < nparam; j++)
+ {
+ out << (j > 0 ? " " : "") << d.getParameter(j);
+ }
+ }
+ else
+ {
+ out << std::endl;
+ out << "ERROR: datatypes in each block must have identical parameter "
+ "lists.";
+ out << std::endl;
+ }
+ out << ") (";
for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
i_end = datatypes.end();
i != i_end;
}
}
- void nmNotifyNewSortConstructor(TypeNode tn) override
+ void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override
{
DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
tn.getAttribute(expr::SortArityAttr()),
tn.toType());
- d_smt.addToModelCommandAndDump(c);
+ if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+ {
+ d_smt.addToModelCommandAndDump(c);
+ }
}
void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override