/**************************************************************
 *       offers.c - LBM Interpreter Offer Manipulation
 **************************************************************/
/***********************************************
 (C) Copyright 1993-1994; dit/upm
   Distributed under the conditions stated in the
   TOPO General Public License (see file LICENSE)
 ***********************************************
 $Log: offers.c,v $
 * Revision 1.2  1994/10/17  16:41:12  lotos
 * cosmetics
 *
 * Revision 1.1  1993/10/16  10:51:46  lotos
 * Initial revision
 *
 **********************************************
 $Id: offers.c,v 1.2 1994/10/17 16:41:12 lotos Exp $
 **********************************************/

#include "swbus.h"

PUBLIC exper
cp_exper (e)
  exper e;
{
  exper aux;

  aux = new_exper ();

  aux->type  = e->type;
  aux->sort  = e->sort;
  aux->var   = e->var;
  aux->ldiui = e->ldiui;
  if (e->vrlst != NULL)
    aux->vrlst = INTdup (e->vrlst);
  if (e->val != NULL)
    aux->val = kd_copy (e->val);

  return aux;
}

PUBLIC exper*
cp_exper_array (size, expl)
  int   size;
  exper *expl;
{
  int   i;
  exper *aux;

  assert (size > 0);

  aux = new_exper_array (size);

  for (i = 0; i < size; i++)
    aux[i] = cp_exper (expl[i]);

  return aux;
}

/* It copies only the node.
 * To copy a list, use cp_sset_off
 */
PUBLIC soffert*
cp_soffert (soff)
  soffert *soff;
{
  soffert *aux;

  aux = new_soffert ();

  aux->OffId  = soff->OffId;
  aux->ready  = soff->ready;
  aux->g      = soff->g;
  aux->nexp   = soff->nexp;
  if (aux->nexp > 0)
    aux->expl = cp_exper_array (soff->nexp, soff->expl);
  if (aux->prdl != NULL)
    aux->prdl = CNDcopy (soff->prdl);
  aux->ktl    = INTdup (soff->ktl);
  return aux;
}

PUBLIC soffert*
search_soffert (S, ofid)
  spe    S;
  offert ofid;
{
  soffert *soffs;

  assert (S != NULL);

  for (soffs = S->soffs; soffs != NULL; soffs = soffs->next)
    if (soffs->OffId == ofid)
      return soffs;

  fatal_error ("No such offert", __FILE__, __LINE__);
  return NULL; /* To shut lint off */
}

/* Return those offerts which are ready
 * to be observed (executed)
 */
PUBLIC soffert*
Ready_fun (soffs)
  soffert *soffs;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs; aux != NULL; aux = aux->next)
    if (aux->ready)
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

/* Converts a list of non ready
 * actions in ready actions
 */
PUBLIC soffert*
Become_Ready (soffs)
  soffert *soffs;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs; aux != NULL; aux = aux->next)
    if (!aux->ready) {
      aux->ready = TRUE;
      new = cons_sset_off (cp_soffert (aux), new);
    }
    else
      fatal_error ("Unexpected ready action", __FILE__, __LINE__);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Sd_fun (soffs)
  soffert *soffs;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs; aux != NULL; aux = aux->next)
    if (!aux->ready && (aux->g == LEXITG))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Sg_fun (soffs, gtes)
  soffert *soffs;
  gtelist gtes;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs; aux != NULL; aux = aux->next)
    if (!aux->ready && (INTIsIn (aux->g, gtes)))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Sgd_fun (soffs, gtes)
  soffert *soffs;
  gtelist  gtes;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs; aux != NULL; aux = aux->next)
    if (!aux->ready && INTIsIn (aux->g, gtes) || (aux->g == LEXITG))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Dd_fun (soffs)
  soffert *soffs;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs ; aux != NULL; aux = aux->next)
    if (!aux->ready && (aux->g != LEXITG))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Dg_fun (soffs, gtes)
  soffert *soffs;
  gtelist gtes;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs ; aux != NULL; aux = aux->next)
    if (!aux->ready && !INTIsIn (aux->g, gtes))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Dgd_fun (soffs, gtes)
  soffert *soffs;
  gtelist  gtes;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs ; aux != NULL; aux = aux->next)
    if (!aux->ready && !INTIsIn (aux->g, gtes) && (aux->g != LEXITG))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC soffert*
Rp_fun (oldgtes, newgtes, soffs)
  gtelist oldgtes, newgtes;
  soffert *soffs;
{
  soffert *aux, *new = NULL, *tmp;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs ; aux != NULL; aux = aux->next)
    if (!aux->ready)
      if (INTIsIn (aux->g, oldgtes)) {
	tmp = cp_soffert (aux);
	tmp->g = INTnth (INTpos (tmp->g, oldgtes), newgtes);
	new = cons_sset_off (tmp, new);
      }
      else if (aux->g == LEXITG)
	new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);
  return new;
}

PUBLIC varlist
rewrite_soffert (soff)
  soffert *soff;
{
  int     i;
  varlist vl, setvl = NULL;

  /* set variables, if any, and collect them   */
  /* in setvl, to unset them after the process */
  for (i = 0; i < soff->nexp; i++)
    for (vl = soff->expl[i]->vrlst; vl != NULL; vl = INTtail (vl))
      if (soff->expl[i]->val != NULL) {
	if (!let_var (INThead (vl), kd_rw_node (kd_copy (soff->expl[i]->val))))
	  fatal_error ("Cannot initialize variable", __FILE__, __LINE__);
	setvl = INTcons (INThead (vl), setvl);
      }

  return setvl;
}

PUBLIC void
unrewrite_soffert (vl)
  varlist vl;
{
  /* unset variables */
  for (; vl != NULL; vl = INTtail (vl))
    if (reset_var (INThead (vl)))
      fatal_error ("Cannot reset variable", __FILE__, __LINE__);
  fIL ((CLR_TYPE) vl);
  vl = NULL;
}

PRIVATE boolean
match_exper (e1, e2)
  exper e1, e2;
{
  /* well, it may be the case, when matching offers  */
  /* that only the sort is known, as in, for example */
  /*  a ? x : bool || a ? y : bool                   */

  if (e1->sort != e2->sort)
    return FALSE;

  if ((e1->type == EXCLAM) && (e2->type == EXCLAM))
    return (NEQ != ldiequal (kd_copy (e1->val), kd_copy (e2->val)));

  return TRUE;
}

PUBLIC boolean
match_expl (max, el1, el2)
  int   max;
  exper *el1, *el2;
{
  int i;

  for (i = 0; i < max; i++)
    if (!match_exper (el1[i], el2[i]))
      return FALSE;
  return TRUE;
}

/* It is supposed that both experiment list match */
PRIVATE exper*
compose_expl (max, el1, el2)
  int   max;
  exper *el1, *el2;
{
  int i;
  exper *new;

  if (max == 0)
    return NULL;

  new = new_exper_array (max);

  for (i = 0; i < max; i++) {
    new[i] = new_exper ();

    new[i]->sort = el1[i]->sort;
    new[i]->vrlst = myINTappend (el1[i]->vrlst, el2[i]->vrlst);

    if (el1[i]->type == EXCLAM) {
      new[i]->type = EXCLAM;
      new[i]->val = kd_rw_node (kd_copy (el1[i]->val));
    }
    else if (el2[i]->type == EXCLAM) {
      new[i]->type = EXCLAM;
      new[i]->val = kd_rw_node (kd_copy (el2[i]->val));
    }
    else
      new[i]->type = INTERR;
  }
  return new;
}

PRIVATE soffert*
and_soff (soff1, soff2)
  soffert *soff1, *soff2;
{
  soffert *auxsof;

  assert (soff1 != NULL);
  assert (soff2 != NULL);

  if (soff1->g != soff2->g)
    return NULL;

  if (soff1->nexp != soff2->nexp)
    return NULL;

  if (soff1->nexp > 0)
    if (!match_expl (soff1->nexp, soff1->expl, soff2->expl))
      return NULL;

  auxsof = new_soffert ();

  auxsof->g    = soff1->g;
  auxsof->nexp = soff1->nexp;
  auxsof->expl = compose_expl (soff1->nexp, soff1->expl, soff2->expl);
  auxsof->prdl = CNDappend (soff1->prdl, CNDcopy (soff2->prdl));
  auxsof->ktl  = myINTappend (soff1->ktl, soff2->ktl);
  return auxsof;
}

/* return the union of both sets
 * Arguments are freed
 */
PUBLIC soffert*
union_sset_off (so1, so2)
  soffert *so1, *so2;
{
  soffert *aux = NULL;

  if (so1 == NULL)
	return so2;
  if (so2 == NULL)
	return so1;

  for (aux = so1 ; aux->next != NULL; aux = aux->next)
    ;
  aux->next = so2;
  return so1;
}

/* return the intersection of both sets
 * arguments are freed
 */
PUBLIC soffert*
inter_sset_off (so1, so2)
  soffert *so1, *so2;
{
  soffert *result = NULL, *p1, *p2;
  soffert *aux;

  if ((so1 == NULL) && (so2 == NULL))
    return NULL;

  if (so1 == NULL) {
    free_sset_off (so2);
    return NULL;
  }
  if (so2 == NULL) {
    free_sset_off (so1);
    return NULL;
  }

  for (p1 = so1; p1 != NULL; p1 = p1->next) {
    for (p2 = so2; p2 != NULL; p2 = p2->next) {
      if ((aux = and_soff (p1, p2)) != NULL)
	result = cons_sset_off (aux, result);
    }
  }

  free_sset_off (so1);
  free_sset_off (so2);

  return result;
}

/* It returns the number of experiment
 * of an _experiment_list node (for an _external_offer)
 * or a _exit_ent (for an _exit_exp). It may
 * be NULL, in which case, 0 is returned
 */
PRIVATE int
number_exp (r)
  TNODE *r;
{
  int i = 0;

  if (r != NULL) {
    for (r = gt_fs (r); r != NULL; r = gt_rb (r))
      i++;
  }
  return i;
}

/* From an "experiment" node or an "exit"ent" node,
 * it creates an "exp" node.
 * An experiment or exit_ent may be (see LBM)
 *     experiment ::= _var_id       (? or !)
 *     experiment ::= _value_exp    (only !)
 *     _exit_ent  ::= _value_exp    (as !)
 *     _exit_ent  ::= _sort_id      (as ?)
 */
PRIVATE exper
do_value (S, pi, r)
  spe   S;
  int   pi;
  TNODE *r;
{
  exper e;
  char  *vname;

  e = new_exper ();

  switch (r->type) {
  case tvar_id :
    e->type  = INTERR;
    e->var   = (int)takeclr (c_var_id, r);
    e->sort  = (int)id2sort (S, (CLR_TYPE)e->var);
    vname    = unique_var_id (S, e->var, pi);
    e->ldiui = get_var_id (vname, id2ui (S, (CLR_TYPE)e->sort));
    free (vname);
    if (e->ldiui >= 0)
      fatal_error ("Using variable not defined", __FILE__, __LINE__);
    e->vrlst = INTcons (e->ldiui, (INTlist)NULL);
    e->val   = get_value (e->ldiui);
    break;
  case tvalue_exp :
    e->type = EXCLAM;
    e->sort = (int)takeclr (c_sort, r);
    e->val  = kd_rw_node (val_exp2kdatum (S, pi, r));
    break;
  case tsort_id :
    e->type = INTERR;
    e->sort = (int)takeclr (c_sort, r);
    default :
      fatal_error ("Wrong node building experiment", __FILE__, __LINE__);
  }

  return e;
}

/* From an ACTION node of the lbm,
 * it creates the predicate for the
 * offert sof, if it exits
 */
PUBLIC void
add_predi (S, sof, pi, r)
  spe   S;
  soffert *sof;
  int   pi;
  TNODE *r;
{
  cond  prd;
  TNODE *h[MAX_TNODES];

  h[0] = r;
  myheval (h[0], h);
  /* Now, we may have  _external_offer ::= [ _experiment_list ]
   *                                       [ _predicate ]
   *			                   state
   *				           [ _annotation_list ]
   */

  if (h[2] != NULL) {
    prd = new_cond ();
    prd->val1 = val_exp2kdatum (S, pi, gt_fs (h[2]));
    prd->val2 = val_exp2kdatum (S, pi, gt_rb (gt_fs (h[2])));
    sof->prdl = CNDcons (prd, (CNDlist)NULL);
  }
}

/* From an ACTION or an EXIT node of the lbm,
 * it creates the experiment for the
 * offert sof, if it exits
 */
PUBLIC void
add_exper (S, sof, pi, r)
  spe   S;
  soffert *sof;
  int   pi;
  TNODE *r;
{
  int   i;
  TNODE *h[MAX_TNODES], *aux;

  h[0] = r;
  myheval (h[0], h);
  /* Now, we may have  _external_offer ::= [ _experiment_list ]
   *                                       [ _predicate ]
   *			                   state
   *				           [ _annotation_list ]
   * or, maybe,
   *               _exit_exp           ::= [ _exit_offer_list ]
   *                                       [ _annotation_list ]
   */

  if (h[1] != NULL) {
    sof->nexp = number_exp (h[1]);
    sof->expl = new_exper_array (sof->nexp);

    for (i = 0, aux = gt_fs (h[1]); i < sof->nexp; i++, aux = gt_rb (aux))
      sof->expl[i] = do_value (S, pi, aux);
  }
}

/* It actualizes the values obtained in the
 * negotiation of a synchronization
 */
PUBLIC void
update_values (sof)
  soffert *sof;
{
  int     i;
  INTlist vl;

  for (i = 0; i < sof->nexp; i++)
    if (sof->expl[i]->type == EXCLAM)
      for (vl = sof->expl[i]->vrlst; vl != NULL; vl = INTtail (vl))
	if (!let_var (INThead (vl), kd_rw_node (kd_copy (sof->expl[i]->val))))
	  fatal_error ("Cannot initialize variable", __FILE__, __LINE__);
}

PRIVATE boolean
pass_predicates (soff)
  soffert *soff;
{
  CNDlist auxl;
  varlist setvl = NULL;
  boolean res = TRUE;

  if (soff->prdl == NULL) /* no predicates! */
    return TRUE;

  setvl = rewrite_soffert (soff);

  /* check predicates */
  for (auxl = soff->prdl; auxl != NULL; auxl = auxl->next)
    if (NEQ == chk_cond (auxl->c))
      res = FALSE;

  unrewrite_soffert (setvl);

  return res;
}

PUBLIC soffert*
check_predicates (soffs)
  soffert *soffs;
{
  soffert *aux, *new = NULL;

  if (soffs == NULL)
    return NULL;

  for (aux = soffs ; aux != NULL; aux = aux->next)
    if (pass_predicates (aux))
      new = cons_sset_off (cp_soffert (aux), new);

  free_sset_off (soffs);

  return new;
}
