diff options
Diffstat (limited to 'test/spass/symbol.c')
| -rw-r--r-- | test/spass/symbol.c | 1020 |
1 files changed, 1020 insertions, 0 deletions
diff --git a/test/spass/symbol.c b/test/spass/symbol.c new file mode 100644 index 0000000..ab1b0b4 --- /dev/null +++ b/test/spass/symbol.c @@ -0,0 +1,1020 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SYMBOLS * */ +/* * * */ +/* * $Module: SYMBOL * */ +/* * * */ +/* * Copyright (C) 1996, 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 GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * 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 GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "symbol.h" + +SIGNATURE *symbol_SIGNATURE; + +SYMBOL symbol_STANDARDVARCOUNTER; +SYMBOL symbol_INDEXVARCOUNTER; + +const int symbol_MASK = 3; /* 0000011 */ +const int symbol_TYPEMASK = 3; /* 0000011 */ +const int symbol_STATMASK = 4; /* 0000100 */ +const int symbol_TYPESTATMASK = 7; /* 0000111 */ + + +const int symbol_TYPEBITS = 2; +const int symbol_STATBITS = 1; +const int symbol_TYPESTATBITS = 3; + +const int symbol_SIGTYPES = 4; + +const char symbol_SKFNAME[]="skf"; +const char symbol_SKCNAME[]="skc"; +const char symbol_SKPNAME[]="SkP"; +const char symbol_SKANAME[]="SkC"; +const int symbol_SKLENGTH = 3; + +static BOOL symbol_HASSIGNATURE; +static LIST symbol_FREEDSYMBOLS; + +int symbol_ACTINDEX; +int symbol_ACTSKOLEMFINDEX; +int symbol_ACTSKOLEMCINDEX; +int symbol_ACTSKOLEMAINDEX; +int symbol_ACTSKOLEMPINDEX; +int symbol_ORDERING; +char *symbol_VARSTRING; + +SYMBOL symbol_CONTEXT[symbol__MAXSIGNATURE]; + +static unsigned long symbol_COUNT[symbol__MAXSIGNATURE]; + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SYMBOL CREATION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +int symbol_GetIncreasedOrderingCounter(void) +{ + return symbol_ORDERING++; +} + +NAT symbol_MaxStringLength(void) +/************************************************************** + INPUT: None. + RETURNS: The maximal number of characters needed for a string in the signature. +***************************************************************/ +{ + int Index; + NAT Result,Length; + SIGNATURE Entry; + + Result = 0; + + for (Index=1; Index < symbol_ACTINDEX; Index++) { + Entry = symbol_Signature(Index); + if (Entry != NULL) { + Length = Entry->length; + if (Length > Result) + Result = Length; + } + } + return Result; +} + +static SYMBOL symbol_SignatureCreate(char* String, int Type, int Arity, + int Status, PRECEDENCE Precedence) +/************************************************************** + INPUT: A pointer to a string, a type, the arity and the status + RETURNS: The symbol containing the passed parameters. + SUMMARY: Establishes a new symbol in the symbol table and returns the + internal representation (pointer and type). + CAUTION: The string is not copied! +***************************************************************/ +{ + SIGNATURE Entry; + +#ifdef CHECK + if (!symbol_SignatureExists()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_SignatureCreate:"); + misc_ErrorReport(" Module was initialized with no signature.\n"); + misc_FinishErrorReport(); + } + if (Type < 0 || Type >= symbol_SIGTYPES) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_SignatureCreate: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if ((int)symbol_ACTINDEX >= symbol__MAXSIGNATURE && + list_Empty(symbol_FREEDSYMBOLS)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n In symbol_SignatureCreate: No more symbols available.\n"); + misc_FinishUserErrorReport(); + } + + if (strlen(String)>=symbol__SYMBOLMAXLEN) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n In symbol_SignatureCreate: String too long.\n"); + misc_FinishUserErrorReport(); + } + + Entry = symbol_GetSignature(); + Entry->weight = 1; + Entry->props = 0; + Entry->name = String; + Entry->length = strlen(String); + Entry->arity = Arity; + Entry->generatedBy = list_Nil(); + + if (list_Empty(symbol_FREEDSYMBOLS)) { + Entry->info = symbol_SignatureSymbol(symbol_ACTINDEX, Type, Status); + symbol_SetSignature(symbol_ACTINDEX++, Entry); + } + else { + int Index; + + Index = (int)list_Car(symbol_FREEDSYMBOLS); + symbol_FREEDSYMBOLS = list_PointerDeleteElement(symbol_FREEDSYMBOLS, + (POINTER)Index); + Entry->info = symbol_SignatureSymbol(Index, Type, Status); + symbol_SetSignature(Index, Entry); + } + + /* Define precedence of symbol */ + symbol_SetIncreasedOrdering(Precedence, Entry->info); + + return Entry->info; +} + + +SYMBOL symbol_CreateFunction(const char* String, int Arity, int Status, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A string defining a symbol name, an arity, the status the + created function symbol is supposed to have and a precedence + object. + RETURNS: A new symbol for a new function. + SUMMARY: Creates a new function symbol. + EFFECTS: Inserts the new function in the symbol table. + The precedence of the new symbol is set in <Precedence>. +***************************************************************/ +{ + if (Arity == 0) + return symbol_SignatureCreate(strcpy(memory_Malloc(symbol__SYMBOLMAXLEN), + String), + symbol_CONSTANT, Arity, Status, Precedence); + else + return symbol_SignatureCreate(strcpy(memory_Malloc(symbol__SYMBOLMAXLEN), + String), + symbol_FUNCTION, Arity, Status, Precedence); +} + +SYMBOL symbol_CreateSkolemFunction(int Arity, PRECEDENCE Precedence) +/************************************************************** + INPUT: The arity of a function to be created, and a precedence. + RETURNS: A new skolem symbol having the required arity. + SUMMARY: Creates a new function symbol. + EFFECTS: Inserts the new function in the symbol table. + The precedence of the new symbol is set in <Precedence>. +***************************************************************/ +{ + char newname[10]; + SYMBOL Result; + + Result = (SYMBOL)NULL; + + while (Result == (SYMBOL)NULL) { + if (Arity == 0) + sprintf(newname,"%s%d",symbol_SKCNAME,symbol_ACTSKOLEMCINDEX++); + else + sprintf(newname,"%s%d",symbol_SKFNAME,symbol_ACTSKOLEMFINDEX++); + if (symbol_Lookup(newname) == 0) + Result = symbol_CreateFunction(newname, Arity, symbol_STATLEX, Precedence); + } + + symbol_AddProperty(Result,SKOLEM); + + return Result; +} + + +SYMBOL symbol_CreatePredicate(const char* String, int Arity, int Status, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A string, a symbol arity, the status the created predicate + is supposed to have, and a precedence object. + RETURNS: A new symbol for a new predicate. + SUMMARY: Creates a new predicate symbol. + EFFECTS: Inserts the new predicate symbol into the symbol table. + The precedence of the new symbol is set in <Precedence>. +***************************************************************/ +{ + return symbol_SignatureCreate(strcpy(memory_Malloc(symbol__SYMBOLMAXLEN), + String), + symbol_PREDICATE, Arity, Status, Precedence); +} + +SYMBOL symbol_CreateSkolemPredicate(int Arity, PRECEDENCE Precedence) +/************************************************************** + INPUT: The arity of a new Skolem predicate symbol and a precedence object. + RETURNS: A new symbol for a new predicate. + SUMMARY: Creates a new predicate symbol. + EFFECTS: Inserts the new predicate symbol into the symbol table. + The precedence of the new symbol is set in <Precedence>. +***************************************************************/ +{ + char newname[10]; + SYMBOL Result; + + Result = (SYMBOL)NULL; + + while (Result == (SYMBOL)NULL) { + if (Arity==0) + sprintf(newname,"%s%d",symbol_SKANAME,symbol_ACTSKOLEMAINDEX++); + else + sprintf(newname,"%s%d",symbol_SKPNAME,symbol_ACTSKOLEMPINDEX++); + if (symbol_Lookup(newname) == 0) + Result = symbol_CreatePredicate(newname, Arity, symbol_STATLEX, Precedence); + } + + return Result; +} + + +SYMBOL symbol_CreateJunctor(const char* String, int Arity, int Status, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A string, a symbol arity, the status the created junctor + is supposed to have, and a precedence object. + RETURNS: A new symbol for a new junctor. + SUMMARY: Creates a new junctor symbol. + EFFECTS: Inserts the new junctor symbol into the symbol table. + The precedence of the new symbol is set in <Precedence>. +***************************************************************/ +{ + return symbol_SignatureCreate(strcpy(memory_Malloc(symbol__SYMBOLMAXLEN), + String), + symbol_JUNCTOR, Arity, Status, Precedence); +} + + +BOOL symbol_IsSymbol(SYMBOL Symbol) +/************************************************************** + INPUT: A symbol. + RETURNS: TRUE if the symbols is a variable or contained + in the symbol table. +***************************************************************/ +{ + return + (!symbol_SignatureExists() || + ((!symbol_Equal(Symbol, symbol__NULL)) && + ((symbol_IsVariable(Symbol) && Symbol<symbol_MaxVars()) || + (symbol_IsSignature(Symbol) && symbol_Index(Symbol)<symbol_ACTINDEX)))); +} + + +void symbol_Delete(SYMBOL Symbol) +/************************************************************** + INPUT: A symbol. + RETURNS: Nothing. + SUMMARY: Deletes the symbol from the symbol table and frees its memory. +***************************************************************/ +{ +#ifdef CHECK + if (!symbol_SignatureExists()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_Delete: Module was initialized without signature.\n"); + misc_FinishErrorReport(); + } + if (!symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_Delete: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (!symbol_IsVariable(Symbol)) { + int Index; + SIGNATURE Entry; + + Index = symbol_Index(Symbol); + symbol_FREEDSYMBOLS = list_Cons((POINTER)Index,symbol_FREEDSYMBOLS); + Entry = symbol_Signature(Index); + symbol_SetSignature(Index, NULL); + symbol_FreeSignature(Entry); + } +} + +LIST symbol_GetAllSymbols(void) +/************************************************************** + INPUT: None. + RETURNS: A list of all generated symbols. +***************************************************************/ +{ + LIST Result; + + Result = list_Nil(); + + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL) { + Result = list_Cons((POINTER)symbol_GetSigSymbol(Index), Result); + } + } + } + return Result; +} + + +LIST symbol_GetAllPredicates(void) +/************************************************************** + INPUT: None. + RETURNS: A list of all predicate symbols. +***************************************************************/ +{ + LIST Result; + + Result = list_Nil(); + + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL && symbol_IsPredicate(symbol_GetSigSymbol(Index))) + Result = list_Cons((POINTER)symbol_GetSigSymbol(Index), Result); + } + } + return Result; +} + + +LIST symbol_GetAllFunctions(void) +/************************************************************** + INPUT: None. + RETURNS: A list of all function symbols. +***************************************************************/ +{ + LIST Result; + + Result = list_Nil(); + + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL && symbol_IsFunction(symbol_GetSigSymbol(Index))) + Result = list_Cons((POINTER)symbol_GetSigSymbol(Index), Result); + } + } + return Result; +} + + +void symbol_FreeAllSymbols(void) +/************************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECTS: Frees all generated symbols +***************************************************************/ +{ + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL) + symbol_FreeSignature(S); + } + memory_Free(symbol_SIGNATURE, sizeof(SIGNATURE[symbol__MAXSIGNATURE])); + } + + memory_Free(symbol_VARSTRING, symbol__SYMBOLMAXLEN); + list_Delete(symbol_FREEDSYMBOLS); +} + + +void symbol_Init(BOOL Signature) +/************************************************************** + INPUT: A flag indicating whether a signature is used or not. + RETURNS: None. + SUMMARY: Initializes the Symbol Module. + EFFECTS: Initializes global variables. + CAUTION: MUST BE CALLED BEFORE ANY OTHER Symbol-FUNCTION. +***************************************************************/ +{ + symbol_ResetSkolemIndex(); + symbol_ContextClean(); + + if (Signature) + symbol_SIGNATURE = (SIGNATURE*)memory_Malloc(sizeof(SIGNATURE[symbol__MAXSIGNATURE])); + + symbol_STANDARDVARCOUNTER = symbol_GetInitialStandardVarCounter(); + symbol_INDEXVARCOUNTER = symbol_GetInitialIndexVarCounter(); + + symbol_ACTINDEX = 1; + symbol_ORDERING = 1; + symbol_VARSTRING = memory_Malloc(symbol__SYMBOLMAXLEN); + + symbol_HASSIGNATURE = Signature; + symbol_FREEDSYMBOLS = list_Nil(); +} + + +BOOL symbol_SignatureExists(void) +/************************************************************** + INPUT: None. + RETURNS: TRUE, if a symbol signature was created, FALSE otherwise. +***************************************************************/ +{ + return symbol_HASSIGNATURE; +} + +void symbol_ReinitGenericNameCounters(void) +/************************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECTS: Scans the symbol signature for generic names and if + there exists some, the corresponding counters are increased. +***************************************************************/ +{ + if (symbol_SignatureExists()) { + int Index,Num; + SYMBOL Info; + SIGNATURE Entry; + char *Name,*Subname; + + for (Index=1; Index < symbol_ACTINDEX; Index++) { + Entry = symbol_Signature(Index); + if (Entry != NULL) { + Info = Entry->info; + Name = Entry->name; + if (strlen(Name)>symbol_SKLENGTH) { + Subname = Name + symbol_SKLENGTH; + + switch (symbol_Type(Info)) { + + case symbol_CONSTANT: + if (strncmp(Name,symbol_SKCNAME,symbol_SKLENGTH) == 0 && + string_StringIsNumber(Subname)) { + Num = atoi(Subname); + if (Num >= symbol_ACTSKOLEMCINDEX) + symbol_ACTSKOLEMCINDEX = Num + 1; + } + break; + case symbol_FUNCTION: + if (strncmp(Name,symbol_SKFNAME,symbol_SKLENGTH) == 0 && + string_StringIsNumber(Subname)) { + Num = atoi(Subname); + if (Num >= symbol_ACTSKOLEMFINDEX) + symbol_ACTSKOLEMFINDEX = Num + 1; + } + break; + case symbol_PREDICATE: + if (Entry->arity == 0) { + if (strncmp(Name,symbol_SKANAME,symbol_SKLENGTH) == 0 && + string_StringIsNumber(Subname)) { + Num = atoi(Subname); + if (Num >= symbol_ACTSKOLEMAINDEX) + symbol_ACTSKOLEMAINDEX = Num + 1; + } + } + else { + if (strncmp(Name,symbol_SKPNAME,symbol_SKLENGTH) == 0 && + string_StringIsNumber(Subname)) { + Num = atoi(Subname); + if (Num >= symbol_ACTSKOLEMPINDEX) + symbol_ACTSKOLEMPINDEX = Num + 1; + } + } + } + } + } + } + } +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SYMBOL SEARCHING * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +SYMBOL symbol_Lookup(const char* String) +/********************************************************** + INPUT: A pointer to a string. + RETURNS: If a symbol with name String exists in the signature, the symbol; + 0 otherwise +********************************************************/ +{ + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL && string_Equal(String, S->name)) + return S->info; + } + } + + return 0; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SPECIALS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void symbol_LowerSignature(void) +/************************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECT: Any predicate or function symbol in the signature that + starts with a capital letter is prefixed with "ss" +***************************************************************/ +{ + int Index; + SIGNATURE Entry; + SYMBOL Info; + char* String; + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + Entry = symbol_Signature(Index); + if (Entry != NULL) { + Info = Entry->info; + + if (symbol_IsPredicate(Info) || symbol_IsFunction(Info)) { + String = Entry->name; + if ('A' <= String[0] && String[0] <= 'Z') { + char* New; + New = (char *)memory_Malloc(symbol__SYMBOLMAXLEN); + strcpy(&(New[2]),String); + New[0] = New[1] = 's'; /* prefix "ss" */ + + Entry->name = New; + memory_Free(String,symbol__SYMBOLMAXLEN); + } + } + } + } +} + +void symbol_Dump(PRECEDENCE Precedence) +/************************************************************** + INPUT: A precedence + RETURNS: Nothing. + EFFECT: Dumps all existing symbols to stdout. +***************************************************************/ +{ + if (symbol_SignatureExists()) { + int Index; + SIGNATURE S; + fputs("Dump:", stdout); + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL) + printf("\n\t %4d:%4d:%4d:%4d:%4d:%s:%d", Index, S->info, S->weight, + Precedence[Index], S->props, S->name, S->length); + } + } +} + + +LIST symbol_SortByPrecedence(LIST Symbols, PRECEDENCE Precedence) +/************************************************************** + INPUT: A list of symbols, and a precedence. + RETURNS: The same list where the elements are sorted with + respect to decreasing precedence. + CAUTION: Destructive. +***************************************************************/ +{ + LIST Scan1,Scan2,Min; + POINTER Exchange; + + /* We can't use list_Sort, since list_Sort expects an ordering + function that receives two arguments. Since symbol_PrecedenceGreater + requires three arguments, we have to define our own sorting function. + */ + + for (Scan1=Symbols; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) { + Min = Scan1; + for (Scan2 = list_Cdr(Scan1); !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) + if (symbol_PrecedenceGreater(Precedence, (SYMBOL) list_Car(Scan2), + (SYMBOL) list_Car(Min))) { + Exchange = list_Car(Min); + list_Rplaca(Min, list_Car(Scan2)); + list_Rplaca(Scan2, Exchange); + } + } + + return Symbols; +} + +void symbol_RearrangePrecedence(PRECEDENCE Precedence, LIST UserPrecedence) +/************************************************************** + INPUT: A precedence and a list of symbols in the user + specified precedence, sorted in decreasing order. + RETURNS: Nothing. + EFFECT: Modifies the given precedence to comply with the + symbol precedence selected by the user. +***************************************************************/ +{ + LIST Scan1, Scan2, Precedences; + + Precedences = list_Nil(); + + for (Scan1 = UserPrecedence; !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) { + Precedences = list_Cons((POINTER) symbol_Ordering(Precedence, (SYMBOL) list_Car(Scan1)), + Precedences); + } + + Precedences = list_PointerSort(Precedences); + + Scan1 = UserPrecedence; + Scan2 = Precedences; + + while (Scan1 != list_Nil() && Scan2 != list_Nil()) { + symbol_SetOrdering(Precedence, (SYMBOL) list_Car(Scan1), (int) list_Car(Scan2)); + Scan1 = list_Cdr(Scan1); + Scan2 = list_Cdr(Scan2); + } + + list_Delete(Precedences); +} + +/* unused */ +void symbol_PrintPrecedence(PRECEDENCE Precedence) +/************************************************************** + INPUT: A precedence. + RETURNS: Nothing. + EFFECT: Prints the precedence to stdout. +***************************************************************/ +{ + if (symbol_SignatureExists()) { + LIST Symbols, Scan; + int Index; + SIGNATURE S; + Symbols = list_Nil(); + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL && + (symbol_IsPredicate(S->info) || symbol_IsFunction(S->info))) + Symbols = list_Cons((POINTER)S->info, Symbols); + } + Symbols = symbol_SortByPrecedence(Symbols, Precedence); + + for (Scan = Symbols; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + S = symbol_Signature(symbol_Index((SYMBOL)list_Car(Scan))); + fputs(S->name, stdout); + if (!list_Empty(list_Cdr(Scan))) + fputs(" > ", stdout); + } + list_Delete(Symbols); + } +} + + +void symbol_FPrintPrecedence(FILE *File, PRECEDENCE Precedence) +/************************************************************** + INPUT: A file pointer and a precedence. + RETURNS: void + EFFECT: Prints the current precedence as a setting command + in DFG syntax to <File>. +***************************************************************/ +{ + if (symbol_SignatureExists()) { + LIST Symbols,Scan; + int Index; + SIGNATURE S; + + Symbols = list_Nil(); + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + S = symbol_Signature(Index); + if (S != NULL && + (symbol_IsPredicate(S->info) || symbol_IsFunction(S->info))) + Symbols = list_Cons((POINTER)S->info, Symbols); + } + Symbols = symbol_SortByPrecedence(Symbols, Precedence); + Index = 0; + fputs("set_precedence(", File); + for (Scan = Symbols; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + S = symbol_Signature(symbol_Index((SYMBOL)list_Car(Scan))); + fputs(S->name, File); + if (!list_Empty(list_Cdr(Scan))) + putc(',', File); + if (Index > 15) { + Index = 0; + fputs("\n\t", File); + } + else + Index++; + } + fputs(").", File); + list_Delete(Symbols); + } +} + +void symbol_SetCount(SYMBOL Symbol, unsigned long Count) +/************************************************************** + INPUT: A symbol, and a symbol count. + RETURNS: Nothing. + SUMMARY: Sets the symbol count for the symbol to Count. +***************************************************************/ +{ + symbol_COUNT[symbol_Index(Symbol)] = Count; +} + +unsigned long symbol_GetCount(SYMBOL Symbol) +/************************************************************** + INPUT: A symbol. + RETURNS: The number of occurences of the symbol in the clause + set. + SUMMARY: Gets the symbol count for the symbol. +***************************************************************/ +{ + return symbol_COUNT[symbol_Index(Symbol)]; +} + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SYMBOL OUTPUT * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void symbol_Print(SYMBOL Symbol) +/************************************************************** + INPUT: A symbol. + RETURNS: Nothing. + SUMMARY: Prints a symbol to stdout. +***************************************************************/ +{ + symbol_FPrint(stdout, Symbol); +} + + +void symbol_FPrint(FILE* File, SYMBOL Symbol) +/************************************************************** + INPUT: A file and a symbol. + RETURNS: None. + SUMMARY: Prints a symbol to the file. +***************************************************************/ +{ +#ifdef CHECK + if (!symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_FPrint: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (symbol_Equal(symbol_Null(),Symbol)) + fputs("NULL", File); + else if (symbol_IsVariable(Symbol)) { + SYMBOL NormSymbol; + + NormSymbol = symbol_NormVar(Symbol); + + if (symbol_IsStandardVariable(Symbol)) { + if (Symbol <= 6) + /* U, V, W, X, Y, Z */ + sprintf(symbol_VARSTRING,"%c", 'U' + NormSymbol - 1); + else + /* X1, X2, X3, ... */ + sprintf(symbol_VARSTRING,"X%d", NormSymbol - 6); + } + else if (symbol_IsIndexVariable(Symbol)) + /* I1, I2, I3, ... */ + sprintf(symbol_VARSTRING,"I%d", NormSymbol); + + fputs(symbol_VARSTRING, File); + } + else if (symbol_SignatureExists()) + fputs(symbol_Name(Symbol), File); + else + fprintf(File, "%d", Symbol); +} + + +void symbol_FPrintOtter(FILE* File, SYMBOL Symbol) +/************************************************************** + INPUT: A file and a symbol. + RETURNS: None. + SUMMARY: Prints a symbol in Otter format to stdout. +***************************************************************/ +{ +#ifdef CHECK + if (!symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In symbol_FPrintOtter: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (symbol_IsVariable(Symbol)) { + SYMBOL NormSymbol; + + NormSymbol = symbol_NormVar(Symbol); + + if (symbol_IsStandardVariable(Symbol)) { + if (Symbol <= 6) + /* u, v, w, x, y, z */ + sprintf(symbol_VARSTRING,"%c", 116 + NormSymbol); + else + /* x1, x2, x3, ... */ + sprintf(symbol_VARSTRING,"x%d", NormSymbol - 6); + } + else if (symbol_IsIndexVariable(Symbol)) + /* I1, I2, I3, ... */ + sprintf(symbol_VARSTRING,"I%d", NormSymbol); + + fputs(symbol_VARSTRING, File); + } + else + if (symbol_SignatureExists()) { + if (symbol_IsConstant(Symbol)) + fprintf(File, "c%s", symbol_Name(Symbol)); + else + if (symbol_IsFunction(Symbol)) + fprintf(File, "f%s", symbol_Name(Symbol)); + else + if (symbol_IsPredicate(Symbol)) + fprintf(File, "P%s", symbol_Name(Symbol)); + else + fputs(symbol_Name(Symbol), File); + } + else + fprintf(File, "%d", Symbol); +} + + +void symbol_PrintLn(SYMBOL Symbol) +/************************************************************** + INPUT: A symbol. + RETURNS: None. + SUMMARY: Prints a symbol and a newline to stdout. +***************************************************************/ +{ + symbol_Print(Symbol); + putchar('\n'); + +} + + +void symbol_PrintAll(void) +/************************************************************** + INPUT: None. + RETURNS: None. + SUMMARY: Prints all symbols to stdout. +***************************************************************/ +{ + const int symbol_TABLEBLANKS = 2; + const int symbol_TABLETYPE = 6; /* breadth of the columns */ + const int symbol_TABLEARITY = 7; + const int symbol_TABLESTAT = 6; + const int symbol_TABLEPROP = 8; + const int symbol_TABLESTRING = 36; + + if (symbol_SignatureExists()) { + int Index; + SYMBOL Info; + SIGNATURE Entry; + unsigned int TypePos, ArityPos, StatPos, PropPos, StringPos, EndPos, ActPos; + + TypePos = symbol_TABLEBLANKS; + ArityPos = TypePos + symbol_TABLETYPE + 1; + StatPos = ArityPos + symbol_TABLEARITY + 1; + PropPos = StatPos + symbol_TABLESTAT + 1; + StringPos = PropPos + symbol_TABLEPROP + 1; + EndPos = StringPos + symbol_TABLESTRING + 1; + + fputs("\n\n", stdout); + misc_PrintChar(symbol_TABLEBLANKS, ' '); putchar('+'); + misc_PrintChar(symbol_TABLETYPE, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEARITY, '-'); putchar('+'); + misc_PrintChar(symbol_TABLESTAT, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEPROP, '-'); putchar('+'); + misc_PrintChar(symbol_TABLESTRING, '-'); putchar('+'); putchar('\n'); + misc_PrintChar(symbol_TABLEBLANKS, ' '); putchar('|'); + ActPos = TypePos + 1 + fputs(" Type", stdout); + misc_PrintChar((ArityPos - ActPos), ' '); putchar('|'); + ActPos = ArityPos + 1 + fputs(" Arity", stdout); + misc_PrintChar((StatPos - ActPos), ' '); putchar('|'); + ActPos = StatPos + 1 + fputs(" Stat", stdout); + misc_PrintChar((PropPos - ActPos), ' '); putchar('|'); + ActPos = PropPos + 1 + fputs(" Prop", stdout); + misc_PrintChar((StringPos - ActPos), ' '); putchar('|'); + ActPos = StringPos + 1 + fputs(" String", stdout); + misc_PrintChar((EndPos - ActPos), ' '); putchar('|'); putchar('\n'); + misc_PrintChar(symbol_TABLEBLANKS, ' '); putchar('+'); + misc_PrintChar(symbol_TABLETYPE, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEARITY, '-'); putchar('+'); + misc_PrintChar(symbol_TABLESTAT, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEPROP, '-'); putchar('+'); + misc_PrintChar(symbol_TABLESTRING, '-'); putchar('+'); putchar('\n'); + + for (Index = 1; Index < symbol_ACTINDEX; Index++) { + Entry = symbol_Signature(Index); + if (Entry != NULL) { + Info = Entry->info; + + misc_PrintChar(symbol_TABLEBLANKS, ' '); putchar('|'); + ActPos = TypePos + 1; + + switch (symbol_Type(Info)) { + case symbol_CONSTANT: + ActPos += fputs(" Con", stdout); break; + case symbol_FUNCTION: + ActPos += fputs(" Fun", stdout); break; + case symbol_PREDICATE: + ActPos += fputs(" Pre", stdout); break; + case symbol_JUNCTOR: + ActPos += fputs(" Jun", stdout); break; + } + misc_PrintChar((ArityPos - ActPos), ' '); putchar('|'); + ActPos = ArityPos + 1 + printf(" %3d", Entry->arity); + misc_PrintChar((StatPos - ActPos), ' '); putchar('|'); + ActPos = StatPos + 1; + if (symbol_Type(Info) == symbol_FUNCTION) { + switch (symbol_Stat(Info)) { + case symbol_STATLEX: + ActPos += fputs(" Lex", stdout); break; + case symbol_STATMUL: + ActPos += fputs(" Mul", stdout); break; + } + } + misc_PrintChar((PropPos - ActPos), ' '); putchar('|'); + ActPos = PropPos + 1 + printf(" %u", Entry->props); + misc_PrintChar((StringPos - ActPos), ' '); putchar('|'); + ActPos = StringPos + 1 + printf(" %s", Entry->name); + misc_PrintChar((EndPos - ActPos), ' '); putchar('|'); putchar('\n'); + } + } + misc_PrintChar(symbol_TABLEBLANKS, ' '); putchar('+'); + misc_PrintChar(symbol_TABLETYPE, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEARITY, '-'); putchar('+'); + misc_PrintChar(symbol_TABLESTAT, '-'); putchar('+'); + misc_PrintChar(symbol_TABLEPROP, '-'); putchar('|'); + misc_PrintChar(symbol_TABLESTRING, '-'); putchar('+'); putchar('\n'); + } +} + |