# 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 "/usr/wiss/oheimb/isabelle/src/Tools/8bit/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
#
> "\#"
> "\$"
> "\%"
> "\&"
> "'"
> "("
> ")"
> "{*}"
> "+"
> ","
> "-"
> "."
> "/"
> "0"
> "1"
> "2"
> "3"
> "4"
> "5"
> "6"
> "7"
> "8"
> "9"
> ":"
> ";"
> "<"
> "="
> ">"
> "?"
> "@"
> "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"
> "["
> "\ttbackslash{}" #?????
> "]"
> "\^{}"
> "{\_\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"
> "\{" #"\ttlbrace{}"
> "|"
> "\}" #"\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{$\hspace{-.33ex}\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
> "\ :\ " ":" "\mbox{$\hspace{.445ex}\in\hspace{.445ex}$}"
> "\ \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{$\hspace{-.29ex}\bot\hspace{-.29ex}$}"
# relational symbols, Pure, HOLCF
> "===" ".=" "\mbox{$\doteq$}"
> "==" "==" "\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}"
> "~=" "~=" "\mbox{$\hspace{-.34ex}\not\hspace{-.3ex}\mbox{=}$}"
> "\\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{$\hspace{.445ex}\notin\hspace{.445ex}$}"
# arithmetic, HOLCF
> "\\times" "*" "\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}"
> "\+\+" "++" "\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}" #\varoplus
> "\\ominus" "--" "\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}" #\varominus
> "\*\*" "**" "\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
> "^and" "^@and" "and" "\mbox{\bf and}"
> "^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}"
> "^end" "^@end" "end" "\mbox{\bf end}"
> "^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}"
> "^syntax" "^@syntax" "syntax" "\mbox{\bf syntax}"
> "^translations""^@translations""translations""\mbox{\bf translations}"
> "^typedef" "^@typedef" "typedef" "\mbox{\bf typedef}"
> "^types" "^@types" "types" "\mbox{\bf types}"
END_SEQ_TABLE