sig
  type session
  type file
  type theory
  type proofNodeID
  val print_proofNodeID :
    Stdlib.Format.formatter -> Session_itp.proofNodeID -> unit
  type transID
  type proofAttemptID
  val print_proofAttemptID :
    Stdlib.Format.formatter -> Session_itp.proofAttemptID -> unit
  type fileID
  module Hfile :
    sig
      type key = fileID
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Hpn :
    sig
      type key = proofNodeID
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Htn :
    sig
      type key = transID
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Hpan :
    sig
      type key = proofAttemptID
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  type any =
      AFile of Session_itp.file
    | ATh of Session_itp.theory
    | ATn of Session_itp.transID
    | APn of Session_itp.proofNodeID
    | APa of Session_itp.proofAttemptID
  val fprintf_any : Stdlib.Format.formatter -> Session_itp.any -> unit
  type notifier = Session_itp.any -> unit
  val get_files : Session_itp.session -> Session_itp.file Session_itp.Hfile.t
  val get_dir : Session_itp.session -> string
  val file_id : Session_itp.file -> Session_itp.fileID
  val file_path : Session_itp.file -> Sysutil.file_path
  val file_format : Session_itp.file -> string
  val file_theories : Session_itp.file -> Session_itp.theory list
  val system_path : Session_itp.session -> Session_itp.file -> string
  val theory_name : Session_itp.theory -> Ident.ident
  val theory_goals : Session_itp.theory -> Session_itp.proofNodeID list
  val theory_parent :
    Session_itp.session -> Session_itp.theory -> Session_itp.file
  type proof_attempt_node = private {
    parent : Session_itp.proofNodeID;
    mutable prover : Whyconf.prover;
    limits : Call_provers.resource_limits;
    mutable proof_state : Call_provers.prover_result option;
    mutable proof_obsolete : bool;
    mutable proof_script : Sysutil.file_path option;
  }
  val set_proof_script :
    Session_itp.proof_attempt_node -> Sysutil.file_path -> unit
  val is_below :
    Session_itp.session -> Session_itp.any -> Session_itp.any -> bool
  type proof_parent =
      Trans of Session_itp.transID
    | Theory of Session_itp.theory
  val get_task : Session_itp.session -> Session_itp.proofNodeID -> Task.task
  val get_task_name_table :
    Session_itp.session ->
    Session_itp.proofNodeID -> Task.task * Trans.naming_table
  val get_transformations :
    Session_itp.session ->
    Session_itp.proofNodeID -> Session_itp.transID list
  val get_proof_attempt_ids :
    Session_itp.session ->
    Session_itp.proofNodeID -> Session_itp.proofAttemptID Whyconf.Hprover.t
  exception BadID
  val get_proof_attempt_node :
    Session_itp.session ->
    Session_itp.proofAttemptID -> Session_itp.proof_attempt_node
  val get_proof_attempt_parent :
    Session_itp.session ->
    Session_itp.proofAttemptID -> Session_itp.proofNodeID
  val get_proof_attempts :
    Session_itp.session ->
    Session_itp.proofNodeID -> Session_itp.proof_attempt_node list
  val get_sub_tasks :
    Session_itp.session ->
    Session_itp.transID -> Session_itp.proofNodeID list
  val get_transf_args :
    Session_itp.session -> Session_itp.transID -> string list
  val get_transf_name : Session_itp.session -> Session_itp.transID -> string
  val get_proof_name :
    Session_itp.session -> Session_itp.proofNodeID -> Ident.ident
  val get_proof_expl :
    Session_itp.session -> Session_itp.proofNodeID -> string
  val get_proof_parent :
    Session_itp.session ->
    Session_itp.proofNodeID -> Session_itp.proof_parent
  val get_trans_parent :
    Session_itp.session -> Session_itp.transID -> Session_itp.proofNodeID
  val find_th :
    Session_itp.session -> Session_itp.proofNodeID -> Session_itp.theory
  val get_any_parent :
    Session_itp.session -> Session_itp.any -> Session_itp.any option
  val is_detached : Session_itp.session -> Session_itp.any -> bool
  val get_encapsulating_theory :
    Session_itp.session -> Session_itp.any -> Session_itp.theory
  val get_encapsulating_file :
    Session_itp.session -> Session_itp.any -> Session_itp.file
  val is_fatal : exn -> bool
  val goal_iter_proof_attempt :
    Session_itp.session ->
    (Session_itp.proofAttemptID -> Session_itp.proof_attempt_node -> unit) ->
    Session_itp.proofNodeID -> unit
  val theory_iter_proof_attempt :
    Session_itp.session ->
    (Session_itp.proofAttemptID -> Session_itp.proof_attempt_node -> unit) ->
    Session_itp.theory -> unit
  val file_iter_proof_attempt :
    Session_itp.session ->
    (Session_itp.proofAttemptID -> Session_itp.proof_attempt_node -> unit) ->
    Session_itp.file -> unit
  val any_iter_proof_attempt :
    Session_itp.session ->
    (Session_itp.proofAttemptID -> Session_itp.proof_attempt_node -> unit) ->
    Session_itp.any -> unit
  val session_iter_proof_attempt :
    (Session_itp.proofAttemptID -> Session_itp.proof_attempt_node -> unit) ->
    Session_itp.session -> unit
  val session_iter_proof_node_id :
    (Session_itp.proofNodeID -> unit) -> Session_itp.session -> unit
  val fold_all_any :
    Session_itp.session ->
    ('a -> Session_itp.any -> 'a) -> 'a -> Session_itp.any -> 'a
  val fold_all_session :
    Session_itp.session -> ('a -> Session_itp.any -> 'a) -> 'a -> 'a
  val empty_session :
    ?sum_shape_version:Termcode.sum_shape_version ->
    ?from:Session_itp.session -> string -> Session_itp.session
  val add_file_section :
    Session_itp.session ->
    Sysutil.file_path ->
    file_is_detached:bool ->
    Theory.theory list -> Env.fformat -> Session_itp.file
  val read_file :
    Env.env ->
    ?format:Env.fformat -> string -> Theory.theory list * Env.fformat
  val merge_files :
    ignore_shapes:bool ->
    Env.env ->
    Session_itp.session -> Session_itp.session -> exn list * bool * bool
  val merge_files_gen :
    ignore_shapes:bool ->
    reparse_file_fun:(Session_itp.session ->
                      Env.env -> Session_itp.file -> Theory.theory list) ->
    Env.env ->
    Session_itp.session -> Session_itp.session -> exn list * bool * bool
  val graft_proof_attempt :
    ?file:Sysutil.file_path ->
    Session_itp.session ->
    Session_itp.proofNodeID ->
    Whyconf.prover ->
    limits:Call_provers.resource_limits -> Session_itp.proofAttemptID
  exception NoProgress
  val apply_trans_to_goal :
    allow_no_effect:bool ->
    Session_itp.session ->
    Env.env ->
    string -> string list -> Session_itp.proofNodeID -> Task.task list
  val graft_transf :
    Session_itp.session ->
    Session_itp.proofNodeID ->
    string -> string list -> Task.task list -> Session_itp.transID
  val remove_proof_attempt :
    Session_itp.session -> Session_itp.proofNodeID -> Whyconf.prover -> unit
  val remove_transformation :
    Session_itp.session -> Session_itp.transID -> unit
  val mark_obsolete :
    Session_itp.session -> Session_itp.proofAttemptID -> unit
  val save_session : Session_itp.session -> unit
  val export_as_zip : Session_itp.session -> string
  val load_session : string -> Session_itp.session
  exception RemoveError
  val remove_subtree :
    notification:Session_itp.notifier ->
    removed:Session_itp.notifier ->
    Session_itp.session -> Session_itp.any -> unit
  val pa_proved : Session_itp.session -> Session_itp.proofAttemptID -> bool
  val th_proved : Session_itp.session -> Session_itp.theory -> bool
  val pn_proved : Session_itp.session -> Session_itp.proofNodeID -> bool
  val tn_proved : Session_itp.session -> Session_itp.transID -> bool
  val file_proved : Session_itp.session -> Session_itp.file -> bool
  val any_proved : Session_itp.session -> Session_itp.any -> bool
  val update_goal_node :
    Session_itp.notifier ->
    Session_itp.session -> Session_itp.proofNodeID -> unit
  val update_trans_node :
    Session_itp.notifier ->
    Session_itp.session -> Session_itp.transID -> unit
  val update_proof_attempt :
    ?obsolete:bool ->
    Session_itp.notifier ->
    Session_itp.session ->
    Session_itp.proofNodeID ->
    Whyconf.prover -> Call_provers.prover_result -> unit
  val change_prover :
    Session_itp.notifier ->
    Session_itp.session ->
    Session_itp.proofNodeID -> Whyconf.prover -> Whyconf.prover -> unit
  val find_file_from_path :
    Session_itp.session -> Sysutil.file_path -> Session_itp.file
  val rename_file :
    Session_itp.session ->
    string -> string -> Sysutil.file_path * Sysutil.file_path
end