let mk_effect_info = Mkeffect_info
let mk_effect_info =
Mkeffect_info
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.Effectful.Mkeffect_info
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;
}
val mk_effect_info : ei_type: FStar.InteractiveHelpers.ExploreTerm.effect_type ->
    ei_ret_type: FStar.InteractiveHelpers.ExploreTerm.type_info ->
    ei_pre: FStar.Pervasives.Native.option FStar.Reflection.Types.term ->
    ei_post: FStar.Pervasives.Native.option FStar.Reflection.Types.term
  -> FStar.InteractiveHelpers.Effectful.effect_info

    ei_type: FStar.InteractiveHelpers.ExploreTerm.effect_type ->
    ei_ret_type: FStar.InteractiveHelpers.ExploreTerm.type_info ->
    ei_pre: FStar.Pervasives.Native.option FStar.Reflection.Types.term ->
    ei_post: FStar.Pervasives.Native.option FStar.Reflection.Types.term
  -> FStar.InteractiveHelpers.Effectful.effect_info