val instantiate_term_implicits (g:env) (t:term)
  : T.Tac (term & term)
let instantiate_term_implicits (g:env) (t0:term) =
  let f = elab_env g in
  let rt = elab_term t0 in
  let f = RU.env_set_range f (Pulse.Typing.Env.get_range g (Some t0.range)) in
  let topt, issues = catch_all (fun _ -> rtb_instantiate_implicits g f rt) in
  T.log_issues issues;
  match topt with
  | None -> 
    let open Pulse.PP in
    fail_doc g (Some t0.range) [
      prefix 4 1 (text "Could not infer implicit arguments in")
                 (pp t0)
    ]
  | Some (t, ty) ->
    let topt = readback_ty t in
    let tyopt = readback_ty ty in
    match topt, tyopt with
    | Some t, Some ty -> t, ty
    | Some _, None ->
      fail g (Some t0.range) (readback_failure ty)
    | None, _ ->
      fail g (Some t0.range) (readback_failure t)
val instantiate_term_implicits (g:env) (t:term)
  : T.Tac (term & term)
let instantiate_term_implicits (g: env) (t0: term) =
let f = elab_env g in
let rt = elab_term t0 in
let f = RU.env_set_range f (Pulse.Typing.Env.get_range g (Some t0.range)) in
let topt, issues = catch_all (fun _ -> rtb_instantiate_implicits g f rt) in
T.log_issues issues;
match topt with
| None ->
  let open Pulse.PP in
  fail_doc g (Some t0.range) [prefix 4 1 (text "Could not infer implicit arguments in") (pp t0)]
| Some (t, ty) ->
  let topt = readback_ty t in
  let tyopt = readback_ty ty in
  match topt, tyopt with
  | Some t, Some ty -> t, ty
  | Some _, None -> fail g (Some t0.range) (readback_failure ty)
  | None, _ -> fail g (Some t0.range) (readback_failure t)
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.option FStar.Pervasives.Native.tuple2 FStar.Reflection.Types.term FStar.Reflection.Types.typ FStar.Tactics.Types.issues Pulse.Typing.Env.fail_doc FStar.Pervasives.Native.Some Pulse.Syntax.Base.range Pulse.Syntax.Base.__proj__Mkterm__item__range Prims.list FStar.Stubs.Pprint.document Prims.Cons Prims.Nil FStar.Stubs.Pprint.prefix Pulse.PP.text Pulse.PP.pp Pulse.PP.uu___44 FStar.Pervasives.Native.Mktuple2 Prims.eq2 Pulse.Elaborate.Pure.elab_term Pulse.Typing.Env.fail Prims.string Pulse.Checker.Pure.readback_failure Pulse.Readback.readback_ty Prims.unit FStar.Tactics.V2.Builtins.log_issues Pulse.Checker.Pure.catch_all Pulse.Checker.Pure.rtb_instantiate_implicits FStar.Reflection.Types.env Pulse.RuntimeUtils.env_set_range FStar.Range.range Pulse.Typing.Env.get_range Pulse.Typing.elab_env
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

let readback_failure (s:R.term) =
  Printf.sprintf "Internal error: failed to readback F* term %s"
                 (T.term_to_string s)

let ill_typed_term (t:term) (expected_typ:option term) (got_typ:option term) : Tac (list FStar.Stubs.Pprint.document) =
  let open Pulse.PP in
  match expected_typ, got_typ with
  | None, _ ->
    [text "Ill-typed term: " ^^ pp t]
  | Some ty, None ->
    [group (text "Expected term of type" ^/^ pp ty) ^/^
     group (text "got term" ^/^ pp t)]
  | Some ty, Some ty' ->
    [group (text "Expected term of type" ^/^ pp ty) ^/^
     group (text "got term" ^/^ pp t) ^/^
     group (text "of type" ^/^ pp ty')]
val instantiate_term_implicits (g:env) (t:term)
  : T.Tac (term & term)
g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac (Pulse.Syntax.Base.term * Pulse.Syntax.Base.term)