let rtb_instantiate_implicits g f t =
  debug g (fun _ -> Printf.sprintf "Calling instantiate_implicits on %s"
                                       (T.term_to_string t));
  (* WARN: unary dependence, see comment in RU *)
  let t = RU.deep_transform_to_unary_applications t in
  let res, iss = RTB.instantiate_implicits f t in
  match res with
  | None ->
    debug g (fun _ -> "Returned from instantiate_implicits: None");
    res, iss
  | Some (t, _) ->
    debug g (fun _ -> Printf.sprintf "Returned from instantiate_implicits: %s" (T.term_to_string t));
    res, iss
let rtb_instantiate_implicits g f t =
debug g (fun _ -> Printf.sprintf "Calling instantiate_implicits on %s" (T.term_to_string t));
let t = RU.deep_transform_to_unary_applications t in
let res, iss = RTB.instantiate_implicits f t in
match res with
| None ->
  debug g (fun _ -> "Returned from instantiate_implicits: None");
  res, iss
| Some (t, _) ->
  debug g (fun _ -> Printf.sprintf "Returned from instantiate_implicits: %s" (T.term_to_string t));
  res, iss
Pulse.Checker.Pure.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked Pulse.PP.fst.checked prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.Squash.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Issue.fsti.checked
Pulse.Checker.Pure.fst
Pulse.Typing.Env.env FStar.Reflection.Types.env FStar.Reflection.Types.term FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.Reflection.Types.typ FStar.Tactics.Types.issues FStar.Pervasives.Native.Mktuple2 Prims.unit Pulse.Checker.Pure.debug Prims.string FStar.Printf.sprintf FStar.Tactics.V2.Builtins.term_to_string FStar.Tactics.V2.Builtins.instantiate_implicits FStar.Tactics.V2.Builtins.ret_t Prims.eq2 Pulse.RuntimeUtils.deep_transform_to_unary_applications
module Pulse.Checker.Pure
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.Tactics.V2
open FStar.Reflection.V2 (* shadow named view *)

open Pulse.Reflection
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
module P = Pulse.Syntax.Printer
module RTB = FStar.Tactics.V2.Builtins
module RU = Pulse.RuntimeUtils

let debug (g:env) (msg: unit -> T.Tac string) =
  let tac_debugging = T.debugging () in
  if tac_debugging || RU.debug_at_level (fstar_env g) "refl_tc_callbacks"
  then T.print (print_context g ^ "\n" ^ msg())

let rtb_core_check_term g f e =
  debug g (fun _ ->
    Printf.sprintf "(%s) Calling core_check_term on %s" 
          (T.range_to_string (RU.range_of_term e))
          (T.term_to_string e));
  let res = RTB.core_compute_term_type f e in
  res

let rtb_tc_term g f e =
  (* WARN: unary dependence, see comment in RU *)
  let e = RU.deep_transform_to_unary_applications e in
  debug g (fun _ ->
    Printf.sprintf "(%s) Calling tc_term on %s"
      (T.range_to_string (RU.range_of_term e))
      (T.term_to_string e));
  let res = RTB.tc_term f e in
  res

let rtb_universe_of g f e =
  debug g (fun _ ->
    Printf.sprintf "(%s) Calling universe_of on %s"
      (T.range_to_string (RU.range_of_term e))
      (T.term_to_string e));
  let res = RTB.universe_of f e in
  res

let rtb_check_subtyping g (t1 t2:term) =
  debug g (fun _ ->
    Printf.sprintf "(%s, %s) Calling check_subtyping on %s <: %s"
        (T.range_to_string (t1.range))
        (T.range_to_string (t2.range))
        (P.term_to_string t1)
        (P.term_to_string t2));
  let res = RTB.check_subtyping (elab_env g) (elab_term t1) (elab_term t2) in
  res
val rtb_instantiate_implicits : g: Pulse.Typing.Env.env -> f: FStar.Reflection.Types.env -> t: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Reflection.Types.term * FStar.Reflection.Types.typ) *
      FStar.Tactics.Types.issues)
g: Pulse.Typing.Env.env -> f: FStar.Reflection.Types.env -> t: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Reflection.Types.term * FStar.Reflection.Types.typ) *
      FStar.Tactics.Types.issues)