#include <stdio.h>
#include <stdlib.h>


#define BIG	500000L
#define NUMFIELDS 2000L
#define FIELDLENGTH 2000L
#define LEMSIZE 15

enum vtag {
	fac,
	maison
} vtag;

enum vtag version = maison;

enum tag {	// 
	Section,
	End,
	Require,
	Theorem,
	Axiom,
	Definition,
	Remark,
	URemark,
	OutRemark,
	Property,
	Parameter,
	Variable,
	Variables,
	Hypothesis,
	Local,
	Hint,
	Hints,
	Proof,
	Record,
	Lemma,
	Fact,
	Save,
	Chapter,
	tooShort,
	comment,
	other,
	empty,
	Database,	// my own but mimicks a coq command
	Comment,
	Precompiler,	// to turn on or off the precompiler or give other instructions
	DefineP,
	DefineE,
	Result,	// this means the actual statement of a hypothesis
	
	unknown,
	sorted,	// for the dictionary
	notsorted,
	set,	// for FREEVAR
	notset,
	internal,
	external
	
} tag;

typedef struct FIELD {
	// firstspace and lastspace refer to the places in the
	// normalizedData array
	int fs;	// firstspace
	int ls;	// lastspace
	
	

} FIELD;

typedef struct SUBSTLIST {
	// a list of occurences of an iv in a clause
	int occurences[LEMSIZE];
	int occurencesL;
	
	

} SUBSTLIST;



typedef struct COQLINE {

	
	FIELD f;
	enum tag LineType; // says what type of line it is
	int opensection;	// 1 says it is in an open section
	
	
} COQLINE;

typedef struct DIENTRY {

	FIELD f;
	FIELD newf;
	
	int lineReference;	// the COQLINE to look at when looking
						// for the guy
	int newlineReference;

	enum tag sortstatus;
	enum tag newsortstatus;
	enum tag ReferenceType;	// the type of the line where it occurs
	
	
	
	
	
	
} DIENTRY;

typedef struct FREEVAR {
	FIELD name;
	FIELD instance;
	FIELD type;
	enum tag status;
	enum tag kind;
	enum tag oldkind;

} FREEVAR;

typedef struct CLAUSE {
	FIELD written;
	FIELD resultName;	// in case it gets successfully instantiated
	int trylow;
	int tryhigh;
	int trycurrent;
	int occs[(LEMSIZE * LEMSIZE) +10];
	int occsL;

} CLAUSE;





char* aPin;
char* aPout;


char* normalizedData;	// this is the file once it has been normalized





COQLINE* CoqLines;
// initialize BIG elements here

DIENTRY* Dictionary;


// toggles for the output format
int debugToggle;	// 0 = only math; 1 =some errors, 2 = all stuff
int newlineToggle; // 0 = \n, 1 = \r\n , 2 = \n\r
int factToggle;	// 0 = remark, 1 = fact
int extensionToggle; // 0 = .html, 1 = .v

int debugThreshold;	// for comparison with debugToggle



int DictionaryL, DictionaryNL, DictionarySpace;
enum tag isitsorted;




int aPinL, aPoutL, normalizedDataL, CoqLinesL;
int normalizedDataL2;



int normalizedDataSpace;	// how much space we have allocated
int aPinSpace;
int aPoutSpace;
int CoqLinesSpace;


char filecontents[50];
FILE  *ourfile;

char currentFilename[200];
int currentFilenameL;

int totalK;

int CheckFieldToggle;

FIELD loadedFields[NUMFIELDS + 10];
FIELD loadedFields2[NUMFIELDS+ 10];
char fieldWritten[FIELDLENGTH+10];
char fieldWritten2[FIELDLENGTH+10];	
char fieldWritten3[FIELDLENGTH+10];	
char fieldWritten4[FIELDLENGTH+10];	


int loadedFieldsL, loadedFields2L, fieldWrittenL, fieldWritten2L;
int fieldWritten3L, fieldWritten4L;
int fieldWrittenB, fieldWritten2B;	// last line breaks


// the following constitute the lemma which is currently loaded
FREEVAR freeVariable[NUMFIELDS + 10];
CLAUSE lemmaClause[LEMSIZE + 10];
FIELD lemmaConclusion;
FIELD conclusionName;
FIELD lemmaName;
int conclusionVariable[NUMFIELDS + 10]; 

FIELD outRemarkName;

SUBSTLIST ivOccurence[LEMSIZE][LEMSIZE];
SUBSTLIST ivInConclusion[LEMSIZE];

int freeVariableL, lemmaClauseL, lemmaClauseT, conclusionVariableL;
// end currently loaded lemma

int maxIndex;	// the max index that is already in the file

int chapterLine[1000];
int chapterLineL;


int sectionDepth;

// weird punctuation guesses

char backslash = '\\';
char apost = '\''; 	
char doublequote = '\"'; 	
char backaccent = '`';


// functions



void InitArrays(int filesize);
void NormalizeData();
int CheckCase(char ourch);
void AddCharToNormData(char ch);
void AddCharToNormData2(char ch);
void AddUnitToNormData(char ch);

void AnalyseData1();
void AnalyseLine1(int theline);
int MyStringCompare(char *string1, char *string2);
void PrintNDtoScreen(int firstplace, int afterlast);
void LoadLineNumber(int number);
void PrintLoadedFieldsToScreen();
void PrintField(FIELD ourfield);
void WriteField(FIELD ourfield);
void WriteField2(FIELD ourfield);
void WriteField3(FIELD ourfield);
void WriteField4(FIELD ourfield);
void MyAppendField(FIELD ourfield);
void MyAppendField2(FIELD ourfield);
void PrintLineType(int theline);
void WriteString(char *thestring);
void WriteString2(char *thestring);
void MyAppendString(char *thestring);
void MyAppendString2(char *thestring);
void PotentialBreak();
void PotentialBreak2();
void WriteEnumTag(enum tag thetag);
void OutputString(char *thestring);
void AnalyseLine4(int theline);
void OutputField(FIELD thefield);
void PrintOutputToFile(char* fname);

FIELD GetHeadLine(FIELD thefield);

int GetFirstLineBreak(FIELD thefield);
void CheckField(FIELD thefield);
void InitCoqLine(FIELD thefield);
FIELD InteriorField(FIELD thefield);
int GetFieldBreak(FIELD thefield);
void LoadField(FIELD thefield);
void LoadField2(FIELD thefield);
void AnalyseField(FIELD thefield);
void AnalyseField2(FIELD thefield);
void PrintFieldBounds(FIELD ourfield);
void MainShell();
int CheckCurrentFile();
void TreatSpecify();
void TreatLook();

void GoodOutputField(FIELD thefield);
void GoodWriteField(FIELD thefield);

void AddDictionaryElement(int theline);
void SetRemainingStuff(int entry);
void AddRestOfDictionary();

void AddToPreDictionary(FIELD thefield, int theline);
int MyCompareFields(FIELD fieldA, FIELD fieldB);
void MiniSortDictionary();
void RearrangeDictionary();
void SortDictionary();
void AddRestOfDictionary();
void SetOpensection();
int LookUp(FIELD thefield);
int LookUpString(char *thestring);
int LookUpPropertySome(FIELD thefield);

int ComparePropOfEntry(FIELD thefield, int theentry);
int LookUpPropertyLow(FIELD thefield);
int LookUpPropertyHigh(FIELD thefield);

void ApplyLemma(int theline);
int LoadLemma(int theline);
int TryClauses();

void MyAppendInt(int theint);
void MyAppendInt2(int theint);
void SetMaxIndex();

void InitToggles();
void TreatToggles();
void OutputNewline();

void SendOutputToFile();

void TreatLemDef();
void AnalyseLine5(int theline);
void AddDictionaryElement5(int theline);


void ApplyDefinition(int theline);

void ApplyProperty();
void ApplyANDProperty();


int CheckFieldBoundType(FIELD thefield);

int BreakDownLine(int theline);

void TreatEndSec();

int ReadInputFromFile();
int LoadIntVariables(FIELD varfield);
void DecomposeField(FIELD thefield);
void DecomposeField2(FIELD thefield);
void GoodDecomposeField(FIELD thefield, int thecl);

int LoadAnyVariables(FIELD varfield);
void MyAppendVariables();
void MyAppendVariablesNB();
void TreatExport();
void MaybeOutputRemark(char *thmwritten);
void TreatZExport();
void AnalyseLineZ(int theline);


//////////////////// functions start here ////////////



void InitArrays(int filesize){
	// does calloc for each of the arrays we need
	// exits if there is a problem (so after this we can
	// assume that our arrays are ok)
	
	
	
	totalK = 0;


	aPinSpace = filesize;

	aPin = (char*) calloc(aPinSpace+100, sizeof(char));
	totalK = totalK + ((aPinSpace+100) * sizeof(char));
	if(aPin == NULL){
		printf("memory allocation for aPin failed\n");
		exit(1);
	}
	
	aPinL = 0;

	aPoutSpace = BIG;
	
	aPout = (char*) calloc(aPoutSpace+100, sizeof(char));
	totalK = totalK + ((aPoutSpace+100) * sizeof(char));
	if(aPout == NULL){
		printf("memory allocation for aPout failed\n");
		exit(1);
	}
	
	aPoutL = 0;

	normalizedDataSpace = 3*filesize;
	
	normalizedData = (char*) calloc(normalizedDataSpace+ 100, sizeof(char));
	totalK = totalK + ((normalizedDataSpace+ 100) * sizeof(char));
	if(normalizedData == NULL){
		printf("memory allocation for normalizedData failed\n");
		exit(1);
	}
	
	normalizedDataL = 0;
	
	CoqLinesSpace = BIG;
	
	CoqLines = (COQLINE*) calloc(CoqLinesSpace +100, sizeof(COQLINE));
	totalK = totalK + ((CoqLinesSpace + 100) * sizeof(COQLINE));
	if(CoqLines == NULL){
		printf("memory allocation for CoqLines failed\n");
		exit(1);
	}
	
	CoqLinesL = 0;

	
	
	DictionarySpace = BIG;
	
	Dictionary = (DIENTRY*) 
		calloc(DictionarySpace +100, sizeof(DIENTRY));
	totalK = totalK + ((DictionarySpace + 100) * sizeof(DIENTRY));
	if(Dictionary == NULL){
		printf("memory allocation for Dictionary failed\n");
		exit(1);
	}
	
	DictionaryL = 0;
	
	
	
	printf("initialized %dK of memory\n", totalK);
	
	

	

}






int MyStringCompare(char *string1, char *string2){
	// assume the length is < 100 characters
	// and that they are null-terminated
	// returns 0 if equal, + or - 1 otherwise

	int i;
	char ch1, ch2;

	i=0;
	while (i<100){
		ch1 = string1[i];
		ch2 = string2[i];

		if (ch1 == 0){
			if(ch2 == 0){
				return 0;
			}
			else{
				return 1;
			}

		}
		else{
			if (ch2 == 0){
				return -1;
			}

		}
		if (ch1 > ch2) return 1;
		if (ch2 > ch1) return -1;
		i = i+1;
	}

	return 0;

}

int CheckCase(char ourch){
	// returns 0 if not a letter, 1 if uppercase, 2 if lowercase
	// for now try assuming that the character values for uppercase letters are all in 
	// a row (so that this program goes faster).
	// returns 3 if it is an underline _,
	// returns 4 if it is another special coq character eg (,_,etc.
	// returns 5 if it is a space
	
	int answer;
	
	char Avalue, Zvalue, avalue, zvalue;
	
	Avalue = 'A';
	Zvalue = 'Z';
	avalue = 'a';
	zvalue = 'z';
	
	answer = 0;
	if (ourch <= Zvalue){
		if (ourch >= Avalue){
			answer = 1;
		
		}
	
	}
	
	if (ourch <= zvalue){
		if (ourch >= avalue){
			answer = 2;
		
		}
	
	}

	if (ourch == '_') answer = 3;
	if (ourch == '0') answer = 3;
	if (ourch == '1') answer = 3;
	if (ourch == '2') answer = 3;
	if (ourch == '3') answer = 3;
	if (ourch == '4') answer = 3;
	if (ourch == '5') answer = 3;
	if (ourch == '6') answer = 3;
	if (ourch == '7') answer = 3;
	if (ourch == '8') answer = 3;
	if (ourch == '9') answer = 3;
	if (ourch == apost) answer = 3;

	if (ourch == '(') answer = 4;
	if (ourch == '[') answer = 4;
	if (ourch == ')') answer = 4;
	if (ourch == ']') answer = 4;
	if (ourch == '{') answer = 4;
	if (ourch == '}') answer = 4;
	if (ourch == ':') answer = 4;
	if (ourch == '.') answer = 4;
	if (ourch == '-') answer = 4;
	if (ourch == ';') answer = 4;
	if (ourch == ',') answer = 4;
	if (ourch == '>') answer = 4;
	if (ourch == '=') answer = 4;
	if (ourch == '?') answer = 4;



	if (ourch == ' ') answer = 5;



	
	return answer;
	
	

}


void AddCharToNormData(char ch){
	if (normalizedDataL > (normalizedDataSpace - 100)){
		printf("\n  normalizedData too big, bye\n");
		exit(1);
	
	}
	
	if (normalizedDataL <0){
		printf("\n  normalizedDataL negative (don't know why), bye \n");
		exit(1);
	
	}
	normalizedData[normalizedDataL] = ch;
	normalizedDataL = normalizedDataL + 1;


}

void AddCharToNormData2(char ch){
	if (normalizedDataL2 > (normalizedDataSpace - 100)){
		printf("\n  normalizedData too big, bye\n");
		exit(1);
	
	}
	
	if (normalizedDataL2 <0){
		printf("\n  normalizedDataL2 negative (don't know why), bye \n");
		exit(1);
	
	}
	normalizedData[normalizedDataL2] = ch;
	normalizedDataL2 = normalizedDataL2 + 1;


}

void AddUnitToNormData(char ch){
	// adds the whole unit consisting of spaces before and after
	// the character
	// note  unfortunately that := is transformed to :  =
	// similarly -> to -  > etc
	
	if (CheckCase(ch) == 4) AddCharToNormData(' ');

	if (CheckCase(ch) > 0) AddCharToNormData(ch);

	if (CheckCase(ch) == 4) AddCharToNormData(' ');

	if (ch == '\n') AddCharToNormData(' ');	

}

void NormalizeData(){
	//adds space around parentheses then contracts extra spaces
int i;
char ch, ch2, ch3;


normalizedDataL = 0;
	AddCharToNormData(' ');
	AddCharToNormData(' ');
	// first we add in the brut characters with
	// eventual surrounding spaces 
	for (i=0; i< aPinL; i++){
			ch = aPin[i];
			AddUnitToNormData(ch);
	}
	AddCharToNormData(' ');
	// next we take out extra spaces
	// note that the first two chars are automatically
	// spaces so we can start at i=1
	// the function AddCharToNormData2 uses the
	// pointer normalizedDataL2
	normalizedDataL2 = 0;

	AddCharToNormData2(' ');
	for (i=1; i<normalizedDataL; i++){
		ch = normalizedData[i];
		ch2 = normalizedData[i-1];
		if (ch == ' '){
			if (ch2 != ' ') AddCharToNormData2(ch);
		}
		else{
			AddCharToNormData2(ch);
		}


	}

	normalizedDataL = normalizedDataL2;
	
	// now we contract := and -> 
	//
	if (normalizedDataL > 3){
	normalizedDataL2 = 0;
	AddCharToNormData2(' ');
	for (i=1; i<normalizedDataL -1; i++){
		ch = normalizedData[i];
		ch2 = normalizedData[i-1];
		ch3 = normalizedData[i+1];
		if (ch == ' '){
			if ((ch2 == ':') && (ch3 == '=')){
			
			} 
			else{
			if ((ch2 == '-') && (ch3 == '>')){
			
			} 
			else{
				AddCharToNormData2(ch);
			}
			
			}
		}
		else{
			AddCharToNormData2(ch);
		}


	}
	AddCharToNormData2(' ');
	normalizedDataL = normalizedDataL2;
	}	// end normalizedDataL > 3
	

	//printf("\nwrote %d characters to normalizedData\n", normalizedDataL);

}

void InitCoqLine(FIELD thefield){

	
	
	CheckField(thefield);
	
	if (CoqLinesL > (CoqLinesSpace - 100)){
		printf("\n  too many lines, bye\n");
		exit(1);
	
	}
	
	if (CoqLinesL <0){
		printf("\n  CoqLinesL negative (don't know why), bye \n");
		exit(1);
	
	}
	
	
	CoqLines[CoqLinesL].f.fs = thefield.fs;
	CoqLines[CoqLinesL].f.ls = thefield.ls;
	
	CoqLinesL = CoqLinesL + 1;
}

void CheckField(FIELD thefield){
	if(CheckFieldToggle == 1){
		PrintFieldBounds(thefield);
	}
	if (thefield.fs < 0){
		printf("\nCheckField generates error 1\n");
		printf("\n thefield.fs = %d\n", thefield.fs);
		printf("\n thefield.ls = %d\n", thefield.ls);
		exit(1);
	}
	if (thefield.ls >= normalizedDataL){
		printf("\nCheckField generates error 2\n");
		printf("\n thefield.fs = %d\n", thefield.fs);
		printf("\n thefield.ls = %d\n", thefield.ls);
		exit(1);
	}
	if (thefield.ls < thefield.fs){
		printf("\nCheckField generates error 3\n");
		printf("\n thefield.fs = %d\n", thefield.fs);
		printf("\n thefield.ls = %d\n", thefield.ls);
		exit(1);
	}
	if (normalizedData[thefield.fs] != ' '){
		printf("\nCheckField generates error 4\n");
		printf("\n thefield.fs = %d\n", thefield.fs);
		printf("\n thefield.ls = %d\n", thefield.ls);
		exit(1);
	}
	if (normalizedData[thefield.ls] != ' '){
		printf("\nCheckField generates error 4\n");
		printf("\n thefield.fs = %d\n", thefield.fs);
		printf("\n thefield.ls = %d\n", thefield.ls);
		exit(1);
	}

}


int GetFirstLineBreak(FIELD thefield){
	// gets the breaking space of the first line

	int i;
	int parcount;
	int regular;	// 1 if a regular line i.e. ends with period, 0 if a parenthesized expression
	
	CheckField(thefield);
	
	if (thefield.fs == thefield.ls) return thefield.fs;
	
	if (thefield.ls == (thefield.fs + 1)) return thefield.ls;
	
	regular = 1;
	if (normalizedData[thefield.fs + 1] == '(') regular = 0;
	if (normalizedData[thefield.fs + 1] == '[') regular = 0;
	
	
	if (regular == 1){
		for (i= thefield.fs + 1; i< thefield.ls; i++){
			if (normalizedData[i] == '.') return i+1;
		}
	
	}
	else{
		parcount = 0;
		for (i= thefield.fs + 1; i<= thefield.ls; i++){
			if (normalizedData[i] == '(') parcount = parcount + 1;
			if (normalizedData[i] == '[') parcount = parcount + 1;
			if (normalizedData[i] == '{') parcount = parcount + 1;
			if (normalizedData[i] == ')') parcount = parcount - 1;
			if (normalizedData[i] == ']') parcount = parcount - 1;
			if (normalizedData[i] == '}') parcount = parcount - 1;
			if (normalizedData[i] == ' '){
				if (parcount == 0) return i;
			}
		}
	
	}
	
	return thefield.ls;
	
	

}

FIELD GetHeadLine(FIELD thefield){
	int linebreak;
	FIELD answer;
	
	linebreak = GetFirstLineBreak(thefield);
	answer.fs = thefield.fs;
	answer.ls = linebreak;
	
	return answer;
	
}



void AnalyseData1(){
	// divides up the data into CoqLines and stores them in the
	// CoqLine array. This part just stores the lines.
	
	FIELD globalfield;
	
	int linebreak;
	
	if (normalizedDataL < 2){
		printf("\nthe file  looks too small\n");
		exit(1);
	}
	
	globalfield.fs = 0;
	globalfield.ls = normalizedDataL-1;
	
	// for degugging :
	//CheckFieldToggle = 1;
	
	CheckField(globalfield);
	
	while(globalfield.fs < globalfield.ls){
		
		CheckField(GetHeadLine(globalfield));
		InitCoqLine(GetHeadLine(globalfield));
		linebreak = GetFirstLineBreak(globalfield);
		if (linebreak <= globalfield.fs) break;
		globalfield.fs = linebreak;
	}
	
	
}

FIELD InteriorField(FIELD thefield){
	char ch1,ch2;
	FIELD answer;
	if (thefield.ls < thefield.fs +4) return thefield;
	
	ch1 = normalizedData[thefield.fs + 1];
	ch2 = normalizedData[thefield.ls - 1];
	
	if ((ch1 == '(') && (ch2 == ')')){
		answer.fs = thefield.fs + 2;
		answer.ls = thefield.ls - 2;
		return answer;
	}
	if ((ch1 == '[') && (ch2 == ']')){
		answer.fs = thefield.fs + 2;
		answer.ls = thefield.ls - 2;
		return answer;
	}
	if ((ch1 == '{') && (ch2 == '}')){
		answer.fs = thefield.fs + 2;
		answer.ls = thefield.ls - 2;
		return answer;
	}
	return thefield;

}

int GetFieldBreak(FIELD thefield){
	// returns the first break space 
	int parcount;
	char ch;
	int i;
	
	CheckField(thefield);
	if (thefield.ls < thefield.fs + 1) return thefield.fs;
	
	parcount = 0;
	for (i=thefield.fs + 1; i <= thefield.ls; i++){
		ch = normalizedData[i];
		if (ch == '(') parcount = parcount + 1;
		if (ch == '[') parcount = parcount + 1;
		if (ch == '{') parcount = parcount + 1;
		if (ch == ')') parcount = parcount - 1;
		if (ch == ']') parcount = parcount - 1;
		if (ch == '}') parcount = parcount - 1;
		if (ch == ' '){
			if (parcount == 0) return i;
		}
		
	} 
	return thefield.ls;
}

void LoadField(FIELD thefield){
	// loads to the loadedFields variable
	
	if (loadedFieldsL > NUMFIELDS - 1){
		printf("\nfield not loaded, out of room\n");
		return;
	}
	if (loadedFieldsL < 0){
		printf("\nloadedFieldsL error\n");
		exit(1);
	}
	loadedFields[loadedFieldsL].fs = thefield.fs;
	loadedFields[loadedFieldsL].ls = thefield.ls;
	loadedFieldsL = loadedFieldsL + 1;
	
}

void LoadField2(FIELD thefield){
	// loads to the loadedFields2 variable
	
	if (loadedFields2L > NUMFIELDS - 1){
		printf("\nfield not loaded, out of room\n");
		return;
	}
	if (loadedFields2L < 0){
		printf("\nloadedFields2L error\n");
		exit(1);
	}
	loadedFields2[loadedFields2L].fs = thefield.fs;
	loadedFields2[loadedFields2L].ls = thefield.ls;
	loadedFields2L = loadedFields2L + 1;
	
}

void DecomposeField(FIELD thefield){
	// breaks the field into all its little components ignoring
	// parenthetization.

	FIELD littlefield;
	int lastsep;
	int i;
	char ch;

	loadedFieldsL=0;
	
	if (thefield.ls < thefield.fs + 2){
		LoadField(thefield);
		return;
	}
	lastsep = thefield.fs;

	for (i=thefield.fs + 1; i<= thefield.ls; i++){
		ch = normalizedData[i];
		if (ch == ' '){
			littlefield.fs = lastsep;
			littlefield.ls = i;
			LoadField(littlefield);
			lastsep = i;
		}

	}
	
	
	
}

void DecomposeField2(FIELD thefield){
	// breaks the field into all its little components ignoring
	// parenthetization.

	FIELD littlefield;
	int lastsep;
	int i;
	char ch;

	loadedFields2L=0;
	
	if (thefield.ls < thefield.fs + 2){
		LoadField2(thefield);
		return;
	}
	lastsep = thefield.fs;

	for (i=thefield.fs + 1; i<= thefield.ls; i++){
		ch = normalizedData[i];
		if (ch == ' '){
			littlefield.fs = lastsep;
			littlefield.ls = i;
			LoadField2(littlefield);
			lastsep = i;
		}

	}
	
	
	
}


void AnalyseField(FIELD thefield){
	// analyses the field into component fields which are loaded to loadedFields
	
	FIELD globalfield;
	FIELD thecomp;
	int linebreak;

	loadedFieldsL=0;
	
	if (thefield.ls < thefield.fs + 2){
		LoadField(thefield);
		return;
	}
	
	globalfield.fs = thefield.fs;
	globalfield.ls = thefield.ls;
	
	while(globalfield.fs < globalfield.ls){
		linebreak = GetFieldBreak(globalfield);
		thecomp.fs = globalfield.fs;
		thecomp.ls = linebreak;
		LoadField(thecomp);
		if (linebreak <= globalfield.fs) break;
		globalfield.fs = linebreak;
	}
	
	
}

void AnalyseField2(FIELD thefield){
	// analyses the field into component fields which are loaded to loadedFields2
	
	FIELD globalfield;
	FIELD thecomp;
	int linebreak;

	loadedFields2L=0;
	
	if (thefield.ls < thefield.fs + 2){
		LoadField2(thefield);
		return;
	}
	
	globalfield.fs = thefield.fs;
	globalfield.ls = thefield.ls;
	
	while(globalfield.fs < globalfield.ls){
		linebreak = GetFieldBreak(globalfield);
		thecomp.fs = globalfield.fs;
		thecomp.ls = linebreak;
		LoadField2(thecomp);
		if (linebreak <= globalfield.fs) break;
		globalfield.fs = linebreak;
	}	
}


void LoadLineNumber(int number){
	// loads the line into the loadedFields variable
	

	
	FIELD linefield;
	

	linefield.fs = CoqLines[number].f.fs;
	linefield.ls = CoqLines[number].f.ls;
	
	CheckField(linefield);

	AnalyseField(linefield);

}

void PrintLoadedFieldsToScreen(){
	int numberToPrint;

	int i;

	numberToPrint = loadedFieldsL;
	if (numberToPrint > 20) numberToPrint = 20;

	printf("\n    Loaded Fields (fs/ls) :\n");
	for (i=0; i< numberToPrint; i++){
		printf(" (%d-", loadedFields[i].fs);
		printf("%d)", loadedFields[i].ls);

	}
	printf("\n");


}

void WriteField(FIELD ourfield){
	// writes the field to fieldWritten string
	// doesnt include the first or last characters
	int i;
	char ch;

	fieldWrittenL = 0;
	fieldWrittenB = 0;
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWrittenL < FIELDLENGTH){
			fieldWritten[fieldWrittenL] = ch;
			fieldWrittenL = fieldWrittenL + 1;
		}

	}
	if (fieldWrittenL >= FIELDLENGTH + 1) fieldWrittenL = FIELDLENGTH;
	fieldWritten[fieldWrittenL] = 0;


}

void MyAppendField(FIELD ourfield){
	// appends the field to fieldWritten string
	// doesnt include the first or last characters
	int i;
	char ch;

	

	if (fieldWrittenL < 0) return;
	
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWrittenL < FIELDLENGTH){
			fieldWritten[fieldWrittenL] = ch;
			fieldWrittenL = fieldWrittenL + 1;
		}

	}
	if (fieldWrittenL >= FIELDLENGTH + 1) fieldWrittenL = FIELDLENGTH;
	fieldWritten[fieldWrittenL] = 0;


}

void WriteField2(FIELD ourfield){
	// writes the field to fieldWritten2 string
	// doesnt include the first or last characters
	int i;
	char ch;

	fieldWritten2L = 0;
	fieldWritten2B = 0;
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWritten2L < FIELDLENGTH){
			fieldWritten2[fieldWritten2L] = ch;
			fieldWritten2L = fieldWritten2L + 1;
		}

	}
	if (fieldWritten2L >= FIELDLENGTH + 1) fieldWritten2L = FIELDLENGTH;
	fieldWritten2[fieldWritten2L] = 0;


}

void WriteField3(FIELD ourfield){
	// writes the field to fieldWritten2 string
	// doesnt include the first or last characters
	int i;
	char ch;

	fieldWritten3L = 0;
	
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWritten3L < FIELDLENGTH){
			fieldWritten3[fieldWritten3L] = ch;
			fieldWritten3L = fieldWritten3L + 1;
		}

	}
	if (fieldWritten3L >= FIELDLENGTH + 1) fieldWritten3L = FIELDLENGTH;
	fieldWritten3[fieldWritten3L] = 0;


}

void WriteField4(FIELD ourfield){
	// writes the field to fieldWritten2 string
	// doesnt include the first or last characters
	int i;
	char ch;

	fieldWritten4L = 0;
	
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWritten4L < FIELDLENGTH){
			fieldWritten4[fieldWritten4L] = ch;
			fieldWritten4L = fieldWritten4L + 1;
		}

	}
	if (fieldWritten4L >= FIELDLENGTH + 1) fieldWritten4L = FIELDLENGTH;
	fieldWritten4[fieldWritten4L] = 0;


}

void MyAppendField2(FIELD ourfield){
	// writes the field to fieldWritten2 string
	// doesnt include the first or last characters
	int i;
	char ch;

	

	if (fieldWritten2L < 0) return;
	
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWritten2L < FIELDLENGTH){
			fieldWritten2[fieldWritten2L] = ch;
			fieldWritten2L = fieldWritten2L + 1;
		}

	}
	if (fieldWritten2L >= FIELDLENGTH + 1) fieldWritten2L = FIELDLENGTH;
	fieldWritten2[fieldWritten2L] = 0;


}

void GoodWriteField(FIELD ourfield){
	// writes the field to fieldWritten string
	// doesnt include the first or last characters
	// the Good version contracts spaces after openpars
	// or before closepars.

	int i;
	char ch, ch1, ch2;

	fieldWrittenL = 0;
	for (i= ourfield.fs + 1; i<ourfield.ls; i++){
		ch = normalizedData[i];
		if (fieldWrittenL < FIELDLENGTH){
			if (ch != ' '){
				fieldWritten[fieldWrittenL] = ch;
				fieldWrittenL = fieldWrittenL + 1;
			}
			else{	// ch == ' '
				ch1 = normalizedData[i-1];
				ch2 = normalizedData[i+1];
				if ((ch1 != '(') && (ch1 != '[') && (ch1 != '{')){
				if ((ch2 != ')') && (ch2 != ']') && (ch2 != '}')&&(ch2 != ',')){
					fieldWritten[fieldWrittenL] = ch;
					fieldWrittenL = fieldWrittenL + 1;
				}
				}

			}
		}

	}
	if (fieldWrittenL >= FIELDLENGTH + 1) fieldWrittenL = FIELDLENGTH;
	fieldWritten[fieldWrittenL] = 0;


}

int MyCompareFields(FIELD fieldA, FIELD fieldB){
	WriteField3(fieldA);
	WriteField4(fieldB);
	return MyStringCompare(fieldWritten3, fieldWritten4);

}

void PrintField(FIELD ourfield){
	WriteField(ourfield);
	printf("%s, ", fieldWritten);

}

void PrintFieldBounds(FIELD ourfield){
	printf(" (%d-",ourfield.fs);
	printf("%d)", ourfield.ls);
}

void PrintLineType(int theline){

	if (theline < 0){
		printf("\n linenumber error %d\n", theline);
		return;
	}
	if (theline >= CoqLinesL){
		printf("\n linenumber error %d\n", theline);
		return;
	}
	
	WriteEnumTag(CoqLines[theline].LineType);
	printf("line %d ", theline);
	printf(" has type %s", fieldWritten);

}



void WriteString(char *thestring){
	int i;
	char ch;
	fieldWrittenL=0;
	fieldWrittenB = 0;
	for (i=0; i<FIELDLENGTH; i++){
		ch = thestring[i];
		fieldWritten[fieldWrittenL]= ch;
		if (ch == 0) break;
		fieldWrittenL = fieldWrittenL +1;
		if (fieldWrittenL > FIELDLENGTH) break;
		
	}
	fieldWritten[fieldWrittenL]=0;

}

void WriteString2(char *thestring){
	int i;
	char ch;
	fieldWritten2L=0;
	fieldWritten2B = 0;
	for (i=0; i<FIELDLENGTH; i++){
		ch = thestring[i];
		fieldWritten2[fieldWritten2L]= ch;
		if (ch == 0) break;
		fieldWritten2L = fieldWritten2L +1;
		if (fieldWritten2L > FIELDLENGTH) break;
		
	}
	fieldWritten2[fieldWritten2L]=0;

}

void MyAppendString(char *thestring){
	int i;
	char ch;
	
	if (fieldWrittenL < 0) return;
	
	for (i=0; i<FIELDLENGTH; i++){
		ch = thestring[i];
		fieldWritten[fieldWrittenL]= ch;
		if (ch == 0) break;
		fieldWrittenL = fieldWrittenL +1;
		if (fieldWrittenL > FIELDLENGTH) break;
	
	}
	fieldWritten[fieldWrittenL]=0;

}

void MyAppendString2(char *thestring){
	int i;
	char ch;
	
	if (fieldWritten2L < 0) return;
	
	for (i=0; i<FIELDLENGTH; i++){
		ch = thestring[i];
		fieldWritten2[fieldWritten2L]= ch;
		if (ch == 0) break;
		fieldWritten2L = fieldWritten2L +1;
		if (fieldWritten2L > FIELDLENGTH) break;
		
	}
	fieldWritten2[fieldWritten2L]=0;

}

void MyAppendInt(int theint){
	// appends its decimal notation to the string
	// fieldWritten
	// maxi 5 decimals, has to be positive

	

	int d_0;
	int d_1;
	int d_2;
	int d_3;
	int d_4;
	int remainder, count;
	char ch;
	char num[6];

	if (theint < 0){
		MyAppendString("NEG");
		return;
	}
	if (theint >= 100000){
		MyAppendString("BIG");
		return;
	}

	remainder = theint;
	count = 0;

	
	d_4 = 0;
	while (((10000L * (d_4 +1)) <= remainder) && (d_4 < 9)){
		d_4 = d_4+1;
		count = count +1;
		if (count >15) break;
	}
	d_3 = 0;
	remainder = remainder - (d_4 * 10000);
	while (((1000L * (d_3 +1)) <= remainder) && (d_3 < 9)){
		d_3 = d_3+1;
		count = count +1;
		if (count >25) break;
	}
	d_2 = 0;
	remainder = remainder - (d_3 * 1000);
	while (((100L * (d_2+1)) <= remainder) && (d_2 < 9)){
		d_2 = d_2+1;
		count = count +1;
		if (count >35) break;
	}
	d_1 = 0;
	remainder = remainder - (d_2 * 100);
	while (((10L * (d_1 +1)) <= remainder) && (d_1 < 9)){
		d_1 = d_1+1;
		count = count +1;
		if (count >45) break;
	}
	d_0 = remainder - (d_1 * 10);

	if ((d_4 < 0)|(d_4 > 9)){
		MyAppendString("ERR");
		return;
	}
	if ((d_3 < 0)|(d_3 > 9)){
		MyAppendString("ERR");
		return;
	}
	if ((d_2 < 0)|(d_2 > 9)){
		MyAppendString("ERR");
		return;
	}
	if ((d_1 < 0)|(d_1 > 9)){
		MyAppendString("ERR");
		return;
	}
	if ((d_0 < 0)|(d_0 > 9)){
		MyAppendString("ERR");
		return;
	}

	ch = '0';
	num[0] = ch + d_4;
	num[1] = ch + d_3;
	num[2] = ch + d_2;
	num[3] = ch + d_1;
	num[4] = ch + d_0;
	num[5] = 0;

	MyAppendString(num);



}

void MyAppendInt2(int theint){
	// appends its decimal notation to the string
	// fieldWritten2
	// maxi 5 decimals, has to be positive

	

	int d_0;
	int d_1;
	int d_2;
	int d_3;
	int d_4;
	int remainder, count;
	char ch;
	char num[6];

	if (theint < 0){
		MyAppendString2("NEG");
		return;
	}
	if (theint >= 100000){
		MyAppendString2("BIG");
		return;
	}

	remainder = theint;
	count = 0;

	
	d_4 = 0;
	while (((10000L * (d_4 +1)) <= remainder) && (d_4 < 9)){
		d_4 = d_4+1;
		count = count +1;
		if (count >15) break;
	}
	d_3 = 0;
	remainder = remainder - (d_4 * 10000);
	while (((1000L * (d_3 +1)) <= remainder) && (d_3 < 9)){
		d_3 = d_3+1;
		count = count +1;
		if (count >25) break;
	}
	d_2 = 0;
	remainder = remainder - (d_3 * 1000);
	while (((100L * (d_2+1)) <= remainder) && (d_2 < 9)){
		d_2 = d_2+1;
		count = count +1;
		if (count >35) break;
	}
	d_1 = 0;
	remainder = remainder - (d_2 * 100);
	while (((10L * (d_1 +1)) <= remainder) && (d_1 < 9)){
		d_1 = d_1+1;
		count = count +1;
		if (count >45) break;
	}
	d_0 = remainder - (d_1 * 10);

	if ((d_4 < 0)|(d_4 > 9)){
		MyAppendString2("ERR");
		return;
	}
	if ((d_3 < 0)|(d_3 > 9)){
		MyAppendString2("ERR");
		return;
	}
	if ((d_2 < 0)|(d_2 > 9)){
		MyAppendString2("ERR");
		return;
	}
	if ((d_1 < 0)|(d_1 > 9)){
		MyAppendString2("ERR");
		return;
	}
	if ((d_0 < 0)|(d_0 > 9)){
		MyAppendString2("ERR");
		return;
	}

	ch = '0';
	num[0] = ch + d_4;
	num[1] = ch + d_3;
	num[2] = ch + d_2;
	num[3] = ch + d_1;
	num[4] = ch + d_0;
	num[5] = 0;

	MyAppendString2(num);



}

void PotentialBreak(){
	// checks to see if we are near where we should do a newline
	// using the last breakpoint fieldWrittenB
	
	if (fieldWrittenL < (fieldWrittenB + 50)) return;
	
	if (newlineToggle == 0){
		MyAppendString("\n");
		fieldWrittenB = fieldWrittenL;
	}
	if (newlineToggle == 1){
		MyAppendString("\r\n");
		fieldWrittenB = fieldWrittenL;
	}

	if (newlineToggle == 2){
		MyAppendString("<br>");
		fieldWrittenB = fieldWrittenL;
	}

}

void PotentialBreak2(){

	if (fieldWritten2L < (fieldWritten2B + 50)) return;
	
	if (newlineToggle == 0){
		MyAppendString2("\n");
		fieldWritten2B = fieldWritten2L;
	}
	if (newlineToggle == 1){
		MyAppendString2("\r\n");
		fieldWritten2B = fieldWritten2L;
	}

	if (newlineToggle == 2){
		MyAppendString2("<br>");
		fieldWritten2B = fieldWritten2L;
	}

}




void OutputString(char *thestring){

	char ch;
	int cursor;

	if (debugThreshold > debugToggle) return;

	cursor = 0;
	if (aPoutL < 0){
		printf("OutputString error\n");
		
	}
	while (aPoutL < aPoutSpace){
		ch = thestring[cursor];
		if (ch == 0) break;
		aPout[aPoutL]= ch;
		aPoutL = aPoutL + 1;
		cursor = cursor + 1;
	}

}

void OutputField(FIELD thefield){
	WriteField(thefield);
	OutputString(fieldWritten);
}

void GoodOutputField(FIELD thefield){
	GoodWriteField(thefield);
	OutputString(fieldWritten);
}


void AnalyseLine1(int theline){
	


	
	
	enum tag answer;

	if (theline < 0){
		printf("\n linenumber error %d\n", theline);
		exit(1);
	}
	if (theline >= CoqLinesL){
		printf("\n linenumber error %d\n", theline);
		exit(1);
	}
	
	
	LoadLineNumber(theline);
	if (loadedFieldsL <= 0){
		CoqLines[theline].LineType = empty;
		CoqLines[theline].opensection = 0;
		return;
	}
	//for debugging:
	//printf("\nline %d has fields:\n", theline);
	//PrintLoadedFieldsToScreen();
	//
	WriteField(loadedFields[0]);
	answer = comment;
	
	// first here are the regular Coq commands
	if (MyStringCompare(fieldWritten, "Section") == 0) answer = Section;
	if (MyStringCompare(fieldWritten, "End") == 0) answer = End;
	if (MyStringCompare(fieldWritten, "Require") == 0) answer = Require;
	if (MyStringCompare(fieldWritten, "Theorem") == 0) answer = Theorem;
	if (MyStringCompare(fieldWritten, "Axiom") == 0) answer = Axiom;
	if (MyStringCompare(fieldWritten, "Definition") == 0) answer = Definition;
	if (MyStringCompare(fieldWritten, "Remark") == 0) answer = Remark;
	if (MyStringCompare(fieldWritten, "Parameter") == 0) answer = Parameter;
	if (MyStringCompare(fieldWritten, "Variable") == 0) answer = Variable;
	if (MyStringCompare(fieldWritten, "Variables") == 0) answer = Variables;
	if (MyStringCompare(fieldWritten, "Hypothesis") == 0) answer = Hypothesis;
	if (MyStringCompare(fieldWritten, "Local") == 0) answer = Local;
	if (MyStringCompare(fieldWritten, "Hint") == 0) answer = Hint;
	if (MyStringCompare(fieldWritten, "Hints") == 0) answer = Hints;
	if (MyStringCompare(fieldWritten, "Proof") == 0) answer = Proof;
	if (MyStringCompare(fieldWritten, "Record") == 0) answer = Record;
	if (MyStringCompare(fieldWritten, "Lemma") == 0) answer = Lemma;
	if (MyStringCompare(fieldWritten, "Fact") == 0) answer = Fact;
	if (MyStringCompare(fieldWritten, "Save") == 0) answer = Save;
	if (MyStringCompare(fieldWritten, "URemark") == 0) answer = URemark;
	if (MyStringCompare(fieldWritten, "OutRemark") == 0) answer = OutRemark;
	if (MyStringCompare(fieldWritten, "Property") == 0) answer = Property;

	if (MyStringCompare(fieldWritten, "Chapter") == 0) answer = Chapter;
	
	if (MyStringCompare(fieldWritten, "RProperty") == 0) answer = Property;
	if (MyStringCompare(fieldWritten, "RLemma") == 0) answer = Lemma;
	if (MyStringCompare(fieldWritten, "RAxiom") == 0) answer = Axiom;
	if (MyStringCompare(fieldWritten, "RParameter") == 0) answer = Parameter;
	if (MyStringCompare(fieldWritten, "RDefinition") == 0) answer = Definition;
	
	
	
	
	
	
	
	CoqLines[theline].LineType = answer;
	

}


void WriteEnumTag(enum tag thetag){
	// sends to fieldWritten
	WriteString("???");
	if (thetag == Section) WriteString("Section");
	if (thetag == End) WriteString("End");
	if (thetag == Require) WriteString("Require");
	if (thetag == Theorem) WriteString("Theorem");
	if (thetag == Axiom) WriteString("Axiom");
	if (thetag == Definition) WriteString("Definition");
	if (thetag == Remark) WriteString("Remark");
	if (thetag == Parameter) WriteString("Parameter");
	if (thetag == Variable) WriteString("Variable");
	if (thetag == Variables) WriteString("Variables");
	if (thetag == Hypothesis) WriteString("Hypothesis");
	if (thetag == Local) WriteString("Local");
	if (thetag == Hint) WriteString("Hint");
	if (thetag == Hints) WriteString("Hints");
	if (thetag == Proof) WriteString("Proof");
	if (thetag == Record) WriteString("Record");
	if (thetag == Lemma) WriteString("Lemma");
	if (thetag == Fact) WriteString("Fact");
	if (thetag == Save) WriteString("Save");
	if (thetag == tooShort) WriteString("tooShort");
	if (thetag == comment) WriteString("comment");
	if (thetag == other) WriteString("other");
	if (thetag == empty) WriteString("empty");
	if (thetag == Database) WriteString("Database");
	if (thetag == Comment) WriteString("Comment");
	if (thetag == Precompiler) WriteString("Precompiler");
	if (thetag == URemark) WriteString("URemark");
	if (thetag == OutRemark) WriteString("OutRemark");
	if (thetag == Property) WriteString("Property");
	if (thetag == Chapter) WriteString("Chapter");
	
	if (thetag == unknown) WriteString("unknown");


}

void AnalyseLine4(int theline){
	// we write out the lines in a standardized format...

	
	if (CoqLines[theline].opensection == 1){

	
	if (CoqLines[theline].LineType == Hypothesis){
		AddDictionaryElement(theline);
	}
	if (CoqLines[theline].LineType == Remark){
		AddDictionaryElement(theline);
	}
	if (CoqLines[theline].LineType == URemark){
		AddDictionaryElement(theline);
	}
	if (CoqLines[theline].LineType == OutRemark){
		AddDictionaryElement(theline);
	}
	if (CoqLines[theline].LineType == Fact){
		AddDictionaryElement(theline);
	}
	


	}	// end opensection == 1

	
	
}


void AnalyseLine5(int theline){
	// we write out the lines in a standardized format...

	
	if (CoqLines[theline].opensection == 1){

	if (CoqLines[theline].LineType == Definition){
		AddDictionaryElement5(theline);
	}
	
	if (CoqLines[theline].LineType == Property){
		AddDictionaryElement5(theline);
	}

	if (CoqLines[theline].LineType == Local){
		AddDictionaryElement5(theline);
	}

	if (CoqLines[theline].LineType == Lemma){
		AddDictionaryElement5(theline);
	}

	if (CoqLines[theline].LineType == Theorem){
		AddDictionaryElement5(theline);
	}
	
	if (CoqLines[theline].LineType == OutRemark){
		AddDictionaryElement5(theline);
	}
	

	}	// end opensection == 1

	
	
}

void AnalyseLineZ(int theline){
	// this is for the ZExport function
	// note that the function 
	// AddDictionaryElement5(theline)
	// adds the identifier with reference to the line number

	if (CoqLines[theline].LineType == Definition){
		AddDictionaryElement5(theline);
	}
	
	if (CoqLines[theline].LineType == Property){
		AddDictionaryElement5(theline);
	}

	if (CoqLines[theline].LineType == Lemma){
		AddDictionaryElement5(theline);
	}


}

void SetOpensection(){
	// sets the opensection parameter in CoqLines
	// this parameter is 1 if the line is in a section that is still open
	// at the end of the file.
	// thus we start from the back.
	// in the cases when the linetype is End or Section,
	// the Section commands for closed sections are given a value of 0
	// note that as a result of our algorithm, 
	//opensection is 1 for the base level
	

	int i;
	int currentlevel;
	int openlevel;

	currentlevel = 0;
	openlevel = 0;

	for (i= CoqLinesL - 1; i>= 0; i=i-1){
		if (CoqLines[i].LineType == End){
			currentlevel = currentlevel + 1;
		}
		if (currentlevel > openlevel){
			CoqLines[i].opensection = 0;
		}
		else{
			CoqLines[i].opensection = 1;
		}
		if (CoqLines[i].LineType == Section){
			currentlevel = currentlevel - 1;
		}
		if (currentlevel < openlevel) openlevel = currentlevel;

		
	}


}

void AddToPreDictionary(FIELD thefield, int theline){
	if (DictionaryL > DictionarySpace - 10) return;
	if (DictionaryL < 0) return;

	Dictionary[DictionaryL].f = thefield;
	Dictionary[DictionaryL].lineReference=theline;
	
	DictionaryL = DictionaryL + 1;
}

void AddDictionaryElement(int theline){
	// add the basic identifier to the dictionary
	// note that the identifier is always the second field
	// eg Theorem myth1 : jsjf.

	

	LoadLineNumber(theline);

	/*if (loadedFieldsL <3) return;
		
	AddToPreDictionary(loadedFields[1], theline);*/

	if (loadedFieldsL == 5){
		// here we add the results directly to the dictionary

	if (CoqLines[theline].LineType == Hypothesis){
		AddToPreDictionary(loadedFields[3], theline);
		AddToPreDictionary(InteriorField(loadedFields[3]), theline);
	}
	if (CoqLines[theline].LineType == Fact){
		AddToPreDictionary(loadedFields[3], theline);
		AddToPreDictionary(InteriorField(loadedFields[3]), theline);
	}
	if (CoqLines[theline].LineType == Remark){
		AddToPreDictionary(loadedFields[3], theline);
		AddToPreDictionary(InteriorField(loadedFields[3]), theline);
	}
	if (CoqLines[theline].LineType == URemark){
		AddToPreDictionary(loadedFields[3], theline);
		//AddToPreDictionary(InteriorField(loadedFields[3]), theline);
	}
	if (CoqLines[theline].LineType == OutRemark){
		AddToPreDictionary(loadedFields[3], theline);
		AddToPreDictionary(InteriorField(loadedFields[3]), theline);
	}

	}	// end loadedFieldsL ==5


}

void AddDictionaryElement5(int theline){
	// add the basic identifier to the dictionary
	// note that the identifier is always the second field
	// eg Theorem myth1 : jsjf.

	

	LoadLineNumber(theline);

	/*if (loadedFieldsL <3) return;
		
	AddToPreDictionary(loadedFields[1], theline);*/

	if (loadedFieldsL >2){
		// here we add the names directly to the dictionary

		AddToPreDictionary(loadedFields[1], theline);
		
	}	// end loadedFieldsL ==5


}





///////

void MiniSortDictionary(){
	// does one pass; the reordering is signified by the reference item; in this way we avoid
	// recopying the strings.
	
	// convention: the sortstatus says whether an element is sorted with respect to
	// the previous element.
	
	// need to do rearrange afterward.
	
	
		
	
	
	int cursor1, cursor2, cursor3, cursor4;
	
	FIELD entry1;
	FIELD entry3;
	int lineref1, lineref3;
	
	int lastcursor2, lastcursor3;
	
	int toggle;
	int val;
	
	if (DictionaryL <= 1) return;
	
	DictionaryNL = 0;
	
	lastcursor2 = 0;
	lastcursor3 = DictionaryL;
	
	printf("\n");
	
	while(lastcursor2 < lastcursor3){	// BIG WHILE
	
	// sets the cursors to the new positions
	cursor1 = lastcursor2;
	cursor2 = cursor1;
	cursor4 = lastcursor3;
	cursor3 = cursor4;
	
	
	
	toggle = 0;
	while (toggle == 0){
		cursor2 = cursor2 + 1;
		if (Dictionary[cursor2].sortstatus == notsorted) toggle = 1;
		if (cursor2 > lastcursor3) toggle = 1;
	}
	if (cursor2 >= DictionaryL) cursor2 = DictionaryL -1;
	
	toggle = 0;
	while (toggle == 0){
		cursor3 = cursor3 - 1;
		if (Dictionary[cursor3].sortstatus == notsorted) toggle = 1;
		if (cursor3 < lastcursor2) toggle = 1;
	}
	
	if (cursor3 < 0) cursor3 = 0;
	
	// now the cursors are set; 
	
	lastcursor2 = cursor2;
	lastcursor3 = cursor3;
	
	
	// now intercal the lists, putting the results into the new items in DIENTRY
	
	while((cursor1 < cursor2) && (cursor3 < cursor4)){
		entry1 = Dictionary[cursor1].f;
		entry3 = Dictionary[cursor3].f;
		lineref1 = Dictionary[cursor1].lineReference;
		lineref3 = Dictionary[cursor3].lineReference;
		val = MyCompareFields(entry1, entry3);
		
		if (val < 0){
			Dictionary[DictionaryNL].newf = entry1;
			Dictionary[DictionaryNL].newlineReference = lineref1;
			DictionaryNL++;
			cursor1 = cursor1 + 1;
		
		}
		if (val > 0){
			Dictionary[DictionaryNL].newf = entry3;
			Dictionary[DictionaryNL].newlineReference = lineref3;
			DictionaryNL++;
			cursor3 = cursor3 + 1;
		
		}
		if (val == 0){
			Dictionary[DictionaryNL].newf = entry3;
			if (lineref1 < lineref3){
				Dictionary[DictionaryNL].newlineReference = lineref1;
			}
			else{
				Dictionary[DictionaryNL].newlineReference = lineref3;
			}
			DictionaryNL++;
			cursor3 = cursor3 + 1;
			cursor1 = cursor1 + 1;
		
		}
		
		
	
	}
	
	
	
	
	while(cursor1 < cursor2){
		entry1 = Dictionary[cursor1].f;
		lineref1 = Dictionary[cursor1].lineReference;
		Dictionary[DictionaryNL].newf = entry1;
		Dictionary[DictionaryNL].newlineReference = lineref1;
		DictionaryNL++;
		cursor1 = cursor1 + 1;
	}
	
	
	
	while(cursor3 < cursor4){
		entry3 = Dictionary[cursor3].f;
		lineref3 = Dictionary[cursor3].lineReference;
		Dictionary[DictionaryNL].newf = entry3;
		Dictionary[DictionaryNL].newlineReference = lineref3;
		DictionaryNL++;
		cursor3 = cursor3 +1;
	}
	
	
	
	
	} 	// END BIG WHILE
	
	

}

void RearrangeDictionary(){
	// fixes things up again after minisort, also checks to see if it is sorted
	
	int i;
	int val;
	
	isitsorted = sorted;
	DictionaryL = DictionaryNL;

	
	
	
	
	
	for (i=0; i<DictionaryL; i++){
		
		Dictionary[i].f = Dictionary[i].newf;
		
		Dictionary[i].lineReference = Dictionary[i].newlineReference;
		if (i== 0) Dictionary[i].sortstatus = notsorted;
		if (i > 0){
	     val = MyCompareFields(Dictionary[i-1].f, Dictionary[i].f);
	     if (val >= 0){
	        Dictionary[i].sortstatus = notsorted;
	      	isitsorted = notsorted;
		
	     }
	     else{
	     	Dictionary[i].sortstatus = sorted;
	     }
	
		}
	}
	
	

}


void SortDictionary(){
	// sorts dictionary by repeatedly applying minisort (limit of 20 times)
	
	int count;
	
	count = 0;
	isitsorted = notsorted;
	
	printf("\nSort report:\n");
	
	while(isitsorted == notsorted){
		MiniSortDictionary();
		RearrangeDictionary();	// this sets isitsorted to sorted if the dictio is sorted
		printf("...sort");
		if(count == 7) printf("\n");
		if(count == 14) printf("\n");
		count = count + 1;
		if (count > 15) break;
	
	}
	
	if (isitsorted == sorted){
		printf("\nSort seems to have succeeded in %d tries\n", count);
	}
	else{
		printf("\nSort seems to have failed\n");
	
	}


}

int LookUp(FIELD thefield){
	// returns the number of the Dictionary entry;
	// returns -1 if the entry is not found
	// otherwise returns a value between 0 and DictionaryL
	// which hits thefield.

	int cursor1, cursor2, cursor3;
	int count;
	int val;

	if (DictionaryL <= 0) return -1;
	if (DictionaryL >= DictionarySpace) return -1;

	cursor1 = 0;
	cursor3 = DictionaryL - 1;

	count = 0;

	while (count < 20){
		cursor2 = (cursor1 + cursor3) / 2;
		if (cursor2 < cursor1) cursor2 = cursor1;
		if (cursor2 > cursor3) cursor2 = cursor3;
		if (cursor1 + 1 < cursor3){
			if (cursor2 == cursor1) cursor2 = cursor1 + 1;
			if (cursor2 == cursor3) cursor2 = cursor3 - 1;
		}
		val = MyCompareFields(thefield, Dictionary[cursor2].f);
		if (val < 0){
			cursor3 = cursor2 - 1;
			if (cursor3 < cursor1) return -1;
		}
		if (val == 0){
			if (cursor2 < 0) return -1;
			if (cursor2 >= DictionaryL) return -1;
			return cursor2;
		}
		if (val > 0){
			cursor1 = cursor2 + 1; 
			if (cursor1 > cursor3) return -1;
		}

		count = count + 1;

	}
	return -1;



}

int LookUpString(char *thestring){
	// returns the number of the Dictionary entry;
	// returns -1 if the entry is not found
	// otherwise returns a value between 0 and DictionaryL
	// which hits thefield.
	// note that this uses the fieldWritten2 variable!!!

	int cursor1, cursor2, cursor3;
	int count;
	int val;

	if (DictionaryL <= 0) return -1;
	if (DictionaryL >= DictionarySpace) return -1;

	cursor1 = 0;
	cursor3 = DictionaryL - 1;

	count = 0;

	while (count < 20){
		cursor2 = (cursor1 + cursor3) / 2;
		if (cursor2 < cursor1) cursor2 = cursor1;
		if (cursor2 > cursor3) cursor2 = cursor3;
		if (cursor1 + 1 < cursor3){
			if (cursor2 == cursor1) cursor2 = cursor1 + 1;
			if (cursor2 == cursor3) cursor2 = cursor3 - 1;
		}
		WriteField2(Dictionary[cursor2].f);
		val = MyStringCompare(thestring, fieldWritten2);
		if (val < 0){
			cursor3 = cursor2 - 1;
			if (cursor3 < cursor1) return -1;
		}
		if (val == 0){
			if (cursor2 < 0) return -1;
			if (cursor2 >= DictionaryL) return -1;
			return cursor2;
		}
		if (val > 0){
			cursor1 = cursor2 + 1; 
			if (cursor1 > cursor3) return -1;
		}

		count = count + 1;

	}
	return -1;



}



int LookUpPropertySome(FIELD thefield){
	// gives some element in the dictionary
	// that looks like ( thefield ... )
	// gives -1 if there arent any

		int cursor1, cursor2, cursor3;
	int count;
	int val;
	

	if (DictionaryL <= 0) return -1;
	if (DictionaryL >= DictionarySpace) return -1;

	cursor1 = 0;
	cursor3 = DictionaryL - 1;

	count = 0;

	while (count < 20){
		cursor2 = (cursor1 + cursor3) / 2;
		if (cursor2 < cursor1) cursor2 = cursor1;
		if (cursor2 > cursor3) cursor2 = cursor3;
		if (cursor1 + 1 < cursor3){
			if (cursor2 == cursor1) cursor2 = cursor1 + 1;
			if (cursor2 == cursor3) cursor2 = cursor3 - 1;
		}
		WriteField(thefield);
		MyAppendString(" ");
		WriteField2(Dictionary[cursor2].f);
		
		val = MyStringCompare(fieldWritten, fieldWritten2);

		AnalyseField(Dictionary[cursor2].f);
		if (loadedFieldsL > 0){
		if (MyCompareFields(thefield, loadedFields[0])==0) val = 0;
		}

		//val = MyCompareFields(thefield, Dictionary[cursor2].f);
		if (val < 0){
			cursor3 = cursor2 - 1;
			if (cursor3 < cursor1) return -1;
		}
		if (val == 0){
			if (cursor2 < 0) return -1;
			if (cursor2 >= DictionaryL) return -1;
			return cursor2;
		}
		if (val > 0){
			cursor1 = cursor2 + 1; 
			if (cursor1 > cursor3) return -1;
		}

		count = count + 1;

	}
	return -1;

}

int ComparePropOfEntry(FIELD thefield, int theentry){
	// compares thefield with the head property of
	// theentry

	AnalyseField(Dictionary[theentry].f);
	if (loadedFieldsL <= 0) return -1;
	return MyCompareFields(thefield, loadedFields[0]);
	

}

int LookUpPropertyLow(FIELD thefield){
	// returns the lowest dictionary entry where the
	// property occurs, if there is one; -1 otherwise

	int res, res2;
	int val;

	res = LookUpPropertySome(thefield);
	if (res < 0) return -1;
	if (res >= DictionaryL) return -1;



	while(res > 0){
		res2 = res -1;
		val = ComparePropOfEntry(thefield, res2);
		if (val == 0){
			res = res2;
		}
		else{
			break;
		}

	}

	val = ComparePropOfEntry(thefield, res);
	if (val == 0){
		return res;
	}
	else{
		return -1;
	}



}

int LookUpPropertyHigh(FIELD thefield){
	// returns the lowest dictionary entry where the
	// property occurs, if there is one; -1 otherwise

	int res, res2;
	int val;

	res = LookUpPropertySome(thefield);
	if (res < 0) return -1;
	if (res >= DictionaryL) return -1;


	while(res < DictionaryL -1){
		res2 = res +1;
		val = ComparePropOfEntry(thefield, res2);
		if (val == 0){
			res = res2;
		}
		else{
			break;
		}

	}

	val = ComparePropOfEntry(thefield, res);
	if (val == 0){
		return res;
	}
	else{
		return -1;
	}



}



////////////

void AddRestOfDictionary(){
	// sets the remaining important info in the dictionary
	int i;
	

	for (i=0; i<DictionaryL; i++){
		SetRemainingStuff(i);

	}


}




void SetRemainingStuff(int entry){
	// sets the remaining info in DIENTRY number entry, looking at the
	// appropriate line

	int lineref;


	if (entry < 0) return;
	if (entry >= DictionaryL) return;
	if (entry >= DictionarySpace) return;

	lineref = Dictionary[entry].lineReference;

	LoadLineNumber(lineref);

	if (CoqLines[lineref].LineType == Definition){
		Dictionary[entry].ReferenceType = Definition;
	}
	if (CoqLines[lineref].LineType == Lemma){
		Dictionary[entry].ReferenceType = Lemma;
	}
	if (CoqLines[lineref].LineType == Theorem){
		Dictionary[entry].ReferenceType = Theorem;
	}
	if (CoqLines[lineref].LineType == Hypothesis){
		Dictionary[entry].ReferenceType = Hypothesis;
	}
	if (CoqLines[lineref].LineType == Remark){
		Dictionary[entry].ReferenceType = Hypothesis;
	}
	if (CoqLines[lineref].LineType == Fact){
		Dictionary[entry].ReferenceType = Hypothesis;
	}
	if (CoqLines[lineref].LineType == URemark){
		Dictionary[entry].ReferenceType = URemark;
	}
	if (CoqLines[lineref].LineType == OutRemark){
		Dictionary[entry].ReferenceType = OutRemark;
	}
	if (CoqLines[lineref].LineType == Property){
		Dictionary[entry].ReferenceType = Property;
	}

	

}

int LoadAnyVariables(FIELD varfield){
	// takes a field and loads some variables from it;
	// returns -1 if it isnt a variable declaration.
	// note that this uses loadedFields2 !!! and fieldWritten2 

	int i,val;
	int colplace;
	FIELD typefield;
	enum tag varkind;

	val = CheckFieldBoundType(varfield);
	if (val == 0) varkind = internal;
	if (val == 1) varkind = internal;
	if (val == 2) varkind = external;

	AnalyseField2(InteriorField(varfield));
	colplace = -1;
	if (loadedFields2L < 3) return -1;
	for (i=0; i<loadedFields2L; i++){
		WriteField2(loadedFields2[i]);
		val = MyStringCompare(fieldWritten2, ":");
		if (val == 0){
			colplace = i;
			break;
		}
	}
	if (colplace < 0) return -2;
	for (i=1; i<colplace; i= i+ 2){
		WriteField2(loadedFields2[i]);
		val = MyStringCompare(fieldWritten2, ",");
		if (val != 0) return -3;
	}
	typefield.fs = loadedFields2[colplace].ls;
	typefield.ls = loadedFields2[loadedFields2L - 1].ls;
	if (typefield.ls < typefield.fs + 2) return -4;
	debugThreshold = 2;
	OutputNewline();
	OutputString("loading variables");
	for (i=0; i<colplace; i=i+2){
		if (freeVariableL > NUMFIELDS -2) return -5;
		freeVariable[freeVariableL].name = loadedFields2[i];
		freeVariable[freeVariableL].status = notset;
		freeVariable[freeVariableL].type = typefield;
		freeVariable[freeVariableL].kind = varkind;
		freeVariableL = freeVariableL + 1;
		//
		OutputField(loadedFields2[i]);
		OutputString(",");
		
	}
	OutputString(":");
	OutputField(typefield);
	OutputNewline();

	return 1;


}

int LoadIntVariables(FIELD varfield){
	// takes a field and loads internal variables from it;
	// returns -1 if it isnt an internal variable declaration.
	// note that this uses loadedFields2 !!! and fieldWritten2 

	int i,val;
	int colplace;
	FIELD typefield;

	val = CheckFieldBoundType(varfield);
	if (val != 1) return -1;

	AnalyseField2(InteriorField(varfield));
	colplace = -1;
	for (i=0; i<loadedFields2L; i++){
		WriteField2(loadedFields2[i]);
		val = MyStringCompare(fieldWritten2, ":");
		if (val == 0){
			colplace = i;
			break;
		}
	}
	if (colplace < 0) return -2;
	for (i=1; i<colplace; i= i+ 2){
		WriteField2(loadedFields2[i]);
		val = MyStringCompare(fieldWritten2, ",");
		if (val != 0) return -3;
	}
	typefield.fs = loadedFields2[colplace].ls;
	typefield.ls = varfield.ls -2;
	if (typefield.ls < typefield.fs + 2) return -4;
	for (i=0; i<colplace; i=i+2){
		if (freeVariableL > NUMFIELDS -2) return -5;
		freeVariable[freeVariableL].name = loadedFields2[i];
		freeVariable[freeVariableL].status = notset;
		freeVariable[freeVariableL].type = typefield;
		freeVariable[freeVariableL].kind = internal;
		freeVariableL = freeVariableL + 1;
	}

	return 1;


}

int LoadLemma(int theline){
	// loads the lemma into the freeVariable, lemmaClause
	// and lemmaConclusion variables.
	// note that the lemmaClause[i].written
	// and the lemmaConclusion fields will be without parentheses
	// returns -1 if load is no good, 1 if load is ok

	// then loads the ivOccurence matrix

	
	int val, i,j;
	int restbase;
	int fv,cl;


	if (CoqLines[theline].LineType != Lemma) return -1;

	AnalyseField(CoqLines[theline].f);

	if (loadedFieldsL < 6) return -2;
	if (loadedFieldsL > NUMFIELDS -2) return -3;


	lemmaName = loadedFields[1];

	WriteField(loadedFields[2]);
	val = MyStringCompare(fieldWritten, ":");
	if (val != 0) return -4;

	freeVariableL = 0;
	restbase = 3;
	for (i=3; i<loadedFieldsL; i++){
		val = LoadIntVariables(loadedFields[i]);
		if (val < 0) break;
		restbase = i+1;
	}
	for (i= restbase + 1; i< loadedFieldsL - 2; i=i+2){
		WriteField(loadedFields[i]);
		val = MyStringCompare(fieldWritten, "->");
		if (val != 0) return -5;
	}
	lemmaConclusion=InteriorField(loadedFields[loadedFieldsL -2]);

	lemmaClauseL = 0;
	for (i=restbase; i<loadedFieldsL -2; i=i+2){
		if (lemmaClauseL >= LEMSIZE ){
			debugThreshold = 1;
			OutputNewline();
			OutputString("too many clauses");
			OutputNewline();
			return -6;
		}
		lemmaClause[lemmaClauseL].written= InteriorField(loadedFields[i]);
		lemmaClauseL = lemmaClauseL + 1;
	}


	// now input the ivOccurence and ivInConclusion stuff
	// first check to see that we dont have too many things

	if (freeVariableL > LEMSIZE){
		debugThreshold = 1;
		OutputNewline();
		WriteString("couldnt load lemma, there are ");
		MyAppendInt(freeVariableL);
		MyAppendString(" free variables, which is too many");
		OutputString(fieldWritten);
		OutputNewline();
		return -7;
	}
	if (lemmaClauseL > LEMSIZE){
	
		return -8;
	}
	for (cl = 0; cl < lemmaClauseL; cl++){
		DecomposeField(lemmaClause[cl].written);
		for (fv = 0; fv < freeVariableL; fv++){
			ivOccurence[fv][cl].occurencesL = 0;
			for (j= 0; j<loadedFieldsL; j++){
				val = MyCompareFields(loadedFields[j], freeVariable[fv].name);
				if (val == 0){
					if (ivOccurence[fv][cl].occurencesL >= LEMSIZE){
						debugThreshold = 1;
						OutputNewline();
						OutputString("too many occurences in a clause");
						OutputNewline();
						return -9;
					}
					
					ivOccurence[fv][cl].occurences[ivOccurence[fv][cl].occurencesL] = j;
					ivOccurence[fv][cl].occurencesL = ivOccurence[fv][cl].occurencesL + 1;
					
				}

					
			}
		}

	}

	// now we set the occs in the clauses, same as above but with j before fv
	for (cl = 0; cl < lemmaClauseL; cl++){
		DecomposeField(lemmaClause[cl].written);
		lemmaClause[cl].occsL = 0;
		for (j= 0; j<loadedFieldsL; j++){
			for (fv = 0; fv < freeVariableL; fv++){
				val = MyCompareFields(loadedFields[j], freeVariable[fv].name);
				if (val == 0){
					if (lemmaClause[cl].occsL >= (LEMSIZE * LEMSIZE)){
						debugThreshold = 1;
						OutputNewline();
						OutputString("too many occurences of all variables in a clause");
						OutputNewline();
						return -9;
					}
					
					lemmaClause[cl].occs[lemmaClause[cl].occsL] = j;
					lemmaClause[cl].occsL = lemmaClause[cl].occsL+1;
					break;	// from the fv loop
				}

					
			}
		}

	}

	DecomposeField(lemmaConclusion);
		for (fv = 0; fv < freeVariableL; fv++){
			ivInConclusion[fv].occurencesL = 0;
			for (j= 0; j<loadedFieldsL; j++){
				val = MyCompareFields(loadedFields[j], freeVariable[fv].name);
				if (val == 0){
					if (ivInConclusion[fv].occurencesL >= LEMSIZE){
						debugThreshold = 1;
						OutputNewline();
						OutputString("too many occurences in conclusion");
						OutputNewline();
						return -9;
					}
					ivInConclusion[fv].occurences[ivInConclusion[fv].occurencesL] = j;
					ivInConclusion[fv].occurencesL = ivInConclusion[fv].occurencesL + 1;
				}

					
			}
		}




	

	return 1;


}

void SetMaxIndex(){
	// sets the maxIndex variable

	int i,j;
	int toggle;
	char base;
	char ch;
	
	
	int testMax;
	int digit;
	int exp;

	maxIndex = 0;
	base = '0';
	
	for (i=0; i<normalizedDataL-6; i++){
		if (normalizedData[i] == '_'){
			toggle = 1;
			for (j=i+1; j<i+6; j++){
				ch = normalizedData[j];
				if (ch < base) toggle = -1;
				if (ch > base + 9) toggle = -1;
			}
			if (toggle > 0){
				exp = 1;
				testMax = 0;
				for (j= i+ 5; j> i; j=j-1){
					ch = normalizedData[j];
					digit = ch - base;
					testMax = testMax + (digit * exp);
					exp = exp * 10;
				}
				if ((testMax > maxIndex) && (testMax < 100000L)){
					maxIndex = testMax;
				}
			}
		
		}
	
	}
	
	


	

}




void ApplyLemma(int theline){
	// we apply the lemma in question to try to obtain a
	// new result; if it is really new then we print it out
	// if it isnt a lemma then return

	// for now we just print out the loaded lemma stuff

	int val, i;
	int count;

	if (CoqLines[theline].LineType != Lemma) return;
	if (CoqLines[theline].opensection != 1) return;

	freeVariableL = 0;
	lemmaClauseL = 0;

	debugThreshold = 2;

	OutputNewline();
	OutputField(CoqLines[theline].f);
	


	AnalyseField(CoqLines[theline].f);

	OutputNewline();
	OutputString("Applying lemma ");
	if (loadedFieldsL <= 1){
		OutputString("too small");
		return;
	}


	

	val = LoadLemma(theline);

	

	if (val < 0){
		OutputString("load error ");
		if (val == -1) OutputString("number 1");
		if (val == -2) OutputString("number 2");
		if (val == -3) OutputString("number 3");
		if (val == -4) OutputString("number 4");
		if (val == -5) OutputString("number 5");
		if (val == -6) OutputString("number 6");
		if (val == -7) OutputString("number 7");
		if (val == -8) OutputString("number 8");
		if (val == -9) OutputString("number 9");
		if (val == -10) OutputString("number 10");
		if (val == -11) OutputString("number 11");
		if (val == -12) OutputString("number 12");
		if (val == -13) OutputString("number 13");
		if (val == -14) OutputString("number 14");
		return;
	}

	OutputField(lemmaName);
	OutputString("  ");

	OutputNewline();
	OutputString("variables");
	OutputNewline();
	for (i=0; i<freeVariableL; i++){
		OutputField(freeVariable[i].name);
		OutputString(", ");
	}
	OutputNewline();
	OutputString("clauses");
	for (i=0; i<lemmaClauseL; i++){
		OutputString("\n");
		OutputField(lemmaClause[i].written);
	}
	OutputNewline();
	OutputString("conclusion");
	OutputNewline();
	OutputField(lemmaConclusion);
	OutputNewline();
	OutputString("Instances :");
	OutputNewline();

	/////////////////

	// now we set the trylow and tryhigh variables in lemmaClause[i]

	lemmaClauseT = 0;

	for (i=0; i<lemmaClauseL; i++){
		AnalyseField2(lemmaClause[i].written);
		if (loadedFields2L <= 0){
			OutputString("empty clause");
			return;
		}
		val = LookUpPropertyLow(loadedFields2[0]);
		lemmaClause[i].trylow = val;
		lemmaClause[i].trycurrent = val;
		if (val < 0){
			OutputNewline();
			OutputString("Couldn't find a result for clause");
			OutputNewline();
			OutputField(lemmaClause[i].written);
			return;
		}
		val = LookUpPropertyHigh(loadedFields2[0]);
		lemmaClause[i].tryhigh = val;
		if (val < 0){
			OutputNewline();
			OutputString("Couldn't find a result for clause");
			OutputNewline();
			OutputField(lemmaClause[i].written);
			return;
		}
		
	}

	///////////
	// in general we now have to try all instances of the clauses;
	
	count = 0;

	val = TryClauses();
	if (val > 0){
		OutputNewline();
		OutputString("Lemma application successful");
		OutputNewline();
	}
	if (val < 0){
		OutputNewline();
		WriteString("Lemma application failed (A) with error -");
		MyAppendInt(-val);
		MyAppendString(" in TryClauses");
		OutputString(fieldWritten);
		OutputNewline();
	}

	while(count < 100){
		lemmaClauseT = lemmaClauseL -1;
		while (lemmaClauseT >= 0){
			if (lemmaClause[lemmaClauseT].trycurrent >= lemmaClause[lemmaClauseT].tryhigh){
				lemmaClauseT = lemmaClauseT - 1;
			}
			else{
				break;
			}
		}
		//now lemmaClauseT is the first which is not at tryhigh
		if (lemmaClauseT < 0){
			
			OutputString("all possibilities tried");
			break;
		}
		if (lemmaClause[lemmaClauseT].trycurrent >= lemmaClause[lemmaClauseT].tryhigh){
			OutputString("error in lemmaClause loop");
			break;
		}
		if (lemmaClause[lemmaClauseT].trycurrent < lemmaClause[lemmaClauseT].trylow){
			OutputString("error in lemmaClause loop");
			break;
		}
		lemmaClause[lemmaClauseT].trycurrent = lemmaClause[lemmaClauseT].trycurrent +1;
		for (i= lemmaClauseT + 1; i< lemmaClauseL; i++){
			lemmaClause[i].trycurrent = lemmaClause[i].trylow;
		}
		val = TryClauses();
		if (val > 0){
			OutputNewline();
			OutputString("Lemma application successful");
			OutputNewline();
		}
		if (val < 0){
			OutputNewline();
			WriteString("Lemma application failed (B) with error -");
			MyAppendInt(-val);
			MyAppendString(" in TryClauses");
			OutputString(fieldWritten);
			OutputNewline();
			
		}
		count = count +1;

		if (count > 98){
			debugThreshold = 1;
			OutputNewline();
			OutputString("tried the lemma 98 times, stopping");
			return;
		}



	}
	



	
	
}

void GoodDecomposeField(FIELD thefield, int thecl){
	// decomposes the field then uses lemmaClause[thecl].occs
	// to contract parenthesized fields at the occurences
	// of free variables in the clause in question

	

	int i;
	char ch;

	int nextOcc;
	int lastsep;
	int parlevel;
	int subtog;

	loadedFieldsL = 0;
	nextOcc = 0;

	lastsep = thefield.fs;
	subtog = 0;
	parlevel = 0;

	if (nextOcc < lemmaClause[thecl].occsL){			
			if (loadedFieldsL == lemmaClause[thecl].occs[nextOcc]){
				subtog = 1;
				parlevel = 0;
			}
	}

	for (i=(thefield.fs + 1); i<=thefield.ls; i++){
		ch = normalizedData[i];
		if (ch == ' '){
			if ((subtog == 0) | (parlevel <= 0)){
				if (loadedFieldsL < 0) return;
				if (loadedFieldsL > NUMFIELDS -2){
					OutputNewline();
					OutputString("too many fields in decomp ");
					OutputNewline();
					return;
				}
				loadedFields[loadedFieldsL].fs = lastsep;
				loadedFields[loadedFieldsL].ls = i;
				lastsep = i;
				if (subtog > 0) nextOcc = nextOcc + 1;
				subtog = 0;
				parlevel = 0;
				loadedFieldsL = loadedFieldsL + 1;
				if (nextOcc < lemmaClause[thecl].occsL){			
					if (loadedFieldsL == lemmaClause[thecl].occs[nextOcc]){
						subtog = 1;
						parlevel = 0;
					}
				}

			}
			

		}
		if (ch == '('){
			if (subtog > 0) parlevel = parlevel + 1;
		}
		if (ch == ')'){
			if (subtog > 0) parlevel = parlevel - 1;
		}
		

	}

	
}

void MyAppendVariables(){
	// appends the variables from freeVariable to fieldWritten
	int cursor,j, val;
	enum tag varkind;
	FIELD typefield;

	cursor=0;
	while(cursor<freeVariableL){
		j = cursor;
		typefield = freeVariable[cursor].type;
		varkind = freeVariable[cursor].kind;
		while(cursor<freeVariableL){
			cursor=cursor+1;
			val = MyCompareFields(typefield, freeVariable[cursor].type);
			if (val != 0) break;
			if (freeVariable[cursor].kind != varkind) break;

		}
		PotentialBreak();
		if (varkind == internal) MyAppendString("(");
		if (varkind == external) MyAppendString("[");
		while(j < cursor){
			MyAppendField(freeVariable[j].name);
			if (j<cursor - 1) MyAppendString(", ");
			j = j+ 1;
		
		}
		MyAppendString(" : ");
		MyAppendField(typefield);
		if (varkind == internal) MyAppendString(")");
		if (varkind == external) MyAppendString("]");
	}
}

void MyAppendVariablesNB(){
	// appends the variables from freeVariable to fieldWritten
	// this version doesnt include potential breaks
	int cursor,j, val;
	enum tag varkind;
	FIELD typefield;

	cursor=0;
	while(cursor<freeVariableL){
		j = cursor;
		typefield = freeVariable[cursor].type;
		varkind = freeVariable[cursor].kind;
		while(cursor<freeVariableL){
			cursor=cursor+1;
			val = MyCompareFields(typefield, freeVariable[cursor].type);
			if (val != 0) break;
			if (freeVariable[cursor].kind != varkind) break;

		}
		if (varkind == internal) MyAppendString("(");
		if (varkind == external) MyAppendString("[");
		while(j < cursor){
			MyAppendField(freeVariable[j].name);
			if (j<cursor - 1) MyAppendString(", ");
			j = j+ 1;
		
		}
		MyAppendString(" : ");
		MyAppendField(typefield);
		if (varkind == internal) MyAppendString(")");
		if (varkind == external) MyAppendString("]");
	}
}




int TryClauses(){
	// we try the current clauses of the loaded lemma
	// returns 1 if successful (i.e. if it wrote a
	// new statement), -e if not.

	

	int i,j;
	int fv,cl;
	int val;
	FIELD resultField;
	int resultLine;
	FIELD resultName;
	int debugThresholdOld;

	for (i= 0; i<freeVariableL; i++){
		freeVariable[i].status = notset;
	}
	


	if (lemmaClauseL <0) return -1;
	if (lemmaClauseL > LEMSIZE) return -1;
	if (freeVariableL < 0) return -1;
	if (freeVariableL > LEMSIZE) return -1;

	debugThreshold = 2;
	for (i=0; i<lemmaClauseL; i++){
		OutputNewline();
		WriteString("clause--");
		MyAppendInt(i+1);
		MyAppendString(" : trying ");
		MyAppendField(Dictionary[lemmaClause[i].trycurrent].f);
		OutputString(fieldWritten);

	}
	
	

	// first we try instantiating the free variables...
	for (fv = 0; fv < freeVariableL; fv++){
		for (cl = 0; cl < lemmaClauseL; cl++){
			if (ivOccurence[fv][cl].occurencesL > 0){
				resultField = Dictionary[lemmaClause[cl].trycurrent].f;
				GoodDecomposeField(resultField, cl);
				OutputNewline();
				if (ivOccurence[fv][cl].occurences[0] >= loadedFieldsL){
					// the following is somewhat complicated for debugging
					debugThreshold = 2;
					OutputNewline();
					OutputString("textual problem when instantiating variable ");
					WriteField(freeVariable[fv].name);
					PotentialBreak();
					MyAppendString(" result field = ");
					for (i=0; i<loadedFieldsL; i++){
						MyAppendField(loadedFields[i]);
						MyAppendString(";");
					}
					MyAppendString(" looking for occ ");
					MyAppendInt(ivOccurence[fv][cl].occurences[0]);
					OutputString(fieldWritten);
					return -12;
				} 
				freeVariable[fv].instance = loadedFields[ivOccurence[fv][cl].occurences[0]];
				freeVariable[fv].status = set;
				break;
			}

		}
		if (freeVariable[fv].status == notset){
			debugThreshold = 2;
			OutputNewline();
			OutputString("unable to instantiate variable ");
			WriteField(freeVariable[fv].name);
			OutputString(fieldWritten);
			return -2;
		}


	}
	// now the variables are instantiated; next, just plug them
	//  in and verify against the results.

	for (cl = 0; cl < lemmaClauseL; cl++){
		DecomposeField(lemmaClause[cl].written);
		for (fv = 0; fv < freeVariableL; fv++){
			for (i = 0; i<ivOccurence[fv][cl].occurencesL; i++){
				if (i<0) return -15;
				if (i>= LEMSIZE) return -16;
				j = ivOccurence[fv][cl].occurences[i];
				if (j<0) return -17;
				if (j>= loadedFieldsL){
					debugThreshold = 2;
					OutputNewline();
					OutputString("textual problem when plugging in variable ");
					WriteField(freeVariable[fv].name);
					OutputString(fieldWritten);
					return -18;
				}
				loadedFields[j] = freeVariable[fv].instance;
			}
		}
		fieldWrittenL = 0;
		fieldWritten[0]=0;
		for (i=0; i<loadedFieldsL; i++){
			MyAppendField(loadedFields[i]);
			if (i<(loadedFieldsL -1)) MyAppendString(" ");
		}
		resultField = Dictionary[lemmaClause[cl].trycurrent].f;
		WriteField2(resultField);
		val = MyStringCompare(fieldWritten, fieldWritten2);
		if (val != 0){
			debugThreshold = 2;
			OutputNewline();
			OutputString("attempt to match instantiated lemma clause");
			OutputNewline();
			OutputString(fieldWritten);
			OutputString(" with result ");
			OutputNewline();
			OutputString(fieldWritten2);
			OutputString(" FAILED");
			return -3;
		}
		// if successful then we set the resultName parameter
		// in order to be able to do the proof.

		resultLine = Dictionary[lemmaClause[cl].trycurrent].lineReference;
		AnalyseField(CoqLines[resultLine].f);
		if (loadedFieldsL < 2) return -4;
		resultName = loadedFields[1];
		lemmaClause[cl].resultName = resultName;


	}

	//next we write the lemma conclusion 
	DecomposeField(lemmaConclusion);
	for (fv = 0; fv < freeVariableL; fv++){
			for (i = 0; i<ivInConclusion[fv].occurencesL; i++){
				if (i<0) return -5;
				if (i>= LEMSIZE) return -6;
				j = ivInConclusion[fv].occurences[i];
				if (j<0) return -7;
				if (j> NUMFIELDS){
					return -8;
				}
				loadedFields[j] = freeVariable[fv].instance;
			}
	}
	WriteString("( ");
	for (i=0; i<loadedFieldsL; i++){
			MyAppendField(loadedFields[i]);
			MyAppendString(" ");
	}
	MyAppendString(")");

	


	
	debugThreshold = 2;
	OutputString("searching ::");
	OutputString(fieldWritten);
	OutputString("::");
	OutputNewline();

	

	val = LookUpString(fieldWritten);
	if (val >= 0){
		OutputString("found a known result");
		return -10;	// the result was already known
	}

	

	if (factToggle == 0){
		WriteString2("Remark automatic_");
	}
	
	if (factToggle == 1){
		WriteString2("URemark automatic_");
	}
	
	maxIndex = maxIndex + 1;
	MyAppendInt2(maxIndex);
	MyAppendString2(" : ");

	if (loadedFieldsL > 1) MyAppendString2("(");
	for (i=0; i<loadedFieldsL; i++){
			MyAppendField2(loadedFields[i]);
			MyAppendString2(" ");
	}
	if (loadedFieldsL > 1) MyAppendString2(")");

	MyAppendString2(".");

	OutputNewline();
	OutputString("FOUND ");

	debugThresholdOld = debugThreshold;
	
	debugThreshold = 0;


	OutputNewline();
	OutputString(fieldWritten2);
	OutputNewline();
	OutputString("Proof ");

	WriteString("( ");
	MyAppendField(lemmaName);
	MyAppendString(" ");
	for (i=0; i<freeVariableL; i++){
		MyAppendField(freeVariable[i].instance);
		MyAppendString(" ");
	}
	for (i=0; i<lemmaClauseL; i++){
		MyAppendField(lemmaClause[i].resultName);
		MyAppendString(" ");
	}
	MyAppendString(")");

	OutputString(fieldWritten);
	OutputString(".");
	OutputNewline();

	debugThreshold = debugThresholdOld;

	return 1;


}



int CheckFieldBoundType(FIELD thefield){
	// returns 0 if there are no field bounds,
	// returns 1 if the field bounds are (  )
	// returns 2 if the field bounds are [  ]
	
	char ch, ch2;
	
	

	if ((thefield.ls - thefield.fs)<4) return 0;

	ch = normalizedData[thefield.fs + 1];
	if (ch == '('){
		ch2 = normalizedData[thefield.ls - 1];
		if (ch2 == ')'){
			return 1;
		}
		else{
			return 0;
		}
	}
	if (ch == '['){
		ch2 = normalizedData[thefield.ls - 1];
		if (ch2 == ']'){
			return 2;
		}
		else{
			return 0;
		}
	}
	return 0;


}



void ApplyDefinition(int theline){
	// switches out to the applyconstruction and applyproperty functions
	// also checks to see if we should print out the stuff or not
	// by looking up in_Mydef or apply_mydef in the dictionary

	FIELD lineName;
	
	
	int val, val2;
	int debugThresholdOld;
	FIELD thefield;
	int toggle;

	thefield = CoqLines[theline].f;
	
	if (CoqLines[theline].LineType != Property) return;

	debugThresholdOld = debugThreshold;
	debugThreshold = 1;

	OutputNewline();
	OutputString("ApplyDefinition for field ");
	OutputField(thefield);
	OutputNewline();

	AnalyseField(thefield);
	if (loadedFieldsL < 5){
		OutputString("ApplyDef out, < 5 fields");
		OutputNewline();
		return;
	}
	WriteField(loadedFields[2]);
	val = MyStringCompare(fieldWritten, ":=");
	if (val != 0){
		OutputString("ApplyDef out, no :=");
		OutputNewline();
		return;
	}

	

	lineName = loadedFields[1];
	

	
	
	
	
		WriteString("apply_");
		MyAppendField(lineName);
		val = LookUpString(fieldWritten);
		if (val >= 0){
			OutputString("Already found the item ");
			OutputString(fieldWritten);
			OutputNewline();
			return;
		}
	
		val = BreakDownLine(theline);
		if (val > 0){
			toggle = 1;
			AnalyseField(lemmaConclusion);
			if (loadedFieldsL == 3){
				WriteField2(loadedFields[0]);
				val2 = MyStringCompare(fieldWritten2, "AND");
				if (val2 == 0){
					ApplyANDProperty();
					toggle = 0;
				}
			}
			if (toggle == 1) ApplyProperty();
		}
		else{
			WriteString("breakdown error number ");
			MyAppendInt(-val);
			OutputNewline();
			OutputString(fieldWritten);
		}
		
	

	debugThreshold = debugThresholdOld;

}

int BreakDownLine(int theline){
	// now modelled on LoadLemma
	
	int val, i;
	int restbase;
	

	AnalyseField(CoqLines[theline].f);

	if (loadedFieldsL < 6) return -2;
	if (loadedFieldsL > NUMFIELDS -2) return -3;


	lemmaName = loadedFields[1];

	

	freeVariableL = 0;
	restbase = 3;
	for (i=3; i<loadedFieldsL; i++){
		val = LoadAnyVariables(loadedFields[i]);
		if (val < 0) break;
		restbase = i+1;
	}
	for (i= restbase + 1; i< loadedFieldsL - 2; i=i+2){
		WriteField(loadedFields[i]);
		val = MyStringCompare(fieldWritten, "->");
		if (val != 0) return -5;
	}
	lemmaConclusion=InteriorField(loadedFields[loadedFieldsL -2]);

	lemmaClauseL = 0;
	for (i=restbase; i<loadedFieldsL -2; i=i+2){
		if (lemmaClauseL >= LEMSIZE ){
			debugThreshold = 1;
			OutputNewline();
			OutputString("too many clauses");
			OutputNewline();
			return -6;
		}
		lemmaClause[lemmaClauseL].written= InteriorField(loadedFields[i]);
		lemmaClauseL = lemmaClauseL + 1;
	}

	
	return 1;

}




void ApplyProperty(){
	// applies a property to broken down line
	// creates a lemma called apply_myproperty

	int i,j;

	for (j= 0; j<freeVariableL; j++){
		freeVariable[j].oldkind = freeVariable[j].kind;
		freeVariable[j].kind = internal;
	}

	debugThreshold = 0;

	OutputNewline();
	WriteString("Lemma apply_");
	MyAppendField(lemmaName);
	MyAppendString(" : ");
	MyAppendVariables();
	PotentialBreak();
	MyAppendString("( ");
	MyAppendField(lemmaName);
	for (i=0; i<freeVariableL; i++){
		if (freeVariable[i].oldkind == external){
			MyAppendString(" ");
			MyAppendField(freeVariable[i].name);
		}
	}
	MyAppendString(" ) -> ");
	PotentialBreak();
	for (i=0; i<lemmaClauseL; i++){
		MyAppendString("( ");
		MyAppendField(lemmaClause[i].written);
		MyAppendString(" ) -> ");
		PotentialBreak();
	}
	MyAppendString("( ");
	MyAppendField(lemmaConclusion);
	MyAppendString(" ).");

	OutputString(fieldWritten);
	OutputNewline();
	WriteString("Proof ");
	for (j=0; j<freeVariableL; j++){
		freeVariable[j].kind = external;
	}
	MyAppendVariables();
	PotentialBreak();
	MyAppendString("[ hyp : ( ");
	MyAppendField(lemmaName);
	for (i=0; i<freeVariableL; i++){
		if (freeVariable[i].oldkind == external){
			MyAppendString(" ");
			MyAppendField(freeVariable[i].name);
		}
	}
	MyAppendString(" )] ");
	for (i=0; i<lemmaClauseL; i++){
		PotentialBreak();
		MyAppendString("[ h");
		MyAppendInt(i+1);
		MyAppendString(" : ( ");
		MyAppendField(lemmaClause[i].written );
		MyAppendString(" )] ");
	}
	PotentialBreak();
	MyAppendString("( hyp");
	for (i=0; i<freeVariableL; i++){
		if (freeVariable[i].oldkind == internal){
			MyAppendString(" ");
			MyAppendField(freeVariable[i].name);
		}
	}
	for (i=0; i<lemmaClauseL; i++){
		MyAppendString(" h");
		MyAppendInt(i+1);
	}
	MyAppendString(" ).");

	OutputString(fieldWritten);
	OutputNewline();


	debugThreshold = 1;


}

void ApplyANDProperty(){
	// applies a property whose constructor is an AND
	// and which has no clauses or ivs, giving the
	// conj and proj1 and proj2 lemmas.
	// we assume AND_conj : [P,Q: Prop]P -> Q -> (AND P Q)
	// and AND_proj1 : [P,Q: Prop](AND P Q) -> P
	// similarly AND_proj2.

	int val, i;
	FIELD Pclause;
	FIELD Qclause;

	for (i=0; i<freeVariableL; i++){
		if (freeVariable[i].kind == internal) return;
		freeVariable[i].kind = internal;
	}
	if (lemmaClauseL > 0) return;
	AnalyseField(lemmaConclusion);
	if (loadedFieldsL != 3) return;

	WriteField(loadedFields[0]);
	val = MyStringCompare(fieldWritten, "AND");
	if (val != 0) return;
	
	Pclause = loadedFields[1];
	Qclause = loadedFields[2];
	

	WriteString("conj_");
	MyAppendField(lemmaName);
	val = LookUpString(fieldWritten);
	if (val >= 0){
		debugThreshold = 1;
		OutputNewline();
		OutputString("alread found result ");
		OutputString(fieldWritten);
		OutputNewline();
		return;
	}

	debugThreshold = 0;

	// now conj

	OutputNewline();
	WriteString("Lemma conj_");
	MyAppendField(lemmaName);
	MyAppendString(" : ");
	MyAppendVariables();	// note that we set these to internal above
	PotentialBreak();
	MyAppendField(Pclause);
	MyAppendString(" -> ");
	PotentialBreak();
	MyAppendField(Qclause);
	MyAppendString(" -> ");
	PotentialBreak();
	MyAppendString("( ");
	MyAppendField(lemmaName);
	for (i= 0;i<freeVariableL; i++){
		MyAppendString(" ");
		MyAppendField(freeVariable[i].name);
	}
	MyAppendString(" ).");

	OutputString(fieldWritten);
	OutputNewline();
	WriteString("Proof ");
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].kind = external;
	}
	MyAppendVariables();
	MyAppendString("[ hyp1 : ");
	MyAppendField(Pclause);
	MyAppendString(" ] ");
	PotentialBreak();
	MyAppendString("[ hyp2 : ");
	MyAppendField(Qclause);
	MyAppendString(" ] ");
	PotentialBreak();
	MyAppendString("(AND_conj ");
	MyAppendField(Pclause);
	PotentialBreak();
	MyAppendField(Qclause);
	MyAppendString(" hyp1 hyp2).");
	PotentialBreak();

	OutputString(fieldWritten);
	OutputNewline();

	// now proj1

	OutputNewline();
	WriteString("Lemma proj1_");
	MyAppendField(lemmaName);
	MyAppendString(" : ");
	PotentialBreak();
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].kind = internal;
	}
	MyAppendVariables();
	
	MyAppendString("( ");
	MyAppendField(lemmaName);
	for (i= 0;i<freeVariableL; i++){
		MyAppendString(" ");
		MyAppendField(freeVariable[i].name );
	}
	MyAppendString(" ) -> ");
	PotentialBreak();
	MyAppendField(Pclause);
	MyAppendString(" .");
	OutputString(fieldWritten);
	OutputNewline();

	WriteString("Proof ");
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].kind = external;
	}
	MyAppendVariables();
	MyAppendString("[ hyp : ( ");
	MyAppendField(lemmaName);
	for (i= 0;i<freeVariableL; i++){
		MyAppendString(" ");
		MyAppendField(freeVariable[i].name );
	}
	MyAppendString(" )] ");
	PotentialBreak();
	MyAppendString("(AND_proj1 ");
	MyAppendField(Pclause);
	MyAppendString(" ");
	PotentialBreak();
	MyAppendField(Qclause);
	MyAppendString("  hyp).");
	PotentialBreak();

	OutputString(fieldWritten);
	OutputNewline();

	// now proj2
	OutputNewline();
	WriteString("Lemma proj2_");
	MyAppendField(lemmaName);
	MyAppendString(" : ");
	PotentialBreak();
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].kind = internal;
	}
	MyAppendVariables();
	
	MyAppendString("( ");
	MyAppendField(lemmaName);
	for (i= 0;i<freeVariableL; i++){
		MyAppendString(" ");
		MyAppendField(freeVariable[i].name );
	}
	MyAppendString(" ) -> ");
	PotentialBreak();
	MyAppendField(Qclause);
	MyAppendString(" .");
	OutputString(fieldWritten);
	OutputNewline();

	WriteString("Proof ");
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].kind = external;
	}
	MyAppendVariables();
	MyAppendString("[ hyp : ( ");
	MyAppendField(lemmaName);
	for (i= 0;i<freeVariableL; i++){
		MyAppendString(" ");
		MyAppendField(freeVariable[i].name );
	}
	MyAppendString(" )] ");
	PotentialBreak();
	MyAppendString("(AND_proj2 ");
	MyAppendField(Pclause);
	MyAppendString(" ");
	PotentialBreak();
	MyAppendField(Qclause);
	MyAppendString("  hyp).");
	PotentialBreak();

	OutputString(fieldWritten);
	OutputNewline();


	


}








void PrintNDtoScreen(int firstplace, int afterlast){
	char ourstring[100];
	char ch;
	int i;

	if (firstplace < 0){
		printf("PrintND called on illegal arguments1\n");
		printf("firstplace = %d\n", firstplace);
		printf("afterlast = %d\n", afterlast);
		return;
	}
	if (afterlast > normalizedDataL){
		printf("PrintND called on illegal arguments2\n");
		printf("firstplace = %d\n", firstplace);
		printf("afterlast = %d\n", afterlast);
		printf("normalizedDataL = %d\n", normalizedDataL);
		return;
	}
	if (afterlast <= firstplace){
		printf("PrintND called on illegal arguments3\n");
		printf("firstplace = %d\n", firstplace);
		printf("afterlast = %d\n", afterlast);
		return;
	}
	if (afterlast - firstplace > 60){
		printf("PrintND length overflow\n");
		printf("firstplace = %d\n", firstplace);
		printf("afterlast = %d\n", afterlast);
		return;
	}

	for (i= 0; i<(afterlast - firstplace); i++){
		ch = normalizedData[firstplace + i];
		ourstring[i]=ch;
	}
	ourstring[afterlast - firstplace] = 0;

	printf("%s", ourstring);

}
	



void PrintOutputToFile(char* fname){
	// prints  aPout array to the file named fname
	
	int val;
	
	
	/// writing file
	
	printf("\nWriting to file named %s\n", fname);

	ourfile = fopen(fname, "w");

	if (ourfile == NULL){
		printf("file opening failed\n");
		exit(0);
	}

	val = fwrite(aPout,sizeof(char),aPoutL,ourfile);

	printf("wrote %d characters to the file\n", aPoutL);

	fclose(ourfile);
	
}

void MainShell(){
	// this is the main shell loop

	int count;
	int specToggle;	// 0 if no file has been specified
		// 1 if a file has been specified
	char command[100];

	
	currentFilenameL = 0;
	count = 0;

	InitToggles();

	while (count < 100){

		specToggle = CheckCurrentFile();
		if (specToggle == 0){
			
			printf("\nenter s to specify a filename");
			printf("\nenter t to treat toggles");
			printf("\nenter q to quit\n");
			printf("?");
			scanf("%s", &command);
			if (command[0] == 's'){
				TreatSpecify();
			}
			if (command[0] == 'q'){
				return;
			}
			if (command[0] == 't'){
				TreatToggles();
			}
		}
		else{
			
			printf("\nwill look at file %s.v", currentFilename);
			printf("\nwith output to file %sOUT",currentFilename);
			if (extensionToggle == 0) printf(".html");
			if (extensionToggle == 1) printf(".v");
			printf("\n");
			printf("\nmost commands yield an explanatory header");
			printf("\nin the output file\n");
			printf("\nenter r to create automatic results");
			printf("\nenter l to create apply_ lemmas");
			printf("\nenter e to end current section");
			printf("\nenter z to list properties and lemmas alphabetically");
			printf("\nenter x to export properties and lemmas");
			printf("\nenter s to specify a new filename");
			printf("\nenter t to view or change some toggles");
			printf("\nenter q to quit\n");
			printf("?");
			scanf("%s", &command);
			if (command[0] == 'r'){
				TreatLook();
			}
			if (command[0] == 'l'){
				TreatLemDef();
			}
			if (command[0] == 'e'){
				TreatEndSec();
			}
			if (command[0] == 'z'){
				TreatZExport();
			}
			if (command[0] == 'x'){
				TreatExport();
			}
			if (command[0] == 's'){
				TreatSpecify();
			}
			if (command[0] == 'q'){
				return;
			}
			if (command[0] == 't'){
				TreatToggles();
			}

		}
		count = count + 1;

	}

	printf("\nSorry, for now there is a limit of 100 shell commands\n");
	

}

int CheckCurrentFile(){
	// checks to make sure that the currentFilename variable is ok
	// returns 1 if ok, 0 if not
	// also returns a 0 if the file length is 0.
	int i;

	if (currentFilenameL < 0){
		printf("\ncurrentFilenameL < 0\n");
		return 0;
	}
	if (currentFilenameL >= 100){
		printf("\ncurrentFilenameL >= 100\n");
		return 0;
	}
	if (currentFilename[currentFilenameL] != 0){
		printf("\ncurrentFilename not null-terminated\n");
		return 0;
	}
	for (i=0; i<currentFilenameL; i++){
		if (currentFilename[i] == 0){
			printf("\ncurrentFilename null-terminates too early\n");
			return 0;
		}
	}
	if (currentFilenameL == 0){
		printf("\napparently no current filename has yet been specified,");
		printf("\ntype s to specify one.\n");
		return 0;
	}
	return 1;

}

void OutputNewline(){
	// does OutputString depending on newlineToggle

	if (newlineToggle == 0){
		OutputString("\n");
	}
	if (newlineToggle == 1){
		OutputString("\r\n");
	}

	if (newlineToggle == 2){
		OutputString("<br>");
	}


}

void InitToggles(){
	
	if (version == fac){
	debugToggle = 0;
	debugThreshold = 2;
	newlineToggle = 0; // 0 = \n, 1 = \r\n , 2 = <br>
	factToggle = 0;	// 0 = Remark, 1 = URemark
	extensionToggle = 1;	// 0 = .html, 1 = .v
	}
	else{
	debugToggle = 0;
	debugThreshold = 2;
	newlineToggle = 2; // 0 = \n, 1 = \r\n , 2 = <br>
	factToggle = 0;	// 0 = Remark, 1 = URemark
	extensionToggle = 0;	// 0 = .html, 1 = .v
	}

}

void TreatToggles(){
	char tcommand[100];
	int tcount;

	tcount = 0;

	while(tcount < 15){
		printf("\nHere are a few toggles that govern what the");
		printf("\noutput will look like.\n");

	
	if (debugToggle == 0){
		printf("\ndebug output OFF (type d to change)\n");
	}
	if (debugToggle == 1){
		printf("\ndebug output PARTIAL (type d to change)\n");
	}
	if (debugToggle == 2){
		printf("\ndebug output FULL (type d to change)\n");
	}
	if (newlineToggle == 0){
		printf("\nnewline character is \\n (type n to change)\n");
	}
	if (newlineToggle == 2){
		printf("\nnewline character is <br> (type n to change)\n");
	}
	if (factToggle == 0){
		printf("\nresults will be printed as Remarks (type f to change)\n");
	}
	if (factToggle == 1){
		printf("\nresults will be printed as URemarks (type f to change)\n");
	}
	if (extensionToggle == 0){
		printf("\noutput file extension .html (type e to change)\n");
	}
	if (extensionToggle == 1){
		printf("\noutput file extension .v (type e to change)\n");
	}

			
	printf("\nenter m to return to main menu\n");
	printf("?");
	scanf("%s", &tcommand);
	if (tcommand[0] == 'm'){
		return;
	}
	if (tcommand[0] == 'd'){
		if (debugToggle == 0){
			debugToggle = 1;
			
		}
		else{
		if (debugToggle == 1){
			debugToggle = 2;
			
		}
		else{
			debugToggle = 0;
			
			
		}	
		}
	}
	if (tcommand[0] == 'n'){
		if (newlineToggle == 0){
			newlineToggle = 2;	// took out case 1 in this version
			
		}
		else{
		if (newlineToggle == 1){
			newlineToggle = 2;
			
		}
		else{
			newlineToggle = 0;
			
			
		}	
		}
	}
	if (tcommand[0] == 'f'){
		if (factToggle == 0){
			factToggle = 1;
			
		}
		else{
			factToggle = 0;
			
		}
	}
	if (tcommand[0] == 'e'){
		if (extensionToggle == 0){
			extensionToggle = 1;
			
		}
		else{
			extensionToggle = 0;
			
		}
	}

	tcount = tcount+1;
	if (tcount > 14){
		printf("\nsorry, only 15 tries allowed in this menu\n");
		return;
	}

	}	// end while

}

void TreatSpecify(){
	int i;
	int check;

	printf("\nType in the module name you would like\n");
	printf("to specify; for example if you type in mymod\n");
	printf("then the precompiler reads the file mymod.v and\n");
	printf("writes to the file mymodOUT");
	if (extensionToggle == 0) printf(".html");
	if (extensionToggle == 1) printf(".v");
	printf("\n---specify?");

	scanf("%s", currentFilename);

	currentFilename[99] = 0;
	currentFilenameL = 0;
	for (i=0; i<100; i++){
		if (currentFilename[i] == 0){
			currentFilenameL = i;
			break;
		}
	}
	check = CheckCurrentFile();
	if (check == 0){
		printf("\nOops!\n");
	}
	else{
		printf("\nThanks!\n");
	}

}

int ReadInputFromFile(){
	// takes care of the file opening stuff
	// returns -1 if it fails, 1 if it succeeds.
	
	int val;
char filename[220];
int i;
int firstplace, afterlast;
int check;


debugThreshold = 2;

	
check = CheckCurrentFile();
	
if (check == 0){
	printf("\nI can't look at that\n");
	return -1;
}

if (currentFilenameL > 200) return -1;
if (currentFilenameL <0) return -1;

for (i=0; i<currentFilenameL; i++){
	filename[i]=currentFilename[i];
}
filename[currentFilenameL] = '.';
filename[currentFilenameL + 1] = 'v';
filename[currentFilenameL + 2] = 0;


// THE MAIN PART STARTS HERE



ourfile = fopen(filename, "r");

if (ourfile == NULL){
printf("failed to open file %s\n", filename);
return -1;
}


aPinL = 0;
normalizedDataL=0;
aPoutL = 0;
CoqLinesL=0;
CheckFieldToggle = 0;
DictionaryL = 0;
DictionaryNL = 0;


val = fread(aPin,sizeof(char),aPinSpace,ourfile);

if (val > aPinSpace) val = aPinSpace;

printf("Read %d elements of the file\n", val);


fclose(ourfile);



aPinL = val;
aPoutL = 0;


if (aPinL > aPinSpace - 100){
	printf("\nLooks like the file was too big, bailing out. \n");
	return -1;

}


printf("\nNormalize data\n");
NormalizeData();

printf("\nNormalized Data has %d elements \n", normalizedDataL);

firstplace = 0;
afterlast = normalizedDataL;
if (afterlast > 59) afterlast = 59;
/*
printf("\nNormalized Data starts off like this: \n");
PrintNDtoScreen(firstplace, afterlast);
printf("\n");*/


printf("\nAnalyse data \n");

AnalyseData1();

printf("\nFound %d Coq lines \n", CoqLinesL);

printf("\nAnalyse lines \n");

for (i=0; i<CoqLinesL; i++){
	//printf("\nAnalysing line %d\n", i);
	AnalyseLine1(i);

}

return 1;

	
}

void TreatLook(){
// this is the main functionality
int val;
char filename[220];
int i;




debugThreshold = 2;

	
val = ReadInputFromFile();
if (val < 0) return;

// now we start the actual analysis and action
// the following generates a header (coq comment) in the output file

debugThreshold = 0;
OutputString("Set debug toggle to PARTIAL to get details on this function.");
OutputNewline();
OutputString("(***************** one iteration *******************)");
OutputNewline();
debugThreshold = 1;
OutputNewline();
OutputString("This function (which is the main functionality) creates");
OutputNewline();
OutputString("a list of suggestions for remarks which could be added");
OutputNewline();
OutputString("to the file, together with their proofs. The remarks");
OutputNewline();
OutputString("are based on the Hypotheses, Remarks and Lemmas of");
OutputNewline();
OutputString("currently open sections (including the global level).");
OutputNewline();
OutputString("A remark is not listed if it already occurs, or if");
OutputNewline();
OutputString("it occurs as a URemark; however URemarks are not used to");
OutputNewline();
OutputString("create new remarks.");
OutputNewline();
OutputString("Limitations: one must be able to instantiate the free");
OutputNewline();
OutputString("variables in a given lemma, based on their occurrences");
OutputNewline();
OutputString("in the hypotheses of that lemma. Also hypotheses of the");
OutputNewline();
OutputString("lemma should begin with a constructor not a variable,");
OutputNewline();
OutputString("so for example a lemma starting with");
OutputNewline();
OutputString("(X: Ens)(P: Ens -> Prop)(P X) -> ...");
OutputNewline();
OutputString("won\'t work; it should be rewritten as something like");
OutputNewline();
OutputString("(X: Ens) (P: Ens -> Prop)(Apply1 P X) -> ...");
OutputNewline();
OutputString("then when you have a property of the form (P X) and");
OutputNewline();
OutputString("would like to apply the lemma, redeclare it by hand");
OutputNewline();
OutputString("as (Apply1 P X).");
OutputNewline();





debugThreshold = 2;
OutputString("(*** this is the dictionary for the file : ");
OutputString(filename);
OutputString("  ***)");
OutputNewline();
OutputNewline();
OutputNewline();


sectionDepth = 0;

SetOpensection();	// sets the opensection parameter in CoqLines

printf("\n");
for (i=0; i<CoqLinesL; i++){
	//printf("\nAnalysing2 line %d\n", i);
	AnalyseLine4(i);
	
}


SortDictionary();

AddRestOfDictionary();

for (i=0; i<DictionaryL; i++){
	OutputNewline();
	
	if (Dictionary[i].ReferenceType == Definition) OutputString("Definition ");
	if (Dictionary[i].ReferenceType == Variable) OutputString("Variable ");
	if (Dictionary[i].ReferenceType == Lemma) OutputString("Lemma ");
	if (Dictionary[i].ReferenceType == Hypothesis) OutputString("Hypothesis ");
	if (Dictionary[i].ReferenceType == Remark) OutputString("Remark ");
	if (Dictionary[i].ReferenceType == Result) OutputString("Result ");
	if (Dictionary[i].ReferenceType == URemark) OutputString("URemark ");
	if (Dictionary[i].ReferenceType == OutRemark) OutputString("OutResult ");
	if (Dictionary[i].ReferenceType == Property) OutputString("Property ");
	

	OutputString("::");
	OutputField(Dictionary[i].f);
	OutputString("::");


	

}

SetMaxIndex();

for (i=0; i<CoqLinesL; i++){
	ApplyLemma(i);
}

// now we open a file to write

SendOutputToFile();

}



void TreatLemDef(){
	// this treats the arrange part of the loop,
	// designed to add in appropriate definitions and
	// lemmas, based on existing definitions.

	
int val;
char filename[220];
int i;

debugThreshold = 2;

val = ReadInputFromFile();
if (val < 0) return;


// now we start the actual analysis and action
// the following generates a header (coq comment) in the output file
OutputString("(*** this is the dictionary for the file : ");
OutputString(filename);
OutputString("  ***)");
OutputNewline();
OutputNewline();
OutputNewline();


sectionDepth = 0;

SetOpensection();	// sets the opensection parameter in CoqLines

printf("\n");
for (i=0; i<CoqLinesL; i++){
	//printf("\nAnalysing2 line %d\n", i);
	AnalyseLine5(i);
	
}


SortDictionary();

AddRestOfDictionary();

for (i=0; i<DictionaryL; i++){
	OutputNewline();
	
	if (Dictionary[i].ReferenceType == Definition) OutputString("Definition ");
	if (Dictionary[i].ReferenceType == Theorem) OutputString("Theorem ");
	if (Dictionary[i].ReferenceType == Lemma) OutputString("Lemma ");
	if (Dictionary[i].ReferenceType == Hypothesis) OutputString("Hypothesis ");
	if (Dictionary[i].ReferenceType == Remark) OutputString("Remark ");
	if (Dictionary[i].ReferenceType == Result) OutputString("Result ");
	if (Dictionary[i].ReferenceType == Local) OutputString("Local ");
	if (Dictionary[i].ReferenceType == URemark) OutputString("URemark ");
	if (Dictionary[i].ReferenceType == OutRemark) OutputString("OutRemark ");
	if (Dictionary[i].ReferenceType == Property) OutputString("Property ");

	OutputString("::");
	OutputField(Dictionary[i].f);
	OutputString("::");
	

}

debugThreshold = 0;
OutputNewline();
OutputString("This function creates a useful lemma (or 3)");
OutputNewline();
OutputString("for each new property which is introduced with");
OutputNewline();
OutputString("the Property ? := ? . command. It creates 3");
OutputNewline();
OutputString("lemmas when the property has the form (AND ? ?).");
OutputNewline();

debugThreshold = 2;

for (i=0; i<CoqLinesL; i++){
	if (CoqLines[i].LineType == Property){
		ApplyDefinition(i);
	}
	

}


// now we open a file to write

SendOutputToFile();


}

void TreatZExport(){
	// this version of Export doesnt output the grammar
	// and it gives an alphabetical listing by order of the
	// identifier. It should be more useful when one is looking
	// for a lemma, property or definition.
	// also, try doing first the defs then the properties then 
	// the lemmas ???

	int i,j,k;
	int val;
	int ourline;
	
	int chapterStart, chapterBound;
	FIELD chapterName;

	debugThreshold = 2;

	val = ReadInputFromFile();
	if (val < 0) return;

	printf("\n");
	for (i=0; i<CoqLinesL; i++){
		//printf("\nAnalysing2 line %d\n", i);
		AnalyseLineZ(i);
	
	}


	SortDictionary();

	AddRestOfDictionary();

	chapterLineL =0;
	for (i=0;i<CoqLinesL; i++){
		if (CoqLines[i].LineType == Chapter){
			if (chapterLineL < 900){
				chapterLine[chapterLineL] = i;
				chapterLineL = chapterLineL + 1;
			}

		}
	}
	chapterLine[chapterLineL] = CoqLinesL;

	debugThreshold = 0;
	OutputNewline();
	OutputString("This function displays the definitions, properties");
	OutputNewline();
	OutputString("and lemmas in order of chapters and by alphabetical");
	OutputNewline();
	OutputString("order within each chapter. Begin chapters with the");
	OutputNewline();
	OutputString("command Chapter mychaptername.");
	OutputNewline();
	OutputNewline();
	OutputString("CONTENTS:");

	for (k=0; k<chapterLineL; k++){
		chapterStart = chapterLine[k];
		AnalyseField2(CoqLines[chapterStart].f);
		if (loadedFields2L <2){
			OutputNewline();
			OutputString("Chapter command syntax ERROR");
			WriteString(" in line ");
			MyAppendInt(chapterStart);
			OutputString(fieldWritten);
			SendOutputToFile();
			return;
		}
		chapterName = loadedFields2[1];
		OutputNewline();
		OutputString("---");
		OutputField(chapterName);
	}

	OutputNewline();
	OutputNewline();


	// go chapter by chapter
	for (k=0; k<chapterLineL; k++){
		chapterStart = chapterLine[k];
		chapterBound = chapterLine[k+1];
		AnalyseField2(CoqLines[chapterStart].f);
		if (loadedFields2L <2){
			OutputNewline();
			OutputString("ERROR");
			return;
		}
		chapterName = loadedFields2[1];
		OutputNewline();
		OutputNewline();
		OutputString("CHAPTER: ");
		OutputField(chapterName);
	
	


	// output Definitions first : 
	OutputNewline();
	OutputNewline();
	for (i=0; i<DictionaryL; i++){
		if (Dictionary[i].ReferenceType == Definition){
		ourline = Dictionary[i].lineReference;
		if ((ourline >= chapterStart) && (ourline < chapterBound)){
			debugThreshold = 0;
			OutputNewline();
			AnalyseField(CoqLines[ourline].f);
			WriteField(chapterName);
			MyAppendString("--Definition ");
			for (j=1; j<loadedFieldsL-1; j++){
				PotentialBreak();
				MyAppendField(loadedFields[j]);
				MyAppendString(" ");
			}
			MyAppendString(".");
			OutputString(fieldWritten);
			OutputNewline();
		}
		}

	}
	OutputNewline();
	OutputNewline();
	for (i=0; i<DictionaryL; i++){
		if (Dictionary[i].ReferenceType == Property){
		ourline = Dictionary[i].lineReference;
		if ((ourline >= chapterStart) && (ourline < chapterBound)){
			debugThreshold = 0;
			OutputNewline();
			AnalyseField(CoqLines[ourline].f);
			WriteField(chapterName);
			MyAppendString("--Property ");
			for (j=1; j<loadedFieldsL-1; j++){
				PotentialBreak();
				MyAppendField(loadedFields[j]);
				MyAppendString(" ");
			}
			MyAppendString(".");
			OutputString(fieldWritten);
			OutputNewline();
		}
		}

	}
	OutputNewline();
	OutputNewline();
	for (i=0; i<DictionaryL; i++){
		if (Dictionary[i].ReferenceType == Lemma){
		ourline = Dictionary[i].lineReference;
		if ((ourline >= chapterStart) && (ourline < chapterBound)){
			debugThreshold = 0;
			OutputNewline();
			AnalyseField(CoqLines[ourline].f);
			WriteField(chapterName);
			MyAppendString("--Lemma ");
			for (j=1; j<loadedFieldsL-1; j++){
				PotentialBreak();
				MyAppendField(loadedFields[j]);
				MyAppendString(" ");
			}
			MyAppendString(".");
			OutputString(fieldWritten);
			OutputNewline();
		}
		}

	}

	


	}	// end k loop

SendOutputToFile();

}

void TreatExport(){

int val;

int i,j;

debugThreshold = 2;

val = ReadInputFromFile();
if (val < 0) return;
debugThreshold = 0;

// here we output the standard grammar 
debugThreshold = 0;
OutputNewline();
OutputString("This function creates: (1) a list of relevant grammar commands");
OutputNewline();
OutputString("which should be included at the top of any file; then");
OutputNewline();
OutputString("(2) a list of parameters, axioms, definitions, properties and");
OutputNewline();
OutputString("lemmas from the file, suitable for exporting to a new file. With");
OutputNewline();
OutputString("the given grammar, Coq will treat the exported lemmas as axioms.");
OutputNewline();
OutputString("NOTA: the grammar is written for Coq 6.3 and may need to be");
OutputNewline();
OutputString("changed for version 7.0");
OutputNewline();
OutputString("To search for results in the file use the command z instead.");
OutputNewline();



OutputNewline();
OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("rlemma_cmd [ \"RLemma\" command:command($a) \":\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [ <:vernac:<Axiom $a : $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("rparam_cmd [ \"RParameter\" command:command($a) \":\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Parameter $a : $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("rdef_cmd [ \"RDefinition\" command:command($a) \":=\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Definition $a := $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("raxiom_cmd [ \"RAxiom\" command:command($a) \":\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Axiom $a : $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("rproperty_cmd [ \"RProperty\" command:command($a) \":=\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Definition $a := $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("chapter_cmd [ \"Chapter\" command:command($a)  \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Definition $a := TRUE.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("property_cmd [ \"Property\" command:command($a) \":=\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Definition $a := $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("uremark_cmd [ \"URemark\" command:command($a) \":\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Remark $a : $b.>> ].");
OutputNewline();
OutputNewline();

OutputString("Grammar vernac vernac :=");
OutputNewline();
OutputString("outremark_cmd [ \"OutRemark\" command:command($a) \":\" command:command($b) \".\" ]");
OutputNewline();
OutputString("-> [<:vernac:<Theorem $a : $b.>> ].");
OutputNewline();
OutputNewline();


for (i=0; i<CoqLinesL; i++){
if (CoqLines[i].LineType == Chapter){
	debugThreshold = 0;
	OutputNewline();
	AnalyseField(CoqLines[i].f);
	WriteString("Chapter ");
	for (j=1; j<loadedFieldsL-1; j++){
		PotentialBreak();
		MyAppendField(loadedFields[j]);
		MyAppendString(" ");
	}
	MyAppendString(".");
	OutputString(fieldWritten);
	OutputNewline();
}
if (CoqLines[i].LineType == Parameter){
	debugThreshold = 0;
	OutputNewline();
	AnalyseField(CoqLines[i].f);
	WriteString("RParameter ");
	for (j=1; j<loadedFieldsL-1; j++){
		PotentialBreak();
		MyAppendField(loadedFields[j]);
		MyAppendString(" ");
	}
	MyAppendString(".");
	OutputString(fieldWritten);
	OutputNewline();
}
if (CoqLines[i].LineType == Definition){
	debugThreshold = 0;
	OutputNewline();
	AnalyseField(CoqLines[i].f);
	WriteString("RDefinition ");
	for (j=1; j<loadedFieldsL-1; j++){
		PotentialBreak();
		MyAppendField(loadedFields[j]);
		MyAppendString(" ");
	}
	MyAppendString(".");
	OutputString(fieldWritten);
	OutputNewline();
}
if (CoqLines[i].LineType == Axiom){
	debugThreshold = 0;
	OutputNewline();
	AnalyseField(CoqLines[i].f);
	WriteString("RAxiom ");
	for (j=1; j<loadedFieldsL-1; j++){
		PotentialBreak();
		MyAppendField(loadedFields[j]);
		MyAppendString(" ");
	}
	MyAppendString(".");
	OutputString(fieldWritten);
	OutputNewline();
}
if (CoqLines[i].LineType == Lemma){
	val = LoadLemma(i);
	if (val > 0){
		debugThreshold = 0;
		OutputNewline();
		WriteString("RLemma ");
		MyAppendField(lemmaName);
		MyAppendString(" : ");
		PotentialBreak();
		MyAppendVariables();
		for (j=0; j<lemmaClauseL ; j++){
			PotentialBreak();
			MyAppendString("(");
			MyAppendField(lemmaClause[j].written);
			MyAppendString(") -> ");
		
		}
		PotentialBreak();
		MyAppendString("(");
		MyAppendField(lemmaConclusion);
		MyAppendString(").");
		OutputString(fieldWritten);
		OutputNewline();
		
		
	
	

	}
}
if (CoqLines[i].LineType == Property){
	val = BreakDownLine(i);
	if (val > 0){
		debugThreshold = 0;
		OutputNewline();
		WriteString("RProperty ");
		MyAppendField(lemmaName);
		MyAppendString(" := ");
		PotentialBreak();
		MyAppendVariables();
		for (j=0; j<lemmaClauseL ; j++){
			PotentialBreak();
			MyAppendString("(");
			MyAppendField(lemmaClause[j].written);
			MyAppendString(") -> ");
		
		}
		PotentialBreak();
		MyAppendString("(");
		MyAppendField(lemmaConclusion);
		MyAppendString(").");
		OutputString(fieldWritten);
		OutputNewline();
	
	}

}
}


// now we open a file to write

SendOutputToFile();


}

void TreatEndSec(){
	// this treats the end section command

	
int val;

int i,j;



int opensectionline;
FIELD sectionName;
FIELD varfield;

int totalResults;
FIELD thmConclusion;

debugThreshold = 2;

val = ReadInputFromFile();
if (val < 0) return;
	

totalResults = 0;
sectionDepth = 0;

SetOpensection();	// sets the opensection parameter in CoqLines

debugThreshold = 0;

OutputNewline();
OutputString("This function creates the material that should be");
OutputNewline();
OutputString("added to the file in order to close the current section.");
OutputNewline();
OutputString("It writes out the theorems corresponding to results");
OutputNewline();
OutputString("which have been declared using the OutRemark ?: ?.");
OutputNewline();
OutputString("command, and also tries to alpha-unify them with");
OutputNewline();
OutputString("known Properties. Note that because of the weird Coq");
OutputNewline();
OutputString("cooking recipe, you may have to erase in the proof");
OutputNewline();
OutputString("any hypotheses or variables which are not effectively used.");
OutputNewline();


debugThreshold = 1;

opensectionline = CoqLinesL;

for (i=CoqLinesL-1;i>= 0; i=i-1){
	if (CoqLines[i].opensection == 1){
		if (CoqLines[i].LineType == Section){
			opensectionline = i;
			break;
		}
	}

}

if (opensectionline >= CoqLinesL){
	debugThreshold = 0;
	OutputNewline();
	OutputString("Didn't find a section to close");
	SendOutputToFile();
	return;
}

if (opensectionline < 0){
	debugThreshold = 0;
	OutputNewline();
	OutputString("error in opensectionline");
	SendOutputToFile();
	return;
}

AnalyseField(CoqLines[opensectionline].f);
if (loadedFieldsL != 3){
	debugThreshold = 0;
	OutputNewline();
	OutputString("opensectionline doesn't appear to open a section");
	SendOutputToFile();
	return;
}

sectionName = loadedFields[1];

debugThreshold = 0;

freeVariableL = 0;
lemmaClauseL = 0;



OutputNewline();
OutputNewline();
WriteString("End ");
MyAppendField(sectionName);
MyAppendString(".");
OutputString(fieldWritten);
OutputNewline();

SetMaxIndex();

for (i=opensectionline; i<CoqLinesL; i++){
	
	if (CoqLines[i].opensection == 1){
	if ((CoqLines[i].LineType == Variable)|(CoqLines[i].LineType == Variables)){

		AnalyseField(CoqLines[i].f);
		if (loadedFieldsL < 5){
			printf("\nincorrect Variable line syntax\n");
			return;
		}
		varfield.fs = loadedFields[1].fs;
		varfield.ls = loadedFields[loadedFieldsL -2].ls;

		val = LoadAnyVariables(varfield);
		if (val < 0){
			printf("\ncouldnt load variables\n");
			return;
		}
		//
		debugThreshold = 1;
		OutputNewline();
		WriteString("current variables : ");
		for (j=0; j<freeVariableL; j++){
			MyAppendField(freeVariable[j].name);
			MyAppendString(":");
			MyAppendField(freeVariable[j].type);
			MyAppendString(" ");
		}
		OutputString(fieldWritten);
		OutputNewline();

	}
	if (CoqLines[i].LineType == Hypothesis){
		AnalyseField(CoqLines[i].f);
		if (loadedFieldsL != 5){
			printf("\nincorrect Hypothesis line syntax\n");
			return;
		}
		if (lemmaClauseL >= LEMSIZE){
			printf("\ntoo many hypotheses\n");
			return;
		}
		if (lemmaClauseL < 0){
			printf("\nerror lemmaClause < 0\n");
			return;
		}
		lemmaClause[lemmaClauseL].written = loadedFields[3];
		lemmaClause[lemmaClauseL].resultName = loadedFields[1];
		lemmaClauseL = lemmaClauseL + 1;
		//
		debugThreshold = 1;
		OutputNewline();
		OutputString("current hypotheses ");
		for (j=0; j<lemmaClauseL; j++){
			OutputField(lemmaClause[j].written);
			OutputString(" ");
		}
		OutputNewline();



	}
	if (CoqLines[i].LineType == OutRemark){
		AnalyseField(CoqLines[i].f);
		if (loadedFieldsL != 5){
			printf("\nincorrect OutRemark line syntax\n");
			return;
		}
		debugThreshold = 0;
		outRemarkName = loadedFields[1];
		thmConclusion = loadedFields[3];
		totalResults = totalResults + 1;
		
		WriteString("a");
		fieldWrittenL = 0;
		fieldWritten[0]=0;
		MyAppendVariablesNB();
		for (j=0; j<lemmaClauseL; j++){
			MyAppendField(lemmaClause[j].written);
			MyAppendString(" -> ");
		}
		MyAppendField(thmConclusion);
		
		// here we try to output the result as a Remark
		MaybeOutputRemark(fieldWritten);
		// now we output the theorem
		debugThreshold = 0;
		OutputNewline();
		WriteString("Lemma ");
		MyAppendField(sectionName);
		fieldWrittenL = fieldWrittenL - 1;
		fieldWritten[fieldWrittenL]=0;
		if (totalResults > 1){
			MyAppendString("_");
			MyAppendInt(totalResults);
		}
		MyAppendString(" : ");
		MyAppendVariables();
		for (j=0; j<lemmaClauseL; j++){
			PotentialBreak();
			MyAppendField(lemmaClause[j].written);
			MyAppendString(" -> ");
		}
		PotentialBreak();
		MyAppendField(thmConclusion);
		
		MyAppendString(".");
		OutputString(fieldWritten);
		OutputNewline();
		// print out the full proof
		// that way it is easier to change in case of
		// a hypothesis or variable that isnt used
		// later: add a toggle to determine whether we
		// do this or whether we do the short proof
		OutputString("Proof");
		OutputNewline();
		WriteString("");
		for (j=0; j<freeVariableL; j++){
			freeVariable[j].oldkind = freeVariable[j].kind;
			freeVariable[j].kind = external;
		}
		MyAppendVariables();
		for (j=0; j<freeVariableL; j++){
			freeVariable[j].kind = freeVariable[j].oldkind;
		}
		for (j=0; j<lemmaClauseL; j++){
			PotentialBreak();
			MyAppendString("[");
			MyAppendField(lemmaClause[j].resultName);
			MyAppendString(" : ");
			MyAppendField(lemmaClause[j].written);
			MyAppendString("] ");
		}
		PotentialBreak();
		MyAppendString("(");
		MyAppendField(outRemarkName);
		for (j=0; j<freeVariableL; j++){
			MyAppendString(" ");
			MyAppendField(freeVariable[j].name);
		}
		for (j=0; j<lemmaClauseL; j++){
			MyAppendString(" ");
			MyAppendField(lemmaClause[j].resultName);
		}
		MyAppendString(").");
		OutputString(fieldWritten);
		OutputNewline();


	}
	}	// end opensection == 1
}


// now we open a file to write

SendOutputToFile();


}

int Unify(){
	// tries to unify fieldWritten3 and fieldWritten4
	// with the variables loaded in freeVariable;
	// the instance fields will refer to fieldWritten4
	// the variables occur in fieldWritten3.
	// returns 1 if successful, -e if not. 

	int cursor3, cursor4;
	int next3, next4;
	int val;
	int i,j,k;
	char ch, ch2;
	int toggle;
	int whichFV;
	int parlevel;
	int count;
	int instanceLength, instanceBase;

	cursor3 = 0;
	cursor4 = 0;
	
	count = 0;

	while(cursor3 < fieldWritten3L -1){
		// we put the next field3 in fieldWritten2
		fieldWritten2L = 0;
		next3 = fieldWritten3L -1;
		for (i = cursor3 + 1; i<fieldWritten3L; i++){
			ch = fieldWritten3[i];
			if (ch == ' '){
				next3 = i;
				break;
			}
			if (fieldWritten2L < FIELDLENGTH){
				fieldWritten2[fieldWritten2L] = ch;
				fieldWritten2L = fieldWritten2L + 1;
			}
		}
		fieldWritten2[fieldWritten2L] = 0;
		// now we try to see if this corresponds to a freeVariable
		whichFV = -1;
		for (k=0; k<freeVariableL; k++){
			WriteField(freeVariable[k].name);
			val = MyStringCompare(fieldWritten, fieldWritten2);
			if (val == 0){
				whichFV = k;
				break;
			}
		}
		// now there are two cases depending on whether we found
		// a freeVariable or not
		if (whichFV < 0){
			fieldWrittenL = 0;
			next4 = fieldWritten4L -1;
			for (i=cursor4 + 1; i<fieldWritten4L; i++){
				ch = fieldWritten4[i];
				if (ch == ' '){
					next4 = i;
					break;
				}
				if (fieldWrittenL < FIELDLENGTH){
					fieldWritten[fieldWrittenL] = ch;
					fieldWrittenL = fieldWrittenL + 1;
				}
			}
			fieldWritten[fieldWrittenL]= 0;
			val = MyStringCompare(fieldWritten, fieldWritten2);
			if (val != 0){
				debugThreshold = 2;
				OutputNewline();
				OutputString("failed to unify at ");
				OutputString(fieldWritten);
				OutputString(" != ");
				OutputString(fieldWritten2);
				OutputNewline();
				return -1;
			}
		}
		else{
			// now there are again two cases depending on whether
			// the freeVariable has already been instantiated or not
			if (freeVariable[whichFV].status != set){
				parlevel = 0;
				for (j=cursor4 + 1; j<fieldWritten4L; j++){
					ch = fieldWritten4[j];
					if (ch == '(') parlevel = parlevel + 1;
					if (ch == ')') parlevel = parlevel -1;
					if ((ch == ' ') && (parlevel <= 0)){
						next4 = j;
						freeVariable[whichFV].instance.fs = cursor4;
						freeVariable[whichFV].instance.ls = j;
						freeVariable[whichFV].status = set;
						break;
					}
				}
				if (freeVariable[whichFV].status != set){
					debugThreshold = 2;
					OutputNewline();
					OutputString(" unable to instantiate a variable ");
					OutputNewline();
					return -2;
				}

			}
			else{
				// in this case we have to compare what is in place with the instance
				instanceLength = freeVariable[whichFV].instance.ls - freeVariable[whichFV].instance.fs;
				instanceBase = freeVariable[whichFV].instance.fs;
				for (j=0; j<= instanceLength; j++){
					toggle = -1;
					if (j + cursor4 < fieldWritten4L){
					if (instanceBase + j < fieldWritten4L){
					if (instanceBase + j >= 0){
							ch = fieldWritten4[j+ cursor4];
							ch2 = fieldWritten4[j+ instanceBase];
							if (ch == ch2) toggle = 1;
					}
					}
					}
					if (toggle < 0){
						debugThreshold = 2;
						OutputNewline();
						OutputString(" non corresponding instantiation ");
						OutputNewline();
						return -3;
					}
				}
				next4 = cursor4 + instanceLength;
			}
		}
		// now were done for the while loop
		cursor3 = next3;
		cursor4 = next4;
		count = count+ 1;
		if (count > 200){
			debugThreshold = 2;
			OutputNewline();
			OutputString(" stepped out of unify because of more than 200 tries ");
			OutputNewline();
			return -4;
		}

	}

	// now we have theoretically instantiated everything
	// but we should check to see (in practice one can get to
	// here without having instantiated all variables).

	for (k=0; k<freeVariableL; k++){
		if (freeVariable[k].status != set){
			debugThreshold = 1;
			OutputNewline();
			OutputString(" not all variables were instantiated ");
			OutputNewline();
			return -5;
		}
	}

	return 1;


}

void MaybeOutputRemark(char *thmwritten){
	// looks for properties to unify with the statement written in the 
	// thmwritten string. 

	
	int i,j,k,l,m;
	
	int val;
	char ch, ch2;

	char normThm[FIELDLENGTH + 20];
	int normThmL;
	int normThmNL;
	


	FIELD propField;
	FIELD ourInstance;


	FREEVAR freeVariableOld[NUMFIELDS + 10];
	CLAUSE lemmaClauseOld[LEMSIZE + 10];
	FIELD lemmaConclusionOld;
	FIELD conclusionNameOld;
	FIELD lemmaNameOld;

	int freeVariableOldL, lemmaClauseOldL;

	lemmaConclusionOld = lemmaConclusion;
	conclusionNameOld = conclusionName;
	lemmaNameOld = lemmaName;
	freeVariableOldL = freeVariableL;
	lemmaClauseOldL = lemmaClauseL;
	for (i=0; i<freeVariableL; i++){
		freeVariableOld[i].instance = freeVariable[i].instance;
		freeVariableOld[i].kind = freeVariable[i].kind;
		freeVariableOld[i].name = freeVariable[i].name;
		freeVariableOld[i].status = freeVariable[i].status;
		freeVariableOld[i].type = freeVariable[i].type;
	}
	for (i=0; i<lemmaClauseL; i++){
		lemmaClauseOld[i].written = lemmaClause[i].written;
		lemmaClauseOld[i].resultName = lemmaClause[i].resultName;
	}
	

	
	normThm[0] = ' ';
	normThmL = 1;
	for (i=0; i<FIELDLENGTH; i++){
		ch = thmwritten[i];
		if (ch == 0) break;
		if (normThmL > FIELDLENGTH) break;
		if ((ch == '(') | (ch == '[') | (ch == ')') | (ch == ']')){
			normThm[normThmL] = ' ';
			normThmL = normThmL + 1;
		}
		normThm[normThmL] = ch;
		normThmL = normThmL + 1;
		if ((ch == '(') | (ch == '[') | (ch == ')') | (ch == ']')){
			normThm[normThmL] = ' ';
			normThmL = normThmL + 1;
		}



	}
	normThm[normThmL] = ' ';
	normThmL = normThmL + 1;
	normThm[normThmL] = 0;

	if (normThmL > FIELDLENGTH + 5){
		debugThreshold = 2;
		OutputString("ERROR IN MAYBE...");
		return;
	}

	normThmNL = 1;
	for (i=1; i<normThmL; i++){
		ch = normThm[i];
		ch2 = normThm[i-1];
		if ((ch2 != ' ') | (ch != ' ')){
			normThm[normThmNL] = ch;
			normThmNL = normThmNL + 1;
		}
	}
	normThmL = normThmNL;
	normThm[normThmL] = 0;




	debugThreshold = 1;
	OutputNewline();
	OutputString("testing for a property that looks like");
	OutputNewline();
	OutputString(normThm);
	OutputNewline();

	for (i=0; i<normThmL; i++){
		fieldWritten4[i] = normThm[i];
	}
	fieldWritten4[normThmL] = 0;
	fieldWritten4L = normThmL;

	
	
	for (i=0; i<CoqLinesL; i++){
	if (CoqLines[i].LineType == Property){
		val = BreakDownLine(i);
		if (val > 0){
			WriteField(lemmaName);
			debugThreshold = 1;
			OutputNewline();
			OutputString("looking at property ");
			OutputString(fieldWritten);
			OutputNewline();
		AnalyseField(CoqLines[i].f);
		if (loadedFieldsL >=5){
			propField.fs = loadedFields[3].fs;
			for (j=3; j<loadedFieldsL-1; j++){
				val = CheckFieldBoundType(loadedFields[j]);
				if (val != 2){
					propField.fs = loadedFields[j].fs;
					break;
				}
			}
			propField.ls = loadedFields[loadedFieldsL -2].ls;

			WriteField(propField);
			debugThreshold = 2;
			OutputString(" written as ");
			OutputString(fieldWritten);
			OutputNewline();
			fieldWritten3[0] = ' ';
			fieldWritten3L = 1;
			for (m=0; m<fieldWrittenL; m++){
				fieldWritten3[fieldWritten3L] = fieldWritten[m];
				fieldWritten3L = fieldWritten3L + 1;
			}
			fieldWritten3[fieldWritten3L] = ' ';
			fieldWritten3L = fieldWritten3L + 1;
			fieldWritten3[fieldWritten3L] = 0;
			val = Unify();
			if (val > 0){
				debugThreshold = 0;
				OutputNewline();
				WriteString("Remark autout_");
				maxIndex = maxIndex + 1;
				MyAppendInt(maxIndex);
				MyAppendString(" : ");
				if (freeVariableL > 0){
					if (freeVariable[0].kind == external) MyAppendString("(");
				}
				MyAppendField(lemmaName);
				for (k=0; k<freeVariableL; k++){
					if (freeVariable[k].kind == external){
						MyAppendString(" ");
						ourInstance = freeVariable[k].instance;
						for (l=ourInstance.fs + 1; l < ourInstance.ls; l++){
							ch = 'x';
							if ((0 <= l) && (l < fieldWritten4L)) ch = fieldWritten4[l];
							if (fieldWrittenL < FIELDLENGTH){
								fieldWritten[fieldWrittenL] = ch;
								fieldWrittenL = fieldWrittenL + 1;
								fieldWritten[fieldWrittenL] = 0;
							}

						}

					}

				}
				if (freeVariableL > 0){
					if (freeVariable[0].kind == external) MyAppendString(")");
				}
				MyAppendString(".");
				OutputString(fieldWritten);
				OutputNewline();
				WriteString("Proof ");
				MyAppendField(outRemarkName);
				MyAppendString(".");
				OutputString(fieldWritten);
				OutputNewline();

			}
			

			
		}
		}
	}
	}

	lemmaConclusion = lemmaConclusionOld;
	conclusionName= conclusionNameOld;
	lemmaName = lemmaNameOld;
	freeVariableL = freeVariableOldL;
	lemmaClauseL = lemmaClauseOldL;
	for (i=0; i<freeVariableL; i++){
		freeVariable[i].instance = freeVariableOld[i].instance;
		freeVariable[i].kind = freeVariableOld[i].kind;
		freeVariable[i].name = freeVariableOld[i].name;
		freeVariable[i].status = freeVariableOld[i].status;
		freeVariable[i].type = freeVariableOld[i].type;
	}
	for (i=0; i<lemmaClauseL; i++){
		lemmaClause[i].written = lemmaClauseOld[i].written;
		lemmaClause[i].resultName = lemmaClauseOld[i].resultName;
	}

}



void SendOutputToFile(){

char filename[220];
int check;
int i;

check = CheckCurrentFile();
	
if (check == 0){
	printf("\nthe target file is no longer valid\n");
	return;
}
if (currentFilenameL > 200) return;
if (currentFilenameL <0) return;

for (i=0; i<currentFilenameL; i++){
	filename[i]=currentFilename[i];
}
filename[currentFilenameL] = 'O';
filename[currentFilenameL + 1] = 'U';
filename[currentFilenameL + 2] = 'T';
if (extensionToggle == 0){
	filename[currentFilenameL + 3] = '.';
	filename[currentFilenameL + 4] = 'h';
	filename[currentFilenameL + 5] = 't';
	filename[currentFilenameL + 6] = 'm';
	filename[currentFilenameL + 7] = 'l';
	filename[currentFilenameL + 8] = 0;
}
else{
	filename[currentFilenameL + 3] = '.';
	filename[currentFilenameL + 4] = 'v';
	filename[currentFilenameL + 5] = 0;
}



PrintOutputToFile(filename);
// note that the file is opened then closed in that procedure

printf("\n - - - - return to shell - - - - \n");


}



main(int argc, char *argv[]){

int guess; // guess how big the file should be




CheckFieldToggle = 0;

printf("\nThis program reads a Coq file and outputs in a different");
printf("\nfile some suggestions for what to write in the original");
printf("\nfile. The basic function r implements a type of forward");
printf("\nautomatization, suggesting all of the things one can  ");
printf("\nconclude in the current situation on the basis of known");
printf("\nlemmas and remarks. Also has functions to end the current");
printf("\nsection and draw appropriate conclusions, to create some");
printf("\napply_ lemmas from properties, and to export stuff to a");
printf("\nnew file. Type q to quit at any time.");

printf("\n---License:");
printf("by typing anything other than q or by looking");
printf("\nat the source code, you agree that if you develop or hear");
printf("\nof a program that does something like this but better,");
printf("\nyou will let me know at carlos@math.unice.fr.");
printf("\n---Carlos Simpson, June 2001\n");


guess = 1000000L;


InitArrays(guess);

////////////

MainShell();

////////////


printf("\nFreeing up memory\n");

free(aPin);
free(aPout);
free(normalizedData);
free(CoqLines);
free(Dictionary);


printf("\nDone\n");





}