val infer_binder_types (g: env) (bs: list binder) (v: vprop) : T.Tac (list binder)
let infer_binder_types (g:env) (bs:list binder) (v:vprop)
  : T.Tac (list binder) =
  match bs with
  | [] -> []
  | _ ->
    let tv = elab_term v in
    if not (is_host_term tv)
    then fail g (Some v.range)
           (Printf.sprintf "assert.infer_binder_types: elaborated %s to %s, which failed the host term check"
              (P.term_to_string v) (T.term_to_string tv));
    let as_binder (b:binder) : R.binder =
      let open R in
      let bv : binder_view = 
        { sort = elab_term b.binder_ty;
          ppname = b.binder_ppname.name;
          qual = Q_Explicit;
          attrs = [] } in
      pack_binder bv
    in
    let abstraction = 
      L.fold_right 
        (fun b (tv:host_term) -> 
         let b = as_binder b in
         R.pack_ln (R.Tv_Abs b tv))
        bs
        tv
    in
    let inst_abstraction, _ = PC.instantiate_term_implicits g (tm_fstar abstraction v.range) in
    match inst_abstraction.t with
    | Tm_FStar t -> refl_abs_binders t []
    | _ -> T.fail "Impossible: instantiated abstraction is not embedded F* term, please file a bug-report"
val infer_binder_types (g: env) (bs: list binder) (v: vprop) : T.Tac (list binder)
let infer_binder_types (g: env) (bs: list binder) (v: vprop) : T.Tac (list binder) =
match bs with
| [] -> []
| _ ->
  let tv = elab_term v in
  if not (is_host_term tv)
  then
    fail g
      (Some v.range)
      (Printf.sprintf "assert.infer_binder_types: elaborated %s to %s, which failed the host term check"
          (P.term_to_string v)
          (T.term_to_string tv));
  let as_binder (b: binder) : R.binder =
    let open R in
    let bv:binder_view =
      { sort = elab_term b.binder_ty; ppname = b.binder_ppname.name; qual = Q_Explicit; attrs = [] }
    in
    pack_binder bv
  in
  let abstraction =
    L.fold_right (fun b (tv: host_term) ->
          let b = as_binder b in
          R.pack_ln (R.Tv_Abs b tv))
      bs
      tv
  in
  let inst_abstraction, _ = PC.instantiate_term_implicits g (tm_fstar abstraction v.range) in
  match inst_abstraction.t with
  | Tm_FStar t -> refl_abs_binders t []
  | _ ->
    T.fail "Impossible: instantiated abstraction is not embedded F* term, please file a bug-report"
Pulse.Checker.AssertWithBinders.fst.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Naming.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.Visit.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.AssertWithBinders.fst
Pulse.Typing.Env.env Prims.list Pulse.Syntax.Base.binder Pulse.Syntax.Base.vprop Prims.Nil Pulse.Syntax.Base.term Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.host_term Pulse.Checker.AssertWithBinders.refl_abs_binders Pulse.Syntax.Base.term' FStar.Tactics.V2.Derived.fail FStar.Pervasives.Native.tuple2 Pulse.Checker.Pure.instantiate_term_implicits Pulse.Syntax.Base.tm_fstar Pulse.Syntax.Base.__proj__Mkterm__item__range FStar.List.Tot.Base.fold_right FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_Abs FStar.Reflection.Types.binder FStar.Reflection.V2.Builtins.pack_binder FStar.Reflection.V2.Data.binder_view FStar.Reflection.V2.Data.Mkbinder_view Pulse.Elaborate.Pure.elab_term Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty FStar.Reflection.V2.Data.Q_Explicit FStar.Reflection.Types.term Pulse.Syntax.Base.__proj__Mkppname__item__name Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname Prims.unit Prims.op_Negation Pulse.Checker.AssertWithBinders.is_host_term Pulse.Typing.Env.fail FStar.Pervasives.Native.Some Pulse.Syntax.Base.range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string FStar.Tactics.V2.Builtins.term_to_string Prims.bool
module Pulse.Checker.AssertWithBinders


open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Base
open Pulse.Elaborate.Pure
open Pulse.Typing.Env

module L = FStar.List.Tot
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module PC = Pulse.Checker.Pure
module P = Pulse.Syntax.Printer
module N = Pulse.Syntax.Naming
module PS = Pulse.Checker.Prover.Substs
module Prover = Pulse.Checker.Prover

module RU = Pulse.RuntimeUtils

let is_host_term (t:R.term) = not (R.Tv_Unknown? (R.inspect_ln t))

let debug_log = Pulse.Typing.debug_log "with_binders"

let option_must (f:option 'a) (msg:string) : T.Tac 'a =
  match f with
  | Some x -> x
  | None -> T.fail msg

let rec refl_abs_binders (t:R.term) (acc:list binder) : T.Tac (list binder) =
  let open R in
  match inspect_ln t with
  | Tv_Abs b body ->
    let {sort; ppname} = R.inspect_binder b in
    let sort = option_must (readback_ty sort)
      (Printf.sprintf "Failed to readback elaborated binder sort %s in refl_abs_binders"
         (T.term_to_string sort)) in
    refl_abs_binders body
     ({ binder_ty = sort; binder_ppname = mk_ppname ppname (RU.range_of_term t) }::acc)
  | _ -> L.rev acc  

let infer_binder_types (g:env) (bs:list binder) (v:vprop)
val infer_binder_types (g: env) (bs: list binder) (v: vprop) : T.Tac (list binder)
g: Pulse.Typing.Env.env -> bs: Prims.list Pulse.Syntax.Base.binder -> v: Pulse.Syntax.Base.vprop
  -> FStar.Tactics.Effect.Tac (Prims.list Pulse.Syntax.Base.binder)