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