src/Tools/8bit/config/conv-tables.inp

minor improvements

#   Title:      Tools/8bit/config/conf-tables.inp
#   ID:         $Id$
#   Author:     Franz Regensburger and David von Oheimb
#   Copyright   1995 TU Muenchen
############################################################
#
# This is the configuration file for the converter isa2latex
# It is interpreted by the perl script `gen-isa2latex' which
# produces rsp. changes the followong files of the converter
# sources:
#
#  Makefile, conv-tables.h, conv-defs.h and conv-lex.x
#
# In the perl script, regular expressions are used to identify
# the keywords. In order to be sure that something is treated
# as a comment, simply begin the line with a # sign. This is
# fool proof.
#
############################################################ 

############################################################ 
# General setup
#
### path to the sources of the converter, 
#   Must be readable for user.
#   
#   Must be delimited by "
#

CONV_SOURCE_DIR "../c-sources/isa2latex"

# End of  general setup
############################################################ 

############################################################ 
# Setup for translationTableLow in file conv-tables.h
#

### Start index START_LOW_TABLE of translationTableLow
#   The index END_LOW_TABLE is computed from the length
#   of the translation  table LOW_TABLE below.
#
#   constraints: 32 <= START_LOW_TABLE <= 127 
#                START_LOW_TABLE + length(LOW_TABLE) - 1 <= 127 
#
#   Must be delimited by "
#

START_LOW_TABLE "32"

### The translation table LOW_TABLE
#
#   Keyword for the begin of the table is BEGIN_LOW_TABLE
#   Keyword for the end of the table is   END_LOW_TABLE
#
#   Lines beginning with # are ignored as everywhere in this file.
#   Lines obeying the syntax given below are treated as table entries.
#   All other lines are ignored, too. This is for comments.
#
#   Syntax of a table entry:
#   
#   > "LaTeX replacement"  anything
#
#   The double quotes enclose the LaTeX replacement in pure 
#   LaTeX syntax. 
#   Every \ in the string except when used for hex-notation \x?? is
#   automatically duplicated by the script! The strings are used in
#   printf output statements in the C code.
#
#   Attention: you have to use hex-notation \x22 to produce a " inside 
#   the double quoted strings. An explicit " will terminate the string.
#
#   The following `anything' is ignored by the perl script.
#   This is for comments.
#   
#   The ordering of entries in the table LOW_TABLE is relevant!
#   Empty table is not allowed.
#
#

BEGIN_LOW_TABLE
>  "\ "			Blank 
>  "!"
#
# if you don't like double quotes to be removed insert the following
#>  "\\x22{}"		double quotes are not removed 
>  "\x22{}"		double quotes are not removed 
#
>  "\mbox{$\#$}"
>  "\$"
>  "\%"
>  "\&"
>  "'"
>  "\mbox{$($}"
>  "\mbox{$)$}"
>  "{*}"
>  "+"
>  ","
>  "-"
>  "."
>  "/"
>  "0"
>  "1"
>  "2"
>  "3"
>  "4"
>  "5"
>  "6"
>  "7"
>  "8"
>  "9"
>  ":"
>  ";"
>  "\mbox{$<$}"
>  "\mbox{$=$}"
>  "\mbox{$>$}"
>  "?"
>  "@"
>  "A"
>  "B"
>  "C"
>  "D"
>  "E"
>  "F"
>  "G"
>  "H"
>  "I"
>  "J"
>  "K"
>  "L"
>  "M"
>  "N"
>  "O"
>  "P"
>  "Q"
>  "R"
>  "S"
>  "T"
>  "U"
>  "V"
>  "W"
>  "X"
>  "Y"
>  "Z"
>  "\mbox{$[$}"
>  "\ttbackslash{}" #?????
>  "\mbox{$]$}"
>  "\^{}"			
>  "{\_\hspace{.344ex}}"
>  "`"
>  "a"
>  "b"
>  "c"
>  "d"
>  "e"
>  "f"
>  "g"
>  "h"
>  "i"
>  "j"
>  "k"
>  "l"
>  "m"
>  "n"
>  "o"
>  "p"
>  "q"
>  "r"
>  "s"
>  "t"
>  "u"
>  "v"
>  "w"
>  "x"
>  "y"
>  "z"
>  "\mbox{$\{$}" #"\ttlbrace{}"
>  "\mbox{$\mid$}"
>  "\mbox{$\}$}" #"\ttrbrace{}"
>  "\tttilde{}"
END_LOW_TABLE

############################################################ 
# Setup for translationTableHi in file conv-tables.h
#

### Start index START_HI_TABLE of translationTableHi
#   The index END_HI_TABLE is computed from the length
#   of the translation table HI_TABLE below.
#
#   constraints: 128 <= START_HI_TABLE <= 255
#                START_HI_TABLE + length(HI_TABLE) - 1 <= 255 
#                
#
#   Must be delimited by "
#

START_HI_TABLE "160"

### The translation table HI_TABLE
#
#   Keyword for the begin of the table is BEGIN_HI_TABLE
#   Keyword for the end of the table is   END_HI_TABLE
#
#   Lines beginning with # are ignored as everywhere in this file.
#   Lines obeying the syntax given below are treated as table entries.
#   All other lines are ignored, too. This is for comments.
#
#   Syntax of a table entry:
#   
#   > "lex expression ascii" "ascii replacement" "LaTeX replacement"  anything
#
#   The double quotes enclose the lex expression, the ascii replacement, and the
#   LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. 
#
#   The string for the lex expression is literally passed to lex. Backslashes
#   are not duplicated!
#   Every \ in the replacements except when used for hex-notation \x?? is
#   automatically duplicated by the script! The strings are used in
#   printf output statements in the C code.
#
#   Attention: you have to use hex-notation \x22 to produce a " inside 
#   the double quoted strings. An explicit " will terminate the string.
#
#   The following `anything' is ignored by the perl script.
#   This is for comments.
#
#   The ordering of entries in the table HI_TABLE is relevant!
#   Empty table is not allowed.
#
#

BEGIN_HI_TABLE

# big (i.e. double) blank space, for compensation of other too long symbols
>  "\ \ "		"  "		"\ \ "

# big greek letters
>  "\\Gamma"		"\Gamma"	"\mbox{$\Gamma$}"
>  "\\Delta"		"\Delta"	"\mbox{$\Delta$}"
>  "\\Theta"		"\Theta"	"\mbox{$\Theta$}"
>  "LAM\ "		"LAM "		"\mbox{$\Lambda$}" 
>  "\\Pi"		"\Pi"		"\mbox{$\Pi$}" 
>  "\\Sigma"		"\Sigma"	"\mbox{$\Sigma$}" 
>  "\\Phi"		"\Phi"		"\mbox{$\Phi$}" 
>  "\\Psi"		"\Psi"		"\mbox{$\Psi$}" 
>  "\\Omega"		"\Omega"	"\mbox{$\Omega$}" 

# small greek letters, HOL, HOLCF
>  "'a"			"'a"		"\mbox{$\alpha$}" 
>  "'b"			"'b"		"\mbox{$\beta$}" 
>  "'c"			"'c"		"\mbox{$\gamma$}" 
>  "\\delta"		"\delta"	"\mbox{$\delta$}" 
>  "\\varepsilon"	"@"		"\mbox{$\varepsilon$}" 
>  "\\zeta"		"\zeta"		"\mbox{$\zeta$}"
>  "\\eta"		"\eta"		"\mbox{$\eta$}" 
>  "\\vartheta"		"\vartheta"	"\mbox{$\vartheta$}" 
>  "\\kappa"		"\kappa"	"\mbox{$\kappa$}" 
>  "%\ "		"%"		"\mbox{$\lambda$}" 
>  "\\mu"		"\mu"		"\mbox{$\mu$}" 
>  "\\nu"		"\nu"		"\mbox{$\nu$}" 
>  "\\xi"		"\xi"		"\mbox{$\xi$}" 
>  "\\pi"		"\p"		"\mbox{$\pi$}" 
>  "'r"			"'r"		"\mbox{$\rho$}" 
>  "'s"			"'s"		"\mbox{$\sigma$}" 
>  "'t"			"'t"		"\mbox{$\tau$}" 
>  "\\varphi"		"\varphi"	"\mbox{$\varphi$}" 
>  "\\chi"		"\chi"		"\mbox{$\chi$}" 
>  "\\psi"		"\psi"		"\mbox{$\psi$}" 
>  "\\omega"		"\omega"	"\mbox{$\omega$}" 

# logical symbols, HOL
>  "~\ "		"~ "		"\mbox{$\neg$}" 
>  "&\ "		"& "		"\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " 
>  "\|\ "		"| "		"\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " 
>  "!\ "		"!"		"\mbox{$\hspace{-.07ex}\forall$}" 
>  "\?\ "		"? "		"\mbox{$\hspace{-.07ex}\exists$}"
>  "!!"			"!!"		"\mbox{$\bigwedge$}" 

# parenthesis. Pure, HOLCF, ...
>  "\\lceil"		"\lceil"	"\mbox{$\lceil$}" 
>  "\\rceil"		"\rceil"	"\mbox{$\rceil$}" 
>  "\\lfloor"		"\lfloor"	"\mbox{$\lfloor$}" 
>  "\\rfloor"		"\rfloor"	"\mbox{$\rfloor$}" 
#> "\|-"		"|-"		"\mbox{$\vdash\hspace{-.2ex}$}"
>  "\|-"		"|-"		"\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}"
>  "\|="		"|="		"\mbox{$\models$}"
>  "\[\|"		"[|"		"\mbox{$[\![\hspace{.32ex}$}"#\llbracket
>  "\|\]"		"|]"		"\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket
>  "\\cdot"		"."		"\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}"

# set theory, HOL
>  "\ :\ "		":"		"\hspace{.1ex}\mbox{$\in$}\hspace{.1ex}"#"\mbox{$\in$}"
>  "\ \subseteq\ "	" \subseteq "	"\mbox{$\subseteq$}" 
>  "\ Int\ "		" Int "		"\mbox{$\cap$}" 
>  "\ Un\ "		" Un "		"\mbox{$\cup$}" 
>  "Inter\ "		"INT "		"\mbox{$\bigcap$}"
>  "Union\ "		"UN "		"\mbox{$\bigcup$}" 

# domain theory, HOLCF
>  "\\sqcap"		"\sqcap"	"\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}" 
>  "\\sqcup"		"\sqcup"	"\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" 
>  "glb\ "		"glb "		"\mbox{$\overline{|\,\,|}$}"#\bigsqcap
>  "LUB\ "		"LUB "		"\mbox{$\bigsqcup$}" 
>  "UU"			"UU"		"\mbox{$\bot$}" 

# relational symbols, Pure, HOLCF
>  "==="		".="		"\mbox{$\doteq$}" 
>  "=="			"=="		"\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" 
>  "~="			"~="		"\mbox{$\not=$}" 
>  "\\sqsubset"		"\sqsubset"	"\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" 
>  "<<"			"<<"		"\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" 
>  "<:"			"<:"		"\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " 
>  "<=:"		"<=:"		"\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}" 
>  ":>"			":>"		"\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ " 
>  "~~"			"~~"		"\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}" 
>  "\\sim\ "		"\sim "		"\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ " 
>  "\\simeq"		"\simeq"	"\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}" 
>  "<="			"<="		"\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}" 
>  "::"			"::"		"\mbox{$:\hspace{-.07ex}:$}" #"\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}" 

# arrows, Pure, HOL
>  "<-"		"<-"		"\mbox{$\leftarrow$}" 
>  "-@@@@@"		"-"		"\mbox{$-$}" 
>  "->"			"->"		"\mbox{$\rightarrow$}" 
>  "\\Leftarrow"	"<="		"\mbox{$\Leftarrow$}" 
>  "=@@@@@"		"="		"\mbox{$=$}" 
>  "=>"			"=>"		"\mbox{$\hspace{.12ex}\Rightarrow$}" 
>  "\\frown"		"\frown"	"\mbox{$\frown$}" 
>  "\\mapsto"		"|->"		"\mbox{$\mapsto$}" 
>  "\\leadsto"		"~>"		"\mbox{$\hspace{.05ex}\leadsto$}" 
>  "\\uparrow"		"\uparrow"	"\mbox{$\uparrow$}" 
>  "\\downarrow"	"\downarrow"	"\mbox{$\downarrow$}" 
>  "~:"			"~:"		"\mbox{$\notin$}" 

# arithmetic, HOLCF
>  "\\times"		"*"		"\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" 
>  "\\oplus"		"++"		"\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}"	#\varoplus
>  "\\ominus"		"--"		"\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}"	#\varominus
>  "\\otimes"		"**"		"\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}"	#\varotimes
>  "\\oslash"		"//"		"\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" 	#\varoslash
>  "\\subset"		"\subset"	"\mbox{$\subset$}" 
>  "\\infty"		"\infty"	"\mbox{$\infty$}" 

# misc
>  "\\Box"		"\Box"		"\mbox{$\Box$}" 
>  "\\Diamond"		"<>"		"\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}"
>  "\\circ"		" o "		"\mbox{$\circ$}" 
>  "\\bullet"		"\bullet"	"\mbox{$\bullet$}" 
>  "\|\|"		"||"		"\mbox{$\parallel$}" 
>  "\\tick"		"\tick"		"\mbox{$\surd$}" 
>  "\\filter"		"\filter"	"\mbox{\copyright}"
END_HI_TABLE

############################################################ 
# Setup for translationTableSeq in file conv-tables.h
# and lexer source conv-lex.x
# 
#   Keyword for the being of the table is BEGIN_SEQ_TABLE
#   Keyword for the end of the table is   END_SEQ_TABLE
#
#   Lines beginning with # are ignored as everywhere in this file.
#   Lines obeying the syntax given below are treated as table entries.
#   All other lines are ignored, too. This is for comments.
#
#   Syntax of a table entry:
#   
#   > "lex expr 8bit" "lex expr ascii" "ascii replace" "LaTeX replace" anything
#
#   The double quotes enclose the lex expressions, the ascii replacement, and
#   the  LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. 
#   
#   The strings for the lex expressions are literally passed to lex. Backslashes
#   are not duplicated!
#   Every \ in the replacements except when used for hex-notation \x?? is
#   automatically duplicated by the script! The strings are used in
#   printf output statements in the C code.
#
#   Attention: you have to use hex-notation \x22 to produce a " inside 
#   the double quoted strings. An explicit " will terminate the string.
#
#   The following `anything' is ignored by the perl script.
#   This is for comments.
#
#   The ordering of entries in table SEQ_TABLE is irrelevant!
#   Empty table is allowed.
#

BEGIN_SEQ_TABLE

# Pure
>  "êë"		"==>"		"==>"		"\mbox{$\hspace{-.083ex}\Longrightarrow$}"

# HOL
>  "çè"		"-->"		"-->"		"\mbox{$\longrightarrow$}"
>  "Ã!"		"\?!"		"?!"		"\mbox{$\exists_1$}"
>  "ALL@@@@@"	"ALL\ "		"ALL "		"\mbox{$\forall$}" 
>  "EX@@@@@"	"EX\ "		"EX "		"\mbox{$\exists$}" 

#HOLCF
>  "<<\|"	"<<\|"		"<<|"		"\mbox{$\ll\!\mid$}"
>  "<\|"	"<\|"		"<|"		"\mbox{$<\!\mid$}"

# misc ?
>  "éê"		"<=="		"<=="		"\mbox{$\Longleftarrow$}"
>  "éë"		"<=>"		"<=>"		"\mbox{$\Leftrightarrow$}"
>  "æç"		"<--"		"<--"		"\mbox{$\longleftarrow$}"
>  "æè"		"<->"		"<->"		"\mbox{$\leftrightarrow$}"
>  "\^-1"	"\^-1"		"^-1"		"\mbox{$^{\tt -1}$}" 

#Isabelle
>  "arities"	"@arities"	"arities"	"\mbox{\bf arities}"
>  "axclass"	"@axclass"	"axclass"	"\mbox{\bf axclass}"
>  "constdefs"	"@constdefs"	"constdefs"	"\mbox{\bf constdefs}"
>  "consts"	"@consts"	"consts"	"\mbox{\bf consts}"
>  "datatype"	"@datatype"	"datatype"	"\mbox{\bf datatype}"
>  "defs"	"@defs"		"defs"		"\mbox{\bf defs}"
>  "domain"	"@domain"	"domain"	"\mbox{\bf domain}"
>  "inductive"	"@inductive"	"inductive"	"\mbox{\bf inductive}"
>  "instance"	"@instance"	"instance"	"\mbox{\bf instance}"
>  "primrec"	"@primrec"	"primrec"	"\mbox{\bf primrec}"
>  "recdef"	"@recdef"	"recdef"	"\mbox{\bf recdef}"
>  "rules"	"@rules"	"rules"		"\mbox{\bf rules}"
>  "translations""@translations""translations"	"\mbox{\bf translations}"
>  "typedef"	"@typedef"	"typedef"	"\mbox{\bf typedef}"
>  "types"	"@types"	"types"		"\mbox{\bf types}"
END_SEQ_TABLE