%{
#include <stdarg.h>
#include <stdio.h>
#include <ctype.h>
#include <stdlib.h>
#include <string.h>
#include <search.h>
#include <assert.h>

#define YYSTYPE char *
void prttok(FILE *iop, int type, YYSTYPE val);
#define YYPRINT(file, type, value) prttok(file, type, value)

char **fstk[512], ***topstk = fstk;
char *toklst[256], **toktop;
char labbuf[256];
size_t yyleng; /* Length of the token currently processed (without \0) */
int line = 1;

#define PRESENT 0x01
#define ACTIVE 0x02

struct symbol {
	struct symbol *next;
	char ty;
	unsigned flg;
};

void yyerror(const char *fmt, ...)
{
	va_list ap;
	fprintf(stderr, "%d: ", line);
	va_start(ap, fmt);
	vfprintf(stderr, fmt, ap);
	va_end(ap);
	fprintf(stderr, "\n");
}

char ***pushstk(char **p)
{
	if (topstk == fstk + sizeof fstk / sizeof *fstk)
		return NULL;
	*topstk++ = p;
	return topstk;
}

void popstk(void)
{
	while (topstk > fstk && *--topstk != NULL) {
		/* Remove nonterminal symbol association. */
		if ((*topstk)[1][1] == 'f') {
			register struct symbol *sym = (struct 
				symbol *)((*topstk)[3] - sizeof *sym);
			sym->flg &= ~ACTIVE;
		}
		free(*topstk);
	}
}
void dumplst(FILE *iop, char **q)
{
	if (!*q)
		return;
	fprintf(iop, "\"%s\"", *q);
	while (*++q)
		fprintf(iop, ", \"%s\"", *q);
}
void dumpstk(void)
{
	char ***p;
	for (p = fstk; p < topstk; p++) {
		if (!*p) {
			fprintf(stderr, "---------\n");
			continue;
		}
		fprintf(stderr, "<%s, ", (*p)[0] ? (*p)[0] : "<>");
		dumplst(stderr, *p + 1);
		fprintf(stderr, ">\n");
	}
}

void printnt(char *s)
{
	/* Print a yacc style nonterminal */
	char *graph = "-|"; /* Characters yacc can't handle in NT idents */
	char *replac[] = {"mt", "st"}; /* replacement for them */
	while (*s) {
		char *t = strchr(graph, *s);
		if (t)
			fputs(replac[t - graph], stdout);
		else
			putchar(*s);
		s++;
	}
}

void printt(char *s)
{
	/* print a yacc style string terminal.*/
	putchar('\"');
	while (*s) {
		if (*s == '\\' || *s == '\"')
			putchar('\\');
		putchar(*s++);
	}
	putchar('\"');
}

int yylex(void);
%}

%token TOKEN

%%
stmlst	: stmt
	| stmlst stmt
	;

stortk	: TOKEN {
		/* Store token */
		struct symbol *sym;
		ENTRY e = {$1, NULL}, *ep;
		if ((ep = hsearch(e, FIND))) {
			sym = ep->data;
			$$ = ep->key;
			if (sym->ty == $-1[1])
				break;
			yyerror("duplicate declaration of %s", $1);
			YYERROR;
		}
		sym = e.data = malloc(yyleng + 1 + sizeof *sym);
		e.key = (char *)e.data + sizeof *sym;
		strcpy(e.key, $1);
		sym->next = NULL;
		sym->ty = $-1[1];
		sym->flg = 0;
		if (!hsearch(e, ENTER)) {
			free(sym);
			yyerror("hash table overflow storing %s.", $1);
			YYERROR;
		}
		$$ = e.key;
	}
	;
retrtk	: TOKEN {
		/* Retrieve token */
		ENTRY e = {$1, NULL}, *ep;
		if (!(ep = hsearch(e, FIND))) {
			dumpstk();
			yyerror("token %s found undeclared", $1);
			YYERROR;
		}
		assert(ep->data == (struct symbol *)(ep->key 
			- sizeof (struct symbol)));
		$$ = ep->key;
	}
	;
initok	: /* EMPTY */ {
		toktop = toklst;
	}
	;
puttok	: /* EMPTY */ {
		if (toktop == toklst + sizeof toklst / sizeof *toklst) {
			yyerror("token buffer overflow.");
			YYERROR;
		}
		*toktop++ = $0;
	}
	;
stklst	: initok stortk puttok
	| stklst stortk puttok
	;
rtklst	: initok retrtk puttok
	| rtklst retrtk puttok
	;

label	: TOKEN {
		$$ = strcpy(labbuf, $1);
	}
	;
proof	: rtklst '=' TOKEN
	| proof TOKEN
	;
lnull	: /* EMPTY */ {
		/* Null label */
		$$ = NULL;
	}
	;
putstk	: /* EMPTY */ {
		/* Put statement on stack.
		 *
		 * expects <label> <stmt> <list> '.' on top of semantic stack.
		 * puts <<list>, <label>> onto statement stack.
		 */
		void *mem = malloc((toktop - toklst + 3) * sizeof *toktop
			+ ($-3 ? strlen($-3) + 1 : 0));
		if (!pushstk(mem)) {
			dumpstk();
			yyerror("stack overflow.");
			YYERROR;
		}
		topstk[-1][0] = $-3 ? strcpy((char *)mem
			+ (toktop - toklst + 3) 
			* sizeof *toktop, $-3) : NULL;
		topstk[-1][1] = $-2;
		memcpy(topstk[-1] + 2, toklst, 
			(toktop - toklst) * sizeof *toktop);
		topstk[-1][toktop - toklst + 2] = NULL;
#if 0
		{
			char **q;
			fprintf(stderr, "::: %s, %s", topstk[-1][0], 
				topstk[-1][1]);
			for (q = topstk[-1] + 2; *q; q++)
				fprintf(stderr, ", \"%s\"", *q);
			fprintf(stderr, "\n");
		}
#endif
	}
	;
stmt	: lnull 'c' stklst '.' putstk
	| lnull 'v' stklst '.' putstk
	| lnull 'd' rtklst '.' putstk
	| label 'f' rtklst '.' putstk {
		/* Generate rule toklst[0]->toklst[1] */
		struct symbol *left = (struct symbol *)(toklst[0] 
			- sizeof *left),
			*right = (struct symbol *)(toklst[1] - sizeof *right);
		if (toktop - toklst != 2 || left->ty != 'c' 
		 || right->ty != 'v' || (right->flg & ACTIVE))
		{
			yyerror("bad $f format.");
			YYERROR;
		}
		if (!right->next) {
			right->next = left;
			printf("/* %s */ ", $1);
			printnt(toklst[0]);
			printf(": ");
			printt(toklst[1]);
			printf(";\n");
		} else if (right->next != left) {
			yyerror("globally contradicting $f hypothesis");
			YYERROR;
		}
		right->flg |= ACTIVE;
	}
	| label 'e' rtklst '.' putstk
	| label 'a' rtklst '.' {
		/* Generate rule toklst[0]->var2nt(toklst[1] ...)  */ 
		char ***curr, **t;
		unsigned int dstcon = 0, equcon = 0, ntsyms = 0, nhyps = 0;
		struct symbol *sym;
		/* Search token list for equality constraints and 
		 * terminal symbol variables.  Mark used tokens.  
		 */
		for (t = toklst; t < toktop; t++) {
			sym = (struct symbol *)(*t - sizeof *sym);

			/* Is the token a variable? */
			if (sym->ty != 'v')
				continue;

			equcon += !!(sym->flg & PRESENT);
			ntsyms += !sym->next;
			sym->flg |= PRESENT;
		}
		/* Search stack for matching inequality constraints.
		 * Count hypotheses.
		 */
		for (curr = fstk; curr < topstk; curr++) {
			/* distinct variables present from current group. */
			unsigned int dstgrp = 0;
			if (!*curr)
				continue;
			nhyps += (*curr)[1][1] == 'e'; /* Count hypotheses. */
			if ((*curr)[1][1] != 'd')
				continue;
			for (t = *curr + 2; *t; t++) {
				sym = (struct symbol *)(*t - sizeof *sym);
				dstgrp += !!(sym->flg & PRESENT);
			}
			/* If more than one variable from a distinct group
			 * is present in the token list, then the 
			 * constraining condition of the group has an effect.
			 */
			dstcon += dstgrp > 1;
		}
		sym = *toklst ? (struct symbol *)(*toklst - sizeof *sym) : NULL;
		if (!sym || sym->ty != 'c') {
			yyerror("bad $a format.  (rule %s.)", $1);
			YYERROR;
		}
		
		printf("/* %s */ ", $1);
		if (nhyps || dstcon || equcon)
			printf("/* not context free (%u, %u, %u) */ ",
				nhyps, dstcon, equcon);
		if (ntsyms)
			printf("/* unresolved (%u) */ ", ntsyms);

		printnt(*toklst);
		putchar(':');
		
		/* Output rule */
		for (t = toklst + 1; t < toktop; t++) {
			sym = (struct symbol *)(*t - sizeof *sym);
			sym->flg &= ~PRESENT; /* Unmark token */
			/* If constant or bogus variable, simply output.
			 * For variables, output non-terminal.
			 */
			putchar(' ');
			if (sym->ty == 'v' && sym->next)
				printnt((char *)sym->next + sizeof *sym);
			else
				printt(*t);
		}
		printf(";\n");
	}
	| label 'p' proof '.' /* Not relevant */
	| '{' {
		/* create new frame */
		if (!pushstk(NULL)) { 
			dumpstk();
			yyerror("stack frame overflow.");
			YYERROR;
		}
	} stmlst '}' {
		/*dumpstk();*/
		popstk();
	}
	;

%%
#define getchar getchar_unlocked
char *tok(void)
{
	static char tokbuf[sizeof labbuf];
	char *p = tokbuf;
	int c;

	do 
		if ((c = getchar()) == EOF)
			return NULL;
	while (line += c == '\n', isspace(c));
	do
		if (p == tokbuf + sizeof tokbuf - 1) /* room for \0 */
			yyerror("token too long");
		else
			*p++ = c;
	while ((c = getchar()) != EOF && !isspace(c));
	line += c == '\n';
	*p = '\0';
	yyleng = p - tokbuf;
	return tokbuf;
}

char *gettok(void)
{
	char *p = "";
	while (p && (p = tok()) && !strcmp(p, "$("))
		while ((p = tok()) && strcmp(p, "$)"));
	return p;
}

char *getstmt(int c)
{
	static char stmt[][3] = {
		"$c", "$v", "$d", "$f", "$e", "$a",
		"$p", "$=", "$.", "${", "$}"
	};
	char (*s)[sizeof *stmt];
	for (s = stmt; s != stmt + sizeof stmt / sizeof *stmt; s++)
		if ((*s)[1] == c)
			return *s;
	return NULL;
}

int yylex(void)
{
	char *s;
	yylval = gettok();
	fflush(stdout);
	if (!yylval)
		return 0;
	if (*yylval != '$' || !yylval[1] || yylval[2] 
	 || (s = getstmt(yylval[1])) == NULL)
		return TOKEN;
	yylval = s;
	return yylval[1];
}
void prttok(FILE *iop, int type, YYSTYPE val)
{
	switch (type) {
	case TOKEN:
		fprintf(iop, "%s", val);
		break;
	}
}

int main(int argc, char *argv[])
{
	/*yydebug = 1;*/
	hcreate(8117);
	printf("%%%%\n");
	yyparse();
	printf("%%%%\n");
	hdestroy();
	return EXIT_SUCCESS;
}