1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Christopher L. Conway, Morgan Deters, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Base for parser inputs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5parser_public.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PARSER__INPUT_H |
19 |
|
#define CVC5__PARSER__INPUT_H |
20 |
|
|
21 |
|
#include <stdio.h> |
22 |
|
|
23 |
|
#include <iostream> |
24 |
|
#include <string> |
25 |
|
#include <vector> |
26 |
|
|
27 |
|
#include "api/cpp/cvc5.h" |
28 |
|
#include "cvc5_export.h" |
29 |
|
#include "options/language.h" |
30 |
|
#include "parser/parser_exception.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
|
34 |
|
class Command; |
35 |
|
|
36 |
|
namespace parser { |
37 |
|
|
38 |
|
class InputStreamException : public Exception |
39 |
|
{ |
40 |
|
public: |
41 |
|
InputStreamException(const std::string& msg); |
42 |
|
}; |
43 |
|
|
44 |
|
/** Wrapper around an input stream. */ |
45 |
|
class InputStream |
46 |
|
{ |
47 |
|
/** The name of this input stream. */ |
48 |
|
std::string d_name; |
49 |
|
|
50 |
|
/** Indicates whether the input file is a temporary that we should |
51 |
|
* delete on exit. */ |
52 |
|
bool d_fileIsTemporary; |
53 |
|
|
54 |
|
protected: |
55 |
|
/** Initialize the input stream with a name. */ |
56 |
4072 |
InputStream(std::string name, bool isTemporary=false) : |
57 |
|
d_name(name), |
58 |
4072 |
d_fileIsTemporary(isTemporary) { |
59 |
4072 |
} |
60 |
|
|
61 |
|
public: |
62 |
|
/** Destructor. */ |
63 |
8144 |
virtual ~InputStream() { |
64 |
4072 |
if( d_fileIsTemporary ) { |
65 |
|
remove(d_name.c_str()); |
66 |
|
} |
67 |
4072 |
} |
68 |
|
|
69 |
|
/** Get the name of this input stream. */ |
70 |
|
const std::string getName() const; |
71 |
|
}; /* class InputStream */ |
72 |
|
|
73 |
|
class Parser; |
74 |
|
|
75 |
|
/** |
76 |
|
* An input to be parsed. The static factory methods in this class (e.g., |
77 |
|
* <code>newFileInput</code>, <code>newStringInput</code>) create a parser |
78 |
|
* for the given input language and attach it to an input source of the |
79 |
|
* appropriate type. |
80 |
|
*/ |
81 |
|
class CVC5_EXPORT Input |
82 |
|
{ |
83 |
|
friend class Parser; // for parseError, parseCommand, parseExpr |
84 |
|
friend class ParserBuilder; |
85 |
|
|
86 |
|
/** The input stream. */ |
87 |
|
InputStream *d_inputStream; |
88 |
|
|
89 |
|
/* Since we own d_inputStream and it needs to be freed, we need to prevent |
90 |
|
* copy construction and assignment. Mark them private and do not define |
91 |
|
* them. |
92 |
|
*/ |
93 |
|
Input(const Input& input) = delete; |
94 |
|
Input& operator=(const Input& input) = delete; |
95 |
|
|
96 |
|
public: |
97 |
|
/** Create an input for the given file. |
98 |
|
* |
99 |
|
* @param lang the input language |
100 |
|
* @param filename the input filename |
101 |
|
* @param useMmap true if the parser should use memory-mapped I/O (default: false) |
102 |
|
*/ |
103 |
|
static Input* newFileInput(const std::string& lang, |
104 |
|
const std::string& filename, |
105 |
|
bool useMmap = false); |
106 |
|
|
107 |
|
/** Create an input for the given stream. |
108 |
|
* |
109 |
|
* @param lang the input language |
110 |
|
* @param input the input stream |
111 |
|
* @param name the name of the stream, for use in error messages |
112 |
|
* @param lineBuffered whether this Input should be line-buffered |
113 |
|
* (false, the default, means that the entire Input might be read |
114 |
|
* before being lexed and parsed) |
115 |
|
*/ |
116 |
|
static Input* newStreamInput(const std::string& lang, |
117 |
|
std::istream& input, |
118 |
|
const std::string& name); |
119 |
|
|
120 |
|
/** Create an input for the given string |
121 |
|
* |
122 |
|
* @param lang the input language |
123 |
|
* @param input the input string |
124 |
|
* @param name the name of the stream, for use in error messages |
125 |
|
*/ |
126 |
|
static Input* newStringInput(const std::string& lang, |
127 |
|
const std::string& input, |
128 |
|
const std::string& name); |
129 |
|
|
130 |
|
/** Destructor. Frees the input stream and closes the input. */ |
131 |
|
virtual ~Input(); |
132 |
|
|
133 |
|
/** Retrieve the name of the input stream */ |
134 |
48 |
const std::string getInputStreamName() { return getInputStream()->getName(); } |
135 |
|
protected: |
136 |
|
/** Create an input. |
137 |
|
* |
138 |
|
* @param inputStream the input stream |
139 |
|
*/ |
140 |
|
Input(InputStream& inputStream); |
141 |
|
|
142 |
|
/** Retrieve the input stream for this parser. */ |
143 |
|
InputStream *getInputStream(); |
144 |
|
|
145 |
|
/** Parse a command from the input by invoking the |
146 |
|
* implementation-specific parsing method. Returns |
147 |
|
* <code>NULL</code> if there is no command there to parse. |
148 |
|
* |
149 |
|
* @throws ParserException if an error is encountered during parsing. |
150 |
|
*/ |
151 |
|
virtual Command* parseCommand() = 0; |
152 |
|
|
153 |
|
/** |
154 |
|
* Issue a warning to the user, with source file, line, and column info. |
155 |
|
*/ |
156 |
|
virtual void warning(const std::string& msg) = 0; |
157 |
|
|
158 |
|
/** |
159 |
|
* Throws a <code>ParserException</code> with the given message. |
160 |
|
*/ |
161 |
|
virtual void parseError(const std::string& msg, |
162 |
|
bool eofException = false) = 0; |
163 |
|
|
164 |
|
/** Parse an expression from the input by invoking the |
165 |
|
* implementation-specific parsing method. Returns a null |
166 |
|
* <code>api::Term</code> if there is no expression there to parse. |
167 |
|
* |
168 |
|
* @throws ParserException if an error is encountered during parsing. |
169 |
|
*/ |
170 |
|
virtual api::Term parseExpr() = 0; |
171 |
|
|
172 |
|
/** Set the Parser object for this input. */ |
173 |
|
virtual void setParser(Parser& parser) = 0; |
174 |
|
|
175 |
|
}; /* class Input */ |
176 |
|
|
177 |
|
} // namespace parser |
178 |
|
} // namespace cvc5 |
179 |
|
|
180 |
|
#endif /* CVC5__PARSER__ANTLR_INPUT_H */ |