#include <stdio.h>
#include <unistd.h>
#include <sys/types.h>
#include <signal.h>
#include <setjmp.h>
#include "pstgen.h"

typedef enum {
  IN,
  READ,
  GEN,
  CHECK,
  HELP,
  ERROR2, 
  FIN,
} TOKEN2 ;

#define MAX2 128

char Name[ MAX2 ] ;

typedef struct {
  TOKEN2 tk ;
  char *kwd ;
} KEYWORD2 ;

#define NumOfKeywords2 5

KEYWORD2 Keyword2[ NumOfKeywords2 ] = {
  { IN,    "in" },
  { READ,  "read" },
  { GEN,   "gen" },
  { CHECK, "check" },
  { HELP,  "help" },
} ;

void
skipSpaceAndTab( FILE *fp ) {
  int c ;
  while ( 1 ) {
    c = getc( fp ) ;
    if ( c != ' ' && c != '\t' ) {
      ungetc( c, fp ) ;
      return ;
    }
  }
}

void
skipTilCR( FILE *fp ) {
  int c ;
  while ( 1 ) {
    c = getc( fp ) ;
    if ( c == '\n' || c == EOF ) {
      return ;
    }
  }
}

#define CafeOBJPROMPT "CafeOBJ> "

void
skipTilString( FILE *fp, char *str ) {
  int c ;
  int i ;

  if ( str[ 0 ] == '\0' ) return ;
  /* skipTilCR( fp ) ; */
  while ( 1 ) {
    while ( 1 ) {
      c = getc( fp ) ;
      if ( c == EOF ) return ;
      if ( c == str[ 0 ] ) break ;
    }
    i = 0 ;
    while ( str[ ++i ] != '\0' ) {
      c = getc( fp ) ;
      if ( c == EOF ) return ;
      if ( c != str[ i ] ) break ;
    }
    if ( str[ i ] == '\0' ) return ;
  }
}

#define CafeOBJErrMsg "[Error]"

int
checkError( FILE *fp, char *str ) {
  int c ;
  int i ;

  for ( i = 0 ; i < strlen( str ) ; i++ ) {
    if ( (c = getc( fp )) == EOF ) return 0 ;
    if ( c != str[ i ] ) {
      ungetc( c, fp ) ;
      return 0 ;
    }
  }
  return 1 ;
}

TOKEN2
pascanner( FILE *fp ) {
  int c ;
  int cnt ;
  int i ;

  while ( (c = getc( fp )) != EOF ) {
    switch ( c ) {
    case ' ':
    case '\t' :
    case '\n' :
      break ;
    default:
      cnt = 0 ;
      do {
	Name[ cnt++ ] = c ;
	c = getc( fp ) ;
      } while ( c != ' ' && c != '\t' && c != '\n' && c != EOF ) ;
      ungetc( c, fp ) ;
      Name[ cnt ] = '\0' ;
      for ( i = 0 ; i < NumOfKeywords2 ; i++ ) {
	if ( !strcmp( Name, Keyword2[ i ].kwd ) ) {
	  switch ( i ) {
	  case IN:
	  case READ:
	  case GEN:
	    skipSpaceAndTab( fp ) ;
	    cnt = 0 ;
	    c = getc( fp ) ;
	    while ( c != ' ' && c != '\t' && c != '\n' && c != EOF ) {
	      Name[ cnt++ ] = c ;
	      c =getc( fp ) ;
	    }
	    ungetc( c, fp ) ;
	    skipTilCR( fp ) ;
	    Name[ cnt ] = '\0' ;
	    break ;
	  case CHECK:
	  case HELP:
	    skipTilCR( fp ) ;
	    break ;
	  default:
	    skipTilCR( fp ) ;
	    return ERROR2 ;
	  }
	  return Keyword2[ i ].tk ;
	}
      }
      skipTilCR( fp ) ;
      return ERROR2 ;
    }
  }
  return FIN ;
}  

int HaveScript = 0 ;

void
processGateauxScript( char *script ) {
  FILE *fp ;
  if ( (fp = fopen( script, "r" )) == NULL ) {
    fprintf( stderr, "No such file: '%s'\n", script ) ;
    return ;
  }
  initPstscanner( ) ;
  initPstparser( ) ;
  HaveScript = pstparser( fp ) ;
  /* printParseResults( ) ; */
  fclose( fp ) ;
}

void
generateProofScores( char *pscore ) {
  if ( !HaveScript ) {
    fprintf( stderr, "Not yet read any Gateaux script files!!!\n" ) ;
    return ;
  }
  if ( pscore[ 0 ] == '\0' ) {
    pstgenerator( stdout ) ;
  } else {
    FILE *fp ;
    if ( (fp = fopen( pscore, "w" )) == NULL ) {
      fprintf( stderr, "Cannot open '%s'\n" ) ;
      return ;
    }
    pstgenerator( fp ) ;
    fclose( fp ) ;
  }
}

int NumOfNonExpectedResults ;
int NumOfCases ;
jmp_buf CheckPSEnv ;
char RESULT[ MAX2 ] ;

void
getResult( FILE *fp, char *buf, int max ) {
  int c ;
  int i ;
  int flag ;

  skipTilString( fp, "-- reduce in " ) ;
  while ( 1 ) {
    skipTilCR( fp ) ;
    c = getc( fp ) ;
    if ( c != ' ' || c == EOF ) {
      ungetc( c, fp ) ;
      break ;
    }
  }
  flag = 0 ;
  i = 0 ;
  while ( i < max ) {
    c = getc( fp ) ;
    if ( c == ':' || c == EOF ) break ;
    if ( c == ' ' || c == '\n' || c == '\t') {
      if ( !flag ) {
	buf[ i++ ] = ' ' ;
	flag = 1 ;
      }
    } else {
      buf[ i++ ] = c ;
      flag = 0 ;
    }
  }
  buf[ i - 1 ] = '\0' ;
}

#define ExpectedResult "true"

void
checkBase( FILE *outfp, FILE *infp ) {
  fprintf( outfp, "open INV\n" ) ;
  fflush( outfp ) ;
  if ( checkError( infp, CafeOBJErrMsg ) ) {
    fprintf( stderr, "No module 'INV'\n" ) ;
    skipTilString( infp, CafeOBJPROMPT ) ;
    longjmp( CheckPSEnv, 1 ) ;
  }
  skipTilString( infp, "%INV> " ) ;
  fprintf( outfp, "red %s .\n", BasePred ) ;
  fflush( outfp ) ;
  if ( checkError( infp, CafeOBJErrMsg ) ) {
    fprintf( stderr, "Error in Base case: 'red %s .'\n", BasePred ) ;
    fprintf( outfp, "close\n" ) ;
    skipTilString( infp, CafeOBJPROMPT ) ;
    longjmp( CheckPSEnv, 1 ) ;
  }
  getResult( infp, RESULT, MAX2 ) ;
  /* printf( "Result: %s\n", RESULT ) ; */
  if ( strcmp( RESULT, ExpectedResult ) ) {
    NumOfNonExpectedResults++ ;
    fprintf( stdout, "Not expected: Base case\n" ) ;
    fprintf( stdout, "Result: %s\n", RESULT ) ;
  } else {
    putc( '.', stdout ) ;
    fflush( stdout ) ;
  }
  fprintf( outfp, "close\n" ) ;
  fflush( outfp ) ;
  skipTilString( infp, CafeOBJPROMPT ) ;
  NumOfCases++ ;
}

void
checkOneICaseOnEffective( FILE *outfp, FILE *infp, int nth ) {
  int i, j ;
  int fin ;

  for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
    Act[ nth ].bcase[ i ].idx = 0 ;
  }

  while ( 1 ) {
    fprintf( outfp, "open ISTEP\n" ) ;
    fflush( outfp ) ;
    if ( checkError( infp, CafeOBJErrMsg ) ) {
      fprintf( stderr, "No module 'ISTEP'\n" ) ;
      skipTilString( infp, CafeOBJPROMPT ) ;
      longjmp( CheckPSEnv, 1 ) ;
    }
    skipTilString( infp, "%ISTEP> " ) ;
    for ( i = 0 ; i < Act[ nth ].numOfConsts ; i++ ) {
      fprintf( outfp, "op %s .\n", Act[ nth ].constant[ i ] ) ;
      fflush( outfp ) ;
      skipTilString( infp, "%ISTEP> " ) ;
    }
    for ( i = 0 ; i < Act[ nth ].numOfConjs ; i++ ) {
      fprintf( outfp, "eq %s .\n", Act[ nth ].conjunct[ i ] ) ;
      fflush( outfp ) ;
      skipTilString( infp, "%ISTEP> " ) ;
    }
    for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
      fprintf( outfp, "eq %s .\n", Act[ nth ].bcase[ i ].bc[ Act[ nth ].bcase[ i ].idx ] ) ;
      fflush( outfp ) ;
      skipTilString( infp, "%ISTEP> " ) ;
      for ( j = 0 ; 
	    Act[ nth ].bcase[ i ].bc[ Act[ nth ].bcase[ i ].idx ][ j ] != '\0' ; j++ ) {
	if ( Act[ nth ].bcase[ i ].bc[ Act[ nth ].bcase[ i ].idx ][ j ] == '\n' ) {
	  skipTilString( infp, "%ISTEP> " ) ;
	}
      }
    }
    fprintf( outfp, "eq %s = %s .\n", SuccessorTerm, Act[ nth ].action ) ;
    fflush( outfp ) ;
    skipTilString( infp, "%ISTEP> " ) ;
    fprintf( outfp, "red " ) ;
    if ( Act[ nth ].uselem ) {
      fprintf( outfp, "%s implies ", Act[ nth ].lemma ) ;
    }
    fprintf( outfp, "%s .\n", InductivePred ) ;
    fflush( outfp ) ;
    if ( checkError( infp, CafeOBJErrMsg ) ) {
      fprintf( stderr, "Error in Inductive case: '%s'\n", Act[ nth ].action ) ;
      fprintf( outfp, "close\n" ) ;
      skipTilString( infp, CafeOBJPROMPT ) ;
      longjmp( CheckPSEnv, 1 ) ;
    }
    getResult( infp, RESULT, MAX2 ) ;
    /* printf( "Result: %s\n", RESULT ) ; */
    if ( strcmp( RESULT, ExpectedResult ) ) {
      NumOfNonExpectedResults++ ;
      fprintf( stdout, "\nNot expected: Inductive case '%s' on effective\n",
	       Act[ nth ].action ) ;
      fprintf( stdout, "--- Assumptions ---\n" ) ;
      for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
	fprintf( stdout, "  eq %s .\n", 
		 Act[ nth ].bcase[ i ].bc[ Act[ nth ].bcase[ i ].idx ] ) ;
      }
      fprintf(stdout,"--- End of Assumptions ---\n" ) ;
      fprintf( stdout, "Result: %s ...\n", RESULT ) ;
    } else {
      putc( '.', stdout ) ;
      fflush( stdout ) ;
    }
    fprintf( outfp, "close\n" ) ;
    fflush( outfp ) ;
    skipTilString( infp, CafeOBJPROMPT ) ;
    NumOfCases++ ;

    fin = 1 ;
    for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
      if ( Act[ nth ].bcase[ i ].idx != Act[ nth ].bcase[ i ].numOfBCases - 1 ) {
	fin = 0 ;
	break ;
      }
    }
    if ( fin ) break ;
    for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
      if ( Act[ nth ].bcase[ i ].idx < Act[ nth ].bcase[ i ].numOfBCases -1 ) {
	Act[ nth ].bcase[ i ].idx++ ;
	break ;
      }
      Act[ nth ].bcase[ i ].idx = 0 ;
    }
  }
}

void
checkOneICaseOnNonEffective( FILE *outfp, FILE *infp, int nth ) {
  int i;
  if ( Act[ nth ].numOfConjs > 0 ) {
    fprintf( outfp, "open ISTEP\n" ) ;
    fflush( outfp ) ;
    if ( checkError( infp, CafeOBJErrMsg ) ) {
      fprintf( stderr, "No module 'ISTEP'\n" ) ;
      skipTilString( infp, CafeOBJPROMPT ) ;
      longjmp( CheckPSEnv, 1 ) ;
    }
    skipTilString( infp, "%ISTEP> " ) ;
    for ( i = 0 ; i < Act[ nth ].numOfConsts ; i++ ) {
      fprintf( outfp, "op %s .\n", Act[ nth ].constant[ i ] ) ;
      fflush( outfp ) ;
      skipTilString( infp, "%ISTEP> " ) ;
    }
    fprintf( outfp, "eq c-%s = false .\n", Act[ nth ].action ) ;
    fflush( outfp ) ;
    skipTilString( infp, "%ISTEP> " ) ;
    fprintf( outfp, "eq %s = %s .\n", SuccessorTerm, Act[ nth ].action ) ;
    fflush( outfp ) ;
    skipTilString( infp, "%ISTEP> " ) ;
    fprintf( outfp, "red %s .\n", InductivePred ) ;
    fflush( outfp ) ;
    if ( checkError( infp, CafeOBJErrMsg ) ) {
      fprintf( stderr, "Error in Inductive case: '%s'\n", Act[ nth ].action ) ;
      fprintf( outfp, "close\n" ) ;
      skipTilString( infp, CafeOBJPROMPT ) ;
      longjmp( CheckPSEnv, 1 ) ;
    }
    getResult( infp, RESULT, MAX2 ) ;
    /* printf( "Result: %s\n", RESULT ) ; */
    if ( strcmp( RESULT, ExpectedResult ) ) {
      NumOfNonExpectedResults++ ;
      fprintf( stdout, "Not expected: Inductive case '%s' on non effective\n", 
	       Act[ nth ].action ) ;
      fprintf( stdout, "%s\n", RESULT ) ;
    } else {
      putc( '.', stdout ) ;
    }
    fprintf( outfp, "close\n" ) ;
    fflush( outfp ) ;
    skipTilString( infp, CafeOBJPROMPT ) ;
    NumOfCases++ ;
  }
}

void
checkOneICase( FILE *outfp, FILE *infp, int nth ) {
  checkOneICaseOnEffective( outfp, infp, nth ) ;
  checkOneICaseOnNonEffective( outfp, infp, nth ) ;
}

void
checkInductive( FILE *outfp, FILE *infp ) {
  int i ;
  for ( i = 0 ; i < NumOfActs ; i++ ) {
    checkOneICase( outfp, infp, i ) ;
  }
}

void
checkProofScores( FILE *outfp, FILE *infp ) {
  if ( !HaveScript ) {
    fprintf( stderr, "Not yet read any Gateaux script files!!!\n" ) ;
    return ;
  }
  if ( setjmp( CheckPSEnv ) ) {
    return ;
  }
  NumOfNonExpectedResults = 0 ;
  NumOfCases = 0 ;
  checkBase( outfp, infp ) ;
  checkInductive( outfp, infp ) ;
  fprintf( stdout, "\n%d cases checked\n", NumOfCases ) ;
  if ( NumOfNonExpectedResults == 0 ) {
    fprintf( stdout, "Proof successfully completed ;-)\n" ) ;
  } else {
    fprintf( stdout, "%d cases left to be considered ... :-(\n", NumOfNonExpectedResults ) ;
  }
}

void
printInitialMessage( void ) {
  printf( "*************************************************************\n" ) ;
  printf( "*** Gateaux: A Proof Assistant for the OTS/CafeOBJ method ***\n" ) ;
  printf( "***                Prototype Version 0.1                  ***\n" ) ;
  printf( "*************************************************************\n" ) ;
}

void
printFinalMessage( void ) {
  printf( "Au revoir!\n" ) ;
}

#define PROMPT "Gateaux> "
#define CAFEPATH "/usr/local/bin/cafeobj"

void
commandInterpreter( FILE *outfp, FILE *infp ) {
  TOKEN2 tk ;

  printInitialMessage( ) ;
  skipTilString( infp, CafeOBJPROMPT ) ;
  printf( "%s", PROMPT ) ;
  while ( (tk = pascanner( stdin )) != FIN ) {
    switch( tk ) {
    case IN:
      if ( Name[ 0 ] == '\0' ) {
	fprintf( stderr, "Uage: in <CafeOBJ File>\n" ) ;
      } else {
	fprintf( outfp, "in %s\n", Name ) ;
	fflush( outfp ) ;
	if ( checkError( infp, CafeOBJErrMsg ) ) {
	  fprintf( stderr, "No such file: '%s.mod'  (Maybe ;-)\n", Name ) ;
	} 
	skipTilString( infp, CafeOBJPROMPT ) ;
      }
      break ;
    case READ:
      if ( Name[ 0 ] == '\0' ) {
	fprintf( stderr, "Uage: read <Gateaux File>\n" ) ;
      } else {
	processGateauxScript( Name ) ;
      }
      break ;
    case GEN:
      generateProofScores( Name ) ;
      break ;
    case CHECK:
      checkProofScores( outfp, infp ) ;
      break ;
    case HELP:
      printf( "The commands available:\n" ) ;
      printf( "1. in <CafeOBJ File>\n" ) ;
      printf( "2. read <Gateaux File>\n" ) ;
      printf( "3. gen\n" ) ;
      printf( "4. check\n" ) ;
      printf( "5. help\n" ) ;
      break ;
    case ERROR2:
    default:
      fprintf( stderr, "No such command!!!\n" ) ;
      break ;
    }
  printf( "%s", PROMPT ) ;
  }
  printFinalMessage( ) ;
}

jmp_buf INTENv ;

void inthandler( int x ) {
  longjmp( INTENv, 1 ) ;
}

void
passist( void ) {
  int pid ;
  int send[ 2 ] ; /* for sending commands to the CafeOBJ system */
  int rec[ 2 ] ;  /* for receving results from the CafeOBJ system */
  FILE *infp, *outfp ; 
  int c ;

  /* sigignore( SIGINT ) ; */
  if ( signal( SIGINT, inthandler ) == SIG_ERR ) {
    fprintf( stderr, "Cannot set a signal handler!!!\n" ) ;
    exit( -1 ) ;
  }
  if ( setjmp( INTENv ) ) {
    fprintf( stdout, "Interrupted!!!\n" ) ;
    kill( pid, SIGKILL ) ;
    exit( -1 ) ;
  }
  if ( pipe( send ) < 0 ) {
    fprintf( stderr, "Cannot create pipes (1)!!!\n" ) ;
    exit( -1 ) ;
  }
  if ( pipe( rec ) < 0 ) {
    fprintf( stderr, "Cannot create pipes (2)!!!\n" ) ;
    exit( -1 ) ;
  }
  if ( (pid = fork( )) == 0 ) {
    close( send[ 1 ] ) ;
    close( rec[ 0 ] ) ;
    dup2( send[ 0 ], 0 ) ;
    dup2( rec[ 1 ], 1 ) ;
    execl( CAFEPATH, "cafeobj", NULL ) ;
    exit( 0 ) ;
  } else {
    if ( pid < 0 ) {
      fprintf( stderr, "Cannot create a process!!!\n" ) ;
      exit( -1 ) ;
    }
    close( send[ 0 ] ) ;
    close( rec[ 1 ] ) ;
    if ( !(outfp = fdopen( send[ 1 ], "w" )) ) {
      fprintf( stderr, "Cannot fdopen (1)!!!\n" ) ;
      kill( pid, SIGKILL ) ;
      exit( -1 ) ;
    }
    if ( !(infp = fdopen( rec[ 0 ], "r" )) ) {
      fprintf( stderr, "Cannot fdopen (2)!!!\n" ) ;
      kill( pid, SIGKILL ) ;
      exit( -1 ) ;
    }
    commandInterpreter( outfp, infp ) ;
    fprintf( outfp, "quit\n" ) ;
    fflush( outfp ) ;
    while ( (c = getc( infp )) != EOF ) {
      /* putchar( c ) ; */
    }
    fclose( infp ) ;
    fclose( outfp ) ;
    close( send[ 1 ] ) ;
    close( rec[ 0 ] ) ;
    /* kill( pid, SIGKILL ) ; */
  }
}