/* 
$Id: backend.c,v 1.13 2001/01/15 15:58:01 sbeyer Exp $
$Log: backend.c,v $
Revision 1.13  2001/01/15 15:58:01  sbeyer

removed backend from project; moved 2 functions from backend to constant

Revision 1.12  2001/01/15 15:11:08  sbeyer

cosmetic changes (like const qualifier)

Revision 1.11  2001/01/11 11:47:28  sbeyer

renamed subknoten to sub in struct knoten

Revision 1.10  2001/01/09 16:27:30  sbeyer
*** empty log message ***

*/
#include "backend.h"
#include <stdio.h>

// dieses Makro wird von der convert-Funktion für die Subknoten von nicht besonders behandelten Knoten aufgerufen
#define convert_default_aktion if (parameter_verbose) \
                                 { \
                                   printf ("Knoten vom Typ %s wurde bei Konvertierung ignoriert.\n",token_string[knot->typ]);\
                                 } \
	                       for (i=0;i<knot->subanz;i++) \
                                 { \
                                   convert_knoten(knot->sub[i]); \
                                 }

struct parameterlisten_eintrag *parameterliste=NULL;
struct funktionslisten_eintrag *funktionsliste=NULL;
struct funktionslisten_eintrag *fehlende_funktionen=NULL;
struct funktionslisten_eintrag *synthetisierte_funktionen=NULL;
struct varlisten_eintrag *akt_varlist=NULL;

// gibt den Speicher eines Knotens und seiner Subknoten frei
void free_knot(struct knoten *knot)
{
  int i;
  for (i=0;i<knot->subanz;i++)
    {
      free_knot(knot->sub[i]);
    }
  if (knot->wert_str)
    {
      freigegebener_speicher+=strlen(knot->wert_str)+1;
      free(knot->wert_str);
    }
  free(knot);
  freigegebener_speicher+=sizeof(struct knoten);
}

// gibt eine variablen_liste aus
void varliste_ausgeben(struct varlisten_eintrag *varlist)
{
  struct varlisten_eintrag *temp=varlist;

  printf ("Variablenliste an Speicherstelle : %d\n",varlist);
  while (temp)
    {
      printf ("%s\n",temp->varname);
      temp=temp->next_variable;
    }
  printf("\n");
}

// erstellt eine Kopie einer Variablenliste und gibt einen Pointer darauf zurück
struct varlisten_eintrag *copy_varliste(struct varlisten_eintrag *original)
{
  struct varlisten_eintrag *anfang=NULL;
  struct varlisten_eintrag *temp_ori=original;
  struct varlisten_eintrag *temp=NULL;
  struct varlisten_eintrag *temp2=NULL;

  while (temp_ori)
    { 
      temp2=temp;
      temp=(struct varlisten_eintrag*) malloc(sizeof(struct varlisten_eintrag));
      allokierter_speicher+=sizeof(struct varlisten_eintrag);
      
      temp->varname=(char *) malloc(strlen(temp_ori->varname)+1);
      allokierter_speicher+=strlen(temp_ori->varname)+1;
      strcpy(temp->varname,temp_ori->varname);

      temp->typ.typ=temp_ori->typ.typ;
      temp->typ.bitvectorbreite=temp_ori->typ.bitvectorbreite;
      temp->previous_variable=temp2;
      if (temp2)
        {
          temp2->next_variable=temp;
        }
      temp->next_variable=NULL;
      
      if (!anfang)
        {
          anfang=temp;
        }

      temp_ori=temp_ori->next_variable;
    }
  return anfang;
}

// fuegt eine Funktion in die Funktionsliste ein (am Ende der Liste!!!)
void funktionsliste_add(struct funktionslisten_eintrag **listenanfang,char *funktionsname,struct knoten* wurzelknoten,struct varlisten_eintrag *varlist,int parameteranzahl,struct parameter_typ *parameter)
{
  struct funktionslisten_eintrag *temp=*listenanfang;
  struct funktionslisten_eintrag *temp2;

  while (temp)
    {
      temp2=temp;
      temp=temp->next_function;
    }
  temp=(struct funktionslisten_eintrag*) malloc(sizeof(struct funktionslisten_eintrag));
  allokierter_speicher+=sizeof(struct funktionslisten_eintrag);
  if (*listenanfang) // falls schon eine Liste existiert
    {
      temp2->next_function=temp;
      temp->previous_function=temp2;
    }
  else // erster Eintrag in einer neuen Liste
    {
      temp->previous_function=NULL;
      *listenanfang=temp;
    }
  temp->next_function=NULL;
  temp->funktionsname=(char *) malloc(strlen(funktionsname)+1);
  allokierter_speicher+=strlen(funktionsname)+1;

  temp->parameteranzahl=parameteranzahl;
  temp->parameter=parameter;
  
  strcpy(temp->funktionsname,funktionsname);
  temp->wurzelknoten=wurzelknoten;
  temp->var_list=copy_varliste(varlist);
}

// fuegt eine Variable in die Variablenliste ein (am Ende der Liste)
void varliste_add(char *varname,struct parameter_typ vartyp)
{
  struct varlisten_eintrag *temp=akt_varlist;
  struct varlisten_eintrag *temp2;
  while (temp)
    {
      temp2=temp;
      temp=temp->next_variable;
    }
  temp=(struct varlisten_eintrag*) malloc(sizeof(struct varlisten_eintrag));
  allokierter_speicher+=sizeof(struct varlisten_eintrag);
  if (akt_varlist) // falls schon eine Liste existiert
    {
      temp2->next_variable=temp;
      temp->previous_variable=temp2;
    }
  else // erster Eintrag in einer neuen Liste
    {
      temp->previous_variable=NULL;
      akt_varlist=temp;
    }
  temp->next_variable=NULL;
  temp->varname=(char *) malloc(strlen(varname)+1);
  allokierter_speicher+=strlen(varname)+1;
  strcpy(temp->varname,varname);
  temp->typ.typ=vartyp.typ;
  temp->typ.bitvectorbreite=vartyp.bitvectorbreite;
}

struct varlisten_eintrag *varliste_speicherfreigeben(struct varlisten_eintrag *varlist)
{
  struct varlisten_eintrag *temp=varlist;
  struct varlisten_eintrag *temp2;
  while (temp)
    {
      temp2=temp;
      freigegebener_speicher+=strlen(temp->varname)+1;
      free(temp->varname);
      temp=temp->next_variable;
      freigegebener_speicher+=sizeof(struct varlisten_eintrag);
      free(temp2);
    }
  return NULL;
}

struct funktionslisten_eintrag *funktionsliste_speicherfreigeben(struct funktionslisteneintrag *listenanfang)
{
  struct funktionslisten_eintrag *temp=listenanfang;
  struct funktionslisten_eintrag *temp2;
  int i;

  while (temp)
    {
      temp2=temp;

      if (temp->parameter) // wenn es eine Parameterliste gibt, diese auch freigeben
        {
          // Zuerst den Speicher fuer die Parameternamen freigeben
          for (i=0;i<temp->parameteranzahl;i++)
            {
              if (temp->parameter[i].name)
                {
                  freigegebener_speicher+=strlen(temp->parameter[i].name)+1;
                  free(temp->parameter[i].name);
                }
            }
          freigegebener_speicher+=temp->parameteranzahl*sizeof(struct parameter_typ);

          free(temp->parameter);
        } 

      if (temp->funktionsname)
	{
	  freigegebener_speicher+=strlen(temp->funktionsname)+1;
	  free(temp->funktionsname);
	}

      if (temp->var_list)
	{
	  temp->var_list=varliste_speicherfreigeben(temp->var_list);
	}
      temp=temp->next_function;
      freigegebener_speicher+=sizeof(struct funktionslisten_eintrag);
      free(temp2);
    }
  return NULL;
}

void funktionsliste_ausgeben(struct funktionslisteneintrag *listenanfang)
{
  struct funktionslisten_eintrag *temp=listenanfang;
  int i;

  while (temp)
    {
      printf ("Funktion : %s\n",temp->funktionsname);
      printf ("\t%d Parameter : ",temp->parameteranzahl);
      for (i=0;i<temp->parameteranzahl;i++)
        {
          printf (" %s",temp->parameter[i].name);
          if (temp->parameter[i].is_constant)
            {
              printf ("(constant)=%d",temp->parameter[i].wert);
            }
          printf(":%s",typname[temp->parameter[i].typ]);
          if (temp->parameter[i].typ==bitvector)
            {
              printf("[%d]",temp->parameter[i].bitvectorbreite);
            }
          printf (" ,");
        }
      if (synthetisierbar(temp)) printf ("\tsynthetisierbar");
      printf("\n");
      temp=temp->next_function;
    }
}

// fügt einen neuen Eintrag in die Paramter-Liste hinzu
void parameterlisten_add(char *parametername,int parametertyp,int bitvector_breite)
{
  struct parameterlisten_eintrag *temp=parameterliste;
  struct parameterlisten_eintrag *temp2;
  while (temp)
    {
      temp2=temp;
      temp=temp->next_parameter;
    }
  temp=(struct parameterlisten_eintrag*) malloc(sizeof(struct parameterlisten_eintrag));
  allokierter_speicher+=sizeof(struct parameterlisten_eintrag);
  if (parameterliste) // falls schon eine Liste existiert
    {
      temp2->next_parameter=temp;
      temp->previous_parameter=temp2;
    }
  else // erster Eintrag in einer neuen Liste
    {
      temp->previous_parameter=NULL;
      parameterliste=temp;
    }
  temp->next_parameter=NULL;
  temp->parametername=(char *) malloc(strlen(parametername)+1);
  allokierter_speicher+=strlen(parametername)+1;
  strcpy(temp->parametername,parametername);
  temp->parametertyp=parametertyp;
  temp->bitvector_breite=bitvector_breite;
}

// gibt den von der Parameter-Liste benutzten Speicher wieder frei
void parameterliste_speicherfreigeben()
{
  struct parameterlisten_eintrag *temp=parameterliste;
  struct parameterlisten_eintrag *temp2;
  while (temp)
    {
      temp2=temp;
      freigegebener_speicher+=strlen(temp->parametername)+1;
      free(temp->parametername);
      temp=temp->next_parameter;
      freigegebener_speicher+=sizeof(struct parameterlisten_eintrag);
      free(temp2);
    }
  parameterliste=NULL;
}

// Parametertyp bestimmen ; erwartet einen Knoten vom Typ : type_expr
struct parameter_typ bestimme_parametertyp(struct knoten *knot)
{
  struct knoten *merke;
  struct parameter_typ typmerke;

  typmerke.typ=other;
  typmerke.bitvectorbreite=0;

  // Paramtertyp bestimmen
  if (knot->subtyp==131)         // type_expr -> name
    {
      merke=knot->sub[0];
      
      // Typ : Bitvector
      if ((merke->subtyp==348)                               // name_token -> idop actuals
          && (merke->sub[0]->subtyp==331)              // idop -> ID
          && (strcmp(merke->sub[0]->sub[0]->wert_str,"bvec")==0)) // Typebezeichnung ist bvec
        {
          // wenn das alles so ist, ist es wohl ein bvec
          typmerke.typ=bitvector;
          
          if ((merke->sub[1]->sub[0]->subtyp==400) // actual_list -> actual
              && (merke->sub[1]->sub[0]->sub[0]->subtyp==402)) // actual -> expr
            typmerke.bitvectorbreite=expression_ausrechnen(merke->sub[1]->sub[0]->sub[0]->sub[0]);
        }

      // Typ : Bit  (wird hier als bvec[1] behandelt)
      if ((merke->subtyp==347)                               // name_token -> idop
          && (merke->sub[0]->subtyp==331)              // idop -> ID
          && (strcmp(merke->sub[0]->sub[0]->wert_str,"bit")==0))  // Typbezeichnung ist bit
        {
          // also ist der Typ : bit
          typmerke.typ=bitvector;
          typmerke.bitvectorbreite=1;
            }
      
      // Typ : nat, posnat
      if ((merke->subtyp==347)                               // name_token -> idop
          && (merke->sub[0]->subtyp==331)              // idop -> ID
          && ( (strcmp(merke->sub[0]->sub[0]->wert_str,"posnat")==0) // Typbezeichnung ist posnat
               || (strcmp(merke->sub[0]->sub[0]->wert_str,"nat")==0))) // Typebezeichnung ist nat
        {
              // also ist er vom Typ nat oder posnat
          typmerke.typ=unbounded_nat;
        }
    }
  else
        {
          printf ("Nicht unterstützte Form des Parametertyps!!! (mit Typ other in Liste eingetragen)\n");
        }
  return typmerke;
}

// ermittelt anhand eines Variablennamens den Typ dieser Variablen
struct parameter_typ get_parametertyp_from_variable(char *varname,struct varlisten_eintrag *parameter_list)
{
  struct varlisten_eintrag *temp=parameter_list;
  struct parameter_typ parameter_merke;

  // Typ initialisieren, falls keine entsprechende Variable gefunden wird
  parameter_merke.typ=-2;
  parameter_merke.bitvectorbreite=0;

  // Variablenliste nach varname durchsuchen
  while (temp)
    {
      if (strcmp(temp->varname,varname)==0)
        {
          parameter_merke.typ=temp->typ.typ;
          parameter_merke.bitvectorbreite=temp->typ.bitvectorbreite;
        }
      temp=temp->next_variable;
    }
  return parameter_merke;
}

// übernimmt einen Knoten vom Typ adformal und extrahiert hieraus den Parameter in die Parameterliste
int verarbeite_adformal(struct knoten *knot,struct varlisten_eintrag *varliste)
{
  struct knoten *merke;
  struct parameter_typ typmerke;
  char *namenmerke;
  int fehler=0;
  int anzahl=0;
  
  if ((knot->subtyp==95)                                         // adformal -> typeid
      && ((knot->sub[0]->subtyp==337)                      // typeid -> idop ':' type_expr
          || (knot->sub[0]->subtyp==335)))                 // typeid -> idop
    {
      // Parameternamen bestimmen
      if (knot->sub[0]->sub[0]->subtyp==331)         // idop -> ID
        {
          namenmerke=knot->sub[0]->sub[0]->sub[0]->wert_str;
        }
      else
        {
          printf ("Nicht unterstützte Form des Parameternamens!!!\n");
          fehler=1;
        }

      // Parametertyp bestimmen
      if (knot->sub[0]->subtyp==337)                       // typeid -> idop ':' type_expr
        {
          typmerke=bestimme_parametertyp(knot->sub[0]->sub[1]);
        }
      if (knot->sub[0]->subtyp==335)                       // typeid -> idop
        {
          typmerke=get_parametertyp_from_variable(namenmerke,varliste);
        }

      // falls kein Fehler aufgetreten ist Parameter in die Liste einfügen
      if (!fehler)
        {
          parameterlisten_add(namenmerke,typmerke.typ,typmerke.bitvectorbreite);
          anzahl++;
        }
    }
  else
    {
      printf ("Nicht unterstützte Parameterform!!! (nicht in Liste eingetragen)\n");
    }
  return anzahl;
}

// übernimmt einen Knoten vom Typ adformals und extrahiert hieraus die Parameter in die Parameterliste
int verarbeite_adformals(struct knoten *knot,struct varlisten_eintrag *varliste)
{
  struct knoten *akt_knot=knot;
  int anzahl=0;

  while (akt_knot->subtyp==94) // 94 entspricht adformals -> adformal ',' adformals
    {
      anzahl+=verarbeite_adformal(akt_knot->sub[0],varliste);
      akt_knot=akt_knot->sub[1];
    }
  anzahl+=verarbeite_adformal(akt_knot->sub[0],varliste);
  return anzahl;
}

// extrahiert die Parameter einer Funktion aus dem Parse-Tree in die Parameter_liste
int extrahiere_parameter(struct funktionslisten_eintrag *funktion)
{
  struct knoten *startpos;
  int anzahl=0;

  startpos=funktion->wurzelknoten->sub[1];
  if (startpos->subanz>0) // d.h. es gibt Parameter
    {
      startpos=startpos->sub[0];
      while (startpos->subtyp==307) // pdformals_plus -> pdformals_plus '(' adformals ')'
        {
          anzahl+=verarbeite_adformals(startpos->sub[1],funktion->var_list);
          startpos=startpos->sub[0]; // naechster pdformals_plus-Teil
        }
      anzahl+=verarbeite_adformals(startpos->sub[0],funktion->var_list);
    }
  return anzahl;
}

// bestimmt den Typ der Rückgabe der Funktion und trägt ihn inm funktionslisten_eintrag ein
void bestimme_rueckgabetyp(struct funktionslisten_eintrag *funktion)
{
  struct knoten *temp=funktion->wurzelknoten;
  struct parameter_typ typmerke;

  // "normale" Funktion
  if ((temp->sub[2]->subtyp==103)                     // theory_decl -> const_decl
      && (temp->sub[2]->sub[0]->subtyp==123))   // const_decl -> type_expr const_value
    {
      typmerke=bestimme_parametertyp(temp->sub[2]->sub[0]->sub[0]);
    }

  // rekursive Funktion
  if ((temp->sub[2]->subtyp==104)                      // theory_decl -> def_decl
      && (temp->sub[2]->sub[0]->subtyp==125))    // def_decl -> RECURSIVE type_expr '=' expr MEASURE expr
    {
      typmerke=bestimme_parametertyp(temp->sub[2]->sub[0]->sub[0]);
    }

  funktion->rueckgabe_parameter_typ=typmerke.typ;
  funktion->rueckgabe_parameter_bitvectorbreite=typmerke.bitvectorbreite;
  if (parameter_verbose)
    {
      printf ("Rückgabeparameter : Typ ");
    }
  switch (typmerke.typ)
    {
    case 0 : 
      {
        if (parameter_verbose)
          {
            printf ("Bitvector Breite : %d\n",typmerke.bitvectorbreite);
          }
        break;
      }
    case 1 :
      {
        if (parameter_verbose)
          {
            printf ("Nat bzw. Posnat\n");
          }
        break;
      }
    case 2 :
      {
        if (parameter_verbose)
          {
            printf ("Other\n");
          }
        break;
      }
    default :
      {
        if (parameter_verbose)
          {
            printf("Unbekannter Typ\n");
          }
      }
    }
}

// testet, ob eine Funktion synthetisierbar ist (d.h. z.B. ob alle Nat-Parameter als Konstanten vorliegen)
int synthetisierbar(struct funktionslisten_eintrag *funktion)
{
  int i;
  int temp=1;

  for (i=0;i<funktion->parameteranzahl;i++)
    {
      if ((funktion->parameter[i].typ!=bitvector) 
          && (funktion->parameter[i].is_constant==0))         // falls Typ!=Bitvector und Wert nicht konstant, kann nicht synth. werden
        {
          temp=0;
        }
      if ((funktion->parameter[i].typ==bitvector) 
          && (funktion->parameter[i].bitvectorbreite==-1))    // falls Bitvector unbekannte Breite hat, kann nicht synth. werden
        {
          temp=0;
        }
    }
  return temp;
}

// übersetzt einen Knoten, samt Subknoten, nach hdl
void convert_knoten(struct knoten *knot)
{
  int i;
  struct parameter_typ typmerke;

  switch (knot->typ)
    {
      case theory:
      {
        convert_default_aktion // erst die Unterknoten der Theory convertieren
        if (akt_varlist)
          {
            akt_varlist=varliste_speicherfreigeben(akt_varlist); // am Ende einer Theory wird die Liste der aktuellen Variablen gelöscht
          }
        break;
      }
    case theory_elt : 
      {
        if (knot->subtyp==77)                      // 77 entspricht : theory_elt => idops pdformals_stern ':' theory_decl ';'
          {
            if (knot->sub[2]->subtyp==106)   // 106 entspricht : theory_decl => formula_decl
              {
                // dieser Knoten (mit Unterknoten) ist ein Lemma, Theorem ...
                if (parameter_verbose)
                  {
                    printf ("LEMMA,THEOREM usw. werden ignoriert\n");
                  }
              }
            else
              {
                if ((knot->sub[0]->subtyp==329)  // 329 entspricht : idops => idop
                    && (knot->sub[0]->sub[0]->subtyp==331)) // 331 entspricht : idop => ID
                  {
                    if (knot->sub[1]->subtyp==68)  // 68 entspricht : pdformals_stern => pdformals_plus
                      {
                        // dieser Knoten ist eine Funktionsdefinition
                        funktionsliste_add(&funktionsliste,knot->sub[0]->sub[0]->sub[0]->wert_str,knot,akt_varlist,0,NULL);
                      }

                    if (knot->sub[2]->subtyp==102)  // 102 entspricht : theory_decl => var_decl
                      {
                        // dieser Knoten ist eine Variablendefinition
                        typmerke=bestimme_parametertyp(knot->sub[2]->sub[0]->sub[0]);
                        varliste_add(knot->sub[0]->sub[0]->sub[0]->wert_str,typmerke);
                        if (parameter_verbose)
                          {
                            printf ("Variable %s vom Typ %d gefunden.\n",knot->sub[0]->sub[0]->sub[0]->wert_str,typmerke);
                          }
                      }
                  }  
              }
          }
        else
          {
            convert_default_aktion
          }
        break;
      }
    case expr :
      {
        knot=vereinfache_expression(knot);
        break;
      } 
    default : 
      {
        convert_default_aktion
      }
    }
}