1 //////////////////////////////////////////////////////////////////////////////
2 //Copyright 2008
3 // Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
4 //////////////////////////////////////////////////////////////////////////////
5 // This file is part of Teyjus. //
6 // //
7 // Teyjus is free software: you can redistribute it and/or modify //
8 // it under the terms of the GNU General Public License as published by //
9 // the Free Software Foundation, either version 3 of the License, or //
10 // (at your option) any later version. //
11 // //
12 // Teyjus is distributed in the hope that it will be useful, //
13 // but WITHOUT ANY WARRANTY; without even the implied warranty of //
14 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the //
15 // GNU General Public License for more details. //
16 // //
17 // You should have received a copy of the GNU General Public License //
18 // along with Teyjus. If not, see <http://www.gnu.org/licenses/>. //
19 //////////////////////////////////////////////////////////////////////////////
20 /****************************************************************************/
21 /* */
22 /* File dataformat.c. */
23 /* The header file identifies the low-level representation of data objects */
24 /* that are manipulated by the machine, through various structure types. */
25 /****************************************************************************/
26 #ifndef DATAFORMATS_C
27 #define DATAFORMATS_C
28
29 #include <math.h>
30 #include <string.h>
31 #include "dataformats.h"
32 #include "mctypes.h"
33 #include "mcstring.h"
34
35 /********************************************************************/
36 /* */
37 /* TYPE REPRESENTATION */
38 /* */
39 /********************************************************************/
40
41 /* Types of relevant fields in type representations. */
42 typedef TwoBytes DF_KstTabInd; //kind symbol table index
43 typedef TwoBytes DF_StrTypeArity; //arity of type structure
44 typedef TwoBytes DF_SkelInd; //offset of variables in type skeletons
45
46
47 /* Structure definitions of each type category. */
48 typedef struct //type sort
49 {
50 DF_Tag tag;
51 DF_KstTabInd kindTabIndex;
52 } DF_SortType;
53
54 typedef struct //type reference
55 {
56 DF_Tag tag;
57 DF_TypePtr target;
58 } DF_RefType;
59
60 typedef struct //variables in type skeletons
61 {
62 DF_Tag tag;
63 DF_SkelInd offset;
64 } DF_SkVarType;
65
66 typedef struct //type arrows
67 {
68 DF_Tag tag;
69 DF_TypePtr args;
70 } DF_ArrowType;
71
72 typedef struct //type functors
73 {
74 DF_Tag tag;
75 DF_StrTypeArity arity;
76 DF_KstTabInd kindTabIndex;
77 } DF_FuncType;
78
79 typedef struct //type structures
80 {
81 DF_Tag tag;
82 DF_FuncType *funcAndArgs;
83 } DF_StrType;
84
85 /******************************************************************/
86 /* Interface functions */
87 /******************************************************************/
88
89 /* TYPE DEREFERENCE */
DF_typeDeref(DF_TypePtr tyPtr)90 DF_TypePtr DF_typeDeref(DF_TypePtr tyPtr)
91 {
92 DF_Type ty = *tyPtr;
93 while ((ty.tag.categoryTag == DF_TY_TAG_REF)){
94 DF_TypePtr target = (DF_TypePtr)(ty.dummy);
95 if (tyPtr == target) return tyPtr;
96 tyPtr = target;
97 ty = *tyPtr;
98 }
99 return tyPtr;
100 }
101
102 /* TYPE RECOGNITION */
103
DF_isSortType(DF_TypePtr tyPtr)104 Boolean DF_isSortType(DF_TypePtr tyPtr)
105 { return (tyPtr->tag.categoryTag == DF_TY_TAG_SORT); }
DF_isRefType(DF_TypePtr tyPtr)106 Boolean DF_isRefType(DF_TypePtr tyPtr)
107 { return (tyPtr->tag.categoryTag == DF_TY_TAG_REF); }
DF_isSkelVarType(DF_TypePtr tyPtr)108 Boolean DF_isSkelVarType(DF_TypePtr tyPtr)
109 { return (tyPtr->tag.categoryTag == DF_TY_TAG_SKVAR);}
DF_isArrowType(DF_TypePtr tyPtr)110 Boolean DF_isArrowType(DF_TypePtr tyPtr)
111 { return (tyPtr->tag.categoryTag == DF_TY_TAG_ARROW);}
DF_isStrType(DF_TypePtr tyPtr)112 Boolean DF_isStrType(DF_TypePtr tyPtr)
113 { return (tyPtr->tag.categoryTag == DF_TY_TAG_STR); }
DF_isFreeVarType(DF_TypePtr tyPtr)114 Boolean DF_isFreeVarType(DF_TypePtr tyPtr)
115 { return ((tyPtr->tag.categoryTag == DF_TY_TAG_REF)
116 && ((DF_RefType*)tyPtr)->target == tyPtr); }
117
118
119 /* TYPE DECOMPOSITION */
DF_typeTag(DF_TypePtr tyPtr)120 int DF_typeTag(DF_TypePtr tyPtr) //generic type
121 {
122 return tyPtr->tag.categoryTag;
123 }
DF_typeKindTabIndex(DF_TypePtr tyPtr)124 int DF_typeKindTabIndex(DF_TypePtr tyPtr) //sorts
125 {
126 return ((DF_SortType*)tyPtr) -> kindTabIndex;
127 }
DF_typeSkelVarIndex(DF_TypePtr tyPtr)128 int DF_typeSkelVarIndex(DF_TypePtr tyPtr) //skel var
129 {
130 return ((DF_SkVarType*)tyPtr) -> offset;
131 }
DF_typeRefTarget(DF_TypePtr tyPtr)132 DF_TypePtr DF_typeRefTarget(DF_TypePtr tyPtr) //reference
133 {
134 return ((DF_RefType*)tyPtr) -> target;
135 }
DF_typeArrowArgs(DF_TypePtr tyPtr)136 DF_TypePtr DF_typeArrowArgs(DF_TypePtr tyPtr) //arrows
137 {
138 return ((DF_ArrowType*)tyPtr) -> args;
139 }
DF_typeStrFuncAndArgs(DF_TypePtr tyPtr)140 DF_TypePtr DF_typeStrFuncAndArgs(DF_TypePtr tyPtr) //structures
141 {
142 return (DF_TypePtr)(((DF_StrType*)tyPtr)->funcAndArgs);
143 }
DF_typeStrFuncInd(DF_TypePtr tyPtr)144 int DF_typeStrFuncInd(DF_TypePtr tyPtr)
145 {//Note tyPtr must refer to funcAndArgs field
146 return ((DF_FuncType*)tyPtr)->kindTabIndex;
147 }
DF_typeStrFuncArity(DF_TypePtr tyPtr)148 int DF_typeStrFuncArity(DF_TypePtr tyPtr)
149 {//Note tyPtr must refer to funcAndArgs field
150 return ((DF_FuncType*)tyPtr)->arity;
151 }
DF_typeStrArgs(DF_TypePtr tyPtr)152 DF_TypePtr DF_typeStrArgs(DF_TypePtr tyPtr)
153 {//Note tyPtr must refer to funcAndArgs field
154 return (DF_TypePtr)(((MemPtr)tyPtr) + DF_TY_ATOMIC_SIZE);
155 }
156
157 /* TYPE CONSTRUCTION */
DF_copyAtomicType(DF_TypePtr src,MemPtr dest)158 void DF_copyAtomicType(DF_TypePtr src, MemPtr dest)
159 {
160 *((DF_TypePtr)dest) = *src;
161 }
DF_mkSortType(MemPtr loc,int ind)162 void DF_mkSortType(MemPtr loc, int ind)
163 {
164 ((DF_SortType*)loc)->tag.categoryTag = DF_TY_TAG_SORT;
165 ((DF_SortType*)loc)->kindTabIndex = ind;
166 }
DF_mkRefType(MemPtr loc,DF_TypePtr target)167 void DF_mkRefType(MemPtr loc, DF_TypePtr target)
168 {
169 ((DF_RefType*)loc)->tag.categoryTag = DF_TY_TAG_REF;
170 ((DF_RefType*)loc)->target = target;
171 }
DF_mkFreeVarType(MemPtr loc)172 void DF_mkFreeVarType(MemPtr loc)
173 {
174 ((DF_RefType*)loc)->tag.categoryTag = DF_TY_TAG_REF;
175 ((DF_RefType*)loc)->target = (DF_TypePtr)loc;
176 }
DF_mkSkelVarType(MemPtr loc,int offset)177 void DF_mkSkelVarType(MemPtr loc, int offset)
178 {
179 ((DF_SkVarType*)loc)->tag.categoryTag = DF_TY_TAG_SKVAR;
180 ((DF_SkVarType*)loc)->offset = offset;
181 }
DF_mkArrowType(MemPtr loc,DF_TypePtr args)182 void DF_mkArrowType(MemPtr loc, DF_TypePtr args)
183 {
184 ((DF_ArrowType*)loc)->tag.categoryTag = DF_TY_TAG_ARROW;
185 ((DF_ArrowType*)loc)->args = args;
186 }
DF_mkStrType(MemPtr loc,DF_TypePtr funcAndArgs)187 void DF_mkStrType(MemPtr loc, DF_TypePtr funcAndArgs)
188 {
189 ((DF_StrType*)loc)->tag.categoryTag = DF_TY_TAG_STR;
190 ((DF_StrType*)loc)->funcAndArgs = (DF_FuncType*)funcAndArgs;
191 }
DF_mkStrFuncType(MemPtr loc,int ind,int n)192 void DF_mkStrFuncType(MemPtr loc, int ind, int n)
193 {
194 ((DF_FuncType*)loc)->tag.categoryTag = DF_TY_TAG_FUNC;
195 ((DF_FuncType*)loc)->kindTabIndex = ind;
196 ((DF_FuncType*)loc)->arity = n;
197 }
198
199 /********************************************************************/
200 /* */
201 /* TERM REPRESENTATION */
202 /* */
203 /********************************************************************/
204
205 /* types of relevant fields in term representions */
206 typedef TwoBytes DF_UnivInd; //universe count
207 typedef TwoBytes DF_CstTabInd; //constant symbol table index
208 typedef TwoBytes DF_Arity; //application arity
209 typedef TwoBytes DF_DBInd; //de Bruijn ind, embed level and num of lams
210 typedef WordPtr DF_StreamTabInd;
211
212 typedef struct //logic variables
213 {
214 DF_Tag tag;
215 DF_UnivInd univCount;
216 } DF_VarTerm;
217
218 typedef struct //de Bruijn indices
219 {
220 DF_Tag tag;
221 DF_DBInd index;
222 } DF_BVTerm;
223
224 typedef struct { //name and universe count field for constants
225 DF_UnivInd univCount;
226 DF_CstTabInd symTabIndex;
227 } DF_NameAndUC;
228
229 typedef struct { //constant without type association
230 DF_Tag tag;
231 Boolean withType;
232 union {
233 unsigned int value;
234 DF_NameAndUC nameAndUC;
235 } data;
236 } DF_ConstTerm;
237
238 typedef struct { //constant with type association
239 DF_Tag tag;
240 Boolean withType;
241 union {
242 unsigned int value;
243 DF_NameAndUC nameAndUC;
244 } data;
245 DF_TypePtr typeEnv;
246 } DF_TConstTerm;
247
248 typedef struct //integers
249 {
250 DF_Tag tag;
251 long int value;
252 } DF_IntTerm;
253
254 typedef struct //floats
255 {
256 DF_Tag tag;
257 float value;
258 } DF_FloatTerm;
259
260 typedef struct //string
261 {
262 DF_Tag tag;
263 DF_StrDataPtr value;
264 } DF_StrTerm;
265
266 typedef struct //stream
267 {
268 DF_Tag tag;
269 DF_StreamTabInd index;
270 } DF_StreamTerm;
271
272 typedef struct //empty list
273 {
274 DF_Tag tag;
275 } DF_NilTerm;
276
277 typedef struct //reference
278 {
279 DF_Tag tag;
280 DF_TermPtr target;
281 } DF_RefTerm;
282
283 typedef struct //list cons
284 {
285 DF_Tag tag;
286 DF_TermPtr args;
287 } DF_ConsTerm;
288
289 typedef struct //abstractions
290 {
291 DF_Tag tag;
292 DF_DBInd numOfLams;
293 DF_TermPtr body;
294 } DF_LamTerm;
295
296 typedef struct //applications
297 {
298 DF_Tag tag;
299 DF_Arity arity;
300 DF_TermPtr functor;
301 DF_TermPtr args;
302 } DF_AppTerm;
303
304 typedef struct //suspensions
305 {
306 DF_Tag tag;
307 DF_DBInd ol;
308 DF_DBInd nl;
309 DF_TermPtr termSkel;
310 DF_EnvPtr envList;
311 } DF_SuspTerm;
312
313
314 //environment items
315 typedef struct //dummy environment item
316 {
317 //Boolean isDummy;
318 DF_Tag tag;
319 DF_DBInd embedLevel;
320 DF_EnvPtr rest;
321 } DF_DummyEnv;
322
323 typedef struct //pair environment item
324 {
325 //Boolean isDummy;
326 DF_Tag tag;
327 DF_DBInd embedLevel;
328 DF_EnvPtr rest;
329 DF_TermPtr term;
330 } DF_PairEnv;
331
332
333 /******************************************************************/
334 /* Interface functions */
335 /******************************************************************/
336
337 /* DEREFERENCE */
DF_termDeref(DF_TermPtr tmPtr)338 DF_TermPtr DF_termDeref(DF_TermPtr tmPtr)
339 {
340 while (DF_isRef(tmPtr)) tmPtr = ((DF_RefTerm*)tmPtr)->target;
341 return tmPtr;
342 }
343
344 /* TERM RECOGNITION */
345 //note ref is neither atomic nor complex
DF_isAtomic(DF_TermPtr tmPtr)346 Boolean DF_isAtomic(DF_TermPtr tmPtr)
347 { return (tmPtr -> tag.categoryTag < DF_TM_TAG_REF); }
DF_isNAtomic(DF_TermPtr tmPtr)348 Boolean DF_isNAtomic(DF_TermPtr tmPtr)
349 { return (tmPtr -> tag.categoryTag > DF_TM_TAG_REF); }
DF_isFV(DF_TermPtr tmPtr)350 Boolean DF_isFV(DF_TermPtr tmPtr)
351 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_VAR); }
DF_isConst(DF_TermPtr tmPtr)352 Boolean DF_isConst(DF_TermPtr tmPtr)
353 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_CONST); }
354 /*assume the tmPtr is known to be a constant */
DF_isTConst(DF_TermPtr tmPtr)355 Boolean DF_isTConst(DF_TermPtr tmPtr)
356 { return ((DF_ConstTerm*)tmPtr) -> withType; }
DF_isInt(DF_TermPtr tmPtr)357 Boolean DF_isInt(DF_TermPtr tmPtr)
358 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_INT); }
DF_isFloat(DF_TermPtr tmPtr)359 Boolean DF_isFloat(DF_TermPtr tmPtr)
360 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_FLOAT); }
DF_isNil(DF_TermPtr tmPtr)361 Boolean DF_isNil(DF_TermPtr tmPtr)
362 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_NIL); }
DF_isStr(DF_TermPtr tmPtr)363 Boolean DF_isStr(DF_TermPtr tmPtr)
364 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_STR); }
DF_isBV(DF_TermPtr tmPtr)365 Boolean DF_isBV(DF_TermPtr tmPtr)
366 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_BVAR); }
DF_isStream(DF_TermPtr tmPtr)367 Boolean DF_isStream(DF_TermPtr tmPtr)
368 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_STREAM);}
DF_isRef(DF_TermPtr tmPtr)369 Boolean DF_isRef(DF_TermPtr tmPtr)
370 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_REF); }
DF_isCons(DF_TermPtr tmPtr)371 Boolean DF_isCons(DF_TermPtr tmPtr)
372 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_CONS); }
DF_isLam(DF_TermPtr tmPtr)373 Boolean DF_isLam(DF_TermPtr tmPtr)
374 { return (tmPtr -> tag.categoryTag == DF_TM_TAG_LAM); }
DF_isApp(DF_TermPtr tmPtr)375 Boolean DF_isApp(DF_TermPtr tmPtr)
376 { return (tmPtr-> tag.categoryTag == DF_TM_TAG_APP); }
DF_isSusp(DF_TermPtr tmPtr)377 Boolean DF_isSusp(DF_TermPtr tmPtr)
378 { return (tmPtr-> tag.categoryTag == DF_TM_TAG_SUSP); }
DF_isEmpEnv(DF_EnvPtr envPtr)379 Boolean DF_isEmpEnv(DF_EnvPtr envPtr)
380 { return (envPtr == DF_EMPTY_ENV); }
DF_isDummyEnv(DF_EnvPtr envPtr)381 Boolean DF_isDummyEnv(DF_EnvPtr envPtr)
382 { return envPtr -> tag.categoryTag == DF_ENV_TAG_DUMMY; }
383
384
385 /* TERM DECOMPOSITION */
DF_termTag(DF_TermPtr tmPtr)386 int DF_termTag(DF_TermPtr tmPtr) // tag
387 {
388 return tmPtr -> tag.categoryTag;
389 }
390 //unbound variables
DF_fvUnivCount(DF_TermPtr tmPtr)391 int DF_fvUnivCount(DF_TermPtr tmPtr) //universe count
392 {
393 return ((DF_VarTerm*)tmPtr)->univCount;
394 }
395 //constant (w/oc type associations)
DF_constUnivCount(DF_TermPtr tmPtr)396 int DF_constUnivCount(DF_TermPtr tmPtr) //universe count
397 {
398 return ((DF_ConstTerm*)tmPtr)->data.nameAndUC.univCount;
399 }
DF_constTabIndex(DF_TermPtr tmPtr)400 int DF_constTabIndex(DF_TermPtr tmPtr) //table index
401 {
402 return ((DF_ConstTerm*)tmPtr)->data.nameAndUC.symTabIndex;
403 }
404 //constants with type associations
DF_constType(DF_TermPtr tmPtr)405 DF_TypePtr DF_constType(DF_TermPtr tmPtr) //type env
406 {
407 return ((DF_TConstTerm*)tmPtr)->typeEnv;
408 }
409 //integer
DF_intValue(DF_TermPtr tmPtr)410 long DF_intValue(DF_TermPtr tmPtr) //integer value
411 {
412 return ((DF_IntTerm*)tmPtr)->value;
413 }
414 //float
DF_floatValue(DF_TermPtr tmPtr)415 float DF_floatValue(DF_TermPtr tmPtr) //float value
416 {
417 return ((DF_FloatTerm*)tmPtr)->value;
418 }
419 //string
DF_strValue(DF_TermPtr tmPtr)420 MCSTR_Str DF_strValue(DF_TermPtr tmPtr) //string value
421 {
422 return (MCSTR_Str)(((MemPtr)(((DF_StrTerm*)tmPtr)->value))
423 + DF_STRDATA_HEAD_SIZE);
424 }
DF_strData(DF_TermPtr tmPtr)425 DF_StrDataPtr DF_strData(DF_TermPtr tmPtr) //string data field
426 {
427 return ((DF_StrTerm*)tmPtr)->value;
428 }
DF_strDataValue(DF_StrDataPtr tmPtr)429 MCSTR_Str DF_strDataValue(DF_StrDataPtr tmPtr) //acc str value from data fd
430 {
431 return (MCSTR_Str)(((MemPtr)tmPtr) + DF_STRDATA_HEAD_SIZE);
432 }
433
434 //stream TEMP
DF_streamTabIndex(DF_TermPtr tmPtr)435 WordPtr DF_streamTabIndex(DF_TermPtr tmPtr) //stream table index
436 {
437 return ((DF_StreamTerm*)tmPtr)->index;
438 }
439 //de Bruijn index
DF_bvIndex(DF_TermPtr tmPtr)440 int DF_bvIndex(DF_TermPtr tmPtr) //de Bruijn index
441 {
442 return ((DF_BVTerm*)tmPtr)->index;
443 }
444 //reference
DF_refTarget(DF_TermPtr tmPtr)445 DF_TermPtr DF_refTarget(DF_TermPtr tmPtr) //target
446 {
447 return ((DF_RefTerm*)tmPtr)->target;
448 }
449 //list cons
DF_consArgs(DF_TermPtr tmPtr)450 DF_TermPtr DF_consArgs(DF_TermPtr tmPtr) //arg vector
451 {
452 return ((DF_ConsTerm*)tmPtr)->args;
453 }
454 //abstraction
DF_lamNumAbs(DF_TermPtr tmPtr)455 int DF_lamNumAbs(DF_TermPtr tmPtr) //embedding level
456 {
457 return ((DF_LamTerm*)tmPtr)->numOfLams;
458 }
DF_lamBody(DF_TermPtr tmPtr)459 DF_TermPtr DF_lamBody(DF_TermPtr tmPtr) //abstraction body
460 {
461 return ((DF_LamTerm*)tmPtr)->body;
462 }
463 //application
DF_appArity(DF_TermPtr tmPtr)464 int DF_appArity(DF_TermPtr tmPtr) //arity
465 {
466 return ((DF_AppTerm*)tmPtr)->arity;
467 }
DF_appFunc(DF_TermPtr tmPtr)468 DF_TermPtr DF_appFunc(DF_TermPtr tmPtr) //functor
469 {
470 return ((DF_AppTerm*)tmPtr)->functor;
471 }
DF_appArgs(DF_TermPtr tmPtr)472 DF_TermPtr DF_appArgs(DF_TermPtr tmPtr) //arg vector
473 {
474 return ((DF_AppTerm*)tmPtr)->args;
475 }
476 //suspension
DF_suspOL(DF_TermPtr tmPtr)477 int DF_suspOL(DF_TermPtr tmPtr) //ol
478 {
479 return ((DF_SuspTerm*)tmPtr)->ol;
480 }
DF_suspNL(DF_TermPtr tmPtr)481 int DF_suspNL(DF_TermPtr tmPtr) //nl
482 {
483 return ((DF_SuspTerm*)tmPtr)->nl;
484 }
DF_suspTermSkel(DF_TermPtr tmPtr)485 DF_TermPtr DF_suspTermSkel(DF_TermPtr tmPtr) //term skeleton
486 {
487 return ((DF_SuspTerm*)tmPtr)->termSkel;
488 }
DF_suspEnv(DF_TermPtr tmPtr)489 DF_EnvPtr DF_suspEnv(DF_TermPtr tmPtr) //environment list
490 {
491 return ((DF_SuspTerm*)tmPtr)->envList;
492 }
493
494 //environment item (dummy/pair)
DF_envListRest(DF_EnvPtr envPtr)495 DF_EnvPtr DF_envListRest(DF_EnvPtr envPtr) //next env item
496 {
497 return envPtr->rest;
498 }
DF_envListNth(DF_EnvPtr envPtr,int n)499 DF_EnvPtr DF_envListNth(DF_EnvPtr envPtr, int n) //nth item
500 {
501 int i;
502 for (i=n; (i!=1); i--) envPtr = envPtr -> rest;
503 return envPtr;
504 }
DF_envIndex(DF_EnvPtr envPtr)505 int DF_envIndex(DF_EnvPtr envPtr) //l in @l or (t,l)
506 {
507 return envPtr -> embedLevel;
508 }
509 //pair environment item
DF_envPairTerm(DF_EnvPtr envPtr)510 DF_TermPtr DF_envPairTerm(DF_EnvPtr envPtr) //t in (t,l)
511 {
512 return ((DF_PairEnv*)envPtr) -> term;
513 }
514
515 /* TERM CONSTRUCTION */
DF_copyAtomic(DF_TermPtr src,MemPtr dest)516 void DF_copyAtomic(DF_TermPtr src, MemPtr dest) //copy atomic
517 {
518 *((DF_TermPtr)dest) = *src;
519 }
DF_copyApp(DF_TermPtr src,MemPtr dest)520 void DF_copyApp(DF_TermPtr src, MemPtr dest) //copy application
521 {
522 *((DF_AppTerm*)dest) = *((DF_AppTerm*)src);
523 }
DF_copySusp(DF_TermPtr src,MemPtr dest)524 void DF_copySusp(DF_TermPtr src, MemPtr dest) //copy suspension
525 {
526 *((DF_SuspTerm*)dest) = *((DF_SuspTerm*)src);
527 }
DF_mkVar(MemPtr loc,int uc)528 void DF_mkVar(MemPtr loc, int uc) //unbound variable
529 {
530 ((DF_VarTerm*)loc) -> tag.categoryTag = DF_TM_TAG_VAR;
531 ((DF_VarTerm*)loc) -> univCount = uc;
532 }
DF_mkBV(MemPtr loc,int ind)533 void DF_mkBV(MemPtr loc, int ind) //de Bruijn index
534 {
535 ((DF_BVTerm*)loc) -> tag.categoryTag = DF_TM_TAG_BVAR;
536 ((DF_BVTerm*)loc) -> index = ind;
537 }
DF_mkConst(MemPtr loc,int uc,int ind)538 void DF_mkConst(MemPtr loc, int uc, int ind) //const
539 {
540 ((DF_ConstTerm*)loc) -> tag.categoryTag = DF_TM_TAG_CONST;
541 ((DF_ConstTerm*)loc) -> withType = FALSE;
542 (((DF_ConstTerm*)loc) -> data).nameAndUC.univCount = uc;
543 (((DF_ConstTerm*)loc) -> data).nameAndUC.symTabIndex = ind;
544 }
DF_mkTConst(MemPtr loc,int uc,int ind,DF_TypePtr typeEnv)545 void DF_mkTConst(MemPtr loc, int uc, int ind, DF_TypePtr typeEnv)
546 //const with type association
547 {
548 ((DF_TConstTerm*)loc) -> tag.categoryTag = DF_TM_TAG_CONST;
549 ((DF_TConstTerm*)loc) -> withType = TRUE;
550 (((DF_TConstTerm*)loc) -> data).nameAndUC.univCount = uc;
551 (((DF_TConstTerm*)loc) -> data).nameAndUC.symTabIndex = ind;
552 ((DF_TConstTerm*)loc) -> typeEnv = typeEnv;
553 }
DF_mkInt(MemPtr loc,long value)554 void DF_mkInt(MemPtr loc, long value) //int
555 {
556 ((DF_IntTerm*)loc) -> tag.categoryTag = DF_TM_TAG_INT;
557 ((DF_IntTerm*)loc) -> value = value;
558 }
DF_mkFloat(MemPtr loc,float value)559 void DF_mkFloat(MemPtr loc, float value) //float
560 {
561 ((DF_FloatTerm*)loc) -> tag.categoryTag = DF_TM_TAG_FLOAT;
562 ((DF_FloatTerm*)loc) -> value = value;
563 }
DF_mkStr(MemPtr loc,DF_StrDataPtr data)564 void DF_mkStr(MemPtr loc, DF_StrDataPtr data) //string
565 {
566 ((DF_StrTerm*)loc) -> tag.categoryTag = DF_TM_TAG_STR;
567 ((DF_StrTerm*)loc) -> value = data;
568 }
DF_mkStrDataHead(MemPtr loc)569 void DF_mkStrDataHead(MemPtr loc) //string data head
570 {
571 ((DF_StrDataPtr)loc) -> tag.categoryTag = DF_TM_TAG_STRBODY;
572 }
573
DF_mkStream(MemPtr loc,WordPtr ind)574 void DF_mkStream(MemPtr loc, WordPtr ind) //stream
575 {
576 ((DF_StreamTerm*)loc) -> tag.categoryTag = DF_TM_TAG_STREAM;
577 ((DF_StreamTerm*)loc) -> index = ind;
578 }
DF_setStreamInd(DF_TermPtr tm,WordPtr ind)579 void DF_setStreamInd(DF_TermPtr tm, WordPtr ind) //update stream ind
580 {
581 ((DF_StreamTerm*)tm) -> index = ind;
582 }
DF_mkNil(MemPtr loc)583 void DF_mkNil(MemPtr loc) //nil
584 {
585 ((DF_NilTerm*)loc) -> tag.categoryTag = DF_TM_TAG_NIL;
586 }
DF_mkRef(MemPtr loc,DF_TermPtr target)587 void DF_mkRef(MemPtr loc, DF_TermPtr target) //reference
588 {
589 ((DF_RefTerm*)loc) -> tag.categoryTag = DF_TM_TAG_REF;
590 ((DF_RefTerm*)loc) -> target = target;
591 }
DF_mkCons(MemPtr loc,DF_TermPtr args)592 void DF_mkCons(MemPtr loc, DF_TermPtr args) //cons
593 {
594 ((DF_ConsTerm*)loc) -> tag.categoryTag = DF_TM_TAG_CONS;
595 ((DF_ConsTerm*)loc) -> args = args;
596 }
DF_mkLam(MemPtr loc,int n,DF_TermPtr body)597 void DF_mkLam(MemPtr loc, int n, DF_TermPtr body) //abstraction
598 {
599 ((DF_LamTerm*)loc) -> tag.categoryTag = DF_TM_TAG_LAM;
600 ((DF_LamTerm*)loc) -> numOfLams = n;
601 ((DF_LamTerm*)loc) -> body = body;
602 }
DF_mkApp(MemPtr loc,int n,DF_TermPtr func,DF_TermPtr args)603 void DF_mkApp(MemPtr loc, int n, DF_TermPtr func, DF_TermPtr args)
604 { //application
605 ((DF_AppTerm*)loc) -> tag.categoryTag = DF_TM_TAG_APP;
606 ((DF_AppTerm*)loc) -> arity = n;
607 ((DF_AppTerm*)loc) -> functor = func;
608 ((DF_AppTerm*)loc) -> args = args;
609 }
DF_mkSusp(MemPtr loc,int ol,int nl,DF_TermPtr tmPtr,DF_EnvPtr env)610 void DF_mkSusp(MemPtr loc, int ol, int nl, DF_TermPtr tmPtr, DF_EnvPtr env)
611 //suspension
612 {
613 ((DF_SuspTerm*)loc) -> tag.categoryTag = DF_TM_TAG_SUSP;
614 ((DF_SuspTerm*)loc) -> ol = ol;
615 ((DF_SuspTerm*)loc) -> nl = nl;
616 ((DF_SuspTerm*)loc) -> termSkel = tmPtr;
617 ((DF_SuspTerm*)loc) -> envList = env;
618 }
619
DF_mkDummyEnv(MemPtr loc,int l,DF_EnvPtr rest)620 void DF_mkDummyEnv(MemPtr loc, int l, DF_EnvPtr rest) //@l env item
621 {
622 ((DF_DummyEnv*)loc) -> tag.categoryTag = DF_ENV_TAG_DUMMY;
623 ((DF_DummyEnv*)loc) -> embedLevel = l;
624 ((DF_DummyEnv*)loc) -> rest = rest;
625 }
DF_mkPairEnv(MemPtr loc,int l,DF_TermPtr t,DF_EnvPtr rest)626 void DF_mkPairEnv(MemPtr loc, int l, DF_TermPtr t, DF_EnvPtr rest)
627 {
628 // (t, l) env item
629 ((DF_PairEnv*)loc) -> tag.categoryTag = DF_ENV_TAG_PAIR;
630 ((DF_PairEnv*)loc) -> embedLevel = l;
631 ((DF_PairEnv*)loc) -> rest = rest;
632 ((DF_PairEnv*)loc) -> term = t;
633 }
634
635
636 /* TERM MODIFICATION */
DF_modVarUC(DF_TermPtr vPtr,int uc)637 void DF_modVarUC(DF_TermPtr vPtr, int uc)
638 {
639 ((DF_VarTerm*)vPtr) -> univCount = uc;
640 }
641
642
643 /* (NON_TRIVIAL) TERM COMPARISON */
DF_sameConsts(DF_TermPtr const1,DF_TermPtr const2)644 Boolean DF_sameConsts(DF_TermPtr const1, DF_TermPtr const2) //same constant?
645 {
646 return (((DF_ConstTerm*)const1)->data.value ==
647 ((DF_ConstTerm*)const2)->data.value);
648 }
DF_sameStrs(DF_TermPtr str1,DF_TermPtr str2)649 Boolean DF_sameStrs(DF_TermPtr str1, DF_TermPtr str2) //same string?
650 {
651 if (str1 == str2) return TRUE;
652 else if (((DF_StrTerm*)str1)->value ==
653 ((DF_StrTerm*)str2)->value) return TRUE; //compare data fd addr
654 //compare literals
655 return MCSTR_sameStrs(
656 (MCSTR_Str)(((MemPtr)(((DF_StrTerm*)str1)->value)) +
657 DF_STRDATA_HEAD_SIZE),
658 (MCSTR_Str)(((MemPtr)(((DF_StrTerm*)str2)->value)) +
659 DF_STRDATA_HEAD_SIZE));
660
661 }
DF_sameStrData(DF_TermPtr tmPtr,DF_StrDataPtr strData)662 Boolean DF_sameStrData(DF_TermPtr tmPtr, DF_StrDataPtr strData)
663 {
664 if (((DF_StrTerm*)tmPtr) -> value == strData) return TRUE; //compare addr
665 return MCSTR_sameStrs(
666 (MCSTR_Str)(((MemPtr)(((DF_StrTerm*)tmPtr)->value)) +
667 DF_STRDATA_HEAD_SIZE),
668 (MCSTR_Str)(((MemPtr)strData) + DF_STRDATA_HEAD_SIZE));
669 }
670
671 /********************************************************************/
672 /* */
673 /* DISAGREEMENT SET REPRESENTATION */
674 /* */
675 /* A double linked list */
676 /********************************************************************/
677
678 //create a new node at the given location
DF_mkDisPair(MemPtr loc,DF_DisPairPtr next,DF_TermPtr first,DF_TermPtr second)679 void DF_mkDisPair(MemPtr loc, DF_DisPairPtr next, DF_TermPtr first,
680 DF_TermPtr second)
681 {
682 ((DF_DisPairPtr)(loc)) -> tag.categoryTag = DF_DISPAIR;
683 ((DF_DisPairPtr)(loc)) -> next = next;
684 ((DF_DisPairPtr)(loc)) -> firstTerm = first;
685 ((DF_DisPairPtr)(loc)) -> secondTerm = second;
686 }
687
688 //decomposition
DF_disPairNext(DF_DisPairPtr disPtr)689 DF_DisPairPtr DF_disPairNext(DF_DisPairPtr disPtr){return disPtr -> next; }
DF_disPairFirstTerm(DF_DisPairPtr disPtr)690 DF_TermPtr DF_disPairFirstTerm(DF_DisPairPtr disPtr)
691 {
692 return disPtr -> firstTerm;
693 }
DF_disPairSecondTerm(DF_DisPairPtr disPtr)694 DF_TermPtr DF_disPairSecondTerm(DF_DisPairPtr disPtr)
695 {
696 return disPtr -> secondTerm;
697 }
698
699 //whether a given disagreement set is empty
DF_isEmpDisSet(DF_DisPairPtr disPtr)700 Boolean DF_isEmpDisSet(DF_DisPairPtr disPtr)
701 {
702 return (disPtr == DF_EMPTY_DIS_SET);
703 }
704
DF_isNEmpDisSet(DF_DisPairPtr disPtr)705 Boolean DF_isNEmpDisSet(DF_DisPairPtr disPtr)
706 {
707 return (disPtr != DF_EMPTY_DIS_SET);
708 }
709
710
711 #endif //DATAFORMATS_C
712