val lambda_over_p (inv_bv: bv) (sort: typ) (t: term) : Tac term
let lambda_over_p (inv_bv: bv) (sort : typ) (t: term): Tac term =
  pack (Tv_Abs (mk_binder inv_bv sort) t)
val lambda_over_p (inv_bv: bv) (sort: typ) (t: term) : Tac term
let lambda_over_p (inv_bv: bv) (sort: typ) (t: term) : Tac term =
pack (Tv_Abs (mk_binder inv_bv sort) t)
Meta.Interface.fst.checked
prims.fst.checked Meta.Attribute.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.Pure.fst.checked FStar.List.fst.checked
Meta.Interface.fst
FStar.Reflection.Types.bv FStar.Reflection.Types.typ FStar.Reflection.Types.term FStar.Tactics.V1.Builtins.pack FStar.Reflection.V1.Data.Tv_Abs FStar.Reflection.V1.Derived.mk_binder
module Meta.Interface

open FStar.List.Tot
open FStar.Reflection
open FStar.Tactics

/// Local library
/// -------------

let assoc (#a: eqtype) #b (x: a) (l: list (a & b)): Tac b =
  match List.Tot.assoc x l with
  | Some x -> x
  | None -> fail "failure: assoc"

let rec zip #a #b (xs: list a) (ys: list b): Tac (list (a & b)) =
  match xs, ys with
  | x :: xs, y :: ys -> (x, y) :: zip xs ys
  | [], [] -> []
  | _ -> fail "invalid argument: zip"

/// Actual tactic
/// -------------
///
/// All function nodes in the call-graph are parameterized over an implicit
/// argument ``#i:t_i`` (coming first) that represents the specialization index.
///
/// The goal is to perform a call-graph rewriting, as follows.
///
/// At definition-site, every function ``f #i x`` is replaced by a function
///  ``mk_f #i (g1: g1_t i) ... (gn: gn_t i) x`` where:
///
/// - the gi are the ``specialize`` nodes reachable via a (possibly-empty) path
///   of ``inline`` nodes through the body of ``f``
/// - the gi_t are the types of the original gi, minus that index i, which has
///   been abstracted over, i.e. if gi had type ``#i:t_i -> t`` then ``gi_t`` is
///   ``fun #i:t_i -> t``
///
/// At call-site, when encountering ``f #i e``, we distinguish between two cases.
///
/// - If ``f`` is a specialize node: this becomes ``gi e`` and references the
///   bound variable instead of the global name
/// - If ``f`` is an inline node: this becomes ``mk_f #i gf1 ... gfn e`` where
///   ``gfi`` is the i-th function needed by f, i.e. one of our gk.
///
/// The intended usage is as follows.
///
/// - For each specialize node ``f``, clients instantiate as follows:
///   ``let f_specialized = mk_f I1 g1_specialized ... gn_specialized``
///   where the gn_specialized have been recursively generated the same way.
///
/// The new (rewritten) name of inline nodes is part of the global tactic state,
/// which we thread through as ``state`` below.
noeq
type mapping =
  | Inline: new_name:name -> mapping
  | Specialize: mapping

noeq
type state = {
  // A mapping from a top-level function f to:
  // - a boolean to indicate whether this function is parameterized over the index
  // - its type f_t (of type index -> Type OR Type if the function doesn't take the index);
  // - its inlining status; and
  // - the extra parameters it transitively needs (its g_i).
  seen: list (name & (bool & term & mapping & list name));
  // For debugging purposes only.
  indent: string;
}

/// Helpers
/// -------

let string_of_mapping = function
  | Inline _ -> "inline"
  | Specialize -> "specialize"

let rec string_of_name (n: name): Tac string =
  match n with
  | [ n ] -> n
  | n :: ns -> n ^ "_" ^ string_of_name ns
  | [] -> fail "impossible: empty name"

let rec suffix_name (n: name) (s: string): Tac name =
  match n with
  | [ m; n ] -> cur_module () @ [ String.lowercase m ^ "_" ^ n ^ s ]
  | n :: ns -> suffix_name ns s
  | [ _ ] | [] -> fail "impossible: empty name"

let has_attr (s: sigelt) (x: term) =
  List.Tot.existsb (fun t -> term_eq t x) (sigelt_attrs s)

let has_inline_for_extraction (s: sigelt) =
  List.Tot.existsb (function Inline_for_extraction -> true | _ -> false) (sigelt_quals s)

let is_implicit = function
  | Q_Implicit -> true
  | _ -> false

(* This function assumes that we end up with an effectful arrow that signals the end of the type. *)
let rec push_pre (st: state) (inv_bv: bv) (t: term): Tac term =
  match inspect t with
  | Tv_Arrow bv c ->
      let c =
        match inspect_comp c with
        | C_Eff us e a args decrs ->
            if string_of_name e = "FStar_HyperStack_ST_Stack" then
              let args =
                match args with
                | (pre, qual) :: rest ->
                    let pre =
                      match inspect pre with
                      | Tv_Abs h body ->
                          let body = mk_app (`( /\ )) [ pack (Tv_Var inv_bv), Q_Explicit; body, Q_Explicit ] in
                          pack (Tv_Abs h body)
                      | _ ->
                          fail "impossible: argument to ST.Stack not a fun"
                    in
                    (pre, qual) :: rest
                | _ ->
                    fail ("impossible: effect not fully applied " ^ string_of_name e)
              in
              C_Eff us e a args decrs
            else
              fail ("rewritten function has an unknown effect: " ^ string_of_name e)
        | C_Total t ->
            C_Total (push_pre st inv_bv t)
        | _ ->
            fail ("rewritten type is neither a Tot or a stateful arrow: " ^ term_to_string t)
      in
      let c = pack_comp c in
      pack (Tv_Arrow bv c)
  | _ ->
      print (st.indent ^ "  WARN: no effect found, are you using the specialize tactic on pure code?");
      t

let rec to_reduce t: Tac _ =
  match fst (collect_app t) with
  | Tv_UInst fv _
  | Tv_FVar fv ->
      [ fv_to_string fv ]
  | Tv_Arrow bv c ->
      begin match inspect_comp c with
      | C_Total t -> to_reduce t
      | _ ->
          []
      end
  | _ ->
      []
val lambda_over_p (inv_bv: bv) (sort: typ) (t: term) : Tac term

    inv_bv: FStar.Reflection.Types.bv ->
    sort: FStar.Reflection.Types.typ ->
    t: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac FStar.Reflection.Types.term