val par_post (u: universe) (aL aR postL postR: term) (x: var) : term
let par_post (u:universe) (aL aR:term) (postL postR:term) (x:var) : term =
  let x_tm = RT.var_as_term x in
  let postL = pack_ln (Tv_App postL (mk_fst u u aL aR x_tm, Q_Explicit)) in
  let postR = pack_ln (Tv_App postR (mk_snd u u aL aR x_tm, Q_Explicit)) in
  let post = mk_star postL postR in
  RT.subst_term post [ RT.ND x 0 ]
val par_post (u: universe) (aL aR postL postR: term) (x: var) : term
let par_post (u: universe) (aL aR postL postR: term) (x: var) : term =
let x_tm = RT.var_as_term x in
let postL = pack_ln (Tv_App postL (mk_fst u u aL aR x_tm, Q_Explicit)) in
let postR = pack_ln (Tv_App postR (mk_snd u u aL aR x_tm, Q_Explicit)) in
let post = mk_star postL postR in
RT.subst_term post [RT.ND x 0]
Pulse.Steel.Wrapper.Typing.fsti.checked
Pulse.Reflection.Util.fst.checked prims.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Steel.Wrapper.Typing.fsti
FStar.Reflection.Types.universe FStar.Reflection.Types.term FStar.Reflection.V2.Data.var FStar.Reflection.Typing.subst_term Prims.Cons FStar.Reflection.Typing.subst_elt FStar.Reflection.Typing.ND Prims.Nil Pulse.Reflection.Util.mk_star FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_App FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv Pulse.Reflection.Util.mk_snd FStar.Reflection.V2.Data.Q_Explicit Pulse.Reflection.Util.mk_fst FStar.Reflection.Typing.var_as_term
module Pulse.Steel.Wrapper.Typing

open FStar.Reflection.V2
open Pulse.Reflection.Util

module RT = FStar.Reflection.Typing

let return_post_with_eq (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  let x_tm = RT.var_as_term x in
  let eq2_tm = mk_eq2 u a x_tm e in
  let p_app_x = pack_ln (Tv_App p (x_tm, Q_Explicit)) in  
  let star_tm = mk_star p_app_x (mk_pure eq2_tm) in
  mk_abs a Q_Explicit (RT.subst_term star_tm [ RT.ND x 0 ])

let return_stt_comp (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  mk_stt_comp u a
    (pack_ln (Tv_App p (e, Q_Explicit)))
    (return_post_with_eq u a e p x)

val return_stt_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#e:term)
  (#p:term)
  (x:var{None? (RT.lookup_bvar g x)})
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (e_typing:RT.tot_typing g e a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_return u a e p)
            (return_stt_comp u a e p x))

let return_stt_noeq_comp (u:universe) (a:term) (x:term) (p:term) : term =
  mk_stt_comp u a (pack_ln (Tv_App p (x, Q_Explicit))) p

val return_stt_noeq_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#x:term)
  (#p:term)
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (x_typing:RT.tot_typing g x a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_return_noeq u a x p)
            (return_stt_noeq_comp u a x p))

let return_stt_atomic_comp (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  mk_stt_atomic_comp u a emp_inames_tm
    (pack_ln (Tv_App p (e, Q_Explicit)))
    (return_post_with_eq u a e p x)

val return_stt_atomic_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#e:term)
  (#p:term)
  (x:var{None? (RT.lookup_bvar g x)})
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (e_typing:RT.tot_typing g e a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_atomic_return u a e p)
            (return_stt_atomic_comp u a e p x))

let return_stt_atomic_noeq_comp (u:universe) (a:term) (x:term) (p:term) : term =
  mk_stt_atomic_comp u a emp_inames_tm (pack_ln (Tv_App p (x, Q_Explicit))) p

val return_stt_atomic_noeq_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#x:term)
  (#p:term)
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (x_typing:RT.tot_typing g x a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_atomic_return_noeq u a x p)
            (return_stt_atomic_noeq_comp u a x p))

let return_stt_ghost_comp (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  mk_stt_ghost_comp u a emp_inames_tm
    (pack_ln (Tv_App p (e, Q_Explicit)))
    (return_post_with_eq u a e p x)

val return_stt_ghost_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#e:term)
  (#p:term)
  (x:var{None? (RT.lookup_bvar g x)})
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (e_typing:RT.tot_typing g e a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_ghost_return u a e p)
            (return_stt_ghost_comp u a e p x))

let return_stt_ghost_noeq_comp (u:universe) (a:term) (x:term) (p:term) : term =
  mk_stt_ghost_comp u a emp_inames_tm (pack_ln (Tv_App p (x, Q_Explicit))) p

val return_stt_ghost_noeq_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#x:term)
  (#p:term)
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (x_typing:RT.tot_typing g x a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_ghost_return_noeq u a x p)
            (return_stt_ghost_noeq_comp u a x p))


(*

 g |- inv  : bool -> vprop
 g |- cond : stt<0> bool (exists_ inv) inv
 g |- body : stt<0> unit (inv true) (fun _ -> exists_ inv)
 -------------------------------------------------------------------------
 g |- while inv cond body : stt<0> unit (exists_ inv) (fun _ -> inv false)

*)

val while_typing
  (#g:env)
  (#inv:term)
  (#cond:term)
  (#body:term)
  (inv_typing:RT.tot_typing g
                inv
                (mk_arrow (bool_tm, Q_Explicit) vprop_tm))
  (cond_typing:RT.tot_typing g
                 cond
                 (mk_stt_comp uzero bool_tm (mk_exists uzero bool_tm inv) inv))
  (body_typing:RT.tot_typing g
                 body
                 (mk_stt_comp uzero unit_tm
                    (pack_ln (Tv_App inv (true_tm, Q_Explicit)))
                    (mk_abs unit_tm Q_Explicit (mk_exists uzero bool_tm inv))))
  : RT.tot_typing g
      (mk_while inv cond body)
      (mk_stt_comp uzero unit_tm (mk_exists uzero bool_tm inv)
         (mk_abs unit_tm Q_Explicit (pack_ln (Tv_App inv (false_tm, Q_Explicit)))))
val par_post (u: universe) (aL aR postL postR: term) (x: var) : term

    u38: FStar.Reflection.Types.universe ->
    aL: FStar.Reflection.Types.term ->
    aR: FStar.Reflection.Types.term ->
    postL: FStar.Reflection.Types.term ->
    postR: FStar.Reflection.Types.term ->
    x: FStar.Reflection.V2.Data.var
  -> FStar.Reflection.Types.term