Writing code in the intersection of F★, F# and OCaml

If you end up hacking on the F★ code base itself, then there are numerous restrictions that you should be aware of. These restrictions are due to the requirement that the source of F★ itself be readable as an F★ program and an F# program simultaneously.

Syntax

The following are forbidden: they will type-check when you run make (F★-as-F#) but your build will fail when you run make ocaml (F★-as-F★).

• No as-patterns (match ... with A ((B x) as y))
• No nested or-patterns (match ... with A (B | C))
• No OCaml-style type application (let f (x: int list)); use let f (x: list<int>) and let f (x: list<(int * int)>). Note the use of parentheses in the latter case: anything that's between brackets and is non-atomic requires parentheses, due to a terrible lexer hack that I won't mention here.

You often need to add extra parentheses in numerous places. If something compiles as F# but doesn't as F★, try sprinkling parentheses here and there.

There's an inconsistency that I (JP) haven't had the courage to investigate between F# and F★ regarding the treatment of namespaces... sometimes something will resolve fine as F★ but not as F#, or maybe the opposite. When in doubt, always use a fully qualified name (e.g. FStar.Util) rather than just Util (there's several of them).

Libraries

• No F# standard library (only basic/{util,list,string}.fsi are available within the source code of F★ itself).
• No printfn, or Printf.printf: use the "dumb" Util.print{1,...,6} and Util.format{1,...,6} that only take %s arguments and use string_of_{int,bool,float}.

See https://github.com/FStarLang/FStar/blob/master/src/README#L13 for instructions regarding the addition of new functions to the standard library.

The F★ parser and lexer

It's complicated. See https://github.com/FStarLang/FStar/blob/master/src/parser/README

Running F★

On Windows: fstar.exe can always be executed. Elsewhere: you must call fstar.exe when using the OCaml build (native binary) and mono fstar.exe otherwise. bin/fstar-any.sh takes care of those differences; you probably want to symlink fstar onto fstar-any.sh and call fstar when doing your own testing.