2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
3 ** See ../LICENSE for license information.
12 /* There are 3 separate namespaces being maintained in this symbol
13 table: (N1) for C objects, functions, typedef names and enumeration
14 constants. (N2) for C tags. (N3) for LSL operators. I re-use the
15 old linked list to represent N1 since it is here and it is convenient
16 for representing scopes. Two more new hashtables are added to store
17 N2 and N3, each keyed on the lsymbol of the identifier. */
19 /*@constant observer char *BEGINSYMTABLE;@*/
20 # define BEGINSYMTABLE "%LCLSymbolTable"
22 /*@constant observer char *SYMTABLEEND;@*/
23 # define SYMTABLEEND "%LCLSymbolTableEnd"
25 typedef long unsigned symbolKey;
27 typedef struct _fctInfo {
29 bool export; /* all HOF maps to one sort kind: SRT_HOF */
30 /*@only@*/ signNode signature; /* in terms of sorts, no HOF */
31 /*@only@*/ pairNodeList globals; /* list of (sort globalnameSym) */
34 typedef struct _typeInfo {
37 bool abstract; /* TRUE means LCL abstract type */
38 bool modifiable; /* TRUE indicates the abstract type is mutable */
39 bool export; /* if TRUE, export it from this module */
44 VRK_CONST, /* an LCL constant */
45 VRK_ENUM, /* an enumeration constant,
46 a special kind of LCL constant */
47 VRK_VAR, /* an LCL variable */
48 VRK_PRIVATE,/* a variable private to current function/module */
49 /* function private overrides module private, usual scoping
51 VRK_GLOBAL, /* in globals of a function */
52 VRK_LET, /* local let variable in a function decl */
53 VRK_PARAM, /* formal parameters of a function/claim */
54 VRK_QUANT /* bound by a quantifier */
57 typedef struct _varInfo {
61 bool export; /* if TRUE, export it from this module */
64 /* The same lsymbol can originate from different files:
65 an LCL file or an LSL file. Each occurrence in an LCL file appears
66 as one of {opId, anyOp, logicalOp, simpleOp, eqOp, MULOP} ltoken.
67 Each occurrence in an LSL file appears as an lslOp AST. */
69 typedef struct _opInfo {
70 /*@only@*/ nameNode name;
71 /*@only@*/ sigNodeSet signatures;
74 typedef struct _tagInfo {
81 /*@null@*/ /*@dependent@*/ ltokenList enums;
82 /*@null@*/ stDeclNodeList decls;
87 IK_SORT, IK_OP, IK_TAG
99 SPE_GLOBAL, SPE_FCN, SPE_QUANT, SPE_CLAIM,
100 SPE_ABSTRACT, SPE_INVALID
103 typedef struct _scopeInfo {
108 ** A simple hash table implementation: Given a key K and a
109 ** pointer P to a piece of data, associate K with P.
111 ** Assumes that K is unsigned int, and data supports
113 ** data_key: htData * -> unsigned int
116 typedef struct _htEntry {
117 /*@only@*/ htData *data;
118 /*@only@*/ struct _htEntry *next;
121 /* Each bucket is a linked list of entries */
123 typedef htEntry bucket;
124 typedef /*@relnull@*/ /*@only@*/ bucket *o_bucket;
129 /*@relnull@*/ /*@only@*/ o_bucket *buckets;
132 /* Local to implementation */
134 typedef struct _symtableStruct *symtable;
136 extern /*@falsenull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti);
137 # define typeInfo_exists(ti) ((ti) != NULL)
139 extern /*@falsenull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi);
140 # define varInfo_exists(vi) ((vi) != NULL)
142 extern /*@falsenull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi);
143 # define tagInfo_exists(ti) ((ti) != NULL)
145 extern /*@falsenull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi);
146 # define opInfo_exists(oi) ((oi) != NULL)
148 extern /*@only@*/ symtable symtable_new (void) /*@*/ ;
149 extern void symtable_enterScope (symtable p_stable, /*@keep@*/ scopeInfo p_si);
150 extern void symtable_exitScope(symtable p_stable);
152 extern bool symtable_enterFct (symtable p_stable, /*@only@*/ fctInfo p_fi);
153 extern void symtable_enterType (symtable p_stable, /*@only@*/ typeInfo p_ti);
155 /* not only --- it is copied! */
156 extern bool symtable_enterVar (symtable p_stable, /*@temp@*/ varInfo p_vi);
157 extern void symtable_enterOp (symtable p_st,
158 /*@only@*/ /*@notnull@*/ nameNode p_n,
159 /*@owned@*/ sigNode p_oi);
160 extern bool symtable_enterTag (symtable p_st, /*@only@*/ tagInfo p_ti);
161 extern bool symtable_enterTagForce(symtable p_st, /*@only@*/ tagInfo p_ti);
163 extern bool symtable_exists(symtable p_stable, lsymbol p_i);
165 extern /*@observer@*/ /*@null@*/ typeInfo symtable_typeInfo(symtable p_stable, lsymbol p_i);
166 extern /*@observer@*/ /*@null@*/ varInfo symtable_varInfo(symtable p_stable, lsymbol p_i);
167 extern /*@observer@*/ /*@null@*/ varInfo symtable_varInfoInScope(symtable p_stable, lsymbol p_id);
168 extern /*@observer@*/ /*@null@*/ opInfo symtable_opInfo(symtable p_st,
169 /*@notnull@*/ nameNode p_n);
170 extern /*@observer@*/ /*@null@*/ tagInfo symtable_tagInfo(symtable p_st, lsymbol p_i);
172 extern void symtable_export(symtable p_stable, bool p_yesNo);
173 extern void symtable_dump(symtable p_stable, FILE *p_f, bool p_lco);
175 extern void symtable_import(tsource *p_imported, ltoken p_tok, mapping *p_map);
177 extern /*@unused@*/ void symtable_printStats (symtable p_s);
179 extern lsymbol lsymbol_sortFromType (symtable, lsymbol);
180 extern cstring tagKind_unparse (tagKind p_k);
181 extern lsymbol lsymbol_translateSort (mapping *p_m, lsymbol p_s);
182 extern void varInfo_free (/*@only@*/ varInfo p_v);
184 extern /*@only@*/ lslOpSet
185 symtable_opsWithLegalDomain (symtable p_tab, /*@temp@*/ /*@null@*/ nameNode p_n,
186 sortSetList p_argSorts, sort p_qual);
187 extern /*@observer@*/ sigNodeSet
188 symtable_possibleOps (symtable p_tab, nameNode p_n);
189 extern bool symtable_opExistsWithArity(symtable p_tab, nameNode p_n, int p_arity);
191 extern void symtable_free (/*@only@*/ symtable p_stable);
194 # error "Multiple include"