This page is using MathJax. See the same page using KaTeX.

Macros

This page explains how to mark up CBS specifications in LaTeX when using the cbs-latex package. It also provides links to the macro definitions for use with LaTeX, KaTeX, and MathJax.

Table of contents

Required packages
Names
- Hyperlinks
- Variables
Language specifications
Funcon specifications
Alignment

Markup using CBS-LaTeX is quite low-level. This makes it easy to adjust the layout to fit the intended page width, but tedious to write.¹

CBS-LaTeX provides the following files:

cbs-latex.sty: a package of macro definitions for use in LaTeX documents
cbs-katex.sty: a configuration defining KaTeX macros for use in web pages
cbs-mathjax.sty: a configuration defining MathJax macros for use in web pages

The packages include some explanatory comments. Each package defines the same collection of LaTeX macro names, taking the same arguments. The rendering of the macros should have the same layout and symbols, regardless of which format is used, except that the font families may differ.

All macro names are uppercase, to reduce the risk of clashes with macros defined by other packages.² They are intended for use primarily in math mode.

Required packages

When used with , the cbs-latex package requires the following packages (all included in TeXLive):

amsmath: Provides various environments and commands for math alignment, including the align and aligned environments.
amssymb: Provides an extended math symbol collection, including .
stmaryrd: Provides symbols for TCS, including and .
textcomp: Provides commands for various characters in text mode, including .³
xcolor: The svgnames option provides color names that can also be used on web pages (see the W3schools Colors Tutorial).
hyperref: Needed for creating hyperlinks. Use \hypersetup{filebordercolor=White} to avoid colored boxes around references to names in CBS specifications.

The following packages are not required, but using them may make the formatting of running text in closer to that produced from Markdown on web pages:

cmbright: Global sans-serif fonts.
geometry: Allows adjustment of page dimensions. Set in the preamble, e.g., \geometry{a4paper, textwidth=150mm, top=10mm, bottom=20mm, footnotesep=10mm plus 10mm}.
parskip: Uses blank lines to separate paragraphs.

Names

CBS specifications involve declaration and reference of names for funcons, entities, syntax sorts, and semantic functions.⁴ The macro used for a name depends on the namespace. Names in different namespaces have different highlighting colors, and the colors depend on the configured color_scheme.

Plain CBS	CBS-LaTeX	Formatted CBS
`funcon-name`	`\FUN{funcon-name}`
`entity-name`	`\FUN{entity-name}`
`syntax-name`	`\SYN{syntax-name}`
`semantics-name`	`\SEM{semantics-name}`
`§2.1 A section`	`\textsf{\S\SECT{2.1} A section}`

Hyperlinks

Variants of the name markup macros indicate that the occurrence of a name is a declaration or a reference. In both PDFs and web pages, each name reference becomes a hyperlink to the declaration of that name. A name should not be declared (in the same namespace) more than once per document.

Plain CBS	CBS-LaTeX	Formatted CBS
`name`	`\FUNDEC{name}`
`name`	`\FUNREF{name}`
`name`	`\FUNHYP{url}{file}{name}`

Similarly for \SYN, \SEM, \SECT.

Variables

The macro for variable names formats its argument in text mode. A Greek letter used as a variable name has to be in math mode. Subscripts should be marked up directly after the variable name, to ensure that they are in the intended sans serif font (and to support italic spacing correction). Any primes and multiplicity are written after the name and subscript.

Plain CBS	CBS-LaTeX	Formatted CBS
`X'`	`\VAR{X}'`
`X12''`	`\VAR{X}\SUB{12}''`
`X+`	`\VAR{X}\PLUS`
`X?`	`\VAR{X}\QUERY`
`X*`	`\VAR{X}\STAR`
`Rho`	`\rho` or `\VAR{$\rho$}`

Language specifications

Grammars

Plain CBS	CBS-LaTeX	Formatted CBS
`Lexis ...`	`\KEY{Lexis} ~ ...`
`Syntax ...`	`\KEY{Syntax} ~ ...`
`...:... ::= ...`	`...:... ::= ...`

Syntactic phrase types

Plain CBS	CBS-LaTeX	Formatted CBS
`syntax-name`	`\SYN{syntax-name}`
`'lexeme'`	`\LEX{lexeme}`
`P_1 P_2`	`P_1 ~ P_2`
`P_1 \| P_2`	`P_1 \mid P_2`
`P+`	`P\PLUS`
`P?`	`P\QUERY`
`P*`	`P\STAR`
`(P)`	`\LEFTGROUP P \RIGHTGROUP`

Lexemes

Characters in lexemes are marked up as follows. Those that require macros include all the special characters of , and characters that look different in text and math mode.

Plain CBS	CBS-LaTeX	Formatted CBS
`'0...9A...Za...z'`	`\LEX{0...9A...Za...z}`
`'!()*,./:;=?@[]'`	`\LEX{!()*,./:;=?@[]}`
`'#'`	`\LEX{\HASH}`
`'$'`	`\LEX{\DOLLAR}`
`'%'`	`\LEX{\PERCENT}`
`'&'`	`\LEX{\AMPERSAND}`
`'\''`	`\LEX{\APOSTROPHE}`
`'\\'`	`\LEX{\BACKSLASH}`
`'^'`	`\LEX{\CARET}`
`'_'`	`\LEX{\UNDERSCORE}`
'`'	`\LEX{\GRAVE}`
`'{'`	`\LEX{\LEFTBRACE}`
`'}'`	`\LEX{\RIGHTBRACE}`
`'~'`	`\LEX{\TILDE}`

Semantic functions

Plain CBS	CBS-LaTeX	Formatted CBS
`Semantics s-n[[_:...]] : ...`	`\KEY{Semantics} ~ \SEMDEC{s-n} \LEFTPHRASE \_ : ... \RIGHTPHRASE : ...`
`Rule ... = ...`	`\KEY{Rule} ~ ... = ...`
`[[...]]`	`\LEFTPHRASE ... \RIGHTPHRASE`
`s-n[[...]]`	`\SEMREF{s-n} \LEFTPHRASE ... \RIGHTPHRASE`

Funcon specifications

Plain CBS	CBS-LaTeX	Formatted CBS
`Funcon f-n ... : ...`	`\KEY{Funcon} ~ \FUNDEC{f-n} ... : ...`
`Alias f-n1 = f-n2`	`\KEY{Alias} ~ \FUNDEC{f-n1} = \FUNREF{f-n2}`
`Type t-n ...`	`\KEY{Type} ~ \FUNDEC{t-n} ...`

Datatype specifications

Plain CBS	CBS-LaTeX	Formatted CBS
`Datatype d-n ::= ...`	`\KEY{Datatype} ~ \FUNDEC{d-n} ::= ...`
`... \| ...`	`... \mid ...`
`c-n`	`\FUNDEC{c-n}`
`c-n(...)`	`\FUNDEC{c-n}(...)`
`{ _ : ... }`	`\{ ~ _ : ... ~ \}`

Entity declarations

Plain CBS	CBS-LaTeX	Formatted CBS
`Entity ...`	`\KEY{Entity} ~ ...`
`e-n(_:...)\|- _ ---> _`	`\FUNDEC{e-n}(\_:...) \vdash \_\TRANS\_`
`<_,e-n(_:...)> ---> <_,e-n(_:...)>`	`\langle\_,\FUNDEC{e-n}(\_:...)\rangle \TRANS \langle\_,\FUN{e-n}(\_:...)\rangle`
`_ -- e-n.(_:...) -> _`	`\_ \xrightarrow{\FUNDEC{e-n}.(\_:...)} \_`

The . in the last line above should be !, ?, or omitted.

Rules

Plain CBS	CBS-LaTeX	Formatted CBS
`Rule ...`	`\KEY{Rule} ~ ...`
`Rule ... ⏎ ...`	`\begin{aligned} \KEY{Rule} ~ & ...\\ & ... \end{aligned}`
`Rule ... ⏎ ---- ⏎ ...`	`\KEY{Rule} ~ \RULE{...}{...}`
`Otherwise ...`	`\KEY{Otherwise} ~ ...`
`Assert ...`	`\KEY{Assert} ~ ...`

Formulae

Plain CBS	CBS-LaTeX	Formatted CBS
`... ~> ...`	`... \leadsto ...`
`... == ...`	`... == ...`
`... =/= ...`	`... \neq ...`
`... <: ...`	`... <: ...`
`... ---> ...`	`... \TRANS ...`
`e-n(...)\|- ...--->...`	`\FUN{e-n}(...) \vdash ...\TRANS...`
`<...,e-n(...)> ---> <...,e-n(...)>`	`\langle...,\FUN{e-n}(...)\rangle \TRANS \langle...,\FUN{e-n}(...)\rangle`
`... -- e-n.(...) -> ...`	`...\xrightarrow{\FUN{e-n}.(...)}...`

The . in the last line above should be !, ?, or omitted.

Terms

Plain CBS	CBS-LaTeX	Formatted CBS
`( )`	`( ~ )`
`'...'`	`\ATOM{text}`
`42`	`42`
`2.14`	`2.14`
`"..."`	`\STRING{text}`
`... : ...`	`... : ...`
`... => ...`	`... \TO ...`
`...+`	`...\PLUS`
`...?`	`...\QUERY`
`...*`	`...\STAR`
`... \| ...`	`... \mid ...`
`... & ...`	`... \& ...`
`...^N`	`...^{N}`
`(..., ...)`	`(..., ...)`
`[..., ...]`	`[..., ...]`
`{..., ...}`	`\{..., ...\}`
`{...\|->..., ...}`	`\{... \mapsto ..., \cdots\}`

Other specifications

Plain CBS	CBS-LaTeX	Formatted CBS
`Auxiliary K ...`	`\KEY{Auxiliary K} ~ ...`
`Built-in K ...`	`\KEY{Built-in K} ~ ...`
`Meta-variables ...`	`\KEY{Meta-variables} ~ ...`

Alignment

Plain CBS	CBS-LaTeX	Formatted CBS
`... ...`	`... \ ...`
`... ...`	`...\quad...`
`... ...`	`...\qquad...`
`... ... ⏎ ...`	`\begin{aligned} ... ~ & ... \\ ~ & ... \end{aligned}`

Generation of marked-up CBS from CBS source text is currently being implemented in Spoofax; when complete, the tool will be made freely available as an Eclipse plugin. ↩
An alternative would be to prefix all macro names with cbs. ↩
The textcomp package is automatically loaded in recent distributions. ↩
CBS section numbers are also treated as names. ↩