/*---------------------------------------------------------------------------

             Resolution theorem proving program based on CGPP,
                  the connection graph proof procedure.

  Independent Study Project, CSci 8599Y
  University of Minnesota, Fall quarter 1991

  Author:       John Henckel
  Advisor:      James Slagle

--------------------------------------------------------------------------*/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "glob.h"

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

#ifdef C2

#define INCL_DOSMEMMGR
#include <os2.h>

void *mymalloc(unsigned short x)
{
  int rc;
  void *p;

  OFFSETOF(p)=0;
  rc = DosAllocSeg(x,&SELECTOROF(p),0);
  if (rc) printf("error in alloc\n");
  if (rc) return NULL;
  return p;
}

void *myrealloc(void *Ptr,unsigned short x)
{
  int rc;

  if (OFFSETOF(Ptr)) printf("Invalid pointer in realloc\n");
  if (Ptr == NULL)
    rc = DosAllocSeg(x,&SELECTOROF(Ptr),0);
  else
    rc = DosReallocSeg(x,SELECTOROF(Ptr));
  if (rc) printf("error in realloc\n");
  if (rc) return NULL;
  return Ptr;
}

unsigned myfree(void *Ptr)
{
  if (OFFSETOF(Ptr)) printf("Invalid pointer in Free\n");
  else DosFreeSeg(SELECTOROF(Ptr));
  return 0 ;
}

#endif
/***********************************************************************/


#define MAXC 20
enum cmd_type { S=1,Q,H,PROOF,CONT,LINK,DEL,LIST,SET,REM,
                READ,WRITE,NEW,END,ENDF,HELP };

static int cmd[MAXC];

int InitConst(void)
{
  memset(cmd,0,sizeof(cmd));
  cmd[S     ] = AddSymbol("s");
  cmd[Q     ] = AddSymbol("q");
  cmd[H     ] = AddSymbol("h");
  cmd[PROOF ] = AddSymbol("proof");
  cmd[CONT  ] = AddSymbol("cont");
  cmd[LINK  ] = AddSymbol("link");
  cmd[DEL   ] = AddSymbol("del");
  cmd[LIST  ] = AddSymbol("list");
  cmd[SET   ] = AddSymbol("set");
  cmd[REM   ] = AddSymbol("*");
  cmd[READ  ] = AddSymbol("read");
  cmd[WRITE ] = AddSymbol("write");
  cmd[NEW   ] = AddSymbol("new");
  cmd[END   ] = AddSymbol("end");
  cmd[ENDF  ] = AddSymbol("eof");
  cmd[HELP  ] = AddSymbol("help");
}

int Command(int c)
{
  int i;

  for (i=0; i<MAXC; ++i)
    if (cmd[i]==c) return i;
  return 0;
}

/*---------------------------------------------------------------------------
  Macros used by main
*/
#define d1_PrintLox(t) if (debug) { printf("After pars: "); \
    PrintLox(t); printf("\n"); }
#define d2_PrintLox(t) if (debug) { printf("After ccnf: "); \
    PrintLox(t); printf("\n"); }


/*---------------------------------------------------------------------------
    M A I N
*/
char line[256];

int main(int argc, char *argv[])
{
  lox *t,*t2;
  graph *gr1;
  int c,i;
  int topic,ask,debug,occur;
  clause *cl,*mt;
  char *s;

  topic = 1;
  ask = 50;
  debug = 0;
  occur = 3;    /* depth of the occurs check */
  mt = NULL;

#ifndef C2
  clrscrn();
#endif
  printf("\n");
  printf("\n");
  printf("             Resolution theorem proving program based on CGPP,\n");
  printf("                  the connection graph proof procedure.\n");
  printf("\n");
  printf("  Independent Study Project, CSci 8599Y\n");
  printf("  University of Minnesota, Fall quarter 1991\n");
  printf("\n");
  printf("  Author:       John Henckel\n");
  printf("  Advisor:      James Slagle\n");
  printf("\n");
  printf("  For a list of commands type help.\n");
  printf("\n");

  NewSymTable();
  InitParser();
  InitConst();
  gr1 = NewGraph("Main Graph");

  while (1) {
    printf("\n=> ");
    switch (Command(c=GetToken())) {
    case S:
      t = ParseLox();
      d1_PrintLox(t);
      ConvertCNF(t);
      cl = Clausify(t);
      d2_PrintLox(t);
      AddClauses(gr1,cl,topic,0);
      AddStrucs(t);
      break;
    case Q:
      t = ParseLox();
      d1_PrintLox(t);
      t2 = Negate(DeepCopyLox(t));
      ConvertCNF(t2);
      cl = Clausify(t2);
      d2_PrintLox(t2);
      AddClauses(gr1,cl,topic,1);
      AddStrucs(t2);
      BuildGraphLinks(gr1);
      mt = FindProof(gr1,ask,debug,occur);
      if (mt==NULL) printf("No proof found.\n");
      else if (mt->numtins) printf("The answer is no.\n");
      else printf("The answer is yes.\n");
      break;
    case H:
      t = ParseLox();
      d1_PrintLox(t);
      ConvertCNF(t);
      cl = Clausify(t);
      d2_PrintLox(t);
      AddClauses(gr1,cl,topic,1);
      AddStrucs(t);
      break;
    case PROOF:
      if (mt==NULL) printf("No proof.\n");
      else DisplayProof(mt);
      break;
    case CONT:
      mt = FindProof(gr1,ask,debug,occur);
      if (mt==NULL) printf("No proof found.\n");
      else if (mt->numtins) printf("The answer is no.\n");
      else printf("The answer is yes.\n");
      break;
    case LINK:
      BuildGraphLinks(gr1);
      printf("Graph links built.\n");
      break;
    case DEL:
      GetLine(line);
      c = 0;
      sscanf(line,"%d",&c);
      c=RemoveClauses(gr1,c);
      printf("There were %d clauses deleted.\n",c);
      break;
    case LIST:
      if (debug) DumpGraph(gr1);
      else PrintGraph(gr1);
      break;
    case SET:
      s = GetSymbol(GetToken());
      if (!strcmp(s,"debug")) { GetLine(line); sscanf(line,"%d",&debug); }
      if (!strcmp(s,"occur")) { GetLine(line); sscanf(line,"%d",&occur); }
      if (!strcmp(s,"topic")) { GetLine(line); sscanf(line,"%d",&topic); }
      if (!strcmp(s,"ask"  )) { GetLine(line); sscanf(line,"%d",&ask  ); }
      break;
    case REM:
      GetLine(line);
      break;
    case READ:
      SetSrc(GetSymbol(GetToken()));
      break;
    case WRITE:
      printf("This does one resolution step.\n");
      mt = FindProof(gr1,1,0,occur);
      if (mt==NULL) printf("No proof found.\n");
      else if (mt->numtins) printf("The answer is no.\n");
      else printf("The answer is yes.\n");
      break;
    case NEW:
      ReleaseGraph(gr1);
      gr1 = NewGraph("Main Graph");
      break;
    case END:
      printf("\n\nProgram is ending.\n\n");
      exit(EXIT_SUCCESS);
      break;
    case ENDF:
      SetSrc("stdin");
      break;
    case HELP:
      printf("\n\nThe valid commands are: ");
      for (i=1; i<MAXC; ++i)
        if (cmd[i]) printf("%s, ",GetSymbol(cmd[i]));
      printf("\n");
      break;
    default:
      eprintf("Error unknown command '%.10s'",GetSymbol(c),0,0);
      GetLine(line);
    }
  }
}