text: //////////////////////////////////////////////////////////////////////////////
  //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 hnorm.c.                                                            */
  /* This file contains the head normalization routines.                      */
  /* These procedures are based on the suspension calculus, and the reduction */
  /* strategy with lazy reduction, lazy substitution and lazy heap            */
  /* commitment is chosen. A SML realization of this process is described in  */
  /* paper "Choices in Representation and Reduction Strategies for Lambda     */
  /* Terms in Intersional Contexts".                                          */
  /****************************************************************************/
  
  #ifndef HNORM_C
  #define HNORM_C
  
  #include <stdlib.h>
  #include "dataformats.h"
  #include "mctypes.h"
  #include "hnorm.h"
  #include "hnormlocal.h"
  #include "abstmachine.h"
  #include "../system/error.h" 
  
  //for debugging: to be removed
  #include <stdio.h>
  #include "printterm.h"
  #include "../system/stream.h"
  
  /*****************************************************************************/
  /* a global(to file hnorm.c) encoding  of the explicit suspension environment*/
  /* and simple checking and updating functions on this environment            */
  /*****************************************************************************/
  /* environment of the implicit suspension, which is initialized to empty*/
  static int        ol, nl;
  static DF_EnvPtr  envlist;
  
  /* clean the environment to empty */
  static void    HN_setEmptyEnv()   { ol = 0; nl = 0; envlist = DF_EMPTY_ENV; }
  /* set the environment according to given values */
  static void    HN_setEnv(int o, int n, DF_EnvPtr e)
  {   ol = o;   nl = n;   envlist = e; }
  /* is an empty environment? */
  static Boolean HN_isEmptyEnv()    { return ((ol == 0) && (nl == 0));       }
  
  /****************************************************************************/
  /* Functions for creating (modifying) the environment list in the suspension*/
  /* environment defined by ol, nl and envlist according to their current     */
  /* values.                                                                  */
  /****************************************************************************/
  
  /* Add n (n > 0) dummy environment items to the front of the current 
     environment list:   @(nl+n-1) :: ... :: @nl :: envlist.
     New dummy env items are created on the current heap top.
  */
  static DF_EnvPtr HN_addNDummyEnv(int n)
  {
      int i;
      DF_EnvPtr last = envlist, current = NULL;
  
      AM_heapError(AM_hreg + n * DF_ENV_DUMMY_SIZE);
      for (i = 0; i < n; i++){
          current = (DF_EnvPtr)AM_hreg;
          DF_mkDummyEnv(AM_hreg, nl+i, last);
          AM_hreg += DF_ENV_DUMMY_SIZE;
          last = current;
      }
      return current;
  }
  
  /* Add n (n > 0) pair environment items to the front of the current 
     environment list as the following:  
     ([|an,myol,mynl,myenv|],nl):: ... ::([|ai,myol,mynl,myenv|],nl)::envlist,
     where ai is the ith argument in the vector referred to by argvec.
     Note if ai is an atomic term, the suspension over it is eagerly evaluated.
   */
  static DF_EnvPtr HN_addNPair(DF_TermPtr argvec, int myol, int mynl, 
                               DF_EnvPtr  myenv,  int n)
  {
      int i;
      DF_EnvPtr   last = envlist, current = NULL;
      MemPtr      myEnvlist = AM_hreg;
      MemPtr      newhtop = AM_hreg + n * DF_ENV_PAIR_SIZE;
      
      AM_heapError(newhtop);
      AM_hreg = newhtop;              //spare space for n pair env items
      for (i = 1; i<= n; i++) {
          current = (DF_EnvPtr)myEnvlist;
          DF_mkPairEnv(myEnvlist, nl, HNL_suspAsEnv(argvec,myol,mynl,myenv), 
                       last);
          myEnvlist += DF_ENV_PAIR_SIZE;
          last = current;
          argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
      }
      return current;
  }   
  
  /* A specialized version of HN_addNPair when the incoming environment is 
     empty.
     Now, n (n > 0) pair environment items are added to the front of the 
     current environment list as the following:
     (an,0) :: ... :: (a1,0) :: envlist, where ai is the ith argument in the
     vector referred to by argvec.
   */
  static DF_EnvPtr HN_addNPairEmpEnv(DF_TermPtr argvec, int n)
  {
      int i;
      DF_EnvPtr    last = envlist, current = NULL;
      AM_heapError(AM_hreg + n * DF_ENV_PAIR_SIZE);
      for (i = 1; i <= n; i++) {
          current = (DF_EnvPtr)AM_hreg;
          DF_mkPairEnv(AM_hreg, 0, argvec, last);
          AM_hreg += DF_ENV_PAIR_SIZE;
          last = current;
          argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
      }
      return current;
  }
  
  /****************************************************************************/
  /* A function for pushing suspension over n abstractions following the rule */
  /* [|lam(n,body), ol, nl, envlist|]                                         */
  /*     -> lam(n, [|body, ol+n, nl+n, @(nl+n-1) :: ... :: @nl :: envlist |]  */
  /* The result is committed on the current top of heap.                      */
  /* The top-level (implicit) suspension is given by the global variable      */
  /* ol, nl, and envlist.                                                     */
  /* This function is used in HN_hnormSusp, HN_hnormSuspOCC and HN_lnormSusp. */ 
  /****************************************************************************/
  static DF_TermPtr HN_pushSuspOverLam(DF_TermPtr lamPtr)
  {
      DF_TermPtr    rtPtr;      //term pointer to be returned 
      DF_TermPtr    suspPtr;    //explicit susp as the lam body in the result
      int           numabs =DF_lamNumAbs(lamPtr);
      int           newol = ol + numabs, newnl = nl + numabs;
      MemPtr        newhtop = AM_hreg+ DF_TM_SUSP_SIZE+ numabs*DF_TM_ATOMIC_SIZE;
      DF_EnvPtr     newenv;
  
      AM_embedError(newol);
      AM_embedError(newnl);
      AM_heapError(newhtop);   
      newenv  = HN_addNDummyEnv(numabs);
      suspPtr = HNL_suspAsEnv(DF_lamBody(lamPtr), newol, newnl, newenv);
      rtPtr   = (DF_TermPtr)AM_hreg; //create lam over the susp
      DF_mkLam(AM_hreg, numabs, suspPtr);
      AM_hreg = newhtop;
  
      return rtPtr;
  }
  
  /****************************************************************************/
  /* functions for (weak) head normalizing terms of known categories          */
  /*--------------------------------------------------------------------------*/
  /* General comments:                                                        */
  /*  An implicit suspension is given by the global variables ol, nl and      */
  /*  envlist together with the first argument tmPtr to the sub-functions:    */
  /*  [|tmPtr, ol, nl, envlist|]                                              */
  /*  The suspension environment could be empty in which case the term        */
  /*  being normalized is tmPtr itself.                                       */
  /*  The second argument of the sub-functions whnf is a flag indicating      */
  /*  whether a head normal form or a weak head normal form is being          */
  /*  computed.                                                               */ 
  /****************************************************************************/
  static DF_TermPtr HN_hnormDispatch(DF_TermPtr tmPtr, Boolean whnf);
  
  /* (weak) head normalize bound variable or implicit suspension with 
     bound variable as term skeleton. */
  static DF_TermPtr HN_hnormBV(DF_TermPtr bvPtr, Boolean whnf)
  {
  							
      DF_TermPtr rtPtr; //term pointer to be returned
      if (HN_isEmptyEnv()){                        //[|#i, 0, 0, nil|] -> #i
          rtPtr = bvPtr;
          HNL_setRegsRig(bvPtr);
      } else { //non-empty env       
          int dbind = DF_bvIndex(bvPtr);
  
          if (dbind > ol) {                        //[|#i,ol,nl,e|] -> #i-ol+nl
              int newind = dbind - ol + nl;
  
              AM_embedError(newind);
              rtPtr =(DF_TermPtr)AM_hreg;
              HNL_pushBV(newind); 
              HNL_setRegsRig(rtPtr);
              HN_setEmptyEnv();
          } else { // i <= ol
              DF_EnvPtr    envitem = DF_envListNth(envlist, dbind);
              int          nladj   = nl-DF_envIndex(envitem);
  
              if (DF_isDummyEnv(envitem)){         //[|#i,ol,nl,..@l..|]->#(nl-l)
                  rtPtr = (DF_TermPtr)AM_hreg;
                  HNL_pushBV(nladj); 
                  HNL_setRegsRig(rtPtr);
                  HN_setEmptyEnv();
              }  else { //pair env    [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
                  DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
                  if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
                      int newnl = DF_suspNL(tmPtr)+nladj;
                      AM_embedError(newnl);
                      HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
                      rtPtr = HN_hnormDispatch(DF_suspTermSkel(tmPtr), whnf);
                  } else {      
                      HN_setEnv(0, nladj, DF_EMPTY_ENV); 
                      rtPtr = HN_hnormDispatch(tmPtr, whnf);
                  }
              }         //pair env  
          }        // i<= ol    
      }        //non-empty env
  
      return rtPtr;    
  }
  
  
  /* (weak) head normalize an abstraction or implicit suspension with term
     skeleton as an abstraction. 
     If an implicit suspension is weak head normalized, the suspension itself
     is returned. The descendant of this suspension over its abstraction skeleton
     is performed in the subsequent app case on a fly.
     Note that this is the only case that hnorm termniates with a non-empty 
     environment.
  */
  static DF_TermPtr HN_hnormLam(DF_TermPtr lamPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
  
      if (whnf) return rtPtr = lamPtr; //weak hn 
      else {  //whnf = FALSE
          int numabs = DF_lamNumAbs(lamPtr);
          DF_TermPtr newbody;
  
          if (HN_isEmptyEnv()){
              newbody = HN_hnormDispatch(DF_lamBody(lamPtr), FALSE);
              rtPtr = lamPtr; //body must have been adjusted in place
          } else {  // non-empty env 
              //[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
              int newol = ol+numabs, newnl = nl+numabs;
              
              AM_embedError(newol);
              AM_embedError(newnl);
              HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
              newbody = HN_hnormDispatch(DF_lamBody(lamPtr), FALSE);
              /* create a new lam on the result of hn the lam body */
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushLam(newbody, numabs);
          }         // non-empty env
          AM_numAbs += numabs;
      }      //whnf == FALSE
      return rtPtr;
  }
  
  /* (weak) head normalize cons or implicit suspension over cons          */
  static DF_TermPtr HN_hnormCons(DF_TermPtr consPtr, Boolean whnf)
  {
      DF_TermPtr argvec = DF_consArgs(consPtr),
                 rtPtr; //term pointer to be returned
      if (HN_isEmptyEnv()){
          AM_argVec = argvec;
          AM_numArgs = DF_CONS_ARITY;
          rtPtr = consPtr;
      } else {
          Boolean changed = HNL_makeConsArgvec(argvec, ol, nl, envlist);
          if (changed){ //new argvec is built because of pushing susp
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushCons(AM_argVec);
          } else rtPtr = consPtr;
  	HN_setEmptyEnv();
      }
      HNL_setRegsCons(rtPtr);
      return rtPtr;
  }
  
  /* (weak) head normalize application or implicit suspension over 
     application. The old application term is destructively changed into
     a reference to its head normal form or its weak head normal form if
     the weak heap normal form is not an implicit suspension (in which
     case the term skeleton must be an abstraction.).
  */
  static DF_TermPtr HN_hnormApp(DF_TermPtr appPtr, Boolean whnf)
  {
      DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
                 rtPtr; // term pointer to be returned
      DF_TermPtr oldFunPtr = funPtr;
      int        arity = DF_appArity(appPtr);
      Boolean    emptyTopEnv = HN_isEmptyEnv();
      int        myol, mynl;       //for book keeping the implicit suspension env
      DF_EnvPtr  myenvlist;        //for book keeping the implicit suspension env
      int        myarity = arity;  //book keeping the arity before contraction    
  
      if (!emptyTopEnv) {          //book keeping the current environment
          myol = ol; mynl = nl; myenvlist = envlist; 
      }
      funPtr = HN_hnormDispatch(funPtr, TRUE); //whf of the function    
      while ((arity > 0) && (DF_isLam(funPtr))) {
          //perform contraction on top-level redexes while you can
          DF_TermPtr  lamBody = DF_lamBody(funPtr); //abs body
          int         numAbsInFun = DF_lamNumAbs(funPtr);   
          int         numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
          DF_EnvPtr   newenv;
          int         newol = ol + numContract;        
  
          AM_embedError(newol);
          if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
          else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
          HN_setEnv(newol, nl, newenv);
  
          if (arity == numAbsInFun){    	  
              funPtr = HN_hnormDispatch(lamBody, whnf);
              arity = 0;
          } else if (arity > numAbsInFun) {
              funPtr = HN_hnormDispatch(lamBody, TRUE);
              argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
              arity -= numAbsInFun;
          } else {  //arity < numabsInFun
              DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
              HNL_pushLam(lamBody, (numAbsInFun-arity));
              funPtr = HN_hnormDispatch(newBody, whnf);
              arity = 0;
          }
      }// while ((arity >0) && (DF_IsLam(fun)))
      
      //update or create application
      if (arity == 0) {  //app disappears   
          rtPtr = funPtr;
          if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
      } else {           //app persists; Note: now HN_isEmptyEnv must be TRUE
          Boolean changed;
          if (emptyTopEnv) changed = HNL_makeArgvecEmpEnv(argvec, arity);
          else changed = HNL_makeArgvec(argvec,arity,myol,mynl,myenvlist);
  
          if ((!changed) && (arity == myarity) && (funPtr == oldFunPtr)) {
  	  rtPtr = appPtr;
          } else {// create new app and in place update the old if empty top env
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
              if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
          }
      }
      return rtPtr;
  }
  
  /* (weak) head normalize (explicit) suspension or implicit suspension
     with a suspension term skeletion. The explicit suspension is destructivly
     changed to its head normal form or weak head normal form in case
     that the whn is not an implicit susp itself (in which case the term
     skeleton must be an abstraction).
  */ 
  static DF_TermPtr HN_hnormSusp(DF_TermPtr suspPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      int myol, mynl ;             // for book keeping the env of implicit susp
      DF_EnvPtr myenvlist;
      Boolean   emptyTopEnv = HN_isEmptyEnv();
      
      if (!emptyTopEnv){
          myol = ol; mynl = nl; myenvlist = envlist;
      }
      //first (weak) head normalize the explicit susp
      HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
      rtPtr = HN_hnormDispatch(DF_suspTermSkel(suspPtr), whnf);
      if (emptyTopEnv) {
          if (HN_isEmptyEnv()) {
  	  HNL_updateToRef(suspPtr, rtPtr);
  	}
      } else {           // ! emptyTopEnv
          if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
          else rtPtr = HN_pushSuspOverLam(rtPtr);
          //(weak) head norm the top-level (imp) susp
          HN_setEnv(myol, mynl, myenvlist);
          /* note that AM_numabs, AM_numargs and AM_argvec have to be 
             re-initialized, because the (w)hnf of the inner suspension
             is to be traversed again. */
          HNL_initRegs();
          rtPtr = HN_hnormDispatch(rtPtr, whnf);
      }
      return rtPtr;
  }
  
  /****************************************************************************/
  /* Dispatching on various term categories.                                  */
  /****************************************************************************/
  static DF_TermPtr HN_hnormDispatch(DF_TermPtr tmPtr, Boolean whnf)
  {
    restart:
      switch (DF_termTag(tmPtr)){
      case DF_TM_TAG_VAR: 
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsFlex(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_CONST:
      case DF_TM_TAG_INT:
      case DF_TM_TAG_FLOAT:
      case DF_TM_TAG_NIL:
      case DF_TM_TAG_STR:
      case DF_TM_TAG_STREAM:
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsRig(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_BVAR:     { return HN_hnormBV(tmPtr, whnf);           }
      case DF_TM_TAG_CONS:     { return HN_hnormCons(tmPtr, whnf);         }
      case DF_TM_TAG_LAM:      { return HN_hnormLam(tmPtr, whnf);          }
      case DF_TM_TAG_APP:      { return HN_hnormApp(tmPtr, whnf);          }
      case DF_TM_TAG_SUSP:     { return HN_hnormSusp(tmPtr, whnf);         }
      case DF_TM_TAG_REF:      { tmPtr = DF_termDeref(tmPtr); goto restart;}
      }
  
      //Impossible to reach this point.
      return NULL;
  }
  
  /****************************************************************************/  
  /* the interface routine for head normalization                             */
  /****************************************************************************/
  void HN_hnorm(DF_TermPtr tmPtr)
  {    
      HN_setEmptyEnv();            
      HNL_initRegs();
      HN_hnormDispatch(DF_termDeref(tmPtr), FALSE);
  }
  
  
  /****************************************************************************/
  /*   HEAD (WEAK HEAD) NORMALIZATION WITH OCCURS CHECK                       */
  /*--------------------------------------------------------------------------*/
  /* General comments:                                                        */
  /*  Checkings are added when the (dereference of) term to be normlized is   */
  /*  an application or a cons. If the term is an application, checking is    */
  /*  made on whether the application is currently referred                   */
  /*  to by register AM_vbbreg, and this checking is added in the APP case    */
  /*  of the dispatch function. If the term is a cons, checking is made on    */
  /*  whether its argument vector is currently referred to by the register    */
  /*  AM_vbbreg, and this checking is added in sub-function HN_hnormConsOcc.  */
  /****************************************************************************/
  static DF_TermPtr HN_hnormDispatchOcc(DF_TermPtr tmPtr, Boolean whnf);
  
  /****************************************************************************/
  /* functions for (weak) head normalizing terms with occurs-check            */
  /* of known categories                                                      */
  /****************************************************************************/
  
  /* (weak) head normalize bound variable or implicit suspension with 
     bound variable as term skeleton. */
  static DF_TermPtr HN_hnormBVOcc(DF_TermPtr bvPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      if (HN_isEmptyEnv()){                        //[|#i, 0, 0, nil|] -> #i
          rtPtr = bvPtr;
          HNL_setRegsRig(bvPtr);
      } else { //non-empty env       
          int dbind = DF_bvIndex(bvPtr);
  
          if (dbind > ol) {                        //[|#i,ol,nl,e|] -> #i-ol+nl
              int newind = dbind - ol + nl;
  
              AM_embedError(newind);
              rtPtr =(DF_TermPtr)AM_hreg;
              HNL_pushBV(newind); 
              HNL_setRegsRig(rtPtr);
              HN_setEmptyEnv();
          } else { // i <= ol
              DF_EnvPtr    envitem = DF_envListNth(envlist, dbind);
              int          nladj   = nl-DF_envIndex(envitem);
  
              if (DF_isDummyEnv(envitem)){         //[|#i,ol,nl,..@l..|]->#(nl-l)
                  rtPtr = (DF_TermPtr)AM_hreg;
                  HNL_pushBV(nladj); 
                  HNL_setRegsRig(rtPtr);
                  HN_setEmptyEnv();
              }  else { //pair env    [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
                  DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
                  if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
                      int newnl = DF_suspNL(tmPtr)+nladj;
                      AM_embedError(newnl);
                      HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
                      rtPtr = HN_hnormDispatchOcc(DF_suspTermSkel(tmPtr), whnf);
                  } else {      
                      HN_setEnv(0, nladj, DF_EMPTY_ENV); 
                      rtPtr = HN_hnormDispatchOcc(tmPtr, whnf);
                  }
              }         //pair env  
          }        // i<= ol    
      }        //non-empty env
      return rtPtr;
  }
  
  /* (weak) head normalize an abstraction or implicit suspension with term
     skeleton as an abstraction. */
  static DF_TermPtr HN_hnormLamOcc(DF_TermPtr lamPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
  
      if (whnf) return rtPtr = lamPtr; //weak hn 
      else {  //whnf = FALSE
          int numabs = DF_lamNumAbs(lamPtr);
          DF_TermPtr newbody;
  
          if (HN_isEmptyEnv()){
              newbody = HN_hnormDispatchOcc(DF_lamBody(lamPtr), FALSE);
              rtPtr = lamPtr; //body must have been adjusted in place
          } else {  // non-empty env 
              //[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
              int newol = ol+numabs, newnl = nl+numabs;
              
              AM_embedError(newol);
              AM_embedError(newnl);
              HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
              newbody = HN_hnormDispatchOcc(DF_lamBody(lamPtr), FALSE);
              /* create a new lam on the result of hn the lam body */
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushLam(newbody, numabs);
          }         // non-empty env
          AM_numAbs += numabs;
      }      //whnf == FALSE
      return rtPtr;
  }
  
  /* (weak) head normalize cons or implicit suspension over cons.
     Note checking on whether the argument vector of the cons term is referred to
     by the register AM_vbbreg is made.
  */
  static DF_TermPtr HN_hnormConsOcc(DF_TermPtr consPtr, Boolean whnf)
  {
      DF_TermPtr argvec = DF_consArgs(consPtr),
                 rtPtr; //term pointer to be returned
      if (AM_vbbreg == argvec) EM_THROW(EM_FAIL);    
      if (HN_isEmptyEnv()){
          AM_argVec = argvec;
          AM_numArgs = DF_CONS_ARITY;
          rtPtr = consPtr;
      } else {
          Boolean changed = HNL_makeConsArgvec(argvec, ol, nl, envlist);
          if (changed){ //new argvec is built because of pushing susp
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushCons(AM_argVec);
          } else rtPtr = consPtr;
  	HN_setEmptyEnv();
      }
      HNL_setRegsCons(rtPtr);
      return rtPtr;
  }
  
  /* (weak) head normalize application or implicit suspension over 
     application.
  */
  static DF_TermPtr HN_hnormAppOcc(DF_TermPtr appPtr, Boolean whnf)
  {
      DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
                 rtPtr; // term pointer to be returned
      DF_TermPtr oldFunPtr = funPtr;
      int        arity = DF_appArity(appPtr);
      Boolean    emptyTopEnv = HN_isEmptyEnv();
      int        myol, mynl;       //for book keeping the implicit suspension env
      DF_EnvPtr  myenvlist;        //for book keeping the implicit suspension env
      int        myarity = arity;  //book keeping the arity before contraction
  
      if (!emptyTopEnv) {          //book keeping the current environment
          myol = ol; mynl = nl; myenvlist = envlist; 
      }
      funPtr = HN_hnormDispatchOcc(funPtr, TRUE); //whf of the function    
      while ((arity > 0) && (DF_isLam(funPtr))) {
          //perform contraction on top-level redexes while you can
          DF_TermPtr  lamBody = DF_lamBody(funPtr); //abs body
          int         numAbsInFun = DF_lamNumAbs(funPtr);   
          int         numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
          DF_EnvPtr   newenv;
          int         newol = ol + numContract;        
  
          AM_embedError(newol);
          if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
          else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
          HN_setEnv(newol, nl, newenv);
  
          if (arity == numAbsInFun){            
              funPtr = HN_hnormDispatchOcc(lamBody, whnf);
              arity = 0;
          } else if (arity > numAbsInFun) {
              funPtr = HN_hnormDispatchOcc(lamBody, TRUE);
              argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
              arity -= numAbsInFun;
          } else {  //arity < numabsInFun
              DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
              HNL_pushLam(lamBody, (numAbsInFun-arity));
              funPtr = HN_hnormDispatchOcc(newBody, whnf);
              arity = 0;
          }
      }// while ((arity >0) && (DF_IsLam(fun)))
      
      //update or create application
      if (arity == 0) {  //app disappears
          rtPtr = funPtr;
          if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
      } else {           //app persists; Note: now HN_isEmptyEnv must be TRUE
          Boolean changed;
          if (emptyTopEnv) changed = HNL_makeArgvecEmpEnv(argvec, arity);
          else changed = HNL_makeArgvec(argvec,arity,myol,mynl,myenvlist);
  
          if ((!changed) && (arity == myarity) && (oldFunPtr == funPtr)) {
  	  rtPtr = appPtr;
          } else {// create new app and in place update the old if empty top env
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
              if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
          }
      }
      return rtPtr;
  }
  
  /* (weak) head normalize (explicit) suspension or implicit suspension
     with a suspension term skeletion. 
  */ 
  static DF_TermPtr HN_hnormSuspOcc(DF_TermPtr suspPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      int myol, mynl ;             // for book keeping the env of implicit susp
      DF_EnvPtr myenvlist;
      Boolean   emptyTopEnv = HN_isEmptyEnv();
      
      if (!emptyTopEnv){
          myol = ol; mynl = nl; myenvlist = envlist;
      }
      //first (weak) head normalize the explicit susp
      HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
      rtPtr = HN_hnormDispatchOcc(DF_suspTermSkel(suspPtr), whnf);
  
      if (emptyTopEnv) {
          if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
      } else {           // ! emptyTopEnv
          if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
          else rtPtr = HN_pushSuspOverLam(rtPtr);
          //(weak) head norm the top-level (imp) susp
          HN_setEnv(myol, mynl, myenvlist);
          /* note that AM_numabs, AM_numargs and AM_argvec have to be 
             re-initialized, because the (w)hnf of the inner suspension
             is to be traversed again. */
          HNL_initRegs();
          rtPtr = HN_hnormDispatchOcc(rtPtr, whnf);
      }
      return rtPtr;
  }
  
  /****************************************************************************/
  /* Dispatching on various term categories.                                  */
  /****************************************************************************/
  static DF_TermPtr HN_hnormDispatchOcc(DF_TermPtr tmPtr, Boolean whnf)
  {
    restart_hnormOcc:
      switch (DF_termTag(tmPtr)){
      case DF_TM_TAG_VAR: 
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsFlex(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_CONST:
      case DF_TM_TAG_INT:
      case DF_TM_TAG_FLOAT:
      case DF_TM_TAG_NIL:
      case DF_TM_TAG_STR:
      case DF_TM_TAG_STREAM:
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsRig(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_BVAR:     { return HN_hnormBVOcc(tmPtr, whnf);           }
      case DF_TM_TAG_CONS:     { return HN_hnormConsOcc(tmPtr, whnf);         }
      case DF_TM_TAG_LAM:      { return HN_hnormLamOcc(tmPtr, whnf);          }
      case DF_TM_TAG_APP:      {
          if (AM_vbbreg == tmPtr) EM_THROW(EM_FAIL);
          return HN_hnormAppOcc(tmPtr, whnf);          }
      case DF_TM_TAG_SUSP:     { return HN_hnormSuspOcc(tmPtr, whnf);         }
      case DF_TM_TAG_REF:      {tmPtr=DF_termDeref(tmPtr); goto restart_hnormOcc;}
      }
  
      //Impossible to reach this point.
      return NULL;
  }
  
  /****************************************************************************/  
  /* the interface routine for head normalization                             */
  /****************************************************************************/
  void HN_hnormOcc(DF_TermPtr tmPtr)
  {    
      HN_setEmptyEnv();            
      HNL_initRegs();
      tmPtr = HN_hnormDispatchOcc(DF_termDeref(tmPtr), FALSE);
  }
  
  
  /****************************************************************************/
  /*               FULL NORMALIZATION                                         */
  /****************************************************************************/
  static DF_TermPtr HN_lnormDispatch(DF_TermPtr, Boolean whnf);
  
  /****************************************************************************/
  /* Functions for creating argument vectors in full normalization            */
  /*--------------------------------------------------------------------------*/
  /* General comments:                                                        */
  /*  This is the counter part of HNL_makeArgvec functions (hnormlocal.c)     */
  /*  in the full normalization process for arranging arguments of            */
  /*  applications (cons) when their "heads" are in (head) normal forms.      */
  /*  Nested applications are unfolded.                                       */
  /*  The difference is that HN_lnormDispatch is invoked on each argument     */
  /*  to fully normalize it.                                                  */
  /****************************************************************************/
  
  /* Fully normalize (implicit) suspensions [| ai, myol, mynl, myenv |],
     where ai's are those in the vector referred to by argvec with size arity,
     and myol, mynl, myenv are given by other parameters.
     Note that a new argument vector is always created.
  */
  static void HN_lnormArgvec(DF_TermPtr argvec, int arity, int myol, int mynl, 
                             DF_EnvPtr myenv)
  {
      int i;
      //book keeping relevant regs.  
      DF_TermPtr head      = AM_head,    myArgvec = AM_argVec;
      int        numAbs    = AM_numAbs,  numArgs  = AM_numArgs;
      Flag       rigFlag   = AM_rigFlag, consFlag = AM_consFlag;
  
      MemPtr     newArgvec = AM_hreg;   //new argvec
      MemPtr     newhtop   = newArgvec + arity * DF_TM_ATOMIC_SIZE;   
      AM_heapError(newhtop);
      AM_hreg = newhtop;       //arrange heap top for creating terms in norm args
  
      for (i = 1; i <= arity; i++){
          HN_setEnv(myol, mynl, myenv);   //imp susp environment
          HNL_initRegs();
          DF_mkRef(newArgvec, HN_lnormDispatch(argvec, FALSE));
          newArgvec += DF_TM_ATOMIC_SIZE;
          argvec = (DF_TermPtr)(((MemPtr)argvec)+DF_TM_ATOMIC_SIZE);
      }
      //reset registers
      AM_head    = head;             AM_argVec   = myArgvec;
      AM_numAbs  = numAbs;           AM_numArgs  = numArgs;
      AM_rigFlag = rigFlag;          AM_consFlag = consFlag;
  }
  
  /* A specialized version of HN_lnormArgvec when the implicit suspension
     over each argument in the vector is known to be empty.
     Note that upon the return of HN_lnormDispatch, the argument has been 
     destructively updated to its normal form, which means the old argument
     vector is always used.
  */
  static void HN_lnormArgvecEmpEnv(DF_TermPtr argvec, int arity)
  {
      int i;
      //book keeping relevant regs.  
      DF_TermPtr head      = AM_head,    myArgvec = AM_argVec;
      int        numAbs    = AM_numAbs,  numArgs  = AM_numArgs;
      Flag       rigFlag   = AM_rigFlag, consFlag = AM_consFlag;
      
      for (i = 1; i <= arity; i++){
          HNL_initRegs();
          HN_lnormDispatch(argvec, FALSE);
          argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
      }
      //reset registers
      AM_head    = head;             AM_argVec   = myArgvec;
      AM_numAbs  = numAbs;           AM_numArgs  = numArgs;
      AM_rigFlag = rigFlag;          AM_consFlag = consFlag;
  }    
  
  /* Create an argument vector for applications within a non-empty environment.
     Actions are carried out in two steps:
     First, nested applications are unfolded if arising. Second, the (implicit)
     suspensions formed by each argument and given parameters are fully 
     normalized.
     Note that a new argument vector is always created.
  */
  static Boolean HN_makeArgvecLnorm(DF_TermPtr argvec, int arity, int myol, 
                                    int mynl, DF_EnvPtr myenv)
  {
      DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg; //new argvec
      int        newArity;
  
      if (AM_numArgs != 0){      //unfold nested app first
          MemPtr newhtop  = AM_hreg + AM_numArgs * DF_TM_ATOMIC_SIZE;
          AM_heapError(newhtop);
          newArity = arity + AM_numArgs;
          AM_arityError(newArity);
          HNL_copyArgs(AM_argVec, AM_numArgs);  //layout inner args
      } else newArity = arity;
      
      //fully normalize arguments
      HN_lnormArgvec(argvec, arity, myol, mynl, myenv);
      AM_argVec = newArgvec;
      AM_numArgs = newArity;
      return TRUE;
  }
  
  /* A specilized version of HN_makeArgvecLnorm when the enclosing environment 
     is known to be empty. Note that new argument vecoter is created 
     if nested applications were unfolded. Otherwise, the old is used.
     Boolean values TRUE or FALSE is returned to inidicate which situation it is.
  */ 
  static Boolean HN_makeArgvecEmpEnvLnorm(DF_TermPtr argvec, int arity)
  {
      HN_lnormArgvecEmpEnv(argvec, arity);          //lnorm arguments
  
      if (AM_numArgs != 0){                           //unfold nested app 
          int        newArity  = arity + AM_numArgs;
          DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg; //new argument vector
          AM_arityError(newArity);
          AM_heapError(((MemPtr)newArgvec + newArity * DF_TM_ATOMIC_SIZE));
  
          HNL_copyArgs(AM_argVec, AM_numArgs);
          HNL_copyArgs(argvec, arity);
          
          AM_argVec = newArgvec;
          AM_numArgs = newArity;
          return TRUE;
      } else {
          AM_argVec = argvec;
          AM_numArgs = arity;
          return FALSE;
      }
  }
  
  /****************************************************************************/
  /* functions for fully normalizing terms of known categories                */
  /*--------------------------------------------------------------------------*/
  /* General comments:                                                        */
  /*                                                                          */
  /*  An implicit suspension is given by the global variables ol, nl and      */
  /*  envlist together with the first argument tmPtr to the sub-functions:    */
  /*  [|tmPtr, ol, nl, envlist|]                                              */
  /*  The suspension environment could be empty in which case the term        */
  /*  being normalized is tmPtr itself.                                       */
  /*  The second argument of the sub-functions whnf is a flag indicating      */
  /*  whether a head normal form or a weak head normal form is being          */
  /*  computed.                                                               */ 
  /****************************************************************************/
  
  /* Fully normalize or weak head normalize bound variable or implicit 
     suspension with bound variable as term skeleton. 
     The actions carried out are the same as the counter part in the head 
     normalization proceee, except that HN_lnormDispatch is invoked as opposed
     to HN_hnormDispatch when necessary.
  */
  static DF_TermPtr HN_lnormBV(DF_TermPtr bvPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      if (HN_isEmptyEnv()){                        //[|#i, 0, 0, nil|] -> #i
          rtPtr = bvPtr;
          HNL_setRegsRig(bvPtr);
      } else { //non-empty env       
          int dbind = DF_bvIndex(bvPtr);
  
          if (dbind > ol) {                        //[|#i,ol,nl,e|] -> #i-ol+nl
              int newind = dbind - ol + nl;
  
              AM_embedError(newind);
              rtPtr =(DF_TermPtr)AM_hreg;
              HNL_pushBV(newind); 
              HNL_setRegsRig(rtPtr);
              HN_setEmptyEnv();
          } else { // i <= ol
              DF_EnvPtr    envitem = DF_envListNth(envlist, dbind);
              int          nladj   = nl-DF_envIndex(envitem);
  
              if (DF_isDummyEnv(envitem)){         //[|#i,ol,nl,..@l..|]->#(nl-l)
                  rtPtr = (DF_TermPtr)AM_hreg;
                  HNL_pushBV(nladj); 
                  HNL_setRegsRig(rtPtr);
                  HN_setEmptyEnv();
              }  else { //pair env    [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
                  DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
                  if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
                      int newnl = DF_suspNL(tmPtr)+nladj;
                      AM_embedError(newnl);
                      HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
                      rtPtr = HN_lnormDispatch(DF_suspTermSkel(tmPtr), whnf);
                  } else {      
                      HN_setEnv(0, nladj, DF_EMPTY_ENV); 
                      rtPtr = HN_lnormDispatch(tmPtr, whnf);
                  }
              }         //pair env  
          }        // i<= ol    
      }        //non-empty env
      return rtPtr;
  }
  
  /* Fully normalize or weak head normalize abstractions or implicit suspension 
     with abstractions as term skeletons. 
     The actions carried out are the same as the counter part in the head 
     normalization process, except that HN_lnormDispatch is invoked as opposed
     to HN_hnormDispatch when necessary.
  */
  static DF_TermPtr HN_lnormLam(DF_TermPtr lamPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      if (whnf) return rtPtr = lamPtr; //weak hn 
      else {  //whnf = FALSE
          int numabs = DF_lamNumAbs(lamPtr);
          DF_TermPtr newbody;
  
          if (HN_isEmptyEnv()){
              newbody = HN_lnormDispatch(DF_lamBody(lamPtr), FALSE);
              rtPtr = lamPtr; //body must have been adjusted in place
          } else {  // non-empty env 
              //[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
              int newol = ol+numabs, newnl = nl+numabs;
              
              AM_embedError(newol);
              AM_embedError(newnl);
              HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
              newbody = HN_lnormDispatch(DF_lamBody(lamPtr), FALSE);
              /* create a new lam on the result of hn the lam body */
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushLam(newbody, numabs);
          }         // non-empty env
          AM_numAbs += numabs;
      }      //whnf == FALSE
      return rtPtr;
  }
  
  /* Fully normalize or weak head normalize cons or implicit suspension over 
     cons. The difference from HN_hnormCons is that the arguments of the cons
     are fully normalized.          
  */
  static DF_TermPtr HN_lnormCons(DF_TermPtr consPtr, Boolean whnf)
  {
      DF_TermPtr argvec = DF_consArgs(consPtr),
                 rtPtr; //term pointer to be returned
      if (HN_isEmptyEnv()){
          HN_lnormArgvecEmpEnv(argvec, DF_CONS_ARITY);
          AM_argVec = argvec;
          AM_numArgs = DF_CONS_ARITY;
          rtPtr = consPtr;
      } else {
          DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg;  //new argument vector
          HN_lnormArgvec(argvec, DF_CONS_ARITY, ol, nl, envlist);
          AM_argVec = newArgvec;
          AM_numArgs = DF_CONS_ARITY;
          rtPtr = (DF_TermPtr)AM_hreg;
          HNL_pushCons(AM_argVec);
  	HN_setEmptyEnv();
      }
      HNL_setRegsCons(rtPtr);
      return rtPtr;
  }
  
  /* Fully normalize or weak head normalize application or implicit suspension 
     over application. The actions carried out here is the same as those in
     HN_hnormApp except that HN_lnormDispatch is invoked as HN_hnormDispatch, and
     in making argument vectors makeArgvecLnorm functions are used to fully
     normalize the arguments.
  */
  static DF_TermPtr HN_lnormApp(DF_TermPtr appPtr, Boolean whnf)
  {
      DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
                 rtPtr; // term pointer to be returned
      DF_TermPtr oldFunPtr = funPtr;
      int        arity = DF_appArity(appPtr);
      Boolean    emptyTopEnv = HN_isEmptyEnv();
      int        myol, mynl;       //for book keeping the implicit suspension env
      DF_EnvPtr  myenvlist;        //for book keeping the implicit suspension env
      int        myarity = arity;  //book keeping the arity before contraction
  
      if (!emptyTopEnv) {          //book keeping the current environment
          myol = ol; mynl = nl; myenvlist = envlist; 
      }
      funPtr = HN_lnormDispatch(funPtr, TRUE); //whf of the function    
      while ((arity > 0) && (DF_isLam(funPtr))) {
          //perform contraction on top-level redexes while you can
          DF_TermPtr  lamBody = DF_lamBody(funPtr); //abs body
          int         numAbsInFun = DF_lamNumAbs(funPtr);   
          int         numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
          DF_EnvPtr   newenv;
          int         newol = ol + numContract;        
  
          AM_embedError(newol);
          if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
          else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
          HN_setEnv(newol, nl, newenv);
  
          if (arity == numAbsInFun){            
              funPtr = HN_lnormDispatch(lamBody, whnf);
              arity = 0;
          } else if (arity > numAbsInFun) {
              funPtr = HN_lnormDispatch(lamBody, TRUE);
              argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
              arity -= numAbsInFun;
          } else {  //arity < numabsInFun
              DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
              HNL_pushLam(lamBody, (numAbsInFun-arity));
              funPtr = HN_lnormDispatch(newBody, whnf);
              arity = 0;
          }
      }// while ((arity >0) && (DF_IsLam(fun)))
      
      //update or create application
      if (arity == 0) {  //app disappears
          rtPtr = funPtr;
          if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
      } else {           //app persists; Note: now HN_isEmptyEnv must be TRUE
          Boolean changed;
          if (emptyTopEnv) changed = HN_makeArgvecEmpEnvLnorm(argvec, arity);
          else changed = HN_makeArgvecLnorm(argvec,arity,myol,mynl,myenvlist);
  
          if ((!changed) && (arity == myarity) && (oldFunPtr == funPtr)) { 
  	  rtPtr = appPtr;
          } else {// create new app and in place update the old if empty top env
              rtPtr = (DF_TermPtr)AM_hreg;
              HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
              if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
          }
      }
      return rtPtr;
  }
  
  /* Fuuly normlize or weak head normalize (explicit) suspension or implicit 
     suspension with a suspension term skeletion. The actions are the same
     as those in HN_hnormSusp except that HN_lnormDispatch is used as opposed
     to HN_hnormSusp with one exception: when the environment of the top-level
     suspension is not empty, the inner suspension is head normalized
     (HN_hnormDispatch).
  */
  
  static DF_TermPtr HN_lnormSusp(DF_TermPtr suspPtr, Boolean whnf)
  {
      DF_TermPtr rtPtr; //term pointer to be returned
      int        myol, mynl; // for book keeping the env of implicit susp
      DF_EnvPtr  myenvlist;
      Boolean    emptyTopEnv = HN_isEmptyEnv();
      
      if (!emptyTopEnv) {
          myol = ol; mynl = nl; myenvlist = envlist;
      }
      HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
  
      if (emptyTopEnv){
          rtPtr = HN_lnormDispatch(DF_suspTermSkel(suspPtr), whnf);
          if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
      } else {          //non-empty top-level env
          rtPtr = HN_hnormDispatch(DF_suspTermSkel(suspPtr), whnf);
      
          if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
          else rtPtr = HN_pushSuspOverLam(rtPtr);
          //fully normalize top-level susp
          HN_setEnv(myol, mynl, myenvlist);        
          /* note that AM_numabs, AM_numargs and AM_argvec have to be 
             re-initialized, because the (w)hnf of the inner suspension
             is to be traversed again. */
          HNL_initRegs();
          rtPtr = HN_lnormDispatch(rtPtr, whnf);
      }
      return rtPtr;
  }
  
  /****************************************************************************/
  /* Dispatching on various term categories.                                  */
  /****************************************************************************/
  static DF_TermPtr HN_lnormDispatch(DF_TermPtr tmPtr, Boolean whnf)
  {
    restart_lnorm:
      switch (DF_termTag(tmPtr)){
      case DF_TM_TAG_VAR: 
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsFlex(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_CONST:
      case DF_TM_TAG_INT:
      case DF_TM_TAG_FLOAT:
      case DF_TM_TAG_NIL:
      case DF_TM_TAG_STR:
      case DF_TM_TAG_STREAM:
      {
          if (!HN_isEmptyEnv()) HN_setEmptyEnv();
          HNL_setRegsRig(tmPtr);
          return tmPtr;
      }
      case DF_TM_TAG_BVAR:     { return HN_lnormBV(tmPtr, whnf);           }
      case DF_TM_TAG_CONS:     { return HN_lnormCons(tmPtr, whnf);         }
      case DF_TM_TAG_LAM:      { return HN_lnormLam(tmPtr, whnf);          }
      case DF_TM_TAG_APP:      { return HN_lnormApp(tmPtr, whnf);          }
      case DF_TM_TAG_SUSP:     { return HN_lnormSusp(tmPtr, whnf);         }
      case DF_TM_TAG_REF:      { tmPtr = DF_termDeref(tmPtr); goto restart_lnorm;}
      }
  
      //Impossible to reach this point.
      return NULL;
  }
  
  /****************************************************************************/  
  /* the interface routine for head normalization                             */
  /****************************************************************************/
  void HN_lnorm(DF_TermPtr tmPtr)
  {    
      HN_setEmptyEnv();            
      HNL_initRegs();
      tmPtr = HN_lnormDispatch(DF_termDeref(tmPtr), FALSE);
  }
  
  #endif //HNORM_C
  
  
  
  
  
  
  
  
  
  
  
  