1 /*-----------------------------------------------------------------------
2
3 File : cte_simplesorts.c
4
5 Author: Stephan Schulz (schulz@eprover.org)
6
7 Contents
8
9 Implementation of the simple sort table infrastructure.
10
11 Copyright 2007 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> Mon Sep 17 21:43:28 EDT 2007
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "cte_simplesorts.h"
25 #include "cte_functypes.c"
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31
32 /*---------------------------------------------------------------------*/
33 /* Forward Declarations */
34 /*---------------------------------------------------------------------*/
35
36
37 /*---------------------------------------------------------------------*/
38 /* Internal Functions */
39 /*---------------------------------------------------------------------*/
40
41 /*-----------------------------------------------------------------------
42 //
43 // Function: default_sort_table_init()
44 //
45 // Add the default types in proper order.
46 //
47 // Global Variables: -
48 //
49 // Side Effects : Indirectly via SortTableInsert()
50 //
51 /----------------------------------------------------------------------*/
default_sort_table_init(SortTable_p table)52 void default_sort_table_init(SortTable_p table)
53 {
54 SortType res;
55
56 res = SortTableInsert(table, "$no_type");
57 UNUSED(res); assert(res == STNoSort);
58 res = SortTableInsert(table, "$o");
59 UNUSED(res); assert(res == STBool);
60 res = SortTableInsert(table, "$i");
61 UNUSED(res); assert(res == STIndividuals);
62 res = SortTableInsert(table, "$tType");
63 UNUSED(res); assert(res == STKind);
64 res = SortTableInsert(table, "$int");
65 UNUSED(res); assert(res == STInteger);
66 res = SortTableInsert(table, "$rat");
67 UNUSED(res); assert(res == STRational);
68 res = SortTableInsert(table, "$real");
69 UNUSED(res); assert(res == STReal);
70 }
71
72
73 /*---------------------------------------------------------------------*/
74 /* Exported Functions */
75 /*---------------------------------------------------------------------*/
76
77 /*-----------------------------------------------------------------------
78 //
79 // Function: SortTableAlloc()
80 //
81 // Allocate an empty but initialized sort table.
82 //
83 // Global Variables: -
84 //
85 // Side Effects : Memory operations
86 //
87 /----------------------------------------------------------------------*/
88
SortTableAlloc(void)89 SortTable_p SortTableAlloc(void)
90 {
91 SortTable_p table = SortTableCellAlloc();
92
93 table->sort_index = NULL;
94 table->back_index = PStackAlloc();
95 table->default_type = STIndividuals;
96
97 return table;
98 }
99
100 /*-----------------------------------------------------------------------
101 //
102 // Function: SortTableFree()
103 //
104 // Free a SortTable.
105 //
106 // Global Variables: -
107 //
108 // Side Effects : Memory operations.
109 //
110 /----------------------------------------------------------------------*/
111
SortTableFree(SortTable_p junk)112 void SortTableFree(SortTable_p junk)
113 {
114 assert(junk);
115
116 PStackFree(junk->back_index);
117 if (junk->sort_index)
118 {
119 StrTreeFree(junk->sort_index);
120 }
121 SortTableCellFree(junk);
122 }
123
124 /*-----------------------------------------------------------------------
125 //
126 // Function: SortTableInsert()
127 //
128 // Add an entry (i.e. sort name) to the table (if unknown) and
129 // retrieve its encoding.
130 //
131 // Global Variables: -
132 //
133 // Side Effects : Memory operations.
134 //
135 /----------------------------------------------------------------------*/
136
SortTableInsert(SortTable_p table,char * sort_name)137 SortType SortTableInsert(SortTable_p table, char* sort_name)
138 {
139 StrTree_p cell = StrTreeFind(&(table->sort_index), sort_name);
140
141 if(!cell)
142 {
143 IntOrP sort_val;
144
145 sort_val.i_val = PStackGetSP(table->back_index);
146 cell = StrTreeStore(&(table->sort_index), sort_name, sort_val, sort_val);
147 assert(cell);
148 PStackPushP(table->back_index, cell->key);
149 }
150 return cell->val1.i_val;
151 }
152
153
154 /*-----------------------------------------------------------------------
155 //
156 // Function: DefaultSortTableAlloc()
157 //
158 // Allocate a sort table and insert the system-defined sorts in the
159 // proper order for their reserved names to work.
160 //
161 // Global Variables: -
162 //
163 // Side Effects : Memory operations
164 //
165 /----------------------------------------------------------------------*/
166
DefaultSortTableAlloc(void)167 SortTable_p DefaultSortTableAlloc(void)
168 {
169 SortTable_p table = SortTableAlloc();
170 default_sort_table_init(table);
171
172 return table;
173 }
174
175
176 /*-----------------------------------------------------------------------
177 //
178 // Function: SortTableGetRep()
179 //
180 // Given a sort, return a pointer to its external representation.
181 //
182 // Global Variables: -
183 //
184 // Side Effects : -
185 //
186 /----------------------------------------------------------------------*/
SortTableGetRep(SortTable_p table,SortType sort)187 char* SortTableGetRep(SortTable_p table, SortType sort)
188 {
189 return PStackElementP(table->back_index, sort);
190 }
191
192 /*-----------------------------------------------------------------------
193 //
194 // Function: SortPrintTSTP()
195 //
196 // Print a sort in the TSTP format
197 //
198 // Global Variables: -
199 //
200 // Side Effects : Output
201 //
202 /----------------------------------------------------------------------*/
SortPrintTSTP(FILE * out,SortTable_p table,SortType sort)203 void SortPrintTSTP(FILE *out, SortTable_p table, SortType sort)
204 {
205 char *name;
206
207 name = SortTableGetRep(table, sort);
208 fputs(name, out);
209 }
210
211 /*-----------------------------------------------------------------------
212 //
213 // Function: SortParseTSTP
214 // parse a sort in the TSTP format
215 //
216 //
217 // Global Variables: -
218 //
219 // Side Effects : Reads from scanner, modifies sort table
220 //
221 /----------------------------------------------------------------------*/
SortParseTSTP(Scanner_p in,SortTable_p table)222 SortType SortParseTSTP(Scanner_p in, SortTable_p table)
223 {
224 DStr_p id;
225 FuncSymbType functype;
226 SortType sort = STNoSort;
227
228 id = DStrAlloc();
229 functype = FuncSymbParse(in, id);
230 if(functype == FSIdentFreeFun || functype == FSIdentInterpreted)
231 {
232 sort = SortTableInsert(table, DStrView(id));
233 }
234 else
235 {
236 AktTokenError(in, "Expected TSTP sort", false);
237 }
238
239 DStrFree(id);
240 return sort;
241 }
242
243 /*-----------------------------------------------------------------------
244 //
245 // Function: SortTablePrint()
246 //
247 // Print a sort table (mainly for debugging)
248 //
249 // Global Variables: -
250 //
251 // Side Effects : Output
252 //
253 /----------------------------------------------------------------------*/
SortTablePrint(FILE * out,SortTable_p table)254 void SortTablePrint(FILE* out, SortTable_p table)
255 {
256 PStackPointer i;
257 StrTree_p cell;
258 PStack_p stack;
259
260 fprintf(out, "Sort table in order of sort creation:\n");
261 fprintf(out, "=====================================\n");
262 for(i=0; i<PStackGetSP(table->back_index); i++)
263 {
264 fprintf(out, "Type %4ld: %s\n", i, SortTableGetRep(table, i));
265 }
266 fprintf(out, "\nSort table in alphabetic order:\n");
267 fprintf(out, "=====================================\n");
268
269
270 stack = StrTreeTraverseInit(table->sort_index);
271 while((cell=StrTreeTraverseNext(stack)))
272 {
273 fprintf(out, "Type %4ld: %s\n", cell->val1.i_val, cell->key);
274 }
275 PStackFree(stack);
276 fprintf(out, "\n");
277 }
278
279
280 /*---------------------------------------------------------------------*/
281 /* End of File */
282 /*---------------------------------------------------------------------*/
283
284
285