Coding style for Beluga
=======================

Naming conventions
------------------
- objects are prefixed with a t: tA, tK, tM, ...

- objects under a substitution are prefixed with a s: sA, sK, sM, ...

- contexts are prefixed with a c: cPsi, cPhi, ...

- function names follow the CamelCase convention

Lexical conventions
-------------------
- files end with a new line (Emacs: require-final-newline)

- tabulations are not used (Emacs: indent-tabs-mode)

- the code is written in ascii

- indentation follows Emacs's tuareg mode

- lines length should be limited to 80 characters

Syntactic conventions
---------------------
- "if" constructs are written with the "then" ending the test line

- code is written in a currified style, a space separating the function from
  its arguments

- tuples are parenthesized even when not ambiguous

- sequential code is written in the OTBS (One True Brace Style), preferred to
  using "let _"

- function declarations list all arguments and match on them explicitly

- function cases are separated by a blank line

- '->' are written at the end of lines

- spaces are inserted after commas and around arithmetic operators

Comments
--------
- each function must list its invariants

- catching of Ocaml errors must be explained by a comment

- leave revision comments to the revision control system

- whenever comment indentation is needed in multiline comment, prefix each line
  with *

- for ease of navigation, comments denoting things that are to be done and
  identifying problematic code use TODO and FIXME tags respectively
