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

Goal: tuned pris;

/*  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_beg0[], isa_env_beg1[], 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, 
			  (yytext[3]=='@' ? "\\mbox{\\isainline[\\isamodify]{"
					  : "\\mbox{\\isainline{")); }
<LATEX>\\I@isa@?[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
				(yytext[6]=='@' ? isa_env_beg1
						: isa_env_beg0)); reset_tabs(); 
			  if (yytext[strlen(yytext)-1] == '\n')
			  { fprintf(foutput, "\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 (yytext[0] == '\n')
			    { fprintf(foutput, "\n"); lineno++; };
			  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"); }
			  }
			}
<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>\ \             	put((char)160,FALSE,0);
<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>\\cdot          	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><:              	put((char)222,FALSE,0);
<ISAA><=:             	put((char)223,FALSE,0);
<ISAA>:>              	put((char)224,FALSE,0);
<ISAA>~~              	put((char)225,FALSE,0);
<ISAA>\\sim\          	put((char)226,FALSE,0);
<ISAA>\\simeq         	put((char)227,FALSE,0);
<ISAA><=              	put((char)228,FALSE,0);
<ISAA>::              	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>\\frown         	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>\+\+            	put((char)243,FALSE,0);
<ISAA>\\ominus        	put((char)244,FALSE,0);
<ISAA>\*\*            	put((char)245,FALSE,0);
<ISAA>\\oslash        	put((char)246,FALSE,0);
<ISAA>\\subset        	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);
<ISA,ISAA>^and            	put((char)32,TRUE,11);
<ISAA>^@and                	put((char)32,TRUE,11);
<ISA,ISAA>^arities        	put((char)32,TRUE,12);
<ISAA>^@arities            	put((char)32,TRUE,12);
<ISA,ISAA>^axclass        	put((char)32,TRUE,13);
<ISAA>^@axclass            	put((char)32,TRUE,13);
<ISA,ISAA>^constdefs      	put((char)32,TRUE,14);
<ISAA>^@constdefs          	put((char)32,TRUE,14);
<ISA,ISAA>^consts         	put((char)32,TRUE,15);
<ISAA>^@consts             	put((char)32,TRUE,15);
<ISA,ISAA>^datatype       	put((char)32,TRUE,16);
<ISAA>^@datatype           	put((char)32,TRUE,16);
<ISA,ISAA>^defs           	put((char)32,TRUE,17);
<ISAA>^@defs               	put((char)32,TRUE,17);
<ISA,ISAA>^domain         	put((char)32,TRUE,18);
<ISAA>^@domain             	put((char)32,TRUE,18);
<ISA,ISAA>^end            	put((char)32,TRUE,19);
<ISAA>^@end                	put((char)32,TRUE,19);
<ISA,ISAA>^inductive      	put((char)32,TRUE,20);
<ISAA>^@inductive          	put((char)32,TRUE,20);
<ISA,ISAA>^instance       	put((char)32,TRUE,21);
<ISAA>^@instance           	put((char)32,TRUE,21);
<ISA,ISAA>^primrec        	put((char)32,TRUE,22);
<ISAA>^@primrec            	put((char)32,TRUE,22);
<ISA,ISAA>^recdef         	put((char)32,TRUE,23);
<ISAA>^@recdef             	put((char)32,TRUE,23);
<ISA,ISAA>^rules          	put((char)32,TRUE,24);
<ISAA>^@rules              	put((char)32,TRUE,24);
<ISA,ISAA>^syntax         	put((char)32,TRUE,25);
<ISAA>^@syntax             	put((char)32,TRUE,25);
<ISA,ISAA>^translations   	put((char)32,TRUE,26);
<ISAA>^@translations       	put((char)32,TRUE,26);
<ISA,ISAA>^typedef        	put((char)32,TRUE,27);
<ISAA>^@typedef            	put((char)32,TRUE,27);
<ISA,ISAA>^types          	put((char)32,TRUE,28);
<ISAA>^@types              	put((char)32,TRUE,28);
  /* 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;
  char s[100];
  extern char *translateHi(int ch, int code);

    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... */
       strcpy(s, translateHi(c, destCode));
       i = strlen(s);
       if((unsigned char)c != 0xa0 &&
	  i >= 2 && s[i-2] == '\\' && s[i-1] == ' ' && (yytext[0] & 0x80))
	 s[i-2] ='\0';
       fprintf(foutput, "%s", s);
        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 */
}