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
    • VD: this snippet captures most of the patterns around colon spacing, as currently implemented in the prettyprinter

let fun_set_equal_elim
  (#t: Type) (#t': Type) (#p: (t -> GSet.set t' -> Type))
  (f1: i_restricted_g_t t (fun x -> g: GSet.set t' {p x g}))
  (f2: i_restricted_g_t t (fun x -> g: GSet.set t' {p x g}))
  : Lemma (requires (fun_set_equal f1 f2)) (ensures (f1 == f2)) =
  assert (FunctionalExtensionality.feq_g f1 f2)

In most cases, the (x y: list t) style is used, except for computation types (e.g., let regions_of_loc (#al: aloc_t) (#c: cls al) (s: loc c) : GTot (Set.set HS.rid)).

Refinements are either separated by one space from the type, as shown above, if the type contains spaces, or is attached to the type if it doesn't (e.g., (r': HS.rid{Set.mem r' r})). (My motivation for this is that it seems to strike a good balance between making larger types more readable while not needlessly expanding smaller types.)

• double colon: x::nil or x :: nil

  • Proposal: Use x::nil whenever x and nil do not contain spaces. And use SomeConstructor x y :: z when one of the sides contains spaces.

• type declarations?

type foo =
| Foo

or

type foo =
  | Foo

VD: Inductives are currently formatted like this:

type pattern =
  | PAny : pattern
  | PVar : name: varname -> pattern
  | PQn : qn: qn -> pattern
  | PType : pattern
  | PApp : hd: pattern -> arg: pattern -> pattern

• records -- where do the curly braces go?

• pattern matching?

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

or

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

VD: where the pattern, arrow and branch don't all fit on one line, I'm currently using the first variant, which I think looks neater

• 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