val is_conjunction : term -> Tac (option (term & term))
let is_conjunction t =
  let t = remove_b2t t in
  let hd, params = collect_app t in
  match params with
  | [(x,Q_Explicit);(y,Q_Explicit)] ->
    begin match inspect hd with
    | Tv_FVar fv ->
      let fvn = inspect_fv fv in
      if fvn = and_qn || fvn = ["Prims"; "op_AmpAmp"]
      then Some (x, y) else None
    | _ -> None
    end
  | _ -> None
val is_conjunction : term -> Tac (option (term & term))
let is_conjunction t =
let t = remove_b2t t in
let hd, params = collect_app t in
match params with
| [x, Q_Explicit ; y, Q_Explicit] ->
  (match inspect hd with
    | Tv_FVar fv ->
      let fvn = inspect_fv fv in
      if fvn = and_qn || fvn = ["Prims"; "op_AmpAmp"] then Some (x, y) else None
    | _ -> None)
| _ -> None
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
FStar.Reflection.Types.term Prims.list FStar.Reflection.V1.Data.argv FStar.Reflection.Types.fv Prims.op_BarBar Prims.op_Equality Prims.string FStar.Reflection.Const.and_qn Prims.Cons Prims.Nil FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Reflection.Types.name FStar.Reflection.V1.Builtins.inspect_fv FStar.Reflection.V1.Data.term_view FStar.Tactics.V1.Builtins.inspect FStar.Tactics.V1.SyntaxHelpers.collect_app FStar.InteractiveHelpers.PostProcess.remove_b2t
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)
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

/// This function raises a MetaAnalysis exception if it can't find a focused term
val find_focused_assert_in_current_goal : bool -> Tac (exploration_result term)
let find_focused_assert_in_current_goal dbg =
  print_dbg dbg ("[> find_focused_assert_in_current_goal");
  let res = find_focused_term_in_current_goal dbg in
  print_dbg dbg ("[> Found focused term:\n" ^ term_to_string res.res);
  (* Check that it is an assert or an assume, retrieve the assertion *)
  let res' = 
    match inspect res.res with
    | Tv_Let _ _ bv0 ty fterm _ ->
      let ge' = genv_push_bv res.ge bv0 ty false None in
      ({ res with res = fterm; ge = ge' })
    | _ -> res
  in
  begin match term_is_assert_or_assume res'.res with
  | None -> mfail ("find_focused_assert_in_current_goal: the found focused term is not an assertion or an assumption:" ^ term_to_string res.res)
  | Some tm ->  { res' with res = tm }
  end

(*** Analyze effectful term *)
/// Analyze a term in order to print properly instantiated pre/postconditions
/// and type conditions.

/// with_globals states whether to analyze the target pre/post together with the
/// focused term.
val analyze_effectful_term : 
     dbg:bool
  -> with_gpre:bool
  -> with_gpost:bool
  -> res:exploration_result term
  -> Tac unit

let analyze_effectful_term dbg with_gpre with_gpost res =
  let ge = res.ge in
  let opt_c = res.tgt_comp in
  (* Analyze the effectful term and check whether it is a 'let' or not *)
  let ge1, studied_term, info, ret_bv, shadowed_bv, is_let =
    begin match inspect res.res with
    | Tv_Let _ _ bv0 ty fterm _ ->
      (* Before pushing the binder, check if it shadows another variable.
       * If it is the case, we will need it to correctly output the pre
       * and post-assertions (because for the pre-assertions the variable
       * will not be shadowed yet, while it will be the case for the post-
       * assertions) *)
      print_dbg dbg ("Restraining to: " ^ term_to_string fterm);
      let shadowed_bv : option bv =
        match genv_get_from_name ge (name_of_bv bv0) with
        | None -> None
        | Some (sbv, _) -> Some (fst sbv)
      in
      let ge1 = genv_push_bv ge bv0 ty false None in
      (* If the bv name is "uu___", introduce a fresh variable and use it instead:
       * the underscore might have been introduced when desugaring a let using
       * tuples. If doing that is not necessary, the introduced variable will
       * not appear in the generated assertions anyway. *)
      let ge2, (bv1 : bv) =
        let bvv0 = inspect_bv bv0 in
        let _ = print_dbg dbg ("Variable bound in let: " ^ abv_to_string bv0) in
        if unseal bvv0.bv_ppname = "uu___" (* this is a bit hacky *)
        then genv_push_fresh_bv ge1 "ret" ty
        else ge1, bv0
      in
      let info = compute_eterm_info dbg ge2.env fterm in
      (ge2, fterm, (info <: eterm_info), Some bv1, shadowed_bv, true)
    | _ -> (ge, res.res, compute_eterm_info dbg ge.env res.res, None, None, false)
    end
  in
  print_dbg dbg ("[> Focused term constructor: " ^ term_construct studied_term);
  print_dbg dbg ("[> Environment information (after effect analysis):\n" ^ genv_to_string ge1);
  (* Check if the considered term is an assert, in which case we will only
   * display the precondition (otherwise we introduce too many assertions
   * in the context) *)
  let is_assert = Some? (term_is_assert_or_assume studied_term) in
  (* Instantiate the refinements *)
  (* TODO: use bv rather than term for ret_arg *)
  let ret_arg = opt_tapply (fun x -> pack (Tv_Var x)) ret_bv in
  let parents = List.Tot.map snd res.parents in
  let ge2, asserts =
    eterm_info_to_assertions dbg with_gpre with_gpost ge1 studied_term is_let
                             is_assert info ret_arg opt_c parents [] in
  (* Simplify and filter *)
  let asserts = simp_filter_assertions ge2.env simpl_norm_steps asserts in
  (* Introduce fresh variables for the shadowed ones and substitute *)
  let ge3, asserts = subst_shadowed_with_abs_in_assertions dbg ge2 shadowed_bv asserts in
  (* If not a let, insert all the assertions before the term *)
  let asserts =
    if is_let then asserts
    else mk_assertions (List.Tot.append asserts.pres asserts.posts) []
  in
  (* Print *)
  printout_success ge3 asserts

[@plugin]
val pp_analyze_effectful_term : bool -> bool -> bool -> unit -> Tac unit
let pp_analyze_effectful_term dbg with_gpre with_gpost () =
  try
    let res = find_focused_term_in_current_goal dbg in
    analyze_effectful_term dbg with_gpre with_gpost res;
    end_proof ()
  with | MetaAnalysis msg -> printout_failure msg; end_proof ()
       | err -> (* Shouldn't happen, so transmit the exception for debugging *) raise err

(*** Split conjunctions *)
/// Split an assert made of conjunctions so that there is one assert per
/// conjunction. We try to be a bit smart. For instance, if the assertion is of
/// the form:
/// [> assert(let Construct x1 ... xn = e in A1 /\ ... /\ An);
/// We generate:
/// [> assert(let Construct x1 ... xn = e in A1);
/// [> ...
/// [> assert(let Construct x1 ... xn = e in An);

/// Remove ``b2t`` if it is the head of the term
val remove_b2t : term -> Tac term
let remove_b2t (t:term) : Tac term =
  match inspect t with
  | Tv_App hd (a, Q_Explicit) ->
    begin match inspect hd with
    | Tv_FVar fv ->
      if fv_eq_name fv b2t_qn then a else t
    | _ -> t
    end
  | _ -> t

// TODO: gather all the functions like split_conjunctions, is_eq...
/// Try to destruct a term of the form '_ && _' or '_ /\ _'
val is_conjunction : term -> Tac (option (term & term))
t: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Reflection.Types.term * FStar.Reflection.Types.term))