val formula_construct (f: formula) : Tac string
let formula_construct (f : formula) : Tac string =
  match f with
  | True_       -> "True_"
  | False_      -> "False_"
  | Comp _ _ _  -> "Comp"
  | And _ _     -> "And"
  | Or _ _      -> "Or"
  | Not _       -> "Not"
  | Implies _ _ -> "Implies"
  | Iff _ _     -> "Iff"
  | Forall _ _ _ -> "Forall"
  | Exists _ _ _ -> "Exists"
  | App _ _     -> "Apply"
  | Name _      -> "Name"
  | FV _        -> "FV"
  | IntLit _    -> "IntLit"
  | F_Unknown   -> "F_Unknown"
val formula_construct (f: formula) : Tac string
let formula_construct (f: formula) : Tac string =
match f with
| True_ -> "True_"
| False_ -> "False_"
| Comp _ _ _ -> "Comp"
| And _ _ -> "And"
| Or _ _ -> "Or"
| Not _ -> "Not"
| Implies _ _ -> "Implies"
| Iff _ _ -> "Iff"
| Forall _ _ _ -> "Forall"
| Exists _ _ _ -> "Exists"
| App _ _ -> "Apply"
| Name _ -> "Name"
| FV _ -> "FV"
| IntLit _ -> "IntLit"
| F_Unknown -> "F_Unknown"
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.V1.Formula.formula FStar.Reflection.V1.Formula.comparison FStar.Reflection.Types.term FStar.Reflection.Types.bv FStar.Reflection.Types.typ FStar.Reflection.Types.fv Prims.int Prims.string
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))
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 split_conjunctions : term -> Tac (list term)

let rec _split_conjunctions (ls : list term) (t : term) : Tac (list term) =
  match is_conjunction t with
  | None -> t :: ls
  | Some (l, r) ->
    let ls1 = _split_conjunctions ls r in
    let ls2 = _split_conjunctions ls1 l in
    ls2

let split_conjunctions t =
  _split_conjunctions [] t

/// Split a term of the form:
/// [> let Constuct x1 ... xn = x in A1 /\ ... /\ Am
/// into m terms:
/// [> let Constuct x1 ... xn = x in A1
/// ...
/// [> let Constuct x1 ... xn = x in Am
val split_conjunctions_under_match : bool -> term -> Tac (list term)

let split_conjunctions_under_match dbg t =
  let t1 = remove_b2t t in
  print_dbg dbg ("[> split_conjunctions_under_match: " ^ term_construct t1);
  match inspect t1 with
  | Tv_Match scrut ret_opt [(pat, br)] ->
    let tl = split_conjunctions br in
    map (fun x -> pack (Tv_Match scrut ret_opt [(pat, x)])) tl
  | _ ->
    (* Not of the proper shape: return the original term *)
    [t]

val split_assert_conjs : bool -> exploration_result term -> Tac unit
let split_assert_conjs dbg res =
  let ge0 = res.ge in
  (* Simplify the term (it may be an abstraction applied to some parameters) *)
  let t = norm_term_env ge0.env simpl_norm_steps res.res in
  (* Split the conjunctions *)
  let conjs = split_conjunctions t in
  (* If there is only one conjunction, check if it is of the following form
   * and try to split:
   * [> let Construct x1 .. xn = x in A1 /\ ... /\ Am
   *)
  let conjs =
    if List.length conjs = 1 then split_conjunctions_under_match dbg t
    else conjs
  in
  let asserts = mk_assertions conjs [] in
  (* Print *)
  printout_success ge0 asserts

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

(*** Term unfolding in assert *)
/// Unfold/rewrite a term in an assert.
/// If the term is a (recursive) top-level identifier, unfold it.
/// Otherwise look for an equality or a pure let-binding to replace it with.
/// If the assert is an equality, unfold/rewrite only on the side chosen by the user.

// TODO: use "kind" keyword rather than type above
/// An equality kind
noeq type eq_kind =
  | Eq_Dec    : typ -> eq_kind          (* =   *)
  | Eq_Undec  : typ -> eq_kind          (* ==  *)
  | Eq_Hetero : typ -> typ -> eq_kind   (* === *)

/// Deconstruct an equality
// We use our own construct because ``term_as_formula`` doesn't always work
// TODO: update ``term_as_formula``
val is_eq : bool -> term -> Tac (option (eq_kind & term & term))
let is_eq dbg t =
  let t = remove_b2t t in
  print_dbg dbg ("[> is_eq: " ^ term_to_string t);
  let hd, params = collect_app t in
  print_dbg dbg ("- hd:\n" ^ term_to_string hd);
  print_dbg dbg ("- parameters:\n" ^ list_to_string (fun (x, y) -> term_to_string x) params);
  match inspect hd with
  | Tv_FVar fv ->
    begin match params with
    | [(a,Q_Implicit);(x,Q_Explicit);(y,Q_Explicit)] ->
      if is_any_fvar a [`%Prims.op_Equality; `%Prims.equals; "Prims.op_Equals"] then
        Some ((Eq_Dec a), x, y)
      else if is_any_fvar a [`%Prims.eq2; "Prims.op_Equals_Equals"] then
        Some ((Eq_Undec a), x, y)
      else None
    | [(a,Q_Implicit);(b,Q_Implicit);(x,Q_Explicit);(y,Q_Explicit)] ->
      if is_fvar a (`%Prims.op_Equals_Equals_Equals) then
        Some ((Eq_Hetero a b), x, y)
      else None
    | _ -> None
    end
  | _ -> None

/// Reconstruct an equality
val mk_eq : eq_kind -> term -> term -> Tot term
let mk_eq k t1 t2 =
  match k with
  | Eq_Dec ty ->
    mk_app (`Prims.op_Equality) [(ty, Q_Implicit); (t1, Q_Explicit); (t2, Q_Explicit)]
  | Eq_Undec ty ->
    mk_app (`Prims.eq2) [(ty, Q_Implicit); (t1, Q_Explicit); (t2, Q_Explicit)]
  | Eq_Hetero ty1 ty2 ->
    mk_app Prims.(`( === )) [(ty1, Q_Implicit); (ty2, Q_Implicit);
                             (t1, Q_Explicit); (t2, Q_Explicit)]
val formula_construct (f: formula) : Tac string
f: FStar.Reflection.V1.Formula.formula -> FStar.Tactics.Effect.Tac Prims.string