1 /*-----------------------------------------------------------------------
2 
3 File  : cte_functypes.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Simple, widely used functions for dealing with function symbols and
10   operators.
11 
12   Copyright 1998, 1999 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> Sun Nov  9 23:09:33 MET 1997
21     New
22 
23 -----------------------------------------------------------------------*/
24 
25 #ifndef CTE_FUNCTYPES
26 
27 #define CTE_FUNCTYPES
28 
29 #include <cio_basicparser.h>
30 
31 
32 /*---------------------------------------------------------------------*/
33 /*                    Data type declarations                           */
34 /*---------------------------------------------------------------------*/
35 
36 /* Data type repesenting the various types of encodings for function
37  * symols (including constants) and predicates. */
38 
39 typedef enum
40 {
41    FSNone,
42    FSIdentVar,         /* Ident, starts with capital letter or _ */
43    FSIdentFreeFun,     /* Ident, starts with Lower case letter or SQString */
44    FSIdentInt,         /* Integer */
45    FSIdentFloat,       /* Floating point number */
46    FSIdentRational,    /* Rational number */
47    FSIdentInterpreted, /* SemIdent */
48    FSIdentObject       /* String "in double quotes" */
49 }FuncSymbType;
50 
51 /*---------------------------------------------------------------------*/
52 /*                Exported Functions and Variables                     */
53 /*---------------------------------------------------------------------*/
54 
55 /* Function symbols in terms are represented by positive numbers,
56    variables by negative numbers. This alias allows clearer
57    specifications. */
58 
59 typedef long FunCode;
60 
61 extern TokenType FuncSymbToken;
62 extern TokenType FuncSymbStartToken;
63 
64 FuncSymbType FuncSymbParse(Scanner_p in, DStr_p id);
65 
66 
67 #endif
68 
69 /*---------------------------------------------------------------------*/
70 /*                        End of File                                  */
71 /*---------------------------------------------------------------------*/
72 
73 
74 
75 
76 
77