| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * CONTEXTS FOR VARIABLES * */ |
| /* * * */ |
| /* * $Module: CONTEXT * */ |
| /* * * */ |
| /* * Copyright (C) 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$ */ |
| |
| |
| #define SHOWBINDINGS 0 |
| |
| #ifndef _CONTEXT_ |
| #define _CONTEXT_ |
| |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "term.h" |
| #include "symbol.h" |
| #include "list.h" |
| |
| /**************************************************************/ |
| /* Structures */ |
| /**************************************************************/ |
| |
| /* Set 'SHOWBINDINGS' to non-zero value to enable debug output. */ |
| /* #define SHOWBINDINGS 1 */ |
| |
| #define cont__SIZE symbol__MAXVARIABLES |
| |
| extern int cont_NOOFCONTEXTS; |
| extern LIST cont_LISTOFCONTEXTS; |
| extern int cont_BINDINGS; |
| |
| /* An array to remember bindings for the variables. The array */ |
| /* is indexed by the variable index and holds the binding term. */ |
| |
| typedef struct binding { |
| SYMBOL symbol; |
| SYMBOL renaming; |
| TERM term; |
| struct binding *context; |
| struct binding *link; |
| } *CONTEXT, CONTEXT_NODE; |
| |
| extern CONTEXT cont_LASTBINDING; /* The last binding made. */ |
| extern CONTEXT cont_CURRENTBINDING; /* Help variable. */ |
| |
| extern SYMBOL cont_INDEXVARSCANNER; |
| |
| /* Two contexts are allocated by default */ |
| |
| extern CONTEXT cont_LEFTCONTEXT; |
| extern CONTEXT cont_RIGHTCONTEXT; |
| extern CONTEXT cont_INSTANCECONTEXT; /* This context is used as a label only (dummy context) */ |
| |
| |
| static __inline__ CONTEXT cont_LeftContext(void) |
| { |
| return cont_LEFTCONTEXT; |
| } |
| |
| static __inline__ CONTEXT cont_RightContext(void) |
| { |
| return cont_RIGHTCONTEXT; |
| } |
| |
| static __inline__ CONTEXT cont_InstanceContext(void) |
| { |
| return cont_INSTANCECONTEXT; |
| } |
| |
| /**************************************************************/ |
| /* A stack for the number of established bindings */ |
| /**************************************************************/ |
| |
| #define cont__STACKSIZE 1000 |
| |
| typedef int cont_STACK_TYPE[cont__STACKSIZE]; |
| |
| extern cont_STACK_TYPE cont_STACK; |
| extern int cont_STACKPOINTER; |
| |
| /* Stack operations */ |
| |
| static __inline__ void cont_StackInit(void) |
| { |
| cont_STACKPOINTER = 1; |
| } |
| |
| static __inline__ void cont_StackPush(int Entry) |
| { |
| #ifdef CHECK |
| if (cont_STACKPOINTER >= cont__STACKSIZE) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_StackPush: Context stack overflow!\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_STACK[cont_STACKPOINTER++] = Entry; |
| } |
| |
| static __inline__ void cont_StackPop(void) |
| { |
| --cont_STACKPOINTER; |
| } |
| |
| static __inline__ int cont_StackPopResult(void) |
| { |
| return cont_STACK[--cont_STACKPOINTER]; |
| } |
| |
| static __inline__ void cont_StackNPop(int N) |
| { |
| cont_STACKPOINTER -= N; |
| } |
| |
| static __inline__ int cont_StackTop(void) |
| { |
| return cont_STACK[cont_STACKPOINTER - 1]; |
| } |
| |
| static __inline__ int cont_StackNthTop(int N) |
| { |
| return cont_STACK[cont_STACKPOINTER - (1 + N)]; |
| } |
| |
| static __inline__ void cont_StackRplacTop(int Entry) |
| { |
| cont_STACK[cont_STACKPOINTER - 1] = Entry; |
| } |
| |
| static __inline__ void cont_StackRplacNthTop(int N, int Entry) |
| { |
| cont_STACK[cont_STACKPOINTER - (1 + N)] = Entry; |
| } |
| |
| static __inline__ void cont_StackRplacNth(int N, int Entry) |
| { |
| cont_STACK[N] = Entry; |
| } |
| |
| static __inline__ int cont_StackBottom(void) |
| { |
| return cont_STACKPOINTER; |
| } |
| |
| static __inline__ void cont_StackSetBottom(int Pointer) |
| { |
| cont_STACKPOINTER = Pointer; |
| } |
| |
| static __inline__ BOOL cont_StackEmpty(int Pointer) |
| { |
| return cont_STACKPOINTER == Pointer; |
| } |
| |
| |
| static __inline__ void cont_StartBinding(void) |
| { |
| cont_StackPush(cont_BINDINGS); |
| |
| cont_BINDINGS = 0; |
| } |
| |
| static __inline__ int cont_BindingsSinceLastStart(void) |
| { |
| return cont_BINDINGS; |
| } |
| |
| static __inline__ void cont_StopAndStartBinding(void) |
| { |
| cont_StackRplacTop(cont_StackTop() + cont_BINDINGS); |
| |
| cont_BINDINGS = 0; |
| } |
| |
| /**************************************************************/ |
| /* Access */ |
| /**************************************************************/ |
| |
| static __inline__ CONTEXT cont_Binding(CONTEXT C, SYMBOL Var) |
| { |
| return &(C)[Var]; |
| } |
| |
| static __inline__ CONTEXT cont_BindingLink(CONTEXT B) |
| { |
| return B->link; |
| } |
| |
| static __inline__ void cont_SetBindingLink(CONTEXT B, CONTEXT L) |
| { |
| B->link = L; |
| } |
| |
| static __inline__ TERM cont_BindingTerm(CONTEXT B) |
| { |
| return B->term; |
| } |
| |
| static __inline__ void cont_SetBindingTerm(CONTEXT B, TERM T) |
| { |
| B->term = T; |
| } |
| |
| static __inline__ SYMBOL cont_BindingSymbol(CONTEXT B) |
| { |
| return B->symbol; |
| } |
| |
| static __inline__ void cont_SetBindingSymbol(CONTEXT B, SYMBOL S) |
| { |
| B->symbol = S; |
| } |
| |
| static __inline__ SYMBOL cont_BindingRenaming(CONTEXT B) |
| { |
| return B->renaming; |
| } |
| |
| static __inline__ void cont_SetBindingRenaming(CONTEXT B, SYMBOL S) |
| { |
| B->renaming = S; |
| } |
| |
| static __inline__ CONTEXT cont_BindingContext(CONTEXT B) |
| { |
| return B->context; |
| } |
| |
| static __inline__ void cont_SetBindingContext(CONTEXT B, CONTEXT C) |
| { |
| B->context = C; |
| } |
| |
| static __inline__ CONTEXT cont_ContextBindingLink(CONTEXT C,SYMBOL Var) |
| { |
| return C[Var].link; |
| } |
| |
| static __inline__ TERM cont_ContextBindingTerm(CONTEXT C,SYMBOL Var) |
| { |
| return C[Var].term; |
| } |
| |
| static __inline__ void cont_SetContextBindingTerm(CONTEXT C, SYMBOL Var, TERM t) |
| { |
| C[Var].term = t; |
| } |
| |
| static __inline__ SYMBOL cont_ContextBindingSymbol(CONTEXT C,SYMBOL Var) |
| { |
| return C[Var].symbol; |
| } |
| |
| static __inline__ SYMBOL cont_ContextBindingRenaming(CONTEXT C,SYMBOL Var) |
| { |
| return C[Var].renaming; |
| } |
| |
| static __inline__ void cont_SetContextBindingRenaming(CONTEXT C, SYMBOL Var, |
| SYMBOL R) |
| { |
| C[Var].renaming = R; |
| } |
| |
| static __inline__ CONTEXT cont_ContextBindingContext(CONTEXT C,SYMBOL Var) |
| { |
| return C[Var].context; |
| } |
| |
| /**************************************************************/ |
| /* Predicates */ |
| /**************************************************************/ |
| |
| static __inline__ BOOL cont_VarIsBound(CONTEXT C, SYMBOL Var) |
| { |
| return cont_ContextBindingTerm(C,Var) != (TERM) NULL; |
| } |
| |
| static __inline__ BOOL cont_VarIsUsed(CONTEXT C, SYMBOL Var) |
| { |
| return cont_ContextBindingContext(C,Var) != (CONTEXT) NULL; |
| } |
| |
| static __inline__ BOOL cont_VarIsLinked(CONTEXT C, SYMBOL Var) |
| { |
| return cont_ContextBindingLink(C,Var) != (CONTEXT) NULL; |
| } |
| |
| static __inline__ BOOL cont_VarIsRenamed(CONTEXT C, SYMBOL Var) |
| { |
| return cont_ContextBindingRenaming(C, Var) != symbol_Null(); |
| } |
| |
| static __inline__ BOOL cont_VarIsClosed(CONTEXT C,SYMBOL Var) |
| { |
| return !cont_VarIsBound(C,Var) && cont_VarIsUsed(C,Var); |
| } |
| |
| static __inline__ BOOL cont_BindingIsBound(CONTEXT B) |
| { |
| return cont_BindingTerm(B) != (TERM) NULL; |
| } |
| |
| static __inline__ BOOL cont_BindingIsUsed(CONTEXT B) |
| { |
| return cont_BindingContext(B) != (CONTEXT) NULL; |
| } |
| |
| /**************************************************************/ |
| /* Aux functions for backtracking */ |
| /**************************************************************/ |
| |
| static __inline__ CONTEXT cont_LastBinding(void) |
| { |
| return cont_LASTBINDING; |
| } |
| |
| static __inline__ void cont_SetLastBinding(CONTEXT B) |
| { |
| cont_LASTBINDING = B; |
| } |
| |
| static __inline__ TERM cont_LastBindingTerm(void) |
| { |
| return cont_BindingTerm(cont_LastBinding()); |
| } |
| |
| static __inline__ SYMBOL cont_LastBindingSymbol(void) |
| { |
| return cont_BindingSymbol(cont_LastBinding()); |
| } |
| |
| static __inline__ CONTEXT cont_LastBindingContext(void) |
| { |
| return cont_BindingContext(cont_LastBinding()); |
| } |
| |
| static __inline__ BOOL cont_LastIsBound(void) |
| { |
| return cont_BindingIsBound(cont_LastBinding()); |
| } |
| |
| static __inline__ BOOL cont_LastIsUsed(void) |
| { |
| return cont_LastBindingContext() != (CONTEXT) NULL; |
| } |
| |
| static __inline__ BOOL cont_LastIsClosed(void) |
| { |
| return !cont_LastIsBound() && cont_LastIsUsed(); |
| } |
| |
| static __inline__ BOOL cont_IsInContext(CONTEXT C, SYMBOL Var, CONTEXT B) |
| { |
| return cont_Binding(C, Var) == B; |
| } |
| |
| static __inline__ CONTEXT cont_ContextOfBinding(CONTEXT B) |
| { |
| CONTEXT Result; |
| LIST Scan; |
| |
| for (Result = NULL, Scan = cont_LISTOFCONTEXTS; |
| list_Exist(Scan); |
| Scan = list_Cdr(Scan)) { |
| if (cont_IsInContext(list_Car(Scan), cont_BindingSymbol(B), B)) { |
| Result = list_Car(Scan); |
| break; |
| } |
| } |
| |
| #ifdef CHECK |
| if (Result == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_ContextOfBinding: Unknown context.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| return Result; |
| } |
| |
| /**************************************************************/ |
| /* Initialization */ |
| /**************************************************************/ |
| |
| static __inline__ void cont_InitBinding(CONTEXT C, SYMBOL Var) |
| { |
| cont_CURRENTBINDING = cont_Binding(C, Var); |
| cont_SetBindingLink(cont_CURRENTBINDING, (CONTEXT)NULL); |
| cont_SetBindingTerm(cont_CURRENTBINDING, (TERM)NULL); |
| cont_SetBindingSymbol(cont_CURRENTBINDING, Var); |
| cont_SetBindingRenaming(cont_CURRENTBINDING, symbol_Null()); |
| cont_SetBindingContext(cont_CURRENTBINDING, (CONTEXT)NULL); |
| } |
| |
| static __inline__ void cont_InitContext(CONTEXT C) |
| { |
| int i; |
| |
| for (i = 0; i < cont__SIZE; i++) |
| cont_InitBinding(C, i); |
| } |
| |
| /**************************************************************/ |
| /* Creation and deletion of contexts */ |
| /**************************************************************/ |
| |
| static __inline__ CONTEXT cont_Create(void) |
| { |
| CONTEXT Result; |
| |
| Result = (CONTEXT)memory_Malloc(cont__SIZE*sizeof(CONTEXT_NODE)); |
| |
| cont_InitContext(Result); |
| |
| cont_LISTOFCONTEXTS = list_Cons(Result, cont_LISTOFCONTEXTS); |
| cont_NOOFCONTEXTS++; |
| |
| return Result; |
| } |
| |
| static __inline__ void cont_Delete(CONTEXT C) |
| { |
| #ifdef CHECK |
| if ((cont_NOOFCONTEXTS == 0) || |
| !list_PointerMember(cont_LISTOFCONTEXTS, C)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_Delete: Context %ld not registered.\n", |
| (unsigned long)C); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_LISTOFCONTEXTS = list_PointerDeleteOneElement(cont_LISTOFCONTEXTS, C); |
| |
| cont_NOOFCONTEXTS--; |
| |
| memory_Free(C, cont__SIZE*sizeof(CONTEXT_NODE)); |
| } |
| |
| static __inline__ void cont_ResetIndexVarScanner(void) |
| { |
| cont_INDEXVARSCANNER = symbol_GetInitialIndexVarCounter(); |
| } |
| |
| /**************************************************************/ |
| /* Output bindings */ |
| /**************************************************************/ |
| |
| static __inline__ void cont_BindingOutput(CONTEXT C, SYMBOL Var) |
| { |
| symbol_Print(cont_ContextBindingSymbol(C, Var)); |
| putchar(':'); |
| symbol_Print(Var); |
| |
| fputs(" -> ", stdout); |
| |
| if (cont_VarIsBound(C, Var)) { |
| term_PrintPrefix(cont_ContextBindingTerm(C, Var)); |
| } else |
| fputs("unbound", stdout); |
| |
| fputs(" in ", stdout); |
| |
| if (cont_VarIsUsed(C, Var)) { |
| printf("%ld", (unsigned long)cont_ContextBindingContext(C, Var)); |
| } else |
| fputs("NULL (unused)", stdout); |
| |
| fputs(". ", stdout); |
| |
| if (cont_VarIsClosed(C, Var)) { |
| fputs("(closed)", stdout); |
| } |
| |
| if (!cont_VarIsBound(C, Var) && |
| !cont_VarIsUsed(C, Var)) { |
| fputs(",(free)", stdout); |
| } |
| |
| if (cont_VarIsRenamed(C, Var)) { |
| fputs(",(renamed): ", stdout); |
| symbol_Print(Var); |
| fputs(" -> ", stdout); |
| symbol_Print(cont_ContextBindingRenaming(C, Var)); |
| } |
| |
| fflush(stdout); |
| } |
| |
| static __inline__ void cont_PrintCurrentTrail(void) |
| { |
| fputs("\nPrint bindings:", stdout); |
| cont_CURRENTBINDING = cont_LastBinding(); |
| while (cont_CURRENTBINDING) { |
| cont_BindingOutput(cont_ContextOfBinding(cont_CURRENTBINDING), |
| cont_BindingSymbol(cont_CURRENTBINDING)); |
| cont_CURRENTBINDING = cont_BindingLink(cont_CURRENTBINDING); |
| if (cont_CURRENTBINDING) |
| putchar('\n'); |
| } |
| fflush(stdout); |
| } |
| |
| /**************************************************************/ |
| /* Close bindings */ |
| /**************************************************************/ |
| |
| static __inline__ void cont_CloseBindingHelp(CONTEXT C, SYMBOL Var) |
| { |
| cont_SetContextBindingTerm(C, Var, NULL); |
| } |
| |
| static __inline__ void cont_CloseBindingBindingHelp(CONTEXT B) |
| { |
| cont_SetBindingTerm(B, NULL); |
| } |
| |
| #if SHOWBINDINGS |
| static __inline__ void cont_CloseBinding(CONTEXT C, SYMBOL Var) |
| { |
| fputs("\nClose binding from ", stdout); |
| cont_BindingOutput(C, Var); |
| cont_CloseBindingHelp(C, Var); |
| } |
| #else |
| static __inline__ void cont_CloseBinding(CONTEXT C, SYMBOL Var) |
| { |
| cont_CloseBindingHelp(C, Var); |
| } |
| #endif |
| |
| static __inline__ void cont_CloseBindingBinding(CONTEXT B) { |
| cont_CloseBindingBindingHelp(B); |
| } |
| |
| /**************************************************************/ |
| /* Establish bindings */ |
| /**************************************************************/ |
| |
| static __inline__ void cont_CreateBindingHelp(CONTEXT C, SYMBOL Var, |
| CONTEXT CTerm, TERM Term) |
| { |
| #ifdef CHECK |
| if (cont_VarIsBound(C, Var)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_CreateBindingHelp: Variable already bound.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_CURRENTBINDING = cont_Binding(C,Var); |
| cont_SetBindingTerm(cont_CURRENTBINDING, Term); |
| cont_SetBindingContext(cont_CURRENTBINDING, CTerm); |
| cont_SetBindingLink(cont_CURRENTBINDING, cont_LastBinding()); |
| cont_SetLastBinding(cont_CURRENTBINDING); |
| } |
| |
| #if SHOWBINDINGS |
| |
| static __inline__ int cont_CreateBinding(CONTEXT C, SYMBOL Var, CONTEXT CTerm, TERM Term) |
| { |
| cont_CreateBindingHelp(C,Var,CTerm,Term); |
| fputs("\nEstablish binding from ", stdout); |
| cont_BindingOutput(C, Var); |
| return ++cont_BINDINGS; |
| } |
| |
| static __inline__ int cont_CreateClosedBinding(CONTEXT C, SYMBOL Var) |
| { |
| cont_CreateBindingHelp(C, Var, C, NULL); |
| fputs("\nEstablish closed binding from ", stdout); |
| cont_BindingOutput(C,Var); |
| return ++cont_BINDINGS; |
| } |
| |
| #else |
| |
| static __inline__ int cont_CreateBinding(CONTEXT C, SYMBOL Var, CONTEXT CTerm, TERM Term) |
| { |
| cont_CreateBindingHelp(C,Var,CTerm,Term); |
| return ++cont_BINDINGS; |
| } |
| |
| static __inline__ int cont_CreateClosedBinding(CONTEXT C, SYMBOL Var) |
| { |
| cont_CreateBindingHelp(C, Var, C, NULL); |
| return ++cont_BINDINGS; |
| } |
| |
| #endif |
| |
| /**************************************************************/ |
| /* Backtracking */ |
| /**************************************************************/ |
| |
| static __inline__ void cont_BackTrackLastBindingHelp(void) |
| { |
| cont_CURRENTBINDING = cont_LastBinding(); |
| cont_SetLastBinding(cont_BindingLink(cont_CURRENTBINDING)); |
| cont_SetBindingTerm(cont_CURRENTBINDING, NULL); |
| cont_SetBindingContext(cont_CURRENTBINDING, NULL); |
| cont_SetBindingRenaming(cont_CURRENTBINDING, symbol_Null()); |
| cont_SetBindingLink(cont_CURRENTBINDING, NULL); |
| |
| cont_BINDINGS--; |
| } |
| |
| #if SHOWBINDINGS |
| |
| static __inline__ void cont_BackTrackLastBinding(void) |
| { |
| CONTEXT LastContext; |
| SYMBOL LastSymbol; |
| |
| LastContext = cont_ContextOfBinding(cont_LastBinding()); |
| LastSymbol = cont_LastBindingSymbol(); |
| fputs("\nBacktrack binding from ", stdout); |
| cont_BindingOutput(LastContext, LastSymbol); |
| cont_BackTrackLastBindingHelp(); |
| } |
| |
| static __inline__ int cont_BackTrack(void) |
| { |
| printf("\nBacktrack %d bindings:", cont_BINDINGS); |
| |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| if (!cont_StackEmpty(0)) |
| cont_BINDINGS = cont_StackPopResult(); |
| |
| fflush(stdout); |
| return 0; |
| } |
| |
| static __inline__ int cont_StopAndBackTrack(void) |
| { |
| #ifdef CHECK |
| if (cont_BINDINGS > 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_StopAndBackTrack: Bindings not reset!\n"); |
| misc_FinishErrorReport(); |
| } else if (cont_StackEmpty(0)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_StopAndBackTrack: No bindings on stack!\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| cont_BINDINGS = cont_StackPopResult(); |
| |
| printf("\nStop and Backtrack %d bindings:", cont_BINDINGS); |
| |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| fflush(stdout); |
| return 0; |
| } |
| |
| static __inline__ int cont_BackTrackAndStart(void) |
| { |
| printf("\nBacktrack %d bindings:", cont_BINDINGS); |
| |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| fflush(stdout); |
| return 0; |
| } |
| |
| static __inline__ void cont_Reset(void) |
| { |
| fputs("\nReset bindings:", stdout); |
| while (cont_LastBinding()) |
| cont_BackTrackLastBinding(); |
| |
| cont_BINDINGS = 0; |
| cont_StackInit(); |
| cont_ResetIndexVarScanner(); |
| fflush(stdout); |
| } |
| |
| #else |
| |
| static __inline__ void cont_BackTrackLastBinding(void) |
| { |
| cont_BackTrackLastBindingHelp(); |
| } |
| |
| static __inline__ int cont_BackTrack(void) |
| { |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| if (!cont_StackEmpty(0)) |
| cont_BINDINGS = cont_StackPopResult(); |
| |
| return 0; |
| } |
| |
| static __inline__ int cont_StopAndBackTrack(void) |
| { |
| #ifdef CHECK |
| if (cont_BINDINGS > 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_StopAndBackTrack: Bindings not reset!\n"); |
| misc_FinishErrorReport(); |
| } else if (cont_StackEmpty(0)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_StopAndBackTrack: No bindings on stack!\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| cont_BINDINGS = cont_StackPopResult(); |
| |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| return 0; |
| } |
| |
| static __inline__ int cont_BackTrackAndStart(void) |
| { |
| while (cont_BINDINGS > 0) |
| cont_BackTrackLastBinding(); |
| |
| return 0; |
| } |
| |
| static __inline__ void cont_Reset(void) |
| { |
| while (cont_LastBinding()) |
| cont_BackTrackLastBinding(); |
| |
| cont_BINDINGS = 0; |
| cont_StackInit(); |
| cont_ResetIndexVarScanner(); |
| } |
| |
| #endif |
| |
| /**************************************************************/ |
| /* Check state of bindings */ |
| /**************************************************************/ |
| |
| #define cont__CHECKSTACKSIZE 1000 |
| #define cont__CHECKSTACKEMPTY 0 |
| |
| typedef POINTER cont_CHECKSTACK_TYPE[cont__CHECKSTACKSIZE]; |
| |
| extern cont_CHECKSTACK_TYPE cont_CHECKSTACK; |
| extern int cont_CHECKSTACKPOINTER; |
| |
| /* Stack operations */ |
| |
| static __inline__ void cont_CheckStackInit(void) |
| { |
| cont_CHECKSTACKPOINTER = cont__CHECKSTACKEMPTY; |
| } |
| |
| static __inline__ void cont_CheckStackPush(POINTER Entry) |
| { |
| #ifdef CHECK |
| if (cont_CHECKSTACKPOINTER >= cont__STACKSIZE) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_CheckStackPush: Context check stack overflow!\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| cont_CHECKSTACK[cont_CHECKSTACKPOINTER++] = Entry; |
| } |
| |
| static __inline__ void cont_CheckStackPop(void) |
| { |
| --cont_CHECKSTACKPOINTER; |
| } |
| |
| static __inline__ POINTER cont_CheckStackPopResult(void) |
| { |
| return cont_CHECKSTACK[--cont_CHECKSTACKPOINTER]; |
| } |
| |
| static __inline__ void cont_CheckStackNPop(int N) |
| { |
| cont_CHECKSTACKPOINTER -= N; |
| } |
| |
| static __inline__ POINTER cont_CheckStackTop(void) |
| { |
| return cont_CHECKSTACK[cont_CHECKSTACKPOINTER - 1]; |
| } |
| |
| static __inline__ POINTER cont_CheckStackNthTop(int N) |
| { |
| return cont_CHECKSTACK[cont_CHECKSTACKPOINTER - (1 + N)]; |
| } |
| |
| static __inline__ void cont_CheckStackRplacTop(POINTER Entry) |
| { |
| cont_CHECKSTACK[cont_CHECKSTACKPOINTER - 1] = Entry; |
| } |
| |
| static __inline__ void cont_CheckStackRplacNthTop(int N, POINTER Entry) |
| { |
| cont_CHECKSTACK[cont_CHECKSTACKPOINTER - (1 + N)] = Entry; |
| } |
| |
| static __inline__ void cont_CheckStackRplacNth(int N, POINTER Entry) |
| { |
| cont_CHECKSTACK[N] = Entry; |
| } |
| |
| static __inline__ int cont_CheckStackBottom(void) |
| { |
| return cont_CHECKSTACKPOINTER; |
| } |
| |
| static __inline__ void cont_CheckStackSetBottom(int Pointer) |
| { |
| cont_CHECKSTACKPOINTER = Pointer; |
| } |
| |
| static __inline__ BOOL cont_CheckStackEmpty(int Pointer) |
| { |
| return cont_CHECKSTACKPOINTER == Pointer; |
| } |
| |
| extern CONTEXT cont_STATELASTBINDING; /* Storage to save state of trails. */ |
| extern int cont_STATEBINDINGS; /* Storage to save number of current bindings. */ |
| extern int cont_STATESTACK; /* Storage to save state of stack. */ |
| extern int cont_STATETOPSTACK; /* Storage to save state of the top element of the stack. */ |
| |
| static __inline__ BOOL cont_CheckLastBinding(CONTEXT Check, int Bindings) |
| { |
| CONTEXT Scan; |
| BOOL Result; |
| |
| Scan = cont_LastBinding(); |
| |
| while (Bindings > 0) { |
| Scan = cont_BindingLink(Scan); |
| Bindings--; |
| } |
| if (Check == Scan) |
| Result = TRUE; |
| else |
| Result = FALSE; |
| |
| return Result; |
| } |
| |
| static __inline__ void cont_CheckState(void) |
| { |
| if (cont_CheckStackEmpty(cont__CHECKSTACKEMPTY)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_CheckState: No states saved.\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| cont_STATETOPSTACK = (int)cont_CheckStackPopResult(); |
| cont_STATESTACK = (int)cont_CheckStackPopResult(); |
| cont_STATEBINDINGS = (int)cont_CheckStackPopResult(); |
| cont_STATELASTBINDING = (CONTEXT)cont_CheckStackPopResult(); |
| |
| if ((cont_STATELASTBINDING != cont_LastBinding()) || |
| (cont_STATEBINDINGS != cont_BINDINGS) || |
| (!cont_StackEmpty(cont_STATESTACK)) || |
| (cont_STATETOPSTACK != cont_StackTop())) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cont_CheckState: State of contexts does not match saved state."); |
| misc_ErrorReport("\nTrail: Saved state: %ld; current state: %ld.", |
| (long)cont_STATELASTBINDING, (long)cont_LastBinding()); |
| misc_ErrorReport("\nNumber of bindings: Saved state: %d; current state: %d.", |
| cont_STATEBINDINGS, cont_BINDINGS); |
| misc_ErrorReport("\nBinding stack pointer: Saved state: %d; current state: %d.", |
| cont_STATESTACK, cont_StackBottom()); |
| misc_ErrorReport("\nNumber of bindings on top of stack: Saved state: %d; current state: %d.\n\n", |
| cont_STATETOPSTACK, cont_StackTop()); |
| misc_FinishErrorReport(); |
| } |
| } |
| |
| static __inline__ void cont_SaveState(void) |
| { |
| cont_CheckStackPush((POINTER)cont_LastBinding()); |
| cont_CheckStackPush((POINTER)cont_BINDINGS); |
| cont_CheckStackPush((POINTER)cont_StackBottom()); |
| cont_CheckStackPush((POINTER)cont_StackTop()); |
| } |
| |
| static __inline__ BOOL cont_IsContextEmpty(const CONTEXT Check) |
| { |
| int i; |
| |
| for (i = 0; i < cont__SIZE; i++) |
| if (cont_VarIsBound(Check, i) || |
| cont_VarIsUsed(Check, i) || |
| cont_VarIsLinked(Check, i) || |
| cont_VarIsRenamed(Check, i)) |
| return FALSE; |
| |
| return TRUE; |
| } |
| |
| /**************************************************************/ |
| /* Generation of index variables */ |
| /**************************************************************/ |
| |
| static __inline__ SYMBOL cont_NextIndexVariable(const CONTEXT IndexContext) |
| { |
| if (symbol_Equal(cont_INDEXVARSCANNER, symbol_LastIndexVariable())) |
| cont_INDEXVARSCANNER = symbol_CreateIndexVariable(); |
| else |
| for (;;) { |
| cont_INDEXVARSCANNER = symbol_NextIndexVariable(cont_INDEXVARSCANNER); |
| if (!cont_VarIsUsed(IndexContext, cont_INDEXVARSCANNER)) |
| break; |
| else |
| if (symbol_Equal(cont_INDEXVARSCANNER, symbol_LastIndexVariable())) { |
| cont_INDEXVARSCANNER = symbol_CreateIndexVariable(); |
| break; |
| } |
| } |
| return cont_INDEXVARSCANNER; |
| } |
| |
| /**************************************************************/ |
| /* Dereferencing of terms wrt. contexts */ |
| /**************************************************************/ |
| |
| static __inline__ TERM cont_Deref(CONTEXT* Context, TERM Term) |
| /************************************************************** |
| INPUT: A call-by-ref context and a term. |
| RETURNS: The dereferenced term and the corresponding context. |
| SUMMARY: Dereferences bindings of variables. |
| CAUTION: In general, the context of the returned term |
| is different to the input context. |
| ***************************************************************/ |
| { |
| |
| while (term_IsVariable(Term) && *Context != cont_InstanceContext()) { |
| SYMBOL TermTop; |
| |
| TermTop = term_TopSymbol(Term); |
| |
| if (cont_VarIsBound(*Context, TermTop)) { |
| CONTEXT HelpContext; |
| |
| HelpContext = cont_ContextBindingContext(*Context, TermTop); |
| Term = cont_ContextBindingTerm(*Context, TermTop); |
| *Context = HelpContext; |
| } |
| else |
| return Term; |
| } |
| |
| return Term; |
| } |
| |
| /**************************************************************/ |
| /* Functions for Initialization and Controlling */ |
| /**************************************************************/ |
| |
| void cont_Init(void); |
| void cont_Check(void); |
| void cont_Free(void); |
| |
| /**************************************************************/ |
| /* Functions for Term Equality Test with respect to Bindings */ |
| /**************************************************************/ |
| |
| BOOL cont_TermEqual(CONTEXT, TERM, CONTEXT, TERM); |
| BOOL cont_TermEqualModuloBindings(CONTEXT, CONTEXT, TERM, CONTEXT, TERM); |
| |
| /**************************************************************/ |
| /* Functions for Applying Bindings */ |
| /**************************************************************/ |
| |
| TERM cont_CopyAndApplyBindings(CONTEXT, TERM); |
| TERM cont_CopyAndApplyBindingsCom(const CONTEXT, TERM); |
| |
| TERM cont_ApplyBindingsModuloMatching(const CONTEXT, TERM, BOOL); |
| TERM cont_ApplyBindingsModuloMatchingReverse(const CONTEXT, TERM); |
| |
| BOOL cont_BindingsAreRenamingModuloMatching(const CONTEXT); |
| |
| /**************************************************************/ |
| /* Misc Functions */ |
| /**************************************************************/ |
| |
| SYMBOL cont_TermMaxVar(CONTEXT, TERM); |
| NAT cont_TermSize(CONTEXT, TERM); |
| BOOL cont_TermContainsSymbol(CONTEXT, TERM, SYMBOL); |
| |
| /**************************************************************/ |
| /* Functions for Output */ |
| /**************************************************************/ |
| |
| void cont_TermPrintPrefix(CONTEXT, TERM); |
| |
| #endif |