/*
$Id: synthesize_type.cpp,v 1.29 2003/02/24 11:00:48 sbeyer Exp $
$Log: synthesize_type.cpp,v $
Revision 1.29  2003/02/24 11:00:48  sbeyer
* added reasonable error message for tuple types

Revision 1.28  2002/12/02 14:36:58  sbeyer
* ported source to gcc-3.2 (still compiles AND WORKS with gcc-2.9x)

Revision 1.27  2002/03/27 18:40:52  sbeyer
* added support for uninterpreted types

Revision 1.26  2002/03/18 20:26:37  sbeyer
* a few optimizations

Revision 1.25  2002/02/26 13:23:14  sbeyer
* fixed bug where RAM lost information about its address width
* fixed bug where array of RAM was treated as single bitvector
* made pseudo-warning in case of overloaded functions real warning
  (source code is now REALLY processed further after WARNING output)
* in case of (case insensitive) overloading, added location of initial definition to warning/error output
* WARNING output no longer reports termination of pvs2hdl

Revision 1.24  2001/07/05 11:36:55  sbeyer
* added special treatment for below(k)->bvec[1] array
  (now simply treated as bvec[k] !!!)

Revision 1.23  2001/06/13 09:52:05  sbeyer
* added width computation for register type

Revision 1.22  2001/06/12 14:56:45  sbeyer
* added reasonable error message for record type overflow
* increased supported record size from 200 to 1000 fields

Revision 1.21  2001/06/11 18:21:41  kroening
* added posint

Revision 1.20  2001/06/06 13:18:16  sbeyer
* started making ram usage safe (no ram on conditional assignments, etc...)

Revision 1.19  2001/05/31 13:46:33  dirkl
- reordering of record-elements implemented

Revision 1.18  2001/05/30 18:07:58  sbeyer
* added array and ram support in types
* BETA support for function lookup table

Revision 1.17  2001/04/20 13:45:35  dirkl
- added support for records in conds

Revision 1.16  2001/03/15 11:19:54  sbeyer

wrote own list-merge (ordered merge required) and fixed last is_member-bug

Revision 1.15  2001/03/14 16:15:35  sbeyer

fixed type_array::is_member-bug

Revision 1.14  2001/03/14 11:15:13  sbeyer

added reasonable error messages for too many/few actuals/parameters (instead of simple core dump)

Revision 1.13  2001/02/05 13:44:09  sbeyer

fixed bug in register support

Revision 1.12  2001/02/05 11:14:46  sbeyer

added register support

Revision 1.11  2001/01/29 11:03:00  sbeyer

fixed get_type_bindings-bug

Revision 1.10  2001/01/26 16:17:40  sbeyer

fixed type_array::is_member - bug

Revision 1.9  2001/01/26 15:07:53  sbeyer
removed output of obsolete error-parse-trees; calling string-constructur in type_array::empty() now

Revision 1.8  2001/01/25 15:41:36  sbeyer

added cvs log

*/
#include "synthesize_core.h"
#include "tools.h"
#include "constant.h"
#include <iostream>

using namespace std;

type_array::type_array(const type_array &tarray)
{ 
  num=tarray.num;
  for (int i=0;i<num;i++)
  {
    name[i]=tarray.name[i]; 
    type[i]=tarray.type[i];
    bitbreite[i]=tarray.bitbreite[i];
    lower_bound[i]=tarray.lower_bound[i];
    upper_bound[i]=tarray.upper_bound[i];    
    ram_address_width[i]=tarray.ram_address_width[i];    
  }
}

bool type_array::add_member(const string &_name,
                            int _type,
                            int _bitbreite  /*=1*/,
                            int _lower_bound/*=0*/,
                            int _upper_bound/*=0*/,
                            int _ram_address_width/*=0*/)
{ 
  if (num<MAX_RECORD_MEMBER_COUNT)
  {
    name[num]=_name; 
    type[num]=_type;
    bitbreite[num]=_bitbreite;
    lower_bound[num]=_lower_bound;
    upper_bound[num]=_upper_bound;
    ram_address_width[num]=_ram_address_width;
    num++;
    return true;
  }
  else
    return false;
}

bool type_array::add_member(const string &_name,
                            const type_array &tarray)
{
  if (num+tarray.num>MAX_RECORD_MEMBER_COUNT)
    return false;
  for (int i=0;i<tarray.num;i++)
    add_member(inv_compose_record_name(_name,tarray.name[i]),
               tarray.type[i],
               tarray.bitbreite[i],
               tarray.lower_bound[i],
               tarray.upper_bound[i],
               tarray.ram_address_width[i]);
  return true;
}

void type_array::make_ram(const type_array &tarray,
                          int _address_width)
{
  *this=tarray;
  ram_address_width[0]=_address_width;
  type[0]=ram;
}

bool type_array::make_array(const type_array &tarray,
                            int _lower_bound, 
                            int _upper_bound)
{
  empty();
  if (tarray.name[0].empty() && 
      tarray.type[0]==bitvector &&
      tarray.bitbreite[0]==1 &&
      _lower_bound==0)
  { // special case : array[0..k-1] of bvec 1 is bvec[k]
    if (!add_member(tarray.name[0],bitvector,_upper_bound+1))
      return false;
  }
  else
    for (int j=_upper_bound;j>=_lower_bound;j--)
    {
      char char_tmp[6];
      sprintf(char_tmp,"(%i)",j);
      for (int i=0;i<tarray.num;i++)
        if (!add_member(char_tmp+tarray.name[i],
                        tarray.type[i],
                        tarray.bitbreite[i],
                        tarray.lower_bound[i],
                        tarray.upper_bound[i],
                        tarray.ram_address_width[i]))
          return false;
    }
  return true;
}

bool type_array::contains_ram() const
{
  for (int i=0; i<num; i++)
    if (type[i]==ram)
      return true;
  return false;    
}

bool type_array::is_member(const string &_name, int &index) const
{
  for (index=0; index<num; index++)
    if (name[index]==_name)
      return true;
  return false;    
}

bool type_array::is_member(const string       &_name, 
                                 type_array   &tarray,
                                 list<string> &strlist) const
{
  if (_name.empty()) // no name is member of all
  {
    tarray=*this;
    return true;
  }
  list<string> ret;
  list<string>::const_iterator j=strlist.begin();
  if (num!=strlist.size())
    raise_error(cout << "internal error!\n")
  for (int i=0; i<num; i++,j++)
	//    if (name[i].find(_name)==0) // name i starts with _name?
    if (name[i]==_name ||
        name[i].find(_name+REC_DEREF)==0 ||
        name[i].find(_name+'(')==0) // name is the same or starts with _name` or _name(
    {
      tarray.add_member(name[i].c_str()+_name.length(),type[i],bitbreite[i],
                        lower_bound[i],upper_bound[i],ram_address_width[i]); // add name
							// AFTER _name
      ret.push_back(*j);
    }
  strlist=ret;
  return tarray.num!=0;
}

// the above function WITHOUT the stringlist-output
bool type_array::is_member(const string       &_name, 
                                 type_array   &tarray) const
{
  if (_name.empty()) // no name is member of all
  {
    tarray=*this;
    return true;
  }
  for (int i=0; i<num; i++)
	//    if (name[i].find(_name)==0) // name i starts with _name?
    if (name[i]==_name ||
        name[i].find(_name+REC_DEREF)==0 ||
        name[i].find(_name+'(')==0) // name is the same or starts with _name` or _name(
      tarray.add_member(name[i].c_str()+_name.length(),type[i],bitbreite[i],
                        lower_bound[i],upper_bound[i],ram_address_width[i]); // add name
							// AFTER _name
  return tarray.num!=0;
}

bool type_array::is_member(const type_array   &tarray,
                           int          &start,
                           int          &end) const
{
  string::size_type n;
  string prefix;
  for (int i=0; i+tarray.num<=num; i++)
  {
    int j;
    for (j=0; j<tarray.num; j++)
    {
      if (!tarray.name[j].empty()) // only for complex types
      {
        if (name[i+j]==tarray.name[j])
          n=0;
        else
        {
          n=name[i+j].rfind(tarray.name[j]);
          if (n==string::npos) // not substring?
            break;
          if (n!=name[i+j].length()-tarray.name[j].length()) // not at the end?
            break;
        }
        if (!j) // first iteration?
          prefix=name[i+j].substr(0,n); // remember prefix
        if (j && prefix!=name[i+j].substr(0,n))  // not same prefix?
          break;
      }
      if (bitbreite[i+j]!=tarray.bitbreite[j]) // finally, same width?
        break;
    }    
    if (j==tarray.num) // none of the above breaks executed?
    {
      start=i;
      end=i+tarray.num;
      return true;
    }          
  }
  return false;
}

int type_array::bit_count() const
{
  int ret=0;
  for (int i=0; i<num; i++)
    if (type[i]==bitvector)
      ret+=bitbreite[i];
  return ret;
}


bool type_array::is_simple() const
{
  for (int i=0; i<num; i++)
    if (type[i]!=bitvector && type[i]!=ram)
      return false;
  return true;    
}

bool type_array::operator ==(const type_array &tarray) const
{
  int dummy;
  if (num!=tarray.num)
    return false;
  for (int i=0;i<num;i++)
    if (!is_member(tarray.name[i],dummy))
      return false;
    else
      if (bitbreite[dummy]!=tarray.bitbreite[i] ||
          ram_address_width[dummy]!=tarray.ram_address_width[i])
        return false;
  return true;
} 

bool type_array::simple_equality(const type_array &tarray) const
{
  if (num!=tarray.num)
    return false;
  for (int i=0;i<num;i++)
    {
      if (name[i]!=tarray.name[i])
        return false;
      if (bitbreite[i]!=tarray.bitbreite[i])
        return false;
      if (ram_address_width[i]!=tarray.ram_address_width[i])
        return false;
    }
  return true;
}

// changes order of record-elements acording to order in tarray
bool type_array::change_order(const type_array &tarray,list<string> &ret_string)
{
  if (*this!=tarray) // umsortieren nur möglich, wenn grundsätzlich gleich
    {
      return false;
    }
  else
    {
      type_array temp=*this;
      list<string> new_ret_string=ret_string;

      list<string>::const_iterator iter;
      int i1,i2;

      // empty type_array and ret_string
      empty();
      ret_string.clear();

      // now refill in correct order
      for (i1=0;i1<tarray.num;i1++)
	{
	  // find correct position in 'this'-type_array
	  i2=0;
	  iter=new_ret_string.begin();
	  while (!( (tarray.name[i1]==temp.name[i2]) && (tarray.bitbreite[i1]==temp.bitbreite[i2])))
	    {
	      if (i2>=temp.num)
		{
		  raise_error(cout << "This error should NOT occur!!!\n")
		}
	      i2++;
	      iter++;
	    }
	  
	  // put data from correct position to new_ret_string and 'this'-type_array
	  ret_string.push_back(*iter);
	  add_member(temp.name[i2],temp.type[i2],temp.bitbreite[i2],temp.lower_bound[i2],temp.upper_bound[i2],temp.ram_address_width[i2]);
	}
      if (simple_equality(tarray))
	{
	  return true;
	}
      else
	{
	  return false;
	}
    }
}

ostream& operator <<(ostream& ostr, const type_array& tarray)
{
  if (!tarray.name[0].empty())
  {
    ostr << "complex type contains " << tarray.num << " subtypes:";
    for (int i=0;i<tarray.num;i++)
    {
      ostr << endl << tarray.name[i] << ": " <<  typname[tarray.type[i]];
      if (tarray.type[i]==bitvector || tarray.type[i]==ram)
        ostr << ", width " << tarray.bitbreite[i];
      if (tarray.type[i]==bounded_nat)
        ostr << ", lower bound " << tarray.lower_bound[i]
             << ", upper bound " << tarray.upper_bound[i];
      if (tarray.type[i]==ram)
        ostr << ", address width " << tarray.ram_address_width[i];
    }
  }
  else
  {
    ostr << "simple type " << typname[tarray.type[0]];
      if (tarray.type[0]==bitvector || tarray.type[0]==ram)
        ostr << ", width " << tarray.bitbreite[0];
      if (tarray.type[0]==bounded_nat)
        ostr << ", lower bound " << tarray.lower_bound[0]
             << ", upper bound " << tarray.upper_bound[0];
      if (tarray.type[0]==ram)
        ostr << ", address width " << tarray.ram_address_width[0];
  }
  return ostr;
}

bool is_bound(const list<binding> &bindings, 
              const string        &name,
              int                 &value)
{
  list<binding>::const_iterator i=bindings.begin();
  while (i!=bindings.end())
  {
    if (i->name==name)
    {
      value = i->value;
      return true;
    }
    i++;
  }
  return false;
};

void apply_bindings(knoten              *root,
                    const list<binding> &bindings);

void apply_bindings_bindlist(knoten        *parent,
                             knoten        *root, 
                             list<binding> &bindings)
{
  int i=0;
  int value;
  knoten *tmp;

  switch (root->subtyp)
  {
    case 241 : // bind_list ',' bind
      // left-to-right evaluation!!!
      apply_bindings_bindlist(root,root->sub[0],bindings);
      // root node might have been changed!
      if (root->subtyp==241)
        i=1;
      // no break!!
    case 240 : // bind
    {
      if (root->sub[i]->subtyp==238) // '(' simplebind_list ')' '=' expr
        knot_error("simplebind_list not supported\n",root->sub[i])
      if (root->sub[i]->sub[0]->sub[0]->subtyp==332) // opsym
        knot_error("only id in bind supported, not opsym\n",root->sub[i]->sub[0])
      const char *const &name=root->sub[i]->sub[0]->sub[0]->sub[0]->wert_str;
      // simplify the expresssion
      apply_bindings(root->sub[i]->sub[1],bindings);
      vereinfache_teilbaum(root->sub[i]->sub[1]);
      switch(root->sub[i]->sub[0]->subtyp)
      {
        case 304 : // idop ':' type_expr
        case 302 : // idop
          if (is_constant(root->sub[i]->sub[1],value))
          {
            // push_front for 'local shadows global'
            bindings.push_front(binding(name,value));
            if (parameter_verbose)
              cout << "removing LET " << name << " = " 
                   << value << " from parse tree\n";
            // and cut this binding from the tree:
            if (parent->subtyp==241) 
            // parent = "bind_list -> bind_list ',' bind"
            {
              if (i) // root = "bind_list -> bind_list ',' bind"
              {
                parent->sub[0]=root->sub[0];
                // free only the tree of the constant bind
                knoten_speicherfreigeben(root->sub[1]);
                // and the root node WITHOUT its bind_list-child
                free_knot(root);
              }
              else   // root = "bind_list -> bind"
              // modify parent to 'bind_list -> bind'
              {
                parent->subtyp=240;  // bind
                parent->subanz=1;
                parent->sub[0]=parent->sub[1];
                knoten_speicherfreigeben(root);
              }
            }      
            else // parent = ''LET bind_list IN expr'
            {
              // modify the toplevel let node
              // from 'LET bind_list IN expr'
              // to 'expr's expression type
              
              // change the parents type
              tmp=parent->sub[1];
              parent->subtyp=tmp->subtyp;
              parent->subanz=tmp->subanz;
              for (int j=i;j<parent->subanz;j++)
                parent->sub[j]=copysyntaxbaum(tmp->sub[j]);
              knoten_speicherfreigeben(root);
              knoten_speicherfreigeben(tmp);
            }      
          }      
          break;
        case 303 : // idop pdformals_plus
        case 305 : // idop pdformals_plus ':' type_expr
          knot_error(cout << "pdformals in bindlist not supported\n",root)
        default :
          knot_error(cout << "bindlist with unexpected subtype\n",root)
      }      
      break;
    }      
    default :
      knot_error(cout << "bindlist with unexpected subtype\n",root)
  }
}

void apply_bindings(knoten              *root,
                    const list<binding> &bindings)
{
  int value;
  list<binding> neu_bindings;

  /* Gehe den Syntaxbaum der Funktion durch und suche Variablen, deren Namen mit einem der konstanten Parameter
     uebereinstimmt und ersetzte dann diese Variable durch eine Konstante */
  
  switch (root->subtyp)
  { 
	//    case 167 :                         // expr -> expr funarg
	//      apply_bindings(root->sub[0],bindings);
	//      apply_bindings(root->sub[1],bindings);
	//      break;
    case 159 :                        // expr -> name
	  if (root->sub[0]->subtyp==348)   // name -> idop actuals 
        // apply bindings in all actuals
        apply_bindings(root->sub[0]->sub[1]->sub[0],bindings);
      if ((root->sub[0]->subtyp==348 ||   // name -> idop actuals 
           root->sub[0]->subtyp==347)    // name -> idop
          && (root->sub[0]->sub[0]->subtyp==331))     // idop -> ID
      {
        if (is_bound(bindings,root->sub[0]->sub[0]->sub[0]->wert_str,value))
        {
          if (parameter_verbose)
            cout << "Variable " << root->sub[0]->sub[0]->sub[0]->wert_str
                 << " wird durch Konstante " << value 
                 << " ersetzt.\n";
          // Knoten fuer Variable freigeben
          knoten_speicherfreigeben(root->sub[0]); 
          // und Knotentyp von root umaendern
          root->subtyp=157; // expr -> NUMBER
          // neuen Knoten fuer Konstante anlegen
          root->sub[0]=number_knoten_int(value);
        }
      }
      break;
    case 227 : // expr -> LET bind_list IN expr
      neu_bindings=bindings;
      apply_bindings_bindlist(root,root->sub[0],neu_bindings);
      // subtype might have been changed!
      if (root->subtyp==227)
        apply_bindings(root->sub[1],neu_bindings);
      else
        apply_bindings(root,neu_bindings);
      break;
    default :
      for (int i=0;i<root->subanz;i++)
        apply_bindings(root->sub[i],bindings);
  }
}

knoten *simplify_tree(const knoten        * const root,
                      const list<binding> &bindings)
{
  knoten *copy=copysyntaxbaum(root);
  apply_bindings(copy,bindings);
  return vereinfache_teilbaum(copy);
};

void add_actual(const knoten        *const root, 
                const actuals_array &act,
                list<binding>       &bindings,
                const string        &name,
                int                  index)
{
  switch (root->subtyp)
  {
    case 400 :   // actual
      if (root->sub[0]->subtyp==402) // actual -> expr ?
        if (is_constant(root->sub[0]->sub[0]))
        {
          if ((signed int)index-(signed int)bindings.size()<0)
            knot_error(cout << "function/type " << name 
                       << " instantiated with too many actuals (" 
                       << act.num << " expected)\n",root)
          if (parameter_verbose)
            cout << "actual " << act.names[index-bindings.size()]
                 << " is constant; value " << get_constant_value(root->sub[0]->sub[0]) << endl;
          bindings.push_front(binding(act.names[index-bindings.size()],
                                      get_constant_value(root->sub[0]->sub[0])));
        }
        else
          knot_error(cout << "actual " << act.names[index-bindings.size()]
                          << " isn't constant!\n",root)
      else
        knot_error(printf("Als actuals werden nur Expressions unterstuetzt!\n"),root);
      break;
    case 401 :   // actual_list ',' actual
      if (root->sub[1]->subtyp==402) // actual -> expr ?
        if (is_constant(root->sub[1]->sub[0]))
        {
          if ((signed int)index-(signed int)bindings.size()<0)
            knot_error(cout << "function/type " << name 
                       << " instantiated with too many actuals (" 
                       << act.num << " expected)\n",root)
          if (parameter_verbose)
            cout << "actual " << act.names[index-bindings.size()]
                 << " is constant; value " << get_constant_value(root->sub[1]->sub[0]) << endl;
            bindings.push_front(binding(act.names[index-bindings.size()],
                                      get_constant_value(root->sub[1]->sub[0])));
        }
        else
           knot_error(cout << "actual " << act.names[index-bindings.size()]
                          << " isn't constant!\n",root)
      else
        knot_error(printf("Als actuals werden nur Expressions unterstuetzt!\n"),root);
      // right-to-left evaluation
      add_actual(root->sub[0],act,bindings,name,index);
      break;
    default:
      knot_error(printf("Aufruf von add_actual mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void add_parameter(const knoten       *const root,
                   const params_array &params,
                   list<binding>      &bindings,
				   list<knoten *>     &parameters,
                   const string       &name,
                   bool                error_if_not_bound)
{
  switch (root->subtyp)
  {
    case 247 :   // expr ',' expr_list
      // right-to-left evaluation
      add_parameter(root->sub[1],params,bindings,parameters,name,error_if_not_bound);
      // no break!!!
    case 246 :   // expr
      if (bindings.size()+parameters.size()>=params.num)
        knot_error(cout << "function/type " << name << " has too many parameters (" 
                   << params.num << " expected)\n",root)
      if (is_constant(root->sub[0]))
      {
        if (parameter_verbose)
          cout << "parameter " << params.names[bindings.size()+parameters.size()]
               << " is constant; value " << get_constant_value(root->sub[0]) << endl;
        bindings.push_front(binding(params.names[bindings.size()+parameters.size()],
                                    get_constant_value(root->sub[0])));
      }
      else
         if (error_if_not_bound)
           knot_error(cout << "parameter " << params.names[bindings.size()+parameters.size()]
                          << " isn't constant!\n",root)
         else
           parameters.push_front(root->sub[0]);
      break;
    default:
      knot_error(printf("Aufruf von add_parameter mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_function_call_bindings(const knoten           *const root,
                                const defined_function &function,
                                list<binding>          &bindings,
								list<knoten *>         &parameters)
{
  switch (root->subtyp)
  {
    case 167 :   // expr funarg
      // only possibility: funarg -> '(' expr_leerlist ')'
      if (root->sub[1]->sub[0]->subtyp==245) // expr_leerlist -> expr_list ?
        add_parameter(root->sub[1]->sub[0]->sub[0],function.params,
                      bindings,parameters,function.name);
      get_function_call_bindings(root->sub[0],function,bindings,parameters);
      break;
    case 159 :   // name
      if (bindings.size()+parameters.size()<function.params.num)
        knot_error(cout <<"function " << function.name << " has too few parameters (" 
                   << function.params.num << " expected)\n",root)
      if (root->sub[0]->subtyp==348) // name -> idop actuals ?
      // only possibility: actuals -> '[' actual_list ']'
      {
        int i=bindings.size();
        add_actual(root->sub[0]->sub[1]->sub[0],*function.p_actuals,
                   bindings,function.name,bindings.size()+function.p_actuals->num-1);
        if (bindings.size()-i<function.p_actuals->num)
          knot_error(cout <<"function " << function.name << " has too few actuals (" 
                     << function.p_actuals->num << " expected)\n",root)
      }
      else // no actuals
        if (function.p_actuals->num)
          knot_error(cout << "function " << function.name 
                     << " instantiated without actuals (" 
                     << function.p_actuals->num << " expected)\n",root)
      break;
    default:
      knot_error(printf("Aufruf von get_function_call_bindings mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_type_bindings(const knoten       *const root,
                       const defined_type &type,
                       list<binding>      &bindings)
{
  list<knoten *> dummy;
  int i;
  switch (root->subtyp)
  {
    case 130 :   // name '(' expr_list ')'
      add_parameter(root->sub[1],type.params,bindings,
                    dummy, type.name, true);
      if (bindings.size()+dummy.size()<type.params.num)
        knot_error(cout <<"type " << type.name << " has too few parameters (" 
                   << type.params.num << " expected)\n",root)
      // no break
    case 131 :   // name
      if (root->sub[0]->subtyp==348) // name -> idop actuals ?
      // only possibility: actuals -> '[' actual_list ']'
      {
        int i=bindings.size();
        add_actual(root->sub[0]->sub[1]->sub[0],*type.p_actuals,
                   bindings,type.name,bindings.size()+type.p_actuals->num-1);
        if (bindings.size()-i<type.p_actuals->num)
          knot_error(cout <<"type " << type.name << " has too few actuals (" 
                     << type.p_actuals->num << " expected)\n",root)
      }
      else // no actuals
        if (type.p_actuals->num)
          knot_error(cout << "type " << type.name 
                     << " instantiated without actuals (" 
                     << type.p_actuals->num << " expected)\n",root)
      break;
    default:
      knot_error(printf("Aufruf von get_type_bindings mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

string get_type_name(const knoten *const root)
{
  switch (root->subtyp)
  {
    case 347 :   // idop
    case 348 :   // idop actuals
      if (root->sub[0]->subtyp==331) // idop -> ID ?
        return root->sub[0]->sub[0]->wert_str;
      break;
    default:
      knot_error(printf("Aufruf von get_type_name mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_defined_function(const knoten     *const root,
                          defined_function &function)
{
  switch (root->subtyp)
  {
    case 167 :   // expr funarg
      get_defined_function(root->sub[0],function);
      break;
    case 159 :   // name
      switch (root->sub[0]->subtyp)
      {
        case 347 :   // idop
        case 348 :   // idop actuals
          if (root->sub[0]->sub[0]->subtyp==331) // idop -> ID ?
            if (!is_function_defined(root->sub[0]->sub[0]->sub[0]->wert_str,function))
              knot_error(cout << "function " << root->sub[0]->sub[0]->sub[0]->wert_str
                              << " not defined\n",root)
          break;
        default:
          knot_error(printf("Aufruf von get_defined_function mit unzulaessigem Subtyp\n"),root);
          break;
      }
      break;
    default:
      knot_error(printf("Aufruf von get_defined_function mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_default_type(const string &name,
                      const knoten *const root,
                      type_array   &tarray)
{
  list<binding> bindings;
  list<knoten *>params;
  switch (root->subtyp)
  {
    case 130 :   // name '(' expr_list ')'
      if (name=="below"  || name=="upto"  || name=="subrange")
      {
        params_array dummy;
        dummy.add_param("a",0);
        dummy.add_param("b",0);
    
        add_parameter(root->sub[1],dummy,bindings,params,name,true);
        if (!tarray.add_member("", bounded_nat,0,
                               name=="subrange"? bindings.front().value: 0,
                               name=="below"? bindings.back().value-1:
                               bindings.back().value))
          knot_error(cout << "record type " << tarray << " too complex!", root);
      }
      else
        if (name=="upfrom" || name=="above")
	{
          if (!tarray.add_member("", unbounded_nat))
            knot_error(cout << "record type " << tarray << " too complex!", root);
        }
        else
          knot_error(cout << "unbekannter Typ " << name << "!\n",root)
      break;
    case 131 :   // name
      if (name=="nat"    || name=="int"   || name=="posnat" || name=="posint")
      {
        if (!tarray.add_member("", unbounded_nat))
          knot_error(cout << "record type " << tarray << " too complex!", root);
      }
      else
        if (name=="bool" || name=="bit")
	{
          if (!tarray.add_member("", bitvector))
            knot_error(cout << "record type " << tarray << " too complex!", root);
	}
        else
          if (name=="bvec")
            if (root->sub[0]->subtyp==348)  // idop actuals
            {
              actuals_array dummy;
              dummy.add_actual("von bvec");
              add_actual(root->sub[0]->sub[1]->sub[0],dummy,bindings,"bvec",0);
              if (!tarray.add_member("", bitvector, bindings.front().value))
                knot_error(cout << "record type " << tarray << " too complex!", root)
            }
            else
	      knot_error(cout << "bvec ohne actuals!\n",root)
          else
            knot_error(cout << "unbekannter Typ " << name << "!\n",root)	    
      break;
    default:
      knot_error(printf("Aufruf von get_default_type mit unzulaessigem Subtyp\n"),root);
  }
}

void add_record_field(const knoten *const root,
                      const knoten *const type_expression,
                      type_array   &tarray)
{
  type_array tmp;
  switch (root->subtyp)
  {
    case 333 :   // ID
      get_type(type_expression,tmp);
      if (!tarray.add_member(root->sub[0]->wert_str,tmp))
        knot_error(cout << "record type " << tarray << " too complex!", root);
      break;
    case 334 :   // ID ',' ids
      get_type(type_expression,tmp);
      if (!tarray.add_member(root->sub[0]->wert_str,tmp))
        knot_error(cout << "record type " << tarray << " too complex!", root);
      add_record_field(root->sub[1],type_expression,tarray);
      break;
    default:
      knot_error(printf("Aufruf von add_record_field mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_record_type(const knoten *const root,
                     type_array   &tarray)
{
  switch (root->subtyp)
  {
    case 149 :   // field_decls
      add_record_field(root->sub[0]->sub[0],root->sub[0]->sub[1],tarray);
      break;
    case 150 :   // field_decls_list ',' field_decls
      get_record_type(root->sub[0],tarray);
      add_record_field(root->sub[1]->sub[0],root->sub[1]->sub[1],tarray);
      break;
    default:
      knot_error(printf("Aufruf von get_record_type mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_type(const knoten *const root,
              type_array   &tarray)
{
  type_array left_side,right_side;
  string name;
  defined_type type;
  list<binding> bindings;
  switch (root->subtyp)
  {
    case 130 :   // name '(' expr_list ')'
    case 131 :   // name
      name=get_type_name(root->sub[0]);
      if (is_type_defined(name,type))
      {
        get_type_bindings(root,type,bindings);
        if (type.root)
          get_type_with_bindings(type.root,bindings,tarray);
	else
	{
	  if (parameter_verbose)
	    cout << "synthesizing uninterpreted type " << name << endl;
	  tarray.empty();
	  tarray.add_member("",ram,0,0,0,0);
        }
      }
      else
        get_default_type(name,root,tarray);
      break;
    case 132 :   // type_expr_sans_name
      if (root->sub[0]->subtyp==136) // comp_type_expr
        switch(root->sub[0]->sub[0]->subtyp)
        {
	  case 137 : // recordtype
            // only possibility:
            // recordtype -> ECKKLAMMERAUF_RAUTE field_decls_list RAUTE_ECKKLAMMERZU
            get_record_type(root->sub[0]->sub[0]->sub[0]->sub[0],tarray);
            break;
          case 138 : // '[' dep_type_expr_list MINUS_GROESSER type_expr ']'
            // TODO:
            // add support for "bounded_nat -> type_expr"
            if (root->sub[0]->sub[0]->sub[0]->subtyp!=146) // dep_type_expr
              knot_error(cout << "only 'dep_type_expr_list -> dep_type_expr' supported", root);
            if (root->sub[0]->sub[0]->sub[0]->sub[0]->subtyp!=154) // type_expr
              knot_error(cout << "only 'dep_type_expr->type_exp' supported", root);
            // synthesize the left-hand side of the function type
            get_type(root->sub[0]->sub[0]->sub[0]->sub[0]->sub[0],left_side);
	    
            // only simple type on the left side (no records)
            if (left_side.num!=1)
              knot_error(cout << "only simple types on left side of function types supported", root);
            // get the right side
            get_type(root->sub[0]->sub[0]->sub[1],right_side);
            switch (left_side.type[0])
            {
              // ram (left-side = bvec)
	      case bitvector:
                if (right_side.num!=1 || right_side.name[0]!="" || right_side.type[0]!=bitvector)
                  knot_error(cout << "only bvec -> bvec as ram type supported", root);
                tarray.make_ram(right_side,left_side.bitbreite[0]);
                break;
  	      case bounded_nat:
                if (!tarray.make_array(right_side,left_side.lower_bound[0],left_side.upper_bound[0]))
                  knot_error(cout << "record type " << tarray << " too complex!", root);
		break;
	      default:
                knot_error(cout<<"only bonded_nat -> type or bvec->bvec supported",root);
	    }
            break;
	    case 142: // '[' dep_type_expr_list ']'
	      knot_error(cout << "tuple types not supported\n",root)
          default:
            knot_error(printf("Aufruf von get_type mit unzulaessigem Subtyp\n"),root)	
        }
      else
        knot_error(cout << "nur 'type_expr_sans_name->comp_type_expr' unterstützt!\n",root)
      break;
    default:
      knot_error(printf("Aufruf von get_type mit unzulaessigem Subtyp\n"),root);
      break;
  }
}

void get_type_with_bindings(const knoten        *const root,
                            const list<binding> &bindings,
                            type_array          &tarray)
{
  knoten *copy=simplify_tree(root,bindings);
  get_type(copy, tarray);
  knoten_speicherfreigeben(copy);
}