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