/******************************************************************
 *  (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

/******************************************************************
 *
 *  Francisco Monfort Martin
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *
 *  3 May 1990
 *
 *  LOTOS data type expressions rewrite system.
 *
 *  Expressions are rewritten by applying recursively One_Rewrite,
 *  which rewrites the most external operation of an expression.
 *
 *  Every operation has attached a set of rewrite rules in the table
 *  of operations.
 *
 *  An operation is rewritten by applying all possible applicable
 *  rewrite rules to that operation.
 *
 *  The subset of applicable rewrite rules is computed by Pattern Matching
 *  of the left hand sides of the rules into the expression, and
 *  rewriting & checking their premises.
 *
 *  A PMT (Pattern Match Tree) is a data structure that must be
 *  attached to each rule in the table of operations in order to
 *  perform a fast pattern matching.
 *
 *  A rule is applied by substitution of the rhs of that rule in the
 *  expression.
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : activate debugging
 *
 *  LOG:
 *     10/06/93 dlarra.
 *     New pattern matching algorithm.
 *
 *     25/01/10 K. J. Turner (KJT)
 *     The constant operation "date_time" is replaced by "YYYYMMDD HHMMSS W"
 *     as a Lotos string
 ******************************************************************/

/* LINTLIBRARY */

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "listdh.h"
#include "listdout.h"
#include "batables.h"
#include "limisc.h"
#include "baattr.h"
#include "batyperw.h"
#include "badefca.h"
#include "babool.h"
#include "balotosf.h"
#include "basust_v.h"

/* KJT 22/01/23: added function prototypes */
boolean StringToExpr(char * s, ExprTyp * pe, DescriptorTyp expSort);

/* KJT 31/01/10: added "time" library and DateTime/LotosString functions */

#include <time.h>

/* DateTime
 * Return current date and time as a string in the format:
 *   YYYYMMDD HHMMSS W
 * where W is 0 (Mon) .. 6 (Sun)
 */

char * DateTime()
{
  char date_time[18];
  time_t time1 = time(NULL);
  struct tm* time2 = localtime(&time1);
  sprintf(date_time, "%04d%02d%02d %02d%02d%02d %d",
    (time2->tm_year + 1900), (time2->tm_mon + 1), time2->tm_mday,
    time2->tm_hour, time2->tm_min, time2->tm_sec,
    (time2->tm_wday + 6) %7);
  return(CopyString(date_time));
}

/* LotosString
 * Copy argument string, returning it as a Lotos string "a~(b ... (<>))".
 * This will work as long as only letters, digits and spaces (converted to '^')
 * are to be translated. Punctuation would need a space after the character.
 */

char * LotosString(str1)
  char * str1;
{
  int len1 = strlen(str1);
  char * str2 = (char *) emalloc(len1 * 5 + 3);
  char * ptr2 = str2;
  char ch;
  while ((ch = *str1++) != '\0') {
    if (ch == ' ') {
      *ptr2++ = '^';
      *ptr2++ = ' ';
      *ptr2++ = '~';
      *ptr2++ = '(';
    }
    else {
      *ptr2++ = ch;
      *ptr2++ = '~';
      *ptr2++ = '(';
    }
  }
  *ptr2++ = '<';
  *ptr2++ = '>';
  int i;
  for (i = 0; i < len1; i++)
    *ptr2++ = ')';
  *ptr2 = '\0';
  return(CopyString(str2));
}

/*  Notation about rules:
 *
 *  a rule has the following pattern :
 *
 *  premise1 => premise2 => ... premiseN => f(x1,...,xn) = g(x1,...,xn) ;
 *
 *  or equivalently:
 *
 *  premises => lhs = rhs ;   or   premises => search_pattern = subst_pattern ;
 *
 */


/* flag_Rules
 *  TRUE if the rewrite rules table has been already rewritten.
 *  FALSE otherwise.
 * This flag must be set to FALSE when a new specification is loaded.
 */
boolean flag_Rules;


/* flag_Beh
 *  TRUE if the expressions in the specification have already been rewritten.
 *  FALSE otherwise.
 * This flag must be set to FALSE when a new specification is loaded.
 */
boolean flag_Beh;


/******************************************************************
 *                                                                *
 *    Management of an internal table to keep track of            *
 *    pattern variables and its expression associated in the      *
 *    expression being rewritten.                                 *
 *                                                                *
 *******************************************************************/

/*
 *   Initial Size and increments of the internal table of matching.
 */
#define MAXTABRW 4096


/*
 *   Internal table for matching between variables and expressions.
 */
typedef struct CellRw { ExprTyp  expres;
			int      var_pat;
		      } CellRwTyp;

static CellRwTyp *MatchingTabRwTyp = NULL;
static int       sizeTabRw         = 0;
static int       nextfreeTabRw     = 0;

/* First position of the current slot. */
typedef int TabRwTyp;

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

/* GetSlotTabRw
 * Get the first position for a new slot in the internal table.
 */
#define GetSlotTabRw() (nextfreeTabRw)

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

/* FreeSlotTabRw
 * Liberate the current slot in the internal table.
 */
static void FreeSlotTabRw(tab)
     TabRwTyp tab;
{
  int i;

  for (i=tab ; i<nextfreeTabRw ; i++)
    FreeE( UnshareE(MatchingTabRwTyp[i].expres) );
  nextfreeTabRw = tab;
}
/* #define FreeSlotTabRw(tab) {nextfreeTabRw = tab;} */

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

/* Is_In_Table
 * Return the position of pat in the internal table tab,
 * if it is in this table, otherwise -1.
 */
static int Is_In_Table( pat_name, tab )
     int pat_name;
     TabRwTyp tab;
{
  int i;

  for ( i=tab; i<nextfreeTabRw; i++ ) {
    if (pat_name == (MatchingTabRwTyp[i].var_pat))
      return i;
  }
  return -1;
}

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

/* Put_In_Table
 * Introduce exp and pat in the internal table tab.
 */
static void Put_In_Table( exp, pat_name )
     ExprTyp exp;
     int     pat_name;
{
  if (sizeTabRw == nextfreeTabRw) {
    if (sizeTabRw == 0) {
      sizeTabRw        = MAXTABRW;
      MatchingTabRwTyp = (CellRwTyp *)emalloc(sizeTabRw*sizeof(CellRwTyp));
    }
    else {
      sizeTabRw       += MAXTABRW;
      MatchingTabRwTyp = (CellRwTyp *)erealloc((void*)MatchingTabRwTyp,
					       (sizeTabRw*sizeof(CellRwTyp)));
      if (MatchingTabRwTyp==NULL)
	Error("Rewrite -> run out of memory.");
    }
  }
  MatchingTabRwTyp[nextfreeTabRw].var_pat = pat_name;
  MatchingTabRwTyp[nextfreeTabRw].expres  = ShareE(exp);
  nextfreeTabRw++;
}

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

/* Get_exp
 * Return the expression of the position number num of the
 * internal table ptab.
 */
static ExprTyp Get_exp( num )
     int num;
{
  LASSERT(num < nextfreeTabRw );
  return MatchingTabRwTyp[num].expres;
}

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

/* InsertTableRw
 * Insert in the table ptab the pair <exp,pat>.
 * If there exist a pair <exp1,pat> in ptab where exp1!=exp, then
 * it is returned FALSE; TRUE otherwise.
 */
static boolean InsertTableRw( exp, pat_name, tab )
     ExprTyp    exp;
     int        pat_name;
     TabRwTyp   tab;
{
  int pos;

  if ( (pos = Is_In_Table(pat_name,tab)) == -1 ) {
    Put_In_Table(exp,pat_name);
    return TRUE;
  }
  else
    return EqualE(exp,MatchingTabRwTyp[pos].expres);
}

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

/* ErrorRule
 * Print a message with a wrong rewrite rule.
 * A wrong rewrite rule is the one which contains a bad-defined
 * variable. Example : f(x) = g(y)
 */
static void ErrorRule(pe,pt)
     ExprTyp   *pe;
     RuleCellPt pt;
{
  char *cr;

  SetPrintParamE(PRINT_NO_PARAM);

  printError("\n\n      Variables used in the right-hand side or in the premises\n");
  printError("      of an equation must be defined in the left-hand side.\n");
  printError("      Please check variable ");
  printError(GetV_name(LookNameE(*pe)));
  printError(" in the following rewrite rule:\n\n      ");
  printError(cr=SPrint_rw(pt));
  (void)free(cr);
  printError("\n\n      Wrong rewrite rule.\n\n");
  Halt();
}

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

/* Fill_Tab_Tmr
 * Replace the variables in the expression e according to tab.
 * Thereafter the new expression is rewritten from the root until the
 * replaced variables ( which are already rewritten ).
 *
 * pt is the rewrite rule which is printed if it contains
 * a bad-defined variable.
 *
 * pe will contain the new expression.
 */
static boolean Fill_Tab_Tmr( pe, pt, tab )
     ExprTyp    *pe;
     RuleCellPt pt;
     TabRwTyp   tab;
{
  int     n,i;
  ExprTyp ne;
  boolean changed;

  LASSERT(*pe != NULL);
  LASSERT(OwnersE(*pe)==0);
  if (IsVariableE(*pe)) {
    i = Is_In_Table(LookNameE(*pe),tab);
    if (i == -1)
      ErrorRule(pe,pt);
    FreeE( *pe );
    *pe = Get_exp(i);
    return TRUE;
  }
  else {
    changed = FALSE;
    n = NumArgE(*pe);
    for (i=1 ; i<=n ; i++) {
      ne = GetArgE(*pe,i);
      LASSERT(OwnersE(ne)==0);
      if (Fill_Tab_Tmr(&ne,pt,tab))
	changed = TRUE;
      PutArgE(*pe,ne,i);
    }
    if (changed) {
      (void) One_Rewrite(pe);
      return TRUE;
    }
    if (pt->rewritten>0)
      return FALSE;
    else {
      return One_Rewrite(pe);
    }
  }
}



/******************************************************************
 *                                                                *
 *              Pattern Matching Trees                            *
 *                                                                *
 ******************************************************************/

/*
 *  Decision tree.
 *
 *  Tree made in order to make quick pattern matching of expressions.
 *  Each operation in the table has one of these decision trees.
 *  The aim is not to perform back-tracking in any case.
 *
 *  Step One: Preorder-wise running of patterns, taking profit of common
 *  --------  root subexpressions.
 *
 *  Example :
 *
 *     x + 0 = x ; (*1* )
 *     1 + 1 = 2 ; (*2* )
 *     1 + 2 = 3 ; (*3* )
 *     2 + 3 = 5 ; (*4* )
 *
 * op. +
 *     |
 *     x-- 1---2
 *     |   |   |
 *     0   |   3
 *     |   |   |
 *   (*1*) | (*4*)      -> lists of applicable rules
 *         |               whose lhs match this pattern
 *         1-----2
 *         |     |
 *       (*2*) (*3*)
 *
 *
 *  Step Two: Collapsing of variables and expanding of values,
 *  --------  ( always keeping the variables at the head of a brotherhood )
 *
 * op. +
 *     |
 *     x-- 1---2
 *     |   |   |
 *     0   |   3------0
 *     |   |   |      |
 *   (*1*) | (*4*)  (*1*)
 *         |
 *         1-----2-----0
 *         |     |     |
 *       (*2*) (*3*) (*1*)
 *
 *
 *
 *  Usage :
 *            BeginConstructPMT( rule_list );
 *
 *             (*  progressive pmt construction * )
 *
 *             pmt = NULL;
 *             for ( rule in rule_list ){
 *               new_pmt = Make_PMatchTree( rule );
 *               if ( pmt==NULL )
 *                 pmt = new_pmt;
 *               else
 *                 pmt = Collapse_PMatchTree( pmt, new_pmt );
 *             }
 *             pmt = Expand_Variables( pmt );
 *
 *            EndConstructPMT(pmt);
 *
 */

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

#define IS_VARIABLE_PMT( n ) ( n->name<0 )

/******************************************************************
 *                                                                *
 *      Account of pattern matching nodes used and released.      *
 *                                                                *
 ******************************************************************/

static int new_pmn_count      = 0;
static int released_pmn_count = 0;

/* InitPMT
 * Init this module
 */
void InitPMT()
{
#ifdef SDEBUG
  new_pmn_count      = 0;
  released_pmn_count = 0;
#endif
}

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

/* StatPMT
 * pmn_used, pmn_released : pmt nodes used and released
 */
void StatPMT( pmn_used, pmn_released )
     int *pmn_used,*pmn_released;
{
  *pmn_used     = new_pmn_count;
  *pmn_released = released_pmn_count;
}

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

/* AuxCountPMT
 */
static void AuxCountPMT( pmt, used_pmt, used_ln )
     PMatchTreeTyp pmt;
     int          *used_pmt, *used_ln;
{
  for ( ; pmt!=NULL; pmt = pmt->brother ){
    AuxCountPMT( pmt->son, used_pmt, used_ln );
    (*used_pmt) ++;
    (*used_ln)  += Length_list( pmt->appl_rules );
  }
}


/* StatisticPMT
 * Number of pmt nodes and list nodes ( of applicable rules ) in a pmt
 */
void StatisticPMT( pmt, used_pmt, used_ln )
     PMatchTreeTyp pmt;
     int          *used_pmt, *used_ln;
{
  (*used_pmt) = 0;
  (*used_ln)  = 0;
  if ( pmt!=NULL )
    AuxCountPMT( pmt, used_pmt, used_ln );
}

/******************************************************************
 *                                                                *
 *           Pattern Match Node Management                        *
 *                                                                *
 ******************************************************************/


/* Create_PMTNode
 *
 */
static PMatchTreeTyp Create_PMTNode()
{
  PMatchTreeTyp n;

  n             = (PMatchTreeTyp)NewCellM(sizeof(PMatchNodeTyp));
  n->name       = 0;
  n->son        = NULL;
  n->brother    = NULL;
  n->appl_rules = Create_list();
#ifdef SDEBUG
  new_pmn_count++;
#endif

  return n;
}

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

/* Dispose_PMTNode
 *
 */
static void Dispose_PMTNode( n )
     PMatchTreeTyp n;
{
  FreeCellM( (void*)n, sizeof(PMatchNodeTyp) );
#ifdef SDEBUG
  released_pmn_count++;
#endif
}


/******************************************************************
 *                                                                *
 *            Pattern Match Trees Management                      *
 *                                                                *
 ******************************************************************/


/* FreePMT
 * Free a pmt
 */
void FreePMT( n )
     PMatchTreeTyp n;
{
  if ( n!=NULL ){
    FreePMT( n->son );
    FreePMT( n->brother );
    Disp_list( n->appl_rules );
    Dispose_PMTNode(n);
  }
}

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

/* Copy_PMatchTree
 * Copy a pmt
 */
PMatchTreeTyp Copy_PMatchTree( pmt )
     PMatchTreeTyp pmt;
{
  PMatchTreeTyp n;

  n = NULL;
  if ( pmt!=NULL ){
    n             = Create_PMTNode();
    n->name       = pmt->name;
    n->son        = Copy_PMatchTree( pmt->son );
    n->brother    = Copy_PMatchTree( pmt->brother );
    n->appl_rules = Copy_list( pmt->appl_rules, (DataListTyp(*)())EchoInt );
  }
  return n;
}

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

/* Expr_to_PMT
 * Transform a search pattern e into a pmt.
 * *last will contain the last node of the pmt.
 */
static PMatchTreeTyp Expr_to_PMT( e, last )
     ExprTyp        e;
     PMatchTreeTyp *last;
{
  ExprTyp       ei;
  PMatchTreeTyp n, arg_last;
  int           i,j;

  n      = NULL;
  *last  = NULL;
  if ( e!=NULL ){
    n         = Create_PMTNode();
    n->name   = LookNameE(e);
    *last     = n;
    /* parameterized values are ignored */
    if ( IsOperationE(e) ){
      arg_last  = n;
      j = NumArgE(e);
      for (i=1 ; i<=j ; i++){
	ei = LookArgE(e,i);
	(*last)->son = Expr_to_PMT( ei, &arg_last );
	*last = arg_last;
      }
    }
  }
  return n;
}


/* Make_PMatchTree
 *  Convert a rule into a single pattern match tree.
 *  Example : Make_PMatchTree( (*1*) succ(succ(x))+0 = 0 ) =   +
 *                                                             |
 *                                                             succ
 *                                                             |
 *                                                             succ
 *                                                             |
 *                                                             x
 *                                                             |
 *                                                             0
 *                                                           (*1*)
 *
 */
PMatchTreeTyp Make_PMatchTree( rule )
     RuleCellPt rule;
{
  ExprTyp       e,ei;
  PMatchTreeTyp arg_last, last, pmt;
  int           n,i;

  e = rule->search_pat;
  LASSERT( e!=NULL );

  last = arg_last  = NULL;
  pmt  = NULL;
  n    = NumArgE(e);
  for ( i=1 ; i<=n ; i++ ) {
    ei = LookArgE(e,i);
    if ( pmt==NULL )
      pmt = Expr_to_PMT( ei, &arg_last );
    else
      last->son = Expr_to_PMT( ei, &arg_last );
    last = arg_last;
  }
  if ( last!=NULL )
    last->appl_rules = Insert_list( (DataListTyp)rule, last->appl_rules );

  return pmt;
}

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

static ListTyp vl,this_rule_vl;
static SVdescriptorTyp sv;
static ExprListTyp new_premises;

/*
 *  this algorithm assumes that EqualV_entry provides a globally unique var id.
 */
static void MkUniqueVars( expr )
     ExprTyp expr;
{
  DescriptorTyp name;
  ExprTyp       prem;
  int           n,i;

  if ( IsVariableE(expr) ){
    name = LookNameE(expr);
    if ( In_list( (DataListTyp)name, this_rule_vl, EqInt ) ){
      ChangeNameE( expr, EqualV_entry(name) );
      PutPVarE( expr, MakeE(name,VariableC) );
      prem = MakeE(GetEqual(),OperationC);
      AddArgE(prem,MakeE(name,VariableC));
      AddArgE(prem,CopyE(expr));  /*mse*/
      new_premises = InsertEL( prem, new_premises );
      /* void premise always at the head of the list */
    }
    else {
      this_rule_vl = Insert_list( (DataListTyp)LookNameE(expr), this_rule_vl );
      if ( In_list( (DataListTyp)name, vl, EqInt ) )
	ChangeNameE( expr, EqualV_entry(name) );
      PutPVarE( expr, MakeE(name,VariableC) );
      InsertSV( name, CopyE(expr), &sv );  /*mse*/
    }
  }
  else {
    n = NumArgE(expr);
    for ( i=1 ; i<=n ; i++ ) {
      MkUniqueVars(LookArgE(expr,i));
    }
  }
}

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

/* MakeUniqueVars_Rules
 * Redefine equal variables found in the search pattern of a list of rules.
 * Leave the old variables parameterized.
 *  Example :
 *   f(x) => g(x,x,y) = h(y,x) ;
 *           g(x,z,z) = z ;
 *      is transformed into
 *   x(*x*) = x'(*x*) => f(x(*x*))=>
 *                       g(x(*x*),x'(*x*),y(*y*))  = h(y(*y*),x(*x*));
 *   z(*z*) = z'(*z*) => g(x"(*x*),z(*z*),z'(*z*)) = z(*z*) ;
 *
 * The parameterized expression are used only for printing.
 */
static void MakeUniqueVars_Rules( rl )
     ListTyp rl;
{
  RuleCellPt rule;
  ListTyp    pl;
  ExprTyp    e;

  vl = Create_list();
  for ( ; rl!=NULL; rl=Next_list(rl) ){
    rule         = (RuleCellPt)LookInfo_list(rl);
    sv           = CreateSV();
    this_rule_vl = Create_list();
    new_premises = CreateEL();
    e            = GetE(UnshareE(rule->search_pat));
    MkUniqueVars(e); /* sv is updated */
    rule->search_pat = ShareE(e);
    e                = GetE(UnshareE(rule->subst_pat));
    (void)SubstExprNoRwSV( &e, &sv );
    rule->subst_pat = ShareE(e);
    rule->premises  = Join_list(new_premises,rule->premises);
    for ( pl = rule->premises; pl!=NULL; pl = Next_list(pl) ){
      e = GetE(UnshareE((ExprTyp)GetInfo_list(pl)));
      (void)SubstExprNoRwSV( &e, &sv );
      PutInfo_list( pl, (DataListTyp)ShareE(e) );
    }
    vl = Join_list( this_rule_vl, vl );
    FreeSV(&sv);
  }
  Disp_list(vl);
}

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

/* DrawPMTNode
 * Print the pattern match cell n.
 * pstr is the function used to print strings.
 */
static void DrawPMTNode( n, pstr )
     PMatchTreeTyp n;
     void        (*pstr)();
{
  ListTyp rl;

  if ( n->name < 0 )
    PrintV( n->name, TRUE, pstr );
  else
    PrintO( n->name, pstr );
  rl = n->appl_rules;
  pstr( " -> " );
  while ( rl!=NULL ) {
    Print_rw( (RuleCellPt)LookInfo_list(rl), pstr );
    rl = Next_list( rl );
  }
}

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

/* DrawPMT
 * Print the no Null Tree t with indentation pos.
 * pstr is the function used to print strings.
 */
static void DrawPMT( t, pos, pstr )
     PMatchTreeTyp  t;
     int       pos;
     void      (*pstr)();
{
  int i;

  while ( t != NULL ) {
    for ( i=0 ; i<pos ; i++ )
      pstr("| ");
    DrawPMTNode(t,pstr);
    pstr("\n");
    DrawPMT(t->son,pos+1,pstr);
    t = t->brother;
  }
}

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

/* Draw_PMatchTree
 * Draw the pattern match tree t.
 * pstr is the function used to print strings.
 */
void Draw_PMatchTree( t, pstr )
     PMatchTreeTyp  t;
     void      (*pstr)();
{
  LASSERT(t!=NULL);
  DrawPMT( t,0,pstr );
}


/******************************************************************
 *                                                                *
 *           Pattern Match Tree Composition                       *
 *                                                                *
 ******************************************************************/

/* SkipExpr
 * Return a list of nodes that corresponds with the last elements of
 * an expression according to the preorder given by pmt.
 * args must be initialized to 1.
 *  example: for a pmt made by the conjunction of suc(succ(x))+5 and succ(0)+y
 *           SkipExpr(pmt,1) would return the nodes of 5 and y.
 */
static ListTyp SkipExpr( pmt, args )
     PMatchTreeTyp pmt;
     int           args;
{
  ListTyp l;

  LASSERT( args>0 );

  args--;
  if ( !IS_VARIABLE_PMT(pmt) )
    args += Length_list(GetO_argl(pmt->name));

  l = Create_list();
  if ( args==0 )
    return Insert_list( (DataListTyp)pmt, l );

  for ( pmt=pmt->son; pmt!=NULL; pmt = pmt->brother )
    l = Join_list( l, SkipExpr( pmt, args ) );
  return l;

}

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

/* CollapseRules
 * both rule lists are disposed off
 */
static ListTyp CollapseRules( rl1, rl2 )
     ListTyp rl1,rl2;
{
  DataListTyp rule;
  ListTyp     l;

  for ( l=rl2; l!=NULL; l=Next_list(l) ){
    rule = GetInfo_list(l);
    if ( !In_list( rule, l, EqInt ) )
      rl1 = Add_list( rule, rl1 );
  }
  Disp_list( rl2 );
  return rl1;
}

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

static void RenameRulesVars();
PMatchTreeTyp Collapse_PMatchTree();

/* Insert_Variable
 * Insert a variable in a pmt. This must be at the head of the pmt-level
 * brotherhood. Solve variables collisions.
 */
static PMatchTreeTyp Insert_Variable( pmt, element )
     PMatchTreeTyp  pmt, element;
{
  LASSERT( pmt!=NULL && element!=NULL);

  if ( IS_VARIABLE_PMT(pmt) ){                 /* another var in the pmt */

    /*
     * collapse applicable rules
     */
    pmt->appl_rules = CollapseRules( pmt->appl_rules, element->appl_rules );

    RenameRulesVars( element->name, pmt->name );
    pmt->name = element->name;
    pmt->son  = Collapse_PMatchTree( pmt->son, element->son );
    Dispose_PMTNode(element);
  }
  else {
    element->brother = pmt;               /* no redundancy */
    pmt              = element;
  }
  return pmt;
}

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

static PMatchTreeTyp Insert_Operation( pmt, element )
     PMatchTreeTyp  pmt, element;
{
  PMatchTreeTyp cursor, prev;
  boolean       found;

  found = FALSE;
  for ( prev = cursor = pmt;
       cursor!=NULL && (cursor->name <= element->name);
       prev = cursor, cursor=cursor->brother ){
    if ( cursor->name==element->name ){
      found = TRUE;
      break; /* for */
    }
  }
  if ( found ){                        /* op. redundancy */
    cursor->appl_rules = CollapseRules( cursor->appl_rules,
				       element->appl_rules );
    cursor->son        = Collapse_PMatchTree( cursor->son, element->son );
    Dispose_PMTNode(element);
  }
  else                               /* no op. redundancy */
    if ( cursor==NULL ){               /* at the end. */
      prev->brother    = element;       /* adopt this node */
      element->brother = NULL;
      LASSERT(prev->name<element->name);
    }
    else {                             /* other places */
      if ( prev == cursor ){            /* the first turned out to be bigger */
	element->brother = prev;
	pmt              = element;
      }
      else {                            /* in the middle */
	prev->brother    = element;
	element->brother = cursor;
      }
      LASSERT(element->name<cursor->name);
    }
  return pmt;
}

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

/* Expand_Variables
 * Expansion of variables with the operations of its level.
 * Entry conditions :
 *  1) all levels in both pmt's have one variable node utmost, and this is
 *     at the beginning.
 */
PMatchTreeTyp Expand_Variables( pmt )
     PMatchTreeTyp pmt;
{
  PMatchTreeTyp cursor,father,var;
  ListTyp       l,parents;

  if ( pmt==NULL )
    return NULL;

  var    = IS_VARIABLE_PMT(pmt) ? pmt : NULL;
  cursor = pmt->brother;
  if ( var!=NULL )
    while ( cursor!=NULL ){
      LASSERT(!IS_VARIABLE_PMT(cursor));
      parents = SkipExpr( cursor, 1 );
      LASSERT( parents!=NULL );
      for ( l=parents; l!=NULL; l=Next_list(l) ){
	father = (PMatchTreeTyp)LookInfo_list(l);
	if ( var->son!=NULL )
	  father->son = Collapse_PMatchTree( father->son,
					    Copy_PMatchTree(var->son)
					    );
	else {
	  father->appl_rules =
	    CollapseRules( father->appl_rules,
			  Copy_list(var->appl_rules, (DataListTyp(*)())EchoInt)
			  );
	}
      }
      Disp_list(parents);
      cursor = cursor->brother;
    }

  for ( cursor=pmt; cursor!=NULL; cursor=cursor->brother )
    cursor->son = Expand_Variables(cursor->son);

  return pmt;
}

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

/* Collapse_PMatchTree
 * Collapse pmt and pmt2 but do not expand variables.
 * (pmt & pmt2 are disposed off)
 * Entry conditions :
 *   1) initially all the variables of the rules are different.
 *   2) all levels in both pmt's have one variable node utmost.
 *
 * Output : Simple collapse.
 *  Both operations and the variables are collapsed.
 *  The variable of a level is left at the head of it.
 *
 */
PMatchTreeTyp Collapse_PMatchTree( pmt, pmt2 )
     PMatchTreeTyp  pmt, pmt2;
{
  PMatchTreeTyp brother;

  if ( pmt==NULL ){
    LASSERT( pmt2==NULL );
    return NULL;
  }
  do {
    brother = pmt2->brother;
    if ( IS_VARIABLE_PMT(pmt2) )
      pmt = Insert_Variable( pmt, pmt2 );
    else
      pmt = Insert_Operation( pmt, pmt2 );
    pmt2 = brother;
  } while ( pmt2!=NULL );
  return pmt;
}

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

static void BeginConstructPMT();
static void EndConstructPMT();

/* MakePMT
 * Take the rewrite rules of an operation as input and
 * return the corresponding pattern match tree
 */
PMatchTreeTyp MakePMT( rwl )
     ListTyp rwl;
{
  ListTyp        l;
  PMatchTreeTyp  pmt,new_pmt;
  RuleCellPt     rule;

  MakeUniqueVars_Rules( rwl );
  BeginConstructPMT( rwl );
  pmt = NULL;
  for ( l=rwl; l!=NULL; l=Next_list(l) ){
    rule = (RuleCellPt)LookInfo_list(l);
    new_pmt = Make_PMatchTree( rule );
    if ( pmt==NULL )
      pmt = new_pmt;
    else
      pmt = Collapse_PMatchTree( pmt, new_pmt );
  }
  pmt = Expand_Variables( pmt );
  EndConstructPMT( pmt );

  return pmt;
}


/******************************************************************
 *                                                                *
 *           expression - pattern matching                        *
 *                                                                *
 ******************************************************************/

/* LastPMT_Expr
 * If expression expr matches onto pmt, then return the last node matched.
 *   This node contains the list of applicable rules.
 * Otherwise
 *   return NULL
 */
static PMatchTreeTyp LastPMT_Expr( expr, pmt, tab )
     ExprTyp       expr;
     PMatchTreeTyp pmt;
     TabRwTyp      tab;
{
  PMatchTreeTyp var;
  int n,i;

  var = NULL;
  if ( IS_VARIABLE_PMT(pmt) ){
    var = pmt;
    pmt = pmt->brother;
    (void)InsertTableRw( expr, var->name, tab );
  }
  while ( pmt!=NULL ){
    if ( LookNameE(expr)==pmt->name ){
      if ( pmt->son!=NULL ) {
	n = NumArgE(expr);
	for (i=1 ; i<=n ; i++)
	  if ((pmt = LastPMT_Expr(LookArgE(expr,i),pmt->son,tab)) == NULL)
	    return var;
      }
      return pmt;
    }
    else
      pmt = pmt->brother;
  }
  return var;
}

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

/* Applicable_Rules
 * return the list of applicable rw-rules to an operation.
 */
ListTyp Applicable_Rules( expr, tab )
     ExprTyp  expr;
     TabRwTyp tab;
{
  int           n,i;
  DescriptorTyp d;
  PMatchTreeTyp pmt;

  LASSERT(IsOperationE(expr));

  d   = LookNameE(expr);
  pmt = GetO_pmt(d);

  if ( pmt==NULL )
    return GetO_rwl(d);

  n = NumArgE(expr);
  for (i=1 ; i<=n ; i++) {
    if ((pmt = LastPMT_Expr(LookArgE(expr,i),pmt,tab)) == NULL)
      return NULL;
    if (i!=n) pmt = pmt->son;
  }

  LASSERT( pmt->son==NULL );
  return pmt->appl_rules;
}

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

static ExprListTyp rule_vars;

/*
 * eye: this sv table is used in an odd way.
 * It is used to keep a record of variables unifications.
 * ouvn holds initially : ( LookNameE(var_in_rule), var_in_rule )
 * but the construction of the pmt changes var_in_rules' names.
 */

static SVdescriptorTyp ouvn;

static void RenameRulesVars( new, old )
     DescriptorTyp new, old;
{
  ExprTyp v;
  ListTyp l;

  if ( new!=old )
    for ( l=rule_vars; l!=NULL; l=Next_list(l) ){
      v = (ExprTyp)LookInfo_list(l);
      if ( LookNameE(v)==old )
	ChangeNameE( v, new );
    }
}

/* BeginConstructPMT
 * Init the construction of a new pmt for a list of rules
 */
static void BeginConstructPMT( rwl )
     ListTyp rwl;
{
  RuleCellPt  rule;
  ListTyp     premises,rv,psp_vars, rsp_vars;
  ExprTyp     var;

  rule_vars = CreateEL();
  ouvn      = CreateSV();
  for ( ;  rwl!=NULL;  rwl = Next_list(rwl) ){
    rule = (RuleCellPt)LookInfo_list(rwl);
    psp_vars  = LookVarsInExpr( rule->subst_pat );
    for ( premises = rule->premises;
	 premises!=NULL;
	 premises = Next_list(premises) )
      psp_vars  = Join_list( psp_vars,
			    LookVarsInExpr((ExprTyp)LookInfo_list(premises)));

    rsp_vars  = LookVarsInExpr( rule->search_pat );
    for ( rv = psp_vars; rv!=NULL;  rv = Next_list(rv) )
      if ( !In_list( LookInfo_list(rv), rsp_vars, EqualE ) ){
	var = (ExprTyp)LookInfo_list(rv);
	ErrorRule(&var,rule);
      }
    rule_vars = Join_list( rule_vars, rsp_vars );
    rule_vars = Join_list( rule_vars, psp_vars );
  }


  for ( rv = rule_vars;  rv!=NULL;  rv = Next_list(rv) ){
    InsertSV( LookNameE((ExprTyp)LookInfo_list(rv)),
	     (ExprTyp)LookInfo_list(rv),
	     &ouvn );
  }
}

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

/* UnifyVariables
 * Run the pmt and verify that the unification of variable names is consistent
 */
static void UnifyVariables( pmt )
  PMatchTreeTyp pmt;
{
  while ( pmt != NULL ) {
    if ( IS_VARIABLE_PMT(pmt) ){
      pmt->name = LookNameE(GetActExp_SV( pmt->name, &ouvn ));
    }
    UnifyVariables(pmt->son);
    pmt = pmt->brother;
  }
}

/* EndConstructPMT
 * End of construction of the pmt of a list of rules.
 */
static void EndConstructPMT( pmt )
     PMatchTreeTyp pmt;
{
  UnifyVariables(pmt);
  FreeEL(rule_vars);
  FreeSV(&ouvn);
}


/******************************************************************
 *                                                                *
 *          Expression Rewrite                                    *
 *                                                                *
 ******************************************************************/


/* CheckPremises
 *  TRUE  if the premises of the rewrite rule are true;
 *  FALSE otherwise.
 */
static boolean CheckPremises( pt, tab )
     RuleCellPt pt;
     TabRwTyp   tab;
{
  ListTyp l;
  ExprTyp p;

  for ( l=pt->premises ; l != NULL ; l=Next_list(l) ) {
    p = CopyUntilVarE((ExprTyp)LookInfo_list(l));
    /*
       printError("  ");
       PrintE(p,printError);
       printError("\n");
       */
    (void) Fill_Tab_Tmr(&p,pt,tab);
    /*
       p = FalseIfConst(p);
       */
    LASSERT((!IsConstE(p))||(!IsEqual(p)));

    if ( !IsTrue(p) ) {
      LASSERT(OwnersE(p)==0);
      FreeE(p);
      return FALSE;
    }
    FreeE(p);
  }
  return TRUE;
}

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

static void Rew_rhs_and_premises();

/* Apply
 *  Return
 *    TRUE if it's possible to apply the rewrite rule pt to the
 *            expression *pexp;
 *    FALSE otherwise.
 *  If possible, the rewrite rule is applied.
 *  *pexp never is a variable ( variables haven't got rewrite rules).
 */
static boolean Apply( pexp, pt, tab )
     ExprTyp   *pexp;
     RuleCellPt pt;
     TabRwTyp   tab;
{
  ExprTyp  ne;

  LASSERT(*pexp != NULL);
  LASSERT(pt->search_pat != NULL);

  if (pt->rewritten==-1)
    Rew_rhs_and_premises(pt);

  if (CheckPremises(pt,tab)) {
    if (pt->rewritten==2) {
      GlueE(*pexp,pt->subst_pat);
    }
    else {
      ne = CopyUntilVarE(pt->subst_pat);
      (void) Fill_Tab_Tmr(&ne,pt,tab);
      GlueE(*pexp,ne);
    }
    return TRUE;
  }
  return FALSE;
}

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

/* Search_Apply_Rule
 * Search and apply one rewrite rule to the expression *pexp . If
 * it's posible it returns TRUE, FALSE otherwise.
 */
static boolean Search_Apply_Rule(pexp)
     ExprTyp *pexp;
{
  ListTyp       l;
  RuleCellPt    p;
  TabRwTyp      tab;

  if ( IsOperationE(*pexp) ) {
    tab = GetSlotTabRw();
    l   = Applicable_Rules( *pexp, tab );
    while ( l!=NULL ) {
      p = (RuleCellPt)LookInfo_list(l);
      LASSERT(p != NULL);
      if ( Apply(pexp,p,tab) ){
	FreeSlotTabRw(tab);
	return TRUE;
      }
      l = Next_list(l);
    }
    FreeSlotTabRw(tab);
    return FALSE;
  }
  else {
    return FALSE;
  }
}

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

/* One_Rewrite
 * Apply all the possible rewrite rules to the most external operation
 * of the expression exp.
 */
boolean One_Rewrite( pexp )
     ExprTyp *pexp;
{
  boolean res;

  res = FALSE;
  while ( Search_Apply_Rule(pexp) )
    res = TRUE;
  if (IsEqual(*pexp) )
    if (EqualE(LookArgE(*pexp,1),LookArgE(*pexp,2))) {
      GlueE(*pexp,MakeE(GetTrue(),OperationC));
    }
    else if (IsConstE(*pexp)) {
      GlueE(*pexp,MakeE(GetFalse(),OperationC));
    }
  return res;
}

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

/* Rewrite
 * Return the rewritten expression of the expression exp.
 */
ExprTyp Rewrite( exp )
     ExprTyp  exp;
{
  int n,i;

  if (IsVariableE(exp)) {
    return exp;
  }
  else {
    n = NumArgE(exp);
    for (i=1 ; i<=n ; i++) {
      (void)Rewrite(LookArgE(exp,i));
    }
    if (strcmp(GetO_name(LookNameE(exp)),"date_time") == 0) {
      char * date_time =  LotosString(DateTime());
      StringToExpr(date_time,&exp,0);
      One_Rewrite(&exp);
    }
    else
      (void) One_Rewrite(&exp);
    return exp;
  }
}

/******************************************************************
 *                                                                *
 *            Predicates evaluation                               *
 *                                                                *
 ******************************************************************/

/* FalseIfConst
 * If e is a constant expression then it is rewritten to false.bool
 */
ExprTyp FalseIfConst(exp)
     ExprTyp exp;
{
  LASSERT(OwnersE(exp)==0);
  exp = GetE(exp);
  if ( !IsTrue(exp) && IsConstE(exp) ) {
    GlueE(exp,MakeFalse());
  }
  return exp;
}

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

/* RewritePred
 */
static void RewritePred ( pp )
     PredicateTyp     *pp;
{
  ExprListTyp   vl1,vl2;
  ExprTyp       er;
  PredNodeTyp   pn;
  PredicateTyp  p,newp;

  newp = NULL;
  p = *pp;
  while (p != NULL) {
    pn = (PredNodeTyp)LookInfo_list(p);
    LASSERT(OwnersE(pn->rewritten)==1);
    /*
       er = FalseIfConst(Rewrite(UnshareE(pn->rewritten)));
       */
    er = Rewrite(UnshareE(pn->rewritten));
    LASSERT((!IsConstE(er))||(!IsEqual(er)));

    pn->rewritten = ShareE(er);
    if (IsFalse(er)) {
      FreePred(*pp);
      FreePred(newp);
      *pp = NewPred(MakeE(GetFalse(),OperationC),(ExprTyp)NULL);
      return;
    }
    else if (!IsTrue(er)) {
      if (pn->original != NULL) {
	LASSERT(OwnersE(pn->original)==1);
	vl1 = VarsInE(er);
	vl2 = VarsInE(pn->original);
	if (Length_list(vl1)!=Length_list(vl2)) {
	  FreeE(UnshareE(pn->original));
	  pn->original = NULL;
	}
	FreeEL(vl1);
	FreeEL(vl2);
      }
      newp = AddPremisePred(newp,pn->rewritten,pn->original);
    }
    p = Next_list(p);
  }
  FreePred(*pp);
  if (newp != NULL)
    *pp = newp;
  else
    *pp = NewPred(MakeE(GetTrue(),OperationC),(ExprTyp)NULL);
}

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

/* Evaluate
 * Evaluate (rewrite) the predicate p.
 * Returns 't' if the result is true.bool, 'f' if it is false.bool
 * and 'i' in another case.
 */
char Evaluate( pp )
     PredicateTyp  *pp;
{
  LASSERT(*pp!=NULL);
  LASSERT( LookRwPred(*pp)!=NULL);
  RewritePred(pp);
  if (IsTrue(LookRwPred(*pp)))
    return 't';
  if (IsFalse(LookRwPred(*pp)))
    return 'f';
  *pp = RemoveEqualExprPred(*pp);
  return 'i';
}

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

/* OneEvaluate
 * Evaluate (One_Rewrite) the predicate p.
 * Return 't' if the result is "true.bool", 'f' if it is "false.bool"
 * and 'i' otherwise.
 */
char OneEvaluate( p )
     PredicateTyp  p;
{
  LASSERT(p!=NULL);
  LASSERT(LookRwPred(p)!=NULL);
  /*
   * p->rewritten = ShareE(FalseIfConst(UnshareE(p->rewritten)));
   *
   */
  if (IsTrue(LookRwPred(p)))
    return 't';
  if (IsFalse(LookRwPred(p)))
    return 'f';
  return 'i';
}


/******************************************************************
 *                                                                *
 *        Rewriting of Rules.                                     *
 *                                                                *
 *        Only premises and rhs's are rewritten.                  *
 *                                                                *
 ******************************************************************/

/* RewriteConstantExpressions
 * Rewrite all the subexpressions of e thar are constant expressions.
 * If the expression e is constant then it returns TRUE else FALSE.
 */
static boolean RewriteConstantExpressions( e )
     ExprTyp e;
{
  int     n,i;
  boolean res;

  if (IsVariableE(e)) {
    return FALSE;
  }
  else { /* operation */
    n   = NumArgE(e);
    res = TRUE;
    for ( i=1 ; i<=n ; i++ ) {
      if ( ! RewriteConstantExpressions(LookArgE(e,i)) )
	res = FALSE;
    }
    if (res)
      (void) One_Rewrite(&e);
    return res;
  }
}

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

/* Rew_rhs_and_premises
 * Rewrite the rewrite rules of one operator.
 */
static void Rew_rhs_and_premises( CellPt )
     RuleCellPt CellPt;
{
  ExprTyp aux;
  ListTyp l;

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

  if (CellPt->rewritten!=-1)
    return;

  CellPt->rewritten=0;

  l = CellPt->premises;
  while (l != NULL) {
    aux = CopyE((ExprTyp)l->info);
#ifdef REWRITERULES
    aux = Rewrite(aux);
#else
    (void) RewriteConstantExpressions(aux);
#endif
    /*
     * aux = FalseIfConst(aux);
     */
    LASSERT((!IsConstE(aux))||(!IsEqual(aux)));

    FreeE(UnshareE((ExprTyp)l->info));
    l->info = (DataListTyp) ShareE(aux);
    l = Next_list(l);
  }

  aux = CopyE(CellPt->subst_pat);
#ifdef REWRITERULES
  aux = Rewrite(aux);
  CellPt->rewritten = IsConstE(aux) ? 2 : 1 ;
#else
  CellPt->rewritten = RewriteConstantExpressions(aux) ? 2 : 1 ;
#endif
  FreeE(UnshareE(CellPt->subst_pat));
  CellPt->subst_pat = ShareE(aux);
}

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

/* Pre_Rw_Rules
 * Redefine duplicate variables of lhs's of rules.
 *  Example : for b(x)=>f(x,x,y)=g(x,y) would yield
 *                b(x)=>x=x'=>f(x,x',y)=g(x,y).
 *
 * And build up the pattern match tree of the equations of each operation.
 */
static void Pre_Rw_Rules()
{
  int            i;
  ListTyp        rwl;
  PMatchTreeTyp  pmt;

  for ( i = 1 ; i <= LastTableO() ; i++ ){
    rwl = GetO_rwl(i);
    pmt = MakePMT( rwl );
    PutO_pmt(i, pmt);
  }
}

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

/* Rw_Rules
 * Rewrite the substitution pattern and the premises of all the
 * rewrite rules of all the operators.
 * This function must be called before any rewrite process can be done.
 */
void Rw_Rules()
{
#ifdef REWRITERULES
  int     i,j;
  char    buff[1024];
  ListTyp l;
#endif

  if (!flag_Rules) {

    /* redefine duplicated variables inside rules */
    /* and make the pattern match trees */
#ifdef SDEBUG
    printMsgs(" Building the rewrite rules tree.\n");
#endif
    Pre_Rw_Rules();
#ifdef SDEBUG
    printMsgs(" Building done.\n");
#endif

#ifdef REWRITERULES
    printMsgs(" Rewriting rewrite rules.\n");
    for ( i = 1 ; i <= LastTableO() ; i++ )
      if ( GetO_rwl(i)!=NULL) {
	if (runtimeConfig==TextMode) {
	  (void)sprintf(buff,"\015 %5d = %-70s",i,GetO_name(i));
	  printMsgs(buff);
	}
	else {
	  (void)sprintf(buff," %5d = %-70s",i,GetO_name(i));
	  printPos(buff,-2);
	  flushTarget();
	}
	Apply_Proc_list(GetO_rwl(i),Rew_rhs_and_premises);
      }
    if (runtimeConfig==TextMode) {
      (void)sprintf(buff,"\015 %-78s\n","Rewriting done.");
      printMsgs(buff);
    }
    else {
      (void)sprintf(buff," %-78s\n","Rewriting done.");
      printPos(buff,-2);
      flushTarget();
    }
#endif
    flag_Rules = TRUE;
  }
}


/******************************************************************
 *                                                                *
 *          Rewrite of expressions in behaviours                  *
 *                                                                *
 ******************************************************************/

static ExprTyp Rw1Expr( e )
     ExprTyp e;
{
  return ShareE(Rewrite(UnshareE(e)));
}

/* Rw1Beh
 * Rewrite the expression in the behaviour b.
 */
static void Rw1Beh( b )
     BehTyp b;
{
#ifdef TIME
  PTimeTyp         time;
#endif
  ExprListTyp      el;
  OfferListTyp     ol;
  ExprTyp          e;
  VarAssignListTyp val;
  PAttrTyp         a;
  ITContListTyp    itcl;
  PITContTyp       pit;
  int              i;
  char             c;

  while ( b!=NULL ) {
    switch ( LookTypeB(b) )
      { case IC:
	case HidingC:
	case RelabellingC:
	case ChoiceC:
	case ProcessDefC:
	case SpecificationC:
	case ParC:
	case GateChoiceC:
	  b =  LookArgB(b,1);
	  break;

	case StopC:
	case TerminationC:
	  b =  NULL;
	  break;

	case ProcessInstC:
	  a = LookA(b,ELA);
	  if (a!=NULL) {
	    el = (ExprListTyp)GetAInfo(a);
	    Apply_Func_list(el,(DataListTyp(*)())Rw1Expr);
	    PutAInfo(a,(AttrValueTyp)el);
	  }
	  b = NULL;
	  break;

	case GuardC:
	  if (SolvePredicate(b) != 'i')
	    SolvePredicateBeh(b);
	  else
	    b = LookArgB(b,1);
	  break;

	case GateC:
	  c = SolvePredicate(b);
	  if (c != 'i')
	    SolvePredicateBeh(b);
	  if (c != 'f') {
	    a = LookA(b,OLA);
	    ol = (OfferListTyp)LookAInfo(a);
	    while (ol != NULL ) {
	      if (IsThereExclamationOL(ol)) {
		e = Rewrite(GetExprOffer(ol));
		PutExprOffer(ol,e);
	      }
	      ol = MvNextOffer(ol);
	    }
#ifdef TIME
	    a =  LookA(b,TA);
	    if (a!=NULL){
	      time = (PTimeTyp)  GetAInfo(a);
	      time->lower_bound = Rewrite(time->lower_bound);
	      time->upper_bound = Rewrite(time->upper_bound);
	      PutAInfo(a, (AttrValueTyp) time);
	    }
#endif
	  }
	  if (c == 'i') /* transforms "a ?x:s [x=E]" into "a !E" */
	    SimplifyPredAndOL( b );

	  if (c == 'f')
	    b = NULL;
	  else
	    b = LookArgB(b,1);
	  break;

	case ExitC:
	  a = LookA(b,OLA);
	  ol = (OfferListTyp)LookAInfo(a);
	  while (ol != NULL ) {
	    if (IsThereExclamationOL(ol)) {
	      e = Rewrite(GetExprOffer(ol));
	      PutExprOffer(ol,e);
	    }
	    ol = MvNextOffer(ol);
	  }
	  b = NULL;
	  break;

	case PletC:
	  a = LookA(b,VALA);
	  if (a!=NULL) {
	    val = (VarAssignListTyp)LookAInfo(a);
	    while (val != NULL ) {
	      e = Rewrite(GetExprVAL(val));
	      PutExprVAL(val,e);
	      val = Next_list(val);
	    }
	  }
	  b = NULL;
	  break;

	case LetC:
	  a = LookA(b,VALA);
	  val = (VarAssignListTyp)LookAInfo(a);
	  while (val != NULL ) {
	    e = Rewrite(GetExprVAL(val));
	    PutExprVAL(val,e);
	    val = Next_list(val);
	  }
	  b = LookArgB(b,1);
	  break;

	case DisablingC:
	case ParallelC:
	case EnablingC:
	  Rw1Beh(LookArgB(b,1));
	  b =  LookArgB(b,2);
	  break;

	case AlternativeC:
	  i = NumArgB(b);
	  while (i>1) {
	    Rw1Beh(LookArgB(b,i));
	    i --;
	  }
	  b = LookArgB(b,1);
	  break;

	case InterleavedC:
	  Rw1Beh( LookArgB( b, 1 ) );
	  itcl= (ITContListTyp)LookAInfo(LookA(b,ITCLA));
	  if ( itcl!=NULL ){
	    for (  ; itcl!=NULL; itcl=Next_list(itcl) ){
	      pit = (PITContTyp) LookInfo_list(itcl);
	      Rw1Beh(pit->b);
	    }
	  }
	  b = LookArgB( b, 2 );
	  break;

	default :
	  Error("RwBeh: unexpected cell.");
	}
  }
}

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

/* RwBeh
 * Rewrite the expressions in behaviours and in the processes.
 */
static void RwBeh()
{
  int    i;
  BehTyp b;
  char   buff[1024];

  for ( i=1; i<=LastTableP(); i++ ) {
    b = GetP_def(i);
    if (runtimeConfig==TextMode) {
      (void)sprintf(buff,"\015 %5d = %-69s",i,GetP_name(i));
      printMsgs(buff);
    }
    else {
      (void)sprintf(buff," %5d = %-69s",i,GetP_name(i));
      printPos(buff,-2);
      flushTarget();
    }
    Rw1Beh(b);
  }
  if (runtimeConfig==TextMode)
    (void)printf("\015");
  else {
    printPos("",-2);
    flushTarget();
  }
}


/******************************************************************
 *                                                                *
 *    Rewrite of expressions in the specification.                *
 *    ( rules and behaviours)                                     *
 *                                                                *
 *******************************************************************/

/* Rw_Spec
 * Rewrite all the data value expression in the current specification.
 * This function must be called before any behaviour processing can be done.
 * Rw_Spec calls Rw_Rules() if it is neccesary.
 */
void Rw_Spec()
{
  char buff[1024];

  if (!flag_Rules)
    Rw_Rules();
  if (!flag_Beh) {
    printMsgs(" Rewriting expressions in the specification.\n");
    RwBeh();
    if (runtimeConfig==TextMode) {
      (void)sprintf(buff,"\015 %-78s\n","Rewriting done.");
      printMsgs(buff);
    }
    else {
      (void)sprintf(buff," %-78s\n","Rewriting done.");
      printPos(buff,-2);
      flushTarget();
    }
    flag_Beh = TRUE;
  }
}

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


