# HG changeset patch # User lcp # Date 766424553 -7200 # Node ID 34bc15b546e6dec19c06362757c246f8fcd8164a # Parent 361a7171317689cb6393d1e3e873562ef5f5b9f5 penultimate Springer draft diff -r 361a71713176 -r 34bc15b546e6 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Fri Apr 15 17:16:23 1994 +0200 +++ b/doc-src/Ref/theories.tex Fri Apr 15 17:42:33 1994 +0200 @@ -5,14 +5,14 @@ \index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}} Theories organize the syntax, declarations and axioms of a mathematical development. They are built, starting from the Pure theory, by extending -and merging existing theories. They have the \ML\ type \ttindex{theory}. -Theory operations signal errors by raising exception \ttindex{THEORY}, +and merging existing theories. They have the \ML\ type \mltydx{theory}. +Theory operations signal errors by raising exception \xdx{THEORY}, returning a message and a list of theories. Signatures, which contain information about sorts, types, constants and -syntax, have the \ML\ type~\ttindexbold{Sign.sg}. For identification, +syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each signature carries a unique list of {\bf stamps}, which are \ML\ -references (to strings). The strings serve as human-readable names; the +references to strings. The strings serve as human-readable names; the references serve as unique identifiers. Each primitive signature has a single stamp. When two signatures are merged, their lists of stamps are also merged. Every theory carries a unique signature. @@ -23,81 +23,108 @@ that looks for subgoals of a particular form. Terms and types may be `certified' to be well-formed with respect to a given signature. -\section{Defining Theories}\label{DefiningTheories} + +\section{Defining theories}\label{sec:ref-defining-theories} Theories can be defined either using concrete syntax or by calling certain \ML{} functions (see \S\ref{BuildingATheory}). Appendix~\ref{app:TheorySyntax} -presents the concrete syntax for theories. A theory definition consists of -several different parts: +presents the concrete syntax for theories; here is an explanation of the +constituent parts: \begin{description} -\item[{\it theoryDef}] A theory has a name $id$ and is an extension of the - union of theories with name {\it name}, the {\bf parent - theories}\indexbold{theories!parent}, with new classes, types, constants, - syntax and axioms. The basic theory, which contains only the meta-logic, - is called {\tt Pure}. +\item[{\it theoryDef}] + is the full definition. The new theory is called $id$. It is the union + of the named {\bf parent theories}\indexbold{theories!parent}, possibly + extended with new classes, etc. The basic theory, which contains only + the meta-logic, is called \thydx{Pure}. - Normally each {\it name\/} is an identifier, the precise name of the parent - theory. Strings can be used to document additional dependencies; see + Normally each {\it name\/} is an identifier, the name of the parent + theory. Strings can be used to document additional dependencies; see \S\ref{LoadingTheories} for details. -\item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass - of existing classes $id@1\dots id@n$. This rules out cyclic class - structures. Isabelle automatically computes the transitive closure of - subclass hierarchies. Hence it is not necessary to declare {\tt c < e} in - addition to {\tt c < d} and {\tt d < e}. -\item[$default$] introduces $sort$ as the new default sort for type - variables. Unconstrained type variables in an input string are - automatically constrained by $sort$; this does not apply to type variables - created internally during type inference. If omitted, the default sort is - the union of the default sorts of the parent theories. -\item[$sort$] is a finite set of classes; a single class $id$ abbreviates the - singleton set {\tt\{}$id${\tt\}}. -\item[$type$] is either the declaration of a new type (constructor) or type - synonym $name$. Only binary type constructors can have infix status and - symbolic names, e.g.\ {\tt ('a,'b)"*"}. Type constructors of $n$ arguments - are declared by $(\alpha@1,\dots,\alpha@n)name$. A {\bf type - synonym}\indexbold{types!synonyms} is simply an abbreviation - $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows - the same rules as in \ML, except that $name$ can be a string and $\tau$ - must be enclosed in quotation marks. -\item[$infix$] declares a type or constant to be an infix operator of - priority $nat$ associating to the left ({\tt infixl}) or right ({\tt - infixr}). -\item[$arities$] Each $name$ must be an existing type constructor which is + +\item[$classes$] + is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ + $id@n$} makes $id$ a subclass of the existing classes $id@1\dots + id@n$. This rules out cyclic class structures. Isabelle automatically + computes the transitive closure of subclass hierarchies; it is not + necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d < + e}. + +\item[$default$] + introduces $sort$ as the new default sort for type variables. This + applies to unconstrained type variables in an input string but not to + type variables created internally. If omitted, the default sort is the + union of the default sorts of the parent theories. + +\item[$sort$] + is a finite set of classes. A single class $id$ abbreviates the singleton + set {\tt\{}$id${\tt\}}. + +\item[$types$] + is a series of type declarations. Each declares a new type constructor + or type synonym. An $n$-place type constructor is specified by + $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to + indicate the number~$n$. + + Only 2-place type constructors can have infix status and symbolic names; + an example is {\tt ('a,'b)"*"}, which expresses binary product types. + + A {\bf type synonym}\indexbold{types!synonyms} is an abbreviation + $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where + $name$ can be a string and $\tau$ must be enclosed in quotation marks. + +\item[$infix$] + declares a type or constant to be an infix operator of priority $nat$ + associating to the left ({\tt infixl}) or right ({\tt infixr}). + +\item[$arities$] + is a series of arity declarations. Each assigns arities to type + constructors. The $name$ must be an existing type constructor, which is given the additional arity $arity$. -\item[$constDecl$] Each new constant $name$ is declared to be of type - $string$. For display purposes $mixfix$ annotations can be attached. -\item[$mixfix$] There are three forms of syntactic annotations: + +\item[$constDecl$] + is a series of constant declarations. Each new constant $name$ is given + the type specified by the $string$. The optional $mixfix$ annotations + may attach concrete syntax to the constant. + +\item[$mixfix$] \index{mixfix declarations} + annotations can take three forms: \begin{itemize} \item A mixfix template given as a $string$ of the form {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore - indicates the position where the $i$-th argument should go. The minimal - priority of each argument is given by a list of natural numbers, the - priority of the whole construct by the following natural number; - priorities are optional. + indicates the position where the $i$-th argument should go. The list + of numbers gives the priority of each argument. The final number gives + the priority of the whole construct. - \item Binary constants can be given infix status. + \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf + infix} status. - \item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\bf - binder} status: the declaration {\tt binder} $\cal Q$ $p$ causes + \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf + binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes ${\cal Q}\,x.F(x)$ to be treated like $f(F)$, where $p$ is the priority. \end{itemize} -\item[$trans$] Specifies syntactic translation rules, that is parse - rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}). -\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule - names must be distinct. -\item[$ml$] This final part of a theory consists of \ML\ code, - typically for parse and print translations. + +\item[$trans$] + specifies syntactic translation rules. There are three forms: parse + rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt ==}). + +\item[$rule$] + is a series of rule declarations. Each has a name $id$ and the + formula is given by the $string$. Rule names must be distinct. + +\item[$ml$] \index{*ML section} + consists of \ML\ code, typically for parse and print translations. \end{description} -The $mixfix$, $trans$ and $ml$ sections are explained in more detail in -the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}. +% +Chapter~\ref{chap:syntax} explains mixfix declarations, translation rules +and the {\tt ML} section in more detail. \subsection{*Classes and arities} -\index{*classes!context conditions}\index{*arities!context conditions} +\index{classes!context conditions}\index{arities!context conditions} In order to guarantee principal types~\cite{nipkow-prehofer}, -classes and arities must obey two conditions: +arity declarations must obey two conditions: \begin{itemize} \item There must be no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is @@ -124,9 +151,8 @@ \end{itemize} -\section{Loading a new theory} -\label{LoadingTheories} -\index{theories!loading} +\section{Loading a new theory}\label{LoadingTheories} +\index{theories!loading}\index{files!reading} \begin{ttbox} use_thy : string -> unit time_use_thy : string -> unit @@ -134,7 +160,7 @@ delete_tmpfiles : bool ref \hfill{\bf initially true} \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{use_thy} $thyname$] reads the theory $thyname$ and creates an \ML{} structure as described below. @@ -146,14 +172,14 @@ define a theory. This list is only used if the theory name in {\tt use_thy} does not specify the path explicitly. -\item[\ttindexbold{delete_tmpfiles} \tt:= false;] +\item[\ttindexbold{delete_tmpfiles} := false;] suppresses the deletion of temporary files. -\end{description} +\end{ttdescription} % Each theory definition must reside in a separate file. Let the file {\it tf}{\tt.thy} contain the definition of a theory called $TF$ with parent theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it - TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate \ML{} + TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes a temporary \ML{} file {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Recursive {\tt use_thy} calls load those parent theories that have not been loaded previously; the recursion may continue to any depth. One {\tt use_thy} @@ -163,7 +189,7 @@ the new theory and components $r@1$ \dots $r@n$ for the rules. The structure also contains the definitions of the {\tt ML} section, if present. The file {\tt.}{\it tf}{\tt.thy.ML} is then deleted if -\ttindexbold{delete_tmpfiles} is set to {\tt true} and no errors occurred. +{\tt delete_tmpfiles} is set to {\tt true} and no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if it exists. This file normally contains proofs involving the new theory. It is also possible to @@ -175,15 +201,22 @@ \indexbold{theories!names of}\indexbold{files!names of} \begin{warn} - Case is significant. The argument of \ttindex{use_thy} must be the exact - theory name. The corresponding filenames are derived by appending - {\tt.thy} or {\tt.ML} to the theory's name {\it after conversion to lower - case}. + Case is significant. The argument of \ttindex{use_thy} should be the + exact theory name, as defined in the theory file. The corresponding + filenames are derived by appending {\tt.thy} or {\tt.ML} to the theory's + name {\it after conversion to lower case}. +\end{warn} + +\begin{warn} + Temporary files are written to the current directory, which therefore + must be writable. Isabelle inherits the current directory from the + operating system; you can change it within Isabelle by typing + \hbox{\tt\ \ \ttindex{cd} "{\it dir}";\ \ }. \end{warn} -\section{Reloading modified theories} -\indexbold{theories!reloading}\index{*update|(} +\section{Reloading modified theories}\label{sec:reloading-theories} +\indexbold{theories!reloading} \begin{ttbox} update : unit -> unit unlink_thy : string -> unit @@ -203,7 +236,7 @@ call {\tt update()}. \end{warn} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{update} ()] reloads all modified theories and their descendants in the correct order. @@ -211,24 +244,26 @@ informs Isabelle that theory $thyname$ no longer exists. If you delete the theory files for $thyname$ then you must execute {\tt unlink_thy}; otherwise {\tt update} will complain about a missing file. -\end{description} +\end{ttdescription} -\subsection{Important note for Poly/ML users}\index{Poly/\ML} +\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} The theory mechanism depends upon reference variables. At the end of a Poly/\ML{} session, the contents of references are lost unless they are declared in the current database. Assignments to references in the {\tt Pure} database are lost, including all information about loaded theories. -To avoid losing such information (assuming you have loaded some theories) -you must declare a new {\tt Readthy} structure in the child database: +To avoid losing such information you must declare a new {\tt Readthy} +structure in the child database: \begin{ttbox} structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); Readthy.loaded_thys := !loaded_thys; open Readthy; \end{ttbox} -This copies into the new reference \verb$loaded_thys$ the contents of the -original reference, which is the list of already loaded theories. +The assignment copies into the new reference \verb$loaded_thys$ the +contents of the original reference, which is the list of already loaded +theories. You should not omit the declarations even if the parent database +has no loaded theories, since they allocate new references. \subsection{*Pseudo theories}\indexbold{theories!pseudo} @@ -236,28 +271,29 @@ dependencies. Sometimes theories depend on objects created in \ML{} files with no associated {\tt.thy} file. Unless such dependencies are documented, {\tt update} fails to reload these \ML{} files and the system is left in a -state where some objects, e.g.\ theorems, still refer to old versions of -theories. This may lead to the error +state where some objects, such as theorems, still refer to old versions of +theories. This may lead to the error \begin{ttbox} Attempt to merge different versions of theory: \(T\) \end{ttbox} -Therefore there is a way to link theories and {\em orphaned\/} \ML{} files --- +Therefore there is a way to link theories and {\bf orphaned} \ML{} files --- those without associated {\tt.thy} file. -Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a theory -$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems -that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this -dependence: +Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a +theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt b.ML} uses +theorems proved in {\tt orphan.ML}. Then {\tt b.thy} should +mention this dependence by means of a string: \begin{ttbox} B = ... + "orphan" + ... \end{ttbox} -Although {\tt orphan} is {\em not\/} used in building the base of theory $B$ -(strings stand for \ML{} files rather than {\tt.thy} files and merely document -additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is -(re)built. +Strings stand for \ML{} files rather than {\tt.thy} files, and merely +document additional dependencies. Thus {\tt orphan} is not a theory and is +not used in building the base of theory~$B$, but {\tt orphan.ML} is loaded +automatically whenever~$B$ is (re)built. -If {\tt orphan.ML} depends on theories $A@1\dots A@n$, this should be recorded -by creating a {\bf pseudo theory} in the file {\tt orphan.thy}: +The orphaned file may have its own dependencies. If {\tt orphan.ML} +depends on theories $A@1$, \ldots, $A@n$, record this by creating a {\bf + pseudo theory} in the file {\tt orphan.thy}: \begin{ttbox} orphan = A1 + \(...\) + An \end{ttbox} @@ -265,24 +301,22 @@ theory {\it orphan} whenever it reloads one of the $A@i$. For an extensive example of how this technique can be used to link over 30 -files and load them by just two {\tt use_thy} calls, consult the ZF source -files. - -\index{*update|)} +theory files and load them by just two {\tt use_thy} calls, consult the +source files of {\tt ZF} set theory. \section{Basic operations on theories} \subsection{Extracting an axiom from a theory} -\index{theories!extracting axioms|bold}\index{axioms} +\index{theories!axioms of}\index{axioms!extracting} \begin{ttbox} get_axiom: theory -> string -> thm assume_ax: theory -> string -> thm \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the given $name$ from $thy$, raising exception -\ttindex{THEORY} if none exists. Merging theories can cause several axioms +\xdx{THEORY} if none exists. Merging theories can cause several axioms to have the same name; {\tt get_axiom} returns an arbitrary one. \item[\ttindexbold{assume_ax} $thy$ $formula$] @@ -295,7 +329,7 @@ For example, if {\it formula} is \hbox{\tt a=b ==> b=a} then the resulting theorem might have the form \hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]} -\end{description} +\end{ttdescription} \subsection{Building a theory} \label{BuildingATheory} @@ -305,7 +339,7 @@ merge_theories: theory * theory -> theory extend_theory: theory -> string -> \(\cdots\) -> theory \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax of the meta-logic. There are no axioms: meta-level inferences are carried out by \ML\ functions. @@ -322,7 +356,7 @@ \begin{ttbox} Attempt to merge different versions of theory: \(T\) \end{ttbox} -\end{description} +\end{ttdescription} %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] @@ -353,11 +387,6 @@ %$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ %$rules$ & \tt[("$name$",$rule$),\dots] %\end{tabular} -% -%If theories are defined as in \S\ref{DefiningTheories}, new syntax is added -%as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can -%be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The -%latter case is not documented. \subsection{Inspecting a theory} @@ -372,7 +401,7 @@ These provide a simple means of viewing a theory's components. Unfortunately, there is no direct connection between a theorem and its theory. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{print_theory} {\it thy}] prints the theory {\it thy\/} at the terminal as a set of identifiers. @@ -390,12 +419,12 @@ \item[\ttindexbold{sign_of} $thy$] returns the signature associated with~$thy$. It is useful with functions like {\tt read_instantiate_sg}, which take a signature as an argument. -\end{description} +\end{ttdescription} \section{Terms} \index{terms|bold} -Terms belong to the \ML\ type \ttindexbold{term}, which is a concrete datatype +Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype with six constructors: there are six kinds of term. \begin{ttbox} type indexname = string * int; @@ -407,47 +436,48 @@ | Abs of string * typ * term | op $ of term * term; \end{ttbox} -\begin{description} -\item[\ttindexbold{Const}($a$, $T$)] +\begin{ttdescription} +\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold} is the {\bf constant} with name~$a$ and type~$T$. Constants include connectives like $\land$ and $\forall$ as well as constants like~0 and~$Suc$. Other constants may be required to define a logic's concrete syntax. -\item[\ttindexbold{Free}($a$, $T$)] -is the {\bf free variable} with name~$a$ and type~$T$. +\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold} + is the {\bf free variable} with name~$a$ and type~$T$. -\item[\ttindexbold{Var}($v$, $T$)] -is the {\bf scheme variable} with indexname~$v$ and type~$T$. An -\ttindexbold{indexname} is a string paired with a non-negative index, or -subscript; a term's scheme variables can be systematically renamed by -incrementing their subscripts. Scheme variables are essentially free -variables, but may be instantiated during unification. +\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold} + is the {\bf scheme variable} with indexname~$v$ and type~$T$. An + \mltydx{indexname} is a string paired with a non-negative index, or + subscript; a term's scheme variables can be systematically renamed by + incrementing their subscripts. Scheme variables are essentially free + variables, but may be instantiated during unification. -\item[\ttindexbold{Bound} $i$] -is the {\bf bound variable} with de Bruijn index~$i$, which counts the -number of lambdas, starting from zero, between a variable's occurrence and -its binding. The representation prevents capture of variables. For more -information see de Bruijn \cite{debruijn72} or -Paulson~\cite[page~336]{paulson91}. +\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold} + is the {\bf bound variable} with de Bruijn index~$i$, which counts the + number of lambdas, starting from zero, between a variable's occurrence + and its binding. The representation prevents capture of variables. For + more information see de Bruijn \cite{debruijn72} or + Paulson~\cite[page~336]{paulson91}. -\item[\ttindexbold{Abs}($a$, $T$, $u$)] -is the {\bf abstraction} with body~$u$, and whose bound variable has -name~$a$ and type~$T$. The name is used only for parsing and printing; it -has no logical significance. +\item[\ttindexbold{Abs}($a$, $T$, $u$)] + \index{lambda abs@$\lambda$-abstractions|bold} + is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound + variable has name~$a$ and type~$T$. The name is used only for parsing + and printing; it has no logical significance. -\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold} +\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold} is the {\bf application} of~$t$ to~$u$. -\end{description} +\end{ttdescription} Application is written as an infix operator to aid readability. -Here is an \ML\ pattern to recognize first-order formula of +Here is an \ML\ pattern to recognize first-order formulae of the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: \begin{ttbox} Const("Trueprop",_) $ (Const("op -->",_) $ A $ B) \end{ttbox} -\section{Terms and variable binding} +\section{Variable binding} \begin{ttbox} loose_bnos : term -> int list incr_boundvars : int -> term -> term @@ -457,7 +487,7 @@ \end{ttbox} These functions are all concerned with the de Bruijn representation of bound variables. -\begin{description} +\begin{ttdescription} \item[\ttindexbold{loose_bnos} $t$] returns the list of all dangling bound variable references. In particular, {\tt Bound~0} is loose unless it is enclosed in an @@ -503,7 +533,7 @@ if the corresponding subterms are. \end{itemize} -\end{description} +\end{ttdescription} \section{Certified terms}\index{terms!certified|bold}\index{signatures} A term $t$ can be {\bf certified} under a signature to ensure that every @@ -512,23 +542,23 @@ well-typed and its use of bound variables must be well-formed. Meta-rules such as {\tt forall_elim} take certified terms as arguments. -Certified terms belong to the abstract type \ttindexbold{cterm}. +Certified terms belong to the abstract type \mltydx{cterm}. Elements of the type can only be created through the certification process. In case of error, Isabelle raises exception~\ttindex{TERM}\@. \subsection{Printing terms} -\index{printing!terms|bold} +\index{terms!printing of} \begin{ttbox} string_of_cterm : cterm -> string Sign.string_of_term : Sign.sg -> term -> string \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{string_of_cterm} $ct$] displays $ct$ as a string. \item[\ttindexbold{Sign.string_of_term} $sign$ $t$] displays $t$ as a string, using the syntax of~$sign$. -\end{description} +\end{ttdescription} \subsection{Making and inspecting certified terms} \begin{ttbox} @@ -536,7 +566,7 @@ read_cterm : Sign.sg -> string * typ -> cterm rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\} \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies $t$ with respect to signature~$sign$. @@ -549,11 +579,11 @@ decomposes $ct$ as a record containing its type, the term itself, its signature, and the maximum subscript of its unknowns. The type and maximum subscript are computed during certification. -\end{description} +\end{ttdescription} \section{Types}\index{types|bold} -Types belong to the \ML\ type \ttindexbold{typ}, which is a concrete +Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with three constructor functions. These correspond to type constructors, free type variables and schematic type variables. Types are classified by sorts, which are lists of classes. A class is represented by @@ -569,23 +599,23 @@ infixr 5 -->; fun S --> T = Type("fun",[S,T]); \end{ttbox} -\begin{description} -\item[\ttindexbold{Type}($a$, $Ts$)] -applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. -Type constructors include~\ttindexbold{fun}, the binary function space -constructor, as well as nullary type constructors such -as~\ttindexbold{prop}. Other type constructors may be introduced. In -expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient -shorthand for function types. +\begin{ttdescription} +\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold} + applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. + Type constructors include~\tydx{fun}, the binary function space + constructor, as well as nullary type constructors such as~\tydx{prop}. + Other type constructors may be introduced. In expressions, but not in + patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function + types. -\item[\ttindexbold{TFree}($a$, $s$)] -is the {\bf free type variable} with name~$a$ and sort~$s$. +\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold} + is the {\bf type variable} with name~$a$ and sort~$s$. -\item[\ttindexbold{TVar}($v$, $s$)] -is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme -type variables are essentially free type variables, but may be instantiated -during unification. -\end{description} +\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold} + is the {\bf type unknown} with indexname~$v$ and sort~$s$. + Type unknowns are essentially free type variables, but may be + instantiated during unification. +\end{ttdescription} \section{Certified types} @@ -594,18 +624,18 @@ \ttindexbold{ctyp}. \subsection{Printing types} -\index{printing!types|bold} +\index{types!printing of} \begin{ttbox} string_of_ctyp : ctyp -> string Sign.string_of_typ : Sign.sg -> typ -> string \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{string_of_ctyp} $cT$] displays $cT$ as a string. \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] displays $T$ as a string, using the syntax of~$sign$. -\end{description} +\end{ttdescription} \subsection{Making and inspecting certified types} @@ -613,12 +643,12 @@ ctyp_of : Sign.sg -> typ -> ctyp rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\} \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies $T$ with respect to signature~$sign$. \item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record containing the type itself and its signature. -\end{description} +\end{ttdescription} \index{theories|)}