val st_equiv_trans (#g: env) (#c0 #c1 #c2: comp) (d01: st_equiv g c0 c1) (d12: st_equiv g c1 c2)
    : option (st_equiv g c0 c2)
let st_equiv_trans (#g:env) (#c0 #c1 #c2:comp) (d01:st_equiv g c0 c1) (d12:st_equiv g c1 c2)
  : option (st_equiv g c0 c2)
  = let ST_VPropEquiv _f _c0 _c1 x c0_pre_typing c0_res_typing c0_post_typing eq_res_01 eq_pre_01 eq_post_01 = d01 in
    let ST_VPropEquiv _f _c1 _c2 y c1_pre_typing c1_res_typing c1_post_typing eq_res_12 eq_pre_12 eq_post_12 = d12 in
    if x = y && eq_tm (comp_res c0) (comp_res c1)
    then Some (
          ST_VPropEquiv g c0 c2 x c0_pre_typing c0_res_typing c0_post_typing
            (RT.Rel_trans _ _ _ _ _ eq_res_01 eq_res_12)
            (VE_Trans _ _ _ _ eq_pre_01 eq_pre_12)
            (VE_Trans _ _ _ _ eq_post_01 eq_post_12)
    )
    else None
val st_equiv_trans (#g: env) (#c0 #c1 #c2: comp) (d01: st_equiv g c0 c1) (d12: st_equiv g c1 c2)
    : option (st_equiv g c0 c2)
let st_equiv_trans (#g: env) (#c0 #c1 #c2: comp) (d01: st_equiv g c0 c1) (d12: st_equiv g c1 c2)
    : option (st_equiv g c0 c2) =
let
ST_VPropEquiv _f _c0 _c1 x c0_pre_typing c0_res_typing c0_post_typing eq_res_01 eq_pre_01 eq_post_01
=
  d01
in
let
ST_VPropEquiv _f _c1 _c2 y c1_pre_typing c1_res_typing c1_post_typing eq_res_12 eq_pre_12 eq_post_12
=
  d12
in
if x = y && eq_tm (comp_res c0) (comp_res c1)
then
  Some
  (ST_VPropEquiv g
      c0
      c2
      x
      c0_pre_typing
      c0_res_typing
      c0_post_typing
      (RT.Rel_trans _ _ _ _ _ eq_res_01 eq_res_12)
      (VE_Trans _ _ _ _ eq_pre_01 eq_pre_12)
      (VE_Trans _ _ _ _ eq_post_01 eq_post_12))
else None
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 Pulse.Typing.st_equiv Pulse.Syntax.Base.comp_st Pulse.Typing.st_equiv_pre Pulse.Syntax.Base.var Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_None Pulse.Syntax.Base.typ Pulse.Typing.Env.lookup Prims.l_not FStar.Set.mem Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.comp_post Pulse.Typing.tot_typing Pulse.Syntax.Base.comp_pre Pulse.Syntax.Base.tm_vprop Pulse.Syntax.Base.comp_res Pulse.Syntax.Pure.tm_type Pulse.Syntax.Base.comp_u Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Syntax.Naming.open_term FStar.Reflection.Typing.equiv Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term Pulse.Typing.vprop_equiv Prims.op_AmpAmp Prims.op_Equality Prims.l_or Pulse.Syntax.Base.eq_tm FStar.Pervasives.Native.Some Pulse.Typing.ST_VPropEquiv FStar.Reflection.Typing.Rel_trans FStar.Reflection.Typing.R_Eq Pulse.Typing.VE_Trans Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option
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 }

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

let k_elab_unit (g:env) (ctxt:term)
  : continuation_elaborator g ctxt g ctxt
  = fun p r -> r

let k_elab_trans
  (#g0:env) (#g1:env { g1 `env_extends` g0 }) (#g2:env { g2 `env_extends` g1 }) (#ctxt0 #ctxt1 #ctxt2:term)
  (k0:continuation_elaborator g0 ctxt0 g1 ctxt1)
  (k1:continuation_elaborator g1 ctxt1 g2 ctxt2 { g1 `env_extends` g0})
   : continuation_elaborator g0 ctxt0 g2 ctxt2
   = fun post_hint res -> k0 post_hint (k1 post_hint res)

let comp_st_with_post (c:comp_st) (post:term)
  : c':comp_st { st_comp_of_comp c' == ({ st_comp_of_comp c with post} <: st_comp) } =
  match c with
  | C_ST st -> C_ST { st with post }
  | C_STGhost i st -> C_STGhost i { st with post }
  | C_STAtomic i st -> C_STAtomic i {st with post}

let ve_unit_r g (p:term) : vprop_equiv g (tm_star p tm_emp) p = 
  VE_Trans _ _ _ _ (VE_Comm _ _ _) (VE_Unit _ _)

let st_equiv_trans (#g:env) (#c0 #c1 #c2:comp) (d01:st_equiv g c0 c1) (d12:st_equiv g c1 c2)
val st_equiv_trans (#g: env) (#c0 #c1 #c2: comp) (d01: st_equiv g c0 c1) (d12: st_equiv g c1 c2)
    : option (st_equiv g c0 c2)
d01: Pulse.Typing.st_equiv g c0 c1 -> d12: Pulse.Typing.st_equiv g c1 c2
  -> FStar.Pervasives.Native.option (Pulse.Typing.st_equiv g c0 c2)