/**CFile*******************************************************************
  PackageName [strucval]
  Synopsis    [Structure-driven validation of hardware and software systems]

  FileName    [strucvalTcl.h]
  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 strucvalTcl.c contains definitions of Tcl commands.]
  SeeAlso     [strucval.h, strucvalInt.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 "strucvalInt.h"
#include "strucvalDecls.h"

#include <tcl.h>

extern StrucvalStubs strucvalStubs;
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);

/* 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 StrucvalInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                        int argc, USECONST char **argv);

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

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

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

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

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

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

#ifdef __cplusplus
extern "C" {
#endif

int
Strucval_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

  Tcl_CreateCommand(interp, "strucval_initPkg", StrucvalInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "strucval_exitPkg", StrucvalExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "strucval_aboutPkg", StrucvalAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "strucval_sync_product", StrucvalSyncProductCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-strucval", "1.0", &strucvalStubs);
}

#ifdef __cplusplus
}
#endif

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

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

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

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

  printf("Initialization of Strucval package... ");
  Strucval_InitPkg();
  printf("OK");

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

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

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

  printf("Exit Strucval package... ");
  Strucval_ExitPkg();
  printf("OK");

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

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

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

  Strucval_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 StrucvalSyncProductCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

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

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  printf("Product %s... ",s1);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Strucval_SyncProduct_Thr(s1,s2,s3,s4);
#else
  Strucval_SyncProduct(s1,s2,s3,s4);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);
  free(s2);
  free(s3);
  free(s4);

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