/***********************************
  (C) Copyright 1992-1993; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************/

/***********************************
  
  David Larrabeiti Lopez
  
  20-02-91
  
  Relabel_Expand
  
  Processing of the Relabel operator relab.
  
  relab = relab rfl in b
  
  where b is any behaviour.
  
  ************************************/

#include "limisc.h"
#include "badefca.h"
#include "balotosf.h"
#include "baattr.h"
#include "exsucces.h"
#include "expre_br.h"


static BehTyp R_E( b, rfla, i_rm_depth )
     BehTyp b;
     PAttrTyp rfla;
     int *i_rm_depth;
{
  int NumArg,i;
  DescriptorTyp name;
  BehTyp bi,out,rf,relab,relab2;
  RelabFuncListTyp rfl2;
  PAttrTyp rfla2;
  
  switch( LookTypeB(b) )
    { case GateC:
	name = ActualRFL( (RelabFuncListTyp)LookAInfo(rfla), LookNameB(b) );
	if ( name!=(DescriptorTyp)NULL )
	  PutNameB( b, name );
	
	if ( LookTypeB(LookArgB(b,1))==HidingC ) {
	  rfl2 = CopyRFL((RelabFuncListTyp)LookAInfo( rfla ));
	  rfl2 = SimplifyRFL( rfl2,
			     (GateSetTyp)LookAInfo(LookA(LookArgB(b,1),GSA)) );
	  if ( rfl2==NULL ) {
	    out = b;
	    break;
	  }
	  else
	    FreeRFL( rfl2 );  /**/ /* temporary. could be passed to R_E */
	}
	
	rf = MakeB( 0, RelabellingC );
	PutA( rf, rfla );                                 /* shared attr */
	bi = GetArgB( b, 1 );
	PutArgB( b, rf, 1 );
	PutArgB( rf, bi, 1 );
	out = b;
	break;
	
      case RelabellingC:
	UnshareA( b, RFLA );
	rfla2 = LookA( b, RFLA );
	rfl2  = (RelabFuncListTyp)GetAInfo( rfla2 );
	rfl2  = JunctionRFL(CopyRFL((RelabFuncListTyp)LookAInfo(rfla)),rfl2);
	if ( rfl2==NULL ){
	  out = GetArgB(b,1);
	  FreeB(b);
	}
	else {
	  PutAInfo( rfla2, (AttrValueTyp)rfl2 );
	  out = Relabel_Expand( b, i_rm_depth );
	}
	break;
	
      case AlternativeC:
	NumArg=NumArgB( b );
	for ( i=1; i<=NumArg; i++ ) {
	  bi = GetArgB( b, i );
	  PutArgB( b, R_E(bi,rfla,i_rm_depth), i );
	}
	out = b;
	break;
	
      case GuardC:
	bi = GetArgB( b, 1 );
	PutArgB( b, R_E(bi,rfla,i_rm_depth), 1 );
	out = b;
	break;
	
      case ChoiceC:
	bi = GetArgB( b, 1 );
	PutArgB( b, R_E(bi,rfla,i_rm_depth), 1 );
	out = b;
	break;
	
      case ExitC:
      case StopC:
      case TerminationC:
      case InterleavedC:                                /* temporary */
	out = b;
	break;
	
      case IC:
	if ( LookTypeB(LookArgB(b,1))==HidingC ) {
	  rfl2 = CopyRFL((RelabFuncListTyp)LookAInfo( rfla ));
	  rfl2 = SimplifyRFL( rfl2,
			     (GateSetTyp)LookAInfo(LookA(LookArgB(b,1),GSA)) );
	  if ( rfl2==NULL ) {
	    out = b;
	    break;
	  }
	  else
	    FreeRFL( rfl2 );  /**/ /* temporary. could be passed to R_E */
	}
	rf = MakeB( 0, RelabellingC );
	PutA( rf, rfla );
	bi= GetArgB( b, 1 );
	PutArgB( b, rf, 1 );
	PutArgB( rf, bi, 1 );
	out = b;
	break;
	
      case DisablingC:
      case EnablingC:        /* rfl in B1>>B2 = (rfl in B1)>>(rfl in B2) */
	b     = GetOperB(b);
	relab = MakeB( 0, RelabellingC );
	PutA( relab, rfla );
	relab2 = CopyB( relab );
	bi = GetArgB( b, 1 );
	PutArgB( b, relab, 1 );
	AddArgB( relab, bi );
	bi = GetArgB( b, 2 );
	PutArgB( b, relab2, 2 );
	AddArgB( relab2, bi );
	if (IS_SHARED_EXP){
	  Pre_Processing_2( b, i_rm_depth );
	  out = b;
	}
	else
	  out = Pre_Processing( b, i_rm_depth );
	break;
	
      case HidingC:
      case LetC:
      case PletC:
      case ParallelC:
	if (IS_SHARED_EXP){
	  Pre_Processing_2( b, i_rm_depth );
	  out = R_E( b, rfla, i_rm_depth );
	}
	else {
	  if (IS_TEST_EQUIV_EXP) {
	    RelabUpdateSuccessStack((RelabFuncListTyp)LookAInfo( rfla ));
	    out = R_E( Pre_Processing( b, i_rm_depth ), rfla, i_rm_depth );
            PopSuccessStack();
	  }
	  else
	    out = R_E( Pre_Processing( b, i_rm_depth ), rfla, i_rm_depth );
	}
	break;
	
      default:
	if (IS_SHARED_EXP){
	  Pre_Processing_2( b, i_rm_depth );
	  out = R_E( b, rfla, i_rm_depth );
	}
	else
	  out = R_E( Pre_Processing( b, i_rm_depth ), rfla, i_rm_depth );
	break;
      }
  
  return out;
}


/* Relabel_Expand
 * Processing of the Relabel operator relab.
 *
 *     relab = relab rfl in b
 *
 * where b is any behaviour.
 */
BehTyp Relabel_Expand( relab, i_rm_depth )
     BehTyp relab;
     int *i_rm_depth;
{
  BehTyp   b, out;
  PAttrTyp rfla;
  
  LASSERT ( LookTypeB(relab)==RelabellingC );
  
  rfla = LookA( relab, RFLA );
  b    = GetArgB( relab, 1 );
  out  = R_E( b, rfla, i_rm_depth );
  LASSERT(LookCopy(relab)==0);
  FreeB( relab );
  
  return out;
}

