Parsing and operator precedence

Operators

Syntax

The syntax of F* pretty much follows the syntax of OCaml. In particular, the precedence and associativity of custom operators is determined by their first character. For a quick reference, this StackOverflow post is your best bet.

The snippet below defines the ++ operator to be the + operator... not very useful, but well.

let (++) = (+)

let main = List.fold_left (++) 0 [ 1; 2 ]

Alternative syntax

F* also supports the F# syntax, i.e.

let op_Plus_Plus = op_Addition

It's not very clear to me why the left-hand side uses Plus vs. Addition in the right-hand side, so... probably better off using the OCaml-style syntax.

Precedence

Since F* uses a unified syntax, where types and terms are on the same level, this means that arrows, conjunctions and disjunctions can now appear alongside regular terms. Here's an extended reference:

** ==> ** left ** -> ** left ** / ** left ** /\ ** left ** ! ~ ? ** prefix, left ** etc. ** (see rest of StackOverflow post).

The only exception is let x: t = e (and type t = e): to avoid shift/reduce conflicts, t may be an arrow, or anything that has the precedence of infix1 or above.

Overloading array access

The array, string assignment and dereference operators of OCaml are modeled as regular operators that can be overridden.

Any code that contains an expression of the form e1.[e2] <- e3 is desugared as a a call to the operator .[]<-. Please note that .( and .[ are one token (instead of two, say, in OCaml). This is due to obscure conflicts in the grammar... This means that forall (x: t).( ... ) no longer works! You need to insert a space between the . and the (.

e1.(e2) <- e3 is desugared as a reference to op_String_Assignment e1.[e2] <- e3 is desugared as a reference to op_Array_Assignment e1.(e2) is desugared as a reference to op_String_Access e1.[e2] is desugared as a reference to op_Array_Access

Example:

open FStar

let op_Array_Assignment = Buffer.upd
let op_Array_Access = Buffer.index

let test =
  let buf = Buffer.create false 16ul in
  buf.(0ul) <- not buf.(0ul);
  buf.(15ul) <- false

Note: you cannot do let (.()<-) because .()<- is not a valid sequence of operator characters. So, use the op_* form.