/* 
$Id: types_and_functions_libs.cpp,v 1.14 2005/01/19 10:24:21 mah Exp $
$Log: types_and_functions_libs.cpp,v $
Revision 1.14  2005/01/19 10:24:21  mah
New command-line option --cvs-status to add `cvs status' information.
This information was always enabled before but this was too annoying if there
is no cvs information available.

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

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

Revision 1.11  2001/11/14 09:38:16  dirkl
- removed compose_path bug : "./../fpu/" + "../../pvsctl" was composed to "./pvsctl" , now is composed to "./../../pvsctl"

Revision 1.10  2001/06/22 10:28:30  dirkl
- prepared new config-file format
- excluded context pvsctl

Revision 1.9  2001/05/31 07:45:32  dirkl
- minor changes

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

Revision 1.7  2001/01/25 13:41:55  sbeyer

for compatibility's sake replaced gl_matchc by gl_pathc in struct glob_t

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

cosmetical adjustments

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

small bugfixes

Revision 1.4  2001/01/15 15:13:00  sbeyer

cosmetic changes

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

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

Revision 1.2  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.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 "types_and_functions_libs.h"
#include "types_and_functions_core.h"
#include "tools.h"
#include <cstdio>
#include <glob.h>
#include "synthesize_core.h"

using namespace std;

list<parse_tree> parse_trees;
list<parsed_theory> parsed_theories;

bool is_theory_parsed(const string &name,
                      const string &lib, 
                      parsed_theory &parsed_theo)
{
  list<parsed_theory>::iterator i=parsed_theories.begin();
  while (i!=parsed_theories.end())
  {
    if (i->name==name && i->lib ==lib)
    {
      parsed_theo=*i;
      return true;
    }
    i++;
  }
  return false;
};

void add_to_parsed_theories(const knoten *knot, const string &lib)
{
  switch (knot->subtyp)
  {
    case 0 :   // adt_or_theory 
      if (parameter_verbose)
        cout << "Theorie " << knot->sub[0]->sub[0]->wert_str 
             << " aus Kontext " << lib
             << " ist geparst\n";
      parsed_theories.push_back(parsed_theory(knot->sub[0]->sub[0]->wert_str,lib,knot->sub[0]));
      break;
    case 1 :   // adt_or_theories adt_or_theory
      add_to_parsed_theories(knot->sub[0],lib);
      if (parameter_verbose)
        cout << "Theorie " << knot->sub[1]->sub[0]->wert_str 
             << " aus Kontext " << lib
             << " ist geparst\n";
      parsed_theories.push_back(parsed_theory(knot->sub[1]->sub[0]->wert_str,lib,knot->sub[1]));
      break;
    default:
      knot_error(printf("Aufruf von add_to_parsed_theories mit unzulaessigem Subtyp\n"),knot);
      break;
  }  
};

// gives info about pvs-file
int parameter_cvs_status;
string get_fileinfo(const string &name)
{
  FILE* pipe;
  char buf[512];
  string ret="";
  if( parameter_cvs_status ) {
	  pipe=popen(("cvs status "+name).c_str(), "r");
	  while(!feof(pipe))
	  {
		  if (fgets(buf, 511, pipe))
			  ret=ret+"// "+buf;
	  }
	  pclose(pipe);
  }
  pipe=popen(("cksum "+name).c_str(), "r");
  while(!feof(pipe))
    {
      if (fgets(buf, 511, pipe))
	ret=ret+"// cksum: "+buf;
    }
  pclose(pipe);
  return ret;
}

// return parameter : info about the pvs-file (laste change, filename ...)
void parse_file(const string &lib, const string &name)
{
  parse_trees.push_back(parse_tree(0,name));
  // add info about the file to pvs_fileinfo
  pvs_fileinfo+=get_fileinfo(parse_trees.back().name);

  // call pvs_parser with name in parse_trees-list!
  parse_trees.back().root=pvs_parser(parse_trees.back().name.c_str());
  if (parameter_gdlausgabe) gdl_ausgabe("parse_tree.gdl",parse_trees.back().root);
  add_to_parsed_theories(parse_trees.back().root, lib);
};

void compose_path(const string &path, 
                  const string &path_part_2,
                        string &comp_path)
{
  // absolute path is easy
  if (path_part_2[0]=='/')
    comp_path=path_part_2;
  else
  // compose correct relative path
    if (path_part_2[0]=='.' && path_part_2[1]=='.' &&
        path.find('/')!=path.length()-1 
	&& path[path.length()-2]!='.')
    // translate '..' directory if it can be
    // translated (ie. path contains >= 2 '/'-characters && last part of path is NOT /../ )
    {
      // cut after last but one '/'
      string tmp=string(path,0,path.rfind('/',path.length()-2)+1);
      // and the obvious recursive call... (cut leading "../" in path_part2)
      compose_path(tmp,path_part_2.c_str()+3,comp_path);
      return;
    }
    else
    {
      comp_path=path + path_part_2;
    }
  if (parameter_verbose)
    cout << "composed path: " << comp_path << endl;
};

bool is_lib_defined(const string &name,
                    const string &path,
                          string &comp_path,
                    list<defined_lib> libs)
{
  list<defined_lib>::const_iterator i=libs.begin();
  while (i!=libs.end())
  {
    if (i->name==name)
    { 
      compose_path(path,i->path,comp_path);
      return true;
    }
    i++;
  }
  return false;
};

void import_it(const string &path, const string &name)
{
  // check if path is to be ignored
  if (path==string(pvs_path) + "/lib/bitvectors/" ||
      path==string(pvs_path) + "/lib/finite_sets/" ||
      path=="./../../pvsctl/")

  {
    if (parameter_verbose)
      cout << "Library " << path
           << " wird ignoriert...\n";
    return;
  }
  if (parameter_verbose)
    cout << "Theory " << name
         << " aus Kontext " << path
         << " wird gesucht...\n";
  parsed_theory parsed_theo;
  if (!is_theory_parsed(name,path,parsed_theo))
  {
    // get all pvs files in context
    string pattern=path + "*.pvs";
    glob_t glob_ret;
    if (parameter_verbose)
      cout << "Suche mit Pattern " << pattern << "...\n";
    if (glob(pattern.c_str(),0,0,&glob_ret))
    {
      globfree(&glob_ret);
      raise_error(printf("Fehler beim Aufruf von glob; Verarbeitung abgebrochen!\n"));
    }
    if (parameter_verbose)
      printf("Kontext enthaelt %i Datei(en), die geparst werden...\n",glob_ret.gl_pathc);
    // now parse all these files
    for (int i=0; i<glob_ret.gl_pathc;i++)
    {
      if (path!=root_path || glob_ret.gl_pathv[i]!=root_file_name)
      {
        parse_file(path,glob_ret.gl_pathv[i]);
      }        
      else
        if (parameter_verbose)
          cout << "Root-File " << root_file_name
               << " wird nicht nochmal geparst!\n";
    }        
      
    // finally, free the file names
    globfree(&glob_ret);
  }
  if (is_theory_parsed(name,path,parsed_theo))
  {
    if (is_theory_imported(parsed_theo))
    {
      if (parameter_verbose)
        printf("ist bereits importiert, wird ignoriert!\n");
      return;
    }
    import_theory(parsed_theo);
  }
  else
  {
    raise_error(cout << "Theorie " << name
		     << " aus Kontext " << path
		     << " nicht gefunden, Programmabbruch!\n");
  }           
}

void import_importing(const knoten *knot,
                      list<defined_lib> &libs,
                      const string &path)
{
  string comp_path;
  switch (knot->subtyp)
  {
    case 310: // IDAT ID
    case 311: // IDAT ID actuals
    case 312: // IDAT ID mappings
    case 313: // IDAT ID actuals mappings
      if (!strcmp(knot->sub[0]->wert_str,"bitvectors@") || 
          !strcmp(knot->sub[0]->wert_str,"finite_sets@") )
      {
        if (parameter_verbose)
          printf("Theorie %s aus Library %s wird ignoriert...\n",
                 knot->sub[1]->wert_str,knot->sub[0]->wert_str);
      }
      else
        if (is_lib_defined(knot->sub[0]->wert_str,path,comp_path,libs))
          import_it(comp_path,knot->sub[1]->wert_str);
        else
        {
          knot_error(printf("Library %s undefiniert, Uebersetzung abgebrochen\n",knot->sub[0]->wert_str),knot);
        }
      break;
    case 314: // ID
    case 315: // ID actuals
    case 316: // ID mappings
    case 317: // ID actuals mappings
      import_it(path,knot->sub[0]->wert_str);
      break;
    default:
      knot_error(printf("Aufruf von import_importing mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

void import_importings(const knoten *knot,
                      list<defined_lib> &libs,
                      const string &path)
{
  switch (knot->subtyp)
  {
    case 79: // modname
      import_importing(knot->sub[0],libs,path);
      break;
    case 80: // modname_list ',' modname
      import_importings(knot->sub[0],libs,path);
      import_importing(knot->sub[1],libs,path);
      break;
    default:
      knot_error(printf("Aufruf von import_importings mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}

void add_lib_decl(knoten* knot, const string &path, list<defined_lib> &libs)
{
  switch (knot->subtyp)
  {
    case 329 :   // idop
      if (knot->sub[0]->subtyp==332) // opsym
      {
        knot_error(printf("Nur ID bei lib_decl idop unerstuetzt, nicht opsym!\n"),knot);
      }
      if (parameter_verbose)
        cout << "Definiere Library " << knot->sub[0]->sub[0]->wert_str
             << " in Pfad " << path
             << "...\n";
      libs.push_back(defined_lib(knot->sub[0]->sub[0]->wert_str,path));
      break;
    case 330 :   // idops ',' idop
      add_lib_decl(knot->sub[0],path,libs);
      if (knot->sub[1]->subtyp==332) // opsym
      {
        knot_error(printf("Nur ID bei lib_decl idop unerstuetzt, nicht opsym!\n"),knot);
      }
      if (parameter_verbose)
        cout << "Definiere Library " << knot->sub[1]->sub[0]->wert_str
             << " in Pfad " << path
             << "...\n";
      libs.push_back(defined_lib(knot->sub[1]->sub[0]->wert_str,path));
      break;
    default:
      knot_error(printf("Aufruf von add_lib_decl mit unzulaessigem Subtyp\n"),knot);
      break;
  }
}