session_itp.mli 7.38 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

Clément Fumex's avatar
Clément Fumex committed
19
type proofNodeID
MARCHE Claude's avatar
MARCHE Claude committed
20
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
21
type transID
22
type proofAttemptID
23 24 25

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

28 29 30
type theory

type file = private {
Clément Fumex's avatar
Clément Fumex committed
31 32 33 34
  file_name              : string;
  file_format            : string option;
  file_theories          : theory list;
  file_detached_theories : theory list;
35 36
}

37
(* Any proof node of the tree *)
38 39 40 41 42 43 44
type any =
  | AFile of file
  | ATh of theory
  | ATn of transID
  | APn of proofNodeID
  | APa of proofAttemptID

45
(** Session / File *)
46

47
(* Get all the files in the session *)
48
val get_files : session -> file Stdlib.Hstr.t
49 50 51
(* 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
52 53
val get_dir : session -> string
val get_shape_version : session -> int
54

55 56 57 58 59 60
(** 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

61
type proof_attempt_node = private {
62
  parent              : proofNodeID;
63 64 65 66
  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
67
  mutable proof_obsolete      : bool;
68 69
  proof_script        : string option;  (* non empty for external ITP *)
}
MARCHE Claude's avatar
MARCHE Claude committed
70

71 72 73
val theory_iter_proof_attempt:
    session -> (proof_attempt_node -> unit) -> theory -> unit

74 75
val session_iter_proof_attempt:
    (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
MARCHE Claude's avatar
MARCHE Claude committed
76

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

80
type proof_parent = Trans of transID | Theory of theory
81

82
val get_task : session -> proofNodeID -> Task.task
83
val get_table : session -> proofNodeID -> Task.names_table option
84

Clément Fumex's avatar
Clément Fumex committed
85
val get_transformations : session -> proofNodeID -> transID list
86 87
val get_proof_attempt_ids :
  session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
88
val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node
MARCHE Claude's avatar
MARCHE Claude committed
89
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
90
val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list
Clément Fumex's avatar
Clément Fumex committed
91
val get_sub_tasks : session -> transID -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
92
val get_detached_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
93

94 95 96
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

97
val get_proof_name : session -> proofNodeID -> Ident.ident
MARCHE Claude's avatar
MARCHE Claude committed
98
val get_proof_expl : session -> proofNodeID -> string
99

100 101 102
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

103
val get_detached_trans : session -> proofNodeID -> transID list
Sylvain Dailler's avatar
Sylvain Dailler committed
104 105
val get_any_parent: session -> any -> any option

106 107 108
(* Answers true if a node is in a detached subtree *)
val is_detached: session -> any -> bool

Sylvain Dailler's avatar
Sylvain Dailler committed
109 110 111 112 113
(* get the parent theory/file of a proof node *)
val get_encapsulating_theory: session -> any -> theory
val get_encapsulating_file: session -> any -> file


114
exception BadCopyDetached of string
Sylvain Dailler's avatar
Sylvain Dailler committed
115 116 117 118 119

(** [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
120 121 122
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
123 124

val add_file_section :
125
  session -> string -> (Theory.theory list) ->
126
  Env.fformat option -> unit
127
(** [add_file_section s fn ths] adds a new
Clément Fumex's avatar
Clément Fumex committed
128
    'file' section in session [s], named [fn], containing fresh theory
MARCHE Claude's avatar
MARCHE Claude committed
129
    subsections corresponding to theories [ths]. The tasks of each
130 131 132 133 134 135 136 137 138 139 140 141 142
    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
143

Sylvain Dailler's avatar
Sylvain Dailler committed
144 145 146
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
147
    [pr] and limits [l] in the session [s] as a child of the task
148
    [id]. If there already a proof attempt with the same prover, it
149
    updates it with the limits. It returns the id of the
Sylvain Dailler's avatar
Sylvain Dailler committed
150 151 152 153
    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
154

155 156 157 158 159 160 161
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
162

163
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
164
  Task.task list -> transID
165
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
166
    child of the task [id] of the session [s]. [l] is the list of
167
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
168
*)
MARCHE Claude's avatar
MARCHE Claude committed
169

Clément Fumex's avatar
Clément Fumex committed
170 171 172
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
173

Clément Fumex's avatar
Clément Fumex committed
174 175 176
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
177

178 179 180
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
181 182
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
183

Clément Fumex's avatar
Clément Fumex committed
184
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
185
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
186 187 188 189 190 191 192 193 194 195
    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.
 *)
196 197 198 199 200 201 202 203

exception RemoveError

val remove_subtree: session -> any -> notification:(any -> unit) -> unit
(** [remove_subtree s a notification] remove the subtree originating from a in
    session s then call the notification function (used to notify the ide.

    If called on a theory or proof node, raise RemoveError *)
204 205 206

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 *)