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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
#ifndef SC2_CHECK_H
#define SC2_CHECK_H
#include "expr.h"
#include "trie.h"
#ifdef _MSC_VER
#include <hash_map>
#include <stdio.h>
#else
#include <ext/hash_map>
#endif
#include <stack>
#include <string>
#include <map>
// see the help message in main.cpp for explanation
typedef struct args {
std::vector<std::string> files;
bool show_runs;
bool no_tail_calls;
bool compile_scc;
bool compile_scc_debug;
bool run_scc;
bool use_nested_app;
bool compile_lib;
} args;
extern int check_time;
class sccwriter;
class libwriter;
void init();
void check_file(const char *_filename, args a, sccwriter* scw = NULL, libwriter* lw = NULL);
void cleanup();
extern char our_getc_c;
void report_error(const std::string &);
extern int linenum;
extern int colnum;
extern const char *filename;
extern FILE *curfile;
inline void our_ungetc(char c) {
if (our_getc_c != 0)
report_error("Internal error: our_ungetc buffer full");
our_getc_c = c;
if (c == '\n') {
linenum--;
colnum=-1;
}
else
colnum--;
}
inline char our_getc() {
char c;
if (our_getc_c > 0) {
c = our_getc_c;
our_getc_c = 0;
}
else{
#ifndef __linux__
c = fgetc(curfile);
#else
c = fgetc_unlocked(curfile);
#endif
}
switch(c) {
case '\n':
linenum++;
#ifdef DEBUG_LINES
std::cout << "line " << linenum << "." << std::endl;
#endif
colnum = 1;
break;
case char(EOF):
break;
default:
colnum++;
}
return c;
}
// return the next character that is not whitespace
inline char non_ws() {
char c;
while(isspace(c = our_getc()));
if (c == ';') {
// comment to end of line
while((c = our_getc()) != '\n' && c != char(EOF));
return non_ws();
}
return c;
}
inline void eat_char(char expected) {
if (non_ws() != expected) {
char tmp[80];
sprintf(tmp,"Expecting a \'%c\'",expected);
report_error(tmp);
}
}
extern int IDBUF_LEN;
extern char idbuf[];
inline const char *prefix_id() {
int i = 0;
char c = idbuf[i++] = non_ws();
while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) {
if (i == IDBUF_LEN)
report_error("Identifier is too long");
idbuf[i++] = c = our_getc();
}
our_ungetc(c);
idbuf[i-1] = 0;
return idbuf;
}
#ifdef _MSC_VER
typedef std::hash_map<std::string, Expr *> symmap;
typedef std::hash_map<std::string, SymExpr *> symmap2;
#else
typedef __gnu_cxx::hash_map<std::string, Expr *> symmap;
typedef __gnu_cxx::hash_map<std::string, SymExpr *> symmap2;
#endif
extern symmap2 progs;
extern std::vector< Expr* > ascHoles;
#ifdef USE_HASH_MAPS
extern symmap symbols;
extern symmap symbol_types;
#else
extern Trie<std::pair<Expr *, Expr *> > *symbols;
#endif
extern std::map<SymExpr*, int > mark_map;
extern std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > local_sym_names;
#ifndef _MSC_VER
namespace __gnu_cxx
{
template<> struct hash< std::string >
{
size_t operator()( const std::string& x ) const
{
return hash< const char* >()( x.c_str() );
}
};
}
#endif
extern Expr *statMpz;
extern Expr *statMpq;
extern Expr *statType;
#endif
|
