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
let rtb_check_subtyping g (t1: term) (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
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 Pulse.Syntax.Base.term FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Tactics.Types.subtyping_token Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term FStar.Tactics.Types.issues FStar.Tactics.V2.Builtins.check_subtyping FStar.Tactics.V2.Builtins.ret_t Prims.unit Pulse.Checker.Pure.debug Prims.string FStar.Printf.sprintf FStar.Tactics.V2.Builtins.range_to_string Pulse.Syntax.Base.__proj__Mkterm__item__range Pulse.Syntax.Printer.term_to_string
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
val rtb_check_subtyping : g: Pulse.Typing.Env.env -> t1: Pulse.Syntax.Base.term -> t2: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Tactics.Types.subtyping_token (Pulse.Typing.elab_env g)
            (Pulse.Elaborate.Pure.elab_term t1)
            (Pulse.Elaborate.Pure.elab_term t2)) *
      FStar.Tactics.Types.issues)
g: Pulse.Typing.Env.env -> t1: Pulse.Syntax.Base.term -> t2: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Tactics.Types.subtyping_token (Pulse.Typing.elab_env g)
            (Pulse.Elaborate.Pure.elab_term t1)
            (Pulse.Elaborate.Pure.elab_term t2)) *
      FStar.Tactics.Types.issues)