Meta F*, (anti) quotations, term views and `inspect` versus `inspect_ln`

The types term and term_view

In F*, one can quote a term, transforming an expression into its representation. The infix operator ` takes an expression of arbitrary type and produces a term. For instance, the expression `(20 + 22) is of type term and correspond to F*'s internal representation of this addition.

Of course, one cannot manipulate directly F*'s internal representation of terms directly within F*. Instead, one should inspect a term to get a view of it, of type term_view.

The different way of quoting a term

The backtick operator is total, i.e. one can write the top-level t1 below.

let t1: term = `(30 + 12)

Such a backtick quotation is purely syntactic: for instance, the top-level t2 below will not capture the value of the local binding x. t2 is a representation of an addition between the literal 40 and some free variable x. Of course one can write t3 as below to fix the problem.

let t2: term =
  let x = 2 in
  `(40 + x)
let t3: term = `(let x = 2 in 40 + x)

However, while meta-programming, it is very useful to capture values from the current scope while quoting an expression. The quote operator is effectful but allows for such a behavior, i.e.:

let t4 (x: int): Tac term =
  let y = x + 1 in
  quote (y + 2)

The backtick quotation operator ` can also be used in conjunction with (effectful) antiquotation operators `@ and `#. The former inserts an expression of arbitrary type in a quotation, while the latter inserts a term in a quotation. Example:

let t4 (x: int) (y: term): Tac term =
  `(`@x + `#y)

Unquoting a term

The reverse operation, unquoting, is the effectful operation unquote. For example, below unquoting t4 12 (`30) results in the integer 42 as expected. Note the syntax assert goal by tac invokes the tactic tac against the goal goal; here the goal is trivial, we just use this construction to print a result.

let _ = assert True by (
  print (string_of_int (unquote (t4 12 (`30))))
)

Others ways for invoking Meta F* programs are documented here.

De Bruijn indexes: inspect vs inspect_ln

The module FStar.Reflection.Builtins exposes the total funtion inspect_ln of type term -> term_view, while FStar.Tactics.Builtins exposes the effectful inspect of type term -> Tac term_view. inspect is almost always preferable to inspect_ln.

In F*, there is two kinds of bounded variables:

• named bounded variables (Tv_Var), and
• De Bruijn bounded variables (Tv_BVar).

inspect produces term_views with only named variables, while inspect_tv produces term_views with only De Bruijn variables.

Observing inspect effectfulness

To disambiguate potential shadowing and for efficiency, F* gives each named variable an index that uniquely refers to it. A named variable is represented by the term_view constructor Tv_Var, of type bv -> term_view: it takes a bv (bounded variable). A bv can be inspected (with inspect_bv) as a record which has the attribute bv_index.

In the following module, we let the top-level example be a term. Inspecting (with inspect) and then observing the index of the variable x (with get_let_bv_index) multiple times yields different result.

module InspectEffectful

open FStar.Tactics

let example = (`(let x = 1 in x))

let get_let_bv_index (tv: term_view): string
  = match tv with
  | Tv_Let _ _ bv _ _ -> string_of_int (inspect_bv bv).bv_index
  | _                 -> "Not a Tv_Let!"

let _ = run_tactic (fun _ -> 
  let with_inspect () = get_let_bv_index (inspect example) in
  let with_inspect_ln () = get_let_bv_index (inspect_ln example) in
  print ( "Inspecting indexes with [inspect] is not pure : 1st run gives "
        ^ with_inspect () ^ ", while 2nd run gives " ^ with_inspect () ^ ". "
        ^ "In opposition, with [inspect_ln], the results are constants: " 
        ^ with_inspect_ln () ^ " is equal to " ^ with_inspect_ln ())
)

This prints (in my F* session, you will get different numbers running this code):

Inspecting indexes with [inspect] is not pure: 1st run gives 205589, while 2nd run gives 205603. In opposition, with [inspect_ln], the results are consistent: 180975 is equal to 180975.

What are De Bruijn indexes and why you should not meta-program with them

De Bruijn indexes are not practical to use by hand: instead of referring to a variable by its name, De Bruijn indexes consist in counting the number of abstractions (lambdas) you need to traverse to reach the binder you want to target.

The following module demonstrates this:

module DeBruijn

open FStar.Tactics

// Let [abs] a term that consists in nested abstractions. Note [fun x y z -> ...] is syntactic sugar for [fun x -> fun y -> fun z -> ...]
let abs = (`(fun x -> fun y -> fun z -> (x, y, z)))

let get_let_bv_index (tv: term_view): string
  = match tv with
  | Tv_Let _ _ bv _ _ -> string_of_int (inspect_bv bv).bv_index
  | _                 -> "Not a Tv_Let!"

// [string_of_bv] prints a [bv] with its index
let string_of_bv (bv: bv): string = 
  let bvv = inspect_bv bv in
  "name="^bvv.bv_ppname ^"; index="^string_of_int (bvv.bv_index)^""

// Given a term (expected to be [Var] or a [BVar]),  [bv_string_of_term] produces a string saying wether it is a named variable or a De Bruijn one, and specifying it's name and index 
let bv_string_of_term (bv: term): Tac string =
  match inspect bv with
  | Tv_BVar b -> "DeBruijn{"^string_of_bv b^"}"
  | Tv_Var b -> "Named{"^string_of_bv b^"}"
  | _ -> "{[bv_string_of_term] ?}"

let observe abs_description = match abs_description with
  | [x_binder;y_binder;z_binder], body -> 
    ( match collect_app body with
    | _Mktuple3, [x_var,_; y_var,_; z_var,_] ->
      print ( "x_var: " ^ bv_string_of_term x_var ^ "\n"
            ^ "y_var: " ^ bv_string_of_term y_var ^ "\n"
            ^ "z_var: " ^ bv_string_of_term z_var ^ "\n"
            )
    | _ -> fail "Expected tuple3"
    )
  | _ -> fail "Expected 3 abstractions"

let _ = run_tactic (fun _ -> observe (collect_abs_ln abs))
// Inspecting with `inspect_ln` yields the message:
// [F*] x_var: DeBruijn{name=x; index=2}
// [F*] y_var: DeBruijn{name=y; index=1}
// [F*] z_var: DeBruijn{name=z; index=0}

let _ = run_tactic (fun _ -> observe (collect_abs abs)) 
// Inspecting with (effectful) `inspect` yields the message:
// [F*] x_var: Named{name=x; index=256152}
// [F*] y_var: Named{name=y; index=256158}
// [F*] z_var: Named{name=z; index=256163}

If one inspects the term fun x -> fun y -> fun z -> (x, y, z) with inspect_ln, the representation of the variable x in the tuple (x, y, z) is a Tv_BVar, that is a De Bruijn represented variable with index 2. The integer 2 is a suffisient representation for x: x is the binder attached to the thrid last abstraction (the first one being z, and the second one being y) in the stack of abstractions.

Basically, here, the term fun x -> fun y -> fun z -> (x, y, z) is encoded as fun _ -> fun _ -> fun _ -> (<2>, <1>, <0>). This is very impractical while meta-programming: if you move this <2> somewhere else, this might make no sense any longer: fun _ -> fun _ -> (<2>, fun _ -> (<1>, <0>)) makes no sense for instance. The function mk_abs crafts such a term naively: invoking it with inspect yields the value fun x y -> (x, (fun z -> (y, z))) while invoking it with inspect_ln yields (as expected) an error.

let mk_abs tv: Tac term = 
  match tv with
  | [x_binder;y_binder;z_binder], body -> 
    ( match collect_app body with
    | _Mktuple3, [x_var,_; y_var,_; z_var,_] ->
      pack (Tv_Abs x_binder (        // λ x →
        pack (Tv_Abs y_binder        // λ y →
          (mk_e_app (`Mktuple2)         // (
                    [ x_var             //   x, 
                    ; pack (
                      Tv_Abs z_binder   //   λ z →
                         (mk_e_app 
                           (`Mktuple2)  //   (
                           [ y_var      //     y,
                           ; z_var]))   //     z
                    ]))                 //   )
        )                               // )
      )
    | _ -> fail "Expected tuple3"
    )
  | _ -> fail "Expected 3 abstractions"

let _ = assert True by (
  let t: int -> int -> (int * (int -> (int * int))) = unquote (mk_abs (collect_abs abs)) in
  print (term_to_string (quote t))
)
// prints "fun x y -> x, (fun z -> y, z)"

let _ = assert True by (
  let t: int -> int -> (int * (int -> (int * int))) = unquote (mk_abs (collect_abs_ln abs)) in
  print (term_to_string (quote t))
)
// (Error 228) user tactic failed: `unquote: Cannot type fun _ y -> x, (fun z -> y, z) in context (). Error = (Violation of locally nameless convention: x)`

With inspect, you end up with term views without any De Bruijn-represented variables (i.e. no Tv_BVar, only Tv_Var), and thus, you can move them freely without worrying about their positions relatively to abstractions.