An initial import of the teyjus source code in the C runtime for GF. The two runtime are still not connected but the source code compiles.

1 files changed, 814 insertions, 0 deletions

diff --git a/src/runtime/c/teyjus/simulator/printterm.c b/src/runtime/c/teyjus/simulator/printterm.c
new file mode 100644
index 000000000..2fbe03fd2
--- /dev/null
+++ b/src/runtime/c/teyjus/simulator/printterm.c
@@ -0,0 +1,814 @@
+//////////////////////////////////////////////////////////////////////////////
+//Copyright 2008
+//  Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
+//////////////////////////////////////////////////////////////////////////////
+// This file is part of Teyjus.                                             //
+//                                                                          //
+// Teyjus 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 3 of the License, or        //
+// (at your option) any later version.                                      //
+//                                                                          //
+// Teyjus 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 Teyjus.  If not, see <http://www.gnu.org/licenses/>.          //
+//////////////////////////////////////////////////////////////////////////////
+/****************************************************************************
+ *                                                                          *
+ * File printterm.c. This file contains routines for printing out lambda    *
+ * terms. It is assumed that these routines will be needed in two           *
+ * situations: printing out answers to queries and displaying terms as      *
+ * needed by invocation of builtin goals.                                   *
+ * The difference between these two situations is in the display of         *
+ * free term variables. Only when displaying answers is an attempt made to  *
+ * present these using sensible names: in this case, either the name in the *
+ * query is used or a concise name is cooked up. In the other situation,    *
+ * the address of the variable cell is used as the name.                    *
+ *                                                                          *
+ * Certain assumptions are relevant to avoiding name clashes. For local     *
+ * constants, the assumption is that no constant names in user              *
+ * programs begin with <lc- and end with >. The use of this idea is         *
+ * buried inside the routine PRINT_writeHCName.                             *
+ * Violation of this condition is *not* checked. For term variables, the    *
+ * assumption is that bound variables do not begin with _.                  *
+ *                                                                          *
+ ****************************************************************************/
+#include <stdlib.h>
+#include <string.h>
+#include "printterm.h"
+#include "mctypes.h"
+#include "mcstring.h"
+#include "hnorm.h"
+#include "dataformats.h"
+#include "abstmachine.h"
+#include "io-datastructures.h"
+#include "builtins/builtins.h"
+#include "../system/stream.h"
+#include "../system/error.h"
+#include "../system/operators.h"
+#include "../tables/pervasives.h"
+
+//temp
+#include <stdio.h>
+
+/* This variable records the number of query variables */
+int PRINT_numQueryVars;
+
+/* flag determining whether or not to print sensible names for free vars */
+Boolean PRINT_names = FALSE;
+
+static void PRINT_writeTerm(WordPtr outStream, DF_TermPtr tmPtr, 
+                            OP_FixityType infx, int inprec, OP_TermContext tc);
+
+/****************************************************************************
+ *                   Auxiliary routines used in this file                   *
+ ****************************************************************************/
+static Boolean PRINT_parenNeeded(OP_FixityType opfx, int opprec, 
+                                 OP_TermContext context, OP_FixityType fx, 
+                                 int prec)
+{
+    Boolean pparen = FALSE;
+    if (context == OP_LEFT_TERM) {
+        switch (fx) {
+        case OP_INFIX: case OP_INFIXR: case OP_POSTFIX:
+            if (opprec <= prec) pparen = TRUE;   break;
+        case OP_INFIXL: case OP_POSTFIXL: 
+        {
+            switch (opfx) {
+            case OP_PREFIX: case OP_INFIX: case OP_INFIXL: case OP_POSTFIX:
+            case OP_POSTFIXL: 
+                if (opprec < prec) pparen = TRUE; break;
+            default:
+                if (opprec <= prec) pparen = TRUE; break;
+            }
+            break;
+        }
+        }
+    } else if (context == OP_RIGHT_TERM) {
+        switch (fx) {
+        case OP_INFIX: case OP_INFIXL: case OP_PREFIX:
+            if (opprec <= prec) pparen = TRUE; break;
+        case OP_INFIXR: case OP_PREFIXR:
+        {
+            switch (opfx) {
+            case OP_INFIXL: case OP_POSTFIXL:
+                if (opprec <= prec) pparen = TRUE; break;
+            default:
+                if (opprec < prec) pparen = TRUE; break;
+            }
+        }
+        }
+    }
+    return pparen;
+}
+
+/* making a name from the address of an unbound term variable */
+static long PRINT_makeNumberName(DF_TermPtr tmPtr)
+{ return (long)tmPtr - (long)AM_heapBeg;                      }
+
+
+/****************************************************************************
+ * Routines for printing out keywords and punctuation symbols in the course *
+ * of displaying lambda terms. These have been extracted out of the other   *
+ * routines so as to make stylistic changes at a later point easier to      *
+ * effect.                                                                  *
+ ****************************************************************************/
+static void PRINT_writeLParen(WordPtr outStream)
+{ STREAM_printf(outStream, "(");                             }
+
+static void PRINT_writeRParen(WordPtr outStream)
+{ STREAM_printf(outStream, ")");                             }
+
+static void PRINT_writeConsSymbol(WordPtr outStream)
+{ STREAM_printf(outStream, " :: ");                          }
+
+static void PRINT_writeNilSymbol(WordPtr outStream)
+{ STREAM_printf(outStream, "nil");                           }
+
+static void PRINT_writeInfixLam(WordPtr outStream)
+{ STREAM_printf(outStream, "\\ ");                           }
+
+static void PRINT_writeLam(WordPtr outStream, int numabs) 
+{ STREAM_printf(outStream, "lam(%d, ", numabs);               }
+
+static void PRINT_writeSpace(WordPtr outStream, int i)
+{ while (i--) STREAM_printf(outStream, " ");                 }    
+
+static void PRINT_writeEquals(WordPtr outStream) 
+{ STREAM_printf(outStream, " = ");                           }
+
+static void PRINT_writeComma(WordPtr outStream)
+{ STREAM_printf(outStream, ",");                             }
+
+static void PRINT_writeDPairStart(WordPtr outStream)
+{ STREAM_printf(outStream, "<");                             }
+    
+static void PRINT_writeDPairEnd(WordPtr outStream)
+{ STREAM_printf(outStream, ">");                             }
+
+/***************************************************************************
+ * Writing out terms corresponding to the builtin constants.               *
+ ***************************************************************************/
+/* Writing out an integer term to a given output stream */
+static void PRINT_writeInt(WordPtr outStream, DF_TermPtr tmPtr)
+{ STREAM_printf(outStream, "%d", DF_intValue(tmPtr));        }
+
+/* Writing out a float term to a given output stream */
+static void PRINT_writeFloat(WordPtr outStream, DF_TermPtr tmPtr)
+{ STREAM_printf(outStream, "%f", DF_floatValue(tmPtr));      }
+
+/* Writing out a string term to a given output stream */
+static void PRINT_writeString(WordPtr outStream, DF_TermPtr tmPtr)
+{ STREAM_printf(outStream, "\"%s\"", MCSTR_toCString(DF_strValue(tmPtr))); }
+
+/* Writing out a stream constant to a given output stream */
+static void PRINT_writeStream(WordPtr outStream, DF_TermPtr tmPtr)
+{
+    WordPtr stream = DF_streamTabIndex(tmPtr);
+    STREAM_printf(outStream, "<stream ");
+    if (stream == STREAM_ILLEGAL) STREAM_printf(outStream, "-- closed>");
+    else STREAM_printf(outStream, "-- \"%s\">", STREAM_getName(stream));
+}
+
+/****************************************************************************
+ *  Writing out a constant. Use the index into the runtime constant table   *
+ *  stored in the constant to get the constant name if one exists. If one   *
+ *  does not exist, i.e. if the constant is a local or hidden one, look for *
+ *  it in a list of constants. If it is not in this list, make up a new     *
+ *  name. Eventually, the name consists of three parts: a generic name for  *
+ *  hidden constants, a part based on the runtime table index and a part    *
+ *  based on the universe index.                                            *
+ ****************************************************************************/
+/* A structure for maintaining information about local constants encountered
+while printing; this structure enables the assignment of a unique integer
+to each runtime symbol table slot for such a constant. */
+typedef struct  PRINT_ConstList_ *PRINT_ConstList;
+
+struct  PRINT_ConstList_ 
+{
+    int   constInd;
+    int   count;
+    PRINT_ConstList  next; 
+};
+
+static PRINT_ConstList PRINT_clist = NULL;
+static int PRINT_lccount = 0;
+
+static void PRINT_cleanCList()
+{
+    PRINT_ConstList tmp;
+    
+    PRINT_lccount = 0;
+    while (PRINT_clist){
+        tmp = PRINT_clist;
+        PRINT_clist = PRINT_clist -> next;
+        free(tmp);
+    }
+}
+
+/* writing out a hidden (local) constant name; as side effect, a note may be 
+   made of a new hidden (local) constant seen during this printing. */
+static void PRINT_writeHCName(WordPtr outStream, int constInd, int uc)
+{
+    PRINT_ConstList lclist = PRINT_clist;
+    while (lclist && (lclist->constInd != constInd)) lclist = lclist->next;
+    
+    if (!lclist) {
+        lclist = (PRINT_ConstList)EM_malloc(sizeof(struct PRINT_ConstList_));
+        lclist->constInd = constInd;
+        lclist->count    = PRINT_lccount++;
+        lclist->next     = PRINT_clist;
+        PRINT_clist      = lclist;
+    }
+    
+    STREAM_printf(outStream, "<lc-%d-%d>", lclist->count, uc);
+}
+
+/* Writing out a constant, hidden or global. */
+static void PRINT_writeConst(WordPtr outStream, DF_TermPtr tmPtr)
+{
+    int   constInd = DF_constTabIndex(tmPtr);
+    char* name     = AM_cstName(constInd);
+    
+    if (name) STREAM_printf(outStream, "%s", name);
+    else PRINT_writeHCName(outStream, constInd, DF_constUnivCount(tmPtr));
+}
+
+/****************************************************************************
+ * Writing out a free variable. Two situations are possible, one where a    *
+ * symbolic name is to be produced and the other where the `address' could  *
+ * serve as the name. In the first case, if the variable is a query         *
+ * variable, then its name from the query is used. Otherwise a new name is  *
+ * invented that is distinct from other free term variable names; the       *
+ * initial segment of the name guarantees that it will be distinct from     *
+ * that of  bound variables.                                                *
+ ****************************************************************************/
+/* counter used to generate free variable name */
+static int  PRINT_fvcounter = 1;
+
+/* Create a free term variable name; this starts with _ has a standard
+   string prefix and then a digit sequence */
+static DF_StrDataPtr PRINT_makeFVarName()
+{
+    int           digits = 0;
+    int           i = PRINT_fvcounter;
+    int           length;
+    char*         cname;
+    DF_StrDataPtr fvname;
+
+    while(i) { digits++; i = i/10; }
+
+    length = digits + 3;
+    cname = (char*)EM_malloc(sizeof(char)*length);
+    cname[0] = '_';
+    cname[1] = 'T';
+    cname[length-1] = '\0';
+    
+    i = PRINT_fvcounter;
+    while(i) {
+        cname[digits+1] = (i%10 + '0');
+        i = i/10;
+        digits--;
+    }
+    PRINT_fvcounter++;
+
+    fvname = (DF_StrDataPtr)EM_malloc(sizeof(Word)*(MCSTR_numWords(length) +
+						    DF_STRDATA_HEAD_SIZE));
+    DF_mkStrDataHead((MemPtr)fvname);
+    MCSTR_toString((MemPtr)((MemPtr)fvname + DF_STRDATA_HEAD_SIZE),
+                   cname, length);
+    free(cname);
+    return fvname;
+}
+
+/* Does a made up name occur in the free term variable table? Clash can
+only occur with names in the user query */
+static Boolean PRINT_nameInFVTab(DF_StrDataPtr name)
+{
+    int i;
+    for (i = 0; i < PRINT_numQueryVars ; i++){
+      if (MCSTR_sameStrs(DF_strDataValue(name), 
+			 DF_strDataValue(IO_freeVarTab[i].varName)))
+	return TRUE;
+    }
+    return FALSE;
+}
+
+/* The main routine for printing out an unbound term variable */
+static void PRINT_writeFVar(WordPtr outStream, DF_TermPtr tmPtr)
+{
+    int           fvind = 0;
+    DF_StrDataPtr fvname;
+
+		//PRINT_names = TRUE;
+    if (PRINT_names) {
+        IO_freeVarTab[IO_freeVarTabTop].rigdes = tmPtr;
+        
+        while (tmPtr != IO_freeVarTab[fvind].rigdes) fvind++;
+        
+        if (fvind == IO_freeVarTabTop) {
+            /* i.e., a free variable not seen before */
+            if (IO_freeVarTabTop == IO_MAX_FREE_VARS) 
+                EM_error(BI_ERROR_TYFVAR_CAP);
+            
+            while(1) {//make a name
+                fvname = PRINT_makeFVarName();
+                if (!PRINT_nameInFVTab(fvname)) break;
+                free(fvname);
+            }
+            
+            IO_freeVarTab[fvind].varName = fvname;
+            IO_freeVarTabTop++;
+        }
+        STREAM_printf(outStream, 
+	       MCSTR_toCString(DF_strDataValue(IO_freeVarTab[fvind].varName)));
+    } else { //PRINT_names = FALSE
+        STREAM_printf(outStream, "_%ld", PRINT_makeNumberName(tmPtr));
+    }
+}
+
+/****************************************************************************
+ * Routines for writing out bound variables (in lambda abstraction and      *
+ * bound variable occurrence)                                               *
+ ****************************************************************************/
+/* prefix for bound variables */
+static char* PRINT_bvname = "W";
+
+/* a counter for determining the suffix part of bound variables */
+static int PRINT_bvcounter = 1;
+
+/* A structure for maintaining information about bound variable names */
+typedef struct PRINT_BVList_ *PRINT_BVList;
+
+struct PRINT_BVList_ {
+  DF_StrDataPtr name;
+  PRINT_BVList  next; };
+
+/* the initial list of bound variable names; initialized in SIM_InitIo */
+static  PRINT_BVList  PRINT_bvs = NULL;
+
+static void PRINT_cleanBV(PRINT_BVList bv)
+{
+  free(bv->name);
+  free(bv);
+}
+
+/* releasing the space for bound variables; needed only in case of error
+   exit */  
+static void PRINT_cleanBVList()
+{
+  PRINT_BVList tbvl;
+
+  PRINT_bvcounter = 1;
+  while (PRINT_bvs) {
+    tbvl = PRINT_bvs; PRINT_bvs = PRINT_bvs->next; 
+    PRINT_cleanBV(tbvl);
+  }
+}
+
+/****************************************************************************
+ * Writing out a bound variable                                             *
+ ****************************************************************************/
+static void PRINT_writeBVar(WordPtr outStream, DF_TermPtr tmPtr)
+{
+  int i;
+  int bvind = DF_bvIndex(tmPtr);
+  PRINT_BVList lbvs = PRINT_bvs;
+
+  for (i = bvind; ((i != 1) && lbvs) ; i--) 
+    lbvs = lbvs->next;
+
+  // Is this checking and the else branch really necessary? 
+  // Printing should start from top-level closed terms?
+  if (lbvs) STREAM_printf(outStream, "%s", 
+			  MCSTR_toCString(DF_strDataValue(lbvs->name)));
+  else STREAM_printf(outStream, "#%d", i); 
+}
+
+/****************************************************************************
+ * Writing out an empty list                                                *
+ ****************************************************************************/
+static void PRINT_writeNil(WordPtr outStream)
+{  PRINT_writeNilSymbol(outStream);                      }
+
+/****************************************************************************
+ * Writing out a non-empty list.                                            *
+ ****************************************************************************/
+static void PRINT_writeCons(WordPtr outStream, DF_TermPtr tmPtr, 
+                            OP_FixityType fx, int prec, OP_TermContext tc)
+{
+    DF_TermPtr    args     = DF_consArgs(tmPtr);
+    DF_TermPtr    arg;
+    OP_FixityType consfix  = (OP_FixityType)AM_cstFixity(PERV_CONS_INDEX);
+    int           consprec = AM_cstPrecedence(PERV_CONS_INDEX);
+    Boolean       pparen   = PRINT_parenNeeded(consfix, consprec, tc, fx,prec);
+
+    if (pparen) PRINT_writeLParen(outStream);
+    PRINT_writeTerm(outStream, args, consfix, consprec, OP_LEFT_TERM);    
+    PRINT_writeConsSymbol(outStream);
+    
+    do {
+        args++;
+        tmPtr = DF_termDeref(args);
+        if (DF_termTag(tmPtr) != DF_TM_TAG_CONS) break;
+        args = DF_consArgs(tmPtr);
+        PRINT_writeTerm(outStream, args, consfix, consprec, OP_LEFT_TERM);
+        PRINT_writeConsSymbol(outStream);
+    } while(1);
+    
+    PRINT_writeTerm(outStream, tmPtr, consfix, consprec, OP_RIGHT_TERM);
+    if (pparen) PRINT_writeRParen(outStream);
+}
+
+/****************************************************************************
+ * Writing out an abstraction.                                              *
+ ****************************************************************************/
+/* creating a bound variable name with bound variable prefix followed by the*/
+/* current bound variable counter value.                                    */
+static DF_StrDataPtr PRINT_makeBVarName()
+{
+  int            digits = 0;
+  int            i = PRINT_bvcounter;
+  int            length;
+  char*          cname;
+  DF_StrDataPtr  bvname;
+
+  while(i) { digits++; i = i/10; }
+
+  length = digits + 2;
+  cname = (char*)EM_malloc(sizeof(char)*length);
+  strcpy(cname, PRINT_bvname);
+  cname[length-1] = '\0';
+  
+  i = PRINT_bvcounter;
+  while(i) {
+    cname[digits] = (i%10 + '0');
+    i = i/10;
+    digits--;
+  }
+  PRINT_bvcounter++;
+
+  bvname = (DF_StrDataPtr)EM_malloc(sizeof(Word)*(MCSTR_numWords(length) +
+						  DF_STRDATA_HEAD_SIZE));
+ 
+  DF_mkStrDataHead((MemPtr)bvname);
+  MCSTR_toString((MemPtr)((MemPtr)bvname + DF_STRDATA_HEAD_SIZE),
+		 cname, length);
+  free(cname);
+  return bvname;
+}
+
+static void PRINT_writeAbstBinders(WordPtr outStream, int nabs) 
+{
+  DF_StrDataPtr bvname;
+  PRINT_BVList  tmpbvs;
+
+  while(nabs > 0) {
+    nabs--;
+    while(1) {//make a bvname not in FV table
+      bvname = PRINT_makeBVarName();
+      if (!PRINT_nameInFVTab(bvname)) break;
+      free(bvname);
+    }
+
+    //record the name into the head of the current bvlist
+    tmpbvs = (PRINT_BVList)EM_malloc(sizeof(struct PRINT_BVList_));
+    tmpbvs->name = bvname;
+    tmpbvs->next = PRINT_bvs;
+    PRINT_bvs = tmpbvs;
+    //write out binder
+    STREAM_printf(outStream, "%s", MCSTR_toCString(DF_strDataValue(bvname)));
+    PRINT_writeInfixLam(outStream);
+  }
+}
+
+static void PRINT_writeAbst(WordPtr outStream, DF_TermPtr tmPtr, 
+                            OP_FixityType fx, int prec, OP_TermContext tc)
+{    
+    int     numabs = 0;
+    Boolean pparen = PRINT_parenNeeded(OP_LAM_FIXITY,OP_LAM_PREC,tc,fx,prec);
+    PRINT_BVList tmpbvs;
+    int          tmpbvc = PRINT_bvcounter;
+    
+    if (pparen) PRINT_writeLParen(outStream);
+    while (DF_isLam(tmPtr)){
+        numabs += DF_lamNumAbs(tmPtr);
+        tmPtr = DF_termDeref(DF_lamBody(tmPtr));
+    }
+    PRINT_writeAbstBinders(outStream, numabs);
+    PRINT_writeTerm(outStream, tmPtr, OP_LAM_FIXITY,OP_LAM_PREC,OP_RIGHT_TERM);
+    if (pparen) PRINT_writeRParen(outStream);
+
+    while (numabs > 0) {
+      numabs--;
+      tmpbvs = PRINT_bvs;
+      PRINT_bvs = PRINT_bvs->next;
+      PRINT_cleanBV(tmpbvs);
+    } 
+    PRINT_bvcounter = tmpbvc;
+}      
+
+/****************************************************************************
+ *                      WRITING OUT AN APPLICATION                          *
+ *                                                                          *
+ * Note that it is assumed that nested application structures are flattened *
+ * during the full normalization process.                                   *
+ ****************************************************************************/
+/* Getting the fixity and precedence for the head of an application. 
+   Assume the pointer to the term head is already dereferenced. */
+static void PRINT_getHeadInfo(DF_TermPtr hdPtr, OP_FixityType *fx, int* prec)
+{
+    int cstInd;
+    switch (DF_termTag(hdPtr)) {
+    case DF_TM_TAG_CONST:
+        cstInd = DF_constTabIndex(hdPtr);
+        if (AM_cstName(cstInd)) {
+            *fx   = (OP_FixityType)AM_cstFixity(cstInd);
+            *prec = AM_cstPrecedence(cstInd);
+        } else {
+            *fx   = OP_NONE;
+            *prec = 0;
+        }
+        break;
+    case DF_TM_TAG_VAR:
+        *fx   = OP_NONE;
+        *prec = OP_MINPREC;
+        break;
+    case DF_TM_TAG_BVAR:
+        *fx   = OP_NONE;
+        *prec = OP_MINPREC;
+        break;
+    }
+}    
+        
+/* Writing out a term with a prefix operator as head; we use the knowledge
+that the operator must be a constant here and that the pointer to it is
+fully dereferenced */
+static void PRINT_writePrefixTerm(WordPtr outStream, DF_TermPtr head,
+                                  OP_FixityType opfx, int opprec,
+                                  OP_TermContext tc, OP_FixityType fx,int prec,
+                                  DF_TermPtr args)
+{
+    Boolean pparen = PRINT_parenNeeded(opfx, opprec, tc, fx, prec);
+    
+    if (pparen) PRINT_writeLParen(outStream);
+    PRINT_writeConst(outStream, head);
+    PRINT_writeSpace(outStream, 1);
+    PRINT_writeTerm(outStream, args, opfx, opprec, OP_RIGHT_TERM);
+    if (pparen) PRINT_writeRParen(outStream);
+}
+
+static void PRINT_writeInfixTerm(WordPtr outStream, DF_TermPtr head,
+                                 OP_FixityType opfx, int opprec, 
+                                 OP_TermContext tc, OP_FixityType fx, int prec,
+                                 DF_TermPtr args)
+{
+    Boolean pparen = PRINT_parenNeeded(opfx, opprec, tc, fx, prec);
+    if(pparen) PRINT_writeLParen(outStream);
+    PRINT_writeTerm(outStream, args, opfx, opprec, OP_LEFT_TERM);
+    PRINT_writeSpace(outStream, 1);
+    PRINT_writeConst(outStream, head);
+    PRINT_writeSpace(outStream, 1);
+    PRINT_writeTerm(outStream, args+1, opfx, opprec, OP_RIGHT_TERM);
+    if (pparen) PRINT_writeRParen(outStream);
+}                                  
+
+static void PRINT_writePostfixTerm(WordPtr outStream, DF_TermPtr head,
+                                   OP_FixityType opfx, int opprec, 
+                                   OP_TermContext tc,OP_FixityType fx,int prec,
+                                   DF_TermPtr args) 
+{
+    Boolean pparen = PRINT_parenNeeded(opfx, opprec, tc, fx, prec);
+    if(pparen) PRINT_writeLParen(outStream);
+    PRINT_writeTerm(outStream, args, opfx, opprec, OP_LEFT_TERM);
+    PRINT_writeSpace(outStream, 1);
+    PRINT_writeConst(outStream, head);
+    if (pparen) PRINT_writeRParen(outStream);
+}                                  
+
+/* Main routine for writing out an application term */
+static void PRINT_writeApp(WordPtr outStream, DF_TermPtr tmPtr, 
+                           OP_FixityType infx, int inprec, OP_TermContext tc)
+{   
+  
+    DF_TermPtr head   = DF_termDeref(DF_appFunc(tmPtr));
+    DF_TermPtr args   = DF_appArgs(tmPtr);
+    int        arity  = DF_appArity(tmPtr);
+    Boolean    pparen = PRINT_parenNeeded(OP_APP_FIXITY, OP_APP_PREC, tc, infx,
+                                          inprec);
+    OP_FixityType  fix;
+    int            prec;
+
+    HN_hnorm(tmPtr);
+    PRINT_getHeadInfo(AM_head, &fix, &prec);  
+    
+    switch(fix){
+    case OP_PREFIX: case OP_PREFIXR:
+      if (arity == 1) {
+	pparen = FALSE;
+	PRINT_writePrefixTerm(outStream, head, fix, prec, tc, infx, inprec,
+			      args);
+	
+       } else { 
+	 if (pparen) PRINT_writeLParen(outStream);
+	 PRINT_writePrefixTerm(outStream, head, fix, prec, OP_LEFT_TERM,
+			       OP_APP_FIXITY, OP_APP_PREC, args);
+       }
+      arity--; args++;
+      break;
+    case OP_INFIX: case OP_INFIXL: case OP_INFIXR:
+      if (arity == 2) {
+	pparen = FALSE;
+	PRINT_writeInfixTerm(outStream, head, fix, prec, tc, infx, inprec, 
+			     args);
+      } else {
+	if (pparen) PRINT_writeLParen(outStream);
+	PRINT_writeInfixTerm(outStream, head, fix, prec, OP_LEFT_TERM,
+			     OP_APP_FIXITY, OP_APP_PREC, args);
+      }
+      arity -= 2; args += 2;
+      break;
+    case OP_POSTFIX: case OP_POSTFIXL:
+      if (arity == 1) {
+	pparen = FALSE;
+	PRINT_writePostfixTerm(outStream, head, fix, prec, tc, infx,
+			       inprec, args);
+      }  else { 
+	if (pparen) PRINT_writeLParen(outStream);
+	PRINT_writePostfixTerm(outStream, head, fix, prec, OP_LEFT_TERM,
+			       OP_APP_FIXITY, OP_APP_PREC, args);
+      }
+      break;
+    case OP_NONE:
+      if (pparen) PRINT_writeLParen(outStream);
+      PRINT_writeTerm(outStream,head,OP_APP_FIXITY,OP_APP_PREC,OP_LEFT_TERM);
+      break;
+    } /*switch*/
+
+    /* print the arguments (if any) of the application */
+    while (arity > 0) {
+        PRINT_writeSpace(outStream, 1);
+        PRINT_writeTerm(outStream, args, OP_APP_FIXITY, OP_APP_PREC,
+			OP_RIGHT_TERM);
+        args++;
+        arity--;
+    }
+    if (pparen) PRINT_writeRParen(outStream);
+}
+
+
+/*****************************************************************************
+ * The main routine for writing out a term; this is called by the interface  *
+ * routines to do the real job of printing.                                  *
+ *****************************************************************************/
+static void PRINT_writeTerm(WordPtr outStream, DF_TermPtr tmPtr, 
+                            OP_FixityType infx, int inprec, OP_TermContext tc)
+{
+    tmPtr = DF_termDeref(tmPtr);
+    switch (DF_termTag(tmPtr)) {
+    case DF_TM_TAG_INT:     PRINT_writeInt(outStream, tmPtr);    break;
+    case DF_TM_TAG_FLOAT:   PRINT_writeFloat(outStream, tmPtr);  break;
+    case DF_TM_TAG_STR:     PRINT_writeString(outStream, tmPtr); break;
+    case DF_TM_TAG_STREAM:  PRINT_writeStream(outStream, tmPtr); break;
+    case DF_TM_TAG_CONST:   PRINT_writeConst(outStream, tmPtr);  break;
+    case DF_TM_TAG_VAR:     PRINT_writeFVar(outStream, tmPtr);   break;
+    case DF_TM_TAG_BVAR:    PRINT_writeBVar(outStream, tmPtr);   break;
+    case DF_TM_TAG_NIL:     PRINT_writeNil(outStream);           break;
+    case DF_TM_TAG_CONS:    
+        PRINT_writeCons(outStream, tmPtr, infx, inprec, tc);     break;
+    case DF_TM_TAG_LAM:     
+        PRINT_writeAbst(outStream, tmPtr, infx, inprec, tc);     break;
+    case DF_TM_TAG_APP:
+        PRINT_writeApp(outStream, tmPtr, infx, inprec, tc);      break;
+    } /* switch */    
+}
+
+
+/* Printing a term to a specified output stream; names will be invented for
+free variables if the boolean variable PRINT_names is set. */
+void PRINT_fPrintTerm(WordPtr outStream, DF_TermPtr tmPtr)
+{
+  HN_lnorm(tmPtr);
+  PRINT_writeTerm(outStream, tmPtr, OP_NONE, 0, OP_WHOLE_TERM);
+}
+
+/* Printing routine for debugging */
+void PRINT_printTerm(DF_TermPtr tmPtr)
+{
+    PRINT_fPrintTerm(STREAM_stdout, tmPtr);
+    STREAM_printf(STREAM_stdout, "\n");
+}
+
+/* printing an answer substitution pair */
+static void PRINT_printSubsPair(WordPtr outStream, int ind)
+{
+    DF_TermPtr tmPtr;
+    char *varName = 
+        MCSTR_toCString(DF_strDataValue(IO_freeVarTab[ind].varName));    
+
+    /* print the variable name if it is not an anonymous variable */
+    if (strcmp(varName, "_") != 0) {        
+        STREAM_printf(outStream, varName);
+        
+        /* Print the equals sign */
+        PRINT_writeEquals(outStream);
+        
+        /* Print the binding of the variable */
+        tmPtr = IO_freeVarTab[ind].rigdes;
+        HN_lnorm(tmPtr);
+        PRINT_writeTerm(outStream, tmPtr, OP_NONE, 0, OP_WHOLE_TERM);
+    }    
+}
+
+void PRINT_showAnswerSubs()
+{
+    int i;
+    
+    PRINT_names = TRUE;
+    
+    for (i = 0; i < PRINT_numQueryVars; i++) {
+        PRINT_printSubsPair(STREAM_stdout, i);
+        STREAM_printf(STREAM_stdout, "\n");
+    }
+}
+
+/* Printing a disagreement pair to a specified output stream */
+static void PRINT_printDPair(WordPtr outStream, DF_DisPairPtr dpair)
+{
+    DF_TermPtr tmPtr;
+    
+    PRINT_writeDPairStart(outStream);
+    
+    tmPtr = DF_disPairFirstTerm(dpair);
+    HN_lnorm(tmPtr);
+    PRINT_writeTerm(outStream, tmPtr, OP_NONE, 0, OP_WHOLE_TERM);
+    
+    PRINT_writeComma(outStream);
+    PRINT_writeSpace(outStream, 1);
+    
+    tmPtr = DF_disPairSecondTerm(dpair);
+    HN_lnorm(tmPtr);    
+    PRINT_writeTerm(outStream, tmPtr, OP_NONE, 0, OP_WHOLE_TERM);
+
+    PRINT_writeDPairEnd(outStream);
+}
+
+void PRINT_showDisAgreeList()
+{
+    DF_DisPairPtr liveList = AM_llreg;
+    
+    while (DF_isNEmpDisSet(liveList)) {
+        PRINT_printDPair(STREAM_stdout, liveList);
+        liveList = DF_disPairNext(liveList);
+        STREAM_printf(STREAM_stdout, "\n");
+    }    
+}
+
+void PRINT_setQueryFreeVariables()
+{
+    PRINT_numQueryVars = IO_freeVarTabTop;
+}
+
+/* Use this function to reset the top of the free variable table
+after a read; this is logical and also needed to avoid trying 
+to release print name space accidentally at some other point. */
+void PRINT_resetFreeVarTab()
+{
+  IO_freeVarTabTop = PRINT_numQueryVars;
+}
+
+
+void PRINT_resetPrintState()
+{
+    /* release space for term variables created during printing */
+    while (IO_freeVarTabTop > PRINT_numQueryVars){
+        IO_freeVarTabTop--;
+        free(IO_freeVarTab[IO_freeVarTabTop].varName);
+    }
+    
+    /* reset counters used in names of anonymous term and type variables */
+    PRINT_fvcounter = 1; 
+
+    /* free space for information created for local consts and reset counter */
+    PRINT_cleanCList();    
+    
+    /* free space for information created for bound vars and reset counter */
+    PRINT_cleanBVList();
+}
+
+Boolean PRINT_queryHasVars()
+{
+    int i = PRINT_numQueryVars - 1;
+    while (!(i < 0) && 
+           (strcmp(MCSTR_toCString(DF_strDataValue(IO_freeVarTab[i].varName)),
+                   "_") == 0)) 
+        i--;
+    
+    if (i < 0) return FALSE;
+    else return TRUE;
+    
+}