why3 1.0.0 · OCaml Package

type session

type file

type theory

type proofNodeID

val print_proofNodeID : Format.formatter -> proofNodeID -> unit

type transID

type proofAttemptID

val print_proofAttemptID : Format.formatter -> proofAttemptID -> unit

module Hpn : sig ... end

module Htn : sig ... end

module Hpan : sig ... end

type any =

| AFile of file
| ATh of theory
| ATn of transID
| APn of proofNodeID
| APa of proofAttemptID

val fprintf_any : Format.formatter -> any -> unit

type notifier = any -> unit

val get_files : session -> file Wstdlib.Hstr.t

val get_file : session -> string -> file

val get_dir : session -> string

val file_name : file -> string

val file_format : file -> string option

val file_theories : file -> theory list

val theory_name : theory -> Ident.ident

val theory_goals : theory -> proofNodeID list

val theory_parent : session -> theory -> file

type proof_attempt_node = private {

parent : proofNodeID;
mutable prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
mutable proof_obsolete : bool;
mutable proof_script : string option;

}

val set_proof_script : proof_attempt_node -> string -> unit

val is_below : session -> any -> any -> bool

type proof_parent =

| Trans of transID
| Theory of theory

val get_task : session -> proofNodeID -> Task.task

val get_task_name_table : 
  session ->
  proofNodeID ->
  Task.task * Trans.naming_table

val get_transformations : session -> proofNodeID -> transID list

val get_proof_attempt_ids : 
  session ->
  proofNodeID ->
  proofAttemptID Whyconf.Hprover.t

exception BadID

val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node

val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID

val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list

val get_sub_tasks : session -> transID -> proofNodeID list

val get_transf_args : session -> transID -> string list

val get_transf_name : session -> transID -> string

val get_proof_name : session -> proofNodeID -> Ident.ident

val get_proof_expl : session -> proofNodeID -> string

val get_proof_parent : session -> proofNodeID -> proof_parent

val get_trans_parent : session -> transID -> proofNodeID

val get_any_parent : session -> any -> any option

val is_detached : session -> any -> bool

val get_encapsulating_theory : session -> any -> theory

val get_encapsulating_file : session -> any -> file

val check_if_already_exists : 
  session ->
  proofNodeID ->
  string ->
  string list ->
  bool

val goal_iter_proof_attempt : 
  session ->
  (proofAttemptID -> proof_attempt_node -> unit) ->
  proofNodeID ->
  unit

val theory_iter_proof_attempt : 
  session ->
  (proofAttemptID -> proof_attempt_node -> unit) ->
  theory ->
  unit

val file_iter_proof_attempt : 
  session ->
  (proofAttemptID -> proof_attempt_node -> unit) ->
  file ->
  unit

val any_iter_proof_attempt : 
  session ->
  (proofAttemptID -> proof_attempt_node -> unit) ->
  any ->
  unit

val session_iter_proof_attempt : 
  (proofAttemptID -> proof_attempt_node -> unit) ->
  session ->
  unit

val fold_all_any : session -> ('a -> any -> 'a) -> 'a -> any -> 'a

val fold_all_session : session -> ('a -> any -> 'a) -> 'a -> 'a

val empty_session : ?from:session -> string -> session

val add_file_section : 
  session ->
  string ->
  file_is_detached:bool ->
  Theory.theory list ->
  Env.fformat option ->
  file

val read_file : Env.env -> ?format:Env.fformat -> string -> Theory.theory list

val merge_files : 
  use_shapes:bool ->
  Env.env ->
  session ->
  session ->
  exn list * bool * bool

val graft_proof_attempt : 
  ?file:string ->
  session ->
  proofNodeID ->
  Whyconf.prover ->
  limit:Call_provers.resource_limit ->
  proofAttemptID

exception NoProgress

val apply_trans_to_goal : 
  allow_no_effect:bool ->
  session ->
  Env.env ->
  string ->
  string list ->
  proofNodeID ->
  Task.task list

val graft_transf : 
  session ->
  proofNodeID ->
  string ->
  string list ->
  Task.task list ->
  transID

val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit

val remove_transformation : session -> transID -> unit

val mark_obsolete : session -> proofAttemptID -> unit

val save_session : session -> unit

val load_session : string -> session * bool

exception RemoveError

val remove_subtree : 
  notification:notifier ->
  removed:notifier ->
  session ->
  any ->
  unit

val pa_proved : session -> proofAttemptID -> bool

val th_proved : session -> theory -> bool

val pn_proved : session -> proofNodeID -> bool

val tn_proved : session -> transID -> bool

val file_proved : session -> file -> bool

val any_proved : session -> any -> bool

val update_goal_node : notifier -> session -> proofNodeID -> unit

val update_trans_node : notifier -> session -> transID -> unit

val update_proof_attempt : 
  ?obsolete:bool ->
  notifier ->
  session ->
  proofNodeID ->
  Whyconf.prover ->
  Call_provers.prover_result ->
  unit

val change_prover : 
  notifier ->
  session ->
  proofNodeID ->
  Whyconf.prover ->
  Whyconf.prover ->
  unit

package why3