session_itp.mli 11.6 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11 12


13
(** Proof sessions *)
14 15 16 17 18 19 20 21 22 23 24 25



(** {2 upper level structure of sessions}

   A [session] contains a collection of files, a [file] contains a
collection of theories, a [theory] contains a collection of goals. The
structure of goals remain abstract, each goal being identified by
unique identifiers of type [proofNodeId]

*)

Clément Fumex's avatar
Clément Fumex committed
26
type session
27 28
type file
type theory
Clément Fumex's avatar
Clément Fumex committed
29
type proofNodeID
30
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
31
type transID
32
type proofAttemptID
MARCHE Claude's avatar
MARCHE Claude committed
33
val print_proofAttemptID : Format.formatter -> proofAttemptID -> unit
34
type fileID
35

36
module Hfile: Exthtbl.S with type key = fileID
37 38
module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
39
module Hpan: Exthtbl.S with type key = proofAttemptID
40

41 42 43
type file_path
val string_of_file_path : file_path -> string
val print_file_path : Format.formatter -> file_path -> unit
44

45
(* Any proof node of the tree *)
46 47 48 49 50 51 52
type any =
  | AFile of file
  | ATh of theory
  | ATn of transID
  | APn of proofNodeID
  | APa of proofAttemptID

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

55 56 57 58
type notifier = any -> unit


(** Session *)
59

60
(* Get all the files in the session *)
61
val get_files : session -> file Hfile.t
62
(* Get a single file in the session using its name *)
63
(* val get_file: session -> string -> file *)
64
(* Get directory containing the session *)
Clément Fumex's avatar
Clément Fumex committed
65
val get_dir : session -> string
66

67
(** File *)
68 69
val file_id : file -> fileID
val file_path : file -> file_path
70 71
val file_format : file -> string option
val file_theories : file -> theory list
72
val system_path : session -> file -> string
MARCHE Claude's avatar
MARCHE Claude committed
73
(** the system-dependent absolute path associated to that file *)
74 75

val basename : file_path -> string
76

77 78 79 80 81
(** Theory *)
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file

82
type proof_attempt_node = private {
83 84 85 86
  parent                 : proofNodeID;
  mutable prover         : Whyconf.prover;
  limit                  : Call_provers.resource_limit;
  mutable proof_state    : Call_provers.prover_result option;
87
  (* None means that there is a prover call in progress *)
88
  mutable proof_obsolete : bool;
89 90 91 92
  mutable proof_script   : string option;  (* non empty for external ITP *)
                            }

val set_proof_script : proof_attempt_node -> string -> unit
MARCHE Claude's avatar
MARCHE Claude committed
93

Sylvain Dailler's avatar
Sylvain Dailler committed
94 95 96
(* [is_below s a b] true if a is below b in the session tree *)
val is_below: session -> any -> any -> bool

97
type proof_parent = Trans of transID | Theory of theory
98

99

100 101
val get_task : session -> proofNodeID -> Task.task
val get_task_name_table : session -> proofNodeID -> Task.task * Trans.naming_table
102

Clément Fumex's avatar
Clément Fumex committed
103
val get_transformations : session -> proofNodeID -> transID list
104 105
val get_proof_attempt_ids :
  session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
106 107 108

exception BadID

109
val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node
MARCHE Claude's avatar
MARCHE Claude committed
110
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
111
val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list
Clément Fumex's avatar
Clément Fumex committed
112
val get_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
113

114 115 116
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

117
val get_proof_name : session -> proofNodeID -> Ident.ident
118
val get_proof_expl : session -> proofNodeID -> string
119

120 121 122
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Sylvain Dailler's avatar
Sylvain Dailler committed
123 124
val get_any_parent: session -> any -> any option

125 126 127
(* Answers true if a node is in a detached subtree *)
val is_detached: session -> any -> bool

Sylvain Dailler's avatar
Sylvain Dailler committed
128 129 130 131
(* get the parent theory/file of a proof node *)
val get_encapsulating_theory: session -> any -> theory
val get_encapsulating_file: session -> any -> file

132 133 134
(* Check if a transformation already exists *)
val check_if_already_exists:
    session -> proofNodeID -> string -> string list -> bool
Sylvain Dailler's avatar
Sylvain Dailler committed
135

136 137 138 139
(* true if the exception transformation is fatal (ie: caused by a bug in the
   code of the transformation) *)
val is_fatal: exn -> bool

140 141 142
(** {2 iterators on sessions} *)

val goal_iter_proof_attempt:
Sylvain Dailler's avatar
Sylvain Dailler committed
143
    session -> (proofAttemptID -> proof_attempt_node -> unit) -> proofNodeID -> unit
144 145

val theory_iter_proof_attempt:
Sylvain Dailler's avatar
Sylvain Dailler committed
146
    session -> (proofAttemptID -> proof_attempt_node -> unit) -> theory -> unit
147 148

val file_iter_proof_attempt:
Sylvain Dailler's avatar
Sylvain Dailler committed
149 150 151 152
    session -> (proofAttemptID -> proof_attempt_node -> unit) -> file -> unit

val any_iter_proof_attempt:
    session -> (proofAttemptID -> proof_attempt_node -> unit) -> any -> unit
153 154 155 156 157 158 159 160 161 162 163 164 165

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

val fold_all_any: session -> ('a -> any -> 'a) -> 'a -> any -> 'a
(** [fold_all_any s f acc any] folds on all the subnodes of any *)

val fold_all_session: session -> ('a -> any -> 'a) -> 'a -> 'a
(** [fold_all_session s f acc] folds on the whole session *)


(** {2 session operations} *)

Sylvain Dailler's avatar
Sylvain Dailler committed
166

167
val empty_session : ?from:session -> string -> session
Clément Fumex's avatar
Clément Fumex committed
168 169
(** create an empty_session in the directory specified by the
    argument *)
MARCHE Claude's avatar
MARCHE Claude committed
170 171

val add_file_section :
172
  session -> string -> file_is_detached:bool -> Theory.theory list->
173
  Env.fformat option -> file
174
(** [add_file_section s fn ths] adds a new
Clément Fumex's avatar
Clément Fumex committed
175
    'file' section in session [s], named [fn], containing fresh theory
MARCHE Claude's avatar
MARCHE Claude committed
176
    subsections corresponding to theories [ths]. The tasks of each
177 178 179 180 181 182
    theory nodes generated are computed using [Task.split_theory].

    Note that this function does not read anything from the file
    system. The file name [fn] is taken as is

 *)
183

184 185 186
val read_file :
  Env.env -> ?format:Env.fformat -> string -> Theory.theory list
(* [read_file env ~format fn] parses the source file [fn], types it
187 188
   and extract its theories. A parse error or a typing error is
   signaled with exceptions .  *)
189 190

val merge_files :
191 192 193
  shape_version:int option ->
  Env.env -> session -> session -> exn list * bool * bool
(** [merge_files ~use_shape_version env ses old_ses] merges the file sections
194 195 196 197
    of session [s] with file sections of the same name in old session
    [old_ses]. Recursively, for each theory whose name is identical to
    old theories, it is attempted to associate the old goals,
    proof_attempts and transformations to the goals of the new theory.
198 199 200 201
    Returns a triple [(e,o,d)] such that [e] is the list of parsing or
    typing errors found, [o] is true when obsolete proof attempts
    where found and [d] is true if detached theories, goals or
    transformations were found.  *)
MARCHE Claude's avatar
MARCHE Claude committed
202

Sylvain Dailler's avatar
Sylvain Dailler committed
203 204 205
val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
  Whyconf.prover -> limit:Call_provers.resource_limit -> proofAttemptID
(** [graft_proof_attempt s id pr file l] adds a proof attempt with prover
206
    [pr] and limits [l] in the session [s] as a child of the task
207
    [id]. If there already a proof attempt with the same prover, it
208
    updates it with the limits. It returns the id of the
Sylvain Dailler's avatar
Sylvain Dailler committed
209 210 211 212
    generated proof attempt.
    For manual proofs, it has the same behaviour except that it adds a
    proof_script field equal to [file].
*)
Clément Fumex's avatar
Clément Fumex committed
213

214
exception NoProgress
215
val apply_trans_to_goal :
216 217
  allow_no_effect:bool -> session -> Env.env -> string -> string list ->
  proofNodeID -> Task.task list
218 219
(** [apply_trans_to_goal s env tr args id] applies the transformation
  [tr] with arguments [args] to the goal [id], and returns the
220
  subtasks.  raises [NoProgress] if [allow_no_effect] is false and [tr]
221
  returns the task unchanged *)
222

223
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
224
  Task.task list -> transID
225
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
226
    child of the task [id] of the session [s]. [l] is the list of
227
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
228
*)
MARCHE Claude's avatar
MARCHE Claude committed
229

Clément Fumex's avatar
Clément Fumex committed
230 231 232
val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
(** [remove_proof_attempt s id pr] removes the proof attempt from the
    prover [pr] from the proof node [id] of the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
233

Clément Fumex's avatar
Clément Fumex committed
234 235 236
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
237

238 239 240
val mark_obsolete: session -> proofAttemptID -> unit
(** [mark_obsolete s id] marks [id] as obsolete in [s] *)

Clément Fumex's avatar
Clément Fumex committed
241 242
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
243

244
val load_session : string -> session * int option
Clément Fumex's avatar
Clément Fumex committed
245
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
246 247
    tasks are initialised to None

248
    The second result is the shape version read from disk, if any
Clément Fumex's avatar
Clément Fumex committed
249 250 251 252 253 254 255

    raises [SessionFileError msg] if the database file cannot be read
    correctly.

    raises [ShapesFileError msg] if the database extra file for shapes
    cannot be read.
 *)
256

MARCHE Claude's avatar
MARCHE Claude committed
257
(** {2 remove} *)
258

259 260
exception RemoveError

261 262 263 264 265 266
val remove_subtree: notification:notifier -> removed:notifier ->
                    session -> any -> unit
(** [remove_subtree s a ~removed ~notification] remove the subtree
    originating from node [a] in session [s]. the notifier [removed] is
    called on each removed node, and notifier [notification] on nodes
    whose proved state changes.
267

268
    raises [RemoveError] when removal is forbidden, e.g. when called on
269
    a file, a theory or a goal that is not detached
270
 *)
271

272
(** {2 proved status} *)
273

274
val pa_proved : session -> proofAttemptID -> bool
275 276 277 278 279 280 281
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
282 283 284
(** updates the proved status of the given goal node. If necessary,
    propagates the update to ancestors. [notifier] is called on all
    nodes whose status changes. *)
285 286

val update_trans_node : notifier -> session -> transID -> unit
287 288 289
(** updates the proved status of the given transformation node. If
    necessary, propagates the update to ancestors. [notifier] is
    called on all nodes whose status changes *)
290

291
val update_proof_attempt : ?obsolete:bool -> notifier -> session -> proofNodeID ->
292 293 294 295
  Whyconf.prover -> Call_provers.prover_result -> unit
(** [update_proof_attempt ?obsolete s id pr st] update the status of the
    corresponding proof attempt with [st].
    If [obsolete] is set to true, it marks the proof_attempt obsolete
296
    directly (useful for interactive prover).
297 298 299 300 301 302 303
*)

val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyconf.prover -> unit
(** [change_prover s id opr npr] changes the prover of the proof
   attempt using prover [opr] by the new prover [npr]. Proof attempt
   status is set to obsolete.
 *)
304

MARCHE Claude's avatar
MARCHE Claude committed
305
(** Extra session update operations *)
306

307 308 309 310
val find_file_from_path: session -> string list -> file
(** raise [Not_found] of path does not appear in session *)

val rename_file: session -> string -> string -> (string list) * (string list)
311
(** [rename_file s from_file to_file] renames the
MARCHE Claude's avatar
MARCHE Claude committed
312
    file section in session [s] named [from_file] into [to_file]
313
    @return the paths relative to the session dir
MARCHE Claude's avatar
MARCHE Claude committed
314 315 316 317 318 319

    Beware that this function does not have any effect on the user's
    file system: if the considered files corresponds the real files,
    they must be renamed independently. See for example the use in
    [why3session/why3session_update].
  *)