| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * 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'); |
| } |
| } |
| |