# HG changeset patch # User haftmann # Date 1175264339 -7200 # Node ID c5039bee260284be2c879357a86d54963d98b0ec # Parent ab23925c64d6997a58f59075677d92f7861b4653 updated diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Mar 30 16:18:59 2007 +0200 @@ -80,7 +80,7 @@ later additions in expressiveness}. As a canonical example, a polymorphic equality function @{text "eq \ \ \ \ \ bool"} which is overloaded on different - types for @{text "\"}, which is achieves by splitting introduction + types for @{text "\"}, which is achieved by splitting introduction of the @{text eq} function from its overloaded definitions by means of @{text class} and @{text instance} declarations: @@ -94,13 +94,13 @@ \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"} \medskip\noindent\hspace*{2ex}@{text "instance (\\eq, \\eq) pair \ eq where"} \\ - \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2"} + \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \ eq y1 y2"} \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\ \hspace*{4ex}@{text "less_eq \ \ \ \ \ bool"} \\ \hspace*{4ex}@{text "less \ \ \ \ \ bool"} - \medskip Type variables are annotated with (finitly many) classes; + \medskip\noindent Type variables are annotated with (finitly many) classes; these annotations are assertions that a particular polymorphic type provides definitions for overloaded functions. @@ -113,7 +113,9 @@ so, it is naturally desirable that type classes do not only provide functions (class operations) but also state specifications implementations must obey. For example, the @{text "class eq"} - above could be given the following specification: + above could be given the following specification, demanding that + @{text "class eq"} is an equivalence relation obeying reflexivity, + symmetry and transitivity: \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\ \hspace*{4ex}@{text "eq \ \ \ \ \ bool"} \\ @@ -122,7 +124,7 @@ \hspace*{4ex}@{text "sym: eq x y \ eq x y"} \\ \hspace*{4ex}@{text "trans: eq x y \ eq y z \ eq x z"} - \medskip From a theoretic point of view, type classes are leightweight + \medskip\noindent From a theoretic point of view, type classes are leightweight modules; Haskell type classes may be emulated by SML functors \cite{classes_modules}. Isabelle/Isar offers a discipline of type classes which brings @@ -137,8 +139,8 @@ \item with a direct link to the Isabelle module system (aka locales). \end{enumerate} - Isar type classes also directly support code generation - in as Haskell like fashion. + \noindent Isar type classes also directly support code generation + in a Haskell like fashion. This tutorial demonstrates common elements of structured specifications and abstract reasoning with type classes by the algebraic hierarchy of @@ -203,7 +205,7 @@ proof goals and should conveniently always be the first method applied in an instantiation proof. - Another instance of @{text "semigroup"} are the natural numbers: + \medskip Another instance of @{text "semigroup"} are the natural numbers: *} instance nat :: semigroup @@ -214,7 +216,7 @@ qed text {* - Also @{text "list"}s form a semigroup with @{const "op @"} as + \noindent Also @{text "list"}s form a semigroup with @{const "op @"} as operation: *} @@ -319,7 +321,8 @@ proof fix i :: int have "-i + i = 0" by simp - then show "i\
\ i = \" unfolding mult_int_def and neutral_int_def and inverse_int_def . + then show "i\
\ i = \" + unfolding mult_int_def and neutral_int_def and inverse_int_def . qed section {* Type classes as locales *} @@ -340,28 +343,29 @@ text {* \noindent essentially introduces the locale *} - (*<*) setup {* Sign.add_path "foo" *} (*>*) - locale idem = fixes f :: "\ \ \" assumes idem: "f (f x) = f x" -text {* \noindent together with corresponding constant(s) and axclass *} +text {* \noindent together with corresponding constant(s): *} consts f :: "\ \ \" +text {* + \noindent The connection to the type system is done by means + of a primitive axclass +*} + axclass idem < type idem: "f (f x) = f x" -text {* This axclass is coupled to the locale by means of an interpretation: *} +text {* \noindent together with a corresponding interpretation: *} interpretation idem_class: idem ["f \ ('a\idem) \ \"] by unfold_locales (rule idem) - (*<*) setup {* Sign.parent_path *} (*>*) - text {* This give you at hand the full power of the Isabelle module system; conclusions in locale @{text idem} are implicitly propagated diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Mar 30 16:18:59 2007 +0200 @@ -59,7 +59,7 @@ later additions in expressiveness}. As a canonical example, a polymorphic equality function \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different - types for \isa{{\isasymalpha}}, which is achieves by splitting introduction + types for \isa{{\isasymalpha}}, which is achieved by splitting introduction of the \isa{eq} function from its overloaded definitions by means of \isa{class} and \isa{instance} declarations: @@ -73,13 +73,13 @@ \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m} \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\ - \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isacharampersand}{\isacharampersand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} + \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\ \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} - \medskip Type variables are annotated with (finitly many) classes; + \medskip\noindent Type variables are annotated with (finitly many) classes; these annotations are assertions that a particular polymorphic type provides definitions for overloaded functions. @@ -92,7 +92,9 @@ so, it is naturally desirable that type classes do not only provide functions (class operations) but also state specifications implementations must obey. For example, the \isa{class\ eq} - above could be given the following specification: + above could be given the following specification, demanding that + \isa{class\ eq} is an equivalence relation obeying reflexivity, + symmetry and transitivity: \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\ \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ @@ -101,7 +103,7 @@ \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\ \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z} - \medskip From a theoretic point of view, type classes are leightweight + \medskip\noindent From a theoretic point of view, type classes are leightweight modules; Haskell type classes may be emulated by SML functors \cite{classes_modules}. Isabelle/Isar offers a discipline of type classes which brings @@ -116,8 +118,8 @@ \item with a direct link to the Isabelle module system (aka locales). \end{enumerate} - Isar type classes also directly support code generation - in as Haskell like fashion. + \noindent Isar type classes also directly support code generation + in a Haskell like fashion. This tutorial demonstrates common elements of structured specifications and abstract reasoning with type classes by the algebraic hierarchy of @@ -207,7 +209,7 @@ proof goals and should conveniently always be the first method applied in an instantiation proof. - Another instance of \isa{semigroup} are the natural numbers:% + \medskip Another instance of \isa{semigroup} are the natural numbers:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% @@ -237,7 +239,7 @@ \endisadelimproof % \begin{isamarkuptext}% -Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as +\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as operation:% \end{isamarkuptext}% \isamarkuptrue% @@ -489,7 +491,8 @@ \ simp\isanewline \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% +\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% @@ -537,23 +540,26 @@ \isadelimML % \endisadelimML -\isanewline \isacommand{locale}\isamarkupfalse% \ idem\ {\isacharequal}\isanewline \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% \begin{isamarkuptext}% -\noindent together with corresponding constant(s) and axclass% +\noindent together with corresponding constant(s):% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isamarkupfalse% -\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline -\isanewline +\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent The connection to the type system is done by means + of a primitive axclass% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{axclass}\isamarkupfalse% \ idem\ {\isacharless}\ type\isanewline \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% \begin{isamarkuptext}% -This axclass is coupled to the locale by means of an interpretation:% +together with a corresponding interpretation:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% @@ -566,8 +572,7 @@ % \isatagproof \isacommand{by}\isamarkupfalse% -\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline -% +\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}% \endisatagproof {\isafoldproof}% % diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 30 16:18:59 2007 +0200 @@ -26,7 +26,7 @@ for running test cases and rapid prototyping. In logical calculi like constructive type theory, a notion of executability is implicit due to the nature - of the calculus. In contrast, specifications in Isabelle/HOL + of the calculus. In contrast, specifications in Isabelle can be highly non-executable. In order to bridge the gap between logic and executable specifications, an explicit non-trivial transformation has to be applied: @@ -38,7 +38,8 @@ \qn{target language} for which code shall ultimately be generated is not fixed but may be an arbitrary state-of-the-art functional programming language (currently, the implementation - supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}). + supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell + \cite{haskell-revised-report}). We aim to provide a versatile environment suitable for software development and verification, @@ -47,9 +48,14 @@ while achieving a big coverage of application areas with maximum flexibility. - For readers, some familiarity and experience - with the ingredients - of the HOL \emph{Main} theory is assumed. + Conceptually the code generator framework is part + of Isabelle's @{text Pure} meta logic; the object logic + @{text HOL} which is an extension of @{text Pure} + already comes with a reasonable framework setup and thus provides + a good working horse for raising code-generation-driven + applications. So, we assume some familiarity and experience + with the ingredients of the @{text HOL} \emph{Main} theory + (see also \cite{isa-tutorial}). *} @@ -58,8 +64,10 @@ text {* The code generator aims to be usable with no further ado in most cases while allowing for detailed customization. - This manifests in the structure of this tutorial: this introduction - continues with a short introduction of concepts. Section + This manifests in the structure of this tutorial: + we start with a generic example \secref{sec:example} + and introduce code generation concepts \secref{sec:concept}. + Section \secref{sec:basics} explains how to use the framework naively, presuming a reasonable default setup. Then, section \secref{sec:advanced} deals with advanced topics, @@ -74,17 +82,34 @@ So, for the moment, there are two distinct code generators in Isabelle. Also note that while the framework itself is largely - object-logic independent, only HOL provides a reasonable + object-logic independent, only @{text HOL} provides a reasonable framework setup. \end{warn} *} -subsection {* An exmaple: a simple theory of search trees *} +section {* An example: a simple theory of search trees \label{sec:example} *} + +text {* + When writing executable specifications, it is convenient to use + three existing packages: the datatype package for defining + datatypes, the function package for (recursive) functions, + and the class package for overloaded definitions. + + We develope a small theory of search trees; trees are represented + as a datatype with key type @{typ "'a"} and value type @{typ "'b"}: +*} datatype ('a, 'b) searchtree = Leaf "'a\linorder" 'b | Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree" +text {* + \noindent Note that we have constrained the type of keys + to the class of total orders, @{text linorder}. + + We define @{text find} and @{text update} functions: +*} + fun find :: "('a\linorder, 'b) searchtree \ 'a \ 'b option" where "find (Leaf key val) it = (if it = key then Some val else None)" @@ -104,17 +129,29 @@ else (Branch t1 key (update (it, entry) t2)) )" +text {* + \noindent For testing purpose, we define a small example + using natural numbers @{typ nat} (which are a @{text linorder}) + as keys and strings values: +*} + fun example :: "nat \ (nat, string) searchtree" where "example n = update (n, ''bar'') (Leaf 0 ''foo'')" +text {* + \noindent Then we generate code +*} + code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML") text {* + \noindent which looks like: \lstsml{Thy/examples/tree.ML} *} -subsection {* Code generation process *} + +section {* Code generation concepts and process \label{sec:concept} *} text {* \begin{figure}[h] @@ -181,13 +218,13 @@ | "fac (Suc n) = Suc n * fac n" text {* - This executable specification is now turned to SML code: + \noindent This executable specification is now turned to SML code: *} code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML") text {* - The @{text "\"} command takes a space-separated list of + \noindent The @{text "\"} command takes a space-separated list of constants together with \qn{serialization directives} in parentheses. These start with a \qn{target language} identifier, followed by arguments, their semantics @@ -202,40 +239,11 @@ \lstsml{Thy/examples/fac.ML} The code generator will complain when a required - ingredient does not provide a executable counterpart. - This is the case if an involved type is not a datatype: -*} - -(*<*) -setup {* Sign.add_path "foo" *} -(*>*) - -typedecl 'a foo - -definition - bar :: "'a foo \ 'a \ 'a" where - "bar x y = y" - -(*<*) -hide type foo -hide const bar - -setup {* Sign.parent_path *} - -datatype 'a foo = Foo - -definition - bar :: "'a foo \ 'a \ 'a" where - "bar x y = y" -(*>*) - -code_gen bar (SML "examples/fail_type.ML") - -text {* - \noindent will result in an error. Likewise, generating code + ingredient does not provide a executable counterpart, + e.g.~generating code for constants not yielding - a defining equation will fail, e.g.~the Hilbert choice - operation @{text "SOME"}: + a defining equation (e.g.~the Hilbert choice + operation @{text "SOME"}): *} (*<*) @@ -258,6 +266,8 @@ code_gen pick_some (SML "examples/fail_const.ML") +text {* \noindent will fail. *} + subsection {* Theorem selection *} text {* @@ -271,8 +281,9 @@ \noindent which displays a table of constant with corresponding defining equations (the additional stuff displayed shall not bother us for the moment). If this table does - not provide at least one function - equation, the table of primitive definitions is searched + not provide at least one defining + equation for a particular constant, the table of primitive + definitions is searched whether it provides one. The typical HOL tools are already set up in a way that @@ -447,9 +458,13 @@ any applied transformation). A list of constants may be given; their function equations are added to the cache if not already present. + + Similarly, the @{text "\"} command shows a graph + visualizing dependencies between defining equations. *} + section {* Recipes and advanced topics \label{sec:advanced} *} text {* @@ -1020,6 +1035,14 @@ sort constraint by hand. *} + +subsection {* Constructor sets for datatypes *} + +text {* + \fixme +*} + + subsection {* Cyclic module dependencies *} text {* @@ -1147,9 +1170,8 @@ text %mlref {* \begin{mldecls} - @{index_ML_type CodegenConsts.const: "string * typ list"} \\ - @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\ - @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\ + @{index_ML_type CodegenConsts.const: "string * string option"} \\ + @{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\ \end{mldecls} \begin{description} @@ -1157,15 +1179,13 @@ \item @{ML_type CodegenConsts.const} is the identifier type: the product of a \emph{string} with a list of \emph{typs}. The \emph{string} is the constant name as represented inside Isabelle; - the \emph{typs} are a type instantiation in the sense of System F, - with canonical names for type variables. + for overloaded constants, the attached \emph{string option} + is either @{text SOME} type constructor denoting an instance, + or @{text NONE} for the polymorphic constant. - \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"} - maps a constant expression @{text "(constname, typ)"} to its canonical identifier. - - \item @{ML CodegenConsts.typ_of_inst}~@{text thy}~@{text const} - maps a canonical identifier @{text const} to a constant - expression with appropriate type. + \item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"} + maps a constant expression @{text "(constname, typ)"} + to its canonical identifier. \end{description} *} @@ -1196,7 +1216,7 @@ text %mlref {* \begin{mldecls} - @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\ + @{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\ @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\ @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ @@ -1272,7 +1292,6 @@ \begin{mldecls} @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\ @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\ - @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\ @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\ @{index_ML_structure CodegenConsts.Consttab} \\ @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\ @@ -1287,9 +1306,6 @@ \item @{ML_struct CodegenConsts.Consttab} provides table structures with constant identifiers as keys. - \item @{ML CodegenConsts.consts_of}~@{text thy}~@{text t} - returns all constant identifiers mentioned in a term @{text t}. - \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Mar 30 16:18:59 2007 +0200 @@ -49,7 +49,7 @@ for running test cases and rapid prototyping. In logical calculi like constructive type theory, a notion of executability is implicit due to the nature - of the calculus. In contrast, specifications in Isabelle/HOL + of the calculus. In contrast, specifications in Isabelle can be highly non-executable. In order to bridge the gap between logic and executable specifications, an explicit non-trivial transformation has to be applied: @@ -61,7 +61,8 @@ \qn{target language} for which code shall ultimately be generated is not fixed but may be an arbitrary state-of-the-art functional programming language (currently, the implementation - supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}). + supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell + \cite{haskell-revised-report}). We aim to provide a versatile environment suitable for software development and verification, @@ -70,9 +71,14 @@ while achieving a big coverage of application areas with maximum flexibility. - For readers, some familiarity and experience - with the ingredients - of the HOL \emph{Main} theory is assumed.% + Conceptually the code generator framework is part + of Isabelle's \isa{Pure} meta logic; the object logic + \isa{HOL} which is an extension of \isa{Pure} + already comes with a reasonable framework setup and thus provides + a good working horse for raising code-generation-driven + applications. So, we assume some familiarity and experience + with the ingredients of the \isa{HOL} \emph{Main} theory + (see also \cite{isa-tutorial}).% \end{isamarkuptext}% \isamarkuptrue% % @@ -83,8 +89,10 @@ \begin{isamarkuptext}% The code generator aims to be usable with no further ado in most cases while allowing for detailed customization. - This manifests in the structure of this tutorial: this introduction - continues with a short introduction of concepts. Section + This manifests in the structure of this tutorial: + we start with a generic example \secref{sec:example} + and introduce code generation concepts \secref{sec:concept}. + Section \secref{sec:basics} explains how to use the framework naively, presuming a reasonable default setup. Then, section \secref{sec:advanced} deals with advanced topics, @@ -99,19 +107,36 @@ So, for the moment, there are two distinct code generators in Isabelle. Also note that while the framework itself is largely - object-logic independent, only HOL provides a reasonable + object-logic independent, only \isa{HOL} provides a reasonable framework setup. \end{warn}% \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{An exmaple: a simple theory of search trees% +\isamarkupsection{An example: a simple theory of search trees \label{sec:example}% } \isamarkuptrue% +% +\begin{isamarkuptext}% +When writing executable specifications, it is convenient to use + three existing packages: the datatype package for defining + datatypes, the function package for (recursive) functions, + and the class package for overloaded definitions. + + We develope a small theory of search trees; trees are represented + as a datatype with key type \isa{{\isacharprime}a} and value type \isa{{\isacharprime}b}:% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{datatype}\isamarkupfalse% \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline -\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline -\isanewline +\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent Note that we have constrained the type of keys + to the class of total orders, \isa{linorder}. + + We define \isa{find} and \isa{update} functions:% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{fun}\isamarkupfalse% \isanewline \ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline @@ -131,21 +156,30 @@ \ \ \ \ if\ it\ {\isasymle}\ key\isanewline \ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline \ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline -\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline +\ \ \ {\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent For testing purpose, we define a small example + using natural numbers \isa{nat} (which are a \isa{linorder}) + as keys and strings values:% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{fun}\isamarkupfalse% \isanewline \ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ string{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline +\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent Then we generate code% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/tree.ML}% +\noindent which looks like: + \lstsml{Thy/examples/tree.ML}% \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Code generation process% +\isamarkupsection{Code generation concepts and process \label{sec:concept}% } \isamarkuptrue% % @@ -217,13 +251,13 @@ \ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline \ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}% \begin{isamarkuptext}% -This executable specification is now turned to SML code:% +\noindent This executable specification is now turned to SML code:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -The \isa{{\isasymCODEGEN}} command takes a space-separated list of +\noindent The \isa{{\isasymCODEGEN}} command takes a space-separated list of constants together with \qn{serialization directives} in parentheses. These start with a \qn{target language} identifier, followed by arguments, their semantics @@ -238,52 +272,11 @@ \lstsml{Thy/examples/fac.ML} The code generator will complain when a required - ingredient does not provide a executable counterpart. - This is the case if an involved type is not a datatype:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -\isanewline -% -\endisadelimML -\isacommand{typedecl}\isamarkupfalse% -\ {\isacharprime}a\ foo\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\isanewline -\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -\isanewline -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ bar\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}type{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -\noindent will result in an error. Likewise, generating code + ingredient does not provide a executable counterpart, + e.g.~generating code for constants not yielding - a defining equation will fail, e.g.~the Hilbert choice - operation \isa{SOME}:% + a defining equation (e.g.~the Hilbert choice + operation \isa{SOME}):% \end{isamarkuptext}% \isamarkuptrue% % @@ -320,6 +313,11 @@ \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\noindent will fail.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Theorem selection% } \isamarkuptrue% @@ -335,8 +333,9 @@ \noindent which displays a table of constant with corresponding defining equations (the additional stuff displayed shall not bother us for the moment). If this table does - not provide at least one function - equation, the table of primitive definitions is searched + not provide at least one defining + equation for a particular constant, the table of primitive + definitions is searched whether it provides one. The typical HOL tools are already set up in a way that @@ -578,7 +577,10 @@ \noindent print all cached defining equations (i.e.~\emph{after} any applied transformation). A list of constants may be given; their function - equations are added to the cache if not already present.% + equations are added to the cache if not already present. + + Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph + visualizing dependencies between defining equations.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1491,6 +1493,15 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Constructor sets for datatypes% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\fixme% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Cyclic module dependencies% } \isamarkuptrue% @@ -1636,9 +1647,8 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * typ list| \\ - \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const| \\ - \indexml{CodegenConsts.typ-of-inst}\verb|CodegenConsts.typ_of_inst: theory -> CodegenConsts.const -> string * typ| \\ + \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * string option| \\ + \indexml{CodegenConsts.const-of-cexpr}\verb|CodegenConsts.const_of_cexpr: theory -> string * typ -> CodegenConsts.const| \\ \end{mldecls} \begin{description} @@ -1646,15 +1656,13 @@ \item \verb|CodegenConsts.const| is the identifier type: the product of a \emph{string} with a list of \emph{typs}. The \emph{string} is the constant name as represented inside Isabelle; - the \emph{typs} are a type instantiation in the sense of System F, - with canonical names for type variables. + for overloaded constants, the attached \emph{string option} + is either \isa{SOME} type constructor denoting an instance, + or \isa{NONE} for the polymorphic constant. - \item \verb|CodegenConsts.norm_of_typ|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} - maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} to its canonical identifier. - - \item \verb|CodegenConsts.typ_of_inst|~\isa{thy}~\isa{const} - maps a canonical identifier \isa{const} to a constant - expression with appropriate type. + \item \verb|CodegenConsts.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} + maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} + to its canonical identifier. \end{description}% \end{isamarkuptext}% @@ -1720,7 +1728,7 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{CodegenData.add-func}\verb|CodegenData.add_func: thm -> theory -> theory| \\ + \indexml{CodegenData.add-func}\verb|CodegenData.add_func: bool -> thm -> theory -> theory| \\ \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\ \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\ \indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\ @@ -1812,7 +1820,6 @@ \begin{mldecls} \indexml{CodegenConsts.const-ord}\verb|CodegenConsts.const_ord: CodegenConsts.const * CodegenConsts.const -> order| \\ \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\ - \indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\ \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\ \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\ \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\ @@ -1827,9 +1834,6 @@ \item \verb|CodegenConsts.Consttab| provides table structures with constant identifiers as keys. - \item \verb|CodegenConsts.consts_of|~\isa{thy}~\isa{t} - returns all constant identifiers mentioned in a term \isa{t}. - \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/codegen.tex --- a/doc-src/IsarAdvanced/Codegen/codegen.tex Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Fri Mar 30 16:18:59 2007 +0200 @@ -33,6 +33,7 @@ \newcommand{\isasymNOTE}{\cmd{note}} \newcommand{\isasymIN}{\cmd{in}} \newcommand{\isasymCODEGEN}{\cmd{code\_gen}} +\newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}} \newcommand{\isasymCODECONST}{\cmd{code\_const}} \newcommand{\isasymCODETYPE}{\cmd{code\_type}} \newcommand{\isasymCODECLASS}{\cmd{code\_class}} @@ -44,6 +45,7 @@ \newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}} \newcommand{\isasymPRINTCODESETUP}{\cmd{print\_codesetup}} \newcommand{\isasymCODETHMS}{\cmd{code\_thms}} +\newcommand{\isasymCODEDEPS}{\cmd{code\_deps}} \newcommand{\isasymFUN}{\cmd{fun}} \newcommand{\isasymFUNCTION}{\cmd{function}} \newcommand{\isasymPRIMREC}{\cmd{primrec}} diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/codegen_process.pdf Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/codegen_process.ps --- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/codegen_process.ps Fri Mar 30 16:18:59 2007 +0200 @@ -1,5 +1,5 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005) +%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005) %%For: (haftmann) Florian Haftmann %%Title: _anonymous_0 %%Pages: (atend) @@ -369,39 +369,39 @@ stroke end grestore -% code_thm +% def_eqn gsave 10 dict begin -newpath 392 198 moveto -294 198 lineto -294 162 lineto -392 162 lineto +newpath 403 198 moveto +283 198 lineto +283 162 lineto +403 162 lineto closepath stroke gsave 10 dict begin -302 175 moveto -(code theorems) -[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52] +291 175 moveto +(defining equations) +[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52] xshow end grestore end grestore -% preprocessing -> code_thm +% preprocessing -> def_eqn newpath 236 180 moveto -252 180 268 180 284 180 curveto +248 180 260 180 273 180 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 284 184 moveto -294 180 lineto -284 177 lineto +newpath 273 184 moveto +283 180 lineto +273 177 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 284 184 moveto -294 180 lineto -284 177 lineto +newpath 273 184 moveto +283 180 lineto +273 177 lineto closepath stroke end grestore @@ -484,19 +484,19 @@ stroke end grestore -% extraction +% translation gsave 10 dict begin -343 126 41 18 ellipse_path +343 126 43 18 ellipse_path stroke gsave 10 dict begin -315 121 moveto -(extraction) -[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96] +313 121 moveto +(translation) +[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96] xshow end grestore end grestore -% code_thm -> extraction +% def_eqn -> translation newpath 343 162 moveto 343 159 343 157 343 154 curveto stroke @@ -533,7 +533,7 @@ end grestore end grestore -% extraction -> iml +% translation -> iml newpath 343 108 moveto 343 105 343 103 343 100 curveto stroke diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Mar 30 16:18:59 2007 +0200 @@ -128,14 +128,18 @@ continued by an application of a function @{text "g \ foo \ bar"}, and so on. As a canoncial example, take primitive functions enriching theories by constants and definitions: - @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory"} - and @{ML "Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory"}. + @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory +-> theory"} + and @{ML "Theory.add_defs_i: bool -> bool +-> (bstring * term) list -> theory -> theory"}. Written with naive application, an addition of a constant with a corresponding definition would look like: - @{ML "Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)"} + @{ML "Theory.add_defs_i false false [dummy_def] + (Sign.add_consts_i [dummy_const] thy)"}. With increasing numbers of applications, this code gets quite unreadable. Using composition, at least the nesting of brackets may be reduced: - @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy"} + @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i + [dummy_const]) thy"}. What remains unsatisfactory is that things are written down in the opposite order as they actually ``happen''. *} @@ -156,7 +160,7 @@ *} text {* - When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ 'a list"}, + \noindent When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ 'a list"}, the @{ML fold} combinator lifts a single function @{text "f \ 'a -> 'b -> 'b"}: @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ y |> f x\<^isub>1 |> f x\<^isub>2 |> \ |> f x\<^isub>n"} *} @@ -172,7 +176,7 @@ *} text {* - FIXME transformations involving side results + \noindent FIXME transformations involving side results *} text %mlref {* @@ -186,7 +190,9 @@ *} text {* - FIXME higher-order variants + \noindent All those linear combinators also exist in higher-order + variants which do not expect a value on the left hand side + but a function. *} text %mlref {* @@ -196,6 +202,10 @@ \end{mldecls} *} +text {* + \noindent FIXME +*} + section {* Options and partiality *} text %mlref {* @@ -211,7 +221,15 @@ \end{mldecls} *} -text FIXME +text {* + Standard selector functions on @{text option}s are provided. + The @{ML try} and @{ML can} functions provide a convenient + interface for handling exceptions -- both take as arguments + a function @{text f} together with a parameter @{text x} + and catch any exception during the evaluation of the application + of @{text f} to @{text x}, either return a lifted result + (@{ML NONE} on failure) or a boolean value (@{ML false} on failure). +*} section {* Common data structures *} diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Mar 29 14:21:47 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Mar 30 16:18:59 2007 +0200 @@ -172,14 +172,18 @@ continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar}, and so on. As a canoncial example, take primitive functions enriching theories by constants and definitions: - \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| - and \verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory|. + \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline% +\verb|-> theory| + and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline% +\verb|-> (bstring * term) list -> theory -> theory|. Written with naive application, an addition of a constant with a corresponding definition would look like: - \verb|Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)| + \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline% +\verb| (Sign.add_consts_i [dummy_const] thy)|. With increasing numbers of applications, this code gets quite unreadable. Using composition, at least the nesting of brackets may be reduced: - \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy| + \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline% +\verb| [dummy_const]) thy|. What remains unsatisfactory is that things are written down in the opposite order as they actually ``happen''.% \end{isamarkuptext}% @@ -209,7 +213,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list}, +\noindent When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list}, the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}: \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}% \end{isamarkuptext}% @@ -240,7 +244,7 @@ \endisadelimmlref % \begin{isamarkuptext}% -FIXME transformations involving side results% +\noindent FIXME transformations involving side results% \end{isamarkuptext}% \isamarkuptrue% % @@ -269,7 +273,9 @@ \endisadelimmlref % \begin{isamarkuptext}% -FIXME higher-order variants% +\noindent All those linear combinators also exist in higher-order + variants which do not expect a value on the left hand side + but a function.% \end{isamarkuptext}% \isamarkuptrue% % @@ -294,6 +300,11 @@ % \endisadelimmlref % +\begin{isamarkuptext}% +\noindent FIXME% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Options and partiality% } \isamarkuptrue% @@ -326,7 +337,13 @@ \endisadelimmlref % \begin{isamarkuptext}% -FIXME% +Standard selector functions on \isa{option}s are provided. + The \verb|try| and \verb|can| functions provide a convenient + interface for handling exceptions -- both take as arguments + a function \isa{f} together with a parameter \isa{x} + and catch any exception during the evaluation of the application + of \isa{f} to \isa{x}, either return a lifted result + (\verb|NONE| on failure) or a boolean value (\verb|false| on failure).% \end{isamarkuptext}% \isamarkuptrue% %