let sub_stt_equiv_pre u t pre1 post1 pre2 post2 = 
  mk_arrow (stt_vprop_equiv pre1 pre2, R.Q_Explicit)
           (sub_stt_equiv_post u t pre1 pre2 post1 post2)
let sub_stt_equiv_pre u t pre1 post1 pre2 post2 =
mk_arrow (stt_vprop_equiv pre1 pre2, R.Q_Explicit) (sub_stt_equiv_post u t pre1 pre2 post1 post2)
Pulse.Soundness.Common.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Soundness.Common.fst
FStar.Reflection.Types.universe FStar.Reflection.Types.term Pulse.Reflection.Util.mk_arrow FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv Pulse.Reflection.Util.stt_vprop_equiv FStar.Reflection.V2.Data.Q_Explicit Pulse.Soundness.Common.sub_stt_equiv_post
module Pulse.Soundness.Common
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
open Pulse.Elaborate

let ln_comp = c:comp_st { ln_c c }

let rec extend_env_l_lookup_fvar (g:R.env) (sg:env_bindings) (fv:R.fv) (us:R.universes)
  : Lemma 
    (ensures
      RT.lookup_fvar_uinst (extend_env_l g sg) fv us ==
      RT.lookup_fvar_uinst g fv us)
    [SMTPat (RT.lookup_fvar_uinst (extend_env_l g sg) fv us)]
  = match sg with
    | [] -> ()
    | hd::tl -> extend_env_l_lookup_fvar g tl fv us


let elab_term_opt (b:option term) =
  match b with
  | Some b -> Some (elab_term b)
  | None -> None

// let rec extend_env_l_lookup_bvar (g:R.env) (sg:env_bindings) (x:var)
//   : Lemma 
//     (requires (forall x. RT.lookup_bvar g x == None))
//     (ensures (RT.lookup_bvar (extend_env_l g sg) x == elab_term_opt (lookup sg x)))
//     (decreases sg)
//     [SMTPat (RT.lookup_bvar (extend_env_l g sg) x)]
//   = match sg with
//     | [] -> ()
//     | hd :: tl -> extend_env_l_lookup_bvar g tl x

let lookup_elab_env (g:env) (x:var)
  : Lemma 
    (ensures (RT.lookup_bvar (elab_env g) x == elab_term_opt (lookup g x)))
    [SMTPat (RT.lookup_bvar (elab_env g) x)]
  = admit ()  // TODO: FIX ME!!!!
  
let tot_typing_soundness (#g:env)
                         (#e:term)
                         (#t:term)
                         (d:tot_typing g e t)
  : GTot (RT.tot_typing (elab_env g) (elab_term e) (elab_term t))
  = let E d = d in
    d

let ghost_typing_soundness (#g:env)
                           (#e:term)
                           (#t:term)
                           (d:ghost_typing g e t)
  : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t))
  = let E d = d in
    d

#push-options "--z3rlimit_factor 4"
let mk_t_abs_tot (g:env)
                 (#u:universe)
                 (#q:option qualifier)
                 (#ty:term)
                 (ppname:ppname)
                 (t_typing:tot_typing g ty (tm_type u))
                 (#body:term)
                 (#body_ty:term)
                 (#x:var { None? (lookup g x) /\ ~(x `Set.mem` freevars body) })
                 (body_typing:tot_typing (push_binding g x ppname ty) (open_term body x) body_ty)
  : GTot (RT.tot_typing (elab_env g)
            (mk_abs_with_name ppname.name (elab_term ty) (elab_qual q) (elab_term body))
            (elab_term (tm_arrow {binder_ty=ty; binder_ppname=ppname} q (close_comp (C_Tot body_ty) x))))
  = let c = C_Tot body_ty in
    let r_ty = elab_term ty in
    let r_body = elab_term (open_term body x) in
    let r_c = elab_comp c in
    let r_t_typing = tot_typing_soundness t_typing in
    let r_body_typing = tot_typing_soundness body_typing in
    RT.well_typed_terms_are_ln _ _ _ r_body_typing;
    RT.open_close_inverse r_body x;
    elab_comp_close_commute c x;      
    elab_freevars body;
    assert (~ (x `Set.mem` RT.freevars (elab_term body)));
    assume (~ (x `Set.mem` RT.freevars (RT.close_term r_body x)));
    RT.close_term_spec (elab_comp c) x;
    assert (elab_term (tm_type u) == RT.tm_type u);
    let r_t_typing : RT.tot_typing (elab_env g) r_ty (RT.tm_type u)
      = coerce_eq () r_t_typing //strange that this coercion is needed
    in
    let d : RT.tot_typing (elab_env g)
              (mk_abs_with_name ppname.name (elab_term ty) (elab_qual q)
                 (RT.close_term (elab_term (open_term body x)) x))
              (elab_term (tm_arrow {binder_ty=ty;binder_ppname=ppname} q (close_comp (C_Tot body_ty) x)))
          = 
    RT.T_Abs (elab_env g)
             x
             r_ty
             (RT.close_term r_body x)
             (T.E_Total, r_c)
             u ppname.name (elab_qual q)
             _
             r_t_typing
             r_body_typing
    in
    elab_open_commute' body (null_var x) 0;
    RT.open_term_spec (elab_term body) x;
    assert (elab_term (open_term body x) ==
            RT.open_term (elab_term body) x);
    let d : RT.typing _
                      (mk_abs_with_name ppname.name (elab_term ty) (elab_qual q)
                              (RT.close_term (RT.open_term (elab_term body) x) x))
                      _
          = d 
    in
    RT.close_open_inverse (elab_term body) x;
    d

let mk_t_abs (g:env)
             (#u:universe)
             (#ty:term)
             (#q:option qualifier)
             (#t_typing:typing g ty T.E_Total (tm_type u))
             (ppname:ppname)
             (r_t_typing:RT.tot_typing (elab_env g)
                                       (elab_term ty)
                                       (elab_comp (C_Tot (tm_type u))))
             (#body:st_term)
             (#x:var { None? (lookup g x) /\ ~(x `Set.mem` freevars_st body) })
             (#c:comp)
             (#body_typing:st_typing (push_binding g x ppname ty) (open_st_term body x) c)
             (r_body_typing:RT.tot_typing (elab_env (push_binding g x ppname ty))
                                          (elab_st_typing body_typing)
                                          (elab_comp c))
  : GTot (RT.tot_typing (elab_env g)
            (mk_abs_with_name ppname.name (elab_term ty) (elab_qual q) (RT.close_term (elab_st_typing body_typing) x))
            (elab_term (tm_arrow {binder_ty=ty;binder_ppname=ppname} q (close_comp c x))))
  = let r_ty = elab_term ty in
    let r_body = elab_st_typing body_typing in
    let r_c = elab_comp c in
    RT.well_typed_terms_are_ln _ _ _ r_body_typing;
    RT.open_close_inverse r_body x;
    elab_comp_close_commute c x;      
    assume (~ (x `Set.mem` RT.freevars (RT.close_term r_body x)));
    RT.close_term_spec (elab_comp c) x;
    RT.T_Abs (elab_env g)
             x
             r_ty
             (RT.close_term r_body x)
             (T.E_Total, r_c)
             u ppname.name (elab_qual q)
             _
             r_t_typing
             r_body_typing

(*** Typing of combinators used
     in the elaboration **)


(** Type of bind **)

let bind_res (u2:R.universe) (t2 pre post2:R.term) =
  mk_stt_comp u2 t2 pre post2

let g_type_bind (u2:R.universe) (t1 t2 post1 post2:R.term) =
    mk_arrow (t1, R.Q_Explicit)
             (bind_res u2 t2 (R.mk_app post1 [bound_var 0 (* x *), R.Q_Explicit]) post2)

let bind_type_t1_t2_pre_post1_post2_f (u1 u2:R.universe) (t1 t2 pre post1 post2:R.term) =
  mk_arrow (g_type_bind u2 t1 t2 post1 post2, R.Q_Explicit)
           (bind_res u2 t2 pre post2)

let bind_type_t1_t2_pre_post1_post2 (u1 u2:R.universe) (t1 t2 pre post1 post2:R.term) =
  let f_type = mk_stt_comp u1 t1 pre post1 in
  mk_arrow (f_type, R.Q_Explicit)
           (bind_type_t1_t2_pre_post1_post2_f u1 u2 t1 t2 pre post1 post2)

let post2_type_bind t2 = mk_arrow (t2, R.Q_Explicit) vprop_tm
let bind_type_t1_t2_pre_post1 (u1 u2:R.universe) (t1 t2 pre post1:R.term) =
  let var = 0 in
  let post2 = mk_name var in
  mk_arrow (post2_type_bind t2, R.Q_Implicit)
           (RT.subst_term (bind_type_t1_t2_pre_post1_post2 u1 u2 t1 t2 pre post1 post2)
                          [ RT.ND var 0 ])

let post1_type_bind t1 = mk_arrow (t1, R.Q_Explicit) vprop_tm
let bind_type_t1_t2_pre (u1 u2:R.universe) (t1 t2 pre:R.term) =
  let var = 1 in
  let post1 = mk_name var in
  mk_arrow (post1_type_bind t1, R.Q_Implicit)
           (RT.subst_term (bind_type_t1_t2_pre_post1 u1 u2 t1 t2 pre post1)
                          [ RT.ND var 0 ])

let bind_type_t1_t2 (u1 u2:R.universe) (t1 t2:R.term) =
  let var = 2 in
  let pre = mk_name var in
  let pre_type = vprop_tm in
  mk_arrow (pre_type, R.Q_Implicit)
           (RT.subst_term (bind_type_t1_t2_pre u1 u2 t1 t2 pre)
                          [ RT.ND var 0 ])

let bind_type_t1 (u1 u2:R.universe) (t1:R.term) =
  let var = 3 in
  let t2 = mk_name var in
  let t2_type = RT.tm_type u2 in
  mk_arrow (t2_type, R.Q_Implicit)
           (RT.subst_term (bind_type_t1_t2 u1 u2 t1 t2)
                          [ RT.ND var 0 ])

let bind_type (u1 u2:R.universe) =
  let var = 4 in
  let t1 = mk_name var in
  let t1_type = RT.tm_type u1 in
  mk_arrow (t1_type, R.Q_Implicit)
           (RT.subst_term (bind_type_t1 u1 u2 t1)
                          [ RT.ND var 0 ])

(** Type of frame **)

let mk_star (l r:R.term) =
  let open R in
  let head = pack_ln (Tv_FVar (pack_fv star_lid)) in      
  R.mk_app head [(l, Q_Explicit); (r, Q_Explicit)]

let frame_res (u:R.universe) (t pre post frame:R.term) =
    mk_stt_comp u t
                  (mk_star pre frame)
                  (mk_abs t R.Q_Explicit (mk_star (R.mk_app post [bound_var 0, R.Q_Explicit]) frame))

let frame_type_t_pre_post_frame (u:R.universe) (t pre post frame:R.term) =
  let open R in
  let f_type = mk_stt_comp u t pre post in
  mk_arrow (f_type, Q_Explicit)
           (frame_res u t pre post frame)

let frame_type_t_pre_post (u:R.universe) (t pre post:R.term) =
  let var = 0 in
  let frame = mk_name var in
  mk_arrow (vprop_tm, R.Q_Explicit)
           (RT.close_term (frame_res u t pre post frame) var)

let frame_type_t_pre (u:R.universe) (t pre:R.term) =
  let var = 1 in
  let post = mk_name var in
  let post_type = mk_arrow (t, R.Q_Explicit) vprop_tm in
  mk_arrow (post_type, R.Q_Implicit)
           (RT.close_term (frame_type_t_pre_post u t pre post) var)

let frame_type_t (u:R.universe) (t:R.term) =
  let var = 2 in
  let pre = mk_name var in
  let pre_type = vprop_tm in
  mk_arrow (pre_type, R.Q_Implicit)
           (RT.close_term (frame_type_t_pre u t pre) var)

let frame_type (u:R.universe) =
  let var = 3 in
  let t = mk_name var in
  let t_type = RT.tm_type u in
  mk_arrow (t_type, R.Q_Implicit)
           (RT.close_term (frame_type_t u t) var)


(** Type of sub_stt **)

let stt_vprop_post_equiv_fv = R.pack_fv (mk_pulse_lib_core_lid "vprop_post_equiv")
let stt_vprop_post_equiv_univ_inst u = R.pack_ln (R.Tv_UInst stt_vprop_post_equiv_fv [u])
let stt_vprop_post_equiv (u:R.universe) (t t1 t2:R.term) = 
  R.mk_app (stt_vprop_post_equiv_univ_inst u) 
           [(t, R.Q_Implicit); (t1, R.Q_Explicit); (t2, R.Q_Explicit)]

let sub_stt_res u t pre post = mk_stt_comp u t pre post

let sub_stt_equiv_post u t pre1 post1 pre2 post2 = 
  mk_arrow (stt_vprop_post_equiv u t post1 post2, R.Q_Explicit)
           (sub_stt_res u t pre2 post2)
val sub_stt_equiv_pre : u126: FStar.Reflection.Types.universe ->
    t: FStar.Reflection.Types.term ->
    pre1: FStar.Reflection.Types.term ->
    post1: FStar.Reflection.Types.term ->
    pre2: FStar.Reflection.Types.term ->
    post2: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term

    u126: FStar.Reflection.Types.universe ->
    t: FStar.Reflection.Types.term ->
    pre1: FStar.Reflection.Types.term ->
    post1: FStar.Reflection.Types.term ->
    pre2: FStar.Reflection.Types.term ->
    post2: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term