1 /*----------------------------------------------------------------------- 2 3 File : cte_simplesorts.h 4 5 Author: Stephan Schulz (schulz@eprover.org) 6 7 Contents 8 9 Data structure and function interfaces for managing simple, disjoint 10 sorts. 11 12 Copyright 2007 by the author. 13 This code is released under the GNU General Public Licence and 14 the GNU Lesser General Public License. 15 See the file COPYING in the main E directory for details.. 16 Run "eprover -h" for contact information. 17 18 Changes 19 20 <1> Sat Sep 15 01:33:52 EDT 2007 21 New 22 23 -----------------------------------------------------------------------*/ 24 25 #ifndef CTE_SIMPLESORTS 26 27 #define CTE_SIMPLESORTS 28 29 #include <clb_stringtrees.h> 30 #include <cio_scanner.h> 31 32 /*---------------------------------------------------------------------*/ 33 /* Data type declarations */ 34 /*---------------------------------------------------------------------*/ 35 36 /* Build-in sorts for the many-sorted logic E is being moved to. Note 37 * that the system relies on the fact that the system-defined sorts are 38 * inserted in a specific order. 39 * 40 * User sorts are integers bigger than STPredefined. */ 41 42 typedef int SortType; 43 44 #define STNoSort 0 45 #define STBool 1 /* Boolean sort, will replace/extend the predicate bit */ 46 #define STIndividuals 2 /* Default sort, "individuums" */ 47 #define STKind 3 /* The "sort of sorts", $tType in TFF */ 48 #define STInteger 4 /* Integer numbers */ 49 #define STRational 5 /* Rational numbers */ 50 #define STReal 6 /* Reals */ 51 #define STPredefined STReal 52 53 /* Datatype for representing the sort system. Currenlty associates 54 * sort types with encodings and tracks the default sort. */ 55 56 typedef struct sort_table 57 { 58 SortType default_type; /* Sort of undeclared function 59 * symbols. STIndividuals by default, but 60 * can be changed */ 61 StrTree_p sort_index; /* Associates a sort name with the type */ 62 PStack_p back_index; /* Back-Association from type to 63 string. Position i on the stack 64 contains the key of sort i in the 65 sort_index. */ 66 }SortTableCell, *SortTable_p; 67 68 69 70 /*---------------------------------------------------------------------*/ 71 /* Exported Functions and Variables */ 72 /*---------------------------------------------------------------------*/ 73 74 #define SortTableCellAlloc() (SortTableCell*)SizeMalloc(sizeof(SortTableCell)) 75 #define SortTableCellFree(junk) SizeFree(junk, sizeof(SortTableCell)) 76 #define SortIsUserDefined(sort) (sort > STPredefined) 77 78 #define SortIsInterpreted(sort) (((sort)>=STInteger)&&((sort)<=STReal)) 79 80 SortTable_p SortTableAlloc(void); 81 void SortTableFree(SortTable_p junk); 82 SortType SortTableInsert(SortTable_p table, char* sort_name); 83 SortTable_p DefaultSortTableAlloc(void); 84 char* SortTableGetRep(SortTable_p table, SortType sort); 85 SortType SortParseTSTP(Scanner_p in, SortTable_p table); 86 void SortPrintTSTP(FILE *out, SortTable_p table, SortType sort); 87 void SortTablePrint(FILE* out, SortTable_p table); 88 89 90 #endif 91 92 /*---------------------------------------------------------------------*/ 93 /* End of File */ 94 /*---------------------------------------------------------------------*/ 95