doc-src/IsarImplementation/Thy/ML.thy
author haftmann
Fri, 03 Nov 2006 14:22:34 +0100
changeset 21148 3a64d58a9f49
parent 20520 05fd007bdeb9
child 21502 7f3ea2b3bab6
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
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     2
(* $Id$ *)
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     3
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     4
theory "ML" imports base begin
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     5
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     6
chapter {* Aesthetics of ML programming *}
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     7
21148
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
     8
text {* This style guide is loosely based on
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
     9
  \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    10
%  FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    11
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    12
  Like any style guide, it should not be interpreted dogmatically.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    13
  Instead, it forms a collection of recommendations which,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    14
  if obeyed, result in code that is not considered to be
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    15
  obfuscated.  In certain cases, derivations are encouraged,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    16
  as far as you know what you are doing.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    17
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    18
  \begin{description}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    19
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    20
    \item[fundamental law of programming]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    21
      Whenever writing code, keep in mind: A program is
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    22
      written once, modified ten times, and read
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    23
      100 times.  So simplify its writing,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    24
      always keep future modifications in mind,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    25
      and never jeopardize readability.  Every second you hesitate
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    26
      to spend on making your code more clear you will
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    27
      have to spend ten times understanding what you have
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    28
      written later on.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    29
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    30
    \item[white space matters]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    31
      Treat white space in your code as if it determines
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    32
      the meaning of code.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    33
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    34
      \begin{itemize}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    35
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    36
        \item The space bar is the easiest key to find on the keyboard,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    37
          press it as often as necessary. {\ttfamily 2 + 2} is better
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    38
          than {\ttfamily 2+2}, likewise {\ttfamily f (x, y)}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    39
          better than {\ttfamily f(x,y)}.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    40
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    41
        \item Restrict your lines to \emph{at most} 80 characters.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    42
          This will allow you to keep the beginning of a line
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    43
          in view while watching its end.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    44
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    45
        \item Ban tabs; they are a context-sensitive formatting
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    46
          feature and likely to confuse anyone not using your
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    47
          favourite editor.
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 Get rid of trailing whitespace.  Instead, do not
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    50
          surpess a trailing newline at the end of your files.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    51
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    52
        \item Choose a generally accepted style of indentation,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    53
          then use it systematically throughout the whole
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    54
          application.  An indentation of two spaces is appropriate.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    55
          Avoid dangling indentation.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    56
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    57
      \end{itemize}
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    58
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    59
    \item[cut-and-paste succeeds over copy-and-paste]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    60
      \emph{Never} copy-and-paste code when programming.  If you
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    61
        need the same piece of code twice, introduce a
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    62
        reasonable auxiliary function (if there is no
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    63
        such function, very likely you got something wrong).
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    64
        Any copy-and-paste will turn out to be painful 
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    65
        when something has to be changed or fixed later on.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    66
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    67
    \item[comments]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    68
      are a device which requires careful thinking before using
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    69
      it.  The best comment for your code should be the code itself.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    70
      Prefer efforts to write clear, understandable code
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    71
      over efforts to explain nasty code.
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[functional programming is based on functions]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    74
      Avoid ``constructivisms'', e.g. pass a table lookup function,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    75
      rather than an actual table with lookup in body.  Accustom
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    76
      your way of codeing to the level of expressiveness
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    77
      a functional programming language is giving onto you.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    78
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    79
    \item[tuples]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    80
      are often in the way.  When there is no striking argument
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    81
      to tuple function arguments, just write your function curried.
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[telling names]
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    84
      Any name should tell its purpose as exactly as possible,
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    85
      while keeping its length to the absolutely neccessary minimum.
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    86
      Always give the same name to function arguments which
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    87
      have the same meaning. Separate words by underscores
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    88
      (``{\ttfamily int\_of\_string}'', not ``{\ttfamily intOfString}'')
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    89
3a64d58a9f49 first version of style guide
haftmann
parents: 20520
diff changeset
    90
  \end{description}
18554
bff7a1466fe4 more stuff;
wenzelm
parents: 18538
diff changeset
    91
*}
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    92
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    93
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    94
chapter {* Basic library functions *}
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    95
20520
wenzelm
parents: 20491
diff changeset
    96
text {* FIXME beyond the NJ basis library proposal *}
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    97
20489
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    98
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    99
chapter {* Cookbook *}
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
   100
20491
wenzelm
parents: 20489
diff changeset
   101
section {* A method that depends on declarations in the context *}
20489
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
   102
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
   103
text FIXME
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
   104
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
   105
end