val check_bind
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_Bind? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)
let check_bind
  (g:env)
  (ctxt:vprop)
  (ctxt_typing:tot_typing g ctxt tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term {Tm_Bind? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g ctxt post_hint) =

  let g = Pulse.Typing.Env.push_context g "check_bind" t.range in

  debug_prover g (fun _ ->
    Printf.sprintf "checking bind:\n%s\n" (P.st_term_to_string t));
 
  if None? post_hint
  then fail g (Some t.range) "check_bind: post hint is not set, please add an annotation";

  let Tm_Bind { binder; head=e1; body=e2 } = t.term in
  if Tm_Admit? e1.term
  then ( //Discard the continuation if the head is an admit
    check g ctxt ctxt_typing post_hint res_ppname e1
  )
  else (
    let (| x, g1, _, (| ctxt', ctxt'_typing |), k1 |) =
      let r = check g ctxt ctxt_typing None binder.binder_ppname e1 in
      (* Check that the type matches the annotation, if any *)
      let ty = binder.binder_ty in
      begin match ty.t with
      | Tm_Unknown -> ()
      | _ ->
        let (| ty, _, _ |) = check_tot_term g ty in //elaborate it first
        let (| _, _, (| _, t, _ |), _, _ |) = r in
        // TODO: once we have the rename operation then we should
        // ditch this check and just elaborate the bind
        //   let x : ty = stapp in ...
        // to
        //   let x0 = stapp in
        //   let x : t = x0 in
        //   rename x0 x; ...
        // to leverage the pure case
        if not (eq_tm ty t) then
          fail g (Some e1.range)
            (Printf.sprintf "Type mismatch: expected %s, got %s" (P.term_to_string ty) (P.term_to_string t))
      end;
      r
    in
    let d : st_typing_in_ctxt g1 ctxt' post_hint =
      let ppname = mk_ppname_no_range "_bind_c" in
      let r =
        check g1 ctxt' ctxt'_typing post_hint ppname (open_st_term_nv e2 (binder.binder_ppname, x)) in
        apply_checker_result_k #_ #_ #(Some?.v post_hint) r ppname in
    let d : st_typing_in_ctxt g ctxt post_hint = k1 post_hint d in

    checker_result_for_st_typing d res_ppname
  )
val check_bind
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_Bind? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)
let check_bind
      (g: env)
      (ctxt: vprop)
      (ctxt_typing: tot_typing g ctxt tm_vprop)
      (post_hint: post_hint_opt g)
      (res_ppname: ppname)
      (t: st_term{Tm_Bind? t.term})
      (check: check_t)
    : T.Tac (checker_result_t g ctxt post_hint) =
let g = Pulse.Typing.Env.push_context g "check_bind" t.range in
debug_prover g (fun _ -> Printf.sprintf "checking bind:\n%s\n" (P.st_term_to_string t));
if None? post_hint
then fail g (Some t.range) "check_bind: post hint is not set, please add an annotation";
let Tm_Bind { binder = binder ; head = e1 ; body = e2 } = t.term in
if Tm_Admit? e1.term
then (check g ctxt ctxt_typing post_hint res_ppname e1)
else
  (let (| x , g1 , _ , (| ctxt' , ctxt'_typing |) , k1 |) =
      let r = check g ctxt ctxt_typing None binder.binder_ppname e1 in
      let ty = binder.binder_ty in
      (match ty.t with
        | Tm_Unknown -> ()
        | _ ->
          let (| ty , _ , _ |) = check_tot_term g ty in
          let (| _ , _ , (| _ , t , _ |) , _ , _ |) = r in
          if not (eq_tm ty t)
          then
            fail g
              (Some e1.range)
              (Printf.sprintf "Type mismatch: expected %s, got %s"
                  (P.term_to_string ty)
                  (P.term_to_string t)));
      r
    in
    let d:st_typing_in_ctxt g1 ctxt' post_hint =
      let ppname = mk_ppname_no_range "_bind_c" in
      let r =
        check g1 ctxt' ctxt'_typing post_hint ppname (open_st_term_nv e2 (binder.binder_ppname, x))
      in
      apply_checker_result_k #_ #_ #(Some?.v post_hint) r ppname
    in
    let d:st_typing_in_ctxt g ctxt post_hint = k1 post_hint d in
    checker_result_for_st_typing d res_ppname)
Pulse.Checker.Bind.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.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.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Bind.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.vprop Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop Pulse.Typing.post_hint_opt Pulse.Syntax.Base.ppname Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_Bind Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Checker.Base.check_t Pulse.Syntax.Base.binder Pulse.Syntax.Base.uu___is_Tm_Admit Pulse.Checker.Base.checker_result_t Prims.bool Pulse.Syntax.Base.var Pulse.Typing.Env.env_extends FStar.Pervasives.dtuple3 Pulse.Syntax.Base.universe Pulse.Syntax.Base.typ Pulse.Typing.universe_of Pulse.Checker.Base.continuation_elaborator FStar.Pervasives.dfst Prims.Mkdtuple2 Pulse.Checker.Base.checker_result_inv FStar.Pervasives.Native.None Pulse.Typing.post_hint_t Pulse.Checker.Base.checker_result_for_st_typing Pulse.Typing.Combinators.st_typing_in_ctxt Pulse.Checker.Base.apply_checker_result_k FStar.Pervasives.Native.__proj__Some__item__v FStar.Pervasives.Native.Some Pulse.Syntax.Naming.open_st_term_nv FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname Pulse.Syntax.Base.mk_ppname_no_range Prims.unit Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.term' Pulse.Syntax.Base.term Prims.dtuple2 FStar.Pervasives.Mkdtuple3 Prims.op_Negation Pulse.Syntax.Base.eq_tm Pulse.Typing.Env.fail Pulse.Syntax.Base.range Pulse.Syntax.Base.__proj__Mkst_term__item__range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string Pulse.Checker.Pure.check_tot_term Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Syntax.Base.st_term' FStar.Pervasives.Native.uu___is_None Pulse.Checker.Prover.Util.debug_prover Pulse.Syntax.Printer.st_term_to_string Prims.eq2 Pulse.Typing.Env.push_context
module Pulse.Checker.Bind

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Checker.Base
open Pulse.Checker.Pure
open Pulse.Checker.Prover

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer
module Metatheory = Pulse.Typing.Metatheory
module PS = Pulse.Checker.Prover.Substs

#push-options "--z3rlimit_factor 4 --fuel 1 --ifuel 1"
let check_bind
  (g:env)
  (ctxt:vprop)
  (ctxt_typing:tot_typing g ctxt tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term {Tm_Bind? t.term})
val check_bind
  (g:env)
  (pre:term)
  (pre_typing:tot_typing g pre tm_vprop)
  (post_hint:post_hint_opt g)
  (res_ppname:ppname)
  (t:st_term{Tm_Bind? t.term})
  (check:check_t)
  : T.Tac (checker_result_t g pre post_hint)

    g: Pulse.Typing.Env.env ->
    pre: Pulse.Syntax.Base.term ->
    pre_typing: Pulse.Typing.tot_typing g pre Pulse.Syntax.Base.tm_vprop ->
    post_hint: Pulse.Typing.post_hint_opt g ->
    res_ppname: Pulse.Syntax.Base.ppname ->
    t: Pulse.Syntax.Base.st_term{Tm_Bind? (Mkst_term?.term t)} ->
    check: Pulse.Checker.Base.check_t
  -> FStar.Tactics.Effect.Tac (Pulse.Checker.Base.checker_result_t g pre post_hint)