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.

Infix function application

We support syntax à la Haskell where `f` is an infix application of function f (e.g. e `f` e').

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 the precedence, arity and associativity of various operators. ==> binds looser, ** binds tighter.

• ==> infix, left
• -> infix, left
• \/ infix, left
• /\ infix, left
• ! ~ ? prefix,
• | infix, left
• & infix, left
• =, <, > infix, left
• $ infix, left
• |> infix, left
• @, ^ infix, right
• +, - infix, left
• *, /, % infix, left
• `foo`, `M.bar` infix, left ← syntax for infix application of functions
• ** infix, left

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.

Note: I didn't write down any special behavior for <|... not sure where it should stand. Shout out if it's wrong.

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_Array_Assignment
• e1.[e2] <- e3 is desugared as a reference to op_String_Assignment
• e1.(e2) is desugared as a reference to op_Array_Access
• e1.[e2] is desugared as a reference to op_String_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.

Precedence of array assignment operators

Assignment operators sit at the precedence level of statements, which bind looser than expressions. This means that you cannot use h.[x] <- e in an expression, for instance, if you overload op_String_Assignment to represent functional updates of the heap in a specification. In practice, you'll have to write (ensures (h' == (h.[x] <- e))). This is unlike OCaml, where you can write the (not very useful) () = e1.[e2] <- e3.

Usage conventions

(tentative)

• op_String_ variants (with square brackets) are used for HyperHeap (and possibly other heap models) -- this are functional updates
• op_Array_ variants (with parentheses) are used for Buffers (and possibly other Array variants) -- these are stateful updates
• op_Curly_ variants (to be added) are used for Sequences -- these are functional updates
• op_Angle_ variants (to be added)

Commonly used operators/symbols

Some "standard" operators, and other commonly useful F* symbols can be found in the F* symbols reference page of the wiki.

Multiplication and tuples

By default, the * operator is used for tuple types, e.g., int * bool. However, one often wants to use * for integer multiplication.

To do this, open FStar.Mul which rebinds * for integer multiplication and use & for tuple types.

For example, this works:

open FStar.Mul
let test (x y:int) : int & int = x * y, x + y

Record literals

Record literals passed as arguments to functions almost always need to be enclosed in parentheses. The following code illustrates the parsing conflict:

module V
type u = {x : unit}
let ffalse (_: u) = nat
let f (b: bool) : (if b then Type0 else (u → Type0)) = if b then unit else ffalse
type dummy =
  | Dummy1 : x: f true { x = () } → dummy
  | Dummy2 : x: f false ({ x = () }) → dummy

See also #2417 : should this restriction also apply to with record literals?