HarpoonState (beluga.Harpoon.HarpoonState)

module Disambiguation_state =
  Beluga_parser.Disambiguation_state.Disambiguation_state

module Indexing_state = Beluga.Index_state.Indexing_state

type t

type substate = {

session : Session.t;
theorem : Theorem.t;
proof_state : Beluga_syntax.Synint.Comp.proof_state;

}

exception No_session

exception No_theorem of Session.t

exception No_subgoal of {

session : Session.t;
theorem : Theorem.t;

}

val make : 
  (Disambiguation_state.state Beluga_syntax.Id.Prog.Hashtbl.t
   * Disambiguation_state.state) ->
  (Indexing_state.state Beluga_syntax.Id.Prog.Hashtbl.t * Indexing_state.state) ->
  Options.save_mode ->
  Options.interaction_mode ->
  string ->
  string list ->
  Io.t ->
  Beluga_syntax.Synint.Comp.open_subgoal list ->
  t

val with_io : t -> (Io.t -> 'a) -> 'a

val printf : t -> ('a, Support.Format.formatter, unit) Stdlib.format -> 'a

Prints a message to the user.

val session_list : t -> Session.t list

Gets a list of all sessions in the prover.

val defer_session : t -> unit

Moves the current session to the bottom of the session stack, selecting the next one.

val session_configuration_wizard : t -> bool

Configures a new session interactively and adds it to the state. Returns whether the new session was indeed added. A session is not added when the user aborts the configuration process.

val select_theorem : t -> Beluga_syntax.Name.t -> bool

val automation_state : t -> Automation.State.t

val interaction_mode : t -> Options.interaction_mode

Gets the interaction mode of the prover.

val next_substate : t -> substate

val is_complete : t -> bool

Decides whether there are any sessions in the theorem.

val on_session_completed : t -> Session.t -> unit

To be called by the REPL when a session is completed. This function analyzes the current save_mode and proceeds accordingly.

val serialize : t -> substate -> unit

Serializes the current state back to the loaded signature, preserving prover focus on the given state substate.

val fmt_ppr_session_list : Support.Format.formatter -> t -> unit

Prints a vertical, enumerated list of all sessions in this state, together with every theorem within each session.