%{
  /*-----------------------------------------------------------------------------*/
#include <stdio.h>
#include <string.h>
#include <stdlib.h>

#include "foldfg.h"
#include "symbol.h"
#include "term.h"
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the FreeBSD    * */
/* *  Licence.                                              * */
/* *                                                        * */
/* *  This program 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 LICENCE file       * */
/* *  for more details.                                     * */
#include "misc.h"
#include "list.h"
#include "strings.h"

#include "tptp.h"
#include "tptpparser.h" /*generated by bison - only include it as a last thing*/

  /*-----------------------------------------------------------------------------*/

  /*flex/bison extern things*/
  extern int tptp_lineno;
  extern char* tptp_text;
  extern FILE* tptp_in;

  int yyparse(void);
  void yyerror(const char*);
  int  yylex(void);		  /* Defined in dfgscanner.l */

  /*-----------------------------------------------------------------------------*/

  typedef enum {
    TPTP_ORDINARY, TPTP_DEFINED, TPTP_SYSTEM
  } TPTP_SYMBOLKIND;

  typedef enum {
    TPTP_UNDEF, TPTP_FOF, TPTP_CNF
  } TPTP_FORMULATYPE;

  static LIST tptp_VARLIST;

  static PRECEDENCE tptp_PRECEDENCE;

  static FILE* tptp_output = NULL; /* for outputting comments */

  static BOOL  tptp_TranslateIdents = TRUE;

  static LIST tptp_Axioms;
  static LIST tptp_Conjectures;
  static LIST tptp_Includes;

  static TPTP_FORMULATYPE tptp_LastFormulaType;

  static BOOL tptp_StatusRead;
  static BOOL tptp_DomainRead;
  static BOOL tptp_ProblemRead;
  static BOOL tptp_EnglishRead;
  static BOOL tptp_EnglishReading;

  static DFGDESCRIPTION tptp_Description;

  static SYMBOL tptp_GetSymbol(char *, int, TPTP_SYMBOLKIND);
  static TERM tptp_TermCreate(SYMBOL, LIST);

  static void tptp_CheckArguments(TERM Term);
  static TERM   tptp_VarTermCreate(char*);
  static void   tptp_RestartVarList(void);
  static SYMBOL tptp_VarLookup(char*);

  static char* tptp_StripQuotes(char *);

  static void tptp_HandleComments(char *);
  static TERM tptp_HandleAtomic(TERM);
  static void tptp_HandleInclude(char*,LIST);
  static TERM tptp_NormalizeLiterals(TERM, BOOL);
  static void tptp_HandleFormula(char*, char*, TERM, BOOL);
  static TERM tptp_CheckClosedness(TERM, BOOL);

  /*-----------------------------------------------------------------------------*/

  %}

%union {  
  char*     string;
  SYMBOL    symbol;
  TERM      term;
  LIST      list;
  BOOL      bool;
}

%start  TPTP_file

%token AMPERSAND
%token COLON
%token COMMA
%token EQUALS
%token EQUALS_GREATER
%token EXCLAMATION
%token EXCLAMATION_EQUALS
%token LBRKT
%token LESS_EQUALS
%token LESS_EQUALS_GREATER
%token LESS_TILDE_GREATER
%token LPAREN
%token PERIOD
%token QUESTION
%token RBRKT
%token RPAREN
%token TILDE
%token TILDE_AMPERSAND
%token TILDE_VLINE
%token VLINE
%token _DLR_cnf
%token _DLR_fof
%token _DLR_fot
%token _LIT_cnf
%token _LIT_fof
%token _LIT_include

%token <string> comment_line
%token <string> distinct_object
%token <string> dollar_dollar_word
%token <string> dollar_word
%token <string> lower_word
%token <string> real
%token <string> signed_integer
%token <string> single_quoted
%token <string> unsigned_integer
%token <string> upper_word

%token unrecognized

%type <string> file_name number atomic_system_word atomic_defined_word atomic_word name formula_role defined_atom
%type <list> formula_selection /*LIST of (char *)*/
%type <list> name_list /*LIST of (char *)*/
%type <list> arguments /*LIST of TERM*/
%type <list> disjunction /*LIST of literal*/
%type <list> variable_list /*LIST of variable*/
%type <list> and_formula /*LIST of formula*/
%type <list> or_formula /*LIST of formula*/

%type <term> system_constant system_term system_atomic_formula 
%type <term> defined_constant defined_plain_term defined_atomic_term defined_term
%type <term> defined_infix_formula defined_plain_formula defined_atomic_formula 

%type <term> term variable constant plain_term function_term  plain_atomic_formula atomic_formula literal
%type <term> cnf_formula unitary_formula unary_formula quantified_formula assoc_binary nonassoc_binary
%type <term> fof_formula binary_formula

%type <string> system_functor defined_functor functor

%type <symbol> unary_connective binary_connective quantifier defined_infix_pred

%%

 /*null*/
TPTP_file : null
| TPTP_file TPTP_input
;
	  
/*null*/
TPTP_input : annotated_formula
| include 
| comment_line { tptp_HandleComments($1); }
;

/*null*/
annotated_formula : fof_annotated
| cnf_annotated
;

/*null*/
fof_annotated : _LIT_fof LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD {
  tptp_HandleFormula($3,$5,tptp_CheckClosedness($7,FALSE),FALSE);
}
;

/*null*/
cnf_annotated : _LIT_cnf LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD {                  
  tptp_HandleFormula($3,$5,tptp_CheckClosedness($7,TRUE),TRUE);
}
;

/*null*/
annotations : COMMA source optional_info {                
  misc_UserWarning("Nonempty anntotation encountered near line %d and ignored!\n",tptp_lineno);
}
| null { }
;

/*(char *)*/
formula_role : lower_word {$$ = $1;}
;
             
/*TERM*/					
fof_formula : binary_formula { $$ = $1; }
| unitary_formula { $$ = $1; }
;

/*TERM*/
binary_formula : nonassoc_binary { $$ = $1; }
| assoc_binary { $$ = $1; }
;
               
/*TERM*/
nonassoc_binary : unitary_formula binary_connective unitary_formula {
  $$ = term_Create($2,list_Cons($1,list_List($3)));
}
;

/*TERM*/
assoc_binary : or_formula { $$ = term_Create(fol_Or(),$1); }
| and_formula { $$ = term_Create(fol_And(),$1); }
;

/*LIST of TERM*/
or_formula : unitary_formula VLINE unitary_formula { $$ = list_Cons($1,list_List($3)); }
| unitary_formula VLINE or_formula { $$ = list_Cons($1,$3); }
;

/*LIST of TERM*/
and_formula : unitary_formula AMPERSAND unitary_formula { $$ = list_Cons($1,list_List($3)); }                              
| unitary_formula AMPERSAND and_formula { $$ = list_Cons($1,$3); }
;
            
/*TERM*/
unitary_formula : quantified_formula { $$ = $1; }
| unary_formula {  $$ = $1; }
| atomic_formula  { $$ = tptp_NormalizeLiterals($1,FALSE); }
| LPAREN fof_formula RPAREN { $$ = $2; }
;

/*TERM*/
quantified_formula : quantifier LBRKT variable_list RBRKT COLON unitary_formula {
  $$ = fol_CreateQuantifier($1, $3, list_List($6));              
}
;

/*LIST of TERM*/
variable_list : variable { $$ = list_List($1); }
| variable COMMA variable_list { $$ = list_Cons($1,$3); }
;

/*TERM*/
unary_formula : unary_connective unitary_formula { $$ = term_Create($1,list_List($2)); }
;
              
/*TERM*/
cnf_formula : LPAREN disjunction RPAREN { $$ = term_Create(fol_Or(),$2); }
| disjunction { $$ = term_Create(fol_Or(),$1); }
;

/*LIST of TERM*/
disjunction : literal { $$ = list_List($1); }
| literal VLINE disjunction { $$ = list_Cons($1,$3); }
;
            
/*TERM*/
literal : atomic_formula { $$ = tptp_NormalizeLiterals($1,FALSE); }
| TILDE atomic_formula { $$ = tptp_NormalizeLiterals($2,TRUE); }
;

	
/*SYMBOL*/
quantifier : EXCLAMATION { $$ = fol_All(); }
| QUESTION { $$ = fol_Exist(); }
;

/*SYMBOL*/
binary_connective : LESS_EQUALS_GREATER { $$ = fol_Equiv(); }
| EQUALS_GREATER { $$ = fol_Implies(); }
| LESS_EQUALS { $$ = fol_Implied(); }
| LESS_TILDE_GREATER { $$ = fol_Xor(); }
| TILDE_VLINE { $$ = fol_Nor(); }
| TILDE_AMPERSAND { $$ = fol_Nand(); }
;

/*SYMBOL*/
unary_connective : TILDE {
  $$ = fol_Not();
}
;

/*TERM*/
atomic_formula : plain_atomic_formula {
  $$ = tptp_HandleAtomic($1);
}
| defined_atomic_formula {
  $$ = tptp_HandleAtomic($1);
}
| system_atomic_formula {
  $$ = tptp_HandleAtomic($1);
}
;

/*TERM*/
plain_atomic_formula : plain_term { $$ = $1; }
;

/*TERM*/
defined_atomic_formula : defined_plain_formula { $$ = $1; }
| defined_infix_formula { $$ = $1; }
;

/*TERM*/
defined_plain_formula : defined_plain_term { $$ = $1; }
;

/*TERM*/
defined_infix_formula : term defined_infix_pred term {
  $$ = term_Create($2,list_Cons($1,list_List($3)));
}
;

/*SYMBOL*/				
defined_infix_pred : EQUALS { $$ = fol_Equality(); }
| EXCLAMATION_EQUALS { $$ = fol_NonEquality(); }
;

/*TERM*/
system_atomic_formula : system_term { $$ = $1; }
;

/*TERM*/
term : function_term { $$ = $1; }
| variable { $$ = $1; }
;

/*TERM*/
function_term : plain_term { $$ = $1; }
| defined_term { $$ = $1; }
| system_term { $$ = $1; }
;

/*TERM*/
plain_term : constant { $$ = $1; }
| functor LPAREN arguments RPAREN {			  
  $$ = tptp_TermCreate(tptp_GetSymbol($1,list_Length($3),TPTP_ORDINARY),$3);
}
;

/*TERM*/
constant : functor {		     
  $$ = tptp_TermCreate(tptp_GetSymbol($1,0,TPTP_ORDINARY),list_Nil());
}
;

/*(char*)*/
functor : atomic_word { $$ = $1; }
;		 		
		
/*TERM*/
defined_term : defined_atom {
  $$ = tptp_TermCreate(tptp_GetSymbol($1,0,TPTP_DEFINED),list_Nil());
}
| defined_atomic_term { $$ = $1; }
;
			 
/*(char*)*/
defined_atom : number { $$ = $1; }
| distinct_object { $$ = $1; }
;			

/*TERM*/
defined_atomic_term : defined_plain_term { $$ = $1; }
;				

/*TERM*/
defined_plain_term : defined_constant { $$ = $1; }
| defined_functor LPAREN arguments RPAREN {			 
  $$ = tptp_TermCreate(tptp_GetSymbol($1,list_Length($3),TPTP_DEFINED),$3);
}
;

/*TERM*/
defined_constant : defined_functor {
  $$ = tptp_TermCreate(tptp_GetSymbol($1,0,TPTP_DEFINED),list_Nil());					 	                
}
;

/*(char *)*/
defined_functor : atomic_defined_word { $$ = $1; }
;

/*TERM*/				
system_term : system_constant { $$ = $1; }
| system_functor LPAREN arguments RPAREN {
  $$ = tptp_TermCreate(tptp_GetSymbol($1,list_Length($3),TPTP_SYSTEM),$3);
}
;

/*TERM*/
system_constant : system_functor {
  $$ = tptp_TermCreate(tptp_GetSymbol($1,0,TPTP_SYSTEM),list_Nil()); 
}
;

/*(char *)*/
system_functor : atomic_system_word { $$ = $1; }
;
			   
/*TERM*/
variable : upper_word { $$ = tptp_VarTermCreate($1);	}
;
 
/*LIST of TERM*/
arguments : term { $$ = list_List($1); }
| term COMMA arguments {
  $$ = list_Cons($1, $3);
}
;
		  
/*NULL - for now*/
source : general_term { /*unsupported yet*/ }
;

/*NULL - for now*/
optional_info : COMMA useful_info { /*unsupported yet*/}
| null { /*unsupported yet*/}
;

/*NULL - for now*/
useful_info : general_list { /*unsupported yet*/}
;

/*null*/
include : _LIT_include LPAREN file_name formula_selection RPAREN PERIOD {
  tptp_HandleInclude($3,$4); /*Handling is also responsible for freeing the strings, so we have nothing to pass on.*/
}
;

/*LIST of (char *)*/
formula_selection : COMMA LBRKT name_list RBRKT { $$ = $3; }
| null { $$ = list_Nil(); }
;

/*LIST of (char *)*/
name_list : name { $$ = list_List($1); }
| name COMMA name_list {
  $$ = list_Cons($1,$3);
}
;

/*NULL - for now*/
general_term : general_data { /*unsupported yet*/}
| general_data COLON general_term { /*unsupported yet*/}
| general_list { /*unsupported yet*/}
;

/*NULL - for now*/
general_data : atomic_word { string_StringFree($1); /*unsupported yet*/}
| atomic_word LPAREN general_terms RPAREN { string_StringFree($1); /*unsupported yet*/}
| variable { term_Delete($1); /*unsupported yet*/}
| number { string_StringFree($1); /*unsupported yet*/}
| distinct_object { string_StringFree($1); /*unsupported yet*/}
| formula_data { /*unsupported yet*/}
;

/*NULL - for now*/
formula_data : _DLR_fof LPAREN fof_formula RPAREN { term_Delete($3); /*unsupported yet*/}
| _DLR_cnf LPAREN cnf_formula RPAREN { term_Delete($3); /*unsupported yet*/}
| _DLR_fot LPAREN term RPAREN { term_Delete($3); /*unsupported yet*/}
;

/*NULL - for now*/
general_list : LBRKT RBRKT {/*unsupported yet*/}
| LBRKT general_terms RBRKT {/*unsupported yet*/}
;

/*NULL - for now*/
general_terms : general_term {/*unsupported yet*/}
| general_term COMMA general_terms {/*unsupported yet*/}
;

/*string*/
name : atomic_word { $$ = $1; }
| unsigned_integer {$$ = $1; }
;
	 
/*string*/
atomic_word : lower_word { $$ = $1; }
| single_quoted { $$ = tptp_StripQuotes($1);}
;

/*string*/
atomic_defined_word : dollar_word {	$$ = $1; }
;

/*string*/
atomic_system_word : dollar_dollar_word {	$$ = $1; }
;
  
/*string*/
number : real {$$ = $1;}
| signed_integer {$$ = $1;}
| unsigned_integer {$$ = $1;}
;

/*string*/
file_name : atomic_word { $$ = $1;}
;

/*null*/
null : { }
;
     
%%

static HASHMAP tptp_dfg_reserved_speedup = NULL;

#define TPTP_DFG_RESERVED_SIZE (85)
static const char * const tptp_dfg_reserveds[TPTP_DFG_RESERVED_SIZE] = {
  /*BEGIN RESERVED*/
  "and",
  "author",				
  "axioms",				
  "begin_problem",
  "by",
  "box",
  "all",
  "clause",
  "cnf",
  "comp",
  "conjectures",
  "conv",
  "date",
  "description",
  "dia",
  "some",
  "div",
  "dnf",
  "domain",
  "domrestr",
  "eml",
  "EML",
  "DL",
  "end_of_list",
  "end_problem",
  "equal",
  "equiv",
  "exists",
  "false",
  "forall",
  "formula",
  "freely",
  "functions",
  "generated",
  "hypothesis",
  "id",
  "implied",
  "implies",
  "list_of_clauses",
  "list_of_declarations",
  "list_of_descriptions",
  "list_of_formulae",
  "list_of_general_settings",
  "list_of_proof",
  "list_of_settings",
  "list_of_special_formulae",
  "list_of_symbols",
  "list_of_terms",
  "list_of_includes",
  "include",
  "logic",
  "name",
  "not",
  "operators",
  "or",
  "prop_formula",
  "concept_formula",
  "predicate",
  "predicates",
  "quantifiers",
  "ranrestr",
  "range",
  "rel_formula",
  "role_formula",
  "satisfiable",
  "set_DomPred",
  "set_flag",
  "set_precedence",
  "set_ClauseFormulaRelation",
  "set_selection",
  "sort",
  "sorts",
  "status",
  "step",
  "subsort",
  "sum",
  "test",
  "translpairs",
  "true",
  "unknown",
  "unsatisfiable",
  "version",
  "xor",
  "nor",
  "nand"
  /*END RESERVED*/
};

void tptp_Init(void)
/**************************************************************
  EFFECT: Initializes the parsing module.
 (Prepares the table of dfg reserved words for future fast tests)
***************************************************************/
{  
  int i;
  
  tptp_dfg_reserved_speedup = hm_Create(7);
  
  for (i = 0; i < TPTP_DFG_RESERVED_SIZE; i++) {
    hm_Insert(tptp_dfg_reserved_speedup,(POINTER)i,hm_StringHash(tptp_dfg_reserveds[i]));
  }  
}
  
void tptp_Free(void)
/**************************************************************
  EFFECT: Deinitialized the parsing module.
 (Frees the memory used by the table of dfg reserved words)
***************************************************************/
{
  hm_Delete(tptp_dfg_reserved_speedup);
}

static BOOL tptp_VarTermsEqual(POINTER t1, POINTER t2) {
  return symbol_Equal(term_TopSymbol((TERM)t1),term_TopSymbol((TERM)t2));
}
	
static LIST tptp_GetFreeVars(TERM Term)
/**************************************************************
  INPUT:   A term.
  RETURNS: List of free variables of the given term
           (i.e. those not captured by any quantifier).
  DETAILS: 
  Returns list of variable terms as they occur somewhere in the term, 
  the list returned is created (should be freed by caller),
  but its content shouldn't be used to build other terms (sharing!).

  The term itself stays intact.
***************************************************************/
{  
  if (term_IsVariable(Term))
    return list_List(Term);

  if (fol_IsQuantifier(term_TopSymbol(Term))) {
    LIST quant_vars, vars_in_subterms;

    quant_vars       = fol_QuantifierVariables(Term);
    vars_in_subterms = tptp_GetFreeVars(term_SecondArgument(Term));

    return list_NDifference(vars_in_subterms,quant_vars,tptp_VarTermsEqual);
  }
   
  if (term_IsComplex(Term)) {
    LIST Scan, Result, Subresult;
    Result = list_Nil();
	  
    for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
      Subresult = tptp_GetFreeVars(list_Car(Scan));
      Result    = list_NUnion(Subresult,Result,tptp_VarTermsEqual);
    }

    return Result;
  }

  return list_Nil();
}

static POINTER tptp_CopyVarTerm(POINTER p) {
  return term_Create(term_TopSymbol((TERM)p),list_Nil());
}

static TERM tptp_CheckClosedness(TERM formula, BOOL repair) 
/**************************************************************
  INPUT:   A formula and a repair flag.
  RETURNS: The same formula (possilby modified).
  EFFECT: 
  Checks if a given formula is closed (every variable captured by a quantifier).
  If not, universal closure is returned (if repair flag is true)
      otherwise an error is reported!
***************************************************************/
{
  LIST free_vars;

  free_vars = tptp_GetFreeVars(formula);
  
  if (!list_Empty(free_vars)) {
    if (repair) {
      list_NMapCar(free_vars,tptp_CopyVarTerm);
      return fol_CreateQuantifier(fol_All(),free_vars,list_List(formula));
    } else {
      list_Delete(free_vars);
      misc_StartUserErrorReport();
      misc_UserErrorReport("Free variable occurence near line %d!\n",tptp_lineno);
      misc_FinishUserErrorReport();
    }
  }
  
  return formula;
}

static char* tptp_NewlinedAppend(char * first, const char * second) {
  char* res;

  res = memory_Malloc(strlen(first) + strlen(second) + 2);
   
  strcpy(res, first);
  strcat(res,"\n");
  strcat(res,second);

  string_StringFree(first);
		 
  return res;
}

static void tptp_HandleComments(char * Comment) 
/**************************************************************
  INPUT:   A comment string.
  RETURNS: void.
  SUMMARY:   
  Takes care of reading some useful information from the comments
    that appear in the file.
  MEMORY: Frees the given string.
***************************************************************/
{
  char* str;
	
  if (!(tptp_StatusRead) && strstr(Comment,"Status")) {
    if (strstr(Comment,"Unsatisfiable"))
      tptp_Description->status = DFG_UNSATISFIABLE;
    else if (strstr(Comment,"Satisfiable"))
      tptp_Description->status = DFG_SATISFIABLE;
    else if (strstr(Comment,"Theorem"))
      tptp_Description->status = DFG_UNSATISFIABLE;
    else
      tptp_Description->status = DFG_UNKNOWNSTATE;
  
    tptp_StatusRead = TRUE;
  }
  
  if (!(tptp_Description->name) && strstr(Comment,"Names")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;
      tptp_Description->name = string_StringCopy(str);
    }
  }
  
  if (!(tptp_Description->author) && strstr(Comment,"Source")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;
      tptp_Description->author = string_StringCopy(str);
    }	 
  }
   
  if (!(tptp_Description->version) && strstr(Comment,"Version")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;
      tptp_Description->version = string_StringCopy(str);
    }	 
  }
  
  if (!tptp_DomainRead && strstr(Comment,"Domain")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;

      if (!(tptp_Description->description)) {
        tptp_Description->description = string_StringCopy(str);
      } else {
        tptp_Description->description = tptp_NewlinedAppend(tptp_Description->description,str);
      }

      tptp_DomainRead = TRUE;
    }	 
  }
  
  if (!tptp_ProblemRead && strstr(Comment,"Problem")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;

      if (!(tptp_Description->description)) {
	tptp_Description->description = string_StringCopy(str);
      } else {
	tptp_Description->description = tptp_NewlinedAppend(tptp_Description->description,str);
      }

      tptp_ProblemRead = TRUE;
    }	 
  }  
  
  if (tptp_EnglishReading) {
    if ((strlen(Comment) > 3) && (Comment[1] == ' ') && (Comment[2] == ' ') ) {
      int pos;

      pos = 3;
      while (Comment[pos] == ' ')
	pos++;
      tptp_Description->description = tptp_NewlinedAppend(tptp_Description->description,Comment+pos);
    } else {
      tptp_EnglishReading = FALSE;
      tptp_EnglishRead = TRUE;
    }
  }
    
  if (!tptp_EnglishRead && !tptp_EnglishReading && strstr(Comment,"English")) {
    str = strstr(Comment,": ");
    if (str) {
      str += 2;
	  
      if (!(tptp_Description->description)) {
	tptp_Description->description = string_StringCopy(str);
      } else { 
	tptp_Description->description = tptp_NewlinedAppend(tptp_Description->description,str);
      }	  			  
	  
      tptp_EnglishReading = TRUE;
    }	 
  }

  if (tptp_output) {
    fputs(Comment,tptp_output);
    fputs("\n",tptp_output);
  }

  string_StringFree(Comment);
}

static BOOL is_dfg_char(char c) 
/**************************************************************
  INPUT:   A character.
  RETURNS: Whether the given character can be part of dfg identifier.
***************************************************************/
{
  return (((c >= 'a') && (c <= 'z')) || 
	  ((c >= 'A') && (c <= 'Z')) ||
	  ((c >= '0') && (c <= '9')) ||
	  (c == '_'));
}
	
static const char* string_ToFind;
static BOOL tptp_DfgReservedLookupTest(POINTER p) {
  int idx;
  idx = (int)p;
  return string_Equal(string_ToFind,tptp_dfg_reserveds[idx]);  
}

static const char * const tptp_distinguisher = "__dfg";

static char * tptp_Identifierify(char * symbol) 
/**************************************************************
  INPUT:   A string.
  RETURNS: Transformed string.
  SUMMARY: 
  Transforms a string into a dfg identifier by handling unsupported characters
  and adding a special suffix so that the result isn't a dfg keyword accidentally.
  
  MEMORY:  The original string gets freed.
***************************************************************/
{
  POINTER LookupIdx;
  char c;
  int specials, len, big_len;
	
  char * result;	
  char * input;
  char * output;
	
  char tmpbuf[5];
		
  specials = 0;
  len = 0;

  /*count special characters*/
  input = symbol;
  while((c = *input++)) {
    len++;
    if (!is_dfg_char(c))
      specials++;
  }

  if ((len >= strlen(tptp_distinguisher)) &&
      (strstr(symbol + (len-strlen(tptp_distinguisher)),tptp_distinguisher) != NULL)) {
    misc_UserWarning("Symbol '%s' ends with '%s'. A possible ambiguity may arise!\n",symbol,tptp_distinguisher);
  }
	
  /*each special gets expanded by a factor of at most 5 and we also append the suffix in the end*/
  big_len = (len + 5*specials+6);
  result = (char*)memory_Malloc(big_len);
	
  input = symbol;
  output = result;

  while((c = *input++)) {
    if (is_dfg_char(c)) { /*just copy*/
      *output = c;
      output++;
    } else {
      if (output != result) { /*no underscore at the very beginning*/
	*output = '_';
	output++;
      }

      *output = 'a'; /*"a" stands for ascii */
      output++;

      sprintf(tmpbuf,"%d",(int)c);
      *output = '\0';
      strcat(output,tmpbuf);
      output += strlen(tmpbuf);

      *output = '_';
      output++;
    }
  }
	
  *output = '\0';

  string_ToFind = result;
  LookupIdx = hm_Retrieve(tptp_dfg_reserved_speedup,hm_StringHash(result),tptp_DfgReservedLookupTest);
  if (LookupIdx != HASHMAP_NO_RETRIEVE)
    strcat(output,tptp_distinguisher);
	
  string_StringFree(symbol);
	
  /*We probably overestimated the length,
    so lets rather copy again so that we return a string whose memory is just as long as needed*/
  output = result;
  result = string_StringCopy(output);
  memory_Free(output, big_len);

  return result;
}	

static void tptp_HandleFormula(char* name, char* role, TERM formula, BOOL cnf)
/**************************************************************
  INPUT:   Formula name, formula role, the actual formula,
           and boolean flag denoting if the formula is in cnf (a clause).
  RETURNS: Nothing.
  SUMMARY: 
  The formula is stored appropriately according to its tptp role
  and everything else is freed.
***************************************************************/
{
  LIST pair;
  TPTP_FORMULATYPE cur_type;

  cur_type = cnf ? TPTP_CNF : TPTP_FOF;

  if ((tptp_LastFormulaType != TPTP_UNDEF) && (tptp_LastFormulaType != cur_type)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("File mixes clauses and general first order formulas near line %d!\n",tptp_lineno);
    misc_FinishUserErrorReport();
  }

  tptp_LastFormulaType = cur_type;

  if (tptp_TranslateIdents)
    name = tptp_Identifierify(name); /* so that the formula name doesn't conflict with dfg reserved words */
    
  /*TODO: place some emphasis on the hypothesis formulae or other?*/
  if (string_Equal(role,"axiom") || 
      /*
	%----"axiom"s are accepted, without proof. There is no guarantee that the
	%----axioms of a problem are consistent.
      */
      string_Equal(role,"hypothesis") ||
      /*
	%----"hypothesis"s are assumed to be true for a particular problem, and are
	%----used like "axiom"s.
      */
      string_Equal(role,"lemma" ) ||
      string_Equal(role,"theorem" ) || 
      /*
	"lemma"s and "theorem"s have been proven from the "axiom"s. They can be
	%----used like "axiom"s in problems, and a problem containing a non-redundant
	%----"lemma" or theorem" is ill-formed. They can also appear in derivations.
	%----"theorem"s are more important than "lemma"s from the user perspective.
      */
      string_Equal(role,"definition" ) ||
      /*
	%----"definition"s are used to define symbols, and are used like "axiom"s.
      */
      string_Equal(role,"assumption" )
      /*
	%----"assumption"s can be used like axioms, but must be discharged before a
	%----derivation is complete.
      */
      ) {
    pair        = list_PairCreate(name, formula);
    tptp_Axioms = list_Cons(pair,tptp_Axioms);

  } else if (!strcmp(role,"conjecture")) {
    pair = list_PairCreate(name, formula);

    if (cnf) {
      misc_UserWarning("Formula role 'conjecture' in CNF format - formula skipped near line %d.\n",tptp_lineno);

      string_StringFree(name);
      term_Delete(formula);

    } else {
      tptp_Conjectures = list_Cons(pair,tptp_Conjectures);
    }
   
  } else if (!strcmp(role,"negated_conjecture")){ /*handled exactly the same as "conjecture", but only in cnf mode*/

    if (cnf) {
      pair = list_PairCreate(name, formula);
      
      tptp_Conjectures = list_Cons(pair, tptp_Conjectures);
    } else {
      misc_UserWarning("Formula role 'negated_conjecture' in FOF format - formula skipped near line %d.\n",tptp_lineno);
      
      string_StringFree(name);
      term_Delete(formula);    
    }
  } else {
    misc_UserWarning("Unknown formula role: %s - formula skipped near line %d.\n",role,tptp_lineno);

    string_StringFree(name);
    term_Delete(formula);    
  }

  string_StringFree(role);

  tptp_RestartVarList();
}

static TERM tptp_NormalizeLiterals(TERM term, BOOL negate)
/**************************************************************
  INPUT: A term and a flag denoting if the term should be negated.
  RETURNS: The transformed term.
  SUMMARY: 
  Resolves the problem of having negated equality sign as atomic formula in tptp.
  When creating a literal we either delete double negation, or add only one.
  The resulting thing doesn't contain "nequal" any more.
***************************************************************/
{
  BOOL negated_inside;
  SYMBOL main_symbol;

  main_symbol = term_TopSymbol(term);
          
  if (symbol_Equal(main_symbol,fol_NonEquality())) { /*it is negated already*/
    negated_inside = TRUE;

    term_RplacTop(term,fol_Equality());
  } else {
    negated_inside = FALSE;
  }

  if ((negate && !negated_inside)||(!negate && negated_inside)) {
    return term_Create(fol_Not(),list_List(term));                    
  } else
    return term;
}

static TERM tptp_HandleAtomic(TERM Atom)
/**************************************************************
  INPUT: A term to become an atominc formula.
  RETURNS: The same term.
  SUMMARY: Ensures that the outermost symbol is a predicate symbol
    and the inner ones are function symbols. 
***************************************************************/
{
  SYMBOL s;

  s = term_TopSymbol(Atom);

  if (!symbol_IsPredicate(s)) {    
    if (symbol_Fixed(s)) {
      misc_StartUserErrorReport();
      misc_UserErrorReport("Parse error near line %d - '%s' is not a predicate!\n", tptp_lineno,symbol_Name(s));	  	      
      misc_FinishUserErrorReport();
    } else {
      /* First occurrence, so change it to a predicate */
      s = symbol_ChangeType(s, symbol_PREDICATE);      
      term_RplacTop(Atom, s);
    }
  }   

  return Atom;
}

static __inline__ void tptp_CheckArity(SYMBOL s, int ArgNum, const char* Name) {   
  if (symbol_Arity(s) != ArgNum) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("Symbol '%s/%d' used with different arity on line %d.\n", Name, symbol_Arity(s),tptp_lineno);
    misc_FinishUserErrorReport();
  }
}

static SYMBOL tptp_GetSymbol(char * Name, int ArgNum, TPTP_SYMBOLKIND Kind)
/**************************************************************
  INPUT: A string name (which might not be a valid dfg identifier),
         number of arguments,
         and a kind (denoting where it comes from in the parse tree).
  RETURNS: A symbol to represent the described object.
  MEMORY: The Name string gets freed.	
***************************************************************/
{
	
  SYMBOL s;
	
  if (Kind != TPTP_ORDINARY) { /*We have something special*/
    if (Kind == TPTP_DEFINED) {
      if (string_Equal(Name,"$true")) {
	s = fol_True();
	tptp_CheckArity(s,ArgNum,Name);
        string_StringFree(Name);
        return s;
      }

      if (string_Equal(Name,"$false")) {
	s = fol_False();
	tptp_CheckArity(s,ArgNum,Name);
        string_StringFree(Name);
        return s;
      }
			
      misc_UserWarning("defined_functor '%s' encountered near line %d - treated as normal one!\n", Name, tptp_lineno);			
    } else if (Kind == TPTP_SYSTEM) {
      misc_UserWarning("system_functor '%s' encountered near line %d - treated as normal one!\n", Name, tptp_lineno);			
    }			
  }

  if (tptp_TranslateIdents)
    Name = tptp_Identifierify(Name);

  if (Kind != TPTP_ORDINARY)
    misc_UserWarning("(translated to '%s')\n", Name);
	
  s = symbol_Lookup(Name);
  if (s == 0)
    s = symbol_CreateFunction(Name, ArgNum, symbol_STATLEX,
			      tptp_PRECEDENCE);

  tptp_CheckArity(s,ArgNum,Name);

  string_StringFree(Name);    /* was copied by symbol_CreateFunction */

  return s;
}

static TERM tptp_TermCreate(SYMBOL s, LIST Arguments)
{
  TERM   result;

  result = term_Create(s, Arguments);
  tptp_CheckArguments(result);
  
  return result;
}

static void tptp_HandleInclude(char * incl, LIST selection)
/**************************************************************
  INPUT: A string - file to include
         A list of strings - formula selection.         
  RETURNS: Nothing.
  EFFECT:
  Called when include section is resolved.
  A touple of the file name and the formula selection list
  is added to the includes list.
***************************************************************/
{
  LIST pair;

  pair          = list_PairCreate(incl,selection);
  tptp_Includes = list_Cons(pair,tptp_Includes);
}
	
  
static char * tptp_StripQuotes(char * str)
/**************************************************************
  INPUT: A string.
  RETURNS: A modifed string.
  EFFECT:
    Gets rid of leading and trailing qoutes of a string.
  MEMORY: Returns a newly allocated thing and frees the one destroyed.
***************************************************************/
{
  char * newstr;
  int len;

  len        = strlen(str);    
  str[len-1] = '\0'; /*one characer shorter from end*/

  newstr = string_StringCopy(str+1);    /*start duplicating from the second char*/

  memory_Free(str,len+1);

  return newstr;
}

void yyerror(const char *s )
/*Called by flex/bison when an error occurs*/
{ 
  misc_StartUserErrorReport();
  misc_UserErrorReport("%s on line %d at item \"%s\".\n", s, tptp_lineno, tptp_text);
  misc_FinishUserErrorReport();   
}

FILE* tptp_OpenFile(const char * FileName, char ** const DiscoveredName)
/**************************************************************
  INPUT: A string filename, and a pointer to char pointer
           to hold the fullpath name of the file 
           that was opened in the end (can be null).
  RETURNS: A opened file.
  EFFECT:
  Opens a file for reading.
  The file is searched for using the extended search mechanism
  wrt TPTP environment variable.
***************************************************************/
{
  return misc_OpenFileEnv(FileName,"r","TPTP",DiscoveredName);
}
 
static LIST tptp_TestList; /* list of strings used in nonmember tests */
	
static BOOL tptp_LabelFormulaPairIsNonmember(POINTER pair) {
  if (list_PairFirst(pair) == NULL)
    return TRUE;
	
  return !list_Member(tptp_TestList,list_PairFirst(pair),(BOOL (*)(POINTER, POINTER))string_Equal);
}

void tptp_DeleteLabelTermPair(POINTER pair) 
{
  term_Delete(list_PairSecond(pair));	
  if (list_PairFirst(pair) != NULL)
    string_StringFree(list_PairFirst(pair));  /* Free the label */
  list_PairFree(pair);  
}

LIST tptp_TPTPParser(FILE* File, FLAGSTORE Flags, PRECEDENCE Precedence, DFGDESCRIPTION Description,
		     LIST* Axioms, LIST* Conjectures, LIST* SortDecl,
		     LIST* UserDefinedPrecedence, LIST* UserDefinedSelection,
		     LIST* ClAxRelation, BOOL* HasPlainClauses)
/**************************************************************
  A stub around the real parser that takes care of following
  include directives.
  
  NOTE: This function is almost the same as dfg_DFGParser form dfgparser.y
    any change in its implementation should propably be also propagated there.
***************************************************************/
{
  LIST Includes, Clauses;
  LIST FilesRead;
  DFGDESCRIPTION description_dummy;
  TPTP_FORMULATYPE old_LastFormulaType;

  FilesRead = list_Nil();
  Includes = list_Nil();	

  Clauses = tptp_TPTPParserIncludesExplicit(File,Flags,Precedence,Description,Axioms,Conjectures,SortDecl,UserDefinedPrecedence,UserDefinedSelection,ClAxRelation,&Includes,HasPlainClauses);
	
  while (list_Exist(Includes)) {
    LIST pair;
    char* filename;
    LIST selection;

    pair      = list_Top(Includes);
    filename  = (char*)list_PairFirst(pair);
    selection = (LIST)list_PairSecond(pair);
    list_PairFree(pair);
    Includes = list_Pop(Includes);
		
    if (list_Member(FilesRead,filename,(BOOL (*)(POINTER, POINTER))string_Equal)) {
      misc_UserWarning("File %s already included, skipped!\n",filename);
      string_StringFree(filename);
    } else {
      LIST Axs, Conjs, Cls, UDS, CAR;
      BOOL HPC;
      FILE* FileToInclude;
				
      FileToInclude = tptp_OpenFile(filename,NULL);

      Axs = Conjs = UDS = CAR = list_Nil();

      old_LastFormulaType = tptp_LastFormulaType;

      description_dummy = desc_Create();
      Cls = tptp_TPTPParserIncludesExplicit(FileToInclude, Flags, Precedence, description_dummy, &Axs, &Conjs, SortDecl, UserDefinedPrecedence, &UDS, &CAR, &Includes, &HPC);
      desc_Delete(description_dummy);

      if ((old_LastFormulaType != TPTP_UNDEF) &&
          (tptp_LastFormulaType != TPTP_UNDEF) &&
          (old_LastFormulaType != tptp_LastFormulaType)) {
	misc_StartUserErrorReport();
	misc_ErrorReport("Clauses and general first order formulas mixed across includes!\n");
	misc_FinishUserErrorReport();
      }

      if (old_LastFormulaType != TPTP_UNDEF) { /*the last thing was more specific than current*/
        tptp_LastFormulaType = old_LastFormulaType; /*if we override non-undef then only with the same value that was there already*/
      }
          
      if (list_Exist(selection)) { /*use the selection to filter Axs and Conjs */
        dfg_FilterClausesBySelection(&Cls,&CAR,selection);
        
        /* filtering Axs and Conjs */
	tptp_TestList = selection;
	Axs = list_DeleteElementIfFree(Axs,tptp_LabelFormulaPairIsNonmember,tptp_DeleteLabelTermPair);
	Conjs = list_DeleteElementIfFree(Conjs,tptp_LabelFormulaPairIsNonmember,tptp_DeleteLabelTermPair);
      }

      Clauses = list_Nconc(Clauses, Cls);

      *Axioms = list_Nconc(*Axioms,Axs);
      *Conjectures = list_Nconc(*Conjectures,Conjs);

      /* "Summing up" UserDefinedSelection and ClAxRelation from all the files inluded. */
      *UserDefinedSelection = list_Nconc(*UserDefinedSelection, UDS);
      *ClAxRelation = list_Nconc(*ClAxRelation, CAR);

      /*The whole thing has plain clauses only if all the files have!*/			
      if (!HPC)
	*HasPlainClauses = FALSE;

      misc_CloseFile(FileToInclude,filename);
      FilesRead = list_Cons(filename,FilesRead);
    }

    list_DeleteWithElement(selection,(void (*)(POINTER))string_StringFree);		
  }
		
  list_DeleteWithElement(FilesRead,(void (*)(POINTER))string_StringFree);		
  return Clauses;
}

LIST tptp_TPTPParserIncludesExplicit(FILE* File, FLAGSTORE Flags, PRECEDENCE Precedence, DFGDESCRIPTION Description,
				     LIST* Axioms, LIST* Conjectures, LIST* SortDecl,
				     LIST* UserDefinedPrecedence, LIST* UserDefinedSelection,
				     LIST* ClAxRelation, LIST* Includes, BOOL* HasPlainClauses)
/**************************************************************
  INPUT:   The input file containing clauses or formulae in TPTP syntax,
           a flag store, a precedence used to memorize settings
	       from the file, and Description to store problem description.
           Axioms, Conjectures, SortDecl, UserDefinedPrecedence
           UserDefinedSelection, and ClAxRelation, and Includes are
	   pointers to lists used as return values.
           HasPlainClauses is a return value to indicate if
           the problem had clauses in the plain format.
  RETURNS: The list of clauses from File.
  EFFECT:  Reads formulae and clauses from the input file.
           The axioms, conjectures, sort declarations, user-defined
	   precedences, and includes are appended to the respective lists,
       the lists are not deleted!
	   The Includes list contains pairs (filename, selection),
	   where selection is a list of names of formulas chosen to include.
	   All lists contain pairs
	   (label, term), where <label> may be NULL, if no
	   label was specified for that term.
	   <UserDefinedPrecedence> contains symbols sorted by decreasing
	   precedence. This list will only be changed, if the precedence
	   is explicitly defined in the input file. This can be done
	   by the 'set_precedence' flag in the SPASS settings list in
	   the DFG input file.
           <UserDefinedSelection> is set to a list of predicates to be
           selected in clause inferences by the 'set_selection' flag
           <ClAxRelation> is set to a clause, axiom relation where the
           clauses are given by their number, the axioms by name (string)
  NOTE: This funtions reads a tptp file and returns things like if it read
        a dfg file. Results concerning features not supported in tptp are 
        returned via empty lists and so on.
***************************************************************/
{
  LIST Clauses;

  tptp_PRECEDENCE = Precedence;
  tptp_VARLIST    = list_Nil();  
    	  
  tptp_Description = Description;
  tptp_LastFormulaType = TPTP_UNDEF; /*No formula read yet.*/
	  
  /*For parsing comments.*/
  tptp_StatusRead     = FALSE;
  tptp_DomainRead     = FALSE;
  tptp_ProblemRead    = FALSE;
  tptp_EnglishRead    = FALSE;
  tptp_EnglishReading = FALSE;	  
	  
  tptp_Axioms      = list_Nil();
  tptp_Conjectures = list_Nil();
  tptp_Includes    = list_Nil();
    
  tptp_in = File;

  yyparse();

  tptp_output          = NULL;    /*keep it in a consistent state - preserve the dafault for next time*/
  tptp_TranslateIdents = TRUE;    /*keep it in a consistent state - preserve the dafault for next time*/
  
  /*Axioms and conjectures and includes are now in opposite order than in the original file - let's reverse them back*/
  tptp_Axioms = list_NReverse(tptp_Axioms);
  tptp_Conjectures = list_NReverse(tptp_Conjectures);
  tptp_Includes = list_NReverse(tptp_Includes);
  
  if (tptp_WasParsingCNF()) { 
    dfg_CreateClausesFromTerms(&tptp_Axioms,&tptp_Conjectures,ClAxRelation,TRUE,Flags,Precedence);
    Clauses = list_Nconc(tptp_Axioms, tptp_Conjectures);
    tptp_Axioms = list_Nil();
    tptp_Conjectures = list_Nil();
  } else
    Clauses = list_Nil();
      
  *Axioms = list_Nconc(*Axioms,tptp_Axioms);
  *Conjectures = list_Nconc(*Conjectures,tptp_Conjectures);
  *Includes = list_Nconc(*Includes,tptp_Includes);

  /* Cleanup */  
  tptp_RestartVarList();

  *HasPlainClauses = FALSE;  
  
  return Clauses;
}

BOOL tptp_WasParsingCNF(void)
/**************************************************************
  RETURNS:
    Whether the last parsing parsed only clauses (TRUE)
      or even first full order formulae (FALSE)      
***************************************************************/
{
  return (tptp_LastFormulaType == TPTP_CNF); /* else it was undef (and nothing was read) or fof*/
}

void tptp_SetParserOutput(FILE* output)
/**************************************************************
  INPUT:
   A opened file to be used for outputting comments.
  EFFECT:
  The parser will output encountered header comments to this file.
  This function need not be called
   - then the parser will not output anything.
***************************************************************/
{
  tptp_output = output;
}

void tptp_SetDoTranslateIdents(BOOL flag)
/**************************************************************
  INPUT:
   A boolean flag indicating whether the indentifiers should
    be translated to be "dfg complient".
  EFFECT:
   Sets up the the flag for the next parser invocation.
   By default, the indentifiers will get translated.  
***************************************************************/
{
  tptp_TranslateIdents = flag;
}

static TERM tptp_VarTermCreate(char* Name)
{
  SYMBOL s;

  s = tptp_VarLookup(Name);
  return term_Create(s, list_Nil());
}

static void tptp_CheckArguments(TERM Term)
{
  LIST scan;
  SYMBOL argsymbol;

  for (scan = term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) {
    argsymbol = term_TopSymbol(list_Car(scan));
    if (symbol_IsPredicate(argsymbol)) {
      misc_StartUserErrorReport();
      misc_UserErrorReport("Term '%s' has predicate term '%s' as argument near line %d\n", 
			   symbol_Name(term_TopSymbol(Term)), symbol_Name(argsymbol), tptp_lineno);            
      misc_FinishUserErrorReport();
    }
    if (!symbol_IsVariable(argsymbol)) {
      symbol_SetFixed(argsymbol,TRUE); /*it is a function a it should remain one*/
    }
  }
}

/**************************************************************/
/* Functions for the Variable Table                           */
/**************************************************************/

typedef struct {
  char*  name;
  SYMBOL symbol;
} TPTP_VARENTRY, *TPTP_VARIABLE;

static __inline__ char* tptp_VarName(TPTP_VARIABLE Entry)
{
  return Entry->name;
}

static __inline__ SYMBOL tptp_VarSymbol(TPTP_VARIABLE Entry)
{
  return Entry->symbol;
}

static SYMBOL tptp_VarCreate(char* Name)
{
  TPTP_VARIABLE item;

  item         = (TPTP_VARIABLE) memory_Malloc(sizeof(TPTP_VARENTRY));
  item->name   = Name;
  item->symbol = symbol_CreateStandardVariable();
  tptp_VARLIST = list_Cons(item, tptp_VARLIST);

  return item->symbol;
}

static void tptp_VarFree(TPTP_VARIABLE Entry)
{
  string_StringFree(Entry->name);
  memory_Free(Entry, sizeof(TPTP_VARENTRY));
}

static void tptp_RestartVarList(void)
{
  list_DeleteWithElement(tptp_VARLIST, (void (*)(POINTER))tptp_VarFree);
  tptp_VARLIST = list_Nil();
  symbol_ResetStandardVarCounter();
}

static SYMBOL tptp_VarLookup(char* Name)
/**************************************************************
  INPUT:   A variable name.
  RETURNS: The corresponding variable symbol.
  EFFECT:  If the variable name occurred before, the corresponding
           symbol is returned and the <Name> is freed.
           If the variable name didn't occur
           a new variable is created.
	   Every occurrence of the special variable "_" generates
           a new variable symbol.
***************************************************************/
{
  LIST scan;

  if (!string_Equal(Name, "_")) {
    for (scan = tptp_VARLIST; !list_Empty(scan); scan = list_Cdr(scan)) {
      if (string_Equal(Name, tptp_VarName(list_Car(scan)))) {
	string_StringFree(Name);
	return tptp_VarSymbol(list_Car(scan));
      }
    }
  }
  /* Create a new variable */
  return tptp_VarCreate(Name);
}