/*************************************************************************** * File: pfnum.c * * Last modified on Mon 15 August 2011 at 17:47:19 PST by lamport * * * * pfnum [-N] [-c | -d] file * * * * Recompute labels for LaTeX "pf" style style "proof" environments. * * The file "file.tex" is renamed "file.pfx", and is replaced by * * the new version. * * * * switches: * * -d : Puts "%%%{long-lbl}" right after every \begin{[no]proof} and * * \end{[no]proof}, where long-lbl is the long label for the * * step of which this is a proof, and deletes anything else * * following the "{proof}" on the same line. * * * * -N : (N is any natural number) * * Converts all proof step labels in file.tex to their * * output form, assuming that all levels < N have long-form * * numbers and all levels >= N have short-form numbers. * * (Default value of N is 0.) * * * * -c : Ignores "%"s, so it converts labels in comments. Without * * this switch, anything between a "%" and the end of a line * * is assumed to be a comment and is not converted. With * * this switch, the sequence "%%%{label}" is treated by * * pfnum as if it were "\stepref{label}". This is useful * * for identifying an "\end{proof}" command * ***************************************************************************/ #include #include #include /*************************************************************************** * MISC GLOBAL VARIABLES * * short_number_depth : produces short-style numbers for all depths * * >= this value * * file_arg : string holding name of file argument * * no_comments : 0 = do not convert comments * * 1 = convert comments * * add_comment_labels : 0 = do not add comments after \begin-\end's. * * 1 = do add comments after \begin-\end's. * **************************************************************************/ int short_number_depth = 0; int no_comments = 0; int add_comment_labels = 0; char file_arg[128]; /*************************************************************************** * LINE LOOP VARIABLES * * line : line currently being transformed. * * line_num : number of lines preceding the current one * * in the input file * * * * level : The number of proof environments that the input is * * currently within. Assumed to be <= MAX_LEVEL * * * * label_num[lev] : The number of the last step encountered at level lev, * * for lev <= level. Must be <= MAX_LABEL_NUM. * * * * labels[lev][num] : The symbolic label of step num of the input * * file, for lev <= level and num <= label_num[lev]. * * labels[level][label_num[level]] always equals the * * null string. * * * * initialize_line_loop_variables() * * Initializes the line loop variables * **************************************************************************/ #define MAX_LINE_LENGTH 500 /* Maximum length of a single input or output line */ #define MAX_LEVEL 20 /* Maximum proof depth */ #define MAX_LABEL_NUM 30 /* Maximum number of steps per proof */ #define MAX_LABEL_LENGTH 30 /* Maximum number of chars per label */ char line[MAX_LINE_LENGTH]; int line_num; int level; int label_num[MAX_LEVEL+1]; char labels[MAX_LEVEL+1][MAX_LABEL_NUM+1][MAX_LABEL_LENGTH+1]; void initialize_line_loop_variables() { line_num = 0; level = 0; label_num[level] = 0; labels[0][0][0] = '\0'; } /*************************************************************************** * FILE HANDLING * * VARIABLES * * ipf_name : Name of input file. * * ipf : Input file hanldle. * * opf_name : Name of output file. * * opf : Output file hanldle. * * * * open_files() * * Opens the input and output files. * * * * close_files() * * Closes the input and output files. * * * * read_input_line() * * line := next line * * returns 0 iff end of input file * * * * write_output_line() * * writes line to the output file * **************************************************************************/ char ipf_name[500]; char opf_name[500]; FILE *ipf; FILE *opf; void open_files() { /* get input-file name */ strcpy(ipf_name, file_arg); if (strchr(ipf_name, '.') == NULL){strcat(ipf_name, ".tex");}; /* get output-file name */ strcpy(opf_name, file_arg); strcat(opf_name, ".tmp"); if ((ipf = fopen(ipf_name, "r")) == NULL) { fprintf(stderr, "Couldn't open input file '%s'\n", ipf_name); exit(-1); } if ((opf = fopen(opf_name, "w")) == NULL) { fprintf(stderr, "Couldn't open output file '%s'\n", opf_name); exit(-1); } } void close_files() { char cmd[128]; fclose(opf); fclose(ipf); sprintf(cmd, "mv %s %s.pfx ; mv %s %s", ipf_name, file_arg, opf_name, ipf_name); system(cmd); } int read_input_line() { if (fgets(line, MAX_LINE_LENGTH, ipf) == NULL) { return(0); } else { return(1); } } void write_output_line() { // In 18 Feb 1998, this used to be only // if (fputs(line, opf) == NULL) // It was changed on 15 Aug 2011 to #if defined(WIN32) || defined(__CYGWIN__) if (fputs(line, opf) != 0) #else if (fputs(line, opf) == NULL) #endif { fprintf(stderr, "Error writing output file\n"); exit(-1); } } /*************************************************************************** * find_next_command(pos) * * Searches for the next command in line, starting from character * * position pos. * * If a command is found, then * * returns the character position after the command. * * command := number of the command. (an integer) * * argument := its argument (a string) * * arg_pos := character position of start of the argument * * arg_length := length of argument * * If no command is found, then * * returns -1 * **************************************************************************/ #define BEGIN_PROOF 1 #define BEGIN_NOPROOF 2 #define STEP 3 #define NOSTEP 4 #define STEPREF 5 #define LEVELREF 6 #define END_PROOF 7 #define END_NOPROOF 8 #define QEDSTEP 9 int found_pos; /* pointer to earliest command found */ int command; char argument[MAX_LINE_LENGTH]; int arg_pos; int arg_length; int next_pos; /* FOR DEBUGGING */ void print_state() { char str[MAX_LABEL_LENGTH +1]; int lev, step; str[0] = '\0'; strncat(str, line + arg_pos, arg_length); printf( "line %d, current argument '%s'\n", line_num, str); printf("level %d, step %d\n", level, label_num[level]); lev = 1; while (lev <= level) { printf(" label_num[%d] = %d\n", lev, label_num[lev]); step = 0; while (step < label_num[lev]) { printf(" labels[%d][%d] = '%s'\n", lev, step, labels[lev][step]); step++; } lev++; } } void look_for(char *cmd_str, /* command string */ int cmd, /* command number */ int pos, /* starting position */ int get_arg /* 0 = no argument, 1 = arg ended by "}" */ ) /*************************************************************************** * looks for first instance of cmd_str starting from line[pos]; * * if it finds one earlier or at the same position as found_pos, then * * it sets found_pos to that value, sets command to cmd, and * * sets arg_pos to point to the first character after the found string * **************************************************************************/ { int temp; /* DEBUG printf("lookfor, line %d, pos %d\n", line_num, pos); printf("cmd_str = %s\n", cmd_str); printf("line[pos] = %s\n", line + pos); */ if ((temp = strstr(line+pos, cmd_str)) == NULL) { return; } /* printf("found: temp = %d, found_pos = %d\n", temp, found_pos); */ if (temp > found_pos) { return; } found_pos = temp; command = cmd; arg_pos = temp - (int) line + strlen(cmd_str); if (get_arg == 0) { next_pos = arg_pos; arg_length = 0; } else { if ((temp = strstr(line+arg_pos, "}")) == NULL) { fprintf(stderr, "Missing '}' on line %d\n", line_num+1); arg_length = 0; return; } arg_length = temp -(int) line - arg_pos; next_pos = arg_pos + arg_length; } } int find_next_command(int pos) { found_pos = MAX_LINE_LENGTH + 99 + (int) line; look_for("\\begin{proof}", BEGIN_PROOF, pos, 0); look_for("\\begin{noproof}", BEGIN_NOPROOF, pos, 0); look_for("\\end{proof}", END_PROOF, pos, 0); look_for("\\end{noproof}", END_NOPROOF, pos, 0); look_for("\\step{", STEP, pos, 1); look_for("\\qedstep", QEDSTEP, pos, 0); look_for("\\nostep{", NOSTEP, pos, 1); look_for("\\stepref{", STEPREF, pos, 1); look_for("\\levelref{", LEVELREF, pos, 1); if (no_comments == 0) { look_for("%", -2, pos, 0); } else { look_for("%%%{", STEPREF, pos, 1); } if ( (found_pos == MAX_LINE_LENGTH + 99 + (int) line) || (command == -2) ) { return(-1); } return(arg_pos); } /*************************************************************************** * process_begin_proof() * * process_end_proof() * * process_step() * * process_ref() * * process_qedstep() * * Process a single command, with command, argument, arg_pos, and * * arg_length having the values set by find_next_command. * * Makes any necessary changes to line. * **************************************************************************/ void process_begin_proof() { char str[MAX_LABEL_LENGTH+1], str2[MAX_LABEL_LENGTH+1]; int lev; int cnt; char *comment_start; if (add_comment_labels == 1) { lev=0; sprintf(str, "%%%%%%{"); while (lev < level) { lev++; sprintf(str2, "%d.", label_num[lev]); strcat(str, str2); } if (strlen(str) > 4) {str[strlen(str)-1] = '\0'; }; strcat(str, "}\n"); /********************************************************************* * comment_start := ptr to beginning of comment position. * *********************************************************************/ if (command == BEGIN_PROOF) { comment_start = line + (found_pos - (int) line) + 13; } else /* Must be BEGIN_NOPROOF */ { comment_start = line + (found_pos - (int) line) + 15; }; /* DEBUG ******************************************** printf("line +13 = %d, ", (int) line+13); printf("comment_start = %d, ", (int) comment_start); printf("found_pos = %d\n", found_pos); printf("line: %s", line); printf("line+13 as string = %s\n", line+13); printf("comment_start as string = %s\n", comment_start); ********************************************/ strcpy(comment_start, str); }; level++; if (level > MAX_LEVEL) { fprintf(stderr, "proofs too deeply nested\n"); exit(-1); } label_num[level] = 0; labels[level][0][0] = '\0'; /* DEBUG printf("begin(proof) at level %d\n", level); */ } void process_end_proof() { char str[MAX_LABEL_LENGTH+1], str2[MAX_LABEL_LENGTH+1]; int lev; int cnt; char *comment_start; level--; if (add_comment_labels == 1) { lev=0; sprintf(str, "%%%%%%{"); while (lev < level) { lev++; sprintf(str2, "%d.", label_num[lev]); strcat(str, str2); } if (strlen(str) > 4) {str[strlen(str)-1] = '\0'; }; strcat(str, "}\n"); /********************************************************************* * comment_start := ptr to beginning of comment position. * *********************************************************************/ if (command == END_PROOF) { comment_start = line + (found_pos - (int) line) + 11; } else /* Must be END_NOPROOF */ { comment_start = line + (found_pos - (int) line) + 13; }; /* DEBUG ******************************************** printf("line +13 = %d, ", (int) line+13); printf("comment_start = %d, ", (int) comment_start); printf("found_pos = %d\n", found_pos); printf("line: %s", line); printf("line+13 as string = %s\n", line+13); printf("comment_start as string = %s\n", comment_start); ********************************************/ strcpy(comment_start, str); }; if (level < 0) { fprintf(stderr, "Extra \\end{proof} on line %d\n", line_num+1); level++; } /* DEBUG printf("end(proof) at level %d\n", level+1); */ } void insert_label(int lev, /* level number of new label */ int step /* step number of new label */ ) /*********************************************************************** * Inserts replaces current argument in line with * * new label "step". * **********************************************************************/ { char str[MAX_LABEL_LENGTH+1], str2[MAX_LABEL_LENGTH+1]; int len; int ptr; if (lev < short_number_depth) { /* PRODUCE LONG NUMBERS */ if (lev == 1) { sprintf(str, "%d", step); } else { sprintf(str, "%d", label_num[1]); ptr = 2; while (ptr < lev) { sprintf(str2, ".%d", label_num[ptr]); strcat(str, str2); ptr++; } sprintf(str2, ".%d", step); strcat(str, str2); } } else { /* PRODUCE SHORT NUMBERS */ sprintf(str, "<%d>%d", lev, step); } len = strlen(str); /* debug printf("inserting '%s', len = %d, arg_pos = %d, arg_length = %d\n", str, len, arg_pos, arg_length); */ if (len < arg_length) { ptr = arg_pos + arg_length; while (line[ptr] != '\0') { line[ptr - arg_length + len] = line[ptr]; ptr++; } line[ptr - arg_length + len] = '\0'; } if (len > arg_length) { ptr = strlen(line); while (ptr >= arg_pos+arg_length) { line[ptr - arg_length + len] = line[ptr]; ptr--; } } ptr = 0; while (str[ptr] != '\0') { line[arg_pos + ptr] = str[ptr]; ptr++; } /* DEBUG printf("line = '%s'\n", line); */ } int find_label(int *lev, /* set to level number of found label */ int *step /* set to step number of found label */ ) /* returns 0 if found, 1 if not found */ { int n, m; char str[MAX_LABEL_LENGTH +1]; str[0] = '\0'; strncat(str, line + arg_pos, arg_length); /* DEBUG printf("find_label(%s)\n", str); */ n = 1; while (n <= level) { m = 0; while (m < label_num[n]) { /* DEBUG printf(" comparing '%s' with labels[%d][%d] = '%s'\n", str, m, n, labels[m][n]); */ if (strcmp(str, labels[n][m]) == 0) { *lev = n; *step = m+1; /* DEBUG printf("found it\n"); */ return(0); } m++; } n++; } return(1); /* not found */ } void process_step() { int m, n; char str[MAX_LABEL_LENGTH +1]; if (find_label(&m, &n) != 1) { str[0] = '\0'; strncat(str, line + arg_pos, arg_length); fprintf(stderr, "Duplicate label '%s' on line %d\n", str, line_num+1); } labels[level][label_num[level]][0] = '\0'; strncat(labels[level][label_num[level]], line + arg_pos, arg_length); (label_num[level])++; insert_label(level, label_num[level]); /* DEBUG printf("added label '%s', at level = %d, step = %d\n", labels[level][label_num[level]-1], level, label_num[level]-1); */ } void process_qedstep() { (label_num[level])++; return; } void process_ref() { int lev, step; char str[MAX_LABEL_LENGTH +1]; if (find_label(&lev, &step) != 0) { str[0] = '\0'; strncat(str, line + arg_pos, arg_length); fprintf(stderr, "Undefined label '%s' on line %d\n", str, line_num+1); /* DEBUG print_state(); */ return; } insert_label(lev, step); } main(int argc, char *argv[]) { int pos; /* get arguments */ if ( (argc < 2) || (argc > 4) ) { fprintf(stderr, "Usage pfnum [-N] [-c] file \n"); exit(-1); } strcpy(file_arg, argv[argc-1]); /* DEBUG printf("file_arg = '%s'\n", file_arg); */ pos = 1; while (pos < argc-1) { if (*(argv[pos]+1) == 'c') { no_comments = 1; /* DEBUG printf("-c switch\n"); */ } else { if (*(argv[pos]+1) == 'd') { add_comment_labels = 1;} else {if (sscanf(argv[pos]+1, "%d", &short_number_depth) == 0) { fprintf(stderr, "Usage pfnum [-N] [-c] file\n"); exit(-1); } /* DEBUG ******************************************** printf("short_number_depth = %d\n", short_number_depth); *********************************************/ } } pos++; } open_files(); initialize_line_loop_variables(); /* main loop */ pos = 0; while (read_input_line() != 0) { /* Loop invariant: The line loop variables have the proper values */ while ( (pos = find_next_command(pos)) != -1 ) { /* Loop Invariant: command, argument, arg_pos, and pos have appropriate values */ /* DEBUG printf("found command %d, arg length %d at pos %d in '%s'", command, arg_length, arg_pos, line); */ switch (command) { case BEGIN_PROOF : case BEGIN_NOPROOF : process_begin_proof(); break; case END_PROOF : case END_NOPROOF : process_end_proof(); break; case STEP : case NOSTEP : /* DEBUG printf("process_step at line %d\n", line_num+1); */ process_step(); break; case QEDSTEP : process_qedstep(); break; case STEPREF : case LEVELREF : /* DEBUG printf("process_ref at line %d\n", line_num+1); */ process_ref(); break; default : fprintf(stderr, "This program has a bug\n"); exit(-1); } /* End switch */ } /* assertion: All commands in the current line have been processed */ write_output_line(); line_num++; pos = 0; } /* END while (read_input_line() != 0) */ /* have reached the end of file */ close_files(); while (level > 0) { fprintf(stderr, "unmatched \\begin{[no]proof}\n"); level--; } }