let return_stt_atomic_noeq_lid = mk_pulse_lib_core_lid "return_stt_atomic_noeq"
let return_stt_atomic_noeq_lid =
mk_pulse_lib_core_lid "return_stt_atomic_noeq"
Pulse.Reflection.Util.fst.checked
Pulse.RuntimeUtils.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.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 FStar.Ghost.fsti.checked
Pulse.Reflection.Util.fst
Pulse.Reflection.Util.mk_pulse_lib_core_lid
module Pulse.Reflection.Util

module R = FStar.Reflection.V2
module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
open FStar.List.Tot

let pulse_lib_core = ["Pulse"; "Lib"; "Core"]
let mk_pulse_lib_core_lid s = pulse_lib_core@[s]

let tun = R.pack_ln R.Tv_Unknown
let unit_lid = R.unit_lid
let bool_lid = R.bool_lid
let int_lid  = R.int_lid
let erased_lid = ["FStar"; "Ghost"; "erased"]
let hide_lid = ["FStar"; "Ghost"; "hide"]
let reveal_lid = ["FStar"; "Ghost"; "reveal"]
let vprop_lid = mk_pulse_lib_core_lid "vprop"
let vprop_fv = R.pack_fv vprop_lid
let vprop_tm = R.pack_ln (R.Tv_FVar vprop_fv)
let unit_fv = R.pack_fv unit_lid
let unit_tm = R.pack_ln (R.Tv_FVar unit_fv)
let bool_fv = R.pack_fv bool_lid
let bool_tm = R.pack_ln (R.Tv_FVar bool_fv)
let nat_lid = ["Prims"; "nat"]
let nat_fv = R.pack_fv nat_lid
let nat_tm = R.pack_ln (R.Tv_FVar nat_fv)
let szt_lid = ["FStar"; "SizeT"; "t"]
let szt_fv = R.pack_fv szt_lid
let szt_tm = R.pack_ln (R.Tv_FVar szt_fv)
let szv_lid = ["FStar"; "SizeT"; "v"]
let szv_fv = R.pack_fv szv_lid
let szv_tm = R.pack_ln (R.Tv_FVar szv_fv)
let seq_lid = ["FStar"; "Seq"; "Base"; "seq"]
let seq_create_lid = ["FStar"; "Seq"; "Base"; "create"]


let tuple2_lid = ["FStar"; "Pervasives"; "Native"; "tuple2"]
let fst_lid = ["FStar"; "Pervasives"; "Native"; "fst"]
let snd_lid = ["FStar"; "Pervasives"; "Native"; "snd"]

let mk_tuple2 (u1 u2:R.universe) (a1 a2:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv tuple2_lid) [u1; u2]) in
  let t = pack_ln (Tv_App t (a1, Q_Explicit)) in
  pack_ln (Tv_App t (a2, Q_Explicit))

let mk_fst (u1 u2:R.universe) (a1 a2 e:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv fst_lid) [u1; u2]) in
  let t = pack_ln (Tv_App t (a1, Q_Implicit)) in
  let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
  pack_ln (Tv_App t (e, Q_Explicit))
  
let mk_snd (u1 u2:R.universe) (a1 a2 e:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv snd_lid) [u1; u2]) in
  let t = pack_ln (Tv_App t (a1, Q_Implicit)) in
  let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
  pack_ln (Tv_App t (e, Q_Explicit))

let true_tm = R.pack_ln (R.Tv_Const (R.C_True))
let false_tm = R.pack_ln (R.Tv_Const (R.C_False))

let emp_lid = mk_pulse_lib_core_lid "emp"
let inames_lid = mk_pulse_lib_core_lid "inames"

let star_lid = mk_pulse_lib_core_lid "op_Star_Star"

let mk_star (l r:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_FVar (pack_fv star_lid)) in
  let t = pack_ln (Tv_App t (l, Q_Explicit)) in
  pack_ln (Tv_App t (r, Q_Explicit))

let pure_lid = mk_pulse_lib_core_lid "pure"
let exists_lid = mk_pulse_lib_core_lid "exists_"
let forall_lid = mk_pulse_lib_core_lid "forall_"
let args_of (tms:list R.term) =
  List.Tot.map (fun x -> x, R.Q_Explicit) tms

let mk_pure (p:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_FVar (pack_fv pure_lid)) in
  pack_ln (Tv_App t (p, Q_Explicit))

let uzero = R.pack_universe (R.Uv_Zero)

let pulse_lib_reference = ["Pulse"; "Lib"; "Reference"]
let mk_pulse_lib_reference_lid s = pulse_lib_reference@[s]

let mk_squash (u:R.universe) (ty:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv R.squash_qn) [u]) in
  pack_ln (Tv_App t (ty, Q_Explicit))

let mk_eq2 (u:R.universe) (ty e1 e2:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv R.eq2_qn) [u]) in
  let t = pack_ln (Tv_App t (ty, Q_Implicit)) in
  let t = pack_ln (Tv_App t (e1, Q_Explicit)) in
  pack_ln (Tv_App t (e2, Q_Explicit))

let stt_admit_lid = mk_pulse_lib_core_lid "stt_admit"
let mk_stt_admit (u:R.universe) (t pre post:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv stt_admit_lid) [u]) in
  let t = pack_ln (Tv_App t (t, Q_Explicit)) in
  let t = pack_ln (Tv_App t (pre, Q_Explicit)) in
  pack_ln (Tv_App t (post, Q_Explicit))

let stt_atomic_admit_lid = mk_pulse_lib_core_lid "stt_atomic_admit"
let mk_stt_atomic_admit (u:R.universe) (t pre post:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv stt_atomic_admit_lid) [u]) in
  let t = pack_ln (Tv_App t (t, Q_Explicit)) in
  let t = pack_ln (Tv_App t (pre, Q_Explicit)) in
  pack_ln (Tv_App t (post, Q_Explicit))

let stt_ghost_admit_lid = mk_pulse_lib_core_lid "stt_ghost_admit"
let mk_stt_ghost_admit (u:R.universe) (t pre post:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv stt_ghost_admit_lid) [u]) in
  let t = pack_ln (Tv_App t (t, Q_Explicit)) in
  let t = pack_ln (Tv_App t (pre, Q_Explicit)) in
  pack_ln (Tv_App t (post, Q_Explicit))

let emp_inames_lid = mk_pulse_lib_core_lid "emp_inames"
let elim_pure_lid = mk_pulse_lib_core_lid "elim_pure"

 //the thunked, value-type counterpart of the effect STT
let stt_lid = mk_pulse_lib_core_lid "stt"
let stt_fv = R.pack_fv stt_lid
let stt_tm = R.pack_ln (R.Tv_FVar stt_fv)
let mk_stt_comp (u:R.universe) (res pre post:R.term) : Tot R.term =
  let t = R.pack_ln (R.Tv_UInst stt_fv [u]) in
  let t = R.pack_ln (R.Tv_App t (res, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (pre, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (post, R.Q_Explicit))

let stt_atomic_lid = mk_pulse_lib_core_lid "stt_atomic"
let stt_atomic_fv = R.pack_fv stt_atomic_lid
let stt_atomic_tm = R.pack_ln (R.Tv_FVar stt_atomic_fv)
let mk_stt_atomic_comp (u:R.universe) (a inames pre post:R.term) =
  let t = R.pack_ln (R.Tv_UInst stt_atomic_fv [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (inames, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (pre, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (post, R.Q_Explicit))

let stt_ghost_lid = mk_pulse_lib_core_lid "stt_ghost"
let stt_ghost_fv = R.pack_fv stt_ghost_lid
let stt_ghost_tm = R.pack_ln (R.Tv_FVar stt_ghost_fv)
let mk_stt_ghost_comp (u:R.universe) (a inames pre post:R.term) =
  let t = R.pack_ln (R.Tv_UInst stt_ghost_fv [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (inames, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (pre, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (post, R.Q_Explicit))

let mk_stt_ghost_comp_post_equiv (g:R.env) (u:R.universe) (a inames pre post1 post2:R.term)
  (posts_equiv:RT.equiv g post1 post2)
  : RT.equiv g (mk_stt_ghost_comp u a inames pre post1)
               (mk_stt_ghost_comp u a inames pre post2) =
  let open R in
  let open RT in
  let t = R.pack_ln (R.Tv_UInst stt_ghost_fv [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (inames, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (pre, R.Q_Explicit)) in
  Rel_ctxt g post1 post2
    (Ctxt_app_arg t Q_Explicit Ctxt_hole)
    posts_equiv

let mk_total t = R.C_Total t
let mk_ghost t = R.C_GTotal t
let binder_of_t_q t q = RT.binder_of_t_q t q
let binder_of_t_q_s (t:R.term) (q:R.aqualv) (s:RT.pp_name_t) = RT.mk_binder s t q
let bound_var i : R.term = RT.bound_var i
let mk_name i : R.term = R.pack_ln (R.Tv_Var (R.pack_namedv (RT.make_namedv i)))

let arrow_dom = (R.term & R.aqualv)
let mk_arrow (f:arrow_dom) (out:R.term) : R.term =
  let ty, q = f in
  R.pack_ln (R.Tv_Arrow (binder_of_t_q ty q) (R.pack_comp (mk_total out)))
let mk_arrow_with_name (s:RT.pp_name_t) (f:arrow_dom) (out:R.term) : R.term =
  let ty, q = f in
  R.pack_ln (R.Tv_Arrow (binder_of_t_q_s ty q s) (R.pack_comp (mk_total out)))
let mk_ghost_arrow_with_name (s:RT.pp_name_t) (f:arrow_dom) (out:R.term) : R.term =
  let ty, q = f in
  R.pack_ln (R.Tv_Arrow (binder_of_t_q_s ty q s) (R.pack_comp (mk_ghost out)))
let mk_abs ty qual t : R.term = RT.mk_abs ty qual t
let mk_abs_with_name s ty qual t : R.term =  R.pack_ln (R.Tv_Abs (binder_of_t_q_s ty qual s) t)
let mk_abs_with_name_and_range s r ty qual t : R.term = 
  let b = (binder_of_t_q_s ty qual s) in
  let b = RU.binder_set_range b r in
  R.pack_ln (R.Tv_Abs b t)
  
let mk_erased (u:R.universe) (t:R.term) : R.term =
  let hd = R.pack_ln (R.Tv_UInst (R.pack_fv erased_lid) [u]) in
  R.pack_ln (R.Tv_App hd (t, R.Q_Explicit))

let mk_reveal (u:R.universe) (t:R.term) (e:R.term) : R.term =
  let hd = R.pack_ln (R.Tv_UInst (R.pack_fv reveal_lid) [u]) in
  let hd = R.pack_ln (R.Tv_App hd (t, R.Q_Implicit)) in
  R.pack_ln (R.Tv_App hd (e, R.Q_Explicit))

let elim_exists_lid = mk_pulse_lib_core_lid "elim_exists"
let intro_exists_lid = mk_pulse_lib_core_lid "intro_exists"
let intro_exists_erased_lid = mk_pulse_lib_core_lid "intro_exists_erased"

let mk_exists (u:R.universe) (a p:R.term) =
  let t = R.pack_ln (R.Tv_UInst (R.pack_fv exists_lid) [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Implicit)) in
  R.pack_ln (R.Tv_App t (p, R.Q_Explicit))

let mk_forall (u:R.universe) (a p:R.term) =
  let t = R.pack_ln (R.Tv_UInst (R.pack_fv forall_lid) [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Implicit)) in
  R.pack_ln (R.Tv_App t (p, R.Q_Explicit))

let mk_elim_exists (u:R.universe) (a p:R.term) : R.term =
  let t = R.pack_ln (R.Tv_UInst (R.pack_fv elim_exists_lid) [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Implicit)) in
  R.pack_ln (R.Tv_App t (p, R.Q_Explicit))

let mk_intro_exists (u:R.universe) (a p:R.term) (e:R.term) : R.term =
  let t = R.pack_ln (R.Tv_UInst (R.pack_fv intro_exists_lid) [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Implicit)) in
  let t = R.pack_ln (R.Tv_App t (p, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (e, R.Q_Explicit))

let mk_intro_exists_erased (u:R.universe) (a p:R.term) (e:R.term) : R.term =
  let t = R.pack_ln (R.Tv_UInst (R.pack_fv intro_exists_erased_lid) [u]) in
  let t = R.pack_ln (R.Tv_App t (a, R.Q_Implicit)) in
  let t = R.pack_ln (R.Tv_App t (p, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (e, R.Q_Explicit))

let while_lid = mk_pulse_lib_core_lid "while_loop"

let mk_while (inv cond body:R.term) : R.term =
  let t = R.pack_ln (R.Tv_FVar (R.pack_fv while_lid)) in
  let t = R.pack_ln (R.Tv_App t (inv, R.Q_Explicit)) in
  let t = R.pack_ln (R.Tv_App t (cond, R.Q_Explicit)) in
  R.pack_ln (R.Tv_App t (body, R.Q_Explicit))

let vprop_eq_tm t1 t2 =
  let open R in
  let u2 =
    pack_universe (Uv_Succ (pack_universe (Uv_Succ (pack_universe Uv_Zero)))) in
  let t = pack_ln (Tv_UInst (pack_fv eq2_qn) [u2]) in
  let t = pack_ln (Tv_App t (pack_ln (Tv_FVar (pack_fv vprop_lid)), Q_Implicit)) in
  let t = pack_ln (Tv_App t (t1, Q_Explicit)) in
  let t = pack_ln (Tv_App t (t2, Q_Explicit)) in
  t

let emp_inames_tm : R.term = R.pack_ln (R.Tv_FVar (R.pack_fv emp_inames_lid))

let non_informative_witness_lid = mk_pulse_lib_core_lid "non_informative_witness"
let non_informative_witness_rt (u:R.universe) (a:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv non_informative_witness_lid) [u]) in
  let t = pack_ln (Tv_App t (a, Q_Explicit)) in
  t


let stt_vprop_equiv_fv =
  R.pack_fv (mk_pulse_lib_core_lid "vprop_equiv")
let stt_vprop_equiv_tm =
  R.pack_ln (R.Tv_FVar stt_vprop_equiv_fv)
let stt_vprop_equiv (t1 t2:R.term) =
  let open R in
		let t = pack_ln (Tv_App stt_vprop_equiv_tm (t1, Q_Explicit)) in
		pack_ln (Tv_App t (t2, Q_Explicit))

let return_stt_lid = mk_pulse_lib_core_lid "return_stt"
let return_stt_noeq_lid = mk_pulse_lib_core_lid "return"
val return_stt_atomic_noeq_lid : Prims.list Prims.string
Prims.list Prims.string