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