val string_of_name (n: name) : Tac string
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"
val string_of_name (n: name) : Tac string
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"
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.name Prims.string Prims.list Prims.op_Hat Meta.Interface.string_of_name FStar.Tactics.V1.Derived.fail
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"
val string_of_name (n: name) : Tac string
n: FStar.Reflection.Types.name -> FStar.Tactics.Effect.Tac Prims.string