val get_refinement (ty: type_info{Some? ty.refin}) : Tot term
let get_refinement (ty:type_info{Some? ty.refin}) : Tot term =
  Some?.v ty.refin
val get_refinement (ty: type_info{Some? ty.refin}) : Tot term
let get_refinement (ty: type_info{Some? ty.refin}) : Tot term =
Some?.v ty.refin
FStar.InteractiveHelpers.Effectful.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.ExploreTerm.fst.checked FStar.InteractiveHelpers.Base.fst.checked FStar.HyperStack.fst.checked
FStar.InteractiveHelpers.Effectful.fst
FStar.InteractiveHelpers.ExploreTerm.type_info Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.Reflection.Types.term FStar.InteractiveHelpers.ExploreTerm.__proj__Mktype_info__item__refin FStar.Pervasives.Native.__proj__Some__item__v
module FStar.InteractiveHelpers.Effectful

module HS = FStar.HyperStack

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

let term_eq = FStar.Tactics.term_eq_old

/// Effectful term analysis: retrieve information about an effectful term, including
/// its return type, its arguments, its correctly instantiated pre/postcondition, etc.

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


(*** Effectful term analysis *)
/// Cast information
noeq type cast_info = {
  term : term;
  p_ty : option type_info; // The type of the term
  exp_ty : option type_info; // The type of the expected parameter
}

let mk_cast_info t p_ty exp_ty : cast_info =
  Mkcast_info t p_ty exp_ty

val cast_info_to_string : cast_info -> Tac string
let cast_info_to_string info =
  "Mkcast_info (" ^ term_to_string info.term ^ ") (" ^
  option_to_string type_info_to_string info.p_ty ^ ") (" ^
  option_to_string type_info_to_string info.exp_ty ^ ")"

/// Extracts the effectful information from a computation
noeq type effect_info = {
  ei_type : effect_type;
  ei_ret_type : type_info;
  ei_pre : option term;
  ei_post : option term;
}

let mk_effect_info = Mkeffect_info

/// Convert a ``typ_or_comp`` to cast information
val effect_info_to_string : effect_info -> Tac string
let effect_info_to_string c =
  "Mkeffect_info " ^
  effect_type_to_string c.ei_type ^ " (" ^
  option_to_string term_to_string c.ei_pre ^ ") (" ^
  type_info_to_string c.ei_ret_type ^ ") (" ^
  option_to_string term_to_string c.ei_post ^ ")"

/// Effectful term information
noeq type eterm_info = {
  einfo : effect_info;
  (* Head and parameters of the decomposition of the term into a function application *)
  head : term;
  parameters : list cast_info;
}

val eterm_info_to_string : eterm_info -> Tac string
let eterm_info_to_string info =
  let params = map (fun x -> "(" ^ cast_info_to_string x ^ ");  \n") info.parameters in
  let params_str = List.Tot.fold_left (fun x y -> x ^ y) "" params in
  "Mketerm_info (" ^
  effect_info_to_string info.einfo ^ ") (" ^
  term_to_string info.head ^ ")\n[" ^
  params_str ^ "]"

let mk_eterm_info = Mketerm_info


(**** Step 1 *)
/// Decompose a function application between its body and parameters
val decompose_application : env -> term -> Tac (term & list cast_info)

#push-options "--ifuel 1"
let rec decompose_application_aux (e : env) (t : term) :
  Tac (term & list cast_info) =
  match inspect t with
  | Tv_App hd (a, qualif) ->
    let hd0, params = decompose_application_aux e hd in
    (* Parameter type *)
    let a_type = get_type_info e a in
    (* Type expected by the function *)
    let hd_ty = safe_tc e hd in
    let param_type =
      match hd_ty with
      | None -> None
      | Some hd_ty' ->
        match inspect hd_ty' with
        | Tv_Arrow b c ->
          Some (get_type_info_from_type (binder_sort b))
        | _ -> None
    in
    let cast_info = mk_cast_info a a_type param_type in
    hd0, cast_info :: params
  | _ -> t, []
#pop-options

let decompose_application e t =
  let hd, params = decompose_application_aux e t in
  hd, List.Tot.rev params

/// Computes an effect type, its return type and its (optional) pre and post
val comp_view_to_effect_info : dbg:bool -> comp_view -> Tac (option effect_info)

let comp_view_to_effect_info dbg cv =
  match cv with
  | C_Total ret_ty ->
    let ret_type_info = get_type_info_from_type ret_ty in
    Some (mk_effect_info E_Total ret_type_info None None)
  | C_GTotal ret_ty ->
    let ret_type_info = get_type_info_from_type ret_ty in
    Some (mk_effect_info E_Total ret_type_info None None)
  | C_Lemma pre post patterns ->
    (* We use unit as the return type information *)
    let pre = prettify_term dbg pre in
    let post = prettify_term dbg post in
    Some (mk_effect_info E_Lemma unit_type_info (Some pre) (Some post))
  | C_Eff univs eff_name ret_ty eff_args _ ->
    print_dbg dbg ("comp_view_to_effect_info: C_Eff " ^ flatten_name eff_name);
    let ret_type_info = get_type_info_from_type ret_ty in
    let etype = effect_name_to_type eff_name in
    let mk_res = mk_effect_info etype ret_type_info in
    let eff_args = map (fun (x,a) -> (prettify_term dbg x, a)) eff_args in
    begin match etype, eff_args with
    | E_PURE, [(pre, _)] -> Some (mk_res (Some pre) None)
    | E_Pure, [(pre, _); (post, _)]
    | E_Stack, [(pre, _); (post, _)]
    | E_ST, [(pre, _); (post, _)] -> Some (mk_res (Some pre) (Some post))
    (* If the effect is unknown and there are two parameters or less, we make the
     * guess that the first one is a pre-condition and the second one is a
     * post-condition *)
    | E_Unknown, [] -> Some (mk_res None None)
    | E_Unknown, [(pre, _)] -> Some (mk_res (Some pre) None)
    | E_Unknown, [(pre, _); (post, _)] -> Some (mk_res (Some pre) (Some post))
    | _ -> None
    end

val comp_to_effect_info : dbg:bool -> comp -> Tac (option effect_info)

let comp_to_effect_info dbg c =
  let cv : comp_view = inspect_comp c in
  comp_view_to_effect_info dbg cv

val compute_effect_info : dbg:bool -> env -> term -> Tac (option effect_info)

let compute_effect_info dbg e tm =
  match safe_tcc e tm with
  | Some c -> comp_to_effect_info dbg c
  | None -> None

/// Converts a ``typ_or_comp`` to an ``effect_info`` by flushing the instantiations
/// stored in the ``typ_or_comp``.
let typ_or_comp_to_effect_info (dbg : bool) (ge : genv) (c : typ_or_comp) :
  Tac effect_info =
(*  match c with
  | TC_Typ ty pl num_unflushed ->
    let tinfo = get_type_info_from_type ty in
    mk_effect_info E_Total tinfo None None
  | TC_Comp cv pl num_unflushed ->
    let opt_einfo = comp_to_effect_info dbg cv in
    match opt_einfo with
    | None -> mfail ("typ_or_comp_to_effect_info failed on: " ^ acomp_to_string cv)
    | Some einfo -> einfo *)
  let c = flush_typ_or_comp dbg ge.env c in
  match c with
  | TC_Typ ty _ _ ->
    let tinfo = get_type_info_from_type ty in
    mk_effect_info E_Total tinfo None None
  | TC_Comp cv _ _ ->
    let opt_einfo = comp_to_effect_info dbg cv in
    match opt_einfo with
    | None -> mfail ("typ_or_comp_to_effect_info failed on: " ^ acomp_to_string cv)
    | Some einfo -> einfo


/// ``tcc`` often returns a lifted effect which is not what we want (ex.: a
/// lemma called inside a Stack function may have been lifted to Stack, but
/// when studying this term effect, we want to retrieve its non-lifted effect).
/// The workaround is to decompose the term if it is an application, then retrieve
/// the effect of the head, and reconstruct it.
/// Note: I tried inspecting then repacking the term before calling ``tcc`` to
/// see if it allows to "forget" the context: it doesn't work.
val tcc_no_lift : env -> term -> Tac comp

let tcc_no_lift e t =
  match inspect t with
  | Tv_App _ _ ->
    let hd, args = collect_app t in
    let c = tcc e hd in
    inst_comp e c (List.Tot.map fst args)
  | _ ->
    (* Fall back to ``tcc`` *)
    tcc e t

/// Returns the effectful information about a term
val compute_eterm_info : dbg:bool -> env -> term -> Tac eterm_info

#push-options "--ifuel 2"
let compute_eterm_info (dbg : bool) (e : env) (t : term) =
  (* Decompose the term if it is a function application *)
  let hd, parameters = decompose_application e t in
  try
    begin
    let c : comp = tcc_no_lift e t in
    let opt_einfo = comp_to_effect_info dbg c in
    match opt_einfo with
    | None -> mfail ("compute_eterm_info: failed on: " ^ term_to_string t)
    | Some einfo ->
      mk_eterm_info einfo hd parameters
    end
  with
  | TacticFailure msg ->
    mfail ("compute_eterm_info: failure: '" ^ msg ^ "'")
  | e -> raise e
#pop-options

(***** Types, casts and refinements *)

(* TODO: those are not needed anymore *)
let has_refinement (ty:type_info) : Tot bool =
  Some? ty.refin
val get_refinement (ty: type_info{Some? ty.refin}) : Tot term
ty: FStar.InteractiveHelpers.ExploreTerm.type_info{Some? (Mktype_info?.refin ty)}
  -> FStar.Reflection.Types.term