src/Tools/8bit/c-sources/isa2latex/conv-lex.x

Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML

/*  Title:      Tools/8bit/c-sources/isa2latex/conv-main.c
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1996 TU Muenchen

converter for isabelle files
definitions for the lexical analyzer
*/

%{
#include "conv-defs.h"
#define output(c) fputc(c, yyout)
#define BEGIN_ISA {	if (accept_ASCII)				\
				BEGIN ISAA;	/* we have -A option */	\
			else						\
				BEGIN ISA;}

extern FILE *finput, *foutput;
extern int tabBlanks;
extern int tabcount;
extern char isa_env_beg[], isa_env_end[];
extern int convMode;
extern int accept_ASCII;
extern int destCode;
extern int cc;

void reset_tabs(void);
void put(char c, int longDetect, int longCode);

int lineno=1;
int inline_mode=FALSE;
%}
%S LATEX ISA ISAA ESC
%option noyywrap

%%
  void warning(char *what);
  void not_suitable(char *what, char *where);
  yyin = finput;
  yyout = foutput;

  if (convMode == MIXED)
	BEGIN LATEX;	/* we have -x option */
  else 
	BEGIN_ISA;

<LATEX>\\I@		{ BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput, 
				"{\\isainline{"); }
<LATEX>\\I@isa[ \t]*\n?	{ BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
				isa_env_beg); reset_tabs(); 
			  if (yytext[strlen(yytext)-1] == '\n') lineno++;
			}
<LATEX>\\E@		{ ECHO; not_suitable("\\E@","LATEX"); }
<LATEX>\n		{ put(*yytext,FALSE,0); lineno++; }

<ISA,ISAA>\\I@		{ if (inline_mode) 
			  { BEGIN LATEX; inline_mode=FALSE; 
			    fprintf(foutput, "}}"); }
			  else
			  { ECHO; not_suitable("\\I@","ISA"); }
			}
<ISA,ISAA>\n?[ \t]*\\I@isa	{ if (inline_mode)
			  { ECHO; not_suitable("\\I@isa","INLINE"); }
			  else
			  { if (convMode == MIXED) {
			      BEGIN LATEX; fprintf(foutput, isa_env_end); }
			    else {
			      ECHO; warning(
				"\\I@isa only allowed with -x option"); }
			  }
			  if (yytext[0] == '\n') lineno++;
			}
<ISA,ISAA>\\E@		{ BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
<ISA,ISAA><<EOF>>	{ if (convMode == MIXED) 
			    not_suitable("EOF", inline_mode? "INLINE": "ISA");
			   yyterminate(); 
			}
<ISA,ISAA>\n		{ if (inline_mode) 
			  { ECHO; not_suitable("\\n","INLINE"); }
			  else
			  { put(*yytext,FALSE,0); }
			  lineno++;
			}
<ISA,ISAA>\t		{ if (inline_mode)
			  { ECHO; not_suitable("\\t","INLINE"); }
			  else
			  { put(*yytext,FALSE,0); }
			}

<ESC>\\I@		{ ECHO; not_suitable("\\I@"   ,"ESC"); }
<ESC>\\I@isa		{ ECHO; not_suitable("\\I@isa","ESC"); }
<ESC>\\E@		{ BEGIN_ISA; fprintf(foutput, "}}"); }
<ESC><<EOF>>		{       not_suitable("EOF"    ,"ESC"); yyterminate(); }
<ESC>\n			{ put(*yytext,FALSE,0); lineno++; }

  /* The following is generated by the perl script gen-isa2latex. */
  /* Make modifications in configuration file for gen-isa2latex!  */             
  /* BEGIN_OF_HI_TABLE */
<ISAA>\\Gamma\         	put((char)161,FALSE,0);
<ISAA>\\Delta\         	put((char)162,FALSE,0);
<ISAA>\\Theta\         	put((char)163,FALSE,0);
<ISAA>LAM\             	put((char)164,FALSE,0);
<ISAA>\\Pi\            	put((char)165,FALSE,0);
<ISAA>\\Sigma\         	put((char)166,FALSE,0);
<ISAA>\\Phi\           	put((char)167,FALSE,0);
<ISAA>\\Psi\           	put((char)168,FALSE,0);
<ISAA>\\Omega\         	put((char)169,FALSE,0);
<ISAA>'a               	put((char)170,FALSE,0);
<ISAA>'b               	put((char)171,FALSE,0);
<ISAA>'c               	put((char)172,FALSE,0);
<ISAA>\\delta\         	put((char)173,FALSE,0);
<ISAA>\\varepsilon\    	put((char)174,FALSE,0);
<ISAA>\\zeta\          	put((char)175,FALSE,0);
<ISAA>\\eta\           	put((char)176,FALSE,0);
<ISAA>\\vartheta\      	put((char)177,FALSE,0);
<ISAA>\\kappa\         	put((char)178,FALSE,0);
<ISAA>%\               	put((char)179,FALSE,0);
<ISAA>\\mu\            	put((char)180,FALSE,0);
<ISAA>\\nu\            	put((char)181,FALSE,0);
<ISAA>\\xi\            	put((char)182,FALSE,0);
<ISAA>\\pi\            	put((char)183,FALSE,0);
<ISAA>'r               	put((char)184,FALSE,0);
<ISAA>'s               	put((char)185,FALSE,0);
<ISAA>'t               	put((char)186,FALSE,0);
<ISAA>\\varphi\        	put((char)187,FALSE,0);
<ISAA>\\chi\           	put((char)188,FALSE,0);
<ISAA>\\psi\           	put((char)189,FALSE,0);
<ISAA>\\omega\         	put((char)190,FALSE,0);
<ISAA>~\               	put((char)191,FALSE,0);
<ISAA>&\               	put((char)192,FALSE,0);
<ISAA>\|\              	put((char)193,FALSE,0);
<ISAA>!\               	put((char)194,FALSE,0);
<ISAA>\?\              	put((char)195,FALSE,0);
<ISAA>!!               	put((char)196,FALSE,0);
<ISAA>\\lceil\         	put((char)197,FALSE,0);
<ISAA>\\rceil\         	put((char)198,FALSE,0);
<ISAA>\\lfloor\        	put((char)199,FALSE,0);
<ISAA>\\rfloor\        	put((char)200,FALSE,0);
<ISAA>\(\|             	put((char)201,FALSE,0);
<ISAA>\|\)             	put((char)202,FALSE,0);
<ISAA>\[\|             	put((char)203,FALSE,0);
<ISAA>\|\]             	put((char)204,FALSE,0);
<ISAA>{}               	put((char)205,FALSE,0);
<ISAA>\ :\             	put((char)206,FALSE,0);
<ISAA>\subseteq\       	put((char)207,FALSE,0);
<ISAA>\ Int\           	put((char)208,FALSE,0);
<ISAA>\ Un\            	put((char)209,FALSE,0);
<ISAA>Inter\           	put((char)210,FALSE,0);
<ISAA>Union\           	put((char)211,FALSE,0);
<ISAA>\sqcap\          	put((char)212,FALSE,0);
<ISAA>\sqcup\          	put((char)213,FALSE,0);
<ISAA>glb\             	put((char)214,FALSE,0);
<ISAA>lub\             	put((char)215,FALSE,0);
<ISAA>UU               	put((char)216,FALSE,0);
<ISAA>===              	put((char)217,FALSE,0);
<ISAA>==               	put((char)218,FALSE,0);
<ISAA>~=               	put((char)219,FALSE,0);
<ISAA>\\sqsubset\      	put((char)220,FALSE,0);
<ISAA><<               	put((char)221,FALSE,0);
<ISAA>\\prec\          	put((char)222,FALSE,0);
<ISAA>\\preceq\        	put((char)223,FALSE,0);
<ISAA>\\succ\          	put((char)224,FALSE,0);
<ISAA>\\succeq\        	put((char)225,FALSE,0);
<ISAA>\\sim\           	put((char)226,FALSE,0);
<ISAA>\\simeq\         	put((char)227,FALSE,0);
<ISAA>\\le\            	put((char)228,FALSE,0);
<ISAA>\\ge\            	put((char)229,FALSE,0);
<ISAA><-               	put((char)230,FALSE,0);
<ISAA>-@@@@@           	put((char)231,FALSE,0);
<ISAA>->               	put((char)232,FALSE,0);
<ISAA>\\Leftarrow\     	put((char)233,FALSE,0);
<ISAA>=@@@@@           	put((char)234,FALSE,0);
<ISAA>=>               	put((char)235,FALSE,0);
<ISAA>->>              	put((char)236,FALSE,0);
<ISAA>\\mapsto\        	put((char)237,FALSE,0);
<ISAA>\\leadsto\       	put((char)238,FALSE,0);
<ISAA>\\uparrow\       	put((char)239,FALSE,0);
<ISAA>\\downarrow\     	put((char)240,FALSE,0);
<ISAA>~:               	put((char)241,FALSE,0);
<ISAA>\\times\         	put((char)242,FALSE,0);
<ISAA>\\oplus\         	put((char)243,FALSE,0);
<ISAA>\\ominus\        	put((char)244,FALSE,0);
<ISAA>\\otimes\        	put((char)245,FALSE,0);
<ISAA>\\oslash\        	put((char)246,FALSE,0);
<ISAA>\\natural\       	put((char)247,FALSE,0);
<ISAA>\\infty\         	put((char)248,FALSE,0);
<ISAA>\\Box\           	put((char)249,FALSE,0);
<ISAA>\\Diamond\       	put((char)250,FALSE,0);
<ISAA>\\circ\          	put((char)251,FALSE,0);
<ISAA>\\bullet\        	put((char)252,FALSE,0);
<ISAA>\|\|             	put((char)253,FALSE,0);
<ISAA>\\tick\          	put((char)254,FALSE,0);
<ISAA>\\filter\        	put((char)255,FALSE,0);
  /* END_OF_HI_TABLE */
  /* This is the end of the generated part */

  /* The following is generated by the perl script gen-isa2latex. */
  /* Make modifications in configuration file for gen-isa2latex!  */             
  /* BEGIN_OF_SEQ_TABLE */
<ISA,ISAA>êë          	put((char)32,TRUE,0);
<ISAA>==>         	put((char)32,TRUE,0);
<ISA,ISAA>çè          	put((char)32,TRUE,1);
<ISAA>-->         	put((char)32,TRUE,1);
<ISA,ISAA>Ã!          	put((char)32,TRUE,2);
<ISAA>\?!         	put((char)32,TRUE,2);
<ISA,ISAA>ALL@@@@@    	put((char)32,TRUE,3);
<ISAA>ALL\        	put((char)32,TRUE,3);
<ISA,ISAA>EX@@@@@     	put((char)32,TRUE,4);
<ISAA>EX\         	put((char)32,TRUE,4);
<ISA,ISAA><\|@@@@@    	put((char)32,TRUE,5);
<ISAA><\|         	put((char)32,TRUE,5);
<ISA,ISAA><<\|@@@@@   	put((char)32,TRUE,6);
<ISAA><<\|        	put((char)32,TRUE,6);
<ISA,ISAA>éê          	put((char)32,TRUE,7);
<ISAA><==         	put((char)32,TRUE,7);
<ISA,ISAA>éë          	put((char)32,TRUE,8);
<ISAA><=>         	put((char)32,TRUE,8);
<ISA,ISAA>æç          	put((char)32,TRUE,9);
<ISAA><--         	put((char)32,TRUE,9);
<ISA,ISAA>æè          	put((char)32,TRUE,10);
<ISAA><->         	put((char)32,TRUE,10);
  /* END_OF_SEQ_TABLE */
  /* This is the end of the generated part */

.			{ put(*yytext,FALSE,0);}

%%

void warning(char *str)
{
  fprintf(stderr,"WARNING: line %d: %s\n", lineno, str);
}

void not_suitable(char *what, char *where)
{
  char buf[80];
  sprintf(buf, "'%s' inside %s mode", what, where);
  warning(buf);
}

void reset_tabs(void)
{
  cc = 0;
  tabcount = 1;
}

void put(char c, int longDetect,int longCode)
{
  int i;

    if (YY_START == LATEX || YY_START == ESC)
        /* do not translate in these modes */ 
	fputc(c,foutput);

    else /* we are in ISA mode */
    if (longDetect) { /* lexer has scanned a long sequence */ 
       fprintf(foutput, "%s", translateLong(longCode, destCode));
        if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
          tabcount++;
       }
    else /* lexer has not scanned a long sequence */		      
    if (c & 0x80) { /* Hi-bit is set... */
       fprintf(foutput, "%s", translateHi(c, destCode));
        if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
          tabcount++;
    } 
    else /* simple char without Hi-Bit*/
    if (destCode == TO_7bit)
        fputc(c, foutput);
    else
        switch (c) {  /* handle control codes */
          case '\n': if (inline_mode)
		       c=' ';
		     else {
		       fprintf(foutput, "\\\\\n");
		       reset_tabs();
		       break;
		     }
          case TAB:  if (inline_mode)
		       c=' ';
		     else {
		       for (i = 0; i < tabcount; i++)
		         fprintf(foutput, "\\>");
		       reset_tabs();
		       break;
		     }
         default:
            if (++cc % tabBlanks == 0)
              tabcount++;
            if ((c >= START_LOW_TABLE) && (c <= END_LOW_TABLE))
	      {
              fprintf(foutput, "%s", translateLow(c));}
            else /* just reproduce the other control codes */
              fputc(c, foutput);
        } /* switch */
}