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