-
Notifications
You must be signed in to change notification settings - Fork 0
/
mmpars.h
137 lines (115 loc) · 6.13 KB
/
mmpars.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
/*****************************************************************************/
/* Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu */
/* License terms: GNU General Public License */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
#ifndef METAMATH_MMPARS_H_
#define METAMATH_MMPARS_H_
#include "mmvstr.h"
#include "mmdata.h"
char *readRawSource(vstring inputFn, long bufOffsetSoFar, long *size);
void parseKeywords(void);
void parseLabels(void);
void parseMathDecl(void);
void parseStatements(void);
char parseProof(long statemNum);
char parseCompressedProof(long statemNum);
nmbrString *getProof(long statemNum, flag printFlag);
void rawSourceError(char *startFile, char *ptr, long tokenLen, long lineNum,
vstring fileName, vstring errMsg);
void sourceError(char *ptr, long tokenLen, long stmtNum, vstring errMsg);
void mathTokenError(long tokenNum /* 0 is 1st one */,
nmbrString *tokenList, long stmtNum, vstring errMsg);
vstring shortDumpRPNStack(void);
/* Label comparison for qsort */
int labelSortCmp(const void *key1, const void *key2);
/* Label comparison for bsearch */
int labelSrchCmp(const void *key, const void *data);
/* Math token comparison for qsort */
int mathSortCmp(const void *key1, const void *key2);
/* Math token label comparison for bsearch */
int mathSrchCmp(const void *key, const void *data);
/* Hypothesis and local label comparison for qsort */
int hypAndLocSortCmp(const void *key1, const void *key2);
/* Hypothesis and local label comparison for bsearch */
int hypAndLocSrchCmp(const void *key, const void *data);
/* This function returns the length of the white space starting at ptr.
Comments are considered white space. ptr should point to the first character
of the white space. If ptr does not point to a white space character, 0
is returned. If ptr points to a null character, 0 is returned. */
long whiteSpaceLen(char *ptr);
/* This function returns the length of the token (non-white-space) starting at
ptr. Comments are considered white space. ptr should point to the first
character of the token. If ptr points to a white space character, 0
is returned. If ptr points to a null character, 0 is returned. If ptr
points to a keyword, 0 is returned. A keyword ends a token. */
long tokenLen(char *ptr);
/* This function returns the length of the proof token starting at
ptr. Comments are considered white space. ptr should point to the first
character of the token. If ptr points to a white space character, 0
is returned. If ptr points to a null character, 0 is returned. If ptr
points to a keyword, 0 is returned. A keyword ends a token.
":" is considered a token. */
long proofTokenLen(char *ptr);
/* Array with sort keys for all possible labels, including the ones for
hypotheses (which may not always be active) */
/* This array is used to see if any label is used anywhere, and is used
to make sure there are no conflicts when local labels inside of compact
proofs are generated. */
extern long *allLabelKeyBase;
extern long numAllLabelKeys;
/* Working structure for parsing proofs */
/* This structure should be deallocated by the ERASE command. */
extern long wrkProofMaxSize; /* Maximum size so far - it may grow */
struct sortHypAndLoc { /* Used for sorting hypAndLocLabel field */
long labelTokenNum;
void *labelName;
};
struct wrkProof_struct {
long numTokens; /* Number of tokens in proof */
long numSteps; /* Number of steps in proof */
long numLocalLabels; /* Number of local labels */
long numHypAndLoc; /* Number of active hypotheses and local labels */
char *localLabelPoolPtr; /* Next free location in local label pool */
long RPNStackPtr; /* Offset of end of RPNStack */
long errorCount; /* Errors in proof - used to suppress too many error msgs */
flag errorSeverity; /* 0 = OK, 1 = unk step, 2 = error, 3 = severe error,
4 = not a $p statement */
/* The following pointers will always be allocated with wrkProofMaxSize
entries. If a function needs more than wrkProofMaxSize, it must
reallocate all of these and increase wrkProofMaxSize. */
nmbrString *tokenSrcPtrNmbr; /* Source parsed into tokens vs. token number
- token size */
pntrString *tokenSrcPtrPntr; /* Source parsed into tokens vs. token number
- token src ptrs */
nmbrString *stepSrcPtrNmbr; /* Pointer to label token in source file
vs. step number - label size */
pntrString *stepSrcPtrPntr; /* Pointer to label token in source file
vs. step number - label src ptrs */
flag *localLabelFlag; /* 1 means step has a local label declaration */
struct sortHypAndLoc *hypAndLocLabel;
/* Sorted ptrs to hyp and local label names + token# */
char *localLabelPool; /* String pool to hold local labels */
nmbrString *proofString; /* The proof in RPN - statement # if > 0
or -(step # + 1000) of local label decl if < -1 */
pntrString *mathStringPtrs; /* Ptr to math string vs. each step */
/* (Allocated in verifyProof() as needed by nmbrLet()) */
nmbrString *RPNStack; /* Stack for RPN parsing */
/* For compressed proof parsing */
nmbrString *compressedPfLabelMap; /* Map from compressed label to actual */
long compressedPfNumLabels; /* Number of compressed labels */
};
extern struct wrkProof_struct wrkProof;
/* Converts an ASCII string to a nmbrString of math symbols. statemNum
provides the context for the parse (to get correct active symbols) */
nmbrString *parseMathTokens(vstring userText, long statemNum);
/* 12-Jun-2011 nm Added reformatFlag */
vstring outputStatement(long stmt, /*flag cleanFlag,*/ flag reformatFlag);
/* 12-Jun-2011 nm */
/* Caller must deallocate return string */
vstring rewrapComment(vstring comment);
/* 10/10/02 */
/* Lookup $a or $p label and return statement number.
Return -1 if not found. */
long lookupLabel(vstring label);
#endif /* METAMATH_MMPARS_H_ */