fstar 2022.01.15 · OCaml Package

type cast_info = {

term : FStar_Reflection_Types.term;
p_ty : FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option;
exp_ty : FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option;

}

val __proj__Mkcast_info__item__term : cast_info -> FStar_Reflection_Types.term

val __proj__Mkcast_info__item__p_ty : 
  cast_info ->
  FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option

val __proj__Mkcast_info__item__exp_ty : 
  cast_info ->
  FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option

val mk_cast_info : 
  FStar_Reflection_Types.term ->
  FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option ->
  FStar_InteractiveHelpers_ExploreTerm.type_info FStar_Pervasives_Native.option ->
  cast_info

val cast_info_to_string : cast_info -> Prims.string

type effect_info = {

ei_type : FStar_InteractiveHelpers_ExploreTerm.effect_type;
ei_ret_type : FStar_InteractiveHelpers_ExploreTerm.type_info;
ei_pre : FStar_Reflection_Types.term FStar_Pervasives_Native.option;
ei_post : FStar_Reflection_Types.term FStar_Pervasives_Native.option;

}

val __proj__Mkeffect_info__item__ei_type : 
  effect_info ->
  FStar_InteractiveHelpers_ExploreTerm.effect_type

val __proj__Mkeffect_info__item__ei_ret_type : 
  effect_info ->
  FStar_InteractiveHelpers_ExploreTerm.type_info

val __proj__Mkeffect_info__item__ei_pre : 
  effect_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option

val __proj__Mkeffect_info__item__ei_post : 
  effect_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option

val mk_effect_info : 
  FStar_InteractiveHelpers_ExploreTerm.effect_type ->
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  effect_info

val effect_info_to_string : effect_info -> Prims.string

type eterm_info = {

einfo : effect_info;
head : FStar_Reflection_Types.term;
parameters : cast_info Prims.list;

}

val __proj__Mketerm_info__item__einfo : eterm_info -> effect_info

val __proj__Mketerm_info__item__head : 
  eterm_info ->
  FStar_Reflection_Types.term

val __proj__Mketerm_info__item__parameters : eterm_info -> cast_info Prims.list

val eterm_info_to_string : eterm_info -> Prims.string

val mk_eterm_info : 
  effect_info ->
  FStar_Reflection_Types.term ->
  cast_info Prims.list ->
  eterm_info

val decompose_application_aux : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term * cast_info Prims.list)
    FStar_Tactics_Result.__result

val decompose_application : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term * cast_info Prims.list)
    FStar_Tactics_Result.__result

val comp_view_to_effect_info : 
  Prims.bool ->
  FStar_Reflection_Data.comp_view ->
  FStar_Tactics_Types.proofstate ->
  effect_info FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val comp_to_effect_info : 
  Prims.bool ->
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  effect_info FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val compute_effect_info : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  effect_info FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val typ_or_comp_to_effect_info : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_InteractiveHelpers_ExploreTerm.typ_or_comp ->
  FStar_Tactics_Types.proofstate ->
  effect_info FStar_Tactics_Result.__result

val tcc_no_lift : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val compute_eterm_info : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  eterm_info FStar_Tactics_Result.__result

val has_refinement : 
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  Prims.bool

val get_refinement : 
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Reflection_Types.term

val get_opt_refinment : 
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option

val get_rawest_type : 
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Reflection_Types.typ

type type_comparison =

| Refines
| Same_raw_type
| Unknown

val uu___is_Refines : type_comparison -> Prims.bool

val uu___is_Same_raw_type : type_comparison -> Prims.bool

val uu___is_Unknown : type_comparison -> Prims.bool

val type_comparison_to_string : type_comparison -> Prims.string

val compare_types : 
  Prims.bool ->
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Tactics_Types.proofstate ->
  type_comparison FStar_Tactics_Result.__result

val compare_cast_types : 
  Prims.bool ->
  cast_info ->
  FStar_Tactics_Types.proofstate ->
  type_comparison FStar_Tactics_Result.__result

val mk_has_type : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val cast_info_to_propositions : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  cast_info ->
  FStar_Tactics_Types.proofstate ->
  FStar_InteractiveHelpers_Propositions.proposition Prims.list
    FStar_Tactics_Result.__result

val cast_info_list_to_propositions : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  cast_info Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_InteractiveHelpers_Propositions.proposition Prims.list
    FStar_Tactics_Result.__result

type pre_post_type =

| PP_Unknown
| PP_Pure
| PP_State of FStar_Reflection_Types.term

val uu___is_PP_Unknown : pre_post_type -> Prims.bool

val uu___is_PP_Pure : pre_post_type -> Prims.bool

val uu___is_PP_State : pre_post_type -> Prims.bool

val __proj__PP_State__item__state_type : 
  pre_post_type ->
  FStar_Reflection_Types.term

val compute_pre_type : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  pre_post_type FStar_Tactics_Result.__result

val opt_remove_refin : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.typ FStar_Tactics_Result.__result

val compute_post_type : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  pre_post_type FStar_Tactics_Result.__result

val check_pre_post_type : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  pre_post_type FStar_Tactics_Result.__result

val check_opt_pre_post_type : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  pre_post_type FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val _introduce_variables_for_abs : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term Prims.list
   * FStar_Reflection_Types.binder Prims.list
   * FStar_InteractiveHelpers_Base.genv)
    FStar_Tactics_Result.__result

val introduce_variables_for_abs : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term Prims.list
   * FStar_Reflection_Types.binder Prims.list
   * FStar_InteractiveHelpers_Base.genv)
    FStar_Tactics_Result.__result

val introduce_variables_for_opt_abs : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term Prims.list
   * FStar_Reflection_Types.binder Prims.list
   * FStar_InteractiveHelpers_Base.genv)
    FStar_Tactics_Result.__result

val effect_type_is_stateful : 
  FStar_InteractiveHelpers_ExploreTerm.effect_type ->
  Prims.bool

val is_st_get : 
  Prims.bool ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val is_let_st_get : 
  Prims.bool ->
  FStar_Reflection_Data.term_view ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val term_has_effectful_comp : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val related_term_is_effectul : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Data.term_view ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val find_mem_in_related : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Data.term_view Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val find_mem_in_children : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (FStar_InteractiveHelpers_Base.genv
   * FStar_Reflection_Types.bv FStar_Pervasives_Native.option)
    FStar_Tactics_Result.__result

val pre_post_to_propositions : 
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_InteractiveHelpers_ExploreTerm.effect_type ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.binder FStar_Pervasives_Native.option ->
  FStar_InteractiveHelpers_ExploreTerm.type_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Reflection_Data.term_view Prims.list ->
  FStar_Reflection_Data.term_view Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (FStar_InteractiveHelpers_Base.genv
   * FStar_InteractiveHelpers_Propositions.proposition
       FStar_Pervasives_Native.option
   * FStar_InteractiveHelpers_Propositions.proposition
       FStar_Pervasives_Native.option)
    FStar_Tactics_Result.__result

val eterm_info_to_assertions : 
  Prims.bool ->
  Prims.bool ->
  Prims.bool ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  Prims.bool ->
  Prims.bool ->
  eterm_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_InteractiveHelpers_ExploreTerm.typ_or_comp
    FStar_Pervasives_Native.option ->
  FStar_Reflection_Data.term_view Prims.list ->
  FStar_Reflection_Data.term_view Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (FStar_InteractiveHelpers_Base.genv
   * FStar_InteractiveHelpers_Propositions.assertions)
    FStar_Tactics_Result.__result