val elab_lift (#g #c1 #c2: _) (d: lift_comp g c1 c2) (e: R.term) : Tot R.term
let elab_lift #g #c1 #c2 (d:lift_comp g c1 c2) (e:R.term)
  : Tot R.term
  = match d with
    | Lift_STAtomic_ST _ _ ->
      let t = elab_term (comp_res c1) in
      mk_lift_atomic_stt
        (comp_u c1)
        (elab_term (comp_res c1))
        t
        (mk_abs t R.Q_Explicit (elab_term (comp_post c1)))
        e
        
    | Lift_STGhost_STAtomic _ _ (| reveal_a, reveal_a_typing |) ->
      let t = elab_term (comp_res c1) in
      mk_lift_ghost_atomic
        (comp_u c1)
        t
        (elab_term (comp_inames c1))
        (elab_term (comp_pre c1))
        (mk_abs t R.Q_Explicit (elab_term (comp_post c1)))
        e
        (elab_term reveal_a)
val elab_lift (#g #c1 #c2: _) (d: lift_comp g c1 c2) (e: R.term) : Tot R.term
let elab_lift #g #c1 #c2 (d: lift_comp g c1 c2) (e: R.term) : Tot R.term =
match d with
| Lift_STAtomic_ST _ _ ->
  let t = elab_term (comp_res c1) in
  mk_lift_atomic_stt (comp_u c1)
    (elab_term (comp_res c1))
    t
    (mk_abs t R.Q_Explicit (elab_term (comp_post c1)))
    e
| Lift_STGhost_STAtomic _ _ (| reveal_a , reveal_a_typing |) ->
  let t = elab_term (comp_res c1) in
  mk_lift_ghost_atomic (comp_u c1)
    t
    (elab_term (comp_inames c1))
    (elab_term (comp_pre c1))
    (mk_abs t R.Q_Explicit (elab_term (comp_post c1)))
    e
    (elab_term reveal_a)
Pulse.Elaborate.Core.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.Pure.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Elaborate.Core.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.comp Pulse.Typing.lift_comp FStar.Reflection.Types.term Pulse.Syntax.Base.comp_st Prims.l_and Prims.b2t Pulse.Syntax.Base.uu___is_C_STAtomic Prims.eq2 Pulse.Syntax.Base.term Pulse.Syntax.Base.comp_inames Pulse.Syntax.Base.tm_emp_inames Pulse.Reflection.Util.mk_lift_atomic_stt Pulse.Syntax.Base.comp_u Pulse.Elaborate.Pure.elab_term Pulse.Syntax.Base.comp_res Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Pulse.Syntax.Base.comp_post Pulse.Syntax.Base.uu___is_C_STGhost Pulse.Typing.tot_typing Pulse.Typing.non_informative_witness_t Pulse.Reflection.Util.mk_lift_ghost_atomic Pulse.Syntax.Base.comp_pre
module Pulse.Elaborate.Core
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.Elaborate.Pure
open Pulse.Typing

open Pulse.Reflection.Util

let elab_frame (c:comp_st) (frame:term) (e:R.term) =
  let u = comp_u c in
  let ty = elab_term (comp_res c) in
  let pre = elab_term (comp_pre c) in
  let post = elab_term (comp_post c) in
  if C_ST? c
  then mk_frame_stt u ty pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
  else let opened = elab_term (comp_inames c) in      
       if C_STAtomic? c
       then mk_frame_stt_atomic u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e
       else let _ = assert (C_STGhost? c) in
            mk_frame_stt_ghost u ty opened pre (mk_abs ty R.Q_Explicit post) (elab_term frame) e

let elab_sub (c1 c2:comp_st) (e:R.term) =
  let ty = elab_term (comp_res c1) in
  let u = comp_u c1 in
  let pre1 = elab_term (comp_pre c1) in
  let pre2 = elab_term (comp_pre c2) in
  let post1 = mk_abs ty R.Q_Explicit (elab_term (comp_post c1)) in
  let post2 = mk_abs ty R.Q_Explicit (elab_term (comp_post c2)) in
  if C_ST? c1
  then mk_sub_stt u ty pre1 pre2 post1 post2 e
  else let opened = elab_term (comp_inames c1) in
       if C_STAtomic? c1
       then mk_sub_stt_atomic u ty opened pre1 pre2 post1 post2 e
       else let _ = assert (C_STGhost? c1) in
            mk_sub_stt_ghost u ty opened pre1 pre2 post1 post2 e


let elab_bind #g #x #c1 #c2 #c
              (bc:bind_comp g x c1 c2 c)
              (e1 e2:R.term)
  : R.term
  = let t1 = elab_term (comp_res c1) in
    let t2 = elab_term (comp_res c2) in
    match bc with
    | Bind_comp _ _ _ _ _ _ _ ->
      if C_ST? c1
      then
        mk_bind_stt
          (comp_u c1)
          (comp_u c2)
          t1 t2
          (elab_term (comp_pre c1))
          (mk_abs t1 R.Q_Explicit (elab_term (comp_post c1)))
          (mk_abs t2 R.Q_Explicit (elab_term (comp_post c2)))
          e1 e2
      else 
        mk_bind_ghost
          (comp_u c1)
          (comp_u c2)
          t1 t2
          (elab_term (comp_inames c1))
          (elab_term (comp_pre c1))
          (mk_abs t1 R.Q_Explicit (elab_term (comp_post c1)))
          (mk_abs t2 R.Q_Explicit (elab_term (comp_post c2)))
          e1 e2
  
    | Bind_comp_ghost_l _ _ _ _ (| reveal_a, reveal_a_typing |) _ _ _ ->
      mk_bind_ghost_atomic
        (comp_u c1)
        (comp_u c2)
        t1 t2
        (elab_term (comp_inames c1))
        (elab_term (comp_pre c1))
        (mk_abs t1 R.Q_Explicit (elab_term (comp_post c1)))
        (mk_abs t2 R.Q_Explicit (elab_term (comp_post c2)))
        e1 e2
        (elab_term reveal_a)

    | Bind_comp_ghost_r _ _ _ _ (| reveal_b, reveal_b_typing |) _ _ _ ->
      mk_bind_atomic_ghost
        (comp_u c1)
        (comp_u c2)
        t1 t2
        (elab_term (comp_inames c1))
        (elab_term (comp_pre c1))
        (mk_abs t1 R.Q_Explicit (elab_term (comp_post c1)))
        (mk_abs t2 R.Q_Explicit (elab_term (comp_post c2)))
        e1 e2
        (elab_term reveal_b)

let elab_lift #g #c1 #c2 (d:lift_comp g c1 c2) (e:R.term)
val elab_lift (#g #c1 #c2: _) (d: lift_comp g c1 c2) (e: R.term) : Tot R.term
d: Pulse.Typing.lift_comp g c1 c2 -> e: FStar.Reflection.Types.term -> FStar.Reflection.Types.term