/*************************************************************
**************************************************************
Proof score (template) generator (prototype)

The generator, called pstgen, takes a script file, 
which looks like this 

-- begin proof1.pst --
#base: inv1(init,i,j)

#inductive: istep1(i,j)

#successor: s'

#action: want(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = l1
#case: i = k 
       (i = k) = false
#case: j = k 
       (j = k) = false

#action: try(s,k)
#constants: k : -> Pid 
#effective: pc(s,k) = l2 
            top(queue(s)) = k
#lemma: inv2(s,i) and inv2(s,j)
#case: i = k 
       (i = k) = false
#case: j = k 
       (j = k) = false

#action: exit(s,k)
#constants: k : -> Pid
#effective: pc(s,k) = cs
#case: i = k 
       (i = k) = false
#case: j = k 
      (j = k) = false
-- end proof1.pst

and generates proof socres of the OTS/CafeOBJ method.
**************************************************************
*************************************************************/

#include <stdio.h>
#include <setjmp.h>

typedef enum {
  BASE,
  INDUCTIVE,
  SUCCESSOR,
  ACTIONS,
  CONSTANTS,
  ACTION,
  EFFECTIVE,
  CASE,
  LEMMA,
  EXP,
  END,
  ERROR,
} TOKEN ;

#define MAX 128

char Term[ 1024 ] ;

typedef struct {
  TOKEN tk ;
  char *kwd ;
} KEYWORD ;

#define NumOfKeywords 8

KEYWORD Keyword[ NumOfKeywords ] = {
  { BASE ,     "#base:" },
  { INDUCTIVE, "#inductive:" },
  { SUCCESSOR, "#successor:" },
  { CONSTANTS, "#constants:" },
  { ACTION,    "#action:" },
  { EFFECTIVE, "#effective:" },
  { CASE,      "#case:" },
  { LEMMA,     "#lemma:" },
} ;

int UnscanFlag ;
TOKEN Token ;

void
initPstscanner( void ) {
  UnscanFlag = 0 ;
}

void
finPstscanner( void) {
}

void
unscan( TOKEN tk ) {
  UnscanFlag = 1 ;
  Token = tk ;
}

TOKEN
pstscanner( FILE *fp ) {
  int c, c2 ;
  int cnt ;
  int i ;
  int flag ;

  if ( UnscanFlag ) {
    UnscanFlag = 0 ;
    return Token ;
  }
  while ( (c = getc( fp )) != EOF ) {
    switch ( c ) {
    case ' ':
    case '\t' :
    case '\n' :
      break ;
    case '#' :
      c2 = getc( fp ) ;
      if ( c2 == '#' ) { /* Comment starts */
	do {
	  c2 = getc( fp ) ;
	} while ( c2 != '\n' && c2 != EOF ) ;
	ungetc( c2, fp ) ;
	break ;
      }
      ungetc( c2, fp ) ;
      cnt = 0 ;
      do {
	Term[ cnt++ ] = c ;
	c = getc( fp ) ;
      } while ( c != ':' && c != EOF ) ;
      if ( c == ':' ) {
	Term[ cnt++ ] = c ;
	Term[ cnt++ ] = '\0' ;
	for ( i = 0 ; i < NumOfKeywords ; i++ ) {
	  if ( !strcmp( Term, Keyword[ i ].kwd ) ) {
	    return Keyword[ i ].tk ;
	  }
	}
	return ERROR ;
      } else {
	return ERROR ;
      }
    default:
      cnt = 0 ;
      flag = 0 ;
      do {
	if ( c == ' ' || c == '\t' ) {
	  if ( !flag ) { 
	    Term[ cnt++ ] = ' ' ;
	    flag = 1 ;
	  }
	} else if ( c == '\\' ) {
          if ( (c2 = getc( fp )) == '\n' ) {
            ungetc( ' ', fp ) ;
          } else {
            ungetc( c2, fp ) ;
            Term[ cnt++ ] = c ;
            flag = 0 ;
          }
	} else if ( c  == '&' ) {
	  if ( (c2 = getc( fp )) == '\n' ) {
	    if ( Term[ cnt ] != ' ' ) {
	      Term[ cnt++ ] = ' ' ;
	    }
	    Term[ cnt++ ] = '.' ;
	    Term[ cnt++ ] = '\n' ;
	    Term[ cnt++ ] = ' ' ;
	    Term[ cnt++ ] = ' ' ;
	    Term[ cnt++ ] = 'e' ;
	    Term[ cnt++ ] = 'q' ;
	    Term[ cnt++ ] = ' ' ;
	    flag = 1 ;
	  } else {
	    ungetc( c2, fp ) ;
            Term[ cnt++ ] = c ;
            flag = 0 ;
	  }
	} else {
	  Term[ cnt++ ] = c ;
	  flag = 0 ;
	}
	c = getc( fp ) ;
      } while ( c != '\n' && c != EOF ) ;
      Term[ cnt++ ] = '\0' ;
      return EXP ;
    }
  }
  return END ;
}

void
testscanner( void ) {
  TOKEN tk ;
  initPstscanner( ) ;
  while ( (tk = pstscanner( stdin )) != END ) {
    printf( "%s\n", Term ) ;
  }
  finPstscanner( ) ;
}

typedef struct {
  int numOfBCases ;
  int idx ;
  char bc[ 32 ][ 1024 ] ;
} BASECASE ;

typedef struct {
  char action[ MAX ] ;
  int numOfConsts ;
  int numOfConjs ;
  int uselem ;
  int numOfCases ;
  char constant[ 32 ][ MAX ] ;
  char conjunct[ 64 ][ MAX ] ;
  char lemma[ MAX ] ;
  BASECASE bcase[ MAX ] ;
} ACT ;

char BasePred[ MAX ] ;
char InductivePred[ MAX ] ;
char SuccessorTerm[ MAX ] ;
int NumOfActs ;
ACT Act[ MAX ] ;

void
initPstparser( void ) {
  NumOfActs = 0 ;
}

void
finPstparser( void ) {
}

jmp_buf ParserEnv ;

int
pstparser( FILE *fp ) {
  TOKEN tk ;

  if ( setjmp( ParserEnv ) ) {
    return 0 ;
  }
  while ( (tk = pstscanner( fp )) != END ) {
    switch ( tk ) {
    case BASE:
      if ( pstscanner( fp ) == EXP ) {
	strcpy( BasePred, Term ) ;
      } else {
	fprintf( stderr, "Syntax Error in #base:!!!\n" ) ;
	longjmp( ParserEnv, 1 ) ;
      }
      break ;
    case INDUCTIVE:
      if ( pstscanner( fp ) == EXP ) {
	strcpy( InductivePred, Term ) ;
      } else {
	fprintf( stderr, "Syntax Errorin #inductive:!!!\n") ;
	longjmp( ParserEnv, 1 ) ;
      }
      break ;
    case SUCCESSOR:
      if ( pstscanner( fp ) == EXP ) {
	strcpy( SuccessorTerm, Term ) ;
      } else {
	fprintf( stderr, "Syntax Errorin #successor:!!!\n") ;
	longjmp( ParserEnv, 1 ) ;
      }
      break ;
    case ACTION:
      if ( pstscanner( fp ) == EXP ) {
	strcpy( Act[ NumOfActs ].action, Term ) ;
      } else {
	fprintf( stderr, "Syntax Errorin #action:!!!\n") ;
	longjmp( ParserEnv, 1 ) ;
      }
      if ( (tk = pstscanner( fp )) == CONSTANTS ) {
	void handleConstants( FILE* ) ;
	handleConstants( fp ) ;
      } else {
	unscan( tk ) ;
      }
      if ( (tk = pstscanner( fp )) == EFFECTIVE ) {
	void handleEffectives( FILE* ) ;
	handleEffectives( fp ) ;
      } else {
	unscan( tk ) ;
      }
      if ( (tk = pstscanner( fp )) == LEMMA ) {
	void handleLemma( FILE* ) ;
	handleLemma( fp ) ;
      } else {
	Act[ NumOfActs ].uselem = 0 ;
	unscan( tk ) ;
      }
      if ( (tk = pstscanner( fp )) == CASE ) {
	void handleCases( FILE* ) ;
	unscan( tk ) ;
	handleCases( fp ) ;
      } else {
	Act[ NumOfActs ].numOfCases = 0 ;
	unscan( tk ) ;
      }
      NumOfActs++;
      break ;
    default:
      fprintf( stderr, "Syntax Error!!!\n") ;
      longjmp( ParserEnv, 1 ) ;
    }
  }
  return 1 ;
}

void
handleConstants( FILE *fp ) {
  int i = 0 ;
  TOKEN tk ;
  while ( (tk = pstscanner( fp )) == EXP ) {
    strcpy( Act[ NumOfActs ].constant[ i++ ], Term ) ;
  }
  unscan( tk ) ;
  Act[ NumOfActs ].numOfConsts = i ;
}

void
handleEffectives( FILE *fp ) {
  int i = 0 ;
  TOKEN tk ;
  while ( (tk = pstscanner( fp )) == EXP ) {
    strcpy( Act[ NumOfActs ].conjunct[ i++ ], Term ) ;
  }
  unscan( tk ) ;
  Act[ NumOfActs ].numOfConjs = i ;
}

void
handleLemma( FILE *fp ) {
  TOKEN tk ;
  if ( (tk = pstscanner( fp )) == EXP ) {
    Act[ NumOfActs ].uselem = 1 ;
    strcpy( Act[ NumOfActs ].lemma, Term ) ;
  } else {
    Act[ NumOfActs ].uselem = 0 ;
    unscan( tk ) ;
  }
}

void
handleCases( FILE *fp ) {
  int i, j ;
  TOKEN tk ;
  i = 0 ;
  while ( (tk = pstscanner( fp )) == CASE ) {
    j = 0 ;
    if ( (tk = pstscanner( fp )) != EXP ) {
      fprintf( stderr, "Syntax error in #case:!!!\n" ) ;
      longjmp( ParserEnv, 1 ) ;
    }
    strcpy( Act[ NumOfActs ].bcase[ i ].bc[ j++ ], Term ) ;
    while( (tk = pstscanner( fp )) == EXP ) {
      strcpy( Act[ NumOfActs ].bcase[ i ].bc[ j++ ], Term ) ;
    }
    Act[ NumOfActs ].bcase[ i++ ].numOfBCases = j ;
    unscan( tk ) ;
  }
  Act[ NumOfActs ].numOfCases = i ;
  unscan( tk ) ;
}

void
testparser( void ) {
  int i, j, k ;

  initPstscanner( ) ;
  initPstparser( ) ;

  pstparser( stdin ) ;
  printf( "%s\n", BasePred ) ;
  printf( "%s\n", InductivePred ) ;
  printf( "%s\n", SuccessorTerm ) ;
  for ( i = 0 ; i < NumOfActs ; i++ ) {
    printf( "%s\n", Act[ i ].action ) ;
    for ( j = 0 ; j < Act[ i ].numOfConsts ; j++ ) {
      printf( "%s\n", Act[ i ].constant[ j ] ) ;
    }
    for ( j = 0 ; j < Act[ i ].numOfConjs ; j++ ) {
      printf( "%s\n", Act[ i ].conjunct[ j ] ) ;
    }
    if ( Act[ i ].uselem ) {
      printf( "%s\n", Act[ i ].lemma ) ;
    }
    for ( j = 0 ; j < Act[ i ].numOfCases ; j++ ) {
      for ( k = 0 ; k < Act[ i ].bcase[ j ].numOfBCases ; k++ ) {
	printf( "%s\n", Act[ i ].bcase[j ].bc[ k ] ) ;
      }
    }
  }

  finPstscanner( ) ;
}

void
printParseResults( void ) {
  int i, j, k ;

  printf( "%s\n", BasePred ) ;
  printf( "%s\n", InductivePred ) ;
  printf( "%s\n", SuccessorTerm ) ;
  for ( i = 0 ; i < NumOfActs ; i++ ) {
    printf( "%s\n", Act[ i ].action ) ;
    for ( j = 0 ; j < Act[ i ].numOfConsts ; j++ ) {
      printf( "%s\n", Act[ i ].constant[ j ] ) ;
    }
    for ( j = 0 ; j < Act[ i ].numOfConjs ; j++ ) {
      printf( "%s\n", Act[ i ].conjunct[ j ] ) ;
    }
    if ( Act[ i ].uselem ) {
      printf( "%s\n", Act[ i ].lemma ) ;
    }
    for ( j = 0 ; j < Act[ i ].numOfCases ; j++ ) {
      for ( k = 0 ; k < Act[ i ].bcase[ j ].numOfBCases ; k++ ) {
	printf( "%s\n", Act[ i ].bcase[j ].bc[ k ] ) ;
      }
    }
  }
}

void
generateBase( FILE *fp ) {
  fprintf( fp, "--> I) Base cases\n" ) ;
  fprintf( fp, "open INV\n" ) ;
  fprintf( fp, "  red %s .\n", BasePred ) ;
  fprintf( fp, "close\n" ) ;
  fprintf( fp, "\n" ) ;
}

void
generateOneICaseOnEffective( FILE *fp, int nth ) {
  int i ;
  int fin ;

  if ( Act[ nth ].numOfConjs > 0 ) {
    fprintf( fp, "-- %d.1 c-%s = true\n", nth + 1, Act[ nth ].action ) ;
  }

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

  while ( 1 ) {
    fprintf( fp, "open ISTEP\n" ) ;
    fprintf( fp, "-- arbitrary objects\n" ) ;
    for ( i = 0 ; i < Act[ nth ].numOfConsts ; i++ ) {
      fprintf( fp, "  op %s .\n", Act[ nth ].constant[ i ] ) ;
    }
    fprintf( fp, "-- assumptions\n" ) ;
    if ( Act[ nth ].numOfConjs > 0 ) {
      fprintf( fp, "  -- eq c-%s = true .\n", Act[ nth ].action ) ;
    }
    for ( i = 0 ; i < Act[ nth ].numOfConjs ; i++ ) {
      fprintf( fp, "  eq %s .\n", Act[ nth ].conjunct[ i ] ) ;
    }
    if ( Act[ nth ].numOfCases > 0 ) {
      fprintf( fp, "  --\n" ) ;
    }
    for ( i = 0 ; i < Act[ nth ].numOfCases ; i++ ) {
      fprintf( fp, "  eq %s .\n", Act[ nth ].bcase[ i ].bc[ Act[ nth ].bcase[ i ].idx ] ) ;
    }
    fprintf( fp, "-- successor\n" ) ;
    fprintf( fp, "  eq %s = %s .\n", SuccessorTerm, Act[ nth ].action ) ;
    fprintf( fp, "-- checking\n" ) ;
    fprintf( fp, "  red " ) ;
    if ( Act[ nth ].uselem ) {
      fprintf( fp, "%s implies ", Act[ nth ].lemma ) ;
    }
    fprintf( fp, "%s .\n", InductivePred ) ;
    fprintf( fp, "close\n" ) ;
    fprintf( fp, "--\n" ) ;
    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 
generateOneICaseOnNoneffective( FILE *fp, int nth ) {
  int i ;

  if ( Act[ nth ].numOfConjs > 0 ) {
    fprintf( fp, "-- %d.2 c-%s = false\n", nth + 1, Act[ nth ].action ) ;
    fprintf( fp, "open ISTEP\n" ) ;
    fprintf( fp, "-- arbitrary objects\n" ) ;
    for ( i = 0 ; i < Act[ nth ].numOfConsts ; i++ ) {
      fprintf( fp, "  op %s .\n", Act[ nth ].constant[ i ] ) ;
    }
    fprintf( fp, "-- assumptions\n" ) ;
    fprintf( fp, "  eq c-%s = false .\n", Act[ nth ].action ) ;
    fprintf( fp, "-- successor\n" ) ;
    fprintf( fp, "  eq %s = %s .\n", SuccessorTerm, Act[ nth ].action ) ;
    fprintf( fp, "-- checking\n" ) ;
    fprintf( fp, "  red %s .\n", InductivePred ) ;
    fprintf( fp, "close\n" ) ;
  }
  fprintf( fp, "\n" ) ;
}

void
generateOneICase( FILE *fp, int nth ) {
  generateOneICaseOnEffective( fp, nth ) ;
  generateOneICaseOnNoneffective( fp, nth ) ;
}

void
generateInductive( FILE *fp ) {
  int i ;
  fprintf( fp, "--> II) Inductive cases\n" ) ;
  for ( i = 0 ; i < NumOfActs ; i++ ) {
    fprintf( fp, "--> %d %s\n", i + 1, Act[ i ].action ) ;
    generateOneICase( fp, i ) ;
  }
}

void
pstgenerator( FILE *fp ) {
  generateBase( fp ) ;
  generateInductive( fp ) ;
  fprintf( fp, "--> Q.E.D.\n" ) ;
}

void
testPstgenerator( void ) {
  initPstscanner( ) ;
  initPstparser( ) ;

  pstparser( stdin ) ;
  pstgenerator( stdout ) ;

  finPstparser( ) ;
  finPstscanner( ) ;
}

/************
main( ) {
  testscanner( ) ;
  testparser( ) ;
  testPstgenerator( ) ;
}
*************/