why3session_lib.mli 3.88 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12 13 14

open Why3
open Whyconf

15 16
val verbose: Debug.flag

17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
type spec_list = (Arg.key * Arg.spec * Arg.doc) list

type cmd =
    {
      cmd_spec : spec_list;
      cmd_desc : string;
      cmd_name : string;
      cmd_run  : unit -> unit;
    }



(** {2 Anonymous argument} *)
val iter_files : (string -> unit) -> unit
val anon_fun : Arg.anon_fun

(** {2 Spec for version, debug} *)
34
(* val simple_spec : spec_list *)
35

MARCHE Claude's avatar
MARCHE Claude committed
36
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
37
val read_simple_spec : unit -> bool
38
(** return if we must exit *)
MARCHE Claude's avatar
MARCHE Claude committed
39
*)
40

41 42
(** {2 Spec for configuration, loadpath} *)
val common_options : spec_list
43 44 45 46

val read_env_spec : unit -> Env.env * Whyconf.config * bool
(** read_simple_spec also *)

47 48
val read_session : string -> Session_itp.session * bool

49
val read_update_session :
50 51
  allow_obsolete:bool -> Env.env ->
  Whyconf.config -> string ->
52
  Controller_itp.controller * bool * bool
53 54

(** {2 Spec for filtering } *)
55
type filter_prover
56 57

val read_opt_prover : string -> filter_prover
58 59
val prover_of_filter_prover : config -> filter_prover -> Why3.Whyconf.prover
val provers_of_filter_prover : config -> filter_prover -> Why3.Whyconf.Sprover.t
60

61
type filters
62 63 64 65 66

val filter_spec : spec_list

val read_filter_spec : Whyconf.config -> filters * bool

67
val theory_iter_proof_attempt_by_filter :
68
  Session_itp.session ->
69
  filters ->
70 71
  (Session_itp.proof_attempt_node -> unit) -> Session_itp.theory -> unit

72
val session_iter_proof_attempt_by_filter :
73
  Session_itp.session ->
74
  filters ->
75
  (Session_itp.proof_attempt_node -> unit) ->  unit
76 77 78 79 80


(* quite ad-hoc *)
type filter_three = | FT_Yes | FT_No | FT_All
val set_filter_verified_goal : filter_three -> unit
81 82 83 84

(** force obsolete *)
val opt_force_obsolete : bool ref
val force_obsolete_spec : spec_list
85 86 87 88 89 90 91 92


(** ask yes/no question to the user *)
val ask_yn : unit -> bool

val ask_yn_nonblock : callback:(bool -> unit) -> (unit -> bool)
(** call the callback when an answer have been given,
    return true if it must be retried *)
93 94

val get_used_provers : Session_itp.session -> Whyconf.Sprover.t
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
(** [get_used_provers s] returns the set of provers used somewhere in
    session [s] *)

val get_used_provers_file : Session_itp.session -> Session_itp.file
                              -> Whyconf.Sprover.t
(** [get_used_provers_file s f] returns the set of provers used
    somewhere in the file [f] of session [s] *)

val get_used_provers_theory : Session_itp.session -> Session_itp.theory
                              -> Whyconf.Sprover.t
(** [get_used_provers_theory s th] returns the set of provers used
    somewhere in the theory [th] of session [s] *)

val get_used_provers_goal : Session_itp.session -> Session_itp.proofNodeID
                            -> Whyconf.Sprover.t
(** [get_used_provers_goal s g] returns the set of provers used
    somewhere under the goal [g] of session [s] *)


val goal_depth : Session_itp.session -> Session_itp.proofNodeID -> int
(** [goal_depth s g] returns the depth of the tree under goal
    [g] in session [s] *)

val theory_depth : Session_itp.session -> Session_itp.theory -> int
(** [theory_depth s th] returns the depth of the tree under theory
    [th] in session [s] *)

val file_depth : Session_itp.session -> Session_itp.file -> int
(** [file_depth s f] returns the depth of the tree under file [f] in
    session [s] *)