/* 
$Id: types_and_functions_core.cpp,v 1.12 2002/12/02 14:36:58 sbeyer Exp $
$Log: types_and_functions_core.cpp,v $
Revision 1.12  2002/12/02 14:36:58  sbeyer
* ported source to gcc-3.2 (still compiles AND WORKS with gcc-2.9x)

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

Revision 1.10  2002/03/21 13:54:54  dirkl
*** empty log message ***

Revision 1.9  2001/06/12 10:05:34  sbeyer
* added support for uninterpreted functions (+warning)

Revision 1.8  2001/01/25 13:06:52  sbeyer

cosmetical adjustments

Revision 1.7  2001/01/18 16:02:51  sbeyer

small bugfixes

Revision 1.6  2001/01/15 16:07:48  sbeyer

small bugfixes

Revision 1.5  2001/01/13 17:00:30  sbeyer

added brief pass-1 summary

Revision 1.4  2001/01/12 16:24:50  sbeyer

C++-files now use 'class string' instead of 'char *'-stuff

Revision 1.3  2001/01/12 09:27:31  sbeyer

added support for overload detection in parameters/actuals
(parameter/actuals names for any function/type must be unique)
made compse_path recursive (now supports all relative paths)

Revision 1.2  2001/01/11 16:34:24  sbeyer

fixed bug in variables support

Revision 1.1  2001/01/11 16:25:27  sbeyer

split types_and_functions (about 900 lines) into the 3 files
    types_and_functions_add
    types_and_functions_core
    types_and_functions_libs

*/
#include "shared_lists.h"
#include "types_and_functions.h"
#include "types_and_functions_core.h"
#include "types_and_functions_add.h"
#include "tools.h"
#include "synthesize_core.h"
#include <cstdio>

using namespace std;

string root_file_name;
string root_path;

void add_actual(knoten* knot, actuals_array&
				theory_actuals)
{
  switch (knot->subtyp)
  {
    case 329 :   // idop
      if (knot->sub[0]->subtyp==332) // opsym
      {
        knot_error(printf("Nur ID als Theory Actual idop unerstuetzt, nicht opsym!\n"),knot);
      }
      if (theory_actuals.is_actual(knot->sub[0]->sub[0]->wert_str))
      {
        knot_error(printf("%s ist als Theory Actual ueberladen!\n",
                          knot->sub[0]->sub[0]->wert_str),knot);
      }
      theory_actuals.add_actual(knot->sub[0]->sub[0]->wert_str);
      if (parameter_verbose)
        printf("Theory Actual: %s\n",knot->sub[0]->sub[0]->wert_str);
      break;
    case 330 :   // idops ',' idop
      add_actual(knot->sub[0],theory_actuals);
      if (knot->sub[1]->subtyp==332) // opsym
      {
        knot_error(printf("Nur ID als Theory Actual idop unerstuetzt, nicht opsym!\n"),knot);
      }
      if (theory_actuals.is_actual(knot->sub[1]->sub[0]->wert_str))
      {
        knot_error(printf("%s ist als Theory Actual ueberladen!\n",
                          knot->sub[1]->sub[0]->wert_str),knot);
      }
      theory_actuals.add_actual(knot->sub[1]->sub[0]->wert_str);
      if (parameter_verbose)
        printf("Theory Actual: %s\n",knot->sub[1]->sub[0]->wert_str);
      break;
    default:
      knot_error(printf("Aufruf von add_actual mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

void add_actuals(knoten* knot, actuals_array&
                 theory_actuals)
{
  switch (knot->subtyp)
  {
    case 37 :   // '(' importing ')' idops ':' theoryformaldecl
      add_actual(knot->sub[1],theory_actuals);
      break;
    case 38 :   // idops ':' theoryformaldecl
      add_actual(knot->sub[0],theory_actuals);
      break;
    default:
      knot_error(printf("Aufruf von add_actual mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

void generate_actuals_array(knoten* knot, actuals_array&
                            theory_actuals)
{
  switch (knot->subtyp)
  {
    case 35 :   // theoryformal
      add_actuals(knot->sub[0],theory_actuals);
      break;
    case 36 :   // theoryformal_list ',' theoryformal
      generate_actuals_array(knot->sub[0],theory_actuals);
      add_actuals(knot->sub[1],theory_actuals);
      break;
    default:
      knot_error(printf("Aufruf von generate_actuals_array mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

struct imported_theory
{
  string name;
  actuals_array theory_actuals;
  string lib;

  imported_theory()
    { memset(this,0,sizeof(*this));}

  imported_theory(const string &_name, 
                  const actuals_array& _theory_actuals, 
                  const string &_lib)
  { name=_name; theory_actuals=_theory_actuals; lib=_lib; }
};

list<imported_theory> imported_theories;

bool is_theory_imported(const parsed_theory& parsed_theo)
{
  list<imported_theory>::iterator i=imported_theories.begin();
  while (i!=imported_theories.end())
  {
    if (i->name==parsed_theo.name &&
        i->lib ==parsed_theo.lib)
      return true;
    i++;
  }
  return false;
};

void import_theory_element(const knoten *knot, 
                           const actuals_array &theory_actuals,
                           list<defined_lib> &libs,
                           list<defined_var> &vars,
                           const string &path,
                           bool is_root)
{
  params_array params;
  if (parameter_verbose)
    printf("theory_element vom Subtyp %d wird importiert\n", knot->subtyp);
  
  string tmp;
  switch (knot->subtyp)
  {
    case 71: // importing ';'
    case 72: // importing
      if (parameter_verbose)
        printf("Verfolge Importings...\n");
      import_importings(knot->sub[0]->sub[0],libs,path);
      break;
    case 73: // judgement
    case 74: // judgement ';'
    case 75: // conversion
    case 76: // conversion ';'
      if (parameter_verbose)
        printf("Subtyp %d wird ignoriert\n", knot->subtyp);
      break;
    case 77: // idops pdformals_stern ':' theory_decl ';'
      if (parameter_verbose)
        printf("Importiere theory_decl vom Subtyp %i...\n",knot->sub[2]->subtyp);
      switch (knot->sub[2]->subtyp)
      {
          case  99: // lib_decl
          // cut the ' from beginning of string and from the end
          tmp=string(knot->sub[2]->sub[0]->sub[0]->wert_str,1,
                     strlen(knot->sub[2]->sub[0]->sub[0]->wert_str)-2);
          // append the "/" in case it isn't already there
          if (tmp[tmp.length()-1]!='/')
            tmp += '/';
          add_lib_decl(knot->sub[0],tmp,libs);
          break;
        case 101: // type_decl
          switch (knot->sub[2]->sub[0]->subtyp)
          {
          case 113: // type_keyword
            get_pdformals_stern(knot->sub[1],theory_actuals,params,vars);
            add_type(knot->sub[0],                         // idops
                     NULL,                                 // type_expr
                     theory_actuals,
                     params);
            break;
	    //            if (parameter_verbose)
	    //              printf("Uninterpretierter Typ in Datei %s, Zeile %d wird ignoriert!\n",
	    //                     knot->sub[2]->sub[0]->source_file,
	    //                     knot->sub[2]->sub[0]->source_line);
            break;
          case 114: // type_keyword type_def
          case 115: // type_keyword type_def CONTAINING expr
            get_pdformals_stern(knot->sub[1],theory_actuals,params,vars);
            add_type(knot->sub[0],                         // idops
                     knot->sub[2]->sub[0]->sub[1]->sub[0], // type_expr
                     theory_actuals,
                     params);
            break;
          default:
            knot_error(printf("type_decl in import_theory_element hat unzulaessigem Subtyp\n"),knot);
            break;
          }

          break;
        case 103: // const_decl
          switch (knot->sub[2]->sub[0]->subtyp)
          {
          case 122: // type_expr
            get_pdformals_stern(knot->sub[1],theory_actuals,params,vars);
            add_function(knot->sub[0],                         // idops
                         0,                                    // expr 
                         knot->sub[2]->sub[0]->sub[0],         // return type_expr
                         theory_actuals,
                         params,
                         false);
            break;
          case 123: // type_expr const_value
            get_pdformals_stern(knot->sub[1],theory_actuals,params,vars);
            add_function(knot->sub[0],                         // idops
                         knot->sub[2]->sub[0]->sub[1]->sub[0], // expr 
                         knot->sub[2]->sub[0]->sub[0],         // return type_expr
                         theory_actuals,
                         params,
                         is_root);
            break;
          default:
            knot_error(printf("const_decl in import_theory_element hat unzulaessigem Subtyp\n"),knot);
            break;
          }
          break;
        case 104: // def_decl
          get_pdformals_stern(knot->sub[1],theory_actuals,params,vars);
          add_function(knot->sub[0],                 // idops
                       knot->sub[2]->sub[0]->sub[1], // expt
                       knot->sub[2]->sub[0]->sub[0], // return type_expr
                       theory_actuals,
                       params,
                       false);
          break;
        case 102: // var_decl
          add_var(knot->sub[0],                 // idops
                  knot->sub[2]->sub[0]->sub[0], // type_expr
                  vars);
          break;
        case 100: // mod_decl
        case 105: // ind_decl
        case 106: // formula_decl
        case 107: // datatype
        case 108: // judgement
          if (parameter_verbose)
            printf("theory_decl vom Subtyp %i wird ignoriert...\n",knot->sub[2]->subtyp);
          break;
        default:
          knot_error(printf("theory_decl in import_theory_element hat unzulaessigem Subtyp\n"),knot);
         break;
      }

      break;
    default:
      knot_error(printf("Aufruf von import_theory_element mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

void import_theory_elements(const knoten *knot,
                            const actuals_array &theory_actuals,
                            list<defined_lib> &libs,
                            list<defined_var> &vars, 
                            const string &path, 
                            bool is_root)
{  
  switch (knot->subtyp)
  {
    case 69 :   // theory_elt
      import_theory_element(knot->sub[0],theory_actuals,libs,vars,path,is_root);
      break;
    case 70 :   // theory_part theory_elt
      import_theory_elements(knot->sub[0],theory_actuals,libs,vars,path,is_root);
      import_theory_element(knot->sub[1],theory_actuals,libs,vars,path,is_root);
      break;
    default:
      knot_error(printf("Aufruf von import_theory_elements mit unzulaessigem Subtyp\n"),knot);
      break;
  }  
}

void import_theory(const parsed_theory& parsed_theo, bool is_root)
{
  if (parameter_verbose)
    cout << "\nImportiere Theorie " << parsed_theo.name
         << " aus Library " << parsed_theo.lib << "...\n";
  if (is_theory_imported(parsed_theo))
  {
    if (parameter_verbose)
      printf("ist bereits importiert; wird ignoriert!\n");
    return;
  }
  
  // generate the theory's actuals
  actuals_array theory_actuals;
  knoten* theo_or_data;
  
  switch (parsed_theo.root->subtyp)
  {
    case 2 :   // ID ':' theory_or_datatype
      if (parameter_verbose)
        printf("Theorie hat keine Actuals!\n");
      theo_or_data=parsed_theo.root->sub[1];
      break;
    case 3 :   // ID theoryformals ':' theory_or_datatype
      if (parameter_verbose)
        printf("Actuals der Theorie:\n");
      generate_actuals_array(parsed_theo.root->sub[1]->sub[0],theory_actuals);
      theo_or_data=parsed_theo.root->sub[2];
      break;
    default:
      knot_error(printf("Aufruf von import_theory mit unzulaessigem Subtyp\n"),parsed_theo.root);
      break;
  }

  // add theory with actuals to imported theories
  imported_theories.push_back(imported_theory(parsed_theo.name,
                                              theory_actuals,
                                              parsed_theo.lib));

  const actuals_array &ref_to_theory_actuals = imported_theories.back().theory_actuals;
  
  if (theo_or_data->subtyp==5) // datatype
  {
    if (parameter_verbose)
      cout << "Theorie " << parsed_theo.name
           << " aus Library " << parsed_theo.lib
           << " ist Datatype; wird nicht weiter verfolgt\n";
    return;
  }

  knoten* theo_part;
  
  switch (theo_or_data->sub[0]->subtyp)
  {
    case  6: // THEORY BEGINN END ID
    case  8: // THEORY BEGINN assumingpart END ID
    case 10: // THEORY exporting BEGINN END ID
    case 12: // THEORY exporting BEGINN assumingpart END ID
      if (parameter_verbose)
        cout << "Theorie " << parsed_theo.name
             << " aus Library " << parsed_theo.lib
             << " enthaelt keinen theory_part; wird nicht weiter verfolgt\n";
      return;
    case  7: // THEORY BEGINN theory_part END ID
      theo_part=theo_or_data->sub[0]->sub[0];
      break;
    case  9: // THEORY BEGINN assumingpart theory_part END ID
      theo_part=theo_or_data->sub[0]->sub[1];
      break;
    case 11: // THEORY exporting BEGINN theory_part END ID
      theo_part=theo_or_data->sub[0]->sub[1];
      break;
    case 13: // THEORY exporting BEGINN assumingpart theory_part END ID
      theo_part=theo_or_data->sub[0]->sub[2];
      break;
    default:
      knot_error(printf("theory in import_theory hat unzulaessigen Subtyp\n"),theo_or_data);
      break;
  }

  list<defined_lib> libs;
  list<defined_var> vars;
  
  import_theory_elements(theo_part, ref_to_theory_actuals, libs, vars,
						 parsed_theo.lib,is_root);

  if (parameter_verbose)
    cout << "Theorie " << parsed_theo.name
         << " aus Library " << parsed_theo.lib
         << " vollstaendig importiert!...\n\n";
}

// returns pvs_fileinfo
void generate_type_and_function_lists(const char* name)
{
  cout << "pass 1: parsing files, importing theories and searching for defined types and functions...\n";
  // treatment of relative paths
  const char* tmp;
  if (tmp=strrchr(name,'/'))
  {
    tmp++;
    root_path=string(name,0,tmp-name);
  }
  else
  {
    tmp=name;
    root_path="./";
  }
  if (parameter_verbose)
    cout << "Pfad " << root_path << ", Datei " << tmp << endl;
  root_file_name=root_path+tmp;  
  parse_file(root_path.c_str(),name);
  // the list of parsed theories will grow by
  // importing => import only current list content
  list<parsed_theory>::iterator i=parsed_theories.begin();
  int num=parsed_theories.size();
  for (int j=0; j<num; j++,i++)
    import_theory(*i,true);
  // give brief import summary
  cout << "\t" << parse_trees.size() << " files parsed (containing "
       << parsed_theories.size() << " theories)\n";
  cout << "\t" << imported_theories.size() << " theories imported (containing "
       << defined_types.size() << " defined types and "
       << defined_functions.size() << " defined functions)\n";
  cout << "\t" << root_functions.size() << " functions of the root file seem to be synthesizeable...\n";

  /*  
  if (parameter_verbose)
  {
    int j;
    printf("\nListe der definerten Typen:\n");
    list<defined_type>::const_iterator i=defined_types.begin();
    while (i!=defined_types.end())
    {
      cout << *i++;
    }

    printf("\nListe der definerten Funktionen:\n");
    list<defined_function>::const_iterator k=defined_functions.begin();
    while (k!=defined_functions.end())
    {
      cout << *k++;
    }

    printf("\nListe der (vermutlich) synthetisierbaren Funktionen:\n");
    k=root_functions.begin();
    while (k!=root_functions.end())
    {
      cout << "\tName: " << k->name << endl;
      k++;
    }
  }
  */
}

void free_parse_trees()
{
  list<parse_tree>::iterator i=parse_trees.begin();
  if (parameter_verbose)
    printf("alle %i Parsetrees freigeben...\n",parse_trees.size());
  while (i!=parse_trees.end())
    knoten_speicherfreigeben(i++->root);
}