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