/* Parser for .log files, C hand-coded version.
   Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*/
#include <stdlib.h>
#include <stddef.h>
#include <stdio.h>
#include <string.h>
#ifdef HAVE_LIBZ
#include <zlib.h>
typedef gzFile fp;
#else
typedef FILE *fp;
#endif
#include "cproof.tab.h"

#ifdef HAVE_LIBZ
extern fp yygzin;
#define YYIN yygzin
#else
extern FILE *yyin;
#define YYIN yyin
#endif
extern FILE *yyout;
extern char *yytext;
extern int yyleng;

void *xmalloc (size_t n)
{
  void *p = malloc (n);

  if (p==NULL)
    {
      fprintf (stderr, "No more memory allocating %ld bytes.\n", n);
      fflush (stderr);
      exit (10);
    }
  return p;
}

#define CHUNK_SIZE 8192
char *endPtr = NULL;
char *curPtr = NULL;

void *small_alloc (size_t n)
{
#define SMALL_CHUNK 4
  /* should be a multiple of 4, so that pointers to such blocks have
     two free low bits. */
  size_t m = ((n+SMALL_CHUNK-1)/SMALL_CHUNK)*SMALL_CHUNK;
  char *p;

  if (curPtr==NULL || curPtr+m>endPtr)
    {
      p = xmalloc (CHUNK_SIZE);
      endPtr = p+CHUNK_SIZE;
      if (((long)p) & 1)
	p++;
      if (((long)p) & 2)
	p += 2;
      /* round p to a multiple of 4 */
      curPtr = p;
    }
  p = curPtr;
  curPtr = p+m;
  return (void *)p;
}

char bsd_cursors[] = { '-', '\\', '|', '/' };

struct bsd_cursor {
  int time;
};

#define BSD_CURSOR(name) struct bsd_cursor name = { -1, }

void bump_bsd_cursor (struct bsd_cursor *cur)
{
  if (cur->time<0)
    ;
  else fputc (8, stderr);
  if (++cur->time==4)
    cur->time = 0;
  fputc (bsd_cursors [cur->time], stderr);
  fflush (stderr);
}

int verbose = 0;
long nClauses = 0;
#define CLAUSE_STEP 1000
long nClausesMod = 0;

long nDeds = 0;

#define yyerror(msg) yy_error (msg)

void yy_error (/*int l1, int c1, int l2, int c2,*/
	       char *msg)
{
  fputs (msg, stderr);
  if (yytext[0]!=0)
    {
      fputs (" (at '", stderr);
      fputs (yytext, stderr);
      fputs ("')", stderr);
    }
  fputc ('\n', stderr);
  fflush (stderr);
}

#define PHASE_SKIP_INTRO 0
#define PHASE_GET_DEPS 1
#define PHASE_COPY_INTRO 2
#define PHASE_OUT_REACHABLE 3

int phase = PHASE_SKIP_INTRO;
int out_prems = 0;

#define BUFFER_SIZE 256

struct buffer {
  size_t size;
  size_t len;
  char s[BUFFER_SIZE];
};

struct buffer *new_buf (void)
{
  struct buffer *b = xmalloc (sizeof(struct buffer));

  b->size = BUFFER_SIZE;
  b->len = 0;
  return b;
}

void bput (struct buffer **bp, char *s, int n)
{
  switch (phase)
    {
    case PHASE_SKIP_INTRO: break;
    case PHASE_GET_DEPS: break;
    case PHASE_COPY_INTRO:
      fputs (s, yyout);
      break;
    default:
      {
	struct buffer *b = *bp;
	int newlen = b->len + n;

	if (newlen>=b->size)
	  {
	    size_t newsize = newlen + BUFFER_SIZE;
	    struct buffer *newb = xmalloc (offsetof(struct buffer, s[newsize]));
	    
	    newb->size = newsize;
	    newb->len = newlen;
	    memcpy (newb->s, b->s, b->len);
	    strcpy (newb->s+b->len, s);
	    *bp = newb;
	    free (b);
	  }
	else
	  {
	    strcpy (b->s+b->len, s);
	    b->len = newlen;
	  }
	break;
      }
    }
}

struct buffer **theBufp = NULL;

struct header {
  unsigned long bits;
#define H_CONS 0
#define H_STRING 1
#define KIND(h) ((h).bits & 1)
#define SETKIND(h,k) { if (k) (h).bits |= 1; else (h).bits &= ~1; }
#define MARK(h) ((h).bits & 2)
#define SETMARK(h,k) { if (k) (h).bits |= 2; else (h).bits &= ~2; }
#define N(h) (((h).bits & ~3) >> 2)
#define SETN(h,i) (h).bits = ((i) << 2) | ((h).bits & 3)
};

struct cinfo {
  struct header h;
  struct cinfo *next;
  struct cons *conc;
  struct cons *prem[1];
};

struct cons {
  struct header h;
  struct cons *next;
  /*struct header *car;*/
#define CAR(c) (struct header *)((c)->h.bits & ~3)
#define SETCAR(c,hdr) (c)->h.bits = ((long)hdr) | ((c)->h.bits & 3)
  struct cons *cdr;
};

struct cons *nil;

struct string {
  struct header h;
  struct string *next;
  char s[1];
};

struct ilist {
  struct ilist *next;
  struct cons *i;
};

struct ilist *thePremList = NULL;
struct ilist *theTargets = NULL;

struct ilist *icons (struct cons *i, struct ilist *next)
{
  struct ilist *il;

  if (thePremList==NULL)
    {
      struct ilist* il = xmalloc (sizeof(struct ilist));

      il->next = NULL;
      thePremList = il;
    }
  il = thePremList;
  thePremList = il->next;
  il->next = next;
  il->i = i;
  return il;
}

unsigned int ilen (struct ilist *il)
{
  unsigned int n;

  for (n=0; il!=NULL; n++, il=il->next);
  return n;
}

void ifree (struct ilist *il)
{
  struct ilist *next, *il0=il;

  if (il==NULL)
    return;
  while ((next = il->next)!=NULL)
    il = next;
  il->next = thePremList;
  thePremList = il0;
}

#define NLOWBITS 2

unsigned long pgcd (unsigned long i, unsigned long j)
{
  unsigned long k, r;

  if (i<j)
    {
      k = i;
      i = j;
      j = k;
    }
  while (j!=0)
    {
      r = i % j;
      i = j;
      j = r;
    }
  return i;
}

unsigned long nCons = 0L;
unsigned long cons_hash_size = 42043;
#define cons_hashcode1(car,cdr,siz) \
	(((231*(unsigned long)car) + ((unsigned long)cdr)) >> NLOWBITS) % (siz)
#define cons_hashcode(car,cdr) cons_hashcode1(car,cdr,cons_hash_size)
struct cons **consTable = NULL;

int expandConsTable (unsigned long size)
{
  struct cons **newConsTable;
  struct cons **src_ap, **app, *ap;
  unsigned long h1, j, h2;
  unsigned long d, p2;
  struct cons ***epp;

  d = pgcd (size, cons_hash_size);
  p2 = size/d;
  epp = (struct cons ***)xmalloc (p2 * sizeof (struct cons **));
  newConsTable = (struct cons **)malloc (size*sizeof(struct cons *));
  if (newConsTable==NULL)
    {
      free (epp);
      return 0;
    }
  for (h1=0, src_ap = consTable; h1<cons_hash_size; h1++, src_ap++)
    {
      for (j=0, h2=h1; j<p2; j++)
	{
	  epp [j] = &newConsTable[h2];
	  h2 += d;
	  if (h2>size)
	    h2 -= size;
	}
      for (ap = *src_ap; ap!=NULL; ap=ap->next)
	{
	  h2 = cons_hashcode1(CAR(ap),ap->cdr,size);
	  if (h2<h1)
	    j = (h2-h1)/d + p2;
	  else j = (h2-h1)/d;
	  *epp [j] = ap;
	  epp [j] = &ap->next;
	}
      for (j=0; j<p2; j++)
	*epp[j] = NULL;
    }
  free (consTable);
  consTable = newConsTable;
  cons_hash_size = size;
  free (epp);
  return 1;
}

#define CONS_N 1024

struct conschunk {
  struct cons m[CONS_N];
};

struct cons *newcons (void)
{
  return (struct cons *)small_alloc (sizeof(struct cons));
}

struct cons *kons (struct header *car, struct cons *cdr)
{
  struct cons **epp0;

  if (nCons>2*cons_hash_size)
    expandConsTable (2*cons_hash_size);
  epp0 = &consTable[cons_hashcode(car,cdr)];
  {
    struct cons *ep;

    for (ep = *epp0; ep!=NULL; ep = ep->next)
      {
	if (cdr==ep->cdr && car==CAR(ep))
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (cdr==ep->cdr && car==CAR(ep))
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (cdr==ep->cdr && car==CAR(ep))
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (cdr==ep->cdr && car==CAR(ep))
	  return ep;
      }
  }
  nCons++;
  {
    struct cons *ep = newcons ();

    ep->h.bits = H_CONS;
    /*
      ep->h.kind = H_CONS;
      ep->h.mark = 0;
      ep->h.n = 0;
    */
    ep->next = *epp0;
    SETCAR(ep, car);
    ep->cdr = cdr;
    *epp0 = ep;
    return ep;
  }
}

unsigned long nStrings = 0L;
unsigned long string_hash_size = 883;

unsigned long string_hashcode1(char *s, unsigned long siz)
{
  unsigned long i = 0;
  unsigned long c;

  while ((c = (unsigned long)(unsigned char)*s++)!=0)
    {
      i = 71 * i + c + 13;
    }
  return i % siz;
}
#define string_hashcode(s) string_hashcode1(s,string_hash_size)
struct string **stringTable = NULL;

int expandStringTable (unsigned long size)
{
  struct string **newStringTable;
  struct string **src_ap, **app, *ap;
  unsigned long h1, j, h2;
  unsigned long d, p2;
  struct string ***epp;

  d = pgcd (size, string_hash_size);
  p2 = size/d;
  epp = (struct string ***)xmalloc (p2 * sizeof (struct string **));
  newStringTable = (struct string **)malloc (size*sizeof(struct string *));
  if (newStringTable==NULL)
    {
      free (epp);
      return 0;
    }
  for (h1=0, src_ap = stringTable; h1<string_hash_size; h1++, src_ap++)
    {
      for (j=0, h2=h1; j<p2; j++)
	{
	  epp [j] = &newStringTable[h2];
	  h2 += d;
	  if (h2>size)
	    h2 -= size;
	}
      for (ap = *src_ap; ap!=NULL; ap=ap->next)
	{
	  h2 = string_hashcode1(ap->s,size);
	  if (h2<h1)
	    j = (h2-h1)/d + p2;
	  else j = (h2-h1)/d;
	  *epp [j] = ap;
	  epp [j] = &ap->next;
	}
      for (j=0; j<p2; j++)
	*epp[j] = NULL;
    }
  free (stringTable);
  stringTable = newStringTable;
  string_hash_size = size;
  free (epp);
  return 1;
}

struct string *kstring (char *s)
{
  struct string **epp0;

  if (nStrings>string_hash_size)
    expandStringTable (2*string_hash_size);
  epp0 = &stringTable[string_hashcode(s)];
  {
    struct string *ep;

    for (ep = *epp0; ep!=NULL; ep = ep->next)
      {
	if (strcmp (s, ep->s)==0)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (strcmp (s, ep->s)==0)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (strcmp (s, ep->s)==0)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (strcmp (s, ep->s)==0)
	  return ep;
      }
  }
  nStrings++;
  {
    struct string *ep = xmalloc (offsetof (struct string, s[strlen(s)+1]));

    ep->h.bits = H_STRING;
    /*
      ep->h.kind = H_STRING;
      ep->h.mark = 0;
      ep->h.n = 0;
    */
    ep->next = *epp0;
    strcpy (ep->s, s);
    *epp0 = ep;
    return ep;
  }
}

unsigned long nCinfos = 0L;
unsigned long cinfo_hash_size = 15581;
#define cinfo_hashcode1(conc,siz) (((unsigned long)conc) >> NLOWBITS) % (siz)
#define cinfo_hashcode(conc) cinfo_hashcode1(conc,cinfo_hash_size)
struct cinfo **cinfoTable = NULL;;

int expandCinfoTable (unsigned long size)
{
  struct cinfo **newCinfoTable;
  struct cinfo **src_ap, **app, *ap;
  unsigned long h1, j, h2;
  unsigned long d, p2;
  struct cinfo ***epp;

  d = pgcd (size, cinfo_hash_size);
  p2 = size/d;
  epp = (struct cinfo ***)xmalloc (p2 * sizeof (struct cinfo **));
  newCinfoTable = (struct cinfo **)malloc (size*sizeof(struct cinfo *));
  if (newCinfoTable==NULL)
    {
      free (epp);
      return 0;
    }
  for (h1=0, src_ap = cinfoTable; h1<cinfo_hash_size; h1++, src_ap++)
    {
      for (j=0, h2=h1; j<p2; j++)
	{
	  epp [j] = &newCinfoTable[h2];
	  h2 += d;
	  if (h2>size)
	    h2 -= size;
	}
      for (ap = *src_ap; ap!=NULL; ap=ap->next)
	{
	  h2 = cinfo_hashcode1(ap->conc,size);
	  if (h2<h1)
	    j = (h2-h1)/d + p2;
	  else j = (h2-h1)/d;
	  *epp [j] = ap;
	  epp [j] = &ap->next;
	}
      for (j=0; j<p2; j++)
	*epp[j] = NULL;
    }
  free (cinfoTable);
  cinfoTable = newCinfoTable;
  cinfo_hash_size = size;
  free (epp);
  return 1;
}

BSD_CURSOR(clauseCursor);

void new_clause (void)
{
  nClauses++;
  if (verbose>=2 && ++nClausesMod==CLAUSE_STEP)
    {
      nClausesMod = 0;
      bump_bsd_cursor (&clauseCursor);
    }
}

struct cinfo *getkinfo (struct cons *conc)
{
  struct cinfo *ep = cinfoTable[cinfo_hashcode(conc)];

  for (; ep!=NULL; ep = ep->next)
    {
      if (conc==ep->conc)
	return ep;
      ep = ep->next; /* unroll loop. */
      if (ep==NULL)
	break;
      if (conc==ep->conc)
	return ep;
      ep = ep->next; /* unroll loop. */
      if (ep==NULL)
	break;
      if (conc==ep->conc)
	return ep;
      ep = ep->next; /* unroll loop. */
      if (ep==NULL)
	break;
      if (conc==ep->conc)
	return ep;
    }
  return NULL;
}

struct cinfo *kinfo (struct cons *conc, struct ilist *il)
{
  struct cinfo **epp0;

  if (nCinfos>32*cinfo_hash_size)
    expandCinfoTable (2*cinfo_hash_size);
  epp0 = &cinfoTable[cinfo_hashcode(conc)];
  {
    struct cinfo *ep;

    for (ep = *epp0; ep!=NULL; ep = ep->next)
      {
	if (conc==ep->conc)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (conc==ep->conc)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (conc==ep->conc)
	  return ep;
	ep = ep->next; /* unroll loop. */
	if (ep==NULL)
	  break;
	if (conc==ep->conc)
	  return ep;
      }
  }
  nCinfos++;
  new_clause ();
  {
    unsigned int n = ilen (il);
    struct cinfo *ep = small_alloc (offsetof (struct cinfo, prem[n]));
    struct cons **ip;

    ep->h.bits = 0;
    SETN(ep->h,n);
    /*
      ep->h.kind = 0;
      ep->h.mark = 0;
      ep->h.n = n;
    */
    ep->next = *epp0;
    ep->conc = conc;
    for (ip=ep->prem; il!=NULL; il=il->next)
      *ip++ = il->i;
    *epp0 = ep;
    return ep;
  }
}

#define TARGET_FALSE (0x1)
#define TARGET_Q (0x2)
#define TARGET_AUTO (0x10)
int target_flags = TARGET_FALSE;

int target_p (struct cons *clause)
{
  /* By default, target is "false".
     That is, either a clause of the form '?.' or
     one of the form '#false([^()]*).'. */
  struct cons *head = (struct cons *)CAR(clause);

  if (target_flags & TARGET_FALSE)
    {
      if (head==nil)
	return 1;
      if (KIND(head->h)==H_STRING && memcmp (((struct string *)head)->s, "#false", 6)==0
	  && clause->cdr==nil)
	return 1;
    }
  if (target_flags & TARGET_Q)
    {
      if (head==nil)
	;
      else if (KIND(head->h)==H_STRING && memcmp (((struct string *)head)->s, "#ne", 3)==0
	       && clause->cdr==nil)
	return 1;
    }
  if (target_flags & TARGET_AUTO)
    {
      if (head==nil)
	;
      else if (KIND(head->h)==H_STRING)
	{
	  if (clause->cdr==nil)
	    return 1;
	}
      else if (KIND(head->h)==H_CONS && head->cdr!=nil)
	{ /* head is P (...) */
	  struct cons *xl = NULL;

	  if (head->cdr->cdr==nil)
	    { /* head is P (t) */
	      struct cons *t = (struct cons *)CAR(head->cdr);

	      if (KIND(t->h)==H_STRING) /* head is P (X) */
		{
		  if (clause->cdr==nil)
		    return 1; /* universal clauses P(X). are marked */
		}
	      else if (KIND(*CAR(t))==H_STRING) /* head is P (f (t1, ..., tn)), t=f(t1,...,tn) */
		xl = t->cdr;
	    }
	  else xl = head->cdr; /* head is P (t1, ..., tn). */
	  if (xl!=NULL)
	    {
	      struct cons *ll;

	      for (ll=xl; ll!=nil; ll=ll->cdr)
		{
		  struct string *x = (struct string *)CAR(ll);

		  if (KIND(x->h)!=H_STRING || MARK(x->h))
		    break; /* fail if some ti is not a variable, or is a duplicate variable. */
		  else SETMARK(x->h,1); /* mark the variables free in the head. */
		}
	      if (ll==nil) /* every ti is a variable. */
		{
		  struct cons *body;

		  for (body = clause->cdr; body!=nil; body=body->cdr)
		    {
		      struct cons *a = (struct cons *)CAR(body);
		      struct header *arg;

		      if (KIND(a->h)!=H_CONS)
			break;
		      a = a->cdr;
		      if (KIND(a->h)!=H_CONS)
			break;
		      if (a->cdr!=nil)
			break;
		      /* here a=Q(arg) */
		      arg = CAR(a);
		      if (KIND(*arg)!=H_STRING)
			break;
		      /* here a=Q(arg), where arg is a variable X. */
		      if (!MARK(*arg))
			break;
		      /* here a=Q(X) with X free in the head, so great. */
		    }
		  for (ll=xl; ll!=nil; ll=ll->cdr)
		    {
		      struct string *x = (struct string *)CAR(ll);

		      if (KIND(x->h)==H_STRING)
			SETMARK(x->h, 0); /* unmark the variables free in the head. */
		    }
		  if (body==nil)
		    return 1; /* OK, this is an automaton clause. */
		}
	      else for (ll=xl; ll!=nil; ll=ll->cdr)
		{
		  struct string *x = (struct string *)CAR(ll);

		  if (KIND(x->h)==H_STRING)
		    SETMARK(x->h, 0); /* unmark the variables free in the head. */
		}
	    }
	}
    }
  return 0;
}

int lookahead = -1;
extern int yylex(void);

int lex (void)
{
  int token;

  if (lookahead!=-1)
    {
      token = lookahead;
      lookahead = -1;
    }
  else token = yylex ();
  return token;
}

void unlex (int token)
{
  lookahead = token;
}

int lalex (void)
{
  int token;

  if (lookahead!=-1)
    return lookahead;
  return (lookahead = yylex ());
}

static const char *const yytname[] =
{
  "$", "error", "$undefined.", "identifier", "open_paren", 
  "close_paren", "provided", "comma", "semicolon", 
  "period", "question_mark", "subst", "open_source", 
  "close_source", "open_clause", "close_clause", "end_tag", 
  "open_definitions", "close_definitions", "open_approximation", 
  "close_approximation", "open_justifications", 
  "close_justifications", "VAR", "ne", "false", 
  "string_constant", "axiom", "open_rule", "clause_def", 
  "clause_use", "close_rule", "problem", "source", "definitions", 
  "approximation", "justifications", "deductions", "named_clause_list", 
  "named_clause", "deduction_list", "deduction", "premise_list", 
  "premise", "processed_clause", "substitution", "clause_list", "clause", 
  "raw_clause", "head", "atomhead", "clause_body", 
  "non_empty_clause_body", "atom", "@1", "term_list", "term", 
  "application", "id", "var", "ne", "false", "open_paren", "close_paren", 
  "comma", "semicolon", "period", "provided", "question_mark", "axiom", 
  "open_rule", "close_rule", "open_clause", "close_clause", "end_tag", 
  "string", "open_source", "close_source", "open_definitions", 
  "close_definitions", "open_approximation", "close_approximation", 
  "open_justifications", "close_justifications", 0
};

void yy_expected (int token, int expected[])
{
  char buf[1024];
  char *s;
  int *exp;
  int etok;
  char *delim = "expected ";

  for (s=buf, exp=expected; (etok = *exp++)!=0; )
    {
      strcpy (s, delim);
      delim = " or ";
      s += strlen (s);
      strcpy (s, yytname[etok-254]);
      s += strlen (s);
    }
  sprintf (s, ", got %s", yytname[token-254]);
  yy_error (buf);
  exit (2);
}

struct cons *parse_term_list (void);

struct header *parse_term (void)
{
  int token;

  token = lex ();
  switch (token)
    {
    case VAR:
      bput (theBufp, yytext, yyleng); 
      return (struct header *)(out_prems?NULL:kstring (yytext));
    case identifier:
      {
	struct string *s;

	bput (theBufp, yytext, yyleng);
	s = out_prems?NULL:kstring (yytext);
	token = lex ();
	if (token==kw_open_paren)
	  {
	    struct cons *tl;

	    bput (theBufp, yytext, yyleng);
	    tl = parse_term_list ();
	    token = lex ();
	    if (token!=kw_close_paren)
	      {
		int expected[] = { kw_close_paren, 0 };

		yy_expected (token, expected);
	      }
	    bput (theBufp, yytext, yyleng);
	    /*parse_close_paren ();*/
	    return (struct header *)(out_prems?NULL:kons ((struct header *)s, tl));
	  }
	else
	  {
	    unlex (token);
	    return (struct header *)s;
	  }
      }
    default:
      {
	int expected[] = { VAR, identifier, 0 };

	yy_expected (token, expected);
	return NULL;
      }
    }
}

struct cons *parse_term_list (void)
{
  int token;
  struct header *t;
  struct cons *tl;

  t = parse_term ();
  tl = out_prems?NULL:kons (t, nil);
  while ((token = lex ())==kw_comma)
    {
      bput (theBufp, yytext, yyleng);
      /* bput (theBufp, ", ", 2); */
      t = parse_term ();
      tl = out_prems?NULL:kons (t, tl);
    }
  unlex (token);
  return tl;
}

struct header *parse_atom (int finals[])
{
  int token;

  token = lex ();
  switch (token)
    {
    case kw_ne:
      bput (theBufp, yytext, yyleng);
      return (struct header *)(out_prems?NULL:kstring (yytext));
    case identifier:
      {
	struct string *s;
	int *fp,final;

	bput (theBufp, yytext, yyleng);
	s = out_prems?NULL:kstring (yytext);
	token = lex ();
	if (token==kw_open_paren)
	  {
	    struct cons *tl;

	    bput (theBufp, yytext, yyleng);
	    tl = parse_term_list ();
	    token = lex ();
	    if (token!=kw_close_paren)
	      {
		int expected[] = { kw_close_paren, 0 };

		yy_expected (token, expected);
	      }
	    bput (theBufp, yytext, yyleng);
	    /*parse_close_paren ();*/
	    if (out_prems)
	      return NULL;
	    else /*if ($3->cdr==nil)
		   return (struct header *)kons ((struct header *)s, (struct cons *)CAR(tl));
		   else*/
	      return (struct header *)kons ((struct header *)s, tl);
	  }
	else
	  {
	    unlex (token);
	    for (fp=finals; (final = *fp++)!=0; )
	      if (final==token)
		break;
	    if (final==0)
	      {
		struct header *t;

		bput (theBufp, " ", 1);
		t = parse_term ();
		return out_prems?NULL:
		  ((struct header *)
		   kons ((struct header *)s,
			 kons (t, nil)
			 ));
	      }
	    else return (struct header *)s;
	  }
      }
    default:
      {
	int expected[] = { kw_ne, identifier, 0 };

	yy_expected (token, expected);
	return NULL;
      }
    }
}

struct cons *parse_non_empty_clause_body (int final)
{
  int token;
  struct cons *body;
  struct header *a;
  int finals[] = { final, kw_comma, 0 };

  a = parse_atom (finals);
  body = out_prems?NULL:kons ((struct header *)a, nil);
  while ((token = lex ())==kw_comma)
    {
      bput (theBufp, yytext, yyleng);
      /* bput (theBufp, ", ", 2); */
      a = parse_atom (finals);
      body = out_prems?NULL:kons ((struct header *)a, body);
    }
  if (token!=final)
    {
      int expected[] = { final, 0 };

      yy_expected (token, expected);
    }
  bput (theBufp, yytext, yyleng);
  return body;
}

struct cons *parse_clause_body (int final)
{
  int token;

  if ((token = lex ())!=final)
    {
      unlex (token);
      return parse_non_empty_clause_body (final);
    }
  else return nil;
}

struct header *parse_atomhead (int finals[])
{
  int token;

  token = lex ();
  if (token==kw_false)
    {
      bput (theBufp, yytext, yyleng);
      return (struct header *)(out_prems?NULL:kstring (yytext));
    }
  unlex (token);
  return parse_atom (finals);
}

struct header *parse_head (int finals[])
{
  int token;
  struct header *head, *next;

  head = parse_atomhead (finals);
  while ((token = lex ())==kw_semicolon)
    {
      bput (theBufp, ";", 1);
      next = parse_atomhead (finals);
      head = out_prems?NULL:((struct header *)
			     kons ((struct header *)kstring ("#or"),
				   kons(head, kons(next, nil))));
    }
  unlex (token);
  return head;
}

struct cons *parse_clause (void)
{
  int token;
  struct cons *body;
  struct header *head;
  int finals[] = { kw_semicolon, kw_provided, kw_period, 0 };

  switch (token = lex ())
    {
    case kw_question_mark:
      bput (theBufp, yytext, yyleng);
      body = parse_clause_body (kw_period);
      bput (theBufp, yytext, yyleng);
      /*parse_period ();*/
      return out_prems?NULL:kons ((struct header *)nil, body);
    default:
      unlex (token);
      head = parse_head (finals);
      token = lex ();
      switch (token)
	{
	case kw_provided:
	  bput (theBufp, " :- ", 4);
	  body = parse_clause_body (kw_period);
	  return out_prems?NULL:kons ((struct header *)head, body);
	case kw_period:
	  bput (theBufp, yytext, yyleng);
	  return out_prems?NULL:kons ((struct header *)head, nil);
	default:
	  {
	    int expected[] = { kw_provided, kw_period, 0 };

	    yy_expected (token, expected);
	    return NULL;
	  }
	}
    }
}

void parse_clause_list (int final)
{
  int token;

  while ((token = lex ())!=final)
    {
      unlex (token);
      (void) parse_clause ();
      switch (phase)
	{
	case PHASE_COPY_INTRO: bput (theBufp, "\n", 1); break;
	case PHASE_GET_DEPS: break;
	}
    }
}

void parse_substitution (void)
{
  int token;

  token = lex ();
  if (token==kw_subst)
    {
      if (phase==PHASE_GET_DEPS)
	(*theBufp)->len = 0;
      else bput (theBufp, yytext, yyleng);
    }
  else unlex (token);
}

struct cons *parse_processed_clause (void)
{
  struct cons *clause;

  clause = parse_clause ();
  switch (phase)
    {
    case PHASE_GET_DEPS:
      (*theBufp)->len = 0;
      /*fallthrough*/
    case PHASE_OUT_REACHABLE:
      return clause;
    default:
      return NULL;
    } 
}

struct cons *parse_premise (void)
{
  struct cons *clause;

  clause = parse_processed_clause ();
  parse_substitution ();
  if (phase==PHASE_GET_DEPS)
    {
      (*theBufp)->len = 0;
    }
  else bput (theBufp, "\n  ", 3);
  return clause;
}

struct ilist *parse_premise_list (int final)
{
  int token;
  struct cons *clause;
  struct ilist *il = NULL;
  
  clause = parse_premise ();
  if (phase==PHASE_GET_DEPS)
    il = icons (clause, NULL);
  while ((token = lex ())!=final)
    {
      unlex (token);
      clause = parse_premise ();
      if (phase==PHASE_GET_DEPS)
	il = icons (clause, il);
    }
  return il;
}

void parse_deduction (void)
{
  int token;
  struct cons *clause;

  clause = parse_processed_clause ();
  token = lex ();
  switch (token)
    {
    case kw_axiom:
      {
	bput (theBufp, yytext, yyleng);
	bput (theBufp, "\n", 1);
	switch (phase)
	  {
	  case PHASE_GET_DEPS:
	    {
	      (void) kinfo (clause, NULL);
	      if (target_p (clause))
		{
		  theTargets = icons (clause, theTargets);
		}
	      nDeds++;
	      break;
	    }
	  case PHASE_OUT_REACHABLE:
	    {
	      struct cinfo *ci = getkinfo (clause);

	      if (ci!=NULL && MARK(ci->h))
		{
		  fputs ((*theBufp)->s, yyout);
		  SETMARK(ci->h, 0); /* we are happy with the first deduction of the clause,
					and won't output any other. */
		}
	      new_clause ();
	    }
	    break;
	  }
	(*theBufp)->len = 0;
	break;
      }
    case kw_open_rule:
      {
	struct ilist *prems;

	bput (theBufp, yytext, yyleng);
	bput (theBufp, "\n  ", 3);
	if (phase==PHASE_OUT_REACHABLE) out_prems = 1;
	if (phase==PHASE_GET_DEPS) (*theBufp)->len = 0;
	prems = parse_premise_list (kw_close_rule);
	bput (theBufp, yytext, yyleng);
	bput (theBufp, "\n", 1);
	out_prems = 0;
	/*parse_close_rule ();*/
	switch (phase)
	  {
	  case PHASE_GET_DEPS:
	    {
	      (void) kinfo (clause, prems);
	      ifree (prems);
	      if (target_p (clause))
		{
		  theTargets = icons (clause, theTargets);
		}
	      nDeds++;
	      break;
	    }
	  case PHASE_OUT_REACHABLE:
	    {
	      struct cinfo *ci = getkinfo (clause);

	      if (ci!=NULL && MARK(ci->h))
		{
		  fputs ((*theBufp)->s, yyout);
		  SETMARK(ci->h, 0); /* we are happy with the first deduction of the clause,
					and won't output any other. */
		}
	      new_clause ();
	    }
	    break;
	  }
	(*theBufp)->len = 0;
	break;
      }
    default:
      {
	int expected[] = { kw_axiom, kw_open_rule, 0 };

	yy_expected (token, expected);
	break;
      }
    }
}

void parse_deduction_list (int final)
{
  int token;

  while ((token = lex ())!=final)
    {
      unlex (token);
      parse_deduction ();
    }
}

void parse_open_clause (void)
{
  int token = lex ();

  if (token==kw_open_clause)
    {
      bput (theBufp, yytext, yyleng);
    }
  else
    {
      int expected[] = { kw_open_clause, 0 };

      yy_expected (token, expected);
    }
}

void parse_string (void)
{
  int token = lex ();

  if (token==string_constant)
    {
      bput (theBufp, yytext, yyleng);
    }
  else
    {
      int expected[] = { string_constant, 0 };

      yy_expected (token, expected);
    }
}

void parse_end_tag (void)
{
  int token = lex ();

  if (token==kw_end_tag)
    {
      bput (theBufp, yytext, yyleng);
    }
  else
    {
      int expected[] = { kw_end_tag, 0 };

      yy_expected (token, expected);
    }
}

void parse_close_clause (void)
{
  int token = lex ();

  if (token==kw_close_clause)
    {
      bput (theBufp, yytext, yyleng);
      bput (theBufp, "\n", 1);
    }
  else
    {
      int expected[] = { kw_close_clause, 0 };

      yy_expected (token, expected);
    }
}

void parse_named_clause (void)
{
  parse_open_clause ();
  parse_string ();
  parse_end_tag ();
  parse_clause ();
  parse_close_clause ();
}

void parse_named_clause_list (int final)
{
  int token;

  while ((token = lex ())!=final)
    {
      unlex (token);
      parse_named_clause ();
    }
}

void parse_deductions (void)
{
  parse_deduction_list (0);
}

void parse_open_justifications (void)
{
  int token = lex ();

  if (token==kw_open_justifications)
    {
      bput (theBufp, yytext, yyleng);
      bput (theBufp, "\n", 1);
    }
  else
    {
      int expected[] = { kw_open_justifications, 0 };

      yy_expected (token, expected);
    }
}

void parse_justifications (void)
{
  parse_open_justifications ();
  parse_deduction_list (kw_close_justifications);
  bput (theBufp, yytext, yyleng);
  bput (theBufp, "\n", 1);
  switch (phase)
    {
    case PHASE_SKIP_INTRO: phase = PHASE_GET_DEPS; break;
    case PHASE_COPY_INTRO: phase = PHASE_OUT_REACHABLE; break;
    }
  /*parse_close_justifications ();*/
}

void parse_open_approximation (void)
{
  int token = lex ();

  if (token==kw_open_approximation)
    {
      bput (theBufp, yytext, yyleng);
      bput (theBufp, "\n", 1);
    }
  else
    {
      int expected[] = { kw_open_approximation, 0 };

      yy_expected (token, expected);
    }
}

void parse_approximation (void)
{
  parse_open_approximation ();
  parse_clause_list (kw_close_approximation);
  bput (theBufp, yytext, yyleng);
  bput (theBufp, "\n", 1);
  /*parse_close_approximation ();*/
}

void parse_open_definitions (void)
{
  int token = lex ();

  if (token==kw_open_definitions)
    {
      bput (theBufp, yytext, yyleng);
      bput (theBufp, "\n", 1);
    }
  else
    {
      int expected[] = { kw_open_definitions, 0 };

      yy_expected (token, expected);
    }
}

void parse_definitions (void)
{
  parse_open_definitions ();
  parse_clause_list (kw_close_definitions);
  bput (theBufp, yytext, yyleng);
  bput (theBufp, "\n", 1);
  /*parse_close_definitions ();*/
}

void parse_open_source (void)
{
  int token = lex ();

  if (token==kw_open_source)
    {
      bput (theBufp, yytext, yyleng);
    }
  else
    {
      int expected[] = { kw_open_source, 0 };

      yy_expected (token, expected);
    }
}

void parse_source (void)
{
  parse_open_source ();
  parse_named_clause_list (kw_close_source);
  bput (theBufp, yytext, yyleng);
  bput (theBufp, "\n", 1);
  /*parse_close_source ();*/
}

void parse_problem (void)
{
  parse_source ();
  parse_definitions ();
  parse_approximation ();
  parse_justifications ();
  parse_deductions ();
  switch (phase)
    {
    case PHASE_GET_DEPS: phase = PHASE_COPY_INTRO; break;
    case PHASE_OUT_REACHABLE: phase = PHASE_SKIP_INTRO; break;
    }
}

long nMarks = 0;
#define MARKS_STEP 1000
long nMarksMod = 0;

BSD_CURSOR(marksCursor);

void mark (struct cons *i)
{
  struct cinfo *ci = getkinfo (i);
  unsigned int k, n;

  if (ci==NULL)
    return;
  if (MARK(ci->h)) /* already marked */
    return;
  SETMARK(ci->h, 1);
  nMarks++;
  if (verbose>=2 && ++nMarksMod==MARKS_STEP)
    {
      nMarksMod = 0;
      bump_bsd_cursor (&marksCursor);
    }
  n = N(ci->h);
  for (k=0; k<n; k++)
    mark (ci->prem[k]);
}

void stringify (char *to, char *from)
{
  char c;

  *to++ = '"';
  while ((c = *from++)!=0)
    {
      switch (c)
	{
	case '"': case '\\':
	  *to++ = '\\';
	  *to++ = c;
	  break;
	default:
	  *to++ = c;
	  break;
	}
    }
  *to++ = '"';
  *to = 0;
}

int gz (char *s)
{
  int len = strlen (s);

  return (len>=3 && strcmp (s+len-3, ".gz")==0);
}

fp hopen (char *name)
{
  char *cmd;
  fp f;

#ifdef HAVE_LIBZ
  f = gzopen (name, "r");
#else
  cmd = xmalloc (16 + 2*strlen (name));
  strcpy (cmd, "zcat ");
  stringify (cmd+strlen(cmd), name);
  if (gz (name))
    f = popen (cmd, "r");
  else f = fopen (name, "r");
  free (cmd);
#endif
  return f;
}

void hclose (char *name, fp f)
{
#ifdef HAVE_LIBZ
  gzclose (f);
#else
  if (gz (name))
    pclose (f);
  else fclose (f);
#endif
}

void usage (void)
{
  fputs ("Usage: h1logstrip <flags*> filename.\n"
	 "Version 1.0, Copyright (C) Jean Goubault-Larrecq;\n"
	 "     see file COPYRIGHT.\n"
	 "  h1logstrip comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.\n"
	 "  This is free software, and you are welcome to redistribute it\n"
	 "  under certain conditions; see TERMS AND CONDITIONS in file COPYING.\n"
	 "  Filename is <name>.log or <name>.log.gz.\n"
	 "  Flags are:\n"
	 "    -h prints this help.\n"
	 "    -v0 runs silently, -v1 (aka., -v) and -v2 are more verbose\n"
	 "    -false outputs all contradictions and their proofs;\n"
	 "       -no-false disables this option.  Default: -false.\n"
	 "    -auto outputs all automaton clauses and their proofs;\n"
	 "       -no-auto disables this option.  Default: -no-auto.\n"
	 "    -ne outputs all non-emptiness clauses #ne(...) and their proofs;\n"
	 "       -no-ne disables this option.  Default: -no-ne.\n",
	 stderr
	 );
  fflush (stderr);
}

int main (int argc, char **argv)
{
  struct buffer *buf = new_buf ();
  char *name;
  fp f;
  int i;

  for (i=1; i<argc; i++)
    {
      if (strcmp (argv[i], "-h")==0)
	{
	  usage ();
	  if (i+1==argc)
	    exit (0);
	}
      else if (argv[i][0]=='-' && argv[i][1]=='v')
	{
	  if (argv[i][2]==0)
	    verbose = 1;
	  else if (sscanf (&argv[i][2], "%d", &verbose)!=1)
	    {
	      fprintf (stderr, "Expected verbosity level (integer) after -v.\n");
	      fflush (stderr);
	      exit (2);
	    }
	}
      else if (strcmp (argv[i], "-no-false")==0)
	target_flags &= ~TARGET_FALSE;
      else if (strcmp (argv[i], "-false")==0)
	target_flags |= TARGET_FALSE;
      else if (strcmp (argv[i], "-no-auto")==0)
	target_flags &= ~TARGET_AUTO;
      else if (strcmp (argv[i], "-auto")==0)
	target_flags |= TARGET_AUTO;
      else if (strcmp (argv[i], "-no-ne")==0)
	target_flags &= ~TARGET_Q;
      else if (strcmp (argv[i], "-ne")==0)
	target_flags |= TARGET_Q;
      else break;
    }
  if (i>=argc)
    {
      fprintf (stderr, "Missing filename.\n");
      usage ();
      exit (2);
    }
  /* Initialization */
  consTable = xmalloc (cons_hash_size * sizeof (struct cons *));
  stringTable = xmalloc (string_hash_size * sizeof (struct string *));
  cinfoTable = xmalloc (cinfo_hash_size * sizeof (struct cinfo *));
  nil = small_alloc (sizeof (struct cinfo));
  nil->h.bits = 0;
  /*
  nil->h.kind = 0;
  nil->h.mark = 0;
  nil->h.n = 0;
  */
  nil->next = NULL;
  SETCAR(nil, NULL);
  nil->cdr = NULL;
  /* Now open files: let's go. */
  name = argv[i];
  f = hopen (name);
  if (f==NULL)
    {
      perror (argv[0]);
      fprintf (stderr, " (file %s).\n", name);
      exit (10);
    }
  YYIN = f;
  theBufp = &buf;
  if (verbose>=1)
    {
      fprintf (stderr, "Scanning ... ");
      fflush (stderr);
    }
  parse_problem ();
  hclose (name, f);
  if (verbose>=1)
    {
      fprintf (stderr, "%c done: %ld deduction steps, %ld clauses.\n", 8, nDeds, nClauses
	       /*, ((double) nTableRecords) / ((double) nHash)*/);
      fflush (stderr);
    }
  {
    struct ilist *il;

    if (verbose>=1)
      {
	fprintf (stderr, "Marking ... ");
	fflush (stderr);
      }
    for (il = theTargets; il!=NULL; il=il->next)
      mark (il->i);
    ifree (theTargets);
    theTargets = NULL;
  }
  if (verbose>=1)
    {
      fprintf (stderr, "%c done: %ld live clauses.\n", 8, nMarks);
      fflush (stderr);
    }
  f = hopen (name);
  if (f==NULL)
    {
      perror (argv[0]);
      fprintf (stderr, " (file %s).\n", name);
      exit (10);
    }
  YYIN = f;
  if (verbose>=1)
    {
      fprintf (stderr, "Outputting ... ");
      fflush (stderr);
      clauseCursor.time = -1;
    }
  parse_problem ();
  hclose (name, f);
  if (verbose>=1)
    {
      fprintf (stderr, "%c done.\n", 8);
      fflush (stderr);
    }
  return 0;
}
