summaryrefslogtreecommitdiff
path: root/dev/doc/style.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/style.txt')
-rw-r--r--dev/doc/style.txt215
1 files changed, 141 insertions, 74 deletions
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09..2ee3dadd 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,75 +1,142 @@
-
-<< L'uniformité du style est plus importante que le style lui-même. >>
-(Kernigan & Pike, The Practice of Programming)
-
-Mode Emacs
-==========
- Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/
-
- avec le réglage suivant : (setq tuareg-in-indent 2)
-
-Types récursifs et filtrages
-============================
- Une barre de séparation y compris sur le premier constructeur
-
-type t =
- | A
- | B of machin
-
-match expr with
- | A -> ...
- | B x -> ...
-
-Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
-format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel intéressant de bloc :
-
-type t =
-| A
-| B of machin
-
-match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = function
-| A -> ...
-| B x -> ...
-
-Le deuxième cas est obtenu sous tuareg avec les réglages
-
- (setq tuareg-with-indent 0)
- (setq tuareg-function-indent 0)
- (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien
- /// pour les let mais pas pour les let-in
-
-Conditionnelles
-===============
- if condition then
- premier-cas
- else
- deuxieme-cas
-
- Si effets de bord dans les branches, utilisez begin ... end et non des
- parenthèses i.e.
-
- if condition then begin
- instr1;
- instr2
- end else begin
- instr3;
- instr4
- end
-
- Si la première branche lève une exception, évitez le else i.e.
-
- if condition then if condition then error "machin";
- error "machin" -----> suite
+<< Style uniformity is more important than style itself >>
+ (Kernigan & Pike, The Practice of Programming)
+
+OCaml Style:
+- Spacing and indentation
+ - indent your code (using tuareg default)
+ - no strong constraints in formatting "let in"; possible styles are:
+ "let x = ... in"
+ "let x =
+ ... in"
+ "let
+ x = ...
+ in"
+ - but: no extra indentation before a "in" coming on next line,
+ otherwise, it first shifts further and further on the right,
+ reducing the amount of space available; second, it is not robust to
+ insertion of a new "let"
+ - it is established usage to have space around "|" as in
+ "match c with
+ | [] | [a] -> ...
+ | a::b::l -> ..."
+ - in a one-line "match", it is preferred to have no "|" in front of
+ the first case (this saves spaces for the match to hold in the line)
+ - from about 8.2, the tendency is to use the following format which
+ limit excessive indentation while providing an interesting "block" aspect
+ type t =
+ | A
+ | B of machin
+
+ let f expr = match expr with
+ | A -> ...
+ | B x -> ...
+
+ let f expr = function
+ | A -> ...
+ | B x -> ...
+ - add spaces around = and == (make the code "breaths")
+ - the common usage is to write "let x,y = ... in ..." rather than
+ "let (x,y) = ... in ..."
+ - parenthesizing with either "(" and ")" or with "begin" and "end" is
+ common practice
+ - preferred layout for conditionals:
+ if condition then
+ premier-cas
else
- suite
-
-
+ deuxieme-cas
+ - in case of effects in branches, use "begin ... end" rather than
+ parentheses
+ if condition then begin
+ instr1;
+ instr2
+ end else begin
+ instr3;
+ instr4
+ end
+ - if the first branch raises an exception, avoid the "else", i.e.:
+ if condition then if condition then error "foo";
+ error "foo" -----> bar
+ else
+ bar
+ - it is the usage not to use ;; to end OCaml sentences (however,
+ inserting ";;" can be useful for debugging syntax errors crossing
+ the boundary of functions)
+ - relevant options in tuareg:
+ (setq tuareg-in-indent 2)
+ (setq tuareg-with-indent 0)
+ (setq tuareg-function-indent 0)
+ (setq tuareg-let-always-indent nil)
+
+- Coding methodology
+ - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C),
+ Out_of_memory, Stack_overflow, etc.
+ at least, use "try with e when Errors.noncritical e -> ..."
+ (to be detailed, Pierre L. ?)
+ - do not abuse of fancy combinators: sometimes what a "let rec" loop
+ does is more readable and simpler to grasp than what a "fold" does
+ - do not break abstractions: if an internal property is hidden
+ behind an interface, do no rely on it in code which uses this
+ interface (e.g. do not use List.map thinking it is left-to-right,
+ use map_left)
+ - in particular, do not use "=" on abstract types: there is no
+ reason a priori that it is the intended equality on this type; use the
+ "equal" function normally provided with the abstract type
+ - avoid polymorphically typed "=" whose implementation is not
+ optimized in OCaml and which has moreover no reason to be the
+ intended implementation of the equality when it comes to be
+ instantiated on a particular type (e.g. use List.mem_f,
+ List.assoc_f, rather than List.mem, List.assoc, etc, unless it is
+ absolutely clear that "=" will implement the intended equality, and
+ with the right complexity)
+ - any new general-purpose enough combinator on list should be put in
+ cList.ml, on type option in cOpt.ml, etc.
+ - unless of a good reason not to so, follow the style of the
+ surrounding code in the same file as much as possible,
+ the general guidelines are otherwise "let spacing breaths" (we
+ have large screen nowadays), "make your code easy to read and
+ to understand"
+ - document what is tricky, but do not overdocument, sometimes the
+ choice of names and the structuration of the code is a better
+ documentation than a long discourse; use of unicode in comments is
+ welcome if it can make comments more readable (then
+ "toggle-enable-multibyte-characters" can help when using the
+ debugger in emacs)
+ - all of initial "open File", or of small-scope File.(...), or
+ per-ident File.foo are common practices
+
+- Choice of variable names
+ - be consistent when naming from one function to another
+ - be consistent with the naming adopted in the functions from the
+ same file, or with the naming used elsewhere by similar functions
+ - use variable names which express meaning
+ - keep "cst" for constants and avoid it for constructors which is
+ otherwise a source of confusion
+ - for constructors, use "cstr" in type constructor (resp. "cstru" in
+ constructor puniverse); avoid "constr" for "constructor" which
+ could be think as the name of an arbitrary Constr.t
+ - for inductive types, use "ind" in the type inductive (resp "indu"
+ in inductive puniverse)
+ - for env, use "env"
+ - for evar_map, use "sigma", with tolerance into "evm" and "evd"
+ - for named_context or rel_context, use "ctxt" or "ctx" (or "sign")
+ - for formal/actual indices of inductive types: "realdecls", "realargs"
+ - for formal/actual parameters of inductive types: "paramdecls", "paramargs"
+ - for terms, use e.g. c, b, a, ...
+ - if a term is known to be a function: f, ...
+ - if a term is known to be a type: t, u, typ, ...
+ - for a declaration, use d or "decl"
+ - for errors, exceptions, use e
+
+- Common OCaml pitfalls
+ - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in
+ "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in
+ parentheses are needed around the "try" and the inner "match"
+ - even if stream are lazy, the Pp.(++) combinator is strict and
+ forces the evaluation of its arguments (use a "lazy" or a "fun () ->")
+ to make it lazy explicitly
+ - in "if ... then ... else ... ++ ...", the default parenthesizing
+ is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..."
+ - in "let myspecialfun = mygenericfun args", be sure that it does no
+ do side-effect; prefer otherwise "let mygenericfun arg =
+ mygenericfun args arg" to ensure that the function is evaluated at
+ runtime