diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-04 15:28:24 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-04 15:41:05 -0600 |
| commit | 5552e43454c3b45ae8c7b35a822ac4b39adca72f (patch) | |
| tree | bf7eacb6908c439bde2c8e8052a83f52cdcd46ca /src/parser/tptp/Tptp.g | |
| parent | 0beaa6fbb218328ade97d1f3c5b40fde7aa6d3b5 (diff) | |
Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes.
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 73dcfa6cb..414c2f6b0 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -803,6 +803,9 @@ parseType[CVC4::Type& type] // non-function types simpleType[CVC4::Type& type] +@declarations { + std::string name; +} : DEFINED_SYMBOL { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL); if(s == "\$i") type = PARSER_STATE->d_unsorted; @@ -813,8 +816,8 @@ simpleType[CVC4::Type& type] else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here"); else PARSER_STATE->parseError("unknown defined type `" + s + "'"); } - | LOWER_WORD - { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); } + | atomicWord[name] + { type = PARSER_STATE->getSort(name); } ; /***********************************************/ |