let collect_app = collect_app' []
let collect_app =
collect_app' []
FStar.Tactics.V2.SyntaxHelpers.fst.checked
prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Types.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Tactics.V2.SyntaxHelpers.fst
FStar.Tactics.V2.SyntaxHelpers.collect_app' Prims.Nil FStar.Reflection.V2.Data.argv
module FStar.Tactics.V2.SyntaxHelpers

open FStar.Reflection.V2
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.Types
open FStar.Tactics.NamedView

(* These are fully-named variants of functions found in FStar.Reflection *)

private
let rec collect_arr' (bs : list binder) (c : comp) : Tac (list binder * comp) =
    begin match c with
    | C_Total t ->
        begin match inspect t with
        | Tv_Arrow b c ->
            collect_arr' (b::bs) c
        | _ ->
            (bs, c)
        end
    | _ -> (bs, c)
    end

val collect_arr_bs : typ -> Tac (list binder * comp)
let collect_arr_bs t =
    let (bs, c) = collect_arr' [] (C_Total t) in
    (List.Tot.Base.rev bs, c)

val collect_arr : typ -> Tac (list typ * comp)
let collect_arr t =
    let (bs, c) = collect_arr' [] (C_Total t) in
    let ts = List.Tot.Base.map (fun (b:binder) -> b.sort) bs in
    (List.Tot.Base.rev ts, c)

private
let rec collect_abs' (bs : list binder) (t : term) : Tac (list binder * term) (decreases t) =
    match inspect t with
    | Tv_Abs b t' ->
        collect_abs' (b::bs) t'
    | _ -> (bs, t)

val collect_abs : term -> Tac (list binder * term)
let collect_abs t =
    let (bs, t') = collect_abs' [] t in
    (List.Tot.Base.rev bs, t')

(* Copied from FStar.Tactics.V2.Derived *)
private
let fail (#a:Type) (m:string) = raise #a (TacticFailure m)

let rec mk_arr (bs: list binder) (cod : comp) : Tac term =
    match bs with
    | [] -> fail "mk_arr, empty binders"
    | [b] -> pack (Tv_Arrow b cod)
    | (b::bs) ->
      pack (Tv_Arrow b (C_Total (mk_arr bs cod)))

let rec mk_tot_arr (bs: list binder) (cod : term) : Tac term =
    match bs with
    | [] -> cod
    | (b::bs) ->
      pack (Tv_Arrow b (C_Total (mk_tot_arr bs cod)))

let lookup_lb (lbs:list letbinding) (nm:name) : Tac letbinding =
  let o = FStar.List.Tot.Base.find
             (fun lb -> (inspect_fv lb.lb_fv) = nm)
             lbs
  in
  match o with
  | Some lb -> lb
  | None -> fail "lookup_letbinding: Name not in let group"

let rec inspect_unascribe (t:term) : Tac (tv:term_view{notAscription tv}) =
  match inspect t with
  | Tv_AscribedT t _ _ _
  | Tv_AscribedC t _ _ _ ->
    inspect_unascribe t
  | tv -> tv

(* Helpers for dealing with nested applications and arrows *)
let rec collect_app' (args : list argv) (t : term)
  : Tac (term * list argv) =
    match inspect_unascribe t with
    | Tv_App l r ->
        collect_app' (r::args) l
    | _ -> (t, args)
val collect_app : t: FStar.Tactics.NamedView.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Tactics.NamedView.term * Prims.list FStar.Reflection.V2.Data.argv)
t: FStar.Tactics.NamedView.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Tactics.NamedView.term * Prims.list FStar.Reflection.V2.Data.argv)