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

/***********************************
  
  David Larrabeiti Lopez
  
  2-07-92
  
  Let_Processing.
  
  Processing of the Let operator let.
  
  let = Let v1:s1=E1,...,vn:sn=En in b
  
  where b is any behaviour.
  
  July 14, 1992
  The operator let is moved down after the actions when it is expanded.
  Push the let operator only into those arguments of operators with arity
  greater than 1, in which the variables of the val are used.

  April 19, 1994  Gualberto Rabay
  Added code to manage time attributes in ProcLet_gate
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  (none)
  
  ************************************/

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


static BehTyp LetProc();

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

/* ProcLet_guard
 */
static BehTyp ProcLet_guard ( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  char r;
  PAttrTyp attr;
  PredicateTyp pred;
  
  if ( Var_in_Pred_SV((PredicateTyp)LookAInfo(LookA(b,PA)),sv) ) {
    UnshareA( b, PA );
    attr = LookA( b, PA );
    pred = (PredicateTyp)GetAInfo(attr);
    (void)SubstPredSV( &pred, sv );
    PutAInfo( attr, (AttrValueTyp)pred );
  }
  r = LookPredicate( b );
  SolvePredicateBeh( b );
  if (r == 'f')
    return b;
  else
    if (r == 't')
      return LetProc( b, vala, sv );
    else {
      PutArgB( b, LetProc( GetArgB( b,1 ), vala, sv ), 1 );
      return b;
    }
}

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

/* ProcLet_par
 */
static BehTyp ProcLet_par( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
     
{
  if ( IsUsedInBehSV( sv, LookArgB(b,1) ) ) 
    PutArgB( b, LetProc( GetArgB(b,1), vala, sv ), 1 );
  if ( IsUsedInBehSV( sv, LookArgB(b,2) ) ) 
    PutArgB( b, LetProc( GetArgB(b,2), vala, sv ), 2 );
  return b;
}

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

/* ProcLet_ena
 */
static BehTyp ProcLet_ena( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
     
{ 
  if ( IsUsedInBehSV( sv, LookArgB(b,1) ) )
    PutArgB( b, LetProc( GetArgB(b,1), vala, sv ), 1 );
  
  if ( IsUsedInBehSV( sv, LookArgB(b,2) ) ) 
    PutArgB( b, LetProc( GetArgB(b,2), vala, sv ), 2 );
  
  return b;
}

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

/* ProcLet_dis
 */
static BehTyp ProcLet_dis( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
     
{
  if ( IsUsedInBehSV( sv, LookArgB(b,1) ) ) 
    PutArgB( b, LetProc( GetArgB(b,1), vala, sv ), 1 );
  if ( IsUsedInBehSV( sv, LookArgB(b,2) ) ) 
    PutArgB( b, LetProc( GetArgB(b,2), vala, sv ), 2 );
  return b;
}

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

/* ProcLet_alt
 */
static BehTyp ProcLet_alt(b,vala,sv)
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  int n,i;
  
  n = NumArgB(b);
  for ( i=1; i<=n; i++ )
    if ( IsUsedInBehSV( sv, LookArgB(b,i) ) ) 
      PutArgB( b, LetProc( GetArgB( b, i ), vala, sv ), i );
  return b;
}

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

/* ProcLet_i
 */
static BehTyp ProcLet_i( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  BehTyp let, b1;
#ifdef TIME 
  PTimeTyp time;
  PAttrTyp a;
#endif 

  
  b1  = GetArgB( b, 1 );
  let = MakeB( 0, LetC );
  PutA( let, vala );
  PutArgB( let, b1, 1 );
  PutArgB( b, let, 1 );

#ifdef TIME

  if ( Var_in_TA_SV((PTimeTyp)LookAInfo(LookA(b,TA)),sv) ) {
   UnshareA( b, TA );
   a  = LookA( b, TA );
   time = (PTimeTyp)GetAInfo( a );
   Subst_TA_SV( time, sv ); 
   if (LookNameE(time->upper_bound)==FindO_time("neg")) {
       TrfStop(b);
    return b;  
  } 
   if (LookNameE(time->lower_bound)==FindO_time("neg")) 
     ChangeNameE(time->lower_bound,FindO_time("0")); 
   PutAInfo( a, (AttrValueTyp)time );
 }
#else
  sv = sv; /* lint please shut up ! */
#endif


  return b;
}

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

/* ProcLet_hid
 */
static BehTyp ProcLet_hid( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  PutArgB( b, LetProc( GetArgB( b,1 ), vala, sv ), 1 );
  return b;
}

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

/* ProcLet_rel
 */
static BehTyp ProcLet_rel( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  PutArgB( b, LetProc( GetArgB( b,1 ), vala, sv ), 1 );
  return b;
}

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

/* ProcLet_parc
 */
static BehTyp ProcLet_parc( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  PutArgB( b, LetProc( GetArgB( b,1 ), vala, sv ), 1 );
  return b;
}

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

/* ProcLet_choice
 */
static BehTyp ProcLet_choice ( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  PutArgB( b, LetProc( GetArgB( b,1 ), vala, sv ), 1 );
  return b;
}

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

/* ProcLet_stop
 */
static BehTyp ProcLet_stop( b )
     BehTyp b;
{  
  return b;
}

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

/* ProcLet_term
 * Only possible when expanding something iexpanded.
 */
static BehTyp ProcLet_term( b, sv )
     BehTyp b;
     SVdescriptorTyp *sv;
{  
  PAttrTyp ela;
  ExprListTyp el;
  
  if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),sv) ) {
    UnshareA(b,ELA);
    ela = LookA(b,ELA);
    el  = (ExprListTyp)GetAInfo(ela);
    Subst_EL_SV( el, sv );
    PutAInfo( ela, (AttrValueTyp)el );
  }
  return b;
}

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

/* ProcLet_exit
 */
static BehTyp ProcLet_exit ( b,sv )
     BehTyp           b;
     SVdescriptorTyp *sv;
{
  PAttrTyp ola;
  OfferListTyp ol;
  
  if ( Var_in_OL_SV( (OfferListTyp)LookAInfo(LookA(b,OLA)), sv ) ) {
    UnshareA(b,OLA);
    ola = LookA(b,OLA);
    ol  = (OfferListTyp)GetAInfo(ola);
    Subst_OL_SV( ol, sv );
    PutAInfo( ola, (AttrValueTyp)ol );
  }
  return b;
}

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


/* ProcLet_gate
 */
static BehTyp ProcLet_gate ( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  BehTyp let, b1;
  PredicateTyp  p;
  PAttrTyp a;
  char     r;
  OfferListTyp ol;

#ifdef TIME 
  PTimeTyp   time;
  BehTyp     let2;
  PAttrTyp   vala2; 

  DescriptorTyp tvar;
  ExprTyp etvar;
  PAttrTyp         nvala;
  VarAssignListTyp nval; 
  SVdescriptorTyp  sv2;
  BehTyp     res ;
#endif 

  
  if ( Var_in_OL_SV((OfferListTyp)LookAInfo(LookA(b,OLA)),sv) )
    { UnshareA( b, OLA );
      a  = GetA( b, OLA );
      ol = (OfferListTyp)GetAInfo( a );
      Subst_OL_SV( ol, sv );
      PutAInfo( a, (AttrValueTyp)ol );
      PutA( b, a );
    }
  
#ifdef TIME
  time= (PTimeTyp)LookAInfo(LookA(b,TA));
  if ( Var_in_TA_SV((PTimeTyp)LookAInfo(LookA(b,TA)),sv) ) {
    UnshareA( b, TA );
    a  = GetA( b, TA );
    time = (PTimeTyp)GetAInfo( a );
    Subst_TA_SV( time, sv ); 
    if (LookNameE(time->upper_bound)==FindO_time("neg")) {
          TrfStop(b);
      return b;  
    } 
   if (LookNameE(time->lower_bound)==FindO_time("neg")) 
     ChangeNameE(time->lower_bound,FindO_time("0")); 
   PutAInfo( a, (AttrValueTyp)time );
   PutA( b, a );
   
    }
#endif

  p = (PredicateTyp)LookAInfo(LookA(b,PA));
  if ( p!=NULL )
    if ( Var_in_Pred_SV( p, sv ) )
      { UnshareA( b, PA );
        a = GetA( b, PA );
        p = (PredicateTyp)GetAInfo( a );
        (void)SubstPredSV( &p, sv );
        PutAInfo( a, (AttrValueTyp)p );
        PutA( b, a );
      }
  r = LookPredicate( b );
  SolvePredicateBeh( b );
  if ( r=='f' )
    return b;                /* stop */
  else {
   
    b1  = GetArgB( b, 1 );
    let = MakeB( 0, LetC );
    PutA( let, vala );  
#ifdef TIME    
   vala2 = NULL; 
   etvar = NULL; 
    if  ((time->tvar!=NULL) && !IsConstE(time->tvar) ) {
      tvar =FindV("time", FindS("time"));
      tvar = EqualV_entry(tvar);
      etvar =  MakeE(tvar,VariableC);
      vala2 =  AgeLet (  etvar ,time, vala  ); 
    } 

    if  (vala2 != NULL)   {
      nval = CreateVAL();

      nval =  AddVAL(nval,LookNameE(time->tvar),etvar ); 
      sv2   = CreateSV();
      Insert_VAL_SV( nval, &sv2 );
      if ( IsUsedInBehSV( &sv2, b1 ) ) { 
	nvala =MakeA ((AttrValueTyp) nval,VALA); 
	res = TLetProc( b1, nvala, &sv2 );
	let2 = MakeB(0,LetC);
	PutA(let2,vala2); 
	PutArgB( let2, res, 1 );
	  
	PutArgB( let,let2, 1 );
      } 
      else { 
	PutArgB( let, b1, 1 );
	FreeE(etvar);
	FreeVAL(nval);
      }
      FreeSV( &sv2 );
      
    }
    else {
      PutArgB( let, b1, 1 );
      if (etvar!=NULL) FreeE(etvar);
    }
#else 
    PutArgB( let, b1, 1 );
#endif
    PutArgB( b, let, 1 );
    return b;
  }
}

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

/* ProcLet_proc
 */
static BehTyp ProcLet_proc( b,sv )
     BehTyp           b;
     SVdescriptorTyp *sv;
{
  PAttrTyp ela;
  ExprListTyp el;
  
  if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),sv) ) {
    UnshareA(b,ELA);
    ela = LookA(b,ELA);
    el  = (ExprListTyp)GetAInfo(ela);
    Subst_EL_SV( el, sv );
    PutAInfo( ela, (AttrValueTyp)el );
  }
  return b;
}

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

/* ProcLet_plet
 */
static BehTyp ProcLet_plet( b, sv )
     BehTyp           b;
     SVdescriptorTyp *sv;
{
  VarAssignListTyp val2;
  PAttrTyp attr;
  
  val2 = (VarAssignListTyp)LookAInfo(LookA(b,VALA));
  if ( val2==NULL ) 
    return b;
  else {
    if ( Var_in_VAL_RightSide_SV(val2,sv) ) {
      UnshareA( b, VALA );      
      attr = LookA( b, VALA );
      val2 = (VarAssignListTyp)GetAInfo( attr );
      Subst_VAL_RightSide_SV( val2, sv );
      PutAInfo( attr, (AttrValueTyp)val2 );
    }
    return b;
  }
}

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

/* ProcLet_let
 */
static BehTyp ProcLet_let( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  VarAssignListTyp val,val2;
  PAttrTyp         vala2;
  SVdescriptorTyp  sv2;
  BehTyp           b1,res;
  
  b1   = GetArgB(b,1);
  val = (VarAssignListTyp)LookAInfo(vala);
  UnshareA( b, VALA );      
  vala2 = LookA( b, VALA );
  val2 = (VarAssignListTyp)GetAInfo(vala2);
  LASSERT(val2!=NULL); 
  if ( Var_in_VAL_BothSides_SV( val2, sv ) )
    Subst_VAL_BothSides_SV( val2, sv );
  val2 = Join_list( val2, CopyVAL(val) );
  PutAInfo( vala2, (AttrValueTyp)val2 );
   sv2 = CreateSV();
  Insert_VAL_SV( val2, &sv2 );
  res =  LetProc( b1 , vala2 , &sv2 );
  FreeSV( &sv2 );
  FreeB(b);
  return res;
}

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

/* ProcLet_it
 * notice that the let advances more than one action.
 */
static BehTyp ProcLet_it( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  PutArgB( b, LetProc( GetArgB( b, 1 ), vala, sv ), 1 );
  return b;
}

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

/* LetProc
 * Adds a let(vala) after the first actions of the behaviour b.
 * If a variable definition is found then a new vala is created adding
 * the redefinition of the variable.
 * sv is the replacement table of vala.
 * Warning: val can not be NULL 
 */
static BehTyp LetProc( b, vala, sv )
     BehTyp           b;
     PAttrTyp         vala;
     SVdescriptorTyp *sv;
{
  BehTyp res;
  
  res = b;
  switch ( LookTypeB(b) )
    { case IC:
	res = ProcLet_i( b, vala, sv );
	break;
      case ChoiceC:
	res = ProcLet_choice( b, vala, sv );
	break;
      case ContSetC:
      case StopC :
	res = ProcLet_stop( b );
	break;
      case ParallelC :
	res = ProcLet_par( b, vala, sv );
	break;
      case AlternativeC :
	res = ProcLet_alt( b, vala, sv );
	break;
      case DisablingC :
	res = ProcLet_dis( b, vala, sv );
	break;
      case LetC :
	res = ProcLet_let( b, vala, sv );
	break;
      case PletC :
	res = ProcLet_plet( b, sv );
	break;
      case GuardC :
	res = ProcLet_guard( b, vala, sv );
	break;
      case GateC :
	res = ProcLet_gate( b, vala, sv );
	break;
      case ExitC : 
	res = ProcLet_exit( b, sv );
	break;
      case ProcessInstC :
	res = ProcLet_proc( b, sv );
	break;
      case TerminationC :
	res = ProcLet_term( b, sv );
	break;
      case HidingC:
	res = ProcLet_hid( b, vala, sv );
	break;
      case EnablingC :
	res = ProcLet_ena( b, vala, sv );
	break;
      case RelabellingC :
	res = ProcLet_rel( b, vala, sv );
	break;
      case ParC:
      case GateChoiceC:
	res = ProcLet_parc( b, vala, sv );
	break;
      case InterleavedC :
	res = ProcLet_it( b, vala, sv );
	break;
	
      default :
	Error("LetProc: Unexpected Cell Type." );
      }
  return res;
}

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

/* Let_Processing
 * Processing of the Let operator let.
 *
 *      let = Let v1:s1=E1,...,vn:sn=En in b
 *
 * where b is any behaviour.
 *
 * This operator is moved after the actions.
 */
BehTyp Let_Processing( let )
     BehTyp let;
{
  BehTyp a,res;
  VarAssignListTyp val;
  PAttrTyp vala;
  SVdescriptorTyp sv;
  
  LASSERT ( LookTypeB( let )==LetC );
  LASSERT ( OwnersB( let )>=0);
  
  a = GetArgB(let,1);
  
  sv   = CreateSV();
  vala = LookA( let, VALA );
  LASSERT( vala!=NULL );
  val  = (VarAssignListTyp) LookAInfo( vala );
  if (val!=NULL)
    Insert_VAL_SV( val, &sv );
  if ( IsUsedInBehSV( &sv, a ) ) 
    res = LetProc( a, vala, &sv );
  else
    res = a;
  FreeB( let );
  FreeSV( &sv );
  return res;
}

