1 /*-----------------------------------------------------------------------
2
3 File : cte_simpletypes.c
4
5 Author: Simon Cruanes (simon.cruanes@inria.fr)
6
7 Contents
8
9 Implementation of simple types for the TSTP TFF format
10
11 Copyright 2013 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> Sat Jul 6 09:45:14 CEST 2013
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "cte_simpletypes.h"
25
26 /*---------------------------------------------------------------------*/
27 /* Global Variables */
28 /*---------------------------------------------------------------------*/
29
30 /*---------------------------------------------------------------------*/
31 /* Forward Declarations */
32 /*---------------------------------------------------------------------*/
33
34
35 /*---------------------------------------------------------------------*/
36 /* Internal Functions */
37 /*---------------------------------------------------------------------*/
38
39
40
41 /*-----------------------------------------------------------------------
42 //
43 // Function: TypeAlloc
44 // Allocate a new type cell, with the given base sort and arity.
45 //
46 //
47 // Global Variables:
48 //
49 // Side Effects : Memory operations
50 //
51 /----------------------------------------------------------------------*/
TypeAlloc(SortType domain,int arity)52 Type_p TypeAlloc(SortType domain, int arity)
53 {
54 Type_p res;
55
56 res = TypeCellAlloc();
57 res->domain_sort = domain;
58 res->lson = NULL;
59 res->rson = NULL;
60 res->args = NULL;
61
62 res->arity = arity;
63 if (arity)
64 {
65 res->args = TypeArgumentAlloc(arity);
66 }
67
68 return res;
69 }
70
71
72 /*-----------------------------------------------------------------------
73 //
74 // Function: TypeFree
75 // free memory of the given type cell
76 //
77 // Global Variables:
78 //
79 // Side Effects : Memory operations
80 //
81 /----------------------------------------------------------------------*/
TypeFree(Type_p junk)82 void TypeFree(Type_p junk)
83 {
84 junk->lson = NULL;
85 junk->rson = NULL;
86
87 if (junk->arity)
88 {
89 TypeArgumentFree(junk->args, junk->arity);
90 }
91
92 TypeCellFree(junk);
93 }
94
95 /*-----------------------------------------------------------------------
96 //
97 // Function: splay_type
98 // performs the splay operation at the root of tree.
99 //
100 //
101 // Global Variables:
102 //
103 // Side Effects : modifies tree
104 //
105 /----------------------------------------------------------------------*/
splay_type(Type_p tree,Type_p splay)106 static Type_p splay_type(Type_p tree, Type_p splay)
107 {
108 Type_p left, right, tmp;
109 TypeCell new;
110 int cmpres;
111
112 if (!tree)
113 {
114 return tree;
115 }
116
117 new.lson = NULL;
118 new.rson = NULL;
119 left = &new;
120 right = &new;
121
122 for (;;)
123 {
124 cmpres = TypeCompare(splay, tree);
125 if (cmpres < 0)
126 {
127 if(!tree->lson)
128 {
129 break;
130 }
131 if(TypeCompare(splay, tree->lson) < 0)
132 {
133 tmp = tree->lson;
134 tree->lson = tmp->rson;
135 tmp->rson = tree;
136 tree = tmp;
137 if (!tree->lson)
138 {
139 break;
140 }
141 }
142 right->lson = tree;
143 right = tree;
144 tree = tree->lson;
145 }
146 else if(cmpres > 0)
147 {
148 if (!tree->rson)
149 {
150 break;
151 }
152 if(TypeCompare(splay, tree->rson) > 0)
153 {
154 tmp = tree->rson;
155 tree->rson = tmp->lson;
156 tmp->lson = tree;
157 tree = tmp;
158 if (!tree->rson)
159 {
160 break;
161 }
162 }
163 left->rson = tree;
164 left = tree;
165 tree = tree->rson;
166 }
167 else
168 {
169 break;
170 }
171 }
172 left->rson = tree->lson;
173 right->lson = tree->rson;
174 tree->lson = new.rson;
175 tree->rson = new.lson;
176
177 return tree;
178 }
179
180 /*-----------------------------------------------------------------------
181 //
182 // Function: TypeTreeFind()
183 //
184 // Find a entry in the type tree
185 //
186 // Global Variables: -
187 //
188 // Side Effects : -
189 //
190 /----------------------------------------------------------------------*/
191
TypeTreeFind(Type_p * root,Type_p key)192 Type_p TypeTreeFind(Type_p *root, Type_p key)
193 {
194 if(*root)
195 {
196 *root = splay_type(*root, key);
197 if(TypeEqual(*root, key))
198 {
199 return *root;
200 }
201 }
202 return NULL;
203 }
204
205
206 /*-----------------------------------------------------------------------
207 //
208 // Function: TypeTreeInsert()
209 //
210 // Insert a type in the tree. If the type already exists,
211 // return pointer to existing entry as usual, otherwise return NULL.
212 //
213 // Global Variables: -
214 //
215 // Side Effects : Changes tree
216 //
217 /----------------------------------------------------------------------*/
218
TypeTreeInsert(Type_p * root,Type_p new)219 Type_p TypeTreeInsert(Type_p *root, Type_p new)
220 {
221 int cmpres;
222
223 if (!*root)
224 {
225 new->lson = new->rson = NULL;
226 *root = new;
227 return NULL;
228 }
229 *root = splay_type(*root, new);
230
231 cmpres = TypeCompare(new, *root);
232
233 if (cmpres < 0)
234 {
235 new->lson = (*root)->lson;
236 new->rson = *root;
237 (*root)->lson = NULL;
238 *root = new;
239 return NULL;
240 }
241 else if(cmpres > 0)
242 {
243 new->rson = (*root)->rson;
244 new->lson = *root;
245 (*root)->rson = NULL;
246 *root = new;
247 return NULL;
248 }
249 return *root;
250 }
251
252
253 /*-----------------------------------------------------------------------
254 //
255 // Function: TypeTreeExtract()
256 //
257 // Remove a type cell from the tree and return a pointer to it.
258 //
259 // Global Variables: -
260 //
261 // Side Effects : Changes tree
262 //
263 /----------------------------------------------------------------------*/
264
TypeTreeExtract(Type_p * root,Type_p key)265 Type_p TypeTreeExtract(Type_p *root, Type_p key)
266 {
267 Type_p x, cell;
268
269 if (!(*root))
270 {
271 return NULL;
272 }
273 *root = splay_type(*root, key);
274 if(TypeEqual(key, (*root)))
275 {
276 if (!(*root)->lson)
277 {
278 x = (*root)->rson;
279 }
280 else
281 {
282 x = splay_type((*root)->lson, key);
283 x->rson = (*root)->rson;
284 }
285 cell = *root;
286 cell->lson = cell->rson = NULL;
287 *root = x;
288 return cell;
289 }
290 return NULL;
291 }
292
293
294 /*-----------------------------------------------------------------------
295 //
296 // Function: parse_sort_list
297 // Parses a list of sorts, separated by "*" into the given array.
298 // Will also consume the opening and trailing parenthesis.
299 //
300 // It returns the number of parsed sorts.
301 //
302 // Global Variables: -
303 //
304 // Side Effects : Modifies scanner, args and len
305 //
306 /----------------------------------------------------------------------*/
parse_sort_list(Scanner_p in,SortTable_p sort_table,SortType ** args,int * len)307 int parse_sort_list(Scanner_p in, SortTable_p sort_table, SortType **args, int *len)
308 {
309 SortType sort;
310 int arity;
311
312 *len = 5;
313 *args = SecureMalloc((*len) * sizeof(SortType));
314
315 AcceptInpTok(in, OpenBracket);
316
317 sort = SortParseTSTP(in, sort_table);
318 (*args)[0] = sort;
319 arity = 1;
320
321 while(TestInpTok(in, Mult))
322 {
323 AcceptInpTok(in, Mult);
324 sort = SortParseTSTP(in, sort_table);
325
326 /* may have to resize args */
327 if(arity == *len)
328 {
329 *len += 5;
330 *args = SecureRealloc(*args, (*len) * sizeof(SortType));
331 }
332 (*args)[arity]= sort;
333 arity++;
334 }
335 AcceptInpTok(in, CloseBracket);
336
337 return arity;
338 }
339
340
341 /*---------------------------------------------------------------------*/
342 /* Exported Functions */
343 /*---------------------------------------------------------------------*/
344
345
346 /*-----------------------------------------------------------------------
347 //
348 // Function: TypeTableAlloc
349 // allocates and initialize a table that stores and shares types. It depends on,
350 // but does not own, a sort table.
351 //
352 //
353 // Global Variables:
354 //
355 // Side Effects : Memory operations
356 //
357 /----------------------------------------------------------------------*/
TypeTableAlloc(SortTable_p sort_table)358 TypeTable_p TypeTableAlloc(SortTable_p sort_table)
359 {
360 TypeTable_p res;
361
362 res = TypeTableCellAlloc();
363 res->sort_table = sort_table;
364 res->size = 0;
365 res->root = NULL;
366
367 return res;
368 }
369
370
371 /*-----------------------------------------------------------------------
372 //
373 // Function: TypeTableFree
374 // free the content of the type table (all types) and the table itself
375 //
376 //
377 //
378 // Global Variables:
379 //
380 // Side Effects : Memory operations
381 //
382 /----------------------------------------------------------------------*/
TypeTableFree(TypeTable_p junk)383 void TypeTableFree(TypeTable_p junk)
384 {
385 Type_p type;
386
387 // free all types, removing them one by one
388 while (junk->root)
389 {
390 type = TypeTreeExtract(&(junk->root), junk->root);
391 TypeFree(type);
392 }
393
394 TypeTableCellFree(junk);
395 }
396
397
398 /*-----------------------------------------------------------------------
399 //
400 // Function: TypeNewConstant
401 // Build a new constant type
402 //
403 //
404 // Global Variables: -
405 //
406 // Side Effects : Modifies the type table
407 //
408 /----------------------------------------------------------------------*/
TypeNewConstant(TypeTable_p table,SortType sort)409 Type_p TypeNewConstant(TypeTable_p table, SortType sort)
410 {
411 Type_p type, res;
412
413 type = TypeAlloc(sort, 0);
414 res = TypeTreeInsert(&(table->root), type);
415 if(!res)
416 {
417 return type;
418 }
419 TypeFree(type);
420 return res;
421 }
422
423
424 /*-----------------------------------------------------------------------
425 //
426 // Function: TypeNewFunction()
427 //
428 // Build a new function type.
429 //
430 // Global Variables: -
431 //
432 // Side Effects : Modifies the type table
433 //
434 /----------------------------------------------------------------------*/
435
TypeNewFunction(TypeTable_p table,SortType sort,int arity,SortType * args)436 Type_p TypeNewFunction(TypeTable_p table, SortType sort,
437 int arity, SortType *args)
438 {
439 Type_p type, res;
440
441 type = TypeAlloc(sort, arity);
442 for(int i=0; i < arity; i++)
443 {
444 type->args[i] = args[i];
445 }
446
447 res = TypeTreeInsert(&(table->root), type);
448 if(!res)
449 {
450 return type;
451 }
452 TypeFree(type);
453 return res;
454 }
455
456
457 /*-----------------------------------------------------------------------
458 //
459 // Function: TypeCompare()
460 //
461 // Implement total order on types.
462 //
463 // Global Variables: -
464 //
465 // Side Effects : -
466 //
467 /----------------------------------------------------------------------*/
468
TypeCompare(Type_p t1,Type_p t2)469 int TypeCompare(Type_p t1, Type_p t2)
470 {
471 int res;
472
473 res = t1->domain_sort - t2->domain_sort;
474 if(res)
475 {
476 return res;
477 }
478
479 res = t1->arity - t2->arity;
480 if(res)
481 {
482 return res;
483 }
484
485 // same domain and arity, lexicographic comparison of arguments
486 assert (t1->arity == t2->arity);
487 for(int i = 0; !res && i < t1->arity; i++)
488 {
489 res = t1->args[i] - t2->args[i];
490 if(res)
491 {
492 return res;
493 }
494 }
495 return res;
496 }
497
498
499 /*-----------------------------------------------------------------------
500 //
501 // Function: TypeCopyWithReturn()
502 //
503 // Return a copy of this term, but with the given domain_sort.
504 //
505 // Global Variables: -
506 //
507 // Side Effects : insert a type in the table
508 //
509 /----------------------------------------------------------------------*/
510
TypeCopyWithReturn(TypeTable_p table,Type_p source,SortType new_domain)511 Type_p TypeCopyWithReturn(TypeTable_p table, Type_p source,
512 SortType new_domain)
513 {
514 return TypeNewFunction(table, new_domain, source->arity, source->args);
515 }
516
517 /*-----------------------------------------------------------------------
518 //
519 // Function: TypePrintTSTP()
520 //
521 // Prints the type in TSTP TFF syntax.
522 //
523 // Global Variables:
524 //
525 // Side Effects : IO
526 //
527 /----------------------------------------------------------------------*/
528
TypePrintTSTP(FILE * out,TypeTable_p table,Type_p type)529 void TypePrintTSTP(FILE *out, TypeTable_p table, Type_p type)
530 {
531 int i;
532
533 if (TypeIsConstant(type))
534 {
535 SortPrintTSTP(out, table->sort_table, type->domain_sort);
536 }
537 else
538 {
539 if (type->arity == 1)
540 {
541 SortPrintTSTP(out, table->sort_table, type->args[0]);
542 }
543 else
544 {
545 fputc('(', out);
546 SortPrintTSTP(out, table->sort_table, type->args[0]);
547 for (i = 1; i < type->arity; i++)
548 {
549 fputs("*", out);
550 SortPrintTSTP(out, table->sort_table, type->args[i]);
551 }
552 fputc(')', out);
553 }
554 fputc('>', out);
555 SortPrintTSTP(out, table->sort_table, type->domain_sort);
556 }
557 }
558
559
560 /*-----------------------------------------------------------------------
561 //
562 // Function: TypeParseTSTP()
563 //
564 // Parses a type in TSTP TFF format.
565 //
566 // Global Variables: -
567 //
568 // Side Effects : reads from the scanner
569 //
570 /----------------------------------------------------------------------*/
571
TypeParseTSTP(Scanner_p in,TypeTable_p table)572 Type_p TypeParseTSTP(Scanner_p in, TypeTable_p table)
573 {
574 SortType left, right, *args = NULL;
575 int arity, len;
576 Type_p res;
577
578 left = right = STNoSort;
579
580 if (TestInpTok(in, OpenBracket))
581 {
582 /* Function type */
583 arity = parse_sort_list(in, table->sort_table, &args, &len);
584 AcceptInpTok(in, GreaterSign);
585 right = SortParseTSTP(in, table->sort_table);
586 assert(right!=STNoSort);
587
588 res = TypeNewFunction(table, right, arity, args);
589 FREE(args);
590 }
591 else
592 {
593 left = SortParseTSTP(in, table->sort_table);
594 assert(left!=STNoSort);
595 if (TestInpTok(in, GreaterSign))
596 {
597 /* Unary function type */
598 AcceptInpTok(in, GreaterSign);
599 right = SortParseTSTP(in, table->sort_table);
600 args = SizeMalloc(sizeof(SortType));
601 args[0] = left;
602 res = TypeNewFunction(table, right, 1, args);
603 SizeFree(args, sizeof(SortType));
604 }
605 else
606 {
607 /* constant type */
608 res = TypeNewConstant(table, left);
609 }
610 }
611 return res;
612 }
613
614
615 AVL_TRAVERSE_DEFINITION(Type, Type_p)
616