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 #ifndef CTE_SIMPLETYPES 25 26 #define CTE_SIMPLETYPES 27 28 #include "cio_scanner.h" 29 #include "cte_simplesorts.h" 30 31 /*---------------------------------------------------------------------*/ 32 /* Data type declarations */ 33 /*---------------------------------------------------------------------*/ 34 35 /* Representation of a simple type. A simple type can be either a 36 * constant type, or a function type whose arguments are constants 37 * (no argument can be a function). */ 38 typedef struct typecell 39 { 40 SortType domain_sort; /* domain sort, ie the sort returned by a function */ 41 int arity; /* arity of the function type */ 42 SortType* args; /* type of the function's arguments */ 43 44 struct typecell* lson; /* for sharing types */ 45 struct typecell* rson; 46 }TypeCell, *Type_p; 47 48 /* Table to store and share types */ 49 typedef struct 50 { 51 SortTable_p sort_table; /* sorts */ 52 unsigned int size; /* number of types */ 53 Type_p root; /* root of the tree of types */ 54 }TypeTableCell, *TypeTable_p; 55 56 /*---------------------------------------------------------------------*/ 57 /* Exported Functions and Variables */ 58 /*---------------------------------------------------------------------*/ 59 60 #define TypeCellAlloc() (TypeCell*)SizeMalloc(sizeof(TypeCell)) 61 #define TypeCellFree(junk) SizeFree(junk, sizeof(TypeCell)) 62 #define TypeTableCellAlloc() (TypeTableCell*)SizeMalloc(sizeof(TypeTableCell)) 63 #define TypeTableCellFree(junk) SizeFree(junk, sizeof(TypeTableCell)) 64 #define TypeArgumentAlloc(i) (SortType*) (SizeMalloc(i * sizeof(SortType))) 65 #define TypeArgumentFree(junk, i) SizeFree(junk, i*sizeof(SortType)) 66 67 #define TypeIsConstant(ty) (ty->arity == 0) 68 #define TypeIsFunction(ty) (ty->arity > 0) 69 #define TypeEqual(type1, type2) (TypeCompare((type1), (type2)) == 0) 70 71 TypeTable_p TypeTableAlloc(SortTable_p sort_table); 72 void TypeTableFree(TypeTable_p junk); 73 int TypeCompare(Type_p t1, Type_p t2); 74 Type_p TypeNewConstant(TypeTable_p table, SortType sort); 75 Type_p TypeNewFunction(TypeTable_p table, SortType sort, 76 int arity, SortType *args); 77 Type_p TypeCopyWithReturn(TypeTable_p table, Type_p source, 78 SortType new_domain); 79 void TypePrintTSTP(FILE *out, TypeTable_p table, Type_p type); 80 Type_p TypeParseTSTP(Scanner_p in, TypeTable_p table); 81 82 AVL_TRAVERSE_DECLARATION(Type, Type_p) 83 #define TypeTraverseExit(stack) PStackFree(stack) 84 85 #endif 86