Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Parsing and operator precedence
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 ]
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
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
e `f` e').
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.
! ~ ?prefix,
=, <, >infix, left
@, ^infix, right
+, -infix, left
*, /, %infix, left
`M.bar`infix, left ← syntax for infix application of functions
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
.[ 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) <- e3is desugared as a reference to
e1.[e2] <- e3is desugared as a reference to
e1.(e2)is desugared as a reference to
e1.[e2]is desugared as a reference to
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
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.
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.