val readback_qual (q:R.aqualv)
  : option qualifier
let readback_qual = function
  | R.Q_Implicit -> Some Implicit
  | _ -> None
val readback_qual (q:R.aqualv)
  : option qualifier
let readback_qual =
function
| R.Q_Implicit -> Some Implicit
| _ -> None
Pulse.Readback.fst.checked
Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Readback.fst
FStar.Reflection.V2.Data.aqualv FStar.Pervasives.Native.Some Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.Implicit FStar.Pervasives.Native.None FStar.Pervasives.Native.option
module Pulse.Readback
module R = FStar.Reflection.V2
open Pulse.Syntax.Base
open Pulse.Reflection.Util
module RU = Pulse.RuntimeUtils
module T = FStar.Tactics
module P = Pulse.Syntax.Printer
let debug_log (f: unit -> T.Tac unit) : T.Tac unit = if RU.debug_at_level_no_module "readback" then f()

let (let?) (f:option 'a) (g:'a -> option 'b) : option 'b =
  match f with
  | None -> None
  | Some x -> g x


#push-options "--z3rlimit_factor 20"
// TODO: FIXME: may be mark as opaque_to_smt
let try_readback_st_comp
  (t:R.term)
  (readback_ty:(t':R.term ->
                option (ty:term { elab_term ty == t' })))

  : option (c:comp{elab_comp c == t}) =

  let open R in
  let hd, args = collect_app_ln t in
  match inspect_ln hd with
  | Tv_UInst fv [u] ->
    let fv_lid = inspect_fv fv in
    if fv_lid = stt_lid
    then match args with
         | [res; pre; post] ->
           (match inspect_ln (fst post) with
            | Tv_Abs b body ->
              let { qual=aq; attrs=attrs; sort=sort } =
                  inspect_binder b
              in    
              assume (fv == stt_fv);
              assume (aq == Q_Explicit           /\
                      attrs == []                /\
                      sort == fst res /\
                      snd res == Q_Explicit      /\
                      snd pre == Q_Explicit      /\
                      snd post == Q_Explicit);

              assume (t == mk_stt_comp u (fst res) (fst pre) (mk_abs (fst res) R.Q_Explicit body));
              let? res' = readback_ty (fst res) in
              let? pre' = readback_ty (fst pre) in
              let? post' = readback_ty body in
              let c = C_ST {u; res=res'; pre=pre';post=post'} in
              Some (c <: c:Pulse.Syntax.Base.comp{ elab_comp c == t })
            | _ -> None)
         | _ -> None
    else if fv_lid = stt_atomic_lid || fv_lid = stt_ghost_lid
    then match args with
         | [res; opened; pre; post] ->
           (match inspect_ln (fst post) with
            | Tv_Abs b body ->
              let { qual=aq; attrs=attrs }
                  = inspect_binder b
              in    
              let? res' = readback_ty (fst res) in
              let? opened' = readback_ty (fst opened) in
              let? pre' = readback_ty (fst pre) in
              let? post' = readback_ty body in
              if fv_lid = stt_atomic_lid
              then begin
                assume (t == mk_stt_atomic_comp u (fst res) (fst opened) (fst pre) (mk_abs (fst res) R.Q_Explicit body));
                let c = C_STAtomic opened' ({u; res=res'; pre=pre';post=post'}) in
                Some (c <: c:Pulse.Syntax.Base.comp { elab_comp c == t })
              end
              else begin
                assume (t == mk_stt_ghost_comp u (fst res) (fst opened) (fst pre) (mk_abs (fst res) R.Q_Explicit body));
                let c = C_STGhost opened' ({u; res=res'; pre=pre';post=post'}) in
                Some (c <: c:Pulse.Syntax.Base.comp { elab_comp c == t })
              end
            | _ -> None)
         | _ -> None
    else None  
  | _ -> None
#pop-options
val readback_qual (q:R.aqualv)
  : option qualifier
q: FStar.Reflection.V2.Data.aqualv -> FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier