val compute_pre_type : bool -> env -> term -> Tac pre_post_type
let compute_pre_type dbg e pre =
  print_dbg dbg "[> compute_pre_type";
  match safe_tc e pre with
  | None ->
    print_dbg dbg "safe_tc failed";
    PP_Unknown
  | Some ty ->
    print_dbg dbg "safe_tc succeeded";
    let brs, c = collect_arr_bs ty in
    print_dbg dbg ("num binders: " ^ string_of_int (List.Tot.length brs));
    match brs, is_total_or_gtotal c with
    | [], true ->
      print_dbg dbg "PP_Pure";
      PP_Pure
    | [b], true ->
      print_dbg dbg ("PP_State " ^ (term_to_string (type_of_binder b)));
      PP_State (type_of_binder b)
    | _ ->
      print_dbg dbg "PP_Unknown";
      PP_Unknown
val compute_pre_type : bool -> env -> term -> Tac pre_post_type
let compute_pre_type dbg e pre =
print_dbg dbg "[> compute_pre_type";
match safe_tc e pre with
| None ->
  print_dbg dbg "safe_tc failed";
  PP_Unknown
| Some ty ->
  print_dbg dbg "safe_tc succeeded";
  let brs, c = collect_arr_bs ty in
  print_dbg dbg ("num binders: " ^ string_of_int (List.Tot.length brs));
  match brs, is_total_or_gtotal c with
  | [], true ->
    print_dbg dbg "PP_Pure";
    PP_Pure
  | [b], true ->
    print_dbg dbg ("PP_State " ^ (term_to_string (type_of_binder b)));
    PP_State (type_of_binder b)
  | _ ->
    print_dbg dbg "PP_Unknown";
    PP_Unknown
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
Prims.bool FStar.Reflection.Types.env FStar.Reflection.Types.term FStar.InteractiveHelpers.Effectful.PP_Unknown FStar.InteractiveHelpers.Effectful.pre_post_type Prims.unit FStar.InteractiveHelpers.Base.print_dbg Prims.list FStar.Reflection.Types.binder FStar.Reflection.Types.comp FStar.Pervasives.Native.Mktuple2 FStar.InteractiveHelpers.ExploreTerm.is_total_or_gtotal FStar.InteractiveHelpers.Effectful.PP_Pure FStar.InteractiveHelpers.Effectful.PP_State FStar.Reflection.V1.Derived.type_of_binder Prims.string Prims.op_Hat FStar.Tactics.V1.Builtins.term_to_string FStar.Pervasives.Native.tuple2 Prims.string_of_int FStar.List.Tot.Base.length FStar.Tactics.V1.SyntaxHelpers.collect_arr_bs FStar.Pervasives.Native.option FStar.InteractiveHelpers.ExploreTerm.safe_tc
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

let get_refinement (ty:type_info{Some? ty.refin}) : Tot term =
  Some?.v ty.refin

let get_opt_refinment (ty:type_info) : Tot (option term) =
  ty.refin

let get_rawest_type (ty:type_info) : Tot typ =
  ty.ty

/// Compare the type of a parameter and its expected type
type type_comparison = | Refines | Same_raw_type | Unknown

#push-options "--ifuel 1"
let type_comparison_to_string c =
  match c with
  | Refines -> "Refines"
  | Same_raw_type -> "Same_raw_type"
  | Unknown -> "Unknown"
#pop-options

// TODO: without debugging information generation, is Tot
let compare_types (dbg : bool) (info1 info2 : type_info) :
  Tac (c:type_comparison{c = Same_raw_type ==> has_refinement info2}) =
  print_dbg dbg "[> compare_types";
  if term_eq info1.ty info2.ty then
      let _ = print_dbg dbg "-> types are equal" in
      if has_refinement info2 then
        let _ = print_dbg dbg "-> 2nd type has refinement" in
        // This doesn't work like in C: we need to check if info1 has a
        // refinement, then we can compare the refinements inside ANOTHER if
        if has_refinement info1 then
          let _ = print_dbg dbg "-> 1st type has refinement" in
          if term_eq (get_refinement info1) (get_refinement info2) then
            let _ = print_dbg dbg "-> Refines" in
            Refines
          else
          let _ = print_dbg dbg "-> Same_raw_type" in
          Same_raw_type // Same raw type but can't say anything about the expected refinement
        else
          let _ = print_dbg dbg "-> 1st type has no refinement" in
          let _ = print_dbg dbg "-> Same_raw_type" in
          Same_raw_type // Same raw type but can't say anything about the expected refinement
      else
        let _ = print_dbg dbg "-> 2nd type has no refinement: Refines" in
        Refines // The first type is more precise than the second type
    else
      let _ = print_dbg dbg "types are not equal" in
      Unknown

let compare_cast_types (dbg : bool) (p:cast_info) :
  Tac (c:type_comparison{
    ((c = Refines \/ c = Same_raw_type) ==> (Some? p.p_ty /\ Some? p.exp_ty)) /\
    (c = Same_raw_type ==> has_refinement (Some?.v p.exp_ty))}) =
  print_dbg dbg "[> compare_cast_types";
  match p.p_ty, p.exp_ty with
  | Some info1, Some info2 ->
    compare_types dbg info1 info2
  | _ -> Unknown

(*/// Retrieve the list of types from the parameters stored in ``typ_or_comp``.
val typ_or_comp_to_param_types : typ_or_comp -> Tot (list typ)

let typ_or_comp_to_param_types c =
  let pl = params_of_typ_or_comp c in
  List.Tot.map type_of_binder pl *)

(**** Step 2 *)
/// The retrieved type refinements and post-conditions are not instantiated (they
/// are lambda functions): instantiate them to get propositions.


/// Generate a term of the form [has_type x ty]
val mk_has_type : term -> typ -> Tac term
let mk_has_type t ty =
  let params = [(ty, Q_Implicit); (t, Q_Explicit); (ty, Q_Explicit)] in
  mk_app (`has_type) params  


// TODO: I don't understand why I need ifuel 2 here
#push-options "--ifuel 2"
/// Generate the propositions equivalent to a correct type cast.
/// Note that the type refinements need to be instantiated.
val cast_info_to_propositions : bool -> genv -> cast_info -> Tac (list proposition)
let cast_info_to_propositions dbg ge ci =
  print_dbg dbg ("[> cast_info_to_propositions:\n" ^ cast_info_to_string ci);
  match compare_cast_types dbg ci with
  | Refines -> 
    print_dbg dbg ("-> Comparison result: Refines");
    []
  | Same_raw_type ->
    print_dbg dbg ("-> Comparison result: Same_raw_type");
    let refin = get_refinement (Some?.v ci.exp_ty) in
    let inst_refin = mk_app_norm ge.env refin [ci.term] in
    [inst_refin]
  | Unknown ->
    print_dbg dbg ("-> Comparison result: Unknown");
    match ci.p_ty, ci.exp_ty with
    | Some p_ty, Some e_ty ->
      let p_rty = get_rawest_type p_ty in
      let e_rty = get_rawest_type e_ty in
      (* For the type cast, we generate an assertion of the form:
       * [> has_type (p <: type_of_p) expected_type
       * The reason is that we want the user to know which parameter is
       * concerned (hence the ``has_type``), and which types should be
       * related (hence the ascription).
       *)
      let ascr_term = pack (Tv_AscribedT ci.term p_rty None false) in
      let has_type_params = [(p_rty, Q_Implicit); (ascr_term, Q_Explicit); (e_rty, Q_Explicit)] in
      let type_cast = mk_app (`has_type) has_type_params in
      (* Expected type's refinement *)
      let inst_opt_refin = opt_mk_app_norm ge.env e_ty.refin [ci.term] in
      opt_cons inst_opt_refin [type_cast]
    | _ -> []
#pop-options

/// Generates a list of propositions from a list of ``cast_info``. Note that
/// the user should revert the list before printing the propositions.
val cast_info_list_to_propositions : bool -> genv -> list cast_info -> Tac (list proposition)
let cast_info_list_to_propositions dbg ge ls =
  let lsl = map (cast_info_to_propositions dbg ge) ls in
  flatten lsl

/// When dealing with unknown effects, we try to guess what the pre and post-conditions
/// are. The effects are indeed very likely to have a pre and a post-condition,
/// and to be parameterized with an internal effect state, so that the pre and posts
/// have the following shapes:
/// - pre  : STATE -> Type0
/// - post : STATE -> RET -> STATE -> Type0
/// Or (no state/pure):
/// - pre  : Type0
/// - post : RET -> Type0
/// We try to detect that with the following functions:
noeq type pre_post_type =
| PP_Unknown | PP_Pure
| PP_State : (state_type:term) -> pre_post_type

val compute_pre_type : bool -> env -> term -> Tac pre_post_type
val compute_pre_type : bool -> env -> term -> Tac pre_post_type
dbg: Prims.bool -> e: FStar.Reflection.Types.env -> pre: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac FStar.InteractiveHelpers.Effectful.pre_post_type