# HG changeset patch # User wenzelm # Date 1010168475 -3600 # Node ID 281aa36829d8a906708da4954bc03dcb4c0855b6 # Parent 6a07c3bf49030aa189063efd641ad7c1cff4fad4 beginnings of concrete syntax; diff -r 6a07c3bf4903 -r 281aa36829d8 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Fri Jan 04 19:20:42 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Fri Jan 04 19:21:15 2002 +0100 @@ -2,6 +2,213 @@ theory Documents = Main: (*>*) +section {* Concrete syntax \label{sec:concrete-syntax} *} + +text {* + Concerning Isabelle's ``inner'' language of simply-typed @{text + \}-calculus, the core concept of Isabelle's elaborate infrastructure + for concrete syntax is that of general \emph{mixfix + annotations}\index{mixfix annotations|bold}. Associated with any + kind of name and type declaration, mixfixes give rise both to + grammar productions for the parser and output templates for the + pretty printer. + + In full generality, the whole affair of parser and pretty printer + configuration is rather subtle. Any syntax specifications given by + end-users need to interact properly with the existing setup of + Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further + details. It is particularly important to get the precedence of new + syntactic constructs right, avoiding ambiguities with existing + elements. + + \medskip Subsequently we introduce a few simple declaration forms + that already cover the most common situations fairly well. +*} + + +subsection {* Infixes *} + +text {* + Syntax annotations may be included wherever constants are declared + directly or indirectly, including \isacommand{consts}, + \isacommand{constdefs}, or \isacommand{datatype} (for the + constructor operations). Type-constructors may be annotated as + well, although this is less frequently encountered in practice + (@{text "*"} and @{text "+"} types may come to mind). + + Infix declarations\index{infix annotations|bold} provide a useful + special case of mixfixes, where users need not care about the full + details of priorities, nesting, spacing, etc. The subsequent + example of the exclusive-or operation on boolean values illustrates + typical infix declarations. +*} + +constdefs + xor :: "bool \ bool \ bool" (infixl "[+]" 60) + "A [+] B \ (A \ \ B) \ (\ A \ B)" + +text {* + Any curried function with at least two arguments may be associated + with infix syntax: @{text "xor A B"} and @{text "A [+] B"} refer to + the same expression internally. In partial applications with less + than two operands there is a special notation with \isa{op} prefix: + @{text xor} without arguments is represented as @{text "op [+]"}; + combined with plain prefix application this turns @{text "xor A"} + into @{text "op [+] A"}. + + \medskip The string @{text [source] "[+]"} in the above declaration + refers to the bit of concrete syntax to represent the operator, + while the number @{text 60} determines the precedence of the whole + construct. + + As it happens, Isabelle/HOL already spends many popular combinations + of ASCII symbols for its own use, including both @{text "+"} and + @{text "++"}. Slightly more awkward combinations like the present + @{text "[+]"} tend to be available for user extensions. The current + arrangement of inner syntax may be inspected via + \commdx{print\protect\_syntax}, albeit its output is enormous. + + Operator precedence also needs some special considerations. The + admissible range is 0--1000. Very low or high priorities are + basically reserved for the meta-logic. Syntax of Isabelle/HOL + mainly uses the range of 10--100: the equality infix @{text "="} is + centered at 50, logical connectives (like @{text "\"} and @{text + "\"}) are below 50, and algebraic ones (like @{text "+"} and @{text + "*"}) above 50. User syntax should strive to coexist with common + HOL forms, or use the mostly unused range 100--900. + + \medskip The keyword \isakeyword{infixl} specifies an operator that + is nested to the \emph{left}: in iterated applications the more + complex expression appears on the left-hand side: @{term "A [+] B + [+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly, + \isakeyword{infixr} refers to nesting to the \emph{right}, which + would turn @{term "A [+] B [+] C"} into @{text "A [+] (B [+] C)"}. + In contrast, a \emph{non-oriented} declaration via + \isakeyword{infix} would always demand explicit parentheses. + + Many binary operations observe the associative law, so the exact + grouping does not matter. Nevertheless, formal statements need be + given in a particular format, associativity needs to be treated + explicitly within the logic. Exclusive-or is happens to be + associative, as shown below. +*} + +lemma xor_assoc: "(A [+] B) [+] C = A [+] (B [+] C)" + by (auto simp add: xor_def) + +text {* + Such rules may be used in simplification to regroup nested + expressions as required. Note that the system would actually print + the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"} + (due to nesting to the left). We have preferred to give the fully + parenthesized form in the text for clarity. +*} + +(*<*)(*FIXME*) +subsection {* Mathematical symbols \label{sec:thy-present-symbols} *} + +text {* + The limitations of the ASCII character set pose a serious + limitations for representing mathematical notation. Even worse + many handsome combinations have already been used up by HOL + itself. Luckily, Isabelle supports infinitely many \emph{named + symbols}. FIXME + +*} + +(*<*) +hide const xor +ML_setup {* Context.>> (Theory.add_path "1") *} +(*>*) +constdefs + xor :: "bool \ bool \ bool" (infixl "\" 60) + "A \ B \ (A \ \ B) \ (\ A \ B)" + +(*<*) +local +(*>*) + + +subsection {* Prefixes *} + +text {* + Prefix declarations are an even more degenerate form of mixfix + annotation, which allow a arbitrary symbolic token to be used for FIXME +*} + +datatype currency = + Euro nat ("\") + | Pounds nat ("\") + | Yen nat ("\") + | Dollar nat ("$") + +text {* + FIXME The predefined Isabelle symbols used above are \verb,\,, + \verb,\,, \verb,\,, and \verb,\,. + + The above syntax annotation makes \verb,\, stand for the + datatype constructor constant @{text Euro}, which happens to be a + function @{typ "nat \ currency"}. Using plain application syntax + we may write @{text "Euro 10"} as @{term "\ 10"}. So we already + achieve a decent syntactic representation without having to consider + arguments and precedences of general mixfix annotations -- prefixes + are already sufficient. +*} + + +subsection {* Syntax translations \label{sec:def-translations} *} + +text{* + FIXME + +\index{syntax translations|(}% +\index{translations@\isacommand {translations} (command)|(} +Isabelle offers an additional definitional facility, +\textbf{syntax translations}. +They resemble macros: upon parsing, the defined concept is immediately +replaced by its definition. This effect is reversed upon printing. For example, +the symbol @{text"\"} is defined via a syntax translation: +*} + +translations "x \ y" \ "\(x = y)" + +text{*\index{$IsaEqTrans@\isasymrightleftharpoons} +\noindent +Internally, @{text"\"} never appears. + +In addition to @{text"\"} there are +@{text"\"}\index{$IsaEqTrans1@\isasymrightharpoonup} +and @{text"\"}\index{$IsaEqTrans2@\isasymleftharpoondown} +for uni-directional translations, which only affect +parsing or printing. This tutorial will not cover the details of +translations. We have mentioned the concept merely because it +crops up occasionally; a number of HOL's built-in constructs are defined +via translations. Translations are preferable to definitions when the new +concept is a trivial variation on an existing one. For example, we +don't need to derive new theorems about @{text"\"}, since existing theorems +about @{text"="} still apply.% +\index{syntax translations|)}% +\index{translations@\isacommand {translations} (command)|)} +*} + + +section {* Document preparation *} + +subsection {* Batch-mode sessions *} + +subsection {* {\LaTeX} macros *} + +subsubsection {* Structure markup *} + +subsubsection {* Symbols and characters *} + +text {* + FIXME + + +*} + (*<*) end (*>*) +(*>*)