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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
/*-----------------------------------------------------------------------
File : cte_simpletypes.c
Author: Simon Cruanes (simon.cruanes@inria.fr)
Contents
Implementation of simple types for the TSTP TFF format
Copyright 2013 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.
Changes
<2> Somewhere at the end of 2017. Completely rewritten
by Petar Vukmirovic.
<1> Sat Jul 6 09:45:14 CEST 2013
New
-----------------------------------------------------------------------*/
#ifndef CTE_SIMPLETYPES
#define CTE_SIMPLETYPES
#include "cio_scanner.h"
#include <clb_ptrees.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
#define ArrowTypeCons 0
#define STBool 1 /* Boolean sort, will replace/extend the predicate bit */
#define STIndividuals 2 /* Default sort, "individuums" */
#define STKind 3 /* The "sort of sorts", $tType in TFF */
#define STInteger 4 /* Integer numbers */
#define STRational 5 /* Rational numbers */
#define STReal 6 /* Reals */
#define STPredefined STReal
typedef long TypeUniqueID;
typedef long TypeConsCode;
typedef struct typecell {
TypeConsCode f_code; // Called the same as for terms.
int arity;
struct typecell** args;
TypeUniqueID type_uid;
} TypeCell, *Type_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define SortIsUserDefined(sort) ((sort) > STPredefined)
#define SortIsInterpreted(sort) (((sort)>=STInteger)&&((sort)<=STPredefined))
Type_p GetReturnSort(Type_p type);
#define NO_TYPE NULL
#define INVALID_TYPE_UID -1
#define TypeIsKind(t) ((t)->f_code == STKind)
#define TypeIsBool(t) ((t)->f_code == STBool)
#define TypeIsArrow(t) ((t)->f_code == ArrowTypeCons)
#define TypeIsPredicate(t) (TypeIsBool(t) || (TypeIsArrow(t) && TypeIsBool((t)->args[(t)->arity-1])))
#define TypeCellAlloc() (Type_p) SizeMalloc(sizeof(TypeCell))
#define TypeCellFree(junk) SizeFree(junk, sizeof(TypeCell))
Type_p TypeCopy(Type_p orig);
#define AllocSimpleSort(code) TypeAlloc((code), 0, NULL)
#define AllocArrowType(arity, args) TypeAlloc(ArrowTypeCons, (arity), (args))
#define TypeArgArrayAlloc(n) ((Type_p*) ((n) == 0 ? NULL : SizeMalloc((n)*sizeof(Type_p))))
#define TypeArgArrayFree(junk, n) (((n)==0) ? NULL : ( SizeFreeReal((junk),((n)*sizeof(Type_p))) ))
#define TypeIsArrow(t) ((t)->f_code == ArrowTypeCons)
#define TypeIsKind(t) ((t)->f_code == STKind)
#define TypeIsIndividual(t) ((t)->f_code == STIndividuals)
#define TypeIsTypeConstructor(t) (TypeIsKind(t) || (TypeIsArrow(t) && TypeIsKind((t)->args[0])))
#define GetRetType(t) (TypeIsArrow(t) ? (t)->args[(t)->arity-1] : (t))
int TypeGetMaxArity(Type_p t);
int TypesCmp(Type_p t1, Type_p t2);
Type_p FlattenType(Type_p type);
DStr_p TypeAppEncodedName(Type_p type);
Type_p ArrowTypeFlattened(Type_p const* args, int args_num, Type_p ret);
Type_p TypeDropFirstArg(Type_p ty);
bool TypeHasBool(Type_p t);
void TypeFree(Type_p junk);
/*-----------------------------------------------------------------------
//
// Function: TypeAlloc()
//
// Allocates new type cell.
//
//
// Global Variables: -
//
// Side Effects : -
//
/----------------------------------------------------------------------*/
static inline Type_p TypeAlloc(TypeConsCode c_code, int arity, Type_p* args)
{
Type_p handle = TypeCellAlloc();
handle->f_code = c_code;
handle->arity = arity;
handle->args = args;
handle->type_uid = INVALID_TYPE_UID;
return handle;
}
/*-----------------------------------------------------------------------
//
// Function: AllocArrowTypeCopyArgs()
//
// Allocates an arrow type where arguments of arrow are represented
// in a statically allocated array -- thus we need to dynamically
// allocate them and copy them in the dynamic array.
//
//
// Global Variables: -
//
// Side Effects : -
//
/----------------------------------------------------------------------*/
static inline Type_p AllocArrowTypeCopyArgs(int arity, Type_p const* args)
{
assert(arity > 0);
Type_p* args_copy = TypeArgArrayAlloc(arity);
for(int i=0; i<arity; i++)
{
args_copy[i] = args[i];
}
return AllocArrowType(arity, args_copy); //casting away the cons
}
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
