session_itp.mli 8.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16




(** {1 New Proof sessions ("Refectoire")} *)


(** {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
17
type session
18 19
type file
type theory
Clément Fumex's avatar
Clément Fumex committed
20
type proofNodeID
MARCHE Claude's avatar
MARCHE Claude committed
21
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
22
type transID
23
type proofAttemptID
24 25 26

module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
27
module Hpan: Exthtbl.S with type key = proofAttemptID
28

29

30
(* Any proof node of the tree *)
31 32 33 34 35 36 37
type any =
  | AFile of file
  | ATh of theory
  | ATn of transID
  | APn of proofNodeID
  | APa of proofAttemptID

38 39 40 41
type notifier = any -> unit


(** Session *)
42

43
(* Get all the files in the session *)
44
val get_files : session -> file Stdlib.Hstr.t
45 46 47
(* Get a single file in the session using its name *)
val get_file: session -> string -> file
(* Get directory containing the session *)
Clément Fumex's avatar
Clément Fumex committed
48 49
val get_dir : session -> string
val get_shape_version : session -> int
50

51 52 53 54 55 56
(** File *)
val file_name : file -> string
val file_format : file -> string option
val file_theories : file -> theory list
val file_detached_theories : file -> theory list

57 58 59 60 61 62
(** Theory *)
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file

63
type proof_attempt_node = private {
64
  parent              : proofNodeID;
65 66 67 68
  prover              : Whyconf.prover;
  limit               : Call_provers.resource_limit;
  mutable proof_state : Call_provers.prover_result option;
  (* None means that the call was not done or never returned *)
Clément Fumex's avatar
Clément Fumex committed
69
  mutable proof_obsolete      : bool;
70 71
  proof_script        : string option;  (* non empty for external ITP *)
}
MARCHE Claude's avatar
MARCHE Claude committed
72

MARCHE Claude's avatar
MARCHE Claude committed
73 74 75
val goal_iter_proof_attempt:
    session -> (proof_attempt_node -> unit) -> proofNodeID -> unit

76 77 78
val theory_iter_proof_attempt:
    session -> (proof_attempt_node -> unit) -> theory -> unit

MARCHE Claude's avatar
MARCHE Claude committed
79 80 81
val file_iter_proof_attempt:
    session -> (proof_attempt_node -> unit) -> file -> unit

82 83
val session_iter_proof_attempt:
    (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
MARCHE Claude's avatar
MARCHE Claude committed
84

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

88
type proof_parent = Trans of transID | Theory of theory
89

90
val get_task : session -> proofNodeID -> Task.task
91
val get_table : session -> proofNodeID -> Task.names_table option
92

Clément Fumex's avatar
Clément Fumex committed
93
val get_transformations : session -> proofNodeID -> transID list
94 95
val get_proof_attempt_ids :
  session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
96
val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node
MARCHE Claude's avatar
MARCHE Claude committed
97
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
98
val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list
Clément Fumex's avatar
Clément Fumex committed
99
val get_sub_tasks : session -> transID -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
100
val get_detached_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
101

102 103 104
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

105
val get_proof_name : session -> proofNodeID -> Ident.ident
MARCHE Claude's avatar
MARCHE Claude committed
106
val get_proof_expl : session -> proofNodeID -> string
107

108 109 110
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

111
val get_detached_trans : session -> proofNodeID -> transID list
Sylvain Dailler's avatar
Sylvain Dailler committed
112 113
val get_any_parent: session -> any -> any option

114 115 116
(* Answers true if a node is in a detached subtree *)
val is_detached: session -> any -> bool

Sylvain Dailler's avatar
Sylvain Dailler committed
117 118 119 120 121
(* get the parent theory/file of a proof node *)
val get_encapsulating_theory: session -> any -> theory
val get_encapsulating_file: session -> any -> file


122
exception BadCopyDetached of string
Sylvain Dailler's avatar
Sylvain Dailler committed
123 124 125 126 127

(** [copy s pn] copy pn and add the copy as detached subgoal of its parent *)
val copy_proof_node_as_detached: session -> proofNodeID -> proofNodeID
val copy_structure: notification:(parent:any -> any -> unit) -> session -> any -> any -> unit

Clément Fumex's avatar
Clément Fumex committed
128 129 130
val empty_session : ?shape_version:int -> string -> session
(** create an empty_session in the directory specified by the
    argument *)
MARCHE Claude's avatar
MARCHE Claude committed
131 132

val add_file_section :
133
  session -> string -> (Theory.theory list) ->
134
  Env.fformat option -> unit
135
(** [add_file_section s fn ths] adds a new
Clément Fumex's avatar
Clément Fumex committed
136
    'file' section in session [s], named [fn], containing fresh theory
MARCHE Claude's avatar
MARCHE Claude committed
137
    subsections corresponding to theories [ths]. The tasks of each
138 139 140 141 142 143 144 145 146 147 148 149 150
    theory nodes generated are computed using [Task.split_theory]. *)

val merge_file_section :
  use_shapes:bool -> old_ses:session -> old_theories:theory list ->
  env:Env.env -> session -> string -> Theory.theory list ->
  Env.fformat option -> unit
(** [merge_file_section ~old_s ~old_theories ~env ~pn_callpack s fn
    ths] adds a new 'file' section in session [s], named [fn],
    containing fresh theory subsections corresponding to theories
    [ths]. For each theory whose name is identical to one theory of
    old_ths, it is attempted to associate the old goals,
    proof_attempts and transformations to the goals of the new
    theory *)
MARCHE Claude's avatar
MARCHE Claude committed
151

Sylvain Dailler's avatar
Sylvain Dailler committed
152 153 154
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
155
    [pr] and limits [l] in the session [s] as a child of the task
156
    [id]. If there already a proof attempt with the same prover, it
157
    updates it with the limits. It returns the id of the
Sylvain Dailler's avatar
Sylvain Dailler committed
158 159 160 161
    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
162

163 164 165 166 167 168 169
val update_proof_attempt : ?obsolete:bool -> session -> proofNodeID ->
  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
    direclty (useful for interactive prover).
*)
MARCHE Claude's avatar
MARCHE Claude committed
170

171
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
172
  Task.task list -> transID
173
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
174
    child of the task [id] of the session [s]. [l] is the list of
175
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
176
*)
MARCHE Claude's avatar
MARCHE Claude committed
177

Clément Fumex's avatar
Clément Fumex committed
178 179 180
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
181

Clément Fumex's avatar
Clément Fumex committed
182 183 184
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
185

186 187 188
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
189 190
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
191

Clément Fumex's avatar
Clément Fumex committed
192
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
193
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
194 195 196 197 198 199 200 201 202 203
    tasks are initialised to None

    The returned boolean is set when there was shapes read from disk.

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

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

exception RemoveError

207 208 209 210 211 212
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.
213

214 215 216
    raises [RemoveError] when removal is forbidden, e.g. when called on
    a theory, or a goal that is not detached
 *)
217 218 219

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 *)
220 221 222

val fold_all_session: session -> ('a -> any -> 'a) -> 'a -> 'a
(** [fold_all_session s f acc] folds on the whole session *)
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240

(* proved status *)

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

(* status update *)

val update_goal_node : notifier -> session -> proofNodeID -> unit
(** [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 *)

val update_trans_node : notifier -> session -> transID -> unit
(** [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 *)