#include #include #include #include #include /* Redefine. Otherwise, systems (Unicos for one) with headers that define it to be a type get syntax errors for the variable declaration below. */ #include "system.h" #include "error.h" #include "fadvise.h" #include "quote.h" #include "xstrtol.h" /* The official name of this program (e.g., no 'g' prefix). */ #define PROGRAM_NAME "fmt" #define AUTHORS proper_name ("Ross Paterson") /* The following parameters represent the program's idea of what is "best". Adjust to taste, subject to the caveats given. */ /* Default longest permitted line length (max_width). */ #define WIDTH 75 /* Prefer lines to be LEEWAY % shorter than the maximum width, giving room for optimization. */ #define LEEWAY 7 /* The default secondary indent of tagged paragraph used for unindented one-line paragraphs not preceded by any multi-line paragraphs. */ #define DEF_INDENT 3 /* Costs and bonuses are expressed as the equivalent departure from the optimal line length, multiplied by 10. e.g. assigning something a cost of 50 means that it is as bad as a line 5 characters too short or too long. The definition of SHORT_COST(n) should not be changed. However, EQUIV(n) may need tuning. */ /* FIXME: "fmt" misbehaves given large inputs or options. One possible workaround for part of the problem is to change COST to be a floating-point type. There are other problems besides COST, though; see MAXWORDS below. */ typedef long int COST; #define MAXCOST TYPE_MAXIMUM (COST) #define SQR(n) ((n) * (n)) #define EQUIV(n) SQR ((COST) (n)) /* Cost of a filled line n chars longer or shorter than goal_width. */ #define SHORT_COST(n) EQUIV ((n) * 10) /* Cost of the difference between adjacent filled lines. */ #define RAGGED_COST(n) (SHORT_COST (n) / 2) /* Basic cost per line. */ #define LINE_COST EQUIV (70) /* Cost of breaking a line after the first word of a sentence, where the length of the word is N. */ #define WIDOW_COST(n) (EQUIV (200) / ((n) + 2)) /* Cost of breaking a line before the last word of a sentence, where the length of the word is N. */ #define ORPHAN_COST(n) (EQUIV (150) / ((n) + 2)) /* Bonus for breaking a line at the end of a sentence. */ #define SENTENCE_BONUS EQUIV (50) /* Cost of breaking a line after a period not marking end of a sentence. With the definition of sentence we are using (borrowed from emacs, see get_line()) such a break would then look like a sentence break. Hence we assign a very high cost -- it should be avoided unless things are really bad. */ #define NOBREAK_COST EQUIV (600) /* Bonus for breaking a line before open parenthesis. */ #define PAREN_BONUS EQUIV (40) /* Bonus for breaking a line after other punctuation. */ #define PUNCT_BONUS EQUIV(40) /* Credit for breaking a long paragraph one line later. */ #define LINE_CREDIT EQUIV(3) /* Size of paragraph buffer, in words and characters. Longer paragraphs are handled neatly (cf. flush_paragraph()), so long as these values are considerably greater than required by the width. These values cannot be extended indefinitely: doing so would run into size limits and/or cause more overflows in cost calculations. FIXME: Remove these arbitrary limits. */ #define MAXWORDS 1000 #define MAXCHARS 5000 /* Extra ctype(3)-style macros. */ #define isopen(c) (strchr ("(['`\"", c) != NULL) #define isclose(c) (strchr (")]'\"", c) != NULL) #define isperiod(c) (strchr (".?!", c) != NULL) /* Size of a tab stop, for expansion on input and re-introduction on output. */ #define TABWIDTH 8 /* Word descriptor structure. */ typedef struct Word WORD; struct Word { /* Static attributes determined during input. */ const char *text; /* the text of the word */ int length; /* length of this word */ int space; /* the size of the following space */ unsigned int paren:1; /* starts with open paren */ unsigned int period:1; /* ends in [.?!])* */ unsigned int punct:1; /* ends in punctuation */ unsigned int final:1; /* end of sentence */ /* The remaining fields are computed during the optimization. */ int line_length; /* length of the best line starting here */ COST best_cost; /* cost of best paragraph starting here */ WORD *next_break; /* break which achieves best_cost */ }; static WORD *word_limit; static char parabuf[MAXCHARS]; static char *wptr; static WORD word[MAXWORDS]; static int prefix_indent; static int first_indent; static int other_indent; static void flush_paragraph(){ WORD *split_point; WORD *w; int shift; COST best_break; /* In the special case where it's all one word, just flush it. */ if (word_limit == word) { fwrite (parabuf, sizeof *parabuf, wptr - parabuf, stdout); wptr = parabuf; return; } /* Otherwise: - format what you have so far as a paragraph, - find a low-cost line break near the end, - output to there, - make that the start of the paragraph. */ fmt_paragraph (); /* Choose a good split point. */ split_point = word_limit; best_break = MAXCOST; for (w = word->next_break; w != word_limit; w = w->next_break) { if (w->best_cost - w->next_break->best_cost < best_break) { split_point = w; best_break = w->best_cost - w->next_break->best_cost; } if (best_break <= MAXCOST - LINE_CREDIT) best_break += LINE_CREDIT; } put_paragraph (split_point); /* Copy text of words down to start of parabuf -- we use memmove because the source and target may overlap. */ memmove (parabuf, split_point->text, wptr - split_point->text); shift = split_point->text - parabuf; wptr -= shift; /* Adjust text pointers. *//* */ for (w = split_point; w <= word_limit; w++) w->text -= shift; /* Copy words from split_point down to word -- we use memmove because the source and target may overlap. */ memmove (word, split_point, (word_limit - split_point + 1) * sizeof *word); word_limit -= split_point - word; } static int get_line(FILE* file, int c){ int start; char *end_of_parabuf; WORD *end_of_word; end_of_parabuf = ¶buf[MAXCHARS]; end_of_word = &word[MAXWORDS - 2]; do { word_limit->text = wptr; if (word_limit == end_of_word) { set_other_indent (true); flush_paragraph (); } word_limit++; } while (c != '\n' && c != EOF); return 1; } static _Bool get_paragraph(FILE* file){ int c; //word_lomit = word; c = get_line (file, c); return true; } static void fmt(FILE* file){ while (get_paragraph (file)) { // fmt_paragraph (); // put_paragraph (word_limit); } } int main(){ FILE* instream; __CPROVER_assume(instream != NULL); fmt (instream); assert(0); return 1; }