/**************************************************************/ /* ********************************************************** */ /* * * */ /* * TERMS * */ /* * * */ /* * $Module: TERM * */ /* * * */ /* * 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 "term.h" /**************************************************************/ /* Global variables */ /**************************************************************/ NAT term_MARK; POINTER term_BIND[symbol__MAXVARIABLES][2]; #ifdef CHECK BOOL term_BINDPHASE; #endif NAT term_STAMP; BOOL term_STAMPBLOCKED; static BOOL term_STAMPOVERFLOW[term_MAXSTAMPUSERS]; static NAT term_STAMPUSERS; /**************************************************************/ /* ********************************************************** */ /* * * */ /* * TERM CREATION FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void term_Init(void) /********************************************************** INPUT: None. RETURNS: None. CAUTION: The term module is initialized. ***********************************************************/ { int i; term_MARK = 1; term_STAMP = 0; term_STAMPBLOCKED = FALSE; for (i = 0; i < term_MAXSTAMPUSERS; i++) term_STAMPOVERFLOW[i] = FALSE; term_STAMPUSERS = 0; #ifdef CHECK term_BINDPHASE = FALSE; #endif } TERM term_Create(SYMBOL Symbol, LIST List) /********************************************************** INPUT: A symbol and a list of arguments. RETURNS: A term consisting of the top symbol 'Symbol' and the arguments stored in 'List'. CAUTION: None. ********************************************************/ { TERM Result; #ifdef CHECK if (!symbol_IsSymbol(Symbol) || !term_IsTermList(List)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_Create: Illegal input."); misc_FinishErrorReport(); } #endif Result = (TERM)memory_Malloc(sizeof(TERM_NODE)); Result->symbol = Symbol; Result->args = List; Result->super.termlist = list_Nil(); Result->stamp = 0; Result->size = 0; return Result; } TERM term_CreateAddFather(SYMBOL Symbol, LIST List) /********************************************************** INPUT: A symbol and a list of arguments. RETURNS: A term consisting of the top symbol 'Symbol' and the arguments stored in 'List'. In contrast to term_Create the superterm members are set for the arguments. CAUTION: None. ********************************************************/ { TERM Result; LIST l; Result = term_Create(Symbol, List); for (l=term_ArgumentList(Result); !list_Empty(l); l = list_Cdr(l)) term_RplacSuperterm((TERM) list_Car(l), Result); return Result; } TERM term_CreateStandardVariable(void) /********************************************************** RETURNS: Returns a term with a new variable as top symbol. ***********************************************************/ { return term_Create(symbol_CreateStandardVariable(), list_Nil()); } void term_Delete(TERM Term) /********************************************************** INPUT: A term. SUMMARY: Deletes the term and frees the storage. CAUTION: The arguments of Term are also deleted. ********************************************************/ { if (term_IsComplex(Term)) { LIST Scan; for (Scan = term_ArgumentList(Term); list_Exist(Scan); Scan = list_Cdr(Scan)) term_Delete(list_Car(Scan)); list_Delete(term_ArgumentList(Term)); } term_Free(Term); } void term_DeleteIterative(TERM Term) /********************************************************** INPUT: A term. SUMMARY: Deletes the term and frees the storage. CAUTION: The arguments of Term are also deleted. ********************************************************/ { if (term_IsComplex(Term)) { LIST Stack, Aux; Stack = list_StackBottom(); do { if (term_IsComplex(Term)) Stack = list_Push(term_ArgumentList(Term),Stack); term_Free(Term); while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) Stack = list_Pop(Stack); if (!list_StackEmpty(Stack)) { Aux = list_Top(Stack); Term = (TERM)list_Car(Aux); list_RplacTop(Stack, list_Cdr(Aux)); list_Free(Aux); } } while (!list_StackEmpty(Stack)); } else term_Free(Term); } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * PRIMITIVE TERM FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ BOOL term_Equal(TERM Term1, TERM Term2) /********************************************************* INPUT: Two terms. RETURNS: The boolean value TRUE if the terms are equal. CAUTION: EQUAL FUNCTION- OR PREDICATE SYMBOLS SHARE THE SAME ARITY. THIS IS NOT VALID FOR JUNCTORS! **********************************************************/ { #ifdef CHECK if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_Equal: Illegal input."); misc_FinishErrorReport(); } #endif /* if (term_IsIndexVariable(Term1)) puts("\nterm_Equal: Left index variable."); else if (term_IsIndexVariable(Term2)) puts("\nterm_Equal: Right index variable."); fflush(stdout); */ if (Term1 == Term2) /* pointers are equal */ return TRUE; else if (!term_EqualTopSymbols(Term1, Term2)) return FALSE; else if (term_ArgumentList(Term1)) { LIST Scan1, Scan2; for (Scan1=term_ArgumentList(Term1), Scan2=term_ArgumentList(Term2); list_Exist(Scan1) && list_Exist(Scan2); Scan1=list_Cdr(Scan1), Scan2=list_Cdr(Scan2)) if (!term_Equal(list_Car(Scan1),list_Car(Scan2))) return FALSE; return (list_Empty(Scan1) ? list_Empty(Scan2) : FALSE); } else return TRUE; } BOOL term_EqualIterative(TERM Term1, TERM Term2) /********************************************************* INPUT: Two terms. RETURNS: The boolean value TRUE if the terms are equal. CAUTION: Notice that there may be symbols with arbitrary arity *******************************************************/ { LIST Stack1,Stack2; #ifdef CHECK if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_EqualIterative: Illegal input."); misc_FinishErrorReport(); } #endif Stack1 = Stack2 = list_StackBottom(); do { if (term_EqualTopSymbols(Term1,Term2) && term_IsComplex(Term1) && term_IsComplex(Term2)) { Stack1 = list_Push(term_ArgumentList(Term1),Stack1); Stack2 = list_Push(term_ArgumentList(Term2),Stack2); } if (!term_EqualTopSymbols(Term1,Term2) || term_IsComplex(Term1) != term_IsComplex(Term2)) { Stack1 = list_StackFree(Stack1); Stack2 = list_StackFree(Stack2); return FALSE; } while (!list_StackEmpty(Stack1) && list_Empty(list_Top(Stack1))) if (!list_StackEmpty(Stack2) && list_Empty(list_Top(Stack2))) { Stack1 = list_Pop(Stack1); Stack2 = list_Pop(Stack2); } else { Stack1 = list_StackFree(Stack1); Stack2 = list_StackFree(Stack2); return FALSE; } if (!list_StackEmpty(Stack1)) { if (!list_Empty(list_Top(Stack2))) { Term1 = (TERM)list_Car(list_Top(Stack1)); list_RplacTop(Stack1, list_Cdr(list_Top(Stack1))); Term2 = (TERM)list_Car(list_Top(Stack2)); list_RplacTop(Stack2, list_Cdr(list_Top(Stack2))); } else { Stack1 = list_StackFree(Stack1); Stack2 = list_StackFree(Stack2); return FALSE; } } } while (!list_StackEmpty(Stack1)); return TRUE; } BOOL term_VariableEqual(TERM Variable1, TERM Variable2) /********************************************************* INPUT: Two Variables. RETURNS: The boolean value TRUE, if the variables are equal. **********************************************************/ { return term_EqualTopSymbols(Variable1, Variable2); } BOOL term_IsGround(TERM Term) /********************************************************** INPUT: A term. RETURNS: A boolean value which is TRUE, if 'Term' is a ground term, i.e. does not contain variables. ********************************************************/ { #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_IsGround: Illegal input."); misc_FinishErrorReport(); } #endif if (term_IsComplex(Term)) { LIST Stack; Stack = list_StackBottom(); do { if (term_IsComplex(Term)) Stack = list_Push(term_ArgumentList(Term),Stack); else if (term_IsVariable(Term)) { Stack = list_StackFree(Stack); return FALSE; } while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) Stack = list_Pop(Stack); if (!list_StackEmpty(Stack)) { Term = (TERM)list_Car(list_Top(Stack)); list_RplacTop(Stack, list_Cdr(list_Top(Stack))); } } while (!list_StackEmpty(Stack)); return TRUE; } else return !term_IsVariable(Term); } BOOL term_IsTerm(TERM Term) /********************************************************* INPUT: A term. RETURNS: TRUE, if 'Term' is not NULL and has a symbol as its top symbol. **********************************************************/ { return (Term != (TERM)NULL && symbol_IsSymbol(term_TopSymbol(Term))); } BOOL term_IsTermList(LIST TermList) /********************************************************* INPUT: A term. RETURNS: TRUE iff is a list of terms. *******************************************************/ { for ( ; !list_Empty(TermList); TermList=list_Cdr(TermList)) if (!(term_IsTerm((TERM)list_Car(TermList)))) return FALSE; return TRUE; } BOOL term_AllArgsAreVar(TERM Term) /********************************************************* INPUT: A term. RETURNS: The boolean value TRUE, if all arguments of the term are variables. *******************************************************/ { LIST Scan; for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) if (!term_IsVariable(list_Car(Scan))) return FALSE; return TRUE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * LOW LEVEL FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ TERM term_Copy(TERM Term) /********************************************************** INPUT: A term. RETURNS: A copy of 'Term' where the stamp field is copied, too. SUMMARY: Copies "Term" and returns a pointer to the copy. *********************************************************/ { TERM Result; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_Copy: Illegal input."); misc_FinishErrorReport(); } #endif if (term_IsComplex(Term)) { LIST Scan, ArgumentList; for (Scan = ArgumentList = list_Copy(term_ArgumentList(Term)); list_Exist(Scan); Scan = list_Cdr(Scan)) list_Rplaca(Scan, term_Copy(list_Car(Scan))); Result = term_Create(term_TopSymbol(Term), ArgumentList); } else Result = term_Create(term_TopSymbol(Term), list_Nil()); Result->stamp = Term->stamp; Result->size = Term->size; return Result; } TERM term_CopyIterative(TERM Term) /********************************************************** INPUT: A term. RETURNS: A copy of . SUMMARY: Copies and returns a pointer to the copy. *********************************************************/ { #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_CopyIterative: Illegal input."); misc_FinishErrorReport(); } #endif if (term_IsComplex(Term)) { LIST TopStack, ArgumentStack, ActStack; TopStack = list_Push((POINTER)term_TopSymbol(Term), list_StackBottom()); ArgumentStack = list_Push(list_Copy(term_ArgumentList(Term)), list_StackBottom()); ActStack = list_Push(list_Top(ArgumentStack), list_StackBottom()); while (!list_StackEmpty(TopStack)) { if (list_Empty(list_Top(ActStack))) { Term = term_Create((SYMBOL)list_Top(TopStack), (LIST)list_Top(ArgumentStack)); TopStack = list_Pop(TopStack); ArgumentStack = list_Pop(ArgumentStack); ActStack = list_Pop(ActStack); if (!list_StackEmpty(TopStack)) { list_Rplaca(list_Top(ActStack), Term); list_RplacTop(ActStack, list_Cdr(list_Top(ActStack))); } } else { Term = (TERM)list_Car(list_Top(ActStack)); if (term_IsComplex(Term)) { TopStack = list_Push((POINTER)term_TopSymbol(Term), TopStack); ArgumentStack = list_Push(list_Copy(term_ArgumentList(Term)), ArgumentStack); ActStack = list_Push(list_Top(ArgumentStack), ActStack); } else { list_Rplaca(list_Top(ActStack), term_Create(term_TopSymbol(Term), list_Nil())); list_RplacTop(ActStack, list_Cdr(list_Top(ActStack))); } } } return Term; } else return term_Create(term_TopSymbol(Term), list_Nil()); } TERM term_CopyWithEmptyArgListNode(TERM Term, LIST ArgListNode, LIST* ListNodeCopyPt) /********************************************************** INPUT: A term and a pointer to an argument list node of this term. RETURNS: A copy of 'Term' with a NULL as list_Car(ListNodeCopy). SUMMARY: Copies "Term" and returns a pointer to the copy. *********************************************************/ { #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_CopyWithEmptyArgListNode: Illegal input."); misc_FinishErrorReport(); } #endif if (term_IsComplex(Term)) { LIST Scan, ArgumentList, HelpScan; TERM Result; HelpScan = term_ArgumentList(Term); ArgumentList = list_Copy(HelpScan); for (Scan = ArgumentList; list_Exist(Scan); Scan = list_Cdr(Scan),HelpScan = list_Cdr(HelpScan)) if (HelpScan != ArgListNode) list_Rplaca(Scan, term_CopyWithEmptyArgListNode(list_Car(Scan), ArgListNode, ListNodeCopyPt)); else{ list_Rplaca(Scan, (TERM)NULL); *ListNodeCopyPt = Scan; } Result = (TERM)memory_Malloc(sizeof(TERM_NODE)); Result->symbol = term_TopSymbol(Term); Result->args = ArgumentList; Result->super.termlist = list_Nil(); return Result; } else return term_Create(term_TopSymbol(Term), list_Nil()); } void term_PrintWithEmptyArgListNode(TERM Term) /************************************************************** INPUT: A term. RETURNS: none. SUMMARY: Prints any term to stdout, especially terms with empty argument list nodes. CAUTION: Uses the other term_Output functions. *************************************************************/ { if (Term == (TERM)NULL) fputs("(NULL)", stdout); else if (term_IsComplex(Term)) { putchar('('); symbol_Print(term_TopSymbol(Term)); putchar(' '); list_Apply((void (*)(POINTER)) term_PrintWithEmptyArgListNode, term_ArgumentList(Term)); putchar(')'); } else if (term_IsVariable(Term)) { symbol_Print(term_TopSymbol(Term)); } else { /* term_IsConstant(Term) */ putchar('('); symbol_Print(term_TopSymbol(Term)); putchar(')'); } } BOOL term_ReplaceSubtermBy(TERM Atom, TERM TermS, TERM TermT) /************************************************************** INPUT: Three terms. RETURNS: None. EFFECT: Replaces all occurrences of TermS in Atom by TermT. Top level is NOT considered! *************************************************************/ { LIST ArgListNode; BOOL Replaced; int B_Stack; #ifdef CHECK if (!term_IsTerm(Atom) || !term_IsTerm(TermS) || !term_IsTerm(TermT) || term_Equal(Atom, TermS)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ReplaceSubtermBy: Illegal input."); misc_FinishErrorReport(); } #endif /*fputs("\nWe look for: ",stdout);term_Print(TermS); fputs("\nin: ",stdout);term_Print(Atom); */ Replaced = FALSE; TermS = term_Copy(TermS); if (!term_Equal(Atom, TermS) && !list_Empty(term_ArgumentList(Atom))) { B_Stack = stack_Bottom(); stack_Push(term_ArgumentList(Atom)); while (!stack_Empty(B_Stack)) { ArgListNode = stack_Top(); Atom = (TERM)list_Car(ArgListNode); stack_RplacTop(list_Cdr(ArgListNode)); if (term_Equal(Atom, TermS)) { Replaced = TRUE; list_Rplaca(ArgListNode, term_Copy(TermT)); term_Delete(Atom); } else if (term_IsComplex(Atom)) stack_Push(term_ArgumentList(Atom)); while (!stack_Empty(B_Stack) && list_Empty(stack_Top())) stack_Pop(); } } term_Delete(TermS); return Replaced; } void term_ReplaceVariable(TERM Term, SYMBOL Symbol, TERM Repl) /************************************************************** INPUT: A term, a variable symbol and a replacement term. RETURNS: void EFFECT: All variables with in are replaced with copies of CAUTION: Destructive ***************************************************************/ { LIST Scan; #ifdef CHECK if (!term_IsTerm(Term) || !term_IsTerm(Repl) || !symbol_IsVariable(Symbol)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ReplaceVariable: Illegal input."); misc_FinishErrorReport(); } #endif if (symbol_Equal(term_TopSymbol(Term), Symbol)) { term_RplacTop(Term,term_TopSymbol(Repl)); term_RplacArgumentList(Term,term_CopyTermList(term_ArgumentList(Repl))); } else for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) term_ReplaceVariable(list_Car(Scan),Symbol,Repl); } void term_ExchangeVariable(TERM Term, SYMBOL Old, SYMBOL New) /************************************************************** INPUT: A term, and two variable symbols. RETURNS: void EFFECT: All variables in are replaced with CAUTION: Destructive ***************************************************************/ { LIST Scan; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsVariable(Old) || !symbol_IsVariable(New)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ExchangeVariable: Illegal input."); misc_FinishErrorReport(); } #endif if (symbol_Equal(term_TopSymbol(Term), Old)) term_RplacTop(Term,New); else for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) term_ExchangeVariable(list_Car(Scan),Old,New); } BOOL term_SubstituteVariable(SYMBOL Symbol, TERM Repl, TERM* Term) /****************************************************** INPUT: A Symbol which has to be found in the Term, a term which is the replacement for the 'Symbol', and a term in which the substitu- tions take place. RETURNS: A boolean value which is TRUE, if any sub- stitutions were made. SUMMARY: term_Substitute works recursively and repl. every occurence of 'Symbol' in 'Term' by 'Repl'. CAUTION: FUNCTION IS DESTRUCTIVE ON 'Term'. REPLACE- MENT IS COPIED EACH TIME A SUB. TAKES PLACE *******************************************************/ { #ifdef CHECK if (!term_IsTerm(*Term) || !term_IsTerm(Repl) || !symbol_IsSymbol(Symbol)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_SubstituteVariable: Illegal input."); misc_FinishErrorReport(); } #endif if (symbol_Equal(term_TopSymbol(*Term), Symbol)) { TERM New; New = term_Copy(Repl); (*Term)->symbol = Repl->symbol; (*Term)->args = term_ArgumentList(New); /* Free Top-Node of New, as the symbol has been written */ /* into the node pointed to by `Term'. */ memory_Free(New, sizeof(TERM_NODE)); return TRUE; } else { BOOL Result; LIST List; Result = FALSE; for (List = term_ArgumentList(*Term); list_Exist(List); List = list_Cdr(List)) if (term_SubstituteVariable(Symbol, Repl, (TERM*) &(List->car))) Result = TRUE; return Result; } } static int term_CompareByConstants(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: The terms are compared by their multisets of constants. The frequency of elements in the multisets is a multiset itself. The frequencies are sorted and the resulting sorted multisets compared. ***************************************************************/ { LIST lconsts, rconsts; int result; /* Get multiset of constants. */ lconsts = term_ListOfConstants(Left); rconsts = term_ListOfConstants(Right); result = list_CompareMultisetsByElementDistribution(lconsts, rconsts); list_Delete(lconsts); list_Delete(rconsts); return result; } static int term_CompareByFunctions(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: The terms are compared by their multisets of functions. The frequency of elements in the multisets is a multiset itself. The frequencies are sorted and the resulting sorted multisets compared. ***************************************************************/ { LIST lfuns, rfuns; int result; /* Get multiset of functions. */ lfuns = term_ListOfFunctions(Left); rfuns = term_ListOfFunctions(Right); result = list_CompareMultisetsByElementDistribution(lfuns, rfuns); list_Delete(lfuns); list_Delete(rfuns); return result; } static int term_CompareByVariables(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: The terms are compared by their multisets of variables. The frequency of elements in the multisets is a multiset itself. The frequencies are sorted and the resulting sorted multisets compared. ***************************************************************/ { LIST lvars, rvars; int result; /* Get multiset of variables. */ lvars = term_ListOfVariables(Left); rvars = term_ListOfVariables(Right); result = list_CompareMultisetsByElementDistribution(lvars, rvars); list_Delete(lvars); list_Delete(rvars); return result; } LIST term_ListOfConstants(TERM Term) /************************************************************** INPUT: A term. RETURNS: A list of constants. EFFECT: Creates a list of constants used in a term. If no constants are used in a term, it returns an empty list. ***************************************************************/ { #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ListOfConstants: Illegal input."); misc_FinishErrorReport(); } #endif if (symbol_IsConstant(term_TopSymbol(Term))) return list_List((POINTER) term_TopSymbol(Term)); else { LIST result; LIST scan; result = list_Nil(); for (scan = term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) { /* Append to the smaller list for efficiency. A subterm's list of constants will usually be smaller than the intermediate result. */ result = list_Nconc(term_ListOfConstants((TERM) list_Car(scan)), result); } return result; } } LIST term_ListOfFunctions(TERM Term) /************************************************************** INPUT: A term. RETURNS: A list of functions. EFFECT: Creates a list of functions used in a term. If no functions are used in a term, it returns an empty list. ***************************************************************/ { LIST result; LIST scan; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ListOfFunctions: Illegal input."); misc_FinishErrorReport(); } #endif result = list_Nil(); /* If the term starts with a function, add the function symbol to the result. */ if (symbol_IsFunction(term_TopSymbol(Term))) { result = list_Nconc(result, list_List((POINTER) term_TopSymbol(Term))); } /* A function can utilize other functions, so traverse the argument list for further functions. */ for (scan = term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) { /* Append to the smaller list for efficiency. A subterm's list of functions will usually be smaller than the intermediate result. */ result = list_Nconc(term_ListOfFunctions((TERM) list_Car(scan)), result); } return result; } void term_CountSymbols(TERM Term) /************************************************************** INPUT: A term. RETURNS: None. EFFECT: Counts the non-variable symbols in the term, and increases their counts accordingly. ***************************************************************/ { LIST scan; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_CountSymbols: Illegal input."); misc_FinishErrorReport(); } #endif /* If the term starts with a function, increase the count for the function symbol. */ if (symbol_IsFunction(term_TopSymbol(Term))) { SYMBOL S; S = term_TopSymbol(Term); symbol_SetCount(S, symbol_GetCount(S) + 1); } /* A function can utilize other functions, so traverse the argument list for further function symbols. */ for (scan = term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) { term_CountSymbols((TERM) list_Car(scan)); } } static int term_CompareByArity(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: Terms are compared top down, left to right with respect to the arity of their signature symbols, where variables in addition are defined to be smaller than constants. ***************************************************************/ { NAT lval, rval; SYMBOL lsymb, rsymb; LIST largs, rargs; int result; result = 0; /* Compare top symbols first */ lsymb = term_TopSymbol(Left); rsymb = term_TopSymbol(Right); if (symbol_IsVariable(lsymb)) { if (symbol_IsVariable(rsymb)) return 0; else return 1; } else if (symbol_IsVariable(rsymb)) return -1; lval = symbol_Arity(lsymb); rval = symbol_Arity(rsymb); if (lval > rval) return -1; if (lval < rval) return 1; /* If top symbol arities are equal, compare subterms left to right */ largs = term_ArgumentList(Left); rargs = term_ArgumentList(Right); while(!list_Empty(largs)) { result = term_CompareByArity(list_Car(largs), list_Car(rargs)); if (result != 0) break; largs = list_Cdr(largs); rargs = list_Cdr(rargs); } return result; } int term_CompareBySymbolOccurences(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: Terms are compared top down, left to right with respect to the frequency of their symbols. ***************************************************************/ { unsigned long lval, rval; SYMBOL lsymb, rsymb; LIST largs, rargs; int result; result = 0; /* Compare top symbols first */ lsymb = term_TopSymbol(Left); rsymb = term_TopSymbol(Right); if (symbol_IsFunction(lsymb)) { if (symbol_IsFunction(rsymb)) { lval = symbol_GetCount(lsymb); rval = symbol_GetCount(rsymb); if (lval > rval) return -1; if (lval < rval) return 1; /* If top symbol arities are equal, compare subterms left to right */ largs = term_ArgumentList(Left); rargs = term_ArgumentList(Right); while(!list_Empty(largs)) { result = term_CompareBySymbolOccurences(list_Car(largs), list_Car(rargs)); if (result != 0) break; largs = list_Cdr(largs); rargs = list_Cdr(rargs); } } else { return -1; } } else { if (symbol_IsFunction(rsymb)) { return 1; } } return result; } int term_CompareAbstract(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: 1 if left term < right term 0 if left term = right term -1 if left term > right term EFFECT: Compares two terms using an internal array of term comparison functions. As soon as a term is found to compare greater than the other, the result of the comparison is returned. If all term comparison functions yield an "equal", then 0 is returned. ***************************************************************/ { int result; int i; int functions; typedef int (*TERM_COMPARE_FUNCTION) (TERM, TERM); static const TERM_COMPARE_FUNCTION term_compare_functions [] = { term_CompareByArity, term_CompareBySymbolOccurences, term_CompareByConstants, term_CompareByVariables, term_CompareByFunctions }; #ifdef CHECK if (!(term_IsTerm(Left) && term_IsTerm(Right))) { misc_StartErrorReport(); misc_ErrorReport("\n In term_CompareAbstract: Illegal input."); misc_FinishErrorReport(); } #endif result = 0; functions = sizeof(term_compare_functions)/sizeof(TERM_COMPARE_FUNCTION); for (i = 0; i < functions; i++) { result = term_compare_functions[i](Left, Right); if ( result != 0) { return result; } } return result; } BOOL term_CompareAbstractLEQ(TERM Left, TERM Right) /************************************************************** INPUT: Two terms. RETURNS: TRUE if left term <= right term, FALSE otherwise. EFFECT: Terms are compared top down, left to right with respect to the arity of their signature symbols, where variables in addition are defined to be smaller than constants. ***************************************************************/ { return (term_CompareAbstract(Left, Right) >= 0); } NAT term_ComputeSize(TERM Term) /************************************************************** INPUT: A term. RETURNS: The number of symbols in the term. EFFECT: None ***************************************************************/ { NAT Weight; LIST Scan; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ComputeSize: Illegal input."); misc_FinishErrorReport(); } #endif Weight = 1; for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) Weight += term_ComputeSize((TERM)list_Car(Scan)); return Weight; } NAT term_RootDistance(TERM Term) /************************************************************** INPUT: A term with establised father links. RETURNS: The distance from to its root father term. EFFECT: None ***************************************************************/ { NAT Distance; Distance = 0; while (term_Superterm(Term) != (TERM)NULL) { Distance++; Term = term_Superterm(Term); } return Distance; } BOOL term_RootDistanceSmaller(TERM Term1, TERM Term2) /************************************************************** INPUT: Two terms with establised father links. RETURNS: TRUE iff root distance of is smaller than root distance of EFFECT: None ***************************************************************/ { return (term_RootDistance(Term1) Depth) Depth = Help; } return (Depth+1); } BOOL term_ContainsSymbol(TERM Term, SYMBOL Symbol) /************************************************************** INPUT: A term and a symbol. RETURNS: TRUE, if the symbol occurs somewhere in the term, FALSE otherwise. ***************************************************************/ { int Stack; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ContainsSymbol: Illegal input."); misc_FinishErrorReport(); } #endif Stack = stack_Bottom(); do { if (term_TopSymbol(Term) == Symbol) { stack_SetBottom(Stack); /* Clean up the stack */ return TRUE; } else if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); return FALSE; } TERM term_FindSubterm(TERM Term, SYMBOL Symbol) /************************************************************** INPUT: A term and a symbol. RETURNS: If the symbol occurs in the Term the subterm is returned. NULL otherwise. ***************************************************************/ { int stack; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_FindSubterm: Illegal input."); misc_FinishErrorReport(); } #endif stack = stack_Bottom(); do { if (term_TopSymbol(Term) == Symbol) { stack_SetBottom(stack); /* Clean up the stack */ return Term; } else if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); while (!stack_Empty(stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(stack)) { Term = list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(stack)); return NULL; } static int term_SharingList(TERM Term, LIST List) /************************************************************** INPUT: A term and a list cell. RETURNS: The number of times occurs in EFFECT: None ***************************************************************/ { LIST Scan; int n; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_SharingList: Illegal input."); misc_FinishErrorReport(); } #endif n = 0; for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) { if (Scan == List) n++; n += term_SharingList(list_Car(Scan), List); } return n; } static int term_SharingTerm(TERM Term, TERM CompareTerm) /************************************************************** INPUT: A term and a compare term RETURNS: The number of occurrences of in EFFECT: None ***************************************************************/ { LIST Scan; int n; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_SharingTerm: Illegal input."); misc_FinishErrorReport(); } #endif n = 0; if (Term == CompareTerm) n = 1; for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) n += term_SharingTerm(list_Car(Scan),CompareTerm); return n; } BOOL term_Sharing(TERM Term) /************************************************************** INPUT: A term. RETURNS: TRUE iff the term shares list cells or subterms. EFFECT: None ***************************************************************/ { LIST Scan; int stack; TERM ActTerm; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_Sharing: Illegal input."); misc_FinishErrorReport(); } #endif stack = stack_Bottom(); stack_Push(Term); while (!stack_Empty(stack)) { ActTerm = (TERM)stack_Top(); stack_Pop(); if (term_SharingTerm(Term,ActTerm)>1) return TRUE; if (term_IsComplex(Term)) { for (Scan = term_ArgumentList(ActTerm); !list_Empty(Scan); Scan=list_Cdr(Scan)) if (term_SharingList(Term, Scan) > 1) return TRUE; else stack_Push(list_Car(Scan)); } } return FALSE; } void term_AddFatherLinks(TERM Term) /************************************************************** INPUT: A term. RETURNS: void. EFFECT: The super term links of Term are cleared and then all its subterms are set. ***************************************************************/ { LIST Scan; TERM ActTerm; term_RplacSuperterm(Term,(TERM)NULL); for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { ActTerm = (TERM)list_Car(Scan); term_AddFatherLinks(ActTerm); term_RplacSuperterm(ActTerm,Term); } } BOOL term_FatherLinksEstablished(TERM Term) /************************************************************** INPUT: A term. RETURNS: TRUE iff all father links in Term are established. EFFECT: None. ***************************************************************/ { LIST Scan; for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) if (Term != term_Superterm(list_Car(Scan)) || !term_FatherLinksEstablished(list_Car(Scan))) return FALSE; return TRUE; } TERM term_TopLevelTerm(TERM Term) /************************************************************** INPUT: A term. RETURNS: The top level father of the term. EFFECT: The father links have to be established! ***************************************************************/ { while (term_Superterm(Term)) Term = term_Superterm(Term); return Term; } BOOL term_HasPointerSubterm(TERM Term, TERM Subterm) /************************************************************** INPUT: Two terms. RETURNS: TRUE, if has as a subterm. CAUTION: Only term pointers are compared, term_Equal isn't used. ***************************************************************/ { if (Term == Subterm) return TRUE; else { LIST scan = term_ArgumentList(Term); while (!list_Empty(scan)) { if (term_HasPointerSubterm((TERM) list_Car(scan), Subterm)) return TRUE; scan = list_Cdr(scan); } } return FALSE; } BOOL term_HasSubterm(TERM Term, TERM Subterm) /************************************************************** INPUT: Two terms. RETURNS: TRUE, if has as a subterm. CAUTION: term_Equal is used. ***************************************************************/ { if (term_Equal(Term,Subterm)) return TRUE; else { LIST Scan; Scan = term_ArgumentList(Term); while (!list_Empty(Scan)) { if (term_HasSubterm((TERM) list_Car(Scan), Subterm)) return TRUE; Scan = list_Cdr(Scan); } } return FALSE; } BOOL term_HasProperSuperterm(TERM Term, TERM Super) /********************************************************** INPUT : Two terms. RETURNS : TRUE iff Super can be reached from Term by following the superterm member of the TERM structure. CAUTION : not reflexive **********************************************************/ { if (Term == Super) return FALSE; while (Term != (TERM) NULL) { if (Term == Super) /* Pointer equality ! */ return TRUE; else Term = term_Superterm(Term); } return FALSE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * TERM OUTPUT FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void term_Print(TERM Term) /************************************************************** INPUT: A term. RETURNS: none. SUMMARY: Prints the term to stdout. CAUTION: Uses the other term output functions. ***************************************************************/ { if (term_IsComplex(Term)) { putchar('('); symbol_Print(term_TopSymbol(Term)); putchar(' '); term_TermListPrint(term_ArgumentList(Term)); putchar(')'); } else if (term_IsVariable(Term)) { symbol_Print(term_TopSymbol(Term)); } else { /* term_IsConstant(Term) */ putchar('('); symbol_Print(term_TopSymbol(Term)); putchar(')'); } } static void term_PrettyPrintIntern(TERM Term, int Depth) /************************************************************** INPUT: A term and a depth parameter for indentation. RETURNS: none. SUMMARY: Prints the term hopefully more pretty to stdout. ***************************************************************/ { int i; LIST scan; for (i=0; i < Depth; i++) fputs(" ", stdout); if (symbol_IsJunctor(term_TopSymbol(Term))) { if (term_IsComplex(Term)) { symbol_Print(term_TopSymbol(Term)); putchar('('); fputs("\n", stdout); for (scan=term_ArgumentList(Term); !list_Empty(scan); scan= list_Cdr(scan)) { term_PrettyPrintIntern((TERM) list_Car(scan), Depth+1); if (!list_Empty(list_Cdr(scan))) fputs(",\n", stdout); } putchar(')'); } else { if (term_IsVariable(Term)) { symbol_Print(term_TopSymbol(Term)); } else { putchar('('); symbol_Print(term_TopSymbol(Term)); putchar(')'); } } } else { term_PrintPrefix(Term); } } void term_PrettyPrint(TERM Term) /************************************************************** INPUT: A term. RETURNS: none. SUMMARY: Prints the term hopefully more pretty to stdout. ***************************************************************/ { term_PrettyPrintIntern(Term, 0); } void term_FPrint(FILE* File,TERM Term) /************************************************************** INPUT: A file and a term. RETURNS: none. SUMMARY: Prints the term to the file. CAUTION: Uses the other term output functions. ***************************************************************/ { if (term_IsComplex(Term)) { putc('(', File); symbol_FPrint(File,term_TopSymbol(Term)); putc(' ', File); term_TermListFPrint(File,term_ArgumentList(Term)); putc(')', File); } else if (term_IsVariable(Term)) { symbol_FPrint(File,term_TopSymbol(Term)); } else { /* term_IsConstant(Term) */ putc('(', File); symbol_FPrint(File,term_TopSymbol(Term)); putc(')', File); } } void term_TermListPrint(LIST List) /************************************************************** INPUT: A list of terms. RETURNS: None. ***************************************************************/ { for (; !list_Empty(List); List=list_Cdr(List)) { term_Print(list_Car(List)); fflush(stdout); if (!list_Empty(list_Cdr(List))) putchar(' '); } } void term_TermListFPrint(FILE* File, LIST List) /************************************************************** INPUT: A list of terms. RETURNS: None. ***************************************************************/ { for (; !list_Empty(List); List=list_Cdr(List)) { term_FPrint(File,list_Car(List)); if (!list_Empty(list_Cdr(List))) putc(' ', File); } } void term_PrintPrefix(TERM Term) /************************************************************** INPUT: A term. RETURNS: none. SUMMARY: Prints the term in prefix notation to stdout. CAUTION: Uses the other term output functions. ***************************************************************/ { if (term_IsComplex(Term)) { symbol_Print(term_TopSymbol(Term)); putchar('('); term_TermListPrintPrefix(term_ArgumentList(Term)); putchar(')'); } else symbol_Print(term_TopSymbol(Term)); } void term_FPrintPrefix(FILE* File, TERM Term) /************************************************************** INPUT: A file and a term. RETURNS: none. SUMMARY: Prints the term in prefix notation to the file. CAUTION: Uses the other term output functions. ***************************************************************/ { if (term_IsComplex(Term)) { symbol_FPrint(File,term_TopSymbol(Term)); putc('(', File); term_TermListFPrintPrefix(File,term_ArgumentList(Term)); putc(')', File); } else symbol_FPrint(File,term_TopSymbol(Term)); } void term_TermListPrintPrefix(LIST List) /************************************************************** INPUT: A list of terms. RETURNS: None. ***************************************************************/ { for (; !list_Empty(List); List=list_Cdr(List)) { term_PrintPrefix(list_Car(List)); if (!list_Empty(list_Cdr(List))) putchar(','); } } void term_TermListFPrintPrefix(FILE* File, LIST List) /************************************************************** INPUT: A list of terms. RETURNS: None. ***************************************************************/ { for (; !list_Empty(List); List=list_Cdr(List)) { term_FPrintPrefix(File,list_Car(List)); if (!list_Empty(list_Cdr(List))) putc(',', File); } } void term_FPrintOtterPrefix(FILE* File, TERM Term) /************************************************************** INPUT: A file and a term. RETURNS: none. SUMMARY: Prints the term in prefix notation to the file. CAUTION: Uses the other term_Output functions. ***************************************************************/ { if (term_IsComplex(Term)) { symbol_FPrintOtter(File, term_TopSymbol(Term)); putc('(', File); term_TermListFPrintOtterPrefix(File, term_ArgumentList(Term)); putc(')', File); } else symbol_FPrintOtter(File, term_TopSymbol(Term)); } void term_TermListFPrintOtterPrefix(FILE* File, LIST List) /************************************************************** INPUT: A list of terms. RETURNS: None. ***************************************************************/ { for (; !list_Empty(List); List=list_Cdr(List)) { term_FPrintOtterPrefix(File,list_Car(List)); if (!list_Empty(list_Cdr(List))) putc(',', File); } } void term_FPrintPosition(FILE* File, TERM TopTerm, TERM Subterm) /************************************************************** INPUT: An output file and two terms where is a subterm of . RETURNS: Nothing. SUMMARY: The position of relative to is printed to the output file. A simple top-down search is done, so the superterm pointers are not needed. Note that we compare terms with respect to pointers! If isn't a subterm of at all, this causes an error message followed by a core dump. ***************************************************************/ { NAT pos; LIST Scan; if (TopTerm == Subterm) return; for (Scan = term_ArgumentList(TopTerm), pos = 1; !list_Empty(Scan); Scan = list_Cdr(Scan), pos++) { if (term_HasPointerSubterm(list_Car(Scan), Subterm)) { fprintf(File, "%u", pos); if (Subterm != list_Car(Scan)) { putc('.', File); term_FPrintPosition(File, list_Car(Scan), Subterm); } return; } } misc_StartErrorReport(); misc_ErrorReport("\n In term_FPrintPosition: Term isn't subterm of the other one."); misc_FinishErrorReport(); } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * HIGH LEVEL FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ NAT term_Bytes(TERM Term) /************************************************************** INPUT: A term. RETURNS: The number of bytes occupied by the term. EFFECT: None ***************************************************************/ { NAT Bytes; LIST Scan; Bytes = sizeof(TERM_NODE) + list_Bytes(term_ArgumentList(Term)); for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) Bytes += term_Bytes((TERM)list_Car(Scan)); return Bytes; } LIST term_ListOfVariables(TERM Term) /************************************************************** INPUT: A term. RETURNS: The list of variables occurring in the term. Note that there may be many terms with same variable symbol. ***************************************************************/ { LIST Stack, Variables; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ListOfVariables: Illegal input."); misc_FinishErrorReport(); } #endif Variables = list_Nil(); Stack = list_StackBottom(); do { if (term_IsComplex(Term)) Stack = list_Push(term_ArgumentList(Term),Stack); else if (term_IsVariable(Term)) Variables = list_Cons(Term, Variables); while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) Stack = list_Pop(Stack); if (!list_StackEmpty(Stack)) { Term = (TERM)list_Car(list_Top(Stack)); list_RplacTop(Stack, list_Cdr(list_Top(Stack))); } } while (!list_StackEmpty(Stack)); return Variables; } void term_MarkVariables(TERM Term, NAT Mark) /************************************************************** INPUT: A term. RETURNS: Nothing. EFFECT: All variables from are marked with . CAUTION: The term module must be in a binding phase (started with term_StartBinding)! ***************************************************************/ { int Stack; #ifdef CHECK if (!term_InBindingPhase()) { misc_StartErrorReport(); misc_ErrorReport("\n In term_MarkVariables:"); misc_ErrorReport(" Called while not in binding phase."); misc_FinishErrorReport(); } #endif Stack = stack_Bottom(); do { if (term_IsComplex(Term)) { stack_Push(term_ArgumentList(Term)); } else if (term_IsVariable(Term)) term_CreateBinding(term_TopSymbol(Term), Mark); while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); } LIST term_VariableSymbols(TERM Term) /************************************************************** INPUT: A term. RETURNS: The list of variable symbols occurring in the term. ***************************************************************/ { LIST Variables; int Stack; SYMBOL Top; NAT ActMark; #ifdef CHECK if (!term_IsTerm(Term) || term_InBindingPhase()) { misc_StartErrorReport(); misc_ErrorReport("\n In term_VariableSymbols: Illegal input or context."); misc_FinishErrorReport(); } #endif term_StartBinding(); Variables = list_Nil(); Stack = stack_Bottom(); ActMark = term_ActMark(); do { if (term_IsComplex(Term)) { stack_Push(term_ArgumentList(Term)); } else { Top = term_TopSymbol(Term); if (symbol_IsVariable(Top) && !term_VarIsMarked(Top, ActMark)) { Variables = list_Cons((POINTER)Top, Variables); term_CreateBinding(Top, ActMark); } } while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); term_StopBinding(); return Variables; } NAT term_NumberOfVarOccs(TERM Term) /************************************************************** INPUT: A term. RETURNS: The list of variable symbols occurring in the term. ***************************************************************/ { NAT Result; int Stack; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_NumberOfVarOccs: Illegal input."); misc_FinishErrorReport(); } #endif Result = 0; Stack = stack_Bottom(); do { if (term_IsComplex(Term)) { stack_Push(term_ArgumentList(Term)); } else { if (symbol_IsVariable(term_TopSymbol(Term))) Result++; } while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); return Result; } NAT term_NumberOfSymbolOccurrences(TERM Term, SYMBOL Symbol) /************************************************************** INPUT: A term and a symbol. RETURNS: The number of occurrences of in ***************************************************************/ { NAT Result; LIST Scan; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_NumberOfSymbolOccurrences: Illegal input."); misc_FinishErrorReport(); } #endif Result = 0; if (symbol_Equal(term_TopSymbol(Term),Symbol)) Result++; for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) Result += term_NumberOfSymbolOccurrences(list_Car(Scan), Symbol); return Result; } BOOL term_ContainsFunctions(TERM Term) /************************************************************** INPUT: A term. RETURNS: TRUE iff the term contains a function symbol ***************************************************************/ { int Stack; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ContainsFunctions: Illegal input."); misc_FinishErrorReport(); } #endif Stack = stack_Bottom(); do { if (term_IsComplex(Term)) { if (symbol_IsFunction(term_TopSymbol(Term)) && !symbol_IsConstant(term_TopSymbol(Term))) { stack_SetBottom(Stack); return TRUE; } stack_Push(term_ArgumentList(Term)); } while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); return FALSE; } BOOL term_ContainsVariable(TERM Term, SYMBOL Var) /************************************************************** INPUT: A term and a variable symbol. RETURNS: TRUE iff the term contains the variable symbol ***************************************************************/ { int Stack; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsSymbol(Var)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_ContainsVariable: Illegal input."); misc_FinishErrorReport(); } #endif Stack = stack_Bottom(); do { if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); else if (symbol_Equal(term_TopSymbol(Term),Var)) { stack_SetBottom(Stack); return TRUE; } while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { Term = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); return FALSE; } SYMBOL term_MaxVar(TERM Term) /********************************************************* INPUT: A term. RETURNS: The maximal variable in , NULL otherwise ********************************************************/ { LIST Scan; int Stack; SYMBOL Result; #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_MaxVar: Illegal input."); misc_FinishErrorReport(); } #endif Result = (SYMBOL)NULL; Stack = stack_Bottom(); if (term_IsStandardVariable(Term)) { if (term_TopSymbol(Term)>Result) Result = term_TopSymbol(Term); } else if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); while (!stack_Empty(Stack)) { Scan = stack_Top(); Term = (TERM)list_Car(Scan); stack_RplacTop(list_Cdr(Scan)); if (term_IsStandardVariable(Term)) { if (term_TopSymbol(Term)>Result) Result = term_TopSymbol(Term); } else if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); } return Result; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * Renaming * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void term_StartMinRenaming(void) /************************************************************** INPUT: None EFFECT: Initializes the term and symbol modules for min co var renaming ***************************************************************/ { symbol_ResetStandardVarCounter(); term_NewMark(); } void term_StartMaxRenaming(SYMBOL MaxVar) /************************************************************** INPUT: A variable symbol. EFFECT: Initializes the term and symbol modules for renaming above ***************************************************************/ { symbol_SetStandardVarCounter(MaxVar); term_NewMark(); } TERM term_Rename(TERM Term) /************************************************************** INPUT: A Term. RETURNS: The destructively renamed term. EFFECT: All co variables are destructively renamed in ***************************************************************/ { int Stack; SYMBOL Top; NAT ActMark; TERM ActTerm; #ifdef CHECK if (!term_IsTerm(Term) || term_InBindingPhase()) { misc_StartErrorReport(); misc_ErrorReport("\n In term_Rename: Illegal input or context."); misc_FinishErrorReport(); } #endif term_StartBinding(); Stack = stack_Bottom(); ActMark = term_OldMark(); ActTerm = Term; do { if (term_IsComplex(ActTerm)) { stack_Push(term_ArgumentList(ActTerm)); } else { Top = term_TopSymbol(ActTerm); if (symbol_IsVariable(Top)) { if (!term_VarIsMarked(Top, ActMark)) term_CreateValueBinding(Top, ActMark, (POINTER)symbol_CreateStandardVariable()); term_RplacTop(ActTerm,(SYMBOL)term_BindingValue(Top)); } } while (!stack_Empty(Stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(Stack)) { ActTerm = (TERM)list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(Stack)); term_StopBinding(); return Term; } SYMBOL term_GetRenamedVarSymbol(SYMBOL Var) /************************************************************** INPUT: A variable symbol. RETURNS: The renamed variable for symbol for with respect to the current renaming. If it does not exist, itself is returned. EFFECT: None. ***************************************************************/ { NAT ActMark; #ifdef CHECK if (!symbol_IsStandardVariable(Var)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_GetRenamedVarSymbol: Illegal input."); misc_FinishErrorReport(); } #endif ActMark = term_OldMark(); if (term_VarIsMarked(Var, ActMark)) return (SYMBOL)term_BindingValue(Var); return Var; } static LIST term_MakePseudoLinear(TERM Term, NAT Depth, NAT Mark) /************************************************************** INPUT: A Term and a variable and the current depth. RETURNS: A list of pairs (,) EFFECT: The term is destructively made pseudo_linear. ***************************************************************/ { LIST Result,Scan; SYMBOL Top; Result = list_Nil(); if (term_IsComplex(Term)) for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) Result = list_Nconc(term_MakePseudoLinear(list_Car(Scan),Depth+1,Mark), Result); else { Top = term_TopSymbol(Term); if (symbol_IsVariable(Top)) { if (term_VarIsMarked(Top, Mark)) { if (Depth != (NAT)term_BindingValue(Top)) term_RplacTop(Term,symbol_CreateStandardVariable()); Result = list_Cons(list_PairCreate((POINTER)Top, (POINTER)term_TopSymbol(Term)), Result); } else { term_CreateValueBinding(Top, Mark, (POINTER)Depth); } } } return Result; } LIST term_RenamePseudoLinear(TERM Term, SYMBOL Var) /************************************************************** INPUT: A Term and a variable. RETURNS: A list of pairs (,) EFFECT: The term is destructively renamed. ***************************************************************/ { NAT Mark; LIST Result; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsVariable(Var) || term_InBindingPhase()) { misc_StartErrorReport(); misc_ErrorReport("\n In term_RenamePseudoLinear: Illegal input or context."); misc_FinishErrorReport(); } #endif term_StartBinding(); symbol_SetStandardVarCounter(Var); term_NewMark(); Mark = term_ActMark(); Result = term_MakePseudoLinear(Term,0,Mark); term_StopBinding(); return Result; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * STAMP FUNCTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ NAT term_GetStampID(void) /************************************************************** INPUT: None RETURNS: An identifier that must be used for some stamp functions EFFECT: Each module using the term stamp has to request an identifier that is needed for function term_StampOverflow The purpose of this identifier is to synchronize different modules in case of an overflow of the variable term_STAMP. ***************************************************************/ { if (term_STAMPUSERS >= term_MAXSTAMPUSERS) { misc_StartUserErrorReport(); misc_UserErrorReport("\n In term_GetStampID: no more free stamp IDs."); misc_UserErrorReport("\n You have to increase the constant term_MAXSTAMPUSERS."); misc_FinishUserErrorReport(); } return term_STAMPUSERS++; } BOOL term_StampOverflow(NAT ID) /************************************************************** INPUT: The identifier of the calling module as returned by the function term_GetStampID. RETURNS: True if an overflow of the variable term_STAMP occurred for the module with the identifier ID. CAUTION: If an overflow occurred for a module you can test that only once!!! After the first test the overflow flag is cleared for that module. ***************************************************************/ { BOOL Result = FALSE; NAT i; #ifdef CHECK if (ID >= term_MAXSTAMPUSERS) { misc_StartErrorReport(); misc_ErrorReport("\n In term_StampOverflow: Illegal input."); misc_FinishErrorReport(); } #endif if (term_STAMP == NAT_MAX) { term_STAMP = 0; /* set overflow flag for all other modules */ for (i = 0; i < term_MAXSTAMPUSERS; i++) term_STAMPOVERFLOW[i] = TRUE; term_STAMPOVERFLOW[ID] = FALSE; Result = TRUE; } else if (term_STAMPOVERFLOW[ID]) { term_STAMPOVERFLOW[ID] = FALSE; Result = TRUE; } return Result; } void term_SetTermSubtermStamp(TERM Term) /************************************************************** INPUT: A term. RETURNS: void. EFFECT: Sets the current stamp to and its subterms. ***************************************************************/ { #ifdef CHECK if (!term_IsTerm(Term)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_SetTermSubtermStamp: Illegal input."); misc_FinishErrorReport(); } #endif term_SetTermStamp(Term); list_Apply((void (*)(POINTER)) term_SetTermSubtermStamp, term_ArgumentList(Term)); } LIST term_ListOfAtoms(TERM Term, SYMBOL Predicate) /************************************************************** INPUT: A term and a predicate symbol. RETURNS: A list of pointers to all atoms in Term with predicate symbol . ***************************************************************/ { if (symbol_Equal(term_TopSymbol(Term), Predicate)) return list_List(Term); else { LIST Result, List; Result = list_Nil(); for (List = term_ArgumentList(Term); !list_Empty(List); List = list_Cdr(List)) Result = list_Nconc(Result, term_ListOfAtoms(list_Car(List), Predicate)); return Result; } } /* Currently only in CHECK mode */ #ifdef CHECK void term_StartStamp(void) /************************************************************** INPUT: None RETURNS: Nothing EFFECT: The stamp is prepared for a new term traversal. ***************************************************************/ { if (term_STAMPBLOCKED) { /* Error: the Stamp is already used */ misc_StartErrorReport(); misc_ErrorReport("\n In term_StartStamp: Illegal context, term stamp is already used."); misc_FinishErrorReport(); } else { term_STAMP++; term_STAMPBLOCKED = TRUE; } } #endif LIST term_FindAllAtoms(TERM Term, SYMBOL Predicate) /********************************************************************** INPUT: A term Term and a symbol Predicate. RETURN: A list of all atoms of Term with Symbol as top symbol. ***********************************************************************/ { int stack; LIST Result; #ifdef CHECK if (!term_IsTerm(Term) || !symbol_IsPredicate(Predicate)) { misc_StartErrorReport(); misc_ErrorReport("\n In term_FindAllPredicates: Illegal input."); misc_FinishErrorReport(); } #endif stack = stack_Bottom(); Result = list_Nil(); do { if (term_TopSymbol(Term) == Predicate) { Result = list_Cons(Term, Result); } else if (term_IsComplex(Term)) stack_Push(term_ArgumentList(Term)); while (!stack_Empty(stack) && list_Empty(stack_Top())) stack_Pop(); if (!stack_Empty(stack)) { Term = list_Car(stack_Top()); stack_RplacTop(list_Cdr(stack_Top())); } } while (!stack_Empty(stack)); return Result; } BOOL term_CheckTermIntern(TERM Term, BOOL Links) /************************************************************************** INPUT: A term and a boolean. RETURN: True iff 1) the arity of each top symbol is equal to the number of arguments of symbol's term. and 2) either all father links are set correctly iff Links is TRUE or none is set iff Links is FALSE. COMMENT: Intern function of term_CheckTerm. ***************************************************************************/ { LIST Scan; SYMBOL Top; if (!term_IsTerm(Term)) return FALSE; Top = term_TopSymbol(Term); if (symbol_IsSignature(Top) && symbol_Arity(Top) != -1 && symbol_Arity(Top) != (int)list_Length(term_ArgumentList(Term))) return FALSE; if (symbol_IsVariable(Top) && !list_Empty(term_ArgumentList(Term))) return FALSE; if (Links) { for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { if (term_Superterm(list_Car(Scan)) != Term || !term_CheckTermIntern(list_Car(Scan), Links)) return FALSE; } } else { for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { if (term_Superterm(list_Car(Scan)) != term_Null() || !term_CheckTermIntern(list_Car(Scan), Links)) return FALSE; } } return TRUE; } BOOL term_CheckTerm(TERM Term) /******************************************************************************** INPUT : A term Term. RETURN: TRUE iff eihter all or no father links are set AND the length of any argument list matches the arity of the respective symbol *********************************************************************************/ { if (term_IsComplex(Term) && term_Superterm(term_FirstArgument(Term)) != term_Null()) /* check father links as well */ return term_CheckTermIntern(Term, TRUE); else return term_CheckTermIntern(Term, FALSE); }