/**CFile*******************************************************************
  PackageName [ccs]
  Synopsis    [Package 'ccs' provides an extended CCS parser.]

  FileName    [ccsTcl.c]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File ccsTcl.c contains definitions of Tcl commands,
               which can be used for manipulating from Tcl interpreter
               (e.g. tclsh or wish).]
  SeeAlso     [ccs.h, ccsInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "ccsInt.h"
#include "ccsDecls.h"

#include <tcl.h>

extern CcsStubs ccsStubs;
extern CONST char *Gui_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Bdd_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Pa_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Versis_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Mc_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Strucval_InitStubs (Tcl_Interp *interp, char *version, int exact);

/* on tcl 8.3 use #define USECONST */
/* on tcl 8.4 use #define USECONST const*/
/* this is defined in Makefile */

/*-----------------------------------------------------------------------*/
/* Constant declarations                                                 */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

static int CcsInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int CcsExitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int CcsAboutPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int CcsReadCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int CcsConvertVerilogCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function Versis_TclInit.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

#ifdef __cplusplus
extern "C" {
#endif

int
Ccs_Init(Tcl_Interp *interp)
{

#ifdef USE_TCL_STUBS
  if (Tcl_InitStubs(interp, "8.1", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_GUI_STUBS
  if (Gui_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_BDD_STUBS
  if (Bdd_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_PA_STUBS
  if (Pa_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_VERSIS_STUBS
  if (Versis_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_MC_STUBS
  if (Mc_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_STRUCVAL_STUBS
  if (Strucval_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

  Tcl_CreateCommand(interp, "ccs_initPkg", CcsInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "ccs_exitPkg", CcsExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "ccs_aboutPkg", CcsAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "ccs_read", CcsReadCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "ccs_convert_verilog", CcsConvertVerilogCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-ccs", "1.0", &ccsStubs);
}

#ifdef __cplusplus
}
#endif

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function CcsInitPkgCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
CcsInitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Initialization of CCS package... ");
  Ccs_InitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

/**Function****************************************************************
  Synopsis    [Function CcsExitPkgCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
CcsExitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Exit CCS package... ");
  Ccs_ExitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

/**Function****************************************************************
  Synopsis    [Function CcsAboutPkgCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
CcsAboutPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                       USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  Ccs_AboutPkg();

  printf("DEBUG: FALSE = %x, TRUE = %x\n",FALSE,TRUE);
  printf("DEBUG: bdd_termTrue = (%p, %x)\n",bdd_termTrue.p,bdd_termTrue.mark);
  printf("DEBUG: bdd_termFalse = (%p, %x)\n",bdd_termFalse.p,bdd_termFalse.mark);
  printf("DEBUG: bdd_termNull = (%p, %x)\n",bdd_termNull,bdd_termNull.mark);
  printf("\n");

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

/**Function****************************************************************
  Synopsis    [Function CcsReadCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
CcsReadCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String s1,s2;
  Est_Boolean q;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  q = FALSE;

  s1 = strdup(argv[1]);

  if (argc == 3) {
    s2 = strdup(argv[2]);
    q = (atoi(s2) == 0);
    free(s2);
  }

  printf("Reading file: %s",s1);
  Ccs_ParseCCS(s1,q);

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

/**Function****************************************************************
  Synopsis    [Function CcsReadCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
CcsConvertVerilogCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String s1,s2;

  if (argc != 3) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  printf("Reading file: %s",s1);
  Ccs_ConvertVerilog(s1,s2);

  free(s1);
  free(s2);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}
