STYLE

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

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

  LF Terms        tM, tN
  LF Types        tA, tB
  LF Spines           tS
  LF Heads        tH

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

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

- Contextual objects are prefixed with a c: cM, cT, cD
  Contextual Object  cM
  Contextual Type    cT
  Meta-Context       cD
  Meta-subst.        theta or t

- Beluga expressions and types
  Beluga expressions e,i
  Beluga types       tau
  Beluga context     cD

- Beluga types under a meta-substitution are prefixed with a t: ttau

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

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