1\chapter{Miscellaneous Features}\label{avramisc} 2 3This section describes some of the features 4that exist for managing the interface 5% 6\index{HOL system@\HOL{} system!adjustment of user interface of} 7% 8to the \HOL{} system. 9 10\begin{itemize} 11\item The help system. 12\item The trace system for controlling feedback and printing. 13\item \holmake{}: a tool for dependency maintenance in large developments. 14\item Functions for counting the number of primitive inferences done in 15an evaluation, and timing it. 16\item A tool for embedding pretty-printed HOL theorems, terms and 17 types in \LaTeX{} documents. 18\end{itemize} 19 20\section{Help} 21 22 There are several kinds of help available in \HOL{}, all accessible 23 through the same incantation: 24 \begin{verbatim} 25 help <string>; 26 \end{verbatim} 27 28 The kinds of help available are: 29 30 \begin{description} 31 32 \item [Moscow~ML help.] \index{Moscow ML} (When using Moscow~ML~\HOL{}) 33 This is uniformly excellent. 34 Information for library routines is available, whether the library is loaded or not \emph{via} \texttt{help~"Lib"}. 35 36\item [\HOL{} overview.] This is a short summary of important information 37 about \HOL{}. 38 39\item [\HOL{} help.] This on-line help is intended to document all 40 HOL-specific functions available to the user. It is very detailed 41 and often accurate; however, it can be out-of-date, refer to earlier 42 versions of the system, or even be missing! 43 44\item [\HOL{} structure information.] For most structures in the 45 \HOL{} source, one can get a listing of the entrypoints found in the 46 accompanying signature. This is helpful for locating functions and 47 is automatically derived from the system sources, so it is alway 48 up-to-date. 49 50\item [Theory facts.] These are automatically derived from theory 51 files, so they are always up-to-date. The signature of each theory 52 is available (since theories are represented by structures in 53 \HOL{}). Also, each axiom, definition, and theorem in the theory can 54 be accessed by name in the help system; the theorem itself is given. 55\end{description} 56 57Therefore the following example queries can be made: 58 59\begin{table}[h] 60 \begin{center} 61 \begin{tabular}{|l|l|} \hline 62 \verb+help "installPP"+ & Moscow ML help \\ 63 \verb+help "hol"+ & \HOL{} overview \\ 64 \verb+help "aconv"+ & on-line \HOL{} help \\ 65 \verb+help "Tactic"+ & \HOL{} source structure information \\ 66 \verb+help "boolTheory"+ & theory structure signature \\ 67 \verb+help "list_Axiom"+ & theory structure signature and theorem 68 statement \\ \hline 69 \end{tabular} 70 \end{center} 71\end{table} 72 73\section{The Trace System} 74\index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback} 75\label{sec:traces} 76 77The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules. 78These flags are typically those that determine the level to which \HOL{} tools provide information to the user while operating. 79For example, a trace level of zero will usually make a tool remain completely 80silent while it operates. 81The tool may still raise an exception when it fails, but it won't also 82output any messages saying so. 83 84There are three core functions, all in the \ml{Feedback} structure: 85\begin{hol} 86\begin{verbatim} 87 traces : unit -> 88 {default: int, max: int, name: string, trace_level: int} list 89 90 set_trace : string -> int -> unit 91 trace : (string * int) -> ('a -> 'b) -> ('a -> 'b) 92\end{verbatim} 93\end{hol} 94 95The \ml{traces} function returns a list of all the traces in the system. 96The \ml{set\_trace} function allows the user to set a trace directly. 97The effect of this might be seen in a subsequent call to \ml{traces()}. 98Finally, the \ml{trace} function allows for a trace to be temporarily set while a function executes, restoring the trace to its old value when the function returns (whether normally, or with an exception). 99 100 101 102\section{Maintaining \HOL{} Formalizations with \holmake} 103\label{Holmake} 104\index{Holmake@\holmake|(} 105 106The purpose of \holmake{} is to maintain dependencies in a \HOL{} 107source directory. A single invocation of \holmake{} will compute 108dependencies between files, (re)compile plain ML code, (re)compile and 109execute theory scripts, and (re)compile the resulting theory modules. 110\holmake{} does not require the user to provide any explicit 111dependency information themselves. \holmake{} can be very convenient 112to use, but there are some conventions and restrictions on it that 113must be followed, described below. 114 115 116 117 118\holmake{} can be accessed through 119\begin{verbatim} 120 <hol-dir>/bin/Holmake. 121\end{verbatim} 122 123The development model that \holmake{} is designed to support is that 124there are two modes of work: theory construction and system revision. 125In `theory construction' mode, the user builds up a theory by 126interacting with HOL, perhaps over many sessions. In `system rebuild' 127mode, a component that others depend on has been altered, so all modules 128dependent on it have to be brought up to date. System rebuild mode is 129simpler so we deal with it first. 130 131\subsection{System rebuild} 132 133A system rebuild happens when an existing theory has been improved in 134some way (augmented with a new theorem, a change to a definition, 135etc.), or perhaps some support ML code has been modified or added to 136the formalization under development. The user needs to find and 137recompile just those modules affected by the change. This is what an 138invocation of \holmake{} does, by identifying the out-of-date modules 139and re-compiling and re-executing them. 140 141 142\subsection{Theory construction} 143 144To start a theory construction, some context (semantic, and also proof 145support) is established, typically by loading parent theories and 146useful libraries. In the course of building the theory, the user keeps 147track of the ML---which, for example, establishes context, makes 148definitions, builds and invokes tactics, and saves theorems---in a 149text file. This file is used to achieve inter-session persistence of 150the theory being constructed. For example, the text file resulting 151from session $n$ is ``\verb+use+''-d to start session $n+1$; after 152that, theory construction resumes. 153 154Once the user finishes the perhaps long and arduous task of constructing 155a theory, the user should 156\begin{enumerate} 157\item make the script separately compilable; 158\item invoke \holmake{}. This will (a) compile and execute the 159 script file; and (b) compile the resulting theory file. After this, 160 the theory file is available for use. 161\end{enumerate} 162 163\subsection{Making the script separately compilable} 164 165First, the invocation 166\begin{verbatim} 167 val _ = export_theory(); 168\end{verbatim} 169should be added at the end of the file. When the script is finally 170executed, this call writes the theory to disk. 171 172\index{load (ML function)@\ml{load} (\ML{} function)} 173Second, we address a crucial environmental issue: if a theory script 174has been constructed using\verb+ <holdir>/bin/hol+, then it has been 175developed in an environment where some commonly used structures, \eg, 176\verb+Tactic+, have already been loaded and opened for the user's 177convenience. When we wish to apply \holmake{} to a script developed 178in this way, we have to take some extra steps to ensure that the 179compilation environment also provides these structures. In the common 180case, this is simple; one must only add, at the head of the theory 181script, the following ``boilerplate'': 182\begin{verbatim} 183 open HolKernel Parse boolLib; 184\end{verbatim} 185This will duplicate the starting environment that one obtains with 186\verb+hol.bare+ and \linebreak \verb+hol.bare.noquote+. If the script was 187developed interactively with \texttt{hol} or \texttt{hol.noquote}, 188then one must also add 189\begin{verbatim} 190 open bossLib 191\end{verbatim} 192Now the script should be separately compilable. Invoke \holmake{} 193to check; the \ML{} compiler will flag any unaccounted-for identifiers it finds. 194The user has to resolve these, either by using the `dot' notation to 195locate the identifier for the compiler, or by \verb+open+-ing the 196relevant module. This ``compile/resolve-identifier'' loop should 197continue until \holmake{} succeeds in compiling the module. 198 199The following notes may be of some further help. 200 201\begin{enumerate} 202\item The filenames of theory scripts must follow the following 203 convention: a HOL theory script for theory ``x'' should be named 204 \texttt{xScript.sml}. When \verb+export_theory+ is called during an 205 invocation of \holmake, the files \texttt{xTheory.sig} and 206 \texttt{xTheory.sml} will be generated and then compiled. 207 208\item In \ML{}, modules are not allowed to include unbound top-level expressions. 209 Hence, something like the following is not allowed: 210\begin{verbatim} 211 new_theory "ted"; 212\end{verbatim} 213To make \ML{} happy, one must instead write something like 214\begin{verbatim} 215 val _ = new_theory "ted"; 216\end{verbatim} 217\noindent 218This is because (due to restrictions imposed by Moscow~ML\index{Moscow ML}) the script file is required to be an ML structure, and the contents of a structure must be \emph{declarations}, not expressions. 219Indeed, one is allowed to (and often will) omit the bracketing \texttt{structure~foo~=~struct} - \texttt{end} lines, but the contents of the file are still interpreted as if belonging to a structure. 220 221\index{load (ML function)@\ml{load} (\ML{} function)} 222\item In the interactive system, one has to explicitly \ml{load} modules; on the other hand, the batch compiler will load modules automatically. 223For example, in order to execute \ml{open Foo} (or refer to values in structure \ml{Foo}) in the interactive system, one must first have executed \ml{load "Foo"}. 224(This is on the assumption that structure \ml{Foo} is defined in a file \texttt{Foo.sml}.) 225Contrarily, the batch compiler will reject files having occurrences of \ml{load}, since \ml{load} is only defined for the interactive system. 226 227\item Take care not to have the string ``Theory'' embedded in the name of any of your files. 228\HOL{} generates files containing this string, and when it cleans up after itself, it removes such files using a regular expression. 229This will also remove other files with names containing ``Theory''. 230For example, if, in your development directory, you had a file of \ML{} code named \texttt{MyTheory.sml} and you were also managing a \HOL{} development there with \holmake, then \texttt{MyTheory.sml} would get deleted if \texttt{Holmake~clean} were invoked. 231 232\end{enumerate} 233 234\subsection{Summary} 235 236A complete theory construction might be performed by the following steps: 237\begin{itemize} 238\item Construct theory script, perhaps over many sessions; 239\item Transform script into separately compilable form; 240\item Invoke \holmake{} to generate the theory and compile it. 241\end{itemize} 242After that, the theory is usable as an ML module. 243This flow is demonstrated in the Euclid example of \TUTORIAL. 244 245Alternatively, and probably with the help of one of the editor modes,\footnote{There are editor modes for \texttt{emacs} and \texttt{vim}.} one can develop a theory with a script file that is always separately compilable. 246 247\subsection{What \holmake{} doesn't do} 248 249\holmake{} only works properly on the current directory. 250\holmake{} will rebuild files in the current directory if something it depends on from another directory is fresher than it is, but it will not do any analysis on files in other directories. 251 252\index{Holmake@\holmake!recursive invocation}% 253However, one can indicate that there is a dependency on other directories by using the \texttt{-I} flag, or the \texttt{INCLUDES} variable in a \texttt{Holmakefile}. 254Such a specification will cause \holmake{} to look in the specified directories for other theory files that the current directory may depend on. 255Moreover, by default \holmake{} will recursively call itself on all those ``include'' directories before doing anything in the current directory. 256In this way, one can get a staged application of \holmake{} across multiple directories.\footnote{See \emph{Recursive Make Considered 257 Harmful} by Peter Miller for why this is not ideal.} 258 259\subsection{\holmake{}'s command-line arguments} 260 261Like {\tt make}, \holmake{} takes command-line arguments corresponding 262to the targets that the user desires to build. If there are none, 263then \holmake{} will attempt to build all ML modules and HOL theories 264it can detect in the current directory. In addition, there are three 265special targets that can be used: 266\begin{description} 267\item[{\tt clean}] Removes all compiled files (unless over-ridden by a 268 make-file target of the same name, see 269 section~\ref{sec:using-Holmakefiles} below). 270\item [{\tt cleanDeps}] Removes all of the pre-computed dependency 271 files. This can be an important thing to do if, for example, you 272 have introduced a new {\tt .sig} file on top of an existing {\tt 273 .sml} file. 274\item [{\tt cleanAll}] Removes all compiled files as well as all of 275 the hidden dependency information. 276\end{description} 277 278\noindent Finally, users can directly affect the workings of \holmake{} 279with the following command-line options: 280\begin{description} 281\item[\tt -I <directory>] Look in specified directory for additional 282 Moscow~ML object files, including other HOL theories. This option 283 can be repeated, with multiple {\tt -I}'s to allow for multiple 284 directories to be referenced. As above, directories specified in 285 this way will also be rebuilt before the current targets are built. 286\item[\tt -d <file>] Ignore the given file and don't try to build it. 287 The file may be rebuilt anyway if other files you have specified 288 depend on it. This is useful to stop Holmake from attempting to 289 compile files that are interactive scripts (include use of {\tt 290 load} or {\tt use}, for example). 291\item[\texttt{-f <theory>}] Toggles whether or not a theory should be 292 built in ``fast'' mode. Fast building causes tactic proofs 293 (invocations of \texttt{prove} and \texttt{store\_thm}) to 294 automatically succeed. This lack of soundness is marked by the 295 \texttt{fast\_proof} oracle tag. This tag will appear on all 296 theorems proved in this way and all subsequent theorems that depend 297 on such theorems. \holmake's default is not to build in fast mode. 298\item[\texttt{-r}]% 299\index{Holmake@\holmake!recursive invocation}% 300Forces \holmake{} to behave recursively, overriding the \texttt{--no\_prereqs} option, and also causing \holmake{} to clean recursively in the ``includes'' directories (which is not done otherwise). 301\item[\texttt{--fast}] Makes \holmake's default be to build in fast 302 mode (see above). 303\item[{\tt --help} or {\tt -h}] Prints out a useful option summary and 304 exits. 305\item[\tt --holdir <directory>] Associate this build with the given 306 HOL directory, rather than the one this version of \holmake{} was 307 configured to use by default. 308\item[\tt --holmakefile <file>] Use the given file as a make-file. 309 See section~\ref{sec:using-Holmakefiles} below for more on this. 310\item[\texttt{--interactive} or \texttt{-i}] Causes the HOL code that 311 runs when a theory building file is executed to have the flag 312 \texttt{Globals.interactive} set to true. This will alter the diagnostic 313 output of a number of functions within the system. 314\item[\texttt{-k} or \texttt{--keep-going}] Causes \holmake{} to try 315 to build all specified targets, rather than stopping as soon as one 316 fails to build. 317\item[\texttt{--logging}] Causes \holmake{} to record the times taken 318 to build any theory files it encounters. The times are logged in a 319 file in the current directory. The name of this file includes the 320 time when \holmake{} completed, and when on a Unix system, the name 321 of the machine where the job was run. If \holmake{} exits 322 unsuccessfully, the filename is preceded by the string 323 ``\texttt{bad-}''. Each line in the log-file is of the form 324 \textit{theory-name time-taken}, with the time recorded in seconds. 325\item[\texttt{--no\_holmakefile}] Do not use a make-file, even if a file 326 called \texttt{Holmakefile} is present in the current directory. 327\item[\texttt{--no\_overlay}] Do not use an overlay file. All HOL 328 builds require the presence of a special overlay file from the 329 kernel when compiling scripts and libraries. This is not 330 appropriate for compiling code that has no connection to HOL, so 331 this option makes the compilation not use the overlay file. This 332 option is also used in building the kernel before the overlay itself 333 has been compiled. 334\item[\texttt{--no\_prereqs}]% 335\index{Holmake@\holmake!recursive invocation}% 336Do not recursively attempt to build ``include'' directories before working in the current directory. 337\item[\texttt{--no\_sigobj}] Do not link against HOL system's 338 directory of HOL system files. Use of this option goes some way 339 towards turning 340 \holmake{} into a general Moscow~ML \textsf{make} system. However, 341 it will still attempt to do ``HOL things'' with files whose names 342 end in \texttt{Script} and \texttt{Theory}. This option implies 343 \texttt{--no\_overlay}. 344\item[\texttt{--overlay <file>}] Use the given file as the overlay 345 rather than the default. 346\item[\texttt{--qof}] Standing for ``quit on failure''. If a tactic 347 fails to prove a theorem, quit the build. The default is to use 348 \texttt{mk\_thm} to assert that the failed goal is true so that the 349 build can continue and other theorems proved. 350\item[\texttt{--quiet}] Minimise the amount of output produced by 351 \holmake{}. Fatal error messages will still be written to the 352 standard error stream. Note that other programs called by \holmake{} will not 353 be affected. 354\item[{\tt --rebuild\_deps}] Forces \holmake{} to always 355 rebuild the dependency information for files it examines, whether or 356 not it thinks it needs to. This option is implemented by having 357 \holmake{} wipe all of its dependency cache (as per the 358 \texttt{cleanDeps} option above) before proceeding with the build. 359\end{description} 360 361\noindent \holmake{} should never exit with the Moscow~ML message ``Uncaught 362exception''. Such behaviour is a bug, please report it! 363 364 365\subsection{Using a make-file with \holmake} 366\label{sec:using-Holmakefiles} 367 368\holmake{} will use a make-file to augment its behaviour if one is 369present in the current directory. By default it will look for a file 370called \texttt{Holmakefile}, but it can be made to look at any file at 371all with the \texttt{--holmakefile} command-line option. The 372combination of \holmake{} and a make-file is supposed to behave as 373much as possible like a standard implementation of \textsf{make}. 374 375A make-file consists of two types of entries, variable definitions and 376rules. Outside of these entries, white-space is insignificant, but 377newline and \texttt{TAB} characters are very significant within them. 378Comments can be started with hash (\texttt{\#}) characters and last 379until the end of the line. Quoting is generally done with use of the 380back-slash (\verb+\+) character. In particular, a backslash-newline 381pair always allows a line to be continued as if the newline wasn't 382present at all. 383 384A variable definition is of the form 385\[ 386\textsl{Ident} \texttt{ = } \textsl{text} \texttt{ <NEWLINE> } 387\] 388and a rule is of the form 389\[ 390\textsl{text } \texttt{:} \textsl{ text} \texttt{ <NEWLINE>} 391(\texttt{<TAB>}\textsl{text}\texttt{ <NEWLINE>})^* 392\] 393Henceforth, the text following a \texttt{TAB} character in a rule will 394be referred to as the \emph{command text}. Text elsewhere will be 395referred to as \emph{normal text}. Normal text has comments stripped 396from it, so hash characters there must be escaped with a back-slash 397character. An \textsl{Ident} is any non-empty sequence of 398alpha-numeric characters, including the underscore (\texttt{\_}). 399 400In some contexts, normal text is interpreted as a list of words. 401These lists use white-space as element separators. If a word needs to 402include white-space itself, those white-space characters should be 403escaped with back-slashes. 404 405\newcommand{\varref}[1]{\texttt{\$(#1)}} 406\paragraph{Variable definitions} The text on the RHS of a variable 407definition can be substituted into any other context by using a 408\emph{variable reference}, of the form \varref{VARNAME}. References 409are evaluated \emph{late}, not at time of definition, so it is quite 410permissible to have forward references. On the other hand, this makes 411it impossible to write things like \[ \texttt{VAR = \varref{VAR} 412something\_new} 413\] because the evaluation of \varref{VAR} would lead to an infinite 414loop. GNU \textsf{make}'s facility for immediate 415definition of variables with \texttt{:=} is not supported. 416 417Note also that white-space around the equals-sign in a variable 418definition is stripped. This means that 419\[ 420\texttt{VAR =<whitespace><NEWLINE>} 421\] gives \texttt{VAR} the empty string as its value.\footnote{It is 422 possible to give a variable a value of pure whitespace by writing \[ 423\begin{array}{l} 424\texttt{NOTHING =}\\ 425\texttt{ONE\_SPACE = \varref{NOTHING}\textvisiblespace\hspace{1mm}\varref{NOTHING}}\\ 426\end{array}\]} 427 428Finally, note that the text inside a variable reference is itself 429evaluated. This means that one can write something like 430\varref{FOO\_\varref{OS}} and have this first expand the \texttt{OS} 431variable, presumably giving rise to some useful string (such as 432\texttt{unix}), and then have the resulting variable 433(\texttt{FOO\_unix}, say) expanded. This effectively allows the 434construction of functions by cases (define variables 435\texttt{FOO\_unix}, \texttt{FOO\_macos} etc; then use the nested 436variable reference above). If the internal variable expands to 437something containing spaces, this will not turn a normal variable 438reference into a function call (see below). On the other hand, 439if the initial reference contains a space, the function name component 440\emph{will} be expanded, allowing implementation of a function by 441cases determining which text-manipulation function should be called. 442 443\paragraph{Rules} 444Make-file rules are interpreted in the same way as by traditional 445\textsf{make}. The files specified after the colon (if any) are those 446files that each target (the files before the colon) is said to 447``depend'' on. If any of these are newer than a target, then 448\holmake{} rebuilds that target according to the commands. If there 449are no dependencies, then the commands are executed iff the 450target doesn't exist. If there are no commands, and the target is not 451of a type that \holmake{} already knows how to build, then it will 452just make sure that the dependencies are up to date (this may or 453may not create the target). If there are no commands attached to a 454rule, and the target is one that \holmake{} does know how to build, 455then the rule's extra dependencies are added to those that \holmake{} 456has managed to infer for itself, and \holmake{} will build the target 457using its built-in rule. If commands are provided for a type of file 458that \holmake{} knows how to build itself, then the make-file's 459commands and dependencies take precedence, and only they will be 460executed. 461 462If a command-line is preceded by a hyphen (\verb!-!) character, then 463the rest of the line is executed, but its error-code is ignored. 464(Normally, a command-line raising an error will cause \holmake{} to 465conclude that the target can not be built.) If a command-line is 466preceded by an at-sign (\verb!@!), then that command-line will not be 467echoed to the screen when it is run. These two options can be 468combined in either order at the start of a command-line. 469 470Command text is interpreted only minimally by \holmake. On Unix, 471back-slashes are not interpreted at all. On Windows, back-slashes 472followed by newlines are turned into spaces. Otherwise, command text 473is passed as is to the underlying command interpreter 474(\texttt{/bin/sh} say, on Unix, or \texttt{COMMAND.COM} on Windows). 475In particular, this means that hash-characters do \emph{not} start 476comments on command-lines, and such ``comments'' will be passed to the 477shell, which may or may not treat them as comments when it sees them. 478 479\paragraph{Functions} 480\index{Holmake@\holmake!functions for text-manipulation} 481\holmake{} supports some simple functions for manipulating text. All 482functions are written with the general form 483\texttt{\$(\textsl{function-name}\textvisiblespace{}\hspace{1mm}\textsl{arg}${}_1$,\textsl{arg}${}_2$\dots,\textsl{arg}${}_n$)}. 484Arguments can not include commas (use variable references to variables 485whose value are commas instead), but can otherwise be arbitrary text. 486\begin{description} 487\item[\texttt{\$(dprot arg)}] quotes (or ``protects'') the space 488 characters that occur in a string so that the string will be treated 489 as a unit if it occurs in a rule's dependency list. For example, 490 the file 491\begin{verbatim} 492 dep = foo bar 493 target: $(dep) 494 do_something 495\end{verbatim} 496 will see \texttt{target} as having two dependencies, not one, 497 because spaces are used to delimit dependencies. If a dependency's 498 name includes spaces, then this function can be used to quote them 499 for \holmake's benefit. Note that the \texttt{dprot} function 500 does \emph{not} do the same thing as \texttt{protect} on either Unix 501 or Windows systems. 502\item[\texttt{\$(findstring arg1,arg2)}] checks if \texttt{arg1} occurs 503 in (is a sub-string of) \texttt{arg2}. If it does so occur, the 504 result is \texttt{arg1}, otherwise the result is the empty string. 505\item[\texttt{\$(if arg1,arg2,arg3)}] examines \texttt{arg1}. If it 506 is the empty string, then the value of the whole is equal to the 507 value of \texttt{arg3}. Otherwise, the value is that of \texttt{arg2}. 508\item[\texttt{\$(patsubst arg1,arg2,text)}] splits \texttt{text} into component 509 words, and then transforms each word by attempting to see if it 510 matches the pattern in \texttt{arg1}. If so, it replaces that word 511 with \texttt{arg2} (suitably instantiated). If not, the word is 512 left alone. The modified words are then reassembled into a 513 white-space separated list and returned as the value. 514 515 A pattern is any piece of text including no more than one occurrence 516 of the percent~(\texttt{\%}) character. The percent character 517 matches any non-empty string. All other characters must be matched 518 literally. The instantiation for \texttt{\%} is remembered when the 519 replacement is constructed. Thus, \[ 520 \texttt{\$(patsubst \%.sml,\%.uo,\$(SMLFILES))} 521 \] turns a list of files with suffixes \texttt{.sml} into the same 522 list with the suffixes replaced with \texttt{.uo}. 523\item[\texttt{\$(protect arg)}] wraps \texttt{arg} in appropriate 524 quote characters to ensure that it will pass through the operating 525 system's command shell unscathed. This is important in the presence 526 of file-names that include spaces or other shell-significant 527 characters like less-than and greater-than. Those make-file 528 variables that point directly at executables (\texttt{MOSMLC}, 529 \texttt{MOSMLLEX} etc) are automatically protected in this way. 530 Others, which might be used in concatenation with other elements, 531 are not so protected. Thus, if \texttt{DIR} might include spaces, 532 one should write 533\begin{verbatim} 534 $(protect $(DIR)/subdirectory/program) 535\end{verbatim} 536 so that the above will be read as one unit by the underlying shell. 537\item[\texttt{\$(subst arg1,arg2,text)}] replaces every occurrence 538 of \texttt{arg1} in \texttt{text} with \texttt{arg2}. 539\end{description} 540 541\paragraph{Special and pre-defined variables} 542 543\index{Holmake@\holmake!variables in makefiles} 544If defined, the \texttt{INCLUDES} variable is used to add directories to the list of directories consulted when files are compiled and linked. 545The effect is as if the directories specified had all been included on the command-line with \texttt{-I} options. 546The \texttt{PRE\_INCLUDES} variable works similarly, but the directories specified here are placed before the \mbox{\texttt{-I <sigobj>}} option that is used in invocations of compiler. 547This option gives the user a way of over-riding code in the core distribution as the compiler will find their code before the distribution's. 548 549\index{Holmake@\holmake!recursive invocation} 550By default, directories specified in the \texttt{INCLUDES} and \texttt{PRE\_INCLUDES} directory are also built by \holmake{} before it attempts to build in the current directory. 551If the \texttt{-r} (``force recursion'') command-line flag is used, these directories are also ``clean''-ed when a cleaning target is given to \holmake{}. 552 553The \texttt{OPTIONS} variable is used for the specification of just 554four possible options (others are ignored): \texttt{NO\_SIGOBJ}, 555\texttt{NO\_OVERLAY}, \texttt{NO\_PREREQS} and 556\texttt{QUIT\_ON\_FAILURE}. The \texttt{OPTIONS} variable should be a 557list of strings, containing some of the above four options. Those 558present are enabled. These have the same effect as the corresponding 559command-line options. The \texttt{EXTRA\_CLEANS} variable is used to 560specify the name of additional files that should be deleted when a 561\texttt{Holmake clean} command is issued. 562 563Under Poly/ML, the \texttt{POLY\_CLINE\_OPTIONS} variable can be used to pass run-time options to the Poly/ML executable that is run during theory construction. 564 565Within a command, the variable \texttt{\$<} is used to stand for the 566name of the first dependency of the rule. The variable \texttt{\$@} is 567used to stand for the target of the rule. 568 569Finally there are variables that expand to program names and other 570useful information: 571\begin{description} 572\item[\texttt{CP}] This variable is replaced by an operating-system 573 appropriate program to perform a file copy. The file to be copied 574 is the first argument, the second is the place to copy to. The 575 second argument can be a directory. (Under Unix, \texttt{CP} 576 expands to \texttt{/bin/cp}; under Windows, it expands to 577 \texttt{copy}.) 578\item[\texttt{HOLDIR}] The root of the HOL installation. 579\item[\texttt{HOLMOSMLC}] This variable is replaced by an invocation 580 of the Moscow ML compiler along with the \texttt{-q} flag (necessary 581 for handling quotations), and the usual \texttt{-I} include 582 specifications (pre-includes, the hol-directory include, and the 583 normal includes). 584\item[\texttt{HOLMOSMLC-C}] This variable is the same as 585 \texttt{HOLMOSMLC} except that it finishes with a closing 586 \texttt{-c} option (hence the name) followed by the name of the 587 system's overlay file. This is needed for compilation of HOL source 588 files, but not for linking of HOL object code, which can be done 589 with \texttt{HOLMOSMLC}. 590\item[\texttt{ML\_SYSNAME}] The name of the ML system being used: 591 either \texttt{mosml} or \texttt{poly}. 592\item[\texttt{MLLEX}] This is the path of the \texttt{mllex} tool that 593 is built as part of HOL's configuration. 594\item[\texttt{MLYACC}] This is the path of the \texttt{mlyacc} tool that 595 is built as part of HOL's configuration. 596\item[\texttt{MOSMLC}] This is replaced by an invocation of the 597 compiler along with just the normal includes. 598\item[\texttt{MOSMLLEX}] This is replaced by an invocation of the 599 \texttt{mosmllex} program that comes with the Moscow ML 600 distribution. 601\item[\texttt{MOSMLYAC}] This is replaced by an invocation of the 602 \texttt{mosmlyac} program that comes with the Moscow ML 603 distribution. 604\item[\texttt{MV}] This variable is replaced by an operating-system 605 appropriate program to perform a file movement. The file to be 606 moved is the first argument, the second is the place to move to. 607 The second argument can be a directory. (Under Unix, \texttt{MV} 608 expands to \texttt{mv}; under Windows, it expands to \texttt{rename}.) 609\item[\texttt{OS}] This variable is replaced by the name of the 610 current operating system, which will be one of the strings 611 \texttt{"linux"}, \texttt{"solaris"}, \texttt{"macosx"}, 612 \texttt{"unix"} (for all other Unices), or \texttt{"winNT"}, for all 613 Microsoft Windows operating systems (those of the 21st century, 614 anyway). 615\item[\texttt{SIGOBJ}] Effectively \varref{HOLDIR}\texttt{/sigobj}, 616 where HOL object code is stored. 617 \item[\texttt{UNQUOTE}] The location of the quotation-filter executable. 618\end{description} 619The \texttt{MOSMLLEX} and \texttt{MOSMLYAC} abbreviations are really 620only useful if the originals aren't necessarily going to be on the 621user's ``path''. For backwards compatibility, the five variables 622above including the sub-string ``\texttt{MOSML}'' in their names can 623also be used by simply writing their names directly (i.e., without the 624enclosing \varref{\dots}), as long as these references occur first on 625a command-line. 626 627Under Poly/ML, commands involving the variable \texttt{MOSMLC} are interpreted ``appropriately''. 628If the behaviour is not as desired, we recommend using \texttt{ifdef~POLY}~(see below) to write rules that pertain only to HOL under Poly/ML. 629We strongly discourage the use of \texttt{MOSMLYAC} and \texttt{MOSMLLEX}, even when running HOL under Moscow~ML. 630 631If a reference is made to an otherwise undefined string, then it is 632treated as a reference to an environment variable. If there is no 633such variable in the environment, then the variable is silently given 634the empty string as its value. 635 636\paragraph{Conditional Parts of Makefiles} 637\index{Holmake@\holmake!conditional inclusion of sections} 638As in GNU~\textsf{make}, parts of a \texttt{Holmakefile} can be included or excluded dynamically, depending on tests that can be performed on strings including variables. 639% 640This is similar to the way directives such as \texttt{\#ifdef} can be used to control the C~preprocessor. 641 642There are four possible directives in a \texttt{Holmakefile}: \texttt{ifdef}, \texttt{ifndef}, \texttt{ifeq} and \texttt{ifneq}. 643% 644The versions including the extra `n' character reverse the boolean sense of the test. 645% 646Conditional directives can be chained together with \texttt{else} directives, and must be terminated by the \texttt{endif} command. 647% 648The following example is a file that only has any content if the \texttt{POLY} variable is defined, which happens when Poly/ML is the underlying \ML{} system. 649\begin{hol} 650\begin{verbatim} 651ifdef POLY 652TARGETS = target1 target2 653 654target1: dependency1 655 build_command -o target1 dependency1 656endif 657\end{verbatim} 658\end{hol} 659The next example includes chained \texttt{else} commands: 660\begin{hol} 661\begin{verbatim} 662ifeq "$(HOLDIR)" "foo" 663VAR = X 664else ifneq "$(HOLDIR)" "bar" 665VAR = Y 666else 667VAR = Z 668endif 669\end{verbatim} 670\end{hol} 671\index{ifeq (Holmake directive)@\texttt{ifeq} (Holmake directive)} 672\index{ifneq (Holmake directive)@\texttt{ifneq} (Holmake directive)} 673The \texttt{ifneq} and \texttt{ifeq} forms test for string equality. 674% 675They can be passed their arguments as in the example, or delimited with apostrophes, or in parentheses with no delimiters, as in: 676\begin{hol} 677\begin{verbatim} 678ifeq ($(HOLDIR),$(OTHERDIR)) 679VAR = value 680endif 681\end{verbatim} 682\end{hol} 683 684\index{ifdef (Holmake directive)@\texttt{ifdef} (Holmake directive)} 685\index{ifndef (Holmake directive)@\texttt{ifndef} (Holmake directive)} 686The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment. 687% 688This test is just of one level of expansion. 689% 690In the following example, \texttt{VAR} is defined even though it ultimately expands to the emptry string, but \texttt{NULL} is not. 691% 692The variable \texttt{FOOBAR} is also not defined. 693\begin{hol} 694\begin{verbatim} 695NULL = 696VAR = $(NULL) 697\end{verbatim} 698\end{hol} 699Note that environment variables with non-empty values are also considered to be defined. 700 701\index{Holmake@\holmake|)} 702 703 704\section{Generating and Using Heaps in Poly/ML \HOL{}} 705\label{sec:polyml-heaps} 706 707\index{heaps (in Poly/ML)|(} 708\index{Poly/ML} 709\index{Moscow ML} 710Poly/ML has a nice facility whereby the state of one of its interactive sessions can be stored on disk and then reloaded. 711This allows for an efficient resumption of work in a known state. 712The \HOL{} implementation uses this facility to implement the \texttt{hol} executable. 713In Poly/ML, \texttt{hol} starts immediately. 714In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}). 715 716Users can use the same basic technology to ``dump'' heaps of their own. 717Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories. 718This can make developing big mechanisations considerably more pleasant. 719 720\subsection{Generating \HOL{} Heaps} 721 722The easiest way to generate a \HOL{} heap is to use the \texttt{buildheap} executable that is built as part of the standard build process for (Poly/ML)~\HOL. 723This program takes a list of object files to include in a heap, an optional heap to build upon (use the \texttt{-b} command-line switch; the default is to use the heap behind the core \texttt{hol} executable), and an optional name for the new heap (the default is the traditional Unix \texttt{a.out}). 724Thus the command-line 725\begin{alltt} 726 buildheap -o realheap transcTheory polyTheory 727\end{alltt} 728would build a heap in the current directory called \texttt{realheap}, and would preload it with the standard theories of transcendental numbers and real-valued polynomials. 729 730A reasonable way to manage the generation of heaps is to use a \texttt{Holmakefile}. 731For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}. 732The use of the special variable \texttt{HOLHEAP} has a number of nice side effects. 733First, it makes the given file a dependency of all other products in the current directory. 734This means that the \HOL{} heap will be built first. 735Secondly, the other products in the current directory will be built on top of that heap, not the default heap behind \texttt{hol}. 736\begin{figure} 737\begin{alltt} 738 ifdef POLY 739 HOLHEAP = realheap 740 OBJNAMES = polyTheory transcTheory 741 DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES)) 742 743 $(HOLHEAP): $(DEPS) 744 $(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES) 745 endif 746\end{alltt} 747\caption{A \texttt{Holmakefile} fragment for building a custom \HOL{} heap embodying the standard real number theories. 748If the heap's dependencies are not core \HOL{} theories as they are here, then both the dependency line and the arguments to \texttt{buildheap} will need to be adjusted to link to the directory containing the files. 749For core \HOL{} theories, the dependency has to mention the \texttt{SIGOBJ} directory, but when passing arguments to \texttt{buildheap}, that information doesn't need to be provided as \texttt{SIGOBJ} is always consulted by all \HOL{} builds. 750Finally, note how the use of the \texttt{dprot} and \texttt{protect} functions will ensure that \holmake{} will do the right thing even when \texttt{HOLDIR} contains spaces.} 751\label{fig:realheap-makefile} 752\end{figure} 753 754\subsection{Using \HOL{} Heaps} 755As just described, if a \texttt{Holmakefile} specifies a \texttt{HOLHEAP}, then files in that directory will be built on top of that heap rather than the default. 756This is also true if the specified heap is in another directory (\ie, the \texttt{HOLHEAP} line might specify a file such as \texttt{otherdir/myheap}). 757In this case, the \texttt{Holmakefile} won't (shouldn't) include instructions on how to build that heap, but the advantages of that heap are still available. 758Again, that heap is also considered a dependency for all files in the current directory, so that they will be rebuilt if it is newer than they are. 759 760It is obviously important to be able to use heaps interactively. 761If the standard \texttt{hol} executable is invoked in a directory where there is a \texttt{Holmakefile} specifying a heap, the default heap will not be used and the given heap will be used instead. 762The fact that this is happening is mentioned as the interactive session begins. 763For example: 764\begin{samepage} 765\begin{alltt} 766--------------------------------------------------------------------- 767 HOL-4 [Kananaskis 8 (stdknl, built Tue Jul 24 16:48:44 2012)] 768 769 For introductory HOL help, type: help "hol"; 770--------------------------------------------------------------------- 771 772[extending loadPath with Holmakefile INCLUDES variable] 773[In non-standard heap: computability-heap] 774Poly/ML 5.4.1 Release 775> 776\end{alltt} 777\end{samepage} 778 779Finally, note that heaps are required to be built first in a directory, and that heaps embody theories or \ML{} sources that are \emph{ancestral} to the directory in which the heap occurs. 780This has the unfortunate consequence that one cannot package up a heap embodying the standard theories for the real numbers in \texttt{src/real}, but that such a heap has to built in some other directory. 781This is counter-intuitive. 782 783\index{heaps (in Poly/ML)|)} 784\section{Timing and Counting Theorems} 785 786\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|(} 787\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|(} 788\index{timing of HOL evaluations@timing of \HOL{} evaluations|(} 789 790 791\HOL{} can be made to record its use of primitive 792inferences, axioms, definitions and use of oracles. Such recording is 793enabled with the function 794 795\begin{holboxed} 796\index{counting_thms@\ml{counting\_thms}|pin} 797\begin{verbatim} 798 val counting_thms : bool -> unit 799\end{verbatim} 800\end{holboxed} 801 802\noindent (This function as with all the others in this section is 803found in the \texttt{Count} structure.) 804 805Calling \ml{counting\_thms true} enables counting, and 806\ml{counting\_thms false} disables it. The default is for counting to 807be disabled. If it is enabled, whenever \HOL{} performs a primitive 808inference (or accepts an axiom or definition) a counter is 809incremented. A total count as well as counts per primitive inference 810are maintained. The value of this counter is returned by the 811function: 812 813\begin{holboxed} 814\index{thm_count@\ml{thm\_count}|pin} 815\begin{verbatim} 816 val thm_count : unit -> 817 {ASSUME : int, REFL : int, BETA_CONV : int, SUBST : int, 818 ABS : int, DISCH : int, MP : int, INST_TYPE : int, MK_COMB : int, 819 AP_TERM : int, AP_THM : int, ALPHA : int, ETA_CONV : int, 820 SYM : int, TRANS : int, EQ_MP : int, EQ_IMP_RULE : int, 821 INST : int, SPEC : int, GEN : int, EXISTS : int, CHOOSE : int, 822 CONJ : int, CONJUNCT1 : int, CONJUNCT2 : int, DISJ1 : int, 823 DISJ2 : int, DISJ_CASES : int, NOT_INTRO : int, NOT_ELIM : int, 824 CCONTR : int, GEN_ABS : int, definition : int, axiom : int, 825 from_disk : int, oracle :int, total :int } 826\end{verbatim}\end{holboxed} 827 828\noindent This counter can be reset with the function: 829 830\begin{holboxed} 831\index{reset_thm_count@\ml{reset\_thm\_count}|pin} 832\begin{verbatim} 833 val reset_thm_count : unit -> unit 834\end{verbatim}\end{holboxed} 835 836Finally, the \texttt{Count} structure also includes another function 837which easily enables the number of inferences performed by an \ML{} 838procedure to be assessed: 839 840\begin{holboxed} 841\index{Count.apply@\ml{Count.apply}|pin} 842\begin{verbatim} 843 val apply : ('a -> 'b) -> 'a -> 'b 844\end{verbatim} 845\end{holboxed} 846 847An invocation, \ml{Count.apply f x}, applies the function \ml{f} to 848the argument \ml{x} and performs a count of inferences during this 849time. This function also records the total time taken in the 850execution of the application. 851 852For example, timing the action of \ml{numLib}'s \ml{ARITH\_CONV}: 853 854\setcounter{sessioncount}{1} 855\begin{session} 856\begin{verbatim} 857- Count.apply numLib.ARITH_CONV ``x > y ==> 2 * x > y``; 858runtime: 0.010s, gctime: 0.000s, systime: 0.000s. 859Axioms asserted: 0. 860Definitions made: 0. 861Oracle invocations: 0. 862Theorems loaded from disk: 0. 863HOL primitive inference steps: 165. 864Total: 165. 865> val it = |- x > y ==> 2 * x > y = T : thm 866\end{verbatim} 867\end{session} 868 869\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|)} 870\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|)} 871\index{timing of HOL evaluations@timing of \HOL{} evaluations|)} 872 873 874\section{Embedding \HOL{} in \LaTeX{}} 875 876\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|(} 877% 878When writing documents in \LaTeX{} about one's favourite \HOL{} development, one frequently wants to include pretty-printed terms, types and theorems from that development. 879% 880Done manually, this will typically require involved use of the \texttt{alltt} environment, and cutting and pasting from a HOL session or theory file. 881% 882The result is that one must also keep two copies of \HOL{} texts synchronised: if the \HOL{} development changes, the \LaTeX{} document should change as well. 883 884\newcommand{\munge}{\texttt{munge.exe}} 885\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})} 886% 887This manual, and error-prone process is not necessary: the standard \HOL{} distribution comes with a tool called \munge{} to automate the process, and to remove the duplicate copies of \HOL{} text. 888% 889(Strictly speaking, the distribution comes with a tool that itself creates \munge{}; see Section~\ref{sec:munger-creation} below.) 890% 891The basic philosophy is that a \LaTeX{} document can be written ``as normal'', but that three new \LaTeX{}-like commands are available to the author. 892 893The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter. 894% 895For example, one might write a document called \texttt{article.htex}. 896% 897This document contains instances of the new commands, and cannot be processed as is by \LaTeX{}. 898% 899Instead one first runs 900\begin{alltt} 901 \munge < article.htex > article.tex 902\end{alltt} 903and then runs \LaTeX{} on \texttt{article.tex}. 904% 905One would probably automate this process with a makefile of course. 906 907\subsection{Munging Commands} 908\label{sec:munging-commands} 909% need to get backslashes conveniently obscures the real names, 910% preventing the munger from seeing them, which will be useful when we 911% run the munger over this document! 912\newcommand{\holtm}{\texttt{\bs{}HOLtm}} 913\newcommand{\holty}{\texttt{\bs{}HOLty}} 914\newcommand{\holthm}{\texttt{\bs{}HOLthm}} 915\paragraph{Before Starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}. 916 917\bigskip 918There are then three commands for inserting text corresponding to \HOL{} entities into \LaTeX{} documents: \holtm, \holty{} and \holthm. 919% 920Each takes one argument, specifying something of the corresponding \HOL{} type. 921% 922In addition, options can be specified in square brackets, just as would be done with a genuine \LaTeX{} command. 923% 924For example, one can write 925\begin{alltt} 926 \holtm{}[tt]\{P(SUC n) /\bs{} q\} 927\end{alltt} 928and one will get \[ 929 \texttt{$P$ (SUC $n$) $\land$ $q$} 930\] 931or something very close to it, appearing in the resulting document.\footnote{The output is a mixture of typewriter font and math-mode characters embedded in a \texttt{\bs{}texttt} block within an \texttt{\bs{}mbox}.} 932% 933Note how the spacing in the input (nothing between the \texttt{P} and the \texttt{SUC n}) is \emph{not} reflected in the output; this is because the input is parsed and pretty-printed with \HOL{}. 934% 935This means that if the \HOL{} input is malformed, the \munge{} program will report errors. 936% 937Note also how the system knows that \texttt{P}, \texttt{n} and \texttt{q} are variables, and that \texttt{SUC} is not. 938% 939This analysis would not be possible without having \HOL{} actually parse and print the term itself. 940 941The default behaviours of each command are as follows: 942\begin{description} 943\item[\holty\{\textit{\mdseries{string}}\}] 944% 945\index{HOLty (munging command)@\holty{} (munging command)} 946% 947Parses the string argument as a type (the input must include the leading colon), and prints it. 948% 949The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}). 950\item[\holtm\{\textit{\mdseries{string}}\}] 951% 952\index{HOLtm (munging command)@\holtm{} (munging command)} 953% 954Parses the string argument as a term, and prints it. 955% 956Again, the output is wrapped in an \texttt{\bs{}mbox}. 957 958\paragraph{Important:} If the string argument includes a right-brace character 959(\ie, the character \rb, which has ASCII code 125), then it must be 960escaped by preceding it with a backslash~(\bs). Otherwise, the 961munger's lexer will incorrectly determine that the argument ends at 962that right-brace character rather than at a subsequent one. 963\item[\holthm\{\textit{\mdseries{thmspecifier}}\}] 964% 965\index{HOLthm (munging command)@\holthm{} (munging command)} 966% 967The argument should be of the form $\langle\mbox{\textit{theory}}\rangle\texttt{.}\langle{\mbox{\textit{theorem-name}}}\rangle$. 968% 969For example, \verb|\HOLthm{bool.AND_CLAUSES}|. 970% 971This prints the specified theorem with a leading turnstile. 972% 973\index{Hol_datatype@\ml{Hol\_datatype}!printing in LaTeX@printing in \LaTeX{}} 974However, as a special case, if the theorem specified is a ``datatype theorem'' (with a name of the form \texttt{datatype\_}$\langle$\textit{type-name}$\rangle$), a BNF-style description of the given type (one that has been defined with \ml{Hol\_datatype}) will be printed. 975% 976Datatype theorems with these names are automatically generated when \ml{Hol\_datatype} is run. 977 978By default, the output is \emph{not} wrapped in an \texttt{\bs{}mbox}, making it best suited for inclusion in an environment such as \texttt{alltt}. 979(The important characteristics of the \texttt{alltt} environment are that it respects layout in terms of newlines, while also allowing the insertion of \LaTeX{} commands. 980The \texttt{verbatim} environment does the former, but not the latter.) 981\end{description} 982 983\paragraph{Munging Command Options} 984\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!command options} 985There are a great many options for controlling the behaviour of each of these commands. 986% 987Some apply to all three commands, others are specific to a subset. 988% 989\newcommand{\indentoption}{\gt\gt} 990If multiple options are desired, they should be separated by commas. For example: \texttt{\holthm{}[nosp,p/t,\indentoption]\{bool.AND\_CLAUSES\}}. 991 992\begin{description} 993\item[\texttt{alltt}] Makes the argument suitable for inclusion in an \texttt{alltt} environment. 994% 995This is the default for \holthm. 996\item[\texttt{case}] (Only for use with \holtm.) 997% 998Causes the string to be parsed in such a way that any embedded \texttt{case} terms are only partly parsed, allowing their input form to appear when they are output. 999% 1000This preserves underscore-patterns, for example. 1001 1002\item[\texttt{conj}$n$] (Only for use with \holthm.) 1003Extracts the $n^{\mbox{\scriptsize th}}$ conjunct of a theorem. 1004The conjuncts are numbered starting at $1$, not $0$. 1005For example, 1006\begin{verbatim} 1007 \HOLthm[conj3]{bool.AND_CLAUSES} 1008\end{verbatim} 1009extracts the conjunct $\vdash \texttt{F} \land t \iff \texttt{F}$. 1010 1011\item[\texttt{def}] (Only for use with \holthm.) 1012% 1013Causes the theorem to be split into its constituent conjuncts, for each conjunct to have any outermost universal quantifiers removed, and for each to be printed on a line of its own. 1014% 1015The turnstiles usually printed in front of theorems are also omitted. 1016% 1017This works well with definitions (or characterising theorems) over multiple data type constructors, changing 1018\begin{alltt} 1019\(\vdash\) (FACT 0 = 1) \(\land\) (\(\forall\)\ensuremath{n}. FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n}) 1020\end{alltt} 1021into 1022\begin{alltt} 1023 FACT 0 = 1 1024 FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n} 1025\end{alltt} 1026 1027\item[\texttt{K}] (Only for use with \holtm.) 1028% 1029The argument must be the name of a theorem (as per the \holthm{} command), and the theorem should be of the form 1030\[ 1031\vdash f\;x\;t 1032\] 1033for some term $t$. 1034% 1035The command prints the term $t$. 1036% 1037\index{combinators, in HOL logic@combinators, in \HOL{} logic} 1038\index{K, the HOL constant@\ml{K}, the \HOL{} constant} 1039The expectation is that $f$ will be the combinator \holtxt{K} from \theoryimp{combin} (see Section~\ref{sec:combinTheory}), and that $x$ will be truth~(\holtxt{T}), allowing $t$ to be anything at all. 1040% 1041In this way, large complicated terms that are not themselves theorems (or even of boolean type), can be stored in \HOL{} theories, and then printed in \LaTeX{} documents. 1042 1043\item[\texttt{merge}, \texttt{nomerge}] (For use with \holtm{} and \holthm.) 1044By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error. 1045% 1046This behaviour can be frustrating when getting one's \LaTeX{} to look ``just so'', so it can be turned off with the \texttt{nomerge} option. 1047 1048Additionally, this behaviour can be turned off globally with the \texttt{--nomergeanalysis} option to the munger. 1049% 1050If this has been made the default, it may be useful to occasionally turn the merge analysis back on for a particular term or theorem; this is done with the \texttt{merge} option. 1051% 1052(In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.) 1053 1054 1055\item[\texttt{nodollarparens}] (For use with \holtm{} and \holthm.) Causes the default escaping of syntactic sugar to be suppressed. 1056\index{ escape, in HOL logic parser@\ml{\$} (escape, in \HOL{} logic parser)}% 1057\index{tokens!suppressing parsing behaviour of} 1058The default behaviour is to use parentheses, so that 1059% encode all the special characters below so that emacs font-locking has a reasonable chance of working 1060\begin{alltt} 1061 \holtm\lb\dol/\bs p\rb 1062\end{alltt} 1063would get printed as $(\land)\;\,p$. 1064Note that this doesn't reflect the default behaviour in the interactive loop, which is to use dollar-signs (as in the input above); see Section~\ref{sec:parser:architecture}. 1065However, with the \texttt{nodollarparens} option specified, nothing at all is printed to indicate that the special syntax has been ``escaped''. 1066 1067\item[\texttt{nosp}] (Only for use with \holthm.) 1068% 1069By default, arguments to \holthm{} are fully specialised (\ie, they have \ml{SPEC\_ALL} applied to them), removing outermost universal quantifiers. 1070% 1071The \texttt{nosp} option prevents this. 1072 1073\item[\texttt{nostile}] (Only for use with \holthm.) 1074% 1075By default, arguments to \holthm{} are printed with a turnstile~($\vdash$). 1076% 1077If this option is present, the turnstile is not printed (and the theorem will have its left margin three spaces further left). 1078 1079\item[\texttt{of}] (Only for use with \holty.) 1080% 1081The argument is a string that parses to a \emph{term}, not a type. 1082% 1083The behaviour is to print the type of this term. 1084% 1085Thus \texttt{\holty{}[of]\{p /\bs{} q\}} will print \texttt{bool}. 1086 1087If the string includes right-braces, they must be escaped with 1088back-slashes, just as with the arguments to \holtm. 1089 1090\item[\texttt{rule}] (Only for use with \holtm{} and \holthm.) 1091Prints a term (or a theorem's conclusion) using the \texttt{\bs{}infer} command (available as part of the \texttt{proof.sty} package). 1092This gives a nice, ``natural deduction'' presentation. 1093\index{natural deduction!presentation style for the LaTeX munger@presentation style for the \LaTeX{} munger} 1094For example, the term 1095\begin{alltt} 1096 (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r 1097\end{alltt} 1098will print as 1099\[ 1100\infer{r}{p \lor q & p \Rightarrow r & q \Rightarrow r} 1101\] 1102Conjuncts to the left of the outermost implication (if any) will be split into hypotheses separated by whitespace. 1103For large rules, this style of presentation breaks down, as there may not be enough horizontal space on the page to fit in all the hypotheses. 1104In this situation, the \texttt{stackedrule} option is appropriate. 1105 1106The term or theorem must be within a \LaTeX{} math-environment (it is typeset as if inline, with the \texttt{tt} option). 1107 1108\item[\texttt{showtypes}] (For use with \holthm{} and \holtm.) 1109% 1110Causes the term or theorem to be printed with the \texttt{types} trace set to level~1 (equivalent to having the \ml{show\_types} reference set to \ml{true}). 1111 1112\item[\texttt{stackedrule}] (For use with \holthm{} and \holtm.) 1113This is similar to the \texttt{rule} option, but causes implication hypotheses to be presented as a ``stack'', centered in a \LaTeX{} array on top of one another. 1114Thus, 1115\begin{alltt} 1116 (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r 1117\end{alltt} 1118will print as 1119\[ 1120\infer{r}{\begin{array}{c}p \lor q \\ p \Rightarrow r \\ q \Rightarrow r\end{array}} 1121\] 1122For this purely propositional example with single-letter variable names, the result looks a little odd, but if the hypotheses are textually larger, this option is indispensable. 1123 1124\item[\texttt{tt}] % 1125Causes the term to be type-set as the argument to a \LaTeX{} command \texttt{\bs{}HOLinline}. 1126% 1127The default definition for \texttt{\bs{}HOLinline} is 1128\begin{verbatim} 1129 \newcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}} 1130\end{verbatim} 1131This makes the argument suitable for inclusion in standard \LaTeX{} positions. 1132% 1133This is the default for \holtm{} and \holty. 1134% 1135(The \texttt{\bs{}HOLinline} command is defined in the \texttt{holtexbasic.sty} style file.) 1136 1137\item[\texttt{width=}$n$] Causes the argument to be typeset in lines of width $n$. 1138% 1139The default width is $63$, which seems to work well with 11pt fonts. 1140% 1141This default can also be changed at the time the \munge{} command is 1142run (see Section~\ref{sec:running-munger} below). 1143 1144\item[\texttt{-}$\mathit{name}$] 1145% 1146\index{parsing, of HOL logic@parsing, of \HOL{} logic!overloading} 1147(Only for use with \holthm{} and \holtm.) 1148This option causes the printing of the term or theorem to be done with respect to a grammar that has all overloading for $\mathit{name}$ removed. 1149For example, the command \texttt{\holtm[-+]\lb{}x + y\rb} will print as 1150\[ 1151\texttt{arithmetic\dol+}\;x\;y 1152\] 1153because the underlying constant will no longer map to the string \texttt{"+"} and, in the absence of any other mappings for it, will be printed as a fully qualified name. 1154 1155\index{integers, the HOL theory of@integers, the \HOL{} theory of} 1156If the theory of integers is loaded, then the command \texttt{\holtm[-+]\lb{}x + y:int\rb} will print as \[ 1157\texttt{int\_add}\;x\;y 1158\] 1159because the mapping from the integer addition constant to \texttt{"+"} is removed, but the mapping to \texttt{"int\_add"} remains, allowing that form to be what is printed. 1160 1161The \texttt{-} option can be useful when complicated notation involving overloads is first introduced in a document. 1162 1163\item[\texttt{\indentoption}] Indents the argument. 1164% 1165 This option only makes sense when used with the \texttt{alltt} option (the additional spaces will have no effect when inside an \texttt{\bs{}mbox}). 1166% 1167 The default indentation is two spaces; if a different indentation is desired, the option can be followed by digits specifying the number of space characters desired. 1168% 1169 For example, \texttt{\holthm{}[\indentoption10,...]\{...\}} will indent by 10 spaces. 1170 1171 Note that simply placing a command such as \holthm{} within its \texttt{alltt} block with a given indentation, for example 1172\begin{alltt} 1173 \bs{}begin\{alltt\} 1174 \holthm\{bool.AND_CLAUSES\} 1175 \bs{}end\{alltt\} 1176\end{alltt} 1177will not do the right thing if the output spans multiple lines. 1178% 1179Rather the first line of \HOL{} output will be indented, and the subsequent lines will not. 1180% 1181The \texttt{\indentoption} option lets the pretty-printer know that it is printing with a given indentation, affecting all lines of its output. 1182 1183 1184\item[$\mathit{nm}_1$\texttt{/}$\mathit{nm}_2$] (For use with \holtm{} 1185 and \holthm{}.) 1186% 1187Causes name $\mathit{nm}_1$ to be substituted for name $\mathit{nm}_2$ in the term or theorem. 1188% 1189This will rename both free and bound variables, wherever they occur throughout a term. 1190% 1191Because it uses instantiation, free variables in theorem hypotheses will get renamed, but bound variables in hypotheses are not affected. 1192% 1193(Hypotheses are not printed by default anyway of course.) 1194 1195If $\mathit{nm}_1$ and $\mathit{nm}_2$ both begin with the colon character then they are parsed as types, and type instantiation is performed on the term or theorem argument instead of variable substitution. 1196\end{description} 1197 1198 1199\subsection{Creating a Munger} 1200\label{sec:munger-creation} 1201 1202\newcommand{\mkmunge}{\texttt{mkmunge.exe}} 1203\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!creating a munger} 1204% 1205The \HOL{} distribution comes with a tool called \mkmunge. 1206% 1207This executable is used to create munge executables that behave as described in this section. 1208% 1209A typical invocation of \mkmunge{} is 1210\begin{alltt} 1211 \mkmunge \(\langle\mathit{thy}\sb{1}\rangle\)Theory ... \(\langle\mathit{thy}\sb{n}\rangle\)Theory 1212\end{alltt} 1213Each commandline argument to \mkmunge{} is the name of a \HOL{} object file, so in addition to theory files, one can also include special purpose SML such as \texttt{monadsyntax}. 1214 1215The \mkmunge{} program can also take an optional \texttt{-o} argument that is used to specify the name of the output munger (the default is \munge). For example 1216\begin{alltt} 1217 \mkmunge -o bagtexprocess bagTheory 1218\end{alltt} 1219 1220The theories specified as arguments to \mkmunge{} determine what theorems are in scope for calls to \holthm, and also determine the grammars that will govern the parsing and printing of the \HOL{} types, terms and theorems. 1221 1222 1223\subsection{Running a Munger} 1224\label{sec:running-munger} 1225 1226\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!running a munger} 1227Once created, a munger can be run as a filter command, consuming its 1228standard input, and writing to standard output. 1229% 1230It may also write error messages and warnings to its standard error. 1231 1232Thus, a standard pattern of use is something like 1233\begin{alltt} 1234 \munge < article.htex > article.tex 1235\end{alltt} 1236 1237However, there are two ways of further modifying the behaviour of the 1238munger, with command-line options. 1239 1240\paragraph{Overrides} 1241Most importantly, one can specify an ``overrides file'' to provide 1242token-to-\LaTeX{} replacements of what is pretty-printed. 1243% 1244The command-line would then look like 1245\begin{alltt} 1246 \munge overrides_file < article.htex > article.tex 1247\end{alltt} 1248The overrides file is a text file containing lines of the form 1249\begin{alltt} 1250 tok width tex 1251\end{alltt} 1252where \texttt{tok} is a \HOL{} token, \texttt{width} is a number 1253giving the width of the \LaTeX{}, and \texttt{tex} is a \LaTeX{} 1254string. 1255 1256As a very simple example, an overrides file might consist of just one 1257line: 1258\begin{alltt} 1259 pi1 2 \bs{}ensuremath\{\bs{}pi_1\} 1260\end{alltt} 1261This would cause the string \texttt{pi1} (presumably occurring in the 1262various \HOL{} entities as a variable name) to be replaced with the 1263rather prettier $\pi_1$. 1264% 1265The \texttt{2} records the fact that the 1266printer should record the provided \LaTeX{} as being 2 characters 1267wide. 1268% 1269This is important for the generation of reasonable line-breaks. 1270 1271Overrides for \HOL{} tokens can also be provided within \HOL{} 1272theories, using the 1273\texttt{TeX\_notation} command (see 1274Section~\ref{sec:holtheories-tex-ready} below). 1275 1276\paragraph{Default width} 1277A munger can specify the default width in which \HOL{} will print its 1278output with a \texttt{-w} option. 1279% 1280For example, 1281\begin{alltt} 1282 \munge -w70 < article.htex > article.tex 1283\end{alltt} 1284This default width can be overridden on a case-by-case basis with the 1285\texttt{width=} option to any of the commands within a \LaTeX{} 1286document. 1287 1288\paragraph{Preventing Merge Analysis} As mentioned above in the description of the \texttt{merge} and \texttt{nomerge} options to the \holtm{} and \holthm{} commands, the munger can be configured to not do token-merging avoidance by passing the \texttt{--nomergeanalysis} option to the munger. 1289 1290\smallskip \noindent The \texttt{-w}, \texttt{--nomergeanalysis} and 1291overrides file options can be given in any order. 1292 1293\subsection{Holindex} 1294 1295\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!Holindex} 1296Till now, it has been explained how the munger can be used as a preprocessor of \LaTeX{} sources. 1297Sometimes a tighter interaction with \LaTeX{} is beneficial. 1298Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands. 1299This allows it to generate an index of all \HOL{}-theorems, types and terms that occur in the document as well as providing citation commands for \HOL{} entities in this index. 1300Holindex can be found in \texttt{src/TeX/}. 1301There is also a demonstration file available in this directory. 1302 1303 1304\paragraph{Using Holindex} 1305To use Holindex add \texttt{\bs{}usepackage\{holindex\}} to the header 1306of the \LaTeX{} source file \texttt{article.tex}. Holindex loads the 1307\texttt{underscore} package which might cause trouble with references 1308and citations. In order to avoid problems, 1309\texttt{holindex} should be included after packages 1310like \texttt{natbib}. Holindex is used like BibTex or 1311MakeIndex. A run of \LaTeX{} on \texttt{jobname.tex} creates an 1312auxiliary file called \texttt{article.hix}. The munger is used to 1313process this file via 1314\begin{alltt} 1315 \munge -index article 1316\end{alltt} 1317This call generates two additional auxiliary files, 1318\texttt{article.tde} and \texttt{article.tid}. The following runs of 1319\LaTeX{} use these files. After modifying the source file, the munger 1320can be rerun to update \texttt{article.tde} and \texttt{article.tid}. 1321If you are using emacs with AUCTeX to write your latex files, you might 1322want to add 1323\begin{verbatim} 1324(eval-after-load "tex" '(add-to-list 'TeX-command-list 1325 '("Holindex" "munge.exe -index %s" 1326 TeX-run-background t t :help "Run Holindex") t)) 1327\end{verbatim} 1328to your emacs configuration file. This will allow 1329you to run Holindex using AUCTeX. 1330 1331\paragraph{Holindex commands} 1332\begin{description} 1333\item[\texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}}, \texttt{ 1334 \bs{}blockHOLty\{id\}}] These commands typeset the theorem, term 1335 or type with the given \texttt{id} as the argument to a \LaTeX{} 1336 command \texttt{\bs{}HOLblock}. They are intended for 1337 typesetting multiple lines in a new block. 1338 For theorem ids of the form \texttt{theory.thm} are predefined. All 1339 other ids have to be defined before usage as explained below. 1340% 1341\item[\texttt{\bs{}inlineHOLthm\{id\}}, \texttt{\bs{}inlineHOLtm\{id\}}, \texttt{\bs{}inlineHOLty\{id\}}] 1342 These commands are similar to \texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}} and \texttt{ 1343 \bs{}blockHOLty\{id\}}. However, they are intended for inline typesetting and 1344 use \texttt{\bs{}HOLinline} instead of \texttt{\bs{}HOLblock}. 1345% 1346\item[\texttt{\bs{}citeHOLthm\{id\}}, \texttt{\bs{}citeHOLtm\{id\}}, \texttt{\bs{}citeHOLty\{id\}}] 1347 These commands cite a theorem, term or type. 1348% 1349\item[\texttt{\bs{}mciteHOLthm\{id,id,...id\}}, \texttt{\bs{}mciteHOLtm\{ids\}}, \texttt{\bs{}mciteHOLty\{ids\}}] 1350 These commands cite multiple theorems, terms or types. 1351% 1352\item[\texttt{\bs{}citePureHOLthm\{id\}}, \texttt{\bs{}citePureHOLtm\{id\}}, 1353 \texttt{\bs{}citePureHOLty\{id\}}] These commands\linebreak cite a theorems, terms or types. 1354 They just typeset the number instead of the 1355 verbose form used by the \texttt{citeHOL} and \texttt{mciteHOL} commands. 1356 1357\item[\texttt{\bs{}citeHiddenHOLthm\{id\}}, 1358 \texttt{\bs{}citeHiddenHOLtm\{id\}}, 1359 \texttt{\bs{}citeHiddenHOLty\{id\}}] These commands cite a 1360 theorems, terms or types, but not typeset anything. These commands 1361 can be used to add a page to the list of pages a theorem, term or 1362 type is cited. 1363 1364 \item[\texttt{\bs{}printHOLIndex}, \texttt{\bs{}printHOLShortIndex}, 1365 \texttt{\bs{}printHOLLongIndex}] These commands typeset the index 1366 of all theorems, terms and types cited in the document. There are 1367 two types of entries in the index: long and short ones. Short 1368 entries contain a unique number, the label of the theorem, term or 1369 type and the pages it is cited. Long entries contain additionally 1370 a representation as it would be inserted by 1371 \texttt{\bs{}blockHOL...} as well as an optional description. 1372 Theorems use by default short entries, while terms and types use 1373 long ones. It is possible to change for each item whether a long 1374 or short entry should be used. \texttt{\bs{}printHOLIndex} prints 1375 the default index with mixed long and short entries. 1376 \texttt{\bs{}printHOLLongIndex} typesets just long entries and 1377 \texttt{\bs{}printHOLShortIndex} just short ones. 1378\end{description} 1379 1380 1381\paragraph{Defining and formating Terms, Types and Theorems} 1382 1383 Most of the Holindex commands require an identifier of a theorem, 1384 term or type as arguments. Theorem identifiers of the form 1385 \texttt{theory.theorem} are predefined. All other identifiers need 1386 defining. Additionally one might want to change the default 1387 formating options for these new identifiers as well as the old ones. 1388 \HOL{} definition files can be used for defining and 1389 setting the formating options of identifiers. They are used by 1390 putting the command \texttt{\bs{}useHOLfile\{\textit{filename.hdf}\}} in 1391 the header of your latex source file. These file use a syntax similar to 1392 BibTex. They consist of a list of entries of the form 1393 \begin{verbatim} 1394@EntryType{id, 1395 option = value, 1396 boolFlag, 1397 ... 1398} 1399\end{verbatim} 1400\noindent 1401There are the following entry types 1402\begin{description} 1403\item[\texttt{Thm}, \texttt{Theorem}] used to define and format a 1404 theorem. If the identifier is of the form \texttt{theory.theorem}, 1405 the \texttt{content} option can be skipped. Otherwise, the 1406 \texttt{content} option should be of this form and a new identifier 1407 is defined for the given theorem. This is for example useful if the 1408 theorem name contains special characters or if a theorem should 1409 be printed with different formatting options. 1410 \item[\texttt{Term}] 1411 used to define and format a term. 1412 \item[\texttt{Type}] 1413 used to define and format a type. 1414 \item[\texttt{Thms}, \texttt{Theorems}] used to set formating options for 1415 a list of theorems. For example one might want to print long index entries 1416 for all theorems in a specific theory. For the \texttt{Theorems} entry 1417 the \texttt{id} part of the entry is given in the form 1418 \texttt{ids = [id,id,...]}. These \texttt{ids} may be theorem ids or special 1419 ids of the form \texttt{theorem.thmprefix*}. The id 1420 \texttt{arithmetic.LESS\_EQ*} for example represents all theorem in 1421 theory \texttt{arithmetic} whose name starts with \texttt{LESS\_EQ}. 1422\end{description} 1423Options are name/value pairs. The value has to be quoted using 1424quotation marks or \HOL{}'s quotation syntax. There are the following 1425option names available: 1426\begin{description} 1427 \item[\texttt{content}] 1428 the content. For a term or type that's it's \HOL{}\ definition. 1429 For theorems it is of the form \texttt{theory.theorem}. 1430 \item[\texttt{options}] 1431 formating options for the munger as described in section~\ref{sec:munging-commands}. 1432 Please use the Holindex commands for typsetting inline or as a block instead 1433 of the options \texttt{tt} or \texttt{alltt}. 1434 \item[\texttt{label}] the label that will appear in the index. For 1435 theorems the label is by default it's name and the label given here 1436 will be added after the name. 1437 \item[\texttt{comment}] latex code that gets typeset as a comment / description 1438 for long index entries. 1439 \item[\texttt{latex}] the latex code for the item. There are very rare cases, 1440 when it might be useful to provide handwritten \LaTeX{} code instead of the one 1441 generated by the munger. This option overrides the \LaTeX{} produced by the munger. 1442 It is recommended to use it very carefully. 1443\end{description} 1444Besides options, there are also boolean flags that change the formating of entries: 1445\begin{description} 1446 \item[\texttt{force-index}] 1447 adds the entry to the index, even if it is not cited in the document. 1448 \item[\texttt{long-index}] 1449 use a long index-entry. 1450 \item[\texttt{short-index}] 1451 use a long index-entry. 1452\end{description} 1453Here is an example of such a \HOL{} definition file: 1454 1455\begin{verbatim} 1456@Term{term_id_1, 1457 content = ``SOME_FUN = SUC a < 0 /\ 0 > SUC b``, 1458 options = "width=20", 1459 label = "a short description of term from external file", 1460 comment = "some lengthy\\comment 1461 1462 with \textbf{formats} and newlines", 1463 force_index 1464} 1465 1466@Type{type_id_1, 1467 content = ``:bool`` 1468} 1469 1470@Thm{arithmetic.LESS_SUCC_EQ_COR, 1471 force-index, long-index 1472} 1473 1474@Thm{thm_1, 1475 label = "(second instance)", 1476 content = "arithmetic.LESS_SUC_EQ_COR" 1477} 1478 1479@Theorems{ 1480 ids = [arithmetic.LESS_ADD_SUC, 1481 arithmetic.LESS_EQ*], 1482 force-index 1483} 1484\end{verbatim} 1485 1486 1487\paragraph{Configuring Holindex} 1488 1489There are some commands that can be used to change the overall behaviour 1490of Holindex. They should be used in the header directly after \texttt{holindex} 1491is included. 1492\begin{description} 1493\item[\texttt{\bs{}setHOLlinewidth}] sets the default line-width. This 1494 corresponds to the \texttt{-w} option of the munger. 1495 1496\item[\texttt{\bs{}setHOLoverrides}] sets the ``overrides file'' to provide 1497token-to-\LaTeX{} replacements of what is pretty-printed. 1498 1499\item[\texttt{\bs{}useHOLfile}] 1500is used to include a \HOL{} definition file. Several such files might be 1501included. 1502\end{description} 1503 1504 1505\paragraph{Additional Documentation} 1506For more information about Holindex, please refer to 1507the demonstration file \texttt{src/TeX/holindex-demo.tex}. This file contains 1508documentation for rarely used commands as well as explanations of how to 1509customise Holindex. 1510 1511 1512\subsection{Making \HOL{} Theories \LaTeX{}-ready} 1513\label{sec:holtheories-tex-ready} 1514 1515Though one might specify all one's desired token-replacements in an \texttt{overrides} file, there is also support for specifying token replacements in the theory where tokens are first ``defined''. 1516% 1517(Of course, \emph{tokens} aren't defined \textit{per se}, but the definition of particular constants will naturally give rise to the generation of corresponding tokens when those constants appear in HOL terms, types or theorems.) 1518 1519A token's printing form is given in a script-file with the \ml{TeX\_notation} command (from the \ml{TexTokenMap} module). 1520% 1521This function has type 1522\begin{alltt} 1523 \{ hol : string, TeX : string * int \} -> unit 1524\end{alltt} 1525The \ml{hol} field specifies the string of the token as \HOL{} prints it. 1526% 1527The \ml{TeX} field specifies both the string that should be emitted into the \LaTeX{} output, and the width that this string should be considered to have (as in the \texttt{overrides} file). 1528 1529For example, in \texttt{boolScript.sml}, there are calls: 1530\begin{alltt} 1531 val _ = TeX_notation \{ hol = "!", TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\} 1532 val _ = TeX_notation \{ hol = UChar.forall, 1533 TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\} 1534\end{alltt} 1535The \texttt{UChar} structure is a local binding in the script-file that points at the standard list of UTF8-encoded Unicode strings in the distribution (\ml{UnicodeChars}). 1536% 1537Note also how the backslashes that are necessary for the \LaTeX{} command have to be doubled because they are appearing in an SML string. 1538 1539Finally, rather than mapping the token directly to the string \texttt{\bs{}forall} as one might expect, the mapping introduces another level of indirection by mapping to \texttt{\bs{}HOLTokenForall}. 1540% 1541Bindings for this, and a number of other \LaTeX{} commands are made in the file 1542\begin{alltt} 1543 src/TeX/holtexbasic.sty 1544\end{alltt} 1545which will need to be included in the \LaTeX{} source file. 1546% 1547(Such bindings can be overridden with the use of the command \texttt{\bs{}renewcommand}.) 1548 1549Finally, all theory-bindings made with \ml{TeX\_notation} can be overridden with \texttt{overrides} files referenced at the time a munger is run. 1550 1551 1552\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|)} 1553 1554%%% Local Variables: 1555%%% mode: latex 1556%%% TeX-master: "description" 1557%%% End: 1558 1559% LocalWords: HOL mechanisations HOLHEAP Holmakefile 1560