/*                       dialog.c                     11-11-89 

**** The main interactive part of MaGIC.c.  This module  ****
**** contains the procedures to be executed in response  ****
**** to menu selections.                                 ****/




/************************************************************/

#include "mp_parse.c"

#define READLN { fflush(stdout); while (getchar() != '\n') ; }


char answer[80];                /* For input of axioms etc */
int Sizmax;


/************************************************************
 ************************************************************/
 
dialog()         /*** Get job specifications from the user
                      Return 1 if 'g' selected, 0 if 'e'
                      Return n > 1 to change to n processes ***/
{
   char menu();
   
   while (1) switch( menu() )
   {
      case 'a': add_axiom();      break;
      case 'b': bad_guy();        break;
      case 'c': connective();     break;
      case 'd': deletion();       break;
      case 'e':                   return(0);
      case 'f': fragment();       break;
      case 'g':                   return(1);
      case 'h': help(0); paws();  break;
      case 'i': IO_setting();     break;
      case 'j': jump_condition(); break;
      case 'k': job_defaults();   break;
      case 'l': logic_choice();   break;
      case '#': return(n_of_procs());
   }
}



/***********************************************************/

char menu()     /*** Return a user choice of next action ***/
{ char c, readin();

  set_frag();
  display();
  return( readin("abcdefghijkl#") );
}
    

/************************************************************/

char readin(str)  char *str;   /*** Return the first char
                                    from stdin which 
                                    matches one in str.   ***/
{ char ch;  int i;

  fflush(stdout);
  while ( 1 )
  {
     gets(answer);
     for ( i = 0; ch = answer[i]; i++ )
     {
        if ( isupper(ch) ) ch = tolower(ch);
        if ( strchr(str,ch) ) return(ch);
     }
  }
}


/*********************************************************/

paws()                               /*** I.e. "pause" ***/
{
  printf("\n\n Now type RETURN to continue.........");
  READLN
}


/*********************************************************/

strpos(str)  char *str; /*** Return the index of the start
                             of the first " "|" ,."-delimited
                             substring of LOGICS matching 
                             str, or -1 if no match.    ***/
{ int i,j;

    for ( i = 0; str[i]; i++ )
    if ( LOGICS[i] != str[i] ) goto P1; 
    if ( LOGICS[i]==',' ) return(0);
P1: for ( i = 1; LOGICS[i]; i++ )
    if ( LOGICS[i-1]==' ' )
    { 
       for ( j = 0; str[j]; j++ )
       if ( LOGICS[i+j] != str[j] ) goto P2; 
       if ( LOGICS[i+j]==',' || LOGICS[i+j]=='.'
            || LOGICS[i+j]==' ' ) return(i);
P2: ;}
    return(-1);
}


/*********************************************************/

char *copy(s,x)  char *s; int x;
                   /*** Return copy of s from offset x
                        to (not including) first non-
                        alphanumeric character.        ***/
{ char rtn[80];
  int i = 0;

  for ( s += x; (*s>='A'&&*s<='Z')||(*s>='0'&&*s<='9'); s++ )
  rtn[i++] = *s;
  rtn[i] = '\0';
  return(rtn);
}

/*********************************************************/

trim()    /*** Convert logic_name to upper case and remove
               non-alphanumeric characters             ***/
{ int i,j = 0;

  for ( i = 0; *(theJob->logic_name+i); i++ )
  { 
    if ( islower(*(theJob->logic_name+i))  )
    *(theJob->logic_name+i) = toupper(*(theJob->logic_name+i));
    if (isupper(*(theJob->logic_name+i)) 
        || isdigit(*(theJob->logic_name+i)))
    theJob->logic_name[j++] = *(theJob->logic_name+i);
  }
  while ( j < i ) theJob->logic_name[j++] = '\0';
}
    


/*********************************************************/

job_defaults()      /*** Get the system and initialise all the 
                         settings.                             ***/
{ char c;
  int i,j;
  
  theJob->symbols[0] = "tfTF          ";
  theJob->symbols[1] = "~             ";
  theJob->symbols[2] = "o&v>          ";
  for ( i = 1; i < AXMAX; i++ ) theJob->axiom[i] = 0;
  theJob->tty_out = PRETTY;  theJob->fil_out = NONE;  
  theJob->outfil_name[0] = '\0';
  theJob->maxmat = theJob->maxtime = 0;
  Sizmax = theJob->sizmax = SZ;  theJob->sizmax_ismax = 1;
  theJob->f_t = theJob->f_n = theJob->f_lat = theJob->f_fus = 1;
  wff_initial();
  if ( !noclear ) system("clear");
  printf("\n This is MaGIC ");  printf(VERSION);
  printf(", finding matrices for ");
  printf("your favourite logic.\n");
  printf(" Matrices come in all sizes up to %dx%d.\n",SZ,SZ);
  logic_choice();
}



/**********************************************************/
 
wff_initial()              /*** Initialise subf[], etc. ***/
{ int i,j;

  for ( i = 0; i < FMAX; i++ )
  { 
     theJob->form[i].lsub = theJob->form[i].rsub = 0;
     if ( i < 8 )
     theJob->form[i].sym = ( i < 5? 'p'+i: ( i == 5? 'f': 
                   ( i == 6? 'T': 'F' )));
     else 
     theJob->form[i].sym = ( i < 8+CMAX ? ' ' : 
                           ( i > 7+(3*CMAX) ? '\0' : 
                           ( i < 8+(2*CMAX)? 'a': 'b' )));
  }
  for ( i = 0; i < CMAX; i++ )
  { 
     theJob->atom[0][i] = 8+CMAX+i;
     theJob->atom[1][i] = 8+(2*CMAX)+i;
     theJob->defcon[i] = 0;
  }
  theJob->dcs[0] = '\0';
  for ( i = 0; i < TMAX; i++ ) theJob->root[i] = 0;
  theJob->failure = 0;
}



/**********************************************************/

set_frag()  /*** Make fragment include used connectives
                 and set Sizmax accordingly             ***/
{ int i;

  for ( i = 0; i < 19; i++ ) if ( theJob->axiom[i] )
  {
     if ( i == AxX || i == AxBA || i == AxSBA || i == AxRED ) 
          theJob->f_n = 1;
     if ( i == AxK || i == AxK2 || i == AxCt ) 
          theJob->f_t = 1;
     if ( i == AxX || i == AxBA || i == AxSBA || i == AxW2
          || i == AxWB || i == Axat ) theJob->f_lat = 1;
     if ( i == AxK || i == AxK2 || i == AxTF ) theJob->f_T = 1;
  }
  if ( theJob->f_n && (theJob->logic == RW || 
                       theJob->logic == R  || theJob->logic == CK) )
     theJob->f_fus = 1;
  for ( i = 0; theJob->root[i]; i++ ) 
  check_frag(theJob->form+theJob->root[i]);
  if ( theJob->failure ) check_frag(theJob->form+theJob->failure);
  for ( i = 0; theJob->dcs[i]; i++ ) 
  check_frag(theJob->form+theJob->defcon[i]);
  if ( theJob->totord ) theJob->f_lat = 1;
  if ( theJob->f_lat ) theJob->f_t = theJob->f_T = theJob->f_F = 1;
  if (( theJob->f_F || theJob->f_T ) && theJob->f_n ) 
  theJob->f_F = theJob->f_T = 1;
  if ( !(theJob->f_lat || theJob->f_n) ) Sizmax = theJob->f_t?  7: 6;
  else if ( !theJob->f_lat )             Sizmax = theJob->f_t?  8: 7;
  else if ( *(theJob->logic_name) == 'L' ) 
                                         Sizmax = theJob->f_n? 10: 8;
  else if ( !theJob->totord )            Sizmax = 
       (theJob->f_n && theJob->logic==S4 || theJob->axiom[AxBA])? 16:
                                                (theJob->f_n? 14: 9);
  else                                   Sizmax = theJob->f_n? 16: 12;
  if ( theJob->sizmax > Sizmax || theJob->sizmax_ismax ) 
  theJob->sizmax = Sizmax;
}


/**********************************************************/

check_frag(s)  WFF *s;       /*** Attend to connectives 
                                  used in (sub)formula   ***/
{
   if ( !s ) return(0);
   switch(s->sym)
   {
      case '~': theJob->f_n = 1;   break;
      case 'f': theJob->f_n = 1;
      case 't': theJob->f_t = 1;   break;
      case 'T': theJob->f_T = 1;   break;
      case 'F': theJob->f_F = 1;   break;
      case 'o': theJob->f_fus = 1; break;
      case '&':
      case 'v': theJob->f_lat = 1;
   }
   check_frag(s->lsub);
   check_frag(s->rsub);
}




/**********************************************************/

add_axiom()
{ int i;

  put_out( "AX.show" );
  printf(" %-5d< User-defined axiom >", AXMAX-1);
  printf("\n\n Select one of the above by typing its number:  ");
  fflush(stdout); scanf("%d", &i); READLN
  if (i==AXMAX-1) user_axiom();
  else if ( i > 0 && i < AXMAX-1 ) theJob->axiom[i] = 1;
}



/**********************************************************/

user_axiom()     /*** Take user definition of a formula
                      to go in next root[].             ***/
{ int i;

  for ( i = 0; theJob->root[i] && i<TMAX; i++ ) ;
  if  (i == TMAX ) 
  { 
     printf(
     "\n\n Maximum number of user-defined axioms is %d",TMAX);
     paws();
     return(0);
  }
  got_formula(0,i,"axiom");
}


/**********************************************************/

bad_guy()        /*** Take user definition of a formula
                      to go in failure.                 ***/
{ 
   got_formula(1,0,"formula");
}


/*********************************************************/

connective()    /*** Take definition of an operator in
                     response to menu option "c".      ***/
{ int i,j;
  char c;

  for ( i = 0; theJob->defcon[i] && i<CMAX; i++ ) ;
  if (i==CMAX) 
  { 
     printf("\n\n Maximum number of definitions is %d", CMAX);
     paws();
     return(0);
  }
  printf("\n\n Type the new connective:  ");
  fflush(stdout); scanf("%c", &c); READLN
  if ( strchr("&v~->o)(.fpqrstabFT",c) || strchr(theJob->dcs,c) )
  {
     printf("\n No fair: \"%c\" already means something.",c);
     paws(); return(0);
  }
  else if ( noclear ) printf("\n Accepted !!\n");
  printf("\n What is the adicity of %c  ", c);
  fflush(stdout); scanf("%d", theJob->adicity+i); READLN
  if ( theJob->adicity[i]<0 || theJob->adicity[i]>2 )
  { 
     printf("\n No fair: adicity must be 0, 1 or 2.");
     paws(); return(0);
  }
  if ( !theJob->adicity[i] ) printf("\n Define %c   ", c);
  else if ( theJob->adicity[i] == 1 ) printf("\n Define %ca   ", c);
  else printf("\n Define a %c b   ", c);
  fflush(stdout);
  theJob->defcon[i] = 0;
  if ( got_formula(2,i,"definition") )
  { 
     for ( j = 0; theJob->symbols[theJob->adicity[i]][j] != ' '; j++ ) ; 
     theJob->symbols[theJob->adicity[i]][j] = c;
     if ( !theJob->adicity[i] ) theJob->form[8+i].sym = c;
     theJob->dcs[i] = c;  theJob->dcs[i+1] = '\0';
  }
}

/**********************************************************/


got_formula(x,y,s)  int x; char *s;   /*** What it says ***/
{ 
   int rc;
   
   while (1) switch( infml(x,y) )
   {
      case -1: return(0);
      case 0:  return(1);
      case 1:  printf("\n H)elp, R)epeat %s or N)either?   ", s);
               switch(readin("hnr"))
               { 
                  case 'n': return(0);
                  case 'h': help(x+1); break;
                  case 'r': printf("\n Definition:   ");  fflush(stdout);
               }
   }
}



/***********************************************************/

deletion()              /*** Response to menu option "d" ***/
{ int i,j;

  printf("\n Delete (a) pre-defined axiom?");
  printf("\n        (b) bad guy?");
  printf("\n        (c) user-defined axiom?    ");
  switch( readin("abc") )
  { 
     case 'a': j = 0; 
               for ( i = 1; i < AXMAX; i++ ) 
               if ( theJob->axiom[i] )
               { 
                  if ( j ) j = AXMAX;
                  else j = i;
               }
               if ( j )
               { 
                  if ( j < AXMAX ) theJob->axiom[j] = 0;
                  else
                  { 
                     for ( i = 1; i < AXMAX; i++ ) 
                     if ( theJob->axiom[i] )
                     { 
                        printf("\n %2d  ", i);
                        print_axiom(stdout,i); 
                     }
                     printf("\n\n Delete which one?    "); fflush(stdout);
                     scanf("%d", &i);  READLN
                     if ( i > 0 && i < AXMAX ) theJob->axiom[i] = 0;
                  }
               }
               break;
     case 'b': theJob->failure = 0;  break;
     case 'c': if ( *(theJob->root) )
               { 
                  if ( theJob->root[1] )
                  { 
                     for ( i = 0; theJob->root[i]; i++ )
                     { 
                        printf("\n %d  ", i+1);
                        outfml(theJob->form+theJob->root[i],
                               theJob->form+theJob->root[i],stdout);
                     }
                     printf("\n\n Delete which one?   ");
                     fflush(stdout); scanf("%d", &j); READLN
                  }
                  else i = j = 1;
                  for ( ; j > 0 && j <= i; j++ ) 
                  theJob->root[j-1] = theJob->root[j]; 
               }
  }
}



          /**************************************/

fragment()
{
  if ( noclear)
  {
     printf("\n\n Select which connectives you want\n\n");
     printf(" ~        (y/n) "); theJob->f_n = ( readin("yn") == 'y' );
     printf(" & and v  (y/n) "); theJob->f_lat = ( readin("yn") == 'y' );
     printf(" t        (y/n) "); theJob->f_t = ( readin("yn") == 'y' );
     printf(" T        (y/n) "); theJob->f_T = ( readin("yn") == 'y' );
     printf(" F        (y/n) "); theJob->f_F = ( readin("yn") == 'y' );
     printf(" o        (y/n) "); theJob->f_fus = ( readin("yn") == 'y' );
  }
  else
  {
     printf("\n\n Do you want negation defined? (y/n)    ");
     theJob->f_n = ( readin("yn") == 'y' );
     printf("\n Do you want & and v defined? (y/n)     ");
     theJob->f_lat = ( readin("yn") == 'y' );
     if ( theJob->f_lat ) theJob->f_t = 1; else
     {
        printf("\n Do you want constant t defined? (y/n)  ");
        theJob->f_t = ( readin("yn") == 'y' );
     }
     if ( theJob->f_lat ) theJob->f_T = theJob->f_F = 1; else
     {
        printf("\n Do you want constant T defined? (y/n)  ");
        theJob->f_T = ( readin("yn") == 'y' );
        if ( theJob->f_T && theJob->f_n ) theJob->f_F = 1; else
        {
           printf("\n Do you want constant F defined? (y/n)  ");
           theJob->f_F = ( readin("yn") == 'y' );
        }
     }
     if ( theJob->f_n && (theJob->logic == RW || 
                       theJob->logic == R  || theJob->logic == CK) )
     theJob->f_fus = 1;
     else
     {
        printf("\n Do you want fusion o defined? (y/n)    ");
        theJob->f_fus = ( readin("yn") == 'y' );
     }
  }
}
              



/***********************************************************/

logic_choice()
{ char glc;

  theJob->logic = -1;  theJob->totord = 0;
  printf("\n\n What is your favourite logic?  ");  fflush(stdout);
  gets(theJob->logic_name);
  trim();
  theJob->logic = strpos(theJob->logic_name, LOGICS);
  if ( theJob->logic >= 0 ) return(1);
  if ( *(theJob->logic_name)=='L' || *(theJob->logic_name)=='T' )
  theJob->logic = strpos(theJob->logic_name+1, LOGICS);
  if ( theJob->logic >= 0 ) 
  {
     theJob->totord = (*(theJob->logic_name)=='T');  return(1);
  }
  printf(
  "\n\n There is no such logic as \"%s\".\n",theJob->logic_name);
  printf("\n Logics are %s\n\n",LOGICS);
  printf(
 " Prefix \"L\" for no distribution, \"T\" for total order.");
  printf("\n\n\n H)elp or R)eselect?    ");
  if ( readin("hr") == 'h' ) 
  {
     help(3); paws();
     help(4); paws();
     help(5);
  }
  logic_choice();
}



/**********************************************************/

IO_setting()           /*** Response to menu option "i" ***/
{ char oc;

  printf("\n\n"); 
  do { 
        printf(
        "\n Tty:   P)retty  U)gly  S)ummary  N)one  H)elp    ");
        oc = readin("pusnh");
        theJob->tty_out = oc=='u'? UGLY: (oc=='p'? PRETTY: 
                                    (oc=='s'? SUMMARY: NONE));
        if (oc=='h') help(6);
     }
  while ( oc == 'h' );
  do { 
        printf(
        "\n File:  P)retty  U)gly  S)ummary  N)one  H)elp    ");
        oc = readin("pusnh");
        theJob->fil_out = oc=='u'? UGLY: (oc=='p'? PRETTY: 
                                   (oc=='s'? SUMMARY: NONE));
        if ( oc == 'h' ) help(6);
     }
  while ( oc == 'h' );
  if (!theJob->fil_out) return(0);
  if ( *(theJob->outfil_name) )
  { 
     printf(" New output file? (y/n)   ");
     if ( readin("yn") == 'n' ) return(0);
  }
  if ( filing ) { fclose(outfil); filing = 0; }
  do { 
        printf(" \n Name output file:   "); fflush(stdout);
        gets(theJob->outfil_name);
     }
  while ( !*(theJob->outfil_name) );
} 



/**********************************************************/

jump_condition()       /*** Response to menu option "j" ***/
{ char oc;

  printf("\n Shall I stop when:");
  printf(" (a) I'm exhausted?\n");
  printf("%20c(b) time's up?\n", ' ');
  printf("%20c(c) I've found enough matrices?\n", ' ');
  printf("%20c(d) the matrices get too big?\n", ' ');
  printf("%20c(e) a combination of the above?        ", ' ');
  oc = readin("abcde");
  theJob->sizmax = Sizmax;  
  theJob->maxtime = theJob->maxmat = 0;  
  theJob->sizmax_ismax = 1;
  switch( oc )
  { 
     case 'c': printf("\n How many is enough?  "); 
               fflush(stdout); scanf("%d", &(theJob->maxmat));  
               if ( theJob->maxmat < 0 ) theJob->maxmat = 0; break;
     case 'd': printf("\n How big is big enough?  ");
               fflush(stdout);  scanf("%d", &(theJob->sizmax)); 
               if ( theJob->sizmax > 1 ) theJob->sizmax_ismax = 0; break;
     case 'e': printf("\n How many matrices are enough?  "); 
               fflush(stdout); scanf("%d", &(theJob->maxmat));  
               if ( theJob->maxmat < 0 ) theJob->maxmat = 0;
               printf("\n How big can they get?          ");
               fflush(stdout);  scanf("%d", &(theJob->sizmax));
               if ( theJob->sizmax > 1 ) theJob->sizmax_ismax = 0;
     case 'b': printf("\n How many seconds have I got?   ");
               fflush(stdout);  scanf("%d", &(theJob->maxtime)); 
               if ( theJob->maxtime < 5 ) theJob->maxtime = 0; break;
  }
}


/***********************************************************/

n_of_procs()               /*** In the parallel version, return the new
                                choice of number of processes.  In the 
                                serial version, return -1 (nonsense) ***/
{
   char *npcp;
   int i;
   
#ifdef PARALLEL
   npcp = strchr(answer,'#');
   while ( *npcp && ( *npcp < '0' || *npcp > '9' )) npcp++;
   if ( !*npcp ) return(gm->nprocs);
   i = 0;
   do {
         i = i*10 + *npcp - '0';
         npcp++;
      }
   while ( *npcp >= '0' && *npcp <= '9' );
   if ( i < 2  || i > PARALLEL )
   {
      printf("\n Number of processes must be in range 2 - %d\n\n",
                 PARALLEL);
      paws();
      return(gm->nprocs);
   }
#else
   i = -1;
#endif
   return(i);
}


/***********************************************************/

print_axiom(f,x)  FILE *f; int x;     /*** Axiom #x to f ***/
{
  if ( noclear ) fprintf(f, "%2d   ", x);
  switch( x )
  { 
     case AxX:   fprintf(f, "p v ~p");               break;
     case AxBA:  fprintf(f, "(p & ~p) -> q");        break;
     case AxSBA: fprintf(f, "(p & ~p) -> (q v ~q)"); break;
     case AxW2:  fprintf(f, "(p & (p -> q)) -> q");  break;
     case AxK:   fprintf(f, "p -> (q -> p)");        break;
     case AxK2:  fprintf(f, "p -> (q -> q)");        break;
     case AxM:   fprintf(f, "p -> (p -> p)");        break;
     case AxRED: fprintf(f, "(p -> ~p) -> ~p");      break;
     case AxC3:  fprintf(f, "(t -> p) -> p");        break;
     case AxCt:  fprintf(f, "p -> (t -> p)");        break;
     case Axat:  fprintf(f, "p v (p -> q)");         break;
     case AxTF:  fprintf(f, "T -> (F -> F)");        break;
     case AxB:   fprintf(f, 
                       "(q -> r) -> ((p -> q) -> (p -> r))"); 
                 break;
     case AxB2:  fprintf(f, 
                       "(p -> q) -> ((q -> r) -> (p -> r))"); 
                 break;
     case AxC2: fprintf(f, "p -> ((p -> q) -> q)"); break;
     case AxW:  fprintf(f, 
                        "(p -> (p -> q)) -> (p -> q)"); break;
     case AxC:  fprintf(f, 
                        "(p -> (q -> r)) -> (q -> (p -> r))");
                break;
     case AxWB: fprintf(f, 
                        "((p -> q) & (q -> r)) -> (p -> r)");
  }
}



/**********************************************************/

display()    /*** Show the current choices and the menu ***/
{ 
  if ( !noclear ) system( "clear" );
  disp(stdout);
  printf("    A)xiom    B)adguy    C)onnective   D)elete\n");
  printf("    E)xit     F)ragment  G)enerate     H)elp\n"); 
  printf("    I)O       J)ump      K)ill         L)ogic      ");
}


/**********************************************************/

disp(f)  FILE *f;
{ int i,j = 0;

#ifdef PARALLEL
  fprintf(f, "\n Parallel MaGIC running %d out of %d processes\n", 
           gm->nprocs, PARALLEL);
#endif
 
  fprintf(f, "\n Logic:%8c%s", ' ', theJob->logic_name);
  
  for ( i = 1; i < AXMAX; i++ ) if ( theJob->axiom[i] )
  { 
     if ( !j )
     { 
        j = 1; fprintf(f, "\n\n Plus:         ");
     }
     else fprintf(f, "\n               ");
     print_axiom(f,i);
  }
  
  for ( i = 0; theJob->root[i]; i++ )
  { 
     if ( i ) fprintf(f, "\n               "); 
     else   fprintf(f, "\n\n Extra:        ", i+1);
     outfml(theJob->form+theJob->root[i],
            theJob->form+theJob->root[i],f);
  }
  
  fprintf(f, "\n\n Fragment:     ->");
  if ( theJob->f_lat ) fprintf(f, ", &, v");
  if ( theJob->f_n ) fprintf(f, ", ~");
  if ( theJob->f_fus ) fprintf(f, ", o");
  if ( theJob->f_t ) 
  { 
     fprintf(f, ", t"); 
     if ( theJob->f_n ) fprintf(f, ", f");
  }
  if ( theJob->f_T ) fprintf(f, ", T");
  if ( theJob->f_F ) fprintf(f, ", F");
  
  for ( i = 0; theJob->defcon[i]; i++ )
  { 
     if ( i ) fprintf(f, "\n             ");
     else fprintf(f, "\n\n Definitions:");
     if ( !theJob->adicity[i] ) 
     fprintf(f, "  %c        ", theJob->dcs[i]);
     else if ( theJob->adicity[i]==1 ) 
     fprintf(f, "  %ca       ", theJob->dcs[i]);
     else fprintf(f, "  a %c b    ", theJob->dcs[i]);
     outfml(theJob->form+theJob->defcon[i],
            theJob->form+theJob->defcon[i],f);
  }

  if ( theJob->failure )
  { 
     fprintf(f, "\n\n Fail:         ");
     outfml(theJob->form+theJob->failure, 
            theJob->form+theJob->failure, f);
  }
  
  fprintf(f, "\n\n TTY output:   %s\n File output:  %s",
   (theJob->tty_out==NONE? "none": 
   (theJob->tty_out==UGLY? "ugly": 
   (theJob->tty_out==PRETTY? "pretty": "summary"))), 
   (theJob->fil_out==NONE? "none": 
   (theJob->fil_out==UGLY? "ugly": 
   (theJob->fil_out==PRETTY? "pretty": "summary"))));
  if ( theJob->fil_out ) 
  fprintf(f,"\n Output file:  \"%s\"", theJob->outfil_name);
  
  fprintf(f, "\n\n Search concludes ");
  if (theJob->maxtime) fprintf(f, "after %d second%s\n or ", 
               theJob->maxtime, (theJob->maxtime==1? "": "s"));
  if (theJob->maxmat)  fprintf(f, "when %d matri%s found\n or ", 
               theJob->maxmat, (theJob->maxmat==1? "x": "ces"));
  fprintf(f, "when size %d finished.\n\n\n", theJob->sizmax);
}



/**********************************************************/

help( x )  int x;     /*** Transfer some text to screen ***/
{ 
  switch( x )
  { 
     case 0: put_out("MEN.show");  break;
     case 1: 
     case 2: put_out("WFF.show");  break;
     case 3: put_out("FDL.show");  break;
     case 4: put_out("BTW.show");  break;
     case 5: put_out("LOG.show");  break;
     case 6: put_out("OUT.show");
  }
}

/***********************************************************/

put_out( f_nm )  char f_nm[];        /*** Show file f_nm ***/
{
   char s[50], *t;
  int i,j=0;

  if ( noclear ) return(0);
  system( "clear" );
  t = "more ";
  for ( i = 0; t[i]; i++ ) s[j++] = t[i];
  t = DATA_DIR;
  for ( i = 0; t[i]; i++ ) s[j++] = t[i];
  while ( s[j++] = *f_nm++ ) ;
  system( s );
}

/***********************************************************/

infml(x,y)  int x,y;   /*** Input a formula from stdin.  
                            x is the destination: 0=axiom,
                            1=badguy 2=definition.  y is
                            the offset for x==0 or x==2. 
                            Return 0 iff successful     ***/
{ int i, j;
  WFF *wf;
  char fml[80];

  if ( x != 2 ) printf("\n\n Enter formula (or RETURN):  ");
  fflush(stdout);
  gets(answer);
  j = 0;
  for ( i = 0; answer[i]; i++ )
  if (    strchr(")(.~&vo>ftFT", answer[i]) 
       || strchr(theJob->dcs, answer[i]) 
     || ( strchr("pqrst", answer[i]) && x < 2 ) 
     || ( answer[i] == 'a' && x == 2 && theJob->adicity[y] )
     || ( answer[i] == 'b' && x == 2 && theJob->adicity[y] == 2 ))
  fml[j++] = answer[i];
  else if ( !strchr(" -", answer[i]) ) 
  {
     printf(
     "\n Illegal input: unrecognised symbol %c\n\n ", answer[i]);
     for ( j = 0; j < i; j++ ) printf(" "); printf("!\n ");
     printf(answer); printf("\n\n");
     return( 1 );
  }
  for ( i = j; fml[i]; i++ ) fml[i] = '\0';
  if ( !j ) return(-1);
  if ( x == 2 )
  {
     if ( j == 1 )
     {
        printf("\n ERROR: definition is too short!\n\n");
        return(1);
     }
     if ( theJob->adicity[y] && !strchr(fml,'a') )
     {
  printf("\n ERROR: variable \"a\" does not occurin the definition\n\n");
        return(1);
     }
     if ( theJob->adicity[y] == 2 && !strchr(fml,'b') )
     {
  printf("\n ERROR: variable \"b\" does not occur in the definition\n\n");
        return(1);
     }
  }
  wf = parse(fml,theJob->form,theJob->symbols);
  if ( !wf ) return(1);
  if ( !x )          theJob->root[y] = wf-theJob->form;
  else if ( x == 1 ) theJob->failure = wf-theJob->form;
  else             { 
                     fix_atoms(y,wf);
                     theJob->defcon[y] = wf-theJob->form;
                   }
  return(0);
}



/**********************************************************/

fix_atoms(y,dy)  int y; WFF *dy;     /*** Change occurrences of 
                                      'a' and 'b' in the definition
                                      of defined connective #y to
                                      its own atom[0] and atom[1] ***/
{
   if ( !dy ) return(0);
   if ( dy->lsub )
   {
      if ( dy->lsub->sym == 'a' ) 
           dy->lsub = theJob->form+theJob->atom[0][y];
      else if ( dy->lsub->sym == 'b' ) 
           dy->lsub = theJob->form+theJob->atom[1][y];
      else fix_atoms(y,dy->lsub);
   }
   if ( dy->rsub )
   {
      if ( dy->rsub->sym == 'a' ) 
           dy->rsub = theJob->form+theJob->atom[0][y];
      else if ( dy->rsub->sym == 'b' ) 
           dy->rsub = theJob->form+theJob->atom[1][y];
      else fix_atoms(y,dy->rsub);
   }
}


/*******************************************************/

outfml(p,q,f)  WFF *p, *q; FILE *f;
               /*** Print subformula rooted at p to f 
                    Note q is the root of a formula  ***/
{ int i,j,k;
  char c;

  c = p->sym; k = -1;
  for ( j = 0; theJob->dcs[j]; j++ )
  if ( c == theJob->dcs[j] )
  { 
     k = theJob->adicity[j]; break; 
  }
  if ( c == '&' || c=='v' || c=='>' || c=='o' || k==2 )
  { 
     if ( p != q ) fprintf( f, "(" );
     outfml(p->lsub,q,f); fprintf( f, " " );
     if ( c == '>' ) fprintf( f, "-" );
     fprintf( f, "%c ", c );
     outfml(p->rsub,q,f);
     if ( p != q ) fprintf( f, ")" );
  }
  else
  { 
     fprintf( f, "%c", c );
     if ( c == '~' || k == 1 )
     outfml(p->rsub,q,f);
  }
}