@@ -22,7 +22,15 @@ extern flag g_toolsMode; /* In metamath mode: 0 = metamath, 1 = tools */
22
22
typedef long nmbrString ; /* String of numbers */
23
23
typedef void * pntrString ; /* String of pointers */
24
24
25
+ /* A nmbrString allocated in temporary storage. These strings will be deallocated
26
+ after the next call to `nmbrLet`.
27
+ See also `temp_vstring` for information on how temporaries are handled. */
28
+ typedef nmbrString temp_nmbrString ;
25
29
30
+ /* A pntrString allocated in temporary storage. These strings will be deallocated
31
+ after the next call to `pntrLet`.
32
+ See also `temp_vstring` for information on how temporaries are handled. */
33
+ typedef pntrString temp_pntrString ;
26
34
27
35
enum mTokenType { var_ , con_ };
28
36
#define lb_ '{' /* ${ */
@@ -186,7 +194,7 @@ void initBigArrays(void);
186
194
long getFreeSpace (long max );
187
195
188
196
/* Fatal memory allocation error */
189
- void outOfMemory (vstring msg );
197
+ void outOfMemory (const char * msg );
190
198
191
199
/* Bug check error */
192
200
void bug (int bugNum );
@@ -213,13 +221,13 @@ extern struct nullPntrStruct g_PntrNull;
213
221
214
222
/* This function returns a 1 if any entry in a comma-separated list
215
223
matches using the matches() function. */
216
- flag matchesList (vstring testString , vstring pattern , char wildCard ,
224
+ flag matchesList (const char * testString , const char * pattern , char wildCard ,
217
225
char oneCharWildCard );
218
226
219
227
/* This function returns a 1 if the first argument matches the pattern of
220
228
the second argument. The second argument may have 0-or-more and
221
229
exactly-1 character match wildcards, typically '*' and '?'.*/
222
- flag matches (vstring testString , vstring pattern , char wildCard ,
230
+ flag matches (const char * testString , const char * pattern , char wildCard ,
223
231
char oneCharWildCard );
224
232
225
233
@@ -247,117 +255,114 @@ void nmbrMakeTempAlloc(nmbrString *s);
247
255
248
256
249
257
/* String assignment - MUST be used to assign vstrings */
250
- void nmbrLet (nmbrString * * target ,nmbrString * source );
258
+ void nmbrLet (nmbrString * * target , const nmbrString * source );
251
259
252
260
/* String concatenation - last argument MUST be NULL */
253
- nmbrString * nmbrCat (nmbrString * string1 ,...);
261
+ temp_nmbrString * nmbrCat (const nmbrString * string1 ,...);
254
262
255
263
/* Emulation of nmbrString functions similar to BASIC string functions */
256
- nmbrString * nmbrSeg (nmbrString * sin , long p1 , long p2 );
257
- nmbrString * nmbrMid (nmbrString * sin , long p , long l );
258
- nmbrString * nmbrLeft (nmbrString * sin , long n );
259
- nmbrString * nmbrRight (nmbrString * sin , long n );
264
+ temp_nmbrString * nmbrSeg (const nmbrString * sin , long p1 , long p2 );
265
+ temp_nmbrString * nmbrMid (const nmbrString * sin , long p , long l );
266
+ temp_nmbrString * nmbrLeft (const nmbrString * sin , long n );
267
+ temp_nmbrString * nmbrRight (const nmbrString * sin , long n );
260
268
261
269
/* Allocate and return an "empty" string n "characters" long */
262
- nmbrString * nmbrSpace (long n );
270
+ temp_nmbrString * nmbrSpace (long n );
263
271
264
- long nmbrLen (nmbrString * s );
265
- long nmbrAllocLen (nmbrString * s );
272
+ long nmbrLen (const nmbrString * s );
273
+ long nmbrAllocLen (const nmbrString * s );
266
274
void nmbrZapLen (nmbrString * s , long length );
267
275
268
276
/* Search for string2 in string 1 starting at start_position */
269
- long nmbrInstr (long start , nmbrString * sin , nmbrString * s );
277
+ long nmbrInstr (long start , const nmbrString * sin , const nmbrString * s );
270
278
271
279
/* Search for string2 in string 1 in reverse starting at start_position */
272
280
/* (Reverse nmbrInstr) */
273
- long nmbrRevInstr (long start_position ,nmbrString * string1 ,
274
- nmbrString * string2 );
281
+ long nmbrRevInstr (long start_position , const nmbrString * string1 ,
282
+ const nmbrString * string2 );
275
283
276
284
/* 1 if strings are equal, 0 otherwise */
277
- int nmbrEq (nmbrString * sout , nmbrString * sin );
285
+ flag nmbrEq (const nmbrString * s , const nmbrString * t );
278
286
279
287
/* Converts mString to a vstring with one space between tokens */
280
- vstring nmbrCvtMToVString (nmbrString * s );
288
+ temp_vstring nmbrCvtMToVString (const nmbrString * s );
281
289
282
290
/* Converts rString to a vstring with one space between tokens */
283
- vstring nmbrCvtRToVString (nmbrString * s ,
291
+ temp_vstring nmbrCvtRToVString (const nmbrString * s ,
284
292
flag explicitTargets ,
285
293
long statemNum );
286
294
287
295
/* Get step numbers in an rString - needed by cvtRToVString & elsewhere */
288
- nmbrString * nmbrGetProofStepNumbs (nmbrString * reason );
296
+ nmbrString * nmbrGetProofStepNumbs (const nmbrString * reason );
289
297
290
298
/* Converts any nmbrString to an ASCII string of numbers corresponding
291
299
to the .tokenNum field -- used for debugging only. */
292
- vstring nmbrCvtAnyToVString (nmbrString * s );
300
+ temp_vstring nmbrCvtAnyToVString (const nmbrString * s );
293
301
294
302
/* Extract variables from a math token string */
295
- nmbrString * nmbrExtractVars (nmbrString * m );
303
+ temp_nmbrString * nmbrExtractVars (const nmbrString * m );
296
304
297
305
/* Determine if an element is in a nmbrString; return position if it is */
298
- long nmbrElementIn (long start , nmbrString * g , long element );
306
+ long nmbrElementIn (long start , const nmbrString * g , long element );
299
307
300
308
/* Add a single number to end of a nmbrString - faster than nmbrCat */
301
- nmbrString * nmbrAddElement (nmbrString * g , long element );
309
+ temp_nmbrString * nmbrAddElement (const nmbrString * g , long element );
302
310
303
311
/* Get the set union of two math token strings (presumably
304
312
variable lists) */
305
- nmbrString * nmbrUnion (nmbrString * m1 ,nmbrString * m2 );
313
+ temp_nmbrString * nmbrUnion (const nmbrString * m1 , const nmbrString * m2 );
306
314
307
315
/* Get the set intersection of two math token strings (presumably
308
316
variable lists) */
309
- nmbrString * nmbrIntersection (nmbrString * m1 ,nmbrString * m2 );
317
+ temp_nmbrString * nmbrIntersection (const nmbrString * m1 , const nmbrString * m2 );
310
318
311
319
/* Get the set difference m1-m2 of two math token strings (presumably
312
320
variable lists) */
313
- nmbrString * nmbrSetMinus (nmbrString * m1 ,nmbrString * m2 );
321
+ temp_nmbrString * nmbrSetMinus (const nmbrString * m1 ,const nmbrString * m2 );
314
322
315
323
316
324
317
325
/* This is a utility function that returns the length of a subproof that
318
326
ends at step */
319
- long nmbrGetSubproofLen (nmbrString * proof , long step );
327
+ long nmbrGetSubproofLen (const nmbrString * proof , long step );
320
328
321
329
/* This function returns a "squished" proof, putting in {} references
322
330
to previous subproofs. */
323
- nmbrString * nmbrSquishProof (nmbrString * proof );
331
+ temp_nmbrString * nmbrSquishProof (const nmbrString * proof );
324
332
325
333
/* This function unsquishes a "squished" proof, replacing {} references
326
- to previous subproofs by the subproofs themselvs. The returned nmbrString
327
- must be deallocated by the caller. */
328
- nmbrString * nmbrUnsquishProof (nmbrString * proof );
334
+ to previous subproofs by the subproofs themselves. */
335
+ temp_nmbrString * nmbrUnsquishProof (const nmbrString * proof );
329
336
330
337
/* This function returns the indentation level vs. step number of a proof
331
338
string. This information is used for formatting proof displays. The
332
339
function calls itself recursively, but the first call should be with
333
- startingLevel = 0. The caller is responsible for deallocating the
334
- result. */
335
- nmbrString * nmbrGetIndentation (nmbrString * proof ,
340
+ startingLevel = 0. */
341
+ temp_nmbrString * nmbrGetIndentation (const nmbrString * proof ,
336
342
long startingLevel );
337
343
338
344
/* This function returns essential (1) or floating (0) vs. step number of a
339
345
proof string. This information is used for formatting proof displays. The
340
346
function calls itself recursively, but the first call should be with
341
- startingLevel = 0. The caller is responsible for deallocating the
342
- result. */
343
- nmbrString * nmbrGetEssential (nmbrString * proof );
347
+ startingLevel = 0. */
348
+ temp_nmbrString * nmbrGetEssential (const nmbrString * proof );
344
349
345
350
/* This function returns the target hypothesis vs. step number of a proof
346
351
string. This information is used for formatting proof displays. The
347
- function calls itself recursively. The caller is responsible for
348
- deallocating the result. statemNum is the statement being proved. */
349
- nmbrString * nmbrGetTargetHyp (nmbrString * proof , long statemNum );
352
+ function calls itself recursively.
353
+ statemNum is the statement being proved. */
354
+ temp_nmbrString * nmbrGetTargetHyp (const nmbrString * proof , long statemNum );
350
355
351
356
/* Converts a proof string to a compressed-proof-format ASCII string.
352
357
Normally, the proof string would be compacted with squishProof first,
353
358
although it's not a requirement. */
354
359
/* The statement number is needed because required hypotheses are
355
360
implicit in the compressed proof. */
356
- vstring compressProof (nmbrString * proof , long statemNum ,
361
+ temp_vstring compressProof (const nmbrString * proof , long statemNum ,
357
362
flag oldCompressionAlgorithm );
358
363
359
364
/* Gets length of the ASCII form of a compressed proof */
360
- long compressedProofSize (nmbrString * proof , long statemNum );
365
+ long compressedProofSize (const nmbrString * proof , long statemNum );
361
366
362
367
363
368
/*******************************************************************/
@@ -383,48 +388,48 @@ void pntrMakeTempAlloc(pntrString *s);
383
388
384
389
385
390
/* String assignment - MUST be used to assign vstrings */
386
- void pntrLet (pntrString * * target ,pntrString * source );
391
+ void pntrLet (pntrString * * target , const pntrString * source );
387
392
388
393
/* String concatenation - last argument MUST be NULL */
389
- pntrString * pntrCat (pntrString * string1 ,...);
394
+ temp_pntrString * pntrCat (const pntrString * string1 ,...);
390
395
391
396
/* Emulation of pntrString functions similar to BASIC string functions */
392
- pntrString * pntrSeg (pntrString * sin , long p1 , long p2 );
393
- pntrString * pntrMid (pntrString * sin , long p , long length );
394
- pntrString * pntrLeft (pntrString * sin , long n );
395
- pntrString * pntrRight (pntrString * sin , long n );
397
+ temp_pntrString * pntrSeg (const pntrString * sin , long p1 , long p2 );
398
+ temp_pntrString * pntrMid (const pntrString * sin , long p , long length );
399
+ temp_pntrString * pntrLeft (const pntrString * sin , long n );
400
+ temp_pntrString * pntrRight (const pntrString * sin , long n );
396
401
397
402
/* Allocate and return an "empty" string n "characters" long */
398
- pntrString * pntrSpace (long n );
403
+ temp_pntrString * pntrSpace (long n );
399
404
400
405
/* Allocate and return an "empty" string n "characters" long
401
406
initialized to nmbrStrings instead of vStrings */
402
- pntrString * pntrNSpace (long n );
407
+ temp_pntrString * pntrNSpace (long n );
403
408
404
409
/* Allocate and return an "empty" string n "characters" long
405
410
initialized to pntrStrings instead of vStrings */
406
- pntrString * pntrPSpace (long n );
411
+ temp_pntrString * pntrPSpace (long n );
407
412
408
- long pntrLen (pntrString * s );
409
- long pntrAllocLen (pntrString * s );
413
+ long pntrLen (const pntrString * s );
414
+ long pntrAllocLen (const pntrString * s );
410
415
void pntrZapLen (pntrString * s , long length );
411
416
412
417
/* Search for string2 in string 1 starting at start_position */
413
- long pntrInstr (long start , pntrString * sin , pntrString * s );
418
+ long pntrInstr (long start , const pntrString * sin , const pntrString * s );
414
419
415
420
/* Search for string2 in string 1 in reverse starting at start_position */
416
421
/* (Reverse pntrInstr) */
417
- long pntrRevInstr (long start_position ,pntrString * string1 ,
418
- pntrString * string2 );
422
+ long pntrRevInstr (long start_position , const pntrString * string1 ,
423
+ const pntrString * string2 );
419
424
420
425
/* 1 if strings are equal, 0 otherwise */
421
- int pntrEq (pntrString * sout ,pntrString * sin );
426
+ flag pntrEq (const pntrString * sout , const pntrString * sin );
422
427
423
428
/* Add a single null string element to a pntrString - faster than pntrCat */
424
- pntrString * pntrAddElement (pntrString * g );
429
+ temp_pntrString * pntrAddElement (const pntrString * g );
425
430
426
431
/* Add a single null pntrString element to a pntrString - faster than pntrCat */
427
- pntrString * pntrAddGElement (pntrString * g );
432
+ temp_pntrString * pntrAddGElement (const pntrString * g );
428
433
429
434
/* Utility functions */
430
435
0 commit comments