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

/******************************************************************
 *  
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *
 *  8 Jan 1990
 *
 *  Internal Tables
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : activate debugging
 *
 *  TYPE DEFINITIONS:
 *     KindTableTyp            : type of table
 *     GtableEntryTyp          : table of gates
 *     VtableEntryTyp          : table of variables
 *     StableEntryTyp          : table of sorts
 *     PtableEntryTyp          : table of processes
 *     OtableEntryTyp          : table of operations
 *     RewRuleListTyp          : list of rewrite rules
 *     RuleCellTyp, RuleCellPt : rewrite rule
 *     SortListTyp             :  list of sorts
 *     FtableEntryTyp          : table of functionalities 
 *
 *  FUNCTION DEFINITIONS:
 *     Init_Tables          : init tables
 *     Reset_Tables         : cold re-initialitation of all the tables
 *     PrintTable           : print a table into a file
 *     StatisticTableO      : statistics of the table of operations
 *     StatisticTableF      : statistics of the table of functionalities
 *     StatisticTableG      : statistics of the table of gates
 *     StatRule             : statistics of rule cells use
 *     PrintSize_Tables     : print maximum and used size of tables
 *     Store_gate           : insert a gate in gTab
 *     Declare_gate         : insert a new gate in gTab
 *     GetG_name            : get the name of a gate
 *     GetG_mask            : get the mask of a gate
 *     PutG_mask            : put the mask to a gate
 *     FindG_byMask         : get the gate determined by mask
 *     FindG                : get the position of a gate in the table
 *     PrintG               : print a gate into a file
 *     SPrintG              : make a string with a gate name
 *     LastTableG           : get the last position occupied
 *     Declare_var          : insert a new variable in vTab
 *     GetV_name            : get the name of a variable
 *     GetV_sort            : get the sort of a variable
 *     PutV_sort            : put the sort to a variable
 *     EqualV_entry         : create an entry equal to a given variable
 *     FindV                : get the position of a variable
 *     PrintV               : print a variable into a file
 *     SPrintV              : make a string with a variable name and sort
 *     LastTableV           : get the last position occupied  
 *     ReleaseRangeTableV   : release a range of variable entries
 *     Declare_opn          : insert a new operation in oTab
 *     GetO_name            : get the name of an operation
 *     GetO_sort            : get the sort of an operation
 *     GetO_infix           : say if an operation is infix
 *     GetO_tableOfsort     : look if there are "of sort" type operations
 *                            in the table
 *     GetO_ofsort          : look if the operation is "of sort" type
 *     GetO_ofsortopl       : get the ofsort operation list of the operation
 *     GetO_pmt             : get the pattern match tree of an operation
 *     PutO_sort            : put the sort to the operation
 *     GetO_argl            : get the list of arguments of an operation
 *     PutO_argl            : put the list of arguments to an operation
 *     PutO_infix           : indicate if the operation is infix
 *     PutO_ofsort          : indicate if the operation is "of sort" type
 *     PutO_ofsortopl       : put the ofsort operation list to the operation
 *     PutO_pmt             : put the pattern match tree to an operation
 *     FindO                : get the position of an operation
 *     PrintO               : print an operation in a file
 *     GetO_rwl             : get the list of rewrite rules of an operation
 *     PutO_rw              : add a rewrite rule to an operation in the oTab
 *     SPrint_rw            : make a string with a rewrite rule
 *     Print_rw             : print a rewrite rule
 *     LastTableO           : get the last position occupied  
 *     Declare_proc         : insert a new process in pTab
 *     Store_func           : store a functionality in the table of funcs
 *     GetF_sl              : get the list of sorts of a functionality
 *     GetP_name            : get the name of a process
 *     GetP_def             : get a pointer to the definition of a process
 *     GetP_func            : get the functionality of a process
 *     PutP_def             : insert a pointer to the definition of a process
 *     PutP_func            : insert the functionality of a process
 *     FindP                : get the position of a process
 *     PrintP               : print a process in a file
 *     LastTableP           : get the last position occupied
 *     DupProcTab_Func      : calculate functionalities of duplicate processes
 *     SPrint_Func          : make a string with a functionality
 *     Print_Func           : print functionality into a file
 *     Declare_sort         : insert a new sort in sTab 
 *     GetS_name            : get the name of a sort
 *     FindS                : get the position of a sort
 *     PrintS               : print a sort in a file
 *     SPrintS              : make a string with a sort name
 *  
 *  LOG:
 *     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.
 *
 ******************************************************************/

#ifndef batables_H
#define batables_H

#include "babeh.h"
#include "baattr.h"
#include "batyperw.h"


#define MAX_GATE_TABLE 320


/******************************************************************
 *                                                                *
 *                    Definitions of Tables                       *
 *                                                                *
 ******************************************************************/

/*
 * TYPES OF TABLES
 *
 */
typedef enum
{
  GateTable, 
  VarTable,
  OperTable,
  SortTable,
  ProcTable
} KindTableTyp;


/* GtableEntryTyp
 * ENTRY OF THE TABLE OF GATES.
 */
typedef struct { char        *name;
                 GateMaskTyp  mask;
               } GtableEntryTyp;


/* VtableEntryTyp
 * ENTRY OF THE TABLE OF VARIABLES.
 */
typedef struct { char          *name;
                 DescriptorTyp  sort;
               } VtableEntryTyp;


/* StableEntryTyp
 * ENTRY OF THE TABLE OF SORTS.
 */
typedef struct { char *name;
               } StableEntryTyp;


/* PtableEntryTyp
 * ENTRY OF THE TABLE OF PROCESSES.
 */
typedef struct { char      *name;
                 BehTyp     def;
                 int        funclity;
               } PtableEntryTyp;


/* OtableEntryTyp
 * ENTRY OF THE TABLE OF OPERATIONS.
 */

/*
 * list of RuleCellTyp 
 */
typedef ListTyp RewRuleListTyp;


/*
 *  A rewrite rule.
 *
 *    If desired , rewrite rules are processed before being used
 *    If the right hand side of a rewrite rule is a constant expression,
 *    then it is rewritten in order to optimize the speed of the rewrite
 *    function. 
 *
 *  Field "rewrite" is used to indicate the state of the rewrite rule: 
 *
 *          -1 if it has not been processed yet.
 *           0 if it is being preprocesed it this moment.
 *           1 if the rewrite rule has been preprocessed and its
 *             right side is not a constant expression.
 *           2 if the rewrite rule has been preprocessed and its
 *             right side is a constant expression.
 *
 */
typedef struct RuleCell { int            id;
                          int            rewritten;
                          ExprTyp        search_pat;
                          ExprTyp        subst_pat;
                          ListTyp        premises;
                        } RuleCellTyp,*RuleCellPt;


typedef struct { char           *name;
                 ListTyp         argl;
                 DescriptorTyp   sort;
                 boolean         infix;
                 boolean         ofsort;
                 ListTyp         ofsortopl;
                 RewRuleListTyp  rwlist;
                 PMatchTreeTyp   pmt;
               } OtableEntryTyp;


/******************************************************************
 *                                                                *
 *                         Initialization                         *
 *                                                                *
 ******************************************************************/


/* Init_Tables
 * Tables initialitation.
 * This function must be called when the application starts
 * and when a specification is loaded.
 */
extern void Init_Tables();


/* 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.
 */
extern void Reset_Tables();


/* PrintTable
 * Print the specified table from the position l to h.
 * pstr is the function used to print strings.
 */
extern void PrintTable( /* t,l,h,pstr */ );
/*  KindTableTyp  t;
    DescriptorTyp l,h;
    void (*pstr)(); */


/* 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.
 */
extern void StatisticTableO( /* pvcv,pocv,pvcr,pocr,pnlev,pnler,pnlv,
                                pnlr,prc,pmc*/ );
/* int *pvcv,*pocv,*pvcr,*pocr,*pnlev,*pnler,*pnlv,*pnlr,*prc,*pmc; */


/* StatisticTableG
 * Statistics of the table of gates.
 * ngs is the number of gate sets used.
 */
extern void StatisticTableG( /* ngs */ );
/* int *ngs; */


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


/* PrintSize_Tables
 * Print the maximum size and the used size of the tables
 */
extern void PrintSize_Tables();


/* StatRule
 * Rule cells statistics
 */
extern void StatRule( /* used, released */ );
/*       int *used, *released; */


/******************************************************************
 *                                                                *
 *                         TABLE OF GATES                         *
 *                                                                *
 ******************************************************************/

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


/* Declare_gate
 * Insert a new gate in gTab.
 * Return the position of the new entry in the table.
 */
extern DescriptorTyp Declare_gate( /* name */ );
/* char *name; */


/* GetG_name
 * Return the name of the gate whose descriptor is d.
 */
extern char* GetG_name( /* d */ );
/* DescriptorTyp  d; */


/* GetG_mask
 * Return the mask of the gate whose descriptor is d.
 */
extern GateMaskTyp GetG_mask( /* d */ );
/* DescriptorTyp  d; */


/* PutG_mask
 * Put the mask m to the gate whose desriptor is d.
 */
extern void PutG_mask( /* d, m */ );
/* DescriptorTyp  d; 
   GateMaskTyp        m;  */


/* FindG_byMask
 * Return the gate associated to the mask m
 */
extern DescriptorTyp FindG_byMask( /* m */ );
/* GateMaskTyp  m;  */


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


/* PrintG
 * Print the name of the gate d.
 * pstr is the function used to print strings.
 */
extern void PrintG( /* d,pstr */ );
/* DescriptorTyp  d;
   void           (*pstr)(); */


/* SPrintG
 *  Make a string with a gate name. 
 */
extern char * SPrintG( /* d */ );
/*       DescriptorTyp   d; */


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


/******************************************************************
 *                                                                *
 *                       TABLE OF VARIABLES                       *
 *                                                                *
 ******************************************************************/


/* Declare_var
 * Insert a new variable in vTab and
 * return the position of the new entry in the table.
 */
extern DescriptorTyp Declare_var( /* name,sort */ );
/* char *name;
   int   sort; */


/* GetV_name
 * Return the name of the variable whose descriptor is d.
 */
extern char* GetV_name( /* d */ );
/* DescriptorTyp  d; */


/* GetV_sort
 * Return the sort of the variable whose descriptor is d.
 */
extern  DescriptorTyp GetV_sort( /* d */ );
/* DescriptorTyp  d; */


/* PutV_sort
 * Put the sort to the variable whose descriptor is d.
 */
extern DescriptorTyp PutV_sort( /* d, sort */ );
/* DescriptorTyp  d, sort; */


/* EqualV_entry
 * Create an entry equal to d and return its new descriptor.
 */
extern  DescriptorTyp EqualV_entry( /* d */ );
/* DescriptorTyp  d; */


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


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


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


/* 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.
 */
extern void ReleaseRangeTableV( /* from */ );
/* DescriptorTyp from; */


/* LastTableV
 * Return the size of the variable table, where the last elements is stored.
 */
extern DescriptorTyp LastTableV();


/******************************************************************
 *                                                                *
 *                       TABLE OF OPERATIONS                      *
 *                                                                *
 ******************************************************************/


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


/* GetO_name 
 * Return the name of the operation whose descriptor is d.
 */
extern char* GetO_name( /* d */ );
/* DescriptorTyp  d; */


/* GetO_sort
 * Return the sort of the operation whose descriptor is d.
 */
extern DescriptorTyp GetO_sort( /* d */ );
/* DescriptorTyp  d; */


/* GetO_infix
 * Return true if the operation whose descriptor is d is infix.
 */
extern boolean GetO_infix( /* d */ );
/* DescriptorTyp  d; */


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


/* GetO_ofsort
 * Return true if the operation d is "of sort" type. 
 */
extern boolean GetO_ofsort( /* d */ );
/* DescriptorTyp  d; */


/* GetO_ofsortopl
 * Return the list of operations in ofsort conflict with the operation d
 */
extern ListTyp GetO_ofsortopl( /* d */ );
/* DescriptorTyp d; */


/* GetO_pmt 
 * Return the pattern match tree of the operation whose descriptor is d.
 */
extern PMatchTreeTyp GetO_pmt( /* d */ );
/* DescriptorTyp  d; */


/* PutO_sort
 * Put the sort to the operation d
 */
extern DescriptorTyp PutO_sort( /* d, sort */ );
/* DescriptorTyp  d, sort; */


/* GetO_argl
 * Return the argument list of the operation whose descriptor is d.
 */
extern ListTyp GetO_argl( /* d */ );
/* DescriptorTyp  d; */


/* PutO_argl
 * Put the argument list of the operation d.
 */
extern void PutO_argl( /* d, al */ );
/* DescriptorTyp  d;
   ListTyp        al; */


/* PutO_infix
 * Put true if the operation d is infix, else false
 */
extern void PutO_infix( /* d, infix */ );
/* DescriptorTyp  d; 
   boolean        infix;  */


/* PutO_ofsort
 * Put in the "of sort" field of the operation d, the "ofsort" flag
 */
extern void PutO_ofsort( /* d, ofsort */ );
/* DescriptorTyp  d; 
   boolean        ofsort;  */


/* PutO_ofsortopl
 * Put the list of operations ofsortopl as the list of operations
 * in ofsort conflict with operation d
 */
extern void PutO_ofsortopl( /* d, ofsortopl */ );
/* DescriptorTyp  d; 
   ListTyp        ofsortopl;  */


/* PutO_pmt
 * Put the pattern match tree of the operation whose descriptor is d.
 */
extern void PutO_pmt( /* d, pmt */ );
/*       DescriptorTyp  d;
         PMatchTreeTyp  pmt;  */


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


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


/* PrintO
 * Print the name of the operation d.
 * pstr is the function used to print strings.
 */
extern void PrintO( /* d,pstr */ );
/* DescriptorTyp   d;
   void           (*pstr)(); */ 


/* GetO_rwl
 * Return the list of rewrite rules of an operation with descriptor d.
 */
extern RewRuleListTyp GetO_rwl ( /* d */ );
/* DescriptorTyp d;*/


/* 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 premises 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.
 */
extern void PutO_rw( /* pb,ps,l */ );
/* ExprTyp pb,ps;
   ListTyp l ;*/


/* SPrint_rw
 * Make a string with a rewrite rule.
 */
extern char * SPrint_rw( /* RulePt */ );
/*     RuleCellPt  RulePt ; */


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


/******************************************************************
 *                                                                *
 *                       TABLE OF PROCESSES                       *
 *                                                                *
 ******************************************************************/

/*
 *  FUNCTIONALITY
 *
 *  The functionality of each process is stored in the process table
 *  as an index to the former functionality table.
 *  There are three predefined index values with a special meaning:
 *      NOTCALCULATEDF   no calculated functionality
 *      NOEXITF          noexit functionality
 *      EXITF            exit functionality
 *
 *  For other index values the functionality is like: exit ( s1, ..., sn )
 *  Look for in the functionality table.
 */

#define NOTCALCULATEDF   -2
#define NOEXITF -1
#define EXITF    0

typedef ListTyp SortListTyp;

/* FtableEntryTyp
 * ENTRY OF THE TABLE OF FUNCTIONALITIES.
 */
typedef SortListTyp FtableEntryTyp;


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


/* Store_func
 * Store the functionality defined by the sort list sl into the internal
 * functionality table.
 * Returns an index to the table.
 */
extern int Store_func( /* sl */ );
/* SortListTyp sl; */


/* GetF_sl
 * Return the sort list associated to the functionality d
 */
extern SortListTyp GetF_sl( /* d */ );
/*  int  d; */


/* GetP_name
 * Return the name of the process d
 */
extern char* GetP_name( /* d */ );
/* DescriptorTyp  d; */


/* GetP_def
 * Return the pointer to the process definition for the process d
 */
extern BehTyp GetP_def( /* d */ );
/* DescriptorTyp  d; */


/* GetP_func
 * Return the funcionality of the process d
 */
extern int GetP_func( /* d */ );
/* DescriptorTyp  d; */


/* PutP_def
 * Insert the pointer to the process definition for the process d
 */
extern void PutP_def( /* d, def */ );
/* DescriptorTyp  d;
   BehTyp         def; */


/* PutP_func
 * Insert the funcionality of the process d
 */
extern void PutP_func( /* d, funclity */ );
/* DescriptorTyp  d; 
   int            funclity; */


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


/* PrintP
 * Print the name of the process d.
 * pstr is the function used to print strings.
 */
extern void PrintP( /* d,pstr */ );
/* DescriptorTyp   d;
   void           (*pstr)(); */  


/* LastTableP
 * Return the size of the process table, where the last elements is stored.
 */
extern DescriptorTyp LastTableP();


/* DupProcTab_Func
 * Calculates 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.
 */
extern void DupProcTab_Func( /* n */ );
/*       int n; */


/* SPrint_Func
 * Make a string with the functionality func.
 */
extern char * SPrint_Func( /* func */ );
/*       int  func; */


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


/******************************************************************
 *                                                                *
 *                       TABLE OF SORTS                           *
 *                                                                *
 ******************************************************************/

/* Declare_sort
 * Insert a new sort in sTab
 * Return the position of the new entry in the table.
 */
extern DescriptorTyp Declare_sort( /* name */ );
/* char *name; */


/* GetS_name
 * Return the name of the sort d
 */
extern char* GetS_name( /* d */ );
/* DescriptorTyp  d; */


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


/* PrintS
 * Print the name of the sort d.
 * pstr is the function used to print strings.
 */
extern void PrintS( /* d,pstr */ );
/* DescriptorTyp   d;
   void            (*pstr)(); */  


/* SPrintS
 * Return a string with a sort name.
 */
extern char * SPrintS( /* d */ );
/*       DescriptorTyp   d; */


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

#ifdef TIME 
/* FindO_time
 * Search for the  opn "name" that has arguments of sort time
 */ 
extern DescriptorTyp FindO_time (/* name */);
/*  char          *name; */ 
#endif 


#endif



