Link Search Menu Expand Document
\( % cbs-katex.sty % \SHADE{MATH} can be defined to produce a shaded background to highlight % inline MATH in running text: \newcommand{\SHADE}[1]{#1} % \KEY{text}, \STRING{text}, \ATOM{text}, \LEX{text} can be used in text or math mode: \newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}} \newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}} \newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}} \newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}} % The following commands produce ASCII characters that are treated specially by LaTeX: \newcommand{\HASH}{\char`\#} \newcommand{\DOLLAR}{\char`\$} \newcommand{\PERCENT}{\char`\%} \newcommand{\AMPERSAND}{\char`\&} \newcommand{\APOSTROPHE}{\char`\'} \newcommand{\BACKSLASH}{\char`\\} \newcommand{\CARET}{\char`\^} \newcommand{\UNDERSCORE}{\char`\_} \newcommand{\GRAVE}{\char`\`} \newcommand{\LEFTBRACE}{\char`\{} \newcommand{\RIGHTBRACE}{\char`\}} \newcommand{\TILDE}{\textasciitilde} % {\char`\~} % \FUN{name} highlights the name. % \FUNDEC{name} declares Name.name as the target of links to name. % \FUNREF{name} links name to the target Name.name in the current file. % \FUNHYP{url}{file}{name} links name to Name.name at url/file/index.html. % Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName}, % and \SECT{sectionnumber} % The kerns in \SUB and \VAR avoid overlaps with primes: \newcommand{\SUB}[1]{_{\kern-2mu#1}} % PLAIN \newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}} \newcommand{\VAR}[1]{\STYLE{PartVariable}{\textit{#1\kern2mu}}} \newcommand{\FUN}[1]{\STYLE{Name}{\textsf{#1}}} \newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}} \newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}} \newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}} \newcommand{\LANG}[1]{\STYLE{Language}{\textsf{#1}}} % DEC \newcommand{\DEC}[3]{\htmlId{#1:#2}{#3}} \newcommand{\VARDEC}[1]{\DEC{PartVariable}{#1}{\VAR{#1}}} \newcommand{\FUNDEC}[1]{\DEC{Name}{#1}{\FUN{#1}}} \newcommand{\SYNDEC}[1]{\DEC{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMDEC}[1]{\DEC{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTDEC}[1]{\DEC{SectionNumber}{#1}{\textsf{#1}}} % \newcommand{\LANGDEC}[1]{\DEC{Language}{#1}{\LANG{#1}}} % REF \newcommand{\REF}[3]{\href{###1:#2}{#3}} \newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}} \newcommand{\FUNREF}[1]{\REF{Name}{#1}{\FUN{#1}}} \newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}} % \newcommand{\LANGREF}[1]{\REF{Language}{#1}{\LANG{#1}}} % HYP \newcommand{\HYP}[5]{\href{#1/#2/index.html###3:#4}{#5}} \newcommand{\VARHYP}[3]{\HYP{#1}{#2}{PartVariable}{#3}{\VAR{#3}}} \newcommand{\FUNHYP}[3]{\HYP{#1}{#2}{Name}{#3}{\FUN{#3}}} \newcommand{\SYNHYP}[3]{\HYP{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}} \newcommand{\SEMHYP}[3]{\HYP{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}} \newcommand{\SECTHYP}[3]{\HYP{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}} % \newcommand{\LANGHYP}[3]{\HYP{#1}{#2}{Language}{#3}{\LANG{#3}}} % CBS-beta/math hyperlinks \newcommand\CBSBETAMATH{https://plancomps.github.io/CBS-beta/math} \newcommand\VARCBS[3]{\VARHYP{\CBSBETAMATH/#1}{#2}{#3}} \newcommand\FUNCBS[3]{\FUNHYP{\CBSBETAMATH/#1}{#2}{#3}} \newcommand\SYNCBS[3]{\SYNHYP{\CBSBETAMATH/#1}{#2}{#3}} \newcommand\SEMCBS[3]{\SEMHYP{\CBSBETAMATH/#1}{#2}{#3}} \newcommand\SECTCBS[3]{\SECTHYP{\CBSBETAMATH/#1}{#2}{#3}} % \newcommand{\LANGCBS}[3]{\LANGHYP{\CBSBETAMATH/#1}{#2}{#3}} % \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets: \newcommand{\LEFTPHRASE}{\llbracket} \newcommand{\RIGHTPHRASE}{\rrbracket} % \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are % highlighted the same as keywords: \newcommand{\LEFTGROUP}{\STYLE{Key}{(}} \newcommand{\RIGHTGROUP}{\STYLE{Key}{)}} % MATH\PLUS produces a superscript + % MATH\STAR produces a superscript * % MATH\QUERY produces a superscript ? \newcommand{\PLUS}{ {}^{\texttt{+}}} \newcommand{\STAR}{ {}^{\texttt{*}}} \newcommand{\QUERY}{ {}^{\texttt{?}}} % \RULE{premise}{conclusion} produces % premise % ---------- % conclusion \newcommand{\RULE}[2]{\mkern-2.2mu\frac{\displaystyle#1}{\displaystyle#2}} % See https://tex.stackexchange.com/questions/337328/superscripts-appear-in-various-weird-places-in-fractions % \RULE % {\begin{aligned} & premise \\ & ... \end{aligned}} % {\begin{aligned} & conclusion ... \\ & ... \end{aligned}} % produces an inference rule with left-aligned premises and split conclusion % premise % ... % -------------- % conclusion ... % ... % \TO TYPE produces => TYPE \newcommand{\TO}{\mathop{\Rightarrow}} % TERM \TRANS TERM produces TERM ---> TERM \newcommand{\TRANS}{\longrightarrow} % TERM \xrightarrow{LABEL} TERM puts the label above the long arrow \)

Samples

The following samples illustrate how plain CBS specifications can be marked up using the CBS-LaTeX macros, and the resulting PDFs and web pages.

Funcon specifications

CBS-beta/Funcons-beta/Computations/Normal/Binding:

CBS source | CBS-LaTeX | PDF | Markdown | Web

Language specifications

CBS-beta/Languages-beta/SIMPLE/SIMPLE-cbs/SIMPLE/SIMPLE-3-Statements:

CBS source | CBS-LaTeX | PDF | Markdown | Web

ASCII tests

The ASCII tests show how various characters used in language grammars are marked up using the CBS-LaTeX macros, and used to produce a PDF and a web page:

CBS source | CBS-LaTeX | PDF | Markdown | Web

Production

A literate CBS source file is a Markdown text that includes plain CBS notation in code blocks. Using the kramdown variant of Markdown, the CBS code blocks can be replaced by math blocks with LaTeX markup. The kramdown package can then transform the file completely to LaTeX (to produce a PDF), and to HTML (relying on math engines such as KaTeX or MathJax to render the embedded LaTeX in web browsers).

The current implementation of the required transformations uses Spoofax, kramdown, and pdflatex. Production of a PDF and a web page from a literate CBS source file involves the following steps.

  1. A CBS editor in Spoofax (generated from the SDF3 and NaBL2 definitions of CBS) parses all the literate CBS source files in a project,1 analysing and checking the names used in the plain CBS code blocks.

  2. A menu action in the CBS editor (implemented in Stratego) produces kramdown files with CBS-LaTeX markup in math blocks.

  3. The kramdown converter generates LaTeX document bodies from the kramdown files with the command:
    kramdown -o remove_html_tags,latex FILE.md > FILE.part.tex
    
  4. pdflatex produces PDFs from the generated LaTeX source files by inputting them in a document template with the cbs-latex package. The LaTeX definitions of the highlighting colours can be overridden using \colorlet{...}{...} (the svgnames colours are pre-loaded).

  5. The kramdown converter automatically generates HTML pages from the kramdown files when building a website on GitHub Pages (or locally) with Jekyll.

  6. KaTeX uses JavaScript and CSS in the browser to automatically render LaTeX code in HTML pages. The cbs-katex package defines the CBS-LaTeX macros for use with KaTeX, and needs to be included by the Jekyll layout (as with the source files for this website). The CSS specifications of the highlighting colours can be overridden (the standard HTML colour names can be used).

  1. The CBS grammar resembles a so-called island grammar, where the islands are the formal notation, and the water is informal text. Currently, the shores of the islands are marked by comment delimiters /*...*/ instead of the code fences used in Markdown. 


Table of contents