-
Notifications
You must be signed in to change notification settings - Fork 234
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.
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)
); uselet f (x: list<int>)
andlet 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. - No trailing semicolon in: sequences, records, lists (e.g.
begin e; e; end
is not ok butbegin e; e end
is, etc). - No
List.exists
andList.forall
, as these are keywords in F★. Useexistsb
andforallb
.
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).
- No F# standard library (only
basic/{util,list,string}.fsi
are available within the source code of F★ itself). - No
printfn
, orPrintf.printf
: use the "dumb"Util.print{1,...,6}
andUtil.format{1,...,6}
that only take%s
arguments and usestring_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.
It's complicated. See https://github.com/FStarLang/FStar/blob/master/src/parser/README
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.