val check_universe (g:env) (t:term)
  : T.Tac (u:universe & universe_of g t u)
let check_universe (g:env) (t:term)
  : T.Tac (u:universe & universe_of g t u)
  = let f = elab_env g in
    let rt = elab_term t in
    let ru_opt, issues = catch_all (fun _ -> rtb_universe_of g f rt) in
    T.log_issues issues;
    match ru_opt with
    | None -> 
      fail_doc g (Some t.range) (ill_typed_term t (Some (tm_type u_unknown)) None)

    | Some ru ->
      let proof : squash (T.typing_token f rt (E_Total, R.pack_ln (R.Tv_Type ru))) =
          FStar.Squash.get_proof _
      in
      let proof : RT.typing f rt (E_Total, R.pack_ln (R.Tv_Type ru)) = RT.T_Token _ _ _ proof in
      (| ru, E proof |)
val check_universe (g:env) (t:term)
  : T.Tac (u:universe & universe_of g t u)
let check_universe (g: env) (t: term) : T.Tac (u: universe & universe_of g t u) =
let f = elab_env g in
let rt = elab_term t in
let ru_opt, issues = catch_all (fun _ -> rtb_universe_of g f rt) in
T.log_issues issues;
match ru_opt with
| None -> fail_doc g (Some t.range) (ill_typed_term t (Some (tm_type u_unknown)) None)
| Some ru ->
  let proof:squash (T.typing_token f rt (E_Total, R.pack_ln (R.Tv_Type ru))) =
    FStar.Squash.get_proof _
  in
  let proof:RT.typing f rt (E_Total, R.pack_ln (R.Tv_Type ru)) = RT.T_Token _ _ _ proof in
  (| ru, E proof |)
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.Reflection.Types.universe FStar.Tactics.Types.typing_token FStar.Pervasives.Native.Mktuple2 FStar.Stubs.TypeChecker.Core.tot_or_ghost FStar.Reflection.Types.typ FStar.Stubs.TypeChecker.Core.E_Total FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_Type FStar.Tactics.Types.issues Pulse.Typing.Env.fail_doc Prims.dtuple2 Pulse.Syntax.Base.universe Pulse.Typing.universe_of FStar.Pervasives.Native.Some Pulse.Syntax.Base.range Pulse.Syntax.Base.__proj__Mkterm__item__range Prims.list FStar.Stubs.Pprint.document Pulse.Checker.Pure.ill_typed_term Pulse.Syntax.Pure.tm_type Pulse.Syntax.Pure.u_unknown FStar.Pervasives.Native.None Prims.Mkdtuple2 Pulse.Typing.E FStar.Reflection.Typing.typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term FStar.Reflection.Typing.T_Token Prims.squash FStar.Squash.get_proof Prims.unit FStar.Tactics.V2.Builtins.log_issues FStar.Pervasives.Native.tuple2 Pulse.Checker.Pure.catch_all Pulse.Checker.Pure.rtb_universe_of FStar.Reflection.Types.term FStar.Reflection.Types.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')]

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)
    
let check_universe (g:env) (t:term)
val check_universe (g:env) (t:term)
  : T.Tac (u:universe & universe_of g t u)
g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac
    (Prims.dtuple2 Pulse.Syntax.Base.universe (fun u45 -> Pulse.Typing.universe_of g t u45))