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, 1693 insertions, 0 deletions

diff --git a/src/runtime/c/teyjus/simulator/hopu.c b/src/runtime/c/teyjus/simulator/hopu.c
new file mode 100644
index 000000000..505eed6df
--- /dev/null
+++ b/src/runtime/c/teyjus/simulator/hopu.c
@@ -0,0 +1,1693 @@
+//////////////////////////////////////////////////////////////////////////////
+//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 hopu.c. This file contains the main routines implementing the      */
+/*  interpretive part of higher-order pattern unification.                  */
+/*                                                                          */
+/****************************************************************************/
+#ifndef HOPU_C
+#define HOPU_C
+
+#include "hopu.h"
+#include "mctypes.h"
+#include "dataformats.h"
+#include "hnorm.h"
+#include "abstmachine.h"
+#include "types.h"
+#include "trail.h"
+#include "../system/error.h"  
+#include "../system/memory.h" 
+
+#include <stdio.h>
+
+/* Unify types associated with constants.                                 */
+static void HOPU_typesUnify(DF_TypePtr tyEnv1, DF_TypePtr tyEnv2, int n)
+{
+    AM_pdlError(2*n);
+    AM_initTypesPDL();
+    TY_pushPairsToPDL((MemPtr)tyEnv1, (MemPtr)tyEnv2, n);
+    TY_typesUnify();
+}
+
+/* Return the dereference of the abstraction body of the given term.       */
+DF_TermPtr HOPU_lamBody(DF_TermPtr tmPtr)
+{
+    tmPtr = DF_termDeref(tmPtr);
+    while (DF_isLam(tmPtr)) tmPtr = DF_termDeref(DF_lamBody(tmPtr));
+    return tmPtr;
+}
+
+/***************************************************************************/ 
+/* Globalize functions needed for HOPU_patternUnidyPair                    */
+/***************************************************************************/
+
+/* Globalize a rigid term.                                                 */
+/* If the term pointer is not one referring to a heap address, the atomic  */
+/* content is then copied onto the current top of heap; the term pointer   */
+/* is updated to the new heap term.                                        */
+static DF_TermPtr HOPU_globalizeRigid(DF_TermPtr rPtr)
+{
+    if (AM_nHeapAddr((MemPtr)rPtr)) {//rPtr must refer to const (no type), int,
+                                     //float, str, (stream), nil, cons
+        MemPtr nhreg = AM_hreg + DF_TM_ATOMIC_SIZE;
+        AM_heapError(nhreg);
+        DF_copyAtomic(rPtr, AM_hreg);
+        rPtr = (DF_TermPtr)AM_hreg;
+        AM_hreg = nhreg;
+    }
+    return rPtr;
+}
+
+/* Globalize a rigid term and make a variable binding.                     */
+/* If the term pointer to the rigid term is not one referring to a heap    */
+/* address, its atomic content is then copied into the variable to be bound*/
+/* Otherwise, the variable is made a reference to the rigid term.          */
+void HOPU_globalizeCopyRigid(DF_TermPtr rPtr, DF_TermPtr vPtr)
+{
+    if (AM_nHeapAddr((MemPtr)rPtr)) //rPtr must refer to rigid atomic term
+        DF_copyAtomic(rPtr, (MemPtr)vPtr);
+    else DF_mkRef((MemPtr)vPtr, rPtr); //rPtr could also be app 
+}        
+  
+/* Globalize a flex term.                                                   */
+/* If the term pointer is one referring to a stack address, (in which case  */
+/* the flex term must be a free variable itself), the atomic content is     */
+/* copied onto the current top of heap; the free variable on stack is then  */
+/* bound to the new heap term, and the binding is trailed if necessary; the */
+/* term pointer is updated to the new heap term.                            */  
+DF_TermPtr HOPU_globalizeFlex(DF_TermPtr fPtr)
+{
+    if (AM_stackAddr((MemPtr)fPtr)) {//fPtr must be a reference to var
+        MemPtr nhreg = AM_hreg + DF_TM_ATOMIC_SIZE;
+        AM_heapError(nhreg);
+        DF_copyAtomic(fPtr, AM_hreg);
+        TR_trailETerm(fPtr);
+        DF_mkRef((MemPtr)fPtr, (DF_TermPtr)AM_hreg);
+        fPtr = (DF_TermPtr)AM_hreg;
+        AM_hreg = nhreg;
+    }   
+    return fPtr;
+}
+
+/***************************************************************************/
+/* Explicit eta expansion (on a rigid term)                                */
+/***************************************************************************/
+
+/* Eta expands a rigid term whose term pointer and decomposition are given */
+/* by arguments. The new lambda body is returned. (It is unnecessary to    */
+/* create a new lambda term for the abstractions in the front of the eta   */
+/* expanded form. Note that the term head and argument vector are updated  */
+/* as side-effect.                                                         */
+/* Note globalization on the term head is always performed and no          */
+/* specialized version of this function is provided based on the assumption*/
+/* that explicit eta-expansion is rarely needed.                           */
+static DF_TermPtr HOPU_etaExpand(DF_TermPtr *h, DF_TermPtr *args, int nargs, 
+                                 int nabs)
+{
+    DF_TermPtr hPtr = *h, oldArgs = *args, rtPtr;
+    MemPtr     suspLoc;  //where susps are to be created
+    int        newArity = nargs + nabs;
+    if (DF_isBV(hPtr)){  //lift index by nabs if the head is a bound variable
+        int ind = DF_bvIndex(hPtr) + nabs;
+        AM_embedError(ind);
+        AM_heapError(AM_hreg + DF_TM_ATOMIC_SIZE);
+        *h = hPtr =(DF_TermPtr)AM_hreg; //update head pointer
+        DF_mkBV(AM_hreg,ind);
+        AM_hreg += DF_TM_ATOMIC_SIZE;
+    } else 
+        //always perform globalization; eta expansion is rarely needed 
+        *h = hPtr = HOPU_globalizeRigid(hPtr); 
+
+    AM_arityError(newArity);
+    AM_heapError(AM_hreg + nargs * DF_TM_SUSP_SIZE + newArity*DF_TM_ATOMIC_SIZE
+                 + DF_TM_APP_SIZE);
+    suspLoc = AM_hreg;
+    AM_hreg += nargs * DF_TM_SUSP_SIZE;  //allocate space for nargs suspensions
+    rtPtr   = (DF_TermPtr)AM_hreg;       //new application
+    DF_mkApp(AM_hreg, newArity, hPtr, (DF_TermPtr)(AM_hreg + DF_TM_APP_SIZE));
+    AM_hreg += DF_TM_APP_SIZE;
+    *args = (DF_TermPtr)AM_hreg;         //update arg vector pointer
+    for (; nargs > 0; nargs--){//create suspensions over original arguments 
+        DF_mkSusp(suspLoc, 0, nabs, DF_termDeref(oldArgs), DF_EMPTY_ENV);
+        DF_mkRef(AM_hreg, (DF_TermPtr)suspLoc);
+        suspLoc += DF_TM_SUSP_SIZE; AM_hreg += DF_TM_ATOMIC_SIZE; 
+        oldArgs = (DF_TermPtr)(((MemPtr)oldArgs) + DF_TM_ATOMIC_SIZE);
+    }
+    for (; nabs > 0; nabs--){//create de Bruijn indices from #nabs to #1
+        DF_mkBV(AM_hreg, nabs); 
+        AM_hreg += DF_TM_ATOMIC_SIZE;
+    }
+    return rtPtr;
+}
+
+/***************************************************************************/
+/*                    PATTERN RECOGNITION                                  */
+/*                                                                         */
+/* Auxiliary functions for recognizing LLambda pattens for flexible terms. */
+/***************************************************************************/
+/* Whether a bound variable occurs in the given arguments.                 */
+/* It is assumned that the given arguments can only contain bound variables*/
+/* and constants.                                                          */
+static Boolean HOPU_uniqueBV(int bvInd, DF_TermPtr args, int n)
+{
+    DF_TermPtr tPtr;
+    for ( ;  n > 0 ; n-- ){
+        tPtr = DF_termDeref(args);
+        if (DF_isBV(tPtr) && (bvInd == DF_bvIndex(tPtr))) return FALSE;
+        //otherwise different bv or constant, check the next
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }
+    return TRUE;
+}
+
+/* Whether a constant occurs in the given arguments.                       */
+/* It is assumned that the given arguments can only contain bound variables*/
+/* and constants.                                                          */
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static Boolean HOPU_uniqueConst(DF_TermPtr cPtr, DF_TermPtr args, int n)
+{
+    DF_TermPtr tPtr;
+    for ( ; n > 0 ; n--){
+        tPtr = DF_termDeref(args);
+        if (DF_isConst(tPtr) && DF_sameConsts(tPtr, cPtr)) {
+            if (DF_isTConst(tPtr)) {
+                EM_TRY { 
+                    HOPU_typesUnify(DF_constType(tPtr), DF_constType(cPtr), 
+                                    AM_cstTyEnvSize(DF_constTabIndex(cPtr)));
+                } EM_CATCH {
+                    if (EM_CurrentExnType == EM_FAIL) {
+                        AM_resetTypesPDL();//remove tys from pdl for ty unif
+                        return FALSE;
+                    } else EM_RETHROW();
+                }
+            } else  return FALSE; 
+        } //otherwise different constant or bv, check the next
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    } //for loop
+    return TRUE;
+}
+
+/* Checking whether the argments of the head normal form given by registers*/
+/* AM_argVec, AM_numArgs and AM_numAbs are those of an eta-expanded form.  */
+/* Specifically, the arguments are attempted to match de Bruijn indices    */
+/* #n ... #1, where n is the current value of AM_numAbs.                   */ 
+/* It is assumed that the argument vector is not empty.                    */
+static Boolean HOPU_isEtaExpArgs()
+{
+    if (AM_numArgs != AM_numAbs) return FALSE;
+    else {
+        int        i      = AM_numAbs;
+        Boolean    match  = TRUE;
+        DF_TermPtr oneArg = AM_argVec;
+        DF_TermPtr head   = AM_head;
+        while (match && (i > 0)){
+            HN_hnorm(oneArg);
+            if (AM_numArgs == 0) 
+                match = ((AM_numArgs == 0) && DF_isBV(AM_head) &&
+                         (DF_bvIndex(AM_head) == i));
+            else 
+                match = (DF_isBV(AM_head) && (DF_bvIndex(AM_head)-AM_numAbs==i)
+                         && HOPU_isEtaExpArgs());
+            oneArg = (DF_TermPtr)(((MemPtr)oneArg + DF_TM_ATOMIC_SIZE));
+            i--;
+        }
+        AM_head = head;
+        return match;
+    }
+}
+
+/* Checking whether the arguments of a flexible term satisfy with the      */
+/* LLambda pattern with respect to the universe count of its flex head.    */
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static Boolean HOPU_isLLambda(int uc, int nargs, DF_TermPtr args)
+{
+    if (nargs == 0) return TRUE;
+    else {
+        int i;
+        DF_TermPtr myArgs = args;
+        for (i = 0; i < nargs; i++){
+            HN_hnorm(args);
+            if (AM_numArgs == 0) {
+                if (AM_numAbs != 0) return FALSE; //abstraction
+                if (DF_isBV(AM_head)) {           //bound variable
+                    if (!HOPU_uniqueBV(DF_bvIndex(AM_head), myArgs, i))
+                        return FALSE;
+                } else if (DF_isConst(AM_head)) { //constant
+                    if (!(uc < DF_constUnivCount(AM_head) && 
+                          HOPU_uniqueConst(AM_head, myArgs, i))) return FALSE;
+                } else return FALSE;              //other sort of terms
+            } else { //AM_numArgs != 0
+                if (DF_isBV(AM_head)) {           //bound variable head
+                    int dbInd = DF_bvIndex(AM_head) - AM_numAbs; //eta-norm
+                    if (dbInd > 0 && HOPU_uniqueBV(dbInd, myArgs, i) &&
+                        HOPU_isEtaExpArgs()) {
+                        TR_trailHTerm(args);
+                        DF_mkBV((MemPtr)args, dbInd);
+                    } else return FALSE;
+                } else { //!(DF_isBV(AM_head))
+                    if (DF_isConst(AM_head)) {    //constant head
+                        if (uc < DF_constUnivCount(AM_head) && 
+                            HOPU_uniqueConst(AM_head, myArgs, i) &&
+                            HOPU_isEtaExpArgs()) {
+                            TR_trailHTerm(args);
+                            if (DF_isTConst(AM_head)) 
+                                DF_mkRef((MemPtr)args, AM_head);
+                            else DF_copyAtomic(AM_head, (MemPtr)args);
+                        } else return FALSE;
+                    } else return FALSE;          //other sort of terms
+                }       //!(DF_isBV(AM_head))
+            }        //AM_numArgs != 0
+            args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+        } //for loop
+        return TRUE;
+    } //nargs != 0
+}
+
+/***************************************************************************/
+/*                            BINDING                                      */
+/*                                                                         */
+/* Attempt to find bindings for free variables (counter part of mksubst in */
+/* the sml pattern unfication code).                                       */
+/***************************************************************************/
+/* A flag denoting whether new structure is created during the process of  */
+/* finding substitutions.                                                  */
+Boolean HOPU_copyFlagGlb = FALSE;
+
+/* Return a non-zero index of a bound variable appears in a list of        */
+/* arguments. Note the index is the position from the right and the        */
+/* embedding level is taken into account.                                  */
+static int HOPU_bvIndex(int dbInd, DF_TermPtr args, int nargs, int lev)
+{   
+    int ind;
+    dbInd -= lev;
+    for (ind = nargs; ind > 0; ind--){
+        DF_TermPtr tPtr = DF_termDeref(args);
+        if (DF_isBV(tPtr) && (dbInd == DF_bvIndex(tPtr))) return (ind+lev);
+        //otherwise try the next
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }
+    return 0; //not found
+}
+
+/* Return a non-zero index if a constant appears in a list of arguments.   */
+/* Note the index is the position from the right and the embedding level   */
+/* is taken into account.                                                  */
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static int HOPU_constIndex(DF_TermPtr cPtr, DF_TermPtr args, int nargs, int lev)
+{
+    int ind;
+    for (ind = nargs; ind > 0; ind--){
+      DF_TermPtr tPtr = DF_termDeref(args);
+      if (DF_isConst(tPtr) && DF_sameConsts(tPtr, cPtr)) {
+	if (DF_isTConst(tPtr)) {
+	  Boolean found = FALSE;
+	  EM_TRY { 
+	    HOPU_typesUnify(DF_constType(tPtr), DF_constType(cPtr), 
+			    AM_cstTyEnvSize(DF_constTabIndex(cPtr)));
+	    found = TRUE;
+	  } EM_CATCH {//remove types added for ty unif from the PDL
+	    if (EM_CurrentExnType == EM_FAIL)  AM_resetTypesPDL();
+	    else EM_RETHROW();
+	  }
+	  if (found) return (ind+lev);
+	} else return (ind+lev);  //cPtr does not have type associated
+      } //otherwise try the next
+      args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }
+    return 0; //not found
+}
+
+/***************************************************************************/
+/*                 BINDING FOR FLEX-FLEX                                   */
+/*                                                                         */
+/* Auxiliary functions for solving flex-flex pairs.                        */
+/* Non-LLambda pairs are delayed onto the disagreement list.               */
+/***************************************************************************/
+
+/* Collect raising components for internal variable in the LLambda case    */
+/* when it is known it has a higher universe index than the outside llambda*/
+/* variable.                                                               */
+/* It is assumned that the incoming argument vector has a size larger than */
+/* zero.                                                                   */
+/* As a result of this process, segments of the argument vectors for both  */
+/* variables are decided. That for the internal variable is created on the */
+/* current top of heap, while that for the outside variable, each          */
+/* argument of which must be a de Bruijn index, is recorded into an integer*/
+/* array which is set by side-effect.                                      */
+/* The number returned by this procedure is the length of both of the      */
+/* argument vector segements. Raising occured when this number is non-zero.*/
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static int HOPU_raise(int varuc, DF_TermPtr args, int nargs, int emblev, 
+                      int *args11)
+{
+    int numRaised = 0;   //number of args that have been raised
+    AM_heapError(AM_hreg + nargs * DF_TM_ATOMIC_SIZE);//max possible size
+    for (; nargs > 0; nargs--){
+        DF_TermPtr tmPtr = DF_termDeref(args);
+        if (DF_isConst(tmPtr) && (DF_constUnivCount(tmPtr) <= varuc)){
+            args11[numRaised] = nargs + emblev;               //args11        
+            if (DF_isTConst(tmPtr)) DF_mkRef(AM_hreg, tmPtr); //args21
+            else DF_copyAtomic(tmPtr, AM_hreg);
+            AM_hreg += DF_TM_ATOMIC_SIZE;
+            numRaised++;
+        }
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }        
+    return numRaised;
+} 
+
+
+/* Generate the indices for items not to be pruned when the internal       */
+/* variable is known to have a universe index greater than that of the     */
+/* external one.                                                           */
+/* It is assumned that arg vector of the internal flex term has a size     */
+/* larger than  zero.                                                      */
+/* As a result of this process, segments of the argument vectors for both  */
+/* variables are decided. That for the internal variable is created on the */
+/* current top of heap, while that for the outside variable, each          */
+/* argument of which must be a de Bruijn index, is recorded into an integer*/
+/* array which is set by side-effect.                                      */
+/* The number returned by this procedure is the length of both of the      */
+/* argument vector segements. Pruning occured when this number is smaller  */
+/* than the size of the arg vector of the internal term.                   */
+static int HOPU_prune(DF_TermPtr args1, int nargs1, DF_TermPtr args2, 
+                      int nargs2, int emblev, int *args12)
+{
+
+    int numNotPruned = 0;
+    AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE);//max possible size
+    for (; nargs2 > 0; nargs2--){
+        DF_TermPtr tmPtr = DF_termDeref(args2);
+        if (DF_isConst(tmPtr)) {
+            int ind = HOPU_constIndex(tmPtr, args1, nargs1, emblev);
+            if (ind > 0) { 
+                args12[numNotPruned] = ind;                   //args12 
+                DF_mkBV(AM_hreg, nargs2);                     //args22
+                AM_hreg += DF_TM_ATOMIC_SIZE;
+                numNotPruned ++;
+                HOPU_copyFlagGlb = TRUE;
+            } //ind == 0 the argument is pruned 
+        } else {//bv
+            int ind = DF_bvIndex(tmPtr);
+            if (ind > emblev) {
+                int newind = HOPU_bvIndex(ind, args1, nargs1, emblev);
+                if (newind > 0) {
+                    args12[numNotPruned] = newind;            //args12
+                    DF_mkBV(AM_hreg, nargs2);                 //args22
+                    AM_hreg += DF_TM_ATOMIC_SIZE;
+                    numNotPruned ++;
+                    if (ind != newind) HOPU_copyFlagGlb = TRUE; 
+                } //newind == 0 the argument is pruned
+            } else {//ind <= lev
+                args12[numNotPruned] = ind;                   //args12
+                DF_mkBV(AM_hreg, nargs2);                     //args22
+                AM_hreg += DF_TM_ATOMIC_SIZE;
+                numNotPruned ++;
+            }
+        }       //bv
+        args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
+    } //for loop
+    return numNotPruned;
+} 
+
+/* When the index of the internal variable is less than or equal to that   */ 
+/* of the external one in the LLambda case, we have to raise the outside   */
+/* variable over those constants in the internal list that have smaller    */
+/* index and we have to prune other constants and bound variables in this  */
+/* list that are not shared.                                               */
+/* It is assumned that the arg vector of the internal flex term has a size */
+/* larger than zero.                                                       */
+/* As a result of this process, the argument vectors for both  variables   */
+/* are decided. That for the outside variable is created on the current    */
+/* top of heap, while that for the internal variable, each argument of     */
+/* which must be a de Bruijn index, is recorded into an integer array which*/
+/* is set by side-effect.                                                  */
+/* The number returned by this procedure is the length of both of the      */
+/* argument vectors. Pruning occured when this number is smaller than the  */
+/* size of the arg vector of the internal term.                            */
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static int HOPU_pruneAndRaise(DF_TermPtr args1, int nargs1, DF_TermPtr args2,
+                              int nargs2, int emblev, int *args)
+{
+    int numNotPruned = 0;    
+    AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE); //max possible size
+    for (; nargs2 > 0; nargs2 --){
+        DF_TermPtr tmPtr = DF_termDeref(args2);
+        if (DF_isBV(tmPtr)){
+            int ind = DF_bvIndex(tmPtr);
+            if (ind > emblev) {
+                int newind = HOPU_bvIndex(ind, args1, nargs1, emblev);
+                if (newind > 0) {
+                    DF_mkBV(AM_hreg, newind);         //args for outside var
+                    AM_hreg += DF_TM_ATOMIC_SIZE;
+                    args[numNotPruned] = nargs2;      //args for internal var 
+                    numNotPruned ++;
+                    if (ind != newind) HOPU_copyFlagGlb = TRUE;
+                } // newind == 0, the argument is prubed
+            } else { //ind <= emblev
+                DF_mkBV(AM_hreg, ind);                //args for outside var
+                AM_hreg += DF_TM_ATOMIC_SIZE;
+                args[numNotPruned] = nargs2;          //args for internal var
+                numNotPruned ++;
+            }
+        } else { //tmPtr is const
+            if (DF_constUnivCount(tmPtr) > AM_adjreg){                
+                int ind = HOPU_constIndex(tmPtr, args1, nargs1, emblev); 
+                if (ind > 0) {
+                    DF_mkBV(AM_hreg, ind);            //args for outside var
+                    AM_hreg += DF_TM_ATOMIC_SIZE;
+                    args[numNotPruned] = nargs2;      //args for internal var
+                    numNotPruned ++;
+                    HOPU_copyFlagGlb = TRUE;
+                } //else ind = 0, the argument is pruned  
+            } else { //const uc <= AM_adjreg
+                if (DF_isTConst(tmPtr)) DF_mkRef(AM_hreg, tmPtr);//args out var
+                else DF_copyAtomic(tmPtr, AM_hreg);
+                AM_hreg += DF_TM_ATOMIC_SIZE;
+                args[numNotPruned] = nargs2;          //args for internal var
+                numNotPruned ++;
+            }
+        }
+        args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
+    } //for loop
+    return numNotPruned;
+} 
+
+/* Generating the arguments of a pruning substitution for the case when    */
+/* when trying to unify two flexible terms of the form                     */
+/*             (F a1 ... an) = lam(k, (F b1 ... bm))                       */
+/* The resulted argument vector is created on the current top of heap, and */
+/* the integer returned by this procedure is the length of the argument    */
+/* vector resulted from pruning. Pruning takes place if this value is      */
+/* smaller that nargs2.                                                    */
+/* It is assumed that the sum of n and k is the same as m.                 */
+/* CHANGES have to be made here if the semantics of local constants are    */
+/* changed with respect to polymorphism.                                   */
+static int HOPU_pruneSameVar(DF_TermPtr args1, int nargs1, DF_TermPtr args2,
+                             int nargs2, int lev)
+{
+    if (nargs2 == 0) return 0;
+    else {
+        int numNotPruned = 0;
+        DF_TermPtr tPtr2;
+        AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE); //max possible size
+        nargs1 = nargs2 - nargs1; //reused nargs1
+        for (; nargs2 > nargs1; nargs2 --){
+            DF_TermPtr tPtr1 = DF_termDeref(args1);
+            tPtr2 = DF_termDeref(args2);
+            if (DF_isBV(tPtr1)){
+                int ind = DF_bvIndex(tPtr1) + lev;
+                if (DF_isBV(tPtr2) && (ind == DF_bvIndex(tPtr2))){
+                    DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
+                    numNotPruned++;
+                    if (nargs2 != ind) HOPU_copyFlagGlb = TRUE;
+                } //else this argument is pruned
+            } else {// tPtr1 is a constant
+                if (DF_isConst(tPtr2) && DF_sameConsts(tPtr1, tPtr2)){
+                    if (DF_isTConst(tPtr2)) {
+		      EM_TRY {
+                        HOPU_typesUnify(DF_constType(tPtr1),DF_constType(tPtr2),
+					AM_cstTyEnvSize(DF_constTabIndex(tPtr1)));
+                        DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
+                        numNotPruned++;
+                        HOPU_copyFlagGlb = TRUE;
+		      } EM_CATCH {//remove tys for type unif from the PDL
+			if (EM_CurrentExnType == EM_FAIL) 
+			  AM_resetTypesPDL();        
+			else EM_RETHROW();
+		      } //EM_catch
+                    } else {//no type association
+		      DF_mkBV(AM_hreg, nargs2); AM_hreg+=DF_TM_ATOMIC_SIZE;
+		      numNotPruned++;
+		      HOPU_copyFlagGlb = TRUE;
+                    }
+                }//else pruned 
+            }       //tPtr1 is a constant
+            args1 = (DF_TermPtr)(((MemPtr)args1) + DF_TM_ATOMIC_SIZE);
+            args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
+        } //for (; nargs2 > nargs1; nargs2--)
+        for (; nargs2 > 0; nargs2--){     
+            tPtr2 = DF_termDeref(args2);
+            if (DF_isBV(tPtr2) && (DF_bvIndex(tPtr2) == nargs2)){
+                DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
+                numNotPruned++;
+            } //else pruned
+            args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
+        } //for (; nargs2 > 0; nargs2--)
+        return numNotPruned;
+    } //nargs2 != 0
+}
+
+/* Push a new free variable with given universe count onto the current heap */  
+/* top.                                                                     */
+static void HOPU_pushVarToHeap(int uc)
+{
+    MemPtr newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
+    AM_heapError(newhtop);
+    DF_mkVar(AM_hreg, uc);
+    AM_hreg = newhtop;
+}
+
+/* Perform substitution to realize pruning and raising for an internal     */
+/* variable in the LLambda situation when the variable has an index greater*/
+/* than that of the outside one                                            */
+/* This procedure is also used to perform substitution for flex-flex pairs */
+/* with same variable heads in the LLambda situation.                      */
+static void HOPU_mkPandRSubst(DF_TermPtr hPtr, DF_TermPtr args, int nargs,
+                              DF_TermPtr vPtr, int nabs)
+{
+    TR_trailTerm(vPtr); AM_bndFlag = ON;
+    if (nargs == 0) {
+        if (nabs == 0) DF_mkRef((MemPtr)vPtr, hPtr);
+        else DF_mkLam((MemPtr)vPtr, nabs, hPtr);
+    } else { //nargs > 0
+        DF_TermPtr tPtr = (DF_TermPtr)AM_hreg;
+        AM_heapError(AM_hreg + DF_TM_APP_SIZE);
+        AM_arityError(nargs);
+        DF_mkApp(AM_hreg, nargs, hPtr, args);  //application body
+        AM_hreg += DF_TM_APP_SIZE;
+        AM_embedError(nabs);
+        if (nabs == 0) DF_mkRef((MemPtr)vPtr, tPtr);
+        else DF_mkLam((MemPtr)vPtr, nabs, tPtr);
+    }
+}
+
+/* Perform substitution to realize pruning and raising for an internal     */
+/* variable in the LLambda situation when the variable has an index smaller*/
+/* than or equal to that of the outside one                                */
+/* The arguments of the substitution which should be de Bruijn indices     */ 
+/* are given by an integer array.                                          */
+static void HOPU_mkPrunedSubst(DF_TermPtr hPtr, int *args, int nargs, 
+                               DF_TermPtr vPtr, int nabs)
+{
+    AM_bndFlag = ON;
+    TR_trailTerm(vPtr);
+    if (nargs == 0) {
+        if (nabs == 0) DF_mkRef((MemPtr)vPtr, hPtr);
+        else DF_mkLam((MemPtr)vPtr, nabs, hPtr);
+    } else { //nargs > 0;
+        DF_TermPtr argvec = (DF_TermPtr)AM_hreg, appPtr;
+        int i;
+        AM_heapError(AM_hreg + DF_TM_APP_SIZE + nargs * DF_TM_ATOMIC_SIZE);
+        for (i = 0; i < nargs; i++){//commit bvs in args onto heap
+            DF_mkBV(AM_hreg, args[i]);
+            AM_hreg += DF_TM_ATOMIC_SIZE;
+        }
+        appPtr = (DF_TermPtr)AM_hreg;
+        DF_mkApp(AM_hreg, nargs, hPtr, argvec);
+        AM_hreg += DF_TM_APP_SIZE;
+        if (nabs == 0) DF_mkRef((MemPtr)vPtr, appPtr);
+        else DF_mkLam((MemPtr)vPtr, nabs, appPtr);
+    }
+}
+
+/* Generating the partial structure of a substitution to realize pruning   */ 
+/* and raising for an outside variable in the LLambda situation when the   */
+/* variable has an index smaller than that of the internal one.            */
+/* The arguments of the susbsitution consists of two segments of de Burijn */
+/* indices, which are given by two integer arrays respectively.            */
+static DF_TermPtr HOPU_mkPandRTerm(DF_TermPtr hPtr, int args1[], int nargs1,
+                                   int args2[], int nargs2)
+{
+    if ((nargs1 == 0) && (nargs2 == 0)) return hPtr;
+    else {
+        DF_TermPtr args = (DF_TermPtr)AM_hreg, rtPtr;
+        int nargs = nargs1 + nargs2;   //new arity (non-zero)
+        int i;
+        AM_arityError(nargs);
+        AM_heapError(AM_hreg + DF_TM_APP_SIZE + nargs * DF_TM_ATOMIC_SIZE);
+        for (i = 0; i < nargs1 ; i++){ //commit bvs in a11 onto heap 
+            DF_mkBV(AM_hreg, args1[i]);
+            AM_hreg += DF_TM_ATOMIC_SIZE;
+        }
+        for (i = 0; i < nargs2 ; i++){ //commit bvs in a12 onto heap
+            DF_mkBV(AM_hreg, args2[i]);
+            AM_hreg += DF_TM_ATOMIC_SIZE;
+        }
+        rtPtr = (DF_TermPtr)AM_hreg;
+        DF_mkApp(AM_hreg, nargs, hPtr, args);
+        AM_hreg += DF_TM_APP_SIZE;
+        return rtPtr;
+    }
+}
+
+/* Generating the partial structure of a substitution to realize pruning   */ 
+/* and raising for an internal variable in the LLambda situation when the  */
+/* variable has an index greater than or equal to that of the outside one. */
+static DF_TermPtr HOPU_mkPrunedTerm(DF_TermPtr hPtr, DF_TermPtr args, int nargs)
+{
+    if (nargs == 0) return hPtr;
+    else {
+        DF_TermPtr rtPtr = (DF_TermPtr)AM_hreg;
+        AM_heapError(AM_hreg + DF_TM_APP_SIZE);
+        DF_mkApp(AM_hreg, nargs, hPtr, args);
+        AM_hreg += DF_TM_APP_SIZE;
+        return rtPtr;
+    }
+}
+
+/* Find the (partial) structure of the substitution for a flex head of a      */
+/* LLambda term corresponding to an internal flex term which is known to be   */
+/* LLambda. The internal free variable is bound to a proper substitution  as  */
+/* side-effect.
+/* The arguments of this procedure are:                                       */
+/*  args1 : reference to the argument vector of the outside flex term         */
+/*  nargs1: number of arguments of the outside flex term                      */
+/*  uc    : universe count of the internal free variable                      */
+/*  tPtr2 : refers to the dereference of ABSTRACTION BODY of the internal     */
+/*          flex term                                                         */
+/*  fhPtr : refers to the head of the internal flex term                      */
+/*  args2 : refers to the argument vector of the internal flex term           */
+/*  nargs2: number of arguments of the internal flex term                     */
+/*  lev   : the abstraction context of the internal flex term                 */
+/* Note that the outside free variable and its universe count are assumed to  */
+/* be given by the global variables (registers) AM_vbbreg and AM_adjreg.      */
+static DF_TermPtr HOPU_flexNestedLLambda(DF_TermPtr args1, int nargs1, int uc,
+                   DF_TermPtr tPtr2, DF_TermPtr fhPtr, DF_TermPtr args2, 
+                   int nargs2, int lev)
+{
+    DF_TermPtr bnd;  //(partial) binding for the outside free var 
+    MemPtr     oldhtop = AM_hreg;
+    DF_TermPtr heapArgs = (DF_TermPtr)AM_hreg;
+    if (AM_adjreg < uc){
+        int *args11 = NULL, *args12 = NULL; //hold args of bnd of the outside v
+        int nargs11 = 0,    nargs12 = 0;
+        if (nargs1 != 0) {
+            args11 = (int*)EM_malloc(nargs1 * sizeof(int));
+            nargs11 = HOPU_raise(uc, args1, nargs1, lev, args11);
+        }
+        if (nargs2 != 0) {
+            args12 = (int*)EM_malloc(nargs2 * sizeof(int));
+            nargs12 = HOPU_prune(args1, nargs1, args2, nargs2, lev, args12); 
+        }
+        if ((nargs11 == 0) && (nargs12 == nargs2)) {//neither raised nor pruned
+            AM_hreg = oldhtop; //the internal free var remains unbound          
+            TR_trailTerm(fhPtr); AM_bndFlag = ON;
+            DF_modVarUC(fhPtr, AM_adjreg);
+            if (HOPU_copyFlagGlb)
+                bnd = HOPU_mkPandRTerm(fhPtr, args11, nargs11, args12, nargs12);
+            else bnd = tPtr2;
+        } else {                                    //raised or pruned
+            DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
+            HOPU_pushVarToHeap(AM_adjreg);
+            HOPU_mkPandRSubst(newVar, heapArgs, nargs11+nargs12, fhPtr, nargs2);
+            bnd = HOPU_mkPandRTerm(newVar, args11, nargs11, args12, nargs12);
+            HOPU_copyFlagGlb = TRUE;
+        }
+        if (nargs1 != 0) free(args11); if (nargs2 != 0) free(args12);        
+    } else { //AM_adjreg >= uc
+        int *newargs2 = NULL;
+        int nnewargs2 = 0;
+        if (nargs2 != 0) {
+            newargs2 = (int*)EM_malloc(nargs2 * sizeof(int));
+            nnewargs2 = HOPU_pruneAndRaise(args1,nargs1,args2,nargs2,lev,
+                                           newargs2);
+        }
+        if (nnewargs2 == nargs2){//not pruned
+            if (HOPU_copyFlagGlb)
+                bnd = HOPU_mkPrunedTerm(fhPtr, heapArgs, nnewargs2);
+            else { AM_hreg = oldhtop; bnd = tPtr2; }
+        } else {                 //pruned            
+            DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
+            HOPU_pushVarToHeap(uc);
+            HOPU_mkPrunedSubst(newVar, newargs2, nnewargs2, fhPtr, nargs2);
+            bnd = HOPU_mkPrunedTerm(newVar, heapArgs, nnewargs2);
+            HOPU_copyFlagGlb = TRUE;
+        }
+        if (nargs2 != 0) free(newargs2);
+    }        //AM_adjreg >= uc
+    return bnd;
+}
+
+/* Checking the arguments of a flex (non-LLambda) term to see whetehr a    */
+/* free variable same as that currently in the AM_vbbreg register, a free  */
+/* variable with higher univ count than that currently in the AM_adjreg    */
+/* register, a constant with higher univ count than that currently in      */
+/* AM_adjreg, or a de Bruijn index bound by abstractions over the variable */
+/* for which a substitution is being constructed occurs.                   */
+/* If one of the situations occurs, exception is raised.                   */   
+static void HOPU_flexCheck(DF_TermPtr args, int nargs, int emblev)
+{
+    for (; nargs > 0; nargs --){
+        int nemblev;  
+        HN_hnorm(args);
+        nemblev = emblev + AM_numAbs;
+        if (AM_rigFlag){
+            if (DF_isBV(AM_head)) {
+                if (DF_bvIndex(AM_head) > nemblev) EM_THROW(EM_FAIL);
+            } else {
+                if (DF_isConst(AM_head)&&(DF_constUnivCount(AM_head)>AM_adjreg))
+                    EM_THROW(EM_FAIL);
+            } //otherwise succeeds
+        } else { //AM_rigFlag == FALSE
+            if ((AM_vbbreg == AM_head) || (DF_fvUnivCount(AM_head)>AM_adjreg))
+                EM_THROW(EM_FAIL);
+        }
+        HOPU_flexCheck(AM_argVec, AM_numArgs, nemblev);
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }
+}
+
+/* This version of flexCheckC is needed in the compiled form of pattern      */
+/* unification. The essential difference from the other version is that the  */
+/* variable being bound is already partially bound to a structure.           */
+/* The difference from the other procedure is the head normalization         */
+/* procedure invoked is one performs the occurs checking on partially bound  */
+/* variables                                                                 */ 
+static void HOPU_flexCheckC(DF_TermPtr args, int nargs, int emblev)
+{
+    for (; nargs > 0; nargs--){
+        int nemblev;
+        HN_hnormOcc(args);
+        nemblev = emblev + AM_numAbs;
+        if (AM_rigFlag) {
+            if (DF_isBV(AM_head)) {
+                if (DF_bvIndex(AM_head) > nemblev) EM_THROW(EM_FAIL);
+            } else {
+                if (DF_isConst(AM_head)&&(DF_constUnivCount(AM_head)>AM_adjreg))
+                    EM_THROW(EM_FAIL);
+            } //otherwise succeeds
+        } else  //AM_rigFlag == FALSE
+            if (DF_fvUnivCount(AM_head) > AM_adjreg) EM_THROW(EM_FAIL);
+
+        HOPU_flexCheckC(AM_argVec, AM_numArgs, nemblev);
+        args = (DF_TermPtr)(((MemPtr)args)+DF_TM_ATOMIC_SIZE);
+    }   
+}
+
+/* Generating a term on the top of heap which is to be added into a        */
+/* disagreement pair.                                                      */
+/* The term has the following structure:                                   */
+/* (h [|a1, 0, lev, nil|] ... [|an, 0, lev, nil|] #lev ... #1)             */
+/* It is assumed that nargs and lev are not equal to zero.                 */
+static void HOPU_mkTermNLL(DF_TermPtr h, DF_TermPtr args, int nargs, int lev)
+{
+    int newArity = nargs + lev;
+    MemPtr newArgs = AM_hreg + DF_TM_APP_SIZE; //spare app (head) size on heap
+    AM_arityError(newArity);
+    AM_heapError(AM_hreg + nargs*DF_TM_SUSP_SIZE + newArity*DF_TM_ATOMIC_SIZE
+                 + DF_TM_APP_SIZE);
+    DF_mkApp(AM_hreg, newArity, h, (DF_TermPtr)newArgs);
+    AM_hreg += (DF_TM_APP_SIZE + newArity * DF_TM_ATOMIC_SIZE);//alloc arg vec
+    for (; nargs > 0; nargs--){ //[|ai, 0, lev, nil|], for i <= nargs
+        DF_mkRef(newArgs, (DF_TermPtr)AM_hreg); 
+        DF_mkSusp(AM_hreg, 0, lev, DF_termDeref(args), DF_EMPTY_ENV);
+        newArgs += DF_TM_ATOMIC_SIZE;  AM_hreg += DF_TM_SUSP_SIZE;
+        args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
+    }
+    for (; lev > 0; lev--){     //#i, for i <= lev
+        DF_mkBV(newArgs, lev);
+        newArgs += DF_TM_ATOMIC_SIZE;
+    }
+}
+
+/* Generating a partial subsitution for the free head of a LLambda term    */
+/* corresponding to an internal flex term which is known to be non-LLambda.*/
+/* The partial substitution is of form:                                    */
+/* (h #n ... #1)                                                           */
+/* It is assumed that n is not equal to zero.                              */ 
+static void HOPU_mkSubstNLL(DF_TermPtr h, int n)
+{
+    AM_arityError(n);
+    AM_heapError(AM_hreg + DF_TM_APP_SIZE + n * DF_TM_ATOMIC_SIZE);
+    DF_mkApp(AM_hreg, n, h, (DF_TermPtr)(AM_hreg + DF_TM_APP_SIZE));
+       AM_hreg += DF_TM_APP_SIZE;
+    for (; n > 0; n--){
+        DF_mkBV(AM_hreg, n);
+        AM_hreg += DF_TM_ATOMIC_SIZE;
+    }
+}
+
+/* Try to solve G = ...(F a1 ... an)..., where F and G are different free  */
+/* variables, and (F a1 ... an) is non-LLambda.                            */
+/* Either G is bound to (F a1 ... an) or an exception is raised. In the    */
+/* latter case, the caller of this function is responsible to add a        */
+/* disagreement pair to the live list.                                     */
+static void HOPU_bndVarNestedFlex(DF_TermPtr fhPtr, DF_TermPtr args, int nargs,
+                                  int lev)
+{
+    HOPU_flexCheck(args, nargs, lev);
+    if (DF_fvUnivCount(fhPtr) > AM_adjreg) {
+        TR_trailTerm(fhPtr);  
+        AM_bndFlag = ON;
+        DF_modVarUC(fhPtr, AM_adjreg);
+    }
+}
+
+/* Try to find the (partial) structure of the substitution for a flex head  */
+/* of a LLambda term corresponding to an internal flex term which is not    */
+/* known to be LLambda.                                                     */
+/* If the internal flex term is LLambda, HOPU_flexNestedLLambda is invoked  */
+/* to generate the (parital) substitution for the outside variable, and     */
+/* perform proper substitutions on the internal free variable if necessary. */
+/* Otherwise, a disagreement pair is added into the live list.              */
+static DF_TermPtr HOPU_flexNestedSubst(DF_TermPtr args1, int nargs1, 
+                                       DF_TermPtr fhPtr, DF_TermPtr args2, 
+                                       int nargs2, DF_TermPtr tmPtr, int emblev)
+{
+    DF_TermPtr bnd;
+    int varuc = DF_fvUnivCount(fhPtr);
+    if (HOPU_isLLambda(varuc, nargs2, args2)){ 
+        if (fhPtr == AM_vbbreg) EM_THROW(EM_FAIL); //occurs check
+        bnd = HOPU_flexNestedLLambda(args1, nargs1, varuc, tmPtr, fhPtr, args2,
+                                     nargs2, emblev);
+    } else {// the internal flex term is not LLambda: delay (opt possible)
+        DF_TermPtr newVar;
+        DF_TermPtr newTerm;
+	Boolean    found = FALSE;
+        if ((fhPtr != AM_vbbreg) && (nargs1 == 0)) {
+            EM_TRY{ 
+                HOPU_bndVarNestedFlex(fhPtr, args2, nargs2, emblev);
+                bnd = tmPtr;
+		found = TRUE;
+            } EM_CATCH {if (EM_CurrentExnType != EM_FAIL) EM_RETHROW();}
+        } 
+	if (!found) {
+	  newVar = (DF_TermPtr)AM_hreg;
+	  HOPU_pushVarToHeap(AM_adjreg);
+	  HOPU_copyFlagGlb = TRUE;
+	  if ((nargs1 == 0) && (emblev == 0)) {
+            bnd = newVar;
+            AM_addDisPair(bnd, tmPtr);
+	  } else {                          
+            newTerm = (DF_TermPtr)AM_hreg;
+            HOPU_mkTermNLL(newVar, args1, nargs1, emblev);
+            AM_addDisPair(newTerm, tmPtr);
+            bnd = (DF_TermPtr)AM_hreg;
+            HOPU_mkSubstNLL(newVar, emblev + nargs1);
+	  }
+	}
+    }
+    return bnd;
+}
+
+/* This version of flexNestedSubst is needed in the compiled form of pattern */
+/* unification. The essential difference from the other version is that the  */
+/* variable being bound is already partially bound to a structure.           */
+/* The difference from the other procedure is first the head normalization   */
+/* process invokded is one performs occurs checking on partially bound       */
+/* variables, and second, the "top-level" flexible term is a free variable:  */
+/* so there is no need to distinguish whether the other flex term is Llambda */
+/* or not: the substitution can be found by an invocation of flexCheckC      */
+DF_TermPtr HOPU_flexNestedSubstC(DF_TermPtr fhPtr, DF_TermPtr args, int nargs,
+                                 DF_TermPtr tmPtr, int emblev)
+{
+    DF_TermPtr bnd, newVar, newTerm;
+    int varuc;
+    Boolean found = FALSE;
+
+    EM_TRY {
+        HOPU_flexCheckC(args, nargs, emblev);
+        if (DF_fvUnivCount(fhPtr) > AM_adjreg){
+            TR_trailTerm(fhPtr);
+            AM_bndFlag = ON;
+            DF_modVarUC(fhPtr, AM_adjreg);
+        }
+	bnd = tmPtr;
+	found = TRUE;
+    } EM_CATCH { if (EM_CurrentExnType != EM_FAIL) EM_RETHROW(); }
+
+    if (!found) {
+      varuc = DF_fvUnivCount(fhPtr);
+      if (HOPU_isLLambda(varuc, nargs, args)){
+        bnd = HOPU_flexNestedLLambda(NULL, 0, varuc, tmPtr, fhPtr, args, nargs,
+                                     emblev);
+      } else {//otherwise delay this pair onto the live list
+        HOPU_copyFlagGlb = TRUE;
+        newVar = (DF_TermPtr)AM_hreg;
+        HOPU_pushVarToHeap(AM_adjreg);
+        if (emblev == 0) {
+	  bnd = newVar;
+	  AM_addDisPair(bnd, tmPtr);
+        } else {
+	  newTerm = (DF_TermPtr)AM_hreg;
+	  HOPU_mkTermNLL(newVar, NULL, 0, emblev);
+	  AM_addDisPair(newTerm, tmPtr);
+	  bnd = (DF_TermPtr)AM_hreg;
+	  HOPU_mkSubstNLL(newVar, emblev);
+        }
+      }
+    }
+    return bnd;    
+}
+
+/* Try to solve G = (F a1 ... an), where F and G are different free        */
+/* variables, and (F a1 ... an) is non-LLambda.                            */
+/* Either G is bound to (F a1 ... an) or an exception is raised. In the    */
+/* latter case, the caller of this function is responsible to add a        */
+/* disagreement pair to the live list.                                     */
+static void HOPU_bndVarFlex(DF_TermPtr vPtr, DF_TermPtr fPtr, DF_TermPtr fhPtr,
+                            DF_TermPtr args, int nargs)
+{
+    AM_vbbreg = vPtr;    AM_adjreg = DF_fvUnivCount(vPtr);
+    HOPU_flexCheck(args, nargs, 0);    
+    if (DF_fvUnivCount(fhPtr) > AM_adjreg) {
+        TR_trailTerm(fPtr);
+        AM_bndFlag = ON;
+        DF_modVarUC(fhPtr, AM_adjreg);
+    }
+    TR_trailTerm(vPtr);
+    AM_bndFlag = ON;
+    DF_mkRef((MemPtr)vPtr, fPtr);
+}
+
+/* Try to solve (F a1 ... an) = lam(k, (G b1 ... bm)), where F and G are   */
+/* both free variables.                                                    */ 
+/*  The arguments are:                                                     */
+/*  tPtr1 : reference to the ABSTRACTION BODY of the first flex term       */
+/*  h1    : reference to the flex head of the first term                   */
+/*  nargs1: number of arguments of the first flex term                     */
+/*  args1 : reference to the argument vector of the first flex term        */
+/*  tPtr2 : reference to the ABSTRACTION BODY of the second flex term      */
+/*  h2    : reference to the flex head of the second flex term             */
+/*  nargs2: number of arguments of the second flex term                    */
+/*  args2 : reference to the argument vector of the second flex term       */
+/*  lev   : abstraction context of the second term with respect to the     */
+/*          first one.                                                     */
+/*                                                                         */
+/*  Non-Llambda pairs could be encountered during this process, and in     */  
+/*  this situation, the pair is delayed onto the disagreement list.        */
+static void HOPU_flexMkSubst(DF_TermPtr tPtr1, DF_TermPtr h1, int nargs1,
+                             DF_TermPtr args1, DF_TermPtr tPtr2, DF_TermPtr h2,
+                             int nargs2, DF_TermPtr args2, int lev)
+{
+    int uc = DF_fvUnivCount(h1);
+    if (HOPU_isLLambda(uc, nargs1, args1)){ //the first term is LLambda
+        DF_TermPtr bndBody;
+        if (h1 == h2) { //same variable (comparing addresses)
+            if (HOPU_isLLambda(uc, nargs2, args2)) {//same var common uc
+                MemPtr oldhtop = AM_hreg;
+                DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;
+                HOPU_copyFlagGlb = FALSE;
+                nargs1 = HOPU_pruneSameVar(args1, nargs1, args2, nargs2, lev);
+                if ((nargs1 != nargs2) || HOPU_copyFlagGlb){
+                    DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
+                    HOPU_pushVarToHeap(uc);
+                    HOPU_mkPandRSubst(newVar, newArgs, nargs1, h1, nargs2);
+                } else AM_hreg = oldhtop; //unbound
+            } else {  //(F a1 ... an)[ll] = (lam(k, (F b1 ... bm)))[non-ll] 
+                if (lev == 0) AM_addDisPair(tPtr1, tPtr2);  
+                else {
+                    MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
+                    DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
+                    AM_heapError(AM_hreg);
+                    DF_mkLam(AM_hreg, lev, tPtr2);
+                    AM_hreg = nhtop;
+                    AM_addDisPair(tPtr1, tmPtr);
+                } //(lev != 0)
+            } //tPtr2 not LLambda 
+        } else {        //different variable
+            int nabs;
+            AM_vbbreg = h1;   AM_adjreg = uc;   //set regs for occ
+            HOPU_copyFlagGlb = FALSE;       
+            bndBody = HOPU_flexNestedSubst(args1, nargs1, h2, args2, nargs2, 
+                                           tPtr2, lev);
+            nabs = lev + nargs1;
+            TR_trailTerm(h1); AM_bndFlag = ON;
+            if (nabs == 0) DF_mkRef((MemPtr)h1, bndBody);
+            else {
+                AM_embedError(nabs);
+                DF_mkLam((MemPtr)h1, nabs, bndBody);
+            }  
+        }               //different variable
+    } else {            //the first term is non-LLambda
+      Boolean found = FALSE;
+      if ((nargs2 == 0) && (lev == 0) && (h1 != h2)) { // (F t1 ... tm) = G  
+	EM_TRY{ 
+	  HOPU_bndVarFlex(h2, tPtr1, h1, args1, nargs1); 
+	  found = TRUE;
+	} EM_CATCH { 
+	  if (EM_CurrentExnType != EM_FAIL) EM_RETHROW(); 
+	} 
+      } 
+      if (!found) {
+        if (lev == 0) AM_addDisPair(tPtr1, tPtr2); 
+        else {
+	  MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
+	  DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
+	  AM_heapError(AM_hreg);
+	  DF_mkLam(AM_hreg, lev, tPtr2);
+	  AM_hreg = nhtop;
+	  AM_addDisPair(tPtr1, tmPtr);
+        } //(lev != 0)
+      }
+    }                  //the first term is non-LLambda
+}
+
+/* The counterpart of HOPU_flexMkSubst invoked from HOPU_patternUnifyPair.  */
+/* Care is taken to avoid making a reference to a stack address in binding  */
+/* and creating disagreement pairs.                                         */
+/* It is assumed that the first term (F a1 ... an) given by its             */
+/* is not embedded in any abstractions.                                     */
+static void HOPU_flexMkSubstGlb(DF_TermPtr tPtr1, DF_TermPtr h1, int nargs1,
+                                DF_TermPtr args1,
+                                DF_TermPtr tPtr2, DF_TermPtr h2, int nargs2,
+                                DF_TermPtr args2, 
+                                DF_TermPtr topPtr2, int lev)
+{
+    int uc = DF_fvUnivCount(h1);
+    if (HOPU_isLLambda(uc, nargs1, args1)) { //the first term is LLambda
+        DF_TermPtr bndBody;
+        if (h1 == h2) { //same variable (comparing addresses)
+            if (HOPU_isLLambda(uc, nargs2, args2)){//same var; common uc
+                MemPtr oldhtop = AM_hreg;
+                DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;
+                HOPU_copyFlagGlb = FALSE;
+                nargs1 = HOPU_pruneSameVar(args1, nargs1, args2, nargs2, lev);
+                if ((nargs1 != nargs2) || HOPU_copyFlagGlb) {
+                    DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
+                    HOPU_pushVarToHeap(uc);
+                    HOPU_mkPandRSubst(newVar, newArgs, nargs1, h1, nargs2);
+                } else AM_hreg = oldhtop; //variable remain unbound
+            } else { //(F a1 ... an)[ll] = (lam(k, (F b1 ... bm)))[non-ll]
+                     //non-LLambda term must locate on the heap
+                if (nargs1 == 0) tPtr1 = HOPU_globalizeFlex(tPtr1);
+                if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
+                else AM_addDisPair(tPtr1, DF_termDeref(topPtr2));
+            } //tPtr2 not LLambda
+        } else { //different variable
+            int nabs;
+            AM_vbbreg = h1; AM_adjreg = uc; //set regs for occ
+            HOPU_copyFlagGlb = FALSE;
+            bndBody = HOPU_flexNestedSubst(args1, nargs1, h2, args2, nargs2,
+                                           tPtr2, lev);
+            nabs = nargs1 + lev;
+            TR_trailTerm(h1); AM_bndFlag = ON;
+            if (HOPU_copyFlagGlb == FALSE)
+                bndBody = HOPU_globalizeFlex(bndBody);
+            if (nabs == 0) DF_mkRef((MemPtr)h1, bndBody);
+            else {
+                AM_embedError(nabs);
+                DF_mkLam((MemPtr)h1, nabs, bndBody);
+            }
+        }
+    } else {//the first term is non-LLambda (must locate on heap)
+      Boolean found = FALSE;
+      if ((nargs2 == 0) && (lev == 0) && (h1 != h2)) {//(F t1...tm)[nll] = G
+	EM_TRY { 
+	  HOPU_bndVarFlex(h2, tPtr1, h1, args1, nargs1); 
+	  found = TRUE;
+	} EM_CATCH {
+	  if (EM_CurrentExnType == EM_FAIL) 
+	    tPtr2 = HOPU_globalizeFlex(tPtr2);
+	  else EM_RETHROW();
+	}
+      }
+      if (!found) {
+        if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
+        else AM_addDisPair(tPtr1, DF_termDeref(topPtr2));
+      }
+    }       //the first term is non-LLambda
+}
+ 
+
+/***************************************************************************/
+/*                 BINDING FOR FLEX-RIGID                                  */
+/*                                                                         */
+/* Auxiliary functions for solving flex-rigid pairs.                       */
+/* Non-LLambda pairs are delayed onto the disagreement list.               */
+/***************************************************************************/
+/* Try to find the (partial) binding of the head of a flex term correponding */
+/* to a rigid atom during the process of unifying the flex term with a       */
+/* rigid one. The global variable HOPU_copyFlagGlb is used to indicate       */
+/* whether a new term is created during this process.                        */
+/* Note it is assumed that rPtr refers to the dereference of a rigid atom    */
+/* or cons.                                                                  */
+static DF_TermPtr HOPU_getHead(DF_TermPtr rPtr, DF_TermPtr args, int nargs, 
+                               int emblev)
+{
+    DF_TermPtr rtPtr;
+    switch(DF_termTag(rPtr)){
+    case DF_TM_TAG_CONST:{
+        if (DF_constUnivCount(rPtr) > AM_adjreg){
+            MemPtr newhtop;
+            int ind = HOPU_constIndex(rPtr, args, nargs, emblev);
+            if (ind == 0) EM_THROW(EM_FAIL);        //occurs-check
+            AM_embedError(ind);
+            newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
+            AM_heapError(newhtop);
+            HOPU_copyFlagGlb = TRUE;         //new structure is created
+            rtPtr = (DF_TermPtr)AM_hreg;     //create a db on the heap top
+            DF_mkBV(AM_hreg, ind);
+            AM_hreg = newhtop;
+        } else rtPtr = rPtr; //DF_constUnivCount(rPtr <= AM_adjreg)
+        break;
+    }
+    case DF_TM_TAG_BVAR:   {
+        int dbInd = DF_bvIndex(rPtr);
+        if (dbInd > emblev){            
+            int ind = HOPU_bvIndex(dbInd, args, nargs, emblev);
+            if (ind == 0) EM_THROW(EM_FAIL);        //occurs-check            
+            AM_embedError(ind);
+            if (ind == dbInd) rtPtr = rPtr;  //use the old db term
+            else {                           //create a db on the heap top
+                MemPtr newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
+                AM_heapError(newhtop);
+                HOPU_copyFlagGlb = TRUE;     //new structure is created
+                rtPtr = (DF_TermPtr)AM_hreg;
+                DF_mkBV(AM_hreg, ind);
+                AM_hreg = newhtop;   
+            }
+        } else rtPtr = rPtr; //dbInd <= emlev
+        break;
+    }
+    default: { rtPtr = rPtr; break;} //other rigid head: cons,nil,int,fl,str 
+    } //switch
+    return rtPtr;
+}
+
+/* Create a new cons or app term on the current heap top.                 */
+static void HOPU_mkConsOrApp(DF_TermPtr tmPtr, DF_TermPtr funcPtr, 
+                             DF_TermPtr argvec, int nargs)
+{
+    MemPtr newhtop;
+    if (DF_isCons(tmPtr)) {
+        newhtop = AM_hreg + DF_TM_CONS_SIZE;
+        AM_heapError(newhtop);
+        DF_mkCons(AM_hreg, argvec);
+    } else {// application
+        newhtop = AM_hreg + DF_TM_APP_SIZE;
+        AM_heapError(newhtop);
+        DF_mkApp(AM_hreg, nargs, funcPtr, argvec);
+    }
+    AM_hreg = newhtop;
+}
+
+/* Try to find the (partial) binding of the head of a flex term when       */
+/* unifying it with a rigid term possible under abstractions.              */
+/* The arguments are:                                                      */
+/*  fargs:    reference to the arguments of the flex term                  */
+/*  fnargs:   number of arguments of the flex term                         */
+/*  rhPtr:    reference to the rigid head                                  */
+/*  rPtr:     reference to the ABSTRACTION BODY of the rigid term          */
+/*  rargs:    reference to the arguments of the rigid term                 */
+/*  rnargs:   number of arguments of the rigid term                        */
+/*  emblev:   abstraction context of the rigid term                        */
+/* The global variable HOPU_copyFlagGlb is used to indicate whether new    */
+/* term is created in this process.                                        */
+/* Note that if the rigid term is app or cons, it is first assumed that    */
+/* a new argument vector is to be created. However, after all the args in  */
+/* the binding are calculated, a checking is made on whether this is       */
+/* really necessary. If it is not, the old arg vector is used, and the new */
+/* one is abandoned. (Heap space for it is deallocated.)                   */ 
+/* It is assumed that the flexible head and its universe count are         */
+/* in registers AM_vbbreg and AM_adjreg.                                   */
+static DF_TermPtr HOPU_rigNestedSubst(DF_TermPtr fargs, int fnargs, 
+                                      DF_TermPtr rhPtr, DF_TermPtr rPtr,
+                                      DF_TermPtr rargs, int rnargs, int emblev)
+{
+    rhPtr = HOPU_getHead(rhPtr, fargs, fnargs, emblev); //head of the binding    
+    if (rnargs == 0) return rhPtr;       //the rigid term is atomic
+    else {                               //the rigid term is cons or app
+        Boolean myCopyFlagHead = HOPU_copyFlagGlb, myCopyFlagArgs = FALSE;
+        int i;
+        MemPtr oldHreg = AM_hreg;                   //the old heap top
+        MemPtr argLoc  = AM_hreg;                   //arg vector location
+        DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;   //new argument vector
+        DF_TermPtr oldArgs = rargs;                 //old argument vector
+        AM_heapError(AM_hreg + rnargs * DF_TM_ATOMIC_SIZE);   
+        AM_hreg += rnargs * DF_TM_ATOMIC_SIZE;      //allocate space for argvec
+        HOPU_copyFlagGlb = FALSE;
+        for (i = 0; i < rnargs; i++){
+            DF_TermPtr bnd;
+            int        nabs;
+	    MemPtr     tmpHreg = AM_hreg;
+            HN_hnorm(rargs);  nabs = AM_numAbs;     //dereference of hnf
+	    if (AM_hreg != tmpHreg) {myCopyFlagArgs = TRUE; }
+
+            if (AM_rigFlag){
+                bnd = HOPU_rigNestedSubst(fargs, fnargs, AM_head,
+                       HOPU_lamBody(rargs), AM_argVec, AM_numArgs, nabs+emblev);
+            } else { //AM_rigFlag = FALSE
+                bnd = HOPU_flexNestedSubst(fargs, fnargs, AM_head, AM_argVec,
+                       AM_numArgs, HOPU_lamBody(rargs), nabs+emblev);
+            }
+            if (nabs == 0) DF_mkRef(argLoc, bnd); //compact atomic??
+            else DF_mkLam(argLoc, nabs, bnd);
+            argLoc += DF_TM_ATOMIC_SIZE;  //note: abs has atomic size
+            if (HOPU_copyFlagGlb) {myCopyFlagArgs=TRUE; HOPU_copyFlagGlb=FALSE;}
+            rargs = (DF_TermPtr)(((MemPtr)rargs)+DF_TM_ATOMIC_SIZE); //next arg
+        } //for loop
+        if (myCopyFlagArgs) {	  
+            DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
+            HOPU_mkConsOrApp(rPtr, rhPtr, newArgs, rnargs);
+            HOPU_copyFlagGlb = TRUE;
+            return tmPtr;
+        } else { //myCopyFlagBody == FALSE
+            AM_hreg = oldHreg; //deallocate space for the argument vector
+            //note no new terms are created form any argument
+            if (myCopyFlagHead){
+                DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
+                HOPU_mkConsOrApp(rPtr, rhPtr, oldArgs, rnargs);
+                HOPU_copyFlagGlb = TRUE;
+                return tmPtr;
+            } else  return rPtr; //myCopyFlagHead==FALSE, myCopyFlagArgs==FALSE
+     	}
+    }//rnargs > 0
+}
+
+/* This version of rigNestedSubstC is needed in the compiled form of pattern */
+/* unification. The essential difference from the other version is that the  */
+/* variable being bound is already partially bound to a structure.           */
+/* The difference from the other procedure is first the head normalization   */
+/* procedure invoked is one performs the occurs checking on partially bound  */
+/* variables, and second, the incoming flexible term is in fact a free       */
+/* variable.                                                                 */ 
+DF_TermPtr HOPU_rigNestedSubstC(DF_TermPtr rhPtr, DF_TermPtr rPtr,
+                                DF_TermPtr rargs, int rnargs, int emblev)
+{
+    rhPtr = HOPU_getHead(rhPtr, NULL, 0, emblev);
+    if (rnargs == 0) return rhPtr;
+    else {
+        Boolean myCopyFlagHead = HOPU_copyFlagGlb, myCopyFlagArgs = FALSE;
+        int i;
+        MemPtr oldHreg = AM_hreg;                    //the old heap top
+        MemPtr argLoc  = AM_hreg;                    //arg vector location
+        DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;    //new arg vector
+        DF_TermPtr oldArgs = rargs;                  //old arg vector
+        AM_heapError(AM_hreg + rnargs * DF_TM_ATOMIC_SIZE); 
+        AM_hreg += rnargs * DF_TM_ATOMIC_SIZE;       //alloc space for new args
+        HOPU_copyFlagGlb = FALSE;
+        for (i = 0; i < rnargs; i++) {
+            DF_TermPtr bnd;
+            int        nabs;
+	    MemPtr     tmpHreg = AM_hreg;
+            HN_hnormOcc(rargs); nabs = AM_numAbs;
+	    if (tmpHreg != AM_hreg) {myCopyFlagArgs = TRUE; }
+            if (AM_rigFlag) 
+                bnd = HOPU_rigNestedSubstC(AM_head, HOPU_lamBody(rargs), 
+                                           AM_argVec, AM_numArgs, nabs+emblev);
+            else  //AM_rigFlag == FALSE
+                bnd = HOPU_flexNestedSubstC(AM_head, AM_argVec, AM_numArgs, 
+                                            HOPU_lamBody(rargs), nabs+emblev);
+
+            if (nabs == 0) DF_mkRef(argLoc, bnd);
+	    else DF_mkLam(argLoc, nabs, bnd);
+
+            argLoc += DF_TM_ATOMIC_SIZE;
+            if (HOPU_copyFlagGlb) {myCopyFlagArgs=TRUE; HOPU_copyFlagGlb=FALSE;}
+            rargs = (DF_TermPtr)(((MemPtr)rargs)+DF_TM_ATOMIC_SIZE);
+        } //for loop
+        if (myCopyFlagArgs) {
+            DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
+            HOPU_mkConsOrApp(rPtr, rhPtr, newArgs, rnargs);
+            HOPU_copyFlagGlb = TRUE;
+            return tmPtr;
+        } else { //myCopyFlagArgs == FALSE
+	  AM_hreg = oldHreg;//deallocate space for arg vector
+	  if (myCopyFlagHead) {
+	    DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
+	    HOPU_mkConsOrApp(rPtr, rhPtr, oldArgs, rnargs);
+	    HOPU_copyFlagGlb = TRUE;
+	    return tmPtr;
+	  } else return rPtr; ////myCopyFlagHead==FALSE, myCopyFlagArgs==FALSE
+        }
+    }//rnargs > 0
+}
+
+/* Try to solve (F a1 ... an) = lam(k, (r b1 ... bm)), where r is rigid.   */ 
+/*  The arguments are:                                                     */
+/*  fPtr  : reference to the ABSTRACTION BODY of the flex term             */
+/*  fhPtr : reference to the flex head                                     */
+/*  fnargs: number of arguments of the flex term                           */
+/*  fargs : reference to the argument vector of the flex term              */
+/*  rPtr  : reference to the ABSTRACTION BODY of the rigid term            */
+/*  rhPtr : reference to the rigid head (Note it could be cons)            */
+/*  rnargs: number of arguments of the rigid term                          */
+/*  rargs : reference to the argument vector of the rigid term             */
+/*                                                                         */
+/*  Non-Llambda pairs could be encountered during this process, and in     */  
+/*  this situation, the pair is delayed onto the disagreement list.        */
+static void HOPU_rigMkSubst(DF_TermPtr fPtr, DF_TermPtr fhPtr, int fnargs,
+                            DF_TermPtr fargs, DF_TermPtr rPtr, DF_TermPtr rhPtr,
+                            int rnargs, DF_TermPtr rargs, int emblev)
+{
+    int uc = DF_fvUnivCount(fhPtr);
+    if (HOPU_isLLambda(uc, fnargs, fargs)){//Llambda pattern
+        DF_TermPtr bndBody;                //abs body of bnd of the fv
+        int nabs;
+        
+        AM_vbbreg = fhPtr; AM_adjreg = uc; //set regs for occurs check
+        HOPU_copyFlagGlb = FALSE;
+        bndBody   = HOPU_rigNestedSubst(fargs, fnargs, rhPtr, rPtr,
+                                        rargs, rnargs, emblev);
+        nabs      = emblev + fnargs; //# abs in the front of the binding
+        TR_trailTerm(fhPtr);  AM_bndFlag = ON;
+        if (nabs == 0) DF_mkRef((MemPtr)fhPtr, bndBody);
+        else {
+            AM_embedError(nabs);
+            DF_mkLam((MemPtr)fhPtr, nabs, bndBody);
+        }
+    } else {                              //non-Llambda pattern        
+        if (emblev == 0) AM_addDisPair(fPtr, rPtr);
+        else {
+            MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
+            DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
+            AM_heapError(AM_hreg);
+            DF_mkLam(AM_hreg, emblev, rPtr);
+            AM_hreg = nhtop;
+            AM_addDisPair(fPtr, tmPtr);
+        } // (emblev != 0)
+    }                                     //non-LLambda pattern
+}
+
+/* The counter part of HOPU_rigMkSubst invoked by HOPU_patternUnifyPair.    */
+/* Care is taken to avoid making a reference to a register/stack address in */
+/* binding and creating disagreement pair.                                  */
+/* It is assumed that the pair of terms are not embedded in any abstractions*/
+/* ie. (F a1 ... an) = (r b1 ... bm)                                        */
+/* Note both fPtr and rPtr are not dereferenced.                            */
+static void HOPU_rigMkSubstGlb(DF_TermPtr fPtr, DF_TermPtr fhPtr, int fnargs,
+                               DF_TermPtr fargs, 
+                               DF_TermPtr rPtr, DF_TermPtr rhPtr, int rnargs,
+                               DF_TermPtr rargs)
+{
+    int uc = DF_fvUnivCount(fhPtr);
+    if (HOPU_isLLambda(uc, fnargs, fargs)) { //LLambda pattern
+        DF_TermPtr bndBody;
+        AM_vbbreg = fhPtr; AM_adjreg = uc;
+        HOPU_copyFlagGlb = FALSE;
+        bndBody = HOPU_rigNestedSubst(fargs, fnargs, rhPtr, DF_termDeref(rPtr),
+                                      rargs, rnargs, 0);
+        TR_trailTerm(fhPtr); AM_bndFlag = ON;
+        if (HOPU_copyFlagGlb) {//bndBody must locate on the heap
+            if (fnargs == 0) DF_mkRef((MemPtr)fhPtr, bndBody);
+            else {
+                AM_embedError(fnargs);
+                DF_mkLam((MemPtr)fhPtr, fnargs, bndBody);
+            }
+        } else { //HOPU_copyFlagGlb == FALSE
+            /*  //note: rPtr is the undereferenced rigid term; in this case,
+            //      it is assumed rPtr cannot be a reference to the stack.
+            //      This assumption should be ensured by the fact that atomic
+            //      rigid terms on stack are alway copied into registers in 
+            //      binding. 
+            if (fnargs == 0) DF_copyAtomic(rPtr, (MemPtr)fhPtr); */
+            if (fnargs == 0) HOPU_globalizeCopyRigid(bndBody, fhPtr);
+            else {
+                bndBody = HOPU_globalizeRigid(bndBody);
+                AM_embedError(fnargs);
+                DF_mkLam((MemPtr)fhPtr, fnargs, bndBody);
+            }
+        }        //HOPU_copyFlagGlb == FALSE 
+    } else //non_LLambda flex (must locate on the heap)
+        AM_addDisPair(DF_termDeref(fPtr),
+                      HOPU_globalizeRigid(DF_termDeref(rPtr)));
+}
+
+/***************************************************************************/
+/*             TERM SIMPLIFICATION (RIGID-RIGID)                           */
+/*                                                                         */
+/* Auxiliary functions for solving rigid-rigid pairs.                      */
+/***************************************************************************/
+
+/* Matching heads of two rigid terms. Eta-expansion is considered when     */
+/* necessary. It is assumed that the heads have been dereferenced.         */
+static void HOPU_matchHeads(DF_TermPtr hPtr1, DF_TermPtr hPtr2, int nabs)
+{
+    switch(DF_termTag(hPtr1)){
+    case DF_TM_TAG_CONST:{
+        if (!(DF_isConst(hPtr2) && (DF_sameConsts(hPtr1, hPtr2)))) 
+            EM_THROW(EM_FAIL);
+        if (DF_isTConst(hPtr1)){ //(first-order) unify type environments
+            HOPU_typesUnify(DF_constType(hPtr1), DF_constType(hPtr2), 
+                            AM_cstTyEnvSize(DF_constTabIndex(hPtr1))); 
+        }
+        break;
+    }
+    case DF_TM_TAG_BVAR: {
+        if (!DF_isBV(hPtr2)) EM_THROW(EM_FAIL);
+        else {                   
+            int ind = DF_bvIndex(hPtr2) + nabs; //lifting for eta-expansion
+            AM_embedError(ind);
+            if (DF_bvIndex(hPtr1) != ind) EM_THROW(EM_FAIL);
+        }
+        break;
+    }
+    case DF_TM_TAG_NIL:  { if (!DF_isNil(hPtr2)) EM_THROW(EM_FAIL); break;}
+    case DF_TM_TAG_INT:  {
+        if (!(DF_isInt(hPtr2) && (DF_intValue(hPtr2) == DF_intValue(hPtr1))))
+            EM_THROW(EM_FAIL);
+        break;
+    }
+    case DF_TM_TAG_FLOAT:{
+        if (!(DF_isFloat(hPtr2)&&(DF_floatValue(hPtr2)==DF_floatValue(hPtr1))))
+            EM_THROW(EM_FAIL);
+        break;
+    }
+    case DF_TM_TAG_STR:  {
+        if (!(DF_isStr(hPtr2) && (DF_sameStrs(hPtr1, hPtr2))))
+            EM_THROW(EM_FAIL);
+        break;
+    }
+    case DF_TM_TAG_CONS: { 
+        if (!(DF_isCons(hPtr2))) EM_THROW(EM_FAIL);
+        break;
+    }
+    } //switch
+}
+
+/* Set up PDL by sub problems resulted from rigid-rigid pairs upon         */
+/* successful matching of their heads. Eta-expansion is performed on-a-fly */
+/* when necessary.                                                         */
+void HOPU_setPDL(MemPtr args1, MemPtr args2, int nargs, int nabs)
+{
+    if (nabs == 0){ //no need for eta-expansion
+        AM_pdlError(nargs * 2);
+        for (; nargs > 0; nargs --){
+            AM_pushPDL(args1);   args1 +=  DF_TM_ATOMIC_SIZE; 
+            AM_pushPDL(args2);   args2 +=  DF_TM_ATOMIC_SIZE;
+        }
+    } else {        //nabs > 0 (eta-expansion)
+        AM_pdlError((nargs + nabs) * 2);
+        AM_heapError(AM_hreg + nargs*DF_TM_SUSP_SIZE + nabs*DF_TM_ATOMIC_SIZE);
+        for (; nargs > 0; nargs --){ //[|ai, 0, nabs, nil|]
+            AM_pushPDL(args1);   AM_pushPDL(AM_hreg);
+            DF_mkSusp(AM_hreg, 0, nabs, DF_termDeref((DF_TermPtr)args2), 
+                      DF_EMPTY_ENV);
+            AM_hreg += DF_TM_SUSP_SIZE;
+            args1 += DF_TM_ATOMIC_SIZE; args2 += DF_TM_ATOMIC_SIZE;
+        }
+        for (; nabs > 0; nabs --){   // bv(i)
+            AM_pushPDL(args1);   AM_pushPDL(AM_hreg);
+            DF_mkBV(AM_hreg, nabs);
+            args1 += DF_TM_ATOMIC_SIZE; AM_hreg += DF_TM_ATOMIC_SIZE;
+        }
+    }
+}
+
+/***************************************************************************/
+/*            HIGHER_ORDER PATTERN UNIFICATION                             */
+/*                                                                         */   
+/*  The main routines of this file.                                        */
+/***************************************************************************/
+/* Perform higher-order pattern unification over the pairs delayed on the  */
+/* PDL stack. The PDL stack is empty upon successful termination of this   */
+/* procedure.                                                              */
+void HOPU_patternUnifyPDL()
+{
+    DF_TermPtr tPtr1, tPtr2,  //pointers to terms to be unified
+               hPtr,          //pointer to head of hnf 
+               args;          //arg vec of hnf
+    Flag       rig,   cons;   //rigid flag and cons flags
+    int        nabs,  nargs;  //binder length and # of arguments of hnf
+    while (AM_nemptyPDL()){
+        //retrieve the pair of terms on the current top of PDL
+        tPtr1 = (DF_TermPtr)AM_popPDL(); tPtr2 = (DF_TermPtr)AM_popPDL();
+        HN_hnorm(tPtr1); //hnorm tPtr1 
+        hPtr  = AM_head; args = AM_argVec; nabs = AM_numAbs; nargs = AM_numArgs;
+        rig   = AM_rigFlag;      //bookkeeping relevant info of hnf of tPtr1
+        HN_hnorm(tPtr2); //hnorm tPtr2
+        if (rig){
+            if (AM_rigFlag){// rigid - rigid
+                if (nabs > AM_numAbs) {
+                    nabs = nabs - AM_numAbs;   //reuse nabs
+                    HOPU_matchHeads(hPtr, AM_head, nabs);
+                    HOPU_setPDL((MemPtr)args,(MemPtr)AM_argVec,AM_numArgs,nabs);
+                } else {      //nabs <= AM_numAbs
+                    nabs = AM_numAbs - nabs;   //reuse nabs
+                    HOPU_matchHeads(AM_head, hPtr, nabs);
+                    HOPU_setPDL((MemPtr)AM_argVec, (MemPtr)args, nargs, nabs);
+                } 
+            } else {        // rigid - flex
+                DF_TermPtr rigBody  = HOPU_lamBody(tPtr1);
+                DF_TermPtr flexBody = HOPU_lamBody(tPtr2);
+                if (nabs < AM_numAbs) { //eta expand rigid term first
+                    nabs = AM_numAbs - nabs;   //reuse nabs
+                    rigBody = HOPU_etaExpand(&hPtr, &args, nargs, nabs);
+                    HOPU_rigMkSubst(flexBody, AM_head, AM_numArgs, AM_argVec, 
+                                    rigBody, hPtr, (nargs+nabs), args, 0);
+                } else HOPU_rigMkSubst(flexBody,AM_head, AM_numArgs, AM_argVec, 
+                                       rigBody,hPtr,nargs,args,nabs-AM_numAbs);
+            }               // rigid-flex
+        } else { //(rig == FALSE)
+            DF_TermPtr absBody1 = HOPU_lamBody(tPtr1);
+            DF_TermPtr absBody2 = HOPU_lamBody(tPtr2);
+            if (AM_rigFlag){// flex - rigid
+                if (AM_numAbs < nabs) { //eta expand rigid term first
+                    nabs = nabs - AM_numAbs;   //reuse nabs
+                    absBody2 = HOPU_etaExpand(&AM_head, &AM_argVec, AM_numArgs,
+                                              nabs);
+                    HOPU_rigMkSubst(absBody1, hPtr, nargs, args, absBody2, 
+                                    AM_head, AM_numArgs+nabs, AM_argVec, 0);
+                }else HOPU_rigMkSubst(absBody1,hPtr,nargs,args,absBody2,AM_head,
+                                      AM_numArgs,AM_argVec,AM_numAbs-nabs);
+            } else {        // flex - flex
+                if (AM_numAbs > nabs)
+                    HOPU_flexMkSubst(absBody1, hPtr, nargs, args, absBody2, 
+                                     AM_head, AM_numArgs, AM_argVec, 
+                                     AM_numAbs-nabs);
+                else HOPU_flexMkSubst(absBody2, AM_head, AM_numArgs, AM_argVec,
+                                      absBody1,hPtr,nargs,args,nabs-AM_numAbs);
+            }               // flex - flex
+        }        //(rig == FALSE)
+    } // while (AM_nemptyPDL())
+}
+
+/* Interpretively pattern unify first the pairs delayed on the PDL, then    */
+/* those delayed on the live list, if binding occured during the first step */
+/* or previous compiled unification process.                                */
+/* Upon successful termination, PDL should be empty and pairs left on the   */
+/* live list should be those other than LLambda.                            */
+void HOPU_patternUnify()
+{
+    HOPU_patternUnifyPDL();   //first solve those left from compiled unification
+    while (AM_bndFlag && AM_nempLiveList()){
+        DF_DisPairPtr dset = AM_llreg;
+        do {  //move everything in live list to PDL
+            AM_pdlError(2);
+            AM_pushPDL((MemPtr)DF_disPairSecondTerm(dset));
+            AM_pushPDL((MemPtr)DF_disPairFirstTerm(dset));
+            dset = DF_disPairNext(dset);
+        } while (DF_isNEmpDisSet(dset));
+        AM_bndFlag = OFF;
+        AM_llreg = DF_EMPTY_DIS_SET;
+        HOPU_patternUnifyPDL(); //unsolvable pairs are added to live list
+    }
+}
+
+/* Interpretively pattern unify a pair of terms given as parameters. This is*/
+/* the counter part of HOPU_patterUnifyPDL that is invoked from the compiled*/
+/* part of unification. In this situation, the procedure has to be applied  */
+/* to two terms as opposed to pairs delayed on the PDL stack.               */
+/*                                                                          */
+/* The input term pointers may dereference to register and stack addresses  */
+/* Care must be taken to avoid making a reference to a register (stack)     */
+/* address in binding a variable, and in making a disagreement pair.        */ 
+
+void HOPU_patternUnifyPair(DF_TermPtr tPtr1, DF_TermPtr tPtr2)
+{
+    DF_TermPtr h1Ptr, h2Ptr, args1, args2;
+    Flag       rig1, rig2, cons1, cons2;
+    int        nabs1, nabs2, nargs1, nargs2;
+    MemPtr     oldPdlBot = AM_pdlBot;
+
+    AM_pdlBot = AM_pdlTop;
+    HN_hnorm(tPtr1); h1Ptr = AM_head; args1 = AM_argVec;
+    nabs1 = AM_numAbs; nargs1 = AM_numArgs; rig1 = AM_rigFlag;    
+    HN_hnorm(tPtr2); h2Ptr = AM_head; args2 = AM_argVec;
+    nabs2 = AM_numAbs; nargs2 = AM_numArgs; rig2 = AM_rigFlag;
+
+
+    if (rig1) {
+        if (rig2) { //rigid-rigid
+            if (nabs1 > nabs2) {
+                nabs1 = nabs1 - nabs2;
+                HOPU_matchHeads(h1Ptr, h2Ptr, nabs1);
+                HOPU_setPDL((MemPtr)args1, (MemPtr)args2, nargs2, nabs1);
+            } else {//nabs1 <= nabs2
+                nabs1 = nabs2 - nabs1;
+                HOPU_matchHeads(h2Ptr, h1Ptr, nabs1);
+                HOPU_setPDL((MemPtr)args2, (MemPtr)args1, nargs1, nabs1);
+            }
+        } else {   //rigid-flex
+            if ((nabs1 == 0) && (nabs2 == 0))
+                HOPU_rigMkSubstGlb(tPtr2, h2Ptr, nargs2, args2, 
+                                   tPtr1, h1Ptr, nargs1, args1);
+            else {
+                DF_TermPtr rigBody = HOPU_lamBody(tPtr1);
+                DF_TermPtr flexBody = HOPU_lamBody(tPtr2);
+                if (nabs1 < nabs2) {
+                    nabs1 = nabs2 - nabs1;
+                    rigBody = HOPU_etaExpand(&h1Ptr, &args1, nargs1, nabs1);
+                    //now rigBody must locate on heap
+                    HOPU_rigMkSubst(flexBody, h2Ptr, nargs2, args2, rigBody,
+                                    h1Ptr, nargs1+nabs1, args1, 0);
+                } else  // (nabs1 >= nabs2)
+                    HOPU_rigMkSubst(flexBody, h2Ptr, nargs2, args2, rigBody,
+                                    h1Ptr, nargs1, args1, nabs1-nabs2);
+            }        // !(nabs1 == nabs2 == 0)
+        }         //rigid-flex
+    } else { // rig1 = FALSE
+        if (rig2) { //flex-rigid
+            if ((nabs2 == 0) && (nabs1 == 0))
+                HOPU_rigMkSubstGlb(tPtr1, h1Ptr, nargs1, args1,
+                                   tPtr2, h2Ptr, nargs2, args2);
+            else { //!(nabs1 == nabs2 == 0)
+                DF_TermPtr rigBody = HOPU_lamBody(tPtr2);
+                DF_TermPtr flexBody = HOPU_lamBody(tPtr1);
+                if (nabs2 < nabs1) {
+                    nabs1 = nabs2 - nabs1;
+                    rigBody = HOPU_etaExpand(&h2Ptr, &args2, nargs2, nabs1);
+                    //now rigBody must locate on heap
+                    HOPU_rigMkSubst(flexBody, h1Ptr, nargs1, args1, rigBody,
+                                    h2Ptr, nargs2+nabs1, args2, 0);
+                } else  //(nabs2 >= nabs1)                    
+                    HOPU_rigMkSubst(flexBody, h1Ptr, nargs1, args1, rigBody,
+                                    h2Ptr, nargs2, args2, nabs2-nabs1);
+            }      //!(nabs1 == nabs2 == 0)
+        } else { //flex-flex
+            if (nabs1 == 0) //nabs2 >= nabs1
+                HOPU_flexMkSubstGlb(DF_termDeref(tPtr1), h1Ptr, nargs1, args1,
+                                    HOPU_lamBody(tPtr2), h2Ptr, nargs2, args2,
+                                    tPtr2, nabs2);
+            else { //(nabs1 > 0)
+                if (nabs2 == 0) //nabs2 < nabs1
+                    HOPU_flexMkSubstGlb(DF_termDeref(tPtr2),h2Ptr,nargs2,args2,
+                                        HOPU_lamBody(tPtr1),h1Ptr,nargs1,args1,
+                                        tPtr1,nabs1);
+            
+                else { //nabs1 != 0 && nabs2 != 0
+                    DF_TermPtr flexBody1 = HOPU_lamBody(tPtr1);
+                    DF_TermPtr flexBody2 = HOPU_lamBody(tPtr2);
+                    if (nabs2 > nabs1)
+                        HOPU_flexMkSubst(flexBody1, h1Ptr, nargs1, args1,
+                                         flexBody2, h2Ptr, nargs2, args2,
+                                         nabs2-nabs1);
+                    else //nabs2 <= nabs1
+                        HOPU_flexMkSubst(flexBody2, h2Ptr, nargs2, args2,
+                                         flexBody1, h1Ptr, nargs1, args1,
+                                         nabs1-nabs2);
+                }      //nabs1 != 0 && nabs2 != 0
+            }     //(nabs1 > 0)
+        }       //flex-flex
+    }        //rig1 = FALSE
+    //solve the pairs (which must locate on heap) remaining on the PDL
+    HOPU_patternUnifyPDL(); 
+    AM_pdlBot = oldPdlBot;
+}
+
+#endif //HOPU_C