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.h. */ 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_H 27 #define DATAFORMATS_H 28 29 #include <limits.h> // to be removed 30 #include <stdlib.h> 31 //#include <math.h> 32 #include "mctypes.h" 33 #include "mcstring.h" 34 35 /********************************************************************/ 36 /* DATA TAG FIELD IN TYPES AND TERMS */ 37 /********************************************************************/ 38 39 /* The first byte is assumed to contain a type or term category tag, 40 and the second is to be used for marking in garbage collection */ 41 typedef struct 42 { 43 Byte categoryTag; 44 Byte mark; //to be used in garbage collection 45 } DF_Tag; 46 47 /* The tags of heap items */ 48 typedef enum 49 { 50 //type categories 51 DF_TY_TAG_SORT = 0, //sort 52 DF_TY_TAG_REF, //reference 53 DF_TY_TAG_SKVAR, //skeleton variable 54 DF_TY_TAG_ARROW, //type arrow 55 DF_TY_TAG_STR, //type structure 56 DF_TY_TAG_FUNC, //functor of type structure 57 58 //term categories 59 DF_TM_TAG_VAR = 6, // existential variables 60 DF_TM_TAG_CONST, // constants 61 DF_TM_TAG_INT, // integers 62 DF_TM_TAG_FLOAT, // floats 63 DF_TM_TAG_NIL, // empty lists 64 DF_TM_TAG_STR, // strings 65 DF_TM_TAG_STREAM, // streams 66 DF_TM_TAG_BVAR, // lambda bound variables (de Bruijn index) 67 // -- atoms above 68 DF_TM_TAG_REF, // references 69 // -- complex terms below 70 DF_TM_TAG_CONS, // list constructors 71 DF_TM_TAG_LAM, // abstractions 72 DF_TM_TAG_APP, // applications 73 DF_TM_TAG_SUSP, // suspensions 74 75 DF_TM_TAG_STRBODY = 19, // string body 76 77 //suspension environment items 78 DF_ENV_TAG_DUMMY = 20, //dummy environment 79 DF_ENV_TAG_PAIR, //pair environment 80 81 //disagreement pair 82 DF_DISPAIR = 22 83 } DF_HeapDataCategory; 84 85 86 /********************************************************************/ 87 /* */ 88 /* TYPE REPRESENTATION */ 89 /* */ 90 /********************************************************************/ 91 92 /********************************************************************/ 93 /* Only generic types are visible from outside. */ 94 /* The "public" information for each specific type category is their*/ 95 /* sizes. Their structure declarations are hidden in dataformat.c. */ 96 /* Construction, recognization and decomposition of types should be */ 97 /* performed through interface functions with declarations present */ 98 /* in this file. */ 99 /********************************************************************/ 100 101 /* 102 //type categories 103 enum DF_TypeCategory 104 { 105 DF_TY_TAG_SORT, //sort 106 DF_TY_TAG_REF, //reference 107 DF_TY_TAG_SKVAR, //skeleton variable 108 DF_TY_TAG_ARROW, //type arrow 109 DF_TY_TAG_STR //type structure 110 }; 111 */ 112 113 //generic type (head) for every category 114 typedef struct 115 { 116 DF_Tag tag; /* the common field for every type (head); can 117 be any one of enum TypeCategory. 118 rely on struct alignment */ 119 Word dummy; /* a place holder which enforces the size of the 120 generic term to be 2 words. */ 121 } DF_Type; 122 123 typedef DF_Type *DF_TypePtr; //type pointer 124 125 //sizes of different type items 126 #define DF_TY_ATOMIC_SIZE 2 //atomic size 127 128 //attributes of special type constructors 129 #define DF_TY_ARROW_ARITY 2 //arity of type arrow 130 131 132 /******************************************************************/ 133 /* Interface functions */ 134 /******************************************************************/ 135 136 /* TYPE DEREFERENCE */ 137 DF_TypePtr DF_typeDeref(DF_TypePtr); 138 139 /* TYPE RECOGNITION */ 140 Boolean DF_isSortType(DF_TypePtr); // is sort? 141 Boolean DF_isRefType(DF_TypePtr); // is reference? (including free var) 142 Boolean DF_isFreeVarType(DF_TypePtr); // is free var? 143 Boolean DF_isSkelVarType(DF_TypePtr); // is skeleton var? 144 Boolean DF_isArrowType(DF_TypePtr); // is type arrow? 145 Boolean DF_isStrType(DF_TypePtr); // is type structure? 146 147 /* TYPE DECOMPOSITION */ 148 int DF_typeTag(DF_TypePtr); //generic type 149 int DF_typeKindTabIndex(DF_TypePtr); //sorts 150 int DF_typeSkelVarIndex(DF_TypePtr); //skel var 151 DF_TypePtr DF_typeRefTarget(DF_TypePtr); //reference 152 DF_TypePtr DF_typeArrowArgs(DF_TypePtr); //arrows 153 DF_TypePtr DF_typeStrFuncAndArgs(DF_TypePtr); //structures 154 int DF_typeStrFuncInd(DF_TypePtr); 155 int DF_typeStrFuncArity(DF_TypePtr); 156 DF_TypePtr DF_typeStrArgs(DF_TypePtr); 157 158 /* TYPE CONSTRUCTION */ 159 void DF_copyAtomicType(DF_TypePtr src, MemPtr dest); 160 void DF_mkSortType(MemPtr loc, int ind); 161 void DF_mkRefType(MemPtr loc, DF_TypePtr target); 162 void DF_mkFreeVarType(MemPtr loc); 163 void DF_mkSkelVarType(MemPtr loc, int offset); 164 void DF_mkArrowType(MemPtr loc, DF_TypePtr args); 165 void DF_mkStrType(MemPtr loc, DF_TypePtr funcAndArgs); 166 void DF_mkStrFuncType(MemPtr loc, int ind, int n); 167 168 169 /********************************************************************/ 170 /* */ 171 /* TERM REPRESENTATION */ 172 /* */ 173 /********************************************************************/ 174 175 /********************************************************************/ 176 /* Only generic terms (environment items) are visible from outside. */ 177 /* The "public" information for each specific term category is their*/ 178 /* sizes. Their structure declarations are hidden in dataformat.c. */ 179 /* Construction, recognization and decomposition of terms should be */ 180 /* performed through interface functions with declarations present */ 181 /* in this file. */ 182 /********************************************************************/ 183 184 /* 185 //term categories 186 enum DF_TermCategory 187 { 188 DF_TM_TAG_VAR, // existential variables 189 DF_TM_TAG_CONST, // constants 190 DF_TM_TAG_INT, // integers 191 DF_TM_TAG_FLOAT, // floats 192 DF_TM_TAG_NIL, // empty lists 193 DF_TM_TAG_STR, // strings 194 DF_TM_TAG_STREAM, // streams 195 DF_TM_TAG_BVAR, // lambda bound variables (de Bruijn index) 196 // -- atoms above 197 DF_TM_TAG_REF, // references 198 // -- complex terms below 199 DF_TM_TAG_CONS, // list constructors 200 DF_TM_TAG_LAM, // abstractions 201 DF_TM_TAG_APP, // applications 202 DF_TM_TAG_SUSP // suspensions 203 }; 204 */ 205 206 // a generic term (head) for every category 207 typedef struct 208 { 209 DF_Tag tag; /* the common field for every term (head); can 210 be any one of enum TermCategory. 211 rely on struct alignment */ 212 Word dummy; /* a place holder which enforces the size of the 213 generic term to be 2 words. */ 214 } DF_Term; 215 216 typedef DF_Term *DF_TermPtr; //term pointer 217 218 //sizes of different term items 219 #define DF_TM_ATOMIC_SIZE 2 // atomic size 220 #define DF_TM_TCONST_SIZE 3 // type associated constant (config set) 221 #define DF_TM_APP_SIZE 3 // application head 222 #define DF_TM_LAM_SIZE 2 // abstraction 223 #define DF_TM_CONS_SIZE 2 // cons 224 #define DF_TM_SUSP_SIZE 4 // suspension (config set) 225 226 // attributes of some special constants 227 #define DF_CONS_ARITY 2 //arity of cons 228 229 // head of string body (a tag word should be followed by encoding of literals) 230 typedef union 231 { 232 DF_Tag tag; 233 Word dummy; 234 } DF_StrData; 235 236 typedef DF_StrData *DF_StrDataPtr; 237 238 //#define DF_STRDATA_HEAD_SIZE (int)ceil((double)sizeof(DF_StrData)/WORD_SIZE) 239 #define DF_STRDATA_HEAD_SIZE 2 240 241 //a generic environment item in suspension 242 typedef struct DF_env 243 { 244 //Boolean isDummy; 245 DF_Tag tag; 246 TwoBytes embedLevel; 247 struct DF_env *rest; //the tail of the list 248 } DF_Env; 249 250 typedef DF_Env *DF_EnvPtr; 251 252 // empty environment list 253 #define DF_EMPTY_ENV NULL 254 255 //sizes of different environment items 256 #define DF_ENV_DUMMY_SIZE 2 // dummy environment item 257 #define DF_ENV_PAIR_SIZE 3 // pair environment item 258 259 //limits (to be set by configuration) 260 #define DF_MAX_BV_IND USHRT_MAX //max db ind (embedding level) 261 #define DF_TM_MAX_ARITY USHRT_MAX //max arity 262 #define DF_MAX_UNIVIND USHRT_MAX //max universe index 263 264 265 /******************************************************************/ 266 /* Interface functions */ 267 /******************************************************************/ 268 269 /* DEREFERENCE */ 270 DF_TermPtr DF_termDeref(DF_TermPtr); // term dereference 271 272 /* TERM RECOGNITION */ 273 Boolean DF_isAtomic(DF_TermPtr); //note ref is neither atomic nor complex 274 Boolean DF_isNAtomic(DF_TermPtr); 275 Boolean DF_isFV(DF_TermPtr); // is unbound variable? 276 Boolean DF_isConst(DF_TermPtr); // is constant (typed and untyped)? 277 Boolean DF_isTConst(DF_TermPtr); // is a type associated constant? 278 // Note we assume the arg is known to be const 279 Boolean DF_isInt(DF_TermPtr); // is integer? 280 Boolean DF_isFloat(DF_TermPtr); // is float? 281 Boolean DF_isNil(DF_TermPtr); // is list nil? 282 Boolean DF_isStr(DF_TermPtr); // is string? 283 Boolean DF_isBV(DF_TermPtr); // is de Bruijn index? 284 Boolean DF_isStream(DF_TermPtr); // is stream? 285 Boolean DF_isRef(DF_TermPtr); // is reference? 286 Boolean DF_isCons(DF_TermPtr); // is list cons? 287 Boolean DF_isLam(DF_TermPtr); // is abstraction? 288 Boolean DF_isApp(DF_TermPtr); // is application? 289 Boolean DF_isSusp(DF_TermPtr); // is suspension? 290 291 Boolean DF_isEmpEnv(DF_EnvPtr); // is empty environment? 292 Boolean DF_isDummyEnv(DF_EnvPtr);// is dummy environment item? 293 294 /* TERM DECOMPOSITION */ 295 //generic term 296 int DF_termTag(DF_TermPtr); // term category tag 297 //unbound variable 298 int DF_fvUnivCount(DF_TermPtr); // universe count 299 //constants (w/oc type associations) 300 int DF_constUnivCount(DF_TermPtr); // universe index 301 int DF_constTabIndex(DF_TermPtr); // symbol table index 302 //constants with type associations 303 DF_TypePtr DF_constType(DF_TermPtr); // type environment 304 //integer 305 long DF_intValue(DF_TermPtr); // integer value (long) 306 //float 307 float DF_floatValue(DF_TermPtr); // float value 308 //string 309 MCSTR_Str DF_strValue(DF_TermPtr); // string value 310 DF_StrDataPtr DF_strData(DF_TermPtr tmPtr); // string data field 311 MCSTR_Str DF_strDataValue(DF_StrDataPtr tmPtr); //acc str value from data fd 312 //stream 313 WordPtr DF_streamTabIndex(DF_TermPtr); // stream table index 314 //de Bruijn indices 315 int DF_bvIndex(DF_TermPtr); // de Bruijn index 316 //reference 317 DF_TermPtr DF_refTarget(DF_TermPtr); // target 318 //list cons 319 DF_TermPtr DF_consArgs(DF_TermPtr); // arg vector 320 //abstractions 321 int DF_lamNumAbs(DF_TermPtr); // embedding level 322 DF_TermPtr DF_lamBody(DF_TermPtr); // lambda body 323 //application 324 int DF_appArity(DF_TermPtr); // arity 325 DF_TermPtr DF_appFunc(DF_TermPtr); // functor 326 DF_TermPtr DF_appArgs(DF_TermPtr); // arg vector 327 //suspension 328 int DF_suspOL(DF_TermPtr); // ol 329 int DF_suspNL(DF_TermPtr); // nl 330 DF_TermPtr DF_suspTermSkel(DF_TermPtr); // term skel 331 DF_EnvPtr DF_suspEnv(DF_TermPtr); // environment list 332 333 //environment item (dummy/pair) 334 DF_EnvPtr DF_envListRest(DF_EnvPtr); // next env item 335 DF_EnvPtr DF_envListNth(DF_EnvPtr, int); // the nth item 336 int DF_envIndex(DF_EnvPtr); // l in @l or (t,l) 337 //pair environment item 338 DF_TermPtr DF_envPairTerm(DF_EnvPtr); // t in (t,l) 339 340 341 /* TERM CONSTRUCTION */ 342 void DF_copyAtomic(DF_TermPtr src, MemPtr dest); //copy atomic 343 void DF_copyApp(DF_TermPtr src, MemPtr dest); //copy application 344 void DF_copySusp(DF_TermPtr src, MemPtr dest); //copy suspension 345 void DF_mkVar(MemPtr loc, int uc); //unbound variable 346 void DF_mkBV(MemPtr loc, int ind); //de Bruijn index 347 void DF_mkConst(MemPtr loc, int uc, int ind); //const 348 void DF_mkTConst(MemPtr loc, int uc, int ind, DF_TypePtr typeEnv); 349 //const with type association 350 void DF_mkInt(MemPtr loc, long value); //int 351 void DF_mkFloat(MemPtr loc, float value); //float 352 void DF_mkStr(MemPtr loc, DF_StrDataPtr data); //string 353 void DF_mkStrDataHead(MemPtr loc); //string data head 354 void DF_mkStream(MemPtr loc, WordPtr ind); //stream 355 void DF_setStreamInd(DF_TermPtr tm, WordPtr ind); //update index of a stream 356 void DF_mkNil(MemPtr loc); //nil 357 void DF_mkRef(MemPtr loc, DF_TermPtr target); //reference 358 void DF_mkCons(MemPtr loc, DF_TermPtr args); //cons 359 void DF_mkLam(MemPtr loc, int n, DF_TermPtr body); //abstraction 360 void DF_mkApp(MemPtr loc, int n, DF_TermPtr func, DF_TermPtr args); 361 //application 362 void DF_mkSusp(MemPtr loc, int ol, int nl, DF_TermPtr tp, DF_EnvPtr env); 363 //suspension 364 void DF_mkDummyEnv(MemPtr loc, int l, DF_EnvPtr rest); //@l env item 365 void DF_mkPairEnv(MemPtr loc, int l, DF_TermPtr t, DF_EnvPtr rest); 366 // (t, l) env item 367 368 /* TERM MODIFICATION */ 369 void DF_modVarUC(DF_TermPtr vPtr, int uc); 370 371 /* (NON_TRIVIAL) TERM COMPARISON */ 372 Boolean DF_sameConsts(DF_TermPtr const1, DF_TermPtr const2); //same const? 373 Boolean DF_sameStrs(DF_TermPtr str1, DF_TermPtr str2); //same string? 374 Boolean DF_sameStrData(DF_TermPtr tmPtr, DF_StrDataPtr strData); //same str? 375 376 /********************************************************************/ 377 /* */ 378 /* DISAGREEMENT SET REPRESENTATION */ 379 /* */ 380 /* Linked list */ 381 /********************************************************************/ 382 383 typedef struct DF_disPair //each node in the disagreement set 384 { 385 DF_Tag tag; 386 struct DF_disPair *next; 387 DF_TermPtr firstTerm; 388 DF_TermPtr secondTerm; 389 } DF_DisPair; 390 391 typedef DF_DisPair *DF_DisPairPtr; //pointer to a disagreement pair 392 393 //note this arithmatic should in reality be performed in configuration 394 #define DF_DISPAIR_SIZE (int)ceil((double)sizeof(DF_DisPair)/WORD_SIZE) 395 396 #define DF_EMPTY_DIS_SET NULL //empty disagreement set 397 398 /******************************************************************/ 399 /* Interface functions */ 400 /******************************************************************/ 401 402 //create a new node at the given location 403 void DF_mkDisPair(MemPtr loc, DF_DisPairPtr next, DF_TermPtr first, 404 DF_TermPtr second); 405 406 //decomposition 407 DF_DisPairPtr DF_disPairNext(DF_DisPairPtr disPtr); 408 DF_TermPtr DF_disPairFirstTerm(DF_DisPairPtr disPtr); 409 DF_TermPtr DF_disPairSecondTerm(DF_DisPairPtr disPtr); 410 411 //whether a given disagreement set is empty 412 Boolean DF_isEmpDisSet(DF_DisPairPtr disPtr); 413 Boolean DF_isNEmpDisSet(DF_DisPairPtr disPtr); 414 415 #endif //DATAFORMATS_H 416 417 418