DeBruijn.fst

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] ?}"

// Given a [term_view] for the term [abs] above, prints the representation of variables [x], [y] and [z] inside the tuple
let observe (abs_description: term_view) = 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}