Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1049 insertions, 0 deletions

diff --git a/test/spass/context.h b/test/spass/context.h
new file mode 100644
index 0000000..a3239ac
--- /dev/null
+++ b/test/spass/context.h
@@ -0,0 +1,1049 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *                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: 21527 $                                        * */
+/* $State$                                            * */
+/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
+/* $Author: duraid $                                       * */
+/* *                                                        * */
+/* *             Contact:                                   * */
+/* *             Christoph Weidenbach                       * */
+/* *             MPI fuer Informatik                        * */
+/* *             Stuhlsatzenhausweg 85                      * */
+/* *             66123 Saarbruecken                         * */
+/* *             Email: weidenb@mpi-sb.mpg.de               * */
+/* *             Germany                                    * */
+/* *                                                        * */
+/* ********************************************************** */
+/**************************************************************/
+
+
+/* $RCSfile$ */
+
+
+#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