1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
/*-----------------------------------------------------------------------
File : cte_typebanks.h
Author: Petar Vukmirovic
Contents
Declarations of functions needed for manipulating shared type objects.
Copyright 1998, 1999 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
-----------------------------------------------------------------------*/
#ifndef CTE_TYPEBANKS
#define CTE_TYPEBANKS
#include <cte_simpletypes.h>
#include <cio_scanner.h>
#include <clb_objtrees.h>
#include <clb_pdarrays.h>
#define TYPEBANK_SIZE 4096
#define TYPEBANK_HASH_MASK TYPEBANK_SIZE-1
#define NAME_NOT_FOUND -1
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct typebank_cell {
PStack_p back_idx; // Type constructor or simple type back index
StrTree_p name_idx; // Name to arity, type_identifier pair
// for sorts arity is always 0
long names_count; // Counter for different names inserted
TypeUniqueID types_count; // Counter for different types inserted -- Each type will
// have unique ID.
PObjTree_p hash_table[TYPEBANK_SIZE]; // Hash table for sharng
// some types that are accessed frequently.
Type_p bool_type;
Type_p i_type;
Type_p kind_type;
Type_p integer_type;
Type_p rational_type;
Type_p real_type;
Type_p default_type;
} TypeBank, *TypeBank_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define TypeBankCellAlloc() SizeMalloc(sizeof(TypeBank));
void TypeBankFree(TypeBank_p junk);
TypeBank_p TypeBankAlloc(void);
Type_p TypeBankInsertTypeShared(TypeBank_p bank, Type_p t);
TypeConsCode TypeBankDefineTypeConstructor(TypeBank_p bank, const char* name, int arity);
TypeConsCode TypeBankDefineSimpleSort(TypeBank_p bank, const char* name);
TypeConsCode TypeBankFindTCCode(TypeBank_p bank, const char* name);
int TypeBankFindTCArity(TypeBank_p bank, TypeConsCode tc_code);
const char* TypeBankFindTCName(TypeBank_p bank, TypeConsCode tc_code);
Type_p TypeBankParseType(Scanner_p in, TypeBank_p bank);
void TypePrintTSTP(FILE* out, TypeBank_p bank, Type_p type);
Type_p TypeChangeReturnType(TypeBank_p bank, Type_p type, Type_p new_ret);
void TypeBankPrintSimpleTypes(FILE* out, TypeBank_p bank);
void TypeBankAppEncodeTypes(FILE* out, TypeBank_p tb, bool print_type_comment);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
