-
Notifications
You must be signed in to change notification settings - Fork 632
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
A proposal for recommended uniformity of style in programming Coq.
Starting listing some recommendations in using the API.
- Loading branch information
Showing
2 changed files
with
151 additions
and
74 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| Recommendations in using the API: | ||
|
|
||
| The type of terms: constr (see kernel/constr.ml and kernel/term.ml) | ||
|
|
||
| - On type constr, the canonical equality on CIC (up to | ||
| alpha-conversion and cast removal) is Constr.equal | ||
| - The type constr is abstract, use mkRel, mkSort, etc. to build | ||
| elements in constr; use "kind_of_term" to analyze the head of a | ||
| constr; use destRel, destSort, etc. when the head constructor is | ||
| known |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |