1.1 --- a/doc-src/IsarImplementation/IsaMakefile Fri Oct 22 20:43:48 2010 +0100
1.2 +++ b/doc-src/IsarImplementation/IsaMakefile Fri Oct 22 20:51:45 2010 +0100
1.3 @@ -21,10 +21,10 @@
1.4
1.5 Thy: $(LOG)/HOL-Thy.gz
1.6
1.7 -$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \
1.8 +$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \
1.9 Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy \
1.10 Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy \
1.11 - Thy/ML_old.thy ../antiquote_setup.ML
1.12 + ../antiquote_setup.ML
1.13 @$(USEDIR) HOL Thy
1.14 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
1.15 Thy/document/pdfsetup.sty Thy/document/session.tex
2.1 --- a/doc-src/IsarImplementation/Thy/ML_old.thy Fri Oct 22 20:43:48 2010 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,321 +0,0 @@
2.4 -theory ML_old
2.5 -imports Base
2.6 -begin
2.7 -
2.8 -chapter {* Advanced ML programming *}
2.9 -
2.10 -section {* Style *}
2.11 -
2.12 -text {*
2.13 - Like any style guide, also this one should not be interpreted dogmatically, but
2.14 - with care and discernment. It consists of a collection of
2.15 - recommendations which have been turned out useful over long years of
2.16 - Isabelle system development and are supposed to support writing of readable
2.17 - and managable code. Special cases encourage derivations,
2.18 - as far as you know what you are doing.
2.19 - \footnote{This style guide is loosely based on
2.20 - \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}}
2.21 -
2.22 - \begin{description}
2.23 -
2.24 - \item[fundamental law of programming]
2.25 - Whenever writing code, keep in mind: A program is
2.26 - written once, modified ten times, and read
2.27 - hundred times. So simplify its writing,
2.28 - always keep future modifications in mind,
2.29 - and never jeopardize readability. Every second you hesitate
2.30 - to spend on making your code more clear you will
2.31 - have to spend ten times understanding what you have
2.32 - written later on.
2.33 -
2.34 - \item[white space matters]
2.35 - Treat white space in your code as if it determines
2.36 - the meaning of code.
2.37 -
2.38 - \begin{itemize}
2.39 -
2.40 - \item The space bar is the easiest key to find on the keyboard,
2.41 - press it as often as necessary. @{verbatim "2 + 2"} is better
2.42 - than @{verbatim "2+2"}, likewise @{verbatim "f (x, y)"} is
2.43 - better than @{verbatim "f(x,y)"}.
2.44 -
2.45 - \item Restrict your lines to 80 characters. This will allow
2.46 - you to keep the beginning of a line in view while watching
2.47 - its end.\footnote{To acknowledge the lax practice of
2.48 - text editing these days, we tolerate as much as 100
2.49 - characters per line, but anything beyond 120 is not
2.50 - considered proper source text.}
2.51 -
2.52 - \item Ban tabulators; they are a context-sensitive formatting
2.53 - feature and likely to confuse anyone not using your favorite
2.54 - editor.\footnote{Some modern programming language even
2.55 - forbid tabulators altogether according to the formal syntax
2.56 - definition.}
2.57 -
2.58 - \item Get rid of trailing whitespace. Instead, do not
2.59 - suppress a trailing newline at the end of your files.
2.60 -
2.61 - \item Choose a generally accepted style of indentation,
2.62 - then use it systematically throughout the whole
2.63 - application. An indentation of two spaces is appropriate.
2.64 - Avoid dangling indentation.
2.65 -
2.66 - \end{itemize}
2.67 -
2.68 - \item[cut-and-paste succeeds over copy-and-paste]
2.69 - \emph{Never} copy-and-paste code when programming. If you
2.70 - need the same piece of code twice, introduce a
2.71 - reasonable auxiliary function (if there is no
2.72 - such function, very likely you got something wrong).
2.73 - Any copy-and-paste will turn out to be painful
2.74 - when something has to be changed later on.
2.75 -
2.76 - \item[comments]
2.77 - are a device which requires careful thinking before using
2.78 - it. The best comment for your code should be the code itself.
2.79 - Prefer efforts to write clear, understandable code
2.80 - over efforts to explain nasty code.
2.81 -
2.82 - \item[functional programming is based on functions]
2.83 - Model things as abstract as appropriate. Avoid unnecessarrily
2.84 - concrete datatype representations. For example, consider a function
2.85 - taking some table data structure as argument and performing
2.86 - lookups on it. Instead of taking a table, it could likewise
2.87 - take just a lookup function. Accustom
2.88 - your way of coding to the level of expressiveness a functional
2.89 - programming language is giving onto you.
2.90 -
2.91 - \item[tuples]
2.92 - are often in the way. When there is no striking argument
2.93 - to tuple function arguments, just write your function curried.
2.94 -
2.95 - \item[telling names]
2.96 - Any name should tell its purpose as exactly as possible, while
2.97 - keeping its length to the absolutely necessary minimum. Always
2.98 - give the same name to function arguments which have the same
2.99 - meaning. Separate words by underscores (@{verbatim
2.100 - int_of_string}, not @{verbatim intOfString}).\footnote{Some
2.101 - recent tools for Emacs include special precautions to cope with
2.102 - bumpy names in @{text "camelCase"}, e.g.\ for improved on-screen
2.103 - readability. It is easier to abstain from using such names in the
2.104 - first place.}
2.105 -
2.106 - \end{description}
2.107 -*}
2.108 -
2.109 -
2.110 -chapter {* Basic library functions *}
2.111 -
2.112 -text {*
2.113 - Beyond the proposal of the SML/NJ basis library, Isabelle comes
2.114 - with its own library, from which selected parts are given here.
2.115 - These should encourage a study of the Isabelle sources,
2.116 - in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.
2.117 -*}
2.118 -
2.119 -section {* Linear transformations \label{sec:ML-linear-trans} *}
2.120 -
2.121 -text %mlref {*
2.122 - \begin{mldecls}
2.123 - @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
2.124 - \end{mldecls}
2.125 -*}
2.126 -
2.127 -(*<*)
2.128 -typedecl foo
2.129 -consts foo :: foo
2.130 -ML {*
2.131 -val thy = Theory.copy @{theory}
2.132 -*}
2.133 -(*>*)
2.134 -
2.135 -text {*
2.136 - \noindent Many problems in functional programming can be thought of
2.137 - as linear transformations, i.e.~a caluclation starts with a
2.138 - particular value @{ML_text "x : foo"} which is then transformed
2.139 - by application of a function @{ML_text "f : foo -> foo"},
2.140 - continued by an application of a function @{ML_text "g : foo -> bar"},
2.141 - and so on. As a canoncial example, take functions enriching
2.142 - a theory by constant declararion and primitive definitions:
2.143 -
2.144 - \smallskip\begin{mldecls}
2.145 - @{ML "Sign.declare_const: (binding * typ) * mixfix
2.146 - -> theory -> term * theory"} \\
2.147 - @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory"}
2.148 - \end{mldecls}
2.149 -
2.150 - \noindent Written with naive application, an addition of constant
2.151 - @{term bar} with type @{typ "foo \<Rightarrow> foo"} and
2.152 - a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
2.153 -
2.154 - \smallskip\begin{mldecls}
2.155 - @{ML "(fn (t, thy) => Thm.add_def false false
2.156 - (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
2.157 - (Sign.declare_const
2.158 - ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
2.159 - \end{mldecls}
2.160 -
2.161 - \noindent With increasing numbers of applications, this code gets quite
2.162 - unreadable. Further, it is unintuitive that things are
2.163 - written down in the opposite order as they actually ``happen''.
2.164 -*}
2.165 -
2.166 -text {*
2.167 - \noindent At this stage, Isabelle offers some combinators which allow
2.168 - for more convenient notation, most notably reverse application:
2.169 -
2.170 - \smallskip\begin{mldecls}
2.171 -@{ML "thy
2.172 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.173 -|> (fn (t, thy) => thy
2.174 -|> Thm.add_def false false
2.175 - (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
2.176 - \end{mldecls}
2.177 -*}
2.178 -
2.179 -text %mlref {*
2.180 - \begin{mldecls}
2.181 - @{index_ML "op |-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
2.182 - @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
2.183 - @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
2.184 - @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
2.185 - \end{mldecls}
2.186 -*}
2.187 -
2.188 -text {*
2.189 - \noindent Usually, functions involving theory updates also return
2.190 - side results; to use these conveniently, yet another
2.191 - set of combinators is at hand, most notably @{ML "op |->"}
2.192 - which allows curried access to side results:
2.193 -
2.194 - \smallskip\begin{mldecls}
2.195 -@{ML "thy
2.196 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.197 -|-> (fn t => Thm.add_def false false
2.198 - (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
2.199 -"}
2.200 - \end{mldecls}
2.201 -
2.202 - \noindent @{ML "op |>>"} allows for processing side results on their own:
2.203 -
2.204 - \smallskip\begin{mldecls}
2.205 -@{ML "thy
2.206 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.207 -|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
2.208 -|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
2.209 -"}
2.210 - \end{mldecls}
2.211 -
2.212 - \noindent Orthogonally, @{ML "op ||>"} applies a transformation
2.213 - in the presence of side results which are left unchanged:
2.214 -
2.215 - \smallskip\begin{mldecls}
2.216 -@{ML "thy
2.217 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.218 -||> Sign.add_path \"foobar\"
2.219 -|-> (fn t => Thm.add_def false false
2.220 - (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
2.221 -||> Sign.restore_naming thy
2.222 -"}
2.223 - \end{mldecls}
2.224 -
2.225 - \noindent @{ML "op ||>>"} accumulates side results:
2.226 -
2.227 - \smallskip\begin{mldecls}
2.228 -@{ML "thy
2.229 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.230 -||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
2.231 -|-> (fn (t1, t2) => Thm.add_def false false
2.232 - (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
2.233 -"}
2.234 - \end{mldecls}
2.235 -*}
2.236 -
2.237 -text %mlref {*
2.238 - \begin{mldecls}
2.239 - @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
2.240 - @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
2.241 - \end{mldecls}
2.242 -*}
2.243 -
2.244 -text {*
2.245 - \noindent This principles naturally lift to \emph{lists} using
2.246 - the @{ML fold} and @{ML fold_map} combinators.
2.247 - The first lifts a single function
2.248 - \begin{quote}\footnotesize
2.249 - @{ML_text "f : 'a -> 'b -> 'b"} to @{ML_text "'a list -> 'b -> 'b"}
2.250 - \end{quote}
2.251 - such that
2.252 - \begin{quote}\footnotesize
2.253 - @{ML_text "y |> fold f [x1, x2, ..., x_n]"} \\
2.254 - \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 |> f x2 |> ... |> f x_n"}
2.255 - \end{quote}
2.256 - \noindent The second accumulates side results in a list by lifting
2.257 - a single function
2.258 - \begin{quote}\footnotesize
2.259 - @{ML_text "f : 'a -> 'b -> 'c * 'b"} to @{ML_text "'a list -> 'b -> 'c list * 'b"}
2.260 - \end{quote}
2.261 - such that
2.262 - \begin{quote}\footnotesize
2.263 - @{ML_text "y |> fold_map f [x1, x2, ..., x_n]"} \\
2.264 - \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 ||>> f x2 ||>> ... ||>> f x_n"} \\
2.265 - \hspace*{6ex}@{ML_text "||> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])"}
2.266 - \end{quote}
2.267 -
2.268 - \noindent Example:
2.269 -
2.270 - \smallskip\begin{mldecls}
2.271 -@{ML "let
2.272 - val consts = [\"foo\", \"bar\"];
2.273 -in
2.274 - thy
2.275 - |> fold_map (fn const => Sign.declare_const
2.276 - ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
2.277 - |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
2.278 - |-> (fn defs => fold_map (fn def =>
2.279 - Thm.add_def false false (Binding.empty, def)) defs)
2.280 -end"}
2.281 - \end{mldecls}
2.282 -*}
2.283 -
2.284 -text %mlref {*
2.285 - \begin{mldecls}
2.286 - @{index_ML "op #> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
2.287 - @{index_ML "op #-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
2.288 - @{index_ML "op #>> ": "('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b"} \\
2.289 - @{index_ML "op ##> ": "('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd"} \\
2.290 - @{index_ML "op ##>> ": "('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd"} \\
2.291 - \end{mldecls}
2.292 -*}
2.293 -
2.294 -text {*
2.295 - \noindent All those linear combinators also exist in higher-order
2.296 - variants which do not expect a value on the left hand side
2.297 - but a function.
2.298 -*}
2.299 -
2.300 -text %mlref {*
2.301 - \begin{mldecls}
2.302 - @{index_ML "op ` ": "('b -> 'a) -> 'b -> 'a * 'b"} \\
2.303 - @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\
2.304 - \end{mldecls}
2.305 -*}
2.306 -
2.307 -text {*
2.308 - \noindent These operators allow to ``query'' a context
2.309 - in a series of context transformations:
2.310 -
2.311 - \smallskip\begin{mldecls}
2.312 -@{ML "thy
2.313 -|> tap (fn _ => writeln \"now adding constant\")
2.314 -|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
2.315 -||>> `(fn thy => Sign.declared_const thy
2.316 - (Sign.full_name thy (Binding.name \"foobar\")))
2.317 -|-> (fn (t, b) => if b then I
2.318 - else Sign.declare_const
2.319 - ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
2.320 -"}
2.321 - \end{mldecls}
2.322 -*}
2.323 -
2.324 -end
2.325 \ No newline at end of file
3.1 --- a/doc-src/IsarImplementation/Thy/ROOT.ML Fri Oct 22 20:43:48 2010 +0100
3.2 +++ b/doc-src/IsarImplementation/Thy/ROOT.ML Fri Oct 22 20:51:45 2010 +0100
3.3 @@ -4,7 +4,6 @@
3.4 "Local_Theory",
3.5 "Logic",
3.6 "ML",
3.7 - "ML_old",
3.8 "Prelim",
3.9 "Proof",
3.10 "Syntax",
4.1 --- a/doc-src/IsarImplementation/implementation.tex Fri Oct 22 20:43:48 2010 +0100
4.2 +++ b/doc-src/IsarImplementation/implementation.tex Fri Oct 22 20:51:45 2010 +0100
4.3 @@ -94,9 +94,6 @@
4.4 \input{Thy/document/Local_Theory.tex}
4.5 \input{Thy/document/Integration.tex}
4.6
4.7 -\appendix
4.8 -\input{Thy/document/ML_old.tex}
4.9 -
4.10 \begingroup
4.11 \tocentry{\bibname}
4.12 \bibliographystyle{abbrv} \small\raggedright\frenchspacing