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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
|
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * VARCONTS FOR VARIABLES * */
/* * * */
/* * $Module: VARCONT * */
/* * * */
/* * Copyright (C) 1997, 1998, 1999, 2000, 2001 * */
/* * MPI fuer Informatik * */
/* * * */
/* * This program is free software; you can redistribute * */
/* * it and/or modify it under the terms of the FreeBSD * */
/* * Licence. * */
/* * * */
/* * This program is distributed in the hope that it will * */
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
/* * for more details. * */
/* * * */
/* * * */
/* $Revision: 1.7 $ * */
/* $State: Exp $ * */
/* $Date: 2011-11-27 11:18:20 $ * */
/* $Author: weidenb $ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: spass@mpi-inf.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile: context.h,v $ */
#define SHOWBINDINGS 0
#ifndef _VARCONT_
#define _VARCONT_
/**************************************************************/
/* Includes */
/**************************************************************/
#include "term.h"
#include "symbol.h"
#include "list.h"
/**************************************************************/
/* Structures */
/**************************************************************/
/* Set 'SHOWBINDINGS' to non-zero value to enable debug output. */
/* #define SHOWBINDINGS 1 */
#define cont__SIZE symbol__MAXVARIABLES
extern int cont_NOOFVARCONTS;
extern LIST cont_LISTOFVARCONTS;
extern intptr_t cont_BINDINGS;
/* An array to remember bindings for the variables. The array */
/* is indexed by the variable index and holds the binding term. */
typedef struct binding {
SYMBOL symbol;
SYMBOL renaming;
TERM term;
struct binding *context;
struct binding *link;
} *VARCONT, VARCONT_NODE;
extern VARCONT cont_LASTBINDING; /* The last binding made. */
extern VARCONT cont_CURRENTBINDING; /* Help variable. */
extern SYMBOL cont_INDEXVARSCANNER;
/* Two contexts are allocated by default */
extern VARCONT cont_LEFTVARCONT;
extern VARCONT cont_RIGHTVARCONT;
extern VARCONT cont_INSTANCEVARCONT; /* This context is used as a label only (dummy context) */
VARCONT cont_LeftContext(void);
VARCONT cont_RightContext(void);
VARCONT cont_InstanceContext(void);
/**************************************************************/
/* Binding Functions */
/**************************************************************/
void cont_BackTrackLastBindingHelp(void);
VARCONT cont_ContextOfBinding(VARCONT);
void cont_CreateBindingHelp(VARCONT, SYMBOL, VARCONT, TERM);
void cont_BindingOutput(VARCONT C, SYMBOL Var);
/**************************************************************/
/* A stack for the number of established bindings */
/**************************************************************/
#define cont__STACKSIZE 1000
typedef int cont_STACK_TYPE[cont__STACKSIZE];
extern cont_STACK_TYPE cont_STACK;
extern int cont_STACKPOINTER;
/* Stack operations */
void cont_StackInit(void);
void cont_StackPush(int Entry);
void cont_StackPop(void);
int cont_StackPopResult(void);
void cont_StackNPop(int N);
intptr_t cont_StackTop(void);
int cont_StackNthTop(int N);
void cont_StackRplacTop(int Entry);
void cont_StackRplacNthTop(int N, int Entry);
void cont_StackRplacNth(int N, int Entry);
intptr_t cont_StackBottom(void);
void cont_StackSetBottom(int Pointer);
BOOL cont_StackEmpty(int Pointer);
void cont_StartBinding(void);
int cont_BindingsSinceLastStart(void);
void cont_StopAndStartBinding(void);
/**************************************************************/
/* Access */
/**************************************************************/
VARCONT cont_Binding(VARCONT C, SYMBOL Var);
VARCONT cont_BindingLink(VARCONT B);
void cont_SetBindingLink(VARCONT B, VARCONT L);
TERM cont_BindingTerm(VARCONT B);
void cont_SetBindingTerm(VARCONT B, TERM T);
SYMBOL cont_BindingSymbol(VARCONT B);
void cont_SetBindingSymbol(VARCONT B, SYMBOL S);
SYMBOL cont_BindingRenaming(VARCONT B);
void cont_SetBindingRenaming(VARCONT B, SYMBOL S);
VARCONT cont_BindingContext(VARCONT B);
void cont_SetBindingContext(VARCONT B, VARCONT C);
VARCONT cont_ContextBindingLink(VARCONT C,SYMBOL Var);
TERM cont_ContextBindingTerm(VARCONT C,SYMBOL Var);
void cont_SetContextBindingTerm(VARCONT C, SYMBOL Var, TERM t);
SYMBOL cont_ContextBindingSymbol(VARCONT C,SYMBOL Var);
SYMBOL cont_ContextBindingRenaming(VARCONT C,SYMBOL Var);
void cont_SetContextBindingRenaming(VARCONT C, SYMBOL Var,
SYMBOL R);
VARCONT cont_ContextBindingContext(VARCONT C,SYMBOL Var);
/**************************************************************/
/* Predicates */
/**************************************************************/
BOOL cont_VarIsBound(VARCONT C, SYMBOL Var);
BOOL cont_VarIsUsed(VARCONT C, SYMBOL Var);
BOOL cont_VarIsLinked(VARCONT C, SYMBOL Var);
BOOL cont_VarIsRenamed(VARCONT C, SYMBOL Var);
BOOL cont_VarIsClosed(VARCONT C,SYMBOL Var);
BOOL cont_BindingIsBound(VARCONT B);
BOOL cont_BindingIsUsed(VARCONT B);
BOOL cont_IsBoundToVar(VARCONT C);
/**************************************************************/
/* Aux functions for backtracking */
/**************************************************************/
VARCONT cont_LastBinding(void);
void cont_SetLastBinding(VARCONT B);
TERM cont_LastBindingTerm(void);
SYMBOL cont_LastBindingSymbol(void);
VARCONT cont_LastBindingContext(void);
BOOL cont_LastIsBound(void);
BOOL cont_LastIsUsed(void);
BOOL cont_LastIsClosed(void);
BOOL cont_IsInContext(VARCONT C, SYMBOL Var, VARCONT B);
/**************************************************************/
/* Initialization */
/**************************************************************/
void cont_InitBinding(VARCONT C, SYMBOL Var);
void cont_InitContext(VARCONT C);
/**************************************************************/
/* Creation and deletion of contexts */
/**************************************************************/
VARCONT cont_Create(void);
void cont_Delete(VARCONT C);
void cont_ResetIndexVarScanner(void);
/**************************************************************/
/* Output bindings */
/**************************************************************/
void cont_PrintCurrentTrail(void);
/**************************************************************/
/* Check Current Trail */
/**************************************************************/
BOOL cont_OnlyVariablesInCoDomOfCurrentTrail();
/**************************************************************/
/* Close bindings */
/**************************************************************/
void cont_CloseBindingHelp(VARCONT C, SYMBOL Var);
void cont_CloseBindingBindingHelp(VARCONT B);
void cont_CloseBinding(VARCONT C, SYMBOL Var);
void cont_CloseBinding(VARCONT C, SYMBOL Var);
void cont_CloseBindingBinding(VARCONT B);
/**************************************************************/
/* Establish bindings */
/**************************************************************/
int cont_CreateBinding(VARCONT C, SYMBOL Var, VARCONT CTerm, TERM Term);
int cont_CreateClosedBinding(VARCONT C, SYMBOL Var);
int cont_CreateBinding(VARCONT C, SYMBOL Var, VARCONT CTerm, TERM Term);
int cont_CreateClosedBinding(VARCONT C, SYMBOL Var);
/**************************************************************/
/* Backtracking */
/**************************************************************/
void cont_BackTrackLastBinding(void);
int cont_BackTrack(void);
int cont_StopAndBackTrack(void);
int cont_BackTrackAndStart(void);
void cont_Reset(void);
void cont_BackTrackLastBinding(void);
int cont_BackTrack(void);
int cont_StopAndBackTrack(void);
int cont_BackTrackAndStart(void);
void cont_Reset(void);
/**************************************************************/
/* Check state of bindings */
/**************************************************************/
#define cont__CHECKSTACKSIZE 1000
#define cont__CHECKSTACKEMPTY 0
typedef POINTER cont_CHECKSTACK_TYPE[cont__CHECKSTACKSIZE];
extern cont_CHECKSTACK_TYPE cont_CHECKSTACK;
extern int cont_CHECKSTACKPOINTER;
/* Stack operations */
void cont_CheckStackInit(void);
void cont_CheckStackPush(POINTER Entry);
void cont_CheckStackPop(void);
POINTER cont_CheckStackPopResult(void);
void cont_CheckStackNPop(int N);
POINTER cont_CheckStackTop(void);
POINTER cont_CheckStackNthTop(int N);
void cont_CheckStackRplacTop(POINTER Entry);
void cont_CheckStackRplacNthTop(int N, POINTER Entry);
void cont_CheckStackRplacNth(int N, POINTER Entry);
int cont_CheckStackBottom(void);
void cont_CheckStackSetBottom(int Pointer);
BOOL cont_CheckStackEmpty(int Pointer);
extern VARCONT cont_STATELASTBINDING; /* Storage to save state of trails. */
extern int cont_STATEBINDINGS; /* Storage to save number of current bindings. */
extern int cont_STATESTACK; /* Storage to save state of stack. */
extern int cont_STATETOPSTACK; /* Storage to save state of the top element of the stack. */
BOOL cont_CheckLastBinding(VARCONT Check, int Bindings);
void cont_CheckState(void);
void cont_SaveState(void);
BOOL cont_IsContextEmpty(const VARCONT Check);
SYMBOL cont_NextIndexVariable(const VARCONT IndexContext);
TERM cont_SymbolDeref(VARCONT* Context, SYMBOL Symbol);
/**************************************************************/
/* Functions for Initialization and Controlling */
/**************************************************************/
void cont_Init(void);
void cont_Check(void);
void cont_Free(void);
/**************************************************************/
/* Functions for Term Equality Test with respect to Bindings */
/**************************************************************/
BOOL cont_TermEqual(VARCONT, VARCONT, TERM, VARCONT, VARCONT, TERM);
BOOL cont_TermEqualModuloBindings(VARCONT, VARCONT, TERM, VARCONT, TERM);
/**************************************************************/
/* Dereferencing of terms wrt. contexts */
/**************************************************************/
TERM cont_Deref(VARCONT, VARCONT*, TERM);
/**************************************************************/
/* Functions for Applying Bindings */
/**************************************************************/
TERM cont_CopyAndApplyBindings(VARCONT, TERM);
TERM cont_CopyAndApplyBindingsCom(const VARCONT, TERM);
TERM cont_ApplyBindingsModuloMatching(const VARCONT, TERM, BOOL);
TERM cont_ApplyBindingsModuloMatchingReverse(const VARCONT, TERM);
BOOL cont_BindingsAreRenamingModuloMatching(const VARCONT);
/**************************************************************/
/* Misc Functions */
/**************************************************************/
SYMBOL cont_TermMaxVar(VARCONT, VARCONT, TERM);
NAT cont_TermSize(VARCONT, VARCONT, TERM);
BOOL cont_TermContainsSymbol(VARCONT, VARCONT, TERM, SYMBOL);
/**************************************************************/
/* Functions for Output */
/**************************************************************/
void cont_TermPrintPrefix(VARCONT, VARCONT, TERM);
#endif
|
