val find_focused_term_in_current_goal : bool -> Tac (exploration_result term)
let find_focused_term_in_current_goal dbg =
  let g = cur_goal () in
  let e = cur_env () in
  print_dbg dbg ("[> find_focused_assert_in_current_goal:\n" ^ term_to_string g);
  begin match unsquash_equality g with
  | Some (l, _) ->
    let c = safe_typ_or_comp dbg e l in
    let ge = mk_genv e [] [] in
    print_dbg dbg ("[> About to explore term:\n" ^ term_to_string l);
    begin match find_focused_term dbg true ge [] c l with
    | Some res ->
      print_dbg dbg ("[> Found focused term:\n" ^ term_to_string res.res);
      res
    | None ->
      mfail ("find_focused_term_in_current_goal: could not find a focused term in the current goal: "
             ^ term_to_string g)
    end
  | _ -> mfail "find_focused_term_in_current_goal: not a squashed equality"
  end
val find_focused_term_in_current_goal : bool -> Tac (exploration_result term)
let find_focused_term_in_current_goal dbg =
let g = cur_goal () in
let e = cur_env () in
print_dbg dbg ("[> find_focused_assert_in_current_goal:\n" ^ term_to_string g);
match unsquash_equality g with
| Some (l, _) ->
  let c = safe_typ_or_comp dbg e l in
  let ge = mk_genv e [] [] in
  print_dbg dbg ("[> About to explore term:\n" ^ term_to_string l);
  (match find_focused_term dbg true ge [] c l with
    | Some res ->
      print_dbg dbg ("[> Found focused term:\n" ^ term_to_string res.res);
      res
    | None ->
      mfail ("find_focused_term_in_current_goal: could not find a focused term in the current goal: " ^
          term_to_string g))
| _ -> mfail "find_focused_term_in_current_goal: not a squashed equality"
FStar.InteractiveHelpers.PostProcess.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.Propositions.fst.checked FStar.InteractiveHelpers.Output.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Effectful.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.PostProcess.fst
Prims.bool FStar.Reflection.Types.term FStar.InteractiveHelpers.PostProcess.exploration_result Prims.unit FStar.InteractiveHelpers.Base.print_dbg Prims.string Prims.op_Hat FStar.Tactics.V1.Builtins.term_to_string FStar.InteractiveHelpers.PostProcess.__proj__Mkexploration_result__item__res FStar.InteractiveHelpers.Base.mfail FStar.Pervasives.Native.option FStar.InteractiveHelpers.PostProcess.find_focused_term Prims.Nil FStar.Pervasives.Native.tuple2 FStar.InteractiveHelpers.Base.genv FStar.Reflection.V1.Data.term_view FStar.InteractiveHelpers.Base.mk_genv FStar.Reflection.Types.bv FStar.Pervasives.Native.tuple3 FStar.Reflection.Types.typ FStar.InteractiveHelpers.ExploreTerm.typ_or_comp Prims.l_imp Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.InteractiveHelpers.ExploreTerm.uu___is_TC_Comp FStar.Pervasives.Native.__proj__Some__item__v FStar.InteractiveHelpers.ExploreTerm.safe_typ_or_comp FStar.InteractiveHelpers.PostProcess.unsquash_equality FStar.Reflection.Types.env FStar.Tactics.V1.Derived.cur_env FStar.Tactics.V1.Derived.cur_goal
module FStar.InteractiveHelpers.PostProcess

open FStar.List
open FStar.Tactics
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
open FStar.InteractiveHelpers.Propositions
open FStar.InteractiveHelpers.Effectful
open FStar.InteractiveHelpers.Output

let term_eq = FStar.Tactics.term_eq_old

/// The high-level post-processing tactics, used to retrieve some specific
/// information from the context and generate output which can be exploited
/// on the IDE side.

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" 

(*** General utilities *)
/// We declare some identifiers that we will use to guide the meta processing
assume type meta_info
assume val focus_on_term : meta_info

let end_proof () =
  tadmit_t (`())

let unsquash_equality (t:term) : Tac (option (term & term)) =
  begin match term_as_formula t with
  | Comp (Eq _) l r -> Some (l, r)
  | _ -> None
  end

#push-options "--ifuel 2"
let pp_explore (dbg dfs : bool)
               (#a : Type0)
               (f : explorer a)
               (x : a) :
  Tac unit =
  let g = cur_goal () in
  let e = cur_env () in
  print_dbg dbg ("[> pp_explore:\n" ^ term_to_string g);
  begin match unsquash_equality g with
  | Some (l, _) ->
    let c = safe_typ_or_comp dbg e l in
    let ge = mk_genv e [] [] in
    print_dbg dbg ("[> About to explore term:\n" ^ term_to_string l);
    let x = explore_term dbg dfs #a f x ge [] c l in
    end_proof ()
  | _ -> mfail "pp_explore: not a squashed equality"
  end
#pop-options

/// This function goes through the goal, which is presumed to be a squashed equality,
/// and prints all the subterms of its left operand. Very useful for debugging.
val pp_explore_print_goal : unit -> Tac unit
let pp_explore_print_goal () =
  let f : explorer unit =
    fun _ _ _ _ _ -> ((), Continue)
  in
  pp_explore true false f ()

/// Check for meta-identifiers. Note that we can't simply use ``term_eq`` which
/// sometimes unexpectedly fails (maybe because of information hidden to Meta-F*)
val is_focus_on_term : term -> Tac bool
let is_focus_on_term t = is_fvar t (`%focus_on_term)

/// Check if a term is an assertion or an assumption and return its content
/// if it is the case.
val term_is_assert_or_assume : term -> Tac (option term)
let term_is_assert_or_assume t =
  match inspect t with
  | Tv_App hd (a, Q_Explicit) ->
    if is_any_fvar a [`%Prims._assert; `%FStar.Pervasives.assert_norm; `%Prims._assume]
    then Some a
    else None
  | _ -> None

/// Check if the given term view is of the form: 'let _ = focus_on_term in body'
/// Returns 'body' if it is the case.
val is_focused_term : term_view -> Tac (option term)
let is_focused_term tv =
  match tv with
  | Tv_Let recf attrs _ _ def body ->
    if is_focus_on_term def then Some body else None
  | _ -> None

noeq type exploration_result (a : Type)= {
  ge : genv;
  parents : list (genv & term_view);
  tgt_comp : option typ_or_comp;
  res : a;
}

let mk_exploration_result = Mkexploration_result

let pred_explorer (a:Type) = 
  genv -> list (genv & term_view) -> option typ_or_comp -> term_view ->
  Tac (option a)

val find_predicated_term_explorer : #a:Type0 -> pred_explorer a -> bool ->
                                    explorer (option (exploration_result a))
let find_predicated_term_explorer #a pred dbg acc ge pl opt_c t =
  if Some? acc then mfail "find_focused_term_explorer: non empty accumulator";
  if dbg then
    begin
    print ("[> find_focused_term_explorer: " ^ term_view_construct t ^ ":\n" ^ term_to_string t)
    end;
  match pred ge pl opt_c t with
  | Some ft -> Some (mk_exploration_result ge pl opt_c ft), Abort
  | None -> None, Continue

val find_predicated_term : #a:Type0 -> pred_explorer a -> bool -> bool ->
                           genv -> list (genv & term_view) ->
                           option typ_or_comp -> term ->
                           Tac (option (exploration_result a))
let find_predicated_term #a pred dbg dfs ge pl opt_c t =
  fst (explore_term dbg dfs #(option (exploration_result a))
                    (find_predicated_term_explorer #a pred dbg)
                    None ge pl opt_c t)

val _is_focused_term_explorer : pred_explorer term
let _is_focused_term_explorer ge pl opt_c tv =
  is_focused_term tv

val find_focused_term : bool -> bool -> genv -> list (genv & term_view) -> option typ_or_comp -> term ->
                        Tac (option (exploration_result term))
let find_focused_term dbg dfs ge pl opt_c t =
  find_predicated_term #term _is_focused_term_explorer dbg dfs ge pl opt_c t

/// This function raises a MetaAnalysis exception if it can't find a focused term
val find_focused_term_in_current_goal : bool -> Tac (exploration_result term)
dbg: Prims.bool
  -> FStar.Tactics.Effect.Tac
    (FStar.InteractiveHelpers.PostProcess.exploration_result FStar.Reflection.Types.term)