Style guide

---

WORK IN PROGRESS! This is just a draft; anything and everything is subject to change!

---

Basic syntactic structure

• Files should begin with copyright notice
• Source files should not contain tabs
• The unit of indentation is 2 spaces
• Lines should not exceed 100 characters

Modular structure

• Module names should use CamelCase
• Module filenames should follow the same case convention as the module names themselves, i.e., CamelCase.fst
• Modules should have separate interface files, i.e., CamelCase.fsti
• Module abbreviations are preferred over opened modules and namespaces, with well-chosen exceptions
• Groups of related modules should be composed into a single module using include for easier use by clients

Naming conventions within a module

• Data constructors must begin with an uppercase letter and, like module names, use upper CamelCase.

• Identifiers are required by F* to begin with a lowercase character. All lowercase identifiers should delimit words in the identifier with underscores. i.e., partial_map rather than partialMap or partialmap.

  • This is more compatible with our existing conventions
  • It works better with abbreviations in identifiers: e.g., use_SMT_pat rather than the camelCase useSMTPat.

• Use descriptive, multi-character names for top-level names, especially those exported by a module. (i.e., contrary to OCaml style, prefer giving names like PartialMap.partial_map rather than PartialMap.t, particularly as the module name may often be abbreviated or opened)

Formatting type annotations

• Annotate all top-level terms with their full types. This may take one of the following forms:

  let f (x1:t1) ... (xn:tn) : C = e
  

  Or

  val f (x1:t1) ... (xn:tn) : C
  let f x1 ... xn = e
  

  Unless required by needs of an interface, prefer the first style (i.e, use only an annotated let rather than let + val).

  If using the val form, do not repeat the types provided in the val in the let also.

• Format of a val

  F* accepts both of the following notations for val

  val f (x1:t1) ... (xn:tn) : C
  

  or

  val f : x1:t1 -> ... -> xn:tn -> C
  

  Prefer the first, as it is more compatible with the syntax of let.

• Prefer writing x:t -> t' rather than (x:t) -> t'. This is particularly useful in conjunction with refinement types, e.g., x:int{x > 0} -> y:int{y > x} -> t, rather than (x:int{x > 0}) -> (y:int{y > x}) -> t, or x:(x:int{x > 0}) -> y:(y:int{y > x}) -> ...

• Repeated arguments with the same type: Prefer writing (x y :int) -> t rather than x:int -> y:int -> t

• Linebreaks in type annotations:

  • A type annotation should be on a single line, except if it would exceed 100 characters.
  • Otherwise, if all the arguments fit within 100 characters, annotate the result computation type on a separate line
  • Otherwise, every argument goes and the result type goes on a separate line.

  Here are some examples:

  Fits on a single line:

  val on_domain (a:Type) (#b:a -> Type) (f:arrow a b) : Tot (arrow a b)
  

  Arguments fit on a single line:

  val idempotence_on_domain (#a:Type) (#b:a -> Type) (f:arrow a b)
      : Lemma (on_domain a (on_domain a f) == on_domain a f)
  

  Too many arguments, layout on multiple lines, one type per line. The arguments are triple indented (6 chars in) The colon is double indented (i.e., 4 chars in).

val modifies_preserves_liveness
      (#aloc: aloc_t)
      (#c: cls aloc)
      (s1 s2: loc c)
      (h h' : HS.mem)
      (#t: Type)
      (#pre: Preorder.preorder t)
      (r: HS.mreference t pre)
    : Lemma
      (requires (modifies (loc_union s1 s2) h h' /\
                 loc_disjoint s1 (loc_mreference r) /\
                 loc_includes (address_liveness_insensitive_locs c) s2 /\
                 h `HS.contains` r))
      (ensures (h' `HS.contains` r))

• Computation types:
  • Fit it on a single line
  • Otherwise effect label and result type (if any) on a single line and other arguments on one line each
  • In pre- and post-conditions, formulae have one conjunct per line (think of /\ as a line delimiter)
  • Alignment is to the start column of the effect label
  • See above for an example

---

Other things:

• recommended style for if-then-else:

if e1 then
  ...
else
  ...

• how to indent List.map

• use (abuse?) of <| and |>

• spaces around operators?

  • colon:
    • in parameters: (x y:list t) or (x y: list t) or (x y :list t) or (x y : list t)
    • in return types: let f (x:int):int or let f (x:int) : int or …
    • in variable types: let x:int = … or let x : int = … or …
    • in record types and datatype declarations
  • double colon: x::nil or x :: nil

• type declarations?

type foo =
| Foo

or

type foo =
  | Foo

• records -- where do the curly braces go?

• pattern matching?

match x with
| Foo ->
  foo
| Bar ->
  bar

or

match x with
| Foo ->
    foo
| Bar ->
    bar

• long let definitions -- where does the = go?

let f (x:int)
    : Lemma
      (requires …)
      (ensures …) // does = go here?
  = // or here? with what indentation?
  5 // same line as =, or different line?

• single-line comments

// Like this?
let x = 5 // like this?
let x = 5  // like this?

or

(* Like this? *)
let x = 5 (* like this? *)
let x = 5  (* like this? *)

• multi-line comments