blob: 0e94e0066d594f5ec3d7c0aeb9ff5fe825e69c72 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * 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');
}
}