diff --git a/dev/doc/style.md b/dev/doc/style.md new file mode 100644 index 0000000000000..f22c8534a1f3e --- /dev/null +++ b/dev/doc/style.md @@ -0,0 +1,180 @@ +> 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: + ```ocaml + let x = ... in + ``` + ```ocaml + let x = + ... in + ``` + ```ocaml + 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 + ```ocaml + 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 + ```ocaml + 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 "breathe") + - 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: + ```ocaml + if condition then + first-case + else + second-case + ``` + - in case of effects in branches, use `begin ... end` rather than + parentheses + ```ocaml + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + ``` + - if the first branch raises an exception, avoid the `else`, i.e. + use + ```ocaml + if condition then error "foo"; + bar + ``` + instead of + ```ocaml + if condition then + error "foo" + 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) + ``` + - when a match fails to compile due to unbound constructors (eg + `match x with VarRef x -> bla | ConstRef x -> bli | _ -> blo` when + `GlobRef` is not open) it can be resolved in several ways: + + locally or globally open `GlobRef` + + type annotate `x : GlobRef.t` (where it is introduced, or in the `match` expression, whichever is nicer) + + annotate the first branch `GlobRef.VarRef x -> bla` + this last solution is not robust to branch reordering so should not be prefered + +- 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 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 for a good reason not to do so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breathe" (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 structure of the code are 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 + ```ocaml + match ... with Case1 -> try ... with ... -> ... | Case2 -> ... + ``` + or in + ```ocaml + match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ... + ``` + parentheses are needed around the `try` and the inner `match` + - even if streams 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 not + do side-effect; prefer otherwise + `let mygenericfun arg = mygenericfun args arg` + to ensure that the function is evaluated at + runtime diff --git a/dev/doc/style.txt b/dev/doc/style.txt deleted file mode 100644 index 699e0e1d76c66..0000000000000 --- a/dev/doc/style.txt +++ /dev/null @@ -1,149 +0,0 @@ -<< 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 "breathe") - - 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 - first-case - else - second-case - - 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) - - when a match fails to compile due to unbound constructors (eg - "match x with VarRef x -> bla | ConstRef x -> bli | _ -> blo" when - GlobRef is not open) it can be resolved in several ways: - + locally or globally open GlobRef - + type annotate "x : GlobRef.t" (where it is introduced, or in the match expression, whichever is nicer) - + annotate the first branch "GlobRef.VarRef x -> bla" - this last solution is not robust to branch reordering so should not be prefered - -- 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 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 for a good reason not to do so, follow the style of the - surrounding code in the same file as much as possible, - the general guidelines are otherwise "let spacing breathe" (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 structure of the code are 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