1 /*-----------------------------------------------------------------------
2
3 File : cio_streams.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Implementation of the stream datatype for look-aheadable input.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Sat Jul 5 02:28:25 MET DST 1997
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "cio_streams.h"
25
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31 /* This variables are really constants and are used to select the input
32 method for a stream. Default is file type (with error messages
33 described by e.g. the GNU coding guidelines), for string input
34 streams the StreamType is used in the error message. */
35
36 const StreamType StreamTypeFile = NULL;
37 const StreamType StreamTypeInternalString =
38 "Internal (programmer-defined) string - if you see this, you"
39 " encountered a bug";
40 const StreamType StreamTypeUserString =
41 "Parsing a user provided string";
42 const StreamType StreamTypeOptionString =
43 "Parsing a user given option argument";
44
45 /*---------------------------------------------------------------------*/
46 /* Forward Declarations */
47 /*---------------------------------------------------------------------*/
48
49
50 /*---------------------------------------------------------------------*/
51 /* Internal Functions */
52 /*---------------------------------------------------------------------*/
53
54
55 /*-----------------------------------------------------------------------
56 //
57 // Function: read_char()
58 //
59 // Read a character and return it. Return an infinite sequence of
60 // EOFs after the end of file.
61 //
62 // Global Variables: -
63 //
64 // Side Effects : May read a character
65 //
66 /----------------------------------------------------------------------*/
67
read_char(Stream_p stream)68 static int read_char(Stream_p stream)
69 {
70 int ch;
71
72 if(stream->eof_seen)
73 {
74 ch = EOF;
75 }
76 else
77 {
78 if(stream->stream_type!=StreamTypeFile)
79 {
80 ch = (int)DStrView(stream->source)[stream->string_pos];
81 if(ch)
82 {
83 stream->string_pos++;
84 }
85 else
86 {
87 ch = EOF;
88 stream->eof_seen = true;
89 }
90 }
91 else
92 {
93 ch = getc(stream->file);
94 if(ch == EOF)
95 {
96 stream->eof_seen = true;
97 }
98 }
99 }
100 return ch;
101 }
102
103 /*---------------------------------------------------------------------*/
104 /* Exported Functions */
105 /*---------------------------------------------------------------------*/
106
107
108 /*-----------------------------------------------------------------------
109 //
110 // Function: CreateStream()
111 //
112 // Create a stream associated with the file name. Both the
113 // NULL-pointer and the name "-" are taken to mean stdin.
114 //
115 // Global Variables: -
116 //
117 // Side Effects : May terminate with an error message
118 //
119 /----------------------------------------------------------------------*/
120
CreateStream(StreamType type,char * source,bool fail)121 Stream_p CreateStream(StreamType type, char* source, bool fail)
122 {
123 Stream_p handle;
124 int i;
125
126 handle = StreamCellAlloc();
127
128 handle->source = DStrAlloc();
129 handle->stream_type = type;
130
131 if(type == StreamTypeFile)
132 {
133 /* Interprete source as a file name ! */
134
135 if(!source || !strcmp(source,"-"))
136 {
137 DStrSet(handle->source, "<stdin>");
138 handle->file = stdin;
139 /* handle->dir == "" */
140 }
141 else
142 {
143 DStrSet(handle->source, source);
144 handle->file = InputOpen(source, fail);
145 if(!handle->file)
146 {
147 DStrFree(handle->source);
148 StreamCellFree(handle);
149 return NULL;
150 }
151 }
152 VERBOUTARG("Opened ", DStrView(handle->source));
153 }
154 else
155 {
156 /* Interprete source as a string to read from! */
157
158 DStrSet(handle->source, source);
159 handle->string_pos = 0;
160 }
161 handle->next = NULL;
162 handle->eof_seen = false;
163 handle->line = 1;
164 handle->column = 1;
165 handle->current = 0;
166
167 for(i=0; i<MAXLOOKAHEAD; i++)
168 {
169 handle->buffer[i] = read_char(handle);
170 }
171
172 return handle;
173 }
174
175
176 /*-----------------------------------------------------------------------
177 //
178 // Function: DestroyStream()
179 //
180 // Free all resources (memory, file handle) associated with the
181 // stream.
182 //
183 // Global Variables: -
184 //
185 // Side Effects : Memory operations, file operations
186 //
187 /----------------------------------------------------------------------*/
188
DestroyStream(Stream_p stream)189 void DestroyStream(Stream_p stream)
190 {
191 if(stream->stream_type == StreamTypeFile)
192 {
193 if(stream->file != stdin)
194 {
195 if(fclose(stream->file) != 0)
196 {
197 TmpErrno = errno;
198 sprintf(ErrStr, "Cannot close file %s", DStrView(stream->source));
199 SysError(ErrStr, FILE_ERROR);
200 }
201 }
202 VERBOUTARG("Closing ", DStrView(stream->source));
203 }
204 DStrFree(stream->source);
205 StreamCellFree(stream);
206 }
207
208
209 /*-----------------------------------------------------------------------
210 //
211 // Function: StreamNextChar()
212 //
213 // Move the current window on the input stream one character
214 // forward. Return the new CurrChar().
215 //
216 // Global Variables: -
217 //
218 // Side Effects : Reads one character from the input, update the
219 // stream information about the current position.
220 //
221 /----------------------------------------------------------------------*/
222
StreamNextChar(Stream_p stream)223 int StreamNextChar(Stream_p stream)
224 {
225 if(StreamCurrChar(stream) == '\n')
226 {
227 stream->line++;
228 stream->column = 1;
229 }
230 else
231 {
232 stream->column++;
233 }
234 stream->current=STREAMREALPOS(stream->current+1);
235 stream->buffer[STREAMREALPOS(stream->current+MAXLOOKAHEAD-1)]
236 = read_char(stream);
237
238 return StreamCurrChar(stream);
239 }
240
241
242 /*-----------------------------------------------------------------------
243 //
244 // Function: OpenStackedInput()
245 //
246 // Open a new input stream and put it on top of the stack. All
247 // further input from this stack is read from the new top of the
248 // stack.
249 //
250 // Global Variables: -
251 //
252 // Side Effects : Memory operations
253 //
254 /----------------------------------------------------------------------*/
255
OpenStackedInput(Inpstack_p stack,StreamType type,char * source,bool fail)256 Stream_p OpenStackedInput(Inpstack_p stack, StreamType type, char* source, bool fail)
257 {
258 Stream_p handle;
259
260 handle = CreateStream(type, source, fail);
261 if(handle)
262 {
263 handle->next = *stack;
264 *stack = handle;
265 }
266 return handle;
267 }
268
269
270 /*-----------------------------------------------------------------------
271 //
272 // Function: CloseStackedInput()
273 //
274 // Pop the top from the input stack and destroy the associated
275 // stream.
276 //
277 // Global Variables: -
278 //
279 // Side Effects : Memory operations
280 //
281 /----------------------------------------------------------------------*/
282
CloseStackedInput(Inpstack_p stack)283 void CloseStackedInput(Inpstack_p stack)
284 {
285 Stream_p handle;
286
287 assert(*stack);
288 handle = *stack;
289 *stack = handle->next;
290 DestroyStream(handle);
291 }
292
293 /*---------------------------------------------------------------------*/
294 /* End of File */
295 /*---------------------------------------------------------------------*/
296
297
298