1 /*
2  *  io.c -- input/output routines
3  *
4  */
5 
6 /*   to do for new operator stuff:
7  *
8  * 5.  optimize seq_to_term?
9  * 8.  can protect cl when in list with parens, but output does not get parens.
10  * 10. -3 should be a number, -(3) should not.  Same for unary +.
11  * 11. Check arity problem?
12  * 12. check set_variables?
13  *
14  */
15 
16 #include "header.h"
17 
18 #define SYM_TAB_SIZE   50
19 #define MAX_COMPLEX  1000  /* number of operators/terms */
20 
21 /* Include the following if ' should be a a quote character (like ").
22    Otter has had that behavior since the beginning.  But I am changing it
23    today, on Feb 19, 2004, making ' a SYM_SYM.  To revert to the old
24    behavior, include the following. */
25 
26 /* #define SINGLE_QUOTE */
27 
28 /* Following structure is to store data on symbol that might be special op. */
29 
30 struct sequence_member {
31   struct term *t;
32   short  binary_type;
33   short  binary_prec;
34   short  unary_type;
35   short  unary_prec;
36 };
37 
38 static struct sym_ent *Sym_tab[SYM_TAB_SIZE];  /* Symbol Table */
39 
40 /*************
41  *
42  *    int str_double(string, double_ptr) -- Translate a string to a double.
43  *
44  *    Return(1) iff success.
45  *
46  *************/
47 
str_double(char * s,double * dp)48 int str_double(char *s,
49 	       double *dp)
50 {
51   char *end;
52   double d;
53 
54   if (*s != '\"')
55     return(0);
56   else if (*(s+1) == '\"')
57     return(0);
58   else {
59     d = strtod(s+1, &end);
60     *dp = d;
61     return (*end == '\"');
62   }
63 }  /* str_double */
64 
65 /*************
66  *
67  *    double_str(double, str) -- translate a double to a string
68  *
69  *    Like sprintf, except that format is built in and string is
70  *    surrouded by double quotes.
71  *
72  *************/
73 
double_str(double d,char * s)74 void double_str(double d,
75 		char *s)
76 {
77   int i, n;
78 
79   sprintf(s, Float_format, d);
80 
81   n = strlen(s);
82   for (i=n; i>0; i--)
83     s[i] = s[i-1];
84   s[0] = '\"';
85   s[n+1] = '\"';
86   s[n+2] = '\0';
87 
88 }  /* double_str */
89 
90 /*************
91  *
92  *    int str_int(string, ilist) -- Translate a string to an integer.
93  *
94  *        String has optional '+' or '-' as first character.
95  *    Return(1) iff success.
96  *
97  *************/
98 
str_int(char * s,int * np)99 int str_int(char *s,
100 	    int *np)
101 {
102   int i, sign, n;
103 
104   i = 0;
105   sign = 1;
106   if (s[0] == '+' || s[0] == '-') {
107     if (s[0] == '-')
108       sign = -1;
109     i = 1;
110   }
111   if (s[i] == '\0')
112     return(0);
113   else {
114     n = 0;
115     for( ; s[i] >= '0' && s[i] <= '9'; i++)
116       n = n * 10 + s[i] - '0';
117     *np = n * sign;
118     return(s[i] == '\0');
119   }
120 }  /* str_int */
121 
122 /*************
123  *
124  *    int_str(int, str) -- translate an integer to a string
125  *
126  *************/
127 
int_str(int i,char * s)128 void int_str(int i,
129 	     char *s)
130 {
131   int j, sign;
132 
133   if ((sign = i) < 0)
134     i = -i;
135 
136   j = 0;
137   if (i == 0)
138     s[j++] = '0';
139   else {
140     while (i > 0) {
141       s[j++] = i % 10 + '0';
142       i = i / 10;
143     }
144   }
145   if (sign < 0)
146     s[j++] = '-';
147   s[j] = '\0';
148   reverse(s);
149 }  /* int_str */
150 
151 /*************
152  *
153  *    int str_long(string, long_ptr) -- Translate a string to a long.
154  *
155  *        String has optional '+' or '-' as first character.
156  *    Return(1) iff success.
157  *
158  *************/
159 
str_long(char * s,long int * np)160 int str_long(char *s,
161 	     long int *np)
162 {
163   int i, sign;
164   long n;
165 
166   i = 0;
167   sign = 1;
168   if (s[0] == '+' || s[0] == '-') {
169     if (s[0] == '-')
170       sign = -1;
171     i = 1;
172   }
173   if (s[i] == '\0')
174     return(0);
175   else {
176     n = 0;
177     for( ; s[i] >= '0' && s[i] <= '9'; i++)
178       n = n * 10 + s[i] - '0';
179     *np = n * sign;
180     return(s[i] == '\0');
181   }
182 }  /* str_long */
183 
184 /*************
185  *
186  *    int bits_ulong(string, long_ptr) -- Translate a string to a long.
187  *
188  *    String must consist only of 0's and 1's.
189  *
190  *    Return(1) iff success.
191  *
192  *************/
193 
bits_ulong(char * s,long unsigned int * np)194 int bits_ulong(char *s,
195 	       long unsigned int *np)
196 {
197   int i;
198   unsigned long n;
199 
200   n = 0;
201   for(i = 0 ; s[i] == '0' || s[i] == '1'; i++)
202     n = n * 2 + s[i] - '0';
203   *np = n;
204   return(s[i] == '\0');
205 }  /* bits_ulong */
206 
207 /*************
208  *
209  *    long_str(int, str) -- translate a long to a string
210  *
211  *************/
212 
long_str(long int i,char * s)213 void long_str(long int i,
214 	      char *s)
215 {
216   int j;
217   long signd;
218 
219   if ((signd = i) < 0)
220     i = -i;
221 
222   j = 0;
223   if (i == 0)
224     s[j++] = '0';
225   else {
226     while (i > 0) {
227       s[j++] = i % 10 + '0';
228       i = i / 10;
229     }
230   }
231   if (signd < 0)
232     s[j++] = '-';
233   s[j] = '\0';
234   reverse(s);
235 }  /* long_str */
236 
237 /*************
238  *
239  *    ulong_bits(int, str) -- translate a long to a base-2 string.
240  *
241  *************/
242 
ulong_bits(long unsigned int i,char * s)243 void ulong_bits(long unsigned int i,
244 		char *s)
245 {
246   unsigned long j;
247   int n, k;
248 
249   /* Set n to the number of places we'll use. */
250   /* First ignore leading 0's, then increase if necessary. */
251   for (j = i, n = 0; j > 0; j = j >> 1, n++);
252   n = (n < Parms[MIN_BIT_WIDTH].val ? Parms[MIN_BIT_WIDTH].val : n);
253   /* build the string */
254   for (k = 0; k < n; k++)
255     s[k] = '0' + ((i >> (n-(k+1))) & 1);
256   s[n] = '\0';
257 }  /* ulong_bits */
258 
259 /*************
260  *
261  *    cat_str(s1, s2, s3)
262  *
263  *************/
264 
cat_str(char * s1,char * s2,char * s3)265 void cat_str(char *s1,
266 	     char *s2,
267 	     char *s3)
268 {
269   int i, j;
270 
271   for (i = 0; s1[i] != '\0'; i++)
272     s3[i] = s1[i];
273   for (j = 0; s2[j] != '\0'; j++, i++)
274     s3[i] = s2[j];
275   s3[i] = '\0';
276 }  /* cat_str */
277 
278 /*************
279  *
280  *     int str_ident(s, t) --  Identity of strings
281  *
282  *************/
283 
str_ident(char * s,char * t)284 int str_ident(char *s,
285 	      char *t)
286 {
287   for ( ; *s == *t; s++, t++)
288     if (*s == '\0') return(1);
289   return(0);
290 }  /* str_ident */
291 
292 /*************
293  *
294  *    reverse(s) -- reverse a string
295  *
296  *************/
297 
reverse(char * s)298 void reverse(char *s)
299 {
300   int i, j;
301   char temp;
302 
303   for (i = 0, j = strlen(s)-1; i<j; i++, j--) {
304     temp = s[i];
305     s[i] = s[j];
306     s[j] = temp;
307   }
308 }  /* reverse */
309 
310 /*************
311  *
312  *    struct sym_ent *insert_sym(string, arity)
313  *
314  *    Insert string/arity into the symbol table and return the symbol
315  *    table node.  Do not check if string/arity is already there.
316  *
317  *************/
318 
insert_sym(char * s,int arity)319 struct sym_ent *insert_sym(char *s,
320 			   int arity)
321 {
322   struct sym_ent *p;
323   int i;
324 
325   p = get_sym_ent();
326   strcpy(p->name, s);
327   p->arity = arity;
328   p->lex_val = (2 * Parms[NEW_SYMBOL_LEX_POSITION].val) - 1;
329   p->sym_num = new_sym_num();
330   i = p->sym_num % SYM_TAB_SIZE;
331   p->next = Sym_tab[i];
332   Sym_tab[i] = p;
333   return(p);
334 }  /* insert_sym */
335 
336 /*************
337  *
338  *    int str_to_sn(str, arity) -- Return a symbol number for string/arity.
339  *
340  *        If the given string/arity is already in the global symbol table,
341  *    then return symbol number; else, create a new symbol table entry and
342  *    return a new symbol number
343  *
344  *************/
345 
str_to_sn(char * str,int arity)346 int str_to_sn(char *str,
347 	      int arity)
348 {
349   struct sym_ent *p, *save;
350   int i;
351   long dummy;
352 
353   save = NULL;
354   for (i = 0; i < SYM_TAB_SIZE; i++) {
355     p = Sym_tab[i];
356     while (p != NULL) {
357       if (!str_ident(str, p->name))
358 	p = p->next;
359       else if (p->arity != arity) {
360 	save = p;
361 	p = p->next;
362       }
363       else {
364 	if (p->eval_code != 0)
365 	  /* recall that evaluable symbols are inserted in init */
366 	  Internal_flags[DOLLAR_PRESENT] = 1;
367 	return(p->sym_num);
368       }
369     }
370   }
371 
372   if (save && !save->special_op &&
373       Flags[CHECK_ARITY].val &&
374       Internal_flags[REALLY_CHECK_ARITY] &&
375       !str_ident(str, "$Quantified") &&
376       !str_ident(str, "$Hyps") &&
377       !str_ident(str, "$Concs")    ) {
378 
379     fprintf(stderr, "%c\n\nWARNING, multiple arity: %s/%d, %s/%d.\n\n", Bell,
380 	    save->name, save->arity, str, arity);
381   }
382 
383   /* String/arity not in table, so create an entry. */
384 
385   p = insert_sym(str, arity);
386 
387   if (str[0] == '$' &&
388 
389       p->sym_num != Cons_sym_num &&  /* Lists */
390       p->sym_num != Nil_sym_num &&
391 
392       p->sym_num != Ignore_sym_num &&  /* Misc */
393       p->sym_num != Chr_sym_num &&
394       p->sym_num != Dots_sym_num &&
395       !initial_str("$Quantified", str) &&
396 
397       !initial_str("$ANS", str) &&  /* Answer literals */
398       !initial_str("$Ans", str) &&
399       !initial_str("$ans", str) &&
400 
401       !initial_str("$Connect", str) &&  /* mace2 connection relations */
402 
403       !str_ident(str, "$NUCLEUS") &&  /* Linked inference */
404       !str_ident(str, "$BOTH") &&
405       !str_ident(str, "$LINK") &&
406       !str_ident(str, "$SATELLITE") &&
407 
408       !str_ident(str, "$FSUB") &&     /* Hints */
409       !str_ident(str, "$BSUB") &&
410       !str_ident(str, "$EQUIV") &&
411 
412       !str_ident(str, "$Concs") &&    /* Sequent i/o */
413       !str_ident(str, "$Hyps") &&
414 
415       !skolem_symbol(p->sym_num) &&
416       !str_long(str+1, &dummy))            /* e.g.,  weight(f($3,a),-2) */
417 
418     fprintf(stderr, "%c\n\nWARNING, unrecognized $ symbol: %s.\n\n", Bell, str);
419 
420   return(p->sym_num);
421 
422 }  /* str_to_sn */
423 
424 /*************
425  *
426  *    print_syms(file_ptr) -- Display the symbol list.
427  *
428  *************/
429 
print_syms(FILE * fp)430 void print_syms(FILE *fp)
431 {
432   struct sym_ent *p;
433   int i;
434 
435   for (i = 0; i < SYM_TAB_SIZE; i++) {
436     p = Sym_tab[i];
437     while (p != NULL) {
438       fprintf(fp, "%d  %s/%d, lex_val=%d\n", p->sym_num, p->name, p->arity, p->lex_val);
439       p = p->next;
440     }
441   }
442 }  /* print_syms */
443 
444 /*************
445  *
446  *    p_syms()
447  *
448  *************/
449 
p_syms(void)450 void p_syms(void)
451 {
452   print_syms(stdout);
453 }  /* p_syms */
454 
455 /*************
456  *
457  *    char *sn_to_str(sym_num)  --  given a symbol number, return the name
458  *
459  *************/
460 
sn_to_str(int sym_num)461 char *sn_to_str(int sym_num)
462 {
463   struct sym_ent *p;
464 
465   p = Sym_tab[sym_num % SYM_TAB_SIZE];
466   while (p != NULL && p->sym_num != sym_num)
467     p = p->next;
468   if (p == NULL)
469     return("");
470   else
471     return(p->name);
472 }  /* sn_to_str */
473 
474 /*************
475  *
476  *    int sn_to_arity(sym_num)  --  given a symbol number, return the arity
477  *
478  *************/
479 
sn_to_arity(int sym_num)480 int sn_to_arity(int sym_num)
481 {
482   struct sym_ent *p;
483 
484   p = Sym_tab[sym_num % SYM_TAB_SIZE];
485   while (p != NULL && p->sym_num != sym_num)
486     p = p->next;
487   if (p == NULL)
488     return(-1);
489   else
490     return(p->arity);
491 }  /* sn_to_arity */
492 
493 /*************
494  *
495  *    int sn_to_node(sym_num)
496  *
497  *    Given a symbol number, return the symbol table node.
498  *
499  *************/
500 
sn_to_node(int sym_num)501 struct sym_ent *sn_to_node(int sym_num)
502 {
503   struct sym_ent *p;
504 
505   p = Sym_tab[sym_num % SYM_TAB_SIZE];
506   while (p != NULL && p->sym_num != sym_num)
507     p = p->next;
508   return(p);  /* possibly NULL */
509 }  /* sn_to_node */
510 
511 /*************
512  *
513  *    int sn_to_ec(sym_num)
514  *
515  *    Given a symbol number, return the evaluation code.
516  *
517  *************/
518 
sn_to_ec(int sym_num)519 int sn_to_ec(int sym_num)
520 {
521   struct sym_ent *p;
522 
523   p = Sym_tab[sym_num % SYM_TAB_SIZE];
524   while (p != NULL && p->sym_num != sym_num)
525     p = p->next;
526   if (p == NULL)
527     return(-1);
528   else
529     return(p->eval_code);
530 }  /* sn_to_ec */
531 
532 /*************
533  *
534  *    sym_tab_member(str, arity)
535  *
536  *    Similar to str_to_sn, but do not insert if not there,
537  *    and return node instead of sn.
538  *
539  *************/
540 
sym_tab_member(char * str,int arity)541 struct sym_ent *sym_tab_member(char *str,
542 			       int arity)
543 {
544   struct sym_ent *p;
545   int i;
546 
547   for (i = 0; i < SYM_TAB_SIZE; i++) {
548     p = Sym_tab[i];
549     while (p != NULL) {
550       if (!str_ident(str, p->name))
551 	p = p->next;
552       else if (p->arity != arity)
553 	p = p->next;
554       else
555 	return(p);
556     }
557   }
558   return((struct sym_ent *) NULL);
559 
560 }  /* sym_tab_member */
561 
562 /*************
563  *
564  *    int in_sym_tab(s)  --  is s in the symbol table?
565  *
566  *************/
567 
in_sym_tab(char * s)568 int in_sym_tab(char *s)
569 {
570   struct sym_ent *p;
571   int i;
572 
573   for (i = 0; i < SYM_TAB_SIZE; i++) {
574     p = Sym_tab[i];
575     while (p != NULL) {
576       if (str_ident(p->name, s))
577 	return(1);
578       p = p->next;
579     }
580   }
581   return(0);
582 }  /* in_sym_tab */
583 
584 /*************
585  *
586  *    free_sym_tab() -- free all symbols in the symbol table
587  *
588  *************/
589 
free_sym_tab(void)590 void free_sym_tab(void)
591 {
592   struct sym_ent *p1, *p2;
593   int i;
594 
595   for (i = 0; i < SYM_TAB_SIZE; i++) {
596     p1 = Sym_tab[i];
597     while (p1 != NULL) {
598       p2 = p1;
599       p1 = p1->next;
600       free_sym_ent(p2);
601     }
602     Sym_tab[i] = NULL;
603   }
604 }  /* free_sym_tab */
605 
606 /*************
607  *
608  *    int is_symbol(t, str, arity)
609  *
610  *    Does t have leading function symbol str with arity?
611  *
612  *************/
613 
is_symbol(struct term * t,char * str,int arity)614 int is_symbol(struct term *t,
615 	      char *str,
616 	      int arity)
617 {
618   return((t->type == COMPLEX || t->type == NAME) &&
619 	 sn_to_arity(t->sym_num) == arity &&
620 	 str_ident(sn_to_str(t->sym_num), str));
621 }  /* is_symbol */
622 
623 /*************
624  *
625  *    mark_as_skolem(sym_num)
626  *
627  *************/
628 
mark_as_skolem(int sym_num)629 void mark_as_skolem(int sym_num)
630 {
631   struct sym_ent *se;
632 
633   se = sn_to_node(sym_num);
634 
635   if (!se) {
636     char s[500];
637     sprintf(s, "mark_as_skolem, no symbol for %d.", sym_num);
638     abend(s);
639   }
640   else
641     se->skolem = 1;
642 }  /* mark_as_skolem */
643 
644 /*************
645  *
646  *    int is_skolem(sym_num)
647  *
648  *************/
649 
is_skolem(int sym_num)650 int is_skolem(int sym_num)
651 {
652   struct sym_ent *se;
653 
654   se = sn_to_node(sym_num);
655 
656   if (!se) {
657     char s[500];
658     sprintf(s, "is_skolem, no symbol for %d.", sym_num);
659     abend(s);
660     return(0);  /* to quiet lint */
661   }
662   else
663     return(se->skolem);
664 }  /* is_skolem */
665 
666 /*************
667  *
668  *     int initial_str(s, t)  --  Is s an initial substring of t?
669  *
670  *************/
671 
initial_str(char * s,char * t)672 int initial_str(char *s,
673 		char *t)
674 {
675   for ( ; *s == *t; s++, t++)
676     if (*s == '\0') return(1);
677   return(*s == '\0');
678 }  /* initial_str */
679 
680 /*************
681  *
682  *    int set_vars(term)
683  *
684  *        Decide which of the names are really variables, and make
685  *    into variables.  (This routine is used only on input terms.)
686  *    Preserve the user's variable names by keeping the pointer into
687  *    the symbol list.
688  *
689  *    If too many variables, return(0); elase return(1).
690  *
691  *************/
692 
set_vars(struct term * t)693 int set_vars(struct term *t)
694 {
695   char *varnames[MAX_VARS];
696   int i;
697 
698   for (i=0; i<MAX_VARS; i++)
699     varnames[i] = NULL;
700 
701   return(set_vars_term(t, varnames));
702 }  /* set_vars */
703 
704 /*************
705  *
706  *     int set_vars_term(term, varnames)
707  *
708  *************/
709 
set_vars_term(struct term * t,char ** varnames)710 int set_vars_term(struct term *t,
711 		  char **varnames)
712 {
713   struct rel *r;
714   int i, rc;
715 
716   if (t->type == COMPLEX) {
717     r = t->farg;
718     rc = 1;
719     while (rc && r != NULL) {
720       rc = set_vars_term(r->argval, varnames);
721       r = r->narg;
722     }
723     return(rc);
724   }
725   else if (var_name(sn_to_str(t->sym_num)) == 0)
726     return(1);
727   else {
728     i = 0;
729     t->type = VARIABLE;
730     while (i < MAX_VARS && varnames[i] != NULL &&
731 	   varnames[i] != sn_to_str(t->sym_num))
732       i++;
733     if (i == MAX_VARS)
734       return(0);
735     else {
736       if (varnames[i] == NULL)
737 	varnames[i] = sn_to_str(t->sym_num);
738       t->varnum = i;
739       return(1);
740       /* t->sym_num = 0;  include this to destroy input variable names */
741     }
742   }
743 }  /* set_vars_term */
744 
745 /*************
746  *
747  *    int var_name(string) -- Decide if a string represents a variable.
748  *
749  *        return("string is a variable")
750  *
751  *************/
752 
var_name(char * s)753 int var_name(char *s)
754 {
755   if (Flags[PROLOG_STYLE_VARIABLES].val)
756     return((*s >= 'A' && *s <= 'Z') || *s == '_');
757   else
758     return(*s >= 'u' && *s <= 'z');
759 }  /* var_name */
760 
761 /*************
762  *
763  *    struct term *read_list(file_ptr, errors_ptr, integrate)
764  *
765  *    Read and return a list of terms.
766  *
767  *    The list must be terminated either with the term `end_of_list.'
768  *    or with an actual EOF.
769  *    Set errors_ptr to point to the number of errors found.
770  *
771  *************/
772 
read_list(FILE * fp,int * ep,int integrate)773 struct term_ptr *read_list(FILE *fp,
774 			   int *ep,
775 			   int integrate)
776 {
777   struct term_ptr *p1, *p2, *p3;
778   struct term *t;
779   int rc;
780 
781   *ep = 0;
782   p3 = NULL;
783   p2 = NULL;
784   t = read_term(fp, &rc);
785   while (rc == 0) {
786     (*ep)++;
787     t = read_term(fp, &rc);
788   }
789 
790   /* keep going until t == NULL || t is end marker */
791 
792   while (t != NULL && (t->type != NAME ||
793 		       str_ident(sn_to_str(t->sym_num), "end_of_list") == 0)) {
794     if (integrate)
795       t = integrate_term(t);
796     p1 = get_term_ptr();
797     p1->term = t;
798     if (p2 == NULL)
799       p3 = p1;
800     else
801       p2->next = p1;
802     p2 = p1;
803     t = read_term(fp, &rc);
804     while (rc == 0) {
805       (*ep)++;
806       t = read_term(fp, &rc);
807     }
808   }
809   if (t == NULL)
810     return(p3);
811   else {
812     zap_term(t);
813     return(p3);
814   }
815 }  /* read_list */
816 
817 /*************
818  *
819  *    print_list(file_ptr, term_ptr) -- Print a list of terms.
820  *
821  *        The list is printed with periods after each term, and
822  *    the list is terminated with `end_of_list.' so that it can
823  *    be read with read_list.
824  *
825  *************/
826 
print_list(FILE * fp,struct term_ptr * p)827 void print_list(FILE *fp,
828 		struct term_ptr *p)
829 {
830   while (p != NULL) {
831     print_term(fp, p->term); fprintf(fp, ".\n");
832     p = p->next;
833   }
834   fprintf(fp, "end_of_list.\n");
835 }  /* print_list */
836 
837 /*************
838  *
839  *    bird_print(fp, t)
840  *
841  *************/
842 
bird_print(FILE * fp,struct term * t)843 void bird_print(FILE *fp,
844 		struct term *t)
845 {
846   struct rel *r;
847 
848   if (t == NULL)
849     fprintf(fp, "(nil)");
850   else if (!is_symbol(t, "a", 2)) {
851     /* t is not of the form a(_,_), so print in prefix */
852     if (t->type == NAME)            /* name */
853       fprintf(fp, "%s", sn_to_str(t->sym_num));
854     else if (t->type == VARIABLE)               /* variable */
855       print_variable(fp, t);
856     else {  /* complex */
857       fprintf(fp, "%s", sn_to_str(t->sym_num));
858       fprintf(fp, "(");
859       r = t->farg;
860       while(r != NULL) {
861 	bird_print(fp, r->argval);
862 	r = r->narg;
863 	if(r != NULL)
864 	  fprintf(fp, ",");
865       }
866       fprintf(fp, ")");
867     }
868   }
869   else {  /* t has form a(_,_), so print in bird notation */
870     if (is_symbol(t->farg->narg->argval, "a", 2)) {
871       bird_print(fp, t->farg->argval);
872       fprintf(fp, " (");
873       bird_print(fp, t->farg->narg->argval);
874       fprintf(fp, ")");
875     }
876     else {
877       bird_print(fp, t->farg->argval);
878       fprintf(fp, " ");
879       bird_print(fp, t->farg->narg->argval);
880     }
881   }
882 }  /* bird_print */
883 
884 /****************************************
885 
886 write_term outputs a term in readable format (w.r.t. infix, prefix,
887 and postfix operators) and without extra parentheses.  It it much
888 complicated by one feature: deciding where to omit space around
889 the special operators.  For example, just as we can input a+b+c
890 instead of a + b + c, we wish to output without spaces were possible.
891 (I'm sorry the code is so complicated---I couldn't see a simpler way
892 of doing it.)
893 
894 There are 2 types of constant/operator/functor:
895 
896     NAME_SYM: string of alphanumerics, $, and _.  Also quoted string.
897     SYM_SYM:  string of *+-/\^<>=`~:?@&!;# and sometimes | (if not in list)
898 
899 For completeness, the other characters are
900     ,()[]{} and sometimes | (if in list)   puctuation for building terms
901     .                                      end of input term
902     %                                      start of comment
903     "'                                     for quoted strings
904 
905 For this problem, tokens are of 4 types:
906     NAME_SYM
907     SYM_SYM
908     OPEN_PAREN  '('
909     OTHER_PUNC   other punctuation (including space)
910 
911 Special ops that are NAME_SYMs are always surrounded by spaces.
912 
913 Here are the space rules for SYM_SYM special ops:
914 
915     infix
916         omit space before if preceding token is NAME_SYM or OTHER_PUNC
917         omit space after if next token is is NAME_SYM or OTHER_PUNC
918               (note that space is included if next is '(')
919 
920     prefix
921         omit space before if preceding token is OTHER_PUNC
922         omit space after if next token is is NAME_SYM or OTHER_PUNC
923 
924     postfix
925         omit space before if preceding token is NAME_SYM or OTHER_PUNC
926         always include space after (could omit if next token is OTHER_PUNC,
927             but current mechanism won't handle that, and it's not
928             that important)
929 
930 *****************************************/
931 
932 /* Token types */
933 
934 #define OPEN_PAREN  1
935 #define OTHER_PUNC  2
936 #define NAME_SYM    6
937 #define SYM_SYM     7
938 
939 /*************
940  *
941  *    int next_token_type(t, n)
942  *
943  *    Find the next token type that would be output for t.
944  *    n is precedence parameter as in write term.
945  *
946  *************/
947 
next_token_type(struct term * t,int n)948 static int next_token_type(struct term *t,
949 			   int n)
950 {
951   struct sym_ent *s;
952   int na1;
953   char *str;
954 
955   str = sn_to_str(t->sym_num);
956   if (t->type == NAME) {
957     if (str_ident(str, "$nil"))
958       return(OTHER_PUNC);
959     else
960       return(name_sym(str) ? NAME_SYM : SYM_SYM);
961   }
962   else if (t->type == VARIABLE) {
963     if (t->sym_num == 0)
964       return(NAME_SYM);
965     else
966       return(name_sym(str) ? NAME_SYM : SYM_SYM);
967   }
968   else {  /* complex */
969     if (t->sym_num == str_to_sn("$cons", 2))
970       return(OTHER_PUNC);
971     else if (str_ident(sn_to_str(t->sym_num), "$Quantified")) {
972       /* parens if parent is special op */
973       if (n < 1000)
974 	return(OPEN_PAREN);
975       else
976 	return(next_token_type(t->farg->argval, 0));
977     }
978     else {
979       s = sn_to_node(t->sym_num);
980       if (s->special_op && s->arity == 2) {
981 	na1 = s->op_prec;
982 	if (s->op_type == XFX || s->op_type == XFY)
983 	  na1--;
984 	if (s->op_prec > n)
985 	  return(OPEN_PAREN);
986 	else
987 	  return(next_token_type(t->farg->argval, na1));
988       }
989       else if (s->special_op && s->arity == 1) {
990 	na1 = s->op_prec;
991 	if (s->op_type == FX || s->op_type == XF)
992 	  na1--;
993 
994 	if (s->op_prec > n)
995 	  return(OPEN_PAREN);
996 	if (s->op_type == FX || s->op_type == FY)
997 	  return(name_sym(str) ? NAME_SYM : SYM_SYM);
998 	else
999 	  return(next_token_type(t->farg->argval, na1));
1000       }
1001       else
1002 	return(name_sym(str) ? NAME_SYM : SYM_SYM);
1003     }
1004   }
1005 }  /* next_token_type */
1006 
1007 /*************
1008  *
1009  *    write_term(file_ptr, term, n, prev) -- print in readable form.
1010  *
1011  *************/
1012 
write_term(FILE * fp,struct term * t,int n,int * prev)1013 void write_term(FILE *fp,
1014 		struct term *t,
1015 		int n,
1016 		int *prev)
1017 {
1018   struct rel *r;
1019   struct term *t1;
1020   struct sym_ent *s;
1021   int na1, na2, next;
1022   char *str, *s1, *s2;
1023 
1024   if (t == NULL) {
1025     fprintf(fp, "<write_term gets NULL pointer>");
1026     return;
1027   }
1028 
1029   if (t->type == NAME) {
1030     str = sn_to_str(t->sym_num);
1031     if (str_ident(str, "$nil"))
1032       { fprintf(fp, "[]"); *prev = OTHER_PUNC;}
1033     else {
1034       fprintf(fp, "%s", str);
1035       *prev = (name_sym(str) ? NAME_SYM : SYM_SYM);
1036     }
1037   }
1038 
1039   else if (t->type == VARIABLE) {
1040     print_variable(fp, t);
1041     if (t->sym_num == 0)
1042       *prev = NAME_SYM;
1043     else
1044       *prev = (name_sym(sn_to_str(t->sym_num)) ? NAME_SYM : SYM_SYM);
1045   }
1046 
1047   else {  /* complex */
1048     str = sn_to_str(t->sym_num);
1049 
1050     if (str_ident(str, "$Quantified")) {  /* Quantified Formula */
1051       /* parens if parent is special op */
1052       if (n < 1000) {
1053 	fprintf(fp, "("); *prev = OPEN_PAREN;
1054       }
1055       for (r = t->farg; r; r = r->narg) {
1056 	/* parens if special op in child */
1057 	write_term(fp, r->argval, 0, prev);
1058 	if (r->narg) {
1059 	  fprintf(fp, " "); *prev = OTHER_PUNC;
1060 	}
1061       }
1062       if (n < 1000) {
1063 	fprintf(fp, ")"); *prev = OTHER_PUNC;
1064       }
1065     }   /* end Formula */
1066 
1067     else if (is_symbol(t, "$cons", 2)) {
1068       fprintf(fp, "["); *prev = OTHER_PUNC;
1069       write_term(fp, t->farg->argval, 1000, prev);
1070       t1 = t->farg->narg->argval;
1071       while (t1->sym_num == str_to_sn("$cons", 2)) {
1072 	fprintf(fp, ","); *prev = OTHER_PUNC;
1073 	write_term(fp, t1->farg->argval, 1000, prev);
1074 	t1 = t1->farg->narg->argval;
1075       }
1076       if (t1->sym_num == str_to_sn("$nil", 0)) {
1077 	fprintf(fp, "]"); *prev = OTHER_PUNC;
1078       }
1079       else {
1080 	fprintf(fp, "|"); *prev = OTHER_PUNC;
1081 	write_term(fp, t1, 1000, prev);
1082 	fprintf(fp, "]"); *prev = OTHER_PUNC;
1083       }
1084     }   /* end list */
1085     else if (Flags[BIRD_PRINT].val &&is_symbol(t, "a", 2))
1086       bird_print(fp, t);
1087 
1088     else {
1089       s = sn_to_node(t->sym_num);
1090 
1091       if (s->special_op && s->arity == 2) {  /* infix */
1092 	na1 = na2 = s->op_prec;
1093 	if (s->op_type == XFX || s->op_type == XFY)
1094 	  na1--;
1095 	if (s->op_type == XFX || s->op_type == YFX)
1096 	  na2--;
1097 	if (s->op_prec > n) {
1098 	  fprintf(fp, "("); *prev = OPEN_PAREN;
1099 	}
1100 	write_term(fp, t->farg->argval, na1, prev);
1101 
1102 	/* Decide on spaces around infix op. */
1103 
1104 	if (name_sym(str))
1105 	  s1 = s2 = " ";
1106 	else {
1107 	  if (*prev == OTHER_PUNC || *prev == NAME_SYM)
1108 	    s1 = "";
1109 	  else
1110 	    s1 = " ";
1111 	  next = next_token_type(t->farg->narg->argval, na2);
1112 	  if (next == OTHER_PUNC || next == NAME_SYM)
1113 	    s2 = "";
1114 	  else
1115 	    s2 = " ";
1116 	}
1117 
1118 	fprintf(fp, "%s%s%s", s1,str,s2);
1119 	if (str_ident(s2, " "))
1120 	  *prev = OTHER_PUNC;
1121 	else
1122 	  *prev = (name_sym(str) ? NAME_SYM : SYM_SYM);
1123 	write_term(fp, t->farg->narg->argval, na2, prev);
1124 	if (s->op_prec > n) {
1125 	  fprintf(fp, ")"); *prev = OTHER_PUNC;
1126 	}
1127       }
1128 
1129       else if (s->special_op && s->arity == 1) {  /* prefix,postfix */
1130 	na1 = s->op_prec;
1131 	if (s->op_type == FX || s->op_type == XF)
1132 	  na1--;
1133 
1134 	if (s->op_prec > n) {
1135 	  fprintf(fp, "("); *prev = OPEN_PAREN;
1136 	}
1137 
1138 	if (s->op_type == FX || s->op_type == FY) {
1139 
1140 	  /* Decide on spaces around special prefix op. */
1141 
1142 	  if (name_sym(str))
1143 	    s1 = s2 = " ";
1144 	  else {
1145 	    if (*prev == OTHER_PUNC || *prev == OPEN_PAREN)
1146 	      s1 = "";
1147 	    else
1148 	      s1 = " ";
1149 	    next = next_token_type(t->farg->argval, na1);
1150 	    if (next == OTHER_PUNC || next == OPEN_PAREN || next == NAME_SYM)
1151 	      s2 = "";
1152 	    else
1153 	      s2 = " ";
1154 	  }
1155 
1156 	  fprintf(fp, "%s%s%s", s1,str,s2);
1157 	  if (str_ident(s2, " "))
1158 	    *prev = OTHER_PUNC;
1159 	  else
1160 	    *prev = (name_sym(str) ? NAME_SYM : SYM_SYM);
1161 	  write_term(fp, t->farg->argval, na1, prev);
1162 	}
1163 	else {
1164 	  write_term(fp, t->farg->argval, na1, prev);
1165 
1166 	  /* Decide on spaces around special postfix op. */
1167 
1168 	  if (name_sym(str))
1169 	    s1 = s2 = " ";
1170 	  else {
1171 	    if (*prev == OTHER_PUNC || *prev == NAME_SYM)
1172 	      s1 = "";
1173 	    else
1174 	      s1 = " ";
1175 	    /* Can't easily tell next token, so just output space. */
1176 	    s2 = " ";
1177 	  }
1178 
1179 	  fprintf(fp, "%s%s%s", s1,str,s2);
1180 	  *prev = OTHER_PUNC;
1181 	}
1182 
1183 	if (s->op_prec > n) {
1184 	  fprintf(fp, ")"); *prev = OTHER_PUNC;
1185 	}
1186       }
1187 
1188       else {  /* functor(args) */
1189 	fprintf(fp, "%s", str);
1190 	fprintf(fp, "("); *prev = OPEN_PAREN;
1191 	r = t->farg;
1192 	while(r != NULL) {
1193 	  write_term(fp, r->argval, 1000, prev);
1194 	  r = r->narg;
1195 	  if(r != NULL) {
1196 	    fprintf(fp, ","); *prev = OTHER_PUNC;
1197 	  }
1198 	}
1199 	fprintf(fp, ")"); *prev = OTHER_PUNC;
1200       }
1201     }
1202   }
1203 }  /* write_term */
1204 
1205 /*************
1206  *
1207  *    display_term(file_ptr, term)  --  Display a term in internal form.
1208  *
1209  *************/
1210 
display_term(FILE * fp,struct term * t)1211 void display_term(FILE *fp,
1212 		  struct term *t)
1213 {
1214   struct rel *r;
1215 
1216   if (t == NULL)
1217     fprintf(fp, "<display_term gets NULL pointer>");
1218   else if (t->type == NAME) {
1219     fprintf(fp, "%s", sn_to_str(t->sym_num));
1220   }
1221   else if (t->type == VARIABLE)
1222     print_variable(fp, t);
1223   else {  /* complex */
1224     fprintf(fp, "%s", sn_to_str(t->sym_num));
1225     fprintf(fp, "(");
1226     r = t->farg;
1227     while(r != NULL) {
1228       display_term(fp, r->argval);
1229       r = r->narg;
1230       if(r != NULL)
1231 	fprintf(fp, ",");
1232     }
1233     fprintf(fp, ")");
1234   }
1235 }  /* display_term */
1236 
1237 /*************
1238  *
1239  *    print_term(file_ptr, term)  --  Print a term to a file.
1240  *
1241  *    Flag determines write_term vs. display_term.
1242  *
1243  *************/
1244 
print_term(FILE * fp,struct term * t)1245 void print_term(FILE *fp,
1246 		struct term *t)
1247 {
1248   int i;
1249 
1250   if (Flags[DISPLAY_TERMS].val)
1251     display_term(fp, t);
1252   else {
1253     i = OTHER_PUNC;  /* Assume previous token is punctuation. */
1254     write_term(fp, t, 1000, &i);
1255   }
1256 }  /* print_term */
1257 
1258 /*************
1259  *
1260  *    p_term(term)  --  print_term and \n to the standard output.
1261  *
1262  *************/
1263 
p_term(struct term * t)1264 void p_term(struct term *t)
1265 {
1266   print_term(stdout, t);
1267   printf("\n");
1268   fflush(stdout);
1269 }  /* p_term */
1270 
1271 /*************
1272  *
1273  *    d_term(term)  --  display_term and \n to the standard output.
1274  *
1275  *************/
1276 
d_term(struct term * t)1277 void d_term(struct term *t)
1278 {
1279   display_term(stdout, t);
1280   printf("\n");
1281   fflush(stdout);
1282 }  /* p_term */
1283 
1284 /*************
1285  *
1286  *    print_term_nl(fp, term)  --  print_term followed by period and newline
1287  *
1288  *************/
1289 
print_term_nl(FILE * fp,struct term * t)1290 void print_term_nl(FILE *fp,
1291 		   struct term *t)
1292 {
1293   print_term(fp, t);
1294   fprintf(fp,".\n");
1295 }  /* print_term_nl */
1296 
1297 /*************
1298  *
1299  *   int print_term_length(t)
1300  *
1301  *************/
1302 
print_term_length(struct term * t)1303 int print_term_length(struct term *t)
1304 {
1305   static FILE *tfp = NULL;
1306   int i;
1307   char s[MAX_BUF];
1308 
1309   if (!tfp)
1310     tfp = tmpfile();
1311 
1312   rewind(tfp);
1313   print_term(tfp, t);
1314   fprintf(tfp, "%c", '\0');  /* end marker */
1315   fflush(tfp);
1316   rewind(tfp);
1317 
1318   for (i = 0, s[i]=getc(tfp); s[i] && i < MAX_BUF; s[++i]=getc(tfp));
1319 
1320 #if 0
1321   printf("%d: ", i); print_term(stdout, t);
1322 #endif
1323 
1324   return(i == MAX_BUF ? MAX_INT : i);
1325 
1326 }  /* print_term_length */
1327 
1328 /*************
1329  *
1330  *   pretty_print_term(fp, t, indents)
1331  *
1332  *************/
1333 
pretty_print_term(FILE * fp,struct term * t,int indents)1334 void  pretty_print_term(FILE *fp,
1335 			struct term *t,
1336 			int indents)
1337 {
1338   int len, spaces_before_term, i;
1339 
1340   spaces_before_term = indents * Parms[PRETTY_PRINT_INDENT].val;
1341 
1342   for (i=0; i<spaces_before_term; i++)
1343     fprintf(fp, " ");
1344 
1345   if (t->type != COMPLEX)
1346     print_term(fp, t);
1347   else {
1348 
1349     len = print_term_length(t);
1350 
1351     if (spaces_before_term + len < 80)
1352       print_term(fp, t);
1353     else {
1354       struct rel *r;
1355 
1356       fprintf(fp, "%s", sn_to_str(t->sym_num));
1357       fprintf(fp, "(\n");
1358       r = t->farg;
1359       while(r) {
1360 	pretty_print_term(fp, r->argval, indents+1);
1361 	r = r->narg;
1362 	if(r != NULL)
1363 	  fprintf(fp, ",");
1364 	fprintf(fp, "\n");
1365       }
1366       for (i=0; i<spaces_before_term; i++)
1367 	fprintf(fp, " ");
1368       fprintf(fp, ")");
1369     }
1370   }
1371 }  /* pretty_print_term */
1372 
1373 /*************
1374  *
1375  *   print_variable(fp, variable)
1376  *
1377  *************/
1378 
print_variable(FILE * fp,struct term * t)1379 void print_variable(FILE *fp,
1380 		    struct term *t)
1381 {
1382   int i;
1383 
1384   if (t->sym_num != 0)
1385     fprintf(fp, "%s", sn_to_str(t->sym_num));
1386   else if (Flags[PROLOG_STYLE_VARIABLES].val) {
1387     fprintf(fp, "%c", (t->varnum % 26) + 'A');
1388     i = t->varnum / 26;
1389     if (i > 0)
1390       fprintf(fp, "%d", i);
1391   }
1392   else {
1393     if (t->varnum <= 2)
1394       fprintf(fp, "%c", 'x'+t->varnum);
1395     else if (t->varnum <= 5)
1396       fprintf(fp, "%c", 'r'+t->varnum);
1397     else
1398       fprintf(fp, "%c%d", 'v', t->varnum);
1399   }
1400 }  /* print_variable */
1401 
1402 /*************
1403  *
1404  *    void built_in_symbols()
1405  *
1406  *    note: in a similar way, user-defined evaluable functions are declared
1407  *    in `declare_user_functions'.
1408  *
1409  *************/
1410 
built_in_symbols(void)1411 void built_in_symbols(void)
1412 {
1413   struct sym_ent *p;
1414 
1415   p = insert_sym("$cons", 2); Cons_sym_num = p->sym_num;
1416   p = insert_sym("$nil", 0);  Nil_sym_num = p->sym_num;
1417   p = insert_sym("$IGNORE", 1); Ignore_sym_num = p->sym_num;
1418   p = insert_sym("$CHR", 1); Chr_sym_num = p->sym_num;
1419   p = insert_sym("$dots", 1); Dots_sym_num = p->sym_num;
1420   p = insert_sym("$", 1);
1421 
1422   p = insert_sym("$SUM", 2);  p->eval_code = SUM_SYM;
1423   p = insert_sym("$PROD", 2); p->eval_code = PROD_SYM;
1424   p = insert_sym("$DIFF", 2); p->eval_code = DIFF_SYM;
1425   p = insert_sym("$DIV", 2);  p->eval_code = DIV_SYM;
1426   p = insert_sym("$MOD", 2);  p->eval_code = MOD_SYM;
1427 
1428   p = insert_sym("$EQ", 2);   p->eval_code = EQ_SYM;
1429   p = insert_sym("$NE", 2);   p->eval_code = NE_SYM;
1430   p = insert_sym("$LT", 2);   p->eval_code = LT_SYM;
1431   p = insert_sym("$LE", 2);   p->eval_code = LE_SYM;
1432   p = insert_sym("$GT", 2);   p->eval_code = GT_SYM;
1433   p = insert_sym("$GE", 2);   p->eval_code = GE_SYM;
1434 
1435   p = insert_sym("$AND", 2);  p->eval_code = AND_SYM;
1436   p = insert_sym("$OR", 2);   p->eval_code = OR_SYM;
1437   p = insert_sym("$NOT", 1);  p->eval_code = NOT_SYM;
1438   p = insert_sym("$TRUE", 1); p->eval_code = TRUE_SYM;
1439   p = insert_sym("$T", 0);    p->eval_code = T_SYM;
1440   p = insert_sym("$F", 0);    p->eval_code = F_SYM;
1441 
1442   p = insert_sym("$ID", 2);   p->eval_code = ID_SYM;
1443   p = insert_sym("$LNE", 2);  p->eval_code = LNE_SYM;
1444   p = insert_sym("$LLT", 2);  p->eval_code = LLT_SYM;
1445   p = insert_sym("$LLE", 2);  p->eval_code = LLE_SYM;
1446   p = insert_sym("$LGT", 2);  p->eval_code = LGT_SYM;
1447   p = insert_sym("$LGE", 2);  p->eval_code = LGE_SYM;
1448 
1449   p = insert_sym("$BIT_AND", 2);     p->eval_code = BIT_AND_SYM;
1450   p = insert_sym("$BIT_OR", 2);      p->eval_code = BIT_OR_SYM;
1451   p = insert_sym("$BIT_XOR", 2);     p->eval_code = BIT_XOR_SYM;
1452   p = insert_sym("$BIT_NOT", 1);     p->eval_code = BIT_NOT_SYM;
1453   p = insert_sym("$SHIFT_LEFT", 2);  p->eval_code = SHIFT_LEFT_SYM;
1454   p = insert_sym("$SHIFT_RIGHT", 2); p->eval_code = SHIFT_RIGHT_SYM;
1455 
1456   p = insert_sym("$INT_TO_BITS", 1);     p->eval_code = INT_TO_BITS_SYM;
1457   p = insert_sym("$BITS_TO_INT", 1);     p->eval_code = BITS_TO_INT_SYM;
1458 
1459   p = insert_sym("$IF", 3);          p->eval_code = IF_SYM;
1460 
1461   p = insert_sym("$NEXT_CL_NUM", 0); p->eval_code = NEXT_CL_NUM_SYM;
1462   p = insert_sym("$ATOMIC", 1);      p->eval_code = ATOMIC_SYM;
1463   p = insert_sym("$INT", 1);         p->eval_code = INT_SYM;
1464   p = insert_sym("$BITS", 1);        p->eval_code = BITS_SYM;
1465   p = insert_sym("$VAR", 1);         p->eval_code = VAR_SYM;
1466   p = insert_sym("$GROUND", 1);      p->eval_code = GROUND_SYM;
1467   p = insert_sym("$OUT", 1);         p->eval_code = OUT_SYM;
1468 
1469   p = insert_sym("$FSUM", 2);  p->eval_code = FSUM_SYM;
1470   p = insert_sym("$FPROD", 2); p->eval_code = FPROD_SYM;
1471   p = insert_sym("$FDIFF", 2); p->eval_code = FDIFF_SYM;
1472   p = insert_sym("$FDIV", 2);  p->eval_code = FDIV_SYM;
1473 
1474   p = insert_sym("$FEQ", 2);   p->eval_code = FEQ_SYM;
1475   p = insert_sym("$FNE", 2);   p->eval_code = FNE_SYM;
1476   p = insert_sym("$FLT", 2);   p->eval_code = FLT_SYM;
1477   p = insert_sym("$FLE", 2);   p->eval_code = FLE_SYM;
1478   p = insert_sym("$FGT", 2);   p->eval_code = FGT_SYM;
1479   p = insert_sym("$FGE", 2);   p->eval_code = FGE_SYM;
1480 
1481   p = insert_sym("$COMMON_EXPRESSION", 3); p->eval_code = COMMON_EXPRESSION_SYM;
1482 
1483   p = insert_sym("$RENAME", 2);      p->eval_code = RENAME_SYM;
1484   p = insert_sym("$UNIQUE_NUM", 0);  p->eval_code = UNIQUE_NUM_SYM;
1485   p = insert_sym("$OCCURS", 2);      p->eval_code = OCCURS_SYM;
1486   p = insert_sym("$VOCCURS", 2);     p->eval_code = VOCCURS_SYM;
1487   p = insert_sym("$VFREE", 2);       p->eval_code = VFREE_SYM;
1488 }  /* built_in_symbols */
1489 
1490 /*************
1491  *
1492  *    int declare_op(prec, type, str)
1493  *
1494  *************/
1495 
declare_op(int prec,int type,char * str)1496 int declare_op(int prec,
1497 	       int type,
1498 	       char *str)
1499 {
1500   int arity, sn, save_flag;
1501   struct sym_ent *p;
1502 
1503   if (prec < 1 || prec > 999)
1504     return(0);
1505 
1506   switch (type) {
1507   case FX:
1508   case FY:
1509   case XF:
1510   case YF: arity = 1; break;
1511   case XFX:
1512   case XFY:
1513   case YFX: arity = 2; break;
1514   default: return(0);
1515   }
1516 
1517   save_flag = Flags[CHECK_ARITY].val;
1518   Flags[CHECK_ARITY].val = 0;
1519   sn = str_to_sn(str, arity);
1520   Flags[CHECK_ARITY].val = save_flag;
1521 
1522   p = sn_to_node(sn);
1523 
1524   /* Don't check if it's already special.  Allow it to change. */
1525 
1526   p->special_op = 1;
1527   p->op_type = type;
1528   p->op_prec = prec;
1529   return(1);
1530 
1531 }  /* declare_op */
1532 
1533 /*************
1534  *
1535  *    init_special_ops()
1536  *
1537  *    Declare the built-in special operators.
1538  *
1539  *************/
1540 
init_special_ops(void)1541 void init_special_ops(void)
1542 {
1543   int rc;
1544 
1545   rc = declare_op(800,  XFY, "#");
1546 
1547   rc = declare_op(800,  XFX, "->");
1548   rc = declare_op(800,  XFX, "<->");
1549   rc = declare_op(790,  XFY, "|");
1550   rc = declare_op(780,  XFY, "&");
1551 
1552   rc = declare_op(700,  XFX, "=");
1553   rc = declare_op(700,  XFX, "!=");
1554 
1555   rc = declare_op(700,  XFX, "<");
1556   rc = declare_op(700,  XFX, ">");
1557   rc = declare_op(700,  XFX, "<=");
1558   rc = declare_op(700,  XFX, ">=");
1559   rc = declare_op(700,  XFX, "==");
1560   rc = declare_op(700,  XFX, "=/=");
1561 
1562   rc = declare_op(700,  XFX, "@<");
1563   rc = declare_op(700,  XFX, "@>");
1564   rc = declare_op(700,  XFX, "@<=");
1565   rc = declare_op(700,  XFX, "@>=");
1566 
1567   rc = declare_op(500,  XFY, "+");
1568   rc = declare_op(500,  XFX, "-");
1569 
1570   rc = declare_op(500,   FX, "+");
1571   rc = declare_op(500,   FX, "-");
1572 
1573   rc = declare_op(400,  XFY, "*");
1574   rc = declare_op(400,  XFX, "/");
1575 
1576   rc = declare_op(300,  XFX, "mod");
1577 
1578 #ifndef SINGLE_QUOTE
1579   rc = declare_op(300,  XF, "\'");
1580 #endif
1581 
1582 }  /* init_special_ops */
1583 
1584 /*************
1585  *
1586  *    int process_op_command(t)
1587  *
1588  *************/
1589 
process_op_command(struct term * t)1590 int process_op_command(struct term *t)
1591 {
1592   int type, n, rc;
1593   struct term *t1, *t2;
1594   char *s;
1595 
1596   if (sn_to_arity(t->sym_num) != 3) {
1597     printf("op command must have arity 3.\n");
1598     return(0);
1599   }
1600   t1 = t->farg->argval;
1601   if (t1->type != NAME || !str_int(sn_to_str(t1->sym_num), &n) ||
1602       n < 1 || n > 999) {
1603     printf("\nERROR: first argument of op command must be 1..999.\n");
1604     return(0);
1605   }
1606   t1 = t->farg->narg->argval;
1607   s = sn_to_str(t1->sym_num);
1608   if (str_ident(s, "xfx") || str_ident(s, "infix"))
1609     type = XFX;
1610   else if (str_ident(s, "xfy") || str_ident(s, "infix_right"))
1611     type = XFY;
1612   else if (str_ident(s, "yfx") || str_ident(s, "infix_left"))
1613     type = YFX;
1614   else if (str_ident(s, "fx") || str_ident(s, "prefix"))
1615     type = FX;
1616   else if (str_ident(s, "xf") || str_ident(s, "postfix"))
1617     type = XF;
1618   else if (str_ident(s, "fy") || str_ident(s, "prefix_assoc"))
1619     type = FY;
1620   else if (str_ident(s, "yf") || str_ident(s, "postfix_assoc"))
1621     type = YF;
1622   else
1623     type = MAX_INT;
1624 
1625   if (type == MAX_INT || t1->type != NAME) {
1626     printf("\nERROR: second argument of op command must be xfx, xfy, yfx, xf, yf, fx, or fy.\n");
1627     return(0);
1628   }
1629 
1630   t1 = t->farg->narg->narg->argval;
1631 
1632   if (t1->type == NAME)
1633     rc = declare_op(n, type, sn_to_str(t1->sym_num));
1634   else if (proper_list(t1)) {
1635     for ( ; t1->type == COMPLEX; t1 = t1->farg->narg->argval) {
1636       t2 = t1->farg->argval;
1637       if (t2->type != NAME) {
1638 	printf("\nERROR: list in op command must be all names.\n");
1639 	return(0);
1640       }
1641       rc = declare_op(n, type, sn_to_str(t2->sym_num));
1642     }
1643   }
1644   else {
1645     printf("\nERROR: third argument of op command must be a name or a list.\n");
1646     return(0);
1647   }
1648   return(1);
1649 }  /* process_op_command */
1650 
1651 /*************
1652  *
1653  *    void fill_in_op_data(p, t)
1654  *
1655  *************/
1656 
fill_in_op_data(struct sequence_member * p,struct term * t)1657 static void fill_in_op_data(struct sequence_member *p,
1658 			    struct term *t)
1659 {
1660   struct sym_ent *nd;
1661   char *str;
1662   int i, flag;
1663 
1664   p->t = t;
1665   p->binary_type = p->unary_type = 0;
1666   p->binary_prec = p->unary_prec = 0;
1667 
1668   if (t->type == NAME) {
1669     str = sn_to_str(t->sym_num);
1670     for (i = flag = 0; i < SYM_TAB_SIZE && flag < 2; i++) {
1671       for (nd = Sym_tab[i]; nd && flag < 2; nd = nd->next) {
1672 	if (str_ident(str, nd->name) && nd->special_op) {
1673 	  if (nd->arity == 1) {
1674 	    p->unary_type = nd->op_type;
1675 	    p->unary_prec = nd->op_prec;
1676 	  }
1677 	  else {  /* must be binary */
1678 	    p->binary_type = nd->op_type;
1679 	    p->binary_prec = nd->op_prec;
1680 	  }
1681 	}
1682       }
1683     }
1684   }
1685 
1686 }  /* fill_in_op_data */
1687 
1688 /*************
1689  *
1690  *    int is_white(c) -- including start-of-comment '%'.
1691  *
1692  *************/
1693 
is_white(char c)1694 static int is_white(char c)
1695 {
1696   return(c == ' ' ||
1697 	 c == '\t' ||  /* tab */
1698 	 c == '\n' ||  /* newline */
1699 	 c == '\v' ||  /* vertical tab */
1700 	 c == '\r' ||  /* carriage return */
1701 	 c == '\f' ||  /* form feed */
1702 	 c == '%');
1703 }  /* is_white */
1704 
1705 /*************
1706  *
1707  *    skip_white(buffer, position)
1708  *
1709  *    Advance the pointer to the next nonwhite, noncomment position.
1710  *
1711  *************/
1712 
skip_white(char * buf,int * p)1713 void skip_white(char *buf,
1714 		int *p)
1715 {
1716   char c;
1717   c = buf[*p];
1718   while (is_white(c)) {
1719     if (c == '%')  /* skip over comment */
1720       while (buf[++(*p)] != '\n' && buf[*p] != '\0') ;
1721     if (buf[*p] == '\0')
1722       c = '\0';
1723     else
1724       c = buf[++(*p)];
1725   }
1726 }  /* skip_white */
1727 
1728 /*************
1729  *
1730  *    int is_symbol_char(c, in_list)
1731  *
1732  *************/
1733 
is_symbol_char(char c,int in_list)1734 static int is_symbol_char(char c,
1735 			  int in_list)
1736 {
1737   return(c == '+' ||
1738 	 c == '-' ||
1739 	 c == '*' ||
1740 	 c == '/' ||
1741 	 c == '\\' ||
1742 	 c == '^' ||
1743 	 c == '<' ||
1744 	 c == '>' ||
1745 	 c == '=' ||
1746 	 c == '`' ||
1747 	 c == '~' ||
1748 	 c == ':' ||
1749 	 c == '?' ||
1750 	 c == '@' ||
1751 	 c == '&' ||
1752 
1753 	 (c == '|' && !in_list) ||
1754 #ifndef SINGLE_QUOTE
1755 	 c == '\'' ||
1756 #endif
1757 	 c == '!' ||
1758 	 c == '#' ||
1759 	 c == ';'    );
1760 
1761 }  /* is_symbol_char */
1762 
1763 /*************
1764  *
1765  *    int quote_char(c)
1766  *
1767  *************/
1768 
quote_char(char c)1769 static int quote_char(char c)
1770 {
1771   return(
1772 #ifdef SINGLE_QUOTE
1773 	 c == '\'' ||
1774 #endif
1775 	 c == '\"');
1776 
1777 }  /* quote_char */
1778 
1779 /*************
1780  *
1781  *    int is_alpha_numeric(c) -- including _ and $
1782  *
1783  *************/
1784 
is_alpha_numeric(char c)1785 static int is_alpha_numeric(char c)
1786 {
1787   return((c >= '0' && c <= '9') ||
1788 	 (c >= 'a' && c <= 'z') ||
1789 	 (c >= 'A' && c <= 'Z') ||
1790 	 c == '_' ||
1791 	 c == '$');
1792 }  /* is_alpha_numeric */
1793 
1794 /*************
1795  *
1796  *    int name_sym(s)
1797  *
1798  *************/
1799 
name_sym(char * s)1800 int name_sym(char *s)
1801 {
1802   if (quote_char(*s))
1803     return(1);  /* quoted string ok */
1804   else {
1805     for ( ; *s; s++)
1806       if (!is_alpha_numeric(*s))
1807 	return(0);
1808     return(1);
1809   }
1810 }  /* name_sym */
1811 
1812 /*************
1813  *
1814  *    get_name(buffer, position, name, in_list)
1815  *
1816  *************/
1817 
get_name(char * buf,int * p,char * name,int in_list)1818 static void get_name(char *buf,
1819 		     int *p,
1820 		     char *name,
1821 		     int in_list)
1822 {
1823   int i, ok, okq;
1824   char c, q;
1825 
1826   i = 0; ok = 1; okq = 1;
1827   skip_white(buf, p);
1828   c = buf[*p];
1829   if (is_alpha_numeric(c)) {
1830     while ((ok = i < MAX_NAME-1) && is_alpha_numeric(c)) {
1831       name[i++] = c;
1832       c = buf[++(*p)];
1833     }
1834   }
1835   else if (is_symbol_char(c, in_list)) {
1836     while ((ok = i < MAX_NAME-1) && is_symbol_char(c, in_list)) {
1837       name[i++] = c;
1838       c = buf[++(*p)];
1839     }
1840   }
1841   else if (quote_char(c)) {
1842     q = c;
1843     name[i++] = c;
1844     c = buf[++(*p)];
1845     while ((ok = i < MAX_NAME-1) && c != q && (okq = c != '\0')) {
1846       name[i++] = c;
1847       c = buf[++(*p)];
1848     }
1849     if (okq) {
1850       name[i++] = c;  /* quote char */
1851       ++(*p);
1852     }
1853   }
1854 
1855   if (!ok) {
1856     fprintf(stdout, "\nERROR, name too big, max is %d; ", MAX_NAME-1);
1857     name[0] = '\0';
1858   }
1859   else if (!okq) {
1860     fprintf(stdout, "\nERROR, quoted name has no end; ");
1861     name[0] = '\0';
1862   }
1863   else
1864     name[i] = '\0';
1865 }  /* get_name */
1866 
1867 /*************
1868  *
1869  *    print_error(fp, buf, pos)
1870  *
1871  *************/
1872 
print_error(FILE * fp,char * buf,int pos)1873 void print_error(FILE *fp,
1874 		 char *buf,
1875 		 int pos)
1876 {
1877 #if 0
1878   int i;
1879 
1880   fprintf(fp, "%s\n", buf);
1881   for (i = 0; i < pos; i++) {
1882     if (buf[i] == '\t')
1883       fprintf(fp, "--------");  /* doesn't always work */
1884     else if (buf[i] == '\n')
1885       fprintf(fp, "\n");
1886     else
1887       fprintf(fp, "-");
1888   }
1889   fprintf(fp, "^\n");
1890 #else
1891   int i;
1892   i = 0;
1893   if (buf[0] == '\n')
1894     i = 1;
1895   while (i < pos) {
1896     if (buf[i] == '%')  /* skip over comment */
1897       while (buf[++i] != '\n') ;
1898     fprintf(fp, "%c", buf[i++]);
1899   }
1900   fprintf(fp, " ***HERE*** ");
1901 
1902   while (buf[i]) {
1903     if (buf[i] == '%')  /* skip over comment */
1904       while (buf[++i] != '\n') ;
1905     fprintf(fp, "%c", buf[i++]);
1906   }
1907   fprintf(fp, "\n");
1908 
1909 #endif
1910 }  /* print_error */
1911 
1912 /* We need this declaration, because seq_to_term is mutually recursive
1913    with seq_to_quant_term
1914 */
1915 
1916 static struct term *seq_to_term(struct sequence_member *seq,
1917 				int start,
1918 				int end,
1919 				int m);
1920 
1921 /*************
1922  *
1923  *    struct term *seq_to_quant_term(seq, n)
1924  *
1925  *    Take a sequence of terms t1,...,tn and build term $Quantified(t1,...,tn).
1926  *    t1 is already known to be a quantifier, and n >= 3.
1927  *    Check that t2,...,tn-1 are all names.
1928  *    On success, the resulting term is an entirely new copy.
1929  *
1930  *************/
1931 
seq_to_quant_term(struct sequence_member * seq,int n)1932 static struct term *seq_to_quant_term(struct sequence_member *seq,
1933 				      int n)
1934 {
1935   struct rel *r_prev, *r_new;
1936   struct term *t, *t1;
1937   int i;
1938 
1939   if (n == 1)
1940     return(NULL);
1941 
1942   for (i = 1; i < n-1; i++)
1943     if (seq[i].t->type != NAME)
1944       return(NULL);
1945 
1946   /* Special case: negated formula need not be parenthesized.
1947    * For example, all x -p(x) is OK.  In this case, the sequence is
1948    * [all, x, -, p(x)], so we must adjust things.
1949    */
1950 
1951   if (str_ident(sn_to_str(seq[n-2].t->sym_num), "-")) {
1952     if (n == 3)
1953       return(NULL);  /* all - p */
1954     else {
1955       struct term *t;
1956       t = seq_to_term(seq, n-2, n-1, 1000);
1957       printf("adjusted term: "); p_term(t);
1958       if (t) {
1959 	zap_term(seq[n-2].t);
1960 	zap_term(seq[n-1].t);
1961 	fill_in_op_data(&seq[n-2], t);
1962 	/* caller will still think there are n terms */
1963 	seq[n-1].t = NULL;
1964 	n--;
1965       }
1966       else
1967 	return(NULL);
1968     }
1969   }
1970 
1971   t = get_term();
1972   t->type = COMPLEX;
1973   t->sym_num = str_to_sn("$Quantified", n);
1974   for (i = 0, r_prev = NULL; i < n; i++) {
1975     r_new = get_rel();
1976     if (!r_prev)
1977       t->farg = r_new;
1978     else
1979       r_prev->narg = r_new;
1980     t1 = copy_term(seq[i].t);
1981     r_new->argval = t1;
1982     r_prev = r_new;
1983   }
1984   return(t);
1985 
1986 }  /* seq_to_quant_term */
1987 
1988 /*************
1989  *
1990  *    struct term *seq_to_term(seq, start, end, m)
1991  *
1992  *    seq is an array of terms/operators, and start and end are
1993  *    indexes into seq.  This routine attempts to construct a term
1994  *    starting with start, ending with end, with precedence <= m.
1995  *    On success, the resulting term is an entirely new copy.
1996  *
1997  *************/
1998 
seq_to_term(struct sequence_member * seq,int start,int end,int m)1999 static struct term *seq_to_term(struct sequence_member *seq,
2000 			 int start,
2001 			 int end,
2002 			 int m)
2003 {
2004   int i, n, type;
2005   struct term *t1, *t2, *t3, *t;
2006   struct rel *r1, *r2;
2007 
2008   if (start == end) {
2009     t = copy_term(seq[start].t);
2010     return(t);
2011   }
2012   else {
2013 
2014     /* Check if first is prefix op that applies to rest. */
2015 
2016     if (seq[start].t->type == NAME) {
2017       type = seq[start].unary_type;
2018       n = seq[start].unary_prec;
2019       t = seq[start].t;
2020 
2021       if (type == FX && n <= m) {
2022 	t1 = seq_to_term(seq, start+1, end, n-1);
2023 	if (t1) {
2024 	  t3 = get_term();
2025 	  t3->type = COMPLEX;
2026 	  t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 1);
2027 	  r1 = get_rel();
2028 	  t3->farg = r1;
2029 	  r1->argval = t1;
2030 	  return(t3);
2031 	}
2032       }
2033       else if (type == FY && n <= m) {
2034 	t1 = seq_to_term(seq, start+1, end, n);
2035 	if (t1) {
2036 	  t3 = get_term();
2037 	  t3->type = COMPLEX;
2038 	  t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 1);
2039 	  r1 = get_rel();
2040 	  t3->farg = r1;
2041 	  r1->argval = t1;
2042 	  return(t3);
2043 	}
2044       }
2045     }
2046 
2047     /* Check if last is postfix op that applies to all preceding. */
2048 
2049     if (seq[end].t->type == NAME) {
2050       type = seq[end].unary_type;
2051       n = seq[end].unary_prec;
2052       t = seq[end].t;
2053 
2054       if (type == XF && n <= m) {
2055 	t1 = seq_to_term(seq, start, end-1, n-1);
2056 	if (t1) {
2057 	  t3 = get_term();
2058 	  t3->type = COMPLEX;
2059 	  t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 1);
2060 	  r1 = get_rel();
2061 	  t3->farg = r1;
2062 	  r1->argval = t1;
2063 	  return(t3);
2064 	}
2065       }
2066       else if (type == YF && n <= m) {
2067 	t1 = seq_to_term(seq, start, end-1, n);
2068 	if (t1) {
2069 	  t3 = get_term();
2070 	  t3->type = COMPLEX;
2071 	  t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 1);
2072 	  r1 = get_rel();
2073 	  t3->farg = r1;
2074 	  r1->argval = t1;
2075 	  return(t3);
2076 	}
2077       }
2078     }
2079 
2080     /* Look for an infix operator. */
2081 
2082     for (i = start+1; i <= end-1; i++) {
2083       if (seq[i].t->type == NAME) {
2084 	type = seq[i].binary_type;
2085 	n = seq[i].binary_prec;
2086 	t = seq[i].t;
2087 
2088 	if (type == XFY && n <= m) {
2089 	  t1 = seq_to_term(seq, start, i-1, n-1);
2090 	  if (t1) {
2091 	    t2 = seq_to_term(seq, i+1, end, n);
2092 	    if (!t2)
2093 	      zap_term(t1);
2094 	  }
2095 	  if (t1 && t2) {
2096 	    t3 = get_term();
2097 	    t3->type = COMPLEX;
2098 	    t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 2);
2099 	    r1 = get_rel(); r2 = get_rel();
2100 	    t3->farg = r1; r1->narg = r2;
2101 	    r1->argval = t1; r2->argval = t2;
2102 	    return(t3);
2103 	  }
2104 	}
2105 	else if (type == YFX && n <= m) {
2106 	  t1 = NULL;
2107 	  t2 = seq_to_term(seq, i+1, end, n-1);
2108 	  if (t2) {
2109 	    t1 = seq_to_term(seq, start, i-1, n);
2110 	    if (!t1)
2111 	      zap_term(t2);
2112 	  }
2113 	  if (t1 && t2) {
2114 	    t3 = get_term();
2115 	    t3->type = COMPLEX;
2116 	    t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 2);
2117 	    r1 = get_rel(); r2 = get_rel();
2118 	    t3->farg = r1; r1->narg = r2;
2119 	    r1->argval = t1; r2->argval = t2;
2120 	    return(t3);
2121 	  }
2122 	}
2123 	else if (type == XFX && n <= m) {
2124 	  t1 = seq_to_term(seq, start, i-1, n-1);
2125 	  t2 = NULL;
2126 	  if (t1) {
2127 	    t2 = seq_to_term(seq, i+1, end, n-1);
2128 	    if (!t2)
2129 	      zap_term(t1);
2130 	  }
2131 	  if (t1 && t2) {
2132 	    t3 = get_term();
2133 	    t3->type = COMPLEX;
2134 	    t3->sym_num = str_to_sn(sn_to_str(t->sym_num), 2);
2135 	    r1 = get_rel(); r2 = get_rel();
2136 	    t3->farg = r1; r1->narg = r2;
2137 	    r1->argval = t1; r2->argval = t2;
2138 	    return(t3);
2139 	  }
2140 	}
2141       }  /* name */
2142     }  /* loop looking for infix op to apply */
2143 
2144     return(NULL);
2145   }
2146 }  /* seq_to_term */
2147 
2148 /*************
2149  *
2150  *    struct term_ptr *str_to_args(buffer, position, name)
2151  *
2152  *    name -- the functor.
2153  *
2154  *    start: functor(  a1 , a2 , a3 )
2155  *                   ^
2156  *    end:   functor(  a1 , a2 , a3 )
2157  *                                  ^
2158  *************/
2159 
str_to_args(char * buf,int * p,char * name)2160 static struct term *str_to_args(char *buf,
2161 				int *p,
2162 				char *name)
2163 {
2164   struct term *t, *t_sub;
2165   struct rel *r1, *r2;
2166   int i;
2167 
2168   t = get_term();
2169   t->type = COMPLEX;
2170   r1 = NULL;
2171   i = 0;  /* count subterms to get arity */
2172 
2173   while (buf[*p] != ')') {
2174     i++;
2175     t_sub = str_to_term(buf, p, 0);
2176     if (t_sub == NULL)
2177       return(NULL);
2178     else if (buf[*p] != ',' && buf[*p] != ')') {
2179       fprintf(stdout, "\nERROR, comma or ) expected:\n");
2180       print_error(stdout, buf, *p);
2181       return(NULL);
2182     }
2183     else {
2184       r2 = get_rel();
2185       r2->argval = t_sub;
2186       if (r1 == NULL)
2187 	t->farg = r2;
2188       else
2189 	r1->narg = r2;
2190       r1 = r2;
2191       if (buf[*p] == ',')
2192 	(*p)++;          /* step past comma */
2193     }
2194   }
2195   if (i == 0) {
2196     fprintf(stdout, "\nERROR, functor has no arguments:\n");
2197     print_error(stdout, buf, *p);
2198     return(NULL);
2199   }
2200 
2201   t->sym_num = str_to_sn(name, i);  /* functor */
2202   return(t);
2203 
2204 }  /* str_to_args */
2205 
2206 /*************
2207  *
2208  *    struct term_ptr *str_to_list(buffer, position)
2209  *
2210  *    start: [ a1 , a2 , a3 ]
2211  *           ^
2212  *    end:   [ a1 , a2 , a3 ]
2213  *                           ^
2214  *************/
2215 
str_to_list(char * buf,int * p)2216 static struct term *str_to_list(char *buf,
2217 				int *p)
2218 {
2219   struct term *t_cons, *t_head, *t_tail, *t_return;
2220   struct rel *r_head, *r_tail;
2221   int go;
2222 
2223   (*p)++;  /* step past '[' */
2224 
2225   if (buf[*p] == ']') {                        /* [] */
2226     t_return = get_term();
2227     t_return->type = NAME;
2228     t_return->sym_num = str_to_sn("$nil", 0);
2229     (*p)++;  /* skip "]" */
2230     return(t_return);
2231   }
2232   else {                           /* [h|t], [t1,...,tn], or [t1,...,tn|t] */
2233     t_return = NULL; r_tail = NULL;
2234     go = 1;
2235 
2236     while (go) {
2237       t_head = str_to_term(buf, p, 1);
2238       if (t_head == NULL)
2239 	return(NULL);  /* error */
2240       t_cons = get_term();
2241       if (r_tail == NULL)
2242 	t_return = t_cons;
2243       else
2244 	r_tail->argval = t_cons;
2245       t_cons->type = COMPLEX;
2246       t_cons->sym_num = str_to_sn("$cons", 2);
2247       r_head = get_rel();
2248       t_cons->farg = r_head;
2249       r_head->argval = t_head;
2250       r_tail = get_rel();
2251       r_head->narg = r_tail;
2252       go = (buf[*p] == ',');
2253       if (go)
2254 	(*p)++;  /* step past ',' */
2255     }
2256 
2257     if (buf[*p] == ']') {
2258       t_tail = get_term();
2259       r_tail->argval = t_tail;
2260       t_tail->type = NAME;
2261       t_tail->sym_num = str_to_sn("$nil", 0);
2262       (*p)++;  /* step past ']' */
2263       return(t_return);
2264     }
2265     else if (buf[*p] == '|') {
2266       (*p)++;  /* step past '|' */
2267       t_tail = str_to_term(buf, p, 1);
2268       if (buf[*p] != ']') {
2269 	fprintf(stdout, "\nERROR, ']' expected in list:\n");
2270 	print_error(stdout, buf, *p);
2271 	return(NULL);
2272       }
2273       r_tail->argval = t_tail;
2274       (*p)++;  /* step past ']' */
2275       return(t_return);
2276     }
2277     else {
2278       fprintf(stdout, "\nERROR, ], |, or comma expected in list:\n");
2279       print_error(stdout, buf, *p);
2280       return(NULL);
2281     }
2282   }
2283 }  /* str_to_list */
2284 
2285 /*************
2286  *
2287  *    int str_to_sequence(buffer, position, seq, in_list)
2288  *
2289  *    Read a sequence of operators/terms---It will be parsed into
2290  *    a term later in str_to_term.
2291  *    After successful call, position is the delimeter following the term.
2292  *
2293  *    Mutually recursive with str_to_term.
2294  *
2295  *    If success, return the number of terms read.
2296  *
2297  *    If a syntax error is found, print message and return(0).
2298  *
2299  *************/
2300 
str_to_sequence(char * buf,int * p,struct sequence_member * seq,int in_list)2301 static int str_to_sequence(char *buf,
2302 			   int *p,
2303 			   struct sequence_member *seq,
2304 			   int in_list)
2305 {
2306   char name[MAX_NAME], c;
2307   struct term *t;
2308   int done, n, white;;
2309 
2310   done = 0; n = 0;
2311   while (!done) {
2312 
2313     get_name(buf, p, name, in_list);
2314     white = is_white(buf[*p]);  /* f(a) vs. f (a) */
2315     skip_white(buf, p);
2316 
2317     if (name[0] == '\0' && buf[*p] != '[' && buf[*p] != '(' && buf[*p] != '{') {
2318       fprintf(stdout, "\nERROR, name expected:\n");
2319       print_error(stdout, buf, *p);
2320       return(0);
2321     }
2322 
2323     else if (name[0] == '\0' && buf[*p] == '(') {         /* (term) */
2324       (*p)++;  /* step past '(' */
2325       t = str_to_term(buf, p, 0);
2326       if (t == NULL)
2327 	return(0);
2328       if (buf[*p] != ')') {
2329 	fprintf(stdout, "\nERROR, ')' expected:\n");
2330 	print_error(stdout, buf, *p);
2331 	return(0);
2332       }
2333       (*p)++;  /* step past ')' */
2334     }
2335 
2336     else if (name[0] == '\0' && buf[*p] == '{') {         /* {term} */
2337       (*p)++;  /* step past '{' */
2338       t = str_to_term(buf, p, 0);
2339       if (t == NULL)
2340 	return(0);
2341       if (buf[*p] != '}') {
2342 	fprintf(stdout, "\nERROR, '}' expected:\n");
2343 	print_error(stdout, buf, *p);
2344 	return(0);
2345       }
2346       (*p)++;  /* step past '}' */
2347     }
2348 
2349     else if (name[0] == '\0' && buf[*p] == '[') {           /* list */
2350       t = str_to_list(buf, p);
2351       if (t == NULL)
2352 	return(0);
2353     }
2354 
2355     else if (name[0] != '\0' && !white && buf[*p] == '(')  /* f(args) */
2356       {
2357 	(*p)++;  /* step past '(' */
2358 	t = str_to_args(buf, p, name);
2359 	if (t == NULL)
2360 	  return(0);
2361 	(*p)++;  /* step past ')' */
2362       }
2363 
2364     else if (name[0] != '\0') {                           /* name */
2365       t = get_term();
2366       t->type = NAME;
2367       /* If it's an operator, change arity later. */
2368       t->sym_num = str_to_sn(name, 0);
2369     }
2370 
2371     else {
2372       fprintf(stdout, "\nERROR, unrecognized error in term:\n");
2373       print_error(stdout, buf, *p);
2374       return(0);
2375     }
2376 
2377     /* We have a term t. */
2378 
2379     if (n == MAX_COMPLEX) {
2380       fprintf(stdout, "\nERROR, term too big:\n");
2381       print_error(stdout, buf, *p);
2382       return(0);
2383     }
2384     else {
2385       fill_in_op_data(&seq[n], t);
2386       n++;
2387     }
2388 
2389     skip_white(buf, p);
2390     c = buf[*p];
2391     done = (c == ',' || c == ')' || c == '}' || c == ']' ||
2392 	    c == '.' || c == '\0' || (in_list && c == '|'));
2393   }
2394   return(n);
2395 }  /* str_to_sequence */
2396 
2397 /*************
2398  *
2399  *    struct term *str_to_term(buffer, position, in_list)
2400  *
2401  *    Parse a string and build a term.
2402  *    Mutually recursive with str_to_sequence.
2403  *    After successful call, position is the delimeter following the term.
2404  *
2405  *    If a syntax error is found, print message and return(NULL).
2406  *
2407  *************/
2408 
str_to_term(char * buf,int * p,int in_list)2409 struct term *str_to_term(char *buf,
2410 			 int *p,
2411 			 int in_list)
2412 {
2413   struct sequence_member seq[MAX_COMPLEX];
2414   struct term *t;
2415   int n, i, save_pos;
2416 
2417   save_pos = *p;
2418 
2419   n = str_to_sequence(buf, p, seq, in_list);
2420   if (n == 0)
2421     return(NULL);
2422 
2423   else if (seq[0].t->type == NAME && n > 2 &&
2424 	   (str_ident(sn_to_str(seq[0].t->sym_num), "all") ||
2425 	    str_ident(sn_to_str(seq[0].t->sym_num), "exists"))) {
2426     t = seq_to_quant_term(seq, n);
2427     if (!t) {
2428       fprintf(stdout, "\nERROR in quantifier prefix starting here:\n");
2429       print_error(stdout, buf, save_pos);
2430     }
2431   }
2432 
2433   else {
2434     t = seq_to_term(seq, 0, n-1, 1000);
2435 
2436     if (!t) {
2437       fprintf(stdout, "\nERROR, the %d terms/operators in the following sequence are OK, but they\ncould not be combined into a single term with special operators.\n", n);
2438       for (i = 0; i < n; i++)
2439 	{ p_term(seq[i].t); printf("  ");}
2440       printf("\n");
2441       fprintf(stdout, "The context of the bad sequence is:\n");
2442       print_error(stdout, buf, save_pos);
2443     }
2444   }
2445 
2446   for (i = 0; i < n; i++)
2447     if (seq[i].t != NULL)
2448       zap_term(seq[i].t);
2449   return(t);
2450 }  /* str_to_term */
2451 
2452 /*************
2453  *
2454  *     int read_buf(file_ptr, buffer)
2455  *
2456  *    Read characters into buffer until one of the following:
2457  *        1.  '.' is reached ('.' goes into the buffer)
2458  *        2.  EOF is reached:  buf[0] = '\0' (an error occurs if
2459  *                 any nonwhite space precedes EOF)
2460  *        3.  MAX_BUF characters have been read (an error occurs)
2461  *
2462  *    If error occurs, return(0), else return(1).
2463  *
2464  *************/
2465 
read_buf(FILE * fp,char * buf)2466 int read_buf(FILE *fp,
2467 	     char *buf)
2468 {
2469   int c, qc, i, j, ok, eof, eof_q, max, max_q;
2470 
2471   ok = eof = eof_q = max = max_q = 0;  /* stop conditions */
2472   i = 0;
2473 
2474   while (!ok && !eof && !eof_q && !max && !max_q) {
2475 
2476     c = getc(fp);
2477     if (c == '%') {  /* comment--discard rest of line */
2478       while (c != '\n' && c != EOF)
2479 	c = getc(fp);
2480     }
2481     if (c =='.')
2482       ok = 1;
2483     else if (c == EOF)
2484       eof = 1;
2485     else if (i == MAX_BUF-1)
2486       max = 1;
2487     else {
2488       buf[i++] = c;
2489       if (quote_char(c)) {
2490 	qc = c;
2491 	c = getc(fp);
2492 	while (c != qc && c != EOF && i != MAX_BUF-1) {
2493 	  buf[i++] = c;
2494 	  c = getc(fp);
2495 	}
2496 	if (i == MAX_BUF-1)
2497 	  max_q = 1;
2498 	else if (c == EOF)
2499 	  eof_q = 1;
2500 	else
2501 	  buf[i++] = c;
2502       }
2503     }
2504   }
2505 
2506   if (ok) {
2507     buf[i++] = '.';
2508     buf[i] = '\0';
2509     return(1);
2510   }
2511   else if (eof) {
2512     /* white space at end of file is OK */
2513     j = 0;
2514     buf[i] = '\0';
2515     skip_white(buf, &j);
2516     if (i != j) {
2517       fprintf(stdout, "\nERROR, characters after last period: %s\n", buf);
2518       buf[0] = '\0';
2519       return(0);
2520     }
2521     else {
2522       buf[0] = '\0';
2523       return(1);
2524     }
2525   }
2526   else if (eof_q) {
2527     char s[500];
2528     buf[i>100 ? 100 : i] = '\0';
2529     sprintf(s, "read_buf, quoted string has no end:%s", buf);
2530     abend(s);
2531   }
2532   else if (max) {
2533     char s[500];
2534     buf[i>100 ? 100 : i] = '\0';
2535     sprintf(s, "read_buf, input string has more than %d characters, increase MAX_BUF", MAX_BUF);
2536     abend(s);
2537   }
2538   else {  /* max_q */
2539     char s[500];
2540     buf[i>100 ? 100 : i] = '\0';
2541     sprintf(s, "read_buf, input string (which contains quote mark) has more than %d characters, increase MAX_BUF", MAX_BUF);
2542     abend(s);
2543   }
2544   return(0);  /* to quiet lint */
2545 }  /* read_buf */
2546 
2547 /*************
2548  *
2549  *    struct term *term_fixup(t)
2550  *
2551  *    change !=(a,b) to -(=(a,b))
2552  *    change -(3)    to -3              not recursive, -(-(3)) -> -(-3))
2553  *    change +(3)    to +3              not recursive, +(+(3)) +> +(+3))
2554  *
2555  *************/
2556 
term_fixup(struct term * t)2557 struct term *term_fixup(struct term *t)
2558 {
2559   struct rel *r, *r1;
2560   struct term *t1;
2561   int neg;
2562   char *s, str[MAX_NAME];
2563   long l;
2564 
2565   if (t->type == COMPLEX) {
2566     if (is_symbol(t, "!=", 2)) {
2567       t1 = get_term(); t1->type = COMPLEX;
2568       r1 = get_rel();
2569       t1->farg = r1;
2570       r1->argval = t;
2571       t1->sym_num = str_to_sn("-", 1);
2572       t->sym_num = str_to_sn("=", 2);
2573       t = t1;
2574     }
2575 
2576     else if ((neg = is_symbol(t, "-", 1)) || is_symbol(t, "+", 1)) {
2577       t1 = t->farg->argval;
2578       s = sn_to_str(t1->sym_num);
2579       if (t1->type == NAME && str_long(s, &l)) {
2580 	cat_str((neg ? "-" : "+"), s, str);
2581 	t1->sym_num = str_to_sn(str, 0);
2582 	free_rel(t->farg);
2583 	free_term(t);
2584 	t = t1;
2585       }
2586     }
2587 
2588     for (r = t->farg; r; r = r->narg)
2589       r->argval = term_fixup(r->argval);
2590 
2591   }
2592   return(t);
2593 }  /* term_fixup */
2594 
2595 /*************
2596  *
2597  *    struct term *term_fixup_2(t)
2598  *
2599  *    change  -(=(a,b)) to !=(a,b)
2600  *
2601  *************/
2602 
term_fixup_2(struct term * t)2603 struct term *term_fixup_2(struct term *t)
2604 {
2605   struct term *t1;
2606   struct rel *r;
2607 
2608   if (is_symbol(t, "-", 1) && is_symbol(t->farg->argval, "=", 2)) {
2609     t1 = t->farg->argval;
2610     t1->sym_num = str_to_sn("!=", 2);
2611     free_rel(t->farg);
2612     free_term(t);
2613     t = t1;
2614   }
2615 
2616   if (t->type == COMPLEX)
2617     for (r = t->farg; r; r = r->narg)
2618       r->argval = term_fixup_2(r->argval);
2619 
2620   return(t);
2621 }  /* term_fixup_2 */
2622 
2623 /*************
2624  *
2625  *    struct term *read_term(file_ptr, retcd_ptr) --
2626  *
2627  *    Read and return then next term.
2628  *    It is assumed that the next term in the file is terminated
2629  *    with a period.   NULL is returned if EOF is reached first.
2630  *
2631  *    If an error is found, return(0); else return(1).
2632  *
2633  *************/
2634 
read_term(FILE * fp,int * rcp)2635 struct term *read_term(FILE *fp,
2636 		       int *rcp)
2637 {
2638   char buf[MAX_BUF+1];  /* one extra for \0 at end */
2639   int p, rc;
2640   struct term *t;
2641 
2642   rc = read_buf(fp, buf);
2643   if (rc == 0) {  /* error */
2644     *rcp = 0;
2645     return(NULL);
2646   }
2647   else if (buf[0] == '\0') {  /* ok. EOF */
2648     *rcp = 1;
2649     return(NULL);
2650   }
2651   else {
2652     p = 0;
2653     t = str_to_term(buf, &p, 0);
2654     if (t == NULL) {
2655       *rcp = 0;
2656       return(NULL);
2657     }
2658     else {
2659       skip_white(buf, &p);
2660       if (buf[p] != '.') {
2661 	fprintf(stdout, "\nERROR, text after term:\n");
2662 	print_error(stdout, buf, p);
2663 	*rcp = 0;
2664 	return(NULL);
2665       }
2666       else {
2667 	t = term_fixup(t);
2668 	*rcp = 1;
2669 	return(t);
2670       }
2671     }
2672   }
2673 }  /* read_term */
2674 
2675 /*************
2676  *
2677  *    merge_sort
2678  *
2679  *************/
2680 
merge_sort(void ** a,void ** w,int start,int end,int (* comp_proc)(void * v1,void * v2))2681 void merge_sort(void **a,
2682 		void **w,
2683 		int start,
2684 		int end,
2685 		int (*comp_proc)(void *v1, void *v2))
2686 {
2687   int mid, i, i1, i2, e1, e2;
2688 
2689   if (start < end) {
2690     mid = (start+end)/2;
2691     merge_sort(a, w, start, mid, comp_proc);
2692     merge_sort(a, w, mid+1, end, comp_proc);
2693     i1 = start; e1 = mid;
2694     i2 = mid+1; e2 = end;
2695     i = start;
2696     while (i1 <= e1 && i2 <= e2) {
2697       if ((*comp_proc)(a[i1], a[i2]) == LESS_THAN)
2698 	w[i++] = a[i1++];
2699       else
2700 	w[i++] = a[i2++];
2701     }
2702 
2703     if (i2 > e2)
2704       while (i1 <= e1)
2705 	w[i++] = a[i1++];
2706     else
2707       while (i2 <= e2)
2708 	w[i++] = a[i2++];
2709 
2710     for (i = start; i <= end; i++)
2711       a[i] = w[i];
2712   }
2713 }  /* merge_sort */
2714 
2715 /*************
2716  *
2717  *   compare_for_auto_lex_order()
2718  *
2719  *   First sort on arity:  0 < MAX_INT < ... < 3 < 2 < 1.
2720  *   Within arity, use strcmp function
2721  *
2722  *************/
2723 
compare_for_auto_lex_order(void * d1,void * d2)2724 int compare_for_auto_lex_order(void *d1,
2725 			       void *d2)
2726 {
2727   struct sym_ent *p1, *p2;
2728   int i;
2729 
2730   p1 = (struct sym_ent *) d1;
2731   p2 = (struct sym_ent *) d2;
2732 
2733   if (p1->arity == p2->arity) {
2734     i = strcmp(p1->name, p2->name);
2735     if (i < 0)
2736       return(LESS_THAN);
2737     else if (i > 0)
2738       return(GREATER_THAN);
2739     else {
2740       char s[500];
2741       sprintf(s, "compare_for_auto_lex_order, strings the same: %s.", p1->name);
2742       abend(s);
2743       return(0);  /* to quiet lint */
2744     }
2745   }
2746 
2747   else if (p1->arity == 0)
2748     return(LESS_THAN);
2749   else if (p2->arity == 0)
2750     return(GREATER_THAN);
2751   else if (p1->arity < p2->arity)
2752     return(GREATER_THAN);
2753   else
2754     return(LESS_THAN);
2755 }  /* compare_for_auto_lex_order */
2756 
2757 /*************
2758  *
2759  *   auto_lex_order()
2760  *
2761  *   Order the symbols in the symbol table using the lex_val field.
2762  *
2763  *************/
2764 
auto_lex_order(void)2765 void auto_lex_order(void)
2766 {
2767   int i, j, n;
2768   struct sym_ent *p;
2769   struct sym_ent **a, **w;
2770 
2771   /* Find an upper limit on the number of symbols. */
2772   n = new_sym_num();  /* don't use this for a sym_num */
2773   /* There should be at most n-1 symbols. */
2774 
2775   /* Allocate arrays for storing and for work. */
2776 
2777   a = (struct sym_ent **) tp_alloc(n * (int) sizeof(struct sym_ent *));
2778   w = (struct sym_ent **) tp_alloc(n * (int) sizeof(struct sym_ent *));
2779 
2780   for (i = j = 0; i < SYM_TAB_SIZE; i++)
2781     for (p = Sym_tab[i]; p; p = p->next)
2782       a[j++] = p;
2783 
2784   /* We find j symbols. */
2785 
2786 #if 0
2787   printf("\nauto_lex_order: new_sym_num=%d, count=%d.\n\n", n, j);
2788 #endif
2789 
2790   merge_sort((void **) a, (void **) w, 0, j-1, compare_for_auto_lex_order);
2791 
2792   /* Symbols get lex vals 2, 4, 6, 8, ... . */
2793 
2794   for (i = 0; i < j; i++) {
2795     a[i]->lex_val = i*2 + 2;
2796 #if 0
2797     printf("%7s %d %d\n", a[i]->name, a[i]->arity, i);
2798 #endif
2799   }
2800 
2801 }  /* auto_lex_order */
2802 
2803