/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 ******************************************************************
 *  $Log$
 ******************************************************************/

#ifndef lint
static char rcsid[]= "$Id$";
#endif

/******************************************************************
 *
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *
 *  8 Jan 1990
 *
 *  Internal Tables
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : activate debugging
 *
 *  LOG:
 *     11/07/92. dlarra.
 *     Masks in the gate table are deallocated.
 *
 *     06/09/92. emilla.
 *     Included functions to maintain information about operations
 *     with the same name in order to know when they must be
 *     printed with the "of sort" qualification.
 *
 *
 ******************************************************************/

/* LINTLIBRARY */

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "batables.h"
#include "limisc.h"
#include "listdout.h"
#include "listrbk.h"
#include "babeh.h"
#include "baattr.h"
#include "badefca.h"
#include "batyperw.h"


/******************************************************************
 *                                                                *
 *                         The Tables                             *
 *                                                                *
 ******************************************************************/


/*
 *  Increments of the size of the tables
 *
 */

#define VAR_BLOCK_INDEX_BITS 10 /* INC_VAR_TABLE index bits */
#define INC_VAR_TABLE 1024      /* := Power(2,VAR_BLOCK_INDEX_BITS) */
#define SEGMENT(n) (n>>VAR_BLOCK_INDEX_BITS)
#define OFFSET(n) (n&~((~0)<<VAR_BLOCK_INDEX_BITS))
#define INC_SORT_TABLE 128
#define INC_PROC_TABLE 1024
#define INC_OPER_TABLE 256


typedef struct { GtableEntryTyp gate[MAX_GATE_TABLE];
		 DescriptorTyp  last;
	       } GateTableTyp;

typedef DescriptorTyp *VarSegmentTyp;

typedef struct { VtableEntryTyp *var;
		 VarSegmentTyp  *evar;
		 DescriptorTyp  vlast, evnext;
		 int            vsize, evsize;
	       } VarTableTyp;


typedef struct { OtableEntryTyp *oper;
		 DescriptorTyp  last;
		 int                size;
		 boolean        tableOfsort;
	       } OperTableTyp;


typedef struct { StableEntryTyp *sort;
		 DescriptorTyp  last;
		 int                size;
	       } SortTableTyp;


typedef struct { PtableEntryTyp *proc;
		 DescriptorTyp   last;
		 int             size;
	       } ProcTableTyp;


static GateTableTyp  gTab;
static VarTableTyp   vTab;
static OperTableTyp  oTab;
static ProcTableTyp  pTab;
static SortTableTyp  sTab;

/******************************************************************
 *                                                                *
 *                         Table of Gates                         *
 *                                                                *
 ******************************************************************/

/* Store_gate
 * Insert a gate in gTab if it is not already in the table.
 * Return the position in the table.
 */
DescriptorTyp Store_gate( name )
     char *name;
{
  DescriptorTyp dg;

  dg = FindG(name);
  return dg==0 ? Declare_gate(name) : dg ;
}

/*--------------------------------------------------------------------------*/

/* Declare_gate
 * Insert a new gate in gTab.
 * Return the position of the new entry in the table.
 */
DescriptorTyp Declare_gate( name )
     char *name;
{
  gTab.last++;
  if (gTab.last >= MAX_GATE_TABLE)
    Error("Maximum number of gates exceeded.\n       Increase the constant: MAX_GATE_TABLE");
  gTab.gate[gTab.last].name = name;
  gTab.gate[gTab.last].mask = Descr_to_Mask(gTab.last);
  return gTab.last;
}

/*--------------------------------------------------------------------------*/

/* GetG_name
 * Return the name of the gate whose descriptor is d.
 */
char * GetG_name( d )
     DescriptorTyp  d;
{
  LASSERT(gTab.last >= d);
  return gTab.gate[d].name;
}


/*----------------------------------------------------------------*/

/* GetG_mask
 * Return the mask of the gate whose descriptor is d.
 */
GateMaskTyp GetG_mask( d )
     DescriptorTyp  d;
{
  LASSERT(gTab.last >= d);
  return gTab.gate[d].mask;
}


/*----------------------------------------------------------------*/

/* PutG_mask
 * Put the mask m to the gate whose desriptor is d.
 */
void PutG_mask( d, m )
     DescriptorTyp d;
     GateMaskTyp   m;
{
  LASSERT(gTab.last >= d);
  gTab.gate[d].mask = m;
}


/*--------------------------------------------------------------------------*/

/* FindG_byMask
 * Return the gate associated to the mask m
 */
DescriptorTyp FindG_byMask( m )
     GateMaskTyp  m;
{
  return Mask_to_Descr(m);
}

/*----------------------------------------------------------------*/

/* FindG
 * Return the position of the gate name in the table.
 * 0 if it is not found.
 */
DescriptorTyp FindG( name )
     char  *name;
{
  DescriptorTyp i;

  for (i=1 ; i<=gTab.last ; i++ )
    if (strcmp(gTab.gate[i].name,name)==0)
      break;
  if ( i>gTab.last )
    return 0;
  else
    return i;
}

/*--------------------------------------------------------------------------*/

/* PrintG
 * Print the name of the gate d.
 * pstr is the function used to print strings.
 */
void PrintG( d, pstr )
     DescriptorTyp d;
     void        (*pstr)();
{
  LASSERT(gTab.last>=d);
  pstr(gTab.gate[d].name);
}

/*----------------------------------------------------------------*/

/* SPrintG
 *  Make a string with a gate name.
 */
char * SPrintG( d )
     DescriptorTyp d;
{
  LASSERT(gTab.last>=d);
  return CopyString(gTab.gate[d].name);
}

/*----------------------------------------------------------------*/

/* LastTableG
 * Return the size of the gate table, where the last elements is stored.
 */
DescriptorTyp LastTableG()
{
  return gTab.last;
}

/*----------------------------------------------------------------*/

/* sizeG
 * Return the size of the gate table, a fixed value.
 */
static int sizeG()
{
  return MAX_GATE_TABLE;
}

/*----------------------------------------------------------------*/

/* PrintTableG
 * Print the gate table from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableG( l, h, pstr )
     DescriptorTyp l,h;
     void        (*pstr)();
{
  DescriptorTyp i;
  char          buff[15];

  pstr("\nTABLE OF GATES:\n\n");
  for ( i=l ; (i<=h) && (i<=gTab.last) ; i++ ) {
    (void)sprintf(buff,"%-2d",i);
    pstr(buff);
    pstr(" = ");
    pstr(gTab.gate[i].name);
#ifdef SDEBUG
    { DescriptorTyp j;

      pstr(" (");
      for ( j=0 ; j < GATESET_WORDS; j++ ) {
	pstr(" ");
	PrintInt(pstr,(int)(*(gTab.gate[i].mask+j)));
      }
      pstr(" )\n");
    }
#else
    pstr("\n");
#endif
  }
}

/*--------------------------------------------------------------------------*/

/* CleanGateTable
 * Clean the table of gates, and resets it to empty.
 */
static void CleanGateTable()
{
  int i ;

  for (i=1 ; i<=gTab.last ; i++) {
    FreeGS(gTab.gate[i].mask);
  }
  gTab.last = 0;
}

/******************************************************************
 *                                                                *
 *                      Table of Variables                        *
 *                                                                *
 ******************************************************************/

/* CreateVTab
 * Allocate memory for the table of variables.
 * Reset the table.
 */
static void CreateVTab()
{
  vTab.vlast   = 0;
  vTab.vsize   = INC_VAR_TABLE;
  vTab.var     =(VtableEntryTyp*)emalloc(INC_VAR_TABLE*sizeof(VtableEntryTyp));
  vTab.evnext  = 1;
  vTab.evsize  = INC_VAR_TABLE;
  vTab.evar    = (VarSegmentTyp*)emalloc(sizeof(VarSegmentTyp));
  vTab.evar[0] =
    (VarSegmentTyp)emalloc(INC_VAR_TABLE*sizeof(DescriptorTyp));
}

/*----------------------------------------------------------------*/

/* CleanVarTable
 */
static void CleanVarTable()
{
  int i;

  free((char*)vTab.var);
  for ( i=0; i<(vTab.evsize/INC_VAR_TABLE); i++ )
    free((char*)vTab.evar[i]);
  free((char*)vTab.evar);
  CreateVTab();
}

/*----------------------------------------------------------------*/

/* ReallocVTab
 * Allocate more memory for the table of variables.
 */
static void ReallocVTab()
{
  vTab.var = (VtableEntryTyp*) erealloc((void*)vTab.var,
					(vTab.vsize + INC_VAR_TABLE)
					*sizeof(VtableEntryTyp));
  if (vTab.var ==NULL)
    Error("Tables -> run out of memory for variable table.");
  vTab.vsize += INC_VAR_TABLE;
}

/*----------------------------------------------------------------*/

/* ReallocEVTab
 * Allocate more memory for the table of equal variables entries.
 */
static void ReallocEVTab()
{
  vTab.evar = (VarSegmentTyp*) erealloc((void*)vTab.evar,
					(vTab.evsize/INC_VAR_TABLE+1)
					*sizeof(VarSegmentTyp)
					);
  vTab.evar[vTab.evsize/INC_VAR_TABLE] =
    (DescriptorTyp*)emalloc(INC_VAR_TABLE*sizeof(DescriptorTyp));

  if (vTab.evar ==NULL)
    Error("Tables -> run out of memory for variable table.");
  vTab.evsize += INC_VAR_TABLE;
}

/*----------------------------------------------------------------*/

/* Declare_var
 * Insert a new variable in vTab and
 * return the position of the new entry in the table.
 */
DescriptorTyp Declare_var( name, sort )
     char *name;
     int   sort;
{
  if (vTab.vlast+1 == vTab.vsize)
    ReallocVTab();
  vTab.vlast++;
  vTab.var[vTab.vlast].name = name;
  vTab.var[vTab.vlast].sort = sort;

  vTab.evar[SEGMENT(vTab.evnext)][OFFSET(vTab.evnext)] = vTab.vlast;
  vTab.evnext++;
  if ( vTab.evnext == vTab.evsize )
    ReallocEVTab();

  return -vTab.evnext+1;
}

/*--------------------------------------------------------------------------*/

/* GetV_name
 * Return the name of the variable whose descriptor is d.
 */
char* GetV_name( d )
     DescriptorTyp d;
{
  LASSERT((vTab.evnext >= -d) && (-d>0));
  return vTab.var[vTab.evar[SEGMENT(-d)][OFFSET(-d)]].name;
}

/*--------------------------------------------------------------------------*/

/* GetV_sort
 * Return the sort of the variable whose descriptor is d.
 */
DescriptorTyp GetV_sort( d )
     DescriptorTyp d;
{
  LASSERT((vTab.evnext >= -d) && (-d>0));
  return vTab.var[vTab.evar[SEGMENT(-d)][OFFSET(-d)]].sort;
}

/*--------------------------------------------------------------------------*/

/* PutV_sort
 * Put the sort to the variable whose descriptor is d.
 */
DescriptorTyp PutV_sort( d, sort )
     DescriptorTyp d, sort;
{
  LASSERT((vTab.evnext >= -d) && (-d>0));
  return vTab.var[vTab.evar[SEGMENT(-d)][OFFSET(-d)]].sort=sort;
}

/*----------------------------------------------------------------*/

/* EqualV_entry
 * Create an entry equal to d and return its new descriptor.
 */
DescriptorTyp EqualV_entry( d )
     DescriptorTyp d;
{
  LASSERT((vTab.evnext >= -d) && (-d>0));
  vTab.evar[SEGMENT(vTab.evnext)][OFFSET(vTab.evnext)] =
    vTab.evar[SEGMENT(-d)][OFFSET(-d)];
  vTab.evnext++;
  if ( vTab.evnext == vTab.evsize )
    ReallocEVTab();
  return -vTab.evnext+1;
}

/*----------------------------------------------------------------*/

/* FindV
 * Return the position of the variable name of a given sort in the table
 * of variables. 0 if it is not found.
 */
DescriptorTyp FindV( name, sort )
     char          *name;
     DescriptorTyp  sort;
{
  DescriptorTyp i;

  for (i=1 ; i<vTab.evnext ; i++ )
    if ( GetV_sort(-i)==sort && (strcmp(GetV_name(-i),name)==0) )
      break;
  if ( i==vTab.evnext )
    return 0;
  else
    return -i;
}

/*----------------------------------------------------------------*/

/* PrintV
 * Print the name and the sort(optional) of the variable d.
 * pstr is the function used to print strings.
 */
void PrintV( d, sort, pstr )
     DescriptorTyp   d;
     boolean         sort;
     void           (*pstr)();
{
  char * str;

  str = SPrintV( d, sort );
  pstr(str);
  (void)free(str);
}

/*----------------------------------------------------------------*/

/* SPrintV
 * Return a string with a variable name and its sort printed.
 */
char * SPrintV( d, sort )
     DescriptorTyp d;
     boolean       sort;
{
  char    * str;
  StrBckTyp strBck;

  LASSERT((vTab.evnext >= -d) && (-d>0));
  strBck = CreateStrBck();
  strBck = ConcatStrBck( strBck,GetV_name(d) );
  strBck = ConcatStrBck( strBck,"_");
  strBck = ConcatIntStrBck( strBck, -d );
  if ( sort ){
    strBck  = ConcatStrBck( strBck, ":" );
    strBck  = ConcatStrBck( strBck,GetS_name(GetV_sort(d)) );
  }
  str    = GetStrStrBck( strBck );
  FreeStrBck( strBck );
  return str;
}

/*----------------------------------------------------------------*/

/* LastTableV
 * Return the size of the variable table, where the last elements is stored.
 */
DescriptorTyp LastTableV()
{
  return (vTab.evnext)-1;
}

/*----------------------------------------------------------------*/

/* ReleaseRangeTableV
 * Release a range of variables: from a given position to the end of the table,
 * so that from-1 becomes LastTableV() becomes from-1.
 */
void ReleaseRangeTableV( from )
     DescriptorTyp from;
{
  LASSERT( from<=vTab.evnext );
  vTab.evnext = from;
}

/*----------------------------------------------------------------*/

/* sizeV
 * Return the size of the variable table.
 */
static int sizeV()
{
  return vTab.evsize;
}

/*----------------------------------------------------------------*/

/* PrintTableV
 * Print the table of variables from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableV( l, h, pstr )
     DescriptorTyp   l,h;
     void          (*pstr)();
{
  DescriptorTyp i;
  char          buff[15];

  pstr("\nTABLE OF VARIABLES:\n\n");
  for (i=l ; (i<=h) && (i<vTab.evnext) ; i++) {
    (void)sprintf(buff,"%-2d",i);
    pstr(buff);
    pstr(" = ");
    pstr(GetV_name(-i));
    pstr("_");
    PrintInt(pstr,i);
    pstr(" : ");
    pstr(sTab.sort[GetV_sort(-i)].name);
    pstr(" (");
    PrintInt(pstr,GetV_sort(-i));
    pstr(")\n");
  }
}


/******************************************************************
 *                                                                *
 *                     Table of operations                        *
 *                                                                *
 ******************************************************************/

static void Free_rw();

/* CleanOperTable
 * Clean the table of operations, and reset it to empty.
 */
static void CleanOperTable()
{
  int i ;

  for ( i=0 ; i<=oTab.last ; i++ ) {
    Disp_list(oTab.oper[i].argl);
    Free_list(oTab.oper[i].rwlist,Free_rw);
    Disp_list(oTab.oper[i].ofsortopl);
    FreePMT( oTab.oper[i].pmt );
    free( oTab.oper[i].name );
  }
  oTab.last           = 0;
  oTab.tableOfsort    = FALSE;
  oTab.oper[0].rwlist = Create_list();
  oTab.oper[0].pmt    = NULL;
  InitPMT();
}

/*-------------------------------------------------------------------------*/

/* CreateOTab
 * Allocate memory for the table of operations.
 * Reset the table.
 */
static void CreateOTab()
{
  oTab.oper  = (OtableEntryTyp*)emalloc(INC_OPER_TABLE*sizeof(OtableEntryTyp));
  oTab.size              = INC_OPER_TABLE;
  oTab.last              = 0;
  oTab.tableOfsort       = FALSE;
  oTab.oper[0].sort      = 0;
  oTab.oper[0].infix     = FALSE;
  oTab.oper[0].ofsort    = FALSE;
  oTab.oper[0].ofsortopl = Create_list();
  oTab.oper[0].argl      = Create_list();
  oTab.oper[0].rwlist    = Create_list();
  oTab.oper[0].name      = (char*)emalloc(5);
  (void)sprintf(oTab.oper[0].name,"%s","NULL");
  oTab.oper[0].pmt       = NULL;
  InitPMT();
}

/*-------------------------------------------------------------------------*/

/* ReallocOTab
 * Allocate more memory for the table of operations.
 */
static void ReallocOTab()
{
  oTab.oper = (OtableEntryTyp*)erealloc((void*)oTab.oper,
					(oTab.size + INC_OPER_TABLE)
					*sizeof(OtableEntryTyp));
  if (oTab.oper ==NULL)
    Error("Tables -> run out of memory for operation table.");
  oTab.size +=  INC_OPER_TABLE;
}

/*--------------------------------------------------------------------------*/

/* Declare_opn
 * Insert a new operation in oTab.
 * Return the position of the new entry in the table.
 */
DescriptorTyp Declare_opn( name, argl, sort, infix, rwlist )
     char          *name;
     ListTyp        argl;
     int            sort;
     boolean        infix;
     RewRuleListTyp rwlist;
{
  DescriptorTyp i;

  if (oTab.last+1 == oTab.size)
    ReallocOTab();
  oTab.last++;
  oTab.oper[oTab.last].name      = name;
  oTab.oper[oTab.last].sort      = sort;
  oTab.oper[oTab.last].infix     = infix;
  oTab.oper[oTab.last].argl      = argl;
  oTab.oper[oTab.last].rwlist    = rwlist;
  oTab.oper[oTab.last].ofsort    = FALSE;
  oTab.oper[oTab.last].ofsortopl = Create_list();
  oTab.oper[oTab.last].pmt       = NULL;
  for (i=1 ; i<oTab.last ; i++ )
    if ((strcmp(oTab.oper[i].name,name)==0) &&
	(Length_list(oTab.oper[i].argl)==Length_list(argl)) &&
	(oTab.oper[i].infix==infix)) {
      oTab.tableOfsort               = TRUE;
      oTab.oper[i].ofsort            = TRUE;
      oTab.oper[oTab.last].ofsort    = TRUE;
      oTab.oper[i].ofsortopl         = Insert_list((DataListTyp)oTab.last,
						   oTab.oper[i].ofsortopl);
      oTab.oper[oTab.last].ofsortopl
	= Insert_list((DataListTyp)i, oTab.oper[oTab.last].ofsortopl);
    }
  oTab.oper[oTab.last].ofsortopl = Insert_list((DataListTyp)oTab.last,
					       oTab.oper[oTab.last].ofsortopl);
  return oTab.last;
}

/*----------------------------------------------------------------*/

/* GetO_name
 * Return the name of the operation whose descriptor is d.
 */
char* GetO_name( d )
     DescriptorTyp      d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].name;
}

/*----------------------------------------------------------------*/

/* GetO_sort
 * Return the sort of the operation whose descriptor is d.
 */
DescriptorTyp GetO_sort( d )
     DescriptorTyp       d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].sort;
}

/*----------------------------------------------------------------*/

/* GetO_infix
 * Return true if the operation whose descriptor is d is infix.
 */
boolean GetO_infix( d )
     DescriptorTyp d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].infix;
}

/*----------------------------------------------------------------*/

/* GetO_tableOfsort
 * Return true if there are operations with "of sort" conflict in
 * the table; false otherwise.
 */
boolean GetO_tableOfsort()
{
  return oTab.tableOfsort;
}

/*----------------------------------------------------------------*/

/* GetO_ofsort
 * Return true if the operation, whose descriptor is d,
 * is "of sort" type.
 */
boolean GetO_ofsort( d )
     DescriptorTyp      d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].ofsort;
}

/*----------------------------------------------------------------*/

/* GetO_ofsortopl
 * Return the list of operations in ofsort conflict with the operation d
 */
ListTyp GetO_ofsortopl( d )
     DescriptorTyp d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].ofsortopl;
}

/*----------------------------------------------------------------*/

/* GetO_argl
 * Return the argument list of the operation whose descriptor is d.
 */
ListTyp GetO_argl( d )
     DescriptorTyp d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].argl;
}

/*----------------------------------------------------------------*/

/* GetO_pmt
 * Return the pattern match tree of the operation whose descriptor is d.
 */
PMatchTreeTyp GetO_pmt( d )
     DescriptorTyp      d;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].pmt;
}

/*----------------------------------------------------------------*/

/* PutO_argl
 * Put the argument list of the operation whose descriptor is d.
 */
void PutO_argl( d,al )
     DescriptorTyp  d;
     ListTyp       al;
{
  LASSERT(oTab.last >= d);
  oTab.oper[d].argl = al;
}

/*--------------------------------------------------------------------------*/

/* PutO_sort
 * Put the sort to the operation whose descriptor is d.
 */
DescriptorTyp PutO_sort( d, sort )
     DescriptorTyp d, sort;
{
  LASSERT(oTab.last >= d);
  return oTab.oper[d].sort = sort;
}

/*-------------------------------------------------------------------------*/

/* PutO_infix
 * Put true if the operation, whose descriptor is d, is infix.
 */
void PutO_infix( d, infix )
     DescriptorTyp d;
     boolean       infix;
{
  LASSERT(oTab.last >= d);
  oTab.oper[d].infix = infix;
}

/*----------------------------------------------------------------*/

/* PutO_ofsort
 * Put in the "of sort" field of the operation d,
 * the value ofsort.
 */
void PutO_ofsort( d, ofsort )
     DescriptorTyp d;
     boolean       ofsort;
{
  LASSERT(oTab.last >= d);
  oTab.oper[d].ofsort = ofsort;
}

/*-------------------------------------------------------------------------*/

/* PutO_ofsortopl
 * Put the list of operations ofsortopl as the list of operations
 * in ofsort conflict with operation d
 */
void PutO_ofsortopl( d, ofsortopl )
     DescriptorTyp  d;
     ListTyp        ofsortopl;
{
  LASSERT(oTab.last >= d);
  oTab.oper[d].ofsortopl=ofsortopl;
}

/*-------------------------------------------------------------------------*/

/* PutO_pmt
 * Put the pattern match tree of the operation whose descriptor is d.
 */
void PutO_pmt( d, pmt )
     DescriptorTyp  d;
     PMatchTreeTyp  pmt;
{
  LASSERT(oTab.last >= d);
  oTab.oper[d].pmt = pmt;
}

/*--------------------------------------------------------------------------*/

/* FindO
 * Return the position of the operation name of a given sort in the table.
 * 0 if it is not found.
 */
DescriptorTyp FindO( name, sort )
     char          *name;
     DescriptorTyp  sort;
{
  DescriptorTyp i;

  for (i=1 ; i<=oTab.last ; i++ )
    if ( (strcmp(oTab.oper[i].name,name)==0) && (oTab.oper[i].sort==sort) )
      break;
  if ( i>oTab.last )
    return 0;
  else
    return i;
}

/*----------------------------------------------------------------*/

/* PrintO
 * Print the name of the operation d.
 * pstr is the function used to print strings.
 */
void PrintO( d, pstr )
     DescriptorTyp  d;
     void         (*pstr)();
{
  LASSERT(oTab.last>=d);
  pstr(oTab.oper[d].name);
}

/*----------------------------------------------------------------*/

/* LastTableO
 * Return the size of the operation table, where the last element is stored.
 */
DescriptorTyp LastTableO()
{
  return oTab.last;
}

/*----------------------------------------------------------------*/

/* sizeO
 * Return the size of the operation table.
 */
static int sizeO()
{
  return oTab.size;
}

/*----------------------------------------------------------------*/

/* PrintTableO
 * Print the table of operations from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableO( l, h, pstr )
     DescriptorTyp   l,h;
     void          (*pstr)();
{
  RewRuleListTyp rl;
  DescriptorTyp  i;
  ListTyp        al;
  char           buff[15];

  pstr("\nTABLE OF OPERATIONS:\n\n");
  SetPrintParamE(PRINT_ONLY_PARAM);
  for (i=l ; (i<=h) && (i<=oTab.last) ; i++) {
    (void)sprintf(buff,"%-2d",i);
    pstr(buff);
    pstr(" = ");
    if (oTab.oper[i].infix)
      pstr("_");
    pstr(oTab.oper[i].name);
    if (oTab.oper[i].infix)
      pstr("_");
    pstr(" : ");
    al=oTab.oper[i].argl;
    if (al!=NULL) {
      while (Next_list(al)!=NULL){
	pstr(sTab.sort[(DescriptorTyp)al->info].name);
	pstr(" (");
	PrintInt(pstr,(int)al->info);
	pstr("), ");
	al=Next_list(al);
      }
      pstr(sTab.sort[(DescriptorTyp)al->info].name);
      pstr(" (");
      PrintInt(pstr,(int)al->info);
      pstr(") ");
    }
    pstr("-> ");
    pstr(sTab.sort[oTab.oper[i].sort].name);
    pstr(" (");
    PrintInt(pstr,oTab.oper[i].sort);
    pstr(")",oTab.oper[i].sort);
    if (oTab.oper[i].ofsort)
      pstr("  of sort");
    pstr("\n");
    rl = oTab.oper[i].rwlist;
    if (rl != NULL) {
      for ( ; rl!=NULL; rl = Next_list(rl) ) {
	Print_rw( (RuleCellPt)LookInfo_list(rl), pstr );
	pstr("\n");
      }
    }
  }
  SetPrintParamE(PRINT_PARAM);
}


/******************************************************************
 *                                                                *
 *                  Rewrite Rules functions                       *
 *                                                                *
 ******************************************************************/

/* GetO_rwl
 * Return the list of rewrite rules of an operation with descriptor d.
 */
RewRuleListTyp GetO_rwl(d)
     DescriptorTyp d;
{
  LASSERT(oTab.last>=d);
  return(oTab.oper[d].rwlist);
}

/*----------------------------------------------------------------*/

static int rule_count = 0;

static int new_rule_count      = 0;
static int released_rule_count = 0;

/* Init_Rules
 *  Init rule cell statistics
 */
static void Init_Rules()
{
#ifdef SDEBUG
  new_rule_count      = 0;
  released_rule_count = 0;
#endif
}

/*----------------------------------------------------------------*/

/* StatRule
 * Rule cells statistics
 */
void StatRule( used, released )
     int *used, *released;
{
  *used     = new_rule_count;
  *released = released_rule_count;
}

/*----------------------------------------------------------------*/

/* New_rw
 * Returns a new cell for a rewrite rule.
 */
static RuleCellPt New_rw()
{
  RuleCellPt   aux;

  aux             = (RuleCellPt) NewCellM(sizeof(RuleCellTyp));
  aux->id         = rule_count++;
  aux->rewritten  = -1;
  aux->subst_pat  = NULL;
  aux->search_pat = NULL;
  aux->premises   = Create_list();
#ifdef SDEBUG
  new_rule_count++;
#endif
  return(aux);
}

/*----------------------------------------------------------------*/

/* Dispose_rw
 * Kill a rewrite rule cell.
 */
static void Dispose_rw( CellPt )
     RuleCellPt CellPt;
{
  LASSERT(CellPt != NULL);
  FreeCellM( (void*)CellPt, sizeof(RuleCellTyp) );
#ifdef SDEBUG
  released_rule_count++;
#endif
}

/*----------------------------------------------------------------*/

static void FEUPVaux(e)
     ExprTyp e;
{
  FreeUntilVarE( UnshareE(e) );
}

/* Free_rw
 * Free a rewrite rule cell.
 */
static void Free_rw( CellPt )
     RuleCellPt CellPt;
{
  LASSERT(CellPt != NULL);
  FEUPVaux( CellPt->subst_pat );
  FEUPVaux( CellPt->search_pat );
  Free_list( CellPt->premises, FEUPVaux );
  Dispose_rw(CellPt);
}

/*--------------------------------------------------------------------------*/

/* PutO_rw
 * Insert a rewrite rule into the table of operations.
 * pb is the search pattern, ps is the sustitution pattern and
 * l is the presmise list.
 * The list of rewritten rules is ordered in the following way:
 * rules with premises are at the beginning of the list;
 * and rules without premises are placed at the end of the list.
 */
void PutO_rw( pb, ps, l )
     ExprTyp pb, ps;
     ListTyp l;
{
  RuleCellPt    aux;
  DescriptorTyp d;

  LASSERT(pb != NULL);
  LASSERT(ps != NULL);
  aux             = New_rw();
  aux->search_pat = ShareE(pb);
  aux->subst_pat  = ShareE(ps);
  aux->premises   = l;
  d               = LookNameE(pb);
  if (l!=NULL)
    oTab.oper[d].rwlist = Insert_list((DataListTyp)aux,oTab.oper[d].rwlist);
  else
    oTab.oper[d].rwlist = Add_list((DataListTyp)aux,oTab.oper[d].rwlist);
}

/*----------------------------------------------------------------*/

static boolean IsVoidPremise( e )
     ExprTyp e;
{
  DescriptorTyp n1,n2;
  ExprTyp       e1,e2;

  LASSERT(IsEqual(e));

  e1 = LookArgE(e,1);
  e2 = LookArgE(e,2);
  if ( IsVariableE(e1) && IsVariableE(e2) ){
    n1 = LookPVarE(e1)==NULL? LookNameE(e1) : LookNameE(LookPVarE(e1));
    n2 = LookPVarE(e2)==NULL? LookNameE(e2) : LookNameE(LookPVarE(e2));
#ifdef SDEBUG
    if ( LookPVarE(e1) )
      LASSERT(IsVariableE(LookPVarE(e1)));
    if ( LookPVarE(e2) )
      LASSERT(IsVariableE(LookPVarE(e2)));
#endif
    return n1==n2;
  }
  return FALSE;
}

/*----------------------------------------------------------------*/

/* SPrint_rw
 * Make a string with a rewrite rule.
 */
char * SPrint_rw( RulePt )
     RuleCellPt     RulePt ;
{
  ListTyp   l;
  char    * str;
  StrBckTyp strBck;
  ExprTyp   e;
  boolean   premisses;

  LASSERT(RulePt->search_pat != NULL);
  LASSERT(RulePt->subst_pat != NULL);

  strBck    = CreateStrBck();
  strBck    = ConcatStrBck( strBck, "   " );
  premisses = FALSE;
  if ( (l=RulePt->premises) != NULL) {
    while ( l != NULL) {
      e = (ExprTyp)LookInfo_list(l);
      if ( !IsVoidPremise(e) ){ /* Void premises must be
				   always at the beginning */
	premisses = TRUE;
	str       = ExprToStringE(e);
	strBck    = ConcatStrBck( strBck, str );
	free(str);
	l = Next_list(l);
	if (l!=NULL)
	  strBck = ConcatStrBck( strBck, " , " );
      }
      else
	l = Next_list(l);
    }
    if (premisses)
      strBck = ConcatStrBck( strBck, " => " );
  }
  str    = ExprToStringE(RulePt->search_pat);
  strBck = ConcatStrBck( strBck, str );
  free(str);
  strBck = ConcatStrBck( strBck, " = " );
  str    = ExprToStringE(RulePt->subst_pat);
  strBck = ConcatStrBck( strBck, str );
  free(str);
  strBck = ConcatStrBck( strBck, " ;" );
  str    = GetStrStrBck( strBck );
  FreeStrBck( strBck );

  return str;
}

/*----------------------------------------------------------------*/

/* Print_rw
 * Print the rewrite rule rr.
 * pstr is the function used to print strings.
 */
void Print_rw( rr, pstr )
     RuleCellPt     rr ;
     void           (*pstr)();
{
  char * str;

  str = SPrint_rw( rr );
  pstr(str);
  (void)free(str);
}



/******************************************************************
 *                                                                *
 *                       Table of processes                       *
 *                                                                *
 ******************************************************************/

/* Exit_Functionality
 * return the functionality of an Exit Cell
 */
static int Exit_Functionality( b )
     BehTyp b;
{
  OfferListTyp ol;
  SortListTyp sl;

  ol = (OfferListTyp)LookAInfo( LookA( b, OLA) );
  if ( ol==NULL )
    return EXITF;

  sl = Create_list();
  while ( ol != NULL ) {
    sl = Add_list( (DataListTyp)LookSortE(LookExprOffer(ol)), sl ) ;
    ol  = MvNextOffer( ol );
  }
  return Store_func(sl);
}

/*----------------------------------------------------------------*/

static ListTyp procList;

typedef struct { DescriptorTyp processName;
		 ListTyp       instList;
		 int           func;
	       } FuncDescTyp, *PFuncDescTyp;

/*----------------------------------------------------------------*/

/* Functionality
 * Calculate the functionalities of a behaviour except the noexit ones
 *
 *  -2 = notcalculated
 *   0 = exit
 *   n = exit ( s1, ..., sm ) ( the position in the table of functionalities )
 *
 *   The functionalities of the processes instantiated are ignored.
 *   A list of instantiations upon which the functionality depends is made
 *   if the result is NOTCALCULATEDF.
 */
static int Functionality( b )
     BehTyp b;
{
  int           i, numArg, func;
  boolean       cont;
  ListTyp       cl;
  DescriptorTyp procName;

  func = NOTCALCULATEDF;
  cont = TRUE;
  while (cont)
    {
      switch( LookTypeB(b) )
	{
	case RelabellingC:
	case HidingC:
	case ChoiceC:
	case PletC:
	case LetC:
	case GuardC:
	case GateC:
	case IC:
	case GateChoiceC:
	case ParC:
	case ProcessDefC:
	case SpecificationC:
	  b = LookArgB( b, 1 );
	  break;

	case EnablingC:
	  b = LookArgB( b, 2 );
	  break;

	case DisablingC:
	  func = Functionality( LookArgB( b, 1 ) );   /* f(exit[>B)= exit */
	  if (func<EXITF)
	    func = Functionality( LookArgB( b, 2 ) ); /* f(stop[>exit)= exit */
	  cont=FALSE;
	  break;

	case ParallelC:
	  func = Functionality( LookArgB( b, 1 ) );
	  if (func>=EXITF)
	    func = Functionality( LookArgB( b, 2 ) );/*f(exit || stop)=noexit*/
	  cont=FALSE;
	  break;

	case AlternativeC:
	  numArg = NumArgB( b );
	  for ( i=1; (i<=numArg) && (func<EXITF); i++ )
	    func = Functionality( LookArgB( b, i ) );
	  cont=FALSE;
	  break;

	case ExitC:
	  func= Exit_Functionality( b );
	  cont=FALSE;
	  break;

	case TerminationC:
	case StopC:
	  cont=FALSE;
	  break;

	case ProcessInstC:
	  procName=LookNameB(b);
	  if (!In_list((DataListTyp)procName,procList,EqInt))
	    procList=Insert_list((DataListTyp)procName,procList);
	  cont=FALSE;
	  break;

	case InterleavedC:
	  b = LookArgB( b, 2 );
	  break;

	case ContSetC:
	  for ( cl=(ITContListTyp)LookAInfo(LookA(b,ITCLA));
	       (cl!=NULL) && (func<EXITF); cl=Next_list(cl) )
	    func = Functionality( ((PITContTyp)LookInfo_list(cl))->b );
	  cont=FALSE;
	  break;

	default:
	  Error("Functionality: unexpected cell type\n");
	}
    }
  return func;
}

/*--------------------------------------------------------------------------*/

static PFuncDescTyp pfdtaux;

/* MaxFunctionality
 *  if there exists a process in the process list "pl" whose functionality
 *     is >=EXITF then returns it
 *  else
 *   if there exists any NOTCALCULATEDF return NOTCALCULATEDF
 *  else
 *   returns NOEXITF
 */
static int MaxFunctionality( pl, from )
     ListTyp pl;
     /* KJT 22/01/23: added declaration */
     int from;
{
  int     func,n;
  boolean dirty = FALSE;

  for ( ;pl!=NULL;pl=Next_list(pl)) {
    n = (int)LookInfo_list(pl);
    if ( n<from )
      func = GetP_func(n);
    else
      func = pfdtaux[n-from].func;
    if (func>=EXITF)
      return func;
    dirty =  func == NOTCALCULATEDF;
  }
  if (dirty)
    return NOTCALCULATEDF;
  return NOEXITF;
}

/*----------------------------------------------------------------*/

/* DupProcTab_Func
 * Calculate the functionalities of the processes, from position n to the end
 * of the table, whose current functionality is in the NOTCALCULATEDF state.
 * These processes are new, and were created by means of some kind of
 * expansion.
 * When n=0 it is assumed that the calculation starts at the first process
 * definition with NOTCALCULATEDF functionality detected.
 */
void DupProcTab_Func( n )
     int n;
{
  int     i,func,lastProc;
  boolean changes;

  lastProc = LastTableP();
  if ( n<1 )
    for ( i=1 ; i<=lastProc; i++ )
      if ( GetP_func(i) == NOTCALCULATEDF ) {
	n = i;
	break;
      }
  if (n<1)
    return;

  pfdtaux = (PFuncDescTyp)emalloc( (lastProc-n+1)*sizeof(FuncDescTyp) );

  for ( i=n ; i<=lastProc; i++ )
    if ( GetP_func(i) == NOTCALCULATEDF ) {
      procList=Create_list();
      func = Functionality( GetP_def(i) );
      if (func==NOTCALCULATEDF && procList==NULL)
	func = NOEXITF;
      pfdtaux[i-n].func = func;
      pfdtaux[i-n].instList = procList;
    }

  changes = TRUE;
  while (changes) {
    changes = FALSE;
    for ( i=n ; i<=lastProc; i++ )
      if ( pfdtaux[i-n].func == NOTCALCULATEDF ) {
	func = MaxFunctionality( pfdtaux[i-n].instList, n );
	if ( func > NOTCALCULATEDF ) {
	  pfdtaux[i-n].func=func;
	  changes = TRUE;
	}
      }
  }

  for ( i=n; i<=lastProc; i++ )
    if ( pfdtaux[i-n].func == NOTCALCULATEDF )
      PutP_func( i, NOEXITF );
    else
      PutP_func( i, pfdtaux[i-n].func );

  /* if you ever want the specification funtionality to be recalculated
   * after the n-th process

   if ( GetP_func(1) >= EXITF ) {
   procList=Create_list();
   func = Functionality( GetP_def(1) );
   if (func==NOTCALCULATEDF) {
   func = MaxFunctionality( procList, n );
   PutP_func(1,func);
   }
   Disp_list(procList);
   }
   */

  for (i=n; i<=lastProc; i++)
    Disp_list(pfdtaux[i-n].instList);

  free((char*)pfdtaux);
}

/******************************************************************
 *                                                                *
 *                   Table of functionalities                     *
 *                                                                *
 ******************************************************************/

#define INC_FUNC_TABLE 128

typedef struct { FtableEntryTyp *func;
		 DescriptorTyp   last;
		 int             size;
	       } FuncTableTyp;

static FuncTableTyp fTab;

/*----------------------------------------------------------------*/

/* CleanFuncTable
 * Clean up the functionalities table, and reset it to empty.
 */
static void CleanFuncTable()
{
  int i;

  for (i=1 ; i<=fTab.last ; i++)
    Disp_list(fTab.func[i]);
  fTab.last = 0;
}

/*--------------------------------------------------------------------------*/

/* ReallocFTab
 * Allocate more memory for the functionality table.
 */
static void ReallocFTab()
{
  fTab.func = (FtableEntryTyp*)erealloc((void*)fTab.func,
					(fTab.size + INC_FUNC_TABLE)
					*sizeof(FtableEntryTyp));
  if (fTab.func ==NULL)
    Error("Tables -> run out of memory for functionality table.");
  fTab.size +=  INC_FUNC_TABLE;
}

/*----------------------------------------------------------------*/

/* CreateFTab
 * Allocate memory for the functionality table.
 * Reset the table.
 */
static void CreateFTab()
{
  fTab.func  = (FtableEntryTyp*)emalloc(INC_FUNC_TABLE*sizeof(FtableEntryTyp));
  fTab.size  = INC_FUNC_TABLE;
  fTab.last  = 0;
  fTab.func[0] = NULL;
}

/*----------------------------------------------------------------*/

/* Declare_func
 * Insert a new functionality in fTab
 * This function returns the position of the new entry in the table.
 */
static int Declare_func( sl )
     SortListTyp sl;
{
  if ( fTab.last+1 == fTab.size )
    ReallocFTab();
  fTab.last++;
  fTab.func[fTab.last] = sl;

  return fTab.last;
}

/*----------------------------------------------------------------*/

/* FindF
 * Return the position of the functionality sl in the table.
 * 0 if it is not found.
 */
static int FindF( sl )
     SortListTyp sl;
{
  int i;

  for (i=1 ; i<=fTab.last ; i++ )
    if ( Equal_list(fTab.func[i], sl, EqInt) )
      break;
  if ( i>fTab.last )
    return 0;
  else
    return i;
}

/*----------------------------------------------------------------*/

/* Store_func
 * Store the functionality defined by the sort list "sl" into the internal
 * functionality table.
 * Return an index to the table.
 */
int Store_func( sl )
     SortListTyp sl;
{
  int df;

  df = FindF(sl);
  if ( df>0 )
    { /* It is only stored in the table if it does not exist already */
      Disp_list( sl );
      return df;
    }
  else
    return Declare_func(sl) ;
}

/*----------------------------------------------------------------*/

/* GetF_sl
 * Return the sort list associated to the functionality d
 */
SortListTyp GetF_sl( d )
     int  d;
{
  LASSERT(fTab.last >= d);
  return fTab.func[d];
}

/*----------------------------------------------------------------*/

/* LastTableF
 * Return the size of the functly table, where the last element is stored.
 */
static int LastTableF()
{
  return fTab.last;
}

/*----------------------------------------------------------------*/

/* sizeF
 *  Return the size of the functly table.
 */
static int sizeF()
{
  return fTab.size;
}

/*----------------------------------------------------------------*/

/* SPrintF
 * Print a functionality sort-list into a new string.
 */
static char * SPrintF( d )
     int    d;
{
  SortListTyp sl, next;
  char      * str;
  StrBckTyp   strBck;

  LASSERT(fTab.last>=d);

  strBck = CreateStrBck();
  sl     = (SortListTyp)fTab.func[d];
  while ( sl!=NULL ) {
    str    = SPrintS( (DescriptorTyp)LookInfo_list(sl) );
    strBck = ConcatStrBck( strBck, str );
    free(str);
    next   = Next_list(sl);
    if ( next != NULL )
      strBck = ConcatStrBck( strBck, ", ");
    sl = next;
  }
  str = GetStrStrBck( strBck );
  FreeStrBck( strBck );
  return str;
}

/*----------------------------------------------------------------*/

/* PrintF
 * Print the functionality sort-list.
 * pstr is the function used to print strings.
 */
static void PrintF( d, pstr )
     int   d;
     void (*pstr)();
{
  char *l;

  l = SPrintF(d);
  pstr(l);
  (void)free(l);
}

/*----------------------------------------------------------------*/

/* PrintTableF
 * Print the table of functionalities from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableF( l, h, pstr )
     DescriptorTyp   l,h;
     void          (*pstr)();
{
  DescriptorTyp i;
  char          buff[15];

  pstr("\n FUNCTIONALITIES:\n");
  for (i=l ; (i<=h) && (i<=fTab.last) ; i++) {
    (void)sprintf(buff,"%-2d",i);
    pstr(buff);
    pstr(" = ");
    PrintF( i, pstr );
  }
}

/*----------------------------------------------------------------*/

/* SPrint_Func
 * Make a string with the functionality func.
 */
char * SPrint_Func( func )
     int func;
{
  char    * str;
  StrBckTyp strBck;

  strBck = CreateStrBck();
  LASSERT ( func > -3 );
  switch( func )
    {
    case NOTCALCULATEDF :
      strBck = ConcatStrBck( strBck, "functionality" );
      break;

    case NOEXITF :
      strBck = ConcatStrBck( strBck, "noexit" );
      break;

    case EXITF :
      strBck = ConcatStrBck( strBck, "exit" );
      break;

    default :
      strBck = ConcatStrBck( strBck, "exit ( " );
      str    = SPrintF( func );
      strBck = ConcatStrBck( strBck, str );
      free(str);
      strBck = ConcatStrBck( strBck, " )" );
      break;
    }
  str = GetStrStrBck( strBck );
  FreeStrBck( strBck );
  return str;
}

/*----------------------------------------------------------------*/

/* Print_Func
 * Print the functionality func.
 * pstr is the function used to print strings.
 */
void Print_Func( func, pstr )
     int  func;
     void (*pstr)();
{
  char * str;

  str = SPrint_Func( func );
  pstr(str);
  (void)free(str);
}

/*----------------------------------------------------------------*/

/* CleanProcTable
 * Clean the process table, and reset it to empty.
 */
static void CleanProcTable()
{
  int i ;

  for (i=1 ; i<=pTab.last ; i++) {
    DecCopyC(pTab.proc[i].def);
    FreeB(pTab.proc[i].def);
  }
  pTab.last = 0;
}

/*----------------------------------------------------------------*/

/* CreatePTab
 * Allocate memory for the process table.
 * Reset the table.
 */
static void CreatePTab()
{
  pTab.proc = (PtableEntryTyp*)emalloc(INC_PROC_TABLE*sizeof(PtableEntryTyp));
  pTab.size = INC_PROC_TABLE;
  pTab.last = 0;
}

/*----------------------------------------------------------------*/

/* ReallocPTab
 * Allocate more memory for the process table.
 */
static void ReallocPTab()
{
  pTab.proc = (PtableEntryTyp*)erealloc((void*)pTab.proc,
					(pTab.size + INC_PROC_TABLE)
					*sizeof(PtableEntryTyp));
  if (pTab.proc ==NULL)
    Error("Tables -> run out of memory for process table.");
  pTab.size +=  INC_PROC_TABLE;
}

/*--------------------------------------------------------------------------*/

/* Declare_proc
 * Insert a new process definition in pTab.
 * Return the position of the new entry in the table.
 */
DescriptorTyp Declare_proc( name,def,funclity )
     char   *name;
     BehTyp  def;
     int     funclity;
{
  DescriptorTyp i;
  char         *nname;

  if (pTab.last+1 == pTab.size)
    ReallocPTab();
  if (FindP(name)!=0) {
    i=1;
    nname = (char*)emalloc(strlen(name)+8);
    do {
      (void)sprintf(nname,"%s_%d",name,i++);
      LASSERT(strlen(nname)<strlen(name)+8);
    } while (FindP(nname)!=0);
  }
  else
    nname = name;
  pTab.last++;
  pTab.proc[pTab.last].name = nname;
  pTab.proc[pTab.last].def  = def;
  if (def!=NULL)
    IncCopyC(def);
  pTab.proc[pTab.last].funclity = funclity;
  return pTab.last;
}

/*----------------------------------------------------------------*/

/* GetP_name
 * Return the name of the process whose descriptor is d.
 */
char* GetP_name( d )
     DescriptorTyp d;
{
  LASSERT(pTab.last >= d);
  return pTab.proc[d].name;
}

/*----------------------------------------------------------------*/

/* GetP_def
 * Return the pointer to the process definition for the process d
 */
BehTyp GetP_def( d )
     DescriptorTyp d;
{
  LASSERT(pTab.last >= d);
  return pTab.proc[d].def;
}

/*----------------------------------------------------------------*/

/* GetP_func
 * Return the funcionality of the process whose desriptor is d.
 */
int GetP_func( d )
     DescriptorTyp d;
{
  LASSERT(pTab.last >= d);
  return pTab.proc[d].funclity;
}

/*----------------------------------------------------------------*/

/* PutP_def
 * Insert the pointer to the process definition for the process d
 */
void PutP_def( d, def )
     DescriptorTyp d;
     BehTyp        def;
{
  LASSERT(pTab.last >= d);
  if (def!=NULL)
    IncCopyC(def);
  pTab.proc[d].def = def;
}

/*----------------------------------------------------------------*/

/* PutP_func
 * Insert the funcionality of the process d
 */
void PutP_func( d, funclity )
     DescriptorTyp d;
     int           funclity;
{
  LASSERT(pTab.last >= d);
  pTab.proc[d].funclity = funclity;
}

/*----------------------------------------------------------------*/

/* FindP
 * Return the position of the process name in the table
 * 0 if it is not found.
 */
DescriptorTyp FindP( name )
     char* name;
{
  DescriptorTyp i;

  for (i=1 ; i<=pTab.last ; i++ )
    if  (strcmp(pTab.proc[i].name,name)==0)
      break;
  if ( i>pTab.last )
    return 0;
  else
    return i;
}

/*----------------------------------------------------------------*/

/* PrintP
 * Print the name of the process d.
 * pstr is the function used to print strings.
 */
void PrintP( d, pstr )
     DescriptorTyp d;
     void        (*pstr)();
{
  LASSERT(pTab.last>=d);
  pstr(pTab.proc[d].name);
}


/*----------------------------------------------------------------*/

/* LastTableP
 * Return the size of the process table, where the last element is stored.
 */
DescriptorTyp LastTableP()
{
  return pTab.last;
}

/*----------------------------------------------------------------*/

/* sizeP
 * Return the size of the process table.
 */
static int sizeP()
{
  return pTab.size;
}

/*----------------------------------------------------------------*/

/* PrintTableP
 * Print the table of processes from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableP( l, h, pstr )
     DescriptorTyp l,h;
     void (*pstr)();
{
  DescriptorTyp i;
  char          buff[15];

  pstr("\nTABLE OF PROCESSES:\n\n");
  for (i=l ; (i<=h) && (i<=pTab.last) ; i++) {
    (void)sprintf(buff,"%-2d",i); pstr(buff);
    pstr(" = ");
    pstr(pTab.proc[i].name);
#ifdef SDEBUG
    pstr(" (");
    PrintInt(pstr,pTab.proc[i].funclity);
    pstr(" ");
    Print_Func(pTab.proc[i].funclity,pstr);
    pstr(") = ");
    PrintInt(pstr,(int)pTab.proc[i].def);
#else
    pstr(" [");
    PrintGL((GateListTyp)LookAInfo(LookA(pTab.proc[i].def,GLA)),pstr);
    pstr("] ");
    if (LookA(pTab.proc[i].def,ELA)!=NULL) {
      pstr("(");
      PrintVL((ExprListTyp)LookAInfo(LookA(pTab.proc[i].def,ELA)),pstr);
      pstr(") ");
    }
    pstr(": ");
    Print_Func(pTab.proc[i].funclity,pstr);
#endif
    pstr("\n");
  }
}


/******************************************************************
 *                                                                *
 *                      Table of Sorts                            *
 *                                                                *
 ******************************************************************/

/* CreateSTab
 * Allocate memory for the table of sorts.
 * Reset the table.
 */
static void CreateSTab()
{
  sTab.sort = (StableEntryTyp*)emalloc(INC_SORT_TABLE*sizeof(StableEntryTyp));
  sTab.size = INC_SORT_TABLE;
  sTab.last = 0;
}

/*----------------------------------------------------------------*/

/* ReallocSTab
 * Allocate more memory for the table of sorts.
 */
static void ReallocSTab()
{
  sTab.sort = (StableEntryTyp*)erealloc((void*)sTab.sort,
					(sTab.size + INC_SORT_TABLE)
					*sizeof(StableEntryTyp));
  if (sTab.sort ==NULL)
    Error("Tables -> run out of memory for sort table.");
  sTab.size +=  INC_SORT_TABLE;
}

/*----------------------------------------------------------------*/

/* Declare_sort
 * Insert a new sort in sTab
 * This function returns the position of the new entry in the table.
 */
DescriptorTyp Declare_sort( name )
     char *name;
{
  DescriptorTyp  i;
  char          *nname;

  if (sTab.last+1 == sTab.size)
    ReallocSTab();
  if (FindS(name)!=0) {
    i=1;
    nname = (char*)emalloc(strlen(name)+8);
    do {
      (void)sprintf(nname,"%s_%d",name,i++);
      LASSERT(strlen(nname)<strlen(name)+8);
    } while (FindS(nname)!=0);
  }
  else
    nname = name;
  sTab.last++;
  sTab.sort[sTab.last].name = nname;
  return sTab.last;
}

/*--------------------------------------------------------------------------*/

/* GetS_name
 * Return the name of the sort d
 */
char* GetS_name( d )
     DescriptorTyp d;
{
  LASSERT(sTab.last >= d);
  return sTab.sort[d].name;
}

/*----------------------------------------------------------------*/

/* FindS
 * Return the position of the sort name in the table
 * 0 if it is not found.
 */
DescriptorTyp FindS( name )
     char *name;
{
  DescriptorTyp i;

  for (i=1 ; i<=sTab.last ; i++ )
    if  (strcmp(sTab.sort[i].name,name)==0)
      break;
  if ( i>sTab.last )
    return 0;
  else
    return i;
}

/*----------------------------------------------------------------*/

/* PrintS
 * Print the name of the sort d.
 * pstr is the function used to print strings.
 */
void PrintS( d, pstr )
     DescriptorTyp   d;
     void          (*pstr)();
{
  LASSERT(sTab.last>=d);
  pstr(sTab.sort[d].name);
}

/*----------------------------------------------------------------*/

/* SPrintS
 * Return a string with a sort name.
 */
char * SPrintS( d )
     DescriptorTyp   d;
{
  LASSERT(sTab.last>=d);
  return CopyString(sTab.sort[d].name);
}

/*----------------------------------------------------------------*/

/* LastTableS
 * Return the size of the sort table, where the last elements is stored.
 */
DescriptorTyp LastTableS()
{
  return sTab.last;
}

/*----------------------------------------------------------------*/

/* sizeS
 * Return the size of the sort table.
 */
static int sizeS()
{
  return sTab.size;
}

/*----------------------------------------------------------------*/

/* PrintTableS
 * Print the table of sorts from the position l to h.
 * pstr is the function used to print strings.
 */
static void PrintTableS( l, h, pstr )
     DescriptorTyp   l, h;
     void          (*pstr)();
{
  DescriptorTyp i;
  char          buff[15];

  pstr("\nTABLE OF SORTS:\n\n");
  for (i=l ; (i<=h) && (i<=sTab.last) ; i++) {
    (void)sprintf(buff,"%-2d",i); pstr(buff);
    pstr(" = ");
    pstr(sTab.sort[i].name);
    pstr("\n");
  }
}


/******************************************************************
 *                                                                *
 *               Initialization and Statistics                    *
 *                                                                *
 ******************************************************************/

/*
 *  never_initialitated is TRUE if the tables have never been initialitated.
 */
static boolean never_initialitated = TRUE;

/*----------------------------------------------------------------*/

/* Init_Tables
 * Tables initialitation.
 * This function must be called when the application starts
 * or when a specification is loaded for a hot re-initialization.
 */
void Init_Tables()
{
  if (never_initialitated) {
    CreateVTab();
    CreatePTab();
    CreateSTab();
    CreateOTab();
    CreateFTab();
  }
  else {
    CleanOperTable();
    CleanProcTable();
    CleanFuncTable();
    CleanGateTable();
    CleanVarTable();
    sTab.last = 0;
  }
  Init_Rules();
  never_initialitated = FALSE;
}

/*----------------------------------------------------------------*/

/* Reset_Tables
 * Cold table re-initialitation.
 * This function must be called when a specification is re-loaded.
 * All table entries are disregarded ( not freed ) and
 * the tables static memory space is freed.
 */
void Reset_Tables()
{
  if (!never_initialitated)
    {
      free((char*)oTab.oper);
      free((char*)pTab.proc);
      free((char*)fTab.func);
      CleanGateTable();
      CleanVarTable();
      free((char*)sTab.sort);
      never_initialitated = TRUE;
    }
  Init_Tables();
}

/*----------------------------------------------------------------*/

/* StatisticTableO
 * Return the statistic of the table of operations.
 *  pvcv is the virtual number of variable cells used.
 *  pocv is the virtual number of operation cells used.
 *  pvcr is the real number of variable cells used.
 *  pocr is the real number of operation cells used.
 *  pnlev is the virtual number of list nodes used in the expressions.
 *  pnler is the real number of list nodes used in the expressions.
 *  pnlv is the virtual number of list nodes used (not in expr.).
 *  pnlr is the real number of list nodes used (not in expr.).
 *  prc  is the number of rewrite rule nodes used.
 *  pmc  is the number of pmt nodes used.
 */
void StatisticTableO( pvcv,pocv,pvcr,pocr,pnlev,pnler,pnlv,pnlr,prc,pmc )
     int *pvcv,*pocv,*pvcr,*pocr,*pnlev,*pnler,*pnlv,*pnlr,*prc,*pmc;
{
  int            n1,var1,op1;
  int            n2,var2,op2;
  int            i,pmn,n3,aux;
  RewRuleListTyp rl;
  RuleCellPt     cr;

  *pvcv=*pocv=*pvcr=*pocr=*pnlev=*pnler=*pnlv=*pnlr=*prc=*pmc=0;
  for ( i=0 ; i<=LastTableO() ; i++ ) {
    aux = Length_list(oTab.oper[i].argl) + Length_list(oTab.oper[i].ofsortopl);
    *pnlr += aux;
    *pnlv += aux;
    for ( rl = oTab.oper[i].rwlist; rl != NULL; rl = Next_list(rl) ) {
      (*prc)++;
      (*pnlr)++;
      (*pnlv)++;
      cr = (RuleCellPt) LookInfo_list(rl);
      StatisticE(cr->search_pat,&n1,&var1,&op1,&n2,&var2,&op2);
      *pvcv += var1;
      *pocv += op1;
      *pnlev += n1;
      *pvcr += var2;
      *pocr += op2;
      *pnler += n2;
      StatisticE(cr->subst_pat,&n1,&var1,&op1,&n2,&var2,&op2);
      *pvcv += var1;
      *pocv += op1;
      *pnlev += n1;
      *pvcr += var2;
      *pocr += op2;
      *pnler += n2;
      StatisticEL(cr->premises,&n1,&var1,&op1,&n2,&var2,&op2,&n3);
      *pvcv += var1;
      *pocv += op1;
      *pvcr += var2;
      *pocr += op2;
      *pnlev += n1;
      *pnler += n2;
      *pnlv += n3;
      *pnlr += n3;
    }
    StatisticPMT( oTab.oper[i].pmt,&pmn,&n1);
    *pmc += pmn;
    *pnlr += n1;
    *pnlv += n1;
  }
}

/*----------------------------------------------------------------*/

/* StatisticTableG
 * Statistics of the table of gates.
 * ngs is the number of gate sets used.
 */
void StatisticTableG( ngs )
     int *ngs;
{
  *ngs = gTab.last;
}

/*----------------------------------------------------------------*/

/* StatisticTableF
 * Return statistics of the table of functionalities.
 *  pcc is the number of cells.
 *  pnl is the number of nodes in the lists.
 */
void StatisticTableF( pcc, pnl )
     int *pcc,*pnl;
{
  int i;

  *pcc = 0;
  *pnl = 0;
  for (i=1 ; i<=LastTableF() ; i++) {
    *pnl += Length_list( GetF_sl( i ) );
  }
}

/*----------------------------------------------------------------*/

/* PrintSize_Tables
 * Print the maximum size and the used size of the tables
 */
extern void PrintSize_Tables()
{
  LASSERT(printTarget!=NULL);

  printTarget("   Size of internal identifier tables (busy/size):\n");

  printTarget("     gate(");
  PrintInt(printTarget,LastTableG());
  printTarget("/");
  PrintInt(printTarget,sizeG());
  printTarget(")  ");

  printTarget("var(");
  PrintInt(printTarget,LastTableV());
  printTarget("/");
  PrintInt(printTarget,sizeV());
  printTarget(")  ");

  printTarget("sort(");
  PrintInt(printTarget,LastTableS());
  printTarget("/");
  PrintInt(printTarget,sizeS());
  printTarget(")\n");

  printTarget("     oper(");
  PrintInt(printTarget,LastTableO());
  printTarget("/");
  PrintInt(printTarget,sizeO());
  printTarget(")  ");

  printTarget("proc(");
  PrintInt(printTarget,LastTableP());
  printTarget("/");
  PrintInt(printTarget,sizeP());
  printTarget(")  ");

  printTarget("functy(");
  PrintInt(printTarget,LastTableF());
  printTarget("/");
  PrintInt(printTarget,sizeF());
  printTarget(")\n\n");
}

/*----------------------------------------------------------------*/

/* PrintTable
 * Print the specified table from the position l to h.
 * pstr is the function used to print strings.
 */
void PrintTable( t, l, h, pstr )
     KindTableTyp    t;
     DescriptorTyp   l,h;
     void          (*pstr)();
{
  switch (t)
    { case GateTable:
	PrintTableG(l,h,pstr);
	break;
      case SortTable:
	PrintTableS(l,h,pstr);
	break;
      case VarTable:
	PrintTableV(l,h,pstr);
	break;
      case OperTable:
	PrintTableO(l,h,pstr);
	break;
      case ProcTable:
	PrintTableP(l,h,pstr);
	break;
      }
}

/*----------------------------------------------------------------*/

#ifdef TIME
/* FindO_time
 * Search for the  opn "name" that has arguments of sort time
 */
DescriptorTyp FindO_time ( name )
     char  *name;
{
  DescriptorTyp i;
  DescriptorTyp time;
  ListTyp l;

  time = FindS("time");
  for (i=1 ; i<=oTab.last ; i++ )
    if ( (strcmp(oTab.oper[i].name,name)==0)) {
     l= GetO_argl(i);
     if  ( ((l==NULL) && (oTab.oper[i].sort==time)) ||
	   ( (l != NULL) && ( (DescriptorTyp )l->info == time)))
       break;
   }
  if ( i>oTab.last )
    return 0;
  else
    return i;

}

#endif







