Partial evaluation before extraction

F* supports normalization, or partial evaluation. At selected points in the codebase, F* terms are normalized, using a symbolic evaluator, or normalizer, based on the Krivine Abstract Machine. For instance, before extracting a term, we normalize it.

The normalization depends on a selected set of steps; these are listed at https://github.com/FStarLang/FStar/blob/master/src/typechecker/normalize.fs#L44 -- for instance, extraction normalizes the body of let-bindings as follows:

                    let lbdef = N.normalize [N.AllowUnboundUniverses; N.EraseUniverses;
                                             N.Inlining; N.Eager_unfolding;
                                             N.Exclude N.Zeta; N.PureSubtermsWithinComputations; N.Primops]
                                tcenv lb.lbdef in

This is not configurable by the user.

Of particular relevance are the Primops and PureSubtermsWithinComputations normalization steps.

Primops

Primsops means that the F* normalizer reduces some primitive operations (see https://github.com/FStarLang/FStar/blob/master/src/typechecker/normalize.fs#L441). Currently, these are:

• Const.op_Addition, Const.op_Subtraction, Const.op_Multiply, Const.op_Division, Const.op_LT, Const.op_LTE, Const.op_GT, Const.op_GTE, Const.op_Modulus -- these are the primitive operations that operate on the int type defined in Prims
• for the following classes of machine integers: Int8, UInt8, Int16, UInt16, Int32, UInt32, Int64, UInt64, UInt128, we normalize three operations: add, sub and mul -- this is insufficient and we should normalize more operations

In particular, we fail to normalize boolean operations (boo!), modulo operations for machine integers, divisions, underspecified additions, shifts, etc. etc. We don't even have boolean negation.

Pure subterms within computations

Recursively descend under effectful abstractions to find pure subterms that can be normalized according to the current normalization steps.

Inline for extraction

References to top-level definitions, such generic below, may reduce into their definition, if marked as inline_for_extraction, or unfold.

Misc.

list_of_string is properly reduced by the normalizer -- I suspect this is for the evaluation of Printf.

Decidable equalities are also reduced by the normalizer, using a comparison routine (see eq_tm in syntax/util.fs) that hopefully corresponds to the same thing as the run-time OCaml polymorphic comparison (which is what we use for extracted code).

Example

Pure applications are normalized, of course. This allows you to leverage partial evaluation to do code specialization as follows:

jonathan@chartreuse:/tmp $ cat Test.fst
module Test

type alg = | Alg1 | Alg2

inline_for_extraction
let generic (a: alg): Tot (unit -> ML unit) =
  fun () ->
    match a with
    | Alg1 ->
        FStar.IO.print_string "special case 1"
    | Alg2 ->
        FStar.IO.print_string "special case 2"

let specialized1 = generic Alg1
let specialized2 = generic Alg2

the final two lines are extracted as:

# 14 "Test.fst"
let specialized1 : Prims.unit  ->  Prims.unit = (fun uu____31 -> (FStar_IO.print_string "special case 1"))

# 15 "Test.fst"
let specialized2 : Prims.unit  ->  Prims.unit = (fun uu____38 -> (FStar_IO.print_string "special case 2"))

JP: actually turns out you don't even need to do the explicit currification