/******************************************************************
 *  (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
 *
 *  28 Dec 1994
 *
 *  Pretty printer for LOTOS behaviours.
 *  Printing follows ISO8807 and supports the IT operator as well.
 *
 *  COMPILATION FLAGS:
 *     ITDEBUG : IT printing debugging
 *
 *  LOG:
 *
 ******************************************************************/

/* LINTLIBRARY */

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "listdh.h"
#include "licell.h"
#include "batables.h"
#include "limisc.h"
#include "baprint.h"
#include "badefca.h"
#include "baattr.h"
#include "babool.h"
#include "listack.h"
#include "lihash.h"
#include "listrbk.h"
#include "libst.h"
#include "batyperw.h"
#include "baexpr.h"


/******************************************************************
 *                                                                *
 *              Buffer string and Functions to manage it          *
 *                                                                *
 ******************************************************************/

static StrBckTyp strbuff = NULL;

/* printstr
 * output function for printing
 */
static void (*printstr)();


     /* AddBuffer
      * Add the string s to the buffer.
      * If printstr is NULL, nothing is added to the buffer.
      */
     static void AddBuffer( s )
     char *s;
{
  if (printstr!=NULL) {
    strbuff = ConcatStrBck(strbuff,s);
  }
}

/******************************************************************
 *                                                                *
 *   Functions to save the cursor movements of each printed line. *
 *                                                                *
 ******************************************************************/

/* calculateMoves
 * TRUE when the pairs <line,movement> must be created during the printing.
 * This variable is set to TRUE when PrintMoves is called,
 * and set to FALSE when it finishes.
 */
static boolean calculateMoves = FALSE;

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

/* printLineNumbers
 * TRUE if PrintMoves must print the lines numbers.
 */
static boolean printLineNumbers = FALSE;

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

/* moveDepthProc
 * printing depth for the used processes.
 */
static int moveDepthProc;

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

/* line_cont
 * the number of the printed line.
 */
static int line_cont;

# define Inc_Line_Cont()  line_cont++

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

/* movementsStack
 * Auxiliary stack to save movements.
 * It is necessary not to use another argument in all the functions.
 */
static StackTyp movementsStack = NULL;

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

/* tableML
 * Hash table to save pairs: <line, movement>.
 */
#define MAX_MOVLIN_TAB 128

typedef struct { int     line;
		 ListTyp move;
	       } MLElemTyp, *PMLElemTyp;

static HashDTyp tableML = NULL;

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

/* CreateElem_ML
 * Get memory for a new element.
 */
static PMLElemTyp CreateElem_ML()
{
  return (PMLElemTyp)Emalloc2Words();
}

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

/* FreeElem_ML
 * Deallocate the memory of the element pe.
 */
static void FreeElem_ML( pe )
     PMLElemTyp pe;
{
  Disp_list(pe->move);
  Free2Words((void*)pe);
}

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

/* KeyElem_ML
 * Calculate the key of the element pe.
 */
static int KeyElem_ML(pe)
     PMLElemTyp pe;
{
  return pe->line;
}

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

/* CompElem_ML
 * Compare the elements pe1 and pe2.
 */
static boolean CompElem_ML(pe1,pe2)
     PMLElemTyp pe1, pe2;
{
  return pe1->line == pe2->line;
}

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

/* PrintElem_ML
 * Print the element pe.
 * pstr is the function used to print strings.
 */
static void PrintElem_ML( pstr, pe )
     void       (*pstr)();
     PMLElemTyp   pe;
{
  ListTyp l;

  pstr(" < "); PrintInt(pstr,pe->line); pstr(" , ");
  for ( l=pe->move ; l!=NULL ; l=Next_list(l) ) {
    PrintInt(pstr,(int)LookInfo_list(l));
    pstr(" ");
  }
  pstr("> ");
}

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

/* Init_ML
 * Init ML hash table
 */
static void Init_ML()
{
  tableML = Create_HT(MAX_MOVLIN_TAB, FreeElem_ML, KeyElem_ML,
		      CompElem_ML, PrintElem_ML);
}

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

/* Add_ML
 * Insert the pair <line, movement> in the hash table.
 */
static void  Add_ML( l , m )
     int     l;
     ListTyp m;
{
  PMLElemTyp pe;

  pe = CreateElem_ML();
  pe->line = l;
  pe->move = m;

  LASSERT(In_HT(tableML,(DataHashTyp)pe)==FALSE);

  Insert_HT(tableML,(DataHashTyp)pe);
}

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

/* Clean_ML
 * Cleans the hash table.
 */
static void Clean_ML()
{
  Clean_HT(tableML);
}

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

static MLElemTyp e_aux;

/* Get_Movement.
 * Returns the movement associated with a line.
 * NULL if it does not exist.
 */
static PMLElemTyp Get_Movement( l )
     int  l;
{
  e_aux.line = l;
  return (PMLElemTyp)LookFor_HT(tableML,(DataHashTyp)(&e_aux));
}

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

/* AddDown
 * Adds "1d" to the movement list m and returns it.
 */
static ListTyp AddDown(m)
     ListTyp m;
{
  int i;

  LASSERT(m!=NULL);
  i = (int)LookInfo_list(m);
  if (i<0)
    return Insert_list((DataListTyp)1,m);
  else if (Length_list(m)>1) {
    PutInfo_list(m,(DataListTyp)(((int)LookInfo_list(m))+1));
    return m;
  }
  else if (i==0)
    return Insert_list((DataListTyp)1,m);
  else {
    PutInfo_list(m,(DataListTyp)(i-1));
    return m;
  }
  /*
     if (m==NULL) {
     return Insert_list((DataListTyp)1,(ListTyp)(NULL));
     }
     else {
     if ((int)LookInfo_list(m)>0) {
     PutInfo_list(m,(DataListTyp)(((int)LookInfo_list(m))+1));
     return m;
     }
     else {
     return Insert_list((DataListTyp)1,m);
     }
     }
     */
}

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

/* AddBranch
 * Adds "<n>b" to the movement list "m" and returns it.
 */
static ListTyp AddBranch(m,n)
     ListTyp m;
     int     n;
{
  return Insert_list((DataListTyp)-n,m);
}

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

/* MoveProc
 * This function is called to indicate that the current behaviour
 * (which is going to be printed now) is the process "d".
 * "d" will be 0 to indicate that the cursor is pointing to the current
 * behaviour).
 * The stack "movementsStack" must be empty when this function is called.
 * It copies "d" in the stack.
 */
static void MoveProc( d )
     DescriptorTyp d;
{
  ListTyp m;

  if (calculateMoves) {
    LASSERT(movementsStack == NULL);
    m = Insert_list((DataListTyp)-d,(ListTyp)NULL);
    movementsStack = Save_Stack( (DataStackTyp)m , movementsStack );
  }
}

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

/* MoveDown
 * This function is called to indicate that the current behaviour
 * (which is going to be printed now) is placed "1d" from its parent.
 * It copies the last entry of the stack "movementsStack" (it is the
 * movement to go to the current place) plus a "1d" movement in the stack.
 */
static void MoveDown()
{
  ListTyp m;

  if (calculateMoves) {
    m = AddDown(Copy_list((ListTyp)Look_Stack(movementsStack),
			  (DataListTyp(*)())NULL));
    movementsStack = Save_Stack( (DataStackTyp)m , movementsStack );
  }
}

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

/* MoveUp
 * This function is called to indicate that the behaviour which is
 * going to be printed now is placed "1u" from the last position (the
 * cursor position).
 * The stack "movementsStack" must be empty.
 */
static void MoveUp()
{
  ListTyp m;

  if (calculateMoves) {
    LASSERT(movementsStack == NULL);
    m = Insert_list((DataListTyp)1,(ListTyp)NULL);
    movementsStack = Save_Stack( (DataStackTyp)m , movementsStack );
  }
}

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

/* MoveBranch
 * This function is called to indicate that the current behaviour
 * (which is going to be printed now) is placed "<n>b" from its parent.
 * It copies the last entry of the stack "movementsStack" (it is the
 * movement to go to the current place) plus a "<n>b"  movement in the stack.
 */
static void MoveBranch(n)
     int n;
{
  ListTyp m;

  if (calculateMoves) {
    m = AddBranch(Copy_list((ListTyp)Look_Stack(movementsStack),
			    (DataListTyp(*)())NULL),n);
    movementsStack = Save_Stack( (DataStackTyp)m , movementsStack );
  }
}

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

/* SaveLineMove
 * Save the last entry of the stack (the position of the line that
 * has been printed now) plus the line number in the hash table.
 */
static void SaveLineMove()
{
  /*
     PMLElemTyp pe;
     char l[100];
     ListTyp lst;
     */

  if (calculateMoves) {
    if (IsEmpty_Stack(movementsStack)) {
      /*
	 AddBuffer("    <");
	 (void)sprintf(l,"%d ",line_cont);
	 AddBuffer(l);
	 AddBuffer(">");
	 */
    }
    else {
      Add_ML( line_cont , Copy_list((ListTyp)Look_Stack(movementsStack),
				    (DataListTyp(*)())NULL));
      /*
	 pe = Get_Movement(line_cont);
	 LASSERT(pe!=NULL);
	 (void)sprintf(l,"     <%d , ",pe->line);
	 AddBuffer(l);
	 for (lst=pe->move ; lst!=NULL ; lst=Next_list(lst)) {
	 (void)sprintf(l,"%d ",(int)LookInfo_list(lst));
	 AddBuffer(l);
	 }
	 AddBuffer(">");
	 */
    }
  }
}

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

/* GetMoveStack
 * Remove the last entry of the "movementsStack".
 */
static void GetMoveStack()
{
  if (calculateMoves) {
    Disp_list((ListTyp)Get_Stack(&movementsStack));
  }
}

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

/* GetMove
 * Return the movement associated to the line l according to
 * the last call to PrintMoves
 *
 * A movement is a list of integers, like 3,-2,1,-5,22,-6.
 *
 * The last value means:
 *    if it is positive: move up the specified value.
 *    if it is zero    : no movement.
 *    if it is negative: go to the specified process definition.
 *
 * The other values mean:
 *     - positive number are down movements.
 *     - negative number are selection of branchs.
 *
 * This example means:
 *             move GetP_name(6) 22d 5b 1d 2b 3d
 *
 * BE CAREFUL: The returned list is not a copy: Do not modify it.
 */
ListTyp GetMove( l )
     int l;
{
  MLElemTyp  e;
  PMLElemTyp pe;

  if (tableML!=NULL) {
    /* looking for the line 1 to see if the table is empty. */
    e.line = 1;
    pe = (PMLElemTyp)LookFor_HT(tableML,(DataHashTyp)(&e));
    if (pe!=NULL) {
      e.line = l;
      pe = (PMLElemTyp)LookFor_HT(tableML,(DataHashTyp)(&e));
      if (pe==NULL) {
	Warning("The especified line has not got behaviour.");
	return NULL;
      }
      else
	return pe->move;
    }
  }
  Warning("There are not associations <line,movement>. Use 'move' first.");
  return NULL;
}

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

/* CleanLinesMovements
 * Cleans the table with the associations <line,movement>.
 * This function must be called when the current behaviour is changed.
 */
void CleanLinesMovements()
{
  if (tableML == NULL)
    Init_ML();
  Clean_ML();
  LASSERT(movementsStack == NULL);
}


/******************************************************************
 *
 * Table of the processes used and the current depth.
 *
 *******************************************************************/

#define PROCLISTINC 256

typedef struct { DescriptorTyp proc ;
		 int depthproc ;
	       } ProcListEntryTyp;

static ProcListEntryTyp * proc_list = NULL;
static int                last_proc_list = -1;
static int                size_proc_list = 0;

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

/* Realloc_proc_list
 * Reallocate more memory for the process list table.
 */
static void Realloc_proc_list()
{
  if (proc_list == NULL)
    proc_list = (ProcListEntryTyp*)ecalloc((unsigned)PROCLISTINC,
					   sizeof(ProcListEntryTyp));
  else
    proc_list = (ProcListEntryTyp*)erealloc((void*)proc_list,
					    (size_proc_list+PROCLISTINC)
					    *sizeof(ProcListEntryTyp));
  size_proc_list += PROCLISTINC;
}

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

#define VPL 4                /* number of variables of equations per line */

/*
 * Flags is TRUE if the types must be printed.
 */
static boolean typeflag;

static StackTyp back_pos_indent = NULL;
static int      pos_indent;
static int      process_id;
static boolean  spec_flag, first_def;
static BehTyp   no_print_proc;
static int      layer;
static int      print_dots;
static int      print_line_num;

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

/* Indentation control.
 *
 * NewLine() prints "indentNL" the first time is invoked,
 * and sets the cursor position to len(indent).
 * "f_indent" is a flag to indicate the first invocation.
 */
static char    *indentNL;
static boolean  f_indent;

/******************************************************************
 *                                                                *
 *                     General functions.                         *
 *                                                                *
 ******************************************************************/

/* NewLine
 * Print a carriage return, the blanks needed to reach current
 * indentation and the buffer.
 * Print also the line number (if XLOLA is not defined).
 * Updates the position cursor to this value.
 */
static void NewLine ()
{
  int  c;
  char l[15];

  if (f_indent) {
    AddBuffer("\n");
    if (calculateMoves) {
      Inc_Line_Cont();
      if (printLineNumbers) {
	(void)sprintf(l,"%-4d ",line_cont);
	AddBuffer(l);
      }
    }
    pos_indent = (int)Look_Stack(back_pos_indent);
    for ( c=1 ; c<=pos_indent ; c++)
      AddBuffer(" ");
  }
  else {
    if (calculateMoves) {
      Inc_Line_Cont();
      if (printLineNumbers) {
	(void)sprintf(l,"%-4d ",line_cont);
	AddBuffer(l);
      }
    }
    f_indent = TRUE;
    AddBuffer(indentNL);
    back_pos_indent = Save_Stack((DataStackTyp)(pos_indent=strlen(indentNL)),
				 back_pos_indent);
  }
  printstr(LookStrStrBck(strbuff));
  CleanStrBck(strbuff);
}

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

/* StartPrintBeh
 * Init the module before printing a behaviour
 */
static void StartPrintBeh (depth, pstr, indent, dots, line_num)
     int     depth ;
     void   (*pstr)();
     char   *indent;
     boolean dots, line_num;
{
  if (calculateMoves) {
    line_cont        = 0;
    CleanLinesMovements();
  }
  if (strbuff==NULL)
    strbuff = CreateStrBck();
  printstr        = pstr;
  print_dots      = dots;
  back_pos_indent = Create_Stack();
  indentNL        = indent;
  f_indent        = FALSE;
  last_proc_list  = -1 ;
  process_id      = 1;
  layer           = depth ;
  no_print_proc   = NULL ;
  spec_flag       = FALSE ;
  first_def       = TRUE ;
  print_line_num  = line_num;
}

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

/* SaveIndentation
 * Stores the current position in the line.
 */
static void SaveIndentation ()
{
  LASSERT(!IsEmpty_Stack(back_pos_indent));
  back_pos_indent = Save_Stack((DataStackTyp)pos_indent,back_pos_indent);
}

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

/* FreeIndentation
 * Removes the last position stored.
 */
static void FreeIndentation ()
{
  LASSERT(!IsEmpty_Stack(back_pos_indent));
  (void)Get_Stack(&back_pos_indent);
}

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

/* CleanIndentation
 * Puts to zero the last position stored.
 */
static void CleanIndentation ()
{
  LASSERT(!IsEmpty_Stack(back_pos_indent));
  (void)Get_Stack(&back_pos_indent);
  back_pos_indent = Save_Stack((DataStackTyp)0,back_pos_indent);
}

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

/* PrintBlank
 * If the line cursor does not overflows the maximum width,
 * a 'space' is printed and its value is updated.
 */
static void PrintBlank ()
{
  AddBuffer(" ");
  pos_indent =  pos_indent + 1 ;
}

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

/* PrintChar
 * Prints one character and updates cursor
 */
static void PrintChar (c)
     char c ;
{
  /*??*/ char tmp[2];
	 pos_indent =  pos_indent + 1 ;
	 (void)sprintf(tmp,"%c",c);
	 AddBuffer(tmp);
       }

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

/* PrintStr
 * Prints the string 'literal'. Update line cursor.
 */
static void PrintStr (literal)
     char * literal ;
{
  int len;

  len = strlen(literal) ;
  pos_indent =  pos_indent + len ;
  AddBuffer(literal);
}

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

/* PrintNumber
 * Prints number 'num'.
 */
static void PrintNumber (num)
     int num ;
{
  char l[15];
  int len;

  (void)sprintf(l,"%d",num);
  len =  strlen(l);
  pos_indent =  pos_indent + len;
  AddBuffer(l);
}

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

/* PutTab
 * Print a tab, update the cursor and store it.
 */
static void PutTab ()
{
  pos_indent += 3;
  AddBuffer("   ");
}


/******************************************************************
 *                                                                *
 *          Printing functions for the data types.                *
 *                                                                *
 ******************************************************************/

/* PrintSorts
 * Print the list of defined sorts.
 */
/* KJT 22/01/23: added "int" type */
static int PrintSorts()
{
  int i, numSorts, mb, sorts_in_line;

  mb       = GetBool();
  numSorts = LastTableS();
  AddBuffer("  ");
  sorts_in_line = 0;
  for ( i=1; i<=numSorts; i++ )
    if ( i!=mb ) {
      AddBuffer(GetS_name(i));
      sorts_in_line++;
      if ( i!=numSorts )
	if (sorts_in_line == 4) {
	  sorts_in_line = 0;
	  AddBuffer(",");
	  NewLine();
	  AddBuffer("    ");
	}
	else
	  AddBuffer(", ");
    }
}

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

/* PrintOpns
 * Print the list of defined operations.
 */
/* KJT 22/01/23: added "int" type */
static int PrintOpns()
{
  int     i, numOpns;
  ListTyp al;

  numOpns = LastTableO();
  for ( i=1; i<=numOpns; i++ ){
    if ( !IsMetaBool(i) ){      /* ignore metabooleans */
      AddBuffer("    ");
      if ( GetO_infix( i ) ){
	AddBuffer("_");
	AddBuffer(GetO_name( i ));
	AddBuffer("_");
      }
      else
	AddBuffer(GetO_name( i ));
      AddBuffer(" : ");
      al = GetO_argl( i );
      AddBuffer(SPrint_list( al,SPrintS ));
      AddBuffer(" -> ");
      AddBuffer(GetS_name(GetO_sort(i)));
      NewLine();
    }
  }
}

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

static ListTyp varList;

/* AppendVarsOfExpr
 * Append to varList the descriptors of the variables contained in
 * an expression e. There are not duplicated elements in varList.
 */
static void AppendVarsOfExpr( e )
     ExprTyp e;
{
  int i,numArg;

  if (IsOperationE(e)) {
    numArg = NumArgE(e);
    for ( i=1; i<=numArg; i++ )
      AppendVarsOfExpr( LookArgE(e,i) );
  }
  else {
    e = LookPVarE(e)==NULL ? e : LookPVarE(e);
    if ( !In_list( (DataListTyp)LookNameE(e), varList, EqInt ) )
      varList=Add_list( (DataListTyp)LookNameE(e), varList );
  }
}

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

/* Mk_patsbus_vl
 * Makes a list of descriptors with the names of the variables contained in
 * the search_patterns (pat_bus) of all the rewrite rules of all the
 * operations in the table.
 */
static ListTyp Mk_patsbus_vl()
{
  RuleCellPt     rulePt;
  RewRuleListTyp rl;
  int            i, numOpns;

  varList = Create_list();
  numOpns = LastTableO();
  for ( i=1; i<=numOpns; i++ )
    if ( !IsMetaBool(i) ){                    /* ignore metabooleans */
      for ( rl=GetO_rwl(i); rl!=NULL; rl=Next_list(rl) ) {
	rulePt= (RuleCellPt)LookInfo_list(rl);
	AppendVarsOfExpr(rulePt->search_pat);
      }
    }
  return varList;
}

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

/* ThereIsEquation
 *  Determine if the sort n has some equation associated.
 */
static boolean ThereIsEquation( n )
     int n;
{
  int     i,numOpns;
  boolean thereis = FALSE;

  numOpns = LastTableO();
  for ( i=1; (i<=numOpns)&&(!thereis); i++ )
    if ( GetO_sort(i) == n )
      thereis = GetO_rwl(i) !=NULL ;
  return thereis;
}

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

/* ThereAreEquations
 * Determine if there is any equation in the global type.
 */
static boolean ThereAreEquations()
{
  int     i,numOpns;
  boolean thereare = FALSE;

  numOpns = LastTableO();
  for ( i=1; (i<=numOpns)&&(!thereare); i++ )
    if ( !IsMetaBool(i) )                       /* ignore metabooleans */
      thereare = GetO_rwl(i) !=NULL ;
  return thereare;
}

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

/* ThereAreOpns
 * Determine if there are operations in the global type.
 */
static boolean ThereAreOpns()
{
  int i;

  for ( i = LastTableO(); (i>0)&&(IsMetaBool(i)); i-- )
    ;
  return i>0;
}

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

/* PrintEqnsOfSort
 *
 */
static void PrintEqnsOfSort( n )
     DescriptorTyp n;
{
  int      i, numOpns;
  ListTyp  rl;
  char    *l;

  SetPrintParamE( PRINT_ONLY_PARAM );
  numOpns = LastTableO();
  for ( i=1; (i<=numOpns); i++ )
    if ( GetO_sort(i) == n ) {
      rl = GetO_rwl(i);
      while ( rl!=NULL ) {
	AddBuffer("   ");
	AddBuffer( l = SPrint_rw( (RuleCellPt)LookInfo_list(rl)) );
	(void)free(l);
	NewLine();
	rl = Next_list( rl );
      }
    }
  SetPrintParamE(PRINT_PARAM);
}

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

/* PrintEqns
 * Print the rewrite rules.
 */
static void PrintEqns()
{
  ListTyp vdl,next,vdlhead;
  int     i,numSorts,mb;
  char   *v;

  vdl     = Mk_patsbus_vl();
  vdlhead = vdl;
  if ( vdlhead!=NULL ) {
    AddBuffer("    forall ");
    for ( i=0, next=Next_list(vdl); next!=NULL;
	 i=(i+1)%VPL, vdl=next, next=Next_list(next) ) {
      if ( i==0 ) {
	NewLine();
	AddBuffer("      ");
      }
      v = SPrintV( (DescriptorTyp)LookInfo_list(vdl), TRUE );
      AddBuffer(v);
      (void)free(v);
      AddBuffer(", ");
    }
    v = SPrintV( (DescriptorTyp)LookInfo_list(vdl), TRUE );
    AddBuffer(v);
    (void)free(v);
    Disp_list(vdlhead);
    NewLine();
    NewLine();
  }

  mb       = GetBool();
  numSorts = LastTableS();
  for ( i=1; i<=numSorts; i++ ){
    if ( i!=mb )                    /* ignore metabooleans */
      if ( ThereIsEquation(i) )
	{
	  AddBuffer("    ofsort " );
	  AddBuffer(GetS_name(i));
	  NewLine();
	  PrintEqnsOfSort( i );
	  NewLine();
	}
  }
}

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

/* PrintType
 * print the internal ( flattened & single ) type of a specification
 * in a file fd
 */
static void PrintType()
{
  if ( LastTableS() > 1 ){
    NewLine();
    AddBuffer("type ");
    AddBuffer(GetP_name(1));
    AddBuffer(" is");
    NewLine();
    NewLine();
    AddBuffer("  sorts");
    NewLine();
    AddBuffer("  ");
    PrintSorts();
    NewLine();
    NewLine();
    if (ThereAreOpns()) {
      AddBuffer("  opns");
      NewLine();
      PrintOpns();
      NewLine();
    }
    if (ThereAreEquations()) {
      AddBuffer("  eqns");
      NewLine();
      PrintEqns();
    }
    AddBuffer("endtype");
    NewLine();
  }
}

/******************************************************************
 *                                                                *
 *              Printing functions for the behaviour.             *
 *                                                                *
 ******************************************************************/

/*
 *  These operations work on the global variables :
 *    -- layer             ( level control )
 *
 */


/* GetLayer
 * Get the current layer.
 */
static int GetLayer ()
{
  return layer;
}

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

/* SaveLayer
 * Put the current layer to new.
 */
static void SaveLayer (new)
     int new ;
{
  layer = new;
}

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

/* UpdateLayer
 * Update the current layer, unless it is blocked or it is negative.
 */
static void UpdateLayer ()
{
  if( layer > 0 )
    layer =  layer - 1;
}

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


/*
 *    PRIORITIES -> Parenthesis
 *
 *     1 -> let, plet, value choice, par, hide.
 *     2 -> enabling
 *     3 -> disabling
 *     4 -> parallel
 *     5 -> choice expression
 *     6 -> guard
 *     7 -> action prefix
 *     8 -> stop, exit, process inst, (behaviour), interleaved(IT), termination
 *
 */

/* Get_prio
 * Returns the priority of a lotos operator.
 * If tf is TRUE then it must be considered that the gate can have a
 * selection predicate with M-AND operators.
 */
static int Get_prio( b, tf )
     BehTyp  b;
     boolean tf;
{
  PredicateTyp p;

  LASSERT(b!=NULL);
  switch (LookTypeB(b))
    { case LetC:
      case PletC:
      case ChoiceC:
      case HidingC:
	return 1;
      case EnablingC :
	return 2;
      case DisablingC :
	return 3;
      case ParallelC :
	return 4;
      case AlternativeC :
	return 5;
      case GuardC :
	return 6;
      case GateC :
	if (tf) {
	  p = (PredicateTyp)LookAInfo(LookA(b,PA));
	  if ((p!=NULL) && (Next_list(p)!=NULL))
	    return 1;
	  else
	    return 7;
	}
	else
	  return 7;
      case IC :
	return 7;
      case StopC :
      case ExitC :
      case ProcessInstC:
	/*
	 *  case RelabellingC:
	 *   is printed as GateChoiceC => prio = 0
	 *
	 */
      case TerminationC:
      case InterleavedC:
	return 8;
      default :
	return 0;
      }
}

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

/* jump_plet
 * jump over the unassigned PletC cells.
 */
static BehTyp jump_plet ( p )
     BehTyp p;
{
  boolean c;

  c = TRUE;
  while ( c && p )
    if ( LookTypeB(p)==PletC &&
	IsNotPrintableVAL((VarAssignListTyp)LookAInfo(LookA(p,VALA))) )
      p = LookB1(p);
    else
      c = FALSE;
  return p;
}



/******************************************************************
 *                                                                *
 *               Printing Control Operations                      *
 *                                                                *
 ******************************************************************/


/* SaveProcList
 * Save a process definition in proc_list.
 */
static void SaveProcList ( proc, depth )
     DescriptorTyp proc ;
     int           depth ;
{
  int     i;
  boolean found;

  if (calculateMoves)
    depth = moveDepthProc;

  if (GetP_def(proc) != no_print_proc ) {
    found = FALSE;
    for ( i=0 ; (i<=last_proc_list) && !found ; i++ )
      found = proc_list[i].proc == proc;

    if (! found ) {
      last_proc_list++;
      if (last_proc_list == size_proc_list )
	Realloc_proc_list();
      proc_list[last_proc_list].proc =  proc ;
      proc_list[last_proc_list].depthproc =  depth;
    }
    else
      if (proc_list[i-1].depthproc < depth)
	proc_list[i-1].depthproc = depth;
  }
}

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

/* PrintCell
 * Print the tree pointed by ptr.
 */
static void PrintCell ( /* ptr */ );
/* BehTyp ptr ; */

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

/* PrintFuncionality
 * ptr points to a process definition or spec cell
 */
void PrintFuncionality (ptr)
     BehTyp  ptr;
{
  char *l;

  AddBuffer(l=SPrint_Func( GetP_func( LookNameB(ptr) )));
  (void)free(l);
}

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

/* FormatGateList
 * Print a gate list inside [ ].
 */
static void FormatGateList( gl )
     GateListTyp gl;
{
  char *l;

  if ( gl ) {
    PrintChar('[');
    AddBuffer(l=SPrintGL(gl));
    (void)free(l);
    PrintStr("] ");
  }
}

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

/* FormatRelabList
 * Print a gate relabelling inside squared brackets
 */
static void FormatRelabList( ptr )
     RelabFuncListTyp  ptr;
{
  char *l;

  if ( ptr) {
    PrintChar('[');
    AddBuffer(l=SPrintRFL(ptr));
    (void)free(l);
    AddBuffer("]");
  }
}

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

/* FormatVarList
 * Print a variable list between parenthesis
 */
static void FormatVarList( ptr )
     ExprListTyp  ptr;
{
  char *l;

  if ( ptr) {
    PrintChar('(');
    AddBuffer(l=SPrintVL(ptr));
    pos_indent =  pos_indent + strlen(l) ;
    (void)free(l);
    PrintStr(") ");
  }
}

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

/* FormatExprList
 * Print an expression list between parenthesis
 */
static void FormatExprList( ptr )
     ExprListTyp  ptr;
{
  char *l;

  if ( ptr ) {
    PrintChar('(');
    AddBuffer(l=SPrintEL(ptr));
    (void)free(l);
    AddBuffer(")");
  }
}

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

/* Format_Exitlist
 * Print an exit offer list inside brackets
 */
static void Format_Exitlist (ol)
     OfferListTyp ol ;
{
  char *l;

  if (ol) {
    PrintChar('(');
    AddBuffer(l=SPrintExitOL(ol));
    (void)free(l);
    AddBuffer(")");
  }
}

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

/* PrintEqualExp
 * Print an expression, but if the first operator is "equal.bool"
 * then it is written as "E1=E2".
 */
static void PrintEqualExp(ptr)
     ExprTyp ptr ;
{
  char *l;

  if ( IsEqual(ptr)==TRUE ) {
    AddBuffer(l=ExprToStringE(LookArgE(ptr,1)));
    (void)free(l);
    AddBuffer(" = ");
    AddBuffer(l=ExprToStringE(LookArgE(ptr,2)));
    (void)free(l);
  }
  else {
    AddBuffer(l=ExprToStringE(ptr));
    (void)free(l);
  }
}

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

/* PrintNextCell
 * Print the behaviour of the cell below c.
 * This behaviour is printed with or without parenthesis depending on the
 * priorities of c and the cell below c.
 */
static void PrintNextCell( c )
     BehTyp c;
{
  if (layer!=0) {
    NewLine();
    MoveDown();
    if  (Get_prio(c,FALSE)>Get_prio(jump_plet(LookB1(c)),TRUE)) {
      PrintChar ( '(' );
      SaveIndentation  ();
      PrintCell ( LookB1 ( c ) ) ;
      FreeIndentation  ();
      NewLine();
      PrintChar ( ')' );
    }
    else {
      PrintCell ( LookB1 ( c ) ) ;
    }
    GetMoveStack();
  }
  else {
    if (print_dots) {
      NewLine();
      MoveDown();
      AddBuffer("......");
      SaveLineMove();
      GetMoveStack();
    }
  }
}

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

/* PrintNextArg
 * Print the  behaviour of the argument i of cell c.
 * i must be only 1 or 2.
 * This behaviour is printed with or without parenthesis depending on the
 * priorities of c and its argument.
 */
static void PrintNextArg( c, i )
     BehTyp c;
     int    i;
{
  BehTyp a;

  LASSERT((i==1) || (i==2));
  a = jump_plet(LookArgB(c,i));
  if ( (Get_prio(c,FALSE)>=Get_prio(a,TRUE)+i-1) && (layer!=0) ) {
    PrintStr("  (");
    SaveIndentation();
    PrintCell( a ) ;
    FreeIndentation();
    NewLine();
    PrintStr("  )");
  }
  else {
    PrintBlank();
    PrintBlank();
    SaveIndentation();
    PrintCell( a ) ;
    FreeIndentation();
  }
}


/******************************************************************
 *                                                                *
 *              Print an observable event.                        *
 *                                                                *
 *   If the selection predicate contains M-AND operations then    *
 *   event "a !E1 ?x:s ?y:t [f(x)]; B" is printed as:             *
 *                                                                *
 *     choice x:s []                                              *
 *     [f(x)]->                                                   *
 *     a ! E1 !x ?y:t ;                                           *
 *     B                                                          *
 *                                                                *
 *   otherwise is printed as: "a !E1 ?x:s ?y:t [f(x)]; B"         *
 *                                                                *
 ******************************************************************/


/* PrintOL_mod
 * Print the Offer List ol replacing the offers "?x:s" by "!x" if "x" is
 * in the list "vl" into the file fd.
 */
static void PrintOL_mod( ol, vl )
     OfferListTyp   ol;
     ExprListTyp    vl;
{
  char *l;

  for (  ; ol!=NULL ; ol=ol->next )
    if ((LookKindOffer(ol)==QUESTION) && (!InEL(LookExprOffer(ol),vl))) {
      AddBuffer(" ? ");
      AddBuffer(l=SPrintV(LookNameE(LookExprOffer(ol)),TRUE));
      (void)free(l);
    }
    else {
      AddBuffer(" ! ");
      AddBuffer(l=ExprToStringE(LookExprOffer(ol)));
      (void)free(l);
    }
}

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

/* PrintGateOfferPred
 * Print an observable event.
 */
static void PrintGateOfferPred( e )
     BehTyp e ;
{
  OfferListTyp ol;
  PredicateTyp p;
  ExprListTyp  vinpo;
  int          line;
  char        *l;
  ExprTyp      exp;
#ifdef TIME
  PTimeTyp   t;
#endif

  p  = (PredicateTyp)LookAInfo(LookA(e,PA));
  ol = (OfferListTyp)LookAInfo(LookA(e,OLA));
  if ( p!=NULL ) {
    if ( Next_list(p) != NULL) {
      /*
       *  Composed selection predicates
       */
      vinpo = IntersEL(VarsDefinedInOL(ol),
		       VarsInPred(p));
      if (vinpo!=NULL) {           /* there are variables definitions */
	AddBuffer("choice ");
	AddBuffer(l=SPrintVL(vinpo));
	(void)free(l);
	AddBuffer(" []" );
	SaveLineMove();
	NewLine  ();
      }
      while(p!=NULL) {
	AddBuffer("[");
	if ((exp=LookOrPred(p))!=NULL) {
	  PrintEqualExp(exp);
	  /*
	   *  AddBuffer(" (* ");
	   *  PrintEqualExp(LookRwPred(p));
	   *  AddBuffer(" *) ");
	   */
	}
	else
	  PrintEqualExp(LookRwPred(p));
	AddBuffer("]-> ");
	p = Next_list(p);
	SaveLineMove();
	NewLine  ();
      }
      AddBuffer(GetG_name(LookNameB(e)));
      AddBuffer(" ");
      PrintOL_mod(ol,vinpo);
      FreeEL(vinpo);
      if (print_line_num && (line=(int)LookAInfo(LookA(e,SSLA)))!=(int)NULL ) {
	AddBuffer(l=SPrintSSL(line));
	(void)free(l);
      }
      return;
    }
  }
  /*
   *   There is not a compound selection predicate
   */
  AddBuffer(GetG_name(LookNameB(e)));
  if (ol!=NULL) {
    AddBuffer(" ");
    AddBuffer(l=SPrintOL(ol));
    (void)free(l);
  }
#ifdef TIME
  t = (PTimeTyp)LookAInfo(LookA(e,TA));
  if (t!=NULL){
      AddBuffer(" ");
      l = SPrintT(t);
      AddBuffer( l );
      free(l);
      AddBuffer(" ");
    }
#endif
  if (p!=NULL) {
    AddBuffer(" [");
    if ((exp=LookOrPred(p))!=NULL) {
      PrintEqualExp(exp);
      /*
       *  AddBuffer(" (* ");
       *  PrintEqualExp(LookRwPred(p));
       *  AddBuffer(" *) ");
       */
    }
    else
      PrintEqualExp(LookRwPred(p));
    AddBuffer("]");
  }
  if ( print_line_num && (line = (int)LookAInfo(LookA(e,SSLA))) !=(int)NULL ) {
    AddBuffer(l=SPrintSSL(line));
    (void)free(l);
  }
}

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

/* Print_HideCell
 * Print a hiding.
 */
static void Print_HideCell( ptr )
     BehTyp ptr;
{
  char *l;

  AddBuffer("hide ");
  AddBuffer(l=SPrintGS((GateSetTyp)LookAInfo(LookA(ptr,GSA))));
  (void)free(l);
  AddBuffer(" in" );
  SaveLineMove();
  NewLine();
  MoveDown();
  PrintCell( LookB1(ptr) ) ;
  GetMoveStack();
}

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

/* PrintParOper
 * Print a parallel operator.
 * pstr is the function used to print strings.
 */
void PrintParOper( p, pstr )
     BehTyp   p ;
     void   (*pstr)();
{
  GateSetTyp gs;
  int        partype;
  char      *l;

  partype = LookNameB(p);
  if (partype==INTER_SYNC) {
    pstr("|||");
    LASSERT(LookAInfo(LookA(p,GSA))==NULL);
  }
  else if (partype==FULL_SYNC) {
    pstr("||");
    LASSERT(LookAInfo(LookA(p,GSA))==NULL);
  }
  else {
    LASSERT(partype==PART_SYNC);
    gs = (GateSetTyp) LookAInfo(LookA(p,GSA));
    pstr("|[");
    pstr(l=SPrintGS(gs));
    (void)free(l);
    pstr("]|");
  }
}

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

/* PrintParCell
 * Print an extended parallel ( ParC ).
 */
static void PrintParCell (ptr)
     BehTyp ptr ;
{
  char        *l;

  AddBuffer("par ");
  AddBuffer( l=SPrintGDL((GateDecListTyp)LookAInfo(LookA(ptr,GDLA))) );
  (void)free(l);
  AddBuffer(" ");
  PrintParOper(ptr,AddBuffer);
  SaveLineMove();
  NewLine();
  PutTab();
  SaveIndentation();
  MoveDown();
  PrintCell ( LookB1(ptr) ) ;
  GetMoveStack();
  FreeIndentation();
}

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

/* Print_ParallelCell
 * Print a parallel.
 */
void Print_ParallelCell( ptr )
     BehTyp ptr ;
{
  int level;

  level =  GetLayer  ();
  MoveDown();
  PrintNextArg(ptr,1);
  GetMoveStack();
  NewLine();
  PrintParOper(ptr,AddBuffer);
  SaveLineMove();
  NewLine();
  SaveLayer( level );
  MoveBranch(2);
  PrintNextArg(ptr,2);
  GetMoveStack();
}

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

/* Print_altcell
 * Print a choice expression
 */
void Print_altcell (ptr)
     BehTyp ptr ;
{
  int level, num_alt;

  num_alt = 1;
  level   =  GetLayer  ();
  MoveDown();
  PrintNextArg(ptr,1);
  GetMoveStack();
  ptr = LookB2(ptr);
  while ( ptr!=NULL) {
    SaveLayer(level);
    level =  GetLayer  ();
    NewLine();
    AddBuffer("[]");
    SaveLineMove();
    NewLine();
    MoveBranch(++num_alt);
    PrintNextArg(ptr,1);
    GetMoveStack();
    ptr = LookB2(ptr);
  }
}

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

/* Print_PletCell
 * Print a plet.
 */
static void Print_PletCell( ptr )
     BehTyp ptr ;
{
  char *l;

  AddBuffer("plet ");
  AddBuffer( l=SPrintVAL((VarAssignListTyp)LookAInfo(LookA(ptr,VALA))) );
  (void)free(l);
  AddBuffer(" in");
  SaveLineMove();
  NewLine ();
  MoveDown();
  PrintCell ( LookB1 ( ptr ) ) ;
  GetMoveStack();
}

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

/* Print_LetCell
 * Print a let.
 */
static void Print_LetCell( ptr )
     BehTyp ptr ;
{
  VarAssignListTyp  val;
  char             *l;

  val = (VarAssignListTyp)LookAInfo(LookA(ptr,VALA));
  if ( IsNotPrintableVAL(val) ) {
    MoveDown();
    PrintCell(LookB1(ptr));
    GetMoveStack();
  }
  else {
    AddBuffer("let ");
    AddBuffer( l=SPrintVAL((VarAssignListTyp)LookAInfo(LookA(ptr,VALA))) );
    (void)free(l);
    AddBuffer(" in");
    SaveLineMove();
    NewLine ();
    MoveDown();
    PrintCell ( LookB1 ( ptr ) ) ;
    GetMoveStack();
  }
}

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

/* Print_disablcell
 * Print a disabling.
 */
void Print_disablcell(ptr)
     BehTyp ptr ;
{
  int level;

  level = GetLayer();
  MoveDown();
  PrintNextArg(ptr,1);
  GetMoveStack();
  NewLine();
  AddBuffer("[>");
  SaveLineMove();
  NewLine();
  SaveLayer(level);
  MoveBranch(2);
  PrintNextArg(ptr,2);
  GetMoveStack();
}

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

/* Print_ContSet
 * Prints an interleaved expansion operator ContSet.
 */
static void Print_ContSet( ptr )
     BehTyp ptr ;
{
  int           level, ncont;
  ITContListTyp itcl;
  PITContTyp    itc;
  LabelTyp      n;

  itcl = (ITContListTyp)LookAInfo(LookA(ptr,ITCLA));
  if ( itcl == NULL ){
    PrintChar('{');
    PrintChar('}');
  }
  else {
    SaveIndentation();
    ncont = 3;
    level =  GetLayer  ();
    while (itcl!=NULL) {
#ifdef ITDEBUG
      SaveLayer ( 1 );
#else
      SaveLayer ( level );
#endif
      PrintChar('<');
      itc = (PITContTyp)LookInfo_list(itcl);
      for ( n=itc->label; n!=NULL; n=LookArgB(n,1) ){
	PrintNumber( (int)LookNameB(n) );
	FormatVarList((ExprListTyp)LookAInfo(LookA(n,ELA)));
	if ( LookArgB(n,1)!=NULL )
	  PrintChar(',');
      }
      PrintStr(">");
      NewLine();
      PrintStr("  ");
      SaveIndentation();
      MoveBranch(ncont++);
      PrintCell ( itc->b ) ;
      GetMoveStack();
      FreeIndentation();
      NewLine();
      NewLine();
      itcl = Next_list(itcl);
    }
    FreeIndentation();
    SaveLineMove(); /*?*/
#ifdef ITDEBUG
    SaveLayer ( level );
#endif
  }
}

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

/* Print_InterleavedCell
 * Prints an interleaving operator IT.
 */
static void Print_InterleavedCell(ptr)
     BehTyp ptr ;
{
  int level;

  level =  GetLayer  ();
  PrintStr("IT( " );
  SaveIndentation();
  MoveDown();
  PrintCell ( LookB1 ( ptr ) ) ;
  GetMoveStack();
  NewLine();
  PrintChar ( ',' );
  NewLine();
  SaveLayer ( level );
  /*  MoveBranch(2); */
  PrintCell ( LookB2 ( ptr ) ) ;
  GetMoveStack();
  /* NewLine(); */
  FreeIndentation();
  PrintStr(")");
}

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

/* PrintEnablCell
 * Print an enabling.
 */
static void PrintEnablCell( ptr )
     BehTyp ptr ;
{
  int         level;
  ExprListTyp el;
  char       *l;

  level = GetLayer();

  MoveDown();
  PrintNextArg(ptr,1);
  GetMoveStack();

  el = (ExprListTyp)LookAInfo(LookA(ptr,ELA));
  NewLine  ();
  if ( ! el )
    AddBuffer(">>");
  else {
    AddBuffer(">> accept " );
    AddBuffer(l=SPrintVL(el));
    (void)free(l);
    AddBuffer(" in" );
  }
  SaveLineMove();
  NewLine  ();
  SaveLayer ( level );
  UpdateLayer ();

  MoveBranch(2);
  PrintNextArg(ptr,2);
  GetMoveStack();
}


/******************************************************************
 *                                                                *
 *   Print a guard                                                *
 *                                                                *
 *   If the guard contains M-AND operations then                  *
 *   it is printed as a cascade of guards with single predicates. *
 *                                                                *
 ******************************************************************/


/* PrintGuardCell
 * Print the contruction associated to a cell of type GuardC.
 */
static void PrintGuardCell( ptr )
     BehTyp ptr ;
{
  PredicateTyp p;
  ExprTyp      exp;

  p = (PredicateTyp)LookAInfo(LookA(ptr,PA));
  while ( p != NULL ) {
    AddBuffer("[");
    LASSERT(OwnersE(LookRwPred(p))>0);
    if ((exp=LookOrPred(p)) != NULL) {
      LASSERT(OwnersE(LookOrPred(p))>0);
      PrintEqualExp(exp);
    }
    else
      PrintEqualExp(LookRwPred(p));
    AddBuffer("]-> ");
    SaveLineMove();
    p = Next_list(p);
    if (p!=NULL)
      NewLine();
  }
  PrintNextCell(ptr);
}

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

/* PrPrefixAction
 * Print a;B
 */
static void PrPrefixAction( ptr )
     BehTyp ptr ;
{
  PrintGateOfferPred(ptr);
  AddBuffer(";");
  SaveLineMove();
  UpdateLayer ();
  PrintNextCell(ptr);
}

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

/* behcell
 * Print the structure attached to a BehaviourC in a suitable form
 */
static void print_behcell( ptr )
     BehTyp ptr ;
{
  AddBuffer("(* Behaviour ( ");
  PrintNumber(LookNameB(ptr));
  if ( LookB1(ptr)==NULL ) {
    AddBuffer(") => Vert is nil ; Hor is below *)");
    NewLine  ();
    MoveBranch(2);
    PrintCell(LookB2(ptr));
    GetMoveStack();
  }
  else
    if( LookB2(ptr)==NULL ) {
      AddBuffer(") => Hor is nil ; Vert is below *)");
      NewLine  ();
      MoveDown();
      PrintCell(LookB1(ptr));
      GetMoveStack();
    }
    else {
      AddBuffer(") => Hor is not nil ; Vert is below *)");
      NewLine  ();
      MoveDown();
      PrintCell(LookB1(ptr));
      GetMoveStack();
    }
  NewLine();
}

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

/* PrintSumCell
 * Print choice v1:s1,...,vn:sn [] ...
 * (ChoiceC)
 */
static void PrintSumCell( ptr )
     BehTyp ptr;
{
  char *l;

  AddBuffer("choice ");
  AddBuffer( l = SPrintVL((ExprListTyp)LookAInfo(LookA(ptr,ELA))) );
  (void)free(l);
  AddBuffer(" []" );
  SaveLineMove();
  NewLine  ();

  MoveDown();
  PrintCell ( LookB1(ptr) ) ;
  GetMoveStack();
}

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

/* PrintGateSumCell
 * Print an extended gate choice in a suitable form
 */
static void PrintGateSumCell( ptr )
     BehTyp ptr ;
{
  char *l;

  AddBuffer("choice ");
  AddBuffer(l=SPrintGDL((GateDecListTyp)LookAInfo(LookA(ptr,GDLA))));
  (void)free(l);
  AddBuffer(" []" );
  SaveLineMove();
  NewLine();

  MoveDown();
  PrintCell( LookB1(ptr) ) ;
  GetMoveStack();
}

/******************************************************************
 *                                                                *
 *        Printing of Relabelling as a generalized gatechoice     *
 *                                                                *
 ******************************************************************/

/* PRIVATE */

/* PrintRelabCell
 * Prints a RelabellingC in a suitable form
 */
static void PrintRelabCell (ptr)
     BehTyp ptr ;
{
  BehTyp nptr;

  AddBuffer("(* Relabelling ");
  FormatRelabList( (RelabFuncListTyp)LookAInfo(LookA(ptr,RFLA)) );
  AddBuffer(" in *)");
  SaveLineMove();

  NewLine();

  nptr = MakeB(0,GateChoiceC);
  PutA(nptr,
       MakeA((AttrValueTyp)
	     RFL_to_GDL((RelabFuncListTyp)
			LookAInfo(LookA(ptr,RFLA))),GDLA ) );
  AddArgB( nptr, LookArgB(ptr,1) );
  PrintGateSumCell( nptr );
  FreeB(nptr);
}

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

/* Print_Exit
 * Print exit(v1,...,vn)
 * ( ExitC ) in a suitable format.
 */
static void Print_Exit (ptr)
     BehTyp ptr ;
{
  int line;
  char *l;

  AddBuffer("exit ");
  Format_Exitlist ((OfferListTyp)LookAInfo(LookA(ptr,OLA)));
  if (print_line_num && (line=(int)LookAInfo(LookA(ptr,SSLA)))!=(int)NULL) {
    AddBuffer(l=SPrintSSL(line));
    (void)free(l);
  }
  SaveLineMove();
}

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

/* PrintSpec
 * Print a Specification
 */
static void PrintSpec (ptr)
     BehTyp ptr;
{
  MoveProc(0);
  spec_flag =  TRUE ;
  AddBuffer("specification ");

  AddBuffer(GetP_name(LookNameB(ptr)));
  AddBuffer(" ");
  FormatGateList((GateListTyp)LookAInfo(LookA(ptr,GLA)));
  FormatVarList((ExprListTyp)LookAInfo(LookA(ptr,ELA)));
  AddBuffer(": ");
  PrintFuncionality(ptr);
  SaveLineMove();
  NewLine();
  if (typeflag) {
    PrintType();
  }
  typeflag = FALSE;
  NewLine();
  MoveDown();
  AddBuffer("behaviour");
  SaveLineMove();
  NewLine();
  NewLine();
  PutTab  ();
  SaveIndentation  ();
  PrintCell(LookB1(ptr));
  GetMoveStack();
  GetMoveStack();
  FreeIndentation  ();
}

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

/* PrintInstantiation
 * Print a process instantiation
 */
static void PrintInstantiation( ptr )
     BehTyp ptr ;
{
  int   line;
  char *l;

  AddBuffer(GetP_name(LookNameB(ptr)));
  AddBuffer(" ");
  FormatGateList((GateListTyp)LookAInfo(LookA(ptr,GLA)));
  FormatExprList((ExprListTyp)LookAInfo(LookA(ptr,ELA)));
  if (print_line_num && (line=(int)LookAInfo(LookA(ptr,SSLA)))!=(int)NULL ) {
    AddBuffer(l=SPrintSSL(line));
    (void)free(l);
  }
  SaveLineMove();
}

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

/* PrintHeadProcDef
 * Print the head of a process definition.
 */
static void PrintHeadProcDef( ptr )
     BehTyp ptr ;
{
  first_def =  FALSE;
  MoveProc(LookNameB(ptr));
  AddBuffer("   process " );
  AddBuffer(GetP_name(LookNameB(ptr)));
  AddBuffer(" ");
  FormatGateList((GateListTyp)LookAInfo(LookA(ptr,GLA)));
  FormatVarList((ExprListTyp)LookAInfo(LookA(ptr,ELA)));
  AddBuffer(": ");
  PrintFuncionality(ptr);
  SaveLineMove();
  NewLine();
  GetMoveStack();
}

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

/* PrintProcDef
 * Print a process definition, its body and the endproc indicator
 */
static void PrintProcDef( ptr )
     BehTyp ptr ;
{
  first_def =  FALSE;
  MoveProc(0);
  AddBuffer("process " );
  AddBuffer(GetP_name(LookNameB(ptr)));
  AddBuffer(" ");
  FormatGateList((GateListTyp)LookAInfo(LookA(ptr,GLA)));
  FormatVarList((ExprListTyp)LookAInfo(LookA(ptr,ELA)));
  AddBuffer(": ");
  PrintFuncionality(ptr);
  AddBuffer(" :=" );
  SaveLineMove();
  NewLine();
  MoveDown();
  PutTab();
  SaveIndentation();
  PrintCell( LookB1 ( ptr ) ) ;
  FreeIndentation();
  GetMoveStack();
  NewLine();
  AddBuffer("endproc");
  NewLine();
  GetMoveStack();
}

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

/* PrintProcess
 * Print the definitions specified by proc_list.
 */
static void PrintProcess()
{
  int i;

  if( last_proc_list>-1 ) {
    if( no_print_proc == NULL ) {
      NewLine ();
      AddBuffer("where");
      NewLine ();
    }
    for (i=0 ; i <= last_proc_list ; i++) {
      if ((!calculateMoves) || (moveDepthProc!=0)) {
	NewLine();
	SaveLayer(proc_list[i].depthproc);
	PrintProcDef(GetP_def(proc_list[i].proc));
      }
      else {
	PrintHeadProcDef(GetP_def(proc_list[i].proc));
      }
    }
  }
}

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

/* PrintI
 * Prints the behaviour i;B
 */
static void PrintI( ptr )
     BehTyp ptr ;
{
  int   line;
  char *l;

  AddBuffer("i");
#ifdef TIME
  if (LookA(ptr,TA)!=NULL){
    AddBuffer(" ");
    AddBuffer(
	      l=SPrintT((PTimeTyp)LookAInfo(LookA(ptr,TA))));
    (void)free(l);
  }
#endif
  AddBuffer(";");
  if (LookNameB(ptr)>0) {
    AddBuffer(" (* ");
    AddBuffer(GetG_name(LookNameB(ptr)));
    if ( LookA(ptr,OLA)!=NULL ) {       /* trace information */
      AddBuffer(
		l=SPrintOL((OfferListTyp)LookAInfo(LookA(ptr,OLA))));
      (void)free(l);
    }

    AddBuffer(" *)");
  }
  else if (LookNameB(ptr)<0) {
    AddBuffer(" (* exit");
    if ( LookA(ptr,OLA)!=NULL ){       /* trace information */
      AddBuffer(" (");
      AddBuffer(
		l=SPrintExitOL((OfferListTyp)LookAInfo(LookA(ptr,OLA))));
      (void)free(l);
      AddBuffer(")");
    }
    AddBuffer(" *)");
  }

  if (print_line_num && (line=(int)LookAInfo(LookA(ptr,SSLA)))!=(int)NULL) {
    AddBuffer(l=SPrintSSL(line));
    (void)free(l);
  }
  SaveLineMove();
  UpdateLayer ();
  PrintNextCell(ptr);
}

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

/* Print_TerminationCell
 * Print a termination.
 */
static void Print_TerminationCell(ptr)
     BehTyp ptr ;
{
  int n;

  n = LookNameB(ptr);
  LASSERT(n>0);
  PrintNumber(n);
  FormatExprList((ExprListTyp)LookAInfo(LookA(ptr,ELA)));
  SaveLineMove();
}

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

/* PrintStop
 * Print a stop.
 */
static void PrintStop()
{
  AddBuffer("stop ");
  SaveLineMove();
}

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

/* PrintCell
 * Print the tree pointed by ptr.
 */
static void PrintCell( ptr )
     BehTyp ptr;
{
  if ((ptr!=NULL) && (layer!=0)) {
    switch ( LookTypeB(ptr) )
      { case SpecificationC:
	  PrintSpec( ptr );
	  break;
	case HidingC:
	  Print_HideCell ( ptr );
	  break;
	case ParallelC:
	  Print_ParallelCell ( ptr );
	  break;
	case AlternativeC:
	  Print_altcell ( ptr );
	  break;
	case DisablingC:
	  Print_disablcell ( ptr );
	  break;
	case EnablingC:
	  PrintEnablCell ( ptr );
	  break;
	case LetC:
	  Print_LetCell ( ptr );
	  break;
	case PletC:
	  /* Print_PletCell ( ptr ); */
	  Print_LetCell ( ptr );
	  break;
	case GuardC:
	  PrintGuardCell ( ptr );
	  break;
	case RelabellingC:
	  PrintRelabCell ( ptr );
	  break;
	case ChoiceC:
	  PrintSumCell ( ptr );
	  break;
	case GateChoiceC:
	  PrintGateSumCell ( ptr );
	  break;
	case ParC:
	  PrintParCell ( ptr );
	  break;
	case ExitC:
	  Print_Exit ( ptr );
	  break;
	case StopC:
	  PrintStop ();
	  break;
	case IC:
	  PrintI(ptr);
	  break;
	case GateC:
	  PrPrefixAction ( ptr );
	  break;
	case BehaviourC:
	  print_behcell ( ptr );
	  break;
	case ProcessDefC:
	  no_print_proc =  ptr;
	  PrintProcDef( ptr );
	  break;
	case ProcessInstC:
	  PrintInstantiation ( ptr);
	  SaveProcList(LookNameB(ptr),GetLayer ());
	  break;
	case InterleavedC:
	  Print_InterleavedCell(ptr);
	  break;
	case TerminationC:
	  Print_TerminationCell(ptr);
	  break;
	case ContSetC:
	  Print_ContSet(ptr);
	  break;

	default :
	  Error("PrintCell : Unexpected Cell");
	}
  }
  else
    if ((layer==0) && (ptr!=NULL) && (print_dots)) {
      AddBuffer("......");
      SaveLineMove();
    }
}

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

/* PrintBeh
 * Print the behaviour pointed by ptr.
 * depth     is the printing depth.
 * proc      indicates which processes must be printed.
 * type      indicates if the type definitions must be printed or not.
 * indent    is string to indent the output.
 * pstr      is a function to print strings. The behaviour is transformed
 *           in a set of lines which are printed with this function.
 * dots      indicates if when a behaviour reachs depth must print ".....".
 * line_nums indicates whether the line number of the original specification
 *           must be printed or not.
 */
void PrintBeh ( ptr, depth, proc, type, indent, pstr, dots, line_nums )
     BehTyp  ptr        ;
     int     depth      ;
     int     proc       ;
     boolean type, dots ;
     char    *indent    ;
     void    (*pstr)()  ;
     boolean line_nums  ;
{
  int i;

  StartPrintBeh ( depth, pstr, indent, dots, line_nums );
  typeflag = type;
  NewLine();
  LASSERT(movementsStack == NULL);
  /* Set the first position of the stack to "0" if the initial cell is
     not a process definition or a specification. */
  if (calculateMoves) {
    if ((LookTypeB(ptr)!=ProcessDefC) && (LookTypeB(ptr)!=SpecificationC)) {
      MoveUp();
      AddBuffer("<< MOVE UP >>");
      SaveLineMove();
      NewLine();
      MoveDown();
      PrintCell ( ptr );
      GetMoveStack();
      GetMoveStack();
    }
    else
      PrintCell ( ptr );
  }
  else
    PrintCell ( ptr );
  CleanIndentation();
  NewLine();
  if (proc==ALL_PROC)
    for (i=2 ; i<=LastTableP() ; i++)
      SaveProcList(i,depth);
  if (proc!=NO_PROC)
    PrintProcess  ();
  if (typeflag)
    PrintType();
  if (spec_flag) {
    NewLine  ();
    AddBuffer("endspec");
    CleanIndentation();
    NewLine();
  }
  Free_Stack( back_pos_indent, (void(*)())NULL );
}

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

/* PBeh
 * Prints a behaviour in stdout
 */
void PBeh( b )
     BehTyp b;
{
  PrintBeh(b,-1,NO_PROC,FALSE,"",PrintString,TRUE,FALSE);
}

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

/* PBehN
 * Prints a behaviour down to level n in stdout
 */
void PBehN( b, n )
     BehTyp b;
     int    n;
{
  PrintBeh(b,n,NO_PROC,FALSE,"",PrintString,TRUE,FALSE);
}


/******************************************************************
 *                                                                *
 *  Function to estimate how many lines is going to print         *
 *  function PrintMoves depending on the depth.                   *
 *                                                                *
 ******************************************************************/


/* Stacks to save the behaviour at each level.
 *    currentStack -> with the behaviours in the current depth level.
 *    nextStack    -> with the behaviours to process in the next depth level.
 */
static StackTyp currentStack,nextStack;


/* Processes used and a counter
 */
static BstTyp usedProc;
static int    usedProcCont;


/* LinesInBeh
 * Estimate and return the number of lines needed to print <b> with depth 1.
 * "...." lines are no counted.
 */
static int LinesInBeh( b )
     BehTyp b;
{
  int           i,lines;
  ITContListTyp itcl;
  PITContTyp    itc;

  lines = 0;
  while ( b!=NULL )
    switch ( LookTypeB(b) )
      { case EnablingC:
	case DisablingC:
	case ParallelC:
	  lines += 1 + LinesInBeh( LookArgB(b,2) );
	  b = LookArgB(b,1);
	  break;

	case AlternativeC:
	  for ( i=NumArgB(b); i>1; i-- )
	    lines += 1 + LinesInBeh( LookArgB(b,i) );
	  b = LookArgB(b,1);
	  break;

	case ChoiceC:
	case GuardC:
	case HidingC:
	case PletC:
	case LetC:
	case GateChoiceC:
	case ParC:
	  lines++;
	  b = LookArgB(b,1);
	  break;

	case GateC:
	case IC:
	  lines++;
	  nextStack = Save_Stack( (DataStackTyp)LookArgB(b,1), nextStack );
	  b = NULL;
	  break;

	case ProcessInstC:
	  lines++;
	  if (LookForBST((DataBstTyp)LookNameB(b),
			 usedProc,EchoInt,EqInt)==NULL) {
	    usedProc = InsertBST((DataBstTyp)LookNameB(b),usedProc,EchoInt);
	    usedProcCont++;
	  }
	  b = NULL;
	  break;

	case ExitC:
	case StopC:
	case TerminationC:
	  lines++;
	  b = NULL;
	  break;

	case RelabellingC:
	case ProcessDefC:
	  lines += 2;
	  b = LookArgB(b,1);
	  break;

	case SpecificationC:
	  lines += 6;
	  b = LookArgB(b,1);
	  break;

	case InterleavedC:
	  lines += 2;
	  itcl = (ITContListTyp)LookAInfo(LookA(LookArgB(b,2),ITCLA));
	  while (itcl!=NULL) {
	    itc = (PITContTyp)LookInfo_list(itcl);
	    lines += LinesInBeh( itc->b ) + 2;
	    itcl = Next_list(itcl);
	  }
	  b = LookArgB(b,1);
	  break;

	default: /* BehaviourC */
	  Error("LinesInBeh: Unexpected cell type");
	}
  return lines;
}

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

/* EstimateDepth
 * Computation of depth to be used in function PrintMoves in order to get
 * a number of lines lower than MAXCURSORLINES.
 * The minimum value will be 1 regardless of the value calculated.
 */
static int EstimateDepth( beh )
     BehTyp beh;
{
  BehTyp b;
  int    cont, depth, totallines;
  int    MAXCURSORLINES;

  if (runtimeConfig==TextMode)
    MAXCURSORLINES = 30;
  else
    MAXCURSORLINES = 100;
  currentStack = Create_Stack();
  nextStack    = Create_Stack();
  currentStack = Save_Stack( (DataStackTyp)beh, currentStack );
  usedProc     = CreateBST();
  usedProcCont = totallines = depth = 0 ;
  for (;;) {
    cont = 0;
    while (!IsEmpty_Stack(currentStack)) {
      b = (BehTyp)Get_Stack(&currentStack);
      cont += LinesInBeh( b );
    }
    currentStack = nextStack;
    nextStack = Create_Stack();
    if (totallines+cont+Length_list(currentStack)+usedProcCont
	< MAXCURSORLINES) { /* too much lines */
      depth++;
      totallines += cont;
      if (Length_list(currentStack)==0)  /* maximun depth reached */
	break;
    }
    else
      break;
  }
  /*
     (void)printf("\nnumero de niveles = %d\n",depth);
     (void)printf(  "numero de lineas  = %d\n",totallines);
     (void)printf(  "numero de .....   = %d\n",Length_list(currentStack));
     (void)printf(  "numero de procesos = %d\n",usedProcCont);
     */
  Free_Stack(currentStack,(void(*)())NULL);
  FreeBST(usedProc,(void(*)())NULL);
  return depth==0 ? 1 : depth;
}

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

/* PrintMoves
 * Print the behaviour pointed by ptr and calculates the pairs
 * <line,movement> from the root of ptr.
 * pstr  is a function to print strings. The behaviour is transformed
 *       in a set of lines which are printed with this function.
 * depth is the printing depth. If depth is 0, it is calculated what
 *       depth must be used so as not to exceed the height of the screen.
 * lines is TRUE if the line numbers must be printed.
 */
void PrintMoves( pstr, ptr, depth, lines )
     BehTyp  ptr        ;
     void    (*pstr)()  ;
     int     depth      ;
     boolean lines      ;
{
  LASSERT(calculateMoves == FALSE);
  calculateMoves   = TRUE;
  moveDepthProc    = 0;
  printLineNumbers = lines;
  if (depth==0)
    depth = EstimateDepth(ptr);
  PrintBeh (ptr, depth, USED_PROC, FALSE, "", pstr, TRUE, FALSE);
  printLineNumbers = FALSE;
  calculateMoves   = FALSE;
}

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

/* StatPrint
 * Number of string blocks used by this module
 */
int StatPrint()
{
  return (strbuff==NULL)? 0: 1;
}

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

/* InitPrint
 * Initialize the LOTOS printer module
 */
void InitPrint()
{
  if ( strbuff!=NULL )
    free(GetStrStrBck(strbuff));
  strbuff=NULL;
}

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



