diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:32 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:41 +0100 |
commit | 82fbac8829cbc41927216b36ab064b50e50b2fa0 (patch) | |
tree | 346361d002c109b8ac2254f4f215a12dfc7643d2 /src/parser/parser.cpp | |
parent | 3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (diff) |
Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index aa91a5a1e..10a729420 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -362,7 +362,15 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { // complained of a bad substitution if anything is left unresolved. // Clear out the set. d_unresolved.clear(); - + + //throw exception if any datatype is not well-founded + for(unsigned i = 0; i < datatypes.size(); ++i) { + const Datatype& dt = types[i].getDatatype(); + if( !dt.isCodatatype() && !dt.isWellFounded() ){ + throw ParserException(dt.getName() + " is not well-founded"); + } + } + return types; } catch(IllegalArgumentException& ie) { throw ParserException(ie.getMessage()); |