val post_hint_from_comp_typing (#g:env) (#c:comp_st) (ct:Metatheory.comp_typing_u g c)
  : post_hint_for_env g
let post_hint_from_comp_typing #g #c ct = 
  let st_comp_typing = Metatheory.comp_typing_inversion ct in
  let (| ty_typing, pre_typing, x, post_typing |) = Metatheory.st_comp_typing_inversion st_comp_typing in
  let p : post_hint_t = 
    { g;
      ctag_hint = Some (ctag_of_comp_st c);
      ret_ty = comp_res c; u=comp_u c; 
      ty_typing=ty_typing;
      post=comp_post c;
      post_typing=post_typing_as_abstraction post_typing }
  in
  p
val post_hint_from_comp_typing (#g:env) (#c:comp_st) (ct:Metatheory.comp_typing_u g c)
  : post_hint_for_env g
let post_hint_from_comp_typing #g #c ct =
let st_comp_typing = Metatheory.comp_typing_inversion ct in
let (| ty_typing , pre_typing , x , post_typing |) =
  Metatheory.st_comp_typing_inversion st_comp_typing
in
let p:post_hint_t =
  {
    g = g;
    ctag_hint = Some (ctag_of_comp_st c);
    ret_ty = comp_res c;
    u = comp_u c;
    ty_typing = ty_typing;
    post = comp_post c;
    post_typing = post_typing_as_abstraction post_typing
  }
in
p
Pulse.Checker.Base.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.LN.fsti.checked Pulse.Typing.FV.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Syntax.Printer.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Checker.Pure.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.Ghost.fsti.checked
Pulse.Checker.Base.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.comp_st Pulse.Typing.Metatheory.Base.comp_typing_u Pulse.Typing.universe_of Pulse.Syntax.Base.__proj__Mkst_comp__item__res Pulse.Syntax.Base.st_comp_of_comp Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Typing.tot_typing Pulse.Syntax.Base.__proj__Mkst_comp__item__pre Pulse.Syntax.Base.tm_vprop Pulse.Syntax.Base.var Pulse.Typing.fresh_wrt Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.__proj__Mkst_comp__item__post Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Syntax.Naming.open_term Pulse.Typing.post_hint_t Pulse.Typing.Mkpost_hint_t FStar.Pervasives.Native.Some Pulse.Syntax.Base.ctag Pulse.Syntax.Base.ctag_of_comp_st Pulse.Syntax.Base.comp_res Pulse.Syntax.Base.comp_u Pulse.Syntax.Base.comp_post Pulse.Checker.Base.post_typing_as_abstraction Pulse.Typing.post_hint_for_env FStar.Pervasives.dtuple4 Pulse.Typing.Metatheory.Base.st_comp_typing_inversion Pulse.Typing.st_comp_typing Pulse.Typing.Metatheory.Base.comp_typing_inversion
module Pulse.Checker.Base

module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module Metatheory = Pulse.Typing.Metatheory
module CP = Pulse.Checker.Pure
module RU = Pulse.RuntimeUtils
module FV = Pulse.Typing.FV
module P = Pulse.Syntax.Printer

open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory

let format_failed_goal (g:env) (ctxt:list term) (goal:list term) =
  let terms_to_strings (ts:list term)= T.map Pulse.Syntax.Printer.term_to_string ts in
  let numbered_list ss = 
       let _, s = T.fold_left (fun (i, acc) s -> (i+1, Printf.sprintf "%d. %s" i s :: acc)) (1, []) ss in
       String.concat "\n  " (List.rev s)
  in
  let format_terms (ts:list term) = numbered_list (terms_to_strings ts) in
  Printf.sprintf 
    "Failed to prove the following goals:\n  \
     %s\n\
     The remaining conjuncts in the separation logic context available for use are:\n  \
     %s\n\
     The typing context is:\n  \
     %s\n"
    (format_terms goal)
    (format_terms ctxt)
    (env_to_string g)


let mk_arrow ty t = RT.mk_arrow (elab_term ty) T.Q_Explicit (elab_term t)
let mk_abs ty t = RT.(mk_abs (elab_term ty) T.Q_Explicit (elab_term t))

let post_typing_as_abstraction
  (#g:env) (#x:var) (#ty:term) (#t:term { fresh_wrt x g (freevars t) })
  (_:tot_typing (push_binding g x ppname_default ty) (open_term t x) tm_vprop)
  : FStar.Ghost.erased (RT.tot_typing (elab_env g) (mk_abs ty t) (mk_arrow ty tm_vprop))                                 
  = admit()

let intro_post_hint g ctag_opt ret_ty_opt post =
  let x = fresh g in
  let ret_ty = 
      match ret_ty_opt with
      | None -> tm_fstar RT.unit_ty FStar.Range.range_0
      | Some t -> t
  in
  let ret_ty, _ = CP.instantiate_term_implicits g ret_ty in
  let (| u, ty_typing |) = CP.check_universe g ret_ty in
  let (| post, post_typing |) = CP.check_vprop (push_binding g x ppname_default ret_ty) (open_term_nv post (v_as_nv x)) in 
  let post' = close_term post x in
  Pulse.Typing.FV.freevars_close_term post x 0;
  assume (open_term post' x == post);
  { g; ctag_hint=ctag_opt; ret_ty; u; ty_typing; post=post'; post_typing=post_typing_as_abstraction #_ #_ #_ #post' post_typing }
val post_hint_from_comp_typing (#g:env) (#c:comp_st) (ct:Metatheory.comp_typing_u g c)
  : post_hint_for_env g
ct: Pulse.Typing.Metatheory.Base.comp_typing_u g c -> Pulse.Typing.post_hint_for_env g