// Fonctions pour la beta-réduction

noeud * duplique_arbre(noeud * r)
{
  if (r==NULL) return NULL ; 
  noeud * x = cree_n(r->type, r->val, duplique_arbre(r->fg),
		     duplique_arbre(r->fd)) ; 
  return x ; 
}

// Hypothèse : l'arbre de la variable est non null, et il est bien de type VAR.
noeud * substitution(noeud * r, noeud * var, noeud * ssarbre)
{
  int valvar = var->val ; 

  // Arbre NULL : RAS
  if (r==NULL) return r ;
  //  printf("substitution (variable %s)\n", string_tds(VAR, valvar)) ; 
  // Variable recherchée : on retourne une copie du terme à la place
  if (r->type==VAR && r->val==valvar) {
    free(r) ; 
    return duplique_arbre(ssarbre) ; 
  }
  // Lieur de la même variable : pas de substitution 
  if (r->type==Q   && r->val==valvar) return r ; 
  // Cas général : on applique la subst. aux deux fils
  r->fg = substitution(r->fg, var, ssarbre) ; 
  r->fd = substitution(r->fd, var, ssarbre) ; 
  return r ; 
}

noeud * beta_reduit(noeud * r)
{
  // Arbre vide : RAF
  if (r == NULL) return NULL ; 
  //  printf("Béta réduction de ") ; affiche_formule(r) ; printf("\n") ; 
  // Arbre pas sous la forme d'une lambda-exp. + AF : 
  // on réduit les deux fils 
  if (r->type != AF || r->fg->type != LBD) {
    r->fg = beta_reduit(r->fg) ; 
    r->fd = beta_reduit(r->fd) ;
    return r ; 
  }
  // Cas intéressant : 
  return beta_reduit(substitution(r->fg->fd,r->fg->fg,r->fd)) ; 
}