doc-src/IsarImplementation/Thy/document/ML.tex
author wenzelm
Thu, 23 Nov 2006 20:33:42 +0100
changeset 21501 8dab1e45c11f
parent 21172 eea3c9048c7a
child 22293 3593a76c9ed3
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{ML}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\isanewline
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
     7
\isanewline
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
     8
\isanewline
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\isacommand{theory}\isamarkupfalse%
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    14
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    15
\endisatagtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    16
{\isafoldtheory}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    17
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    18
\isadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    19
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    20
\endisadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    21
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    22
\isamarkupchapter{Aesthetics of ML programming%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    23
}
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    24
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    25
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    26
\begin{isamarkuptext}%
21501
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
    27
FIXME%
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
    28
\end{isamarkuptext}%
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
    29
\isamarkuptrue%
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
    30
%
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
    31
\begin{isamarkuptext}%
21148
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    32
This style guide is loosely based on
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    33
  \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    34
%  FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    35
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    36
  Like any style guide, it should not be interpreted dogmatically.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    37
  Instead, it forms a collection of recommendations which,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    38
  if obeyed, result in code that is not considered to be
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    39
  obfuscated.  In certain cases, derivations are encouraged,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    40
  as far as you know what you are doing.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    41
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    42
  \begin{description}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    43
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    44
    \item[fundamental law of programming]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    45
      Whenever writing code, keep in mind: A program is
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    46
      written once, modified ten times, and read
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    47
      100 times.  So simplify its writing,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    48
      always keep future modifications in mind,
21172
eea3c9048c7a updated;
wenzelm
parents: 21148
diff changeset
    49
      and never jeopardize readability.  Every second you hesitate
21148
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    50
      to spend on making your code more clear you will
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    51
      have to spend ten times understanding what you have
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    52
      written later on.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    53
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    54
    \item[white space matters]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    55
      Treat white space in your code as if it determines
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    56
      the meaning of code.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    57
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    58
      \begin{itemize}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    59
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    60
        \item The space bar is the easiest key to find on the keyboard,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    61
          press it as often as necessary. {\ttfamily 2 + 2} is better
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    62
          than {\ttfamily 2+2}, likewise {\ttfamily f (x, y)}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    63
          better than {\ttfamily f(x,y)}.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    64
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    65
        \item Restrict your lines to \emph{at most} 80 characters.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    66
          This will allow you to keep the beginning of a line
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    67
          in view while watching its end.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    68
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    69
        \item Ban tabs; they are a context-sensitive formatting
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    70
          feature and likely to confuse anyone not using your
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    71
          favourite editor.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    72
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    73
        \item Get rid of trailing whitespace.  Instead, do not
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    74
          surpess a trailing newline at the end of your files.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    75
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    76
        \item Choose a generally accepted style of indentation,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    77
          then use it systematically throughout the whole
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    78
          application.  An indentation of two spaces is appropriate.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    79
          Avoid dangling indentation.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    80
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    81
      \end{itemize}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    82
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    83
    \item[cut-and-paste succeeds over copy-and-paste]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    84
      \emph{Never} copy-and-paste code when programming.  If you
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    85
        need the same piece of code twice, introduce a
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    86
        reasonable auxiliary function (if there is no
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    87
        such function, very likely you got something wrong).
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    88
        Any copy-and-paste will turn out to be painful 
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    89
        when something has to be changed or fixed later on.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    90
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    91
    \item[comments]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    92
      are a device which requires careful thinking before using
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    93
      it.  The best comment for your code should be the code itself.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    94
      Prefer efforts to write clear, understandable code
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    95
      over efforts to explain nasty code.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    96
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    97
    \item[functional programming is based on functions]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    98
      Avoid ``constructivisms'', e.g. pass a table lookup function,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    99
      rather than an actual table with lookup in body.  Accustom
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   100
      your way of codeing to the level of expressiveness
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   101
      a functional programming language is giving onto you.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   102
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   103
    \item[tuples]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   104
      are often in the way.  When there is no striking argument
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   105
      to tuple function arguments, just write your function curried.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   106
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   107
    \item[telling names]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   108
      Any name should tell its purpose as exactly as possible,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   109
      while keeping its length to the absolutely neccessary minimum.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   110
      Always give the same name to function arguments which
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   111
      have the same meaning. Separate words by underscores
21501
8dab1e45c11f updated;
wenzelm
parents: 21172
diff changeset
   112
      (``\verb|int_of_string|'', not ``\verb|intOfString|'')
21148
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   113
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
   114
  \end{description}%
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   115
\end{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   116
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   117
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   118
\isamarkupchapter{Basic library functions%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   119
}
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   120
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   121
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   122
\begin{isamarkuptext}%
20520
wenzelm
parents: 20491
diff changeset
   123
FIXME beyond the NJ basis library proposal%
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   124
\end{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   125
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   126
%
20490
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   127
\isamarkupchapter{Cookbook%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   128
}
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   129
\isamarkuptrue%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   130
%
20491
wenzelm
parents: 20490
diff changeset
   131
\isamarkupsection{A method that depends on declarations in the context%
20490
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   132
}
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   133
\isamarkuptrue%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   134
%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   135
\begin{isamarkuptext}%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   136
FIXME%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   137
\end{isamarkuptext}%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   138
\isamarkuptrue%
e502690952be updated;
wenzelm
parents: 18554
diff changeset
   139
%
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   140
\isadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   141
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   142
\endisadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   143
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   144
\isatagtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   145
\isacommand{end}\isamarkupfalse%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   146
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   147
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   149
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   150
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   151
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   152
\endisadelimtheory
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
   153
\isanewline
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   154
\end{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   155
%%% Local Variables:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   156
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   157
%%% TeX-master: "root"
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   158
%%% End: