let readback_failure (s:R.term) =
  Printf.sprintf "Internal error: failed to readback F* term %s"
                 (T.term_to_string s)
let readback_failure (s: R.term) =
Printf.sprintf "Internal error: failed to readback F* term %s" (T.term_to_string s)
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
FStar.Reflection.Types.term FStar.Printf.sprintf Prims.string FStar.Tactics.V2.Builtins.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

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_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_core_check_term_at_type g f e eff t =
  debug g (fun _ ->
    Printf.sprintf "(%s) Calling core_check_term on %s and %s"
                (T.range_to_string (RU.range_of_term e))
                (T.term_to_string e)
                (T.term_to_string t));
  let res = RTB.core_check_term f e t eff in
  res

let mk_squash t =
  let sq : R.term = pack_ln (Tv_UInst (pack_fv squash_qn) [u_zero]) in
  mk_e_app sq [t]

let squash_prop_validity_token f p (t:prop_validity_token f (mk_squash p))
  : prop_validity_token f p
  = admit(); t

let rtb_check_prop_validity (g:env) (f:_) (p:_) = 
  debug g (fun _ -> 
    Printf.sprintf "(%s) Calling check_prop_validity on %s"
          (T.range_to_string (RU.range_of_term p))
          (T.term_to_string p));
  let sp = mk_squash p in
  let res, issues = RTB.check_prop_validity f sp in
  match res with
  | None -> None, issues
  | Some tok -> Some (squash_prop_validity_token f p tok), issues

let exn_as_issue (e:exn) : FStar.Issue.issue = 
  FStar.Issue.mk_issue "Error" (RU.print_exn e) None None []

let catch_all (f:unit -> Tac (option 'a & issues))
  : Tac (option 'a & issues)
  = match T.catch f with
    | Inl exn ->
      None, [exn_as_issue exn]
    | Inr v -> v
val readback_failure : s: FStar.Reflection.Types.term -> FStar.Tactics.Effect.Tac (Prims.string <: Type0)
s: FStar.Reflection.Types.term -> FStar.Tactics.Effect.Tac (Prims.string <: Type0)